%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN659-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 : n012.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.08s 0.40s
% Output : Proof 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c27_is_p22_1,negated_conjecture,
p22(c27),
file('theBenchmark.p',c27_is_p22_1) ).
cnf(p10_2,negated_conjecture,
p10(X0,X0),
file('theBenchmark.p',p10_2) ).
cnf(p7_3,negated_conjecture,
p7(X87,X87),
file('theBenchmark.p',p7_3) ).
cnf(p6_4,negated_conjecture,
p6(X84,X84),
file('theBenchmark.p',p6_4) ).
cnf(p3_5,negated_conjecture,
p3(X79,X79),
file('theBenchmark.p',p3_5) ).
cnf(p20_6,negated_conjecture,
p20(X51,X51),
file('theBenchmark.p',p20_6) ).
cnf(p2_7,negated_conjecture,
p2(X32,X32),
file('theBenchmark.p',p2_7) ).
cnf(p19_8,negated_conjecture,
p19(X29,X29),
file('theBenchmark.p',p19_8) ).
cnf(p14_9,negated_conjecture,
p14(X20,X20),
file('theBenchmark.p',p14_9) ).
cnf(p12_10,negated_conjecture,
p12(X13,X13),
file('theBenchmark.p',p12_10) ).
cnf(p2_11,negated_conjecture,
p2(c41,c38),
file('theBenchmark.p',p2_11) ).
cnf(p10_12,negated_conjecture,
p10(f16(c31),c32),
file('theBenchmark.p',p10_12) ).
cnf(p7_13,negated_conjecture,
p7(f8(c28),c29),
file('theBenchmark.p',p7_13) ).
cnf(p2_14,negated_conjecture,
p2(f17(c36),c38),
file('theBenchmark.p',p2_14) ).
cnf(p2_15,negated_conjecture,
p2(f17(c31),c33),
file('theBenchmark.p',p2_15) ).
cnf(p10_16,negated_conjecture,
p10(f16(c36),c37),
file('theBenchmark.p',p10_16) ).
cnf(not_p14_17,negated_conjecture,
~ p14(f18(c34),c35),
file('theBenchmark.p',not_p14_17) ).
cnf(p23_18,negated_conjecture,
p23(c27,f4(f5(X66)),f4(X66)),
file('theBenchmark.p',p23_18) ).
cnf(p22_19,negated_conjecture,
( ~ p19(X59,X58)
| ~ p22(X59)
| p22(X58) ),
file('theBenchmark.p',p22_19) ).
cnf(p10_20,negated_conjecture,
( ~ p12(X11,X12)
| p10(f16(X11),f16(X12)) ),
file('theBenchmark.p',p10_20) ).
cnf(p7_21,negated_conjecture,
( ~ p6(X90,X91)
| p7(f8(X90),f8(X91)) ),
file('theBenchmark.p',p7_21) ).
cnf(p3_22,negated_conjecture,
( ~ p2(X82,X83)
| p3(f4(X82),f4(X83)) ),
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(p2_25,negated_conjecture,
( ~ p12(X45,X46)
| p2(f17(X45),f17(X46)) ),
file('theBenchmark.p',p2_25) ).
cnf(p14_26,negated_conjecture,
( ~ p14(X27,X28)
| p14(f18(X27),f18(X28)) ),
file('theBenchmark.p',p14_26) ).
cnf(p24_27,negated_conjecture,
p24(f15(c29,f13(c40,c41)),f13(c32,c33)),
file('theBenchmark.p',p24_27) ).
cnf(p24_28,negated_conjecture,
p24(f15(c29,f13(c37,c38)),f13(c32,c33)),
file('theBenchmark.p',p24_28) ).
cnf(p12_29,negated_conjecture,
p12(f13(f16(c39),f17(c39)),f13(c40,c41)),
file('theBenchmark.p',p12_29) ).
cnf(p10_30,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_30) ).
cnf(p7_31,negated_conjecture,
( ~ p7(X87,X89)
| ~ p7(X87,X88)
| p7(X88,X89) ),
file('theBenchmark.p',p7_31) ).
cnf(p6_32,negated_conjecture,
( ~ p6(X84,X86)
| ~ p6(X84,X85)
| p6(X85,X86) ),
file('theBenchmark.p',p6_32) ).
cnf(p3_33,negated_conjecture,
( ~ p3(X79,X81)
| ~ p3(X79,X80)
| p3(X80,X81) ),
file('theBenchmark.p',p3_33) ).
cnf(p20_34,negated_conjecture,
( ~ p20(X51,X53)
| ~ p20(X51,X52)
| p20(X52,X53) ),
file('theBenchmark.p',p20_34) ).
cnf(p2_35,negated_conjecture,
( ~ p2(X32,X34)
| ~ p2(X32,X33)
| p2(X33,X34) ),
file('theBenchmark.p',p2_35) ).
cnf(p19_36,negated_conjecture,
( ~ p19(X29,X31)
| ~ p19(X29,X30)
| p19(X30,X31) ),
file('theBenchmark.p',p19_36) ).
cnf(p14_37,negated_conjecture,
( ~ p14(X20,X22)
| ~ p14(X20,X21)
| p14(X21,X22) ),
file('theBenchmark.p',p14_37) ).
cnf(p12_38,negated_conjecture,
( ~ p12(X13,X15)
| ~ p12(X13,X14)
| p12(X14,X15) ),
file('theBenchmark.p',p12_38) ).
cnf(not_p24_39,negated_conjecture,
~ p24(f15(c29,f13(f16(c39),f17(c39))),f13(c32,c33)),
file('theBenchmark.p',not_p24_39) ).
cnf(p26_40,negated_conjecture,
( ~ p2(X77,X75)
| ~ p26(X77,X78)
| ~ p2(X78,X76)
| p26(X75,X76) ),
file('theBenchmark.p',p26_40) ).
cnf(p24_41,negated_conjecture,
( ~ p12(X69,X68)
| ~ p24(X70,X69)
| ~ p14(X70,X67)
| p24(X67,X68) ),
file('theBenchmark.p',p24_41) ).
cnf(p25_42,negated_conjecture,
( ~ p10(X73,X72)
| ~ p25(X74,X73)
| ~ p20(X74,X71)
| p25(X71,X72) ),
file('theBenchmark.p',p25_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(X17,X19)
| ~ p10(X16,X18)
| p12(f13(X16,X17),f13(X18,X19)) ),
file('theBenchmark.p',p12_44) ).
cnf(p14_45,negated_conjecture,
( ~ p7(X23,X25)
| ~ p12(X24,X26)
| p14(f15(X23,X24),f15(X25,X26)) ),
file('theBenchmark.p',p14_45) ).
cnf(p2_46,negated_conjecture,
( ~ p3(X41,X43)
| ~ p10(X42,X44)
| p2(f11(X41,X42),f11(X43,X44)) ),
file('theBenchmark.p',p2_46) ).
cnf(p10_47,negated_conjecture,
( ~ p24(f15(c29,f13(X7,X9)),f13(X8,X10))
| p25(f21(c27,X7),X8)
| p10(X7,X8) ),
file('theBenchmark.p',p10_47) ).
cnf(p23_48,negated_conjecture,
( ~ p23(X63,X64,X65)
| ~ p19(X63,X60)
| ~ p3(X64,X61)
| ~ p3(X65,X62)
| p23(X60,X61,X62) ),
file('theBenchmark.p',p23_48) ).
cnf(p10_49,negated_conjecture,
( ~ p24(f15(c29,f13(X3,X5)),f13(X4,X6))
| ~ p2(f11(f4(X5),X3),f9(c30))
| p10(X3,X4) ),
file('theBenchmark.p',p10_49) ).
cnf(p2_50,negated_conjecture,
( ~ p24(f15(c29,f13(X40,X36)),f13(X38,X39))
| ~ p24(f15(c29,f13(X37,X35)),f13(X38,X39))
| p2(X35,X36) ),
file('theBenchmark.p',p2_50) ).
cnf(p25_51,negated_conjecture,
( ~ p24(f15(c29,f13(X7,X9)),f13(X8,X10))
| p26(f11(f4(X9),X8),f11(f4(X10),X8))
| p25(f21(c27,X7),X8) ),
file('theBenchmark.p',p25_51) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN659-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.01 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.02 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Sun Sep 20 07:06:24 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.08/0.40 % SZS status Unsatisfiable for theBenchmark
% 0.08/0.40 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------