%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO677-1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:16 AM UTC 2026
% Result : Unsatisfiable 63.03s 63.32s
% Output : Proof 63.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO677-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/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.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:46:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 63.03/63.32 % SZS status Unsatisfiable for theBenchmark
% 63.03/63.32 % SZS output start Proof for theBenchmark
% 63.03/63.33 cnf(clause_24, axiom,
% 63.03/63.33 ( ~E(s(s(0)), f(B_10)) | ~E(s(s(0)), f(suc(A_2))) | ~E(f(B_10), f(suc(B_10))) | ~iLEQ(suc(A_2), suc(B_10)) | ~E(s(s(0)), f(suc(B_10))) | ~E(s(s(0)), f(suc(suc(A_2)))) | ~E(s(s(0)), f(A_2)) | ~E(f(A_2), f(suc(A_2))) | ~E(s(s(0)), f(suc(suc(B_10)))) ),
% 63.03/63.33 file('theBenchmark.p', clause_24) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_23, axiom,
% 63.03/63.33 ( ~E(0, f(suc(B_17))) | ~iLEQ(suc(A_4), suc(B_17)) | ~E(0, f(suc(suc(B_17)))) | ~E(0, f(B_17)) | ~E(0, f(suc(A_4))) | ~E(f(B_17), f(suc(B_17))) | ~E(0, f(A_4)) | E(f(A_4), f(suc(A_4))) ),
% 63.03/63.33 file('theBenchmark.p', clause_23) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_143, axiom,
% 63.03/63.33 ( ~LE(f(suc(suc(B_4))), s(s(s(s(0))))) | E(s(s(s(0))), f(suc(suc(B_4)))) | LE(f(B_4), s(s(s(0)))) ),
% 63.03/63.33 file('theBenchmark.p', clause_143) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_59, axiom,
% 63.03/63.33 ( ~E(s(s(s(0))), f(suc(B_5))) | ~iLEQ(suc(A_1), suc(B_5)) | ~E(s(s(s(0))), f(B_5)) | ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(s(s(0))), f(suc(A_1))) | E(f(B_5), f(suc(B_5))) ),
% 63.03/63.33 file('theBenchmark.p', clause_59) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_7, axiom,
% 63.03/63.33 ( ~E(f(A_4), f(suc(A_4))) | ~E(0, f(suc(B_17))) | ~iLEQ(suc(A_4), suc(B_17)) | ~E(0, f(suc(suc(A_4)))) | ~E(0, f(B_17)) | ~E(0, f(suc(A_4))) | ~E(0, f(A_4)) | E(f(B_17), f(suc(B_17))) ),
% 63.03/63.33 file('theBenchmark.p', clause_7) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_38, axiom,
% 63.03/63.33 ( ~E(s(s(0)), f(B_10)) | ~E(s(s(0)), f(suc(A_2))) | ~iLEQ(suc(A_2), suc(B_10)) | ~E(s(s(0)), f(suc(B_10))) | ~E(s(s(0)), f(A_2)) | E(f(A_2), f(suc(A_2))) | E(f(B_10), f(suc(B_10))) ),
% 63.03/63.33 file('theBenchmark.p', clause_38) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_15, axiom,
% 63.03/63.33 ( ~LE(f(B_13), s(s(0))) | E(s(0), f(B_13)) | LE(f(B_13), s(0)) ),
% 63.03/63.33 file('theBenchmark.p', clause_15) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_74, axiom,
% 63.03/63.33 ( ~E(s(0), f(suc(B_14))) | ~E(s(0), f(suc(suc(B_14)))) | ~E(s(0), f(suc(A_3))) | ~E(s(0), f(B_14)) | ~E(f(B_14), f(suc(B_14))) | ~E(s(0), f(A_3)) | ~iLEQ(suc(A_3), suc(B_14)) | E(f(A_3), f(suc(A_3))) ),
% 63.03/63.33 file('theBenchmark.p', clause_74) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_13, axiom,
% 63.03/63.33 ( ~LE(f(suc(B_4)), s(s(s(s(0))))) | E(s(s(s(0))), f(suc(B_4))) | LE(f(B_4), s(s(s(0)))) ),
% 63.03/63.33 file('theBenchmark.p', clause_13) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_51, axiom,
% 63.03/63.33 ( ~E(s(s(s(0))), f(suc(B_5))) | ~iLEQ(suc(A_1), suc(B_5)) | ~E(s(s(s(0))), f(B_5)) | ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(A_1))) | E(f(A_1), f(suc(A_1))) | E(f(B_5), f(suc(B_5))) ),
% 63.03/63.33 file('theBenchmark.p', clause_51) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_91, axiom,
% 63.03/63.33 ( ~E(s(0), f(suc(B_14))) | ~E(s(0), f(suc(A_3))) | ~E(s(0), f(B_14)) | ~E(f(A_3), f(suc(A_3))) | ~E(s(0), f(A_3)) | ~E(s(0), f(suc(suc(A_3)))) | ~iLEQ(suc(A_3), suc(B_14)) | E(f(B_14), f(suc(B_14))) ),
% 63.03/63.33 file('theBenchmark.p', clause_91) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_97, axiom,
% 63.03/63.33 ( ~E(s(s(0)), f(suc(suc(A_2)))) | ~E(s(s(0)), f(suc(A_2))) | ~E(f(A_2), f(suc(A_2))) | ~E(s(s(0)), f(A_2)) | iLEQ(suc(A_2), suc(A_2)) ),
% 63.03/63.33 file('theBenchmark.p', clause_97) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_2, axiom,
% 63.03/63.33 ( ~LE(f(suc(B_16)), s(0)) | E(0, f(suc(B_16))) | LE(f(B_16), 0) ),
% 63.03/63.33 file('theBenchmark.p', clause_2) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_145, axiom,
% 63.03/63.33 ( ~LE(f(B_16), s(0)) | E(0, f(B_16)) | LE(f(B_16), 0) ),
% 63.03/63.33 file('theBenchmark.p', clause_145) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_18, axiom,
% 63.03/63.33 ( ~LE(f(suc(suc(B_9))), s(s(s(0)))) | E(s(s(0)), f(suc(suc(B_9)))) | LE(f(B_9), s(s(0))) ),
% 63.03/63.33 file('theBenchmark.p', clause_18) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_61, axiom,
% 63.03/63.33 ( ~LE(f(B_4), s(s(s(s(0))))) | E(s(s(s(0))), f(B_4)) | LE(f(B_4), s(s(s(0)))) ),
% 63.03/63.33 file('theBenchmark.p', clause_61) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_0, axiom,
% 63.03/63.33 ( ~E(0, f(suc(B_17))) | ~iLEQ(suc(A_4), suc(B_17)) | ~E(0, f(B_17)) | ~E(0, f(suc(A_4))) | ~E(0, f(A_4)) | E(f(A_4), f(suc(A_4))) | E(f(B_17), f(suc(B_17))) ),
% 63.03/63.33 file('theBenchmark.p', clause_0) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_113, axiom,
% 63.03/63.33 ( LE(f(A), s(s(s(s(0))))) ),
% 63.03/63.33 file('theBenchmark.p', clause_113) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_73, axiom,
% 63.03/63.33 ( ~LE(f(B_9), s(s(s(0)))) | E(s(s(0)), f(B_9)) | LE(f(B_9), s(s(0))) ),
% 63.03/63.33 file('theBenchmark.p', clause_73) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_48, axiom,
% 63.03/63.33 ( ~E(f(A_4), f(suc(A_4))) | ~E(0, f(suc(B_17))) | ~iLEQ(suc(A_4), suc(B_17)) | ~E(0, f(suc(suc(B_17)))) | ~E(0, f(suc(suc(A_4)))) | ~E(0, f(B_17)) | ~E(0, f(suc(A_4))) | ~E(f(B_17), f(suc(B_17))) | ~E(0, f(A_4)) ),
% 63.03/63.33 file('theBenchmark.p', clause_48) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_10, axiom,
% 63.03/63.33 ( ~E(s(s(s(0))), f(suc(B_5))) | ~E(f(B_5), f(suc(B_5))) | ~iLEQ(suc(A_1), suc(B_5)) | ~E(s(s(s(0))), f(B_5)) | ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(suc(B_5)))) | ~E(s(s(s(0))), f(suc(A_1))) | E(f(A_1), f(suc(A_1))) ),
% 63.03/63.33 file('theBenchmark.p', clause_10) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_140, axiom,
% 63.03/63.33 ( ~E(s(s(s(0))), f(suc(suc(A_1)))) | ~E(s(s(s(0))), f(suc(A_1))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(s(s(0))), f(A_1)) | iLEQ(suc(A_1), suc(A_1)) ),
% 63.03/63.33 file('theBenchmark.p', clause_140) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_150, axiom,
% 63.03/63.33 ( ~E(0, f(A_4)) | ~E(0, f(suc(A_4))) | E(f(A_4), f(suc(A_4))) | iLEQ(suc(A_4), suc(A_4)) ),
% 63.03/63.33 file('theBenchmark.p', clause_150) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_31, axiom,
% 63.03/63.33 ( ~E(s(0), f(suc(suc(A_3)))) | ~E(s(0), f(suc(A_3))) | ~E(f(A_3), f(suc(A_3))) | ~E(s(0), f(A_3)) | iLEQ(suc(A_3), suc(A_3)) ),
% 63.03/63.33 file('theBenchmark.p', clause_31) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_39, axiom,
% 63.03/63.33 ( ~LE(f(suc(B_13)), s(s(0))) | E(s(0), f(suc(B_13))) | LE(f(B_13), s(0)) ),
% 63.03/63.33 file('theBenchmark.p', clause_39) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_11, axiom,
% 63.03/63.33 ( ~E(s(s(0)), f(B_10)) | ~E(s(s(0)), f(suc(A_2))) | ~iLEQ(suc(A_2), suc(B_10)) | ~E(s(s(0)), f(suc(B_10))) | ~E(s(s(0)), f(suc(suc(A_2)))) | ~E(s(s(0)), f(A_2)) | ~E(f(A_2), f(suc(A_2))) | E(f(B_10), f(suc(B_10))) ),
% 63.03/63.33 file('theBenchmark.p', clause_11) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_49, axiom,
% 63.03/63.33 ( ~LE(f(suc(suc(B_13))), s(s(0))) | E(s(0), f(suc(suc(B_13)))) | LE(f(B_13), s(0)) ),
% 63.03/63.33 file('theBenchmark.p', clause_49) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_77, axiom,
% 63.03/63.33 ( ~LE(f(z), 0) ),
% 63.03/63.33 file('theBenchmark.p', clause_77) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_57, axiom,
% 63.03/63.33 ( ~E(s(0), f(suc(B_14))) | ~E(s(0), f(suc(suc(B_14)))) | ~E(s(0), f(suc(A_3))) | ~E(s(0), f(B_14)) | ~E(f(B_14), f(suc(B_14))) | ~E(f(A_3), f(suc(A_3))) | ~E(s(0), f(A_3)) | ~E(s(0), f(suc(suc(A_3)))) | ~iLEQ(suc(A_3), suc(B_14)) ),
% 63.03/63.33 file('theBenchmark.p', clause_57) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_121, axiom,
% 63.03/63.33 ( ~E(s(s(s(0))), f(suc(B_5))) | ~E(f(B_5), f(suc(B_5))) | ~iLEQ(suc(A_1), suc(B_5)) | ~E(s(s(s(0))), f(B_5)) | ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(suc(A_1)))) | ~E(f(A_1), f(suc(A_1))) | ~E(s(s(s(0))), f(suc(suc(B_5)))) | ~E(s(s(s(0))), f(suc(A_1))) ),
% 63.03/63.33 file('theBenchmark.p', clause_121) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_87, axiom,
% 63.03/63.33 ( ~LE(f(suc(B_9)), s(s(s(0)))) | E(s(s(0)), f(suc(B_9))) | LE(f(B_9), s(s(0))) ),
% 63.03/63.33 file('theBenchmark.p', clause_87) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_65, axiom,
% 63.03/63.33 ( ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(A_1))) | E(f(A_1), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)) ),
% 63.03/63.33 file('theBenchmark.p', clause_65) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_99, axiom,
% 63.03/63.33 ( ~E(s(s(0)), f(B_10)) | ~E(s(s(0)), f(suc(A_2))) | ~E(f(B_10), f(suc(B_10))) | ~iLEQ(suc(A_2), suc(B_10)) | ~E(s(s(0)), f(suc(B_10))) | ~E(s(s(0)), f(A_2)) | ~E(s(s(0)), f(suc(suc(B_10)))) | E(f(A_2), f(suc(A_2))) ),
% 63.03/63.33 file('theBenchmark.p', clause_99) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_84, axiom,
% 63.03/63.33 ( ~E(s(s(0)), f(A_2)) | ~E(s(s(0)), f(suc(A_2))) | E(f(A_2), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)) ),
% 63.03/63.33 file('theBenchmark.p', clause_84) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_112, axiom,
% 63.03/63.33 ( ~E(s(0), f(suc(B_14))) | ~E(s(0), f(suc(A_3))) | ~E(s(0), f(B_14)) | ~E(s(0), f(A_3)) | ~iLEQ(suc(A_3), suc(B_14)) | E(f(A_3), f(suc(A_3))) | E(f(B_14), f(suc(B_14))) ),
% 63.03/63.33 file('theBenchmark.p', clause_112) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_27, axiom,
% 63.03/63.33 ( ~LE(f(suc(suc(B_16))), s(0)) | E(0, f(suc(suc(B_16)))) | LE(f(B_16), 0) ),
% 63.03/63.33 file('theBenchmark.p', clause_27) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_115, axiom,
% 63.03/63.33 ( ~E(s(0), f(A_3)) | ~E(s(0), f(suc(A_3))) | E(f(A_3), f(suc(A_3))) | iLEQ(suc(A_3), suc(A_3)) ),
% 63.03/63.33 file('theBenchmark.p', clause_115) ).
% 63.03/63.33
% 63.03/63.33 cnf(clause_114, axiom,
% 63.03/63.33 ( ~E(0, f(suc(suc(A_4)))) | ~E(0, f(suc(A_4))) | ~E(f(A_4), f(suc(A_4))) | ~E(0, f(A_4)) | iLEQ(suc(A_4), suc(A_4)) ),
% 63.03/63.33 file('theBenchmark.p', clause_114) ).
% 63.03/63.33
% 63.03/63.33 cnf(sat_proved, plain, $false,
% 63.03/63.33 inference(cadical, [status(thm)], [
% 63.03/63.34 ]) ).
% 63.03/63.34 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------