%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN666-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:49 AM UTC 2026
% Result : Unsatisfiable 0.41s 0.68s
% Output : Proof 0.41s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c28_is_p22_1,negated_conjecture,
p22(c28),
file('theBenchmark.p',c28_is_p22_1) ).
cnf(p10_2,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_2) ).
cnf(p7_3,negated_conjecture,
p7(X91,X91),
file('theBenchmark.p',p7_3) ).
cnf(p6_4,negated_conjecture,
p6(X88,X88),
file('theBenchmark.p',p6_4) ).
cnf(p3_5,negated_conjecture,
p3(X83,X83),
file('theBenchmark.p',p3_5) ).
cnf(p20_6,negated_conjecture,
p20(X51,X51),
file('theBenchmark.p',p20_6) ).
cnf(p2_7,negated_conjecture,
p2(X28,X28),
file('theBenchmark.p',p2_7) ).
cnf(p19_8,negated_conjecture,
p19(X25,X25),
file('theBenchmark.p',p19_8) ).
cnf(p14_9,negated_conjecture,
p14(X18,X18),
file('theBenchmark.p',p14_9) ).
cnf(p12_10,negated_conjecture,
p12(X11,X11),
file('theBenchmark.p',p12_10) ).
cnf(p10_11,negated_conjecture,
p10(c35,c34),
file('theBenchmark.p',p10_11) ).
cnf(p25_12,negated_conjecture,
p25(c33,c36),
file('theBenchmark.p',p25_12) ).
cnf(p25_13,negated_conjecture,
p25(c32,c36),
file('theBenchmark.p',p25_13) ).
cnf(p25_14,negated_conjecture,
p25(c32,c33),
file('theBenchmark.p',p25_14) ).
cnf(p7_15,negated_conjecture,
p7(f8(c29),c30),
file('theBenchmark.p',p7_15) ).
cnf(p26_16,negated_conjecture,
p26(f21(c28,c37),c34),
file('theBenchmark.p',p26_16) ).
cnf(p23_17,negated_conjecture,
p23(c28,f4(f5(X66)),f4(X66)),
file('theBenchmark.p',p23_17) ).
cnf(not_p2_18,negated_conjecture,
~ p2(X96,f18(X96,f9(f17(c31)))),
file('theBenchmark.p',not_p2_18) ).
cnf(p22_19,negated_conjecture,
( ~ p19(X59,X58)
| ~ p22(X59)
| p22(X58) ),
file('theBenchmark.p',p22_19) ).
cnf(p2_20,negated_conjecture,
( ~ p2(X41,X42)
| p2(f17(X41),f17(X42)) ),
file('theBenchmark.p',p2_20) ).
cnf(p7_21,negated_conjecture,
( ~ p6(X94,X95)
| p7(f8(X94),f8(X95)) ),
file('theBenchmark.p',p7_21) ).
cnf(p3_22,negated_conjecture,
( ~ p2(X86,X87)
| p3(f4(X86),f4(X87)) ),
file('theBenchmark.p',p3_22) ).
cnf(p2_23,negated_conjecture,
( ~ p2(X49,X50)
| p2(f9(X49),f9(X50)) ),
file('theBenchmark.p',p2_23) ).
cnf(p2_24,negated_conjecture,
( ~ p2(X47,X48)
| p2(f5(X47),f5(X48)) ),
file('theBenchmark.p',p2_24) ).
cnf(p10_25,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_25) ).
cnf(p7_26,negated_conjecture,
( ~ p7(X91,X93)
| ~ p7(X91,X92)
| p7(X92,X93) ),
file('theBenchmark.p',p7_26) ).
cnf(p6_27,negated_conjecture,
( ~ p6(X88,X90)
| ~ p6(X88,X89)
| p6(X89,X90) ),
file('theBenchmark.p',p6_27) ).
cnf(p3_28,negated_conjecture,
( ~ p3(X83,X85)
| ~ p3(X83,X84)
| p3(X84,X85) ),
file('theBenchmark.p',p3_28) ).
cnf(p20_29,negated_conjecture,
( ~ p20(X51,X53)
| ~ p20(X51,X52)
| p20(X52,X53) ),
file('theBenchmark.p',p20_29) ).
cnf(p2_30,negated_conjecture,
( ~ p2(X28,X30)
| ~ p2(X28,X29)
| p2(X29,X30) ),
file('theBenchmark.p',p2_30) ).
cnf(p19_31,negated_conjecture,
( ~ p19(X25,X27)
| ~ p19(X25,X26)
| p19(X26,X27) ),
file('theBenchmark.p',p19_31) ).
cnf(p14_32,negated_conjecture,
( ~ p14(X18,X20)
| ~ p14(X18,X19)
| p14(X19,X20) ),
file('theBenchmark.p',p14_32) ).
cnf(p12_33,negated_conjecture,
( ~ p12(X11,X13)
| ~ p12(X11,X12)
| p12(X12,X13) ),
file('theBenchmark.p',p12_33) ).
cnf(p27_34,negated_conjecture,
( ~ p2(X81,X79)
| ~ p27(X81,X82)
| ~ p2(X82,X80)
| p27(X79,X80) ),
file('theBenchmark.p',p27_34) ).
cnf(p24_35,negated_conjecture,
( ~ p12(X69,X68)
| ~ p24(X70,X69)
| ~ p14(X70,X67)
| p24(X67,X68) ),
file('theBenchmark.p',p24_35) ).
cnf(p25_36,negated_conjecture,
( ~ p2(X73,X71)
| ~ p25(X73,X74)
| ~ p2(X74,X72)
| p25(X71,X72) ),
file('theBenchmark.p',p25_36) ).
cnf(p26_37,negated_conjecture,
( ~ p10(X77,X76)
| ~ p26(X78,X77)
| ~ p20(X78,X75)
| p26(X75,X76) ),
file('theBenchmark.p',p26_37) ).
cnf(p2_38,negated_conjecture,
p2(f11(f4(c32),c34),f18(f11(f4(c33),c34),f9(f17(c31)))),
file('theBenchmark.p',p2_38) ).
cnf(p2_39,negated_conjecture,
p2(f11(f4(c32),c34),f18(f11(f4(c36),c34),f9(f17(c31)))),
file('theBenchmark.p',p2_39) ).
cnf(p27_40,negated_conjecture,
p27(f11(f4(c36),c37),f11(f4(f16(c36,f9(f17(c31)))),c37)),
file('theBenchmark.p',p27_40) ).
cnf(p25_41,negated_conjecture,
p25(f11(f4(c33),c35),f11(f4(f16(c33,f9(f17(c31)))),c35)),
file('theBenchmark.p',p25_41) ).
cnf(not_p2_42,negated_conjecture,
~ p2(f11(f4(f16(c32,f9(f17(c31)))),c34),f11(f4(c32),c34)),
file('theBenchmark.p',not_p2_42) ).
cnf(p20_43,negated_conjecture,
( ~ p19(X54,X56)
| ~ p10(X55,X57)
| p20(f21(X54,X55),f21(X56,X57)) ),
file('theBenchmark.p',p20_43) ).
cnf(p12_44,negated_conjecture,
( ~ p2(X15,X17)
| ~ p10(X14,X16)
| p12(f13(X14,X15),f13(X16,X17)) ),
file('theBenchmark.p',p12_44) ).
cnf(p14_45,negated_conjecture,
( ~ p7(X21,X23)
| ~ p12(X22,X24)
| p14(f15(X21,X22),f15(X23,X24)) ),
file('theBenchmark.p',p14_45) ).
cnf(p2_46,negated_conjecture,
( ~ p3(X31,X33)
| ~ p10(X32,X34)
| p2(f11(X31,X32),f11(X33,X34)) ),
file('theBenchmark.p',p2_46) ).
cnf(p2_47,negated_conjecture,
( ~ p2(X38,X40)
| ~ p2(X37,X39)
| p2(f16(X37,X38),f16(X39,X40)) ),
file('theBenchmark.p',p2_47) ).
cnf(p2_48,negated_conjecture,
( ~ p2(X44,X46)
| ~ p2(X43,X45)
| p2(f18(X43,X44),f18(X45,X46)) ),
file('theBenchmark.p',p2_48) ).
cnf(p2_49,negated_conjecture,
( ~ p25(c32,X35)
| ~ p25(X35,c33)
| p2(f11(f4(X35),c34),f11(f4(c32),c34)) ),
file('theBenchmark.p',p2_49) ).
cnf(p2_50,negated_conjecture,
( ~ p25(c32,X36)
| ~ p25(X36,c36)
| p2(f11(f4(X36),c34),f11(f4(c32),c34)) ),
file('theBenchmark.p',p2_50) ).
cnf(p10_51,negated_conjecture,
( ~ p24(f15(c30,f13(X7,X9)),f13(X8,X10))
| p26(f21(c28,X7),X8)
| p10(X7,X8) ),
file('theBenchmark.p',p10_51) ).
cnf(p23_52,negated_conjecture,
( ~ p23(X63,X64,X65)
| ~ p19(X63,X60)
| ~ p3(X64,X61)
| ~ p3(X65,X62)
| p23(X60,X61,X62) ),
file('theBenchmark.p',p23_52) ).
cnf(p10_53,negated_conjecture,
( ~ p24(f15(c30,f13(X3,X5)),f13(X4,X6))
| ~ p2(f11(f4(X5),X3),f9(c31))
| p10(X3,X4) ),
file('theBenchmark.p',p10_53) ).
cnf(p26_54,negated_conjecture,
( ~ p24(f15(c30,f13(X7,X9)),f13(X8,X10))
| p25(f11(f4(X9),X8),f11(f4(X10),X8))
| p26(f21(c28,X7),X8) ),
file('theBenchmark.p',p26_54) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN666-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.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 07:06:48 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.41/0.68 % SZS status Unsatisfiable for theBenchmark
% 0.41/0.68 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------