%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO543+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n006.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:25 PM UTC 2026
% Result : Theorem 40.01s 7.37s
% Output : CNFRefutation 40.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 33
% Syntax : Number of formulae : 608 ( 177 unt; 0 def)
% Number of atoms : 1386 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1452 ( 674 ~; 668 |; 76 &)
% ( 0 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 993 ( 0 sgn 973 !; 20 ?; 446 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD2) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( coll(X0,X1,X3)
& coll(X0,X1,X2) )
=> coll(X2,X3,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD3) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD4) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD5) ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( para(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD6) ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD7) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD8) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& perp(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(f10,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> perp(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD10) ).
fof(f11,axiom,
! [X0,X1,X2] :
( midp(X2,X1,X0)
=> midp(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD11) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( ( cong(X3,X0,X3,X2)
& cong(X3,X0,X3,X1) )
=> circle(X3,X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD12) ).
fof(f13,axiom,
! [X0,X1,X2,X3,X4] :
( ( cong(X4,X0,X4,X3)
& cong(X4,X0,X4,X2)
& cong(X4,X0,X4,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD13) ).
fof(f14,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD14) ).
fof(f15,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD15) ).
fof(f16,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X1,X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD16) ).
fof(f17,axiom,
! [X0,X1,X2,X3,X4] :
( ( cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cyclic(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD17) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD24) ).
fof(f25,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( cong(X2,X3,X4,X5)
& cong(X0,X1,X2,X3) )
=> cong(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD25) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( coll(X2,X3,X1)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
& cyclic(X0,X1,X2,X5)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f45,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X0,X2)
& midp(X3,X0,X1) )
=> para(X3,X4,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD44) ).
fof(f46,axiom,
! [X0,X1,X2,X3,X4] :
( ( coll(X4,X0,X2)
& para(X3,X4,X1,X2)
& midp(X3,X0,X1) )
=> midp(X4,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD45) ).
fof(f54,axiom,
! [X0,X1,X2,X3] :
( ( coll(X3,X0,X2)
& circle(X3,X0,X1,X2) )
=> perp(X0,X1,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD53) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( perp(X3,X2,X0,X1)
& midp(X2,X0,X1) )
=> cong(X3,X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD55) ).
fof(f57,axiom,
! [X0,X1,X2,X3] :
( ( cong(X0,X3,X1,X3)
& cong(X0,X2,X1,X2) )
=> perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD56) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X2,X3)
& midp(X4,X0,X1) )
=> para(X0,X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD63) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4] :
( ( para(X0,X3,X1,X2)
& para(X0,X2,X1,X3)
& midp(X4,X0,X1) )
=> midp(X4,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD64) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( coll(X0,X1,X2)
& cong(X0,X1,X0,X2) )
=> midp(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD67) ).
fof(f69,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> cong(X0,X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD68) ).
fof(f70,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD69) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( midp(X9,X5,X2)
& midp(X8,X4,X1)
& midp(X7,X2,X1)
& coll(X6,X2,X5)
& coll(X6,X1,X4)
& coll(X5,X0,X1)
& perp(X5,X2,X0,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2) )
=> cyclic(X8,X9,X6,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL012003) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( midp(X9,X5,X2)
& midp(X8,X4,X1)
& midp(X7,X2,X1)
& coll(X6,X2,X5)
& coll(X6,X1,X4)
& coll(X5,X0,X1)
& perp(X5,X2,X0,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2) )
=> cyclic(X8,X9,X6,X3) ),
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(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(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(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(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(f191,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f192,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f191]) ).
fof(f193,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(ennf_transformation,[],[f65]) ).
fof(f194,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(flattening,[],[f193]) ).
fof(f198,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f199,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f198]) ).
fof(f200,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f201,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( midp(X9,X5,X2)
& midp(X8,X4,X1)
& midp(X7,X2,X1)
& coll(X6,X2,X5)
& coll(X6,X1,X4)
& coll(X5,X0,X1)
& perp(X5,X2,X0,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2)
& ~ cyclic(X8,X9,X6,X3) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( midp(X9,X5,X2)
& midp(X8,X4,X1)
& midp(X7,X2,X1)
& coll(X6,X2,X5)
& coll(X6,X1,X4)
& coll(X5,X0,X1)
& perp(X5,X2,X0,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X1,X2)
& perp(X3,X0,X1,X2)
& ~ cyclic(X8,X9,X6,X3) ),
inference(flattening,[],[f249]) ).
fof(f270,plain,
( midp(sK29,sK25,sK22)
& midp(sK28,sK24,sK21)
& midp(sK27,sK22,sK21)
& coll(sK26,sK22,sK25)
& coll(sK26,sK21,sK24)
& coll(sK25,sK20,sK21)
& perp(sK25,sK22,sK20,sK21)
& coll(sK24,sK20,sK22)
& perp(sK24,sK21,sK20,sK22)
& coll(sK23,sK21,sK22)
& perp(sK23,sK20,sK21,sK22)
& ~ cyclic(sK28,sK29,sK26,sK23) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29]),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)],[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(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(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(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(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(f334,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f192]) ).
fof(f335,plain,
! [X2,X3,X0,X1,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(cnf_transformation,[],[f194]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f199]) ).
fof(f339,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f200]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f201]) ).
fof(f384,plain,
midp(sK29,sK25,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f385,plain,
midp(sK28,sK24,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f386,plain,
midp(sK27,sK22,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f387,plain,
coll(sK26,sK22,sK25),
inference(cnf_transformation,[],[f270]) ).
fof(f388,plain,
coll(sK26,sK21,sK24),
inference(cnf_transformation,[],[f270]) ).
fof(f389,plain,
coll(sK25,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
perp(sK25,sK22,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f391,plain,
coll(sK24,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f392,plain,
perp(sK24,sK21,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f393,plain,
coll(sK23,sK21,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f394,plain,
perp(sK23,sK20,sK21,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f395,plain,
~ cyclic(sK28,sK29,sK26,sK23),
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_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_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_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_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_112,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X1,X3,X2,X4)
| ~ midp(X0,X3,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X4,X1,X3)
| ~ midp(X4,X0,X2)
| ~ para(X0,X3,X2,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_162,negated_conjecture,
~ cyclic(sK28,sK29,sK26,sK23),
inference(cnf_transformation,[],[f395]) ).
tcf(c_163,negated_conjecture,
perp(sK23,sK20,sK21,sK22),
inference(cnf_transformation,[],[f394]) ).
tcf(c_164,negated_conjecture,
coll(sK23,sK21,sK22),
inference(cnf_transformation,[],[f393]) ).
tcf(c_165,negated_conjecture,
perp(sK24,sK21,sK20,sK22),
inference(cnf_transformation,[],[f392]) ).
tcf(c_166,negated_conjecture,
coll(sK24,sK20,sK22),
inference(cnf_transformation,[],[f391]) ).
tcf(c_167,negated_conjecture,
perp(sK25,sK22,sK20,sK21),
inference(cnf_transformation,[],[f390]) ).
tcf(c_168,negated_conjecture,
coll(sK25,sK20,sK21),
inference(cnf_transformation,[],[f389]) ).
tcf(c_169,negated_conjecture,
coll(sK26,sK21,sK24),
inference(cnf_transformation,[],[f388]) ).
tcf(c_170,negated_conjecture,
coll(sK26,sK22,sK25),
inference(cnf_transformation,[],[f387]) ).
tcf(c_171,negated_conjecture,
midp(sK27,sK22,sK21),
inference(cnf_transformation,[],[f386]) ).
tcf(c_172,negated_conjecture,
midp(sK28,sK24,sK21),
inference(cnf_transformation,[],[f385]) ).
tcf(c_173,negated_conjecture,
midp(sK29,sK25,sK22),
inference(cnf_transformation,[],[f384]) ).
tcf(c_179,plain,
( midp(sK21,sK21,sK21)
| ~ coll(sK21,sK21,sK21)
| ~ cong(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_183,plain,
( eqangle(sK21,sK21,sK21,sK21,sK21,sK21,sK21,sK21)
| ~ para(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_188,plain,
( perp(sK21,sK21,sK21,sK21)
| ~ cong(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_237,plain,
( cong(sK21,sK21,sK21,sK21)
| ~ cyclic(sK21,sK21,sK21,sK21)
| ~ eqangle(sK21,sK21,sK21,sK21,sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_4303,negated_conjecture,
midp(sK29,sK25,sK22),
inference(demodulation,[status(thm)],[c_173]) ).
tcf(c_4304,negated_conjecture,
midp(sK28,sK24,sK21),
inference(demodulation,[status(thm)],[c_172]) ).
tcf(c_4305,negated_conjecture,
midp(sK27,sK22,sK21),
inference(demodulation,[status(thm)],[c_171]) ).
tcf(c_4306,negated_conjecture,
coll(sK26,sK22,sK25),
inference(demodulation,[status(thm)],[c_170]) ).
tcf(c_4307,negated_conjecture,
coll(sK26,sK21,sK24),
inference(demodulation,[status(thm)],[c_169]) ).
tcf(c_4308,negated_conjecture,
coll(sK25,sK20,sK21),
inference(demodulation,[status(thm)],[c_168]) ).
tcf(c_4309,negated_conjecture,
perp(sK25,sK22,sK20,sK21),
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_4310,negated_conjecture,
coll(sK24,sK20,sK22),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_4311,negated_conjecture,
perp(sK24,sK21,sK20,sK22),
inference(demodulation,[status(thm)],[c_165]) ).
tcf(c_4312,negated_conjecture,
coll(sK23,sK21,sK22),
inference(demodulation,[status(thm)],[c_164]) ).
tcf(c_4313,negated_conjecture,
perp(sK23,sK20,sK21,sK22),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_5852,plain,
coll(sK23,sK22,sK21),
inference(superposition,[status(thm)],[c_4312,c_49]) ).
tcf(c_5853,plain,
coll(sK24,sK22,sK20),
inference(superposition,[status(thm)],[c_4310,c_49]) ).
tcf(c_5854,plain,
coll(sK25,sK21,sK20),
inference(superposition,[status(thm)],[c_4308,c_49]) ).
tcf(c_5855,plain,
coll(sK26,sK24,sK21),
inference(superposition,[status(thm)],[c_4307,c_49]) ).
tcf(c_5856,plain,
coll(sK26,sK25,sK22),
inference(superposition,[status(thm)],[c_4306,c_49]) ).
tcf(c_5866,plain,
coll(sK21,sK23,sK22),
inference(superposition,[status(thm)],[c_4312,c_50]) ).
tcf(c_5867,plain,
coll(sK20,sK24,sK22),
inference(superposition,[status(thm)],[c_4310,c_50]) ).
tcf(c_5869,plain,
coll(sK21,sK26,sK24),
inference(superposition,[status(thm)],[c_4307,c_50]) ).
tcf(c_5871,plain,
coll(sK22,sK23,sK21),
inference(superposition,[status(thm)],[c_5852,c_50]) ).
tcf(c_5873,plain,
coll(sK21,sK25,sK20),
inference(superposition,[status(thm)],[c_5854,c_50]) ).
tcf(c_5875,plain,
coll(sK25,sK26,sK22),
inference(superposition,[status(thm)],[c_5856,c_50]) ).
tcf(c_5894,plain,
midp(sK27,sK21,sK22),
inference(superposition,[status(thm)],[c_4305,c_59]) ).
tcf(c_5895,plain,
midp(sK28,sK21,sK24),
inference(superposition,[status(thm)],[c_4304,c_59]) ).
tcf(c_5896,plain,
midp(sK29,sK22,sK25),
inference(superposition,[status(thm)],[c_4303,c_59]) ).
tcf(c_5901,plain,
coll(sK27,sK22,sK21),
inference(superposition,[status(thm)],[c_4305,c_118]) ).
tcf(c_5902,plain,
coll(sK28,sK24,sK21),
inference(superposition,[status(thm)],[c_4304,c_118]) ).
tcf(c_5903,plain,
coll(sK29,sK25,sK22),
inference(superposition,[status(thm)],[c_4303,c_118]) ).
tcf(c_5920,plain,
coll(sK27,sK21,sK22),
inference(superposition,[status(thm)],[c_5894,c_118]) ).
tcf(c_5922,plain,
coll(sK28,sK21,sK24),
inference(superposition,[status(thm)],[c_5895,c_118]) ).
tcf(c_5924,plain,
coll(sK29,sK22,sK25),
inference(superposition,[status(thm)],[c_5896,c_118]) ).
tcf(c_5926,plain,
coll(sK22,sK27,sK21),
inference(superposition,[status(thm)],[c_5901,c_50]) ).
tcf(c_5928,plain,
coll(sK24,sK28,sK21),
inference(superposition,[status(thm)],[c_5902,c_50]) ).
tcf(c_5930,plain,
coll(sK25,sK29,sK22),
inference(superposition,[status(thm)],[c_5903,c_50]) ).
tcf(c_5950,plain,
perp(sK23,sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_4313,c_55]) ).
tcf(c_5957,plain,
perp(sK21,sK22,sK23,sK20),
inference(superposition,[status(thm)],[c_4313,c_56]) ).
tcf(c_5958,plain,
perp(sK20,sK22,sK24,sK21),
inference(superposition,[status(thm)],[c_4311,c_56]) ).
tcf(c_5977,plain,
perp(sK20,sK22,sK21,sK24),
inference(superposition,[status(thm)],[c_5958,c_55]) ).
tcf(c_5980,plain,
coll(sK21,sK27,sK22),
inference(superposition,[status(thm)],[c_5920,c_50]) ).
tcf(c_5982,plain,
coll(sK21,sK28,sK24),
inference(superposition,[status(thm)],[c_5922,c_50]) ).
tcf(c_6007,plain,
coll(sK22,sK29,sK25),
inference(superposition,[status(thm)],[c_5924,c_50]) ).
tcf(c_6010,plain,
coll(sK22,sK21,sK27),
inference(superposition,[status(thm)],[c_5926,c_49]) ).
tcf(c_6012,plain,
coll(sK24,sK21,sK28),
inference(superposition,[status(thm)],[c_5928,c_49]) ).
tcf(c_6014,plain,
coll(sK25,sK22,sK29),
inference(superposition,[status(thm)],[c_5930,c_49]) ).
tcf(c_6028,plain,
coll(sK21,sK22,sK27),
inference(superposition,[status(thm)],[c_5980,c_49]) ).
tcf(c_6030,plain,
coll(sK21,sK24,sK28),
inference(superposition,[status(thm)],[c_5982,c_49]) ).
tcf(c_6048,plain,
! [X0: $i] :
( coll(sK22,X0,sK23)
| ~ coll(sK23,sK21,X0) ),
inference(superposition,[status(thm)],[c_4312,c_51]) ).
tcf(c_6049,plain,
! [X0: $i] :
( coll(sK22,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_4310,c_51]) ).
tcf(c_6050,plain,
! [X0: $i] :
( coll(sK21,X0,sK25)
| ~ coll(sK25,sK20,X0) ),
inference(superposition,[status(thm)],[c_4308,c_51]) ).
tcf(c_6051,plain,
! [X0: $i] :
( coll(sK24,X0,sK26)
| ~ coll(sK26,sK21,X0) ),
inference(superposition,[status(thm)],[c_4307,c_51]) ).
tcf(c_6052,plain,
! [X0: $i] :
( coll(sK25,X0,sK26)
| ~ coll(sK26,sK22,X0) ),
inference(superposition,[status(thm)],[c_4306,c_51]) ).
tcf(c_6053,plain,
! [X0: $i] :
( coll(sK21,X0,sK23)
| ~ coll(sK23,sK22,X0) ),
inference(superposition,[status(thm)],[c_5852,c_51]) ).
tcf(c_6054,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK22,X0) ),
inference(superposition,[status(thm)],[c_5853,c_51]) ).
tcf(c_6056,plain,
! [X0: $i] :
( coll(sK21,X0,sK26)
| ~ coll(sK26,sK24,X0) ),
inference(superposition,[status(thm)],[c_5855,c_51]) ).
tcf(c_6058,plain,
! [X0: $i] :
( coll(sK22,X0,sK21)
| ~ coll(sK21,sK23,X0) ),
inference(superposition,[status(thm)],[c_5866,c_51]) ).
tcf(c_6059,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_5867,c_51]) ).
tcf(c_6061,plain,
! [X0: $i] :
( coll(sK24,X0,sK21)
| ~ coll(sK21,sK26,X0) ),
inference(superposition,[status(thm)],[c_5869,c_51]) ).
tcf(c_6063,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK23,X0) ),
inference(superposition,[status(thm)],[c_5871,c_51]) ).
tcf(c_6065,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK25,X0) ),
inference(superposition,[status(thm)],[c_5873,c_51]) ).
tcf(c_6067,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK26,X0) ),
inference(superposition,[status(thm)],[c_5875,c_51]) ).
tcf(c_6075,plain,
! [X0: $i] :
( coll(sK21,X0,sK27)
| ~ coll(sK27,sK22,X0) ),
inference(superposition,[status(thm)],[c_5901,c_51]) ).
tcf(c_6076,plain,
! [X0: $i] :
( coll(sK21,X0,sK28)
| ~ coll(sK28,sK24,X0) ),
inference(superposition,[status(thm)],[c_5902,c_51]) ).
tcf(c_6077,plain,
! [X0: $i] :
( coll(sK22,X0,sK29)
| ~ coll(sK29,sK25,X0) ),
inference(superposition,[status(thm)],[c_5903,c_51]) ).
tcf(c_6081,plain,
! [X0: $i] :
( coll(sK22,X0,sK27)
| ~ coll(sK27,sK21,X0) ),
inference(superposition,[status(thm)],[c_5920,c_51]) ).
tcf(c_6083,plain,
! [X0: $i] :
( coll(sK25,X0,sK29)
| ~ coll(sK29,sK22,X0) ),
inference(superposition,[status(thm)],[c_5924,c_51]) ).
tcf(c_6193,plain,
( coll(sK24,sK21,sK21)
| ~ coll(sK21,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_6061]) ).
tcf(c_6198,plain,
( coll(sK21,sK21,sK26)
| ~ coll(sK26,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_6056]) ).
tcf(c_6210,plain,
coll(sK22,sK25,sK29),
inference(superposition,[status(thm)],[c_6007,c_49]) ).
tcf(c_6214,plain,
! [X0: $i] :
( coll(sK27,X0,sK22)
| ~ coll(sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_6010,c_51]) ).
tcf(c_6224,plain,
! [X0: $i] :
( coll(sK28,X0,sK24)
| ~ coll(sK24,sK21,X0) ),
inference(superposition,[status(thm)],[c_6012,c_51]) ).
tcf(c_6229,plain,
! [X0: $i] :
( coll(sK29,X0,sK25)
| ~ coll(sK25,sK22,X0) ),
inference(superposition,[status(thm)],[c_6014,c_51]) ).
tcf(c_6239,plain,
coll(sK22,sK22,sK23),
inference(superposition,[status(thm)],[c_4312,c_6048]) ).
tcf(c_6240,plain,
! [X0: $i] :
( coll(sK23,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6239,c_51]) ).
tcf(c_6249,plain,
coll(sK22,sK22,sK24),
inference(superposition,[status(thm)],[c_4310,c_6049]) ).
tcf(c_6250,plain,
! [X0: $i] :
( coll(sK24,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6249,c_51]) ).
tcf(c_6265,plain,
coll(sK21,sK21,sK25),
inference(superposition,[status(thm)],[c_4308,c_6050]) ).
tcf(c_6266,plain,
! [X0: $i] :
( coll(sK25,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6265,c_51]) ).
tcf(c_6268,plain,
coll(sK21,sK25,sK21),
inference(superposition,[status(thm)],[c_6265,c_49]) ).
tcf(c_6276,plain,
coll(sK24,sK24,sK26),
inference(superposition,[status(thm)],[c_4307,c_6051]) ).
tcf(c_6277,plain,
! [X0: $i] :
( coll(sK26,X0,sK24)
| ~ coll(sK24,sK24,X0) ),
inference(superposition,[status(thm)],[c_6276,c_51]) ).
tcf(c_6282,plain,
! [X0: $i] :
( coll(sK27,X0,sK21)
| ~ coll(sK21,sK22,X0) ),
inference(superposition,[status(thm)],[c_6028,c_51]) ).
tcf(c_6307,plain,
! [X0: $i] :
( coll(sK28,X0,sK21)
| ~ coll(sK21,sK24,X0) ),
inference(superposition,[status(thm)],[c_6030,c_51]) ).
tcf(c_6313,plain,
! [X0: $i] :
( coll(sK29,X0,sK22)
| ~ coll(sK22,sK25,X0) ),
inference(superposition,[status(thm)],[c_6210,c_51]) ).
tcf(c_6345,plain,
( cong(sK27,sK22,sK27,sK21)
| ~ midp(sK27,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6346,plain,
( cong(sK28,sK24,sK28,sK21)
| ~ midp(sK28,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6348,plain,
! [X0: $i] :
( coll(sK21,X0,sK21)
| ~ coll(sK21,sK25,X0) ),
inference(superposition,[status(thm)],[c_6268,c_51]) ).
tcf(c_6349,plain,
coll(sK25,sK21,sK21),
inference(superposition,[status(thm)],[c_6268,c_50]) ).
tcf(c_6353,plain,
( coll(sK21,sK21,sK21)
| ~ coll(sK21,sK25,sK21) ),
inference(instantiation,[status(thm)],[c_6348]) ).
tcf(c_6373,plain,
coll(sK21,sK21,sK23),
inference(superposition,[status(thm)],[c_5852,c_6053]) ).
tcf(c_6376,plain,
coll(sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_6373,c_49]) ).
tcf(c_6458,plain,
coll(sK21,sK21,sK26),
inference(superposition,[status(thm)],[c_5855,c_6056]) ).
tcf(c_6464,plain,
! [X0: $i,X1: $i] :
( para(sK29,X0,sK22,X1)
| ~ midp(sK29,sK25,sK22)
| ~ midp(X0,sK25,X1) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_6468,plain,
coll(sK21,sK26,sK21),
inference(superposition,[status(thm)],[c_6458,c_49]) ).
tcf(c_6483,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK21,X1)
| ~ midp(sK27,sK22,sK21)
| ~ midp(sK27,X0,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_6493,plain,
coll(sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_5866,c_6058]) ).
tcf(c_6496,plain,
coll(sK22,sK21,sK22),
inference(superposition,[status(thm)],[c_6493,c_49]) ).
tcf(c_6504,plain,
coll(sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_5867,c_6059]) ).
tcf(c_6516,plain,
! [X0: $i,X1: $i] :
( para(sK27,X0,sK21,X1)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_4305,c_93]) ).
tcf(c_6517,plain,
! [X0: $i,X1: $i] :
( para(sK28,X0,sK21,X1)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_4304,c_93]) ).
tcf(c_6518,plain,
! [X0: $i,X1: $i] :
( para(sK29,X0,sK22,X1)
| ~ midp(X0,sK25,X1) ),
inference(superposition,[status(thm)],[c_4303,c_93]) ).
tcf(c_6519,plain,
! [X0: $i,X1: $i] :
( para(sK27,X0,sK22,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_5894,c_93]) ).
tcf(c_6520,plain,
! [X0: $i,X1: $i] :
( para(sK28,X0,sK24,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_5895,c_93]) ).
tcf(c_6521,plain,
! [X0: $i,X1: $i] :
( para(sK29,X0,sK25,X1)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_5896,c_93]) ).
tcf(c_6560,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK21,X1)
| ~ midp(sK27,X0,X1) ),
inference(superposition,[status(thm)],[c_4305,c_112]) ).
tcf(c_6561,plain,
! [X0: $i,X1: $i] :
( para(sK24,X0,sK21,X1)
| ~ midp(sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_4304,c_112]) ).
tcf(c_6562,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,sK22,X1)
| ~ midp(sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_4303,c_112]) ).
tcf(c_6563,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK22,X1)
| ~ midp(sK27,X0,X1) ),
inference(superposition,[status(thm)],[c_5894,c_112]) ).
tcf(c_6564,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK24,X1)
| ~ midp(sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_5895,c_112]) ).
tcf(c_6565,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK25,X1)
| ~ midp(sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_5896,c_112]) ).
tcf(c_6608,plain,
! [X0: $i] :
( coll(sK21,X0,sK21)
| ~ coll(sK21,sK23,X0) ),
inference(superposition,[status(thm)],[c_6376,c_51]) ).
tcf(c_6611,plain,
coll(sK22,sK21,sK21),
inference(superposition,[status(thm)],[c_6376,c_6058]) ).
tcf(c_6638,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,sK27,X0)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6516,c_53]) ).
tcf(c_6639,plain,
! [X0: $i,X1: $i] :
( para(sK27,X0,X1,sK21)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6516,c_52]) ).
tcf(c_6655,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,sK28,X0)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_6517,c_53]) ).
tcf(c_6785,plain,
( cong(sK25,sK20,sK25,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_4309,c_104]) ).
tcf(c_6786,plain,
( cong(sK23,sK22,sK23,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_5950,c_104]) ).
tcf(c_6790,plain,
( cong(sK20,sK24,sK20,sK21)
| ~ midp(sK22,sK24,sK21) ),
inference(superposition,[status(thm)],[c_5958,c_104]) ).
tcf(c_6832,plain,
! [X0: $i,X1: $i] :
( midp(sK27,X0,X1)
| ~ midp(sK27,sK22,sK21)
| ~ para(sK22,X1,sK21,X0)
| ~ para(sK22,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6833,plain,
( midp(sK27,sK21,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ para(sK22,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_6832]) ).
tcf(c_6834,plain,
! [X0: $i,X1: $i] :
( midp(sK28,X0,X1)
| ~ midp(sK28,sK24,sK21)
| ~ para(sK24,X1,sK21,X0)
| ~ para(sK24,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6835,plain,
( midp(sK28,sK21,sK21)
| ~ midp(sK28,sK24,sK21)
| ~ para(sK24,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_6834]) ).
tcf(c_6850,plain,
coll(sK24,sK21,sK21),
inference(superposition,[status(thm)],[c_6468,c_6061]) ).
tcf(c_6923,plain,
( cong(sK25,sK21,sK25,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6785,c_72]) ).
tcf(c_6975,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK29,X3,X1,X2)
| ~ midp(X3,sK25,X0)
| ~ para(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6518,c_54]) ).
tcf(c_6978,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK25,X3,X1,X2)
| ~ midp(sK29,X3,X0)
| ~ para(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6562,c_54]) ).
tcf(c_7017,plain,
! [X0: $i,X1: $i] :
( para(sK24,sK21,X0,X1)
| ~ perp(sK20,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_4311,c_57]) ).
tcf(c_7018,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK22,X0,X1)
| ~ perp(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_4309,c_57]) ).
tcf(c_7022,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK22,X0,X1)
| ~ perp(sK23,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_5957,c_57]) ).
tcf(c_7146,plain,
! [X0: $i] :
( circle(sK25,sK20,X0,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ cong(sK25,sK20,sK25,X0) ),
inference(superposition,[status(thm)],[c_6785,c_60]) ).
tcf(c_7166,plain,
coll(sK21,sK22,sK21),
inference(superposition,[status(thm)],[c_6611,c_50]) ).
tcf(c_7211,plain,
para(sK24,sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_5977,c_7017]) ).
tcf(c_7258,plain,
para(sK21,sK24,sK24,sK21),
inference(superposition,[status(thm)],[c_7211,c_53]) ).
tcf(c_7280,plain,
coll(sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_5871,c_6063]) ).
tcf(c_7355,plain,
coll(sK21,sK24,sK21),
inference(superposition,[status(thm)],[c_6850,c_50]) ).
tcf(c_7382,plain,
coll(sK21,sK21,sK27),
inference(superposition,[status(thm)],[c_5901,c_6075]) ).
tcf(c_7385,plain,
coll(sK21,sK27,sK21),
inference(superposition,[status(thm)],[c_7382,c_49]) ).
tcf(c_7396,plain,
coll(sK21,sK21,sK28),
inference(superposition,[status(thm)],[c_5902,c_6076]) ).
tcf(c_7397,plain,
! [X0: $i] :
( coll(sK28,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_7396,c_51]) ).
tcf(c_7399,plain,
coll(sK21,sK28,sK21),
inference(superposition,[status(thm)],[c_7396,c_49]) ).
tcf(c_7407,plain,
coll(sK22,sK22,sK29),
inference(superposition,[status(thm)],[c_5903,c_6077]) ).
tcf(c_7450,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK22,X1)
| ~ midp(sK27,sK22,sK21)
| ~ coll(X0,sK22,X1)
| ~ para(sK27,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_7451,plain,
( midp(sK21,sK22,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ coll(sK21,sK22,sK21)
| ~ para(sK27,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_7450]) ).
tcf(c_7452,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK24,X1)
| ~ midp(sK28,sK24,sK21)
| ~ coll(X0,sK24,X1)
| ~ para(sK28,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_7453,plain,
( midp(sK21,sK24,sK21)
| ~ midp(sK28,sK24,sK21)
| ~ coll(sK21,sK24,sK21)
| ~ para(sK28,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_7452]) ).
tcf(c_7454,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK25,X1)
| ~ midp(sK29,sK25,sK22)
| ~ coll(X0,sK25,X1)
| ~ para(sK29,X0,sK22,X1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_7535,plain,
coll(sK23,sK24,sK22),
inference(superposition,[status(thm)],[c_6249,c_6240]) ).
tcf(c_7537,plain,
coll(sK23,sK20,sK22),
inference(superposition,[status(thm)],[c_6504,c_6240]) ).
tcf(c_7538,plain,
coll(sK23,sK29,sK22),
inference(superposition,[status(thm)],[c_7407,c_6240]) ).
tcf(c_7588,plain,
coll(sK23,sK22,sK24),
inference(superposition,[status(thm)],[c_7535,c_49]) ).
tcf(c_7596,plain,
coll(sK24,sK21,sK22),
inference(superposition,[status(thm)],[c_6493,c_6250]) ).
tcf(c_7597,plain,
coll(sK24,sK24,sK22),
inference(superposition,[status(thm)],[c_6249,c_6250]) ).
tcf(c_7612,plain,
coll(sK25,sK27,sK21),
inference(superposition,[status(thm)],[c_7382,c_6266]) ).
tcf(c_7614,plain,
coll(sK25,sK26,sK21),
inference(superposition,[status(thm)],[c_6458,c_6266]) ).
tcf(c_7628,plain,
coll(sK26,sK22,sK24),
inference(superposition,[status(thm)],[c_7597,c_6277]) ).
tcf(c_7750,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK27,X3,X1,X2)
| ~ midp(X3,sK21,X0)
| ~ perp(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6519,c_58]) ).
tcf(c_7767,plain,
( perp(sK27,sK21,sK21,sK21)
| ~ midp(sK21,sK21,sK21)
| ~ perp(sK22,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_7750]) ).
tcf(c_7779,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK28,X3,X1,X2)
| ~ midp(X3,sK21,X0)
| ~ perp(sK24,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6520,c_58]) ).
tcf(c_7781,plain,
! [X0: $i,X1: $i] :
( para(sK24,X1,sK28,X0)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6520,c_53]) ).
tcf(c_7794,plain,
( para(sK24,sK21,sK28,sK21)
| ~ midp(sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_7781]) ).
tcf(c_7796,plain,
( perp(sK28,sK21,sK21,sK21)
| ~ midp(sK21,sK21,sK21)
| ~ perp(sK24,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_7779]) ).
tcf(c_7866,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,X1,sK24)
| ~ midp(sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_6564,c_52]) ).
tcf(c_8001,plain,
coll(sK25,sK22,sK21),
inference(superposition,[status(thm)],[c_7280,c_6266]) ).
tcf(c_8043,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,X0,sK27)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6638,c_52]) ).
tcf(c_8061,plain,
! [X0: $i,X1: $i] :
( para(X1,sK21,sK27,X0)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6639,c_53]) ).
tcf(c_8084,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,X0,sK28)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_6655,c_52]) ).
tcf(c_8099,plain,
! [X0: $i] :
( circle(sK27,sK22,X0,sK21)
| ~ cong(sK27,sK22,sK27,sK21)
| ~ cong(sK27,sK22,sK27,X0) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_8103,plain,
( circle(sK27,sK22,sK21,sK21)
| ~ cong(sK27,sK22,sK27,sK21) ),
inference(instantiation,[status(thm)],[c_8099]) ).
tcf(c_8372,plain,
! [X0: $i] :
( circle(sK28,sK24,X0,sK21)
| ~ cong(sK28,sK24,sK28,sK21)
| ~ cong(sK28,sK24,sK28,X0) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_8376,plain,
( circle(sK28,sK24,sK21,sK21)
| ~ cong(sK28,sK24,sK28,sK21) ),
inference(instantiation,[status(thm)],[c_8372]) ).
tcf(c_8433,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,X0,X0)
| ~ coll(X0,X0,X2)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_88,c_91]) ).
tcf(c_8446,plain,
( cyclic(sK21,sK21,sK21,sK21)
| ~ coll(sK21,sK21,sK21)
| ~ para(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_8433]) ).
tcf(c_8460,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK27,X1,sK21)
| ~ midp(X0,sK22,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6516,c_94]) ).
tcf(c_8461,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK28,X1,sK21)
| ~ midp(X0,sK24,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6517,c_94]) ).
tcf(c_8462,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK29,X1,sK22)
| ~ midp(X0,sK25,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6518,c_94]) ).
tcf(c_8466,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK27,X1,sK22)
| ~ midp(X0,sK21,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6519,c_94]) ).
tcf(c_8467,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK28,X1,sK24)
| ~ midp(X0,sK21,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6520,c_94]) ).
tcf(c_8468,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK29,X1,sK25)
| ~ midp(X0,sK22,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6521,c_94]) ).
tcf(c_8469,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK21,X1,sK22)
| ~ midp(sK27,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6563,c_94]) ).
tcf(c_8471,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK22,X1,sK25)
| ~ midp(sK29,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6565,c_94]) ).
tcf(c_8472,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK21,X1,sK27)
| ~ midp(X2,sK22,X0)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6638,c_94]) ).
tcf(c_8702,plain,
coll(sK27,sK21,sK21),
inference(superposition,[status(thm)],[c_7385,c_50]) ).
tcf(c_8904,plain,
( midp(sK23,sK22,sK21)
| ~ midp(sK20,sK22,sK21)
| ~ coll(sK23,sK22,sK21) ),
inference(superposition,[status(thm)],[c_6786,c_116]) ).
tcf(c_8912,plain,
( midp(sK23,sK22,sK21)
| ~ midp(sK20,sK22,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8904,c_5852]) ).
tcf(c_9244,plain,
( midp(sK20,sK24,sK21)
| ~ midp(sK22,sK24,sK21)
| ~ coll(sK20,sK24,sK21) ),
inference(superposition,[status(thm)],[c_6790,c_116]) ).
tcf(c_9489,plain,
coll(sK23,sK22,sK20),
inference(superposition,[status(thm)],[c_7537,c_49]) ).
tcf(c_9626,plain,
coll(sK29,sK23,sK22),
inference(superposition,[status(thm)],[c_7538,c_50]) ).
tcf(c_9627,plain,
coll(sK23,sK22,sK29),
inference(superposition,[status(thm)],[c_7538,c_49]) ).
tcf(c_9703,plain,
( para(sK29,sK29,sK22,sK22)
| ~ midp(sK29,sK25,sK22) ),
inference(instantiation,[status(thm)],[c_6464]) ).
tcf(c_9704,plain,
( para(sK22,sK22,sK21,sK21)
| ~ midp(sK27,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_6483]) ).
tcf(c_9711,plain,
( midp(sK25,sK21,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK25,sK21,sK20) ),
inference(superposition,[status(thm)],[c_6923,c_116]) ).
tcf(c_9718,plain,
( midp(sK25,sK21,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9711,c_5854]) ).
tcf(c_9872,plain,
coll(sK21,sK24,sK23),
inference(superposition,[status(thm)],[c_7588,c_6053]) ).
tcf(c_9881,plain,
coll(sK21,sK24,sK22),
inference(superposition,[status(thm)],[c_7596,c_50]) ).
tcf(c_9882,plain,
coll(sK24,sK22,sK21),
inference(superposition,[status(thm)],[c_7596,c_49]) ).
tcf(c_9925,plain,
para(sK21,sK22,sK21,sK22),
inference(superposition,[status(thm)],[c_4313,c_7022]) ).
tcf(c_10020,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X0)
| ~ midp(X2,sK24,sK21)
| ~ midp(sK28,X1,X0)
| ~ para(sK24,X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6561,c_113]) ).
tcf(c_10046,plain,
! [X0: $i] :
( midp(X0,sK22,sK22)
| ~ midp(X0,sK21,sK21)
| ~ para(sK21,sK22,sK21,sK22) ),
inference(superposition,[status(thm)],[c_9925,c_113]) ).
tcf(c_10059,plain,
! [X0: $i] :
( midp(X0,sK22,sK22)
| ~ midp(X0,sK21,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10046,c_9925]) ).
tcf(c_10341,plain,
coll(sK27,sK25,sK21),
inference(superposition,[status(thm)],[c_7612,c_50]) ).
tcf(c_10342,plain,
coll(sK25,sK21,sK27),
inference(superposition,[status(thm)],[c_7612,c_49]) ).
tcf(c_10354,plain,
coll(sK22,sK21,sK25),
inference(superposition,[status(thm)],[c_7614,c_6067]) ).
tcf(c_10682,plain,
coll(sK25,sK24,sK26),
inference(superposition,[status(thm)],[c_7628,c_6052]) ).
tcf(c_10702,plain,
coll(sK25,sK26,sK24),
inference(superposition,[status(thm)],[c_10682,c_49]) ).
tcf(c_10872,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK29,X0,sK21,X2)
| ~ midp(sK27,X1,X2)
| ~ midp(X0,sK25,X1) ),
inference(superposition,[status(thm)],[c_6560,c_6975]) ).
tcf(c_10907,plain,
! [X0: $i] :
( para(sK29,sK29,sK21,X0)
| ~ midp(sK27,sK22,X0) ),
inference(superposition,[status(thm)],[c_4303,c_10872]) ).
tcf(c_10914,plain,
( para(sK29,sK29,sK21,sK21)
| ~ midp(sK27,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_10907]) ).
tcf(c_11160,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK29,sK29,X1,X2)
| ~ midp(sK27,sK22,X0)
| ~ perp(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_10907,c_58]) ).
tcf(c_11161,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK29,sK29,X1,X2)
| ~ midp(sK27,sK22,X0)
| ~ para(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_10907,c_54]) ).
tcf(c_11162,plain,
! [X0: $i] :
( para(sK21,X0,sK29,sK29)
| ~ midp(sK27,sK22,X0) ),
inference(superposition,[status(thm)],[c_10907,c_53]) ).
tcf(c_11225,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK21,X2,X0,X1)
| ~ midp(sK27,sK22,X2)
| ~ para(sK29,sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_11162,c_54]) ).
tcf(c_11252,plain,
( para(sK21,sK21,sK21,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ para(sK29,sK29,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_11225]) ).
tcf(c_11420,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK25,X0,sK21,X2)
| ~ midp(sK27,X1,X2)
| ~ midp(sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_6560,c_6978]) ).
tcf(c_11659,plain,
! [X0: $i,X1: $i] :
( para(sK29,sK29,X0,X1)
| ~ para(sK29,sK29,sK22,sK22)
| ~ para(sK22,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_11744,plain,
coll(sK22,sK25,sK21),
inference(superposition,[status(thm)],[c_8001,c_50]) ).
tcf(c_11745,plain,
coll(sK25,sK21,sK22),
inference(superposition,[status(thm)],[c_8001,c_49]) ).
tcf(c_11755,plain,
! [X0: $i,X1: $i] :
( perp(sK22,sK22,X0,X1)
| ~ para(sK22,sK22,sK21,sK21)
| ~ perp(sK21,sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_11757,plain,
( perp(sK22,sK22,sK21,sK21)
| ~ perp(sK21,sK21,sK21,sK21)
| ~ para(sK22,sK22,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_11755]) ).
tcf(c_11773,plain,
! [X0: $i] :
( para(sK25,sK25,sK21,X0)
| ~ midp(sK27,sK22,X0) ),
inference(superposition,[status(thm)],[c_4303,c_11420]) ).
tcf(c_11788,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK25,sK25,X1,X2)
| ~ midp(sK27,sK22,X0)
| ~ para(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_11773,c_54]) ).
tcf(c_13626,plain,
coll(sK22,sK23,sK20),
inference(superposition,[status(thm)],[c_9489,c_50]) ).
tcf(c_13628,plain,
coll(sK21,sK20,sK23),
inference(superposition,[status(thm)],[c_9489,c_6053]) ).
tcf(c_13632,plain,
! [X0: $i] :
( coll(sK22,X0,sK29)
| ~ coll(sK29,sK23,X0) ),
inference(superposition,[status(thm)],[c_9626,c_51]) ).
tcf(c_13637,plain,
( coll(sK22,sK21,sK29)
| ~ coll(sK29,sK23,sK21) ),
inference(instantiation,[status(thm)],[c_13632]) ).
tcf(c_14235,plain,
coll(sK22,sK23,sK29),
inference(superposition,[status(thm)],[c_9627,c_50]) ).
tcf(c_14237,plain,
coll(sK21,sK29,sK23),
inference(superposition,[status(thm)],[c_9627,c_6053]) ).
tcf(c_14307,plain,
( circle(sK25,sK20,sK21,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6785,c_7146]) ).
tcf(c_14327,plain,
( perp(sK20,sK21,sK21,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK25,sK20,sK21) ),
inference(superposition,[status(thm)],[c_14307,c_102]) ).
tcf(c_14328,plain,
( perp(sK20,sK21,sK21,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14327,c_4308]) ).
tcf(c_14337,plain,
( perp(sK21,sK21,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_14328,c_56]) ).
tcf(c_15152,plain,
coll(sK24,sK21,sK23),
inference(superposition,[status(thm)],[c_9872,c_50]) ).
tcf(c_15300,plain,
( perp(sK29,sK29,sK20,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_14337,c_11160]) ).
tcf(c_15307,plain,
( perp(sK29,sK29,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15300,c_4305]) ).
tcf(c_15329,plain,
( perp(sK20,sK21,sK29,sK29)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_15307,c_56]) ).
tcf(c_15421,plain,
( para(sK25,sK22,sK29,sK29)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_15329,c_7018]) ).
tcf(c_15912,plain,
coll(sK22,sK24,sK21),
inference(superposition,[status(thm)],[c_9882,c_50]) ).
tcf(c_15914,plain,
coll(sK20,sK21,sK24),
inference(superposition,[status(thm)],[c_9882,c_6054]) ).
tcf(c_15941,plain,
! [X0: $i] :
( midp(sK22,X0,sK29)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,X0,sK29)
| ~ coll(sK22,X0,sK29) ),
inference(superposition,[status(thm)],[c_15421,c_94]) ).
tcf(c_15963,plain,
( midp(sK22,sK21,sK29)
| ~ midp(sK25,sK21,sK29)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK22,sK21,sK29) ),
inference(instantiation,[status(thm)],[c_15941]) ).
tcf(c_16557,plain,
! [X0: $i,X1: $i] :
( para(sK24,X0,X1,sK28)
| ~ para(sK24,X0,sK28,X1) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_16558,plain,
( para(sK24,sK21,sK21,sK28)
| ~ para(sK24,sK21,sK28,sK21) ),
inference(instantiation,[status(thm)],[c_16557]) ).
tcf(c_16820,plain,
coll(sK27,sK21,sK25),
inference(superposition,[status(thm)],[c_10341,c_49]) ).
tcf(c_16906,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK22,X1)
| ~ midp(X0,X1,sK22) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_16912,plain,
! [X0: $i,X1: $i] :
( midp(sK27,X1,X0)
| ~ midp(sK27,X0,X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_16913,plain,
! [X0: $i,X1: $i] :
( midp(sK28,X1,X0)
| ~ midp(sK28,X0,X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_16915,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK20,X1)
| ~ midp(X0,X1,sK20) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_17160,plain,
coll(sK22,sK24,sK25),
inference(superposition,[status(thm)],[c_10702,c_6067]) ).
tcf(c_18504,plain,
coll(sK21,sK25,sK22),
inference(superposition,[status(thm)],[c_11745,c_50]) ).
tcf(c_18744,plain,
( midp(sK21,sK28,sK21)
| ~ midp(sK21,sK24,sK21)
| ~ midp(sK28,sK28,sK21) ),
inference(superposition,[status(thm)],[c_7399,c_8461]) ).
tcf(c_19543,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK24,X0,sK21,X2)
| ~ midp(sK24,X1,sK21)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_20213,plain,
coll(sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_13626,c_6063]) ).
tcf(c_20311,plain,
coll(sK27,sK25,sK22),
inference(superposition,[status(thm)],[c_10354,c_6214]) ).
tcf(c_20312,plain,
coll(sK27,sK22,sK22),
inference(superposition,[status(thm)],[c_6496,c_6214]) ).
tcf(c_20364,plain,
coll(sK21,sK29,sK22),
inference(superposition,[status(thm)],[c_14235,c_6063]) ).
tcf(c_20412,plain,
coll(sK21,sK23,sK20),
inference(superposition,[status(thm)],[c_13628,c_49]) ).
tcf(c_20465,plain,
coll(sK29,sK21,sK23),
inference(superposition,[status(thm)],[c_14237,c_50]) ).
tcf(c_20466,plain,
coll(sK21,sK23,sK29),
inference(superposition,[status(thm)],[c_14237,c_49]) ).
tcf(c_22092,plain,
coll(sK28,sK22,sK24),
inference(superposition,[status(thm)],[c_7596,c_6224]) ).
tcf(c_22110,plain,
coll(sK28,sK23,sK24),
inference(superposition,[status(thm)],[c_15152,c_6224]) ).
tcf(c_22330,plain,
coll(sK29,sK21,sK25),
inference(superposition,[status(thm)],[c_8001,c_6229]) ).
tcf(c_22493,plain,
coll(sK20,sK24,sK21),
inference(superposition,[status(thm)],[c_15914,c_49]) ).
tcf(c_22832,plain,
coll(sK22,sK25,sK27),
inference(superposition,[status(thm)],[c_16820,c_6081]) ).
tcf(c_23996,plain,
! [X0: $i,X1: $i] :
( perp(sK22,X1,X1,sK21)
| ~ coll(X0,sK22,sK21)
| ~ circle(X0,sK22,X1,sK21) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_23998,plain,
! [X0: $i,X1: $i] :
( perp(sK24,X1,X1,sK21)
| ~ coll(X0,sK24,sK21)
| ~ circle(X0,sK24,X1,sK21) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_24569,plain,
coll(sK28,sK22,sK21),
inference(superposition,[status(thm)],[c_9881,c_6307]) ).
tcf(c_24761,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK27,X3,sK21,X2)
| ~ perp(sK27,X3,X0,X1)
| ~ perp(X0,X1,sK21,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_24762,plain,
( para(sK27,sK21,sK21,sK21)
| ~ perp(sK27,sK21,sK21,sK21)
| ~ perp(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_24761]) ).
tcf(c_24763,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK28,X3,sK21,X2)
| ~ perp(sK28,X3,X0,X1)
| ~ perp(X0,X1,sK21,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_24764,plain,
( para(sK28,sK21,sK21,sK21)
| ~ perp(sK21,sK21,sK21,sK21)
| ~ perp(sK28,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_24763]) ).
tcf(c_24767,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK22,X3,sK21,X2)
| ~ perp(sK22,X3,X0,X1)
| ~ perp(X0,X1,sK21,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_24768,plain,
( para(sK22,sK21,sK21,sK21)
| ~ perp(sK22,sK21,sK21,sK21)
| ~ perp(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_24767]) ).
tcf(c_24769,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK24,X3,sK21,X2)
| ~ perp(sK24,X3,X0,X1)
| ~ perp(X0,X1,sK21,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_24770,plain,
( para(sK24,sK21,sK21,sK21)
| ~ perp(sK24,sK21,sK21,sK21)
| ~ perp(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_24769]) ).
tcf(c_24791,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK21,sK24,X2,X3)
| ~ perp(sK21,sK24,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_24792,plain,
( para(sK21,sK24,sK21,sK21)
| ~ perp(sK21,sK24,sK21,sK21)
| ~ perp(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_24791]) ).
tcf(c_24944,plain,
coll(sK29,sK21,sK22),
inference(superposition,[status(thm)],[c_11744,c_6313]) ).
tcf(c_25466,plain,
coll(sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_18504,c_6065]) ).
tcf(c_26840,plain,
! [X0: $i] :
( cyclic(sK28,sK29,sK26,sK23)
| ~ cyclic(X0,sK28,sK29,sK23)
| ~ cyclic(X0,sK28,sK29,sK26) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_26841,plain,
( cyclic(sK28,sK29,sK26,sK23)
| ~ cyclic(sK21,sK28,sK29,sK23)
| ~ cyclic(sK21,sK28,sK29,sK26) ),
inference(instantiation,[status(thm)],[c_26840]) ).
tcf(c_28519,plain,
coll(sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_20213,c_49]) ).
tcf(c_28582,plain,
coll(sK27,sK22,sK25),
inference(superposition,[status(thm)],[c_20311,c_49]) ).
tcf(c_28844,plain,
coll(sK22,sK20,sK21),
inference(superposition,[status(thm)],[c_20412,c_6058]) ).
tcf(c_28957,plain,
coll(sK21,sK22,sK29),
inference(superposition,[status(thm)],[c_20364,c_49]) ).
tcf(c_29021,plain,
coll(sK29,sK23,sK21),
inference(superposition,[status(thm)],[c_20465,c_49]) ).
tcf(c_31576,plain,
coll(sK28,sK24,sK22),
inference(superposition,[status(thm)],[c_22092,c_49]) ).
tcf(c_31651,plain,
coll(sK28,sK24,sK23),
inference(superposition,[status(thm)],[c_22110,c_49]) ).
tcf(c_32457,plain,
coll(sK29,sK25,sK21),
inference(superposition,[status(thm)],[c_22330,c_49]) ).
tcf(c_34618,plain,
! [X0: $i] :
( para(sK29,sK29,sK22,X0)
| ~ para(sK29,sK29,sK22,sK22)
| ~ para(sK22,sK22,sK22,X0) ),
inference(instantiation,[status(thm)],[c_11659]) ).
tcf(c_34619,plain,
! [X0: $i] :
( midp(sK29,sK25,X0)
| ~ midp(sK29,sK25,sK22)
| ~ coll(sK29,sK25,X0)
| ~ para(sK29,sK29,sK22,X0) ),
inference(instantiation,[status(thm)],[c_7454]) ).
tcf(c_34620,plain,
( para(sK29,sK29,sK22,sK21)
| ~ para(sK22,sK22,sK22,sK21)
| ~ para(sK29,sK29,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_34618]) ).
tcf(c_34621,plain,
( midp(sK29,sK25,sK21)
| ~ midp(sK29,sK25,sK22)
| ~ coll(sK29,sK25,sK21)
| ~ para(sK29,sK29,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_34619]) ).
tcf(c_34732,plain,
coll(sK25,sK22,sK27),
inference(superposition,[status(thm)],[c_22832,c_50]) ).
tcf(c_34734,plain,
coll(sK29,sK27,sK22),
inference(superposition,[status(thm)],[c_22832,c_6313]) ).
tcf(c_35051,plain,
! [X0: $i,X1: $i] :
( cyclic(X1,sK28,sK29,sK26)
| ~ cyclic(X0,X1,sK28,sK26)
| ~ cyclic(X0,X1,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_35052,plain,
( cyclic(sK21,sK28,sK29,sK26)
| ~ cyclic(sK21,sK21,sK28,sK26)
| ~ cyclic(sK21,sK21,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_35051]) ).
tcf(c_35380,plain,
coll(sK29,sK22,sK21),
inference(superposition,[status(thm)],[c_24944,c_49]) ).
tcf(c_35474,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X0)
| ~ midp(X2,sK24,sK21)
| ~ midp(sK28,X1,X0)
| ~ midp(sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_6561,c_10020]) ).
tcf(c_35492,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X0)
| ~ midp(X2,sK24,sK21)
| ~ midp(sK28,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_35474,c_16913,c_35474]) ).
tcf(c_37645,plain,
( midp(sK20,sK22,sK21)
| ~ midp(sK20,sK24,sK21)
| ~ midp(sK28,sK22,sK21) ),
inference(superposition,[status(thm)],[c_25466,c_8461]) ).
tcf(c_39533,plain,
coll(sK21,sK29,sK21),
inference(superposition,[status(thm)],[c_20466,c_6608]) ).
tcf(c_39698,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK22,sK22,sK22,X2)
| ~ perp(sK22,sK22,X0,X1)
| ~ perp(X0,X1,sK22,X2) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_39703,plain,
( para(sK22,sK22,sK22,sK21)
| ~ perp(sK22,sK22,sK21,sK21)
| ~ perp(sK21,sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_39698]) ).
tcf(c_40953,plain,
coll(sK27,sK29,sK21),
inference(superposition,[status(thm)],[c_28957,c_6282]) ).
tcf(c_42675,plain,
coll(sK21,sK22,sK28),
inference(superposition,[status(thm)],[c_31576,c_6076]) ).
tcf(c_42783,plain,
coll(sK21,sK23,sK28),
inference(superposition,[status(thm)],[c_31651,c_6076]) ).
tcf(c_44065,plain,
coll(sK21,sK28,sK23),
inference(superposition,[status(thm)],[c_42783,c_49]) ).
tcf(c_44954,plain,
! [X0: $i] :
( midp(sK24,X0,sK21)
| ~ midp(sK21,X0,sK24)
| ~ coll(sK24,X0,sK21) ),
inference(superposition,[status(thm)],[c_7258,c_94]) ).
tcf(c_44955,plain,
! [X0: $i,X1: $i] :
( perp(sK21,sK24,X0,X1)
| ~ perp(sK24,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_7258,c_58]) ).
tcf(c_44991,plain,
( perp(sK21,sK24,sK21,sK21)
| ~ perp(sK24,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_44955]) ).
tcf(c_44992,plain,
( midp(sK24,sK21,sK21)
| ~ midp(sK21,sK21,sK24)
| ~ coll(sK24,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_44954]) ).
tcf(c_46697,plain,
coll(sK29,sK22,sK27),
inference(superposition,[status(thm)],[c_34734,c_49]) ).
tcf(c_47658,plain,
coll(sK25,sK21,sK29),
inference(superposition,[status(thm)],[c_35380,c_6083]) ).
tcf(c_49063,plain,
( cong(sK25,sK20,sK25,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_4309,c_104]) ).
tcf(c_49400,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cong(X0,X4,X2,X3)
| ~ midp(X0,X4,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_117,c_73]) ).
tcf(c_49500,plain,
! [X0: $i] :
( cong(sK25,X0,sK25,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,X0,sK20) ),
inference(superposition,[status(thm)],[c_49063,c_49400]) ).
tcf(c_55180,plain,
coll(sK29,sK21,sK21),
inference(superposition,[status(thm)],[c_39533,c_50]) ).
tcf(c_55181,plain,
coll(sK21,sK21,sK29),
inference(superposition,[status(thm)],[c_39533,c_49]) ).
tcf(c_55520,plain,
coll(sK29,sK27,sK21),
inference(superposition,[status(thm)],[c_40953,c_50]) ).
tcf(c_55521,plain,
coll(sK27,sK21,sK29),
inference(superposition,[status(thm)],[c_40953,c_49]) ).
tcf(c_56551,plain,
( perp(sK21,sK21,sK22,sK21)
| ~ perp(sK22,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_57922,plain,
( midp(sK21,sK28,sK23)
| ~ midp(sK21,sK24,sK23)
| ~ midp(sK28,sK28,sK21) ),
inference(superposition,[status(thm)],[c_44065,c_8461]) ).
tcf(c_60910,plain,
( midp(sK25,sK21,sK29)
| ~ midp(sK27,sK21,sK21)
| ~ midp(sK25,sK22,sK29) ),
inference(superposition,[status(thm)],[c_47658,c_8460]) ).
tcf(c_61012,plain,
( midp(sK29,sK21,sK21)
| ~ midp(sK29,sK25,sK21)
| ~ midp(sK29,sK21,sK22) ),
inference(superposition,[status(thm)],[c_55180,c_8462]) ).
tcf(c_61433,plain,
coll(sK28,sK29,sK21),
inference(superposition,[status(thm)],[c_55181,c_7397]) ).
tcf(c_61737,plain,
coll(sK29,sK21,sK27),
inference(superposition,[status(thm)],[c_55520,c_49]) ).
tcf(c_62062,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,sK24)
| ~ midp(sK28,X1,X0)
| ~ midp(X2,sK21,X0)
| ~ para(sK21,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_7866,c_113]) ).
tcf(c_62119,plain,
( midp(sK21,sK21,sK24)
| ~ midp(sK21,sK21,sK21)
| ~ midp(sK28,sK21,sK21)
| ~ para(sK21,sK24,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_62062]) ).
tcf(c_62194,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,sK27)
| ~ midp(X2,sK21,X0)
| ~ midp(X0,sK22,X1)
| ~ para(sK21,sK27,X0,X1) ),
inference(superposition,[status(thm)],[c_8043,c_113]) ).
tcf(c_62198,plain,
! [X0: $i,X1: $i] :
( para(X0,sK27,sK21,X1)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_8043,c_53]) ).
tcf(c_62243,plain,
( para(sK21,sK27,sK21,sK21)
| ~ midp(sK21,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_62198]) ).
tcf(c_62253,plain,
( midp(sK21,sK21,sK27)
| ~ midp(sK21,sK22,sK21)
| ~ midp(sK21,sK21,sK21)
| ~ para(sK21,sK27,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_62194]) ).
tcf(c_62315,plain,
! [X0: $i] :
( para(sK25,sK25,sK27,X0)
| ~ midp(sK27,sK22,sK21)
| ~ midp(X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8061,c_11788]) ).
tcf(c_62316,plain,
! [X0: $i] :
( para(sK29,sK29,sK27,X0)
| ~ midp(sK27,sK22,sK21)
| ~ midp(X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8061,c_11161]) ).
tcf(c_62345,plain,
! [X0: $i] :
( para(sK29,sK29,sK27,X0)
| ~ midp(X0,sK22,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_62316,c_4305]) ).
tcf(c_62348,plain,
! [X0: $i] :
( para(sK25,sK25,sK27,X0)
| ~ midp(X0,sK22,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_62315,c_4305]) ).
tcf(c_62429,plain,
! [X0: $i,X1: $i] :
( midp(sK29,X0,X1)
| ~ midp(sK29,X0,sK27)
| ~ midp(X1,sK22,sK21)
| ~ coll(sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_62345,c_94]) ).
tcf(c_62433,plain,
! [X0: $i] :
( para(sK29,sK29,X0,sK27)
| ~ midp(X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_62345,c_52]) ).
tcf(c_62941,plain,
! [X0: $i] :
( para(sK25,sK25,X0,sK27)
| ~ midp(X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_62348,c_52]) ).
tcf(c_62967,plain,
! [X0: $i,X1: $i] :
( midp(sK29,X0,sK27)
| ~ midp(X1,sK22,sK21)
| ~ coll(sK29,X0,sK27)
| ~ midp(sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_62433,c_94]) ).
tcf(c_63000,plain,
( midp(sK29,sK21,sK27)
| ~ midp(sK21,sK22,sK21)
| ~ midp(sK29,sK21,sK21)
| ~ coll(sK29,sK21,sK27) ),
inference(instantiation,[status(thm)],[c_62967]) ).
tcf(c_63007,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X0,sK27)
| ~ midp(X1,sK22,sK21)
| ~ coll(sK25,X0,sK27)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_62941,c_94]) ).
tcf(c_63033,plain,
( midp(sK25,sK21,sK27)
| ~ midp(sK25,sK21,sK21)
| ~ midp(sK21,sK22,sK21)
| ~ coll(sK25,sK21,sK27) ),
inference(instantiation,[status(thm)],[c_63007]) ).
tcf(c_63884,plain,
( midp(sK29,sK21,sK23)
| ~ midp(sK23,sK22,sK21)
| ~ midp(sK29,sK21,sK27) ),
inference(superposition,[status(thm)],[c_20465,c_62429]) ).
tcf(c_65785,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,sK28)
| ~ midp(X2,sK21,X0)
| ~ midp(X0,sK24,X1)
| ~ para(sK21,sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_8084,c_113]) ).
tcf(c_65789,plain,
! [X0: $i,X1: $i] :
( para(X0,sK28,sK21,X1)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_8084,c_53]) ).
tcf(c_65834,plain,
( para(sK21,sK28,sK21,sK21)
| ~ midp(sK21,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_65789]) ).
tcf(c_65844,plain,
( midp(sK21,sK21,sK28)
| ~ midp(sK21,sK24,sK21)
| ~ midp(sK21,sK21,sK21)
| ~ para(sK21,sK28,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_65785]) ).
tcf(c_66419,plain,
coll(sK29,sK28,sK21),
inference(superposition,[status(thm)],[c_61433,c_50]) ).
tcf(c_67628,plain,
! [X0: $i] :
( cong(X0,sK28,X0,sK29)
| ~ midp(X0,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_67629,plain,
( cong(sK21,sK28,sK21,sK29)
| ~ midp(sK21,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_67628]) ).
tcf(c_69695,plain,
( midp(sK22,sK22,sK29)
| ~ midp(sK27,sK22,sK22)
| ~ midp(sK22,sK21,sK29) ),
inference(superposition,[status(thm)],[c_7407,c_8466]) ).
tcf(c_69911,plain,
( midp(sK28,sK22,sK24)
| ~ midp(sK27,sK22,sK22)
| ~ midp(sK28,sK21,sK24) ),
inference(superposition,[status(thm)],[c_22092,c_8466]) ).
tcf(c_71048,plain,
( midp(sK28,sK22,sK24)
| ~ midp(sK27,sK22,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_69911,c_5895]) ).
tcf(c_73740,plain,
( midp(sK21,sK22,sK27)
| ~ midp(sK21,sK21,sK27)
| ~ midp(sK28,sK22,sK24) ),
inference(superposition,[status(thm)],[c_6028,c_8467]) ).
tcf(c_74044,plain,
( midp(sK27,sK22,sK22)
| ~ midp(sK27,sK21,sK22)
| ~ midp(sK28,sK22,sK24) ),
inference(superposition,[status(thm)],[c_20312,c_8467]) ).
tcf(c_74093,plain,
( midp(sK28,sK22,sK21)
| ~ midp(sK28,sK22,sK24)
| ~ midp(sK28,sK21,sK21) ),
inference(superposition,[status(thm)],[c_24569,c_8467]) ).
tcf(c_74193,plain,
( midp(sK25,sK22,sK27)
| ~ midp(sK25,sK21,sK27)
| ~ midp(sK28,sK22,sK24) ),
inference(superposition,[status(thm)],[c_34732,c_8467]) ).
tcf(c_74245,plain,
( midp(sK21,sK22,sK28)
| ~ midp(sK21,sK21,sK28)
| ~ midp(sK28,sK22,sK24) ),
inference(superposition,[status(thm)],[c_42675,c_8467]) ).
tcf(c_74283,plain,
( midp(sK29,sK22,sK27)
| ~ midp(sK29,sK21,sK27)
| ~ midp(sK28,sK22,sK24) ),
inference(superposition,[status(thm)],[c_46697,c_8467]) ).
tcf(c_75245,plain,
( midp(sK27,sK22,sK22)
| ~ midp(sK28,sK22,sK24) ),
inference(forward_subsumption_resolution,[status(thm)],[c_74044,c_5894]) ).
tcf(c_76458,plain,
! [X0: $i] :
( perp(sK22,X0,X0,sK21)
| ~ coll(sK27,sK22,sK21)
| ~ circle(sK27,sK22,X0,sK21) ),
inference(instantiation,[status(thm)],[c_23996]) ).
tcf(c_76459,plain,
( perp(sK22,sK21,sK21,sK21)
| ~ coll(sK27,sK22,sK21)
| ~ circle(sK27,sK22,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_76458]) ).
tcf(c_76471,plain,
! [X0: $i] :
( perp(sK24,X0,X0,sK21)
| ~ coll(sK28,sK24,sK21)
| ~ circle(sK28,sK24,X0,sK21) ),
inference(instantiation,[status(thm)],[c_23998]) ).
tcf(c_76472,plain,
( perp(sK24,sK21,sK21,sK21)
| ~ coll(sK28,sK24,sK21)
| ~ circle(sK28,sK24,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_76471]) ).
tcf(c_76681,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,sK28,sK29)
| ~ cong(X0,X1,X0,sK29)
| ~ cong(X0,X1,X0,sK28)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_76682,plain,
( cyclic(sK21,sK21,sK28,sK29)
| ~ cong(sK21,sK21,sK21,sK21)
| ~ cong(sK21,sK21,sK21,sK29)
| ~ cong(sK21,sK21,sK21,sK28) ),
inference(instantiation,[status(thm)],[c_76681]) ).
tcf(c_78187,plain,
! [X0: $i] :
( midp(X0,sK20,sK22)
| ~ midp(X0,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_16915]) ).
tcf(c_78189,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK21,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_78187]) ).
tcf(c_78201,plain,
coll(sK29,sK21,sK28),
inference(superposition,[status(thm)],[c_66419,c_49]) ).
tcf(c_78476,plain,
( midp(sK27,sK21,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ midp(sK29,sK21,sK25) ),
inference(superposition,[status(thm)],[c_8702,c_8468]) ).
tcf(c_80642,plain,
( midp(sK27,sK21,sK21)
| ~ midp(sK29,sK21,sK25) ),
inference(forward_subsumption_resolution,[status(thm)],[c_78476,c_4305]) ).
tcf(c_82131,plain,
! [X0: $i] :
( midp(sK29,sK22,X0)
| ~ midp(sK29,X0,sK22) ),
inference(instantiation,[status(thm)],[c_16906]) ).
tcf(c_82133,plain,
( midp(sK29,sK22,sK21)
| ~ midp(sK29,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_82131]) ).
tcf(c_82386,plain,
! [X0: $i] :
( midp(X0,sK28,sK29)
| ~ midp(X0,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_82387,plain,
( midp(sK21,sK28,sK29)
| ~ midp(sK21,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_82386]) ).
tcf(c_82522,plain,
! [X0: $i] :
( midp(sK28,sK28,X0)
| ~ midp(sK28,sK24,sK21)
| ~ para(sK24,sK28,sK21,X0)
| ~ para(sK24,X0,sK21,sK28) ),
inference(instantiation,[status(thm)],[c_6834]) ).
tcf(c_82523,plain,
( midp(sK28,sK28,sK21)
| ~ midp(sK28,sK24,sK21)
| ~ para(sK24,sK21,sK21,sK28)
| ~ para(sK24,sK28,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_82522]) ).
tcf(c_84345,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_28844,c_8469]) ).
tcf(c_84358,plain,
( midp(sK22,sK24,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ midp(sK21,sK24,sK22) ),
inference(superposition,[status(thm)],[c_15912,c_8469]) ).
tcf(c_84592,plain,
( midp(sK22,sK24,sK25)
| ~ midp(sK27,sK22,sK25)
| ~ midp(sK21,sK24,sK22) ),
inference(superposition,[status(thm)],[c_17160,c_8469]) ).
tcf(c_86666,plain,
( midp(sK22,sK24,sK21)
| ~ midp(sK21,sK24,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_84358,c_4305]) ).
tcf(c_86705,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_84345,c_4305]) ).
tcf(c_89723,plain,
midp(sK27,sK21,sK21),
inference(global_subsumption_just,[status(thm)],[c_80642,c_171,c_183,c_188,c_237,c_5901,c_6268,c_6345,c_6353,c_6833,c_8103,c_8446,c_10914,c_11252,c_24768,c_76459]) ).
tcf(c_89746,plain,
midp(sK27,sK22,sK22),
inference(superposition,[status(thm)],[c_89723,c_10059]) ).
tcf(c_89753,plain,
midp(sK28,sK22,sK24),
inference(backward_subsumption_resolution,[status(thm)],[c_71048,c_89746]) ).
tcf(c_96753,plain,
coll(sK21,sK29,sK28),
inference(superposition,[status(thm)],[c_78201,c_50]) ).
tcf(c_97840,plain,
( midp(sK21,sK24,sK23)
| ~ midp(sK22,sK24,sK25)
| ~ midp(sK29,sK21,sK23) ),
inference(superposition,[status(thm)],[c_9872,c_8471]) ).
tcf(c_101413,plain,
! [X0: $i] :
( midp(sK27,sK29,X0)
| ~ midp(sK27,X0,sK29) ),
inference(instantiation,[status(thm)],[c_16912]) ).
tcf(c_101414,plain,
( midp(sK27,sK29,sK21)
| ~ midp(sK27,sK21,sK29) ),
inference(instantiation,[status(thm)],[c_101413]) ).
tcf(c_102544,plain,
! [X0: $i] :
( midp(sK25,X0,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,X0,sK20)
| ~ coll(sK25,X0,sK21) ),
inference(superposition,[status(thm)],[c_49500,c_116]) ).
tcf(c_102629,plain,
( midp(sK25,sK21,sK21)
| ~ midp(sK25,sK21,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK25,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_102544]) ).
tcf(c_103746,plain,
( midp(sK25,sK22,sK29)
| ~ midp(sK21,sK22,sK27)
| ~ midp(sK29,sK22,sK25) ),
inference(superposition,[status(thm)],[c_6014,c_8472]) ).
tcf(c_103813,plain,
( midp(sK29,sK21,sK22)
| ~ midp(sK22,sK22,sK29)
| ~ midp(sK21,sK21,sK27) ),
inference(superposition,[status(thm)],[c_24944,c_8472]) ).
tcf(c_103943,plain,
( midp(sK21,sK21,sK29)
| ~ midp(sK21,sK21,sK27)
| ~ midp(sK29,sK22,sK21) ),
inference(superposition,[status(thm)],[c_55181,c_8472]) ).
tcf(c_104143,plain,
( midp(sK21,sK22,sK20)
| ~ midp(sK21,sK22,sK27)
| ~ midp(sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_28519,c_8472]) ).
tcf(c_104146,plain,
( midp(sK27,sK22,sK25)
| ~ midp(sK25,sK22,sK27)
| ~ midp(sK21,sK22,sK27) ),
inference(superposition,[status(thm)],[c_28582,c_8472]) ).
tcf(c_104306,plain,
( midp(sK27,sK21,sK29)
| ~ midp(sK21,sK21,sK27)
| ~ midp(sK29,sK22,sK27) ),
inference(superposition,[status(thm)],[c_55521,c_8472]) ).
tcf(c_106248,plain,
( midp(sK25,sK22,sK29)
| ~ midp(sK21,sK22,sK27) ),
inference(forward_subsumption_resolution,[status(thm)],[c_103746,c_5896]) ).
tcf(c_109484,plain,
( midp(sK21,sK29,sK28)
| ~ midp(sK27,sK29,sK21)
| ~ midp(sK21,sK22,sK28) ),
inference(superposition,[status(thm)],[c_96753,c_8460]) ).
tcf(c_110306,plain,
! [X0: $i] :
( midp(X0,sK24,sK22)
| ~ midp(X0,sK24,sK21) ),
inference(superposition,[status(thm)],[c_89753,c_35492]) ).
tcf(c_110324,plain,
( midp(sK21,sK24,sK22)
| ~ midp(sK21,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_110306]) ).
tcf(c_120691,plain,
! [X0: $i,X1: $i] :
( para(sK24,sK28,sK21,X1)
| ~ midp(sK24,X0,sK21)
| ~ midp(sK28,X0,X1) ),
inference(instantiation,[status(thm)],[c_19543]) ).
tcf(c_120692,plain,
( para(sK24,sK28,sK21,sK21)
| ~ midp(sK24,sK21,sK21)
| ~ midp(sK28,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_120691]) ).
tcf(c_135229,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK28,X0,X1)
| ~ midp(X0,sK28,X1) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_135230,plain,
( cong(sK21,sK28,sK21,sK21)
| ~ midp(sK21,sK28,sK21) ),
inference(instantiation,[status(thm)],[c_135229]) ).
tcf(c_135263,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,X0,sK28)
| ~ midp(X0,X1,sK28) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_135264,plain,
( cong(sK21,sK21,sK21,sK28)
| ~ midp(sK21,sK21,sK28) ),
inference(instantiation,[status(thm)],[c_135263]) ).
tcf(c_136447,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,X0,sK29)
| ~ midp(X0,X1,sK29) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_136448,plain,
( cong(sK21,sK21,sK21,sK29)
| ~ midp(sK21,sK21,sK29) ),
inference(instantiation,[status(thm)],[c_136447]) ).
tcf(c_136682,plain,
! [X0: $i,X1: $i] :
( cyclic(X0,X1,sK28,sK26)
| ~ cyclic(X0,X1,sK26,sK28) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_136683,plain,
( cyclic(sK21,sK21,sK28,sK26)
| ~ cyclic(sK21,sK21,sK26,sK28) ),
inference(instantiation,[status(thm)],[c_136682]) ).
tcf(c_139224,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,X2,sK26)
| ~ cyclic(X0,X1,sK26,X2) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_139225,plain,
( cyclic(sK21,sK21,sK21,sK26)
| ~ cyclic(sK21,sK21,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_139224]) ).
tcf(c_140557,plain,
! [X0: $i] :
( cyclic(X0,sK28,sK29,sK23)
| ~ cyclic(sK28,X0,sK29,sK23) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_140558,plain,
( cyclic(sK21,sK28,sK29,sK23)
| ~ cyclic(sK28,sK21,sK29,sK23) ),
inference(instantiation,[status(thm)],[c_140557]) ).
tcf(c_140790,plain,
! [X0: $i,X1: $i] :
( cyclic(sK28,X1,sK29,sK23)
| ~ cong(X0,sK28,X0,sK23)
| ~ cong(X0,sK28,X0,sK29)
| ~ cong(X0,sK28,X0,X1) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_140791,plain,
( cyclic(sK28,sK21,sK29,sK23)
| ~ cong(sK21,sK28,sK21,sK21)
| ~ cong(sK21,sK28,sK21,sK23)
| ~ cong(sK21,sK28,sK21,sK29) ),
inference(instantiation,[status(thm)],[c_140790]) ).
tcf(c_142529,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,X2,sK26,sK28)
| ~ cyclic(X0,X1,X2,sK26)
| ~ cyclic(X0,X1,X2,sK28) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_142530,plain,
( cyclic(sK21,sK21,sK26,sK28)
| ~ cyclic(sK21,sK21,sK21,sK26)
| ~ cyclic(sK21,sK21,sK21,sK28) ),
inference(instantiation,[status(thm)],[c_142529]) ).
tcf(c_146219,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X0,X1,sK26,X2)
| ~ cyclic(X0,sK26,X1,X2) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_146220,plain,
( cyclic(sK21,sK21,sK26,sK21)
| ~ cyclic(sK21,sK26,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_146219]) ).
tcf(c_146781,plain,
! [X0: $i] :
( cong(X0,sK28,X0,sK23)
| ~ midp(X0,sK28,sK23) ),
inference(instantiation,[status(thm)],[c_135229]) ).
tcf(c_146782,plain,
( cong(sK21,sK28,sK21,sK23)
| ~ midp(sK21,sK28,sK23) ),
inference(instantiation,[status(thm)],[c_146781]) ).
tcf(c_155382,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X3,X2,sK28)
| ~ cong(X0,X1,X0,sK28)
| ~ cong(X0,X1,X0,X3)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_155383,plain,
( cyclic(sK21,sK21,sK21,sK28)
| ~ cong(sK21,sK21,sK21,sK21)
| ~ cong(sK21,sK21,sK21,sK28) ),
inference(instantiation,[status(thm)],[c_155382]) ).
tcf(c_172146,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X0,X1,X4,sK26,X2,X3,X4,sK26)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_172147,plain,
( eqangle(sK21,sK21,sK21,sK26,sK21,sK21,sK21,sK26)
| ~ para(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_172146]) ).
tcf(c_188981,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK26,X0,X2)
| ~ coll(X0,X2,sK26)
| ~ eqangle(X0,X1,X0,sK26,X2,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_188982,plain,
( cyclic(sK21,sK26,sK21,sK21)
| ~ coll(sK21,sK21,sK26)
| ~ eqangle(sK21,sK21,sK21,sK26,sK21,sK21,sK21,sK26) ),
inference(instantiation,[status(thm)],[c_188981]) ).
tcf(c_188983,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_188982,c_172147,c_155383,c_146782,c_146220,c_142530,c_140791,c_140558,c_139225,c_136683,c_136448,c_135264,c_135230,c_120692,c_110324,c_109484,c_103813,c_103943,c_104143,c_104146,c_104306,c_106248,c_102629,c_101414,c_97840,c_89753,c_84592,c_86666,c_86705,c_82523,c_82387,c_82133,c_78189,c_76682,c_76472,c_76459,c_73740,c_74093,c_74193,c_74245,c_74283,c_75245,c_69695,c_67629,c_65844,c_65834,c_63884,c_63033,c_63000,c_62253,c_62243,c_62119,c_61737,c_61012,c_60910,c_57922,c_56551,c_44992,c_44991,c_39703,c_37645,c_35052,c_34621,c_34620,c_32457,c_29021,c_26841,c_24792,c_24770,c_24768,c_24764,c_24762,c_22493,c_18744,c_16558,c_15963,c_13637,c_11757,c_11252,c_10914,c_10342,c_9718,c_9704,c_9703,c_9244,c_8912,c_8446,c_8376,c_8103,c_7796,c_7794,c_7767,c_7453,c_7451,c_7355,c_7166,c_6835,c_6833,c_6468,c_6353,c_6349,c_6346,c_6345,c_6268,c_6198,c_6193,c_5901,c_5902,c_5855,c_237,c_188,c_183,c_179,c_162,c_171,c_172,c_173]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO543+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.37 % Computer : n006.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Wed Sep 23 12:21:26 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41
% 0.15/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.41
% 0.15/0.41 % Detected problem language: tptp
% 0.15/0.42 % Proving...
% 40.01/7.37 % SZS status Started for theBenchmark.p
% 40.01/7.37 % SZS status Theorem for theBenchmark.p
% 40.01/7.37
% 40.01/7.37 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 40.01/7.37
% 40.01/7.37 % ------ iProver source info
% 40.01/7.37
% 40.01/7.37 % git: date: 2026-07-19 20:42:38 +0200
% 40.01/7.37 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 40.01/7.37 % git: non_committed_changes: false
% 40.01/7.37
% 40.01/7.37 % ------ Parsing...
% 40.01/7.37 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 40.01/7.37
% 40.01/7.37 % ------ 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 %
% 40.01/7.37
% 40.01/7.37 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 40.01/7.37
% 40.01/7.37 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 40.01/7.37 % ------ Proving...
% 40.01/7.37 % ------ Problem Properties
% 40.01/7.37
% 40.01/7.37 %
% 40.01/7.37 % clauses 124
% 40.01/7.37 % conjectures 12
% 40.01/7.37 % EPR 87
% 40.01/7.37 % Horn 114
% 40.01/7.37 % unary 12
% 40.01/7.37 % binary 37
% 40.01/7.37 % lits 340
% 40.01/7.37 % lits eq 4
% 40.01/7.37 % fd_pure 0
% 40.01/7.37 % fd_pseudo 0
% 40.01/7.37 % fd_cond 0
% 40.01/7.37 % fd_pseudo_cond 4
% 40.01/7.37 % AC symbols 0
% 40.01/7.37
% 40.01/7.37 % ------ Schedule dynamic 5 is on
% 40.01/7.37
% 40.01/7.37 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 40.01/7.37
% 40.01/7.37
% 40.01/7.37 % ------
% 40.01/7.37 % Current options:
% 40.01/7.37 % ------
% 40.01/7.37
% 40.01/7.37
% 40.01/7.37 %
% 40.01/7.37
% 40.01/7.37 % ------ Proving...
% 40.01/7.37 %
% 40.01/7.37
% 40.01/7.37 % SZS status Theorem for theBenchmark.p
% 40.01/7.37
% 40.01/7.37 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 40.01/7.38
% 40.01/7.38
%------------------------------------------------------------------------------