%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN697-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:53 AM UTC 2026
% Result : Unsatisfiable 0.40s 0.68s
% Output : Proof 0.40s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c34_is_p25_1,negated_conjecture,
p25(c34),
file('theBenchmark.p',c34_is_p25_1) ).
cnf(c36_is_p29_2,negated_conjecture,
p29(c36),
file('theBenchmark.p',c36_is_p29_2) ).
cnf(f18_is_p30_3,negated_conjecture,
p30(f18(c41)),
file('theBenchmark.p',f18_is_p30_3) ).
cnf(f16_is_p28_4,negated_conjecture,
p28(f16(c38)),
file('theBenchmark.p',f16_is_p28_4) ).
cnf(f16_is_p28_5,negated_conjecture,
p28(f16(c39)),
file('theBenchmark.p',f16_is_p28_5) ).
cnf(f18_is_p30_6,negated_conjecture,
p30(f18(c40)),
file('theBenchmark.p',f18_is_p30_6) ).
cnf(p10_7,negated_conjecture,
p10(X5,X5),
file('theBenchmark.p',p10_7) ).
cnf(p7_8,negated_conjecture,
p7(X112,X112),
file('theBenchmark.p',p7_8) ).
cnf(p6_9,negated_conjecture,
p6(X109,X109),
file('theBenchmark.p',p6_9) ).
cnf(p3_10,negated_conjecture,
p3(X88,X88),
file('theBenchmark.p',p3_10) ).
cnf(p21_11,negated_conjecture,
p21(X68,X68),
file('theBenchmark.p',p21_11) ).
cnf(p2_12,negated_conjecture,
p2(X43,X43),
file('theBenchmark.p',p2_12) ).
cnf(p17_13,negated_conjecture,
p17(X28,X28),
file('theBenchmark.p',p17_13) ).
cnf(p14_14,negated_conjecture,
p14(X19,X19),
file('theBenchmark.p',p14_14) ).
cnf(p12_15,negated_conjecture,
p12(X12,X12),
file('theBenchmark.p',p12_15) ).
cnf(p2_16,negated_conjecture,
p2(c44,c45),
file('theBenchmark.p',p2_16) ).
cnf(p31_17,negated_conjecture,
p31(c46,c42),
file('theBenchmark.p',p31_17) ).
cnf(p31_18,negated_conjecture,
p31(c45,f5(c42)),
file('theBenchmark.p',p31_18) ).
cnf(p31_19,negated_conjecture,
p31(c44,f5(c42)),
file('theBenchmark.p',p31_19) ).
cnf(p7_20,negated_conjecture,
p7(f8(c35),c36),
file('theBenchmark.p',p7_20) ).
cnf(p32_21,negated_conjecture,
p32(f22(c34,c43),c47),
file('theBenchmark.p',p32_21) ).
cnf(p31_22,negated_conjecture,
p31(f23(c44,f9(f20(c37))),c45),
file('theBenchmark.p',p31_22) ).
cnf(p26_23,negated_conjecture,
p26(c34,f4(f5(X79)),f4(X79)),
file('theBenchmark.p',p26_23) ).
cnf(p25_24,negated_conjecture,
( ~ p21(X72,X71)
| ~ p25(X72)
| p25(X71) ),
file('theBenchmark.p',p25_24) ).
cnf(p30_25,negated_conjecture,
( ~ p17(X94,X93)
| ~ p30(X94)
| p30(X93) ),
file('theBenchmark.p',p30_25) ).
cnf(p29_26,negated_conjecture,
( ~ p7(X87,X86)
| ~ p29(X87)
| p29(X86) ),
file('theBenchmark.p',p29_26) ).
cnf(p28_27,negated_conjecture,
( ~ p14(X85,X84)
| ~ p28(X85)
| p28(X84) ),
file('theBenchmark.p',p28_27) ).
cnf(p14_28,negated_conjecture,
( ~ p14(X26,X27)
| p14(f16(X26),f16(X27)) ),
file('theBenchmark.p',p14_28) ).
cnf(p7_29,negated_conjecture,
( ~ p6(X115,X116)
| p7(f8(X115),f8(X116)) ),
file('theBenchmark.p',p7_29) ).
cnf(p3_30,negated_conjecture,
( ~ p2(X91,X92)
| p3(f4(X91),f4(X92)) ),
file('theBenchmark.p',p3_30) ).
cnf(p2_31,negated_conjecture,
( ~ p2(X66,X67)
| p2(f9(X66),f9(X67)) ),
file('theBenchmark.p',p2_31) ).
cnf(p2_32,negated_conjecture,
( ~ p2(X64,X65)
| p2(f5(X64),f5(X65)) ),
file('theBenchmark.p',p2_32) ).
cnf(p2_33,negated_conjecture,
( ~ p2(X62,X63)
| p2(f24(X62),f24(X63)) ),
file('theBenchmark.p',p2_33) ).
cnf(p2_34,negated_conjecture,
( ~ p2(X56,X57)
| p2(f20(X56),f20(X57)) ),
file('theBenchmark.p',p2_34) ).
cnf(p17_35,negated_conjecture,
( ~ p17(X31,X32)
| p17(f18(X31),f18(X32)) ),
file('theBenchmark.p',p17_35) ).
cnf(p10_36,negated_conjecture,
( ~ p10(X5,X7)
| ~ p10(X5,X6)
| p10(X6,X7) ),
file('theBenchmark.p',p10_36) ).
cnf(p7_37,negated_conjecture,
( ~ p7(X112,X114)
| ~ p7(X112,X113)
| p7(X113,X114) ),
file('theBenchmark.p',p7_37) ).
cnf(p6_38,negated_conjecture,
( ~ p6(X109,X111)
| ~ p6(X109,X110)
| p6(X110,X111) ),
file('theBenchmark.p',p6_38) ).
cnf(p3_39,negated_conjecture,
( ~ p3(X88,X90)
| ~ p3(X88,X89)
| p3(X89,X90) ),
file('theBenchmark.p',p3_39) ).
cnf(p21_40,negated_conjecture,
( ~ p21(X68,X70)
| ~ p21(X68,X69)
| p21(X69,X70) ),
file('theBenchmark.p',p21_40) ).
cnf(p2_41,negated_conjecture,
( ~ p2(X43,X45)
| ~ p2(X43,X44)
| p2(X44,X45) ),
file('theBenchmark.p',p2_41) ).
cnf(p17_42,negated_conjecture,
( ~ p17(X28,X30)
| ~ p17(X28,X29)
| p17(X29,X30) ),
file('theBenchmark.p',p17_42) ).
cnf(p14_43,negated_conjecture,
( ~ p14(X19,X21)
| ~ p14(X19,X20)
| p14(X20,X21) ),
file('theBenchmark.p',p14_43) ).
cnf(p12_44,negated_conjecture,
( ~ p12(X12,X14)
| ~ p12(X12,X13)
| p12(X13,X14) ),
file('theBenchmark.p',p12_44) ).
cnf(p31_45,negated_conjecture,
p31(f11(f4(f5(c42)),c43),f11(f4(c42),c43)),
file('theBenchmark.p',p31_45) ).
cnf(p31_46,negated_conjecture,
( ~ p31(X95,f5(c42))
| ~ p31(X95,c44)
| p31(X95,f24(X95)) ),
file('theBenchmark.p',p31_46) ).
cnf(p31_47,negated_conjecture,
( ~ p31(X95,f5(c42))
| ~ p31(X95,c44)
| p31(f24(X95),f5(c42)) ),
file('theBenchmark.p',p31_47) ).
cnf(p33_48,negated_conjecture,
( ~ p2(X107,X105)
| ~ p33(X107,X108)
| ~ p2(X108,X106)
| p33(X105,X106) ),
file('theBenchmark.p',p33_48) ).
cnf(p27_49,negated_conjecture,
( ~ p12(X82,X81)
| ~ p27(X83,X82)
| ~ p14(X83,X80)
| p27(X80,X81) ),
file('theBenchmark.p',p27_49) ).
cnf(p31_50,negated_conjecture,
( ~ p2(X98,X96)
| ~ p31(X98,X99)
| ~ p2(X99,X97)
| p31(X96,X97) ),
file('theBenchmark.p',p31_50) ).
cnf(p32_51,negated_conjecture,
( ~ p10(X102,X101)
| ~ p32(X103,X102)
| ~ p17(X103,X100)
| p32(X100,X101) ),
file('theBenchmark.p',p32_51) ).
cnf(p2_52,negated_conjecture,
p2(f11(f4(c46),c47),f19(f11(f4(c42),c47),f9(f20(c37)))),
file('theBenchmark.p',p2_52) ).
cnf(p33_53,negated_conjecture,
p33(f11(f4(c42),c43),f11(f4(f23(c42,f9(f20(c37)))),c43)),
file('theBenchmark.p',p33_53) ).
cnf(p2_54,negated_conjecture,
p2(f11(f4(f23(c44,f9(f20(c37)))),c43),f11(f4(c44),c43)),
file('theBenchmark.p',p2_54) ).
cnf(not_p2_55,negated_conjecture,
~ p2(f11(f4(c45),c43),f11(f4(f23(c44,f9(f20(c37)))),c43)),
file('theBenchmark.p',not_p2_55) ).
cnf(not_p2_56,negated_conjecture,
~ p2(f11(f4(f23(c46,f9(f20(c37)))),c47),f11(f4(c46),c47)),
file('theBenchmark.p',not_p2_56) ).
cnf(p10_57,negated_conjecture,
( ~ p31(f11(f4(f5(c42)),X0),f11(f4(c42),X0))
| p10(X0,c43) ),
file('theBenchmark.p',p10_57) ).
cnf(p12_58,negated_conjecture,
( ~ p2(X16,X18)
| ~ p10(X15,X17)
| p12(f13(X15,X16),f13(X17,X18)) ),
file('theBenchmark.p',p12_58) ).
cnf(p2_59,negated_conjecture,
( ~ p2(X59,X61)
| ~ p2(X58,X60)
| p2(f23(X58,X59),f23(X60,X61)) ),
file('theBenchmark.p',p2_59) ).
cnf(p2_60,negated_conjecture,
( ~ p2(X53,X55)
| ~ p2(X52,X54)
| p2(f19(X52,X53),f19(X54,X55)) ),
file('theBenchmark.p',p2_60) ).
cnf(p2_61,negated_conjecture,
( ~ p3(X46,X48)
| ~ p10(X47,X49)
| p2(f11(X46,X47),f11(X48,X49)) ),
file('theBenchmark.p',p2_61) ).
cnf(p17_62,negated_conjecture,
( ~ p21(X33,X35)
| ~ p10(X34,X36)
| p17(f22(X33,X34),f22(X35,X36)) ),
file('theBenchmark.p',p17_62) ).
cnf(p14_63,negated_conjecture,
( ~ p7(X22,X24)
| ~ p12(X23,X25)
| p14(f15(X22,X23),f15(X24,X25)) ),
file('theBenchmark.p',p14_63) ).
cnf(p2_64,negated_conjecture,
p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),f11(f4(c42),c43)),
file('theBenchmark.p',p2_64) ).
cnf(p32_65,negated_conjecture,
( ~ p33(f11(f4(f5(c42)),X104),f11(f4(c42),X104))
| p32(f22(c34,X104),c43) ),
file('theBenchmark.p',p32_65) ).
cnf(p2_66,negated_conjecture,
( ~ p31(c46,X51)
| ~ p31(X51,c42)
| p2(f11(f4(X51),c47),f11(f4(c46),c47)) ),
file('theBenchmark.p',p2_66) ).
cnf(p2_67,negated_conjecture,
( ~ p31(X50,f5(c42))
| ~ p31(c44,X50)
| p2(f11(f4(X50),c43),f11(f4(c44),c43)) ),
file('theBenchmark.p',p2_67) ).
cnf(p10_68,negated_conjecture,
( ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4))
| p32(f22(c34,X1),X2)
| p10(X1,X2) ),
file('theBenchmark.p',p10_68) ).
cnf(not_p31_69,negated_conjecture,
( ~ p2(f11(f4(f24(X95)),c43),f11(f4(X95),c43))
| ~ p31(X95,f5(c42))
| ~ p31(X95,c44) ),
file('theBenchmark.p',not_p31_69) ).
cnf(p26_70,negated_conjecture,
( ~ p26(X76,X77,X78)
| ~ p21(X76,X73)
| ~ p3(X77,X74)
| ~ p3(X78,X75)
| p26(X73,X74,X75) ),
file('theBenchmark.p',p26_70) ).
cnf(p10_71,negated_conjecture,
( ~ p27(f15(c36,f13(X8,X10)),f13(X9,X11))
| ~ p2(f11(f4(X10),X8),f9(c37))
| p10(X8,X9) ),
file('theBenchmark.p',p10_71) ).
cnf(p2_72,negated_conjecture,
( ~ p27(f15(c36,f13(X42,X38)),f13(X40,X41))
| ~ p27(f15(c36,f13(X39,X37)),f13(X40,X41))
| p2(X37,X38) ),
file('theBenchmark.p',p2_72) ).
cnf(p32_73,negated_conjecture,
( ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4))
| p31(f11(f4(X3),X2),f11(f4(X4),X2))
| p32(f22(c34,X1),X2) ),
file('theBenchmark.p',p32_73) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN697-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.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 07:07:23 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.40/0.68 % SZS status Unsatisfiable for theBenchmark
% 0.40/0.68 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------