%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN648-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 : n004.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:47 AM UTC 2026
% Result : Unsatisfiable 0.11s 0.39s
% Output : Proof 0.11s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(p10_1,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_1) ).
cnf(p8_2,negated_conjecture,
p8(X86,X86),
file('theBenchmark.p',p8_2) ).
cnf(p7_3,negated_conjecture,
p7(X79,X79),
file('theBenchmark.p',p7_3) ).
cnf(p5_4,negated_conjecture,
p5(X76,X76),
file('theBenchmark.p',p5_4) ).
cnf(p3_5,negated_conjecture,
p3(X65,X65),
file('theBenchmark.p',p3_5) ).
cnf(p25_6,negated_conjecture,
p25(X58,X58),
file('theBenchmark.p',p25_6) ).
cnf(p22_7,negated_conjecture,
p22(X45,X45),
file('theBenchmark.p',p22_7) ).
cnf(p20_8,negated_conjecture,
p20(X38,X38),
file('theBenchmark.p',p20_8) ).
cnf(p2_9,negated_conjecture,
p2(X31,X31),
file('theBenchmark.p',p2_9) ).
cnf(p18_10,negated_conjecture,
p18(X24,X24),
file('theBenchmark.p',p18_10) ).
cnf(p16_11,negated_conjecture,
p16(X17,X17),
file('theBenchmark.p',p16_11) ).
cnf(p14_12,negated_conjecture,
p14(X14,X14),
file('theBenchmark.p',p14_12) ).
cnf(p12_13,negated_conjecture,
p12(X7,X7),
file('theBenchmark.p',p12_13) ).
cnf(p2_14,negated_conjecture,
p2(c27,c30),
file('theBenchmark.p',p2_14) ).
cnf(p26_15,negated_conjecture,
p26(c31,c30),
file('theBenchmark.p',p26_15) ).
cnf(not_p24_16,negated_conjecture,
~ p24(f4(c27,c28),c29),
file('theBenchmark.p',not_p24_16) ).
cnf(p10_17,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_17) ).
cnf(p8_18,negated_conjecture,
( ~ p8(X86,X88)
| ~ p8(X86,X87)
| p8(X87,X88) ),
file('theBenchmark.p',p8_18) ).
cnf(p7_19,negated_conjecture,
( ~ p7(X79,X81)
| ~ p7(X79,X80)
| p7(X80,X81) ),
file('theBenchmark.p',p7_19) ).
cnf(p5_20,negated_conjecture,
( ~ p5(X76,X78)
| ~ p5(X76,X77)
| p5(X77,X78) ),
file('theBenchmark.p',p5_20) ).
cnf(p3_21,negated_conjecture,
( ~ p3(X65,X67)
| ~ p3(X65,X66)
| p3(X66,X67) ),
file('theBenchmark.p',p3_21) ).
cnf(p25_22,negated_conjecture,
( ~ p25(X58,X60)
| ~ p25(X58,X59)
| p25(X59,X60) ),
file('theBenchmark.p',p25_22) ).
cnf(p22_23,negated_conjecture,
( ~ p22(X45,X47)
| ~ p22(X45,X46)
| p22(X46,X47) ),
file('theBenchmark.p',p22_23) ).
cnf(p20_24,negated_conjecture,
( ~ p20(X38,X40)
| ~ p20(X38,X39)
| p20(X39,X40) ),
file('theBenchmark.p',p20_24) ).
cnf(p2_25,negated_conjecture,
( ~ p2(X31,X33)
| ~ p2(X31,X32)
| p2(X32,X33) ),
file('theBenchmark.p',p2_25) ).
cnf(p18_26,negated_conjecture,
( ~ p18(X24,X26)
| ~ p18(X24,X25)
| p18(X25,X26) ),
file('theBenchmark.p',p18_26) ).
cnf(p16_27,negated_conjecture,
( ~ p16(X17,X19)
| ~ p16(X17,X18)
| p16(X18,X19) ),
file('theBenchmark.p',p16_27) ).
cnf(p14_28,negated_conjecture,
( ~ p14(X14,X16)
| ~ p14(X14,X15)
| p14(X15,X16) ),
file('theBenchmark.p',p14_28) ).
cnf(p12_29,negated_conjecture,
( ~ p12(X7,X9)
| ~ p12(X7,X8)
| p12(X8,X9) ),
file('theBenchmark.p',p12_29) ).
cnf(p24_30,negated_conjecture,
( ~ p24(f4(f6(c32,c30),X56),X57)
| p24(f4(c30,X56),X57) ),
file('theBenchmark.p',p24_30) ).
cnf(p24_31,negated_conjecture,
( ~ p24(X50,X51)
| ~ p8(X51,X49)
| ~ p3(X50,X48)
| p24(X48,X49) ),
file('theBenchmark.p',p24_31) ).
cnf(p26_32,negated_conjecture,
( ~ p2(X63,X62)
| ~ p26(X64,X63)
| ~ p25(X64,X61)
| p26(X61,X62) ),
file('theBenchmark.p',p26_32) ).
cnf(p8_33,negated_conjecture,
( ~ p7(X89,X91)
| ~ p2(X90,X92)
| p8(f9(X89,X90),f9(X91,X92)) ),
file('theBenchmark.p',p8_33) ).
cnf(p10_34,negated_conjecture,
( ~ p3(X4,X6)
| ~ p12(X3,X5)
| p10(f13(X3,X4),f13(X5,X6)) ),
file('theBenchmark.p',p10_34) ).
cnf(p12_35,negated_conjecture,
( ~ p3(X11,X13)
| ~ p14(X10,X12)
| p12(f15(X10,X11),f15(X12,X13)) ),
file('theBenchmark.p',p12_35) ).
cnf(p16_36,negated_conjecture,
( ~ p2(X21,X23)
| ~ p18(X20,X22)
| p16(f19(X20,X21),f19(X22,X23)) ),
file('theBenchmark.p',p16_36) ).
cnf(p18_37,negated_conjecture,
( ~ p3(X28,X30)
| ~ p20(X27,X29)
| p18(f21(X27,X28),f21(X29,X30)) ),
file('theBenchmark.p',p18_37) ).
cnf(p2_38,negated_conjecture,
( ~ p5(X34,X36)
| ~ p2(X35,X37)
| p2(f6(X34,X35),f6(X36,X37)) ),
file('theBenchmark.p',p2_38) ).
cnf(p20_39,negated_conjecture,
( ~ p3(X42,X44)
| ~ p22(X41,X43)
| p20(f23(X41,X42),f23(X43,X44)) ),
file('theBenchmark.p',p20_39) ).
cnf(p3_40,negated_conjecture,
( ~ p2(X69,X71)
| ~ p16(X68,X70)
| p3(f17(X68,X69),f17(X70,X71)) ),
file('theBenchmark.p',p3_40) ).
cnf(p3_41,negated_conjecture,
( ~ p3(X73,X75)
| ~ p2(X72,X74)
| p3(f4(X72,X73),f4(X74,X75)) ),
file('theBenchmark.p',p3_41) ).
cnf(p7_42,negated_conjecture,
( ~ p2(X83,X85)
| ~ p10(X82,X84)
| p7(f11(X82,X83),f11(X84,X85)) ),
file('theBenchmark.p',p7_42) ).
cnf(p24_43,negated_conjecture,
( ~ p24(f4(X53,f17(f19(f21(f23(c33,X52),X54),X55),X53)),f9(f11(f13(f15(c34,X52),X54),X55),X53))
| ~ p3(X54,f4(X55,c28))
| ~ p26(c31,X53)
| ~ p2(X55,X53)
| ~ p3(X52,X54)
| p24(X52,c29) ),
file('theBenchmark.p',p24_43) ).
cnf(p24_44,negated_conjecture,
( ~ p3(X54,f4(X55,c28))
| ~ p26(c31,X53)
| ~ p2(X55,X53)
| ~ p3(X52,X54)
| p24(f4(f6(c32,X53),f17(f19(f21(f23(c33,X52),X54),X55),X53)),f9(f11(f13(f15(c34,X52),X54),X55),X53))
| p24(X52,c29) ),
file('theBenchmark.p',p24_44) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN648-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.11/0.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 07:06:19 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.11/0.39 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------