%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO606+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 : n008.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:37 PM UTC 2026
% Result : Theorem 121.38s 20.88s
% Output : CNFRefutation 121.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 45
% Syntax : Number of formulae : 745 ( 220 unt; 0 def)
% Number of atoms : 1624 ( 4 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 1616 ( 737 ~; 734 |; 99 &)
% ( 0 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 21 ( 21 usr; 18 con; 0-5 aty)
% Number of variables : 1359 ( 0 sgn1315 !; 44 ?; 574 :)
% 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(f6,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( para(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD6) ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X0,X1,X3,X2) ),
file('/export/starexec/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(f14,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/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/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(f17,axiom,
! [X0,X1,X2,X3,X4] :
( ( cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cyclic(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD17) ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD21) ).
fof(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(f39,axiom,
! [X0,X1,X2,X3,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD39) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f41,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD41) ).
fof(f42,axiom,
! [X0,X1,X2,X3] :
( ( ~ coll(X2,X3,X0)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD42a) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( coll(X2,X3,X1)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
& cyclic(X0,X1,X2,X5)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(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(f47,axiom,
! [X0,X1,X2] :
( cong(X2,X0,X2,X1)
=> eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD46) ).
fof(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(f58,axiom,
! [X0,X1,X2,X3] :
( ( cyclic(X0,X1,X2,X3)
& cong(X0,X3,X1,X3)
& cong(X0,X2,X1,X2) )
=> perp(X2,X0,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD57) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X2,X3)
& midp(X4,X0,X1) )
=> para(X0,X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD63) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4] :
( ( para(X0,X3,X1,X2)
& para(X0,X2,X1,X3)
& midp(X4,X0,X1) )
=> midp(X4,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD64) ).
fof(f67,axiom,
! [X0,X1,X2] :
( para(X0,X1,X0,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD66) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( coll(X0,X1,X2)
& cong(X0,X1,X0,X2) )
=> midp(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD67) ).
fof(f69,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> cong(X0,X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD68) ).
fof(f70,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD69) ).
fof(f85,axiom,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ( perp(X0,X1,X1,X4)
& cong(X4,X2,X4,X3) )
=> ( cong(X1,X2,X1,X5)
& para(X5,X2,X0,X1)
& cong(X4,X2,X4,X5) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX9) ).
fof(f87,axiom,
! [X0,X1,X2,X3] :
? [X4] :
( circle(X3,X0,X1,X2)
=> perp(X4,X0,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX11) ).
fof(f91,axiom,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ( coll(X1,X3,X4)
& perp(X0,X2,X2,X1) )
=> ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX15) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ( coll(X7,X6,X1)
& circle(X1,X6,X7,X17)
& circle(X1,X2,X6,X16)
& coll(X6,X3,X5)
& circle(X1,X2,X5,X15)
& circle(X0,X2,X5,X14)
& coll(X4,X3,X0)
& circle(X0,X3,X4,X13)
& circle(X0,X2,X3,X12)
& circle(X1,X2,X10,X11)
& circle(X0,X2,X8,X9)
& perp(X2,X0,X2,X1) )
=> perp(X7,X6,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL618068) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ( coll(X7,X6,X1)
& circle(X1,X6,X7,X17)
& circle(X1,X2,X6,X16)
& coll(X6,X3,X5)
& circle(X1,X2,X5,X15)
& circle(X0,X2,X5,X14)
& coll(X4,X3,X0)
& circle(X0,X3,X4,X13)
& circle(X0,X2,X3,X12)
& circle(X1,X2,X10,X11)
& circle(X0,X2,X8,X9)
& perp(X2,X0,X2,X1) )
=> perp(X7,X6,X3,X4) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f6]) ).
fof(f105,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f9]) ).
fof(f109,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f10]) ).
fof(f111,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(flattening,[],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(flattening,[],[f113]) ).
fof(f115,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f13]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f120,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f17]) ).
fof(f121,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(flattening,[],[f120]) ).
fof(f125,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(ennf_transformation,[],[f21]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f25]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f130]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f39]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f40]) ).
fof(f150,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f41]) ).
fof(f151,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f42]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f151]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f154,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f156,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(ennf_transformation,[],[f46]) ).
fof(f160,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(flattening,[],[f159]) ).
fof(f161,plain,
! [X0,X1,X2] :
( ~ cong(X2,X0,X2,X1)
| eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(ennf_transformation,[],[f53]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(flattening,[],[f172]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f174]) ).
fof(f178,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f56]) ).
fof(f179,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(flattening,[],[f178]) ).
fof(f180,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f57]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f180]) ).
fof(f182,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(ennf_transformation,[],[f58]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(flattening,[],[f182]) ).
fof(f191,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f192,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f191]) ).
fof(f193,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(ennf_transformation,[],[f65]) ).
fof(f194,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(flattening,[],[f193]) ).
fof(f197,plain,
! [X0,X1,X2] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f198,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f199,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f198]) ).
fof(f200,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f201,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f230,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ perp(X0,X1,X1,X4)
| ~ cong(X4,X2,X4,X3)
| ( cong(X1,X2,X1,X5)
& para(X5,X2,X0,X1)
& cong(X4,X2,X4,X5) ) ),
inference(ennf_transformation,[],[f85]) ).
fof(f231,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ perp(X0,X1,X1,X4)
| ~ cong(X4,X2,X4,X3)
| ( cong(X1,X2,X1,X5)
& para(X5,X2,X0,X1)
& cong(X4,X2,X4,X5) ) ),
inference(flattening,[],[f230]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
? [X4] :
( ~ circle(X3,X0,X1,X2)
| perp(X4,X0,X0,X3) ),
inference(ennf_transformation,[],[f87]) ).
fof(f241,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f242,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(flattening,[],[f241]) ).
fof(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( coll(X7,X6,X1)
& circle(X1,X6,X7,X17)
& circle(X1,X2,X6,X16)
& coll(X6,X3,X5)
& circle(X1,X2,X5,X15)
& circle(X0,X2,X5,X14)
& coll(X4,X3,X0)
& circle(X0,X3,X4,X13)
& circle(X0,X2,X3,X12)
& circle(X1,X2,X10,X11)
& circle(X0,X2,X8,X9)
& perp(X2,X0,X2,X1)
& ~ perp(X7,X6,X3,X4) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( coll(X7,X6,X1)
& circle(X1,X6,X7,X17)
& circle(X1,X2,X6,X16)
& coll(X6,X3,X5)
& circle(X1,X2,X5,X15)
& circle(X0,X2,X5,X14)
& coll(X4,X3,X0)
& circle(X0,X3,X4,X13)
& circle(X0,X2,X3,X12)
& circle(X1,X2,X10,X11)
& circle(X0,X2,X8,X9)
& perp(X2,X0,X2,X1)
& ~ perp(X7,X6,X3,X4) ),
inference(flattening,[],[f249]) ).
fof(f260,plain,
! [X0,X1,X2,X3,X4] :
( ~ perp(X0,X1,X1,X4)
| ~ cong(X4,X2,X4,X3)
| ( cong(X1,X2,X1,sK8(X0,X1,X2,X3,X4))
& para(sK8(X0,X1,X2,X3,X4),X2,X0,X1)
& cong(X4,X2,X4,sK8(X0,X1,X2,X3,X4)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X5,sK8(X0,X1,X2,X3,X4))],[f231]) ).
fof(f262,plain,
! [X0,X1,X2,X3] :
( ~ circle(X3,X0,X1,X2)
| perp(sK11(X0,X1,X2,X3),X0,X0,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X4,sK11(X0,X1,X2,X3))],[f234]) ).
fof(f266,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(sK16(X0,X1,X2,X3,X4),X0,X3,X4)
& coll(sK16(X0,X1,X2,X3,X4),X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X5,sK16(X0,X1,X2,X3,X4))],[f242]) ).
fof(f270,plain,
( coll(sK27,sK26,sK21)
& circle(sK21,sK26,sK27,sK37)
& circle(sK21,sK22,sK26,sK36)
& coll(sK26,sK23,sK25)
& circle(sK21,sK22,sK25,sK35)
& circle(sK20,sK22,sK25,sK34)
& coll(sK24,sK23,sK20)
& circle(sK20,sK23,sK24,sK33)
& circle(sK20,sK22,sK23,sK32)
& circle(sK21,sK22,sK30,sK31)
& circle(sK20,sK22,sK28,sK29)
& perp(sK22,sK20,sK22,sK21)
& ~ perp(sK27,sK26,sK23,sK24) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25),skolemize(X6,sK26),skolemize(X7,sK27),skolemize(X8,sK28),skolemize(X9,sK29),skolemize(X10,sK30),skolemize(X11,sK31),skolemize(X12,sK32),skolemize(X13,sK33),skolemize(X14,sK34),skolemize(X15,sK35),skolemize(X16,sK36),skolemize(X17,sK37)],[f250]) ).
fof(f271,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f273,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f274,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f275,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f276,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f105]) ).
fof(f277,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f106]) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f279,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f280,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f111]) ).
fof(f281,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f282,plain,
! [X2,X3,X0,X1] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f283,plain,
! [X2,X3,X0,X1,X4] :
( ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f116]) ).
fof(f284,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f285,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f118]) ).
fof(f286,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f119]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f121]) ).
fof(f291,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(cnf_transformation,[],[f125]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f294,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f131]) ).
fof(f309,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f148]) ).
fof(f310,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f149]) ).
fof(f311,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f150]) ).
fof(f312,plain,
! [X2,X3,X0,X1] :
( coll(X2,X3,X0)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f152]) ).
fof(f313,plain,
! [X2,X3,X0,X1] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f314,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f156]) ).
fof(f315,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f316,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(cnf_transformation,[],[f160]) ).
fof(f317,plain,
! [X2,X0,X1] :
( ~ cong(X2,X0,X2,X1)
| eqangle(X2,X0,X0,X1,X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f161]) ).
fof(f323,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f173]) ).
fof(f324,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f326,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f179]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f181]) ).
fof(f328,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(cnf_transformation,[],[f183]) ).
fof(f334,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f192]) ).
fof(f335,plain,
! [X2,X3,X0,X1,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(cnf_transformation,[],[f194]) ).
fof(f337,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f197]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f199]) ).
fof(f339,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f200]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f201]) ).
fof(f363,plain,
! [X2,X3,X0,X1,X4] :
( ~ perp(X0,X1,X1,X4)
| ~ cong(X4,X2,X4,X3)
| cong(X1,X2,X1,sK8(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f260]) ).
fof(f370,plain,
! [X2,X3,X0,X1] :
( ~ circle(X3,X0,X1,X2)
| perp(sK11(X0,X1,X2,X3),X0,X0,X3) ),
inference(cnf_transformation,[],[f262]) ).
fof(f378,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| coll(sK16(X0,X1,X2,X3,X4),X3,X4) ),
inference(cnf_transformation,[],[f266]) ).
fof(f384,plain,
coll(sK27,sK26,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f385,plain,
circle(sK21,sK26,sK27,sK37),
inference(cnf_transformation,[],[f270]) ).
fof(f387,plain,
coll(sK26,sK23,sK25),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
coll(sK24,sK23,sK20),
inference(cnf_transformation,[],[f270]) ).
fof(f392,plain,
circle(sK20,sK22,sK23,sK32),
inference(cnf_transformation,[],[f270]) ).
fof(f395,plain,
perp(sK22,sK20,sK22,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f396,plain,
~ perp(sK27,sK26,sK23,sK24),
inference(cnf_transformation,[],[f270]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X0,X1,X4,X5)
| ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( circle(X0,X1,X3,X2)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X3,X2,X4)
| ~ cong(X0,X1,X0,X4)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X2,X3,X0,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X0,X1,X4,X5)
| ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X2,X3) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( coll(X0,X3,X1)
| cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X0,X3)
| ~ coll(X0,X3,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X1,X2,X4,X5)
| ~ cyclic(X1,X2,X0,X5)
| ~ cyclic(X1,X2,X0,X4)
| ~ cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X4,X3,X5) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X3,X2,X4)
| ~ midp(X3,X1,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X1,X4,X3)
| ~ midp(X0,X4,X2)
| ~ coll(X1,X4,X3)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,X1,X1,X2,X1,X2,X0,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X3,X1,X3)
| ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X1,X2,X2,X3)
| ~ coll(X0,X1,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f324]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X0,X2,X0,X3)
| ~ midp(X1,X2,X3)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X2,X1,X3)
| ~ cong(X0,X3,X2,X3)
| ~ cong(X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X1,X0,X0,X3)
| ~ cyclic(X0,X2,X1,X3)
| ~ cong(X0,X3,X2,X3)
| ~ cong(X0,X1,X2,X1) ),
inference(cnf_transformation,[],[f328]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X1,X3,X2,X4)
| ~ midp(X0,X3,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X4,X1,X3)
| ~ midp(X4,X0,X2)
| ~ para(X0,X3,X2,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(X1,X3,X1,sK8(X0,X1,X3,X4,X2))
| ~ cong(X2,X3,X2,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK11(X1,X2,X3,X0),X1,X1,X0)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( coll(sK16(X0,X2,X1,X3,X4),X3,X4)
| ~ coll(X2,X3,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_162,negated_conjecture,
~ perp(sK27,sK26,sK23,sK24),
inference(cnf_transformation,[],[f396]) ).
tcf(c_163,negated_conjecture,
perp(sK22,sK20,sK22,sK21),
inference(cnf_transformation,[],[f395]) ).
tcf(c_166,negated_conjecture,
circle(sK20,sK22,sK23,sK32),
inference(cnf_transformation,[],[f392]) ).
tcf(c_168,negated_conjecture,
coll(sK24,sK23,sK20),
inference(cnf_transformation,[],[f390]) ).
tcf(c_171,negated_conjecture,
coll(sK26,sK23,sK25),
inference(cnf_transformation,[],[f387]) ).
tcf(c_173,negated_conjecture,
circle(sK21,sK26,sK27,sK37),
inference(cnf_transformation,[],[f385]) ).
tcf(c_174,negated_conjecture,
coll(sK27,sK26,sK21),
inference(cnf_transformation,[],[f384]) ).
tcf(c_180,plain,
( midp(sK22,sK22,sK22)
| ~ coll(sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_183,plain,
( eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_189,plain,
( perp(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_238,plain,
( cong(sK22,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK22,sK22)
| ~ eqangle(sK22,sK22,sK22,sK22,sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_2871,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK11(X1,X2,X3,X0),X1,X1,X0)
| ( X3 != sK37 )
| ( X2 != sK27 )
| ( X1 != sK26 )
| ( X0 != sK21 ) ),
inference(resolution_lifted,[status(thm)],[c_148,c_173]) ).
tcf(c_2872,plain,
perp(sK11(sK26,sK27,sK37,sK21),sK26,sK26,sK21),
inference(unflattening,[status(thm)],[c_2871]) ).
tcf(c_6484,negated_conjecture,
coll(sK27,sK26,sK21),
inference(demodulation,[status(thm)],[c_174]) ).
tcf(c_6485,negated_conjecture,
circle(sK21,sK26,sK27,sK37),
inference(demodulation,[status(thm)],[c_173]) ).
tcf(c_6487,negated_conjecture,
coll(sK26,sK23,sK25),
inference(demodulation,[status(thm)],[c_171]) ).
tcf(c_6490,negated_conjecture,
coll(sK24,sK23,sK20),
inference(demodulation,[status(thm)],[c_168]) ).
tcf(c_6492,negated_conjecture,
circle(sK20,sK22,sK23,sK32),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_6495,negated_conjecture,
perp(sK22,sK20,sK22,sK21),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_8030,plain,
coll(sK24,sK20,sK23),
inference(superposition,[status(thm)],[c_6490,c_49]) ).
tcf(c_8031,plain,
coll(sK26,sK25,sK23),
inference(superposition,[status(thm)],[c_6487,c_49]) ).
tcf(c_8032,plain,
coll(sK27,sK21,sK26),
inference(superposition,[status(thm)],[c_6484,c_49]) ).
tcf(c_8041,plain,
coll(sK23,sK26,sK25),
inference(superposition,[status(thm)],[c_6487,c_50]) ).
tcf(c_8043,plain,
coll(sK20,sK24,sK23),
inference(superposition,[status(thm)],[c_8030,c_50]) ).
tcf(c_8044,plain,
coll(sK25,sK26,sK23),
inference(superposition,[status(thm)],[c_8031,c_50]) ).
tcf(c_8045,plain,
coll(sK21,sK27,sK26),
inference(superposition,[status(thm)],[c_8032,c_50]) ).
tcf(c_8049,plain,
coll(sK23,sK25,sK26),
inference(superposition,[status(thm)],[c_8041,c_49]) ).
tcf(c_8098,plain,
perp(sK22,sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_6495,c_55]) ).
tcf(c_8104,plain,
perp(sK22,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_6495,c_56]) ).
tcf(c_8105,plain,
perp(sK21,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_8098,c_56]) ).
tcf(c_8107,plain,
perp(sK22,sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_8104,c_55]) ).
tcf(c_8130,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X2,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_117,c_71]) ).
tcf(c_8146,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_117,c_72]) ).
tcf(c_8147,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X2,X0,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_8130,c_72]) ).
tcf(c_8165,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X2,X0,X1,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_8147,c_71]) ).
tcf(c_8180,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X1,X0,X2,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_8165,c_72]) ).
tcf(c_8206,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK23,X0) ),
inference(superposition,[status(thm)],[c_6490,c_51]) ).
tcf(c_8207,plain,
! [X0: $i] :
( coll(sK25,X0,sK26)
| ~ coll(sK26,sK23,X0) ),
inference(superposition,[status(thm)],[c_6487,c_51]) ).
tcf(c_8208,plain,
! [X0: $i] :
( coll(sK21,X0,sK27)
| ~ coll(sK27,sK26,X0) ),
inference(superposition,[status(thm)],[c_6484,c_51]) ).
tcf(c_8209,plain,
! [X0: $i] :
( coll(sK23,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_8030,c_51]) ).
tcf(c_8210,plain,
! [X0: $i] :
( coll(sK23,X0,sK26)
| ~ coll(sK26,sK25,X0) ),
inference(superposition,[status(thm)],[c_8031,c_51]) ).
tcf(c_8211,plain,
! [X0: $i] :
( coll(sK26,X0,sK27)
| ~ coll(sK27,sK21,X0) ),
inference(superposition,[status(thm)],[c_8032,c_51]) ).
tcf(c_8215,plain,
! [X0: $i] :
( coll(sK23,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_8043,c_51]) ).
tcf(c_8216,plain,
! [X0: $i] :
( coll(sK23,X0,sK25)
| ~ coll(sK25,sK26,X0) ),
inference(superposition,[status(thm)],[c_8044,c_51]) ).
tcf(c_8217,plain,
! [X0: $i] :
( coll(sK26,X0,sK21)
| ~ coll(sK21,sK27,X0) ),
inference(superposition,[status(thm)],[c_8045,c_51]) ).
tcf(c_8219,plain,
! [X0: $i] :
( coll(sK26,X0,sK23)
| ~ coll(sK23,sK25,X0) ),
inference(superposition,[status(thm)],[c_8049,c_51]) ).
tcf(c_8282,plain,
coll(sK20,sK20,sK24),
inference(superposition,[status(thm)],[c_6490,c_8206]) ).
tcf(c_8299,plain,
! [X0: $i] :
( coll(sK24,X0,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(superposition,[status(thm)],[c_8282,c_51]) ).
tcf(c_8321,plain,
coll(sK25,sK25,sK26),
inference(superposition,[status(thm)],[c_6487,c_8207]) ).
tcf(c_8322,plain,
! [X0: $i] :
( coll(sK26,X0,sK25)
| ~ coll(sK25,sK25,X0) ),
inference(superposition,[status(thm)],[c_8321,c_51]) ).
tcf(c_8332,plain,
coll(sK21,sK21,sK27),
inference(superposition,[status(thm)],[c_6484,c_8208]) ).
tcf(c_8333,plain,
! [X0: $i] :
( coll(sK27,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_8332,c_51]) ).
tcf(c_8335,plain,
coll(sK21,sK27,sK21),
inference(superposition,[status(thm)],[c_8332,c_49]) ).
tcf(c_8345,plain,
! [X0: $i] :
( coll(sK21,X0,sK21)
| ~ coll(sK21,sK27,X0) ),
inference(superposition,[status(thm)],[c_8335,c_51]) ).
tcf(c_8355,plain,
coll(sK23,sK23,sK24),
inference(superposition,[status(thm)],[c_8030,c_8209]) ).
tcf(c_8357,plain,
! [X0: $i] :
( coll(sK24,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_8355,c_51]) ).
tcf(c_8367,plain,
coll(sK23,sK23,sK26),
inference(superposition,[status(thm)],[c_8031,c_8210]) ).
tcf(c_8372,plain,
coll(sK26,sK26,sK27),
inference(superposition,[status(thm)],[c_8032,c_8211]) ).
tcf(c_8410,plain,
! [X0: $i] :
( coll(sK26,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_8367,c_51]) ).
tcf(c_8412,plain,
coll(sK23,sK26,sK23),
inference(superposition,[status(thm)],[c_8367,c_49]) ).
tcf(c_8416,plain,
! [X0: $i] :
( coll(sK27,X0,sK26)
| ~ coll(sK26,sK26,X0) ),
inference(superposition,[status(thm)],[c_8372,c_51]) ).
tcf(c_8418,plain,
coll(sK26,sK27,sK26),
inference(superposition,[status(thm)],[c_8372,c_49]) ).
tcf(c_8466,plain,
coll(sK23,sK23,sK20),
inference(superposition,[status(thm)],[c_8043,c_8215]) ).
tcf(c_8472,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X2,X0,X2,X0)
| ~ cyclic(X0,X1,X2,X2) ),
inference(superposition,[status(thm)],[c_89,c_87]) ).
tcf(c_8475,plain,
( para(sK22,sK22,sK22,sK22)
| ~ cyclic(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_8472]) ).
tcf(c_8503,plain,
! [X0: $i] :
( coll(sK23,X0,sK23)
| ~ coll(sK23,sK26,X0) ),
inference(superposition,[status(thm)],[c_8412,c_51]) ).
tcf(c_8510,plain,
! [X0: $i] :
( coll(sK26,X0,sK26)
| ~ coll(sK26,sK27,X0) ),
inference(superposition,[status(thm)],[c_8418,c_51]) ).
tcf(c_8533,plain,
coll(sK26,sK26,sK25),
inference(superposition,[status(thm)],[c_8321,c_8322]) ).
tcf(c_8537,plain,
coll(sK26,sK25,sK26),
inference(superposition,[status(thm)],[c_8533,c_49]) ).
tcf(c_8578,plain,
coll(sK23,sK23,sK25),
inference(superposition,[status(thm)],[c_8044,c_8216]) ).
tcf(c_8627,plain,
! [X0: $i] :
( cong(sK21,X0,sK22,X0)
| ~ midp(X0,sK21,sK20) ),
inference(superposition,[status(thm)],[c_8105,c_101]) ).
tcf(c_8654,plain,
( perp(sK26,sK27,sK27,sK37)
| ~ coll(sK21,sK26,sK37) ),
inference(superposition,[status(thm)],[c_6485,c_102]) ).
tcf(c_8677,plain,
! [X0: $i] :
( coll(sK20,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_8466,c_51]) ).
tcf(c_8839,plain,
( perp(sK27,sK37,sK26,sK27)
| ~ coll(sK21,sK26,sK37) ),
inference(superposition,[status(thm)],[c_8654,c_56]) ).
tcf(c_8865,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_6495,c_104]) ).
tcf(c_8874,plain,
( cong(sK22,sK21,sK22,sK22)
| ~ midp(sK20,sK21,sK22) ),
inference(superposition,[status(thm)],[c_8098,c_104]) ).
tcf(c_8875,plain,
( cong(sK22,sK22,sK22,sK20)
| ~ midp(sK21,sK22,sK20) ),
inference(superposition,[status(thm)],[c_8104,c_104]) ).
tcf(c_8876,plain,
( cong(sK21,sK22,sK21,sK20)
| ~ midp(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_8105,c_104]) ).
tcf(c_8960,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ perp(sK22,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6495,c_57]) ).
tcf(c_8968,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK27,X0,X1)
| ~ coll(sK21,sK26,sK37)
| ~ perp(sK27,sK37,X0,X1) ),
inference(superposition,[status(thm)],[c_8654,c_57]) ).
tcf(c_8970,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK21,X0,X1)
| ~ perp(sK22,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_8104,c_57]) ).
tcf(c_9100,plain,
( midp(sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK22,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_116]) ).
tcf(c_9101,plain,
( cong(sK22,sK21,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_72]) ).
tcf(c_9114,plain,
para(sK22,sK20,sK22,sK20),
inference(superposition,[status(thm)],[c_8104,c_8960]) ).
tcf(c_9115,plain,
para(sK22,sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_8107,c_8960]) ).
tcf(c_9120,plain,
coll(sK22,sK20,sK20),
inference(superposition,[status(thm)],[c_9114,c_115]) ).
tcf(c_9123,plain,
para(sK20,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_9115,c_53]) ).
tcf(c_9240,plain,
! [X0: $i] :
( circle(sK22,sK22,X0,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8865,c_60]) ).
tcf(c_9292,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK22,X0,X1)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_8865,c_73]) ).
tcf(c_9404,plain,
! [X0: $i] :
( coll(sK26,X0,sK26)
| ~ coll(sK26,sK25,X0) ),
inference(superposition,[status(thm)],[c_8537,c_51]) ).
tcf(c_9600,plain,
coll(sK26,sK26,sK23),
inference(superposition,[status(thm)],[c_8049,c_8219]) ).
tcf(c_9775,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK21,X0,X1)
| ~ midp(sK20,sK21,sK22)
| ~ cong(sK22,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_8874,c_73]) ).
tcf(c_9776,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK20,sK21,sK22) ),
inference(superposition,[status(thm)],[c_8874,c_72]) ).
tcf(c_9794,plain,
! [X0: $i] :
( circle(sK22,sK22,X0,sK20)
| ~ midp(sK21,sK22,sK20)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8875,c_60]) ).
tcf(c_9820,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK21,X0,X1)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_9101,c_73]) ).
tcf(c_9947,plain,
coll(sK20,sK22,sK20),
inference(superposition,[status(thm)],[c_9120,c_50]) ).
tcf(c_9968,plain,
para(sK22,sK21,sK22,sK21),
inference(superposition,[status(thm)],[c_6495,c_8970]) ).
tcf(c_9969,plain,
para(sK22,sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_8098,c_8970]) ).
tcf(c_9974,plain,
coll(sK22,sK21,sK21),
inference(superposition,[status(thm)],[c_9968,c_115]) ).
tcf(c_9975,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_9974,c_51]) ).
tcf(c_9976,plain,
coll(sK21,sK22,sK21),
inference(superposition,[status(thm)],[c_9974,c_50]) ).
tcf(c_9983,plain,
para(sK21,sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_9969,c_53]) ).
tcf(c_10414,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ perp(sK22,sK20,sK21,sK22)
| ~ perp(sK21,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_10704,plain,
! [X0: $i] :
( midp(sK21,X0,sK21)
| ~ midp(sK22,X0,sK22)
| ~ coll(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_9968,c_94]) ).
tcf(c_10705,plain,
! [X0: $i] :
( midp(sK21,X0,sK22)
| ~ midp(sK22,X0,sK21)
| ~ coll(sK21,X0,sK22) ),
inference(superposition,[status(thm)],[c_9969,c_94]) ).
tcf(c_10718,plain,
( midp(sK21,sK22,sK22)
| ~ midp(sK22,sK22,sK21)
| ~ coll(sK21,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_10705]) ).
tcf(c_10719,plain,
( midp(sK21,sK22,sK21)
| ~ midp(sK22,sK22,sK22)
| ~ coll(sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_10704]) ).
tcf(c_10743,plain,
coll(sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_9947,c_49]) ).
tcf(c_11359,plain,
coll(sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_9976,c_49]) ).
tcf(c_11379,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(superposition,[status(thm)],[c_10743,c_51]) ).
tcf(c_11382,plain,
coll(sK24,sK22,sK20),
inference(superposition,[status(thm)],[c_10743,c_8299]) ).
tcf(c_11385,plain,
( coll(sK22,sK22,sK20)
| ~ coll(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_11379]) ).
tcf(c_11516,plain,
( para(sK26,sK27,sK26,sK27)
| ~ coll(sK21,sK26,sK37) ),
inference(superposition,[status(thm)],[c_8839,c_8968]) ).
tcf(c_11533,plain,
( circle(sK22,sK22,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_9240]) ).
tcf(c_11720,plain,
! [X0: $i] :
( coll(sK22,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_11359,c_51]) ).
tcf(c_11723,plain,
coll(sK27,sK22,sK21),
inference(superposition,[status(thm)],[c_11359,c_8333]) ).
tcf(c_11726,plain,
( coll(sK22,sK22,sK21)
| ~ coll(sK21,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_11720]) ).
tcf(c_11729,plain,
coll(sK24,sK20,sK22),
inference(superposition,[status(thm)],[c_11382,c_49]) ).
tcf(c_11741,plain,
coll(sK27,sK21,sK22),
inference(superposition,[status(thm)],[c_11723,c_49]) ).
tcf(c_11749,plain,
( perp(sK22,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK22,sK22,sK21) ),
inference(superposition,[status(thm)],[c_11533,c_102]) ).
tcf(c_11760,plain,
! [X0: $i] :
( cong(sK22,sK22,sK22,X0)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,X0,sK21) ),
inference(superposition,[status(thm)],[c_8146,c_9292]) ).
tcf(c_11766,plain,
! [X0: $i] :
( cong(sK22,sK22,X0,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK21,sK22,X0) ),
inference(superposition,[status(thm)],[c_8180,c_9292]) ).
tcf(c_11773,plain,
( cong(sK22,sK22,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_9101,c_9292]) ).
tcf(c_12272,plain,
coll(sK20,sK24,sK22),
inference(superposition,[status(thm)],[c_11729,c_50]) ).
tcf(c_12296,plain,
coll(sK21,sK27,sK22),
inference(superposition,[status(thm)],[c_11741,c_50]) ).
tcf(c_12298,plain,
coll(sK26,sK22,sK27),
inference(superposition,[status(thm)],[c_11741,c_8211]) ).
tcf(c_12594,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK22,sK22)
| ~ para(sK22,sK21,sK22,sK21) ),
inference(superposition,[status(thm)],[c_9968,c_113]) ).
tcf(c_12599,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK22,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12594,c_9968]) ).
tcf(c_12609,plain,
( midp(sK22,sK21,sK21)
| ~ midp(sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_12599]) ).
tcf(c_12733,plain,
! [X0: $i,X1: $i] :
( cong(sK26,X0,sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,X0,X1,sK21))
| ~ cong(sK21,X0,sK21,X1)
| ~ perp(sK11(sK26,sK27,sK37,sK21),sK26,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_12744,plain,
( cong(sK26,sK22,sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,sK22,sK22,sK21))
| ~ cong(sK21,sK22,sK21,sK22)
| ~ perp(sK11(sK26,sK27,sK37,sK21),sK26,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_12733]) ).
tcf(c_12765,plain,
coll(sK23,sK22,sK20),
inference(superposition,[status(thm)],[c_12272,c_8215]) ).
tcf(c_13157,plain,
coll(sK26,sK27,sK22),
inference(superposition,[status(thm)],[c_12298,c_49]) ).
tcf(c_13369,plain,
coll(sK26,sK22,sK21),
inference(superposition,[status(thm)],[c_12296,c_8217]) ).
tcf(c_13388,plain,
coll(sK23,sK20,sK22),
inference(superposition,[status(thm)],[c_12765,c_49]) ).
tcf(c_13422,plain,
para(sK20,sK22,sK20,sK22),
inference(superposition,[status(thm)],[c_9123,c_52]) ).
tcf(c_13438,plain,
! [X0: $i] :
( midp(sK22,X0,sK21)
| ~ midp(sK21,X0,sK22)
| ~ coll(sK22,X0,sK21) ),
inference(superposition,[status(thm)],[c_9983,c_94]) ).
tcf(c_13455,plain,
( midp(sK22,sK22,sK21)
| ~ midp(sK21,sK22,sK22)
| ~ coll(sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_13438]) ).
tcf(c_13468,plain,
coll(sK24,sK26,sK23),
inference(superposition,[status(thm)],[c_8367,c_8357]) ).
tcf(c_13470,plain,
coll(sK24,sK25,sK23),
inference(superposition,[status(thm)],[c_8578,c_8357]) ).
tcf(c_13476,plain,
coll(sK26,sK24,sK23),
inference(superposition,[status(thm)],[c_13468,c_50]) ).
tcf(c_13477,plain,
coll(sK24,sK23,sK26),
inference(superposition,[status(thm)],[c_13468,c_49]) ).
tcf(c_13492,plain,
coll(sK26,sK20,sK23),
inference(superposition,[status(thm)],[c_8466,c_8410]) ).
tcf(c_13504,plain,
coll(sK27,sK25,sK26),
inference(superposition,[status(thm)],[c_8533,c_8416]) ).
tcf(c_13506,plain,
coll(sK27,sK23,sK26),
inference(superposition,[status(thm)],[c_9600,c_8416]) ).
tcf(c_13529,plain,
coll(sK27,sK26,sK25),
inference(superposition,[status(thm)],[c_13504,c_49]) ).
tcf(c_13667,plain,
! [X0: $i] :
( coll(sK20,sK24,X0)
| ~ coll(sK20,X0,sK24) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_13787,plain,
! [X0: $i] :
( coll(sK22,X0,sK26)
| ~ coll(sK26,sK27,X0) ),
inference(superposition,[status(thm)],[c_13157,c_51]) ).
tcf(c_13793,plain,
( coll(sK22,sK22,sK26)
| ~ coll(sK26,sK27,sK22) ),
inference(instantiation,[status(thm)],[c_13787]) ).
tcf(c_14795,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X0,sK21,X1)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X1)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8865,c_61]) ).
tcf(c_14804,plain,
! [X0: $i,X1: $i] :
( cyclic(sK21,X0,sK22,X1)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK21,sK22,X1)
| ~ cong(sK22,sK21,sK22,X0) ),
inference(superposition,[status(thm)],[c_9101,c_61]) ).
tcf(c_14806,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X0,sK20,X1)
| ~ midp(sK21,sK22,sK20)
| ~ cong(sK22,sK22,sK22,X1)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8875,c_61]) ).
tcf(c_14963,plain,
coll(sK22,sK26,sK21),
inference(superposition,[status(thm)],[c_13369,c_50]) ).
tcf(c_14988,plain,
coll(sK20,sK23,sK22),
inference(superposition,[status(thm)],[c_13388,c_50]) ).
tcf(c_15837,plain,
coll(sK24,sK23,sK25),
inference(superposition,[status(thm)],[c_13470,c_49]) ).
tcf(c_15842,plain,
coll(sK26,sK23,sK24),
inference(superposition,[status(thm)],[c_13476,c_49]) ).
tcf(c_15849,plain,
coll(sK20,sK26,sK24),
inference(superposition,[status(thm)],[c_13477,c_8206]) ).
tcf(c_15855,plain,
coll(sK26,sK23,sK20),
inference(superposition,[status(thm)],[c_13492,c_49]) ).
tcf(c_15861,plain,
coll(sK20,sK24,sK26),
inference(superposition,[status(thm)],[c_15849,c_49]) ).
tcf(c_16021,plain,
! [X0: $i] :
( cyclic(sK22,sK21,sK21,X0)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8865,c_14795]) ).
tcf(c_16071,plain,
( cyclic(sK22,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_16021]) ).
tcf(c_16400,plain,
coll(sK27,sK26,sK23),
inference(superposition,[status(thm)],[c_13506,c_49]) ).
tcf(c_16412,plain,
coll(sK21,sK25,sK27),
inference(superposition,[status(thm)],[c_13529,c_8208]) ).
tcf(c_16459,plain,
coll(sK21,sK27,sK25),
inference(superposition,[status(thm)],[c_16412,c_49]) ).
tcf(c_16468,plain,
! [X0: $i] :
( coll(sK26,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_15861,c_51]) ).
tcf(c_16486,plain,
coll(sK26,sK25,sK21),
inference(superposition,[status(thm)],[c_16459,c_8217]) ).
tcf(c_16842,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK26,X0) ),
inference(superposition,[status(thm)],[c_14963,c_51]) ).
tcf(c_16847,plain,
( coll(sK21,sK22,sK22)
| ~ coll(sK22,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_16842]) ).
tcf(c_17197,plain,
! [X0: $i] :
( cong(sK21,X0,X0,sK22)
| ~ midp(X0,sK21,sK20) ),
inference(superposition,[status(thm)],[c_8627,c_71]) ).
tcf(c_17233,plain,
( midp(sK21,sK22,sK20)
| ~ midp(sK22,sK22,sK20)
| ~ coll(sK21,sK22,sK20) ),
inference(superposition,[status(thm)],[c_8876,c_116]) ).
tcf(c_17443,plain,
coll(sK26,sK22,sK26),
inference(superposition,[status(thm)],[c_13157,c_8510]) ).
tcf(c_18101,plain,
coll(sK20,sK25,sK24),
inference(superposition,[status(thm)],[c_15837,c_8206]) ).
tcf(c_18139,plain,
! [X0: $i] :
( coll(sK24,X0,sK20)
| ~ coll(sK20,sK25,X0) ),
inference(superposition,[status(thm)],[c_18101,c_51]) ).
tcf(c_19099,plain,
! [X0: $i] :
( coll(sK24,X0,sK26)
| ~ coll(sK26,sK23,X0) ),
inference(superposition,[status(thm)],[c_15842,c_51]) ).
tcf(c_19139,plain,
coll(sK25,sK20,sK26),
inference(superposition,[status(thm)],[c_15855,c_8207]) ).
tcf(c_19166,plain,
coll(sK20,sK25,sK26),
inference(superposition,[status(thm)],[c_19139,c_50]) ).
tcf(c_19167,plain,
coll(sK25,sK26,sK20),
inference(superposition,[status(thm)],[c_19139,c_49]) ).
tcf(c_19538,plain,
coll(sK24,sK26,sK20),
inference(superposition,[status(thm)],[c_19166,c_18139]) ).
tcf(c_19543,plain,
coll(sK26,sK25,sK20),
inference(superposition,[status(thm)],[c_19167,c_50]) ).
tcf(c_20266,plain,
coll(sK21,sK23,sK27),
inference(superposition,[status(thm)],[c_16400,c_8208]) ).
tcf(c_20296,plain,
coll(sK21,sK27,sK23),
inference(superposition,[status(thm)],[c_20266,c_49]) ).
tcf(c_20384,plain,
coll(sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_20296,c_8345]) ).
tcf(c_20600,plain,
! [X0: $i] :
( coll(sK26,sK23,X0)
| ~ coll(sK26,X0,sK23) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_20602,plain,
! [X0: $i,X1: $i] :
( coll(sK24,X1,X0)
| ~ coll(sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_20609,plain,
! [X0: $i,X1: $i] :
( coll(X0,sK26,X1)
| ~ coll(X0,X1,sK26) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_20610,plain,
( coll(sK22,sK26,sK22)
| ~ coll(sK22,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_20609]) ).
tcf(c_20698,plain,
! [X0: $i,X1: $i] :
( coll(sK26,X0,X1)
| ~ coll(X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_20699,plain,
( coll(sK26,sK22,sK22)
| ~ coll(sK22,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_20698]) ).
tcf(c_20813,plain,
coll(sK23,sK21,sK26),
inference(superposition,[status(thm)],[c_16486,c_8210]) ).
tcf(c_20848,plain,
coll(sK22,sK26,sK26),
inference(superposition,[status(thm)],[c_17443,c_50]) ).
tcf(c_20854,plain,
coll(sK23,sK26,sK21),
inference(superposition,[status(thm)],[c_20813,c_49]) ).
tcf(c_21564,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK26,X0) ),
inference(superposition,[status(thm)],[c_19538,c_51]) ).
tcf(c_21691,plain,
! [X0: $i] :
( midp(X0,sK27,sK27)
| ~ coll(sK21,sK26,sK37)
| ~ midp(X0,sK26,sK26)
| ~ para(sK26,sK27,sK26,sK27) ),
inference(superposition,[status(thm)],[c_11516,c_113]) ).
tcf(c_21707,plain,
( midp(sK22,sK27,sK27)
| ~ midp(sK22,sK26,sK26)
| ~ coll(sK21,sK26,sK37)
| ~ para(sK26,sK27,sK26,sK27) ),
inference(instantiation,[status(thm)],[c_21691]) ).
tcf(c_22032,plain,
coll(sK21,sK21,sK23),
inference(superposition,[status(thm)],[c_20384,c_49]) ).
tcf(c_22686,plain,
( midp(sK21,sK21,sK22)
| ~ midp(sK22,sK21,sK21) ),
inference(superposition,[status(thm)],[c_11359,c_10705]) ).
tcf(c_22763,plain,
coll(sK23,sK21,sK23),
inference(superposition,[status(thm)],[c_20854,c_8503]) ).
tcf(c_24087,plain,
( perp(sK27,sK26,sK23,sK24)
| ~ perp(sK23,sK24,sK27,sK26) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_25666,plain,
coll(sK26,sK20,sK26),
inference(superposition,[status(thm)],[c_19543,c_9404]) ).
tcf(c_25751,plain,
coll(sK23,sK23,sK21),
inference(superposition,[status(thm)],[c_22763,c_49]) ).
tcf(c_27224,plain,
coll(sK26,sK26,sK20),
inference(superposition,[status(thm)],[c_25666,c_49]) ).
tcf(c_27748,plain,
coll(sK20,sK21,sK23),
inference(superposition,[status(thm)],[c_25751,c_8677]) ).
tcf(c_28150,plain,
( perp(sK22,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_11749,c_11359,c_11726,c_11749]) ).
tcf(c_28165,plain,
( para(sK22,sK20,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_28150,c_8960]) ).
tcf(c_28339,plain,
! [X0: $i,X1: $i] :
( perp(sK22,sK20,X0,X1)
| ~ midp(sK20,sK22,sK21)
| ~ perp(sK21,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_28165,c_58]) ).
tcf(c_28341,plain,
( para(sK21,sK21,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_28165,c_53]) ).
tcf(c_28415,plain,
! [X0: $i] :
( midp(sK21,X0,sK20)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK21,X0,sK22)
| ~ coll(sK21,X0,sK20) ),
inference(superposition,[status(thm)],[c_28341,c_94]) ).
tcf(c_28438,plain,
( midp(sK21,sK22,sK20)
| ~ midp(sK21,sK22,sK22)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK21,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_28415]) ).
tcf(c_28632,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X1,sK21,X0)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,X1,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_11760,c_14795]) ).
tcf(c_29204,plain,
coll(sK27,sK20,sK26),
inference(superposition,[status(thm)],[c_27224,c_8416]) ).
tcf(c_29623,plain,
coll(sK20,sK23,sK21),
inference(superposition,[status(thm)],[c_27748,c_49]) ).
tcf(c_29942,plain,
coll(sK27,sK26,sK20),
inference(superposition,[status(thm)],[c_29204,c_49]) ).
tcf(c_30215,plain,
! [X0: $i] :
( coll(sK21,X0,sK20)
| ~ coll(sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_29623,c_51]) ).
tcf(c_30223,plain,
( coll(sK21,sK22,sK20)
| ~ coll(sK20,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_30215]) ).
tcf(c_30600,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK21,X0,X1,sK22,sK21,X0,X1)
| ~ para(sK22,sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_30601,plain,
( eqangle(sK22,sK21,sK22,sK22,sK22,sK21,sK22,sK22)
| ~ para(sK22,sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_30600]) ).
tcf(c_30801,plain,
coll(sK21,sK20,sK27),
inference(superposition,[status(thm)],[c_29942,c_8208]) ).
tcf(c_30827,plain,
coll(sK21,sK27,sK20),
inference(superposition,[status(thm)],[c_30801,c_49]) ).
tcf(c_30878,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK27,X0) ),
inference(superposition,[status(thm)],[c_30827,c_51]) ).
tcf(c_30885,plain,
( coll(sK20,sK22,sK21)
| ~ coll(sK21,sK27,sK22) ),
inference(instantiation,[status(thm)],[c_30878]) ).
tcf(c_32576,plain,
( cong(sK22,sK21,sK22,sK21)
| ~ midp(sK20,sK21,sK22) ),
inference(superposition,[status(thm)],[c_9776,c_9775]) ).
tcf(c_32719,plain,
! [X0: $i] :
( coll(sK24,sK26,X0)
| ~ coll(sK24,X0,sK26) ),
inference(instantiation,[status(thm)],[c_20602]) ).
tcf(c_33755,plain,
coll(sK20,sK22,sK22),
inference(superposition,[status(thm)],[c_13422,c_115]) ).
tcf(c_33766,plain,
coll(sK22,sK20,sK22),
inference(superposition,[status(thm)],[c_33755,c_50]) ).
tcf(c_33806,plain,
( cong(sK22,sK21,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_9820]) ).
tcf(c_33807,plain,
( cong(sK22,sK21,sK22,sK20)
| ~ midp(sK21,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8875,c_9820]) ).
tcf(c_34025,plain,
! [X0: $i] :
( circle(sK22,sK21,X0,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK21,sK22,X0) ),
inference(superposition,[status(thm)],[c_33806,c_60]) ).
tcf(c_34163,plain,
( cong(sK22,sK21,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_33807,c_9100,c_10718,c_11359,c_11726,c_13157,c_13793,c_14988,c_16847,c_20610,c_28438,c_30223,c_33807]) ).
tcf(c_34182,plain,
( cong(sK22,sK22,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_34163,c_9292]) ).
tcf(c_34290,plain,
( midp(sK22,sK22,sK20)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_34182,c_116]) ).
tcf(c_34296,plain,
( cong(sK22,sK20,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_34182,c_72]) ).
tcf(c_34303,plain,
! [X0: $i] :
( cyclic(sK22,sK20,sK21,X0)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_34182,c_14795]) ).
tcf(c_34440,plain,
! [X0: $i] :
( coll(sK22,X0,sK22)
| ~ coll(sK22,sK20,X0) ),
inference(superposition,[status(thm)],[c_33766,c_51]) ).
tcf(c_34446,plain,
( coll(sK22,sK22,sK22)
| ~ coll(sK22,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_34440]) ).
tcf(c_34902,plain,
coll(sK22,sK23,sK21),
inference(superposition,[status(thm)],[c_22032,c_11720]) ).
tcf(c_35174,plain,
coll(sK22,sK21,sK23),
inference(superposition,[status(thm)],[c_34902,c_49]) ).
tcf(c_35813,plain,
( circle(sK22,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_33806,c_34025]) ).
tcf(c_35855,plain,
( perp(sK21,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK22,sK21,sK21) ),
inference(superposition,[status(thm)],[c_35813,c_102]) ).
tcf(c_35856,plain,
( perp(sK21,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_35855,c_9974]) ).
tcf(c_35994,plain,
coll(sK21,sK23,sK22),
inference(superposition,[status(thm)],[c_35174,c_9975]) ).
tcf(c_36139,plain,
( perp(sK22,sK20,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_35856,c_28339]) ).
tcf(c_36313,plain,
( cyclic(sK22,sK20,sK21,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_11773,c_34303]) ).
tcf(c_59956,plain,
! [X0: $i] :
( cyclic(sK21,X0,sK22,sK22)
| ~ coll(sK22,sK22,X0)
| ~ eqangle(sK22,sK21,sK22,X0,sK22,sK21,sK22,X0) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_59957,plain,
( cyclic(sK21,sK22,sK22,sK22)
| ~ coll(sK22,sK22,sK22)
| ~ eqangle(sK22,sK21,sK22,sK22,sK22,sK21,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_59956]) ).
tcf(c_63653,plain,
perp(sK22,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_6495,c_56]) ).
tcf(c_63684,plain,
perp(sK22,sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_63653,c_55]) ).
tcf(c_63687,plain,
perp(sK20,sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_63684,c_56]) ).
tcf(c_64119,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X0,X1)
| ~ cong(X0,X0,X0,X1) ),
inference(superposition,[status(thm)],[c_95,c_87]) ).
tcf(c_64182,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X0,X1)
| ~ midp(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_117,c_64119]) ).
tcf(c_64383,plain,
( cong(sK20,sK22,sK20,sK21)
| ~ midp(sK22,sK22,sK21) ),
inference(superposition,[status(thm)],[c_63687,c_104]) ).
tcf(c_64541,plain,
( midp(sK20,sK22,sK21)
| ~ midp(sK22,sK22,sK21)
| ~ coll(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_64383,c_116]) ).
tcf(c_65473,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X2,X3,X4,X5,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_88,c_69]) ).
tcf(c_81568,plain,
! [X0: $i] :
( cyclic(sK22,X0,sK21,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,X0,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_28632]) ).
tcf(c_81705,plain,
! [X0: $i] :
( cyclic(X0,sK22,sK21,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,X0,sK21) ),
inference(superposition,[status(thm)],[c_81568,c_64]) ).
tcf(c_81725,plain,
! [X0: $i] :
( perp(sK21,X0,X0,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,X0,sK21)
| ~ cong(X0,sK21,sK22,sK21) ),
inference(superposition,[status(thm)],[c_81705,c_106]) ).
tcf(c_81742,plain,
( perp(sK21,sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,sK22,sK21)
| ~ cong(sK22,sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_81725]) ).
tcf(c_87121,plain,
! [X0: $i] :
( cyclic(sK21,sK22,sK22,X0)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK21,sK22,X0) ),
inference(superposition,[status(thm)],[c_9101,c_14804]) ).
tcf(c_87212,plain,
( cyclic(sK21,sK22,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_9101,c_87121]) ).
tcf(c_87267,plain,
cyclic(sK21,sK22,sK22,sK22),
inference(global_subsumption_just,[status(thm)],[c_87212,c_9968,c_30601,c_33766,c_34446,c_59957]) ).
tcf(c_87270,plain,
! [X0: $i] :
( cyclic(sK22,sK22,sK22,X0)
| ~ cyclic(sK21,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_87267,c_65]) ).
tcf(c_87271,plain,
cyclic(sK22,sK21,sK22,sK22),
inference(superposition,[status(thm)],[c_87267,c_64]) ).
tcf(c_87278,plain,
( cyclic(sK22,sK22,sK22,sK22)
| ~ cyclic(sK21,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_87270]) ).
tcf(c_87312,plain,
! [X0: $i] :
( cyclic(sK21,sK22,sK22,X0)
| ~ cyclic(sK22,sK21,sK22,X0) ),
inference(superposition,[status(thm)],[c_87271,c_65]) ).
tcf(c_88480,plain,
! [X0: $i] :
( cyclic(sK22,sK20,sK20,X0)
| ~ midp(sK21,sK22,sK20)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8875,c_14806]) ).
tcf(c_89457,plain,
( cyclic(sK22,sK20,sK20,sK21)
| ~ midp(sK21,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8865,c_88480]) ).
tcf(c_89470,plain,
( cyclic(sK22,sK20,sK20,sK21)
| ~ midp(sK21,sK22,sK20)
| ~ midp(sK21,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_11766,c_88480]) ).
tcf(c_89597,plain,
( cyclic(sK22,sK20,sK20,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_89457,c_9100,c_10718,c_10743,c_11359,c_11385,c_11726,c_13157,c_13793,c_14988,c_16847,c_17233,c_20610,c_30223,c_34290,c_89470]) ).
tcf(c_89605,plain,
( cyclic(sK20,sK22,sK20,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_89597,c_64]) ).
tcf(c_89732,plain,
( cyclic(sK20,sK20,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_89605,c_63]) ).
tcf(c_94959,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X1,X0,X2)
| ~ coll(X0,X2,X1)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_65473,c_91]) ).
tcf(c_94960,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| cyclic(X1,X1,X0,X2)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_65473,c_90]) ).
tcf(c_94980,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X1,X0,X2)
| ~ para(X0,X1,X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_94960,c_94959]) ).
tcf(c_102570,plain,
( midp(sK21,sK21,sK22)
| ~ midp(sK21,sK21,sK20)
| ~ coll(sK21,sK21,sK22) ),
inference(superposition,[status(thm)],[c_17197,c_116]) ).
tcf(c_102585,plain,
( midp(sK21,sK21,sK22)
| ~ midp(sK21,sK21,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_102570,c_11359]) ).
tcf(c_102638,plain,
midp(sK21,sK21,sK22),
inference(global_subsumption_just,[status(thm)],[c_102585,c_180,c_183,c_238,c_9968,c_12609,c_22686,c_30601,c_33766,c_34446,c_59957,c_87278]) ).
tcf(c_102640,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK22,X1)
| ~ midp(sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_102638,c_112]) ).
tcf(c_104738,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK26,X1)
| ~ coll(X0,sK26,X1)
| ~ cong(X0,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_105164,plain,
( midp(sK22,sK21,sK21)
| ~ midp(sK20,sK21,sK22)
| ~ coll(sK22,sK21,sK21) ),
inference(superposition,[status(thm)],[c_32576,c_116]) ).
tcf(c_105191,plain,
( midp(sK22,sK21,sK21)
| ~ midp(sK20,sK21,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_105164,c_9974]) ).
tcf(c_105388,plain,
midp(sK22,sK21,sK21),
inference(global_subsumption_just,[status(thm)],[c_105191,c_180,c_183,c_238,c_9968,c_12609,c_30601,c_33766,c_34446,c_59957,c_87278]) ).
tcf(c_105390,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK21,X1)
| ~ midp(sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_105388,c_112]) ).
tcf(c_110545,plain,
( perp(sK21,sK21,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_36139,c_56]) ).
tcf(c_110548,plain,
( para(sK22,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_36139,c_8970]) ).
tcf(c_110582,plain,
( cyclic(sK20,sK22,sK21,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_36313,c_64]) ).
tcf(c_110628,plain,
! [X0: $i] :
( midp(sK21,X0,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ midp(sK22,X0,sK21)
| ~ coll(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_110548,c_94]) ).
tcf(c_112522,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK22,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_112536,plain,
! [X0: $i,X1: $i] :
( cong(sK21,X0,sK21,X1)
| ~ midp(sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_112537,plain,
( cong(sK21,sK22,sK21,sK22)
| ~ midp(sK21,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_112536]) ).
tcf(c_113498,plain,
! [X0: $i] :
( cyclic(sK20,sK22,sK21,X0)
| ~ midp(sK20,sK22,sK21)
| ~ cyclic(sK20,sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_89732,c_65]) ).
tcf(c_115708,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,X1,sK22)
| ~ midp(sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_102640,c_52]) ).
tcf(c_119638,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,X1,sK21)
| ~ midp(sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_105390,c_52]) ).
tcf(c_125558,plain,
! [X0: $i,X1: $i] :
( perp(sK23,sK24,sK27,sK26)
| ~ perp(X0,X1,sK27,sK26)
| ~ para(sK23,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_125559,plain,
( perp(sK23,sK24,sK27,sK26)
| ~ perp(sK22,sK22,sK27,sK26)
| ~ para(sK23,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_125558]) ).
tcf(c_126284,plain,
! [X0: $i,X1: $i] :
( perp(X1,sK24,X0,X1)
| ~ perp(X0,X1,X1,sK24) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_126285,plain,
( perp(sK22,sK24,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_126284]) ).
tcf(c_126462,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X4,sK24,X2,X3)
| ~ perp(X4,sK24,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_126463,plain,
( para(sK22,sK24,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22)
| ~ perp(sK22,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_126462]) ).
tcf(c_128892,plain,
! [X0: $i] :
( para(sK22,sK20,sK22,X0)
| ~ perp(sK22,sK20,sK21,sK22)
| ~ perp(sK21,sK22,sK22,X0) ),
inference(instantiation,[status(thm)],[c_10414]) ).
tcf(c_130154,plain,
( cong(sK21,sK22,sK21,sK20)
| ~ midp(sK21,sK22,sK20)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_110545,c_104]) ).
tcf(c_130869,plain,
! [X0: $i] :
( cyclic(sK22,sK21,sK22,X0)
| ~ midp(sK20,sK22,sK21)
| ~ cyclic(sK20,sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_110582,c_65]) ).
tcf(c_131968,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X1,sK24)
| ~ cong(X0,sK24,X1,sK24)
| ~ cong(X0,X1,X1,X1) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_131969,plain,
( perp(sK22,sK22,sK22,sK24)
| ~ cong(sK22,sK22,sK22,sK22)
| ~ cong(sK22,sK24,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_131968]) ).
tcf(c_139377,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ midp(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_115708,c_115]) ).
tcf(c_139762,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK21,sK22,sK21)
| ~ midp(sK21,X0,X1)
| ~ perp(X0,sK22,sK22,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_139763,plain,
( cong(sK22,sK21,sK22,sK21)
| ~ midp(sK21,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_139762]) ).
tcf(c_142045,plain,
! [X0: $i] :
( midp(X0,sK26,sK26)
| ~ coll(X0,sK26,sK26)
| ~ cong(X0,sK26,X0,sK26) ),
inference(instantiation,[status(thm)],[c_104738]) ).
tcf(c_142046,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK26,X0,sK26)
| ~ midp(sK26,X0,X1)
| ~ perp(X0,X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_142047,plain,
( midp(sK22,sK26,sK26)
| ~ coll(sK22,sK26,sK26)
| ~ cong(sK22,sK26,sK22,sK26) ),
inference(instantiation,[status(thm)],[c_142045]) ).
tcf(c_142048,plain,
( cong(sK22,sK26,sK22,sK26)
| ~ midp(sK26,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_142046]) ).
tcf(c_144142,plain,
! [X0: $i] :
( coll(sK21,X0,sK21)
| ~ midp(sK22,X0,sK21) ),
inference(superposition,[status(thm)],[c_119638,c_115]) ).
tcf(c_152425,plain,
! [X0: $i] :
( cong(X0,sK27,X0,sK27)
| ~ midp(X0,sK27,sK27) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_152426,plain,
( cong(sK22,sK27,sK22,sK27)
| ~ midp(sK22,sK27,sK27) ),
inference(instantiation,[status(thm)],[c_152425]) ).
tcf(c_170998,plain,
coll(sK26,sK25,sK23),
inference(superposition,[status(thm)],[c_6487,c_49]) ).
tcf(c_171139,plain,
! [X0: $i] :
( coll(sK23,X0,sK26)
| ~ coll(sK26,sK25,X0) ),
inference(superposition,[status(thm)],[c_170998,c_51]) ).
tcf(c_171215,plain,
perp(sK22,sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_6495,c_55]) ).
tcf(c_171220,plain,
perp(sK22,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_6495,c_56]) ).
tcf(c_171221,plain,
perp(sK21,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_171215,c_56]) ).
tcf(c_171224,plain,
perp(sK22,sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_171220,c_55]) ).
tcf(c_171359,plain,
coll(sK23,sK23,sK26),
inference(superposition,[status(thm)],[c_170998,c_171139]) ).
tcf(c_171361,plain,
! [X0: $i] :
( coll(sK26,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_171359,c_51]) ).
tcf(c_171405,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_117,c_72]) ).
tcf(c_171805,plain,
( perp(sK22,sK23,sK23,sK32)
| ~ coll(sK20,sK22,sK32) ),
inference(superposition,[status(thm)],[c_6492,c_102]) ).
tcf(c_171830,plain,
! [X0: $i,X1: $i] :
( midp(sK21,sK22,sK22)
| ~ coll(sK21,sK22,sK22)
| ~ midp(X0,sK22,X1)
| ~ para(X0,sK21,X1,sK22) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_171842,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_6495,c_104]) ).
tcf(c_171843,plain,
( cong(sK22,sK21,sK22,sK22)
| ~ midp(sK20,sK21,sK22) ),
inference(superposition,[status(thm)],[c_171215,c_104]) ).
tcf(c_171844,plain,
( cong(sK22,sK22,sK22,sK20)
| ~ midp(sK21,sK22,sK20) ),
inference(superposition,[status(thm)],[c_171220,c_104]) ).
tcf(c_171845,plain,
( cong(sK21,sK22,sK21,sK20)
| ~ midp(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_171221,c_104]) ).
tcf(c_171846,plain,
( cong(sK22,sK20,sK22,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_171224,c_104]) ).
tcf(c_171967,plain,
! [X0: $i] :
( cong(sK22,X0,sK23,X0)
| ~ coll(sK20,sK22,sK32)
| ~ midp(X0,sK22,sK32) ),
inference(superposition,[status(thm)],[c_171805,c_101]) ).
tcf(c_172106,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ perp(sK22,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6495,c_57]) ).
tcf(c_172115,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ perp(sK21,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_171215,c_57]) ).
tcf(c_172116,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK21,X0,X1)
| ~ perp(sK22,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_171220,c_57]) ).
tcf(c_172272,plain,
! [X0: $i] :
( circle(sK22,sK22,X0,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_171842,c_60]) ).
tcf(c_172273,plain,
( midp(sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK22,sK22,sK21) ),
inference(superposition,[status(thm)],[c_171842,c_116]) ).
tcf(c_172274,plain,
( cong(sK22,sK21,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_171842,c_72]) ).
tcf(c_172311,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK20,sK21,sK22) ),
inference(superposition,[status(thm)],[c_171843,c_72]) ).
tcf(c_172325,plain,
! [X0: $i] :
( circle(sK22,sK22,X0,sK20)
| ~ midp(sK21,sK22,sK20)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_171844,c_60]) ).
tcf(c_172326,plain,
( midp(sK22,sK22,sK20)
| ~ midp(sK21,sK22,sK20)
| ~ coll(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_171844,c_116]) ).
tcf(c_172395,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK22,X0,X1)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_171842,c_73]) ).
tcf(c_172396,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK21,X0,X1)
| ~ midp(sK20,sK21,sK22)
| ~ cong(sK22,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_171843,c_73]) ).
tcf(c_172945,plain,
( midp(sK21,sK22,sK22)
| ~ midp(sK21,sK22,sK21)
| ~ coll(sK21,sK22,sK22)
| ~ para(sK21,sK21,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_171830]) ).
tcf(c_172946,plain,
( para(sK21,sK21,sK21,sK22)
| ~ midp(sK21,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_64182]) ).
tcf(c_172987,plain,
para(sK22,sK21,sK22,sK21),
inference(superposition,[status(thm)],[c_6495,c_172116]) ).
tcf(c_172988,plain,
para(sK22,sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_171215,c_172116]) ).
tcf(c_172993,plain,
coll(sK22,sK21,sK21),
inference(superposition,[status(thm)],[c_172987,c_115]) ).
tcf(c_172994,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_172993,c_51]) ).
tcf(c_173000,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK21,X0,X1)
| ~ para(sK21,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_172988,c_54]) ).
tcf(c_173007,plain,
midp(sK22,sK22,sK21),
inference(global_subsumption_just,[status(thm)],[c_172273,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_33766,c_34446,c_59957,c_87278,c_172945,c_172946]) ).
tcf(c_173011,plain,
coll(sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_173007,c_118]) ).
tcf(c_173012,plain,
midp(sK22,sK21,sK22),
inference(superposition,[status(thm)],[c_173007,c_59]) ).
tcf(c_173071,plain,
! [X0: $i,X1: $i] :
( midp(sK21,X0,X1)
| ~ coll(sK21,X0,X1)
| ~ cong(sK21,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_173076,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(sK21,X1,X3)
| ~ midp(sK21,X0,X2)
| ~ para(X0,X3,X2,X1)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_173657,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK23,sK24,X1,X2)
| ~ midp(X0,sK24,X2)
| ~ midp(X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_173672,plain,
! [X0: $i] :
( midp(sK21,X0,sK22)
| ~ midp(sK22,X0,sK21)
| ~ coll(sK21,X0,sK22) ),
inference(superposition,[status(thm)],[c_172988,c_94]) ).
tcf(c_173783,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK22,X1)
| ~ midp(sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_173012,c_112]) ).
tcf(c_174321,plain,
! [X0: $i] :
( circle(sK22,sK22,X0,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(global_subsumption_just,[status(thm)],[c_172272,c_180,c_183,c_238,c_9240,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_174366,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X0,X1)
| ~ coll(sK26,X0,X1)
| ~ cong(sK26,X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_174368,plain,
( midp(sK26,sK22,sK22)
| ~ coll(sK26,sK22,sK22)
| ~ cong(sK26,sK22,sK26,sK22) ),
inference(instantiation,[status(thm)],[c_174366]) ).
tcf(c_174669,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK22,X0,X1)
| ~ cong(sK22,sK21,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_172395,c_180,c_183,c_238,c_9292,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_174679,plain,
( cong(sK22,sK22,sK23,sK21)
| ~ midp(sK21,sK22,sK32)
| ~ coll(sK20,sK22,sK32) ),
inference(superposition,[status(thm)],[c_171967,c_174669]) ).
tcf(c_174683,plain,
( cong(sK22,sK22,sK22,sK22)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_172274,c_174669]) ).
tcf(c_177275,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X0,sK21,X1)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X1)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_171842,c_61]) ).
tcf(c_178755,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X0,sK21,X1)
| ~ cong(sK22,sK22,sK22,X0)
| ~ cong(sK22,sK22,sK22,X1) ),
inference(global_subsumption_just,[status(thm)],[c_177275,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_14795,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_178756,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X0,sK21,X1)
| ~ cong(sK22,sK22,sK22,X1)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(renaming,[status(thm)],[c_178755]) ).
tcf(c_178765,plain,
! [X0: $i] :
( cyclic(sK22,sK21,sK21,X0)
| ~ midp(sK20,sK22,sK21)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_171842,c_178756]) ).
tcf(c_178805,plain,
! [X0: $i] :
( cyclic(sK22,sK21,sK21,X0)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(global_subsumption_just,[status(thm)],[c_178765,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16021,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_178814,plain,
( cyclic(sK22,sK21,sK21,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_171842,c_178805]) ).
tcf(c_178850,plain,
cyclic(sK22,sK21,sK21,sK21),
inference(global_subsumption_just,[status(thm)],[c_178814,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16071,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_178852,plain,
( perp(sK21,sK22,sK22,sK21)
| ~ cong(sK22,sK21,sK21,sK21) ),
inference(superposition,[status(thm)],[c_178850,c_106]) ).
tcf(c_179693,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_6495,c_104]) ).
tcf(c_180808,plain,
perp(sK22,sK21,sK22,sK20),
inference(resolution,[status(thm)],[c_56,c_6495]) ).
tcf(c_181644,plain,
cong(sK21,sK22,sK21,sK20),
inference(global_subsumption_just,[status(thm)],[c_171845,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_14988,c_16847,c_20610,c_22686,c_28438,c_30223,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_130154,c_172945,c_172946]) ).
tcf(c_181651,plain,
cong(sK21,sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_181644,c_72]) ).
tcf(c_182486,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK27,sK26)
| ~ cong(X0,sK26,X1,sK26)
| ~ cong(X0,sK27,X1,sK27) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_182487,plain,
( perp(sK22,sK22,sK27,sK26)
| ~ cong(sK22,sK26,sK22,sK26)
| ~ cong(sK22,sK27,sK22,sK27) ),
inference(instantiation,[status(thm)],[c_182486]) ).
tcf(c_182637,plain,
cong(sK22,sK22,sK22,sK21),
inference(global_subsumption_just,[status(thm)],[c_179693,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_33766,c_34446,c_59957,c_87278,c_112522,c_172945,c_172946]) ).
tcf(c_182641,plain,
cong(sK22,sK21,sK22,sK22),
inference(superposition,[status(thm)],[c_182637,c_72]) ).
tcf(c_182716,plain,
cong(sK22,sK20,sK22,sK22),
inference(global_subsumption_just,[status(thm)],[c_171846,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34296,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_182725,plain,
cong(sK22,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_182716,c_72]) ).
tcf(c_182797,plain,
cong(sK22,sK22,sK22,sK21),
inference(global_subsumption_just,[status(thm)],[c_172311,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_33766,c_34446,c_59957,c_87278,c_112522,c_172945,c_172946]) ).
tcf(c_183323,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK21,X0,X1)
| ~ cong(sK22,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_182641,c_73]) ).
tcf(c_184575,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK24,X0,X1)
| ~ midp(sK21,sK24,X1)
| ~ midp(sK21,sK23,X0) ),
inference(instantiation,[status(thm)],[c_173657]) ).
tcf(c_184578,plain,
( para(sK23,sK24,sK22,sK22)
| ~ midp(sK21,sK24,sK22)
| ~ midp(sK21,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_184575]) ).
tcf(c_184611,plain,
cong(sK22,sK22,sK22,sK22),
inference(global_subsumption_just,[status(thm)],[c_174683,c_183,c_238,c_9968,c_30601,c_33766,c_34446,c_59957,c_87278]) ).
tcf(c_184627,plain,
cyclic(sK22,sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_184611,c_178805]) ).
tcf(c_184629,plain,
circle(sK22,sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_184611,c_174321]) ).
tcf(c_184711,plain,
cyclic(sK21,sK22,sK21,sK22),
inference(superposition,[status(thm)],[c_184627,c_64]) ).
tcf(c_184746,plain,
( perp(sK22,sK22,sK22,sK21)
| ~ coll(sK22,sK22,sK21) ),
inference(superposition,[status(thm)],[c_184629,c_102]) ).
tcf(c_184747,plain,
perp(sK22,sK22,sK22,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_184746,c_173011]) ).
tcf(c_185101,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,sK24,X3,sK24)
| ~ cyclic(X1,sK24,X0,sK24)
| ~ cyclic(X1,sK24,X0,X3)
| ~ cyclic(X1,sK24,X0,X2)
| ~ eqangle(X0,X1,X0,sK24,X2,X3,X2,sK24) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_185102,plain,
( cong(sK22,sK24,sK22,sK24)
| ~ cyclic(sK22,sK24,sK22,sK22)
| ~ cyclic(sK22,sK24,sK22,sK24)
| ~ eqangle(sK22,sK22,sK22,sK24,sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_185101]) ).
tcf(c_185331,plain,
! [X0: $i,X1: $i] :
( cong(sK26,X1,sK26,X0)
| ~ cong(sK26,X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_185332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(sK26,X3,sK26,X2)
| ~ cong(sK26,X3,X0,X1)
| ~ cong(X0,X1,sK26,X2) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_185525,plain,
perp(sK21,sK22,sK22,sK21),
inference(global_subsumption_just,[status(thm)],[c_178852,c_180,c_183,c_189,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_81742,c_87278,c_139763,c_172945,c_172946]) ).
tcf(c_185537,plain,
para(sK22,sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_185525,c_172115]) ).
tcf(c_185816,plain,
coll(sK22,sK20,sK21),
inference(superposition,[status(thm)],[c_185537,c_115]) ).
tcf(c_186023,plain,
midp(sK22,sK22,sK20),
inference(global_subsumption_just,[status(thm)],[c_172326,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_10743,c_11359,c_11385,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34290,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_186027,plain,
coll(sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_186023,c_118]) ).
tcf(c_186200,plain,
! [X0: $i] :
( midp(sK21,X0,sK22)
| ~ midp(sK22,X0,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_173672,c_180,c_183,c_238,c_9968,c_9976,c_10705,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_110628,c_139377,c_144142,c_172945,c_172946]) ).
tcf(c_187644,plain,
coll(sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_185816,c_49]) ).
tcf(c_190561,plain,
coll(sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_187644,c_172994]) ).
tcf(c_192974,plain,
! [X0: $i] :
( eqangle(X0,sK22,X0,sK24,X0,sK22,X0,sK24)
| ~ para(X0,sK22,X0,sK22) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_192976,plain,
( eqangle(sK22,sK22,sK22,sK24,sK22,sK22,sK22,sK24)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_192974]) ).
tcf(c_193133,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ perp(sK22,sK21,X0,X1) ),
inference(resolution,[status(thm)],[c_57,c_6495]) ).
tcf(c_193961,plain,
! [X0: $i] :
( circle(sK22,sK22,X0,sK20)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(global_subsumption_just,[status(thm)],[c_172325,c_180,c_183,c_238,c_9794,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_14988,c_16847,c_20610,c_22686,c_28438,c_30223,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_172945,c_172946]) ).
tcf(c_193970,plain,
circle(sK22,sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_182797,c_193961]) ).
tcf(c_194227,plain,
para(sK22,sK20,sK22,sK20),
inference(resolution,[status(thm)],[c_193133,c_180808]) ).
tcf(c_194679,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X2,X1,sK24)
| ~ cyclic(X0,X1,X2,sK24) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_194685,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X3,sK24)
| ~ cyclic(X0,X1,X2,sK24)
| ~ cyclic(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_194701,plain,
! [X0: $i,X1: $i] :
( cyclic(X1,X1,X0,sK24)
| ~ para(X0,X1,X0,X1) ),
inference(instantiation,[status(thm)],[c_94980]) ).
tcf(c_194702,plain,
( cyclic(sK22,sK22,sK22,sK24)
| ~ para(sK22,sK22,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_194701]) ).
tcf(c_194735,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK21,X0,X1)
| ~ cong(sK22,sK22,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_172396,c_183323]) ).
tcf(c_197893,plain,
( midp(sK21,sK20,sK22)
| ~ coll(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_181651,c_116]) ).
tcf(c_197904,plain,
midp(sK21,sK20,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_197893,c_190561]) ).
tcf(c_198041,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK22,X1)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_197904,c_93]) ).
tcf(c_198399,plain,
! [X0: $i] :
( cyclic(sK22,sK20,sK21,X0)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_182725,c_178756]) ).
tcf(c_198926,plain,
cyclic(sK22,sK20,sK21,sK21),
inference(superposition,[status(thm)],[c_182797,c_198399]) ).
tcf(c_198927,plain,
cyclic(sK22,sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_182725,c_198399]) ).
tcf(c_199327,plain,
cyclic(sK21,sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_184711,c_62]) ).
tcf(c_199342,plain,
perp(sK22,sK21,sK22,sK22),
inference(superposition,[status(thm)],[c_184747,c_56]) ).
tcf(c_200700,plain,
( perp(sK22,sK21,sK21,sK20)
| ~ coll(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_193970,c_102]) ).
tcf(c_200701,plain,
perp(sK22,sK21,sK21,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_200700,c_186027]) ).
tcf(c_202765,plain,
! [X0: $i] :
( cyclic(sK22,sK22,sK21,X0)
| ~ cyclic(sK21,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_199327,c_65]) ).
tcf(c_202775,plain,
para(sK22,sK20,sK22,sK22),
inference(superposition,[status(thm)],[c_199342,c_172106]) ).
tcf(c_202874,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ para(sK22,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_202775,c_54]) ).
tcf(c_205435,plain,
cyclic(sK20,sK22,sK21,sK21),
inference(superposition,[status(thm)],[c_198926,c_64]) ).
tcf(c_205443,plain,
cyclic(sK20,sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_198927,c_64]) ).
tcf(c_206651,plain,
para(sK22,sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_200701,c_172106]) ).
tcf(c_206742,plain,
! [X0: $i] :
( midp(X0,sK20,sK20)
| ~ midp(X0,sK22,sK21)
| ~ para(sK22,sK20,sK21,sK20) ),
inference(superposition,[status(thm)],[c_206651,c_113]) ).
tcf(c_206755,plain,
! [X0: $i] :
( midp(X0,sK20,sK20)
| ~ midp(X0,sK22,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_206742,c_206651]) ).
tcf(c_206864,plain,
midp(sK22,sK20,sK20),
inference(superposition,[status(thm)],[c_173007,c_206755]) ).
tcf(c_209415,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK21,sK24,X1)
| ~ midp(sK21,X0,X2)
| ~ para(X0,sK24,X2,X1)
| ~ para(X0,X1,X2,sK24) ),
inference(instantiation,[status(thm)],[c_173076]) ).
tcf(c_209416,plain,
( midp(sK21,sK24,sK22)
| ~ midp(sK21,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK24)
| ~ para(sK22,sK24,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_209415]) ).
tcf(c_211809,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X1,X4,sK24)
| ~ perp(X2,X3,X4,sK24)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_211810,plain,
( para(sK22,sK22,sK22,sK24)
| ~ perp(sK22,sK22,sK22,sK22)
| ~ perp(sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_211809]) ).
tcf(c_213196,plain,
! [X0: $i] :
( cyclic(sK22,sK21,sK21,X0)
| ~ cyclic(sK20,sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_205435,c_65]) ).
tcf(c_214504,plain,
cyclic(sK20,sK22,sK20,sK21),
inference(superposition,[status(thm)],[c_205443,c_62]) ).
tcf(c_218389,plain,
cyclic(sK20,sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_214504,c_63]) ).
tcf(c_219582,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,sK24,X2)
| ~ cyclic(X0,X1,X2,sK24) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_219583,plain,
( cyclic(sK22,sK22,sK24,sK22)
| ~ cyclic(sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_219582]) ).
tcf(c_220792,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,sK24,X1,X2)
| ~ cyclic(X0,X1,sK24,X2) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_220793,plain,
( cyclic(sK22,sK24,sK22,sK22)
| ~ cyclic(sK22,sK22,sK24,sK22) ),
inference(instantiation,[status(thm)],[c_220792]) ).
tcf(c_220818,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,sK24,X1,sK24)
| ~ cyclic(X0,X1,sK24,sK24) ),
inference(instantiation,[status(thm)],[c_194679]) ).
tcf(c_220820,plain,
( cyclic(sK22,sK24,sK22,sK24)
| ~ cyclic(sK22,sK22,sK24,sK24) ),
inference(instantiation,[status(thm)],[c_220818]) ).
tcf(c_220962,plain,
! [X0: $i] :
( cyclic(sK20,sK22,sK21,X0)
| ~ cyclic(sK20,sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_218389,c_65]) ).
tcf(c_228034,plain,
coll(sK24,sK20,sK23),
inference(superposition,[status(thm)],[c_6490,c_49]) ).
tcf(c_228035,plain,
coll(sK26,sK25,sK23),
inference(superposition,[status(thm)],[c_6487,c_49]) ).
tcf(c_228346,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK23,X0) ),
inference(superposition,[status(thm)],[c_6490,c_51]) ).
tcf(c_228349,plain,
! [X0: $i] :
( coll(sK23,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_228034,c_51]) ).
tcf(c_228350,plain,
! [X0: $i] :
( coll(sK23,X0,sK26)
| ~ coll(sK26,sK25,X0) ),
inference(superposition,[status(thm)],[c_228035,c_51]) ).
tcf(c_228618,plain,
coll(sK23,sK23,sK24),
inference(superposition,[status(thm)],[c_228034,c_228349]) ).
tcf(c_228619,plain,
! [X0: $i] :
( coll(sK24,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_228618,c_51]) ).
tcf(c_228628,plain,
coll(sK23,sK23,sK26),
inference(superposition,[status(thm)],[c_228035,c_228350]) ).
tcf(c_228818,plain,
( perp(sK26,sK27,sK27,sK37)
| ~ coll(sK21,sK26,sK37) ),
inference(superposition,[status(thm)],[c_6485,c_102]) ).
tcf(c_228851,plain,
( cong(sK22,sK22,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_6495,c_104]) ).
tcf(c_228912,plain,
cong(sK22,sK22,sK22,sK21),
inference(global_subsumption_just,[status(thm)],[c_228851,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_33766,c_34446,c_59957,c_87278,c_112522,c_172945,c_172946]) ).
tcf(c_228915,plain,
cong(sK22,sK21,sK22,sK22),
inference(superposition,[status(thm)],[c_228912,c_72]) ).
tcf(c_229353,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK22,X0,X1)
| ~ cong(sK22,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_228912,c_73]) ).
tcf(c_229354,plain,
! [X0: $i,X1: $i] :
( cong(sK22,sK21,X0,X1)
| ~ cong(sK22,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_228915,c_73]) ).
tcf(c_230243,plain,
cong(sK22,sK22,sK22,sK22),
inference(superposition,[status(thm)],[c_228915,c_229353]) ).
tcf(c_231242,plain,
! [X0: $i,X1: $i] :
( coll(sK16(sK26,sK37,sK27,X0,X1),X0,X1)
| ~ coll(sK21,sK26,sK37)
| ~ coll(sK37,X0,X1) ),
inference(superposition,[status(thm)],[c_228818,c_155]) ).
tcf(c_232173,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X2,sK16(sK26,sK37,sK27,X0,X1))
| ~ coll(sK21,sK26,sK37)
| ~ coll(sK37,X0,X1)
| ~ coll(sK16(sK26,sK37,sK27,X0,X1),X0,X2) ),
inference(superposition,[status(thm)],[c_231242,c_51]) ).
tcf(c_233203,plain,
! [X0: $i,X1: $i] :
( cyclic(sK22,X0,sK21,X1)
| ~ cong(sK22,sK22,sK22,X1)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_228912,c_61]) ).
tcf(c_233447,plain,
cong(sK22,sK21,sK22,sK21),
inference(superposition,[status(thm)],[c_228912,c_229354]) ).
tcf(c_239531,plain,
! [X0: $i] :
( midp(sK21,sK23,X0)
| ~ coll(sK21,sK23,X0)
| ~ cong(sK21,sK23,sK21,X0) ),
inference(instantiation,[status(thm)],[c_173071]) ).
tcf(c_239533,plain,
( midp(sK21,sK23,sK22)
| ~ coll(sK21,sK23,sK22)
| ~ cong(sK21,sK23,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_239531]) ).
tcf(c_254548,plain,
! [X0: $i,X1: $i] :
( cyclic(X1,X1,sK24,sK24)
| ~ cyclic(X0,X1,X1,sK24) ),
inference(instantiation,[status(thm)],[c_194685]) ).
tcf(c_254549,plain,
( cyclic(sK22,sK22,sK24,sK24)
| ~ cyclic(sK22,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_254548]) ).
tcf(c_255701,plain,
! [X0: $i] :
( cyclic(sK22,sK22,sK21,X0)
| ~ cong(sK22,sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_230243,c_233203]) ).
tcf(c_256668,plain,
! [X0: $i,X1: $i] :
( cong(sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,X0,X1,sK21),sK26,X0)
| ~ cong(sK26,X0,sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,X0,X1,sK21)) ),
inference(instantiation,[status(thm)],[c_185331]) ).
tcf(c_256670,plain,
( cong(sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,sK22,sK22,sK21),sK26,sK22)
| ~ cong(sK26,sK22,sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,sK22,sK22,sK21)) ),
inference(instantiation,[status(thm)],[c_256668]) ).
tcf(c_256679,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(sK26,X0,sK26,X2)
| ~ cong(sK26,X0,sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,X0,X1,sK21))
| ~ cong(sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,X0,X1,sK21),sK26,X2) ),
inference(instantiation,[status(thm)],[c_185332]) ).
tcf(c_256680,plain,
( cong(sK26,sK22,sK26,sK22)
| ~ cong(sK26,sK22,sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,sK22,sK22,sK21))
| ~ cong(sK26,sK8(sK11(sK26,sK27,sK37,sK21),sK26,sK22,sK22,sK21),sK26,sK22) ),
inference(instantiation,[status(thm)],[c_256679]) ).
tcf(c_263672,plain,
coll(sK24,sK26,sK23),
inference(superposition,[status(thm)],[c_228628,c_228619]) ).
tcf(c_263692,plain,
coll(sK24,sK23,sK26),
inference(superposition,[status(thm)],[c_263672,c_49]) ).
tcf(c_266750,plain,
coll(sK20,sK26,sK24),
inference(superposition,[status(thm)],[c_263692,c_228346]) ).
tcf(c_267580,plain,
coll(sK20,sK24,sK26),
inference(superposition,[status(thm)],[c_266750,c_49]) ).
tcf(c_267956,plain,
! [X0: $i] :
( coll(sK26,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_267580,c_51]) ).
tcf(c_287413,plain,
! [X0: $i] : cyclic(sK20,sK20,sK22,X0),
inference(resolution,[status(thm)],[c_94980,c_194227]) ).
tcf(c_288317,plain,
! [X0: $i] : cyclic(sK22,sK22,sK21,X0),
inference(global_subsumption_just,[status(thm)],[c_255701,c_180,c_183,c_238,c_9968,c_9976,c_10719,c_11359,c_11726,c_12296,c_12609,c_13157,c_13455,c_13793,c_16847,c_20610,c_22686,c_30601,c_30885,c_33766,c_34446,c_59957,c_64541,c_87278,c_87312,c_113498,c_130869,c_172945,c_172946,c_202765,c_287413]) ).
tcf(c_288319,plain,
! [X0: $i] :
( perp(sK21,sK22,sK22,X0)
| ~ cong(sK22,sK21,sK22,sK21)
| ~ cong(sK22,X0,sK22,X0) ),
inference(superposition,[status(thm)],[c_288317,c_106]) ).
tcf(c_288326,plain,
! [X0: $i] :
( perp(sK21,sK22,sK22,X0)
| ~ cong(sK22,X0,sK22,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_288319,c_233447]) ).
tcf(c_289551,plain,
! [X0: $i] :
( perp(sK21,sK22,sK22,X0)
| ~ midp(sK22,X0,X0) ),
inference(superposition,[status(thm)],[c_117,c_288326]) ).
tcf(c_297985,plain,
! [X0: $i] :
( para(sK22,sK20,sK22,X0)
| ~ midp(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_64182,c_202874]) ).
tcf(c_299734,plain,
! [X0: $i] :
( cyclic(sK22,sK21,sK21,X0)
| ~ midp(sK22,X0,sK22) ),
inference(superposition,[status(thm)],[c_171405,c_178805]) ).
tcf(c_300452,plain,
! [X0: $i] :
( para(sK22,sK21,sK22,X0)
| ~ midp(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_173783,c_173000]) ).
tcf(c_300577,plain,
! [X0: $i] : cyclic(sK22,sK21,sK21,X0),
inference(global_subsumption_just,[status(thm)],[c_299734,c_213196,c_220962,c_287413]) ).
tcf(c_300581,plain,
! [X0: $i,X1: $i] :
( cyclic(sK21,sK21,X1,X0)
| ~ cyclic(sK22,sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_300577,c_65]) ).
tcf(c_300585,plain,
! [X0: $i,X1: $i] : cyclic(sK21,sK21,X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_300581,c_300577]) ).
tcf(c_301695,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK21,X0,X2,X1)
| ~ cyclic(sK21,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_300585,c_65]) ).
tcf(c_301699,plain,
! [X0: $i,X1: $i,X2: $i] : cyclic(sK21,X0,X1,X2),
inference(forward_subsumption_resolution,[status(thm)],[c_301695,c_300585]) ).
tcf(c_301853,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_301699,c_65]) ).
tcf(c_301857,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : cyclic(X0,X1,X2,X3),
inference(forward_subsumption_resolution,[status(thm)],[c_301853,c_301699]) ).
tcf(c_301863,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eqangle(X0,X1,X0,X2,X3,X1,X3,X2),
inference(backward_subsumption_resolution,[status(thm)],[c_89,c_301857]) ).
tcf(c_302959,plain,
! [X0: $i,X1: $i] : para(X0,X1,X0,X1),
inference(superposition,[status(thm)],[c_301863,c_87]) ).
tcf(c_303034,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X1)
| ~ midp(X2,X0,X0)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_302959,c_113]) ).
tcf(c_303040,plain,
! [X0: $i,X1: $i] : coll(X0,X1,X1),
inference(superposition,[status(thm)],[c_302959,c_115]) ).
tcf(c_303060,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X2)
| ~ midp(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_303034,c_302959]) ).
tcf(c_305592,plain,
! [X0: $i,X1: $i] : coll(X0,X1,X0),
inference(superposition,[status(thm)],[c_303040,c_50]) ).
tcf(c_306221,plain,
! [X0: $i,X1: $i] : coll(X0,X0,X1),
inference(superposition,[status(thm)],[c_305592,c_49]) ).
tcf(c_306735,plain,
! [X0: $i] : coll(sK26,X0,sK23),
inference(backward_subsumption_resolution,[status(thm)],[c_171361,c_306221]) ).
tcf(c_306784,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X2,X1,X0)
| ~ coll(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_306221,c_51]) ).
tcf(c_306796,plain,
! [X0: $i,X1: $i,X2: $i] : coll(X0,X1,X2),
inference(forward_subsumption_resolution,[status(thm)],[c_306784,c_306221]) ).
tcf(c_306830,plain,
( cong(sK22,sK22,sK23,sK21)
| ~ midp(sK21,sK22,sK32) ),
inference(backward_subsumption_resolution,[status(thm)],[c_174679,c_306796]) ).
tcf(c_310971,plain,
! [X0: $i] : midp(sK22,X0,X0),
inference(superposition,[status(thm)],[c_206864,c_303060]) ).
tcf(c_315232,plain,
! [X0: $i] :
( para(sK22,sK21,sK22,X0)
| ~ midp(sK22,sK20,X0) ),
inference(superposition,[status(thm)],[c_198041,c_173000]) ).
tcf(c_316214,plain,
! [X0: $i] : para(sK22,sK20,sK22,X0),
inference(global_subsumption_just,[status(thm)],[c_297985,c_8098,c_128892,c_289551,c_310971]) ).
tcf(c_316216,plain,
! [X0: $i,X1: $i] :
( midp(X1,sK20,X0)
| ~ midp(X1,sK22,sK22)
| ~ para(sK22,X0,sK22,sK20) ),
inference(superposition,[status(thm)],[c_316214,c_113]) ).
tcf(c_316219,plain,
! [X0: $i] : para(sK22,X0,sK22,sK20),
inference(superposition,[status(thm)],[c_316214,c_53]) ).
tcf(c_316225,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK20,X1)
| ~ midp(X0,sK22,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_316216,c_316219]) ).
tcf(c_316381,plain,
! [X0: $i] : midp(sK22,sK20,X0),
inference(superposition,[status(thm)],[c_310971,c_316225]) ).
tcf(c_316568,plain,
! [X0: $i] : para(sK22,sK21,sK22,X0),
inference(global_subsumption_just,[status(thm)],[c_300452,c_315232,c_316381]) ).
tcf(c_316570,plain,
! [X0: $i,X1: $i] :
( midp(X1,sK21,X0)
| ~ midp(X1,sK22,sK22)
| ~ para(sK22,X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_316568,c_113]) ).
tcf(c_316573,plain,
! [X0: $i] : para(sK22,X0,sK22,sK21),
inference(superposition,[status(thm)],[c_316568,c_53]) ).
tcf(c_316579,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK21,X1)
| ~ midp(X0,sK22,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_316570,c_316573]) ).
tcf(c_318653,plain,
! [X0: $i] : midp(sK22,sK21,X0),
inference(superposition,[status(thm)],[c_310971,c_316579]) ).
tcf(c_318737,plain,
! [X0: $i] : midp(sK22,X0,sK21),
inference(superposition,[status(thm)],[c_318653,c_59]) ).
tcf(c_318756,plain,
! [X0: $i] : midp(sK21,X0,sK22),
inference(backward_subsumption_resolution,[status(thm)],[c_186200,c_318737]) ).
tcf(c_318870,plain,
! [X0: $i] : midp(sK21,sK22,X0),
inference(superposition,[status(thm)],[c_318756,c_59]) ).
tcf(c_318888,plain,
cong(sK22,sK22,sK23,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_306830,c_318870]) ).
tcf(c_319174,plain,
cong(sK22,sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_318888,c_194735]) ).
tcf(c_319230,plain,
cong(sK22,sK21,sK21,sK23),
inference(superposition,[status(thm)],[c_319174,c_71]) ).
tcf(c_319696,plain,
! [X0: $i] : coll(sK26,X0,sK20),
inference(global_subsumption_just,[status(thm)],[c_267956,c_13667,c_16468,c_19099,c_20600,c_21564,c_32719,c_306735]) ).
tcf(c_319700,plain,
! [X0: $i] : coll(sK26,sK20,X0),
inference(superposition,[status(thm)],[c_319696,c_49]) ).
tcf(c_320170,plain,
cong(sK21,sK23,sK22,sK21),
inference(superposition,[status(thm)],[c_319230,c_72]) ).
tcf(c_320626,plain,
cong(sK21,sK23,sK21,sK22),
inference(superposition,[status(thm)],[c_320170,c_71]) ).
tcf(c_320932,plain,
~ coll(sK21,sK26,sK37),
inference(global_subsumption_just,[status(thm)],[c_232173,c_162,c_180,c_183,c_189,c_238,c_2872,c_8475,c_9968,c_9976,c_10719,c_11516,c_12609,c_12744,c_13157,c_13793,c_16847,c_20610,c_20699,c_20848,c_21707,c_22686,c_24087,c_30601,c_33766,c_34446,c_35994,c_59957,c_87278,c_112537,c_125559,c_126285,c_126463,c_131969,c_142047,c_142048,c_152426,c_172945,c_172946,c_174368,c_182487,c_184578,c_185102,c_192976,c_194702,c_209416,c_211810,c_219583,c_220793,c_220820,c_239533,c_254549,c_256670,c_256680,c_320626]) ).
tcf(c_321005,plain,
! [X0: $i,X1: $i] :
( coll(X1,X0,sK26)
| ~ coll(sK26,sK20,X0) ),
inference(superposition,[status(thm)],[c_319700,c_51]) ).
tcf(c_321008,plain,
! [X0: $i,X1: $i] : coll(X0,X1,sK26),
inference(forward_subsumption_resolution,[status(thm)],[c_321005,c_319700]) ).
tcf(c_322849,plain,
! [X0: $i,X1: $i] : coll(X0,sK26,X1),
inference(superposition,[status(thm)],[c_321008,c_49]) ).
tcf(c_322883,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_320932,c_322849]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO606+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.18/0.44 % Computer : n008.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Wed Sep 23 12:32:39 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.18/0.50 Running first-order theorem proving
% 0.18/0.50 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.27/0.52
% 0.27/0.52 % ======== iProver multi-core TPTP/SMT =========
% 0.27/0.52
% 0.27/0.52 % Detected problem language: tptp
% 0.27/0.54 % Proving...
% 121.38/20.88 % SZS status Started for theBenchmark.p
% 121.38/20.88 % SZS status Theorem for theBenchmark.p
% 121.38/20.88
% 121.38/20.88 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 121.38/20.88
% 121.38/20.88 % ------ iProver source info
% 121.38/20.88
% 121.38/20.88 % git: date: 2026-07-19 20:42:38 +0200
% 121.38/20.88 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 121.38/20.88 % git: non_committed_changes: false
% 121.38/20.88
% 121.38/20.88 % ------ Parsing...
% 121.38/20.88 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 121.38/20.88
% 121.38/20.88 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 121.38/20.88
% 121.38/20.88 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 121.38/20.88
% 121.38/20.88 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 121.38/20.88 % ------ Proving...
% 121.38/20.88 % ------ Problem Properties
% 121.38/20.88
% 121.38/20.88 %
% 121.38/20.88 % clauses 125
% 121.38/20.88 % conjectures 13
% 121.38/20.88 % EPR 88
% 121.38/20.88 % Horn 115
% 121.38/20.88 % unary 13
% 121.38/20.88 % binary 37
% 121.38/20.88 % lits 341
% 121.38/20.88 % lits eq 4
% 121.38/20.88 % fd_pure 0
% 121.38/20.88 % fd_pseudo 0
% 121.38/20.88 % fd_cond 0
% 121.38/20.88 % fd_pseudo_cond 4
% 121.38/20.88 % AC symbols 0
% 121.38/20.88
% 121.38/20.88 % ------ Schedule dynamic 5 is on
% 121.38/20.88
% 121.38/20.88 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 121.38/20.88
% 121.38/20.88
% 121.38/20.88 % ------
% 121.38/20.88 % Current options:
% 121.38/20.88 % ------
% 121.38/20.88
% 121.38/20.88
% 121.38/20.88 %
% 121.38/20.88
% 121.38/20.88 % ------ Proving...
% 121.38/20.88 % Proof_search_loop: time out after: 5882 full_loop iterations
% 121.38/20.88
% 121.38/20.88 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 121.38/20.88
% 121.38/20.88
% 121.38/20.88 % ------
% 121.38/20.88 % Current options:
% 121.38/20.88 % ------
% 121.38/20.88
% 121.38/20.88
% 121.38/20.88 %
% 121.38/20.88
% 121.38/20.88 % ------ Proving...
% 121.38/20.88 %
% 121.38/20.88
% 121.38/20.88 % SZS status Theorem for theBenchmark.p
% 121.38/20.88
% 121.38/20.88 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 121.38/20.90
% 121.38/20.90
%------------------------------------------------------------------------------