%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO680-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 : n011.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 47.45s 47.76s
% Output : Proof 47.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO680-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.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 07:46:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 47.45/47.76 % SZS status Unsatisfiable for theBenchmark
% 47.45/47.76 % SZS output start Proof for theBenchmark
% 47.45/47.77 cnf(clause_109, axiom,
% 47.45/47.77 ( ~E(0, f(A_4)) | ~E(0, f(suc(A_4))) | iLEQ(suc(A_4), suc(A_4)) ),
% 47.45/47.77 file('theBenchmark.p', clause_109) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_104, axiom,
% 47.45/47.77 ( LE(f(A), s(s(s(s(0))))) ),
% 47.45/47.77 file('theBenchmark.p', clause_104) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_91, axiom,
% 47.45/47.77 ( ~E(s(0), f(A_3)) | ~E(s(0), f(suc(A_3))) | iLEQ(suc(A_3), suc(A_3)) ),
% 47.45/47.77 file('theBenchmark.p', clause_91) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_114, axiom,
% 47.45/47.77 ( ~LE(f(suc(B_60)), s(0)) | E(0, f(suc(B_60))) | LE(f(B_60), 0) ),
% 47.45/47.77 file('theBenchmark.p', clause_114) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_5, axiom,
% 47.45/47.77 ( ~E(s(s(0)), f(A_2)) | ~E(s(s(0)), f(suc(A_2))) | iLEQ(suc(A_2), suc(A_2)) ),
% 47.45/47.77 file('theBenchmark.p', clause_5) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_20, axiom,
% 47.45/47.77 ( ~E(s(s(0)), f(suc(B_42))) | ~E(s(s(0)), f(B_42)) | ~iLEQ(suc(B_42), suc(B_43)) | ~E(s(s(0)), f(suc(A_2))) | ~E(s(s(0)), f(suc(B_43))) | ~iLEQ(suc(A_2), suc(B_42)) | ~E(s(s(0)), f(B_43)) | ~E(s(s(0)), f(A_2)) ),
% 47.45/47.77 file('theBenchmark.p', clause_20) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_71, axiom,
% 47.45/47.77 ( ~iLEQ(suc(B_24), suc(B_25)) | ~E(s(s(s(0))), f(B_25)) | ~E(s(s(s(0))), f(B_24)) | ~iLEQ(suc(A_1), suc(B_24)) | ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(B_24))) | ~E(s(s(s(0))), f(suc(B_25))) | ~E(s(s(s(0))), f(suc(A_1))) ),
% 47.45/47.77 file('theBenchmark.p', clause_71) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_6, axiom,
% 47.45/47.77 ( ~LE(f(B_53), s(s(0))) | E(s(0), f(B_53)) | LE(f(B_53), s(0)) ),
% 47.45/47.77 file('theBenchmark.p', clause_6) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_66, axiom,
% 47.45/47.77 ( ~LE(f(z), 0) ),
% 47.45/47.77 file('theBenchmark.p', clause_66) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_84, axiom,
% 47.45/47.77 ( ~LE(f(suc(B_41)), s(s(s(0)))) | E(s(s(0)), f(suc(B_41))) | LE(f(B_41), s(s(0))) ),
% 47.45/47.77 file('theBenchmark.p', clause_84) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_144, axiom,
% 47.45/47.77 ( ~E(0, f(suc(B_61))) | ~iLEQ(suc(B_61), suc(B_62)) | ~iLEQ(suc(A_4), suc(B_61)) | ~E(0, f(suc(B_62))) | ~E(0, f(B_61)) | ~E(0, f(suc(A_4))) | ~E(0, f(B_62)) | ~E(0, f(A_4)) ),
% 47.45/47.77 file('theBenchmark.p', clause_144) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_127, axiom,
% 47.45/47.77 ( ~LE(f(B_23), s(s(s(s(0))))) | E(s(s(s(0))), f(B_23)) | LE(f(B_23), s(s(s(0)))) ),
% 47.45/47.77 file('theBenchmark.p', clause_127) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_51, axiom,
% 47.45/47.77 ( ~LE(f(B_41), s(s(s(0)))) | E(s(s(0)), f(B_41)) | LE(f(B_41), s(s(0))) ),
% 47.45/47.77 file('theBenchmark.p', clause_51) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_21, axiom,
% 47.45/47.77 ( ~iLEQ(suc(B_54), suc(B_55)) | ~E(s(0), f(suc(A_3))) | ~iLEQ(suc(A_3), suc(B_54)) | ~E(s(0), f(suc(B_55))) | ~E(s(0), f(A_3)) | ~E(s(0), f(B_55)) | ~E(s(0), f(suc(B_54))) | ~E(s(0), f(B_54)) ),
% 47.45/47.77 file('theBenchmark.p', clause_21) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_102, axiom,
% 47.45/47.77 ( ~LE(f(suc(B_23)), s(s(s(s(0))))) | E(s(s(s(0))), f(suc(B_23))) | LE(f(B_23), s(s(s(0)))) ),
% 47.45/47.77 file('theBenchmark.p', clause_102) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_14, axiom,
% 47.45/47.77 ( ~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(A_1))) | iLEQ(suc(A_1), suc(A_1)) ),
% 47.45/47.77 file('theBenchmark.p', clause_14) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_96, axiom,
% 47.45/47.77 ( ~LE(f(B_60), s(0)) | E(0, f(B_60)) | LE(f(B_60), 0) ),
% 47.45/47.77 file('theBenchmark.p', clause_96) ).
% 47.45/47.77
% 47.45/47.77 cnf(clause_15, axiom,
% 47.45/47.77 ( ~LE(f(suc(B_53)), s(s(0))) | E(s(0), f(suc(B_53))) | LE(f(B_53), s(0)) ),
% 47.45/47.77 file('theBenchmark.p', clause_15) ).
% 47.45/47.77
% 47.45/47.77 cnf(sat_proved, plain, $false,
% 47.45/47.77 inference(cadical, [status(thm)], [
% 47.45/47.77 ]) ).
% 47.45/47.77 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------