%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN656-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 : n010.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.15s 10.58s
% Output : Proof 0.15s
% 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(X88,X88),
file('theBenchmark.p',p9_2) ).
cnf(p8_3,negated_conjecture,
p8(X85,X85),
file('theBenchmark.p',p8_3) ).
cnf(p6_4,negated_conjecture,
p6(X82,X82),
file('theBenchmark.p',p6_4) ).
cnf(p4_5,negated_conjecture,
p4(X75,X75),
file('theBenchmark.p',p4_5) ).
cnf(p3_6,negated_conjecture,
p3(X64,X64),
file('theBenchmark.p',p3_6) ).
cnf(p22_7,negated_conjecture,
p22(X41,X41),
file('theBenchmark.p',p22_7) ).
cnf(p20_8,negated_conjecture,
p20(X34,X34),
file('theBenchmark.p',p20_8) ).
cnf(p2_9,negated_conjecture,
p2(X27,X27),
file('theBenchmark.p',p2_9) ).
cnf(p18_10,negated_conjecture,
p18(X20,X20),
file('theBenchmark.p',p18_10) ).
cnf(p16_11,negated_conjecture,
p16(X17,X17),
file('theBenchmark.p',p16_11) ).
cnf(p14_12,negated_conjecture,
p14(X10,X10),
file('theBenchmark.p',p14_12) ).
cnf(p12_13,negated_conjecture,
p12(X3,X3),
file('theBenchmark.p',p12_13) ).
cnf(p24_14,negated_conjecture,
p24(c26,c27),
file('theBenchmark.p',p24_14) ).
cnf(p24_15,negated_conjecture,
p24(f10(c30,f13(c31,X50)),c27),
file('theBenchmark.p',p24_15) ).
cnf(not_p25_16,negated_conjecture,
~ p25(f5(f7(c28,c29),X95),X95),
file('theBenchmark.p',not_p25_16) ).
cnf(p11_17,negated_conjecture,
( ~ p11(X0,X2)
| ~ p11(X0,X1)
| p11(X1,X2) ),
file('theBenchmark.p',p11_17) ).
cnf(p9_18,negated_conjecture,
( ~ p9(X88,X90)
| ~ p9(X88,X89)
| p9(X89,X90) ),
file('theBenchmark.p',p9_18) ).
cnf(p8_19,negated_conjecture,
( ~ p8(X85,X87)
| ~ p8(X85,X86)
| p8(X86,X87) ),
file('theBenchmark.p',p8_19) ).
cnf(p6_20,negated_conjecture,
( ~ p6(X82,X84)
| ~ p6(X82,X83)
| p6(X83,X84) ),
file('theBenchmark.p',p6_20) ).
cnf(p4_21,negated_conjecture,
( ~ p4(X75,X77)
| ~ p4(X75,X76)
| p4(X76,X77) ),
file('theBenchmark.p',p4_21) ).
cnf(p3_22,negated_conjecture,
( ~ p3(X64,X66)
| ~ p3(X64,X65)
| p3(X65,X66) ),
file('theBenchmark.p',p3_22) ).
cnf(p22_23,negated_conjecture,
( ~ p22(X41,X43)
| ~ p22(X41,X42)
| p22(X42,X43) ),
file('theBenchmark.p',p22_23) ).
cnf(p20_24,negated_conjecture,
( ~ p20(X34,X36)
| ~ p20(X34,X35)
| p20(X35,X36) ),
file('theBenchmark.p',p20_24) ).
cnf(p2_25,negated_conjecture,
( ~ p2(X27,X29)
| ~ p2(X27,X28)
| p2(X28,X29) ),
file('theBenchmark.p',p2_25) ).
cnf(p18_26,negated_conjecture,
( ~ p18(X20,X22)
| ~ p18(X20,X21)
| p18(X21,X22) ),
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(X10,X12)
| ~ p14(X10,X11)
| p14(X11,X12) ),
file('theBenchmark.p',p14_28) ).
cnf(p12_29,negated_conjecture,
( ~ p12(X3,X5)
| ~ p12(X3,X4)
| p12(X4,X5) ),
file('theBenchmark.p',p12_29) ).
cnf(p24_30,negated_conjecture,
( ~ p25(f5(c29,X49),X48)
| p24(f10(c30,X48),c27) ),
file('theBenchmark.p',p24_30) ).
cnf(p25_31,negated_conjecture,
p25(f5(c29,f13(c31,f15(c32,X58))),f13(c31,X58)),
file('theBenchmark.p',p25_31) ).
cnf(p25_32,negated_conjecture,
( ~ p25(f5(X55,X56),X57)
| p25(f5(f7(c28,X55),X56),X57) ),
file('theBenchmark.p',p25_32) ).
cnf(p25_33,negated_conjecture,
( ~ p25(f5(X59,X60),X61)
| p25(f5(f7(c28,X59),X60),X61) ),
file('theBenchmark.p',p25_33) ).
cnf(p24_34,negated_conjecture,
( ~ p24(X46,X47)
| ~ p9(X46,X44)
| ~ p4(X47,X45)
| p24(X44,X45) ),
file('theBenchmark.p',p24_34) ).
cnf(p25_35,negated_conjecture,
( ~ p25(X53,X54)
| ~ p4(X53,X51)
| ~ p3(X54,X52)
| p25(X51,X52) ),
file('theBenchmark.p',p25_35) ).
cnf(p9_36,negated_conjecture,
( ~ p8(X91,X93)
| ~ p3(X92,X94)
| p9(f10(X91,X92),f10(X93,X94)) ),
file('theBenchmark.p',p9_36) ).
cnf(p12_37,negated_conjecture,
( ~ p14(X6,X8)
| ~ p12(X7,X9)
| p12(f15(X6,X7),f15(X8,X9)) ),
file('theBenchmark.p',p12_37) ).
cnf(p14_38,negated_conjecture,
( ~ p16(X13,X15)
| ~ p12(X14,X16)
| p14(f17(X13,X14),f17(X15,X16)) ),
file('theBenchmark.p',p14_38) ).
cnf(p18_39,negated_conjecture,
( ~ p3(X24,X26)
| ~ p20(X23,X25)
| p18(f21(X23,X24),f21(X25,X26)) ),
file('theBenchmark.p',p18_39) ).
cnf(p2_40,negated_conjecture,
( ~ p6(X30,X32)
| ~ p2(X31,X33)
| p2(f7(X30,X31),f7(X32,X33)) ),
file('theBenchmark.p',p2_40) ).
cnf(p20_41,negated_conjecture,
( ~ p22(X37,X39)
| ~ p2(X38,X40)
| p20(f23(X37,X38),f23(X39,X40)) ),
file('theBenchmark.p',p20_41) ).
cnf(p3_42,negated_conjecture,
( ~ p12(X68,X70)
| ~ p11(X67,X69)
| p3(f13(X67,X68),f13(X69,X70)) ),
file('theBenchmark.p',p3_42) ).
cnf(p3_43,negated_conjecture,
( ~ p3(X72,X74)
| ~ p18(X71,X73)
| p3(f19(X71,X72),f19(X73,X74)) ),
file('theBenchmark.p',p3_43) ).
cnf(p4_44,negated_conjecture,
( ~ p3(X79,X81)
| ~ p2(X78,X80)
| p4(f5(X78,X79),f5(X80,X81)) ),
file('theBenchmark.p',p4_44) ).
cnf(not_p25_45,negated_conjecture,
~ p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)),
file('theBenchmark.p',not_p25_45) ).
cnf(p25_46,negated_conjecture,
( ~ p25(f5(f7(c28,X55),X62),X57)
| ~ p25(f5(X55,X56),X62)
| p25(f5(f7(c28,X55),X56),X57) ),
file('theBenchmark.p',p25_46) ).
cnf(p25_47,negated_conjecture,
( ~ p25(f5(f7(c28,X55),X56),X57)
| p25(f5(X55,X56),f19(f21(f23(c36,X55),X56),X57))
| p25(f5(X55,X56),X57) ),
file('theBenchmark.p',p25_47) ).
cnf(p25_48,negated_conjecture,
( ~ p25(f5(f7(c28,X55),X56),X57)
| p25(f5(f7(c28,X55),f19(f21(f23(c36,X55),X56),X57)),X57)
| p25(f5(X55,X56),X57) ),
file('theBenchmark.p',p25_48) ).
cnf(p3_49,negated_conjecture,
( p25(f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),X63))),f13(c31,c34))
| p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),X63))) ),
file('theBenchmark.p',p3_49) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN656-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.05 % 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/10.38 % Computer : n010.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Sun Sep 20 07:07:08 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.15/10.58 % SZS status Unsatisfiable for theBenchmark
% 0.15/10.58 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------