%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO568+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n007.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:30 PM UTC 2026
% Result : Theorem 25.97s 5.78s
% Output : CNFRefutation 25.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 30
% Syntax : Number of formulae : 621 ( 213 unt; 0 def)
% Number of atoms : 1341 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 1346 ( 626 ~; 620 |; 69 &)
% ( 0 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 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 : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 863 ( 0 sgn 845 !; 18 ?; 371 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD2) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( coll(X0,X1,X3)
& coll(X0,X1,X2) )
=> coll(X2,X3,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD3) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD4) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( para(X0,X1,X2,X3)
=> para(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD5) ).
fof(f6,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( para(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD6) ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD7) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD8) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& perp(X0,X1,X2,X3) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(f10,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X2,X3,X4,X5)
& para(X0,X1,X2,X3) )
=> perp(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD10) ).
fof(f11,axiom,
! [X0,X1,X2] :
( midp(X2,X1,X0)
=> midp(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD11) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( ( cong(X3,X0,X3,X2)
& cong(X3,X0,X3,X1) )
=> circle(X3,X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD12) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD23) ).
fof(f25,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( cong(X2,X3,X4,X5)
& cong(X0,X1,X2,X3) )
=> cong(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD25) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( coll(X2,X3,X1)
& eqangle(X2,X0,X2,X1,X3,X0,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
& cyclic(X0,X1,X2,X5)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f45,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X0,X2)
& midp(X3,X0,X1) )
=> para(X3,X4,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD44) ).
fof(f46,axiom,
! [X0,X1,X2,X3,X4] :
( ( coll(X4,X0,X2)
& para(X3,X4,X1,X2)
& midp(X3,X0,X1) )
=> midp(X4,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD45) ).
fof(f53,axiom,
! [X0,X1,X2,X3] :
( ( midp(X3,X0,X2)
& perp(X0,X1,X1,X2) )
=> cong(X0,X3,X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD52) ).
fof(f54,axiom,
! [X0,X1,X2,X3] :
( ( coll(X3,X0,X2)
& circle(X3,X0,X1,X2) )
=> perp(X0,X1,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD53) ).
fof(f56,axiom,
! [X0,X1,X2,X3] :
( ( perp(X3,X2,X0,X1)
& midp(X2,X0,X1) )
=> cong(X3,X0,X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD55) ).
fof(f57,axiom,
! [X0,X1,X2,X3] :
( ( cong(X0,X3,X1,X3)
& cong(X0,X2,X1,X2) )
=> perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD56) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X2,X3)
& midp(X4,X0,X1) )
=> para(X0,X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD63) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4] :
( ( para(X0,X3,X1,X2)
& para(X0,X2,X1,X3)
& midp(X4,X0,X1) )
=> midp(X4,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD64) ).
fof(f67,axiom,
! [X0,X1,X2] :
( para(X0,X1,X0,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD67) ).
fof(f69,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> cong(X0,X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD68) ).
fof(f70,axiom,
! [X0,X1,X2] :
( midp(X0,X1,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD69) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( coll(X5,X0,X2)
& perp(X5,X1,X0,X2)
& coll(X4,X0,X1)
& perp(X4,X2,X0,X1)
& perp(X1,X2,X8,X3)
& midp(X8,X1,X2)
& perp(X0,X2,X7,X3)
& midp(X7,X0,X2)
& perp(X0,X1,X6,X3)
& midp(X6,X0,X1) )
=> perp(X0,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL214030) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( coll(X5,X0,X2)
& perp(X5,X1,X0,X2)
& coll(X4,X0,X1)
& perp(X4,X2,X0,X1)
& perp(X1,X2,X8,X3)
& midp(X8,X1,X2)
& perp(X0,X2,X7,X3)
& midp(X7,X0,X2)
& perp(X0,X1,X6,X3)
& midp(X6,X0,X1) )
=> perp(X0,X3,X4,X5) ),
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(f128,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f25]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f130]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f40]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f154,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f156,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(ennf_transformation,[],[f46]) ).
fof(f160,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(flattening,[],[f159]) ).
fof(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,X7,X8] :
( coll(X5,X0,X2)
& perp(X5,X1,X0,X2)
& coll(X4,X0,X1)
& perp(X4,X2,X0,X1)
& perp(X1,X2,X8,X3)
& midp(X8,X1,X2)
& perp(X0,X2,X7,X3)
& midp(X7,X0,X2)
& perp(X0,X1,X6,X3)
& midp(X6,X0,X1)
& ~ perp(X0,X3,X4,X5) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( coll(X5,X0,X2)
& perp(X5,X1,X0,X2)
& coll(X4,X0,X1)
& perp(X4,X2,X0,X1)
& perp(X1,X2,X8,X3)
& midp(X8,X1,X2)
& perp(X0,X2,X7,X3)
& midp(X7,X0,X2)
& perp(X0,X1,X6,X3)
& midp(X6,X0,X1)
& ~ perp(X0,X3,X4,X5) ),
inference(flattening,[],[f249]) ).
fof(f270,plain,
( coll(sK25,sK20,sK22)
& perp(sK25,sK21,sK20,sK22)
& coll(sK24,sK20,sK21)
& perp(sK24,sK22,sK20,sK21)
& perp(sK21,sK22,sK28,sK23)
& midp(sK28,sK21,sK22)
& perp(sK20,sK22,sK27,sK23)
& midp(sK27,sK20,sK22)
& perp(sK20,sK21,sK26,sK23)
& midp(sK26,sK20,sK21)
& ~ perp(sK20,sK23,sK24,sK25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25),skolemize(X6,sK26),skolemize(X7,sK27),skolemize(X8,sK28)],[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(f293,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f131]) ).
fof(f310,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f149]) ).
fof(f313,plain,
! [X2,X3,X0,X1] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f314,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f156]) ).
fof(f315,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f316,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(cnf_transformation,[],[f160]) ).
fof(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,
coll(sK25,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f385,plain,
perp(sK25,sK21,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f386,plain,
coll(sK24,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f387,plain,
perp(sK24,sK22,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f388,plain,
perp(sK21,sK22,sK28,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f389,plain,
midp(sK28,sK21,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
perp(sK20,sK22,sK27,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f391,plain,
midp(sK27,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f392,plain,
perp(sK20,sK21,sK26,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f393,plain,
midp(sK26,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f394,plain,
~ perp(sK20,sK23,sK24,sK25),
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_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_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X0,X1,X4,X5)
| ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X0,X3)
| ~ coll(X0,X3,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( cong(X1,X2,X4,X5)
| ~ cyclic(X1,X2,X0,X5)
| ~ cyclic(X1,X2,X0,X4)
| ~ cyclic(X1,X2,X0,X3)
| ~ eqangle(X0,X1,X0,X2,X3,X4,X3,X5) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X3,X2,X4)
| ~ midp(X3,X1,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( midp(X1,X4,X3)
| ~ midp(X0,X4,X2)
| ~ coll(X1,X4,X3)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_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(sK20,sK23,sK24,sK25),
inference(cnf_transformation,[],[f394]) ).
tcf(c_163,negated_conjecture,
midp(sK26,sK20,sK21),
inference(cnf_transformation,[],[f393]) ).
tcf(c_164,negated_conjecture,
perp(sK20,sK21,sK26,sK23),
inference(cnf_transformation,[],[f392]) ).
tcf(c_165,negated_conjecture,
midp(sK27,sK20,sK22),
inference(cnf_transformation,[],[f391]) ).
tcf(c_166,negated_conjecture,
perp(sK20,sK22,sK27,sK23),
inference(cnf_transformation,[],[f390]) ).
tcf(c_167,negated_conjecture,
midp(sK28,sK21,sK22),
inference(cnf_transformation,[],[f389]) ).
tcf(c_168,negated_conjecture,
perp(sK21,sK22,sK28,sK23),
inference(cnf_transformation,[],[f388]) ).
tcf(c_169,negated_conjecture,
perp(sK24,sK22,sK20,sK21),
inference(cnf_transformation,[],[f387]) ).
tcf(c_170,negated_conjecture,
coll(sK24,sK20,sK21),
inference(cnf_transformation,[],[f386]) ).
tcf(c_171,negated_conjecture,
perp(sK25,sK21,sK20,sK22),
inference(cnf_transformation,[],[f385]) ).
tcf(c_172,negated_conjecture,
coll(sK25,sK20,sK22),
inference(cnf_transformation,[],[f384]) ).
tcf(c_178,plain,
( midp(sK20,sK20,sK20)
| ~ coll(sK20,sK20,sK20)
| ~ cong(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_182,plain,
( eqangle(sK20,sK20,sK20,sK20,sK20,sK20,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_187,plain,
( perp(sK20,sK20,sK20,sK20)
| ~ cong(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_236,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_4298,negated_conjecture,
coll(sK25,sK20,sK22),
inference(demodulation,[status(thm)],[c_172]) ).
tcf(c_4299,negated_conjecture,
perp(sK25,sK21,sK20,sK22),
inference(demodulation,[status(thm)],[c_171]) ).
tcf(c_4300,negated_conjecture,
coll(sK24,sK20,sK21),
inference(demodulation,[status(thm)],[c_170]) ).
tcf(c_4301,negated_conjecture,
perp(sK24,sK22,sK20,sK21),
inference(demodulation,[status(thm)],[c_169]) ).
tcf(c_4302,negated_conjecture,
perp(sK21,sK22,sK28,sK23),
inference(demodulation,[status(thm)],[c_168]) ).
tcf(c_4303,negated_conjecture,
midp(sK28,sK21,sK22),
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_4304,negated_conjecture,
perp(sK20,sK22,sK27,sK23),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_4305,negated_conjecture,
midp(sK27,sK20,sK22),
inference(demodulation,[status(thm)],[c_165]) ).
tcf(c_4306,negated_conjecture,
perp(sK20,sK21,sK26,sK23),
inference(demodulation,[status(thm)],[c_164]) ).
tcf(c_4307,negated_conjecture,
midp(sK26,sK20,sK21),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_5830,plain,
coll(sK24,sK21,sK20),
inference(superposition,[status(thm)],[c_4300,c_49]) ).
tcf(c_5831,plain,
coll(sK25,sK22,sK20),
inference(superposition,[status(thm)],[c_4298,c_49]) ).
tcf(c_5836,plain,
coll(sK20,sK24,sK21),
inference(superposition,[status(thm)],[c_4300,c_50]) ).
tcf(c_5837,plain,
coll(sK20,sK25,sK22),
inference(superposition,[status(thm)],[c_4298,c_50]) ).
tcf(c_5838,plain,
coll(sK21,sK24,sK20),
inference(superposition,[status(thm)],[c_5830,c_50]) ).
tcf(c_5840,plain,
coll(sK22,sK25,sK20),
inference(superposition,[status(thm)],[c_5831,c_50]) ).
tcf(c_5862,plain,
midp(sK26,sK21,sK20),
inference(superposition,[status(thm)],[c_4307,c_59]) ).
tcf(c_5863,plain,
midp(sK27,sK22,sK20),
inference(superposition,[status(thm)],[c_4305,c_59]) ).
tcf(c_5864,plain,
midp(sK28,sK22,sK21),
inference(superposition,[status(thm)],[c_4303,c_59]) ).
tcf(c_5871,plain,
coll(sK26,sK20,sK21),
inference(superposition,[status(thm)],[c_4307,c_118]) ).
tcf(c_5872,plain,
coll(sK27,sK20,sK22),
inference(superposition,[status(thm)],[c_4305,c_118]) ).
tcf(c_5873,plain,
coll(sK28,sK21,sK22),
inference(superposition,[status(thm)],[c_4303,c_118]) ).
tcf(c_5874,plain,
coll(sK26,sK21,sK20),
inference(superposition,[status(thm)],[c_5862,c_118]) ).
tcf(c_5875,plain,
coll(sK27,sK22,sK20),
inference(superposition,[status(thm)],[c_5863,c_118]) ).
tcf(c_5888,plain,
coll(sK28,sK22,sK21),
inference(superposition,[status(thm)],[c_5864,c_118]) ).
tcf(c_5890,plain,
coll(sK20,sK26,sK21),
inference(superposition,[status(thm)],[c_5871,c_50]) ).
tcf(c_5892,plain,
coll(sK20,sK27,sK22),
inference(superposition,[status(thm)],[c_5872,c_50]) ).
tcf(c_5894,plain,
coll(sK21,sK28,sK22),
inference(superposition,[status(thm)],[c_5873,c_50]) ).
tcf(c_5896,plain,
coll(sK21,sK26,sK20),
inference(superposition,[status(thm)],[c_5874,c_50]) ).
tcf(c_5898,plain,
coll(sK22,sK27,sK20),
inference(superposition,[status(thm)],[c_5875,c_50]) ).
tcf(c_5900,plain,
coll(sK22,sK28,sK21),
inference(superposition,[status(thm)],[c_5888,c_50]) ).
tcf(c_5903,plain,
coll(sK20,sK21,sK26),
inference(superposition,[status(thm)],[c_5890,c_49]) ).
tcf(c_5905,plain,
coll(sK20,sK22,sK27),
inference(superposition,[status(thm)],[c_5892,c_49]) ).
tcf(c_5909,plain,
coll(sK21,sK20,sK26),
inference(superposition,[status(thm)],[c_5896,c_49]) ).
tcf(c_5911,plain,
coll(sK22,sK20,sK27),
inference(superposition,[status(thm)],[c_5898,c_49]) ).
tcf(c_5913,plain,
coll(sK22,sK21,sK28),
inference(superposition,[status(thm)],[c_5900,c_49]) ).
tcf(c_5922,plain,
perp(sK20,sK21,sK23,sK26),
inference(superposition,[status(thm)],[c_4306,c_55]) ).
tcf(c_5926,plain,
perp(sK25,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_4299,c_55]) ).
tcf(c_5931,plain,
perp(sK26,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_4306,c_56]) ).
tcf(c_5932,plain,
perp(sK27,sK23,sK20,sK22),
inference(superposition,[status(thm)],[c_4304,c_56]) ).
tcf(c_5933,plain,
perp(sK28,sK23,sK21,sK22),
inference(superposition,[status(thm)],[c_4302,c_56]) ).
tcf(c_5935,plain,
perp(sK20,sK22,sK25,sK21),
inference(superposition,[status(thm)],[c_4299,c_56]) ).
tcf(c_5948,plain,
perp(sK23,sK26,sK20,sK21),
inference(superposition,[status(thm)],[c_5922,c_56]) ).
tcf(c_5956,plain,
perp(sK22,sK20,sK25,sK21),
inference(superposition,[status(thm)],[c_5926,c_56]) ).
tcf(c_5959,plain,
perp(sK26,sK23,sK21,sK20),
inference(superposition,[status(thm)],[c_5931,c_55]) ).
tcf(c_5961,plain,
perp(sK27,sK23,sK22,sK20),
inference(superposition,[status(thm)],[c_5932,c_55]) ).
tcf(c_5963,plain,
perp(sK28,sK23,sK22,sK21),
inference(superposition,[status(thm)],[c_5933,c_55]) ).
tcf(c_5993,plain,
perp(sK20,sK22,sK21,sK25),
inference(superposition,[status(thm)],[c_5935,c_55]) ).
tcf(c_5995,plain,
perp(sK23,sK26,sK21,sK20),
inference(superposition,[status(thm)],[c_5948,c_55]) ).
tcf(c_6012,plain,
perp(sK21,sK25,sK20,sK22),
inference(superposition,[status(thm)],[c_5993,c_56]) ).
tcf(c_6024,plain,
! [X0: $i] :
( coll(sK21,X0,sK24)
| ~ coll(sK24,sK20,X0) ),
inference(superposition,[status(thm)],[c_4300,c_51]) ).
tcf(c_6025,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK20,X0) ),
inference(superposition,[status(thm)],[c_4298,c_51]) ).
tcf(c_6026,plain,
! [X0: $i] :
( coll(sK20,X0,sK24)
| ~ coll(sK24,sK21,X0) ),
inference(superposition,[status(thm)],[c_5830,c_51]) ).
tcf(c_6027,plain,
! [X0: $i] :
( coll(sK20,X0,sK25)
| ~ coll(sK25,sK22,X0) ),
inference(superposition,[status(thm)],[c_5831,c_51]) ).
tcf(c_6028,plain,
! [X0: $i] :
( coll(sK21,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_5836,c_51]) ).
tcf(c_6029,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK25,X0) ),
inference(superposition,[status(thm)],[c_5837,c_51]) ).
tcf(c_6030,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK24,X0) ),
inference(superposition,[status(thm)],[c_5838,c_51]) ).
tcf(c_6031,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK25,X0) ),
inference(superposition,[status(thm)],[c_5840,c_51]) ).
tcf(c_6036,plain,
! [X0: $i] :
( coll(sK21,X0,sK26)
| ~ coll(sK26,sK20,X0) ),
inference(superposition,[status(thm)],[c_5871,c_51]) ).
tcf(c_6037,plain,
! [X0: $i] :
( coll(sK22,X0,sK27)
| ~ coll(sK27,sK20,X0) ),
inference(superposition,[status(thm)],[c_5872,c_51]) ).
tcf(c_6038,plain,
! [X0: $i] :
( coll(sK22,X0,sK28)
| ~ coll(sK28,sK21,X0) ),
inference(superposition,[status(thm)],[c_5873,c_51]) ).
tcf(c_6039,plain,
! [X0: $i] :
( coll(sK20,X0,sK26)
| ~ coll(sK26,sK21,X0) ),
inference(superposition,[status(thm)],[c_5874,c_51]) ).
tcf(c_6040,plain,
! [X0: $i] :
( coll(sK20,X0,sK27)
| ~ coll(sK27,sK22,X0) ),
inference(superposition,[status(thm)],[c_5875,c_51]) ).
tcf(c_6041,plain,
! [X0: $i] :
( coll(sK21,X0,sK28)
| ~ coll(sK28,sK22,X0) ),
inference(superposition,[status(thm)],[c_5888,c_51]) ).
tcf(c_6044,plain,
! [X0: $i] :
( coll(sK22,X0,sK21)
| ~ coll(sK21,sK28,X0) ),
inference(superposition,[status(thm)],[c_5894,c_51]) ).
tcf(c_6045,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK26,X0) ),
inference(superposition,[status(thm)],[c_5896,c_51]) ).
tcf(c_6046,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK27,X0) ),
inference(superposition,[status(thm)],[c_5898,c_51]) ).
tcf(c_6047,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK28,X0) ),
inference(superposition,[status(thm)],[c_5900,c_51]) ).
tcf(c_6048,plain,
! [X0: $i] :
( coll(sK26,X0,sK20)
| ~ coll(sK20,sK21,X0) ),
inference(superposition,[status(thm)],[c_5903,c_51]) ).
tcf(c_6049,plain,
! [X0: $i] :
( coll(sK27,X0,sK20)
| ~ coll(sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_5905,c_51]) ).
tcf(c_6051,plain,
! [X0: $i] :
( coll(sK26,X0,sK21)
| ~ coll(sK21,sK20,X0) ),
inference(superposition,[status(thm)],[c_5909,c_51]) ).
tcf(c_6052,plain,
! [X0: $i] :
( coll(sK27,X0,sK22)
| ~ coll(sK22,sK20,X0) ),
inference(superposition,[status(thm)],[c_5911,c_51]) ).
tcf(c_6053,plain,
! [X0: $i] :
( coll(sK28,X0,sK22)
| ~ coll(sK22,sK21,X0) ),
inference(superposition,[status(thm)],[c_5913,c_51]) ).
tcf(c_6116,plain,
( coll(sK27,sK20,sK20)
| ~ coll(sK20,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_6049]) ).
tcf(c_6117,plain,
( coll(sK26,sK20,sK20)
| ~ coll(sK20,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_6048]) ).
tcf(c_6119,plain,
( coll(sK20,sK20,sK22)
| ~ coll(sK22,sK27,sK20) ),
inference(instantiation,[status(thm)],[c_6046]) ).
tcf(c_6120,plain,
( coll(sK20,sK20,sK21)
| ~ coll(sK21,sK26,sK20) ),
inference(instantiation,[status(thm)],[c_6045]) ).
tcf(c_6132,plain,
( coll(sK22,sK20,sK20)
| ~ coll(sK20,sK25,sK20) ),
inference(instantiation,[status(thm)],[c_6029]) ).
tcf(c_6156,plain,
coll(sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_4300,c_6024]) ).
tcf(c_6157,plain,
! [X0: $i] :
( coll(sK24,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6156,c_51]) ).
tcf(c_6166,plain,
coll(sK22,sK22,sK25),
inference(superposition,[status(thm)],[c_4298,c_6025]) ).
tcf(c_6167,plain,
! [X0: $i] :
( coll(sK25,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6166,c_51]) ).
tcf(c_6188,plain,
coll(sK20,sK20,sK24),
inference(superposition,[status(thm)],[c_5830,c_6026]) ).
tcf(c_6191,plain,
! [X0: $i] :
( coll(sK24,X0,sK20)
| ~ coll(sK20,sK20,X0) ),
inference(superposition,[status(thm)],[c_6188,c_51]) ).
tcf(c_6193,plain,
coll(sK20,sK24,sK20),
inference(superposition,[status(thm)],[c_6188,c_49]) ).
tcf(c_6201,plain,
coll(sK20,sK20,sK25),
inference(superposition,[status(thm)],[c_5831,c_6027]) ).
tcf(c_6232,plain,
! [X0: $i] :
( coll(sK20,X0,sK20)
| ~ coll(sK20,sK24,X0) ),
inference(superposition,[status(thm)],[c_6193,c_51]) ).
tcf(c_6233,plain,
coll(sK24,sK20,sK20),
inference(superposition,[status(thm)],[c_6193,c_50]) ).
tcf(c_6237,plain,
( coll(sK20,sK20,sK20)
| ~ coll(sK20,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_6232]) ).
tcf(c_6243,plain,
coll(sK20,sK25,sK20),
inference(superposition,[status(thm)],[c_6201,c_49]) ).
tcf(c_6251,plain,
coll(sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_5836,c_6028]) ).
tcf(c_6252,plain,
coll(sK21,sK20,sK20),
inference(superposition,[status(thm)],[c_6193,c_6028]) ).
tcf(c_6256,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6251,c_51]) ).
tcf(c_6266,plain,
coll(sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_5837,c_6029]) ).
tcf(c_6273,plain,
( cong(sK26,sK20,sK26,sK21)
| ~ midp(sK26,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6274,plain,
( cong(sK27,sK20,sK27,sK22)
| ~ midp(sK27,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6280,plain,
coll(sK21,sK21,sK26),
inference(superposition,[status(thm)],[c_5871,c_6036]) ).
tcf(c_6281,plain,
! [X0: $i] :
( coll(sK26,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_6280,c_51]) ).
tcf(c_6295,plain,
coll(sK22,sK22,sK27),
inference(superposition,[status(thm)],[c_5872,c_6037]) ).
tcf(c_6296,plain,
! [X0: $i] :
( coll(sK27,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6295,c_51]) ).
tcf(c_6330,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,sK21,X1)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_4307,c_93]) ).
tcf(c_6331,plain,
! [X0: $i,X1: $i] :
( para(sK27,X0,sK22,X1)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_4305,c_93]) ).
tcf(c_6332,plain,
! [X0: $i,X1: $i] :
( para(sK28,X0,sK22,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_4303,c_93]) ).
tcf(c_6333,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,sK20,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_5862,c_93]) ).
tcf(c_6334,plain,
! [X0: $i,X1: $i] :
( para(sK27,X0,sK20,X1)
| ~ midp(X0,sK22,X1) ),
inference(superposition,[status(thm)],[c_5863,c_93]) ).
tcf(c_6368,plain,
coll(sK22,sK20,sK20),
inference(superposition,[status(thm)],[c_6243,c_6029]) ).
tcf(c_6375,plain,
coll(sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_6252,c_50]) ).
tcf(c_6391,plain,
! [X0: $i,X1: $i] :
( para(sK21,X1,sK26,X0)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_6330,c_53]) ).
tcf(c_6392,plain,
! [X0: $i,X1: $i] :
( para(sK26,X0,X1,sK21)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_6330,c_52]) ).
tcf(c_6403,plain,
! [X0: $i,X1: $i] :
( para(sK22,X1,sK27,X0)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_6331,c_53]) ).
tcf(c_6404,plain,
! [X0: $i,X1: $i] :
( para(sK27,X0,X1,sK22)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_6331,c_52]) ).
tcf(c_6423,plain,
! [X0: $i,X1: $i] :
( para(sK20,X0,sK21,X1)
| ~ midp(sK26,sK20,sK21)
| ~ midp(sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_6425,plain,
! [X0: $i,X1: $i] :
( para(sK20,X0,sK22,X1)
| ~ midp(sK27,sK20,sK22)
| ~ midp(sK27,X0,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_6426,plain,
( para(sK20,sK20,sK22,sK20)
| ~ midp(sK27,sK20,sK22)
| ~ midp(sK27,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_6425]) ).
tcf(c_6433,plain,
coll(sK22,sK22,sK28),
inference(superposition,[status(thm)],[c_5873,c_6038]) ).
tcf(c_6467,plain,
coll(sK25,sK28,sK22),
inference(superposition,[status(thm)],[c_6433,c_6167]) ).
tcf(c_6476,plain,
coll(sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_5840,c_6031]) ).
tcf(c_6498,plain,
! [X0: $i,X1: $i] :
( para(sK20,X0,sK21,X1)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_4307,c_112]) ).
tcf(c_6499,plain,
! [X0: $i,X1: $i] :
( para(sK20,X0,sK22,X1)
| ~ midp(sK27,X0,X1) ),
inference(superposition,[status(thm)],[c_4305,c_112]) ).
tcf(c_6500,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK22,X1)
| ~ midp(sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_4303,c_112]) ).
tcf(c_6501,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK20,X1)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_5862,c_112]) ).
tcf(c_6502,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK20,X1)
| ~ midp(sK27,X0,X1) ),
inference(superposition,[status(thm)],[c_5863,c_112]) ).
tcf(c_6503,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK21,X1)
| ~ midp(sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_5864,c_112]) ).
tcf(c_6518,plain,
( para(sK21,sK20,sK20,sK20)
| ~ midp(sK26,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_6501]) ).
tcf(c_6579,plain,
! [X0: $i,X1: $i] :
( para(sK20,X0,X1,sK21)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6498,c_52]) ).
tcf(c_6584,plain,
( para(sK20,sK20,sK20,sK21)
| ~ midp(sK26,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_6579]) ).
tcf(c_6637,plain,
! [X0: $i,X1: $i] :
( midp(sK28,X0,X1)
| ~ midp(sK28,sK21,sK22)
| ~ para(sK21,X1,sK22,X0)
| ~ para(sK21,X0,sK22,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6638,plain,
( midp(sK28,sK20,sK20)
| ~ midp(sK28,sK21,sK22)
| ~ para(sK21,sK20,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_6637]) ).
tcf(c_6715,plain,
( cong(sK24,sK20,sK24,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(superposition,[status(thm)],[c_4301,c_104]) ).
tcf(c_6716,plain,
( cong(sK25,sK20,sK25,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_4299,c_104]) ).
tcf(c_6727,plain,
( cong(sK23,sK20,sK23,sK21)
| ~ midp(sK26,sK20,sK21) ),
inference(superposition,[status(thm)],[c_5948,c_104]) ).
tcf(c_6737,plain,
( cong(sK23,sK21,sK23,sK20)
| ~ midp(sK26,sK21,sK20) ),
inference(superposition,[status(thm)],[c_5995,c_104]) ).
tcf(c_6745,plain,
cong(sK23,sK21,sK23,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_6737,c_5862]) ).
tcf(c_6762,plain,
cong(sK23,sK20,sK23,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_6727,c_4307]) ).
tcf(c_6824,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK26,X3,X1,X2)
| ~ midp(X3,sK20,X0)
| ~ para(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6330,c_54]) ).
tcf(c_6831,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK20,X3,X1,X2)
| ~ midp(sK26,X3,X0)
| ~ para(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6498,c_54]) ).
tcf(c_6899,plain,
coll(sK20,sK22,sK20),
inference(superposition,[status(thm)],[c_6368,c_50]) ).
tcf(c_6988,plain,
( midp(sK24,sK20,sK21)
| ~ midp(sK22,sK20,sK21)
| ~ coll(sK24,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6715,c_116]) ).
tcf(c_6995,plain,
( midp(sK24,sK20,sK21)
| ~ midp(sK22,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6988,c_4300]) ).
tcf(c_7020,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK21,X0,X1)
| ~ perp(sK26,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_4306,c_57]) ).
tcf(c_7021,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK22,X0,X1)
| ~ perp(sK27,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_4304,c_57]) ).
tcf(c_7022,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK22,X0,X1)
| ~ perp(sK28,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_4302,c_57]) ).
tcf(c_7024,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK21,X0,X1)
| ~ perp(sK20,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_4299,c_57]) ).
tcf(c_7030,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK23,X0,X1)
| ~ perp(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_5931,c_57]) ).
tcf(c_7039,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK20,X0,X1)
| ~ perp(sK25,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_5956,c_57]) ).
tcf(c_7119,plain,
( para(sK22,sK20,sK20,sK20)
| ~ perp(sK25,sK21,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_7039]) ).
tcf(c_7336,plain,
! [X0: $i] :
( circle(sK25,sK20,X0,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ cong(sK25,sK20,sK25,X0) ),
inference(superposition,[status(thm)],[c_6716,c_60]) ).
tcf(c_7337,plain,
( midp(sK25,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ coll(sK25,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6716,c_116]) ).
tcf(c_7344,plain,
( midp(sK25,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7337,c_4298]) ).
tcf(c_7365,plain,
para(sK20,sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_5931,c_7020]) ).
tcf(c_7366,plain,
para(sK20,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_5959,c_7020]) ).
tcf(c_7378,plain,
para(sK20,sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_5961,c_7021]) ).
tcf(c_7384,plain,
para(sK21,sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_5963,c_7022]) ).
tcf(c_7399,plain,
( cong(sK26,sK21,sK26,sK20)
| ~ midp(sK26,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_7466,plain,
! [X0: $i,X1: $i] :
( cong(sK23,sK20,X0,X1)
| ~ cong(sK23,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6762,c_73]) ).
tcf(c_7524,plain,
coll(sK28,sK25,sK22),
inference(superposition,[status(thm)],[c_6467,c_50]) ).
tcf(c_7525,plain,
coll(sK25,sK22,sK28),
inference(superposition,[status(thm)],[c_6467,c_49]) ).
tcf(c_7560,plain,
( cong(sK27,sK22,sK27,sK20)
| ~ midp(sK27,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_7577,plain,
! [X0: $i,X1: $i] :
( midp(sK27,X0,X1)
| ~ midp(sK27,sK22,sK20)
| ~ para(sK22,X1,sK20,X0)
| ~ para(sK22,X0,sK20,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_7578,plain,
( midp(sK27,sK20,sK20)
| ~ midp(sK27,sK22,sK20)
| ~ para(sK22,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_7577]) ).
tcf(c_7832,plain,
para(sK22,sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_7384,c_53]) ).
tcf(c_7886,plain,
! [X0: $i,X1: $i] :
( cong(sK26,sK20,X0,X1)
| ~ cong(sK26,sK20,sK26,sK21)
| ~ cong(sK26,sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_7904,plain,
coll(sK20,sK20,sK26),
inference(superposition,[status(thm)],[c_5874,c_6039]) ).
tcf(c_7994,plain,
! [X0: $i,X1: $i] :
( cong(sK27,sK20,X0,X1)
| ~ cong(sK27,sK20,sK27,sK22)
| ~ cong(sK27,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_8049,plain,
coll(sK20,sK20,sK27),
inference(superposition,[status(thm)],[c_5875,c_6040]) ).
tcf(c_8540,plain,
coll(sK21,sK21,sK28),
inference(superposition,[status(thm)],[c_5888,c_6041]) ).
tcf(c_8552,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_8565,plain,
( cyclic(sK20,sK20,sK20,sK20)
| ~ coll(sK20,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_8552]) ).
tcf(c_8584,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK26,X1,sK21)
| ~ midp(X0,sK20,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6330,c_94]) ).
tcf(c_8585,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK27,X1,sK22)
| ~ midp(X0,sK20,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6331,c_94]) ).
tcf(c_8586,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK28,X1,sK22)
| ~ midp(X0,sK21,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6332,c_94]) ).
tcf(c_8587,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK26,X1,sK20)
| ~ midp(X0,sK21,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6333,c_94]) ).
tcf(c_8588,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK27,X1,sK20)
| ~ midp(X0,sK22,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6334,c_94]) ).
tcf(c_8590,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK21,X1,sK26)
| ~ midp(X2,sK20,X0)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6391,c_94]) ).
tcf(c_8591,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK21)
| ~ midp(sK26,X1,X2)
| ~ midp(X0,sK20,X2)
| ~ coll(X0,X1,sK21) ),
inference(superposition,[status(thm)],[c_6392,c_94]) ).
tcf(c_8592,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK22,X1,sK27)
| ~ midp(X2,sK20,X0)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6403,c_94]) ).
tcf(c_8593,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK22)
| ~ midp(sK27,X1,X2)
| ~ midp(X0,sK20,X2)
| ~ coll(X0,X1,sK22) ),
inference(superposition,[status(thm)],[c_6404,c_94]) ).
tcf(c_8596,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK20,X1,sK21)
| ~ midp(sK26,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6498,c_94]) ).
tcf(c_8597,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK20,X1,sK22)
| ~ midp(sK27,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6499,c_94]) ).
tcf(c_8598,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK21,X1,sK22)
| ~ midp(sK28,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6500,c_94]) ).
tcf(c_8599,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK21,X1,sK20)
| ~ midp(sK26,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6501,c_94]) ).
tcf(c_8600,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK22,X1,sK20)
| ~ midp(sK27,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6502,c_94]) ).
tcf(c_8601,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,X2)
| ~ midp(sK22,X1,sK21)
| ~ midp(sK28,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6503,c_94]) ).
tcf(c_8602,plain,
! [X0: $i] :
( midp(sK21,X0,sK21)
| ~ midp(sK20,X0,sK20)
| ~ coll(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_7365,c_94]) ).
tcf(c_8605,plain,
! [X0: $i] :
( midp(sK22,X0,sK20)
| ~ midp(sK20,X0,sK22)
| ~ coll(sK22,X0,sK20) ),
inference(superposition,[status(thm)],[c_7378,c_94]) ).
tcf(c_8748,plain,
( midp(sK22,sK20,sK20)
| ~ midp(sK20,sK20,sK22)
| ~ coll(sK22,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_8605]) ).
tcf(c_8760,plain,
( midp(sK20,sK20,sK22)
| ~ midp(sK27,sK20,sK20)
| ~ midp(sK20,sK20,sK20)
| ~ coll(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_8593]) ).
tcf(c_8761,plain,
( midp(sK20,sK20,sK21)
| ~ midp(sK26,sK20,sK20)
| ~ midp(sK20,sK20,sK20)
| ~ coll(sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_8591]) ).
tcf(c_8926,plain,
coll(sK28,sK22,sK25),
inference(superposition,[status(thm)],[c_7524,c_49]) ).
tcf(c_8935,plain,
coll(sK22,sK25,sK28),
inference(superposition,[status(thm)],[c_7525,c_50]) ).
tcf(c_8937,plain,
coll(sK20,sK28,sK25),
inference(superposition,[status(thm)],[c_7525,c_6027]) ).
tcf(c_8989,plain,
! [X0: $i,X1: $i] :
( para(X1,sK21,sK20,X0)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6579,c_53]) ).
tcf(c_9006,plain,
( para(sK20,sK21,sK20,sK20)
| ~ midp(sK26,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_8989]) ).
tcf(c_9657,plain,
( para(sK20,sK20,sK21,sK21)
| ~ midp(sK26,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_6423]) ).
tcf(c_9690,plain,
( para(sK20,sK20,sK22,sK22)
| ~ midp(sK27,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_6425]) ).
tcf(c_9784,plain,
coll(sK20,sK26,sK20),
inference(superposition,[status(thm)],[c_7904,c_49]) ).
tcf(c_9999,plain,
coll(sK22,sK22,sK21),
inference(superposition,[status(thm)],[c_5894,c_6044]) ).
tcf(c_10132,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK20,sK20)
| ~ para(sK20,sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_7365,c_113]) ).
tcf(c_10133,plain,
! [X0: $i] :
( midp(X0,sK21,sK20)
| ~ midp(X0,sK20,sK21)
| ~ para(sK20,sK20,sK21,sK21) ),
inference(superposition,[status(thm)],[c_7366,c_113]) ).
tcf(c_10193,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK20,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10132,c_7365]) ).
tcf(c_10292,plain,
( midp(sK20,sK21,sK21)
| ~ midp(sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_10193]) ).
tcf(c_10307,plain,
( midp(sK20,sK21,sK20)
| ~ midp(sK20,sK20,sK21)
| ~ para(sK20,sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_10133]) ).
tcf(c_10789,plain,
para(sK26,sK23,sK26,sK23),
inference(superposition,[status(thm)],[c_4306,c_7030]) ).
tcf(c_10794,plain,
! [X0: $i] :
( midp(sK23,X0,sK23)
| ~ midp(sK26,X0,sK26)
| ~ coll(sK23,X0,sK23) ),
inference(superposition,[status(thm)],[c_10789,c_94]) ).
tcf(c_10799,plain,
coll(sK26,sK23,sK23),
inference(superposition,[status(thm)],[c_10789,c_115]) ).
tcf(c_10809,plain,
coll(sK23,sK26,sK23),
inference(superposition,[status(thm)],[c_10799,c_50]) ).
tcf(c_10964,plain,
coll(sK21,sK28,sK21),
inference(superposition,[status(thm)],[c_8540,c_49]) ).
tcf(c_10965,plain,
coll(sK24,sK28,sK21),
inference(superposition,[status(thm)],[c_8540,c_6157]) ).
tcf(c_11143,plain,
coll(sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_5900,c_6047]) ).
tcf(c_11588,plain,
coll(sK21,sK25,sK28),
inference(superposition,[status(thm)],[c_8926,c_6041]) ).
tcf(c_11595,plain,
coll(sK20,sK28,sK22),
inference(superposition,[status(thm)],[c_8935,c_6031]) ).
tcf(c_11623,plain,
coll(sK20,sK25,sK28),
inference(superposition,[status(thm)],[c_8937,c_49]) ).
tcf(c_11764,plain,
coll(sK26,sK20,sK20),
inference(superposition,[status(thm)],[c_6375,c_6048]) ).
tcf(c_12100,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK20,X0,X1)
| ~ para(sK20,sK20,sK21,sK21)
| ~ para(sK21,sK21,X0,X1) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_12104,plain,
( para(sK21,sK21,sK20,sK20)
| ~ para(sK20,sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_12111,plain,
( para(sK20,sK20,sK20,sK20)
| ~ para(sK21,sK21,sK20,sK20)
| ~ para(sK20,sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_12100]) ).
tcf(c_12359,plain,
! [X0: $i] :
( coll(sK21,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_9999,c_51]) ).
tcf(c_12365,plain,
( coll(sK21,sK20,sK22)
| ~ coll(sK22,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_12359]) ).
tcf(c_12448,plain,
cong(sK23,sK20,sK23,sK20),
inference(superposition,[status(thm)],[c_6745,c_7466]) ).
tcf(c_12818,plain,
coll(sK28,sK21,sK21),
inference(superposition,[status(thm)],[c_10964,c_50]) ).
tcf(c_12820,plain,
coll(sK22,sK21,sK21),
inference(superposition,[status(thm)],[c_10964,c_6044]) ).
tcf(c_12825,plain,
coll(sK24,sK21,sK28),
inference(superposition,[status(thm)],[c_10965,c_49]) ).
tcf(c_12944,plain,
( midp(sK23,sK26,sK23)
| ~ midp(sK26,sK26,sK26) ),
inference(superposition,[status(thm)],[c_10809,c_10794]) ).
tcf(c_12953,plain,
coll(sK26,sK26,sK21),
inference(superposition,[status(thm)],[c_5909,c_6051]) ).
tcf(c_13156,plain,
coll(sK21,sK22,sK21),
inference(superposition,[status(thm)],[c_11143,c_49]) ).
tcf(c_13175,plain,
coll(sK21,sK28,sK25),
inference(superposition,[status(thm)],[c_11588,c_49]) ).
tcf(c_13335,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK26,X0,sK22,X2)
| ~ midp(sK28,X1,X2)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_6500,c_6824]) ).
tcf(c_13374,plain,
! [X0: $i] :
( para(sK26,sK26,sK22,X0)
| ~ midp(sK28,sK21,X0) ),
inference(superposition,[status(thm)],[c_4307,c_13335]) ).
tcf(c_13375,plain,
! [X0: $i] :
( para(sK26,sK27,sK22,X0)
| ~ midp(sK28,sK22,X0) ),
inference(superposition,[status(thm)],[c_4305,c_13335]) ).
tcf(c_13403,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X0,X1)
| ~ midp(sK28,sK21,X1)
| ~ midp(sK26,X0,sK22)
| ~ coll(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_13374,c_94]) ).
tcf(c_13405,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK26,sK26,X1,X2)
| ~ midp(sK28,sK21,X0)
| ~ para(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_13374,c_54]) ).
tcf(c_13407,plain,
! [X0: $i] :
( para(sK26,sK26,X0,sK22)
| ~ midp(sK28,sK21,X0) ),
inference(superposition,[status(thm)],[c_13374,c_52]) ).
tcf(c_13496,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK26,sK27,X1,X2)
| ~ midp(sK28,sK22,X0)
| ~ para(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_13375,c_54]) ).
tcf(c_13972,plain,
coll(sK28,sK20,sK22),
inference(superposition,[status(thm)],[c_11595,c_50]) ).
tcf(c_13973,plain,
coll(sK20,sK22,sK28),
inference(superposition,[status(thm)],[c_11595,c_49]) ).
tcf(c_13985,plain,
coll(sK22,sK28,sK20),
inference(superposition,[status(thm)],[c_11623,c_6029]) ).
tcf(c_14037,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X0,sK22)
| ~ midp(sK28,sK21,X1)
| ~ coll(sK26,X0,sK22)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_13407,c_94]) ).
tcf(c_14064,plain,
( midp(sK26,sK20,sK22)
| ~ midp(sK28,sK21,sK20)
| ~ midp(sK26,sK20,sK20)
| ~ coll(sK26,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_14037]) ).
tcf(c_14270,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK20,X2,sK26,X0)
| ~ midp(sK26,X2,X1)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_6391,c_6831]) ).
tcf(c_14271,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK20,X0,sK22,X2)
| ~ midp(sK28,X1,X2)
| ~ midp(sK26,X0,X1) ),
inference(superposition,[status(thm)],[c_6500,c_6831]) ).
tcf(c_14301,plain,
( para(sK20,sK20,sK26,sK20)
| ~ midp(sK26,sK20,sK20)
| ~ midp(sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_14270]) ).
tcf(c_14365,plain,
! [X0: $i] :
( para(sK20,sK20,sK22,X0)
| ~ midp(sK28,sK21,X0) ),
inference(superposition,[status(thm)],[c_4307,c_14271]) ).
tcf(c_14366,plain,
! [X0: $i] :
( para(sK20,sK21,sK22,X0)
| ~ midp(sK28,sK20,X0) ),
inference(superposition,[status(thm)],[c_5862,c_14271]) ).
tcf(c_14728,plain,
! [X0: $i,X1: $i] :
( midp(X1,sK20,X0)
| ~ midp(sK28,sK21,X0)
| ~ midp(X1,sK20,sK22)
| ~ para(sK20,X0,sK22,sK20) ),
inference(superposition,[status(thm)],[c_14365,c_113]) ).
tcf(c_14730,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK20,sK20,X1,X2)
| ~ midp(sK28,sK21,X0)
| ~ perp(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_14365,c_58]) ).
tcf(c_14773,plain,
! [X0: $i] :
( para(sK20,sK21,X0,sK22)
| ~ midp(sK28,sK20,X0) ),
inference(superposition,[status(thm)],[c_14366,c_52]) ).
tcf(c_14792,plain,
( para(sK20,sK21,sK20,sK22)
| ~ midp(sK28,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_14773]) ).
tcf(c_16411,plain,
coll(sK21,sK24,sK28),
inference(superposition,[status(thm)],[c_12825,c_50]) ).
tcf(c_16419,plain,
coll(sK26,sK21,sK26),
inference(superposition,[status(thm)],[c_12953,c_49]) ).
tcf(c_16836,plain,
coll(sK24,sK27,sK20),
inference(superposition,[status(thm)],[c_8049,c_6191]) ).
tcf(c_16864,plain,
coll(sK22,sK25,sK21),
inference(superposition,[status(thm)],[c_13175,c_6044]) ).
tcf(c_16907,plain,
coll(sK22,sK20,sK28),
inference(superposition,[status(thm)],[c_13973,c_50]) ).
tcf(c_16909,plain,
coll(sK27,sK28,sK20),
inference(superposition,[status(thm)],[c_13973,c_6049]) ).
tcf(c_16984,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X1,X0)
| ~ midp(sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_17228,plain,
coll(sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_13985,c_6047]) ).
tcf(c_17408,plain,
! [X0: $i,X1: $i] :
( para(sK20,X0,X1,sK26)
| ~ para(sK20,X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_17409,plain,
( para(sK20,sK20,sK20,sK26)
| ~ para(sK20,sK20,sK26,sK20) ),
inference(instantiation,[status(thm)],[c_17408]) ).
tcf(c_17685,plain,
coll(sK20,sK28,sK21),
inference(superposition,[status(thm)],[c_16411,c_6030]) ).
tcf(c_17918,plain,
( circle(sK25,sK20,sK22,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6716,c_7336]) ).
tcf(c_17982,plain,
coll(sK24,sK20,sK27),
inference(superposition,[status(thm)],[c_16836,c_49]) ).
tcf(c_17995,plain,
( perp(sK20,sK23,sK24,sK25)
| ~ perp(sK24,sK25,sK20,sK23) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_18041,plain,
coll(sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_16864,c_6031]) ).
tcf(c_18048,plain,
( perp(sK20,sK22,sK22,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ coll(sK25,sK20,sK22) ),
inference(superposition,[status(thm)],[c_17918,c_102]) ).
tcf(c_18049,plain,
( perp(sK20,sK22,sK22,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18048,c_4298]) ).
tcf(c_18058,plain,
( perp(sK22,sK22,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_18049,c_56]) ).
tcf(c_18064,plain,
! [X0: $i] :
( cong(sK20,X0,sK22,X0)
| ~ midp(sK21,sK20,sK22)
| ~ midp(X0,sK20,sK22) ),
inference(superposition,[status(thm)],[c_18049,c_101]) ).
tcf(c_18345,plain,
! [X0: $i] :
( cong(sK20,X0,X0,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ midp(X0,sK20,sK22) ),
inference(superposition,[status(thm)],[c_18064,c_71]) ).
tcf(c_18361,plain,
( cong(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_18345]) ).
tcf(c_18481,plain,
coll(sK27,sK28,sK22),
inference(superposition,[status(thm)],[c_16907,c_6052]) ).
tcf(c_18487,plain,
coll(sK27,sK20,sK28),
inference(superposition,[status(thm)],[c_16909,c_49]) ).
tcf(c_18971,plain,
coll(sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_11143,c_6256]) ).
tcf(c_19044,plain,
coll(sK26,sK22,sK21),
inference(superposition,[status(thm)],[c_17228,c_6051]) ).
tcf(c_19472,plain,
! [X0: $i,X1: $i] :
( midp(sK26,X0,X1)
| ~ coll(sK26,X0,X1)
| ~ cong(sK26,X0,sK26,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_19473,plain,
( midp(sK26,sK20,sK20)
| ~ coll(sK26,sK20,sK20)
| ~ cong(sK26,sK20,sK26,sK20) ),
inference(instantiation,[status(thm)],[c_19472]) ).
tcf(c_19474,plain,
! [X0: $i,X1: $i] :
( midp(sK27,X0,X1)
| ~ coll(sK27,X0,X1)
| ~ cong(sK27,X0,sK27,X1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_19475,plain,
( midp(sK27,sK20,sK20)
| ~ coll(sK27,sK20,sK20)
| ~ cong(sK27,sK20,sK27,sK20) ),
inference(instantiation,[status(thm)],[c_19474]) ).
tcf(c_19759,plain,
( perp(sK20,sK20,sK20,sK22)
| ~ midp(sK28,sK21,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_18058,c_14730]) ).
tcf(c_19762,plain,
( perp(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_19759,c_4303]) ).
tcf(c_19779,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK20,X0,X1)
| ~ midp(sK21,sK20,sK22)
| ~ perp(sK20,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_19762,c_57]) ).
tcf(c_19780,plain,
( cong(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK22) ),
inference(superposition,[status(thm)],[c_19762,c_104]) ).
tcf(c_19781,plain,
( perp(sK20,sK22,sK20,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_19762,c_56]) ).
tcf(c_19852,plain,
( para(sK25,sK21,sK20,sK20)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_19781,c_7024]) ).
tcf(c_19895,plain,
! [X0: $i,X1: $i] :
( perp(sK25,sK21,X0,X1)
| ~ midp(sK21,sK20,sK22)
| ~ perp(sK20,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_19852,c_58]) ).
tcf(c_19915,plain,
( perp(sK25,sK21,sK20,sK20)
| ~ midp(sK21,sK20,sK22)
| ~ perp(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_19895]) ).
tcf(c_19932,plain,
coll(sK26,sK28,sK21),
inference(superposition,[status(thm)],[c_8540,c_6281]) ).
tcf(c_19996,plain,
coll(sK20,sK21,sK28),
inference(superposition,[status(thm)],[c_17685,c_49]) ).
tcf(c_20029,plain,
( cong(sK20,sK20,sK20,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(global_subsumption_just,[status(thm)],[c_19780,c_163,c_178,c_182,c_187,c_236,c_5863,c_5898,c_6119,c_6193,c_6237,c_7119,c_7578,c_8565,c_8760,c_9657,c_12104,c_12111,c_18361,c_19915]) ).
tcf(c_20339,plain,
! [X0: $i] :
( cong(sK26,sK20,sK26,X0)
| ~ cong(sK26,sK20,sK26,sK21)
| ~ cong(sK26,sK21,sK26,X0) ),
inference(instantiation,[status(thm)],[c_7886]) ).
tcf(c_20341,plain,
( cong(sK26,sK20,sK26,sK20)
| ~ cong(sK26,sK21,sK26,sK20)
| ~ cong(sK26,sK20,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_20339]) ).
tcf(c_20411,plain,
coll(sK27,sK21,sK22),
inference(superposition,[status(thm)],[c_9999,c_6296]) ).
tcf(c_20433,plain,
coll(sK20,sK24,sK27),
inference(superposition,[status(thm)],[c_17982,c_50]) ).
tcf(c_20435,plain,
coll(sK21,sK27,sK24),
inference(superposition,[status(thm)],[c_17982,c_6024]) ).
tcf(c_20449,plain,
! [X0: $i] :
( cong(sK27,sK20,sK27,X0)
| ~ cong(sK27,sK20,sK27,sK22)
| ~ cong(sK27,sK22,sK27,X0) ),
inference(instantiation,[status(thm)],[c_7994]) ).
tcf(c_20451,plain,
( cong(sK27,sK20,sK27,sK20)
| ~ cong(sK27,sK22,sK27,sK20)
| ~ cong(sK27,sK20,sK27,sK22) ),
inference(instantiation,[status(thm)],[c_20449]) ).
tcf(c_20489,plain,
coll(sK26,sK22,sK20),
inference(superposition,[status(thm)],[c_18041,c_6048]) ).
tcf(c_20537,plain,
coll(sK21,sK24,sK27),
inference(superposition,[status(thm)],[c_20435,c_49]) ).
tcf(c_20745,plain,
( para(sK20,sK20,sK22,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_18049,c_19779]) ).
tcf(c_20878,plain,
coll(sK22,sK28,sK27),
inference(superposition,[status(thm)],[c_18487,c_6037]) ).
tcf(c_20936,plain,
coll(sK28,sK27,sK22),
inference(superposition,[status(thm)],[c_18481,c_50]) ).
tcf(c_20943,plain,
coll(sK27,sK21,sK20),
inference(superposition,[status(thm)],[c_18971,c_6049]) ).
tcf(c_21003,plain,
para(sK20,sK20,sK22,sK22),
inference(global_subsumption_just,[status(thm)],[c_20745,c_165,c_9690]) ).
tcf(c_21009,plain,
para(sK22,sK22,sK20,sK20),
inference(superposition,[status(thm)],[c_21003,c_53]) ).
tcf(c_21375,plain,
coll(sK22,sK26,sK21),
inference(superposition,[status(thm)],[c_19044,c_50]) ).
tcf(c_21376,plain,
coll(sK26,sK21,sK22),
inference(superposition,[status(thm)],[c_19044,c_49]) ).
tcf(c_21968,plain,
coll(sK26,sK28,sK20),
inference(superposition,[status(thm)],[c_19996,c_6048]) ).
tcf(c_21999,plain,
coll(sK28,sK26,sK21),
inference(superposition,[status(thm)],[c_19932,c_50]) ).
tcf(c_23620,plain,
coll(sK21,sK27,sK20),
inference(superposition,[status(thm)],[c_20433,c_6028]) ).
tcf(c_23652,plain,
coll(sK27,sK22,sK21),
inference(superposition,[status(thm)],[c_20411,c_49]) ).
tcf(c_23679,plain,
coll(sK26,sK20,sK22),
inference(superposition,[status(thm)],[c_20489,c_49]) ).
tcf(c_23801,plain,
( midp(sK21,sK21,sK26)
| ~ midp(sK27,sK21,sK22)
| ~ midp(sK21,sK20,sK26) ),
inference(superposition,[status(thm)],[c_6280,c_8585]) ).
tcf(c_24705,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK21,X3,sK22,X2)
| ~ para(sK21,X3,X0,X1)
| ~ para(X0,X1,sK22,X2) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_24706,plain,
( para(sK21,sK20,sK22,sK20)
| ~ para(sK21,sK20,sK20,sK20)
| ~ para(sK20,sK20,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_24705]) ).
tcf(c_24946,plain,
! [X0: $i,X1: $i] :
( perp(sK24,sK25,sK20,sK23)
| ~ perp(X0,X1,sK20,sK23)
| ~ para(sK24,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_24947,plain,
( perp(sK24,sK25,sK20,sK23)
| ~ perp(sK20,sK20,sK20,sK23)
| ~ para(sK24,sK25,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_24946]) ).
tcf(c_25181,plain,
! [X0: $i] :
( coll(sK27,X0,sK21)
| ~ coll(sK21,sK24,X0) ),
inference(superposition,[status(thm)],[c_20537,c_51]) ).
tcf(c_25194,plain,
( coll(sK27,sK20,sK21)
| ~ coll(sK21,sK24,sK20) ),
inference(instantiation,[status(thm)],[c_25181]) ).
tcf(c_25267,plain,
coll(sK22,sK27,sK28),
inference(superposition,[status(thm)],[c_20878,c_49]) ).
tcf(c_25478,plain,
coll(sK27,sK20,sK21),
inference(superposition,[status(thm)],[c_20943,c_49]) ).
tcf(c_25491,plain,
coll(sK22,sK21,sK26),
inference(superposition,[status(thm)],[c_21375,c_49]) ).
tcf(c_25517,plain,
coll(sK20,sK22,sK26),
inference(superposition,[status(thm)],[c_21376,c_6039]) ).
tcf(c_25685,plain,
( midp(sK26,sK20,sK20)
| ~ midp(sK28,sK20,sK22)
| ~ midp(sK26,sK21,sK20) ),
inference(superposition,[status(thm)],[c_11764,c_8586]) ).
tcf(c_26505,plain,
( midp(sK26,sK20,sK20)
| ~ midp(sK28,sK20,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25685,c_5862]) ).
tcf(c_27350,plain,
coll(sK28,sK21,sK26),
inference(superposition,[status(thm)],[c_21999,c_49]) ).
tcf(c_27551,plain,
midp(sK26,sK20,sK20),
inference(global_subsumption_just,[status(thm)],[c_26505,c_163,c_5862,c_6117,c_6273,c_6375,c_7399,c_19473,c_20341]) ).
tcf(c_27694,plain,
coll(sK21,sK20,sK27),
inference(superposition,[status(thm)],[c_23620,c_49]) ).
tcf(c_27726,plain,
coll(sK22,sK27,sK21),
inference(superposition,[status(thm)],[c_23652,c_50]) ).
tcf(c_27728,plain,
coll(sK20,sK21,sK27),
inference(superposition,[status(thm)],[c_23652,c_6040]) ).
tcf(c_27838,plain,
( midp(sK21,sK26,sK20)
| ~ midp(sK26,sK21,sK20)
| ~ midp(sK20,sK26,sK21) ),
inference(superposition,[status(thm)],[c_5896,c_8596]) ).
tcf(c_28896,plain,
( midp(sK21,sK26,sK20)
| ~ midp(sK20,sK26,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27838,c_5862]) ).
tcf(c_30315,plain,
( midp(sK22,sK27,sK28)
| ~ midp(sK22,sK20,sK28)
| ~ midp(sK26,sK27,sK21) ),
inference(superposition,[status(thm)],[c_25267,c_8584]) ).
tcf(c_30482,plain,
coll(sK28,sK26,sK22),
inference(superposition,[status(thm)],[c_25491,c_6053]) ).
tcf(c_30529,plain,
coll(sK27,sK26,sK20),
inference(superposition,[status(thm)],[c_25517,c_6049]) ).
tcf(c_32787,plain,
coll(sK21,sK28,sK26),
inference(superposition,[status(thm)],[c_27350,c_50]) ).
tcf(c_33284,plain,
coll(sK26,sK27,sK21),
inference(superposition,[status(thm)],[c_27694,c_6051]) ).
tcf(c_33444,plain,
( midp(sK22,sK27,sK21)
| ~ midp(sK28,sK27,sK22)
| ~ midp(sK22,sK21,sK21) ),
inference(superposition,[status(thm)],[c_27726,c_8586]) ).
tcf(c_33478,plain,
coll(sK26,sK27,sK20),
inference(superposition,[status(thm)],[c_27728,c_6048]) ).
tcf(c_33537,plain,
( midp(sK24,sK20,sK21)
| ~ midp(sK28,sK24,sK21)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_4300,c_8598]) ).
tcf(c_33538,plain,
( midp(sK25,sK20,sK22)
| ~ midp(sK28,sK25,sK22)
| ~ midp(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_4298,c_8598]) ).
tcf(c_33713,plain,
( midp(sK22,sK21,sK21)
| ~ midp(sK28,sK22,sK21)
| ~ midp(sK21,sK21,sK22) ),
inference(superposition,[status(thm)],[c_12820,c_8598]) ).
tcf(c_34303,plain,
( midp(sK22,sK21,sK21)
| ~ midp(sK21,sK21,sK22) ),
inference(forward_subsumption_resolution,[status(thm)],[c_33713,c_5864]) ).
tcf(c_35425,plain,
! [X0: $i,X1: $i] :
( midp(sK22,sK20,sK21)
| ~ midp(sK22,X0,X1)
| ~ para(X0,sK21,X1,sK20)
| ~ para(X0,sK20,X1,sK21) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_35426,plain,
( midp(sK22,sK20,sK21)
| ~ midp(sK22,sK20,sK20)
| ~ para(sK20,sK21,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_35425]) ).
tcf(c_35467,plain,
! [X0: $i,X1: $i] :
( midp(sK21,sK20,sK22)
| ~ coll(sK21,sK20,sK22)
| ~ midp(X0,sK20,X1)
| ~ para(X0,sK21,X1,sK22) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_35468,plain,
( midp(sK21,sK20,sK22)
| ~ midp(sK20,sK20,sK20)
| ~ coll(sK21,sK20,sK22)
| ~ para(sK20,sK21,sK20,sK22) ),
inference(instantiation,[status(thm)],[c_35467]) ).
tcf(c_35669,plain,
midp(sK24,sK20,sK21),
inference(global_subsumption_just,[status(thm)],[c_33537,c_165,c_163,c_178,c_182,c_236,c_5863,c_5862,c_5898,c_6116,c_6117,c_6119,c_6132,c_6193,c_6237,c_6243,c_6273,c_6274,c_6375,c_6584,c_6899,c_6995,c_7399,c_7560,c_8565,c_8748,c_8760,c_9006,c_9657,c_12104,c_12111,c_19473,c_19475,c_20341,c_20451,c_35426]) ).
tcf(c_35675,plain,
! [X0: $i] :
( para(sK26,sK24,sK22,X0)
| ~ midp(sK28,sK21,X0) ),
inference(superposition,[status(thm)],[c_35669,c_13335]) ).
tcf(c_35685,plain,
midp(sK25,sK20,sK22),
inference(global_subsumption_just,[status(thm)],[c_33538,c_167,c_165,c_163,c_178,c_182,c_236,c_5863,c_5862,c_6116,c_6117,c_6193,c_6237,c_6266,c_6273,c_6274,c_6375,c_6426,c_6518,c_6638,c_6899,c_7344,c_7399,c_7560,c_8565,c_9657,c_12104,c_12111,c_12365,c_14792,c_19473,c_19475,c_20341,c_20451,c_24706,c_35468]) ).
tcf(c_36616,plain,
! [X0: $i,X1: $i] :
( midp(sK24,X0,X1)
| ~ midp(sK28,sK21,X1)
| ~ midp(sK26,X0,sK22)
| ~ coll(sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_35675,c_94]) ).
tcf(c_36643,plain,
( midp(sK24,sK20,sK20)
| ~ midp(sK28,sK21,sK20)
| ~ midp(sK26,sK20,sK22)
| ~ coll(sK24,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_36616]) ).
tcf(c_37101,plain,
( midp(sK26,sK27,sK20)
| ~ midp(sK27,sK26,sK20)
| ~ midp(sK20,sK27,sK22) ),
inference(superposition,[status(thm)],[c_33478,c_8597]) ).
tcf(c_38323,plain,
( midp(sK26,sK21,sK26)
| ~ midp(sK28,sK21,sK26)
| ~ midp(sK26,sK21,sK22) ),
inference(superposition,[status(thm)],[c_16419,c_13403]) ).
tcf(c_40191,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK28,sK21,X1)
| ~ midp(sK28,X0,X2)
| ~ para(X0,sK21,X2,X1)
| ~ para(X0,X1,X2,sK21) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_40192,plain,
( midp(sK28,sK21,sK20)
| ~ midp(sK28,sK20,sK20)
| ~ para(sK20,sK21,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_40191]) ).
tcf(c_41761,plain,
( cong(sK21,sK20,sK21,sK22)
| ~ midp(sK25,sK20,sK22) ),
inference(superposition,[status(thm)],[c_6012,c_104]) ).
tcf(c_41770,plain,
cong(sK21,sK20,sK21,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_41761,c_35685]) ).
tcf(c_41995,plain,
( midp(sK21,sK20,sK22)
| ~ coll(sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_41770,c_116]) ).
tcf(c_42006,plain,
midp(sK21,sK20,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_41995,c_17228]) ).
tcf(c_42050,plain,
cong(sK20,sK20,sK20,sK22),
inference(backward_subsumption_resolution,[status(thm)],[c_20029,c_42006]) ).
tcf(c_42895,plain,
( para(sK26,sK27,sK21,sK22)
| ~ midp(sK28,sK22,sK21) ),
inference(superposition,[status(thm)],[c_7832,c_13496]) ).
tcf(c_42911,plain,
para(sK26,sK27,sK21,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_42895,c_5864]) ).
tcf(c_43337,plain,
para(sK26,sK27,sK22,sK21),
inference(superposition,[status(thm)],[c_42911,c_52]) ).
tcf(c_43482,plain,
! [X0: $i] :
( midp(X0,sK20,sK20)
| ~ midp(sK28,sK21,sK20)
| ~ midp(X0,sK20,sK22) ),
inference(superposition,[status(thm)],[c_14365,c_14728]) ).
tcf(c_43501,plain,
! [X0: $i] :
( midp(X0,sK20,sK20)
| ~ midp(X0,sK20,sK22) ),
inference(global_subsumption_just,[status(thm)],[c_43482,c_167,c_165,c_163,c_5863,c_5862,c_6116,c_6117,c_6273,c_6274,c_6375,c_6426,c_6518,c_6584,c_6638,c_6899,c_7399,c_7560,c_9006,c_19473,c_19475,c_20341,c_20451,c_24706,c_40192,c_43482]) ).
tcf(c_43511,plain,
midp(sK27,sK20,sK20),
inference(superposition,[status(thm)],[c_4305,c_43501]) ).
tcf(c_43512,plain,
midp(sK25,sK20,sK20),
inference(superposition,[status(thm)],[c_35685,c_43501]) ).
tcf(c_44427,plain,
( midp(sK23,sK20,sK20)
| ~ coll(sK23,sK20,sK20) ),
inference(superposition,[status(thm)],[c_12448,c_116]) ).
tcf(c_44681,plain,
( para(sK26,sK26,sK20,sK20)
| ~ midp(sK28,sK21,sK22) ),
inference(superposition,[status(thm)],[c_21009,c_13405]) ).
tcf(c_44694,plain,
para(sK26,sK26,sK20,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_44681,c_4303]) ).
tcf(c_44914,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK26,X0,X1)
| ~ para(sK20,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_44694,c_54]) ).
tcf(c_44915,plain,
para(sK20,sK20,sK26,sK26),
inference(superposition,[status(thm)],[c_44694,c_53]) ).
tcf(c_45020,plain,
para(sK26,sK26,sK26,sK26),
inference(superposition,[status(thm)],[c_44915,c_44914]) ).
tcf(c_48268,plain,
perp(sK26,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_4306,c_56]) ).
tcf(c_48270,plain,
perp(sK28,sK23,sK21,sK22),
inference(superposition,[status(thm)],[c_4302,c_56]) ).
tcf(c_48859,plain,
! [X0: $i,X1: $i] :
( para(sK26,sK23,X0,X1)
| ~ perp(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_48268,c_57]) ).
tcf(c_48861,plain,
! [X0: $i,X1: $i] :
( para(sK28,sK23,X0,X1)
| ~ perp(sK21,sK22,X0,X1) ),
inference(superposition,[status(thm)],[c_48270,c_57]) ).
tcf(c_54413,plain,
para(sK26,sK23,sK26,sK23),
inference(superposition,[status(thm)],[c_4306,c_48859]) ).
tcf(c_54427,plain,
coll(sK26,sK23,sK23),
inference(superposition,[status(thm)],[c_54413,c_115]) ).
tcf(c_54444,plain,
coll(sK23,sK26,sK23),
inference(superposition,[status(thm)],[c_54427,c_50]) ).
tcf(c_54739,plain,
( midp(sK20,sK20,sK22)
| ~ coll(sK20,sK20,sK22) ),
inference(superposition,[status(thm)],[c_42050,c_116]) ).
tcf(c_54752,plain,
midp(sK20,sK20,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_54739,c_6476]) ).
tcf(c_55490,plain,
midp(sK20,sK22,sK20),
inference(superposition,[status(thm)],[c_54752,c_59]) ).
tcf(c_57636,plain,
! [X0: $i] :
( midp(sK27,X0,sK21)
| ~ midp(sK26,X0,sK22)
| ~ coll(sK27,X0,sK21) ),
inference(superposition,[status(thm)],[c_43337,c_94]) ).
tcf(c_57653,plain,
( midp(sK27,sK20,sK21)
| ~ midp(sK26,sK20,sK22)
| ~ coll(sK27,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_57636]) ).
tcf(c_59889,plain,
para(sK28,sK23,sK28,sK23),
inference(superposition,[status(thm)],[c_4302,c_48861]) ).
tcf(c_59927,plain,
! [X0: $i] :
( midp(sK23,X0,sK23)
| ~ midp(sK28,X0,sK28)
| ~ coll(sK23,X0,sK23) ),
inference(superposition,[status(thm)],[c_59889,c_94]) ).
tcf(c_60212,plain,
coll(sK26,sK26,sK26),
inference(superposition,[status(thm)],[c_45020,c_115]) ).
tcf(c_60494,plain,
( midp(sK26,sK26,sK26)
| ~ midp(sK28,sK26,sK22)
| ~ midp(sK26,sK21,sK26) ),
inference(superposition,[status(thm)],[c_60212,c_8586]) ).
tcf(c_60737,plain,
! [X0: $i] :
( midp(sK26,X0,sK28)
| ~ midp(sK26,sK28,X0) ),
inference(instantiation,[status(thm)],[c_16984]) ).
tcf(c_60738,plain,
( midp(sK26,sK20,sK28)
| ~ midp(sK26,sK28,sK20) ),
inference(instantiation,[status(thm)],[c_60737]) ).
tcf(c_60834,plain,
( midp(sK20,sK26,sK21)
| ~ midp(sK26,sK26,sK20)
| ~ midp(sK20,sK21,sK21) ),
inference(superposition,[status(thm)],[c_5890,c_8587]) ).
tcf(c_60847,plain,
( midp(sK28,sK20,sK22)
| ~ midp(sK28,sK21,sK22)
| ~ midp(sK26,sK20,sK20) ),
inference(superposition,[status(thm)],[c_13972,c_8587]) ).
tcf(c_60863,plain,
( midp(sK20,sK26,sK20)
| ~ midp(sK26,sK26,sK20)
| ~ midp(sK20,sK21,sK20) ),
inference(superposition,[status(thm)],[c_9784,c_8587]) ).
tcf(c_60867,plain,
( midp(sK20,sK20,sK26)
| ~ midp(sK26,sK20,sK20)
| ~ midp(sK20,sK21,sK26) ),
inference(superposition,[status(thm)],[c_7904,c_8587]) ).
tcf(c_61110,plain,
( midp(sK28,sK27,sK22)
| ~ midp(sK28,sK21,sK22)
| ~ midp(sK26,sK27,sK20) ),
inference(superposition,[status(thm)],[c_20936,c_8587]) ).
tcf(c_61120,plain,
( midp(sK28,sK26,sK21)
| ~ midp(sK28,sK21,sK21)
| ~ midp(sK26,sK26,sK20) ),
inference(superposition,[status(thm)],[c_21999,c_8587]) ).
tcf(c_61169,plain,
( midp(sK28,sK26,sK22)
| ~ midp(sK28,sK21,sK22)
| ~ midp(sK26,sK26,sK20) ),
inference(superposition,[status(thm)],[c_30482,c_8587]) ).
tcf(c_61170,plain,
( midp(sK27,sK26,sK20)
| ~ midp(sK27,sK21,sK20)
| ~ midp(sK26,sK26,sK20) ),
inference(superposition,[status(thm)],[c_30529,c_8587]) ).
tcf(c_61508,plain,
( midp(sK28,sK26,sK22)
| ~ midp(sK26,sK26,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_61169,c_4303]) ).
tcf(c_61646,plain,
( midp(sK28,sK27,sK22)
| ~ midp(sK26,sK27,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_61110,c_4303]) ).
tcf(c_62196,plain,
( midp(sK20,sK20,sK26)
| ~ midp(sK20,sK21,sK26) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60867,c_27551]) ).
tcf(c_62226,plain,
midp(sK28,sK20,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_60847,c_4303,c_27551]) ).
tcf(c_63754,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK24,sK25,X1,X2)
| ~ midp(sK25,X0,X2)
| ~ midp(sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_63755,plain,
( para(sK24,sK25,sK20,sK20)
| ~ midp(sK25,sK20,sK20)
| ~ midp(sK24,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_63754]) ).
tcf(c_63925,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK23,sK20,sK23)
| ~ midp(sK23,X0,X1)
| ~ perp(X0,sK20,sK20,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_63926,plain,
( cong(sK20,sK23,sK20,sK23)
| ~ midp(sK23,sK20,sK20)
| ~ perp(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_63925]) ).
tcf(c_64307,plain,
( midp(sK28,sK21,sK21)
| ~ midp(sK28,sK22,sK21)
| ~ midp(sK27,sK21,sK20) ),
inference(superposition,[status(thm)],[c_12818,c_8588]) ).
tcf(c_64444,plain,
( midp(sK27,sK20,sK21)
| ~ midp(sK27,sK22,sK21)
| ~ midp(sK27,sK20,sK20) ),
inference(superposition,[status(thm)],[c_25478,c_8588]) ).
tcf(c_64902,plain,
( midp(sK27,sK20,sK21)
| ~ midp(sK27,sK22,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_64444,c_43511]) ).
tcf(c_65229,plain,
( midp(sK28,sK21,sK21)
| ~ midp(sK27,sK21,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_64307,c_5864]) ).
tcf(c_66981,plain,
midp(sK27,sK20,sK21),
inference(global_subsumption_just,[status(thm)],[c_64902,c_167,c_165,c_163,c_5838,c_5863,c_5862,c_6116,c_6117,c_6273,c_6274,c_6375,c_6426,c_6518,c_6584,c_6638,c_6899,c_7399,c_7560,c_9006,c_14064,c_19473,c_19475,c_20341,c_20451,c_23679,c_24706,c_25194,c_40192,c_57653]) ).
tcf(c_66989,plain,
midp(sK27,sK21,sK20),
inference(superposition,[status(thm)],[c_66981,c_59]) ).
tcf(c_69498,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK20,sK23)
| ~ cong(X0,sK23,X1,sK23)
| ~ cong(X0,sK20,X1,sK20) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_69499,plain,
( perp(sK20,sK20,sK20,sK23)
| ~ cong(sK20,sK23,sK20,sK23)
| ~ cong(sK20,sK20,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_69498]) ).
tcf(c_70143,plain,
( midp(sK22,sK20,sK27)
| ~ midp(sK27,sK20,sK22)
| ~ midp(sK21,sK20,sK26) ),
inference(superposition,[status(thm)],[c_5911,c_8590]) ).
tcf(c_70416,plain,
( midp(sK26,sK28,sK20)
| ~ midp(sK21,sK28,sK26)
| ~ midp(sK20,sK20,sK26) ),
inference(superposition,[status(thm)],[c_21968,c_8590]) ).
tcf(c_70436,plain,
( midp(sK22,sK27,sK28)
| ~ midp(sK28,sK20,sK22)
| ~ midp(sK21,sK27,sK26) ),
inference(superposition,[status(thm)],[c_25267,c_8590]) ).
tcf(c_70444,plain,
( midp(sK28,sK21,sK26)
| ~ midp(sK21,sK21,sK26)
| ~ midp(sK26,sK20,sK28) ),
inference(superposition,[status(thm)],[c_27350,c_8590]) ).
tcf(c_70941,plain,
( midp(sK22,sK27,sK28)
| ~ midp(sK21,sK27,sK26) ),
inference(forward_subsumption_resolution,[status(thm)],[c_70436,c_62226]) ).
tcf(c_71670,plain,
( midp(sK22,sK20,sK27)
| ~ midp(sK21,sK20,sK26) ),
inference(forward_subsumption_resolution,[status(thm)],[c_70143,c_4305]) ).
tcf(c_73757,plain,
( midp(sK21,sK20,sK26)
| ~ midp(sK22,sK20,sK27)
| ~ midp(sK26,sK20,sK21) ),
inference(superposition,[status(thm)],[c_5909,c_8592]) ).
tcf(c_73783,plain,
( midp(sK22,sK20,sK28)
| ~ midp(sK28,sK20,sK22)
| ~ midp(sK22,sK20,sK27) ),
inference(superposition,[status(thm)],[c_16907,c_8592]) ).
tcf(c_74084,plain,
( midp(sK21,sK28,sK26)
| ~ midp(sK22,sK28,sK27)
| ~ midp(sK26,sK20,sK21) ),
inference(superposition,[status(thm)],[c_32787,c_8592]) ).
tcf(c_74466,plain,
( midp(sK21,sK28,sK26)
| ~ midp(sK22,sK28,sK27) ),
inference(forward_subsumption_resolution,[status(thm)],[c_74084,c_4307]) ).
tcf(c_75234,plain,
( midp(sK22,sK20,sK28)
| ~ midp(sK22,sK20,sK27) ),
inference(forward_subsumption_resolution,[status(thm)],[c_73783,c_62226]) ).
tcf(c_75267,plain,
( midp(sK21,sK20,sK26)
| ~ midp(sK22,sK20,sK27) ),
inference(forward_subsumption_resolution,[status(thm)],[c_73757,c_4307]) ).
tcf(c_77057,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X2,sK26,X0,X1)
| ~ para(X0,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_77058,plain,
( para(sK20,sK26,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK26) ),
inference(instantiation,[status(thm)],[c_77057]) ).
tcf(c_80429,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK26,sK26,X1)
| ~ midp(sK26,X0,X2)
| ~ para(X0,sK26,X2,X1)
| ~ para(X0,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_80430,plain,
( midp(sK26,sK26,sK20)
| ~ midp(sK26,sK20,sK20)
| ~ para(sK20,sK26,sK20,sK20)
| ~ para(sK20,sK20,sK20,sK26) ),
inference(instantiation,[status(thm)],[c_80429]) ).
tcf(c_81263,plain,
( midp(sK20,sK26,sK21)
| ~ midp(sK21,sK26,sK20)
| ~ midp(sK26,sK20,sK21) ),
inference(superposition,[status(thm)],[c_5890,c_8599]) ).
tcf(c_82715,plain,
( midp(sK20,sK26,sK21)
| ~ midp(sK21,sK26,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_81263,c_4307]) ).
tcf(c_82936,plain,
! [X0: $i] :
( coll(sK23,sK20,X0)
| ~ para(sK23,sK20,sK23,X0) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_82943,plain,
( coll(sK23,sK20,sK20)
| ~ para(sK23,sK20,sK23,sK20) ),
inference(instantiation,[status(thm)],[c_82936]) ).
tcf(c_84366,plain,
midp(sK20,sK26,sK21),
inference(global_subsumption_just,[status(thm)],[c_82715,c_163,c_178,c_182,c_236,c_5862,c_6117,c_6193,c_6237,c_6273,c_6375,c_7399,c_8565,c_9657,c_10292,c_12104,c_12111,c_14301,c_17409,c_19473,c_20341,c_60834,c_77058,c_80430]) ).
tcf(c_84368,plain,
midp(sK21,sK26,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_28896,c_84366]) ).
tcf(c_84372,plain,
midp(sK20,sK21,sK26),
inference(superposition,[status(thm)],[c_84366,c_59]) ).
tcf(c_84385,plain,
midp(sK21,sK20,sK26),
inference(superposition,[status(thm)],[c_84368,c_59]) ).
tcf(c_84390,plain,
midp(sK22,sK20,sK27),
inference(backward_subsumption_resolution,[status(thm)],[c_71670,c_84385]) ).
tcf(c_84436,plain,
( midp(sK20,sK27,sK22)
| ~ midp(sK22,sK27,sK20)
| ~ midp(sK27,sK20,sK22) ),
inference(superposition,[status(thm)],[c_5892,c_8600]) ).
tcf(c_85860,plain,
( midp(sK20,sK27,sK22)
| ~ midp(sK22,sK27,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_84436,c_4305]) ).
tcf(c_86585,plain,
( midp(sK23,sK26,sK23)
| ~ midp(sK28,sK26,sK28) ),
inference(superposition,[status(thm)],[c_54444,c_59927]) ).
tcf(c_87292,plain,
midp(sK22,sK27,sK20),
inference(superposition,[status(thm)],[c_84390,c_59]) ).
tcf(c_87314,plain,
midp(sK20,sK27,sK22),
inference(backward_subsumption_resolution,[status(thm)],[c_85860,c_87292]) ).
tcf(c_87655,plain,
( midp(sK27,sK21,sK22)
| ~ midp(sK28,sK27,sK22)
| ~ midp(sK22,sK21,sK21) ),
inference(superposition,[status(thm)],[c_20411,c_8601]) ).
tcf(c_87674,plain,
( midp(sK26,sK21,sK22)
| ~ midp(sK28,sK26,sK22)
| ~ midp(sK22,sK21,sK21) ),
inference(superposition,[status(thm)],[c_21376,c_8601]) ).
tcf(c_87735,plain,
( midp(sK26,sK27,sK21)
| ~ midp(sK28,sK26,sK21)
| ~ midp(sK22,sK27,sK21) ),
inference(superposition,[status(thm)],[c_33284,c_8601]) ).
tcf(c_89938,plain,
( midp(sK21,sK22,sK21)
| ~ midp(sK20,sK22,sK20) ),
inference(superposition,[status(thm)],[c_13156,c_8602]) ).
tcf(c_89945,plain,
midp(sK21,sK22,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_89938,c_55490]) ).
tcf(c_90492,plain,
midp(sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_89945,c_59]) ).
tcf(c_90497,plain,
midp(sK22,sK21,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_34303,c_90492]) ).
tcf(c_90706,plain,
midp(sK22,sK27,sK28),
inference(global_subsumption_just,[status(thm)],[c_70941,c_163,c_178,c_182,c_236,c_5862,c_6117,c_6193,c_6237,c_6273,c_6375,c_7399,c_8565,c_9657,c_12104,c_12111,c_14301,c_17409,c_19473,c_20341,c_30315,c_33444,c_37101,c_61646,c_61170,c_61120,c_65229,c_66989,c_75234,c_77058,c_80430,c_84390,c_87314,c_87735,c_90497]) ).
tcf(c_90711,plain,
midp(sK22,sK28,sK27),
inference(superposition,[status(thm)],[c_90706,c_59]) ).
tcf(c_90716,plain,
midp(sK21,sK28,sK26),
inference(backward_subsumption_resolution,[status(thm)],[c_74466,c_90711]) ).
tcf(c_91868,plain,
midp(sK23,sK26,sK23),
inference(global_subsumption_just,[status(thm)],[c_86585,c_163,c_178,c_182,c_236,c_5862,c_6117,c_6193,c_6237,c_6273,c_6375,c_7399,c_8565,c_9657,c_12104,c_12111,c_12944,c_14301,c_17409,c_19473,c_20341,c_23801,c_37101,c_38323,c_60494,c_60738,c_62196,c_61646,c_61508,c_61170,c_66989,c_70444,c_70416,c_75267,c_77058,c_80430,c_84372,c_84390,c_87314,c_87674,c_87655,c_90497,c_90716]) ).
tcf(c_91871,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK23,X1)
| ~ midp(X0,sK26,X1) ),
inference(superposition,[status(thm)],[c_91868,c_93]) ).
tcf(c_91878,plain,
( para(sK23,sK20,sK23,sK20)
| ~ midp(sK20,sK26,sK20) ),
inference(instantiation,[status(thm)],[c_91871]) ).
tcf(c_91879,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_91878,c_82943,c_80430,c_77058,c_69499,c_63926,c_63755,c_60863,c_44427,c_43512,c_40192,c_36643,c_24947,c_24706,c_23679,c_20451,c_20341,c_19475,c_19473,c_17995,c_17409,c_14301,c_14064,c_12111,c_12104,c_10307,c_9657,c_9006,c_8761,c_8565,c_7560,c_7399,c_6899,c_6638,c_6584,c_6518,c_6426,c_6375,c_6274,c_6273,c_6237,c_6233,c_6193,c_6120,c_6117,c_6116,c_5896,c_5862,c_5863,c_236,c_187,c_182,c_178,c_162,c_163,c_165,c_167]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO568+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 12:23:37 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 25.97/5.78 % SZS status Started for theBenchmark.p
% 25.97/5.78 % SZS status Theorem for theBenchmark.p
% 25.97/5.78
% 25.97/5.78 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 25.97/5.78
% 25.97/5.78 % ------ iProver source info
% 25.97/5.78
% 25.97/5.78 % git: date: 2026-07-19 20:42:38 +0200
% 25.97/5.78 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 25.97/5.78 % git: non_committed_changes: false
% 25.97/5.78
% 25.97/5.78 % ------ Parsing...
% 25.97/5.78 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 25.97/5.78
% 25.97/5.78 % ------ 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 %
% 25.97/5.78
% 25.97/5.78 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 25.97/5.78
% 25.97/5.78 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 25.97/5.78 % ------ Proving...
% 25.97/5.78 % ------ Problem Properties
% 25.97/5.78
% 25.97/5.78 %
% 25.97/5.78 % clauses 123
% 25.97/5.78 % conjectures 11
% 25.97/5.78 % EPR 86
% 25.97/5.78 % Horn 113
% 25.97/5.78 % unary 11
% 25.97/5.78 % binary 37
% 25.97/5.78 % lits 339
% 25.97/5.78 % lits eq 4
% 25.97/5.78 % fd_pure 0
% 25.97/5.78 % fd_pseudo 0
% 25.97/5.78 % fd_cond 0
% 25.97/5.78 % fd_pseudo_cond 4
% 25.97/5.78 % AC symbols 0
% 25.97/5.78
% 25.97/5.78 % ------ Schedule dynamic 5 is on
% 25.97/5.78
% 25.97/5.78 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 25.97/5.78
% 25.97/5.78
% 25.97/5.78 % ------
% 25.97/5.78 % Current options:
% 25.97/5.78 % ------
% 25.97/5.78
% 25.97/5.78
% 25.97/5.78 %
% 25.97/5.78
% 25.97/5.78 % ------ Proving...
% 25.97/5.78 %
% 25.97/5.78
% 25.97/5.78 % SZS status Theorem for theBenchmark.p
% 25.97/5.78
% 25.97/5.78 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 25.97/5.79
% 25.97/5.79
%------------------------------------------------------------------------------