%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN673-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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 : Fri Sep 25 03:41:21 PM UTC 2026
% Result : Unsatisfiable 4.51s 1.28s
% Output : CNFRefutation 4.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 19
% Syntax : Number of formulae : 84 ( 28 unt; 0 def)
% Number of atoms : 185 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 200 ( 99 ~; 101 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 17 usr; 8 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 14 con; 0-2 aty)
% Number of variables : 113 ( 0 sgn 113 !; 0 ?; 82 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0] : p10(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_1) ).
fof(f3,negated_conjecture,
! [X0] : p7(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_3) ).
fof(f4,negated_conjecture,
! [X0] : p6(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p6_4) ).
fof(f10,negated_conjecture,
! [X0] : p2(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_10) ).
fof(f12,negated_conjecture,
! [X0] : p16(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16_12) ).
fof(f16,negated_conjecture,
! [X0] : p10(f14(f19(c35,X0),c41),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_16) ).
fof(f17,negated_conjecture,
~ p29(f5(c33,f8(c34,c30)),c38),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p29_17) ).
fof(f18,negated_conjecture,
! [X0,X1] :
( ~ p27(f12(c32,X1),X0)
| p29(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p29_18) ).
fof(f19,negated_conjecture,
! [X0,X1] :
( ~ p29(X1,X0)
| p27(f12(c32,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p27_19) ).
fof(f20,negated_conjecture,
! [X0] :
( ~ p16(X0,c40)
| p28(f21(c30,X0),c31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p28_20) ).
fof(f22,negated_conjecture,
! [X2,X0,X1] :
( ~ p10(X2,X1)
| ~ p10(X2,X0)
| p10(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_22) ).
fof(f37,negated_conjecture,
! [X0] :
( ~ p29(f24(c42,X0),c39)
| p28(f21(c30,X0),c31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p28_37) ).
fof(f38,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p10(X3,X1)
| ~ p4(X2,X0)
| ~ p29(X2,X3)
| p29(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p29_38) ).
fof(f41,negated_conjecture,
p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_41) ).
fof(f42,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p3(X1,X3)
| ~ p2(X0,X2)
| p4(f5(X0,X1),f5(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_42) ).
fof(f49,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p7(X1,X3)
| ~ p6(X0,X2)
| p3(f8(X0,X1),f8(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_49) ).
fof(f52,negated_conjecture,
! [X0] :
( ~ p10(X0,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),X0)
| p29(f24(c42,f26(c43,X0)),c39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p29_52) ).
fof(f53,negated_conjecture,
! [X0] :
( ~ p28(f21(c30,f26(c43,X0)),c31)
| ~ p10(X0,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p29_53) ).
fof(f55,negated_conjecture,
! [X0,X1] :
( ~ p27(f12(c32,X0),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,X1),c31)
| p27(f12(c32,f14(f19(c35,X0),f17(c36,X1))),f5(c33,f8(c34,c30))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p27_55) ).
tcf(c_104,negated_conjecture,
! [X0: $i] : p10(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_106,negated_conjecture,
! [X0: $i] : p7(X0,X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_107,negated_conjecture,
! [X0: $i] : p6(X0,X0),
inference(cnf_transformation,[],[f4]) ).
tcf(c_113,negated_conjecture,
! [X0: $i] : p2(X0,X0),
inference(cnf_transformation,[],[f10]) ).
tcf(c_115,negated_conjecture,
! [X0: $i] : p16(X0,X0),
inference(cnf_transformation,[],[f12]) ).
tcf(c_119,negated_conjecture,
! [X0: $i] : p10(f14(f19(c35,X0),c41),X0),
inference(cnf_transformation,[],[f16]) ).
tcf(c_120,negated_conjecture,
~ p29(f5(c33,f8(c34,c30)),c38),
inference(cnf_transformation,[],[f17]) ).
tcf(c_121,negated_conjecture,
! [X0: $i,X1: $i] :
( p29(X1,X0)
| ~ p27(f12(c32,X0),X1) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_122,negated_conjecture,
! [X0: $i,X1: $i] :
( p27(f12(c32,X1),X0)
| ~ p29(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_123,negated_conjecture,
! [X0: $i] :
( p28(f21(c30,X0),c31)
| ~ p16(X0,c40) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_125,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p10(X1,X2)
| ~ p10(X0,X2)
| ~ p10(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_140,negated_conjecture,
! [X0: $i] :
( p28(f21(c30,X0),c31)
| ~ p29(f24(c42,X0),c39) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_141,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p29(X3,X1)
| ~ p29(X2,X0)
| ~ p4(X2,X3)
| ~ p10(X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_144,negated_conjecture,
p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),
inference(cnf_transformation,[],[f41]) ).
tcf(c_145,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p4(f5(X2,X0),f5(X3,X1))
| ~ p2(X2,X3)
| ~ p3(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_152,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p3(f8(X2,X0),f8(X3,X1))
| ~ p6(X2,X3)
| ~ p7(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_155,negated_conjecture,
! [X0: $i] :
( p29(f5(c33,f8(c34,c30)),X0)
| p29(f24(c42,f26(c43,X0)),c39)
| ~ p10(X0,f14(f19(c35,c37),c39)) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_156,negated_conjecture,
! [X0: $i] :
( p29(f5(c33,f8(c34,c30)),X0)
| ~ p28(f21(c30,f26(c43,X0)),c31)
| ~ p10(X0,f14(f19(c35,c37),c39)) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_158,negated_conjecture,
! [X0: $i,X1: $i] :
( p27(f12(c32,f14(f19(c35,X0),f17(c36,X1))),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,X1),c31)
| ~ p27(f12(c32,X0),f5(c33,f8(c34,c30))) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_171,plain,
p7(c30,c30),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_443,negated_conjecture,
! [X0_iProver_f12_2: iProver_f12_2,X0_iProver_f17_2: iProver_f17_2] :
( p27(f12(c32,f14(f19(c35,X0_iProver_f12_2),f17(c36,X0_iProver_f17_2))),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,X0_iProver_f17_2),c31)
| ~ p27(f12(c32,X0_iProver_f12_2),f5(c33,f8(c34,c30))) ),
inference(subtyping,[status(esa)],[c_158]) ).
tcf(c_445,negated_conjecture,
! [X0_iProver_f12_2: iProver_f12_2] :
( p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| ~ p28(f21(c30,f26(c43,X0_iProver_f12_2)),c31)
| ~ p10(X0_iProver_f12_2,f14(f19(c35,c37),c39)) ),
inference(subtyping,[status(esa)],[c_156]) ).
tcf(c_446,negated_conjecture,
! [X0_iProver_f12_2: iProver_f12_2] :
( p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| p29(f24(c42,f26(c43,X0_iProver_f12_2)),c39)
| ~ p10(X0_iProver_f12_2,f14(f19(c35,c37),c39)) ),
inference(subtyping,[status(esa)],[c_155]) ).
tcf(c_449,negated_conjecture,
! [X0_iProver_f8_1: iProver_f8_1,X0_iProver_f8_2: iProver_f8_2,X1_iProver_f8_1: iProver_f8_1,X1_iProver_f8_2: iProver_f8_2] :
( p3(f8(X0_iProver_f8_1,X0_iProver_f8_2),f8(X1_iProver_f8_1,X1_iProver_f8_2))
| ~ p6(X0_iProver_f8_1,X1_iProver_f8_1)
| ~ p7(X0_iProver_f8_2,X1_iProver_f8_2) ),
inference(subtyping,[status(esa)],[c_152]) ).
tcf(c_456,negated_conjecture,
! [X0_iProver_f5_1: iProver_f5_1,X0_iProver_f5_2: iProver_f5_2,X1_iProver_f5_1: iProver_f5_1,X1_iProver_f5_2: iProver_f5_2] :
( p4(f5(X0_iProver_f5_1,X0_iProver_f5_2),f5(X1_iProver_f5_1,X1_iProver_f5_2))
| ~ p2(X0_iProver_f5_1,X1_iProver_f5_1)
| ~ p3(X0_iProver_f5_2,X1_iProver_f5_2) ),
inference(subtyping,[status(esa)],[c_145]) ).
tcf(c_460,negated_conjecture,
! [X0_iProver_p29_1: iProver_p29_1,X0_iProver_f12_2: iProver_f12_2,X1_iProver_p29_1: iProver_p29_1,X1_iProver_f12_2: iProver_f12_2] :
( p29(X1_iProver_p29_1,X1_iProver_f12_2)
| ~ p29(X0_iProver_p29_1,X0_iProver_f12_2)
| ~ p4(X0_iProver_p29_1,X1_iProver_p29_1)
| ~ p10(X0_iProver_f12_2,X1_iProver_f12_2) ),
inference(subtyping,[status(esa)],[c_141]) ).
tcf(c_461,negated_conjecture,
! [X0_iProver_f17_2: iProver_f17_2] :
( p28(f21(c30,X0_iProver_f17_2),c31)
| ~ p29(f24(c42,X0_iProver_f17_2),c39) ),
inference(subtyping,[status(esa)],[c_140]) ).
tcf(c_476,negated_conjecture,
! [X0_iProver_f12_2: iProver_f12_2,X1_iProver_f12_2: iProver_f12_2,X2_iProver_f12_2: iProver_f12_2] :
( p10(X1_iProver_f12_2,X2_iProver_f12_2)
| ~ p10(X0_iProver_f12_2,X2_iProver_f12_2)
| ~ p10(X0_iProver_f12_2,X1_iProver_f12_2) ),
inference(subtyping,[status(esa)],[c_125]) ).
tcf(c_478,negated_conjecture,
! [X0_iProver_f17_2: iProver_f17_2] :
( p28(f21(c30,X0_iProver_f17_2),c31)
| ~ p16(X0_iProver_f17_2,c40) ),
inference(subtyping,[status(esa)],[c_123]) ).
tcf(c_479,negated_conjecture,
! [X0_iProver_p29_1: iProver_p29_1,X0_iProver_f12_2: iProver_f12_2] :
( p27(f12(c32,X0_iProver_f12_2),X0_iProver_p29_1)
| ~ p29(X0_iProver_p29_1,X0_iProver_f12_2) ),
inference(subtyping,[status(esa)],[c_122]) ).
tcf(c_480,negated_conjecture,
! [X0_iProver_p29_1: iProver_p29_1,X0_iProver_f12_2: iProver_f12_2] :
( p29(X0_iProver_p29_1,X0_iProver_f12_2)
| ~ p27(f12(c32,X0_iProver_f12_2),X0_iProver_p29_1) ),
inference(subtyping,[status(esa)],[c_121]) ).
tcf(c_482,negated_conjecture,
! [X0_iProver_f12_2: iProver_f12_2] : p10(f14(f19(c35,X0_iProver_f12_2),c41),X0_iProver_f12_2),
inference(subtyping,[status(esa)],[c_119]) ).
tcf(c_486,negated_conjecture,
! [X0_iProver_f17_2: iProver_f17_2] : p16(X0_iProver_f17_2,X0_iProver_f17_2),
inference(subtyping,[status(esa)],[c_115]) ).
tcf(c_488,negated_conjecture,
! [X0_iProver_f5_1: iProver_f5_1] : p2(X0_iProver_f5_1,X0_iProver_f5_1),
inference(subtyping,[status(esa)],[c_113]) ).
tcf(c_494,negated_conjecture,
! [X0_iProver_f8_1: iProver_f8_1] : p6(X0_iProver_f8_1,X0_iProver_f8_1),
inference(subtyping,[status(esa)],[c_107]) ).
tcf(c_497,negated_conjecture,
! [X0_iProver_f12_2: iProver_f12_2] : p10(X0_iProver_f12_2,X0_iProver_f12_2),
inference(subtyping,[status(esa)],[c_104]) ).
tcf(c_503,plain,
p2(c33,c33),
inference(instantiation,[status(thm)],[c_488]) ).
tcf(c_509,plain,
p6(c34,c34),
inference(instantiation,[status(thm)],[c_494]) ).
tcf(c_519,plain,
( p3(f8(c34,c30),f8(c34,c30))
| ~ p6(c34,c34)
| ~ p7(c30,c30) ),
inference(instantiation,[status(thm)],[c_449]) ).
tcf(c_536,plain,
p16(c40,c40),
inference(instantiation,[status(thm)],[c_486]) ).
tcf(c_537,plain,
p10(f14(f19(c35,c37),c39),f14(f19(c35,c37),c39)),
inference(instantiation,[status(thm)],[c_497]) ).
tcf(c_567,plain,
( p28(f21(c30,c40),c31)
| ~ p16(c40,c40) ),
inference(instantiation,[status(thm)],[c_478]) ).
tcf(c_608,plain,
( p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31)
| ~ p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39) ),
inference(instantiation,[status(thm)],[c_461]) ).
tcf(c_626,plain,
! [X0_iProver_f5_1: iProver_f5_1,X0_iProver_f5_2: iProver_f5_2] :
( p4(f5(c33,f8(c34,c30)),f5(X0_iProver_f5_1,X0_iProver_f5_2))
| ~ p2(c33,X0_iProver_f5_1)
| ~ p3(f8(c34,c30),X0_iProver_f5_2) ),
inference(instantiation,[status(thm)],[c_456]) ).
tcf(c_654,plain,
( p27(f12(c32,f14(f19(c35,c37),c39)),f5(c33,f8(c34,c30)))
| ~ p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39)) ),
inference(instantiation,[status(thm)],[c_479]) ).
tcf(c_691,plain,
( p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
| ~ p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31)
| ~ p10(f14(f19(c35,c37),c39),f14(f19(c35,c37),c39)) ),
inference(instantiation,[status(thm)],[c_445]) ).
tcf(c_723,plain,
! [X0_iProver_f5_1: iProver_f5_1,X0_iProver_f8_1: iProver_f8_1,X0_iProver_f8_2: iProver_f8_2] :
( p4(f5(c33,f8(c34,c30)),f5(X0_iProver_f5_1,f8(X0_iProver_f8_1,X0_iProver_f8_2)))
| ~ p2(c33,X0_iProver_f5_1)
| ~ p3(f8(c34,c30),f8(X0_iProver_f8_1,X0_iProver_f8_2)) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_724,plain,
( p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30)))
| ~ p2(c33,c33)
| ~ p3(f8(c34,c30),f8(c34,c30)) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_1261,plain,
( p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
| p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39) ),
inference(superposition,[status(thm)],[c_497,c_446]) ).
tcf(c_1413,plain,
! [X0_iProver_p29_1: iProver_p29_1,X0_iProver_f12_2: iProver_f12_2,X1_iProver_f12_2: iProver_f12_2] :
( p29(X0_iProver_p29_1,X1_iProver_f12_2)
| ~ p10(X0_iProver_f12_2,X1_iProver_f12_2)
| ~ p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| ~ p4(f5(c33,f8(c34,c30)),X0_iProver_p29_1) ),
inference(instantiation,[status(thm)],[c_460]) ).
tcf(c_1421,plain,
! [X0_iProver_f12_2: iProver_f12_2] :
( p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| ~ p27(f12(c32,X0_iProver_f12_2),f5(c33,f8(c34,c30))) ),
inference(instantiation,[status(thm)],[c_480]) ).
tcf(c_1422,plain,
! [X0_iProver_f12_2: iProver_f12_2,X0_iProver_f5_1: iProver_f5_1,X0_iProver_f5_2: iProver_f5_2,X1_iProver_f12_2: iProver_f12_2] :
( p29(f5(X0_iProver_f5_1,X0_iProver_f5_2),X1_iProver_f12_2)
| ~ p10(X0_iProver_f12_2,X1_iProver_f12_2)
| ~ p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| ~ p4(f5(c33,f8(c34,c30)),f5(X0_iProver_f5_1,X0_iProver_f5_2)) ),
inference(instantiation,[status(thm)],[c_1413]) ).
tcf(c_1446,plain,
! [X0_iProver_f12_2: iProver_f12_2,X1_iProver_f12_2: iProver_f12_2] :
( p29(f5(c33,f8(c34,c30)),X1_iProver_f12_2)
| ~ p10(X0_iProver_f12_2,X1_iProver_f12_2)
| ~ p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| ~ p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))) ),
inference(instantiation,[status(thm)],[c_1422]) ).
tcf(c_1461,plain,
! [X0_iProver_f12_2: iProver_f12_2] :
( p27(f12(c32,f14(f19(c35,X0_iProver_f12_2),f17(c36,c40))),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,c40),c31)
| ~ p27(f12(c32,X0_iProver_f12_2),f5(c33,f8(c34,c30))) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_1469,plain,
! [X0_iProver_f12_2: iProver_f12_2] :
( p29(f5(c33,f8(c34,c30)),c38)
| ~ p10(X0_iProver_f12_2,c38)
| ~ p29(f5(c33,f8(c34,c30)),X0_iProver_f12_2)
| ~ p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30))) ),
inference(instantiation,[status(thm)],[c_1446]) ).
tcf(c_1487,plain,
! [X0_iProver_f12_2: iProver_f12_2,X1_iProver_f12_2: iProver_f12_2] :
( p10(X1_iProver_f12_2,c38)
| ~ p10(X0_iProver_f12_2,c38)
| ~ p10(X0_iProver_f12_2,X1_iProver_f12_2) ),
inference(instantiation,[status(thm)],[c_476]) ).
tcf(c_1549,plain,
! [X0_iProver_f12_2: iProver_f12_2] :
( p10(X0_iProver_f12_2,c38)
| ~ p10(f14(f19(c35,c38),c41),c38)
| ~ p10(f14(f19(c35,c38),c41),X0_iProver_f12_2) ),
inference(instantiation,[status(thm)],[c_1487]) ).
tcf(c_1550,plain,
! [X0_iProver_f12_2: iProver_f12_2] :
( p10(X0_iProver_f12_2,c38)
| ~ p10(c38,c38)
| ~ p10(c38,X0_iProver_f12_2) ),
inference(instantiation,[status(thm)],[c_1487]) ).
tcf(c_1552,plain,
p10(f14(f19(c35,c38),c41),c38),
inference(instantiation,[status(thm)],[c_482]) ).
tcf(c_1658,plain,
( p10(c38,c38)
| ~ p10(f14(f19(c35,c38),c41),c38) ),
inference(instantiation,[status(thm)],[c_1549]) ).
tcf(c_1837,plain,
( p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),c38)
| ~ p10(c38,c38)
| ~ p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))) ),
inference(instantiation,[status(thm)],[c_1550]) ).
tcf(c_2073,plain,
( p29(f5(c33,f8(c34,c30)),c38)
| ~ p4(f5(c33,f8(c34,c30)),f5(c33,f8(c34,c30)))
| ~ p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),c38)
| ~ p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))) ),
inference(instantiation,[status(thm)],[c_1469]) ).
tcf(c_2412,plain,
( p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)))
| ~ p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f5(c33,f8(c34,c30))) ),
inference(instantiation,[status(thm)],[c_1421]) ).
tcf(c_3135,plain,
( p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,c40),c31)
| ~ p27(f12(c32,f14(f19(c35,c37),c39)),f5(c33,f8(c34,c30))) ),
inference(instantiation,[status(thm)],[c_1461]) ).
tcf(c_3136,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_3135,c_2412,c_2073,c_1837,c_1658,c_1552,c_1261,c_724,c_691,c_654,c_608,c_567,c_537,c_536,c_519,c_509,c_503,c_144,c_120,c_171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN673-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 02:05:04 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 4.51/1.28 % SZS status Started for theBenchmark.p
% 4.51/1.28 % SZS status Unsatisfiable for theBenchmark.p
% 4.51/1.28
% 4.51/1.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.51/1.28
% 4.51/1.28 % ------ iProver source info
% 4.51/1.28
% 4.51/1.28 % git: date: 2026-07-19 20:42:38 +0200
% 4.51/1.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.51/1.28 % git: non_committed_changes: false
% 4.51/1.28
% 4.51/1.28 % ------ Parsing...% successful
% 4.51/1.28
% 4.51/1.28
% 4.51/1.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.51/1.28
% 4.51/1.28 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 4.51/1.28
% 4.51/1.28 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 4.51/1.28 % ------ Proving...
% 4.51/1.28 % ------ Problem Properties
% 4.51/1.28
% 4.51/1.28 %
% 4.51/1.28 % clauses 55
% 4.51/1.28 % conjectures 55
% 4.51/1.28 % EPR 33
% 4.51/1.28 % Horn 54
% 4.51/1.28 % unary 19
% 4.51/1.28 % binary 5
% 4.51/1.28 % lits 125
% 4.51/1.28 % lits eq 0
% 4.51/1.28 % fd_pure 0
% 4.51/1.28 % fd_pseudo 0
% 4.51/1.28 % fd_cond 0
% 4.51/1.28 % fd_pseudo_cond 0
% 4.51/1.28 % AC symbols 0
% 4.51/1.28
% 4.51/1.28 % ------ Input Options Time Limit: Unbounded
% 4.51/1.28
% 4.51/1.28
% 4.51/1.28 % ------
% 4.51/1.28 % Current options:
% 4.51/1.28 % ------
% 4.51/1.28
% 4.51/1.28
% 4.51/1.28 %
% 4.51/1.28
% 4.51/1.28 % ------ Proving...
% 4.51/1.28 %
% 4.51/1.28
% 4.51/1.28 % SZS status Unsatisfiable for theBenchmark.p
% 4.51/1.28
% 4.51/1.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.51/1.28
% 4.51/1.28
%------------------------------------------------------------------------------