%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN633-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 : n006.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:45 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.38s
% Output : Proof 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(p10_1,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_1) ).
cnf(p9_2,negated_conjecture,
p9(X92,X92),
file('theBenchmark.p',p9_2) ).
cnf(p5_3,negated_conjecture,
p5(X85,X85),
file('theBenchmark.p',p5_3) ).
cnf(p3_4,negated_conjecture,
p3(X75,X75),
file('theBenchmark.p',p3_4) ).
cnf(p2_5,negated_conjecture,
p2(X58,X58),
file('theBenchmark.p',p2_5) ).
cnf(p14_6,negated_conjecture,
p14(X51,X51),
file('theBenchmark.p',p14_6) ).
cnf(not_p3_7,negated_conjecture,
~ p3(c23,f8(c24)),
file('theBenchmark.p',not_p3_7) ).
cnf(p3_8,negated_conjecture,
p3(f4(f6(X80,f7(X81,X82))),X81),
file('theBenchmark.p',p3_8) ).
cnf(p3_9,negated_conjecture,
( ~ p3(X83,X84)
| p3(f8(X83),f8(X84)) ),
file('theBenchmark.p',p3_9) ).
cnf(p10_10,negated_conjecture,
( ~ p10(X21,X22)
| p10(f12(X21),f12(X22)) ),
file('theBenchmark.p',p10_10) ).
cnf(p14_11,negated_conjecture,
( ~ p2(X54,X55)
| p14(f15(X54),f15(X55)) ),
file('theBenchmark.p',p14_11) ).
cnf(p14_12,negated_conjecture,
( ~ p2(X56,X57)
| p14(f16(X56),f16(X57)) ),
file('theBenchmark.p',p14_12) ).
cnf(p3_13,negated_conjecture,
( ~ p2(X78,X79)
| p3(f4(X78),f4(X79)) ),
file('theBenchmark.p',p3_13) ).
cnf(p10_14,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_14) ).
cnf(p9_15,negated_conjecture,
( ~ p9(X92,X94)
| ~ p9(X92,X93)
| p9(X93,X94) ),
file('theBenchmark.p',p9_15) ).
cnf(p5_16,negated_conjecture,
( ~ p5(X85,X87)
| ~ p5(X85,X86)
| p5(X86,X87) ),
file('theBenchmark.p',p5_16) ).
cnf(p3_17,negated_conjecture,
( ~ p3(X75,X77)
| ~ p3(X75,X76)
| p3(X76,X77) ),
file('theBenchmark.p',p3_17) ).
cnf(p2_18,negated_conjecture,
( ~ p2(X58,X60)
| ~ p2(X58,X59)
| p2(X59,X60) ),
file('theBenchmark.p',p2_18) ).
cnf(p14_19,negated_conjecture,
( ~ p14(X51,X53)
| ~ p14(X51,X52)
| p14(X52,X53) ),
file('theBenchmark.p',p14_19) ).
cnf(p22_20,negated_conjecture,
( ~ p10(X73,X71)
| ~ p22(X73,X74)
| ~ p14(X74,X72)
| p22(X71,X72) ),
file('theBenchmark.p',p22_20) ).
cnf(p21_21,negated_conjecture,
( ~ p10(X67,X65)
| ~ p21(X67,X68)
| ~ p10(X68,X66)
| p21(X65,X66) ),
file('theBenchmark.p',p21_21) ).
cnf(p10_22,negated_conjecture,
( ~ p10(X24,X26)
| ~ p10(X23,X25)
| p10(f13(X23,X24),f13(X25,X26)) ),
file('theBenchmark.p',p10_22) ).
cnf(p5_23,negated_conjecture,
( ~ p3(X89,X91)
| ~ p3(X88,X90)
| p5(f7(X88,X89),f7(X90,X91)) ),
file('theBenchmark.p',p5_23) ).
cnf(p2_24,negated_conjecture,
( ~ p5(X62,X64)
| ~ p3(X61,X63)
| p2(f6(X61,X62),f6(X63,X64)) ),
file('theBenchmark.p',p2_24) ).
cnf(not_p10_25,negated_conjecture,
~ p10(f11(f6(c25,f7(c23,c26)),c27,c28),f11(f6(c25,f7(c23,c26)),c27,c29)),
file('theBenchmark.p',not_p10_25) ).
cnf(p21_26,negated_conjecture,
( ~ p22(X70,f16(f6(c25,f7(c23,c26))))
| p21(f12(f13(c28,c29)),f12(f13(c28,X70))) ),
file('theBenchmark.p',p21_26) ).
cnf(p21_27,negated_conjecture,
( ~ p22(X69,f15(f6(c25,f7(c23,c26))))
| p21(f12(f13(c28,c29)),f12(f13(c28,X69))) ),
file('theBenchmark.p',p21_27) ).
cnf(p10_28,negated_conjecture,
( ~ p10(X5,X8)
| ~ p9(X4,X7)
| ~ p2(X3,X6)
| p10(f11(X3,X4,X5),f11(X6,X7,X8)) ),
file('theBenchmark.p',p10_28) ).
cnf(p10_29,negated_conjecture,
( ~ p10(X46,X49)
| ~ p2(X45,X48)
| ~ p10(X47,X50)
| p10(f20(X45,X46,X47),f20(X48,X49,X50)) ),
file('theBenchmark.p',p10_29) ).
cnf(p10_30,negated_conjecture,
( ~ p10(X40,X43)
| ~ p2(X39,X42)
| ~ p10(X41,X44)
| p10(f19(X39,X40,X41),f19(X42,X43,X44)) ),
file('theBenchmark.p',p10_30) ).
cnf(p10_31,negated_conjecture,
( ~ p10(X34,X37)
| ~ p2(X33,X36)
| ~ p10(X35,X38)
| p10(f18(X33,X34,X35),f18(X36,X37,X38)) ),
file('theBenchmark.p',p10_31) ).
cnf(p10_32,negated_conjecture,
( ~ p10(X28,X31)
| ~ p2(X27,X30)
| ~ p10(X29,X32)
| p10(f17(X27,X28,X29),f17(X30,X31,X32)) ),
file('theBenchmark.p',p10_32) ).
cnf(p3_33,negated_conjecture,
( p10(f11(X9,c27,X10),f11(X9,c27,X11))
| p22(f17(X9,X10,X11),f16(X9))
| p3(f4(X9),f8(c24)) ),
file('theBenchmark.p',p3_33) ).
cnf(p3_34,negated_conjecture,
( p10(f11(X18,c32,X19),f11(X18,c32,X20))
| p22(f20(X18,X19,X20),f15(X18))
| p3(f4(X18),f8(c24)) ),
file('theBenchmark.p',p3_34) ).
cnf(p3_35,negated_conjecture,
( p10(f11(X15,c31,X16),f11(X15,c31,X17))
| p22(f19(X15,X16,X17),f16(X15))
| p3(f4(X15),f8(c24)) ),
file('theBenchmark.p',p3_35) ).
cnf(p3_36,negated_conjecture,
( p10(f11(X12,c30,X13),f11(X12,c30,X14))
| p22(f18(X12,X13,X14),f16(X12))
| p3(f4(X12),f8(c24)) ),
file('theBenchmark.p',p3_36) ).
cnf(p3_37,negated_conjecture,
( ~ p21(f12(f13(X19,X20)),f12(f13(X19,f20(X18,X19,X20))))
| p10(f11(X18,c32,X19),f11(X18,c32,X20))
| p3(f4(X18),f8(c24)) ),
file('theBenchmark.p',p3_37) ).
cnf(p3_38,negated_conjecture,
( ~ p21(f12(f13(X10,X11)),f12(f13(X10,f17(X9,X10,X11))))
| p10(f11(X9,c27,X10),f11(X9,c27,X11))
| p3(f4(X9),f8(c24)) ),
file('theBenchmark.p',p3_38) ).
cnf(p3_39,negated_conjecture,
( ~ p21(f12(f13(X13,X14)),f12(f13(X13,f18(X12,X13,X14))))
| p10(f11(X12,c30,X13),f11(X12,c30,X14))
| p3(f4(X12),f8(c24)) ),
file('theBenchmark.p',p3_39) ).
cnf(p3_40,negated_conjecture,
( ~ p21(f12(f13(X16,X17)),f12(f13(X16,f19(X15,X16,X17))))
| p10(f11(X15,c31,X16),f11(X15,c31,X17))
| p3(f4(X15),f8(c24)) ),
file('theBenchmark.p',p3_40) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN633-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.03 % 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.34 % Computer : n006.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sun Sep 20 07:05:57 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.13/0.38 % SZS status Unsatisfiable for theBenchmark
% 0.13/0.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------