%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO658+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n003.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:46 PM UTC 2026
% Result : Theorem 173.87s 26.39s
% Output : CNFRefutation 173.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 47
% Syntax : Number of formulae : 974 ( 170 unt; 0 def)
% Number of atoms : 2382 ( 23 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 2691 (1283 ~;1277 |; 85 &)
% ( 0 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 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 : 10 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 1804 ( 0 sgn1786 !; 18 ?; 968 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD4) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD5) ).
fof(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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD8) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& perp(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD10) ).
fof(f11,axiom,
! [X0,X1,X2] :
( midp(X2,X1,X0)
=> midp(X2,X0,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD12) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD17) ).
fof(f19,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD19) ).
fof(f20,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD20) ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD21) ).
fof(f22,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD22) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD24) ).
fof(f25,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( cong(X2,X3,X4,X5)
& cong(X0,X1,X2,X3) )
=> cong(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD25) ).
fof(f39,axiom,
! [X0,X1,X2,X3,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD39) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f41,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
& cyclic(X0,X1,X2,X5)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f45,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X0,X2)
& midp(X3,X0,X1) )
=> para(X3,X4,X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD45) ).
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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD48) ).
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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD52) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( perp(X3,X2,X0,X1)
& midp(X2,X0,X1) )
=> cong(X3,X0,X3,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD56) ).
fof(f58,axiom,
! [X0,X1,X2,X3] :
( ( cyclic(X0,X1,X2,X3)
& cong(X0,X3,X1,X3)
& cong(X0,X2,X1,X2) )
=> perp(X2,X0,X0,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD57) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X2,X3)
& midp(X4,X0,X1) )
=> para(X0,X2,X1,X3) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD64) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( coll(X0,X1,X2)
& cong(X0,X1,X0,X2) )
=> midp(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD67) ).
fof(f69,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> cong(X0,X1,X0,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD73) ).
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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD74) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( coll(X8,X0,X1)
& coll(X8,X4,X5)
& coll(X7,X0,X3)
& coll(X7,X4,X6)
& coll(X6,X1,X2)
& perp(X6,X4,X1,X2)
& coll(X5,X2,X3)
& perp(X5,X4,X2,X3)
& coll(X4,X0,X2)
& para(X0,X2,X1,X3)
& para(X0,X1,X2,X3) )
=> para(X6,X5,X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULLmoreE02316) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( coll(X8,X0,X1)
& coll(X8,X4,X5)
& coll(X7,X0,X3)
& coll(X7,X4,X6)
& coll(X6,X1,X2)
& perp(X6,X4,X1,X2)
& coll(X5,X2,X3)
& perp(X5,X4,X2,X3)
& coll(X4,X0,X2)
& para(X0,X2,X1,X3)
& para(X0,X1,X2,X3) )
=> para(X6,X5,X7,X8) ),
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(f104,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(f105,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f104]) ).
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(f115,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(f116,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,[],[f115]) ).
fof(f117,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
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(f130,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f25]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f130]) ).
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(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(f157,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f157]) ).
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(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(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(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(f182,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(ennf_transformation,[],[f58]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(flattening,[],[f182]) ).
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(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(f208,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(f209,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,[],[f208]) ).
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(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( coll(X8,X0,X1)
& coll(X8,X4,X5)
& coll(X7,X0,X3)
& coll(X7,X4,X6)
& coll(X6,X1,X2)
& perp(X6,X4,X1,X2)
& coll(X5,X2,X3)
& perp(X5,X4,X2,X3)
& coll(X4,X0,X2)
& para(X0,X2,X1,X3)
& para(X0,X1,X2,X3)
& ~ para(X6,X5,X7,X8) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( coll(X8,X0,X1)
& coll(X8,X4,X5)
& coll(X7,X0,X3)
& coll(X7,X4,X6)
& coll(X6,X1,X2)
& perp(X6,X4,X1,X2)
& coll(X5,X2,X3)
& perp(X5,X4,X2,X3)
& coll(X4,X0,X2)
& para(X0,X2,X1,X3)
& para(X0,X1,X2,X3)
& ~ para(X6,X5,X7,X8) ),
inference(flattening,[],[f249]) ).
fof(f270,plain,
( coll(sK28,sK20,sK21)
& coll(sK28,sK24,sK25)
& coll(sK27,sK20,sK23)
& coll(sK27,sK24,sK26)
& coll(sK26,sK21,sK22)
& perp(sK26,sK24,sK21,sK22)
& coll(sK25,sK22,sK23)
& perp(sK25,sK24,sK22,sK23)
& coll(sK24,sK20,sK22)
& para(sK20,sK22,sK21,sK23)
& para(sK20,sK21,sK22,sK23)
& ~ para(sK26,sK25,sK27,sK28) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28]),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)],[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(f276,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,[],[f105]) ).
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(f283,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,[],[f116]) ).
fof(f284,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f285,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f118]) ).
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(f295,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f131]) ).
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(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(f315,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
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(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(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(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(f328,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(cnf_transformation,[],[f183]) ).
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(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(f344,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,[],[f209]) ).
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(f385,plain,
coll(sK28,sK24,sK25),
inference(cnf_transformation,[],[f270]) ).
fof(f387,plain,
coll(sK27,sK24,sK26),
inference(cnf_transformation,[],[f270]) ).
fof(f388,plain,
coll(sK26,sK21,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f389,plain,
perp(sK26,sK24,sK21,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
coll(sK25,sK22,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f391,plain,
perp(sK25,sK24,sK22,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f392,plain,
coll(sK24,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f393,plain,
para(sK20,sK22,sK21,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f394,plain,
para(sK20,sK21,sK22,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f395,plain,
~ para(sK26,sK25,sK27,sK28),
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_54,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,[],[f276]) ).
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_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X3,X2,X4)
| ~ cong(X0,X1,X0,X4)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f285]) ).
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_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X0,X1,X4,X5)
| ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f295]) ).
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_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_93,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X3,X2,X4)
| ~ midp(X3,X1,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f315]) ).
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_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_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_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_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X1,X0,X0,X3)
| ~ cyclic(X0,X2,X1,X3)
| ~ cong(X0,X3,X2,X3)
| ~ cong(X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f328]) ).
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_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_122,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,[],[f344]) ).
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_162,negated_conjecture,
~ para(sK26,sK25,sK27,sK28),
inference(cnf_transformation,[],[f395]) ).
tcf(c_163,negated_conjecture,
para(sK20,sK21,sK22,sK23),
inference(cnf_transformation,[],[f394]) ).
tcf(c_164,negated_conjecture,
para(sK20,sK22,sK21,sK23),
inference(cnf_transformation,[],[f393]) ).
tcf(c_165,negated_conjecture,
coll(sK24,sK20,sK22),
inference(cnf_transformation,[],[f392]) ).
tcf(c_166,negated_conjecture,
perp(sK25,sK24,sK22,sK23),
inference(cnf_transformation,[],[f391]) ).
tcf(c_167,negated_conjecture,
coll(sK25,sK22,sK23),
inference(cnf_transformation,[],[f390]) ).
tcf(c_168,negated_conjecture,
perp(sK26,sK24,sK21,sK22),
inference(cnf_transformation,[],[f389]) ).
tcf(c_169,negated_conjecture,
coll(sK26,sK21,sK22),
inference(cnf_transformation,[],[f388]) ).
tcf(c_170,negated_conjecture,
coll(sK27,sK24,sK26),
inference(cnf_transformation,[],[f387]) ).
tcf(c_172,negated_conjecture,
coll(sK28,sK24,sK25),
inference(cnf_transformation,[],[f385]) ).
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_184,plain,
( para(sK22,sK22,sK22,sK22)
| ~ eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_188,plain,
( perp(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_189,plain,
( circle(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_60]) ).
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_260,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_263,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( coll(X0,X2,X4)
| ~ coll(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_276,plain,
( coll(sK25,sK23,sK22)
| ~ coll(sK25,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_277,plain,
( coll(sK26,sK22,sK21)
| ~ coll(sK26,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_280,plain,
( coll(sK28,sK25,sK24)
| ~ coll(sK28,sK24,sK25) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_284,plain,
( coll(sK20,sK24,sK22)
| ~ coll(sK24,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_285,plain,
( coll(sK22,sK25,sK23)
| ~ coll(sK25,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_299,plain,
( para(sK22,sK23,sK20,sK21)
| ~ para(sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_303,plain,
( perp(sK25,sK24,sK23,sK22)
| ~ perp(sK25,sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_305,plain,
( perp(sK22,sK23,sK25,sK24)
| ~ perp(sK25,sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_306,plain,
( perp(sK21,sK22,sK26,sK24)
| ~ perp(sK26,sK24,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_309,plain,
! [X0: $i] :
( coll(X0,sK22,sK24)
| ~ coll(sK24,sK20,sK22)
| ~ coll(sK24,sK20,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_310,plain,
( coll(sK22,sK22,sK24)
| ~ coll(sK24,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_313,plain,
! [X0: $i] :
( coll(X0,sK22,sK26)
| ~ coll(sK26,sK21,sK22)
| ~ coll(sK26,sK21,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_314,plain,
( coll(sK22,sK22,sK26)
| ~ coll(sK26,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_313]) ).
tcf(c_337,plain,
coll(sK24,sK22,sK20),
inference(resolution,[status(thm)],[c_49,c_165]) ).
tcf(c_338,plain,
coll(sK25,sK23,sK22),
inference(resolution,[status(thm)],[c_49,c_167]) ).
tcf(c_339,plain,
coll(sK26,sK22,sK21),
inference(resolution,[status(thm)],[c_49,c_169]) ).
tcf(c_342,plain,
coll(sK28,sK25,sK24),
inference(resolution,[status(thm)],[c_49,c_172]) ).
tcf(c_354,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK22,sK23)
| ~ para(sK20,sK21,sK22,sK23)
| ~ para(X0,X1,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_369,plain,
! [X0: $i,X1: $i] :
( eqangle(sK20,sK21,X0,X1,sK22,sK23,X0,X1)
| ~ para(sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_370,plain,
( eqangle(sK20,sK21,sK22,sK22,sK22,sK23,sK22,sK22)
| ~ para(sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_369]) ).
tcf(c_373,plain,
coll(sK24,sK22,sK20),
inference(superposition,[status(thm)],[c_165,c_49]) ).
tcf(c_388,plain,
coll(sK25,sK23,sK22),
inference(superposition,[status(thm)],[c_167,c_49]) ).
tcf(c_389,plain,
coll(sK26,sK22,sK21),
inference(superposition,[status(thm)],[c_169,c_49]) ).
tcf(c_390,plain,
coll(sK27,sK26,sK24),
inference(superposition,[status(thm)],[c_170,c_49]) ).
tcf(c_392,plain,
coll(sK28,sK25,sK24),
inference(superposition,[status(thm)],[c_172,c_49]) ).
tcf(c_437,plain,
coll(sK21,sK26,sK22),
inference(resolution,[status(thm)],[c_50,c_169]) ).
tcf(c_438,plain,
coll(sK24,sK27,sK26),
inference(resolution,[status(thm)],[c_50,c_170]) ).
tcf(c_442,plain,
coll(sK22,sK24,sK20),
inference(resolution,[status(thm)],[c_50,c_337]) ).
tcf(c_443,plain,
coll(sK23,sK25,sK22),
inference(resolution,[status(thm)],[c_50,c_338]) ).
tcf(c_462,plain,
coll(sK20,sK24,sK22),
inference(superposition,[status(thm)],[c_165,c_50]) ).
tcf(c_463,plain,
coll(sK22,sK25,sK23),
inference(superposition,[status(thm)],[c_167,c_50]) ).
tcf(c_464,plain,
coll(sK21,sK26,sK22),
inference(superposition,[status(thm)],[c_169,c_50]) ).
tcf(c_465,plain,
coll(sK24,sK27,sK26),
inference(superposition,[status(thm)],[c_170,c_50]) ).
tcf(c_467,plain,
coll(sK24,sK28,sK25),
inference(superposition,[status(thm)],[c_172,c_50]) ).
tcf(c_469,plain,
coll(sK22,sK24,sK20),
inference(superposition,[status(thm)],[c_373,c_50]) ).
tcf(c_471,plain,
coll(sK22,sK26,sK21),
inference(superposition,[status(thm)],[c_389,c_50]) ).
tcf(c_472,plain,
coll(sK26,sK27,sK24),
inference(superposition,[status(thm)],[c_390,c_50]) ).
tcf(c_474,plain,
coll(sK25,sK28,sK24),
inference(superposition,[status(thm)],[c_392,c_50]) ).
tcf(c_479,plain,
coll(sK22,sK26,sK21),
inference(resolution,[status(thm)],[c_339,c_50]) ).
tcf(c_482,plain,
! [X0: $i] :
( coll(X0,sK22,sK25)
| ~ coll(sK25,sK23,sK22)
| ~ coll(sK25,sK23,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_483,plain,
( coll(sK22,sK22,sK25)
| ~ coll(sK25,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_482]) ).
tcf(c_484,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ coll(sK25,sK23,sK22)
| ( X2 != sK22 )
| ( X1 != sK23 )
| ( X0 != sK25 ) ),
inference(instantiation,[status(thm)],[c_263]) ).
tcf(c_535,plain,
coll(sK22,sK23,sK25),
inference(superposition,[status(thm)],[c_463,c_49]) ).
tcf(c_542,plain,
! [X0: $i] :
( coll(X0,sK24,sK28)
| ~ coll(sK28,sK25,sK24)
| ~ coll(sK28,sK25,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_562,plain,
! [X0: $i] :
( coll(X0,sK22,sK20)
| ~ coll(sK20,sK24,sK22)
| ~ coll(sK20,sK24,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_563,plain,
( coll(sK22,sK22,sK20)
| ~ coll(sK20,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_574,plain,
! [X0: $i] :
( coll(X0,sK23,sK22)
| ~ coll(sK22,sK25,sK23)
| ~ coll(sK22,sK25,X0) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_575,plain,
( coll(sK22,sK23,sK22)
| ~ coll(sK22,sK25,sK23)
| ~ coll(sK22,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_574]) ).
tcf(c_619,plain,
! [X0: $i] :
( coll(sK22,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_165,c_51]) ).
tcf(c_620,plain,
! [X0: $i] :
( coll(sK23,X0,sK25)
| ~ coll(sK25,sK22,X0) ),
inference(superposition,[status(thm)],[c_167,c_51]) ).
tcf(c_621,plain,
! [X0: $i] :
( coll(sK22,X0,sK26)
| ~ coll(sK26,sK21,X0) ),
inference(superposition,[status(thm)],[c_169,c_51]) ).
tcf(c_622,plain,
! [X0: $i] :
( coll(sK26,X0,sK27)
| ~ coll(sK27,sK24,X0) ),
inference(superposition,[status(thm)],[c_170,c_51]) ).
tcf(c_624,plain,
! [X0: $i] :
( coll(sK25,X0,sK28)
| ~ coll(sK28,sK24,X0) ),
inference(superposition,[status(thm)],[c_172,c_51]) ).
tcf(c_626,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK22,X0) ),
inference(superposition,[status(thm)],[c_373,c_51]) ).
tcf(c_627,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK23,X0) ),
inference(superposition,[status(thm)],[c_388,c_51]) ).
tcf(c_628,plain,
! [X0: $i] :
( coll(sK21,X0,sK26)
| ~ coll(sK26,sK22,X0) ),
inference(superposition,[status(thm)],[c_389,c_51]) ).
tcf(c_631,plain,
! [X0: $i] :
( coll(sK24,X0,sK28)
| ~ coll(sK28,sK25,X0) ),
inference(superposition,[status(thm)],[c_392,c_51]) ).
tcf(c_633,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_462,c_51]) ).
tcf(c_634,plain,
! [X0: $i] :
( coll(sK23,X0,sK22)
| ~ coll(sK22,sK25,X0) ),
inference(superposition,[status(thm)],[c_463,c_51]) ).
tcf(c_635,plain,
! [X0: $i] :
( coll(sK22,X0,sK21)
| ~ coll(sK21,sK26,X0) ),
inference(superposition,[status(thm)],[c_464,c_51]) ).
tcf(c_636,plain,
! [X0: $i] :
( coll(sK26,X0,sK24)
| ~ coll(sK24,sK27,X0) ),
inference(superposition,[status(thm)],[c_465,c_51]) ).
tcf(c_646,plain,
( coll(sK23,sK22,sK22)
| ~ coll(sK22,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_634]) ).
tcf(c_654,plain,
( coll(sK24,sK22,sK28)
| ~ coll(sK28,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_631]) ).
tcf(c_802,plain,
para(sK21,sK23,sK20,sK22),
inference(resolution,[status(thm)],[c_53,c_164]) ).
tcf(c_808,plain,
perp(sK26,sK24,sK22,sK21),
inference(resolution,[status(thm)],[c_55,c_168]) ).
tcf(c_811,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK23,sK22)
| ~ perp(sK25,sK24,sK23,sK22)
| ~ para(X0,X1,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_825,plain,
perp(sK22,sK23,sK25,sK24),
inference(resolution,[status(thm)],[c_56,c_166]) ).
tcf(c_826,plain,
perp(sK21,sK22,sK26,sK24),
inference(resolution,[status(thm)],[c_56,c_168]) ).
tcf(c_858,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK25,sK24)
| ~ perp(sK22,sK23,sK25,sK24)
| ~ perp(X0,X1,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_874,plain,
perp(sK22,sK21,sK26,sK24),
inference(resolution,[status(thm)],[c_808,c_56]) ).
tcf(c_877,plain,
perp(sK22,sK23,sK24,sK25),
inference(resolution,[status(thm)],[c_825,c_55]) ).
tcf(c_896,plain,
! [X0: $i] :
( coll(X0,sK24,sK22)
| ~ coll(X0,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_897,plain,
( coll(sK22,sK24,sK22)
| ~ coll(sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_896]) ).
tcf(c_904,plain,
! [X0: $i] :
( coll(sK22,X0,sK26)
| ~ coll(X0,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_905,plain,
! [X0: $i] :
( coll(X0,sK26,sK22)
| ~ coll(X0,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_906,plain,
( coll(sK22,sK26,sK22)
| ~ coll(sK22,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_905]) ).
tcf(c_916,plain,
( para(sK22,sK23,sK22,sK23)
| ~ para(sK22,sK23,sK20,sK21)
| ~ para(sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_354]) ).
tcf(c_920,plain,
! [X0: $i,X1: $i] :
( eqangle(sK20,sK21,sK22,sK23,X0,X1,X0,X1)
| ~ eqangle(sK20,sK21,X0,X1,sK22,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_922,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK20,sK21,X0,X1,sK22,sK23)
| ~ eqangle(sK20,sK21,X0,X1,sK22,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_931,plain,
( eqangle(sK20,sK21,sK22,sK23,sK22,sK22,sK22,sK22)
| ~ eqangle(sK20,sK21,sK22,sK22,sK22,sK23,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_920]) ).
tcf(c_1014,plain,
! [X0: $i] :
( coll(sK25,X0,sK24)
| ~ coll(sK24,sK28,X0) ),
inference(superposition,[status(thm)],[c_467,c_51]) ).
tcf(c_1017,plain,
( coll(sK25,sK22,sK24)
| ~ coll(sK24,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_1014]) ).
tcf(c_1051,plain,
sK23 = sK23,
inference(instantiation,[status(thm)],[c_260]) ).
tcf(c_1067,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(superposition,[status(thm)],[c_469,c_51]) ).
tcf(c_1069,plain,
coll(sK22,sK20,sK24),
inference(superposition,[status(thm)],[c_469,c_49]) ).
tcf(c_1070,plain,
( coll(sK20,sK22,sK22)
| ~ coll(sK22,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_1067]) ).
tcf(c_1134,plain,
coll(sK22,sK21,sK26),
inference(superposition,[status(thm)],[c_471,c_49]) ).
tcf(c_1147,plain,
perp(sK24,sK25,sK22,sK23),
inference(resolution,[status(thm)],[c_877,c_56]) ).
tcf(c_1157,plain,
sK25 = sK25,
inference(instantiation,[status(thm)],[c_260]) ).
tcf(c_1163,plain,
coll(sK26,sK24,sK27),
inference(superposition,[status(thm)],[c_472,c_49]) ).
tcf(c_1240,plain,
! [X0: $i] :
( coll(X0,sK22,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(resolution,[status(thm)],[c_51,c_165]) ).
tcf(c_1241,plain,
! [X0: $i] :
( coll(X0,sK23,sK25)
| ~ coll(sK25,sK22,X0) ),
inference(resolution,[status(thm)],[c_51,c_167]) ).
tcf(c_1242,plain,
! [X0: $i] :
( coll(X0,sK22,sK26)
| ~ coll(sK26,sK21,X0) ),
inference(resolution,[status(thm)],[c_51,c_169]) ).
tcf(c_1247,plain,
! [X0: $i] :
( coll(X0,sK25,sK28)
| ~ coll(sK28,sK24,X0) ),
inference(resolution,[status(thm)],[c_51,c_172]) ).
tcf(c_1252,plain,
! [X0: $i] :
( coll(X0,sK22,sK25)
| ~ coll(sK25,sK23,X0) ),
inference(resolution,[status(thm)],[c_51,c_338]) ).
tcf(c_1253,plain,
! [X0: $i] :
( coll(X0,sK21,sK26)
| ~ coll(sK26,sK22,X0) ),
inference(resolution,[status(thm)],[c_51,c_339]) ).
tcf(c_1258,plain,
! [X0: $i] :
( coll(X0,sK24,sK28)
| ~ coll(sK28,sK25,X0) ),
inference(resolution,[status(thm)],[c_51,c_342]) ).
tcf(c_1265,plain,
! [X0: $i] :
( coll(X0,sK22,sK21)
| ~ coll(sK21,sK26,X0) ),
inference(resolution,[status(thm)],[c_51,c_437]) ).
tcf(c_1266,plain,
! [X0: $i] :
( coll(X0,sK26,sK24)
| ~ coll(sK24,sK27,X0) ),
inference(resolution,[status(thm)],[c_51,c_438]) ).
tcf(c_1276,plain,
! [X0: $i] :
( coll(X0,sK20,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(resolution,[status(thm)],[c_51,c_442]) ).
tcf(c_1277,plain,
( coll(sK22,sK20,sK22)
| ~ coll(sK22,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_1276]) ).
tcf(c_1281,plain,
! [X0: $i] :
( coll(X0,sK21,sK22)
| ~ coll(sK22,sK26,X0) ),
inference(resolution,[status(thm)],[c_51,c_479]) ).
tcf(c_1282,plain,
( coll(sK22,sK21,sK22)
| ~ coll(sK22,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_1281]) ).
tcf(c_1349,plain,
coll(sK25,sK24,sK28),
inference(superposition,[status(thm)],[c_474,c_49]) ).
tcf(c_1395,plain,
! [X0: $i] :
( coll(sK25,X0,sK22)
| ~ coll(sK22,sK23,X0) ),
inference(superposition,[status(thm)],[c_535,c_51]) ).
tcf(c_1398,plain,
( coll(sK25,sK22,sK22)
| ~ coll(sK22,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_1395]) ).
tcf(c_1506,plain,
! [X0: $i] :
( coll(sK24,X0,sK22)
| ~ coll(sK22,sK20,X0) ),
inference(superposition,[status(thm)],[c_1069,c_51]) ).
tcf(c_1509,plain,
( coll(sK24,sK22,sK22)
| ~ coll(sK22,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_1506]) ).
tcf(c_1536,plain,
! [X0: $i] :
( coll(sK26,X0,sK22)
| ~ coll(sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_1134,c_51]) ).
tcf(c_1539,plain,
( coll(sK26,sK22,sK22)
| ~ coll(sK22,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_1536]) ).
tcf(c_1551,plain,
! [X0: $i] :
( coll(sK27,X0,sK26)
| ~ coll(sK26,sK24,X0) ),
inference(superposition,[status(thm)],[c_1163,c_51]) ).
tcf(c_1554,plain,
( coll(sK27,sK22,sK26)
| ~ coll(sK26,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_1551]) ).
tcf(c_1609,plain,
coll(sK22,sK22,sK24),
inference(resolution,[status(thm)],[c_1240,c_165]) ).
tcf(c_1610,plain,
! [X0: $i] :
( coll(sK28,X0,sK25)
| ~ coll(sK25,sK24,X0) ),
inference(superposition,[status(thm)],[c_1349,c_51]) ).
tcf(c_1613,plain,
( coll(sK28,sK22,sK25)
| ~ coll(sK25,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_1610]) ).
tcf(c_1620,plain,
coll(sK22,sK24,sK22),
inference(resolution,[status(thm)],[c_1609,c_49]) ).
tcf(c_1622,plain,
! [X0: $i] :
( coll(X0,sK24,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_1609,c_51]) ).
tcf(c_1640,plain,
coll(sK23,sK23,sK25),
inference(resolution,[status(thm)],[c_1241,c_167]) ).
tcf(c_1666,plain,
! [X0: $i] :
( coll(X0,sK25,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(resolution,[status(thm)],[c_1640,c_51]) ).
tcf(c_1671,plain,
coll(sK22,sK22,sK26),
inference(resolution,[status(thm)],[c_1242,c_169]) ).
tcf(c_1672,plain,
coll(sK22,sK22,sK24),
inference(superposition,[status(thm)],[c_165,c_619]) ).
tcf(c_1675,plain,
coll(sK22,sK24,sK22),
inference(superposition,[status(thm)],[c_1672,c_49]) ).
tcf(c_1685,plain,
! [X0: $i] :
( coll(X0,sK26,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_1671,c_51]) ).
tcf(c_1742,plain,
! [X0: $i] :
( coll(sK22,X0,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(superposition,[status(thm)],[c_1675,c_51]) ).
tcf(c_1745,plain,
( coll(sK22,sK22,sK22)
| ~ coll(sK22,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_1742]) ).
tcf(c_1772,plain,
coll(sK25,sK25,sK28),
inference(resolution,[status(thm)],[c_1247,c_172]) ).
tcf(c_1796,plain,
! [X0: $i] :
( coll(X0,sK28,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(resolution,[status(thm)],[c_1772,c_51]) ).
tcf(c_1825,plain,
! [X0: $i] :
( coll(X0,sK22,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(resolution,[status(thm)],[c_1620,c_51]) ).
tcf(c_1866,plain,
coll(sK23,sK23,sK25),
inference(superposition,[status(thm)],[c_167,c_620]) ).
tcf(c_1887,plain,
! [X0: $i] :
( coll(sK25,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_1866,c_51]) ).
tcf(c_1889,plain,
coll(sK23,sK25,sK23),
inference(superposition,[status(thm)],[c_1866,c_49]) ).
tcf(c_1906,plain,
! [X0: $i] :
( coll(sK23,X0,sK23)
| ~ coll(sK23,sK25,X0) ),
inference(superposition,[status(thm)],[c_1889,c_51]) ).
tcf(c_1909,plain,
( coll(sK23,sK22,sK23)
| ~ coll(sK23,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_1906]) ).
tcf(c_1970,plain,
coll(sK22,sK22,sK26),
inference(superposition,[status(thm)],[c_169,c_621]) ).
tcf(c_1977,plain,
! [X0: $i] :
( coll(sK26,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_1970,c_51]) ).
tcf(c_1994,plain,
( coll(sK25,sK22,sK25)
| ~ coll(sK25,sK23,sK22)
| ~ coll(sK25,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_482]) ).
tcf(c_2025,plain,
coll(sK22,sK22,sK25),
inference(resolution,[status(thm)],[c_1252,c_338]) ).
tcf(c_2035,plain,
coll(sK22,sK25,sK22),
inference(resolution,[status(thm)],[c_2025,c_49]) ).
tcf(c_2038,plain,
coll(sK26,sK26,sK27),
inference(superposition,[status(thm)],[c_170,c_622]) ).
tcf(c_2040,plain,
! [X0: $i] :
( coll(sK25,sK22,X0)
| ~ coll(sK25,X0,sK22) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2051,plain,
! [X0: $i] :
( coll(sK27,sK26,X0)
| ~ coll(sK27,X0,sK26) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2052,plain,
( coll(sK27,sK26,sK22)
| ~ coll(sK27,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_2051]) ).
tcf(c_2055,plain,
! [X0: $i] :
( coll(sK28,sK25,X0)
| ~ coll(sK28,X0,sK25) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2056,plain,
( coll(sK28,sK25,sK22)
| ~ coll(sK28,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_2055]) ).
tcf(c_2064,plain,
! [X0: $i] :
( coll(sK24,sK28,X0)
| ~ coll(sK24,X0,sK28) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_2065,plain,
( coll(sK24,sK28,sK22)
| ~ coll(sK24,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_2064]) ).
tcf(c_2075,plain,
! [X0: $i] :
( coll(sK27,X0,sK26)
| ~ coll(sK26,sK26,X0) ),
inference(superposition,[status(thm)],[c_2038,c_51]) ).
tcf(c_2186,plain,
( coll(sK22,sK25,sK26)
| ~ coll(sK25,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_904]) ).
tcf(c_2257,plain,
coll(sK25,sK25,sK28),
inference(superposition,[status(thm)],[c_172,c_624]) ).
tcf(c_2258,plain,
! [X0: $i] :
( coll(sK28,X0,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(superposition,[status(thm)],[c_2257,c_51]) ).
tcf(c_2260,plain,
coll(sK25,sK28,sK25),
inference(superposition,[status(thm)],[c_2257,c_49]) ).
tcf(c_2267,plain,
coll(sK28,sK25,sK25),
inference(superposition,[status(thm)],[c_2260,c_50]) ).
tcf(c_2278,plain,
! [X0: $i] :
( coll(sK25,X0,sK28)
| ~ coll(sK28,sK25,X0) ),
inference(superposition,[status(thm)],[c_2267,c_51]) ).
tcf(c_2281,plain,
( coll(sK25,sK22,sK28)
| ~ coll(sK28,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_2278]) ).
tcf(c_2332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( circle(X0,X1,X2,X3)
| ~ midp(X0,X1,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_117,c_60]) ).
tcf(c_2452,plain,
coll(sK22,sK22,sK21),
inference(resolution,[status(thm)],[c_1265,c_437]) ).
tcf(c_2518,plain,
coll(sK26,sK26,sK24),
inference(resolution,[status(thm)],[c_1266,c_438]) ).
tcf(c_2521,plain,
coll(sK26,sK24,sK26),
inference(resolution,[status(thm)],[c_2518,c_49]) ).
tcf(c_2576,plain,
coll(sK20,sK20,sK24),
inference(superposition,[status(thm)],[c_373,c_626]) ).
tcf(c_2627,plain,
coll(sK20,sK24,sK20),
inference(superposition,[status(thm)],[c_2576,c_49]) ).
tcf(c_2664,plain,
coll(sK24,sK24,sK22),
inference(resolution,[status(thm)],[c_1622,c_1609]) ).
tcf(c_2665,plain,
coll(sK26,sK24,sK22),
inference(resolution,[status(thm)],[c_1622,c_1671]) ).
tcf(c_2666,plain,
coll(sK25,sK24,sK22),
inference(resolution,[status(thm)],[c_1622,c_2025]) ).
tcf(c_2668,plain,
coll(sK21,sK24,sK22),
inference(resolution,[status(thm)],[c_1622,c_2452]) ).
tcf(c_2684,plain,
coll(sK24,sK22,sK24),
inference(resolution,[status(thm)],[c_2664,c_49]) ).
tcf(c_2711,plain,
coll(sK26,sK22,sK24),
inference(resolution,[status(thm)],[c_2665,c_49]) ).
tcf(c_2737,plain,
coll(sK25,sK25,sK23),
inference(resolution,[status(thm)],[c_1666,c_1640]) ).
tcf(c_2754,plain,
coll(sK25,sK23,sK25),
inference(resolution,[status(thm)],[c_2737,c_49]) ).
tcf(c_2802,plain,
coll(sK26,sK26,sK22),
inference(resolution,[status(thm)],[c_1685,c_1671]) ).
tcf(c_2803,plain,
coll(sK25,sK26,sK22),
inference(resolution,[status(thm)],[c_1685,c_2025]) ).
tcf(c_2806,plain,
coll(sK22,sK22,sK25),
inference(superposition,[status(thm)],[c_388,c_627]) ).
tcf(c_2836,plain,
coll(sK26,sK22,sK26),
inference(resolution,[status(thm)],[c_2802,c_49]) ).
tcf(c_2921,plain,
! [X0: $i,X1: $i] :
( coll(X0,sK23,X1)
| ~ coll(sK25,sK23,sK22)
| ( sK23 != sK23 )
| ( X1 != sK22 )
| ( X0 != sK25 ) ),
inference(instantiation,[status(thm)],[c_484]) ).
tcf(c_2941,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,X1,sK20,sK21,sK22,sK23)
| ~ eqangle(sK20,sK21,sK22,sK23,X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_2944,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK21,sK22,sK23)
| ~ perp(X0,X1,X0,X1)
| ~ eqangle(sK20,sK21,sK22,sK23,X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_2946,plain,
( perp(sK20,sK21,sK22,sK23)
| ~ perp(sK22,sK22,sK22,sK22)
| ~ eqangle(sK20,sK21,sK22,sK23,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_2944]) ).
tcf(c_2949,plain,
( eqangle(sK22,sK22,sK22,sK22,sK20,sK21,sK22,sK23)
| ~ eqangle(sK20,sK21,sK22,sK23,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_2941]) ).
tcf(c_2951,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X2,X3,X4,X5,X4,X5)
| ~ eqangle(sK20,sK21,sK22,sK23,X4,X5,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_2952,plain,
( eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22)
| ~ eqangle(sK22,sK22,sK22,sK22,sK20,sK21,sK22,sK23)
| ~ eqangle(sK20,sK21,sK22,sK23,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_2951]) ).
tcf(c_3047,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK20,sK22)
| ~ para(X0,X1,sK21,sK23) ),
inference(resolution,[status(thm)],[c_54,c_802]) ).
tcf(c_3354,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,X1,sK20,sK21,sK22,sK23)
| ~ eqangle(X0,X1,sK20,sK21,X0,X1,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_3409,plain,
coll(sK28,sK28,sK25),
inference(resolution,[status(thm)],[c_1796,c_1772]) ).
tcf(c_3702,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK21,sK22)
| ~ perp(X0,X1,sK26,sK24) ),
inference(resolution,[status(thm)],[c_57,c_168]) ).
tcf(c_3706,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK22,sK21)
| ~ perp(X0,X1,sK26,sK24) ),
inference(resolution,[status(thm)],[c_57,c_808]) ).
tcf(c_3708,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK25,sK24)
| ~ perp(X0,X1,sK22,sK23) ),
inference(resolution,[status(thm)],[c_57,c_825]) ).
tcf(c_3766,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK22,sK23)
| ~ para(X0,X1,sK25,sK24) ),
inference(resolution,[status(thm)],[c_58,c_166]) ).
tcf(c_3776,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK26,sK24)
| ~ para(X0,X1,sK21,sK22) ),
inference(resolution,[status(thm)],[c_58,c_826]) ).
tcf(c_3879,plain,
( coll(sK25,sK22,sK26)
| ~ coll(sK25,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_2040]) ).
tcf(c_3988,plain,
para(sK22,sK21,sK21,sK22),
inference(resolution,[status(thm)],[c_3702,c_874]) ).
tcf(c_4103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( circle(X0,X1,X2,X3)
| ~ midp(X0,X1,X3)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_117,c_2332]) ).
tcf(c_4119,plain,
para(sK22,sK21,sK22,sK21),
inference(resolution,[status(thm)],[c_3988,c_52]) ).
tcf(c_4135,plain,
para(sK20,sK22,sK20,sK22),
inference(resolution,[status(thm)],[c_3047,c_164]) ).
tcf(c_4193,plain,
( para(sK26,sK25,sK27,sK28)
| ~ para(sK26,sK25,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_4245,plain,
coll(sK22,sK20,sK20),
inference(superposition,[status(thm)],[c_2627,c_633]) ).
tcf(c_4248,plain,
! [X0: $i] :
( coll(sK25,sK25,X0)
| ~ coll(sK25,X0,sK25) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_4249,plain,
( coll(sK25,sK25,sK22)
| ~ coll(sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_4248]) ).
tcf(c_4300,plain,
coll(sK20,sK22,sK20),
inference(superposition,[status(thm)],[c_4245,c_50]) ).
tcf(c_4366,plain,
coll(sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_4300,c_49]) ).
tcf(c_4395,plain,
para(sK25,sK24,sK25,sK24),
inference(resolution,[status(thm)],[c_3708,c_166]) ).
tcf(c_4424,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK22,sK23)
| ~ para(X2,X3,sK25,sK24)
| ~ perp(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[c_3766,c_57]) ).
tcf(c_4451,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK20,sK21)
| ~ para(sK20,sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_4459,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK21,sK22)
| ~ para(sK21,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_4460,plain,
( para(sK22,sK22,sK21,sK22)
| ~ para(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_4459]) ).
tcf(c_4461,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK25,sK24)
| ~ para(sK25,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_4605,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK21,sK22)
| ~ perp(sK21,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_4606,plain,
( perp(sK22,sK22,sK21,sK22)
| ~ perp(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_4605]) ).
tcf(c_5020,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK22,sK23,X2,X3)
| ~ perp(sK22,sK23,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_5021,plain,
( para(sK22,sK23,sK22,sK22)
| ~ perp(sK22,sK23,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_5020]) ).
tcf(c_5055,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK22,sK21)
| ~ para(X0,X1,sK21,sK22) ),
inference(resolution,[status(thm)],[c_3776,c_3706]) ).
tcf(c_5056,plain,
( para(sK22,sK22,sK22,sK21)
| ~ para(sK22,sK22,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_5055]) ).
tcf(c_5435,plain,
coll(sK26,sK26,sK24),
inference(superposition,[status(thm)],[c_465,c_636]) ).
tcf(c_5459,plain,
! [X0: $i] :
( coll(sK24,X0,sK26)
| ~ coll(sK26,sK26,X0) ),
inference(superposition,[status(thm)],[c_5435,c_51]) ).
tcf(c_5462,plain,
( coll(sK24,sK22,sK26)
| ~ coll(sK26,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_5459]) ).
tcf(c_6250,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,X0,X0)
| ~ coll(X0,X0,X2)
| ~ para(X0,X1,X0,X1) ),
inference(resolution,[status(thm)],[c_91,c_88]) ).
tcf(c_6281,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK24,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_166,c_57]) ).
tcf(c_6342,plain,
( para(sK25,sK24,sK22,sK22)
| ~ perp(sK22,sK23,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_6281]) ).
tcf(c_6440,plain,
! [X0: $i] :
( coll(sK25,sK23,X0)
| ~ coll(sK25,sK23,sK22)
| ( sK23 != sK23 )
| ( sK25 != sK25 )
| ( X0 != sK22 ) ),
inference(instantiation,[status(thm)],[c_2921]) ).
tcf(c_7131,plain,
! [X0: $i] :
( coll(X0,sK26,sK26)
| ~ coll(sK26,sK24,X0) ),
inference(resolution,[status(thm)],[c_2521,c_51]) ).
tcf(c_7132,plain,
( coll(sK22,sK26,sK26)
| ~ coll(sK26,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_7131]) ).
tcf(c_7155,plain,
coll(sK25,sK25,sK24),
inference(superposition,[status(thm)],[c_467,c_1014]) ).
tcf(c_7203,plain,
! [X0: $i] :
( coll(sK24,X0,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(superposition,[status(thm)],[c_7155,c_51]) ).
tcf(c_7206,plain,
( coll(sK24,sK22,sK25)
| ~ coll(sK25,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_7203]) ).
tcf(c_7288,plain,
coll(sK24,sK21,sK22),
inference(resolution,[status(thm)],[c_2668,c_50]) ).
tcf(c_7334,plain,
coll(sK24,sK21,sK26),
inference(resolution,[status(thm)],[c_2711,c_1253]) ).
tcf(c_7954,plain,
( para(sK20,sK21,sK25,sK24)
| ~ perp(sK22,sK23,sK25,sK24)
| ~ perp(sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_858]) ).
tcf(c_8417,plain,
coll(sK21,sK24,sK26),
inference(resolution,[status(thm)],[c_7334,c_50]) ).
tcf(c_8618,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(sK26,sK25,X0,X1)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(sK26,sK25,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_8622,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK25,X1,X0)
| ~ para(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_8623,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK25,X0,X1)
| ~ para(X0,X1,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_8624,plain,
( para(sK26,sK25,sK22,sK22)
| ~ para(sK22,sK22,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_8623]) ).
tcf(c_8630,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(sK26,sK25,X0,X1)
| ~ perp(X2,X3,X4,X5)
| ~ eqangle(sK26,sK25,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_8632,plain,
! [X0: $i,X1: $i] :
( perp(sK26,sK25,X1,X0)
| ~ perp(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_8652,plain,
! [X0: $i,X1: $i] :
( eqangle(sK26,sK25,sK27,sK28,X0,X1,sK27,sK28)
| ~ para(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_9957,plain,
( para(sK24,sK25,sK22,sK23)
| ~ para(sK22,sK23,sK25,sK24) ),
inference(resolution,[status(thm)],[c_1147,c_4424]) ).
tcf(c_11498,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ( X2 != sK22 )
| ( X1 != sK20 )
| ( X0 != sK24 ) ),
inference(resolution,[status(thm)],[c_263,c_165]) ).
tcf(c_11758,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK22,sK24,X1,X2)
| ~ midp(sK24,X0,X2)
| ~ midp(sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_11759,plain,
( para(sK22,sK24,sK22,sK22)
| ~ midp(sK24,sK22,sK22)
| ~ midp(sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_11758]) ).
tcf(c_12687,plain,
! [X0: $i] :
( coll(X0,sK24,sK28)
| ( sK28 != sK24 )
| ( sK25 != sK20 )
| ( X0 != sK22 ) ),
inference(resolution,[status(thm)],[c_11498,c_1258]) ).
tcf(c_12913,plain,
coll(sK25,sK25,sK23),
inference(superposition,[status(thm)],[c_1866,c_1887]) ).
tcf(c_12986,plain,
coll(sK25,sK23,sK25),
inference(superposition,[status(thm)],[c_12913,c_49]) ).
tcf(c_12998,plain,
! [X0: $i] :
( coll(sK25,X0,sK25)
| ~ coll(sK25,sK23,X0) ),
inference(superposition,[status(thm)],[c_12986,c_51]) ).
tcf(c_13216,plain,
! [X0: $i,X1: $i] :
( perp(sK22,sK23,X0,X1)
| ~ cong(sK22,X1,sK23,X1)
| ~ cong(sK22,X0,sK23,X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_13217,plain,
( perp(sK22,sK23,sK22,sK22)
| ~ cong(sK22,sK22,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_13216]) ).
tcf(c_14044,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK26,sK25)
| ~ para(X0,X1,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_14045,plain,
( para(sK22,sK22,sK26,sK25)
| ~ para(sK22,sK22,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_14044]) ).
tcf(c_14046,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK26,sK25)
| ~ para(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_14450,plain,
coll(sK26,sK25,sK22),
inference(superposition,[status(thm)],[c_2806,c_1977]) ).
tcf(c_14457,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK24)
| ~ coll(X1,X3,sK24)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK24) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_14458,plain,
( midp(sK22,sK22,sK24)
| ~ midp(sK22,sK22,sK22)
| ~ coll(sK22,sK22,sK24)
| ~ para(sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_14457]) ).
tcf(c_14489,plain,
coll(sK26,sK22,sK25),
inference(superposition,[status(thm)],[c_14450,c_49]) ).
tcf(c_14494,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X0,X1)
| ~ coll(sK25,X0,X1)
| ~ cong(sK25,X0,sK25,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_14495,plain,
( midp(sK25,sK22,sK22)
| ~ coll(sK25,sK22,sK22)
| ~ cong(sK25,sK22,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_14494]) ).
tcf(c_14639,plain,
coll(sK21,sK25,sK26),
inference(superposition,[status(thm)],[c_14489,c_628]) ).
tcf(c_14646,plain,
coll(sK21,sK26,sK25),
inference(superposition,[status(thm)],[c_14639,c_49]) ).
tcf(c_14931,plain,
coll(sK22,sK25,sK21),
inference(superposition,[status(thm)],[c_14646,c_635]) ).
tcf(c_14960,plain,
coll(sK25,sK22,sK21),
inference(superposition,[status(thm)],[c_14931,c_50]) ).
tcf(c_15050,plain,
coll(sK25,sK21,sK22),
inference(superposition,[status(thm)],[c_14960,c_49]) ).
tcf(c_15418,plain,
( eqangle(sK26,sK25,sK20,sK21,sK26,sK25,sK22,sK23)
| ~ eqangle(sK20,sK21,sK26,sK25,sK22,sK23,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_922]) ).
tcf(c_15431,plain,
( para(sK26,sK25,sK26,sK25)
| ~ para(sK20,sK21,sK22,sK23)
| ~ eqangle(sK26,sK25,sK26,sK25,sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_8618]) ).
tcf(c_15432,plain,
( eqangle(sK26,sK25,sK26,sK25,sK20,sK21,sK22,sK23)
| ~ eqangle(sK26,sK25,sK20,sK21,sK26,sK25,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_3354]) ).
tcf(c_15613,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK28,sK25)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK28,X1,sK25)
| ~ para(X0,sK25,X1,sK28) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_15614,plain,
( midp(sK22,sK28,sK25)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK28,sK22,sK25)
| ~ para(sK22,sK25,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_15613]) ).
tcf(c_15615,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK25,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK25,X2,X1)
| ~ para(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_15616,plain,
( midp(sK22,sK25,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK25)
| ~ para(sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_15615]) ).
tcf(c_16389,plain,
coll(sK27,sK27,sK26),
inference(superposition,[status(thm)],[c_2038,c_2075]) ).
tcf(c_16395,plain,
coll(sK27,sK26,sK27),
inference(superposition,[status(thm)],[c_16389,c_49]) ).
tcf(c_16417,plain,
! [X0: $i] :
( coll(sK27,X0,sK27)
| ~ coll(sK27,sK26,X0) ),
inference(superposition,[status(thm)],[c_16395,c_51]) ).
tcf(c_16421,plain,
( coll(sK27,sK22,sK27)
| ~ coll(sK27,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_16417]) ).
tcf(c_17120,plain,
( para(sK25,sK24,sK20,sK21)
| ~ para(sK20,sK21,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_4451]) ).
tcf(c_17544,plain,
coll(sK25,sK23,sK22),
inference(superposition,[status(thm)],[c_167,c_49]) ).
tcf(c_17545,plain,
coll(sK26,sK22,sK21),
inference(superposition,[status(thm)],[c_169,c_49]) ).
tcf(c_17814,plain,
coll(sK22,sK25,sK23),
inference(superposition,[status(thm)],[c_167,c_50]) ).
tcf(c_17815,plain,
coll(sK21,sK26,sK22),
inference(superposition,[status(thm)],[c_169,c_50]) ).
tcf(c_17839,plain,
! [X0: $i] :
( coll(sK23,X0,sK25)
| ~ coll(sK25,sK22,X0) ),
inference(superposition,[status(thm)],[c_167,c_51]) ).
tcf(c_17840,plain,
! [X0: $i] :
( coll(sK22,X0,sK26)
| ~ coll(sK26,sK21,X0) ),
inference(superposition,[status(thm)],[c_169,c_51]) ).
tcf(c_17843,plain,
! [X0: $i] :
( coll(sK25,X0,sK28)
| ~ coll(sK28,sK24,X0) ),
inference(superposition,[status(thm)],[c_172,c_51]) ).
tcf(c_17846,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK23,X0) ),
inference(superposition,[status(thm)],[c_17544,c_51]) ).
tcf(c_17847,plain,
! [X0: $i] :
( coll(sK21,X0,sK26)
| ~ coll(sK26,sK22,X0) ),
inference(superposition,[status(thm)],[c_17545,c_51]) ).
tcf(c_17853,plain,
! [X0: $i] :
( coll(sK23,X0,sK22)
| ~ coll(sK22,sK25,X0) ),
inference(superposition,[status(thm)],[c_17814,c_51]) ).
tcf(c_17854,plain,
! [X0: $i] :
( coll(sK22,X0,sK21)
| ~ coll(sK21,sK26,X0) ),
inference(superposition,[status(thm)],[c_17815,c_51]) ).
tcf(c_18556,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,sK25,X2,sK28)
| ~ midp(sK25,X1,sK28)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_18557,plain,
( para(sK22,sK25,sK22,sK28)
| ~ midp(sK22,sK22,sK22)
| ~ midp(sK25,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_18556]) ).
tcf(c_18579,plain,
coll(sK23,sK23,sK25),
inference(superposition,[status(thm)],[c_167,c_17839]) ).
tcf(c_18580,plain,
! [X0: $i] :
( coll(sK25,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_18579,c_51]) ).
tcf(c_18745,plain,
coll(sK22,sK22,sK26),
inference(superposition,[status(thm)],[c_169,c_17840]) ).
tcf(c_18746,plain,
! [X0: $i] :
( coll(sK26,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_18745,c_51]) ).
tcf(c_18897,plain,
coll(sK25,sK25,sK28),
inference(superposition,[status(thm)],[c_172,c_17843]) ).
tcf(c_18898,plain,
! [X0: $i] :
( coll(sK28,X0,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(superposition,[status(thm)],[c_18897,c_51]) ).
tcf(c_18926,plain,
! [X0: $i,X1: $i] :
( para(X0,sK28,X1,sK25)
| ~ para(X0,sK28,sK25,X1) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_18927,plain,
( para(sK22,sK28,sK22,sK25)
| ~ para(sK22,sK28,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_18926]) ).
tcf(c_18954,plain,
para(sK22,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_163,c_53]) ).
tcf(c_18955,plain,
para(sK21,sK23,sK20,sK22),
inference(superposition,[status(thm)],[c_164,c_53]) ).
tcf(c_18968,plain,
para(sK21,sK23,sK22,sK20),
inference(superposition,[status(thm)],[c_18955,c_52]) ).
tcf(c_19358,plain,
coll(sK22,sK22,sK25),
inference(superposition,[status(thm)],[c_17544,c_17846]) ).
tcf(c_19362,plain,
coll(sK22,sK25,sK22),
inference(superposition,[status(thm)],[c_19358,c_49]) ).
tcf(c_19393,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(X0,X4,X2,X3)
| ~ midp(X0,X4,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_117,c_73]) ).
tcf(c_19496,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK21,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK21,X2,X1)
| ~ para(X0,X1,X2,sK21) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_19497,plain,
( midp(sK22,sK21,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK21)
| ~ para(sK22,sK21,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_19496]) ).
tcf(c_19821,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK22,X0,X1)
| ~ para(sK21,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_164,c_54]) ).
tcf(c_19824,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK23,X0,X1)
| ~ para(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_18954,c_54]) ).
tcf(c_19921,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(sK20,X1,sK20,X3)
| ~ cyclic(sK20,X1,X0,sK20)
| ~ cyclic(sK20,X1,X0,X3)
| ~ cyclic(sK20,X1,X0,X2)
| ~ eqangle(X0,sK20,X0,X1,X2,sK20,X2,X3) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_19922,plain,
( cong(sK20,sK22,sK20,sK22)
| ~ cyclic(sK20,sK22,sK22,sK22)
| ~ cyclic(sK20,sK22,sK22,sK20)
| ~ eqangle(sK22,sK20,sK22,sK22,sK22,sK20,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_19921]) ).
tcf(c_19929,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(sK25,X1,sK25,X3)
| ~ cyclic(sK25,X1,X0,sK25)
| ~ cyclic(sK25,X1,X0,X3)
| ~ cyclic(sK25,X1,X0,X2)
| ~ eqangle(X0,sK25,X0,X1,X2,sK25,X2,X3) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_19930,plain,
( cong(sK25,sK22,sK25,sK22)
| ~ cyclic(sK25,sK22,sK22,sK22)
| ~ cyclic(sK25,sK22,sK22,sK25)
| ~ eqangle(sK22,sK25,sK22,sK22,sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_19929]) ).
tcf(c_20097,plain,
para(sK20,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_18968,c_19821]) ).
tcf(c_20512,plain,
perp(sK26,sK24,sK22,sK21),
inference(superposition,[status(thm)],[c_168,c_55]) ).
tcf(c_20859,plain,
coll(sK23,sK23,sK22),
inference(superposition,[status(thm)],[c_17814,c_17853]) ).
tcf(c_20860,plain,
coll(sK23,sK22,sK22),
inference(superposition,[status(thm)],[c_19362,c_17853]) ).
tcf(c_20863,plain,
coll(sK23,sK22,sK23),
inference(superposition,[status(thm)],[c_20859,c_49]) ).
tcf(c_20871,plain,
coll(sK22,sK23,sK22),
inference(superposition,[status(thm)],[c_20860,c_50]) ).
tcf(c_20920,plain,
coll(sK22,sK22,sK23),
inference(superposition,[status(thm)],[c_20871,c_49]) ).
tcf(c_21539,plain,
perp(sK22,sK23,sK25,sK24),
inference(superposition,[status(thm)],[c_166,c_56]) ).
tcf(c_21540,plain,
perp(sK21,sK22,sK26,sK24),
inference(superposition,[status(thm)],[c_168,c_56]) ).
tcf(c_21542,plain,
perp(sK22,sK21,sK26,sK24),
inference(superposition,[status(thm)],[c_20512,c_56]) ).
tcf(c_21556,plain,
perp(sK22,sK23,sK24,sK25),
inference(superposition,[status(thm)],[c_21539,c_55]) ).
tcf(c_21558,plain,
perp(sK21,sK22,sK24,sK26),
inference(superposition,[status(thm)],[c_21540,c_55]) ).
tcf(c_21562,plain,
perp(sK22,sK21,sK24,sK26),
inference(superposition,[status(thm)],[c_21542,c_55]) ).
tcf(c_21813,plain,
( eqangle(sK20,sK21,sK26,sK25,sK22,sK23,sK26,sK25)
| ~ para(sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_369]) ).
tcf(c_22225,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK24,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_166,c_57]) ).
tcf(c_22226,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK24,X0,X1)
| ~ perp(sK21,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_168,c_57]) ).
tcf(c_22230,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK22,X0,X1)
| ~ perp(sK26,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_21540,c_57]) ).
tcf(c_22503,plain,
( para(sK25,sK24,sK22,sK23)
| ~ para(sK20,sK21,sK22,sK23)
| ~ para(sK25,sK24,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_354]) ).
tcf(c_22596,plain,
para(sK25,sK24,sK25,sK24),
inference(superposition,[status(thm)],[c_21539,c_22225]) ).
tcf(c_22597,plain,
para(sK25,sK24,sK24,sK25),
inference(superposition,[status(thm)],[c_21556,c_22225]) ).
tcf(c_22617,plain,
para(sK24,sK25,sK25,sK24),
inference(superposition,[status(thm)],[c_22597,c_53]) ).
tcf(c_22634,plain,
para(sK26,sK24,sK24,sK26),
inference(superposition,[status(thm)],[c_21558,c_22226]) ).
tcf(c_22639,plain,
para(sK24,sK26,sK26,sK24),
inference(superposition,[status(thm)],[c_22634,c_53]) ).
tcf(c_22647,plain,
para(sK24,sK26,sK24,sK26),
inference(superposition,[status(thm)],[c_22639,c_52]) ).
tcf(c_24165,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,X1,sK25)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK25,X2,X1)
| ~ para(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_24166,plain,
( midp(sK22,sK22,sK25)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK25)
| ~ para(sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_24165]) ).
tcf(c_24536,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK23,sK22,X2)
| ~ coll(sK23,sK22,X2)
| ~ midp(X0,sK22,X1)
| ~ para(X0,sK23,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_24537,plain,
( midp(sK23,sK22,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ coll(sK23,sK22,sK22)
| ~ para(sK22,sK23,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_24536]) ).
tcf(c_24601,plain,
( eqangle(sK26,sK25,sK27,sK28,sK26,sK25,sK27,sK28)
| ~ para(sK26,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_8652]) ).
tcf(c_24602,plain,
( para(sK26,sK25,sK25,sK26)
| ~ para(sK26,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_8622]) ).
tcf(c_24606,plain,
! [X0: $i,X1: $i] :
( midp(sK20,X0,X1)
| ~ coll(sK20,X0,X1)
| ~ cong(sK20,X0,sK20,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_24607,plain,
( midp(sK20,sK22,sK22)
| ~ coll(sK20,sK22,sK22)
| ~ cong(sK20,sK22,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_24606]) ).
tcf(c_25061,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X0,X1)
| ~ coll(sK26,X0,X1)
| ~ cong(sK26,X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_25062,plain,
( midp(sK26,sK22,sK22)
| ~ coll(sK26,sK22,sK22)
| ~ cong(sK26,sK22,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_25061]) ).
tcf(c_25183,plain,
( para(sK22,sK23,sK25,sK24)
| ~ para(sK25,sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_4461]) ).
tcf(c_25523,plain,
( perp(sK26,sK25,sK26,sK25)
| ~ perp(sK20,sK21,sK22,sK23)
| ~ eqangle(sK26,sK25,sK26,sK25,sK20,sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_8630]) ).
tcf(c_26353,plain,
! [X0: $i] :
( perp(sK28,sK25,X0,sK28)
| ~ perp(sK28,sK25,sK28,X0) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_26354,plain,
( perp(sK28,sK25,sK22,sK28)
| ~ perp(sK28,sK25,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_26353]) ).
tcf(c_26477,plain,
! [X0: $i] :
( coll(X0,sK24,sK28)
| ( X0 != sK22 ) ),
inference(global_subsumption_just,[status(thm)],[c_12687,c_172,c_167,c_276,c_280,c_542,c_1051,c_1157,c_2055,c_2258,c_4248,c_6440,c_12998]) ).
tcf(c_26669,plain,
( coll(sK28,sK22,sK22)
| ( sK22 != sK22 ) ),
inference(resolution,[status(thm)],[c_26477,c_1825]) ).
tcf(c_26670,plain,
coll(sK28,sK22,sK22),
inference(equality_resolution_simp,[status(thm)],[c_26669]) ).
tcf(c_27303,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK21,sK22,X2,X3)
| ~ para(sK21,sK22,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_27304,plain,
( perp(sK21,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22)
| ~ para(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_27303]) ).
tcf(c_27828,plain,
coll(sK25,sK25,sK23),
inference(superposition,[status(thm)],[c_18579,c_18580]) ).
tcf(c_27873,plain,
coll(sK25,sK23,sK25),
inference(superposition,[status(thm)],[c_27828,c_49]) ).
tcf(c_27912,plain,
coll(sK22,sK25,sK25),
inference(superposition,[status(thm)],[c_27873,c_17846]) ).
tcf(c_27975,plain,
coll(sK25,sK22,sK25),
inference(superposition,[status(thm)],[c_27912,c_50]) ).
tcf(c_28492,plain,
coll(sK25,sK25,sK22),
inference(superposition,[status(thm)],[c_27975,c_49]) ).
tcf(c_29296,plain,
coll(sK26,sK23,sK22),
inference(superposition,[status(thm)],[c_20920,c_18746]) ).
tcf(c_29321,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK22,sK24)
| ~ para(sK22,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_29322,plain,
( para(sK22,sK22,sK22,sK24)
| ~ para(sK22,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_29321]) ).
tcf(c_29402,plain,
coll(sK26,sK22,sK23),
inference(superposition,[status(thm)],[c_29296,c_49]) ).
tcf(c_29612,plain,
coll(sK21,sK23,sK26),
inference(superposition,[status(thm)],[c_29402,c_17847]) ).
tcf(c_29619,plain,
coll(sK21,sK26,sK23),
inference(superposition,[status(thm)],[c_29612,c_49]) ).
tcf(c_29824,plain,
coll(sK22,sK23,sK21),
inference(superposition,[status(thm)],[c_29619,c_17854]) ).
tcf(c_29845,plain,
coll(sK23,sK22,sK21),
inference(superposition,[status(thm)],[c_29824,c_50]) ).
tcf(c_29846,plain,
coll(sK22,sK21,sK23),
inference(superposition,[status(thm)],[c_29824,c_49]) ).
tcf(c_30046,plain,
coll(sK21,sK22,sK23),
inference(superposition,[status(thm)],[c_29846,c_50]) ).
tcf(c_31429,plain,
( perp(sK22,sK23,sK23,sK22)
| ~ perp(sK25,sK24,sK23,sK22)
| ~ para(sK22,sK23,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_31532,plain,
( para(sK25,sK26,sK26,sK25)
| ~ para(sK26,sK25,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_14046]) ).
tcf(c_31711,plain,
( perp(sK26,sK25,sK25,sK26)
| ~ perp(sK26,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_8632]) ).
tcf(c_33387,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK26,X0,X1)
| ~ para(X0,X1,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_33388,plain,
( para(sK25,sK26,sK22,sK22)
| ~ para(sK22,sK22,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_33387]) ).
tcf(c_34755,plain,
! [X0: $i] :
( cyclic(sK22,X0,sK20,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(resolution,[status(thm)],[c_6250,c_4135]) ).
tcf(c_34757,plain,
! [X0: $i] :
( cyclic(sK21,X0,sK22,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(resolution,[status(thm)],[c_6250,c_4119]) ).
tcf(c_34758,plain,
( cyclic(sK21,sK22,sK22,sK22)
| ~ coll(sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_34757]) ).
tcf(c_34759,plain,
! [X0: $i] :
( cyclic(sK24,X0,sK25,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(resolution,[status(thm)],[c_6250,c_4395]) ).
tcf(c_35050,plain,
coll(sK28,sK28,sK25),
inference(superposition,[status(thm)],[c_18897,c_18898]) ).
tcf(c_35051,plain,
coll(sK28,sK22,sK25),
inference(superposition,[status(thm)],[c_28492,c_18898]) ).
tcf(c_35056,plain,
coll(sK28,sK25,sK28),
inference(superposition,[status(thm)],[c_35050,c_49]) ).
tcf(c_35064,plain,
coll(sK28,sK25,sK22),
inference(superposition,[status(thm)],[c_35051,c_49]) ).
tcf(c_35142,plain,
! [X0: $i] :
( coll(sK28,X0,sK28)
| ~ coll(sK28,sK25,X0) ),
inference(superposition,[status(thm)],[c_35056,c_51]) ).
tcf(c_35146,plain,
( coll(sK28,sK22,sK28)
| ~ coll(sK28,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_35142]) ).
tcf(c_35159,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X1,sK25)
| ~ cong(X0,sK25,X1,sK25)
| ~ cong(X0,X1,X1,X1) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_35160,plain,
( perp(sK22,sK22,sK22,sK25)
| ~ cong(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_35159]) ).
tcf(c_35306,plain,
! [X0: $i] :
( coll(sK22,X0,sK28)
| ~ coll(sK28,sK25,X0) ),
inference(superposition,[status(thm)],[c_35064,c_51]) ).
tcf(c_35310,plain,
( coll(sK22,sK22,sK28)
| ~ coll(sK28,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_35306]) ).
tcf(c_35752,plain,
! [X0: $i] :
( cyclic(sK22,sK20,X0,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(resolution,[status(thm)],[c_63,c_34755]) ).
tcf(c_35753,plain,
( cyclic(sK22,sK20,sK22,sK20)
| ~ coll(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_35752]) ).
tcf(c_36797,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK25,sK28,sK27)
| ~ perp(sK26,sK25,X0,X1)
| ~ perp(X0,X1,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_37057,plain,
! [X0: $i,X1: $i] :
( perp(sK26,sK25,sK25,X0)
| ~ cong(sK25,sK26,X1,sK26)
| ~ cyclic(sK25,X1,sK26,X0)
| ~ cong(sK25,X0,X1,X0) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_37200,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK27,sK28,X2,X3)
| ~ eqangle(sK27,sK28,X0,X1,X2,X3,X0,X1) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_37335,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK25,X1,sK25)
| ~ coll(sK25,sK25,X0)
| ~ cyclic(sK24,X0,sK25,X1) ),
inference(resolution,[status(thm)],[c_65,c_34759]) ).
tcf(c_37336,plain,
( cyclic(sK22,sK25,sK22,sK25)
| ~ coll(sK25,sK25,sK22)
| ~ cyclic(sK24,sK22,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_37335]) ).
tcf(c_37348,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK25,X3,X2)
| ~ coll(sK25,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_37349,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK25,X1,X2)
| ~ coll(sK25,X1,X2)
| ~ circle(X3,X0,X1,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,sK25) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_37356,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK25,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK25,X2,X1)
| ~ para(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_37463,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK27,sK28,sK26,sK25,X2,X3,X0,X1)
| ~ eqangle(sK26,sK25,sK27,sK28,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_37542,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(sK28,sK25,sK28,X0)
| ~ perp(X1,X2,X3,X4)
| ~ eqangle(sK28,sK25,sK28,X0,X1,X2,X3,X4) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_38152,plain,
( para(sK26,sK25,sK28,sK27)
| ~ perp(sK25,sK26,sK28,sK27)
| ~ perp(sK26,sK25,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_36797]) ).
tcf(c_38332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK25)
| ~ coll(X1,X3,sK25)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_38668,plain,
! [X0: $i,X1: $i] :
( para(sK28,sK27,X0,X1)
| ~ para(X0,X1,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_38963,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,sK25,sK26)
| ~ perp(X2,X3,sK25,sK26)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_39009,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK27)
| ~ para(X0,X1,sK27,sK28) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_39368,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK26,X0,X1)
| ~ para(X0,X1,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_39484,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK26,X1)
| ~ coll(X0,sK26,X1)
| ~ cong(X0,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_39491,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK26,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK26,X2,X1)
| ~ para(X0,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_39492,plain,
( midp(sK22,sK26,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK26)
| ~ para(sK22,sK26,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_39491]) ).
tcf(c_39692,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK28,X3,X2)
| ~ coll(sK28,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK28,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_39693,plain,
( midp(sK28,sK22,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ coll(sK28,sK22,sK22)
| ~ para(sK22,sK28,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_39692]) ).
tcf(c_39727,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,sK25,X3,sK25)
| ~ cyclic(X1,sK25,X0,sK25)
| ~ cyclic(X1,sK25,X0,X3)
| ~ cyclic(X1,sK25,X0,X2)
| ~ eqangle(X0,X1,X0,sK25,X2,X3,X2,sK25) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_39728,plain,
( cong(sK22,sK25,sK22,sK25)
| ~ cyclic(sK22,sK25,sK22,sK22)
| ~ cyclic(sK22,sK25,sK22,sK25)
| ~ eqangle(sK22,sK22,sK22,sK25,sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_39727]) ).
tcf(c_39801,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(sK25,X1,sK25,X2)
| ~ midp(X0,X1,X2)
| ~ perp(sK25,X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_39992,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK25,sK28,X1)
| ~ coll(sK28,X1,sK25)
| ~ eqangle(sK28,X0,sK28,sK25,X1,X0,X1,sK25) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_40118,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK25,X2,sK26,X2)
| ~ perp(sK25,X2,X0,X1)
| ~ perp(X0,X1,sK26,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_40404,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK28,X0,sK28)
| ~ midp(sK28,X0,X1)
| ~ perp(X0,X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_40406,plain,
( cong(sK22,sK28,sK22,sK28)
| ~ midp(sK28,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_40404]) ).
tcf(c_40961,plain,
para(sK22,sK23,sK22,sK23),
inference(superposition,[status(thm)],[c_163,c_19824]) ).
tcf(c_41378,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(X2,sK25,X0,X1)
| ~ perp(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_41379,plain,
( perp(sK22,sK25,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_41378]) ).
tcf(c_41688,plain,
para(sK21,sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_20512,c_22230]) ).
tcf(c_41723,plain,
para(sK22,sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_41688,c_53]) ).
tcf(c_41816,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK21,X0,X1)
| ~ para(sK21,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_41723,c_54]) ).
tcf(c_41819,plain,
( para(sK22,sK21,sK22,sK22)
| ~ para(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_41816]) ).
tcf(c_42074,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,sK25,X0,X2)
| ~ midp(sK25,X1,X2)
| ~ midp(X0,X1,X0) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_42075,plain,
( para(sK22,sK25,sK22,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ midp(sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_42074]) ).
tcf(c_42109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,sK26,X2,X3)
| ~ perp(X2,sK26,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_42947,plain,
! [X0: $i,X1: $i] :
( perp(sK25,sK26,sK28,sK27)
| ~ perp(X0,X1,sK28,sK27)
| ~ para(sK25,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_42948,plain,
( perp(sK25,sK26,sK28,sK27)
| ~ perp(sK22,sK22,sK28,sK27)
| ~ para(sK25,sK26,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_42947]) ).
tcf(c_42983,plain,
( eqangle(sK27,sK28,sK26,sK25,sK27,sK28,sK26,sK25)
| ~ eqangle(sK26,sK25,sK27,sK28,sK26,sK25,sK27,sK28) ),
inference(instantiation,[status(thm)],[c_37463]) ).
tcf(c_43160,plain,
! [X0: $i,X1: $i] :
( perp(sK28,sK25,sK28,X0)
| ~ perp(X1,sK25,X1,X0)
| ~ eqangle(sK28,sK25,sK28,X0,X1,sK25,X1,X0) ),
inference(instantiation,[status(thm)],[c_37542]) ).
tcf(c_43161,plain,
! [X0: $i,X1: $i] :
( eqangle(sK28,sK25,sK28,X0,X1,sK25,X1,X0)
| ~ cyclic(sK25,X0,sK28,X1) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_43162,plain,
( perp(sK28,sK25,sK28,sK22)
| ~ perp(sK22,sK25,sK22,sK22)
| ~ eqangle(sK28,sK25,sK28,sK22,sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_43160]) ).
tcf(c_43163,plain,
( eqangle(sK28,sK25,sK28,sK22,sK22,sK25,sK22,sK22)
| ~ cyclic(sK25,sK22,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_43161]) ).
tcf(c_43208,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,sK28,X2)
| ~ cyclic(X0,sK28,X1,X2) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_43209,plain,
( cyclic(sK22,sK22,sK28,sK22)
| ~ cyclic(sK22,sK28,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_43208]) ).
tcf(c_43214,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X0,sK28,X2)
| ~ cyclic(X0,X1,sK28,X2) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_43215,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,sK28,X3)
| ~ cyclic(X0,X1,X2,sK28)
| ~ cyclic(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_43354,plain,
! [X0: $i,X1: $i,X2: $i] :
( circle(X0,X1,X2,sK25)
| ~ midp(X0,X1,sK25)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_4103]) ).
tcf(c_43355,plain,
( circle(sK22,sK22,sK22,sK25)
| ~ midp(sK22,sK22,sK22)
| ~ midp(sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_43354]) ).
tcf(c_43367,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,X1,X2,sK25)
| ~ para(X0,X1,sK25,X2) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_43372,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X1,X4,sK25)
| ~ perp(X2,X3,X4,sK25)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_43374,plain,
( para(sK22,sK22,sK22,sK25)
| ~ perp(sK22,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_43372]) ).
tcf(c_43393,plain,
! [X0: $i] :
( midp(X0,sK25,sK25)
| ~ midp(X0,sK26,sK26)
| ~ para(sK26,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_37356]) ).
tcf(c_43394,plain,
( midp(sK22,sK25,sK25)
| ~ midp(sK22,sK26,sK26)
| ~ para(sK26,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_43393]) ).
tcf(c_43858,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,sK25,X3,sK28,X1,X2,X3,sK28)
| ~ para(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_43860,plain,
( eqangle(sK22,sK25,sK22,sK28,sK22,sK22,sK22,sK28)
| ~ para(sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_43858]) ).
tcf(c_44284,plain,
! [X0: $i,X1: $i] :
( cyclic(sK25,X1,X0,sK28)
| ~ cyclic(sK25,X0,X1,sK28) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_44291,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK25,X1,X2,sK28)
| ~ cyclic(X0,sK25,X1,sK28)
| ~ cyclic(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_44516,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X1,sK25)
| ~ coll(sK25,X1,sK25)
| ~ circle(X0,X0,X1,sK25)
| ~ eqangle(X0,X1,X0,sK25,X0,X1,X0,sK25) ),
inference(instantiation,[status(thm)],[c_37349]) ).
tcf(c_44517,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,sK25,X0,X1,X0,sK25)
| ~ para(X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_44518,plain,
( midp(sK25,sK22,sK25)
| ~ coll(sK25,sK22,sK25)
| ~ circle(sK22,sK22,sK22,sK25)
| ~ eqangle(sK22,sK22,sK22,sK25,sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_44516]) ).
tcf(c_44519,plain,
( eqangle(sK22,sK22,sK22,sK25,sK22,sK22,sK22,sK25)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_44517]) ).
tcf(c_44525,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,X2,X1,X3,X0,X2,X0,sK25)
| ~ midp(sK25,X2,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_44526,plain,
( eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK25)
| ~ midp(sK25,sK22,sK22)
| ~ circle(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_44525]) ).
tcf(c_44625,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK25,X1,sK28)
| ~ cyclic(X0,X1,sK25,sK28) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_44626,plain,
( cyclic(sK22,sK25,sK22,sK28)
| ~ cyclic(sK22,sK22,sK25,sK28) ),
inference(instantiation,[status(thm)],[c_44625]) ).
tcf(c_46838,plain,
! [X0: $i,X1: $i] :
( perp(sK28,sK25,sK25,X0)
| ~ cong(sK25,sK28,X1,sK28)
| ~ cyclic(sK25,X1,sK28,X0)
| ~ cong(sK25,X0,X1,X0) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_46839,plain,
( perp(sK28,sK25,sK25,sK22)
| ~ cyclic(sK25,sK22,sK28,sK22)
| ~ cong(sK25,sK22,sK22,sK22)
| ~ cong(sK25,sK28,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_46838]) ).
tcf(c_46897,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK25,X2,sK26)
| ~ cong(X0,X1,X0,sK25)
| ~ cong(X0,X1,X0,sK26)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_46898,plain,
( cyclic(sK22,sK25,sK22,sK26)
| ~ cong(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK25)
| ~ cong(sK22,sK22,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_46897]) ).
tcf(c_47566,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK28,sK27)
| ~ cong(X0,sK28,X1,sK28)
| ~ cong(X0,sK27,X1,sK27) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_47567,plain,
( perp(sK22,sK22,sK28,sK27)
| ~ cong(sK22,sK28,sK22,sK28)
| ~ cong(sK22,sK27,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_47566]) ).
tcf(c_49266,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,X2,X1,sK25)
| ~ cyclic(X1,X2,X0,sK25)
| ~ cyclic(X1,X2,X0,X3)
| ~ cyclic(X1,X2,X0,X1)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,sK25) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_49267,plain,
( cong(sK22,sK22,sK22,sK25)
| ~ cyclic(sK22,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK22,sK25)
| ~ eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_49266]) ).
tcf(c_51304,plain,
( para(sK27,sK28,sK27,sK28)
| ~ eqangle(sK27,sK28,sK26,sK25,sK27,sK28,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_37200]) ).
tcf(c_52259,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,sK25,sK28)
| ~ cyclic(X0,X1,X2,sK28)
| ~ cyclic(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_52260,plain,
( cyclic(sK22,sK22,sK25,sK28)
| ~ cyclic(sK22,sK22,sK22,sK28)
| ~ cyclic(sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_52259]) ).
tcf(c_52510,plain,
! [X0: $i,X1: $i] :
( cong(sK25,sK26,X0,sK26)
| ~ midp(sK26,sK25,X1)
| ~ perp(sK25,X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_52511,plain,
( cong(sK25,sK26,sK22,sK26)
| ~ midp(sK26,sK25,sK22)
| ~ perp(sK25,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_52510]) ).
tcf(c_52702,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,X0,sK26)
| ~ para(X0,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_52703,plain,
( para(sK22,sK22,sK22,sK26)
| ~ para(sK22,sK26,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_52702]) ).
tcf(c_53026,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK28,X0,X2)
| ~ coll(X0,X2,sK28)
| ~ eqangle(X0,X1,X0,sK28,X2,X1,X2,sK28) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_53027,plain,
( cyclic(sK22,sK28,sK22,sK22)
| ~ coll(sK22,sK22,sK28)
| ~ eqangle(sK22,sK22,sK22,sK28,sK22,sK22,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_53026]) ).
tcf(c_53032,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,X2,sK28)
| ~ cyclic(X0,X1,sK28,X2) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_53033,plain,
( cyclic(sK22,sK22,sK22,sK28)
| ~ cyclic(sK22,sK22,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_53032]) ).
tcf(c_53290,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK25,X0,X1,X2)
| ~ cyclic(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_53291,plain,
( cyclic(sK25,sK22,sK22,sK22)
| ~ cyclic(sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_53290]) ).
tcf(c_53577,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK25,X0,X2)
| ~ coll(X0,X2,sK25)
| ~ eqangle(X0,X1,X0,sK25,X2,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_53578,plain,
( cyclic(sK22,sK25,sK22,sK22)
| ~ coll(sK22,sK22,sK25)
| ~ eqangle(sK22,sK22,sK22,sK25,sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_53577]) ).
tcf(c_53633,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK25,X0,X0,X1)
| ~ cong(X0,sK25,X2,sK25)
| ~ cyclic(X0,X2,sK25,X1)
| ~ cong(X0,X1,X2,X1) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_53634,plain,
( perp(sK25,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK25,sK22)
| ~ cong(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_53633]) ).
tcf(c_53882,plain,
! [X0: $i] :
( midp(X0,sK26,sK26)
| ~ coll(X0,sK26,sK26)
| ~ cong(X0,sK26,X0,sK26) ),
inference(instantiation,[status(thm)],[c_39484]) ).
tcf(c_53883,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK26,X0,sK26)
| ~ midp(sK26,X0,X1)
| ~ perp(X0,X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_53884,plain,
( midp(sK22,sK26,sK26)
| ~ coll(sK22,sK26,sK26)
| ~ cong(sK22,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_53882]) ).
tcf(c_53885,plain,
( cong(sK22,sK26,sK22,sK26)
| ~ midp(sK26,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_53883]) ).
tcf(c_55329,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK25,sK26)
| ~ perp(sK26,sK25,sK25,sK26)
| ~ para(X0,X1,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_38963]) ).
tcf(c_55439,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(sK25,X1,X3,X4)
| ~ cyclic(sK25,X1,X0,X4)
| ~ cyclic(sK25,X1,X0,X3)
| ~ cyclic(sK25,X1,X0,X2)
| ~ eqangle(X0,sK25,X0,X1,X2,X3,X2,X4) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_55440,plain,
( cong(sK25,sK22,sK22,sK22)
| ~ cyclic(sK25,sK22,sK22,sK22)
| ~ eqangle(sK22,sK25,sK22,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_55439]) ).
tcf(c_56015,plain,
( para(sK25,sK24,sK26,sK24)
| ~ perp(sK22,sK23,sK26,sK24)
| ~ perp(sK25,sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_40118]) ).
tcf(c_56024,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(sK25,X4,X2,X3)
| ~ perp(sK25,X4,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_56026,plain,
( para(sK25,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22)
| ~ perp(sK25,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_56024]) ).
tcf(c_57353,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_57355,plain,
( eqangle(sK22,sK25,sK22,sK22,sK22,sK25,sK22,sK22)
| ~ cyclic(sK25,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_57353]) ).
tcf(c_57360,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X1,sK25,X1,X2,X1,X1,X1,X2)
| ~ perp(X0,X1,X1,sK25)
| ~ circle(X0,X1,X2,X1) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_57361,plain,
( eqangle(sK22,sK25,sK22,sK22,sK22,sK22,sK22,sK22)
| ~ circle(sK22,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_57360]) ).
tcf(c_59222,plain,
! [X0: $i,X1: $i] :
( perp(sK22,sK23,sK26,sK24)
| ~ perp(X0,X1,sK26,sK24)
| ~ para(sK22,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_60328,plain,
! [X0: $i] :
( eqangle(sK28,X0,sK28,sK25,sK28,X0,sK28,sK25)
| ~ para(sK28,X0,sK28,X0) ),
inference(instantiation,[status(thm)],[c_44517]) ).
tcf(c_60329,plain,
! [X0: $i] :
( cyclic(X0,sK25,sK28,sK28)
| ~ coll(sK28,sK28,sK25)
| ~ eqangle(sK28,X0,sK28,sK25,sK28,X0,sK28,sK25) ),
inference(instantiation,[status(thm)],[c_39992]) ).
tcf(c_60330,plain,
( eqangle(sK28,sK22,sK28,sK25,sK28,sK22,sK28,sK25)
| ~ para(sK28,sK22,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_60328]) ).
tcf(c_60331,plain,
( cyclic(sK22,sK25,sK28,sK28)
| ~ coll(sK28,sK28,sK25)
| ~ eqangle(sK28,sK22,sK28,sK25,sK28,sK22,sK28,sK25) ),
inference(instantiation,[status(thm)],[c_60329]) ).
tcf(c_60802,plain,
( para(sK27,sK28,sK28,sK27)
| ~ para(sK27,sK28,sK27,sK28) ),
inference(instantiation,[status(thm)],[c_39009]) ).
tcf(c_64896,plain,
! [X0: $i] :
( midp(sK26,X0,sK25)
| ~ midp(sK25,X0,sK26)
| ~ coll(sK26,X0,sK25)
| ~ para(sK25,sK26,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_38332]) ).
tcf(c_64897,plain,
( midp(sK26,sK22,sK25)
| ~ midp(sK25,sK22,sK26)
| ~ coll(sK26,sK22,sK25)
| ~ para(sK25,sK26,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_64896]) ).
tcf(c_66455,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,sK25,X2)
| ~ cyclic(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_66456,plain,
( cyclic(sK22,sK22,sK25,sK22)
| ~ cyclic(sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_66455]) ).
tcf(c_67542,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(sK28,X0,sK28,X1,X2,X0,X2,X1)
| ~ cyclic(X0,X1,sK28,X2) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_67543,plain,
( eqangle(sK28,sK22,sK28,sK22,sK22,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_67542]) ).
tcf(c_69236,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK24,X3,sK23)
| ~ perp(X1,X2,X3,sK23)
| ~ perp(X0,sK24,X1,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_69264,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK22,sK23,X2,X3)
| ~ para(sK22,sK23,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_69266,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK22,sK23,X1,X2)
| ~ midp(X0,sK23,X2)
| ~ midp(X0,sK22,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_69533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK24,X3,X2)
| ~ coll(sK24,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK24,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_71136,plain,
( para(sK28,sK27,sK27,sK28)
| ~ para(sK27,sK28,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_38668]) ).
tcf(c_79751,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X1,sK22,sK23)
| ~ coll(X1,sK22,sK23)
| ~ midp(X0,sK22,X2)
| ~ para(X0,X1,X2,sK23) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_79831,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK23,X1)
| ~ coll(X0,sK23,X1)
| ~ cong(X0,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_79832,plain,
( midp(sK22,sK23,sK22)
| ~ coll(sK22,sK23,sK22)
| ~ cong(sK22,sK23,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_79831]) ).
tcf(c_79833,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK23,X1)
| ~ midp(X0,X1,sK23) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_80977,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,sK24,X2,X1)
| ~ para(X0,sK24,X1,X2) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_81160,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,X0,sK23)
| ~ cong(X0,X1,sK23,X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_81161,plain,
( cong(sK22,sK22,sK22,sK23)
| ~ cong(sK22,sK22,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_81160]) ).
tcf(c_81168,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK23,X0,sK23)
| ~ midp(sK23,X0,X1)
| ~ perp(X0,X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_81170,plain,
( cong(sK22,sK23,sK22,sK23)
| ~ midp(sK23,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_81168]) ).
tcf(c_81658,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X0,X1,X4,sK28,X2,X3,X4,sK28)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_81659,plain,
( eqangle(sK22,sK22,sK22,sK28,sK22,sK22,sK22,sK28)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_81658]) ).
tcf(c_82403,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,sK24,X0,X1,X0,sK24)
| ~ para(X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_82405,plain,
( eqangle(sK22,sK22,sK22,sK24,sK22,sK22,sK22,sK24)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_82403]) ).
tcf(c_91252,plain,
! [X0: $i,X1: $i] :
( cyclic(sK24,sK22,X0,X1)
| ~ cyclic(sK22,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_91253,plain,
( cyclic(sK24,sK22,sK22,sK22)
| ~ cyclic(sK22,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_91252]) ).
tcf(c_91286,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,sK24,X0,X1)
| ~ coll(X0,X1,sK24)
| ~ eqangle(X0,sK22,X0,sK24,X1,sK22,X1,sK24) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_91287,plain,
( cyclic(sK22,sK24,sK22,sK22)
| ~ coll(sK22,sK22,sK24)
| ~ eqangle(sK22,sK22,sK22,sK24,sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_91286]) ).
tcf(c_91821,plain,
! [X0: $i] :
( cong(sK22,sK23,sK22,X0)
| ~ cong(sK22,X0,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_91822,plain,
( cong(sK22,sK23,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_91821]) ).
tcf(c_92771,plain,
! [X0: $i,X1: $i] :
( cong(sK22,X1,sK23,X1)
| ~ midp(X1,sK22,X0)
| ~ perp(sK22,sK23,sK23,X0) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_92772,plain,
( cong(sK22,sK22,sK23,sK22)
| ~ midp(sK22,sK22,sK22)
| ~ perp(sK22,sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_92771]) ).
tcf(c_93428,plain,
( midp(sK23,sK22,sK23)
| ~ midp(sK22,sK22,sK22)
| ~ coll(sK23,sK22,sK23)
| ~ para(sK22,sK23,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_79751]) ).
tcf(c_94205,plain,
! [X0: $i] :
( midp(sK21,X0,sK23)
| ~ midp(sK20,X0,sK22)
| ~ coll(sK21,X0,sK23) ),
inference(superposition,[status(thm)],[c_163,c_94]) ).
tcf(c_94209,plain,
! [X0: $i] :
( midp(sK23,X0,sK21)
| ~ midp(sK22,X0,sK20)
| ~ coll(sK23,X0,sK21) ),
inference(superposition,[status(thm)],[c_18954,c_94]) ).
tcf(c_94215,plain,
! [X0: $i] :
( midp(sK23,X0,sK23)
| ~ midp(sK22,X0,sK22)
| ~ coll(sK23,X0,sK23) ),
inference(superposition,[status(thm)],[c_40961,c_94]) ).
tcf(c_94235,plain,
! [X0: $i] :
( midp(sK24,X0,sK24)
| ~ midp(sK25,X0,sK25)
| ~ coll(sK24,X0,sK24) ),
inference(superposition,[status(thm)],[c_22596,c_94]) ).
tcf(c_94238,plain,
! [X0: $i] :
( midp(sK22,X0,sK20)
| ~ midp(sK20,X0,sK22)
| ~ coll(sK22,X0,sK20) ),
inference(superposition,[status(thm)],[c_20097,c_94]) ).
tcf(c_94245,plain,
! [X0: $i] :
( midp(sK25,X0,sK24)
| ~ midp(sK24,X0,sK25)
| ~ coll(sK25,X0,sK24) ),
inference(superposition,[status(thm)],[c_22617,c_94]) ).
tcf(c_94248,plain,
! [X0: $i] :
( midp(sK26,X0,sK26)
| ~ midp(sK24,X0,sK24)
| ~ coll(sK26,X0,sK26) ),
inference(superposition,[status(thm)],[c_22647,c_94]) ).
tcf(c_94249,plain,
( midp(sK26,sK22,sK26)
| ~ midp(sK24,sK22,sK24)
| ~ coll(sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_94248]) ).
tcf(c_94261,plain,
( midp(sK25,sK22,sK24)
| ~ midp(sK24,sK22,sK25)
| ~ coll(sK25,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_94245]) ).
tcf(c_94289,plain,
( midp(sK22,sK22,sK20)
| ~ midp(sK20,sK22,sK22)
| ~ coll(sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_94238]) ).
tcf(c_94301,plain,
( midp(sK24,sK22,sK24)
| ~ midp(sK25,sK22,sK25)
| ~ coll(sK24,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_94235]) ).
tcf(c_94641,plain,
! [X0: $i,X1: $i] :
( perp(sK21,sK22,X0,X1)
| ~ cong(sK21,X1,sK22,X1)
| ~ cong(sK21,X0,sK22,X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_94646,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK21,sK22,X2,X3)
| ~ para(sK21,sK22,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_94864,plain,
( perp(sK22,sK23,sK25,sK26)
| ~ perp(sK26,sK25,sK25,sK26)
| ~ para(sK22,sK23,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_55329]) ).
tcf(c_94892,plain,
( para(sK25,sK26,sK22,sK23)
| ~ para(sK22,sK23,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_39368]) ).
tcf(c_95470,plain,
( midp(sK21,sK22,sK23)
| ~ midp(sK20,sK22,sK22) ),
inference(superposition,[status(thm)],[c_30046,c_94205]) ).
tcf(c_98184,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X1,sK23)
| ~ coll(sK25,X1,sK23)
| ~ midp(X0,X1,sK22)
| ~ para(X0,sK25,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_37348]) ).
tcf(c_101359,plain,
( para(sK25,sK24,sK23,sK25)
| ~ para(sK25,sK24,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_43367]) ).
tcf(c_101767,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK21,sK22)
| ~ perp(sK21,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_101768,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,sK21,sK22)
| ~ perp(X2,X3,sK21,sK22)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_101807,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(sK21,X1,sK22,X1)
| ~ cyclic(sK21,X1,X0,sK22)
| ~ cyclic(sK21,X1,X0,X2)
| ~ cyclic(sK21,X1,X0,X1)
| ~ eqangle(X0,sK21,X0,X1,X2,sK22,X2,X1) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_101808,plain,
( cong(sK21,sK22,sK22,sK22)
| ~ cyclic(sK21,sK22,sK22,sK22)
| ~ eqangle(sK22,sK21,sK22,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_101807]) ).
tcf(c_101839,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK21,sK22,X1,X2)
| ~ midp(sK22,X0,X2)
| ~ midp(sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_102475,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK23,sK26,sK25)
| ~ para(sK22,sK23,X0,X1)
| ~ para(X0,X1,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_69264]) ).
tcf(c_102477,plain,
( para(sK22,sK23,sK26,sK25)
| ~ para(sK22,sK23,sK22,sK22)
| ~ para(sK22,sK22,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_102475]) ).
tcf(c_102688,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK23,sK25,sK26)
| ~ para(sK22,sK23,X0,X1)
| ~ para(X0,X1,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_69264]) ).
tcf(c_102691,plain,
( para(sK22,sK23,sK25,sK26)
| ~ para(sK22,sK23,sK22,sK22)
| ~ para(sK22,sK22,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_102688]) ).
tcf(c_102955,plain,
( midp(sK23,sK22,sK21)
| ~ midp(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_29845,c_94209]) ).
tcf(c_111325,plain,
( perp(sK22,sK23,sK26,sK24)
| ~ perp(sK21,sK22,sK26,sK24)
| ~ para(sK22,sK23,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_59222]) ).
tcf(c_111718,plain,
! [X0: $i] :
( midp(sK24,X0,sK25)
| ~ midp(sK25,X0,sK23)
| ~ coll(sK24,X0,sK25)
| ~ para(sK25,sK24,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_38332]) ).
tcf(c_111723,plain,
( midp(sK24,sK22,sK25)
| ~ midp(sK25,sK22,sK23)
| ~ coll(sK24,sK22,sK25)
| ~ para(sK25,sK24,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_111718]) ).
tcf(c_111866,plain,
( midp(sK23,sK22,sK23)
| ~ midp(sK22,sK22,sK22) ),
inference(superposition,[status(thm)],[c_20863,c_94215]) ).
tcf(c_111885,plain,
midp(sK23,sK22,sK23),
inference(global_subsumption_just,[status(thm)],[c_111866,c_165,c_163,c_179,c_204,c_237,c_299,c_310,c_370,c_443,c_897,c_916,c_931,c_1745,c_1909,c_2949,c_2952,c_93428]) ).
tcf(c_112313,plain,
midp(sK23,sK23,sK22),
inference(superposition,[status(thm)],[c_111885,c_59]) ).
tcf(c_112577,plain,
! [X0: $i] :
( para(sK22,sK23,sK21,sK22)
| ~ midp(X0,sK23,sK22)
| ~ midp(X0,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_69266]) ).
tcf(c_114963,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK22,X0,X1)
| ~ midp(sK22,sK23,X1)
| ~ midp(sK21,sK23,X0) ),
inference(instantiation,[status(thm)],[c_101839]) ).
tcf(c_114965,plain,
( para(sK21,sK22,sK22,sK22)
| ~ midp(sK22,sK23,sK22)
| ~ midp(sK21,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_114963]) ).
tcf(c_115153,plain,
! [X0: $i] :
( cyclic(sK20,sK22,X0,sK22)
| ~ cyclic(sK22,sK20,X0,sK22) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_115154,plain,
( cyclic(sK20,sK22,sK22,sK22)
| ~ cyclic(sK22,sK20,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_115153]) ).
tcf(c_115659,plain,
! [X0: $i] :
( cyclic(X0,sK20,X0,sK22)
| ~ coll(X0,sK22,sK20)
| ~ eqangle(X0,X0,X0,sK20,sK22,X0,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_115660,plain,
( cyclic(sK22,sK20,sK22,sK22)
| ~ coll(sK22,sK22,sK20)
| ~ eqangle(sK22,sK22,sK22,sK20,sK22,sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_115659]) ).
tcf(c_116484,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,sK20,X0,sK22,X1,sK20,X1,sK22)
| ~ cyclic(sK20,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_116485,plain,
( eqangle(sK22,sK20,sK22,sK22,sK22,sK20,sK22,sK22)
| ~ cyclic(sK20,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_116484]) ).
tcf(c_116834,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK21,X2,X3,X0,X1,X2,X3)
| ~ para(sK22,sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_116835,plain,
( eqangle(sK22,sK21,sK22,sK22,sK22,sK22,sK22,sK22)
| ~ para(sK22,sK21,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_116834]) ).
tcf(c_119686,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,sK20,X0,X1,X0,sK20)
| ~ para(X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_119688,plain,
( eqangle(sK22,sK22,sK22,sK20,sK22,sK22,sK22,sK20)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_119686]) ).
tcf(c_121881,plain,
! [X0: $i] :
( midp(sK25,X0,sK23)
| ~ midp(sK24,X0,sK22)
| ~ coll(sK25,X0,sK23)
| ~ para(sK24,sK25,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_98184]) ).
tcf(c_121889,plain,
( midp(sK25,sK22,sK23)
| ~ midp(sK24,sK22,sK22)
| ~ coll(sK25,sK22,sK23)
| ~ para(sK24,sK25,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_121881]) ).
tcf(c_121954,plain,
( midp(sK21,sK23,sK22)
| ~ midp(sK21,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_79833]) ).
tcf(c_124405,plain,
( para(sK22,sK23,sK21,sK22)
| ~ midp(sK23,sK23,sK22)
| ~ midp(sK23,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_112577]) ).
tcf(c_125592,plain,
! [X0: $i] :
( cyclic(sK20,sK22,X0,sK20)
| ~ cyclic(sK22,sK20,X0,sK20) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_125593,plain,
( cyclic(sK20,sK22,sK22,sK20)
| ~ cyclic(sK22,sK20,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_125592]) ).
tcf(c_126041,plain,
! [X0: $i] :
( cyclic(sK25,X0,sK28,sK28)
| ~ cyclic(X0,sK25,sK28,sK28) ),
inference(instantiation,[status(thm)],[c_43214]) ).
tcf(c_126043,plain,
( cyclic(sK25,sK22,sK28,sK28)
| ~ cyclic(sK22,sK25,sK28,sK28) ),
inference(instantiation,[status(thm)],[c_126041]) ).
tcf(c_127845,plain,
! [X0: $i,X1: $i] :
( para(X0,sK24,X1,sK23)
| ~ perp(sK21,sK22,X1,sK23)
| ~ perp(X0,sK24,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_69236]) ).
tcf(c_127857,plain,
! [X0: $i] :
( cong(sK25,sK21,sK25,sK22)
| ~ midp(X0,sK21,sK22)
| ~ perp(sK25,X0,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_39801]) ).
tcf(c_127859,plain,
( cong(sK25,sK21,sK25,sK22)
| ~ midp(sK22,sK21,sK22)
| ~ perp(sK25,sK22,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_127857]) ).
tcf(c_127924,plain,
! [X0: $i,X1: $i] :
( para(X0,sK26,X0,X1)
| ~ perp(X0,sK26,sK21,sK22)
| ~ perp(sK21,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_42109]) ).
tcf(c_127926,plain,
( para(sK22,sK26,sK22,sK22)
| ~ perp(sK22,sK26,sK21,sK22)
| ~ perp(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_127924]) ).
tcf(c_128221,plain,
( para(sK25,sK24,sK24,sK26)
| ~ para(sK25,sK24,sK26,sK24) ),
inference(instantiation,[status(thm)],[c_80977]) ).
tcf(c_128458,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK25,X1,sK28,X2)
| ~ cyclic(X0,sK25,X1,sK28)
| ~ cyclic(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_43215]) ).
tcf(c_128459,plain,
( cyclic(sK25,sK22,sK28,sK22)
| ~ cyclic(sK22,sK25,sK22,sK22)
| ~ cyclic(sK22,sK25,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_128458]) ).
tcf(c_133003,plain,
! [X0: $i,X1: $i] :
( perp(sK25,sK24,sK21,sK22)
| ~ perp(X0,X1,sK21,sK22)
| ~ para(sK25,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_101768]) ).
tcf(c_133004,plain,
( perp(sK25,sK24,sK21,sK22)
| ~ perp(sK22,sK22,sK21,sK22)
| ~ para(sK25,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_133003]) ).
tcf(c_136244,plain,
! [X0: $i,X1: $i] :
( perp(sK21,sK22,sK25,sK23)
| ~ perp(X0,X1,sK25,sK23)
| ~ para(sK21,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_94646]) ).
tcf(c_136245,plain,
( perp(sK21,sK22,sK25,sK23)
| ~ perp(sK22,sK22,sK25,sK23)
| ~ para(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_136244]) ).
tcf(c_138315,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK25,X0,sK21,sK22)
| ~ perp(X1,X2,sK21,sK22)
| ~ para(sK25,X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_101768]) ).
tcf(c_138324,plain,
( perp(sK25,sK22,sK21,sK22)
| ~ perp(sK22,sK22,sK21,sK22)
| ~ para(sK25,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_138315]) ).
tcf(c_138987,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,X2,sK25)
| ~ cyclic(X0,X1,sK25,X2) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_138988,plain,
( cyclic(sK22,sK22,sK22,sK25)
| ~ cyclic(sK22,sK22,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_138987]) ).
tcf(c_139350,plain,
! [X0: $i] :
( perp(X0,sK26,sK21,sK22)
| ~ perp(sK21,sK22,X0,sK26) ),
inference(instantiation,[status(thm)],[c_101767]) ).
tcf(c_139354,plain,
( perp(sK22,sK26,sK21,sK22)
| ~ perp(sK21,sK22,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_139350]) ).
tcf(c_140807,plain,
! [X0: $i] :
( midp(sK24,X0,sK26)
| ~ midp(sK25,X0,sK24)
| ~ coll(sK24,X0,sK26)
| ~ para(sK25,sK24,sK24,sK26) ),
inference(instantiation,[status(thm)],[c_69533]) ).
tcf(c_140809,plain,
( midp(sK24,sK22,sK26)
| ~ midp(sK25,sK22,sK24)
| ~ coll(sK24,sK22,sK26)
| ~ para(sK25,sK24,sK24,sK26) ),
inference(instantiation,[status(thm)],[c_140807]) ).
tcf(c_146535,plain,
! [X0: $i] :
( para(sK25,sK24,X0,sK23)
| ~ perp(sK25,sK24,sK21,sK22)
| ~ perp(sK21,sK22,X0,sK23) ),
inference(instantiation,[status(thm)],[c_127845]) ).
tcf(c_148370,plain,
! [X0: $i] :
( cyclic(sK25,sK28,X0,sK28)
| ~ cyclic(sK25,X0,sK28,sK28) ),
inference(instantiation,[status(thm)],[c_44284]) ).
tcf(c_148372,plain,
( cyclic(sK25,sK28,sK22,sK28)
| ~ cyclic(sK25,sK22,sK28,sK28) ),
inference(instantiation,[status(thm)],[c_148370]) ).
tcf(c_148932,plain,
! [X0: $i] :
( perp(sK26,sK25,sK25,sK28)
| ~ cyclic(sK25,X0,sK26,sK28)
| ~ cong(sK25,sK28,X0,sK28)
| ~ cong(sK25,sK26,X0,sK26) ),
inference(instantiation,[status(thm)],[c_37057]) ).
tcf(c_148934,plain,
( perp(sK26,sK25,sK25,sK28)
| ~ cyclic(sK25,sK22,sK26,sK28)
| ~ cong(sK25,sK28,sK22,sK28)
| ~ cong(sK25,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_148932]) ).
tcf(c_151374,plain,
! [X0: $i,X1: $i] :
( cyclic(sK25,X1,sK26,sK28)
| ~ cyclic(X0,sK25,X1,sK28)
| ~ cyclic(X0,sK25,X1,sK26) ),
inference(instantiation,[status(thm)],[c_44291]) ).
tcf(c_151376,plain,
( cyclic(sK25,sK22,sK26,sK28)
| ~ cyclic(sK22,sK25,sK22,sK28)
| ~ cyclic(sK22,sK25,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_151374]) ).
tcf(c_151441,plain,
! [X0: $i] :
( perp(sK21,sK22,X0,sK26)
| ~ cong(sK21,sK26,sK22,sK26)
| ~ cong(sK21,X0,sK22,X0) ),
inference(instantiation,[status(thm)],[c_94641]) ).
tcf(c_151452,plain,
( perp(sK21,sK22,sK22,sK26)
| ~ cong(sK21,sK22,sK22,sK22)
| ~ cong(sK21,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_151441]) ).
tcf(c_158272,plain,
( cong(sK26,sK21,sK26,sK22)
| ~ midp(sK24,sK21,sK22) ),
inference(superposition,[status(thm)],[c_168,c_104]) ).
tcf(c_158276,plain,
( cong(sK21,sK26,sK21,sK24)
| ~ midp(sK22,sK26,sK24) ),
inference(superposition,[status(thm)],[c_21540,c_104]) ).
tcf(c_158282,plain,
( cong(sK22,sK24,sK22,sK26)
| ~ midp(sK21,sK24,sK26) ),
inference(superposition,[status(thm)],[c_21562,c_104]) ).
tcf(c_159410,plain,
( para(sK25,sK24,sK25,sK23)
| ~ perp(sK21,sK22,sK25,sK23)
| ~ perp(sK25,sK24,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_146535]) ).
tcf(c_160108,plain,
! [X0: $i] :
( cong(sK26,X0,sK26,sK22)
| ~ midp(sK24,sK21,sK22)
| ~ midp(sK26,X0,sK21) ),
inference(superposition,[status(thm)],[c_158272,c_19393]) ).
tcf(c_160110,plain,
( cong(sK26,sK22,sK26,sK21)
| ~ midp(sK24,sK21,sK22) ),
inference(superposition,[status(thm)],[c_158272,c_72]) ).
tcf(c_160116,plain,
( cong(sK26,sK22,sK26,sK22)
| ~ midp(sK24,sK21,sK22)
| ~ midp(sK26,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_160108]) ).
tcf(c_163050,plain,
( cong(sK21,sK24,sK21,sK26)
| ~ midp(sK22,sK26,sK24) ),
inference(superposition,[status(thm)],[c_158276,c_72]) ).
tcf(c_164860,plain,
( cong(sK26,sK22,sK21,sK26)
| ~ midp(sK24,sK21,sK22) ),
inference(superposition,[status(thm)],[c_160110,c_71]) ).
tcf(c_171235,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK25,X2,sK28)
| ~ coll(sK25,X2,sK28)
| ~ midp(X0,X2,X1)
| ~ para(X0,sK25,X1,sK28) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_171253,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK25,X0,X1)
| ~ para(X0,X1,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_171263,plain,
! [X0: $i,X1: $i] :
( perp(sK26,sK25,X1,X0)
| ~ perp(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_171485,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK26,sK25)
| ~ perp(X2,X3,sK26,sK25)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_171488,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X1,X2,sK26,sK25)
| ~ midp(X0,X2,sK25)
| ~ midp(X0,X1,sK26) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_171599,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK26,sK25)
| ~ perp(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_171652,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X0,X1)
| ~ coll(sK25,X0,X1)
| ~ cong(sK25,X0,sK25,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_171654,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK25,X3,X2)
| ~ coll(sK25,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_171659,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK25,X1)
| ~ midp(X0,X1,sK25) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_171660,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,sK25,X3)
| ~ midp(X0,sK25,X2)
| ~ coll(X1,sK25,X3)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_171689,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK25,X3,sK28)
| ~ perp(X1,X2,X3,sK28)
| ~ perp(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_171794,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK28)
| ~ coll(X1,X3,sK28)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK28) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_173492,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X1,X2,sK25,sK26)
| ~ midp(X0,X2,sK26)
| ~ midp(X0,X1,sK25) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_173596,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK27)
| ~ para(X0,X1,sK27,sK28) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_173702,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK28,sK25,X3)
| ~ perp(X1,X2,sK25,X3)
| ~ perp(X0,sK28,X1,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_173839,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(sK25,sK26,X0,X1)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(sK25,sK26,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_173929,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK26,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK26,X2,X1)
| ~ para(X0,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_174205,plain,
! [X0: $i] :
( perp(X0,sK28,sK28,sK25)
| ~ perp(sK28,sK25,X0,sK28) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_174206,plain,
( perp(sK22,sK28,sK28,sK25)
| ~ perp(sK28,sK25,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_174205]) ).
tcf(c_174307,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,sK26,X0)
| ~ midp(sK25,X1,sK26)
| ~ midp(X0,X1,X0) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_174644,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,X1,sK27)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK27,X2,X1)
| ~ para(X0,X1,X2,sK27) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_175243,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(X1,X2,X4,sK28)
| ~ cyclic(X1,X2,X0,sK28)
| ~ cyclic(X1,X2,X0,X4)
| ~ cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X4,X3,sK28) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_175505,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X4,sK28,X2,X3)
| ~ para(X4,sK28,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_176169,plain,
! [X0: $i] :
( para(sK26,sK25,X0,sK28)
| ~ perp(sK26,sK25,sK26,sK25)
| ~ perp(sK26,sK25,X0,sK28) ),
inference(instantiation,[status(thm)],[c_171689]) ).
tcf(c_176696,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK25,sK26,X0,X1,X4,X5,X2,X3)
| ~ eqangle(X0,X1,sK25,sK26,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_176887,plain,
! [X0: $i,X1: $i] :
( cyclic(sK25,X0,X1,sK25)
| ~ cyclic(X0,sK25,X1,sK25) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_176888,plain,
( cyclic(sK25,sK22,sK22,sK25)
| ~ cyclic(sK22,sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_176887]) ).
tcf(c_177003,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,X0,sK25,X0,X1,X0,sK25)
| ~ para(X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_177013,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( para(X0,X1,sK28,X2)
| ~ para(X3,X4,X5,X6)
| ~ eqangle(X0,X1,sK28,X2,X3,X4,X5,X6) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_178339,plain,
! [X0: $i,X1: $i] :
( midp(X0,X1,sK26)
| ~ midp(X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_182490,plain,
( para(sK28,sK27,sK28,sK27)
| ~ para(sK28,sK27,sK27,sK28) ),
inference(instantiation,[status(thm)],[c_173596]) ).
tcf(c_183910,plain,
! [X0: $i,X1: $i] :
( cyclic(sK25,sK28,X0,X1)
| ~ cyclic(sK25,X0,sK28,X1) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_183911,plain,
( cyclic(sK25,sK28,sK22,sK22)
| ~ cyclic(sK25,sK22,sK28,sK22) ),
inference(instantiation,[status(thm)],[c_183910]) ).
tcf(c_188480,plain,
( cong(sK21,sK26,sK26,sK22)
| ~ midp(sK24,sK21,sK22) ),
inference(superposition,[status(thm)],[c_164860,c_72]) ).
tcf(c_188934,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK26,X2,sK26,X2)
| ~ para(sK26,X2,X0,X1)
| ~ para(X0,X1,sK26,X2) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_189962,plain,
! [X0: $i] :
( cong(sK22,X0,sK22,sK26)
| ~ midp(sK21,sK24,sK26)
| ~ midp(sK22,X0,sK24) ),
inference(superposition,[status(thm)],[c_158282,c_19393]) ).
tcf(c_189970,plain,
( cong(sK22,sK22,sK22,sK26)
| ~ midp(sK22,sK22,sK24)
| ~ midp(sK21,sK24,sK26) ),
inference(instantiation,[status(thm)],[c_189962]) ).
tcf(c_197203,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK24,X3,X2)
| ~ coll(sK24,X3,X2)
| ~ midp(X0,X3,X1)
| ~ para(X0,sK24,X1,X2) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_207411,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,sK24,X2,X3,X1,sK23,X2,X3)
| ~ para(X0,sK24,X1,sK23) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_207449,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,sK24,X3,X4)
| ~ eqangle(X0,sK24,X1,X2,X3,X4,X1,X2) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_207450,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X4,sK24,X2,X3)
| ~ perp(X4,sK24,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_213278,plain,
( cong(sK21,sK26,sK22,sK26)
| ~ midp(sK24,sK21,sK22) ),
inference(superposition,[status(thm)],[c_188480,c_71]) ).
tcf(c_219269,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK28,X0,sK28,X1)
| ~ para(X2,X0,X2,X1)
| ~ eqangle(sK28,X0,sK28,X1,X2,X0,X2,X1) ),
inference(instantiation,[status(thm)],[c_177013]) ).
tcf(c_219271,plain,
( para(sK28,sK22,sK28,sK22)
| ~ para(sK22,sK22,sK22,sK22)
| ~ eqangle(sK28,sK22,sK28,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_219269]) ).
tcf(c_222107,plain,
! [X0: $i,X1: $i] :
( midp(sK24,X1,sK22)
| ~ coll(sK24,X1,sK22)
| ~ midp(sK25,X1,X0)
| ~ para(sK25,sK24,X0,sK22) ),
inference(instantiation,[status(thm)],[c_197203]) ).
tcf(c_222109,plain,
( midp(sK24,sK22,sK22)
| ~ midp(sK25,sK22,sK22)
| ~ coll(sK24,sK22,sK22)
| ~ para(sK25,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_222107]) ).
tcf(c_225977,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(sK25,sK24,X1,X2,X0,sK23,X1,X2)
| ~ para(sK25,sK24,X0,sK23) ),
inference(instantiation,[status(thm)],[c_207411]) ).
tcf(c_231631,plain,
! [X0: $i] :
( eqangle(sK25,sK24,sK25,sK26,X0,sK23,sK25,sK26)
| ~ para(sK25,sK24,X0,sK23) ),
inference(instantiation,[status(thm)],[c_225977]) ).
tcf(c_231632,plain,
! [X0: $i] :
( eqangle(sK25,sK26,sK25,sK24,sK25,sK26,X0,sK23)
| ~ eqangle(sK25,sK24,sK25,sK26,X0,sK23,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_176696]) ).
tcf(c_231635,plain,
( eqangle(sK25,sK24,sK25,sK26,sK22,sK23,sK25,sK26)
| ~ para(sK25,sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_231631]) ).
tcf(c_231637,plain,
( eqangle(sK25,sK26,sK25,sK24,sK25,sK26,sK22,sK23)
| ~ eqangle(sK25,sK24,sK25,sK26,sK22,sK23,sK25,sK26) ),
inference(instantiation,[status(thm)],[c_231632]) ).
tcf(c_234475,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK25,sK23)
| ~ cong(X0,sK23,X1,sK23)
| ~ cong(X0,sK25,X1,sK25) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_234476,plain,
( perp(sK22,sK22,sK25,sK23)
| ~ cong(sK22,sK23,sK22,sK23)
| ~ cong(sK22,sK25,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_234475]) ).
tcf(c_244228,plain,
! [X0: $i] :
( para(sK25,sK26,sK25,sK24)
| ~ para(sK25,sK26,X0,sK23)
| ~ eqangle(sK25,sK26,sK25,sK24,sK25,sK26,X0,sK23) ),
inference(instantiation,[status(thm)],[c_173839]) ).
tcf(c_244231,plain,
( para(sK25,sK26,sK25,sK24)
| ~ para(sK25,sK26,sK22,sK23)
| ~ eqangle(sK25,sK26,sK25,sK24,sK25,sK26,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_244228]) ).
tcf(c_252285,plain,
! [X0: $i] :
( cyclic(sK24,sK25,X0,sK22)
| ~ coll(X0,sK22,sK25)
| ~ eqangle(X0,sK24,X0,sK25,sK22,sK24,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_252286,plain,
( cyclic(sK24,sK25,sK22,sK22)
| ~ coll(sK22,sK22,sK25)
| ~ eqangle(sK22,sK24,sK22,sK25,sK22,sK24,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_252285]) ).
tcf(c_262735,plain,
! [X0: $i] :
( cyclic(sK24,X0,sK25,sK22)
| ~ cyclic(sK24,sK25,X0,sK22) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_262736,plain,
( cyclic(sK24,sK22,sK25,sK22)
| ~ cyclic(sK24,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_262735]) ).
tcf(c_268755,plain,
( eqangle(sK22,sK24,sK22,sK25,sK22,sK24,sK22,sK25)
| ~ para(sK22,sK24,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_177003]) ).
tcf(c_296899,plain,
! [X0: $i,X1: $i] :
( para(X0,sK24,X0,sK24)
| ~ eqangle(X0,sK24,X0,X1,X0,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_207449]) ).
tcf(c_296900,plain,
! [X0: $i,X1: $i] :
( eqangle(X1,sK24,X1,X0,X1,sK24,X1,X0)
| ~ cyclic(sK24,X0,X1,X1) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_296901,plain,
( para(sK22,sK24,sK22,sK24)
| ~ eqangle(sK22,sK24,sK22,sK22,sK22,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_296899]) ).
tcf(c_296902,plain,
( eqangle(sK22,sK24,sK22,sK22,sK22,sK24,sK22,sK22)
| ~ cyclic(sK24,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_296900]) ).
tcf(c_297000,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK24,X0,X1)
| ~ perp(sK25,sK24,sK22,sK23)
| ~ perp(sK22,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_207450]) ).
tcf(c_297415,plain,
! [X0: $i] :
( midp(sK25,X0,sK26)
| ~ midp(sK25,sK26,X0) ),
inference(instantiation,[status(thm)],[c_178339]) ).
tcf(c_297419,plain,
( midp(sK25,sK22,sK26)
| ~ midp(sK25,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_297415]) ).
tcf(c_298041,plain,
! [X0: $i] :
( midp(sK24,sK21,sK22)
| ~ coll(sK24,sK21,sK22)
| ~ midp(sK25,sK21,X0)
| ~ para(sK25,sK24,X0,sK22) ),
inference(instantiation,[status(thm)],[c_222107]) ).
tcf(c_298043,plain,
( midp(sK24,sK21,sK22)
| ~ midp(sK25,sK21,sK22)
| ~ coll(sK24,sK21,sK22)
| ~ para(sK25,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_298041]) ).
tcf(c_298814,plain,
! [X0: $i] :
( midp(sK26,sK25,X0)
| ~ midp(sK26,X0,sK25) ),
inference(instantiation,[status(thm)],[c_171659]) ).
tcf(c_298819,plain,
( midp(sK26,sK25,sK22)
| ~ midp(sK26,sK22,sK25) ),
inference(instantiation,[status(thm)],[c_298814]) ).
tcf(c_299369,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK25,sK26)
| ~ midp(sK24,X1,sK26)
| ~ midp(sK24,X0,sK25) ),
inference(instantiation,[status(thm)],[c_173492]) ).
tcf(c_299370,plain,
( para(sK22,sK22,sK25,sK26)
| ~ midp(sK24,sK22,sK25)
| ~ midp(sK24,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_299369]) ).
tcf(c_300147,plain,
( para(sK25,sK24,sK25,sK26)
| ~ perp(sK22,sK23,sK25,sK26)
| ~ perp(sK25,sK24,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_297000]) ).
tcf(c_300298,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X1,sK28)
| ~ coll(sK25,X1,sK28)
| ~ midp(sK26,X1,X0)
| ~ para(sK26,sK25,X0,sK28) ),
inference(instantiation,[status(thm)],[c_171235]) ).
tcf(c_300321,plain,
! [X0: $i] :
( para(sK26,sK25,sK26,X0)
| ~ para(sK26,X0,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_171253]) ).
tcf(c_300322,plain,
! [X0: $i] :
( para(sK26,X0,sK26,X0)
| ~ para(sK26,sK25,sK26,X0)
| ~ para(sK26,X0,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_188934]) ).
tcf(c_301021,plain,
! [X0: $i] :
( perp(sK26,sK25,sK28,X0)
| ~ perp(sK26,sK25,X0,sK28) ),
inference(instantiation,[status(thm)],[c_171263]) ).
tcf(c_303255,plain,
( midp(sK26,sK22,sK21)
| ~ midp(sK24,sK21,sK22)
| ~ coll(sK26,sK22,sK21) ),
inference(superposition,[status(thm)],[c_160110,c_116]) ).
tcf(c_303261,plain,
( midp(sK21,sK24,sK26)
| ~ midp(sK22,sK26,sK24)
| ~ coll(sK21,sK24,sK26) ),
inference(superposition,[status(thm)],[c_163050,c_116]) ).
tcf(c_305176,plain,
( perp(sK28,sK25,sK26,sK25)
| ~ perp(sK26,sK25,sK28,sK25) ),
inference(instantiation,[status(thm)],[c_171599]) ).
tcf(c_307013,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,sK28,sK26,sK25)
| ~ perp(X1,X2,sK26,sK25)
| ~ perp(X0,sK28,X1,X2) ),
inference(instantiation,[status(thm)],[c_171485]) ).
tcf(c_307396,plain,
! [X0: $i] :
( midp(sK25,sK21,X0)
| ~ coll(sK25,sK21,X0)
| ~ cong(sK25,sK21,sK25,X0) ),
inference(instantiation,[status(thm)],[c_171652]) ).
tcf(c_307397,plain,
( midp(sK25,sK21,sK22)
| ~ coll(sK25,sK21,sK22)
| ~ cong(sK25,sK21,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_307396]) ).
tcf(c_308918,plain,
! [X0: $i] :
( midp(X0,sK26,sK24)
| ~ midp(X0,sK25,sK25)
| ~ para(sK25,sK24,sK25,sK26)
| ~ para(sK25,sK26,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_173929]) ).
tcf(c_308919,plain,
( midp(sK22,sK26,sK24)
| ~ midp(sK22,sK25,sK25)
| ~ para(sK25,sK24,sK25,sK26)
| ~ para(sK25,sK26,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_308918]) ).
tcf(c_309070,plain,
( para(sK26,sK25,sK25,sK28)
| ~ perp(sK26,sK25,sK25,sK28)
| ~ perp(sK26,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_176169]) ).
tcf(c_310924,plain,
! [X0: $i] :
( midp(sK28,X0,sK28)
| ~ midp(sK26,X0,sK26)
| ~ coll(sK28,X0,sK28)
| ~ para(sK26,sK28,sK26,sK28) ),
inference(instantiation,[status(thm)],[c_171794]) ).
tcf(c_310925,plain,
( midp(sK28,sK22,sK28)
| ~ midp(sK26,sK22,sK26)
| ~ coll(sK28,sK22,sK28)
| ~ para(sK26,sK28,sK26,sK28) ),
inference(instantiation,[status(thm)],[c_310924]) ).
tcf(c_315565,plain,
( para(sK26,sK25,sK26,sK28)
| ~ para(sK26,sK28,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_300321]) ).
tcf(c_317284,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK25,sK26,X2)
| ~ coll(sK25,sK26,X2)
| ~ midp(X0,sK26,X1)
| ~ para(X0,sK25,X1,X2) ),
inference(instantiation,[status(thm)],[c_171654]) ).
tcf(c_317285,plain,
( midp(sK25,sK26,sK22)
| ~ midp(sK22,sK26,sK22)
| ~ coll(sK25,sK26,sK22)
| ~ para(sK22,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_317284]) ).
tcf(c_318118,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X2,sK28,X0,X1)
| ~ para(X2,sK28,sK26,sK25)
| ~ para(sK26,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_175505]) ).
tcf(c_318122,plain,
( para(sK22,sK28,sK22,sK22)
| ~ para(sK22,sK28,sK26,sK25)
| ~ para(sK26,sK25,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_318118]) ).
tcf(c_318342,plain,
! [X0: $i] :
( para(sK26,sK28,sK26,sK25)
| ~ midp(X0,sK28,sK25)
| ~ midp(X0,sK26,sK26) ),
inference(instantiation,[status(thm)],[c_171488]) ).
tcf(c_318344,plain,
( para(sK26,sK28,sK26,sK25)
| ~ midp(sK22,sK28,sK25)
| ~ midp(sK22,sK26,sK26) ),
inference(instantiation,[status(thm)],[c_318342]) ).
tcf(c_320193,plain,
( perp(sK26,sK25,sK28,sK25)
| ~ perp(sK26,sK25,sK25,sK28) ),
inference(instantiation,[status(thm)],[c_301021]) ).
tcf(c_321629,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X1,sK25,sK26)
| ~ coll(X1,sK25,sK26)
| ~ midp(X0,sK25,X2)
| ~ para(X0,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_171660]) ).
tcf(c_321630,plain,
( midp(sK22,sK25,sK26)
| ~ midp(sK22,sK25,sK22)
| ~ coll(sK22,sK25,sK26)
| ~ para(sK22,sK22,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_321629]) ).
tcf(c_327935,plain,
( para(sK26,sK28,sK26,sK28)
| ~ para(sK26,sK28,sK26,sK25)
| ~ para(sK26,sK25,sK26,sK28) ),
inference(instantiation,[status(thm)],[c_300322]) ).
tcf(c_328294,plain,
! [X0: $i] :
( midp(sK25,X0,sK28)
| ~ midp(sK26,X0,sK25)
| ~ coll(sK25,X0,sK28)
| ~ para(sK26,sK25,sK25,sK28) ),
inference(instantiation,[status(thm)],[c_300298]) ).
tcf(c_328300,plain,
( midp(sK25,sK22,sK28)
| ~ midp(sK26,sK22,sK25)
| ~ coll(sK25,sK22,sK28)
| ~ para(sK26,sK25,sK25,sK28) ),
inference(instantiation,[status(thm)],[c_328294]) ).
tcf(c_360289,plain,
! [X0: $i] :
( para(X0,sK28,sK26,sK25)
| ~ perp(sK28,sK25,sK26,sK25)
| ~ perp(X0,sK28,sK28,sK25) ),
inference(instantiation,[status(thm)],[c_307013]) ).
tcf(c_360290,plain,
! [X0: $i,X1: $i] :
( para(X0,sK28,sK25,X1)
| ~ perp(sK28,sK25,sK25,X1)
| ~ perp(X0,sK28,sK28,sK25) ),
inference(instantiation,[status(thm)],[c_173702]) ).
tcf(c_360294,plain,
( para(sK22,sK28,sK25,sK22)
| ~ perp(sK22,sK28,sK28,sK25)
| ~ perp(sK28,sK25,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_360290]) ).
tcf(c_360295,plain,
( para(sK22,sK28,sK26,sK25)
| ~ perp(sK22,sK28,sK28,sK25)
| ~ perp(sK28,sK25,sK26,sK25) ),
inference(instantiation,[status(thm)],[c_360289]) ).
tcf(c_360865,plain,
! [X0: $i] :
( midp(X0,sK27,sK27)
| ~ midp(X0,sK25,sK26)
| ~ para(sK25,sK27,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_174644]) ).
tcf(c_360866,plain,
( midp(sK22,sK27,sK27)
| ~ midp(sK22,sK25,sK26)
| ~ para(sK25,sK27,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_360865]) ).
tcf(c_386083,plain,
! [X0: $i] :
( para(sK25,sK27,sK26,sK27)
| ~ midp(sK27,X0,sK27)
| ~ midp(sK25,X0,sK26) ),
inference(instantiation,[status(thm)],[c_174307]) ).
tcf(c_386085,plain,
( para(sK25,sK27,sK26,sK27)
| ~ midp(sK27,sK22,sK27)
| ~ midp(sK25,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_386083]) ).
tcf(c_394784,plain,
! [X0: $i,X1: $i] :
( cong(sK25,sK28,X1,sK28)
| ~ cyclic(sK25,sK28,X0,sK28)
| ~ cyclic(sK25,sK28,X0,X1)
| ~ cyclic(sK25,sK28,X0,X0)
| ~ eqangle(X0,sK25,X0,sK28,X0,X1,X0,sK28) ),
inference(instantiation,[status(thm)],[c_175243]) ).
tcf(c_394785,plain,
( cong(sK25,sK28,sK22,sK28)
| ~ cyclic(sK25,sK28,sK22,sK22)
| ~ cyclic(sK25,sK28,sK22,sK28)
| ~ eqangle(sK22,sK25,sK22,sK28,sK22,sK22,sK22,sK28) ),
inference(instantiation,[status(thm)],[c_394784]) ).
tcf(c_446352,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK27)
| ~ coll(X1,X3,sK27)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK27) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_446376,plain,
! [X0: $i] :
( cong(X0,sK27,X0,sK27)
| ~ midp(X0,sK27,sK27) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_446377,plain,
( cong(sK22,sK27,sK22,sK27)
| ~ midp(sK22,sK27,sK27) ),
inference(instantiation,[status(thm)],[c_446376]) ).
tcf(c_459579,plain,
! [X0: $i] :
( midp(sK27,X0,sK27)
| ~ midp(sK28,X0,sK28)
| ~ coll(sK27,X0,sK27)
| ~ para(sK28,sK27,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_446352]) ).
tcf(c_459586,plain,
( midp(sK27,sK22,sK27)
| ~ midp(sK28,sK22,sK28)
| ~ coll(sK27,sK22,sK27)
| ~ para(sK28,sK27,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_459579]) ).
tcf(c_459587,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_459586,c_446377,c_394785,c_386085,c_360866,c_360295,c_360294,c_328300,c_327935,c_321630,c_320193,c_318344,c_318122,c_317285,c_315565,c_310925,c_309070,c_308919,c_307397,c_305176,c_303255,c_303261,c_300147,c_299370,c_298819,c_298043,c_297419,c_296902,c_296901,c_268755,c_262736,c_252286,c_244231,c_234476,c_231637,c_231635,c_222109,c_219271,c_213278,c_189970,c_183911,c_182490,c_176888,c_174206,c_160116,c_159410,c_151452,c_151376,c_148934,c_148372,c_140809,c_139354,c_138988,c_138324,c_136245,c_133004,c_128459,c_128221,c_127926,c_127859,c_126043,c_125593,c_124405,c_121954,c_121889,c_119688,c_116835,c_116485,c_115660,c_115154,c_114965,c_112313,c_111723,c_111325,c_102955,c_102691,c_102477,c_101808,c_101359,c_95470,c_94892,c_94864,c_94301,c_94289,c_94261,c_94249,c_92772,c_91822,c_91287,c_91253,c_82405,c_81659,c_81170,c_81161,c_79832,c_71136,c_67543,c_66456,c_64897,c_60802,c_60331,c_60330,c_57361,c_57355,c_56026,c_56015,c_55440,c_53885,c_53884,c_53634,c_53578,c_53291,c_53033,c_53027,c_52703,c_52511,c_52260,c_51304,c_49267,c_47567,c_46898,c_46839,c_44626,c_44526,c_44519,c_44518,c_43860,c_43394,c_43374,c_43355,c_43209,c_43163,c_43162,c_42983,c_42948,c_42075,c_41819,c_41379,c_40406,c_39728,c_39693,c_39492,c_38152,c_37336,c_35753,c_35310,c_35160,c_35146,c_34758,c_33388,c_31711,c_31532,c_31429,c_29322,c_27304,c_26670,c_26354,c_25523,c_25183,c_25062,c_24607,c_24601,c_24602,c_24537,c_24166,c_22503,c_21813,c_19930,c_19922,c_19497,c_18927,c_18557,c_17120,c_16421,c_15616,c_15614,c_15432,c_15431,c_15418,c_15050,c_14495,c_14489,c_14458,c_14045,c_13217,c_11759,c_9957,c_8624,c_8417,c_7954,c_7288,c_7206,c_7132,c_6342,c_5462,c_5056,c_5021,c_4606,c_4460,c_4366,c_4249,c_4193,c_3879,c_3409,c_2952,c_2949,c_2946,c_2836,c_2803,c_2802,c_2754,c_2684,c_2666,c_2665,c_2281,c_2186,c_2065,c_2056,c_2052,c_2035,c_1994,c_1745,c_1613,c_1554,c_1539,c_1509,c_1398,c_1282,c_1277,c_1070,c_1017,c_931,c_906,c_897,c_654,c_646,c_575,c_563,c_483,c_370,c_314,c_310,c_306,c_305,c_303,c_285,c_284,c_277,c_276,c_237,c_204,c_189,c_188,c_184,c_179,c_162,c_163,c_166,c_168,c_165,c_167,c_169]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO658+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 12:43:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 173.87/26.39 % SZS status Started for theBenchmark.p
% 173.87/26.39 % SZS status Theorem for theBenchmark.p
% 173.87/26.39
% 173.87/26.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 173.87/26.39
% 173.87/26.39 % ------ iProver source info
% 173.87/26.39
% 173.87/26.39 % git: date: 2026-07-19 20:42:38 +0200
% 173.87/26.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 173.87/26.39 % git: non_committed_changes: false
% 173.87/26.39
% 173.87/26.39 % ------ Parsing...
% 173.87/26.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 173.87/26.39
% 173.87/26.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 1 0s sf_e %
% 173.87/26.39
% 173.87/26.39 % ------ Preprocessing...%
% 173.87/26.39
% 173.87/26.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 173.87/26.39 % ------ Proving...
% 173.87/26.39 % ------ Problem Properties
% 173.87/26.39
% 173.87/26.39 %
% 173.87/26.39 % clauses 124
% 173.87/26.39 % conjectures 12
% 173.87/26.39 % EPR 87
% 173.87/26.39 % Horn 114
% 173.87/26.39 % unary 12
% 173.87/26.39 % binary 37
% 173.87/26.39 % lits 340
% 173.87/26.39 % lits eq 4
% 173.87/26.39 % fd_pure 0
% 173.87/26.39 % fd_pseudo 0
% 173.87/26.39 % fd_cond 0
% 173.87/26.39 % fd_pseudo_cond 4
% 173.87/26.39 % AC symbols 0
% 173.87/26.39
% 173.87/26.39 % ------ Input Options Time Limit: Unbounded
% 173.87/26.39
% 173.87/26.39
% 173.87/26.39 % ------
% 173.87/26.39 % Current options:
% 173.87/26.39 % ------
% 173.87/26.39
% 173.87/26.39
% 173.87/26.39 %
% 173.87/26.39
% 173.87/26.39 % ------ Proving...
% 173.87/26.39 %
% 173.87/26.39
% 173.87/26.39 % SZS status Theorem for theBenchmark.p
% 173.87/26.39
% 173.87/26.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 173.87/26.40
% 173.87/26.40
%------------------------------------------------------------------------------