%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO575+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n011.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:31 PM UTC 2026
% Result : Theorem 50.37s 12.90s
% Output : CNFRefutation 50.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 32
% Syntax : Number of formulae : 386 ( 57 unt; 0 def)
% Number of atoms : 933 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1012 ( 465 ~; 458 |; 56 &)
% ( 0 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 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 : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 891 ( 0 sgn 873 !; 18 ?; 360 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD2) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( coll(X0,X1,X3)
& coll(X0,X1,X2) )
=> coll(X2,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD3) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD5) ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( para(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD6) ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD7) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(f11,axiom,
! [X0,X1,X2] :
( midp(X2,X1,X0)
=> midp(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD11) ).
fof(f13,axiom,
! [X0,X1,X2,X3,X4] :
( ( cong(X4,X0,X4,X3)
& cong(X4,X0,X4,X2)
& cong(X4,X0,X4,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD13) ).
fof(f14,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD14) ).
fof(f15,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD15) ).
fof(f16,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X1,X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD16) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD19) ).
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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD21) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD23) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD24) ).
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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f41,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD41) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f45,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X0,X2)
& midp(X3,X0,X1) )
=> para(X3,X4,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD44) ).
fof(f46,axiom,
! [X0,X1,X2,X3,X4] :
( ( coll(X4,X0,X2)
& para(X3,X4,X1,X2)
& midp(X3,X0,X1) )
=> midp(X4,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD45) ).
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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD56) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4] :
( ( para(X0,X3,X1,X2)
& para(X0,X2,X1,X3)
& midp(X4,X0,X1) )
=> midp(X4,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD64) ).
fof(f67,axiom,
! [X0,X1,X2] :
( para(X0,X1,X0,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD66) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( coll(X0,X1,X2)
& cong(X0,X1,X0,X2) )
=> midp(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD67) ).
fof(f69,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> cong(X0,X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD68) ).
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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD73) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( coll(X6,X0,X4)
& circle(X3,X0,X6,X8)
& coll(X5,X2,X4)
& circle(X3,X2,X5,X7)
& perp(X1,X2,X0,X4)
& perp(X0,X2,X1,X4)
& perp(X0,X1,X2,X4)
& circle(X3,X0,X1,X2) )
=> cong(X1,X6,X1,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL214037) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( coll(X6,X0,X4)
& circle(X3,X0,X6,X8)
& coll(X5,X2,X4)
& circle(X3,X2,X5,X7)
& perp(X1,X2,X0,X4)
& perp(X0,X2,X1,X4)
& perp(X0,X1,X2,X4)
& circle(X3,X0,X1,X2) )
=> cong(X1,X6,X1,X5) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( coll(X6,X0,X4)
& circle(X3,X0,X6,X8)
& coll(X5,X2,X4)
& circle(X3,X2,X5,X7)
& perp(X1,X2,X0,X4)
& perp(X0,X2,X1,X4)
& perp(X0,X1,X2,X4)
& circle(X3,X0,X1,X2)
& ~ cong(X1,X6,X1,X5) ),
inference(ennf_transformation,[],[f96]) ).
fof(f99,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( coll(X6,X0,X4)
& circle(X3,X0,X6,X8)
& coll(X5,X2,X4)
& circle(X3,X2,X5,X7)
& perp(X1,X2,X0,X4)
& perp(X0,X2,X1,X4)
& perp(X0,X1,X2,X4)
& circle(X3,X0,X1,X2)
& ~ cong(X1,X6,X1,X5) ),
inference(flattening,[],[f98]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(ennf_transformation,[],[f46]) ).
fof(f127,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(flattening,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(flattening,[],[f128]) ).
fof(f130,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f131,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f142,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(f143,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f142]) ).
fof(f150,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(f151,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f154,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f158,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f159,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f179,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(f180,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,[],[f179]) ).
fof(f181,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(ennf_transformation,[],[f65]) ).
fof(f182,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(flattening,[],[f181]) ).
fof(f185,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f186,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f185]) ).
fof(f187,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(f189,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f6]) ).
fof(f190,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f189]) ).
fof(f191,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f192,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f193,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f196,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(f198,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(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(f212,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f41]) ).
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(f215,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f216,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f217,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f218,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f13]) ).
fof(f219,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f218]) ).
fof(f220,plain,
( coll(sK6,sK0,sK4)
& circle(sK3,sK0,sK6,sK8)
& coll(sK5,sK2,sK4)
& circle(sK3,sK2,sK5,sK7)
& perp(sK1,sK2,sK0,sK4)
& perp(sK0,sK2,sK1,sK4)
& perp(sK0,sK1,sK2,sK4)
& circle(sK3,sK0,sK1,sK2)
& ~ cong(sK1,sK6,sK1,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8)],[f99]) ).
fof(f239,plain,
coll(sK6,sK0,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f241,plain,
coll(sK5,sK2,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f243,plain,
perp(sK1,sK2,sK0,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f244,plain,
perp(sK0,sK2,sK1,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f245,plain,
perp(sK0,sK1,sK2,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f247,plain,
~ cong(sK1,sK6,sK1,sK5),
inference(cnf_transformation,[],[f220]) ).
fof(f270,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f122]) ).
fof(f271,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f273,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(cnf_transformation,[],[f127]) ).
fof(f274,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f275,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f130]) ).
fof(f276,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f284,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f143]) ).
fof(f288,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,[],[f151]) ).
fof(f289,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f290,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f153]) ).
fof(f291,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f154]) ).
fof(f294,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f158]) ).
fof(f295,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f159]) ).
fof(f308,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,[],[f180]) ).
fof(f309,plain,
! [X2,X3,X0,X1,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(cnf_transformation,[],[f182]) ).
fof(f311,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f186]) ).
fof(f312,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f187]) ).
fof(f314,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f190]) ).
fof(f315,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f191]) ).
fof(f316,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f192]) ).
fof(f317,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
fof(f319,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,[],[f196]) ).
fof(f321,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,[],[f198]) ).
fof(f327,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(f328,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(f330,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f212]) ).
fof(f331,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(f332,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f215]) ).
fof(f333,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f216]) ).
fof(f334,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f217]) ).
fof(f335,plain,
! [X2,X3,X0,X1,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_49,negated_conjecture,
~ cong(sK1,sK6,sK1,sK5),
inference(cnf_transformation,[],[f247]) ).
tcf(c_51,negated_conjecture,
perp(sK0,sK1,sK2,sK4),
inference(cnf_transformation,[],[f245]) ).
tcf(c_52,negated_conjecture,
perp(sK0,sK2,sK1,sK4),
inference(cnf_transformation,[],[f244]) ).
tcf(c_53,negated_conjecture,
perp(sK1,sK2,sK0,sK4),
inference(cnf_transformation,[],[f243]) ).
tcf(c_55,negated_conjecture,
coll(sK5,sK2,sK4),
inference(cnf_transformation,[],[f241]) ).
tcf(c_57,negated_conjecture,
coll(sK6,sK0,sK4),
inference(cnf_transformation,[],[f239]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X1,X4,X3)
| ~ midp(X0,X4,X2)
| ~ coll(X1,X4,X3)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_94,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,[],[f284]) ).
tcf(c_98,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,[],[f288]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X2,X3,X0,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_118,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,[],[f308]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X4,X1,X3)
| ~ midp(X4,X0,X2)
| ~ para(X0,X3,X2,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X3,X0,X4,X2)
| ~ midp(X3,X1,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_122,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,[],[f312]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_129,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,[],[f319]) ).
tcf(c_131,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,[],[f321]) ).
tcf(c_137,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,[],[f327]) ).
tcf(c_138,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,[],[f328]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f330]) ).
tcf(c_141,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,[],[f331]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X3,X4)
| ~ cong(X0,X1,X0,X4)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_155,plain,
( midp(sK0,sK0,sK0)
| ~ coll(sK0,sK0,sK0)
| ~ cong(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_159,plain,
( perp(sK0,sK0,sK0,sK0)
| ~ cong(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_2269,plain,
( coll(sK6,sK4,sK0)
| ~ coll(sK6,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_2270,plain,
( perp(sK2,sK4,sK0,sK1)
| ~ perp(sK0,sK1,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_2272,plain,
( perp(sK0,sK4,sK1,sK2)
| ~ perp(sK1,sK2,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_2295,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK1,X0,X1)
| ~ perp(sK0,sK1,sK2,sK4)
| ~ perp(sK2,sK4,X0,X1) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_2466,plain,
! [X0: $i] :
( coll(sK0,X0,sK6)
| ~ coll(sK6,sK4,sK0)
| ~ coll(sK6,sK4,X0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_2469,plain,
( coll(sK0,sK0,sK6)
| ~ coll(sK6,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_2466]) ).
tcf(c_2511,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK4,X0,X1)
| ~ perp(sK0,sK4,sK1,sK2)
| ~ perp(sK1,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_2789,plain,
( para(sK0,sK1,sK0,sK1)
| ~ perp(sK2,sK4,sK0,sK1)
| ~ perp(sK0,sK1,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_2295]) ).
tcf(c_2895,plain,
coll(sK0,sK6,sK4),
inference(superposition,[status(thm)],[c_57,c_85]) ).
tcf(c_2901,plain,
coll(sK0,sK6,sK4),
inference(superposition,[status(thm)],[c_57,c_85]) ).
tcf(c_2936,plain,
coll(sK6,sK4,sK0),
inference(superposition,[status(thm)],[c_57,c_86]) ).
tcf(c_2942,plain,
coll(sK6,sK4,sK0),
inference(superposition,[status(thm)],[c_57,c_86]) ).
tcf(c_3093,plain,
~ midp(sK1,sK6,sK5),
inference(superposition,[status(thm)],[c_101,c_49]) ).
tcf(c_3111,plain,
perp(sK2,sK4,sK0,sK1),
inference(superposition,[status(thm)],[c_51,c_99]) ).
tcf(c_3118,plain,
perp(sK2,sK4,sK0,sK1),
inference(superposition,[status(thm)],[c_51,c_99]) ).
tcf(c_3119,plain,
perp(sK1,sK4,sK0,sK2),
inference(superposition,[status(thm)],[c_52,c_99]) ).
tcf(c_3245,plain,
perp(sK2,sK4,sK1,sK0),
inference(superposition,[status(thm)],[c_3111,c_100]) ).
tcf(c_3611,plain,
! [X0: $i] :
( coll(sK4,X0,sK5)
| ~ coll(sK5,sK2,X0) ),
inference(superposition,[status(thm)],[c_55,c_84]) ).
tcf(c_3614,plain,
! [X0: $i] :
( coll(sK4,X0,sK0)
| ~ coll(sK0,sK6,X0) ),
inference(superposition,[status(thm)],[c_2895,c_84]) ).
tcf(c_3616,plain,
! [X0: $i] :
( coll(sK0,X0,sK6)
| ~ coll(sK6,sK4,X0) ),
inference(superposition,[status(thm)],[c_2936,c_84]) ).
tcf(c_3661,plain,
! [X0: $i] :
( coll(sK4,X0,sK5)
| ~ coll(sK5,sK2,X0) ),
inference(superposition,[status(thm)],[c_55,c_84]) ).
tcf(c_3662,plain,
! [X0: $i] :
( coll(sK4,X0,sK6)
| ~ coll(sK6,sK0,X0) ),
inference(superposition,[status(thm)],[c_57,c_84]) ).
tcf(c_3664,plain,
! [X0: $i] :
( coll(sK4,X0,sK0)
| ~ coll(sK0,sK6,X0) ),
inference(superposition,[status(thm)],[c_2901,c_84]) ).
tcf(c_3666,plain,
! [X0: $i] :
( coll(sK0,X0,sK6)
| ~ coll(sK6,sK4,X0) ),
inference(superposition,[status(thm)],[c_2942,c_84]) ).
tcf(c_3850,plain,
coll(sK4,sK4,sK5),
inference(superposition,[status(thm)],[c_55,c_3611]) ).
tcf(c_3855,plain,
coll(sK4,sK4,sK5),
inference(superposition,[status(thm)],[c_55,c_3661]) ).
tcf(c_3856,plain,
! [X0: $i] :
( coll(sK5,X0,sK4)
| ~ coll(sK4,sK4,X0) ),
inference(superposition,[status(thm)],[c_3850,c_84]) ).
tcf(c_3862,plain,
! [X0: $i] :
( coll(sK5,X0,sK4)
| ~ coll(sK4,sK4,X0) ),
inference(superposition,[status(thm)],[c_3855,c_84]) ).
tcf(c_3943,plain,
coll(sK4,sK4,sK6),
inference(superposition,[status(thm)],[c_57,c_3662]) ).
tcf(c_3980,plain,
! [X0: $i] :
( coll(sK6,X0,sK4)
| ~ coll(sK4,sK4,X0) ),
inference(superposition,[status(thm)],[c_3943,c_84]) ).
tcf(c_4050,plain,
coll(sK4,sK4,sK0),
inference(superposition,[status(thm)],[c_2895,c_3614]) ).
tcf(c_4295,plain,
coll(sK0,sK0,sK6),
inference(superposition,[status(thm)],[c_2936,c_3616]) ).
tcf(c_4304,plain,
coll(sK0,sK6,sK0),
inference(superposition,[status(thm)],[c_4295,c_86]) ).
tcf(c_4334,plain,
coll(sK5,sK0,sK4),
inference(superposition,[status(thm)],[c_4050,c_3856]) ).
tcf(c_5079,plain,
! [X0: $i] :
( coll(sK0,X0,sK0)
| ~ coll(sK0,sK6,X0) ),
inference(superposition,[status(thm)],[c_4304,c_84]) ).
tcf(c_5085,plain,
( coll(sK0,sK0,sK0)
| ~ coll(sK0,sK6,sK0) ),
inference(instantiation,[status(thm)],[c_5079]) ).
tcf(c_5107,plain,
coll(sK5,sK4,sK0),
inference(superposition,[status(thm)],[c_4334,c_86]) ).
tcf(c_5346,plain,
( para(sK0,sK4,sK0,sK4)
| ~ perp(sK0,sK4,sK1,sK2)
| ~ perp(sK1,sK2,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_2511]) ).
tcf(c_5428,plain,
! [X0: $i,X1: $i] :
( perp(sK0,sK1,X0,X1)
| ~ perp(X0,X1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_5429,plain,
( perp(sK0,sK1,sK0,sK0)
| ~ perp(sK0,sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_5428]) ).
tcf(c_6301,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK1,X0,X1)
| ~ perp(sK2,sK4,X0,X1) ),
inference(superposition,[status(thm)],[c_51,c_98]) ).
tcf(c_6436,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK1,X0,X1)
| ~ perp(sK2,sK4,X0,X1) ),
inference(superposition,[status(thm)],[c_51,c_98]) ).
tcf(c_6444,plain,
! [X0: $i,X1: $i] :
( para(sK1,sK4,X0,X1)
| ~ perp(sK0,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_3119,c_98]) ).
tcf(c_6735,plain,
! [X0: $i,X1: $i] :
( eqangle(sK0,sK4,X0,X1,sK0,sK4,X0,X1)
| ~ para(sK0,sK4,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_6736,plain,
( eqangle(sK0,sK4,sK0,sK0,sK0,sK4,sK0,sK0)
| ~ para(sK0,sK4,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_6735]) ).
tcf(c_6770,plain,
! [X0: $i,X1: $i] :
( coll(sK6,sK1,X0)
| ~ coll(X0,X1,sK6)
| ~ coll(X0,X1,sK1) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_6771,plain,
( coll(sK6,sK1,sK0)
| ~ coll(sK0,sK0,sK6)
| ~ coll(sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_6770]) ).
tcf(c_7519,plain,
para(sK0,sK1,sK0,sK1),
inference(superposition,[status(thm)],[c_3111,c_6301]) ).
tcf(c_7520,plain,
para(sK0,sK1,sK1,sK0),
inference(superposition,[status(thm)],[c_3245,c_6301]) ).
tcf(c_7533,plain,
para(sK0,sK1,sK0,sK1),
inference(superposition,[status(thm)],[c_3118,c_6436]) ).
tcf(c_7749,plain,
coll(sK0,sK1,sK1),
inference(superposition,[status(thm)],[c_7519,c_81]) ).
tcf(c_7753,plain,
coll(sK0,sK1,sK1),
inference(superposition,[status(thm)],[c_7533,c_81]) ).
tcf(c_7756,plain,
para(sK1,sK0,sK0,sK1),
inference(superposition,[status(thm)],[c_7520,c_125]) ).
tcf(c_9765,plain,
! [X0: $i] :
( coll(sK0,X0,sK5)
| ~ coll(sK5,sK4,X0) ),
inference(superposition,[status(thm)],[c_5107,c_84]) ).
tcf(c_9771,plain,
( coll(sK0,sK0,sK5)
| ~ coll(sK5,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_9765]) ).
tcf(c_12474,plain,
coll(sK1,sK0,sK1),
inference(superposition,[status(thm)],[c_7749,c_85]) ).
tcf(c_12480,plain,
coll(sK1,sK0,sK1),
inference(superposition,[status(thm)],[c_7753,c_85]) ).
tcf(c_12883,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK0,sK4,X0,X1,sK0,sK4)
| ~ eqangle(sK0,sK4,X0,X1,sK0,sK4,X0,X1) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_12887,plain,
( eqangle(sK0,sK0,sK0,sK4,sK0,sK0,sK0,sK4)
| ~ eqangle(sK0,sK4,sK0,sK0,sK0,sK4,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_12883]) ).
tcf(c_13152,plain,
para(sK1,sK4,sK1,sK4),
inference(superposition,[status(thm)],[c_52,c_6444]) ).
tcf(c_13303,plain,
coll(sK1,sK4,sK4),
inference(superposition,[status(thm)],[c_13152,c_81]) ).
tcf(c_13966,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,X0,X0)
| ~ coll(X0,X0,X2)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_122,c_138]) ).
tcf(c_13978,plain,
( cyclic(sK0,sK0,sK0,sK0)
| ~ coll(sK0,sK0,sK0)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_13966]) ).
tcf(c_14052,plain,
coll(sK4,sK1,sK4),
inference(superposition,[status(thm)],[c_13303,c_85]) ).
tcf(c_14632,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X2,X3)
| ~ para(sK0,sK4,sK0,sK4)
| ~ eqangle(X0,X1,X2,X3,sK0,sK4,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_14633,plain,
( para(sK0,sK0,sK0,sK0)
| ~ para(sK0,sK4,sK0,sK4)
| ~ eqangle(sK0,sK0,sK0,sK0,sK0,sK4,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_14632]) ).
tcf(c_16218,plain,
( coll(sK6,sK0,sK1)
| ~ coll(sK6,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_18873,plain,
! [X0: $i] :
( midp(X0,sK1,sK1)
| ~ midp(X0,sK0,sK0)
| ~ para(sK0,sK1,sK0,sK1) ),
inference(superposition,[status(thm)],[c_7519,c_119]) ).
tcf(c_18921,plain,
! [X0: $i] :
( midp(X0,sK1,sK1)
| ~ midp(X0,sK0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18873,c_7519]) ).
tcf(c_18946,plain,
( midp(sK0,sK1,sK1)
| ~ midp(sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_18921]) ).
tcf(c_21871,plain,
coll(sK1,sK1,sK0),
inference(superposition,[status(thm)],[c_12474,c_86]) ).
tcf(c_21876,plain,
coll(sK1,sK1,sK0),
inference(superposition,[status(thm)],[c_12480,c_86]) ).
tcf(c_23968,plain,
coll(sK4,sK4,sK1),
inference(superposition,[status(thm)],[c_14052,c_86]) ).
tcf(c_24965,plain,
( para(sK1,sK0,sK1,sK0)
| ~ para(sK1,sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_28272,plain,
perp(sK2,sK4,sK0,sK1),
inference(superposition,[status(thm)],[c_51,c_99]) ).
tcf(c_28334,plain,
perp(sK2,sK4,sK1,sK0),
inference(superposition,[status(thm)],[c_28272,c_100]) ).
tcf(c_29164,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK1,X0,X1)
| ~ perp(sK2,sK4,X0,X1) ),
inference(superposition,[status(thm)],[c_51,c_98]) ).
tcf(c_29390,plain,
para(sK0,sK1,sK1,sK0),
inference(superposition,[status(thm)],[c_28334,c_29164]) ).
tcf(c_29411,plain,
para(sK1,sK0,sK0,sK1),
inference(superposition,[status(thm)],[c_29390,c_125]) ).
tcf(c_30755,plain,
! [X0: $i] :
( midp(sK0,X0,sK1)
| ~ midp(sK1,X0,sK0)
| ~ coll(sK0,X0,sK1) ),
inference(superposition,[status(thm)],[c_29411,c_83]) ).
tcf(c_30793,plain,
( midp(sK0,sK0,sK1)
| ~ midp(sK1,sK0,sK0)
| ~ coll(sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_30755]) ).
tcf(c_35316,plain,
! [X0: $i] :
( coll(sK0,X0,sK1)
| ~ coll(sK1,sK1,X0) ),
inference(superposition,[status(thm)],[c_21876,c_84]) ).
tcf(c_35321,plain,
( coll(sK0,sK0,sK1)
| ~ coll(sK1,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_35316]) ).
tcf(c_36749,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,X3,X2,X3)
| ~ cyclic(X1,X3,X0,X3)
| ~ cyclic(X1,X3,X0,X2)
| ~ cyclic(X1,X3,X0,X0)
| ~ para(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_122,c_137]) ).
tcf(c_36865,plain,
( cong(sK0,sK0,sK0,sK0)
| ~ cyclic(sK0,sK0,sK0,sK0)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_36749]) ).
tcf(c_37025,plain,
coll(sK6,sK1,sK4),
inference(superposition,[status(thm)],[c_23968,c_3980]) ).
tcf(c_37026,plain,
coll(sK5,sK1,sK4),
inference(superposition,[status(thm)],[c_23968,c_3862]) ).
tcf(c_39120,plain,
coll(sK6,sK4,sK1),
inference(superposition,[status(thm)],[c_37025,c_86]) ).
tcf(c_39350,plain,
coll(sK1,sK5,sK4),
inference(superposition,[status(thm)],[c_37026,c_85]) ).
tcf(c_41131,plain,
! [X0: $i] :
( coll(sK1,X0,sK6)
| ~ coll(sK6,sK4,X0) ),
inference(superposition,[status(thm)],[c_39120,c_84]) ).
tcf(c_41134,plain,
coll(sK0,sK1,sK6),
inference(superposition,[status(thm)],[c_39120,c_3666]) ).
tcf(c_41137,plain,
( coll(sK1,sK0,sK6)
| ~ coll(sK6,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_41131]) ).
tcf(c_41228,plain,
coll(sK1,sK4,sK5),
inference(superposition,[status(thm)],[c_39350,c_86]) ).
tcf(c_41273,plain,
coll(sK0,sK6,sK1),
inference(superposition,[status(thm)],[c_41134,c_86]) ).
tcf(c_41283,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK0,sK1,X2,X3)
| ~ perp(sK0,sK1,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_41284,plain,
( para(sK0,sK1,sK0,sK0)
| ~ perp(sK0,sK0,sK0,sK0)
| ~ perp(sK0,sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_41283]) ).
tcf(c_41377,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK1,sK0)
| ~ perp(X2,X3,sK1,sK0)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_41378,plain,
( para(sK0,sK0,sK1,sK0)
| ~ perp(sK0,sK0,sK0,sK0)
| ~ perp(sK0,sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_41377]) ).
tcf(c_42331,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK0,sK4,sK0,sK4)
| ~ eqangle(X0,X1,sK0,sK4,X2,X3,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_42332,plain,
( eqangle(sK0,sK0,sK0,sK0,sK0,sK4,sK0,sK4)
| ~ eqangle(sK0,sK0,sK0,sK4,sK0,sK0,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_42331]) ).
tcf(c_44221,plain,
! [X0: $i] :
( coll(sK5,X0,sK1)
| ~ coll(sK1,sK4,X0) ),
inference(superposition,[status(thm)],[c_41228,c_84]) ).
tcf(c_44226,plain,
( coll(sK5,sK0,sK1)
| ~ coll(sK1,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_44221]) ).
tcf(c_44313,plain,
! [X0: $i] :
( coll(sK1,X0,sK0)
| ~ coll(sK0,sK6,X0) ),
inference(superposition,[status(thm)],[c_41273,c_84]) ).
tcf(c_44316,plain,
coll(sK4,sK1,sK0),
inference(superposition,[status(thm)],[c_41273,c_3664]) ).
tcf(c_44319,plain,
( coll(sK1,sK0,sK0)
| ~ coll(sK0,sK6,sK0) ),
inference(instantiation,[status(thm)],[c_44313]) ).
tcf(c_46139,plain,
coll(sK1,sK4,sK0),
inference(superposition,[status(thm)],[c_44316,c_85]) ).
tcf(c_53292,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK1,X1)
| ~ midp(X0,X1,sK1) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_53293,plain,
( midp(sK0,sK1,sK0)
| ~ midp(sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_53292]) ).
tcf(c_55977,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X1,sK5,X2,X3,X1,sK5)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_55978,plain,
( eqangle(sK0,sK0,sK0,sK5,sK0,sK0,sK0,sK5)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_55977]) ).
tcf(c_56883,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK5,X2,X3)
| ~ midp(sK5,X1,X3)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_56884,plain,
( para(sK0,sK5,sK0,sK0)
| ~ midp(sK0,sK0,sK0)
| ~ midp(sK5,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_56883]) ).
tcf(c_58228,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK1,sK0)
| ~ cong(X0,sK0,X1,sK0)
| ~ cong(X0,sK1,X1,sK1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_58229,plain,
( perp(sK0,sK0,sK1,sK0)
| ~ cong(sK0,sK0,sK0,sK0)
| ~ cong(sK0,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_58228]) ).
tcf(c_58321,plain,
! [X0: $i] :
( perp(sK0,X0,sK0,sK1)
| ~ cong(sK0,sK0,X0,sK0)
| ~ cong(sK0,sK1,X0,sK1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_58322,plain,
( perp(sK0,sK0,sK0,sK1)
| ~ cong(sK0,sK0,sK0,sK0)
| ~ cong(sK0,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_58321]) ).
tcf(c_59637,plain,
! [X0: $i,X1: $i] :
( midp(sK1,sK6,sK5)
| ~ midp(sK1,X0,X1)
| ~ para(X0,sK5,X1,sK6)
| ~ para(X0,sK6,X1,sK5) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_59638,plain,
( midp(sK1,sK6,sK5)
| ~ midp(sK1,sK0,sK0)
| ~ para(sK0,sK5,sK0,sK6)
| ~ para(sK0,sK6,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_59637]) ).
tcf(c_59683,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK1,sK5)
| ~ cong(sK1,sK5,X0,X1) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_60096,plain,
! [X0: $i] :
( cong(X0,sK5,sK1,sK5)
| ~ cong(sK1,sK5,X0,sK5) ),
inference(instantiation,[status(thm)],[c_59683]) ).
tcf(c_60098,plain,
( cong(sK0,sK5,sK1,sK5)
| ~ cong(sK1,sK5,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_60096]) ).
tcf(c_60104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(sK1,sK5,X2,X3)
| ~ cyclic(sK1,sK5,X0,X3)
| ~ cyclic(sK1,sK5,X0,X2)
| ~ cyclic(sK1,sK5,X0,X1)
| ~ eqangle(X0,sK1,X0,sK5,X1,X2,X1,X3) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_60116,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK5,sK1)
| ~ cong(sK5,sK1,X0,X1) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_60119,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK5,sK1)
| ~ cong(X0,X1,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_60144,plain,
! [X0: $i] :
( cyclic(sK6,sK1,X0,sK1)
| ~ cyclic(sK6,X0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_60145,plain,
( cyclic(sK6,sK1,sK0,sK1)
| ~ cyclic(sK6,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_60144]) ).
tcf(c_60158,plain,
! [X0: $i] :
( cyclic(sK1,sK6,sK1,X0)
| ~ cyclic(sK1,sK1,sK6,X0) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_60242,plain,
! [X0: $i] :
( cyclic(X0,sK1,sK6,sK1)
| ~ cyclic(X0,sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_60243,plain,
( cyclic(sK0,sK1,sK6,sK1)
| ~ cyclic(sK0,sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_60242]) ).
tcf(c_60257,plain,
! [X0: $i,X1: $i] :
( midp(sK5,X0,X1)
| ~ coll(sK5,X0,X1)
| ~ cong(sK5,X0,sK5,X1) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_60261,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK5,X1,X3)
| ~ midp(sK5,X0,X2)
| ~ para(X0,X3,X2,X1)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_60276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK1,X3,X2)
| ~ coll(sK1,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK1,X1,X2) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_60277,plain,
( midp(sK1,sK0,sK0)
| ~ midp(sK0,sK0,sK0)
| ~ coll(sK1,sK0,sK0)
| ~ para(sK0,sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_60276]) ).
tcf(c_60344,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,sK6,X1,sK5)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(X0,sK6,X1,sK5,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_60426,plain,
! [X0: $i] :
( cong(X0,sK1,X0,sK1)
| ~ midp(X0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_60427,plain,
( cong(sK0,sK1,sK0,sK1)
| ~ midp(sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_60426]) ).
tcf(c_60436,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X1,sK1,X1,sK1)
| ~ cyclic(X1,sK1,X0,sK1)
| ~ cyclic(X1,sK1,X0,X2)
| ~ cyclic(X1,sK1,X0,X1)
| ~ eqangle(X0,X1,X0,sK1,X2,X1,X2,sK1) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_60468,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,X0,sK1)
| ~ coll(X0,sK1,X2)
| ~ eqangle(X0,X1,X0,X2,sK1,X1,sK1,X2) ),
inference(instantiation,[status(thm)],[c_138]) ).
tcf(c_60471,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X0,X2,sK1)
| ~ cyclic(X0,X1,X2,sK1) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_60474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X3,sK1)
| ~ cong(X0,X1,X0,sK1)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_145]) ).
tcf(c_60475,plain,
( cyclic(sK0,sK0,sK0,sK1)
| ~ cong(sK0,sK0,sK0,sK0)
| ~ cong(sK0,sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_60474]) ).
tcf(c_62264,plain,
! [X0: $i] :
( coll(sK1,sK1,sK6)
| ~ coll(sK6,X0,sK1) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_62265,plain,
( coll(sK1,sK1,sK6)
| ~ coll(sK6,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_62264]) ).
tcf(c_62536,plain,
! [X0: $i] :
( cyclic(sK6,sK1,sK1,X0)
| ~ cyclic(sK1,sK6,sK1,X0) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_62538,plain,
! [X0: $i] :
( cyclic(sK6,sK1,sK1,X0)
| ~ cyclic(sK6,sK1,X0,sK1) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_62539,plain,
( cyclic(sK6,sK1,sK1,sK0)
| ~ cyclic(sK6,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_62538]) ).
tcf(c_62548,plain,
! [X0: $i,X1: $i] :
( cyclic(sK1,sK1,sK6,X1)
| ~ cyclic(X0,sK1,sK1,sK6)
| ~ cyclic(X0,sK1,sK1,X1) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_62555,plain,
( cyclic(sK1,sK6,sK1,sK6)
| ~ cyclic(sK1,sK1,sK6,sK6) ),
inference(instantiation,[status(thm)],[c_60158]) ).
tcf(c_62667,plain,
! [X0: $i] :
( cyclic(X0,sK1,sK1,sK6)
| ~ cyclic(X0,sK1,sK6,sK1) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_62668,plain,
( cyclic(sK0,sK1,sK1,sK6)
| ~ cyclic(sK0,sK1,sK6,sK1) ),
inference(instantiation,[status(thm)],[c_62667]) ).
tcf(c_62844,plain,
! [X0: $i] :
( coll(sK6,sK1,sK1)
| ~ coll(sK1,X0,sK6)
| ~ coll(sK1,X0,sK1) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_62845,plain,
( coll(sK6,sK1,sK1)
| ~ coll(sK1,sK0,sK6)
| ~ coll(sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_62844]) ).
tcf(c_63020,plain,
! [X0: $i] :
( cong(sK5,X0,sK5,sK1)
| ~ cong(sK5,sK1,sK5,X0) ),
inference(instantiation,[status(thm)],[c_60116]) ).
tcf(c_63022,plain,
( cong(sK5,sK0,sK5,sK1)
| ~ cong(sK5,sK1,sK5,sK0) ),
inference(instantiation,[status(thm)],[c_63020]) ).
tcf(c_63308,plain,
! [X0: $i,X1: $i] :
( para(X1,sK5,X0,sK6)
| ~ para(X0,sK6,X1,sK5) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_63309,plain,
( para(sK0,sK5,sK0,sK6)
| ~ para(sK0,sK6,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_63308]) ).
tcf(c_63520,plain,
! [X0: $i,X1: $i] :
( midp(sK6,X0,X1)
| ~ coll(sK6,X0,X1)
| ~ cong(sK6,X0,sK6,X1) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_63708,plain,
! [X0: $i,X1: $i] :
( cong(sK5,X0,sK5,X1)
| ~ cong(sK5,X0,X1,sK5) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_63859,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,sK1,X3)
| ~ cyclic(X0,X1,X2,sK1)
| ~ cyclic(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_63942,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK1,X3,sK5)
| ~ para(X1,X2,X3,sK5)
| ~ para(X0,sK1,X1,X2) ),
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_63947,plain,
( para(sK0,sK1,sK0,sK5)
| ~ para(sK0,sK0,sK0,sK5)
| ~ para(sK0,sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_63942]) ).
tcf(c_64042,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,X0,sK1)
| ~ midp(X0,X1,sK1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_64043,plain,
( cong(sK0,sK0,sK0,sK1)
| ~ midp(sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_64042]) ).
tcf(c_64412,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK6,X2,X3)
| ~ midp(sK6,X1,X3)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_64563,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X2,sK1,X0,X1)
| ~ cong(X0,X1,X2,sK1) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_64610,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X1,X2,X0,sK5)
| ~ para(X0,sK5,X1,X2) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_64611,plain,
( para(sK0,sK0,sK0,sK5)
| ~ para(sK0,sK5,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_64610]) ).
tcf(c_65088,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,X1,sK1,sK1)
| ~ coll(sK1,sK1,X1)
| ~ eqangle(sK1,X0,sK1,X1,sK1,X0,sK1,X1) ),
inference(instantiation,[status(thm)],[c_60468]) ).
tcf(c_65089,plain,
! [X0: $i,X1: $i] :
( eqangle(sK1,X0,sK1,X1,sK1,X0,sK1,X1)
| ~ para(sK1,X0,sK1,X0) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_65583,plain,
! [X0: $i,X1: $i] :
( cyclic(sK1,sK5,X0,X1)
| ~ cyclic(sK1,X0,sK5,X1) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_65585,plain,
! [X0: $i,X1: $i] :
( cyclic(sK1,sK5,X0,X1)
| ~ coll(X0,X1,sK5)
| ~ eqangle(X0,sK1,X0,sK5,X1,sK1,X1,sK5) ),
inference(instantiation,[status(thm)],[c_138]) ).
tcf(c_65586,plain,
( cyclic(sK1,sK5,sK0,sK0)
| ~ coll(sK0,sK0,sK5)
| ~ eqangle(sK0,sK1,sK0,sK5,sK0,sK1,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_65585]) ).
tcf(c_65683,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,sK5,X0,X1,X0,sK5)
| ~ para(X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_68245,plain,
! [X0: $i] :
( eqangle(sK1,sK6,sK1,sK1,X0,sK6,X0,sK1)
| ~ cyclic(sK6,sK1,sK1,X0) ),
inference(instantiation,[status(thm)],[c_140]) ).
tcf(c_68246,plain,
( eqangle(sK1,sK6,sK1,sK1,sK0,sK6,sK0,sK1)
| ~ cyclic(sK6,sK1,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_68245]) ).
tcf(c_68721,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X2,X1,sK5)
| ~ cyclic(X0,X1,X2,sK5) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_68724,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X3,sK5)
| ~ cyclic(X0,X1,X2,sK5)
| ~ cyclic(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_68726,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,X2,sK5)
| ~ cyclic(X0,X1,sK5,X2) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_68727,plain,
( cyclic(sK0,sK0,sK0,sK5)
| ~ cyclic(sK0,sK0,sK5,sK0) ),
inference(instantiation,[status(thm)],[c_68726]) ).
tcf(c_68786,plain,
! [X0: $i] :
( cyclic(sK6,X0,sK1,sK1)
| ~ cyclic(X0,sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_60471]) ).
tcf(c_68787,plain,
( cyclic(sK6,sK0,sK1,sK1)
| ~ cyclic(sK0,sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_68786]) ).
tcf(c_71036,plain,
! [X0: $i] :
( midp(sK5,X0,sK1)
| ~ coll(sK5,X0,sK1)
| ~ cong(sK5,X0,sK5,sK1) ),
inference(instantiation,[status(thm)],[c_60257]) ).
tcf(c_71038,plain,
( midp(sK5,sK0,sK1)
| ~ coll(sK5,sK0,sK1)
| ~ cong(sK5,sK0,sK5,sK1) ),
inference(instantiation,[status(thm)],[c_71036]) ).
tcf(c_71153,plain,
( midp(sK6,sK1,sK1)
| ~ coll(sK6,sK1,sK1)
| ~ cong(sK6,sK1,sK6,sK1) ),
inference(instantiation,[status(thm)],[c_63520]) ).
tcf(c_71154,plain,
! [X0: $i,X1: $i] :
( cong(sK6,sK1,sK6,sK1)
| ~ cyclic(sK6,sK1,X0,sK6)
| ~ cyclic(sK6,sK1,X0,sK1)
| ~ cyclic(sK6,sK1,X0,X1)
| ~ eqangle(X0,sK6,X0,sK1,X1,sK6,X1,sK1) ),
inference(instantiation,[status(thm)],[c_60436]) ).
tcf(c_71548,plain,
! [X0: $i] :
( cong(sK5,sK1,X0,sK5)
| ~ cong(X0,sK5,sK5,sK1) ),
inference(instantiation,[status(thm)],[c_64563]) ).
tcf(c_71549,plain,
! [X0: $i] :
( cong(sK5,sK1,sK5,X0)
| ~ cong(sK5,sK1,X0,sK5) ),
inference(instantiation,[status(thm)],[c_63708]) ).
tcf(c_71550,plain,
( cong(sK5,sK1,sK0,sK5)
| ~ cong(sK0,sK5,sK5,sK1) ),
inference(instantiation,[status(thm)],[c_71548]) ).
tcf(c_71551,plain,
( cong(sK5,sK1,sK5,sK0)
| ~ cong(sK5,sK1,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_71549]) ).
tcf(c_72743,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK1,X1,sK5)
| ~ cyclic(X0,X1,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_68721]) ).
tcf(c_72746,plain,
( cyclic(sK0,sK1,sK0,sK5)
| ~ cyclic(sK0,sK0,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_72743]) ).
tcf(c_73328,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,sK5,X2)
| ~ cyclic(X0,sK5,X1,X2) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_73329,plain,
( cyclic(sK0,sK0,sK5,sK0)
| ~ cyclic(sK0,sK5,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_73328]) ).
tcf(c_74514,plain,
( cyclic(sK6,sK1,sK1,sK6)
| ~ cyclic(sK1,sK6,sK1,sK6) ),
inference(instantiation,[status(thm)],[c_62536]) ).
tcf(c_75219,plain,
! [X0: $i] :
( cyclic(X0,sK6,sK1,sK1)
| ~ coll(sK1,sK1,sK6)
| ~ eqangle(sK1,X0,sK1,sK6,sK1,X0,sK1,sK6) ),
inference(instantiation,[status(thm)],[c_65088]) ).
tcf(c_75220,plain,
( cyclic(sK0,sK6,sK1,sK1)
| ~ coll(sK1,sK1,sK6)
| ~ eqangle(sK1,sK0,sK1,sK6,sK1,sK0,sK1,sK6) ),
inference(instantiation,[status(thm)],[c_75219]) ).
tcf(c_79067,plain,
! [X0: $i] :
( eqangle(X0,sK1,X0,sK5,X0,sK1,X0,sK5)
| ~ para(X0,sK1,X0,sK1) ),
inference(instantiation,[status(thm)],[c_65683]) ).
tcf(c_79068,plain,
( eqangle(sK0,sK1,sK0,sK5,sK0,sK1,sK0,sK5)
| ~ para(sK0,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_79067]) ).
tcf(c_79975,plain,
! [X0: $i] :
( cyclic(sK6,sK1,sK1,sK1)
| ~ cyclic(X0,sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_63859]) ).
tcf(c_79976,plain,
! [X0: $i] :
( cong(sK6,sK1,sK6,sK1)
| ~ cyclic(sK6,sK1,sK1,sK6)
| ~ cyclic(sK6,sK1,sK1,sK1)
| ~ cyclic(sK6,sK1,sK1,X0)
| ~ eqangle(sK1,sK6,sK1,sK1,X0,sK6,X0,sK1) ),
inference(instantiation,[status(thm)],[c_71154]) ).
tcf(c_79981,plain,
( cyclic(sK6,sK1,sK1,sK1)
| ~ cyclic(sK0,sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_79975]) ).
tcf(c_79982,plain,
( cong(sK6,sK1,sK6,sK1)
| ~ cyclic(sK6,sK1,sK1,sK0)
| ~ cyclic(sK6,sK1,sK1,sK6)
| ~ cyclic(sK6,sK1,sK1,sK1)
| ~ eqangle(sK1,sK6,sK1,sK1,sK0,sK6,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_79976]) ).
tcf(c_80006,plain,
! [X0: $i,X1: $i] :
( cyclic(X1,X1,sK1,sK5)
| ~ cyclic(X0,X1,X1,sK5)
| ~ cyclic(X0,X1,X1,sK1) ),
inference(instantiation,[status(thm)],[c_63859]) ).
tcf(c_80007,plain,
( cyclic(sK0,sK0,sK1,sK5)
| ~ cyclic(sK0,sK0,sK0,sK5)
| ~ cyclic(sK0,sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_80006]) ).
tcf(c_80041,plain,
! [X0: $i,X1: $i] :
( cong(sK1,sK5,X0,sK5)
| ~ cyclic(sK1,sK5,X0,sK5)
| ~ cyclic(sK1,sK5,X0,X1)
| ~ cyclic(sK1,sK5,X0,X0)
| ~ eqangle(X0,sK1,X0,sK5,X1,X0,X1,sK5) ),
inference(instantiation,[status(thm)],[c_60104]) ).
tcf(c_80043,plain,
( cong(sK1,sK5,sK0,sK5)
| ~ cyclic(sK1,sK5,sK0,sK0)
| ~ cyclic(sK1,sK5,sK0,sK5)
| ~ eqangle(sK0,sK1,sK0,sK5,sK0,sK0,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_80041]) ).
tcf(c_80046,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,sK1,X0,sK5,X0,X1,X0,sK5)
| ~ para(X0,sK1,X0,X1) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_80047,plain,
( eqangle(sK0,sK1,sK0,sK5,sK0,sK0,sK0,sK5)
| ~ para(sK0,sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_80046]) ).
tcf(c_80126,plain,
! [X0: $i] :
( cyclic(sK1,sK5,X0,sK5)
| ~ cyclic(sK1,X0,sK5,sK5) ),
inference(instantiation,[status(thm)],[c_65583]) ).
tcf(c_80130,plain,
( cyclic(sK1,sK5,sK0,sK5)
| ~ cyclic(sK1,sK0,sK5,sK5) ),
inference(instantiation,[status(thm)],[c_80126]) ).
tcf(c_80903,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK5,X0,X2)
| ~ coll(X0,X2,sK5)
| ~ eqangle(X0,X1,X0,sK5,X2,X1,X2,sK5) ),
inference(instantiation,[status(thm)],[c_138]) ).
tcf(c_80904,plain,
( cyclic(sK0,sK5,sK0,sK0)
| ~ coll(sK0,sK0,sK5)
| ~ eqangle(sK0,sK0,sK0,sK5,sK0,sK0,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_80903]) ).
tcf(c_81740,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,sK5,X0,sK1,X0,sK5)
| ~ para(X0,X1,X0,sK1) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_88164,plain,
! [X0: $i,X1: $i] :
( cyclic(sK1,X1,sK5,sK5)
| ~ cyclic(X0,sK1,X1,sK5) ),
inference(instantiation,[status(thm)],[c_68724]) ).
tcf(c_88165,plain,
( cyclic(sK1,sK0,sK5,sK5)
| ~ cyclic(sK0,sK1,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_88164]) ).
tcf(c_88282,plain,
! [X0: $i] :
( eqangle(sK1,X0,sK1,sK6,sK1,X0,sK1,sK6)
| ~ para(sK1,X0,sK1,X0) ),
inference(instantiation,[status(thm)],[c_65089]) ).
tcf(c_88283,plain,
( eqangle(sK1,sK0,sK1,sK6,sK1,sK0,sK1,sK6)
| ~ para(sK1,sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_88282]) ).
tcf(c_89366,plain,
! [X0: $i] :
( eqangle(X0,sK6,X0,sK5,X0,sK1,X0,sK5)
| ~ para(X0,sK6,X0,sK1) ),
inference(instantiation,[status(thm)],[c_81740]) ).
tcf(c_89368,plain,
( eqangle(sK0,sK6,sK0,sK5,sK0,sK1,sK0,sK5)
| ~ para(sK0,sK6,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_89366]) ).
tcf(c_89507,plain,
! [X0: $i] :
( cong(X0,sK5,sK5,sK1)
| ~ cong(X0,sK5,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_60119]) ).
tcf(c_89511,plain,
( cong(sK0,sK5,sK5,sK1)
| ~ cong(sK0,sK5,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_89507]) ).
tcf(c_92251,plain,
! [X0: $i] :
( cyclic(sK1,sK1,sK6,sK6)
| ~ cyclic(X0,sK1,sK1,sK6) ),
inference(instantiation,[status(thm)],[c_62548]) ).
tcf(c_92255,plain,
( cyclic(sK1,sK1,sK6,sK6)
| ~ cyclic(sK0,sK1,sK1,sK6) ),
inference(instantiation,[status(thm)],[c_92251]) ).
tcf(c_95733,plain,
! [X0: $i,X1: $i] :
( para(X0,sK6,X1,sK1)
| ~ midp(sK6,sK1,sK1)
| ~ midp(X0,sK1,X1) ),
inference(instantiation,[status(thm)],[c_64412]) ).
tcf(c_95734,plain,
( para(sK0,sK6,sK0,sK1)
| ~ midp(sK0,sK1,sK0)
| ~ midp(sK6,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_95733]) ).
tcf(c_95861,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK5,X1,X2)
| ~ midp(sK5,X0,sK1)
| ~ para(X0,X2,sK1,X1)
| ~ para(X0,X1,sK1,X2) ),
inference(instantiation,[status(thm)],[c_60261]) ).
tcf(c_95862,plain,
( midp(sK5,sK0,sK0)
| ~ midp(sK5,sK0,sK1)
| ~ para(sK0,sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_95861]) ).
tcf(c_97673,plain,
! [X0: $i,X1: $i] :
( para(X0,sK6,X0,sK5)
| ~ para(X1,sK1,X1,sK5)
| ~ eqangle(X0,sK6,X0,sK5,X1,sK1,X1,sK5) ),
inference(instantiation,[status(thm)],[c_60344]) ).
tcf(c_97675,plain,
( para(sK0,sK6,sK0,sK5)
| ~ para(sK0,sK1,sK0,sK5)
| ~ eqangle(sK0,sK6,sK0,sK5,sK0,sK1,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_97673]) ).
tcf(c_97676,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_97675,c_95862,c_95734,c_92255,c_89511,c_89368,c_88283,c_88165,c_80904,c_80130,c_80047,c_80043,c_80007,c_79982,c_79981,c_79068,c_75220,c_74514,c_73329,c_72746,c_71551,c_71550,c_71153,c_71038,c_68787,c_68727,c_68246,c_65586,c_64611,c_64043,c_63947,c_63309,c_63022,c_62845,c_62668,c_62555,c_62539,c_62265,c_60475,c_60427,c_60277,c_60243,c_60145,c_60098,c_59638,c_58322,c_58229,c_56884,c_55978,c_53293,c_46139,c_44319,c_44226,c_42332,c_41378,c_41284,c_41137,c_36865,c_35321,c_30793,c_24965,c_21871,c_18946,c_16218,c_14633,c_13978,c_12887,c_12474,c_9771,c_7756,c_6771,c_6736,c_5429,c_5346,c_5107,c_5085,c_4304,c_3093,c_2789,c_2469,c_2272,c_2270,c_2269,c_159,c_155,c_51,c_53,c_57]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO575+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.38 % Computer : n011.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Wed Sep 23 12:27:19 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.42 Running first-order theorem proving
% 0.16/5.42 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.16/5.43
% 0.16/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.43
% 0.16/5.44 % Detected problem language: tptp
% 0.16/5.45 % Proving...
% 50.37/12.90 % SZS status Started for theBenchmark.p
% 50.37/12.90 % SZS status Theorem for theBenchmark.p
% 50.37/12.90
% 50.37/12.90 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 50.37/12.90
% 50.37/12.90 % ------ iProver source info
% 50.37/12.90
% 50.37/12.90 % git: date: 2026-07-19 20:42:38 +0200
% 50.37/12.90 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 50.37/12.90 % git: non_committed_changes: false
% 50.37/12.90
% 50.37/12.90 % ------ Parsing...
% 50.37/12.90 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 50.37/12.90
% 50.37/12.90 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 50.37/12.90
% 50.37/12.90 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 50.37/12.90 % ------ Proving...
% 50.37/12.90 % ------ Problem Properties
% 50.37/12.90
% 50.37/12.90 %
% 50.37/12.90 % clauses 96
% 50.37/12.90 % conjectures 9
% 50.37/12.90 % EPR 63
% 50.37/12.90 % Horn 91
% 50.37/12.90 % unary 9
% 50.37/12.90 % binary 24
% 50.37/12.90 % lits 265
% 50.37/12.90 % lits eq 0
% 50.37/12.90 % fd_pure 0
% 50.37/12.90 % fd_pseudo 0
% 50.37/12.90 % fd_cond 0
% 50.37/12.90 % fd_pseudo_cond 0
% 50.37/12.90 % AC symbols 0
% 50.37/12.90
% 50.37/12.90 % ------ Schedule dynamic 5 is on
% 50.37/12.90
% 50.37/12.90 % ------ no equalities: superposition off
% 50.37/12.90
% 50.37/12.90 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 50.37/12.90
% 50.37/12.90
% 50.37/12.90 % ------
% 50.37/12.90 % Current options:
% 50.37/12.90 % ------
% 50.37/12.90
% 50.37/12.90
% 50.37/12.90 %
% 50.37/12.90
% 50.37/12.90 % ------ Proving...
% 50.37/12.90 %
% 50.37/12.90
% 50.37/12.90 % SZS status Theorem for theBenchmark.p
% 50.37/12.90
% 50.37/12.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 50.37/12.91
% 50.37/12.91
%------------------------------------------------------------------------------