%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO639+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 : n010.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:43 PM UTC 2026
% Result : Theorem 132.95s 21.60s
% Output : CNFRefutation 132.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 42
% Syntax : Number of formulae : 533 ( 40 unt; 0 def)
% Number of atoms : 1396 ( 0 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1589 ( 726 ~; 725 |; 95 &)
% ( 0 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 1371 ( 0 sgn1339 !; 32 ?; 582 :)
% 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(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(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(f18,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD18) ).
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(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(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(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(f70,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD69) ).
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,X9,X10,X11,X12,X13,X14,X15] :
( ( coll(X8,X2,X3)
& coll(X8,X0,X1)
& circle(X5,X4,X7,X15)
& coll(X7,X1,X2)
& circle(X5,X4,X6,X14)
& coll(X6,X0,X2)
& circle(X5,X4,X12,X13)
& midp(X5,X4,X2)
& circle(X3,X0,X4,X11)
& coll(X4,X2,X3)
& circle(X3,X0,X9,X10)
& perp(X1,X2,X1,X3)
& perp(X0,X2,X0,X3)
& ( cong(X2,X0,X2,X1)
| cong(X2,X0,X0,X1) ) )
=> eqangle(X2,X6,X6,X8,X8,X6,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL81109105) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
( ( coll(X8,X2,X3)
& coll(X8,X0,X1)
& circle(X5,X4,X7,X15)
& coll(X7,X1,X2)
& circle(X5,X4,X6,X14)
& coll(X6,X0,X2)
& circle(X5,X4,X12,X13)
& midp(X5,X4,X2)
& circle(X3,X0,X4,X11)
& coll(X4,X2,X3)
& circle(X3,X0,X9,X10)
& perp(X1,X2,X1,X3)
& perp(X0,X2,X0,X3)
& ( cong(X2,X0,X2,X1)
| cong(X2,X0,X0,X1) ) )
=> eqangle(X2,X6,X6,X8,X8,X6,X6,X7) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
( coll(X8,X2,X3)
& coll(X8,X0,X1)
& circle(X5,X4,X7,X15)
& coll(X7,X1,X2)
& circle(X5,X4,X6,X14)
& coll(X6,X0,X2)
& circle(X5,X4,X12,X13)
& midp(X5,X4,X2)
& circle(X3,X0,X4,X11)
& coll(X4,X2,X3)
& circle(X3,X0,X9,X10)
& perp(X1,X2,X1,X3)
& perp(X0,X2,X0,X3)
& ( cong(X2,X0,X2,X1)
| cong(X2,X0,X0,X1) )
& ~ eqangle(X2,X6,X6,X8,X8,X6,X6,X7) ),
inference(ennf_transformation,[],[f96]) ).
fof(f99,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
( coll(X8,X2,X3)
& coll(X8,X0,X1)
& circle(X5,X4,X7,X15)
& coll(X7,X1,X2)
& circle(X5,X4,X6,X14)
& coll(X6,X0,X2)
& circle(X5,X4,X12,X13)
& midp(X5,X4,X2)
& circle(X3,X0,X4,X11)
& coll(X4,X2,X3)
& circle(X3,X0,X9,X10)
& perp(X1,X2,X1,X3)
& perp(X0,X2,X0,X3)
& ( cong(X2,X0,X2,X1)
| cong(X2,X0,X0,X1) )
& ~ eqangle(X2,X6,X6,X8,X8,X6,X6,X7) ),
inference(flattening,[],[f98]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
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(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] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f75]) ).
fof(f137,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,[],[f136]) ).
fof(f142,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f57]) ).
fof(f143,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f56]) ).
fof(f145,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(ennf_transformation,[],[f53]) ).
fof(f147,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(flattening,[],[f146]) ).
fof(f148,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(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(flattening,[],[f148]) ).
fof(f150,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f9]) ).
fof(f151,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f156,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f157,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(f158,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,[],[f157]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f160,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f159]) ).
fof(f161,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f162,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f161]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f165,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(f166,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f165]) ).
fof(f167,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f174]) ).
fof(f176,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(f177,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,[],[f176]) ).
fof(f184,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(f185,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(flattening,[],[f184]) ).
fof(f188,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f40]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f39]) ).
fof(f190,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(f191,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,[],[f190]) ).
fof(f192,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(f193,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(f194,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(f195,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f18]) ).
fof(f198,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f206,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f207,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(flattening,[],[f206]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f209,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f208]) ).
fof(f212,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f41]) ).
fof(f213,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f17]) ).
fof(f214,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(flattening,[],[f213]) ).
fof(f215,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f216,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f217,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f218,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f13]) ).
fof(f219,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f218]) ).
fof(f220,plain,
( coll(sK8,sK2,sK3)
& coll(sK8,sK0,sK1)
& circle(sK5,sK4,sK7,sK15)
& coll(sK7,sK1,sK2)
& circle(sK5,sK4,sK6,sK14)
& coll(sK6,sK0,sK2)
& circle(sK5,sK4,sK12,sK13)
& midp(sK5,sK4,sK2)
& circle(sK3,sK0,sK4,sK11)
& coll(sK4,sK2,sK3)
& circle(sK3,sK0,sK9,sK10)
& perp(sK1,sK2,sK1,sK3)
& perp(sK0,sK2,sK0,sK3)
& ( cong(sK2,sK0,sK2,sK1)
| cong(sK2,sK0,sK0,sK1) )
& ~ eqangle(sK2,sK6,sK6,sK8,sK8,sK6,sK6,sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15]),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),skolemize(X10,sK10),skolemize(X11,sK11),skolemize(X12,sK12),skolemize(X13,sK13),skolemize(X14,sK14),skolemize(X15,sK15)],[f99]) ).
fof(f239,plain,
coll(sK8,sK2,sK3),
inference(cnf_transformation,[],[f220]) ).
fof(f240,plain,
coll(sK8,sK0,sK1),
inference(cnf_transformation,[],[f220]) ).
fof(f242,plain,
coll(sK7,sK1,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f244,plain,
coll(sK6,sK0,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f246,plain,
midp(sK5,sK4,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f248,plain,
coll(sK4,sK2,sK3),
inference(cnf_transformation,[],[f220]) ).
fof(f253,plain,
~ eqangle(sK2,sK6,sK6,sK8,sK8,sK6,sK6,sK7),
inference(cnf_transformation,[],[f220]) ).
fof(f275,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f276,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f122]) ).
fof(f279,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(f280,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f281,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f130]) ).
fof(f282,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f287,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,[],[f137]) ).
fof(f290,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f143]) ).
fof(f291,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f145]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f147]) ).
fof(f293,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,[],[f149]) ).
fof(f294,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f151]) ).
fof(f295,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f296,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f153]) ).
fof(f300,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f156]) ).
fof(f301,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,[],[f158]) ).
fof(f302,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f160]) ).
fof(f303,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f162]) ).
fof(f304,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f163]) ).
fof(f306,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,[],[f166]) ).
fof(f307,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f308,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f168]) ).
fof(f312,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f313,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,[],[f177]) ).
fof(f317,plain,
! [X2,X3,X0,X1] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f185]) ).
fof(f319,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f188]) ).
fof(f320,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f189]) ).
fof(f321,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,[],[f191]) ).
fof(f322,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,[],[f192]) ).
fof(f323,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,[],[f193]) ).
fof(f324,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,[],[f194]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f195]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f198]) ).
fof(f333,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(f334,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(f336,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f212]) ).
fof(f337,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f214]) ).
fof(f338,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f215]) ).
fof(f339,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f216]) ).
fof(f340,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f217]) ).
fof(f341,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,
~ eqangle(sK2,sK6,sK6,sK8,sK8,sK6,sK6,sK7),
inference(cnf_transformation,[],[f253]) ).
tcf(c_54,negated_conjecture,
coll(sK4,sK2,sK3),
inference(cnf_transformation,[],[f248]) ).
tcf(c_56,negated_conjecture,
midp(sK5,sK4,sK2),
inference(cnf_transformation,[],[f246]) ).
tcf(c_58,negated_conjecture,
coll(sK6,sK0,sK2),
inference(cnf_transformation,[],[f244]) ).
tcf(c_60,negated_conjecture,
coll(sK7,sK1,sK2),
inference(cnf_transformation,[],[f242]) ).
tcf(c_62,negated_conjecture,
coll(sK8,sK0,sK1),
inference(cnf_transformation,[],[f240]) ).
tcf(c_63,negated_conjecture,
coll(sK8,sK2,sK3),
inference(cnf_transformation,[],[f239]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_89,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,[],[f279]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_97,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,[],[f287]) ).
tcf(c_100,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,[],[f290]) ).
tcf(c_101,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,[],[f291]) ).
tcf(c_102,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,[],[f292]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X4,X5,X2,X3)
| ~ para(X4,X5,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_104,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,[],[f294]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_111,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,[],[f301]) ).
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,[],[f302]) ).
tcf(c_113,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,[],[f303]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_116,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,[],[f306]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X2,X3,X0,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_122,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,[],[f312]) ).
tcf(c_123,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,[],[f313]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( circle(X0,X1,X2,X3)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_129,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,[],[f319]) ).
tcf(c_130,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,[],[f320]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
( eqangle(X8,X9,X10,X11,X4,X5,X6,X7)
| ~ eqangle(X8,X9,X10,X11,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_132,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,[],[f322]) ).
tcf(c_133,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,[],[f323]) ).
tcf(c_134,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,[],[f324]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X1,X0,X2,X3,X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_143,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,[],[f333]) ).
tcf(c_144,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,[],[f334]) ).
tcf(c_146,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,[],[f336]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X4,X3)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_151,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,[],[f341]) ).
tcf(c_155,plain,
( eqangle(sK2,sK2,sK2,sK2,sK2,sK2,sK2,sK2)
| ~ cyclic(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_161,plain,
( midp(sK2,sK2,sK2)
| ~ coll(sK2,sK2,sK2)
| ~ cong(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_165,plain,
( perp(sK2,sK2,sK2,sK2)
| ~ cong(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_203,plain,
( cong(sK2,sK2,sK2,sK2)
| ~ cyclic(sK2,sK2,sK2,sK2)
| ~ eqangle(sK2,sK2,sK2,sK2,sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_2524,plain,
( coll(sK5,sK4,sK2)
| ~ midp(sK5,sK4,sK2) ),
inference(instantiation,[status(thm)],[c_85]) ).
tcf(c_2530,plain,
( coll(sK4,sK3,sK2)
| ~ coll(sK4,sK2,sK3) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_2534,plain,
( coll(sK8,sK3,sK2)
| ~ coll(sK8,sK2,sK3) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_2535,plain,
( midp(sK5,sK2,sK4)
| ~ midp(sK5,sK4,sK2) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_2536,plain,
( cong(sK5,sK4,sK5,sK2)
| ~ midp(sK5,sK4,sK2) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_2545,plain,
! [X0: $i] :
( coll(sK2,X0,sK6)
| ~ coll(sK6,sK0,sK2)
| ~ coll(sK6,sK0,X0) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_2546,plain,
( coll(sK2,sK2,sK6)
| ~ coll(sK6,sK0,sK2) ),
inference(instantiation,[status(thm)],[c_2545]) ).
tcf(c_2547,plain,
! [X0: $i] :
( coll(sK2,X0,sK7)
| ~ coll(sK7,sK1,sK2)
| ~ coll(sK7,sK1,X0) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_2548,plain,
( coll(sK2,sK2,sK7)
| ~ coll(sK7,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_2560,plain,
! [X0: $i,X1: $i] :
( para(X0,sK5,X1,sK2)
| ~ midp(sK5,sK4,sK2)
| ~ midp(X0,sK4,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_2561,plain,
( para(sK2,sK5,sK2,sK2)
| ~ midp(sK5,sK4,sK2)
| ~ midp(sK2,sK4,sK2) ),
inference(instantiation,[status(thm)],[c_2560]) ).
tcf(c_2626,plain,
! [X0: $i,X1: $i] :
( midp(sK5,X0,X1)
| ~ midp(sK5,sK4,sK2)
| ~ para(sK4,X1,sK2,X0)
| ~ para(sK4,X0,sK2,X1) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_2627,plain,
( midp(sK5,sK2,sK2)
| ~ midp(sK5,sK4,sK2)
| ~ para(sK4,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_2626]) ).
tcf(c_2766,plain,
! [X0: $i] :
( perp(sK4,X0,X0,sK2)
| ~ coll(sK5,sK4,sK2)
| ~ circle(sK5,sK4,X0,sK2) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_2767,plain,
( perp(sK4,sK2,sK2,sK2)
| ~ coll(sK5,sK4,sK2)
| ~ circle(sK5,sK4,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_2766]) ).
tcf(c_2920,plain,
! [X0: $i] :
( coll(sK2,X0,sK4)
| ~ coll(sK4,sK3,sK2)
| ~ coll(sK4,sK3,X0) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_2923,plain,
( coll(sK2,sK2,sK4)
| ~ coll(sK4,sK3,sK2) ),
inference(instantiation,[status(thm)],[c_2920]) ).
tcf(c_3028,plain,
! [X0: $i] :
( coll(sK2,X0,sK8)
| ~ coll(sK8,sK3,sK2)
| ~ coll(sK8,sK3,X0) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_3031,plain,
( coll(sK2,sK2,sK8)
| ~ coll(sK8,sK3,sK2) ),
inference(instantiation,[status(thm)],[c_3028]) ).
tcf(c_3041,plain,
! [X0: $i] :
( cong(X0,sK2,X0,sK4)
| ~ midp(sK5,sK2,sK4)
| ~ perp(X0,sK5,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_3042,plain,
( cong(sK2,sK2,sK2,sK4)
| ~ midp(sK5,sK2,sK4)
| ~ perp(sK2,sK5,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_3041]) ).
tcf(c_3062,plain,
! [X0: $i,X1: $i] :
( midp(sK5,X0,X1)
| ~ midp(sK5,sK2,sK4)
| ~ para(sK2,X1,sK4,X0)
| ~ para(sK2,X0,sK4,X1) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_3066,plain,
! [X0: $i,X1: $i] :
( cyclic(sK4,sK2,X0,X1)
| ~ cong(sK5,sK4,sK5,sK2)
| ~ cong(sK5,sK4,sK5,X1)
| ~ cong(sK5,sK4,sK5,X0) ),
inference(instantiation,[status(thm)],[c_151]) ).
tcf(c_3074,plain,
! [X0: $i] :
( circle(sK5,sK4,sK2,X0)
| ~ cong(sK5,sK4,sK5,sK2)
| ~ cong(sK5,sK4,sK5,X0) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_3076,plain,
( circle(sK5,sK4,sK2,sK2)
| ~ cong(sK5,sK4,sK5,sK2) ),
inference(instantiation,[status(thm)],[c_3074]) ).
tcf(c_3082,plain,
( cyclic(sK4,sK2,sK2,sK2)
| ~ cong(sK5,sK4,sK5,sK2) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_3301,plain,
! [X0: $i] :
( midp(sK2,X0,sK6)
| ~ coll(sK2,X0,sK6)
| ~ cong(sK2,X0,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_3303,plain,
! [X0: $i] :
( coll(sK2,sK6,X0)
| ~ coll(sK2,X0,sK6) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_3305,plain,
( coll(sK2,sK6,sK2)
| ~ coll(sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_3303]) ).
tcf(c_3307,plain,
( midp(sK2,sK2,sK6)
| ~ coll(sK2,sK2,sK6)
| ~ cong(sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_3301]) ).
tcf(c_3343,plain,
coll(sK7,sK2,sK1),
inference(superposition,[status(thm)],[c_60,c_92]) ).
tcf(c_3361,plain,
coll(sK8,sK3,sK2),
inference(superposition,[status(thm)],[c_63,c_92]) ).
tcf(c_3638,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK7,sK2,X1)
| ~ coll(sK2,X1,sK7)
| ~ eqangle(sK2,X0,sK2,sK7,X1,X0,X1,sK7) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_3639,plain,
( cyclic(sK2,sK7,sK2,sK2)
| ~ coll(sK2,sK2,sK7)
| ~ eqangle(sK2,sK2,sK2,sK7,sK2,sK2,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_3638]) ).
tcf(c_3710,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_110,c_117]) ).
tcf(c_4179,plain,
! [X0: $i] :
( coll(sK2,X0,sK6)
| ~ coll(sK6,sK0,X0) ),
inference(superposition,[status(thm)],[c_58,c_90]) ).
tcf(c_4181,plain,
! [X0: $i] :
( coll(sK1,X0,sK8)
| ~ coll(sK8,sK0,X0) ),
inference(superposition,[status(thm)],[c_62,c_90]) ).
tcf(c_4191,plain,
! [X0: $i] :
( coll(sK1,X0,sK7)
| ~ coll(sK7,sK2,X0) ),
inference(superposition,[status(thm)],[c_3343,c_90]) ).
tcf(c_4308,plain,
! [X0: $i] :
( coll(sK2,X0,sK6)
| ~ coll(sK6,sK0,X0) ),
inference(superposition,[status(thm)],[c_58,c_90]) ).
tcf(c_4309,plain,
! [X0: $i] :
( coll(sK2,X0,sK7)
| ~ coll(sK7,sK1,X0) ),
inference(superposition,[status(thm)],[c_60,c_90]) ).
tcf(c_4322,plain,
! [X0: $i] :
( coll(sK2,X0,sK8)
| ~ coll(sK8,sK3,X0) ),
inference(superposition,[status(thm)],[c_3361,c_90]) ).
tcf(c_4783,plain,
! [X0: $i,X1: $i] :
( para(sK4,X0,sK2,X1)
| ~ midp(sK5,X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_112]) ).
tcf(c_4948,plain,
coll(sK2,sK2,sK6),
inference(superposition,[status(thm)],[c_58,c_4179]) ).
tcf(c_4953,plain,
coll(sK2,sK2,sK6),
inference(superposition,[status(thm)],[c_58,c_4308]) ).
tcf(c_4962,plain,
! [X0: $i] :
( coll(sK6,X0,sK2)
| ~ coll(sK2,sK2,X0) ),
inference(superposition,[status(thm)],[c_4948,c_90]) ).
tcf(c_4963,plain,
coll(sK2,sK6,sK2),
inference(superposition,[status(thm)],[c_4948,c_92]) ).
tcf(c_4968,plain,
! [X0: $i] :
( coll(sK6,X0,sK2)
| ~ coll(sK2,sK2,X0) ),
inference(superposition,[status(thm)],[c_4953,c_90]) ).
tcf(c_4997,plain,
! [X0: $i,X1: $i] :
( coll(X0,sK1,X1)
| ~ coll(X0,X1,sK1) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_5014,plain,
coll(sK2,sK2,sK7),
inference(superposition,[status(thm)],[c_60,c_4309]) ).
tcf(c_5021,plain,
! [X0: $i] :
( coll(sK7,X0,sK2)
| ~ coll(sK2,sK2,X0) ),
inference(superposition,[status(thm)],[c_5014,c_90]) ).
tcf(c_5070,plain,
coll(sK1,sK1,sK8),
inference(superposition,[status(thm)],[c_62,c_4181]) ).
tcf(c_5076,plain,
! [X0: $i] :
( coll(sK8,X0,sK1)
| ~ coll(sK1,sK1,X0) ),
inference(superposition,[status(thm)],[c_5070,c_90]) ).
tcf(c_5258,plain,
! [X0: $i] :
( coll(sK2,X0,sK2)
| ~ coll(sK2,sK6,X0) ),
inference(superposition,[status(thm)],[c_4963,c_90]) ).
tcf(c_5263,plain,
( coll(sK2,sK2,sK2)
| ~ coll(sK2,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_5258]) ).
tcf(c_5269,plain,
! [X0: $i,X1: $i] :
( coll(sK4,sK2,X0)
| ~ coll(X0,X1,sK4)
| ~ coll(X0,X1,sK2) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_5270,plain,
( coll(sK4,sK2,sK2)
| ~ coll(sK2,sK2,sK4)
| ~ coll(sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_5269]) ).
tcf(c_5586,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X2,X0,X2,X0)
| ~ cyclic(X0,X1,X2,X2) ),
inference(superposition,[status(thm)],[c_146,c_130]) ).
tcf(c_5589,plain,
( para(sK2,sK2,sK2,sK2)
| ~ cyclic(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_5586]) ).
tcf(c_5736,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK4,X1)
| ~ midp(sK5,sK4,sK2)
| ~ coll(X0,sK4,X1)
| ~ para(sK5,X0,sK2,X1) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_5737,plain,
( midp(sK2,sK4,sK2)
| ~ midp(sK5,sK4,sK2)
| ~ coll(sK2,sK4,sK2)
| ~ para(sK5,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_5736]) ).
tcf(c_6456,plain,
! [X0: $i,X1: $i] :
( coll(sK2,sK4,X0)
| ~ coll(X0,X1,sK4)
| ~ coll(X0,X1,sK2) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_6457,plain,
( coll(sK2,sK4,sK2)
| ~ coll(sK2,sK2,sK4)
| ~ coll(sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_6456]) ).
tcf(c_6537,plain,
( coll(sK2,sK8,sK7)
| ~ coll(sK7,sK1,sK8)
| ~ coll(sK7,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_6650,plain,
! [X0: $i,X1: $i] :
( perp(X1,X0,X0,sK4)
| ~ perp(X0,sK4,X1,X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_6651,plain,
( perp(sK2,sK2,sK2,sK4)
| ~ perp(sK2,sK4,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_6650]) ).
tcf(c_6652,plain,
! [X0: $i,X1: $i] :
( perp(X1,X0,X0,sK6)
| ~ perp(X0,sK6,X1,X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_6653,plain,
( perp(sK2,sK2,sK2,sK6)
| ~ perp(sK2,sK6,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_6652]) ).
tcf(c_7177,plain,
! [X0: $i] :
( cong(sK2,X0,sK2,sK6)
| ~ cong(sK2,X0,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_7178,plain,
( cong(sK2,sK2,sK2,sK6)
| ~ cong(sK2,sK2,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_7177]) ).
tcf(c_7206,plain,
! [X0: $i,X1: $i] :
( para(X1,sK8,X0,sK2)
| ~ para(X0,sK2,X1,sK8) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_7207,plain,
( para(sK2,sK8,sK2,sK2)
| ~ para(sK2,sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_7206]) ).
tcf(c_7384,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK2,X0,X2,X1)
| ~ cyclic(sK4,sK2,X0,X2)
| ~ cyclic(sK4,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_7391,plain,
( cyclic(sK2,sK2,sK2,sK2)
| ~ cyclic(sK4,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_7384]) ).
tcf(c_7745,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK6,X1)
| ~ midp(X0,X1,sK6) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_7746,plain,
( midp(sK2,sK6,sK2)
| ~ midp(sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_7745]) ).
tcf(c_7843,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X1,sK4,X2,sK2)
| ~ midp(X0,sK4,sK2)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_7844,plain,
( para(sK2,sK4,sK2,sK2)
| ~ midp(sK2,sK4,sK2)
| ~ midp(sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_7843]) ).
tcf(c_7932,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK5,X0,sK2,X2)
| ~ midp(sK5,X1,sK2)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_7933,plain,
( para(sK5,sK2,sK2,sK2)
| ~ midp(sK5,sK2,sK2)
| ~ midp(sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_7932]) ).
tcf(c_8322,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( circle(X0,X1,X3,X2)
| ~ midp(X0,X3,X1)
| ~ cong(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_3710,c_127]) ).
tcf(c_8718,plain,
( midp(sK2,sK6,sK6)
| ~ coll(sK2,sK6,sK6)
| ~ cong(sK2,sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_3301]) ).
tcf(c_8872,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X1,sK8)
| ~ cong(X0,sK8,X1,sK8)
| ~ cong(X0,X1,X1,X1) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_8873,plain,
( perp(sK2,sK2,sK2,sK8)
| ~ cong(sK2,sK8,sK2,sK8)
| ~ cong(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_8872]) ).
tcf(c_9133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,sK4,X2,X3)
| ~ para(X2,sK4,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_9134,plain,
( perp(sK2,sK4,sK2,sK2)
| ~ para(sK2,sK4,sK2,sK2)
| ~ perp(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_9133]) ).
tcf(c_9138,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(X0,sK5,sK2,sK4)
| ~ perp(X1,X2,sK2,sK4)
| ~ para(X0,sK5,X1,X2) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_9139,plain,
( perp(sK2,sK5,sK2,sK4)
| ~ para(sK2,sK5,sK2,sK2)
| ~ perp(sK2,sK2,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_9138]) ).
tcf(c_9259,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK4,X3,sK2,X2)
| ~ perp(sK4,X3,X0,X1)
| ~ perp(X0,X1,sK2,X2) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_9260,plain,
( para(sK4,sK2,sK2,sK2)
| ~ perp(sK4,sK2,sK2,sK2)
| ~ perp(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_9259]) ).
tcf(c_9895,plain,
coll(sK1,sK1,sK7),
inference(superposition,[status(thm)],[c_3343,c_4191]) ).
tcf(c_10642,plain,
coll(sK2,sK2,sK8),
inference(superposition,[status(thm)],[c_3361,c_4322]) ).
tcf(c_10951,plain,
coll(sK6,sK6,sK2),
inference(superposition,[status(thm)],[c_4948,c_4962]) ).
tcf(c_10967,plain,
coll(sK6,sK6,sK2),
inference(superposition,[status(thm)],[c_4953,c_4968]) ).
tcf(c_10973,plain,
coll(sK6,sK8,sK2),
inference(superposition,[status(thm)],[c_10642,c_4968]) ).
tcf(c_10978,plain,
coll(sK6,sK2,sK6),
inference(superposition,[status(thm)],[c_10951,c_92]) ).
tcf(c_10983,plain,
coll(sK6,sK2,sK6),
inference(superposition,[status(thm)],[c_10967,c_92]) ).
tcf(c_11670,plain,
coll(sK7,sK8,sK2),
inference(superposition,[status(thm)],[c_10642,c_5021]) ).
tcf(c_11787,plain,
coll(sK8,sK7,sK1),
inference(superposition,[status(thm)],[c_9895,c_5076]) ).
tcf(c_12010,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK4,X1,sK2)
| ~ midp(sK5,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_4783,c_89]) ).
tcf(c_13213,plain,
( eqangle(sK2,sK6,sK6,sK8,sK8,sK6,sK6,sK7)
| ~ eqangle(sK6,sK2,sK6,sK8,sK8,sK6,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_15678,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK4,sK2,X2)
| ~ coll(sK4,sK2,X2)
| ~ midp(X0,sK2,X1)
| ~ para(X0,sK4,X1,X2) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_15679,plain,
( midp(sK4,sK2,sK2)
| ~ midp(sK2,sK2,sK2)
| ~ coll(sK4,sK2,sK2)
| ~ para(sK2,sK4,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_15678]) ).
tcf(c_15867,plain,
! [X0: $i] :
( midp(X0,sK2,sK4)
| ~ coll(X0,sK2,sK4)
| ~ cong(X0,sK2,X0,sK4) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_15868,plain,
( midp(sK2,sK2,sK4)
| ~ coll(sK2,sK2,sK4)
| ~ cong(sK2,sK2,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_15867]) ).
tcf(c_16248,plain,
( eqangle(sK6,sK2,sK6,sK8,sK8,sK6,sK6,sK7)
| ~ eqangle(sK6,sK8,sK6,sK2,sK6,sK7,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_17360,plain,
coll(sK6,sK2,sK8),
inference(superposition,[status(thm)],[c_10973,c_92]) ).
tcf(c_17613,plain,
coll(sK2,sK6,sK6),
inference(superposition,[status(thm)],[c_10978,c_91]) ).
tcf(c_18319,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK8,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK8,X2,X1)
| ~ para(X0,X1,X2,sK8) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_18320,plain,
( midp(sK2,sK8,sK2)
| ~ midp(sK2,sK2,sK2)
| ~ para(sK2,sK8,sK2,sK2)
| ~ para(sK2,sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_18319]) ).
tcf(c_20337,plain,
( coll(sK7,sK1,sK8)
| ~ coll(sK7,sK8,sK1) ),
inference(instantiation,[status(thm)],[c_4997]) ).
tcf(c_20884,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X1,X3,sK8)
| ~ coll(X1,X3,sK8)
| ~ midp(X0,X3,X2)
| ~ para(X0,X1,X2,sK8) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_20885,plain,
( midp(sK2,sK2,sK8)
| ~ midp(sK2,sK2,sK2)
| ~ coll(sK2,sK2,sK8)
| ~ para(sK2,sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_20884]) ).
tcf(c_21224,plain,
( eqangle(sK6,sK8,sK6,sK2,sK6,sK7,sK8,sK6)
| ~ eqangle(sK8,sK6,sK6,sK2,sK6,sK7,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_22001,plain,
coll(sK7,sK2,sK8),
inference(superposition,[status(thm)],[c_11670,c_92]) ).
tcf(c_22096,plain,
coll(sK7,sK8,sK1),
inference(superposition,[status(thm)],[c_11787,c_91]) ).
tcf(c_25669,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,sK2,X3,sK8)
| ~ perp(X1,X2,X3,sK8)
| ~ perp(X0,sK2,X1,X2) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_25672,plain,
( para(sK2,sK2,sK2,sK8)
| ~ perp(sK2,sK2,sK2,sK8)
| ~ perp(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_25669]) ).
tcf(c_28570,plain,
coll(sK2,sK8,sK3),
inference(superposition,[status(thm)],[c_63,c_91]) ).
tcf(c_28703,plain,
coll(sK2,sK3,sK8),
inference(superposition,[status(thm)],[c_28570,c_92]) ).
tcf(c_29179,plain,
! [X0: $i] :
( coll(sK8,X0,sK2)
| ~ coll(sK2,sK3,X0) ),
inference(superposition,[status(thm)],[c_28703,c_90]) ).
tcf(c_29290,plain,
coll(sK8,sK8,sK2),
inference(superposition,[status(thm)],[c_28703,c_29179]) ).
tcf(c_35534,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK2,sK6,sK2)
| ~ midp(sK2,X0,X1)
| ~ perp(X0,sK6,sK6,X1) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_35535,plain,
( cong(sK2,sK2,sK6,sK2)
| ~ midp(sK2,sK2,sK2)
| ~ perp(sK2,sK6,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_35534]) ).
tcf(c_35903,plain,
! [X0: $i,X1: $i] :
( perp(X0,sK6,X1,X0)
| ~ cong(X0,X1,sK6,X1)
| ~ cong(X0,X0,sK6,X0) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_35904,plain,
( perp(sK2,sK6,sK2,sK2)
| ~ cong(sK2,sK2,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_35903]) ).
tcf(c_37051,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK6,sK7,sK8,sK6,sK6,sK7)
| ~ para(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_37053,plain,
( eqangle(sK2,sK2,sK6,sK7,sK8,sK6,sK6,sK7)
| ~ para(sK2,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_37051]) ).
tcf(c_37522,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK6,X1)
| ~ perp(X0,X1,X1,sK6) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_37523,plain,
( perp(sK2,sK2,sK6,sK2)
| ~ perp(sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_37522]) ).
tcf(c_38826,plain,
coll(sK2,sK6,sK8),
inference(superposition,[status(thm)],[c_17360,c_91]) ).
tcf(c_41952,plain,
coll(sK2,sK7,sK8),
inference(superposition,[status(thm)],[c_22001,c_91]) ).
tcf(c_47178,plain,
( midp(sK5,sK6,sK6)
| ~ midp(sK5,sK2,sK4)
| ~ para(sK2,sK6,sK4,sK6) ),
inference(instantiation,[status(thm)],[c_3062]) ).
tcf(c_48715,plain,
( midp(sK6,sK2,sK6)
| ~ midp(sK5,sK6,sK6)
| ~ midp(sK4,sK2,sK2) ),
inference(superposition,[status(thm)],[c_10983,c_12010]) ).
tcf(c_49718,plain,
! [X0: $i] :
( para(sK2,sK6,sK4,sK6)
| ~ midp(X0,sK6,sK6)
| ~ midp(X0,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_49719,plain,
( para(sK2,sK6,sK4,sK6)
| ~ midp(sK2,sK6,sK6)
| ~ midp(sK2,sK2,sK4) ),
inference(instantiation,[status(thm)],[c_49718]) ).
tcf(c_58063,plain,
! [X0: $i] :
( eqangle(sK2,X0,sK2,sK6,sK2,X0,sK2,sK6)
| ~ para(sK2,X0,sK2,X0) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_58064,plain,
( eqangle(sK2,sK2,sK2,sK6,sK2,sK2,sK2,sK6)
| ~ para(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_58063]) ).
tcf(c_58228,plain,
! [X0: $i] :
( eqangle(sK2,X0,sK2,sK7,sK2,X0,sK2,sK7)
| ~ para(sK2,X0,sK2,X0) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_58229,plain,
( eqangle(sK2,sK2,sK2,sK7,sK2,sK2,sK2,sK7)
| ~ para(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_58228]) ).
tcf(c_61639,plain,
! [X0: $i] :
( perp(X0,sK6,sK6,sK2)
| ~ perp(X0,sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_61640,plain,
( perp(sK2,sK6,sK6,sK2)
| ~ perp(sK2,sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_61639]) ).
tcf(c_65845,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK8,sK6)
| ~ eqangle(X0,X1,X2,X3,sK8,sK6,X2,X3) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_66267,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK2,sK6)
| ~ eqangle(X0,X1,X2,X3,sK2,sK6,X2,X3) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_66340,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK8,sK6,X2,X3)
| ~ para(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_66347,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK8,sK6,X0,X1)
| ~ eqangle(X0,X1,X2,X3,X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_66515,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK6,sK8,sK6,sK2,sK6,sK8)
| ~ para(X0,X1,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_66562,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X0,X1,sK8,sK6)
| ~ perp(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK8,sK6,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_66575,plain,
! [X0: $i,X1: $i] :
( perp(X1,sK8,sK8,sK6)
| ~ coll(X0,X1,sK6)
| ~ circle(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_66577,plain,
( perp(sK2,sK8,sK8,sK6)
| ~ coll(sK2,sK2,sK6)
| ~ circle(sK2,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_66575]) ).
tcf(c_66578,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK8,sK6)
| ~ cong(X0,sK8,X1,sK8)
| ~ cong(X0,sK6,X1,sK6) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_66579,plain,
( perp(sK2,sK2,sK8,sK6)
| ~ cong(sK2,sK8,sK2,sK8)
| ~ cong(sK2,sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_66578]) ).
tcf(c_66648,plain,
! [X0: $i] :
( eqangle(X0,sK7,X0,sK8,sK6,sK7,sK6,sK8)
| ~ cyclic(sK7,sK8,X0,sK6) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_66650,plain,
( eqangle(sK2,sK7,sK2,sK8,sK6,sK7,sK6,sK8)
| ~ cyclic(sK7,sK8,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_66648]) ).
tcf(c_66912,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK8,sK6,X2,X3,sK8,sK6)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_66913,plain,
( eqangle(sK2,sK2,sK8,sK6,sK2,sK2,sK8,sK6)
| ~ para(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_66912]) ).
tcf(c_66915,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK8,sK6,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK8,sK6,X4,X5) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_66969,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK6,sK7,X2,X3,sK6,sK7)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_66977,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X1,X0,X2,X3,X4,X5,sK6,sK7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_67170,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK6,X1)
| ~ midp(X0,X1,sK6) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_67599,plain,
! [X0: $i,X1: $i] :
( cyclic(sK7,sK8,X1,sK6)
| ~ cyclic(X0,sK7,sK8,sK6)
| ~ cyclic(X0,sK7,sK8,X1) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_67600,plain,
( cyclic(sK7,sK8,sK2,sK6)
| ~ cyclic(sK2,sK7,sK8,sK6)
| ~ cyclic(sK2,sK7,sK8,sK2) ),
inference(instantiation,[status(thm)],[c_67599]) ).
tcf(c_67692,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK2,sK6,X2,X3)
| ~ perp(sK2,sK6,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_67701,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK6,sK2)
| ~ perp(X2,X3,sK6,sK2)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_67876,plain,
! [X0: $i] :
( circle(X0,sK2,sK8,sK6)
| ~ midp(X0,sK8,sK2)
| ~ cong(X0,sK2,X0,sK6) ),
inference(instantiation,[status(thm)],[c_8322]) ).
tcf(c_67877,plain,
( circle(sK2,sK2,sK8,sK6)
| ~ midp(sK2,sK8,sK2)
| ~ cong(sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_67876]) ).
tcf(c_67915,plain,
! [X0: $i,X1: $i] :
( perp(sK8,sK6,X0,X1)
| ~ perp(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_67916,plain,
( perp(sK8,sK6,sK2,sK2)
| ~ perp(sK2,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_67915]) ).
tcf(c_67943,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK6,sK8)
| ~ cong(X0,sK8,X1,sK8)
| ~ cong(X0,sK6,X1,sK6) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_67944,plain,
( perp(sK2,sK2,sK6,sK8)
| ~ cong(sK2,sK8,sK2,sK8)
| ~ cong(sK2,sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_67943]) ).
tcf(c_68334,plain,
! [X0: $i] :
( para(sK2,sK6,sK2,sK6)
| ~ eqangle(sK2,sK6,sK2,X0,sK2,sK6,sK2,X0) ),
inference(instantiation,[status(thm)],[c_66267]) ).
tcf(c_68336,plain,
( para(sK2,sK6,sK2,sK6)
| ~ eqangle(sK2,sK6,sK2,sK2,sK2,sK6,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_68334]) ).
tcf(c_68345,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK2,sK6,X0,X1)
| ~ eqangle(X0,X1,X2,X3,X0,X1,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_68471,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,sK6,X3,sK6)
| ~ cong(X1,X2,X3,sK6)
| ~ cong(X0,sK6,X1,X2) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_68472,plain,
( cong(sK2,sK6,sK2,sK6)
| ~ cong(sK2,sK6,sK2,sK2)
| ~ cong(sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_68471]) ).
tcf(c_68558,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,X0,sK8)
| ~ midp(X0,X1,sK8) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_68559,plain,
( cong(sK2,sK2,sK2,sK8)
| ~ midp(sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_68558]) ).
tcf(c_69280,plain,
! [X0: $i,X1: $i] :
( eqangle(sK6,sK2,sK6,sK8,X0,X1,sK6,sK8)
| ~ para(sK6,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_69584,plain,
! [X0: $i] :
( eqangle(sK6,sK2,sK6,sK8,X0,sK2,X0,sK8)
| ~ cyclic(sK2,sK8,sK6,X0) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_69586,plain,
( eqangle(sK6,sK2,sK6,sK8,sK2,sK2,sK2,sK8)
| ~ cyclic(sK2,sK8,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_69584]) ).
tcf(c_69679,plain,
! [X0: $i] :
( cyclic(sK8,sK6,X0,sK8)
| ~ cyclic(sK6,sK8,X0,sK8) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_69680,plain,
( cyclic(sK8,sK6,sK2,sK8)
| ~ cyclic(sK6,sK8,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_69679]) ).
tcf(c_69811,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,X2,X3,sK8,sK6)
| ~ eqangle(X0,X1,X2,X3,sK8,sK6,X2,X3) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_69816,plain,
! [X0: $i,X1: $i] :
( eqangle(sK8,sK6,X0,X1,sK8,sK6,X0,X1)
| ~ eqangle(X0,X1,sK8,sK6,X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_66347]) ).
tcf(c_69817,plain,
( eqangle(sK8,sK6,sK2,sK2,sK8,sK6,sK2,sK2)
| ~ eqangle(sK2,sK2,sK8,sK6,sK2,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_69816]) ).
tcf(c_69889,plain,
! [X0: $i] :
( perp(sK6,sK7,sK7,X0)
| ~ perp(sK6,sK7,X0,sK7) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_69890,plain,
( perp(sK6,sK7,sK7,sK2)
| ~ perp(sK6,sK7,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_69889]) ).
tcf(c_70318,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK8,sK6,X2,X3,X0,X1,X4,X5)
| ~ eqangle(sK8,sK6,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_70365,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK2,sK6,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK2,sK6,X4,X5) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_70621,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,X0,sK6,sK7,X2,X3,sK6,sK7)
| ~ eqangle(X0,X1,sK6,sK7,X2,X3,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_66977]) ).
tcf(c_70665,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK6,X3,sK6,X2)
| ~ para(sK6,X3,X0,X1)
| ~ perp(X0,X1,sK6,X2) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_72218,plain,
! [X0: $i] :
( cyclic(sK8,X0,sK6,sK8)
| ~ cyclic(sK8,sK6,X0,sK8) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_72219,plain,
( cyclic(sK8,sK2,sK6,sK8)
| ~ cyclic(sK8,sK6,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_72218]) ).
tcf(c_72234,plain,
! [X0: $i] :
( cyclic(sK6,sK8,X0,sK8)
| ~ cyclic(sK6,X0,sK8,sK8) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_72235,plain,
( cyclic(sK6,sK8,sK2,sK8)
| ~ cyclic(sK6,sK2,sK8,sK8) ),
inference(instantiation,[status(thm)],[c_72234]) ).
tcf(c_72283,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(sK2,sK6,X0,sK6)
| ~ perp(X1,X2,X3,X4)
| ~ eqangle(sK2,sK6,X0,sK6,X1,X2,X3,X4) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_72284,plain,
( perp(sK2,sK6,sK2,sK6)
| ~ perp(sK2,sK2,sK2,sK2)
| ~ eqangle(sK2,sK6,sK2,sK6,sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_72283]) ).
tcf(c_72320,plain,
! [X0: $i] :
( perp(sK6,sK7,X0,sK7)
| ~ perp(X0,sK7,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_72321,plain,
( perp(sK6,sK7,sK2,sK7)
| ~ perp(sK2,sK7,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_72320]) ).
tcf(c_72365,plain,
! [X0: $i] :
( cyclic(sK6,X0,sK8,sK8)
| ~ coll(sK8,sK8,X0)
| ~ eqangle(sK8,sK6,sK8,X0,sK8,sK6,sK8,X0) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_72366,plain,
( cyclic(sK6,sK2,sK8,sK8)
| ~ coll(sK8,sK8,sK2)
| ~ eqangle(sK8,sK6,sK8,sK2,sK8,sK6,sK8,sK2) ),
inference(instantiation,[status(thm)],[c_72365]) ).
tcf(c_72615,plain,
! [X0: $i] :
( cyclic(sK2,sK8,sK6,X0)
| ~ cyclic(sK2,sK6,sK8,X0) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_72616,plain,
( cyclic(sK2,sK8,sK6,sK2)
| ~ cyclic(sK2,sK6,sK8,sK2) ),
inference(instantiation,[status(thm)],[c_72615]) ).
tcf(c_72776,plain,
! [X0: $i,X1: $i] :
( cyclic(X1,sK7,sK8,sK6)
| ~ cyclic(X0,X1,sK7,sK8)
| ~ cyclic(X0,X1,sK7,sK6) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_72777,plain,
( cyclic(sK2,sK7,sK8,sK6)
| ~ cyclic(sK2,sK2,sK7,sK8)
| ~ cyclic(sK2,sK2,sK7,sK6) ),
inference(instantiation,[status(thm)],[c_72776]) ).
tcf(c_72875,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK6,sK2,X2,X3)
| ~ perp(sK6,sK2,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_72876,plain,
( para(sK6,sK2,sK2,sK2)
| ~ perp(sK6,sK2,sK2,sK2)
| ~ perp(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_72875]) ).
tcf(c_73788,plain,
! [X0: $i] :
( cyclic(X0,sK8,sK6,sK8)
| ~ cyclic(sK8,X0,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_73789,plain,
( cyclic(sK2,sK8,sK6,sK8)
| ~ cyclic(sK8,sK2,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_73788]) ).
tcf(c_73855,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK6,X0,X1)
| ~ cong(X0,X1,X0,sK6) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_73856,plain,
( cong(sK2,sK6,sK2,sK2)
| ~ cong(sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_73855]) ).
tcf(c_74603,plain,
! [X0: $i] :
( perp(sK6,sK2,sK2,X0)
| ~ cong(sK6,sK2,sK2,sK2)
| ~ cong(sK6,X0,sK2,X0) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_74604,plain,
( perp(sK6,sK2,sK2,sK2)
| ~ cong(sK6,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_74603]) ).
tcf(c_75204,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK6,sK8,X1)
| ~ cyclic(sK6,X0,sK8,X1) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_75205,plain,
( cyclic(sK2,sK6,sK8,sK2)
| ~ cyclic(sK6,sK2,sK8,sK2) ),
inference(instantiation,[status(thm)],[c_75204]) ).
tcf(c_75305,plain,
! [X0: $i,X1: $i] :
( cyclic(sK6,X0,sK8,X1)
| ~ cyclic(sK6,sK8,X0,X1) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_75306,plain,
( cyclic(sK6,sK2,sK8,sK2)
| ~ cyclic(sK6,sK8,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_75305]) ).
tcf(c_75426,plain,
! [X0: $i,X1: $i] :
( eqangle(sK2,sK6,sK6,sK7,X0,X1,sK6,sK7)
| ~ para(sK2,sK6,X0,X1) ),
inference(instantiation,[status(thm)],[c_66969]) ).
tcf(c_75999,plain,
! [X0: $i] :
( cong(sK6,sK2,X0,sK2)
| ~ cong(X0,sK2,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_76000,plain,
( cong(sK6,sK2,sK2,sK2)
| ~ cong(sK2,sK2,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_75999]) ).
tcf(c_77411,plain,
! [X0: $i,X1: $i] :
( eqangle(sK6,sK2,sK8,sK6,X0,X1,sK8,sK6)
| ~ para(sK6,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_66912]) ).
tcf(c_78146,plain,
! [X0: $i,X1: $i] :
( para(sK8,sK6,sK8,sK6)
| ~ eqangle(sK8,sK6,X0,X1,sK8,sK6,X0,X1) ),
inference(instantiation,[status(thm)],[c_65845]) ).
tcf(c_78147,plain,
( para(sK8,sK6,sK8,sK6)
| ~ eqangle(sK8,sK6,sK2,sK2,sK8,sK6,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_78146]) ).
tcf(c_78160,plain,
! [X0: $i,X1: $i] :
( eqangle(sK8,sK6,sK8,sK6,X0,X1,X0,X1)
| ~ eqangle(sK8,sK6,X0,X1,sK8,sK6,X0,X1) ),
inference(instantiation,[status(thm)],[c_66915]) ).
tcf(c_78161,plain,
( eqangle(sK8,sK6,sK8,sK6,sK2,sK2,sK2,sK2)
| ~ eqangle(sK8,sK6,sK2,sK2,sK8,sK6,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_78160]) ).
tcf(c_79219,plain,
! [X0: $i,X1: $i] :
( eqangle(X1,X0,sK6,sK7,sK6,sK8,sK6,sK7)
| ~ eqangle(X0,X1,sK6,sK7,sK6,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_70621]) ).
tcf(c_81418,plain,
! [X0: $i,X1: $i] :
( eqangle(sK2,sK6,X0,X1,sK2,sK6,X0,X1)
| ~ eqangle(X0,X1,sK2,sK6,X0,X1,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_68345]) ).
tcf(c_81419,plain,
( eqangle(sK2,sK6,sK2,sK2,sK2,sK6,sK2,sK2)
| ~ eqangle(sK2,sK2,sK2,sK6,sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_81418]) ).
tcf(c_82388,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,sK6,sK2,sK6,X0,X1,sK2,X2)
| ~ eqangle(X0,sK6,X0,X1,sK2,sK6,sK2,X2) ),
inference(instantiation,[status(thm)],[c_70365]) ).
tcf(c_82390,plain,
( eqangle(sK2,sK6,sK2,sK6,sK2,sK2,sK2,sK2)
| ~ eqangle(sK2,sK6,sK2,sK2,sK2,sK6,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_82388]) ).
tcf(c_83295,plain,
! [X0: $i,X1: $i] :
( eqangle(sK8,sK6,X0,X1,sK8,sK6,X0,X1)
| ~ para(sK8,sK6,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_66340]) ).
tcf(c_85284,plain,
( eqangle(sK8,sK6,sK6,sK8,sK6,sK2,sK6,sK8)
| ~ para(sK8,sK6,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_66515]) ).
tcf(c_85285,plain,
( eqangle(sK8,sK6,sK6,sK2,sK6,sK8,sK6,sK8)
| ~ eqangle(sK8,sK6,sK6,sK8,sK6,sK2,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_70318]) ).
tcf(c_85886,plain,
( eqangle(sK6,sK2,sK6,sK8,sK8,sK6,sK6,sK8)
| ~ para(sK6,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_69280]) ).
tcf(c_85887,plain,
( eqangle(sK6,sK8,sK6,sK2,sK6,sK8,sK8,sK6)
| ~ eqangle(sK6,sK2,sK6,sK8,sK8,sK6,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_69811]) ).
tcf(c_86165,plain,
( eqangle(sK2,sK6,sK6,sK7,sK6,sK8,sK6,sK7)
| ~ para(sK2,sK6,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_75426]) ).
tcf(c_86169,plain,
( eqangle(sK6,sK2,sK6,sK7,sK6,sK8,sK6,sK7)
| ~ eqangle(sK2,sK6,sK6,sK7,sK6,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_79219]) ).
tcf(c_86548,plain,
( eqangle(sK6,sK2,sK8,sK6,sK6,sK7,sK8,sK6)
| ~ para(sK6,sK2,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_77411]) ).
tcf(c_91953,plain,
! [X0: $i,X1: $i] :
( para(sK2,sK6,sK6,sK8)
| ~ perp(sK2,sK6,X0,X1)
| ~ perp(X0,X1,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_67692]) ).
tcf(c_91958,plain,
( para(sK2,sK6,sK6,sK8)
| ~ perp(sK2,sK6,sK2,sK2)
| ~ perp(sK2,sK2,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_91953]) ).
tcf(c_93032,plain,
! [X0: $i,X1: $i] :
( para(sK8,sK6,sK6,sK2)
| ~ perp(sK8,sK6,X0,X1)
| ~ perp(X0,X1,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_67701]) ).
tcf(c_93040,plain,
( para(sK8,sK6,sK6,sK2)
| ~ perp(sK8,sK6,sK2,sK2)
| ~ perp(sK2,sK2,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_93032]) ).
tcf(c_95585,plain,
! [X0: $i,X1: $i] :
( perp(sK6,sK2,sK6,sK8)
| ~ para(sK6,sK2,X0,X1)
| ~ perp(X0,X1,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_70665]) ).
tcf(c_95586,plain,
( perp(sK6,sK2,sK6,sK8)
| ~ para(sK6,sK2,sK2,sK2)
| ~ perp(sK2,sK2,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_95585]) ).
tcf(c_98365,plain,
! [X0: $i] :
( eqangle(sK8,sK6,sK8,X0,sK8,sK6,sK8,X0)
| ~ para(sK8,sK6,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_83295]) ).
tcf(c_98366,plain,
( eqangle(sK8,sK6,sK8,sK2,sK8,sK6,sK8,sK2)
| ~ para(sK8,sK6,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_98365]) ).
tcf(c_99621,plain,
! [X0: $i] :
( midp(sK6,sK6,X0)
| ~ midp(sK6,X0,sK6) ),
inference(instantiation,[status(thm)],[c_67170]) ).
tcf(c_99622,plain,
( midp(sK6,sK6,sK2)
| ~ midp(sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_99621]) ).
tcf(c_102273,plain,
! [X0: $i,X1: $i] :
( perp(sK8,sK6,sK8,sK6)
| ~ perp(X0,X1,X0,X1)
| ~ eqangle(sK8,sK6,sK8,sK6,X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_66562]) ).
tcf(c_102276,plain,
( perp(sK8,sK6,sK8,sK6)
| ~ perp(sK2,sK2,sK2,sK2)
| ~ eqangle(sK8,sK6,sK8,sK6,sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_102273]) ).
tcf(c_103566,plain,
! [X0: $i,X1: $i] :
( midp(sK2,sK6,sK8)
| ~ coll(sK2,sK6,sK8)
| ~ midp(X0,sK6,X1)
| ~ para(X0,sK2,X1,sK8) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_103567,plain,
( midp(sK2,sK6,sK8)
| ~ midp(sK2,sK6,sK2)
| ~ coll(sK2,sK6,sK8)
| ~ para(sK2,sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_103566]) ).
tcf(c_103646,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK8,sK6,sK6,sK2,sK6,sK7,sK8,sK6)
| ~ eqangle(sK8,sK6,sK6,sK2,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK6,sK7,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_103727,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,X2,sK2,sK8)
| ~ cyclic(X1,X2,X0,sK8)
| ~ cyclic(X1,X2,X0,sK2)
| ~ cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,sK2,X3,sK8) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_103759,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK6,sK8,X0,X1,sK6,sK7,sK8,sK6)
| ~ eqangle(X2,X3,X4,X5,sK6,sK7,sK8,sK6)
| ~ eqangle(sK6,sK8,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_104240,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK6,sK8,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK6,sK8,X4,X5) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_105001,plain,
! [X0: $i,X1: $i] :
( para(sK6,sK2,sK8,sK6)
| ~ perp(sK6,sK2,X0,X1)
| ~ perp(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_105002,plain,
( para(sK6,sK2,sK8,sK6)
| ~ perp(sK6,sK2,sK2,sK2)
| ~ perp(sK2,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_105001]) ).
tcf(c_106083,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK6,sK8)
| ~ perp(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_106141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK8,sK6)
| ~ perp(X2,X3,sK8,sK6)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_106840,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK2,X2,sK8)
| ~ cong(X0,X1,X0,sK8)
| ~ cong(X0,X1,X0,sK2)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_151]) ).
tcf(c_106841,plain,
( cyclic(sK2,sK2,sK2,sK8)
| ~ cong(sK2,sK2,sK2,sK8)
| ~ cong(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_106840]) ).
tcf(c_107375,plain,
! [X0: $i,X1: $i] :
( cyclic(sK6,sK8,X0,X1)
| ~ coll(X0,X1,sK8)
| ~ eqangle(X0,sK6,X0,sK8,X1,sK6,X1,sK8) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_107376,plain,
( cyclic(sK6,sK8,sK2,sK2)
| ~ coll(sK2,sK2,sK8)
| ~ eqangle(sK2,sK6,sK2,sK8,sK2,sK6,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_107375]) ).
tcf(c_111627,plain,
! [X0: $i,X1: $i] :
( eqangle(sK6,sK8,X0,X1,sK6,sK7,sK8,sK6)
| ~ eqangle(sK6,sK2,sK8,sK6,sK6,sK7,sK8,sK6)
| ~ eqangle(sK6,sK8,X0,X1,sK6,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_103759]) ).
tcf(c_111663,plain,
! [X0: $i,X1: $i] :
( eqangle(sK6,sK8,sK6,sK8,sK6,sK2,X0,X1)
| ~ eqangle(sK6,sK8,sK6,sK2,sK6,sK8,X0,X1) ),
inference(instantiation,[status(thm)],[c_104240]) ).
tcf(c_112687,plain,
( eqangle(sK8,sK6,sK6,sK2,sK6,sK7,sK8,sK6)
| ~ eqangle(sK8,sK6,sK6,sK2,sK6,sK8,sK6,sK8)
| ~ eqangle(sK6,sK8,sK6,sK8,sK6,sK7,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_103646]) ).
tcf(c_113707,plain,
! [X0: $i,X1: $i] :
( para(sK6,sK2,sK6,sK7)
| ~ perp(sK6,sK2,X0,X1)
| ~ perp(X0,X1,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_113708,plain,
( para(sK6,sK2,sK6,sK7)
| ~ perp(sK6,sK2,sK2,sK2)
| ~ perp(sK2,sK2,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_113707]) ).
tcf(c_115933,plain,
! [X0: $i] :
( perp(X0,sK8,sK6,sK8)
| ~ perp(X0,sK8,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_106083]) ).
tcf(c_115935,plain,
( perp(sK2,sK8,sK6,sK8)
| ~ perp(sK2,sK8,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_115933]) ).
tcf(c_117864,plain,
! [X0: $i] :
( cong(X0,sK8,X0,sK7)
| ~ cong(X0,sK7,X0,sK8) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_117865,plain,
( cong(sK2,sK8,sK2,sK7)
| ~ cong(sK2,sK7,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_117864]) ).
tcf(c_121016,plain,
! [X0: $i] :
( cong(sK2,sK8,sK2,sK8)
| ~ cyclic(sK2,sK8,sK6,sK8)
| ~ cyclic(sK2,sK8,sK6,sK2)
| ~ cyclic(sK2,sK8,sK6,X0)
| ~ eqangle(sK6,sK2,sK6,sK8,X0,sK2,X0,sK8) ),
inference(instantiation,[status(thm)],[c_103727]) ).
tcf(c_121017,plain,
( cong(sK2,sK8,sK2,sK8)
| ~ cyclic(sK2,sK8,sK6,sK8)
| ~ cyclic(sK2,sK8,sK6,sK2)
| ~ eqangle(sK6,sK2,sK6,sK8,sK2,sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_121016]) ).
tcf(c_122694,plain,
( eqangle(sK6,sK8,sK6,sK8,sK6,sK2,sK8,sK6)
| ~ eqangle(sK6,sK8,sK6,sK2,sK6,sK8,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_111663]) ).
tcf(c_123193,plain,
( eqangle(sK6,sK8,sK6,sK8,sK6,sK7,sK8,sK6)
| ~ eqangle(sK6,sK8,sK6,sK8,sK6,sK2,sK8,sK6)
| ~ eqangle(sK6,sK2,sK8,sK6,sK6,sK7,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_111627]) ).
tcf(c_125829,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,sK2,sK6)
| ~ cong(X0,X1,X0,sK6)
| ~ cong(X0,X1,X0,sK2)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_151]) ).
tcf(c_125830,plain,
( cyclic(sK2,sK2,sK2,sK6)
| ~ cong(sK2,sK2,sK2,sK6)
| ~ cong(sK2,sK2,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_125829]) ).
tcf(c_127363,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK8,sK6)
| ~ perp(sK8,sK6,sK8,sK6)
| ~ perp(X0,X1,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_106141]) ).
tcf(c_127364,plain,
( para(sK2,sK2,sK8,sK6)
| ~ perp(sK8,sK6,sK8,sK6)
| ~ perp(sK2,sK2,sK8,sK6) ),
inference(instantiation,[status(thm)],[c_127363]) ).
tcf(c_135733,plain,
! [X0: $i] :
( eqangle(X0,sK6,X0,sK8,X0,sK6,X0,sK8)
| ~ para(X0,sK6,X0,sK6) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_135734,plain,
( eqangle(sK2,sK6,sK2,sK8,sK2,sK6,sK2,sK8)
| ~ para(sK2,sK6,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_135733]) ).
tcf(c_162041,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK6,sK7,sK6,sK8)
| ~ eqangle(X0,X1,X2,X3,sK6,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_162939,plain,
! [X0: $i] :
( perp(sK8,sK6,sK6,sK7)
| ~ coll(X0,sK8,sK7)
| ~ circle(X0,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_162940,plain,
( perp(sK8,sK6,sK6,sK7)
| ~ coll(sK2,sK8,sK7)
| ~ circle(sK2,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_162939]) ).
tcf(c_163312,plain,
! [X0: $i] :
( circle(sK6,sK6,X0,sK8)
| ~ cong(sK6,sK6,sK6,sK8)
| ~ cong(sK6,sK6,sK6,X0) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_163369,plain,
! [X0: $i] :
( cong(sK6,X0,sK6,sK7)
| ~ cong(sK6,X0,sK7,sK6) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_163430,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,sK7,sK8)
| ~ cyclic(X0,X1,X2,sK7)
| ~ cyclic(X0,X1,X2,sK8) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_163431,plain,
( cyclic(sK2,sK2,sK7,sK8)
| ~ cyclic(sK2,sK2,sK2,sK7)
| ~ cyclic(sK2,sK2,sK2,sK8) ),
inference(instantiation,[status(thm)],[c_163430]) ).
tcf(c_163584,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK6,sK7,sK6,sK8,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_163772,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X0,X1,sK6,sK7)
| ~ perp(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK6,sK7,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_163867,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK6,sK7,X2,X3,sK6,sK8)
| ~ eqangle(X0,X1,X2,X3,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_163906,plain,
! [X0: $i,X1: $i] :
( eqangle(sK6,sK7,X0,X1,sK6,sK7,sK6,sK8)
| ~ eqangle(X0,X1,sK6,sK7,sK6,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_162041]) ).
tcf(c_164187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK7,X1)
| ~ coll(X3,sK7,X1)
| ~ circle(X2,X0,sK7,X1)
| ~ eqangle(X0,sK7,X0,X1,X2,sK7,X2,X3) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_166798,plain,
! [X0: $i] :
( cong(sK6,sK6,sK6,sK8)
| ~ midp(X0,sK6,sK8)
| ~ perp(sK6,X0,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_166799,plain,
( cong(sK6,sK6,sK6,sK8)
| ~ midp(sK2,sK6,sK8)
| ~ perp(sK6,sK2,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_166798]) ).
tcf(c_167241,plain,
! [X0: $i] :
( circle(X0,sK8,sK6,sK7)
| ~ midp(X0,sK6,sK8)
| ~ cong(X0,sK8,X0,sK7) ),
inference(instantiation,[status(thm)],[c_8322]) ).
tcf(c_167242,plain,
( circle(sK2,sK8,sK6,sK7)
| ~ midp(sK2,sK6,sK8)
| ~ cong(sK2,sK8,sK2,sK7) ),
inference(instantiation,[status(thm)],[c_167241]) ).
tcf(c_167469,plain,
( cong(sK6,sK6,sK6,sK7)
| ~ cong(sK6,sK6,sK7,sK6) ),
inference(instantiation,[status(thm)],[c_163369]) ).
tcf(c_167470,plain,
! [X0: $i] :
( cong(sK6,sK6,sK7,sK6)
| ~ midp(sK6,sK6,X0)
| ~ perp(sK6,sK7,sK7,X0) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_167471,plain,
( cong(sK6,sK6,sK7,sK6)
| ~ midp(sK6,sK6,sK2)
| ~ perp(sK6,sK7,sK7,sK2) ),
inference(instantiation,[status(thm)],[c_167470]) ).
tcf(c_167914,plain,
( eqangle(sK6,sK7,sK6,sK2,sK6,sK7,sK6,sK8)
| ~ eqangle(sK6,sK2,sK6,sK7,sK6,sK8,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_163906]) ).
tcf(c_168009,plain,
! [X0: $i] :
( cong(X0,sK7,X0,sK8)
| ~ midp(X0,sK7,sK8) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_168010,plain,
( cong(sK2,sK7,sK2,sK8)
| ~ midp(sK2,sK7,sK8) ),
inference(instantiation,[status(thm)],[c_168009]) ).
tcf(c_168280,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,sK7,sK6)
| ~ cyclic(X0,X1,X2,sK7)
| ~ cyclic(X0,X1,X2,sK6) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_168281,plain,
( cyclic(sK2,sK2,sK7,sK6)
| ~ cyclic(sK2,sK2,sK2,sK7)
| ~ cyclic(sK2,sK2,sK2,sK6) ),
inference(instantiation,[status(thm)],[c_168280]) ).
tcf(c_173503,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,X2,sK7)
| ~ cyclic(X0,X1,sK7,X2) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_173504,plain,
( cyclic(sK2,sK2,sK2,sK7)
| ~ cyclic(sK2,sK2,sK7,sK2) ),
inference(instantiation,[status(thm)],[c_173503]) ).
tcf(c_174818,plain,
! [X0: $i,X1: $i] :
( eqangle(sK6,sK7,sK6,sK8,sK6,sK7,X0,X1)
| ~ eqangle(sK6,sK7,X0,X1,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_163584]) ).
tcf(c_178633,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK6,sK7)
| ~ perp(sK8,sK6,sK6,sK7)
| ~ eqangle(X0,X1,sK6,sK7,sK8,sK6,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_163772]) ).
tcf(c_178634,plain,
( perp(sK2,sK2,sK6,sK7)
| ~ perp(sK8,sK6,sK6,sK7)
| ~ eqangle(sK2,sK2,sK6,sK7,sK8,sK6,sK6,sK7) ),
inference(instantiation,[status(thm)],[c_178633]) ).
tcf(c_197334,plain,
! [X0: $i] :
( midp(X0,sK7,sK8)
| ~ coll(X0,sK7,sK8)
| ~ circle(sK6,sK6,sK7,sK8)
| ~ eqangle(sK6,sK7,sK6,sK8,sK6,sK7,sK6,X0) ),
inference(instantiation,[status(thm)],[c_164187]) ).
tcf(c_197335,plain,
( midp(sK2,sK7,sK8)
| ~ coll(sK2,sK7,sK8)
| ~ circle(sK6,sK6,sK7,sK8)
| ~ eqangle(sK6,sK7,sK6,sK8,sK6,sK7,sK6,sK2) ),
inference(instantiation,[status(thm)],[c_197334]) ).
tcf(c_197345,plain,
( circle(sK6,sK6,sK7,sK8)
| ~ cong(sK6,sK6,sK6,sK7)
| ~ cong(sK6,sK6,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_163312]) ).
tcf(c_236330,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK7,sK8,X2)
| ~ cyclic(X0,X1,sK7,sK8)
| ~ cyclic(X0,X1,sK7,X2) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_236331,plain,
( cyclic(sK2,sK7,sK8,sK2)
| ~ cyclic(sK2,sK2,sK7,sK8)
| ~ cyclic(sK2,sK2,sK7,sK2) ),
inference(instantiation,[status(thm)],[c_236330]) ).
tcf(c_263654,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,sK7,X2)
| ~ cyclic(X0,sK7,X1,X2) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_263655,plain,
( cyclic(sK2,sK2,sK7,sK2)
| ~ cyclic(sK2,sK7,sK2,sK2) ),
inference(instantiation,[status(thm)],[c_263654]) ).
tcf(c_266536,plain,
! [X0: $i] :
( eqangle(X0,sK7,sK6,sK7,X0,sK8,sK6,sK8)
| ~ eqangle(X0,sK7,X0,sK8,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_163867]) ).
tcf(c_266547,plain,
( eqangle(sK2,sK7,sK6,sK7,sK2,sK8,sK6,sK8)
| ~ eqangle(sK2,sK7,sK2,sK8,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_266536]) ).
tcf(c_277617,plain,
! [X0: $i] :
( perp(X0,sK7,sK6,sK7)
| ~ perp(X0,sK8,sK6,sK8)
| ~ eqangle(X0,sK7,sK6,sK7,X0,sK8,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_163772]) ).
tcf(c_277630,plain,
( perp(sK2,sK7,sK6,sK7)
| ~ perp(sK2,sK8,sK6,sK8)
| ~ eqangle(sK2,sK7,sK6,sK7,sK2,sK8,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_277617]) ).
tcf(c_281650,plain,
! [X0: $i] :
( eqangle(sK6,sK7,sK6,sK8,sK6,sK7,sK6,X0)
| ~ eqangle(sK6,sK7,sK6,X0,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_174818]) ).
tcf(c_281651,plain,
( eqangle(sK6,sK7,sK6,sK8,sK6,sK7,sK6,sK2)
| ~ eqangle(sK6,sK7,sK6,sK2,sK6,sK7,sK6,sK8) ),
inference(instantiation,[status(thm)],[c_281650]) ).
tcf(c_281652,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_281651,c_277630,c_266547,c_263655,c_236331,c_197345,c_197335,c_178634,c_173504,c_168281,c_168010,c_167914,c_167471,c_167469,c_167242,c_166799,c_163431,c_162940,c_135734,c_127364,c_125830,c_123193,c_122694,c_121017,c_117865,c_115935,c_113708,c_112687,c_107376,c_106841,c_105002,c_103567,c_102276,c_99622,c_98366,c_95586,c_93040,c_91958,c_86548,c_86169,c_86165,c_85887,c_85886,c_85285,c_85284,c_82390,c_81419,c_78161,c_78147,c_76000,c_75306,c_75205,c_74604,c_73856,c_73789,c_72876,c_72777,c_72616,c_72366,c_72321,c_72284,c_72235,c_72219,c_69890,c_69817,c_69680,c_69586,c_68559,c_68472,c_68336,c_67944,c_67916,c_67877,c_67600,c_66913,c_66650,c_66579,c_66577,c_61640,c_58229,c_58064,c_49719,c_48715,c_47178,c_41952,c_38826,c_37523,c_37053,c_35904,c_35535,c_29290,c_25672,c_22096,c_21224,c_20885,c_20337,c_18320,c_17613,c_16248,c_15868,c_15679,c_13213,c_9260,c_9139,c_9134,c_8873,c_8718,c_7933,c_7844,c_7746,c_7391,c_7207,c_7178,c_6653,c_6651,c_6537,c_6457,c_5737,c_5589,c_5270,c_5263,c_3639,c_3307,c_3305,c_3082,c_3076,c_3042,c_3031,c_2923,c_2767,c_2627,c_2561,c_2548,c_2546,c_2536,c_2535,c_2534,c_2530,c_2524,c_203,c_165,c_161,c_155,c_49,c_54,c_56,c_58,c_60,c_63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO639+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 : n010.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.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 12:38:12 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 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.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 132.95/21.60 % SZS status Started for theBenchmark.p
% 132.95/21.60 % SZS status Theorem for theBenchmark.p
% 132.95/21.60
% 132.95/21.60 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 132.95/21.60
% 132.95/21.60 % ------ iProver source info
% 132.95/21.60
% 132.95/21.60 % git: date: 2026-07-19 20:42:38 +0200
% 132.95/21.60 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 132.95/21.60 % git: non_committed_changes: false
% 132.95/21.60
% 132.95/21.60 % ------ Parsing...
% 132.95/21.60 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 132.95/21.60
% 132.95/21.60 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 132.95/21.60
% 132.95/21.60 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 132.95/21.60 % ------ Proving...
% 132.95/21.60 % ------ Problem Properties
% 132.95/21.60
% 132.95/21.60 %
% 132.95/21.60 % clauses 102
% 132.95/21.60 % conjectures 15
% 132.95/21.60 % EPR 69
% 132.95/21.60 % Horn 96
% 132.95/21.60 % unary 14
% 132.95/21.60 % binary 25
% 132.95/21.60 % lits 272
% 132.95/21.60 % lits eq 0
% 132.95/21.60 % fd_pure 0
% 132.95/21.60 % fd_pseudo 0
% 132.95/21.60 % fd_cond 0
% 132.95/21.60 % fd_pseudo_cond 0
% 132.95/21.60 % AC symbols 0
% 132.95/21.60
% 132.95/21.60 % ------ Schedule dynamic 5 is on
% 132.95/21.60
% 132.95/21.60 % ------ no equalities: superposition off
% 132.95/21.60
% 132.95/21.60 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 132.95/21.60
% 132.95/21.60
% 132.95/21.60 % ------
% 132.95/21.60 % Current options:
% 132.95/21.60 % ------
% 132.95/21.60
% 132.95/21.60
% 132.95/21.60 %
% 132.95/21.60
% 132.95/21.60 % ------ Proving...
% 132.95/21.60 % Proof_search_loop: time out after: 6156 full_loop iterations
% 132.95/21.60
% 132.95/21.60 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 132.95/21.60
% 132.95/21.60
% 132.95/21.60 % ------
% 132.95/21.60 % Current options:
% 132.95/21.60 % ------
% 132.95/21.60
% 132.95/21.60
% 132.95/21.60 %
% 132.95/21.60
% 132.95/21.60 % ------ Proving...
% 132.95/21.60 %
% 132.95/21.60
% 132.95/21.60 % SZS status Theorem for theBenchmark.p
% 132.95/21.60
% 132.95/21.60 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 132.95/21.62
% 132.95/21.62
%------------------------------------------------------------------------------