%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SYO673-1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n013.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 : 600s
% DateTime : Thu Jul 21 18:40:48 EDT 2022
% Result : Unsatisfiable 0.77s 0.96s
% Output : CNFRefutation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SYO673-1 : TPTP v8.1.0. Released v7.3.0.
% 0.11/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jul 9 08:04:14 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.77/0.96 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.77/0.96
% 0.77/0.96 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.77/0.97 cnf(clause_1370, axiom,
% 0.77/0.97 (~ 'E'(0, f(suc(B_82))) | ~ 'E'(0, f(B_80)) |
% 0.77/0.97 ~ iLEQ(suc(B_80), suc(B_81)) | ~ 'E'(0, f(suc(B_81))) |
% 0.77/0.97 ~ 'E'(0, f(B_81)) | ~ 'E'(0, f(A_3)) | ~ 'E'(0, f(B_82)) |
% 0.77/0.97 ~ iLEQ(suc(A_3), suc(B_80)) | ~ 'E'(0, f(suc(A_3))) |
% 0.77/0.97 ~ 'E'(0, f(suc(B_80))) | ~ iLEQ(suc(B_81), suc(B_82)) |
% 0.77/0.97 'E'(f(A_3), f(suc(A_3))) | 'E'(f(B_80), f(suc(B_80))) |
% 0.77/0.97 'E'(f(B_81), f(suc(B_81))) | 'E'(f(B_82), f(suc(B_82))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1497, axiom, ('LE'(f(A), s(s(s(0)))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_345, axiom,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(suc(A_1)))) | ~ 'E'(s(s(0)), f(suc(A_1))) |
% 0.77/0.97 ~ 'E'(f(A_1), f(suc(A_1))) | ~ 'E'(s(s(0)), f(A_1)) |
% 0.77/0.97 iLEQ(suc(A_1), suc(A_1)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1397, axiom,
% 0.77/0.97 (~ 'E'(0, f(suc(B_82))) | ~ 'E'(f(B_82), f(suc(B_82))) |
% 0.77/0.97 ~ 'E'(0, f(B_80)) | ~ iLEQ(suc(B_80), suc(B_81)) |
% 0.77/0.97 ~ 'E'(f(B_81), f(suc(B_81))) | ~ 'E'(f(B_80), f(suc(B_80))) |
% 0.77/0.97 ~ 'E'(0, f(suc(B_81))) | ~ 'E'(0, f(B_81)) | ~ 'E'(0, f(A_3)) |
% 0.77/0.97 ~ 'E'(0, f(B_82)) | ~ 'E'(0, f(suc(suc(B_82)))) |
% 0.77/0.97 ~ iLEQ(suc(A_3), suc(B_80)) | ~ 'E'(0, f(suc(suc(A_3)))) |
% 0.77/0.97 ~ 'E'(0, f(suc(A_3))) | ~ 'E'(f(A_3), f(suc(A_3))) |
% 0.77/0.97 ~ 'E'(0, f(suc(suc(B_80)))) | ~ 'E'(0, f(suc(B_80))) |
% 0.77/0.97 ~ 'E'(0, f(suc(suc(B_81)))) | ~ iLEQ(suc(B_81), suc(B_82)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_418, axiom,
% 0.77/0.97 (~ 'E'(0, f(suc(suc(A_3)))) | ~ 'E'(0, f(suc(A_3))) |
% 0.77/0.97 ~ 'E'(f(A_3), f(suc(A_3))) | ~ 'E'(0, f(A_3)) |
% 0.77/0.97 iLEQ(suc(A_3), suc(A_3)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1415, axiom,
% 0.77/0.97 (~ 'LE'(f(B_67), s(s(0))) | 'E'(s(0), f(B_67)) | 'LE'(f(B_67), s(0)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1472, axiom,
% 0.77/0.97 (~ 'LE'(f(suc(suc(B_67))), s(s(0))) | 'E'(s(0), f(suc(suc(B_67)))) |
% 0.77/0.97 'LE'(f(B_67), s(0)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_225, axiom,
% 0.77/0.97 (~ 'LE'(f(suc(suc(B_79))), s(0)) | 'E'(0, f(suc(suc(B_79)))) |
% 0.77/0.97 'LE'(f(B_79), 0))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_165, axiom,
% 0.77/0.97 (~ 'E'(s(0), f(suc(suc(A_2)))) | ~ 'E'(s(0), f(suc(A_2))) |
% 0.77/0.97 ~ 'E'(f(A_2), f(suc(A_2))) | ~ 'E'(s(0), f(A_2)) |
% 0.77/0.97 iLEQ(suc(A_2), suc(A_2)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_709, axiom, (~ 'LE'(f(z), 0))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_120, axiom,
% 0.77/0.97 (~ 'E'(s(s(0)), f(A_1)) | ~ 'E'(s(s(0)), f(suc(A_1))) |
% 0.77/0.97 'E'(f(A_1), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_243, axiom,
% 0.77/0.97 (~ 'E'(s(0), f(A_2)) | ~ 'E'(s(0), f(suc(A_2))) |
% 0.77/0.97 'E'(f(A_2), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1246, axiom,
% 0.77/0.97 (~ 'LE'(f(suc(B_67)), s(s(0))) | 'E'(s(0), f(suc(B_67))) |
% 0.77/0.97 'LE'(f(B_67), s(0)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1322, axiom,
% 0.77/0.97 (~ 'E'(s(0), f(B_69)) | ~ 'E'(s(0), f(B_68)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(A_2))) | ~ iLEQ(suc(B_69), suc(B_70)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(B_69))) | ~ iLEQ(suc(A_2), suc(B_68)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(B_70))) | ~ iLEQ(suc(B_68), suc(B_69)) |
% 0.77/0.97 ~ 'E'(s(0), f(B_70)) | ~ 'E'(s(0), f(suc(B_68))) |
% 0.77/0.97 ~ 'E'(s(0), f(A_2)) | 'E'(f(A_2), f(suc(A_2))) |
% 0.77/0.97 'E'(f(B_68), f(suc(B_68))) | 'E'(f(B_69), f(suc(B_69))) |
% 0.77/0.97 'E'(f(B_70), f(suc(B_70))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_332, axiom,
% 0.77/0.97 (~ 'E'(0, f(A_3)) | ~ 'E'(0, f(suc(A_3))) | 'E'(f(A_3), f(suc(A_3))) |
% 0.77/0.97 iLEQ(suc(A_3), suc(A_3)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1439, axiom,
% 0.77/0.97 (~ 'LE'(f(suc(B_42)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(B_42))) |
% 0.77/0.97 'LE'(f(B_42), s(s(0))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1017, axiom,
% 0.77/0.97 (~ 'E'(s(s(0)), f(A_1)) | ~ 'E'(s(s(0)), f(suc(suc(B_45)))) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(B_44)) | ~ 'E'(s(s(0)), f(suc(A_1))) |
% 0.77/0.97 ~ iLEQ(suc(A_1), suc(B_43)) | ~ 'E'(f(B_44), f(suc(B_44))) |
% 0.77/0.97 ~ 'E'(f(B_43), f(suc(B_43))) | ~ 'E'(s(s(0)), f(suc(B_45))) |
% 0.77/0.97 ~ iLEQ(suc(B_44), suc(B_45)) | ~ 'E'(s(s(0)), f(suc(suc(B_43)))) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(B_43))) | ~ 'E'(s(s(0)), f(suc(B_44))) |
% 0.77/0.97 ~ 'E'(f(A_1), f(suc(A_1))) | ~ iLEQ(suc(B_43), suc(B_44)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(B_45)) | ~ 'E'(s(s(0)), f(suc(suc(B_44)))) |
% 0.77/0.97 ~ 'E'(f(B_45), f(suc(B_45))) | ~ 'E'(s(s(0)), f(B_43)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(suc(A_1)))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1256, axiom,
% 0.77/0.97 (~ 'LE'(f(suc(B_79)), s(0)) | 'E'(0, f(suc(B_79))) |
% 0.77/0.97 'LE'(f(B_79), 0))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1442, axiom,
% 0.77/0.97 (~ 'LE'(f(B_42), s(s(s(0)))) | 'E'(s(s(0)), f(B_42)) |
% 0.77/0.97 'LE'(f(B_42), s(s(0))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1106, axiom,
% 0.77/0.97 (~ 'E'(s(s(0)), f(A_1)) | ~ 'E'(s(s(0)), f(B_44)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(A_1))) | ~ iLEQ(suc(A_1), suc(B_43)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(B_45))) | ~ iLEQ(suc(B_44), suc(B_45)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(B_43))) | ~ 'E'(s(s(0)), f(suc(B_44))) |
% 0.77/0.97 ~ iLEQ(suc(B_43), suc(B_44)) | ~ 'E'(s(s(0)), f(B_45)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(B_43)) | 'E'(f(A_1), f(suc(A_1))) |
% 0.77/0.97 'E'(f(B_43), f(suc(B_43))) | 'E'(f(B_44), f(suc(B_44))) |
% 0.77/0.97 'E'(f(B_45), f(suc(B_45))))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1132, axiom,
% 0.77/0.97 (~ 'E'(s(0), f(B_69)) | ~ 'E'(s(0), f(B_68)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(suc(B_69)))) | ~ 'E'(s(0), f(suc(A_2))) |
% 0.77/0.97 ~ 'E'(f(B_69), f(suc(B_69))) | ~ iLEQ(suc(B_69), suc(B_70)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(B_69))) | ~ 'E'(s(0), f(suc(suc(B_68)))) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(suc(B_70)))) | ~ 'E'(f(B_70), f(suc(B_70))) |
% 0.77/0.97 ~ iLEQ(suc(A_2), suc(B_68)) | ~ 'E'(s(0), f(suc(B_70))) |
% 0.77/0.97 ~ 'E'(f(B_68), f(suc(B_68))) | ~ iLEQ(suc(B_68), suc(B_69)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(suc(A_2)))) | ~ 'E'(s(0), f(B_70)) |
% 0.77/0.97 ~ 'E'(f(A_2), f(suc(A_2))) | ~ 'E'(s(0), f(suc(B_68))) |
% 0.77/0.97 ~ 'E'(s(0), f(A_2)))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_509, axiom,
% 0.77/0.97 (~ 'LE'(f(B_79), s(0)) | 'E'(0, f(B_79)) | 'LE'(f(B_79), 0))).
% 0.77/0.97
% 0.77/0.97 cnf(clause_1261, axiom,
% 0.77/0.97 (~ 'LE'(f(suc(suc(B_42))), s(s(s(0)))) |
% 0.77/0.97 'E'(s(s(0)), f(suc(suc(B_42)))) | 'LE'(f(B_42), s(s(0))))).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_0, plain,
% 0.77/0.97 (~ 'LE'(f(suc(X_186)), s(0)) | 'E'(0, f(suc(X_186))) |
% 0.77/0.97 'LE'(f(X_186), 0)),
% 0.77/0.97 inference(subst, [], [clause_1256 : [bind(B_79, $fot(X_186))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_1, plain,
% 0.77/0.97 (~ 'LE'(f(X_73), s(s(0))) | 'E'(s(0), f(X_73)) | 'LE'(f(X_73), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1415 : [bind(B_67, $fot(X_73))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_2, plain,
% 0.77/0.97 (~ 'LE'(f(X_68), s(s(0))) | 'E'(s(0), f(X_68)) | 'LE'(f(X_68), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1415 : [bind(B_67, $fot(X_68))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_3, plain,
% 0.77/0.97 (~ 'LE'(f(X_49), s(s(0))) | 'E'(s(0), f(X_49)) | 'LE'(f(X_49), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1415 : [bind(B_67, $fot(X_49))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_4, plain, ('LE'(f(B_42), s(s(s(0))))),
% 0.77/0.97 inference(subst, [], [clause_1497 : [bind(A, $fot(B_42))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_5, plain, ('E'(s(s(0)), f(B_42)) | 'LE'(f(B_42), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(B_42), s(s(s(0)))))],
% 0.77/0.97 [refute_0_4, clause_1442])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_6, plain, ('E'(s(s(0)), f(X_7)) | 'LE'(f(X_7), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_5 : [bind(B_42, $fot(X_7))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_7, plain,
% 0.77/0.97 (~ 'LE'(f(X_7), s(s(0))) | 'E'(s(0), f(X_7)) | 'LE'(f(X_7), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1415 : [bind(B_67, $fot(X_7))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_8, plain,
% 0.77/0.97 ('E'(s(0), f(X_7)) | 'E'(s(s(0)), f(X_7)) | 'LE'(f(X_7), s(0))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(X_7), s(s(0))))],
% 0.77/0.97 [refute_0_6, refute_0_7])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_9, plain,
% 0.77/0.97 ('E'(s(0), f(X_19)) | 'E'(s(s(0)), f(X_19)) | 'LE'(f(X_19), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_8 : [bind(X_7, $fot(X_19))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_10, plain, ('LE'(f(suc(B_42)), s(s(s(0))))),
% 0.77/0.97 inference(subst, [], [clause_1497 : [bind(A, $fot(suc(B_42)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_11, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(B_42))) | 'LE'(f(B_42), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(suc(B_42)), s(s(s(0)))))],
% 0.77/0.97 [refute_0_10, clause_1439])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_12, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(X_17))) | 'LE'(f(X_17), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_11 : [bind(B_42, $fot(X_17))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_13, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(X_17)) | ~ 'E'(s(s(0)), f(suc(X_17))) |
% 0.77/0.97 'E'(f(X_17), f(suc(X_17))) | iLEQ(suc(X_17), suc(X_17))),
% 0.77/0.97 inference(subst, [], [clause_120 : [bind(A_1, $fot(X_17))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_14, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(X_17)) | 'E'(f(X_17), f(suc(X_17))) |
% 0.77/0.97 'LE'(f(X_17), s(s(0))) | iLEQ(suc(X_17), suc(X_17))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_17))))],
% 0.77/0.97 [refute_0_12, refute_0_13])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_15, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(X_19)) | 'E'(f(X_19), f(suc(X_19))) |
% 0.77/0.97 'LE'(f(X_19), s(s(0))) | iLEQ(suc(X_19), suc(X_19))),
% 0.77/0.97 inference(subst, [], [refute_0_14 : [bind(X_17, $fot(X_19))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_16, plain,
% 0.77/0.97 ('E'(f(X_19), f(suc(X_19))) | 'E'(s(0), f(X_19)) |
% 0.77/0.97 'LE'(f(X_19), s(0)) | 'LE'(f(X_19), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_19), suc(X_19))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(X_19)))],
% 0.77/0.97 [refute_0_9, refute_0_15])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_17, plain,
% 0.77/0.97 ('E'(f(X_49), f(suc(X_49))) | 'E'(s(0), f(X_49)) |
% 0.77/0.97 'LE'(f(X_49), s(0)) | 'LE'(f(X_49), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_49), suc(X_49))),
% 0.77/0.97 inference(subst, [], [refute_0_16 : [bind(X_19, $fot(X_49))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_18, plain,
% 0.77/0.97 ('E'(f(X_49), f(suc(X_49))) | 'E'(s(0), f(X_49)) |
% 0.77/0.97 'LE'(f(X_49), s(0)) | iLEQ(suc(X_49), suc(X_49))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(X_49), s(s(0))))],
% 0.77/0.97 [refute_0_17, refute_0_3])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_19, plain,
% 0.77/0.97 ('E'(f(X_67), f(suc(X_67))) | 'E'(s(0), f(X_67)) |
% 0.77/0.97 'LE'(f(X_67), s(0)) | iLEQ(suc(X_67), suc(X_67))),
% 0.77/0.97 inference(subst, [], [refute_0_18 : [bind(X_49, $fot(X_67))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_20, plain,
% 0.77/0.97 ('E'(s(0), f(X_43)) | 'E'(s(s(0)), f(X_43)) | 'LE'(f(X_43), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_8 : [bind(X_7, $fot(X_43))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_21, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(X_42))) | 'LE'(f(X_42), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_11 : [bind(B_42, $fot(X_42))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_22, plain, ('LE'(f(suc(suc(B_42))), s(s(s(0))))),
% 0.77/0.97 inference(subst, [], [clause_1497 : [bind(A, $fot(suc(suc(B_42))))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_23, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(suc(B_42)))) | 'LE'(f(B_42), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(suc(suc(B_42))), s(s(s(0)))))],
% 0.77/0.97 [refute_0_22, clause_1261])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_24, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(suc(X_29)))) | 'LE'(f(X_29), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_23 : [bind(B_42, $fot(X_29))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_25, plain,
% 0.77/0.97 (~ 'E'(f(X_29), f(suc(X_29))) | ~ 'E'(s(s(0)), f(X_29)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_29))) | ~ 'E'(s(s(0)), f(suc(suc(X_29)))) |
% 0.77/0.97 iLEQ(suc(X_29), suc(X_29))),
% 0.77/0.97 inference(subst, [], [clause_345 : [bind(A_1, $fot(X_29))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_26, plain,
% 0.77/0.97 (~ 'E'(f(X_29), f(suc(X_29))) | ~ 'E'(s(s(0)), f(X_29)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_29))) | 'LE'(f(X_29), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_29), suc(X_29))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_29)))))],
% 0.77/0.97 [refute_0_24, refute_0_25])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_27, plain,
% 0.77/0.97 (~ 'E'(f(X_42), f(suc(X_42))) | ~ 'E'(s(s(0)), f(X_42)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_42))) | 'LE'(f(X_42), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_42), suc(X_42))),
% 0.77/0.97 inference(subst, [], [refute_0_26 : [bind(X_29, $fot(X_42))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_28, plain,
% 0.77/0.97 (~ 'E'(f(X_42), f(suc(X_42))) | ~ 'E'(s(s(0)), f(X_42)) |
% 0.77/0.97 'LE'(f(X_42), s(s(0))) | iLEQ(suc(X_42), suc(X_42))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_42))))],
% 0.77/0.97 [refute_0_21, refute_0_27])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_29, plain,
% 0.77/0.97 (~ 'E'(f(X_43), f(suc(X_43))) | ~ 'E'(s(s(0)), f(X_43)) |
% 0.77/0.97 'LE'(f(X_43), s(s(0))) | iLEQ(suc(X_43), suc(X_43))),
% 0.77/0.97 inference(subst, [], [refute_0_28 : [bind(X_42, $fot(X_43))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_30, plain,
% 0.77/0.97 (~ 'E'(f(X_43), f(suc(X_43))) | 'E'(s(0), f(X_43)) |
% 0.77/0.97 'LE'(f(X_43), s(0)) | 'LE'(f(X_43), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_43), suc(X_43))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(X_43)))],
% 0.77/0.97 [refute_0_20, refute_0_29])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_31, plain,
% 0.77/0.97 (~ 'E'(f(X_67), f(suc(X_67))) | 'E'(s(0), f(X_67)) |
% 0.77/0.97 'LE'(f(X_67), s(0)) | 'LE'(f(X_67), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_67), suc(X_67))),
% 0.77/0.97 inference(subst, [], [refute_0_30 : [bind(X_43, $fot(X_67))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_32, plain,
% 0.77/0.97 ('E'(s(0), f(X_67)) | 'LE'(f(X_67), s(0)) | 'LE'(f(X_67), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_67), suc(X_67))),
% 0.77/0.97 inference(resolve, [$cnf('E'(f(X_67), f(suc(X_67))))],
% 0.77/0.97 [refute_0_19, refute_0_31])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_33, plain,
% 0.77/0.97 ('E'(s(0), f(X_68)) | 'LE'(f(X_68), s(0)) | 'LE'(f(X_68), s(s(0))) |
% 0.77/0.97 iLEQ(suc(X_68), suc(X_68))),
% 0.77/0.97 inference(subst, [], [refute_0_32 : [bind(X_67, $fot(X_68))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_34, plain,
% 0.77/0.97 ('E'(s(0), f(X_68)) | 'LE'(f(X_68), s(0)) |
% 0.77/0.97 iLEQ(suc(X_68), suc(X_68))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(X_68), s(s(0))))],
% 0.77/0.97 [refute_0_33, refute_0_2])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_35, plain,
% 0.77/0.97 ('E'(s(0), f(X_72)) | 'LE'(f(X_72), s(0)) |
% 0.77/0.97 iLEQ(suc(X_72), suc(X_72))),
% 0.77/0.97 inference(subst, [], [refute_0_34 : [bind(X_68, $fot(X_72))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_36, plain,
% 0.77/0.97 ('E'(s(0), f(X_36)) | 'E'(s(s(0)), f(X_36)) | 'LE'(f(X_36), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_8 : [bind(X_7, $fot(X_36))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_37, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(X_35))) | 'LE'(f(X_35), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_11 : [bind(B_42, $fot(X_35))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_38, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(suc(X_28)))) | 'LE'(f(X_28), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_23 : [bind(B_42, $fot(X_28))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_39, plain,
% 0.77/0.97 (~ 'E'(f(X_28), f(suc(X_28))) | ~ 'E'(s(s(0)), f(X_28)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_28))) | ~ 'E'(s(s(0)), f(suc(suc(X_28)))) |
% 0.77/0.97 ~ iLEQ(suc(X_28), suc(X_28))),
% 0.77/0.97 inference(subst, [],
% 0.77/0.97 [clause_1017 :
% 0.77/0.97 [bind(A_1, $fot(X_28)), bind(B_43, $fot(X_28)),
% 0.77/0.97 bind(B_44, $fot(X_28)), bind(B_45, $fot(X_28))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_40, plain,
% 0.77/0.97 (~ 'E'(f(X_28), f(suc(X_28))) | ~ 'E'(s(s(0)), f(X_28)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_28))) | ~ iLEQ(suc(X_28), suc(X_28)) |
% 0.77/0.97 'LE'(f(X_28), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_28)))))],
% 0.77/0.97 [refute_0_38, refute_0_39])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_41, plain,
% 0.77/0.97 (~ 'E'(f(X_35), f(suc(X_35))) | ~ 'E'(s(s(0)), f(X_35)) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_35))) | ~ iLEQ(suc(X_35), suc(X_35)) |
% 0.77/0.97 'LE'(f(X_35), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_40 : [bind(X_28, $fot(X_35))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_42, plain,
% 0.77/0.97 (~ 'E'(f(X_35), f(suc(X_35))) | ~ 'E'(s(s(0)), f(X_35)) |
% 0.77/0.97 ~ iLEQ(suc(X_35), suc(X_35)) | 'LE'(f(X_35), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_35))))],
% 0.77/0.97 [refute_0_37, refute_0_41])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_43, plain,
% 0.77/0.97 (~ 'E'(f(X_36), f(suc(X_36))) | ~ 'E'(s(s(0)), f(X_36)) |
% 0.77/0.97 ~ iLEQ(suc(X_36), suc(X_36)) | 'LE'(f(X_36), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_42 : [bind(X_35, $fot(X_36))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_44, plain,
% 0.77/0.97 (~ 'E'(f(X_36), f(suc(X_36))) | ~ iLEQ(suc(X_36), suc(X_36)) |
% 0.77/0.97 'E'(s(0), f(X_36)) | 'LE'(f(X_36), s(0)) | 'LE'(f(X_36), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(X_36)))],
% 0.77/0.97 [refute_0_36, refute_0_43])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_45, plain,
% 0.77/0.97 (~ 'E'(f(X_70), f(suc(X_70))) | ~ iLEQ(suc(X_70), suc(X_70)) |
% 0.77/0.97 'E'(s(0), f(X_70)) | 'LE'(f(X_70), s(0)) | 'LE'(f(X_70), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_44 : [bind(X_36, $fot(X_70))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_46, plain,
% 0.77/0.97 ('E'(s(0), f(X_20)) | 'E'(s(s(0)), f(X_20)) | 'LE'(f(X_20), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_8 : [bind(X_7, $fot(X_20))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_47, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(X_18))) | 'LE'(f(X_18), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_11 : [bind(B_42, $fot(X_18))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_48, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(X_18)) | ~ 'E'(s(s(0)), f(suc(X_18))) |
% 0.77/0.97 ~ iLEQ(suc(X_18), suc(X_18)) | 'E'(f(X_18), f(suc(X_18)))),
% 0.77/0.97 inference(subst, [],
% 0.77/0.97 [clause_1106 :
% 0.77/0.97 [bind(A_1, $fot(X_18)), bind(B_43, $fot(X_18)),
% 0.77/0.97 bind(B_44, $fot(X_18)), bind(B_45, $fot(X_18))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_49, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(X_18)) | ~ iLEQ(suc(X_18), suc(X_18)) |
% 0.77/0.97 'E'(f(X_18), f(suc(X_18))) | 'LE'(f(X_18), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_18))))],
% 0.77/0.97 [refute_0_47, refute_0_48])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_50, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(X_20)) | ~ iLEQ(suc(X_20), suc(X_20)) |
% 0.77/0.97 'E'(f(X_20), f(suc(X_20))) | 'LE'(f(X_20), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_49 : [bind(X_18, $fot(X_20))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_51, plain,
% 0.77/0.97 (~ iLEQ(suc(X_20), suc(X_20)) | 'E'(f(X_20), f(suc(X_20))) |
% 0.77/0.97 'E'(s(0), f(X_20)) | 'LE'(f(X_20), s(0)) | 'LE'(f(X_20), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(X_20)))],
% 0.77/0.97 [refute_0_46, refute_0_50])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_52, plain,
% 0.77/0.97 (~ iLEQ(suc(X_68), suc(X_68)) | 'E'(f(X_68), f(suc(X_68))) |
% 0.77/0.97 'E'(s(0), f(X_68)) | 'LE'(f(X_68), s(0)) | 'LE'(f(X_68), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_51 : [bind(X_20, $fot(X_68))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_53, plain,
% 0.77/0.97 ('E'(f(X_68), f(suc(X_68))) | 'E'(s(0), f(X_68)) |
% 0.77/0.97 'LE'(f(X_68), s(0)) | 'LE'(f(X_68), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf(iLEQ(suc(X_68), suc(X_68)))],
% 0.77/0.97 [refute_0_33, refute_0_52])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_54, plain,
% 0.77/0.97 ('E'(f(X_70), f(suc(X_70))) | 'E'(s(0), f(X_70)) |
% 0.77/0.97 'LE'(f(X_70), s(0)) | 'LE'(f(X_70), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_53 : [bind(X_68, $fot(X_70))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_55, plain,
% 0.77/0.97 (~ iLEQ(suc(X_70), suc(X_70)) | 'E'(s(0), f(X_70)) |
% 0.77/0.97 'LE'(f(X_70), s(0)) | 'LE'(f(X_70), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(f(X_70), f(suc(X_70))))],
% 0.77/0.97 [refute_0_54, refute_0_45])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_56, plain,
% 0.77/0.97 (~ iLEQ(suc(X_72), suc(X_72)) | 'E'(s(0), f(X_72)) |
% 0.77/0.97 'LE'(f(X_72), s(0)) | 'LE'(f(X_72), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_55 : [bind(X_70, $fot(X_72))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_57, plain,
% 0.77/0.97 ('E'(s(0), f(X_72)) | 'LE'(f(X_72), s(0)) | 'LE'(f(X_72), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf(iLEQ(suc(X_72), suc(X_72)))],
% 0.77/0.97 [refute_0_35, refute_0_56])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_58, plain,
% 0.77/0.97 ('E'(s(0), f(X_73)) | 'LE'(f(X_73), s(0)) | 'LE'(f(X_73), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_57 : [bind(X_72, $fot(X_73))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_59, plain, ('E'(s(0), f(X_73)) | 'LE'(f(X_73), s(0))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(X_73), s(s(0))))],
% 0.77/0.97 [refute_0_58, refute_0_1])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_60, plain,
% 0.77/0.97 ('E'(s(0), f(suc(B_79))) | 'LE'(f(suc(B_79)), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_59 : [bind(X_73, $fot(suc(B_79)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_61, plain,
% 0.77/0.97 ('E'(0, f(suc(B_79))) | 'E'(s(0), f(suc(B_79))) | 'LE'(f(B_79), 0)),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(suc(B_79)), s(0)))],
% 0.77/0.97 [refute_0_60, clause_1256])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_62, plain,
% 0.77/0.97 ('E'(0, f(suc(X_185))) | 'E'(s(0), f(suc(X_185))) | 'LE'(f(X_185), 0)),
% 0.77/0.97 inference(subst, [], [refute_0_61 : [bind(B_79, $fot(X_185))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_63, plain,
% 0.77/0.97 ('E'(0, f(suc(X_172))) | 'E'(s(0), f(suc(X_172))) | 'LE'(f(X_172), 0)),
% 0.77/0.97 inference(subst, [], [refute_0_61 : [bind(B_79, $fot(X_172))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_64, plain,
% 0.77/0.97 (~ 'LE'(f(suc(X_103)), s(s(0))) | 'E'(s(0), f(suc(X_103))) |
% 0.77/0.97 'LE'(f(X_103), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1246 : [bind(B_67, $fot(X_103))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_65, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(X_9))) | 'LE'(f(suc(X_9)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_5 : [bind(B_42, $fot(suc(X_9)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_66, plain,
% 0.77/0.97 (~ 'LE'(f(suc(X_9)), s(s(0))) | 'E'(s(0), f(suc(X_9))) |
% 0.77/0.97 'LE'(f(X_9), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1246 : [bind(B_67, $fot(X_9))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_67, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_9))) | 'E'(s(s(0)), f(suc(X_9))) |
% 0.77/0.97 'LE'(f(X_9), s(0))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(suc(X_9)), s(s(0))))],
% 0.77/0.97 [refute_0_65, refute_0_66])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_68, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_102))) | 'E'(s(s(0)), f(suc(X_102))) |
% 0.77/0.97 'LE'(f(X_102), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_67 : [bind(X_9, $fot(X_102))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_69, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_87))) | 'E'(s(s(0)), f(suc(X_87))) |
% 0.77/0.97 'LE'(f(X_87), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_67 : [bind(X_9, $fot(X_87))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_70, plain,
% 0.77/0.97 (~ 'E'(f(suc(X_86)), f(suc(suc(X_86)))) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_86))) | 'LE'(f(suc(X_86)), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(X_86)), suc(suc(X_86)))),
% 0.77/0.97 inference(subst, [], [refute_0_28 : [bind(X_42, $fot(suc(X_86)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_71, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_9))) | 'E'(f(suc(X_9)), f(suc(suc(X_9)))) |
% 0.77/0.97 'LE'(f(suc(X_9)), s(s(0))) | iLEQ(suc(suc(X_9)), suc(suc(X_9)))),
% 0.77/0.97 inference(subst, [], [refute_0_14 : [bind(X_17, $fot(suc(X_9)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_72, plain,
% 0.77/0.97 ('E'(f(suc(X_9)), f(suc(suc(X_9)))) | 'E'(s(0), f(suc(X_9))) |
% 0.77/0.97 'LE'(f(X_9), s(0)) | 'LE'(f(suc(X_9)), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(X_9)), suc(suc(X_9)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_9))))],
% 0.77/0.97 [refute_0_67, refute_0_71])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_73, plain,
% 0.77/0.97 ('E'(f(suc(X_86)), f(suc(suc(X_86)))) | 'E'(s(0), f(suc(X_86))) |
% 0.77/0.97 'LE'(f(X_86), s(0)) | 'LE'(f(suc(X_86)), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(X_86)), suc(suc(X_86)))),
% 0.77/0.97 inference(subst, [], [refute_0_72 : [bind(X_9, $fot(X_86))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_74, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_86))) | 'E'(s(0), f(suc(X_86))) |
% 0.77/0.97 'LE'(f(X_86), s(0)) | 'LE'(f(suc(X_86)), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(X_86)), suc(suc(X_86)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(f(suc(X_86)), f(suc(suc(X_86)))))],
% 0.77/0.97 [refute_0_73, refute_0_70])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_75, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_87))) | 'E'(s(0), f(suc(X_87))) |
% 0.77/0.97 'LE'(f(X_87), s(0)) | 'LE'(f(suc(X_87)), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(X_87)), suc(suc(X_87)))),
% 0.77/0.97 inference(subst, [], [refute_0_74 : [bind(X_86, $fot(X_87))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_76, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_87))) | 'LE'(f(X_87), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_87)), s(s(0))) | iLEQ(suc(suc(X_87)), suc(suc(X_87)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_87))))],
% 0.77/0.97 [refute_0_69, refute_0_75])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_77, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_101))) | 'LE'(f(X_101), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_101)), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(X_101)), suc(suc(X_101)))),
% 0.77/0.97 inference(subst, [], [refute_0_76 : [bind(X_87, $fot(X_101))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_78, plain,
% 0.77/0.97 (~ 'E'(f(suc(X_97)), f(suc(suc(X_97)))) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(X_97))) |
% 0.77/0.97 ~ iLEQ(suc(suc(X_97)), suc(suc(X_97))) | 'LE'(f(suc(X_97)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_42 : [bind(X_35, $fot(suc(X_97)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_79, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_96))) | 'E'(s(s(0)), f(suc(X_96))) |
% 0.77/0.97 'LE'(f(X_96), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_67 : [bind(X_9, $fot(X_96))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_80, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_88))) |
% 0.77/0.97 ~ iLEQ(suc(suc(X_88)), suc(suc(X_88))) |
% 0.77/0.97 'E'(f(suc(X_88)), f(suc(suc(X_88)))) | 'LE'(f(suc(X_88)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_49 : [bind(X_18, $fot(suc(X_88)))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_81, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_88))) | 'LE'(f(X_88), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_88)), s(s(0))) | iLEQ(suc(suc(X_88)), suc(suc(X_88)))),
% 0.77/0.97 inference(subst, [], [refute_0_76 : [bind(X_87, $fot(X_88))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_82, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_88))) | 'E'(f(suc(X_88)), f(suc(suc(X_88)))) |
% 0.77/0.97 'E'(s(0), f(suc(X_88))) | 'LE'(f(X_88), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_88)), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf(iLEQ(suc(suc(X_88)), suc(suc(X_88))))],
% 0.77/0.97 [refute_0_81, refute_0_80])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_83, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_96))) | 'E'(f(suc(X_96)), f(suc(suc(X_96)))) |
% 0.77/0.97 'E'(s(0), f(suc(X_96))) | 'LE'(f(X_96), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_96)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_82 : [bind(X_88, $fot(X_96))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_84, plain,
% 0.77/0.97 ('E'(f(suc(X_96)), f(suc(suc(X_96)))) | 'E'(s(0), f(suc(X_96))) |
% 0.77/0.97 'LE'(f(X_96), s(0)) | 'LE'(f(suc(X_96)), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_96))))],
% 0.77/0.97 [refute_0_79, refute_0_83])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_85, plain,
% 0.77/0.97 ('E'(f(suc(X_97)), f(suc(suc(X_97)))) | 'E'(s(0), f(suc(X_97))) |
% 0.77/0.97 'LE'(f(X_97), s(0)) | 'LE'(f(suc(X_97)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_84 : [bind(X_96, $fot(X_97))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_86, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_97))) |
% 0.77/0.97 ~ iLEQ(suc(suc(X_97)), suc(suc(X_97))) | 'E'(s(0), f(suc(X_97))) |
% 0.77/0.97 'LE'(f(X_97), s(0)) | 'LE'(f(suc(X_97)), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(f(suc(X_97)), f(suc(suc(X_97)))))],
% 0.77/0.97 [refute_0_85, refute_0_78])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_87, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_101))) |
% 0.77/0.97 ~ iLEQ(suc(suc(X_101)), suc(suc(X_101))) | 'E'(s(0), f(suc(X_101))) |
% 0.77/0.97 'LE'(f(X_101), s(0)) | 'LE'(f(suc(X_101)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_86 : [bind(X_97, $fot(X_101))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_88, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_101))) | 'E'(s(0), f(suc(X_101))) |
% 0.77/0.97 'LE'(f(X_101), s(0)) | 'LE'(f(suc(X_101)), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf(iLEQ(suc(suc(X_101)), suc(suc(X_101))))],
% 0.77/0.97 [refute_0_77, refute_0_87])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_89, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(X_102))) | 'E'(s(0), f(suc(X_102))) |
% 0.77/0.97 'LE'(f(X_102), s(0)) | 'LE'(f(suc(X_102)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_88 : [bind(X_101, $fot(X_102))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_90, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_102))) | 'LE'(f(X_102), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_102)), s(s(0)))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_102))))],
% 0.77/0.97 [refute_0_68, refute_0_89])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_91, plain,
% 0.77/0.97 ('E'(s(0), f(suc(X_103))) | 'LE'(f(X_103), s(0)) |
% 0.77/0.97 'LE'(f(suc(X_103)), s(s(0)))),
% 0.77/0.97 inference(subst, [], [refute_0_90 : [bind(X_102, $fot(X_103))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_92, plain, ('E'(s(0), f(suc(X_103))) | 'LE'(f(X_103), s(0))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(suc(X_103)), s(s(0))))],
% 0.77/0.97 [refute_0_91, refute_0_64])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_93, plain, ('E'(s(0), f(suc(X_133))) | 'LE'(f(X_133), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_92 : [bind(X_103, $fot(X_133))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_94, plain,
% 0.77/0.97 (~ 'E'(f(X_126), f(suc(X_126))) | ~ 'E'(s(0), f(X_126)) |
% 0.77/0.97 ~ 'E'(s(0), f(suc(X_126))) | ~ 'E'(s(0), f(suc(suc(X_126)))) |
% 0.77/0.97 iLEQ(suc(X_126), suc(X_126))),
% 0.77/0.97 inference(subst, [], [clause_165 : [bind(A_2, $fot(X_126))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_95, plain,
% 0.77/0.97 (~ 'LE'(f(suc(suc(X_125))), s(s(0))) | 'E'(s(0), f(suc(suc(X_125)))) |
% 0.77/0.97 'LE'(f(X_125), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1472 : [bind(B_67, $fot(X_125))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_96, plain,
% 0.77/0.97 ('E'(s(s(0)), f(suc(suc(X_11)))) | 'LE'(f(suc(suc(X_11))), s(s(0)))),
% 0.77/0.97 inference(subst, [],
% 0.77/0.97 [refute_0_5 : [bind(B_42, $fot(suc(suc(X_11))))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_97, plain,
% 0.77/0.97 (~ 'LE'(f(suc(suc(X_11))), s(s(0))) | 'E'(s(0), f(suc(suc(X_11)))) |
% 0.77/0.97 'LE'(f(X_11), s(0))),
% 0.77/0.97 inference(subst, [], [clause_1472 : [bind(B_67, $fot(X_11))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_98, plain,
% 0.77/0.97 ('E'(s(0), f(suc(suc(X_11)))) | 'E'(s(s(0)), f(suc(suc(X_11)))) |
% 0.77/0.97 'LE'(f(X_11), s(0))),
% 0.77/0.97 inference(resolve, [$cnf('LE'(f(suc(suc(X_11))), s(s(0))))],
% 0.77/0.97 [refute_0_96, refute_0_97])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_99, plain,
% 0.77/0.97 ('E'(s(0), f(suc(suc(X_124)))) | 'E'(s(s(0)), f(suc(suc(X_124)))) |
% 0.77/0.97 'LE'(f(X_124), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_98 : [bind(X_11, $fot(X_124))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_100, plain,
% 0.77/0.97 ('E'(s(0), f(suc(suc(X_111)))) | 'E'(s(s(0)), f(suc(suc(X_111)))) |
% 0.77/0.97 'LE'(f(X_111), s(0))),
% 0.77/0.97 inference(subst, [], [refute_0_98 : [bind(X_11, $fot(X_111))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_101, plain,
% 0.77/0.97 (~ 'E'(f(suc(suc(X_99))), f(suc(suc(suc(X_99))))) |
% 0.77/0.97 ~ 'E'(s(s(0)), f(suc(suc(X_99)))) | 'LE'(f(suc(suc(X_99))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_99))), suc(suc(suc(X_99))))),
% 0.77/0.97 inference(subst, [],
% 0.77/0.97 [refute_0_28 : [bind(X_42, $fot(suc(suc(X_99))))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_102, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(suc(X_11)))) |
% 0.77/0.97 'E'(f(suc(suc(X_11))), f(suc(suc(suc(X_11))))) |
% 0.77/0.97 'LE'(f(suc(suc(X_11))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_11))), suc(suc(suc(X_11))))),
% 0.77/0.97 inference(subst, [],
% 0.77/0.97 [refute_0_14 : [bind(X_17, $fot(suc(suc(X_11))))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_103, plain,
% 0.77/0.97 ('E'(f(suc(suc(X_11))), f(suc(suc(suc(X_11))))) |
% 0.77/0.97 'E'(s(0), f(suc(suc(X_11)))) | 'LE'(f(X_11), s(0)) |
% 0.77/0.97 'LE'(f(suc(suc(X_11))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_11))), suc(suc(suc(X_11))))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_11)))))],
% 0.77/0.97 [refute_0_98, refute_0_102])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_104, plain,
% 0.77/0.97 ('E'(f(suc(suc(X_99))), f(suc(suc(suc(X_99))))) |
% 0.77/0.97 'E'(s(0), f(suc(suc(X_99)))) | 'LE'(f(X_99), s(0)) |
% 0.77/0.97 'LE'(f(suc(suc(X_99))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_99))), suc(suc(suc(X_99))))),
% 0.77/0.97 inference(subst, [], [refute_0_103 : [bind(X_11, $fot(X_99))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_105, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(suc(X_99)))) | 'E'(s(0), f(suc(suc(X_99)))) |
% 0.77/0.97 'LE'(f(X_99), s(0)) | 'LE'(f(suc(suc(X_99))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_99))), suc(suc(suc(X_99))))),
% 0.77/0.97 inference(resolve,
% 0.77/0.97 [$cnf('E'(f(suc(suc(X_99))), f(suc(suc(suc(X_99))))))],
% 0.77/0.97 [refute_0_104, refute_0_101])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_106, plain,
% 0.77/0.97 (~ 'E'(s(s(0)), f(suc(suc(X_111)))) | 'E'(s(0), f(suc(suc(X_111)))) |
% 0.77/0.97 'LE'(f(X_111), s(0)) | 'LE'(f(suc(suc(X_111))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_111))), suc(suc(suc(X_111))))),
% 0.77/0.97 inference(subst, [], [refute_0_105 : [bind(X_99, $fot(X_111))]])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_107, plain,
% 0.77/0.97 ('E'(s(0), f(suc(suc(X_111)))) | 'LE'(f(X_111), s(0)) |
% 0.77/0.97 'LE'(f(suc(suc(X_111))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_111))), suc(suc(suc(X_111))))),
% 0.77/0.97 inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_111)))))],
% 0.77/0.97 [refute_0_100, refute_0_106])).
% 0.77/0.97
% 0.77/0.97 cnf(refute_0_108, plain,
% 0.77/0.97 ('E'(s(0), f(suc(suc(X_123)))) | 'LE'(f(X_123), s(0)) |
% 0.77/0.97 'LE'(f(suc(suc(X_123))), s(s(0))) |
% 0.77/0.97 iLEQ(suc(suc(suc(X_123))), suc(suc(suc(X_123))))),
% 0.77/0.97 inference(subst, [], [refute_0_107 : [bind(X_111, $fot(X_123))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_109, plain,
% 0.77/0.98 (~ 'E'(f(suc(suc(X_120))), f(suc(suc(suc(X_120))))) |
% 0.77/0.98 ~ 'E'(s(s(0)), f(suc(suc(X_120)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_120))), suc(suc(suc(X_120)))) |
% 0.77/0.98 'LE'(f(suc(suc(X_120))), s(s(0)))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_42 : [bind(X_35, $fot(suc(suc(X_120))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_110, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(X_119)))) | 'E'(s(s(0)), f(suc(suc(X_119)))) |
% 0.77/0.98 'LE'(f(X_119), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_98 : [bind(X_11, $fot(X_119))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_111, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_112)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_112))), suc(suc(suc(X_112)))) |
% 0.77/0.98 'E'(f(suc(suc(X_112))), f(suc(suc(suc(X_112))))) |
% 0.77/0.98 'LE'(f(suc(suc(X_112))), s(s(0)))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_49 : [bind(X_18, $fot(suc(suc(X_112))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_112, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(X_112)))) | 'LE'(f(X_112), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_112))), s(s(0))) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_112))), suc(suc(suc(X_112))))),
% 0.77/0.98 inference(subst, [], [refute_0_107 : [bind(X_111, $fot(X_112))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_113, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_112)))) |
% 0.77/0.98 'E'(f(suc(suc(X_112))), f(suc(suc(suc(X_112))))) |
% 0.77/0.98 'E'(s(0), f(suc(suc(X_112)))) | 'LE'(f(X_112), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_112))), s(s(0)))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf(iLEQ(suc(suc(suc(X_112))), suc(suc(suc(X_112)))))],
% 0.77/0.98 [refute_0_112, refute_0_111])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_114, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_119)))) |
% 0.77/0.98 'E'(f(suc(suc(X_119))), f(suc(suc(suc(X_119))))) |
% 0.77/0.98 'E'(s(0), f(suc(suc(X_119)))) | 'LE'(f(X_119), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_119))), s(s(0)))),
% 0.77/0.98 inference(subst, [], [refute_0_113 : [bind(X_112, $fot(X_119))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_115, plain,
% 0.77/0.98 ('E'(f(suc(suc(X_119))), f(suc(suc(suc(X_119))))) |
% 0.77/0.98 'E'(s(0), f(suc(suc(X_119)))) | 'LE'(f(X_119), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_119))), s(s(0)))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_119)))))],
% 0.77/0.98 [refute_0_110, refute_0_114])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_116, plain,
% 0.77/0.98 ('E'(f(suc(suc(X_120))), f(suc(suc(suc(X_120))))) |
% 0.77/0.98 'E'(s(0), f(suc(suc(X_120)))) | 'LE'(f(X_120), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_120))), s(s(0)))),
% 0.77/0.98 inference(subst, [], [refute_0_115 : [bind(X_119, $fot(X_120))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_117, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_120)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_120))), suc(suc(suc(X_120)))) |
% 0.77/0.98 'E'(s(0), f(suc(suc(X_120)))) | 'LE'(f(X_120), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_120))), s(s(0)))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf('E'(f(suc(suc(X_120))), f(suc(suc(suc(X_120))))))],
% 0.77/0.98 [refute_0_116, refute_0_109])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_118, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_123)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_123))), suc(suc(suc(X_123)))) |
% 0.77/0.98 'E'(s(0), f(suc(suc(X_123)))) | 'LE'(f(X_123), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_123))), s(s(0)))),
% 0.77/0.98 inference(subst, [], [refute_0_117 : [bind(X_120, $fot(X_123))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_119, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_123)))) | 'E'(s(0), f(suc(suc(X_123)))) |
% 0.77/0.98 'LE'(f(X_123), s(0)) | 'LE'(f(suc(suc(X_123))), s(s(0)))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf(iLEQ(suc(suc(suc(X_123))), suc(suc(suc(X_123)))))],
% 0.77/0.98 [refute_0_108, refute_0_118])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_120, plain,
% 0.77/0.98 (~ 'E'(s(s(0)), f(suc(suc(X_124)))) | 'E'(s(0), f(suc(suc(X_124)))) |
% 0.77/0.98 'LE'(f(X_124), s(0)) | 'LE'(f(suc(suc(X_124))), s(s(0)))),
% 0.77/0.98 inference(subst, [], [refute_0_119 : [bind(X_123, $fot(X_124))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_121, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(X_124)))) | 'LE'(f(X_124), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_124))), s(s(0)))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_124)))))],
% 0.77/0.98 [refute_0_99, refute_0_120])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_122, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(X_125)))) | 'LE'(f(X_125), s(0)) |
% 0.77/0.98 'LE'(f(suc(suc(X_125))), s(s(0)))),
% 0.77/0.98 inference(subst, [], [refute_0_121 : [bind(X_124, $fot(X_125))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_123, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(X_125)))) | 'LE'(f(X_125), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(suc(suc(X_125))), s(s(0))))],
% 0.77/0.98 [refute_0_122, refute_0_95])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_124, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(X_126)))) | 'LE'(f(X_126), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_123 : [bind(X_125, $fot(X_126))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_125, plain,
% 0.77/0.98 (~ 'E'(f(X_126), f(suc(X_126))) | ~ 'E'(s(0), f(X_126)) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_126))) | 'LE'(f(X_126), s(0)) |
% 0.77/0.98 iLEQ(suc(X_126), suc(X_126))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_126)))))],
% 0.77/0.98 [refute_0_124, refute_0_94])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_126, plain,
% 0.77/0.98 (~ 'E'(f(X_133), f(suc(X_133))) | ~ 'E'(s(0), f(X_133)) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_133))) | 'LE'(f(X_133), s(0)) |
% 0.77/0.98 iLEQ(suc(X_133), suc(X_133))),
% 0.77/0.98 inference(subst, [], [refute_0_125 : [bind(X_126, $fot(X_133))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_127, plain,
% 0.77/0.98 (~ 'E'(f(X_133), f(suc(X_133))) | ~ 'E'(s(0), f(X_133)) |
% 0.77/0.98 'LE'(f(X_133), s(0)) | iLEQ(suc(X_133), suc(X_133))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_133))))],
% 0.77/0.98 [refute_0_93, refute_0_126])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_128, plain,
% 0.77/0.98 (~ 'E'(f(suc(X_170)), f(suc(suc(X_170)))) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_170))) | 'LE'(f(suc(X_170)), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(X_170)), suc(suc(X_170)))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_127 : [bind(X_133, $fot(suc(X_170)))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_129, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_104)) | ~ 'E'(s(0), f(suc(X_104))) |
% 0.77/0.98 'E'(f(X_104), f(suc(X_104))) | iLEQ(suc(X_104), suc(X_104))),
% 0.77/0.98 inference(subst, [], [clause_243 : [bind(A_2, $fot(X_104))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_130, plain, ('E'(s(0), f(suc(X_104))) | 'LE'(f(X_104), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_92 : [bind(X_103, $fot(X_104))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_131, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_104)) | 'E'(f(X_104), f(suc(X_104))) |
% 0.77/0.98 'LE'(f(X_104), s(0)) | iLEQ(suc(X_104), suc(X_104))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_104))))],
% 0.77/0.98 [refute_0_130, refute_0_129])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_132, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(B_79))) | 'E'(f(suc(B_79)), f(suc(suc(B_79)))) |
% 0.77/0.98 'LE'(f(suc(B_79)), s(0)) | iLEQ(suc(suc(B_79)), suc(suc(B_79)))),
% 0.77/0.98 inference(subst, [], [refute_0_131 : [bind(X_104, $fot(suc(B_79)))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_133, plain,
% 0.77/0.98 ('E'(0, f(suc(B_79))) | 'E'(f(suc(B_79)), f(suc(suc(B_79)))) |
% 0.77/0.98 'LE'(f(B_79), 0) | 'LE'(f(suc(B_79)), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(B_79)), suc(suc(B_79)))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(B_79))))],
% 0.77/0.98 [refute_0_61, refute_0_132])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_134, plain,
% 0.77/0.98 ('E'(0, f(suc(X_170))) | 'E'(f(suc(X_170)), f(suc(suc(X_170)))) |
% 0.77/0.98 'LE'(f(X_170), 0) | 'LE'(f(suc(X_170)), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(X_170)), suc(suc(X_170)))),
% 0.77/0.98 inference(subst, [], [refute_0_133 : [bind(B_79, $fot(X_170))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_135, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_170))) | 'E'(0, f(suc(X_170))) |
% 0.77/0.98 'LE'(f(X_170), 0) | 'LE'(f(suc(X_170)), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(X_170)), suc(suc(X_170)))),
% 0.77/0.98 inference(resolve, [$cnf('E'(f(suc(X_170)), f(suc(suc(X_170)))))],
% 0.77/0.98 [refute_0_134, refute_0_128])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_136, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_172))) | 'E'(0, f(suc(X_172))) |
% 0.77/0.98 'LE'(f(X_172), 0) | 'LE'(f(suc(X_172)), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(X_172)), suc(suc(X_172)))),
% 0.77/0.98 inference(subst, [], [refute_0_135 : [bind(X_170, $fot(X_172))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_137, plain,
% 0.77/0.98 ('E'(0, f(suc(X_172))) | 'LE'(f(X_172), 0) |
% 0.77/0.98 'LE'(f(suc(X_172)), s(0)) | iLEQ(suc(suc(X_172)), suc(suc(X_172)))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_172))))],
% 0.77/0.98 [refute_0_63, refute_0_136])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_138, plain,
% 0.77/0.98 ('E'(0, f(suc(X_184))) | 'LE'(f(X_184), 0) |
% 0.77/0.98 'LE'(f(suc(X_184)), s(0)) | iLEQ(suc(suc(X_184)), suc(suc(X_184)))),
% 0.77/0.98 inference(subst, [], [refute_0_137 : [bind(X_172, $fot(X_184))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_139, plain, ('E'(s(0), f(suc(X_131))) | 'LE'(f(X_131), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_92 : [bind(X_103, $fot(X_131))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_140, plain,
% 0.77/0.98 (~ 'E'(f(X_126), f(suc(X_126))) | ~ 'E'(s(0), f(X_126)) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_126))) | ~ 'E'(s(0), f(suc(suc(X_126)))) |
% 0.77/0.98 ~ iLEQ(suc(X_126), suc(X_126))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [clause_1132 :
% 0.77/0.98 [bind(A_2, $fot(X_126)), bind(B_68, $fot(X_126)),
% 0.77/0.98 bind(B_69, $fot(X_126)), bind(B_70, $fot(X_126))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_141, plain,
% 0.77/0.98 (~ 'E'(f(X_126), f(suc(X_126))) | ~ 'E'(s(0), f(X_126)) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_126))) | ~ iLEQ(suc(X_126), suc(X_126)) |
% 0.77/0.98 'LE'(f(X_126), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_126)))))],
% 0.77/0.98 [refute_0_124, refute_0_140])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_142, plain,
% 0.77/0.98 (~ 'E'(f(X_131), f(suc(X_131))) | ~ 'E'(s(0), f(X_131)) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_131))) | ~ iLEQ(suc(X_131), suc(X_131)) |
% 0.77/0.98 'LE'(f(X_131), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_141 : [bind(X_126, $fot(X_131))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_143, plain,
% 0.77/0.98 (~ 'E'(f(X_131), f(suc(X_131))) | ~ 'E'(s(0), f(X_131)) |
% 0.77/0.98 ~ iLEQ(suc(X_131), suc(X_131)) | 'LE'(f(X_131), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_131))))],
% 0.77/0.98 [refute_0_139, refute_0_142])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_144, plain,
% 0.77/0.98 (~ 'E'(f(suc(X_179)), f(suc(suc(X_179)))) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(X_179))) |
% 0.77/0.98 ~ iLEQ(suc(suc(X_179)), suc(suc(X_179))) | 'LE'(f(suc(X_179)), s(0))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_143 : [bind(X_131, $fot(suc(X_179)))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_145, plain,
% 0.77/0.98 ('E'(0, f(suc(X_178))) | 'E'(s(0), f(suc(X_178))) | 'LE'(f(X_178), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_61 : [bind(B_79, $fot(X_178))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_146, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_104)) | ~ 'E'(s(0), f(suc(X_104))) |
% 0.77/0.98 ~ iLEQ(suc(X_104), suc(X_104)) | 'E'(f(X_104), f(suc(X_104)))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [clause_1322 :
% 0.77/0.98 [bind(A_2, $fot(X_104)), bind(B_68, $fot(X_104)),
% 0.77/0.98 bind(B_69, $fot(X_104)), bind(B_70, $fot(X_104))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_147, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_104)) | ~ iLEQ(suc(X_104), suc(X_104)) |
% 0.77/0.98 'E'(f(X_104), f(suc(X_104))) | 'LE'(f(X_104), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_104))))],
% 0.77/0.98 [refute_0_130, refute_0_146])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_148, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_173))) |
% 0.77/0.98 ~ iLEQ(suc(suc(X_173)), suc(suc(X_173))) |
% 0.77/0.98 'E'(f(suc(X_173)), f(suc(suc(X_173)))) | 'LE'(f(suc(X_173)), s(0))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_147 : [bind(X_104, $fot(suc(X_173)))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_149, plain,
% 0.77/0.98 ('E'(0, f(suc(X_173))) | 'LE'(f(X_173), 0) |
% 0.77/0.98 'LE'(f(suc(X_173)), s(0)) | iLEQ(suc(suc(X_173)), suc(suc(X_173)))),
% 0.77/0.98 inference(subst, [], [refute_0_137 : [bind(X_172, $fot(X_173))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_150, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_173))) | 'E'(0, f(suc(X_173))) |
% 0.77/0.98 'E'(f(suc(X_173)), f(suc(suc(X_173)))) | 'LE'(f(X_173), 0) |
% 0.77/0.98 'LE'(f(suc(X_173)), s(0))),
% 0.77/0.98 inference(resolve, [$cnf(iLEQ(suc(suc(X_173)), suc(suc(X_173))))],
% 0.77/0.98 [refute_0_149, refute_0_148])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_151, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_178))) | 'E'(0, f(suc(X_178))) |
% 0.77/0.98 'E'(f(suc(X_178)), f(suc(suc(X_178)))) | 'LE'(f(X_178), 0) |
% 0.77/0.98 'LE'(f(suc(X_178)), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_150 : [bind(X_173, $fot(X_178))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_152, plain,
% 0.77/0.98 ('E'(0, f(suc(X_178))) | 'E'(f(suc(X_178)), f(suc(suc(X_178)))) |
% 0.77/0.98 'LE'(f(X_178), 0) | 'LE'(f(suc(X_178)), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_178))))],
% 0.77/0.98 [refute_0_145, refute_0_151])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_153, plain,
% 0.77/0.98 ('E'(0, f(suc(X_179))) | 'E'(f(suc(X_179)), f(suc(suc(X_179)))) |
% 0.77/0.98 'LE'(f(X_179), 0) | 'LE'(f(suc(X_179)), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_152 : [bind(X_178, $fot(X_179))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_154, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_179))) |
% 0.77/0.98 ~ iLEQ(suc(suc(X_179)), suc(suc(X_179))) | 'E'(0, f(suc(X_179))) |
% 0.77/0.98 'LE'(f(X_179), 0) | 'LE'(f(suc(X_179)), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(f(suc(X_179)), f(suc(suc(X_179)))))],
% 0.77/0.98 [refute_0_153, refute_0_144])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_155, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_184))) |
% 0.77/0.98 ~ iLEQ(suc(suc(X_184)), suc(suc(X_184))) | 'E'(0, f(suc(X_184))) |
% 0.77/0.98 'LE'(f(X_184), 0) | 'LE'(f(suc(X_184)), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_154 : [bind(X_179, $fot(X_184))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_156, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_184))) | 'E'(0, f(suc(X_184))) |
% 0.77/0.98 'LE'(f(X_184), 0) | 'LE'(f(suc(X_184)), s(0))),
% 0.77/0.98 inference(resolve, [$cnf(iLEQ(suc(suc(X_184)), suc(suc(X_184))))],
% 0.77/0.98 [refute_0_138, refute_0_155])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_157, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(X_185))) | 'E'(0, f(suc(X_185))) |
% 0.77/0.98 'LE'(f(X_185), 0) | 'LE'(f(suc(X_185)), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_156 : [bind(X_184, $fot(X_185))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_158, plain,
% 0.77/0.98 ('E'(0, f(suc(X_185))) | 'LE'(f(X_185), 0) |
% 0.77/0.98 'LE'(f(suc(X_185)), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(X_185))))],
% 0.77/0.98 [refute_0_62, refute_0_157])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_159, plain,
% 0.77/0.98 ('E'(0, f(suc(X_186))) | 'LE'(f(X_186), 0) |
% 0.77/0.98 'LE'(f(suc(X_186)), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_158 : [bind(X_185, $fot(X_186))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_160, plain, ('E'(0, f(suc(X_186))) | 'LE'(f(X_186), 0)),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(suc(X_186)), s(0)))],
% 0.77/0.98 [refute_0_159, refute_0_0])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_161, plain, ('E'(0, f(suc(z))) | 'LE'(f(z), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_160 : [bind(X_186, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_162, plain,
% 0.77/0.98 (~ 'LE'(f(suc(suc(X_225))), s(0)) | 'E'(0, f(suc(suc(X_225)))) |
% 0.77/0.98 'LE'(f(X_225), 0)),
% 0.77/0.98 inference(subst, [], [clause_225 : [bind(B_79, $fot(X_225))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_163, plain,
% 0.77/0.98 ('E'(s(0), f(suc(suc(B_79)))) | 'LE'(f(suc(suc(B_79))), s(0))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_59 : [bind(X_73, $fot(suc(suc(B_79))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_164, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(B_79)))) | 'E'(s(0), f(suc(suc(B_79)))) |
% 0.77/0.98 'LE'(f(B_79), 0)),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(suc(suc(B_79))), s(0)))],
% 0.77/0.98 [refute_0_163, clause_225])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_165, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_224)))) | 'E'(s(0), f(suc(suc(X_224)))) |
% 0.77/0.98 'LE'(f(X_224), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_164 : [bind(B_79, $fot(X_224))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_166, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_191)))) | 'E'(s(0), f(suc(suc(X_191)))) |
% 0.77/0.98 'LE'(f(X_191), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_164 : [bind(B_79, $fot(X_191))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_167, plain,
% 0.77/0.98 (~ 'E'(f(suc(suc(X_183))), f(suc(suc(suc(X_183))))) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(suc(X_183)))) | 'LE'(f(suc(suc(X_183))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_183))), suc(suc(suc(X_183))))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_127 : [bind(X_133, $fot(suc(suc(X_183))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_168, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(B_79)))) |
% 0.77/0.98 'E'(f(suc(suc(B_79))), f(suc(suc(suc(B_79))))) |
% 0.77/0.98 'LE'(f(suc(suc(B_79))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(B_79))), suc(suc(suc(B_79))))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_131 : [bind(X_104, $fot(suc(suc(B_79))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_169, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(B_79)))) |
% 0.77/0.98 'E'(f(suc(suc(B_79))), f(suc(suc(suc(B_79))))) | 'LE'(f(B_79), 0) |
% 0.77/0.98 'LE'(f(suc(suc(B_79))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(B_79))), suc(suc(suc(B_79))))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(suc(B_79)))))],
% 0.77/0.98 [refute_0_164, refute_0_168])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_170, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_183)))) |
% 0.77/0.98 'E'(f(suc(suc(X_183))), f(suc(suc(suc(X_183))))) | 'LE'(f(X_183), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_183))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_183))), suc(suc(suc(X_183))))),
% 0.77/0.98 inference(subst, [], [refute_0_169 : [bind(B_79, $fot(X_183))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_171, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_183)))) | 'E'(0, f(suc(suc(X_183)))) |
% 0.77/0.98 'LE'(f(X_183), 0) | 'LE'(f(suc(suc(X_183))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_183))), suc(suc(suc(X_183))))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf('E'(f(suc(suc(X_183))), f(suc(suc(suc(X_183))))))],
% 0.77/0.98 [refute_0_170, refute_0_167])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_172, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_191)))) | 'E'(0, f(suc(suc(X_191)))) |
% 0.77/0.98 'LE'(f(X_191), 0) | 'LE'(f(suc(suc(X_191))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_191))), suc(suc(suc(X_191))))),
% 0.77/0.98 inference(subst, [], [refute_0_171 : [bind(X_183, $fot(X_191))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_173, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_191)))) | 'LE'(f(X_191), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_191))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_191))), suc(suc(suc(X_191))))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_191)))))],
% 0.77/0.98 [refute_0_166, refute_0_172])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_174, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_223)))) | 'LE'(f(X_223), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_223))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_223))), suc(suc(suc(X_223))))),
% 0.77/0.98 inference(subst, [], [refute_0_173 : [bind(X_191, $fot(X_223))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_175, plain,
% 0.77/0.98 (~ 'E'(f(suc(suc(X_204))), f(suc(suc(suc(X_204))))) |
% 0.77/0.98 ~ 'E'(s(0), f(suc(suc(X_204)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_204))), suc(suc(suc(X_204)))) |
% 0.77/0.98 'LE'(f(suc(suc(X_204))), s(0))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_143 : [bind(X_131, $fot(suc(suc(X_204))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_176, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_203)))) | 'E'(s(0), f(suc(suc(X_203)))) |
% 0.77/0.98 'LE'(f(X_203), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_164 : [bind(B_79, $fot(X_203))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_177, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_192)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_192))), suc(suc(suc(X_192)))) |
% 0.77/0.98 'E'(f(suc(suc(X_192))), f(suc(suc(suc(X_192))))) |
% 0.77/0.98 'LE'(f(suc(suc(X_192))), s(0))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [refute_0_147 : [bind(X_104, $fot(suc(suc(X_192))))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_178, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_192)))) | 'LE'(f(X_192), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_192))), s(0)) |
% 0.77/0.98 iLEQ(suc(suc(suc(X_192))), suc(suc(suc(X_192))))),
% 0.77/0.98 inference(subst, [], [refute_0_173 : [bind(X_191, $fot(X_192))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_179, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_192)))) | 'E'(0, f(suc(suc(X_192)))) |
% 0.77/0.98 'E'(f(suc(suc(X_192))), f(suc(suc(suc(X_192))))) | 'LE'(f(X_192), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_192))), s(0))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf(iLEQ(suc(suc(suc(X_192))), suc(suc(suc(X_192)))))],
% 0.77/0.98 [refute_0_178, refute_0_177])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_180, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_203)))) | 'E'(0, f(suc(suc(X_203)))) |
% 0.77/0.98 'E'(f(suc(suc(X_203))), f(suc(suc(suc(X_203))))) | 'LE'(f(X_203), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_203))), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_179 : [bind(X_192, $fot(X_203))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_181, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_203)))) |
% 0.77/0.98 'E'(f(suc(suc(X_203))), f(suc(suc(suc(X_203))))) | 'LE'(f(X_203), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_203))), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_203)))))],
% 0.77/0.98 [refute_0_176, refute_0_180])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_182, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_204)))) |
% 0.77/0.98 'E'(f(suc(suc(X_204))), f(suc(suc(suc(X_204))))) | 'LE'(f(X_204), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_204))), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_181 : [bind(X_203, $fot(X_204))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_183, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_204)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_204))), suc(suc(suc(X_204)))) |
% 0.77/0.98 'E'(0, f(suc(suc(X_204)))) | 'LE'(f(X_204), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_204))), s(0))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf('E'(f(suc(suc(X_204))), f(suc(suc(suc(X_204))))))],
% 0.77/0.98 [refute_0_182, refute_0_175])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_184, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_223)))) |
% 0.77/0.98 ~ iLEQ(suc(suc(suc(X_223))), suc(suc(suc(X_223)))) |
% 0.77/0.98 'E'(0, f(suc(suc(X_223)))) | 'LE'(f(X_223), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_223))), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_183 : [bind(X_204, $fot(X_223))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_185, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_223)))) | 'E'(0, f(suc(suc(X_223)))) |
% 0.77/0.98 'LE'(f(X_223), 0) | 'LE'(f(suc(suc(X_223))), s(0))),
% 0.77/0.98 inference(resolve,
% 0.77/0.98 [$cnf(iLEQ(suc(suc(suc(X_223))), suc(suc(suc(X_223)))))],
% 0.77/0.98 [refute_0_174, refute_0_184])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_186, plain,
% 0.77/0.98 (~ 'E'(s(0), f(suc(suc(X_224)))) | 'E'(0, f(suc(suc(X_224)))) |
% 0.77/0.98 'LE'(f(X_224), 0) | 'LE'(f(suc(suc(X_224))), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_185 : [bind(X_223, $fot(X_224))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_187, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_224)))) | 'LE'(f(X_224), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_224))), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_224)))))],
% 0.77/0.98 [refute_0_165, refute_0_186])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_188, plain,
% 0.77/0.98 ('E'(0, f(suc(suc(X_225)))) | 'LE'(f(X_225), 0) |
% 0.77/0.98 'LE'(f(suc(suc(X_225))), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_187 : [bind(X_224, $fot(X_225))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_189, plain, ('E'(0, f(suc(suc(X_225)))) | 'LE'(f(X_225), 0)),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(suc(suc(X_225))), s(0)))],
% 0.77/0.98 [refute_0_188, refute_0_162])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_190, plain, ('E'(0, f(suc(suc(z)))) | 'LE'(f(z), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_189 : [bind(X_225, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_191, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 0.77/0.98 ~ 'E'(f(z), f(suc(z))) | ~ iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [clause_1397 :
% 0.77/0.98 [bind(A_3, $fot(z)), bind(B_80, $fot(z)),
% 0.77/0.98 bind(B_81, $fot(z)), bind(B_82, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_192, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) | ~ iLEQ(suc(z), suc(z)) |
% 0.77/0.98 'E'(f(z), f(suc(z)))),
% 0.77/0.98 inference(subst, [],
% 0.77/0.98 [clause_1370 :
% 0.77/0.98 [bind(A_3, $fot(z)), bind(B_80, $fot(z)),
% 0.77/0.98 bind(B_81, $fot(z)), bind(B_82, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_193, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 0.77/0.98 ~ 'E'(f(z), f(suc(z))) | iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(subst, [], [clause_418 : [bind(A_3, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_194, plain,
% 0.77/0.98 (~ 'LE'(f(X_168), s(0)) | 'E'(0, f(X_168)) | 'LE'(f(X_168), 0)),
% 0.77/0.98 inference(subst, [], [clause_509 : [bind(B_79, $fot(X_168))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_195, plain,
% 0.77/0.98 (~ 'LE'(f(X_74), s(0)) | 'E'(0, f(X_74)) | 'LE'(f(X_74), 0)),
% 0.77/0.98 inference(subst, [], [clause_509 : [bind(B_79, $fot(X_74))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_196, plain, ('E'(s(0), f(X_74)) | 'LE'(f(X_74), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_59 : [bind(X_73, $fot(X_74))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_197, plain,
% 0.77/0.98 ('E'(0, f(X_74)) | 'E'(s(0), f(X_74)) | 'LE'(f(X_74), 0)),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(X_74), s(0)))],
% 0.77/0.98 [refute_0_196, refute_0_195])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_198, plain,
% 0.77/0.98 ('E'(0, f(X_167)) | 'E'(s(0), f(X_167)) | 'LE'(f(X_167), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_197 : [bind(X_74, $fot(X_167))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_199, plain,
% 0.77/0.98 ('E'(0, f(X_150)) | 'E'(s(0), f(X_150)) | 'LE'(f(X_150), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_197 : [bind(X_74, $fot(X_150))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_200, plain,
% 0.77/0.98 ('E'(0, f(X_105)) | 'E'(s(0), f(X_105)) | 'LE'(f(X_105), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_197 : [bind(X_74, $fot(X_105))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_201, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_105)) | 'E'(f(X_105), f(suc(X_105))) |
% 0.77/0.98 'LE'(f(X_105), s(0)) | iLEQ(suc(X_105), suc(X_105))),
% 0.77/0.98 inference(subst, [], [refute_0_131 : [bind(X_104, $fot(X_105))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_202, plain,
% 0.77/0.98 ('E'(0, f(X_105)) | 'E'(f(X_105), f(suc(X_105))) | 'LE'(f(X_105), 0) |
% 0.77/0.98 'LE'(f(X_105), s(0)) | iLEQ(suc(X_105), suc(X_105))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(X_105)))],
% 0.77/0.98 [refute_0_200, refute_0_201])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_203, plain,
% 0.77/0.98 ('E'(0, f(X_134)) | 'E'(f(X_134), f(suc(X_134))) | 'LE'(f(X_134), 0) |
% 0.77/0.98 'LE'(f(X_134), s(0)) | iLEQ(suc(X_134), suc(X_134))),
% 0.77/0.98 inference(subst, [], [refute_0_202 : [bind(X_105, $fot(X_134))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_204, plain,
% 0.77/0.98 (~ 'E'(f(X_134), f(suc(X_134))) | ~ 'E'(s(0), f(X_134)) |
% 0.77/0.98 'LE'(f(X_134), s(0)) | iLEQ(suc(X_134), suc(X_134))),
% 0.77/0.98 inference(subst, [], [refute_0_127 : [bind(X_133, $fot(X_134))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_205, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_134)) | 'E'(0, f(X_134)) | 'LE'(f(X_134), 0) |
% 0.77/0.98 'LE'(f(X_134), s(0)) | iLEQ(suc(X_134), suc(X_134))),
% 0.77/0.98 inference(resolve, [$cnf('E'(f(X_134), f(suc(X_134))))],
% 0.77/0.98 [refute_0_203, refute_0_204])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_206, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_150)) | 'E'(0, f(X_150)) | 'LE'(f(X_150), 0) |
% 0.77/0.98 'LE'(f(X_150), s(0)) | iLEQ(suc(X_150), suc(X_150))),
% 0.77/0.98 inference(subst, [], [refute_0_205 : [bind(X_134, $fot(X_150))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_207, plain,
% 0.77/0.98 ('E'(0, f(X_150)) | 'LE'(f(X_150), 0) | 'LE'(f(X_150), s(0)) |
% 0.77/0.98 iLEQ(suc(X_150), suc(X_150))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(X_150)))],
% 0.77/0.98 [refute_0_199, refute_0_206])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_208, plain,
% 0.77/0.98 ('E'(0, f(X_166)) | 'LE'(f(X_166), 0) | 'LE'(f(X_166), s(0)) |
% 0.77/0.98 iLEQ(suc(X_166), suc(X_166))),
% 0.77/0.98 inference(subst, [], [refute_0_207 : [bind(X_150, $fot(X_166))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_209, plain,
% 0.77/0.98 (~ 'E'(f(X_161), f(suc(X_161))) | ~ 'E'(s(0), f(X_161)) |
% 0.77/0.98 ~ iLEQ(suc(X_161), suc(X_161)) | 'LE'(f(X_161), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_143 : [bind(X_131, $fot(X_161))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_210, plain,
% 0.77/0.98 ('E'(0, f(X_160)) | 'E'(s(0), f(X_160)) | 'LE'(f(X_160), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_197 : [bind(X_74, $fot(X_160))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_211, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_151)) | ~ iLEQ(suc(X_151), suc(X_151)) |
% 0.77/0.98 'E'(f(X_151), f(suc(X_151))) | 'LE'(f(X_151), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_147 : [bind(X_104, $fot(X_151))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_212, plain,
% 0.77/0.98 ('E'(0, f(X_151)) | 'LE'(f(X_151), 0) | 'LE'(f(X_151), s(0)) |
% 0.77/0.98 iLEQ(suc(X_151), suc(X_151))),
% 0.77/0.98 inference(subst, [], [refute_0_207 : [bind(X_150, $fot(X_151))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_213, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_151)) | 'E'(0, f(X_151)) |
% 0.77/0.98 'E'(f(X_151), f(suc(X_151))) | 'LE'(f(X_151), 0) |
% 0.77/0.98 'LE'(f(X_151), s(0))),
% 0.77/0.98 inference(resolve, [$cnf(iLEQ(suc(X_151), suc(X_151)))],
% 0.77/0.98 [refute_0_212, refute_0_211])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_214, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_160)) | 'E'(0, f(X_160)) |
% 0.77/0.98 'E'(f(X_160), f(suc(X_160))) | 'LE'(f(X_160), 0) |
% 0.77/0.98 'LE'(f(X_160), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_213 : [bind(X_151, $fot(X_160))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_215, plain,
% 0.77/0.98 ('E'(0, f(X_160)) | 'E'(f(X_160), f(suc(X_160))) | 'LE'(f(X_160), 0) |
% 0.77/0.98 'LE'(f(X_160), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(X_160)))],
% 0.77/0.98 [refute_0_210, refute_0_214])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_216, plain,
% 0.77/0.98 ('E'(0, f(X_161)) | 'E'(f(X_161), f(suc(X_161))) | 'LE'(f(X_161), 0) |
% 0.77/0.98 'LE'(f(X_161), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_215 : [bind(X_160, $fot(X_161))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_217, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_161)) | ~ iLEQ(suc(X_161), suc(X_161)) |
% 0.77/0.98 'E'(0, f(X_161)) | 'LE'(f(X_161), 0) | 'LE'(f(X_161), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(f(X_161), f(suc(X_161))))],
% 0.77/0.98 [refute_0_216, refute_0_209])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_218, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_166)) | ~ iLEQ(suc(X_166), suc(X_166)) |
% 0.77/0.98 'E'(0, f(X_166)) | 'LE'(f(X_166), 0) | 'LE'(f(X_166), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_217 : [bind(X_161, $fot(X_166))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_219, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_166)) | 'E'(0, f(X_166)) | 'LE'(f(X_166), 0) |
% 0.77/0.98 'LE'(f(X_166), s(0))),
% 0.77/0.98 inference(resolve, [$cnf(iLEQ(suc(X_166), suc(X_166)))],
% 0.77/0.98 [refute_0_208, refute_0_218])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_220, plain,
% 0.77/0.98 (~ 'E'(s(0), f(X_167)) | 'E'(0, f(X_167)) | 'LE'(f(X_167), 0) |
% 0.77/0.98 'LE'(f(X_167), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_219 : [bind(X_166, $fot(X_167))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_221, plain,
% 0.77/0.98 ('E'(0, f(X_167)) | 'LE'(f(X_167), 0) | 'LE'(f(X_167), s(0))),
% 0.77/0.98 inference(resolve, [$cnf('E'(s(0), f(X_167)))],
% 0.77/0.98 [refute_0_198, refute_0_220])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_222, plain,
% 0.77/0.98 ('E'(0, f(X_168)) | 'LE'(f(X_168), 0) | 'LE'(f(X_168), s(0))),
% 0.77/0.98 inference(subst, [], [refute_0_221 : [bind(X_167, $fot(X_168))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_223, plain, ('E'(0, f(X_168)) | 'LE'(f(X_168), 0)),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(X_168), s(0)))],
% 0.77/0.98 [refute_0_222, refute_0_194])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_224, plain, ('E'(0, f(z)) | 'LE'(f(z), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_223 : [bind(X_168, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_225, plain, ('E'(0, f(z))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_224, clause_709])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_226, plain,
% 0.77/0.98 (~ 'E'(0, f(X_187)) | ~ 'E'(0, f(suc(X_187))) |
% 0.77/0.98 'E'(f(X_187), f(suc(X_187))) | iLEQ(suc(X_187), suc(X_187))),
% 0.77/0.98 inference(subst, [], [clause_332 : [bind(A_3, $fot(X_187))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_227, plain, ('E'(0, f(suc(X_187))) | 'LE'(f(X_187), 0)),
% 0.77/0.98 inference(subst, [], [refute_0_160 : [bind(X_186, $fot(X_187))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_228, plain,
% 0.77/0.98 (~ 'E'(0, f(X_187)) | 'E'(f(X_187), f(suc(X_187))) |
% 0.77/0.98 'LE'(f(X_187), 0) | iLEQ(suc(X_187), suc(X_187))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(suc(X_187))))],
% 0.77/0.98 [refute_0_227, refute_0_226])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_229, plain,
% 0.77/0.98 (~ 'E'(0, f(z)) | 'E'(f(z), f(suc(z))) | 'LE'(f(z), 0) |
% 0.77/0.98 iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(subst, [], [refute_0_228 : [bind(X_187, $fot(z))]])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_230, plain,
% 0.77/0.98 ('E'(f(z), f(suc(z))) | 'LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(z)))],
% 0.77/0.98 [refute_0_225, refute_0_229])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_231, plain, ('E'(f(z), f(suc(z))) | iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_230, clause_709])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_232, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 0.77/0.98 iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(f(z), f(suc(z))))],
% 0.77/0.98 [refute_0_231, refute_0_193])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_233, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) |
% 0.77/0.98 iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(z)))],
% 0.77/0.98 [refute_0_225, refute_0_232])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_234, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(z))) | 'LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(suc(suc(z)))))],
% 0.77/0.98 [refute_0_190, refute_0_233])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_235, plain, (~ 'E'(0, f(suc(z))) | iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_234, clause_709])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_236, plain, ('LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 0.77/0.98 [refute_0_161, refute_0_235])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_237, plain, (iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_236, clause_709])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_238, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) | 'E'(f(z), f(suc(z)))),
% 0.77/0.98 inference(resolve, [$cnf(iLEQ(suc(z), suc(z)))],
% 0.77/0.98 [refute_0_237, refute_0_192])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_239, plain, (~ 'E'(0, f(suc(z))) | 'E'(f(z), f(suc(z)))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(z)))],
% 0.77/0.98 [refute_0_225, refute_0_238])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_240, plain, ('E'(f(z), f(suc(z))) | 'LE'(f(z), 0)),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 0.77/0.98 [refute_0_161, refute_0_239])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_241, plain, ('E'(f(z), f(suc(z)))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_240, clause_709])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_242, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 0.77/0.98 ~ iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(f(z), f(suc(z))))],
% 0.77/0.98 [refute_0_241, refute_0_191])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_243, plain,
% 0.77/0.98 (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) |
% 0.77/0.98 ~ iLEQ(suc(z), suc(z))),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(z)))],
% 0.77/0.98 [refute_0_225, refute_0_242])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_244, plain, (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z)))),
% 0.77/0.98 inference(resolve, [$cnf(iLEQ(suc(z), suc(z)))],
% 0.77/0.98 [refute_0_237, refute_0_243])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_245, plain, (~ 'E'(0, f(suc(z))) | 'LE'(f(z), 0)),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(suc(suc(z)))))],
% 0.77/0.98 [refute_0_190, refute_0_244])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_246, plain, (~ 'E'(0, f(suc(z)))),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_245, clause_709])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_247, plain, ('LE'(f(z), 0)),
% 0.77/0.98 inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 0.77/0.98 [refute_0_161, refute_0_246])).
% 0.77/0.98
% 0.77/0.98 cnf(refute_0_248, plain, ($false),
% 0.77/0.98 inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_247, clause_709])).
% 0.77/0.98 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.77/0.98
%------------------------------------------------------------------------------