%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN627-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:44 AM UTC 2026
% Result : Unsatisfiable 0.22s 0.54s
% Output : Proof 0.22s
% 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(X70,X70),
file('theBenchmark.p',p8_2) ).
cnf(p6_3,negated_conjecture,
p6(X67,X67),
file('theBenchmark.p',p6_3) ).
cnf(p5_4,negated_conjecture,
p5(X64,X64),
file('theBenchmark.p',p5_4) ).
cnf(p3_5,negated_conjecture,
p3(X40,X40),
file('theBenchmark.p',p3_5) ).
cnf(p2_6,negated_conjecture,
p2(X33,X33),
file('theBenchmark.p',p2_6) ).
cnf(p15_7,negated_conjecture,
p15(c18,c19),
file('theBenchmark.p',p15_7) ).
cnf(not_p3_8,negated_conjecture,
~ p3(c23,c24),
file('theBenchmark.p',not_p3_8) ).
cnf(p3_9,negated_conjecture,
p3(c23,f4(f7(c17,c18),c21)),
file('theBenchmark.p',p3_9) ).
cnf(p16_10,negated_conjecture,
p16(c17,c20,f9(c19,c18),c21,c22),
file('theBenchmark.p',p16_10) ).
cnf(p3_11,negated_conjecture,
( ~ p6(X55,X56)
| p3(f14(X55),f14(X56)) ),
file('theBenchmark.p',p3_11) ).
cnf(p10_12,negated_conjecture,
( ~ p10(X7,X8)
| p10(f12(X7),f12(X8)) ),
file('theBenchmark.p',p10_12) ).
cnf(p3_13,negated_conjecture,
( ~ p6(X53,X54)
| p3(f13(X53),f13(X54)) ),
file('theBenchmark.p',p3_13) ).
cnf(p10_14,negated_conjecture,
( ~ p10(X0,X2)
| ~ p10(X0,X1)
| p10(X1,X2) ),
file('theBenchmark.p',p10_14) ).
cnf(p8_15,negated_conjecture,
( ~ p8(X70,X72)
| ~ p8(X70,X71)
| p8(X71,X72) ),
file('theBenchmark.p',p8_15) ).
cnf(p6_16,negated_conjecture,
( ~ p6(X67,X69)
| ~ p6(X67,X68)
| p6(X68,X69) ),
file('theBenchmark.p',p6_16) ).
cnf(p5_17,negated_conjecture,
( ~ p5(X64,X66)
| ~ p5(X64,X65)
| p5(X65,X66) ),
file('theBenchmark.p',p5_17) ).
cnf(p3_18,negated_conjecture,
( ~ p3(X40,X42)
| ~ p3(X40,X41)
| p3(X41,X42) ),
file('theBenchmark.p',p3_18) ).
cnf(p2_19,negated_conjecture,
( ~ p2(X33,X35)
| ~ p2(X33,X34)
| p2(X34,X35) ),
file('theBenchmark.p',p2_19) ).
cnf(p3_20,negated_conjecture,
( ~ p15(X32,c19)
| p3(c24,f4(f7(c17,X32),f14(X32))) ),
file('theBenchmark.p',p3_20) ).
cnf(p3_21,negated_conjecture,
( ~ p15(X31,c19)
| p3(c23,f4(f7(c17,X31),f13(X31))) ),
file('theBenchmark.p',p3_21) ).
cnf(p16_22,negated_conjecture,
( ~ p15(X31,c19)
| p16(c17,c20,f9(c19,X31),f13(X31),c22) ),
file('theBenchmark.p',p16_22) ).
cnf(p16_23,negated_conjecture,
( ~ p15(X32,c19)
| p16(c17,c20,f9(c19,X32),f14(X32),c25) ),
file('theBenchmark.p',p16_23) ).
cnf(p15_24,negated_conjecture,
( ~ p15(X14,X15)
| ~ p8(X15,X13)
| ~ p6(X14,X12)
| p15(X12,X13) ),
file('theBenchmark.p',p15_24) ).
cnf(p8_25,negated_conjecture,
( ~ p8(X73,X75)
| ~ p6(X74,X76)
| p8(f9(X73,X74),f9(X75,X76)) ),
file('theBenchmark.p',p8_25) ).
cnf(p2_26,negated_conjecture,
( ~ p6(X37,X39)
| ~ p5(X36,X38)
| p2(f7(X36,X37),f7(X38,X39)) ),
file('theBenchmark.p',p2_26) ).
cnf(p3_27,negated_conjecture,
( ~ p3(X58,X60)
| ~ p2(X57,X59)
| p3(f4(X57,X58),f4(X59,X60)) ),
file('theBenchmark.p',p3_27) ).
cnf(p3_28,negated_conjecture,
( ~ p16(c17,c20,X4,X5,c22)
| ~ p16(c17,c20,X4,X6,X3)
| p3(X5,X6) ),
file('theBenchmark.p',p3_28) ).
cnf(p10_29,negated_conjecture,
( ~ p16(c17,c20,X4,X5,c22)
| ~ p16(c17,c20,X4,X6,X3)
| p10(c22,X3) ),
file('theBenchmark.p',p10_29) ).
cnf(p3_30,negated_conjecture,
( ~ p16(c17,c20,X9,X10,f12(c22))
| ~ p16(c17,c20,X9,X11,c25)
| p3(X10,X11) ),
file('theBenchmark.p',p3_30) ).
cnf(p10_31,negated_conjecture,
( ~ p16(c17,c20,X9,X10,f12(c22))
| ~ p16(c17,c20,X9,X11,c25)
| p10(f12(c22),c25) ),
file('theBenchmark.p',p10_31) ).
cnf(p6_32,negated_conjecture,
( p3(f4(f7(c17,X61),f4(f7(c17,X62),X63)),f4(f7(c17,X62),f4(f7(c17,X61),X63)))
| p6(X61,X62) ),
file('theBenchmark.p',p6_32) ).
cnf(p3_33,negated_conjecture,
( ~ p16(c17,X26,X27,X30,f12(X29))
| ~ p15(X28,X27)
| p3(X30,f4(f7(c17,X28),f11(X26,X29,X27,X30,X28))) ),
file('theBenchmark.p',p3_33) ).
cnf(p16_34,negated_conjecture,
( ~ p16(c17,X26,X27,X30,f12(X29))
| ~ p15(X28,X27)
| p16(c17,X26,f9(X27,X28),f11(X26,X29,X27,X30,X28),X29) ),
file('theBenchmark.p',p16_34) ).
cnf(p16_35,negated_conjecture,
( ~ p16(X22,X23,X24,X25,X21)
| ~ p10(X21,X20)
| ~ p3(X23,X17)
| ~ p3(X25,X19)
| ~ p5(X22,X16)
| ~ p8(X24,X18)
| p16(X16,X17,X18,X19,X20) ),
file('theBenchmark.p',p16_35) ).
cnf(p3_36,negated_conjecture,
( ~ p3(X46,X51)
| ~ p3(X43,X48)
| ~ p10(X44,X49)
| ~ p8(X45,X50)
| ~ p6(X47,X52)
| p3(f11(X43,X44,X45,X46,X47),f11(X48,X49,X50,X51,X52)) ),
file('theBenchmark.p',p3_36) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN627-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.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 07:06:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.22/0.54 % SZS status Unsatisfiable for theBenchmark
% 0.22/0.54 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------