%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYN619-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 : n005.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:43 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.38s
% Output : Proof 0.12s
% 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(X51,X51),
file('theBenchmark.p',p8_2) ).
cnf(p5_3,negated_conjecture,
p5(X46,X46),
file('theBenchmark.p',p5_3) ).
cnf(p4_4,negated_conjecture,
p4(X39,X39),
file('theBenchmark.p',p4_4) ).
cnf(p2_5,negated_conjecture,
p2(X18,X18),
file('theBenchmark.p',p2_5) ).
cnf(p17_6,negated_conjecture,
p17(X9,X9),
file('theBenchmark.p',p17_6) ).
cnf(p18_7,negated_conjecture,
p18(c24,f6(c25)),
file('theBenchmark.p',p18_7) ).
cnf(not_p18_8,negated_conjecture,
~ p18(c24,f6(f7(c22,c23))),
file('theBenchmark.p',not_p18_8) ).
cnf(p17_9,negated_conjecture,
( ~ p17(f3(X10),X11)
| p17(X10,X11) ),
file('theBenchmark.p',p17_9) ).
cnf(p5_10,negated_conjecture,
( ~ p4(X49,X50)
| p5(f6(X49),f6(X50)) ),
file('theBenchmark.p',p5_10) ).
cnf(p10_11,negated_conjecture,
( ~ p4(X3,X4)
| p10(f12(X3),f12(X4)) ),
file('theBenchmark.p',p10_11) ).
cnf(p2_12,negated_conjecture,
( ~ p10(X25,X26)
| p2(f11(X25),f11(X26)) ),
file('theBenchmark.p',p2_12) ).
cnf(p2_13,negated_conjecture,
( ~ p8(X31,X32)
| p2(f14(X31),f14(X32)) ),
file('theBenchmark.p',p2_13) ).
cnf(p2_14,negated_conjecture,
( ~ p8(X33,X34)
| p2(f15(X33),f15(X34)) ),
file('theBenchmark.p',p2_14) ).
cnf(p2_15,negated_conjecture,
( ~ p8(X35,X36)
| p2(f16(X35),f16(X36)) ),
file('theBenchmark.p',p2_15) ).
cnf(p2_16,negated_conjecture,
( ~ p2(X37,X38)
| p2(f3(X37),f3(X38)) ),
file('theBenchmark.p',p2_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(X51,X53)
| ~ p8(X51,X52)
| p8(X52,X53) ),
file('theBenchmark.p',p8_18) ).
cnf(p5_19,negated_conjecture,
( ~ p5(X46,X48)
| ~ p5(X46,X47)
| p5(X47,X48) ),
file('theBenchmark.p',p5_19) ).
cnf(p4_20,negated_conjecture,
( ~ p4(X39,X41)
| ~ p4(X39,X40)
| p4(X40,X41) ),
file('theBenchmark.p',p4_20) ).
cnf(p2_21,negated_conjecture,
( ~ p2(X18,X20)
| ~ p2(X18,X19)
| p2(X19,X20) ),
file('theBenchmark.p',p2_21) ).
cnf(p2_22,negated_conjecture,
( ~ p2(f13(X21,X23),f13(X22,X24))
| p2(X23,X24) ),
file('theBenchmark.p',p2_22) ).
cnf(p2_23,negated_conjecture,
( ~ p2(f13(X21,X23),f13(X22,X24))
| p2(X21,X22) ),
file('theBenchmark.p',p2_23) ).
cnf(p18_24,negated_conjecture,
( ~ p18(X12,f6(c25))
| p2(f14(X12),c20)
| p18(X12,f6(c19)) ),
file('theBenchmark.p',p18_24) ).
cnf(p17_25,negated_conjecture,
( ~ p17(X7,X8)
| ~ p2(X8,X6)
| ~ p2(X7,X5)
| p17(X5,X6) ),
file('theBenchmark.p',p17_25) ).
cnf(p18_26,negated_conjecture,
( ~ p18(X15,X16)
| ~ p8(X15,X13)
| ~ p5(X16,X14)
| p18(X13,X14) ),
file('theBenchmark.p',p18_26) ).
cnf(p18_27,negated_conjecture,
( ~ p18(X12,f6(c25))
| p17(f3(c21),f15(X12))
| p18(X12,f6(c19)) ),
file('theBenchmark.p',p18_27) ).
cnf(p8_28,negated_conjecture,
( ~ p2(X54,X56)
| ~ p2(X55,X57)
| p8(f9(X54,X55),f9(X56,X57)) ),
file('theBenchmark.p',p8_28) ).
cnf(p2_29,negated_conjecture,
( ~ p2(X28,X30)
| ~ p2(X27,X29)
| p2(f13(X27,X28),f13(X29,X30)) ),
file('theBenchmark.p',p2_29) ).
cnf(p2_30,negated_conjecture,
( ~ p2(X23,X24)
| ~ p2(X21,X22)
| p2(f13(X21,X23),f13(X22,X24)) ),
file('theBenchmark.p',p2_30) ).
cnf(p4_31,negated_conjecture,
( ~ p4(X43,X45)
| ~ p2(X42,X44)
| p4(f7(X42,X43),f7(X44,X45)) ),
file('theBenchmark.p',p4_31) ).
cnf(not_p2_32,negated_conjecture,
( ~ p8(c24,f9(f13(X59,X58),X60))
| ~ p17(c21,X58)
| ~ p2(X59,c20) ),
file('theBenchmark.p',not_p2_32) ).
cnf(p18_33,negated_conjecture,
( ~ p18(X12,f6(c25))
| p8(X12,f9(f13(f14(X12),f15(X12)),f16(X12)))
| p18(X12,f6(c19)) ),
file('theBenchmark.p',p18_33) ).
cnf(p18_34,negated_conjecture,
( ~ p18(X17,f6(c19))
| p8(X17,f9(f13(c20,c21),f11(f12(f7(c22,c23)))))
| p18(X17,f6(f7(c22,c23))) ),
file('theBenchmark.p',p18_34) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN619-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/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n005.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 07:06:03 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.38 % SZS status Unsatisfiable for theBenchmark
% 0.12/0.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------