%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO660-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:12:15 AM UTC 2026
% Result : Unsatisfiable 150.06s 150.39s
% Output : Proof 150.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO660-1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 07:52:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 150.06/150.39 % SZS status Unsatisfiable for theBenchmark
% 150.06/150.39 % SZS output start Proof for theBenchmark
% 150.16/150.42 cnf(clause_1847, axiom,
% 150.16/150.42 ( ~LE(f(suc(B_2)), s(s(0))) | E(s(0), f(suc(B_2))) | LE(f(B_2), s(0)) ),
% 150.16/150.42 file('theBenchmark.p', clause_1847) ).
% 150.16/150.42
% 150.16/150.42 cnf(clause_794, axiom,
% 150.16/150.42 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(A_1))) | E(f(B_3), f(suc(suc(suc(B_3))))) ),
% 150.16/150.42 file('theBenchmark.p', clause_794) ).
% 150.16/150.42
% 150.16/150.42 cnf(clause_1502, axiom,
% 150.16/150.42 ( ~LE(f(z), 0) ),
% 150.16/150.42 file('theBenchmark.p', clause_1502) ).
% 150.16/150.42
% 150.16/150.42 cnf(clause_1962, axiom,
% 150.16/150.42 ( ~LE(f(B_5), s(0)) | E(0, f(B_5)) | LE(f(B_5), 0) ),
% 150.16/150.42 file('theBenchmark.p', clause_1962) ).
% 150.16/150.42
% 150.16/150.42 cnf(clause_2540, axiom,
% 150.16/150.42 ( ~LE(f(suc(suc(B_5))), s(0)) | E(0, f(suc(suc(B_5)))) | LE(f(B_5), 0) ),
% 150.16/150.42 file('theBenchmark.p', clause_2540) ).
% 150.16/150.42
% 150.16/150.42 cnf(clause_1397, axiom,
% 150.16/150.42 ( ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | E(f(A_1), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)) ),
% 150.16/150.42 file('theBenchmark.p', clause_1397) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2034, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(suc(suc(suc(A_1))))))) | ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(suc(suc(suc(B_3))))))) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2034) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2529, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(suc(suc(suc(A_1))))))) | ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(B_3), f(suc(suc(suc(B_3))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2529) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_467, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(A_2))) | E(f(B_6), f(suc(suc(suc(suc(B_6)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_467) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2680, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(A_2))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(B_6), f(suc(suc(B_6)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2680) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2600, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(suc(suc(suc(A_1))))))) | ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(B_3), f(suc(B_3))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2600) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2932, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(f(A_2), f(suc(A_2))) | E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | iLEQ(suc(A_2), suc(A_2)) ),
% 150.16/150.43 file('theBenchmark.p', clause_2932) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2724, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(A_1), f(suc(suc(suc(A_1))))) | E(f(B_3), f(suc(suc(B_3)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2724) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_169, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(A_2))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(0, f(suc(B_6))) | E(f(B_6), f(suc(B_6))) ),
% 150.16/150.43 file('theBenchmark.p', clause_169) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_572, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(A_1), f(suc(suc(suc(A_1))))) | E(f(B_3), f(suc(B_3))) ),
% 150.16/150.43 file('theBenchmark.p', clause_572) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_623, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(A_2))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(B_6), f(suc(suc(suc(B_6))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_623) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_147, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(B_6))))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(A_2))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_147) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2543, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(A_2)))) | E(f(B_6), f(suc(suc(suc(suc(B_6)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2543) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1826, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(A_2)))) | E(f(B_6), f(suc(suc(suc(B_6))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1826) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1946, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(A_2))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(B_6), f(suc(suc(suc(suc(B_6)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1946) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_724, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(A_1)))) | E(f(B_3), f(suc(suc(suc(suc(B_3)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_724) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2580, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(A_1))) | E(f(B_3), f(suc(suc(suc(suc(B_3)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2580) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2384, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(suc(suc(suc(B_3))))))) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(suc(suc(A_1)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2384) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2165, axiom,
% 150.16/150.43 ( ~LE(f(suc(B_5)), s(0)) | E(0, f(suc(B_5))) | LE(f(B_5), 0) ),
% 150.16/150.43 file('theBenchmark.p', clause_2165) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1707, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(B_6))))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(A_2))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1707) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_3037, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | E(f(B_3), f(suc(B_3))) ),
% 150.16/150.43 file('theBenchmark.p', clause_3037) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_733, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(B_6))))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(A_2)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_733) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2700, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(suc(B_5)))), s(0)) | E(0, f(suc(suc(suc(B_5))))) | LE(f(B_5), 0) ),
% 150.16/150.43 file('theBenchmark.p', clause_2700) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1276, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(suc(B_2)))), s(s(0))) | E(s(0), f(suc(suc(suc(B_2))))) | LE(f(B_2), s(0)) ),
% 150.16/150.43 file('theBenchmark.p', clause_1276) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1696, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(A_1)))) | E(f(B_3), f(suc(suc(suc(B_3))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1696) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1388, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | E(f(B_6), f(suc(suc(suc(B_6))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1388) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1114, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(A_2))) | E(f(B_6), f(suc(suc(suc(B_6))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1114) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1574, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(A_2))))) | E(f(B_6), f(suc(suc(suc(B_6))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1574) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2118, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(A_2))))) | E(f(B_6), f(suc(suc(suc(suc(B_6)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2118) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_410, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(suc(suc(B_2))))), s(s(0))) | E(s(0), f(suc(suc(suc(suc(B_2)))))) | LE(f(B_2), s(0)) ),
% 150.16/150.43 file('theBenchmark.p', clause_410) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1151, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | E(f(B_6), f(suc(suc(suc(suc(B_6)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1151) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_669, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | E(f(B_6), f(suc(suc(B_6)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_669) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1225, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | E(f(B_3), f(suc(suc(suc(B_3))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1225) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_664, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | iLEQ(suc(A_1), suc(A_1)) ),
% 150.16/150.43 file('theBenchmark.p', clause_664) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2336, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(B_2))), s(s(0))) | E(s(0), f(suc(suc(B_2)))) | LE(f(B_2), s(0)) ),
% 150.16/150.43 file('theBenchmark.p', clause_2336) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_70, axiom,
% 150.16/150.43 ( ~E(0, f(suc(suc(A_2)))) | ~E(0, f(suc(A_2))) | ~E(f(A_2), f(suc(A_2))) | ~E(0, f(A_2)) | E(f(A_2), f(suc(suc(A_2)))) | iLEQ(suc(A_2), suc(A_2)) ),
% 150.16/150.43 file('theBenchmark.p', clause_70) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_514, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(suc(suc(B_5))))), s(0)) | E(0, f(suc(suc(suc(suc(B_5)))))) | LE(f(B_5), 0) ),
% 150.16/150.43 file('theBenchmark.p', clause_514) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2196, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(f(A_2), f(suc(A_2))) | E(f(A_2), f(suc(suc(suc(A_2))))) | iLEQ(suc(A_2), suc(A_2)) ),
% 150.16/150.43 file('theBenchmark.p', clause_2196) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1410, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(suc(A_1))))) | E(f(B_3), f(suc(suc(suc(suc(B_3)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1410) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1927, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(A_2)))) | E(f(B_6), f(suc(B_6))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1927) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_3120, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(A_2))) | E(f(B_6), f(suc(suc(B_6)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_3120) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1896, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(A_2))))) | E(f(B_6), f(suc(suc(B_6)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1896) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2649, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(suc(suc(suc(B_3))))))) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(A_1)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2649) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_165, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(B_6))))))) | ~E(0, f(suc(suc(suc(suc(suc(A_2))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) ),
% 150.16/150.43 file('theBenchmark.p', clause_165) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_842, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | E(f(B_6), f(suc(B_6))) ),
% 150.16/150.43 file('theBenchmark.p', clause_842) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_344, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(suc(suc(suc(B_3))))))) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(suc(A_1))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_344) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2349, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(A_2))))) | E(f(B_6), f(suc(B_6))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2349) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_997, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(B_6)) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(A_2))) | E(f(B_6), f(suc(B_6))) ),
% 150.16/150.43 file('theBenchmark.p', clause_997) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_249, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~E(0, f(suc(suc(suc(suc(suc(A_2))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(f(A_2), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)) ),
% 150.16/150.43 file('theBenchmark.p', clause_249) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2494, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(suc(A_1))))) | E(f(B_3), f(suc(suc(suc(B_3))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2494) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1158, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(suc(suc(suc(B_3))))))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(A_1))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1158) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1595, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(suc(suc(suc(B_2)))))), s(s(0))) | E(s(0), f(suc(suc(suc(suc(suc(B_2))))))) | LE(f(B_2), s(0)) ),
% 150.16/150.43 file('theBenchmark.p', clause_1595) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1195, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(f(A_2), f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(suc(suc(suc(suc(suc(B_6))))))) | ~E(0, f(suc(suc(suc(suc(A_2)))))) | ~E(0, f(suc(suc(suc(B_6))))) | ~E(f(A_2), f(suc(suc(suc(A_2))))) | ~E(0, f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(A_2))))) | ~E(0, f(B_6)) | ~E(f(B_6), f(suc(suc(suc(suc(B_6)))))) | ~E(f(B_6), f(suc(suc(B_6)))) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(suc(suc(A_2)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1195) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1204, axiom,
% 150.16/150.43 ( ~LE(f(suc(suc(suc(suc(suc(B_5)))))), s(0)) | E(0, f(suc(suc(suc(suc(suc(B_5))))))) | LE(f(B_5), 0) ),
% 150.16/150.43 file('theBenchmark.p', clause_1204) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1186, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | E(f(A_1), f(suc(A_1))) | E(f(B_3), f(suc(suc(B_3)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1186) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_934, axiom,
% 150.16/150.43 ( ~LE(f(B_2), s(s(0))) | E(s(0), f(B_2)) | LE(f(B_2), s(0)) ),
% 150.16/150.43 file('theBenchmark.p', clause_934) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1137, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(A_1))) | E(f(A_1), f(suc(suc(A_1)))) | E(f(B_3), f(suc(B_3))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1137) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1944, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(suc(suc(suc(A_1))))))) | ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(B_3), f(suc(suc(B_3)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1944) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2717, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | E(f(B_3), f(suc(suc(suc(suc(B_3)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2717) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2795, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(A_1), f(suc(suc(suc(A_1))))) | iLEQ(suc(A_1), suc(A_1)) ),
% 150.16/150.43 file('theBenchmark.p', clause_2795) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_692, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(A_1))))) | E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | E(f(B_3), f(suc(suc(B_3)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_692) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2550, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | E(f(A_1), f(suc(A_1))) | E(f(B_3), f(suc(B_3))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2550) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1325, axiom,
% 150.16/150.43 ( ~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6)))) | ~E(0, f(suc(suc(A_2)))) | ~E(0, f(A_2)) | ~iLEQ(suc(A_2), suc(B_6)) | ~E(0, f(B_6)) | ~E(f(A_2), f(suc(A_2))) | ~E(f(B_6), f(suc(B_6))) | ~E(0, f(suc(B_6))) | E(f(A_2), f(suc(suc(A_2)))) | E(f(B_6), f(suc(suc(B_6)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1325) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_720, axiom,
% 150.16/150.43 ( ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | E(f(A_1), f(suc(suc(A_1)))) | E(f(B_3), f(suc(suc(B_3)))) ),
% 150.16/150.43 file('theBenchmark.p', clause_720) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1634, axiom,
% 150.16/150.43 ( ~E(0, f(A_2)) | ~E(0, f(suc(A_2))) | E(f(A_2), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)) ),
% 150.16/150.43 file('theBenchmark.p', clause_1634) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_307, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(A_1))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(0), f(A_1)) | E(f(A_1), f(suc(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)) ),
% 150.16/150.43 file('theBenchmark.p', clause_307) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2827, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(suc(suc(suc(A_1))))))) | ~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(suc(suc(suc(B_3)))))) | ~E(s(0), f(A_1)) | ~E(s(0), f(suc(suc(B_3)))) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(B_3))))) | ~E(s(0), f(suc(B_3))) | ~E(s(0), f(B_3)) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(B_3), f(suc(B_3))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(B_3), f(suc(suc(suc(B_3))))) | ~E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | ~E(f(B_3), f(suc(suc(B_3)))) | E(f(B_3), f(suc(suc(suc(suc(B_3)))))) ),
% 150.16/150.43 file('theBenchmark.p', clause_2827) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_1215, axiom,
% 150.16/150.43 ( LE(f(A), s(s(0))) ),
% 150.16/150.43 file('theBenchmark.p', clause_1215) ).
% 150.16/150.43
% 150.16/150.43 cnf(clause_2367, axiom,
% 150.16/150.43 ( ~E(s(0), f(suc(suc(suc(suc(suc(A_1))))))) | ~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(A_1)) | ~E(f(A_1), f(suc(suc(suc(A_1))))) | ~E(s(0), f(suc(A_1))) | ~E(s(0), f(suc(suc(suc(suc(A_1)))))) | ~E(f(A_1), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(f(A_1), f(suc(suc(suc(suc(A_1)))))) | ~E(s(0), f(suc(suc(suc(A_1))))) | iLEQ(suc(A_1), suc(A_1)) ),
% 150.16/150.43 file('theBenchmark.p', clause_2367) ).
% 150.16/150.43
% 150.16/150.43 cnf(sat_proved, plain, $false,
% 150.16/150.43 inference(cadical, [status(thm)], [
% 150.16/150.45 ]) ).
% 150.16/150.45 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------