%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO596+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/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 01:21:35 PM UTC 2026
% Result : Theorem 10.35s 2.79s
% Output : CNFRefutation 10.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 18
% Syntax : Number of formulae : 145 ( 27 unt; 0 def)
% Number of atoms : 356 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 366 ( 155 ~; 154 |; 38 &)
% ( 0 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 8 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-8 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 722 ( 0 sgn 706 !; 16 ?; 338 :)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD4) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD5) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD8) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& perp(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(f15,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD15) ).
fof(f17,axiom,
! [X0,X1,X2,X3,X4] :
( ( cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cyclic(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD17) ).
fof(f19,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD19) ).
fof(f20,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD20) ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD21) ).
fof(f22,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD22) ).
fof(f39,axiom,
! [X0,X1,X2,X3,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD39) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f42,axiom,
! [X0,X1,X2,X3] :
( ( ~ coll(X2,X3,X0)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD42a) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( coll(X2,X3,X1)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
& cyclic(X0,X1,X2,X5)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f57,axiom,
! [X0,X1,X2,X3] :
( ( cong(X0,X3,X1,X3)
& cong(X0,X2,X1,X2) )
=> perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD56) ).
fof(f74,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( para(X4,X5,X6,X7)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD73) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( coll(X6,X1,X2)
& para(X0,X4,X6,X5)
& coll(X5,X2,X4)
& coll(X5,X0,X1)
& circle(X3,X0,X4,X7)
& circle(X3,X0,X1,X2) )
=> eqangle(X6,X5,X5,X1,X5,X2,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL416058) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( coll(X6,X1,X2)
& para(X0,X4,X6,X5)
& coll(X5,X2,X4)
& coll(X5,X0,X1)
& circle(X3,X0,X4,X7)
& circle(X3,X0,X1,X2) )
=> eqangle(X6,X5,X5,X1,X5,X2,X2,X1) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( coll(X6,X1,X2)
& para(X0,X4,X6,X5)
& coll(X5,X2,X4)
& coll(X5,X0,X1)
& circle(X3,X0,X4,X7)
& circle(X3,X0,X1,X2)
& ~ eqangle(X6,X5,X5,X1,X5,X2,X2,X1) ),
inference(ennf_transformation,[],[f96]) ).
fof(f99,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( coll(X6,X1,X2)
& para(X0,X4,X6,X5)
& coll(X5,X2,X4)
& coll(X5,X0,X1)
& circle(X3,X0,X4,X7)
& circle(X3,X0,X1,X2)
& ~ eqangle(X6,X5,X5,X1,X5,X2,X2,X1) ),
inference(flattening,[],[f98]) ).
fof(f136,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f74]) ).
fof(f137,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(flattening,[],[f136]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f40]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f39]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f9]) ).
fof(f153,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f152]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f157,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f178,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
inference(ennf_transformation,[],[f22]) ).
fof(f179,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
inference(flattening,[],[f178]) ).
fof(f180,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(ennf_transformation,[],[f21]) ).
fof(f181,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f20]) ).
fof(f182,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(ennf_transformation,[],[f19]) ).
fof(f186,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f57]) ).
fof(f187,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f186]) ).
fof(f192,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f206,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f207,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(flattening,[],[f206]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f209,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f208]) ).
fof(f210,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f42]) ).
fof(f211,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f210]) ).
fof(f213,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f17]) ).
fof(f214,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(flattening,[],[f213]) ).
fof(f216,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f220,plain,
( coll(sK6,sK1,sK2)
& para(sK0,sK4,sK6,sK5)
& coll(sK5,sK2,sK4)
& coll(sK5,sK0,sK1)
& circle(sK3,sK0,sK4,sK7)
& circle(sK3,sK0,sK1,sK2)
& ~ eqangle(sK6,sK5,sK5,sK1,sK5,sK2,sK2,sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7)],[f99]) ).
fof(f240,plain,
para(sK0,sK4,sK6,sK5),
inference(cnf_transformation,[],[f220]) ).
fof(f245,plain,
~ eqangle(sK6,sK5,sK5,sK1,sK5,sK2,sK2,sK1),
inference(cnf_transformation,[],[f220]) ).
fof(f281,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f137]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f148]) ).
fof(f288,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f149]) ).
fof(f290,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f153]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f156]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f157]) ).
fof(f305,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
inference(cnf_transformation,[],[f179]) ).
fof(f306,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(cnf_transformation,[],[f180]) ).
fof(f307,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f181]) ).
fof(f308,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(cnf_transformation,[],[f182]) ).
fof(f311,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f187]) ).
fof(f314,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f192]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f207]) ).
fof(f326,plain,
! [X2,X3,X0,X1] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f209]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( coll(X2,X3,X0)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f211]) ).
fof(f329,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f214]) ).
fof(f331,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_49,negated_conjecture,
~ eqangle(sK6,sK5,sK5,sK1,sK5,sK2,sK2,sK1),
inference(cnf_transformation,[],[f245]) ).
tcf(c_54,negated_conjecture,
para(sK0,sK4,sK6,sK5),
inference(cnf_transformation,[],[f240]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( para(X0,X1,X2,X3)
| ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X2,X3) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
( eqangle(X8,X9,X10,X11,X4,X5,X6,X7)
| ~ eqangle(X8,X9,X10,X11,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X4,X5,X6,X7,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X2,X3,X0,X1,X6,X7,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X2,X1,X3)
| ~ cong(X0,X3,X2,X3)
| ~ cong(X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X1,X2,X4,X5)
| ~ cyclic(X1,X2,X0,X5)
| ~ cyclic(X1,X2,X0,X4)
| ~ cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X4,X3,X5) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X0,X3)
| ~ coll(X0,X3,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X0,X3,X1)
| cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X4,X3)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_3021,plain,
para(sK6,sK5,sK0,sK4),
inference(superposition,[status(thm)],[c_54,c_102]) ).
tcf(c_3026,plain,
para(sK6,sK5,sK0,sK4),
inference(superposition,[status(thm)],[c_54,c_102]) ).
tcf(c_3046,plain,
para(sK0,sK4,sK5,sK6),
inference(superposition,[status(thm)],[c_54,c_103]) ).
tcf(c_3070,plain,
para(sK6,sK5,sK4,sK0),
inference(superposition,[status(thm)],[c_3026,c_103]) ).
tcf(c_3089,plain,
para(sK5,sK6,sK0,sK4),
inference(superposition,[status(thm)],[c_3046,c_102]) ).
tcf(c_4013,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] :
( eqangle(X0,X1,X2,X3,X8,X9,X6,X7)
| ~ para(X4,X5,X8,X9)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(superposition,[status(thm)],[c_97,c_115]) ).
tcf(c_4021,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] :
( eqangle(X0,X1,X2,X3,X8,X9,X6,X7)
| ~ para(X4,X5,X8,X9)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(superposition,[status(thm)],[c_97,c_115]) ).
tcf(c_4343,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X6,X7,X4,X5,X6,X7)
| ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_97,c_4013]) ).
tcf(c_4357,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X6,X7,X4,X5,X6,X7)
| ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_97,c_4021]) ).
tcf(c_5102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK6,sK5,X2,X3)
| ~ para(X0,X1,sK0,sK4) ),
inference(superposition,[status(thm)],[c_54,c_4343]) ).
tcf(c_5103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK0,sK4,X2,X3)
| ~ para(X0,X1,sK6,sK5) ),
inference(superposition,[status(thm)],[c_3021,c_4343]) ).
tcf(c_5140,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK6,sK5,X2,X3)
| ~ para(X0,X1,sK0,sK4) ),
inference(superposition,[status(thm)],[c_54,c_4357]) ).
tcf(c_5143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK4,sK0,X2,X3)
| ~ para(X0,X1,sK6,sK5) ),
inference(superposition,[status(thm)],[c_3070,c_4357]) ).
tcf(c_5144,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK0,sK4,X2,X3)
| ~ para(X0,X1,sK5,sK6) ),
inference(superposition,[status(thm)],[c_3089,c_4357]) ).
tcf(c_7315,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(sK4,sK0,X2,X3)
| ~ para(X0,X1,sK6,sK5) ),
inference(superposition,[status(thm)],[c_5143,c_4021]) ).
tcf(c_8024,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK6,sK5,X2,X3,X2,X3)
| ~ para(X0,X1,sK0,sK4) ),
inference(superposition,[status(thm)],[c_5102,c_116]) ).
tcf(c_8051,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK6,sK5,X2,X3,X2,X3)
| ~ para(X0,X1,sK0,sK4) ),
inference(superposition,[status(thm)],[c_5140,c_116]) ).
tcf(c_8687,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X4,X5,sK6,sK5,X2,X3,X0,X1)
| ~ para(X4,X5,sK0,sK4)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_8051,c_4021]) ).
tcf(c_8911,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK0,sK4,X6,X7)
| ~ para(X4,X5,sK5,sK6)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(superposition,[status(thm)],[c_5144,c_115]) ).
tcf(c_8933,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK0,sK4,X2,X3,X0,X1,X2,X3)
| ~ para(X0,X1,sK6,sK5) ),
inference(superposition,[status(thm)],[c_5103,c_117]) ).
tcf(c_8968,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK6,sK5,X2,X3,X0,X1,X2,X3)
| ~ para(X0,X1,sK0,sK4) ),
inference(superposition,[status(thm)],[c_5140,c_117]) ).
tcf(c_8969,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK0,sK4,X2,X3,X0,X1,X2,X3)
| ~ para(X0,X1,sK5,sK6) ),
inference(superposition,[status(thm)],[c_5144,c_117]) ).
tcf(c_9163,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X4,X5,X0,X1,X4,X5,X2,X3)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_97,c_118]) ).
tcf(c_9198,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X4,X5,X0,X1,X4,X5,X2,X3)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_97,c_118]) ).
tcf(c_9462,plain,
! [X0: $i] :
( coll(sK6,X0,sK5)
| cyclic(sK5,sK5,sK6,X0)
| ~ para(sK6,sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_8024,c_137]) ).
tcf(c_9463,plain,
! [X0: $i] :
( coll(sK6,X0,sK5)
| cyclic(sK5,sK5,sK6,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9462,c_3021]) ).
tcf(c_10198,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,X6,X7,X4,X5)
| ~ para(X6,X7,sK0,sK4)
| ~ eqangle(X0,X1,X2,X3,sK6,sK5,X4,X5) ),
inference(superposition,[status(thm)],[c_8968,c_115]) ).
tcf(c_13990,plain,
! [X0: $i] :
( cyclic(sK5,sK5,sK6,X0)
| ~ coll(sK6,X0,sK5)
| ~ para(sK6,sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_8024,c_136]) ).
tcf(c_14000,plain,
! [X0: $i] :
( cyclic(sK5,sK5,sK6,X0)
| ~ coll(sK6,X0,sK5) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13990,c_3021]) ).
tcf(c_14047,plain,
! [X0: $i] :
( cyclic(sK5,sK5,sK6,X0)
| ~ coll(sK6,X0,sK5)
| ~ para(sK6,sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_8051,c_136]) ).
tcf(c_14057,plain,
! [X0: $i] :
( cyclic(sK5,sK5,sK6,X0)
| ~ coll(sK6,X0,sK5) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14047,c_3026]) ).
tcf(c_14397,plain,
! [X0: $i] : cyclic(sK5,sK5,sK6,X0),
inference(global_subsumption_just,[status(thm)],[c_14000,c_9463,c_14000]) ).
tcf(c_14407,plain,
! [X0: $i] : cyclic(sK5,sK5,sK6,X0),
inference(global_subsumption_just,[status(thm)],[c_14057,c_14397]) ).
tcf(c_14409,plain,
! [X0: $i,X1: $i] :
( cyclic(sK5,sK6,X0,X1)
| ~ cyclic(sK5,sK5,sK6,X0) ),
inference(superposition,[status(thm)],[c_14407,c_139]) ).
tcf(c_14413,plain,
! [X0: $i,X1: $i] : cyclic(sK5,sK6,X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_14409,c_14407]) ).
tcf(c_16204,plain,
! [X0: $i,X1: $i] : cyclic(sK5,X0,sK6,X1),
inference(superposition,[status(thm)],[c_14413,c_141]) ).
tcf(c_16992,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,sK6,sK5)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK6,sK5,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_32909,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X2,X3,X4,X5,X0,X1,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_97,c_117]) ).
tcf(c_34145,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X2,X3,X4,X5)
| ~ para(X0,X1,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_32909,c_91]) ).
tcf(c_40717,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK5,X1)
| ~ para(sK6,X0,sK0,sK4)
| ~ cyclic(X0,X1,sK6,sK5)
| ~ cyclic(X0,X1,sK6,sK6)
| ~ cyclic(X0,X1,sK6,X1) ),
inference(superposition,[status(thm)],[c_5140,c_135]) ).
tcf(c_44246,plain,
! [X0: $i] :
( cong(sK5,X0,sK5,X0)
| ~ para(sK6,sK5,sK0,sK4)
| ~ cyclic(sK5,X0,sK6,sK5)
| ~ cyclic(sK5,X0,sK6,X0) ),
inference(superposition,[status(thm)],[c_16204,c_40717]) ).
tcf(c_44251,plain,
! [X0: $i] :
( cong(sK5,X0,sK5,X0)
| ~ para(sK6,sK5,sK0,sK4) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44246,c_16204,c_16204]) ).
tcf(c_44252,plain,
! [X0: $i] : cong(sK5,X0,sK5,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_44251,c_3026]) ).
tcf(c_44332,plain,
! [X0: $i,X1: $i] :
( perp(sK5,sK5,X1,X0)
| ~ cong(sK5,X0,sK5,X0) ),
inference(superposition,[status(thm)],[c_44252,c_121]) ).
tcf(c_44336,plain,
! [X0: $i,X1: $i] : perp(sK5,sK5,X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_44332,c_44252]) ).
tcf(c_45596,plain,
! [X0: $i,X1: $i] : perp(X0,X1,sK5,sK5),
inference(superposition,[status(thm)],[c_44336,c_124]) ).
tcf(c_46582,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ perp(sK5,sK5,X0,X1) ),
inference(superposition,[status(thm)],[c_45596,c_100]) ).
tcf(c_46594,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : para(X0,X1,X2,X3),
inference(forward_subsumption_resolution,[status(thm)],[c_46582,c_44336]) ).
tcf(c_46616,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : eqangle(X0,X1,sK6,sK5,X2,X3,X4,X5),
inference(backward_subsumption_resolution,[status(thm)],[c_8687,c_46594]) ).
tcf(c_46623,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : eqangle(X0,X1,X2,X3,X4,X5,X2,X3),
inference(backward_subsumption_resolution,[status(thm)],[c_7315,c_46594]) ).
tcf(c_46887,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK0,sK4,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8911,c_46594]) ).
tcf(c_47092,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eqangle(sK0,sK4,X2,X3,X0,X1,X2,X3),
inference(global_subsumption_just,[status(thm)],[c_8969,c_98,c_8933,c_16992,c_34145,c_46594,c_46623,c_46616]) ).
tcf(c_47093,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eqangle(sK0,sK4,X0,X1,X2,X3,X0,X1),
inference(renaming,[status(thm)],[c_47092]) ).
tcf(c_47100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,X6,X7,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK0,sK4,X4,X5) ),
inference(superposition,[status(thm)],[c_47093,c_115]) ).
tcf(c_49849,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : eqangle(X4,X5,X0,X1,X4,X5,X2,X3),
inference(global_subsumption_just,[status(thm)],[c_9198,c_9163,c_46594]) ).
tcf(c_49850,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : eqangle(X0,X1,X2,X3,X0,X1,X4,X5),
inference(renaming,[status(thm)],[c_49849]) ).
tcf(c_49851,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : eqangle(X0,X1,X2,X3,sK0,sK4,X4,X5),
inference(superposition,[status(thm)],[c_49850,c_46887]) ).
tcf(c_55694,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : eqangle(X0,X1,X2,X3,X6,X7,X4,X5),
inference(global_subsumption_just,[status(thm)],[c_10198,c_47100,c_49851]) ).
tcf(c_55695,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : eqangle(X0,X1,X2,X3,X4,X5,X6,X7),
inference(renaming,[status(thm)],[c_55694]) ).
tcf(c_55696,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_49,c_55695]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO596+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 12:32:47 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.41
% 0.12/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.41
% 0.12/0.41 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 10.35/2.79 % SZS status Started for theBenchmark.p
% 10.35/2.79 % SZS status Theorem for theBenchmark.p
% 10.35/2.79
% 10.35/2.79 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.35/2.79
% 10.35/2.79 % ------ iProver source info
% 10.35/2.79
% 10.35/2.79 % git: date: 2026-07-19 20:42:38 +0200
% 10.35/2.79 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.35/2.79 % git: non_committed_changes: false
% 10.35/2.79
% 10.35/2.79 % ------ Parsing...
% 10.35/2.79 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.35/2.79
% 10.35/2.79 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 10.35/2.79
% 10.35/2.79 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 10.35/2.79 % ------ Proving...
% 10.35/2.79 % ------ Problem Properties
% 10.35/2.79
% 10.35/2.79 %
% 10.35/2.79 % clauses 94
% 10.35/2.79 % conjectures 7
% 10.35/2.79 % EPR 61
% 10.35/2.79 % Horn 89
% 10.35/2.79 % unary 7
% 10.35/2.79 % binary 24
% 10.35/2.79 % lits 263
% 10.35/2.79 % lits eq 0
% 10.35/2.79 % fd_pure 0
% 10.35/2.79 % fd_pseudo 0
% 10.35/2.79 % fd_cond 0
% 10.35/2.79 % fd_pseudo_cond 0
% 10.35/2.79 % AC symbols 0
% 10.35/2.79
% 10.35/2.79 % ------ Schedule dynamic 5 is on
% 10.35/2.79
% 10.35/2.79 % ------ no equalities: superposition off
% 10.35/2.79
% 10.35/2.79 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.35/2.79
% 10.35/2.79
% 10.35/2.79 % ------
% 10.35/2.79 % Current options:
% 10.35/2.79 % ------
% 10.35/2.79
% 10.35/2.79
% 10.35/2.79 %
% 10.35/2.79
% 10.35/2.79 % ------ Proving...
% 10.35/2.79 %
% 10.35/2.79
% 10.35/2.79 % SZS status Theorem for theBenchmark.p
% 10.35/2.79
% 10.35/2.79 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.35/2.79
% 10.35/2.79
%------------------------------------------------------------------------------