Metis---2.4.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SYO681-1 : TPTP v8.1.0. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n011.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:51 EDT 2022

% Result   : Unsatisfiable 3.72s 3.89s
% Output   : CNFRefutation 3.72s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.11  % Problem  : SYO681-1 : TPTP v8.1.0. Released v7.3.0.
% 0.02/0.12  % Command  : metis --show proof --show saturation %s
% 0.11/0.33  % Computer : n011.cluster.edu
% 0.11/0.33  % Model    : x86_64 x86_64
% 0.11/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33  % Memory   : 8042.1875MB
% 0.11/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33  % CPULimit : 300
% 0.11/0.33  % WCLimit  : 600
% 0.11/0.33  % DateTime : Sat Jul  9 01:03:55 EDT 2022
% 0.11/0.33  % CPUTime  : 
% 0.11/0.33  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 3.72/3.89  % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.72/3.89  
% 3.72/3.89  % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.72/3.90  cnf(clause_658, axiom,
% 3.72/3.90      (~ 'LE'(f(B_23), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(B_23)) |
% 3.72/3.90       'LE'(f(B_23), s(s(s(0)))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_556, axiom, ('LE'(f(A), s(s(s(s(0))))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_300, axiom,
% 3.72/3.90      (~ 'LE'(f(B_41), s(s(s(0)))) | 'E'(s(s(0)), f(B_41)) |
% 3.72/3.90       'LE'(f(B_41), s(s(0))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_415, axiom,
% 3.72/3.90      (~ 'E'(s(s(0)), f(suc(suc(A_2)))) | ~ 'E'(s(s(0)), f(suc(A_2))) |
% 3.72/3.90       ~ 'E'(f(A_2), f(suc(A_2))) | ~ 'E'(s(s(0)), f(A_2)) |
% 3.72/3.90       iLEQ(suc(A_2), suc(A_2)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_614, axiom,
% 3.72/3.90      (~ 'E'(0, f(suc(B_61))) | ~ iLEQ(suc(B_61), suc(B_62)) |
% 3.72/3.90       ~ iLEQ(suc(A_4), suc(B_61)) | ~ 'E'(0, f(suc(B_62))) |
% 3.72/3.90       ~ 'E'(0, f(B_61)) | ~ 'E'(0, f(suc(A_4))) | ~ 'E'(0, f(B_62)) |
% 3.72/3.90       ~ 'E'(0, f(A_4)) | 'E'(f(A_4), f(suc(A_4))) |
% 3.72/3.90       'E'(f(B_61), f(suc(B_61))) | 'E'(f(B_62), f(suc(B_62))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_607, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(suc(B_41))), s(s(s(0)))) |
% 3.72/3.90       'E'(s(s(0)), f(suc(suc(B_41)))) | 'LE'(f(B_41), s(s(0))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_486, axiom,
% 3.72/3.90      (~ iLEQ(suc(B_24), suc(B_25)) | ~ 'E'(s(s(s(0))), f(B_25)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(B_24)) | ~ iLEQ(suc(A_1), suc(B_24)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(A_1)) | ~ 'E'(s(s(s(0))), f(suc(B_24))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(B_25))) | ~ 'E'(s(s(s(0))), f(suc(A_1))) |
% 3.72/3.90       'E'(f(A_1), f(suc(A_1))) | 'E'(f(B_24), f(suc(B_24))) |
% 3.72/3.90       'E'(f(B_25), f(suc(B_25))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_687, axiom,
% 3.72/3.90      (~ iLEQ(suc(B_54), suc(B_55)) | ~ 'E'(s(0), f(suc(A_3))) |
% 3.72/3.90       ~ iLEQ(suc(A_3), suc(B_54)) | ~ 'E'(s(0), f(suc(B_55))) |
% 3.72/3.90       ~ 'E'(s(0), f(A_3)) | ~ 'E'(s(0), f(B_55)) |
% 3.72/3.90       ~ 'E'(s(0), f(suc(B_54))) | ~ 'E'(s(0), f(B_54)) |
% 3.72/3.90       'E'(f(A_3), f(suc(A_3))) | 'E'(f(B_54), f(suc(B_54))) |
% 3.72/3.90       'E'(f(B_55), f(suc(B_55))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_528, axiom,
% 3.72/3.90      (~ 'E'(s(s(0)), f(suc(B_42))) | ~ 'E'(f(B_43), f(suc(B_43))) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(B_42)) | ~ iLEQ(suc(B_42), suc(B_43)) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(suc(suc(B_42)))) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(suc(suc(B_43)))) | ~ 'E'(s(s(0)), f(suc(A_2))) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(suc(B_43))) | ~ iLEQ(suc(A_2), suc(B_42)) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(B_43)) | ~ 'E'(s(s(0)), f(suc(suc(A_2)))) |
% 3.72/3.90       ~ 'E'(f(B_42), f(suc(B_42))) | ~ 'E'(s(s(0)), f(A_2)) |
% 3.72/3.90       ~ 'E'(f(A_2), f(suc(A_2))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_359, axiom, (~ 'LE'(f(z), 0))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_497, axiom,
% 3.72/3.90      (~ 'LE'(f(B_60), s(0)) | 'E'(0, f(B_60)) | 'LE'(f(B_60), 0))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_463, axiom,
% 3.72/3.90      (~ 'E'(s(s(0)), f(suc(B_42))) | ~ 'E'(s(s(0)), f(B_42)) |
% 3.72/3.90       ~ iLEQ(suc(B_42), suc(B_43)) | ~ 'E'(s(s(0)), f(suc(A_2))) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(suc(B_43))) | ~ iLEQ(suc(A_2), suc(B_42)) |
% 3.72/3.90       ~ 'E'(s(s(0)), f(B_43)) | ~ 'E'(s(s(0)), f(A_2)) |
% 3.72/3.90       'E'(f(A_2), f(suc(A_2))) | 'E'(f(B_42), f(suc(B_42))) |
% 3.72/3.90       'E'(f(B_43), f(suc(B_43))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_95, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(B_53)), s(s(0))) | 'E'(s(0), f(suc(B_53))) |
% 3.72/3.90       'LE'(f(B_53), s(0)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_125, axiom,
% 3.72/3.90      (~ 'E'(s(0), f(suc(suc(A_3)))) | ~ 'E'(s(0), f(suc(A_3))) |
% 3.72/3.90       ~ 'E'(f(A_3), f(suc(A_3))) | ~ 'E'(s(0), f(A_3)) |
% 3.72/3.90       iLEQ(suc(A_3), suc(A_3)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_61, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(suc(B_60))), s(0)) | 'E'(0, f(suc(suc(B_60)))) |
% 3.72/3.90       'LE'(f(B_60), 0))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_713, axiom,
% 3.72/3.90      (~ 'E'(0, f(A_4)) | ~ 'E'(0, f(suc(A_4))) | 'E'(f(A_4), f(suc(A_4))) |
% 3.72/3.90       iLEQ(suc(A_4), suc(A_4)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_560, axiom,
% 3.72/3.90      (~ 'E'(0, f(suc(suc(A_4)))) | ~ 'E'(0, f(suc(A_4))) |
% 3.72/3.90       ~ 'E'(f(A_4), f(suc(A_4))) | ~ 'E'(0, f(A_4)) |
% 3.72/3.90       iLEQ(suc(A_4), suc(A_4)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_103, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(suc(B_23))), s(s(s(s(0))))) |
% 3.72/3.90       'E'(s(s(s(0))), f(suc(suc(B_23)))) | 'LE'(f(B_23), s(s(s(0)))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_563, axiom,
% 3.72/3.90      (~ 'E'(s(0), f(A_3)) | ~ 'E'(s(0), f(suc(A_3))) |
% 3.72/3.90       'E'(f(A_3), f(suc(A_3))) | iLEQ(suc(A_3), suc(A_3)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_283, axiom,
% 3.72/3.90      (~ 'E'(s(s(s(0))), f(A_1)) | ~ 'E'(s(s(s(0))), f(suc(A_1))) |
% 3.72/3.90       'E'(f(A_1), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_457, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(B_41)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(B_41))) |
% 3.72/3.90       'LE'(f(B_41), s(s(0))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_663, axiom,
% 3.72/3.90      (~ 'E'(s(s(s(0))), f(suc(suc(A_1)))) | ~ 'E'(s(s(s(0))), f(suc(A_1))) |
% 3.72/3.90       ~ 'E'(f(A_1), f(suc(A_1))) | ~ 'E'(s(s(s(0))), f(A_1)) |
% 3.72/3.90       iLEQ(suc(A_1), suc(A_1)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_131, axiom,
% 3.72/3.90      (~ iLEQ(suc(B_24), suc(B_25)) | ~ 'E'(s(s(s(0))), f(suc(suc(B_24)))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(B_25)) | ~ 'E'(f(B_24), f(suc(B_24))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(B_24)) | ~ iLEQ(suc(A_1), suc(B_24)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(A_1)) | ~ 'E'(s(s(s(0))), f(suc(suc(A_1)))) |
% 3.72/3.90       ~ 'E'(f(B_25), f(suc(B_25))) | ~ 'E'(f(A_1), f(suc(A_1))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(B_24))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(suc(B_25)))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(B_25))) | ~ 'E'(s(s(s(0))), f(suc(A_1))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_41, axiom,
% 3.72/3.90      (~ iLEQ(suc(B_54), suc(B_55)) | ~ 'E'(s(0), f(suc(A_3))) |
% 3.72/3.90       ~ 'E'(f(B_55), f(suc(B_55))) | ~ iLEQ(suc(A_3), suc(B_54)) |
% 3.72/3.90       ~ 'E'(s(0), f(suc(B_55))) | ~ 'E'(s(0), f(suc(suc(B_54)))) |
% 3.72/3.90       ~ 'E'(f(B_54), f(suc(B_54))) | ~ 'E'(f(A_3), f(suc(A_3))) |
% 3.72/3.90       ~ 'E'(s(0), f(A_3)) | ~ 'E'(s(0), f(B_55)) |
% 3.72/3.90       ~ 'E'(s(0), f(suc(suc(B_55)))) | ~ 'E'(s(0), f(suc(B_54))) |
% 3.72/3.90       ~ 'E'(s(0), f(suc(suc(A_3)))) | ~ 'E'(s(0), f(B_54)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_44, axiom,
% 3.72/3.90      (~ 'LE'(f(B_53), s(s(0))) | 'E'(s(0), f(B_53)) | 'LE'(f(B_53), s(0)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_550, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(B_23)), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(suc(B_23))) |
% 3.72/3.90       'LE'(f(B_23), s(s(s(0)))))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_383, axiom,
% 3.72/3.90      (~ 'E'(s(s(0)), f(A_2)) | ~ 'E'(s(s(0)), f(suc(A_2))) |
% 3.72/3.90       'E'(f(A_2), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_363, axiom,
% 3.72/3.90      (~ 'E'(0, f(suc(B_61))) | ~ iLEQ(suc(B_61), suc(B_62)) |
% 3.72/3.90       ~ 'E'(f(A_4), f(suc(A_4))) | ~ iLEQ(suc(A_4), suc(B_61)) |
% 3.72/3.90       ~ 'E'(0, f(suc(B_62))) | ~ 'E'(0, f(suc(suc(A_4)))) |
% 3.72/3.90       ~ 'E'(f(B_62), f(suc(B_62))) | ~ 'E'(0, f(B_61)) |
% 3.72/3.90       ~ 'E'(0, f(suc(suc(B_62)))) | ~ 'E'(0, f(suc(A_4))) |
% 3.72/3.90       ~ 'E'(0, f(B_62)) | ~ 'E'(0, f(suc(suc(B_61)))) |
% 3.72/3.90       ~ 'E'(f(B_61), f(suc(B_61))) | ~ 'E'(0, f(A_4)))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_595, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(B_60)), s(0)) | 'E'(0, f(suc(B_60))) |
% 3.72/3.90       'LE'(f(B_60), 0))).
% 3.72/3.90  
% 3.72/3.90  cnf(clause_508, axiom,
% 3.72/3.90      (~ 'LE'(f(suc(suc(B_53))), s(s(0))) | 'E'(s(0), f(suc(suc(B_53)))) |
% 3.72/3.90       'LE'(f(B_53), s(0)))).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_0, plain,
% 3.72/3.90      (~ 'LE'(f(suc(X_484)), s(0)) | 'E'(0, f(suc(X_484))) |
% 3.72/3.90       'LE'(f(X_484), 0)),
% 3.72/3.90      inference(subst, [], [clause_595 : [bind(B_60, $fot(X_484))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_1, plain,
% 3.72/3.90      (~ 'LE'(f(X_184), s(s(0))) | 'E'(s(0), f(X_184)) |
% 3.72/3.90       'LE'(f(X_184), s(0))),
% 3.72/3.90      inference(subst, [], [clause_44 : [bind(B_53, $fot(X_184))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_2, plain,
% 3.72/3.90      (~ 'LE'(f(X_179), s(s(0))) | 'E'(s(0), f(X_179)) |
% 3.72/3.90       'LE'(f(X_179), s(0))),
% 3.72/3.90      inference(subst, [], [clause_44 : [bind(B_53, $fot(X_179))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_3, plain,
% 3.72/3.90      (~ 'LE'(f(X_91), s(s(0))) | 'E'(s(0), f(X_91)) | 'LE'(f(X_91), s(0))),
% 3.72/3.90      inference(subst, [], [clause_44 : [bind(B_53, $fot(X_91))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_4, plain,
% 3.72/3.90      (~ 'LE'(f(X_90), s(s(s(0)))) | 'E'(s(s(0)), f(X_90)) |
% 3.72/3.90       'LE'(f(X_90), s(s(0)))),
% 3.72/3.90      inference(subst, [], [clause_300 : [bind(B_41, $fot(X_90))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_5, plain,
% 3.72/3.90      (~ 'LE'(f(X_85), s(s(s(0)))) | 'E'(s(s(0)), f(X_85)) |
% 3.72/3.90       'LE'(f(X_85), s(s(0)))),
% 3.72/3.90      inference(subst, [], [clause_300 : [bind(B_41, $fot(X_85))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_6, plain,
% 3.72/3.90      (~ 'LE'(f(X_46), s(s(s(0)))) | 'E'(s(s(0)), f(X_46)) |
% 3.72/3.90       'LE'(f(X_46), s(s(0)))),
% 3.72/3.90      inference(subst, [], [clause_300 : [bind(B_41, $fot(X_46))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_7, plain, ('LE'(f(B_23), s(s(s(s(0)))))),
% 3.72/3.90      inference(subst, [], [clause_556 : [bind(A, $fot(B_23))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_8, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(B_23)) | 'LE'(f(B_23), s(s(s(0))))),
% 3.72/3.90      inference(resolve, [$cnf('LE'(f(B_23), s(s(s(s(0))))))],
% 3.72/3.90                [refute_0_7, clause_658])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_9, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(X_8)) | 'LE'(f(X_8), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_8 : [bind(B_23, $fot(X_8))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_10, plain,
% 3.72/3.90      (~ 'LE'(f(X_8), s(s(s(0)))) | 'E'(s(s(0)), f(X_8)) |
% 3.72/3.90       'LE'(f(X_8), s(s(0)))),
% 3.72/3.90      inference(subst, [], [clause_300 : [bind(B_41, $fot(X_8))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_11, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_8)) | 'E'(s(s(s(0))), f(X_8)) |
% 3.72/3.90       'LE'(f(X_8), s(s(0)))),
% 3.72/3.90      inference(resolve, [$cnf('LE'(f(X_8), s(s(s(0)))))],
% 3.72/3.90                [refute_0_9, refute_0_10])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_12, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_27)) | 'E'(s(s(s(0))), f(X_27)) |
% 3.72/3.90       'LE'(f(X_27), s(s(0)))),
% 3.72/3.90      inference(subst, [], [refute_0_11 : [bind(X_8, $fot(X_27))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_13, plain, ('LE'(f(suc(B_23)), s(s(s(s(0)))))),
% 3.72/3.90      inference(subst, [], [clause_556 : [bind(A, $fot(suc(B_23)))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_14, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(B_23))) | 'LE'(f(B_23), s(s(s(0))))),
% 3.72/3.90      inference(resolve, [$cnf('LE'(f(suc(B_23)), s(s(s(s(0))))))],
% 3.72/3.90                [refute_0_13, clause_550])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_15, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(X_22))) | 'LE'(f(X_22), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_14 : [bind(B_23, $fot(X_22))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_16, plain,
% 3.72/3.90      (~ 'E'(s(s(s(0))), f(X_22)) | ~ 'E'(s(s(s(0))), f(suc(X_22))) |
% 3.72/3.90       'E'(f(X_22), f(suc(X_22))) | iLEQ(suc(X_22), suc(X_22))),
% 3.72/3.90      inference(subst, [], [clause_283 : [bind(A_1, $fot(X_22))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_17, plain,
% 3.72/3.90      (~ 'E'(s(s(s(0))), f(X_22)) | 'E'(f(X_22), f(suc(X_22))) |
% 3.72/3.90       'LE'(f(X_22), s(s(s(0)))) | iLEQ(suc(X_22), suc(X_22))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_22))))],
% 3.72/3.90                [refute_0_15, refute_0_16])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_18, plain,
% 3.72/3.90      (~ 'E'(s(s(s(0))), f(X_27)) | 'E'(f(X_27), f(suc(X_27))) |
% 3.72/3.90       'LE'(f(X_27), s(s(s(0)))) | iLEQ(suc(X_27), suc(X_27))),
% 3.72/3.90      inference(subst, [], [refute_0_17 : [bind(X_22, $fot(X_27))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_19, plain,
% 3.72/3.90      ('E'(f(X_27), f(suc(X_27))) | 'E'(s(s(0)), f(X_27)) |
% 3.72/3.90       'LE'(f(X_27), s(s(0))) | 'LE'(f(X_27), s(s(s(0)))) |
% 3.72/3.90       iLEQ(suc(X_27), suc(X_27))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_27)))],
% 3.72/3.90                [refute_0_12, refute_0_18])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_20, plain,
% 3.72/3.90      ('E'(f(X_46), f(suc(X_46))) | 'E'(s(s(0)), f(X_46)) |
% 3.72/3.90       'LE'(f(X_46), s(s(0))) | 'LE'(f(X_46), s(s(s(0)))) |
% 3.72/3.90       iLEQ(suc(X_46), suc(X_46))),
% 3.72/3.90      inference(subst, [], [refute_0_19 : [bind(X_27, $fot(X_46))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_21, plain,
% 3.72/3.90      ('E'(f(X_46), f(suc(X_46))) | 'E'(s(s(0)), f(X_46)) |
% 3.72/3.90       'LE'(f(X_46), s(s(0))) | iLEQ(suc(X_46), suc(X_46))),
% 3.72/3.90      inference(resolve, [$cnf('LE'(f(X_46), s(s(s(0)))))],
% 3.72/3.90                [refute_0_20, refute_0_6])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_22, plain,
% 3.72/3.90      ('E'(f(X_84), f(suc(X_84))) | 'E'(s(s(0)), f(X_84)) |
% 3.72/3.90       'LE'(f(X_84), s(s(0))) | iLEQ(suc(X_84), suc(X_84))),
% 3.72/3.90      inference(subst, [], [refute_0_21 : [bind(X_46, $fot(X_84))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_23, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_54)) | 'E'(s(s(s(0))), f(X_54)) |
% 3.72/3.90       'LE'(f(X_54), s(s(0)))),
% 3.72/3.90      inference(subst, [], [refute_0_11 : [bind(X_8, $fot(X_54))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_24, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(X_53))) | 'LE'(f(X_53), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_14 : [bind(B_23, $fot(X_53))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_25, plain, ('LE'(f(suc(suc(B_23))), s(s(s(s(0)))))),
% 3.72/3.90      inference(subst, [], [clause_556 : [bind(A, $fot(suc(suc(B_23))))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_26, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(suc(B_23)))) | 'LE'(f(B_23), s(s(s(0))))),
% 3.72/3.90      inference(resolve, [$cnf('LE'(f(suc(suc(B_23))), s(s(s(s(0))))))],
% 3.72/3.90                [refute_0_25, clause_103])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_27, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(suc(X_36)))) | 'LE'(f(X_36), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_26 : [bind(B_23, $fot(X_36))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_28, plain,
% 3.72/3.90      (~ 'E'(f(X_36), f(suc(X_36))) | ~ 'E'(s(s(s(0))), f(X_36)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(X_36))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(suc(X_36)))) | iLEQ(suc(X_36), suc(X_36))),
% 3.72/3.90      inference(subst, [], [clause_663 : [bind(A_1, $fot(X_36))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_29, plain,
% 3.72/3.90      (~ 'E'(f(X_36), f(suc(X_36))) | ~ 'E'(s(s(s(0))), f(X_36)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(X_36))) | 'LE'(f(X_36), s(s(s(0)))) |
% 3.72/3.90       iLEQ(suc(X_36), suc(X_36))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_36)))))],
% 3.72/3.90                [refute_0_27, refute_0_28])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_30, plain,
% 3.72/3.90      (~ 'E'(f(X_53), f(suc(X_53))) | ~ 'E'(s(s(s(0))), f(X_53)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(X_53))) | 'LE'(f(X_53), s(s(s(0)))) |
% 3.72/3.90       iLEQ(suc(X_53), suc(X_53))),
% 3.72/3.90      inference(subst, [], [refute_0_29 : [bind(X_36, $fot(X_53))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_31, plain,
% 3.72/3.90      (~ 'E'(f(X_53), f(suc(X_53))) | ~ 'E'(s(s(s(0))), f(X_53)) |
% 3.72/3.90       'LE'(f(X_53), s(s(s(0)))) | iLEQ(suc(X_53), suc(X_53))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_53))))],
% 3.72/3.90                [refute_0_24, refute_0_30])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_32, plain,
% 3.72/3.90      (~ 'E'(f(X_54), f(suc(X_54))) | ~ 'E'(s(s(s(0))), f(X_54)) |
% 3.72/3.90       'LE'(f(X_54), s(s(s(0)))) | iLEQ(suc(X_54), suc(X_54))),
% 3.72/3.90      inference(subst, [], [refute_0_31 : [bind(X_53, $fot(X_54))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_33, plain,
% 3.72/3.90      (~ 'E'(f(X_54), f(suc(X_54))) | 'E'(s(s(0)), f(X_54)) |
% 3.72/3.90       'LE'(f(X_54), s(s(0))) | 'LE'(f(X_54), s(s(s(0)))) |
% 3.72/3.90       iLEQ(suc(X_54), suc(X_54))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_54)))],
% 3.72/3.90                [refute_0_23, refute_0_32])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_34, plain,
% 3.72/3.90      (~ 'E'(f(X_84), f(suc(X_84))) | 'E'(s(s(0)), f(X_84)) |
% 3.72/3.90       'LE'(f(X_84), s(s(0))) | 'LE'(f(X_84), s(s(s(0)))) |
% 3.72/3.90       iLEQ(suc(X_84), suc(X_84))),
% 3.72/3.90      inference(subst, [], [refute_0_33 : [bind(X_54, $fot(X_84))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_35, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_84)) | 'LE'(f(X_84), s(s(0))) |
% 3.72/3.90       'LE'(f(X_84), s(s(s(0)))) | iLEQ(suc(X_84), suc(X_84))),
% 3.72/3.90      inference(resolve, [$cnf('E'(f(X_84), f(suc(X_84))))],
% 3.72/3.90                [refute_0_22, refute_0_34])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_36, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_85)) | 'LE'(f(X_85), s(s(0))) |
% 3.72/3.90       'LE'(f(X_85), s(s(s(0)))) | iLEQ(suc(X_85), suc(X_85))),
% 3.72/3.90      inference(subst, [], [refute_0_35 : [bind(X_84, $fot(X_85))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_37, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_85)) | 'LE'(f(X_85), s(s(0))) |
% 3.72/3.90       iLEQ(suc(X_85), suc(X_85))),
% 3.72/3.90      inference(resolve, [$cnf('LE'(f(X_85), s(s(s(0)))))],
% 3.72/3.90                [refute_0_36, refute_0_5])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_38, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_89)) | 'LE'(f(X_89), s(s(0))) |
% 3.72/3.90       iLEQ(suc(X_89), suc(X_89))),
% 3.72/3.90      inference(subst, [], [refute_0_37 : [bind(X_85, $fot(X_89))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_39, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_50)) | 'E'(s(s(s(0))), f(X_50)) |
% 3.72/3.90       'LE'(f(X_50), s(s(0)))),
% 3.72/3.90      inference(subst, [], [refute_0_11 : [bind(X_8, $fot(X_50))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_40, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(X_49))) | 'LE'(f(X_49), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_14 : [bind(B_23, $fot(X_49))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_41, plain,
% 3.72/3.90      ('E'(s(s(s(0))), f(suc(suc(X_37)))) | 'LE'(f(X_37), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_26 : [bind(B_23, $fot(X_37))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_42, plain,
% 3.72/3.90      (~ 'E'(f(X_37), f(suc(X_37))) | ~ 'E'(s(s(s(0))), f(X_37)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(X_37))) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(suc(X_37)))) | ~ iLEQ(suc(X_37), suc(X_37))),
% 3.72/3.90      inference(subst, [],
% 3.72/3.90                [clause_131 :
% 3.72/3.90                 [bind(A_1, $fot(X_37)), bind(B_24, $fot(X_37)),
% 3.72/3.90                  bind(B_25, $fot(X_37))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_43, plain,
% 3.72/3.90      (~ 'E'(f(X_37), f(suc(X_37))) | ~ 'E'(s(s(s(0))), f(X_37)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(X_37))) | ~ iLEQ(suc(X_37), suc(X_37)) |
% 3.72/3.90       'LE'(f(X_37), s(s(s(0))))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_37)))))],
% 3.72/3.90                [refute_0_41, refute_0_42])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_44, plain,
% 3.72/3.90      (~ 'E'(f(X_49), f(suc(X_49))) | ~ 'E'(s(s(s(0))), f(X_49)) |
% 3.72/3.90       ~ 'E'(s(s(s(0))), f(suc(X_49))) | ~ iLEQ(suc(X_49), suc(X_49)) |
% 3.72/3.90       'LE'(f(X_49), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_43 : [bind(X_37, $fot(X_49))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_45, plain,
% 3.72/3.90      (~ 'E'(f(X_49), f(suc(X_49))) | ~ 'E'(s(s(s(0))), f(X_49)) |
% 3.72/3.90       ~ iLEQ(suc(X_49), suc(X_49)) | 'LE'(f(X_49), s(s(s(0))))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_49))))],
% 3.72/3.90                [refute_0_40, refute_0_44])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_46, plain,
% 3.72/3.90      (~ 'E'(f(X_50), f(suc(X_50))) | ~ 'E'(s(s(s(0))), f(X_50)) |
% 3.72/3.90       ~ iLEQ(suc(X_50), suc(X_50)) | 'LE'(f(X_50), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_45 : [bind(X_49, $fot(X_50))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_47, plain,
% 3.72/3.90      (~ 'E'(f(X_50), f(suc(X_50))) | ~ iLEQ(suc(X_50), suc(X_50)) |
% 3.72/3.90       'E'(s(s(0)), f(X_50)) | 'LE'(f(X_50), s(s(0))) |
% 3.72/3.90       'LE'(f(X_50), s(s(s(0))))),
% 3.72/3.90      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_50)))],
% 3.72/3.90                [refute_0_39, refute_0_46])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_48, plain,
% 3.72/3.90      (~ 'E'(f(X_87), f(suc(X_87))) | ~ iLEQ(suc(X_87), suc(X_87)) |
% 3.72/3.90       'E'(s(s(0)), f(X_87)) | 'LE'(f(X_87), s(s(0))) |
% 3.72/3.90       'LE'(f(X_87), s(s(s(0))))),
% 3.72/3.90      inference(subst, [], [refute_0_47 : [bind(X_50, $fot(X_87))]])).
% 3.72/3.90  
% 3.72/3.90  cnf(refute_0_49, plain,
% 3.72/3.90      ('E'(s(s(0)), f(X_24)) | 'E'(s(s(s(0))), f(X_24)) |
% 3.72/3.90       'LE'(f(X_24), s(s(0)))),
% 3.72/3.90      inference(subst, [], [refute_0_11 : [bind(X_8, $fot(X_24))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_50, plain,
% 3.72/3.91      ('E'(s(s(s(0))), f(suc(X_23))) | 'LE'(f(X_23), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_14 : [bind(B_23, $fot(X_23))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_51, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(X_23)) | ~ 'E'(s(s(s(0))), f(suc(X_23))) |
% 3.72/3.91       ~ iLEQ(suc(X_23), suc(X_23)) | 'E'(f(X_23), f(suc(X_23)))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [clause_486 :
% 3.72/3.91                 [bind(A_1, $fot(X_23)), bind(B_24, $fot(X_23)),
% 3.72/3.91                  bind(B_25, $fot(X_23))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_52, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(X_23)) | ~ iLEQ(suc(X_23), suc(X_23)) |
% 3.72/3.91       'E'(f(X_23), f(suc(X_23))) | 'LE'(f(X_23), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_23))))],
% 3.72/3.91                [refute_0_50, refute_0_51])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_53, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(X_24)) | ~ iLEQ(suc(X_24), suc(X_24)) |
% 3.72/3.91       'E'(f(X_24), f(suc(X_24))) | 'LE'(f(X_24), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_52 : [bind(X_23, $fot(X_24))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_54, plain,
% 3.72/3.91      (~ iLEQ(suc(X_24), suc(X_24)) | 'E'(f(X_24), f(suc(X_24))) |
% 3.72/3.91       'E'(s(s(0)), f(X_24)) | 'LE'(f(X_24), s(s(0))) |
% 3.72/3.91       'LE'(f(X_24), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_24)))],
% 3.72/3.91                [refute_0_49, refute_0_53])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_55, plain,
% 3.72/3.91      (~ iLEQ(suc(X_85), suc(X_85)) | 'E'(f(X_85), f(suc(X_85))) |
% 3.72/3.91       'E'(s(s(0)), f(X_85)) | 'LE'(f(X_85), s(s(0))) |
% 3.72/3.91       'LE'(f(X_85), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_54 : [bind(X_24, $fot(X_85))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_56, plain,
% 3.72/3.91      ('E'(f(X_85), f(suc(X_85))) | 'E'(s(s(0)), f(X_85)) |
% 3.72/3.91       'LE'(f(X_85), s(s(0))) | 'LE'(f(X_85), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf(iLEQ(suc(X_85), suc(X_85)))],
% 3.72/3.91                [refute_0_36, refute_0_55])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_57, plain,
% 3.72/3.91      ('E'(f(X_87), f(suc(X_87))) | 'E'(s(s(0)), f(X_87)) |
% 3.72/3.91       'LE'(f(X_87), s(s(0))) | 'LE'(f(X_87), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_56 : [bind(X_85, $fot(X_87))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_58, plain,
% 3.72/3.91      (~ iLEQ(suc(X_87), suc(X_87)) | 'E'(s(s(0)), f(X_87)) |
% 3.72/3.91       'LE'(f(X_87), s(s(0))) | 'LE'(f(X_87), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(f(X_87), f(suc(X_87))))],
% 3.72/3.91                [refute_0_57, refute_0_48])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_59, plain,
% 3.72/3.91      (~ iLEQ(suc(X_89), suc(X_89)) | 'E'(s(s(0)), f(X_89)) |
% 3.72/3.91       'LE'(f(X_89), s(s(0))) | 'LE'(f(X_89), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_58 : [bind(X_87, $fot(X_89))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_60, plain,
% 3.72/3.91      ('E'(s(s(0)), f(X_89)) | 'LE'(f(X_89), s(s(0))) |
% 3.72/3.91       'LE'(f(X_89), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf(iLEQ(suc(X_89), suc(X_89)))],
% 3.72/3.91                [refute_0_38, refute_0_59])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_61, plain,
% 3.72/3.91      ('E'(s(s(0)), f(X_90)) | 'LE'(f(X_90), s(s(0))) |
% 3.72/3.91       'LE'(f(X_90), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_60 : [bind(X_89, $fot(X_90))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_62, plain, ('E'(s(s(0)), f(X_90)) | 'LE'(f(X_90), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(X_90), s(s(s(0)))))],
% 3.72/3.91                [refute_0_61, refute_0_4])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_63, plain, ('E'(s(s(0)), f(X_91)) | 'LE'(f(X_91), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_62 : [bind(X_90, $fot(X_91))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_64, plain,
% 3.72/3.91      ('E'(s(0), f(X_91)) | 'E'(s(s(0)), f(X_91)) | 'LE'(f(X_91), s(0))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(X_91), s(s(0))))],
% 3.72/3.91                [refute_0_63, refute_0_3])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_65, plain,
% 3.72/3.91      ('E'(s(0), f(X_178)) | 'E'(s(s(0)), f(X_178)) | 'LE'(f(X_178), s(0))),
% 3.72/3.91      inference(subst, [], [refute_0_64 : [bind(X_91, $fot(X_178))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_66, plain,
% 3.72/3.91      (~ 'LE'(f(X_129), s(s(0))) | 'E'(s(0), f(X_129)) |
% 3.72/3.91       'LE'(f(X_129), s(0))),
% 3.72/3.91      inference(subst, [], [clause_44 : [bind(B_53, $fot(X_129))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_67, plain,
% 3.72/3.91      ('E'(s(0), f(X_124)) | 'E'(s(s(0)), f(X_124)) | 'LE'(f(X_124), s(0))),
% 3.72/3.91      inference(subst, [], [refute_0_64 : [bind(X_91, $fot(X_124))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_68, plain,
% 3.72/3.91      (~ 'E'(s(s(0)), f(X_122)) | ~ 'E'(s(s(0)), f(suc(X_122))) |
% 3.72/3.91       'E'(f(X_122), f(suc(X_122))) | iLEQ(suc(X_122), suc(X_122))),
% 3.72/3.91      inference(subst, [], [clause_383 : [bind(A_2, $fot(X_122))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_69, plain,
% 3.72/3.91      (~ 'LE'(f(suc(X_121)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(X_121))) |
% 3.72/3.91       'LE'(f(X_121), s(s(0)))),
% 3.72/3.91      inference(subst, [], [clause_457 : [bind(B_41, $fot(X_121))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_70, plain,
% 3.72/3.91      (~ 'LE'(f(suc(X_116)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(X_116))) |
% 3.72/3.91       'LE'(f(X_116), s(s(0)))),
% 3.72/3.91      inference(subst, [], [clause_457 : [bind(B_41, $fot(X_116))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_71, plain,
% 3.72/3.91      ('E'(s(s(s(0))), f(suc(X_11))) | 'LE'(f(suc(X_11)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_8 : [bind(B_23, $fot(suc(X_11)))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_72, plain,
% 3.72/3.91      (~ 'LE'(f(suc(X_11)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(X_11))) |
% 3.72/3.91       'LE'(f(X_11), s(s(0)))),
% 3.72/3.91      inference(subst, [], [clause_457 : [bind(B_41, $fot(X_11))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_73, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_11))) | 'E'(s(s(s(0))), f(suc(X_11))) |
% 3.72/3.91       'LE'(f(X_11), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(suc(X_11)), s(s(s(0)))))],
% 3.72/3.91                [refute_0_71, refute_0_72])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_74, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_115))) | 'E'(s(s(s(0))), f(suc(X_115))) |
% 3.72/3.91       'LE'(f(X_115), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_73 : [bind(X_11, $fot(X_115))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_75, plain,
% 3.72/3.91      (~ 'E'(f(suc(X_70)), f(suc(suc(X_70)))) |
% 3.72/3.91       ~ 'E'(s(s(s(0))), f(suc(X_70))) | 'LE'(f(suc(X_70)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_70)), suc(suc(X_70)))),
% 3.72/3.91      inference(subst, [], [refute_0_31 : [bind(X_53, $fot(suc(X_70)))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_76, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(X_11))) |
% 3.72/3.91       'E'(f(suc(X_11)), f(suc(suc(X_11)))) |
% 3.72/3.91       'LE'(f(suc(X_11)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_11)), suc(suc(X_11)))),
% 3.72/3.91      inference(subst, [], [refute_0_17 : [bind(X_22, $fot(suc(X_11)))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_77, plain,
% 3.72/3.91      ('E'(f(suc(X_11)), f(suc(suc(X_11)))) | 'E'(s(s(0)), f(suc(X_11))) |
% 3.72/3.91       'LE'(f(X_11), s(s(0))) | 'LE'(f(suc(X_11)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_11)), suc(suc(X_11)))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_11))))],
% 3.72/3.91                [refute_0_73, refute_0_76])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_78, plain,
% 3.72/3.91      ('E'(f(suc(X_70)), f(suc(suc(X_70)))) | 'E'(s(s(0)), f(suc(X_70))) |
% 3.72/3.91       'LE'(f(X_70), s(s(0))) | 'LE'(f(suc(X_70)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_70)), suc(suc(X_70)))),
% 3.72/3.91      inference(subst, [], [refute_0_77 : [bind(X_11, $fot(X_70))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_79, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(X_70))) | 'E'(s(s(0)), f(suc(X_70))) |
% 3.72/3.91       'LE'(f(X_70), s(s(0))) | 'LE'(f(suc(X_70)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_70)), suc(suc(X_70)))),
% 3.72/3.91      inference(resolve, [$cnf('E'(f(suc(X_70)), f(suc(suc(X_70)))))],
% 3.72/3.91                [refute_0_78, refute_0_75])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_80, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(X_115))) | 'E'(s(s(0)), f(suc(X_115))) |
% 3.72/3.91       'LE'(f(X_115), s(s(0))) | 'LE'(f(suc(X_115)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_115)), suc(suc(X_115)))),
% 3.72/3.91      inference(subst, [], [refute_0_79 : [bind(X_70, $fot(X_115))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_81, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_115))) | 'LE'(f(X_115), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_115)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_115)), suc(suc(X_115)))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_115))))],
% 3.72/3.91                [refute_0_74, refute_0_80])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_82, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_116))) | 'LE'(f(X_116), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_116)), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(X_116)), suc(suc(X_116)))),
% 3.72/3.91      inference(subst, [], [refute_0_81 : [bind(X_115, $fot(X_116))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_83, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_116))) | 'LE'(f(X_116), s(s(0))) |
% 3.72/3.91       iLEQ(suc(suc(X_116)), suc(suc(X_116)))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(suc(X_116)), s(s(s(0)))))],
% 3.72/3.91                [refute_0_82, refute_0_70])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_84, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_120))) | 'LE'(f(X_120), s(s(0))) |
% 3.72/3.91       iLEQ(suc(suc(X_120)), suc(suc(X_120)))),
% 3.72/3.91      inference(subst, [], [refute_0_83 : [bind(X_116, $fot(X_120))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_85, plain,
% 3.72/3.91      (~ 'E'(f(suc(X_11)), f(suc(suc(X_11)))) |
% 3.72/3.91       ~ 'E'(s(s(s(0))), f(suc(X_11))) |
% 3.72/3.91       ~ iLEQ(suc(suc(X_11)), suc(suc(X_11))) |
% 3.72/3.91       'LE'(f(suc(X_11)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_45 : [bind(X_49, $fot(suc(X_11)))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_86, plain,
% 3.72/3.91      (~ 'E'(f(suc(X_11)), f(suc(suc(X_11)))) |
% 3.72/3.91       ~ iLEQ(suc(suc(X_11)), suc(suc(X_11))) | 'E'(s(s(0)), f(suc(X_11))) |
% 3.72/3.91       'LE'(f(X_11), s(s(0))) | 'LE'(f(suc(X_11)), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_11))))],
% 3.72/3.91                [refute_0_73, refute_0_85])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_87, plain,
% 3.72/3.91      (~ 'E'(f(suc(X_118)), f(suc(suc(X_118)))) |
% 3.72/3.91       ~ iLEQ(suc(suc(X_118)), suc(suc(X_118))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(X_118))) | 'LE'(f(X_118), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_118)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_86 : [bind(X_11, $fot(X_118))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_88, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(X_11))) |
% 3.72/3.91       ~ iLEQ(suc(suc(X_11)), suc(suc(X_11))) |
% 3.72/3.91       'E'(f(suc(X_11)), f(suc(suc(X_11)))) |
% 3.72/3.91       'LE'(f(suc(X_11)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_52 : [bind(X_23, $fot(suc(X_11)))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_89, plain,
% 3.72/3.91      (~ iLEQ(suc(suc(X_11)), suc(suc(X_11))) |
% 3.72/3.91       'E'(f(suc(X_11)), f(suc(suc(X_11)))) | 'E'(s(s(0)), f(suc(X_11))) |
% 3.72/3.91       'LE'(f(X_11), s(s(0))) | 'LE'(f(suc(X_11)), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_11))))],
% 3.72/3.91                [refute_0_73, refute_0_88])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_90, plain,
% 3.72/3.91      (~ iLEQ(suc(suc(X_116)), suc(suc(X_116))) |
% 3.72/3.91       'E'(f(suc(X_116)), f(suc(suc(X_116)))) | 'E'(s(s(0)), f(suc(X_116))) |
% 3.72/3.91       'LE'(f(X_116), s(s(0))) | 'LE'(f(suc(X_116)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_89 : [bind(X_11, $fot(X_116))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_91, plain,
% 3.72/3.91      ('E'(f(suc(X_116)), f(suc(suc(X_116)))) | 'E'(s(s(0)), f(suc(X_116))) |
% 3.72/3.91       'LE'(f(X_116), s(s(0))) | 'LE'(f(suc(X_116)), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf(iLEQ(suc(suc(X_116)), suc(suc(X_116))))],
% 3.72/3.91                [refute_0_82, refute_0_90])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_92, plain,
% 3.72/3.91      ('E'(f(suc(X_118)), f(suc(suc(X_118)))) | 'E'(s(s(0)), f(suc(X_118))) |
% 3.72/3.91       'LE'(f(X_118), s(s(0))) | 'LE'(f(suc(X_118)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_91 : [bind(X_116, $fot(X_118))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_93, plain,
% 3.72/3.91      (~ iLEQ(suc(suc(X_118)), suc(suc(X_118))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(X_118))) | 'LE'(f(X_118), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_118)), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(f(suc(X_118)), f(suc(suc(X_118)))))],
% 3.72/3.91                [refute_0_92, refute_0_87])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_94, plain,
% 3.72/3.91      (~ iLEQ(suc(suc(X_120)), suc(suc(X_120))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(X_120))) | 'LE'(f(X_120), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_120)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_93 : [bind(X_118, $fot(X_120))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_95, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_120))) | 'LE'(f(X_120), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_120)), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf(iLEQ(suc(suc(X_120)), suc(suc(X_120))))],
% 3.72/3.91                [refute_0_84, refute_0_94])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_96, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_121))) | 'LE'(f(X_121), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(X_121)), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_95 : [bind(X_120, $fot(X_121))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_97, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_121))) | 'LE'(f(X_121), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(suc(X_121)), s(s(s(0)))))],
% 3.72/3.91                [refute_0_96, refute_0_69])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_98, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_122))) | 'LE'(f(X_122), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_97 : [bind(X_121, $fot(X_122))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_99, plain,
% 3.72/3.91      (~ 'E'(s(s(0)), f(X_122)) | 'E'(f(X_122), f(suc(X_122))) |
% 3.72/3.91       'LE'(f(X_122), s(s(0))) | iLEQ(suc(X_122), suc(X_122))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_122))))],
% 3.72/3.91                [refute_0_98, refute_0_68])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_100, plain,
% 3.72/3.91      (~ 'E'(s(s(0)), f(X_124)) | 'E'(f(X_124), f(suc(X_124))) |
% 3.72/3.91       'LE'(f(X_124), s(s(0))) | iLEQ(suc(X_124), suc(X_124))),
% 3.72/3.91      inference(subst, [], [refute_0_99 : [bind(X_122, $fot(X_124))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_101, plain,
% 3.72/3.91      ('E'(f(X_124), f(suc(X_124))) | 'E'(s(0), f(X_124)) |
% 3.72/3.91       'LE'(f(X_124), s(0)) | 'LE'(f(X_124), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_124), suc(X_124))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(X_124)))],
% 3.72/3.91                [refute_0_67, refute_0_100])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_102, plain,
% 3.72/3.91      ('E'(f(X_129), f(suc(X_129))) | 'E'(s(0), f(X_129)) |
% 3.72/3.91       'LE'(f(X_129), s(0)) | 'LE'(f(X_129), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_129), suc(X_129))),
% 3.72/3.91      inference(subst, [], [refute_0_101 : [bind(X_124, $fot(X_129))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_103, plain,
% 3.72/3.91      ('E'(f(X_129), f(suc(X_129))) | 'E'(s(0), f(X_129)) |
% 3.72/3.91       'LE'(f(X_129), s(0)) | iLEQ(suc(X_129), suc(X_129))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(X_129), s(s(0))))],
% 3.72/3.91                [refute_0_102, refute_0_66])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_104, plain,
% 3.72/3.91      ('E'(f(X_150), f(suc(X_150))) | 'E'(s(0), f(X_150)) |
% 3.72/3.91       'LE'(f(X_150), s(0)) | iLEQ(suc(X_150), suc(X_150))),
% 3.72/3.91      inference(subst, [], [refute_0_103 : [bind(X_129, $fot(X_150))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_105, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_149))) | 'LE'(f(X_149), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_97 : [bind(X_121, $fot(X_149))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_106, plain,
% 3.72/3.91      (~ 'E'(f(X_143), f(suc(X_143))) | ~ 'E'(s(s(0)), f(X_143)) |
% 3.72/3.91       ~ 'E'(s(s(0)), f(suc(X_143))) | ~ 'E'(s(s(0)), f(suc(suc(X_143)))) |
% 3.72/3.91       iLEQ(suc(X_143), suc(X_143))),
% 3.72/3.91      inference(subst, [], [clause_415 : [bind(A_2, $fot(X_143))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_107, plain,
% 3.72/3.91      (~ 'LE'(f(suc(suc(X_142))), s(s(s(0)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_142)))) | 'LE'(f(X_142), s(s(0)))),
% 3.72/3.91      inference(subst, [], [clause_607 : [bind(B_41, $fot(X_142))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_108, plain,
% 3.72/3.91      ('E'(s(s(s(0))), f(suc(suc(X_14)))) |
% 3.72/3.91       'LE'(f(suc(suc(X_14))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [refute_0_8 : [bind(B_23, $fot(suc(suc(X_14))))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_109, plain,
% 3.72/3.91      (~ 'LE'(f(suc(suc(X_14))), s(s(s(0)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_14)))) | 'LE'(f(X_14), s(s(0)))),
% 3.72/3.91      inference(subst, [], [clause_607 : [bind(B_41, $fot(X_14))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_110, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_14)))) | 'E'(s(s(s(0))), f(suc(suc(X_14)))) |
% 3.72/3.91       'LE'(f(X_14), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(suc(suc(X_14))), s(s(s(0)))))],
% 3.72/3.91                [refute_0_108, refute_0_109])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_111, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_141)))) |
% 3.72/3.91       'E'(s(s(s(0))), f(suc(suc(X_141)))) | 'LE'(f(X_141), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_110 : [bind(X_14, $fot(X_141))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_112, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_127)))) |
% 3.72/3.91       'E'(s(s(s(0))), f(suc(suc(X_127)))) | 'LE'(f(X_127), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_110 : [bind(X_14, $fot(X_127))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_113, plain,
% 3.72/3.91      (~ 'E'(f(suc(suc(X_100))), f(suc(suc(suc(X_100))))) |
% 3.72/3.91       ~ 'E'(s(s(s(0))), f(suc(suc(X_100)))) |
% 3.72/3.91       'LE'(f(suc(suc(X_100))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_100))), suc(suc(suc(X_100))))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [refute_0_31 : [bind(X_53, $fot(suc(suc(X_100))))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_114, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_14)))) |
% 3.72/3.91       'E'(f(suc(suc(X_14))), f(suc(suc(suc(X_14))))) |
% 3.72/3.91       'LE'(f(suc(suc(X_14))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_14))), suc(suc(suc(X_14))))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [refute_0_17 : [bind(X_22, $fot(suc(suc(X_14))))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_115, plain,
% 3.72/3.91      ('E'(f(suc(suc(X_14))), f(suc(suc(suc(X_14))))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_14)))) | 'LE'(f(X_14), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_14))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_14))), suc(suc(suc(X_14))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_14)))))],
% 3.72/3.91                [refute_0_110, refute_0_114])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_116, plain,
% 3.72/3.91      ('E'(f(suc(suc(X_100))), f(suc(suc(suc(X_100))))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_100)))) | 'LE'(f(X_100), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_100))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_100))), suc(suc(suc(X_100))))),
% 3.72/3.91      inference(subst, [], [refute_0_115 : [bind(X_14, $fot(X_100))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_117, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_100)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_100)))) | 'LE'(f(X_100), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_100))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_100))), suc(suc(suc(X_100))))),
% 3.72/3.91      inference(resolve,
% 3.72/3.91                [$cnf('E'(f(suc(suc(X_100))), f(suc(suc(suc(X_100))))))],
% 3.72/3.91                [refute_0_116, refute_0_113])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_118, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_127)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_127)))) | 'LE'(f(X_127), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_127))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_127))), suc(suc(suc(X_127))))),
% 3.72/3.91      inference(subst, [], [refute_0_117 : [bind(X_100, $fot(X_127))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_119, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_127)))) | 'LE'(f(X_127), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_127))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_127))), suc(suc(suc(X_127))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_127)))))],
% 3.72/3.91                [refute_0_112, refute_0_118])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_120, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_140)))) | 'LE'(f(X_140), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_140))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_140))), suc(suc(suc(X_140))))),
% 3.72/3.91      inference(subst, [], [refute_0_119 : [bind(X_127, $fot(X_140))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_121, plain,
% 3.72/3.91      (~ 'E'(f(suc(suc(X_139))), f(suc(suc(suc(X_139))))) |
% 3.72/3.91       ~ 'E'(s(s(s(0))), f(suc(suc(X_139)))) |
% 3.72/3.91       ~ iLEQ(suc(suc(suc(X_139))), suc(suc(suc(X_139)))) |
% 3.72/3.91       'LE'(f(suc(suc(X_139))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [refute_0_45 : [bind(X_49, $fot(suc(suc(X_139))))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_122, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_138)))) |
% 3.72/3.91       'E'(s(s(s(0))), f(suc(suc(X_138)))) | 'LE'(f(X_138), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_110 : [bind(X_14, $fot(X_138))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_123, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_128)))) |
% 3.72/3.91       ~ iLEQ(suc(suc(suc(X_128))), suc(suc(suc(X_128)))) |
% 3.72/3.91       'E'(f(suc(suc(X_128))), f(suc(suc(suc(X_128))))) |
% 3.72/3.91       'LE'(f(suc(suc(X_128))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [refute_0_52 : [bind(X_23, $fot(suc(suc(X_128))))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_124, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_128)))) | 'LE'(f(X_128), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_128))), s(s(s(0)))) |
% 3.72/3.91       iLEQ(suc(suc(suc(X_128))), suc(suc(suc(X_128))))),
% 3.72/3.91      inference(subst, [], [refute_0_119 : [bind(X_127, $fot(X_128))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_125, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_128)))) |
% 3.72/3.91       'E'(f(suc(suc(X_128))), f(suc(suc(suc(X_128))))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_128)))) | 'LE'(f(X_128), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_128))), s(s(s(0))))),
% 3.72/3.91      inference(resolve,
% 3.72/3.91                [$cnf(iLEQ(suc(suc(suc(X_128))), suc(suc(suc(X_128)))))],
% 3.72/3.91                [refute_0_124, refute_0_123])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_126, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_138)))) |
% 3.72/3.91       'E'(f(suc(suc(X_138))), f(suc(suc(suc(X_138))))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_138)))) | 'LE'(f(X_138), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_138))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_125 : [bind(X_128, $fot(X_138))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_127, plain,
% 3.72/3.91      ('E'(f(suc(suc(X_138))), f(suc(suc(suc(X_138))))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_138)))) | 'LE'(f(X_138), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_138))), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_138)))))],
% 3.72/3.91                [refute_0_122, refute_0_126])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_128, plain,
% 3.72/3.91      ('E'(f(suc(suc(X_139))), f(suc(suc(suc(X_139))))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_139)))) | 'LE'(f(X_139), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_139))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_127 : [bind(X_138, $fot(X_139))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_129, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_139)))) |
% 3.72/3.91       ~ iLEQ(suc(suc(suc(X_139))), suc(suc(suc(X_139)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_139)))) | 'LE'(f(X_139), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_139))), s(s(s(0))))),
% 3.72/3.91      inference(resolve,
% 3.72/3.91                [$cnf('E'(f(suc(suc(X_139))), f(suc(suc(suc(X_139))))))],
% 3.72/3.91                [refute_0_128, refute_0_121])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_130, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_140)))) |
% 3.72/3.91       ~ iLEQ(suc(suc(suc(X_140))), suc(suc(suc(X_140)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_140)))) | 'LE'(f(X_140), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_140))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_129 : [bind(X_139, $fot(X_140))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_131, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_140)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_140)))) | 'LE'(f(X_140), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_140))), s(s(s(0))))),
% 3.72/3.91      inference(resolve,
% 3.72/3.91                [$cnf(iLEQ(suc(suc(suc(X_140))), suc(suc(suc(X_140)))))],
% 3.72/3.91                [refute_0_120, refute_0_130])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_132, plain,
% 3.72/3.91      (~ 'E'(s(s(s(0))), f(suc(suc(X_141)))) |
% 3.72/3.91       'E'(s(s(0)), f(suc(suc(X_141)))) | 'LE'(f(X_141), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_141))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_131 : [bind(X_140, $fot(X_141))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_133, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_141)))) | 'LE'(f(X_141), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_141))), s(s(s(0))))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_141)))))],
% 3.72/3.91                [refute_0_111, refute_0_132])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_134, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_142)))) | 'LE'(f(X_142), s(s(0))) |
% 3.72/3.91       'LE'(f(suc(suc(X_142))), s(s(s(0))))),
% 3.72/3.91      inference(subst, [], [refute_0_133 : [bind(X_141, $fot(X_142))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_135, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_142)))) | 'LE'(f(X_142), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(suc(suc(X_142))), s(s(s(0)))))],
% 3.72/3.91                [refute_0_134, refute_0_107])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_136, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(suc(X_143)))) | 'LE'(f(X_143), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_135 : [bind(X_142, $fot(X_143))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_137, plain,
% 3.72/3.91      (~ 'E'(f(X_143), f(suc(X_143))) | ~ 'E'(s(s(0)), f(X_143)) |
% 3.72/3.91       ~ 'E'(s(s(0)), f(suc(X_143))) | 'LE'(f(X_143), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_143), suc(X_143))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_143)))))],
% 3.72/3.91                [refute_0_136, refute_0_106])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_138, plain,
% 3.72/3.91      (~ 'E'(f(X_149), f(suc(X_149))) | ~ 'E'(s(s(0)), f(X_149)) |
% 3.72/3.91       ~ 'E'(s(s(0)), f(suc(X_149))) | 'LE'(f(X_149), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_149), suc(X_149))),
% 3.72/3.91      inference(subst, [], [refute_0_137 : [bind(X_143, $fot(X_149))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_139, plain,
% 3.72/3.91      (~ 'E'(f(X_149), f(suc(X_149))) | ~ 'E'(s(s(0)), f(X_149)) |
% 3.72/3.91       'LE'(f(X_149), s(s(0))) | iLEQ(suc(X_149), suc(X_149))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_149))))],
% 3.72/3.91                [refute_0_105, refute_0_138])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_140, plain,
% 3.72/3.91      (~ 'E'(f(X_150), f(suc(X_150))) | ~ 'E'(s(s(0)), f(X_150)) |
% 3.72/3.91       'LE'(f(X_150), s(s(0))) | iLEQ(suc(X_150), suc(X_150))),
% 3.72/3.91      inference(subst, [], [refute_0_139 : [bind(X_149, $fot(X_150))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_141, plain,
% 3.72/3.91      (~ 'E'(s(s(0)), f(X_150)) | 'E'(s(0), f(X_150)) |
% 3.72/3.91       'LE'(f(X_150), s(0)) | 'LE'(f(X_150), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_150), suc(X_150))),
% 3.72/3.91      inference(resolve, [$cnf('E'(f(X_150), f(suc(X_150))))],
% 3.72/3.91                [refute_0_104, refute_0_140])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_142, plain,
% 3.72/3.91      (~ 'E'(s(s(0)), f(X_178)) | 'E'(s(0), f(X_178)) |
% 3.72/3.91       'LE'(f(X_178), s(0)) | 'LE'(f(X_178), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_178), suc(X_178))),
% 3.72/3.91      inference(subst, [], [refute_0_141 : [bind(X_150, $fot(X_178))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_143, plain,
% 3.72/3.91      ('E'(s(0), f(X_178)) | 'LE'(f(X_178), s(0)) | 'LE'(f(X_178), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_178), suc(X_178))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(X_178)))],
% 3.72/3.91                [refute_0_65, refute_0_142])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_144, plain,
% 3.72/3.91      ('E'(s(0), f(X_179)) | 'LE'(f(X_179), s(0)) | 'LE'(f(X_179), s(s(0))) |
% 3.72/3.91       iLEQ(suc(X_179), suc(X_179))),
% 3.72/3.91      inference(subst, [], [refute_0_143 : [bind(X_178, $fot(X_179))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_145, plain,
% 3.72/3.91      ('E'(s(0), f(X_179)) | 'LE'(f(X_179), s(0)) |
% 3.72/3.91       iLEQ(suc(X_179), suc(X_179))),
% 3.72/3.91      inference(resolve, [$cnf('LE'(f(X_179), s(s(0))))],
% 3.72/3.91                [refute_0_144, refute_0_2])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_146, plain,
% 3.72/3.91      ('E'(s(0), f(X_183)) | 'LE'(f(X_183), s(0)) |
% 3.72/3.91       iLEQ(suc(X_183), suc(X_183))),
% 3.72/3.91      inference(subst, [], [refute_0_145 : [bind(X_179, $fot(X_183))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_147, plain,
% 3.72/3.91      ('E'(s(0), f(X_156)) | 'E'(s(s(0)), f(X_156)) | 'LE'(f(X_156), s(0))),
% 3.72/3.91      inference(subst, [], [refute_0_64 : [bind(X_91, $fot(X_156))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_148, plain,
% 3.72/3.91      ('E'(s(s(0)), f(suc(X_155))) | 'LE'(f(X_155), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_97 : [bind(X_121, $fot(X_155))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_149, plain,
% 3.72/3.91      (~ 'E'(f(X_143), f(suc(X_143))) | ~ 'E'(s(s(0)), f(X_143)) |
% 3.72/3.91       ~ 'E'(s(s(0)), f(suc(X_143))) | ~ 'E'(s(s(0)), f(suc(suc(X_143)))) |
% 3.72/3.91       ~ iLEQ(suc(X_143), suc(X_143))),
% 3.72/3.91      inference(subst, [],
% 3.72/3.91                [clause_528 :
% 3.72/3.91                 [bind(A_2, $fot(X_143)), bind(B_42, $fot(X_143)),
% 3.72/3.91                  bind(B_43, $fot(X_143))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_150, plain,
% 3.72/3.91      (~ 'E'(f(X_143), f(suc(X_143))) | ~ 'E'(s(s(0)), f(X_143)) |
% 3.72/3.91       ~ 'E'(s(s(0)), f(suc(X_143))) | ~ iLEQ(suc(X_143), suc(X_143)) |
% 3.72/3.91       'LE'(f(X_143), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_143)))))],
% 3.72/3.91                [refute_0_136, refute_0_149])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_151, plain,
% 3.72/3.91      (~ 'E'(f(X_155), f(suc(X_155))) | ~ 'E'(s(s(0)), f(X_155)) |
% 3.72/3.91       ~ 'E'(s(s(0)), f(suc(X_155))) | ~ iLEQ(suc(X_155), suc(X_155)) |
% 3.72/3.91       'LE'(f(X_155), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_150 : [bind(X_143, $fot(X_155))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_152, plain,
% 3.72/3.91      (~ 'E'(f(X_155), f(suc(X_155))) | ~ 'E'(s(s(0)), f(X_155)) |
% 3.72/3.91       ~ iLEQ(suc(X_155), suc(X_155)) | 'LE'(f(X_155), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_155))))],
% 3.72/3.91                [refute_0_148, refute_0_151])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_153, plain,
% 3.72/3.91      (~ 'E'(f(X_156), f(suc(X_156))) | ~ 'E'(s(s(0)), f(X_156)) |
% 3.72/3.91       ~ iLEQ(suc(X_156), suc(X_156)) | 'LE'(f(X_156), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_152 : [bind(X_155, $fot(X_156))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_154, plain,
% 3.72/3.91      (~ 'E'(f(X_156), f(suc(X_156))) | ~ iLEQ(suc(X_156), suc(X_156)) |
% 3.72/3.91       'E'(s(0), f(X_156)) | 'LE'(f(X_156), s(0)) | 'LE'(f(X_156), s(s(0)))),
% 3.72/3.91      inference(resolve, [$cnf('E'(s(s(0)), f(X_156)))],
% 3.72/3.91                [refute_0_147, refute_0_153])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_155, plain,
% 3.72/3.91      (~ 'E'(f(X_181), f(suc(X_181))) | ~ iLEQ(suc(X_181), suc(X_181)) |
% 3.72/3.91       'E'(s(0), f(X_181)) | 'LE'(f(X_181), s(0)) | 'LE'(f(X_181), s(s(0)))),
% 3.72/3.91      inference(subst, [], [refute_0_154 : [bind(X_156, $fot(X_181))]])).
% 3.72/3.91  
% 3.72/3.91  cnf(refute_0_156, plain,
% 3.72/3.92      ('E'(s(0), f(X_123)) | 'E'(s(s(0)), f(X_123)) | 'LE'(f(X_123), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_64 : [bind(X_91, $fot(X_123))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_157, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(X_122)) | ~ 'E'(s(s(0)), f(suc(X_122))) |
% 3.72/3.92       ~ iLEQ(suc(X_122), suc(X_122)) | 'E'(f(X_122), f(suc(X_122)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [clause_463 :
% 3.72/3.92                 [bind(A_2, $fot(X_122)), bind(B_42, $fot(X_122)),
% 3.72/3.92                  bind(B_43, $fot(X_122))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_158, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(X_122)) | ~ iLEQ(suc(X_122), suc(X_122)) |
% 3.72/3.92       'E'(f(X_122), f(suc(X_122))) | 'LE'(f(X_122), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_122))))],
% 3.72/3.92                [refute_0_98, refute_0_157])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_159, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(X_123)) | ~ iLEQ(suc(X_123), suc(X_123)) |
% 3.72/3.92       'E'(f(X_123), f(suc(X_123))) | 'LE'(f(X_123), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_158 : [bind(X_122, $fot(X_123))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_160, plain,
% 3.72/3.92      (~ iLEQ(suc(X_123), suc(X_123)) | 'E'(f(X_123), f(suc(X_123))) |
% 3.72/3.92       'E'(s(0), f(X_123)) | 'LE'(f(X_123), s(0)) | 'LE'(f(X_123), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(X_123)))],
% 3.72/3.92                [refute_0_156, refute_0_159])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_161, plain,
% 3.72/3.92      (~ iLEQ(suc(X_179), suc(X_179)) | 'E'(f(X_179), f(suc(X_179))) |
% 3.72/3.92       'E'(s(0), f(X_179)) | 'LE'(f(X_179), s(0)) | 'LE'(f(X_179), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_160 : [bind(X_123, $fot(X_179))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_162, plain,
% 3.72/3.92      ('E'(f(X_179), f(suc(X_179))) | 'E'(s(0), f(X_179)) |
% 3.72/3.92       'LE'(f(X_179), s(0)) | 'LE'(f(X_179), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf(iLEQ(suc(X_179), suc(X_179)))],
% 3.72/3.92                [refute_0_144, refute_0_161])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_163, plain,
% 3.72/3.92      ('E'(f(X_181), f(suc(X_181))) | 'E'(s(0), f(X_181)) |
% 3.72/3.92       'LE'(f(X_181), s(0)) | 'LE'(f(X_181), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_162 : [bind(X_179, $fot(X_181))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_164, plain,
% 3.72/3.92      (~ iLEQ(suc(X_181), suc(X_181)) | 'E'(s(0), f(X_181)) |
% 3.72/3.92       'LE'(f(X_181), s(0)) | 'LE'(f(X_181), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(f(X_181), f(suc(X_181))))],
% 3.72/3.92                [refute_0_163, refute_0_155])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_165, plain,
% 3.72/3.92      (~ iLEQ(suc(X_183), suc(X_183)) | 'E'(s(0), f(X_183)) |
% 3.72/3.92       'LE'(f(X_183), s(0)) | 'LE'(f(X_183), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_164 : [bind(X_181, $fot(X_183))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_166, plain,
% 3.72/3.92      ('E'(s(0), f(X_183)) | 'LE'(f(X_183), s(0)) | 'LE'(f(X_183), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf(iLEQ(suc(X_183), suc(X_183)))],
% 3.72/3.92                [refute_0_146, refute_0_165])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_167, plain,
% 3.72/3.92      ('E'(s(0), f(X_184)) | 'LE'(f(X_184), s(0)) | 'LE'(f(X_184), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_166 : [bind(X_183, $fot(X_184))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_168, plain, ('E'(s(0), f(X_184)) | 'LE'(f(X_184), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(X_184), s(s(0))))],
% 3.72/3.92                [refute_0_167, refute_0_1])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_169, plain,
% 3.72/3.92      ('E'(s(0), f(suc(B_60))) | 'LE'(f(suc(B_60)), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_168 : [bind(X_184, $fot(suc(B_60)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_170, plain,
% 3.72/3.92      ('E'(0, f(suc(B_60))) | 'E'(s(0), f(suc(B_60))) | 'LE'(f(B_60), 0)),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(B_60)), s(0)))],
% 3.72/3.92                [refute_0_169, clause_595])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_171, plain,
% 3.72/3.92      ('E'(0, f(suc(X_483))) | 'E'(s(0), f(suc(X_483))) | 'LE'(f(X_483), 0)),
% 3.72/3.92      inference(subst, [], [refute_0_170 : [bind(B_60, $fot(X_483))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_172, plain,
% 3.72/3.92      ('E'(0, f(suc(X_435))) | 'E'(s(0), f(suc(X_435))) | 'LE'(f(X_435), 0)),
% 3.72/3.92      inference(subst, [], [refute_0_170 : [bind(B_60, $fot(X_435))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_173, plain,
% 3.72/3.92      (~ 'E'(s(0), f(X_242)) | ~ 'E'(s(0), f(suc(X_242))) |
% 3.72/3.92       'E'(f(X_242), f(suc(X_242))) | iLEQ(suc(X_242), suc(X_242))),
% 3.72/3.92      inference(subst, [], [clause_563 : [bind(A_3, $fot(X_242))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_174, plain,
% 3.72/3.92      (~ 'LE'(f(suc(X_241)), s(s(0))) | 'E'(s(0), f(suc(X_241))) |
% 3.72/3.92       'LE'(f(X_241), s(0))),
% 3.72/3.92      inference(subst, [], [clause_95 : [bind(B_53, $fot(X_241))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_175, plain,
% 3.72/3.92      ('E'(s(s(0)), f(suc(B_53))) | 'LE'(f(suc(B_53)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_62 : [bind(X_90, $fot(suc(B_53)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_176, plain,
% 3.72/3.92      ('E'(s(0), f(suc(B_53))) | 'E'(s(s(0)), f(suc(B_53))) |
% 3.72/3.92       'LE'(f(B_53), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(B_53)), s(s(0))))],
% 3.72/3.92                [refute_0_175, clause_95])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_177, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_240))) | 'E'(s(s(0)), f(suc(X_240))) |
% 3.72/3.92       'LE'(f(X_240), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_176 : [bind(B_53, $fot(X_240))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_178, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_222))) | 'E'(s(s(0)), f(suc(X_222))) |
% 3.72/3.92       'LE'(f(X_222), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_176 : [bind(B_53, $fot(X_222))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_179, plain,
% 3.72/3.92      (~ 'E'(f(suc(X_166)), f(suc(suc(X_166)))) |
% 3.72/3.92       ~ 'E'(s(s(0)), f(suc(X_166))) | 'LE'(f(suc(X_166)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(X_166)), suc(suc(X_166)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_139 : [bind(X_149, $fot(suc(X_166)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_180, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(B_53))) | 'E'(f(suc(B_53)), f(suc(suc(B_53)))) |
% 3.72/3.92       'LE'(f(suc(B_53)), s(s(0))) | iLEQ(suc(suc(B_53)), suc(suc(B_53)))),
% 3.72/3.92      inference(subst, [], [refute_0_99 : [bind(X_122, $fot(suc(B_53)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_181, plain,
% 3.72/3.92      ('E'(f(suc(B_53)), f(suc(suc(B_53)))) | 'E'(s(0), f(suc(B_53))) |
% 3.72/3.92       'LE'(f(B_53), s(0)) | 'LE'(f(suc(B_53)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(B_53)), suc(suc(B_53)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(B_53))))],
% 3.72/3.92                [refute_0_176, refute_0_180])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_182, plain,
% 3.72/3.92      ('E'(f(suc(X_166)), f(suc(suc(X_166)))) | 'E'(s(0), f(suc(X_166))) |
% 3.72/3.92       'LE'(f(X_166), s(0)) | 'LE'(f(suc(X_166)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(X_166)), suc(suc(X_166)))),
% 3.72/3.92      inference(subst, [], [refute_0_181 : [bind(B_53, $fot(X_166))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_183, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_166))) | 'E'(s(0), f(suc(X_166))) |
% 3.72/3.92       'LE'(f(X_166), s(0)) | 'LE'(f(suc(X_166)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(X_166)), suc(suc(X_166)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(f(suc(X_166)), f(suc(suc(X_166)))))],
% 3.72/3.92                [refute_0_182, refute_0_179])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_184, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_222))) | 'E'(s(0), f(suc(X_222))) |
% 3.72/3.92       'LE'(f(X_222), s(0)) | 'LE'(f(suc(X_222)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(X_222)), suc(suc(X_222)))),
% 3.72/3.92      inference(subst, [], [refute_0_183 : [bind(X_166, $fot(X_222))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_185, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_222))) | 'LE'(f(X_222), s(0)) |
% 3.72/3.92       'LE'(f(suc(X_222)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(X_222)), suc(suc(X_222)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_222))))],
% 3.72/3.92                [refute_0_178, refute_0_184])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_186, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_239))) | 'LE'(f(X_239), s(0)) |
% 3.72/3.92       'LE'(f(suc(X_239)), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(X_239)), suc(suc(X_239)))),
% 3.72/3.92      inference(subst, [], [refute_0_185 : [bind(X_222, $fot(X_239))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_187, plain,
% 3.72/3.92      (~ 'E'(f(suc(X_238)), f(suc(suc(X_238)))) |
% 3.72/3.92       ~ 'E'(s(s(0)), f(suc(X_238))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_238)), suc(suc(X_238))) |
% 3.72/3.92       'LE'(f(suc(X_238)), s(s(0)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_152 : [bind(X_155, $fot(suc(X_238)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_188, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_237))) | 'E'(s(s(0)), f(suc(X_237))) |
% 3.72/3.92       'LE'(f(X_237), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_176 : [bind(B_53, $fot(X_237))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_189, plain,
% 3.72/3.92      ('E'(s(s(0)), f(suc(suc(X_236)))) | 'LE'(f(suc(X_236)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_97 : [bind(X_121, $fot(suc(X_236)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_190, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_222))) | ~ 'E'(s(s(0)), f(suc(suc(X_222)))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_222)), suc(suc(X_222))) |
% 3.72/3.92       'E'(f(suc(X_222)), f(suc(suc(X_222))))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [clause_463 :
% 3.72/3.92                 [bind(A_2, $fot(suc(X_222))), bind(B_42, $fot(suc(X_222))),
% 3.72/3.92                  bind(B_43, $fot(suc(X_222)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_191, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_222))) | ~ 'E'(s(s(0)), f(suc(suc(X_222)))) |
% 3.72/3.92       'E'(f(suc(X_222)), f(suc(suc(X_222)))) | 'E'(s(0), f(suc(X_222))) |
% 3.72/3.92       'LE'(f(X_222), s(0)) | 'LE'(f(suc(X_222)), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf(iLEQ(suc(suc(X_222)), suc(suc(X_222))))],
% 3.72/3.92                [refute_0_185, refute_0_190])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_192, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_236))) | ~ 'E'(s(s(0)), f(suc(suc(X_236)))) |
% 3.72/3.92       'E'(f(suc(X_236)), f(suc(suc(X_236)))) | 'E'(s(0), f(suc(X_236))) |
% 3.72/3.92       'LE'(f(X_236), s(0)) | 'LE'(f(suc(X_236)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_191 : [bind(X_222, $fot(X_236))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_193, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_236))) |
% 3.72/3.92       'E'(f(suc(X_236)), f(suc(suc(X_236)))) | 'E'(s(0), f(suc(X_236))) |
% 3.72/3.92       'LE'(f(X_236), s(0)) | 'LE'(f(suc(X_236)), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_236)))))],
% 3.72/3.92                [refute_0_189, refute_0_192])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_194, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_237))) |
% 3.72/3.92       'E'(f(suc(X_237)), f(suc(suc(X_237)))) | 'E'(s(0), f(suc(X_237))) |
% 3.72/3.92       'LE'(f(X_237), s(0)) | 'LE'(f(suc(X_237)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_193 : [bind(X_236, $fot(X_237))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_195, plain,
% 3.72/3.92      ('E'(f(suc(X_237)), f(suc(suc(X_237)))) | 'E'(s(0), f(suc(X_237))) |
% 3.72/3.92       'LE'(f(X_237), s(0)) | 'LE'(f(suc(X_237)), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_237))))],
% 3.72/3.92                [refute_0_188, refute_0_194])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_196, plain,
% 3.72/3.92      ('E'(f(suc(X_238)), f(suc(suc(X_238)))) | 'E'(s(0), f(suc(X_238))) |
% 3.72/3.92       'LE'(f(X_238), s(0)) | 'LE'(f(suc(X_238)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_195 : [bind(X_237, $fot(X_238))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_197, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_238))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_238)), suc(suc(X_238))) | 'E'(s(0), f(suc(X_238))) |
% 3.72/3.92       'LE'(f(X_238), s(0)) | 'LE'(f(suc(X_238)), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(f(suc(X_238)), f(suc(suc(X_238)))))],
% 3.72/3.92                [refute_0_196, refute_0_187])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_198, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_239))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_239)), suc(suc(X_239))) | 'E'(s(0), f(suc(X_239))) |
% 3.72/3.92       'LE'(f(X_239), s(0)) | 'LE'(f(suc(X_239)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_197 : [bind(X_238, $fot(X_239))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_199, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_239))) | 'E'(s(0), f(suc(X_239))) |
% 3.72/3.92       'LE'(f(X_239), s(0)) | 'LE'(f(suc(X_239)), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf(iLEQ(suc(suc(X_239)), suc(suc(X_239))))],
% 3.72/3.92                [refute_0_186, refute_0_198])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_200, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(X_240))) | 'E'(s(0), f(suc(X_240))) |
% 3.72/3.92       'LE'(f(X_240), s(0)) | 'LE'(f(suc(X_240)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_199 : [bind(X_239, $fot(X_240))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_201, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_240))) | 'LE'(f(X_240), s(0)) |
% 3.72/3.92       'LE'(f(suc(X_240)), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_240))))],
% 3.72/3.92                [refute_0_177, refute_0_200])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_202, plain,
% 3.72/3.92      ('E'(s(0), f(suc(X_241))) | 'LE'(f(X_241), s(0)) |
% 3.72/3.92       'LE'(f(suc(X_241)), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_201 : [bind(X_240, $fot(X_241))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_203, plain, ('E'(s(0), f(suc(X_241))) | 'LE'(f(X_241), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(X_241)), s(s(0))))],
% 3.72/3.92                [refute_0_202, refute_0_174])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_204, plain, ('E'(s(0), f(suc(X_242))) | 'LE'(f(X_242), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_203 : [bind(X_241, $fot(X_242))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_205, plain,
% 3.72/3.92      (~ 'E'(s(0), f(X_242)) | 'E'(f(X_242), f(suc(X_242))) |
% 3.72/3.92       'LE'(f(X_242), s(0)) | iLEQ(suc(X_242), suc(X_242))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_242))))],
% 3.72/3.92                [refute_0_204, refute_0_173])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_206, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(B_60))) | 'E'(f(suc(B_60)), f(suc(suc(B_60)))) |
% 3.72/3.92       'LE'(f(suc(B_60)), s(0)) | iLEQ(suc(suc(B_60)), suc(suc(B_60)))),
% 3.72/3.92      inference(subst, [], [refute_0_205 : [bind(X_242, $fot(suc(B_60)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_207, plain,
% 3.72/3.92      ('E'(0, f(suc(B_60))) | 'E'(f(suc(B_60)), f(suc(suc(B_60)))) |
% 3.72/3.92       'LE'(f(B_60), 0) | 'LE'(f(suc(B_60)), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(B_60)), suc(suc(B_60)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(B_60))))],
% 3.72/3.92                [refute_0_170, refute_0_206])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_208, plain, ('E'(s(0), f(suc(X_391))) | 'LE'(f(X_391), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_203 : [bind(X_241, $fot(X_391))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_209, plain,
% 3.72/3.92      (~ 'E'(f(X_385), f(suc(X_385))) | ~ 'E'(s(0), f(X_385)) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_385))) | ~ 'E'(s(0), f(suc(suc(X_385)))) |
% 3.72/3.92       iLEQ(suc(X_385), suc(X_385))),
% 3.72/3.92      inference(subst, [], [clause_125 : [bind(A_3, $fot(X_385))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_210, plain,
% 3.72/3.92      (~ 'LE'(f(suc(suc(X_384))), s(s(0))) | 'E'(s(0), f(suc(suc(X_384)))) |
% 3.72/3.92       'LE'(f(X_384), s(0))),
% 3.72/3.92      inference(subst, [], [clause_508 : [bind(B_53, $fot(X_384))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_211, plain,
% 3.72/3.92      ('E'(s(s(0)), f(suc(suc(B_53)))) | 'LE'(f(suc(suc(B_53))), s(s(0)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_62 : [bind(X_90, $fot(suc(suc(B_53))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_212, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(B_53)))) | 'E'(s(s(0)), f(suc(suc(B_53)))) |
% 3.72/3.92       'LE'(f(B_53), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(suc(B_53))), s(s(0))))],
% 3.72/3.92                [refute_0_211, clause_508])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_213, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_383)))) | 'E'(s(s(0)), f(suc(suc(X_383)))) |
% 3.72/3.92       'LE'(f(X_383), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_212 : [bind(B_53, $fot(X_383))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_214, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_305)))) | 'E'(s(s(0)), f(suc(suc(X_305)))) |
% 3.72/3.92       'LE'(f(X_305), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_212 : [bind(B_53, $fot(X_305))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_215, plain,
% 3.72/3.92      (~ 'E'(f(suc(suc(X_233))), f(suc(suc(suc(X_233))))) |
% 3.72/3.92       ~ 'E'(s(s(0)), f(suc(suc(X_233)))) |
% 3.72/3.92       'LE'(f(suc(suc(X_233))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_233))), suc(suc(suc(X_233))))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_139 : [bind(X_149, $fot(suc(suc(X_233))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_216, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(B_53)))) |
% 3.72/3.92       'E'(f(suc(suc(B_53))), f(suc(suc(suc(B_53))))) |
% 3.72/3.92       'LE'(f(suc(suc(B_53))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(B_53))), suc(suc(suc(B_53))))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_99 : [bind(X_122, $fot(suc(suc(B_53))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_217, plain,
% 3.72/3.92      ('E'(f(suc(suc(B_53))), f(suc(suc(suc(B_53))))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(B_53)))) | 'LE'(f(B_53), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(B_53))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(B_53))), suc(suc(suc(B_53))))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(B_53)))))],
% 3.72/3.92                [refute_0_212, refute_0_216])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_218, plain,
% 3.72/3.92      ('E'(f(suc(suc(X_233))), f(suc(suc(suc(X_233))))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_233)))) | 'LE'(f(X_233), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_233))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_233))), suc(suc(suc(X_233))))),
% 3.72/3.92      inference(subst, [], [refute_0_217 : [bind(B_53, $fot(X_233))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_219, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_233)))) | 'E'(s(0), f(suc(suc(X_233)))) |
% 3.72/3.92       'LE'(f(X_233), s(0)) | 'LE'(f(suc(suc(X_233))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_233))), suc(suc(suc(X_233))))),
% 3.72/3.92      inference(resolve,
% 3.72/3.92                [$cnf('E'(f(suc(suc(X_233))), f(suc(suc(suc(X_233))))))],
% 3.72/3.92                [refute_0_218, refute_0_215])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_220, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_305)))) | 'E'(s(0), f(suc(suc(X_305)))) |
% 3.72/3.92       'LE'(f(X_305), s(0)) | 'LE'(f(suc(suc(X_305))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_305))), suc(suc(suc(X_305))))),
% 3.72/3.92      inference(subst, [], [refute_0_219 : [bind(X_233, $fot(X_305))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_221, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_305)))) | 'LE'(f(X_305), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_305))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_305))), suc(suc(suc(X_305))))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_305)))))],
% 3.72/3.92                [refute_0_214, refute_0_220])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_222, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_382)))) | 'LE'(f(X_382), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_382))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_382))), suc(suc(suc(X_382))))),
% 3.72/3.92      inference(subst, [], [refute_0_221 : [bind(X_305, $fot(X_382))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_223, plain,
% 3.72/3.92      (~ 'E'(f(suc(suc(X_368))), f(suc(suc(suc(X_368))))) |
% 3.72/3.92       ~ 'E'(s(s(0)), f(suc(suc(X_368)))) |
% 3.72/3.92       ~ iLEQ(suc(suc(suc(X_368))), suc(suc(suc(X_368)))) |
% 3.72/3.92       'LE'(f(suc(suc(X_368))), s(s(0)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_152 : [bind(X_155, $fot(suc(suc(X_368))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_224, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_367)))) | 'E'(s(s(0)), f(suc(suc(X_367)))) |
% 3.72/3.92       'LE'(f(X_367), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_212 : [bind(B_53, $fot(X_367))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_225, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_306)))) |
% 3.72/3.92       ~ iLEQ(suc(suc(suc(X_306))), suc(suc(suc(X_306)))) |
% 3.72/3.92       'E'(f(suc(suc(X_306))), f(suc(suc(suc(X_306))))) |
% 3.72/3.92       'LE'(f(suc(suc(X_306))), s(s(0)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_158 : [bind(X_122, $fot(suc(suc(X_306))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_226, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_306)))) | 'LE'(f(X_306), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_306))), s(s(0))) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_306))), suc(suc(suc(X_306))))),
% 3.72/3.92      inference(subst, [], [refute_0_221 : [bind(X_305, $fot(X_306))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_227, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_306)))) |
% 3.72/3.92       'E'(f(suc(suc(X_306))), f(suc(suc(suc(X_306))))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_306)))) | 'LE'(f(X_306), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_306))), s(s(0)))),
% 3.72/3.92      inference(resolve,
% 3.72/3.92                [$cnf(iLEQ(suc(suc(suc(X_306))), suc(suc(suc(X_306)))))],
% 3.72/3.92                [refute_0_226, refute_0_225])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_228, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_367)))) |
% 3.72/3.92       'E'(f(suc(suc(X_367))), f(suc(suc(suc(X_367))))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_367)))) | 'LE'(f(X_367), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_367))), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_227 : [bind(X_306, $fot(X_367))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_229, plain,
% 3.72/3.92      ('E'(f(suc(suc(X_367))), f(suc(suc(suc(X_367))))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_367)))) | 'LE'(f(X_367), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_367))), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_367)))))],
% 3.72/3.92                [refute_0_224, refute_0_228])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_230, plain,
% 3.72/3.92      ('E'(f(suc(suc(X_368))), f(suc(suc(suc(X_368))))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_368)))) | 'LE'(f(X_368), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_368))), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_229 : [bind(X_367, $fot(X_368))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_231, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_368)))) |
% 3.72/3.92       ~ iLEQ(suc(suc(suc(X_368))), suc(suc(suc(X_368)))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_368)))) | 'LE'(f(X_368), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_368))), s(s(0)))),
% 3.72/3.92      inference(resolve,
% 3.72/3.92                [$cnf('E'(f(suc(suc(X_368))), f(suc(suc(suc(X_368))))))],
% 3.72/3.92                [refute_0_230, refute_0_223])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_232, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_382)))) |
% 3.72/3.92       ~ iLEQ(suc(suc(suc(X_382))), suc(suc(suc(X_382)))) |
% 3.72/3.92       'E'(s(0), f(suc(suc(X_382)))) | 'LE'(f(X_382), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_382))), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_231 : [bind(X_368, $fot(X_382))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_233, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_382)))) | 'E'(s(0), f(suc(suc(X_382)))) |
% 3.72/3.92       'LE'(f(X_382), s(0)) | 'LE'(f(suc(suc(X_382))), s(s(0)))),
% 3.72/3.92      inference(resolve,
% 3.72/3.92                [$cnf(iLEQ(suc(suc(suc(X_382))), suc(suc(suc(X_382)))))],
% 3.72/3.92                [refute_0_222, refute_0_232])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_234, plain,
% 3.72/3.92      (~ 'E'(s(s(0)), f(suc(suc(X_383)))) | 'E'(s(0), f(suc(suc(X_383)))) |
% 3.72/3.92       'LE'(f(X_383), s(0)) | 'LE'(f(suc(suc(X_383))), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_233 : [bind(X_382, $fot(X_383))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_235, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_383)))) | 'LE'(f(X_383), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_383))), s(s(0)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_383)))))],
% 3.72/3.92                [refute_0_213, refute_0_234])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_236, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_384)))) | 'LE'(f(X_384), s(0)) |
% 3.72/3.92       'LE'(f(suc(suc(X_384))), s(s(0)))),
% 3.72/3.92      inference(subst, [], [refute_0_235 : [bind(X_383, $fot(X_384))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_237, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_384)))) | 'LE'(f(X_384), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(suc(X_384))), s(s(0))))],
% 3.72/3.92                [refute_0_236, refute_0_210])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_238, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(X_385)))) | 'LE'(f(X_385), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_237 : [bind(X_384, $fot(X_385))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_239, plain,
% 3.72/3.92      (~ 'E'(f(X_385), f(suc(X_385))) | ~ 'E'(s(0), f(X_385)) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_385))) | 'LE'(f(X_385), s(0)) |
% 3.72/3.92       iLEQ(suc(X_385), suc(X_385))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_385)))))],
% 3.72/3.92                [refute_0_238, refute_0_209])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_240, plain,
% 3.72/3.92      (~ 'E'(f(X_391), f(suc(X_391))) | ~ 'E'(s(0), f(X_391)) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_391))) | 'LE'(f(X_391), s(0)) |
% 3.72/3.92       iLEQ(suc(X_391), suc(X_391))),
% 3.72/3.92      inference(subst, [], [refute_0_239 : [bind(X_385, $fot(X_391))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_241, plain,
% 3.72/3.92      (~ 'E'(f(X_391), f(suc(X_391))) | ~ 'E'(s(0), f(X_391)) |
% 3.72/3.92       'LE'(f(X_391), s(0)) | iLEQ(suc(X_391), suc(X_391))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_391))))],
% 3.72/3.92                [refute_0_208, refute_0_240])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_242, plain,
% 3.72/3.92      (~ 'E'(f(suc(B_60)), f(suc(suc(B_60)))) | ~ 'E'(s(0), f(suc(B_60))) |
% 3.72/3.92       'LE'(f(suc(B_60)), s(0)) | iLEQ(suc(suc(B_60)), suc(suc(B_60)))),
% 3.72/3.92      inference(subst, [], [refute_0_241 : [bind(X_391, $fot(suc(B_60)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_243, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(B_60))) | 'E'(0, f(suc(B_60))) | 'LE'(f(B_60), 0) |
% 3.72/3.92       'LE'(f(suc(B_60)), s(0)) | iLEQ(suc(suc(B_60)), suc(suc(B_60)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(f(suc(B_60)), f(suc(suc(B_60)))))],
% 3.72/3.92                [refute_0_207, refute_0_242])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_244, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_435))) | 'E'(0, f(suc(X_435))) |
% 3.72/3.92       'LE'(f(X_435), 0) | 'LE'(f(suc(X_435)), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(X_435)), suc(suc(X_435)))),
% 3.72/3.92      inference(subst, [], [refute_0_243 : [bind(B_60, $fot(X_435))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_245, plain,
% 3.72/3.92      ('E'(0, f(suc(X_435))) | 'LE'(f(X_435), 0) |
% 3.72/3.92       'LE'(f(suc(X_435)), s(0)) | iLEQ(suc(suc(X_435)), suc(suc(X_435)))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_435))))],
% 3.72/3.92                [refute_0_172, refute_0_244])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_246, plain,
% 3.72/3.92      ('E'(0, f(suc(X_482))) | 'LE'(f(X_482), 0) |
% 3.72/3.92       'LE'(f(suc(X_482)), s(0)) | iLEQ(suc(suc(X_482)), suc(suc(X_482)))),
% 3.72/3.92      inference(subst, [], [refute_0_245 : [bind(X_435, $fot(X_482))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_247, plain, ('E'(s(0), f(suc(X_403))) | 'LE'(f(X_403), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_203 : [bind(X_241, $fot(X_403))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_248, plain,
% 3.72/3.92      (~ 'E'(f(X_385), f(suc(X_385))) | ~ 'E'(s(0), f(X_385)) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_385))) | ~ 'E'(s(0), f(suc(suc(X_385)))) |
% 3.72/3.92       ~ iLEQ(suc(X_385), suc(X_385))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [clause_41 :
% 3.72/3.92                 [bind(A_3, $fot(X_385)), bind(B_54, $fot(X_385)),
% 3.72/3.92                  bind(B_55, $fot(X_385))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_249, plain,
% 3.72/3.92      (~ 'E'(f(X_385), f(suc(X_385))) | ~ 'E'(s(0), f(X_385)) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_385))) | ~ iLEQ(suc(X_385), suc(X_385)) |
% 3.72/3.92       'LE'(f(X_385), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_385)))))],
% 3.72/3.92                [refute_0_238, refute_0_248])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_250, plain,
% 3.72/3.92      (~ 'E'(f(X_403), f(suc(X_403))) | ~ 'E'(s(0), f(X_403)) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_403))) | ~ iLEQ(suc(X_403), suc(X_403)) |
% 3.72/3.92       'LE'(f(X_403), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_249 : [bind(X_385, $fot(X_403))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_251, plain,
% 3.72/3.92      (~ 'E'(f(X_403), f(suc(X_403))) | ~ 'E'(s(0), f(X_403)) |
% 3.72/3.92       ~ iLEQ(suc(X_403), suc(X_403)) | 'LE'(f(X_403), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_403))))],
% 3.72/3.92                [refute_0_247, refute_0_250])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_252, plain,
% 3.72/3.92      (~ 'E'(f(suc(X_468)), f(suc(suc(X_468)))) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(X_468))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_468)), suc(suc(X_468))) | 'LE'(f(suc(X_468)), s(0))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_251 : [bind(X_403, $fot(suc(X_468)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_253, plain,
% 3.72/3.92      ('E'(0, f(suc(X_467))) | 'E'(s(0), f(suc(X_467))) | 'LE'(f(X_467), 0)),
% 3.72/3.92      inference(subst, [], [refute_0_170 : [bind(B_60, $fot(X_467))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_254, plain,
% 3.72/3.92      (~ 'E'(s(0), f(X_242)) | ~ 'E'(s(0), f(suc(X_242))) |
% 3.72/3.92       ~ iLEQ(suc(X_242), suc(X_242)) | 'E'(f(X_242), f(suc(X_242)))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [clause_687 :
% 3.72/3.92                 [bind(A_3, $fot(X_242)), bind(B_54, $fot(X_242)),
% 3.72/3.92                  bind(B_55, $fot(X_242))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_255, plain,
% 3.72/3.92      (~ 'E'(s(0), f(X_242)) | ~ iLEQ(suc(X_242), suc(X_242)) |
% 3.72/3.92       'E'(f(X_242), f(suc(X_242))) | 'LE'(f(X_242), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_242))))],
% 3.72/3.92                [refute_0_204, refute_0_254])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_256, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_436))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_436)), suc(suc(X_436))) |
% 3.72/3.92       'E'(f(suc(X_436)), f(suc(suc(X_436)))) | 'LE'(f(suc(X_436)), s(0))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_255 : [bind(X_242, $fot(suc(X_436)))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_257, plain,
% 3.72/3.92      ('E'(0, f(suc(X_436))) | 'LE'(f(X_436), 0) |
% 3.72/3.92       'LE'(f(suc(X_436)), s(0)) | iLEQ(suc(suc(X_436)), suc(suc(X_436)))),
% 3.72/3.92      inference(subst, [], [refute_0_245 : [bind(X_435, $fot(X_436))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_258, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_436))) | 'E'(0, f(suc(X_436))) |
% 3.72/3.92       'E'(f(suc(X_436)), f(suc(suc(X_436)))) | 'LE'(f(X_436), 0) |
% 3.72/3.92       'LE'(f(suc(X_436)), s(0))),
% 3.72/3.92      inference(resolve, [$cnf(iLEQ(suc(suc(X_436)), suc(suc(X_436))))],
% 3.72/3.92                [refute_0_257, refute_0_256])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_259, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_467))) | 'E'(0, f(suc(X_467))) |
% 3.72/3.92       'E'(f(suc(X_467)), f(suc(suc(X_467)))) | 'LE'(f(X_467), 0) |
% 3.72/3.92       'LE'(f(suc(X_467)), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_258 : [bind(X_436, $fot(X_467))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_260, plain,
% 3.72/3.92      ('E'(0, f(suc(X_467))) | 'E'(f(suc(X_467)), f(suc(suc(X_467)))) |
% 3.72/3.92       'LE'(f(X_467), 0) | 'LE'(f(suc(X_467)), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_467))))],
% 3.72/3.92                [refute_0_253, refute_0_259])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_261, plain,
% 3.72/3.92      ('E'(0, f(suc(X_468))) | 'E'(f(suc(X_468)), f(suc(suc(X_468)))) |
% 3.72/3.92       'LE'(f(X_468), 0) | 'LE'(f(suc(X_468)), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_260 : [bind(X_467, $fot(X_468))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_262, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_468))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_468)), suc(suc(X_468))) | 'E'(0, f(suc(X_468))) |
% 3.72/3.92       'LE'(f(X_468), 0) | 'LE'(f(suc(X_468)), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('E'(f(suc(X_468)), f(suc(suc(X_468)))))],
% 3.72/3.92                [refute_0_261, refute_0_252])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_263, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_482))) |
% 3.72/3.92       ~ iLEQ(suc(suc(X_482)), suc(suc(X_482))) | 'E'(0, f(suc(X_482))) |
% 3.72/3.92       'LE'(f(X_482), 0) | 'LE'(f(suc(X_482)), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_262 : [bind(X_468, $fot(X_482))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_264, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_482))) | 'E'(0, f(suc(X_482))) |
% 3.72/3.92       'LE'(f(X_482), 0) | 'LE'(f(suc(X_482)), s(0))),
% 3.72/3.92      inference(resolve, [$cnf(iLEQ(suc(suc(X_482)), suc(suc(X_482))))],
% 3.72/3.92                [refute_0_246, refute_0_263])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_265, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(X_483))) | 'E'(0, f(suc(X_483))) |
% 3.72/3.92       'LE'(f(X_483), 0) | 'LE'(f(suc(X_483)), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_264 : [bind(X_482, $fot(X_483))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_266, plain,
% 3.72/3.92      ('E'(0, f(suc(X_483))) | 'LE'(f(X_483), 0) |
% 3.72/3.92       'LE'(f(suc(X_483)), s(0))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(X_483))))],
% 3.72/3.92                [refute_0_171, refute_0_265])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_267, plain,
% 3.72/3.92      ('E'(0, f(suc(X_484))) | 'LE'(f(X_484), 0) |
% 3.72/3.92       'LE'(f(suc(X_484)), s(0))),
% 3.72/3.92      inference(subst, [], [refute_0_266 : [bind(X_483, $fot(X_484))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_268, plain, ('E'(0, f(suc(X_484))) | 'LE'(f(X_484), 0)),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(X_484)), s(0)))],
% 3.72/3.92                [refute_0_267, refute_0_0])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_269, plain, ('E'(0, f(suc(z))) | 'LE'(f(z), 0)),
% 3.72/3.92      inference(subst, [], [refute_0_268 : [bind(X_484, $fot(z))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_270, plain,
% 3.72/3.92      (~ 'LE'(f(suc(suc(X_666))), s(0)) | 'E'(0, f(suc(suc(X_666)))) |
% 3.72/3.92       'LE'(f(X_666), 0)),
% 3.72/3.92      inference(subst, [], [clause_61 : [bind(B_60, $fot(X_666))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_271, plain,
% 3.72/3.92      ('E'(s(0), f(suc(suc(B_60)))) | 'LE'(f(suc(suc(B_60))), s(0))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_168 : [bind(X_184, $fot(suc(suc(B_60))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_272, plain,
% 3.72/3.92      ('E'(0, f(suc(suc(B_60)))) | 'E'(s(0), f(suc(suc(B_60)))) |
% 3.72/3.92       'LE'(f(B_60), 0)),
% 3.72/3.92      inference(resolve, [$cnf('LE'(f(suc(suc(B_60))), s(0)))],
% 3.72/3.92                [refute_0_271, clause_61])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_273, plain,
% 3.72/3.92      ('E'(0, f(suc(suc(X_665)))) | 'E'(s(0), f(suc(suc(X_665)))) |
% 3.72/3.92       'LE'(f(X_665), 0)),
% 3.72/3.92      inference(subst, [], [refute_0_272 : [bind(B_60, $fot(X_665))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_274, plain,
% 3.72/3.92      ('E'(0, f(suc(suc(X_465)))) | 'E'(s(0), f(suc(suc(X_465)))) |
% 3.72/3.92       'LE'(f(X_465), 0)),
% 3.72/3.92      inference(subst, [], [refute_0_272 : [bind(B_60, $fot(X_465))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_275, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(suc(B_60)))) |
% 3.72/3.92       'E'(f(suc(suc(B_60))), f(suc(suc(suc(B_60))))) |
% 3.72/3.92       'LE'(f(suc(suc(B_60))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(B_60))), suc(suc(suc(B_60))))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_205 : [bind(X_242, $fot(suc(suc(B_60))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_276, plain,
% 3.72/3.92      ('E'(0, f(suc(suc(B_60)))) |
% 3.72/3.92       'E'(f(suc(suc(B_60))), f(suc(suc(suc(B_60))))) | 'LE'(f(B_60), 0) |
% 3.72/3.92       'LE'(f(suc(suc(B_60))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(B_60))), suc(suc(suc(B_60))))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(suc(B_60)))))],
% 3.72/3.92                [refute_0_272, refute_0_275])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_277, plain,
% 3.72/3.92      (~ 'E'(f(suc(suc(B_60))), f(suc(suc(suc(B_60))))) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(suc(B_60)))) | 'LE'(f(suc(suc(B_60))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(B_60))), suc(suc(suc(B_60))))),
% 3.72/3.92      inference(subst, [],
% 3.72/3.92                [refute_0_241 : [bind(X_391, $fot(suc(suc(B_60))))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_278, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(suc(B_60)))) | 'E'(0, f(suc(suc(B_60)))) |
% 3.72/3.92       'LE'(f(B_60), 0) | 'LE'(f(suc(suc(B_60))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(B_60))), suc(suc(suc(B_60))))),
% 3.72/3.92      inference(resolve,
% 3.72/3.92                [$cnf('E'(f(suc(suc(B_60))), f(suc(suc(suc(B_60))))))],
% 3.72/3.92                [refute_0_276, refute_0_277])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_279, plain,
% 3.72/3.92      (~ 'E'(s(0), f(suc(suc(X_465)))) | 'E'(0, f(suc(suc(X_465)))) |
% 3.72/3.92       'LE'(f(X_465), 0) | 'LE'(f(suc(suc(X_465))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_465))), suc(suc(suc(X_465))))),
% 3.72/3.92      inference(subst, [], [refute_0_278 : [bind(B_60, $fot(X_465))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_280, plain,
% 3.72/3.92      ('E'(0, f(suc(suc(X_465)))) | 'LE'(f(X_465), 0) |
% 3.72/3.92       'LE'(f(suc(suc(X_465))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_465))), suc(suc(suc(X_465))))),
% 3.72/3.92      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_465)))))],
% 3.72/3.92                [refute_0_274, refute_0_279])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_281, plain,
% 3.72/3.92      ('E'(0, f(suc(suc(X_664)))) | 'LE'(f(X_664), 0) |
% 3.72/3.92       'LE'(f(suc(suc(X_664))), s(0)) |
% 3.72/3.92       iLEQ(suc(suc(suc(X_664))), suc(suc(suc(X_664))))),
% 3.72/3.92      inference(subst, [], [refute_0_280 : [bind(X_465, $fot(X_664))]])).
% 3.72/3.92  
% 3.72/3.92  cnf(refute_0_282, plain,
% 3.72/3.92      (~ 'E'(f(suc(suc(X_526))), f(suc(suc(suc(X_526))))) |
% 3.72/3.92       ~ 'E'(s(0), f(suc(suc(X_526)))) |
% 3.72/3.92       ~ iLEQ(suc(suc(suc(X_526))), suc(suc(suc(X_526)))) |
% 3.72/3.92       'LE'(f(suc(suc(X_526))), s(0))),
% 3.72/3.93      inference(subst, [],
% 3.72/3.93                [refute_0_251 : [bind(X_403, $fot(suc(suc(X_526))))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_283, plain,
% 3.72/3.93      ('E'(0, f(suc(suc(X_525)))) | 'E'(s(0), f(suc(suc(X_525)))) |
% 3.72/3.93       'LE'(f(X_525), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_272 : [bind(B_60, $fot(X_525))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_284, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_466)))) |
% 3.72/3.93       ~ iLEQ(suc(suc(suc(X_466))), suc(suc(suc(X_466)))) |
% 3.72/3.93       'E'(f(suc(suc(X_466))), f(suc(suc(suc(X_466))))) |
% 3.72/3.93       'LE'(f(suc(suc(X_466))), s(0))),
% 3.72/3.93      inference(subst, [],
% 3.72/3.93                [refute_0_255 : [bind(X_242, $fot(suc(suc(X_466))))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_285, plain,
% 3.72/3.93      ('E'(0, f(suc(suc(X_466)))) | 'LE'(f(X_466), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_466))), s(0)) |
% 3.72/3.93       iLEQ(suc(suc(suc(X_466))), suc(suc(suc(X_466))))),
% 3.72/3.93      inference(subst, [], [refute_0_280 : [bind(X_465, $fot(X_466))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_286, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_466)))) | 'E'(0, f(suc(suc(X_466)))) |
% 3.72/3.93       'E'(f(suc(suc(X_466))), f(suc(suc(suc(X_466))))) | 'LE'(f(X_466), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_466))), s(0))),
% 3.72/3.93      inference(resolve,
% 3.72/3.93                [$cnf(iLEQ(suc(suc(suc(X_466))), suc(suc(suc(X_466)))))],
% 3.72/3.93                [refute_0_285, refute_0_284])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_287, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_525)))) | 'E'(0, f(suc(suc(X_525)))) |
% 3.72/3.93       'E'(f(suc(suc(X_525))), f(suc(suc(suc(X_525))))) | 'LE'(f(X_525), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_525))), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_286 : [bind(X_466, $fot(X_525))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_288, plain,
% 3.72/3.93      ('E'(0, f(suc(suc(X_525)))) |
% 3.72/3.93       'E'(f(suc(suc(X_525))), f(suc(suc(suc(X_525))))) | 'LE'(f(X_525), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_525))), s(0))),
% 3.72/3.93      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_525)))))],
% 3.72/3.93                [refute_0_283, refute_0_287])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_289, plain,
% 3.72/3.93      ('E'(0, f(suc(suc(X_526)))) |
% 3.72/3.93       'E'(f(suc(suc(X_526))), f(suc(suc(suc(X_526))))) | 'LE'(f(X_526), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_526))), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_288 : [bind(X_525, $fot(X_526))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_290, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_526)))) |
% 3.72/3.93       ~ iLEQ(suc(suc(suc(X_526))), suc(suc(suc(X_526)))) |
% 3.72/3.93       'E'(0, f(suc(suc(X_526)))) | 'LE'(f(X_526), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_526))), s(0))),
% 3.72/3.93      inference(resolve,
% 3.72/3.93                [$cnf('E'(f(suc(suc(X_526))), f(suc(suc(suc(X_526))))))],
% 3.72/3.93                [refute_0_289, refute_0_282])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_291, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_664)))) |
% 3.72/3.93       ~ iLEQ(suc(suc(suc(X_664))), suc(suc(suc(X_664)))) |
% 3.72/3.93       'E'(0, f(suc(suc(X_664)))) | 'LE'(f(X_664), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_664))), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_290 : [bind(X_526, $fot(X_664))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_292, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_664)))) | 'E'(0, f(suc(suc(X_664)))) |
% 3.72/3.93       'LE'(f(X_664), 0) | 'LE'(f(suc(suc(X_664))), s(0))),
% 3.72/3.93      inference(resolve,
% 3.72/3.93                [$cnf(iLEQ(suc(suc(suc(X_664))), suc(suc(suc(X_664)))))],
% 3.72/3.93                [refute_0_281, refute_0_291])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_293, plain,
% 3.72/3.93      (~ 'E'(s(0), f(suc(suc(X_665)))) | 'E'(0, f(suc(suc(X_665)))) |
% 3.72/3.93       'LE'(f(X_665), 0) | 'LE'(f(suc(suc(X_665))), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_292 : [bind(X_664, $fot(X_665))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_294, plain,
% 3.72/3.93      ('E'(0, f(suc(suc(X_665)))) | 'LE'(f(X_665), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_665))), s(0))),
% 3.72/3.93      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_665)))))],
% 3.72/3.93                [refute_0_273, refute_0_293])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_295, plain,
% 3.72/3.93      ('E'(0, f(suc(suc(X_666)))) | 'LE'(f(X_666), 0) |
% 3.72/3.93       'LE'(f(suc(suc(X_666))), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_294 : [bind(X_665, $fot(X_666))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_296, plain, ('E'(0, f(suc(suc(X_666)))) | 'LE'(f(X_666), 0)),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(suc(suc(X_666))), s(0)))],
% 3.72/3.93                [refute_0_295, refute_0_270])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_297, plain, ('E'(0, f(suc(suc(z)))) | 'LE'(f(z), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_296 : [bind(X_666, $fot(z))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_298, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 3.72/3.93       ~ 'E'(f(z), f(suc(z))) | ~ iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(subst, [],
% 3.72/3.93                [clause_363 :
% 3.72/3.93                 [bind(A_4, $fot(z)), bind(B_61, $fot(z)),
% 3.72/3.93                  bind(B_62, $fot(z))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_299, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) | ~ iLEQ(suc(z), suc(z)) |
% 3.72/3.93       'E'(f(z), f(suc(z)))),
% 3.72/3.93      inference(subst, [],
% 3.72/3.93                [clause_614 :
% 3.72/3.93                 [bind(A_4, $fot(z)), bind(B_61, $fot(z)),
% 3.72/3.93                  bind(B_62, $fot(z))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_300, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 3.72/3.93       ~ 'E'(f(z), f(suc(z))) | iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(subst, [], [clause_560 : [bind(A_4, $fot(z))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_301, plain,
% 3.72/3.93      (~ 'LE'(f(X_424), s(0)) | 'E'(0, f(X_424)) | 'LE'(f(X_424), 0)),
% 3.72/3.93      inference(subst, [], [clause_497 : [bind(B_60, $fot(X_424))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_302, plain,
% 3.72/3.93      (~ 'LE'(f(X_185), s(0)) | 'E'(0, f(X_185)) | 'LE'(f(X_185), 0)),
% 3.72/3.93      inference(subst, [], [clause_497 : [bind(B_60, $fot(X_185))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_303, plain, ('E'(s(0), f(X_185)) | 'LE'(f(X_185), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_168 : [bind(X_184, $fot(X_185))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_304, plain,
% 3.72/3.93      ('E'(0, f(X_185)) | 'E'(s(0), f(X_185)) | 'LE'(f(X_185), 0)),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(X_185), s(0)))],
% 3.72/3.93                [refute_0_303, refute_0_302])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_305, plain,
% 3.72/3.93      ('E'(0, f(X_423)) | 'E'(s(0), f(X_423)) | 'LE'(f(X_423), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_304 : [bind(X_185, $fot(X_423))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_306, plain,
% 3.72/3.93      ('E'(0, f(X_401)) | 'E'(s(0), f(X_401)) | 'LE'(f(X_401), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_304 : [bind(X_185, $fot(X_401))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_307, plain,
% 3.72/3.93      ('E'(0, f(X_243)) | 'E'(s(0), f(X_243)) | 'LE'(f(X_243), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_304 : [bind(X_185, $fot(X_243))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_308, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_243)) | 'E'(f(X_243), f(suc(X_243))) |
% 3.72/3.93       'LE'(f(X_243), s(0)) | iLEQ(suc(X_243), suc(X_243))),
% 3.72/3.93      inference(subst, [], [refute_0_205 : [bind(X_242, $fot(X_243))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_309, plain,
% 3.72/3.93      ('E'(0, f(X_243)) | 'E'(f(X_243), f(suc(X_243))) | 'LE'(f(X_243), 0) |
% 3.72/3.93       'LE'(f(X_243), s(0)) | iLEQ(suc(X_243), suc(X_243))),
% 3.72/3.93      inference(resolve, [$cnf('E'(s(0), f(X_243)))],
% 3.72/3.93                [refute_0_307, refute_0_308])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_310, plain,
% 3.72/3.93      ('E'(0, f(X_392)) | 'E'(f(X_392), f(suc(X_392))) | 'LE'(f(X_392), 0) |
% 3.72/3.93       'LE'(f(X_392), s(0)) | iLEQ(suc(X_392), suc(X_392))),
% 3.72/3.93      inference(subst, [], [refute_0_309 : [bind(X_243, $fot(X_392))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_311, plain,
% 3.72/3.93      (~ 'E'(f(X_392), f(suc(X_392))) | ~ 'E'(s(0), f(X_392)) |
% 3.72/3.93       'LE'(f(X_392), s(0)) | iLEQ(suc(X_392), suc(X_392))),
% 3.72/3.93      inference(subst, [], [refute_0_241 : [bind(X_391, $fot(X_392))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_312, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_392)) | 'E'(0, f(X_392)) | 'LE'(f(X_392), 0) |
% 3.72/3.93       'LE'(f(X_392), s(0)) | iLEQ(suc(X_392), suc(X_392))),
% 3.72/3.93      inference(resolve, [$cnf('E'(f(X_392), f(suc(X_392))))],
% 3.72/3.93                [refute_0_310, refute_0_311])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_313, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_401)) | 'E'(0, f(X_401)) | 'LE'(f(X_401), 0) |
% 3.72/3.93       'LE'(f(X_401), s(0)) | iLEQ(suc(X_401), suc(X_401))),
% 3.72/3.93      inference(subst, [], [refute_0_312 : [bind(X_392, $fot(X_401))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_314, plain,
% 3.72/3.93      ('E'(0, f(X_401)) | 'LE'(f(X_401), 0) | 'LE'(f(X_401), s(0)) |
% 3.72/3.93       iLEQ(suc(X_401), suc(X_401))),
% 3.72/3.93      inference(resolve, [$cnf('E'(s(0), f(X_401)))],
% 3.72/3.93                [refute_0_306, refute_0_313])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_315, plain,
% 3.72/3.93      ('E'(0, f(X_422)) | 'LE'(f(X_422), 0) | 'LE'(f(X_422), s(0)) |
% 3.72/3.93       iLEQ(suc(X_422), suc(X_422))),
% 3.72/3.93      inference(subst, [], [refute_0_314 : [bind(X_401, $fot(X_422))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_316, plain,
% 3.72/3.93      (~ 'E'(f(X_415), f(suc(X_415))) | ~ 'E'(s(0), f(X_415)) |
% 3.72/3.93       ~ iLEQ(suc(X_415), suc(X_415)) | 'LE'(f(X_415), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_251 : [bind(X_403, $fot(X_415))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_317, plain,
% 3.72/3.93      ('E'(0, f(X_414)) | 'E'(s(0), f(X_414)) | 'LE'(f(X_414), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_304 : [bind(X_185, $fot(X_414))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_318, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_402)) | ~ iLEQ(suc(X_402), suc(X_402)) |
% 3.72/3.93       'E'(f(X_402), f(suc(X_402))) | 'LE'(f(X_402), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_255 : [bind(X_242, $fot(X_402))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_319, plain,
% 3.72/3.93      ('E'(0, f(X_402)) | 'LE'(f(X_402), 0) | 'LE'(f(X_402), s(0)) |
% 3.72/3.93       iLEQ(suc(X_402), suc(X_402))),
% 3.72/3.93      inference(subst, [], [refute_0_314 : [bind(X_401, $fot(X_402))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_320, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_402)) | 'E'(0, f(X_402)) |
% 3.72/3.93       'E'(f(X_402), f(suc(X_402))) | 'LE'(f(X_402), 0) |
% 3.72/3.93       'LE'(f(X_402), s(0))),
% 3.72/3.93      inference(resolve, [$cnf(iLEQ(suc(X_402), suc(X_402)))],
% 3.72/3.93                [refute_0_319, refute_0_318])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_321, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_414)) | 'E'(0, f(X_414)) |
% 3.72/3.93       'E'(f(X_414), f(suc(X_414))) | 'LE'(f(X_414), 0) |
% 3.72/3.93       'LE'(f(X_414), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_320 : [bind(X_402, $fot(X_414))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_322, plain,
% 3.72/3.93      ('E'(0, f(X_414)) | 'E'(f(X_414), f(suc(X_414))) | 'LE'(f(X_414), 0) |
% 3.72/3.93       'LE'(f(X_414), s(0))),
% 3.72/3.93      inference(resolve, [$cnf('E'(s(0), f(X_414)))],
% 3.72/3.93                [refute_0_317, refute_0_321])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_323, plain,
% 3.72/3.93      ('E'(0, f(X_415)) | 'E'(f(X_415), f(suc(X_415))) | 'LE'(f(X_415), 0) |
% 3.72/3.93       'LE'(f(X_415), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_322 : [bind(X_414, $fot(X_415))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_324, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_415)) | ~ iLEQ(suc(X_415), suc(X_415)) |
% 3.72/3.93       'E'(0, f(X_415)) | 'LE'(f(X_415), 0) | 'LE'(f(X_415), s(0))),
% 3.72/3.93      inference(resolve, [$cnf('E'(f(X_415), f(suc(X_415))))],
% 3.72/3.93                [refute_0_323, refute_0_316])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_325, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_422)) | ~ iLEQ(suc(X_422), suc(X_422)) |
% 3.72/3.93       'E'(0, f(X_422)) | 'LE'(f(X_422), 0) | 'LE'(f(X_422), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_324 : [bind(X_415, $fot(X_422))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_326, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_422)) | 'E'(0, f(X_422)) | 'LE'(f(X_422), 0) |
% 3.72/3.93       'LE'(f(X_422), s(0))),
% 3.72/3.93      inference(resolve, [$cnf(iLEQ(suc(X_422), suc(X_422)))],
% 3.72/3.93                [refute_0_315, refute_0_325])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_327, plain,
% 3.72/3.93      (~ 'E'(s(0), f(X_423)) | 'E'(0, f(X_423)) | 'LE'(f(X_423), 0) |
% 3.72/3.93       'LE'(f(X_423), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_326 : [bind(X_422, $fot(X_423))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_328, plain,
% 3.72/3.93      ('E'(0, f(X_423)) | 'LE'(f(X_423), 0) | 'LE'(f(X_423), s(0))),
% 3.72/3.93      inference(resolve, [$cnf('E'(s(0), f(X_423)))],
% 3.72/3.93                [refute_0_305, refute_0_327])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_329, plain,
% 3.72/3.93      ('E'(0, f(X_424)) | 'LE'(f(X_424), 0) | 'LE'(f(X_424), s(0))),
% 3.72/3.93      inference(subst, [], [refute_0_328 : [bind(X_423, $fot(X_424))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_330, plain, ('E'(0, f(X_424)) | 'LE'(f(X_424), 0)),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(X_424), s(0)))],
% 3.72/3.93                [refute_0_329, refute_0_301])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_331, plain, ('E'(0, f(z)) | 'LE'(f(z), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_330 : [bind(X_424, $fot(z))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_332, plain, ('E'(0, f(z))),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_331, clause_359])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_333, plain,
% 3.72/3.93      (~ 'E'(0, f(X_485)) | ~ 'E'(0, f(suc(X_485))) |
% 3.72/3.93       'E'(f(X_485), f(suc(X_485))) | iLEQ(suc(X_485), suc(X_485))),
% 3.72/3.93      inference(subst, [], [clause_713 : [bind(A_4, $fot(X_485))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_334, plain, ('E'(0, f(suc(X_485))) | 'LE'(f(X_485), 0)),
% 3.72/3.93      inference(subst, [], [refute_0_268 : [bind(X_484, $fot(X_485))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_335, plain,
% 3.72/3.93      (~ 'E'(0, f(X_485)) | 'E'(f(X_485), f(suc(X_485))) |
% 3.72/3.93       'LE'(f(X_485), 0) | iLEQ(suc(X_485), suc(X_485))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(suc(X_485))))],
% 3.72/3.93                [refute_0_334, refute_0_333])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_336, plain,
% 3.72/3.93      (~ 'E'(0, f(z)) | 'E'(f(z), f(suc(z))) | 'LE'(f(z), 0) |
% 3.72/3.93       iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(subst, [], [refute_0_335 : [bind(X_485, $fot(z))]])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_337, plain,
% 3.72/3.93      ('E'(f(z), f(suc(z))) | 'LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(z)))],
% 3.72/3.93                [refute_0_332, refute_0_336])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_338, plain, ('E'(f(z), f(suc(z))) | iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_337, clause_359])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_339, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 3.72/3.93       iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(f(z), f(suc(z))))],
% 3.72/3.93                [refute_0_338, refute_0_300])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_340, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) |
% 3.72/3.93       iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(z)))],
% 3.72/3.93                [refute_0_332, refute_0_339])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_341, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(z))) | 'LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(suc(suc(z)))))],
% 3.72/3.93                [refute_0_297, refute_0_340])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_342, plain, (~ 'E'(0, f(suc(z))) | iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_341, clause_359])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_343, plain, ('LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 3.72/3.93                [refute_0_269, refute_0_342])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_344, plain, (iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_343, clause_359])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_345, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) | 'E'(f(z), f(suc(z)))),
% 3.72/3.93      inference(resolve, [$cnf(iLEQ(suc(z), suc(z)))],
% 3.72/3.93                [refute_0_344, refute_0_299])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_346, plain, (~ 'E'(0, f(suc(z))) | 'E'(f(z), f(suc(z)))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(z)))],
% 3.72/3.93                [refute_0_332, refute_0_345])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_347, plain, ('E'(f(z), f(suc(z))) | 'LE'(f(z), 0)),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 3.72/3.93                [refute_0_269, refute_0_346])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_348, plain, ('E'(f(z), f(suc(z)))),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_347, clause_359])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_349, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 3.72/3.93       ~ iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(f(z), f(suc(z))))],
% 3.72/3.93                [refute_0_348, refute_0_298])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_350, plain,
% 3.72/3.93      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) |
% 3.72/3.93       ~ iLEQ(suc(z), suc(z))),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(z)))],
% 3.72/3.93                [refute_0_332, refute_0_349])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_351, plain, (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z)))),
% 3.72/3.93      inference(resolve, [$cnf(iLEQ(suc(z), suc(z)))],
% 3.72/3.93                [refute_0_344, refute_0_350])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_352, plain, (~ 'E'(0, f(suc(z))) | 'LE'(f(z), 0)),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(suc(suc(z)))))],
% 3.72/3.93                [refute_0_297, refute_0_351])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_353, plain, (~ 'E'(0, f(suc(z)))),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_352, clause_359])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_354, plain, ('LE'(f(z), 0)),
% 3.72/3.93      inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 3.72/3.93                [refute_0_269, refute_0_353])).
% 3.72/3.93  
% 3.72/3.93  cnf(refute_0_355, plain, ($false),
% 3.72/3.93      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_354, clause_359])).
% 3.72/3.93  % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.72/3.93  
%------------------------------------------------------------------------------