%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO168+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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:20:03 PM UTC 2026
% Result : Theorem 262.12s 45.63s
% Output : CNFRefutation 233.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 25
% Syntax : Number of formulae : 878 ( 172 unt; 0 def)
% Number of atoms : 2617 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 2943 (1204 ~;1695 |; 24 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 7 usr; 4 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-3 aty)
% Number of variables : 820 ( 0 sgn 814 !; 6 ?; 601 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( colinear(d,e,f,m)
& colinear(a,b,c,l) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption1) ).
fof(f2,axiom,
( colinear(c,e,g,o)
& colinear(b,f,g,n) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption2) ).
fof(f3,axiom,
( colinear(a,e,h,q)
& colinear(b,d,h,p) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption3) ).
fof(f4,axiom,
( colinear(a,f,i,s)
& colinear(c,d,i,r) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption4) ).
fof(f5,axiom,
( incident(a,m)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goalam) ).
fof(f6,axiom,
( incident(b,m)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goalbm) ).
fof(f7,axiom,
( incident(c,m)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goalcm) ).
fof(f8,axiom,
( incident(d,l)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goaldl) ).
fof(f9,axiom,
( incident(e,l)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goalel) ).
fof(f10,axiom,
( incident(f,l)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goalfl) ).
fof(f11,axiom,
! [X0] :
( ( incident(i,X0)
& incident(h,X0)
& incident(g,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal4) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( colinear(X0,X1,X2,X3)
=> incident(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity_elimination1) ).
fof(f13,axiom,
! [X0,X1,X2,X3] :
( colinear(X0,X1,X2,X3)
=> incident(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity_elimination2) ).
fof(f14,axiom,
! [X0,X1,X2,X3] :
( colinear(X0,X1,X2,X3)
=> incident(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity_elimination3) ).
fof(f15,axiom,
! [X0,X1] :
( incident(X0,X1)
=> point_equal(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_point_equal) ).
fof(f16,axiom,
! [X0,X1] :
( point_equal(X0,X1)
=> point_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_point_equal) ).
fof(f17,axiom,
! [X0,X1,X2] :
( ( point_equal(X1,X2)
& point_equal(X0,X1) )
=> point_equal(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_point_equal) ).
fof(f18,axiom,
! [X0,X1] :
( incident(X0,X1)
=> line_equal(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_line_equal) ).
fof(f19,axiom,
! [X0,X1] :
( line_equal(X0,X1)
=> line_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_line_equal) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ( incident(X1,X2)
& point_equal(X0,X1) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pcon) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( line_equal(X1,X2)
& incident(X0,X1) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcon) ).
fof(f23,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ( colinear(X0,X5,X8,X16)
& colinear(X2,X3,X8,X15)
& colinear(X0,X4,X7,X14)
& colinear(X1,X3,X7,X13)
& colinear(X2,X4,X6,X12)
& colinear(X1,X5,X6,X11)
& colinear(X3,X4,X5,X10)
& colinear(X0,X1,X2,X9) )
=> ( line_equal(X15,X16)
| line_equal(X13,X14)
| line_equal(X11,X12)
| ? [X17] : colinear(X6,X7,X8,X17) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pappus1) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( ( incident(X3,X1)
& incident(X3,X0)
& incident(X2,X1)
& incident(X2,X0) )
=> ( line_equal(X0,X1)
| point_equal(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique) ).
fof(f25,axiom,
! [X0,X1] :
( ( point_equal(X1,X1)
& point_equal(X0,X0) )
=> ? [X2] :
( incident(X1,X2)
& incident(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',line) ).
fof(f27,conjecture,
goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f28,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f30,plain,
~ goal,
inference(flattening,[],[f28]) ).
fof(f31,plain,
( ~ incident(a,m)
| goal ),
inference(ennf_transformation,[],[f5]) ).
fof(f32,plain,
( ~ incident(b,m)
| goal ),
inference(ennf_transformation,[],[f6]) ).
fof(f33,plain,
( ~ incident(c,m)
| goal ),
inference(ennf_transformation,[],[f7]) ).
fof(f34,plain,
( ~ incident(d,l)
| goal ),
inference(ennf_transformation,[],[f8]) ).
fof(f35,plain,
( ~ incident(e,l)
| goal ),
inference(ennf_transformation,[],[f9]) ).
fof(f36,plain,
( ~ incident(f,l)
| goal ),
inference(ennf_transformation,[],[f10]) ).
fof(f37,plain,
! [X0] :
( ~ incident(i,X0)
| ~ incident(h,X0)
| ~ incident(g,X0)
| goal ),
inference(ennf_transformation,[],[f11]) ).
fof(f38,plain,
! [X0] :
( ~ incident(i,X0)
| ~ incident(h,X0)
| ~ incident(g,X0)
| goal ),
inference(flattening,[],[f37]) ).
fof(f39,plain,
! [X0,X1,X2,X3] :
( ~ colinear(X0,X1,X2,X3)
| incident(X0,X3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f40,plain,
! [X0,X1,X2,X3] :
( ~ colinear(X0,X1,X2,X3)
| incident(X1,X3) ),
inference(ennf_transformation,[],[f13]) ).
fof(f41,plain,
! [X0,X1,X2,X3] :
( ~ colinear(X0,X1,X2,X3)
| incident(X2,X3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f42,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| point_equal(X0,X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f43,plain,
! [X0,X1] :
( ~ point_equal(X0,X1)
| point_equal(X1,X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f45,plain,
! [X0,X1,X2] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(flattening,[],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line_equal(X1,X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f47,plain,
! [X0,X1] :
( ~ line_equal(X0,X1)
| line_equal(X1,X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f50,plain,
! [X0,X1,X2] :
( ~ incident(X1,X2)
| ~ point_equal(X0,X1)
| incident(X0,X2) ),
inference(ennf_transformation,[],[f21]) ).
fof(f51,plain,
! [X0,X1,X2] :
( ~ incident(X1,X2)
| ~ point_equal(X0,X1)
| incident(X0,X2) ),
inference(flattening,[],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(flattening,[],[f52]) ).
fof(f54,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ~ colinear(X0,X5,X8,X16)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X0,X1,X2,X9)
| line_equal(X15,X16)
| line_equal(X13,X14)
| line_equal(X11,X12)
| ? [X17] : colinear(X6,X7,X8,X17) ),
inference(ennf_transformation,[],[f23]) ).
fof(f55,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ~ colinear(X0,X5,X8,X16)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X0,X1,X2,X9)
| line_equal(X15,X16)
| line_equal(X13,X14)
| line_equal(X11,X12)
| ? [X17] : colinear(X6,X7,X8,X17) ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
! [X0,X1,X2,X3] :
( ~ incident(X3,X1)
| ~ incident(X3,X0)
| ~ incident(X2,X1)
| ~ incident(X2,X0)
| line_equal(X0,X1)
| point_equal(X2,X3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( ~ incident(X3,X1)
| ~ incident(X3,X0)
| ~ incident(X2,X1)
| ~ incident(X2,X0)
| line_equal(X0,X1)
| point_equal(X2,X3) ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| ? [X2] :
( incident(X1,X2)
& incident(X0,X2) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f59,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| ? [X2] :
( incident(X1,X2)
& incident(X0,X2) ) ),
inference(flattening,[],[f58]) ).
fof(f62,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
( ~ colinear(X0,X5,X8,X16)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X0,X1,X2,X9)
| line_equal(X15,X16)
| line_equal(X13,X14)
| line_equal(X11,X12)
| colinear(X6,X7,X8,sK0(X6,X7,X8)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X17,sK0(X6,X7,X8))],[f55]) ).
fof(f63,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| ( incident(X1,sK1(X0,X1))
& incident(X0,sK1(X0,X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f59]) ).
fof(f66,plain,
colinear(d,e,f,m),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
colinear(a,b,c,l),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
colinear(c,e,g,o),
inference(cnf_transformation,[],[f2]) ).
fof(f69,plain,
colinear(b,f,g,n),
inference(cnf_transformation,[],[f2]) ).
fof(f70,plain,
colinear(a,e,h,q),
inference(cnf_transformation,[],[f3]) ).
fof(f71,plain,
colinear(b,d,h,p),
inference(cnf_transformation,[],[f3]) ).
fof(f72,plain,
colinear(a,f,i,s),
inference(cnf_transformation,[],[f4]) ).
fof(f73,plain,
colinear(c,d,i,r),
inference(cnf_transformation,[],[f4]) ).
fof(f74,plain,
( ~ incident(a,m)
| goal ),
inference(cnf_transformation,[],[f31]) ).
fof(f75,plain,
( ~ incident(b,m)
| goal ),
inference(cnf_transformation,[],[f32]) ).
fof(f76,plain,
( ~ incident(c,m)
| goal ),
inference(cnf_transformation,[],[f33]) ).
fof(f77,plain,
( ~ incident(d,l)
| goal ),
inference(cnf_transformation,[],[f34]) ).
fof(f78,plain,
( ~ incident(e,l)
| goal ),
inference(cnf_transformation,[],[f35]) ).
fof(f79,plain,
( ~ incident(f,l)
| goal ),
inference(cnf_transformation,[],[f36]) ).
fof(f80,plain,
! [X0] :
( ~ incident(i,X0)
| ~ incident(h,X0)
| ~ incident(g,X0)
| goal ),
inference(cnf_transformation,[],[f38]) ).
fof(f81,plain,
! [X2,X3,X0,X1] :
( ~ colinear(X0,X1,X2,X3)
| incident(X0,X3) ),
inference(cnf_transformation,[],[f39]) ).
fof(f82,plain,
! [X2,X3,X0,X1] :
( ~ colinear(X0,X1,X2,X3)
| incident(X1,X3) ),
inference(cnf_transformation,[],[f40]) ).
fof(f83,plain,
! [X2,X3,X0,X1] :
( ~ colinear(X0,X1,X2,X3)
| incident(X2,X3) ),
inference(cnf_transformation,[],[f41]) ).
fof(f84,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| point_equal(X0,X0) ),
inference(cnf_transformation,[],[f42]) ).
fof(f85,plain,
! [X0,X1] :
( ~ point_equal(X0,X1)
| point_equal(X1,X0) ),
inference(cnf_transformation,[],[f43]) ).
fof(f86,plain,
! [X2,X0,X1] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(cnf_transformation,[],[f45]) ).
fof(f87,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line_equal(X1,X1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f88,plain,
! [X0,X1] :
( ~ line_equal(X0,X1)
| line_equal(X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f90,plain,
! [X2,X0,X1] :
( ~ incident(X1,X2)
| ~ point_equal(X0,X1)
| incident(X0,X2) ),
inference(cnf_transformation,[],[f51]) ).
fof(f91,plain,
! [X2,X0,X1] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(cnf_transformation,[],[f53]) ).
fof(f92,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X4,X15,X5,X12,X13] :
( ~ colinear(X0,X5,X8,X16)
| ~ colinear(X2,X3,X8,X15)
| ~ colinear(X0,X4,X7,X14)
| ~ colinear(X1,X3,X7,X13)
| ~ colinear(X2,X4,X6,X12)
| ~ colinear(X1,X5,X6,X11)
| ~ colinear(X3,X4,X5,X10)
| ~ colinear(X0,X1,X2,X9)
| line_equal(X15,X16)
| line_equal(X13,X14)
| line_equal(X11,X12)
| colinear(X6,X7,X8,sK0(X6,X7,X8)) ),
inference(cnf_transformation,[],[f62]) ).
fof(f93,plain,
! [X2,X3,X0,X1] :
( ~ incident(X3,X1)
| ~ incident(X3,X0)
| ~ incident(X2,X1)
| ~ incident(X2,X0)
| line_equal(X0,X1)
| point_equal(X2,X3) ),
inference(cnf_transformation,[],[f57]) ).
fof(f94,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| incident(X1,sK1(X0,X1)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f95,plain,
! [X0,X1] :
( ~ point_equal(X1,X1)
| ~ point_equal(X0,X0)
| incident(X0,sK1(X0,X1)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f98,plain,
~ goal,
inference(cnf_transformation,[],[f30]) ).
tcf(c_49,plain,
colinear(a,b,c,l),
inference(cnf_transformation,[],[f67]) ).
tcf(c_50,plain,
colinear(d,e,f,m),
inference(cnf_transformation,[],[f66]) ).
tcf(c_51,plain,
colinear(b,f,g,n),
inference(cnf_transformation,[],[f69]) ).
tcf(c_52,plain,
colinear(c,e,g,o),
inference(cnf_transformation,[],[f68]) ).
tcf(c_53,plain,
colinear(b,d,h,p),
inference(cnf_transformation,[],[f71]) ).
tcf(c_54,plain,
colinear(a,e,h,q),
inference(cnf_transformation,[],[f70]) ).
tcf(c_55,plain,
colinear(c,d,i,r),
inference(cnf_transformation,[],[f73]) ).
tcf(c_56,plain,
colinear(a,f,i,s),
inference(cnf_transformation,[],[f72]) ).
tcf(c_57,plain,
( goal
| ~ incident(a,m) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_58,plain,
( goal
| ~ incident(b,m) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_59,plain,
( goal
| ~ incident(c,m) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_60,plain,
( goal
| ~ incident(d,l) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_61,plain,
( goal
| ~ incident(e,l) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_62,plain,
( goal
| ~ incident(f,l) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_63,plain,
! [X0: $i] :
( goal
| ~ incident(i,X0)
| ~ incident(h,X0)
| ~ incident(g,X0) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident(X0,X3)
| ~ colinear(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident(X1,X3)
| ~ colinear(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( incident(X2,X3)
| ~ colinear(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( point_equal(X0,X0)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] :
( point_equal(X1,X0)
| ~ point_equal(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( point_equal(X0,X2)
| ~ point_equal(X1,X2)
| ~ point_equal(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] :
( line_equal(X1,X1)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( line_equal(X1,X0)
| ~ line_equal(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident(X2,X1)
| ~ point_equal(X2,X0)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident(X0,X2)
| ~ line_equal(X1,X2)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_75,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,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i] :
( line_equal(X15,X9)
| line_equal(X14,X16)
| line_equal(X12,X6)
| colinear(X13,X5,X8,sK0(X13,X5,X8))
| ~ colinear(X10,X4,X7,X11)
| ~ colinear(X2,X10,X8,X15)
| ~ colinear(X2,X4,X13,X16)
| ~ colinear(X1,X10,X5,X12)
| ~ colinear(X1,X7,X13,X14)
| ~ colinear(X0,X7,X8,X9)
| ~ colinear(X0,X4,X5,X6)
| ~ colinear(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( line_equal(X1,X2)
| point_equal(X3,X0)
| ~ incident(X3,X2)
| ~ incident(X3,X1)
| ~ incident(X0,X2)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( incident(X0,sK1(X0,X1))
| ~ point_equal(X1,X1)
| ~ point_equal(X0,X0) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i] :
( incident(X1,sK1(X0,X1))
| ~ point_equal(X1,X1)
| ~ point_equal(X0,X0) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_81,negated_conjecture,
~ goal,
inference(cnf_transformation,[],[f98]) ).
tcf(c_101,plain,
! [X0: $i] :
( ~ incident(g,X0)
| ~ incident(h,X0)
| ~ incident(i,X0) ),
inference(global_subsumption_just,[status(thm)],[c_63,c_81,c_63]) ).
tcf(c_102,plain,
! [X0: $i] :
( ~ incident(i,X0)
| ~ incident(h,X0)
| ~ incident(g,X0) ),
inference(renaming,[status(thm)],[c_101]) ).
tcf(c_398,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( ~ incident(i,X0_iProver_incident_2)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(g,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_102]) ).
tcf(c_407,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X1_iProver_incident_1,sK1(X0_iProver_incident_1,X1_iProver_incident_1))
| ~ point_equal(X1_iProver_incident_1,X1_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(subtyping,[status(esa)],[c_78]) ).
tcf(c_408,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(X0_iProver_incident_1,X1_iProver_incident_1))
| ~ point_equal(X1_iProver_incident_1,X1_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(subtyping,[status(esa)],[c_77]) ).
tcf(c_409,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| ~ incident(X1_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_76]) ).
tcf(c_410,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_1: iProver_incident_1,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_1: iProver_incident_1,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_1: iProver_incident_1,X5_iProver_incident_2: iProver_incident_2,X6_iProver_incident_1: iProver_incident_1,X6_iProver_incident_2: iProver_incident_2,X7_iProver_incident_1: iProver_incident_1,X7_iProver_incident_2: iProver_incident_2,X8_iProver_incident_1: iProver_incident_1] :
( line_equal(X6_iProver_incident_2,X2_iProver_incident_2)
| line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| colinear(X7_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_1,sK0(X7_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_1))
| ~ colinear(X8_iProver_incident_1,X3_iProver_incident_1,X5_iProver_incident_1,X7_iProver_incident_2)
| ~ colinear(X2_iProver_incident_1,X8_iProver_incident_1,X6_iProver_incident_1,X6_iProver_incident_2)
| ~ colinear(X2_iProver_incident_1,X3_iProver_incident_1,X7_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(X1_iProver_incident_1,X8_iProver_incident_1,X4_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(X1_iProver_incident_1,X5_iProver_incident_1,X7_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X5_iProver_incident_1,X6_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_75]) ).
tcf(c_411,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_74]) ).
tcf(c_412,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1] :
( incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ point_equal(X1_iProver_incident_1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_73]) ).
tcf(c_414,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(X1_iProver_incident_2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_71]) ).
tcf(c_415,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_70]) ).
tcf(c_416,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1,X2_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,X2_iProver_incident_1)
| ~ point_equal(X1_iProver_incident_1,X2_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(subtyping,[status(esa)],[c_69]) ).
tcf(c_417,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( point_equal(X1_iProver_incident_1,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(subtyping,[status(esa)],[c_68]) ).
tcf(c_418,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_67]) ).
tcf(c_419,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X2_iProver_incident_1: iProver_incident_1] :
( incident(X2_iProver_incident_1,X0_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_66]) ).
tcf(c_420,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X2_iProver_incident_1: iProver_incident_1] :
( incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_65]) ).
tcf(c_421,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X2_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,X0_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_64]) ).
tcf(c_422,plain,
colinear(a,f,i,s),
inference(subtyping,[status(esa)],[c_56]) ).
tcf(c_423,plain,
colinear(c,d,i,r),
inference(subtyping,[status(esa)],[c_55]) ).
tcf(c_424,plain,
colinear(a,e,h,q),
inference(subtyping,[status(esa)],[c_54]) ).
tcf(c_425,plain,
colinear(b,d,h,p),
inference(subtyping,[status(esa)],[c_53]) ).
tcf(c_426,plain,
colinear(c,e,g,o),
inference(subtyping,[status(esa)],[c_52]) ).
tcf(c_427,plain,
colinear(b,f,g,n),
inference(subtyping,[status(esa)],[c_51]) ).
tcf(c_428,plain,
colinear(d,e,f,m),
inference(subtyping,[status(esa)],[c_50]) ).
tcf(c_429,plain,
colinear(a,b,c,l),
inference(subtyping,[status(esa)],[c_49]) ).
tcf(c_433,plain,
incident(c,l),
inference(superposition,[status(thm)],[c_429,c_419]) ).
tcf(c_434,plain,
incident(f,m),
inference(superposition,[status(thm)],[c_428,c_419]) ).
tcf(c_435,plain,
incident(g,n),
inference(superposition,[status(thm)],[c_427,c_419]) ).
tcf(c_436,plain,
incident(g,o),
inference(superposition,[status(thm)],[c_426,c_419]) ).
tcf(c_437,plain,
incident(h,p),
inference(superposition,[status(thm)],[c_425,c_419]) ).
tcf(c_438,plain,
incident(h,q),
inference(superposition,[status(thm)],[c_424,c_419]) ).
tcf(c_439,plain,
incident(i,r),
inference(superposition,[status(thm)],[c_423,c_419]) ).
tcf(c_440,plain,
incident(i,s),
inference(superposition,[status(thm)],[c_422,c_419]) ).
tcf(c_441,plain,
incident(b,l),
inference(superposition,[status(thm)],[c_429,c_420]) ).
tcf(c_442,plain,
incident(e,m),
inference(superposition,[status(thm)],[c_428,c_420]) ).
tcf(c_443,plain,
incident(f,n),
inference(superposition,[status(thm)],[c_427,c_420]) ).
tcf(c_444,plain,
incident(e,o),
inference(superposition,[status(thm)],[c_426,c_420]) ).
tcf(c_445,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_446,plain,
incident(e,q),
inference(superposition,[status(thm)],[c_424,c_420]) ).
tcf(c_447,plain,
incident(d,r),
inference(superposition,[status(thm)],[c_423,c_420]) ).
tcf(c_448,plain,
incident(f,s),
inference(superposition,[status(thm)],[c_422,c_420]) ).
tcf(c_457,plain,
incident(a,l),
inference(superposition,[status(thm)],[c_429,c_421]) ).
tcf(c_458,plain,
incident(d,m),
inference(superposition,[status(thm)],[c_428,c_421]) ).
tcf(c_459,plain,
incident(b,n),
inference(superposition,[status(thm)],[c_427,c_421]) ).
tcf(c_460,plain,
incident(c,o),
inference(superposition,[status(thm)],[c_426,c_421]) ).
tcf(c_461,plain,
incident(b,p),
inference(superposition,[status(thm)],[c_425,c_421]) ).
tcf(c_462,plain,
incident(a,q),
inference(superposition,[status(thm)],[c_424,c_421]) ).
tcf(c_463,plain,
incident(c,r),
inference(superposition,[status(thm)],[c_423,c_421]) ).
tcf(c_464,plain,
incident(a,s),
inference(superposition,[status(thm)],[c_422,c_421]) ).
tcf(c_473,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_1: iProver_incident_1,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_1: iProver_incident_1,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_1: iProver_incident_1,X5_iProver_incident_2: iProver_incident_2,X6_iProver_incident_2: iProver_incident_2] :
( line_equal(X6_iProver_incident_2,X2_iProver_incident_2)
| line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| colinear(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1,sK0(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1))
| ~ colinear(c,X1_iProver_incident_1,X5_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,X0_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_2)
| ~ colinear(b,X2_iProver_incident_1,X5_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,X0_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(a,X2_iProver_incident_1,X4_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,X1_iProver_incident_1,X3_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_429,c_410]) ).
tcf(c_490,plain,
( ~ incident(i,o)
| ~ incident(h,o) ),
inference(superposition,[status(thm)],[c_436,c_398]) ).
tcf(c_492,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| colinear(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1,sK0(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1))
| ~ colinear(c,e,X2_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,d,X1_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(b,f,X2_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,e,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_428,c_473]) ).
tcf(c_517,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,q)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| line_equal(X1_iProver_incident_2,X3_iProver_incident_2)
| colinear(X1_iProver_incident_1,h,X0_iProver_incident_1,sK0(X1_iProver_incident_1,h,X0_iProver_incident_1))
| ~ colinear(b,d,h,X4_iProver_incident_2)
| ~ colinear(c,e,X1_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(c,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(b,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_424,c_492]) ).
tcf(c_519,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2] :
( line_equal(X3_iProver_incident_2,s)
| line_equal(X2_iProver_incident_2,q)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| colinear(X0_iProver_incident_1,h,i,sK0(X0_iProver_incident_1,h,i))
| ~ colinear(c,d,i,X3_iProver_incident_2)
| ~ colinear(b,d,h,X2_iProver_incident_2)
| ~ colinear(c,e,X0_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(b,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_422,c_517]) ).
tcf(c_521,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2] :
( line_equal(n,X2_iProver_incident_2)
| line_equal(X1_iProver_incident_2,s)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X2_iProver_incident_2)
| ~ colinear(c,d,i,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_427,c_519]) ).
tcf(c_523,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(n,X1_iProver_incident_2)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_423,c_521]) ).
tcf(c_525,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,X0_iProver_incident_2)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_425,c_523]) ).
tcf(c_527,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| colinear(g,h,i,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_426,c_525]) ).
tcf(c_530,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| incident(g,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_527,c_421]) ).
tcf(c_531,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| incident(h,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_527,c_420]) ).
tcf(c_532,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| incident(i,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_527,c_419]) ).
tcf(c_534,plain,
( ~ incident(i,r)
| ~ incident(h,r)
| ~ incident(g,r) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_535,plain,
( ~ incident(i,s)
| ~ incident(h,s)
| ~ incident(g,s) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_540,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| ~ incident(i,sK0(g,h,i))
| ~ incident(h,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_530,c_398]) ).
tcf(c_541,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o) ),
inference(global_subsumption_just,[status(thm)],[c_531,c_532,c_531,c_540]) ).
tcf(c_577,plain,
incident(f,n),
inference(superposition,[status(thm)],[c_427,c_420]) ).
tcf(c_578,plain,
incident(e,o),
inference(superposition,[status(thm)],[c_426,c_420]) ).
tcf(c_579,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_580,plain,
incident(e,q),
inference(superposition,[status(thm)],[c_424,c_420]) ).
tcf(c_581,plain,
incident(d,r),
inference(superposition,[status(thm)],[c_423,c_420]) ).
tcf(c_582,plain,
incident(f,s),
inference(superposition,[status(thm)],[c_422,c_420]) ).
tcf(c_599,plain,
incident(b,n),
inference(superposition,[status(thm)],[c_427,c_421]) ).
tcf(c_601,plain,
incident(b,p),
inference(superposition,[status(thm)],[c_425,c_421]) ).
tcf(c_666,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_577,c_411]) ).
tcf(c_668,plain,
( incident(f,l)
| ~ line_equal(n,l) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_669,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ line_equal(o,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_578,c_411]) ).
tcf(c_671,plain,
( incident(e,l)
| ~ line_equal(o,l) ),
inference(instantiation,[status(thm)],[c_669]) ).
tcf(c_672,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_1: iProver_incident_1,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_1: iProver_incident_1,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_1: iProver_incident_1,X5_iProver_incident_2: iProver_incident_2,X6_iProver_incident_2: iProver_incident_2] :
( line_equal(X6_iProver_incident_2,X2_iProver_incident_2)
| line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| colinear(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1,sK0(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1))
| ~ colinear(c,X1_iProver_incident_1,X5_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,X0_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_2)
| ~ colinear(b,X2_iProver_incident_1,X5_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,X0_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(a,X2_iProver_incident_1,X4_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,X1_iProver_incident_1,X3_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_429,c_410]) ).
tcf(c_693,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(d,X1_iProver_incident_2)
| ~ incident(d,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_697,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(d,X0_iProver_incident_2)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_579,c_411]) ).
tcf(c_699,plain,
( incident(d,l)
| ~ line_equal(p,l) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_700,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ line_equal(q,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_580,c_411]) ).
tcf(c_702,plain,
( incident(e,l)
| ~ line_equal(q,l) ),
inference(instantiation,[status(thm)],[c_700]) ).
tcf(c_703,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(d,X0_iProver_incident_2)
| ~ line_equal(r,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_581,c_411]) ).
tcf(c_705,plain,
( incident(d,l)
| ~ line_equal(r,l) ),
inference(instantiation,[status(thm)],[c_703]) ).
tcf(c_706,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ line_equal(s,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_582,c_411]) ).
tcf(c_708,plain,
( incident(f,l)
| ~ line_equal(s,l) ),
inference(instantiation,[status(thm)],[c_706]) ).
tcf(c_718,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_599,c_411]) ).
tcf(c_722,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_601,c_411]) ).
tcf(c_724,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(f,X1_iProver_incident_2)
| ~ incident(f,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_763,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| colinear(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1,sK0(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1))
| ~ colinear(c,e,X2_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,d,X1_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(b,f,X2_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,e,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_428,c_672]) ).
tcf(c_830,plain,
incident(i,r),
inference(resolution,[status(thm)],[c_419,c_423]) ).
tcf(c_831,plain,
incident(i,s),
inference(resolution,[status(thm)],[c_419,c_422]) ).
tcf(c_833,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,q)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| line_equal(X1_iProver_incident_2,X3_iProver_incident_2)
| colinear(X1_iProver_incident_1,h,X0_iProver_incident_1,sK0(X1_iProver_incident_1,h,X0_iProver_incident_1))
| ~ colinear(b,d,h,X4_iProver_incident_2)
| ~ colinear(c,e,X1_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(c,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(b,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_424,c_763]) ).
tcf(c_836,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2] :
( line_equal(X3_iProver_incident_2,s)
| line_equal(X2_iProver_incident_2,q)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| colinear(X0_iProver_incident_1,h,i,sK0(X0_iProver_incident_1,h,i))
| ~ colinear(c,d,i,X3_iProver_incident_2)
| ~ colinear(b,d,h,X2_iProver_incident_2)
| ~ colinear(c,e,X0_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(b,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_422,c_833]) ).
tcf(c_837,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2] :
( line_equal(n,X2_iProver_incident_2)
| line_equal(X1_iProver_incident_2,s)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X2_iProver_incident_2)
| ~ colinear(c,d,i,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_427,c_836]) ).
tcf(c_838,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(n,X1_iProver_incident_2)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_423,c_837]) ).
tcf(c_842,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,X0_iProver_incident_2)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_425,c_838]) ).
tcf(c_843,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| colinear(g,h,i,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_426,c_842]) ).
tcf(c_848,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o) ),
inference(global_subsumption_just,[status(thm)],[c_843,c_532,c_531,c_540]) ).
tcf(c_853,plain,
( line_equal(p,q)
| line_equal(n,o)
| incident(d,s) ),
inference(superposition,[status(thm)],[c_848,c_703]) ).
tcf(c_888,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,r)
| ~ line_equal(X0_iProver_incident_2,r)
| ~ incident(h,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_898,plain,
( line_equal(n,o)
| incident(d,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_853,c_722]) ).
tcf(c_902,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(d,X0_iProver_incident_2)
| ~ incident(d,p)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_930,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,s)
| ~ line_equal(X0_iProver_incident_2,s)
| ~ incident(h,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_970,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ incident(f,n)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_724]) ).
tcf(c_974,plain,
( incident(d,s)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_898,c_718]) ).
tcf(c_999,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,r) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1000,plain,
( line_equal(r,l)
| ~ line_equal(l,r) ),
inference(instantiation,[status(thm)],[c_999]) ).
tcf(c_1016,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(s,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,s) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1017,plain,
( line_equal(s,l)
| ~ line_equal(l,s) ),
inference(instantiation,[status(thm)],[c_1016]) ).
tcf(c_1039,plain,
( line_equal(p,l)
| ~ line_equal(l,p) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1057,plain,
( line_equal(o,l)
| ~ line_equal(l,o) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1072,plain,
( line_equal(q,l)
| ~ line_equal(l,q) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1081,plain,
( line_equal(n,l)
| ~ line_equal(l,n) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1146,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(q,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,q) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_1558,plain,
( ~ incident(h,r)
| ~ incident(g,r) ),
inference(resolution,[status(thm)],[c_398,c_830]) ).
tcf(c_1559,plain,
( ~ incident(h,s)
| ~ incident(g,s) ),
inference(resolution,[status(thm)],[c_398,c_831]) ).
tcf(c_1767,plain,
( incident(h,s)
| ~ line_equal(p,s)
| ~ incident(h,p) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_1768,plain,
( incident(h,r)
| ~ line_equal(p,r)
| ~ incident(h,p) ),
inference(instantiation,[status(thm)],[c_888]) ).
tcf(c_1799,plain,
( incident(h,s)
| ~ line_equal(q,s)
| ~ incident(h,q) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_3232,plain,
( incident(f,o)
| ~ line_equal(n,o)
| ~ incident(f,n) ),
inference(instantiation,[status(thm)],[c_970]) ).
tcf(c_3378,plain,
( line_equal(q,p)
| ~ line_equal(p,q) ),
inference(instantiation,[status(thm)],[c_1146]) ).
tcf(c_3383,plain,
( incident(d,q)
| ~ line_equal(p,q)
| ~ incident(d,p) ),
inference(instantiation,[status(thm)],[c_902]) ).
tcf(c_11746,plain,
incident(c,l),
inference(superposition,[status(thm)],[c_429,c_419]) ).
tcf(c_11747,plain,
incident(f,m),
inference(superposition,[status(thm)],[c_428,c_419]) ).
tcf(c_11748,plain,
incident(g,n),
inference(superposition,[status(thm)],[c_427,c_419]) ).
tcf(c_11749,plain,
incident(g,o),
inference(superposition,[status(thm)],[c_426,c_419]) ).
tcf(c_11751,plain,
incident(h,q),
inference(superposition,[status(thm)],[c_424,c_419]) ).
tcf(c_11753,plain,
incident(i,s),
inference(superposition,[status(thm)],[c_422,c_419]) ).
tcf(c_11768,plain,
incident(b,l),
inference(superposition,[status(thm)],[c_429,c_420]) ).
tcf(c_11769,plain,
incident(e,m),
inference(superposition,[status(thm)],[c_428,c_420]) ).
tcf(c_11771,plain,
incident(e,o),
inference(superposition,[status(thm)],[c_426,c_420]) ).
tcf(c_11772,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_11773,plain,
incident(e,q),
inference(superposition,[status(thm)],[c_424,c_420]) ).
tcf(c_11774,plain,
incident(d,r),
inference(superposition,[status(thm)],[c_423,c_420]) ).
tcf(c_11775,plain,
incident(f,s),
inference(superposition,[status(thm)],[c_422,c_420]) ).
tcf(c_11783,plain,
incident(a,l),
inference(superposition,[status(thm)],[c_429,c_421]) ).
tcf(c_11785,plain,
incident(b,n),
inference(superposition,[status(thm)],[c_427,c_421]) ).
tcf(c_11786,plain,
incident(c,o),
inference(superposition,[status(thm)],[c_426,c_421]) ).
tcf(c_11787,plain,
incident(b,p),
inference(superposition,[status(thm)],[c_425,c_421]) ).
tcf(c_11788,plain,
incident(a,q),
inference(superposition,[status(thm)],[c_424,c_421]) ).
tcf(c_11789,plain,
incident(c,r),
inference(superposition,[status(thm)],[c_423,c_421]) ).
tcf(c_11790,plain,
incident(a,s),
inference(superposition,[status(thm)],[c_422,c_421]) ).
tcf(c_11836,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(c,X0_iProver_incident_1)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11746,c_409]) ).
tcf(c_11837,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,m)
| point_equal(f,X0_iProver_incident_1)
| ~ incident(f,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,m)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11747,c_409]) ).
tcf(c_11839,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,o)
| point_equal(g,X0_iProver_incident_1)
| ~ incident(g,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11749,c_409]) ).
tcf(c_11841,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,q)
| point_equal(h,X0_iProver_incident_1)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,q)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11751,c_409]) ).
tcf(c_11844,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(b,X0_iProver_incident_1)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11768,c_409]) ).
tcf(c_11845,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,m)
| point_equal(e,X0_iProver_incident_1)
| ~ incident(e,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,m)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11769,c_409]) ).
tcf(c_11847,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,o)
| point_equal(e,X0_iProver_incident_1)
| ~ incident(e,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11771,c_409]) ).
tcf(c_11850,plain,
( line_equal(l,q)
| point_equal(h,a)
| ~ incident(h,l)
| ~ incident(a,q)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_11841]) ).
tcf(c_11904,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(f,X0_iProver_incident_1)
| ~ incident(f,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11775,c_409]) ).
tcf(c_11912,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(a,X0_iProver_incident_1)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11783,c_409]) ).
tcf(c_11960,plain,
incident(c,l),
inference(resolution,[status(thm)],[c_419,c_429]) ).
tcf(c_11962,plain,
incident(g,n),
inference(resolution,[status(thm)],[c_419,c_427]) ).
tcf(c_11963,plain,
incident(g,o),
inference(resolution,[status(thm)],[c_419,c_426]) ).
tcf(c_11965,plain,
incident(h,q),
inference(resolution,[status(thm)],[c_419,c_424]) ).
tcf(c_11966,plain,
incident(i,r),
inference(resolution,[status(thm)],[c_419,c_423]) ).
tcf(c_11968,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(b,X0_iProver_incident_1)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11785,c_409]) ).
tcf(c_11972,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,o)
| point_equal(c,X0_iProver_incident_1)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11786,c_409]) ).
tcf(c_11978,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(b,X0_iProver_incident_1)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11787,c_409]) ).
tcf(c_11988,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(c,X0_iProver_incident_1)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_11789,c_409]) ).
tcf(c_11991,plain,
( line_equal(l,r)
| point_equal(c,a)
| ~ incident(c,l)
| ~ incident(a,r)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_11988]) ).
tcf(c_12065,plain,
( line_equal(n,l)
| point_equal(c,b)
| ~ incident(c,n)
| ~ incident(b,l) ),
inference(superposition,[status(thm)],[c_11785,c_11836]) ).
tcf(c_12070,plain,
( line_equal(s,l)
| point_equal(c,a)
| ~ incident(c,s)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_11790,c_11836]) ).
tcf(c_12103,plain,
( line_equal(o,m)
| point_equal(f,e)
| ~ incident(f,o)
| ~ incident(e,m) ),
inference(superposition,[status(thm)],[c_11771,c_11837]) ).
tcf(c_12106,plain,
( line_equal(r,m)
| point_equal(f,d)
| ~ incident(f,r)
| ~ incident(d,m) ),
inference(superposition,[status(thm)],[c_11774,c_11837]) ).
tcf(c_12141,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(n,o)
| point_equal(g,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,n) ),
inference(superposition,[status(thm)],[c_11748,c_11839]) ).
tcf(c_12143,plain,
( line_equal(n,o)
| point_equal(g,a)
| ~ incident(a,o)
| ~ incident(a,n) ),
inference(instantiation,[status(thm)],[c_12141]) ).
tcf(c_12149,plain,
( ~ incident(c,n)
| point_equal(c,b) ),
inference(global_subsumption_just,[status(thm)],[c_12065,c_81,c_62,c_441,c_668,c_12065]) ).
tcf(c_12150,plain,
( point_equal(c,b)
| ~ incident(c,n) ),
inference(renaming,[status(thm)],[c_12149]) ).
tcf(c_12162,plain,
( ~ incident(c,s)
| point_equal(c,a) ),
inference(global_subsumption_just,[status(thm)],[c_12070,c_81,c_62,c_457,c_708,c_12070]) ).
tcf(c_12163,plain,
( point_equal(c,a)
| ~ incident(c,s) ),
inference(renaming,[status(thm)],[c_12162]) ).
tcf(c_12198,plain,
( line_equal(o,l)
| point_equal(b,c)
| ~ incident(c,l)
| ~ incident(b,o) ),
inference(superposition,[status(thm)],[c_11786,c_11844]) ).
tcf(c_12200,plain,
( line_equal(q,l)
| point_equal(b,a)
| ~ incident(b,q)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_11788,c_11844]) ).
tcf(c_12201,plain,
( line_equal(r,l)
| point_equal(b,c)
| ~ incident(c,l)
| ~ incident(b,r) ),
inference(superposition,[status(thm)],[c_11789,c_11844]) ).
tcf(c_12237,plain,
( line_equal(o,m)
| point_equal(f,e)
| ~ incident(f,o) ),
inference(global_subsumption_just,[status(thm)],[c_12103,c_442,c_12103]) ).
tcf(c_12293,plain,
( line_equal(p,m)
| point_equal(e,d)
| ~ incident(e,p)
| ~ incident(d,m) ),
inference(superposition,[status(thm)],[c_11772,c_11845]) ).
tcf(c_12453,plain,
( line_equal(m,o)
| point_equal(e,f)
| ~ incident(f,o)
| ~ incident(e,m) ),
inference(superposition,[status(thm)],[c_11747,c_11847]) ).
tcf(c_12472,plain,
( line_equal(q,o)
| point_equal(e,a)
| ~ incident(e,q)
| ~ incident(a,o) ),
inference(superposition,[status(thm)],[c_11788,c_11847]) ).
tcf(c_12559,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(X0_iProver_incident_1,c)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_11960]) ).
tcf(c_12561,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(X0_iProver_incident_1,g)
| ~ incident(g,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_11962]) ).
tcf(c_12562,plain,
( line_equal(l,n)
| point_equal(a,g)
| ~ incident(g,l)
| ~ incident(a,n)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_12561]) ).
tcf(c_12567,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,q)
| point_equal(X0_iProver_incident_1,h)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,q)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_11965]) ).
tcf(c_12568,plain,
( line_equal(l,q)
| point_equal(a,h)
| ~ incident(h,l)
| ~ incident(a,q)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_12567]) ).
tcf(c_12800,plain,
( line_equal(q,s)
| point_equal(f,a)
| ~ incident(f,q)
| ~ incident(a,s) ),
inference(superposition,[status(thm)],[c_11788,c_11904]) ).
tcf(c_12857,plain,
( line_equal(s,l)
| point_equal(a,i)
| ~ incident(i,l)
| ~ incident(a,s) ),
inference(superposition,[status(thm)],[c_11753,c_11912]) ).
tcf(c_12867,plain,
( line_equal(n,l)
| point_equal(a,b)
| ~ incident(b,l)
| ~ incident(a,n) ),
inference(superposition,[status(thm)],[c_11785,c_11912]) ).
tcf(c_12868,plain,
( line_equal(o,l)
| point_equal(a,c)
| ~ incident(c,l)
| ~ incident(a,o) ),
inference(superposition,[status(thm)],[c_11786,c_11912]) ).
tcf(c_12871,plain,
( line_equal(r,l)
| point_equal(a,c)
| ~ incident(c,l)
| ~ incident(a,r) ),
inference(superposition,[status(thm)],[c_11789,c_11912]) ).
tcf(c_13084,plain,
( line_equal(p,n)
| point_equal(b,d)
| ~ incident(d,n)
| ~ incident(b,p) ),
inference(superposition,[status(thm)],[c_11772,c_11968]) ).
tcf(c_13182,plain,
( line_equal(l,o)
| point_equal(c,b)
| ~ incident(c,l)
| ~ incident(b,o) ),
inference(superposition,[status(thm)],[c_11768,c_11972]) ).
tcf(c_13187,plain,
( line_equal(q,o)
| point_equal(c,e)
| ~ incident(e,o)
| ~ incident(c,q) ),
inference(superposition,[status(thm)],[c_11773,c_11972]) ).
tcf(c_13188,plain,
( line_equal(r,o)
| point_equal(c,d)
| ~ incident(d,o)
| ~ incident(c,r) ),
inference(superposition,[status(thm)],[c_11774,c_11972]) ).
tcf(c_13269,plain,
( line_equal(o,l)
| point_equal(g,c)
| ~ incident(g,l)
| ~ incident(c,o) ),
inference(resolution,[status(thm)],[c_12559,c_11963]) ).
tcf(c_13272,plain,
( line_equal(r,l)
| point_equal(i,c)
| ~ incident(i,l)
| ~ incident(c,r) ),
inference(resolution,[status(thm)],[c_12559,c_11966]) ).
tcf(c_13297,plain,
( line_equal(l,p)
| point_equal(b,a)
| ~ incident(b,l)
| ~ incident(a,p) ),
inference(superposition,[status(thm)],[c_11783,c_11978]) ).
tcf(c_13394,plain,
incident(c,l),
inference(superposition,[status(thm)],[c_429,c_419]) ).
tcf(c_13395,plain,
incident(f,m),
inference(superposition,[status(thm)],[c_428,c_419]) ).
tcf(c_13396,plain,
incident(g,n),
inference(superposition,[status(thm)],[c_427,c_419]) ).
tcf(c_13397,plain,
incident(g,o),
inference(superposition,[status(thm)],[c_426,c_419]) ).
tcf(c_13398,plain,
incident(h,p),
inference(superposition,[status(thm)],[c_425,c_419]) ).
tcf(c_13400,plain,
incident(i,r),
inference(superposition,[status(thm)],[c_423,c_419]) ).
tcf(c_13401,plain,
incident(i,s),
inference(superposition,[status(thm)],[c_422,c_419]) ).
tcf(c_13406,plain,
point_equal(g,g),
inference(superposition,[status(thm)],[c_13396,c_418]) ).
tcf(c_13408,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a,m)
| ~ line_equal(X0_iProver_incident_2,m)
| ~ incident(a,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_13409,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,m)
| ~ line_equal(X0_iProver_incident_2,m)
| ~ incident(b,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_13410,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c,m)
| ~ line_equal(X0_iProver_incident_2,m)
| ~ incident(c,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_13414,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(i,X1_iProver_incident_2)
| ~ incident(i,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_13417,plain,
point_equal(h,h),
inference(superposition,[status(thm)],[c_13398,c_418]) ).
tcf(c_13419,plain,
incident(b,l),
inference(superposition,[status(thm)],[c_429,c_420]) ).
tcf(c_13420,plain,
incident(e,m),
inference(superposition,[status(thm)],[c_428,c_420]) ).
tcf(c_13421,plain,
incident(f,n),
inference(superposition,[status(thm)],[c_427,c_420]) ).
tcf(c_13422,plain,
incident(e,o),
inference(superposition,[status(thm)],[c_426,c_420]) ).
tcf(c_13423,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_13424,plain,
incident(e,q),
inference(superposition,[status(thm)],[c_424,c_420]) ).
tcf(c_13425,plain,
incident(d,r),
inference(superposition,[status(thm)],[c_423,c_420]) ).
tcf(c_13426,plain,
incident(f,s),
inference(superposition,[status(thm)],[c_422,c_420]) ).
tcf(c_13428,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b,m)
| ~ point_equal(b,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,m) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13429,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(c,m)
| ~ point_equal(c,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,m) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13430,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(d,l)
| ~ point_equal(d,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,l) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13431,plain,
( incident(d,l)
| ~ point_equal(d,a)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_13430]) ).
tcf(c_13432,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(e,l)
| ~ point_equal(e,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,l) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13433,plain,
( incident(e,l)
| ~ point_equal(e,a)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_13432]) ).
tcf(c_13434,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(f,l)
| ~ point_equal(f,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,l) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13435,plain,
( incident(f,l)
| ~ point_equal(f,a)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_13434]) ).
tcf(c_13436,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(i,X0_iProver_incident_2)
| ~ point_equal(i,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13437,plain,
( incident(i,l)
| ~ point_equal(i,a)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_13436]) ).
tcf(c_13438,plain,
incident(a,l),
inference(superposition,[status(thm)],[c_429,c_421]) ).
tcf(c_13440,plain,
incident(b,n),
inference(superposition,[status(thm)],[c_427,c_421]) ).
tcf(c_13441,plain,
incident(c,o),
inference(superposition,[status(thm)],[c_426,c_421]) ).
tcf(c_13442,plain,
incident(b,p),
inference(superposition,[status(thm)],[c_425,c_421]) ).
tcf(c_13443,plain,
incident(a,q),
inference(superposition,[status(thm)],[c_424,c_421]) ).
tcf(c_13444,plain,
incident(c,r),
inference(superposition,[status(thm)],[c_423,c_421]) ).
tcf(c_13445,plain,
incident(a,s),
inference(superposition,[status(thm)],[c_422,c_421]) ).
tcf(c_13455,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(g,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13396,c_411]) ).
tcf(c_13456,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(g,X0_iProver_incident_2)
| ~ line_equal(o,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13397,c_411]) ).
tcf(c_13457,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,X0_iProver_incident_2)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13398,c_411]) ).
tcf(c_13459,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,m)
| ~ point_equal(X0_iProver_incident_1,f) ),
inference(superposition,[status(thm)],[c_13395,c_412]) ).
tcf(c_13460,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,n)
| ~ point_equal(X0_iProver_incident_1,g) ),
inference(superposition,[status(thm)],[c_13396,c_412]) ).
tcf(c_13461,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,o)
| ~ point_equal(X0_iProver_incident_1,g) ),
inference(superposition,[status(thm)],[c_13397,c_412]) ).
tcf(c_13462,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,p)
| ~ point_equal(X0_iProver_incident_1,h) ),
inference(superposition,[status(thm)],[c_13398,c_412]) ).
tcf(c_13463,plain,
( incident(a,p)
| ~ point_equal(a,h) ),
inference(instantiation,[status(thm)],[c_13462]) ).
tcf(c_13464,plain,
( incident(a,o)
| ~ point_equal(a,g) ),
inference(instantiation,[status(thm)],[c_13461]) ).
tcf(c_13465,plain,
( incident(a,n)
| ~ point_equal(a,g) ),
inference(instantiation,[status(thm)],[c_13460]) ).
tcf(c_13466,plain,
( incident(a,m)
| ~ point_equal(a,f) ),
inference(instantiation,[status(thm)],[c_13459]) ).
tcf(c_13478,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,r)
| ~ point_equal(X0_iProver_incident_1,i) ),
inference(superposition,[status(thm)],[c_13400,c_412]) ).
tcf(c_13480,plain,
point_equal(i,i),
inference(superposition,[status(thm)],[c_13400,c_418]) ).
tcf(c_13482,plain,
( incident(a,r)
| ~ point_equal(a,i) ),
inference(instantiation,[status(thm)],[c_13478]) ).
tcf(c_13512,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(c,X0_iProver_incident_1)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13394,c_409]) ).
tcf(c_13513,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,m)
| point_equal(f,X0_iProver_incident_1)
| ~ incident(f,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,m)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13395,c_409]) ).
tcf(c_13514,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(g,X0_iProver_incident_1)
| ~ incident(g,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13396,c_409]) ).
tcf(c_13518,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(i,X0_iProver_incident_1)
| ~ incident(i,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13400,c_409]) ).
tcf(c_13525,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_1: iProver_incident_1,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_1: iProver_incident_1,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_1: iProver_incident_1,X5_iProver_incident_2: iProver_incident_2,X6_iProver_incident_2: iProver_incident_2] :
( line_equal(X6_iProver_incident_2,X2_iProver_incident_2)
| line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| colinear(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1,sK0(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1))
| ~ colinear(c,X1_iProver_incident_1,X5_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,X0_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_2)
| ~ colinear(b,X2_iProver_incident_1,X5_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,X0_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(a,X2_iProver_incident_1,X4_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,X1_iProver_incident_1,X3_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_429,c_410]) ).
tcf(c_13548,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(b,X0_iProver_incident_1)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13419,c_409]) ).
tcf(c_13553,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(e,X1_iProver_incident_2)
| ~ incident(e,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_13555,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ point_equal(e,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13558,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,m)
| point_equal(e,X0_iProver_incident_1)
| ~ incident(e,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,m)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13420,c_409]) ).
tcf(c_13566,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ point_equal(f,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13569,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(f,X0_iProver_incident_1)
| ~ incident(f,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13421,c_409]) ).
tcf(c_13570,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,n)
| ~ point_equal(X0_iProver_incident_1,f) ),
inference(superposition,[status(thm)],[c_13421,c_412]) ).
tcf(c_13571,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13421,c_411]) ).
tcf(c_13575,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,o)
| point_equal(e,X0_iProver_incident_1)
| ~ incident(e,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13422,c_409]) ).
tcf(c_13576,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,o)
| ~ point_equal(X0_iProver_incident_1,e) ),
inference(superposition,[status(thm)],[c_13422,c_412]) ).
tcf(c_13577,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ line_equal(o,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13422,c_411]) ).
tcf(c_13593,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,q)
| ~ point_equal(X0_iProver_incident_1,e) ),
inference(superposition,[status(thm)],[c_13424,c_412]) ).
tcf(c_13594,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ line_equal(q,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13424,c_411]) ).
tcf(c_13647,plain,
incident(g,n),
inference(resolution,[status(thm)],[c_419,c_427]) ).
tcf(c_13648,plain,
incident(g,o),
inference(resolution,[status(thm)],[c_419,c_426]) ).
tcf(c_13649,plain,
incident(h,p),
inference(resolution,[status(thm)],[c_419,c_425]) ).
tcf(c_13650,plain,
incident(h,q),
inference(resolution,[status(thm)],[c_419,c_424]) ).
tcf(c_13651,plain,
incident(i,r),
inference(resolution,[status(thm)],[c_419,c_423]) ).
tcf(c_13652,plain,
incident(i,s),
inference(resolution,[status(thm)],[c_419,c_422]) ).
tcf(c_13664,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(d,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,d) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_13665,plain,
( point_equal(d,a)
| ~ point_equal(a,d) ),
inference(instantiation,[status(thm)],[c_13664]) ).
tcf(c_13679,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ line_equal(s,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13426,c_411]) ).
tcf(c_13686,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(a,X0_iProver_incident_1)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13438,c_409]) ).
tcf(c_13697,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(i,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,i) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_13698,plain,
( point_equal(i,a)
| ~ point_equal(a,i) ),
inference(instantiation,[status(thm)],[c_13697]) ).
tcf(c_13708,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(i,X0_iProver_incident_2)
| ~ incident(i,r)
| ~ line_equal(r,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_13414]) ).
tcf(c_13711,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,n)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(superposition,[status(thm)],[c_13440,c_412]) ).
tcf(c_13712,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13440,c_411]) ).
tcf(c_13715,plain,
( incident(a,n)
| ~ point_equal(a,b) ),
inference(instantiation,[status(thm)],[c_13711]) ).
tcf(c_13719,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,o)
| ~ point_equal(X0_iProver_incident_1,c) ),
inference(superposition,[status(thm)],[c_13441,c_412]) ).
tcf(c_13720,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c,X0_iProver_incident_2)
| ~ line_equal(o,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13441,c_411]) ).
tcf(c_13723,plain,
( incident(a,o)
| ~ point_equal(a,c) ),
inference(instantiation,[status(thm)],[c_13719]) ).
tcf(c_13730,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,p)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(superposition,[status(thm)],[c_13442,c_412]) ).
tcf(c_13731,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13442,c_411]) ).
tcf(c_13734,plain,
( incident(a,p)
| ~ point_equal(a,b) ),
inference(instantiation,[status(thm)],[c_13730]) ).
tcf(c_13735,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,q)
| point_equal(a,X0_iProver_incident_1)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,q)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13443,c_409]) ).
tcf(c_13736,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,q)
| ~ point_equal(X0_iProver_incident_1,a) ),
inference(superposition,[status(thm)],[c_13443,c_412]) ).
tcf(c_13737,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a,X0_iProver_incident_2)
| ~ line_equal(q,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13443,c_411]) ).
tcf(c_13744,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(c,X0_iProver_incident_1)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13444,c_409]) ).
tcf(c_13745,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,r)
| ~ point_equal(X0_iProver_incident_1,c) ),
inference(superposition,[status(thm)],[c_13444,c_412]) ).
tcf(c_13746,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c,X0_iProver_incident_2)
| ~ line_equal(r,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13444,c_411]) ).
tcf(c_13749,plain,
( incident(a,r)
| ~ point_equal(a,c) ),
inference(instantiation,[status(thm)],[c_13745]) ).
tcf(c_13758,plain,
incident(b,l),
inference(resolution,[status(thm)],[c_420,c_429]) ).
tcf(c_13761,plain,
incident(e,o),
inference(resolution,[status(thm)],[c_420,c_426]) ).
tcf(c_13762,plain,
incident(d,p),
inference(resolution,[status(thm)],[c_420,c_425]) ).
tcf(c_13763,plain,
incident(e,q),
inference(resolution,[status(thm)],[c_420,c_424]) ).
tcf(c_13764,plain,
incident(d,r),
inference(resolution,[status(thm)],[c_420,c_423]) ).
tcf(c_13765,plain,
incident(f,s),
inference(resolution,[status(thm)],[c_420,c_422]) ).
tcf(c_13767,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,f)
| ~ point_equal(f,X0_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_13770,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(a,X0_iProver_incident_1)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13445,c_409]) ).
tcf(c_13771,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,s)
| ~ point_equal(X0_iProver_incident_1,a) ),
inference(superposition,[status(thm)],[c_13445,c_412]) ).
tcf(c_13772,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a,X0_iProver_incident_2)
| ~ line_equal(s,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_13445,c_411]) ).
tcf(c_13863,plain,
( line_equal(n,l)
| point_equal(c,b)
| ~ incident(c,n)
| ~ incident(b,l) ),
inference(superposition,[status(thm)],[c_13440,c_13512]) ).
tcf(c_13868,plain,
( line_equal(s,l)
| point_equal(c,a)
| ~ incident(c,s)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_13445,c_13512]) ).
tcf(c_13918,plain,
( line_equal(r,m)
| point_equal(f,d)
| ~ incident(f,r)
| ~ incident(d,m) ),
inference(superposition,[status(thm)],[c_13425,c_13513]) ).
tcf(c_13962,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,r)
| ~ line_equal(X0_iProver_incident_2,r)
| ~ incident(h,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_13969,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(o,n)
| point_equal(g,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,n) ),
inference(superposition,[status(thm)],[c_13397,c_13514]) ).
tcf(c_13972,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(h,s)
| ~ point_equal(h,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,s) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_13973,plain,
( incident(h,s)
| ~ point_equal(h,a)
| ~ incident(a,s) ),
inference(instantiation,[status(thm)],[c_13972]) ).
tcf(c_13992,plain,
( ~ incident(c,n)
| point_equal(c,b) ),
inference(global_subsumption_just,[status(thm)],[c_13863,c_81,c_62,c_441,c_668,c_12065]) ).
tcf(c_13993,plain,
( point_equal(c,b)
| ~ incident(c,n) ),
inference(renaming,[status(thm)],[c_13992]) ).
tcf(c_14008,plain,
( ~ incident(c,s)
| point_equal(c,a) ),
inference(global_subsumption_just,[status(thm)],[c_13868,c_12163]) ).
tcf(c_14009,plain,
( point_equal(c,a)
| ~ incident(c,s) ),
inference(renaming,[status(thm)],[c_14008]) ).
tcf(c_14058,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(s,r)
| point_equal(i,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,r) ),
inference(superposition,[status(thm)],[c_13401,c_13518]) ).
tcf(c_14080,plain,
( line_equal(o,l)
| point_equal(b,c)
| ~ incident(c,l)
| ~ incident(b,o) ),
inference(superposition,[status(thm)],[c_13441,c_13548]) ).
tcf(c_14082,plain,
( line_equal(q,l)
| point_equal(b,a)
| ~ incident(b,q)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_13443,c_13548]) ).
tcf(c_14083,plain,
( line_equal(r,l)
| point_equal(b,c)
| ~ incident(c,l)
| ~ incident(b,r) ),
inference(superposition,[status(thm)],[c_13444,c_13548]) ).
tcf(c_14087,plain,
( incident(c,m)
| ~ point_equal(c,d)
| ~ incident(d,m) ),
inference(instantiation,[status(thm)],[c_13429]) ).
tcf(c_14088,plain,
( incident(b,m)
| ~ point_equal(b,d)
| ~ incident(d,m) ),
inference(instantiation,[status(thm)],[c_13428]) ).
tcf(c_14094,plain,
( incident(c,m)
| ~ point_equal(c,e)
| ~ incident(e,m) ),
inference(instantiation,[status(thm)],[c_13429]) ).
tcf(c_14107,plain,
( line_equal(r,m)
| point_equal(f,d)
| ~ incident(f,r) ),
inference(global_subsumption_just,[status(thm)],[c_13918,c_458,c_12106]) ).
tcf(c_14130,plain,
( line_equal(p,m)
| point_equal(e,d)
| ~ incident(e,p)
| ~ incident(d,m) ),
inference(superposition,[status(thm)],[c_13423,c_13558]) ).
tcf(c_14141,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ incident(e,q)
| ~ line_equal(q,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_13553]) ).
tcf(c_14187,plain,
( line_equal(p,n)
| point_equal(f,d)
| ~ incident(f,p)
| ~ incident(d,n) ),
inference(superposition,[status(thm)],[c_13423,c_13569]) ).
tcf(c_14201,plain,
( incident(b,m)
| ~ point_equal(b,f)
| ~ incident(f,m) ),
inference(instantiation,[status(thm)],[c_13428]) ).
tcf(c_14206,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1] :
( line_equal(r,X0_iProver_incident_2)
| point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| ~ incident(X1_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_14217,plain,
( line_equal(m,o)
| point_equal(e,f)
| ~ incident(f,o)
| ~ incident(e,m) ),
inference(superposition,[status(thm)],[c_13395,c_13575]) ).
tcf(c_14230,plain,
( line_equal(r,o)
| point_equal(e,d)
| ~ incident(e,r)
| ~ incident(d,o) ),
inference(superposition,[status(thm)],[c_13425,c_13575]) ).
tcf(c_14236,plain,
( line_equal(q,o)
| point_equal(e,a)
| ~ incident(e,q)
| ~ incident(a,o) ),
inference(superposition,[status(thm)],[c_13443,c_13575]) ).
tcf(c_14282,plain,
incident(a,l),
inference(resolution,[status(thm)],[c_421,c_429]) ).
tcf(c_14283,plain,
incident(d,m),
inference(resolution,[status(thm)],[c_421,c_428]) ).
tcf(c_14284,plain,
incident(b,n),
inference(resolution,[status(thm)],[c_421,c_427]) ).
tcf(c_14285,plain,
incident(c,o),
inference(resolution,[status(thm)],[c_421,c_426]) ).
tcf(c_14286,plain,
incident(b,p),
inference(resolution,[status(thm)],[c_421,c_425]) ).
tcf(c_14287,plain,
incident(a,q),
inference(resolution,[status(thm)],[c_421,c_424]) ).
tcf(c_14288,plain,
incident(c,r),
inference(resolution,[status(thm)],[c_421,c_423]) ).
tcf(c_14289,plain,
incident(a,s),
inference(resolution,[status(thm)],[c_421,c_422]) ).
tcf(c_14348,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( line_equal(o,l)
| point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| ~ incident(X1_iProver_incident_1,o)
| ~ incident(X1_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,l) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_14380,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(h,X1_iProver_incident_2)
| ~ incident(h,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_14382,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(h,X0_iProver_incident_2)
| ~ point_equal(h,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_14383,plain,
( incident(h,l)
| ~ point_equal(h,a)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_14382]) ).
tcf(c_14417,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(h,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,h) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_14418,plain,
( point_equal(h,a)
| ~ point_equal(a,h) ),
inference(instantiation,[status(thm)],[c_14417]) ).
tcf(c_14445,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1] :
( line_equal(o,X0_iProver_incident_2)
| point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| ~ incident(X1_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_14674,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| ~ incident(X1_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_14677,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| ~ line_equal(r,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_14694,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(X0_iProver_incident_1,a)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14282]) ).
tcf(c_14697,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(X0_iProver_incident_1,g)
| ~ incident(g,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13647]) ).
tcf(c_14698,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,o)
| point_equal(X0_iProver_incident_1,g)
| ~ incident(g,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13648]) ).
tcf(c_14699,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(X0_iProver_incident_1,h)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13649]) ).
tcf(c_14700,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,q)
| point_equal(X0_iProver_incident_1,h)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,q)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13650]) ).
tcf(c_14701,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(X0_iProver_incident_1,i)
| ~ incident(i,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13651]) ).
tcf(c_14702,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(X0_iProver_incident_1,i)
| ~ incident(i,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13652]) ).
tcf(c_14703,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(X0_iProver_incident_1,b)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13758]) ).
tcf(c_14707,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(X0_iProver_incident_1,d)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13762]) ).
tcf(c_14709,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(X0_iProver_incident_1,d)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13764]) ).
tcf(c_14710,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(X0_iProver_incident_1,f)
| ~ incident(f,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_13765]) ).
tcf(c_14711,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,m)
| point_equal(X0_iProver_incident_1,d)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,m)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14283]) ).
tcf(c_14712,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(X0_iProver_incident_1,b)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14284]) ).
tcf(c_14713,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,o)
| point_equal(X0_iProver_incident_1,c)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14285]) ).
tcf(c_14714,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(X0_iProver_incident_1,b)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14286]) ).
tcf(c_14715,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,q)
| point_equal(X0_iProver_incident_1,a)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,q)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14287]) ).
tcf(c_14717,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(X0_iProver_incident_1,a)
| ~ incident(a,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_14289]) ).
tcf(c_14719,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| ~ incident(X1_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X1_iProver_incident_1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_409]) ).
tcf(c_14829,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,r)
| ~ line_equal(X0_iProver_incident_2,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_14832,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,r)
| ~ incident(X1_iProver_incident_1,r)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_14836,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,X0_iProver_incident_2)
| point_equal(X0_iProver_incident_1,i)
| ~ incident(i,r)
| ~ incident(i,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_14206]) ).
tcf(c_14851,plain,
( ~ incident(b,o)
| point_equal(b,c) ),
inference(global_subsumption_just,[status(thm)],[c_14080,c_81,c_61,c_433,c_671,c_12198]) ).
tcf(c_14852,plain,
( point_equal(b,c)
| ~ incident(b,o) ),
inference(renaming,[status(thm)],[c_14851]) ).
tcf(c_14853,plain,
( ~ incident(b,q)
| point_equal(b,a) ),
inference(global_subsumption_just,[status(thm)],[c_14082,c_81,c_61,c_457,c_702,c_12200]) ).
tcf(c_14854,plain,
( point_equal(b,a)
| ~ incident(b,q) ),
inference(renaming,[status(thm)],[c_14853]) ).
tcf(c_14855,plain,
( ~ incident(b,r)
| point_equal(b,c) ),
inference(global_subsumption_just,[status(thm)],[c_14083,c_81,c_60,c_433,c_705,c_12201]) ).
tcf(c_14856,plain,
( point_equal(b,c)
| ~ incident(b,r) ),
inference(renaming,[status(thm)],[c_14855]) ).
tcf(c_15077,plain,
( line_equal(p,m)
| point_equal(e,d)
| ~ incident(e,p) ),
inference(global_subsumption_just,[status(thm)],[c_14130,c_458,c_12293]) ).
tcf(c_15095,plain,
( line_equal(p,q)
| point_equal(a,h)
| ~ incident(h,q)
| ~ incident(a,p) ),
inference(superposition,[status(thm)],[c_13398,c_13735]) ).
tcf(c_15099,plain,
( line_equal(l,q)
| point_equal(a,b)
| ~ incident(b,q)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_13419,c_13735]) ).
tcf(c_15151,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,p)
| ~ incident(X1_iProver_incident_1,p)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_15160,plain,
( line_equal(o,r)
| point_equal(c,g)
| ~ incident(g,r)
| ~ incident(c,o) ),
inference(superposition,[status(thm)],[c_13397,c_13744]) ).
tcf(c_15168,plain,
( line_equal(o,r)
| point_equal(c,e)
| ~ incident(e,r)
| ~ incident(c,o) ),
inference(superposition,[status(thm)],[c_13422,c_13744]) ).
tcf(c_15169,plain,
( line_equal(p,r)
| point_equal(c,d)
| ~ incident(d,r)
| ~ incident(c,p) ),
inference(superposition,[status(thm)],[c_13423,c_13744]) ).
tcf(c_15190,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,o)
| ~ incident(X1_iProver_incident_1,o)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_15251,plain,
( line_equal(l,s)
| point_equal(a,b)
| ~ incident(b,s)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_13419,c_13770]) ).
tcf(c_15255,plain,
( line_equal(p,s)
| point_equal(a,d)
| ~ incident(d,s)
| ~ incident(a,p) ),
inference(superposition,[status(thm)],[c_13423,c_13770]) ).
tcf(c_15274,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,n)
| ~ line_equal(X0_iProver_incident_2,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_15277,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,n)
| ~ incident(X1_iProver_incident_1,n)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_15318,plain,
( line_equal(o,l)
| point_equal(g,a)
| ~ incident(g,l)
| ~ incident(a,o) ),
inference(resolution,[status(thm)],[c_14694,c_13648]) ).
tcf(c_15321,plain,
( line_equal(r,l)
| point_equal(i,a)
| ~ incident(i,l)
| ~ incident(a,r) ),
inference(resolution,[status(thm)],[c_14694,c_13651]) ).
tcf(c_15322,plain,
( line_equal(s,l)
| point_equal(i,a)
| ~ incident(i,l)
| ~ incident(a,s) ),
inference(resolution,[status(thm)],[c_14694,c_13652]) ).
tcf(c_15334,plain,
( line_equal(p,l)
| point_equal(b,a)
| ~ incident(b,l)
| ~ incident(a,p) ),
inference(resolution,[status(thm)],[c_14694,c_14286]) ).
tcf(c_15339,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| colinear(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1,sK0(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1))
| ~ colinear(c,e,X2_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,d,X1_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(b,f,X2_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,e,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_428,c_13525]) ).
tcf(c_15378,plain,
( line_equal(p,n)
| ~ incident(d,n) ),
inference(global_subsumption_just,[status(thm)],[c_14187,c_81,c_58,c_461,c_458,c_13084,c_14088]) ).
tcf(c_15410,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,q)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| line_equal(X1_iProver_incident_2,X3_iProver_incident_2)
| colinear(X1_iProver_incident_1,h,X0_iProver_incident_1,sK0(X1_iProver_incident_1,h,X0_iProver_incident_1))
| ~ colinear(b,d,h,X4_iProver_incident_2)
| ~ colinear(c,e,X1_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(c,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(b,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_424,c_15339]) ).
tcf(c_15411,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2] :
( line_equal(X3_iProver_incident_2,s)
| line_equal(X2_iProver_incident_2,q)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| colinear(X0_iProver_incident_1,h,i,sK0(X0_iProver_incident_1,h,i))
| ~ colinear(c,d,i,X3_iProver_incident_2)
| ~ colinear(b,d,h,X2_iProver_incident_2)
| ~ colinear(c,e,X0_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(b,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_422,c_15410]) ).
tcf(c_15424,plain,
( line_equal(m,o)
| point_equal(e,f)
| ~ incident(f,o) ),
inference(global_subsumption_just,[status(thm)],[c_14217,c_442,c_12453]) ).
tcf(c_15478,plain,
( line_equal(r,o)
| ~ incident(d,o) ),
inference(global_subsumption_just,[status(thm)],[c_14230,c_81,c_59,c_463,c_458,c_13188,c_14087]) ).
tcf(c_15480,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2] :
( line_equal(n,X2_iProver_incident_2)
| line_equal(X1_iProver_incident_2,s)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X2_iProver_incident_2)
| ~ colinear(c,d,i,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_427,c_15411]) ).
tcf(c_15481,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(n,X1_iProver_incident_2)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_423,c_15480]) ).
tcf(c_15483,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,X0_iProver_incident_2)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_425,c_15481]) ).
tcf(c_15524,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| colinear(g,h,i,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_426,c_15483]) ).
tcf(c_15527,plain,
( line_equal(q,o)
| ~ incident(a,o) ),
inference(global_subsumption_just,[status(thm)],[c_14236,c_81,c_61,c_446,c_457,c_12472,c_13433]) ).
tcf(c_15559,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(r,s)
| point_equal(X0_iProver_incident_1,i)
| ~ incident(i,s)
| ~ incident(i,r)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,r) ),
inference(instantiation,[status(thm)],[c_14836]) ).
tcf(c_15563,plain,
( ~ incident(a,o)
| ~ incident(g,l)
| point_equal(g,a) ),
inference(global_subsumption_just,[status(thm)],[c_15318,c_81,c_61,c_671,c_15318]) ).
tcf(c_15564,plain,
( point_equal(g,a)
| ~ incident(g,l)
| ~ incident(a,o) ),
inference(renaming,[status(thm)],[c_15563]) ).
tcf(c_15589,plain,
( ~ incident(i,l)
| point_equal(i,a) ),
inference(global_subsumption_just,[status(thm)],[c_15321,c_81,c_62,c_464,c_708,c_15322]) ).
tcf(c_15590,plain,
( point_equal(i,a)
| ~ incident(i,l) ),
inference(renaming,[status(thm)],[c_15589]) ).
tcf(c_15729,plain,
( ~ incident(a,p)
| point_equal(b,a) ),
inference(global_subsumption_just,[status(thm)],[c_15334,c_81,c_60,c_441,c_699,c_15334]) ).
tcf(c_15730,plain,
( point_equal(b,a)
| ~ incident(a,p) ),
inference(renaming,[status(thm)],[c_15729]) ).
tcf(c_15792,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o) ),
inference(global_subsumption_just,[status(thm)],[c_15524,c_541]) ).
tcf(c_15795,plain,
( line_equal(s,r)
| line_equal(p,q)
| line_equal(n,o) ),
inference(superposition,[status(thm)],[c_15792,c_414]) ).
tcf(c_15796,plain,
( line_equal(p,q)
| line_equal(n,o)
| incident(c,s) ),
inference(superposition,[status(thm)],[c_15792,c_13746]) ).
tcf(c_15815,plain,
( line_equal(p,q)
| line_equal(n,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_15795,c_13772]) ).
tcf(c_15816,plain,
( line_equal(p,q)
| line_equal(n,o)
| incident(f,r) ),
inference(superposition,[status(thm)],[c_15795,c_13679]) ).
tcf(c_15830,plain,
( line_equal(q,p)
| line_equal(n,o)
| incident(c,s) ),
inference(superposition,[status(thm)],[c_15796,c_414]) ).
tcf(c_15831,plain,
( line_equal(n,o)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_15796,c_13731]) ).
tcf(c_15863,plain,
( line_equal(q,p)
| line_equal(n,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_15815,c_414]) ).
tcf(c_15864,plain,
( line_equal(n,o)
| incident(b,q)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_15815,c_13731]) ).
tcf(c_15891,plain,
( line_equal(n,o)
| incident(f,r)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_15816,c_13731]) ).
tcf(c_15905,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(o,X0_iProver_incident_2)
| point_equal(X0_iProver_incident_1,e)
| ~ incident(e,o)
| ~ incident(e,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_14445]) ).
tcf(c_15908,plain,
( line_equal(n,o)
| incident(c,s)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_15830,c_13737]) ).
tcf(c_15935,plain,
( line_equal(o,n)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_15831,c_414]) ).
tcf(c_15936,plain,
( incident(c,s)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_15831,c_13712]) ).
tcf(c_15937,plain,
( incident(f,o)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_15831,c_13571]) ).
tcf(c_16049,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,r)
| point_equal(X0_iProver_incident_1,d)
| ~ incident(d,r)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_14674]) ).
tcf(c_16057,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,s)
| point_equal(i,X0_iProver_incident_1)
| ~ incident(i,s)
| ~ incident(i,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_14719]) ).
tcf(c_16085,plain,
( line_equal(n,o)
| incident(e,p)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_15863,c_13594]) ).
tcf(c_16088,plain,
( line_equal(o,n)
| incident(b,q)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_15864,c_414]) ).
tcf(c_16089,plain,
( incident(b,q)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_15864,c_13712]) ).
tcf(c_16101,plain,
( incident(e,n)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_15935,c_13577]) ).
tcf(c_16143,plain,
( line_equal(r,n)
| point_equal(c,g)
| ~ incident(g,r)
| ~ incident(c,n) ),
inference(resolution,[status(thm)],[c_14697,c_14288]) ).
tcf(c_16162,plain,
( incident(f,r)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_15891,c_13712]) ).
tcf(c_16183,plain,
( point_equal(d,f)
| ~ point_equal(f,d) ),
inference(instantiation,[status(thm)],[c_13767]) ).
tcf(c_16198,plain,
( line_equal(o,n)
| incident(c,s)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_15908,c_414]) ).
tcf(c_16199,plain,
( incident(c,s)
| incident(b,o)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_15908,c_13712]) ).
tcf(c_16204,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(e,X0_iProver_incident_2)
| ~ point_equal(e,d)
| ~ incident(d,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_13555]) ).
tcf(c_16241,plain,
( point_equal(c,a)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_15936,c_14009]) ).
tcf(c_16249,plain,
( point_equal(e,f)
| ~ point_equal(f,e) ),
inference(instantiation,[status(thm)],[c_13767]) ).
tcf(c_16251,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(f,X0_iProver_incident_2)
| ~ point_equal(f,e)
| ~ incident(e,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_13566]) ).
tcf(c_16336,plain,
( line_equal(m,o)
| point_equal(e,f)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_15937,c_15424]) ).
tcf(c_16387,plain,
( incident(a,m)
| ~ line_equal(q,m)
| ~ incident(a,q) ),
inference(instantiation,[status(thm)],[c_13408]) ).
tcf(c_16537,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,X0_iProver_incident_2)
| ~ incident(h,q)
| ~ line_equal(q,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_14380]) ).
tcf(c_16544,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,r)
| ~ incident(c,r)
| ~ point_equal(X0_iProver_incident_1,c) ),
inference(instantiation,[status(thm)],[c_14832]) ).
tcf(c_16736,plain,
( line_equal(l,o)
| point_equal(a,g)
| ~ incident(g,l)
| ~ incident(a,o) ),
inference(resolution,[status(thm)],[c_14698,c_14282]) ).
tcf(c_16752,plain,
( line_equal(s,o)
| point_equal(f,g)
| ~ incident(g,s)
| ~ incident(f,o) ),
inference(resolution,[status(thm)],[c_14698,c_13765]) ).
tcf(c_16754,plain,
( line_equal(n,o)
| point_equal(b,g)
| ~ incident(g,n)
| ~ incident(b,o) ),
inference(resolution,[status(thm)],[c_14698,c_14284]) ).
tcf(c_17034,plain,
( incident(c,n)
| incident(b,q)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_16088,c_13720]) ).
tcf(c_17078,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(p,r)
| point_equal(X0_iProver_incident_1,d)
| ~ incident(d,r)
| ~ incident(d,p)
| ~ incident(X0_iProver_incident_1,r)
| ~ incident(X0_iProver_incident_1,p) ),
inference(instantiation,[status(thm)],[c_16049]) ).
tcf(c_17079,plain,
( line_equal(p,r)
| point_equal(a,d)
| ~ incident(d,r)
| ~ incident(d,p)
| ~ incident(a,r)
| ~ incident(a,p) ),
inference(instantiation,[status(thm)],[c_17078]) ).
tcf(c_17140,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(r,s)
| point_equal(i,X0_iProver_incident_1)
| ~ incident(i,s)
| ~ incident(i,r)
| ~ incident(X0_iProver_incident_1,s)
| ~ incident(X0_iProver_incident_1,r) ),
inference(instantiation,[status(thm)],[c_16057]) ).
tcf(c_17268,plain,
( line_equal(l,p)
| point_equal(a,h)
| ~ incident(h,l)
| ~ incident(a,p) ),
inference(resolution,[status(thm)],[c_14699,c_14282]) ).
tcf(c_17276,plain,
( line_equal(s,p)
| point_equal(i,h)
| ~ incident(i,p)
| ~ incident(h,s) ),
inference(resolution,[status(thm)],[c_14699,c_13652]) ).
tcf(c_17291,plain,
( line_equal(s,p)
| point_equal(a,h)
| ~ incident(h,s)
| ~ incident(a,p) ),
inference(resolution,[status(thm)],[c_14699,c_14289]) ).
tcf(c_17473,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(c,q)
| ~ point_equal(c,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,q) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_17474,plain,
( incident(c,q)
| ~ point_equal(c,a)
| ~ incident(a,q) ),
inference(instantiation,[status(thm)],[c_17473]) ).
tcf(c_17483,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b,q)
| ~ point_equal(b,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,q) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_17484,plain,
( incident(b,q)
| ~ point_equal(b,a)
| ~ incident(a,q) ),
inference(instantiation,[status(thm)],[c_17483]) ).
tcf(c_17529,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,p)
| ~ incident(b,p)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(instantiation,[status(thm)],[c_15151]) ).
tcf(c_17534,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c,e)
| line_equal(o,X0_iProver_incident_2)
| ~ incident(e,o)
| ~ incident(c,o)
| ~ incident(e,X0_iProver_incident_2)
| ~ incident(c,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_15905]) ).
tcf(c_17539,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,o)
| ~ incident(c,o)
| ~ point_equal(X0_iProver_incident_1,c) ),
inference(instantiation,[status(thm)],[c_15190]) ).
tcf(c_17551,plain,
( incident(e,p)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_16085,c_13712]) ).
tcf(c_17592,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c,s)
| ~ line_equal(X0_iProver_incident_2,s)
| ~ incident(c,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_17595,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(c,s)
| ~ point_equal(c,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,s) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_17596,plain,
( incident(c,s)
| ~ point_equal(c,a)
| ~ incident(a,s) ),
inference(instantiation,[status(thm)],[c_17595]) ).
tcf(c_17625,plain,
( point_equal(b,a)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_16089,c_14854]) ).
tcf(c_17734,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,n)
| ~ incident(b,n)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(instantiation,[status(thm)],[c_15277]) ).
tcf(c_17786,plain,
( line_equal(p,q)
| point_equal(b,h)
| ~ incident(h,p)
| ~ incident(b,q) ),
inference(resolution,[status(thm)],[c_14700,c_14286]) ).
tcf(c_17833,plain,
( incident(e,r)
| ~ point_equal(e,d)
| ~ incident(d,r) ),
inference(instantiation,[status(thm)],[c_16204]) ).
tcf(c_17887,plain,
( incident(f,q)
| ~ point_equal(f,e)
| ~ incident(e,q) ),
inference(instantiation,[status(thm)],[c_16251]) ).
tcf(c_17986,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,c)
| ~ point_equal(c,X0_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_18006,plain,
( line_equal(n,m)
| point_equal(f,e)
| incident(c,s)
| incident(b,q)
| ~ incident(f,n)
| ~ incident(e,m) ),
inference(superposition,[status(thm)],[c_16101,c_13513]) ).
tcf(c_18250,plain,
( incident(c,s)
| incident(c,n)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_16198,c_13720]) ).
tcf(c_18490,plain,
( line_equal(o,r)
| point_equal(e,i)
| ~ incident(i,o)
| ~ incident(e,r) ),
inference(resolution,[status(thm)],[c_14701,c_13761]) ).
tcf(c_18611,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,s)
| ~ line_equal(X0_iProver_incident_2,s)
| ~ incident(b,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_18614,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b,s)
| ~ point_equal(b,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,s) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_18615,plain,
( incident(b,s)
| ~ point_equal(b,a)
| ~ incident(a,s) ),
inference(instantiation,[status(thm)],[c_18614]) ).
tcf(c_18657,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(g,s)
| ~ line_equal(X0_iProver_incident_2,s)
| ~ incident(g,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_19065,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(b,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_19066,plain,
( point_equal(b,a)
| ~ point_equal(a,b) ),
inference(instantiation,[status(thm)],[c_19065]) ).
tcf(c_19151,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,g)
| ~ point_equal(g,X0_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_19152,plain,
( point_equal(a,g)
| ~ point_equal(g,a) ),
inference(instantiation,[status(thm)],[c_19151]) ).
tcf(c_19169,plain,
( line_equal(p,s)
| point_equal(h,i)
| ~ incident(i,p)
| ~ incident(h,s) ),
inference(resolution,[status(thm)],[c_14702,c_13649]) ).
tcf(c_19173,plain,
( line_equal(l,s)
| point_equal(b,i)
| ~ incident(i,l)
| ~ incident(b,s) ),
inference(resolution,[status(thm)],[c_14702,c_13758]) ).
tcf(c_19183,plain,
( line_equal(o,s)
| point_equal(c,i)
| ~ incident(i,o)
| ~ incident(c,s) ),
inference(resolution,[status(thm)],[c_14702,c_14285]) ).
tcf(c_19184,plain,
( line_equal(p,s)
| point_equal(b,i)
| ~ incident(i,p)
| ~ incident(b,s) ),
inference(resolution,[status(thm)],[c_14702,c_14286]) ).
tcf(c_19222,plain,
( line_equal(r,m)
| point_equal(f,d)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_16162,c_14107]) ).
tcf(c_19365,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(g,X0_iProver_incident_2)
| ~ point_equal(g,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_412]) ).
tcf(c_19366,plain,
( incident(g,l)
| ~ point_equal(g,a)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_19365]) ).
tcf(c_19668,plain,
( point_equal(c,a)
| incident(b,o)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_16199,c_14009]) ).
tcf(c_19722,plain,
( line_equal(o,l)
| point_equal(c,b)
| ~ incident(c,l)
| ~ incident(b,o) ),
inference(resolution,[status(thm)],[c_14703,c_14285]) ).
tcf(c_19726,plain,
( line_equal(s,l)
| point_equal(a,b)
| ~ incident(b,s)
| ~ incident(a,l) ),
inference(resolution,[status(thm)],[c_14703,c_14289]) ).
tcf(c_19921,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,n)
| ~ line_equal(o,n)
| ~ incident(X0_iProver_incident_1,o) ),
inference(instantiation,[status(thm)],[c_15274]) ).
tcf(c_19924,plain,
( incident(a,n)
| ~ line_equal(o,n)
| ~ incident(a,o) ),
inference(instantiation,[status(thm)],[c_19921]) ).
tcf(c_20144,plain,
( incident(g,s)
| ~ line_equal(n,s)
| ~ incident(g,n) ),
inference(instantiation,[status(thm)],[c_18657]) ).
tcf(c_20145,plain,
( incident(g,s)
| ~ line_equal(o,s)
| ~ incident(g,o) ),
inference(instantiation,[status(thm)],[c_18657]) ).
tcf(c_20553,plain,
( point_equal(a,c)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_16241,c_417]) ).
tcf(c_21515,plain,
( incident(b,m)
| ~ line_equal(n,m)
| ~ incident(b,n) ),
inference(instantiation,[status(thm)],[c_13409]) ).
tcf(c_21542,plain,
( point_equal(c,b)
| incident(b,q)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_17034,c_13993]) ).
tcf(c_21571,plain,
( line_equal(q,p)
| point_equal(e,d)
| ~ incident(e,p)
| ~ incident(d,q) ),
inference(resolution,[status(thm)],[c_14707,c_13763]) ).
tcf(c_21579,plain,
( line_equal(r,p)
| point_equal(c,d)
| ~ incident(d,r)
| ~ incident(c,p) ),
inference(resolution,[status(thm)],[c_14707,c_14288]) ).
tcf(c_21580,plain,
( line_equal(s,p)
| point_equal(a,d)
| ~ incident(d,s)
| ~ incident(a,p) ),
inference(resolution,[status(thm)],[c_14707,c_14289]) ).
tcf(c_21782,plain,
( incident(c,m)
| ~ line_equal(o,m)
| ~ incident(c,o) ),
inference(instantiation,[status(thm)],[c_13410]) ).
tcf(c_22022,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(o,l)
| point_equal(X0_iProver_incident_1,b)
| ~ incident(b,o)
| ~ incident(b,l)
| ~ incident(X0_iProver_incident_1,o)
| ~ incident(X0_iProver_incident_1,l) ),
inference(instantiation,[status(thm)],[c_14348]) ).
tcf(c_22023,plain,
( line_equal(o,l)
| point_equal(a,b)
| ~ incident(b,o)
| ~ incident(b,l)
| ~ incident(a,o)
| ~ incident(a,l) ),
inference(instantiation,[status(thm)],[c_22022]) ).
tcf(c_22068,plain,
( incident(b,q)
| incident(b,o)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_20553,c_13719]) ).
tcf(c_22357,plain,
( line_equal(p,r)
| point_equal(b,d)
| ~ incident(d,p)
| ~ incident(b,r) ),
inference(resolution,[status(thm)],[c_14709,c_14286]) ).
tcf(c_22470,plain,
( line_equal(p,m)
| point_equal(e,d)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_17551,c_15077]) ).
tcf(c_22754,plain,
( line_equal(m,s)
| point_equal(d,f)
| ~ incident(f,m)
| ~ incident(d,s) ),
inference(resolution,[status(thm)],[c_14710,c_14283]) ).
tcf(c_22755,plain,
( line_equal(n,s)
| point_equal(b,f)
| ~ incident(f,n)
| ~ incident(b,s) ),
inference(resolution,[status(thm)],[c_14710,c_14284]) ).
tcf(c_22758,plain,
( line_equal(q,s)
| point_equal(a,f)
| ~ incident(f,q)
| ~ incident(a,s) ),
inference(resolution,[status(thm)],[c_14710,c_14287]) ).
tcf(c_22832,plain,
( line_equal(o,s)
| point_equal(c,e)
| ~ incident(e,s)
| ~ incident(e,o)
| ~ incident(c,s)
| ~ incident(c,o) ),
inference(instantiation,[status(thm)],[c_17534]) ).
tcf(c_23389,plain,
( incident(c,n)
| ~ point_equal(c,b)
| ~ incident(b,n) ),
inference(instantiation,[status(thm)],[c_17734]) ).
tcf(c_23390,plain,
( incident(c,p)
| ~ point_equal(c,b)
| ~ incident(b,p) ),
inference(instantiation,[status(thm)],[c_17529]) ).
tcf(c_23586,plain,
( line_equal(q,m)
| point_equal(e,d)
| ~ incident(e,m)
| ~ incident(d,q) ),
inference(resolution,[status(thm)],[c_14711,c_13763]) ).
tcf(c_23588,plain,
( line_equal(s,m)
| point_equal(f,d)
| ~ incident(f,m)
| ~ incident(d,s) ),
inference(resolution,[status(thm)],[c_14711,c_13765]) ).
tcf(c_23671,plain,
( incident(b,o)
| ~ point_equal(b,c)
| ~ incident(c,o) ),
inference(instantiation,[status(thm)],[c_17539]) ).
tcf(c_23672,plain,
( incident(b,r)
| ~ point_equal(b,c)
| ~ incident(c,r) ),
inference(instantiation,[status(thm)],[c_16544]) ).
tcf(c_23830,plain,
( line_equal(l,n)
| point_equal(a,b)
| ~ incident(b,l)
| ~ incident(a,n) ),
inference(resolution,[status(thm)],[c_14712,c_14282]) ).
tcf(c_24602,plain,
( point_equal(c,a)
| incident(c,n)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_18250,c_14009]) ).
tcf(c_24755,plain,
( line_equal(n,o)
| point_equal(g,c)
| ~ incident(g,o)
| ~ incident(c,n) ),
inference(resolution,[status(thm)],[c_14713,c_13647]) ).
tcf(c_25084,plain,
( line_equal(p,r)
| ~ line_equal(r,p) ),
inference(instantiation,[status(thm)],[c_14677]) ).
tcf(c_25087,plain,
( incident(i,p)
| ~ line_equal(r,p)
| ~ incident(i,r) ),
inference(instantiation,[status(thm)],[c_13708]) ).
tcf(c_25099,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,r)
| ~ line_equal(p,r)
| ~ incident(X0_iProver_incident_1,p) ),
inference(instantiation,[status(thm)],[c_14829]) ).
tcf(c_25152,plain,
( line_equal(r,s)
| point_equal(i,h)
| ~ incident(i,s)
| ~ incident(i,r)
| ~ incident(h,s)
| ~ incident(h,r) ),
inference(instantiation,[status(thm)],[c_17140]) ).
tcf(c_25156,plain,
( line_equal(r,s)
| point_equal(h,i)
| ~ incident(i,s)
| ~ incident(i,r)
| ~ incident(h,s)
| ~ incident(h,r) ),
inference(instantiation,[status(thm)],[c_15559]) ).
tcf(c_25215,plain,
( line_equal(q,p)
| point_equal(h,b)
| ~ incident(h,p)
| ~ incident(b,q) ),
inference(resolution,[status(thm)],[c_14714,c_13650]) ).
tcf(c_25234,plain,
( point_equal(a,c)
| incident(b,o)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_19668,c_417]) ).
tcf(c_25920,plain,
( line_equal(p,q)
| point_equal(h,a)
| ~ incident(h,q)
| ~ incident(a,p) ),
inference(resolution,[status(thm)],[c_14715,c_13649]) ).
tcf(c_25946,plain,
( incident(e,s)
| ~ line_equal(q,s)
| ~ incident(e,q) ),
inference(instantiation,[status(thm)],[c_14141]) ).
tcf(c_25947,plain,
( incident(b,s)
| ~ line_equal(q,s)
| ~ incident(b,q) ),
inference(instantiation,[status(thm)],[c_18611]) ).
tcf(c_25998,plain,
( incident(b,o)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_25234,c_13719]) ).
tcf(c_26369,plain,
( ~ incident(g,r)
| ~ incident(c,n) ),
inference(global_subsumption_just,[status(thm)],[c_16143,c_81,c_59,c_437,c_447,c_461,c_458,c_1558,c_1768,c_12150,c_14087,c_15169,c_23390]) ).
tcf(c_26389,plain,
( ~ incident(a,o)
| ~ incident(g,l)
| point_equal(a,g) ),
inference(global_subsumption_just,[status(thm)],[c_16736,c_15564,c_19152]) ).
tcf(c_26390,plain,
( point_equal(a,g)
| ~ incident(g,l)
| ~ incident(a,o) ),
inference(renaming,[status(thm)],[c_26389]) ).
tcf(c_27407,plain,
( line_equal(q,s)
| point_equal(h,a)
| ~ incident(h,s)
| ~ incident(a,q) ),
inference(resolution,[status(thm)],[c_14717,c_13650]) ).
tcf(c_27413,plain,
( line_equal(o,s)
| point_equal(e,a)
| ~ incident(e,s)
| ~ incident(a,o) ),
inference(resolution,[status(thm)],[c_14717,c_13761]) ).
tcf(c_27473,plain,
( incident(c,s)
| ~ line_equal(r,s)
| ~ incident(c,r) ),
inference(instantiation,[status(thm)],[c_17592]) ).
tcf(c_27771,plain,
( incident(g,r)
| ~ point_equal(g,c)
| ~ incident(c,r) ),
inference(instantiation,[status(thm)],[c_16544]) ).
tcf(c_27890,plain,
( incident(c,p)
| incident(b,q)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_21542,c_13730]) ).
tcf(c_27960,plain,
( line_equal(q,l)
| point_equal(a,b)
| incident(b,o)
| incident(a,o)
| ~ incident(b,l)
| ~ incident(a,q) ),
inference(superposition,[status(thm)],[c_22068,c_13686]) ).
tcf(c_27975,plain,
( point_equal(b,a)
| incident(b,o)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_22068,c_14854]) ).
tcf(c_28039,plain,
( point_equal(a,g)
| ~ incident(g,l) ),
inference(global_subsumption_just,[status(thm)],[c_26390,c_81,c_62,c_61,c_60,c_439,c_437,c_433,c_447,c_445,c_441,c_463,c_462,c_460,c_459,c_457,c_534,c_668,c_671,c_702,c_1057,c_1081,c_1768,c_12562,c_12868,c_12867,c_13182,c_13269,c_13431,c_13464,c_13465,c_13665,c_13715,c_13734,c_13749,c_17079,c_23389,c_26369,c_26390,c_27771,c_27960]) ).
tcf(c_28041,plain,
~ incident(g,l),
inference(global_subsumption_just,[status(thm)],[c_28039,c_81,c_62,c_61,c_60,c_439,c_437,c_433,c_447,c_445,c_441,c_463,c_460,c_457,c_534,c_668,c_671,c_1768,c_12868,c_12867,c_13269,c_13431,c_13464,c_13465,c_13665,c_13734,c_13749,c_17079,c_27771,c_28039]) ).
tcf(c_28113,plain,
( ~ incident(g,s)
| ~ incident(f,o) ),
inference(global_subsumption_just,[status(thm)],[c_16752,c_81,c_59,c_57,c_438,c_446,c_464,c_460,c_1559,c_1799,c_12237,c_13466,c_17887,c_21782,c_22758]) ).
tcf(c_28137,plain,
( line_equal(n,o)
| ~ incident(b,o) ),
inference(global_subsumption_just,[status(thm)],[c_16754,c_81,c_61,c_436,c_433,c_463,c_459,c_671,c_1057,c_13182,c_23389,c_24755,c_26369,c_27771]) ).
tcf(c_28179,plain,
~ incident(h,l),
inference(global_subsumption_just,[status(thm)],[c_17268,c_81,c_61,c_58,c_435,c_434,c_443,c_464,c_462,c_457,c_702,c_1072,c_1559,c_11850,c_12568,c_13463,c_13973,c_14201,c_15730,c_18615,c_20144,c_22755]) ).
tcf(c_28217,plain,
( ~ incident(h,s)
| point_equal(i,h) ),
inference(global_subsumption_just,[status(thm)],[c_17276,c_81,c_61,c_60,c_59,c_58,c_440,c_439,c_437,c_436,c_435,c_434,c_433,c_447,c_446,c_444,c_443,c_442,c_464,c_463,c_462,c_460,c_458,c_457,c_702,c_705,c_1000,c_1072,c_1559,c_1768,c_11850,c_11991,c_12568,c_13463,c_13973,c_14087,c_14094,c_14201,c_14383,c_15169,c_15730,c_17596,c_18615,c_20144,c_20145,c_22755,c_22832,c_25152,c_25946,c_25947,c_27407,c_27473,c_27890]) ).
tcf(c_28218,plain,
( point_equal(i,h)
| ~ incident(h,s) ),
inference(renaming,[status(thm)],[c_28217]) ).
tcf(c_28347,plain,
( ~ incident(h,s)
| ~ incident(a,p) ),
inference(global_subsumption_just,[status(thm)],[c_17291,c_81,c_58,c_440,c_435,c_434,c_443,c_464,c_535,c_14201,c_15730,c_18615,c_20144,c_22755]) ).
tcf(c_28487,plain,
( line_equal(p,q)
| ~ incident(b,q) ),
inference(global_subsumption_just,[status(thm)],[c_17786,c_81,c_61,c_438,c_457,c_702,c_1072,c_13734,c_14383,c_14418,c_15099,c_15095,c_28179]) ).
tcf(c_28599,plain,
( line_equal(o,r)
| ~ incident(e,r) ),
inference(global_subsumption_just,[status(thm)],[c_18490,c_81,c_59,c_442,c_460,c_14094,c_15168]) ).
tcf(c_28745,plain,
( ~ incident(h,s)
| point_equal(h,i) ),
inference(global_subsumption_just,[status(thm)],[c_19169,c_81,c_61,c_59,c_58,c_440,c_439,c_437,c_436,c_435,c_434,c_446,c_445,c_444,c_443,c_442,c_441,c_464,c_463,c_462,c_460,c_458,c_457,c_702,c_1072,c_1559,c_1768,c_11850,c_12568,c_13433,c_13463,c_13734,c_13973,c_14088,c_14094,c_14201,c_14383,c_14852,c_15730,c_18615,c_20144,c_20145,c_22357,c_22755,c_22832,c_23672,c_25156,c_25946,c_27407,c_27413,c_27473,c_27960,c_28347]) ).
tcf(c_28746,plain,
( point_equal(h,i)
| ~ incident(h,s) ),
inference(renaming,[status(thm)],[c_28745]) ).
tcf(c_28755,plain,
( ~ incident(i,l)
| ~ incident(b,s) ),
inference(global_subsumption_just,[status(thm)],[c_19173,c_81,c_62,c_61,c_60,c_58,c_439,c_437,c_435,c_434,c_433,c_447,c_445,c_443,c_441,c_464,c_463,c_462,c_460,c_459,c_457,c_534,c_668,c_671,c_702,c_705,c_708,c_1017,c_1057,c_1081,c_1768,c_3232,c_12143,c_12562,c_12871,c_12868,c_12867,c_12857,c_13182,c_13269,c_13431,c_13464,c_13465,c_13482,c_13665,c_13715,c_13723,c_13734,c_13749,c_14201,c_15251,c_17079,c_19366,c_20144,c_22755,c_23389,c_26369,c_26390,c_27771,c_27960,c_28113]) ).
tcf(c_28865,plain,
( ~ incident(b,s)
| ~ incident(i,p)
| point_equal(b,i) ),
inference(global_subsumption_just,[status(thm)],[c_19184,c_81,c_58,c_440,c_437,c_435,c_434,c_443,c_535,c_1767,c_14201,c_19184,c_20144,c_22755]) ).
tcf(c_28866,plain,
( point_equal(b,i)
| ~ incident(i,p)
| ~ incident(b,s) ),
inference(renaming,[status(thm)],[c_28865]) ).
tcf(c_28903,plain,
( ~ incident(b,o)
| point_equal(c,b) ),
inference(global_subsumption_just,[status(thm)],[c_19722,c_81,c_61,c_433,c_671,c_1057,c_13182]) ).
tcf(c_28904,plain,
( point_equal(c,b)
| ~ incident(b,o) ),
inference(renaming,[status(thm)],[c_28903]) ).
tcf(c_28933,plain,
( ~ incident(b,s)
| point_equal(a,b) ),
inference(global_subsumption_just,[status(thm)],[c_19726,c_81,c_62,c_457,c_708,c_1017,c_15251]) ).
tcf(c_28934,plain,
( point_equal(a,b)
| ~ incident(b,s) ),
inference(renaming,[status(thm)],[c_28933]) ).
tcf(c_29315,plain,
( ~ incident(d,q)
| point_equal(e,d) ),
inference(global_subsumption_just,[status(thm)],[c_21571,c_81,c_57,c_442,c_462,c_16387,c_23586]) ).
tcf(c_29316,plain,
( point_equal(e,d)
| ~ incident(d,q) ),
inference(renaming,[status(thm)],[c_29315]) ).
tcf(c_29347,plain,
( ~ incident(d,s)
| ~ incident(a,p) ),
inference(global_subsumption_just,[status(thm)],[c_21580,c_81,c_60,c_437,c_457,c_1767,c_13431,c_13665,c_15255,c_28347]) ).
tcf(c_29647,plain,
( line_equal(m,s)
| point_equal(d,f)
| ~ incident(d,s) ),
inference(global_subsumption_just,[status(thm)],[c_22754,c_434,c_22754]) ).
tcf(c_29769,plain,
( line_equal(s,m)
| point_equal(f,d)
| ~ incident(d,s) ),
inference(global_subsumption_just,[status(thm)],[c_23588,c_434,c_23588]) ).
tcf(c_29783,plain,
( ~ incident(a,n)
| point_equal(a,b) ),
inference(global_subsumption_just,[status(thm)],[c_23830,c_81,c_62,c_441,c_668,c_12867]) ).
tcf(c_29784,plain,
( point_equal(a,b)
| ~ incident(a,n) ),
inference(renaming,[status(thm)],[c_29783]) ).
tcf(c_30005,plain,
( line_equal(q,p)
| ~ incident(b,q) ),
inference(global_subsumption_just,[status(thm)],[c_25215,c_3378,c_28487]) ).
tcf(c_30450,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,X0_iProver_incident_2)
| ~ incident(h,s)
| ~ incident(i,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_28746,c_412]) ).
tcf(c_30451,plain,
( incident(h,l)
| ~ incident(i,l)
| ~ incident(h,s) ),
inference(instantiation,[status(thm)],[c_30450]) ).
tcf(c_30585,plain,
( line_equal(s,m)
| point_equal(d,f)
| ~ incident(d,s) ),
inference(resolution,[status(thm)],[c_29647,c_414]) ).
tcf(c_30596,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(f,d)
| incident(X0_iProver_incident_1,m)
| ~ incident(d,s)
| ~ incident(X0_iProver_incident_1,s) ),
inference(resolution,[status(thm)],[c_29769,c_411]) ).
tcf(c_30597,plain,
( point_equal(f,d)
| incident(a,m)
| ~ incident(d,s)
| ~ incident(a,s) ),
inference(instantiation,[status(thm)],[c_30596]) ).
tcf(c_30642,plain,
( ~ incident(d,s)
| point_equal(d,f) ),
inference(global_subsumption_just,[status(thm)],[c_30585,c_81,c_57,c_464,c_16183,c_30597]) ).
tcf(c_30643,plain,
( point_equal(d,f)
| ~ incident(d,s) ),
inference(renaming,[status(thm)],[c_30642]) ).
tcf(c_30652,plain,
( point_equal(f,d)
| ~ incident(d,s) ),
inference(resolution,[status(thm)],[c_30643,c_417]) ).
tcf(c_31239,plain,
( incident(c,q)
| incident(c,n)
| incident(a,p) ),
inference(superposition,[status(thm)],[c_24602,c_13736]) ).
tcf(c_31354,plain,
( point_equal(b,c)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_25998,c_14852]) ).
tcf(c_31388,plain,
( incident(b,s)
| incident(b,o)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_27975,c_13771]) ).
tcf(c_31449,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(i,X0_iProver_incident_2)
| ~ incident(i,l)
| ~ incident(a,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_15590,c_412]) ).
tcf(c_31577,plain,
( line_equal(q,o)
| point_equal(e,c)
| incident(c,n)
| incident(a,p)
| ~ incident(e,q)
| ~ incident(c,o) ),
inference(superposition,[status(thm)],[c_31239,c_13575]) ).
tcf(c_31616,plain,
( point_equal(c,b)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_31354,c_417]) ).
tcf(c_31921,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,r)
| ~ line_equal(s,r)
| ~ incident(X0_iProver_incident_1,s) ),
inference(instantiation,[status(thm)],[c_14829]) ).
tcf(c_32342,plain,
( incident(c,p)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_31616,c_13730]) ).
tcf(c_32559,plain,
( incident(h,o)
| ~ line_equal(q,o)
| ~ incident(h,q) ),
inference(instantiation,[status(thm)],[c_16537]) ).
tcf(c_32972,plain,
( incident(h,r)
| ~ line_equal(o,r)
| ~ incident(h,o) ),
inference(instantiation,[status(thm)],[c_13962]) ).
tcf(c_32983,plain,
( incident(i,o)
| ~ point_equal(i,c)
| ~ incident(c,o) ),
inference(instantiation,[status(thm)],[c_17539]) ).
tcf(c_33104,plain,
( incident(b,q)
| incident(c,s)
| point_equal(e,f) ),
inference(global_subsumption_just,[status(thm)],[c_16336,c_81,c_58,c_443,c_442,c_459,c_16249,c_18006,c_21515]) ).
tcf(c_33105,plain,
( point_equal(e,f)
| incident(c,s)
| incident(b,q) ),
inference(renaming,[status(thm)],[c_33104]) ).
tcf(c_33107,plain,
( point_equal(f,e)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_33105,c_417]) ).
tcf(c_33114,plain,
( incident(f,q)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_33107,c_13593]) ).
tcf(c_33195,plain,
( line_equal(q,s)
| point_equal(a,f)
| incident(c,s)
| incident(b,q)
| ~ incident(f,s)
| ~ incident(a,q) ),
inference(superposition,[status(thm)],[c_33114,c_13770]) ).
tcf(c_33696,plain,
( point_equal(i,b)
| ~ incident(i,p)
| ~ incident(b,s) ),
inference(resolution,[status(thm)],[c_28866,c_417]) ).
tcf(c_33698,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,i)
| ~ incident(i,p)
| ~ incident(b,s)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(resolution,[status(thm)],[c_28866,c_416]) ).
tcf(c_33699,plain,
( point_equal(a,i)
| ~ point_equal(a,b)
| ~ incident(i,p)
| ~ incident(b,s) ),
inference(instantiation,[status(thm)],[c_33698]) ).
tcf(c_33973,plain,
( incident(e,l)
| ~ point_equal(e,c)
| ~ incident(c,l) ),
inference(instantiation,[status(thm)],[c_13432]) ).
tcf(c_33997,plain,
( point_equal(g,c)
| ~ point_equal(c,g) ),
inference(instantiation,[status(thm)],[c_17986]) ).
tcf(c_33999,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(g,X0_iProver_incident_2)
| ~ point_equal(g,c)
| ~ incident(c,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_19365]) ).
tcf(c_34003,plain,
( incident(g,l)
| ~ point_equal(g,c)
| ~ incident(c,l) ),
inference(instantiation,[status(thm)],[c_33999]) ).
tcf(c_34325,plain,
( incident(b,r)
| ~ line_equal(p,r)
| ~ incident(b,p) ),
inference(instantiation,[status(thm)],[c_25099]) ).
tcf(c_34531,plain,
( ~ incident(i,o)
| ~ incident(c,s) ),
inference(global_subsumption_just,[status(thm)],[c_19183,c_81,c_59,c_438,c_444,c_442,c_462,c_490,c_12163,c_13187,c_14094,c_17474,c_32559]) ).
tcf(c_35074,plain,
( incident(b,o)
| incident(b,q)
| point_equal(f,d) ),
inference(global_subsumption_just,[status(thm)],[c_19222,c_974,c_30652]) ).
tcf(c_35075,plain,
( point_equal(f,d)
| incident(b,q)
| incident(b,o) ),
inference(renaming,[status(thm)],[c_35074]) ).
tcf(c_35077,plain,
( point_equal(d,f)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_35075,c_417]) ).
tcf(c_35140,plain,
( incident(d,n)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_35077,c_13570]) ).
tcf(c_35273,plain,
( line_equal(p,n)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_35140,c_15378]) ).
tcf(c_35417,plain,
( line_equal(n,p)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_35273,c_414]) ).
tcf(c_35420,plain,
( incident(h,n)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_35273,c_13457]) ).
tcf(c_35451,plain,
( incident(g,p)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_35417,c_13455]) ).
tcf(c_35682,plain,
( line_equal(o,n)
| point_equal(g,h)
| incident(b,q)
| incident(b,o)
| ~ incident(h,o) ),
inference(superposition,[status(thm)],[c_35420,c_13969]) ).
tcf(c_35987,plain,
( incident(b,q)
| incident(b,o)
| ~ incident(i,p)
| ~ incident(h,p) ),
inference(superposition,[status(thm)],[c_35451,c_398]) ).
tcf(c_40207,plain,
( incident(b,r)
| ~ line_equal(s,r)
| ~ incident(b,s) ),
inference(instantiation,[status(thm)],[c_31921]) ).
tcf(c_44133,plain,
( incident(a,r)
| incident(b,o)
| point_equal(e,d) ),
inference(global_subsumption_just,[status(thm)],[c_22470,c_81,c_57,c_445,c_442,c_462,c_3383,c_16387,c_17484,c_17625,c_23586,c_28487]) ).
tcf(c_44134,plain,
( point_equal(e,d)
| incident(b,o)
| incident(a,r) ),
inference(renaming,[status(thm)],[c_44133]) ).
tcf(c_44136,plain,
( point_equal(d,e)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_44134,c_417]) ).
tcf(c_44153,plain,
( incident(d,o)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_44136,c_13576]) ).
tcf(c_44288,plain,
~ incident(i,l),
inference(global_subsumption_just,[status(thm)],[c_31449,c_81,c_61,c_60,c_58,c_57,c_438,c_435,c_434,c_448,c_443,c_464,c_463,c_462,c_460,c_457,c_702,c_705,c_1072,c_1559,c_1799,c_11850,c_12200,c_12568,c_13272,c_13463,c_13466,c_13973,c_14201,c_15730,c_18615,c_20144,c_22755,c_28755,c_30451,c_32983,c_33195,c_34531]) ).
tcf(c_44543,plain,
( line_equal(r,o)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_44153,c_15478]) ).
tcf(c_44583,plain,
( line_equal(o,r)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_44543,c_414]) ).
tcf(c_44610,plain,
( incident(g,r)
| incident(b,o)
| incident(a,r) ),
inference(superposition,[status(thm)],[c_44583,c_13456]) ).
tcf(c_45552,plain,
( ~ incident(b,s)
| ~ incident(i,p) ),
inference(global_subsumption_just,[status(thm)],[c_33696,c_457,c_13437,c_13698,c_28934,c_33699,c_44288]) ).
tcf(c_45553,plain,
( ~ incident(i,p)
| ~ incident(b,s) ),
inference(renaming,[status(thm)],[c_45552]) ).
tcf(c_46226,plain,
( line_equal(s,r)
| point_equal(i,g)
| incident(b,o)
| incident(a,r)
| ~ incident(g,s) ),
inference(superposition,[status(thm)],[c_44610,c_14058]) ).
tcf(c_48107,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(g,X0_iProver_incident_2)
| ~ point_equal(g,h)
| ~ incident(h,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_19365]) ).
tcf(c_53974,plain,
incident(i,r),
inference(superposition,[status(thm)],[c_423,c_419]) ).
tcf(c_53997,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_54148,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(d,X0_iProver_incident_1)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_53997,c_409]) ).
tcf(c_54208,plain,
incident(g,n),
inference(resolution,[status(thm)],[c_419,c_427]) ).
tcf(c_54210,plain,
incident(h,p),
inference(resolution,[status(thm)],[c_419,c_425]) ).
tcf(c_54212,plain,
incident(i,r),
inference(resolution,[status(thm)],[c_419,c_423]) ).
tcf(c_54213,plain,
incident(i,s),
inference(resolution,[status(thm)],[c_419,c_422]) ).
tcf(c_54849,plain,
( line_equal(r,p)
| point_equal(d,i)
| ~ incident(i,p)
| ~ incident(d,r) ),
inference(superposition,[status(thm)],[c_53974,c_54148]) ).
tcf(c_55227,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,n)
| point_equal(X0_iProver_incident_1,g)
| ~ incident(g,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,n)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_54208]) ).
tcf(c_55229,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(X0_iProver_incident_1,h)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_409,c_54210]) ).
tcf(c_56032,plain,
( line_equal(r,p)
| ~ incident(i,p) ),
inference(global_subsumption_just,[status(thm)],[c_54849,c_81,c_61,c_60,c_59,c_437,c_447,c_441,c_464,c_458,c_457,c_671,c_699,c_702,c_1039,c_12200,c_13297,c_14087,c_18615,c_19066,c_21579,c_22023,c_32342,c_35987,c_45553]) ).
tcf(c_56640,plain,
( line_equal(r,n)
| point_equal(i,g)
| ~ incident(i,n)
| ~ incident(g,r) ),
inference(resolution,[status(thm)],[c_55227,c_54212]) ).
tcf(c_57407,plain,
( line_equal(s,p)
| point_equal(i,h)
| ~ incident(i,p)
| ~ incident(h,s) ),
inference(resolution,[status(thm)],[c_55229,c_54213]) ).
tcf(c_60423,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(g,r)
| ~ line_equal(X0_iProver_incident_2,r)
| ~ incident(g,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_60799,plain,
( ~ incident(g,r)
| point_equal(i,g) ),
inference(global_subsumption_just,[status(thm)],[c_56640,c_81,c_61,c_60,c_58,c_439,c_438,c_437,c_435,c_434,c_433,c_447,c_446,c_445,c_443,c_460,c_459,c_458,c_457,c_534,c_1768,c_13431,c_13665,c_14088,c_14201,c_15160,c_15527,c_17079,c_20144,c_22357,c_22755,c_23389,c_26369,c_28041,c_28904,c_31388,c_31577,c_32559,c_32972,c_33973,c_33997,c_34003,c_40207,c_46226]) ).
tcf(c_60800,plain,
( point_equal(i,g)
| ~ incident(g,r) ),
inference(renaming,[status(thm)],[c_60799]) ).
tcf(c_64296,plain,
( incident(g,r)
| ~ line_equal(o,r)
| ~ incident(g,o) ),
inference(instantiation,[status(thm)],[c_60423]) ).
tcf(c_67165,plain,
( ~ incident(i,p)
| point_equal(i,h) ),
inference(global_subsumption_just,[status(thm)],[c_57407,c_81,c_62,c_59,c_438,c_446,c_443,c_464,c_461,c_460,c_457,c_1799,c_3232,c_12237,c_12800,c_13435,c_14856,c_17887,c_21782,c_23671,c_25084,c_28137,c_28218,c_34325,c_56032]) ).
tcf(c_67166,plain,
( point_equal(i,h)
| ~ incident(i,p) ),
inference(renaming,[status(thm)],[c_67165]) ).
tcf(c_411965,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_411967,plain,
incident(d,r),
inference(superposition,[status(thm)],[c_423,c_420]) ).
tcf(c_411971,plain,
incident(b,n),
inference(superposition,[status(thm)],[c_427,c_421]) ).
tcf(c_411976,plain,
incident(a,s),
inference(superposition,[status(thm)],[c_422,c_421]) ).
tcf(c_412038,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_1: iProver_incident_1,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_1: iProver_incident_1,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_1: iProver_incident_1,X5_iProver_incident_2: iProver_incident_2,X6_iProver_incident_2: iProver_incident_2] :
( line_equal(X6_iProver_incident_2,X2_iProver_incident_2)
| line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| colinear(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1,sK0(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1))
| ~ colinear(c,X1_iProver_incident_1,X5_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,X0_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_2)
| ~ colinear(b,X2_iProver_incident_1,X5_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,X0_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(a,X2_iProver_incident_1,X4_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,X1_iProver_incident_1,X3_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_429,c_410]) ).
tcf(c_412129,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(d,X0_iProver_incident_1)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_411965,c_409]) ).
tcf(c_412131,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(d,X0_iProver_incident_2)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_411965,c_411]) ).
tcf(c_412160,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(d,X0_iProver_incident_2)
| ~ line_equal(r,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_411967,c_411]) ).
tcf(c_412207,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_411971,c_411]) ).
tcf(c_412785,plain,
( line_equal(s,p)
| point_equal(d,a)
| ~ incident(d,s)
| ~ incident(a,p) ),
inference(superposition,[status(thm)],[c_411976,c_412129]) ).
tcf(c_413834,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| colinear(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1,sK0(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1))
| ~ colinear(c,e,X2_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,d,X1_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(b,f,X2_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,e,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_428,c_412038]) ).
tcf(c_413926,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,q)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| line_equal(X1_iProver_incident_2,X3_iProver_incident_2)
| colinear(X1_iProver_incident_1,h,X0_iProver_incident_1,sK0(X1_iProver_incident_1,h,X0_iProver_incident_1))
| ~ colinear(b,d,h,X4_iProver_incident_2)
| ~ colinear(c,e,X1_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(c,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(b,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_424,c_413834]) ).
tcf(c_413927,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2] :
( line_equal(X3_iProver_incident_2,s)
| line_equal(X2_iProver_incident_2,q)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| colinear(X0_iProver_incident_1,h,i,sK0(X0_iProver_incident_1,h,i))
| ~ colinear(c,d,i,X3_iProver_incident_2)
| ~ colinear(b,d,h,X2_iProver_incident_2)
| ~ colinear(c,e,X0_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(b,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_422,c_413926]) ).
tcf(c_413970,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2] :
( line_equal(n,X2_iProver_incident_2)
| line_equal(X1_iProver_incident_2,s)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X2_iProver_incident_2)
| ~ colinear(c,d,i,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_427,c_413927]) ).
tcf(c_413999,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(n,X1_iProver_incident_2)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_423,c_413970]) ).
tcf(c_414047,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,X0_iProver_incident_2)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_425,c_413999]) ).
tcf(c_414048,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| colinear(g,h,i,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_426,c_414047]) ).
tcf(c_414223,plain,
( ~ incident(d,s)
| ~ incident(a,p) ),
inference(global_subsumption_just,[status(thm)],[c_412785,c_29347]) ).
tcf(c_414231,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o) ),
inference(global_subsumption_just,[status(thm)],[c_414048,c_532,c_531,c_540]) ).
tcf(c_414234,plain,
( line_equal(p,q)
| line_equal(n,o)
| incident(d,s) ),
inference(superposition,[status(thm)],[c_414231,c_412160]) ).
tcf(c_414282,plain,
( line_equal(n,o)
| incident(d,s)
| incident(d,q) ),
inference(superposition,[status(thm)],[c_414234,c_412131]) ).
tcf(c_414309,plain,
( incident(d,s)
| incident(d,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_414282,c_412207]) ).
tcf(c_414959,plain,
( incident(d,q)
| incident(b,o)
| ~ incident(a,p) ),
inference(superposition,[status(thm)],[c_414309,c_414223]) ).
tcf(c_420832,plain,
( incident(d,q)
| ~ incident(a,p) ),
inference(global_subsumption_just,[status(thm)],[c_414959,c_81,c_61,c_58,c_438,c_435,c_434,c_445,c_443,c_464,c_462,c_457,c_702,c_1072,c_1559,c_3383,c_11850,c_12568,c_13463,c_13973,c_14201,c_14383,c_15730,c_18615,c_20144,c_22755,c_25920]) ).
tcf(c_725982,plain,
incident(c,l),
inference(superposition,[status(thm)],[c_429,c_419]) ).
tcf(c_725986,plain,
incident(h,p),
inference(superposition,[status(thm)],[c_425,c_419]) ).
tcf(c_725987,plain,
incident(h,q),
inference(superposition,[status(thm)],[c_424,c_419]) ).
tcf(c_726009,plain,
incident(b,l),
inference(superposition,[status(thm)],[c_429,c_420]) ).
tcf(c_726013,plain,
incident(d,p),
inference(superposition,[status(thm)],[c_425,c_420]) ).
tcf(c_726026,plain,
incident(b,n),
inference(superposition,[status(thm)],[c_427,c_421]) ).
tcf(c_726027,plain,
incident(c,o),
inference(superposition,[status(thm)],[c_426,c_421]) ).
tcf(c_726028,plain,
incident(b,p),
inference(superposition,[status(thm)],[c_425,c_421]) ).
tcf(c_726029,plain,
incident(a,q),
inference(superposition,[status(thm)],[c_424,c_421]) ).
tcf(c_726030,plain,
incident(c,r),
inference(superposition,[status(thm)],[c_423,c_421]) ).
tcf(c_726031,plain,
incident(a,s),
inference(superposition,[status(thm)],[c_422,c_421]) ).
tcf(c_726081,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(c,X0_iProver_incident_1)
| ~ incident(c,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_725982,c_409]) ).
tcf(c_726085,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(h,X0_iProver_incident_1)
| ~ incident(h,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_725986,c_409]) ).
tcf(c_726103,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_1: iProver_incident_1,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_1: iProver_incident_1,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_1: iProver_incident_1,X5_iProver_incident_2: iProver_incident_2,X6_iProver_incident_2: iProver_incident_2] :
( line_equal(X6_iProver_incident_2,X2_iProver_incident_2)
| line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| colinear(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1,sK0(X5_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_1))
| ~ colinear(c,X1_iProver_incident_1,X5_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,X0_iProver_incident_1,X4_iProver_incident_1,X6_iProver_incident_2)
| ~ colinear(b,X2_iProver_incident_1,X5_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,X0_iProver_incident_1,X3_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(a,X2_iProver_incident_1,X4_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,X1_iProver_incident_1,X3_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(X0_iProver_incident_1,X1_iProver_incident_1,X2_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_429,c_410]) ).
tcf(c_726116,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,l)
| point_equal(b,X0_iProver_incident_1)
| ~ incident(b,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,l)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_726009,c_409]) ).
tcf(c_726198,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,p)
| point_equal(d,X0_iProver_incident_1)
| ~ incident(d,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,p)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_726013,c_409]) ).
tcf(c_726259,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(n,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_726026,c_411]) ).
tcf(c_726265,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,o)
| ~ point_equal(X0_iProver_incident_1,c) ),
inference(superposition,[status(thm)],[c_726027,c_412]) ).
tcf(c_726273,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,p)
| ~ point_equal(X0_iProver_incident_1,b) ),
inference(superposition,[status(thm)],[c_726028,c_412]) ).
tcf(c_726274,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b,X0_iProver_incident_2)
| ~ line_equal(p,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_726028,c_411]) ).
tcf(c_726297,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a,X0_iProver_incident_2)
| ~ line_equal(q,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_726029,c_411]) ).
tcf(c_726302,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c,X0_iProver_incident_2)
| ~ line_equal(r,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_726030,c_411]) ).
tcf(c_726410,plain,
( line_equal(s,l)
| point_equal(c,a)
| ~ incident(c,s)
| ~ incident(a,l) ),
inference(superposition,[status(thm)],[c_726031,c_726081]) ).
tcf(c_726520,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(q,p)
| point_equal(h,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,q)
| ~ incident(X0_iProver_incident_1,p) ),
inference(superposition,[status(thm)],[c_725987,c_726085]) ).
tcf(c_726539,plain,
( ~ incident(c,s)
| point_equal(c,a) ),
inference(global_subsumption_just,[status(thm)],[c_726410,c_81,c_62,c_457,c_708,c_12070]) ).
tcf(c_726540,plain,
( point_equal(c,a)
| ~ incident(c,s) ),
inference(renaming,[status(thm)],[c_726539]) ).
tcf(c_726580,plain,
( line_equal(o,l)
| point_equal(b,c)
| ~ incident(c,l)
| ~ incident(b,o) ),
inference(superposition,[status(thm)],[c_726027,c_726116]) ).
tcf(c_726870,plain,
( line_equal(r,p)
| point_equal(d,c)
| ~ incident(d,r)
| ~ incident(c,p) ),
inference(superposition,[status(thm)],[c_726030,c_726198]) ).
tcf(c_726923,plain,
( line_equal(q,p)
| point_equal(h,b)
| ~ incident(b,q) ),
inference(superposition,[status(thm)],[c_726028,c_726520]) ).
tcf(c_726934,plain,
( line_equal(q,p)
| ~ incident(b,q) ),
inference(global_subsumption_just,[status(thm)],[c_726923,c_30005]) ).
tcf(c_727256,plain,
( ~ incident(b,o)
| point_equal(b,c) ),
inference(global_subsumption_just,[status(thm)],[c_726580,c_81,c_61,c_433,c_671,c_12198]) ).
tcf(c_727257,plain,
( point_equal(b,c)
| ~ incident(b,o) ),
inference(renaming,[status(thm)],[c_727256]) ).
tcf(c_728035,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_1: iProver_incident_1,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2,X5_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,X1_iProver_incident_2)
| line_equal(X3_iProver_incident_2,X5_iProver_incident_2)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| colinear(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1,sK0(X2_iProver_incident_1,X0_iProver_incident_1,X1_iProver_incident_1))
| ~ colinear(c,e,X2_iProver_incident_1,X5_iProver_incident_2)
| ~ colinear(c,d,X1_iProver_incident_1,X4_iProver_incident_2)
| ~ colinear(b,f,X2_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(b,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(a,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,e,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_428,c_726103]) ).
tcf(c_728090,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_1: iProver_incident_1,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2,X4_iProver_incident_2: iProver_incident_2] :
( line_equal(X4_iProver_incident_2,q)
| line_equal(X2_iProver_incident_2,X0_iProver_incident_2)
| line_equal(X1_iProver_incident_2,X3_iProver_incident_2)
| colinear(X1_iProver_incident_1,h,X0_iProver_incident_1,sK0(X1_iProver_incident_1,h,X0_iProver_incident_1))
| ~ colinear(b,d,h,X4_iProver_incident_2)
| ~ colinear(c,e,X1_iProver_incident_1,X3_iProver_incident_2)
| ~ colinear(c,d,X0_iProver_incident_1,X2_iProver_incident_2)
| ~ colinear(b,f,X1_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(a,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_424,c_728035]) ).
tcf(c_728091,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2,X3_iProver_incident_2: iProver_incident_2] :
( line_equal(X3_iProver_incident_2,s)
| line_equal(X2_iProver_incident_2,q)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| colinear(X0_iProver_incident_1,h,i,sK0(X0_iProver_incident_1,h,i))
| ~ colinear(c,d,i,X3_iProver_incident_2)
| ~ colinear(b,d,h,X2_iProver_incident_2)
| ~ colinear(c,e,X0_iProver_incident_1,X1_iProver_incident_2)
| ~ colinear(b,f,X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_422,c_728090]) ).
tcf(c_728116,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2] :
( line_equal(n,X2_iProver_incident_2)
| line_equal(X1_iProver_incident_2,s)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X2_iProver_incident_2)
| ~ colinear(c,d,i,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_427,c_728091]) ).
tcf(c_728117,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(n,X1_iProver_incident_2)
| line_equal(X0_iProver_incident_2,q)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X1_iProver_incident_2)
| ~ colinear(b,d,h,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_423,c_728116]) ).
tcf(c_728118,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,X0_iProver_incident_2)
| colinear(g,h,i,sK0(g,h,i))
| ~ colinear(c,e,g,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_425,c_728117]) ).
tcf(c_728119,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o)
| colinear(g,h,i,sK0(g,h,i)) ),
inference(superposition,[status(thm)],[c_426,c_728118]) ).
tcf(c_728288,plain,
( line_equal(r,p)
| ~ incident(c,p) ),
inference(global_subsumption_just,[status(thm)],[c_726870,c_81,c_59,c_447,c_458,c_14087,c_21579]) ).
tcf(c_728295,plain,
( line_equal(r,s)
| line_equal(p,q)
| line_equal(n,o) ),
inference(global_subsumption_just,[status(thm)],[c_728119,c_532,c_531,c_540]) ).
tcf(c_728297,plain,
( line_equal(p,q)
| line_equal(n,o)
| incident(c,s) ),
inference(superposition,[status(thm)],[c_728295,c_726302]) ).
tcf(c_728338,plain,
( line_equal(n,o)
| incident(c,s)
| incident(b,q) ),
inference(superposition,[status(thm)],[c_728297,c_726274]) ).
tcf(c_728347,plain,
( incident(c,s)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_728338,c_726259]) ).
tcf(c_728396,plain,
( point_equal(c,a)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_728347,c_726540]) ).
tcf(c_729303,plain,
( point_equal(a,c)
| incident(b,q)
| incident(b,o) ),
inference(superposition,[status(thm)],[c_728396,c_417]) ).
tcf(c_729466,plain,
( incident(b,q)
| incident(b,o)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_729303,c_726265]) ).
tcf(c_730552,plain,
( line_equal(q,p)
| incident(b,o)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_729466,c_726934]) ).
tcf(c_731735,plain,
( incident(b,o)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_730552,c_726297]) ).
tcf(c_733606,plain,
( point_equal(b,c)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_731735,c_727257]) ).
tcf(c_734304,plain,
( point_equal(c,b)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_733606,c_417]) ).
tcf(c_734653,plain,
( incident(c,p)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_734304,c_726273]) ).
tcf(c_737947,plain,
( line_equal(r,p)
| incident(a,p)
| incident(a,o) ),
inference(superposition,[status(thm)],[c_734653,c_728288]) ).
tcf(c_773231,plain,
incident(g,n),
inference(superposition,[status(thm)],[c_427,c_419]) ).
tcf(c_773233,plain,
incident(h,p),
inference(superposition,[status(thm)],[c_425,c_419]) ).
tcf(c_773235,plain,
incident(i,r),
inference(superposition,[status(thm)],[c_423,c_419]) ).
tcf(c_773241,plain,
point_equal(g,g),
inference(superposition,[status(thm)],[c_773231,c_418]) ).
tcf(c_773252,plain,
point_equal(h,h),
inference(superposition,[status(thm)],[c_773233,c_418]) ).
tcf(c_773307,plain,
point_equal(i,i),
inference(superposition,[status(thm)],[c_773235,c_418]) ).
tcf(c_773456,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(h,X0_iProver_incident_1))
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773252,c_407]) ).
tcf(c_773476,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(X0_iProver_incident_1,g))
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773241,c_408]) ).
tcf(c_773477,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(X0_iProver_incident_1,h))
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773252,c_408]) ).
tcf(c_773646,plain,
( incident(h,sK1(i,h))
| ~ point_equal(i,i)
| ~ point_equal(h,h) ),
inference(instantiation,[status(thm)],[c_407]) ).
tcf(c_773662,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(i,X0_iProver_incident_1))
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773307,c_407]) ).
tcf(c_773974,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X1_iProver_incident_1,sK1(h,X0_iProver_incident_1))
| ~ point_equal(X1_iProver_incident_1,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773456,c_412]) ).
tcf(c_773975,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,X0_iProver_incident_2)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1)
| ~ line_equal(sK1(h,X0_iProver_incident_1),X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_773456,c_411]) ).
tcf(c_774003,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X1_iProver_incident_1,sK1(X0_iProver_incident_1,g))
| ~ point_equal(X1_iProver_incident_1,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773476,c_412]) ).
tcf(c_774012,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X1_iProver_incident_1,sK1(X0_iProver_incident_1,h))
| ~ point_equal(X1_iProver_incident_1,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773477,c_412]) ).
tcf(c_774013,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,X0_iProver_incident_2)
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1)
| ~ line_equal(sK1(X0_iProver_incident_1,h),X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_773477,c_411]) ).
tcf(c_774079,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(sK1(i,X0_iProver_incident_1),sK1(i,X0_iProver_incident_1))
| ~ point_equal(X0_iProver_incident_1,X0_iProver_incident_1) ),
inference(superposition,[status(thm)],[c_773662,c_415]) ).
tcf(c_774184,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(h,X1_iProver_incident_2)
| ~ incident(h,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_411]) ).
tcf(c_775218,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(h,X0_iProver_incident_2)
| ~ incident(h,sK1(i,h))
| ~ line_equal(sK1(i,h),X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_774184]) ).
tcf(c_790684,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(h,g))
| ~ point_equal(X0_iProver_incident_1,g) ),
inference(superposition,[status(thm)],[c_773241,c_773974]) ).
tcf(c_791607,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(sK1(h,g),sK1(h,g))
| ~ point_equal(X0_iProver_incident_1,g) ),
inference(superposition,[status(thm)],[c_790684,c_415]) ).
tcf(c_791990,plain,
line_equal(sK1(h,g),sK1(h,g)),
inference(superposition,[status(thm)],[c_773241,c_791607]) ).
tcf(c_792655,plain,
( incident(g,sK1(h,g))
| ~ point_equal(g,g) ),
inference(superposition,[status(thm)],[c_791990,c_773975]) ).
tcf(c_792767,plain,
incident(g,sK1(h,g)),
inference(global_subsumption_just,[status(thm)],[c_792655,c_13406,c_792655]) ).
tcf(c_792769,plain,
( ~ incident(i,sK1(h,g))
| ~ incident(h,sK1(h,g)) ),
inference(superposition,[status(thm)],[c_792767,c_398]) ).
tcf(c_792860,plain,
( ~ point_equal(h,h)
| ~ incident(i,sK1(h,g)) ),
inference(superposition,[status(thm)],[c_773476,c_792769]) ).
tcf(c_792862,plain,
~ incident(i,sK1(h,g)),
inference(global_subsumption_just,[status(thm)],[c_792860,c_13417,c_792860]) ).
tcf(c_792864,plain,
~ point_equal(i,g),
inference(superposition,[status(thm)],[c_790684,c_792862]) ).
tcf(c_796388,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(h,g))
| ~ point_equal(X0_iProver_incident_1,h) ),
inference(superposition,[status(thm)],[c_773252,c_774003]) ).
tcf(c_797184,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,sK1(i,h))
| ~ point_equal(X0_iProver_incident_1,i) ),
inference(superposition,[status(thm)],[c_773307,c_774012]) ).
tcf(c_797747,plain,
( incident(i,sK1(i,h))
| ~ point_equal(i,i)
| ~ point_equal(h,h) ),
inference(superposition,[status(thm)],[c_774079,c_774013]) ).
tcf(c_798050,plain,
~ point_equal(i,h),
inference(superposition,[status(thm)],[c_796388,c_792862]) ).
tcf(c_798490,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(sK1(i,h),sK1(i,h))
| ~ point_equal(X0_iProver_incident_1,i) ),
inference(superposition,[status(thm)],[c_797184,c_415]) ).
tcf(c_799181,plain,
line_equal(sK1(i,h),sK1(i,h)),
inference(superposition,[status(thm)],[c_773307,c_798490]) ).
tcf(c_799670,plain,
( incident(i,sK1(i,h))
| ~ point_equal(i,i) ),
inference(superposition,[status(thm)],[c_799181,c_774013]) ).
tcf(c_800043,plain,
incident(i,sK1(i,h)),
inference(global_subsumption_just,[status(thm)],[c_799670,c_13417,c_13480,c_797747]) ).
tcf(c_800047,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(i,X0_iProver_incident_2)
| ~ line_equal(sK1(i,h),X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_800043,c_411]) ).
tcf(c_800060,plain,
! [X0_iProver_incident_2: iProver_incident_2] : ~ line_equal(sK1(i,h),X0_iProver_incident_2),
inference(global_subsumption_just,[status(thm)],[c_800047,c_81,c_61,c_398,c_439,c_438,c_436,c_447,c_446,c_445,c_441,c_457,c_671,c_3383,c_12472,c_13417,c_13433,c_13480,c_13734,c_17833,c_19924,c_22023,c_25087,c_28487,c_28599,c_29316,c_29784,c_32559,c_35682,c_48107,c_60800,c_64296,c_67166,c_420832,c_737947,c_773646,c_775218,c_792864,c_798050,c_800047]) ).
tcf(c_800065,plain,
$false,
inference(superposition,[status(thm)],[c_799181,c_800060]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO168+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/10.37 % Computer : n019.cluster.edu
% 0.10/10.37 % Model : x86_64 x86_64
% 0.10/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.37 % Memory : 8046.5625MB
% 0.10/10.37 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Wed Sep 23 11:14:54 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/10.42 Running first-order theorem proving
% 0.14/10.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/10.43
% 0.14/10.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/10.43
% 0.14/10.43 % Detected problem language: tptp
% 0.14/10.44 % Proving...
% 262.12/45.63 % SZS status Started for theBenchmark.p
% 262.12/45.63 % SZS status Theorem for theBenchmark.p
% 262.12/45.63
% 262.12/45.63 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 262.12/45.63
% 262.12/45.63 % ------ iProver source info
% 262.12/45.63
% 262.12/45.63 % git: date: 2026-07-19 20:42:38 +0200
% 262.12/45.63 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 262.12/45.63 % git: non_committed_changes: false
% 262.12/45.63
% 262.12/45.63 % ------ Parsing...
% 262.12/45.63 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 262.12/45.63
% 262.12/45.63 % ------ Preprocessing... sf_s rm: 1 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 262.12/45.63
% 262.12/45.63 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 % ------ Problem Properties
% 262.12/45.63
% 262.12/45.63 %
% 262.12/45.63 % clauses 32
% 262.12/45.63 % conjectures 0
% 262.12/45.63 % EPR 27
% 262.12/45.63 % Horn 30
% 262.12/45.63 % unary 14
% 262.12/45.63 % binary 7
% 262.12/45.63 % lits 73
% 262.12/45.63 % lits eq 0
% 262.12/45.63 % fd_pure 0
% 262.12/45.63 % fd_pseudo 0
% 262.12/45.63 % fd_cond 0
% 262.12/45.63 % fd_pseudo_cond 0
% 262.12/45.63 % AC symbols 0
% 262.12/45.63
% 262.12/45.63 % ------ Input Options Time Limit: Unbounded
% 262.12/45.63
% 262.12/45.63
% 262.12/45.63 % ------
% 262.12/45.63 % Current options:
% 262.12/45.63 % ------
% 262.12/45.63
% 262.12/45.63
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 262.12/45.63 %
% 262.12/45.63
% 262.12/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % ------ Proving...
% 233.10/45.63 %
% 233.10/45.63
% 233.10/45.63 % SZS status Theorem for theBenchmark.p
% 233.10/45.63
% 233.10/45.63 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 233.10/45.64
% 233.10/45.64
%------------------------------------------------------------------------------