%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN626-1 : TPTP v9.3.1. Released v2.5.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:10:44 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.39s
% Output : Proof 0.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(p11_1,negated_conjecture,
p11(X0,X0),
file('theBenchmark.p',p11_1) ).
cnf(p7_2,negated_conjecture,
p7(X54,X54),
file('theBenchmark.p',p7_2) ).
cnf(p6_3,negated_conjecture,
p6(X47,X47),
file('theBenchmark.p',p6_3) ).
cnf(p3_4,negated_conjecture,
p3(X38,X38),
file('theBenchmark.p',p3_4) ).
cnf(p2_5,negated_conjecture,
p2(X33,X33),
file('theBenchmark.p',p2_5) ).
cnf(p11_6,negated_conjecture,
p11(f13(f12(X5)),X5),
file('theBenchmark.p',p11_6) ).
cnf(p14_7,negated_conjecture,
p14(f4(f5(c20)),f4(c21)),
file('theBenchmark.p',p14_7) ).
cnf(p16_8,negated_conjecture,
( ~ p15(X14,X15)
| p16(X14,X15) ),
file('theBenchmark.p',p16_8) ).
cnf(p15_9,negated_conjecture,
p15(c22,f8(f5(c20),f9(c23,c24))),
file('theBenchmark.p',p15_9) ).
cnf(p16_10,negated_conjecture,
( ~ p7(f12(f13(X20)),X20)
| p16(c22,X20) ),
file('theBenchmark.p',p16_10) ).
cnf(p11_11,negated_conjecture,
( ~ p7(X3,X4)
| p11(f13(X3),f13(X4)) ),
file('theBenchmark.p',p11_11) ).
cnf(p7_12,negated_conjecture,
( ~ p11(X57,X58)
| p7(f12(X57),f12(X58)) ),
file('theBenchmark.p',p7_12) ).
cnf(p3_13,negated_conjecture,
( ~ p2(X45,X46)
| p3(f4(X45),f4(X46)) ),
file('theBenchmark.p',p3_13) ).
cnf(p2_14,negated_conjecture,
( ~ p2(X36,X37)
| p2(f5(X36),f5(X37)) ),
file('theBenchmark.p',p2_14) ).
cnf(p7_15,negated_conjecture,
( ~ p16(c22,X20)
| p7(f12(f13(X20)),X20) ),
file('theBenchmark.p',p7_15) ).
cnf(p11_16,negated_conjecture,
( ~ p11(X0,X2)
| ~ p11(X0,X1)
| p11(X1,X2) ),
file('theBenchmark.p',p11_16) ).
cnf(p7_17,negated_conjecture,
( ~ p7(X54,X56)
| ~ p7(X54,X55)
| p7(X55,X56) ),
file('theBenchmark.p',p7_17) ).
cnf(p6_18,negated_conjecture,
( ~ p6(X47,X49)
| ~ p6(X47,X48)
| p6(X48,X49) ),
file('theBenchmark.p',p6_18) ).
cnf(p3_19,negated_conjecture,
( ~ p3(X38,X40)
| ~ p3(X38,X39)
| p3(X39,X40) ),
file('theBenchmark.p',p3_19) ).
cnf(p2_20,negated_conjecture,
( ~ p2(X33,X35)
| ~ p2(X33,X34)
| p2(X34,X35) ),
file('theBenchmark.p',p2_20) ).
cnf(p15_21,negated_conjecture,
( ~ p19(X14,X15)
| ~ p16(X14,X15)
| p15(X14,X15) ),
file('theBenchmark.p',p15_21) ).
cnf(p15_22,negated_conjecture,
( ~ p18(X14,X15)
| ~ p16(X14,X15)
| p15(X14,X15) ),
file('theBenchmark.p',p15_22) ).
cnf(p15_23,negated_conjecture,
( ~ p17(X14,X15)
| ~ p16(X14,X15)
| p15(X14,X15) ),
file('theBenchmark.p',p15_23) ).
cnf(not_p15_24,negated_conjecture,
~ p15(c22,f12(f13(f8(f5(c20),f9(c23,c24))))),
file('theBenchmark.p',not_p15_24) ).
cnf(p17_25,negated_conjecture,
( ~ p15(X14,X15)
| p19(X14,X15)
| p18(X14,X15)
| p17(X14,X15) ),
file('theBenchmark.p',p17_25) ).
cnf(p14_26,negated_conjecture,
( ~ p14(X8,X9)
| ~ p3(X9,X7)
| ~ p3(X8,X6)
| p14(X6,X7) ),
file('theBenchmark.p',p14_26) ).
cnf(p19_27,negated_conjecture,
( ~ p19(X31,X32)
| ~ p7(X32,X30)
| ~ p6(X31,X29)
| p19(X29,X30) ),
file('theBenchmark.p',p19_27) ).
cnf(p18_28,negated_conjecture,
( ~ p18(X27,X28)
| ~ p7(X28,X26)
| ~ p6(X27,X25)
| p18(X25,X26) ),
file('theBenchmark.p',p18_28) ).
cnf(p17_29,negated_conjecture,
( ~ p17(X23,X24)
| ~ p7(X24,X22)
| ~ p6(X23,X21)
| p17(X21,X22) ),
file('theBenchmark.p',p17_29) ).
cnf(p16_30,negated_conjecture,
( ~ p16(X18,X19)
| ~ p7(X19,X17)
| ~ p6(X18,X16)
| p16(X16,X17) ),
file('theBenchmark.p',p16_30) ).
cnf(p15_31,negated_conjecture,
( ~ p15(X12,X13)
| ~ p7(X13,X11)
| ~ p6(X12,X10)
| p15(X10,X11) ),
file('theBenchmark.p',p15_31) ).
cnf(p3_32,negated_conjecture,
p3(f10(c22,f12(f13(f8(f5(c20),f9(c23,c24))))),f4(c21)),
file('theBenchmark.p',p3_32) ).
cnf(p7_33,negated_conjecture,
( ~ p6(X60,X62)
| ~ p2(X59,X61)
| p7(f8(X59,X60),f8(X61,X62)) ),
file('theBenchmark.p',p7_33) ).
cnf(p3_34,negated_conjecture,
( ~ p7(X42,X44)
| ~ p6(X41,X43)
| p3(f10(X41,X42),f10(X43,X44)) ),
file('theBenchmark.p',p3_34) ).
cnf(p6_35,negated_conjecture,
( ~ p2(X50,X52)
| ~ p2(X51,X53)
| p6(f9(X50,X51),f9(X52,X53)) ),
file('theBenchmark.p',p6_35) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN626-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/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n011.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 07:06:09 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.12/0.39 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------