# Initializing proof state
# Scanning for AC axioms
#
#cnf(i_0_393, plain, (x2_s_1(esk148_0))).
#
#cnf(i_0_399, plain, (x2_s_2(esk153_0))).
#
#cnf(i_0_203, plain, (l_s_13(esk64_0))).
#
#cnf(i_0_460, negated_conjecture, (~join_pat(X1))).
#
#cnf(i_0_12, plain, (x2_s_5(esk5_0))).
#
#cnf(i_0_100, plain, (l_s_11(esk28_0))).
#
#cnf(i_0_294, plain, (x2_s_3(esk110_0))).
#
#cnf(i_0_406, plain, (~x2_s_2(X1)|~x2_s_1(X1))).
#
#cnf(i_0_258, plain, (l_s_3(esk86_0))).
#
#cnf(i_0_210, plain, (a2_s_2(esk67_0))).
#
#cnf(i_0_209, plain, (l_s_0(esk66_0))).
#
#cnf(i_0_487, plain, (~x2_s_1(esk153_0))).
#
#cnf(i_0_461, negated_conjecture, (new(esk178_0))).
#
#cnf(i_0_93, plain, (x2_s_0(esk27_0))).
#
#cnf(i_0_404, plain, (a2_s_0(esk155_0))).
#
#cnf(i_0_405, plain, (~code_ok(X1)|~x2_s_1(X1))).
#
#cnf(i_0_250, plain, (l_s_15(esk83_0))).
#
#cnf(i_0_289, plain, (l_s_2(esk106_0))).
#
#cnf(i_0_43, plain, (l_s_4(esk17_0))).
#
#cnf(i_0_11, plain, (~l_s_13(X1)|~x2_s_1(X1))).
#
#cnf(i_0_44, plain, (x3_s_4(esk18_0))).
#
#cnf(i_0_284, plain, (x2_s_9(esk105_0))).
#
#cnf(i_0_397, plain, (l_s_5(esk152_0))).
#
#cnf(i_0_488, plain, (~x2_s_1(esk64_0))).
#
#cnf(i_0_291, plain, (l_s_6(esk107_0))).
#
#cnf(i_0_231, plain, (l_s_12(esk75_0))).
#
#cnf(i_0_74, plain, (a2_s_1(esk20_0))).
#
#cnf(i_0_10, plain, (~set_status(X1)|~x2_s_1(X1))).
#
#cnf(i_0_295, plain, (l_s_8(esk111_0))).
#
#cnf(i_0_349, plain, (l_s_14(esk132_0))).
#
#cnf(i_0_378, plain, (x2_s_6(esk146_0))).
#
#cnf(i_0_195, plain, (~a2_s_0(X1)|~x2_s_1(X1))).
#
#cnf(i_0_157, plain, (x2_s_7(esk51_0))).
#
#cnf(i_0_185, plain, (l_s_10(esk58_0))).
#
#cnf(i_0_439, plain, (x2_s_8(esk170_0))).
#
#cnf(i_0_489, plain, (~x2_s_1(esk155_0))).
#
#cnf(i_0_394, plain, (l_s_9(esk149_0))).
#
#cnf(i_0_279, plain, (l_s_7(esk102_0))).
#
#cnf(i_0_149, plain, (l_s_1(esk48_0))).
#
#cnf(i_0_415, plain, (~x2_e_1(X1)|~x2_s_1(X1))).
#
#cnf(i_0_344, plain, (code_ok(esk129_0)|~tau_15(X1))).
#
#cnf(i_0_119, plain, (set_status(esk35_0)|~tau_16(X1))).
#
#cnf(i_0_13, plain, (storno(esk6_0)|~tau_5(X1))).
#
#cnf(i_0_433, plain, (~x2_s_7(X1)|~x2_s_1(X1))).
#
#cnf(i_0_408, plain, (release(esk156_0)|~tau_14(X1))).
#
#cnf(i_0_247, plain, (a2_e_2(esk82_0)|~reject(X1))).
#
#cnf(i_0_401, plain, (a2_e_2(esk154_0)|~code_nok(X1))).
#
#cnf(i_0_490, plain, (~x2_s_1(esk51_0))).
#
#cnf(i_0_90, plain, (a2_e_1(esk25_0)|~a2_e_2(X1))).
#
#cnf(i_0_303, plain, (a2_e_1(esk114_0)|~storno(X1))).
#
#cnf(i_0_227, plain, (x2_e_2(esk74_0)|~manual(X1))).
#
#cnf(i_0_432, plain, (~x2_e_7(X1)|~x2_s_1(X1))).
#
#cnf(i_0_229, plain, (x2_e_2(esk74_0)|~fin(X1))).
#
#cnf(i_0_78, plain, (new(esk22_0)|~tau_0(X1))).
#
#cnf(i_0_452, plain, (x2_e_0(esk175_0)|~x2_e_9(X1))).
#
#cnf(i_0_252, plain, (~a2_e_0(X1)|~x2_s_1(X1))).
##
#cnf(i_0_343, plain, (x2_e_9(esk128_0)|~tau_19(X1))).
#
#cnf(i_0_341, plain, (x2_e_9(esk128_0)|~delete(X1))).
#
#cnf(i_0_58, plain, (~code_ok(X1)|~x2_s_2(X1))).
#
#cnf(i_0_278, plain, (~tau_21(X1))).
#
#cnf(i_0_226, plain, (code_error(esk73_0)|~tau_4(X1))).
#
#cnf(i_0_143, plain, (x2_e_3(esk44_0)|~tau_2(X1))).
#
#cnf(i_0_137, plain, (~l_s_13(X1)|~x2_s_2(X1))).
#
#cnf(i_0_141, plain, (x2_e_3(esk44_0)|~x3_e_4(X1))).
#
#cnf(i_0_305, plain, (manual(esk115_0)|~tau_13(X1))).
#
#cnf(i_0_151, plain, (fin(esk49_0)|~tau_12(X1))).
#
#cnf(i_0_491, plain, (~x2_s_2(esk64_0))).
#
#cnf(i_0_120, plain, (reopen(esk36_0)|~tau_9(X1))).
#
#cnf(i_0_444, plain, (billed(esk171_0)|~tau_1(X1))).
#
#cnf(i_0_152, plain, (reject(esk50_0)|~tau_7(X1))).
#
#cnf(i_0_136, plain, (~set_status(X1)|~x2_s_2(X1))).
#
#cnf(i_0_145, plain, (x2_e_5(esk46_0)|~code_error(X1))).
#
#cnf(i_0_147, plain, (x2_e_5(esk46_0)|~tau_3(X1))).
#
#cnf(i_0_374, plain, (x2_e_6(esk144_0)|~tau_8(X1))).
#
#cnf(i_0_23, plain, (~l_s_11(X1)|~x2_s_2(X1))).
#
#cnf(i_0_164, plain, (x2_e_1(esk52_0)|~code_ok(X1))).
#
#cnf(i_0_162, plain, (x2_e_1(esk52_0)|~set_status(X1))).
#
#cnf(i_0_106, plain, (code_nok(esk29_0)|~tau_6(X1))).
#
#cnf(i_0_492, plain, (~x2_s_2(esk28_0))).
#
#cnf(i_0_281, plain, (change_end(esk103_0)|~tau_11(X1))).
#
#cnf(i_0_355, plain, (delete(esk136_0)|~tau_20(X1))).
#
#cnf(i_0_182, plain, (x3_e_4(esk57_0)|~x2_e_6(X1))).
#
#cnf(i_0_22, plain, (~release(X1)|~x2_s_2(X1))).
#
#cnf(i_0_178, plain, (x3_e_4(esk57_0)|~change_end(X1))).
#
#cnf(i_0_180, plain, (x3_e_4(esk57_0)|~change_diagn(X1))).
#
#cnf(i_0_187, plain, (x2_e_7(esk59_0)|~tau_17(X1))).
#
#cnf(i_0_242, plain, (~x2_s_3(X1)|~x2_s_2(X1))).
#
#cnf(i_0_186, plain, (x2_e_7(esk59_0)|~zdbc_behan(X1))).
#
#cnf(i_0_454, plain, (change_diagn(esk176_0)|~tau_10(X1))).
#
#cnf(i_0_309, plain, (x2_e_8(esk117_0)|~tau_18(X1))).
#
#cnf(i_0_493, plain, (~x2_s_2(esk110_0))).
#
#cnf(i_0_204, plain, (a2_e_0(esk65_0)|~billed(X1))).
#
#cnf(i_0_212, plain, (a2_e_0(esk68_0)|~x2_e_7(X1))).
#
#cnf(i_0_282, plain, (code_ok(esk104_0)|~l_s_12(X1))).
#
#cnf(i_0_327, plain, (~x2_e_2(X1)|~x2_s_2(X1))).
#
#cnf(i_0_92, plain, (set_status(esk26_0)|~l_s_13(X1))).
#
#cnf(i_0_198, plain, (storno(esk63_0)|~l_s_3(X1))).
#
#cnf(i_0_411, plain, (release(esk157_0)|~l_s_11(X1))).
#
#cnf(i_0_375, plain, (~manual(X1)|~x2_s_2(X1))).
#
#cnf(i_0_248, plain, (a2_e_2(esk82_0)|~l_s_5(X1))).
#
#cnf(i_0_402, plain, (a2_e_2(esk154_0)|~l_s_4(X1))).
#
#cnf(i_0_91, plain, (a2_e_1(esk25_0)|~a2_s_2(X1))).
#
#cnf(i_0_241, plain, (~fin(X1)|~x2_s_2(X1))).
#
#cnf(i_0_304, plain, (a2_e_1(esk114_0)|~l_s_3(X1))).
#
#cnf(i_0_230, plain, (x2_e_2(esk74_0)|~x2_s_3(X1))).
#
#cnf(i_0_228, plain, (x2_e_2(esk74_0)|~l_s_10(X1))).
#
#cnf(i_0_59, plain, (~l_s_12(X1)|~x2_s_2(X1))).
#
#cnf(i_0_148, plain, (new(esk47_0)|~l_s_0(X1))).
#
#cnf(i_0_453, plain, (x2_e_0(esk175_0)|~a2_s_0(X1))).
#
#cnf(i_0_451, plain, (x2_e_0(esk175_0)|~l_s_15(X1))).
#
#cnf(i_0_506, plain, (~x2_s_2(esk75_0))).
#
#cnf(i_0_342, plain, (x2_e_9(esk128_0)|~l_s_14(X1))).
#
#cnf(i_0_350, plain, (~l_s_15(X1))).

# Proof found!
# SZS status Theorem

