%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO602+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 : n006.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:36 PM UTC 2026
% Result : Theorem 154.82s 23.58s
% Output : CNFRefutation 154.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 44
% Syntax : Number of formulae : 509 ( 89 unt; 0 def)
% Number of atoms : 1224 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1301 ( 586 ~; 585 |; 85 &)
% ( 0 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 6 avg)
% Maximal term depth : 3 ( 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 : 19 ( 19 usr; 17 con; 0-5 aty)
% Number of variables : 1253 ( 0 sgn1214 !; 39 ?; 429 :)
% 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(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(f10,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> perp(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD10) ).
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(f12,axiom,
! [X0,X1,X2,X3] :
( ( cong(X3,X0,X3,X2)
& cong(X3,X0,X3,X1) )
=> circle(X3,X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD12) ).
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(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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD22) ).
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(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/sandbox2/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/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(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/sandbox2/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/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(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(f47,axiom,
! [X0,X1,X2] :
( cong(X2,X0,X2,X1)
=> eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD46) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( perp(X3,X0,X0,X4)
& circle(X3,X0,X1,X2) )
=> eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD48) ).
fof(f50,axiom,
! [X0,X1,X2,X3,X4] :
( ( eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
& circle(X3,X0,X1,X2) )
=> perp(X3,X0,X0,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD49) ).
fof(f51,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X1,X2)
& circle(X3,X0,X1,X2) )
=> eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD50) ).
fof(f52,axiom,
! [X0,X1,X2,X3,X4] :
( ( eqangle(X0,X1,X0,X2,X3,X1,X3,X4)
& coll(X4,X1,X2)
& circle(X3,X0,X1,X2) )
=> midp(X4,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD51) ).
fof(f53,axiom,
! [X0,X1,X2,X3] :
( ( midp(X3,X0,X2)
& perp(X0,X1,X1,X2) )
=> cong(X0,X3,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD52) ).
fof(f54,axiom,
! [X0,X1,X2,X3] :
( ( coll(X3,X0,X2)
& circle(X3,X0,X1,X2) )
=> perp(X0,X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD53) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( perp(X3,X2,X0,X1)
& midp(X2,X0,X1) )
=> cong(X3,X0,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD55) ).
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(f64,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X2,X3)
& midp(X4,X0,X1) )
=> para(X0,X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD63) ).
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(f75,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( perp(X4,X5,X6,X7)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD74) ).
fof(f87,axiom,
! [X0,X1,X2,X3] :
? [X4] :
( circle(X3,X0,X1,X2)
=> perp(X4,X0,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX11) ).
fof(f91,axiom,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ( coll(X1,X3,X4)
& perp(X0,X2,X2,X1) )
=> ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX15) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ( circle(X0,X2,X7,X16)
& coll(X7,X3,X5)
& coll(X6,X2,X5)
& circle(X0,X2,X6,X15)
& circle(X1,X2,X5,X14)
& coll(X4,X2,X3)
& coll(X4,X0,X1)
& circle(X0,X2,X3,X13)
& circle(X1,X2,X3,X12)
& circle(X0,X2,X10,X11)
& circle(X1,X2,X8,X9) )
=> perp(X6,X7,X5,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL618064) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ( circle(X0,X2,X7,X16)
& coll(X7,X3,X5)
& coll(X6,X2,X5)
& circle(X0,X2,X6,X15)
& circle(X1,X2,X5,X14)
& coll(X4,X2,X3)
& coll(X4,X0,X1)
& circle(X0,X2,X3,X13)
& circle(X1,X2,X3,X12)
& circle(X0,X2,X10,X11)
& circle(X1,X2,X8,X9) )
=> perp(X6,X7,X5,X1) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f108,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(f109,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f10]) ).
fof(f111,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(flattening,[],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(flattening,[],[f113]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f120,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(f121,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(flattening,[],[f120]) ).
fof(f123,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(f124,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(f125,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(f126,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(f127,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,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f148,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(f149,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(f150,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f41]) ).
fof(f151,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(f152,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,[],[f151]) ).
fof(f153,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(f154,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,[],[f153]) ).
fof(f155,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(f156,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,[],[f155]) ).
fof(f159,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(f160,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,[],[f159]) ).
fof(f161,plain,
! [X0,X1,X2] :
( ~ cong(X2,X0,X2,X1)
| eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(f164,plain,
! [X0,X1,X2,X3,X4] :
( ~ perp(X3,X0,X0,X4)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4] :
( ~ perp(X3,X0,X0,X4)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(flattening,[],[f164]) ).
fof(f166,plain,
! [X0,X1,X2,X3,X4] :
( ~ eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| perp(X3,X0,X0,X4) ),
inference(ennf_transformation,[],[f50]) ).
fof(f167,plain,
! [X0,X1,X2,X3,X4] :
( ~ eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| perp(X3,X0,X0,X4) ),
inference(flattening,[],[f166]) ).
fof(f168,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(ennf_transformation,[],[f51]) ).
fof(f169,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(flattening,[],[f168]) ).
fof(f170,plain,
! [X0,X1,X2,X3,X4] :
( ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X4)
| ~ coll(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| midp(X4,X1,X2) ),
inference(ennf_transformation,[],[f52]) ).
fof(f171,plain,
! [X0,X1,X2,X3,X4] :
( ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X4)
| ~ coll(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| midp(X4,X1,X2) ),
inference(flattening,[],[f170]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(ennf_transformation,[],[f53]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(flattening,[],[f172]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f174]) ).
fof(f178,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f56]) ).
fof(f179,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(flattening,[],[f178]) ).
fof(f180,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(f181,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f180]) ).
fof(f191,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f192,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f191]) ).
fof(f193,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(f194,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,[],[f193]) ).
fof(f197,plain,
! [X0,X1,X2] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f198,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f199,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f198]) ).
fof(f200,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f210,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f75]) ).
fof(f211,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f210]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
? [X4] :
( ~ circle(X3,X0,X1,X2)
| perp(X4,X0,X0,X3) ),
inference(ennf_transformation,[],[f87]) ).
fof(f241,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f242,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(flattening,[],[f241]) ).
fof(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( circle(X0,X2,X7,X16)
& coll(X7,X3,X5)
& coll(X6,X2,X5)
& circle(X0,X2,X6,X15)
& circle(X1,X2,X5,X14)
& coll(X4,X2,X3)
& coll(X4,X0,X1)
& circle(X0,X2,X3,X13)
& circle(X1,X2,X3,X12)
& circle(X0,X2,X10,X11)
& circle(X1,X2,X8,X9)
& ~ perp(X6,X7,X5,X1) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( circle(X0,X2,X7,X16)
& coll(X7,X3,X5)
& coll(X6,X2,X5)
& circle(X0,X2,X6,X15)
& circle(X1,X2,X5,X14)
& coll(X4,X2,X3)
& coll(X4,X0,X1)
& circle(X0,X2,X3,X13)
& circle(X1,X2,X3,X12)
& circle(X0,X2,X10,X11)
& circle(X1,X2,X8,X9)
& ~ perp(X6,X7,X5,X1) ),
inference(flattening,[],[f249]) ).
fof(f262,plain,
! [X0,X1,X2,X3] :
( ~ circle(X3,X0,X1,X2)
| perp(sK11(X0,X1,X2,X3),X0,X0,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X4,sK11(X0,X1,X2,X3))],[f234]) ).
fof(f266,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(sK16(X0,X1,X2,X3,X4),X0,X3,X4)
& coll(sK16(X0,X1,X2,X3,X4),X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X5,sK16(X0,X1,X2,X3,X4))],[f242]) ).
fof(f270,plain,
( circle(sK20,sK22,sK27,sK36)
& coll(sK27,sK23,sK25)
& coll(sK26,sK22,sK25)
& circle(sK20,sK22,sK26,sK35)
& circle(sK21,sK22,sK25,sK34)
& coll(sK24,sK22,sK23)
& coll(sK24,sK20,sK21)
& circle(sK20,sK22,sK23,sK33)
& circle(sK21,sK22,sK23,sK32)
& circle(sK20,sK22,sK30,sK31)
& circle(sK21,sK22,sK28,sK29)
& ~ perp(sK26,sK27,sK25,sK21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25),skolemize(X6,sK26),skolemize(X7,sK27),skolemize(X8,sK28),skolemize(X9,sK29),skolemize(X10,sK30),skolemize(X11,sK31),skolemize(X12,sK32),skolemize(X13,sK33),skolemize(X14,sK34),skolemize(X15,sK35),skolemize(X16,sK36)],[f250]) ).
fof(f271,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f273,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f274,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f275,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f277,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f106]) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f279,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,[],[f109]) ).
fof(f280,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f111]) ).
fof(f281,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f282,plain,
! [X2,X3,X0,X1] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f286,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f119]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f121]) ).
fof(f289,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,[],[f123]) ).
fof(f290,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,[],[f124]) ).
fof(f291,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,[],[f125]) ).
fof(f292,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,[],[f127]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f294,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
fof(f309,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f148]) ).
fof(f310,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f149]) ).
fof(f311,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f150]) ).
fof(f312,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,[],[f152]) ).
fof(f313,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,[],[f154]) ).
fof(f314,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,[],[f156]) ).
fof(f316,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,[],[f160]) ).
fof(f317,plain,
! [X2,X0,X1] :
( ~ cong(X2,X0,X2,X1)
| eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f161]) ).
fof(f319,plain,
! [X2,X3,X0,X1,X4] :
( ~ perp(X3,X0,X0,X4)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(cnf_transformation,[],[f165]) ).
fof(f320,plain,
! [X2,X3,X0,X1,X4] :
( ~ eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| perp(X3,X0,X0,X4) ),
inference(cnf_transformation,[],[f167]) ).
fof(f321,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(cnf_transformation,[],[f169]) ).
fof(f322,plain,
! [X2,X3,X0,X1,X4] :
( ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X4)
| ~ coll(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| midp(X4,X1,X2) ),
inference(cnf_transformation,[],[f171]) ).
fof(f323,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f173]) ).
fof(f324,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f326,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f179]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f181]) ).
fof(f334,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f192]) ).
fof(f335,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,[],[f194]) ).
fof(f337,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f197]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f199]) ).
fof(f339,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f200]) ).
fof(f345,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f211]) ).
fof(f370,plain,
! [X2,X3,X0,X1] :
( ~ circle(X3,X0,X1,X2)
| perp(sK11(X0,X1,X2,X3),X0,X0,X3) ),
inference(cnf_transformation,[],[f262]) ).
fof(f377,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| perp(sK16(X0,X1,X2,X3,X4),X0,X3,X4) ),
inference(cnf_transformation,[],[f266]) ).
fof(f384,plain,
circle(sK20,sK22,sK27,sK36),
inference(cnf_transformation,[],[f270]) ).
fof(f385,plain,
coll(sK27,sK23,sK25),
inference(cnf_transformation,[],[f270]) ).
fof(f386,plain,
coll(sK26,sK22,sK25),
inference(cnf_transformation,[],[f270]) ).
fof(f387,plain,
circle(sK20,sK22,sK26,sK35),
inference(cnf_transformation,[],[f270]) ).
fof(f389,plain,
coll(sK24,sK22,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
coll(sK24,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f393,plain,
circle(sK20,sK22,sK30,sK31),
inference(cnf_transformation,[],[f270]) ).
fof(f394,plain,
circle(sK21,sK22,sK28,sK29),
inference(cnf_transformation,[],[f270]) ).
fof(f395,plain,
~ perp(sK26,sK27,sK25,sK21),
inference(cnf_transformation,[],[f270]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_57,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,[],[f279]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X0,X1,X4,X5)
| ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( circle(X0,X1,X3,X2)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_67,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,[],[f289]) ).
tcf(c_68,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,[],[f290]) ).
tcf(c_69,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,[],[f291]) ).
tcf(c_70,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(X0,X1,X2,X3,X8,X9,X10,X11)
| ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_72,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_87,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,[],[f309]) ).
tcf(c_88,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,[],[f310]) ).
tcf(c_89,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,[],[f311]) ).
tcf(c_90,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,[],[f312]) ).
tcf(c_91,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,[],[f313]) ).
tcf(c_92,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,[],[f314]) ).
tcf(c_94,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,[],[f316]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,X1,X2,X1,X2,X0,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X1,X2,X1,X3,X4,X1,X4,X3)
| ~ circle(X0,X1,X3,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(X4,X0,X0,X1)
| ~ circle(X4,X0,X2,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X0,X3,X2) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X1,X2,X1,X3,X0,X2,X0,X4)
| ~ midp(X4,X2,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X4,X1,X2)
| ~ coll(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X3,X1,X3)
| ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X1,X2,X2,X3)
| ~ coll(X0,X1,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f324]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X2,X0,X3)
| ~ midp(X1,X2,X3)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_105,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,[],[f327]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X1,X3,X2,X4)
| ~ midp(X0,X3,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_113,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,[],[f335]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( perp(X0,X1,X2,X3)
| ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK11(X1,X2,X3,X0),X1,X1,X0)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(sK16(X0,X2,X1,X3,X4),X0,X3,X4)
| ~ coll(X2,X3,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_162,negated_conjecture,
~ perp(sK26,sK27,sK25,sK21),
inference(cnf_transformation,[],[f395]) ).
tcf(c_163,negated_conjecture,
circle(sK21,sK22,sK28,sK29),
inference(cnf_transformation,[],[f394]) ).
tcf(c_164,negated_conjecture,
circle(sK20,sK22,sK30,sK31),
inference(cnf_transformation,[],[f393]) ).
tcf(c_167,negated_conjecture,
coll(sK24,sK20,sK21),
inference(cnf_transformation,[],[f390]) ).
tcf(c_168,negated_conjecture,
coll(sK24,sK22,sK23),
inference(cnf_transformation,[],[f389]) ).
tcf(c_170,negated_conjecture,
circle(sK20,sK22,sK26,sK35),
inference(cnf_transformation,[],[f387]) ).
tcf(c_171,negated_conjecture,
coll(sK26,sK22,sK25),
inference(cnf_transformation,[],[f386]) ).
tcf(c_172,negated_conjecture,
coll(sK27,sK23,sK25),
inference(cnf_transformation,[],[f385]) ).
tcf(c_173,negated_conjecture,
circle(sK20,sK22,sK27,sK36),
inference(cnf_transformation,[],[f384]) ).
tcf(c_179,plain,
( midp(sK22,sK22,sK22)
| ~ coll(sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_183,plain,
( eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_188,plain,
( perp(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_204,plain,
( cyclic(sK22,sK22,sK22,sK22)
| ~ coll(sK22,sK22,sK22)
| ~ eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_237,plain,
( cong(sK22,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK22,sK22)
| ~ eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_277,plain,
( coll(sK26,sK25,sK22)
| ~ coll(sK26,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_282,plain,
( coll(sK22,sK24,sK23)
| ~ coll(sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_325,plain,
coll(sK24,sK21,sK20),
inference(resolution,[status(thm)],[c_49,c_167]) ).
tcf(c_326,plain,
coll(sK24,sK23,sK22),
inference(resolution,[status(thm)],[c_49,c_168]) ).
tcf(c_327,plain,
coll(sK26,sK25,sK22),
inference(resolution,[status(thm)],[c_49,c_171]) ).
tcf(c_329,plain,
( perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21)
| ~ circle(sK21,sK22,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_330,plain,
( perp(sK11(sK22,sK30,sK31,sK20),sK22,sK22,sK20)
| ~ circle(sK20,sK22,sK30,sK31) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_350,plain,
coll(sK24,sK21,sK20),
inference(superposition,[status(thm)],[c_167,c_49]) ).
tcf(c_365,plain,
coll(sK24,sK23,sK22),
inference(superposition,[status(thm)],[c_168,c_49]) ).
tcf(c_366,plain,
coll(sK26,sK25,sK22),
inference(superposition,[status(thm)],[c_171,c_49]) ).
tcf(c_369,plain,
coll(sK27,sK25,sK23),
inference(superposition,[status(thm)],[c_172,c_49]) ).
tcf(c_376,plain,
coll(sK22,sK24,sK23),
inference(resolution,[status(thm)],[c_50,c_168]) ).
tcf(c_377,plain,
coll(sK22,sK26,sK25),
inference(resolution,[status(thm)],[c_50,c_171]) ).
tcf(c_384,plain,
coll(sK20,sK24,sK21),
inference(superposition,[status(thm)],[c_167,c_50]) ).
tcf(c_385,plain,
coll(sK22,sK24,sK23),
inference(superposition,[status(thm)],[c_168,c_50]) ).
tcf(c_388,plain,
coll(sK21,sK24,sK20),
inference(superposition,[status(thm)],[c_350,c_50]) ).
tcf(c_390,plain,
coll(sK25,sK26,sK22),
inference(superposition,[status(thm)],[c_366,c_50]) ).
tcf(c_397,plain,
coll(sK20,sK21,sK24),
inference(superposition,[status(thm)],[c_384,c_49]) ).
tcf(c_433,plain,
! [X0: $i] :
( coll(X0,sK22,sK26)
| ~ coll(sK26,sK25,sK22)
| ~ coll(sK26,sK25,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_434,plain,
( coll(sK22,sK22,sK26)
| ~ coll(sK26,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_433]) ).
tcf(c_465,plain,
! [X0: $i] :
( coll(X0,sK23,sK22)
| ~ coll(sK22,sK24,sK23)
| ~ coll(sK22,sK24,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_502,plain,
( perp(sK22,sK21,sK11(sK22,sK28,sK29,sK21),sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_503,plain,
( perp(sK11(sK22,sK28,sK29,sK21),sK22,sK21,sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_505,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK22,sK21)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21)
| ~ perp(X0,X1,sK11(sK22,sK28,sK29,sK21),sK22) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_509,plain,
! [X0: $i,X1: $i] :
( perp(sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,X0,X1),sK11(sK22,sK28,sK29,sK21),X0,X1)
| ~ coll(sK21,X0,X1)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_156]) ).
tcf(c_512,plain,
( perp(sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,sK22,sK22),sK11(sK22,sK28,sK29,sK21),sK22,sK22)
| ~ coll(sK21,sK22,sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_509]) ).
tcf(c_582,plain,
( perp(sK22,sK20,sK11(sK22,sK30,sK31,sK20),sK22)
| ~ perp(sK11(sK22,sK30,sK31,sK20),sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK22,sK20)
| ~ perp(sK11(sK22,sK30,sK31,sK20),sK22,sK22,sK20)
| ~ perp(X0,X1,sK11(sK22,sK30,sK31,sK20),sK22) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_612,plain,
! [X0: $i] :
( coll(sK21,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_167,c_51]) ).
tcf(c_613,plain,
! [X0: $i] :
( coll(sK23,X0,sK24)
| ~ coll(sK24,sK22,X0) ),
inference(superposition,[status(thm)],[c_168,c_51]) ).
tcf(c_615,plain,
! [X0: $i] :
( coll(sK25,X0,sK27)
| ~ coll(sK27,sK23,X0) ),
inference(superposition,[status(thm)],[c_172,c_51]) ).
tcf(c_616,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK21,X0) ),
inference(superposition,[status(thm)],[c_350,c_51]) ).
tcf(c_617,plain,
! [X0: $i] :
( coll(sK22,X0,sK24)
| ~ coll(sK24,sK23,X0) ),
inference(superposition,[status(thm)],[c_365,c_51]) ).
tcf(c_619,plain,
! [X0: $i] :
( coll(sK23,X0,sK27)
| ~ coll(sK27,sK25,X0) ),
inference(superposition,[status(thm)],[c_369,c_51]) ).
tcf(c_621,plain,
! [X0: $i] :
( coll(sK23,X0,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(superposition,[status(thm)],[c_385,c_51]) ).
tcf(c_624,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK24,X0) ),
inference(superposition,[status(thm)],[c_388,c_51]) ).
tcf(c_626,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK26,X0) ),
inference(superposition,[status(thm)],[c_390,c_51]) ).
tcf(c_631,plain,
( coll(sK22,sK22,sK25)
| ~ coll(sK25,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_626]) ).
tcf(c_752,plain,
! [X0: $i] :
( coll(X0,sK21,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(resolution,[status(thm)],[c_51,c_167]) ).
tcf(c_754,plain,
! [X0: $i] :
( coll(X0,sK23,sK24)
| ~ coll(sK24,sK22,X0) ),
inference(resolution,[status(thm)],[c_51,c_168]) ).
tcf(c_755,plain,
! [X0: $i] :
( coll(X0,sK25,sK26)
| ~ coll(sK26,sK22,X0) ),
inference(resolution,[status(thm)],[c_51,c_171]) ).
tcf(c_756,plain,
! [X0: $i] :
( coll(X0,sK25,sK27)
| ~ coll(sK27,sK23,X0) ),
inference(resolution,[status(thm)],[c_51,c_172]) ).
tcf(c_758,plain,
! [X0: $i] :
( coll(X0,sK20,sK24)
| ~ coll(sK24,sK21,X0) ),
inference(resolution,[status(thm)],[c_51,c_325]) ).
tcf(c_760,plain,
! [X0: $i] :
( coll(X0,sK22,sK24)
| ~ coll(sK24,sK23,X0) ),
inference(resolution,[status(thm)],[c_51,c_326]) ).
tcf(c_761,plain,
! [X0: $i] :
( coll(X0,sK22,sK26)
| ~ coll(sK26,sK25,X0) ),
inference(resolution,[status(thm)],[c_51,c_327]) ).
tcf(c_766,plain,
! [X0: $i] :
( coll(X0,sK23,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(resolution,[status(thm)],[c_51,c_376]) ).
tcf(c_768,plain,
! [X0: $i] :
( coll(X0,sK25,sK22)
| ~ coll(sK22,sK26,X0) ),
inference(resolution,[status(thm)],[c_51,c_377]) ).
tcf(c_848,plain,
coll(sK21,sK21,sK24),
inference(resolution,[status(thm)],[c_752,c_167]) ).
tcf(c_853,plain,
! [X0: $i] :
( coll(X0,sK24,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(resolution,[status(thm)],[c_848,c_51]) ).
tcf(c_859,plain,
coll(sK23,sK23,sK24),
inference(resolution,[status(thm)],[c_754,c_168]) ).
tcf(c_860,plain,
! [X0: $i] :
( coll(sK24,X0,sK20)
| ~ coll(sK20,sK21,X0) ),
inference(superposition,[status(thm)],[c_397,c_51]) ).
tcf(c_898,plain,
! [X0: $i] :
( coll(X0,sK24,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(resolution,[status(thm)],[c_859,c_51]) ).
tcf(c_911,plain,
coll(sK25,sK25,sK26),
inference(resolution,[status(thm)],[c_755,c_171]) ).
tcf(c_916,plain,
! [X0: $i] :
( coll(X0,sK26,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(resolution,[status(thm)],[c_911,c_51]) ).
tcf(c_929,plain,
coll(sK25,sK25,sK27),
inference(resolution,[status(thm)],[c_756,c_172]) ).
tcf(c_1081,plain,
coll(sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_167,c_612]) ).
tcf(c_1102,plain,
! [X0: $i] :
( coll(sK24,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_1081,c_51]) ).
tcf(c_1152,plain,
coll(sK23,sK23,sK24),
inference(superposition,[status(thm)],[c_168,c_613]) ).
tcf(c_1153,plain,
! [X0: $i] :
( coll(sK24,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_1152,c_51]) ).
tcf(c_1222,plain,
coll(sK22,sK22,sK24),
inference(resolution,[status(thm)],[c_760,c_326]) ).
tcf(c_1267,plain,
coll(sK22,sK24,sK22),
inference(resolution,[status(thm)],[c_1222,c_49]) ).
tcf(c_1287,plain,
coll(sK25,sK25,sK27),
inference(superposition,[status(thm)],[c_172,c_615]) ).
tcf(c_1293,plain,
! [X0: $i] :
( coll(sK27,X0,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(superposition,[status(thm)],[c_1287,c_51]) ).
tcf(c_1296,plain,
( coll(sK27,sK22,sK25)
| ~ coll(sK25,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_1293]) ).
tcf(c_1381,plain,
coll(sK23,sK23,sK22),
inference(resolution,[status(thm)],[c_766,c_376]) ).
tcf(c_1415,plain,
coll(sK25,sK25,sK22),
inference(resolution,[status(thm)],[c_768,c_377]) ).
tcf(c_1509,plain,
( perp(sK21,sK22,sK11(sK22,sK28,sK29,sK21),sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_1512,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK21,sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK21,sK22)
| ~ perp(X0,X1,sK11(sK22,sK28,sK29,sK21),sK22) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_1566,plain,
coll(sK24,sK24,sK21),
inference(resolution,[status(thm)],[c_853,c_848]) ).
tcf(c_1586,plain,
coll(sK24,sK21,sK24),
inference(resolution,[status(thm)],[c_1566,c_49]) ).
tcf(c_1594,plain,
coll(sK24,sK24,sK23),
inference(resolution,[status(thm)],[c_898,c_859]) ).
tcf(c_1615,plain,
coll(sK24,sK23,sK24),
inference(resolution,[status(thm)],[c_1594,c_49]) ).
tcf(c_1622,plain,
coll(sK26,sK26,sK25),
inference(resolution,[status(thm)],[c_916,c_911]) ).
tcf(c_1624,plain,
coll(sK27,sK26,sK25),
inference(resolution,[status(thm)],[c_916,c_929]) ).
tcf(c_1652,plain,
coll(sK26,sK25,sK26),
inference(resolution,[status(thm)],[c_1622,c_49]) ).
tcf(c_1666,plain,
coll(sK27,sK25,sK26),
inference(resolution,[status(thm)],[c_1624,c_49]) ).
tcf(c_1667,plain,
coll(sK26,sK27,sK25),
inference(resolution,[status(thm)],[c_1624,c_50]) ).
tcf(c_1670,plain,
coll(sK22,sK22,sK24),
inference(superposition,[status(thm)],[c_365,c_617]) ).
tcf(c_1698,plain,
coll(sK22,sK24,sK22),
inference(superposition,[status(thm)],[c_1670,c_49]) ).
tcf(c_1717,plain,
! [X0: $i] :
( coll(sK22,X0,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(superposition,[status(thm)],[c_1698,c_51]) ).
tcf(c_1720,plain,
( coll(sK22,sK22,sK22)
| ~ coll(sK22,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_1717]) ).
tcf(c_1863,plain,
coll(sK23,sK23,sK27),
inference(superposition,[status(thm)],[c_369,c_619]) ).
tcf(c_1887,plain,
! [X0: $i] :
( coll(sK27,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_1863,c_51]) ).
tcf(c_1890,plain,
( coll(sK27,sK22,sK23)
| ~ coll(sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_1887]) ).
tcf(c_1987,plain,
coll(sK24,sK20,sK24),
inference(resolution,[status(thm)],[c_1586,c_758]) ).
tcf(c_2032,plain,
coll(sK24,sK22,sK24),
inference(resolution,[status(thm)],[c_1615,c_760]) ).
tcf(c_2061,plain,
coll(sK26,sK22,sK26),
inference(resolution,[status(thm)],[c_1652,c_761]) ).
tcf(c_2086,plain,
! [X0: $i] :
( coll(X0,sK26,sK27)
| ~ coll(sK27,sK25,X0) ),
inference(resolution,[status(thm)],[c_1666,c_51]) ).
tcf(c_2097,plain,
! [X0: $i] :
( coll(sK27,sK23,X0)
| ~ coll(sK27,X0,sK23) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2098,plain,
( coll(sK27,sK23,sK22)
| ~ coll(sK27,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_2097]) ).
tcf(c_2101,plain,
! [X0: $i] :
( coll(sK27,sK25,X0)
| ~ coll(sK27,X0,sK25) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2102,plain,
( coll(sK27,sK25,sK22)
| ~ coll(sK27,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_2101]) ).
tcf(c_2103,plain,
! [X0: $i] :
( coll(sK20,sK24,X0)
| ~ coll(sK20,X0,sK24) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2104,plain,
( coll(sK20,sK24,sK22)
| ~ coll(sK20,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_2103]) ).
tcf(c_2121,plain,
( para(sK22,sK21,sK22,sK21)
| ~ perp(sK22,sK21,sK11(sK22,sK28,sK29,sK21),sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_505]) ).
tcf(c_2122,plain,
( para(sK22,sK20,sK22,sK20)
| ~ perp(sK22,sK20,sK11(sK22,sK30,sK31,sK20),sK22)
| ~ perp(sK11(sK22,sK30,sK31,sK20),sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_585]) ).
tcf(c_2206,plain,
coll(sK26,sK25,sK27),
inference(resolution,[status(thm)],[c_1667,c_49]) ).
tcf(c_2461,plain,
coll(sK20,sK24,sK24),
inference(resolution,[status(thm)],[c_1987,c_50]) ).
tcf(c_2496,plain,
coll(sK24,sK24,sK22),
inference(resolution,[status(thm)],[c_2032,c_49]) ).
tcf(c_2836,plain,
! [X0: $i,X1: $i] :
( coll(sK20,X1,X0)
| ~ coll(sK20,X0,X1) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2852,plain,
( coll(sK20,sK23,sK22)
| ~ coll(sK22,sK24,sK23)
| ~ coll(sK22,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_3005,plain,
coll(sK24,sK24,sK21),
inference(superposition,[status(thm)],[c_1081,c_1102]) ).
tcf(c_3013,plain,
! [X0: $i] :
( coll(sK21,X0,sK24)
| ~ coll(sK24,sK24,X0) ),
inference(superposition,[status(thm)],[c_3005,c_51]) ).
tcf(c_3015,plain,
coll(sK24,sK21,sK24),
inference(superposition,[status(thm)],[c_3005,c_49]) ).
tcf(c_3033,plain,
( perp(sK22,sK27,sK27,sK36)
| ~ coll(sK20,sK22,sK36) ),
inference(resolution,[status(thm)],[c_102,c_173]) ).
tcf(c_3181,plain,
coll(sK20,sK24,sK24),
inference(superposition,[status(thm)],[c_3015,c_616]) ).
tcf(c_3229,plain,
coll(sK24,sK20,sK24),
inference(superposition,[status(thm)],[c_3181,c_50]) ).
tcf(c_3353,plain,
coll(sK24,sK24,sK20),
inference(superposition,[status(thm)],[c_3229,c_49]) ).
tcf(c_3397,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK24,X0) ),
inference(superposition,[status(thm)],[c_3353,c_51]) ).
tcf(c_3400,plain,
( coll(sK20,sK22,sK24)
| ~ coll(sK24,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_3397]) ).
tcf(c_3843,plain,
coll(sK24,sK24,sK23),
inference(superposition,[status(thm)],[c_1152,c_1153]) ).
tcf(c_3845,plain,
coll(sK24,sK27,sK23),
inference(superposition,[status(thm)],[c_1863,c_1153]) ).
tcf(c_3901,plain,
coll(sK24,sK23,sK27),
inference(superposition,[status(thm)],[c_3845,c_49]) ).
tcf(c_4042,plain,
coll(sK22,sK27,sK24),
inference(superposition,[status(thm)],[c_3901,c_617]) ).
tcf(c_4092,plain,
coll(sK22,sK24,sK27),
inference(superposition,[status(thm)],[c_4042,c_49]) ).
tcf(c_4262,plain,
coll(sK27,sK22,sK26),
inference(resolution,[status(thm)],[c_2206,c_761]) ).
tcf(c_4266,plain,
coll(sK23,sK27,sK22),
inference(superposition,[status(thm)],[c_4092,c_621]) ).
tcf(c_4294,plain,
coll(sK27,sK23,sK22),
inference(superposition,[status(thm)],[c_4266,c_50]) ).
tcf(c_4538,plain,
! [X0: $i] :
( coll(sK22,X0,sK27)
| ~ coll(sK27,sK23,X0) ),
inference(superposition,[status(thm)],[c_4294,c_51]) ).
tcf(c_4542,plain,
( coll(sK22,sK22,sK27)
| ~ coll(sK27,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_4538]) ).
tcf(c_4619,plain,
! [X0: $i] :
( coll(X0,sK24,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(resolution,[status(thm)],[c_2461,c_51]) ).
tcf(c_4620,plain,
( coll(sK22,sK24,sK20)
| ~ coll(sK20,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_4619]) ).
tcf(c_5170,plain,
! [X0: $i,X1: $i] :
( coll(sK21,X0,X1)
| ~ para(sK21,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_5171,plain,
( coll(sK21,sK22,sK22)
| ~ para(sK21,sK22,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_5170]) ).
tcf(c_5493,plain,
! [X0: $i,X1: $i] :
( perp(sK26,sK27,sK25,sK21)
| ~ perp(X0,X1,sK25,sK21)
| ~ para(sK26,sK27,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_5494,plain,
( perp(sK26,sK27,sK25,sK21)
| ~ perp(sK22,sK22,sK25,sK21)
| ~ para(sK26,sK27,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_5493]) ).
tcf(c_6070,plain,
! [X0: $i] :
( eqangle(sK22,X0,sK22,sK26,sK35,sK22,sK35,sK26)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_97,c_170]) ).
tcf(c_6072,plain,
! [X0: $i] :
( eqangle(sK22,X0,sK22,sK27,sK36,sK22,sK36,sK27)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_97,c_173]) ).
tcf(c_7109,plain,
( para(sK21,sK22,sK21,sK22)
| ~ perp(sK21,sK22,sK11(sK22,sK28,sK29,sK21),sK22)
| ~ perp(sK11(sK22,sK28,sK29,sK21),sK22,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_1512]) ).
tcf(c_7820,plain,
coll(sK26,sK26,sK27),
inference(resolution,[status(thm)],[c_2086,c_1666]) ).
tcf(c_7824,plain,
coll(sK26,sK27,sK26),
inference(resolution,[status(thm)],[c_7820,c_49]) ).
tcf(c_9070,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,X0,X1),sK11(sK22,sK28,sK29,sK21))
| ~ perp(sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,X0,X1),sK11(sK22,sK28,sK29,sK21),X0,X1) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_9072,plain,
( perp(sK22,sK22,sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,sK22,sK22),sK11(sK22,sK28,sK29,sK21))
| ~ perp(sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,sK22,sK22),sK11(sK22,sK28,sK29,sK21),sK22,sK22) ),
inference(instantiation,[status(thm)],[c_9070]) ).
tcf(c_9644,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ perp(X2,X3,sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,X0,X1),sK11(sK22,sK28,sK29,sK21))
| ~ perp(sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,X0,X1),sK11(sK22,sK28,sK29,sK21),X0,X1) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_9645,plain,
( para(sK22,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,sK22,sK22),sK11(sK22,sK28,sK29,sK21))
| ~ perp(sK16(sK11(sK22,sK28,sK29,sK21),sK21,sK22,sK22,sK22),sK11(sK22,sK28,sK29,sK21),sK22,sK22) ),
inference(instantiation,[status(thm)],[c_9644]) ).
tcf(c_10229,plain,
coll(sK27,sK27,sK25),
inference(superposition,[status(thm)],[c_1287,c_1293]) ).
tcf(c_10238,plain,
coll(sK27,sK25,sK27),
inference(superposition,[status(thm)],[c_10229,c_49]) ).
tcf(c_10243,plain,
! [X0: $i] :
( coll(sK27,X0,sK27)
| ~ coll(sK27,sK25,X0) ),
inference(superposition,[status(thm)],[c_10238,c_51]) ).
tcf(c_10247,plain,
( coll(sK27,sK22,sK27)
| ~ coll(sK27,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_10243]) ).
tcf(c_12687,plain,
( perp(sK22,sK27,sK36,sK27)
| ~ coll(sK20,sK22,sK36) ),
inference(resolution,[status(thm)],[c_3033,c_55]) ).
tcf(c_14586,plain,
coll(sK21,sK23,sK24),
inference(superposition,[status(thm)],[c_3843,c_3013]) ).
tcf(c_14604,plain,
coll(sK21,sK24,sK23),
inference(superposition,[status(thm)],[c_14586,c_49]) ).
tcf(c_14932,plain,
coll(sK20,sK23,sK21),
inference(superposition,[status(thm)],[c_14604,c_624]) ).
tcf(c_14943,plain,
( coll(sK20,sK22,sK36)
| ~ coll(sK20,sK36,sK22) ),
inference(instantiation,[status(thm)],[c_2836]) ).
tcf(c_15078,plain,
coll(sK20,sK21,sK23),
inference(superposition,[status(thm)],[c_14932,c_49]) ).
tcf(c_15550,plain,
coll(sK24,sK23,sK20),
inference(superposition,[status(thm)],[c_15078,c_860]) ).
tcf(c_15567,plain,
coll(sK22,sK20,sK24),
inference(superposition,[status(thm)],[c_15550,c_617]) ).
tcf(c_15605,plain,
coll(sK22,sK24,sK20),
inference(superposition,[status(thm)],[c_15567,c_49]) ).
tcf(c_15666,plain,
! [X0: $i] :
( perp(sK20,sK22,sK22,X0)
| ~ perp(sK22,X0,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_15667,plain,
( perp(sK20,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_15666]) ).
tcf(c_15687,plain,
coll(sK23,sK20,sK22),
inference(superposition,[status(thm)],[c_15605,c_621]) ).
tcf(c_20624,plain,
coll(sK20,sK23,sK22),
inference(superposition,[status(thm)],[c_15687,c_50]) ).
tcf(c_20630,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_20624,c_51]) ).
tcf(c_20633,plain,
( coll(sK22,sK22,sK20)
| ~ coll(sK20,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_20630]) ).
tcf(c_22579,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK27,X0,X1)
| ~ para(X0,X1,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_22580,plain,
( para(sK26,sK27,sK22,sK22)
| ~ para(sK22,sK22,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_22579]) ).
tcf(c_22779,plain,
( cong(sK22,sK21,sK22,sK21)
| ~ midp(sK22,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_22784,plain,
( cong(sK22,sK20,sK22,sK20)
| ~ midp(sK22,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_24456,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK25,sK21)
| ~ cong(X0,sK21,X1,sK21)
| ~ cong(X0,sK25,X1,sK25) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_24457,plain,
( perp(sK22,sK22,sK25,sK21)
| ~ cong(sK22,sK21,sK22,sK21)
| ~ cong(sK22,sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_24456]) ).
tcf(c_24537,plain,
! [X0: $i] :
( perp(sK22,X0,sK20,sK22)
| ~ cong(sK22,sK20,X0,sK20)
| ~ cong(sK22,sK22,X0,sK22) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_24538,plain,
( perp(sK22,sK22,sK20,sK22)
| ~ cong(sK22,sK20,sK22,sK20)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_24537]) ).
tcf(c_27634,plain,
! [X0: $i,X1: $i] :
( midp(sK22,sK21,sK21)
| ~ midp(sK22,X0,X1)
| ~ para(X0,sK21,X1,sK21) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_27635,plain,
( midp(sK22,sK21,sK21)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_27634]) ).
tcf(c_27667,plain,
! [X0: $i,X1: $i] :
( midp(sK22,sK20,sK20)
| ~ midp(sK22,X0,X1)
| ~ para(X0,sK20,X1,sK20) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_27668,plain,
( midp(sK22,sK20,sK20)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK20,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_27667]) ).
tcf(c_28459,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK22,sK36)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK36,X1,sK22)
| ~ para(X0,sK22,X1,sK36) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_28460,plain,
( midp(sK22,sK22,sK36)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK36,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK36) ),
inference(instantiation,[status(thm)],[c_28459]) ).
tcf(c_31623,plain,
! [X0: $i] :
( cong(X0,sK25,X0,sK25)
| ~ midp(X0,sK25,sK25) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_31624,plain,
( cong(sK22,sK25,sK22,sK25)
| ~ midp(sK22,sK25,sK25) ),
inference(instantiation,[status(thm)],[c_31623]) ).
tcf(c_31817,plain,
! [X0: $i] :
( eqangle(sK22,sK26,sK22,X0,sK35,sK26,sK35,sK22)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_67,c_6070]) ).
tcf(c_31867,plain,
! [X0: $i] :
( eqangle(sK35,sK22,sK35,sK26,sK22,X0,sK22,sK26)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_68,c_6070]) ).
tcf(c_31869,plain,
! [X0: $i] :
( eqangle(sK36,sK22,sK36,sK27,sK22,X0,sK22,sK27)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_68,c_6072]) ).
tcf(c_32030,plain,
! [X0: $i] :
( eqangle(sK22,X0,sK36,sK22,sK22,sK27,sK36,sK27)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_69,c_6072]) ).
tcf(c_32360,plain,
! [X0: $i] :
( eqangle(sK35,sK26,sK35,sK22,sK22,sK26,sK22,X0)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_31817,c_68]) ).
tcf(c_32363,plain,
( eqangle(sK35,sK26,sK35,sK22,sK22,sK26,sK22,sK22)
| ~ perp(sK20,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_32360]) ).
tcf(c_32889,plain,
( cyclic(sK22,sK26,sK35,sK22)
| ~ coll(sK35,sK22,sK26)
| ~ perp(sK20,sK22,sK22,sK22) ),
inference(resolution,[status(thm)],[c_91,c_31867]) ).
tcf(c_33659,plain,
! [X0: $i] :
( perp(sK22,X0,sK36,sK22)
| ~ perp(sK22,sK27,sK36,sK27)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_32030,c_123]) ).
tcf(c_33660,plain,
( perp(sK22,sK22,sK36,sK22)
| ~ perp(sK20,sK22,sK22,sK22)
| ~ perp(sK22,sK27,sK36,sK27) ),
inference(instantiation,[status(thm)],[c_33659]) ).
tcf(c_36361,plain,
( midp(sK27,sK22,sK27)
| ~ coll(sK27,sK22,sK27)
| ~ circle(sK22,sK36,sK22,sK27)
| ~ perp(sK20,sK22,sK22,sK22) ),
inference(resolution,[status(thm)],[c_100,c_31869]) ).
tcf(c_36799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK26,sK27)
| ~ eqangle(X0,X1,X2,X3,sK26,sK27,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_36806,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X1,X2,sK26,sK27)
| ~ midp(X0,X2,sK27)
| ~ midp(X0,X1,sK26) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_36895,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK27,X3,X2)
| ~ coll(sK27,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK27,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_36934,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK27,X1)
| ~ midp(X0,X1,sK27) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_36935,plain,
( midp(sK22,sK27,sK22)
| ~ midp(sK22,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_36934]) ).
tcf(c_37234,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,X7,X5,X7,X6)
| ~ cyclic(X5,X6,X4,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X4,X6) ),
inference(resolution,[status(thm)],[c_70,c_89]) ).
tcf(c_37247,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X0,X1,X2,X3,sK36,sK22,sK36,sK27)
| ~ perp(sK20,sK22,sK22,X4)
| ~ eqangle(X0,X1,X2,X3,sK22,X4,sK22,sK27) ),
inference(resolution,[status(thm)],[c_70,c_6072]) ).
tcf(c_37599,plain,
! [X0: $i,X1: $i] :
( midp(X0,X1,sK27)
| ~ coll(X0,X1,sK27)
| ~ cong(X0,X1,X0,sK27) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_37600,plain,
( midp(sK22,sK22,sK27)
| ~ coll(sK22,sK22,sK27)
| ~ cong(sK22,sK22,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_37599]) ).
tcf(c_38771,plain,
! [X0: $i] :
( cong(sK26,sK27,sK26,X0)
| ~ midp(sK26,sK27,X0) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_39407,plain,
( para(sK26,sK26,sK26,sK27)
| ~ eqangle(sK26,sK26,sK26,sK27,sK26,sK27,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_36799]) ).
tcf(c_39408,plain,
( eqangle(sK26,sK26,sK26,sK27,sK26,sK27,sK26,sK27)
| ~ cong(sK26,sK26,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_40467,plain,
! [X0: $i,X1: $i] :
( para(X0,sK27,X0,X1)
| ~ para(X0,X1,X0,sK27) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_40469,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK27,X0,X3)
| ~ eqangle(X0,sK27,X1,X2,X0,X3,X1,X2) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_40486,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK26,X0,X3)
| ~ eqangle(X0,sK26,X1,X2,X0,X3,X1,X2) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_40587,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK26,X2,sK26)
| ~ coll(sK26,X2,sK26)
| ~ midp(X0,X2,X1)
| ~ para(X0,sK26,X1,sK26) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_40588,plain,
( midp(sK26,sK22,sK26)
| ~ midp(sK22,sK22,sK22)
| ~ coll(sK26,sK22,sK26)
| ~ para(sK22,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_40587]) ).
tcf(c_41522,plain,
! [X0: $i,X1: $i,X2: $i] :
( circle(X0,X1,sK27,X2)
| ~ cong(X0,X1,X0,sK27)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_41523,plain,
( circle(sK22,sK22,sK27,sK22)
| ~ cong(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_41522]) ).
tcf(c_42606,plain,
( cong(sK26,sK26,sK26,sK27)
| ~ cong(sK26,sK27,sK26,sK26) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_43792,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK25,sK25)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK25,X1,sK25) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_43793,plain,
( midp(sK22,sK25,sK25)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_43792]) ).
tcf(c_45920,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,X0,sK22,sK26,X1,sK22,X1,sK26)
| ~ cyclic(sK22,sK26,sK35,X1)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_37234,c_6070]) ).
tcf(c_45921,plain,
( eqangle(sK22,sK22,sK22,sK26,sK22,sK22,sK22,sK26)
| ~ cyclic(sK22,sK26,sK35,sK22)
| ~ perp(sK20,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_45920]) ).
tcf(c_45945,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK26,sK22,X0,X1,sK26,X1,sK22)
| ~ cyclic(sK26,sK22,sK35,X1)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_37234,c_31817]) ).
tcf(c_45946,plain,
( eqangle(sK22,sK26,sK22,sK22,sK22,sK26,sK22,sK22)
| ~ cyclic(sK26,sK22,sK35,sK22)
| ~ perp(sK20,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_45945]) ).
tcf(c_48227,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK26,X0,X1,X2)
| ~ cyclic(X0,sK26,X1,X2) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_48228,plain,
( cyclic(sK26,sK22,sK22,sK22)
| ~ cyclic(sK22,sK26,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_48227]) ).
tcf(c_48369,plain,
! [X0: $i] :
( coll(sK27,sK27,sK36)
| ~ coll(sK36,X0,sK27) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_48370,plain,
( coll(sK27,sK27,sK36)
| ~ coll(sK36,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_48369]) ).
tcf(c_48872,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X1,sK36,X4)
| ~ eqangle(X0,X1,X2,X3,sK36,X4,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_48874,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X1,sK36,X4)
| ~ perp(X2,X3,sK36,X4)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_48875,plain,
( para(sK22,sK22,sK36,sK22)
| ~ perp(sK22,sK22,sK36,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_48874]) ).
tcf(c_52125,plain,
! [X0: $i,X1: $i] :
( para(X0,sK27,X0,sK27)
| ~ eqangle(X0,sK27,X0,X1,X0,sK27,X0,X1) ),
inference(instantiation,[status(thm)],[c_40469]) ).
tcf(c_52127,plain,
( para(sK22,sK27,sK22,sK27)
| ~ eqangle(sK22,sK27,sK22,sK22,sK22,sK27,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_52125]) ).
tcf(c_52874,plain,
! [X0: $i,X1: $i] :
( para(X0,sK26,X0,sK26)
| ~ eqangle(X0,sK26,X0,X1,X0,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_40486]) ).
tcf(c_52875,plain,
! [X0: $i,X1: $i] :
( eqangle(X1,sK26,X1,X0,X1,sK26,X1,X0)
| ~ cyclic(sK26,X0,X1,X1) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_52876,plain,
( para(sK22,sK26,sK22,sK26)
| ~ eqangle(sK22,sK26,sK22,sK22,sK22,sK26,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_52874]) ).
tcf(c_52877,plain,
( eqangle(sK22,sK26,sK22,sK22,sK22,sK26,sK22,sK22)
| ~ cyclic(sK26,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_52875]) ).
tcf(c_55057,plain,
( coll(sK27,sK36,sK27)
| ~ coll(sK27,sK27,sK36) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_55775,plain,
! [X0: $i] :
( coll(sK36,X0,sK27)
| ~ coll(sK36,sK27,X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_55776,plain,
( coll(sK36,sK22,sK27)
| ~ coll(sK36,sK27,sK22) ),
inference(instantiation,[status(thm)],[c_55775]) ).
tcf(c_57842,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,X1,X2,sK36)
| ~ para(X0,X1,sK36,X2) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_57843,plain,
( para(sK22,sK22,sK22,sK36)
| ~ para(sK22,sK22,sK36,sK22) ),
inference(instantiation,[status(thm)],[c_57842]) ).
tcf(c_58729,plain,
! [X0: $i,X1: $i] :
( para(sK36,X0,sK36,X0)
| ~ eqangle(sK36,X0,sK36,X1,sK36,X0,sK36,X1) ),
inference(instantiation,[status(thm)],[c_48872]) ).
tcf(c_58993,plain,
! [X0: $i] :
( coll(sK20,sK36,sK22)
| ~ coll(sK22,X0,sK36)
| ~ coll(sK22,X0,sK20) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_58994,plain,
( coll(sK20,sK36,sK22)
| ~ coll(sK22,sK22,sK36)
| ~ coll(sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_58993]) ).
tcf(c_59442,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK36,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK36,X2,X1)
| ~ para(X0,X1,X2,sK36) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_59443,plain,
( midp(sK22,sK36,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK36,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK36) ),
inference(instantiation,[status(thm)],[c_59442]) ).
tcf(c_63501,plain,
! [X0: $i,X1: $i] :
( coll(sK36,sK27,X0)
| ~ coll(X0,X1,sK36)
| ~ coll(X0,X1,sK27) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_63502,plain,
( coll(sK36,sK27,sK22)
| ~ coll(sK22,sK22,sK36)
| ~ coll(sK22,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_63501]) ).
tcf(c_64463,plain,
! [X0: $i,X1: $i] :
( coll(sK22,X1,sK36)
| ~ coll(sK36,X0,sK22)
| ~ coll(sK36,X0,X1) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_64464,plain,
( coll(sK22,sK22,sK36)
| ~ coll(sK36,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_64463]) ).
tcf(c_71923,plain,
! [X0: $i] :
( para(sK22,sK36,sK22,X0)
| ~ para(sK22,X0,sK22,sK36) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_71924,plain,
( para(sK22,sK36,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK36) ),
inference(instantiation,[status(thm)],[c_71923]) ).
tcf(c_73408,plain,
! [X0: $i,X1: $i] :
( coll(sK35,X1,sK26)
| cyclic(sK26,X0,sK35,X1)
| ~ eqangle(sK35,sK26,sK35,X0,X1,sK26,X1,X0) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_73409,plain,
( coll(sK35,sK22,sK26)
| cyclic(sK26,sK22,sK35,sK22)
| ~ eqangle(sK35,sK26,sK35,sK22,sK22,sK26,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_73408]) ).
tcf(c_75602,plain,
! [X0: $i] :
( cong(sK22,X0,sK27,X0)
| ~ coll(sK20,sK22,sK36)
| ~ midp(X0,sK22,sK36) ),
inference(resolution,[status(thm)],[c_101,c_3033]) ).
tcf(c_75849,plain,
( cong(sK22,sK36,sK22,sK27)
| ~ midp(sK27,sK36,sK27)
| ~ coll(sK20,sK22,sK36) ),
inference(resolution,[status(thm)],[c_104,c_12687]) ).
tcf(c_77957,plain,
! [X0: $i] :
( coll(sK36,X0,sK22)
| ~ para(sK36,X0,sK36,sK22) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_77960,plain,
( coll(sK36,sK22,sK22)
| ~ para(sK36,sK22,sK36,sK22) ),
inference(instantiation,[status(thm)],[c_77957]) ).
tcf(c_78150,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X3,X1,X1,X1)
| ~ midp(X2,X1,X2)
| ~ circle(X3,X1,X2,X0)
| ~ circle(X0,X1,X1,X2) ),
inference(resolution,[status(thm)],[c_99,c_98]) ).
tcf(c_79524,plain,
! [X0: $i] :
( cong(sK22,X0,X0,sK27)
| ~ coll(sK20,sK22,sK36)
| ~ midp(X0,sK22,sK36) ),
inference(resolution,[status(thm)],[c_75602,c_71]) ).
tcf(c_79527,plain,
( cong(sK22,sK22,sK22,sK27)
| ~ midp(sK22,sK22,sK36)
| ~ coll(sK20,sK22,sK36) ),
inference(instantiation,[status(thm)],[c_79524]) ).
tcf(c_79802,plain,
! [X0: $i,X1: $i] :
( circle(X0,sK36,X1,sK27)
| ~ cong(X0,sK36,X0,sK27)
| ~ cong(X0,sK36,X0,X1) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_79803,plain,
( circle(sK22,sK36,sK22,sK27)
| ~ cong(sK22,sK36,sK22,sK22)
| ~ cong(sK22,sK36,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_79802]) ).
tcf(c_81797,plain,
! [X0: $i] :
( para(sK36,X0,sK36,X0)
| ~ eqangle(sK36,X0,sK36,sK27,sK36,X0,sK36,sK27) ),
inference(instantiation,[status(thm)],[c_58729]) ).
tcf(c_81799,plain,
( para(sK36,sK22,sK36,sK22)
| ~ eqangle(sK36,sK22,sK36,sK27,sK36,sK22,sK36,sK27) ),
inference(instantiation,[status(thm)],[c_81797]) ).
tcf(c_83054,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK36,X0,X1)
| ~ midp(X0,sK36,X1) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_83055,plain,
( cong(sK22,sK36,sK22,sK22)
| ~ midp(sK22,sK36,sK22) ),
inference(instantiation,[status(thm)],[c_83054]) ).
tcf(c_94866,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,sK27,X1,X2,X0,sK27,X0,X3)
| ~ midp(X3,sK27,X2)
| ~ circle(X0,X1,sK27,X2) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_94867,plain,
( eqangle(sK22,sK27,sK22,sK22,sK22,sK27,sK22,sK22)
| ~ midp(sK22,sK27,sK22)
| ~ circle(sK22,sK22,sK27,sK22) ),
inference(instantiation,[status(thm)],[c_94866]) ).
tcf(c_96452,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK26,X0,X2)
| ~ coll(X0,X2,sK26)
| ~ eqangle(X0,X1,X0,sK26,X2,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_96453,plain,
( cyclic(sK22,sK26,sK22,sK22)
| ~ coll(sK22,sK22,sK26)
| ~ eqangle(sK22,sK22,sK22,sK26,sK22,sK22,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_96452]) ).
tcf(c_101783,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK27,X2,sK26)
| ~ coll(sK27,X2,sK26)
| ~ midp(X0,X2,X1)
| ~ para(X0,sK27,X1,sK26) ),
inference(instantiation,[status(thm)],[c_36895]) ).
tcf(c_101784,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK26,sK27)
| ~ midp(sK27,X1,sK27)
| ~ midp(sK27,X0,sK26) ),
inference(instantiation,[status(thm)],[c_36806]) ).
tcf(c_101789,plain,
( para(sK22,sK22,sK26,sK27)
| ~ midp(sK27,sK22,sK27)
| ~ midp(sK27,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_101784]) ).
tcf(c_101824,plain,
! [X0: $i,X1: $i] :
( midp(sK27,sK36,sK27)
| ~ coll(sK27,sK36,sK27)
| ~ midp(X0,sK36,X1)
| ~ para(X0,sK27,X1,sK27) ),
inference(instantiation,[status(thm)],[c_36895]) ).
tcf(c_101825,plain,
( midp(sK27,sK36,sK27)
| ~ midp(sK22,sK36,sK22)
| ~ coll(sK27,sK36,sK27)
| ~ para(sK22,sK27,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_101824]) ).
tcf(c_110627,plain,
! [X0: $i] :
( para(sK26,sK27,sK26,X0)
| ~ para(sK26,X0,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_40467]) ).
tcf(c_115424,plain,
( cong(sK26,sK27,sK26,sK26)
| ~ midp(sK26,sK27,sK26) ),
inference(instantiation,[status(thm)],[c_38771]) ).
tcf(c_122260,plain,
! [X0: $i] :
( eqangle(sK36,sK22,sK36,sK27,sK36,sK22,sK36,sK27)
| ~ perp(sK20,sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_37247,c_31869]) ).
tcf(c_122261,plain,
( eqangle(sK36,sK22,sK36,sK27,sK36,sK22,sK36,sK27)
| ~ perp(sK20,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_122260]) ).
tcf(c_142523,plain,
( para(sK26,sK27,sK26,sK26)
| ~ para(sK26,sK26,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_110627]) ).
tcf(c_143608,plain,
! [X0: $i,X1: $i] :
( midp(sK26,sK27,sK26)
| ~ coll(sK26,sK27,sK26)
| ~ midp(X0,sK27,X1)
| ~ para(X0,sK26,X1,sK26) ),
inference(instantiation,[status(thm)],[c_40587]) ).
tcf(c_143613,plain,
( midp(sK26,sK27,sK26)
| ~ midp(sK22,sK27,sK22)
| ~ coll(sK26,sK27,sK26)
| ~ para(sK22,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_143608]) ).
tcf(c_146003,plain,
! [X0: $i] :
( midp(sK27,X0,sK26)
| ~ midp(sK26,X0,sK26)
| ~ coll(sK27,X0,sK26)
| ~ para(sK26,sK27,sK26,sK26) ),
inference(instantiation,[status(thm)],[c_101783]) ).
tcf(c_146004,plain,
( midp(sK27,sK22,sK26)
| ~ midp(sK26,sK22,sK26)
| ~ coll(sK27,sK22,sK26)
| ~ para(sK26,sK27,sK26,sK26) ),
inference(instantiation,[status(thm)],[c_146003]) ).
tcf(c_161382,plain,
! [X0: $i,X1: $i] :
( cyclic(sK26,sK25,X0,X1)
| ~ coll(X0,X1,sK25)
| ~ eqangle(X0,sK26,X0,sK25,X1,sK26,X1,sK25) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_161383,plain,
( cyclic(sK26,sK25,sK22,sK22)
| ~ coll(sK22,sK22,sK25)
| ~ eqangle(sK22,sK26,sK22,sK25,sK22,sK26,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_161382]) ).
tcf(c_161533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X1,X4,sK25)
| ~ eqangle(X0,X1,X2,X3,X4,sK25,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_162802,plain,
! [X0: $i] :
( eqangle(X0,sK26,X0,sK25,X0,sK26,X0,sK25)
| ~ para(X0,sK26,X0,sK26) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_162804,plain,
( eqangle(sK22,sK26,sK22,sK25,sK22,sK26,sK22,sK25)
| ~ para(sK22,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_162802]) ).
tcf(c_163832,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(sK25,X1,X2,X3)
| ~ cyclic(X0,sK25,X1,X3)
| ~ cyclic(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_171998,plain,
! [X0: $i,X1: $i] :
( para(X0,sK25,X0,sK25)
| ~ eqangle(X0,sK25,X0,X1,X0,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_161533]) ).
tcf(c_171999,plain,
! [X0: $i,X1: $i] :
( eqangle(X1,sK25,X1,X0,X1,sK25,X1,X0)
| ~ cyclic(sK25,X0,X1,X1) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_172000,plain,
( para(sK22,sK25,sK22,sK25)
| ~ eqangle(sK22,sK25,sK22,sK22,sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_171998]) ).
tcf(c_172001,plain,
( eqangle(sK22,sK25,sK22,sK22,sK22,sK25,sK22,sK22)
| ~ cyclic(sK25,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_171999]) ).
tcf(c_173597,plain,
( perp(sK20,sK22,sK22,sK22)
| ~ midp(sK30,sK22,sK30)
| ~ circle(sK31,sK22,sK22,sK30) ),
inference(resolution,[status(thm)],[c_78150,c_164]) ).
tcf(c_177588,plain,
perp(sK20,sK22,sK22,sK22),
inference(global_subsumption_just,[status(thm)],[c_173597,c_164,c_163,c_179,c_183,c_204,c_237,c_329,c_330,c_503,c_512,c_582,c_1267,c_1509,c_1720,c_2122,c_5171,c_7109,c_9072,c_9645,c_15667,c_22784,c_24538,c_27668]) ).
tcf(c_177608,plain,
( cyclic(sK22,sK26,sK35,sK22)
| ~ coll(sK35,sK22,sK26) ),
inference(backward_subsumption_resolution,[status(thm)],[c_32889,c_177588]) ).
tcf(c_178787,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK25,X0,X1,X2)
| ~ cyclic(sK26,sK25,X0,X2)
| ~ cyclic(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_163832]) ).
tcf(c_178788,plain,
( cyclic(sK25,sK22,sK22,sK22)
| ~ cyclic(sK26,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_178787]) ).
tcf(c_178789,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_178788,c_177608,c_172001,c_172000,c_162804,c_161383,c_146004,c_143613,c_142523,c_122261,c_115424,c_101825,c_101789,c_96453,c_94867,c_83055,c_81799,c_79803,c_79527,c_77960,c_75849,c_73409,c_71924,c_64464,c_63502,c_59443,c_58994,c_57843,c_55776,c_55057,c_52877,c_52876,c_52127,c_48875,c_48370,c_48228,c_45946,c_45921,c_43793,c_42606,c_41523,c_40588,c_39408,c_39407,c_37600,c_36935,c_36361,c_33660,c_32363,c_31624,c_28460,c_27668,c_27635,c_24538,c_24457,c_22784,c_22779,c_22580,c_20633,c_15667,c_14943,c_12687,c_10247,c_9645,c_9072,c_7824,c_7109,c_5494,c_5171,c_4620,c_4542,c_4262,c_3400,c_2852,c_2496,c_2122,c_2121,c_2104,c_2102,c_2098,c_2061,c_1890,c_1720,c_1509,c_1415,c_1381,c_1296,c_1267,c_631,c_582,c_512,c_502,c_503,c_434,c_390,c_330,c_329,c_282,c_277,c_237,c_204,c_188,c_183,c_179,c_162,c_163,c_164,c_168,c_171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO602+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.36 % Computer : n006.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8046.5625MB
% 0.13/0.36 % OS : Linux 6.8.0-71-generic
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Sep 23 12:31:26 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/0.40 Running first-order theorem proving
% 0.16/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.16/0.41
% 0.16/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.41
% 0.16/0.41 % Detected problem language: tptp
% 0.16/0.43 % Proving...
% 154.82/23.58 % SZS status Started for theBenchmark.p
% 154.82/23.58 % SZS status Theorem for theBenchmark.p
% 154.82/23.58
% 154.82/23.58 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 154.82/23.58
% 154.82/23.58 % ------ iProver source info
% 154.82/23.58
% 154.82/23.58 % git: date: 2026-07-19 20:42:38 +0200
% 154.82/23.58 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 154.82/23.58 % git: non_committed_changes: false
% 154.82/23.58
% 154.82/23.58 % ------ Parsing...
% 154.82/23.58 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 154.82/23.58
% 154.82/23.58 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 1 0s sf_e %
% 154.82/23.58
% 154.82/23.58 % ------ Preprocessing...%
% 154.82/23.58
% 154.82/23.58 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 154.82/23.58 % ------ Proving...
% 154.82/23.58 % ------ Problem Properties
% 154.82/23.58
% 154.82/23.58 %
% 154.82/23.58 % clauses 124
% 154.82/23.58 % conjectures 12
% 154.82/23.58 % EPR 87
% 154.82/23.58 % Horn 114
% 154.82/23.58 % unary 12
% 154.82/23.58 % binary 37
% 154.82/23.58 % lits 340
% 154.82/23.58 % lits eq 4
% 154.82/23.58 % fd_pure 0
% 154.82/23.58 % fd_pseudo 0
% 154.82/23.58 % fd_cond 0
% 154.82/23.58 % fd_pseudo_cond 4
% 154.82/23.58 % AC symbols 0
% 154.82/23.58
% 154.82/23.58 % ------ Input Options Time Limit: Unbounded
% 154.82/23.58
% 154.82/23.58
% 154.82/23.58 % ------
% 154.82/23.58 % Current options:
% 154.82/23.58 % ------
% 154.82/23.58
% 154.82/23.58
% 154.82/23.58 %
% 154.82/23.58
% 154.82/23.58 % ------ Proving...
% 154.82/23.58 %
% 154.82/23.58
% 154.82/23.58 % SZS status Theorem for theBenchmark.p
% 154.82/23.58
% 154.82/23.58 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 154.82/23.59
% 154.82/23.59
%------------------------------------------------------------------------------