%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN673-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 : n001.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:50 AM UTC 2026
% Result : Unsatisfiable 0.46s 0.79s
% Output : Proof 0.56s
% 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(X102,X102),
file('theBenchmark.p',p9_2) ).
cnf(p7_3,negated_conjecture,
p7(X99,X99),
file('theBenchmark.p',p7_3) ).
cnf(p6_4,negated_conjecture,
p6(X96,X96),
file('theBenchmark.p',p6_4) ).
cnf(p4_5,negated_conjecture,
p4(X81,X81),
file('theBenchmark.p',p4_5) ).
cnf(p3_6,negated_conjecture,
p3(X74,X74),
file('theBenchmark.p',p3_6) ).
cnf(p25_7,negated_conjecture,
p25(X52,X52),
file('theBenchmark.p',p25_7) ).
cnf(p23_8,negated_conjecture,
p23(X49,X49),
file('theBenchmark.p',p23_8) ).
cnf(p20_9,negated_conjecture,
p20(X42,X42),
file('theBenchmark.p',p20_9) ).
cnf(p2_10,negated_conjecture,
p2(X39,X39),
file('theBenchmark.p',p2_10) ).
cnf(p18_11,negated_conjecture,
p18(X36,X36),
file('theBenchmark.p',p18_11) ).
cnf(p16_12,negated_conjecture,
p16(X29,X29),
file('theBenchmark.p',p16_12) ).
cnf(p15_13,negated_conjecture,
p15(X26,X26),
file('theBenchmark.p',p15_13) ).
cnf(p13_14,negated_conjecture,
p13(X19,X19),
file('theBenchmark.p',p13_14) ).
cnf(p11_15,negated_conjecture,
p11(X12,X12),
file('theBenchmark.p',p11_15) ).
cnf(p10_16,negated_conjecture,
p10(f14(f19(c35,X7),c41),X7),
file('theBenchmark.p',p10_16) ).
cnf(not_p29_17,negated_conjecture,
~ p29(f5(c33,f8(c34,c30)),c38),
file('theBenchmark.p',not_p29_17) ).
cnf(p29_18,negated_conjecture,
( ~ p27(f12(c32,X59),X60)
| p29(X60,X59) ),
file('theBenchmark.p',p29_18) ).
cnf(p27_19,negated_conjecture,
( ~ p29(X60,X59)
| p27(f12(c32,X59),X60) ),
file('theBenchmark.p',p27_19) ).
cnf(p28_20,negated_conjecture,
( ~ p16(X68,c40)
| p28(f21(c30,X68),c31) ),
file('theBenchmark.p',p28_20) ).
cnf(p27_21,negated_conjecture,
p27(f12(c32,c37),f5(c33,f8(c34,c30))),
file('theBenchmark.p',p27_21) ).
cnf(p10_22,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_22) ).
cnf(p9_23,negated_conjecture,
( ~ p9(X102,X104)
| ~ p9(X102,X103)
| p9(X103,X104) ),
file('theBenchmark.p',p9_23) ).
cnf(p7_24,negated_conjecture,
( ~ p7(X99,X101)
| ~ p7(X99,X100)
| p7(X100,X101) ),
file('theBenchmark.p',p7_24) ).
cnf(p6_25,negated_conjecture,
( ~ p6(X96,X98)
| ~ p6(X96,X97)
| p6(X97,X98) ),
file('theBenchmark.p',p6_25) ).
cnf(p4_26,negated_conjecture,
( ~ p4(X81,X83)
| ~ p4(X81,X82)
| p4(X82,X83) ),
file('theBenchmark.p',p4_26) ).
cnf(p3_27,negated_conjecture,
( ~ p3(X74,X76)
| ~ p3(X74,X75)
| p3(X75,X76) ),
file('theBenchmark.p',p3_27) ).
cnf(p25_28,negated_conjecture,
( ~ p25(X52,X54)
| ~ p25(X52,X53)
| p25(X53,X54) ),
file('theBenchmark.p',p25_28) ).
cnf(p23_29,negated_conjecture,
( ~ p23(X49,X51)
| ~ p23(X49,X50)
| p23(X50,X51) ),
file('theBenchmark.p',p23_29) ).
cnf(p20_30,negated_conjecture,
( ~ p20(X42,X44)
| ~ p20(X42,X43)
| p20(X43,X44) ),
file('theBenchmark.p',p20_30) ).
cnf(p2_31,negated_conjecture,
( ~ p2(X39,X41)
| ~ p2(X39,X40)
| p2(X40,X41) ),
file('theBenchmark.p',p2_31) ).
cnf(p18_32,negated_conjecture,
( ~ p18(X36,X38)
| ~ p18(X36,X37)
| p18(X37,X38) ),
file('theBenchmark.p',p18_32) ).
cnf(p16_33,negated_conjecture,
( ~ p16(X29,X31)
| ~ p16(X29,X30)
| p16(X30,X31) ),
file('theBenchmark.p',p16_33) ).
cnf(p15_34,negated_conjecture,
( ~ p15(X26,X28)
| ~ p15(X26,X27)
| p15(X27,X28) ),
file('theBenchmark.p',p15_34) ).
cnf(p13_35,negated_conjecture,
( ~ p13(X19,X21)
| ~ p13(X19,X20)
| p13(X20,X21) ),
file('theBenchmark.p',p13_35) ).
cnf(p11_36,negated_conjecture,
( ~ p11(X12,X14)
| ~ p11(X12,X13)
| p11(X13,X14) ),
file('theBenchmark.p',p11_36) ).
cnf(p28_37,negated_conjecture,
( ~ p29(f24(c42,X68),c39)
| p28(f21(c30,X68),c31) ),
file('theBenchmark.p',p28_37) ).
cnf(p29_38,negated_conjecture,
( ~ p10(X71,X70)
| ~ p4(X72,X69)
| ~ p29(X72,X71)
| p29(X69,X70) ),
file('theBenchmark.p',p29_38) ).
cnf(p27_39,negated_conjecture,
( ~ p11(X57,X55)
| ~ p4(X58,X56)
| ~ p27(X57,X58)
| p27(X55,X56) ),
file('theBenchmark.p',p27_39) ).
cnf(p28_40,negated_conjecture,
( ~ p16(X66,X65)
| ~ p28(X67,X66)
| ~ p20(X67,X64)
| p28(X64,X65) ),
file('theBenchmark.p',p28_40) ).
cnf(p10_41,negated_conjecture,
p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),
file('theBenchmark.p',p10_41) ).
cnf(p4_42,negated_conjecture,
( ~ p3(X93,X95)
| ~ p2(X92,X94)
| p4(f5(X92,X93),f5(X94,X95)) ),
file('theBenchmark.p',p4_42) ).
cnf(p10_43,negated_conjecture,
( ~ p13(X3,X5)
| ~ p10(X4,X6)
| p10(f14(X3,X4),f14(X5,X6)) ),
file('theBenchmark.p',p10_43) ).
cnf(p10_44,negated_conjecture,
( ~ p16(X9,X11)
| ~ p15(X8,X10)
| p10(f17(X8,X9),f17(X10,X11)) ),
file('theBenchmark.p',p10_44) ).
cnf(p11_45,negated_conjecture,
( ~ p9(X15,X17)
| ~ p10(X16,X18)
| p11(f12(X15,X16),f12(X17,X18)) ),
file('theBenchmark.p',p11_45) ).
cnf(p13_46,negated_conjecture,
( ~ p18(X22,X24)
| ~ p10(X23,X25)
| p13(f19(X22,X23),f19(X24,X25)) ),
file('theBenchmark.p',p13_46) ).
cnf(p16_47,negated_conjecture,
( ~ p25(X32,X34)
| ~ p10(X33,X35)
| p16(f26(X32,X33),f26(X34,X35)) ),
file('theBenchmark.p',p16_47) ).
cnf(p20_48,negated_conjecture,
( ~ p7(X45,X47)
| ~ p16(X46,X48)
| p20(f21(X45,X46),f21(X47,X48)) ),
file('theBenchmark.p',p20_48) ).
cnf(p3_49,negated_conjecture,
( ~ p7(X78,X80)
| ~ p6(X77,X79)
| p3(f8(X77,X78),f8(X79,X80)) ),
file('theBenchmark.p',p3_49) ).
cnf(p4_50,negated_conjecture,
( ~ p3(X84,X86)
| ~ p10(X85,X87)
| p4(f22(X84,X85),f22(X86,X87)) ),
file('theBenchmark.p',p4_50) ).
cnf(p4_51,negated_conjecture,
( ~ p23(X88,X90)
| ~ p16(X89,X91)
| p4(f24(X88,X89),f24(X90,X91)) ),
file('theBenchmark.p',p4_51) ).
cnf(p29_52,negated_conjecture,
( ~ p10(X73,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),X73)
| p29(f24(c42,f26(c43,X73)),c39) ),
file('theBenchmark.p',p29_52) ).
cnf(p29_53,negated_conjecture,
( ~ p28(f21(c30,f26(c43,X73)),c31)
| ~ p10(X73,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),X73) ),
file('theBenchmark.p',p29_53) ).
cnf(p27_54,negated_conjecture,
( ~ p29(f22(f8(c34,c30),X63),c37)
| p27(f12(c32,f14(f19(c35,X63),f17(c36,c31))),f5(c33,f8(c34,c30))) ),
file('theBenchmark.p',p27_54) ).
cnf(p27_55,negated_conjecture,
( ~ p27(f12(c32,X61),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,X62),c31)
| p27(f12(c32,f14(f19(c35,X61),f17(c36,X62))),f5(c33,f8(c34,c30))) ),
file('theBenchmark.p',p27_55) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN673-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.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 07:12:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.46/0.79 % SZS status Unsatisfiable for theBenchmark
% 0.46/0.79 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------