%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN672-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 : 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:50 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.40s
% Output : Proof 0.10s
% 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(X105,X105),
file('theBenchmark.p',p9_2) ).
cnf(p8_3,negated_conjecture,
p8(X98,X98),
file('theBenchmark.p',p8_3) ).
cnf(p6_4,negated_conjecture,
p6(X95,X95),
file('theBenchmark.p',p6_4) ).
cnf(p5_5,negated_conjecture,
p5(X92,X92),
file('theBenchmark.p',p5_5) ).
cnf(p3_6,negated_conjecture,
p3(X62,X62),
file('theBenchmark.p',p3_6) ).
cnf(p28_7,negated_conjecture,
p28(X57,X57),
file('theBenchmark.p',p28_7) ).
cnf(p26_8,negated_conjecture,
p26(X54,X54),
file('theBenchmark.p',p26_8) ).
cnf(p24_9,negated_conjecture,
p24(X47,X47),
file('theBenchmark.p',p24_9) ).
cnf(p22_10,negated_conjecture,
p22(X40,X40),
file('theBenchmark.p',p22_10) ).
cnf(p21_11,negated_conjecture,
p21(X33,X33),
file('theBenchmark.p',p21_11) ).
cnf(p2_12,negated_conjecture,
p2(X26,X26),
file('theBenchmark.p',p2_12) ).
cnf(p19_13,negated_conjecture,
p19(X19,X19),
file('theBenchmark.p',p19_13) ).
cnf(p18_14,negated_conjecture,
p18(X16,X16),
file('theBenchmark.p',p18_14) ).
cnf(p16_15,negated_conjecture,
p16(X9,X9),
file('theBenchmark.p',p16_15) ).
cnf(p15_16,negated_conjecture,
p15(X6,X6),
file('theBenchmark.p',p15_16) ).
cnf(p13_17,negated_conjecture,
p13(X3,X3),
file('theBenchmark.p',p13_17) ).
cnf(not_p3_18,negated_conjecture,
~ p3(c40,f14(c38,c39)),
file('theBenchmark.p',not_p3_18) ).
cnf(p31_19,negated_conjecture,
p31(f20(c36,c39),f17(c37,c40)),
file('theBenchmark.p',p31_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(X105,X107)
| ~ p9(X105,X106)
| p9(X106,X107) ),
file('theBenchmark.p',p9_21) ).
cnf(p8_22,negated_conjecture,
( ~ p8(X98,X100)
| ~ p8(X98,X99)
| p8(X99,X100) ),
file('theBenchmark.p',p8_22) ).
cnf(p6_23,negated_conjecture,
( ~ p6(X95,X97)
| ~ p6(X95,X96)
| p6(X96,X97) ),
file('theBenchmark.p',p6_23) ).
cnf(p5_24,negated_conjecture,
( ~ p5(X92,X94)
| ~ p5(X92,X93)
| p5(X93,X94) ),
file('theBenchmark.p',p5_24) ).
cnf(p3_25,negated_conjecture,
( ~ p3(X62,X64)
| ~ p3(X62,X63)
| p3(X63,X64) ),
file('theBenchmark.p',p3_25) ).
cnf(p28_26,negated_conjecture,
( ~ p28(X57,X59)
| ~ p28(X57,X58)
| p28(X58,X59) ),
file('theBenchmark.p',p28_26) ).
cnf(p26_27,negated_conjecture,
( ~ p26(X54,X56)
| ~ p26(X54,X55)
| p26(X55,X56) ),
file('theBenchmark.p',p26_27) ).
cnf(p24_28,negated_conjecture,
( ~ p24(X47,X49)
| ~ p24(X47,X48)
| p24(X48,X49) ),
file('theBenchmark.p',p24_28) ).
cnf(p22_29,negated_conjecture,
( ~ p22(X40,X42)
| ~ p22(X40,X41)
| p22(X41,X42) ),
file('theBenchmark.p',p22_29) ).
cnf(p21_30,negated_conjecture,
( ~ p21(X33,X35)
| ~ p21(X33,X34)
| p21(X34,X35) ),
file('theBenchmark.p',p21_30) ).
cnf(p2_31,negated_conjecture,
( ~ p2(X26,X28)
| ~ p2(X26,X27)
| p2(X27,X28) ),
file('theBenchmark.p',p2_31) ).
cnf(p19_32,negated_conjecture,
( ~ p19(X19,X21)
| ~ p19(X19,X20)
| p19(X20,X21) ),
file('theBenchmark.p',p19_32) ).
cnf(p18_33,negated_conjecture,
( ~ p18(X16,X18)
| ~ p18(X16,X17)
| p18(X17,X18) ),
file('theBenchmark.p',p18_33) ).
cnf(p16_34,negated_conjecture,
( ~ p16(X9,X11)
| ~ p16(X9,X10)
| p16(X10,X11) ),
file('theBenchmark.p',p16_34) ).
cnf(p15_35,negated_conjecture,
( ~ p15(X6,X8)
| ~ p15(X6,X7)
| p15(X7,X8) ),
file('theBenchmark.p',p15_35) ).
cnf(p13_36,negated_conjecture,
( ~ p13(X3,X5)
| ~ p13(X3,X4)
| p13(X4,X5) ),
file('theBenchmark.p',p13_36) ).
cnf(p3_37,negated_conjecture,
p3(f4(f7(c34,X77),f14(c38,X78)),f14(X77,X78)),
file('theBenchmark.p',p3_37) ).
cnf(p31_38,negated_conjecture,
( ~ p16(X90,X89)
| ~ p31(X91,X90)
| ~ p19(X91,X88)
| p31(X88,X89) ),
file('theBenchmark.p',p31_38) ).
cnf(p30_39,negated_conjecture,
( ~ p3(X84,X83)
| ~ p9(X85,X82)
| ~ p30(X85,X84)
| p30(X82,X83) ),
file('theBenchmark.p',p30_39) ).
cnf(not_p30_40,negated_conjecture,
~ p30(f10(f12(c32,c33),f14(c35,c39)),f4(f7(c34,c35),c40)),
file('theBenchmark.p',not_p30_40) ).
cnf(p16_41,negated_conjecture,
( ~ p3(X13,X15)
| ~ p15(X12,X14)
| p16(f17(X12,X13),f17(X14,X15)) ),
file('theBenchmark.p',p16_41) ).
cnf(p9_42,negated_conjecture,
( ~ p8(X108,X110)
| ~ p3(X109,X111)
| p9(f10(X108,X109),f10(X110,X111)) ),
file('theBenchmark.p',p9_42) ).
cnf(p8_43,negated_conjecture,
( ~ p8(X102,X104)
| ~ p11(X101,X103)
| p8(f12(X101,X102),f12(X103,X104)) ),
file('theBenchmark.p',p8_43) ).
cnf(p3_44,negated_conjecture,
( ~ p3(X74,X76)
| ~ p2(X73,X75)
| p3(f4(X73,X74),f4(X75,X76)) ),
file('theBenchmark.p',p3_44) ).
cnf(p3_45,negated_conjecture,
( ~ p22(X70,X72)
| ~ p21(X69,X71)
| p3(f23(X69,X70),f23(X71,X72)) ),
file('theBenchmark.p',p3_45) ).
cnf(p3_46,negated_conjecture,
( ~ p6(X65,X67)
| ~ p13(X66,X68)
| p3(f14(X65,X66),f14(X67,X68)) ),
file('theBenchmark.p',p3_46) ).
cnf(p24_47,negated_conjecture,
( ~ p26(X50,X52)
| ~ p2(X51,X53)
| p24(f27(X50,X51),f27(X52,X53)) ),
file('theBenchmark.p',p24_47) ).
cnf(p22_48,negated_conjecture,
( ~ p24(X43,X45)
| ~ p22(X44,X46)
| p22(f25(X43,X44),f25(X45,X46)) ),
file('theBenchmark.p',p22_48) ).
cnf(p21_49,negated_conjecture,
( ~ p28(X36,X38)
| ~ p13(X37,X39)
| p21(f29(X36,X37),f29(X38,X39)) ),
file('theBenchmark.p',p21_49) ).
cnf(p2_50,negated_conjecture,
( ~ p6(X30,X32)
| ~ p5(X29,X31)
| p2(f7(X29,X30),f7(X31,X32)) ),
file('theBenchmark.p',p2_50) ).
cnf(p19_51,negated_conjecture,
( ~ p18(X22,X24)
| ~ p13(X23,X25)
| p19(f20(X22,X23),f20(X24,X25)) ),
file('theBenchmark.p',p19_51) ).
cnf(p3_52,negated_conjecture,
p3(f4(f7(c34,X79),f23(f29(c41,X80),X81)),f23(f29(c41,X80),f25(f27(c42,f7(c34,X79)),X81))),
file('theBenchmark.p',p3_52) ).
cnf(p3_53,negated_conjecture,
( ~ p31(f20(c36,X61),f17(c37,X60))
| p30(f10(f12(c32,c33),f14(c38,X61)),X60)
| p3(X60,f14(c38,X61)) ),
file('theBenchmark.p',p3_53) ).
cnf(p30_54,negated_conjecture,
( ~ p30(f10(f12(c32,c33),X86),X87)
| p30(f10(f12(c32,c33),f4(f7(c34,c35),X86)),f4(f7(c34,c35),X87)) ),
file('theBenchmark.p',p30_54) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN672-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.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 07:06:28 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % SZS status Unsatisfiable for theBenchmark
% 0.10/0.40 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------