%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN573-1 : TPTP v9.3.1. Released v2.5.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 : n002.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:10:37 AM UTC 2026
% Result : Unsatisfiable 0.02s 0.44s
% Output : Proof 0.02s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c15_is_p12_1,negated_conjecture,
p12(c15),
file('theBenchmark.p',c15_is_p12_1) ).
cnf(p4_2,negated_conjecture,
p4(X30,X30),
file('theBenchmark.p',p4_2) ).
cnf(p2_3,negated_conjecture,
p2(X17,X17),
file('theBenchmark.p',p2_3) ).
cnf(p2_4,negated_conjecture,
( ~ p12(X16)
| p2(X16,f9(f10(X16))) ),
file('theBenchmark.p',p2_4) ).
cnf(p12_5,negated_conjecture,
( ~ p2(X11,X10)
| ~ p12(X11)
| p12(X10) ),
file('theBenchmark.p',p12_5) ).
cnf(p4_6,negated_conjecture,
( ~ p4(X37,X38)
| p4(f7(X37),f7(X38)) ),
file('theBenchmark.p',p4_6) ).
cnf(p2_7,negated_conjecture,
( ~ p4(X24,X25)
| p2(f5(X24),f5(X25)) ),
file('theBenchmark.p',p2_7) ).
cnf(p2_8,negated_conjecture,
( ~ p2(X26,X27)
| p2(f8(X26),f8(X27)) ),
file('theBenchmark.p',p2_8) ).
cnf(p2_9,negated_conjecture,
( ~ p4(X28,X29)
| p2(f9(X28),f9(X29)) ),
file('theBenchmark.p',p2_9) ).
cnf(p4_10,negated_conjecture,
( ~ p2(X33,X34)
| p4(f10(X33),f10(X34)) ),
file('theBenchmark.p',p4_10) ).
cnf(p4_11,negated_conjecture,
( ~ p4(X35,X36)
| p4(f6(X35),f6(X36)) ),
file('theBenchmark.p',p4_11) ).
cnf(p4_12,negated_conjecture,
( ~ p4(X30,X32)
| ~ p4(X30,X31)
| p4(X31,X32) ),
file('theBenchmark.p',p4_12) ).
cnf(p2_13,negated_conjecture,
( ~ p2(X17,X19)
| ~ p2(X17,X18)
| p2(X18,X19) ),
file('theBenchmark.p',p2_13) ).
cnf(p11_14,negated_conjecture,
( ~ p12(X9)
| p2(X9,f9(c17))
| p11(X9,c16) ),
file('theBenchmark.p',p11_14) ).
cnf(p13_15,negated_conjecture,
( ~ p12(X16)
| p4(f10(X16),c17)
| p13(f10(X16),c17) ),
file('theBenchmark.p',p13_15) ).
cnf(p11_16,negated_conjecture,
p11(X7,f3(f8(X8),f3(f8(X7),f5(f6(f7(c14)))))),
file('theBenchmark.p',p11_16) ).
cnf(p11_17,negated_conjecture,
( ~ p11(X2,X3)
| ~ p2(X3,X1)
| ~ p2(X2,X0)
| p11(X0,X1) ),
file('theBenchmark.p',p11_17) ).
cnf(p13_18,negated_conjecture,
( ~ p13(X14,X15)
| ~ p4(X15,X13)
| ~ p4(X14,X12)
| p13(X12,X13) ),
file('theBenchmark.p',p13_18) ).
cnf(not_p11_19,negated_conjecture,
~ p11(c15,f3(f8(c16),f3(f8(f9(c17)),f5(f6(f7(c14)))))),
file('theBenchmark.p',not_p11_19) ).
cnf(p2_20,negated_conjecture,
( ~ p2(X21,X23)
| ~ p2(X20,X22)
| p2(f3(X20,X21),f3(X22,X23)) ),
file('theBenchmark.p',p2_20) ).
cnf(p11_21,negated_conjecture,
( ~ p11(X4,X5)
| p11(X4,f3(f8(X5),f3(f8(X6),f5(f6(f7(c14)))))) ),
file('theBenchmark.p',p11_21) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN573-1 : TPTP v9.3.1. Released v2.5.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.08/0.36 % Computer : n002.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 07:07:46 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.44 % SZS status Unsatisfiable for theBenchmark
% 0.02/0.44 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------