%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN617-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 : n005.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:43 AM UTC 2026
% Result : Unsatisfiable 0.23s 0.49s
% Output : Proof 0.23s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(p11_1,negated_conjecture,
p11(X0,X0),
file('theBenchmark.p',p11_1) ).
cnf(p9_2,negated_conjecture,
p9(X53,X53),
file('theBenchmark.p',p9_2) ).
cnf(p7_3,negated_conjecture,
p7(X42,X42),
file('theBenchmark.p',p7_3) ).
cnf(p2_4,negated_conjecture,
p2(X27,X27),
file('theBenchmark.p',p2_4) ).
cnf(p13_5,negated_conjecture,
p13(X11,X11),
file('theBenchmark.p',p13_5) ).
cnf(p19_6,negated_conjecture,
p19(c21,c22),
file('theBenchmark.p',p19_6) ).
cnf(p11_7,negated_conjecture,
p11(f12(f14(X5,X6)),X6),
file('theBenchmark.p',p11_7) ).
cnf(p7_8,negated_conjecture,
p7(f8(f10(X51,X52)),X52),
file('theBenchmark.p',p7_8) ).
cnf(p9_9,negated_conjecture,
p9(f18(f5(c20),X64),f17(X64)),
file('theBenchmark.p',p9_9) ).
cnf(p13_10,negated_conjecture,
p13(f15(f5(c20),X20),f16(X20)),
file('theBenchmark.p',p13_10) ).
cnf(p11_11,negated_conjecture,
( ~ p11(X3,X4)
| p11(f12(X3),f12(X4)) ),
file('theBenchmark.p',p11_11) ).
cnf(p9_12,negated_conjecture,
( ~ p7(X56,X57)
| p9(f17(X56),f17(X57)) ),
file('theBenchmark.p',p9_12) ).
cnf(p7_13,negated_conjecture,
( ~ p7(X49,X50)
| p7(f8(X49),f8(X50)) ),
file('theBenchmark.p',p7_13) ).
cnf(p2_14,negated_conjecture,
( ~ p2(X40,X41)
| p2(f6(X40),f6(X41)) ),
file('theBenchmark.p',p2_14) ).
cnf(p2_15,negated_conjecture,
( ~ p2(X38,X39)
| p2(f5(X38),f5(X39)) ),
file('theBenchmark.p',p2_15) ).
cnf(p2_16,negated_conjecture,
( ~ p2(X30,X31)
| p2(f3(X30),f3(X31)) ),
file('theBenchmark.p',p2_16) ).
cnf(p13_17,negated_conjecture,
( ~ p11(X21,X22)
| p13(f16(X21),f16(X22)) ),
file('theBenchmark.p',p13_17) ).
cnf(p9_18,negated_conjecture,
p9(f18(f3(X62),X63),f18(X62,f8(X63))),
file('theBenchmark.p',p9_18) ).
cnf(p13_19,negated_conjecture,
p13(f15(f3(X18),X19),f15(X18,f12(X19))),
file('theBenchmark.p',p13_19) ).
cnf(p11_20,negated_conjecture,
( ~ p11(X0,X2)
| ~ p11(X0,X1)
| p11(X1,X2) ),
file('theBenchmark.p',p11_20) ).
cnf(p9_21,negated_conjecture,
( ~ p9(X53,X55)
| ~ p9(X53,X54)
| p9(X54,X55) ),
file('theBenchmark.p',p9_21) ).
cnf(p7_22,negated_conjecture,
( ~ p7(X42,X44)
| ~ p7(X42,X43)
| p7(X43,X44) ),
file('theBenchmark.p',p7_22) ).
cnf(p2_23,negated_conjecture,
( ~ p2(X27,X29)
| ~ p2(X27,X28)
| p2(X28,X29) ),
file('theBenchmark.p',p2_23) ).
cnf(p13_24,negated_conjecture,
( ~ p13(X11,X13)
| ~ p13(X11,X12)
| p13(X12,X13) ),
file('theBenchmark.p',p13_24) ).
cnf(p19_25,negated_conjecture,
( ~ p19(X25,X26)
| ~ p2(X26,X24)
| ~ p2(X25,X23)
| p19(X23,X24) ),
file('theBenchmark.p',p19_25) ).
cnf(p9_26,negated_conjecture,
( ~ p7(X59,X61)
| ~ p2(X58,X60)
| p9(f18(X58,X59),f18(X60,X61)) ),
file('theBenchmark.p',p9_26) ).
cnf(p11_27,negated_conjecture,
( ~ p13(X7,X9)
| ~ p11(X8,X10)
| p11(f14(X7,X8),f14(X9,X10)) ),
file('theBenchmark.p',p11_27) ).
cnf(p13_28,negated_conjecture,
( ~ p2(X14,X16)
| ~ p11(X15,X17)
| p13(f15(X14,X15),f15(X16,X17)) ),
file('theBenchmark.p',p13_28) ).
cnf(p2_29,negated_conjecture,
( ~ p2(X33,X35)
| ~ p2(X32,X34)
| p2(f4(X32,X33),f4(X34,X35)) ),
file('theBenchmark.p',p2_29) ).
cnf(p7_30,negated_conjecture,
( ~ p9(X45,X47)
| ~ p7(X46,X48)
| p7(f10(X45,X46),f10(X47,X48)) ),
file('theBenchmark.p',p7_30) ).
cnf(p2_31,negated_conjecture,
( ~ p19(X37,X36)
| p2(f4(f4(f3(X36),f5(f6(c20))),X37),f3(f4(f4(X36,f5(f6(c20))),X37))) ),
file('theBenchmark.p',p2_31) ).
cnf(not_p13_32,negated_conjecture,
~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)),
file('theBenchmark.p',not_p13_32) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN617-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_HRN 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.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 07:05:48 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.23/0.49 % SZS status Unsatisfiable for theBenchmark
% 0.23/0.49 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------