%------------------------------------------------------------------------------
% File : Etableau---0.67
% Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Apr 1 02:13:21 AM UTC 2025
% Result : Theorem 8.37s 1.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0.
% 0.06/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Mar 31 14:58:06 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.45 # No SInE strategy applied
% 0.20/0.45 # Auto-Mode selected heuristic G_E___208_C18__C_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
% 0.20/0.45 # and selection function SelectComplexExceptUniqMaxHorn.
% 0.20/0.45 #
% 0.20/0.45 # Presaturation interreduction done
% 0.20/0.45 # Number of axioms: 555 Number of unprocessed: 551
% 0.20/0.45 # Tableaux proof search.
% 0.20/0.45 # APR header successfully linked.
% 0.20/0.45 # Hello from C++
% 0.20/0.45 # The folding up rule is enabled...
% 0.20/0.45 # Local unification is enabled...
% 0.20/0.45 # Any saturation attempts will use folding labels...
% 0.20/0.45 # 551 beginning clauses after preprocessing and clausification
% 0.20/0.45 # Creating start rules for all 3 conjectures.
% 0.20/0.45 # There are 3 start rule candidates:
% 0.20/0.45 # Found 47 unit axioms.
% 0.20/0.45 # Unsuccessfully attempted saturation on 1 start tableaux, moving on.
% 0.20/0.45 # 3 start rule tableaux created.
% 0.20/0.45 # 504 extension rule candidate clauses
% 0.20/0.45 # 47 unit axiom clauses
% 0.20/0.45
% 0.20/0.45 # Requested 8, 32 cores available to the main process.
% 0.20/0.45 # There are not enough tableaux to fork, creating more from the initial 3
% 0.20/0.45 # Returning from population with 50 new_tableaux and 0 remaining starting tableaux.
% 0.20/0.45 # We now have 50 tableaux to operate on
% 8.37/1.49 # There were 5 total branch saturation attempts.
% 8.37/1.49 # There were 0 of these attempts blocked.
% 8.37/1.49 # There were 0 deferred branch saturation attempts.
% 8.37/1.49 # There were 0 free duplicated saturations.
% 8.37/1.49 # There were 5 total successful branch saturations.
% 8.37/1.49 # There were 0 successful branch saturations in interreduction.
% 8.37/1.49 # There were 0 successful branch saturations on the branch.
% 8.37/1.49 # There were 5 successful branch saturations after the branch.
% 8.37/1.49 # SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/1.49 # SZS output start for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/1.49 # Begin clausification derivation
% 8.37/1.49
% 8.37/1.49 # End clausification derivation
% 8.37/1.49 # Begin listing active clauses obtained from FOF to CNF conversion
% 8.37/1.49 cnf(i_0_555, negated_conjecture, (list_succeeds(esk137_0))).
% 8.37/1.49 cnf(i_0_464, plain, (lh(nil)='0')).
% 8.37/1.49 cnf(i_0_10, plain, (gr('0'))).
% 8.37/1.49 cnf(i_0_11, plain, (gr(nil))).
% 8.37/1.49 cnf(i_0_226, plain, (list_succeeds(nil))).
% 8.37/1.49 cnf(i_0_237, plain, (nat_list_succeeds(nil))).
% 8.37/1.49 cnf(i_0_547, plain, (occ(X1,nil)='0')).
% 8.37/1.49 cnf(i_0_428, plain, (list_succeeds(cons(X1,nil)))).
% 8.37/1.49 cnf(i_0_327, plain, (nat_succeeds('0'))).
% 8.37/1.49 cnf(i_0_479, plain, (sub(nil,X1))).
% 8.37/1.49 cnf(i_0_477, plain, (sub(X1,X1))).
% 8.37/1.49 cnf(i_0_351, plain, ('@+'('0',X1)=X1)).
% 8.37/1.49 cnf(i_0_449, plain, ('**'(nil,X1)=X1)).
% 8.37/1.49 cnf(i_0_429, plain, (list_succeeds(cons(X1,cons(X2,nil))))).
% 8.37/1.49 cnf(i_0_293, plain, ('@=<_succeeds'('0',X1))).
% 8.37/1.49 cnf(i_0_476, plain, (sub(X1,cons(X2,X1)))).
% 8.37/1.49 cnf(i_0_140, plain, (permutation_succeeds(nil,nil))).
% 8.37/1.49 cnf(i_0_430, plain, (list_succeeds(cons(X1,cons(X2,cons(X3,nil)))))).
% 8.37/1.49 cnf(i_0_175, plain, (length_succeeds(nil,'0'))).
% 8.37/1.49 cnf(i_0_215, plain, (member_succeeds(X1,cons(X1,X2)))).
% 8.37/1.49 cnf(i_0_307, plain, ('@<_succeeds'('0',s(X1)))).
% 8.37/1.49 cnf(i_0_161, plain, (delete_succeeds(X1,cons(X1,X2),X2))).
% 8.37/1.49 cnf(i_0_58, plain, (occ_succeeds(X1,nil,'0'))).
% 8.37/1.49 cnf(i_0_252, plain, (times_succeeds('0',X1,'0'))).
% 8.37/1.49 cnf(i_0_195, plain, (append_succeeds(nil,X1,X1))).
% 8.37/1.49 cnf(i_0_273, plain, (plus_succeeds('0',X1,X1))).
% 8.37/1.49 cnf(i_0_554, negated_conjecture, (esk136_0!=esk135_0)).
% 8.37/1.49 cnf(i_0_553, negated_conjecture, (occ(esk135_0,cons(esk136_0,esk137_0))!=occ(esk135_0,esk137_0))).
% 8.37/1.49 cnf(i_0_1, plain, (nil!='0')).
% 8.37/1.49 cnf(i_0_2, plain, (s(X1)!='0')).
% 8.37/1.49 cnf(i_0_4, plain, (s(X1)!=nil)).
% 8.37/1.49 cnf(i_0_3, plain, (cons(X1,X2)!='0')).
% 8.37/1.49 cnf(i_0_5, plain, (cons(X1,X2)!=nil)).
% 8.37/1.49 cnf(i_0_333, plain, (~nat_fails('0'))).
% 8.37/1.49 cnf(i_0_232, plain, (~list_fails(nil))).
% 8.37/1.49 cnf(i_0_245, plain, (~nat_list_fails(nil))).
% 8.37/1.49 cnf(i_0_301, plain, (~'@=<_fails'('0',X1))).
% 8.37/1.49 cnf(i_0_7, plain, (s(X1)!=cons(X2,X3))).
% 8.37/1.49 cnf(i_0_189, plain, (~length_fails(nil,'0'))).
% 8.37/1.49 cnf(i_0_154, plain, (~permutation_fails(nil,nil))).
% 8.37/1.49 cnf(i_0_169, plain, (~delete_fails(X1,cons(X1,X2),X2))).
% 8.37/1.49 cnf(i_0_221, plain, (~member_fails(X1,cons(X1,X2)))).
% 8.37/1.49 cnf(i_0_287, plain, (~plus_fails('0',X1,X1))).
% 8.37/1.49 cnf(i_0_209, plain, (~append_fails(nil,X1,X1))).
% 8.37/1.49 cnf(i_0_266, plain, (~times_fails('0',X1,'0'))).
% 8.37/1.49 cnf(i_0_97, plain, (~occ_fails(X1,nil,'0'))).
% 8.37/1.49 cnf(i_0_321, plain, (~'@<_fails'('0',s(X1)))).
% 8.37/1.49 cnf(i_0_35, plain, (~list_fails(X1)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_37, plain, (~nat_list_fails(X1)|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_47, plain, (~nat_fails(X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_497, plain, (list_succeeds(X1)|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_385, plain, (~nat_succeeds(X1)|~'@<_succeeds'(X1,X1))).
% 8.37/1.49 cnf(i_0_499, plain, (gr(X1)|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_431, plain, (list_succeeds(X1)|~list_succeeds(cons(X2,X1)))).
% 8.37/1.49 cnf(i_0_432, plain, (list_terminates(X1)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_533, plain, (list_succeeds(X1)|~permutation_succeeds(X2,X1))).
% 8.37/1.49 cnf(i_0_339, plain, (gr(X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_21, plain, (~not_same_occ_fails(X1,X2)|~not_same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_23, plain, (~same_occ_fails(X1,X2)|~same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_25, plain, (~permutation_fails(X1,X2)|~permutation_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_29, plain, (~length_fails(X1,X2)|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_534, plain, (list_succeeds(X1)|~permutation_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_459, plain, (list_succeeds(X1)|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_498, plain, (nat_list_terminates(X1)|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_338, plain, (nat_terminates(X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_466, plain, (nat_succeeds(lh(X1))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_33, plain, (~member_fails(X1,X2)|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_43, plain, (~'@=<_fails'(X1,X2)|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_45, plain, (~'@<_fails'(X1,X2)|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_461, plain, (gr(X1)|~length_succeeds(X2,X1))).
% 8.37/1.49 cnf(i_0_536, plain, (permutation_terminates(X1,X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_452, plain, (list_succeeds(X1)|~list_succeeds('**'(X2,X1))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_12, plain, (gr(X1)|~gr(s(X1)))).
% 8.37/1.49 cnf(i_0_234, plain, (list_terminates(X1)|~list_terminates(esk75_1(X1)))).
% 8.37/1.49 cnf(i_0_6, plain, (X1=X2|s(X1)!=s(X2))).
% 8.37/1.49 cnf(i_0_460, plain, (length_terminates(X1,X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_137, plain, (gr(X1)|~same_occ_terminates(X2,X1))).
% 8.37/1.49 cnf(i_0_138, plain, (gr(X1)|~same_occ_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_458, plain, (nat_succeeds(X1)|~length_succeeds(X2,X1))).
% 8.37/1.49 cnf(i_0_391, plain, (nat_succeeds(X1)|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_433, plain, (member_terminates(X1,X2)|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_335, plain, (nat_terminates(X1)|~nat_terminates(esk111_1(X1)))).
% 8.37/1.49 cnf(i_0_379, plain, (nat_succeeds(X1)|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_14, plain, (gr(X1)|~gr(cons(X2,X1)))).
% 8.37/1.49 cnf(i_0_15, plain, (gr(X1)|~gr(cons(X1,X2)))).
% 8.37/1.49 cnf(i_0_467, plain, (X1=nil|lh(X1)!='0'|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_17, plain, (~member2_fails(X1,X2,X3)|~member2_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_19, plain, (~occ_fails(X1,X2,X3)|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_27, plain, (~delete_fails(X1,X2,X3)|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_31, plain, (~append_fails(X1,X2,X3)|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_544, plain, (list_succeeds(X1)|~occ_succeeds(X2,X1,X3))).
% 8.37/1.49 cnf(i_0_437, plain, (list_succeeds(X1)|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_36, plain, (list_fails(X1)|list_succeeds(X1)|~list_terminates(X1))).
% 8.37/1.49 cnf(i_0_39, plain, (~times_fails(X1,X2,X3)|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_41, plain, (~plus_fails(X1,X2,X3)|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_13, plain, (gr(s(X1))|~gr(X1))).
% 8.37/1.49 cnf(i_0_397, plain, ('@=<_succeeds'(X1,X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_390, plain, ('@=<_terminates'(X1,X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_384, plain, ('@<_fails'(X1,X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_378, plain, ('@<_terminates'(X1,X2)|~nat_succeeds(X2))).
% 8.37/1.49 cnf(i_0_336, plain, (s(esk111_1(X1))=X1|nat_terminates(X1))).
% 8.37/1.49 cnf(i_0_457, plain, ('**'(X1,nil)=X1|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_540, plain, (gr(X1)|~occ_succeeds(X2,X3,X1))).
% 8.37/1.49 cnf(i_0_361, plain, (gr(X1)|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_346, plain, (gr(X1)|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_543, plain, (nat_succeeds(X1)|~occ_succeeds(X2,X3,X1))).
% 8.37/1.49 cnf(i_0_377, plain, ('@<_terminates'(X1,X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_504, plain, (list_succeeds(X1)|~list_succeeds(X2)|~delete_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_438, plain, (list_succeeds(X1)|~list_succeeds(X2)|~append_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_505, plain, (list_succeeds(X1)|~list_succeeds(X2)|~delete_succeeds(X3,X1,X2))).
% 8.37/1.49 cnf(i_0_439, plain, (list_succeeds(X1)|~list_succeeds(X2)|~append_succeeds(X3,X1,X2))).
% 8.37/1.49 cnf(i_0_38, plain, (nat_list_fails(X1)|nat_list_succeeds(X1)|~nat_list_terminates(X1))).
% 8.37/1.49 cnf(i_0_371, plain, ('@*'(X1,'0')='0'|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_359, plain, (nat_succeeds(X1)|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_342, plain, (nat_succeeds(X1)|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_366, plain, ('@*'('0',X1)='0'|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_227, plain, (list_succeeds(cons(X1,X2))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_48, plain, (nat_fails(X1)|nat_succeeds(X1)|~nat_terminates(X1))).
% 8.37/1.49 cnf(i_0_355, plain, ('@+'(X1,'0')=X1|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_135, plain, (not_same_occ_succeeds(X1,X2)|~same_occ_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_133, plain, (not_same_occ_fails(X1,X2)|~same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_139, plain, (not_same_occ_terminates(X1,X2)|~same_occ_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_114, plain, (esk14_2(X1,X2)!=esk15_2(X1,X2)|~not_same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_228, plain, (X1=nil|list_succeeds(esk71_1(X1))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_8, plain, (X1=X2|cons(X3,X1)!=cons(X4,X2))).
% 8.37/1.49 cnf(i_0_9, plain, (X1=X2|cons(X1,X3)!=cons(X2,X4))).
% 8.37/1.49 cnf(i_0_332, plain, (s(esk110_1(X1))=X1|X1='0'|nat_fails(X1))).
% 8.37/1.49 cnf(i_0_462, plain, (length_succeeds(X1,esk120_1(X1))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_435, plain, (gr(X1)|~member_succeeds(X1,X2)|~gr(X2))).
% 8.37/1.49 cnf(i_0_451, plain, (list_succeeds('**'(X1,X2))|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_132, plain, (same_occ_succeeds(X1,X2)|~not_same_occ_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_134, plain, (same_occ_fails(X1,X2)|~not_same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_396, plain, ('@=<_succeeds'(X1,X2)|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_503, plain, (delete_terminates(X1,X2,X3)|~list_succeeds(X3))).
% 8.37/1.49 cnf(i_0_526, plain, (lh(X1)=X2|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_493, plain, (X1=nil|~list_succeeds(X2)|~append_succeeds(X1,X2,X2))).
% 8.37/1.49 cnf(i_0_502, plain, (delete_terminates(X1,X2,X3)|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_516, plain, (member_succeeds(X1,X2)|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_54, plain, (member_fails(X1,X2)|~member2_fails(X1,X3,X2))).
% 8.37/1.49 cnf(i_0_53, plain, (member_fails(X1,X2)|~member2_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_57, plain, (member_terminates(X1,X2)|~member2_terminates(X1,X3,X2))).
% 8.37/1.49 cnf(i_0_443, plain, (append_terminates(X1,X2,X3)|~list_succeeds(X3))).
% 8.37/1.49 cnf(i_0_442, plain, (append_terminates(X1,X2,X3)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_454, plain, (gr(X1)|~list_succeeds(X2)|~gr('**'(X2,X1)))).
% 8.37/1.49 cnf(i_0_455, plain, (gr(X1)|~list_succeeds(X1)|~gr('**'(X1,X2)))).
% 8.37/1.49 cnf(i_0_331, plain, (X1='0'|nat_fails(X1)|~nat_fails(esk110_1(X1)))).
% 8.37/1.49 cnf(i_0_329, plain, (X1='0'|nat_succeeds(esk109_1(X1))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_406, plain, ('@=<_succeeds'(X1,s(X1))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_56, plain, (member_terminates(X1,X2)|~member2_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_362, plain, (gr(X1)|~times_succeeds(X2,X3,X1)|~gr(X3))).
% 8.37/1.49 cnf(i_0_347, plain, (gr(X1)|~plus_succeeds(X2,X3,X1)|~gr(X3))).
% 8.37/1.49 cnf(i_0_348, plain, (gr(X1)|~plus_succeeds(X2,X1,X3)|~gr(X3))).
% 8.37/1.49 cnf(i_0_386, plain, ('@<_succeeds'(X1,s(X1))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_230, plain, (X1=nil|list_fails(X1)|~list_fails(esk73_1(X1)))).
% 8.37/1.49 cnf(i_0_242, plain, (X1=nil|nat_list_fails(X1)|~nat_list_fails(esk79_1(X1)))).
% 8.37/1.49 cnf(i_0_243, plain, (X1=nil|nat_list_fails(X1)|~nat_fails(esk78_1(X1)))).
% 8.37/1.49 cnf(i_0_247, plain, (nat_list_terminates(X1)|~nat_terminates(esk80_1(X1))|~nat_list_terminates(esk81_1(X1)))).
% 8.37/1.49 cnf(i_0_239, plain, (X1=nil|nat_list_succeeds(esk77_1(X1))|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_407, plain, ('@=<_fails'(s(X1),X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_513, plain, (gr(X1)|~delete_succeeds(X2,X3,X1)|~gr(X3))).
% 8.37/1.49 cnf(i_0_445, plain, (gr(X1)|~append_succeeds(X2,X1,X3)|~gr(X3))).
% 8.37/1.49 cnf(i_0_446, plain, (gr(X1)|~append_succeeds(X1,X2,X3)|~gr(X3))).
% 8.37/1.49 cnf(i_0_514, plain, (gr(X1)|~delete_succeeds(X1,X2,X3)|~gr(X2))).
% 8.37/1.49 cnf(i_0_341, plain, (plus_terminates(X1,X2,X3)|~nat_succeeds(X3))).
% 8.37/1.49 cnf(i_0_248, plain, (nat_list_terminates(X1)|~nat_terminates(esk80_1(X1))|~nat_fails(esk80_1(X1)))).
% 8.37/1.49 cnf(i_0_527, plain, (length_succeeds(X1,lh(X1))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_340, plain, (plus_terminates(X1,X2,X3)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_360, plain, (nat_succeeds(X1)|~nat_succeeds(X2)|~times_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_343, plain, (nat_succeeds(X1)|~nat_succeeds(X2)|~plus_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_344, plain, (nat_succeeds(X1)|~nat_succeeds(X2)|~plus_succeeds(X3,X1,X2))).
% 8.37/1.49 cnf(i_0_512, plain, (nat_succeeds(X1)|~nat_list_succeeds(X2)|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_240, plain, (X1=nil|nat_succeeds(esk76_1(X1))|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_328, plain, (nat_succeeds(s(X1))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_16, plain, (gr(cons(X1,X2))|~gr(X2)|~gr(X1))).
% 8.37/1.49 cnf(i_0_537, plain, (member2_terminates(X1,X2,X3)|~list_succeeds(X3)|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_330, plain, (s(esk109_1(X1))=X1|X1='0'|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_389, plain, (X1='0'|'@<_succeeds'('0',X1)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_405, plain, (X1=X2|~'@=<_succeeds'(X2,X1)|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_118, plain, (not_same_occ_fails(X1,X2)|esk17_2(X1,X2)!=esk18_2(X1,X2))).
% 8.37/1.49 cnf(i_0_223, plain, (member_terminates(X1,X2)|~member_terminates(X1,esk69_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_528, plain, (sub(X1,X2)|~member_succeeds(esk128_2(X1,X2),X2))).
% 8.37/1.49 cnf(i_0_375, plain, ('@*'(X1,s('0'))=X1|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_492, plain, (~list_succeeds(X1)|~append_succeeds(X2,cons(X3,X1),X1))).
% 8.37/1.49 cnf(i_0_334, plain, (nat_fails(X1)|~nat_fails(s(X1)))).
% 8.37/1.49 cnf(i_0_444, plain, (gr(X1)|~append_succeeds(X2,X3,X1)|~gr(X3)|~gr(X2))).
% 8.37/1.49 cnf(i_0_539, plain, (gr(X1)|~member2_succeeds(X1,X2,X3)|~gr(X3)|~gr(X2))).
% 8.37/1.49 cnf(i_0_50, plain, (member2_succeeds(X1,X2,X3)|~member_succeeds(X1,X3))).
% 8.37/1.49 cnf(i_0_49, plain, (member2_succeeds(X1,X2,X3)|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_374, plain, ('@*'(s('0'),X1)=X1|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_382, plain, ('@<_succeeds'(X1,s(X2))|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_131, plain, (member2_terminates(X1,X2,X3)|~not_same_occ_terminates(X2,X3))).
% 8.37/1.49 cnf(i_0_337, plain, (nat_terminates(X1)|~nat_terminates(s(X1)))).
% 8.37/1.49 cnf(i_0_400, plain, ('@=<_succeeds'(X1,X2)|~nat_succeeds(X1)|~nat_succeeds(X2)|~'@=<_fails'(X2,X1))).
% 8.37/1.49 cnf(i_0_487, plain, (member_succeeds(X1,X2)|~append_succeeds(X3,cons(X1,X4),X2))).
% 8.37/1.49 cnf(i_0_121, plain, (not_same_occ_fails(X1,X2)|~member2_fails(esk16_2(X1,X2),X1,X2))).
% 8.37/1.49 cnf(i_0_511, plain, (nat_list_succeeds(X1)|~nat_list_succeeds(X2)|~delete_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_491, plain, (sub(X1,'**'(X2,X1))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_233, plain, (list_fails(X1)|~list_fails(cons(X2,X1)))).
% 8.37/1.49 cnf(i_0_235, plain, (cons(esk74_1(X1),esk75_1(X1))=X1|list_terminates(X1))).
% 8.37/1.49 cnf(i_0_490, plain, (sub(X1,'**'(X1,X2))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_345, plain, (plus_terminates(X1,X2,X3)|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_363, plain, (times_terminates(X1,X2,X3)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_463, plain, (X1=X2|~length_succeeds(X3,X2)|~length_succeeds(X3,X1))).
% 8.37/1.49 cnf(i_0_136, plain, (same_occ_terminates(X1,X2)|~not_same_occ_terminates(X1,X2)|~gr(X2)|~gr(X1))).
% 8.37/1.49 cnf(i_0_249, plain, (cons(esk80_1(X1),esk81_1(X1))=X1|nat_list_terminates(X1))).
% 8.37/1.49 cnf(i_0_236, plain, (list_terminates(X1)|~list_terminates(cons(X2,X1)))).
% 8.37/1.49 cnf(i_0_251, plain, (nat_terminates(X1)|~nat_list_terminates(cons(X1,X2)))).
% 8.37/1.49 cnf(i_0_231, plain, (cons(esk72_1(X1),esk73_1(X1))=X1|X1=nil|list_fails(X1))).
% 8.37/1.49 cnf(i_0_434, plain, (member_fails(X1,X2)|member_succeeds(X1,X2)|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_26, plain, (permutation_fails(X1,X2)|permutation_succeeds(X1,X2)|~permutation_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_30, plain, (length_fails(X1,X2)|length_succeeds(X1,X2)|~length_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_34, plain, (member_fails(X1,X2)|member_succeeds(X1,X2)|~member_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_44, plain, ('@=<_fails'(X1,X2)|'@=<_succeeds'(X1,X2)|~'@=<_terminates'(X1,X2))).
% 8.37/1.49 cnf(i_0_192, plain, (s(esk52_2(X1,X2))=X2|length_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_244, plain, (cons(esk78_1(X1),esk79_1(X1))=X1|X1=nil|nat_list_fails(X1))).
% 8.37/1.49 cnf(i_0_305, plain, (s(esk99_2(X1,X2))=X1|'@=<_terminates'(X1,X2))).
% 8.37/1.49 cnf(i_0_46, plain, ('@<_fails'(X1,X2)|'@<_succeeds'(X1,X2)|~'@<_terminates'(X1,X2))).
% 8.37/1.49 cnf(i_0_353, plain, (nat_succeeds('@+'(X1,X2))|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_368, plain, (nat_succeeds('@*'(X1,X2))|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_541, plain, (not_same_occ_terminates(X1,X2)|~list_succeeds(X2)|~list_succeeds(X1)|~gr(X2)|~gr(X1))).
% 8.37/1.49 cnf(i_0_542, plain, (same_occ_terminates(X1,X2)|~list_succeeds(X2)|~list_succeeds(X1)|~gr(X2)|~gr(X1))).
% 8.37/1.49 cnf(i_0_229, plain, (cons(esk70_1(X1),esk71_1(X1))=X1|X1=nil|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_304, plain, (s(esk100_2(X1,X2))=X2|'@=<_terminates'(X1,X2))).
% 8.37/1.49 cnf(i_0_358, plain, (X1=X2|'@+'(X3,X1)!='@+'(X3,X2)|~nat_succeeds(X3))).
% 8.37/1.49 cnf(i_0_112, plain, (gr(X1)|~occ_terminates(X1,cons(X2,X3),X4))).
% 8.37/1.49 cnf(i_0_520, plain, ('@+'(X1,X2)=X3|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_325, plain, (s(esk107_2(X1,X2))=X1|'@<_terminates'(X1,X2))).
% 8.37/1.49 cnf(i_0_510, plain, (list_succeeds(esk125_3(X1,X2,X3))|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_414, plain, ('@=<_succeeds'(X1,'@+'(X1,X2))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_380, plain, (s(esk114_2(X1,X2))=X2|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_436, plain, (X1=X2|member_succeeds(X1,X3)|~member_succeeds(X1,cons(X2,X3)))).
% 8.37/1.49 cnf(i_0_241, plain, (cons(esk76_1(X1),esk77_1(X1))=X1|X1=nil|~nat_list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_324, plain, (s(esk108_2(X1,X2))=X2|'@<_terminates'(X1,X2))).
% 8.37/1.49 cnf(i_0_191, plain, (length_terminates(X1,X2)|~length_terminates(esk51_2(X1,X2),esk52_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_303, plain, ('@=<_terminates'(X1,X2)|~'@=<_terminates'(esk99_2(X1,X2),esk100_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_323, plain, ('@<_terminates'(X1,X2)|~'@<_terminates'(esk107_2(X1,X2),esk108_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_401, plain, (X1=X2|'@<_succeeds'(X1,X2)|~nat_succeeds(X2)|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_529, plain, (sub(X1,X2)|member_succeeds(esk128_2(X1,X2),X1))).
% 8.37/1.49 cnf(i_0_531, plain, (occ(X1,X2)=X3|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_453, plain, (gr('**'(X1,X2))|~list_succeeds(X1)|~gr(X2)|~gr(X1))).
% 8.37/1.49 cnf(i_0_538, plain, (occ_terminates(X1,X2,X3)|~list_succeeds(X2)|~gr(X1)|~gr(X2))).
% 8.37/1.49 cnf(i_0_22, plain, (not_same_occ_fails(X1,X2)|not_same_occ_succeeds(X1,X2)|~not_same_occ_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_545, plain, (occ_succeeds(X1,X2,esk129_2(X1,X2))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_52, plain, (member2_fails(X1,X2,X3)|~member_fails(X1,X2)|~member_fails(X1,X3))).
% 8.37/1.49 cnf(i_0_55, plain, (member2_terminates(X1,X2,X3)|~member_terminates(X1,X2)|~member_terminates(X1,X3))).
% 8.37/1.49 cnf(i_0_51, plain, (member_succeeds(X1,X2)|member_succeeds(X1,X3)|~member2_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_24, plain, (same_occ_fails(X1,X2)|same_occ_succeeds(X1,X2)|~same_occ_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_447, plain, (append_succeeds(X1,X2,esk119_2(X1,X2))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_506, plain, (lh(X1)=s(lh(X2))|~list_succeeds(X1)|~delete_succeeds(X3,X1,X2))).
% 8.37/1.49 cnf(i_0_465, plain, (lh(cons(X1,X2))=s(lh(X2))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_481, plain, (sub(cons(X1,X2),cons(X1,X3))|~sub(X2,X3))).
% 8.37/1.49 cnf(i_0_532, plain, (occ_succeeds(X1,X2,occ(X1,X2))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_409, plain, ('@<_succeeds'(X1,'@+'(X1,s(X2)))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_530, plain, (member_succeeds(X1,X2)|~sub(X3,X2)|~member_succeeds(X1,X3))).
% 8.37/1.49 cnf(i_0_404, plain, ('@=<_succeeds'(X1,X2)|~'@=<_succeeds'(X3,X2)|~'@=<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_403, plain, ('@<_succeeds'(X1,X2)|~'@<_succeeds'(X1,X3)|~'@=<_succeeds'(X3,X2))).
% 8.37/1.49 cnf(i_0_402, plain, ('@<_succeeds'(X1,X2)|~'@<_succeeds'(X3,X2)|~'@=<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_393, plain, ('@+'(X1,esk116_2(X1,X2))=X2|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_472, plain, ('@=<_succeeds'(lh(X1),lh(cons(X2,X1)))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_111, plain, (gr(X1)|~occ_terminates(X2,cons(X1,X3),X4))).
% 8.37/1.49 cnf(i_0_521, plain, (plus_succeeds(X1,X2,'@+'(X1,X2))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_349, plain, (plus_succeeds(X1,X2,esk112_2(X1,X2))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_383, plain, ('@<_succeeds'(X1,X2)|~'@<_succeeds'(X3,X2)|~'@<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_478, plain, (sub(X1,X2)|~sub(X3,X2)|~sub(X1,X3))).
% 8.37/1.49 cnf(i_0_119, plain, (not_same_occ_fails(X1,X2)|~occ_fails(esk16_2(X1,X2),X2,esk18_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_120, plain, (not_same_occ_fails(X1,X2)|~occ_fails(esk16_2(X1,X2),X1,esk17_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_299, plain, (s(esk98_2(X1,X2))=X2|X1='0'|'@=<_fails'(X1,X2))).
% 8.37/1.49 cnf(i_0_238, plain, (nat_list_succeeds(cons(X1,X2))|~nat_succeeds(X1)|~nat_list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_495, plain, (X1=X2|'**'(X1,X3)!='**'(X2,X3)|~list_succeeds(X3)|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_480, plain, (sub(cons(X1,X2),X3)|~sub(X2,X3)|~member_succeeds(X1,X3))).
% 8.37/1.49 cnf(i_0_246, plain, (nat_fails(X1)|nat_list_fails(X2)|~nat_list_fails(cons(X1,X2)))).
% 8.37/1.49 cnf(i_0_546, plain, (X1=X2|~occ_succeeds(X3,X4,X2)|~occ_succeeds(X3,X4,X1))).
% 8.37/1.49 cnf(i_0_448, plain, (X1=X2|~append_succeeds(X3,X4,X2)|~append_succeeds(X3,X4,X1))).
% 8.37/1.49 cnf(i_0_365, plain, (X1=X2|~times_succeeds(X3,X4,X2)|~times_succeeds(X3,X4,X1))).
% 8.37/1.49 cnf(i_0_350, plain, (X1=X2|~plus_succeeds(X3,X4,X2)|~plus_succeeds(X3,X4,X1))).
% 8.37/1.49 cnf(i_0_318, plain, (s(esk105_2(X1,X2))=X2|X1='0'|'@<_fails'(X1,X2))).
% 8.37/1.49 cnf(i_0_415, plain, ('@=<_succeeds'(X1,'@+'(X2,X1))|~nat_succeeds(X1)|~nat_succeeds(X2))).
% 8.37/1.49 cnf(i_0_399, plain, ('@<_succeeds'(X1,X2)|'@=<_succeeds'(X2,X1)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_486, plain, (member_succeeds(X1,'**'(X2,X3))|~list_succeeds(X2)|~member_succeeds(X1,X3))).
% 8.37/1.49 cnf(i_0_485, plain, (member_succeeds(X1,'**'(X2,X3))|~list_succeeds(X2)|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_250, plain, (nat_fails(X1)|nat_list_terminates(X2)|~nat_list_terminates(cons(X1,X2)))).
% 8.37/1.49 cnf(i_0_496, plain, (X1=X2|~append_succeeds(X3,X2,X4)|~append_succeeds(X3,X1,X4))).
% 8.37/1.49 cnf(i_0_522, plain, ('@*'(X1,X2)=X3|~nat_succeeds(X2)|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_418, plain, ('@=<_succeeds'(X1,X2)|~nat_succeeds(X3)|~'@=<_succeeds'('@+'(X3,X1),'@+'(X3,X2)))).
% 8.37/1.49 cnf(i_0_416, plain, ('@<_succeeds'(X1,X2)|~nat_succeeds(X3)|~'@<_succeeds'('@+'(X3,X1),'@+'(X3,X2)))).
% 8.37/1.49 cnf(i_0_185, plain, (s(esk49_2(X1,X2))=X2|X2='0'|length_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_387, plain, (X1=X2|'@<_succeeds'(X2,X1)|~nat_succeeds(X1)|~'@<_succeeds'(X2,s(X1)))).
% 8.37/1.49 cnf(i_0_216, plain, (member_succeeds(X1,cons(X2,X3))|~member_succeeds(X1,X3))).
% 8.37/1.49 cnf(i_0_222, plain, (member_fails(X1,X2)|~member_fails(X1,cons(X3,X2)))).
% 8.37/1.49 cnf(i_0_300, plain, (s(esk97_2(X1,X2))=X1|X1='0'|'@=<_fails'(X1,X2))).
% 8.37/1.49 cnf(i_0_484, plain, (member_succeeds(X1,X2)|~member_succeeds(X1,X3)|~append_succeeds(X4,X3,X2))).
% 8.37/1.49 cnf(i_0_483, plain, (member_succeeds(X1,X2)|~member_succeeds(X1,X3)|~append_succeeds(X3,X4,X2))).
% 8.37/1.49 cnf(i_0_517, plain, (member_succeeds(X1,X2)|~member_succeeds(X1,X3)|~delete_succeeds(X4,X2,X3))).
% 8.37/1.49 cnf(i_0_381, plain, ('@<_succeeds'(X1,X2)|~'@<_succeeds'(X3,s(X2))|~'@<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_320, plain, (s(esk104_2(X1,X2))=X1|X1='0'|'@<_fails'(X1,X2))).
% 8.37/1.49 cnf(i_0_225, plain, (member_terminates(X1,X2)|~member_terminates(X1,cons(X3,X2)))).
% 8.37/1.49 cnf(i_0_549, plain, (occ(X1,cons(X2,X3))=occ(X1,X3)|X1=X2|esk134_0!=esk133_0|~list_succeeds(X3))).
% 8.37/1.49 cnf(i_0_524, plain, ('**'(X1,X2)=X3|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_357, plain, ('@+'(X1,X2)='@+'(X2,X1)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_186, plain, (s(esk49_2(X1,X2))=X2|X1=nil|length_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_525, plain, (append_succeeds(X1,X2,'**'(X1,X2))|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_494, plain, (X1=X2|~list_succeeds(X3)|~append_succeeds(X2,X4,X3)|~append_succeeds(X1,X4,X3))).
% 8.37/1.49 cnf(i_0_296, plain, (s(esk96_2(X1,X2))=X2|X1='0'|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_450, plain, ('**'(cons(X1,X2),X3)=cons(X1,'**'(X2,X3))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_312, plain, (s(esk102_2(X1,X2))=X2|X1='0'|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_179, plain, (s(esk46_2(X1,X2))=X2|X2='0'|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_297, plain, (s(esk95_2(X1,X2))=X1|X1='0'|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_523, plain, (times_succeeds(X1,X2,'@*'(X1,X2))|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_314, plain, (s(esk101_2(X1,X2))=X1|X1='0'|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_518, plain, (delete_succeeds(X1,X2,esk127_2(X1,X2))|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_392, plain, (plus_succeeds(X1,esk115_2(X1,X2),X2)|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_117, plain, (member2_succeeds(esk13_2(X1,X2),X1,X2)|~not_same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_126, plain, (not_same_occ_terminates(X1,X2)|~member2_terminates(esk19_2(X1,X2),X1,X2)|~member2_fails(esk20_2(X1,X2),X1,X2))).
% 8.37/1.49 cnf(i_0_180, plain, (s(esk46_2(X1,X2))=X2|X1=nil|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_352, plain, ('@+'(s(X1),X2)=s('@+'(X1,X2))|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_373, plain, ('@*'(X1,X2)='@*'(X2,X1)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_364, plain, (times_succeeds(X1,X2,esk113_2(X1,X2))|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_398, plain, ('@=<_succeeds'(X1,X2)|'@=<_succeeds'(X2,X1)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_388, plain, (X1=X2|'@<_succeeds'(X1,X2)|'@<_succeeds'(X2,X1)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_270, plain, (s(esk86_3(X1,X2,X3))=X1|times_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_427, plain, (X1=X2|'@+'(X1,X3)!='@+'(X2,X3)|~nat_succeeds(X3)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_20, plain, (occ_fails(X1,X2,X3)|occ_succeeds(X1,X2,X3)|~occ_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_28, plain, (delete_fails(X1,X2,X3)|delete_succeeds(X1,X2,X3)|~delete_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_32, plain, (append_fails(X1,X2,X3)|append_succeeds(X1,X2,X3)|~append_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_291, plain, (s(esk93_3(X1,X2,X3))=X1|plus_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_489, plain, (member_succeeds(X1,X2)|member_succeeds(X1,X3)|~list_succeeds(X2)|~member_succeeds(X1,'**'(X2,X3)))).
% 8.37/1.49 cnf(i_0_395, plain, ('@+'(X1,s(esk118_2(X1,X2)))=X2|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_183, plain, (X1='0'|length_fails(X2,X1)|~length_fails(esk48_2(X2,X1),esk49_2(X2,X1)))).
% 8.37/1.49 cnf(i_0_298, plain, (X1='0'|'@=<_fails'(X1,X2)|~'@=<_fails'(esk97_2(X1,X2),esk98_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_294, plain, ('@=<_succeeds'(s(X1),s(X2))|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_40, plain, (times_fails(X1,X2,X3)|times_succeeds(X1,X2,X3)|~times_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_42, plain, (plus_fails(X1,X2,X3)|plus_succeeds(X1,X2,X3)|~plus_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_316, plain, (X1='0'|'@<_fails'(X1,X2)|~'@<_fails'(esk104_2(X1,X2),esk105_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_148, plain, (X1=nil|permutation_fails(X2,X1)|~permutation_fails(esk30_2(X2,X1),esk29_2(X2,X1)))).
% 8.37/1.49 cnf(i_0_290, plain, (s(esk94_3(X1,X2,X3))=X3|plus_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_149, plain, (X1=nil|permutation_fails(X1,X2)|~permutation_fails(esk30_2(X1,X2),esk29_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_184, plain, (X1=nil|length_fails(X1,X2)|~length_fails(esk48_2(X1,X2),esk49_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_471, plain, ('@=<_succeeds'(lh(X1),lh('**'(X2,X1)))|~list_succeeds(X1)|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_470, plain, ('@=<_succeeds'(lh(X1),lh('**'(X1,X2)))|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_302, plain, ('@=<_fails'(X1,X2)|~'@=<_fails'(s(X1),s(X2)))).
% 8.37/1.49 cnf(i_0_171, plain, (delete_terminates(X1,X2,X3)|~delete_terminates(X1,esk42_3(X1,X2,X3),esk43_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_211, plain, (append_terminates(X1,X2,X3)|~append_terminates(esk60_3(X1,X2,X3),X2,esk61_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_289, plain, (plus_terminates(X1,X2,X3)|~plus_terminates(esk93_3(X1,X2,X3),X2,esk94_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_160, plain, (delete_terminates(X1,X2,X3)|~permutation_terminates(X2,cons(X1,X4)))).
% 8.37/1.49 cnf(i_0_411, plain, ('@<_succeeds'(X1,'@+'(X2,X1))|~nat_succeeds(X1)|~nat_succeeds(X2)|~'@<_succeeds'('0',X2))).
% 8.37/1.49 cnf(i_0_475, plain, ('@=<_succeeds'(lh(X1),lh(X2))|~list_succeeds(X2)|~append_succeeds(X3,X1,X2))).
% 8.37/1.49 cnf(i_0_474, plain, ('@=<_succeeds'(lh(X1),lh(X2))|~list_succeeds(X2)|~append_succeeds(X1,X3,X2))).
% 8.37/1.49 cnf(i_0_551, plain, (occ(X1,cons(X2,X3))=occ(X1,X3)|esk130_0=nil|X1=X2|list_succeeds(esk132_0)|~list_succeeds(X3))).
% 8.37/1.49 cnf(i_0_306, plain, ('@=<_terminates'(X1,X2)|~'@=<_terminates'(s(X1),s(X2)))).
% 8.37/1.49 cnf(i_0_272, plain, (times_terminates(X1,X2,X3)|~times_terminates(s(X1),X2,X4))).
% 8.37/1.49 cnf(i_0_18, plain, (member2_fails(X1,X2,X3)|member2_succeeds(X1,X2,X3)|~member2_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_417, plain, ('@<_succeeds'(X1,X2)|~nat_succeeds(X3)|~nat_succeeds(X2)|~nat_succeeds(X1)|~'@<_succeeds'('@+'(X1,X3),'@+'(X2,X3)))).
% 8.37/1.49 cnf(i_0_158, plain, (cons(esk31_2(X1,X2),esk32_2(X1,X2))=X2|permutation_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_394, plain, (plus_succeeds(X1,s(esk117_2(X1,X2)),X2)|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_356, plain, ('@+'(s(X1),X2)='@+'(X1,s(X2))|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_219, plain, (cons(X1,esk67_2(X1,X2))=X2|member_fails(X1,X2)|~member_fails(X1,esk66_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_469, plain, ('@+'(lh(X1),lh(X2))=lh('**'(X1,X2))|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_308, plain, ('@<_succeeds'(s(X1),s(X2))|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_260, plain, (X1='0'|times_fails(X2,X3,X1)|~plus_fails(X3,esk85_3(X2,X3,X1),X1))).
% 8.37/1.49 cnf(i_0_261, plain, (X1='0'|times_fails(X1,X2,X3)|~plus_fails(X2,esk85_3(X1,X2,X3),X3))).
% 8.37/1.49 cnf(i_0_150, plain, (X1=nil|permutation_fails(X2,X1)|~delete_fails(esk28_2(X2,X1),X2,esk30_2(X2,X1)))).
% 8.37/1.49 cnf(i_0_151, plain, (X1=nil|permutation_fails(X1,X2)|~delete_fails(esk28_2(X1,X2),X1,esk30_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_193, plain, (cons(esk50_2(X1,X2),esk51_2(X1,X2))=X1|length_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_258, plain, (s(esk82_3(X1,X2,X3))=X1|X3='0'|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_278, plain, (s(esk90_3(X1,X2,X3))=X3|X1='0'|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_259, plain, (s(esk82_3(X1,X2,X3))=X1|X1='0'|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_280, plain, (s(esk89_3(X1,X2,X3))=X1|X1='0'|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_322, plain, ('@<_fails'(X1,X2)|~'@<_fails'(s(X1),s(X2)))).
% 8.37/1.49 cnf(i_0_326, plain, ('@<_terminates'(X1,X2)|~'@<_terminates'(s(X1),s(X2)))).
% 8.37/1.49 cnf(i_0_176, plain, (length_succeeds(cons(X1,X2),s(X3))|~length_succeeds(X2,X3))).
% 8.37/1.49 cnf(i_0_224, plain, (cons(esk68_2(X1,X2),esk69_2(X1,X2))=X2|member_terminates(X1,X2))).
% 8.37/1.49 cnf(i_0_279, plain, (s(esk89_3(X1,X2,X3))=X1|X3=X2|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_277, plain, (s(esk90_3(X1,X2,X3))=X3|X3=X2|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_468, plain, (cons(esk121_2(X1,X2),esk122_2(X1,X2))=X2|lh(X2)!=s(X1)|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_313, plain, (s(esk103_2(X1,X2))=X2|s(esk101_2(X1,X2))=X1|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_190, plain, (length_fails(X1,X2)|~length_fails(cons(X3,X1),s(X2)))).
% 8.37/1.49 cnf(i_0_194, plain, (length_terminates(X1,X2)|~length_terminates(cons(X3,X1),s(X2)))).
% 8.37/1.49 cnf(i_0_141, plain, (permutation_succeeds(X1,cons(X2,X3))|~delete_succeeds(X2,X1,X4)|~permutation_succeeds(X4,X3))).
% 8.37/1.49 cnf(i_0_264, plain, (s(esk84_3(X1,X2,X3))=X1|X3='0'|times_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_311, plain, (s(esk103_2(X1,X2))=X2|s(esk102_2(X1,X2))=X2|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_412, plain, ('@=<_succeeds'('@+'(X1,X2),'@+'(X1,X3))|~nat_succeeds(X1)|~'@=<_succeeds'(X2,X3))).
% 8.37/1.49 cnf(i_0_408, plain, ('@<_succeeds'('@+'(X1,X2),'@+'(X1,X3))|~nat_succeeds(X1)|~'@<_succeeds'(X2,X3))).
% 8.37/1.49 cnf(i_0_456, plain, ('**'('**'(X1,X2),X3)='**'(X1,'**'(X2,X3))|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_367, plain, ('@+'(X1,'@*'(X2,X1))='@*'(s(X2),X1)|~nat_succeeds(X1)|~nat_succeeds(X2))).
% 8.37/1.49 cnf(i_0_284, plain, (s(esk92_3(X1,X2,X3))=X3|X1='0'|plus_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_130, plain, (occ_terminates(X1,X2,X3)|member2_fails(X1,X2,X4)|~not_same_occ_terminates(X2,X4))).
% 8.37/1.49 cnf(i_0_515, plain, (X1=X2|member_succeeds(X2,X3)|~member_succeeds(X2,X4)|~delete_succeeds(X1,X4,X3))).
% 8.37/1.49 cnf(i_0_157, plain, (permutation_terminates(X1,X2)|~delete_terminates(esk31_2(X1,X2),X1,esk33_2(X1,X2))|~delete_fails(esk31_2(X1,X2),X1,esk34_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_265, plain, (s(esk84_3(X1,X2,X3))=X1|X1='0'|times_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_552, plain, (occ(X1,cons(X2,X3))=occ(X1,X3)|cons(esk131_0,esk132_0)=esk130_0|esk130_0=nil|X1=X2|~list_succeeds(X3))).
% 8.37/1.49 cnf(i_0_115, plain, (occ_succeeds(esk13_2(X1,X2),X2,esk15_2(X1,X2))|~not_same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_116, plain, (occ_succeeds(esk13_2(X1,X2),X1,esk14_2(X1,X2))|~not_same_occ_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_181, plain, (cons(esk44_2(X1,X2),esk45_2(X1,X2))=X1|X2='0'|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_372, plain, ('@+'('@*'(X1,X2),X1)='@*'(X1,s(X2))|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_286, plain, (s(esk91_3(X1,X2,X3))=X1|X1='0'|plus_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_426, plain, ('@=<_succeeds'(X1,X2)|~nat_succeeds(X2)|~nat_succeeds(X1)|~nat_succeeds(X3)|~'@=<_succeeds'('@*'(s(X3),X1),'@*'(s(X3),X2)))).
% 8.37/1.49 cnf(i_0_203, plain, (X1=X2|append_fails(X3,X2,X1)|~append_fails(esk57_3(X3,X2,X1),X2,esk58_3(X3,X2,X1)))).
% 8.37/1.49 cnf(i_0_281, plain, (X1=X2|plus_fails(X3,X2,X1)|~plus_fails(esk91_3(X3,X2,X1),X2,esk92_3(X3,X2,X1)))).
% 8.37/1.49 cnf(i_0_315, plain, (s(esk106_2(X1,X2))=X2|'@<_fails'(X1,X2)|~'@<_fails'(esk104_2(X1,X2),esk105_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_285, plain, (s(esk91_3(X1,X2,X3))=X1|X3=X2|plus_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_147, plain, (cons(esk25_2(X1,X2),esk26_2(X1,X2))=X2|X1=nil|~permutation_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_146, plain, (cons(esk25_2(X1,X2),esk26_2(X1,X2))=X2|X2=nil|~permutation_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_182, plain, (cons(esk44_2(X1,X2),esk45_2(X1,X2))=X1|X1=nil|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_548, plain, (occ(X1,cons(X2,X3))=occ(X1,X3)|X1=X2|occ(esk133_0,cons(esk134_0,esk130_0))!=occ(esk133_0,esk130_0)|~list_succeeds(X3))).
% 8.37/1.49 cnf(i_0_319, plain, (s(esk106_2(X1,X2))=X2|s(esk104_2(X1,X2))=X1|'@<_fails'(X1,X2))).
% 8.37/1.49 cnf(i_0_283, plain, (s(esk92_3(X1,X2,X3))=X3|X3=X2|plus_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_262, plain, (X1='0'|times_fails(X2,X3,X1)|~times_fails(esk84_3(X2,X3,X1),X3,esk85_3(X2,X3,X1)))).
% 8.37/1.49 cnf(i_0_263, plain, (X1='0'|times_fails(X1,X2,X3)|~times_fails(esk84_3(X1,X2,X3),X2,esk85_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_282, plain, (X1='0'|plus_fails(X1,X2,X3)|~plus_fails(esk91_3(X1,X2,X3),X2,esk92_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_204, plain, (X1=nil|append_fails(X1,X2,X3)|~append_fails(esk57_3(X1,X2,X3),X2,esk58_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_317, plain, (s(esk106_2(X1,X2))=X2|s(esk105_2(X1,X2))=X2|'@<_fails'(X1,X2))).
% 8.37/1.49 cnf(i_0_217, plain, (cons(X1,esk64_2(X1,X2))=X2|member_succeeds(X1,esk63_2(X1,X2))|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_507, plain, (delete_succeeds(X1,'**'(X2,cons(X1,X3)),'**'(X2,X3))|~list_succeeds(X2))).
% 8.37/1.49 cnf(i_0_177, plain, (X1='0'|length_succeeds(esk45_2(X2,X1),esk46_2(X2,X1))|~length_succeeds(X2,X1))).
% 8.37/1.49 cnf(i_0_295, plain, (X1='0'|'@=<_succeeds'(esk95_2(X1,X2),esk96_2(X1,X2))|~'@=<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_187, plain, (cons(esk47_2(X1,X2),esk48_2(X1,X2))=X1|X2='0'|length_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_153, plain, (cons(esk28_2(X1,X2),esk29_2(X1,X2))=X2|X1=nil|permutation_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_488, plain, (member_succeeds(X1,X2)|member_succeeds(X1,X3)|~member_succeeds(X1,X4)|~append_succeeds(X2,X3,X4))).
% 8.37/1.49 cnf(i_0_274, plain, (plus_succeeds(s(X1),X2,s(X3))|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_288, plain, (plus_fails(X1,X2,X3)|~plus_fails(s(X1),X2,s(X3)))).
% 8.37/1.49 cnf(i_0_310, plain, (X1='0'|'@<_succeeds'(esk101_2(X1,X2),esk102_2(X1,X2))|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_142, plain, (X1=nil|permutation_succeeds(esk27_2(X2,X1),esk26_2(X2,X1))|~permutation_succeeds(X2,X1))).
% 8.37/1.49 cnf(i_0_143, plain, (X1=nil|permutation_succeeds(esk27_2(X1,X2),esk26_2(X1,X2))|~permutation_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_178, plain, (X1=nil|length_succeeds(esk45_2(X1,X2),esk46_2(X1,X2))|~length_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_152, plain, (cons(esk28_2(X1,X2),esk29_2(X1,X2))=X2|X2=nil|permutation_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_188, plain, (cons(esk47_2(X1,X2),esk48_2(X1,X2))=X1|X1=nil|length_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_292, plain, (plus_terminates(X1,X2,X3)|~plus_terminates(s(X1),X2,s(X3)))).
% 8.37/1.49 cnf(i_0_253, plain, (times_succeeds(s(X1),X2,X3)|~plus_succeeds(X2,X4,X3)|~times_succeeds(X1,X2,X4))).
% 8.37/1.49 cnf(i_0_254, plain, (X1='0'|plus_succeeds(X2,esk83_3(X3,X2,X1),X1)|~times_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_255, plain, (X1='0'|plus_succeeds(X2,esk83_3(X1,X2,X3),X3)|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_473, plain, ('@+'(lh(X1),lh(X2))=lh(X3)|~list_succeeds(X3)|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_413, plain, ('@=<_succeeds'('@+'(X1,X2),'@+'(X3,X2))|~nat_succeeds(X2)|~nat_succeeds(X3)|~'@=<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_424, plain, ('@=<_succeeds'('@*'(X1,X2),'@*'(X3,X2))|~nat_succeeds(X2)|~nat_succeeds(X3)|~'@=<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_354, plain, ('@+'('@+'(X1,X2),X3)='@+'(X1,'@+'(X2,X3))|~nat_succeeds(X3)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_144, plain, (X1=nil|delete_succeeds(esk25_2(X2,X1),X2,esk27_2(X2,X1))|~permutation_succeeds(X2,X1))).
% 8.37/1.49 cnf(i_0_423, plain, ('@=<_succeeds'('@*'(X1,X2),'@*'(X1,X3))|~nat_succeeds(X3)|~nat_succeeds(X1)|~'@=<_succeeds'(X2,X3))).
% 8.37/1.49 cnf(i_0_410, plain, ('@<_succeeds'('@+'(X1,X2),'@+'(X3,X2))|~nat_succeeds(X2)|~nat_succeeds(X3)|~'@<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_156, plain, (permutation_terminates(X1,X2)|~delete_terminates(esk31_2(X1,X2),X1,esk33_2(X1,X2))|~permutation_terminates(esk34_2(X1,X2),esk32_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_268, plain, (times_terminates(X1,X2,X3)|~plus_terminates(X2,esk88_3(X1,X2,X3),X3)|~times_terminates(esk86_3(X1,X2,X3),X2,esk87_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_145, plain, (X1=nil|delete_succeeds(esk25_2(X1,X2),X1,esk27_2(X1,X2))|~permutation_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_482, plain, (append_succeeds(esk123_2(X1,X2),cons(X1,esk124_2(X1,X2)),X2)|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_419, plain, ('@=<_succeeds'('@+'(X1,X2),'@+'(X3,X4))|~nat_succeeds(X3)|~'@=<_succeeds'(X2,X4)|~'@=<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_420, plain, ('@<_succeeds'('@+'(X1,X2),'@+'(X3,X4))|~nat_succeeds(X3)|~'@<_succeeds'(X1,X3)|~'@=<_succeeds'(X2,X4))).
% 8.37/1.49 cnf(i_0_421, plain, ('@<_succeeds'('@+'(X1,X2),'@+'(X3,X4))|~nat_succeeds(X3)|~'@<_succeeds'(X2,X4)|~'@=<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_370, plain, ('@*'('@*'(X1,X2),X3)='@*'(X1,'@*'(X2,X3))|~nat_succeeds(X3)|~nat_succeeds(X2)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_172, plain, (cons(esk41_3(X1,X2,X3),esk43_3(X1,X2,X3))=X3|delete_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_59, plain, (occ_succeeds(X1,cons(X1,X2),s(X3))|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_98, plain, (occ_fails(X1,X2,X3)|~occ_fails(X1,cons(X1,X2),s(X3)))).
% 8.37/1.49 cnf(i_0_173, plain, (cons(esk41_3(X1,X2,X3),esk42_3(X1,X2,X3))=X2|delete_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_422, plain, ('@<_succeeds'('@+'(X1,X2),'@+'(X3,X4))|~nat_succeeds(X3)|~'@<_succeeds'(X2,X4)|~'@<_succeeds'(X1,X3))).
% 8.37/1.49 cnf(i_0_60, plain, (X1=X2|occ_succeeds(X2,cons(X1,X3),X4)|~occ_succeeds(X2,X3,X4))).
% 8.37/1.49 cnf(i_0_99, plain, (X1=X2|occ_fails(X2,X3,X4)|~occ_fails(X2,cons(X1,X3),X4))).
% 8.37/1.49 cnf(i_0_212, plain, (cons(esk59_3(X1,X2,X3),esk61_3(X1,X2,X3))=X3|append_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_109, plain, (occ_terminates(X1,X2,X3)|~occ_terminates(X1,cons(X1,X2),s(X3)))).
% 8.37/1.49 cnf(i_0_113, plain, (X1=X2|not_same_occ_succeeds(X3,X4)|~occ_succeeds(X5,X4,X2)|~occ_succeeds(X5,X3,X1)|~member2_succeeds(X5,X3,X4))).
% 8.37/1.49 cnf(i_0_162, plain, (delete_succeeds(X1,cons(X2,X3),cons(X2,X4))|~delete_succeeds(X1,X3,X4))).
% 8.37/1.49 cnf(i_0_110, plain, (X1=X2|occ_terminates(X1,X3,X4)|~occ_terminates(X1,cons(X2,X3),X4))).
% 8.37/1.49 cnf(i_0_69, plain, (s(esk4_3(X1,X2,X3))=X3|X3='0'|esk1_3(X1,X2,X3)!=X1|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_70, plain, (s(esk4_3(X1,X2,X3))=X3|X2=nil|esk1_3(X1,X2,X3)!=X1|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_425, plain, (X1='0'|'@<_succeeds'('@*'(X1,X2),'@*'(X1,X3))|~nat_succeeds(X3)|~nat_succeeds(X1)|~'@<_succeeds'(X2,X3))).
% 8.37/1.49 cnf(i_0_213, plain, (cons(esk59_3(X1,X2,X3),esk60_3(X1,X2,X3))=X1|append_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_170, plain, (delete_fails(X1,X2,X3)|~delete_fails(X1,cons(X4,X2),cons(X4,X3)))).
% 8.37/1.49 cnf(i_0_174, plain, (delete_terminates(X1,X2,X3)|~delete_terminates(X1,cons(X4,X2),cons(X4,X3)))).
% 8.37/1.49 cnf(i_0_508, plain, ('**'(esk125_3(X1,X2,X3),esk126_3(X1,X2,X3))=X3|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_196, plain, (append_succeeds(cons(X1,X2),X3,cons(X1,X4))|~append_succeeds(X2,X3,X4))).
% 8.37/1.49 cnf(i_0_210, plain, (append_fails(X1,X2,X3)|~append_fails(cons(X4,X1),X2,cons(X4,X3)))).
% 8.37/1.49 cnf(i_0_155, plain, (delete_fails(X1,X2,X3)|permutation_fails(X3,X4)|~permutation_fails(X2,cons(X1,X4)))).
% 8.37/1.49 cnf(i_0_214, plain, (append_terminates(X1,X2,X3)|~append_terminates(cons(X4,X1),X2,cons(X4,X3)))).
% 8.37/1.49 cnf(i_0_166, plain, (X1=cons(X2,X3)|delete_fails(X2,X1,X3)|~delete_fails(X2,esk39_3(X2,X1,X3),esk40_3(X2,X1,X3)))).
% 8.37/1.49 cnf(i_0_159, plain, (delete_fails(X1,X2,X3)|permutation_terminates(X3,X4)|~permutation_terminates(X2,cons(X1,X4)))).
% 8.37/1.49 cnf(i_0_71, plain, (cons(X1,esk3_3(X1,X2,X3))=X2|X3='0'|esk1_3(X1,X2,X3)!=X1|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_72, plain, (cons(X1,esk3_3(X1,X2,X3))=X2|X2=nil|esk1_3(X1,X2,X3)!=X1|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_218, plain, (cons(esk62_2(X1,X2),esk63_2(X1,X2))=X2|cons(X1,esk64_2(X1,X2))=X2|~member_succeeds(X1,X2))).
% 8.37/1.49 cnf(i_0_309, plain, (s(esk103_2(X1,X2))=X2|'@<_succeeds'(esk101_2(X1,X2),esk102_2(X1,X2))|~'@<_succeeds'(X1,X2))).
% 8.37/1.49 cnf(i_0_550, plain, (occ(X1,cons(X2,esk132_0))=occ(X1,esk132_0)|occ(X3,cons(X4,X5))=occ(X3,X5)|esk130_0=nil|X1=X2|X3=X4|~list_succeeds(X5))).
% 8.37/1.49 cnf(i_0_220, plain, (cons(esk65_2(X1,X2),esk66_2(X1,X2))=X2|cons(X1,esk67_2(X1,X2))=X2|member_fails(X1,X2))).
% 8.37/1.49 cnf(i_0_125, plain, (not_same_occ_terminates(X1,X2)|~occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2))|~occ_fails(esk20_2(X1,X2),X1,esk22_2(X1,X2))|~member2_terminates(esk19_2(X1,X2),X1,X2))).
% 8.37/1.49 cnf(i_0_269, plain, (times_terminates(X1,X2,X3)|~times_terminates(esk86_3(X1,X2,X3),X2,esk87_3(X1,X2,X3))|~times_fails(esk86_3(X1,X2,X3),X2,esk88_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_85, plain, (X1='0'|occ_fails(X2,X3,X1)|esk5_3(X2,X3,X1)!=X2|~occ_fails(X2,esk7_3(X2,X3,X1),esk8_3(X2,X3,X1)))).
% 8.37/1.49 cnf(i_0_86, plain, (X1=nil|occ_fails(X2,X1,X3)|esk5_3(X2,X1,X3)!=X2|~occ_fails(X2,esk7_3(X2,X1,X3),esk8_3(X2,X1,X3)))).
% 8.37/1.49 cnf(i_0_87, plain, (s(esk8_3(X1,X2,X3))=X3|X3='0'|occ_fails(X1,X2,X3)|esk5_3(X1,X2,X3)!=X1)).
% 8.37/1.49 cnf(i_0_88, plain, (s(esk8_3(X1,X2,X3))=X3|X2=nil|occ_fails(X1,X2,X3)|esk5_3(X1,X2,X3)!=X1)).
% 8.37/1.49 cnf(i_0_501, plain, ('@<_succeeds'('@+'(lh(X1),lh(X2)),X3)|~'@<_succeeds'('@+'(lh(X1),lh(cons(X4,X2))),s(X3))|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_500, plain, ('@<_succeeds'('@+'(lh(X1),lh(X2)),X3)|~'@<_succeeds'('@+'(lh(cons(X4,X1)),lh(X2)),s(X3))|~list_succeeds(X2)|~list_succeeds(X1))).
% 8.37/1.49 cnf(i_0_89, plain, (cons(X1,esk7_3(X1,X2,X3))=X2|X3='0'|occ_fails(X1,X2,X3)|esk5_3(X1,X2,X3)!=X1)).
% 8.37/1.49 cnf(i_0_376, plain, ('@+'('@*'(X1,X2),'@*'(X1,X3))='@*'(X1,'@+'(X2,X3))|~nat_succeeds(X1)|~nat_succeeds(X3)|~nat_succeeds(X2))).
% 8.37/1.49 cnf(i_0_206, plain, (cons(esk56_3(X1,X2,X3),esk58_3(X1,X2,X3))=X3|X1=nil|append_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_267, plain, (plus_fails(X1,X2,X3)|times_fails(X4,X1,X2)|~times_fails(s(X4),X1,X3))).
% 8.37/1.49 cnf(i_0_271, plain, (plus_terminates(X1,X2,X3)|times_fails(X4,X1,X2)|~times_terminates(s(X4),X1,X3))).
% 8.37/1.49 cnf(i_0_208, plain, (cons(esk56_3(X1,X2,X3),esk57_3(X1,X2,X3))=X1|X1=nil|append_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_90, plain, (cons(X1,esk7_3(X1,X2,X3))=X2|X2=nil|occ_fails(X1,X2,X3)|esk5_3(X1,X2,X3)!=X1)).
% 8.37/1.49 cnf(i_0_200, plain, (cons(esk53_3(X1,X2,X3),esk55_3(X1,X2,X3))=X3|X1=nil|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_202, plain, (cons(esk53_3(X1,X2,X3),esk54_3(X1,X2,X3))=X1|X1=nil|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_201, plain, (cons(esk53_3(X1,X2,X3),esk54_3(X1,X2,X3))=X1|X3=X2|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_369, plain, ('@+'('@*'(X1,X2),'@*'(X3,X2))='@*'('@+'(X1,X3),X2)|~nat_succeeds(X2)|~nat_succeeds(X3)|~nat_succeeds(X1))).
% 8.37/1.49 cnf(i_0_207, plain, (cons(esk56_3(X1,X2,X3),esk57_3(X1,X2,X3))=X1|X3=X2|append_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_103, plain, (occ_terminates(X1,X2,X3)|esk9_3(X1,X2,X3)!=X1|~occ_terminates(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))|~gr(esk9_3(X1,X2,X3))|~gr(X1))).
% 8.37/1.49 cnf(i_0_79, plain, (X1='0'|occ_fails(X2,X3,X1)|~occ_fails(X2,esk7_3(X2,X3,X1),esk8_3(X2,X3,X1))|~occ_fails(X2,esk6_3(X2,X3,X1),X1))).
% 8.37/1.49 cnf(i_0_80, plain, (X1=nil|occ_fails(X2,X1,X3)|~occ_fails(X2,esk7_3(X2,X1,X3),esk8_3(X2,X1,X3))|~occ_fails(X2,esk6_3(X2,X1,X3),X3))).
% 8.37/1.49 cnf(i_0_81, plain, (s(esk8_3(X1,X2,X3))=X3|X3='0'|occ_fails(X1,X2,X3)|~occ_fails(X1,esk6_3(X1,X2,X3),X3))).
% 8.37/1.49 cnf(i_0_205, plain, (cons(esk56_3(X1,X2,X3),esk58_3(X1,X2,X3))=X3|X3=X2|append_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_199, plain, (cons(esk53_3(X1,X2,X3),esk55_3(X1,X2,X3))=X3|X3=X2|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_82, plain, (s(esk8_3(X1,X2,X3))=X3|X2=nil|occ_fails(X1,X2,X3)|~occ_fails(X1,esk6_3(X1,X2,X3),X3))).
% 8.37/1.49 cnf(i_0_509, plain, ('**'(esk125_3(X1,X2,X3),cons(X1,esk126_3(X1,X2,X3)))=X2|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_83, plain, (cons(X1,esk7_3(X1,X2,X3))=X2|X3='0'|occ_fails(X1,X2,X3)|~occ_fails(X1,esk6_3(X1,X2,X3),X3))).
% 8.37/1.49 cnf(i_0_129, plain, (occ_terminates(X1,X2,X3)|occ_fails(X1,X4,X5)|member2_fails(X1,X4,X2)|~not_same_occ_terminates(X4,X2))).
% 8.37/1.49 cnf(i_0_167, plain, (cons(esk38_3(X1,X2,X3),esk40_3(X1,X2,X3))=X3|X2=cons(X1,X3)|delete_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_100, plain, (occ_terminates(X1,X2,X3)|~occ_terminates(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))|~occ_terminates(X1,esk10_3(X1,X2,X3),X3)|~gr(esk9_3(X1,X2,X3))|~gr(X1))).
% 8.37/1.49 cnf(i_0_84, plain, (cons(X1,esk7_3(X1,X2,X3))=X2|X2=nil|occ_fails(X1,X2,X3)|~occ_fails(X1,esk6_3(X1,X2,X3),X3))).
% 8.37/1.49 cnf(i_0_101, plain, (s(esk12_3(X1,X2,X3))=X3|occ_terminates(X1,X2,X3)|~occ_terminates(X1,esk10_3(X1,X2,X3),X3)|~gr(esk9_3(X1,X2,X3))|~gr(X1))).
% 8.37/1.49 cnf(i_0_197, plain, (X1=X2|append_succeeds(esk54_3(X3,X2,X1),X2,esk55_3(X3,X2,X1))|~append_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_168, plain, (cons(esk38_3(X1,X2,X3),esk39_3(X1,X2,X3))=X2|X2=cons(X1,X3)|delete_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_164, plain, (cons(esk35_3(X1,X2,X3),esk37_3(X1,X2,X3))=X3|X2=cons(X1,X3)|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_165, plain, (cons(esk35_3(X1,X2,X3),esk36_3(X1,X2,X3))=X2|X2=cons(X1,X3)|~delete_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_256, plain, (X1='0'|times_succeeds(esk82_3(X2,X3,X1),X3,esk83_3(X2,X3,X1))|~times_succeeds(X2,X3,X1))).
% 8.37/1.49 cnf(i_0_257, plain, (X1='0'|times_succeeds(esk82_3(X1,X2,X3),X2,esk83_3(X1,X2,X3))|~times_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_122, plain, (X1=X2|occ_fails(X3,X4,X1)|occ_fails(X3,X5,X2)|member2_fails(X3,X4,X5)|~not_same_occ_fails(X4,X5))).
% 8.37/1.49 cnf(i_0_276, plain, (X1='0'|plus_succeeds(esk89_3(X1,X2,X3),X2,esk90_3(X1,X2,X3))|~plus_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_275, plain, (X1=X2|plus_succeeds(esk89_3(X3,X2,X1),X2,esk90_3(X3,X2,X1))|~plus_succeeds(X3,X2,X1))).
% 8.37/1.49 cnf(i_0_104, plain, (s(esk12_3(X1,X2,X3))=X3|occ_terminates(X1,X2,X3)|esk9_3(X1,X2,X3)!=X1|~gr(esk9_3(X1,X2,X3))|~gr(X1))).
% 8.37/1.49 cnf(i_0_198, plain, (X1=nil|append_succeeds(esk54_3(X1,X2,X3),X2,esk55_3(X1,X2,X3))|~append_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_102, plain, (cons(X1,esk11_3(X1,X2,X3))=X2|occ_terminates(X1,X2,X3)|~occ_terminates(X1,esk10_3(X1,X2,X3),X3)|~gr(esk9_3(X1,X2,X3))|~gr(X1))).
% 8.37/1.49 cnf(i_0_63, plain, (s(esk4_3(X1,X2,X3))=X3|X3='0'|occ_succeeds(X1,esk2_3(X1,X2,X3),X3)|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_105, plain, (cons(X1,esk11_3(X1,X2,X3))=X2|occ_terminates(X1,X2,X3)|esk9_3(X1,X2,X3)!=X1|~gr(esk9_3(X1,X2,X3))|~gr(X1))).
% 8.37/1.49 cnf(i_0_163, plain, (X1=cons(X2,X3)|delete_succeeds(X2,esk36_3(X2,X1,X3),esk37_3(X2,X1,X3))|~delete_succeeds(X2,X1,X3))).
% 8.37/1.49 cnf(i_0_64, plain, (s(esk4_3(X1,X2,X3))=X3|X2=nil|occ_succeeds(X1,esk2_3(X1,X2,X3),X3)|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_65, plain, (cons(X1,esk3_3(X1,X2,X3))=X2|X3='0'|occ_succeeds(X1,esk2_3(X1,X2,X3),X3)|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_128, plain, (occ_fails(X1,X2,X3)|occ_fails(X1,X4,X5)|member2_fails(X1,X4,X2)|gr(X5)|~not_same_occ_terminates(X4,X2))).
% 8.37/1.49 cnf(i_0_66, plain, (cons(X1,esk3_3(X1,X2,X3))=X2|X2=nil|occ_succeeds(X1,esk2_3(X1,X2,X3),X3)|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_127, plain, (occ_fails(X1,X2,X3)|occ_fails(X1,X4,X5)|member2_fails(X1,X4,X2)|gr(X3)|~not_same_occ_terminates(X4,X2))).
% 8.37/1.49 cnf(i_0_106, plain, (cons(esk9_3(X1,X2,X3),esk10_3(X1,X2,X3))=X2|occ_terminates(X1,X2,X3)|~occ_terminates(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_67, plain, (X1='0'|occ_succeeds(X2,esk3_3(X2,X3,X1),esk4_3(X2,X3,X1))|esk1_3(X2,X3,X1)!=X2|~occ_succeeds(X2,X3,X1))).
% 8.37/1.49 cnf(i_0_68, plain, (X1=nil|occ_succeeds(X2,esk3_3(X2,X1,X3),esk4_3(X2,X1,X3))|esk1_3(X2,X1,X3)!=X2|~occ_succeeds(X2,X1,X3))).
% 8.37/1.49 cnf(i_0_107, plain, (cons(esk9_3(X1,X2,X3),esk10_3(X1,X2,X3))=X2|s(esk12_3(X1,X2,X3))=X3|occ_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_108, plain, (cons(esk9_3(X1,X2,X3),esk10_3(X1,X2,X3))=X2|cons(X1,esk11_3(X1,X2,X3))=X2|occ_terminates(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_75, plain, (cons(esk1_3(X1,X2,X3),esk2_3(X1,X2,X3))=X2|s(esk4_3(X1,X2,X3))=X3|X3='0'|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_76, plain, (cons(esk1_3(X1,X2,X3),esk2_3(X1,X2,X3))=X2|s(esk4_3(X1,X2,X3))=X3|X2=nil|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_77, plain, (cons(esk1_3(X1,X2,X3),esk2_3(X1,X2,X3))=X2|cons(X1,esk3_3(X1,X2,X3))=X2|X3='0'|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_93, plain, (cons(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))=X2|s(esk8_3(X1,X2,X3))=X3|X3='0'|occ_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_94, plain, (cons(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))=X2|s(esk8_3(X1,X2,X3))=X3|X2=nil|occ_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_124, plain, (not_same_occ_terminates(X1,X2)|~occ_terminates(esk20_2(X1,X2),X2,esk23_2(X1,X2))|~occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2))|~occ_fails(esk20_2(X1,X2),X2,esk24_2(X1,X2))|~member2_terminates(esk19_2(X1,X2),X1,X2))).
% 8.37/1.49 cnf(i_0_123, plain, (not_same_occ_terminates(X1,X2)|~occ_terminates(esk20_2(X1,X2),X2,esk23_2(X1,X2))|~occ_terminates(esk20_2(X1,X2),X1,esk21_2(X1,X2))|~member2_terminates(esk19_2(X1,X2),X1,X2)|~gr(esk22_2(X1,X2))|~gr(esk24_2(X1,X2)))).
% 8.37/1.49 cnf(i_0_91, plain, (cons(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))=X2|X3='0'|occ_fails(X1,X2,X3)|~occ_fails(X1,esk7_3(X1,X2,X3),esk8_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_92, plain, (cons(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))=X2|X2=nil|occ_fails(X1,X2,X3)|~occ_fails(X1,esk7_3(X1,X2,X3),esk8_3(X1,X2,X3)))).
% 8.37/1.49 cnf(i_0_95, plain, (cons(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))=X2|cons(X1,esk7_3(X1,X2,X3))=X2|X3='0'|occ_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_78, plain, (cons(esk1_3(X1,X2,X3),esk2_3(X1,X2,X3))=X2|cons(X1,esk3_3(X1,X2,X3))=X2|X2=nil|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_96, plain, (cons(esk5_3(X1,X2,X3),esk6_3(X1,X2,X3))=X2|cons(X1,esk7_3(X1,X2,X3))=X2|X2=nil|occ_fails(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_61, plain, (X1='0'|occ_succeeds(X2,esk3_3(X2,X3,X1),esk4_3(X2,X3,X1))|occ_succeeds(X2,esk2_3(X2,X3,X1),X1)|~occ_succeeds(X2,X3,X1))).
% 8.37/1.49 cnf(i_0_62, plain, (X1=nil|occ_succeeds(X2,esk3_3(X2,X1,X3),esk4_3(X2,X1,X3))|occ_succeeds(X2,esk2_3(X2,X1,X3),X3)|~occ_succeeds(X2,X1,X3))).
% 8.37/1.49 cnf(i_0_73, plain, (cons(esk1_3(X1,X2,X3),esk2_3(X1,X2,X3))=X2|X3='0'|occ_succeeds(X1,esk3_3(X1,X2,X3),esk4_3(X1,X2,X3))|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 cnf(i_0_74, plain, (cons(esk1_3(X1,X2,X3),esk2_3(X1,X2,X3))=X2|X2=nil|occ_succeeds(X1,esk3_3(X1,X2,X3),esk4_3(X1,X2,X3))|~occ_succeeds(X1,X2,X3))).
% 8.37/1.49 # End listing active clauses. There is an equivalent clause to each of these in the clausification!
% 8.37/1.49 # Begin printing tableau
% 8.37/1.49 # Found 16 steps
% 8.37/1.49 cnf(i_0_553, negated_conjecture, (occ(esk135_0,cons(esk136_0,esk137_0))!=occ(esk135_0,esk137_0)), inference(start_rule)).
% 8.37/1.49 cnf(i_0_670, plain, (occ(esk135_0,cons(esk136_0,esk137_0))!=occ(esk135_0,esk137_0)), inference(extension_rule, [i_0_113])).
% 8.37/1.49 cnf(i_0_1755, plain, (not_same_occ_succeeds(cons(esk136_0,nil),esk137_0)), inference(extension_rule, [i_0_21])).
% 8.37/1.49 cnf(i_0_3563, plain, (~not_same_occ_fails(cons(esk136_0,nil),esk137_0)), inference(extension_rule, [i_0_133])).
% 8.37/1.49 cnf(i_0_1756, plain, (~occ_succeeds(esk135_0,esk137_0,occ(esk135_0,esk137_0))), inference(extension_rule, [i_0_532])).
% 8.37/1.49 cnf(i_0_4209, plain, (~list_succeeds(esk137_0)), inference(closure_rule, [i_0_555])).
% 8.37/1.49 cnf(i_0_1757, plain, (~occ_succeeds(esk135_0,cons(esk136_0,nil),occ(esk135_0,cons(esk136_0,esk137_0)))), inference(extension_rule, [i_0_20])).
% 8.37/1.49 cnf(i_0_4897, plain, (occ_fails(esk135_0,cons(esk136_0,nil),occ(esk135_0,cons(esk136_0,esk137_0)))), inference(extension_rule, [i_0_99])).
% 8.37/1.49 cnf(i_0_5965, plain, (esk136_0=esk135_0), inference(closure_rule, [i_0_554])).
% 8.37/1.49 cnf(i_0_4899, plain, (~occ_terminates(esk135_0,cons(esk136_0,nil),occ(esk135_0,cons(esk136_0,esk137_0)))), inference(extension_rule, [i_0_538])).
% 8.37/1.49 cnf(i_0_6427, plain, (~list_succeeds(cons(esk136_0,nil))), inference(closure_rule, [i_0_428])).
% 8.37/1.49 cnf(i_0_1758, plain, (~member2_succeeds(esk135_0,cons(esk136_0,nil),esk137_0)), inference(etableau_closure_rule, [i_0_1758, ...])).
% 8.37/1.49 cnf(i_0_3719, plain, (~same_occ_succeeds(cons(esk136_0,nil),esk137_0)), inference(etableau_closure_rule, [i_0_3719, ...])).
% 8.37/1.49 cnf(i_0_5966, plain, (occ_fails(esk135_0,nil,occ(esk135_0,cons(esk136_0,esk137_0)))), inference(etableau_closure_rule, [i_0_5966, ...])).
% 8.37/1.49 cnf(i_0_6428, plain, (~gr(esk135_0)), inference(etableau_closure_rule, [i_0_6428, ...])).
% 8.37/1.49 cnf(i_0_6429, plain, (~gr(cons(esk136_0,nil))), inference(etableau_closure_rule, [i_0_6429, ...])).
% 8.37/1.49 # End printing tableau
% 8.37/1.49 # SZS output end
% 8.37/1.49 # Branches closed with saturation will be marked with an "s"
% 8.37/1.50 # Child (359) has found a proof.
% 8.37/1.50
% 8.37/1.50 # Proof search is over...
% 8.37/1.50 # Freeing feature tree
%------------------------------------------------------------------------------