%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO615+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 : n004.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:38 PM UTC 2026
% Result : Theorem 91.16s 22.96s
% Output : CNFRefutation 91.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 47
% Syntax : Number of formulae : 690 ( 200 unt; 0 def)
% Number of atoms : 1491 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1460 ( 659 ~; 657 |; 95 &)
% ( 0 <=>; 49 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-8 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-5 aty)
% Number of variables : 1416 ( 0 sgn1386 !; 30 ?; 518 :)
% 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(f14,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD14) ).
fof(f15,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD15) ).
fof(f16,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X1,X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD16) ).
fof(f17,axiom,
! [X0,X1,X2,X3,X4] :
( ( cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X3) )
=> cyclic(X1,X2,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD17) ).
fof(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/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD19) ).
fof(f20,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD20) ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD21) ).
fof(f22,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD22) ).
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(f24,axiom,
! [X0,X1,X2,X3] :
( cong(X0,X1,X2,X3)
=> cong(X2,X3,X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD24) ).
fof(f25,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( cong(X2,X3,X4,X5)
& cong(X0,X1,X2,X3) )
=> cong(X0,X1,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD25) ).
fof(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/sandbox/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/sandbox/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/sandbox/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/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(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( perp(X3,X0,X0,X4)
& circle(X3,X0,X1,X2) )
=> eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD48) ).
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(f74,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( para(X4,X5,X6,X7)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD73) ).
fof(f75,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( perp(X4,X5,X6,X7)
& eqangle(X0,X1,X2,X3,X4,X5,X6,X7) )
=> perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD74) ).
fof(f81,axiom,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ( ~ coll(X0,X1,X2)
& eqangle(X0,X2,X1,X2,X0,X3,X1,X4) )
=> ( cyclic(X3,X1,X2,X5)
& eqangle(X0,X2,X1,X2,X0,X5,X1,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleX5) ).
fof(f91,axiom,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ( coll(X1,X3,X4)
& perp(X0,X2,X2,X1) )
=> ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleX15) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( coll(X6,X5,X0)
& circle(X4,X5,X6,X11)
& circle(X4,X1,X5,X10)
& coll(X5,X0,X2)
& circle(X4,X1,X8,X9)
& perp(X0,X1,X1,X4)
& perp(X1,X3,X7,X4)
& midpoint(X7,X1,X3)
& eqangle(X3,X2,X2,X0,X3,X2,X2,X1)
& eqangle(X3,X1,X1,X2,X3,X1,X1,X0)
& eqangle(X3,X0,X0,X1,X3,X0,X0,X2) )
=> eqangle(X5,X3,X3,X2,X2,X3,X3,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL618077) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( coll(X6,X5,X0)
& circle(X4,X5,X6,X11)
& circle(X4,X1,X5,X10)
& coll(X5,X0,X2)
& circle(X4,X1,X8,X9)
& perp(X0,X1,X1,X4)
& perp(X1,X3,X7,X4)
& midpoint(X7,X1,X3)
& eqangle(X3,X2,X2,X0,X3,X2,X2,X1)
& eqangle(X3,X1,X1,X2,X3,X1,X1,X0)
& eqangle(X3,X0,X0,X1,X3,X0,X0,X2) )
=> eqangle(X5,X3,X3,X2,X2,X3,X3,X6) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ( coll(X6,X5,X0)
& circle(X4,X5,X6,X11)
& circle(X4,X1,X5,X10)
& coll(X5,X0,X2)
& circle(X4,X1,X8,X9)
& perp(X0,X1,X1,X4)
& perp(X1,X3,X7,X4)
& eqangle(X3,X2,X2,X0,X3,X2,X2,X1)
& eqangle(X3,X1,X1,X2,X3,X1,X1,X0)
& eqangle(X3,X0,X0,X1,X3,X0,X0,X2) )
=> eqangle(X5,X3,X3,X2,X2,X3,X3,X6) ),
inference(pure_predicate_removal,[],[f96]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(flattening,[],[f101]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f104,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
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(ennf_transformation,[],[f6]) ).
fof(f106,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f105]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
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(ennf_transformation,[],[f9]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f109]) ).
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(ennf_transformation,[],[f10]) ).
fof(f112,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f114,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(f115,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(flattening,[],[f114]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
fof(f121,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f17]) ).
fof(f122,plain,
! [X0,X1,X2,X3,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(flattening,[],[f121]) ).
fof(f123,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(f124,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(f125,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f20]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(ennf_transformation,[],[f21]) ).
fof(f127,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
inference(ennf_transformation,[],[f22]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
inference(flattening,[],[f127]) ).
fof(f129,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] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
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(ennf_transformation,[],[f25]) ).
fof(f132,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X4,X5) ),
inference(flattening,[],[f131]) ).
fof(f149,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(f150,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(f151,plain,
! [X0,X1,X2,X3] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f41]) ).
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(ennf_transformation,[],[f43]) ).
fof(f155,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,[],[f154]) ).
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(ennf_transformation,[],[f44]) ).
fof(f157,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,[],[f156]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f158]) ).
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(ennf_transformation,[],[f46]) ).
fof(f161,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,[],[f160]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4] :
( ~ perp(X3,X0,X0,X4)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f166,plain,
! [X0,X1,X2,X3,X4] :
( ~ perp(X3,X0,X0,X4)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(flattening,[],[f165]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(ennf_transformation,[],[f53]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(flattening,[],[f173]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f175]) ).
fof(f179,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f56]) ).
fof(f180,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(flattening,[],[f179]) ).
fof(f181,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(f182,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f181]) ).
fof(f192,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f193,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f192]) ).
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(ennf_transformation,[],[f65]) ).
fof(f195,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,[],[f194]) ).
fof(f198,plain,
! [X0,X1,X2] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f199,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f200,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f199]) ).
fof(f201,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f202,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f209,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f74]) ).
fof(f210,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(flattening,[],[f209]) ).
fof(f211,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f75]) ).
fof(f212,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f211]) ).
fof(f223,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( coll(X0,X1,X2)
| ~ eqangle(X0,X2,X1,X2,X0,X3,X1,X4)
| ( cyclic(X3,X1,X2,X5)
& eqangle(X0,X2,X1,X2,X0,X5,X1,X5) ) ),
inference(ennf_transformation,[],[f81]) ).
fof(f224,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( coll(X0,X1,X2)
| ~ eqangle(X0,X2,X1,X2,X0,X3,X1,X4)
| ( cyclic(X3,X1,X2,X5)
& eqangle(X0,X2,X1,X2,X0,X5,X1,X5) ) ),
inference(flattening,[],[f223]) ).
fof(f242,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(ennf_transformation,[],[f91]) ).
fof(f243,plain,
! [X0,X1,X2,X3,X4] :
? [X5] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(X5,X0,X3,X4)
& coll(X5,X3,X4) ) ),
inference(flattening,[],[f242]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( coll(X6,X5,X0)
& circle(X4,X5,X6,X11)
& circle(X4,X1,X5,X10)
& coll(X5,X0,X2)
& circle(X4,X1,X8,X9)
& perp(X0,X1,X1,X4)
& perp(X1,X3,X7,X4)
& eqangle(X3,X2,X2,X0,X3,X2,X2,X1)
& eqangle(X3,X1,X1,X2,X3,X1,X1,X0)
& eqangle(X3,X0,X0,X1,X3,X0,X0,X2)
& ~ eqangle(X5,X3,X3,X2,X2,X3,X3,X6) ),
inference(ennf_transformation,[],[f98]) ).
fof(f251,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( coll(X6,X5,X0)
& circle(X4,X5,X6,X11)
& circle(X4,X1,X5,X10)
& coll(X5,X0,X2)
& circle(X4,X1,X8,X9)
& perp(X0,X1,X1,X4)
& perp(X1,X3,X7,X4)
& eqangle(X3,X2,X2,X0,X3,X2,X2,X1)
& eqangle(X3,X1,X1,X2,X3,X1,X1,X0)
& eqangle(X3,X0,X0,X1,X3,X0,X0,X2)
& ~ eqangle(X5,X3,X3,X2,X2,X3,X3,X6) ),
inference(flattening,[],[f250]) ).
fof(f256,plain,
! [X0,X1,X2,X3,X4] :
( coll(X0,X1,X2)
| ~ eqangle(X0,X2,X1,X2,X0,X3,X1,X4)
| ( cyclic(X3,X1,X2,sK4(X0,X1,X2,X3,X4))
& eqangle(X0,X2,X1,X2,X0,sK4(X0,X1,X2,X3,X4),X1,sK4(X0,X1,X2,X3,X4)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X5,sK4(X0,X1,X2,X3,X4))],[f224]) ).
fof(f267,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| ( perp(sK16(X0,X1,X2,X3,X4),X0,X3,X4)
& coll(sK16(X0,X1,X2,X3,X4),X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X5,sK16(X0,X1,X2,X3,X4))],[f243]) ).
fof(f271,plain,
( coll(sK26,sK25,sK20)
& circle(sK24,sK25,sK26,sK31)
& circle(sK24,sK21,sK25,sK30)
& coll(sK25,sK20,sK22)
& circle(sK24,sK21,sK28,sK29)
& perp(sK20,sK21,sK21,sK24)
& perp(sK21,sK23,sK27,sK24)
& eqangle(sK23,sK22,sK22,sK20,sK23,sK22,sK22,sK21)
& eqangle(sK23,sK21,sK21,sK22,sK23,sK21,sK21,sK20)
& eqangle(sK23,sK20,sK20,sK21,sK23,sK20,sK20,sK22)
& ~ eqangle(sK25,sK23,sK23,sK22,sK22,sK23,sK23,sK26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25),skolemize(X6,sK26),skolemize(X7,sK27),skolemize(X8,sK28),skolemize(X9,sK29),skolemize(X10,sK30),skolemize(X11,sK31)],[f251]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f273,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f274,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f275,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f103]) ).
fof(f276,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f277,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,[],[f106]) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f279,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f108]) ).
fof(f280,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,[],[f110]) ).
fof(f281,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,[],[f112]) ).
fof(f282,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f283,plain,
! [X2,X3,X0,X1] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f285,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f118]) ).
fof(f286,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f119]) ).
fof(f287,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f120]) ).
fof(f288,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
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(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f123]) ).
fof(f290,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,[],[f124]) ).
fof(f291,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f125]) ).
fof(f292,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(cnf_transformation,[],[f126]) ).
fof(f293,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X2,X3,X8,X9,X10,X11) ),
inference(cnf_transformation,[],[f128]) ).
fof(f294,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f129]) ).
fof(f295,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f296,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,[],[f132]) ).
fof(f310,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f149]) ).
fof(f311,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f150]) ).
fof(f312,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| eqangle(X2,X0,X2,X1,X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f151]) ).
fof(f314,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,[],[f155]) ).
fof(f315,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,[],[f157]) ).
fof(f316,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f159]) ).
fof(f317,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,[],[f161]) ).
fof(f320,plain,
! [X2,X3,X0,X1,X4] :
( ~ perp(X3,X0,X0,X4)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f324,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f174]) ).
fof(f325,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f176]) ).
fof(f327,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f328,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f182]) ).
fof(f335,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f193]) ).
fof(f336,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,[],[f195]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f198]) ).
fof(f339,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f200]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f201]) ).
fof(f341,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f202]) ).
fof(f345,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f210]) ).
fof(f346,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f212]) ).
fof(f356,plain,
! [X2,X3,X0,X1,X4] :
( coll(X0,X1,X2)
| ~ eqangle(X0,X2,X1,X2,X0,X3,X1,X4)
| cyclic(X3,X1,X2,sK4(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f256]) ).
fof(f378,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X1,X3,X4)
| ~ perp(X0,X2,X2,X1)
| perp(sK16(X0,X1,X2,X3,X4),X0,X3,X4) ),
inference(cnf_transformation,[],[f267]) ).
fof(f385,plain,
coll(sK26,sK25,sK20),
inference(cnf_transformation,[],[f271]) ).
fof(f388,plain,
coll(sK25,sK20,sK22),
inference(cnf_transformation,[],[f271]) ).
fof(f390,plain,
perp(sK20,sK21,sK21,sK24),
inference(cnf_transformation,[],[f271]) ).
fof(f391,plain,
perp(sK21,sK23,sK27,sK24),
inference(cnf_transformation,[],[f271]) ).
fof(f392,plain,
eqangle(sK23,sK22,sK22,sK20,sK23,sK22,sK22,sK21),
inference(cnf_transformation,[],[f271]) ).
fof(f393,plain,
eqangle(sK23,sK21,sK21,sK22,sK23,sK21,sK21,sK20),
inference(cnf_transformation,[],[f271]) ).
fof(f394,plain,
eqangle(sK23,sK20,sK20,sK21,sK23,sK20,sK20,sK22),
inference(cnf_transformation,[],[f271]) ).
fof(f395,plain,
~ eqangle(sK25,sK23,sK23,sK22,sK22,sK23,sK23,sK26),
inference(cnf_transformation,[],[f271]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f273]) ).
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,[],[f274]) ).
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,[],[f275]) ).
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,[],[f276]) ).
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,[],[f277]) ).
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,[],[f278]) ).
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,[],[f279]) ).
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,[],[f280]) ).
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,[],[f281]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f282]) ).
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,[],[f283]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f288]) ).
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,[],[f289]) ).
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,[],[f290]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X4,X5,X6,X7,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X4,X5,X2,X3,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
( eqangle(X0,X1,X2,X3,X8,X9,X10,X11)
| ~ eqangle(X4,X5,X6,X7,X8,X9,X10,X11)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f293]) ).
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,[],[f294]) ).
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,[],[f295]) ).
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,[],[f296]) ).
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,[],[f310]) ).
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,[],[f311]) ).
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,[],[f312]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cyclic(X1,X2,X0,X3)
| ~ coll(X0,X3,X2)
| ~ eqangle(X0,X1,X0,X2,X3,X1,X3,X2) ),
inference(cnf_transformation,[],[f314]) ).
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,[],[f315]) ).
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,[],[f316]) ).
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,[],[f317]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X1,X2,X1,X3,X4,X1,X4,X3)
| ~ circle(X0,X1,X3,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f320]) ).
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,[],[f324]) ).
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,[],[f325]) ).
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,[],[f327]) ).
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,[],[f328]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X1,X3,X2,X4)
| ~ midp(X0,X3,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f335]) ).
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,[],[f336]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f338]) ).
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,[],[f339]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f341]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( para(X0,X1,X2,X3)
| ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( perp(X0,X1,X2,X3)
| ~ perp(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( coll(X0,X2,X1)
| cyclic(X3,X2,X1,sK4(X0,X2,X1,X3,X4))
| ~ eqangle(X0,X1,X2,X1,X0,X3,X2,X4) ),
inference(cnf_transformation,[],[f356]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( perp(sK16(X0,X2,X1,X3,X4),X0,X3,X4)
| ~ coll(X2,X3,X4)
| ~ perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_162,negated_conjecture,
~ eqangle(sK25,sK23,sK23,sK22,sK22,sK23,sK23,sK26),
inference(cnf_transformation,[],[f395]) ).
tcf(c_163,negated_conjecture,
eqangle(sK23,sK20,sK20,sK21,sK23,sK20,sK20,sK22),
inference(cnf_transformation,[],[f394]) ).
tcf(c_164,negated_conjecture,
eqangle(sK23,sK21,sK21,sK22,sK23,sK21,sK21,sK20),
inference(cnf_transformation,[],[f393]) ).
tcf(c_165,negated_conjecture,
eqangle(sK23,sK22,sK22,sK20,sK23,sK22,sK22,sK21),
inference(cnf_transformation,[],[f392]) ).
tcf(c_166,negated_conjecture,
perp(sK21,sK23,sK27,sK24),
inference(cnf_transformation,[],[f391]) ).
tcf(c_167,negated_conjecture,
perp(sK20,sK21,sK21,sK24),
inference(cnf_transformation,[],[f390]) ).
tcf(c_169,negated_conjecture,
coll(sK25,sK20,sK22),
inference(cnf_transformation,[],[f388]) ).
tcf(c_172,negated_conjecture,
coll(sK26,sK25,sK20),
inference(cnf_transformation,[],[f385]) ).
tcf(c_178,plain,
( midp(sK21,sK21,sK21)
| ~ coll(sK21,sK21,sK21)
| ~ cong(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_182,plain,
( eqangle(sK21,sK21,sK21,sK21,sK21,sK21,sK21,sK21)
| ~ para(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_187,plain,
( perp(sK21,sK21,sK21,sK21)
| ~ cong(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_236,plain,
( cong(sK21,sK21,sK21,sK21)
| ~ cyclic(sK21,sK21,sK21,sK21)
| ~ eqangle(sK21,sK21,sK21,sK21,sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_5114,negated_conjecture,
coll(sK26,sK25,sK20),
inference(demodulation,[status(thm)],[c_172]) ).
tcf(c_5117,negated_conjecture,
coll(sK25,sK20,sK22),
inference(demodulation,[status(thm)],[c_169]) ).
tcf(c_5119,negated_conjecture,
perp(sK20,sK21,sK21,sK24),
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_5120,negated_conjecture,
perp(sK21,sK23,sK27,sK24),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_5121,negated_conjecture,
eqangle(sK23,sK22,sK22,sK20,sK23,sK22,sK22,sK21),
inference(demodulation,[status(thm)],[c_165]) ).
tcf(c_5122,negated_conjecture,
eqangle(sK23,sK21,sK21,sK22,sK23,sK21,sK21,sK20),
inference(demodulation,[status(thm)],[c_164]) ).
tcf(c_5123,negated_conjecture,
eqangle(sK23,sK20,sK20,sK21,sK23,sK20,sK20,sK22),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_6674,plain,
coll(sK25,sK22,sK20),
inference(superposition,[status(thm)],[c_5117,c_49]) ).
tcf(c_6680,plain,
coll(sK20,sK25,sK22),
inference(superposition,[status(thm)],[c_5117,c_50]) ).
tcf(c_6681,plain,
coll(sK25,sK26,sK20),
inference(superposition,[status(thm)],[c_5114,c_50]) ).
tcf(c_6690,plain,
coll(sK22,sK25,sK20),
inference(superposition,[status(thm)],[c_6674,c_50]) ).
tcf(c_6697,plain,
coll(sK25,sK20,sK26),
inference(superposition,[status(thm)],[c_6681,c_49]) ).
tcf(c_6716,plain,
! [X0: $i] :
( coll(sK22,X0,sK25)
| ~ coll(sK25,sK20,X0) ),
inference(superposition,[status(thm)],[c_5117,c_51]) ).
tcf(c_6717,plain,
! [X0: $i] :
( coll(sK20,X0,sK26)
| ~ coll(sK26,sK25,X0) ),
inference(superposition,[status(thm)],[c_5114,c_51]) ).
tcf(c_6720,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK25,X0) ),
inference(superposition,[status(thm)],[c_6680,c_51]) ).
tcf(c_6722,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK25,X0) ),
inference(superposition,[status(thm)],[c_6690,c_51]) ).
tcf(c_6785,plain,
coll(sK22,sK26,sK25),
inference(superposition,[status(thm)],[c_6697,c_6716]) ).
tcf(c_6793,plain,
coll(sK26,sK22,sK25),
inference(superposition,[status(thm)],[c_6785,c_50]) ).
tcf(c_6808,plain,
coll(sK20,sK20,sK26),
inference(superposition,[status(thm)],[c_5114,c_6717]) ).
tcf(c_6811,plain,
coll(sK20,sK26,sK20),
inference(superposition,[status(thm)],[c_6808,c_49]) ).
tcf(c_6815,plain,
! [X0: $i] :
( coll(sK20,X0,sK20)
| ~ coll(sK20,sK26,X0) ),
inference(superposition,[status(thm)],[c_6811,c_51]) ).
tcf(c_6847,plain,
coll(sK22,sK22,sK20),
inference(superposition,[status(thm)],[c_6680,c_6720]) ).
tcf(c_6859,plain,
perp(sK20,sK21,sK24,sK21),
inference(superposition,[status(thm)],[c_5119,c_55]) ).
tcf(c_6864,plain,
perp(sK27,sK24,sK21,sK23),
inference(superposition,[status(thm)],[c_5120,c_56]) ).
tcf(c_6865,plain,
perp(sK21,sK24,sK20,sK21),
inference(superposition,[status(thm)],[c_5119,c_56]) ).
tcf(c_6876,plain,
coll(sK26,sK25,sK22),
inference(superposition,[status(thm)],[c_6793,c_49]) ).
tcf(c_6902,plain,
perp(sK24,sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_6859,c_56]) ).
tcf(c_6905,plain,
perp(sK27,sK24,sK23,sK21),
inference(superposition,[status(thm)],[c_6864,c_55]) ).
tcf(c_6907,plain,
perp(sK21,sK24,sK21,sK20),
inference(superposition,[status(thm)],[c_6865,c_55]) ).
tcf(c_6908,plain,
! [X0: $i] :
( coll(sK20,X0,sK22)
| ~ coll(sK22,sK22,X0) ),
inference(superposition,[status(thm)],[c_6847,c_51]) ).
tcf(c_6924,plain,
coll(sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_6690,c_6722]) ).
tcf(c_6972,plain,
coll(sK20,sK22,sK26),
inference(superposition,[status(thm)],[c_6876,c_6717]) ).
tcf(c_6976,plain,
! [X0: $i] :
( coll(sK26,X0,sK20)
| ~ coll(sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_6972,c_51]) ).
tcf(c_7016,plain,
coll(sK20,sK22,sK20),
inference(superposition,[status(thm)],[c_6924,c_49]) ).
tcf(c_7256,plain,
! [X0: $i] :
( coll(sK20,X0,sK20)
| ~ coll(sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_7016,c_51]) ).
tcf(c_7262,plain,
( coll(sK20,sK21,sK20)
| ~ coll(sK20,sK22,sK21) ),
inference(instantiation,[status(thm)],[c_7256]) ).
tcf(c_7384,plain,
! [X0: $i] :
( cong(sK20,X0,sK21,X0)
| ~ midp(X0,sK20,sK24) ),
inference(superposition,[status(thm)],[c_5119,c_101]) ).
tcf(c_7411,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK23,X0,X1)
| ~ perp(sK21,sK23,sK27,sK24)
| ~ perp(sK27,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_7456,plain,
! [X0: $i] :
( cong(sK21,X0,sK20,X0)
| ~ midp(X0,sK20,sK24) ),
inference(superposition,[status(thm)],[c_7384,c_72]) ).
tcf(c_7573,plain,
( cong(sK20,sK21,sK20,sK24)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_5119,c_104]) ).
tcf(c_7578,plain,
( cong(sK20,sK24,sK20,sK21)
| ~ midp(sK21,sK24,sK21) ),
inference(superposition,[status(thm)],[c_6859,c_104]) ).
tcf(c_7580,plain,
( cong(sK21,sK20,sK21,sK21)
| ~ midp(sK24,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6865,c_104]) ).
tcf(c_7582,plain,
( cong(sK24,sK20,sK24,sK21)
| ~ midp(sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_6902,c_104]) ).
tcf(c_7668,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK23,X0,X1)
| ~ perp(sK27,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_5120,c_57]) ).
tcf(c_7669,plain,
! [X0: $i,X1: $i] :
( para(sK20,sK21,X0,X1)
| ~ perp(sK21,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_5119,c_57]) ).
tcf(c_7676,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK24,X0,X1)
| ~ perp(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6865,c_57]) ).
tcf(c_7679,plain,
! [X0: $i,X1: $i] :
( para(sK27,sK24,X0,X1)
| ~ perp(sK23,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_6905,c_57]) ).
tcf(c_7738,plain,
( para(sK27,sK24,sK21,sK21)
| ~ perp(sK23,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_7679]) ).
tcf(c_7845,plain,
( cong(sK20,sK24,sK20,sK21)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_7573,c_72]) ).
tcf(c_7858,plain,
para(sK21,sK23,sK21,sK23),
inference(superposition,[status(thm)],[c_6864,c_7668]) ).
tcf(c_7859,plain,
para(sK21,sK23,sK23,sK21),
inference(superposition,[status(thm)],[c_6905,c_7668]) ).
tcf(c_7864,plain,
para(sK20,sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_6865,c_7669]) ).
tcf(c_7865,plain,
para(sK20,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_6907,c_7669]) ).
tcf(c_7874,plain,
coll(sK21,sK23,sK23),
inference(superposition,[status(thm)],[c_7858,c_115]) ).
tcf(c_7881,plain,
para(sK23,sK21,sK21,sK23),
inference(superposition,[status(thm)],[c_7859,c_53]) ).
tcf(c_7895,plain,
coll(sK20,sK21,sK21),
inference(superposition,[status(thm)],[c_7864,c_115]) ).
tcf(c_7900,plain,
para(sK21,sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_7865,c_53]) ).
tcf(c_7927,plain,
! [X0: $i] :
( circle(sK20,sK21,X0,sK24)
| ~ midp(sK21,sK21,sK24)
| ~ cong(sK20,sK21,sK20,X0) ),
inference(superposition,[status(thm)],[c_7573,c_60]) ).
tcf(c_7958,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(sK20,X0,X1,X2)
| ~ midp(X0,sK20,sK24)
| ~ cong(sK21,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_7384,c_73]) ).
tcf(c_7959,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(sK21,X0,X1,X2)
| ~ midp(X0,sK20,sK24)
| ~ cong(sK20,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_7456,c_73]) ).
tcf(c_7962,plain,
! [X0: $i,X1: $i] :
( cong(sK20,sK21,X0,X1)
| ~ midp(sK21,sK21,sK24)
| ~ cong(sK20,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_7573,c_73]) ).
tcf(c_7999,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK21,X1,X0)
| ~ midp(X1,sK20,sK24)
| ~ cong(sK20,X0,sK21,X0) ),
inference(superposition,[status(thm)],[c_7384,c_105]) ).
tcf(c_8032,plain,
coll(sK23,sK21,sK23),
inference(superposition,[status(thm)],[c_7874,c_50]) ).
tcf(c_8037,plain,
! [X0: $i] :
( coll(sK21,X0,sK20)
| ~ coll(sK20,sK21,X0) ),
inference(superposition,[status(thm)],[c_7895,c_51]) ).
tcf(c_8038,plain,
coll(sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_7895,c_50]) ).
tcf(c_8042,plain,
( coll(sK21,sK21,sK20)
| ~ coll(sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_8037]) ).
tcf(c_8196,plain,
( cong(sK20,sK24,sK21,sK20)
| ~ midp(sK21,sK24,sK21) ),
inference(superposition,[status(thm)],[c_7578,c_71]) ).
tcf(c_8286,plain,
eqangle(sK20,sK23,sK20,sK21,sK23,sK20,sK20,sK22),
inference(superposition,[status(thm)],[c_5123,c_66]) ).
tcf(c_8287,plain,
eqangle(sK21,sK23,sK21,sK22,sK23,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_5122,c_66]) ).
tcf(c_8335,plain,
eqangle(sK20,sK21,sK23,sK20,sK20,sK22,sK23,sK20),
inference(superposition,[status(thm)],[c_5123,c_67]) ).
tcf(c_8336,plain,
eqangle(sK21,sK22,sK23,sK21,sK21,sK20,sK23,sK21),
inference(superposition,[status(thm)],[c_5122,c_67]) ).
tcf(c_8337,plain,
eqangle(sK22,sK20,sK23,sK22,sK22,sK21,sK23,sK22),
inference(superposition,[status(thm)],[c_5121,c_67]) ).
tcf(c_8348,plain,
coll(sK23,sK23,sK21),
inference(superposition,[status(thm)],[c_8032,c_49]) ).
tcf(c_8351,plain,
! [X0: $i] :
( coll(sK21,X0,sK21)
| ~ coll(sK21,sK20,X0) ),
inference(superposition,[status(thm)],[c_8038,c_51]) ).
tcf(c_8353,plain,
coll(sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_8038,c_49]) ).
tcf(c_8356,plain,
( coll(sK21,sK21,sK21)
| ~ coll(sK21,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_8351]) ).
tcf(c_8357,plain,
! [X0: $i] :
( coll(sK21,X0,sK23)
| ~ coll(sK23,sK23,X0) ),
inference(superposition,[status(thm)],[c_8348,c_51]) ).
tcf(c_8362,plain,
( coll(sK21,sK21,sK23)
| ~ coll(sK23,sK23,sK21) ),
inference(instantiation,[status(thm)],[c_8357]) ).
tcf(c_8363,plain,
! [X0: $i] :
( coll(sK20,X0,sK21)
| ~ coll(sK21,sK21,X0) ),
inference(superposition,[status(thm)],[c_8353,c_51]) ).
tcf(c_8370,plain,
eqangle(sK21,sK22,sK21,sK23,sK21,sK20,sK23,sK21),
inference(superposition,[status(thm)],[c_8287,c_67]) ).
tcf(c_8375,plain,
eqangle(sK21,sK20,sK23,sK20,sK20,sK22,sK23,sK20),
inference(superposition,[status(thm)],[c_8335,c_66]) ).
tcf(c_8376,plain,
para(sK20,sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_8335,c_87]) ).
tcf(c_8409,plain,
para(sK21,sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_8336,c_87]) ).
tcf(c_8412,plain,
para(sK22,sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_8337,c_87]) ).
tcf(c_8415,plain,
para(sK20,sK22,sK20,sK21),
inference(superposition,[status(thm)],[c_8376,c_53]) ).
tcf(c_8416,plain,
para(sK20,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_8376,c_52]) ).
tcf(c_8417,plain,
coll(sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_8376,c_115]) ).
tcf(c_8440,plain,
eqangle(sK23,sK20,sK20,sK22,sK23,sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_5123,c_68]) ).
tcf(c_8441,plain,
eqangle(sK23,sK21,sK21,sK20,sK23,sK21,sK21,sK22),
inference(superposition,[status(thm)],[c_5122,c_68]) ).
tcf(c_8443,plain,
eqangle(sK23,sK20,sK20,sK22,sK20,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_8286,c_68]) ).
tcf(c_8446,plain,
eqangle(sK20,sK22,sK23,sK20,sK20,sK21,sK23,sK20),
inference(superposition,[status(thm)],[c_8335,c_68]) ).
tcf(c_8465,plain,
eqangle(sK23,sK20,sK23,sK20,sK20,sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_5123,c_69]) ).
tcf(c_8466,plain,
eqangle(sK23,sK21,sK23,sK21,sK21,sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_5122,c_69]) ).
tcf(c_8467,plain,
eqangle(sK23,sK22,sK23,sK22,sK22,sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_5121,c_69]) ).
tcf(c_8468,plain,
eqangle(sK20,sK23,sK23,sK20,sK20,sK21,sK20,sK22),
inference(superposition,[status(thm)],[c_8286,c_69]) ).
tcf(c_8469,plain,
eqangle(sK21,sK23,sK23,sK21,sK21,sK22,sK21,sK20),
inference(superposition,[status(thm)],[c_8287,c_69]) ).
tcf(c_8471,plain,
eqangle(sK20,sK21,sK20,sK22,sK23,sK20,sK23,sK20),
inference(superposition,[status(thm)],[c_8335,c_69]) ).
tcf(c_8472,plain,
eqangle(sK21,sK22,sK21,sK20,sK23,sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_8336,c_69]) ).
tcf(c_8509,plain,
! [X0: $i] :
( coll(sK22,X0,sK20)
| ~ coll(sK20,sK21,X0) ),
inference(superposition,[status(thm)],[c_8417,c_51]) ).
tcf(c_8511,plain,
coll(sK20,sK22,sK21),
inference(superposition,[status(thm)],[c_8417,c_49]) ).
tcf(c_8531,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X2,X3)
| ~ perp(sK20,sK21,sK24,sK21)
| ~ eqangle(X0,X1,X2,X3,sK20,sK21,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_8540,plain,
coll(sK26,sK21,sK20),
inference(superposition,[status(thm)],[c_8511,c_6976]) ).
tcf(c_8575,plain,
para(sK21,sK20,sK21,sK22),
inference(superposition,[status(thm)],[c_8409,c_53]) ).
tcf(c_8586,plain,
para(sK22,sK21,sK22,sK20),
inference(superposition,[status(thm)],[c_8412,c_53]) ).
tcf(c_8683,plain,
coll(sK26,sK20,sK21),
inference(superposition,[status(thm)],[c_8540,c_49]) ).
tcf(c_8712,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,X1,X2,X3)
| ~ perp(sK21,sK24,sK20,sK21)
| ~ eqangle(X0,X1,X2,X3,sK21,sK24,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_8727,plain,
eqangle(sK21,sK22,sK21,sK20,sK21,sK23,sK23,sK21),
inference(superposition,[status(thm)],[c_8370,c_69]) ).
tcf(c_9099,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_9112,plain,
( cyclic(sK21,sK21,sK21,sK21)
| ~ coll(sK21,sK21,sK21)
| ~ para(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_9099]) ).
tcf(c_9122,plain,
! [X0: $i] :
( midp(sK23,X0,sK23)
| ~ midp(sK21,X0,sK21)
| ~ coll(sK23,X0,sK23) ),
inference(superposition,[status(thm)],[c_7858,c_94]) ).
tcf(c_9123,plain,
! [X0: $i] :
( midp(sK23,X0,sK21)
| ~ midp(sK21,X0,sK23)
| ~ coll(sK23,X0,sK21) ),
inference(superposition,[status(thm)],[c_7859,c_94]) ).
tcf(c_9124,plain,
! [X0: $i] :
( midp(sK21,X0,sK21)
| ~ midp(sK20,X0,sK20)
| ~ coll(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_7864,c_94]) ).
tcf(c_9156,plain,
( midp(sK23,sK21,sK23)
| ~ midp(sK21,sK21,sK21)
| ~ coll(sK23,sK21,sK23) ),
inference(instantiation,[status(thm)],[c_9122]) ).
tcf(c_9176,plain,
! [X0: $i] :
( coll(sK21,X0,sK26)
| ~ coll(sK26,sK20,X0) ),
inference(superposition,[status(thm)],[c_8683,c_51]) ).
tcf(c_9177,plain,
coll(sK20,sK26,sK21),
inference(superposition,[status(thm)],[c_8683,c_50]) ).
tcf(c_9183,plain,
( coll(sK21,sK21,sK26)
| ~ coll(sK26,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_9176]) ).
tcf(c_9687,plain,
coll(sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_9177,c_6815]) ).
tcf(c_9933,plain,
! [X0: $i,X1: $i] :
( eqangle(sK21,sK24,sK21,X0,X1,sK21,X1,X0)
| ~ circle(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_5119,c_97]) ).
tcf(c_10197,plain,
para(sK21,sK24,sK21,sK24),
inference(superposition,[status(thm)],[c_5119,c_7676]) ).
tcf(c_10198,plain,
para(sK21,sK24,sK24,sK21),
inference(superposition,[status(thm)],[c_6859,c_7676]) ).
tcf(c_10199,plain,
! [X0: $i] :
( midp(sK24,X0,sK24)
| ~ midp(sK21,X0,sK21)
| ~ coll(sK24,X0,sK24) ),
inference(superposition,[status(thm)],[c_10197,c_94]) ).
tcf(c_10204,plain,
coll(sK21,sK24,sK24),
inference(superposition,[status(thm)],[c_10197,c_115]) ).
tcf(c_10213,plain,
coll(sK24,sK21,sK24),
inference(superposition,[status(thm)],[c_10204,c_50]) ).
tcf(c_10249,plain,
! [X0: $i] :
( midp(X0,sK23,sK23)
| ~ midp(X0,sK21,sK21)
| ~ para(sK21,sK23,sK21,sK23) ),
inference(superposition,[status(thm)],[c_7858,c_113]) ).
tcf(c_10255,plain,
! [X0: $i] :
( midp(X0,sK20,sK21)
| ~ midp(X0,sK22,sK22)
| ~ para(sK22,sK21,sK22,sK20) ),
inference(superposition,[status(thm)],[c_8412,c_113]) ).
tcf(c_10258,plain,
! [X0: $i] :
( midp(X0,sK24,sK24)
| ~ midp(X0,sK21,sK21)
| ~ para(sK21,sK24,sK21,sK24) ),
inference(superposition,[status(thm)],[c_10197,c_113]) ).
tcf(c_10259,plain,
! [X0: $i] :
( midp(X0,sK24,sK24)
| ~ midp(X0,sK21,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10258,c_10197]) ).
tcf(c_10286,plain,
! [X0: $i] :
( midp(X0,sK23,sK23)
| ~ midp(X0,sK21,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10249,c_7858]) ).
tcf(c_10289,plain,
( midp(sK21,sK23,sK23)
| ~ midp(sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_10286]) ).
tcf(c_10294,plain,
( midp(sK21,sK20,sK21)
| ~ midp(sK21,sK22,sK22)
| ~ para(sK22,sK21,sK22,sK20) ),
inference(instantiation,[status(thm)],[c_10255]) ).
tcf(c_10333,plain,
( para(sK23,sK20,sK23,sK20)
| ~ para(sK20,sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_8465,c_122]) ).
tcf(c_10334,plain,
( para(sK23,sK21,sK23,sK21)
| ~ para(sK21,sK22,sK21,sK20) ),
inference(superposition,[status(thm)],[c_8466,c_122]) ).
tcf(c_10335,plain,
( para(sK23,sK22,sK23,sK22)
| ~ para(sK22,sK20,sK22,sK21) ),
inference(superposition,[status(thm)],[c_8467,c_122]) ).
tcf(c_10349,plain,
( para(sK20,sK23,sK23,sK20)
| ~ para(sK20,sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_8468,c_122]) ).
tcf(c_10374,plain,
para(sK20,sK23,sK23,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_10349,c_8376]) ).
tcf(c_10399,plain,
para(sK23,sK22,sK23,sK22),
inference(forward_subsumption_resolution,[status(thm)],[c_10335,c_8412]) ).
tcf(c_10400,plain,
para(sK23,sK21,sK23,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_10334,c_8409]) ).
tcf(c_10401,plain,
para(sK23,sK20,sK23,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_10333,c_8376]) ).
tcf(c_10551,plain,
( perp(sK23,sK20,sK23,sK20)
| ~ perp(sK20,sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_8465,c_123]) ).
tcf(c_10558,plain,
( perp(sK21,sK20,sK23,sK20)
| ~ perp(sK20,sK22,sK23,sK20) ),
inference(superposition,[status(thm)],[c_8375,c_123]) ).
tcf(c_10564,plain,
( perp(sK20,sK22,sK23,sK20)
| ~ perp(sK20,sK21,sK23,sK20) ),
inference(superposition,[status(thm)],[c_8446,c_123]) ).
tcf(c_10567,plain,
( perp(sK20,sK23,sK23,sK20)
| ~ perp(sK20,sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_8468,c_123]) ).
tcf(c_10568,plain,
( perp(sK21,sK23,sK23,sK21)
| ~ perp(sK21,sK22,sK21,sK20) ),
inference(superposition,[status(thm)],[c_8469,c_123]) ).
tcf(c_10570,plain,
( perp(sK20,sK21,sK20,sK22)
| ~ perp(sK23,sK20,sK23,sK20) ),
inference(superposition,[status(thm)],[c_8471,c_123]) ).
tcf(c_10571,plain,
( perp(sK21,sK22,sK21,sK20)
| ~ perp(sK23,sK21,sK23,sK21) ),
inference(superposition,[status(thm)],[c_8472,c_123]) ).
tcf(c_10788,plain,
coll(sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_9687,c_49]) ).
tcf(c_10824,plain,
! [X0: $i,X1: $i] :
( para(sK21,sK24,X0,X1)
| ~ para(sK24,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_10198,c_54]) ).
tcf(c_10825,plain,
para(sK24,sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_10198,c_53]) ).
tcf(c_10837,plain,
( para(sK21,sK24,sK21,sK21)
| ~ para(sK24,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_10824]) ).
tcf(c_11242,plain,
! [X0: $i,X1: $i] :
( perp(sK16(sK20,sK24,sK21,X0,X1),sK20,X0,X1)
| ~ coll(sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_5119,c_156]) ).
tcf(c_11264,plain,
( perp(sK16(sK20,sK24,sK21,sK21,sK21),sK20,sK21,sK21)
| ~ coll(sK24,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_11242]) ).
tcf(c_11337,plain,
coll(sK24,sK24,sK21),
inference(superposition,[status(thm)],[c_10213,c_49]) ).
tcf(c_11368,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK16(sK20,sK24,sK21,X0,X1),sK20)
| ~ coll(sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_11242,c_56]) ).
tcf(c_11691,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(sK24,X2,X0)
| ~ coll(X0,X1,sK24)
| ~ coll(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_11692,plain,
( coll(sK24,sK21,sK21)
| ~ coll(sK21,sK21,sK24)
| ~ coll(sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_11691]) ).
tcf(c_12072,plain,
! [X0: $i] :
( coll(sK21,X0,sK24)
| ~ coll(sK24,sK24,X0) ),
inference(superposition,[status(thm)],[c_11337,c_51]) ).
tcf(c_12077,plain,
( coll(sK21,sK21,sK24)
| ~ coll(sK24,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_12072]) ).
tcf(c_12996,plain,
( coll(sK21,sK21,sK24)
| cyclic(sK21,sK21,sK24,sK4(sK21,sK21,sK24,sK21,sK24))
| ~ circle(sK20,sK21,sK24,sK21) ),
inference(superposition,[status(thm)],[c_9933,c_134]) ).
tcf(c_13213,plain,
! [X0: $i] :
( midp(sK21,X0,sK23)
| ~ midp(sK23,X0,sK21)
| ~ coll(sK21,X0,sK23) ),
inference(superposition,[status(thm)],[c_7881,c_94]) ).
tcf(c_13230,plain,
( midp(sK21,sK21,sK23)
| ~ midp(sK23,sK21,sK21)
| ~ coll(sK21,sK21,sK23) ),
inference(instantiation,[status(thm)],[c_13213]) ).
tcf(c_13247,plain,
! [X0: $i] :
( midp(sK20,X0,sK21)
| ~ midp(sK21,X0,sK20)
| ~ coll(sK20,X0,sK21) ),
inference(superposition,[status(thm)],[c_7900,c_94]) ).
tcf(c_13264,plain,
( midp(sK20,sK21,sK21)
| ~ midp(sK21,sK21,sK20)
| ~ coll(sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_13247]) ).
tcf(c_13282,plain,
! [X0: $i] :
( midp(X0,sK22,sK21)
| ~ midp(X0,sK20,sK20)
| ~ para(sK20,sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_8415,c_113]) ).
tcf(c_13284,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK22,X0,X1)
| ~ perp(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_8415,c_58]) ).
tcf(c_13296,plain,
! [X0: $i] :
( midp(X0,sK22,sK21)
| ~ midp(X0,sK20,sK20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13282,c_8376]) ).
tcf(c_13299,plain,
( midp(sK21,sK22,sK21)
| ~ midp(sK21,sK20,sK20) ),
inference(instantiation,[status(thm)],[c_13296]) ).
tcf(c_13301,plain,
( perp(sK20,sK22,sK21,sK21)
| ~ perp(sK20,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_13284]) ).
tcf(c_13386,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,X2,X3)
| ~ coll(sK24,X0,X1)
| ~ perp(sK16(sK20,sK24,sK21,X0,X1),sK20,X2,X3) ),
inference(superposition,[status(thm)],[c_11368,c_57]) ).
tcf(c_13413,plain,
( para(sK21,sK21,sK21,sK21)
| ~ coll(sK24,sK21,sK21)
| ~ perp(sK16(sK20,sK24,sK21,sK21,sK21),sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_13386]) ).
tcf(c_13683,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK20,sK20,sK21,X0,X1,X2,X3)
| ~ eqangle(sK23,sK20,sK20,sK22,X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_5123,c_70]) ).
tcf(c_13684,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK21,sK21,sK22,X0,X1,X2,X3)
| ~ eqangle(sK23,sK21,sK21,sK20,X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_5122,c_70]) ).
tcf(c_13686,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK20,sK23,sK20,sK21,X0,X1,X2,X3)
| ~ eqangle(sK23,sK20,sK20,sK22,X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_8286,c_70]) ).
tcf(c_13692,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK20,sK20,sK22,X0,X1,X2,X3)
| ~ eqangle(sK23,sK20,sK20,sK21,X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_8440,c_70]) ).
tcf(c_13693,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK21,sK21,sK20,X0,X1,X2,X3)
| ~ eqangle(sK23,sK21,sK21,sK22,X0,X1,X2,X3) ),
inference(superposition,[status(thm)],[c_8441,c_70]) ).
tcf(c_14091,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK20,sK20,sK21,X0,X1,sK20,sK22)
| ~ para(sK23,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_88,c_13683]) ).
tcf(c_14094,plain,
eqangle(sK23,sK20,sK20,sK21,sK23,sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_8440,c_13683]) ).
tcf(c_14095,plain,
eqangle(sK23,sK20,sK20,sK21,sK20,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_8443,c_13683]) ).
tcf(c_14108,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK21,sK21,sK22,X0,X1,sK21,sK20)
| ~ para(sK23,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_88,c_13684]) ).
tcf(c_14150,plain,
eqangle(sK23,sK20,sK23,sK20,sK20,sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_14094,c_69]) ).
tcf(c_14168,plain,
eqangle(sK20,sK23,sK20,sK21,sK20,sK23,sK20,sK21),
inference(superposition,[status(thm)],[c_14095,c_66]) ).
tcf(c_14758,plain,
! [X0: $i] :
( midp(sK21,X0,sK20)
| ~ midp(sK20,X0,sK22)
| ~ coll(sK21,X0,sK20) ),
inference(superposition,[status(thm)],[c_8416,c_94]) ).
tcf(c_14775,plain,
( midp(sK21,sK21,sK20)
| ~ midp(sK20,sK21,sK22)
| ~ coll(sK21,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_14758]) ).
tcf(c_14792,plain,
! [X0: $i] :
( midp(sK20,X0,sK22)
| ~ midp(sK21,X0,sK21)
| ~ coll(sK20,X0,sK22) ),
inference(superposition,[status(thm)],[c_8575,c_94]) ).
tcf(c_14811,plain,
( midp(sK20,sK21,sK22)
| ~ midp(sK21,sK21,sK21)
| ~ coll(sK20,sK21,sK22) ),
inference(instantiation,[status(thm)],[c_14792]) ).
tcf(c_14917,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK20,X0,X1,sK20,sK21,sK20,sK22)
| ~ para(sK23,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_14091,c_69]) ).
tcf(c_14919,plain,
! [X0: $i,X1: $i] :
( eqangle(sK20,sK21,sK23,sK20,sK20,sK22,X0,X1)
| ~ para(sK23,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_14091,c_67]) ).
tcf(c_15021,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK21,X0,X1,sK21,sK22,sK21,sK20)
| ~ para(sK23,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_14108,c_69]) ).
tcf(c_15244,plain,
! [X0: $i] :
( circle(sK20,sK21,X0,sK24)
| ~ midp(sK21,sK21,sK24)
| ~ midp(sK20,sK21,X0) ),
inference(superposition,[status(thm)],[c_117,c_7927]) ).
tcf(c_15246,plain,
( circle(sK20,sK21,sK24,sK24)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_7573,c_7927]) ).
tcf(c_15256,plain,
( circle(sK20,sK21,sK21,sK24)
| ~ midp(sK21,sK21,sK24)
| ~ midp(sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_15244]) ).
tcf(c_15922,plain,
( cong(sK20,sK20,sK21,sK21)
| ~ midp(sK24,sK20,sK21)
| ~ midp(sK20,sK20,sK24) ),
inference(superposition,[status(thm)],[c_7580,c_7958]) ).
tcf(c_16085,plain,
( cong(sK20,sK21,sK21,sK24)
| ~ midp(sK24,sK20,sK24)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_7384,c_7962]) ).
tcf(c_16087,plain,
( cong(sK20,sK21,sK20,sK21)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_7845,c_7962]) ).
tcf(c_16147,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK21,X1,X0)
| ~ midp(X1,sK20,sK24)
| ~ midp(X0,sK20,sK24) ),
inference(superposition,[status(thm)],[c_7384,c_7999]) ).
tcf(c_16164,plain,
! [X0: $i,X1: $i] :
( perp(X1,X0,sK20,sK21)
| ~ midp(X1,sK20,sK24)
| ~ midp(X0,sK20,sK24) ),
inference(superposition,[status(thm)],[c_16147,c_56]) ).
tcf(c_16172,plain,
( perp(sK23,sK20,sK23,sK20)
| ~ midp(sK20,sK20,sK24)
| ~ midp(sK22,sK20,sK24) ),
inference(superposition,[status(thm)],[c_16147,c_10551]) ).
tcf(c_16777,plain,
para(sK20,sK23,sK20,sK23),
inference(superposition,[status(thm)],[c_10374,c_52]) ).
tcf(c_16800,plain,
! [X0: $i] :
( midp(X0,sK22,sK22)
| ~ midp(X0,sK23,sK23)
| ~ para(sK23,sK22,sK23,sK22) ),
inference(superposition,[status(thm)],[c_10399,c_113]) ).
tcf(c_16806,plain,
coll(sK23,sK22,sK22),
inference(superposition,[status(thm)],[c_10399,c_115]) ).
tcf(c_16810,plain,
! [X0: $i] :
( midp(X0,sK22,sK22)
| ~ midp(X0,sK23,sK23) ),
inference(forward_subsumption_resolution,[status(thm)],[c_16800,c_10399]) ).
tcf(c_16813,plain,
( midp(sK21,sK22,sK22)
| ~ midp(sK21,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_16810]) ).
tcf(c_16816,plain,
coll(sK22,sK23,sK22),
inference(superposition,[status(thm)],[c_16806,c_50]) ).
tcf(c_17148,plain,
coll(sK22,sK22,sK23),
inference(superposition,[status(thm)],[c_16816,c_49]) ).
tcf(c_17154,plain,
coll(sK20,sK23,sK22),
inference(superposition,[status(thm)],[c_17148,c_6908]) ).
tcf(c_17169,plain,
coll(sK23,sK21,sK21),
inference(superposition,[status(thm)],[c_10400,c_115]) ).
tcf(c_17186,plain,
coll(sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_17169,c_50]) ).
tcf(c_17193,plain,
coll(sK20,sK22,sK23),
inference(superposition,[status(thm)],[c_17154,c_49]) ).
tcf(c_17574,plain,
! [X0: $i] :
( coll(sK23,X0,sK20)
| ~ coll(sK20,sK22,X0) ),
inference(superposition,[status(thm)],[c_17193,c_51]) ).
tcf(c_17578,plain,
coll(sK26,sK23,sK20),
inference(superposition,[status(thm)],[c_17193,c_6976]) ).
tcf(c_17661,plain,
coll(sK26,sK20,sK23),
inference(superposition,[status(thm)],[c_17578,c_49]) ).
tcf(c_17763,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK20,sK20,sK22,X0,X1,sK20,sK21)
| ~ para(sK23,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_88,c_13692]) ).
tcf(c_17855,plain,
coll(sK20,sK26,sK23),
inference(superposition,[status(thm)],[c_17661,c_50]) ).
tcf(c_18024,plain,
eqangle(sK23,sK21,sK21,sK20,sK23,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_5122,c_13693]) ).
tcf(c_18074,plain,
eqangle(sK23,sK21,sK23,sK21,sK21,sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_18024,c_69]) ).
tcf(c_18213,plain,
( perp(sK23,sK21,sK23,sK21)
| ~ perp(sK21,sK20,sK21,sK20) ),
inference(superposition,[status(thm)],[c_18074,c_123]) ).
tcf(c_18216,plain,
eqangle(sK21,sK20,sK21,sK20,sK23,sK21,sK23,sK21),
inference(superposition,[status(thm)],[c_18074,c_68]) ).
tcf(c_18269,plain,
coll(sK20,sK23,sK20),
inference(superposition,[status(thm)],[c_17855,c_6815]) ).
tcf(c_19105,plain,
coll(sK21,sK21,sK24),
inference(global_subsumption_just,[status(thm)],[c_12996,c_11337,c_12077]) ).
tcf(c_19109,plain,
coll(sK21,sK24,sK21),
inference(superposition,[status(thm)],[c_19105,c_49]) ).
tcf(c_20019,plain,
! [X0: $i,X1: $i] :
( perp(sK27,sK24,X1,X0)
| ~ perp(sK27,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_20107,plain,
! [X0: $i] :
( midp(X0,sK20,sK20)
| ~ midp(X0,sK23,sK23)
| ~ para(sK23,sK20,sK23,sK20) ),
inference(superposition,[status(thm)],[c_10401,c_113]) ).
tcf(c_20108,plain,
! [X0: $i] :
( midp(sK20,X0,sK20)
| ~ midp(sK23,X0,sK23)
| ~ coll(sK20,X0,sK20) ),
inference(superposition,[status(thm)],[c_10401,c_94]) ).
tcf(c_20117,plain,
! [X0: $i] :
( midp(X0,sK20,sK20)
| ~ midp(X0,sK23,sK23) ),
inference(forward_subsumption_resolution,[status(thm)],[c_20107,c_10401]) ).
tcf(c_20120,plain,
( midp(sK21,sK20,sK20)
| ~ midp(sK21,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_20117]) ).
tcf(c_20121,plain,
( midp(sK20,sK21,sK20)
| ~ midp(sK23,sK21,sK23)
| ~ coll(sK20,sK21,sK20) ),
inference(instantiation,[status(thm)],[c_20108]) ).
tcf(c_20123,plain,
! [X0: $i] :
( midp(sK21,X0,sK24)
| ~ midp(sK24,X0,sK21)
| ~ coll(sK21,X0,sK24) ),
inference(superposition,[status(thm)],[c_10825,c_94]) ).
tcf(c_20140,plain,
( midp(sK21,sK21,sK24)
| ~ midp(sK24,sK21,sK21)
| ~ coll(sK21,sK21,sK24) ),
inference(instantiation,[status(thm)],[c_20123]) ).
tcf(c_20163,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK21,X0,X1)
| ~ perp(X0,X1,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_20164,plain,
( perp(sK20,sK21,sK21,sK21)
| ~ perp(sK21,sK21,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_20163]) ).
tcf(c_21887,plain,
coll(sK20,sK23,sK23),
inference(superposition,[status(thm)],[c_16777,c_115]) ).
tcf(c_21897,plain,
coll(sK23,sK20,sK23),
inference(superposition,[status(thm)],[c_21887,c_50]) ).
tcf(c_24496,plain,
( perp(sK21,sK22,sK21,sK20)
| ~ perp(sK21,sK23,sK23,sK21) ),
inference(superposition,[status(thm)],[c_8727,c_123]) ).
tcf(c_24609,plain,
coll(sK20,sK24,sK21),
inference(superposition,[status(thm)],[c_19105,c_8363]) ).
tcf(c_24766,plain,
coll(sK24,sK20,sK21),
inference(superposition,[status(thm)],[c_24609,c_50]) ).
tcf(c_24767,plain,
coll(sK20,sK21,sK24),
inference(superposition,[status(thm)],[c_24609,c_49]) ).
tcf(c_25346,plain,
coll(sK22,sK24,sK20),
inference(superposition,[status(thm)],[c_24767,c_8509]) ).
tcf(c_25347,plain,
coll(sK21,sK24,sK20),
inference(superposition,[status(thm)],[c_24767,c_8037]) ).
tcf(c_25756,plain,
coll(sK22,sK20,sK24),
inference(superposition,[status(thm)],[c_25346,c_49]) ).
tcf(c_26039,plain,
coll(sK20,sK22,sK24),
inference(superposition,[status(thm)],[c_25756,c_50]) ).
tcf(c_26241,plain,
! [X0: $i,X1: $i] :
( eqangle(sK21,sK24,sK21,X0,X1,sK21,X1,X0)
| ~ circle(sK20,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_5119,c_97]) ).
tcf(c_26665,plain,
( perp(sK23,sK20,sK23,sK20)
| ~ perp(sK20,sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_14150,c_123]) ).
tcf(c_26760,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK24,sK21,sK20,sK21,sK24,sK21)
| ~ para(X0,X1,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_26761,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK24,sK21)
| ~ perp(sK20,sK21,sK24,sK21)
| ~ eqangle(X0,X1,sK24,sK21,sK20,sK21,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_8531]) ).
tcf(c_26762,plain,
( eqangle(sK21,sK21,sK24,sK21,sK20,sK21,sK24,sK21)
| ~ para(sK21,sK21,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_26760]) ).
tcf(c_26763,plain,
( perp(sK21,sK21,sK24,sK21)
| ~ perp(sK20,sK21,sK24,sK21)
| ~ eqangle(sK21,sK21,sK24,sK21,sK20,sK21,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_26761]) ).
tcf(c_26769,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK20,sK21,sK21,sK24,sK20,sK21)
| ~ para(X0,X1,sK21,sK24) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_26770,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK20,sK21)
| ~ perp(sK21,sK24,sK20,sK21)
| ~ eqangle(X0,X1,sK20,sK21,sK21,sK24,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_8712]) ).
tcf(c_26771,plain,
( eqangle(sK21,sK21,sK20,sK21,sK21,sK24,sK20,sK21)
| ~ para(sK21,sK21,sK21,sK24) ),
inference(instantiation,[status(thm)],[c_26769]) ).
tcf(c_26772,plain,
( perp(sK21,sK21,sK20,sK21)
| ~ perp(sK21,sK24,sK20,sK21)
| ~ eqangle(sK21,sK21,sK20,sK21,sK21,sK24,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_26770]) ).
tcf(c_26866,plain,
( cyclic(sK23,sK21,sK20,sK20)
| ~ coll(sK20,sK20,sK21) ),
inference(superposition,[status(thm)],[c_14168,c_91]) ).
tcf(c_26870,plain,
cyclic(sK23,sK21,sK20,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_26866,c_10788]) ).
tcf(c_27038,plain,
! [X0: $i] :
( para(sK21,sK24,sK21,sK21)
| ~ circle(sK20,sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_26241,c_87]) ).
tcf(c_27717,plain,
( cong(sK20,sK20,sK21,sK21)
| ~ cyclic(sK20,sK20,sK21,sK21)
| ~ cyclic(sK20,sK20,sK21,sK23) ),
inference(superposition,[status(thm)],[c_18216,c_92]) ).
tcf(c_28269,plain,
cyclic(sK21,sK23,sK20,sK20),
inference(superposition,[status(thm)],[c_26870,c_64]) ).
tcf(c_28270,plain,
cyclic(sK23,sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_26870,c_63]) ).
tcf(c_28581,plain,
cyclic(sK21,sK20,sK23,sK20),
inference(superposition,[status(thm)],[c_28269,c_63]) ).
tcf(c_28592,plain,
cyclic(sK23,sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_28270,c_62]) ).
tcf(c_29196,plain,
cong(sK24,sK20,sK24,sK21),
inference(global_subsumption_just,[status(thm)],[c_7582,c_178,c_182,c_236,c_7582,c_8038,c_8356,c_8586,c_9112,c_10289,c_10294,c_11264,c_11337,c_11692,c_12077,c_13413,c_16813]) ).
tcf(c_29202,plain,
( midp(sK24,sK20,sK21)
| ~ coll(sK24,sK20,sK21) ),
inference(superposition,[status(thm)],[c_29196,c_116]) ).
tcf(c_29213,plain,
midp(sK24,sK20,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_29202,c_24766]) ).
tcf(c_29243,plain,
cong(sK21,sK20,sK21,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_7580,c_29213]) ).
tcf(c_29290,plain,
( midp(sK21,sK20,sK21)
| ~ coll(sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_29243,c_116]) ).
tcf(c_29296,plain,
cong(sK21,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_29243,c_72]) ).
tcf(c_29302,plain,
midp(sK21,sK20,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_29290,c_8038]) ).
tcf(c_29574,plain,
! [X0: $i,X1: $i] :
( para(sK24,X0,sK21,X1)
| ~ midp(X0,sK20,X1) ),
inference(superposition,[status(thm)],[c_29213,c_93]) ).
tcf(c_29581,plain,
( para(sK24,sK21,sK21,sK21)
| ~ midp(sK21,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_29574]) ).
tcf(c_29586,plain,
midp(sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_29302,c_59]) ).
tcf(c_29587,plain,
( midp(sK24,sK20,sK24)
| ~ coll(sK24,sK20,sK24) ),
inference(superposition,[status(thm)],[c_29302,c_10199]) ).
tcf(c_29929,plain,
( cong(sK20,sK21,sK21,sK20)
| ~ midp(sK21,sK24,sK21)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_8196,c_7962]) ).
tcf(c_30451,plain,
! [X0: $i,X1: $i] :
( para(sK21,X0,sK20,X1)
| ~ midp(X0,sK21,X1) ),
inference(superposition,[status(thm)],[c_29586,c_93]) ).
tcf(c_30458,plain,
( para(sK21,sK21,sK20,sK21)
| ~ midp(sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_30451]) ).
tcf(c_31028,plain,
( circle(sK20,sK21,sK21,sK24)
| ~ midp(sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_16087,c_7927]) ).
tcf(c_31649,plain,
para(sK21,sK24,sK21,sK21),
inference(global_subsumption_just,[status(thm)],[c_27038,c_178,c_182,c_236,c_8038,c_8356,c_8586,c_9112,c_10289,c_10294,c_10837,c_11264,c_11337,c_11692,c_12077,c_13413,c_16813,c_29581]) ).
tcf(c_31651,plain,
! [X0: $i] :
( midp(X0,sK24,sK21)
| ~ midp(X0,sK21,sK21)
| ~ para(sK21,sK21,sK21,sK24) ),
inference(superposition,[status(thm)],[c_31649,c_113]) ).
tcf(c_31652,plain,
! [X0: $i] :
( midp(sK24,X0,sK21)
| ~ midp(sK21,X0,sK21)
| ~ coll(sK24,X0,sK21) ),
inference(superposition,[status(thm)],[c_31649,c_94]) ).
tcf(c_31655,plain,
para(sK21,sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_31649,c_53]) ).
tcf(c_31665,plain,
! [X0: $i] :
( midp(X0,sK24,sK21)
| ~ midp(X0,sK21,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31651,c_31655]) ).
tcf(c_31668,plain,
( midp(sK21,sK24,sK21)
| ~ midp(sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_31665]) ).
tcf(c_31670,plain,
( midp(sK24,sK21,sK21)
| ~ midp(sK21,sK21,sK21)
| ~ coll(sK24,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_31652]) ).
tcf(c_31846,plain,
circle(sK20,sK21,sK21,sK24),
inference(global_subsumption_just,[status(thm)],[c_31028,c_178,c_182,c_236,c_7895,c_8038,c_8042,c_8356,c_8417,c_9112,c_11264,c_11337,c_11692,c_12077,c_13264,c_13413,c_14775,c_14811,c_15256,c_20140,c_31670]) ).
tcf(c_31848,plain,
( perp(sK21,sK21,sK21,sK24)
| ~ coll(sK20,sK21,sK24) ),
inference(superposition,[status(thm)],[c_31846,c_102]) ).
tcf(c_31852,plain,
perp(sK21,sK21,sK21,sK24),
inference(forward_subsumption_resolution,[status(thm)],[c_31848,c_24767]) ).
tcf(c_32080,plain,
cyclic(sK20,sK21,sK23,sK20),
inference(superposition,[status(thm)],[c_28581,c_64]) ).
tcf(c_32252,plain,
! [X0: $i] :
( cyclic(sK20,sK20,sK21,X0)
| ~ cyclic(sK23,sK20,sK20,X0) ),
inference(superposition,[status(thm)],[c_28592,c_65]) ).
tcf(c_32261,plain,
( cyclic(sK20,sK20,sK21,sK21)
| ~ cyclic(sK23,sK20,sK20,sK21) ),
inference(instantiation,[status(thm)],[c_32252]) ).
tcf(c_32417,plain,
( cong(sK20,sK21,sK21,sK20)
| ~ midp(sK21,sK20,sK24) ),
inference(superposition,[status(thm)],[c_29296,c_7958]) ).
tcf(c_32615,plain,
cong(sK20,sK21,sK21,sK20),
inference(global_subsumption_just,[status(thm)],[c_32417,c_178,c_182,c_236,c_8038,c_8356,c_9112,c_11264,c_11337,c_11692,c_12077,c_13413,c_20140,c_29929,c_31668,c_31670]) ).
tcf(c_32619,plain,
cong(sK20,sK21,sK20,sK21),
inference(superposition,[status(thm)],[c_32615,c_71]) ).
tcf(c_32751,plain,
perp(sK21,sK24,sK21,sK21),
inference(superposition,[status(thm)],[c_31852,c_56]) ).
tcf(c_32992,plain,
cyclic(sK20,sK21,sK20,sK23),
inference(superposition,[status(thm)],[c_32080,c_62]) ).
tcf(c_33280,plain,
( midp(sK20,sK21,sK21)
| ~ coll(sK20,sK21,sK21) ),
inference(superposition,[status(thm)],[c_32619,c_116]) ).
tcf(c_33297,plain,
midp(sK20,sK21,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_33280,c_7895]) ).
tcf(c_33457,plain,
midp(sK20,sK24,sK24),
inference(superposition,[status(thm)],[c_33297,c_10259]) ).
tcf(c_33465,plain,
coll(sK20,sK24,sK24),
inference(superposition,[status(thm)],[c_33457,c_118]) ).
tcf(c_33536,plain,
coll(sK24,sK20,sK24),
inference(superposition,[status(thm)],[c_33465,c_50]) ).
tcf(c_33540,plain,
midp(sK24,sK20,sK24),
inference(backward_subsumption_resolution,[status(thm)],[c_29587,c_33536]) ).
tcf(c_33541,plain,
( cong(sK20,sK21,sK21,sK24)
| ~ midp(sK21,sK21,sK24) ),
inference(backward_subsumption_resolution,[status(thm)],[c_16085,c_33540]) ).
tcf(c_33637,plain,
cong(sK20,sK21,sK21,sK24),
inference(global_subsumption_just,[status(thm)],[c_33541,c_178,c_182,c_236,c_8038,c_8356,c_9112,c_11264,c_11337,c_11692,c_12077,c_13413,c_16085,c_20140,c_31670,c_33540]) ).
tcf(c_33640,plain,
cong(sK21,sK24,sK20,sK21),
inference(superposition,[status(thm)],[c_33637,c_72]) ).
tcf(c_33644,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK27,sK24,X2,X3)
| ~ para(sK27,sK24,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_33684,plain,
( perp(sK20,sK22,sK23,sK20)
| ~ midp(sK20,sK20,sK24)
| ~ midp(sK23,sK20,sK24) ),
inference(superposition,[status(thm)],[c_16147,c_10564]) ).
tcf(c_33770,plain,
para(sK20,sK21,sK21,sK21),
inference(superposition,[status(thm)],[c_32751,c_7669]) ).
tcf(c_33872,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK20,sK21)
| ~ para(sK20,sK21,sK21,sK21) ),
inference(superposition,[status(thm)],[c_33770,c_113]) ).
tcf(c_33873,plain,
! [X0: $i] :
( midp(sK21,X0,sK21)
| ~ midp(sK20,X0,sK21)
| ~ coll(sK21,X0,sK21) ),
inference(superposition,[status(thm)],[c_33770,c_94]) ).
tcf(c_33885,plain,
! [X0: $i] :
( midp(X0,sK21,sK21)
| ~ midp(X0,sK20,sK21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_33872,c_33770]) ).
tcf(c_33944,plain,
midp(sK21,sK21,sK21),
inference(superposition,[status(thm)],[c_29302,c_33885]) ).
tcf(c_34037,plain,
cyclic(sK20,sK20,sK21,sK23),
inference(superposition,[status(thm)],[c_32992,c_63]) ).
tcf(c_34056,plain,
midp(sK21,sK23,sK23),
inference(superposition,[status(thm)],[c_33944,c_10286]) ).
tcf(c_34725,plain,
! [X0: $i] :
( perp(sK27,sK24,X0,sK24)
| ~ perp(sK27,sK24,sK24,X0) ),
inference(instantiation,[status(thm)],[c_20019]) ).
tcf(c_34729,plain,
( perp(sK27,sK24,sK21,sK24)
| ~ perp(sK27,sK24,sK24,sK21) ),
inference(instantiation,[status(thm)],[c_34725]) ).
tcf(c_35157,plain,
cong(sK21,sK24,sK21,sK20),
inference(superposition,[status(thm)],[c_33640,c_71]) ).
tcf(c_35158,plain,
( cong(sK20,sK24,sK20,sK21)
| ~ midp(sK24,sK20,sK24) ),
inference(superposition,[status(thm)],[c_33640,c_7958]) ).
tcf(c_35162,plain,
cong(sK20,sK24,sK20,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_35158,c_33540]) ).
tcf(c_35788,plain,
( midp(sK21,sK24,sK20)
| ~ coll(sK21,sK24,sK20) ),
inference(superposition,[status(thm)],[c_35157,c_116]) ).
tcf(c_35801,plain,
midp(sK21,sK24,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_35788,c_25347]) ).
tcf(c_35891,plain,
midp(sK21,sK20,sK24),
inference(superposition,[status(thm)],[c_35801,c_59]) ).
tcf(c_36019,plain,
( midp(sK20,sK24,sK21)
| ~ coll(sK20,sK24,sK21) ),
inference(superposition,[status(thm)],[c_35162,c_116]) ).
tcf(c_36031,plain,
midp(sK20,sK24,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_36019,c_24609]) ).
tcf(c_36647,plain,
( midp(sK23,sK20,sK23)
| ~ midp(sK21,sK20,sK21) ),
inference(superposition,[status(thm)],[c_21897,c_9122]) ).
tcf(c_36660,plain,
midp(sK23,sK20,sK23),
inference(forward_subsumption_resolution,[status(thm)],[c_36647,c_29302]) ).
tcf(c_36697,plain,
( midp(sK23,sK23,sK21)
| ~ midp(sK21,sK23,sK23) ),
inference(superposition,[status(thm)],[c_8348,c_9123]) ).
tcf(c_36716,plain,
midp(sK23,sK23,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_36697,c_34056]) ).
tcf(c_36813,plain,
( midp(sK21,sK23,sK21)
| ~ midp(sK20,sK23,sK20) ),
inference(superposition,[status(thm)],[c_17186,c_9124]) ).
tcf(c_36945,plain,
midp(sK23,sK23,sK20),
inference(superposition,[status(thm)],[c_36660,c_59]) ).
tcf(c_37001,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK21,X1)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_36716,c_93]) ).
tcf(c_37008,plain,
( para(sK23,sK21,sK21,sK21)
| ~ midp(sK21,sK23,sK21) ),
inference(instantiation,[status(thm)],[c_37001]) ).
tcf(c_37867,plain,
( eqangle(sK25,sK23,sK23,sK22,sK22,sK23,sK23,sK26)
| ~ eqangle(sK22,sK23,sK23,sK26,sK25,sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_39130,plain,
( midp(sK21,sK24,sK21)
| ~ midp(sK20,sK24,sK21) ),
inference(superposition,[status(thm)],[c_19109,c_33873]) ).
tcf(c_39133,plain,
midp(sK21,sK24,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_39130,c_36031]) ).
tcf(c_39672,plain,
midp(sK21,sK21,sK24),
inference(superposition,[status(thm)],[c_39133,c_59]) ).
tcf(c_39689,plain,
circle(sK20,sK21,sK24,sK24),
inference(backward_subsumption_resolution,[status(thm)],[c_15246,c_39672]) ).
tcf(c_39751,plain,
( perp(sK21,sK24,sK24,sK24)
| ~ coll(sK20,sK21,sK24) ),
inference(superposition,[status(thm)],[c_39689,c_102]) ).
tcf(c_39755,plain,
perp(sK21,sK24,sK24,sK24),
inference(forward_subsumption_resolution,[status(thm)],[c_39751,c_24767]) ).
tcf(c_41076,plain,
para(sK20,sK21,sK24,sK24),
inference(superposition,[status(thm)],[c_39755,c_7669]) ).
tcf(c_41337,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK21,X0,X1)
| ~ perp(sK24,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_41076,c_58]) ).
tcf(c_44335,plain,
( para(sK21,sK23,sK21,sK24)
| ~ perp(sK27,sK24,sK21,sK24)
| ~ perp(sK21,sK23,sK27,sK24) ),
inference(instantiation,[status(thm)],[c_7411]) ).
tcf(c_44439,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK23,sK20,X1,X2)
| ~ midp(X0,sK20,X2)
| ~ midp(X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_44440,plain,
( para(sK23,sK20,sK21,sK21)
| ~ midp(sK21,sK20,sK21)
| ~ midp(sK21,sK23,sK21) ),
inference(instantiation,[status(thm)],[c_44439]) ).
tcf(c_44644,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK23,sK22,X1,X2)
| ~ midp(X0,sK22,X2)
| ~ midp(X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_44645,plain,
( para(sK23,sK22,sK21,sK21)
| ~ midp(sK21,sK22,sK21)
| ~ midp(sK21,sK23,sK21) ),
inference(instantiation,[status(thm)],[c_44644]) ).
tcf(c_45051,plain,
( eqangle(sK20,sK23,sK20,sK21,sK20,sK21,sK20,sK22)
| ~ para(sK23,sK20,sK20,sK22) ),
inference(superposition,[status(thm)],[c_14917,c_13686]) ).
tcf(c_45503,plain,
! [X0: $i,X1: $i] :
( perp(sK20,sK21,sK23,sK20)
| ~ perp(sK20,sK22,X0,X1)
| ~ para(sK23,sK20,X0,X1) ),
inference(superposition,[status(thm)],[c_14919,c_123]) ).
tcf(c_45523,plain,
( perp(sK20,sK21,sK23,sK20)
| ~ perp(sK20,sK22,sK21,sK21)
| ~ para(sK23,sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_45503]) ).
tcf(c_46184,plain,
! [X0: $i,X1: $i] :
( perp(sK23,sK21,X0,X1)
| ~ perp(sK21,sK22,sK21,sK20)
| ~ para(sK23,sK21,X0,X1) ),
inference(superposition,[status(thm)],[c_15021,c_123]) ).
tcf(c_46229,plain,
( perp(sK23,sK21,sK21,sK21)
| ~ perp(sK21,sK22,sK21,sK20)
| ~ para(sK23,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_46184]) ).
tcf(c_47910,plain,
cong(sK20,sK20,sK21,sK21),
inference(global_subsumption_just,[status(thm)],[c_15922,c_27717,c_28592,c_32261,c_34037]) ).
tcf(c_47913,plain,
cong(sK21,sK21,sK20,sK20),
inference(superposition,[status(thm)],[c_47910,c_72]) ).
tcf(c_48855,plain,
( cong(sK20,sK21,sK20,sK20)
| ~ midp(sK21,sK20,sK24) ),
inference(superposition,[status(thm)],[c_47913,c_7958]) ).
tcf(c_48856,plain,
cong(sK20,sK21,sK20,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_48855,c_35891]) ).
tcf(c_49267,plain,
( perp(sK20,sK21,sK20,sK21)
| ~ midp(sK24,sK20,sK24) ),
inference(superposition,[status(thm)],[c_16164,c_41337]) ).
tcf(c_49268,plain,
perp(sK20,sK21,sK20,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_49267,c_33540]) ).
tcf(c_49660,plain,
( midp(sK20,sK21,sK20)
| ~ coll(sK20,sK21,sK20) ),
inference(superposition,[status(thm)],[c_48856,c_116]) ).
tcf(c_49672,plain,
midp(sK20,sK21,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_49660,c_9687]) ).
tcf(c_49748,plain,
perp(sK23,sK20,sK23,sK20),
inference(global_subsumption_just,[status(thm)],[c_16172,c_26665,c_49268]) ).
tcf(c_49750,plain,
perp(sK20,sK21,sK20,sK22),
inference(backward_subsumption_resolution,[status(thm)],[c_10570,c_49748]) ).
tcf(c_49751,plain,
perp(sK20,sK23,sK23,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_10567,c_49750]) ).
tcf(c_49899,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK20,sK20,sK22)
| ~ para(sK23,sK20,X0,X1)
| ~ para(X0,X1,sK20,sK21) ),
inference(superposition,[status(thm)],[c_17763,c_122]) ).
tcf(c_49948,plain,
( para(sK23,sK20,sK20,sK22)
| ~ para(sK21,sK21,sK20,sK21)
| ~ para(sK23,sK20,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_49899]) ).
tcf(c_50285,plain,
perp(sK20,sK21,sK21,sK20),
inference(superposition,[status(thm)],[c_49268,c_55]) ).
tcf(c_50315,plain,
( eqangle(sK22,sK23,sK23,sK26,sK25,sK23,sK23,sK22)
| ~ eqangle(sK23,sK22,sK23,sK26,sK25,sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_50704,plain,
perp(sK21,sK20,sK20,sK21),
inference(superposition,[status(thm)],[c_50285,c_56]) ).
tcf(c_50811,plain,
( cong(sK20,sK23,sK20,sK20)
| ~ midp(sK23,sK23,sK20) ),
inference(superposition,[status(thm)],[c_49751,c_104]) ).
tcf(c_50821,plain,
cong(sK20,sK23,sK20,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_50811,c_36945]) ).
tcf(c_51330,plain,
perp(sK21,sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_50704,c_55]) ).
tcf(c_51351,plain,
perp(sK23,sK21,sK23,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_18213,c_51330]) ).
tcf(c_51352,plain,
perp(sK21,sK22,sK21,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_10571,c_51351]) ).
tcf(c_51353,plain,
perp(sK21,sK23,sK23,sK21),
inference(backward_subsumption_resolution,[status(thm)],[c_10568,c_51352]) ).
tcf(c_57825,plain,
( midp(sK20,sK23,sK20)
| ~ coll(sK20,sK23,sK20) ),
inference(superposition,[status(thm)],[c_50821,c_116]) ).
tcf(c_57836,plain,
midp(sK20,sK23,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_57825,c_18269]) ).
tcf(c_60376,plain,
perp(sK20,sK22,sK23,sK20),
inference(global_subsumption_just,[status(thm)],[c_33684,c_178,c_182,c_236,c_6865,c_8038,c_8356,c_8586,c_9112,c_10289,c_10294,c_10564,c_11264,c_11337,c_11692,c_12077,c_13301,c_13413,c_16813,c_20164,c_26771,c_26772,c_31655,c_36813,c_44440,c_45523,c_57836]) ).
tcf(c_60378,plain,
perp(sK21,sK20,sK23,sK20),
inference(backward_subsumption_resolution,[status(thm)],[c_10558,c_60376]) ).
tcf(c_61154,plain,
eqangle(sK20,sK23,sK20,sK21,sK20,sK21,sK20,sK22),
inference(global_subsumption_just,[status(thm)],[c_45051,c_178,c_182,c_236,c_8038,c_8356,c_8586,c_9112,c_10289,c_10294,c_11264,c_11337,c_11692,c_12077,c_13413,c_16813,c_30458,c_36813,c_44440,c_45051,c_49948,c_57836]) ).
tcf(c_61158,plain,
( para(sK20,sK23,sK20,sK21)
| ~ para(sK20,sK21,sK20,sK22) ),
inference(superposition,[status(thm)],[c_61154,c_122]) ).
tcf(c_61164,plain,
para(sK20,sK23,sK20,sK21),
inference(forward_subsumption_resolution,[status(thm)],[c_61158,c_8376]) ).
tcf(c_61188,plain,
! [X0: $i] :
( midp(sK23,X0,sK21)
| ~ midp(sK20,X0,sK20)
| ~ coll(sK23,X0,sK21) ),
inference(superposition,[status(thm)],[c_61164,c_94]) ).
tcf(c_61207,plain,
( midp(sK23,sK21,sK21)
| ~ midp(sK20,sK21,sK20)
| ~ coll(sK23,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_61188]) ).
tcf(c_65839,plain,
perp(sK23,sK20,sK21,sK20),
inference(superposition,[status(thm)],[c_60378,c_56]) ).
tcf(c_67213,plain,
! [X0: $i,X1: $i,X2: $i] :
( perp(sK27,sK24,sK24,X2)
| ~ para(sK27,sK24,X0,X1)
| ~ perp(X0,X1,sK24,X2) ),
inference(instantiation,[status(thm)],[c_33644]) ).
tcf(c_67214,plain,
( perp(sK27,sK24,sK24,sK21)
| ~ perp(sK21,sK21,sK24,sK21)
| ~ para(sK27,sK24,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_67213]) ).
tcf(c_70097,plain,
( cong(sK23,sK21,sK23,sK20)
| ~ midp(sK20,sK21,sK20) ),
inference(superposition,[status(thm)],[c_65839,c_104]) ).
tcf(c_70100,plain,
cong(sK23,sK21,sK23,sK20),
inference(forward_subsumption_resolution,[status(thm)],[c_70097,c_49672]) ).
tcf(c_76828,plain,
cong(sK23,sK21,sK20,sK23),
inference(superposition,[status(thm)],[c_70100,c_71]) ).
tcf(c_78419,plain,
coll(sK23,sK24,sK20),
inference(superposition,[status(thm)],[c_26039,c_17574]) ).
tcf(c_78596,plain,
coll(sK23,sK20,sK24),
inference(superposition,[status(thm)],[c_78419,c_49]) ).
tcf(c_85043,plain,
cong(sK20,sK23,sK23,sK21),
inference(superposition,[status(thm)],[c_76828,c_72]) ).
tcf(c_86731,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X1,sK26,X2,X3,X1,sK26)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_86732,plain,
( eqangle(sK21,sK21,sK21,sK26,sK21,sK21,sK21,sK26)
| ~ para(sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_86731]) ).
tcf(c_91133,plain,
cong(sK20,sK23,sK21,sK23),
inference(superposition,[status(thm)],[c_85043,c_71]) ).
tcf(c_96145,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK22,sK23,sK26,sK25,sK23,sK23,sK22)
| ~ eqangle(sK23,sK22,sK23,sK26,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK25,sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_96146,plain,
( eqangle(sK23,sK22,sK23,sK26,sK25,sK23,sK23,sK22)
| ~ eqangle(sK21,sK21,sK21,sK21,sK25,sK23,sK23,sK22)
| ~ eqangle(sK23,sK22,sK23,sK26,sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_96145]) ).
tcf(c_99176,plain,
( cong(sK21,sK23,sK21,sK23)
| ~ midp(sK23,sK20,sK24) ),
inference(superposition,[status(thm)],[c_91133,c_7959]) ).
tcf(c_116468,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK25,sK23,sK23,sK22,X2,X3,X0,X1)
| ~ eqangle(sK23,sK22,sK25,sK23,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_117087,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK23,X1,X0)
| ~ para(sK25,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_117091,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK25,sK23,X2,X3)
| ~ eqangle(sK25,sK23,X0,X1,X2,X3,X0,X1) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_117323,plain,
! [X0: $i,X1: $i] :
( eqangle(sK25,sK23,sK23,sK22,sK25,sK23,X0,X1)
| ~ eqangle(sK23,sK22,sK25,sK23,X0,X1,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_116468]) ).
tcf(c_117324,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK22,sK25,sK23,X0,X1,sK25,sK23)
| ~ para(sK23,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_117325,plain,
( eqangle(sK25,sK23,sK23,sK22,sK25,sK23,sK21,sK21)
| ~ eqangle(sK23,sK22,sK25,sK23,sK21,sK21,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_117323]) ).
tcf(c_117326,plain,
( eqangle(sK23,sK22,sK25,sK23,sK21,sK21,sK25,sK23)
| ~ para(sK23,sK22,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_117324]) ).
tcf(c_117494,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK25,sK23,sK23,sK22)
| ~ eqangle(sK25,sK23,sK23,sK22,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_117498,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK25,sK23,sK23,sK22)
| ~ eqangle(X4,X5,X6,X7,sK25,sK23,sK23,sK22)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_119455,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK25,sK23)
| ~ para(sK25,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_119459,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK25,sK23)
| ~ perp(X2,X3,sK25,sK23)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_119460,plain,
( para(sK21,sK21,sK25,sK23)
| ~ perp(sK21,sK21,sK21,sK21)
| ~ perp(sK21,sK21,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_119459]) ).
tcf(c_119715,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK25,X1,X0)
| ~ para(sK23,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_120093,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,sK25,X1)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK25,X2,X1)
| ~ para(X0,X1,X2,sK25) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_120782,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK22,sK23,sK26,X0,X1,X2,X3)
| ~ eqangle(sK23,sK22,X0,X1,sK23,sK26,X2,X3) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_120783,plain,
( eqangle(sK23,sK22,sK23,sK26,sK21,sK21,sK21,sK21)
| ~ eqangle(sK23,sK22,sK21,sK21,sK23,sK26,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_120782]) ).
tcf(c_121124,plain,
( para(sK25,sK23,sK25,sK23)
| ~ eqangle(sK25,sK23,sK23,sK22,sK25,sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_117091]) ).
tcf(c_121125,plain,
( eqangle(sK25,sK23,sK23,sK22,sK25,sK23,sK23,sK22)
| ~ eqangle(sK23,sK22,sK25,sK23,sK23,sK22,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_117323]) ).
tcf(c_122293,plain,
! [X0: $i,X1: $i] :
( eqangle(sK25,sK23,X0,X1,sK25,sK23,sK23,sK22)
| ~ eqangle(sK25,sK23,sK23,sK22,sK25,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_117494]) ).
tcf(c_122294,plain,
( eqangle(sK25,sK23,sK21,sK21,sK25,sK23,sK23,sK22)
| ~ eqangle(sK25,sK23,sK23,sK22,sK25,sK23,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_122293]) ).
tcf(c_124916,plain,
( para(sK25,sK23,sK23,sK25)
| ~ para(sK25,sK23,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_117087]) ).
tcf(c_128986,plain,
( eqangle(sK23,sK22,sK25,sK23,sK23,sK22,sK25,sK23)
| ~ para(sK23,sK22,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_117324]) ).
tcf(c_129185,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK25,sK23)
| ~ cong(X0,sK23,X1,sK23)
| ~ cong(X0,sK25,X1,sK25) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_129186,plain,
( perp(sK21,sK21,sK25,sK23)
| ~ cong(sK21,sK23,sK21,sK23)
| ~ cong(sK21,sK25,sK21,sK25) ),
inference(instantiation,[status(thm)],[c_129185]) ).
tcf(c_130855,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,X2,X3,sK25,sK23,sK23,sK22)
| ~ eqangle(sK25,sK23,X4,X5,sK25,sK23,sK23,sK22)
| ~ eqangle(X0,X1,X2,X3,sK25,sK23,X4,X5) ),
inference(instantiation,[status(thm)],[c_117498]) ).
tcf(c_130856,plain,
( eqangle(sK21,sK21,sK21,sK21,sK25,sK23,sK23,sK22)
| ~ eqangle(sK21,sK21,sK21,sK21,sK25,sK23,sK21,sK21)
| ~ eqangle(sK25,sK23,sK21,sK21,sK25,sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_130855]) ).
tcf(c_132768,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK25,sK23,X2,X3)
| ~ para(X0,X1,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_132769,plain,
( eqangle(sK21,sK21,sK21,sK21,sK25,sK23,sK21,sK21)
| ~ para(sK21,sK21,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_132768]) ).
tcf(c_134199,plain,
! [X0: $i,X1: $i] :
( perp(X0,sK26,sK26,X1)
| ~ perp(X0,sK26,X1,sK26) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_134200,plain,
( perp(sK21,sK26,sK26,sK21)
| ~ perp(sK21,sK26,sK21,sK26) ),
inference(instantiation,[status(thm)],[c_134199]) ).
tcf(c_136517,plain,
( para(sK23,sK25,sK25,sK23)
| ~ para(sK25,sK23,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_119455]) ).
tcf(c_141220,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK22,X0,X1,sK23,sK26,X0,X1)
| ~ para(sK23,sK22,sK23,sK26) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_141221,plain,
( eqangle(sK23,sK22,sK21,sK21,sK23,sK26,sK21,sK21)
| ~ para(sK23,sK22,sK23,sK26) ),
inference(instantiation,[status(thm)],[c_141220]) ).
tcf(c_149005,plain,
! [X0: $i,X1: $i] :
( midp(X0,X1,sK26)
| ~ coll(X0,X1,sK26)
| ~ cong(X0,X1,X0,sK26) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_149006,plain,
( midp(sK21,sK21,sK26)
| ~ coll(sK21,sK21,sK26)
| ~ cong(sK21,sK21,sK21,sK26) ),
inference(instantiation,[status(thm)],[c_149005]) ).
tcf(c_152957,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( eqangle(X0,sK26,X3,X4,X1,X2,X5,X6)
| ~ eqangle(X0,sK26,X1,X2,X3,X4,X5,X6) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_152961,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X1,sK26,X1,X0,X2,sK26,X2,X0)
| ~ cyclic(sK26,X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_152963,plain,
( eqangle(sK21,sK26,sK21,sK21,sK21,sK26,sK21,sK21)
| ~ cyclic(sK26,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_152961]) ).
tcf(c_153963,plain,
! [X0: $i,X1: $i] :
( midp(sK23,sK20,sK24)
| ~ coll(sK23,sK20,sK24)
| ~ midp(X0,sK20,X1)
| ~ para(X0,sK23,X1,sK24) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_153964,plain,
( midp(sK23,sK20,sK24)
| ~ midp(sK21,sK20,sK21)
| ~ coll(sK23,sK20,sK24)
| ~ para(sK21,sK23,sK21,sK24) ),
inference(instantiation,[status(thm)],[c_153963]) ).
tcf(c_154059,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK22,sK23,sK26)
| ~ para(sK23,sK22,X0,X1)
| ~ para(X0,X1,sK23,sK26) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_154064,plain,
( para(sK23,sK22,sK23,sK26)
| ~ para(sK21,sK21,sK23,sK26)
| ~ para(sK23,sK22,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_154059]) ).
tcf(c_158617,plain,
( para(sK23,sK25,sK23,sK25)
| ~ para(sK23,sK25,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_119715]) ).
tcf(c_163099,plain,
! [X0: $i] :
( midp(X0,sK25,sK25)
| ~ midp(X0,sK23,sK23)
| ~ para(sK23,sK25,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_120093]) ).
tcf(c_163100,plain,
( midp(sK21,sK25,sK25)
| ~ midp(sK21,sK23,sK23)
| ~ para(sK23,sK25,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_163099]) ).
tcf(c_176831,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,X2,sK23,sK26)
| ~ midp(X2,X1,sK26)
| ~ midp(X0,X1,sK23) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_176832,plain,
( para(sK21,sK21,sK23,sK26)
| ~ midp(sK21,sK21,sK26)
| ~ midp(sK21,sK21,sK23) ),
inference(instantiation,[status(thm)],[c_176831]) ).
tcf(c_177935,plain,
! [X0: $i,X1: $i] :
( cong(X0,X1,X0,sK26)
| ~ cong(X0,X1,sK26,X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_177936,plain,
( cong(sK21,sK21,sK21,sK26)
| ~ cong(sK21,sK21,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_177935]) ).
tcf(c_178411,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(X1,sK26,X0,X2)
| ~ coll(X0,X2,sK26)
| ~ eqangle(X0,X1,X0,sK26,X2,X1,X2,sK26) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_178412,plain,
( cyclic(sK21,sK26,sK21,sK21)
| ~ coll(sK21,sK21,sK26)
| ~ eqangle(sK21,sK21,sK21,sK26,sK21,sK21,sK21,sK26) ),
inference(instantiation,[status(thm)],[c_178411]) ).
tcf(c_178579,plain,
! [X0: $i,X1: $i,X2: $i] :
( cyclic(sK26,X0,X1,X2)
| ~ cyclic(X0,sK26,X1,X2) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_178580,plain,
( cyclic(sK26,sK21,sK21,sK21)
| ~ cyclic(sK21,sK26,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_178579]) ).
tcf(c_192982,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X0,sK26,X1,sK26)
| ~ perp(X2,X3,X4,X5)
| ~ eqangle(X0,sK26,X1,sK26,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_192985,plain,
( perp(sK21,sK26,sK21,sK26)
| ~ perp(sK21,sK21,sK21,sK21)
| ~ eqangle(sK21,sK26,sK21,sK26,sK21,sK21,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_192982]) ).
tcf(c_197586,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X2,sK26,X2)
| ~ midp(X2,X0,X1)
| ~ perp(X0,sK26,sK26,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_197587,plain,
( cong(sK21,sK21,sK26,sK21)
| ~ midp(sK21,sK21,sK21)
| ~ perp(sK21,sK26,sK26,sK21) ),
inference(instantiation,[status(thm)],[c_197586]) ).
tcf(c_200064,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(X0,sK26,X2,sK26,X0,X1,X2,X1)
| ~ eqangle(X0,sK26,X0,X1,X2,sK26,X2,X1) ),
inference(instantiation,[status(thm)],[c_152957]) ).
tcf(c_200067,plain,
( eqangle(sK21,sK26,sK21,sK26,sK21,sK21,sK21,sK21)
| ~ eqangle(sK21,sK26,sK21,sK21,sK21,sK26,sK21,sK21) ),
inference(instantiation,[status(thm)],[c_200064]) ).
tcf(c_229339,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK25,X0,X1)
| ~ midp(X0,sK25,X1) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_238127,plain,
! [X0: $i] :
( cong(X0,sK25,X0,sK25)
| ~ midp(X0,sK25,sK25) ),
inference(instantiation,[status(thm)],[c_229339]) ).
tcf(c_238137,plain,
( cong(sK21,sK25,sK21,sK25)
| ~ midp(sK21,sK25,sK25) ),
inference(instantiation,[status(thm)],[c_238127]) ).
tcf(c_238138,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_238137,c_200067,c_197587,c_192985,c_178580,c_178412,c_177936,c_176832,c_163100,c_158617,c_154064,c_153964,c_152963,c_149006,c_141221,c_136517,c_134200,c_132769,c_130856,c_129186,c_128986,c_124916,c_122294,c_121125,c_121124,c_120783,c_119460,c_117326,c_117325,c_99176,c_96146,c_86732,c_78596,c_67214,c_61207,c_57836,c_51353,c_50315,c_46229,c_44645,c_44335,c_37867,c_37008,c_36813,c_34729,c_30458,c_26763,c_26762,c_24496,c_20121,c_20120,c_17169,c_16813,c_13413,c_13299,c_13230,c_12077,c_11692,c_11337,c_11264,c_10399,c_10294,c_10289,c_9183,c_9156,c_9112,c_8683,c_8586,c_8511,c_8362,c_8356,c_8348,c_8038,c_8032,c_7738,c_7262,c_6859,c_236,c_187,c_182,c_178,c_162,c_166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO615+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.41 % Computer : n004.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Wed Sep 23 12:33:51 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.21/0.48 Running first-order theorem proving
% 0.21/0.48 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.21/0.50
% 0.21/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.21/0.50
% 0.21/0.50 % Detected problem language: tptp
% 0.21/0.52 % Proving...
% 91.16/22.96 % SZS status Started for theBenchmark.p
% 91.16/22.96 % SZS status Theorem for theBenchmark.p
% 91.16/22.96
% 91.16/22.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 91.16/22.96
% 91.16/22.96 % ------ iProver source info
% 91.16/22.96
% 91.16/22.96 % git: date: 2026-07-19 20:42:38 +0200
% 91.16/22.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 91.16/22.96 % git: non_committed_changes: false
% 91.16/22.96
% 91.16/22.96 % ------ Parsing...
% 91.16/22.96 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 91.16/22.96
% 91.16/22.96 % ------ 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 %
% 91.16/22.96
% 91.16/22.96 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 91.16/22.96
% 91.16/22.96 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 91.16/22.96 % ------ Proving...
% 91.16/22.96 % ------ Problem Properties
% 91.16/22.96
% 91.16/22.96 %
% 91.16/22.96 % clauses 123
% 91.16/22.96 % conjectures 11
% 91.16/22.96 % EPR 86
% 91.16/22.96 % Horn 113
% 91.16/22.96 % unary 11
% 91.16/22.96 % binary 37
% 91.16/22.96 % lits 339
% 91.16/22.96 % lits eq 4
% 91.16/22.96 % fd_pure 0
% 91.16/22.96 % fd_pseudo 0
% 91.16/22.96 % fd_cond 0
% 91.16/22.96 % fd_pseudo_cond 4
% 91.16/22.96 % AC symbols 0
% 91.16/22.96
% 91.16/22.96 % ------ Schedule dynamic 5 is on
% 91.16/22.96
% 91.16/22.96 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 91.16/22.96
% 91.16/22.96
% 91.16/22.96 % ------
% 91.16/22.96 % Current options:
% 91.16/22.96 % ------
% 91.16/22.96
% 91.16/22.96
% 91.16/22.96 %
% 91.16/22.96
% 91.16/22.96 % ------ Proving...
% 91.16/22.96 % Proof_search_loop: time out after: 5920 full_loop iterations
% 91.16/22.96
% 91.16/22.96 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 91.16/22.96
% 91.16/22.96
% 91.16/22.96 % ------
% 91.16/22.96 % Current options:
% 91.16/22.96 % ------
% 91.16/22.96
% 91.16/22.96
% 91.16/22.96 %
% 91.16/22.96
% 91.16/22.96 % ------ Proving...
% 91.16/22.96 %
% 91.16/22.96
% 91.16/22.96 % SZS status Theorem for theBenchmark.p
% 91.16/22.96
% 91.16/22.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 91.16/22.98
% 91.16/22.98
%------------------------------------------------------------------------------