%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO559+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 : n017.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:28 PM UTC 2026
% Result : Theorem 57.61s 12.37s
% Output : CNFRefutation 57.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 43
% Syntax : Number of formulae : 543 ( 54 unt; 0 def)
% Number of atoms : 1353 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1524 ( 714 ~; 708 |; 58 &)
% ( 0 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-5 aty)
% Number of variables : 1237 ( 0 sgn1212 !; 25 ?; 473 :)
% 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(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(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(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(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(f47,axiom,
! [X0,X1,X2] :
( cong(X2,X0,X2,X1)
=> eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD46) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( perp(X3,X0,X0,X4)
& circle(X3,X0,X1,X2) )
=> eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD48) ).
fof(f50,axiom,
! [X0,X1,X2,X3,X4] :
( ( eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
& circle(X3,X0,X1,X2) )
=> perp(X3,X0,X0,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD49) ).
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(f54,axiom,
! [X0,X1,X2,X3] :
( ( coll(X3,X0,X2)
& circle(X3,X0,X1,X2) )
=> perp(X0,X1,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD53) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( perp(X3,X2,X0,X1)
& midp(X2,X0,X1) )
=> cong(X3,X0,X3,X1) ),
file('/export/starexec/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(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(f67,axiom,
! [X0,X1,X2] :
( para(X0,X1,X0,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD66) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( coll(X0,X1,X2)
& cong(X0,X1,X0,X2) )
=> midp(X0,X1,X2) ),
file('/export/starexec/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(f87,axiom,
! [X0,X1,X2,X3] :
? [X4] :
( circle(X3,X0,X1,X2)
=> perp(X4,X0,X0,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleX11) ).
fof(f91,axiom,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ( coll(X1,X3,X4)
& perp(X0,X2,X2,X1) )
=> ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleX15) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( coll(X7,X1,X4)
& circle(X3,X1,X7,X9)
& coll(X6,X0,X2)
& circle(X5,X0,X6,X8)
& circle(X5,X0,X1,X4)
& circle(X3,X0,X1,X2) )
=> para(X2,X7,X6,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL012019) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( coll(X7,X1,X4)
& circle(X3,X1,X7,X9)
& coll(X6,X0,X2)
& circle(X5,X0,X6,X8)
& circle(X5,X0,X1,X4)
& circle(X3,X0,X1,X2) )
=> para(X2,X7,X6,X4) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( coll(X7,X1,X4)
& circle(X3,X1,X7,X9)
& coll(X6,X0,X2)
& circle(X5,X0,X6,X8)
& circle(X5,X0,X1,X4)
& circle(X3,X0,X1,X2)
& ~ para(X2,X7,X6,X4) ),
inference(ennf_transformation,[],[f96]) ).
fof(f99,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( coll(X7,X1,X4)
& circle(X3,X1,X7,X9)
& coll(X6,X0,X2)
& circle(X5,X0,X6,X8)
& circle(X5,X0,X1,X4)
& circle(X3,X0,X1,X2)
& ~ para(X2,X7,X6,X4) ),
inference(flattening,[],[f98]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f105,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(flattening,[],[f104]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(ennf_transformation,[],[f46]) ).
fof(f127,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(flattening,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(flattening,[],[f128]) ).
fof(f130,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f131,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f136,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f74]) ).
fof(f137,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(flattening,[],[f136]) ).
fof(f142,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(f143,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,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f146]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f40]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f39]) ).
fof(f150,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(f151,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f9]) ).
fof(f153,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f152]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f157,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
? [X4] :
( ~ circle(X3,X0,X1,X2)
| perp(X4,X0,X0,X3) ),
inference(ennf_transformation,[],[f87]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f164,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f163]) ).
fof(f169,plain,
! [X0,X1,X2,X3,X4] :
( ~ eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| perp(X3,X0,X0,X4) ),
inference(ennf_transformation,[],[f50]) ).
fof(f170,plain,
! [X0,X1,X2,X3,X4] :
( ~ eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| perp(X3,X0,X0,X4) ),
inference(flattening,[],[f169]) ).
fof(f171,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(f172,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,[],[f171]) ).
fof(f177,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(f178,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,[],[f177]) ).
fof(f179,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(f180,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f179]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f56]) ).
fof(f182,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(flattening,[],[f181]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(ennf_transformation,[],[f53]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(flattening,[],[f183]) ).
fof(f185,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f186,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f187,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f188,plain,
! [X0,X1,X2] :
( ~ cong(X2,X0,X2,X1)
| eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(f189,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(f190,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f189]) ).
fof(f191,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f192,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f193,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f196,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(ennf_transformation,[],[f21]) ).
fof(f197,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(f198,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(ennf_transformation,[],[f19]) ).
fof(f206,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f207,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(flattening,[],[f206]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f209,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f208]) ).
fof(f212,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f41]) ).
fof(f216,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f217,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f218,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f13]) ).
fof(f219,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f218]) ).
fof(f220,plain,
( coll(sK7,sK1,sK4)
& circle(sK3,sK1,sK7,sK9)
& coll(sK6,sK0,sK2)
& circle(sK5,sK0,sK6,sK8)
& circle(sK5,sK0,sK1,sK4)
& circle(sK3,sK0,sK1,sK2)
& ~ para(sK2,sK7,sK6,sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X9,sK9)],[f99]) ).
fof(f223,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(sK12(X0,X1,X2,X3,X4),X0,X3,X4)
& coll(sK12(X0,X1,X2,X3,X4),X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X5,sK12(X0,X1,X2,X3,X4))],[f105]) ).
fof(f236,plain,
! [X0,X1,X2,X3] :
( ~ circle(X3,X0,X1,X2)
| perp(sK25(X0,X1,X2,X3),X0,X0,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X4,sK25(X0,X1,X2,X3))],[f162]) ).
fof(f239,plain,
coll(sK7,sK1,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f241,plain,
coll(sK6,sK0,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f242,plain,
circle(sK5,sK0,sK6,sK8),
inference(cnf_transformation,[],[f220]) ).
fof(f243,plain,
circle(sK5,sK0,sK1,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f244,plain,
circle(sK3,sK0,sK1,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f245,plain,
~ para(sK2,sK7,sK6,sK4),
inference(cnf_transformation,[],[f220]) ).
fof(f250,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| perp(sK12(X0,X1,X2,X3,X4),X0,X3,X4) ),
inference(cnf_transformation,[],[f223]) ).
fof(f268,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f122]) ).
fof(f269,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f271,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(cnf_transformation,[],[f127]) ).
fof(f272,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f273,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f130]) ).
fof(f274,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f281,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f137]) ).
fof(f284,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,[],[f143]) ).
fof(f285,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f145]) ).
fof(f286,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f148]) ).
fof(f288,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f149]) ).
fof(f289,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,[],[f151]) ).
fof(f290,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f153]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f156]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f157]) ).
fof(f296,plain,
! [X2,X3,X0,X1] :
( ~ circle(X3,X0,X1,X2)
| perp(sK25(X0,X1,X2,X3),X0,X0,X3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f297,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f164]) ).
fof(f300,plain,
! [X2,X3,X0,X1,X4] :
( ~ eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| perp(X3,X0,X0,X4) ),
inference(cnf_transformation,[],[f170]) ).
fof(f301,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,[],[f172]) ).
fof(f304,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,[],[f178]) ).
fof(f305,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f180]) ).
fof(f306,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f182]) ).
fof(f307,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f184]) ).
fof(f308,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f185]) ).
fof(f309,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f186]) ).
fof(f310,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f187]) ).
fof(f311,plain,
! [X2,X0,X1] :
( ~ cong(X2,X0,X2,X1)
| eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f188]) ).
fof(f312,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,[],[f190]) ).
fof(f313,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f191]) ).
fof(f314,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f192]) ).
fof(f315,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
fof(f317,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(cnf_transformation,[],[f196]) ).
fof(f318,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,[],[f197]) ).
fof(f319,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(cnf_transformation,[],[f198]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f207]) ).
fof(f326,plain,
! [X2,X3,X0,X1] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f209]) ).
fof(f328,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f212]) ).
fof(f331,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f216]) ).
fof(f332,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f217]) ).
fof(f333,plain,
! [X2,X3,X0,X1,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_49,negated_conjecture,
~ para(sK2,sK7,sK6,sK4),
inference(cnf_transformation,[],[f245]) ).
tcf(c_50,negated_conjecture,
circle(sK3,sK0,sK1,sK2),
inference(cnf_transformation,[],[f244]) ).
tcf(c_51,negated_conjecture,
circle(sK5,sK0,sK1,sK4),
inference(cnf_transformation,[],[f243]) ).
tcf(c_52,negated_conjecture,
circle(sK5,sK0,sK6,sK8),
inference(cnf_transformation,[],[f242]) ).
tcf(c_53,negated_conjecture,
coll(sK6,sK0,sK2),
inference(cnf_transformation,[],[f241]) ).
tcf(c_55,negated_conjecture,
coll(sK7,sK1,sK4),
inference(cnf_transformation,[],[f239]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(sK12(X0,X2,X1,X3,X4),X0,X3,X4)
| ~ coll(X2,X3,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_81,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,[],[f271]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( para(X0,X1,X2,X3)
| ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_94,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,[],[f284]) ).
tcf(c_95,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,[],[f285]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X3,X0,X4,X2)
| ~ midp(X3,X1,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X2,X3) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_99,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,[],[f289]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK25(X1,X2,X3,X0),X1,X1,X0)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X1,X2,X2,X3)
| ~ coll(X0,X1,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(X4,X0,X0,X1)
| ~ circle(X4,X0,X2,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X0,X3,X2) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X1,X4,X1,X2,X3,X1,X3,X2)
| ~ perp(X0,X1,X1,X4)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_114,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,[],[f304]) ).
tcf(c_115,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,[],[f305]) ).
tcf(c_116,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,[],[f306]) ).
tcf(c_117,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,[],[f307]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,X1,X2,X1,X2,X0,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_122,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,[],[f312]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X2,X3,X0,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_127,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,[],[f317]) ).
tcf(c_128,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,[],[f318]) ).
tcf(c_129,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,[],[f319]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X1,X2,X4,X5)
| ~ cyclic(X1,X2,X0,X5)
| ~ cyclic(X1,X2,X0,X4)
| ~ cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X4,X3,X5) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X0,X3)
| ~ coll(X0,X3,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_138,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,[],[f328]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X3,X4)
| ~ cong(X0,X1,X0,X4)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_153,plain,
( midp(sK0,sK0,sK0)
| ~ coll(sK0,sK0,sK0)
| ~ cong(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_155,plain,
( perp(sK0,sK0,sK0,sK0)
| ~ cong(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_797,plain,
perp(sK25(sK0,sK1,sK2,sK3),sK0,sK0,sK3),
inference(resolution,[status(thm)],[c_50,c_106]) ).
tcf(c_843,plain,
perp(sK25(sK0,sK1,sK4,sK5),sK0,sK0,sK5),
inference(resolution,[status(thm)],[c_51,c_106]) ).
tcf(c_2368,plain,
( coll(sK0,sK6,sK2)
| ~ coll(sK6,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_2369,plain,
( coll(sK1,sK7,sK4)
| ~ coll(sK7,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_2370,plain,
( coll(sK6,sK2,sK0)
| ~ coll(sK6,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_2448,plain,
! [X0: $i] :
( coll(sK2,X0,sK0)
| ~ coll(sK0,sK6,sK2)
| ~ coll(sK0,sK6,X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_2449,plain,
( coll(sK0,sK2,sK6)
| ~ coll(sK0,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_2451,plain,
( coll(sK2,sK0,sK0)
| ~ coll(sK0,sK6,sK0)
| ~ coll(sK0,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_2448]) ).
tcf(c_2476,plain,
( coll(sK1,sK4,sK7)
| ~ coll(sK1,sK7,sK4) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_2502,plain,
! [X0: $i] :
( coll(sK0,X0,sK6)
| ~ coll(sK6,sK2,sK0)
| ~ coll(sK6,sK2,X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_2504,plain,
( coll(sK2,sK6,sK0)
| ~ coll(sK6,sK2,sK0) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_2505,plain,
( coll(sK0,sK0,sK6)
| ~ coll(sK6,sK2,sK0) ),
inference(instantiation,[status(thm)],[c_2502]) ).
tcf(c_2546,plain,
( perp(sK25(sK0,sK1,sK2,sK3),sK0,sK3,sK0)
| ~ perp(sK25(sK0,sK1,sK2,sK3),sK0,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_2547,plain,
( perp(sK0,sK3,sK25(sK0,sK1,sK2,sK3),sK0)
| ~ perp(sK25(sK0,sK1,sK2,sK3),sK0,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_2564,plain,
( perp(sK25(sK0,sK1,sK4,sK5),sK0,sK5,sK0)
| ~ perp(sK25(sK0,sK1,sK4,sK5),sK0,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_2565,plain,
( perp(sK0,sK5,sK25(sK0,sK1,sK4,sK5),sK0)
| ~ perp(sK25(sK0,sK1,sK4,sK5),sK0,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_2703,plain,
! [X0: $i,X1: $i] :
( midp(sK0,sK2,sK6)
| ~ coll(sK0,sK2,sK6)
| ~ midp(X0,sK2,X1)
| ~ para(X0,sK0,X1,sK6) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_2704,plain,
( midp(sK0,sK2,sK6)
| ~ midp(sK0,sK2,sK0)
| ~ coll(sK0,sK2,sK6)
| ~ para(sK0,sK0,sK0,sK6) ),
inference(instantiation,[status(thm)],[c_2703]) ).
tcf(c_2727,plain,
( coll(sK4,sK1,sK7)
| ~ coll(sK1,sK4,sK7) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_2752,plain,
! [X0: $i] :
( coll(sK0,X0,sK2)
| ~ coll(sK2,sK6,sK0)
| ~ coll(sK2,sK6,X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_2755,plain,
( coll(sK0,sK0,sK2)
| ~ coll(sK2,sK6,sK0) ),
inference(instantiation,[status(thm)],[c_2752]) ).
tcf(c_2810,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK3,X0,X1)
| ~ perp(sK0,sK3,sK25(sK0,sK1,sK2,sK3),sK0)
| ~ perp(sK25(sK0,sK1,sK2,sK3),sK0,X0,X1) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_2816,plain,
( coll(sK2,sK2,sK0)
| ~ coll(sK0,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_2448]) ).
tcf(c_2836,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK5,X0,X1)
| ~ perp(sK0,sK5,sK25(sK0,sK1,sK4,sK5),sK0)
| ~ perp(sK25(sK0,sK1,sK4,sK5),sK0,X0,X1) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_2905,plain,
! [X0: $i] :
( coll(sK0,sK6,X0)
| ~ coll(sK0,X0,sK6) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_2907,plain,
( coll(sK0,sK6,sK0)
| ~ coll(sK0,sK0,sK6) ),
inference(instantiation,[status(thm)],[c_2905]) ).
tcf(c_3003,plain,
coll(sK1,sK7,sK4),
inference(superposition,[status(thm)],[c_55,c_83]) ).
tcf(c_3032,plain,
coll(sK6,sK2,sK0),
inference(superposition,[status(thm)],[c_53,c_84]) ).
tcf(c_3033,plain,
coll(sK7,sK4,sK1),
inference(superposition,[status(thm)],[c_55,c_84]) ).
tcf(c_3039,plain,
coll(sK7,sK4,sK1),
inference(superposition,[status(thm)],[c_55,c_84]) ).
tcf(c_3158,plain,
! [X0: $i] :
( coll(sK0,X0,sK2)
| ~ coll(sK2,sK2,sK0)
| ~ coll(sK2,sK2,X0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_3513,plain,
! [X0: $i] :
( coll(sK0,X0,sK6)
| ~ coll(sK6,sK2,X0) ),
inference(superposition,[status(thm)],[c_3032,c_82]) ).
tcf(c_3514,plain,
! [X0: $i] :
( coll(sK1,X0,sK7)
| ~ coll(sK7,sK4,X0) ),
inference(superposition,[status(thm)],[c_3033,c_82]) ).
tcf(c_3562,plain,
! [X0: $i] :
( coll(sK4,X0,sK1)
| ~ coll(sK1,sK7,X0) ),
inference(superposition,[status(thm)],[c_3003,c_82]) ).
tcf(c_3564,plain,
! [X0: $i] :
( coll(sK1,X0,sK7)
| ~ coll(sK7,sK4,X0) ),
inference(superposition,[status(thm)],[c_3039,c_82]) ).
tcf(c_4094,plain,
coll(sK0,sK0,sK6),
inference(superposition,[status(thm)],[c_3032,c_3513]) ).
tcf(c_4103,plain,
coll(sK0,sK6,sK0),
inference(superposition,[status(thm)],[c_4094,c_84]) ).
tcf(c_4150,plain,
coll(sK1,sK1,sK7),
inference(superposition,[status(thm)],[c_3033,c_3514]) ).
tcf(c_4155,plain,
coll(sK1,sK1,sK7),
inference(superposition,[status(thm)],[c_3039,c_3564]) ).
tcf(c_4381,plain,
! [X0: $i] :
( coll(sK0,X0,sK0)
| ~ coll(sK0,sK6,X0) ),
inference(superposition,[status(thm)],[c_4103,c_82]) ).
tcf(c_4387,plain,
( coll(sK0,sK0,sK0)
| ~ coll(sK0,sK6,sK0) ),
inference(instantiation,[status(thm)],[c_4381]) ).
tcf(c_4431,plain,
! [X0: $i] :
( coll(sK7,X0,sK1)
| ~ coll(sK1,sK1,X0) ),
inference(superposition,[status(thm)],[c_4150,c_82]) ).
tcf(c_4432,plain,
coll(sK1,sK7,sK1),
inference(superposition,[status(thm)],[c_4150,c_84]) ).
tcf(c_4436,plain,
( coll(sK7,sK0,sK1)
| ~ coll(sK1,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_4431]) ).
tcf(c_4438,plain,
coll(sK1,sK7,sK1),
inference(superposition,[status(thm)],[c_4155,c_84]) ).
tcf(c_4472,plain,
! [X0: $i,X1: $i] :
( coll(X0,sK2,X1)
| ~ coll(sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_4473,plain,
( coll(sK0,sK2,sK0)
| ~ coll(sK2,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_4472]) ).
tcf(c_4646,plain,
coll(sK7,sK1,sK1),
inference(superposition,[status(thm)],[c_4432,c_83]) ).
tcf(c_4654,plain,
coll(sK4,sK1,sK1),
inference(superposition,[status(thm)],[c_4438,c_3562]) ).
tcf(c_4657,plain,
! [X0: $i] :
( coll(sK7,sK1,X0)
| ~ coll(sK7,X0,sK1) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_4658,plain,
( coll(sK7,sK1,sK0)
| ~ coll(sK7,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_4657]) ).
tcf(c_4685,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X2,sK7,X0)
| ~ coll(X0,X1,sK7)
| ~ coll(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_4688,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X2,sK2,X0)
| ~ coll(X0,X1,sK2)
| ~ coll(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_4778,plain,
( perp(sK0,sK1,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_50,c_107]) ).
tcf(c_4779,plain,
( perp(sK0,sK1,sK1,sK4)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_51,c_107]) ).
tcf(c_4780,plain,
( perp(sK0,sK6,sK6,sK8)
| ~ coll(sK5,sK0,sK8) ),
inference(superposition,[status(thm)],[c_52,c_107]) ).
tcf(c_4796,plain,
( perp(sK0,sK1,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_50,c_107]) ).
tcf(c_4797,plain,
( perp(sK0,sK1,sK1,sK4)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_51,c_107]) ).
tcf(c_5018,plain,
( perp(sK0,sK1,sK2,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_4778,c_119]) ).
tcf(c_5019,plain,
( perp(sK1,sK2,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_4778,c_118]) ).
tcf(c_5036,plain,
( cong(sK0,sK1,sK0,sK2)
| ~ midp(sK1,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_4796,c_116]) ).
tcf(c_5038,plain,
( perp(sK1,sK2,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_4796,c_118]) ).
tcf(c_5092,plain,
! [X0: $i] :
( cong(sK0,X0,sK1,X0)
| ~ coll(sK5,sK0,sK4)
| ~ midp(X0,sK0,sK4) ),
inference(superposition,[status(thm)],[c_4779,c_117]) ).
tcf(c_5112,plain,
( cong(sK0,sK1,sK0,sK4)
| ~ midp(sK1,sK1,sK4)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_4797,c_116]) ).
tcf(c_5114,plain,
( perp(sK1,sK4,sK0,sK1)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_4797,c_118]) ).
tcf(c_5168,plain,
( perp(sK0,sK6,sK8,sK6)
| ~ coll(sK5,sK0,sK8) ),
inference(superposition,[status(thm)],[c_4780,c_119]) ).
tcf(c_5300,plain,
( cong(sK0,sK2,sK0,sK1)
| ~ midp(sK1,sK2,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5018,c_116]) ).
tcf(c_5302,plain,
( perp(sK2,sK1,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5018,c_118]) ).
tcf(c_5350,plain,
( cong(sK1,sK0,sK1,sK1)
| ~ midp(sK2,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5019,c_116]) ).
tcf(c_5351,plain,
( perp(sK1,sK2,sK1,sK0)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5019,c_119]) ).
tcf(c_5363,plain,
( perp(sK1,sK2,sK1,sK0)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5038,c_119]) ).
tcf(c_5514,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK1,X0,X1)
| ~ coll(sK3,sK0,sK2)
| ~ perp(sK1,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_4778,c_100]) ).
tcf(c_5519,plain,
! [X0: $i,X1: $i] :
( para(sK1,sK2,X0,X1)
| ~ coll(sK3,sK0,sK2)
| ~ perp(sK0,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_5019,c_100]) ).
tcf(c_5565,plain,
! [X0: $i,X1: $i] :
( para(sK0,sK1,X0,X1)
| ~ coll(sK3,sK0,sK2)
| ~ perp(sK1,sK2,X0,X1) ),
inference(superposition,[status(thm)],[c_4796,c_100]) ).
tcf(c_5570,plain,
! [X0: $i,X1: $i] :
( para(sK1,sK2,X0,X1)
| ~ coll(sK3,sK0,sK2)
| ~ perp(sK0,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_5038,c_100]) ).
tcf(c_5892,plain,
( para(sK0,sK3,sK0,sK3)
| ~ perp(sK0,sK3,sK25(sK0,sK1,sK2,sK3),sK0)
| ~ perp(sK25(sK0,sK1,sK2,sK3),sK0,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_2810]) ).
tcf(c_5893,plain,
( para(sK0,sK3,sK3,sK0)
| ~ perp(sK0,sK3,sK25(sK0,sK1,sK2,sK3),sK0)
| ~ perp(sK25(sK0,sK1,sK2,sK3),sK0,sK3,sK0) ),
inference(instantiation,[status(thm)],[c_2810]) ).
tcf(c_5897,plain,
( para(sK0,sK5,sK5,sK0)
| ~ perp(sK0,sK5,sK25(sK0,sK1,sK4,sK5),sK0)
| ~ perp(sK25(sK0,sK1,sK4,sK5),sK0,sK5,sK0) ),
inference(instantiation,[status(thm)],[c_2836]) ).
tcf(c_6085,plain,
! [X0: $i] :
( coll(sK1,X0,sK7)
| ~ coll(sK7,sK1,X0) ),
inference(superposition,[status(thm)],[c_4646,c_82]) ).
tcf(c_6091,plain,
( coll(sK1,sK0,sK7)
| ~ coll(sK7,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_6085]) ).
tcf(c_6131,plain,
coll(sK1,sK4,sK1),
inference(superposition,[status(thm)],[c_4654,c_83]) ).
tcf(c_6186,plain,
( coll(sK3,sK0,sK2)
| ~ coll(sK3,sK2,sK0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_6223,plain,
( coll(sK5,sK0,sK4)
| ~ coll(sK5,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_6227,plain,
( coll(sK5,sK0,sK8)
| ~ coll(sK5,sK8,sK0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_6368,plain,
! [X0: $i,X1: $i] :
( eqangle(sK0,sK3,X0,X1,sK0,sK3,X0,X1)
| ~ para(sK0,sK3,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_6371,plain,
( eqangle(sK0,sK3,sK0,sK0,sK0,sK3,sK0,sK0)
| ~ para(sK0,sK3,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_6368]) ).
tcf(c_6375,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X2,X3)
| ~ para(sK0,sK3,sK0,sK3)
| ~ eqangle(X0,X1,X2,X3,sK0,sK3,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_6376,plain,
( para(sK0,sK0,sK0,sK0)
| ~ para(sK0,sK3,sK0,sK3)
| ~ eqangle(sK0,sK0,sK0,sK0,sK0,sK3,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_6375]) ).
tcf(c_6467,plain,
! [X0: $i,X1: $i] :
( coll(sK1,X0,X1)
| ~ coll(X0,sK1,X1) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_6516,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X2,sK1)
| ~ coll(sK1,X0,X2)
| ~ coll(sK1,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_6517,plain,
( coll(sK0,sK0,sK1)
| ~ coll(sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_6516]) ).
tcf(c_6592,plain,
( midp(sK0,sK1,sK2)
| ~ midp(sK1,sK1,sK2)
| ~ coll(sK0,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5036,c_78]) ).
tcf(c_6658,plain,
! [X0: $i,X1: $i] :
( coll(X0,X1,sK7)
| ~ coll(X0,sK7,X1) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_6659,plain,
( coll(sK0,sK0,sK7)
| ~ coll(sK0,sK7,sK0) ),
inference(instantiation,[status(thm)],[c_6658]) ).
tcf(c_6684,plain,
! [X0: $i] :
( cong(sK0,X0,X0,sK1)
| ~ coll(sK5,sK0,sK4)
| ~ midp(X0,sK0,sK4) ),
inference(superposition,[status(thm)],[c_5092,c_124]) ).
tcf(c_6697,plain,
( cong(sK0,sK0,sK0,sK1)
| ~ midp(sK0,sK0,sK4)
| ~ coll(sK5,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_6684]) ).
tcf(c_6833,plain,
( midp(sK0,sK1,sK4)
| ~ midp(sK1,sK1,sK4)
| ~ coll(sK5,sK0,sK4)
| ~ coll(sK0,sK1,sK4) ),
inference(superposition,[status(thm)],[c_5112,c_78]) ).
tcf(c_6966,plain,
! [X0: $i] :
( coll(X0,sK2,sK7)
| ~ coll(sK2,X0,sK7) ),
inference(instantiation,[status(thm)],[c_4472]) ).
tcf(c_6968,plain,
( coll(sK0,sK2,sK7)
| ~ coll(sK2,sK0,sK7) ),
inference(instantiation,[status(thm)],[c_6966]) ).
tcf(c_7570,plain,
( para(sK3,sK0,sK0,sK3)
| ~ para(sK0,sK3,sK3,sK0) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_7609,plain,
( para(sK5,sK0,sK0,sK5)
| ~ para(sK0,sK5,sK5,sK0) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_7709,plain,
( coll(sK7,sK1,sK2)
| ~ coll(sK7,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_4657]) ).
tcf(c_7738,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X2,sK4)
| ~ coll(sK4,X0,X2)
| ~ coll(sK4,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_7739,plain,
( coll(sK0,sK0,sK4)
| ~ coll(sK4,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_7738]) ).
tcf(c_7846,plain,
( coll(sK0,sK1,sK2)
| ~ coll(sK2,sK2,sK1)
| ~ coll(sK2,sK2,sK0) ),
inference(instantiation,[status(thm)],[c_3158]) ).
tcf(c_8081,plain,
! [X0: $i] :
( coll(X0,sK7,sK4)
| ~ coll(sK4,sK1,sK7)
| ~ coll(sK4,sK1,X0) ),
inference(instantiation,[status(thm)],[c_4685]) ).
tcf(c_8082,plain,
( coll(sK0,sK7,sK4)
| ~ coll(sK4,sK1,sK0)
| ~ coll(sK4,sK1,sK7) ),
inference(instantiation,[status(thm)],[c_8081]) ).
tcf(c_8106,plain,
! [X0: $i] :
( coll(sK2,sK2,sK1)
| ~ coll(sK1,X0,sK2) ),
inference(instantiation,[status(thm)],[c_4688]) ).
tcf(c_8116,plain,
! [X0: $i,X1: $i] :
( coll(X1,sK7,X0)
| ~ coll(X0,sK2,sK7)
| ~ coll(X0,sK2,X1) ),
inference(instantiation,[status(thm)],[c_4685]) ).
tcf(c_8120,plain,
( coll(sK0,sK7,sK0)
| ~ coll(sK0,sK2,sK0)
| ~ coll(sK0,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_8116]) ).
tcf(c_8144,plain,
( para(sK0,sK1,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5019,c_5514]) ).
tcf(c_8980,plain,
! [X0: $i] :
( coll(sK1,X0,sK1)
| ~ coll(sK1,sK4,X0) ),
inference(superposition,[status(thm)],[c_6131,c_82]) ).
tcf(c_11254,plain,
( cong(sK2,sK0,sK2,sK1)
| ~ midp(sK1,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5302,c_116]) ).
tcf(c_11290,plain,
( para(sK0,sK1,sK1,sK0)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5351,c_5514]) ).
tcf(c_11310,plain,
( para(sK0,sK1,sK1,sK0)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_5363,c_5565]) ).
tcf(c_11454,plain,
! [X0: $i,X1: $i] :
( coll(sK1,X0,X1)
| ~ para(sK1,X0,sK1,X1) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_11455,plain,
( coll(sK1,sK0,sK0)
| ~ para(sK1,sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_11454]) ).
tcf(c_11464,plain,
! [X0: $i,X1: $i] :
( coll(sK4,X0,X1)
| ~ para(sK4,X0,sK4,X1) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_11465,plain,
( coll(sK4,sK0,sK0)
| ~ para(sK4,sK0,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_11464]) ).
tcf(c_11556,plain,
! [X0: $i,X1: $i] :
( coll(sK3,X0,X1)
| ~ para(sK3,X0,sK3,X1) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_11557,plain,
( coll(sK3,sK0,sK0)
| ~ para(sK3,sK0,sK3,sK0) ),
inference(instantiation,[status(thm)],[c_11556]) ).
tcf(c_11558,plain,
! [X0: $i,X1: $i] :
( coll(sK5,X0,X1)
| ~ para(sK5,X0,sK5,X1) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_11559,plain,
( coll(sK5,sK0,sK0)
| ~ para(sK5,sK0,sK5,sK0) ),
inference(instantiation,[status(thm)],[c_11558]) ).
tcf(c_11722,plain,
! [X0: $i,X1: $i] :
( para(X1,sK1,X0,sK4)
| ~ para(X0,sK4,X1,sK1) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_11723,plain,
( para(sK0,sK1,sK0,sK4)
| ~ para(sK0,sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_11722]) ).
tcf(c_12033,plain,
! [X0: $i] :
( coll(sK3,sK2,sK0)
| ~ coll(sK0,X0,sK3)
| ~ coll(sK0,X0,sK2) ),
inference(instantiation,[status(thm)],[c_4688]) ).
tcf(c_12034,plain,
( coll(sK3,sK2,sK0)
| ~ coll(sK0,sK0,sK3)
| ~ coll(sK0,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_12033]) ).
tcf(c_12468,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,X0,X0)
| ~ coll(X0,X0,X2)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_97,c_136]) ).
tcf(c_12481,plain,
( cyclic(sK0,sK0,sK0,sK0)
| ~ coll(sK0,sK0,sK0)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_12468]) ).
tcf(c_12553,plain,
! [X0: $i] :
( coll(sK8,X0,sK0)
| ~ para(sK8,X0,sK8,sK0) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_12554,plain,
( coll(sK8,sK0,sK0)
| ~ para(sK8,sK0,sK8,sK0) ),
inference(instantiation,[status(thm)],[c_12553]) ).
tcf(c_12732,plain,
! [X0: $i] :
( midp(sK1,X0,sK1)
| ~ coll(sK3,sK0,sK2)
| ~ midp(sK0,X0,sK0)
| ~ coll(sK1,X0,sK1) ),
inference(superposition,[status(thm)],[c_8144,c_81]) ).
tcf(c_12735,plain,
! [X0: $i] :
( midp(X0,sK1,sK1)
| ~ coll(sK3,sK0,sK2)
| ~ midp(X0,sK0,sK0)
| ~ para(sK0,sK1,sK0,sK1) ),
inference(superposition,[status(thm)],[c_8144,c_94]) ).
tcf(c_12737,plain,
( coll(sK0,sK1,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_8144,c_79]) ).
tcf(c_12748,plain,
( midp(sK1,sK0,sK1)
| ~ midp(sK0,sK0,sK0)
| ~ coll(sK1,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_12732]) ).
tcf(c_12749,plain,
( midp(sK0,sK1,sK1)
| ~ midp(sK0,sK0,sK0)
| ~ coll(sK3,sK0,sK2)
| ~ para(sK0,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_12735]) ).
tcf(c_13102,plain,
( para(sK1,sK0,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_11310,c_102]) ).
tcf(c_13132,plain,
( para(sK1,sK0,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_11290,c_102]) ).
tcf(c_15817,plain,
( coll(sK2,sK2,sK1)
| ~ coll(sK1,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_8106]) ).
tcf(c_16066,plain,
! [X0: $i] :
( eqangle(sK0,X0,sK0,sK6,sK8,sK0,sK8,sK6)
| ~ perp(sK5,sK0,sK0,X0) ),
inference(superposition,[status(thm)],[c_52,c_111]) ).
tcf(c_16819,plain,
! [X0: $i] :
( eqangle(sK0,X0,sK8,sK0,sK0,sK6,sK8,sK6)
| ~ perp(sK5,sK0,sK0,X0) ),
inference(superposition,[status(thm)],[c_16066,c_127]) ).
tcf(c_17777,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK0,sK3,X0,X1,sK0,sK3)
| ~ eqangle(sK0,sK3,X0,X1,sK0,sK3,X0,X1) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_17781,plain,
( eqangle(sK0,sK0,sK0,sK3,sK0,sK0,sK0,sK3)
| ~ eqangle(sK0,sK3,sK0,sK0,sK0,sK3,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_17777]) ).
tcf(c_19862,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X2,sK8)
| ~ coll(sK8,X0,X2)
| ~ coll(sK8,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_19863,plain,
( coll(sK0,sK0,sK8)
| ~ coll(sK8,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_19862]) ).
tcf(c_21407,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X4,X2,X3)
| ~ midp(X0,X1,X4)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_120,c_143]) ).
tcf(c_21932,plain,
! [X0: $i] :
( perp(sK0,X0,sK8,sK0)
| ~ perp(sK0,sK6,sK8,sK6)
| ~ perp(sK5,sK0,sK0,X0) ),
inference(superposition,[status(thm)],[c_16819,c_114]) ).
tcf(c_21945,plain,
( perp(sK0,sK0,sK8,sK0)
| ~ perp(sK5,sK0,sK0,sK0)
| ~ perp(sK0,sK6,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_21932]) ).
tcf(c_28171,plain,
! [X0: $i,X1: $i] :
( coll(sK0,X1,sK3)
| ~ coll(sK3,X0,sK0)
| ~ coll(sK3,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_28172,plain,
( coll(sK0,sK0,sK3)
| ~ coll(sK3,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_28171]) ).
tcf(c_28862,plain,
! [X0: $i] :
( coll(sK1,X0,sK1)
| ~ coll(X0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_6467]) ).
tcf(c_28863,plain,
( coll(sK1,sK0,sK1)
| ~ coll(sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_28862]) ).
tcf(c_31011,plain,
! [X0: $i] :
( midp(sK0,X0,sK1)
| ~ coll(sK3,sK0,sK2)
| ~ midp(sK1,X0,sK0)
| ~ coll(sK0,X0,sK1) ),
inference(superposition,[status(thm)],[c_13132,c_81]) ).
tcf(c_31013,plain,
( para(sK1,sK0,sK1,sK0)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_13132,c_103]) ).
tcf(c_31034,plain,
( midp(sK0,sK0,sK1)
| ~ midp(sK1,sK0,sK0)
| ~ coll(sK0,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_31011]) ).
tcf(c_31043,plain,
( para(sK1,sK0,sK1,sK0)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_13102,c_103]) ).
tcf(c_32823,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X2,sK5)
| ~ coll(sK5,X0,X2)
| ~ coll(sK5,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_32824,plain,
( coll(sK0,sK0,sK5)
| ~ coll(sK5,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_32823]) ).
tcf(c_33823,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,X3,X2,X3)
| ~ cyclic(X1,X3,X0,X3)
| ~ cyclic(X1,X3,X0,X2)
| ~ cyclic(X1,X3,X0,X0)
| ~ para(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_97,c_135]) ).
tcf(c_33967,plain,
( cong(sK0,sK0,sK0,sK0)
| ~ cyclic(sK0,sK0,sK0,sK0)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_33823]) ).
tcf(c_35578,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_120,c_123]) ).
tcf(c_36073,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X0,X1)
| ~ cong(X0,X0,X0,X1) ),
inference(superposition,[status(thm)],[c_121,c_98]) ).
tcf(c_36089,plain,
( perp(sK0,sK1,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_50,c_107]) ).
tcf(c_36090,plain,
( perp(sK0,sK1,sK1,sK4)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_51,c_107]) ).
tcf(c_36091,plain,
( perp(sK0,sK6,sK6,sK8)
| ~ coll(sK5,sK0,sK8) ),
inference(superposition,[status(thm)],[c_52,c_107]) ).
tcf(c_36212,plain,
( perp(sK0,sK1,sK2,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36089,c_119]) ).
tcf(c_36213,plain,
( perp(sK1,sK2,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36089,c_118]) ).
tcf(c_36284,plain,
( cong(sK0,sK2,sK0,sK1)
| ~ midp(sK1,sK2,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36212,c_116]) ).
tcf(c_36296,plain,
( cong(sK1,sK0,sK1,sK1)
| ~ midp(sK2,sK0,sK1)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36213,c_116]) ).
tcf(c_36340,plain,
! [X0: $i] :
( cong(sK0,X0,sK6,X0)
| ~ coll(sK5,sK0,sK8)
| ~ midp(X0,sK0,sK8) ),
inference(superposition,[status(thm)],[c_36091,c_117]) ).
tcf(c_36392,plain,
! [X0: $i,X1: $i] :
( para(sK1,sK2,X0,X1)
| ~ coll(sK3,sK0,sK2)
| ~ perp(sK0,sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_36213,c_100]) ).
tcf(c_36454,plain,
( para(sK1,sK2,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36089,c_36392]) ).
tcf(c_36455,plain,
( para(sK1,sK2,sK1,sK4)
| ~ coll(sK5,sK0,sK4)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36090,c_36392]) ).
tcf(c_36613,plain,
( coll(sK1,sK2,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_36454,c_79]) ).
tcf(c_36725,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(X0,X1,X2,X4)
| ~ midp(X2,X3,X4)
| ~ cong(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_120,c_122]) ).
tcf(c_36726,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(X0,X1,X2,X4)
| ~ midp(X2,X4,X3)
| ~ cong(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_35578,c_122]) ).
tcf(c_37170,plain,
! [X0: $i] :
( cong(sK0,X0,X0,sK6)
| ~ coll(sK5,sK0,sK8)
| ~ midp(X0,sK0,sK8) ),
inference(superposition,[status(thm)],[c_36340,c_124]) ).
tcf(c_38196,plain,
( para(sK0,sK0,sK0,sK6)
| ~ midp(sK0,sK0,sK8)
| ~ coll(sK5,sK0,sK8) ),
inference(superposition,[status(thm)],[c_37170,c_36073]) ).
tcf(c_39150,plain,
! [X0: $i] :
( midp(X0,sK2,sK2)
| ~ coll(sK3,sK0,sK2)
| ~ midp(X0,sK1,sK1)
| ~ para(sK1,sK2,sK1,sK2) ),
inference(superposition,[status(thm)],[c_36454,c_94]) ).
tcf(c_39203,plain,
( midp(sK0,sK2,sK2)
| ~ midp(sK0,sK1,sK1)
| ~ coll(sK3,sK0,sK2)
| ~ para(sK1,sK2,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_39150]) ).
tcf(c_39502,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X1,X1)
| ~ cyclic(X1,X2,X1,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_138,c_110]) ).
tcf(c_42827,plain,
! [X0: $i] :
( coll(sK5,sK4,sK0)
| ~ coll(sK0,X0,sK5)
| ~ coll(sK0,X0,sK4) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_42828,plain,
( coll(sK5,sK4,sK0)
| ~ coll(sK0,sK0,sK5)
| ~ coll(sK0,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_42827]) ).
tcf(c_42852,plain,
! [X0: $i] :
( coll(sK5,sK8,sK0)
| ~ coll(sK0,X0,sK8)
| ~ coll(sK0,X0,sK5) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_42853,plain,
( coll(sK5,sK8,sK0)
| ~ coll(sK0,sK0,sK8)
| ~ coll(sK0,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_42852]) ).
tcf(c_42956,plain,
! [X0: $i] :
( coll(sK1,X0,sK2)
| ~ coll(X0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_42957,plain,
( coll(sK1,sK0,sK2)
| ~ coll(sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_42956]) ).
tcf(c_43016,plain,
! [X0: $i,X1: $i] :
( coll(X1,sK2,sK1)
| ~ coll(sK1,X0,sK2)
| ~ coll(sK1,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_43255,plain,
! [X0: $i] :
( coll(sK2,X0,sK1)
| ~ coll(sK2,sK1,X0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_43256,plain,
( coll(sK2,sK0,sK1)
| ~ coll(sK2,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_43255]) ).
tcf(c_43273,plain,
! [X0: $i] :
( coll(sK4,X0,sK1)
| ~ coll(sK4,sK1,X0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_43274,plain,
( coll(sK4,sK0,sK1)
| ~ coll(sK4,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_43273]) ).
tcf(c_44220,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X2,sK7)
| ~ coll(sK7,X0,X2)
| ~ coll(sK7,X0,X1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_46791,plain,
! [X0: $i,X1: $i] :
( coll(sK2,sK1,X0)
| ~ coll(X0,X1,sK1)
| ~ coll(X0,X1,sK2) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_46792,plain,
( coll(sK2,sK1,sK0)
| ~ coll(sK0,sK0,sK1)
| ~ coll(sK0,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_46791]) ).
tcf(c_46860,plain,
! [X0: $i,X1: $i] :
( coll(sK4,sK1,X0)
| ~ coll(X0,X1,sK1)
| ~ coll(X0,X1,sK4) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_46861,plain,
( coll(sK4,sK1,sK0)
| ~ coll(sK0,sK0,sK1)
| ~ coll(sK0,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_46860]) ).
tcf(c_54868,plain,
! [X0: $i] :
( coll(sK2,X0,sK7)
| ~ coll(sK7,sK1,sK2)
| ~ coll(sK7,sK1,X0) ),
inference(instantiation,[status(thm)],[c_44220]) ).
tcf(c_54869,plain,
( coll(sK2,sK0,sK7)
| ~ coll(sK7,sK1,sK0)
| ~ coll(sK7,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_54868]) ).
tcf(c_57097,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(X2,sK8,X0,X1)
| ~ perp(X0,X1,X2,sK8) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_57098,plain,
( perp(sK0,sK8,sK0,sK0)
| ~ perp(sK0,sK0,sK0,sK8) ),
inference(instantiation,[status(thm)],[c_57097]) ).
tcf(c_57215,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(X0,X1,X2,sK8)
| ~ perp(X0,X1,sK8,X2) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_57216,plain,
( perp(sK0,sK0,sK0,sK8)
| ~ perp(sK0,sK0,sK8,sK0) ),
inference(instantiation,[status(thm)],[c_57215]) ).
tcf(c_57489,plain,
! [X0: $i] :
( coll(sK7,sK2,sK1)
| ~ coll(sK1,X0,sK7)
| ~ coll(sK1,X0,sK2) ),
inference(instantiation,[status(thm)],[c_43016]) ).
tcf(c_57490,plain,
( coll(sK7,sK2,sK1)
| ~ coll(sK1,sK0,sK7)
| ~ coll(sK1,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_57489]) ).
tcf(c_57546,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X0,sK7)
| ~ perp(X2,X3,X0,sK7)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_57547,plain,
( para(sK0,sK0,sK0,sK7)
| ~ perp(sK0,sK0,sK0,sK0)
| ~ perp(sK0,sK0,sK0,sK7) ),
inference(instantiation,[status(thm)],[c_57546]) ).
tcf(c_57595,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X0,sK8)
| ~ perp(X2,X3,X0,sK8)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_57596,plain,
( para(sK0,sK0,sK0,sK8)
| ~ perp(sK0,sK0,sK0,sK8)
| ~ perp(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_57595]) ).
tcf(c_57611,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,sK8,X2,X3)
| ~ perp(X2,sK8,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_57612,plain,
( para(sK0,sK8,sK0,sK0)
| ~ perp(sK0,sK8,sK0,sK0)
| ~ perp(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_57611]) ).
tcf(c_57805,plain,
! [X0: $i] :
( para(X0,sK1,X0,sK2)
| ~ para(X0,sK2,X0,sK1) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_57806,plain,
( para(sK0,sK1,sK0,sK2)
| ~ para(sK0,sK2,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_57805]) ).
tcf(c_58162,plain,
! [X0: $i,X1: $i] :
( para(sK3,X0,sK3,X1)
| ~ para(sK3,X0,X1,sK3) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_58163,plain,
( para(sK3,sK0,sK3,sK0)
| ~ para(sK3,sK0,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_58162]) ).
tcf(c_58164,plain,
! [X0: $i,X1: $i] :
( para(sK5,X0,sK5,X1)
| ~ para(sK5,X0,X1,sK5) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_58165,plain,
( para(sK5,sK0,sK5,sK0)
| ~ para(sK5,sK0,sK0,sK5) ),
inference(instantiation,[status(thm)],[c_58164]) ).
tcf(c_58763,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,sK4,X1,X0,X2,sK4,X1)
| ~ para(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_58764,plain,
( eqangle(sK0,sK0,sK4,sK0,sK0,sK0,sK4,sK0)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_58763]) ).
tcf(c_58779,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,sK8,X1,X0,X2,sK8,X1)
| ~ para(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_58780,plain,
( eqangle(sK0,sK0,sK8,sK0,sK0,sK0,sK8,sK0)
| ~ para(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_58779]) ).
tcf(c_59161,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK4,X0,sK4,sK0)
| ~ eqangle(sK4,X0,X1,X2,sK4,sK0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_59162,plain,
( para(sK4,sK0,sK4,sK0)
| ~ eqangle(sK4,sK0,sK0,sK0,sK4,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_59161]) ).
tcf(c_59163,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK8,X0,sK8,sK0)
| ~ eqangle(sK8,X0,X1,X2,sK8,sK0,X1,X2) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_59164,plain,
( para(sK8,sK0,sK8,sK0)
| ~ eqangle(sK8,sK0,sK0,sK0,sK8,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_59163]) ).
tcf(c_60142,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK0,sK3,sK0,sK3)
| ~ eqangle(X0,X1,sK0,sK3,X2,X3,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_60143,plain,
( eqangle(sK0,sK0,sK0,sK0,sK0,sK3,sK0,sK3)
| ~ eqangle(sK0,sK0,sK0,sK3,sK0,sK0,sK0,sK3) ),
inference(instantiation,[status(thm)],[c_60142]) ).
tcf(c_60271,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(sK4,sK0,X1,sK0,sK4,X0,X1,X2)
| ~ eqangle(sK4,sK0,sK4,X0,X1,sK0,X1,X2) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_60272,plain,
( eqangle(sK4,sK0,sK0,sK0,sK4,sK0,sK0,sK0)
| ~ eqangle(sK4,sK0,sK4,sK0,sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_60271]) ).
tcf(c_60276,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(sK8,sK0,X1,sK0,sK8,X0,X1,X2)
| ~ eqangle(sK8,sK0,sK8,X0,X1,sK0,X1,X2) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_60277,plain,
( eqangle(sK8,sK0,sK0,sK0,sK8,sK0,sK0,sK0)
| ~ eqangle(sK8,sK0,sK8,sK0,sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_60276]) ).
tcf(c_60349,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,X0,X2,sK4,X1,sK4,X2)
| ~ eqangle(X0,X1,sK4,X1,X0,X2,sK4,X2) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_60350,plain,
( eqangle(sK0,sK0,sK0,sK0,sK4,sK0,sK4,sK0)
| ~ eqangle(sK0,sK0,sK4,sK0,sK0,sK0,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_60349]) ).
tcf(c_60357,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,X0,X2,sK8,X1,sK8,X2)
| ~ eqangle(X0,X1,sK8,X1,X0,X2,sK8,X2) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_60358,plain,
( eqangle(sK0,sK0,sK0,sK0,sK8,sK0,sK8,sK0)
| ~ eqangle(sK0,sK0,sK8,sK0,sK0,sK0,sK8,sK0) ),
inference(instantiation,[status(thm)],[c_60357]) ).
tcf(c_60759,plain,
! [X0: $i,X1: $i] :
( eqangle(sK4,sK0,sK4,X1,X0,sK0,X0,X1)
| ~ eqangle(X0,sK0,X0,X1,sK4,sK0,sK4,X1) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_60760,plain,
( eqangle(sK4,sK0,sK4,sK0,sK0,sK0,sK0,sK0)
| ~ eqangle(sK0,sK0,sK0,sK0,sK4,sK0,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_60759]) ).
tcf(c_60764,plain,
! [X0: $i,X1: $i] :
( eqangle(sK8,sK0,sK8,X1,X0,sK0,X0,X1)
| ~ eqangle(X0,sK0,X0,X1,sK8,sK0,sK8,X1) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_60765,plain,
( eqangle(sK8,sK0,sK8,sK0,sK0,sK0,sK0,sK0)
| ~ eqangle(sK0,sK0,sK0,sK0,sK8,sK0,sK8,sK0) ),
inference(instantiation,[status(thm)],[c_60764]) ).
tcf(c_62301,plain,
para(sK1,sK0,sK1,sK0),
inference(global_subsumption_just,[status(thm)],[c_31043,c_53,c_797,c_2370,c_2504,c_2547,c_2546,c_2755,c_5893,c_6186,c_7570,c_11557,c_12034,c_28172,c_31013,c_58163]) ).
tcf(c_62306,plain,
para(sK1,sK0,sK0,sK1),
inference(superposition,[status(thm)],[c_62301,c_103]) ).
tcf(c_63266,plain,
para(sK0,sK1,sK1,sK0),
inference(superposition,[status(thm)],[c_62306,c_102]) ).
tcf(c_65528,plain,
para(sK0,sK1,sK0,sK1),
inference(superposition,[status(thm)],[c_63266,c_103]) ).
tcf(c_65568,plain,
coll(sK0,sK1,sK1),
inference(superposition,[status(thm)],[c_65528,c_79]) ).
tcf(c_65758,plain,
coll(sK1,sK0,sK1),
inference(superposition,[status(thm)],[c_65568,c_83]) ).
tcf(c_65762,plain,
coll(sK1,sK1,sK0),
inference(superposition,[status(thm)],[c_65758,c_84]) ).
tcf(c_66418,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK12(X0,X2,X1,sK2,sK7),X0,sK2,sK7)
| ~ coll(X2,sK2,sK7)
| ~ perp(X0,X1,X1,X2) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_66420,plain,
( perp(sK12(sK0,sK0,sK0,sK2,sK7),sK0,sK2,sK7)
| ~ coll(sK0,sK2,sK7)
| ~ perp(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_66418]) ).
tcf(c_69344,plain,
( cyclic(sK0,sK1,sK0,sK4)
| ~ cyclic(sK0,sK1,sK4,sK0) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_71316,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK1,X1)
| ~ midp(X0,X1,sK1) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_71317,plain,
( midp(sK0,sK1,sK0)
| ~ midp(sK0,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_71316]) ).
tcf(c_71322,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK7,X1)
| ~ midp(X0,X1,sK7) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_71323,plain,
( midp(sK0,sK7,sK0)
| ~ midp(sK0,sK0,sK7) ),
inference(instantiation,[status(thm)],[c_71322]) ).
tcf(c_72331,plain,
! [X0: $i,X1: $i] :
( midp(sK1,X0,X1)
| ~ coll(sK1,X0,X1)
| ~ cong(sK1,X0,sK1,X1) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_72332,plain,
( midp(sK1,sK0,sK0)
| ~ coll(sK1,sK0,sK0)
| ~ cong(sK1,sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_72331]) ).
tcf(c_72412,plain,
! [X0: $i] :
( midp(sK2,X0,sK1)
| ~ coll(sK2,X0,sK1)
| ~ cong(sK2,X0,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_72413,plain,
( midp(sK2,sK0,sK1)
| ~ coll(sK2,sK0,sK1)
| ~ cong(sK2,sK0,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_72412]) ).
tcf(c_72566,plain,
! [X0: $i] :
( para(sK2,sK7,sK6,sK4)
| ~ midp(X0,sK7,sK4)
| ~ midp(X0,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_72567,plain,
( para(sK2,sK7,sK6,sK4)
| ~ midp(sK0,sK7,sK4)
| ~ midp(sK0,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_72566]) ).
tcf(c_73279,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,sK4,X2,sK1)
| ~ midp(sK4,X1,sK1)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_73280,plain,
( para(sK0,sK4,sK0,sK1)
| ~ midp(sK0,sK0,sK0)
| ~ midp(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_73279]) ).
tcf(c_73537,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,sK2,X2,sK1)
| ~ midp(sK2,X1,sK1)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_73538,plain,
( para(sK0,sK2,sK0,sK1)
| ~ midp(sK0,sK0,sK0)
| ~ midp(sK2,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_73537]) ).
tcf(c_74803,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X1,sK7)
| ~ cong(X0,sK7,X1,sK7)
| ~ cong(X0,X1,X1,X1) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_74804,plain,
( perp(sK0,sK0,sK0,sK7)
| ~ cong(sK0,sK0,sK0,sK0)
| ~ cong(sK0,sK7,sK0,sK7) ),
inference(instantiation,[status(thm)],[c_74803]) ).
tcf(c_75376,plain,
! [X0: $i,X1: $i] :
( para(sK1,sK2,X0,X1)
| ~ perp(sK0,sK1,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5570,c_53,c_797,c_2370,c_2504,c_2547,c_2546,c_2755,c_5519,c_5893,c_6186,c_7570,c_11557,c_12034,c_28172,c_58163]) ).
tcf(c_75383,plain,
( para(sK1,sK2,sK1,sK2)
| ~ coll(sK3,sK0,sK2) ),
inference(superposition,[status(thm)],[c_4796,c_75376]) ).
tcf(c_75384,plain,
( para(sK1,sK2,sK1,sK4)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_4797,c_75376]) ).
tcf(c_75423,plain,
para(sK1,sK2,sK1,sK2),
inference(global_subsumption_just,[status(thm)],[c_75383,c_53,c_797,c_2370,c_2504,c_2547,c_2546,c_2755,c_5893,c_6186,c_7570,c_11557,c_12034,c_28172,c_36454,c_58163]) ).
tcf(c_75428,plain,
para(sK1,sK2,sK2,sK1),
inference(superposition,[status(thm)],[c_75423,c_103]) ).
tcf(c_75590,plain,
para(sK2,sK1,sK1,sK2),
inference(superposition,[status(thm)],[c_75428,c_102]) ).
tcf(c_75737,plain,
! [X0: $i] :
( cong(X0,sK7,X0,sK7)
| ~ midp(X0,sK7,sK7) ),
inference(instantiation,[status(thm)],[c_120]) ).
tcf(c_75738,plain,
( cong(sK0,sK7,sK0,sK7)
| ~ midp(sK0,sK7,sK7) ),
inference(instantiation,[status(thm)],[c_75737]) ).
tcf(c_75912,plain,
para(sK1,sK2,sK1,sK4),
inference(global_subsumption_just,[status(thm)],[c_75384,c_53,c_797,c_843,c_2370,c_2504,c_2547,c_2546,c_2565,c_2564,c_2755,c_5892,c_5893,c_5897,c_6186,c_6223,c_6371,c_6376,c_7570,c_7609,c_7739,c_11465,c_11557,c_11559,c_12034,c_17781,c_28172,c_32824,c_36455,c_42828,c_58163,c_58165,c_58764,c_59162,c_60143,c_60272,c_60350,c_60760]) ).
tcf(c_75916,plain,
! [X0: $i,X1: $i] :
( perp(sK1,sK2,X0,X1)
| ~ perp(sK1,sK4,X0,X1) ),
inference(superposition,[status(thm)],[c_75912,c_99]) ).
tcf(c_75919,plain,
para(sK1,sK4,sK1,sK2),
inference(superposition,[status(thm)],[c_75912,c_102]) ).
tcf(c_75920,plain,
coll(sK1,sK2,sK4),
inference(superposition,[status(thm)],[c_75912,c_79]) ).
tcf(c_76125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK7)
| ~ coll(X1,X3,sK7)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK7) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_76126,plain,
( midp(sK0,sK0,sK7)
| ~ midp(sK0,sK0,sK0)
| ~ coll(sK0,sK0,sK7)
| ~ para(sK0,sK0,sK0,sK7) ),
inference(instantiation,[status(thm)],[c_76125]) ).
tcf(c_76134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK4)
| ~ coll(X1,X3,sK4)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK4) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_76135,plain,
( midp(sK0,sK0,sK4)
| ~ midp(sK0,sK0,sK0)
| ~ coll(sK0,sK0,sK4)
| ~ para(sK0,sK0,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_76134]) ).
tcf(c_76242,plain,
coll(sK1,sK4,sK2),
inference(superposition,[status(thm)],[c_75920,c_84]) ).
tcf(c_76476,plain,
para(sK1,sK4,sK2,sK1),
inference(superposition,[status(thm)],[c_75919,c_103]) ).
tcf(c_77014,plain,
coll(sK1,sK2,sK1),
inference(superposition,[status(thm)],[c_76242,c_8980]) ).
tcf(c_77404,plain,
( perp(sK1,sK2,sK0,sK1)
| ~ coll(sK5,sK0,sK4) ),
inference(superposition,[status(thm)],[c_5114,c_75916]) ).
tcf(c_77423,plain,
perp(sK1,sK2,sK0,sK1),
inference(global_subsumption_just,[status(thm)],[c_77404,c_53,c_797,c_2370,c_2504,c_2547,c_2546,c_2755,c_5019,c_5893,c_6186,c_7570,c_11557,c_12034,c_28172,c_58163]) ).
tcf(c_77427,plain,
perp(sK1,sK2,sK1,sK0),
inference(superposition,[status(thm)],[c_77423,c_119]) ).
tcf(c_77914,plain,
! [X0: $i] :
( midp(sK1,X0,sK2)
| ~ midp(sK2,X0,sK1)
| ~ coll(sK1,X0,sK2) ),
inference(superposition,[status(thm)],[c_75590,c_81]) ).
tcf(c_77931,plain,
( midp(sK1,sK0,sK2)
| ~ midp(sK2,sK0,sK1)
| ~ coll(sK1,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_77914]) ).
tcf(c_77956,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK1,sK2)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK1,X1,sK2)
| ~ para(X0,sK2,X1,sK1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_77957,plain,
( midp(sK0,sK1,sK2)
| ~ midp(sK0,sK0,sK0)
| ~ para(sK0,sK1,sK0,sK2)
| ~ para(sK0,sK2,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_77956]) ).
tcf(c_77958,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK1,sK4)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK1,X1,sK4)
| ~ para(X0,sK4,X1,sK1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_77959,plain,
( midp(sK0,sK1,sK4)
| ~ midp(sK0,sK0,sK0)
| ~ para(sK0,sK1,sK0,sK4)
| ~ para(sK0,sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_77958]) ).
tcf(c_78070,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,X1,sK8)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK8,X2,X1)
| ~ para(X0,X1,X2,sK8) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_78071,plain,
( midp(sK0,sK0,sK8)
| ~ midp(sK0,sK0,sK0)
| ~ para(sK0,sK8,sK0,sK0)
| ~ para(sK0,sK0,sK0,sK8) ),
inference(instantiation,[status(thm)],[c_78070]) ).
tcf(c_78258,plain,
coll(sK1,sK1,sK2),
inference(superposition,[status(thm)],[c_77014,c_84]) ).
tcf(c_78274,plain,
( cong(sK0,sK2,sK0,sK1)
| ~ midp(sK1,sK2,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_36284,c_53,c_797,c_2370,c_2504,c_2547,c_2546,c_2755,c_5300,c_5893,c_6186,c_7570,c_11557,c_12034,c_28172,c_58163]) ).
tcf(c_78476,plain,
cong(sK1,sK0,sK1,sK1),
inference(global_subsumption_just,[status(thm)],[c_36296,c_53,c_153,c_797,c_2370,c_2504,c_2505,c_2547,c_2546,c_2755,c_2907,c_4387,c_5350,c_5892,c_5893,c_6186,c_6371,c_6376,c_6517,c_7570,c_11254,c_11455,c_11557,c_12034,c_12481,c_12737,c_12748,c_17781,c_28172,c_28863,c_31013,c_33967,c_43256,c_46792,c_58163,c_60143,c_72413]) ).
tcf(c_80115,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK2,X1)
| ~ coll(X0,sK2,X1)
| ~ cong(X0,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_80116,plain,
( midp(sK0,sK2,sK0)
| ~ coll(sK0,sK2,sK0)
| ~ cong(sK0,sK2,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_80115]) ).
tcf(c_80383,plain,
! [X0: $i] :
( midp(sK4,X0,sK1)
| ~ midp(sK1,X0,sK2)
| ~ coll(sK4,X0,sK1) ),
inference(superposition,[status(thm)],[c_76476,c_81]) ).
tcf(c_80400,plain,
( midp(sK4,sK0,sK1)
| ~ midp(sK1,sK0,sK2)
| ~ coll(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_80383]) ).
tcf(c_82347,plain,
perp(sK1,sK0,sK1,sK2),
inference(superposition,[status(thm)],[c_77427,c_118]) ).
tcf(c_82616,plain,
midp(sK0,sK1,sK2),
inference(global_subsumption_just,[status(thm)],[c_6592,c_53,c_153,c_797,c_2370,c_2504,c_2505,c_2547,c_2546,c_2755,c_2907,c_4387,c_5892,c_5893,c_6186,c_6371,c_6376,c_6517,c_7570,c_11254,c_11455,c_11557,c_12034,c_12481,c_12737,c_12748,c_17781,c_28172,c_28863,c_31013,c_33967,c_43256,c_46792,c_57806,c_58163,c_60143,c_72413,c_73538,c_77957]) ).
tcf(c_82693,plain,
midp(sK0,sK1,sK4),
inference(global_subsumption_just,[status(thm)],[c_6833,c_53,c_153,c_797,c_2368,c_2370,c_2504,c_2505,c_2547,c_2546,c_2755,c_2816,c_2907,c_4387,c_5892,c_5893,c_6186,c_6371,c_6376,c_6517,c_7570,c_7739,c_7846,c_11254,c_11455,c_11465,c_11557,c_11723,c_12034,c_12481,c_12737,c_12748,c_15817,c_17781,c_28172,c_28863,c_31013,c_33967,c_36613,c_42957,c_43256,c_43274,c_46792,c_46861,c_58163,c_58764,c_59162,c_60143,c_60272,c_60350,c_60760,c_72413,c_73280,c_77931,c_77959,c_80400]) ).
tcf(c_82695,plain,
! [X0: $i,X1: $i] :
( para(X0,sK0,X1,sK4)
| ~ midp(X0,sK1,X1) ),
inference(superposition,[status(thm)],[c_82693,c_96]) ).
tcf(c_82704,plain,
( para(sK0,sK0,sK0,sK4)
| ~ midp(sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_82695]) ).
tcf(c_83299,plain,
( cong(sK1,sK1,sK1,sK2)
| ~ midp(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_82347,c_116]) ).
tcf(c_83302,plain,
cong(sK1,sK1,sK1,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_83299,c_82616]) ).
tcf(c_84035,plain,
( midp(sK1,sK1,sK2)
| ~ coll(sK1,sK1,sK2) ),
inference(superposition,[status(thm)],[c_83302,c_78]) ).
tcf(c_84039,plain,
midp(sK1,sK1,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_84035,c_78258]) ).
tcf(c_84150,plain,
midp(sK1,sK2,sK1),
inference(superposition,[status(thm)],[c_84039,c_125]) ).
tcf(c_84602,plain,
! [X0: $i] :
( cong(sK0,sK2,sK0,X0)
| ~ midp(sK1,sK2,sK1)
| ~ midp(sK0,sK1,X0) ),
inference(superposition,[status(thm)],[c_78274,c_36725]) ).
tcf(c_84810,plain,
( cong(sK0,sK2,sK0,sK0)
| ~ midp(sK1,sK2,sK1)
| ~ midp(sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_84602]) ).
tcf(c_86057,plain,
! [X0: $i] :
( cong(sK1,sK0,sK1,X0)
| ~ midp(sK1,X0,sK1) ),
inference(superposition,[status(thm)],[c_78476,c_36726]) ).
tcf(c_86258,plain,
( cong(sK1,sK0,sK1,sK0)
| ~ midp(sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_86057]) ).
tcf(c_90012,plain,
! [X0: $i,X1: $i] :
( cyclic(sK0,sK4,sK1,X1)
| ~ midp(X0,sK0,sK4)
| ~ cong(X0,sK0,X0,sK1)
| ~ cong(X0,sK0,X0,X1) ),
inference(instantiation,[status(thm)],[c_21407]) ).
tcf(c_90013,plain,
( cyclic(sK0,sK4,sK1,sK0)
| ~ midp(sK0,sK0,sK4)
| ~ cong(sK0,sK0,sK0,sK1)
| ~ cong(sK0,sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_90012]) ).
tcf(c_92237,plain,
( perp(sK5,sK0,sK0,sK0)
| ~ cyclic(sK0,sK1,sK0,sK4) ),
inference(superposition,[status(thm)],[c_51,c_39502]) ).
tcf(c_98131,plain,
( cyclic(sK0,sK1,sK4,sK0)
| ~ cyclic(sK0,sK4,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_116020,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X1,sK7,sK4)
| ~ coll(X1,sK7,sK4)
| ~ midp(X0,sK7,X2)
| ~ para(X0,X1,X2,sK4) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_116021,plain,
( midp(sK0,sK7,sK4)
| ~ midp(sK0,sK7,sK0)
| ~ coll(sK0,sK7,sK4)
| ~ para(sK0,sK0,sK0,sK4) ),
inference(instantiation,[status(thm)],[c_116020]) ).
tcf(c_116062,plain,
! [X0: $i,X1: $i] :
( perp(sK2,sK7,X0,X1)
| ~ perp(X0,X1,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_116074,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK2,sK7,X2,X3)
| ~ perp(sK2,sK7,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_116312,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK2,sK7,sK12(X0,X1,X2,sK2,sK7),X0)
| ~ perp(sK12(X0,X1,X2,sK2,sK7),X0,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_116062]) ).
tcf(c_116314,plain,
( perp(sK2,sK7,sK12(sK0,sK0,sK0,sK2,sK7),sK0)
| ~ perp(sK12(sK0,sK0,sK0,sK2,sK7),sK0,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_116312]) ).
tcf(c_116485,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK7,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK7,X2,X1)
| ~ para(X0,X1,X2,sK7) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_120091,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(sK2,sK7,X3,X4)
| ~ perp(sK2,sK7,sK12(X0,X1,X2,sK2,sK7),X0)
| ~ perp(sK12(X0,X1,X2,sK2,sK7),X0,X3,X4) ),
inference(instantiation,[status(thm)],[c_116074]) ).
tcf(c_123369,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK2,sK7,sK2,sK7)
| ~ perp(sK2,sK7,sK12(X0,X1,X2,sK2,sK7),X0)
| ~ perp(sK12(X0,X1,X2,sK2,sK7),X0,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_120091]) ).
tcf(c_123370,plain,
( para(sK2,sK7,sK2,sK7)
| ~ perp(sK2,sK7,sK12(sK0,sK0,sK0,sK2,sK7),sK0)
| ~ perp(sK12(sK0,sK0,sK0,sK2,sK7),sK0,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_123369]) ).
tcf(c_133468,plain,
! [X0: $i] :
( midp(X0,sK7,sK7)
| ~ midp(X0,sK2,sK2)
| ~ para(sK2,sK7,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_116485]) ).
tcf(c_133470,plain,
( midp(sK0,sK7,sK7)
| ~ midp(sK0,sK2,sK2)
| ~ para(sK2,sK7,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_133468]) ).
tcf(c_133471,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_133470,c_123370,c_116314,c_116021,c_98131,c_92237,c_90013,c_86258,c_84810,c_84150,c_82704,c_80116,c_78071,c_76135,c_76126,c_75738,c_74804,c_72567,c_72332,c_71323,c_71317,c_69344,c_66420,c_65762,c_60765,c_60760,c_60358,c_60350,c_60277,c_60272,c_60143,c_59164,c_59162,c_58780,c_58764,c_58165,c_58163,c_57612,c_57596,c_57547,c_57490,c_57216,c_57098,c_54869,c_46861,c_42957,c_42853,c_42828,c_39203,c_38196,c_36613,c_36454,c_33967,c_32824,c_31034,c_31013,c_28863,c_28172,c_21945,c_19863,c_17781,c_15817,c_12749,c_12748,c_12737,c_12554,c_12481,c_12034,c_11559,c_11557,c_11465,c_11455,c_8144,c_8120,c_8082,c_7846,c_7739,c_7709,c_7609,c_7570,c_6968,c_6697,c_6659,c_6517,c_6376,c_6371,c_6227,c_6223,c_6186,c_6091,c_5897,c_5893,c_5892,c_5168,c_4658,c_4473,c_4436,c_4387,c_2907,c_2816,c_2755,c_2727,c_2704,c_2564,c_2565,c_2546,c_2547,c_2505,c_2504,c_2476,c_2451,c_2449,c_2370,c_2369,c_2368,c_843,c_797,c_155,c_153,c_49,c_53,c_55]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO559+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.07/0.35 % Computer : n017.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Wed Sep 23 12:19:31 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 Running first-order theorem proving
% 0.11/0.38 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.39
% 0.11/0.39 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.39
% 0.11/0.40 % Detected problem language: tptp
% 0.11/0.41 % Proving...
% 57.61/12.37 % SZS status Started for theBenchmark.p
% 57.61/12.37 % SZS status Theorem for theBenchmark.p
% 57.61/12.37
% 57.61/12.37 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 57.61/12.37
% 57.61/12.37 % ------ iProver source info
% 57.61/12.37
% 57.61/12.37 % git: date: 2026-07-19 20:42:38 +0200
% 57.61/12.37 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 57.61/12.37 % git: non_committed_changes: false
% 57.61/12.37
% 57.61/12.37 % ------ Parsing...
% 57.61/12.37 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 57.61/12.37
% 57.61/12.37 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 57.61/12.37
% 57.61/12.37 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 57.61/12.37 % ------ Proving...
% 57.61/12.37 % ------ Problem Properties
% 57.61/12.37
% 57.61/12.37 %
% 57.61/12.37 % clauses 94
% 57.61/12.37 % conjectures 7
% 57.61/12.37 % EPR 61
% 57.61/12.37 % Horn 89
% 57.61/12.37 % unary 7
% 57.61/12.37 % binary 24
% 57.61/12.37 % lits 263
% 57.61/12.37 % lits eq 0
% 57.61/12.37 % fd_pure 0
% 57.61/12.37 % fd_pseudo 0
% 57.61/12.37 % fd_cond 0
% 57.61/12.37 % fd_pseudo_cond 0
% 57.61/12.37 % AC symbols 0
% 57.61/12.37
% 57.61/12.37 % ------ Schedule dynamic 5 is on
% 57.61/12.37
% 57.61/12.37 % ------ no equalities: superposition off
% 57.61/12.37
% 57.61/12.37 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 57.61/12.37
% 57.61/12.37
% 57.61/12.37 % ------
% 57.61/12.37 % Current options:
% 57.61/12.37 % ------
% 57.61/12.37
% 57.61/12.37
% 57.61/12.37 %
% 57.61/12.37
% 57.61/12.37 % ------ Proving...
% 57.61/12.37 % Proof_search_loop: time out after: 8674 full_loop iterations
% 57.61/12.37
% 57.61/12.37 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 57.61/12.37
% 57.61/12.37
% 57.61/12.37 % ------
% 57.61/12.37 % Current options:
% 57.61/12.37 % ------
% 57.61/12.37
% 57.61/12.37
% 57.61/12.37 %
% 57.61/12.37
% 57.61/12.37 % ------ Proving...
% 57.61/12.37 %
% 57.61/12.37
% 57.61/12.37 % SZS status Theorem for theBenchmark.p
% 57.61/12.37
% 57.61/12.37 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 57.61/12.38
% 57.61/12.38
%------------------------------------------------------------------------------