%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN657-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 : n026.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:48 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.42s
% Output : Proof 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(p17_1,negated_conjecture,
p17(X0,X0),
file('theBenchmark.p',p17_1) ).
cnf(p7_2,negated_conjecture,
p7(X85,X85),
file('theBenchmark.p',p7_2) ).
cnf(p6_3,negated_conjecture,
p6(X71,X71),
file('theBenchmark.p',p6_3) ).
cnf(p4_4,negated_conjecture,
p4(X36,X36),
file('theBenchmark.p',p4_4) ).
cnf(p3_5,negated_conjecture,
p3(X33,X33),
file('theBenchmark.p',p3_5) ).
cnf(p2_6,negated_conjecture,
p2(X5,X5),
file('theBenchmark.p',p2_6) ).
cnf(p24_7,negated_conjecture,
p24(c32,c31),
file('theBenchmark.p',p24_7) ).
cnf(p26_8,negated_conjecture,
p26(c32,c31),
file('theBenchmark.p',p26_8) ).
cnf(p26_9,negated_conjecture,
p26(c31,c35),
file('theBenchmark.p',p26_9) ).
cnf(p24_10,negated_conjecture,
p24(c32,c34),
file('theBenchmark.p',p24_10) ).
cnf(not_p6_11,negated_conjecture,
~ p6(c28,f10(c33)),
file('theBenchmark.p',not_p6_11) ).
cnf(p23_12,negated_conjecture,
p23(f10(f11(f12(c33))),c28),
file('theBenchmark.p',p23_12) ).
cnf(p25_13,negated_conjecture,
p25(c35,f18(f8(c27,f9(c28,c29)))),
file('theBenchmark.p',p25_13) ).
cnf(p25_14,negated_conjecture,
p25(c32,f18(f8(c27,f9(c28,c29)))),
file('theBenchmark.p',p25_14) ).
cnf(p6_15,negated_conjecture,
p6(f21(f8(X82,f9(X83,X84))),X83),
file('theBenchmark.p',p6_15) ).
cnf(p17_16,negated_conjecture,
( ~ p2(X3,X4)
| p17(f18(X3),f18(X4)) ),
file('theBenchmark.p',p17_16) ).
cnf(p6_17,negated_conjecture,
( ~ p2(X80,X81)
| p6(f21(X80),f21(X81)) ),
file('theBenchmark.p',p6_17) ).
cnf(p6_18,negated_conjecture,
( ~ p6(X78,X79)
| p6(f12(X78),f12(X79)) ),
file('theBenchmark.p',p6_18) ).
cnf(p6_19,negated_conjecture,
( ~ p6(X76,X77)
| p6(f11(X76),f11(X77)) ),
file('theBenchmark.p',p6_19) ).
cnf(p6_20,negated_conjecture,
( ~ p6(X74,X75)
| p6(f10(X74),f10(X75)) ),
file('theBenchmark.p',p6_20) ).
cnf(p4_21,negated_conjecture,
( ~ p4(X53,X54)
| p4(f19(X53),f19(X54)) ),
file('theBenchmark.p',p4_21) ).
cnf(p4_22,negated_conjecture,
( ~ p6(X47,X48)
| p4(f15(X47),f15(X48)) ),
file('theBenchmark.p',p4_22) ).
cnf(p17_23,negated_conjecture,
( ~ p17(X0,X2)
| ~ p17(X0,X1)
| p17(X1,X2) ),
file('theBenchmark.p',p17_23) ).
cnf(p7_24,negated_conjecture,
( ~ p7(X85,X87)
| ~ p7(X85,X86)
| p7(X86,X87) ),
file('theBenchmark.p',p7_24) ).
cnf(p6_25,negated_conjecture,
( ~ p6(X71,X73)
| ~ p6(X71,X72)
| p6(X72,X73) ),
file('theBenchmark.p',p6_25) ).
cnf(p4_26,negated_conjecture,
( ~ p4(X36,X38)
| ~ p4(X36,X37)
| p4(X37,X38) ),
file('theBenchmark.p',p4_26) ).
cnf(p3_27,negated_conjecture,
( ~ p3(X33,X35)
| ~ p3(X33,X34)
| p3(X34,X35) ),
file('theBenchmark.p',p3_27) ).
cnf(p2_28,negated_conjecture,
( ~ p2(X5,X7)
| ~ p2(X5,X6)
| p2(X6,X7) ),
file('theBenchmark.p',p2_28) ).
cnf(p4_29,negated_conjecture,
p4(f5(f8(c27,f9(c28,c29)),c30,c31),c32),
file('theBenchmark.p',p4_29) ).
cnf(p4_30,negated_conjecture,
p4(c35,f13(c32,f16(f8(c27,f9(c28,c29)),c31))),
file('theBenchmark.p',p4_30) ).
cnf(p23_31,negated_conjecture,
( ~ p23(X14,X15)
| ~ p6(X15,X13)
| ~ p6(X14,X12)
| p23(X12,X13) ),
file('theBenchmark.p',p23_31) ).
cnf(p26_32,negated_conjecture,
( ~ p26(X30,X31)
| ~ p4(X31,X29)
| ~ p4(X30,X28)
| p26(X28,X29) ),
file('theBenchmark.p',p26_32) ).
cnf(p25_33,negated_conjecture,
( ~ p17(X23,X22)
| ~ p4(X24,X21)
| ~ p25(X24,X23)
| p25(X21,X22) ),
file('theBenchmark.p',p25_33) ).
cnf(p24_34,negated_conjecture,
( ~ p24(X18,X19)
| ~ p4(X19,X17)
| ~ p4(X18,X16)
| p24(X16,X17) ),
file('theBenchmark.p',p24_34) ).
cnf(p2_35,negated_conjecture,
( ~ p7(X9,X11)
| ~ p6(X8,X10)
| p2(f8(X8,X9),f8(X10,X11)) ),
file('theBenchmark.p',p2_35) ).
cnf(p7_36,negated_conjecture,
( ~ p6(X89,X91)
| ~ p6(X88,X90)
| p7(f9(X88,X89),f9(X90,X91)) ),
file('theBenchmark.p',p7_36) ).
cnf(p4_37,negated_conjecture,
( ~ p4(X56,X58)
| ~ p4(X55,X57)
| p4(f20(X55,X56),f20(X57,X58)) ),
file('theBenchmark.p',p4_37) ).
cnf(p4_38,negated_conjecture,
( ~ p4(X50,X52)
| ~ p2(X49,X51)
| p4(f16(X49,X50),f16(X51,X52)) ),
file('theBenchmark.p',p4_38) ).
cnf(p4_39,negated_conjecture,
( ~ p4(X44,X46)
| ~ p4(X43,X45)
| p4(f14(X43,X44),f14(X45,X46)) ),
file('theBenchmark.p',p4_39) ).
cnf(p4_40,negated_conjecture,
( ~ p4(X40,X42)
| ~ p4(X39,X41)
| p4(f13(X39,X40),f13(X41,X42)) ),
file('theBenchmark.p',p4_40) ).
cnf(not_p24_41,negated_conjecture,
( ~ p25(X92,f18(f8(c27,f9(c28,c29))))
| ~ p24(c32,X92)
| ~ p24(X92,c35) ),
file('theBenchmark.p',not_p24_41) ).
cnf(p4_42,negated_conjecture,
p4(f16(f8(c27,f9(c28,c29)),c34),f16(f8(c27,f9(c28,c29)),c31)),
file('theBenchmark.p',p4_42) ).
cnf(p24_43,negated_conjecture,
p24(c34,f13(c32,f14(f16(f8(c27,f9(c28,c29)),c31),f15(f10(f11(f12(c33))))))),
file('theBenchmark.p',p24_43) ).
cnf(not_p4_44,negated_conjecture,
~ p4(f5(f8(c27,f9(c28,c29)),c36,c31),f5(f8(c27,f9(c28,c29)),c36,c34)),
file('theBenchmark.p',not_p4_44) ).
cnf(p24_45,negated_conjecture,
( ~ p25(X20,f18(f8(c27,f9(c28,c29))))
| p24(f19(f20(c31,c34)),f19(f20(c31,X20))) ),
file('theBenchmark.p',p24_45) ).
cnf(p4_46,negated_conjecture,
( ~ p2(X65,X68)
| ~ p4(X67,X70)
| ~ p3(X66,X69)
| p4(f5(X65,X66,X67),f5(X68,X69,X70)) ),
file('theBenchmark.p',p4_46) ).
cnf(p4_47,negated_conjecture,
( ~ p2(X59,X62)
| ~ p4(X61,X64)
| ~ p4(X60,X63)
| p4(f22(X59,X60,X61),f22(X62,X63,X64)) ),
file('theBenchmark.p',p4_47) ).
cnf(p6_48,negated_conjecture,
( p4(f5(X25,c36,X26),f5(X25,c36,X27))
| p25(f22(X25,X26,X27),f18(X25))
| p6(f21(X25),f10(c33)) ),
file('theBenchmark.p',p6_48) ).
cnf(p6_49,negated_conjecture,
( ~ p24(f19(f20(X26,X27)),f19(f20(X26,f22(X25,X26,X27))))
| p4(f5(X25,c36,X26),f5(X25,c36,X27))
| p6(f21(X25),f10(c33)) ),
file('theBenchmark.p',p6_49) ).
cnf(p26_50,negated_conjecture,
( ~ p25(X32,f18(f8(c27,f9(c28,c29))))
| p26(f19(f20(c31,c35)),f19(f20(c31,X32)))
| p26(f19(f20(c31,c32)),f19(f20(c31,X32))) ),
file('theBenchmark.p',p26_50) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN657-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.10/0.35 % Computer : n026.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 07:09:22 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.42 % SZS status Unsatisfiable for theBenchmark
% 0.13/0.42 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------