%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO564+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 : n020.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:29 PM UTC 2026
% Result : Theorem 198.13s 27.54s
% Output : CNFRefutation 198.13s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f430ERROR: Could not build tree for root c_399672ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
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(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(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(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(f51,axiom,
! [X0,X1,X2,X3,X4] :
( ( midp(X4,X1,X2)
& circle(X3,X0,X1,X2) )
=> eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD50) ).
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(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ( perp(X3,X0,X19,X7)
& midp(X19,X3,X0)
& perp(X2,X0,X18,X7)
& midp(X18,X2,X0)
& perp(X2,X3,X17,X7)
& midp(X17,X2,X3)
& perp(X3,X2,X16,X6)
& midp(X16,X3,X2)
& perp(X1,X2,X15,X6)
& midp(X15,X1,X2)
& perp(X1,X3,X14,X6)
& midp(X14,X1,X3)
& perp(X3,X1,X13,X5)
& midp(X13,X3,X1)
& perp(X0,X1,X12,X5)
& midp(X12,X0,X1)
& perp(X0,X3,X11,X5)
& midp(X11,X0,X3)
& perp(X1,X2,X10,X4)
& midp(X10,X1,X2)
& perp(X0,X2,X9,X4)
& midp(X9,X0,X2)
& perp(X0,X1,X8,X4)
& midp(X8,X0,X1)
& perp(X1,X2,X0,X3)
& perp(X0,X2,X1,X3)
& perp(X0,X1,X2,X3) )
=> ( eqangle(X0,X1,X1,X2,X6,X7,X7,X5)
& ( eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
| eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
& ( eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
| eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
& ( eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
| eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
& ( eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
| eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
& ( eqangle(X1,X0,X0,X2,X7,X6,X6,X5)
| eqangle(X0,X1,X1,X2,X6,X7,X7,X5) )
& eqangle(X1,X0,X0,X2,X7,X6,X6,X5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL214026) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ( perp(X3,X0,X19,X7)
& midp(X19,X3,X0)
& perp(X2,X0,X18,X7)
& midp(X18,X2,X0)
& perp(X2,X3,X17,X7)
& midp(X17,X2,X3)
& perp(X3,X2,X16,X6)
& midp(X16,X3,X2)
& perp(X1,X2,X15,X6)
& midp(X15,X1,X2)
& perp(X1,X3,X14,X6)
& midp(X14,X1,X3)
& perp(X3,X1,X13,X5)
& midp(X13,X3,X1)
& perp(X0,X1,X12,X5)
& midp(X12,X0,X1)
& perp(X0,X3,X11,X5)
& midp(X11,X0,X3)
& perp(X1,X2,X10,X4)
& midp(X10,X1,X2)
& perp(X0,X2,X9,X4)
& midp(X9,X0,X2)
& perp(X0,X1,X8,X4)
& midp(X8,X0,X1)
& perp(X1,X2,X0,X3)
& perp(X0,X2,X1,X3)
& perp(X0,X1,X2,X3) )
=> ( eqangle(X0,X1,X1,X2,X6,X7,X7,X5)
& ( eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
| eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
& ( eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
| eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
& ( eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
| eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
& ( eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
| eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
& ( eqangle(X1,X0,X0,X2,X7,X6,X6,X5)
| eqangle(X0,X1,X1,X2,X6,X7,X7,X5) )
& eqangle(X1,X0,X0,X2,X7,X6,X6,X5) ) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f6]) ).
fof(f105,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f9]) ).
fof(f109,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(ennf_transformation,[],[f10]) ).
fof(f111,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(flattening,[],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(flattening,[],[f113]) ).
fof(f122,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f18]) ).
fof(f123,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(ennf_transformation,[],[f19]) ).
fof(f124,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(f125,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(ennf_transformation,[],[f21]) ).
fof(f126,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(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(flattening,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f39]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f40]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f154,plain,
! [X0,X1,X2,X3] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f156,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(ennf_transformation,[],[f46]) ).
fof(f160,plain,
! [X0,X1,X2,X3,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(flattening,[],[f159]) ).
fof(f168,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(ennf_transformation,[],[f51]) ).
fof(f169,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(flattening,[],[f168]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(ennf_transformation,[],[f53]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(flattening,[],[f172]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(ennf_transformation,[],[f54]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(flattening,[],[f174]) ).
fof(f178,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(ennf_transformation,[],[f56]) ).
fof(f179,plain,
! [X0,X1,X2,X3] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(flattening,[],[f178]) ).
fof(f180,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f57]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(flattening,[],[f180]) ).
fof(f191,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(ennf_transformation,[],[f64]) ).
fof(f192,plain,
! [X0,X1,X2,X3,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(flattening,[],[f191]) ).
fof(f193,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(ennf_transformation,[],[f65]) ).
fof(f194,plain,
! [X0,X1,X2,X3,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(flattening,[],[f193]) ).
fof(f197,plain,
! [X0,X1,X2] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f198,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(ennf_transformation,[],[f68]) ).
fof(f199,plain,
! [X0,X1,X2] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(flattening,[],[f198]) ).
fof(f200,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f69]) ).
fof(f201,plain,
! [X0,X1,X2] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f208,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(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(flattening,[],[f208]) ).
fof(f210,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(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(flattening,[],[f210]) ).
fof(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( perp(X3,X0,X19,X7)
& midp(X19,X3,X0)
& perp(X2,X0,X18,X7)
& midp(X18,X2,X0)
& perp(X2,X3,X17,X7)
& midp(X17,X2,X3)
& perp(X3,X2,X16,X6)
& midp(X16,X3,X2)
& perp(X1,X2,X15,X6)
& midp(X15,X1,X2)
& perp(X1,X3,X14,X6)
& midp(X14,X1,X3)
& perp(X3,X1,X13,X5)
& midp(X13,X3,X1)
& perp(X0,X1,X12,X5)
& midp(X12,X0,X1)
& perp(X0,X3,X11,X5)
& midp(X11,X0,X3)
& perp(X1,X2,X10,X4)
& midp(X10,X1,X2)
& perp(X0,X2,X9,X4)
& midp(X9,X0,X2)
& perp(X0,X1,X8,X4)
& midp(X8,X0,X1)
& perp(X1,X2,X0,X3)
& perp(X0,X2,X1,X3)
& perp(X0,X1,X2,X3)
& ( ~ eqangle(X0,X1,X1,X2,X6,X7,X7,X5)
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
| ( ~ eqangle(X1,X0,X0,X2,X7,X6,X6,X5)
& ~ eqangle(X0,X1,X1,X2,X6,X7,X7,X5) )
| ~ eqangle(X1,X0,X0,X2,X7,X6,X6,X5) ) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( perp(X3,X0,X19,X7)
& midp(X19,X3,X0)
& perp(X2,X0,X18,X7)
& midp(X18,X2,X0)
& perp(X2,X3,X17,X7)
& midp(X17,X2,X3)
& perp(X3,X2,X16,X6)
& midp(X16,X3,X2)
& perp(X1,X2,X15,X6)
& midp(X15,X1,X2)
& perp(X1,X3,X14,X6)
& midp(X14,X1,X3)
& perp(X3,X1,X13,X5)
& midp(X13,X3,X1)
& perp(X0,X1,X12,X5)
& midp(X12,X0,X1)
& perp(X0,X3,X11,X5)
& midp(X11,X0,X3)
& perp(X1,X2,X10,X4)
& midp(X10,X1,X2)
& perp(X0,X2,X9,X4)
& midp(X9,X0,X2)
& perp(X0,X1,X8,X4)
& midp(X8,X0,X1)
& perp(X1,X2,X0,X3)
& perp(X0,X2,X1,X3)
& perp(X0,X1,X2,X3)
& ( ~ eqangle(X0,X1,X1,X2,X6,X7,X7,X5)
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
| ( ~ eqangle(X1,X0,X0,X2,X7,X6,X6,X5)
& ~ eqangle(X0,X1,X1,X2,X6,X7,X7,X5) )
| ~ eqangle(X1,X0,X0,X2,X7,X6,X6,X5) ) ),
inference(flattening,[],[f249]) ).
fof(f273,plain,
! [X7,X5,X6,X2,X1,X0] :
( ~ sP1(X7,X5,X6,X2,X1,X0)
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) ) ),
inference(nnf_transformation,[],[f252]) ).
fof(f274,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sP1(X0,X1,X2,X3,X4,X5)
| ( ~ eqangle(X4,X5,X5,X3,X2,X1,X1,X0)
& ~ eqangle(X5,X4,X4,X3,X2,X1,X1,X0) ) ),
inference(rectify,[],[f273]) ).
fof(f277,plain,
( perp(sK25,sK22,sK41,sK29)
& midp(sK41,sK25,sK22)
& perp(sK24,sK22,sK40,sK29)
& midp(sK40,sK24,sK22)
& perp(sK24,sK25,sK39,sK29)
& midp(sK39,sK24,sK25)
& perp(sK25,sK24,sK38,sK28)
& midp(sK38,sK25,sK24)
& perp(sK23,sK24,sK37,sK28)
& midp(sK37,sK23,sK24)
& perp(sK23,sK25,sK36,sK28)
& midp(sK36,sK23,sK25)
& perp(sK25,sK23,sK35,sK27)
& midp(sK35,sK25,sK23)
& perp(sK22,sK23,sK34,sK27)
& midp(sK34,sK22,sK23)
& perp(sK22,sK25,sK33,sK27)
& midp(sK33,sK22,sK25)
& perp(sK23,sK24,sK32,sK26)
& midp(sK32,sK23,sK24)
& perp(sK22,sK24,sK31,sK26)
& midp(sK31,sK22,sK24)
& perp(sK22,sK23,sK30,sK26)
& midp(sK30,sK22,sK23)
& perp(sK23,sK24,sK22,sK25)
& perp(sK22,sK24,sK23,sK25)
& perp(sK22,sK23,sK24,sK25)
& ( ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| sP0(sK27,sK28,sK29,sK24,sK23,sK22)
| sP1(sK29,sK27,sK28,sK24,sK23,sK22)
| ( ~ eqangle(sK23,sK22,sK22,sK24,sK28,sK29,sK29,sK27)
& ~ eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK28,sK27) )
| ( ~ eqangle(sK23,sK22,sK22,sK24,sK28,sK29,sK29,sK27)
& ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29) )
| ( ~ eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27)
& ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27) )
| ~ eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24),skolemize(X3,sK25),skolemize(X4,sK26),skolemize(X5,sK27),skolemize(X6,sK28),skolemize(X7,sK29),skolemize(X8,sK30),skolemize(X9,sK31),skolemize(X10,sK32),skolemize(X11,sK33),skolemize(X12,sK34),skolemize(X13,sK35),skolemize(X14,sK36),skolemize(X15,sK37),skolemize(X16,sK38),skolemize(X17,sK39),skolemize(X18,sK40),skolemize(X19,sK41)],[f253]) ).
fof(f279,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f280,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f281,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f282,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f283,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f105]) ).
fof(f284,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f106]) ).
fof(f285,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f286,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3)
| perp(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f111]) ).
fof(f288,plain,
! [X2,X0,X1] :
( ~ midp(X2,X1,X0)
| midp(X2,X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f289,plain,
! [X2,X3,X0,X1] :
( ~ cong(X3,X0,X3,X2)
| ~ cong(X3,X0,X3,X1)
| circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f122]) ).
fof(f296,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(cnf_transformation,[],[f123]) ).
fof(f297,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,[],[f124]) ).
fof(f298,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(cnf_transformation,[],[f125]) ).
fof(f299,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,[],[f127]) ).
fof(f300,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f301,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X1,X2,X3)
| cong(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
fof(f316,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f148]) ).
fof(f317,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X0,X1,X2,X3)
| eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f149]) ).
fof(f320,plain,
! [X2,X3,X0,X1] :
( ~ coll(X2,X3,X1)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f321,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f156]) ).
fof(f322,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1)
| para(X3,X4,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f323,plain,
! [X2,X3,X0,X1,X4] :
( ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1)
| midp(X4,X0,X2) ),
inference(cnf_transformation,[],[f160]) ).
fof(f328,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X1,X2)
| ~ circle(X3,X0,X1,X2)
| eqangle(X0,X1,X0,X2,X3,X1,X3,X4) ),
inference(cnf_transformation,[],[f169]) ).
fof(f330,plain,
! [X2,X3,X0,X1] :
( ~ midp(X3,X0,X2)
| ~ perp(X0,X1,X1,X2)
| cong(X0,X3,X1,X3) ),
inference(cnf_transformation,[],[f173]) ).
fof(f331,plain,
! [X2,X3,X0,X1] :
( ~ coll(X3,X0,X2)
| ~ circle(X3,X0,X1,X2)
| perp(X0,X1,X1,X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f333,plain,
! [X2,X3,X0,X1] :
( ~ perp(X3,X2,X0,X1)
| ~ midp(X2,X0,X1)
| cong(X3,X0,X3,X1) ),
inference(cnf_transformation,[],[f179]) ).
fof(f334,plain,
! [X2,X3,X0,X1] :
( ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f181]) ).
fof(f341,plain,
! [X2,X3,X0,X1,X4] :
( ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1)
| para(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f192]) ).
fof(f342,plain,
! [X2,X3,X0,X1,X4] :
( ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1)
| midp(X4,X2,X3) ),
inference(cnf_transformation,[],[f194]) ).
fof(f344,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f197]) ).
fof(f345,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2)
| midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f199]) ).
fof(f346,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f200]) ).
fof(f347,plain,
! [X2,X0,X1] :
( ~ midp(X0,X1,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f201]) ).
fof(f351,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,[],[f209]) ).
fof(f352,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,[],[f211]) ).
fof(f392,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP1(X0,X1,X2,X3,X4,X5)
| ~ eqangle(X5,X4,X4,X3,X2,X1,X1,X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f396,plain,
midp(sK41,sK25,sK22),
inference(cnf_transformation,[],[f277]) ).
fof(f398,plain,
midp(sK40,sK24,sK22),
inference(cnf_transformation,[],[f277]) ).
fof(f399,plain,
perp(sK24,sK25,sK39,sK29),
inference(cnf_transformation,[],[f277]) ).
fof(f400,plain,
midp(sK39,sK24,sK25),
inference(cnf_transformation,[],[f277]) ).
fof(f401,plain,
perp(sK25,sK24,sK38,sK28),
inference(cnf_transformation,[],[f277]) ).
fof(f404,plain,
midp(sK37,sK23,sK24),
inference(cnf_transformation,[],[f277]) ).
fof(f405,plain,
perp(sK23,sK25,sK36,sK28),
inference(cnf_transformation,[],[f277]) ).
fof(f406,plain,
midp(sK36,sK23,sK25),
inference(cnf_transformation,[],[f277]) ).
fof(f407,plain,
perp(sK25,sK23,sK35,sK27),
inference(cnf_transformation,[],[f277]) ).
fof(f408,plain,
midp(sK35,sK25,sK23),
inference(cnf_transformation,[],[f277]) ).
fof(f412,plain,
midp(sK33,sK22,sK25),
inference(cnf_transformation,[],[f277]) ).
fof(f414,plain,
midp(sK32,sK23,sK24),
inference(cnf_transformation,[],[f277]) ).
fof(f416,plain,
midp(sK31,sK22,sK24),
inference(cnf_transformation,[],[f277]) ).
fof(f417,plain,
perp(sK22,sK23,sK30,sK26),
inference(cnf_transformation,[],[f277]) ).
fof(f418,plain,
midp(sK30,sK22,sK23),
inference(cnf_transformation,[],[f277]) ).
fof(f419,plain,
perp(sK23,sK24,sK22,sK25),
inference(cnf_transformation,[],[f277]) ).
fof(f420,plain,
perp(sK22,sK24,sK23,sK25),
inference(cnf_transformation,[],[f277]) ).
fof(f421,plain,
perp(sK22,sK23,sK24,sK25),
inference(cnf_transformation,[],[f277]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f279]) ).
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,[],[f280]) ).
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,[],[f281]) ).
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,[],[f282]) ).
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,[],[f283]) ).
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,[],[f284]) ).
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,[],[f285]) ).
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,[],[f286]) ).
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,[],[f287]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f288]) ).
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,[],[f289]) ).
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,[],[f295]) ).
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,[],[f296]) ).
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,[],[f297]) ).
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,[],[f298]) ).
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,[],[f299]) ).
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,[],[f300]) ).
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,[],[f301]) ).
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,[],[f316]) ).
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,[],[f317]) ).
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,[],[f320]) ).
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,[],[f321]) ).
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,[],[f322]) ).
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,[],[f323]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X1,X2,X1,X3,X0,X2,X0,X4)
| ~ midp(X4,X2,X3)
| ~ circle(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f328]) ).
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,[],[f330]) ).
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,[],[f331]) ).
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,[],[f333]) ).
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,[],[f334]) ).
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,[],[f341]) ).
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,[],[f342]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[],[f344]) ).
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,[],[f345]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i] :
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[],[f347]) ).
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,[],[f351]) ).
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,[],[f352]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ sP1(X5,X4,X3,X2,X1,X0)
| ~ eqangle(X0,X1,X1,X2,X3,X4,X4,X5) ),
inference(cnf_transformation,[],[f392]) ).
tcf(c_166,negated_conjecture,
( sP0(sK27,sK28,sK29,sK24,sK23,sK22)
| sP1(sK29,sK27,sK28,sK24,sK23,sK22)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK28,sK27)
| ~ eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_174,negated_conjecture,
perp(sK22,sK23,sK24,sK25),
inference(cnf_transformation,[],[f421]) ).
tcf(c_175,negated_conjecture,
perp(sK22,sK24,sK23,sK25),
inference(cnf_transformation,[],[f420]) ).
tcf(c_176,negated_conjecture,
perp(sK23,sK24,sK22,sK25),
inference(cnf_transformation,[],[f419]) ).
tcf(c_177,negated_conjecture,
midp(sK30,sK22,sK23),
inference(cnf_transformation,[],[f418]) ).
tcf(c_178,negated_conjecture,
perp(sK22,sK23,sK30,sK26),
inference(cnf_transformation,[],[f417]) ).
tcf(c_179,negated_conjecture,
midp(sK31,sK22,sK24),
inference(cnf_transformation,[],[f416]) ).
tcf(c_181,negated_conjecture,
midp(sK32,sK23,sK24),
inference(cnf_transformation,[],[f414]) ).
tcf(c_183,negated_conjecture,
midp(sK33,sK22,sK25),
inference(cnf_transformation,[],[f412]) ).
tcf(c_187,negated_conjecture,
midp(sK35,sK25,sK23),
inference(cnf_transformation,[],[f408]) ).
tcf(c_188,negated_conjecture,
perp(sK25,sK23,sK35,sK27),
inference(cnf_transformation,[],[f407]) ).
tcf(c_189,negated_conjecture,
midp(sK36,sK23,sK25),
inference(cnf_transformation,[],[f406]) ).
tcf(c_190,negated_conjecture,
perp(sK23,sK25,sK36,sK28),
inference(cnf_transformation,[],[f405]) ).
tcf(c_191,negated_conjecture,
midp(sK37,sK23,sK24),
inference(cnf_transformation,[],[f404]) ).
tcf(c_194,negated_conjecture,
perp(sK25,sK24,sK38,sK28),
inference(cnf_transformation,[],[f401]) ).
tcf(c_195,negated_conjecture,
midp(sK39,sK24,sK25),
inference(cnf_transformation,[],[f400]) ).
tcf(c_196,negated_conjecture,
perp(sK24,sK25,sK39,sK29),
inference(cnf_transformation,[],[f399]) ).
tcf(c_197,negated_conjecture,
midp(sK40,sK24,sK22),
inference(cnf_transformation,[],[f398]) ).
tcf(c_199,negated_conjecture,
midp(sK41,sK25,sK22),
inference(cnf_transformation,[],[f396]) ).
tcf(c_206,plain,
( midp(sK23,sK23,sK23)
| ~ coll(sK23,sK23,sK23)
| ~ cong(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_215,plain,
( perp(sK23,sK23,sK23,sK23)
| ~ cong(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_449,plain,
( sP0(sK27,sK28,sK29,sK24,sK23,sK22)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK28,sK27)
| ~ eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27) ),
inference(backward_subsumption_resolution,[status(thm)],[c_166,c_162]) ).
tcf(c_4556,negated_conjecture,
midp(sK41,sK25,sK22),
inference(demodulation,[status(thm)],[c_199]) ).
tcf(c_4558,negated_conjecture,
midp(sK40,sK24,sK22),
inference(demodulation,[status(thm)],[c_197]) ).
tcf(c_4559,negated_conjecture,
perp(sK24,sK25,sK39,sK29),
inference(demodulation,[status(thm)],[c_196]) ).
tcf(c_4560,negated_conjecture,
midp(sK39,sK24,sK25),
inference(demodulation,[status(thm)],[c_195]) ).
tcf(c_4561,negated_conjecture,
perp(sK25,sK24,sK38,sK28),
inference(demodulation,[status(thm)],[c_194]) ).
tcf(c_4564,negated_conjecture,
midp(sK37,sK23,sK24),
inference(demodulation,[status(thm)],[c_191]) ).
tcf(c_4565,negated_conjecture,
perp(sK23,sK25,sK36,sK28),
inference(demodulation,[status(thm)],[c_190]) ).
tcf(c_4566,negated_conjecture,
midp(sK36,sK23,sK25),
inference(demodulation,[status(thm)],[c_189]) ).
tcf(c_4567,negated_conjecture,
perp(sK25,sK23,sK35,sK27),
inference(demodulation,[status(thm)],[c_188]) ).
tcf(c_4568,negated_conjecture,
midp(sK35,sK25,sK23),
inference(demodulation,[status(thm)],[c_187]) ).
tcf(c_4572,negated_conjecture,
midp(sK33,sK22,sK25),
inference(demodulation,[status(thm)],[c_183]) ).
tcf(c_4574,negated_conjecture,
midp(sK32,sK23,sK24),
inference(demodulation,[status(thm)],[c_181]) ).
tcf(c_4576,negated_conjecture,
midp(sK31,sK22,sK24),
inference(demodulation,[status(thm)],[c_179]) ).
tcf(c_4577,negated_conjecture,
perp(sK22,sK23,sK30,sK26),
inference(demodulation,[status(thm)],[c_178]) ).
tcf(c_4578,negated_conjecture,
midp(sK30,sK22,sK23),
inference(demodulation,[status(thm)],[c_177]) ).
tcf(c_4579,negated_conjecture,
perp(sK23,sK24,sK22,sK25),
inference(demodulation,[status(thm)],[c_176]) ).
tcf(c_4580,negated_conjecture,
perp(sK22,sK24,sK23,sK25),
inference(demodulation,[status(thm)],[c_175]) ).
tcf(c_4581,negated_conjecture,
perp(sK22,sK23,sK24,sK25),
inference(demodulation,[status(thm)],[c_174]) ).
tcf(c_6243,plain,
midp(sK32,sK24,sK23),
inference(superposition,[status(thm)],[c_4574,c_59]) ).
tcf(c_6246,plain,
midp(sK35,sK23,sK25),
inference(superposition,[status(thm)],[c_4568,c_59]) ).
tcf(c_6247,plain,
midp(sK36,sK25,sK23),
inference(superposition,[status(thm)],[c_4566,c_59]) ).
tcf(c_6248,plain,
midp(sK37,sK24,sK23),
inference(superposition,[status(thm)],[c_4564,c_59]) ).
tcf(c_6250,plain,
midp(sK39,sK25,sK24),
inference(superposition,[status(thm)],[c_4560,c_59]) ).
tcf(c_6251,plain,
midp(sK40,sK22,sK24),
inference(superposition,[status(thm)],[c_4558,c_59]) ).
tcf(c_6252,plain,
midp(sK41,sK22,sK25),
inference(superposition,[status(thm)],[c_4556,c_59]) ).
tcf(c_6268,plain,
coll(sK30,sK22,sK23),
inference(superposition,[status(thm)],[c_4578,c_118]) ).
tcf(c_6273,plain,
coll(sK35,sK25,sK23),
inference(superposition,[status(thm)],[c_4568,c_118]) ).
tcf(c_6282,plain,
coll(sK32,sK24,sK23),
inference(superposition,[status(thm)],[c_6243,c_118]) ).
tcf(c_6305,plain,
coll(sK22,sK30,sK23),
inference(superposition,[status(thm)],[c_6268,c_50]) ).
tcf(c_6315,plain,
coll(sK25,sK35,sK23),
inference(superposition,[status(thm)],[c_6273,c_50]) ).
tcf(c_6341,plain,
perp(sK22,sK23,sK25,sK24),
inference(superposition,[status(thm)],[c_4581,c_55]) ).
tcf(c_6342,plain,
perp(sK22,sK24,sK25,sK23),
inference(superposition,[status(thm)],[c_4580,c_55]) ).
tcf(c_6360,plain,
perp(sK24,sK25,sK22,sK23),
inference(superposition,[status(thm)],[c_4581,c_56]) ).
tcf(c_6362,plain,
perp(sK22,sK25,sK23,sK24),
inference(superposition,[status(thm)],[c_4579,c_56]) ).
tcf(c_6363,plain,
perp(sK30,sK26,sK22,sK23),
inference(superposition,[status(thm)],[c_4577,c_56]) ).
tcf(c_6369,plain,
perp(sK36,sK28,sK23,sK25),
inference(superposition,[status(thm)],[c_4565,c_56]) ).
tcf(c_6371,plain,
perp(sK38,sK28,sK25,sK24),
inference(superposition,[status(thm)],[c_4561,c_56]) ).
tcf(c_6372,plain,
perp(sK39,sK29,sK24,sK25),
inference(superposition,[status(thm)],[c_4559,c_56]) ).
tcf(c_6385,plain,
coll(sK24,sK32,sK23),
inference(superposition,[status(thm)],[c_6282,c_50]) ).
tcf(c_6387,plain,
perp(sK25,sK24,sK22,sK23),
inference(superposition,[status(thm)],[c_6341,c_56]) ).
tcf(c_6389,plain,
perp(sK25,sK23,sK22,sK24),
inference(superposition,[status(thm)],[c_6342,c_56]) ).
tcf(c_6448,plain,
perp(sK24,sK25,sK23,sK22),
inference(superposition,[status(thm)],[c_6360,c_55]) ).
tcf(c_6452,plain,
perp(sK22,sK25,sK24,sK23),
inference(superposition,[status(thm)],[c_6362,c_55]) ).
tcf(c_6596,plain,
perp(sK36,sK28,sK25,sK23),
inference(superposition,[status(thm)],[c_6369,c_55]) ).
tcf(c_6612,plain,
perp(sK38,sK28,sK24,sK25),
inference(superposition,[status(thm)],[c_6371,c_55]) ).
tcf(c_6635,plain,
! [X0: $i] :
( coll(sK23,X0,sK22)
| ~ coll(sK22,sK30,X0) ),
inference(superposition,[status(thm)],[c_6305,c_51]) ).
tcf(c_6640,plain,
( coll(sK23,sK23,sK22)
| ~ coll(sK22,sK30,sK23) ),
inference(instantiation,[status(thm)],[c_6635]) ).
tcf(c_6671,plain,
! [X0: $i] :
( coll(sK23,X0,sK25)
| ~ coll(sK25,sK35,X0) ),
inference(superposition,[status(thm)],[c_6315,c_51]) ).
tcf(c_6676,plain,
( coll(sK23,sK23,sK25)
| ~ coll(sK25,sK35,sK23) ),
inference(instantiation,[status(thm)],[c_6671]) ).
tcf(c_6677,plain,
( cong(sK30,sK22,sK30,sK23)
| ~ midp(sK30,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6682,plain,
( cong(sK35,sK25,sK35,sK23)
| ~ midp(sK35,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6683,plain,
( cong(sK36,sK23,sK36,sK25)
| ~ midp(sK36,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_6702,plain,
perp(sK25,sK24,sK23,sK22),
inference(superposition,[status(thm)],[c_6387,c_55]) ).
tcf(c_6728,plain,
! [X0: $i,X1: $i] :
( para(sK32,X0,sK24,X1)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_4574,c_93]) ).
tcf(c_6732,plain,
! [X0: $i,X1: $i] :
( para(sK36,X0,sK25,X1)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_4566,c_93]) ).
tcf(c_6735,plain,
! [X0: $i,X1: $i] :
( para(sK39,X0,sK25,X1)
| ~ midp(X0,sK24,X1) ),
inference(superposition,[status(thm)],[c_4560,c_93]) ).
tcf(c_6737,plain,
! [X0: $i,X1: $i] :
( para(sK41,X0,sK22,X1)
| ~ midp(X0,sK25,X1) ),
inference(superposition,[status(thm)],[c_4556,c_93]) ).
tcf(c_6903,plain,
! [X0: $i,X1: $i] :
( para(sK24,X1,sK32,X0)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6728,c_53]) ).
tcf(c_6904,plain,
! [X0: $i,X1: $i] :
( para(sK32,X0,X1,sK24)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6728,c_52]) ).
tcf(c_6950,plain,
! [X0: $i,X1: $i] :
( para(sK36,X0,X1,sK25)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_6732,c_52]) ).
tcf(c_6986,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK24,X1)
| ~ midp(sK31,X0,X1) ),
inference(superposition,[status(thm)],[c_4576,c_112]) ).
tcf(c_6987,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK24,X1)
| ~ midp(sK32,X0,X1) ),
inference(superposition,[status(thm)],[c_4574,c_112]) ).
tcf(c_6988,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,sK25,X1)
| ~ midp(sK33,X0,X1) ),
inference(superposition,[status(thm)],[c_4572,c_112]) ).
tcf(c_6992,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK24,X1)
| ~ midp(sK37,X0,X1) ),
inference(superposition,[status(thm)],[c_4564,c_112]) ).
tcf(c_6995,plain,
! [X0: $i,X1: $i] :
( para(sK24,X0,sK22,X1)
| ~ midp(sK40,X0,X1) ),
inference(superposition,[status(thm)],[c_4558,c_112]) ).
tcf(c_6996,plain,
! [X0: $i,X1: $i] :
( para(sK25,X0,sK22,X1)
| ~ midp(sK41,X0,X1) ),
inference(superposition,[status(thm)],[c_4556,c_112]) ).
tcf(c_7002,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK25,X1)
| ~ midp(sK35,X0,X1) ),
inference(superposition,[status(thm)],[c_6246,c_112]) ).
tcf(c_7063,plain,
( para(sK23,sK23,sK25,sK23)
| ~ midp(sK35,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7002]) ).
tcf(c_7078,plain,
( para(sK23,sK23,sK24,sK23)
| ~ midp(sK32,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_6987]) ).
tcf(c_7102,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK24,X1)
| ~ midp(sK32,sK23,sK24)
| ~ midp(sK32,X0,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_7106,plain,
! [X0: $i,X1: $i] :
( para(sK23,X0,sK25,X1)
| ~ midp(sK36,sK23,sK25)
| ~ midp(sK36,X0,X1) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_7135,plain,
! [X0: $i] :
( coll(sK23,X0,sK24)
| ~ coll(sK24,sK32,X0) ),
inference(superposition,[status(thm)],[c_6385,c_51]) ).
tcf(c_7140,plain,
( coll(sK23,sK23,sK24)
| ~ coll(sK24,sK32,sK23) ),
inference(instantiation,[status(thm)],[c_7135]) ).
tcf(c_7188,plain,
! [X0: $i,X1: $i] :
( para(sK41,X0,X1,sK22)
| ~ midp(X0,sK25,X1) ),
inference(superposition,[status(thm)],[c_6737,c_52]) ).
tcf(c_7234,plain,
! [X0: $i,X1: $i] :
( para(sK22,X0,X1,sK24)
| ~ midp(sK31,X0,X1) ),
inference(superposition,[status(thm)],[c_6986,c_52]) ).
tcf(c_7239,plain,
( para(sK22,sK23,sK23,sK24)
| ~ midp(sK31,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7234]) ).
tcf(c_7321,plain,
( cong(sK36,sK23,sK36,sK25)
| ~ midp(sK28,sK23,sK25) ),
inference(superposition,[status(thm)],[c_6369,c_104]) ).
tcf(c_7442,plain,
! [X0: $i] :
( cong(X0,sK23,X0,sK25)
| ~ midp(sK36,sK23,sK25)
| ~ perp(X0,sK36,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_7443,plain,
( cong(sK23,sK23,sK23,sK25)
| ~ midp(sK36,sK23,sK25)
| ~ perp(sK23,sK36,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_7442]) ).
tcf(c_7456,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK24,X0,X1)
| ~ perp(sK22,sK24,sK23,sK25)
| ~ perp(sK23,sK25,X0,X1) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_7460,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK23,X0,X1)
| ~ perp(sK22,sK23,sK30,sK26)
| ~ perp(sK30,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_7597,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK23,X0,X1)
| ~ perp(sK24,sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_4581,c_57]) ).
tcf(c_7598,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK24,X0,X1)
| ~ perp(sK23,sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_4580,c_57]) ).
tcf(c_7599,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK24,X0,X1)
| ~ perp(sK22,sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_4579,c_57]) ).
tcf(c_7606,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK25,X0,X1)
| ~ perp(sK36,sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_4565,c_57]) ).
tcf(c_7612,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK23,X0,X1)
| ~ perp(sK25,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_6341,c_57]) ).
tcf(c_7613,plain,
! [X0: $i,X1: $i] :
( para(sK22,sK24,X0,X1)
| ~ perp(sK25,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_6342,c_57]) ).
tcf(c_7630,plain,
! [X0: $i,X1: $i] :
( para(sK30,sK26,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_6363,c_57]) ).
tcf(c_7639,plain,
! [X0: $i,X1: $i] :
( para(sK39,sK29,X0,X1)
| ~ perp(sK24,sK25,X0,X1) ),
inference(superposition,[status(thm)],[c_6372,c_57]) ).
tcf(c_7642,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK24,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_6387,c_57]) ).
tcf(c_7643,plain,
! [X0: $i,X1: $i] :
( para(sK25,sK23,X0,X1)
| ~ perp(sK22,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_6389,c_57]) ).
tcf(c_7745,plain,
( para(sK25,sK23,sK23,sK23)
| ~ perp(sK22,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7643]) ).
tcf(c_7746,plain,
( para(sK25,sK24,sK23,sK23)
| ~ perp(sK22,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7642]) ).
tcf(c_7758,plain,
( para(sK30,sK26,sK23,sK23)
| ~ perp(sK22,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7630]) ).
tcf(c_7775,plain,
( para(sK22,sK24,sK23,sK23)
| ~ perp(sK25,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7613]) ).
tcf(c_7776,plain,
( para(sK22,sK23,sK23,sK23)
| ~ perp(sK25,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7612]) ).
tcf(c_7795,plain,
! [X0: $i,X1: $i] :
( midp(sK31,X0,X1)
| ~ midp(sK31,sK22,sK24)
| ~ para(sK22,X1,sK24,X0)
| ~ para(sK22,X0,sK24,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_7796,plain,
( midp(sK31,sK23,sK23)
| ~ midp(sK31,sK22,sK24)
| ~ para(sK22,sK23,sK24,sK23) ),
inference(instantiation,[status(thm)],[c_7795]) ).
tcf(c_7799,plain,
! [X0: $i,X1: $i] :
( midp(sK33,X0,X1)
| ~ midp(sK33,sK22,sK25)
| ~ para(sK22,X1,sK25,X0)
| ~ para(sK22,X0,sK25,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_7803,plain,
! [X0: $i,X1: $i] :
( midp(sK35,X0,X1)
| ~ midp(sK35,sK25,sK23)
| ~ para(sK25,X1,sK23,X0)
| ~ para(sK25,X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_7804,plain,
( midp(sK35,sK23,sK23)
| ~ midp(sK35,sK25,sK23)
| ~ para(sK25,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_7803]) ).
tcf(c_8059,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK32,X3,X1,X2)
| ~ midp(X3,sK23,X0)
| ~ perp(sK24,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6728,c_58]) ).
tcf(c_8066,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK39,X3,X1,X2)
| ~ midp(X3,sK24,X0)
| ~ perp(sK25,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6735,c_58]) ).
tcf(c_8072,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK23,X3,X1,X2)
| ~ midp(sK37,X3,X0)
| ~ perp(sK24,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6992,c_58]) ).
tcf(c_8074,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK22,X3,X1,X2)
| ~ midp(sK33,X3,X0)
| ~ perp(sK25,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6988,c_58]) ).
tcf(c_8079,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK24,X3,X1,X2)
| ~ midp(sK40,X3,X0)
| ~ perp(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6995,c_58]) ).
tcf(c_8080,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK25,X3,X1,X2)
| ~ midp(sK41,X3,X0)
| ~ perp(sK22,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6996,c_58]) ).
tcf(c_9012,plain,
para(sK22,sK23,sK39,sK29),
inference(superposition,[status(thm)],[c_4559,c_7597]) ).
tcf(c_9014,plain,
para(sK22,sK23,sK22,sK23),
inference(superposition,[status(thm)],[c_6360,c_7597]) ).
tcf(c_9019,plain,
para(sK39,sK29,sK22,sK23),
inference(superposition,[status(thm)],[c_9012,c_53]) ).
tcf(c_9035,plain,
para(sK22,sK24,sK36,sK28),
inference(superposition,[status(thm)],[c_4565,c_7598]) ).
tcf(c_9042,plain,
para(sK36,sK28,sK22,sK24),
inference(superposition,[status(thm)],[c_9035,c_53]) ).
tcf(c_9058,plain,
para(sK23,sK24,sK23,sK24),
inference(superposition,[status(thm)],[c_6362,c_7599]) ).
tcf(c_9370,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_9383,plain,
( cyclic(sK23,sK23,sK23,sK23)
| ~ coll(sK23,sK23,sK23)
| ~ para(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_9370]) ).
tcf(c_10231,plain,
! [X0: $i,X1: $i] :
( midp(sK32,X0,X1)
| ~ midp(sK32,sK24,sK23)
| ~ para(sK24,X1,sK23,X0)
| ~ para(sK24,X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_10232,plain,
( midp(sK32,sK23,sK23)
| ~ midp(sK32,sK24,sK23)
| ~ para(sK24,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_10231]) ).
tcf(c_10305,plain,
para(sK22,sK23,sK23,sK22),
inference(superposition,[status(thm)],[c_6448,c_7597]) ).
tcf(c_10376,plain,
para(sK23,sK24,sK24,sK23),
inference(superposition,[status(thm)],[c_6452,c_7599]) ).
tcf(c_10582,plain,
para(sK23,sK25,sK25,sK23),
inference(superposition,[status(thm)],[c_6596,c_7606]) ).
tcf(c_10606,plain,
perp(sK24,sK25,sK38,sK28),
inference(superposition,[status(thm)],[c_6612,c_56]) ).
tcf(c_10789,plain,
perp(sK23,sK22,sK25,sK24),
inference(superposition,[status(thm)],[c_6702,c_56]) ).
tcf(c_10817,plain,
! [X0: $i,X1: $i] :
( midp(sK36,X0,X1)
| ~ midp(sK36,sK25,sK23)
| ~ para(sK25,X1,sK23,X0)
| ~ para(sK25,X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_10818,plain,
( midp(sK36,sK23,sK23)
| ~ midp(sK36,sK25,sK23)
| ~ para(sK25,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_10817]) ).
tcf(c_11055,plain,
! [X0: $i,X1: $i] :
( midp(sK37,X0,X1)
| ~ midp(sK37,sK24,sK23)
| ~ para(sK24,X1,sK23,X0)
| ~ para(sK24,X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_11056,plain,
( midp(sK37,sK23,sK23)
| ~ midp(sK37,sK24,sK23)
| ~ para(sK24,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_11055]) ).
tcf(c_11211,plain,
coll(sK22,sK23,sK23),
inference(superposition,[status(thm)],[c_9014,c_115]) ).
tcf(c_11227,plain,
! [X0: $i,X1: $i] :
( perp(sK39,sK29,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_9019,c_58]) ).
tcf(c_11242,plain,
( perp(sK39,sK29,sK23,sK23)
| ~ perp(sK22,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_11227]) ).
tcf(c_11271,plain,
! [X0: $i,X1: $i] :
( midp(sK39,X0,X1)
| ~ midp(sK39,sK25,sK24)
| ~ para(sK25,X1,sK24,X0)
| ~ para(sK25,X0,sK24,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_11272,plain,
( midp(sK39,sK23,sK23)
| ~ midp(sK39,sK25,sK24)
| ~ para(sK25,sK23,sK24,sK23) ),
inference(instantiation,[status(thm)],[c_11271]) ).
tcf(c_11314,plain,
! [X0: $i,X1: $i] :
( perp(sK36,sK28,X0,X1)
| ~ perp(sK22,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_9042,c_58]) ).
tcf(c_11409,plain,
! [X0: $i,X1: $i] :
( midp(sK40,X0,X1)
| ~ midp(sK40,sK22,sK24)
| ~ para(sK22,X1,sK24,X0)
| ~ para(sK22,X0,sK24,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_11410,plain,
( midp(sK40,sK23,sK23)
| ~ midp(sK40,sK22,sK24)
| ~ para(sK22,sK23,sK24,sK23) ),
inference(instantiation,[status(thm)],[c_11409]) ).
tcf(c_11543,plain,
coll(sK23,sK22,sK23),
inference(superposition,[status(thm)],[c_11211,c_50]) ).
tcf(c_11558,plain,
! [X0: $i] :
( coll(sK23,X0,sK23)
| ~ coll(sK23,sK22,X0) ),
inference(superposition,[status(thm)],[c_11543,c_51]) ).
tcf(c_11563,plain,
( coll(sK23,sK23,sK23)
| ~ coll(sK23,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_11558]) ).
tcf(c_11585,plain,
! [X0: $i,X1: $i] :
( midp(sK41,X0,X1)
| ~ midp(sK41,sK22,sK25)
| ~ para(sK22,X1,sK25,X0)
| ~ para(sK22,X0,sK25,X1) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_11586,plain,
( midp(sK41,sK23,sK23)
| ~ midp(sK41,sK22,sK25)
| ~ para(sK22,sK23,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_11585]) ).
tcf(c_11782,plain,
! [X0: $i] :
( perp(sK22,X0,X0,sK23)
| ~ coll(sK30,sK22,sK23)
| ~ circle(sK30,sK22,X0,sK23) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_11783,plain,
( perp(sK22,sK23,sK23,sK23)
| ~ coll(sK30,sK22,sK23)
| ~ circle(sK30,sK22,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_11782]) ).
tcf(c_11828,plain,
! [X0: $i] :
( midp(X0,sK24,sK24)
| ~ midp(X0,sK23,sK23)
| ~ para(sK23,sK24,sK23,sK24) ),
inference(superposition,[status(thm)],[c_9058,c_113]) ).
tcf(c_11838,plain,
! [X0: $i] :
( midp(X0,sK24,sK24)
| ~ midp(X0,sK23,sK23) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11828,c_9058]) ).
tcf(c_11841,plain,
( midp(sK23,sK24,sK24)
| ~ midp(sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_11838]) ).
tcf(c_12427,plain,
! [X0: $i] :
( perp(sK32,X0,sK39,sK29)
| ~ midp(X0,sK23,sK25) ),
inference(superposition,[status(thm)],[c_4559,c_8059]) ).
tcf(c_12695,plain,
! [X0: $i] :
( perp(sK25,X0,X0,sK23)
| ~ coll(sK35,sK25,sK23)
| ~ circle(sK35,sK25,X0,sK23) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_12696,plain,
( perp(sK25,sK23,sK23,sK23)
| ~ coll(sK35,sK25,sK23)
| ~ circle(sK35,sK25,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_12695]) ).
tcf(c_13251,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK32,X2,X0,X1)
| ~ midp(X2,sK23,sK25)
| ~ perp(sK39,sK29,X0,X1) ),
inference(superposition,[status(thm)],[c_12427,c_57]) ).
tcf(c_13289,plain,
( para(sK32,sK23,sK23,sK23)
| ~ midp(sK23,sK23,sK25)
| ~ perp(sK39,sK29,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_13251]) ).
tcf(c_13685,plain,
! [X0: $i] :
( circle(sK30,sK22,X0,sK23)
| ~ cong(sK30,sK22,sK30,sK23)
| ~ cong(sK30,sK22,sK30,X0) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_13687,plain,
( circle(sK30,sK22,sK23,sK23)
| ~ cong(sK30,sK22,sK30,sK23) ),
inference(instantiation,[status(thm)],[c_13685]) ).
tcf(c_14250,plain,
! [X0: $i] :
( circle(sK35,sK25,X0,sK23)
| ~ cong(sK35,sK25,sK35,sK23)
| ~ cong(sK35,sK25,sK35,X0) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_14252,plain,
( circle(sK35,sK25,sK23,sK23)
| ~ cong(sK35,sK25,sK35,sK23) ),
inference(instantiation,[status(thm)],[c_14250]) ).
tcf(c_15510,plain,
para(sK23,sK22,sK22,sK23),
inference(superposition,[status(thm)],[c_10305,c_53]) ).
tcf(c_15937,plain,
! [X0: $i] :
( midp(sK24,X0,sK23)
| ~ midp(sK23,X0,sK24)
| ~ coll(sK24,X0,sK23) ),
inference(superposition,[status(thm)],[c_10376,c_94]) ).
tcf(c_15939,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK24,X0,X1)
| ~ para(sK24,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_10376,c_54]) ).
tcf(c_15940,plain,
para(sK24,sK23,sK23,sK24),
inference(superposition,[status(thm)],[c_10376,c_53]) ).
tcf(c_15952,plain,
( para(sK23,sK24,sK23,sK23)
| ~ para(sK24,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_15939]) ).
tcf(c_15954,plain,
( midp(sK24,sK23,sK23)
| ~ midp(sK23,sK23,sK24)
| ~ coll(sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_15937]) ).
tcf(c_16011,plain,
! [X0: $i] :
( midp(X0,sK25,sK23)
| ~ midp(X0,sK23,sK25)
| ~ para(sK23,sK23,sK25,sK25) ),
inference(superposition,[status(thm)],[c_10582,c_113]) ).
tcf(c_16013,plain,
! [X0: $i,X1: $i] :
( perp(sK23,sK25,X0,X1)
| ~ perp(sK25,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_10582,c_58]) ).
tcf(c_16030,plain,
( midp(sK23,sK25,sK23)
| ~ midp(sK23,sK23,sK25)
| ~ para(sK23,sK23,sK25,sK25) ),
inference(instantiation,[status(thm)],[c_16011]) ).
tcf(c_17641,plain,
! [X0: $i] :
( perp(sK39,X0,sK38,sK28)
| ~ midp(X0,sK24,sK24) ),
inference(superposition,[status(thm)],[c_4561,c_8066]) ).
tcf(c_17723,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( cong(X1,X3,X2,X3)
| ~ cyclic(X1,X3,X0,X3)
| ~ cyclic(X1,X3,X0,X2)
| ~ cyclic(X1,X3,X0,X0)
| ~ para(X0,X1,X0,X2) ),
inference(superposition,[status(thm)],[c_88,c_92]) ).
tcf(c_17759,plain,
( cong(sK23,sK23,sK23,sK23)
| ~ cyclic(sK23,sK23,sK23,sK23)
| ~ para(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_17723]) ).
tcf(c_18536,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK39,X2,X0,X1)
| ~ midp(X2,sK24,sK24)
| ~ perp(sK38,sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_17641,c_57]) ).
tcf(c_18574,plain,
( para(sK39,sK23,sK23,sK23)
| ~ midp(sK23,sK24,sK24)
| ~ perp(sK38,sK28,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_18536]) ).
tcf(c_19806,plain,
! [X0: $i] :
( perp(X0,sK36,sK23,sK25)
| ~ perp(sK23,sK25,X0,sK36) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_19807,plain,
( perp(sK23,sK36,sK23,sK25)
| ~ perp(sK23,sK25,sK23,sK36) ),
inference(instantiation,[status(thm)],[c_19806]) ).
tcf(c_20420,plain,
( para(sK23,sK23,sK24,sK24)
| ~ midp(sK32,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_7102]) ).
tcf(c_20542,plain,
( para(sK23,sK23,sK25,sK25)
| ~ midp(sK36,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_7106]) ).
tcf(c_21538,plain,
para(sK22,sK23,sK38,sK28),
inference(superposition,[status(thm)],[c_10606,c_7597]) ).
tcf(c_21847,plain,
para(sK38,sK28,sK22,sK23),
inference(superposition,[status(thm)],[c_21538,c_53]) ).
tcf(c_22071,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK22,X0,X1)
| ~ perp(sK25,sK24,X0,X1) ),
inference(superposition,[status(thm)],[c_10789,c_57]) ).
tcf(c_22097,plain,
( para(sK23,sK22,sK23,sK23)
| ~ perp(sK25,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_22071]) ).
tcf(c_22577,plain,
! [X0: $i] :
( midp(sK33,sK24,X0)
| ~ midp(sK33,sK22,sK25)
| ~ para(sK22,sK24,sK25,X0)
| ~ para(sK22,X0,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_7799]) ).
tcf(c_22579,plain,
! [X0: $i] :
( para(sK22,sK24,sK25,X0)
| ~ perp(sK22,sK24,sK23,sK25)
| ~ perp(sK23,sK25,sK25,X0) ),
inference(instantiation,[status(thm)],[c_7456]) ).
tcf(c_22580,plain,
( midp(sK33,sK24,sK23)
| ~ midp(sK33,sK22,sK25)
| ~ para(sK22,sK24,sK25,sK23)
| ~ para(sK22,sK23,sK25,sK24) ),
inference(instantiation,[status(thm)],[c_22577]) ).
tcf(c_22581,plain,
( para(sK22,sK24,sK25,sK23)
| ~ perp(sK22,sK24,sK23,sK25)
| ~ perp(sK23,sK25,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_22579]) ).
tcf(c_22955,plain,
( para(sK24,sK24,sK23,sK23)
| ~ para(sK23,sK23,sK24,sK24) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_23263,plain,
! [X0: $i] :
( perp(sK22,X0,sK35,sK27)
| ~ midp(sK33,X0,sK23) ),
inference(superposition,[status(thm)],[c_4567,c_8074]) ).
tcf(c_24898,plain,
! [X0: $i] :
( midp(sK22,X0,sK23)
| ~ midp(sK23,X0,sK22)
| ~ coll(sK22,X0,sK23) ),
inference(superposition,[status(thm)],[c_15510,c_94]) ).
tcf(c_24899,plain,
! [X0: $i,X1: $i] :
( perp(sK23,sK22,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_15510,c_58]) ).
tcf(c_24902,plain,
para(sK23,sK22,sK23,sK22),
inference(superposition,[status(thm)],[c_15510,c_52]) ).
tcf(c_24914,plain,
( perp(sK23,sK22,sK23,sK23)
| ~ perp(sK22,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_24899]) ).
tcf(c_24915,plain,
( midp(sK22,sK23,sK23)
| ~ midp(sK23,sK23,sK22)
| ~ coll(sK22,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_24898]) ).
tcf(c_24978,plain,
para(sK24,sK23,sK24,sK23),
inference(superposition,[status(thm)],[c_15940,c_52]) ).
tcf(c_25580,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK24,X3,X1,X2)
| ~ midp(X0,sK23,X3)
| ~ para(sK32,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_6903,c_54]) ).
tcf(c_25600,plain,
( para(sK24,sK23,sK23,sK23)
| ~ midp(sK23,sK23,sK23)
| ~ para(sK32,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_25580]) ).
tcf(c_25625,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK24)
| ~ midp(sK32,X1,X2)
| ~ midp(X0,sK23,X2)
| ~ coll(X0,X1,sK24) ),
inference(superposition,[status(thm)],[c_6904,c_94]) ).
tcf(c_25652,plain,
( midp(sK23,sK23,sK24)
| ~ midp(sK32,sK23,sK23)
| ~ midp(sK23,sK23,sK23)
| ~ coll(sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_25625]) ).
tcf(c_27048,plain,
! [X0: $i,X1: $i] :
( perp(sK38,sK28,X0,X1)
| ~ perp(sK22,sK23,X0,X1) ),
inference(superposition,[status(thm)],[c_21847,c_58]) ).
tcf(c_27063,plain,
( perp(sK38,sK28,sK23,sK23)
| ~ perp(sK22,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_27048]) ).
tcf(c_27685,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK25)
| ~ midp(sK36,X1,X2)
| ~ midp(X0,sK23,X2)
| ~ coll(X0,X1,sK25) ),
inference(superposition,[status(thm)],[c_6950,c_94]) ).
tcf(c_27712,plain,
( midp(sK23,sK23,sK25)
| ~ midp(sK36,sK23,sK23)
| ~ midp(sK23,sK23,sK23)
| ~ coll(sK23,sK23,sK25) ),
inference(instantiation,[status(thm)],[c_27685]) ).
tcf(c_27945,plain,
! [X0: $i] :
( perp(sK24,X0,sK25,sK24)
| ~ midp(sK40,X0,sK23) ),
inference(superposition,[status(thm)],[c_6341,c_8079]) ).
tcf(c_28529,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK23,X0,X1)
| ~ para(sK23,sK23,sK24,sK24)
| ~ para(sK24,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_28530,plain,
( para(sK23,sK23,sK23,sK23)
| ~ para(sK24,sK24,sK23,sK23)
| ~ para(sK23,sK23,sK24,sK24) ),
inference(instantiation,[status(thm)],[c_28529]) ).
tcf(c_29071,plain,
! [X0: $i] :
( perp(sK25,X0,sK24,sK25)
| ~ midp(sK41,X0,sK23) ),
inference(superposition,[status(thm)],[c_4581,c_8080]) ).
tcf(c_29710,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK22,sK24,X2,X3)
| ~ para(sK22,sK24,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_29711,plain,
( perp(sK22,sK24,sK23,sK23)
| ~ perp(sK23,sK23,sK23,sK23)
| ~ para(sK22,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_29710]) ).
tcf(c_29712,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK25,sK24,X2,X3)
| ~ para(sK25,sK24,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_29713,plain,
( perp(sK25,sK24,sK23,sK23)
| ~ perp(sK23,sK23,sK23,sK23)
| ~ para(sK25,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_29712]) ).
tcf(c_30524,plain,
! [X0: $i,X1: $i] :
( circle(X0,X1,sK25,sK23)
| ~ cong(X0,X1,X0,sK25)
| ~ cong(X0,X1,X0,sK23) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_30525,plain,
( circle(sK23,sK23,sK25,sK23)
| ~ cong(sK23,sK23,sK23,sK25)
| ~ cong(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_30524]) ).
tcf(c_30686,plain,
coll(sK24,sK23,sK23),
inference(superposition,[status(thm)],[c_24978,c_115]) ).
tcf(c_30947,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(X0,X1,sK22)
| ~ midp(sK41,X1,X2)
| ~ midp(X0,sK25,X2)
| ~ coll(X0,X1,sK22) ),
inference(superposition,[status(thm)],[c_7188,c_94]) ).
tcf(c_30975,plain,
( midp(sK23,sK23,sK22)
| ~ midp(sK41,sK23,sK23)
| ~ midp(sK23,sK25,sK23)
| ~ coll(sK23,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_30947]) ).
tcf(c_31875,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,X0,sK22)
| ~ perp(X0,sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_31876,plain,
( perp(sK23,sK23,sK23,sK22)
| ~ perp(sK23,sK22,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_31875]) ).
tcf(c_34225,plain,
( perp(sK36,sK28,sK35,sK27)
| ~ midp(sK33,sK24,sK23) ),
inference(superposition,[status(thm)],[c_23263,c_11314]) ).
tcf(c_34928,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK22,X3,sK25,X2)
| ~ para(sK22,X3,X0,X1)
| ~ para(X0,X1,sK25,X2) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_34929,plain,
( para(sK22,sK23,sK25,sK23)
| ~ para(sK22,sK23,sK23,sK23)
| ~ para(sK23,sK23,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_34928]) ).
tcf(c_34930,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK22,X3,sK24,X2)
| ~ para(sK22,X3,X0,X1)
| ~ para(X0,X1,sK24,X2) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_34931,plain,
( para(sK22,sK23,sK24,sK23)
| ~ para(sK22,sK23,sK23,sK23)
| ~ para(sK23,sK23,sK24,sK23) ),
inference(instantiation,[status(thm)],[c_34930]) ).
tcf(c_34932,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK25,X3,sK24,X2)
| ~ para(sK25,X3,X0,X1)
| ~ para(X0,X1,sK24,X2) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_34933,plain,
( para(sK25,sK23,sK24,sK23)
| ~ para(sK25,sK23,sK23,sK23)
| ~ para(sK23,sK23,sK24,sK23) ),
inference(instantiation,[status(thm)],[c_34932]) ).
tcf(c_35556,plain,
cong(sK36,sK23,sK36,sK25),
inference(global_subsumption_just,[status(thm)],[c_7321,c_189,c_6683]) ).
tcf(c_35566,plain,
cong(sK36,sK25,sK36,sK23),
inference(superposition,[status(thm)],[c_35556,c_72]) ).
tcf(c_38036,plain,
cong(sK36,sK25,sK23,sK36),
inference(superposition,[status(thm)],[c_35566,c_71]) ).
tcf(c_38570,plain,
( eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27)
| ~ eqangle(sK29,sK28,sK28,sK27,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_41283,plain,
cong(sK23,sK36,sK36,sK25),
inference(superposition,[status(thm)],[c_38036,c_72]) ).
tcf(c_43099,plain,
! [X0: $i] :
( perp(sK23,sK25,X0,sK36)
| ~ cong(sK23,sK36,sK25,sK36)
| ~ cong(sK23,X0,sK25,X0) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_43100,plain,
( perp(sK23,sK25,sK23,sK36)
| ~ cong(sK23,sK36,sK25,sK36)
| ~ cong(sK23,sK23,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_43099]) ).
tcf(c_43906,plain,
cong(sK23,sK36,sK25,sK36),
inference(superposition,[status(thm)],[c_41283,c_71]) ).
tcf(c_47610,plain,
! [X0: $i,X1: $i] :
( perp(sK23,sK25,sK25,X1)
| ~ coll(X0,sK23,X1)
| ~ circle(X0,sK23,sK25,X1) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_47611,plain,
( perp(sK23,sK25,sK25,sK23)
| ~ coll(sK23,sK23,sK23)
| ~ circle(sK23,sK23,sK25,sK23) ),
inference(instantiation,[status(thm)],[c_47610]) ).
tcf(c_64791,plain,
! [X0: $i,X1: $i] :
( perp(sK23,X0,sK25,sK24)
| ~ midp(sK40,X1,sK23)
| ~ midp(sK37,X0,X1) ),
inference(superposition,[status(thm)],[c_27945,c_8072]) ).
tcf(c_64851,plain,
( perp(sK23,sK23,sK25,sK24)
| ~ midp(sK40,sK23,sK23)
| ~ midp(sK37,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_64791]) ).
tcf(c_70674,plain,
( para(sK23,sK25,sK35,sK27)
| ~ midp(sK33,sK24,sK23) ),
inference(superposition,[status(thm)],[c_34225,c_7606]) ).
tcf(c_75603,plain,
( perp(sK23,sK25,sK24,sK25)
| ~ midp(sK41,sK23,sK23) ),
inference(superposition,[status(thm)],[c_29071,c_16013]) ).
tcf(c_85377,plain,
( eqangle(sK29,sK28,sK28,sK27,sK23,sK22,sK22,sK24)
| ~ eqangle(sK29,sK28,sK23,sK22,sK28,sK27,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_88245,plain,
perp(sK23,sK25,sK24,sK25),
inference(global_subsumption_just,[status(thm)],[c_75603,c_187,c_181,c_177,c_215,c_6252,c_6273,c_6268,c_6677,c_6682,c_7063,c_7745,c_7746,c_7775,c_7776,c_7804,c_9383,c_11543,c_11563,c_11586,c_11783,c_12696,c_13687,c_14252,c_17759,c_20420,c_22955,c_28530,c_29711,c_29713,c_34929,c_75603]) ).
tcf(c_88250,plain,
perp(sK23,sK25,sK25,sK24),
inference(superposition,[status(thm)],[c_88245,c_55]) ).
tcf(c_91100,plain,
! [X0: $i] :
( cong(sK23,X0,sK25,X0)
| ~ midp(X0,sK23,sK24) ),
inference(superposition,[status(thm)],[c_88250,c_101]) ).
tcf(c_91138,plain,
( cong(sK23,sK23,sK25,sK23)
| ~ midp(sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_91100]) ).
tcf(c_103273,plain,
( para(sK22,sK23,sK25,sK24)
| ~ perp(sK30,sK26,sK25,sK24)
| ~ perp(sK22,sK23,sK30,sK26) ),
inference(instantiation,[status(thm)],[c_7460]) ).
tcf(c_118705,plain,
para(sK39,sK29,sK39,sK29),
inference(superposition,[status(thm)],[c_4559,c_7639]) ).
tcf(c_118811,plain,
! [X0: $i] :
( midp(X0,sK29,sK29)
| ~ midp(X0,sK39,sK39)
| ~ para(sK39,sK29,sK39,sK29) ),
inference(superposition,[status(thm)],[c_118705,c_113]) ).
tcf(c_118821,plain,
! [X0: $i] :
( midp(X0,sK29,sK29)
| ~ midp(X0,sK39,sK39) ),
inference(forward_subsumption_resolution,[status(thm)],[c_118811,c_118705]) ).
tcf(c_118824,plain,
( midp(sK23,sK29,sK29)
| ~ midp(sK23,sK39,sK39) ),
inference(instantiation,[status(thm)],[c_118821]) ).
tcf(c_122460,plain,
! [X0: $i,X1: $i] :
( perp(sK30,sK26,sK25,sK24)
| ~ perp(X0,X1,sK25,sK24)
| ~ para(sK30,sK26,X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_122461,plain,
( perp(sK30,sK26,sK25,sK24)
| ~ perp(sK23,sK23,sK25,sK24)
| ~ para(sK30,sK26,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_122460]) ).
tcf(c_123442,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK29,sK28,sK23,sK22,sK28,sK27,sK22,sK24)
| ~ eqangle(sK29,sK28,sK23,sK22,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK28,sK27,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_123484,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK29,sK28)
| ~ para(X0,X1,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_123485,plain,
( para(sK23,sK23,sK29,sK28)
| ~ para(sK23,sK23,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_123484]) ).
tcf(c_123489,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK29,sK28)
| ~ eqangle(X0,X1,X2,X3,sK29,sK28,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_123544,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK23,sK22,sK22,sK24)
| ~ eqangle(sK23,sK22,sK22,sK24,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_123545,plain,
( eqangle(sK23,sK23,sK23,sK23,sK23,sK22,sK22,sK24)
| ~ eqangle(sK23,sK22,sK22,sK24,sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_123544]) ).
tcf(c_123548,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK23,sK22,sK22,sK24)
| ~ eqangle(X4,X5,X6,X7,sK23,sK22,sK22,sK24)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_123566,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK28,sK27,sK22,sK24,sK28,sK27)
| ~ para(X0,X1,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_123680,plain,
! [X0: $i,X1: $i] :
( cong(sK22,X0,sK22,X1)
| ~ midp(sK22,X0,X1) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_123681,plain,
( cong(sK22,sK23,sK22,sK23)
| ~ midp(sK22,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_123680]) ).
tcf(c_123852,plain,
! [X0: $i,X1: $i,X2: $i] :
( circle(sK22,X0,X2,X1)
| ~ cong(sK22,X0,sK22,X2)
| ~ cong(sK22,X0,sK22,X1) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_123853,plain,
( circle(sK22,sK23,sK23,sK23)
| ~ cong(sK22,sK23,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_123852]) ).
tcf(c_124010,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK29)
| ~ para(X0,X1,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_124016,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK28,sK29)
| ~ perp(X2,X3,sK28,sK29)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_124040,plain,
! [X0: $i,X1: $i] :
( para(sK29,sK28,X0,X1)
| ~ para(X0,X1,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_124041,plain,
( para(sK29,sK28,sK23,sK23)
| ~ para(sK23,sK23,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_124040]) ).
tcf(c_124082,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,sK28,sK27)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK28,sK27,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_124092,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK28,sK27)
| ~ perp(X2,X3,sK28,sK27)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_124093,plain,
( para(sK23,sK23,sK28,sK27)
| ~ perp(sK23,sK23,sK28,sK27)
| ~ perp(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_124092]) ).
tcf(c_124263,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,X0,X2,X3,sK29,sK28,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK29,sK28,X2,X3) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_124264,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK29,sK28,X0,X1)
| ~ eqangle(X0,X1,X2,X3,X0,X1,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_124318,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,sK23,X0,X1,sK22,sK23,sK22,sK24)
| ~ midp(sK24,sK23,X1)
| ~ circle(sK22,X0,sK23,X1) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_124319,plain,
( eqangle(sK23,sK23,sK23,sK23,sK22,sK23,sK22,sK24)
| ~ midp(sK24,sK23,sK23)
| ~ circle(sK22,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_124318]) ).
tcf(c_124367,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK29,sK28,sK23,sK22,sK29,sK28)
| ~ para(X0,X1,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_124391,plain,
! [X0: $i,X1: $i] :
( eqangle(sK29,sK28,sK23,sK22,sK28,sK27,sK22,sK24)
| ~ eqangle(sK29,sK28,sK23,sK22,X0,X1,sK22,sK24)
| ~ eqangle(X0,X1,sK22,sK24,sK28,sK27,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_123442]) ).
tcf(c_124392,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK22,sK24,sK28,sK27,sK22,sK24)
| ~ para(X0,X1,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_124393,plain,
( eqangle(sK29,sK28,sK23,sK22,sK28,sK27,sK22,sK24)
| ~ eqangle(sK29,sK28,sK23,sK22,sK23,sK23,sK22,sK24)
| ~ eqangle(sK23,sK23,sK22,sK24,sK28,sK27,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_124391]) ).
tcf(c_124394,plain,
( eqangle(sK23,sK23,sK22,sK24,sK28,sK27,sK22,sK24)
| ~ para(sK23,sK23,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_124392]) ).
tcf(c_124431,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK29,sK28)
| ~ cong(X0,sK28,X1,sK28)
| ~ cong(X0,sK29,X1,sK29) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_124432,plain,
( perp(sK23,sK23,sK29,sK28)
| ~ cong(sK23,sK28,sK23,sK28)
| ~ cong(sK23,sK29,sK23,sK29) ),
inference(instantiation,[status(thm)],[c_124431]) ).
tcf(c_124433,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( perp(X0,X1,sK29,sK28)
| ~ perp(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK29,sK28,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_124541,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK22,sK22,sK24,X0,X1,X2,X3)
| ~ eqangle(sK22,sK23,sK22,sK24,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_124542,plain,
( eqangle(sK23,sK22,sK22,sK24,sK23,sK23,sK23,sK23)
| ~ eqangle(sK22,sK23,sK22,sK24,sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_124541]) ).
tcf(c_124547,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK22,sK22,sK24,X0,X1,X2,X3)
| ~ eqangle(sK23,sK22,X0,X1,sK22,sK24,X2,X3) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_124566,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK23,sK22,X2,X3,sK22,sK24)
| ~ eqangle(X0,X1,X2,X3,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_124776,plain,
! [X0: $i] :
( perp(sK29,sK28,sK28,X0)
| ~ perp(sK28,X0,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_124832,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK29,sK28,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK29,sK28,X4,X5) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_125897,plain,
( perp(sK29,sK28,sK28,sK29)
| ~ perp(sK28,sK29,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_124776]) ).
tcf(c_126170,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X0,sK22,X3,sK22)
| ~ perp(X1,X2,X3,sK22)
| ~ para(X0,sK22,X1,X2) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_126171,plain,
( perp(sK23,sK22,sK23,sK22)
| ~ perp(sK23,sK23,sK23,sK22)
| ~ para(sK23,sK22,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_126170]) ).
tcf(c_127039,plain,
! [X0: $i] :
( cong(X0,sK29,X0,sK29)
| ~ midp(X0,sK29,sK29) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_127040,plain,
( cong(sK23,sK29,sK23,sK29)
| ~ midp(sK23,sK29,sK29) ),
inference(instantiation,[status(thm)],[c_127039]) ).
tcf(c_127348,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK29,sK28,X2,X3,X0,X1,X2,X3)
| ~ para(sK29,sK28,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_127349,plain,
( eqangle(sK29,sK28,sK23,sK23,sK23,sK23,sK23,sK23)
| ~ para(sK29,sK28,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_127348]) ).
tcf(c_127928,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK28,sK27)
| ~ cong(X0,sK27,X1,sK27)
| ~ cong(X0,sK28,X1,sK28) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_127929,plain,
( perp(sK23,sK23,sK28,sK27)
| ~ cong(sK23,sK27,sK23,sK27)
| ~ cong(sK23,sK28,sK23,sK28) ),
inference(instantiation,[status(thm)],[c_127928]) ).
tcf(c_128839,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK22,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK22,sK23,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_128840,plain,
( eqangle(sK22,sK23,sK22,sK24,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK22,sK23,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_128839]) ).
tcf(c_128918,plain,
( eqangle(sK23,sK22,sK22,sK24,sK28,sK27,sK28,sK27)
| ~ eqangle(sK23,sK22,sK28,sK27,sK22,sK24,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_124547]) ).
tcf(c_128920,plain,
( eqangle(sK23,sK22,sK28,sK27,sK22,sK24,sK28,sK27)
| ~ para(sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_123566]) ).
tcf(c_129296,plain,
( eqangle(sK29,sK28,sK23,sK22,sK29,sK28,sK23,sK22)
| ~ eqangle(sK23,sK22,sK29,sK28,sK23,sK22,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_124264]) ).
tcf(c_129297,plain,
( eqangle(sK23,sK22,sK29,sK28,sK23,sK22,sK29,sK28)
| ~ para(sK23,sK22,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_124367]) ).
tcf(c_130408,plain,
( eqangle(sK28,sK27,sK28,sK27,sK23,sK22,sK22,sK24)
| ~ eqangle(sK23,sK22,sK22,sK24,sK28,sK27,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_123544]) ).
tcf(c_132328,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK29,sK28,X0,X1,sK23,sK22,sK22,sK24)
| ~ eqangle(X2,X3,X4,X5,sK23,sK22,sK22,sK24)
| ~ eqangle(sK29,sK28,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_123548]) ).
tcf(c_132334,plain,
( eqangle(sK29,sK28,sK23,sK23,sK23,sK22,sK22,sK24)
| ~ eqangle(sK29,sK28,sK23,sK23,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_132328]) ).
tcf(c_132345,plain,
! [X0: $i,X1: $i] :
( eqangle(sK29,sK28,sK23,sK22,X0,X1,sK22,sK24)
| ~ eqangle(sK29,sK28,X0,X1,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_124566]) ).
tcf(c_132349,plain,
( eqangle(sK29,sK28,sK23,sK22,sK23,sK23,sK22,sK24)
| ~ eqangle(sK29,sK28,sK23,sK23,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_132345]) ).
tcf(c_132417,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK27)
| ~ para(sK23,sK22,sK22,sK24)
| ~ eqangle(X0,X1,sK28,sK27,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_124082]) ).
tcf(c_132451,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(sK23,sK22,sK22,sK24)
| ~ para(X0,X1,X2,X3)
| ~ eqangle(sK23,sK22,sK22,sK24,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_132453,plain,
( para(sK23,sK22,sK22,sK24)
| ~ para(sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK22,sK22,sK24,sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_132451]) ).
tcf(c_138319,plain,
( para(sK28,sK27,sK28,sK27)
| ~ para(sK23,sK22,sK22,sK24)
| ~ eqangle(sK28,sK27,sK28,sK27,sK23,sK22,sK22,sK24) ),
inference(instantiation,[status(thm)],[c_132417]) ).
tcf(c_139160,plain,
! [X0: $i,X1: $i] :
( cong(X0,sK27,X0,sK27)
| ~ midp(sK27,X0,X1)
| ~ perp(X0,X0,X0,X1) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_139162,plain,
( cong(sK23,sK27,sK23,sK27)
| ~ midp(sK27,sK23,sK23)
| ~ perp(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_139160]) ).
tcf(c_143141,plain,
( eqangle(sK28,sK29,sK23,sK22,sK29,sK28,sK23,sK22)
| ~ eqangle(sK29,sK28,sK23,sK22,sK29,sK28,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_124263]) ).
tcf(c_143142,plain,
( para(sK29,sK28,sK29,sK28)
| ~ eqangle(sK29,sK28,sK23,sK22,sK29,sK28,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_123489]) ).
tcf(c_149795,plain,
( para(sK28,sK29,sK29,sK28)
| ~ eqangle(sK28,sK29,sK23,sK22,sK29,sK28,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_123489]) ).
tcf(c_149800,plain,
( eqangle(sK28,sK29,sK29,sK28,sK23,sK22,sK23,sK22)
| ~ eqangle(sK28,sK29,sK23,sK22,sK29,sK28,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_124832]) ).
tcf(c_152142,plain,
( para(sK28,sK29,sK28,sK29)
| ~ para(sK28,sK29,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_124010]) ).
tcf(c_156126,plain,
( perp(sK28,sK29,sK29,sK28)
| ~ perp(sK23,sK22,sK23,sK22)
| ~ eqangle(sK28,sK29,sK29,sK28,sK23,sK22,sK23,sK22) ),
inference(instantiation,[status(thm)],[c_124433]) ).
tcf(c_162453,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK29)
| ~ perp(sK29,sK28,sK28,sK29)
| ~ perp(X0,X1,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_124016]) ).
tcf(c_162454,plain,
( para(sK23,sK23,sK28,sK29)
| ~ perp(sK29,sK28,sK28,sK29)
| ~ perp(sK23,sK23,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_162453]) ).
tcf(c_164507,plain,
! [X0: $i,X1: $i] :
( coll(sK27,X0,X1)
| ~ para(sK27,X0,sK27,X1) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_164512,plain,
( coll(sK27,sK23,sK23)
| ~ para(sK27,sK23,sK27,sK23) ),
inference(instantiation,[status(thm)],[c_164507]) ).
tcf(c_167100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_167102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_167147,plain,
! [X0: $i,X1: $i] :
( para(sK36,X0,sK25,X1)
| ~ midp(X0,sK23,X1) ),
inference(superposition,[status(thm)],[c_4566,c_93]) ).
tcf(c_167222,plain,
( eqangle(sK23,sK24,sK22,sK23,sK29,sK27,sK28,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_167436,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK23,sK24,X2,X3,X0,X1)
| ~ eqangle(sK23,sK24,sK22,sK23,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_167440,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(sK22,sK23,X0,X1,sK23,sK24,X2,X3) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_167441,plain,
( eqangle(sK22,sK23,sK23,sK24,sK23,sK23,sK23,sK23)
| ~ eqangle(sK22,sK23,sK23,sK23,sK23,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_167440]) ).
tcf(c_167442,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(sK22,sK23,sK23,sK24,X4,X5,X6,X7)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_167945,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK25,X0,X1)
| ~ perp(sK36,sK28,X0,X1) ),
inference(superposition,[status(thm)],[c_4565,c_57]) ).
tcf(c_168161,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(sK36,X3,X1,X2)
| ~ midp(X3,sK23,X0)
| ~ perp(sK25,X0,X1,X2) ),
inference(superposition,[status(thm)],[c_167147,c_58]) ).
tcf(c_168674,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK24,sK22,sK23,X0,X1,sK22,sK23)
| ~ para(sK23,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_168830,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK28,sK29,X0,X1,sK28,sK29)
| ~ para(sK22,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_168911,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK28,sK27,X0,X1,sK28,sK27)
| ~ para(sK22,sK23,X0,X1) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_168970,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK22,sK23,sK23,sK24)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_168971,plain,
( eqangle(sK23,sK23,sK23,sK23,sK22,sK23,sK23,sK24)
| ~ eqangle(sK22,sK23,sK23,sK24,sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_168970]) ).
tcf(c_168974,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK22,sK23,sK23,sK24)
| ~ eqangle(X4,X5,X6,X7,sK22,sK23,sK23,sK24)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_169053,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,X0,X1,sK23,sK24,X2,X3)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_169057,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,X0,X1,sK23,sK24,X0,X1)
| ~ para(sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_169058,plain,
( eqangle(sK22,sK23,sK23,sK23,sK23,sK24,sK23,sK23)
| ~ para(sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_169057]) ).
tcf(c_169144,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X0,X1,sK27,X4,X2,X3,sK27,X4)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_169146,plain,
( eqangle(sK23,sK23,sK27,sK23,sK23,sK23,sK27,sK23)
| ~ para(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_169144]) ).
tcf(c_169704,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( eqangle(X1,X0,X2,X3,X4,X5,X6,sK27)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,sK27) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_169705,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( eqangle(X2,X3,X0,X1,X5,X6,X4,sK27)
| ~ eqangle(X0,X1,X2,X3,X4,sK27,X5,X6) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_169710,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] :
( eqangle(X0,X1,X2,X3,X8,X9,X10,sK27)
| ~ eqangle(X4,X5,X6,X7,X8,X9,X10,sK27)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_169712,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(X0,X1,X4,sK27,X2,X3,X4,sK27)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_171175,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(sK22,sK23,sK23,sK24,X0,X1,sK27,X2)
| ~ eqangle(sK22,sK23,X0,X1,sK23,sK24,sK27,X2) ),
inference(instantiation,[status(thm)],[c_167440]) ).
tcf(c_171963,plain,
( eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK29,sK27)
| ~ eqangle(sK23,sK24,sK22,sK23,sK29,sK27,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_167436]) ).
tcf(c_172087,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK27,sK29,sK28,sK27,sK27,sK29)
| ~ para(X0,X1,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_169144]) ).
tcf(c_172089,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,sK27,sK29)
| ~ eqangle(X0,X1,sK27,sK29,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_167102]) ).
tcf(c_172090,plain,
( eqangle(sK23,sK23,sK27,sK29,sK28,sK27,sK27,sK29)
| ~ para(sK23,sK23,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_172087]) ).
tcf(c_172091,plain,
( eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK23,sK23,sK27,sK29)
| ~ eqangle(sK23,sK23,sK27,sK29,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_172089]) ).
tcf(c_174922,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK28,sK29,X0,X1)
| ~ eqangle(sK22,sK23,sK28,sK29,sK23,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_167440]) ).
tcf(c_175888,plain,
! [X0: $i,X1: $i,X2: $i] :
( eqangle(sK22,sK23,X0,X1,sK23,sK24,X2,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,sK27) ),
inference(instantiation,[status(thm)],[c_169053]) ).
tcf(c_176020,plain,
! [X0: $i] :
( eqangle(sK22,sK23,sK27,X0,sK23,sK24,sK27,X0)
| ~ para(sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_169057]) ).
tcf(c_176741,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( eqangle(X2,X3,X0,X1,sK27,X6,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,sK27,X6) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_178818,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK28,sK27)
| ~ eqangle(X0,X1,X2,X3,sK28,sK27,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_179660,plain,
( eqangle(sK22,sK23,sK23,sK24,sK22,sK23,sK28,sK27)
| ~ eqangle(sK23,sK24,sK22,sK23,sK28,sK27,sK22,sK23) ),
inference(instantiation,[status(thm)],[c_167436]) ).
tcf(c_179796,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK29,sK27)
| ~ perp(X2,X3,sK29,sK27)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_179797,plain,
( para(sK23,sK23,sK29,sK27)
| ~ perp(sK23,sK23,sK29,sK27)
| ~ perp(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_179796]) ).
tcf(c_179841,plain,
! [X0: $i] :
( perp(sK36,X0,sK35,sK27)
| ~ midp(X0,sK23,sK23) ),
inference(superposition,[status(thm)],[c_4567,c_168161]) ).
tcf(c_180432,plain,
( eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK28,sK29)
| ~ eqangle(sK22,sK23,sK28,sK29,sK23,sK24,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_174922]) ).
tcf(c_180433,plain,
( eqangle(sK22,sK23,sK28,sK29,sK23,sK24,sK28,sK29)
| ~ para(sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_168830]) ).
tcf(c_181742,plain,
( para(sK23,sK25,sK35,sK27)
| ~ midp(sK28,sK23,sK23) ),
inference(superposition,[status(thm)],[c_179841,c_167945]) ).
tcf(c_182768,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK29,sK27,sK28,sK29,sK29,sK27)
| ~ para(X0,X1,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_169712]) ).
tcf(c_182774,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,sK29,sK27)
| ~ eqangle(X0,X1,sK29,sK27,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_167100]) ).
tcf(c_182775,plain,
( eqangle(sK23,sK23,sK29,sK27,sK28,sK29,sK29,sK27)
| ~ para(sK23,sK23,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_182768]) ).
tcf(c_182776,plain,
( eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK23,sK23,sK29,sK27)
| ~ eqangle(sK23,sK23,sK29,sK27,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_182774]) ).
tcf(c_182794,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK24,sK29,sK27,X0,X1,sK29,sK27)
| ~ para(sK23,sK24,X0,X1) ),
inference(instantiation,[status(thm)],[c_169712]) ).
tcf(c_182796,plain,
( eqangle(sK23,sK24,sK29,sK27,sK23,sK23,sK29,sK27)
| ~ para(sK23,sK24,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_182794]) ).
tcf(c_187368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK23,sK24,sK29,sK27,sK22,sK23,sK23,sK24)
| ~ eqangle(sK23,sK24,sK29,sK27,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_168974]) ).
tcf(c_187370,plain,
( eqangle(sK23,sK24,sK29,sK27,sK22,sK23,sK23,sK24)
| ~ eqangle(sK23,sK24,sK29,sK27,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_187368]) ).
tcf(c_188251,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,X4,X5,X6,sK27)
| ~ eqangle(X0,X1,X2,X3,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_169710]) ).
tcf(c_188881,plain,
! [X0: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK27,X0,sK27,X0)
| ~ eqangle(sK22,sK23,sK27,X0,sK23,sK24,sK27,X0) ),
inference(instantiation,[status(thm)],[c_171175]) ).
tcf(c_193192,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(sK27,X0,sK27,X0)
| ~ eqangle(sK27,X0,X1,X2,sK27,X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_193195,plain,
( para(sK27,sK23,sK27,sK23)
| ~ eqangle(sK27,sK23,sK23,sK23,sK27,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_193192]) ).
tcf(c_194095,plain,
( eqangle(sK23,sK24,sK22,sK23,sK28,sK27,sK22,sK23)
| ~ para(sK23,sK24,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_168674]) ).
tcf(c_202058,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK27,sK29)
| ~ cong(X0,sK27,X1,sK27)
| ~ cong(X0,sK29,X1,sK29) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_202059,plain,
( perp(sK23,sK23,sK27,sK29)
| ~ cong(sK23,sK27,sK23,sK27)
| ~ cong(sK23,sK29,sK23,sK29) ),
inference(instantiation,[status(thm)],[c_202058]) ).
tcf(c_202939,plain,
( eqangle(sK22,sK23,sK27,sK29,sK23,sK24,sK27,sK29)
| ~ para(sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_176020]) ).
tcf(c_203597,plain,
( para(sK23,sK24,sK28,sK27)
| ~ eqangle(sK23,sK24,sK29,sK27,sK28,sK27,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_178818]) ).
tcf(c_221006,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( eqangle(sK27,X2,X0,X1,sK27,X2,X3,X4)
| ~ eqangle(X0,X1,sK27,X2,X3,X4,sK27,X2) ),
inference(instantiation,[status(thm)],[c_176741]) ).
tcf(c_221007,plain,
( eqangle(sK27,sK23,sK23,sK23,sK27,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK27,sK23,sK23,sK23,sK27,sK23) ),
inference(instantiation,[status(thm)],[c_221006]) ).
tcf(c_222372,plain,
para(sK23,sK25,sK35,sK27),
inference(global_subsumption_just,[status(thm)],[c_181742,c_189,c_187,c_183,c_181,c_177,c_178,c_175,c_206,c_215,c_6251,c_6248,c_6247,c_6243,c_6273,c_6268,c_6315,c_6385,c_6676,c_6677,c_6682,c_7078,c_7140,c_7443,c_7745,c_7746,c_7758,c_7775,c_7776,c_9383,c_10232,c_10818,c_11056,c_11242,c_11410,c_11543,c_11563,c_11783,c_12696,c_13289,c_13687,c_14252,c_17759,c_19807,c_20420,c_22580,c_22581,c_22955,c_25600,c_25652,c_27712,c_28530,c_29711,c_29713,c_30525,c_34931,c_43100,c_43906,c_47611,c_64851,c_70674,c_91138,c_103273,c_122461]) ).
tcf(c_222378,plain,
para(sK35,sK27,sK23,sK25),
inference(superposition,[status(thm)],[c_222372,c_53]) ).
tcf(c_222959,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK22,sK23,sK23,sK24,sK29,sK28,X4,X5)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK29,sK28,X4,X5) ),
inference(instantiation,[status(thm)],[c_167442]) ).
tcf(c_229062,plain,
para(sK35,sK27,sK25,sK23),
inference(superposition,[status(thm)],[c_222378,c_52]) ).
tcf(c_243132,plain,
( eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK28,sK27)
| ~ eqangle(sK22,sK23,sK28,sK27,sK29,sK28,sK28,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK22,sK23,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_222959]) ).
tcf(c_243136,plain,
( eqangle(sK22,sK23,sK28,sK27,sK29,sK28,sK28,sK27)
| ~ para(sK22,sK23,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_168911]) ).
tcf(c_245145,plain,
! [X0: $i] :
( midp(sK27,X0,sK23)
| ~ midp(sK35,X0,sK25)
| ~ coll(sK27,X0,sK23) ),
inference(superposition,[status(thm)],[c_229062,c_94]) ).
tcf(c_245162,plain,
( midp(sK27,sK23,sK23)
| ~ midp(sK35,sK23,sK25)
| ~ coll(sK27,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_245145]) ).
tcf(c_246161,plain,
( eqangle(sK28,sK27,sK27,sK29,sK28,sK27,sK27,sK29)
| ~ para(sK28,sK27,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_172087]) ).
tcf(c_249115,plain,
( eqangle(sK22,sK23,sK29,sK28,sK23,sK24,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_175888]) ).
tcf(c_252075,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,X0,X2,X3,sK27,sK29,sK28,sK27)
| ~ eqangle(X0,X1,X2,X3,sK27,sK29,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_169704]) ).
tcf(c_253472,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK27,sK29,sK28,sK27)
| ~ eqangle(X0,X1,X2,X3,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_169705]) ).
tcf(c_256658,plain,
( eqangle(sK27,sK29,sK28,sK27,sK27,sK29,sK28,sK27)
| ~ eqangle(sK28,sK27,sK27,sK29,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_253472]) ).
tcf(c_259983,plain,
( eqangle(sK23,sK24,sK29,sK27,sK28,sK27,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK29,sK27)
| ~ eqangle(sK23,sK24,sK29,sK27,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_188251]) ).
tcf(c_279484,plain,
( eqangle(sK29,sK27,sK28,sK27,sK27,sK29,sK28,sK27)
| ~ eqangle(sK27,sK29,sK28,sK27,sK27,sK29,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_252075]) ).
tcf(c_290584,plain,
( eqangle(sK22,sK23,sK23,sK24,sK27,sK29,sK27,sK29)
| ~ eqangle(sK22,sK23,sK27,sK29,sK23,sK24,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_188881]) ).
tcf(c_297083,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,X0,X2,X3,sK28,sK29,sK29,sK27)
| ~ eqangle(X0,X1,X2,X3,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_297084,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK28,sK29,sK29,sK27)
| ~ eqangle(X0,X1,X2,X3,sK29,sK27,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_297089,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK29,sK27,sK28,sK29,sK29,sK27)
| ~ para(X0,X1,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_297093,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK28,sK27,sK27,sK29)
| ~ eqangle(X0,X1,X2,X3,sK27,sK29,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_297194,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK28,sK27)
| ~ eqangle(X0,X1,X2,X3,sK28,sK27,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_297342,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK22,sK23,sK23,sK24,X4,X5,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_297350,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK28,sK29)
| ~ eqangle(X0,X1,X2,X3,sK28,sK29,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_297373,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK22,sK23,sK23,sK24,X4,X5,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_297402,plain,
! [X0: $i,X1: $i] :
( eqangle(sK28,sK27,X0,X1,sK28,sK27,sK27,sK29)
| ~ eqangle(X0,X1,sK28,sK27,sK27,sK29,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_297093]) ).
tcf(c_297423,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X1,X0,X2,X3,sK29,sK27,sK28,sK29)
| ~ eqangle(X0,X1,X2,X3,sK29,sK27,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_297424,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X2,X3,X0,X1,sK29,sK27,sK28,sK29)
| ~ eqangle(X0,X1,X2,X3,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_297441,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK28,sK29,sK29,sK27,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_297451,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK28,sK27,sK27,sK29,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_297957,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK28,sK27,X2,X3)
| ~ eqangle(X4,X5,X6,X7,sK28,sK27,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_297971,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( midp(X3,X1,sK28)
| ~ midp(X3,X0,X2)
| ~ para(X0,sK28,X2,X1)
| ~ para(X0,X1,X2,sK28) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_298153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( para(X0,X1,sK27,sK29)
| ~ perp(X2,X3,sK27,sK29)
| ~ perp(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_298154,plain,
( para(sK23,sK23,sK27,sK29)
| ~ perp(sK23,sK23,sK27,sK29)
| ~ perp(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_298153]) ).
tcf(c_298237,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK23,sK24,sK22,sK23,sK29,sK27,X4,X5)
| ~ eqangle(sK23,sK24,sK22,sK23,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,sK29,sK27,X4,X5) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_298250,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK29,sK27,sK22,sK23,sK23,sK24)
| ~ eqangle(X2,X3,X4,X5,sK22,sK23,sK23,sK24)
| ~ eqangle(X0,X1,sK29,sK27,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_298251,plain,
( eqangle(sK23,sK23,sK29,sK27,sK22,sK23,sK23,sK24)
| ~ eqangle(sK23,sK23,sK29,sK27,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_298250]) ).
tcf(c_298268,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,sK29,sK28)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK29,sK28,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_298330,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK27,sK29,sK22,sK23,sK23,sK24)
| ~ eqangle(X2,X3,X4,X5,sK22,sK23,sK23,sK24)
| ~ eqangle(X0,X1,sK27,sK29,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_298331,plain,
( eqangle(sK23,sK23,sK27,sK29,sK22,sK23,sK23,sK24)
| ~ eqangle(sK23,sK23,sK27,sK29,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_298330]) ).
tcf(c_298360,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( para(X0,X1,sK29,sK27)
| ~ para(X2,X3,X4,X5)
| ~ eqangle(X0,X1,sK29,sK27,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_298673,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(sK23,sK24,sK29,sK27,X4,X5,X6,X7)
| ~ eqangle(sK23,sK24,sK29,sK27,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_298776,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( eqangle(X0,X1,X2,X3,sK28,sK29,X2,X3)
| ~ eqangle(X4,X5,X6,X7,sK28,sK29,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_299255,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK23,sK24,X2,X3,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,sK29,sK27)
| ~ eqangle(X0,X1,sK29,sK27,X2,X3,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297342]) ).
tcf(c_299256,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK29,sK27,X2,X3,sK29,sK27)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_299280,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK28,sK29,X4,X5,X2,X3)
| ~ eqangle(sK28,sK29,X0,X1,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_299282,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK28,sK29,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK28,sK29,X4,X5) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_299305,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(sK22,sK23,sK23,sK24,X2,X3,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,X0,X1,sK27,sK29)
| ~ eqangle(X0,X1,sK27,sK29,X2,X3,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_297373]) ).
tcf(c_299306,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,sK27,sK29,X2,X3,sK27,sK29)
| ~ para(X0,X1,X2,X3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_300654,plain,
! [X0: $i,X1: $i] :
( para(sK27,sK29,X0,X1)
| ~ para(X0,X1,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_300655,plain,
( para(sK27,sK29,sK23,sK23)
| ~ para(sK23,sK23,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_300654]) ).
tcf(c_301021,plain,
( eqangle(sK28,sK29,sK29,sK27,sK28,sK29,sK29,sK27)
| ~ para(sK28,sK29,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_297089]) ).
tcf(c_302476,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK27,sK29,X2,X3)
| ~ para(X0,X1,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_302477,plain,
( eqangle(sK23,sK23,sK23,sK23,sK27,sK29,sK23,sK23)
| ~ para(sK23,sK23,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_302476]) ).
tcf(c_303272,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK29)
| ~ eqangle(X0,X1,sK27,sK29,sK28,sK29,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_297350]) ).
tcf(c_303274,plain,
( para(sK23,sK23,sK28,sK29)
| ~ eqangle(sK23,sK23,sK27,sK29,sK28,sK29,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_303272]) ).
tcf(c_303363,plain,
( eqangle(sK29,sK27,sK28,sK29,sK29,sK27,sK28,sK29)
| ~ eqangle(sK28,sK29,sK29,sK27,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297424]) ).
tcf(c_303364,plain,
( eqangle(sK29,sK28,sK29,sK27,sK28,sK29,sK29,sK27)
| ~ eqangle(sK28,sK29,sK29,sK27,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297083]) ).
tcf(c_304788,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( eqangle(X0,X1,X2,X3,sK29,sK27,X2,X3)
| ~ para(X0,X1,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_304789,plain,
( eqangle(sK23,sK23,sK23,sK23,sK29,sK27,sK23,sK23)
| ~ para(sK23,sK23,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_304788]) ).
tcf(c_304821,plain,
! [X0: $i,X1: $i] :
( perp(X0,X1,sK29,sK27)
| ~ cong(X0,sK27,X1,sK27)
| ~ cong(X0,sK29,X1,sK29) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_304822,plain,
( perp(sK23,sK23,sK29,sK27)
| ~ cong(sK23,sK27,sK23,sK27)
| ~ cong(sK23,sK29,sK23,sK29) ),
inference(instantiation,[status(thm)],[c_304821]) ).
tcf(c_305958,plain,
! [X0: $i,X1: $i] :
( para(X0,X1,sK28,sK27)
| ~ eqangle(X0,X1,sK29,sK27,sK28,sK27,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297194]) ).
tcf(c_305960,plain,
( para(sK23,sK23,sK28,sK27)
| ~ eqangle(sK23,sK23,sK29,sK27,sK28,sK27,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_305958]) ).
tcf(c_306193,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK23,sK24,X0,X1,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK27,sK29,sK27,sK29)
| ~ eqangle(sK27,sK29,sK27,sK29,X0,X1,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_299305]) ).
tcf(c_306194,plain,
( eqangle(sK22,sK23,sK23,sK24,sK23,sK23,sK27,sK29)
| ~ eqangle(sK27,sK29,sK27,sK29,sK23,sK23,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK27,sK29,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_306193]) ).
tcf(c_307188,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK27,sK29,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK27,sK29,X4,X5) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_307189,plain,
( eqangle(sK23,sK23,sK27,sK29,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK27,sK29,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_307188]) ).
tcf(c_307535,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(X0,X1,sK29,sK27,X2,X3,X4,X5)
| ~ eqangle(X0,X1,X2,X3,sK29,sK27,X4,X5) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_307536,plain,
( eqangle(sK23,sK23,sK29,sK27,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK23,sK23,sK23,sK29,sK27,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_307535]) ).
tcf(c_307762,plain,
! [X0: $i,X1: $i] :
( para(sK23,sK24,sK29,sK27)
| ~ para(X0,X1,sK29,sK27)
| ~ eqangle(sK23,sK24,sK29,sK27,X0,X1,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_298360]) ).
tcf(c_307763,plain,
( para(sK23,sK24,sK29,sK27)
| ~ para(sK23,sK23,sK29,sK27)
| ~ eqangle(sK23,sK24,sK29,sK27,sK23,sK23,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_307762]) ).
tcf(c_308531,plain,
! [X0: $i,X1: $i,X2: $i] :
( midp(sK23,X2,sK39)
| ~ coll(sK23,X2,sK39)
| ~ midp(X0,X2,X1)
| ~ para(X0,sK23,X1,sK39) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_308532,plain,
( midp(sK23,sK23,sK39)
| ~ midp(sK23,sK23,sK23)
| ~ coll(sK23,sK23,sK39)
| ~ para(sK23,sK23,sK23,sK39) ),
inference(instantiation,[status(thm)],[c_308531]) ).
tcf(c_308567,plain,
( eqangle(sK28,sK29,sK29,sK27,sK29,sK28,sK29,sK27)
| ~ eqangle(sK29,sK28,sK29,sK27,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297441]) ).
tcf(c_309016,plain,
( eqangle(sK27,sK29,sK28,sK29,sK29,sK27,sK28,sK29)
| ~ eqangle(sK29,sK27,sK28,sK29,sK29,sK27,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_297423]) ).
tcf(c_311003,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( eqangle(sK23,sK24,sK29,sK27,X2,X3,X4,X5)
| ~ eqangle(sK23,sK24,sK29,sK27,X0,X1,sK29,sK27)
| ~ eqangle(X0,X1,sK29,sK27,X2,X3,X4,X5) ),
inference(instantiation,[status(thm)],[c_298673]) ).
tcf(c_311004,plain,
( eqangle(sK23,sK24,sK29,sK27,sK23,sK23,sK23,sK23)
| ~ eqangle(sK23,sK24,sK29,sK27,sK23,sK23,sK29,sK27)
| ~ eqangle(sK23,sK23,sK29,sK27,sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_311003]) ).
tcf(c_315343,plain,
! [X0: $i] :
( midp(sK23,sK39,X0)
| ~ coll(sK23,sK39,X0)
| ~ cong(sK23,sK39,sK23,X0) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_315345,plain,
! [X0: $i] :
( midp(sK23,sK39,X0)
| ~ midp(sK23,X0,sK39) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_315346,plain,
( midp(sK23,sK39,sK23)
| ~ midp(sK23,sK23,sK39) ),
inference(instantiation,[status(thm)],[c_315345]) ).
tcf(c_315355,plain,
! [X0: $i] :
( coll(sK23,X0,sK39)
| ~ para(sK23,X0,sK23,sK39) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_315369,plain,
! [X0: $i,X1: $i] :
( coll(sK23,X1,sK39)
| ~ coll(sK39,X0,sK23)
| ~ coll(sK39,X0,X1) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_315370,plain,
( coll(sK23,sK23,sK39)
| ~ coll(sK39,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_315369]) ).
tcf(c_315495,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X0,X1,X2,sK39)
| ~ para(X0,X1,sK39,X2) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_315496,plain,
( para(sK23,sK23,sK23,sK39)
| ~ para(sK23,sK23,sK39,sK23) ),
inference(instantiation,[status(thm)],[c_315495]) ).
tcf(c_315500,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( para(X0,X1,X4,sK39)
| ~ eqangle(X0,X1,X2,X3,X4,sK39,X2,X3) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_316988,plain,
( eqangle(sK29,sK27,sK28,sK29,sK29,sK27,sK29,sK28)
| ~ eqangle(sK28,sK29,sK29,sK27,sK29,sK28,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_299280]) ).
tcf(c_317138,plain,
( eqangle(sK28,sK27,sK29,sK27,sK28,sK27,sK27,sK29)
| ~ eqangle(sK29,sK27,sK28,sK27,sK27,sK29,sK28,sK27) ),
inference(instantiation,[status(thm)],[c_297402]) ).
tcf(c_317263,plain,
( eqangle(sK28,sK29,sK27,sK29,sK28,sK29,sK29,sK27)
| ~ eqangle(sK27,sK29,sK28,sK29,sK29,sK27,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_297084]) ).
tcf(c_320158,plain,
( eqangle(sK28,sK29,sK28,sK29,sK27,sK29,sK29,sK27)
| ~ eqangle(sK28,sK29,sK27,sK29,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_299282]) ).
tcf(c_320161,plain,
( eqangle(sK28,sK29,sK29,sK27,sK28,sK29,sK27,sK29)
| ~ eqangle(sK28,sK29,sK27,sK29,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297441]) ).
tcf(c_321306,plain,
( eqangle(sK28,sK27,sK27,sK29,sK28,sK27,sK29,sK27)
| ~ eqangle(sK28,sK27,sK29,sK27,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_297451]) ).
tcf(c_321624,plain,
( midp(sK23,sK39,sK39)
| ~ coll(sK23,sK39,sK39)
| ~ cong(sK23,sK39,sK23,sK39) ),
inference(instantiation,[status(thm)],[c_315343]) ).
tcf(c_321625,plain,
! [X0: $i] :
( cong(sK23,sK39,sK23,sK39)
| ~ midp(sK39,sK23,X0)
| ~ perp(sK23,sK23,sK23,X0) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_321626,plain,
( cong(sK23,sK39,sK23,sK39)
| ~ midp(sK39,sK23,sK23)
| ~ perp(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_321625]) ).
tcf(c_321645,plain,
! [X0: $i] :
( coll(sK39,X0,sK23)
| ~ midp(sK39,X0,sK23) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_321646,plain,
( coll(sK39,sK23,sK23)
| ~ midp(sK39,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_321645]) ).
tcf(c_321929,plain,
! [X0: $i,X1: $i,X2: $i] :
( para(X1,X2,sK39,X0)
| ~ para(sK39,X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_321930,plain,
( para(sK23,sK23,sK39,sK23)
| ~ para(sK39,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_321929]) ).
tcf(c_322033,plain,
! [X0: $i,X1: $i] :
( eqangle(sK23,sK39,sK23,X1,X0,sK39,X0,X1)
| ~ midp(X1,sK39,X1)
| ~ circle(X0,sK23,sK39,X1) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_322034,plain,
( eqangle(sK23,sK39,sK23,sK23,sK23,sK39,sK23,sK23)
| ~ midp(sK23,sK39,sK23)
| ~ circle(sK23,sK23,sK39,sK23) ),
inference(instantiation,[status(thm)],[c_322033]) ).
tcf(c_322279,plain,
! [X0: $i,X1: $i,X2: $i] :
( circle(X0,X1,sK39,X2)
| ~ cong(X0,X1,X0,sK39)
| ~ cong(X0,X1,X0,X2) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_322280,plain,
( circle(sK23,sK23,sK39,sK23)
| ~ cong(sK23,sK23,sK23,sK39)
| ~ cong(sK23,sK23,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_322279]) ).
tcf(c_322339,plain,
! [X0: $i,X1: $i] :
( para(X0,sK39,X0,sK39)
| ~ eqangle(X0,sK39,X0,X1,X0,sK39,X0,X1) ),
inference(instantiation,[status(thm)],[c_315500]) ).
tcf(c_322341,plain,
( para(sK23,sK39,sK23,sK39)
| ~ eqangle(sK23,sK39,sK23,sK23,sK23,sK39,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_322339]) ).
tcf(c_322841,plain,
! [X0: $i] :
( cong(sK23,X0,sK23,sK39)
| ~ midp(sK23,X0,sK39) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_322842,plain,
( cong(sK23,sK23,sK23,sK39)
| ~ midp(sK23,sK23,sK39) ),
inference(instantiation,[status(thm)],[c_322841]) ).
tcf(c_325897,plain,
( eqangle(sK22,sK23,sK23,sK24,sK27,sK29,sK29,sK27)
| ~ eqangle(sK28,sK29,sK28,sK29,sK27,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_297342]) ).
tcf(c_325932,plain,
( eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK27,sK29)
| ~ eqangle(sK28,sK29,sK29,sK27,sK28,sK29,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_297373]) ).
tcf(c_326056,plain,
( eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK29,sK27)
| ~ eqangle(sK28,sK27,sK27,sK29,sK28,sK27,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29) ),
inference(instantiation,[status(thm)],[c_297342]) ).
tcf(c_327113,plain,
! [X0: $i,X1: $i] :
( eqangle(sK27,sK29,sK29,sK27,X0,X1,sK29,sK27)
| ~ para(sK27,sK29,X0,X1) ),
inference(instantiation,[status(thm)],[c_299256]) ).
tcf(c_327115,plain,
( eqangle(sK27,sK29,sK29,sK27,sK23,sK23,sK29,sK27)
| ~ para(sK27,sK29,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_327113]) ).
tcf(c_327117,plain,
! [X0: $i,X1: $i] :
( eqangle(sK27,sK29,sK27,sK29,X0,X1,sK27,sK29)
| ~ para(sK27,sK29,X0,X1) ),
inference(instantiation,[status(thm)],[c_299306]) ).
tcf(c_327119,plain,
( eqangle(sK27,sK29,sK27,sK29,sK23,sK23,sK27,sK29)
| ~ para(sK27,sK29,sK23,sK23) ),
inference(instantiation,[status(thm)],[c_327117]) ).
tcf(c_331283,plain,
! [X0: $i,X1: $i] :
( eqangle(sK22,sK23,sK23,sK24,X0,X1,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK27,sK29,sK29,sK27)
| ~ eqangle(sK27,sK29,sK29,sK27,X0,X1,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_299255]) ).
tcf(c_331289,plain,
( eqangle(sK22,sK23,sK23,sK24,sK23,sK23,sK29,sK27)
| ~ eqangle(sK27,sK29,sK29,sK27,sK23,sK23,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK27,sK29,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_331283]) ).
tcf(c_379828,plain,
! [X0: $i] :
( midp(X0,sK28,sK28)
| ~ midp(X0,sK29,sK29)
| ~ para(sK29,sK28,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_297971]) ).
tcf(c_379829,plain,
( midp(sK23,sK28,sK28)
| ~ midp(sK23,sK29,sK29)
| ~ para(sK29,sK28,sK29,sK28) ),
inference(instantiation,[status(thm)],[c_379828]) ).
tcf(c_380264,plain,
( eqangle(sK23,sK24,sK22,sK23,sK29,sK27,sK29,sK28)
| ~ eqangle(sK29,sK27,sK28,sK29,sK29,sK27,sK29,sK28)
| ~ eqangle(sK23,sK24,sK22,sK23,sK29,sK27,sK28,sK29) ),
inference(instantiation,[status(thm)],[c_298237]) ).
tcf(c_384049,plain,
( coll(sK23,sK39,sK39)
| ~ para(sK23,sK39,sK23,sK39) ),
inference(instantiation,[status(thm)],[c_315355]) ).
tcf(c_385523,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK29,sK27,sK28,sK27,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK29,sK27)
| ~ eqangle(X0,X1,sK29,sK27,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_297957]) ).
tcf(c_385524,plain,
( eqangle(sK23,sK23,sK29,sK27,sK28,sK27,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK29,sK27)
| ~ eqangle(sK23,sK23,sK29,sK27,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_385523]) ).
tcf(c_386221,plain,
! [X0: $i,X1: $i] :
( eqangle(X0,X1,sK27,sK29,sK28,sK29,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK27,sK29)
| ~ eqangle(X0,X1,sK27,sK29,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_298776]) ).
tcf(c_386223,plain,
( eqangle(sK23,sK23,sK27,sK29,sK28,sK29,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK27,sK29)
| ~ eqangle(sK23,sK23,sK27,sK29,sK22,sK23,sK23,sK24) ),
inference(instantiation,[status(thm)],[c_386221]) ).
tcf(c_387036,plain,
( para(sK22,sK23,sK29,sK28)
| ~ para(sK23,sK24,sK29,sK27)
| ~ eqangle(sK22,sK23,sK29,sK28,sK23,sK24,sK29,sK27) ),
inference(instantiation,[status(thm)],[c_298268]) ).
tcf(c_399670,plain,
! [X0: $i] :
( cong(X0,sK28,X0,sK28)
| ~ midp(X0,sK28,sK28) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_399671,plain,
( cong(sK23,sK28,sK23,sK28)
| ~ midp(sK23,sK28,sK28) ),
inference(instantiation,[status(thm)],[c_399670]) ).
fof(f251,definition,
! [X5,X6,X7,X2,X1,X0] :
( ~ sP0(X5,X6,X7,X2,X1,X0)
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f252,definition,
! [X7,X5,X6,X2,X1,X0] :
( ~ sP1(X7,X5,X6,X2,X1,X0)
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f253,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( perp(X3,X0,X19,X7)
& midp(X19,X3,X0)
& perp(X2,X0,X18,X7)
& midp(X18,X2,X0)
& perp(X2,X3,X17,X7)
& midp(X17,X2,X3)
& perp(X3,X2,X16,X6)
& midp(X16,X3,X2)
& perp(X1,X2,X15,X6)
& midp(X15,X1,X2)
& perp(X1,X3,X14,X6)
& midp(X14,X1,X3)
& perp(X3,X1,X13,X5)
& midp(X13,X3,X1)
& perp(X0,X1,X12,X5)
& midp(X12,X0,X1)
& perp(X0,X3,X11,X5)
& midp(X11,X0,X3)
& perp(X1,X2,X10,X4)
& midp(X10,X1,X2)
& perp(X0,X2,X9,X4)
& midp(X9,X0,X2)
& perp(X0,X1,X8,X4)
& midp(X8,X0,X1)
& perp(X1,X2,X0,X3)
& perp(X0,X2,X1,X3)
& perp(X0,X1,X2,X3)
& ( ~ eqangle(X0,X1,X1,X2,X6,X7,X7,X5)
| sP0(X5,X6,X7,X2,X1,X0)
| sP1(X7,X5,X6,X2,X1,X0)
| ( ~ eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) )
| ( ~ eqangle(X1,X0,X0,X2,X6,X7,X7,X5)
& ~ eqangle(X0,X1,X1,X2,X6,X5,X5,X7) )
| ( ~ eqangle(X1,X0,X0,X2,X7,X6,X6,X5)
& ~ eqangle(X0,X1,X1,X2,X6,X7,X7,X5) )
| ~ eqangle(X1,X0,X0,X2,X7,X6,X6,X5) ) ),
inference(definition_folding,[],[f250,f252,f251]) ).
fof(f275,plain,
! [X5,X6,X7,X2,X1,X0] :
( ~ sP0(X5,X6,X7,X2,X1,X0)
| ( ~ eqangle(X1,X0,X0,X2,X6,X5,X5,X7)
& ~ eqangle(X0,X1,X1,X2,X7,X6,X6,X5) ) ),
inference(nnf_transformation,[],[f251]) ).
fof(f276,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sP0(X0,X1,X2,X3,X4,X5)
| ( ~ eqangle(X4,X5,X5,X3,X1,X0,X0,X2)
& ~ eqangle(X5,X4,X4,X3,X2,X1,X1,X0) ) ),
inference(rectify,[],[f275]) ).
fof(f394,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sP0(X0,X1,X2,X3,X4,X5)
| ~ eqangle(X5,X4,X4,X3,X2,X1,X1,X0) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ sP0(X5,X4,X3,X2,X1,X0)
| ~ eqangle(X0,X1,X1,X2,X3,X4,X4,X5) ),
inference(cnf_transformation,[],[f394]) ).
tcf(c_458,plain,
( ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK28,sK27)
| ~ eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27) ),
inference(backward_subsumption_resolution,[status(thm)],[c_449,c_164]) ).
tcf(c_4554,plain,
( ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27)
| ~ eqangle(sK22,sK23,sK23,sK24,sK29,sK28,sK28,sK27)
| ~ eqangle(sK23,sK22,sK22,sK24,sK29,sK28,sK28,sK27) ),
inference(demodulation,[status(thm)],[c_458]) ).
tcf(c_391091,plain,
( ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK27,sK27,sK29)
| ~ eqangle(sK22,sK23,sK23,sK24,sK28,sK29,sK29,sK27) ),
inference(global_subsumption_just,[status(thm)],[c_4554,c_189,c_187,c_181,c_179,c_177,c_206,c_215,c_458,c_6252,c_6250,c_6247,c_6246,c_6243,c_6273,c_6268,c_6305,c_6315,c_6385,c_6640,c_6676,c_6677,c_6682,c_7063,c_7078,c_7140,c_7239,c_7745,c_7746,c_7775,c_7776,c_7796,c_7804,c_9383,c_10232,c_10818,c_11211,c_11242,c_11272,c_11543,c_11563,c_11586,c_11783,c_11841,c_12696,c_13289,c_13687,c_14252,c_15952,c_15954,c_16030,c_17759,c_18574,c_20420,c_20542,c_22955,c_24902,c_24915,c_25600,c_25652,c_27063,c_27712,c_28530,c_29711,c_29713,c_30686,c_30975,c_34929,c_34931,c_34933,c_38570,c_85377,c_118824,c_123485,c_123545,c_123681,c_123853,c_124041,c_124319,c_124393,c_124394,c_124542,c_127040,c_127349,c_128840,c_128918,c_128920,c_129296,c_129297,c_130408,c_132334,c_132349,c_132453,c_138319,c_139162,c_143141,c_149795,c_152142,c_164512,c_167222,c_167441,c_168971,c_169058,c_169146,c_171963,c_179660,c_179797,c_182796,c_187370,c_193195,c_194095,c_202059,c_203597,c_221007,c_243132,c_243136,c_245162,c_246161,c_249115,c_256658,c_259983,c_279484,c_298154,c_298251,c_298331,c_301021,c_302477,c_303274,c_303364,c_303363,c_304789,c_304822,c_305960,c_307189,c_307536,c_307763,c_308532,c_308567,c_309016,c_311004,c_315346,c_315370,c_315496,c_316988,c_317138,c_317263,c_320161,c_321306,c_321624,c_321626,c_321646,c_321930,c_322034,c_322280,c_322341,c_322842,c_325932,c_326056,c_380264,c_384049,c_385524,c_386223,c_387036]) ).
tcf(c_399672,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_399671,c_391091,c_384049,c_379829,c_331289,c_327119,c_327115,c_325897,c_322842,c_322341,c_322280,c_322034,c_321930,c_321646,c_321626,c_321624,c_320158,c_317263,c_315496,c_315370,c_315346,c_309016,c_308532,c_306194,c_303363,c_301021,c_300655,c_298154,c_290584,c_245162,c_221007,c_202939,c_202059,c_193195,c_182776,c_182775,c_180433,c_180432,c_172091,c_172090,c_169146,c_164512,c_162454,c_156126,c_152142,c_149800,c_149795,c_143141,c_143142,c_139162,c_129297,c_129296,c_127929,c_127040,c_126171,c_125897,c_124432,c_124093,c_118824,c_34933,c_34931,c_31876,c_29713,c_29711,c_28530,c_27712,c_27063,c_25600,c_24914,c_24902,c_22955,c_22097,c_20420,c_18574,c_17759,c_14252,c_13687,c_13289,c_12696,c_11841,c_11783,c_11563,c_11543,c_11272,c_11242,c_10818,c_10232,c_9383,c_7796,c_7776,c_7775,c_7746,c_7745,c_7239,c_7078,c_6682,c_6677,c_6676,c_6315,c_6268,c_6273,c_6243,c_6246,c_6247,c_6250,c_215,c_206,c_177,c_179,c_181,c_187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO564+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n020.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 12:25:50 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 198.13/27.54 % SZS status Started for theBenchmark.p
% 198.13/27.54 % SZS status Theorem for theBenchmark.p
% 198.13/27.54
% 198.13/27.54 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 198.13/27.54
% 198.13/27.54 % ------ iProver source info
% 198.13/27.54
% 198.13/27.54 % git: date: 2026-07-19 20:42:38 +0200
% 198.13/27.54 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 198.13/27.54 % git: non_committed_changes: false
% 198.13/27.54
% 198.13/27.54 % ------ Parsing...
% 198.13/27.54 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 198.13/27.54
% 198.13/27.54 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 198.13/27.54
% 198.13/27.54 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 198.13/27.54
% 198.13/27.54 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 198.13/27.54 % ------ Proving...
% 198.13/27.54 % ------ Problem Properties
% 198.13/27.54
% 198.13/27.54 %
% 198.13/27.54 % clauses 141
% 198.13/27.54 % conjectures 27
% 198.13/27.54 % EPR 104
% 198.13/27.54 % Horn 131
% 198.13/27.54 % unary 27
% 198.13/27.54 % binary 37
% 198.13/27.54 % lits 363
% 198.13/27.54 % lits eq 4
% 198.13/27.54 % fd_pure 0
% 198.13/27.54 % fd_pseudo 0
% 198.13/27.54 % fd_cond 0
% 198.13/27.54 % fd_pseudo_cond 4
% 198.13/27.54 % AC symbols 0
% 198.13/27.54
% 198.13/27.54 % ------ Schedule dynamic 5 is on
% 198.13/27.54
% 198.13/27.54 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 198.13/27.54
% 198.13/27.54
% 198.13/27.54 % ------
% 198.13/27.54 % Current options:
% 198.13/27.54 % ------
% 198.13/27.54
% 198.13/27.54
% 198.13/27.54 %
% 198.13/27.54
% 198.13/27.54 % ------ Proving...
% 198.13/27.54 % Proof_search_loop: time out after: 9806 full_loop iterations
% 198.13/27.54
% 198.13/27.54 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 198.13/27.54
% 198.13/27.54
% 198.13/27.54 % ------
% 198.13/27.54 % Current options:
% 198.13/27.54 % ------
% 198.13/27.54
% 198.13/27.54
% 198.13/27.54 %
% 198.13/27.54
% 198.13/27.54 % ------ Proving...
% 198.13/27.54 % Proof_search_loop: time out after: 11178 full_loop iterations
% 198.13/27.54
% 198.13/27.54 % ------ Option_1: Negative Selections Time Limit: 35.
% 198.13/27.54
% 198.13/27.54
% 198.13/27.54 % ------
% 198.13/27.54 % Current options:
% 198.13/27.54 % ------
% 198.13/27.54
% 198.13/27.54
% 198.13/27.54 %
% 198.13/27.54
% 198.13/27.54 % ------ Proving...
% 198.13/27.54 %
% 198.13/27.54
% 198.13/27.54 % SZS status Theorem for theBenchmark.p
% 198.13/27.54
% 198.13/27.54 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 198.13/27.54
% 198.13/27.54
%------------------------------------------------------------------------------