%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO541+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 : n026.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 31.43s 6.87s
% Output : CNFRefutation 31.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 37
% Syntax : Number of formulae : 712 ( 165 unt; 0 def)
% Number of atoms : 1616 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1726 ( 822 ~; 815 |; 51 &)
% ( 0 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 1249 ( 0 sgn1235 !; 14 ?; 646 :)
% 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(f18,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD18) ).
fof(f19,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD19) ).
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(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(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(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( midp(X6,X3,X4)
& midp(X5,X2,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X0,X1)
& perp(X3,X2,X0,X1) )
=> perp(X5,X6,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL012001) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6] :
( ( midp(X6,X3,X4)
& midp(X5,X2,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X0,X1)
& perp(X3,X2,X0,X1) )
=> perp(X5,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(f122,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f18]) ).
fof(f123,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(ennf_transformation,[],[f19]) ).
fof(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(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(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(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6] :
( midp(X6,X3,X4)
& midp(X5,X2,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X0,X1)
& perp(X3,X2,X0,X1)
& ~ perp(X5,X6,X3,X4) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6] :
( midp(X6,X3,X4)
& midp(X5,X2,X1)
& coll(X4,X0,X2)
& perp(X4,X1,X0,X2)
& coll(X3,X0,X1)
& perp(X3,X2,X0,X1)
& ~ perp(X5,X6,X3,X4) ),
inference(flattening,[],[f249]) ).
fof(f270,plain,
( midp(sK26,sK23,sK24)
& midp(sK25,sK22,sK21)
& coll(sK24,sK20,sK22)
& perp(sK24,sK21,sK20,sK22)
& coll(sK23,sK20,sK21)
& perp(sK23,sK22,sK20,sK21)
& ~ perp(sK25,sK26,sK23,sK24) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25),skolemize(X6,sK26)],[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(f288,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f122]) ).
fof(f289,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(cnf_transformation,[],[f123]) ).
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(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(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(f384,plain,
midp(sK26,sK23,sK24),
inference(cnf_transformation,[],[f270]) ).
fof(f385,plain,
midp(sK25,sK22,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f386,plain,
coll(sK24,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f387,plain,
perp(sK24,sK21,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f388,plain,
coll(sK23,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f389,plain,
perp(sK23,sK22,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
~ perp(sK25,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_66,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X1,X0,X2,X3,X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X2,X3,X0,X1,X6,X7,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f289]) ).
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_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_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_162,negated_conjecture,
~ perp(sK25,sK26,sK23,sK24),
inference(cnf_transformation,[],[f390]) ).
tcf(c_163,negated_conjecture,
perp(sK23,sK22,sK20,sK21),
inference(cnf_transformation,[],[f389]) ).
tcf(c_164,negated_conjecture,
coll(sK23,sK20,sK21),
inference(cnf_transformation,[],[f388]) ).
tcf(c_165,negated_conjecture,
perp(sK24,sK21,sK20,sK22),
inference(cnf_transformation,[],[f387]) ).
tcf(c_166,negated_conjecture,
coll(sK24,sK20,sK22),
inference(cnf_transformation,[],[f386]) ).
tcf(c_167,negated_conjecture,
midp(sK25,sK22,sK21),
inference(cnf_transformation,[],[f385]) ).
tcf(c_168,negated_conjecture,
midp(sK26,sK23,sK24),
inference(cnf_transformation,[],[f384]) ).
tcf(c_174,plain,
( midp(sK20,sK20,sK20)
| ~ coll(sK20,sK20,sK20)
| ~ cong(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_177,plain,
( eqangle(sK20,sK20,sK20,sK20,sK20,sK20,sK20,sK20)
| ~ cyclic(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_232,plain,
( cong(sK20,sK20,sK20,sK20)
| ~ cyclic(sK20,sK20,sK20,sK20)
| ~ eqangle(sK20,sK20,sK20,sK20,sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_4278,negated_conjecture,
midp(sK26,sK23,sK24),
inference(demodulation,[status(thm)],[c_168]) ).
tcf(c_4279,negated_conjecture,
midp(sK25,sK22,sK21),
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_4280,negated_conjecture,
coll(sK24,sK20,sK22),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_4281,negated_conjecture,
perp(sK24,sK21,sK20,sK22),
inference(demodulation,[status(thm)],[c_165]) ).
tcf(c_4282,negated_conjecture,
coll(sK23,sK20,sK21),
inference(demodulation,[status(thm)],[c_164]) ).
tcf(c_4283,negated_conjecture,
perp(sK23,sK22,sK20,sK21),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_4284,negated_conjecture,
~ perp(sK25,sK26,sK23,sK24),
inference(demodulation,[status(thm)],[c_162]) ).
tcf(c_5790,plain,
coll(sK23,sK21,sK20),
inference(superposition,[status(thm)],[c_4282,c_49]) ).
tcf(c_5791,plain,
coll(sK24,sK22,sK20),
inference(superposition,[status(thm)],[c_4280,c_49]) ).
tcf(c_5797,plain,
coll(sK20,sK23,sK21),
inference(superposition,[status(thm)],[c_4282,c_50]) ).
tcf(c_5798,plain,
coll(sK20,sK24,sK22),
inference(superposition,[status(thm)],[c_4280,c_50]) ).
tcf(c_5799,plain,
coll(sK21,sK23,sK20),
inference(superposition,[status(thm)],[c_5790,c_50]) ).
tcf(c_5804,plain,
midp(sK25,sK21,sK22),
inference(superposition,[status(thm)],[c_4279,c_59]) ).
tcf(c_5805,plain,
midp(sK26,sK24,sK23),
inference(superposition,[status(thm)],[c_4278,c_59]) ).
tcf(c_5810,plain,
coll(sK25,sK22,sK21),
inference(superposition,[status(thm)],[c_4279,c_118]) ).
tcf(c_5811,plain,
coll(sK26,sK23,sK24),
inference(superposition,[status(thm)],[c_4278,c_118]) ).
tcf(c_5816,plain,
coll(sK22,sK24,sK20),
inference(superposition,[status(thm)],[c_5791,c_50]) ).
tcf(c_5819,plain,
coll(sK20,sK21,sK23),
inference(superposition,[status(thm)],[c_5797,c_49]) ).
tcf(c_5821,plain,
coll(sK20,sK22,sK24),
inference(superposition,[status(thm)],[c_5798,c_49]) ).
tcf(c_5824,plain,
coll(sK25,sK21,sK22),
inference(superposition,[status(thm)],[c_5804,c_118]) ).
tcf(c_5826,plain,
coll(sK26,sK24,sK23),
inference(superposition,[status(thm)],[c_5805,c_118]) ).
tcf(c_5828,plain,
coll(sK22,sK25,sK21),
inference(superposition,[status(thm)],[c_5810,c_50]) ).
tcf(c_5830,plain,
coll(sK23,sK26,sK24),
inference(superposition,[status(thm)],[c_5811,c_50]) ).
tcf(c_5838,plain,
coll(sK21,sK25,sK22),
inference(superposition,[status(thm)],[c_5824,c_50]) ).
tcf(c_5858,plain,
perp(sK23,sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_4283,c_55]) ).
tcf(c_5859,plain,
perp(sK24,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_4281,c_55]) ).
tcf(c_5860,plain,
coll(sK24,sK26,sK23),
inference(superposition,[status(thm)],[c_5826,c_50]) ).
tcf(c_5865,plain,
coll(sK23,sK24,sK26),
inference(superposition,[status(thm)],[c_5830,c_49]) ).
tcf(c_5873,plain,
coll(sK24,sK23,sK26),
inference(superposition,[status(thm)],[c_5860,c_49]) ).
tcf(c_5888,plain,
! [X0: $i] :
( coll(sK21,X0,sK23)
| ~ coll(sK23,sK20,X0) ),
inference(superposition,[status(thm)],[c_4282,c_51]) ).
tcf(c_5889,plain,
! [X0: $i] :
( coll(sK22,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_4280,c_51]) ).
tcf(c_5890,plain,
! [X0: $i] :
( coll(sK20,X0,sK23)
| ~ coll(sK23,sK21,X0) ),
inference(superposition,[status(thm)],[c_5790,c_51]) ).
tcf(c_5891,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK22,X0) ),
inference(superposition,[status(thm)],[c_5791,c_51]) ).
tcf(c_5892,plain,
! [X0: $i] :
( coll(sK21,X0,sK20)
| ~ coll(sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_5797,c_51]) ).
tcf(c_5893,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_5798,c_51]) ).
tcf(c_5894,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK23,X0) ),
inference(superposition,[status(thm)],[c_5799,c_51]) ).
tcf(c_5895,plain,
! [X0: $i] :
( coll(sK21,X0,sK25)
| ~ coll(sK25,sK22,X0) ),
inference(superposition,[status(thm)],[c_5810,c_51]) ).
tcf(c_5896,plain,
! [X0: $i] :
( coll(sK24,X0,sK26)
| ~ coll(sK26,sK23,X0) ),
inference(superposition,[status(thm)],[c_5811,c_51]) ).
tcf(c_5897,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(superposition,[status(thm)],[c_5816,c_51]) ).
tcf(c_5898,plain,
! [X0: $i] :
( coll(sK23,X0,sK20)
| ~ coll(sK20,sK21,X0) ),
inference(superposition,[status(thm)],[c_5819,c_51]) ).
tcf(c_5899,plain,
! [X0: $i] :
( coll(sK24,X0,sK20)
| ~ coll(sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_5821,c_51]) ).
tcf(c_5901,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK21,X0) ),
inference(superposition,[status(thm)],[c_5824,c_51]) ).
tcf(c_5902,plain,
! [X0: $i] :
( coll(sK23,X0,sK26)
| ~ coll(sK26,sK24,X0) ),
inference(superposition,[status(thm)],[c_5826,c_51]) ).
tcf(c_5903,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK25,X0) ),
inference(superposition,[status(thm)],[c_5828,c_51]) ).
tcf(c_5904,plain,
! [X0: $i] :
( coll(sK24,X0,sK23)
| ~ coll(sK23,sK26,X0) ),
inference(superposition,[status(thm)],[c_5830,c_51]) ).
tcf(c_5906,plain,
! [X0: $i] :
( coll(sK22,X0,sK21)
| ~ coll(sK21,sK25,X0) ),
inference(superposition,[status(thm)],[c_5838,c_51]) ).
tcf(c_5907,plain,
! [X0: $i] :
( coll(sK23,X0,sK24)
| ~ coll(sK24,sK26,X0) ),
inference(superposition,[status(thm)],[c_5860,c_51]) ).
tcf(c_5909,plain,
! [X0: $i] :
( coll(sK26,X0,sK23)
| ~ coll(sK23,sK24,X0) ),
inference(superposition,[status(thm)],[c_5865,c_51]) ).
tcf(c_5911,plain,
! [X0: $i] :
( coll(sK26,X0,sK24)
| ~ coll(sK24,sK23,X0) ),
inference(superposition,[status(thm)],[c_5873,c_51]) ).
tcf(c_5965,plain,
( coll(sK22,sK20,sK21)
| ~ coll(sK21,sK25,sK20) ),
inference(instantiation,[status(thm)],[c_5906]) ).
tcf(c_5969,plain,
( coll(sK22,sK20,sK25)
| ~ coll(sK25,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_5901]) ).
tcf(c_5972,plain,
( coll(sK20,sK20,sK22)
| ~ coll(sK22,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_5897]) ).
tcf(c_5975,plain,
( coll(sK20,sK20,sK21)
| ~ coll(sK21,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_5894]) ).
tcf(c_5976,plain,
( coll(sK22,sK20,sK20)
| ~ coll(sK20,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_5893]) ).
tcf(c_5977,plain,
( coll(sK21,sK20,sK20)
| ~ coll(sK20,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_5892]) ).
tcf(c_5984,plain,
perp(sK20,sK21,sK23,sK22),
inference(superposition,[status(thm)],[c_4283,c_56]) ).
tcf(c_5985,plain,
perp(sK20,sK22,sK24,sK21),
inference(superposition,[status(thm)],[c_4281,c_56]) ).
tcf(c_5986,plain,
perp(sK21,sK20,sK23,sK22),
inference(superposition,[status(thm)],[c_5858,c_56]) ).
tcf(c_5987,plain,
perp(sK22,sK20,sK24,sK21),
inference(superposition,[status(thm)],[c_5859,c_56]) ).
tcf(c_6001,plain,
perp(sK20,sK21,sK22,sK23),
inference(superposition,[status(thm)],[c_5984,c_55]) ).
tcf(c_6003,plain,
perp(sK20,sK22,sK21,sK24),
inference(superposition,[status(thm)],[c_5985,c_55]) ).
tcf(c_6005,plain,
perp(sK21,sK20,sK22,sK23),
inference(superposition,[status(thm)],[c_5986,c_55]) ).
tcf(c_6007,plain,
perp(sK22,sK20,sK21,sK24),
inference(superposition,[status(thm)],[c_5987,c_55]) ).
tcf(c_6012,plain,
coll(sK21,sK21,sK23),
inference(superposition,[status(thm)],[c_4282,c_5888]) ).
tcf(c_6013,plain,
! [X0: $i] :
( coll(sK23,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6012,c_51]) ).
tcf(c_6015,plain,
coll(sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_6012,c_49]) ).
tcf(c_6022,plain,
coll(sK22,sK22,sK24),
inference(superposition,[status(thm)],[c_4280,c_5889]) ).
tcf(c_6023,plain,
! [X0: $i] :
( coll(sK24,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6022,c_51]) ).
tcf(c_6025,plain,
coll(sK22,sK24,sK22),
inference(superposition,[status(thm)],[c_6022,c_49]) ).
tcf(c_6028,plain,
! [X0: $i] :
( coll(sK21,X0,sK21)
| ~ coll(sK21,sK23,X0) ),
inference(superposition,[status(thm)],[c_6015,c_51]) ).
tcf(c_6033,plain,
( coll(sK21,sK20,sK21)
| ~ coll(sK21,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_6028]) ).
tcf(c_6034,plain,
! [X0: $i] :
( coll(sK22,X0,sK22)
| ~ coll(sK22,sK24,X0) ),
inference(superposition,[status(thm)],[c_6025,c_51]) ).
tcf(c_6039,plain,
( coll(sK22,sK20,sK22)
| ~ coll(sK22,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_6034]) ).
tcf(c_6040,plain,
perp(sK22,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_6001,c_56]) ).
tcf(c_6048,plain,
coll(sK20,sK20,sK23),
inference(superposition,[status(thm)],[c_5790,c_5890]) ).
tcf(c_6053,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_6060,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_6082,plain,
! [X0: $i] :
( coll(sK23,X0,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(superposition,[status(thm)],[c_6048,c_51]) ).
tcf(c_6084,plain,
coll(sK20,sK23,sK20),
inference(superposition,[status(thm)],[c_6048,c_49]) ).
tcf(c_6088,plain,
! [X0: $i] :
( coll(sK20,X0,sK20)
| ~ coll(sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_6084,c_51]) ).
tcf(c_6089,plain,
coll(sK23,sK20,sK20),
inference(superposition,[status(thm)],[c_6084,c_50]) ).
tcf(c_6093,plain,
( coll(sK20,sK20,sK20)
| ~ coll(sK20,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_6088]) ).
tcf(c_6098,plain,
coll(sK20,sK20,sK24),
inference(superposition,[status(thm)],[c_5791,c_5891]) ).
tcf(c_6100,plain,
! [X0: $i] :
( coll(sK24,X0,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(superposition,[status(thm)],[c_6098,c_51]) ).
tcf(c_6102,plain,
coll(sK20,sK24,sK20),
inference(superposition,[status(thm)],[c_6098,c_49]) ).
tcf(c_6110,plain,
coll(sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_5797,c_5892]) ).
tcf(c_6111,plain,
coll(sK21,sK20,sK20),
inference(superposition,[status(thm)],[c_6084,c_5892]) ).
tcf(c_6112,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6110,c_51]) ).
tcf(c_6122,plain,
coll(sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_5798,c_5893]) ).
tcf(c_6123,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6122,c_51]) ).
tcf(c_6133,plain,
coll(sK21,sK21,sK25),
inference(superposition,[status(thm)],[c_5810,c_5895]) ).
tcf(c_6134,plain,
! [X0: $i] :
( coll(sK25,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6133,c_51]) ).
tcf(c_6139,plain,
( coll(sK25,sK20,sK21)
| ~ coll(sK21,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_6134]) ).
tcf(c_6144,plain,
coll(sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_5799,c_5894]) ).
tcf(c_6169,plain,
coll(sK24,sK20,sK20),
inference(superposition,[status(thm)],[c_6102,c_50]) ).
tcf(c_6176,plain,
coll(sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_6111,c_50]) ).
tcf(c_6189,plain,
coll(sK24,sK24,sK26),
inference(superposition,[status(thm)],[c_5811,c_5896]) ).
tcf(c_6190,plain,
! [X0: $i] :
( coll(sK26,X0,sK24)
| ~ coll(sK24,sK24,X0) ),
inference(superposition,[status(thm)],[c_6189,c_51]) ).
tcf(c_6195,plain,
( coll(sK26,sK20,sK24)
| ~ coll(sK24,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_6190]) ).
tcf(c_6202,plain,
coll(sK23,sK25,sK21),
inference(superposition,[status(thm)],[c_6133,c_6013]) ).
tcf(c_6216,plain,
coll(sK24,sK24,sK22),
inference(superposition,[status(thm)],[c_6022,c_6023]) ).
tcf(c_6220,plain,
coll(sK24,sK22,sK24),
inference(superposition,[status(thm)],[c_6216,c_49]) ).
tcf(c_6241,plain,
coll(sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_5816,c_5897]) ).
tcf(c_6304,plain,
coll(sK25,sK23,sK21),
inference(superposition,[status(thm)],[c_6202,c_50]) ).
tcf(c_6305,plain,
coll(sK23,sK21,sK25),
inference(superposition,[status(thm)],[c_6202,c_49]) ).
tcf(c_6323,plain,
! [X0: $i] :
( coll(sK24,X0,sK24)
| ~ coll(sK24,sK22,X0) ),
inference(superposition,[status(thm)],[c_6220,c_51]) ).
tcf(c_6329,plain,
( coll(sK24,sK20,sK24)
| ~ coll(sK24,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_6323]) ).
tcf(c_6347,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK23,X1)
| ~ midp(sK26,sK23,sK24)
| ~ coll(X0,sK23,X1)
| ~ para(sK26,X0,sK24,X1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_6348,plain,
( midp(sK20,sK23,sK20)
| ~ midp(sK26,sK23,sK24)
| ~ coll(sK20,sK23,sK20)
| ~ para(sK26,sK20,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_6347]) ).
tcf(c_6355,plain,
perp(sK22,sK23,sK21,sK20),
inference(superposition,[status(thm)],[c_6005,c_56]) ).
tcf(c_6357,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X0,X1)
| ~ midp(sK25,sK22,sK21)
| ~ para(sK22,X1,sK21,X0)
| ~ para(sK22,X0,sK21,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6358,plain,
( midp(sK25,sK20,sK20)
| ~ midp(sK25,sK22,sK21)
| ~ para(sK22,sK20,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_6357]) ).
tcf(c_6359,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X0,X1)
| ~ midp(sK26,sK23,sK24)
| ~ para(sK23,X1,sK24,X0)
| ~ para(sK23,X0,sK24,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6360,plain,
( midp(sK26,sK20,sK20)
| ~ midp(sK26,sK23,sK24)
| ~ para(sK23,sK20,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_6359]) ).
tcf(c_6365,plain,
coll(sK23,sK23,sK20),
inference(superposition,[status(thm)],[c_5819,c_5898]) ).
tcf(c_6373,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,sK21,X1)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_4279,c_93]) ).
tcf(c_6374,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,sK24,X1)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_4278,c_93]) ).
tcf(c_6375,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,sK22,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_5804,c_93]) ).
tcf(c_6376,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,sK23,X1)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_5805,c_93]) ).
tcf(c_6399,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_6409,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK21,X1)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_4279,c_112]) ).
tcf(c_6410,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK24,X1)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_4278,c_112]) ).
tcf(c_6411,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK22,X1)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_5804,c_112]) ).
tcf(c_6412,plain,
! [X0: $i,X1: $i] :
( para(sK24,X0,sK23,X1)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_5805,c_112]) ).
tcf(c_6468,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,sK25,X0)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6373,c_53]) ).
tcf(c_6469,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,X1,sK21)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6373,c_52]) ).
tcf(c_6480,plain,
! [X0: $i,X1: $i] :
( para(sK24,X1,sK26,X0)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6374,c_53]) ).
tcf(c_6481,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,X1,sK24)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6374,c_52]) ).
tcf(c_6495,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,X1,sK21)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_6409,c_52]) ).
tcf(c_6509,plain,
! [X0: $i,X1: $i] :
( para(sK24,X1,sK23,X0)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6410,c_53]) ).
tcf(c_6510,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,X1,sK24)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6410,c_52]) ).
tcf(c_6520,plain,
! [X0: $i,X1: $i] :
( para(sK22,X1,sK25,X0)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6375,c_53]) ).
tcf(c_6521,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,X1,sK22)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6375,c_52]) ).
tcf(c_6536,plain,
! [X0: $i,X1: $i] :
( para(sK23,X1,sK26,X0)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_6376,c_53]) ).
tcf(c_6537,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,X1,sK23)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_6376,c_52]) ).
tcf(c_6564,plain,
! [X0: $i,X1: $i] :
( para(sK24,X0,X1,sK23)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6412,c_52]) ).
tcf(c_6576,plain,
coll(sK24,sK24,sK20),
inference(superposition,[status(thm)],[c_5821,c_5899]) ).
tcf(c_6616,plain,
( cong(sK23,sK20,sK23,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_4283,c_104]) ).
tcf(c_6617,plain,
( cong(sK24,sK20,sK24,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_4281,c_104]) ).
tcf(c_6618,plain,
( cong(sK23,sK21,sK23,sK20)
| ~ midp(sK22,sK21,sK20) ),
inference(superposition,[status(thm)],[c_5858,c_104]) ).
tcf(c_6677,plain,
coll(sK25,sK21,sK23),
inference(superposition,[status(thm)],[c_6304,c_49]) ).
tcf(c_6682,plain,
coll(sK21,sK23,sK25),
inference(superposition,[status(thm)],[c_6305,c_50]) ).
tcf(c_6684,plain,
coll(sK20,sK25,sK23),
inference(superposition,[status(thm)],[c_6305,c_5890]) ).
tcf(c_6706,plain,
( midp(sK23,sK20,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK23,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6616,c_116]) ).
tcf(c_6707,plain,
( cong(sK23,sK21,sK23,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6616,c_72]) ).
tcf(c_6713,plain,
( midp(sK23,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6706,c_4282]) ).
tcf(c_6729,plain,
( cong(sK24,sK22,sK24,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6617,c_72]) ).
tcf(c_6751,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,X0,sK25)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6468,c_52]) ).
tcf(c_6759,plain,
! [X0: $i,X1: $i] :
( para(X1,sK21,sK25,X0)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6469,c_53]) ).
tcf(c_6773,plain,
! [X0: $i,X1: $i] :
( para(sK24,X1,X0,sK26)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6480,c_52]) ).
tcf(c_6799,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X0,X1)
| ~ midp(sK25,sK21,sK22)
| ~ para(sK21,X1,sK22,X0)
| ~ para(sK21,X0,sK22,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6800,plain,
( midp(sK25,sK20,sK20)
| ~ midp(sK25,sK21,sK22)
| ~ para(sK21,sK20,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_6799]) ).
tcf(c_6837,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK25,X3,X1,X2)
| ~ midp(X3,sK22,X0)
| ~ para(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6373,c_54]) ).
tcf(c_6838,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK26,X3,X1,X2)
| ~ midp(X3,sK23,X0)
| ~ para(sK24,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6374,c_54]) ).
tcf(c_6839,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK22,X3,X1,X2)
| ~ midp(sK25,X3,X0)
| ~ para(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6409,c_54]) ).
tcf(c_6840,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK23,X3,X1,X2)
| ~ midp(sK26,X3,X0)
| ~ para(sK24,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6410,c_54]) ).
tcf(c_6904,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK22,X0,X1)
| ~ perp(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_4283,c_57]) ).
tcf(c_6905,plain,
! [X0: $i,X1: $i] :
( para(sK24,sK21,X0,X1)
| ~ perp(sK20,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_4281,c_57]) ).
tcf(c_6907,plain,
! [X0: $i,X1: $i] :
( para(sK24,sK21,X0,X1)
| ~ perp(sK22,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_5859,c_57]) ).
tcf(c_6908,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK21,X0,X1)
| ~ perp(sK23,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_5984,c_57]) ).
tcf(c_6909,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK22,X0,X1)
| ~ perp(sK24,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_5985,c_57]) ).
tcf(c_6960,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK22,X3,X1,X2)
| ~ midp(sK25,X3,X0)
| ~ perp(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6409,c_58]) ).
tcf(c_7059,plain,
! [X0: $i] :
( circle(sK23,sK20,X0,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ cong(sK23,sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_6616,c_60]) ).
tcf(c_7060,plain,
! [X0: $i] :
( circle(sK24,sK20,X0,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ cong(sK24,sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_6617,c_60]) ).
tcf(c_7100,plain,
para(sK23,sK22,sK22,sK23),
inference(superposition,[status(thm)],[c_6001,c_6904]) ).
tcf(c_7106,plain,
para(sK24,sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_6003,c_6905]) ).
tcf(c_7114,plain,
para(sK22,sK23,sK23,sK22),
inference(superposition,[status(thm)],[c_7100,c_53]) ).
tcf(c_7149,plain,
para(sK21,sK24,sK24,sK21),
inference(superposition,[status(thm)],[c_7106,c_53]) ).
tcf(c_7179,plain,
! [X0: $i,X1: $i] :
( para(X1,sK21,sK22,X0)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_6495,c_53]) ).
tcf(c_7215,plain,
! [X0: $i,X1: $i] :
( cong(sK23,sK20,X0,X1)
| ~ midp(sK22,sK20,sK21)
| ~ cong(sK23,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6616,c_73]) ).
tcf(c_7216,plain,
! [X0: $i,X1: $i] :
( cong(sK24,sK20,X0,X1)
| ~ midp(sK21,sK20,sK22)
| ~ cong(sK24,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_6617,c_73]) ).
tcf(c_7270,plain,
coll(sK22,sK23,sK25),
inference(superposition,[status(thm)],[c_6677,c_5901]) ).
tcf(c_7277,plain,
coll(sK20,sK25,sK21),
inference(superposition,[status(thm)],[c_6682,c_5894]) ).
tcf(c_7283,plain,
coll(sK20,sK23,sK25),
inference(superposition,[status(thm)],[c_6684,c_49]) ).
tcf(c_7308,plain,
! [X0: $i,X1: $i] :
( para(X1,sK24,sK23,X0)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6510,c_53]) ).
tcf(c_7330,plain,
( midp(sK23,sK21,sK20)
| ~ midp(sK22,sK21,sK20)
| ~ coll(sK23,sK21,sK20) ),
inference(superposition,[status(thm)],[c_6618,c_116]) ).
tcf(c_7338,plain,
( midp(sK23,sK21,sK20)
| ~ midp(sK22,sK21,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7330,c_5790]) ).
tcf(c_7463,plain,
coll(sK23,sK23,sK26),
inference(superposition,[status(thm)],[c_5826,c_5902]) ).
tcf(c_7477,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X1,X0,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_88,c_66]) ).
tcf(c_7493,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X4,X5,X0,X1,X4,X5,X2,X3)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_88,c_67]) ).
tcf(c_7706,plain,
coll(sK22,sK25,sK23),
inference(superposition,[status(thm)],[c_7270,c_49]) ).
tcf(c_7711,plain,
coll(sK25,sK20,sK21),
inference(superposition,[status(thm)],[c_7277,c_50]) ).
tcf(c_7721,plain,
! [X0: $i] :
( coll(sK25,X0,sK20)
| ~ coll(sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_7283,c_51]) ).
tcf(c_7724,plain,
coll(sK21,sK25,sK20),
inference(superposition,[status(thm)],[c_7283,c_5892]) ).
tcf(c_7727,plain,
( coll(sK25,sK20,sK20)
| ~ coll(sK20,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_7721]) ).
tcf(c_7736,plain,
para(sK20,sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_4283,c_6908]) ).
tcf(c_7737,plain,
para(sK20,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_5858,c_6908]) ).
tcf(c_7747,plain,
para(sK21,sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_7737,c_53]) ).
tcf(c_7761,plain,
para(sK20,sK22,sK20,sK22),
inference(superposition,[status(thm)],[c_4281,c_6909]) ).
tcf(c_7762,plain,
para(sK20,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_5859,c_6909]) ).
tcf(c_7779,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK22,X0,X1)
| ~ para(sK22,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_7762,c_54]) ).
tcf(c_7780,plain,
para(sK22,sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_7762,c_53]) ).
tcf(c_7855,plain,
coll(sK24,sK24,sK23),
inference(superposition,[status(thm)],[c_5830,c_5904]) ).
tcf(c_7952,plain,
! [X0: $i] :
( coll(sK26,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_7463,c_51]) ).
tcf(c_7957,plain,
( coll(sK26,sK20,sK23)
| ~ coll(sK23,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_7952]) ).
tcf(c_8337,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_8350,plain,
( cyclic(sK20,sK20,sK20,sK20)
| ~ coll(sK20,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_8337]) ).
tcf(c_8375,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK25,X1,sK21)
| ~ midp(X0,sK22,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6373,c_94]) ).
tcf(c_8377,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK22,X1,sK21)
| ~ midp(sK25,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6409,c_94]) ).
tcf(c_8378,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK23,X1,sK24)
| ~ midp(sK26,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6410,c_94]) ).
tcf(c_8381,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK21,X1,sK22)
| ~ midp(sK25,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6411,c_94]) ).
tcf(c_8382,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK24,X1,sK23)
| ~ midp(sK26,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6412,c_94]) ).
tcf(c_8384,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK21)
| ~ midp(sK25,X1,X2)
| ~ midp(X0,sK22,X2)
| ~ coll(X0,X1,sK21) ),
inference(superposition,[status(thm)],[c_6469,c_94]) ).
tcf(c_8386,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK24)
| ~ midp(sK26,X1,X2)
| ~ midp(X0,sK23,X2)
| ~ coll(X0,X1,sK24) ),
inference(superposition,[status(thm)],[c_6481,c_94]) ).
tcf(c_8388,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK21)
| ~ midp(sK22,X1,X2)
| ~ midp(sK25,X0,X2)
| ~ coll(X0,X1,sK21) ),
inference(superposition,[status(thm)],[c_6495,c_94]) ).
tcf(c_8389,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK24,X1,sK23)
| ~ midp(sK26,X2,X0)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6509,c_94]) ).
tcf(c_8395,plain,
! [X0: $i] :
( midp(sK21,X0,sK21)
| ~ midp(sK20,X0,sK20)
| ~ coll(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_7736,c_94]) ).
tcf(c_8396,plain,
! [X0: $i] :
( midp(sK21,X0,sK20)
| ~ midp(sK20,X0,sK21)
| ~ coll(sK21,X0,sK20) ),
inference(superposition,[status(thm)],[c_7737,c_94]) ).
tcf(c_8397,plain,
! [X0: $i] :
( midp(sK22,X0,sK22)
| ~ midp(sK20,X0,sK20)
| ~ coll(sK22,X0,sK22) ),
inference(superposition,[status(thm)],[c_7761,c_94]) ).
tcf(c_8488,plain,
( midp(sK22,sK20,sK22)
| ~ midp(sK20,sK20,sK20)
| ~ coll(sK22,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_8397]) ).
tcf(c_8490,plain,
( midp(sK21,sK20,sK21)
| ~ midp(sK20,sK20,sK20)
| ~ coll(sK21,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_8395]) ).
tcf(c_8497,plain,
( midp(sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK20)
| ~ midp(sK25,sK20,sK20)
| ~ coll(sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_8388]) ).
tcf(c_8702,plain,
coll(sK21,sK23,sK22),
inference(superposition,[status(thm)],[c_7706,c_5903]) ).
tcf(c_8803,plain,
! [X0: $i] :
( perp(sK22,X0,sK22,sK23)
| ~ midp(sK25,X0,sK20) ),
inference(superposition,[status(thm)],[c_6005,c_6960]) ).
tcf(c_8903,plain,
coll(sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_5838,c_5906]) ).
tcf(c_9080,plain,
coll(sK25,sK21,sK20),
inference(superposition,[status(thm)],[c_7711,c_49]) ).
tcf(c_9212,plain,
( circle(sK23,sK20,sK21,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6616,c_7059]) ).
tcf(c_9231,plain,
( perp(sK20,sK21,sK21,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK23,sK20,sK21) ),
inference(superposition,[status(thm)],[c_9212,c_102]) ).
tcf(c_9232,plain,
( perp(sK20,sK21,sK21,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9231,c_4282]) ).
tcf(c_9243,plain,
! [X0: $i] :
( cong(sK20,X0,sK21,X0)
| ~ midp(sK22,sK20,sK21)
| ~ midp(X0,sK20,sK21) ),
inference(superposition,[status(thm)],[c_9232,c_101]) ).
tcf(c_9265,plain,
coll(sK23,sK23,sK24),
inference(superposition,[status(thm)],[c_5860,c_5907]) ).
tcf(c_9444,plain,
coll(sK22,sK20,sK21),
inference(superposition,[status(thm)],[c_7724,c_5906]) ).
tcf(c_9447,plain,
! [X0: $i] :
( coll(sK23,X0,sK24)
| ~ coll(sK24,sK24,X0) ),
inference(superposition,[status(thm)],[c_7855,c_51]) ).
tcf(c_9452,plain,
( coll(sK23,sK20,sK24)
| ~ coll(sK24,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_9447]) ).
tcf(c_9609,plain,
! [X0: $i] :
( cong(sK20,X0,X0,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ midp(X0,sK20,sK21) ),
inference(superposition,[status(thm)],[c_9243,c_71]) ).
tcf(c_9625,plain,
( cong(sK20,sK20,sK20,sK21)
| ~ midp(sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_9609]) ).
tcf(c_9642,plain,
( circle(sK24,sK20,sK22,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6617,c_7060]) ).
tcf(c_9663,plain,
( perp(sK20,sK22,sK22,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ coll(sK24,sK20,sK22) ),
inference(superposition,[status(thm)],[c_9642,c_102]) ).
tcf(c_9664,plain,
( perp(sK20,sK22,sK22,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9663,c_4280]) ).
tcf(c_9676,plain,
! [X0: $i] :
( cong(sK20,X0,sK22,X0)
| ~ midp(sK21,sK20,sK22)
| ~ midp(X0,sK20,sK22) ),
inference(superposition,[status(thm)],[c_9664,c_101]) ).
tcf(c_10046,plain,
! [X0: $i] :
( cong(sK20,X0,X0,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ midp(X0,sK20,sK22) ),
inference(superposition,[status(thm)],[c_9676,c_71]) ).
tcf(c_10062,plain,
( cong(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_10046]) ).
tcf(c_10074,plain,
( cong(sK23,sK20,sK23,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6707,c_7215]) ).
tcf(c_10113,plain,
( cong(sK24,sK20,sK24,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6729,c_7216]) ).
tcf(c_10238,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X0)
| ~ midp(X2,sK25,sK21)
| ~ midp(X1,sK22,X0)
| ~ para(sK25,X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6373,c_113]) ).
tcf(c_10240,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X0)
| ~ midp(X2,sK22,sK21)
| ~ midp(sK25,X1,X0)
| ~ para(sK22,X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6409,c_113]) ).
tcf(c_10258,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK20,sK20)
| ~ para(sK20,sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_7736,c_113]) ).
tcf(c_10260,plain,
! [X0: $i] :
( midp(X0,sK22,sK22)
| ~ midp(X0,sK20,sK20)
| ~ para(sK20,sK22,sK20,sK22) ),
inference(superposition,[status(thm)],[c_7761,c_113]) ).
tcf(c_10268,plain,
! [X0: $i] :
( midp(X0,sK22,sK22)
| ~ midp(X0,sK20,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10260,c_7761]) ).
tcf(c_10274,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK20,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10258,c_7736]) ).
tcf(c_10367,plain,
( midp(sK20,sK21,sK21)
| ~ midp(sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_10274]) ).
tcf(c_10368,plain,
( midp(sK20,sK22,sK22)
| ~ midp(sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_10268]) ).
tcf(c_11493,plain,
coll(sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_8702,c_5894]) ).
tcf(c_11500,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_8903,c_51]) ).
tcf(c_11506,plain,
( coll(sK21,sK20,sK22)
| ~ coll(sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_11500]) ).
tcf(c_12447,plain,
coll(sK22,sK20,sK25),
inference(superposition,[status(thm)],[c_9080,c_5901]) ).
tcf(c_12573,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6241,c_8377]) ).
tcf(c_13476,plain,
! [X0: $i] :
( coll(sK24,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_9265,c_51]) ).
tcf(c_13487,plain,
( coll(sK24,sK20,sK23)
| ~ coll(sK23,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_13476]) ).
tcf(c_13536,plain,
coll(sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_9444,c_49]) ).
tcf(c_14023,plain,
( midp(sK20,sK20,sK23)
| ~ midp(sK23,sK20,sK24)
| ~ midp(sK26,sK20,sK23) ),
inference(superposition,[status(thm)],[c_6048,c_8378]) ).
tcf(c_16271,plain,
coll(sK23,sK24,sK20),
inference(superposition,[status(thm)],[c_6098,c_6082]) ).
tcf(c_16581,plain,
coll(sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_11493,c_49]) ).
tcf(c_16712,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X0)
| ~ midp(X2,sK22,sK21)
| ~ midp(sK25,X1,X0)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_6409,c_10240]) ).
tcf(c_16749,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X0,X1)
| ~ midp(X2,sK22,sK21)
| ~ midp(sK25,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16712,c_59]) ).
tcf(c_17505,plain,
( midp(sK22,sK20,sK25)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,sK22,sK25) ),
inference(superposition,[status(thm)],[c_12447,c_8377]) ).
tcf(c_18019,plain,
coll(sK24,sK23,sK20),
inference(superposition,[status(thm)],[c_6048,c_6100]) ).
tcf(c_18314,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,X3,X2,X3)
| ~ cyclic(X1,X3,X0,X3)
| ~ cyclic(X1,X3,X0,X2)
| ~ cyclic(X1,X3,X0,X0)
| ~ para(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_88,c_92]) ).
tcf(c_18378,plain,
( cong(sK20,sK20,sK20,sK20)
| ~ cyclic(sK20,sK20,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_18314]) ).
tcf(c_21366,plain,
coll(sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_16581,c_50]) ).
tcf(c_21463,plain,
coll(sK23,sK20,sK24),
inference(superposition,[status(thm)],[c_16271,c_49]) ).
tcf(c_21464,plain,
coll(sK26,sK20,sK23),
inference(superposition,[status(thm)],[c_16271,c_5909]) ).
tcf(c_21646,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK22,X1)
| ~ midp(X0,X1,sK22) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_21647,plain,
( midp(sK20,sK22,sK20)
| ~ midp(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_21646]) ).
tcf(c_21648,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK23,X1)
| ~ midp(X0,X1,sK23) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_21649,plain,
( midp(sK20,sK23,sK20)
| ~ midp(sK20,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_21648]) ).
tcf(c_21652,plain,
! [X0: $i,X1: $i] :
( midp(X0,sK21,X1)
| ~ midp(X0,X1,sK21) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_21653,plain,
( midp(sK20,sK21,sK20)
| ~ midp(sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_21652]) ).
tcf(c_21700,plain,
coll(sK24,sK20,sK23),
inference(superposition,[status(thm)],[c_18019,c_49]) ).
tcf(c_21701,plain,
coll(sK26,sK20,sK24),
inference(superposition,[status(thm)],[c_18019,c_5911]) ).
tcf(c_22216,plain,
perp(sK21,sK24,sK22,sK20),
inference(superposition,[status(thm)],[c_6007,c_56]) ).
tcf(c_22225,plain,
( cong(sK22,sK20,sK22,sK21)
| ~ midp(sK23,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6040,c_104]) ).
tcf(c_22258,plain,
para(sK22,sK23,sK22,sK23),
inference(superposition,[status(thm)],[c_7114,c_52]) ).
tcf(c_22315,plain,
para(sK21,sK24,sK21,sK24),
inference(superposition,[status(thm)],[c_7149,c_52]) ).
tcf(c_22339,plain,
! [X0: $i] :
( midp(sK20,X0,sK21)
| ~ midp(sK21,X0,sK20)
| ~ coll(sK20,X0,sK21) ),
inference(superposition,[status(thm)],[c_7747,c_94]) ).
tcf(c_22341,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK20,X0,X1)
| ~ para(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_7747,c_54]) ).
tcf(c_22362,plain,
( midp(sK20,sK20,sK21)
| ~ midp(sK21,sK20,sK20)
| ~ coll(sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_22339]) ).
tcf(c_22641,plain,
! [X0: $i] :
( midp(sK20,X0,sK22)
| ~ midp(sK22,X0,sK20)
| ~ coll(sK20,X0,sK22) ),
inference(superposition,[status(thm)],[c_7780,c_94]) ).
tcf(c_22643,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ para(sK20,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_7780,c_54]) ).
tcf(c_22736,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK22,X0,sK21,X2)
| ~ midp(sK22,X1,sK21)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_22737,plain,
( para(sK22,sK20,sK21,sK20)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_22736]) ).
tcf(c_22738,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK23,X0,sK24,X2)
| ~ midp(sK23,X1,sK24)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_22739,plain,
( para(sK23,sK20,sK24,sK20)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK23,sK20,sK24) ),
inference(instantiation,[status(thm)],[c_22738]) ).
tcf(c_22746,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK21,X0,sK22,X2)
| ~ midp(sK21,X1,sK22)
| ~ midp(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_22747,plain,
( para(sK21,sK20,sK22,sK20)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_22746]) ).
tcf(c_23333,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,sK21,sK22) ),
inference(superposition,[status(thm)],[c_21366,c_8377]) ).
tcf(c_23350,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23333,c_5804]) ).
tcf(c_23581,plain,
( midp(sK23,sK20,sK24)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,sK23,sK24) ),
inference(superposition,[status(thm)],[c_21463,c_8377]) ).
tcf(c_23764,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK23,sK20,sK24)
| ~ midp(sK26,sK26,sK23) ),
inference(superposition,[status(thm)],[c_21464,c_8378]) ).
tcf(c_23765,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,sK26,sK23) ),
inference(superposition,[status(thm)],[c_21464,c_8377]) ).
tcf(c_23767,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK26,sK22,sK23)
| ~ midp(sK25,sK20,sK21) ),
inference(superposition,[status(thm)],[c_21464,c_8375]) ).
tcf(c_23769,plain,
coll(sK20,sK26,sK23),
inference(superposition,[status(thm)],[c_21464,c_50]) ).
tcf(c_23812,plain,
( midp(sK24,sK20,sK23)
| ~ midp(sK24,sK22,sK23)
| ~ midp(sK25,sK20,sK21) ),
inference(superposition,[status(thm)],[c_21700,c_8375]) ).
tcf(c_23875,plain,
! [X0: $i,X1: $i] :
( para(sK22,X1,X0,sK25)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6520,c_52]) ).
tcf(c_23902,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK22)
| ~ midp(sK25,X1,X2)
| ~ midp(X0,sK21,X2)
| ~ coll(X0,X1,sK22) ),
inference(superposition,[status(thm)],[c_6521,c_94]) ).
tcf(c_23905,plain,
! [X0: $i,X1: $i] :
( para(X1,sK22,sK25,X0)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_6521,c_53]) ).
tcf(c_23935,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK20,sK21,sK20)
| ~ midp(sK25,sK20,sK20)
| ~ coll(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_23902]) ).
tcf(c_23957,plain,
! [X0: $i,X1: $i] :
( para(sK23,X1,X0,sK26)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_6536,c_52]) ).
tcf(c_23987,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK23)
| ~ midp(sK26,X1,X2)
| ~ midp(X0,sK24,X2)
| ~ coll(X0,X1,sK23) ),
inference(superposition,[status(thm)],[c_6537,c_94]) ).
tcf(c_24264,plain,
( midp(sK26,sK20,sK24)
| ~ midp(sK23,sK20,sK24)
| ~ midp(sK26,sK26,sK24) ),
inference(superposition,[status(thm)],[c_21701,c_8378]) ).
tcf(c_24267,plain,
( midp(sK26,sK20,sK24)
| ~ midp(sK26,sK22,sK24)
| ~ midp(sK25,sK20,sK21) ),
inference(superposition,[status(thm)],[c_21701,c_8375]) ).
tcf(c_24541,plain,
! [X0: $i,X1: $i] :
( para(X1,sK23,sK24,X0)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6564,c_53]) ).
tcf(c_25390,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK25)
| ~ midp(sK21,X1,X2)
| ~ midp(X2,sK22,X0)
| ~ coll(X0,X1,sK25) ),
inference(superposition,[status(thm)],[c_6751,c_94]) ).
tcf(c_25393,plain,
! [X0: $i,X1: $i] :
( para(X0,sK25,sK21,X1)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_6751,c_53]) ).
tcf(c_25457,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK21,X0,X1)
| ~ midp(X2,X0,sK25)
| ~ midp(X1,sK22,X2)
| ~ coll(sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6759,c_94]) ).
tcf(c_25514,plain,
! [X0: $i,X1: $i] :
( para(X0,sK26,sK24,X1)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6773,c_53]) ).
tcf(c_25731,plain,
! [X0: $i,X1: $i] :
( para(X1,sK21,X0,sK22)
| ~ midp(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_7179,c_52]) ).
tcf(c_25869,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK24,X1)
| ~ midp(sK26,X1,X0)
| ~ midp(X2,X0,sK23)
| ~ para(X0,X1,sK23,sK24) ),
inference(superposition,[status(thm)],[c_7308,c_113]) ).
tcf(c_25870,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK24,X0,X1)
| ~ midp(sK26,X1,X2)
| ~ midp(X2,X0,sK23)
| ~ coll(sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_7308,c_94]) ).
tcf(c_25874,plain,
! [X0: $i,X1: $i] :
( para(X1,sK24,X0,sK23)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_7308,c_52]) ).
tcf(c_25910,plain,
( para(sK20,sK24,sK20,sK23)
| ~ midp(sK26,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_25874]) ).
tcf(c_25918,plain,
( midp(sK20,sK24,sK20)
| ~ midp(sK20,sK20,sK23)
| ~ midp(sK26,sK20,sK20)
| ~ para(sK20,sK20,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_25869]) ).
tcf(c_25997,plain,
coll(sK20,sK23,sK26),
inference(superposition,[status(thm)],[c_23769,c_49]) ).
tcf(c_26678,plain,
coll(sK20,sK26,sK20),
inference(superposition,[status(thm)],[c_25997,c_6088]) ).
tcf(c_27622,plain,
coll(sK26,sK20,sK20),
inference(superposition,[status(thm)],[c_26678,c_50]) ).
tcf(c_28087,plain,
( midp(sK26,sK20,sK20)
| ~ midp(sK23,sK20,sK24)
| ~ midp(sK26,sK26,sK20) ),
inference(superposition,[status(thm)],[c_27622,c_8378]) ).
tcf(c_28454,plain,
( para(sK24,sK21,sK22,sK23)
| ~ midp(sK25,sK20,sK20) ),
inference(superposition,[status(thm)],[c_8803,c_6907]) ).
tcf(c_28594,plain,
( cong(sK22,sK21,sK22,sK20)
| ~ midp(sK23,sK21,sK20) ),
inference(superposition,[status(thm)],[c_6355,c_104]) ).
tcf(c_28603,plain,
( cong(sK21,sK22,sK21,sK20)
| ~ midp(sK24,sK22,sK20) ),
inference(superposition,[status(thm)],[c_22216,c_104]) ).
tcf(c_29313,plain,
! [X0: $i,X1: $i] :
( cyclic(sK20,X0,sK20,X1)
| ~ midp(sK22,sK20,sK21)
| ~ cong(sK23,sK20,sK23,X1)
| ~ cong(sK23,sK20,sK23,X0) ),
inference(superposition,[status(thm)],[c_10074,c_61]) ).
tcf(c_29315,plain,
( midp(sK23,sK20,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK23,sK20,sK20) ),
inference(superposition,[status(thm)],[c_10074,c_116]) ).
tcf(c_29329,plain,
( circle(sK23,sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_10074,c_7059]) ).
tcf(c_29338,plain,
( midp(sK23,sK20,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29315,c_6089]) ).
tcf(c_29398,plain,
( cyclic(sK20,sK20,sK20,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ cong(sK23,sK20,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_29313]) ).
tcf(c_29689,plain,
! [X0: $i,X1: $i] :
( cyclic(sK20,X0,sK20,X1)
| ~ midp(sK21,sK20,sK22)
| ~ cong(sK24,sK20,sK24,X1)
| ~ cong(sK24,sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_10113,c_61]) ).
tcf(c_29691,plain,
( midp(sK24,sK20,sK20)
| ~ midp(sK21,sK20,sK22)
| ~ coll(sK24,sK20,sK20) ),
inference(superposition,[status(thm)],[c_10113,c_116]) ).
tcf(c_29705,plain,
( circle(sK24,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_10113,c_7060]) ).
tcf(c_29714,plain,
( midp(sK24,sK20,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_29691,c_6169]) ).
tcf(c_29773,plain,
( cyclic(sK20,sK20,sK20,sK20)
| ~ midp(sK21,sK20,sK22)
| ~ cong(sK24,sK20,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_29689]) ).
tcf(c_30478,plain,
( para(sK22,sK23,sK24,sK21)
| ~ midp(sK25,sK20,sK20) ),
inference(superposition,[status(thm)],[c_28454,c_53]) ).
tcf(c_31474,plain,
( perp(sK20,sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK23,sK20,sK21) ),
inference(superposition,[status(thm)],[c_29329,c_102]) ).
tcf(c_31475,plain,
( perp(sK20,sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31474,c_4282]) ).
tcf(c_31483,plain,
( cong(sK20,sK20,sK20,sK21)
| ~ midp(sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_31475,c_104]) ).
tcf(c_31484,plain,
( perp(sK20,sK21,sK20,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_31475,c_56]) ).
tcf(c_31490,plain,
! [X0: $i] :
( cong(sK20,X0,sK20,X0)
| ~ midp(sK22,sK20,sK21)
| ~ midp(X0,sK20,sK21) ),
inference(superposition,[status(thm)],[c_31475,c_101]) ).
tcf(c_31530,plain,
( para(sK23,sK22,sK20,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_31484,c_6904]) ).
tcf(c_31562,plain,
! [X0: $i] :
( midp(sK22,X0,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK23,X0,sK20)
| ~ coll(sK22,X0,sK20) ),
inference(superposition,[status(thm)],[c_31530,c_94]) ).
tcf(c_31584,plain,
( midp(sK22,sK20,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK23,sK20,sK20)
| ~ coll(sK22,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_31562]) ).
tcf(c_31586,plain,
( cong(sK20,sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_31483,c_167,c_174,c_177,c_232,c_5799,c_5975,c_5976,c_6084,c_6093,c_6102,c_6358,c_8497,c_9625,c_10074,c_22737,c_29338,c_29398,c_31584]) ).
tcf(c_31594,plain,
( midp(sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK20,sK20,sK21) ),
inference(superposition,[status(thm)],[c_31586,c_116]) ).
tcf(c_31600,plain,
( cong(sK20,sK21,sK20,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_31586,c_72]) ).
tcf(c_31613,plain,
( midp(sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31594,c_6144]) ).
tcf(c_31823,plain,
! [X0: $i] :
( midp(sK20,X0,X0)
| ~ midp(sK22,sK20,sK21)
| ~ midp(X0,sK20,sK21)
| ~ coll(sK20,X0,X0) ),
inference(superposition,[status(thm)],[c_31490,c_116]) ).
tcf(c_31917,plain,
( midp(sK20,sK20,sK20)
| ~ midp(sK20,sK20,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_31823]) ).
tcf(c_31990,plain,
! [X0: $i] :
( midp(sK24,X0,sK24)
| ~ midp(sK21,X0,sK21)
| ~ coll(sK24,X0,sK24) ),
inference(superposition,[status(thm)],[c_22315,c_94]) ).
tcf(c_32011,plain,
( midp(sK24,sK20,sK24)
| ~ midp(sK21,sK20,sK21)
| ~ coll(sK24,sK20,sK24) ),
inference(instantiation,[status(thm)],[c_31990]) ).
tcf(c_32690,plain,
( perp(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ coll(sK24,sK20,sK22) ),
inference(superposition,[status(thm)],[c_29705,c_102]) ).
tcf(c_32691,plain,
( perp(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_32690,c_4280]) ).
tcf(c_32885,plain,
( cong(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK22) ),
inference(superposition,[status(thm)],[c_32691,c_104]) ).
tcf(c_32886,plain,
( perp(sK20,sK22,sK20,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_32691,c_56]) ).
tcf(c_32934,plain,
( para(sK24,sK21,sK20,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_32886,c_6905]) ).
tcf(c_33098,plain,
! [X0: $i] :
( midp(sK21,X0,sK20)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK24,X0,sK20)
| ~ coll(sK21,X0,sK20) ),
inference(superposition,[status(thm)],[c_32934,c_94]) ).
tcf(c_33122,plain,
( midp(sK21,sK20,sK20)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK24,sK20,sK20)
| ~ coll(sK21,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_33098]) ).
tcf(c_33124,plain,
( cong(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(global_subsumption_just,[status(thm)],[c_32885,c_174,c_177,c_232,c_5799,c_5804,c_5816,c_5972,c_5975,c_5977,c_6084,c_6093,c_6800,c_10062,c_10113,c_21653,c_22362,c_22747,c_23935,c_29714,c_29773,c_33122]) ).
tcf(c_33132,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ coll(sK20,sK20,sK22) ),
inference(superposition,[status(thm)],[c_33124,c_116]) ).
tcf(c_33151,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_33132,c_6241]) ).
tcf(c_34492,plain,
( midp(sK20,sK21,sK20)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK20,sK21,sK20) ),
inference(superposition,[status(thm)],[c_31600,c_116]) ).
tcf(c_34503,plain,
( midp(sK20,sK21,sK20)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_34492,c_6176]) ).
tcf(c_41155,plain,
( midp(sK23,sK20,sK21)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK25,sK23,sK21) ),
inference(superposition,[status(thm)],[c_4282,c_8381]) ).
tcf(c_41191,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK25,sK22,sK21) ),
inference(superposition,[status(thm)],[c_9444,c_8381]) ).
tcf(c_42309,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41191,c_4279]) ).
tcf(c_43326,plain,
( midp(sK23,sK20,sK21)
| ~ midp(sK21,sK20,sK22) ),
inference(global_subsumption_just,[status(thm)],[c_41155,c_6713,c_42309]) ).
tcf(c_43382,plain,
( midp(sK23,sK20,sK24)
| ~ midp(sK24,sK20,sK23)
| ~ midp(sK26,sK23,sK24) ),
inference(superposition,[status(thm)],[c_21463,c_8382]) ).
tcf(c_44531,plain,
( midp(sK23,sK20,sK24)
| ~ midp(sK24,sK20,sK23) ),
inference(forward_subsumption_resolution,[status(thm)],[c_43382,c_4278]) ).
tcf(c_69258,plain,
! [X0: $i] :
( para(sK20,sK22,X0,sK21)
| ~ midp(sK25,sK20,X0) ),
inference(superposition,[status(thm)],[c_6495,c_7779]) ).
tcf(c_69306,plain,
! [X0: $i,X1: $i] :
( midp(sK22,X0,sK21)
| ~ midp(sK25,sK20,X1)
| ~ coll(sK22,X0,sK21)
| ~ midp(sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_69258,c_94]) ).
tcf(c_69330,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK25,sK20,sK20)
| ~ coll(sK22,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_69306]) ).
tcf(c_70448,plain,
( midp(sK21,sK21,sK20)
| ~ midp(sK20,sK21,sK21) ),
inference(superposition,[status(thm)],[c_6110,c_8396]) ).
tcf(c_81559,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK22,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_12573,c_23350,c_33151]) ).
tcf(c_82318,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X2,X0,X0,X1)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6053,c_72]) ).
tcf(c_82865,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,X1,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6060,c_71]) ).
tcf(c_83321,plain,
( cong(sK22,sK21,sK22,sK20)
| ~ midp(sK23,sK20,sK21) ),
inference(superposition,[status(thm)],[c_22225,c_72]) ).
tcf(c_83744,plain,
! [X0: $i,X1: $i] :
( para(X0,sK25,sK22,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_23875,c_53]) ).
tcf(c_83791,plain,
! [X0: $i,X1: $i] :
( para(X1,sK22,X0,sK25)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_23905,c_52]) ).
tcf(c_84072,plain,
! [X0: $i,X1: $i] :
( para(X0,sK26,sK23,X1)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_23957,c_53]) ).
tcf(c_85134,plain,
! [X0: $i,X1: $i] :
( para(X1,sK23,X0,sK24)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_24541,c_52]) ).
tcf(c_85139,plain,
! [X0: $i,X1: $i] :
( para(sK23,X1,sK24,X0)
| ~ midp(sK26,X1,sK23)
| ~ midp(sK26,X0,sK24) ),
inference(superposition,[status(thm)],[c_24541,c_6840]) ).
tcf(c_85181,plain,
( para(sK23,sK20,sK24,sK20)
| ~ midp(sK26,sK20,sK24)
| ~ midp(sK26,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_85139]) ).
tcf(c_86353,plain,
! [X0: $i,X1: $i] :
( para(X0,sK25,X1,sK21)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_25393,c_52]) ).
tcf(c_86553,plain,
! [X0: $i,X1: $i] :
( para(X0,sK26,X1,sK24)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_25514,c_52]) ).
tcf(c_86810,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK21,X1,sK22)
| ~ coll(sK21,X1,sK22)
| ~ midp(sK25,X2,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_25731,c_94]) ).
tcf(c_86863,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK25,sK20,sK20)
| ~ coll(sK21,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_86810]) ).
tcf(c_87901,plain,
( cong(sK22,sK20,sK22,sK21)
| ~ midp(sK23,sK21,sK20) ),
inference(superposition,[status(thm)],[c_28594,c_72]) ).
tcf(c_88541,plain,
( cong(sK21,sK20,sK21,sK22)
| ~ midp(sK24,sK22,sK20) ),
inference(superposition,[status(thm)],[c_28603,c_72]) ).
tcf(c_89005,plain,
( para(sK22,sK23,sK21,sK24)
| ~ midp(sK25,sK20,sK20) ),
inference(superposition,[status(thm)],[c_30478,c_52]) ).
tcf(c_89746,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X2,X0,X1,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_82318,c_71]) ).
tcf(c_89866,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X1,X0,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_82865,c_72]) ).
tcf(c_90801,plain,
( midp(sK22,sK21,sK20)
| ~ midp(sK23,sK20,sK21)
| ~ coll(sK22,sK21,sK20) ),
inference(superposition,[status(thm)],[c_83321,c_116]) ).
tcf(c_90814,plain,
( midp(sK22,sK21,sK20)
| ~ midp(sK23,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_90801,c_13536]) ).
tcf(c_91740,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK25,X0,X1)
| ~ midp(X2,sK21,X1)
| ~ midp(X2,X0,sK22)
| ~ coll(sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_83744,c_94]) ).
tcf(c_91744,plain,
! [X0: $i,X1: $i] :
( para(X0,sK25,X1,sK22)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_83744,c_52]) ).
tcf(c_91780,plain,
( para(sK20,sK25,sK20,sK22)
| ~ midp(sK20,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_91744]) ).
tcf(c_91786,plain,
( midp(sK25,sK20,sK20)
| ~ midp(sK20,sK21,sK20)
| ~ midp(sK20,sK20,sK22)
| ~ coll(sK25,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_91740]) ).
tcf(c_91796,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK22,sK25)
| ~ midp(X1,sK21,X0)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK25,X1,sK22) ),
inference(superposition,[status(thm)],[c_83791,c_113]) ).
tcf(c_91797,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK22,X1,sK25)
| ~ coll(sK22,X1,sK25)
| ~ midp(X2,sK21,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_83791,c_94]) ).
tcf(c_91853,plain,
( midp(sK22,sK20,sK25)
| ~ midp(sK20,sK21,sK20)
| ~ midp(sK20,sK20,sK20)
| ~ coll(sK22,sK20,sK25) ),
inference(instantiation,[status(thm)],[c_91797]) ).
tcf(c_91854,plain,
( midp(sK20,sK22,sK25)
| ~ midp(sK20,sK21,sK20)
| ~ midp(sK20,sK20,sK20)
| ~ para(sK20,sK25,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_91796]) ).
tcf(c_91936,plain,
! [X0: $i,X1: $i] :
( para(X0,sK26,X1,sK23)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_84072,c_52]) ).
tcf(c_92283,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,sK23,sK24)
| ~ midp(sK26,X1,X0)
| ~ midp(X2,X0,X1)
| ~ para(X0,sK24,X1,sK23) ),
inference(superposition,[status(thm)],[c_85134,c_113]) ).
tcf(c_92345,plain,
( midp(sK20,sK23,sK24)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK26,sK20,sK20)
| ~ para(sK20,sK24,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_92283]) ).
tcf(c_92590,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK25,X1,sK21)
| ~ coll(sK25,X1,sK21)
| ~ midp(X0,sK22,X2)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_86353,c_94]) ).
tcf(c_92642,plain,
( midp(sK25,sK20,sK21)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK20,sK22,sK20)
| ~ coll(sK25,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_92590]) ).
tcf(c_92699,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK26,X1,sK24)
| ~ coll(sK26,X1,sK24)
| ~ midp(X0,sK23,X2)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_86553,c_94]) ).
tcf(c_92751,plain,
( midp(sK26,sK20,sK24)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK20,sK23,sK20)
| ~ coll(sK26,sK20,sK24) ),
inference(instantiation,[status(thm)],[c_92699]) ).
tcf(c_93542,plain,
( midp(sK22,sK20,sK25)
| ~ midp(sK22,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_17505,c_5969,c_6084,c_6093,c_9080,c_31613,c_31917,c_34503,c_91853]) ).
tcf(c_94200,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK23,sK21,sK20)
| ~ coll(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_87901,c_116]) ).
tcf(c_94217,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK23,sK21,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_94200,c_9444]) ).
tcf(c_94316,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK24,sK22,sK20)
| ~ coll(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_88541,c_116]) ).
tcf(c_94333,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK24,sK22,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_94316,c_21366]) ).
tcf(c_95017,plain,
! [X0: $i] :
( midp(sK23,X0,sK24)
| ~ midp(sK25,sK20,sK20)
| ~ midp(sK22,X0,sK21)
| ~ coll(sK23,X0,sK24) ),
inference(superposition,[status(thm)],[c_89005,c_94]) ).
tcf(c_95020,plain,
( para(sK21,sK24,sK22,sK23)
| ~ midp(sK25,sK20,sK20) ),
inference(superposition,[status(thm)],[c_89005,c_53]) ).
tcf(c_95041,plain,
( midp(sK23,sK20,sK24)
| ~ midp(sK22,sK20,sK21)
| ~ midp(sK25,sK20,sK20)
| ~ coll(sK23,sK20,sK24) ),
inference(instantiation,[status(thm)],[c_95017]) ).
tcf(c_95454,plain,
! [X0: $i,X1: $i] :
( midp(X0,X1,X1)
| ~ midp(X1,X0,X0)
| ~ coll(X0,X1,X1) ),
inference(superposition,[status(thm)],[c_89746,c_116]) ).
tcf(c_95460,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X1,X0,X2,X0)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_89746,c_72]) ).
tcf(c_96714,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK26,X1,sK23)
| ~ coll(sK26,X1,sK23)
| ~ midp(X0,sK24,X2)
| ~ midp(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_91936,c_94]) ).
tcf(c_96770,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK20,sK20,sK20)
| ~ midp(sK20,sK24,sK20)
| ~ coll(sK26,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_96714]) ).
tcf(c_98218,plain,
! [X0: $i] :
( midp(sK24,X0,sK23)
| ~ midp(sK25,sK20,sK20)
| ~ midp(sK21,X0,sK22)
| ~ coll(sK24,X0,sK23) ),
inference(superposition,[status(thm)],[c_95020,c_94]) ).
tcf(c_98250,plain,
( midp(sK24,sK20,sK23)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK25,sK20,sK20)
| ~ coll(sK24,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_98218]) ).
tcf(c_98939,plain,
! [X0: $i,X1: $i] :
( midp(X0,X1,sK23)
| ~ midp(X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_98940,plain,
( midp(sK20,sK20,sK23)
| ~ midp(sK20,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_98939]) ).
tcf(c_100016,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X0,X1)
| ~ midp(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_82318,c_6399]) ).
tcf(c_100019,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X0,X1)
| ~ midp(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_89866,c_6399]) ).
tcf(c_100156,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,X2,sK23,sK24)
| ~ midp(X2,X1,sK24)
| ~ midp(X0,X1,sK23) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_100157,plain,
( para(sK20,sK20,sK23,sK24)
| ~ midp(sK20,sK20,sK24)
| ~ midp(sK20,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_100156]) ).
tcf(c_100332,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X1,X0)
| ~ midp(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_100016,c_52]) ).
tcf(c_100337,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,sK24,X1)
| ~ midp(sK24,X1,sK24)
| ~ midp(X0,sK23,sK24) ),
inference(superposition,[status(thm)],[c_100016,c_6838]) ).
tcf(c_100370,plain,
( para(sK26,sK20,sK24,sK20)
| ~ midp(sK20,sK23,sK24)
| ~ midp(sK24,sK20,sK24) ),
inference(instantiation,[status(thm)],[c_100337]) ).
tcf(c_100648,plain,
! [X0: $i,X1: $i] :
( para(X0,X0,X1,X0)
| ~ midp(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_100019,c_52]) ).
tcf(c_100650,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK21,X1)
| ~ midp(sK21,sK21,X1)
| ~ midp(sK25,X0,sK21) ),
inference(superposition,[status(thm)],[c_100019,c_6839]) ).
tcf(c_100689,plain,
( para(sK22,sK20,sK21,sK20)
| ~ midp(sK21,sK21,sK20)
| ~ midp(sK25,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_100650]) ).
tcf(c_101038,plain,
! [X0: $i,X1: $i] :
( para(X1,X0,X0,X0)
| ~ midp(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_100332,c_53]) ).
tcf(c_101649,plain,
! [X0: $i,X1: $i] :
( para(X1,X0,X0,X0)
| ~ midp(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_100648,c_53]) ).
tcf(c_107499,plain,
( para(sK21,sK20,sK21,sK21)
| ~ midp(sK21,sK21,sK20) ),
inference(superposition,[status(thm)],[c_101649,c_22341]) ).
tcf(c_107500,plain,
( para(sK21,sK20,sK21,sK21)
| ~ midp(sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_101038,c_22341]) ).
tcf(c_107586,plain,
( para(sK22,sK20,sK22,sK22)
| ~ midp(sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_101649,c_22643]) ).
tcf(c_107587,plain,
( para(sK22,sK20,sK22,sK22)
| ~ midp(sK22,sK20,sK22) ),
inference(superposition,[status(thm)],[c_101038,c_22643]) ).
tcf(c_119328,plain,
( midp(sK23,sK20,sK24)
| ~ midp(sK22,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_23581,c_6084,c_6576,c_7727,c_9452,c_34503,c_81559,c_91786,c_95041]) ).
tcf(c_119973,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X1,X0,X2,X3)
| ~ para(X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_7477,c_87]) ).
tcf(c_120491,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X2,X3,X2,X3)
| ~ para(X0,X1,X0,X1) ),
inference(superposition,[status(thm)],[c_7493,c_87]) ).
tcf(c_120657,plain,
! [X0: $i,X1: $i] : para(X0,X1,X0,X1),
inference(superposition,[status(thm)],[c_22258,c_120491]) ).
tcf(c_120673,plain,
para(sK20,sK20,sK20,sK20),
inference(instantiation,[status(thm)],[c_120657]) ).
tcf(c_120734,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_120657,c_113]) ).
tcf(c_120735,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X0)
| ~ midp(X2,X1,X2)
| ~ coll(X0,X1,X0) ),
inference(superposition,[status(thm)],[c_120657,c_94]) ).
tcf(c_120740,plain,
! [X0: $i,X1: $i] : coll(X0,X1,X1),
inference(superposition,[status(thm)],[c_120657,c_115]) ).
tcf(c_120748,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X2)
| ~ midp(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_120734,c_120657]) ).
tcf(c_120751,plain,
! [X0: $i,X1: $i] :
( midp(X1,X0,X0)
| ~ midp(X0,X1,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_95454,c_120740]) ).
tcf(c_120767,plain,
! [X0: $i,X1: $i] : coll(X0,X1,X0),
inference(superposition,[status(thm)],[c_120740,c_50]) ).
tcf(c_121230,plain,
! [X0: $i,X1: $i] : coll(X0,X0,X1),
inference(superposition,[status(thm)],[c_120767,c_49]) ).
tcf(c_121597,plain,
! [X0: $i] : coll(sK20,X0,sK22),
inference(backward_subsumption_resolution,[status(thm)],[c_6123,c_121230]) ).
tcf(c_121598,plain,
! [X0: $i] : coll(sK20,X0,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_6112,c_121230]) ).
tcf(c_121633,plain,
! [X0: $i] :
( midp(sK20,X0,sK22)
| ~ midp(sK22,X0,sK20) ),
inference(backward_subsumption_resolution,[status(thm)],[c_22641,c_121597]) ).
tcf(c_121636,plain,
! [X0: $i] :
( midp(sK20,X0,sK21)
| ~ midp(sK21,X0,sK20) ),
inference(backward_subsumption_resolution,[status(thm)],[c_22339,c_121598]) ).
tcf(c_121653,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X2,X1,X0)
| ~ coll(X0,X0,X1) ),
inference(superposition,[status(thm)],[c_121230,c_51]) ).
tcf(c_121657,plain,
! [X0: $i,X1: $i,X2: $i] : coll(X0,X1,X2),
inference(forward_subsumption_resolution,[status(thm)],[c_121653,c_121230]) ).
tcf(c_121705,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X1,X2,X0)
| ~ midp(sK24,X2,sK23)
| ~ midp(sK26,X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8389,c_121657]) ).
tcf(c_121708,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,sK24)
| ~ midp(sK26,X2,X1)
| ~ midp(X0,sK23,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8386,c_121657]) ).
tcf(c_121710,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,sK21)
| ~ midp(sK25,X2,X1)
| ~ midp(X0,sK22,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8384,c_121657]) ).
tcf(c_121940,plain,
( midp(sK20,sK20,sK24)
| ~ midp(sK20,sK23,sK20)
| ~ midp(sK26,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_121708]) ).
tcf(c_122000,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK23,sK20,sK24) ),
inference(global_subsumption_just,[status(thm)],[c_23764,c_168,c_174,c_5791,c_5799,c_6033,c_6084,c_6093,c_6329,c_6348,c_6360,c_6365,c_7957,c_8350,c_8490,c_18378,c_22739,c_25910,c_25918,c_32011,c_92345,c_96770,c_98940,c_100157,c_100370,c_120673,c_121940]) ).
tcf(c_122006,plain,
( midp(sK20,sK20,sK23)
| ~ midp(sK23,sK20,sK24) ),
inference(backward_subsumption_resolution,[status(thm)],[c_14023,c_122000]) ).
tcf(c_122009,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK22,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_23765,c_119328,c_122000]) ).
tcf(c_122021,plain,
( midp(sK26,sK20,sK23)
| ~ midp(sK25,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_23767,c_167,c_174,c_5965,c_6084,c_6093,c_6358,c_7724,c_8350,c_10367,c_18378,c_69330,c_70448,c_100689,c_120673,c_122009]) ).
tcf(c_122071,plain,
( midp(sK24,sK20,sK23)
| ~ midp(sK25,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_23812,c_167,c_174,c_6084,c_6093,c_6122,c_6358,c_6365,c_8350,c_10367,c_11506,c_13487,c_18378,c_70448,c_86863,c_98250,c_100689,c_120673]) ).
tcf(c_122169,plain,
( midp(sK26,sK20,sK24)
| ~ midp(sK23,sK20,sK24) ),
inference(global_subsumption_just,[status(thm)],[c_24264,c_174,c_6084,c_6093,c_6195,c_6576,c_8350,c_18378,c_21649,c_92751,c_120673,c_122006]) ).
tcf(c_122184,plain,
( midp(sK26,sK20,sK24)
| ~ midp(sK25,sK20,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_24267,c_44531,c_122071,c_122169]) ).
tcf(c_122792,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X0)
| ~ midp(X2,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_120735,c_120735,c_120767]) ).
tcf(c_122793,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X2,X1,X2)
| ~ midp(X0,X1,X0) ),
inference(renaming,[status(thm)],[c_122792]) ).
tcf(c_123480,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,sK22)
| ~ midp(sK25,X2,X1)
| ~ midp(X0,sK21,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23902,c_121657]) ).
tcf(c_123699,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,sK23)
| ~ midp(sK26,X2,X1)
| ~ midp(X0,sK24,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23987,c_121657]) ).
tcf(c_123919,plain,
para(sK21,sK20,sK21,sK21),
inference(global_subsumption_just,[status(thm)],[c_107499,c_174,c_5799,c_6033,c_6084,c_6093,c_8350,c_8490,c_18378,c_107500,c_120673]) ).
tcf(c_123922,plain,
! [X0: $i] :
( midp(X0,sK20,sK21)
| ~ midp(X0,sK21,sK21)
| ~ para(sK21,sK21,sK21,sK20) ),
inference(superposition,[status(thm)],[c_123919,c_113]) ).
tcf(c_123925,plain,
para(sK21,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_123919,c_53]) ).
tcf(c_123937,plain,
! [X0: $i] :
( midp(X0,sK20,sK21)
| ~ midp(X0,sK21,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_123922,c_123925]) ).
tcf(c_123940,plain,
( midp(sK20,sK20,sK21)
| ~ midp(sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_123937]) ).
tcf(c_123968,plain,
! [X0: $i] :
( para(sK25,X0,sK21,sK20)
| ~ midp(X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_123925,c_6837]) ).
tcf(c_124106,plain,
! [X0: $i] :
( para(X0,sK25,sK21,sK20)
| ~ midp(X0,sK22,sK21) ),
inference(superposition,[status(thm)],[c_123968,c_119973]) ).
tcf(c_124703,plain,
para(sK22,sK20,sK22,sK22),
inference(global_subsumption_just,[status(thm)],[c_107586,c_174,c_5816,c_6039,c_6084,c_6093,c_8350,c_8488,c_18378,c_107587,c_120673]) ).
tcf(c_124706,plain,
! [X0: $i] :
( midp(X0,sK20,sK22)
| ~ midp(X0,sK22,sK22)
| ~ para(sK22,sK22,sK22,sK20) ),
inference(superposition,[status(thm)],[c_124703,c_113]) ).
tcf(c_124709,plain,
para(sK22,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_124703,c_53]) ).
tcf(c_124715,plain,
! [X0: $i] :
( midp(X0,sK20,sK22)
| ~ midp(X0,sK22,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_124706,c_124709]) ).
tcf(c_124718,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK20,sK22,sK22) ),
inference(instantiation,[status(thm)],[c_124715]) ).
tcf(c_124766,plain,
! [X0: $i] :
( midp(X0,sK22,sK20)
| ~ midp(X0,sK22,sK22)
| ~ para(sK22,sK20,sK22,sK22) ),
inference(superposition,[status(thm)],[c_124709,c_113]) ).
tcf(c_124775,plain,
! [X0: $i] :
( midp(X0,sK22,sK20)
| ~ midp(X0,sK22,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_124766,c_124703]) ).
tcf(c_125293,plain,
! [X0: $i] :
( midp(X0,sK20,sK25)
| ~ midp(sK20,sK22,sK25)
| ~ midp(sK25,sK22,sK21)
| ~ midp(X0,sK25,sK21) ),
inference(superposition,[status(thm)],[c_124106,c_10238]) ).
tcf(c_125316,plain,
! [X0: $i] :
( midp(X0,sK20,sK25)
| ~ midp(sK20,sK22,sK25)
| ~ midp(X0,sK25,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_125293,c_4279]) ).
tcf(c_125332,plain,
! [X0: $i] :
( midp(X0,sK20,sK25)
| ~ midp(X0,sK25,sK21) ),
inference(global_subsumption_just,[status(thm)],[c_125316,c_174,c_6084,c_6093,c_8350,c_10367,c_18378,c_21653,c_91780,c_91854,c_120673,c_123940,c_125316]) ).
tcf(c_125718,plain,
midp(sK26,sK20,sK20),
inference(global_subsumption_just,[status(thm)],[c_28087,c_168,c_174,c_6084,c_6093,c_6110,c_6139,c_6360,c_8350,c_10368,c_18378,c_21647,c_85181,c_92642,c_120673,c_122021,c_122184,c_124718]) ).
tcf(c_125730,plain,
! [X0: $i] : midp(sK26,X0,X0),
inference(superposition,[status(thm)],[c_125718,c_120748]) ).
tcf(c_125733,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X1,X2,sK25)
| ~ midp(sK21,X2,X0)
| ~ midp(X0,sK22,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25390,c_121657]) ).
tcf(c_125888,plain,
! [X0: $i] : midp(X0,sK26,sK26),
inference(superposition,[status(thm)],[c_125730,c_120751]) ).
tcf(c_125999,plain,
! [X0: $i,X1: $i] : midp(X0,X1,X1),
inference(superposition,[status(thm)],[c_125888,c_120748]) ).
tcf(c_126002,plain,
! [X0: $i] : midp(X0,sK22,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_124775,c_125999]) ).
tcf(c_126025,plain,
midp(sK21,sK20,sK22),
inference(backward_subsumption_resolution,[status(thm)],[c_94333,c_126002]) ).
tcf(c_126060,plain,
midp(sK23,sK20,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_43326,c_126025]) ).
tcf(c_126123,plain,
midp(sK22,sK21,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_90814,c_126060]) ).
tcf(c_126134,plain,
midp(sK23,sK21,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_7338,c_126123]) ).
tcf(c_126138,plain,
midp(sK22,sK20,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_94217,c_126134]) ).
tcf(c_126155,plain,
midp(sK22,sK20,sK25),
inference(backward_subsumption_resolution,[status(thm)],[c_93542,c_126138]) ).
tcf(c_126491,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK21,X2,X0)
| ~ midp(X1,X2,sK25)
| ~ midp(X0,sK22,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25457,c_121657]) ).
tcf(c_127124,plain,
! [X0: $i,X1: $i] : midp(X0,X1,X0),
inference(superposition,[status(thm)],[c_125999,c_122793]) ).
tcf(c_127818,plain,
midp(sK22,sK25,sK20),
inference(superposition,[status(thm)],[c_126155,c_59]) ).
tcf(c_127995,plain,
midp(sK20,sK25,sK22),
inference(superposition,[status(thm)],[c_127818,c_121633]) ).
tcf(c_128609,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK24,X1,X2)
| ~ midp(sK26,X2,X0)
| ~ midp(X0,X1,sK23) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25870,c_121657]) ).
tcf(c_128992,plain,
midp(sK21,sK20,sK25),
inference(superposition,[status(thm)],[c_127124,c_125332]) ).
tcf(c_129050,plain,
midp(sK21,sK25,sK20),
inference(superposition,[status(thm)],[c_128992,c_59]) ).
tcf(c_129052,plain,
midp(sK20,sK25,sK21),
inference(superposition,[status(thm)],[c_129050,c_121636]) ).
tcf(c_129697,plain,
midp(sK20,sK22,sK25),
inference(superposition,[status(thm)],[c_127995,c_59]) ).
tcf(c_129840,plain,
! [X0: $i] :
( midp(sK21,X0,sK20)
| ~ midp(sK25,X0,sK25) ),
inference(superposition,[status(thm)],[c_129697,c_126491]) ).
tcf(c_129851,plain,
! [X0: $i] : midp(sK21,X0,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_129840,c_127124]) ).
tcf(c_129886,plain,
midp(sK20,sK21,sK25),
inference(superposition,[status(thm)],[c_129052,c_59]) ).
tcf(c_129982,plain,
! [X0: $i] :
( midp(sK20,X0,sK22)
| ~ midp(sK25,X0,sK25) ),
inference(superposition,[status(thm)],[c_129886,c_123480]) ).
tcf(c_129989,plain,
! [X0: $i] : midp(sK20,X0,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_129982,c_127124]) ).
tcf(c_130371,plain,
! [X0: $i] : midp(sK20,sK22,X0),
inference(superposition,[status(thm)],[c_129989,c_59]) ).
tcf(c_130499,plain,
! [X0: $i,X1: $i] :
( midp(X1,X0,sK25)
| ~ midp(sK21,X0,sK20) ),
inference(superposition,[status(thm)],[c_130371,c_125733]) ).
tcf(c_130508,plain,
! [X0: $i,X1: $i] : midp(X0,X1,sK25),
inference(forward_subsumption_resolution,[status(thm)],[c_130499,c_129851]) ).
tcf(c_130960,plain,
! [X0: $i,X1: $i] :
( midp(X1,X0,sK21)
| ~ midp(sK25,X0,sK25) ),
inference(superposition,[status(thm)],[c_130508,c_121710]) ).
tcf(c_130975,plain,
! [X0: $i,X1: $i] :
( midp(sK25,X0,X1)
| ~ midp(sK24,X0,sK23) ),
inference(superposition,[status(thm)],[c_130508,c_121705]) ).
tcf(c_130978,plain,
! [X0: $i,X1: $i] :
( midp(X1,X0,sK23)
| ~ midp(sK26,X0,sK25) ),
inference(superposition,[status(thm)],[c_130508,c_123699]) ).
tcf(c_130981,plain,
! [X0: $i,X1: $i] :
( midp(sK24,X0,X1)
| ~ midp(sK25,X0,sK23) ),
inference(superposition,[status(thm)],[c_130508,c_128609]) ).
tcf(c_130986,plain,
! [X0: $i,X1: $i] : midp(X0,X1,sK23),
inference(forward_subsumption_resolution,[status(thm)],[c_130978,c_130508]) ).
tcf(c_130987,plain,
! [X0: $i,X1: $i] : midp(sK24,X0,X1),
inference(backward_subsumption_resolution,[status(thm)],[c_130981,c_130986]) ).
tcf(c_130989,plain,
! [X0: $i,X1: $i] : midp(sK25,X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[c_130975,c_130987]) ).
tcf(c_130990,plain,
! [X0: $i,X1: $i] : midp(X0,X1,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_130960,c_130989]) ).
tcf(c_131031,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(X0,sK22,sK21) ),
inference(backward_subsumption_resolution,[status(thm)],[c_16749,c_130989]) ).
tcf(c_131035,plain,
! [X0: $i,X1: $i,X2: $i] : midp(X0,X1,X2),
inference(forward_subsumption_resolution,[status(thm)],[c_131031,c_130990]) ).
tcf(c_131041,plain,
! [X0: $i,X1: $i,X2: $i] : cong(X0,X1,X2,X1),
inference(backward_subsumption_resolution,[status(thm)],[c_95460,c_131035]) ).
tcf(c_131062,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : perp(X0,X1,X2,X3),
inference(backward_subsumption_resolution,[status(thm)],[c_105,c_131041]) ).
tcf(c_131065,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_4284,c_131062]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO541+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 12:23:53 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 31.43/6.87 % SZS status Started for theBenchmark.p
% 31.43/6.87 % SZS status Theorem for theBenchmark.p
% 31.43/6.87
% 31.43/6.87 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 31.43/6.87
% 31.43/6.87 % ------ iProver source info
% 31.43/6.87
% 31.43/6.87 % git: date: 2026-07-19 20:42:38 +0200
% 31.43/6.87 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 31.43/6.87 % git: non_committed_changes: false
% 31.43/6.87
% 31.43/6.87 % ------ Parsing...
% 31.43/6.87 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 31.43/6.87
% 31.43/6.87 % ------ 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 %
% 31.43/6.87
% 31.43/6.87 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 31.43/6.87
% 31.43/6.87 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 31.43/6.87 % ------ Proving...
% 31.43/6.87 % ------ Problem Properties
% 31.43/6.87
% 31.43/6.87 %
% 31.43/6.87 % clauses 119
% 31.43/6.87 % conjectures 7
% 31.43/6.87 % EPR 82
% 31.43/6.87 % Horn 109
% 31.43/6.87 % unary 7
% 31.43/6.87 % binary 37
% 31.43/6.87 % lits 335
% 31.43/6.87 % lits eq 4
% 31.43/6.87 % fd_pure 0
% 31.43/6.87 % fd_pseudo 0
% 31.43/6.87 % fd_cond 0
% 31.43/6.87 % fd_pseudo_cond 4
% 31.43/6.87 % AC symbols 0
% 31.43/6.87
% 31.43/6.87 % ------ Schedule dynamic 5 is on
% 31.43/6.87
% 31.43/6.87 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 31.43/6.87
% 31.43/6.87
% 31.43/6.87 % ------
% 31.43/6.87 % Current options:
% 31.43/6.87 % ------
% 31.43/6.87
% 31.43/6.87
% 31.43/6.87 %
% 31.43/6.87
% 31.43/6.87 % ------ Proving...
% 31.43/6.87 %
% 31.43/6.87
% 31.43/6.87 % SZS status Theorem for theBenchmark.p
% 31.43/6.87
% 31.43/6.87 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 31.43/6.88
% 31.43/6.88
%------------------------------------------------------------------------------