%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO629-1 : TPTP v9.3.1. Released v7.1.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 : n008.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:12 AM UTC 2026
% Result : Unsatisfiable 0.09s 0.38s
% Output : Proof 0.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO629-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.03 % 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 : n008.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:42:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % SZS status Unsatisfiable for theBenchmark
% 0.09/0.38 % SZS output start Proof for theBenchmark
% 0.09/0.38 cnf(clause_8_01, axiom,
% 0.09/0.38 ( ~E(f(A_3), f(g(A_3))) ),
% 0.09/0.38 file('theBenchmark.p', clause_8_01) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_11_03, axiom,
% 0.09/0.38 ( ~E(0, f(A_3)) | ~E(0, f(g(A_3))) | E(f(A_3), f(g(A_3))) ),
% 0.09/0.38 file('theBenchmark.p', clause_11_03) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_6_04, axiom,
% 0.09/0.38 ( E(s(0), f(A)) | LE(f(A), s(0)) ),
% 0.09/0.38 file('theBenchmark.p', clause_6_04) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_10_06, axiom,
% 0.09/0.38 ( ~LE(f(A_1), s(0)) | ~iLEQ(A_1, B_0) | E(0, f(B_0)) | LE(f(B_0), 0) ),
% 0.09/0.38 file('theBenchmark.p', clause_10_06) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_1_07, axiom,
% 0.09/0.38 ( ~E(s(0), f(A_2)) | ~E(s(0), f(g(A_2))) | E(f(A_2), f(g(A_2))) ),
% 0.09/0.38 file('theBenchmark.p', clause_1_07) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_2_08, axiom,
% 0.09/0.38 ( ~LE(f(g(A_3)), 0) ),
% 0.09/0.38 file('theBenchmark.p', clause_2_08) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_5_10, axiom,
% 0.09/0.38 ( iLEQ(A_2, g(A_2)) ),
% 0.09/0.38 file('theBenchmark.p', clause_5_10) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_4_11, axiom,
% 0.09/0.38 ( ~E(f(A_2), f(g(A_2))) ),
% 0.09/0.38 file('theBenchmark.p', clause_4_11) ).
% 0.09/0.38
% 0.09/0.38 cnf(clause_9_12, axiom,
% 0.09/0.38 ( iLEQ(A_2, A_2) ),
% 0.09/0.38 file('theBenchmark.p', clause_9_12) ).
% 0.09/0.38
% 0.09/0.38 cnf(t1, plain, ( ~E(f(g(U_74)), f(g(g(U_74)))) ),
% 0.09/0.38 inference(start, [status(thm), parent(0:0)], [clause_8_01]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t2, plain, ( E(f(g(U_74)), f(g(g(U_74)))) | ~E(s(0), f(g(U_74))) | ~E(s(0), f(g(g(U_74)))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t1:1)], [clause_1_07]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t3, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t2:1)], [t2:1,t1:1]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t4, plain, ( E(s(0), f(g(U_74))) | LE(f(g(U_74)), s(0)) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t2:2)], [clause_6_04]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t5, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t4:1)], [t4:1,t2:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t6, plain, ( ~LE(f(g(U_74)), s(0)) | LE(f(g(g(U_74))), 0) | E(0, f(g(g(U_74)))) | ~iLEQ(g(U_74), g(g(U_74))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t4:2)], [clause_10_06]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t7, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t6:1)], [t6:1,t4:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t8, plain, ( ~LE(f(g(g(U_74))), 0) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t6:2)], [clause_2_08]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t9, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t8:1)], [t8:1,t6:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t10, plain, ( ~E(0, f(g(g(U_74)))) | ~E(0, f(g(U_74))) | E(f(g(U_74)), f(g(g(U_74)))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t6:3)], [clause_11_03]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t11, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t10:1)], [t10:1,t6:3]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t12, plain, ( E(0, f(g(U_74))) | ~LE(f(g(U_74)), s(0)) | LE(f(g(U_74)), 0) | ~iLEQ(g(U_74), g(U_74)) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t10:2)], [clause_10_06]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t13, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t12:1)], [t12:1,t10:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t14, plain, $false,
% 0.09/0.38 inference(reduction, [status(thm), parent(t12:2)], [t12:2,t4:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t15, plain, ( ~LE(f(g(U_74)), 0) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t12:3)], [clause_2_08]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t16, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t15:1)], [t15:1,t12:3]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t17, plain, ( iLEQ(g(U_74), g(U_74)) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t12:4)], [clause_9_12]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t18, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t17:1)], [t17:1,t12:4]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t19, plain, $false,
% 0.09/0.38 inference(reduction, [status(thm), parent(t10:3)], [t10:3,t1:1]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t20, plain, ( iLEQ(g(U_74), g(g(U_74))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t6:4)], [clause_5_10]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t21, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t20:1)], [t20:1,t6:4]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t22, plain, ( E(s(0), f(g(g(U_74)))) | LE(f(g(g(U_74))), s(0)) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t2:3)], [clause_6_04]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t23, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t22:1)], [t22:1,t2:3]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t24, plain, ( ~LE(f(g(g(U_74))), s(0)) | LE(f(g(g(g(U_74)))), 0) | E(0, f(g(g(g(U_74))))) | ~iLEQ(g(g(U_74)), g(g(g(U_74)))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t22:2)], [clause_10_06]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t25, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t24:1)], [t24:1,t22:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t26, plain, ( ~LE(f(g(g(g(U_74)))), 0) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t24:2)], [clause_2_08]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t27, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t26:1)], [t26:1,t24:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t28, plain, ( ~E(0, f(g(g(g(U_74))))) | ~E(0, f(g(g(U_74)))) | E(f(g(g(U_74))), f(g(g(g(U_74))))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t24:3)], [clause_11_03]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t29, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t28:1)], [t28:1,t24:3]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t30, plain, ( E(0, f(g(g(U_74)))) | ~LE(f(g(g(U_74))), s(0)) | LE(f(g(g(U_74))), 0) | ~iLEQ(g(g(U_74)), g(g(U_74))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t28:2)], [clause_10_06]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t31, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t30:1)], [t30:1,t28:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t32, plain, $false,
% 0.09/0.38 inference(reduction, [status(thm), parent(t30:2)], [t30:2,t22:2]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t33, plain, ( ~LE(f(g(g(U_74))), 0) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t30:3)], [clause_2_08]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t34, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t33:1)], [t33:1,t30:3]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t35, plain, ( iLEQ(g(g(U_74)), g(g(U_74))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t30:4)], [clause_9_12]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t36, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t35:1)], [t35:1,t30:4]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t37, plain, ( ~E(f(g(g(U_74))), f(g(g(g(U_74))))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t28:3)], [clause_4_11]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t38, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t37:1)], [t37:1,t28:3]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t39, plain, ( iLEQ(g(g(U_74)), g(g(g(U_74)))) ),
% 0.09/0.38 inference(extension, [status(thm), parent(t24:4)], [clause_5_10]) ).
% 0.09/0.38
% 0.09/0.38 cnf(t40, plain, $false,
% 0.09/0.38 inference(connection, [status(thm), parent(t39:1)], [t39:1,t24:4]) ).
% 0.09/0.38
% 0.09/0.38 % SZS output end Proof for theBenchmark
%------------------------------------------------------------------------------