%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO169+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:20:04 PM UTC 2026
% Result : Theorem 6.75s 7.02s
% Output : CNFRefutation 8.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 50
% Syntax : Number of formulae : 766 ( 115 unt; 0 def)
% Number of atoms : 2514 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 3159 (1411 ~;1711 |; 18 &)
% ( 0 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 6 usr; 4 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 551 ( 0 sgn 551 !; 0 ?; 457 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ( incident(ab,X0)
& incident(ac,X0)
& incident(bc,X0)
& line_equal(X0,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_normal) ).
fof(f2,axiom,
( ( incident(c1,a2b2)
& incident(b1,a2c2)
& incident(a1,b2c2) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1in2) ).
fof(f3,axiom,
( ( incident(c2,a1b1)
& incident(b2,a1c1)
& incident(a2,b1c1) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2in1) ).
fof(f4,axiom,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap_a) ).
fof(f5,axiom,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap_b) ).
fof(f6,axiom,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap_c) ).
fof(f7,axiom,
incident(a1,a1b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1b1) ).
fof(f8,axiom,
incident(b1,a1b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1a1) ).
fof(f9,axiom,
incident(a2,a2b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2b2) ).
fof(f10,axiom,
incident(b2,a2b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2a2) ).
fof(f11,axiom,
incident(a1,a1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1c1) ).
fof(f12,axiom,
incident(c1,a1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic1a1) ).
fof(f13,axiom,
incident(a2,a2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2c2) ).
fof(f14,axiom,
incident(c2,a2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic2a2) ).
fof(f15,axiom,
incident(c1,b1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic1b1) ).
fof(f16,axiom,
incident(b1,b1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1c1) ).
fof(f17,axiom,
incident(c2,b2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic2b2) ).
fof(f18,axiom,
incident(b2,b2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2c2) ).
fof(f19,axiom,
incident(o,oa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iooa) ).
fof(f20,axiom,
incident(o,ob),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ioob) ).
fof(f21,axiom,
incident(o,oc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iooc) ).
fof(f22,axiom,
incident(a1,oa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1oa) ).
fof(f23,axiom,
incident(a2,oa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2oa) ).
fof(f24,axiom,
incident(b1,ob),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1ob) ).
fof(f25,axiom,
incident(b2,ob),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2ob) ).
fof(f26,axiom,
incident(c1,oc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic1oc) ).
fof(f27,axiom,
incident(c2,oc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic2oc) ).
fof(f28,axiom,
incident(bc,b1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ibc1) ).
fof(f29,axiom,
incident(bc,b2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ibc2) ).
fof(f30,axiom,
incident(ac,a1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iac1) ).
fof(f31,axiom,
incident(ac,a2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iac2) ).
fof(f32,axiom,
incident(ab,a1b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iab1) ).
fof(f33,axiom,
incident(ab,a2b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iab2) ).
fof(f34,axiom,
! [X0] :
( ( incident(c1,X0)
& incident(b1,X0)
& incident(a1,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',triangle1) ).
fof(f35,axiom,
! [X0] :
( ( incident(c2,X0)
& incident(b2,X0)
& incident(a2,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',triangle2) ).
fof(f36,axiom,
( point_equal(a2,a1)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notaa) ).
fof(f37,axiom,
( point_equal(b2,b1)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notbb) ).
fof(f38,axiom,
( point_equal(c2,c1)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notcc) ).
fof(f39,axiom,
( line_equal(b1c1,b2c2)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notbc) ).
fof(f40,axiom,
( line_equal(a1c1,a2c2)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notac) ).
fof(f41,axiom,
( line_equal(a1b1,a2b2)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notab) ).
fof(f43,axiom,
! [X0,X1] :
( point_equal(X0,X1)
=> point_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_point_equal) ).
fof(f44,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(f45,axiom,
! [X0,X1] :
( incident(X0,X1)
=> line_equal(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_line_equal) ).
fof(f46,axiom,
! [X0,X1] :
( line_equal(X0,X1)
=> line_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_line_equal) ).
fof(f47,axiom,
! [X0,X1,X2] :
( ( line_equal(X1,X2)
& line_equal(X0,X1) )
=> line_equal(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_line_equal) ).
fof(f48,axiom,
! [X0,X1,X2] :
( ( incident(X1,X2)
& point_equal(X0,X1) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pcon) ).
fof(f49,axiom,
! [X0,X1,X2] :
( ( line_equal(X1,X2)
& incident(X0,X1) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcon) ).
fof(f50,axiom,
! [X0,X1,X2,X3] :
( ( incident(X1,X3)
& incident(X1,X2)
& incident(X0,X3)
& incident(X0,X2) )
=> ( line_equal(X2,X3)
| point_equal(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique) ).
fof(f51,conjecture,
goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f52,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f53,plain,
~ goal,
inference(flattening,[],[f52]) ).
fof(f54,plain,
! [X0] :
( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0)
| goal ),
inference(ennf_transformation,[],[f1]) ).
fof(f55,plain,
! [X0] :
( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0)
| goal ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
( ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2)
| goal ),
inference(ennf_transformation,[],[f2]) ).
fof(f57,plain,
( ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2)
| goal ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
( ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1)
| goal ),
inference(ennf_transformation,[],[f3]) ).
fof(f59,plain,
( ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1)
| goal ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
! [X0] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0)
| goal ),
inference(ennf_transformation,[],[f34]) ).
fof(f61,plain,
! [X0] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0)
| goal ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0] :
( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0)
| goal ),
inference(ennf_transformation,[],[f35]) ).
fof(f63,plain,
! [X0] :
( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0)
| goal ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
( ~ point_equal(a2,a1)
| goal ),
inference(ennf_transformation,[],[f36]) ).
fof(f65,plain,
( ~ point_equal(b2,b1)
| goal ),
inference(ennf_transformation,[],[f37]) ).
fof(f66,plain,
( ~ point_equal(c2,c1)
| goal ),
inference(ennf_transformation,[],[f38]) ).
fof(f67,plain,
( ~ line_equal(b1c1,b2c2)
| goal ),
inference(ennf_transformation,[],[f39]) ).
fof(f68,plain,
( ~ line_equal(a1c1,a2c2)
| goal ),
inference(ennf_transformation,[],[f40]) ).
fof(f69,plain,
( ~ line_equal(a1b1,a2b2)
| goal ),
inference(ennf_transformation,[],[f41]) ).
fof(f71,plain,
! [X0,X1] :
( ~ point_equal(X0,X1)
| point_equal(X1,X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f72,plain,
! [X0,X1,X2] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(ennf_transformation,[],[f44]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line_equal(X1,X1) ),
inference(ennf_transformation,[],[f45]) ).
fof(f75,plain,
! [X0,X1] :
( ~ line_equal(X0,X1)
| line_equal(X1,X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ line_equal(X1,X2)
| ~ line_equal(X0,X1)
| line_equal(X0,X2) ),
inference(ennf_transformation,[],[f47]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ line_equal(X1,X2)
| ~ line_equal(X0,X1)
| line_equal(X0,X2) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ incident(X1,X2)
| ~ point_equal(X0,X1)
| incident(X0,X2) ),
inference(ennf_transformation,[],[f48]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ incident(X1,X2)
| ~ point_equal(X0,X1)
| incident(X0,X2) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(ennf_transformation,[],[f49]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ~ incident(X1,X3)
| ~ incident(X1,X2)
| ~ incident(X0,X3)
| ~ incident(X0,X2)
| line_equal(X2,X3)
| point_equal(X0,X1) ),
inference(ennf_transformation,[],[f50]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( ~ incident(X1,X3)
| ~ incident(X1,X2)
| ~ incident(X0,X3)
| ~ incident(X0,X2)
| line_equal(X2,X3)
| point_equal(X0,X1) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0] :
( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0)
| goal ),
inference(cnf_transformation,[],[f55]) ).
fof(f85,plain,
( ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2)
| goal ),
inference(cnf_transformation,[],[f57]) ).
fof(f86,plain,
( ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1)
| goal ),
inference(cnf_transformation,[],[f59]) ).
fof(f87,plain,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
inference(cnf_transformation,[],[f4]) ).
fof(f88,plain,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f89,plain,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
inference(cnf_transformation,[],[f6]) ).
fof(f90,plain,
incident(a1,a1b1),
inference(cnf_transformation,[],[f7]) ).
fof(f91,plain,
incident(b1,a1b1),
inference(cnf_transformation,[],[f8]) ).
fof(f92,plain,
incident(a2,a2b2),
inference(cnf_transformation,[],[f9]) ).
fof(f93,plain,
incident(b2,a2b2),
inference(cnf_transformation,[],[f10]) ).
fof(f94,plain,
incident(a1,a1c1),
inference(cnf_transformation,[],[f11]) ).
fof(f95,plain,
incident(c1,a1c1),
inference(cnf_transformation,[],[f12]) ).
fof(f96,plain,
incident(a2,a2c2),
inference(cnf_transformation,[],[f13]) ).
fof(f97,plain,
incident(c2,a2c2),
inference(cnf_transformation,[],[f14]) ).
fof(f98,plain,
incident(c1,b1c1),
inference(cnf_transformation,[],[f15]) ).
fof(f99,plain,
incident(b1,b1c1),
inference(cnf_transformation,[],[f16]) ).
fof(f100,plain,
incident(c2,b2c2),
inference(cnf_transformation,[],[f17]) ).
fof(f101,plain,
incident(b2,b2c2),
inference(cnf_transformation,[],[f18]) ).
fof(f102,plain,
incident(o,oa),
inference(cnf_transformation,[],[f19]) ).
fof(f103,plain,
incident(o,ob),
inference(cnf_transformation,[],[f20]) ).
fof(f104,plain,
incident(o,oc),
inference(cnf_transformation,[],[f21]) ).
fof(f105,plain,
incident(a1,oa),
inference(cnf_transformation,[],[f22]) ).
fof(f106,plain,
incident(a2,oa),
inference(cnf_transformation,[],[f23]) ).
fof(f107,plain,
incident(b1,ob),
inference(cnf_transformation,[],[f24]) ).
fof(f108,plain,
incident(b2,ob),
inference(cnf_transformation,[],[f25]) ).
fof(f109,plain,
incident(c1,oc),
inference(cnf_transformation,[],[f26]) ).
fof(f110,plain,
incident(c2,oc),
inference(cnf_transformation,[],[f27]) ).
fof(f111,plain,
incident(bc,b1c1),
inference(cnf_transformation,[],[f28]) ).
fof(f112,plain,
incident(bc,b2c2),
inference(cnf_transformation,[],[f29]) ).
fof(f113,plain,
incident(ac,a1c1),
inference(cnf_transformation,[],[f30]) ).
fof(f114,plain,
incident(ac,a2c2),
inference(cnf_transformation,[],[f31]) ).
fof(f115,plain,
incident(ab,a1b1),
inference(cnf_transformation,[],[f32]) ).
fof(f116,plain,
incident(ab,a2b2),
inference(cnf_transformation,[],[f33]) ).
fof(f117,plain,
! [X0] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0)
| goal ),
inference(cnf_transformation,[],[f61]) ).
fof(f118,plain,
! [X0] :
( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0)
| goal ),
inference(cnf_transformation,[],[f63]) ).
fof(f119,plain,
( ~ point_equal(a2,a1)
| goal ),
inference(cnf_transformation,[],[f64]) ).
fof(f120,plain,
( ~ point_equal(b2,b1)
| goal ),
inference(cnf_transformation,[],[f65]) ).
fof(f121,plain,
( ~ point_equal(c2,c1)
| goal ),
inference(cnf_transformation,[],[f66]) ).
fof(f122,plain,
( ~ line_equal(b1c1,b2c2)
| goal ),
inference(cnf_transformation,[],[f67]) ).
fof(f123,plain,
( ~ line_equal(a1c1,a2c2)
| goal ),
inference(cnf_transformation,[],[f68]) ).
fof(f124,plain,
( ~ line_equal(a1b1,a2b2)
| goal ),
inference(cnf_transformation,[],[f69]) ).
fof(f126,plain,
! [X0,X1] :
( ~ point_equal(X0,X1)
| point_equal(X1,X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f127,plain,
! [X2,X0,X1] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f128,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line_equal(X1,X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f129,plain,
! [X0,X1] :
( ~ line_equal(X0,X1)
| line_equal(X1,X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ line_equal(X1,X2)
| ~ line_equal(X0,X1)
| line_equal(X0,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ incident(X1,X2)
| ~ point_equal(X0,X1)
| incident(X0,X2) ),
inference(cnf_transformation,[],[f79]) ).
fof(f132,plain,
! [X2,X0,X1] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(cnf_transformation,[],[f81]) ).
fof(f133,plain,
! [X2,X3,X0,X1] :
( ~ incident(X1,X3)
| ~ incident(X1,X2)
| ~ incident(X0,X3)
| ~ incident(X0,X2)
| line_equal(X2,X3)
| point_equal(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f134,plain,
~ goal,
inference(cnf_transformation,[],[f53]) ).
tcf(c_49,plain,
! [X0: $i] :
( goal
| ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_50,plain,
( goal
| ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_51,plain,
( goal
| ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_52,plain,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_53,plain,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_54,plain,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_55,plain,
incident(a1,a1b1),
inference(cnf_transformation,[],[f90]) ).
tcf(c_56,plain,
incident(b1,a1b1),
inference(cnf_transformation,[],[f91]) ).
tcf(c_57,plain,
incident(a2,a2b2),
inference(cnf_transformation,[],[f92]) ).
tcf(c_58,plain,
incident(b2,a2b2),
inference(cnf_transformation,[],[f93]) ).
tcf(c_59,plain,
incident(a1,a1c1),
inference(cnf_transformation,[],[f94]) ).
tcf(c_60,plain,
incident(c1,a1c1),
inference(cnf_transformation,[],[f95]) ).
tcf(c_61,plain,
incident(a2,a2c2),
inference(cnf_transformation,[],[f96]) ).
tcf(c_62,plain,
incident(c2,a2c2),
inference(cnf_transformation,[],[f97]) ).
tcf(c_63,plain,
incident(c1,b1c1),
inference(cnf_transformation,[],[f98]) ).
tcf(c_64,plain,
incident(b1,b1c1),
inference(cnf_transformation,[],[f99]) ).
tcf(c_65,plain,
incident(c2,b2c2),
inference(cnf_transformation,[],[f100]) ).
tcf(c_66,plain,
incident(b2,b2c2),
inference(cnf_transformation,[],[f101]) ).
tcf(c_67,plain,
incident(o,oa),
inference(cnf_transformation,[],[f102]) ).
tcf(c_68,plain,
incident(o,ob),
inference(cnf_transformation,[],[f103]) ).
tcf(c_69,plain,
incident(o,oc),
inference(cnf_transformation,[],[f104]) ).
tcf(c_70,plain,
incident(a1,oa),
inference(cnf_transformation,[],[f105]) ).
tcf(c_71,plain,
incident(a2,oa),
inference(cnf_transformation,[],[f106]) ).
tcf(c_72,plain,
incident(b1,ob),
inference(cnf_transformation,[],[f107]) ).
tcf(c_73,plain,
incident(b2,ob),
inference(cnf_transformation,[],[f108]) ).
tcf(c_74,plain,
incident(c1,oc),
inference(cnf_transformation,[],[f109]) ).
tcf(c_75,plain,
incident(c2,oc),
inference(cnf_transformation,[],[f110]) ).
tcf(c_76,plain,
incident(bc,b1c1),
inference(cnf_transformation,[],[f111]) ).
tcf(c_77,plain,
incident(bc,b2c2),
inference(cnf_transformation,[],[f112]) ).
tcf(c_78,plain,
incident(ac,a1c1),
inference(cnf_transformation,[],[f113]) ).
tcf(c_79,plain,
incident(ac,a2c2),
inference(cnf_transformation,[],[f114]) ).
tcf(c_80,plain,
incident(ab,a1b1),
inference(cnf_transformation,[],[f115]) ).
tcf(c_81,plain,
incident(ab,a2b2),
inference(cnf_transformation,[],[f116]) ).
tcf(c_82,plain,
! [X0: $i] :
( goal
| ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_83,plain,
! [X0: $i] :
( goal
| ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_84,plain,
( goal
| ~ point_equal(a2,a1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_85,plain,
( goal
| ~ point_equal(b2,b1) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_86,plain,
( goal
| ~ point_equal(c2,c1) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_87,plain,
( goal
| ~ line_equal(b1c1,b2c2) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_88,plain,
( goal
| ~ line_equal(a1c1,a2c2) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_89,plain,
( goal
| ~ line_equal(a1b1,a2b2) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( point_equal(X1,X0)
| ~ point_equal(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] :
( point_equal(X0,X2)
| ~ point_equal(X1,X2)
| ~ point_equal(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( line_equal(X1,X1)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( line_equal(X1,X0)
| ~ line_equal(X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( line_equal(X0,X2)
| ~ line_equal(X1,X2)
| ~ line_equal(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident(X2,X1)
| ~ point_equal(X2,X0)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] :
( incident(X2,X1)
| ~ incident(X2,X0)
| ~ line_equal(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( point_equal(X0,X3)
| line_equal(X1,X2)
| ~ incident(X3,X2)
| ~ incident(X3,X1)
| ~ incident(X0,X2)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_99,negated_conjecture,
~ goal,
inference(cnf_transformation,[],[f134]) ).
tcf(c_117,plain,
! [X0: $i] :
( ~ incident(a2,X0)
| ~ incident(b2,X0)
| ~ incident(c2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_83,c_99,c_83]) ).
tcf(c_118,plain,
! [X0: $i] :
( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(renaming,[status(thm)],[c_117]) ).
tcf(c_120,plain,
! [X0: $i] :
( ~ incident(a1,X0)
| ~ incident(b1,X0)
| ~ incident(c1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_82,c_99,c_82]) ).
tcf(c_121,plain,
! [X0: $i] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(renaming,[status(thm)],[c_120]) ).
tcf(c_123,plain,
( ~ incident(a2,b1c1)
| ~ incident(b2,a1c1)
| ~ incident(c2,a1b1) ),
inference(global_subsumption_just,[status(thm)],[c_51,c_99,c_51]) ).
tcf(c_124,plain,
( ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(renaming,[status(thm)],[c_123]) ).
tcf(c_125,plain,
( ~ incident(a1,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(c1,a2b2) ),
inference(global_subsumption_just,[status(thm)],[c_50,c_99,c_50]) ).
tcf(c_126,plain,
( ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(renaming,[status(thm)],[c_125]) ).
tcf(c_127,plain,
! [X0: $i] :
( ~ line_equal(X0,X0)
| ~ incident(bc,X0)
| ~ incident(ac,X0)
| ~ incident(ab,X0) ),
inference(global_subsumption_just,[status(thm)],[c_49,c_99,c_49]) ).
tcf(c_128,plain,
! [X0: $i] :
( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0) ),
inference(renaming,[status(thm)],[c_127]) ).
tcf(c_222,plain,
! [X0: $i] :
( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_128,c_93]) ).
tcf(c_454,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( ~ incident(ab,X0_iProver_incident_2)
| ~ incident(ac,X0_iProver_incident_2)
| ~ incident(bc,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_222]) ).
tcf(c_456,plain,
( ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(subtyping,[status(esa)],[c_124]) ).
tcf(c_457,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( ~ incident(c1,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(a1,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_121]) ).
tcf(c_458,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( ~ incident(c2,X0_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_118]) ).
tcf(c_465,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] :
( point_equal(X0_iProver_incident_1,X1_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ 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_98]) ).
tcf(c_466,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)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_97]) ).
tcf(c_467,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_96]) ).
tcf(c_468,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2,X2_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,X2_iProver_incident_2)
| ~ line_equal(X1_iProver_incident_2,X2_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(subtyping,[status(esa)],[c_95]) ).
tcf(c_469,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_94]) ).
tcf(c_471,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_92]) ).
tcf(c_472,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_91]) ).
tcf(c_474,plain,
incident(ab,a2b2),
inference(subtyping,[status(esa)],[c_81]) ).
tcf(c_475,plain,
incident(ab,a1b1),
inference(subtyping,[status(esa)],[c_80]) ).
tcf(c_476,plain,
incident(ac,a2c2),
inference(subtyping,[status(esa)],[c_79]) ).
tcf(c_477,plain,
incident(ac,a1c1),
inference(subtyping,[status(esa)],[c_78]) ).
tcf(c_478,plain,
incident(bc,b2c2),
inference(subtyping,[status(esa)],[c_77]) ).
tcf(c_479,plain,
incident(bc,b1c1),
inference(subtyping,[status(esa)],[c_76]) ).
tcf(c_480,plain,
incident(c2,oc),
inference(subtyping,[status(esa)],[c_75]) ).
tcf(c_481,plain,
incident(c1,oc),
inference(subtyping,[status(esa)],[c_74]) ).
tcf(c_482,plain,
incident(b2,ob),
inference(subtyping,[status(esa)],[c_73]) ).
tcf(c_483,plain,
incident(b1,ob),
inference(subtyping,[status(esa)],[c_72]) ).
tcf(c_484,plain,
incident(a2,oa),
inference(subtyping,[status(esa)],[c_71]) ).
tcf(c_485,plain,
incident(a1,oa),
inference(subtyping,[status(esa)],[c_70]) ).
tcf(c_486,plain,
incident(o,oc),
inference(subtyping,[status(esa)],[c_69]) ).
tcf(c_487,plain,
incident(o,ob),
inference(subtyping,[status(esa)],[c_68]) ).
tcf(c_488,plain,
incident(o,oa),
inference(subtyping,[status(esa)],[c_67]) ).
tcf(c_489,plain,
incident(b2,b2c2),
inference(subtyping,[status(esa)],[c_66]) ).
tcf(c_490,plain,
incident(c2,b2c2),
inference(subtyping,[status(esa)],[c_65]) ).
tcf(c_492,plain,
incident(c1,b1c1),
inference(subtyping,[status(esa)],[c_63]) ).
tcf(c_493,plain,
incident(c2,a2c2),
inference(subtyping,[status(esa)],[c_62]) ).
tcf(c_494,plain,
incident(a2,a2c2),
inference(subtyping,[status(esa)],[c_61]) ).
tcf(c_495,plain,
incident(c1,a1c1),
inference(subtyping,[status(esa)],[c_60]) ).
tcf(c_496,plain,
incident(a1,a1c1),
inference(subtyping,[status(esa)],[c_59]) ).
tcf(c_497,plain,
incident(b2,a2b2),
inference(subtyping,[status(esa)],[c_58]) ).
tcf(c_498,plain,
incident(a2,a2b2),
inference(subtyping,[status(esa)],[c_57]) ).
tcf(c_499,plain,
incident(b1,a1b1),
inference(subtyping,[status(esa)],[c_56]) ).
tcf(c_500,plain,
incident(a1,a1b1),
inference(subtyping,[status(esa)],[c_55]) ).
tcf(c_501,plain,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
inference(subtyping,[status(esa)],[c_54]) ).
tcf(c_502,plain,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
inference(subtyping,[status(esa)],[c_53]) ).
tcf(c_503,plain,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
inference(subtyping,[status(esa)],[c_52]) ).
tcf(c_506,plain,
( ~ incident(ab,a1b1)
| ~ incident(ac,a1b1)
| ~ incident(bc,a1b1) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_507,plain,
( ~ incident(c1,a1b1)
| ~ incident(b1,a1b1)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_510,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(c1,X1_iProver_incident_2)
| ~ incident(c1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_512,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(ac,X0_iProver_incident_2)
| ~ point_equal(ac,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_513,plain,
( incident(ac,a1b1)
| ~ point_equal(ac,a1)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_512]) ).
tcf(c_514,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(c1,X0_iProver_incident_2)
| ~ point_equal(c1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_515,plain,
( incident(c1,a1b1)
| ~ point_equal(c1,a1)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_514]) ).
tcf(c_524,plain,
( point_equal(a2,a1)
| ~ point_equal(a1,a2) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_526,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,b1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b2,X1_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(b1,X1_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_528,plain,
( point_equal(b2,b1)
| ~ point_equal(b1,b2) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_531,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,c1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(c2,X1_iProver_incident_2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(c1,X1_iProver_incident_2)
| ~ incident(c1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_533,plain,
( point_equal(c2,c1)
| ~ point_equal(c1,c2) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_538,plain,
( line_equal(b1c1,b2c2)
| ~ line_equal(b2c2,b1c1) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_541,plain,
( line_equal(a1c1,a2c2)
| ~ line_equal(a2c2,a1c1) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_543,plain,
( line_equal(a1b1,a2b2)
| ~ line_equal(a2b2,a1b1) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_544,plain,
( ~ incident(ab,a2c2)
| ~ incident(ac,a2c2)
| ~ incident(bc,a2c2) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_545,plain,
( ~ incident(ab,a1c1)
| ~ incident(ac,a1c1)
| ~ incident(bc,a1c1) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_547,plain,
( ~ incident(c1,oc)
| ~ incident(b1,oc)
| ~ incident(a1,oc) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_548,plain,
( ~ incident(c2,b2c2)
| ~ incident(b2,b2c2)
| ~ incident(a2,b2c2) ),
inference(instantiation,[status(thm)],[c_458]) ).
tcf(c_549,plain,
( ~ incident(c1,b1c1)
| ~ incident(b1,b1c1)
| ~ incident(a1,b1c1) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_550,plain,
( ~ incident(c2,a2c2)
| ~ incident(b2,a2c2)
| ~ incident(a2,a2c2) ),
inference(instantiation,[status(thm)],[c_458]) ).
tcf(c_551,plain,
( ~ incident(c1,a1c1)
| ~ incident(b1,a1c1)
| ~ incident(a1,a1c1) ),
inference(instantiation,[status(thm)],[c_457]) ).
tcf(c_558,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c1,X0_iProver_incident_2)
| ~ incident(c1,a1c1)
| ~ line_equal(a1c1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_510]) ).
tcf(c_559,plain,
( incident(c1,a1b1)
| ~ incident(c1,a1c1)
| ~ line_equal(a1c1,a1b1) ),
inference(instantiation,[status(thm)],[c_558]) ).
tcf(c_562,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c1,X0_iProver_incident_2)
| ~ incident(c1,oc)
| ~ line_equal(oc,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_510]) ).
tcf(c_563,plain,
( incident(c1,a1b1)
| ~ incident(c1,oc)
| ~ line_equal(oc,a1b1) ),
inference(instantiation,[status(thm)],[c_562]) ).
tcf(c_592,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(a2,X1_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_596,plain,
( point_equal(b2,b1)
| line_equal(b1c1,b2c2)
| ~ incident(b2,b1c1)
| ~ incident(b2,b2c2)
| ~ incident(b1,b1c1)
| ~ incident(b1,b2c2) ),
inference(instantiation,[status(thm)],[c_526]) ).
tcf(c_599,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b2,X1_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_628,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(a1c1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a1c1) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_629,plain,
( line_equal(a1c1,a1b1)
| ~ line_equal(a1b1,a1c1) ),
inference(instantiation,[status(thm)],[c_628]) ).
tcf(c_637,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(a1,a2)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(a2,X1_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(a1,X1_iProver_incident_2)
| ~ incident(a1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_640,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,b2)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b2,X1_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(b1,X1_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_667,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(ab,a2c2)
| ~ point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_671,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(ab,a1c1)
| ~ point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_672,plain,
( incident(ab,a1c1)
| ~ point_equal(ab,a1)
| ~ incident(a1,a1c1) ),
inference(instantiation,[status(thm)],[c_671]) ).
tcf(c_673,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,oc)
| ~ incident(b2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oc) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_675,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b2,oc)
| ~ point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_679,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,oc)
| ~ point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_681,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,b2c2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,b2c2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_687,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,a2c2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a2c2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_689,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b2,a2c2)
| ~ point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_690,plain,
( incident(b2,a2c2)
| ~ point_equal(b2,a1)
| ~ incident(a1,a2c2) ),
inference(instantiation,[status(thm)],[c_689]) ).
tcf(c_693,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a1c1)
| ~ point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_694,plain,
( incident(b1,a1c1)
| ~ point_equal(b1,a1)
| ~ incident(a1,a1c1) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_708,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(a2c2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a2c2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_709,plain,
( line_equal(a2c2,a1b1)
| ~ line_equal(a1b1,a2c2) ),
inference(instantiation,[status(thm)],[c_708]) ).
tcf(c_730,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(oc,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oc) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_731,plain,
( line_equal(oc,a1b1)
| ~ line_equal(a1b1,oc) ),
inference(instantiation,[status(thm)],[c_730]) ).
tcf(c_746,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(b2c2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,b2c2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_747,plain,
( line_equal(b2c2,a1b1)
| ~ line_equal(a1b1,b2c2) ),
inference(instantiation,[status(thm)],[c_746]) ).
tcf(c_825,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c2)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(c2,X1_iProver_incident_2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_826,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,c2)
| ~ point_equal(c2,X0_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_827,plain,
( point_equal(a1,c2)
| ~ point_equal(c2,a1) ),
inference(instantiation,[status(thm)],[c_826]) ).
tcf(c_836,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(a2,a2b2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_592]) ).
tcf(c_885,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(b2,b2c2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_599]) ).
tcf(c_886,plain,
( point_equal(b2,a1)
| line_equal(a1b1,b2c2)
| ~ incident(b2,a1b1)
| ~ incident(b2,b2c2)
| ~ incident(a1,a1b1)
| ~ incident(a1,b2c2) ),
inference(instantiation,[status(thm)],[c_885]) ).
tcf(c_947,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2b2)
| ~ point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_958,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,X0_iProver_incident_2)
| ~ line_equal(a2c2,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_494,c_466]) ).
tcf(c_959,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c2,X0_iProver_incident_2)
| ~ line_equal(a2c2,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_493,c_466]) ).
tcf(c_963,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,X0_iProver_incident_2)
| ~ line_equal(b2c2,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_489,c_466]) ).
tcf(c_964,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(o,X0_iProver_incident_2)
| ~ line_equal(oa,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_488,c_466]) ).
tcf(c_965,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(o,X0_iProver_incident_2)
| ~ line_equal(ob,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_487,c_466]) ).
tcf(c_968,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,X0_iProver_incident_2)
| ~ line_equal(oa,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_484,c_466]) ).
tcf(c_970,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,X0_iProver_incident_2)
| ~ line_equal(ob,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_482,c_466]) ).
tcf(c_974,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(bc,X0_iProver_incident_2)
| ~ line_equal(b2c2,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_478,c_466]) ).
tcf(c_981,plain,
( incident(bc,a1b1)
| ~ line_equal(b2c2,a1b1) ),
inference(instantiation,[status(thm)],[c_974]) ).
tcf(c_985,plain,
( incident(b2,a1b1)
| ~ line_equal(ob,a1b1) ),
inference(instantiation,[status(thm)],[c_970]) ).
tcf(c_986,plain,
( incident(a2,a1b1)
| ~ line_equal(oa,a1b1) ),
inference(instantiation,[status(thm)],[c_968]) ).
tcf(c_988,plain,
( incident(o,a1b1)
| ~ line_equal(ob,a1b1) ),
inference(instantiation,[status(thm)],[c_965]) ).
tcf(c_989,plain,
( incident(o,a1b1)
| ~ line_equal(oa,a1b1) ),
inference(instantiation,[status(thm)],[c_964]) ).
tcf(c_990,plain,
( incident(b2,a1b1)
| ~ line_equal(b2c2,a1b1) ),
inference(instantiation,[status(thm)],[c_963]) ).
tcf(c_993,plain,
( incident(c2,a1b1)
| ~ line_equal(a2c2,a1b1) ),
inference(instantiation,[status(thm)],[c_959]) ).
tcf(c_994,plain,
( incident(a2,a1b1)
| ~ line_equal(a2c2,a1b1) ),
inference(instantiation,[status(thm)],[c_958]) ).
tcf(c_1020,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a1,a2)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(a2,oa)
| ~ incident(a1,oa)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(a1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_637]) ).
tcf(c_1021,plain,
( point_equal(a1,a2)
| line_equal(a1b1,oa)
| ~ incident(a2,oa)
| ~ incident(a2,a1b1)
| ~ incident(a1,oa)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_1020]) ).
tcf(c_1032,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,b2)
| line_equal(X0_iProver_incident_2,ob)
| ~ incident(b2,ob)
| ~ incident(b1,ob)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_640]) ).
tcf(c_1036,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b1,X1_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_1037,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(b1,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,b1) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_1038,plain,
( point_equal(b1,a1)
| ~ point_equal(a1,b1) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_1065,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,a2c2)
| ~ line_equal(a2c2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_1066,plain,
( line_equal(a1b1,a2c2)
| ~ line_equal(a2c2,a1b1) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_1069,plain,
( incident(ab,a2c2)
| ~ point_equal(ab,a2)
| ~ incident(a2,a2c2) ),
inference(instantiation,[status(thm)],[c_667]) ).
tcf(c_1072,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,a2c2)
| ~ line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_1073,plain,
( incident(a1,a2c2)
| ~ incident(a1,a1b1)
| ~ line_equal(a1b1,a2c2) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1082,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(ab,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,ab) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_1083,plain,
( point_equal(ab,a1)
| ~ point_equal(a1,ab) ),
inference(instantiation,[status(thm)],[c_1082]) ).
tcf(c_1087,plain,
( incident(b2,oc)
| ~ incident(b2,b2c2)
| ~ line_equal(b2c2,oc) ),
inference(instantiation,[status(thm)],[c_673]) ).
tcf(c_1088,plain,
( incident(b2,oc)
| ~ incident(b2,ob)
| ~ line_equal(ob,oc) ),
inference(instantiation,[status(thm)],[c_673]) ).
tcf(c_1091,plain,
( incident(b2,oc)
| ~ point_equal(b2,o)
| ~ incident(o,oc) ),
inference(instantiation,[status(thm)],[c_675]) ).
tcf(c_1092,plain,
( incident(b2,oc)
| ~ point_equal(b2,c1)
| ~ incident(c1,oc) ),
inference(instantiation,[status(thm)],[c_675]) ).
tcf(c_1097,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,c1)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c2,oc)
| ~ incident(c1,oc)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(c1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_531]) ).
tcf(c_1107,plain,
( incident(b1,oc)
| ~ point_equal(b1,o)
| ~ incident(o,oc) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_1109,plain,
( incident(b1,oc)
| ~ point_equal(b1,c2)
| ~ incident(c2,oc) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_1113,plain,
( incident(a2,b2c2)
| ~ incident(a2,a2b2)
| ~ line_equal(a2b2,b2c2) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_1135,plain,
( incident(b2,a2c2)
| ~ incident(b2,b2c2)
| ~ line_equal(b2c2,a2c2) ),
inference(instantiation,[status(thm)],[c_687]) ).
tcf(c_1140,plain,
( incident(b2,a2c2)
| ~ point_equal(b2,a2)
| ~ incident(a2,a2c2) ),
inference(instantiation,[status(thm)],[c_689]) ).
tcf(c_1141,plain,
( incident(b2,a2c2)
| ~ point_equal(b2,c2)
| ~ incident(c2,a2c2) ),
inference(instantiation,[status(thm)],[c_689]) ).
tcf(c_1280,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,a2c2)
| ~ point_equal(X0_iProver_incident_1,c2) ),
inference(superposition,[status(thm)],[c_493,c_467]) ).
tcf(c_1283,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,b2c2)
| ~ point_equal(X0_iProver_incident_1,c2) ),
inference(superposition,[status(thm)],[c_490,c_467]) ).
tcf(c_1284,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,b2c2)
| ~ point_equal(X0_iProver_incident_1,b2) ),
inference(superposition,[status(thm)],[c_489,c_467]) ).
tcf(c_1286,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,ob)
| ~ point_equal(X0_iProver_incident_1,o) ),
inference(superposition,[status(thm)],[c_487,c_467]) ).
tcf(c_1287,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,oc)
| ~ point_equal(X0_iProver_incident_1,o) ),
inference(superposition,[status(thm)],[c_486,c_467]) ).
tcf(c_1293,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,oc)
| ~ point_equal(X0_iProver_incident_1,c2) ),
inference(superposition,[status(thm)],[c_480,c_467]) ).
tcf(c_1304,plain,
( incident(a1,oc)
| ~ point_equal(a1,c2) ),
inference(instantiation,[status(thm)],[c_1293]) ).
tcf(c_1308,plain,
( incident(a1,oc)
| ~ point_equal(a1,o) ),
inference(instantiation,[status(thm)],[c_1287]) ).
tcf(c_1309,plain,
( incident(a1,ob)
| ~ point_equal(a1,o) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_1310,plain,
( incident(a1,b2c2)
| ~ point_equal(a1,b2) ),
inference(instantiation,[status(thm)],[c_1284]) ).
tcf(c_1311,plain,
( incident(a1,b2c2)
| ~ point_equal(a1,c2) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_1314,plain,
( incident(a1,a2c2)
| ~ point_equal(a1,c2) ),
inference(instantiation,[status(thm)],[c_1280]) ).
tcf(c_1389,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c2)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_825]) ).
tcf(c_1390,plain,
( point_equal(a1,c2)
| line_equal(a1b1,oc)
| ~ incident(c2,oc)
| ~ incident(c2,a1b1)
| ~ incident(a1,oc)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_1389]) ).
tcf(c_1413,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,ab)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(a2,a2b2)
| ~ incident(ab,a2b2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(ab,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_836]) ).
tcf(c_1414,plain,
( point_equal(a2,ab)
| line_equal(a1b1,a2b2)
| ~ incident(a2,a1b1)
| ~ incident(a2,a2b2)
| ~ incident(ab,a1b1)
| ~ incident(ab,a2b2) ),
inference(instantiation,[status(thm)],[c_1413]) ).
tcf(c_1664,plain,
( incident(b1,a2b2)
| ~ point_equal(b1,a2)
| ~ incident(a2,a2b2) ),
inference(instantiation,[status(thm)],[c_947]) ).
tcf(c_1753,plain,
( point_equal(b1,b2)
| line_equal(b2c2,ob)
| ~ incident(b2,ob)
| ~ incident(b2,b2c2)
| ~ incident(b1,ob)
| ~ incident(b1,b2c2) ),
inference(instantiation,[status(thm)],[c_1032]) ).
tcf(c_1782,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(b2c2,X0_iProver_incident_2)
| ~ incident(b1,b2c2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_1036]) ).
tcf(c_1783,plain,
( point_equal(b1,a1)
| line_equal(b2c2,a1b1)
| ~ incident(b1,a1b1)
| ~ incident(b1,b2c2)
| ~ incident(a1,a1b1)
| ~ incident(a1,b2c2) ),
inference(instantiation,[status(thm)],[c_1782]) ).
tcf(c_1967,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(a1,b2c2)
| point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1c1)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_503,c_465]) ).
tcf(c_1969,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(a1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_500,c_465]) ).
tcf(c_1970,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_499,c_465]) ).
tcf(c_1971,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_498,c_465]) ).
tcf(c_2018,plain,
( point_equal(b2,a1)
| incident(a1,b2c2)
| line_equal(a1b1,a1c1)
| ~ incident(b2,a1b1)
| ~ incident(a1,a1b1)
| ~ incident(a1,a1c1) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_2119,plain,
( point_equal(c2,c1)
| line_equal(b2c2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,b2c2)
| ~ incident(c1,oc)
| ~ incident(c1,b2c2) ),
inference(instantiation,[status(thm)],[c_1097]) ).
tcf(c_2135,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(ac,X1_iProver_incident_2)
| ~ incident(ac,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2137,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(c2,X1_iProver_incident_2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2139,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(c1,X0_iProver_incident_2)
| ~ point_equal(c1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2145,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,a1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(a2,X1_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(a1,X1_iProver_incident_2)
| ~ incident(a1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2148,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,b1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b2,X1_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(b1,X1_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2168,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(ac,X0_iProver_incident_2)
| ~ incident(ac,a1c1)
| ~ line_equal(a1c1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2135]) ).
tcf(c_2177,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c2,X0_iProver_incident_2)
| ~ incident(c2,a2c2)
| ~ line_equal(a2c2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2137]) ).
tcf(c_2178,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c2,X0_iProver_incident_2)
| ~ incident(c2,b2c2)
| ~ line_equal(b2c2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2137]) ).
tcf(c_2179,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c2,X0_iProver_incident_2)
| ~ incident(c2,oc)
| ~ line_equal(oc,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2137]) ).
tcf(c_2186,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(c1,X1_iProver_incident_2)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2190,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(c2,X1_iProver_incident_2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2198,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(a2,X1_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2206,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,b1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b1,X1_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2213,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(c1,X1_iProver_incident_2)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2214,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,c1)
| ~ point_equal(c1,X0_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_2233,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,a2b2)
| ~ line_equal(a2b2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_2237,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(a1,a2)
| ~ point_equal(a1,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,a2) ),
inference(instantiation,[status(thm)],[c_471]) ).
tcf(c_2247,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(b2c2,b1c1)
| ~ line_equal(b2c2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,b1c1) ),
inference(instantiation,[status(thm)],[c_468]) ).
tcf(c_2252,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(a2c2,a1c1)
| ~ line_equal(a2c2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a1c1) ),
inference(instantiation,[status(thm)],[c_468]) ).
tcf(c_2265,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b1,oc)
| ~ incident(b1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oc) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2267,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,b2c2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,b2c2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2269,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a1,b1c1)
| ~ incident(a1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,b1c1) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2271,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,a2c2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a2c2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2272,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b2,a2c2)
| ~ point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2274,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a1c1)
| ~ point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2339,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(c1,b1c1)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2186]) ).
tcf(c_2340,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c1,oc)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2186]) ).
tcf(c_2351,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(c2,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2190]) ).
tcf(c_2352,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(c2,b2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2190]) ).
tcf(c_2353,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2190]) ).
tcf(c_2356,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c2)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(c2,X1_iProver_incident_2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2358,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,c2)
| ~ point_equal(X1_iProver_incident_1,c2)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_471]) ).
tcf(c_2366,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(a2,b1c1)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2198]) ).
tcf(c_2370,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(a2,X1_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2371,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,X0_iProver_incident_2)
| ~ point_equal(a2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2372,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,a2)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(a2,X1_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2389,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,b1)
| line_equal(b1c1,X0_iProver_incident_2)
| ~ incident(b1,b1c1)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2206]) ).
tcf(c_2409,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b1,X1_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2418,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(c1,b1c1)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2213]) ).
tcf(c_2419,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c1)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c1,oc)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2213]) ).
tcf(c_2432,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b1,b2c2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,b2c2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2433,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,b2c2)
| ~ point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2472,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b1,a2b2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a2b2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2474,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a1,a2b2)
| ~ incident(a1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a2b2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2488,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(a2b2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,a2b2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_2504,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(b2,X1_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2505,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,X0_iProver_incident_2)
| ~ point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2543,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,a2c2)
| ~ incident(X1_iProver_incident_1,a2c2)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2553,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(ab,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(ab,X1_iProver_incident_2)
| ~ incident(ab,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_2565,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,oc)
| ~ line_equal(X0_iProver_incident_2,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2566,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,oc)
| ~ incident(X1_iProver_incident_1,oc)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2572,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,oc)
| ~ line_equal(X1_iProver_incident_2,oc)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_468]) ).
tcf(c_2573,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,oc)
| ~ line_equal(oc,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_2591,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,b1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(b1,b1c1)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2206]) ).
tcf(c_2604,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,b1c1)
| ~ line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_2605,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,b1c1)
| ~ incident(X1_iProver_incident_1,b1c1)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2799,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,b1c1)
| point_equal(c1,X0_iProver_incident_1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b1c1) ),
inference(instantiation,[status(thm)],[c_2339]) ).
tcf(c_2803,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b1c1,oc)
| point_equal(c1,X0_iProver_incident_1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b1c1) ),
inference(instantiation,[status(thm)],[c_2340]) ).
tcf(c_2808,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b2c2,a2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(c2,a2c2)
| ~ incident(c2,b2c2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_2351]) ).
tcf(c_2814,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,b2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(c2,oc)
| ~ incident(c2,b2c2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_2352]) ).
tcf(c_2817,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2c2,oc)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(c2,oc)
| ~ incident(c2,a2c2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(instantiation,[status(thm)],[c_2353]) ).
tcf(c_2822,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c2)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(c2,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2356]) ).
tcf(c_2824,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c2)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2356]) ).
tcf(c_2839,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2c2,b1c1)
| point_equal(a2,X0_iProver_incident_1)
| ~ incident(a2,b1c1)
| ~ incident(a2,a2c2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(instantiation,[status(thm)],[c_2366]) ).
tcf(c_2847,plain,
! [X0_iProver_incident_1: iProver_incident_1,X1_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,a2b2)
| ~ incident(X1_iProver_incident_1,a2b2)
| ~ point_equal(X0_iProver_incident_1,X1_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_2863,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,X0_iProver_incident_2)
| ~ incident(a2,oa)
| ~ line_equal(oa,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2370]) ).
tcf(c_2872,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,a2)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(a2,a2b2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2372]) ).
tcf(c_2874,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,a2)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(a2,oa)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2372]) ).
tcf(c_2900,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(bc,b1)
| line_equal(b1c1,X0_iProver_incident_2)
| ~ incident(b1,b1c1)
| ~ incident(bc,b1c1)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(bc,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2389]) ).
tcf(c_2944,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(b1,a2c2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2409]) ).
tcf(c_2947,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(a2c2,X0_iProver_incident_2)
| ~ incident(b1,a2c2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2409]) ).
tcf(c_2975,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,b1c1)
| point_equal(X0_iProver_incident_1,c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b1c1) ),
inference(instantiation,[status(thm)],[c_2418]) ).
tcf(c_2981,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b1c1,oc)
| point_equal(X0_iProver_incident_1,c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b1c1) ),
inference(instantiation,[status(thm)],[c_2419]) ).
tcf(c_3083,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,X0_iProver_incident_2)
| ~ incident(b2,a2b2)
| ~ line_equal(a2b2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2504]) ).
tcf(c_3088,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(b2,X1_iProver_incident_2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_3103,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,a2c2)
| ~ incident(c2,a2c2)
| ~ point_equal(X0_iProver_incident_1,c2) ),
inference(instantiation,[status(thm)],[c_2543]) ).
tcf(c_3155,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,ab)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(ab,X1_iProver_incident_2)
| ~ incident(ab,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_3218,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,b1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(c1,b1c1)
| ~ incident(b1,b1c1)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2591]) ).
tcf(c_3301,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(ac,X0_iProver_incident_2)
| ~ line_equal(a2c2,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_466,c_476]) ).
tcf(c_3342,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,b1c1)
| ~ incident(b1,b1c1)
| ~ point_equal(X0_iProver_incident_1,b1) ),
inference(instantiation,[status(thm)],[c_2605]) ).
tcf(c_3579,plain,
( point_equal(c1,c2)
| line_equal(b1c1,oc)
| ~ incident(c2,oc)
| ~ incident(c2,b1c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1) ),
inference(instantiation,[status(thm)],[c_2803]) ).
tcf(c_3596,plain,
( point_equal(c2,b1)
| line_equal(b2c2,a2c2)
| ~ incident(c2,a2c2)
| ~ incident(c2,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(b1,b2c2) ),
inference(instantiation,[status(thm)],[c_2808]) ).
tcf(c_3653,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b2c2,a2c2)
| point_equal(X0_iProver_incident_1,c2)
| ~ incident(c2,a2c2)
| ~ incident(c2,b2c2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_2822]) ).
tcf(c_3668,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b2c2,oc)
| point_equal(X0_iProver_incident_1,c2)
| ~ incident(c2,oc)
| ~ incident(c2,b2c2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_2824]) ).
tcf(c_3684,plain,
( point_equal(a2,b1)
| line_equal(a2c2,b1c1)
| ~ incident(a2,b1c1)
| ~ incident(a2,a2c2)
| ~ incident(b1,b1c1)
| ~ incident(b1,a2c2) ),
inference(instantiation,[status(thm)],[c_2839]) ).
tcf(c_3689,plain,
( ~ incident(c2,a2b2)
| ~ incident(b2,a2b2) ),
inference(superposition,[status(thm)],[c_498,c_458]) ).
tcf(c_3730,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a1c1,a1b1)
| point_equal(a1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(superposition,[status(thm)],[c_496,c_1969]) ).
tcf(c_3731,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oa,a1b1)
| point_equal(a1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a1b1) ),
inference(superposition,[status(thm)],[c_485,c_1969]) ).
tcf(c_3757,plain,
( point_equal(a1,b1)
| line_equal(oa,a1b1)
| ~ incident(b1,oa) ),
inference(superposition,[status(thm)],[c_499,c_3731]) ).
tcf(c_3780,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,a1b1)
| point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,a1b1) ),
inference(superposition,[status(thm)],[c_483,c_1970]) ).
tcf(c_3781,plain,
( point_equal(b1,a1)
| line_equal(ob,a1b1)
| ~ incident(a1,ob)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_3780]) ).
tcf(c_3824,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(ab,X0_iProver_incident_1)
| line_equal(oa,X0_iProver_incident_2)
| ~ incident(ab,oa)
| ~ incident(ab,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2553]) ).
tcf(c_3829,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,a1)
| line_equal(oa,X0_iProver_incident_2)
| ~ incident(a2,oa)
| ~ incident(a1,oa)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(a1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2145]) ).
tcf(c_3830,plain,
( point_equal(a2,a1)
| line_equal(oa,a1b1)
| ~ incident(a2,oa)
| ~ incident(a2,a1b1)
| ~ incident(a1,oa)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_3829]) ).
tcf(c_3831,plain,
( point_equal(ab,a1)
| line_equal(oa,a1b1)
| ~ incident(a1,oa)
| ~ incident(a1,a1b1)
| ~ incident(ab,oa)
| ~ incident(ab,a1b1) ),
inference(instantiation,[status(thm)],[c_3824]) ).
tcf(c_3833,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(oa,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oa) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_3834,plain,
( line_equal(oa,a1b1)
| ~ line_equal(a1b1,oa) ),
inference(instantiation,[status(thm)],[c_3833]) ).
tcf(c_3845,plain,
( point_equal(b1,c2)
| incident(b1,a2c2)
| line_equal(ob,a1b1)
| ~ incident(c2,ob) ),
inference(superposition,[status(thm)],[c_502,c_3780]) ).
tcf(c_3846,plain,
( point_equal(b1,a1)
| line_equal(ob,a1b1)
| ~ incident(a1,ob) ),
inference(superposition,[status(thm)],[c_500,c_3780]) ).
tcf(c_3850,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,a2)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(b2,a2b2)
| ~ incident(a2,a2b2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2872]) ).
tcf(c_3851,plain,
( point_equal(b2,a2)
| line_equal(a1b1,a2b2)
| ~ incident(b2,a1b1)
| ~ incident(b2,a2b2)
| ~ incident(a2,a1b1)
| ~ incident(a2,a2b2) ),
inference(instantiation,[status(thm)],[c_3850]) ).
tcf(c_3864,plain,
( ~ incident(a1,ob)
| line_equal(ob,a1b1) ),
inference(global_subsumption_just,[status(thm)],[c_3846,c_60,c_59,c_55,c_551,c_694,c_3781]) ).
tcf(c_3865,plain,
( line_equal(ob,a1b1)
| ~ incident(a1,ob) ),
inference(renaming,[status(thm)],[c_3864]) ).
tcf(c_3867,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2b2,oa)
| point_equal(X0_iProver_incident_1,a2)
| ~ incident(a2,oa)
| ~ incident(a2,a2b2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_2874]) ).
tcf(c_3875,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oa,a2b2)
| point_equal(a2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_484,c_1971]) ).
tcf(c_3898,plain,
( point_equal(bc,b1)
| line_equal(b1c1,b2c2)
| ~ incident(b1,b1c1)
| ~ incident(b1,b2c2)
| ~ incident(bc,b1c1)
| ~ incident(bc,b2c2) ),
inference(instantiation,[status(thm)],[c_2900]) ).
tcf(c_3899,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(bc,X1_iProver_incident_2)
| ~ incident(bc,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_3900,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(bc,X0_iProver_incident_2)
| ~ point_equal(bc,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_3943,plain,
( point_equal(a2,ab)
| line_equal(oa,a2b2)
| ~ incident(ab,oa) ),
inference(superposition,[status(thm)],[c_474,c_3875]) ).
tcf(c_3982,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,a2)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(a2,a2c2)
| ~ incident(b1,a2c2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2944]) ).
tcf(c_3983,plain,
( point_equal(b1,a2)
| line_equal(a1b1,a2c2)
| ~ incident(a2,a1b1)
| ~ incident(a2,a2c2)
| ~ incident(b1,a1b1)
| ~ incident(b1,a2c2) ),
inference(instantiation,[status(thm)],[c_3982]) ).
tcf(c_3984,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,c2)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(c2,a2c2)
| ~ incident(b1,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2944]) ).
tcf(c_3986,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,ac)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(b1,a2c2)
| ~ incident(ac,a2c2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(ac,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2944]) ).
tcf(c_3987,plain,
( point_equal(b1,ac)
| line_equal(a1b1,a2c2)
| ~ incident(b1,a1b1)
| ~ incident(b1,a2c2)
| ~ incident(ac,a1b1)
| ~ incident(ac,a2c2) ),
inference(instantiation,[status(thm)],[c_3986]) ).
tcf(c_4028,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,c2)
| line_equal(a2c2,X0_iProver_incident_2)
| ~ incident(c2,a2c2)
| ~ incident(b1,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2947]) ).
tcf(c_4030,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,ac)
| line_equal(a2c2,X0_iProver_incident_2)
| ~ incident(b1,a2c2)
| ~ incident(ac,a2c2)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(ac,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2947]) ).
tcf(c_4031,plain,
( point_equal(b1,ac)
| line_equal(a2c2,a1b1)
| ~ incident(b1,a1b1)
| ~ incident(b1,a2c2)
| ~ incident(ac,a1b1)
| ~ incident(ac,a2c2) ),
inference(instantiation,[status(thm)],[c_4030]) ).
tcf(c_4249,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(b1,a2c2)
| point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_502,c_465]) ).
tcf(c_4251,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_499,c_465]) ).
tcf(c_4252,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_498,c_465]) ).
tcf(c_4255,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1c1)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_495,c_465]) ).
tcf(c_4257,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_493,c_465]) ).
tcf(c_4258,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_492,c_465]) ).
tcf(c_4260,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_490,c_465]) ).
tcf(c_4261,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_489,c_465]) ).
tcf(c_4262,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(o,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_488,c_465]) ).
tcf(c_4263,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(o,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,ob)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_487,c_465]) ).
tcf(c_4264,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(o,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_486,c_465]) ).
tcf(c_4266,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_484,c_465]) ).
tcf(c_4272,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(bc,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(bc,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_478,c_465]) ).
tcf(c_4274,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(ac,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(ac,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_476,c_465]) ).
tcf(c_4275,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(ab,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(ab,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_475,c_465]) ).
tcf(c_4290,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,a1c1)
| point_equal(c1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(superposition,[status(thm)],[c_481,c_4255]) ).
tcf(c_4291,plain,
( point_equal(c1,a1)
| line_equal(oc,a1c1)
| ~ incident(a1,oc)
| ~ incident(a1,a1c1) ),
inference(instantiation,[status(thm)],[c_4290]) ).
tcf(c_4311,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b2c2,a2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_490,c_4257]) ).
tcf(c_4314,plain,
( point_equal(c2,a1)
| line_equal(b2c2,a2c2)
| ~ incident(a1,a2c2)
| ~ incident(a1,b2c2) ),
inference(instantiation,[status(thm)],[c_4311]) ).
tcf(c_4318,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,b1c1)
| point_equal(c1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b1c1) ),
inference(superposition,[status(thm)],[c_481,c_4258]) ).
tcf(c_4322,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| line_equal(a1b1,b2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_502,c_4260]) ).
tcf(c_4325,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,b2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_480,c_4260]) ).
tcf(c_4328,plain,
( point_equal(c2,a1)
| incident(b1,a2c2)
| line_equal(a1b1,b2c2)
| ~ incident(a1,a1b1)
| ~ incident(a1,b2c2) ),
inference(instantiation,[status(thm)],[c_4322]) ).
tcf(c_4344,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,b2c2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_482,c_4261]) ).
tcf(c_4353,plain,
( point_equal(o,b2)
| line_equal(a2b2,oa)
| ~ incident(o,a2b2)
| ~ incident(b2,oa) ),
inference(superposition,[status(thm)],[c_497,c_4262]) ).
tcf(c_4390,plain,
( point_equal(c2,c1)
| line_equal(oc,b1c1)
| ~ incident(c2,oc)
| ~ incident(c2,b1c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1) ),
inference(instantiation,[status(thm)],[c_2975]) ).
tcf(c_4400,plain,
( point_equal(c2,c1)
| line_equal(b1c1,oc)
| ~ incident(c2,oc)
| ~ incident(c2,b1c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1) ),
inference(instantiation,[status(thm)],[c_2981]) ).
tcf(c_4428,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(ob,X0_iProver_incident_2)
| ~ incident(b1,ob)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2409]) ).
tcf(c_4431,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,b1)
| line_equal(ob,X0_iProver_incident_2)
| ~ incident(b2,ob)
| ~ incident(b1,ob)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2148]) ).
tcf(c_4433,plain,
( point_equal(b2,b1)
| line_equal(ob,a1b1)
| ~ incident(b2,ob)
| ~ incident(b2,a1b1)
| ~ incident(b1,ob)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_4431]) ).
tcf(c_4452,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(b2,a2b2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_3088]) ).
tcf(c_4453,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(b2,b2c2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_3088]) ).
tcf(c_4517,plain,
( point_equal(o,a1)
| line_equal(a1b1,ob)
| ~ incident(o,a1b1)
| ~ incident(a1,ob) ),
inference(superposition,[status(thm)],[c_500,c_4263]) ).
tcf(c_4583,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a1b1,a2b2)
| point_equal(X0_iProver_incident_1,ab)
| ~ incident(ab,a1b1)
| ~ incident(ab,a2b2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_3155]) ).
tcf(c_4584,plain,
( point_equal(a1,ab)
| line_equal(a1b1,a2b2)
| ~ incident(a1,a1b1)
| ~ incident(a1,a2b2)
| ~ incident(ab,a1b1)
| ~ incident(ab,a2b2) ),
inference(instantiation,[status(thm)],[c_4583]) ).
tcf(c_4634,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,o)
| line_equal(X0_iProver_incident_2,X1_iProver_incident_2)
| ~ incident(o,X1_iProver_incident_2)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X1_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_465]) ).
tcf(c_4635,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(X0_iProver_incident_1,o)
| ~ point_equal(o,X0_iProver_incident_1) ),
inference(instantiation,[status(thm)],[c_472]) ).
tcf(c_4636,plain,
( point_equal(a1,o)
| ~ point_equal(o,a1) ),
inference(instantiation,[status(thm)],[c_4635]) ).
tcf(c_4656,plain,
( point_equal(c1,b1)
| line_equal(oc,b1c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1)
| ~ incident(b1,oc)
| ~ incident(b1,b1c1) ),
inference(instantiation,[status(thm)],[c_3218]) ).
tcf(c_4719,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(a1,b2c2)
| point_equal(X0_iProver_incident_1,b2)
| line_equal(X0_iProver_incident_2,a1c1)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_465,c_503]) ).
tcf(c_4720,plain,
( point_equal(a1,b2)
| incident(a1,b2c2)
| line_equal(a1b1,a1c1)
| ~ incident(b2,a1b1)
| ~ incident(a1,a1b1)
| ~ incident(a1,a1c1) ),
inference(instantiation,[status(thm)],[c_4719]) ).
tcf(c_4740,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,o)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_465,c_488]) ).
tcf(c_4741,plain,
( point_equal(a1,o)
| line_equal(a1b1,oa)
| ~ incident(o,a1b1)
| ~ incident(a1,oa)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_4740]) ).
tcf(c_4744,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,o)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(resolution,[status(thm)],[c_465,c_486]) ).
tcf(c_4745,plain,
( point_equal(a1,o)
| line_equal(a1b1,oc)
| ~ incident(o,a1b1)
| ~ incident(a1,oc)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_4744]) ).
tcf(c_4865,plain,
( point_equal(b1,c2)
| line_equal(b2c2,a2c2)
| ~ incident(c2,a2c2)
| ~ incident(c2,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(b1,b2c2) ),
inference(instantiation,[status(thm)],[c_3653]) ).
tcf(c_4925,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(ab,oa)
| ~ incident(ab,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oa) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_4926,plain,
( incident(ab,oa)
| ~ incident(ab,a1b1)
| ~ line_equal(a1b1,oa) ),
inference(instantiation,[status(thm)],[c_4925]) ).
tcf(c_4927,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(ab,oa)
| ~ point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_4928,plain,
( incident(ab,oa)
| ~ point_equal(ab,a1)
| ~ incident(a1,oa) ),
inference(instantiation,[status(thm)],[c_4927]) ).
tcf(c_4929,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b1,oa)
| ~ incident(b1,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oa) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_4930,plain,
( incident(b1,oa)
| ~ incident(b1,a1b1)
| ~ line_equal(a1b1,oa) ),
inference(instantiation,[status(thm)],[c_4929]) ).
tcf(c_4931,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,oa)
| ~ point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_5009,plain,
( point_equal(o,b2)
| line_equal(b2c2,oc)
| ~ incident(o,b2c2)
| ~ incident(b2,oc) ),
inference(superposition,[status(thm)],[c_489,c_4264]) ).
tcf(c_5013,plain,
( point_equal(o,a1)
| line_equal(oa,oc)
| ~ incident(o,oa)
| ~ incident(a1,oc) ),
inference(superposition,[status(thm)],[c_485,c_4264]) ).
tcf(c_5061,plain,
( point_equal(b2,a2)
| line_equal(a2b2,oa)
| ~ incident(b2,oa)
| ~ incident(b2,a2b2)
| ~ incident(a2,oa)
| ~ incident(a2,a2b2) ),
inference(instantiation,[status(thm)],[c_3867]) ).
tcf(c_5105,plain,
( point_equal(b1,c2)
| line_equal(oc,a2c2)
| ~ incident(c2,oc)
| ~ incident(c2,a2c2)
| ~ incident(b1,oc)
| ~ incident(b1,a2c2) ),
inference(instantiation,[status(thm)],[c_3984]) ).
tcf(c_5120,plain,
( point_equal(b1,c2)
| line_equal(a2c2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,a2c2)
| ~ incident(b1,oc)
| ~ incident(b1,a2c2) ),
inference(instantiation,[status(thm)],[c_4028]) ).
tcf(c_5146,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,o)
| line_equal(ob,X0_iProver_incident_2)
| ~ incident(o,ob)
| ~ incident(b1,ob)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_4428]) ).
tcf(c_5147,plain,
( point_equal(b1,o)
| line_equal(ob,a1b1)
| ~ incident(o,ob)
| ~ incident(o,a1b1)
| ~ incident(b1,ob)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_5146]) ).
tcf(c_5151,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(X0_iProver_incident_1,ob)
| ~ line_equal(X0_iProver_incident_2,ob)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_5152,plain,
( incident(a1,ob)
| ~ incident(a1,a1b1)
| ~ line_equal(a1b1,ob) ),
inference(instantiation,[status(thm)],[c_5151]) ).
tcf(c_5182,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,ob)
| ~ incident(b1,ob)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2409]) ).
tcf(c_5185,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,b1)
| line_equal(X0_iProver_incident_2,ob)
| ~ incident(b2,ob)
| ~ incident(b1,ob)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2148]) ).
tcf(c_5188,plain,
( point_equal(b2,b1)
| line_equal(a1b1,ob)
| ~ incident(b2,ob)
| ~ incident(b2,a1b1)
| ~ incident(b1,ob)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_5185]) ).
tcf(c_5194,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,ob)
| ~ line_equal(ob,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_469]) ).
tcf(c_5195,plain,
( line_equal(a1b1,ob)
| ~ line_equal(ob,a1b1) ),
inference(instantiation,[status(thm)],[c_5194]) ).
tcf(c_5200,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,a2b2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(b2,ob)
| ~ incident(b2,a2b2)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_4452]) ).
tcf(c_5203,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2b2,b2c2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(b2,a2b2)
| ~ incident(b2,b2c2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_4453]) ).
tcf(c_5205,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,b2c2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(b2,ob)
| ~ incident(b2,b2c2)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(instantiation,[status(thm)],[c_4453]) ).
tcf(c_5249,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2b2,oa)
| point_equal(a2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_498,c_4266]) ).
tcf(c_5253,plain,
( point_equal(a2,a1)
| line_equal(a2b2,oa)
| ~ incident(a1,oa)
| ~ incident(a1,a2b2) ),
inference(instantiation,[status(thm)],[c_5249]) ).
tcf(c_5299,plain,
( point_equal(b2,ab)
| line_equal(a1b1,a2b2)
| ~ incident(b2,a1b1)
| ~ incident(b2,a2b2)
| ~ incident(ab,a1b1)
| ~ incident(ab,a2b2) ),
inference(instantiation,[status(thm)],[c_4583]) ).
tcf(c_5352,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,o)
| line_equal(X0_iProver_incident_2,ob)
| ~ incident(o,ob)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_4634]) ).
tcf(c_5354,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,o)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(o,oc)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_4634]) ).
tcf(c_5356,plain,
! [X0_iProver_incident_2: iProver_incident_2,X1_iProver_incident_2: iProver_incident_2] :
( incident(o,X1_iProver_incident_2)
| ~ incident(o,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,X1_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_466]) ).
tcf(c_5357,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( incident(o,X0_iProver_incident_2)
| ~ point_equal(o,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_467]) ).
tcf(c_5358,plain,
( incident(o,a1b1)
| ~ point_equal(o,a1)
| ~ incident(a1,a1b1) ),
inference(instantiation,[status(thm)],[c_5357]) ).
tcf(c_5658,plain,
( incident(c2,b1c1)
| ~ incident(c2,a2c2)
| ~ line_equal(a2c2,b1c1) ),
inference(instantiation,[status(thm)],[c_2177]) ).
tcf(c_5716,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(a2,X0_iProver_incident_2)
| ~ point_equal(a2,b1)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2371]) ).
tcf(c_5720,plain,
( incident(a2,a1b1)
| ~ point_equal(a2,b1)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_5716]) ).
tcf(c_5729,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b1c1,b2c2)
| point_equal(bc,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_479,c_4272]) ).
tcf(c_5840,plain,
( incident(c2,b1c1)
| ~ incident(c2,oc)
| ~ line_equal(oc,b1c1) ),
inference(instantiation,[status(thm)],[c_2179]) ).
tcf(c_5843,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,b1c1)
| ~ line_equal(oc,b1c1)
| ~ incident(X0_iProver_incident_1,oc) ),
inference(instantiation,[status(thm)],[c_2604]) ).
tcf(c_5845,plain,
( incident(a1,b1c1)
| ~ incident(a1,oc)
| ~ line_equal(oc,b1c1) ),
inference(instantiation,[status(thm)],[c_2269]) ).
tcf(c_5861,plain,
( incident(b1,oc)
| ~ incident(b1,b1c1)
| ~ line_equal(b1c1,oc) ),
inference(instantiation,[status(thm)],[c_2265]) ).
tcf(c_5886,plain,
( point_equal(a1,a2)
| ~ point_equal(a1,ab)
| ~ point_equal(ab,a2) ),
inference(instantiation,[status(thm)],[c_2237]) ).
tcf(c_5924,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(a2c2,X0_iProver_incident_2)
| ~ incident(c2,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2190]) ).
tcf(c_5995,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(X0_iProver_incident_1,c2)
| line_equal(b2c2,X0_iProver_incident_2)
| ~ incident(c2,b2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2356]) ).
tcf(c_5996,plain,
( point_equal(a1,c2)
| line_equal(b2c2,a1b1)
| ~ incident(c2,a1b1)
| ~ incident(c2,b2c2)
| ~ incident(a1,a1b1)
| ~ incident(a1,b2c2) ),
inference(instantiation,[status(thm)],[c_5995]) ).
tcf(c_6027,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a1c1,a2c2)
| point_equal(ac,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(superposition,[status(thm)],[c_477,c_4274]) ).
tcf(c_6029,plain,
( point_equal(ac,a1)
| line_equal(a1c1,a2c2)
| ~ incident(a1,a1c1)
| ~ incident(a1,a2c2) ),
inference(instantiation,[status(thm)],[c_6027]) ).
tcf(c_6031,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2b2,a1b1)
| point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_474,c_4275]) ).
tcf(c_6065,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c2,ob)
| ~ incident(c2,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,ob) ),
inference(instantiation,[status(thm)],[c_2137]) ).
tcf(c_6066,plain,
( incident(c2,ob)
| ~ incident(c2,a1b1)
| ~ line_equal(a1b1,ob) ),
inference(instantiation,[status(thm)],[c_6065]) ).
tcf(c_6084,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(ab,oc)
| ~ point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc) ),
inference(instantiation,[status(thm)],[c_2566]) ).
tcf(c_6120,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(b2,c2)
| ~ point_equal(b2,X0_iProver_incident_1)
| ~ point_equal(X0_iProver_incident_1,c2) ),
inference(instantiation,[status(thm)],[c_2358]) ).
tcf(c_6121,plain,
( point_equal(b2,c2)
| ~ point_equal(b2,a1)
| ~ point_equal(a1,c2) ),
inference(instantiation,[status(thm)],[c_6120]) ).
tcf(c_6194,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| line_equal(a2c2,a1b1)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(superposition,[status(thm)],[c_493,c_4249]) ).
tcf(c_6195,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| line_equal(b2c2,a1b1)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_490,c_4249]) ).
tcf(c_6208,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a1c1,a2b2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(b2,a1c1)
| ~ incident(b2,a2b2)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_4452]) ).
tcf(c_6342,plain,
( incident(a2,b2c2)
| ~ incident(a2,oc)
| ~ line_equal(oc,b2c2) ),
inference(instantiation,[status(thm)],[c_2267]) ).
tcf(c_6464,plain,
( ~ incident(ab,oc)
| ~ incident(ac,oc)
| ~ incident(bc,oc) ),
inference(instantiation,[status(thm)],[c_454]) ).
tcf(c_6571,plain,
( line_equal(a1c1,oc)
| ~ line_equal(oc,a1c1) ),
inference(instantiation,[status(thm)],[c_2573]) ).
tcf(c_6583,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,a1b1)
| point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,a1b1) ),
inference(superposition,[status(thm)],[c_483,c_4251]) ).
tcf(c_6586,plain,
( point_equal(c1,bc)
| line_equal(oc,b1c1)
| ~ incident(c1,oc)
| ~ incident(c1,b1c1)
| ~ incident(bc,oc)
| ~ incident(bc,b1c1) ),
inference(instantiation,[status(thm)],[c_2799]) ).
tcf(c_6598,plain,
( incident(ac,oc)
| ~ incident(ac,a1c1)
| ~ line_equal(a1c1,oc) ),
inference(instantiation,[status(thm)],[c_2168]) ).
tcf(c_6600,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,oc)
| ~ line_equal(a1c1,oc)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(instantiation,[status(thm)],[c_2565]) ).
tcf(c_6603,plain,
( incident(a1,oc)
| ~ incident(a1,a1c1)
| ~ line_equal(a1c1,oc) ),
inference(instantiation,[status(thm)],[c_6600]) ).
tcf(c_6619,plain,
( point_equal(c1,b2)
| incident(a1,b2c2)
| line_equal(oc,a1c1)
| ~ incident(b2,oc) ),
inference(superposition,[status(thm)],[c_503,c_4290]) ).
tcf(c_6620,plain,
( point_equal(c1,a1)
| line_equal(oc,a1c1)
| ~ incident(a1,oc) ),
inference(superposition,[status(thm)],[c_496,c_4290]) ).
tcf(c_6638,plain,
( point_equal(c2,b2)
| line_equal(oc,b2c2)
| ~ incident(c2,oc)
| ~ incident(c2,b2c2)
| ~ incident(b2,oc)
| ~ incident(b2,b2c2) ),
inference(instantiation,[status(thm)],[c_2814]) ).
tcf(c_6642,plain,
( ~ incident(a1,oc)
| line_equal(oc,a1c1) ),
inference(global_subsumption_just,[status(thm)],[c_6620,c_59,c_56,c_55,c_507,c_515,c_4291]) ).
tcf(c_6643,plain,
( line_equal(oc,a1c1)
| ~ incident(a1,oc) ),
inference(renaming,[status(thm)],[c_6642]) ).
tcf(c_6645,plain,
( point_equal(c2,a2)
| line_equal(a2c2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,a2c2)
| ~ incident(a2,oc)
| ~ incident(a2,a2c2) ),
inference(instantiation,[status(thm)],[c_2817]) ).
tcf(c_6732,plain,
( point_equal(b2,c2)
| line_equal(b2c2,oc)
| ~ incident(c2,oc)
| ~ incident(c2,b2c2)
| ~ incident(b2,oc)
| ~ incident(b2,b2c2) ),
inference(instantiation,[status(thm)],[c_3668]) ).
tcf(c_6781,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(c2,a2b2)
| ~ point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_2847]) ).
tcf(c_6783,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(o,a2b2)
| ~ point_equal(o,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(instantiation,[status(thm)],[c_2847]) ).
tcf(c_6784,plain,
( incident(o,a2b2)
| ~ point_equal(o,a1)
| ~ incident(a1,a2b2) ),
inference(instantiation,[status(thm)],[c_6783]) ).
tcf(c_6834,plain,
( incident(b2,oa)
| ~ incident(b2,a2b2)
| ~ line_equal(a2b2,oa) ),
inference(instantiation,[status(thm)],[c_3083]) ).
tcf(c_6838,plain,
( line_equal(oa,a2b2)
| ~ line_equal(a2b2,oa) ),
inference(instantiation,[status(thm)],[c_2233]) ).
tcf(c_6875,plain,
( point_equal(c1,c2)
| line_equal(oc,b1c1)
| ~ incident(c2,b1c1) ),
inference(superposition,[status(thm)],[c_480,c_4318]) ).
tcf(c_6897,plain,
( ~ incident(c2,b1c1)
| line_equal(oc,b1c1) ),
inference(global_subsumption_just,[status(thm)],[c_6875,c_99,c_75,c_74,c_63,c_86,c_4390]) ).
tcf(c_6898,plain,
( line_equal(oc,b1c1)
| ~ incident(c2,b1c1) ),
inference(renaming,[status(thm)],[c_6897]) ).
tcf(c_6899,plain,
( point_equal(b1,c2)
| incident(b1,a2c2)
| line_equal(ob,a1b1)
| ~ incident(c2,ob) ),
inference(superposition,[status(thm)],[c_502,c_6583]) ).
tcf(c_6950,plain,
( point_equal(b1,c2)
| incident(b1,a2c2)
| ~ incident(c2,ob) ),
inference(global_subsumption_just,[status(thm)],[c_6899,c_99,c_80,c_75,c_74,c_70,c_66,c_62,c_61,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_53,c_506,c_507,c_513,c_550,c_563,c_731,c_747,c_886,c_981,c_985,c_986,c_988,c_1140,c_1141,c_1308,c_1311,c_1314,c_1390,c_3834,c_3845,c_3851,c_4741,c_6029,c_6121]) ).
tcf(c_7016,plain,
( point_equal(c2,c1)
| line_equal(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(superposition,[status(thm)],[c_481,c_4325]) ).
tcf(c_7049,plain,
( ~ incident(c1,b2c2)
| line_equal(oc,b2c2) ),
inference(global_subsumption_just,[status(thm)],[c_7016,c_99,c_86,c_7016]) ).
tcf(c_7050,plain,
( line_equal(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(renaming,[status(thm)],[c_7049]) ).
tcf(c_7076,plain,
( incident(c2,b1c1)
| ~ point_equal(c2,b1)
| ~ incident(b1,b1c1) ),
inference(instantiation,[status(thm)],[c_3342]) ).
tcf(c_7085,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oa,a2b2)
| point_equal(a2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_484,c_4252]) ).
tcf(c_7088,plain,
( point_equal(a2,b2)
| line_equal(oa,a2b2)
| ~ incident(b2,oa) ),
inference(superposition,[status(thm)],[c_497,c_7085]) ).
tcf(c_7107,plain,
( incident(b1,a2c2)
| ~ point_equal(b1,c2)
| ~ incident(c2,a2c2) ),
inference(instantiation,[status(thm)],[c_3103]) ).
tcf(c_7111,plain,
( incident(b1,b2c2)
| ~ point_equal(b1,c2)
| ~ incident(c2,b2c2) ),
inference(instantiation,[status(thm)],[c_2433]) ).
tcf(c_7119,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,c2)
| line_equal(X0_iProver_incident_2,oc)
| ~ incident(c2,oc)
| ~ incident(b1,oc)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2824]) ).
tcf(c_7122,plain,
( point_equal(b1,c2)
| line_equal(a1b1,oc)
| ~ incident(c2,oc)
| ~ incident(c2,a1b1)
| ~ incident(b1,oc)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_7119]) ).
tcf(c_7125,plain,
( ~ incident(b2,oa)
| line_equal(oa,a2b2) ),
inference(global_subsumption_just,[status(thm)],[c_7088,c_71,c_62,c_61,c_58,c_57,c_550,c_1140,c_5061,c_6838]) ).
tcf(c_7126,plain,
( line_equal(oa,a2b2)
| ~ incident(b2,oa) ),
inference(renaming,[status(thm)],[c_7125]) ).
tcf(c_7159,plain,
( ~ incident(b2,oa)
| line_equal(a2b2,oa) ),
inference(global_subsumption_just,[status(thm)],[c_4353,c_71,c_62,c_61,c_58,c_57,c_550,c_1140,c_5061]) ).
tcf(c_7160,plain,
( line_equal(a2b2,oa)
| ~ incident(b2,oa) ),
inference(renaming,[status(thm)],[c_7159]) ).
tcf(c_7182,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(c1,X0_iProver_incident_2)
| ~ point_equal(c1,b1)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2139]) ).
tcf(c_7183,plain,
( incident(c1,a1b1)
| ~ point_equal(c1,b1)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_7182]) ).
tcf(c_7445,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(bc,X0_iProver_incident_2)
| ~ point_equal(bc,b1)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_3900]) ).
tcf(c_7446,plain,
( incident(bc,a1b1)
| ~ point_equal(bc,b1)
| ~ incident(b1,a1b1) ),
inference(instantiation,[status(thm)],[c_7445]) ).
tcf(c_7629,plain,
( point_equal(o,a1)
| ~ incident(a1,ob) ),
inference(global_subsumption_just,[status(thm)],[c_4517,c_99,c_80,c_75,c_74,c_70,c_66,c_64,c_63,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_86,c_54,c_53,c_126,c_506,c_507,c_513,c_533,c_549,c_550,c_551,c_559,c_563,c_629,c_694,c_731,c_747,c_886,c_981,c_985,c_986,c_988,c_1140,c_1141,c_1308,c_1310,c_1311,c_1314,c_1390,c_3684,c_3781,c_3834,c_3851,c_4720,c_4741,c_5658,c_5720,c_5845,c_6029,c_6121,c_6875]) ).
tcf(c_7668,plain,
( incident(b2,a2c2)
| ~ incident(b2,oc)
| ~ line_equal(oc,a2c2) ),
inference(instantiation,[status(thm)],[c_2271]) ).
tcf(c_7885,plain,
( point_equal(b1,o)
| line_equal(ob,oc)
| ~ incident(o,oc)
| ~ incident(o,ob)
| ~ incident(b1,oc)
| ~ incident(b1,ob) ),
inference(instantiation,[status(thm)],[c_5146]) ).
tcf(c_7910,plain,
( ~ incident(b2,oc)
| line_equal(b2c2,oc) ),
inference(global_subsumption_just,[status(thm)],[c_5009,c_75,c_66,c_65,c_62,c_61,c_550,c_1141,c_6732]) ).
tcf(c_7911,plain,
( line_equal(b2c2,oc)
| ~ incident(b2,oc) ),
inference(renaming,[status(thm)],[c_7910]) ).
tcf(c_7912,plain,
( point_equal(o,a1)
| line_equal(oa,oc)
| ~ incident(a1,oc) ),
inference(global_subsumption_just,[status(thm)],[c_5013,c_99,c_80,c_75,c_74,c_72,c_70,c_69,c_68,c_67,c_66,c_64,c_63,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_54,c_53,c_126,c_506,c_507,c_513,c_547,c_549,c_550,c_559,c_563,c_629,c_731,c_747,c_886,c_981,c_985,c_986,c_988,c_1107,c_1140,c_1141,c_1308,c_1310,c_1311,c_1314,c_1390,c_3684,c_3834,c_3851,c_4720,c_4741,c_5013,c_5147,c_5358,c_5658,c_5720,c_5845,c_6029,c_6121,c_6898]) ).
tcf(c_7976,plain,
( ~ incident(ac,a1b1)
| ~ incident(bc,a1b1) ),
inference(resolution,[status(thm)],[c_454,c_475]) ).
tcf(c_7984,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,o)
| line_equal(X0_iProver_incident_2,ob)
| ~ incident(o,ob)
| ~ incident(b1,ob)
| ~ incident(o,X0_iProver_incident_2)
| ~ incident(b1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_5182]) ).
tcf(c_8051,plain,
( incident(c1,a2b2)
| ~ incident(c2,a1b1)
| ~ incident(b2,a1c1) ),
inference(superposition,[status(thm)],[c_501,c_456]) ).
tcf(c_8052,plain,
( incident(c1,a2b2)
| incident(a1,b2c2)
| ~ incident(c2,a1b1) ),
inference(superposition,[status(thm)],[c_503,c_8051]) ).
tcf(c_8142,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(o,X0_iProver_incident_2)
| ~ line_equal(oc,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_486,c_466]) ).
tcf(c_8154,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(ab,X0_iProver_incident_2)
| ~ line_equal(a2b2,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_474,c_466]) ).
tcf(c_8169,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,b2c2)
| ~ point_equal(X0_iProver_incident_1,b2) ),
inference(superposition,[status(thm)],[c_489,c_467]) ).
tcf(c_8173,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,oa)
| ~ point_equal(X0_iProver_incident_1,a1) ),
inference(superposition,[status(thm)],[c_485,c_467]) ).
tcf(c_8183,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,a1b1)
| ~ point_equal(X0_iProver_incident_1,ab) ),
inference(superposition,[status(thm)],[c_475,c_467]) ).
tcf(c_8184,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,a2b2)
| ~ point_equal(X0_iProver_incident_1,ab) ),
inference(superposition,[status(thm)],[c_474,c_467]) ).
tcf(c_8219,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(a1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_500,c_465]) ).
tcf(c_8220,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(b1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_499,c_465]) ).
tcf(c_8222,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2b2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_497,c_465]) ).
tcf(c_8224,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1c1)
| ~ incident(c1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_495,c_465]) ).
tcf(c_8226,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_493,c_465]) ).
tcf(c_8229,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_490,c_465]) ).
tcf(c_8230,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(b2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b2c2)
| ~ incident(b2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_489,c_465]) ).
tcf(c_8234,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a1,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(a1,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_485,c_465]) ).
tcf(c_8235,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(a2,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,oa)
| ~ incident(a2,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_484,c_465]) ).
tcf(c_8240,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(bc,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,b1c1)
| ~ incident(bc,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_479,c_465]) ).
tcf(c_8244,plain,
! [X0_iProver_incident_1: iProver_incident_1,X0_iProver_incident_2: iProver_incident_2] :
( point_equal(ab,X0_iProver_incident_1)
| line_equal(X0_iProver_incident_2,a1b1)
| ~ incident(ab,X0_iProver_incident_2)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,X0_iProver_incident_2) ),
inference(superposition,[status(thm)],[c_475,c_465]) ).
tcf(c_8295,plain,
( incident(c1,a2b2)
| incident(b1,a2c2)
| incident(a1,b2c2) ),
inference(superposition,[status(thm)],[c_502,c_8052]) ).
tcf(c_8323,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a1c1,a1b1)
| point_equal(a1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(superposition,[status(thm)],[c_496,c_8219]) ).
tcf(c_8324,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oa,a1b1)
| point_equal(a1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a1b1) ),
inference(superposition,[status(thm)],[c_485,c_8219]) ).
tcf(c_8325,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,a1b1)
| point_equal(a1,X0_iProver_incident_1) ),
inference(global_subsumption_just,[status(thm)],[c_8323,c_60,c_56,c_55,c_507,c_559,c_3730]) ).
tcf(c_8326,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(a1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(renaming,[status(thm)],[c_8325]) ).
tcf(c_8330,plain,
( point_equal(a1,ab)
| ~ incident(ab,a1c1) ),
inference(superposition,[status(thm)],[c_475,c_8326]) ).
tcf(c_8334,plain,
( point_equal(a1,ab)
| line_equal(oa,a1b1)
| ~ incident(ab,oa) ),
inference(superposition,[status(thm)],[c_475,c_8324]) ).
tcf(c_8341,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,a1b1)
| point_equal(b1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,a1b1) ),
inference(superposition,[status(thm)],[c_483,c_8220]) ).
tcf(c_8351,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(b2c2,b1c1)
| point_equal(bc,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_478,c_8240]) ).
tcf(c_8352,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,b1c1)
| point_equal(bc,X0_iProver_incident_1) ),
inference(global_subsumption_just,[status(thm)],[c_8351,c_99,c_87,c_5729]) ).
tcf(c_8353,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(bc,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,b1c1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(renaming,[status(thm)],[c_8352]) ).
tcf(c_8354,plain,
( point_equal(bc,c2)
| ~ incident(c2,b1c1) ),
inference(superposition,[status(thm)],[c_490,c_8353]) ).
tcf(c_8361,plain,
( point_equal(b1,c2)
| incident(b1,a2c2)
| line_equal(ob,a1b1)
| ~ incident(c2,ob) ),
inference(superposition,[status(thm)],[c_502,c_8341]) ).
tcf(c_8367,plain,
( ~ incident(c2,ob)
| incident(b1,a2c2) ),
inference(global_subsumption_just,[status(thm)],[c_8361,c_62,c_6950,c_7107]) ).
tcf(c_8368,plain,
( incident(b1,a2c2)
| ~ incident(c2,ob) ),
inference(renaming,[status(thm)],[c_8367]) ).
tcf(c_8390,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2b2,a1b1)
| point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_474,c_8244]) ).
tcf(c_8391,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( ~ incident(X0_iProver_incident_1,a2b2)
| ~ incident(X0_iProver_incident_1,a1b1)
| point_equal(ab,X0_iProver_incident_1) ),
inference(global_subsumption_just,[status(thm)],[c_8390,c_99,c_89,c_543,c_6031]) ).
tcf(c_8392,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(ab,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(renaming,[status(thm)],[c_8391]) ).
tcf(c_8395,plain,
( point_equal(ab,a2)
| ~ incident(a2,a1b1) ),
inference(superposition,[status(thm)],[c_498,c_8392]) ).
tcf(c_8396,plain,
( point_equal(ab,b2)
| ~ incident(b2,a1b1) ),
inference(superposition,[status(thm)],[c_497,c_8392]) ).
tcf(c_8410,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(a1,b2c2)
| line_equal(a1c1,a2b2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_503,c_8222]) ).
tcf(c_8422,plain,
( point_equal(b2,c1)
| incident(b1,a2c2)
| incident(a1,b2c2)
| line_equal(a1c1,a2b2)
| ~ incident(c1,a1c1) ),
inference(superposition,[status(thm)],[c_8295,c_8410]) ).
tcf(c_8438,plain,
( point_equal(b2,c1)
| incident(b1,a2c2)
| incident(a1,b2c2)
| line_equal(a1c1,a2b2) ),
inference(global_subsumption_just,[status(thm)],[c_8422,c_60,c_8422]) ).
tcf(c_8441,plain,
( point_equal(c1,b2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| line_equal(a1c1,a2b2) ),
inference(superposition,[status(thm)],[c_8438,c_472]) ).
tcf(c_8451,plain,
( incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| line_equal(a1c1,a2b2) ),
inference(superposition,[status(thm)],[c_8441,c_8169]) ).
tcf(c_8480,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a1b1,oa)
| point_equal(a1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a1b1) ),
inference(superposition,[status(thm)],[c_500,c_8234]) ).
tcf(c_8500,plain,
( incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| line_equal(a2b2,a1c1) ),
inference(superposition,[status(thm)],[c_8451,c_469]) ).
tcf(c_8565,plain,
( incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| incident(ab,a1c1) ),
inference(superposition,[status(thm)],[c_8500,c_8154]) ).
tcf(c_8580,plain,
( point_equal(a1,b1)
| line_equal(a1b1,oa)
| ~ incident(b1,oa) ),
inference(superposition,[status(thm)],[c_499,c_8480]) ).
tcf(c_8581,plain,
( point_equal(a1,ab)
| line_equal(a1b1,oa)
| ~ incident(ab,oa) ),
inference(superposition,[status(thm)],[c_475,c_8480]) ).
tcf(c_8734,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,a1c1)
| point_equal(c1,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,a1c1) ),
inference(superposition,[status(thm)],[c_481,c_8224]) ).
tcf(c_8804,plain,
( point_equal(b2,o)
| line_equal(ob,a2b2)
| ~ incident(o,ob)
| ~ incident(o,a2b2)
| ~ incident(b2,ob)
| ~ incident(b2,a2b2) ),
inference(instantiation,[status(thm)],[c_5200]) ).
tcf(c_8824,plain,
( point_equal(a1,ab)
| incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2) ),
inference(superposition,[status(thm)],[c_8565,c_8330]) ).
tcf(c_8845,plain,
( point_equal(b2,o)
| line_equal(ob,b2c2)
| ~ incident(o,ob)
| ~ incident(o,b2c2)
| ~ incident(b2,ob)
| ~ incident(b2,b2c2) ),
inference(instantiation,[status(thm)],[c_5205]) ).
tcf(c_8930,plain,
( point_equal(c1,b2)
| incident(a1,b2c2)
| line_equal(oc,a1c1)
| ~ incident(b2,oc) ),
inference(superposition,[status(thm)],[c_503,c_8734]) ).
tcf(c_8939,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oa,ob)
| point_equal(X0_iProver_incident_1,o)
| ~ incident(o,ob)
| ~ incident(o,oa)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,oa) ),
inference(instantiation,[status(thm)],[c_5352]) ).
tcf(c_8946,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oa,oc)
| point_equal(X0_iProver_incident_1,o)
| ~ incident(o,oc)
| ~ incident(o,oa)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,oa) ),
inference(instantiation,[status(thm)],[c_5354]) ).
tcf(c_8947,plain,
( point_equal(a1,o)
| line_equal(oa,oc)
| ~ incident(o,oc)
| ~ incident(o,oa)
| ~ incident(a1,oc)
| ~ incident(a1,oa) ),
inference(instantiation,[status(thm)],[c_8946]) ).
tcf(c_8955,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(o,X0_iProver_incident_2)
| ~ incident(o,oc)
| ~ line_equal(oc,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_5356]) ).
tcf(c_9085,plain,
( incident(b2,b1c1)
| ~ incident(b2,oc)
| ~ line_equal(oc,b1c1) ),
inference(instantiation,[status(thm)],[c_5843]) ).
tcf(c_9151,plain,
( point_equal(c1,b2)
| ~ incident(b2,oc)
| line_equal(oc,a1c1) ),
inference(global_subsumption_just,[status(thm)],[c_8930,c_99,c_75,c_74,c_73,c_72,c_71,c_70,c_69,c_68,c_65,c_64,c_63,c_62,c_61,c_60,c_59,c_56,c_55,c_86,c_85,c_84,c_54,c_50,c_550,c_551,c_694,c_747,c_827,c_989,c_990,c_1107,c_1304,c_1308,c_1783,c_3684,c_3830,c_4328,c_4400,c_4636,c_5105,c_5147,c_5152,c_5188,c_5195,c_5658,c_5720,c_5861,c_6619,c_6643,c_7111,c_7629,c_7668]) ).
tcf(c_9152,plain,
( point_equal(c1,b2)
| line_equal(oc,a1c1)
| ~ incident(b2,oc) ),
inference(renaming,[status(thm)],[c_9151]) ).
tcf(c_9214,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( point_equal(c2,a2)
| line_equal(a2c2,X0_iProver_incident_2)
| ~ incident(c2,a2c2)
| ~ incident(a2,a2c2)
| ~ incident(c2,X0_iProver_incident_2)
| ~ incident(a2,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_5924]) ).
tcf(c_9215,plain,
( point_equal(c2,a2)
| line_equal(a2c2,a1b1)
| ~ incident(c2,a1b1)
| ~ incident(c2,a2c2)
| ~ incident(a2,a1b1)
| ~ incident(a2,a2c2) ),
inference(instantiation,[status(thm)],[c_9214]) ).
tcf(c_9672,plain,
( ~ incident(bc,a1b1)
| ~ line_equal(a2c2,a1b1) ),
inference(resolution,[status(thm)],[c_7976,c_3301]) ).
tcf(c_9731,plain,
( point_equal(b2,c1)
| line_equal(a1c1,a2b2)
| ~ incident(b2,a1c1)
| ~ incident(b2,a2b2)
| ~ incident(c1,a1c1)
| ~ incident(c1,a2b2) ),
inference(instantiation,[status(thm)],[c_6208]) ).
tcf(c_10001,plain,
( incident(c2,a2b2)
| ~ point_equal(c2,a2)
| ~ incident(a2,a2b2) ),
inference(instantiation,[status(thm)],[c_6781]) ).
tcf(c_10002,plain,
( incident(c2,a2b2)
| ~ point_equal(c2,b2)
| ~ incident(b2,a2b2) ),
inference(instantiation,[status(thm)],[c_6781]) ).
tcf(c_10110,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| line_equal(a1b1,a2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(superposition,[status(thm)],[c_502,c_8226]) ).
tcf(c_10181,plain,
( incident(bc,a2c2)
| ~ point_equal(bc,c2)
| ~ incident(c2,a2c2) ),
inference(instantiation,[status(thm)],[c_3103]) ).
tcf(c_10192,plain,
( point_equal(ab,a1)
| incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2) ),
inference(superposition,[status(thm)],[c_8824,c_472]) ).
tcf(c_11119,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(bc,oc)
| ~ incident(bc,X0_iProver_incident_2)
| ~ line_equal(X0_iProver_incident_2,oc) ),
inference(instantiation,[status(thm)],[c_3899]) ).
tcf(c_11228,plain,
( incident(b1,a1c1)
| ~ point_equal(b1,ac)
| ~ incident(ac,a1c1) ),
inference(instantiation,[status(thm)],[c_2274]) ).
tcf(c_11447,plain,
( incident(b1,oa)
| ~ incident(b1,a2b2)
| ~ line_equal(a2b2,oa) ),
inference(instantiation,[status(thm)],[c_4929]) ).
tcf(c_11448,plain,
( incident(ab,oa)
| ~ incident(ab,a2b2)
| ~ line_equal(a2b2,oa) ),
inference(instantiation,[status(thm)],[c_4925]) ).
tcf(c_11513,plain,
( line_equal(a2c2,a1c1)
| ~ line_equal(oc,a1c1)
| ~ line_equal(a2c2,oc) ),
inference(instantiation,[status(thm)],[c_2252]) ).
tcf(c_11523,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( line_equal(X0_iProver_incident_2,oc)
| ~ line_equal(a2c2,oc)
| ~ line_equal(X0_iProver_incident_2,a2c2) ),
inference(instantiation,[status(thm)],[c_2572]) ).
tcf(c_11524,plain,
( line_equal(a1b1,oc)
| ~ line_equal(a1b1,a2c2)
| ~ line_equal(a2c2,oc) ),
inference(instantiation,[status(thm)],[c_11523]) ).
tcf(c_11527,plain,
( incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,b2c2)
| incident(ab,oa) ),
inference(superposition,[status(thm)],[c_10192,c_8173]) ).
tcf(c_11569,plain,
( incident(b1,b2c2)
| ~ incident(b1,ob)
| ~ line_equal(ob,b2c2) ),
inference(instantiation,[status(thm)],[c_2432]) ).
tcf(c_11583,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| ~ incident(X0_iProver_incident_1,a2c2)
| ~ incident(X0_iProver_incident_1,a1b1)
| point_equal(c2,X0_iProver_incident_1) ),
inference(global_subsumption_just,[status(thm)],[c_10110,c_99,c_80,c_75,c_74,c_72,c_71,c_70,c_69,c_68,c_66,c_62,c_61,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_84,c_53,c_506,c_507,c_513,c_550,c_563,c_731,c_747,c_886,c_981,c_985,c_986,c_988,c_989,c_994,c_1107,c_1140,c_1141,c_1308,c_1311,c_1314,c_1390,c_3830,c_3834,c_3851,c_4741,c_5147,c_6029,c_6121,c_6194,c_7107,c_7122]) ).
tcf(c_11584,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,a2c2) ),
inference(renaming,[status(thm)],[c_11583]) ).
tcf(c_11587,plain,
( point_equal(c2,a1)
| incident(b1,a2c2)
| ~ incident(a1,a2c2) ),
inference(superposition,[status(thm)],[c_500,c_11584]) ).
tcf(c_11677,plain,
( point_equal(c2,a1)
| ~ incident(a1,a2c2) ),
inference(global_subsumption_just,[status(thm)],[c_11587,c_99,c_80,c_79,c_78,c_77,c_76,c_75,c_74,c_72,c_71,c_70,c_69,c_68,c_66,c_65,c_64,c_62,c_61,c_60,c_59,c_56,c_55,c_88,c_87,c_84,c_506,c_507,c_513,c_550,c_551,c_559,c_563,c_629,c_690,c_731,c_985,c_989,c_994,c_1107,c_1135,c_2018,c_3830,c_3898,c_3987,c_4031,c_4314,c_5120,c_5147,c_6029,c_7111,c_7446,c_11228,c_11524,c_11587]) ).
tcf(c_12150,plain,
( line_equal(a2b2,oa)
| ~ line_equal(oa,a2b2) ),
inference(instantiation,[status(thm)],[c_2488]) ).
tcf(c_12151,plain,
( incident(a1,a2b2)
| ~ incident(a1,oa)
| ~ line_equal(oa,a2b2) ),
inference(instantiation,[status(thm)],[c_2474]) ).
tcf(c_12337,plain,
( point_equal(b2,b1)
| line_equal(a2b2,b2c2)
| ~ incident(b2,a2b2)
| ~ incident(b2,b2c2)
| ~ incident(b1,a2b2)
| ~ incident(b1,b2c2) ),
inference(instantiation,[status(thm)],[c_5203]) ).
tcf(c_12499,plain,
( incident(c2,ob)
| ~ incident(c2,b2c2)
| ~ line_equal(b2c2,ob) ),
inference(instantiation,[status(thm)],[c_2178]) ).
tcf(c_12526,plain,
~ line_equal(a2c2,a1b1),
inference(global_subsumption_just,[status(thm)],[c_9672,c_99,c_80,c_75,c_74,c_71,c_70,c_66,c_62,c_61,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_84,c_506,c_507,c_513,c_550,c_563,c_731,c_747,c_827,c_886,c_981,c_985,c_986,c_988,c_989,c_993,c_994,c_1066,c_1073,c_1140,c_1141,c_1304,c_1308,c_1309,c_1311,c_1314,c_1390,c_3830,c_3834,c_3851,c_3865,c_4741,c_4745,c_6029,c_6121,c_11677]) ).
tcf(c_13056,plain,
( point_equal(b1,o)
| line_equal(oa,ob)
| ~ incident(o,ob)
| ~ incident(o,oa)
| ~ incident(b1,ob)
| ~ incident(b1,oa) ),
inference(instantiation,[status(thm)],[c_7984]) ).
tcf(c_13188,plain,
( point_equal(b2,o)
| line_equal(oa,ob)
| ~ incident(o,ob)
| ~ incident(o,oa)
| ~ incident(b2,ob)
| ~ incident(b2,oa) ),
inference(instantiation,[status(thm)],[c_8939]) ).
tcf(c_13250,plain,
( incident(a2,oc)
| ~ incident(a2,oa)
| ~ line_equal(oa,oc) ),
inference(instantiation,[status(thm)],[c_2863]) ).
tcf(c_13367,plain,
( incident(c1,b2c2)
| incident(b1,a2c2)
| incident(ab,oa) ),
inference(global_subsumption_just,[status(thm)],[c_11527,c_99,c_80,c_75,c_74,c_73,c_72,c_71,c_70,c_69,c_67,c_66,c_65,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_85,c_53,c_506,c_507,c_513,c_515,c_541,c_550,c_551,c_563,c_694,c_731,c_747,c_886,c_981,c_985,c_986,c_988,c_990,c_1083,c_1140,c_1141,c_1304,c_1308,c_1309,c_1311,c_1314,c_1390,c_3689,c_3781,c_3834,c_3851,c_4433,c_4741,c_4928,c_5996,c_6029,c_6121,c_6620,c_6645,c_8824,c_8947,c_10001,c_11513,c_13250]) ).
tcf(c_13376,plain,
( point_equal(a1,ab)
| incident(c1,b2c2)
| incident(b1,a2c2)
| line_equal(a1b1,oa) ),
inference(superposition,[status(thm)],[c_13367,c_8581]) ).
tcf(c_13378,plain,
( point_equal(a1,ab)
| incident(c1,b2c2)
| incident(b1,a2c2)
| line_equal(oa,a1b1) ),
inference(superposition,[status(thm)],[c_13367,c_8334]) ).
tcf(c_13696,plain,
( point_equal(a1,ab)
| incident(c1,b2c2)
| incident(b1,a2c2) ),
inference(global_subsumption_just,[status(thm)],[c_13376,c_99,c_80,c_75,c_74,c_71,c_70,c_66,c_62,c_61,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_84,c_53,c_506,c_507,c_513,c_550,c_563,c_731,c_747,c_827,c_886,c_981,c_985,c_986,c_988,c_989,c_993,c_994,c_1066,c_1073,c_1140,c_1141,c_1304,c_1308,c_1309,c_1311,c_1314,c_1390,c_3689,c_3830,c_3834,c_3851,c_3865,c_4741,c_4745,c_6029,c_6121,c_9215,c_10001,c_11677,c_13378]) ).
tcf(c_13700,plain,
( incident(c1,b2c2)
| incident(b1,a2c2)
| incident(a1,a2b2) ),
inference(superposition,[status(thm)],[c_13696,c_8184]) ).
tcf(c_14324,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| line_equal(a1b1,b2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_502,c_8229]) ).
tcf(c_14327,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(oc,b2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oc)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_480,c_8229]) ).
tcf(c_14368,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,a1b1)
| point_equal(c2,X0_iProver_incident_1) ),
inference(global_subsumption_just,[status(thm)],[c_14324,c_99,c_73,c_72,c_56,c_85,c_53,c_990,c_5188,c_6066,c_6195,c_8368]) ).
tcf(c_14369,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(b1,a2c2)
| point_equal(c2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1b1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(renaming,[status(thm)],[c_14368]) ).
tcf(c_14373,plain,
( point_equal(c2,b1)
| incident(b1,a2c2)
| ~ incident(b1,b2c2) ),
inference(superposition,[status(thm)],[c_499,c_14369]) ).
tcf(c_14523,plain,
( point_equal(c2,c1)
| line_equal(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(superposition,[status(thm)],[c_481,c_14327]) ).
tcf(c_15329,plain,
( incident(b1,oa)
| ~ point_equal(b1,o)
| ~ incident(o,oa) ),
inference(instantiation,[status(thm)],[c_4931]) ).
tcf(c_15457,plain,
( point_equal(bc,c1)
| ~ point_equal(c1,bc) ),
inference(instantiation,[status(thm)],[c_2214]) ).
tcf(c_15483,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(bc,X0_iProver_incident_2)
| ~ point_equal(bc,c1)
| ~ incident(c1,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_3900]) ).
tcf(c_15531,plain,
( incident(bc,oc)
| ~ incident(bc,b2c2)
| ~ line_equal(b2c2,oc) ),
inference(instantiation,[status(thm)],[c_11119]) ).
tcf(c_15717,plain,
~ incident(b1,b2c2),
inference(global_subsumption_just,[status(thm)],[c_14373,c_99,c_75,c_73,c_72,c_69,c_68,c_67,c_66,c_65,c_64,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_87,c_86,c_85,c_528,c_533,c_548,c_550,c_551,c_596,c_694,c_709,c_986,c_1038,c_1088,c_1109,c_1113,c_1135,c_1664,c_1753,c_3596,c_3757,c_3983,c_4865,c_6875,c_7076,c_7885,c_8368,c_9085,c_12337,c_12499,c_12526,c_15329]) ).
tcf(c_15723,plain,
( ~ incident(c1,b2c2)
| line_equal(oc,b2c2) ),
inference(global_subsumption_just,[status(thm)],[c_14523,c_7050]) ).
tcf(c_15724,plain,
( line_equal(oc,b2c2)
| ~ incident(c1,b2c2) ),
inference(renaming,[status(thm)],[c_15723]) ).
tcf(c_15725,plain,
( incident(b1,a2c2)
| incident(a1,a2b2)
| line_equal(oc,b2c2) ),
inference(superposition,[status(thm)],[c_13700,c_15724]) ).
tcf(c_15777,plain,
( incident(ab,oc)
| ~ point_equal(ab,b2)
| ~ incident(b2,oc) ),
inference(instantiation,[status(thm)],[c_6084]) ).
tcf(c_15814,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(a1,b2c2)
| line_equal(a1c1,b2c2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,a1c1)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_503,c_8230]) ).
tcf(c_15817,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(ob,b2c2)
| point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(superposition,[status(thm)],[c_482,c_8230]) ).
tcf(c_15824,plain,
( point_equal(b2,c1)
| incident(a1,b2c2)
| line_equal(a1c1,b2c2)
| ~ incident(c1,b2c2) ),
inference(superposition,[status(thm)],[c_495,c_15814]) ).
tcf(c_15842,plain,
( incident(o,b2c2)
| ~ incident(o,oc)
| ~ line_equal(oc,b2c2) ),
inference(instantiation,[status(thm)],[c_8955]) ).
tcf(c_15875,plain,
( line_equal(b2c2,b1c1)
| ~ line_equal(oc,b1c1)
| ~ line_equal(b2c2,oc) ),
inference(instantiation,[status(thm)],[c_2247]) ).
tcf(c_15886,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( ~ incident(X0_iProver_incident_1,b2c2)
| ~ incident(X0_iProver_incident_1,ob)
| point_equal(b2,X0_iProver_incident_1) ),
inference(global_subsumption_just,[status(thm)],[c_15817,c_99,c_80,c_75,c_74,c_73,c_72,c_71,c_70,c_69,c_68,c_67,c_66,c_65,c_64,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_87,c_86,c_85,c_84,c_506,c_507,c_513,c_528,c_533,c_548,c_550,c_551,c_563,c_596,c_694,c_709,c_731,c_747,c_827,c_886,c_981,c_985,c_986,c_988,c_989,c_993,c_994,c_1038,c_1066,c_1073,c_1088,c_1109,c_1113,c_1135,c_1140,c_1141,c_1304,c_1308,c_1309,c_1311,c_1314,c_1390,c_1664,c_1753,c_3596,c_3757,c_3830,c_3834,c_3851,c_3865,c_3983,c_4344,c_4741,c_4745,c_4865,c_6029,c_6121,c_6875,c_7076,c_7885,c_8368,c_9085,c_11569,c_11677,c_12337,c_12499,c_15329]) ).
tcf(c_15887,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( point_equal(b2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,ob)
| ~ incident(X0_iProver_incident_1,b2c2) ),
inference(renaming,[status(thm)],[c_15886]) ).
tcf(c_16026,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( line_equal(a2b2,oa)
| point_equal(a2,X0_iProver_incident_1)
| ~ incident(X0_iProver_incident_1,oa)
| ~ incident(X0_iProver_incident_1,a2b2) ),
inference(superposition,[status(thm)],[c_498,c_8235]) ).
tcf(c_16107,plain,
( incident(b2,a2c2)
| ~ point_equal(b2,ab)
| ~ incident(ab,a2c2) ),
inference(instantiation,[status(thm)],[c_2272]) ).
tcf(c_16266,plain,
( incident(o,b2c2)
| incident(b1,a2c2)
| incident(a1,a2b2) ),
inference(superposition,[status(thm)],[c_15725,c_8142]) ).
tcf(c_16332,plain,
! [X0_iProver_incident_2: iProver_incident_2] :
( incident(b2,X0_iProver_incident_2)
| ~ point_equal(b2,o)
| ~ incident(o,X0_iProver_incident_2) ),
inference(instantiation,[status(thm)],[c_2505]) ).
tcf(c_16333,plain,
( incident(b2,a1b1)
| ~ point_equal(b2,o)
| ~ incident(o,a1b1) ),
inference(instantiation,[status(thm)],[c_16332]) ).
tcf(c_16345,plain,
( point_equal(b2,o)
| incident(b1,a2c2)
| incident(a1,a2b2)
| ~ incident(o,ob) ),
inference(superposition,[status(thm)],[c_16266,c_15887]) ).
tcf(c_16504,plain,
( point_equal(b2,c1)
| ~ point_equal(c1,b2) ),
inference(instantiation,[status(thm)],[c_2214]) ).
tcf(c_18110,plain,
( point_equal(b2,c1)
| ~ incident(c1,b2c2) ),
inference(global_subsumption_just,[status(thm)],[c_15824,c_99,c_80,c_78,c_77,c_75,c_74,c_73,c_72,c_71,c_70,c_69,c_68,c_67,c_66,c_65,c_64,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_89,c_88,c_87,c_86,c_85,c_84,c_506,c_507,c_513,c_528,c_533,c_548,c_550,c_551,c_563,c_596,c_694,c_709,c_731,c_747,c_827,c_886,c_981,c_985,c_986,c_988,c_989,c_993,c_994,c_1038,c_1066,c_1073,c_1087,c_1088,c_1109,c_1113,c_1135,c_1140,c_1141,c_1304,c_1308,c_1309,c_1311,c_1314,c_1390,c_1664,c_1753,c_2119,c_3596,c_3757,c_3830,c_3834,c_3851,c_3865,c_3983,c_4741,c_4745,c_4865,c_5358,c_6029,c_6121,c_6342,c_6464,c_6571,c_6598,c_6603,c_6875,c_7016,c_7076,c_7885,c_7912,c_8368,c_8396,c_8845,c_9085,c_9152,c_11569,c_11677,c_12337,c_12499,c_13250,c_15329,c_15531,c_15777,c_15842,c_16333,c_16504]) ).
tcf(c_18112,plain,
( point_equal(b2,c1)
| incident(b1,a2c2)
| incident(a1,a2b2) ),
inference(superposition,[status(thm)],[c_13700,c_18110]) ).
tcf(c_18155,plain,
( point_equal(a2,ab)
| line_equal(a2b2,oa)
| ~ incident(ab,oa) ),
inference(superposition,[status(thm)],[c_474,c_16026]) ).
tcf(c_18600,plain,
( incident(bc,a1c1)
| ~ point_equal(bc,c1)
| ~ incident(c1,a1c1) ),
inference(instantiation,[status(thm)],[c_15483]) ).
tcf(c_18816,plain,
( point_equal(c1,b2)
| incident(b1,a2c2)
| incident(a1,a2b2) ),
inference(superposition,[status(thm)],[c_18112,c_472]) ).
tcf(c_18896,plain,
( incident(b2,oa)
| ~ point_equal(b2,o)
| ~ incident(o,oa) ),
inference(instantiation,[status(thm)],[c_16332]) ).
tcf(c_19088,plain,
( incident(a1,a2b2)
| ~ incident(a1,a1c1)
| ~ line_equal(a1c1,a2b2) ),
inference(instantiation,[status(thm)],[c_2474]) ).
tcf(c_19098,plain,
( incident(a1,a2b2)
| incident(b1,a2c2) ),
inference(global_subsumption_just,[status(thm)],[c_18816,c_70,c_68,c_67,c_7126,c_12151,c_16345,c_18896]) ).
tcf(c_19099,plain,
( incident(b1,a2c2)
| incident(a1,a2b2) ),
inference(renaming,[status(thm)],[c_19098]) ).
tcf(c_19139,plain,
( incident(b1,a2b2)
| ~ incident(b1,ob)
| ~ line_equal(ob,a2b2) ),
inference(instantiation,[status(thm)],[c_2472]) ).
tcf(c_19151,plain,
( point_equal(a2,ab)
| line_equal(a2b2,oa) ),
inference(global_subsumption_just,[status(thm)],[c_18155,c_99,c_81,c_80,c_75,c_74,c_73,c_72,c_70,c_69,c_68,c_67,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_89,c_86,c_84,c_54,c_52,c_50,c_533,c_551,c_694,c_1038,c_1088,c_1092,c_1414,c_3579,c_3684,c_3689,c_3943,c_4926,c_5253,c_5658,c_5720,c_5861,c_6638,c_7160,c_7885,c_8580,c_8845,c_9731,c_10002,c_11569,c_12150,c_15329,c_15717,c_15842,c_18896,c_19088,c_19099]) ).
tcf(c_19154,plain,
( point_equal(ab,a2)
| line_equal(a2b2,oa) ),
inference(superposition,[status(thm)],[c_19151,c_472]) ).
tcf(c_19158,plain,
( incident(a2,a1b1)
| line_equal(a2b2,oa) ),
inference(superposition,[status(thm)],[c_19151,c_8183]) ).
tcf(c_19194,plain,
! [X0_iProver_incident_1: iProver_incident_1] :
( incident(X0_iProver_incident_1,ob)
| ~ line_equal(oa,ob)
| ~ incident(X0_iProver_incident_1,oa) ),
inference(instantiation,[status(thm)],[c_5151]) ).
tcf(c_19197,plain,
( incident(a1,ob)
| ~ incident(a1,oa)
| ~ line_equal(oa,ob) ),
inference(instantiation,[status(thm)],[c_19194]) ).
tcf(c_19208,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_19197,c_19154,c_19158,c_19139,c_18600,c_16107,c_15875,c_15531,c_15457,c_13188,c_13056,c_12151,c_11447,c_11448,c_10181,c_8804,c_8395,c_8354,c_7911,c_7629,c_7183,c_6834,c_6838,c_6784,c_6586,c_5886,c_5840,c_5299,c_4930,c_4656,c_4584,c_3865,c_3831,c_3757,c_1107,c_1091,c_1069,c_1038,c_1021,c_986,c_985,c_694,c_672,c_551,c_550,c_545,c_544,c_538,c_524,c_507,c_84,c_87,c_89,c_55,c_56,c_58,c_59,c_60,c_61,c_62,c_63,c_64,c_67,c_68,c_69,c_70,c_71,c_72,c_73,c_74,c_75,c_76,c_77,c_78,c_79,c_80,c_81,c_99]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.19/5.47 % Computer : n026.cluster.edu
% 0.19/5.47 % Model : x86_64 x86_64
% 0.19/5.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.47 % Memory : 8046.5625MB
% 0.19/5.47 % OS : Linux 6.8.0-71-generic
% 0.19/5.47 % CPULimit : 300
% 0.19/5.47 % WCLimit : 300
% 0.19/5.47 % DateTime : Wed Sep 23 11:17:46 UTC 2026
% 0.19/5.47 % CPUTime :
% 0.19/5.47 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.24/5.53 Running first-order theorem proving
% 0.24/5.53 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.24/5.55
% 0.24/5.55 % ======== iProver multi-core TPTP/SMT =========
% 0.24/5.55
% 0.24/5.55 % Detected problem language: tptp
% 0.24/5.57 % Proving...
% 6.75/7.02 % SZS status Started for theBenchmark.p
% 6.75/7.02 % SZS status Theorem for theBenchmark.p
% 6.75/7.02
% 6.75/7.02 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.75/7.02
% 6.75/7.02 % ------ iProver source info
% 6.75/7.02
% 6.75/7.02 % git: date: 2026-07-19 20:42:38 +0200
% 6.75/7.02 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.75/7.02 % git: non_committed_changes: false
% 6.75/7.02
% 6.75/7.02 % ------ Parsing...
% 6.75/7.02 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.75/7.02
% 6.75/7.02 % ------ Preprocessing... sf_s rm: 1 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.75/7.02
% 6.75/7.02 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 6.75/7.02 % ------ Proving...
% 6.75/7.02 % ------ Problem Properties
% 6.75/7.02
% 6.75/7.02 %
% 6.75/7.02 % clauses 50
% 6.75/7.02 % conjectures 0
% 6.75/7.02 % EPR 50
% 6.75/7.02 % Horn 46
% 6.75/7.02 % unary 33
% 6.75/7.02 % binary 7
% 6.75/7.02 % lits 80
% 6.75/7.02 % lits eq 0
% 6.75/7.02 % fd_pure 0
% 6.75/7.02 % fd_pseudo 0
% 6.75/7.02 % fd_cond 0
% 6.75/7.02 % fd_pseudo_cond 0
% 6.75/7.02 % AC symbols 0
% 6.75/7.02
% 6.75/7.02 % ------ Input Options Time Limit: Unbounded
% 6.75/7.02
% 6.75/7.02
% 6.75/7.02 % ------
% 6.75/7.02 % Current options:
% 6.75/7.02 % ------
% 6.75/7.02
% 6.75/7.02
% 6.75/7.02 %
% 6.75/7.02
% 6.75/7.02 % ------ Proving...
% 6.75/7.02 %
% 6.75/7.02
% 6.75/7.02 % SZS status Theorem for theBenchmark.p
% 6.75/7.02
% 6.75/7.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.58/7.04
% 8.58/7.04
%------------------------------------------------------------------------------