Metis---2.4.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SYO688-1 : TPTP v8.1.0. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n019.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:53 EDT 2022

% Result   : Unsatisfiable 5.54s 5.72s
% Output   : CNFRefutation 5.57s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SYO688-1 : TPTP v8.1.0. Released v7.3.0.
% 0.03/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n019.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Sat Jul  9 09:52:53 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 5.54/5.72  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.54/5.72  
% 5.54/5.72  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.57/5.74  cnf(clause_299, axiom, ('LE'(f(A), s(s(s(s(s(0)))))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_743, axiom,
% 5.57/5.74      (~ iLEQ(suc(A_5), suc(B_94)) | ~ 'E'(0, f(A_5)) |
% 5.57/5.74       ~ 'E'(0, f(suc(B_94))) | ~ 'E'(0, f(suc(suc(B_94)))) |
% 5.57/5.74       ~ 'E'(0, f(suc(suc(B_95)))) | ~ 'E'(0, f(suc(A_5))) |
% 5.57/5.74       ~ 'E'(0, f(suc(suc(A_5)))) | ~ 'E'(f(B_95), f(suc(B_95))) |
% 5.57/5.74       ~ 'E'(f(B_94), f(suc(B_94))) | ~ 'E'(f(A_5), f(suc(A_5))) |
% 5.57/5.74       ~ iLEQ(suc(B_94), suc(B_95)) | ~ 'E'(0, f(B_94)) |
% 5.57/5.74       ~ 'E'(0, f(suc(B_95))) | ~ 'E'(0, f(B_95)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_773, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(B_74)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(B_74))) |
% 5.57/5.74       'LE'(f(B_74), s(s(0))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_1123, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(suc(B_56))), s(s(s(s(0))))) |
% 5.57/5.74       'E'(s(s(s(0))), f(suc(suc(B_56)))) | 'LE'(f(B_56), s(s(s(0)))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_171, axiom,
% 5.57/5.74      (~ 'E'(s(s(s(0))), f(A_2)) | ~ 'E'(s(s(s(0))), f(suc(A_2))) |
% 5.57/5.74       'E'(f(A_2), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_1158, axiom,
% 5.57/5.74      (~ 'LE'(f(B_86), s(s(0))) | 'E'(s(0), f(B_86)) | 'LE'(f(B_86), s(0)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_269, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(B_56)), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(suc(B_56))) |
% 5.57/5.74       'LE'(f(B_56), s(s(s(0)))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_1023, axiom,
% 5.57/5.74      (~ 'E'(s(s(s(0))), f(suc(suc(A_2)))) | ~ 'E'(s(s(s(0))), f(suc(A_2))) |
% 5.57/5.74       ~ 'E'(f(A_2), f(suc(A_2))) | ~ 'E'(s(s(s(0))), f(A_2)) |
% 5.57/5.74       iLEQ(suc(A_2), suc(A_2)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_199, axiom,
% 5.57/5.74      (~ 'LE'(f(B_93), s(0)) | 'E'(0, f(B_93)) | 'LE'(f(B_93), 0))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_237, axiom,
% 5.57/5.74      (~ 'E'(s(s(0)), f(suc(suc(A_3)))) | ~ 'E'(s(s(0)), f(suc(A_3))) |
% 5.57/5.74       ~ 'E'(f(A_3), f(suc(A_3))) | ~ 'E'(s(s(0)), f(A_3)) |
% 5.57/5.74       iLEQ(suc(A_3), suc(A_3)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_340, axiom,
% 5.57/5.74      (~ 'E'(s(0), f(suc(suc(A_4)))) | ~ 'E'(s(0), f(suc(A_4))) |
% 5.57/5.74       ~ 'E'(f(A_4), f(suc(A_4))) | ~ 'E'(s(0), f(A_4)) |
% 5.57/5.74       iLEQ(suc(A_4), suc(A_4)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_546, axiom, (~ 'LE'(f(z), 0))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_813, axiom,
% 5.57/5.74      (~ 'E'(s(0), f(B_88)) | ~ 'E'(f(A_4), f(suc(A_4))) |
% 5.57/5.74       ~ 'E'(s(0), f(suc(B_88))) | ~ 'E'(s(0), f(suc(suc(A_4)))) |
% 5.57/5.74       ~ 'E'(s(0), f(suc(suc(B_87)))) | ~ 'E'(f(B_87), f(suc(B_87))) |
% 5.57/5.74       ~ 'E'(f(B_88), f(suc(B_88))) | ~ 'E'(s(0), f(suc(B_87))) |
% 5.57/5.74       ~ 'E'(s(0), f(B_87)) | ~ iLEQ(suc(B_87), suc(B_88)) |
% 5.57/5.74       ~ 'E'(s(0), f(suc(A_4))) | ~ 'E'(s(0), f(suc(suc(B_88)))) |
% 5.57/5.74       ~ 'E'(s(0), f(A_4)) | ~ iLEQ(suc(A_4), suc(B_87)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_436, axiom,
% 5.57/5.74      (~ 'E'(s(s(s(s(0)))), f(suc(suc(B_33)))) |
% 5.57/5.74       ~ 'E'(s(s(s(s(0)))), f(suc(suc(A_1)))) |
% 5.57/5.74       ~ 'E'(f(B_32), f(suc(B_32))) | ~ iLEQ(suc(B_32), suc(B_33)) |
% 5.57/5.74       ~ 'E'(f(B_33), f(suc(B_33))) | ~ 'E'(s(s(s(s(0)))), f(suc(A_1))) |
% 5.57/5.74       ~ 'E'(s(s(s(s(0)))), f(B_33)) | ~ 'E'(s(s(s(s(0)))), f(suc(B_32))) |
% 5.57/5.74       ~ 'E'(f(A_1), f(suc(A_1))) | ~ 'E'(s(s(s(s(0)))), f(suc(suc(B_32)))) |
% 5.57/5.74       ~ iLEQ(suc(A_1), suc(B_32)) | ~ 'E'(s(s(s(s(0)))), f(A_1)) |
% 5.57/5.74       ~ 'E'(s(s(s(s(0)))), f(B_32)) | ~ 'E'(s(s(s(s(0)))), f(suc(B_33))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_473, axiom,
% 5.57/5.74      (~ 'E'(s(s(s(s(0)))), f(suc(suc(A_1)))) |
% 5.57/5.74       ~ 'E'(s(s(s(s(0)))), f(suc(A_1))) | ~ 'E'(f(A_1), f(suc(A_1))) |
% 5.57/5.74       ~ 'E'(s(s(s(s(0)))), f(A_1)) | iLEQ(suc(A_1), suc(A_1)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_1143, axiom,
% 5.57/5.74      (~ 'LE'(f(B_74), s(s(s(0)))) | 'E'(s(s(0)), f(B_74)) |
% 5.57/5.74       'LE'(f(B_74), s(s(0))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_160, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(suc(B_86))), s(s(0))) | 'E'(s(0), f(suc(suc(B_86)))) |
% 5.57/5.74       'LE'(f(B_86), s(0)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_231, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(suc(B_31))), s(s(s(s(s(0)))))) |
% 5.57/5.74       'E'(s(s(s(s(0)))), f(suc(suc(B_31)))) |
% 5.57/5.74       'LE'(f(B_31), s(s(s(s(0))))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_106, axiom,
% 5.57/5.74      (~ 'E'(0, f(A_5)) | ~ 'E'(0, f(suc(A_5))) | 'E'(f(A_5), f(suc(A_5))) |
% 5.57/5.74       iLEQ(suc(A_5), suc(A_5)))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_778, axiom,
% 5.57/5.74      (~ 'E'(s(s(0)), f(suc(B_75))) | ~ 'E'(s(s(0)), f(suc(A_3))) |
% 5.57/5.74       ~ 'E'(s(s(0)), f(suc(B_76))) | ~ 'E'(s(s(0)), f(B_76)) |
% 5.57/5.74       ~ iLEQ(suc(B_75), suc(B_76)) | ~ iLEQ(suc(A_3), suc(B_75)) |
% 5.57/5.74       ~ 'E'(s(s(0)), f(B_75)) | ~ 'E'(s(s(0)), f(A_3)) |
% 5.57/5.74       'E'(f(A_3), f(suc(A_3))) | 'E'(f(B_75), f(suc(B_75))) |
% 5.57/5.74       'E'(f(B_76), f(suc(B_76))))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_840, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(suc(B_93))), s(0)) | 'E'(0, f(suc(suc(B_93)))) |
% 5.57/5.74       'LE'(f(B_93), 0))).
% 5.57/5.74  
% 5.57/5.74  cnf(clause_149, axiom,
% 5.57/5.74      (~ 'LE'(f(suc(B_86)), s(s(0))) | 'E'(s(0), f(suc(B_86))) |
% 5.57/5.74       'LE'(f(B_86), s(0)))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_256, axiom,
% 5.57/5.75      (~ 'E'(0, f(suc(suc(A_5)))) | ~ 'E'(0, f(suc(A_5))) |
% 5.57/5.75       ~ 'E'(f(A_5), f(suc(A_5))) | ~ 'E'(0, f(A_5)) |
% 5.57/5.75       iLEQ(suc(A_5), suc(A_5)))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_694, axiom,
% 5.57/5.75      (~ 'E'(s(0), f(B_88)) | ~ 'E'(s(0), f(suc(B_88))) |
% 5.57/5.75       ~ 'E'(s(0), f(suc(B_87))) | ~ 'E'(s(0), f(B_87)) |
% 5.57/5.75       ~ iLEQ(suc(B_87), suc(B_88)) | ~ 'E'(s(0), f(suc(A_4))) |
% 5.57/5.75       ~ 'E'(s(0), f(A_4)) | ~ iLEQ(suc(A_4), suc(B_87)) |
% 5.57/5.75       'E'(f(A_4), f(suc(A_4))) | 'E'(f(B_87), f(suc(B_87))) |
% 5.57/5.75       'E'(f(B_88), f(suc(B_88))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_105, axiom,
% 5.57/5.75      (~ iLEQ(suc(B_32), suc(B_33)) | ~ 'E'(s(s(s(s(0)))), f(suc(A_1))) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(B_33)) | ~ 'E'(s(s(s(s(0)))), f(suc(B_32))) |
% 5.57/5.75       ~ iLEQ(suc(A_1), suc(B_32)) | ~ 'E'(s(s(s(s(0)))), f(A_1)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(B_32)) | ~ 'E'(s(s(s(s(0)))), f(suc(B_33))) |
% 5.57/5.75       'E'(f(A_1), f(suc(A_1))) | 'E'(f(B_32), f(suc(B_32))) |
% 5.57/5.75       'E'(f(B_33), f(suc(B_33))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_1089, axiom,
% 5.57/5.75      (~ 'E'(s(0), f(A_4)) | ~ 'E'(s(0), f(suc(A_4))) |
% 5.57/5.75       'E'(f(A_4), f(suc(A_4))) | iLEQ(suc(A_4), suc(A_4)))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_298, axiom,
% 5.57/5.75      (~ 'LE'(f(B_31), s(s(s(s(s(0)))))) | 'E'(s(s(s(s(0)))), f(B_31)) |
% 5.57/5.75       'LE'(f(B_31), s(s(s(s(0))))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_569, axiom,
% 5.57/5.75      (~ 'LE'(f(suc(suc(B_74))), s(s(s(0)))) |
% 5.57/5.75       'E'(s(s(0)), f(suc(suc(B_74)))) | 'LE'(f(B_74), s(s(0))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_1016, axiom,
% 5.57/5.75      (~ 'E'(s(s(s(0))), f(suc(suc(B_58)))) | ~ iLEQ(suc(A_2), suc(B_57)) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(B_57)) | ~ 'E'(s(s(s(0))), f(suc(A_2))) |
% 5.57/5.75       ~ iLEQ(suc(B_57), suc(B_58)) | ~ 'E'(s(s(s(0))), f(A_2)) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(suc(B_57))) | ~ 'E'(f(B_58), f(suc(B_58))) |
% 5.57/5.75       ~ 'E'(f(B_57), f(suc(B_57))) | ~ 'E'(s(s(s(0))), f(B_58)) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(suc(B_58))) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(suc(suc(A_2)))) | ~ 'E'(f(A_2), f(suc(A_2))) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(suc(suc(B_57)))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_794, axiom,
% 5.57/5.75      (~ 'E'(s(s(0)), f(A_3)) | ~ 'E'(s(s(0)), f(suc(A_3))) |
% 5.57/5.75       'E'(f(A_3), f(suc(A_3))) | iLEQ(suc(A_3), suc(A_3)))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_115, axiom,
% 5.57/5.75      (~ 'E'(s(s(0)), f(suc(B_75))) | ~ 'E'(s(s(0)), f(suc(A_3))) |
% 5.57/5.75       ~ 'E'(s(s(0)), f(suc(B_76))) | ~ 'E'(f(B_76), f(suc(B_76))) |
% 5.57/5.75       ~ 'E'(s(s(0)), f(B_76)) | ~ 'E'(s(s(0)), f(suc(suc(A_3)))) |
% 5.57/5.75       ~ iLEQ(suc(B_75), suc(B_76)) | ~ 'E'(s(s(0)), f(suc(suc(B_76)))) |
% 5.57/5.75       ~ 'E'(f(A_3), f(suc(A_3))) | ~ 'E'(s(s(0)), f(suc(suc(B_75)))) |
% 5.57/5.75       ~ iLEQ(suc(A_3), suc(B_75)) | ~ 'E'(s(s(0)), f(B_75)) |
% 5.57/5.75       ~ 'E'(f(B_75), f(suc(B_75))) | ~ 'E'(s(s(0)), f(A_3)))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_303, axiom,
% 5.57/5.75      (~ iLEQ(suc(A_5), suc(B_94)) | ~ 'E'(0, f(A_5)) |
% 5.57/5.75       ~ 'E'(0, f(suc(B_94))) | ~ 'E'(0, f(suc(A_5))) |
% 5.57/5.75       ~ iLEQ(suc(B_94), suc(B_95)) | ~ 'E'(0, f(B_94)) |
% 5.57/5.75       ~ 'E'(0, f(suc(B_95))) | ~ 'E'(0, f(B_95)) |
% 5.57/5.75       'E'(f(A_5), f(suc(A_5))) | 'E'(f(B_94), f(suc(B_94))) |
% 5.57/5.75       'E'(f(B_95), f(suc(B_95))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_24, axiom,
% 5.57/5.75      (~ 'LE'(f(B_56), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(B_56)) |
% 5.57/5.75       'LE'(f(B_56), s(s(s(0)))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_713, axiom,
% 5.57/5.75      (~ 'LE'(f(suc(B_93)), s(0)) | 'E'(0, f(suc(B_93))) |
% 5.57/5.75       'LE'(f(B_93), 0))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_698, axiom,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(A_1)) | ~ 'E'(s(s(s(s(0)))), f(suc(A_1))) |
% 5.57/5.75       'E'(f(A_1), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_297, axiom,
% 5.57/5.75      (~ 'LE'(f(suc(B_31)), s(s(s(s(s(0)))))) |
% 5.57/5.75       'E'(s(s(s(s(0)))), f(suc(B_31))) | 'LE'(f(B_31), s(s(s(s(0))))))).
% 5.57/5.75  
% 5.57/5.75  cnf(clause_249, axiom,
% 5.57/5.75      (~ iLEQ(suc(A_2), suc(B_57)) | ~ 'E'(s(s(s(0))), f(B_57)) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(suc(A_2))) | ~ iLEQ(suc(B_57), suc(B_58)) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(A_2)) | ~ 'E'(s(s(s(0))), f(suc(B_57))) |
% 5.57/5.75       ~ 'E'(s(s(s(0))), f(B_58)) | ~ 'E'(s(s(s(0))), f(suc(B_58))) |
% 5.57/5.75       'E'(f(A_2), f(suc(A_2))) | 'E'(f(B_57), f(suc(B_57))) |
% 5.57/5.75       'E'(f(B_58), f(suc(B_58))))).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_0, plain,
% 5.57/5.75      (~ 'LE'(f(suc(X_735)), s(0)) | 'E'(0, f(suc(X_735))) |
% 5.57/5.75       'LE'(f(X_735), 0)),
% 5.57/5.75      inference(subst, [], [clause_713 : [bind(B_93, $fot(X_735))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_1, plain,
% 5.57/5.75      (~ 'LE'(f(X_360), s(s(0))) | 'E'(s(0), f(X_360)) |
% 5.57/5.75       'LE'(f(X_360), s(0))),
% 5.57/5.75      inference(subst, [], [clause_1158 : [bind(B_86, $fot(X_360))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_2, plain,
% 5.57/5.75      (~ 'LE'(f(X_355), s(s(0))) | 'E'(s(0), f(X_355)) |
% 5.57/5.75       'LE'(f(X_355), s(0))),
% 5.57/5.75      inference(subst, [], [clause_1158 : [bind(B_86, $fot(X_355))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_3, plain,
% 5.57/5.75      (~ 'LE'(f(X_206), s(s(0))) | 'E'(s(0), f(X_206)) |
% 5.57/5.75       'LE'(f(X_206), s(0))),
% 5.57/5.75      inference(subst, [], [clause_1158 : [bind(B_86, $fot(X_206))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_4, plain,
% 5.57/5.75      (~ 'LE'(f(X_205), s(s(s(0)))) | 'E'(s(s(0)), f(X_205)) |
% 5.57/5.75       'LE'(f(X_205), s(s(0)))),
% 5.57/5.75      inference(subst, [], [clause_1143 : [bind(B_74, $fot(X_205))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_5, plain,
% 5.57/5.75      (~ 'LE'(f(X_198), s(s(s(0)))) | 'E'(s(s(0)), f(X_198)) |
% 5.57/5.75       'LE'(f(X_198), s(s(0)))),
% 5.57/5.75      inference(subst, [], [clause_1143 : [bind(B_74, $fot(X_198))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_6, plain,
% 5.57/5.75      (~ 'LE'(f(X_142), s(s(s(0)))) | 'E'(s(s(0)), f(X_142)) |
% 5.57/5.75       'LE'(f(X_142), s(s(0)))),
% 5.57/5.75      inference(subst, [], [clause_1143 : [bind(B_74, $fot(X_142))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_7, plain,
% 5.57/5.75      (~ 'LE'(f(X_111), s(s(s(0)))) | 'E'(s(s(0)), f(X_111)) |
% 5.57/5.75       'LE'(f(X_111), s(s(0)))),
% 5.57/5.75      inference(subst, [], [clause_1143 : [bind(B_74, $fot(X_111))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_8, plain,
% 5.57/5.75      (~ 'LE'(f(X_110), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(X_110)) |
% 5.57/5.75       'LE'(f(X_110), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_24 : [bind(B_56, $fot(X_110))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_9, plain,
% 5.57/5.75      (~ 'LE'(f(X_104), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(X_104)) |
% 5.57/5.75       'LE'(f(X_104), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_24 : [bind(B_56, $fot(X_104))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_10, plain, ('LE'(f(B_31), s(s(s(s(s(0))))))),
% 5.57/5.75      inference(subst, [], [clause_299 : [bind(A, $fot(B_31))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_11, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(B_31)) | 'LE'(f(B_31), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(B_31), s(s(s(s(s(0)))))))],
% 5.57/5.75                [refute_0_10, clause_298])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_12, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(X_11)) | 'LE'(f(X_11), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_11 : [bind(B_31, $fot(X_11))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_13, plain,
% 5.57/5.75      (~ 'LE'(f(X_11), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(X_11)) |
% 5.57/5.75       'LE'(f(X_11), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_24 : [bind(B_56, $fot(X_11))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_14, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_11)) | 'E'(s(s(s(s(0)))), f(X_11)) |
% 5.57/5.75       'LE'(f(X_11), s(s(s(0))))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(X_11), s(s(s(s(0))))))],
% 5.57/5.75                [refute_0_12, refute_0_13])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_15, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_103)) | 'E'(s(s(s(s(0)))), f(X_103)) |
% 5.57/5.75       'LE'(f(X_103), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [refute_0_14 : [bind(X_11, $fot(X_103))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_16, plain,
% 5.57/5.75      (~ 'LE'(f(X_59), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(X_59)) |
% 5.57/5.75       'LE'(f(X_59), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_24 : [bind(B_56, $fot(X_59))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_17, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_29)) | 'E'(s(s(s(s(0)))), f(X_29)) |
% 5.57/5.75       'LE'(f(X_29), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [refute_0_14 : [bind(X_11, $fot(X_29))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_18, plain, ('LE'(f(suc(B_31)), s(s(s(s(s(0))))))),
% 5.57/5.75      inference(subst, [], [clause_299 : [bind(A, $fot(suc(B_31)))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_19, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(B_31))) | 'LE'(f(B_31), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(suc(B_31)), s(s(s(s(s(0)))))))],
% 5.57/5.75                [refute_0_18, clause_297])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_20, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(X_26))) | 'LE'(f(X_26), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_19 : [bind(B_31, $fot(X_26))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_21, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_26)) | ~ 'E'(s(s(s(s(0)))), f(suc(X_26))) |
% 5.57/5.75       'E'(f(X_26), f(suc(X_26))) | iLEQ(suc(X_26), suc(X_26))),
% 5.57/5.75      inference(subst, [], [clause_698 : [bind(A_1, $fot(X_26))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_22, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_26)) | 'E'(f(X_26), f(suc(X_26))) |
% 5.57/5.75       'LE'(f(X_26), s(s(s(s(0))))) | iLEQ(suc(X_26), suc(X_26))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_26))))],
% 5.57/5.75                [refute_0_20, refute_0_21])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_23, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_29)) | 'E'(f(X_29), f(suc(X_29))) |
% 5.57/5.75       'LE'(f(X_29), s(s(s(s(0))))) | iLEQ(suc(X_29), suc(X_29))),
% 5.57/5.75      inference(subst, [], [refute_0_22 : [bind(X_26, $fot(X_29))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_24, plain,
% 5.57/5.75      ('E'(f(X_29), f(suc(X_29))) | 'E'(s(s(s(0))), f(X_29)) |
% 5.57/5.75       'LE'(f(X_29), s(s(s(0)))) | 'LE'(f(X_29), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(X_29), suc(X_29))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(X_29)))],
% 5.57/5.75                [refute_0_17, refute_0_23])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_25, plain,
% 5.57/5.75      ('E'(f(X_59), f(suc(X_59))) | 'E'(s(s(s(0))), f(X_59)) |
% 5.57/5.75       'LE'(f(X_59), s(s(s(0)))) | 'LE'(f(X_59), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(X_59), suc(X_59))),
% 5.57/5.75      inference(subst, [], [refute_0_24 : [bind(X_29, $fot(X_59))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_26, plain,
% 5.57/5.75      ('E'(f(X_59), f(suc(X_59))) | 'E'(s(s(s(0))), f(X_59)) |
% 5.57/5.75       'LE'(f(X_59), s(s(s(0)))) | iLEQ(suc(X_59), suc(X_59))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(X_59), s(s(s(s(0))))))],
% 5.57/5.75                [refute_0_25, refute_0_16])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_27, plain,
% 5.57/5.75      ('E'(f(X_70), f(suc(X_70))) | 'E'(s(s(s(0))), f(X_70)) |
% 5.57/5.75       'LE'(f(X_70), s(s(s(0)))) | iLEQ(suc(X_70), suc(X_70))),
% 5.57/5.75      inference(subst, [], [refute_0_26 : [bind(X_59, $fot(X_70))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_28, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(X_69))) | 'LE'(f(X_69), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_19 : [bind(B_31, $fot(X_69))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_29, plain, ('LE'(f(suc(suc(B_31))), s(s(s(s(s(0))))))),
% 5.57/5.75      inference(subst, [], [clause_299 : [bind(A, $fot(suc(suc(B_31))))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_30, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(suc(B_31)))) | 'LE'(f(B_31), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(suc(suc(B_31))), s(s(s(s(s(0)))))))],
% 5.57/5.75                [refute_0_29, clause_231])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_31, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(suc(X_50)))) | 'LE'(f(X_50), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_30 : [bind(B_31, $fot(X_50))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_32, plain,
% 5.57/5.75      (~ 'E'(f(X_50), f(suc(X_50))) | ~ 'E'(s(s(s(s(0)))), f(X_50)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_50))) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(suc(X_50)))) | iLEQ(suc(X_50), suc(X_50))),
% 5.57/5.75      inference(subst, [], [clause_473 : [bind(A_1, $fot(X_50))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_33, plain,
% 5.57/5.75      (~ 'E'(f(X_50), f(suc(X_50))) | ~ 'E'(s(s(s(s(0)))), f(X_50)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_50))) | 'LE'(f(X_50), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(X_50), suc(X_50))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(suc(X_50)))))],
% 5.57/5.75                [refute_0_31, refute_0_32])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_34, plain,
% 5.57/5.75      (~ 'E'(f(X_69), f(suc(X_69))) | ~ 'E'(s(s(s(s(0)))), f(X_69)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_69))) | 'LE'(f(X_69), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(X_69), suc(X_69))),
% 5.57/5.75      inference(subst, [], [refute_0_33 : [bind(X_50, $fot(X_69))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_35, plain,
% 5.57/5.75      (~ 'E'(f(X_69), f(suc(X_69))) | ~ 'E'(s(s(s(s(0)))), f(X_69)) |
% 5.57/5.75       'LE'(f(X_69), s(s(s(s(0))))) | iLEQ(suc(X_69), suc(X_69))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_69))))],
% 5.57/5.75                [refute_0_28, refute_0_34])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_36, plain,
% 5.57/5.75      (~ 'E'(f(X_70), f(suc(X_70))) | ~ 'E'(s(s(s(s(0)))), f(X_70)) |
% 5.57/5.75       'LE'(f(X_70), s(s(s(s(0))))) | iLEQ(suc(X_70), suc(X_70))),
% 5.57/5.75      inference(subst, [], [refute_0_35 : [bind(X_69, $fot(X_70))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_37, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_70)) | 'E'(s(s(s(0))), f(X_70)) |
% 5.57/5.75       'LE'(f(X_70), s(s(s(0)))) | 'LE'(f(X_70), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(X_70), suc(X_70))),
% 5.57/5.75      inference(resolve, [$cnf('E'(f(X_70), f(suc(X_70))))],
% 5.57/5.75                [refute_0_27, refute_0_36])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_38, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_103)) | 'E'(s(s(s(0))), f(X_103)) |
% 5.57/5.75       'LE'(f(X_103), s(s(s(0)))) | 'LE'(f(X_103), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(X_103), suc(X_103))),
% 5.57/5.75      inference(subst, [], [refute_0_37 : [bind(X_70, $fot(X_103))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_39, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_103)) | 'LE'(f(X_103), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_103), s(s(s(s(0))))) | iLEQ(suc(X_103), suc(X_103))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(X_103)))],
% 5.57/5.75                [refute_0_15, refute_0_38])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_40, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_104)) | 'LE'(f(X_104), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_104), s(s(s(s(0))))) | iLEQ(suc(X_104), suc(X_104))),
% 5.57/5.75      inference(subst, [], [refute_0_39 : [bind(X_103, $fot(X_104))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_41, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_104)) | 'LE'(f(X_104), s(s(s(0)))) |
% 5.57/5.75       iLEQ(suc(X_104), suc(X_104))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(X_104), s(s(s(s(0))))))],
% 5.57/5.75                [refute_0_40, refute_0_9])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_42, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_109)) | 'LE'(f(X_109), s(s(s(0)))) |
% 5.57/5.75       iLEQ(suc(X_109), suc(X_109))),
% 5.57/5.75      inference(subst, [], [refute_0_41 : [bind(X_104, $fot(X_109))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_43, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_64)) | 'E'(s(s(s(s(0)))), f(X_64)) |
% 5.57/5.75       'LE'(f(X_64), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [refute_0_14 : [bind(X_11, $fot(X_64))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_44, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(X_63))) | 'LE'(f(X_63), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_19 : [bind(B_31, $fot(X_63))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_45, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(suc(X_51)))) | 'LE'(f(X_51), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_30 : [bind(B_31, $fot(X_51))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_46, plain,
% 5.57/5.75      (~ 'E'(f(X_51), f(suc(X_51))) | ~ 'E'(s(s(s(s(0)))), f(X_51)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_51))) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(suc(X_51)))) |
% 5.57/5.75       ~ iLEQ(suc(X_51), suc(X_51))),
% 5.57/5.75      inference(subst, [],
% 5.57/5.75                [clause_436 :
% 5.57/5.75                 [bind(A_1, $fot(X_51)), bind(B_32, $fot(X_51)),
% 5.57/5.75                  bind(B_33, $fot(X_51))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_47, plain,
% 5.57/5.75      (~ 'E'(f(X_51), f(suc(X_51))) | ~ 'E'(s(s(s(s(0)))), f(X_51)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_51))) | ~ iLEQ(suc(X_51), suc(X_51)) |
% 5.57/5.75       'LE'(f(X_51), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(suc(X_51)))))],
% 5.57/5.75                [refute_0_45, refute_0_46])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_48, plain,
% 5.57/5.75      (~ 'E'(f(X_63), f(suc(X_63))) | ~ 'E'(s(s(s(s(0)))), f(X_63)) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_63))) | ~ iLEQ(suc(X_63), suc(X_63)) |
% 5.57/5.75       'LE'(f(X_63), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_47 : [bind(X_51, $fot(X_63))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_49, plain,
% 5.57/5.75      (~ 'E'(f(X_63), f(suc(X_63))) | ~ 'E'(s(s(s(s(0)))), f(X_63)) |
% 5.57/5.75       ~ iLEQ(suc(X_63), suc(X_63)) | 'LE'(f(X_63), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_63))))],
% 5.57/5.75                [refute_0_44, refute_0_48])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_50, plain,
% 5.57/5.75      (~ 'E'(f(X_64), f(suc(X_64))) | ~ 'E'(s(s(s(s(0)))), f(X_64)) |
% 5.57/5.75       ~ iLEQ(suc(X_64), suc(X_64)) | 'LE'(f(X_64), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_49 : [bind(X_63, $fot(X_64))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_51, plain,
% 5.57/5.75      (~ 'E'(f(X_64), f(suc(X_64))) | ~ iLEQ(suc(X_64), suc(X_64)) |
% 5.57/5.75       'E'(s(s(s(0))), f(X_64)) | 'LE'(f(X_64), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_64), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(X_64)))],
% 5.57/5.75                [refute_0_43, refute_0_50])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_52, plain,
% 5.57/5.75      (~ 'E'(f(X_106), f(suc(X_106))) | ~ iLEQ(suc(X_106), suc(X_106)) |
% 5.57/5.75       'E'(s(s(s(0))), f(X_106)) | 'LE'(f(X_106), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_106), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_51 : [bind(X_64, $fot(X_106))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_53, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_32)) | 'E'(s(s(s(s(0)))), f(X_32)) |
% 5.57/5.75       'LE'(f(X_32), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [refute_0_14 : [bind(X_11, $fot(X_32))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_54, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(X_28))) | 'LE'(f(X_28), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_19 : [bind(B_31, $fot(X_28))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_55, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_28)) | ~ 'E'(s(s(s(s(0)))), f(suc(X_28))) |
% 5.57/5.75       ~ iLEQ(suc(X_28), suc(X_28)) | 'E'(f(X_28), f(suc(X_28)))),
% 5.57/5.75      inference(subst, [],
% 5.57/5.75                [clause_105 :
% 5.57/5.75                 [bind(A_1, $fot(X_28)), bind(B_32, $fot(X_28)),
% 5.57/5.75                  bind(B_33, $fot(X_28))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_56, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_28)) | ~ iLEQ(suc(X_28), suc(X_28)) |
% 5.57/5.75       'E'(f(X_28), f(suc(X_28))) | 'LE'(f(X_28), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_28))))],
% 5.57/5.75                [refute_0_54, refute_0_55])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_57, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(X_32)) | ~ iLEQ(suc(X_32), suc(X_32)) |
% 5.57/5.75       'E'(f(X_32), f(suc(X_32))) | 'LE'(f(X_32), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_56 : [bind(X_28, $fot(X_32))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_58, plain,
% 5.57/5.75      (~ iLEQ(suc(X_32), suc(X_32)) | 'E'(f(X_32), f(suc(X_32))) |
% 5.57/5.75       'E'(s(s(s(0))), f(X_32)) | 'LE'(f(X_32), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_32), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(X_32)))],
% 5.57/5.75                [refute_0_53, refute_0_57])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_59, plain,
% 5.57/5.75      (~ iLEQ(suc(X_104), suc(X_104)) | 'E'(f(X_104), f(suc(X_104))) |
% 5.57/5.75       'E'(s(s(s(0))), f(X_104)) | 'LE'(f(X_104), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_104), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_58 : [bind(X_32, $fot(X_104))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_60, plain,
% 5.57/5.75      ('E'(f(X_104), f(suc(X_104))) | 'E'(s(s(s(0))), f(X_104)) |
% 5.57/5.75       'LE'(f(X_104), s(s(s(0)))) | 'LE'(f(X_104), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf(iLEQ(suc(X_104), suc(X_104)))],
% 5.57/5.75                [refute_0_40, refute_0_59])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_61, plain,
% 5.57/5.75      ('E'(f(X_106), f(suc(X_106))) | 'E'(s(s(s(0))), f(X_106)) |
% 5.57/5.75       'LE'(f(X_106), s(s(s(0)))) | 'LE'(f(X_106), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_60 : [bind(X_104, $fot(X_106))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_62, plain,
% 5.57/5.75      (~ iLEQ(suc(X_106), suc(X_106)) | 'E'(s(s(s(0))), f(X_106)) |
% 5.57/5.75       'LE'(f(X_106), s(s(s(0)))) | 'LE'(f(X_106), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(f(X_106), f(suc(X_106))))],
% 5.57/5.75                [refute_0_61, refute_0_52])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_63, plain,
% 5.57/5.75      (~ iLEQ(suc(X_109), suc(X_109)) | 'E'(s(s(s(0))), f(X_109)) |
% 5.57/5.75       'LE'(f(X_109), s(s(s(0)))) | 'LE'(f(X_109), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_62 : [bind(X_106, $fot(X_109))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_64, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_109)) | 'LE'(f(X_109), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_109), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf(iLEQ(suc(X_109), suc(X_109)))],
% 5.57/5.75                [refute_0_42, refute_0_63])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_65, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_110)) | 'LE'(f(X_110), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(X_110), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_64 : [bind(X_109, $fot(X_110))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_66, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_110)) | 'LE'(f(X_110), s(s(s(0))))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(X_110), s(s(s(s(0))))))],
% 5.57/5.75                [refute_0_65, refute_0_8])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_67, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(X_111)) | 'LE'(f(X_111), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [refute_0_66 : [bind(X_110, $fot(X_111))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_68, plain,
% 5.57/5.75      ('E'(s(s(0)), f(X_111)) | 'E'(s(s(s(0))), f(X_111)) |
% 5.57/5.75       'LE'(f(X_111), s(s(0)))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(X_111), s(s(s(0)))))],
% 5.57/5.75                [refute_0_67, refute_0_7])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_69, plain,
% 5.57/5.75      ('E'(s(s(0)), f(X_127)) | 'E'(s(s(s(0))), f(X_127)) |
% 5.57/5.75       'LE'(f(X_127), s(s(0)))),
% 5.57/5.75      inference(subst, [], [refute_0_68 : [bind(X_111, $fot(X_127))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_70, plain,
% 5.57/5.75      (~ 'E'(s(s(s(0))), f(X_125)) | ~ 'E'(s(s(s(0))), f(suc(X_125))) |
% 5.57/5.75       'E'(f(X_125), f(suc(X_125))) | iLEQ(suc(X_125), suc(X_125))),
% 5.57/5.75      inference(subst, [], [clause_171 : [bind(A_2, $fot(X_125))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_71, plain,
% 5.57/5.75      (~ 'LE'(f(suc(X_124)), s(s(s(s(0))))) |
% 5.57/5.75       'E'(s(s(s(0))), f(suc(X_124))) | 'LE'(f(X_124), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_269 : [bind(B_56, $fot(X_124))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_72, plain,
% 5.57/5.75      (~ 'LE'(f(suc(X_119)), s(s(s(s(0))))) |
% 5.57/5.75       'E'(s(s(s(0))), f(suc(X_119))) | 'LE'(f(X_119), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_269 : [bind(B_56, $fot(X_119))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_73, plain,
% 5.57/5.75      ('E'(s(s(s(s(0)))), f(suc(X_16))) | 'LE'(f(suc(X_16)), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_11 : [bind(B_31, $fot(suc(X_16)))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_74, plain,
% 5.57/5.75      (~ 'LE'(f(suc(X_16)), s(s(s(s(0))))) | 'E'(s(s(s(0))), f(suc(X_16))) |
% 5.57/5.75       'LE'(f(X_16), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [clause_269 : [bind(B_56, $fot(X_16))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_75, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(suc(X_16))) | 'E'(s(s(s(s(0)))), f(suc(X_16))) |
% 5.57/5.75       'LE'(f(X_16), s(s(s(0))))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(suc(X_16)), s(s(s(s(0))))))],
% 5.57/5.75                [refute_0_73, refute_0_74])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_76, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(suc(X_118))) | 'E'(s(s(s(s(0)))), f(suc(X_118))) |
% 5.57/5.75       'LE'(f(X_118), s(s(s(0))))),
% 5.57/5.75      inference(subst, [], [refute_0_75 : [bind(X_16, $fot(X_118))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_77, plain,
% 5.57/5.75      (~ 'E'(f(suc(X_94)), f(suc(suc(X_94)))) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_94))) |
% 5.57/5.75       'LE'(f(suc(X_94)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_94)), suc(suc(X_94)))),
% 5.57/5.75      inference(subst, [], [refute_0_35 : [bind(X_69, $fot(suc(X_94)))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_78, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(suc(X_16))) |
% 5.57/5.75       'E'(f(suc(X_16)), f(suc(suc(X_16)))) |
% 5.57/5.75       'LE'(f(suc(X_16)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_16)), suc(suc(X_16)))),
% 5.57/5.75      inference(subst, [], [refute_0_22 : [bind(X_26, $fot(suc(X_16)))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_79, plain,
% 5.57/5.75      ('E'(f(suc(X_16)), f(suc(suc(X_16)))) | 'E'(s(s(s(0))), f(suc(X_16))) |
% 5.57/5.75       'LE'(f(X_16), s(s(s(0)))) | 'LE'(f(suc(X_16)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_16)), suc(suc(X_16)))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_16))))],
% 5.57/5.75                [refute_0_75, refute_0_78])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_80, plain,
% 5.57/5.75      ('E'(f(suc(X_94)), f(suc(suc(X_94)))) | 'E'(s(s(s(0))), f(suc(X_94))) |
% 5.57/5.75       'LE'(f(X_94), s(s(s(0)))) | 'LE'(f(suc(X_94)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_94)), suc(suc(X_94)))),
% 5.57/5.75      inference(subst, [], [refute_0_79 : [bind(X_16, $fot(X_94))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_81, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(suc(X_94))) | 'E'(s(s(s(0))), f(suc(X_94))) |
% 5.57/5.75       'LE'(f(X_94), s(s(s(0)))) | 'LE'(f(suc(X_94)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_94)), suc(suc(X_94)))),
% 5.57/5.75      inference(resolve, [$cnf('E'(f(suc(X_94)), f(suc(suc(X_94)))))],
% 5.57/5.75                [refute_0_80, refute_0_77])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_82, plain,
% 5.57/5.75      (~ 'E'(s(s(s(s(0)))), f(suc(X_118))) | 'E'(s(s(s(0))), f(suc(X_118))) |
% 5.57/5.75       'LE'(f(X_118), s(s(s(0)))) | 'LE'(f(suc(X_118)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_118)), suc(suc(X_118)))),
% 5.57/5.75      inference(subst, [], [refute_0_81 : [bind(X_94, $fot(X_118))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_83, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(suc(X_118))) | 'LE'(f(X_118), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(suc(X_118)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_118)), suc(suc(X_118)))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_118))))],
% 5.57/5.75                [refute_0_76, refute_0_82])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_84, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(suc(X_119))) | 'LE'(f(X_119), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(suc(X_119)), s(s(s(s(0))))) |
% 5.57/5.75       iLEQ(suc(suc(X_119)), suc(suc(X_119)))),
% 5.57/5.75      inference(subst, [], [refute_0_83 : [bind(X_118, $fot(X_119))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_85, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(suc(X_119))) | 'LE'(f(X_119), s(s(s(0)))) |
% 5.57/5.75       iLEQ(suc(suc(X_119)), suc(suc(X_119)))),
% 5.57/5.75      inference(resolve, [$cnf('LE'(f(suc(X_119)), s(s(s(s(0))))))],
% 5.57/5.75                [refute_0_84, refute_0_72])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_86, plain,
% 5.57/5.75      ('E'(s(s(s(0))), f(suc(X_123))) | 'LE'(f(X_123), s(s(s(0)))) |
% 5.57/5.75       iLEQ(suc(suc(X_123)), suc(suc(X_123)))),
% 5.57/5.75      inference(subst, [], [refute_0_85 : [bind(X_119, $fot(X_123))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_87, plain,
% 5.57/5.75      (~ 'E'(f(suc(X_16)), f(suc(suc(X_16)))) |
% 5.57/5.75       ~ 'E'(s(s(s(s(0)))), f(suc(X_16))) |
% 5.57/5.75       ~ iLEQ(suc(suc(X_16)), suc(suc(X_16))) |
% 5.57/5.75       'LE'(f(suc(X_16)), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_49 : [bind(X_63, $fot(suc(X_16)))]])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_88, plain,
% 5.57/5.75      (~ 'E'(f(suc(X_16)), f(suc(suc(X_16)))) |
% 5.57/5.75       ~ iLEQ(suc(suc(X_16)), suc(suc(X_16))) |
% 5.57/5.75       'E'(s(s(s(0))), f(suc(X_16))) | 'LE'(f(X_16), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(suc(X_16)), s(s(s(s(0)))))),
% 5.57/5.75      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_16))))],
% 5.57/5.75                [refute_0_75, refute_0_87])).
% 5.57/5.75  
% 5.57/5.75  cnf(refute_0_89, plain,
% 5.57/5.75      (~ 'E'(f(suc(X_121)), f(suc(suc(X_121)))) |
% 5.57/5.75       ~ iLEQ(suc(suc(X_121)), suc(suc(X_121))) |
% 5.57/5.75       'E'(s(s(s(0))), f(suc(X_121))) | 'LE'(f(X_121), s(s(s(0)))) |
% 5.57/5.75       'LE'(f(suc(X_121)), s(s(s(s(0)))))),
% 5.57/5.75      inference(subst, [], [refute_0_88 : [bind(X_16, $fot(X_121))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_90, plain,
% 5.57/5.76      (~ 'E'(s(s(s(s(0)))), f(suc(X_16))) |
% 5.57/5.76       ~ iLEQ(suc(suc(X_16)), suc(suc(X_16))) |
% 5.57/5.76       'E'(f(suc(X_16)), f(suc(suc(X_16)))) |
% 5.57/5.76       'LE'(f(suc(X_16)), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_56 : [bind(X_28, $fot(suc(X_16)))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_91, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(X_16)), suc(suc(X_16))) |
% 5.57/5.76       'E'(f(suc(X_16)), f(suc(suc(X_16)))) | 'E'(s(s(s(0))), f(suc(X_16))) |
% 5.57/5.76       'LE'(f(X_16), s(s(s(0)))) | 'LE'(f(suc(X_16)), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(X_16))))],
% 5.57/5.76                [refute_0_75, refute_0_90])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_92, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(X_119)), suc(suc(X_119))) |
% 5.57/5.76       'E'(f(suc(X_119)), f(suc(suc(X_119)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(X_119))) | 'LE'(f(X_119), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_119)), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_91 : [bind(X_16, $fot(X_119))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_93, plain,
% 5.57/5.76      ('E'(f(suc(X_119)), f(suc(suc(X_119)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(X_119))) | 'LE'(f(X_119), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_119)), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve, [$cnf(iLEQ(suc(suc(X_119)), suc(suc(X_119))))],
% 5.57/5.76                [refute_0_84, refute_0_92])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_94, plain,
% 5.57/5.76      ('E'(f(suc(X_121)), f(suc(suc(X_121)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(X_121))) | 'LE'(f(X_121), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_121)), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_93 : [bind(X_119, $fot(X_121))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_95, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(X_121)), suc(suc(X_121))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(X_121))) | 'LE'(f(X_121), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_121)), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(f(suc(X_121)), f(suc(suc(X_121)))))],
% 5.57/5.76                [refute_0_94, refute_0_89])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_96, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(X_123)), suc(suc(X_123))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(X_123))) | 'LE'(f(X_123), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_123)), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_95 : [bind(X_121, $fot(X_123))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_97, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(X_123))) | 'LE'(f(X_123), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_123)), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve, [$cnf(iLEQ(suc(suc(X_123)), suc(suc(X_123))))],
% 5.57/5.76                [refute_0_86, refute_0_96])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_98, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(X_124))) | 'LE'(f(X_124), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(X_124)), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_97 : [bind(X_123, $fot(X_124))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_99, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(X_124))) | 'LE'(f(X_124), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(suc(X_124)), s(s(s(s(0))))))],
% 5.57/5.76                [refute_0_98, refute_0_71])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_100, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(X_125))) | 'LE'(f(X_125), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_99 : [bind(X_124, $fot(X_125))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_101, plain,
% 5.57/5.76      (~ 'E'(s(s(s(0))), f(X_125)) | 'E'(f(X_125), f(suc(X_125))) |
% 5.57/5.76       'LE'(f(X_125), s(s(s(0)))) | iLEQ(suc(X_125), suc(X_125))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_125))))],
% 5.57/5.76                [refute_0_100, refute_0_70])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_102, plain,
% 5.57/5.76      (~ 'E'(s(s(s(0))), f(X_127)) | 'E'(f(X_127), f(suc(X_127))) |
% 5.57/5.76       'LE'(f(X_127), s(s(s(0)))) | iLEQ(suc(X_127), suc(X_127))),
% 5.57/5.76      inference(subst, [], [refute_0_101 : [bind(X_125, $fot(X_127))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_103, plain,
% 5.57/5.76      ('E'(f(X_127), f(suc(X_127))) | 'E'(s(s(0)), f(X_127)) |
% 5.57/5.76       'LE'(f(X_127), s(s(0))) | 'LE'(f(X_127), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(X_127), suc(X_127))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_127)))],
% 5.57/5.76                [refute_0_69, refute_0_102])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_104, plain,
% 5.57/5.76      ('E'(f(X_142), f(suc(X_142))) | 'E'(s(s(0)), f(X_142)) |
% 5.57/5.76       'LE'(f(X_142), s(s(0))) | 'LE'(f(X_142), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(X_142), suc(X_142))),
% 5.57/5.76      inference(subst, [], [refute_0_103 : [bind(X_127, $fot(X_142))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_105, plain,
% 5.57/5.76      ('E'(f(X_142), f(suc(X_142))) | 'E'(s(s(0)), f(X_142)) |
% 5.57/5.76       'LE'(f(X_142), s(s(0))) | iLEQ(suc(X_142), suc(X_142))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(X_142), s(s(s(0)))))],
% 5.57/5.76                [refute_0_104, refute_0_6])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_106, plain,
% 5.57/5.76      ('E'(f(X_197), f(suc(X_197))) | 'E'(s(s(0)), f(X_197)) |
% 5.57/5.76       'LE'(f(X_197), s(s(0))) | iLEQ(suc(X_197), suc(X_197))),
% 5.57/5.76      inference(subst, [], [refute_0_105 : [bind(X_142, $fot(X_197))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_107, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_171)) | 'E'(s(s(s(0))), f(X_171)) |
% 5.57/5.76       'LE'(f(X_171), s(s(0)))),
% 5.57/5.76      inference(subst, [], [refute_0_68 : [bind(X_111, $fot(X_171))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_108, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(X_170))) | 'LE'(f(X_170), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_99 : [bind(X_124, $fot(X_170))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_109, plain,
% 5.57/5.76      (~ 'E'(f(X_159), f(suc(X_159))) | ~ 'E'(s(s(s(0))), f(X_159)) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(X_159))) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(suc(X_159)))) | iLEQ(suc(X_159), suc(X_159))),
% 5.57/5.76      inference(subst, [], [clause_1023 : [bind(A_2, $fot(X_159))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_110, plain,
% 5.57/5.76      (~ 'LE'(f(suc(suc(X_158))), s(s(s(s(0))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_158)))) | 'LE'(f(X_158), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [clause_1123 : [bind(B_56, $fot(X_158))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_111, plain,
% 5.57/5.76      (~ 'LE'(f(suc(suc(X_153))), s(s(s(s(0))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_153)))) | 'LE'(f(X_153), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [clause_1123 : [bind(B_56, $fot(X_153))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_112, plain,
% 5.57/5.76      ('E'(s(s(s(s(0)))), f(suc(suc(X_19)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [refute_0_11 : [bind(B_31, $fot(suc(suc(X_19))))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_113, plain,
% 5.57/5.76      (~ 'LE'(f(suc(suc(X_19))), s(s(s(s(0))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_19)))) | 'LE'(f(X_19), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [clause_1123 : [bind(B_56, $fot(X_19))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_114, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_19)))) |
% 5.57/5.76       'E'(s(s(s(s(0)))), f(suc(suc(X_19)))) | 'LE'(f(X_19), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(suc(suc(X_19))), s(s(s(s(0))))))],
% 5.57/5.76                [refute_0_112, refute_0_113])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_115, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_152)))) |
% 5.57/5.76       'E'(s(s(s(s(0)))), f(suc(suc(X_152)))) | 'LE'(f(X_152), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_114 : [bind(X_19, $fot(X_152))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_116, plain,
% 5.57/5.76      (~ 'E'(f(suc(suc(X_135))), f(suc(suc(suc(X_135))))) |
% 5.57/5.76       ~ 'E'(s(s(s(s(0)))), f(suc(suc(X_135)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_135))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_135))), suc(suc(suc(X_135))))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [refute_0_35 : [bind(X_69, $fot(suc(suc(X_135))))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_117, plain,
% 5.57/5.76      (~ 'E'(s(s(s(s(0)))), f(suc(suc(X_19)))) |
% 5.57/5.76       'E'(f(suc(suc(X_19))), f(suc(suc(suc(X_19))))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_19))), suc(suc(suc(X_19))))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [refute_0_22 : [bind(X_26, $fot(suc(suc(X_19))))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_118, plain,
% 5.57/5.76      ('E'(f(suc(suc(X_19))), f(suc(suc(suc(X_19))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_19)))) | 'LE'(f(X_19), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_19))), suc(suc(suc(X_19))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(suc(X_19)))))],
% 5.57/5.76                [refute_0_114, refute_0_117])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_119, plain,
% 5.57/5.76      ('E'(f(suc(suc(X_135))), f(suc(suc(suc(X_135))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_135)))) | 'LE'(f(X_135), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_135))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_135))), suc(suc(suc(X_135))))),
% 5.57/5.76      inference(subst, [], [refute_0_118 : [bind(X_19, $fot(X_135))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_120, plain,
% 5.57/5.76      (~ 'E'(s(s(s(s(0)))), f(suc(suc(X_135)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_135)))) | 'LE'(f(X_135), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_135))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_135))), suc(suc(suc(X_135))))),
% 5.57/5.76      inference(resolve,
% 5.57/5.76                [$cnf('E'(f(suc(suc(X_135))), f(suc(suc(suc(X_135))))))],
% 5.57/5.76                [refute_0_119, refute_0_116])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_121, plain,
% 5.57/5.76      (~ 'E'(s(s(s(s(0)))), f(suc(suc(X_152)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_152)))) | 'LE'(f(X_152), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_152))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_152))), suc(suc(suc(X_152))))),
% 5.57/5.76      inference(subst, [], [refute_0_120 : [bind(X_135, $fot(X_152))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_122, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_152)))) | 'LE'(f(X_152), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_152))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_152))), suc(suc(suc(X_152))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(suc(X_152)))))],
% 5.57/5.76                [refute_0_115, refute_0_121])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_123, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_153)))) | 'LE'(f(X_153), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_153))), s(s(s(s(0))))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_153))), suc(suc(suc(X_153))))),
% 5.57/5.76      inference(subst, [], [refute_0_122 : [bind(X_152, $fot(X_153))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_124, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_153)))) | 'LE'(f(X_153), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_153))), suc(suc(suc(X_153))))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(suc(suc(X_153))), s(s(s(s(0))))))],
% 5.57/5.76                [refute_0_123, refute_0_111])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_125, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_157)))) | 'LE'(f(X_157), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(suc(suc(X_157))), suc(suc(suc(X_157))))),
% 5.57/5.76      inference(subst, [], [refute_0_124 : [bind(X_153, $fot(X_157))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_126, plain,
% 5.57/5.76      (~ 'E'(f(suc(suc(X_19))), f(suc(suc(suc(X_19))))) |
% 5.57/5.76       ~ 'E'(s(s(s(s(0)))), f(suc(suc(X_19)))) |
% 5.57/5.76       ~ iLEQ(suc(suc(suc(X_19))), suc(suc(suc(X_19)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [refute_0_49 : [bind(X_63, $fot(suc(suc(X_19))))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_127, plain,
% 5.57/5.76      (~ 'E'(f(suc(suc(X_19))), f(suc(suc(suc(X_19))))) |
% 5.57/5.76       ~ iLEQ(suc(suc(suc(X_19))), suc(suc(suc(X_19)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_19)))) | 'LE'(f(X_19), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(suc(X_19)))))],
% 5.57/5.76                [refute_0_114, refute_0_126])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_128, plain,
% 5.57/5.76      (~ 'E'(f(suc(suc(X_155))), f(suc(suc(suc(X_155))))) |
% 5.57/5.76       ~ iLEQ(suc(suc(suc(X_155))), suc(suc(suc(X_155)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_155)))) | 'LE'(f(X_155), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_155))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_127 : [bind(X_19, $fot(X_155))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_129, plain,
% 5.57/5.76      (~ 'E'(s(s(s(s(0)))), f(suc(suc(X_19)))) |
% 5.57/5.76       ~ iLEQ(suc(suc(suc(X_19))), suc(suc(suc(X_19)))) |
% 5.57/5.76       'E'(f(suc(suc(X_19))), f(suc(suc(suc(X_19))))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [refute_0_56 : [bind(X_28, $fot(suc(suc(X_19))))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_130, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(suc(X_19))), suc(suc(suc(X_19)))) |
% 5.57/5.76       'E'(f(suc(suc(X_19))), f(suc(suc(suc(X_19))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_19)))) | 'LE'(f(X_19), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_19))), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(s(0)))), f(suc(suc(X_19)))))],
% 5.57/5.76                [refute_0_114, refute_0_129])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_131, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(suc(X_153))), suc(suc(suc(X_153)))) |
% 5.57/5.76       'E'(f(suc(suc(X_153))), f(suc(suc(suc(X_153))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_153)))) | 'LE'(f(X_153), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_153))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_130 : [bind(X_19, $fot(X_153))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_132, plain,
% 5.57/5.76      ('E'(f(suc(suc(X_153))), f(suc(suc(suc(X_153))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_153)))) | 'LE'(f(X_153), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_153))), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve,
% 5.57/5.76                [$cnf(iLEQ(suc(suc(suc(X_153))), suc(suc(suc(X_153)))))],
% 5.57/5.76                [refute_0_123, refute_0_131])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_133, plain,
% 5.57/5.76      ('E'(f(suc(suc(X_155))), f(suc(suc(suc(X_155))))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_155)))) | 'LE'(f(X_155), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_155))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_132 : [bind(X_153, $fot(X_155))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_134, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(suc(X_155))), suc(suc(suc(X_155)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_155)))) | 'LE'(f(X_155), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_155))), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve,
% 5.57/5.76                [$cnf('E'(f(suc(suc(X_155))), f(suc(suc(suc(X_155))))))],
% 5.57/5.76                [refute_0_133, refute_0_128])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_135, plain,
% 5.57/5.76      (~ iLEQ(suc(suc(suc(X_157))), suc(suc(suc(X_157)))) |
% 5.57/5.76       'E'(s(s(s(0))), f(suc(suc(X_157)))) | 'LE'(f(X_157), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_157))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_134 : [bind(X_155, $fot(X_157))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_136, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_157)))) | 'LE'(f(X_157), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_157))), s(s(s(s(0)))))),
% 5.57/5.76      inference(resolve,
% 5.57/5.76                [$cnf(iLEQ(suc(suc(suc(X_157))), suc(suc(suc(X_157)))))],
% 5.57/5.76                [refute_0_125, refute_0_135])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_137, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_158)))) | 'LE'(f(X_158), s(s(s(0)))) |
% 5.57/5.76       'LE'(f(suc(suc(X_158))), s(s(s(s(0)))))),
% 5.57/5.76      inference(subst, [], [refute_0_136 : [bind(X_157, $fot(X_158))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_138, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_158)))) | 'LE'(f(X_158), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(suc(suc(X_158))), s(s(s(s(0))))))],
% 5.57/5.76                [refute_0_137, refute_0_110])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_139, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(suc(X_159)))) | 'LE'(f(X_159), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_138 : [bind(X_158, $fot(X_159))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_140, plain,
% 5.57/5.76      (~ 'E'(f(X_159), f(suc(X_159))) | ~ 'E'(s(s(s(0))), f(X_159)) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(X_159))) | 'LE'(f(X_159), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(X_159), suc(X_159))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_159)))))],
% 5.57/5.76                [refute_0_139, refute_0_109])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_141, plain,
% 5.57/5.76      (~ 'E'(f(X_170), f(suc(X_170))) | ~ 'E'(s(s(s(0))), f(X_170)) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(X_170))) | 'LE'(f(X_170), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(X_170), suc(X_170))),
% 5.57/5.76      inference(subst, [], [refute_0_140 : [bind(X_159, $fot(X_170))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_142, plain,
% 5.57/5.76      (~ 'E'(f(X_170), f(suc(X_170))) | ~ 'E'(s(s(s(0))), f(X_170)) |
% 5.57/5.76       'LE'(f(X_170), s(s(s(0)))) | iLEQ(suc(X_170), suc(X_170))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_170))))],
% 5.57/5.76                [refute_0_108, refute_0_141])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_143, plain,
% 5.57/5.76      (~ 'E'(f(X_171), f(suc(X_171))) | ~ 'E'(s(s(s(0))), f(X_171)) |
% 5.57/5.76       'LE'(f(X_171), s(s(s(0)))) | iLEQ(suc(X_171), suc(X_171))),
% 5.57/5.76      inference(subst, [], [refute_0_142 : [bind(X_170, $fot(X_171))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_144, plain,
% 5.57/5.76      (~ 'E'(f(X_171), f(suc(X_171))) | 'E'(s(s(0)), f(X_171)) |
% 5.57/5.76       'LE'(f(X_171), s(s(0))) | 'LE'(f(X_171), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(X_171), suc(X_171))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_171)))],
% 5.57/5.76                [refute_0_107, refute_0_143])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_145, plain,
% 5.57/5.76      (~ 'E'(f(X_197), f(suc(X_197))) | 'E'(s(s(0)), f(X_197)) |
% 5.57/5.76       'LE'(f(X_197), s(s(0))) | 'LE'(f(X_197), s(s(s(0)))) |
% 5.57/5.76       iLEQ(suc(X_197), suc(X_197))),
% 5.57/5.76      inference(subst, [], [refute_0_144 : [bind(X_171, $fot(X_197))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_146, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_197)) | 'LE'(f(X_197), s(s(0))) |
% 5.57/5.76       'LE'(f(X_197), s(s(s(0)))) | iLEQ(suc(X_197), suc(X_197))),
% 5.57/5.76      inference(resolve, [$cnf('E'(f(X_197), f(suc(X_197))))],
% 5.57/5.76                [refute_0_106, refute_0_145])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_147, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_198)) | 'LE'(f(X_198), s(s(0))) |
% 5.57/5.76       'LE'(f(X_198), s(s(s(0)))) | iLEQ(suc(X_198), suc(X_198))),
% 5.57/5.76      inference(subst, [], [refute_0_146 : [bind(X_197, $fot(X_198))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_148, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_198)) | 'LE'(f(X_198), s(s(0))) |
% 5.57/5.76       iLEQ(suc(X_198), suc(X_198))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(X_198), s(s(s(0)))))],
% 5.57/5.76                [refute_0_147, refute_0_5])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_149, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_204)) | 'LE'(f(X_204), s(s(0))) |
% 5.57/5.76       iLEQ(suc(X_204), suc(X_204))),
% 5.57/5.76      inference(subst, [], [refute_0_148 : [bind(X_198, $fot(X_204))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_150, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_167)) | 'E'(s(s(s(0))), f(X_167)) |
% 5.57/5.76       'LE'(f(X_167), s(s(0)))),
% 5.57/5.76      inference(subst, [], [refute_0_68 : [bind(X_111, $fot(X_167))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_151, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(X_166))) | 'LE'(f(X_166), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_99 : [bind(X_124, $fot(X_166))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_152, plain,
% 5.57/5.76      (~ 'E'(f(X_159), f(suc(X_159))) | ~ 'E'(s(s(s(0))), f(X_159)) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(X_159))) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(suc(X_159)))) |
% 5.57/5.76       ~ iLEQ(suc(X_159), suc(X_159))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [clause_1016 :
% 5.57/5.76                 [bind(A_2, $fot(X_159)), bind(B_57, $fot(X_159)),
% 5.57/5.76                  bind(B_58, $fot(X_159))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_153, plain,
% 5.57/5.76      (~ 'E'(f(X_159), f(suc(X_159))) | ~ 'E'(s(s(s(0))), f(X_159)) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(X_159))) | ~ iLEQ(suc(X_159), suc(X_159)) |
% 5.57/5.76       'LE'(f(X_159), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_159)))))],
% 5.57/5.76                [refute_0_139, refute_0_152])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_154, plain,
% 5.57/5.76      (~ 'E'(f(X_166), f(suc(X_166))) | ~ 'E'(s(s(s(0))), f(X_166)) |
% 5.57/5.76       ~ 'E'(s(s(s(0))), f(suc(X_166))) | ~ iLEQ(suc(X_166), suc(X_166)) |
% 5.57/5.76       'LE'(f(X_166), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_153 : [bind(X_159, $fot(X_166))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_155, plain,
% 5.57/5.76      (~ 'E'(f(X_166), f(suc(X_166))) | ~ 'E'(s(s(s(0))), f(X_166)) |
% 5.57/5.76       ~ iLEQ(suc(X_166), suc(X_166)) | 'LE'(f(X_166), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_166))))],
% 5.57/5.76                [refute_0_151, refute_0_154])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_156, plain,
% 5.57/5.76      (~ 'E'(f(X_167), f(suc(X_167))) | ~ 'E'(s(s(s(0))), f(X_167)) |
% 5.57/5.76       ~ iLEQ(suc(X_167), suc(X_167)) | 'LE'(f(X_167), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_155 : [bind(X_166, $fot(X_167))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_157, plain,
% 5.57/5.76      (~ 'E'(f(X_167), f(suc(X_167))) | ~ iLEQ(suc(X_167), suc(X_167)) |
% 5.57/5.76       'E'(s(s(0)), f(X_167)) | 'LE'(f(X_167), s(s(0))) |
% 5.57/5.76       'LE'(f(X_167), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_167)))],
% 5.57/5.76                [refute_0_150, refute_0_156])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_158, plain,
% 5.57/5.76      (~ 'E'(f(X_201), f(suc(X_201))) | ~ iLEQ(suc(X_201), suc(X_201)) |
% 5.57/5.76       'E'(s(s(0)), f(X_201)) | 'LE'(f(X_201), s(s(0))) |
% 5.57/5.76       'LE'(f(X_201), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_157 : [bind(X_167, $fot(X_201))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_159, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_126)) | 'E'(s(s(s(0))), f(X_126)) |
% 5.57/5.76       'LE'(f(X_126), s(s(0)))),
% 5.57/5.76      inference(subst, [], [refute_0_68 : [bind(X_111, $fot(X_126))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_160, plain,
% 5.57/5.76      (~ 'E'(s(s(s(0))), f(X_125)) | ~ 'E'(s(s(s(0))), f(suc(X_125))) |
% 5.57/5.76       ~ iLEQ(suc(X_125), suc(X_125)) | 'E'(f(X_125), f(suc(X_125)))),
% 5.57/5.76      inference(subst, [],
% 5.57/5.76                [clause_249 :
% 5.57/5.76                 [bind(A_2, $fot(X_125)), bind(B_57, $fot(X_125)),
% 5.57/5.76                  bind(B_58, $fot(X_125))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_161, plain,
% 5.57/5.76      (~ 'E'(s(s(s(0))), f(X_125)) | ~ iLEQ(suc(X_125), suc(X_125)) |
% 5.57/5.76       'E'(f(X_125), f(suc(X_125))) | 'LE'(f(X_125), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_125))))],
% 5.57/5.76                [refute_0_100, refute_0_160])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_162, plain,
% 5.57/5.76      (~ 'E'(s(s(s(0))), f(X_126)) | ~ iLEQ(suc(X_126), suc(X_126)) |
% 5.57/5.76       'E'(f(X_126), f(suc(X_126))) | 'LE'(f(X_126), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_161 : [bind(X_125, $fot(X_126))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_163, plain,
% 5.57/5.76      (~ iLEQ(suc(X_126), suc(X_126)) | 'E'(f(X_126), f(suc(X_126))) |
% 5.57/5.76       'E'(s(s(0)), f(X_126)) | 'LE'(f(X_126), s(s(0))) |
% 5.57/5.76       'LE'(f(X_126), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(s(s(s(0))), f(X_126)))],
% 5.57/5.76                [refute_0_159, refute_0_162])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_164, plain,
% 5.57/5.76      (~ iLEQ(suc(X_198), suc(X_198)) | 'E'(f(X_198), f(suc(X_198))) |
% 5.57/5.76       'E'(s(s(0)), f(X_198)) | 'LE'(f(X_198), s(s(0))) |
% 5.57/5.76       'LE'(f(X_198), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_163 : [bind(X_126, $fot(X_198))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_165, plain,
% 5.57/5.76      ('E'(f(X_198), f(suc(X_198))) | 'E'(s(s(0)), f(X_198)) |
% 5.57/5.76       'LE'(f(X_198), s(s(0))) | 'LE'(f(X_198), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf(iLEQ(suc(X_198), suc(X_198)))],
% 5.57/5.76                [refute_0_147, refute_0_164])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_166, plain,
% 5.57/5.76      ('E'(f(X_201), f(suc(X_201))) | 'E'(s(s(0)), f(X_201)) |
% 5.57/5.76       'LE'(f(X_201), s(s(0))) | 'LE'(f(X_201), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_165 : [bind(X_198, $fot(X_201))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_167, plain,
% 5.57/5.76      (~ iLEQ(suc(X_201), suc(X_201)) | 'E'(s(s(0)), f(X_201)) |
% 5.57/5.76       'LE'(f(X_201), s(s(0))) | 'LE'(f(X_201), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf('E'(f(X_201), f(suc(X_201))))],
% 5.57/5.76                [refute_0_166, refute_0_158])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_168, plain,
% 5.57/5.76      (~ iLEQ(suc(X_204), suc(X_204)) | 'E'(s(s(0)), f(X_204)) |
% 5.57/5.76       'LE'(f(X_204), s(s(0))) | 'LE'(f(X_204), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_167 : [bind(X_201, $fot(X_204))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_169, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_204)) | 'LE'(f(X_204), s(s(0))) |
% 5.57/5.76       'LE'(f(X_204), s(s(s(0))))),
% 5.57/5.76      inference(resolve, [$cnf(iLEQ(suc(X_204), suc(X_204)))],
% 5.57/5.76                [refute_0_149, refute_0_168])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_170, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_205)) | 'LE'(f(X_205), s(s(0))) |
% 5.57/5.76       'LE'(f(X_205), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_169 : [bind(X_204, $fot(X_205))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_171, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_205)) | 'LE'(f(X_205), s(s(0)))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(X_205), s(s(s(0)))))],
% 5.57/5.76                [refute_0_170, refute_0_4])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_172, plain,
% 5.57/5.76      ('E'(s(s(0)), f(X_206)) | 'LE'(f(X_206), s(s(0)))),
% 5.57/5.76      inference(subst, [], [refute_0_171 : [bind(X_205, $fot(X_206))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_173, plain,
% 5.57/5.76      ('E'(s(0), f(X_206)) | 'E'(s(s(0)), f(X_206)) | 'LE'(f(X_206), s(0))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(X_206), s(s(0))))],
% 5.57/5.76                [refute_0_172, refute_0_3])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_174, plain,
% 5.57/5.76      ('E'(s(0), f(X_354)) | 'E'(s(s(0)), f(X_354)) | 'LE'(f(X_354), s(0))),
% 5.57/5.76      inference(subst, [], [refute_0_173 : [bind(X_206, $fot(X_354))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_175, plain,
% 5.57/5.76      (~ 'LE'(f(X_253), s(s(0))) | 'E'(s(0), f(X_253)) |
% 5.57/5.76       'LE'(f(X_253), s(0))),
% 5.57/5.76      inference(subst, [], [clause_1158 : [bind(B_86, $fot(X_253))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_176, plain,
% 5.57/5.76      ('E'(s(0), f(X_249)) | 'E'(s(s(0)), f(X_249)) | 'LE'(f(X_249), s(0))),
% 5.57/5.76      inference(subst, [], [refute_0_173 : [bind(X_206, $fot(X_249))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_177, plain,
% 5.57/5.76      (~ 'E'(s(s(0)), f(X_248)) | ~ 'E'(s(s(0)), f(suc(X_248))) |
% 5.57/5.76       'E'(f(X_248), f(suc(X_248))) | iLEQ(suc(X_248), suc(X_248))),
% 5.57/5.76      inference(subst, [], [clause_794 : [bind(A_3, $fot(X_248))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_178, plain,
% 5.57/5.76      (~ 'LE'(f(suc(X_247)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(X_247))) |
% 5.57/5.76       'LE'(f(X_247), s(s(0)))),
% 5.57/5.76      inference(subst, [], [clause_773 : [bind(B_74, $fot(X_247))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_179, plain,
% 5.57/5.76      (~ 'LE'(f(suc(X_242)), s(s(s(0)))) | 'E'(s(s(0)), f(suc(X_242))) |
% 5.57/5.76       'LE'(f(X_242), s(s(0)))),
% 5.57/5.76      inference(subst, [], [clause_773 : [bind(B_74, $fot(X_242))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_180, plain,
% 5.57/5.76      ('E'(s(s(s(0))), f(suc(B_74))) | 'LE'(f(suc(B_74)), s(s(s(0))))),
% 5.57/5.76      inference(subst, [], [refute_0_66 : [bind(X_110, $fot(suc(B_74)))]])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_181, plain,
% 5.57/5.76      ('E'(s(s(0)), f(suc(B_74))) | 'E'(s(s(s(0))), f(suc(B_74))) |
% 5.57/5.76       'LE'(f(B_74), s(s(0)))),
% 5.57/5.76      inference(resolve, [$cnf('LE'(f(suc(B_74)), s(s(s(0)))))],
% 5.57/5.76                [refute_0_180, clause_773])).
% 5.57/5.76  
% 5.57/5.76  cnf(refute_0_182, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_241))) | 'E'(s(s(s(0))), f(suc(X_241))) |
% 5.57/5.77       'LE'(f(X_241), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_181 : [bind(B_74, $fot(X_241))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_183, plain,
% 5.57/5.77      (~ 'E'(f(suc(X_192)), f(suc(suc(X_192)))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(X_192))) | 'LE'(f(suc(X_192)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(X_192)), suc(suc(X_192)))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_142 : [bind(X_170, $fot(suc(X_192)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_184, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(B_74))) |
% 5.57/5.77       'E'(f(suc(B_74)), f(suc(suc(B_74)))) |
% 5.57/5.77       'LE'(f(suc(B_74)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(B_74)), suc(suc(B_74)))),
% 5.57/5.77      inference(subst, [], [refute_0_101 : [bind(X_125, $fot(suc(B_74)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_185, plain,
% 5.57/5.77      ('E'(f(suc(B_74)), f(suc(suc(B_74)))) | 'E'(s(s(0)), f(suc(B_74))) |
% 5.57/5.77       'LE'(f(B_74), s(s(0))) | 'LE'(f(suc(B_74)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(B_74)), suc(suc(B_74)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(B_74))))],
% 5.57/5.77                [refute_0_181, refute_0_184])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_186, plain,
% 5.57/5.77      ('E'(f(suc(X_192)), f(suc(suc(X_192)))) | 'E'(s(s(0)), f(suc(X_192))) |
% 5.57/5.77       'LE'(f(X_192), s(s(0))) | 'LE'(f(suc(X_192)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(X_192)), suc(suc(X_192)))),
% 5.57/5.77      inference(subst, [], [refute_0_185 : [bind(B_74, $fot(X_192))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_187, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(X_192))) | 'E'(s(s(0)), f(suc(X_192))) |
% 5.57/5.77       'LE'(f(X_192), s(s(0))) | 'LE'(f(suc(X_192)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(X_192)), suc(suc(X_192)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(f(suc(X_192)), f(suc(suc(X_192)))))],
% 5.57/5.77                [refute_0_186, refute_0_183])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_188, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(X_241))) | 'E'(s(s(0)), f(suc(X_241))) |
% 5.57/5.77       'LE'(f(X_241), s(s(0))) | 'LE'(f(suc(X_241)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(X_241)), suc(suc(X_241)))),
% 5.57/5.77      inference(subst, [], [refute_0_187 : [bind(X_192, $fot(X_241))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_189, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_241))) | 'LE'(f(X_241), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_241)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(X_241)), suc(suc(X_241)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(X_241))))],
% 5.57/5.77                [refute_0_182, refute_0_188])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_190, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_242))) | 'LE'(f(X_242), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_242)), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(X_242)), suc(suc(X_242)))),
% 5.57/5.77      inference(subst, [], [refute_0_189 : [bind(X_241, $fot(X_242))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_191, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_242))) | 'LE'(f(X_242), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(X_242)), suc(suc(X_242)))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(suc(X_242)), s(s(s(0)))))],
% 5.57/5.77                [refute_0_190, refute_0_179])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_192, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_246))) | 'LE'(f(X_246), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(X_246)), suc(suc(X_246)))),
% 5.57/5.77      inference(subst, [], [refute_0_191 : [bind(X_242, $fot(X_246))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_193, plain,
% 5.57/5.77      (~ 'E'(f(suc(B_74)), f(suc(suc(B_74)))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(B_74))) |
% 5.57/5.77       ~ iLEQ(suc(suc(B_74)), suc(suc(B_74))) |
% 5.57/5.77       'LE'(f(suc(B_74)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_155 : [bind(X_166, $fot(suc(B_74)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_194, plain,
% 5.57/5.77      (~ 'E'(f(suc(B_74)), f(suc(suc(B_74)))) |
% 5.57/5.77       ~ iLEQ(suc(suc(B_74)), suc(suc(B_74))) | 'E'(s(s(0)), f(suc(B_74))) |
% 5.57/5.77       'LE'(f(B_74), s(s(0))) | 'LE'(f(suc(B_74)), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(B_74))))],
% 5.57/5.77                [refute_0_181, refute_0_193])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_195, plain,
% 5.57/5.77      (~ 'E'(f(suc(X_244)), f(suc(suc(X_244)))) |
% 5.57/5.77       ~ iLEQ(suc(suc(X_244)), suc(suc(X_244))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(X_244))) | 'LE'(f(X_244), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_244)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_194 : [bind(B_74, $fot(X_244))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_196, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(B_74))) |
% 5.57/5.77       ~ iLEQ(suc(suc(B_74)), suc(suc(B_74))) |
% 5.57/5.77       'E'(f(suc(B_74)), f(suc(suc(B_74)))) |
% 5.57/5.77       'LE'(f(suc(B_74)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_161 : [bind(X_125, $fot(suc(B_74)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_197, plain,
% 5.57/5.77      (~ iLEQ(suc(suc(B_74)), suc(suc(B_74))) |
% 5.57/5.77       'E'(f(suc(B_74)), f(suc(suc(B_74)))) | 'E'(s(s(0)), f(suc(B_74))) |
% 5.57/5.77       'LE'(f(B_74), s(s(0))) | 'LE'(f(suc(B_74)), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(B_74))))],
% 5.57/5.77                [refute_0_181, refute_0_196])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_198, plain,
% 5.57/5.77      (~ iLEQ(suc(suc(X_242)), suc(suc(X_242))) |
% 5.57/5.77       'E'(f(suc(X_242)), f(suc(suc(X_242)))) | 'E'(s(s(0)), f(suc(X_242))) |
% 5.57/5.77       'LE'(f(X_242), s(s(0))) | 'LE'(f(suc(X_242)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_197 : [bind(B_74, $fot(X_242))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_199, plain,
% 5.57/5.77      ('E'(f(suc(X_242)), f(suc(suc(X_242)))) | 'E'(s(s(0)), f(suc(X_242))) |
% 5.57/5.77       'LE'(f(X_242), s(s(0))) | 'LE'(f(suc(X_242)), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf(iLEQ(suc(suc(X_242)), suc(suc(X_242))))],
% 5.57/5.77                [refute_0_190, refute_0_198])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_200, plain,
% 5.57/5.77      ('E'(f(suc(X_244)), f(suc(suc(X_244)))) | 'E'(s(s(0)), f(suc(X_244))) |
% 5.57/5.77       'LE'(f(X_244), s(s(0))) | 'LE'(f(suc(X_244)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_199 : [bind(X_242, $fot(X_244))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_201, plain,
% 5.57/5.77      (~ iLEQ(suc(suc(X_244)), suc(suc(X_244))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(X_244))) | 'LE'(f(X_244), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_244)), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(f(suc(X_244)), f(suc(suc(X_244)))))],
% 5.57/5.77                [refute_0_200, refute_0_195])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_202, plain,
% 5.57/5.77      (~ iLEQ(suc(suc(X_246)), suc(suc(X_246))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(X_246))) | 'LE'(f(X_246), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_246)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_201 : [bind(X_244, $fot(X_246))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_203, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_246))) | 'LE'(f(X_246), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_246)), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf(iLEQ(suc(suc(X_246)), suc(suc(X_246))))],
% 5.57/5.77                [refute_0_192, refute_0_202])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_204, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_247))) | 'LE'(f(X_247), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(X_247)), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_203 : [bind(X_246, $fot(X_247))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_205, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_247))) | 'LE'(f(X_247), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(suc(X_247)), s(s(s(0)))))],
% 5.57/5.77                [refute_0_204, refute_0_178])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_206, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_248))) | 'LE'(f(X_248), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_205 : [bind(X_247, $fot(X_248))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_207, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_248)) | 'E'(f(X_248), f(suc(X_248))) |
% 5.57/5.77       'LE'(f(X_248), s(s(0))) | iLEQ(suc(X_248), suc(X_248))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_248))))],
% 5.57/5.77                [refute_0_206, refute_0_177])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_208, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_249)) | 'E'(f(X_249), f(suc(X_249))) |
% 5.57/5.77       'LE'(f(X_249), s(s(0))) | iLEQ(suc(X_249), suc(X_249))),
% 5.57/5.77      inference(subst, [], [refute_0_207 : [bind(X_248, $fot(X_249))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_209, plain,
% 5.57/5.77      ('E'(f(X_249), f(suc(X_249))) | 'E'(s(0), f(X_249)) |
% 5.57/5.77       'LE'(f(X_249), s(0)) | 'LE'(f(X_249), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_249), suc(X_249))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(X_249)))],
% 5.57/5.77                [refute_0_176, refute_0_208])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_210, plain,
% 5.57/5.77      ('E'(f(X_253), f(suc(X_253))) | 'E'(s(0), f(X_253)) |
% 5.57/5.77       'LE'(f(X_253), s(0)) | 'LE'(f(X_253), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_253), suc(X_253))),
% 5.57/5.77      inference(subst, [], [refute_0_209 : [bind(X_249, $fot(X_253))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_211, plain,
% 5.57/5.77      ('E'(f(X_253), f(suc(X_253))) | 'E'(s(0), f(X_253)) |
% 5.57/5.77       'LE'(f(X_253), s(0)) | iLEQ(suc(X_253), suc(X_253))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(X_253), s(s(0))))],
% 5.57/5.77                [refute_0_210, refute_0_175])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_212, plain,
% 5.57/5.77      ('E'(f(X_342), f(suc(X_342))) | 'E'(s(0), f(X_342)) |
% 5.57/5.77       'LE'(f(X_342), s(0)) | iLEQ(suc(X_342), suc(X_342))),
% 5.57/5.77      inference(subst, [], [refute_0_211 : [bind(X_253, $fot(X_342))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_213, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_341))) | 'LE'(f(X_341), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_205 : [bind(X_247, $fot(X_341))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_214, plain,
% 5.57/5.77      (~ 'E'(f(X_334), f(suc(X_334))) | ~ 'E'(s(s(0)), f(X_334)) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_334))) | ~ 'E'(s(s(0)), f(suc(suc(X_334)))) |
% 5.57/5.77       iLEQ(suc(X_334), suc(X_334))),
% 5.57/5.77      inference(subst, [], [clause_237 : [bind(A_3, $fot(X_334))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_215, plain,
% 5.57/5.77      (~ 'LE'(f(suc(suc(X_333))), s(s(s(0)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_333)))) | 'LE'(f(X_333), s(s(0)))),
% 5.57/5.77      inference(subst, [], [clause_569 : [bind(B_74, $fot(X_333))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_216, plain,
% 5.57/5.77      ('E'(s(s(s(0))), f(suc(suc(B_74)))) |
% 5.57/5.77       'LE'(f(suc(suc(B_74))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_66 : [bind(X_110, $fot(suc(suc(B_74))))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_217, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(B_74)))) | 'E'(s(s(s(0))), f(suc(suc(B_74)))) |
% 5.57/5.77       'LE'(f(B_74), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(suc(suc(B_74))), s(s(s(0)))))],
% 5.57/5.77                [refute_0_216, clause_569])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_218, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_332)))) |
% 5.57/5.77       'E'(s(s(s(0))), f(suc(suc(X_332)))) | 'LE'(f(X_332), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_217 : [bind(B_74, $fot(X_332))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_219, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_280)))) |
% 5.57/5.77       'E'(s(s(s(0))), f(suc(suc(X_280)))) | 'LE'(f(X_280), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_217 : [bind(B_74, $fot(X_280))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_220, plain,
% 5.57/5.77      (~ 'E'(f(suc(suc(X_235))), f(suc(suc(suc(X_235))))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(suc(X_235)))) |
% 5.57/5.77       'LE'(f(suc(suc(X_235))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(X_235))), suc(suc(suc(X_235))))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_142 : [bind(X_170, $fot(suc(suc(X_235))))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_221, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(B_74)))) |
% 5.57/5.77       'E'(f(suc(suc(B_74))), f(suc(suc(suc(B_74))))) |
% 5.57/5.77       'LE'(f(suc(suc(B_74))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(B_74))), suc(suc(suc(B_74))))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_101 : [bind(X_125, $fot(suc(suc(B_74))))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_222, plain,
% 5.57/5.77      ('E'(f(suc(suc(B_74))), f(suc(suc(suc(B_74))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(B_74)))) | 'LE'(f(B_74), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(B_74))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(B_74))), suc(suc(suc(B_74))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(B_74)))))],
% 5.57/5.77                [refute_0_217, refute_0_221])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_223, plain,
% 5.57/5.77      ('E'(f(suc(suc(X_235))), f(suc(suc(suc(X_235))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_235)))) | 'LE'(f(X_235), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_235))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(X_235))), suc(suc(suc(X_235))))),
% 5.57/5.77      inference(subst, [], [refute_0_222 : [bind(B_74, $fot(X_235))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_224, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_235)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_235)))) | 'LE'(f(X_235), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_235))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(X_235))), suc(suc(suc(X_235))))),
% 5.57/5.77      inference(resolve,
% 5.57/5.77                [$cnf('E'(f(suc(suc(X_235))), f(suc(suc(suc(X_235))))))],
% 5.57/5.77                [refute_0_223, refute_0_220])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_225, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_280)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_280)))) | 'LE'(f(X_280), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_280))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(X_280))), suc(suc(suc(X_280))))),
% 5.57/5.77      inference(subst, [], [refute_0_224 : [bind(X_235, $fot(X_280))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_226, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_280)))) | 'LE'(f(X_280), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_280))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(X_280))), suc(suc(suc(X_280))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_280)))))],
% 5.57/5.77                [refute_0_219, refute_0_225])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_227, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_331)))) | 'LE'(f(X_331), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_331))), s(s(s(0)))) |
% 5.57/5.77       iLEQ(suc(suc(suc(X_331))), suc(suc(suc(X_331))))),
% 5.57/5.77      inference(subst, [], [refute_0_226 : [bind(X_280, $fot(X_331))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_228, plain,
% 5.57/5.77      (~ 'E'(f(suc(suc(X_330))), f(suc(suc(suc(X_330))))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(suc(X_330)))) |
% 5.57/5.77       ~ iLEQ(suc(suc(suc(X_330))), suc(suc(suc(X_330)))) |
% 5.57/5.77       'LE'(f(suc(suc(X_330))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_155 : [bind(X_166, $fot(suc(suc(X_330))))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_229, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_329)))) |
% 5.57/5.77       'E'(s(s(s(0))), f(suc(suc(X_329)))) | 'LE'(f(X_329), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_217 : [bind(B_74, $fot(X_329))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_230, plain,
% 5.57/5.77      ('E'(s(s(s(0))), f(suc(suc(suc(X_328))))) |
% 5.57/5.77       'LE'(f(suc(suc(X_328))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_99 : [bind(X_124, $fot(suc(suc(X_328))))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_231, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_280)))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(suc(suc(X_280))))) |
% 5.57/5.77       ~ iLEQ(suc(suc(suc(X_280))), suc(suc(suc(X_280)))) |
% 5.57/5.77       'E'(f(suc(suc(X_280))), f(suc(suc(suc(X_280)))))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [clause_249 :
% 5.57/5.77                 [bind(A_2, $fot(suc(suc(X_280)))),
% 5.57/5.77                  bind(B_57, $fot(suc(suc(X_280)))),
% 5.57/5.77                  bind(B_58, $fot(suc(suc(X_280))))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_232, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_280)))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(suc(suc(X_280))))) |
% 5.57/5.77       'E'(f(suc(suc(X_280))), f(suc(suc(suc(X_280))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_280)))) | 'LE'(f(X_280), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_280))), s(s(s(0))))),
% 5.57/5.77      inference(resolve,
% 5.57/5.77                [$cnf(iLEQ(suc(suc(suc(X_280))), suc(suc(suc(X_280)))))],
% 5.57/5.77                [refute_0_226, refute_0_231])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_233, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_328)))) |
% 5.57/5.77       ~ 'E'(s(s(s(0))), f(suc(suc(suc(X_328))))) |
% 5.57/5.77       'E'(f(suc(suc(X_328))), f(suc(suc(suc(X_328))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_328)))) | 'LE'(f(X_328), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_328))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_232 : [bind(X_280, $fot(X_328))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_234, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_328)))) |
% 5.57/5.77       'E'(f(suc(suc(X_328))), f(suc(suc(suc(X_328))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_328)))) | 'LE'(f(X_328), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_328))), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(suc(X_328))))))],
% 5.57/5.77                [refute_0_230, refute_0_233])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_235, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_329)))) |
% 5.57/5.77       'E'(f(suc(suc(X_329))), f(suc(suc(suc(X_329))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_329)))) | 'LE'(f(X_329), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_329))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_234 : [bind(X_328, $fot(X_329))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_236, plain,
% 5.57/5.77      ('E'(f(suc(suc(X_329))), f(suc(suc(suc(X_329))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_329)))) | 'LE'(f(X_329), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_329))), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_329)))))],
% 5.57/5.77                [refute_0_229, refute_0_235])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_237, plain,
% 5.57/5.77      ('E'(f(suc(suc(X_330))), f(suc(suc(suc(X_330))))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_330)))) | 'LE'(f(X_330), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_330))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_236 : [bind(X_329, $fot(X_330))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_238, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_330)))) |
% 5.57/5.77       ~ iLEQ(suc(suc(suc(X_330))), suc(suc(suc(X_330)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_330)))) | 'LE'(f(X_330), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_330))), s(s(s(0))))),
% 5.57/5.77      inference(resolve,
% 5.57/5.77                [$cnf('E'(f(suc(suc(X_330))), f(suc(suc(suc(X_330))))))],
% 5.57/5.77                [refute_0_237, refute_0_228])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_239, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_331)))) |
% 5.57/5.77       ~ iLEQ(suc(suc(suc(X_331))), suc(suc(suc(X_331)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_331)))) | 'LE'(f(X_331), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_331))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_238 : [bind(X_330, $fot(X_331))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_240, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_331)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_331)))) | 'LE'(f(X_331), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_331))), s(s(s(0))))),
% 5.57/5.77      inference(resolve,
% 5.57/5.77                [$cnf(iLEQ(suc(suc(suc(X_331))), suc(suc(suc(X_331)))))],
% 5.57/5.77                [refute_0_227, refute_0_239])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_241, plain,
% 5.57/5.77      (~ 'E'(s(s(s(0))), f(suc(suc(X_332)))) |
% 5.57/5.77       'E'(s(s(0)), f(suc(suc(X_332)))) | 'LE'(f(X_332), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_332))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_240 : [bind(X_331, $fot(X_332))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_242, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_332)))) | 'LE'(f(X_332), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_332))), s(s(s(0))))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(s(0))), f(suc(suc(X_332)))))],
% 5.57/5.77                [refute_0_218, refute_0_241])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_243, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_333)))) | 'LE'(f(X_333), s(s(0))) |
% 5.57/5.77       'LE'(f(suc(suc(X_333))), s(s(s(0))))),
% 5.57/5.77      inference(subst, [], [refute_0_242 : [bind(X_332, $fot(X_333))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_244, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_333)))) | 'LE'(f(X_333), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(suc(suc(X_333))), s(s(s(0)))))],
% 5.57/5.77                [refute_0_243, refute_0_215])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_245, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(suc(X_334)))) | 'LE'(f(X_334), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_244 : [bind(X_333, $fot(X_334))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_246, plain,
% 5.57/5.77      (~ 'E'(f(X_334), f(suc(X_334))) | ~ 'E'(s(s(0)), f(X_334)) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_334))) | 'LE'(f(X_334), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_334), suc(X_334))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_334)))))],
% 5.57/5.77                [refute_0_245, refute_0_214])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_247, plain,
% 5.57/5.77      (~ 'E'(f(X_341), f(suc(X_341))) | ~ 'E'(s(s(0)), f(X_341)) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_341))) | 'LE'(f(X_341), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_341), suc(X_341))),
% 5.57/5.77      inference(subst, [], [refute_0_246 : [bind(X_334, $fot(X_341))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_248, plain,
% 5.57/5.77      (~ 'E'(f(X_341), f(suc(X_341))) | ~ 'E'(s(s(0)), f(X_341)) |
% 5.57/5.77       'LE'(f(X_341), s(s(0))) | iLEQ(suc(X_341), suc(X_341))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_341))))],
% 5.57/5.77                [refute_0_213, refute_0_247])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_249, plain,
% 5.57/5.77      (~ 'E'(f(X_342), f(suc(X_342))) | ~ 'E'(s(s(0)), f(X_342)) |
% 5.57/5.77       'LE'(f(X_342), s(s(0))) | iLEQ(suc(X_342), suc(X_342))),
% 5.57/5.77      inference(subst, [], [refute_0_248 : [bind(X_341, $fot(X_342))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_250, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_342)) | 'E'(s(0), f(X_342)) |
% 5.57/5.77       'LE'(f(X_342), s(0)) | 'LE'(f(X_342), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_342), suc(X_342))),
% 5.57/5.77      inference(resolve, [$cnf('E'(f(X_342), f(suc(X_342))))],
% 5.57/5.77                [refute_0_212, refute_0_249])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_251, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_354)) | 'E'(s(0), f(X_354)) |
% 5.57/5.77       'LE'(f(X_354), s(0)) | 'LE'(f(X_354), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_354), suc(X_354))),
% 5.57/5.77      inference(subst, [], [refute_0_250 : [bind(X_342, $fot(X_354))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_252, plain,
% 5.57/5.77      ('E'(s(0), f(X_354)) | 'LE'(f(X_354), s(0)) | 'LE'(f(X_354), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_354), suc(X_354))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(X_354)))],
% 5.57/5.77                [refute_0_174, refute_0_251])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_253, plain,
% 5.57/5.77      ('E'(s(0), f(X_355)) | 'LE'(f(X_355), s(0)) | 'LE'(f(X_355), s(s(0))) |
% 5.57/5.77       iLEQ(suc(X_355), suc(X_355))),
% 5.57/5.77      inference(subst, [], [refute_0_252 : [bind(X_354, $fot(X_355))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_254, plain,
% 5.57/5.77      ('E'(s(0), f(X_355)) | 'LE'(f(X_355), s(0)) |
% 5.57/5.77       iLEQ(suc(X_355), suc(X_355))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(X_355), s(s(0))))],
% 5.57/5.77                [refute_0_253, refute_0_2])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_255, plain,
% 5.57/5.77      ('E'(s(0), f(X_359)) | 'LE'(f(X_359), s(0)) |
% 5.57/5.77       iLEQ(suc(X_359), suc(X_359))),
% 5.57/5.77      inference(subst, [], [refute_0_254 : [bind(X_355, $fot(X_359))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_256, plain,
% 5.57/5.77      ('E'(s(0), f(X_348)) | 'E'(s(s(0)), f(X_348)) | 'LE'(f(X_348), s(0))),
% 5.57/5.77      inference(subst, [], [refute_0_173 : [bind(X_206, $fot(X_348))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_257, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(X_347))) | 'LE'(f(X_347), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_205 : [bind(X_247, $fot(X_347))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_258, plain,
% 5.57/5.77      (~ 'E'(f(X_334), f(suc(X_334))) | ~ 'E'(s(s(0)), f(X_334)) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_334))) | ~ 'E'(s(s(0)), f(suc(suc(X_334)))) |
% 5.57/5.77       ~ iLEQ(suc(X_334), suc(X_334))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [clause_115 :
% 5.57/5.77                 [bind(A_3, $fot(X_334)), bind(B_75, $fot(X_334)),
% 5.57/5.77                  bind(B_76, $fot(X_334))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_259, plain,
% 5.57/5.77      (~ 'E'(f(X_334), f(suc(X_334))) | ~ 'E'(s(s(0)), f(X_334)) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_334))) | ~ iLEQ(suc(X_334), suc(X_334)) |
% 5.57/5.77       'LE'(f(X_334), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_334)))))],
% 5.57/5.77                [refute_0_245, refute_0_258])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_260, plain,
% 5.57/5.77      (~ 'E'(f(X_347), f(suc(X_347))) | ~ 'E'(s(s(0)), f(X_347)) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_347))) | ~ iLEQ(suc(X_347), suc(X_347)) |
% 5.57/5.77       'LE'(f(X_347), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_259 : [bind(X_334, $fot(X_347))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_261, plain,
% 5.57/5.77      (~ 'E'(f(X_347), f(suc(X_347))) | ~ 'E'(s(s(0)), f(X_347)) |
% 5.57/5.77       ~ iLEQ(suc(X_347), suc(X_347)) | 'LE'(f(X_347), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_347))))],
% 5.57/5.77                [refute_0_257, refute_0_260])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_262, plain,
% 5.57/5.77      (~ 'E'(f(X_348), f(suc(X_348))) | ~ 'E'(s(s(0)), f(X_348)) |
% 5.57/5.77       ~ iLEQ(suc(X_348), suc(X_348)) | 'LE'(f(X_348), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_261 : [bind(X_347, $fot(X_348))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_263, plain,
% 5.57/5.77      (~ 'E'(f(X_348), f(suc(X_348))) | ~ iLEQ(suc(X_348), suc(X_348)) |
% 5.57/5.77       'E'(s(0), f(X_348)) | 'LE'(f(X_348), s(0)) | 'LE'(f(X_348), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(X_348)))],
% 5.57/5.77                [refute_0_256, refute_0_262])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_264, plain,
% 5.57/5.77      (~ 'E'(f(X_357), f(suc(X_357))) | ~ iLEQ(suc(X_357), suc(X_357)) |
% 5.57/5.77       'E'(s(0), f(X_357)) | 'LE'(f(X_357), s(0)) | 'LE'(f(X_357), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_263 : [bind(X_348, $fot(X_357))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_265, plain,
% 5.57/5.77      ('E'(s(0), f(X_250)) | 'E'(s(s(0)), f(X_250)) | 'LE'(f(X_250), s(0))),
% 5.57/5.77      inference(subst, [], [refute_0_173 : [bind(X_206, $fot(X_250))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_266, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_248)) | ~ 'E'(s(s(0)), f(suc(X_248))) |
% 5.57/5.77       ~ iLEQ(suc(X_248), suc(X_248)) | 'E'(f(X_248), f(suc(X_248)))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [clause_778 :
% 5.57/5.77                 [bind(A_3, $fot(X_248)), bind(B_75, $fot(X_248)),
% 5.57/5.77                  bind(B_76, $fot(X_248))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_267, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_248)) | ~ iLEQ(suc(X_248), suc(X_248)) |
% 5.57/5.77       'E'(f(X_248), f(suc(X_248))) | 'LE'(f(X_248), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_248))))],
% 5.57/5.77                [refute_0_206, refute_0_266])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_268, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(X_250)) | ~ iLEQ(suc(X_250), suc(X_250)) |
% 5.57/5.77       'E'(f(X_250), f(suc(X_250))) | 'LE'(f(X_250), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_267 : [bind(X_248, $fot(X_250))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_269, plain,
% 5.57/5.77      (~ iLEQ(suc(X_250), suc(X_250)) | 'E'(f(X_250), f(suc(X_250))) |
% 5.57/5.77       'E'(s(0), f(X_250)) | 'LE'(f(X_250), s(0)) | 'LE'(f(X_250), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(X_250)))],
% 5.57/5.77                [refute_0_265, refute_0_268])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_270, plain,
% 5.57/5.77      (~ iLEQ(suc(X_355), suc(X_355)) | 'E'(f(X_355), f(suc(X_355))) |
% 5.57/5.77       'E'(s(0), f(X_355)) | 'LE'(f(X_355), s(0)) | 'LE'(f(X_355), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_269 : [bind(X_250, $fot(X_355))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_271, plain,
% 5.57/5.77      ('E'(f(X_355), f(suc(X_355))) | 'E'(s(0), f(X_355)) |
% 5.57/5.77       'LE'(f(X_355), s(0)) | 'LE'(f(X_355), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf(iLEQ(suc(X_355), suc(X_355)))],
% 5.57/5.77                [refute_0_253, refute_0_270])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_272, plain,
% 5.57/5.77      ('E'(f(X_357), f(suc(X_357))) | 'E'(s(0), f(X_357)) |
% 5.57/5.77       'LE'(f(X_357), s(0)) | 'LE'(f(X_357), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_271 : [bind(X_355, $fot(X_357))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_273, plain,
% 5.57/5.77      (~ iLEQ(suc(X_357), suc(X_357)) | 'E'(s(0), f(X_357)) |
% 5.57/5.77       'LE'(f(X_357), s(0)) | 'LE'(f(X_357), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(f(X_357), f(suc(X_357))))],
% 5.57/5.77                [refute_0_272, refute_0_264])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_274, plain,
% 5.57/5.77      (~ iLEQ(suc(X_359), suc(X_359)) | 'E'(s(0), f(X_359)) |
% 5.57/5.77       'LE'(f(X_359), s(0)) | 'LE'(f(X_359), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_273 : [bind(X_357, $fot(X_359))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_275, plain,
% 5.57/5.77      ('E'(s(0), f(X_359)) | 'LE'(f(X_359), s(0)) | 'LE'(f(X_359), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf(iLEQ(suc(X_359), suc(X_359)))],
% 5.57/5.77                [refute_0_255, refute_0_274])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_276, plain,
% 5.57/5.77      ('E'(s(0), f(X_360)) | 'LE'(f(X_360), s(0)) | 'LE'(f(X_360), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_275 : [bind(X_359, $fot(X_360))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_277, plain, ('E'(s(0), f(X_360)) | 'LE'(f(X_360), s(0))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(X_360), s(s(0))))],
% 5.57/5.77                [refute_0_276, refute_0_1])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_278, plain,
% 5.57/5.77      ('E'(s(0), f(suc(B_93))) | 'LE'(f(suc(B_93)), s(0))),
% 5.57/5.77      inference(subst, [], [refute_0_277 : [bind(X_360, $fot(suc(B_93)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_279, plain,
% 5.57/5.77      ('E'(0, f(suc(B_93))) | 'E'(s(0), f(suc(B_93))) | 'LE'(f(B_93), 0)),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(suc(B_93)), s(0)))],
% 5.57/5.77                [refute_0_278, clause_713])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_280, plain,
% 5.57/5.77      ('E'(0, f(suc(X_734))) | 'E'(s(0), f(suc(X_734))) | 'LE'(f(X_734), 0)),
% 5.57/5.77      inference(subst, [], [refute_0_279 : [bind(B_93, $fot(X_734))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_281, plain,
% 5.57/5.77      ('E'(0, f(suc(X_691))) | 'E'(s(0), f(suc(X_691))) | 'LE'(f(X_691), 0)),
% 5.57/5.77      inference(subst, [], [refute_0_279 : [bind(B_93, $fot(X_691))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_282, plain,
% 5.57/5.77      (~ 'E'(s(0), f(X_418)) | ~ 'E'(s(0), f(suc(X_418))) |
% 5.57/5.77       'E'(f(X_418), f(suc(X_418))) | iLEQ(suc(X_418), suc(X_418))),
% 5.57/5.77      inference(subst, [], [clause_1089 : [bind(A_4, $fot(X_418))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_283, plain,
% 5.57/5.77      (~ 'LE'(f(suc(X_417)), s(s(0))) | 'E'(s(0), f(suc(X_417))) |
% 5.57/5.77       'LE'(f(X_417), s(0))),
% 5.57/5.77      inference(subst, [], [clause_149 : [bind(B_86, $fot(X_417))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_284, plain,
% 5.57/5.77      ('E'(s(s(0)), f(suc(B_86))) | 'LE'(f(suc(B_86)), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_171 : [bind(X_205, $fot(suc(B_86)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_285, plain,
% 5.57/5.77      ('E'(s(0), f(suc(B_86))) | 'E'(s(s(0)), f(suc(B_86))) |
% 5.57/5.77       'LE'(f(B_86), s(0))),
% 5.57/5.77      inference(resolve, [$cnf('LE'(f(suc(B_86)), s(s(0))))],
% 5.57/5.77                [refute_0_284, clause_149])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_286, plain,
% 5.57/5.77      ('E'(s(0), f(suc(X_416))) | 'E'(s(s(0)), f(suc(X_416))) |
% 5.57/5.77       'LE'(f(X_416), s(0))),
% 5.57/5.77      inference(subst, [], [refute_0_285 : [bind(B_86, $fot(X_416))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_287, plain,
% 5.57/5.77      ('E'(s(0), f(suc(X_398))) | 'E'(s(s(0)), f(suc(X_398))) |
% 5.57/5.77       'LE'(f(X_398), s(0))),
% 5.57/5.77      inference(subst, [], [refute_0_285 : [bind(B_86, $fot(X_398))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_288, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(B_86))) | 'E'(f(suc(B_86)), f(suc(suc(B_86)))) |
% 5.57/5.77       'LE'(f(suc(B_86)), s(s(0))) | iLEQ(suc(suc(B_86)), suc(suc(B_86)))),
% 5.57/5.77      inference(subst, [], [refute_0_207 : [bind(X_248, $fot(suc(B_86)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_289, plain,
% 5.57/5.77      ('E'(f(suc(B_86)), f(suc(suc(B_86)))) | 'E'(s(0), f(suc(B_86))) |
% 5.57/5.77       'LE'(f(B_86), s(0)) | 'LE'(f(suc(B_86)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(B_86)), suc(suc(B_86)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(B_86))))],
% 5.57/5.77                [refute_0_285, refute_0_288])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_290, plain,
% 5.57/5.77      (~ 'E'(f(suc(B_86)), f(suc(suc(B_86)))) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(B_86))) | 'LE'(f(suc(B_86)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(B_86)), suc(suc(B_86)))),
% 5.57/5.77      inference(subst, [], [refute_0_248 : [bind(X_341, $fot(suc(B_86)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_291, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(B_86))) | 'E'(s(0), f(suc(B_86))) |
% 5.57/5.77       'LE'(f(B_86), s(0)) | 'LE'(f(suc(B_86)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(B_86)), suc(suc(B_86)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(f(suc(B_86)), f(suc(suc(B_86)))))],
% 5.57/5.77                [refute_0_289, refute_0_290])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_292, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(X_398))) | 'E'(s(0), f(suc(X_398))) |
% 5.57/5.77       'LE'(f(X_398), s(0)) | 'LE'(f(suc(X_398)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(X_398)), suc(suc(X_398)))),
% 5.57/5.77      inference(subst, [], [refute_0_291 : [bind(B_86, $fot(X_398))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_293, plain,
% 5.57/5.77      ('E'(s(0), f(suc(X_398))) | 'LE'(f(X_398), s(0)) |
% 5.57/5.77       'LE'(f(suc(X_398)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(X_398)), suc(suc(X_398)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_398))))],
% 5.57/5.77                [refute_0_287, refute_0_292])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_294, plain,
% 5.57/5.77      ('E'(s(0), f(suc(X_415))) | 'LE'(f(X_415), s(0)) |
% 5.57/5.77       'LE'(f(suc(X_415)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(X_415)), suc(suc(X_415)))),
% 5.57/5.77      inference(subst, [], [refute_0_293 : [bind(X_398, $fot(X_415))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_295, plain,
% 5.57/5.77      (~ 'E'(f(suc(X_412)), f(suc(suc(X_412)))) |
% 5.57/5.77       ~ 'E'(s(s(0)), f(suc(X_412))) |
% 5.57/5.77       ~ iLEQ(suc(suc(X_412)), suc(suc(X_412))) |
% 5.57/5.77       'LE'(f(suc(X_412)), s(s(0)))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_261 : [bind(X_347, $fot(suc(X_412)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_296, plain,
% 5.57/5.77      ('E'(s(0), f(suc(X_411))) | 'E'(s(s(0)), f(suc(X_411))) |
% 5.57/5.77       'LE'(f(X_411), s(0))),
% 5.57/5.77      inference(subst, [], [refute_0_285 : [bind(B_86, $fot(X_411))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_297, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(X_399))) |
% 5.57/5.77       ~ iLEQ(suc(suc(X_399)), suc(suc(X_399))) |
% 5.57/5.77       'E'(f(suc(X_399)), f(suc(suc(X_399)))) |
% 5.57/5.77       'LE'(f(suc(X_399)), s(s(0)))),
% 5.57/5.77      inference(subst, [],
% 5.57/5.77                [refute_0_267 : [bind(X_248, $fot(suc(X_399)))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_298, plain,
% 5.57/5.77      ('E'(s(0), f(suc(X_399))) | 'LE'(f(X_399), s(0)) |
% 5.57/5.77       'LE'(f(suc(X_399)), s(s(0))) |
% 5.57/5.77       iLEQ(suc(suc(X_399)), suc(suc(X_399)))),
% 5.57/5.77      inference(subst, [], [refute_0_293 : [bind(X_398, $fot(X_399))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_299, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(X_399))) |
% 5.57/5.77       'E'(f(suc(X_399)), f(suc(suc(X_399)))) | 'E'(s(0), f(suc(X_399))) |
% 5.57/5.77       'LE'(f(X_399), s(0)) | 'LE'(f(suc(X_399)), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf(iLEQ(suc(suc(X_399)), suc(suc(X_399))))],
% 5.57/5.77                [refute_0_298, refute_0_297])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_300, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(X_411))) |
% 5.57/5.77       'E'(f(suc(X_411)), f(suc(suc(X_411)))) | 'E'(s(0), f(suc(X_411))) |
% 5.57/5.77       'LE'(f(X_411), s(0)) | 'LE'(f(suc(X_411)), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_299 : [bind(X_399, $fot(X_411))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_301, plain,
% 5.57/5.77      ('E'(f(suc(X_411)), f(suc(suc(X_411)))) | 'E'(s(0), f(suc(X_411))) |
% 5.57/5.77       'LE'(f(X_411), s(0)) | 'LE'(f(suc(X_411)), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_411))))],
% 5.57/5.77                [refute_0_296, refute_0_300])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_302, plain,
% 5.57/5.77      ('E'(f(suc(X_412)), f(suc(suc(X_412)))) | 'E'(s(0), f(suc(X_412))) |
% 5.57/5.77       'LE'(f(X_412), s(0)) | 'LE'(f(suc(X_412)), s(s(0)))),
% 5.57/5.77      inference(subst, [], [refute_0_301 : [bind(X_411, $fot(X_412))]])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_303, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(X_412))) |
% 5.57/5.77       ~ iLEQ(suc(suc(X_412)), suc(suc(X_412))) | 'E'(s(0), f(suc(X_412))) |
% 5.57/5.77       'LE'(f(X_412), s(0)) | 'LE'(f(suc(X_412)), s(s(0)))),
% 5.57/5.77      inference(resolve, [$cnf('E'(f(suc(X_412)), f(suc(suc(X_412)))))],
% 5.57/5.77                [refute_0_302, refute_0_295])).
% 5.57/5.77  
% 5.57/5.77  cnf(refute_0_304, plain,
% 5.57/5.77      (~ 'E'(s(s(0)), f(suc(X_415))) |
% 5.57/5.77       ~ iLEQ(suc(suc(X_415)), suc(suc(X_415))) | 'E'(s(0), f(suc(X_415))) |
% 5.57/5.77       'LE'(f(X_415), s(0)) | 'LE'(f(suc(X_415)), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_303 : [bind(X_412, $fot(X_415))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_305, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(X_415))) | 'E'(s(0), f(suc(X_415))) |
% 5.57/5.78       'LE'(f(X_415), s(0)) | 'LE'(f(suc(X_415)), s(s(0)))),
% 5.57/5.78      inference(resolve, [$cnf(iLEQ(suc(suc(X_415)), suc(suc(X_415))))],
% 5.57/5.78                [refute_0_294, refute_0_304])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_306, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(X_416))) | 'E'(s(0), f(suc(X_416))) |
% 5.57/5.78       'LE'(f(X_416), s(0)) | 'LE'(f(suc(X_416)), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_305 : [bind(X_415, $fot(X_416))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_307, plain,
% 5.57/5.78      ('E'(s(0), f(suc(X_416))) | 'LE'(f(X_416), s(0)) |
% 5.57/5.78       'LE'(f(suc(X_416)), s(s(0)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_416))))],
% 5.57/5.78                [refute_0_286, refute_0_306])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_308, plain,
% 5.57/5.78      ('E'(s(0), f(suc(X_417))) | 'LE'(f(X_417), s(0)) |
% 5.57/5.78       'LE'(f(suc(X_417)), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_307 : [bind(X_416, $fot(X_417))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_309, plain, ('E'(s(0), f(suc(X_417))) | 'LE'(f(X_417), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(suc(X_417)), s(s(0))))],
% 5.57/5.78                [refute_0_308, refute_0_283])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_310, plain, ('E'(s(0), f(suc(X_418))) | 'LE'(f(X_418), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_309 : [bind(X_417, $fot(X_418))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_311, plain,
% 5.57/5.78      (~ 'E'(s(0), f(X_418)) | 'E'(f(X_418), f(suc(X_418))) |
% 5.57/5.78       'LE'(f(X_418), s(0)) | iLEQ(suc(X_418), suc(X_418))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_418))))],
% 5.57/5.78                [refute_0_310, refute_0_282])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_312, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(B_93))) | 'E'(f(suc(B_93)), f(suc(suc(B_93)))) |
% 5.57/5.78       'LE'(f(suc(B_93)), s(0)) | iLEQ(suc(suc(B_93)), suc(suc(B_93)))),
% 5.57/5.78      inference(subst, [], [refute_0_311 : [bind(X_418, $fot(suc(B_93)))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_313, plain,
% 5.57/5.78      ('E'(0, f(suc(B_93))) | 'E'(f(suc(B_93)), f(suc(suc(B_93)))) |
% 5.57/5.78       'LE'(f(B_93), 0) | 'LE'(f(suc(B_93)), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(B_93)), suc(suc(B_93)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(B_93))))],
% 5.57/5.78                [refute_0_279, refute_0_312])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_314, plain, ('E'(s(0), f(suc(X_679))) | 'LE'(f(X_679), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_309 : [bind(X_417, $fot(X_679))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_315, plain,
% 5.57/5.78      (~ 'E'(f(X_668), f(suc(X_668))) | ~ 'E'(s(0), f(X_668)) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_668))) | ~ 'E'(s(0), f(suc(suc(X_668)))) |
% 5.57/5.78       iLEQ(suc(X_668), suc(X_668))),
% 5.57/5.78      inference(subst, [], [clause_340 : [bind(A_4, $fot(X_668))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_316, plain,
% 5.57/5.78      (~ 'LE'(f(suc(suc(X_667))), s(s(0))) | 'E'(s(0), f(suc(suc(X_667)))) |
% 5.57/5.78       'LE'(f(X_667), s(0))),
% 5.57/5.78      inference(subst, [], [clause_160 : [bind(B_86, $fot(X_667))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_317, plain,
% 5.57/5.78      ('E'(s(s(0)), f(suc(suc(B_86)))) | 'LE'(f(suc(suc(B_86))), s(s(0)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_171 : [bind(X_205, $fot(suc(suc(B_86))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_318, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(B_86)))) | 'E'(s(s(0)), f(suc(suc(B_86)))) |
% 5.57/5.78       'LE'(f(B_86), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(suc(suc(B_86))), s(s(0))))],
% 5.57/5.78                [refute_0_317, clause_160])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_319, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_666)))) | 'E'(s(s(0)), f(suc(suc(X_666)))) |
% 5.57/5.78       'LE'(f(X_666), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_318 : [bind(B_86, $fot(X_666))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_320, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_591)))) | 'E'(s(s(0)), f(suc(suc(X_591)))) |
% 5.57/5.78       'LE'(f(X_591), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_318 : [bind(B_86, $fot(X_591))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_321, plain,
% 5.57/5.78      (~ 'E'(f(suc(suc(X_571))), f(suc(suc(suc(X_571))))) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(suc(X_571)))) |
% 5.57/5.78       'LE'(f(suc(suc(X_571))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_571))), suc(suc(suc(X_571))))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_248 : [bind(X_341, $fot(suc(suc(X_571))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_322, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(B_86)))) |
% 5.57/5.78       'E'(f(suc(suc(B_86))), f(suc(suc(suc(B_86))))) |
% 5.57/5.78       'LE'(f(suc(suc(B_86))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(B_86))), suc(suc(suc(B_86))))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_207 : [bind(X_248, $fot(suc(suc(B_86))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_323, plain,
% 5.57/5.78      ('E'(f(suc(suc(B_86))), f(suc(suc(suc(B_86))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(B_86)))) | 'LE'(f(B_86), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(B_86))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(B_86))), suc(suc(suc(B_86))))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(B_86)))))],
% 5.57/5.78                [refute_0_318, refute_0_322])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_324, plain,
% 5.57/5.78      ('E'(f(suc(suc(X_571))), f(suc(suc(suc(X_571))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_571)))) | 'LE'(f(X_571), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_571))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_571))), suc(suc(suc(X_571))))),
% 5.57/5.78      inference(subst, [], [refute_0_323 : [bind(B_86, $fot(X_571))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_325, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_571)))) | 'E'(s(0), f(suc(suc(X_571)))) |
% 5.57/5.78       'LE'(f(X_571), s(0)) | 'LE'(f(suc(suc(X_571))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_571))), suc(suc(suc(X_571))))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf('E'(f(suc(suc(X_571))), f(suc(suc(suc(X_571))))))],
% 5.57/5.78                [refute_0_324, refute_0_321])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_326, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_591)))) | 'E'(s(0), f(suc(suc(X_591)))) |
% 5.57/5.78       'LE'(f(X_591), s(0)) | 'LE'(f(suc(suc(X_591))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_591))), suc(suc(suc(X_591))))),
% 5.57/5.78      inference(subst, [], [refute_0_325 : [bind(X_571, $fot(X_591))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_327, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_591)))) | 'LE'(f(X_591), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_591))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_591))), suc(suc(suc(X_591))))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_591)))))],
% 5.57/5.78                [refute_0_320, refute_0_326])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_328, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_665)))) | 'LE'(f(X_665), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_665))), s(s(0))) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_665))), suc(suc(suc(X_665))))),
% 5.57/5.78      inference(subst, [], [refute_0_327 : [bind(X_591, $fot(X_665))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_329, plain,
% 5.57/5.78      (~ 'E'(f(suc(suc(X_664))), f(suc(suc(suc(X_664))))) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(suc(X_664)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_664))), suc(suc(suc(X_664)))) |
% 5.57/5.78       'LE'(f(suc(suc(X_664))), s(s(0)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_261 : [bind(X_347, $fot(suc(suc(X_664))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_330, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_663)))) | 'E'(s(s(0)), f(suc(suc(X_663)))) |
% 5.57/5.78       'LE'(f(X_663), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_318 : [bind(B_86, $fot(X_663))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_331, plain,
% 5.57/5.78      ('E'(s(s(0)), f(suc(suc(suc(X_662))))) |
% 5.57/5.78       'LE'(f(suc(suc(X_662))), s(s(0)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_205 : [bind(X_247, $fot(suc(suc(X_662))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_332, plain,
% 5.57/5.78      ('E'(s(s(0)), f(suc(X_286))) | 'LE'(f(X_286), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_205 : [bind(X_247, $fot(X_286))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_333, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(X_286)) | ~ 'E'(s(s(0)), f(X_287)) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(X_286))) | ~ 'E'(s(s(0)), f(suc(X_287))) |
% 5.57/5.78       ~ iLEQ(suc(X_286), suc(X_287)) | ~ iLEQ(suc(X_287), suc(X_286)) |
% 5.57/5.78       'E'(f(X_286), f(suc(X_286))) | 'E'(f(X_287), f(suc(X_287)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [clause_778 :
% 5.57/5.78                 [bind(A_3, $fot(X_287)), bind(B_75, $fot(X_286)),
% 5.57/5.78                  bind(B_76, $fot(X_287))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_334, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(X_286)) | ~ 'E'(s(s(0)), f(X_287)) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(X_287))) | ~ iLEQ(suc(X_286), suc(X_287)) |
% 5.57/5.78       ~ iLEQ(suc(X_287), suc(X_286)) | 'E'(f(X_286), f(suc(X_286))) |
% 5.57/5.78       'E'(f(X_287), f(suc(X_287))) | 'LE'(f(X_286), s(s(0)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(X_286))))],
% 5.57/5.78                [refute_0_332, refute_0_333])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_335, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_591)))) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(suc(suc(X_591))))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_591))), suc(suc(suc(X_591)))) |
% 5.57/5.78       'E'(f(suc(suc(X_591))), f(suc(suc(suc(X_591))))) |
% 5.57/5.78       'LE'(f(suc(suc(X_591))), s(s(0)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_334 :
% 5.57/5.78                 [bind(X_286, $fot(suc(suc(X_591)))),
% 5.57/5.78                  bind(X_287, $fot(suc(suc(X_591))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_336, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_591)))) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(suc(suc(X_591))))) |
% 5.57/5.78       'E'(f(suc(suc(X_591))), f(suc(suc(suc(X_591))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_591)))) | 'LE'(f(X_591), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_591))), s(s(0)))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf(iLEQ(suc(suc(suc(X_591))), suc(suc(suc(X_591)))))],
% 5.57/5.78                [refute_0_327, refute_0_335])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_337, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_662)))) |
% 5.57/5.78       ~ 'E'(s(s(0)), f(suc(suc(suc(X_662))))) |
% 5.57/5.78       'E'(f(suc(suc(X_662))), f(suc(suc(suc(X_662))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_662)))) | 'LE'(f(X_662), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_662))), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_336 : [bind(X_591, $fot(X_662))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_338, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_662)))) |
% 5.57/5.78       'E'(f(suc(suc(X_662))), f(suc(suc(suc(X_662))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_662)))) | 'LE'(f(X_662), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_662))), s(s(0)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(suc(X_662))))))],
% 5.57/5.78                [refute_0_331, refute_0_337])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_339, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_663)))) |
% 5.57/5.78       'E'(f(suc(suc(X_663))), f(suc(suc(suc(X_663))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_663)))) | 'LE'(f(X_663), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_663))), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_338 : [bind(X_662, $fot(X_663))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_340, plain,
% 5.57/5.78      ('E'(f(suc(suc(X_663))), f(suc(suc(suc(X_663))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_663)))) | 'LE'(f(X_663), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_663))), s(s(0)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_663)))))],
% 5.57/5.78                [refute_0_330, refute_0_339])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_341, plain,
% 5.57/5.78      ('E'(f(suc(suc(X_664))), f(suc(suc(suc(X_664))))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_664)))) | 'LE'(f(X_664), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_664))), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_340 : [bind(X_663, $fot(X_664))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_342, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_664)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_664))), suc(suc(suc(X_664)))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_664)))) | 'LE'(f(X_664), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_664))), s(s(0)))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf('E'(f(suc(suc(X_664))), f(suc(suc(suc(X_664))))))],
% 5.57/5.78                [refute_0_341, refute_0_329])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_343, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_665)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_665))), suc(suc(suc(X_665)))) |
% 5.57/5.78       'E'(s(0), f(suc(suc(X_665)))) | 'LE'(f(X_665), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_665))), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_342 : [bind(X_664, $fot(X_665))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_344, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_665)))) | 'E'(s(0), f(suc(suc(X_665)))) |
% 5.57/5.78       'LE'(f(X_665), s(0)) | 'LE'(f(suc(suc(X_665))), s(s(0)))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf(iLEQ(suc(suc(suc(X_665))), suc(suc(suc(X_665)))))],
% 5.57/5.78                [refute_0_328, refute_0_343])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_345, plain,
% 5.57/5.78      (~ 'E'(s(s(0)), f(suc(suc(X_666)))) | 'E'(s(0), f(suc(suc(X_666)))) |
% 5.57/5.78       'LE'(f(X_666), s(0)) | 'LE'(f(suc(suc(X_666))), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_344 : [bind(X_665, $fot(X_666))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_346, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_666)))) | 'LE'(f(X_666), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_666))), s(s(0)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(s(0)), f(suc(suc(X_666)))))],
% 5.57/5.78                [refute_0_319, refute_0_345])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_347, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_667)))) | 'LE'(f(X_667), s(0)) |
% 5.57/5.78       'LE'(f(suc(suc(X_667))), s(s(0)))),
% 5.57/5.78      inference(subst, [], [refute_0_346 : [bind(X_666, $fot(X_667))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_348, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_667)))) | 'LE'(f(X_667), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(suc(suc(X_667))), s(s(0))))],
% 5.57/5.78                [refute_0_347, refute_0_316])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_349, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(X_668)))) | 'LE'(f(X_668), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_348 : [bind(X_667, $fot(X_668))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_350, plain,
% 5.57/5.78      (~ 'E'(f(X_668), f(suc(X_668))) | ~ 'E'(s(0), f(X_668)) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_668))) | 'LE'(f(X_668), s(0)) |
% 5.57/5.78       iLEQ(suc(X_668), suc(X_668))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_668)))))],
% 5.57/5.78                [refute_0_349, refute_0_315])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_351, plain,
% 5.57/5.78      (~ 'E'(f(X_679), f(suc(X_679))) | ~ 'E'(s(0), f(X_679)) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_679))) | 'LE'(f(X_679), s(0)) |
% 5.57/5.78       iLEQ(suc(X_679), suc(X_679))),
% 5.57/5.78      inference(subst, [], [refute_0_350 : [bind(X_668, $fot(X_679))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_352, plain,
% 5.57/5.78      (~ 'E'(f(X_679), f(suc(X_679))) | ~ 'E'(s(0), f(X_679)) |
% 5.57/5.78       'LE'(f(X_679), s(0)) | iLEQ(suc(X_679), suc(X_679))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_679))))],
% 5.57/5.78                [refute_0_314, refute_0_351])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_353, plain,
% 5.57/5.78      (~ 'E'(f(suc(B_93)), f(suc(suc(B_93)))) | ~ 'E'(s(0), f(suc(B_93))) |
% 5.57/5.78       'LE'(f(suc(B_93)), s(0)) | iLEQ(suc(suc(B_93)), suc(suc(B_93)))),
% 5.57/5.78      inference(subst, [], [refute_0_352 : [bind(X_679, $fot(suc(B_93)))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_354, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(B_93))) | 'E'(0, f(suc(B_93))) | 'LE'(f(B_93), 0) |
% 5.57/5.78       'LE'(f(suc(B_93)), s(0)) | iLEQ(suc(suc(B_93)), suc(suc(B_93)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(f(suc(B_93)), f(suc(suc(B_93)))))],
% 5.57/5.78                [refute_0_313, refute_0_353])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_355, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_691))) | 'E'(0, f(suc(X_691))) |
% 5.57/5.78       'LE'(f(X_691), 0) | 'LE'(f(suc(X_691)), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(X_691)), suc(suc(X_691)))),
% 5.57/5.78      inference(subst, [], [refute_0_354 : [bind(B_93, $fot(X_691))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_356, plain,
% 5.57/5.78      ('E'(0, f(suc(X_691))) | 'LE'(f(X_691), 0) |
% 5.57/5.78       'LE'(f(suc(X_691)), s(0)) | iLEQ(suc(suc(X_691)), suc(suc(X_691)))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_691))))],
% 5.57/5.78                [refute_0_281, refute_0_355])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_357, plain,
% 5.57/5.78      ('E'(0, f(suc(X_733))) | 'LE'(f(X_733), 0) |
% 5.57/5.78       'LE'(f(suc(X_733)), s(0)) | iLEQ(suc(suc(X_733)), suc(suc(X_733)))),
% 5.57/5.78      inference(subst, [], [refute_0_356 : [bind(X_691, $fot(X_733))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_358, plain, ('E'(s(0), f(suc(X_693))) | 'LE'(f(X_693), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_309 : [bind(X_417, $fot(X_693))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_359, plain,
% 5.57/5.78      (~ 'E'(f(X_668), f(suc(X_668))) | ~ 'E'(s(0), f(X_668)) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_668))) | ~ 'E'(s(0), f(suc(suc(X_668)))) |
% 5.57/5.78       ~ iLEQ(suc(X_668), suc(X_668))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [clause_813 :
% 5.57/5.78                 [bind(A_4, $fot(X_668)), bind(B_87, $fot(X_668)),
% 5.57/5.78                  bind(B_88, $fot(X_668))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_360, plain,
% 5.57/5.78      (~ 'E'(f(X_668), f(suc(X_668))) | ~ 'E'(s(0), f(X_668)) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_668))) | ~ iLEQ(suc(X_668), suc(X_668)) |
% 5.57/5.78       'LE'(f(X_668), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_668)))))],
% 5.57/5.78                [refute_0_349, refute_0_359])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_361, plain,
% 5.57/5.78      (~ 'E'(f(X_693), f(suc(X_693))) | ~ 'E'(s(0), f(X_693)) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_693))) | ~ iLEQ(suc(X_693), suc(X_693)) |
% 5.57/5.78       'LE'(f(X_693), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_360 : [bind(X_668, $fot(X_693))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_362, plain,
% 5.57/5.78      (~ 'E'(f(X_693), f(suc(X_693))) | ~ 'E'(s(0), f(X_693)) |
% 5.57/5.78       ~ iLEQ(suc(X_693), suc(X_693)) | 'LE'(f(X_693), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_693))))],
% 5.57/5.78                [refute_0_358, refute_0_361])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_363, plain,
% 5.57/5.78      (~ 'E'(f(suc(X_709)), f(suc(suc(X_709)))) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(X_709))) |
% 5.57/5.78       ~ iLEQ(suc(suc(X_709)), suc(suc(X_709))) | 'LE'(f(suc(X_709)), s(0))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_362 : [bind(X_693, $fot(suc(X_709)))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_364, plain,
% 5.57/5.78      ('E'(0, f(suc(X_708))) | 'E'(s(0), f(suc(X_708))) | 'LE'(f(X_708), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_279 : [bind(B_93, $fot(X_708))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_365, plain,
% 5.57/5.78      (~ 'E'(s(0), f(X_418)) | ~ 'E'(s(0), f(suc(X_418))) |
% 5.57/5.78       ~ iLEQ(suc(X_418), suc(X_418)) | 'E'(f(X_418), f(suc(X_418)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [clause_694 :
% 5.57/5.78                 [bind(A_4, $fot(X_418)), bind(B_87, $fot(X_418)),
% 5.57/5.78                  bind(B_88, $fot(X_418))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_366, plain,
% 5.57/5.78      (~ 'E'(s(0), f(X_418)) | ~ iLEQ(suc(X_418), suc(X_418)) |
% 5.57/5.78       'E'(f(X_418), f(suc(X_418))) | 'LE'(f(X_418), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_418))))],
% 5.57/5.78                [refute_0_310, refute_0_365])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_367, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_692))) |
% 5.57/5.78       ~ iLEQ(suc(suc(X_692)), suc(suc(X_692))) |
% 5.57/5.78       'E'(f(suc(X_692)), f(suc(suc(X_692)))) | 'LE'(f(suc(X_692)), s(0))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_366 : [bind(X_418, $fot(suc(X_692)))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_368, plain,
% 5.57/5.78      ('E'(0, f(suc(X_692))) | 'LE'(f(X_692), 0) |
% 5.57/5.78       'LE'(f(suc(X_692)), s(0)) | iLEQ(suc(suc(X_692)), suc(suc(X_692)))),
% 5.57/5.78      inference(subst, [], [refute_0_356 : [bind(X_691, $fot(X_692))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_369, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_692))) | 'E'(0, f(suc(X_692))) |
% 5.57/5.78       'E'(f(suc(X_692)), f(suc(suc(X_692)))) | 'LE'(f(X_692), 0) |
% 5.57/5.78       'LE'(f(suc(X_692)), s(0))),
% 5.57/5.78      inference(resolve, [$cnf(iLEQ(suc(suc(X_692)), suc(suc(X_692))))],
% 5.57/5.78                [refute_0_368, refute_0_367])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_370, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_708))) | 'E'(0, f(suc(X_708))) |
% 5.57/5.78       'E'(f(suc(X_708)), f(suc(suc(X_708)))) | 'LE'(f(X_708), 0) |
% 5.57/5.78       'LE'(f(suc(X_708)), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_369 : [bind(X_692, $fot(X_708))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_371, plain,
% 5.57/5.78      ('E'(0, f(suc(X_708))) | 'E'(f(suc(X_708)), f(suc(suc(X_708)))) |
% 5.57/5.78       'LE'(f(X_708), 0) | 'LE'(f(suc(X_708)), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_708))))],
% 5.57/5.78                [refute_0_364, refute_0_370])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_372, plain,
% 5.57/5.78      ('E'(0, f(suc(X_709))) | 'E'(f(suc(X_709)), f(suc(suc(X_709)))) |
% 5.57/5.78       'LE'(f(X_709), 0) | 'LE'(f(suc(X_709)), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_371 : [bind(X_708, $fot(X_709))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_373, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_709))) |
% 5.57/5.78       ~ iLEQ(suc(suc(X_709)), suc(suc(X_709))) | 'E'(0, f(suc(X_709))) |
% 5.57/5.78       'LE'(f(X_709), 0) | 'LE'(f(suc(X_709)), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(f(suc(X_709)), f(suc(suc(X_709)))))],
% 5.57/5.78                [refute_0_372, refute_0_363])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_374, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_733))) |
% 5.57/5.78       ~ iLEQ(suc(suc(X_733)), suc(suc(X_733))) | 'E'(0, f(suc(X_733))) |
% 5.57/5.78       'LE'(f(X_733), 0) | 'LE'(f(suc(X_733)), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_373 : [bind(X_709, $fot(X_733))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_375, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_733))) | 'E'(0, f(suc(X_733))) |
% 5.57/5.78       'LE'(f(X_733), 0) | 'LE'(f(suc(X_733)), s(0))),
% 5.57/5.78      inference(resolve, [$cnf(iLEQ(suc(suc(X_733)), suc(suc(X_733))))],
% 5.57/5.78                [refute_0_357, refute_0_374])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_376, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(X_734))) | 'E'(0, f(suc(X_734))) |
% 5.57/5.78       'LE'(f(X_734), 0) | 'LE'(f(suc(X_734)), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_375 : [bind(X_733, $fot(X_734))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_377, plain,
% 5.57/5.78      ('E'(0, f(suc(X_734))) | 'LE'(f(X_734), 0) |
% 5.57/5.78       'LE'(f(suc(X_734)), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(X_734))))],
% 5.57/5.78                [refute_0_280, refute_0_376])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_378, plain,
% 5.57/5.78      ('E'(0, f(suc(X_735))) | 'LE'(f(X_735), 0) |
% 5.57/5.78       'LE'(f(suc(X_735)), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_377 : [bind(X_734, $fot(X_735))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_379, plain, ('E'(0, f(suc(X_735))) | 'LE'(f(X_735), 0)),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(suc(X_735)), s(0)))],
% 5.57/5.78                [refute_0_378, refute_0_0])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_380, plain, ('E'(0, f(suc(z))) | 'LE'(f(z), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_379 : [bind(X_735, $fot(z))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_381, plain,
% 5.57/5.78      (~ 'LE'(f(suc(suc(X_764))), s(0)) | 'E'(0, f(suc(suc(X_764)))) |
% 5.57/5.78       'LE'(f(X_764), 0)),
% 5.57/5.78      inference(subst, [], [clause_840 : [bind(B_93, $fot(X_764))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_382, plain,
% 5.57/5.78      ('E'(s(0), f(suc(suc(B_93)))) | 'LE'(f(suc(suc(B_93))), s(0))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_277 : [bind(X_360, $fot(suc(suc(B_93))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_383, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(B_93)))) | 'E'(s(0), f(suc(suc(B_93)))) |
% 5.57/5.78       'LE'(f(B_93), 0)),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(suc(suc(B_93))), s(0)))],
% 5.57/5.78                [refute_0_382, clause_840])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_384, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_763)))) | 'E'(s(0), f(suc(suc(X_763)))) |
% 5.57/5.78       'LE'(f(X_763), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_383 : [bind(B_93, $fot(X_763))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_385, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_715)))) | 'E'(s(0), f(suc(suc(X_715)))) |
% 5.57/5.78       'LE'(f(X_715), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_383 : [bind(B_93, $fot(X_715))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_386, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(B_93)))) |
% 5.57/5.78       'E'(f(suc(suc(B_93))), f(suc(suc(suc(B_93))))) |
% 5.57/5.78       'LE'(f(suc(suc(B_93))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(B_93))), suc(suc(suc(B_93))))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_311 : [bind(X_418, $fot(suc(suc(B_93))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_387, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(B_93)))) |
% 5.57/5.78       'E'(f(suc(suc(B_93))), f(suc(suc(suc(B_93))))) | 'LE'(f(B_93), 0) |
% 5.57/5.78       'LE'(f(suc(suc(B_93))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(B_93))), suc(suc(suc(B_93))))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(suc(B_93)))))],
% 5.57/5.78                [refute_0_383, refute_0_386])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_388, plain,
% 5.57/5.78      (~ 'E'(f(suc(suc(B_93))), f(suc(suc(suc(B_93))))) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(suc(B_93)))) | 'LE'(f(suc(suc(B_93))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(B_93))), suc(suc(suc(B_93))))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_352 : [bind(X_679, $fot(suc(suc(B_93))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_389, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(B_93)))) | 'E'(0, f(suc(suc(B_93)))) |
% 5.57/5.78       'LE'(f(B_93), 0) | 'LE'(f(suc(suc(B_93))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(B_93))), suc(suc(suc(B_93))))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf('E'(f(suc(suc(B_93))), f(suc(suc(suc(B_93))))))],
% 5.57/5.78                [refute_0_387, refute_0_388])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_390, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_715)))) | 'E'(0, f(suc(suc(X_715)))) |
% 5.57/5.78       'LE'(f(X_715), 0) | 'LE'(f(suc(suc(X_715))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_715))), suc(suc(suc(X_715))))),
% 5.57/5.78      inference(subst, [], [refute_0_389 : [bind(B_93, $fot(X_715))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_391, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_715)))) | 'LE'(f(X_715), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_715))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_715))), suc(suc(suc(X_715))))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_715)))))],
% 5.57/5.78                [refute_0_385, refute_0_390])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_392, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_762)))) | 'LE'(f(X_762), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_762))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_762))), suc(suc(suc(X_762))))),
% 5.57/5.78      inference(subst, [], [refute_0_391 : [bind(X_715, $fot(X_762))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_393, plain,
% 5.57/5.78      (~ 'E'(f(suc(suc(X_730))), f(suc(suc(suc(X_730))))) |
% 5.57/5.78       ~ 'E'(s(0), f(suc(suc(X_730)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_730))), suc(suc(suc(X_730)))) |
% 5.57/5.78       'LE'(f(suc(suc(X_730))), s(0))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_362 : [bind(X_693, $fot(suc(suc(X_730))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_394, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_729)))) | 'E'(s(0), f(suc(suc(X_729)))) |
% 5.57/5.78       'LE'(f(X_729), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_383 : [bind(B_93, $fot(X_729))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_395, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_716)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_716))), suc(suc(suc(X_716)))) |
% 5.57/5.78       'E'(f(suc(suc(X_716))), f(suc(suc(suc(X_716))))) |
% 5.57/5.78       'LE'(f(suc(suc(X_716))), s(0))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [refute_0_366 : [bind(X_418, $fot(suc(suc(X_716))))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_396, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_716)))) | 'LE'(f(X_716), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_716))), s(0)) |
% 5.57/5.78       iLEQ(suc(suc(suc(X_716))), suc(suc(suc(X_716))))),
% 5.57/5.78      inference(subst, [], [refute_0_391 : [bind(X_715, $fot(X_716))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_397, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_716)))) | 'E'(0, f(suc(suc(X_716)))) |
% 5.57/5.78       'E'(f(suc(suc(X_716))), f(suc(suc(suc(X_716))))) | 'LE'(f(X_716), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_716))), s(0))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf(iLEQ(suc(suc(suc(X_716))), suc(suc(suc(X_716)))))],
% 5.57/5.78                [refute_0_396, refute_0_395])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_398, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_729)))) | 'E'(0, f(suc(suc(X_729)))) |
% 5.57/5.78       'E'(f(suc(suc(X_729))), f(suc(suc(suc(X_729))))) | 'LE'(f(X_729), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_729))), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_397 : [bind(X_716, $fot(X_729))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_399, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_729)))) |
% 5.57/5.78       'E'(f(suc(suc(X_729))), f(suc(suc(suc(X_729))))) | 'LE'(f(X_729), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_729))), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_729)))))],
% 5.57/5.78                [refute_0_394, refute_0_398])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_400, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_730)))) |
% 5.57/5.78       'E'(f(suc(suc(X_730))), f(suc(suc(suc(X_730))))) | 'LE'(f(X_730), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_730))), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_399 : [bind(X_729, $fot(X_730))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_401, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_730)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_730))), suc(suc(suc(X_730)))) |
% 5.57/5.78       'E'(0, f(suc(suc(X_730)))) | 'LE'(f(X_730), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_730))), s(0))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf('E'(f(suc(suc(X_730))), f(suc(suc(suc(X_730))))))],
% 5.57/5.78                [refute_0_400, refute_0_393])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_402, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_762)))) |
% 5.57/5.78       ~ iLEQ(suc(suc(suc(X_762))), suc(suc(suc(X_762)))) |
% 5.57/5.78       'E'(0, f(suc(suc(X_762)))) | 'LE'(f(X_762), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_762))), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_401 : [bind(X_730, $fot(X_762))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_403, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_762)))) | 'E'(0, f(suc(suc(X_762)))) |
% 5.57/5.78       'LE'(f(X_762), 0) | 'LE'(f(suc(suc(X_762))), s(0))),
% 5.57/5.78      inference(resolve,
% 5.57/5.78                [$cnf(iLEQ(suc(suc(suc(X_762))), suc(suc(suc(X_762)))))],
% 5.57/5.78                [refute_0_392, refute_0_402])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_404, plain,
% 5.57/5.78      (~ 'E'(s(0), f(suc(suc(X_763)))) | 'E'(0, f(suc(suc(X_763)))) |
% 5.57/5.78       'LE'(f(X_763), 0) | 'LE'(f(suc(suc(X_763))), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_403 : [bind(X_762, $fot(X_763))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_405, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_763)))) | 'LE'(f(X_763), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_763))), s(0))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(suc(suc(X_763)))))],
% 5.57/5.78                [refute_0_384, refute_0_404])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_406, plain,
% 5.57/5.78      ('E'(0, f(suc(suc(X_764)))) | 'LE'(f(X_764), 0) |
% 5.57/5.78       'LE'(f(suc(suc(X_764))), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_405 : [bind(X_763, $fot(X_764))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_407, plain, ('E'(0, f(suc(suc(X_764)))) | 'LE'(f(X_764), 0)),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(suc(suc(X_764))), s(0)))],
% 5.57/5.78                [refute_0_406, refute_0_381])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_408, plain, ('E'(0, f(suc(suc(z)))) | 'LE'(f(z), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_407 : [bind(X_764, $fot(z))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_409, plain,
% 5.57/5.78      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 5.57/5.78       ~ 'E'(f(z), f(suc(z))) | ~ iLEQ(suc(z), suc(z))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [clause_743 :
% 5.57/5.78                 [bind(A_5, $fot(z)), bind(B_94, $fot(z)),
% 5.57/5.78                  bind(B_95, $fot(z))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_410, plain,
% 5.57/5.78      (~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) | ~ iLEQ(suc(z), suc(z)) |
% 5.57/5.78       'E'(f(z), f(suc(z)))),
% 5.57/5.78      inference(subst, [],
% 5.57/5.78                [clause_303 :
% 5.57/5.78                 [bind(A_5, $fot(z)), bind(B_94, $fot(z)),
% 5.57/5.78                  bind(B_95, $fot(z))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_411, plain,
% 5.57/5.78      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 5.57/5.78       ~ 'E'(f(z), f(suc(z))) | iLEQ(suc(z), suc(z))),
% 5.57/5.78      inference(subst, [], [clause_256 : [bind(A_5, $fot(z))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_412, plain,
% 5.57/5.78      (~ 'LE'(f(X_725), s(0)) | 'E'(0, f(X_725)) | 'LE'(f(X_725), 0)),
% 5.57/5.78      inference(subst, [], [clause_199 : [bind(B_93, $fot(X_725))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_413, plain,
% 5.57/5.78      (~ 'LE'(f(X_361), s(0)) | 'E'(0, f(X_361)) | 'LE'(f(X_361), 0)),
% 5.57/5.78      inference(subst, [], [clause_199 : [bind(B_93, $fot(X_361))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_414, plain, ('E'(s(0), f(X_361)) | 'LE'(f(X_361), s(0))),
% 5.57/5.78      inference(subst, [], [refute_0_277 : [bind(X_360, $fot(X_361))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_415, plain,
% 5.57/5.78      ('E'(0, f(X_361)) | 'E'(s(0), f(X_361)) | 'LE'(f(X_361), 0)),
% 5.57/5.78      inference(resolve, [$cnf('LE'(f(X_361), s(0)))],
% 5.57/5.78                [refute_0_414, refute_0_413])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_416, plain,
% 5.57/5.78      ('E'(0, f(X_724)) | 'E'(s(0), f(X_724)) | 'LE'(f(X_724), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_415 : [bind(X_361, $fot(X_724))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_417, plain,
% 5.57/5.78      ('E'(0, f(X_687)) | 'E'(s(0), f(X_687)) | 'LE'(f(X_687), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_415 : [bind(X_361, $fot(X_687))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_418, plain,
% 5.57/5.78      ('E'(0, f(X_419)) | 'E'(s(0), f(X_419)) | 'LE'(f(X_419), 0)),
% 5.57/5.78      inference(subst, [], [refute_0_415 : [bind(X_361, $fot(X_419))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_419, plain,
% 5.57/5.78      (~ 'E'(s(0), f(X_419)) | 'E'(f(X_419), f(suc(X_419))) |
% 5.57/5.78       'LE'(f(X_419), s(0)) | iLEQ(suc(X_419), suc(X_419))),
% 5.57/5.78      inference(subst, [], [refute_0_311 : [bind(X_418, $fot(X_419))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_420, plain,
% 5.57/5.78      ('E'(0, f(X_419)) | 'E'(f(X_419), f(suc(X_419))) | 'LE'(f(X_419), 0) |
% 5.57/5.78       'LE'(f(X_419), s(0)) | iLEQ(suc(X_419), suc(X_419))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(X_419)))],
% 5.57/5.78                [refute_0_418, refute_0_419])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_421, plain,
% 5.57/5.78      ('E'(0, f(X_680)) | 'E'(f(X_680), f(suc(X_680))) | 'LE'(f(X_680), 0) |
% 5.57/5.78       'LE'(f(X_680), s(0)) | iLEQ(suc(X_680), suc(X_680))),
% 5.57/5.78      inference(subst, [], [refute_0_420 : [bind(X_419, $fot(X_680))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_422, plain,
% 5.57/5.78      (~ 'E'(f(X_680), f(suc(X_680))) | ~ 'E'(s(0), f(X_680)) |
% 5.57/5.78       'LE'(f(X_680), s(0)) | iLEQ(suc(X_680), suc(X_680))),
% 5.57/5.78      inference(subst, [], [refute_0_352 : [bind(X_679, $fot(X_680))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_423, plain,
% 5.57/5.78      (~ 'E'(s(0), f(X_680)) | 'E'(0, f(X_680)) | 'LE'(f(X_680), 0) |
% 5.57/5.78       'LE'(f(X_680), s(0)) | iLEQ(suc(X_680), suc(X_680))),
% 5.57/5.78      inference(resolve, [$cnf('E'(f(X_680), f(suc(X_680))))],
% 5.57/5.78                [refute_0_421, refute_0_422])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_424, plain,
% 5.57/5.78      (~ 'E'(s(0), f(X_687)) | 'E'(0, f(X_687)) | 'LE'(f(X_687), 0) |
% 5.57/5.78       'LE'(f(X_687), s(0)) | iLEQ(suc(X_687), suc(X_687))),
% 5.57/5.78      inference(subst, [], [refute_0_423 : [bind(X_680, $fot(X_687))]])).
% 5.57/5.78  
% 5.57/5.78  cnf(refute_0_425, plain,
% 5.57/5.78      ('E'(0, f(X_687)) | 'LE'(f(X_687), 0) | 'LE'(f(X_687), s(0)) |
% 5.57/5.78       iLEQ(suc(X_687), suc(X_687))),
% 5.57/5.78      inference(resolve, [$cnf('E'(s(0), f(X_687)))],
% 5.57/5.78                [refute_0_417, refute_0_424])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_426, plain,
% 5.57/5.79      ('E'(0, f(X_723)) | 'LE'(f(X_723), 0) | 'LE'(f(X_723), s(0)) |
% 5.57/5.79       iLEQ(suc(X_723), suc(X_723))),
% 5.57/5.79      inference(subst, [], [refute_0_425 : [bind(X_687, $fot(X_723))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_427, plain,
% 5.57/5.79      (~ 'E'(f(X_707), f(suc(X_707))) | ~ 'E'(s(0), f(X_707)) |
% 5.57/5.79       ~ iLEQ(suc(X_707), suc(X_707)) | 'LE'(f(X_707), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_362 : [bind(X_693, $fot(X_707))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_428, plain,
% 5.57/5.79      ('E'(0, f(X_706)) | 'E'(s(0), f(X_706)) | 'LE'(f(X_706), 0)),
% 5.57/5.79      inference(subst, [], [refute_0_415 : [bind(X_361, $fot(X_706))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_429, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_688)) | ~ iLEQ(suc(X_688), suc(X_688)) |
% 5.57/5.79       'E'(f(X_688), f(suc(X_688))) | 'LE'(f(X_688), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_366 : [bind(X_418, $fot(X_688))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_430, plain,
% 5.57/5.79      ('E'(0, f(X_688)) | 'LE'(f(X_688), 0) | 'LE'(f(X_688), s(0)) |
% 5.57/5.79       iLEQ(suc(X_688), suc(X_688))),
% 5.57/5.79      inference(subst, [], [refute_0_425 : [bind(X_687, $fot(X_688))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_431, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_688)) | 'E'(0, f(X_688)) |
% 5.57/5.79       'E'(f(X_688), f(suc(X_688))) | 'LE'(f(X_688), 0) |
% 5.57/5.79       'LE'(f(X_688), s(0))),
% 5.57/5.79      inference(resolve, [$cnf(iLEQ(suc(X_688), suc(X_688)))],
% 5.57/5.79                [refute_0_430, refute_0_429])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_432, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_706)) | 'E'(0, f(X_706)) |
% 5.57/5.79       'E'(f(X_706), f(suc(X_706))) | 'LE'(f(X_706), 0) |
% 5.57/5.79       'LE'(f(X_706), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_431 : [bind(X_688, $fot(X_706))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_433, plain,
% 5.57/5.79      ('E'(0, f(X_706)) | 'E'(f(X_706), f(suc(X_706))) | 'LE'(f(X_706), 0) |
% 5.57/5.79       'LE'(f(X_706), s(0))),
% 5.57/5.79      inference(resolve, [$cnf('E'(s(0), f(X_706)))],
% 5.57/5.79                [refute_0_428, refute_0_432])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_434, plain,
% 5.57/5.79      ('E'(0, f(X_707)) | 'E'(f(X_707), f(suc(X_707))) | 'LE'(f(X_707), 0) |
% 5.57/5.79       'LE'(f(X_707), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_433 : [bind(X_706, $fot(X_707))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_435, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_707)) | ~ iLEQ(suc(X_707), suc(X_707)) |
% 5.57/5.79       'E'(0, f(X_707)) | 'LE'(f(X_707), 0) | 'LE'(f(X_707), s(0))),
% 5.57/5.79      inference(resolve, [$cnf('E'(f(X_707), f(suc(X_707))))],
% 5.57/5.79                [refute_0_434, refute_0_427])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_436, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_723)) | ~ iLEQ(suc(X_723), suc(X_723)) |
% 5.57/5.79       'E'(0, f(X_723)) | 'LE'(f(X_723), 0) | 'LE'(f(X_723), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_435 : [bind(X_707, $fot(X_723))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_437, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_723)) | 'E'(0, f(X_723)) | 'LE'(f(X_723), 0) |
% 5.57/5.79       'LE'(f(X_723), s(0))),
% 5.57/5.79      inference(resolve, [$cnf(iLEQ(suc(X_723), suc(X_723)))],
% 5.57/5.79                [refute_0_426, refute_0_436])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_438, plain,
% 5.57/5.79      (~ 'E'(s(0), f(X_724)) | 'E'(0, f(X_724)) | 'LE'(f(X_724), 0) |
% 5.57/5.79       'LE'(f(X_724), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_437 : [bind(X_723, $fot(X_724))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_439, plain,
% 5.57/5.79      ('E'(0, f(X_724)) | 'LE'(f(X_724), 0) | 'LE'(f(X_724), s(0))),
% 5.57/5.79      inference(resolve, [$cnf('E'(s(0), f(X_724)))],
% 5.57/5.79                [refute_0_416, refute_0_438])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_440, plain,
% 5.57/5.79      ('E'(0, f(X_725)) | 'LE'(f(X_725), 0) | 'LE'(f(X_725), s(0))),
% 5.57/5.79      inference(subst, [], [refute_0_439 : [bind(X_724, $fot(X_725))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_441, plain, ('E'(0, f(X_725)) | 'LE'(f(X_725), 0)),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(X_725), s(0)))],
% 5.57/5.79                [refute_0_440, refute_0_412])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_442, plain, ('E'(0, f(z)) | 'LE'(f(z), 0)),
% 5.57/5.79      inference(subst, [], [refute_0_441 : [bind(X_725, $fot(z))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_443, plain, ('E'(0, f(z))),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_442, clause_546])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_444, plain,
% 5.57/5.79      (~ 'E'(0, f(X_736)) | ~ 'E'(0, f(suc(X_736))) |
% 5.57/5.79       'E'(f(X_736), f(suc(X_736))) | iLEQ(suc(X_736), suc(X_736))),
% 5.57/5.79      inference(subst, [], [clause_106 : [bind(A_5, $fot(X_736))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_445, plain, ('E'(0, f(suc(X_736))) | 'LE'(f(X_736), 0)),
% 5.57/5.79      inference(subst, [], [refute_0_379 : [bind(X_735, $fot(X_736))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_446, plain,
% 5.57/5.79      (~ 'E'(0, f(X_736)) | 'E'(f(X_736), f(suc(X_736))) |
% 5.57/5.79       'LE'(f(X_736), 0) | iLEQ(suc(X_736), suc(X_736))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(suc(X_736))))],
% 5.57/5.79                [refute_0_445, refute_0_444])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_447, plain,
% 5.57/5.79      (~ 'E'(0, f(z)) | 'E'(f(z), f(suc(z))) | 'LE'(f(z), 0) |
% 5.57/5.79       iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(subst, [], [refute_0_446 : [bind(X_736, $fot(z))]])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_448, plain,
% 5.57/5.79      ('E'(f(z), f(suc(z))) | 'LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(z)))],
% 5.57/5.79                [refute_0_443, refute_0_447])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_449, plain, ('E'(f(z), f(suc(z))) | iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_448, clause_546])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_450, plain,
% 5.57/5.79      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 5.57/5.79       iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(f(z), f(suc(z))))],
% 5.57/5.79                [refute_0_449, refute_0_411])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_451, plain,
% 5.57/5.79      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) |
% 5.57/5.79       iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(z)))],
% 5.57/5.79                [refute_0_443, refute_0_450])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_452, plain,
% 5.57/5.79      (~ 'E'(0, f(suc(z))) | 'LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(suc(suc(z)))))],
% 5.57/5.79                [refute_0_408, refute_0_451])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_453, plain, (~ 'E'(0, f(suc(z))) | iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_452, clause_546])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_454, plain, ('LE'(f(z), 0) | iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 5.57/5.79                [refute_0_380, refute_0_453])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_455, plain, (iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_454, clause_546])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_456, plain,
% 5.57/5.79      (~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) | 'E'(f(z), f(suc(z)))),
% 5.57/5.79      inference(resolve, [$cnf(iLEQ(suc(z), suc(z)))],
% 5.57/5.79                [refute_0_455, refute_0_410])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_457, plain, (~ 'E'(0, f(suc(z))) | 'E'(f(z), f(suc(z)))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(z)))],
% 5.57/5.79                [refute_0_443, refute_0_456])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_458, plain, ('E'(f(z), f(suc(z))) | 'LE'(f(z), 0)),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 5.57/5.79                [refute_0_380, refute_0_457])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_459, plain, ('E'(f(z), f(suc(z)))),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_458, clause_546])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_460, plain,
% 5.57/5.79      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) | ~ 'E'(0, f(z)) |
% 5.57/5.79       ~ iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(f(z), f(suc(z))))],
% 5.57/5.79                [refute_0_459, refute_0_409])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_461, plain,
% 5.57/5.79      (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z))) |
% 5.57/5.79       ~ iLEQ(suc(z), suc(z))),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(z)))],
% 5.57/5.79                [refute_0_443, refute_0_460])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_462, plain, (~ 'E'(0, f(suc(suc(z)))) | ~ 'E'(0, f(suc(z)))),
% 5.57/5.79      inference(resolve, [$cnf(iLEQ(suc(z), suc(z)))],
% 5.57/5.79                [refute_0_455, refute_0_461])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_463, plain, (~ 'E'(0, f(suc(z))) | 'LE'(f(z), 0)),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(suc(suc(z)))))],
% 5.57/5.79                [refute_0_408, refute_0_462])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_464, plain, (~ 'E'(0, f(suc(z)))),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_463, clause_546])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_465, plain, ('LE'(f(z), 0)),
% 5.57/5.79      inference(resolve, [$cnf('E'(0, f(suc(z))))],
% 5.57/5.79                [refute_0_380, refute_0_464])).
% 5.57/5.79  
% 5.57/5.79  cnf(refute_0_466, plain, ($false),
% 5.57/5.79      inference(resolve, [$cnf('LE'(f(z), 0))], [refute_0_465, clause_546])).
% 5.57/5.79  % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.57/5.79  
%------------------------------------------------------------------------------