%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO551+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n020.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:27 PM UTC 2026
% Result : Theorem 27.70s 4.86s
% Output : CNFRefutation 27.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 33
% Syntax : Number of formulae : 368 ( 46 unt; 0 def)
% Number of atoms : 916 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1022 ( 474 ~; 468 |; 46 &)
% ( 0 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 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 : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 839 ( 0 sgn 825 !; 14 ?; 300 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD2) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( coll(X0,X1,X3)
& coll(X0,X1,X2) )
=> coll(X2,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD3) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD4) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD5) ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD7) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD8) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& perp(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(f10,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> perp(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD10) ).
fof(f11,axiom,
! [X0,X1,X2] :
( midp(X2,X1,X0)
=> midp(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD11) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( ( cong(X3,X0,X3,X2)
& cong(X3,X0,X3,X1) )
=> circle(X3,X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD12) ).
fof(f13,axiom,
! [X0,X1,X2,X3,X4] :
( ( cong(X4,X0,X4,X3)
& cong(X4,X0,X4,X2)
& cong(X4,X0,X4,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD13) ).
fof(f15,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD15) ).
fof(f16,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X1,X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD16) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD23) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD24) ).
fof(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/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD25) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( coll(X2,X3,X1)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
& cyclic(X0,X1,X2,X5)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f45,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X0,X2)
& midp(X3,X0,X1) )
=> para(X3,X4,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD44) ).
fof(f46,axiom,
! [X0,X1,X2,X3,X4] :
( ( coll(X4,X0,X2)
& para(X3,X4,X1,X2)
& midp(X3,X0,X1) )
=> midp(X4,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD45) ).
fof(f53,axiom,
! [X0,X1,X2,X3] :
( ( midp(X3,X0,X2)
& perp(X0,X1,X1,X2) )
=> cong(X0,X3,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD52) ).
fof(f54,axiom,
! [X0,X1,X2,X3] :
( ( coll(X3,X0,X2)
& circle(X3,X0,X1,X2) )
=> perp(X0,X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD53) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( perp(X3,X2,X0,X1)
& midp(X2,X0,X1) )
=> cong(X3,X0,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD55) ).
fof(f57,axiom,
! [X0,X1,X2,X3] :
( ( cong(X0,X3,X1,X3)
& cong(X0,X2,X1,X2) )
=> perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD56) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X2,X3)
& midp(X4,X0,X1) )
=> para(X0,X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD63) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4] :
( ( para(X0,X3,X1,X2)
& para(X0,X2,X1,X3)
& midp(X4,X0,X1) )
=> midp(X4,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD64) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( coll(X0,X1,X2)
& cong(X0,X1,X0,X2) )
=> midp(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD67) ).
fof(f69,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> cong(X0,X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD68) ).
fof(f70,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD69) ).
fof(f74,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( para(X4,X5,X6,X7)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD73) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( midp(X6,X0,X2)
& midp(X5,X2,X1)
& midp(X4,X0,X1)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2) )
=> cyclic(X4,X3,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL012011) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6] :
( ( midp(X6,X0,X2)
& midp(X5,X2,X1)
& midp(X4,X0,X1)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2) )
=> cyclic(X4,X3,X5,X6) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
? [X0,X1,X2,X3,X4,X5,X6] :
( midp(X6,X0,X2)
& midp(X5,X2,X1)
& midp(X4,X0,X1)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2)
& ~ cyclic(X4,X3,X5,X6) ),
inference(ennf_transformation,[],[f96]) ).
fof(f99,plain,
? [X0,X1,X2,X3,X4,X5,X6] :
( midp(X6,X0,X2)
& midp(X5,X2,X1)
& midp(X4,X0,X1)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2)
& ~ cyclic(X4,X3,X5,X6) ),
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(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(f174,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(f175,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,[],[f174]) ).
fof(f176,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(f177,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,[],[f176]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f186,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(f187,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,[],[f186]) ).
fof(f188,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(f189,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,[],[f188]) ).
fof(f190,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(f194,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f195,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f197,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(f198,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f197]) ).
fof(f199,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f200,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f209,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f208]) ).
fof(f218,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(f219,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(flattening,[],[f218]) ).
fof(f220,plain,
( midp(sK6,sK0,sK2)
& midp(sK5,sK2,sK1)
& midp(sK4,sK0,sK1)
& coll(sK3,sK1,sK2)
& perp(sK3,sK0,sK1,sK2)
& ~ cyclic(sK4,sK3,sK5,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6)],[f99]) ).
fof(f239,plain,
midp(sK6,sK0,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f240,plain,
midp(sK5,sK2,sK1),
inference(cnf_transformation,[],[f220]) ).
fof(f241,plain,
midp(sK4,sK0,sK1),
inference(cnf_transformation,[],[f220]) ).
fof(f242,plain,
coll(sK3,sK1,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f243,plain,
perp(sK3,sK0,sK1,sK2),
inference(cnf_transformation,[],[f220]) ).
fof(f244,plain,
~ cyclic(sK4,sK3,sK5,sK6),
inference(cnf_transformation,[],[f220]) ).
fof(f266,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f267,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f122]) ).
fof(f270,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(f271,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f130]) ).
fof(f273,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f281,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(f282,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f145]) ).
fof(f283,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f147]) ).
fof(f284,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(f285,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(f286,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f287,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f153]) ).
fof(f291,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f156]) ).
fof(f292,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(f293,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f160]) ).
fof(f294,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f162]) ).
fof(f295,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f163]) ).
fof(f302,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,[],[f175]) ).
fof(f303,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,[],[f177]) ).
fof(f307,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f183]) ).
fof(f308,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f184]) ).
fof(f310,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,[],[f187]) ).
fof(f311,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,[],[f189]) ).
fof(f312,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f190]) ).
fof(f315,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f194]) ).
fof(f316,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f195]) ).
fof(f318,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,[],[f198]) ).
fof(f319,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f199]) ).
fof(f320,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f200]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f209]) ).
fof(f332,plain,
! [X2,X3,X0,X1] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_49,negated_conjecture,
~ cyclic(sK4,sK3,sK5,sK6),
inference(cnf_transformation,[],[f244]) ).
tcf(c_50,negated_conjecture,
perp(sK3,sK0,sK1,sK2),
inference(cnf_transformation,[],[f243]) ).
tcf(c_51,negated_conjecture,
coll(sK3,sK1,sK2),
inference(cnf_transformation,[],[f242]) ).
tcf(c_52,negated_conjecture,
midp(sK4,sK0,sK1),
inference(cnf_transformation,[],[f241]) ).
tcf(c_53,negated_conjecture,
midp(sK5,sK2,sK1),
inference(cnf_transformation,[],[f240]) ).
tcf(c_54,negated_conjecture,
midp(sK6,sK0,sK2),
inference(cnf_transformation,[],[f239]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_80,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,[],[f270]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_91,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,[],[f281]) ).
tcf(c_92,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,[],[f282]) ).
tcf(c_93,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,[],[f283]) ).
tcf(c_94,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,[],[f284]) ).
tcf(c_95,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,[],[f285]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_102,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,[],[f292]) ).
tcf(c_103,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,[],[f293]) ).
tcf(c_104,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,[],[f294]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_112,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,[],[f302]) ).
tcf(c_113,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,[],[f303]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_120,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,[],[f310]) ).
tcf(c_121,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,[],[f311]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_128,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,[],[f318]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X2,X3,X0,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_137,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,[],[f327]) ).
tcf(c_142,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,[],[f332]) ).
tcf(c_149,plain,
( eqangle(sK1,sK1,sK1,sK1,sK1,sK1,sK1,sK1)
| ~ para(sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_152,plain,
( midp(sK1,sK1,sK1)
| ~ coll(sK1,sK1,sK1)
| ~ cong(sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_156,plain,
( perp(sK1,sK1,sK1,sK1)
| ~ cong(sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_161,plain,
( cyclic(sK1,sK1,sK1,sK1)
| ~ coll(sK1,sK1,sK1)
| ~ eqangle(sK1,sK1,sK1,sK1,sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_194,plain,
( cong(sK1,sK1,sK1,sK1)
| ~ cyclic(sK1,sK1,sK1,sK1)
| ~ eqangle(sK1,sK1,sK1,sK1,sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_1915,plain,
( coll(sK4,sK0,sK1)
| ~ midp(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_1916,plain,
( coll(sK5,sK2,sK1)
| ~ midp(sK5,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_1918,plain,
( coll(sK1,sK3,sK2)
| ~ coll(sK3,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_1920,plain,
( midp(sK4,sK1,sK0)
| ~ midp(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_1921,plain,
( midp(sK5,sK1,sK2)
| ~ midp(sK5,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_1923,plain,
( cong(sK4,sK0,sK4,sK1)
| ~ midp(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_1924,plain,
( cong(sK5,sK2,sK5,sK1)
| ~ midp(sK5,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_1927,plain,
( perp(sK3,sK0,sK2,sK1)
| ~ perp(sK3,sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_1931,plain,
! [X0: $i,X1: $i] :
( para(sK0,X0,sK1,X1)
| ~ midp(sK4,sK0,sK1)
| ~ midp(sK4,X0,X1) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1943,plain,
! [X0: $i] :
( cong(X0,sK0,X0,sK1)
| ~ midp(sK4,sK0,sK1)
| ~ perp(X0,sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_1944,plain,
( cong(sK1,sK0,sK1,sK1)
| ~ midp(sK4,sK0,sK1)
| ~ perp(sK1,sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_1943]) ).
tcf(c_1945,plain,
! [X0: $i] :
( cong(X0,sK2,X0,sK1)
| ~ midp(sK5,sK2,sK1)
| ~ perp(X0,sK5,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_1946,plain,
( cong(sK1,sK2,sK1,sK1)
| ~ midp(sK5,sK2,sK1)
| ~ perp(sK1,sK5,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_1945]) ).
tcf(c_2047,plain,
! [X0: $i] :
( coll(sK1,X0,sK4)
| ~ coll(sK4,sK0,sK1)
| ~ coll(sK4,sK0,X0) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_2050,plain,
( coll(sK1,sK1,sK4)
| ~ coll(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_2047]) ).
tcf(c_2053,plain,
! [X0: $i] :
( perp(sK0,X0,X0,sK1)
| ~ coll(sK4,sK0,sK1)
| ~ circle(sK4,sK0,X0,sK1) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_2054,plain,
( perp(sK0,sK1,sK1,sK1)
| ~ coll(sK4,sK0,sK1)
| ~ circle(sK4,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_2053]) ).
tcf(c_2078,plain,
! [X0: $i] :
( perp(sK2,X0,X0,sK1)
| ~ coll(sK5,sK2,sK1)
| ~ circle(sK5,sK2,X0,sK1) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_2079,plain,
( perp(sK2,sK1,sK1,sK1)
| ~ coll(sK5,sK2,sK1)
| ~ circle(sK5,sK2,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_2078]) ).
tcf(c_2123,plain,
( coll(sK1,sK2,sK3)
| ~ coll(sK1,sK3,sK2) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_2181,plain,
! [X0: $i] :
( cong(sK1,sK4,X0,sK4)
| ~ midp(sK4,sK1,sK0)
| ~ perp(sK1,X0,X0,sK0) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_2182,plain,
( cong(sK1,sK4,sK1,sK4)
| ~ midp(sK4,sK1,sK0)
| ~ perp(sK1,sK1,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_2181]) ).
tcf(c_2206,plain,
! [X0: $i] :
( cong(sK1,sK5,X0,sK5)
| ~ midp(sK5,sK1,sK2)
| ~ perp(sK1,X0,X0,sK2) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_2207,plain,
( cong(sK1,sK5,sK1,sK5)
| ~ midp(sK5,sK1,sK2)
| ~ perp(sK1,sK1,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_2206]) ).
tcf(c_2241,plain,
! [X0: $i] :
( circle(sK4,sK0,sK1,X0)
| ~ cong(sK4,sK0,sK4,sK1)
| ~ cong(sK4,sK0,sK4,X0) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_2245,plain,
( circle(sK4,sK0,sK1,sK1)
| ~ cong(sK4,sK0,sK4,sK1) ),
inference(instantiation,[status(thm)],[c_2241]) ).
tcf(c_2254,plain,
! [X0: $i] :
( circle(sK5,sK2,sK1,X0)
| ~ cong(sK5,sK2,sK5,sK1)
| ~ cong(sK5,sK2,sK5,X0) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_2258,plain,
( circle(sK5,sK2,sK1,sK1)
| ~ cong(sK5,sK2,sK5,sK1) ),
inference(instantiation,[status(thm)],[c_2254]) ).
tcf(c_2298,plain,
! [X0: $i,X1: $i] :
( para(sK3,sK0,X0,X1)
| ~ perp(sK3,sK0,sK2,sK1)
| ~ perp(sK2,sK1,X0,X1) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_2301,plain,
( perp(sK2,sK1,sK3,sK0)
| ~ perp(sK3,sK0,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_2303,plain,
( para(sK3,sK0,sK1,sK1)
| ~ perp(sK2,sK1,sK1,sK1)
| ~ perp(sK3,sK0,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_2298]) ).
tcf(c_2309,plain,
( para(sK0,sK0,sK1,sK1)
| ~ midp(sK4,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_1931]) ).
tcf(c_2413,plain,
( para(sK1,sK1,sK0,sK0)
| ~ para(sK0,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_2415,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X2,X3)
| ~ para(sK0,sK0,sK1,sK1)
| ~ eqangle(X0,X1,X2,X3,sK0,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_2416,plain,
( para(sK1,sK1,sK1,sK1)
| ~ para(sK0,sK0,sK1,sK1)
| ~ eqangle(sK1,sK1,sK1,sK1,sK0,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_2415]) ).
tcf(c_2547,plain,
coll(sK4,sK0,sK1),
inference(superposition,[status(thm)],[c_52,c_76]) ).
tcf(c_2548,plain,
coll(sK5,sK2,sK1),
inference(superposition,[status(thm)],[c_53,c_76]) ).
tcf(c_2549,plain,
coll(sK6,sK0,sK2),
inference(superposition,[status(thm)],[c_54,c_76]) ).
tcf(c_2559,plain,
coll(sK1,sK3,sK2),
inference(superposition,[status(thm)],[c_51,c_82]) ).
tcf(c_2561,plain,
coll(sK2,sK5,sK1),
inference(superposition,[status(thm)],[c_2548,c_82]) ).
tcf(c_2609,plain,
coll(sK3,sK2,sK1),
inference(superposition,[status(thm)],[c_51,c_83]) ).
tcf(c_2610,plain,
coll(sK4,sK1,sK0),
inference(superposition,[status(thm)],[c_2547,c_83]) ).
tcf(c_2611,plain,
coll(sK5,sK1,sK2),
inference(superposition,[status(thm)],[c_2548,c_83]) ).
tcf(c_2660,plain,
midp(sK6,sK2,sK0),
inference(superposition,[status(thm)],[c_54,c_105]) ).
tcf(c_2715,plain,
coll(sK1,sK2,sK3),
inference(superposition,[status(thm)],[c_2559,c_83]) ).
tcf(c_2723,plain,
coll(sK2,sK1,sK5),
inference(superposition,[status(thm)],[c_2561,c_83]) ).
tcf(c_2744,plain,
coll(sK1,sK4,sK0),
inference(superposition,[status(thm)],[c_2610,c_82]) ).
tcf(c_2783,plain,
coll(sK1,sK5,sK2),
inference(superposition,[status(thm)],[c_2611,c_82]) ).
tcf(c_2795,plain,
coll(sK2,sK1,sK3),
inference(superposition,[status(thm)],[c_2715,c_82]) ).
tcf(c_2846,plain,
perp(sK1,sK2,sK3,sK0),
inference(superposition,[status(thm)],[c_50,c_96]) ).
tcf(c_3050,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_101,c_129]) ).
tcf(c_3075,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X1,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_3050,c_130]) ).
tcf(c_3194,plain,
! [X0: $i] :
( coll(sK2,X0,sK3)
| ~ coll(sK3,sK1,X0) ),
inference(superposition,[status(thm)],[c_51,c_81]) ).
tcf(c_3195,plain,
! [X0: $i] :
( coll(sK1,X0,sK4)
| ~ coll(sK4,sK0,X0) ),
inference(superposition,[status(thm)],[c_2547,c_81]) ).
tcf(c_3196,plain,
! [X0: $i] :
( coll(sK1,X0,sK5)
| ~ coll(sK5,sK2,X0) ),
inference(superposition,[status(thm)],[c_2548,c_81]) ).
tcf(c_3197,plain,
! [X0: $i] :
( coll(sK2,X0,sK6)
| ~ coll(sK6,sK0,X0) ),
inference(superposition,[status(thm)],[c_2549,c_81]) ).
tcf(c_3199,plain,
! [X0: $i] :
( coll(sK1,X0,sK3)
| ~ coll(sK3,sK2,X0) ),
inference(superposition,[status(thm)],[c_2609,c_81]) ).
tcf(c_3200,plain,
! [X0: $i] :
( coll(sK3,X0,sK2)
| ~ coll(sK2,sK1,X0) ),
inference(superposition,[status(thm)],[c_2795,c_81]) ).
tcf(c_3211,plain,
! [X0: $i] :
( coll(sK0,X0,sK1)
| ~ coll(sK1,sK4,X0) ),
inference(superposition,[status(thm)],[c_2744,c_81]) ).
tcf(c_3212,plain,
! [X0: $i] :
( coll(sK2,X0,sK1)
| ~ coll(sK1,sK5,X0) ),
inference(superposition,[status(thm)],[c_2783,c_81]) ).
tcf(c_3271,plain,
( coll(sK2,sK1,sK1)
| ~ coll(sK1,sK5,sK1) ),
inference(instantiation,[status(thm)],[c_3212]) ).
tcf(c_3272,plain,
( coll(sK0,sK1,sK1)
| ~ coll(sK1,sK4,sK1) ),
inference(instantiation,[status(thm)],[c_3211]) ).
tcf(c_3739,plain,
! [X0: $i,X1: $i] :
( para(X0,sK4,X1,sK1)
| ~ midp(X0,sK0,X1) ),
inference(superposition,[status(thm)],[c_52,c_104]) ).
tcf(c_3740,plain,
! [X0: $i,X1: $i] :
( para(X0,sK5,X1,sK1)
| ~ midp(X0,sK2,X1) ),
inference(superposition,[status(thm)],[c_53,c_104]) ).
tcf(c_3741,plain,
! [X0: $i,X1: $i] :
( para(X0,sK6,X1,sK2)
| ~ midp(X0,sK0,X1) ),
inference(superposition,[status(thm)],[c_54,c_104]) ).
tcf(c_3744,plain,
! [X0: $i,X1: $i] :
( para(X0,sK6,X1,sK0)
| ~ midp(X0,sK2,X1) ),
inference(superposition,[status(thm)],[c_2660,c_104]) ).
tcf(c_3805,plain,
! [X0: $i,X1: $i] :
( midp(sK1,sK2,sK3)
| ~ coll(sK1,sK2,sK3)
| ~ midp(X0,sK2,X1)
| ~ para(X0,sK1,X1,sK3) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_3806,plain,
( midp(sK1,sK2,sK3)
| ~ midp(sK1,sK2,sK1)
| ~ coll(sK1,sK2,sK3)
| ~ para(sK1,sK1,sK1,sK3) ),
inference(instantiation,[status(thm)],[c_3805]) ).
tcf(c_3843,plain,
coll(sK2,sK2,sK3),
inference(superposition,[status(thm)],[c_51,c_3194]) ).
tcf(c_3849,plain,
! [X0: $i] :
( coll(sK3,X0,sK2)
| ~ coll(sK2,sK2,X0) ),
inference(superposition,[status(thm)],[c_3843,c_81]) ).
tcf(c_4109,plain,
! [X0: $i,X1: $i] :
( para(X0,sK4,sK1,X1)
| ~ midp(X0,sK0,X1) ),
inference(superposition,[status(thm)],[c_3739,c_126]) ).
tcf(c_4110,plain,
! [X0: $i,X1: $i] :
( para(X1,sK1,X0,sK4)
| ~ midp(X0,sK0,X1) ),
inference(superposition,[status(thm)],[c_3739,c_125]) ).
tcf(c_4119,plain,
( para(sK1,sK1,sK1,sK4)
| ~ midp(sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_4110]) ).
tcf(c_4139,plain,
! [X0: $i,X1: $i] :
( para(sK2,sK1,X0,X1)
| ~ perp(sK2,sK1,sK3,sK0)
| ~ perp(sK3,sK0,X0,X1) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_4144,plain,
( para(sK2,sK1,sK1,sK1)
| ~ perp(sK2,sK1,sK3,sK0)
| ~ perp(sK3,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_4139]) ).
tcf(c_4153,plain,
! [X0: $i,X1: $i] :
( para(X0,sK5,sK1,X1)
| ~ midp(X0,sK2,X1) ),
inference(superposition,[status(thm)],[c_3740,c_126]) ).
tcf(c_4154,plain,
! [X0: $i,X1: $i] :
( para(X1,sK1,X0,sK5)
| ~ midp(X0,sK2,X1) ),
inference(superposition,[status(thm)],[c_3740,c_125]) ).
tcf(c_4163,plain,
( para(sK1,sK1,sK1,sK5)
| ~ midp(sK1,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_4154]) ).
tcf(c_4192,plain,
! [X0: $i] :
( coll(sK1,sK4,X0)
| ~ coll(sK1,X0,sK4) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_4194,plain,
( coll(sK1,sK4,sK1)
| ~ coll(sK1,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_4192]) ).
tcf(c_4216,plain,
! [X0: $i,X1: $i] :
( para(X1,sK2,X0,sK6)
| ~ midp(X0,sK0,X1) ),
inference(superposition,[status(thm)],[c_3741,c_125]) ).
tcf(c_4253,plain,
coll(sK1,sK1,sK4),
inference(superposition,[status(thm)],[c_2547,c_3195]) ).
tcf(c_4269,plain,
coll(sK1,sK4,sK1),
inference(superposition,[status(thm)],[c_4253,c_83]) ).
tcf(c_4300,plain,
coll(sK1,sK1,sK5),
inference(superposition,[status(thm)],[c_2548,c_3196]) ).
tcf(c_4399,plain,
! [X0: $i] :
( coll(sK1,X0,sK1)
| ~ coll(sK1,sK4,X0) ),
inference(superposition,[status(thm)],[c_4269,c_81]) ).
tcf(c_4404,plain,
( coll(sK1,sK1,sK1)
| ~ coll(sK1,sK4,sK1) ),
inference(instantiation,[status(thm)],[c_4399]) ).
tcf(c_4411,plain,
coll(sK1,sK5,sK1),
inference(superposition,[status(thm)],[c_4300,c_83]) ).
tcf(c_4482,plain,
coll(sK2,sK2,sK6),
inference(superposition,[status(thm)],[c_2549,c_3197]) ).
tcf(c_4620,plain,
coll(sK3,sK6,sK2),
inference(superposition,[status(thm)],[c_4482,c_3849]) ).
tcf(c_4678,plain,
coll(sK3,sK5,sK2),
inference(superposition,[status(thm)],[c_2723,c_3200]) ).
tcf(c_4747,plain,
( cong(sK3,sK1,sK3,sK2)
| ~ midp(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_50,c_92]) ).
tcf(c_5011,plain,
( cong(sK3,sK2,sK3,sK1)
| ~ midp(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_4747,c_129]) ).
tcf(c_5033,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK3,X1)
| ~ midp(X0,X1,sK3) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_5290,plain,
! [X0: $i] :
( perp(X0,sK4,sK0,sK1)
| ~ perp(sK0,sK1,X0,sK4) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_5291,plain,
( perp(sK1,sK4,sK0,sK1)
| ~ perp(sK0,sK1,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_5290]) ).
tcf(c_5292,plain,
! [X0: $i] :
( perp(X0,sK5,sK2,sK1)
| ~ perp(sK2,sK1,X0,sK5) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_5293,plain,
( perp(sK1,sK5,sK2,sK1)
| ~ perp(sK2,sK1,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_5292]) ).
tcf(c_5302,plain,
! [X0: $i,X1: $i] :
( perp(X1,X0,X0,sK3)
| ~ perp(X0,sK3,X1,X0) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_5303,plain,
( perp(sK1,sK1,sK1,sK3)
| ~ perp(sK1,sK3,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_5302]) ).
tcf(c_5340,plain,
! [X0: $i] :
( perp(sK1,X0,X0,sK0)
| ~ perp(sK1,X0,sK0,X0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_5341,plain,
( perp(sK1,sK1,sK1,sK0)
| ~ perp(sK1,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_5340]) ).
tcf(c_5357,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK1,sK2)
| ~ para(X0,X1,sK3,sK0) ),
inference(superposition,[status(thm)],[c_50,c_94]) ).
tcf(c_5392,plain,
( perp(sK1,sK1,sK1,sK2)
| ~ para(sK1,sK1,sK3,sK0) ),
inference(instantiation,[status(thm)],[c_5357]) ).
tcf(c_5486,plain,
( cyclic(sK4,sK3,sK5,sK6)
| ~ cyclic(sK3,sK4,sK5,sK6) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_5504,plain,
! [X0: $i,X1: $i] :
( para(sK1,sK2,X0,X1)
| ~ perp(sK3,sK0,X0,X1) ),
inference(superposition,[status(thm)],[c_2846,c_95]) ).
tcf(c_5536,plain,
( para(sK1,sK2,sK1,sK1)
| ~ perp(sK3,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_5504]) ).
tcf(c_5796,plain,
! [X0: $i] :
( coll(X0,sK0,sK1)
| ~ coll(sK0,X0,sK1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_5797,plain,
( coll(sK1,sK0,sK1)
| ~ coll(sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_5796]) ).
tcf(c_5809,plain,
! [X0: $i] :
( coll(X0,sK2,sK1)
| ~ coll(sK2,X0,sK1) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_5810,plain,
( coll(sK1,sK2,sK1)
| ~ coll(sK2,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_5809]) ).
tcf(c_5863,plain,
coll(sK3,sK2,sK6),
inference(superposition,[status(thm)],[c_4620,c_83]) ).
tcf(c_5864,plain,
coll(sK6,sK3,sK2),
inference(superposition,[status(thm)],[c_4620,c_82]) ).
tcf(c_6021,plain,
coll(sK3,sK2,sK5),
inference(superposition,[status(thm)],[c_4678,c_83]) ).
tcf(c_6198,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK3,sK0)
| ~ para(sK3,sK0,X0,X1) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_6199,plain,
( para(sK1,sK1,sK3,sK0)
| ~ para(sK3,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_6198]) ).
tcf(c_6385,plain,
! [X0: $i] :
( perp(X0,sK6,sK1,sK2)
| ~ midp(X0,sK2,sK3) ),
inference(superposition,[status(thm)],[c_3744,c_5357]) ).
tcf(c_6712,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK3,sK2)
| ~ midp(sK0,sK1,sK2)
| ~ cong(X0,X1,sK3,sK1) ),
inference(superposition,[status(thm)],[c_4747,c_128]) ).
tcf(c_7856,plain,
! [X0: $i,X1: $i] :
( eqangle(sK1,sK1,X0,X1,sK0,sK0,X0,X1)
| ~ para(sK1,sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_7857,plain,
( eqangle(sK1,sK1,sK1,sK1,sK0,sK0,sK1,sK1)
| ~ para(sK1,sK1,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_7856]) ).
tcf(c_8089,plain,
! [X0: $i] :
( perp(sK1,sK2,X0,sK6)
| ~ midp(X0,sK2,sK3) ),
inference(superposition,[status(thm)],[c_6385,c_96]) ).
tcf(c_8237,plain,
coll(sK1,sK6,sK3),
inference(superposition,[status(thm)],[c_5863,c_3199]) ).
tcf(c_8247,plain,
! [X0: $i] :
( coll(sK2,X0,sK6)
| ~ coll(sK6,sK3,X0) ),
inference(superposition,[status(thm)],[c_5864,c_81]) ).
tcf(c_8252,plain,
( coll(sK2,sK1,sK6)
| ~ coll(sK6,sK3,sK1) ),
inference(instantiation,[status(thm)],[c_8247]) ).
tcf(c_8713,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK3,sK1)
| ~ midp(sK0,sK1,sK2)
| ~ cong(X0,X1,sK3,sK2) ),
inference(superposition,[status(thm)],[c_5011,c_128]) ).
tcf(c_8727,plain,
( cong(sK1,sK1,sK3,sK1)
| ~ midp(sK0,sK1,sK2)
| ~ cong(sK1,sK1,sK3,sK2) ),
inference(instantiation,[status(thm)],[c_8713]) ).
tcf(c_9131,plain,
coll(sK1,sK5,sK3),
inference(superposition,[status(thm)],[c_6021,c_3199]) ).
tcf(c_10219,plain,
! [X0: $i] :
( perp(X0,sK1,sK0,X0)
| ~ perp(sK0,X0,X0,sK1) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_10220,plain,
( perp(sK1,sK1,sK0,sK1)
| ~ perp(sK0,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_10219]) ).
tcf(c_10291,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK2,X1,sK6)
| ~ coll(sK2,X1,sK6)
| ~ midp(X2,sK0,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_4216,c_80]) ).
tcf(c_10400,plain,
( midp(sK2,sK1,sK6)
| ~ midp(sK1,sK1,sK1)
| ~ midp(sK1,sK0,sK1)
| ~ coll(sK2,sK1,sK6) ),
inference(instantiation,[status(thm)],[c_10291]) ).
tcf(c_10916,plain,
coll(sK6,sK1,sK3),
inference(superposition,[status(thm)],[c_8237,c_82]) ).
tcf(c_11755,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK1,sK2)
| ~ para(sK1,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_11756,plain,
( para(sK1,sK1,sK1,sK2)
| ~ para(sK1,sK2,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_11755]) ).
tcf(c_12280,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK0,X1)
| ~ coll(X0,sK0,X1)
| ~ cong(X0,sK0,X0,X1) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_12281,plain,
( midp(sK1,sK0,sK1)
| ~ coll(sK1,sK0,sK1)
| ~ cong(sK1,sK0,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_12280]) ).
tcf(c_12282,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK2,X1)
| ~ coll(X0,sK2,X1)
| ~ cong(X0,sK2,X0,X1) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_12283,plain,
( midp(sK1,sK2,sK1)
| ~ coll(sK1,sK2,sK1)
| ~ cong(sK1,sK2,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_12282]) ).
tcf(c_12291,plain,
( midp(sK0,sK1,sK1)
| ~ coll(sK0,sK1,sK1)
| ~ cong(sK0,sK1,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_12667,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X1,sK4)
| ~ cong(X0,sK4,X1,sK4)
| ~ cong(X0,X1,X1,X1) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_12668,plain,
( perp(sK1,sK1,sK1,sK4)
| ~ cong(sK1,sK1,sK1,sK1)
| ~ cong(sK1,sK4,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_12667]) ).
tcf(c_12669,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X1,sK5)
| ~ cong(X0,sK5,X1,sK5)
| ~ cong(X0,X1,X1,X1) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_12670,plain,
( perp(sK1,sK1,sK1,sK5)
| ~ cong(sK1,sK1,sK1,sK1)
| ~ cong(sK1,sK5,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_12669]) ).
tcf(c_12722,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK3,sK0,X2,X3)
| ~ para(sK3,sK0,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_12723,plain,
( perp(sK3,sK0,sK1,sK1)
| ~ para(sK3,sK0,sK1,sK1)
| ~ perp(sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_12722]) ).
tcf(c_12914,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK0,X3,sK1,X2)
| ~ perp(sK0,X3,X0,X1)
| ~ perp(X0,X1,sK1,X2) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_12915,plain,
( para(sK0,sK1,sK1,sK1)
| ~ perp(sK1,sK1,sK1,sK1)
| ~ perp(sK0,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_12914]) ).
tcf(c_12979,plain,
( cyclic(sK3,sK4,sK5,sK6)
| ~ cyclic(sK3,sK5,sK4,sK6) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_13702,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK0,sK1,X2,sK4)
| ~ para(sK0,sK1,X0,X1)
| ~ perp(X0,X1,X2,sK4) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_13703,plain,
( perp(sK0,sK1,sK1,sK4)
| ~ para(sK0,sK1,sK1,sK1)
| ~ perp(sK1,sK1,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_13702]) ).
tcf(c_13712,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK2,sK1,X2,sK5)
| ~ para(sK2,sK1,X0,X1)
| ~ perp(X0,X1,X2,sK5) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_13713,plain,
( perp(sK2,sK1,sK1,sK5)
| ~ para(sK2,sK1,sK1,sK1)
| ~ perp(sK1,sK1,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_13712]) ).
tcf(c_13781,plain,
! [X0: $i] :
( cong(sK1,X0,sK1,sK6)
| ~ midp(sK2,X0,sK6)
| ~ midp(X0,sK2,sK3) ),
inference(superposition,[status(thm)],[c_8089,c_92]) ).
tcf(c_13806,plain,
( cong(sK1,sK1,sK1,sK6)
| ~ midp(sK2,sK1,sK6)
| ~ midp(sK1,sK2,sK3) ),
inference(instantiation,[status(thm)],[c_13781]) ).
tcf(c_15000,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK3,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK3,X2,X1)
| ~ para(X0,X1,X2,sK3) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_15001,plain,
( midp(sK1,sK3,sK1)
| ~ midp(sK1,sK1,sK1)
| ~ para(sK1,sK1,sK1,sK3)
| ~ para(sK1,sK3,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_15000]) ).
tcf(c_15003,plain,
! [X0: $i,X1: $i] :
( midp(sK0,sK1,sK2)
| ~ midp(sK0,X0,X1)
| ~ para(X0,sK2,X1,sK1)
| ~ para(X0,sK1,X1,sK2) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_15004,plain,
( midp(sK0,sK1,sK2)
| ~ midp(sK0,sK1,sK1)
| ~ para(sK1,sK2,sK1,sK1)
| ~ para(sK1,sK1,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_15003]) ).
tcf(c_17116,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK4,X1)
| ~ midp(X2,X0,sK1)
| ~ midp(X0,sK0,X1)
| ~ para(X0,X1,sK1,sK4) ),
inference(superposition,[status(thm)],[c_4109,c_102]) ).
tcf(c_17120,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK5,X1)
| ~ midp(X2,X0,sK1)
| ~ midp(X0,sK2,X1)
| ~ para(X0,X1,sK1,sK5) ),
inference(superposition,[status(thm)],[c_4153,c_102]) ).
tcf(c_17358,plain,
( midp(sK1,sK5,sK1)
| ~ midp(sK1,sK2,sK1)
| ~ midp(sK1,sK1,sK1)
| ~ para(sK1,sK1,sK1,sK5) ),
inference(instantiation,[status(thm)],[c_17120]) ).
tcf(c_17360,plain,
( midp(sK1,sK4,sK1)
| ~ midp(sK1,sK1,sK1)
| ~ midp(sK1,sK0,sK1)
| ~ para(sK1,sK1,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_17116]) ).
tcf(c_17773,plain,
! [X0: $i,X1: $i] :
( para(X1,sK1,X0,sK3)
| ~ para(X0,sK3,X1,sK1) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_17774,plain,
( para(sK1,sK1,sK1,sK3)
| ~ para(sK1,sK3,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_17773]) ).
tcf(c_18431,plain,
coll(sK6,sK3,sK1),
inference(superposition,[status(thm)],[c_10916,c_83]) ).
tcf(c_19111,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X3,sK3,X2,X3)
| ~ para(X3,sK3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_19112,plain,
( perp(sK1,sK3,sK1,sK1)
| ~ para(sK1,sK3,sK1,sK1)
| ~ perp(sK1,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_19111]) ).
tcf(c_19181,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK3,X1)
| ~ perp(X0,X1,X1,sK3) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_19182,plain,
( perp(sK1,sK1,sK3,sK1)
| ~ perp(sK1,sK1,sK1,sK3) ),
inference(instantiation,[status(thm)],[c_19181]) ).
tcf(c_19526,plain,
! [X0: $i] :
( cong(X0,sK4,X0,sK3)
| ~ cong(X0,sK4,sK3,X0) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_19527,plain,
( cong(sK1,sK4,sK1,sK3)
| ~ cong(sK1,sK4,sK3,sK1) ),
inference(instantiation,[status(thm)],[c_19526]) ).
tcf(c_21364,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X1,sK5,sK3)
| ~ coll(X1,sK5,sK3)
| ~ midp(X0,sK5,X2)
| ~ para(X0,X1,X2,sK3) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_21365,plain,
( midp(sK1,sK5,sK3)
| ~ midp(sK1,sK5,sK1)
| ~ coll(sK1,sK5,sK3)
| ~ para(sK1,sK1,sK1,sK3) ),
inference(instantiation,[status(thm)],[c_21364]) ).
tcf(c_21555,plain,
! [X0: $i,X1: $i] :
( cong(sK0,X1,sK0,X1)
| ~ midp(X0,X1,X1)
| ~ perp(sK0,X0,X1,X1) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_21557,plain,
( cong(sK0,sK1,sK0,sK1)
| ~ midp(sK1,sK1,sK1)
| ~ perp(sK0,sK1,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_21555]) ).
tcf(c_22478,plain,
! [X0: $i] :
( cong(X0,sK3,X0,sK4)
| ~ cong(X0,sK4,X0,sK3) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_22479,plain,
( cong(sK1,sK3,sK1,sK4)
| ~ cong(sK1,sK4,sK1,sK3) ),
inference(instantiation,[status(thm)],[c_22478]) ).
tcf(c_23108,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,sK3,sK2)
| ~ cong(X0,X1,sK3,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_6712,c_53,c_52,c_50,c_149,c_152,c_156,c_161,c_194,c_1915,c_1916,c_1923,c_1924,c_1927,c_2050,c_2054,c_2079,c_2245,c_2258,c_2303,c_2309,c_2413,c_2416,c_3272,c_4194,c_4404,c_5536,c_6712,c_7857,c_11756,c_12291,c_12723,c_15004,c_21557]) ).
tcf(c_23120,plain,
! [X0: $i] :
( cong(sK1,X0,sK3,sK2)
| ~ midp(sK1,sK3,X0) ),
inference(superposition,[status(thm)],[c_3075,c_23108]) ).
tcf(c_23140,plain,
( cong(sK1,sK1,sK3,sK2)
| ~ midp(sK1,sK3,sK1) ),
inference(instantiation,[status(thm)],[c_23120]) ).
tcf(c_25782,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_101,c_120]) ).
tcf(c_26966,plain,
( cong(sK3,sK1,sK3,sK2)
| ~ midp(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_50,c_92]) ).
tcf(c_27043,plain,
cong(sK3,sK1,sK3,sK2),
inference(global_subsumption_just,[status(thm)],[c_26966,c_53,c_52,c_50,c_149,c_152,c_156,c_161,c_194,c_1915,c_1916,c_1923,c_1924,c_1927,c_2050,c_2054,c_2079,c_2245,c_2258,c_2303,c_2309,c_2413,c_2416,c_3272,c_4194,c_4404,c_4747,c_5536,c_7857,c_11756,c_12291,c_12723,c_15004,c_21557]) ).
tcf(c_27045,plain,
( midp(sK3,sK1,sK2)
| ~ coll(sK3,sK1,sK2) ),
inference(superposition,[status(thm)],[c_27043,c_77]) ).
tcf(c_27052,plain,
midp(sK3,sK1,sK2),
inference(forward_subsumption_resolution,[status(thm)],[c_27045,c_51]) ).
tcf(c_27067,plain,
midp(sK3,sK2,sK1),
inference(superposition,[status(thm)],[c_27052,c_105]) ).
tcf(c_27080,plain,
! [X0: $i,X1: $i] :
( para(X0,sK3,X1,sK1)
| ~ midp(X0,sK2,X1) ),
inference(superposition,[status(thm)],[c_27067,c_104]) ).
tcf(c_27089,plain,
( para(sK1,sK3,sK1,sK1)
| ~ midp(sK1,sK2,sK1) ),
inference(instantiation,[status(thm)],[c_27080]) ).
tcf(c_31939,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,sK4,sK3,X0)
| ~ cong(X1,X2,sK3,X0)
| ~ cong(X0,sK4,X1,X2) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_31940,plain,
( cong(sK1,sK4,sK3,sK1)
| ~ cong(sK1,sK1,sK3,sK1)
| ~ cong(sK1,sK4,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_31939]) ).
tcf(c_35393,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK4,X0,X1)
| ~ midp(X0,sK4,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_35394,plain,
( cong(sK1,sK4,sK1,sK1)
| ~ midp(sK1,sK4,sK1) ),
inference(instantiation,[status(thm)],[c_35393]) ).
tcf(c_40513,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,sK3,X0,X2)
| ~ midp(X1,sK3,X2)
| ~ perp(X0,X1,sK3,X2) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_40514,plain,
( cong(sK1,sK3,sK1,sK1)
| ~ midp(sK1,sK3,sK1)
| ~ perp(sK1,sK1,sK3,sK1) ),
inference(instantiation,[status(thm)],[c_40513]) ).
tcf(c_44297,plain,
! [X0: $i] :
( midp(X0,sK3,sK5)
| ~ midp(X0,sK5,sK3) ),
inference(instantiation,[status(thm)],[c_5033]) ).
tcf(c_44298,plain,
( midp(sK1,sK3,sK5)
| ~ midp(sK1,sK5,sK3) ),
inference(instantiation,[status(thm)],[c_44297]) ).
tcf(c_44555,plain,
! [X0: $i] :
( cyclic(sK3,sK5,sK4,sK6)
| ~ midp(X0,sK3,sK5)
| ~ cong(X0,sK3,X0,sK6)
| ~ cong(X0,sK3,X0,sK4) ),
inference(instantiation,[status(thm)],[c_25782]) ).
tcf(c_44556,plain,
( cyclic(sK3,sK5,sK4,sK6)
| ~ midp(sK1,sK3,sK5)
| ~ cong(sK1,sK3,sK1,sK6)
| ~ cong(sK1,sK3,sK1,sK4) ),
inference(instantiation,[status(thm)],[c_44555]) ).
tcf(c_45270,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,sK3,X0,sK6)
| ~ cong(X1,X2,X0,sK6)
| ~ cong(X0,sK3,X1,X2) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_45271,plain,
( cong(sK1,sK3,sK1,sK6)
| ~ cong(sK1,sK1,sK1,sK6)
| ~ cong(sK1,sK3,sK1,sK1) ),
inference(instantiation,[status(thm)],[c_45270]) ).
tcf(c_45272,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_45271,c_44556,c_44298,c_40514,c_35394,c_31940,c_27089,c_23140,c_22479,c_21557,c_21365,c_19527,c_19182,c_19112,c_18431,c_17774,c_17360,c_17358,c_15004,c_15001,c_13806,c_13713,c_13703,c_12979,c_12915,c_12723,c_12670,c_12668,c_12291,c_12283,c_12281,c_11756,c_10400,c_10220,c_9131,c_8727,c_8252,c_7857,c_6199,c_5810,c_5797,c_5536,c_5486,c_5392,c_5341,c_5303,c_5293,c_5291,c_4411,c_4404,c_4194,c_4163,c_4144,c_4119,c_3806,c_3272,c_3271,c_2416,c_2413,c_2309,c_2303,c_2301,c_2258,c_2245,c_2207,c_2182,c_2123,c_2079,c_2054,c_2050,c_1946,c_1944,c_1927,c_1924,c_1923,c_1921,c_1920,c_1918,c_1916,c_1915,c_194,c_161,c_156,c_152,c_149,c_49,c_50,c_51,c_52,c_53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO551+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n020.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:23:47 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 27.70/4.86 % SZS status Started for theBenchmark.p
% 27.70/4.86 % SZS status Theorem for theBenchmark.p
% 27.70/4.86
% 27.70/4.86 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 27.70/4.86
% 27.70/4.86 % ------ iProver source info
% 27.70/4.86
% 27.70/4.86 % git: date: 2026-07-19 20:42:38 +0200
% 27.70/4.86 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 27.70/4.86 % git: non_committed_changes: false
% 27.70/4.86
% 27.70/4.86 % ------ Parsing...
% 27.70/4.86 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 27.70/4.86
% 27.70/4.86 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 27.70/4.86
% 27.70/4.86 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 27.70/4.86 % ------ Proving...
% 27.70/4.86 % ------ Problem Properties
% 27.70/4.86
% 27.70/4.86 %
% 27.70/4.86 % clauses 93
% 27.70/4.86 % conjectures 6
% 27.70/4.86 % EPR 60
% 27.70/4.86 % Horn 88
% 27.70/4.86 % unary 6
% 27.70/4.86 % binary 24
% 27.70/4.86 % lits 262
% 27.70/4.86 % lits eq 0
% 27.70/4.86 % fd_pure 0
% 27.70/4.86 % fd_pseudo 0
% 27.70/4.86 % fd_cond 0
% 27.70/4.86 % fd_pseudo_cond 0
% 27.70/4.86 % AC symbols 0
% 27.70/4.86
% 27.70/4.86 % ------ Schedule dynamic 5 is on
% 27.70/4.86
% 27.70/4.86 % ------ no equalities: superposition off
% 27.70/4.86
% 27.70/4.86 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 27.70/4.86
% 27.70/4.86
% 27.70/4.86 % ------
% 27.70/4.86 % Current options:
% 27.70/4.86 % ------
% 27.70/4.86
% 27.70/4.86
% 27.70/4.86 %
% 27.70/4.86
% 27.70/4.86 % ------ Proving...
% 27.70/4.86 %
% 27.70/4.86
% 27.70/4.86 % SZS status Theorem for theBenchmark.p
% 27.70/4.86
% 27.70/4.86 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 27.70/4.87
% 27.70/4.87
%------------------------------------------------------------------------------