%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 12:24:14 PM UTC 2026
% Result : Theorem 15.11s 2.77s
% Output : CNFRefutation 15.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 337
% Syntax : Number of formulae : 1536 ( 82 unt; 289 def)
% Number of atoms : 4175 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 4635 (1996 ~;2317 |; 16 &)
% ( 289 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 294 ( 293 usr; 291 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 487 ( 487 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] :
( ( incident(ab,A)
& incident(ac,A)
& incident(bc,A)
& line_equal(A,A) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( ( incident(c1,a2b2)
& incident(b1,a2c2)
& incident(a1,b2c2) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( ( incident(c2,a1b1)
& incident(b2,a1c1)
& incident(a2,b1c1) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
incident(a1,a1b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
incident(b1,a1b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
incident(a2,a2b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
incident(b2,a2b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
incident(a1,a1c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
incident(c1,a1c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
incident(a2,a2c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
incident(c2,a2c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
incident(c1,b1c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
incident(b1,b1c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
incident(c2,b2c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
incident(b2,b2c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
incident(o,oa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
incident(o,ob),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
incident(o,oc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
incident(a1,oa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
incident(a2,oa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
incident(b1,ob),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
incident(b2,ob),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
incident(c1,oc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
incident(c2,oc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
incident(bc,b1c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
incident(bc,b2c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
incident(ac,a1c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
incident(ac,a2c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
incident(ab,a1b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
incident(ab,a2b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A] :
( ( incident(c1,A)
& incident(b1,A)
& incident(a1,A) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( ( incident(c2,A)
& incident(b2,A)
& incident(a2,A) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
( point_equal(a2,a1)
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
( point_equal(b2,b1)
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
( point_equal(c2,c1)
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
( line_equal(b1c1,b2c2)
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
( line_equal(a1c1,a2c2)
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
( line_equal(a1b1,a2b2)
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [A,B] :
( point_equal(A,B)
=> point_equal(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,B] :
( incident(A,B)
=> line_equal(B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A,B] :
( line_equal(A,B)
=> line_equal(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A,B,C] :
( ( incident(B,C)
& point_equal(A,B) )
=> incident(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A,B,C] :
( ( line_equal(B,C)
& incident(A,B) )
=> incident(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A,B,C,D] :
( ( incident(B,D)
& incident(B,C)
& incident(A,D)
& incident(A,C) )
=> ( line_equal(C,D)
| point_equal(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,conjecture,
goal,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f53,plain,
! [A] :
( goal
| ~ incident(ab,A)
| ~ incident(ac,A)
| ~ incident(bc,A)
| ~ line_equal(A,A) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f54,plain,
( goal
| ! [A] :
( ~ incident(ab,A)
| ~ incident(ac,A)
| ~ incident(bc,A)
| ~ line_equal(A,A) ) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f55,plain,
! [X0] :
( goal
| ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
( goal
| ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f57,plain,
( goal
| ~ incident(c1,a2b2)
| ~ incident(b1,a2c2)
| ~ incident(a1,b2c2) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
( goal
| ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f59,plain,
( goal
| ~ incident(c2,a1b1)
| ~ incident(b2,a1c1)
| ~ incident(a2,b1c1) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
( incident(b2,a1c1)
| incident(a1,b2c2) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f61,plain,
( incident(c2,a1b1)
| incident(b1,a2c2) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f62,plain,
( incident(a2,b1c1)
| incident(c1,a2b2) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f63,plain,
incident(a1,a1b1),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f64,plain,
incident(b1,a1b1),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f65,plain,
incident(a2,a2b2),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f66,plain,
incident(b2,a2b2),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f67,plain,
incident(a1,a1c1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f68,plain,
incident(c1,a1c1),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f69,plain,
incident(a2,a2c2),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f70,plain,
incident(c2,a2c2),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f71,plain,
incident(c1,b1c1),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f72,plain,
incident(b1,b1c1),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f73,plain,
incident(c2,b2c2),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f74,plain,
incident(b2,b2c2),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f75,plain,
incident(o,oa),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f76,plain,
incident(o,ob),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f77,plain,
incident(o,oc),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f78,plain,
incident(a1,oa),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f79,plain,
incident(a2,oa),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f80,plain,
incident(b1,ob),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f81,plain,
incident(b2,ob),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f82,plain,
incident(c1,oc),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f83,plain,
incident(c2,oc),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f84,plain,
incident(bc,b1c1),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f85,plain,
incident(bc,b2c2),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f86,plain,
incident(ac,a1c1),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f87,plain,
incident(ac,a2c2),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f88,plain,
incident(ab,a1b1),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f89,plain,
incident(ab,a2b2),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f90,plain,
! [A] :
( goal
| ~ incident(c1,A)
| ~ incident(b1,A)
| ~ incident(a1,A) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f91,plain,
( goal
| ! [A] :
( ~ incident(c1,A)
| ~ incident(b1,A)
| ~ incident(a1,A) ) ),
inference(miniscoping,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0] :
( goal
| ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [A] :
( goal
| ~ incident(c2,A)
| ~ incident(b2,A)
| ~ incident(a2,A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f94,plain,
( goal
| ! [A] :
( ~ incident(c2,A)
| ~ incident(b2,A)
| ~ incident(a2,A) ) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f95,plain,
! [X0] :
( goal
| ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
( goal
| ~ point_equal(a2,a1) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f97,plain,
( goal
| ~ point_equal(a2,a1) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f98,plain,
( goal
| ~ point_equal(b2,b1) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f99,plain,
( goal
| ~ point_equal(b2,b1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
( goal
| ~ point_equal(c2,c1) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f101,plain,
( goal
| ~ point_equal(c2,c1) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
( goal
| ~ line_equal(b1c1,b2c2) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f103,plain,
( goal
| ~ line_equal(b1c1,b2c2) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
( goal
| ~ line_equal(a1c1,a2c2) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f105,plain,
( goal
| ~ line_equal(a1c1,a2c2) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
( goal
| ~ line_equal(a1b1,a2b2) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f107,plain,
( goal
| ~ line_equal(a1b1,a2b2) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f111,plain,
! [A,B] :
( point_equal(B,A)
| ~ point_equal(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f112,plain,
! [X0,X1] :
( point_equal(X1,X0)
| ~ point_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f116,plain,
! [A,B] :
( line_equal(B,B)
| ~ incident(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f117,plain,
! [B] :
( line_equal(B,B)
| ! [A] : ~ incident(A,B) ),
inference(miniscoping,[status(thm)],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( line_equal(X1,X1)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [A,B] :
( line_equal(B,A)
| ~ line_equal(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f120,plain,
! [X0,X1] :
( line_equal(X1,X0)
| ~ line_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f124,plain,
! [A,B,C] :
( incident(A,C)
| ~ incident(B,C)
| ~ point_equal(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f125,plain,
! [A,C] :
( incident(A,C)
| ! [B] :
( ~ incident(B,C)
| ~ point_equal(A,B) ) ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ incident(X1,X2)
| ~ point_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [A,B,C] :
( incident(A,C)
| ~ line_equal(B,C)
| ~ incident(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f128,plain,
! [A,C] :
( incident(A,C)
| ! [B] :
( ~ line_equal(B,C)
| ~ incident(A,B) ) ),
inference(miniscoping,[status(thm)],[f127]) ).
fof(f129,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ line_equal(X1,X2)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [A,B,C,D] :
( line_equal(C,D)
| point_equal(A,B)
| ~ incident(B,D)
| ~ incident(B,C)
| ~ incident(A,D)
| ~ incident(A,C) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f131,plain,
! [X0,X1,X2,X3] :
( line_equal(X1,X2)
| point_equal(X0,X3)
| ~ incident(X3,X2)
| ~ incident(X3,X1)
| ~ incident(X0,X2)
| ~ incident(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
~ goal,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f133,definition,
! [X0] :
( sQ0_spl
<=> ( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f134,plain,
! [X0] :
( ~ sQ0_spl
| ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0)
| ~ line_equal(X0,X0) ),
inference(component_clause,[status(thm)],[f133]) ).
fof(f136,definition,
( sQ1_spl
<=> goal ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f137,plain,
( ~ sQ1_spl
| goal ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f139,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f55,f133,f136]) ).
fof(f140,definition,
( sQ2_spl
<=> incident(a1,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f141,plain,
( ~ sQ2_spl
| incident(a1,b2c2) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f143,definition,
( sQ3_spl
<=> incident(b1,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f144,plain,
( ~ sQ3_spl
| incident(b1,a2c2) ),
inference(component_clause,[status(thm)],[f143]) ).
fof(f146,definition,
( sQ4_spl
<=> incident(c1,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f147,plain,
( ~ sQ4_spl
| incident(c1,a2b2) ),
inference(component_clause,[status(thm)],[f146]) ).
fof(f149,plain,
( sQ1_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f57,f140,f143,f146,f136]) ).
fof(f150,definition,
( sQ5_spl
<=> incident(a2,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( ~ sQ5_spl
| incident(a2,b1c1) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f153,definition,
( sQ6_spl
<=> incident(b2,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( ~ sQ6_spl
| incident(b2,a1c1) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f156,definition,
( sQ7_spl
<=> incident(c2,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( ~ sQ7_spl
| incident(c2,a1b1) ),
inference(component_clause,[status(thm)],[f156]) ).
fof(f159,plain,
( sQ1_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f59,f150,f153,f156,f136]) ).
fof(f160,plain,
( sQ6_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f60,f140,f153]) ).
fof(f161,plain,
( sQ7_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f61,f143,f156]) ).
fof(f162,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f62,f146,f150]) ).
fof(f163,definition,
! [X0] :
( sQ8_spl
<=> ( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f164,plain,
! [X0] :
( ~ sQ8_spl
| ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(component_clause,[status(thm)],[f163]) ).
fof(f166,plain,
( sQ1_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f92,f163,f136]) ).
fof(f167,definition,
! [X0] :
( sQ9_spl
<=> ( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f168,plain,
! [X0] :
( ~ sQ9_spl
| ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(component_clause,[status(thm)],[f167]) ).
fof(f170,plain,
( sQ1_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f95,f167,f136]) ).
fof(f171,definition,
( sQ10_spl
<=> point_equal(a2,a1) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( sQ1_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f97,f171,f136]) ).
fof(f175,definition,
( sQ11_spl
<=> point_equal(b2,b1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f177,plain,
( sQ11_spl
| ~ point_equal(b2,b1) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,plain,
( sQ1_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f99,f175,f136]) ).
fof(f179,definition,
( sQ12_spl
<=> point_equal(c2,c1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( sQ1_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f101,f179,f136]) ).
fof(f183,definition,
( sQ13_spl
<=> line_equal(b1c1,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( sQ13_spl
| ~ line_equal(b1c1,b2c2) ),
inference(component_clause,[status(thm)],[f183]) ).
fof(f186,plain,
( sQ1_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f103,f183,f136]) ).
fof(f187,definition,
( sQ14_spl
<=> line_equal(a1c1,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f190,plain,
( sQ1_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f105,f187,f136]) ).
fof(f191,definition,
( sQ15_spl
<=> line_equal(a1b1,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( sQ15_spl
| ~ line_equal(a1b1,a2b2) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,plain,
( sQ1_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f107,f191,f136]) ).
fof(f195,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f137,f132]) ).
fof(f196,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f195]) ).
fof(f255,plain,
! [X0] :
( incident(X0,a2b2)
| ~ point_equal(X0,ab) ),
inference(resolution,[status(thm)],[f126,f89]) ).
fof(f258,plain,
! [X0] :
( incident(X0,a1c1)
| ~ point_equal(X0,ac) ),
inference(resolution,[status(thm)],[f126,f86]) ).
fof(f260,plain,
! [X0] :
( incident(X0,b1c1)
| ~ point_equal(X0,bc) ),
inference(resolution,[status(thm)],[f126,f84]) ).
fof(f261,plain,
! [X0] :
( incident(X0,oc)
| ~ point_equal(X0,o) ),
inference(resolution,[status(thm)],[f126,f77]) ).
fof(f262,plain,
! [X0] :
( incident(X0,ob)
| ~ point_equal(X0,o) ),
inference(resolution,[status(thm)],[f126,f76]) ).
fof(f263,plain,
! [X0] :
( incident(X0,oa)
| ~ point_equal(X0,o) ),
inference(resolution,[status(thm)],[f126,f75]) ).
fof(f264,plain,
! [X0] :
( incident(X0,oc)
| ~ point_equal(X0,c2) ),
inference(resolution,[status(thm)],[f126,f83]) ).
fof(f265,plain,
! [X0] :
( incident(X0,b2c2)
| ~ point_equal(X0,c2) ),
inference(resolution,[status(thm)],[f126,f73]) ).
fof(f266,plain,
! [X0] :
( incident(X0,a2c2)
| ~ point_equal(X0,c2) ),
inference(resolution,[status(thm)],[f126,f70]) ).
fof(f267,plain,
! [X0] :
( ~ sQ4_spl
| incident(X0,a2b2)
| ~ point_equal(X0,c1) ),
inference(resolution,[status(thm)],[f126,f147]) ).
fof(f268,plain,
! [X0] :
( incident(X0,oc)
| ~ point_equal(X0,c1) ),
inference(resolution,[status(thm)],[f126,f82]) ).
fof(f269,plain,
! [X0] :
( incident(X0,b1c1)
| ~ point_equal(X0,c1) ),
inference(resolution,[status(thm)],[f126,f71]) ).
fof(f270,plain,
! [X0] :
( incident(X0,a1c1)
| ~ point_equal(X0,c1) ),
inference(resolution,[status(thm)],[f126,f68]) ).
fof(f271,plain,
! [X0] :
( incident(X0,ob)
| ~ point_equal(X0,b2) ),
inference(resolution,[status(thm)],[f126,f81]) ).
fof(f272,plain,
! [X0] :
( incident(X0,b2c2)
| ~ point_equal(X0,b2) ),
inference(resolution,[status(thm)],[f126,f74]) ).
fof(f273,plain,
! [X0] :
( incident(X0,a2b2)
| ~ point_equal(X0,b2) ),
inference(resolution,[status(thm)],[f126,f66]) ).
fof(f276,plain,
! [X0] :
( incident(X0,a2b2)
| ~ point_equal(X0,a2) ),
inference(resolution,[status(thm)],[f126,f65]) ).
fof(f279,plain,
! [X0] :
( incident(X0,b1c1)
| ~ point_equal(X0,b1) ),
inference(resolution,[status(thm)],[f126,f72]) ).
fof(f280,plain,
! [X0] :
( incident(X0,a1b1)
| ~ point_equal(X0,b1) ),
inference(resolution,[status(thm)],[f126,f64]) ).
fof(f282,plain,
! [X0] :
( incident(X0,a1c1)
| ~ point_equal(X0,a1) ),
inference(resolution,[status(thm)],[f126,f67]) ).
fof(f283,plain,
! [X0] :
( incident(X0,a1b1)
| ~ point_equal(X0,a1) ),
inference(resolution,[status(thm)],[f126,f63]) ).
fof(f287,plain,
! [X0] :
( incident(ac,X0)
| ~ line_equal(a1c1,X0) ),
inference(resolution,[status(thm)],[f129,f86]) ).
fof(f289,plain,
! [X0] :
( incident(bc,X0)
| ~ line_equal(b1c1,X0) ),
inference(resolution,[status(thm)],[f129,f84]) ).
fof(f290,plain,
! [X0] :
( incident(o,X0)
| ~ line_equal(oc,X0) ),
inference(resolution,[status(thm)],[f129,f77]) ).
fof(f291,plain,
! [X0] :
( incident(o,X0)
| ~ line_equal(ob,X0) ),
inference(resolution,[status(thm)],[f129,f76]) ).
fof(f293,plain,
! [X0] :
( incident(c2,X0)
| ~ line_equal(oc,X0) ),
inference(resolution,[status(thm)],[f129,f83]) ).
fof(f294,plain,
! [X0] :
( incident(c2,X0)
| ~ line_equal(b2c2,X0) ),
inference(resolution,[status(thm)],[f129,f73]) ).
fof(f295,plain,
! [X0] :
( incident(c2,X0)
| ~ line_equal(a2c2,X0) ),
inference(resolution,[status(thm)],[f129,f70]) ).
fof(f297,plain,
! [X0] :
( incident(c1,X0)
| ~ line_equal(oc,X0) ),
inference(resolution,[status(thm)],[f129,f82]) ).
fof(f298,plain,
! [X0] :
( incident(c1,X0)
| ~ line_equal(b1c1,X0) ),
inference(resolution,[status(thm)],[f129,f71]) ).
fof(f299,plain,
! [X0] :
( incident(c1,X0)
| ~ line_equal(a1c1,X0) ),
inference(resolution,[status(thm)],[f129,f68]) ).
fof(f300,plain,
! [X0] :
( incident(b2,X0)
| ~ line_equal(ob,X0) ),
inference(resolution,[status(thm)],[f129,f81]) ).
fof(f301,plain,
! [X0] :
( incident(b2,X0)
| ~ line_equal(b2c2,X0) ),
inference(resolution,[status(thm)],[f129,f74]) ).
fof(f302,plain,
! [X0] :
( incident(b2,X0)
| ~ line_equal(a2b2,X0) ),
inference(resolution,[status(thm)],[f129,f66]) ).
fof(f303,plain,
! [X0] :
( incident(a2,X0)
| ~ line_equal(oa,X0) ),
inference(resolution,[status(thm)],[f129,f79]) ).
fof(f304,plain,
! [X0] :
( incident(a2,X0)
| ~ line_equal(a2c2,X0) ),
inference(resolution,[status(thm)],[f129,f69]) ).
fof(f305,plain,
! [X0] :
( incident(a2,X0)
| ~ line_equal(a2b2,X0) ),
inference(resolution,[status(thm)],[f129,f65]) ).
fof(f307,plain,
! [X0] :
( incident(b1,X0)
| ~ line_equal(ob,X0) ),
inference(resolution,[status(thm)],[f129,f80]) ).
fof(f308,plain,
! [X0] :
( incident(b1,X0)
| ~ line_equal(b1c1,X0) ),
inference(resolution,[status(thm)],[f129,f72]) ).
fof(f309,plain,
! [X0] :
( incident(b1,X0)
| ~ line_equal(a1b1,X0) ),
inference(resolution,[status(thm)],[f129,f64]) ).
fof(f310,plain,
! [X0] :
( incident(a1,X0)
| ~ line_equal(oa,X0) ),
inference(resolution,[status(thm)],[f129,f78]) ).
fof(f311,plain,
! [X0] :
( incident(a1,X0)
| ~ line_equal(a1c1,X0) ),
inference(resolution,[status(thm)],[f129,f67]) ).
fof(f312,plain,
! [X0] :
( incident(a1,X0)
| ~ line_equal(a1b1,X0) ),
inference(resolution,[status(thm)],[f129,f63]) ).
fof(f314,plain,
! [X0,X1] :
( line_equal(X0,a2b2)
| point_equal(ab,X1)
| ~ incident(X1,a2b2)
| ~ incident(X1,X0)
| ~ incident(ab,X0) ),
inference(resolution,[status(thm)],[f131,f89]) ).
fof(f318,plain,
! [X0,X1] :
( line_equal(X0,a2c2)
| point_equal(ac,X1)
| ~ incident(X1,a2c2)
| ~ incident(X1,X0)
| ~ incident(ac,X0) ),
inference(resolution,[status(thm)],[f131,f87]) ).
fof(f322,plain,
! [X0,X1] :
( line_equal(X0,b2c2)
| point_equal(bc,X1)
| ~ incident(X1,b2c2)
| ~ incident(X1,X0)
| ~ incident(bc,X0) ),
inference(resolution,[status(thm)],[f131,f85]) ).
fof(f324,plain,
! [X0,X1] :
( line_equal(X0,b1c1)
| point_equal(bc,X1)
| ~ incident(X1,b1c1)
| ~ incident(X1,X0)
| ~ incident(bc,X0) ),
inference(resolution,[status(thm)],[f131,f84]) ).
fof(f326,plain,
! [X0,X1] :
( line_equal(X0,oc)
| point_equal(o,X1)
| ~ incident(X1,oc)
| ~ incident(X1,X0)
| ~ incident(o,X0) ),
inference(resolution,[status(thm)],[f131,f77]) ).
fof(f328,plain,
! [X0,X1] :
( line_equal(X0,ob)
| point_equal(o,X1)
| ~ incident(X1,ob)
| ~ incident(X1,X0)
| ~ incident(o,X0) ),
inference(resolution,[status(thm)],[f131,f76]) ).
fof(f332,plain,
! [X0,X1] :
( line_equal(X0,oc)
| point_equal(c2,X1)
| ~ incident(X1,oc)
| ~ incident(X1,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f131,f83]) ).
fof(f334,plain,
! [X0,X1] :
( line_equal(X0,b2c2)
| point_equal(c2,X1)
| ~ incident(X1,b2c2)
| ~ incident(X1,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f131,f73]) ).
fof(f336,plain,
! [X0,X1] :
( line_equal(X0,a2c2)
| point_equal(c2,X1)
| ~ incident(X1,a2c2)
| ~ incident(X1,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f131,f70]) ).
fof(f338,plain,
! [X0,X1] :
( ~ sQ4_spl
| line_equal(X0,a2b2)
| point_equal(c1,X1)
| ~ incident(X1,a2b2)
| ~ incident(X1,X0)
| ~ incident(c1,X0) ),
inference(resolution,[status(thm)],[f131,f147]) ).
fof(f340,plain,
! [X0,X1] :
( line_equal(X0,oc)
| point_equal(c1,X1)
| ~ incident(X1,oc)
| ~ incident(X1,X0)
| ~ incident(c1,X0) ),
inference(resolution,[status(thm)],[f131,f82]) ).
fof(f342,plain,
! [X0,X1] :
( line_equal(X0,b1c1)
| point_equal(c1,X1)
| ~ incident(X1,b1c1)
| ~ incident(X1,X0)
| ~ incident(c1,X0) ),
inference(resolution,[status(thm)],[f131,f71]) ).
fof(f344,plain,
! [X0,X1] :
( line_equal(X0,a1c1)
| point_equal(c1,X1)
| ~ incident(X1,a1c1)
| ~ incident(X1,X0)
| ~ incident(c1,X0) ),
inference(resolution,[status(thm)],[f131,f68]) ).
fof(f346,plain,
! [X0,X1] :
( line_equal(X0,ob)
| point_equal(b2,X1)
| ~ incident(X1,ob)
| ~ incident(X1,X0)
| ~ incident(b2,X0) ),
inference(resolution,[status(thm)],[f131,f81]) ).
fof(f348,plain,
! [X0,X1] :
( line_equal(X0,b2c2)
| point_equal(b2,X1)
| ~ incident(X1,b2c2)
| ~ incident(X1,X0)
| ~ incident(b2,X0) ),
inference(resolution,[status(thm)],[f131,f74]) ).
fof(f350,plain,
! [X0,X1] :
( line_equal(X0,a2b2)
| point_equal(b2,X1)
| ~ incident(X1,a2b2)
| ~ incident(X1,X0)
| ~ incident(b2,X0) ),
inference(resolution,[status(thm)],[f131,f66]) ).
fof(f354,plain,
! [X0,X1] :
( line_equal(X0,a2c2)
| point_equal(a2,X1)
| ~ incident(X1,a2c2)
| ~ incident(X1,X0)
| ~ incident(a2,X0) ),
inference(resolution,[status(thm)],[f131,f69]) ).
fof(f360,plain,
! [X0,X1] :
( line_equal(X0,ob)
| point_equal(b1,X1)
| ~ incident(X1,ob)
| ~ incident(X1,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f131,f80]) ).
fof(f362,plain,
! [X0,X1] :
( line_equal(X0,b1c1)
| point_equal(b1,X1)
| ~ incident(X1,b1c1)
| ~ incident(X1,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f131,f72]) ).
fof(f364,plain,
! [X0,X1] :
( line_equal(X0,a1b1)
| point_equal(b1,X1)
| ~ incident(X1,a1b1)
| ~ incident(X1,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f131,f64]) ).
fof(f368,plain,
! [X0,X1] :
( line_equal(X0,a1c1)
| point_equal(a1,X1)
| ~ incident(X1,a1c1)
| ~ incident(X1,X0)
| ~ incident(a1,X0) ),
inference(resolution,[status(thm)],[f131,f67]) ).
fof(f370,plain,
! [X0,X1] :
( line_equal(X0,a1b1)
| point_equal(a1,X1)
| ~ incident(X1,a1b1)
| ~ incident(X1,X0)
| ~ incident(a1,X0) ),
inference(resolution,[status(thm)],[f131,f63]) ).
fof(f374,plain,
! [X0,X1] :
( line_equal(a1b1,X1)
| point_equal(X0,ab)
| ~ incident(ab,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f131,f88]) ).
fof(f378,plain,
! [X0,X1] :
( line_equal(a1c1,X1)
| point_equal(X0,ac)
| ~ incident(ac,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f131,f86]) ).
fof(f382,plain,
! [X0,X1] :
( line_equal(b1c1,X1)
| point_equal(X0,bc)
| ~ incident(bc,X1)
| ~ incident(X0,X1)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f131,f84]) ).
fof(f384,plain,
! [X0,X1] :
( line_equal(oc,X1)
| point_equal(X0,o)
| ~ incident(o,X1)
| ~ incident(X0,X1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f131,f77]) ).
fof(f388,plain,
! [X0,X1] :
( line_equal(oa,X1)
| point_equal(X0,o)
| ~ incident(o,X1)
| ~ incident(X0,X1)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f131,f75]) ).
fof(f390,plain,
! [X0,X1] :
( line_equal(oc,X1)
| point_equal(X0,c2)
| ~ incident(c2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f131,f83]) ).
fof(f392,plain,
! [X0,X1] :
( line_equal(b2c2,X1)
| point_equal(X0,c2)
| ~ incident(c2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f131,f73]) ).
fof(f394,plain,
! [X0,X1] :
( line_equal(a2c2,X1)
| point_equal(X0,c2)
| ~ incident(c2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f131,f70]) ).
fof(f396,plain,
! [X0,X1] :
( ~ sQ4_spl
| line_equal(a2b2,X1)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f131,f147]) ).
fof(f398,plain,
! [X0,X1] :
( line_equal(oc,X1)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f131,f82]) ).
fof(f400,plain,
! [X0,X1] :
( line_equal(b1c1,X1)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f131,f71]) ).
fof(f402,plain,
! [X0,X1] :
( line_equal(a1c1,X1)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f131,f68]) ).
fof(f404,plain,
! [X0,X1] :
( line_equal(ob,X1)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f131,f81]) ).
fof(f406,plain,
! [X0,X1] :
( line_equal(b2c2,X1)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f131,f74]) ).
fof(f408,plain,
! [X0,X1] :
( line_equal(a2b2,X1)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f131,f66]) ).
fof(f410,plain,
! [X0,X1] :
( line_equal(oa,X1)
| point_equal(X0,a2)
| ~ incident(a2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f131,f79]) ).
fof(f412,plain,
! [X0,X1] :
( line_equal(a2c2,X1)
| point_equal(X0,a2)
| ~ incident(a2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f131,f69]) ).
fof(f414,plain,
! [X0,X1] :
( line_equal(a2b2,X1)
| point_equal(X0,a2)
| ~ incident(a2,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f131,f65]) ).
fof(f418,plain,
! [X0,X1] :
( line_equal(ob,X1)
| point_equal(X0,b1)
| ~ incident(b1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f131,f80]) ).
fof(f422,plain,
! [X0,X1] :
( line_equal(a1b1,X1)
| point_equal(X0,b1)
| ~ incident(b1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f131,f64]) ).
fof(f428,plain,
! [X0,X1] :
( line_equal(a1b1,X1)
| point_equal(X0,a1)
| ~ incident(a1,X1)
| ~ incident(X0,X1)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f131,f63]) ).
fof(f431,plain,
! [X0,X1] :
( line_equal(X1,a2c2)
| point_equal(X0,ac)
| ~ incident(ac,X1)
| ~ incident(X0,a2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f87]) ).
fof(f433,plain,
! [X0,X1] :
( line_equal(X1,b2c2)
| point_equal(X0,bc)
| ~ incident(bc,X1)
| ~ incident(X0,b2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f85]) ).
fof(f434,plain,
! [X0,X1] :
( line_equal(X1,b1c1)
| point_equal(X0,bc)
| ~ incident(bc,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f84]) ).
fof(f435,plain,
! [X0,X1] :
( line_equal(X1,oc)
| point_equal(X0,o)
| ~ incident(o,X1)
| ~ incident(X0,oc)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f77]) ).
fof(f436,plain,
! [X0,X1] :
( line_equal(X1,ob)
| point_equal(X0,o)
| ~ incident(o,X1)
| ~ incident(X0,ob)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f76]) ).
fof(f437,plain,
! [X0,X1] :
( line_equal(X1,oa)
| point_equal(X0,o)
| ~ incident(o,X1)
| ~ incident(X0,oa)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f75]) ).
fof(f439,plain,
! [X0,X1] :
( line_equal(X1,b2c2)
| point_equal(X0,c2)
| ~ incident(c2,X1)
| ~ incident(X0,b2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f73]) ).
fof(f440,plain,
! [X0,X1] :
( line_equal(X1,a2c2)
| point_equal(X0,c2)
| ~ incident(c2,X1)
| ~ incident(X0,a2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f70]) ).
fof(f441,plain,
! [X0,X1] :
( ~ sQ4_spl
| line_equal(X1,a2b2)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,a2b2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f147]) ).
fof(f442,plain,
! [X0,X1] :
( line_equal(X1,oc)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,oc)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f82]) ).
fof(f443,plain,
! [X0,X1] :
( line_equal(X1,b1c1)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f71]) ).
fof(f444,plain,
! [X0,X1] :
( line_equal(X1,a1c1)
| point_equal(X0,c1)
| ~ incident(c1,X1)
| ~ incident(X0,a1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f68]) ).
fof(f445,plain,
! [X0,X1] :
( line_equal(X1,ob)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,ob)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f81]) ).
fof(f446,plain,
! [X0,X1] :
( line_equal(X1,b2c2)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,b2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f74]) ).
fof(f447,plain,
! [X0,X1] :
( line_equal(X1,a2b2)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,a2b2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f66]) ).
fof(f449,plain,
! [X0,X1] :
( line_equal(X1,a2c2)
| point_equal(X0,a2)
| ~ incident(a2,X1)
| ~ incident(X0,a2c2)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f69]) ).
fof(f452,plain,
! [X0,X1] :
( line_equal(X1,ob)
| point_equal(X0,b1)
| ~ incident(b1,X1)
| ~ incident(X0,ob)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f80]) ).
fof(f453,plain,
! [X0,X1] :
( line_equal(X1,b1c1)
| point_equal(X0,b1)
| ~ incident(b1,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f72]) ).
fof(f454,plain,
! [X0,X1] :
( line_equal(X1,a1b1)
| point_equal(X0,b1)
| ~ incident(b1,X1)
| ~ incident(X0,a1b1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f64]) ).
fof(f455,plain,
! [X0,X1] :
( line_equal(X1,oa)
| point_equal(X0,a1)
| ~ incident(a1,X1)
| ~ incident(X0,oa)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f131,f78]) ).
fof(f458,definition,
( sQ16_spl
<=> incident(ab,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ16_spl
| ~ incident(ab,a2b2) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,definition,
( sQ17_spl
<=> point_equal(ab,ab) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f464,definition,
( sQ18_spl
<=> line_equal(a2b2,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f468,definition,
( sQ19_spl
<=> incident(ab,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( sQ19_spl
| ~ incident(ab,a1b1) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,definition,
( sQ20_spl
<=> line_equal(a1b1,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f475,definition,
( sQ21_spl
<=> incident(ac,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( sQ21_spl
| ~ incident(ac,a2c2) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ22_spl
<=> point_equal(ac,ac) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f481,definition,
( sQ23_spl
<=> line_equal(a2c2,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f488,definition,
( sQ25_spl
<=> line_equal(a1c1,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f492,definition,
( sQ26_spl
<=> incident(bc,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ26_spl
| ~ incident(bc,b2c2) ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f495,definition,
( sQ27_spl
<=> point_equal(bc,bc) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f498,definition,
( sQ28_spl
<=> line_equal(b2c2,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f502,definition,
( sQ29_spl
<=> incident(bc,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ29_spl
| ~ incident(bc,b1c1) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f505,definition,
( sQ30_spl
<=> line_equal(b1c1,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f512,definition,
( sQ32_spl
<=> point_equal(o,o) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f515,definition,
( sQ33_spl
<=> line_equal(oc,oc) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f519,definition,
( sQ34_spl
<=> incident(o,ob) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f521,plain,
( sQ34_spl
| ~ incident(o,ob) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f522,definition,
( sQ35_spl
<=> line_equal(ob,ob) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f526,definition,
( sQ36_spl
<=> incident(o,oa) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f528,plain,
( sQ36_spl
| ~ incident(o,oa) ),
inference(component_clause,[status(thm)],[f526]) ).
fof(f529,definition,
( sQ37_spl
<=> line_equal(oa,oa) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f533,definition,
( sQ38_spl
<=> incident(c2,oc) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f535,plain,
( sQ38_spl
| ~ incident(c2,oc) ),
inference(component_clause,[status(thm)],[f533]) ).
fof(f536,definition,
( sQ39_spl
<=> point_equal(c2,c2) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f540,definition,
( sQ40_spl
<=> incident(c2,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ40_spl
| ~ incident(c2,b2c2) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f544,definition,
( sQ41_spl
<=> incident(c2,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( sQ41_spl
| ~ incident(c2,a2c2) ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f548,definition,
( sQ42_spl
<=> point_equal(c1,c1) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f552,definition,
( sQ43_spl
<=> incident(c1,oc) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( sQ43_spl
| ~ incident(c1,oc) ),
inference(component_clause,[status(thm)],[f552]) ).
fof(f556,definition,
( sQ44_spl
<=> incident(c1,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f558,plain,
( sQ44_spl
| ~ incident(c1,b1c1) ),
inference(component_clause,[status(thm)],[f556]) ).
fof(f564,definition,
( sQ46_spl
<=> incident(b2,ob) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( sQ46_spl
| ~ incident(b2,ob) ),
inference(component_clause,[status(thm)],[f564]) ).
fof(f567,definition,
( sQ47_spl
<=> point_equal(b2,b2) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f571,definition,
( sQ48_spl
<=> incident(b2,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( sQ48_spl
| ~ incident(b2,b2c2) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f575,definition,
( sQ49_spl
<=> incident(b2,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( sQ49_spl
| ~ incident(b2,a2b2) ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f579,definition,
( sQ50_spl
<=> incident(a2,oa) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f581,plain,
( sQ50_spl
| ~ incident(a2,oa) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,definition,
( sQ51_spl
<=> point_equal(a2,a2) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f586,definition,
( sQ52_spl
<=> incident(a2,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( sQ52_spl
| ~ incident(a2,a2c2) ),
inference(component_clause,[status(thm)],[f586]) ).
fof(f590,definition,
( sQ53_spl
<=> incident(a2,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f592,plain,
( sQ53_spl
| ~ incident(a2,a2b2) ),
inference(component_clause,[status(thm)],[f590]) ).
fof(f594,definition,
( sQ54_spl
<=> point_equal(b1,b1) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f598,definition,
( sQ55_spl
<=> incident(b1,ob) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( sQ55_spl
| ~ incident(b1,ob) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f602,definition,
( sQ56_spl
<=> incident(b1,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ56_spl
| ~ incident(b1,b1c1) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f610,definition,
( sQ58_spl
<=> incident(a1,oa) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f612,plain,
( sQ58_spl
| ~ incident(a1,oa) ),
inference(component_clause,[status(thm)],[f610]) ).
fof(f613,definition,
( sQ59_spl
<=> point_equal(a1,a1) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f617,definition,
( sQ60_spl
<=> incident(a1,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f619,plain,
( sQ60_spl
| ~ incident(a1,a1c1) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f621,definition,
( sQ61_spl
<=> incident(a1,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ61_spl
| ~ incident(a1,a1b1) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f741,plain,
! [X0] :
( ~ sQ0_spl
| ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f134,f118]) ).
fof(f742,plain,
( ~ sQ0_spl
| ~ incident(ab,a2c2)
| ~ incident(bc,a2c2) ),
inference(resolution,[status(thm)],[f741,f87]) ).
fof(f743,plain,
( ~ sQ0_spl
| ~ incident(ab,a1c1)
| ~ incident(bc,a1c1) ),
inference(resolution,[status(thm)],[f741,f86]) ).
fof(f744,plain,
( ~ sQ0_spl
| ~ incident(ac,a2b2)
| ~ incident(bc,a2b2) ),
inference(resolution,[status(thm)],[f741,f89]) ).
fof(f745,plain,
( ~ sQ0_spl
| ~ incident(ac,a1b1)
| ~ incident(bc,a1b1) ),
inference(resolution,[status(thm)],[f741,f88]) ).
fof(f746,definition,
( sQ91_spl
<=> incident(bc,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( ~ sQ91_spl
| incident(bc,a2c2) ),
inference(component_clause,[status(thm)],[f746]) ).
fof(f748,plain,
( sQ91_spl
| ~ incident(bc,a2c2) ),
inference(component_clause,[status(thm)],[f746]) ).
fof(f749,definition,
( sQ92_spl
<=> incident(ab,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f751,plain,
( sQ92_spl
| ~ incident(ab,a2c2) ),
inference(component_clause,[status(thm)],[f749]) ).
fof(f752,plain,
( ~ sQ0_spl
| ~ sQ92_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f742,f746,f749,f133]) ).
fof(f753,definition,
( sQ93_spl
<=> incident(bc,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f756,definition,
( sQ94_spl
<=> incident(ab,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ94_spl
| ~ incident(ab,a1c1) ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,plain,
( ~ sQ0_spl
| ~ sQ94_spl
| ~ sQ93_spl ),
inference(split_clause,[status(thm)],[f743,f753,f756,f133]) ).
fof(f760,definition,
( sQ95_spl
<=> incident(bc,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( ~ sQ95_spl
| incident(bc,a2b2) ),
inference(component_clause,[status(thm)],[f760]) ).
fof(f763,definition,
( sQ96_spl
<=> incident(ac,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( sQ96_spl
| ~ incident(ac,a2b2) ),
inference(component_clause,[status(thm)],[f763]) ).
fof(f766,plain,
( ~ sQ0_spl
| ~ sQ96_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f744,f760,f763,f133]) ).
fof(f767,definition,
( sQ97_spl
<=> incident(bc,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( sQ97_spl
| ~ incident(bc,a1b1) ),
inference(component_clause,[status(thm)],[f767]) ).
fof(f770,definition,
( sQ98_spl
<=> incident(ac,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f772,plain,
( sQ98_spl
| ~ incident(ac,a1b1) ),
inference(component_clause,[status(thm)],[f770]) ).
fof(f773,plain,
( ~ sQ0_spl
| ~ sQ98_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f745,f767,f770,f133]) ).
fof(f774,plain,
( ~ sQ8_spl
| ~ incident(c1,ob)
| ~ incident(a1,ob) ),
inference(resolution,[status(thm)],[f164,f80]) ).
fof(f775,plain,
( ~ sQ8_spl
| ~ incident(c1,b1c1)
| ~ incident(a1,b1c1) ),
inference(resolution,[status(thm)],[f164,f72]) ).
fof(f776,plain,
( ~ sQ8_spl
| ~ incident(c1,a1b1)
| ~ incident(a1,a1b1) ),
inference(resolution,[status(thm)],[f164,f64]) ).
fof(f777,plain,
( ~ sQ4_spl
| ~ sQ8_spl
| ~ incident(b1,a2b2)
| ~ incident(a1,a2b2) ),
inference(resolution,[status(thm)],[f164,f147]) ).
fof(f781,definition,
( sQ99_spl
<=> incident(a1,ob) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f784,definition,
( sQ100_spl
<=> incident(c1,ob) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f786,plain,
( sQ100_spl
| ~ incident(c1,ob) ),
inference(component_clause,[status(thm)],[f784]) ).
fof(f787,plain,
( ~ sQ8_spl
| ~ sQ100_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f774,f781,f784,f163]) ).
fof(f788,definition,
( sQ101_spl
<=> incident(a1,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( sQ101_spl
| ~ incident(a1,b1c1) ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f791,plain,
( ~ sQ8_spl
| ~ sQ44_spl
| ~ sQ101_spl ),
inference(split_clause,[status(thm)],[f775,f788,f556,f163]) ).
fof(f792,definition,
( sQ102_spl
<=> incident(c1,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f794,plain,
( sQ102_spl
| ~ incident(c1,a1b1) ),
inference(component_clause,[status(thm)],[f792]) ).
fof(f795,plain,
( ~ sQ8_spl
| ~ sQ102_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f776,f621,f792,f163]) ).
fof(f796,definition,
( sQ103_spl
<=> incident(a1,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f797,plain,
( ~ sQ103_spl
| incident(a1,a2b2) ),
inference(component_clause,[status(thm)],[f796]) ).
fof(f798,plain,
( sQ103_spl
| ~ incident(a1,a2b2) ),
inference(component_clause,[status(thm)],[f796]) ).
fof(f799,definition,
( sQ104_spl
<=> incident(b1,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f801,plain,
( sQ104_spl
| ~ incident(b1,a2b2) ),
inference(component_clause,[status(thm)],[f799]) ).
fof(f802,plain,
( ~ sQ4_spl
| ~ sQ8_spl
| ~ sQ104_spl
| ~ sQ103_spl ),
inference(split_clause,[status(thm)],[f777,f796,f799,f163,f146]) ).
fof(f803,definition,
( sQ105_spl
<=> incident(a1,oc) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f805,plain,
( sQ105_spl
| ~ incident(a1,oc) ),
inference(component_clause,[status(thm)],[f803]) ).
fof(f806,definition,
( sQ106_spl
<=> incident(b1,oc) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f808,plain,
( sQ106_spl
| ~ incident(b1,oc) ),
inference(component_clause,[status(thm)],[f806]) ).
fof(f811,definition,
( sQ107_spl
<=> incident(b1,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( sQ107_spl
| ~ incident(b1,a1c1) ),
inference(component_clause,[status(thm)],[f811]) ).
fof(f815,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f63]) ).
fof(f816,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f815]) ).
fof(f817,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f619,f67]) ).
fof(f818,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f817]) ).
fof(f820,plain,
( ~ sQ9_spl
| ~ incident(c2,b2c2)
| ~ incident(a2,b2c2) ),
inference(resolution,[status(thm)],[f168,f74]) ).
fof(f821,plain,
( ~ sQ9_spl
| ~ incident(c2,a2b2)
| ~ incident(a2,a2b2) ),
inference(resolution,[status(thm)],[f168,f66]) ).
fof(f822,plain,
( ~ sQ9_spl
| ~ incident(b2,oc)
| ~ incident(a2,oc) ),
inference(resolution,[status(thm)],[f168,f83]) ).
fof(f825,definition,
( sQ108_spl
<=> incident(a2,ob) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f827,plain,
( sQ108_spl
| ~ incident(a2,ob) ),
inference(component_clause,[status(thm)],[f825]) ).
fof(f828,definition,
( sQ109_spl
<=> incident(c2,ob) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f829,plain,
( ~ sQ109_spl
| incident(c2,ob) ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f830,plain,
( sQ109_spl
| ~ incident(c2,ob) ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f832,definition,
( sQ110_spl
<=> incident(a2,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f834,plain,
( sQ110_spl
| ~ incident(a2,b2c2) ),
inference(component_clause,[status(thm)],[f832]) ).
fof(f835,plain,
( ~ sQ9_spl
| ~ sQ40_spl
| ~ sQ110_spl ),
inference(split_clause,[status(thm)],[f820,f832,f540,f167]) ).
fof(f836,definition,
( sQ111_spl
<=> incident(c2,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( sQ111_spl
| ~ incident(c2,a2b2) ),
inference(component_clause,[status(thm)],[f836]) ).
fof(f839,plain,
( ~ sQ9_spl
| ~ sQ111_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f821,f590,f836,f167]) ).
fof(f840,definition,
( sQ112_spl
<=> incident(a2,oc) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f843,definition,
( sQ113_spl
<=> incident(b2,oc) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( sQ113_spl
| ~ incident(b2,oc) ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,plain,
( ~ sQ9_spl
| ~ sQ113_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f822,f840,f843,f167]) ).
fof(f848,definition,
( sQ114_spl
<=> incident(b2,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f850,plain,
( sQ114_spl
| ~ incident(b2,a2c2) ),
inference(component_clause,[status(thm)],[f848]) ).
fof(f852,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f592,f65]) ).
fof(f853,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f852]) ).
fof(f854,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f588,f69]) ).
fof(f855,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f854]) ).
fof(f858,plain,
! [X0,X1] :
( ~ sQ7_spl
| line_equal(X1,a1b1)
| point_equal(X0,c2)
| ~ incident(c2,X1)
| ~ incident(X0,a1b1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f157,f131]) ).
fof(f862,plain,
! [X0,X1] :
( ~ sQ7_spl
| line_equal(X0,a1b1)
| point_equal(c2,X1)
| ~ incident(X1,a1b1)
| ~ incident(X1,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f157,f131]) ).
fof(f867,definition,
( sQ115_spl
<=> incident(a2,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f870,definition,
( sQ116_spl
<=> incident(b2,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f985,plain,
! [X0] :
( line_equal(a1b1,a2b2)
| point_equal(ab,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f314,f88]) ).
fof(f990,definition,
! [X0] :
( sQ118_spl
<=> ( point_equal(ab,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f991,plain,
! [X0] :
( ~ sQ118_spl
| point_equal(ab,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1b1) ),
inference(component_clause,[status(thm)],[f990]) ).
fof(f993,plain,
( sQ15_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f985,f990,f191]) ).
fof(f996,definition,
( sQ119_spl
<=> line_equal(a2b2,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f997,plain,
( ~ sQ119_spl
| line_equal(a2b2,a1b1) ),
inference(component_clause,[status(thm)],[f996]) ).
fof(f1005,plain,
! [X0] :
( line_equal(a1c1,a2c2)
| point_equal(ac,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f318,f86]) ).
fof(f1010,definition,
! [X0] :
( sQ122_spl
<=> ( point_equal(ac,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
! [X0] :
( ~ sQ122_spl
| point_equal(ac,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1c1) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,plain,
( sQ14_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1005,f1010,f187]) ).
fof(f1026,plain,
! [X0] :
( line_equal(b1c1,b2c2)
| point_equal(bc,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f322,f84]) ).
fof(f1031,definition,
! [X0] :
( sQ126_spl
<=> ( point_equal(bc,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1032,plain,
! [X0] :
( ~ sQ126_spl
| point_equal(bc,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,b1c1) ),
inference(component_clause,[status(thm)],[f1031]) ).
fof(f1034,plain,
( sQ13_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f1026,f1031,f183]) ).
fof(f1037,definition,
( sQ127_spl
<=> line_equal(b2c2,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1038,plain,
( ~ sQ127_spl
| line_equal(b2c2,b1c1) ),
inference(component_clause,[status(thm)],[f1037]) ).
fof(f1048,plain,
! [X0] :
( line_equal(ob,oc)
| point_equal(o,X0)
| ~ incident(X0,oc)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f326,f76]) ).
fof(f1049,plain,
! [X0] :
( line_equal(oa,oc)
| point_equal(o,X0)
| ~ incident(X0,oc)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f326,f75]) ).
fof(f1054,definition,
! [X0] :
( sQ130_spl
<=> ( point_equal(o,X0)
| ~ incident(X0,oc)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
! [X0] :
( ~ sQ130_spl
| point_equal(o,X0)
| ~ incident(X0,oc)
| ~ incident(X0,ob) ),
inference(component_clause,[status(thm)],[f1054]) ).
fof(f1057,definition,
( sQ131_spl
<=> line_equal(ob,oc) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1058,plain,
( ~ sQ131_spl
| line_equal(ob,oc) ),
inference(component_clause,[status(thm)],[f1057]) ).
fof(f1060,plain,
( sQ131_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f1048,f1054,f1057]) ).
fof(f1061,definition,
! [X0] :
( sQ132_spl
<=> ( point_equal(o,X0)
| ~ incident(X0,oc)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
! [X0] :
( ~ sQ132_spl
| point_equal(o,X0)
| ~ incident(X0,oc)
| ~ incident(X0,oa) ),
inference(component_clause,[status(thm)],[f1061]) ).
fof(f1064,definition,
( sQ133_spl
<=> line_equal(oa,oc) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1065,plain,
( ~ sQ133_spl
| line_equal(oa,oc) ),
inference(component_clause,[status(thm)],[f1064]) ).
fof(f1067,plain,
( sQ133_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f1049,f1061,f1064]) ).
fof(f1068,plain,
! [X0] :
( line_equal(oc,ob)
| point_equal(o,X0)
| ~ incident(X0,ob)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f328,f77]) ).
fof(f1070,plain,
! [X0] :
( line_equal(oa,ob)
| point_equal(o,X0)
| ~ incident(X0,ob)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f328,f75]) ).
fof(f1071,definition,
( sQ134_spl
<=> line_equal(oc,ob) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1072,plain,
( ~ sQ134_spl
| line_equal(oc,ob) ),
inference(component_clause,[status(thm)],[f1071]) ).
fof(f1074,plain,
( sQ134_spl
| sQ130_spl ),
inference(split_clause,[status(thm)],[f1068,f1054,f1071]) ).
fof(f1079,definition,
! [X0] :
( sQ136_spl
<=> ( point_equal(o,X0)
| ~ incident(X0,ob)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1080,plain,
! [X0] :
( ~ sQ136_spl
| point_equal(o,X0)
| ~ incident(X0,ob)
| ~ incident(X0,oa) ),
inference(component_clause,[status(thm)],[f1079]) ).
fof(f1082,definition,
( sQ137_spl
<=> line_equal(oa,ob) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1083,plain,
( ~ sQ137_spl
| line_equal(oa,ob) ),
inference(component_clause,[status(thm)],[f1082]) ).
fof(f1085,plain,
( sQ137_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f1070,f1079,f1082]) ).
fof(f1089,definition,
( sQ138_spl
<=> line_equal(oc,oa) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1090,plain,
( ~ sQ138_spl
| line_equal(oc,oa) ),
inference(component_clause,[status(thm)],[f1089]) ).
fof(f1093,definition,
( sQ139_spl
<=> line_equal(ob,oa) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1094,plain,
( ~ sQ139_spl
| line_equal(ob,oa) ),
inference(component_clause,[status(thm)],[f1093]) ).
fof(f1103,plain,
! [X0] :
( line_equal(b2c2,oc)
| point_equal(c2,X0)
| ~ incident(X0,oc)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f332,f73]) ).
fof(f1105,definition,
! [X0] :
( sQ141_spl
<=> ( point_equal(c2,X0)
| ~ incident(X0,oc)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1108,definition,
( sQ142_spl
<=> line_equal(a1b1,oc) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1109,plain,
( ~ sQ142_spl
| line_equal(a1b1,oc) ),
inference(component_clause,[status(thm)],[f1108]) ).
fof(f1116,definition,
! [X0] :
( sQ144_spl
<=> ( point_equal(c2,X0)
| ~ incident(X0,oc)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1117,plain,
! [X0] :
( ~ sQ144_spl
| point_equal(c2,X0)
| ~ incident(X0,oc)
| ~ incident(X0,b2c2) ),
inference(component_clause,[status(thm)],[f1116]) ).
fof(f1119,definition,
( sQ145_spl
<=> line_equal(b2c2,oc) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( ~ sQ145_spl
| line_equal(b2c2,oc) ),
inference(component_clause,[status(thm)],[f1119]) ).
fof(f1122,plain,
( sQ145_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f1103,f1116,f1119]) ).
fof(f1123,definition,
! [X0] :
( sQ146_spl
<=> ( point_equal(c2,X0)
| ~ incident(X0,oc)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1124,plain,
! [X0] :
( ~ sQ146_spl
| point_equal(c2,X0)
| ~ incident(X0,oc)
| ~ incident(X0,a2c2) ),
inference(component_clause,[status(thm)],[f1123]) ).
fof(f1126,definition,
( sQ147_spl
<=> line_equal(a2c2,oc) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1127,plain,
( ~ sQ147_spl
| line_equal(a2c2,oc) ),
inference(component_clause,[status(thm)],[f1126]) ).
fof(f1131,plain,
( ~ sQ118_spl
| point_equal(ab,ab)
| ~ incident(ab,a2b2) ),
inference(resolution,[status(thm)],[f991,f88]) ).
fof(f1133,plain,
( ~ sQ118_spl
| point_equal(ab,b1)
| ~ incident(b1,a2b2) ),
inference(resolution,[status(thm)],[f991,f64]) ).
fof(f1134,plain,
( ~ sQ118_spl
| point_equal(ab,a1)
| ~ incident(a1,a2b2) ),
inference(resolution,[status(thm)],[f991,f63]) ).
fof(f1135,plain,
( ~ sQ118_spl
| sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f1131,f458,f461,f990]) ).
fof(f1136,definition,
( sQ148_spl
<=> point_equal(ab,c2) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1137,plain,
( ~ sQ148_spl
| point_equal(ab,c2) ),
inference(component_clause,[status(thm)],[f1136]) ).
fof(f1140,definition,
( sQ149_spl
<=> point_equal(ab,b1) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1141,plain,
( ~ sQ149_spl
| point_equal(ab,b1) ),
inference(component_clause,[status(thm)],[f1140]) ).
fof(f1143,plain,
( ~ sQ118_spl
| sQ149_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f1133,f799,f1140,f990]) ).
fof(f1144,definition,
( sQ150_spl
<=> point_equal(ab,a1) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1145,plain,
( ~ sQ150_spl
| point_equal(ab,a1) ),
inference(component_clause,[status(thm)],[f1144]) ).
fof(f1147,plain,
( ~ sQ118_spl
| sQ150_spl
| ~ sQ103_spl ),
inference(split_clause,[status(thm)],[f1134,f796,f1144,f990]) ).
fof(f1148,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(a1b1,b2c2)
| point_equal(c2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f334,f157]) ).
fof(f1151,plain,
! [X0] :
( line_equal(a2c2,b2c2)
| point_equal(c2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f334,f70]) ).
fof(f1152,definition,
! [X0] :
( sQ151_spl
<=> ( point_equal(c2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1155,definition,
( sQ152_spl
<=> line_equal(a1b1,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
( ~ sQ152_spl
| line_equal(a1b1,b2c2) ),
inference(component_clause,[status(thm)],[f1155]) ).
fof(f1158,plain,
( ~ sQ7_spl
| sQ152_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f1148,f1152,f1155,f156]) ).
fof(f1159,definition,
( sQ153_spl
<=> line_equal(oc,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1160,plain,
( ~ sQ153_spl
| line_equal(oc,b2c2) ),
inference(component_clause,[status(thm)],[f1159]) ).
fof(f1167,definition,
! [X0] :
( sQ155_spl
<=> ( point_equal(c2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1168,plain,
! [X0] :
( ~ sQ155_spl
| point_equal(c2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ),
inference(component_clause,[status(thm)],[f1167]) ).
fof(f1170,definition,
( sQ156_spl
<=> line_equal(a2c2,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
( ~ sQ156_spl
| line_equal(a2c2,b2c2) ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1173,plain,
( sQ156_spl
| sQ155_spl ),
inference(split_clause,[status(thm)],[f1151,f1167,f1170]) ).
fof(f1174,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(a1b1,a2c2)
| point_equal(c2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f336,f157]) ).
fof(f1175,plain,
! [X0] :
( line_equal(oc,a2c2)
| point_equal(c2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f336,f83]) ).
fof(f1178,definition,
! [X0] :
( sQ157_spl
<=> ( point_equal(c2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1181,definition,
( sQ158_spl
<=> line_equal(a1b1,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f1182,plain,
( ~ sQ158_spl
| line_equal(a1b1,a2c2) ),
inference(component_clause,[status(thm)],[f1181]) ).
fof(f1184,plain,
( ~ sQ7_spl
| sQ158_spl
| sQ157_spl ),
inference(split_clause,[status(thm)],[f1174,f1178,f1181,f156]) ).
fof(f1185,definition,
( sQ159_spl
<=> line_equal(oc,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1186,plain,
( ~ sQ159_spl
| line_equal(oc,a2c2) ),
inference(component_clause,[status(thm)],[f1185]) ).
fof(f1188,plain,
( sQ159_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f1175,f1123,f1185]) ).
fof(f1189,definition,
( sQ160_spl
<=> line_equal(b2c2,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1190,plain,
( ~ sQ160_spl
| line_equal(b2c2,a2c2) ),
inference(component_clause,[status(thm)],[f1189]) ).
fof(f1198,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(oc,a2b2)
| point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f338,f82]) ).
fof(f1199,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(b1c1,a2b2)
| point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f338,f71]) ).
fof(f1200,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(a1c1,a2b2)
| point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f338,f68]) ).
fof(f1205,definition,
! [X0] :
( sQ163_spl
<=> ( point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1206,plain,
! [X0] :
( ~ sQ163_spl
| point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,oc) ),
inference(component_clause,[status(thm)],[f1205]) ).
fof(f1208,definition,
( sQ164_spl
<=> line_equal(oc,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1209,plain,
( ~ sQ164_spl
| line_equal(oc,a2b2) ),
inference(component_clause,[status(thm)],[f1208]) ).
fof(f1211,plain,
( ~ sQ4_spl
| sQ164_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f1198,f1205,f1208,f146]) ).
fof(f1212,definition,
! [X0] :
( sQ165_spl
<=> ( point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1215,definition,
( sQ166_spl
<=> line_equal(b1c1,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1216,plain,
( ~ sQ166_spl
| line_equal(b1c1,a2b2) ),
inference(component_clause,[status(thm)],[f1215]) ).
fof(f1218,plain,
( ~ sQ4_spl
| sQ166_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f1199,f1212,f1215,f146]) ).
fof(f1219,definition,
! [X0] :
( sQ167_spl
<=> ( point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f1220,plain,
! [X0] :
( ~ sQ167_spl
| point_equal(c1,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1c1) ),
inference(component_clause,[status(thm)],[f1219]) ).
fof(f1222,definition,
( sQ168_spl
<=> line_equal(a1c1,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
( ~ sQ168_spl
| line_equal(a1c1,a2b2) ),
inference(component_clause,[status(thm)],[f1222]) ).
fof(f1225,plain,
( ~ sQ4_spl
| sQ168_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f1200,f1219,f1222,f146]) ).
fof(f1228,plain,
! [X0] :
( line_equal(b1c1,oc)
| point_equal(c1,X0)
| ~ incident(X0,oc)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f340,f71]) ).
fof(f1229,plain,
! [X0] :
( line_equal(a1c1,oc)
| point_equal(c1,X0)
| ~ incident(X0,oc)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f340,f68]) ).
fof(f1238,definition,
! [X0] :
( sQ171_spl
<=> ( point_equal(c1,X0)
| ~ incident(X0,oc)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1241,definition,
( sQ172_spl
<=> line_equal(b1c1,oc) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1242,plain,
( ~ sQ172_spl
| line_equal(b1c1,oc) ),
inference(component_clause,[status(thm)],[f1241]) ).
fof(f1244,plain,
( sQ172_spl
| sQ171_spl ),
inference(split_clause,[status(thm)],[f1228,f1238,f1241]) ).
fof(f1245,definition,
! [X0] :
( sQ173_spl
<=> ( point_equal(c1,X0)
| ~ incident(X0,oc)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f1248,definition,
( sQ174_spl
<=> line_equal(a1c1,oc) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1249,plain,
( ~ sQ174_spl
| line_equal(a1c1,oc) ),
inference(component_clause,[status(thm)],[f1248]) ).
fof(f1251,plain,
( sQ174_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f1229,f1245,f1248]) ).
fof(f1255,plain,
! [X0] :
( line_equal(a1c1,b1c1)
| point_equal(c1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f342,f68]) ).
fof(f1256,definition,
( sQ175_spl
<=> line_equal(a2b2,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f1257,plain,
( ~ sQ175_spl
| line_equal(a2b2,b1c1) ),
inference(component_clause,[status(thm)],[f1256]) ).
fof(f1260,definition,
( sQ176_spl
<=> line_equal(oc,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1261,plain,
( ~ sQ176_spl
| line_equal(oc,b1c1) ),
inference(component_clause,[status(thm)],[f1260]) ).
fof(f1268,definition,
! [X0] :
( sQ178_spl
<=> ( point_equal(c1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f1269,plain,
! [X0] :
( ~ sQ178_spl
| point_equal(c1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1c1) ),
inference(component_clause,[status(thm)],[f1268]) ).
fof(f1271,definition,
( sQ179_spl
<=> line_equal(a1c1,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1272,plain,
( ~ sQ179_spl
| line_equal(a1c1,b1c1) ),
inference(component_clause,[status(thm)],[f1271]) ).
fof(f1274,plain,
( sQ179_spl
| sQ178_spl ),
inference(split_clause,[status(thm)],[f1255,f1268,f1271]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(a2b2,a1c1)
| point_equal(c1,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f344,f147]) ).
fof(f1279,definition,
( sQ180_spl
<=> line_equal(a2b2,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f1280,plain,
( ~ sQ180_spl
| line_equal(a2b2,a1c1) ),
inference(component_clause,[status(thm)],[f1279]) ).
fof(f1282,plain,
( ~ sQ4_spl
| sQ180_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f1275,f1219,f1279,f146]) ).
fof(f1287,definition,
( sQ182_spl
<=> line_equal(b1c1,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f1288,plain,
( ~ sQ182_spl
| line_equal(b1c1,a1c1) ),
inference(component_clause,[status(thm)],[f1287]) ).
fof(f1295,plain,
( ~ sQ122_spl
| point_equal(ac,ac)
| ~ incident(ac,a2c2) ),
inference(resolution,[status(thm)],[f1011,f86]) ).
fof(f1296,plain,
( ~ sQ122_spl
| point_equal(ac,c1)
| ~ incident(c1,a2c2) ),
inference(resolution,[status(thm)],[f1011,f68]) ).
fof(f1297,plain,
( ~ sQ122_spl
| point_equal(ac,a1)
| ~ incident(a1,a2c2) ),
inference(resolution,[status(thm)],[f1011,f67]) ).
fof(f1298,plain,
( ~ sQ122_spl
| sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f1295,f475,f478,f1010]) ).
fof(f1299,definition,
( sQ184_spl
<=> incident(c1,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f1301,plain,
( sQ184_spl
| ~ incident(c1,a2c2) ),
inference(component_clause,[status(thm)],[f1299]) ).
fof(f1302,definition,
( sQ185_spl
<=> point_equal(ac,c1) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( ~ sQ185_spl
| point_equal(ac,c1) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1305,plain,
( ~ sQ122_spl
| sQ185_spl
| ~ sQ184_spl ),
inference(split_clause,[status(thm)],[f1296,f1299,f1302,f1010]) ).
fof(f1306,definition,
( sQ186_spl
<=> incident(a1,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f1309,definition,
( sQ187_spl
<=> point_equal(ac,a1) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
( ~ sQ187_spl
| point_equal(ac,a1) ),
inference(component_clause,[status(thm)],[f1309]) ).
fof(f1312,plain,
( ~ sQ122_spl
| sQ187_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f1297,f1306,f1309,f1010]) ).
fof(f1314,plain,
! [X0] :
( line_equal(b2c2,ob)
| point_equal(b2,X0)
| ~ incident(X0,ob)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f346,f74]) ).
fof(f1320,definition,
! [X0] :
( sQ189_spl
<=> ( point_equal(b2,X0)
| ~ incident(X0,ob)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f1323,definition,
( sQ190_spl
<=> line_equal(b2c2,ob) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f1324,plain,
( ~ sQ190_spl
| line_equal(b2c2,ob) ),
inference(component_clause,[status(thm)],[f1323]) ).
fof(f1326,plain,
( sQ190_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f1314,f1320,f1323]) ).
fof(f1327,definition,
! [X0] :
( sQ191_spl
<=> ( point_equal(b2,X0)
| ~ incident(X0,ob)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f1330,definition,
( sQ192_spl
<=> line_equal(a2b2,ob) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f1331,plain,
( ~ sQ192_spl
| line_equal(a2b2,ob) ),
inference(component_clause,[status(thm)],[f1330]) ).
fof(f1336,plain,
! [X0] :
( line_equal(a2b2,b2c2)
| point_equal(b2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f348,f66]) ).
fof(f1337,definition,
( sQ193_spl
<=> line_equal(ob,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f1338,plain,
( ~ sQ193_spl
| line_equal(ob,b2c2) ),
inference(component_clause,[status(thm)],[f1337]) ).
fof(f1345,definition,
! [X0] :
( sQ195_spl
<=> ( point_equal(b2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f1346,plain,
! [X0] :
( ~ sQ195_spl
| point_equal(b2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2b2) ),
inference(component_clause,[status(thm)],[f1345]) ).
fof(f1348,definition,
( sQ196_spl
<=> line_equal(a2b2,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f1349,plain,
( ~ sQ196_spl
| line_equal(a2b2,b2c2) ),
inference(component_clause,[status(thm)],[f1348]) ).
fof(f1351,plain,
( sQ196_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f1336,f1345,f1348]) ).
fof(f1352,plain,
! [X0] :
( line_equal(ob,a2b2)
| point_equal(b2,X0)
| ~ incident(X0,a2b2)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f350,f81]) ).
fof(f1355,definition,
( sQ197_spl
<=> line_equal(ob,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f1356,plain,
( ~ sQ197_spl
| line_equal(ob,a2b2) ),
inference(component_clause,[status(thm)],[f1355]) ).
fof(f1358,plain,
( sQ197_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f1352,f1327,f1355]) ).
fof(f1359,definition,
( sQ198_spl
<=> line_equal(b2c2,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
( ~ sQ198_spl
| line_equal(b2c2,a2b2) ),
inference(component_clause,[status(thm)],[f1359]) ).
fof(f1374,definition,
! [X0] :
( sQ201_spl
<=> ( point_equal(a2,X0)
| ~ incident(X0,oa)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1375,plain,
! [X0] :
( ~ sQ201_spl
| point_equal(a2,X0)
| ~ incident(X0,oa)
| ~ incident(X0,a2c2) ),
inference(component_clause,[status(thm)],[f1374]) ).
fof(f1377,definition,
( sQ202_spl
<=> line_equal(a2c2,oa) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f1378,plain,
( ~ sQ202_spl
| line_equal(a2c2,oa) ),
inference(component_clause,[status(thm)],[f1377]) ).
fof(f1384,definition,
( sQ204_spl
<=> line_equal(a2b2,oa) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f1385,plain,
( ~ sQ204_spl
| line_equal(a2b2,oa) ),
inference(component_clause,[status(thm)],[f1384]) ).
fof(f1388,plain,
! [X0] :
( line_equal(oa,a2c2)
| point_equal(a2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f354,f79]) ).
fof(f1390,plain,
! [X0] :
( line_equal(a2b2,a2c2)
| point_equal(a2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f354,f65]) ).
fof(f1391,definition,
( sQ205_spl
<=> line_equal(oa,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1392,plain,
( ~ sQ205_spl
| line_equal(oa,a2c2) ),
inference(component_clause,[status(thm)],[f1391]) ).
fof(f1394,plain,
( sQ205_spl
| sQ201_spl ),
inference(split_clause,[status(thm)],[f1388,f1374,f1391]) ).
fof(f1399,definition,
! [X0] :
( sQ207_spl
<=> ( point_equal(a2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f1400,plain,
! [X0] :
( ~ sQ207_spl
| point_equal(a2,X0)
| ~ incident(X0,a2c2)
| ~ incident(X0,a2b2) ),
inference(component_clause,[status(thm)],[f1399]) ).
fof(f1402,definition,
( sQ208_spl
<=> line_equal(a2b2,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f1403,plain,
( ~ sQ208_spl
| line_equal(a2b2,a2c2) ),
inference(component_clause,[status(thm)],[f1402]) ).
fof(f1405,plain,
( sQ208_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f1390,f1399,f1402]) ).
fof(f1409,definition,
( sQ209_spl
<=> line_equal(oa,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1410,plain,
( ~ sQ209_spl
| line_equal(oa,a2b2) ),
inference(component_clause,[status(thm)],[f1409]) ).
fof(f1421,plain,
( ~ sQ126_spl
| point_equal(bc,bc)
| ~ incident(bc,b2c2) ),
inference(resolution,[status(thm)],[f1032,f84]) ).
fof(f1422,plain,
( ~ sQ126_spl
| point_equal(bc,c1)
| ~ incident(c1,b2c2) ),
inference(resolution,[status(thm)],[f1032,f71]) ).
fof(f1423,plain,
( ~ sQ126_spl
| point_equal(bc,b1)
| ~ incident(b1,b2c2) ),
inference(resolution,[status(thm)],[f1032,f72]) ).
fof(f1424,plain,
( ~ sQ126_spl
| sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1421,f492,f495,f1031]) ).
fof(f1425,definition,
( sQ212_spl
<=> incident(c1,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( sQ212_spl
| ~ incident(c1,b2c2) ),
inference(component_clause,[status(thm)],[f1425]) ).
fof(f1428,definition,
( sQ213_spl
<=> point_equal(bc,c1) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
( ~ sQ213_spl
| point_equal(bc,c1) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,plain,
( ~ sQ126_spl
| sQ213_spl
| ~ sQ212_spl ),
inference(split_clause,[status(thm)],[f1422,f1425,f1428,f1031]) ).
fof(f1432,definition,
( sQ214_spl
<=> incident(b1,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( sQ214_spl
| ~ incident(b1,b2c2) ),
inference(component_clause,[status(thm)],[f1432]) ).
fof(f1435,definition,
( sQ215_spl
<=> point_equal(bc,b1) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( ~ sQ215_spl
| point_equal(bc,b1) ),
inference(component_clause,[status(thm)],[f1435]) ).
fof(f1438,plain,
( ~ sQ126_spl
| sQ215_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f1423,f1432,f1435,f1031]) ).
fof(f1449,definition,
( sQ218_spl
<=> line_equal(b1c1,ob) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f1450,plain,
( ~ sQ218_spl
| line_equal(b1c1,ob) ),
inference(component_clause,[status(thm)],[f1449]) ).
fof(f1462,plain,
! [X0] :
( line_equal(a1b1,b1c1)
| point_equal(b1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f362,f64]) ).
fof(f1471,definition,
! [X0] :
( sQ223_spl
<=> ( point_equal(b1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f1472,plain,
! [X0] :
( ~ sQ223_spl
| point_equal(b1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1b1) ),
inference(component_clause,[status(thm)],[f1471]) ).
fof(f1474,definition,
( sQ224_spl
<=> line_equal(a1b1,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f1475,plain,
( ~ sQ224_spl
| line_equal(a1b1,b1c1) ),
inference(component_clause,[status(thm)],[f1474]) ).
fof(f1477,plain,
( sQ224_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f1462,f1471,f1474]) ).
fof(f1481,definition,
( sQ225_spl
<=> line_equal(ob,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition]) ).
fof(f1482,plain,
( ~ sQ225_spl
| line_equal(ob,a1b1) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1485,definition,
( sQ226_spl
<=> line_equal(b1c1,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f1486,plain,
( ~ sQ226_spl
| line_equal(b1c1,a1b1) ),
inference(component_clause,[status(thm)],[f1485]) ).
fof(f1511,definition,
( sQ232_spl
<=> line_equal(a1c1,oa) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( ~ sQ232_spl
| line_equal(a1c1,oa) ),
inference(component_clause,[status(thm)],[f1511]) ).
fof(f1523,plain,
! [X0] :
( ~ sQ3_spl
| line_equal(a2c2,b1c1)
| point_equal(b1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f144,f362]) ).
fof(f1524,plain,
! [X0] :
( ~ sQ3_spl
| line_equal(a2c2,ob)
| point_equal(b1,X0)
| ~ incident(X0,ob)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f144,f360]) ).
fof(f1525,plain,
( ~ sQ8_spl
| ~ sQ3_spl
| ~ incident(c1,a2c2)
| ~ incident(a1,a2c2) ),
inference(resolution,[status(thm)],[f144,f164]) ).
fof(f1539,definition,
( sQ236_spl
<=> line_equal(a2c2,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f1540,plain,
( ~ sQ236_spl
| line_equal(a2c2,a1b1) ),
inference(component_clause,[status(thm)],[f1539]) ).
fof(f1543,definition,
! [X0] :
( sQ237_spl
<=> ( point_equal(b1,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f1546,definition,
( sQ238_spl
<=> line_equal(a2c2,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f1547,plain,
( ~ sQ238_spl
| line_equal(a2c2,b1c1) ),
inference(component_clause,[status(thm)],[f1546]) ).
fof(f1549,plain,
( ~ sQ3_spl
| sQ238_spl
| sQ237_spl ),
inference(split_clause,[status(thm)],[f1523,f1543,f1546,f143]) ).
fof(f1550,definition,
! [X0] :
( sQ239_spl
<=> ( point_equal(b1,X0)
| ~ incident(X0,ob)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition]) ).
fof(f1553,definition,
( sQ240_spl
<=> line_equal(a2c2,ob) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f1554,plain,
( ~ sQ240_spl
| line_equal(a2c2,ob) ),
inference(component_clause,[status(thm)],[f1553]) ).
fof(f1556,plain,
( ~ sQ3_spl
| sQ240_spl
| sQ239_spl ),
inference(split_clause,[status(thm)],[f1524,f1550,f1553,f143]) ).
fof(f1557,plain,
( ~ sQ8_spl
| ~ sQ3_spl
| ~ sQ184_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f1525,f1306,f1299,f143,f163]) ).
fof(f1573,plain,
! [X0] :
( ~ sQ7_spl
| incident(X0,a1b1)
| ~ point_equal(X0,c2) ),
inference(resolution,[status(thm)],[f157,f126]) ).
fof(f1599,plain,
! [X0] :
( ~ sQ2_spl
| line_equal(b2c2,a1c1)
| point_equal(a1,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f368,f141]) ).
fof(f1603,definition,
! [X0] :
( sQ241_spl
<=> ( point_equal(a1,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f1604,plain,
! [X0] :
( ~ sQ241_spl
| point_equal(a1,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,b2c2) ),
inference(component_clause,[status(thm)],[f1603]) ).
fof(f1606,definition,
( sQ242_spl
<=> line_equal(b2c2,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f1607,plain,
( ~ sQ242_spl
| line_equal(b2c2,a1c1) ),
inference(component_clause,[status(thm)],[f1606]) ).
fof(f1609,plain,
( ~ sQ2_spl
| sQ242_spl
| sQ241_spl ),
inference(split_clause,[status(thm)],[f1599,f1603,f1606,f140]) ).
fof(f1618,definition,
! [X0] :
( sQ245_spl
<=> ( point_equal(a1,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f1619,plain,
! [X0] :
( ~ sQ245_spl
| point_equal(a1,X0)
| ~ incident(X0,a1c1)
| ~ incident(X0,a1b1) ),
inference(component_clause,[status(thm)],[f1618]) ).
fof(f1621,definition,
( sQ246_spl
<=> line_equal(a1b1,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f1622,plain,
( ~ sQ246_spl
| line_equal(a1b1,a1c1) ),
inference(component_clause,[status(thm)],[f1621]) ).
fof(f1627,plain,
! [X0] :
( line_equal(a1c1,a1b1)
| point_equal(a1,X0)
| ~ incident(X0,a1b1)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f370,f67]) ).
fof(f1632,definition,
( sQ248_spl
<=> line_equal(b2c2,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition]) ).
fof(f1633,plain,
( ~ sQ248_spl
| line_equal(b2c2,a1b1) ),
inference(component_clause,[status(thm)],[f1632]) ).
fof(f1640,definition,
( sQ250_spl
<=> line_equal(a1c1,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f1641,plain,
( ~ sQ250_spl
| line_equal(a1c1,a1b1) ),
inference(component_clause,[status(thm)],[f1640]) ).
fof(f1643,plain,
( sQ250_spl
| sQ245_spl ),
inference(split_clause,[status(thm)],[f1627,f1618,f1640]) ).
fof(f1651,definition,
! [X0] :
( sQ252_spl
<=> ( point_equal(X0,ab)
| ~ incident(X0,a1b1)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f1660,plain,
( ~ sQ119_spl
| line_equal(a1b1,a2b2) ),
inference(resolution,[status(thm)],[f997,f120]) ).
fof(f1663,plain,
! [X0] :
( line_equal(a1b1,a2b2)
| point_equal(X0,ab)
| ~ incident(X0,a2b2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f374,f89]) ).
fof(f1665,plain,
( sQ15_spl
| sQ252_spl ),
inference(split_clause,[status(thm)],[f1663,f1651,f191]) ).
fof(f1670,definition,
! [X0] :
( sQ253_spl
<=> ( point_equal(X0,ac)
| ~ incident(X0,a1c1)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f1674,plain,
! [X0] :
( line_equal(a1c1,a2c2)
| point_equal(X0,ac)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f378,f87]) ).
fof(f1676,plain,
( sQ14_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f1674,f1670,f187]) ).
fof(f1681,definition,
! [X0] :
( sQ254_spl
<=> ( point_equal(X0,bc)
| ~ incident(X0,b1c1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f1685,plain,
! [X0] :
( line_equal(b1c1,b2c2)
| point_equal(X0,bc)
| ~ incident(X0,b2c2)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f382,f85]) ).
fof(f1687,plain,
( sQ13_spl
| sQ254_spl ),
inference(split_clause,[status(thm)],[f1685,f1681,f183]) ).
fof(f1690,plain,
! [X0] :
( line_equal(oc,ob)
| point_equal(X0,o)
| ~ incident(X0,ob)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f384,f76]) ).
fof(f1693,definition,
! [X0] :
( sQ255_spl
<=> ( point_equal(X0,o)
| ~ incident(X0,ob)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f1696,plain,
( sQ134_spl
| sQ255_spl ),
inference(split_clause,[status(thm)],[f1690,f1693,f1071]) ).
fof(f1697,definition,
! [X0] :
( sQ256_spl
<=> ( point_equal(X0,o)
| ~ incident(X0,oa)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f1698,plain,
! [X0] :
( ~ sQ256_spl
| point_equal(X0,o)
| ~ incident(X0,oa)
| ~ incident(X0,oc) ),
inference(component_clause,[status(thm)],[f1697]) ).
fof(f1711,definition,
! [X0] :
( sQ257_spl
<=> ( point_equal(X0,o)
| ~ incident(X0,oa)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f1712,plain,
! [X0] :
( ~ sQ257_spl
| point_equal(X0,o)
| ~ incident(X0,oa)
| ~ incident(X0,ob) ),
inference(component_clause,[status(thm)],[f1711]) ).
fof(f1715,plain,
! [X0] :
( line_equal(oa,oc)
| point_equal(X0,o)
| ~ incident(X0,oc)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f388,f77]) ).
fof(f1716,plain,
! [X0] :
( line_equal(oa,ob)
| point_equal(X0,o)
| ~ incident(X0,ob)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f388,f76]) ).
fof(f1718,plain,
( sQ133_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f1715,f1697,f1064]) ).
fof(f1719,plain,
( sQ137_spl
| sQ257_spl ),
inference(split_clause,[status(thm)],[f1716,f1711,f1082]) ).
fof(f1723,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(oc,a1b1)
| point_equal(X0,c2)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f390,f157]) ).
fof(f1727,definition,
! [X0] :
( sQ258_spl
<=> ( point_equal(X0,c2)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f1728,plain,
! [X0] :
( ~ sQ258_spl
| point_equal(X0,c2)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ),
inference(component_clause,[status(thm)],[f1727]) ).
fof(f1730,definition,
( sQ259_spl
<=> line_equal(oc,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f1731,plain,
( ~ sQ259_spl
| line_equal(oc,a1b1) ),
inference(component_clause,[status(thm)],[f1730]) ).
fof(f1733,plain,
( ~ sQ7_spl
| sQ259_spl
| sQ258_spl ),
inference(split_clause,[status(thm)],[f1723,f1727,f1730,f156]) ).
fof(f1735,definition,
! [X0] :
( sQ260_spl
<=> ( point_equal(X0,c2)
| ~ incident(X0,b2c2)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f1744,plain,
! [X0] :
( line_equal(b2c2,oc)
| point_equal(X0,c2)
| ~ incident(X0,oc)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f392,f83]) ).
fof(f1747,definition,
! [X0] :
( sQ262_spl
<=> ( point_equal(X0,c2)
| ~ incident(X0,a1b1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f1751,plain,
( sQ145_spl
| sQ260_spl ),
inference(split_clause,[status(thm)],[f1744,f1735,f1119]) ).
fof(f1753,definition,
! [X0] :
( sQ263_spl
<=> ( point_equal(X0,c2)
| ~ incident(X0,a2c2)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f1754,plain,
! [X0] :
( ~ sQ263_spl
| point_equal(X0,c2)
| ~ incident(X0,a2c2)
| ~ incident(X0,b2c2) ),
inference(component_clause,[status(thm)],[f1753]) ).
fof(f1759,plain,
! [X0] :
( line_equal(a2c2,b2c2)
| point_equal(X0,c2)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f394,f73]) ).
fof(f1761,definition,
! [X0] :
( sQ264_spl
<=> ( point_equal(X0,c2)
| ~ incident(X0,a1b1)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f1766,plain,
( sQ156_spl
| sQ263_spl ),
inference(split_clause,[status(thm)],[f1759,f1753,f1170]) ).
fof(f1770,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(a2b2,b1c1)
| point_equal(X0,c1)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f396,f71]) ).
fof(f1773,definition,
! [X0] :
( sQ265_spl
<=> ( point_equal(X0,c1)
| ~ incident(X0,oc)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f1774,plain,
! [X0] :
( ~ sQ265_spl
| point_equal(X0,c1)
| ~ incident(X0,oc)
| ~ incident(X0,a2b2) ),
inference(component_clause,[status(thm)],[f1773]) ).
fof(f1777,definition,
! [X0] :
( sQ266_spl
<=> ( point_equal(X0,c1)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f1780,plain,
( ~ sQ4_spl
| sQ175_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f1770,f1777,f1256,f146]) ).
fof(f1789,plain,
( ~ sQ248_spl
| line_equal(a1b1,b2c2) ),
inference(resolution,[status(thm)],[f1633,f120]) ).
fof(f1793,plain,
( ~ sQ236_spl
| incident(c2,a1b1) ),
inference(resolution,[status(thm)],[f1540,f295]) ).
fof(f1796,plain,
( ~ sQ236_spl
| line_equal(a1b1,a2c2) ),
inference(resolution,[status(thm)],[f1540,f120]) ).
fof(f1797,plain,
( ~ sQ236_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1793,f156,f1539]) ).
fof(f1807,plain,
! [X0] :
( ~ sQ6_spl
| line_equal(a1c1,b2c2)
| point_equal(b2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f154,f348]) ).
fof(f1812,plain,
! [X0,X1] :
( ~ sQ6_spl
| line_equal(X1,a1c1)
| point_equal(X0,b2)
| ~ incident(b2,X1)
| ~ incident(X0,a1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f154,f131]) ).
fof(f1825,definition,
! [X0] :
( sQ269_spl
<=> ( point_equal(b2,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f1828,definition,
( sQ270_spl
<=> line_equal(a1c1,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f1829,plain,
( ~ sQ270_spl
| line_equal(a1c1,b2c2) ),
inference(component_clause,[status(thm)],[f1828]) ).
fof(f1831,plain,
( ~ sQ6_spl
| sQ270_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f1807,f1825,f1828,f153]) ).
fof(f1835,definition,
( sQ272_spl
<=> line_equal(a1c1,ob) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f1836,plain,
( ~ sQ272_spl
| line_equal(a1c1,ob) ),
inference(component_clause,[status(thm)],[f1835]) ).
fof(f1839,definition,
( sQ273_spl
<=> incident(a2,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition]) ).
fof(f1840,plain,
( ~ sQ273_spl
| incident(a2,a1c1) ),
inference(component_clause,[status(thm)],[f1839]) ).
fof(f1841,plain,
( sQ273_spl
| ~ incident(a2,a1c1) ),
inference(component_clause,[status(thm)],[f1839]) ).
fof(f1842,definition,
( sQ274_spl
<=> incident(c2,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f1844,plain,
( sQ274_spl
| ~ incident(c2,a1c1) ),
inference(component_clause,[status(thm)],[f1842]) ).
fof(f1879,plain,
! [X0,X1] :
( ~ sQ5_spl
| line_equal(X1,b1c1)
| point_equal(X0,a2)
| ~ incident(a2,X1)
| ~ incident(X0,b1c1)
| ~ incident(X0,X1) ),
inference(resolution,[status(thm)],[f151,f131]) ).
fof(f1895,definition,
( sQ278_spl
<=> line_equal(b1c1,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f1896,plain,
( ~ sQ278_spl
| line_equal(b1c1,a2c2) ),
inference(component_clause,[status(thm)],[f1895]) ).
fof(f1902,definition,
( sQ280_spl
<=> line_equal(b1c1,oa) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f1903,plain,
( ~ sQ280_spl
| line_equal(b1c1,oa) ),
inference(component_clause,[status(thm)],[f1902]) ).
fof(f1914,plain,
! [X0] :
( line_equal(oc,b1c1)
| point_equal(X0,c1)
| ~ incident(X0,b1c1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f398,f71]) ).
fof(f1917,definition,
! [X0] :
( sQ282_spl
<=> ( point_equal(X0,c1)
| ~ incident(X0,b1c1)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f1918,plain,
! [X0] :
( ~ sQ282_spl
| point_equal(X0,c1)
| ~ incident(X0,b1c1)
| ~ incident(X0,oc) ),
inference(component_clause,[status(thm)],[f1917]) ).
fof(f1920,plain,
( sQ176_spl
| sQ282_spl ),
inference(split_clause,[status(thm)],[f1914,f1917,f1260]) ).
fof(f1921,definition,
! [X0] :
( sQ283_spl
<=> ( point_equal(X0,c1)
| ~ incident(X0,a1c1)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f1925,plain,
! [X0] :
( line_equal(b1c1,oc)
| point_equal(X0,c1)
| ~ incident(X0,oc)
| ~ incident(X0,b1c1) ),
inference(resolution,[status(thm)],[f400,f82]) ).
fof(f1928,plain,
( sQ172_spl
| sQ282_spl ),
inference(split_clause,[status(thm)],[f1925,f1917,f1241]) ).
fof(f1930,definition,
! [X0] :
( sQ284_spl
<=> ( point_equal(X0,c1)
| ~ incident(X0,a1c1)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f1939,plain,
! [X0] :
( line_equal(a1c1,oc)
| point_equal(X0,c1)
| ~ incident(X0,oc)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f402,f82]) ).
fof(f1940,plain,
! [X0] :
( line_equal(a1c1,b1c1)
| point_equal(X0,c1)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f402,f71]) ).
fof(f1942,plain,
( sQ174_spl
| sQ283_spl ),
inference(split_clause,[status(thm)],[f1939,f1921,f1248]) ).
fof(f1943,plain,
( sQ179_spl
| sQ284_spl ),
inference(split_clause,[status(thm)],[f1940,f1930,f1271]) ).
fof(f1947,plain,
! [X0] :
( line_equal(ob,b2c2)
| point_equal(X0,b2)
| ~ incident(X0,b2c2)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f404,f74]) ).
fof(f1948,plain,
! [X0] :
( line_equal(ob,a2b2)
| point_equal(X0,b2)
| ~ incident(X0,a2b2)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f404,f66]) ).
fof(f1957,definition,
! [X0] :
( sQ287_spl
<=> ( point_equal(X0,b2)
| ~ incident(X0,b2c2)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition]) ).
fof(f1958,plain,
! [X0] :
( ~ sQ287_spl
| point_equal(X0,b2)
| ~ incident(X0,b2c2)
| ~ incident(X0,ob) ),
inference(component_clause,[status(thm)],[f1957]) ).
fof(f1960,plain,
( sQ193_spl
| sQ287_spl ),
inference(split_clause,[status(thm)],[f1947,f1957,f1337]) ).
fof(f1961,definition,
! [X0] :
( sQ288_spl
<=> ( point_equal(X0,b2)
| ~ incident(X0,a2b2)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition]) ).
fof(f1962,plain,
! [X0] :
( ~ sQ288_spl
| point_equal(X0,b2)
| ~ incident(X0,a2b2)
| ~ incident(X0,ob) ),
inference(component_clause,[status(thm)],[f1961]) ).
fof(f1964,plain,
( sQ197_spl
| sQ288_spl ),
inference(split_clause,[status(thm)],[f1948,f1961,f1355]) ).
fof(f1966,plain,
! [X0] :
( line_equal(b2c2,ob)
| point_equal(X0,b2)
| ~ incident(X0,ob)
| ~ incident(X0,b2c2) ),
inference(resolution,[status(thm)],[f406,f81]) ).
fof(f1969,definition,
! [X0] :
( sQ289_spl
<=> ( point_equal(X0,b2)
| ~ incident(X0,a1c1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition]) ).
fof(f1973,plain,
( sQ190_spl
| sQ287_spl ),
inference(split_clause,[status(thm)],[f1966,f1957,f1323]) ).
fof(f1975,definition,
! [X0] :
( sQ290_spl
<=> ( point_equal(X0,b2)
| ~ incident(X0,a2b2)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f1979,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f494,f85]) ).
fof(f1980,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1979]) ).
fof(f1981,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f87]) ).
fof(f1982,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1981]) ).
fof(f1983,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f89]) ).
fof(f1984,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1983]) ).
fof(f1985,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f74]) ).
fof(f1986,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f1985]) ).
fof(f1987,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f73]) ).
fof(f1988,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f1987]) ).
fof(f1989,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f604,f72]) ).
fof(f1990,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f1989]) ).
fof(f1991,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f558,f71]) ).
fof(f1992,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f1991]) ).
fof(f2042,plain,
! [X0] :
( line_equal(a2b2,b2c2)
| point_equal(X0,b2)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f408,f74]) ).
fof(f2045,plain,
( sQ196_spl
| sQ290_spl ),
inference(split_clause,[status(thm)],[f2042,f1975,f1348]) ).
fof(f2049,plain,
! [X0] :
( line_equal(oa,a2c2)
| point_equal(X0,a2)
| ~ incident(X0,a2c2)
| ~ incident(X0,oa) ),
inference(resolution,[status(thm)],[f410,f69]) ).
fof(f2059,definition,
! [X0] :
( sQ293_spl
<=> ( point_equal(X0,a2)
| ~ incident(X0,a2c2)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[sQ293_spl])],[split_symbol_definition]) ).
fof(f2060,plain,
! [X0] :
( ~ sQ293_spl
| point_equal(X0,a2)
| ~ incident(X0,a2c2)
| ~ incident(X0,oa) ),
inference(component_clause,[status(thm)],[f2059]) ).
fof(f2062,plain,
( sQ205_spl
| sQ293_spl ),
inference(split_clause,[status(thm)],[f2049,f2059,f1391]) ).
fof(f2068,plain,
! [X0] :
( line_equal(a2c2,oa)
| point_equal(X0,a2)
| ~ incident(X0,oa)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f412,f79]) ).
fof(f2075,plain,
( sQ202_spl
| sQ293_spl ),
inference(split_clause,[status(thm)],[f2068,f2059,f1377]) ).
fof(f2077,definition,
! [X0] :
( sQ296_spl
<=> ( point_equal(X0,a2)
| ~ incident(X0,a2b2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f2083,plain,
! [X0] :
( line_equal(a2b2,a2c2)
| point_equal(X0,a2)
| ~ incident(X0,a2c2)
| ~ incident(X0,a2b2) ),
inference(resolution,[status(thm)],[f414,f69]) ).
fof(f2090,plain,
( sQ208_spl
| sQ296_spl ),
inference(split_clause,[status(thm)],[f2083,f2077,f1402]) ).
fof(f2092,plain,
( ~ sQ168_spl
| incident(a1,a2b2) ),
inference(resolution,[status(thm)],[f1223,f311]) ).
fof(f2093,plain,
( ~ sQ168_spl
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[f1223,f299]) ).
fof(f2094,plain,
( ~ sQ168_spl
| incident(ac,a2b2) ),
inference(resolution,[status(thm)],[f1223,f287]) ).
fof(f2097,plain,
( ~ sQ168_spl
| sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f798]) ).
fof(f2098,plain,
( ~ sQ168_spl
| sQ103_spl ),
inference(contradiction_clause,[status(thm)],[f2097]) ).
fof(f2116,definition,
! [X0] :
( sQ300_spl
<=> ( point_equal(X0,b1)
| ~ incident(X0,a1b1)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ300_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( ~ sQ166_spl
| incident(b1,a2b2) ),
inference(resolution,[status(thm)],[f1216,f308]) ).
fof(f2121,plain,
( ~ sQ166_spl
| incident(c1,a2b2) ),
inference(resolution,[status(thm)],[f1216,f298]) ).
fof(f2125,plain,
( ~ sQ166_spl
| sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2120,f801]) ).
fof(f2126,plain,
( ~ sQ166_spl
| sQ104_spl ),
inference(contradiction_clause,[status(thm)],[f2125]) ).
fof(f2127,plain,
( ~ sQ197_spl
| incident(b1,a2b2) ),
inference(resolution,[status(thm)],[f1356,f307]) ).
fof(f2129,plain,
( ~ sQ197_spl
| incident(o,a2b2) ),
inference(resolution,[status(thm)],[f1356,f291]) ).
fof(f2132,plain,
( ~ sQ197_spl
| sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2127,f801]) ).
fof(f2133,plain,
( ~ sQ197_spl
| sQ104_spl ),
inference(contradiction_clause,[status(thm)],[f2132]) ).
fof(f2135,plain,
! [X0] :
( line_equal(a1b1,b1c1)
| point_equal(X0,b1)
| ~ incident(X0,b1c1)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f422,f72]) ).
fof(f2138,plain,
( sQ224_spl
| sQ300_spl ),
inference(split_clause,[status(thm)],[f2135,f2116,f1474]) ).
fof(f2170,definition,
! [X0] :
( sQ306_spl
<=> ( point_equal(X0,a1)
| ~ incident(X0,a1b1)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f2171,plain,
! [X0] :
( ~ sQ306_spl
| point_equal(X0,a1)
| ~ incident(X0,a1b1)
| ~ incident(X0,a1c1) ),
inference(component_clause,[status(thm)],[f2170]) ).
fof(f2176,plain,
! [X0] :
( line_equal(a1b1,a1c1)
| point_equal(X0,a1)
| ~ incident(X0,a1c1)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f428,f67]) ).
fof(f2183,plain,
( sQ246_spl
| sQ306_spl ),
inference(split_clause,[status(thm)],[f2176,f2170,f1621]) ).
fof(f2185,plain,
( ~ sQ193_spl
| incident(b1,b2c2) ),
inference(resolution,[status(thm)],[f1338,f307]) ).
fof(f2190,plain,
( ~ sQ193_spl
| sQ214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2185,f1434]) ).
fof(f2191,plain,
( ~ sQ193_spl
| sQ214_spl ),
inference(contradiction_clause,[status(thm)],[f2190]) ).
fof(f2193,plain,
( ~ sQ198_spl
| incident(c2,a2b2) ),
inference(resolution,[status(thm)],[f1360,f294]) ).
fof(f2197,plain,
( ~ sQ198_spl
| sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2193,f838]) ).
fof(f2198,plain,
( ~ sQ198_spl
| sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f2197]) ).
fof(f2199,plain,
( ~ sQ242_spl
| incident(b2,a1c1) ),
inference(resolution,[status(thm)],[f1607,f301]) ).
fof(f2204,plain,
( ~ sQ242_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f2199,f153,f1606]) ).
fof(f2209,plain,
! [X0] :
( ~ sQ3_spl
| line_equal(ob,a2c2)
| point_equal(X0,b1)
| ~ incident(X0,a2c2)
| ~ incident(X0,ob) ),
inference(resolution,[status(thm)],[f144,f418]) ).
fof(f2228,definition,
! [X0] :
( sQ309_spl
<=> ( point_equal(X0,b1)
| ~ incident(X0,a2c2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f2232,definition,
! [X0] :
( sQ310_spl
<=> ( point_equal(X0,b1)
| ~ incident(X0,a2c2)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f2235,definition,
( sQ311_spl
<=> line_equal(ob,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f2236,plain,
( ~ sQ311_spl
| line_equal(ob,a2c2) ),
inference(component_clause,[status(thm)],[f2235]) ).
fof(f2238,plain,
( ~ sQ3_spl
| sQ311_spl
| sQ310_spl ),
inference(split_clause,[status(thm)],[f2209,f2232,f2235,f143]) ).
fof(f2257,definition,
! [X0] :
( sQ313_spl
<=> ( line_equal(X0,a2b2)
| ~ incident(ab,X0)
| ~ incident(b2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f2258,plain,
! [X0] :
( ~ sQ313_spl
| line_equal(X0,a2b2)
| ~ incident(ab,X0)
| ~ incident(b2,X0) ),
inference(component_clause,[status(thm)],[f2257]) ).
fof(f2284,definition,
! [X0] :
( sQ318_spl
<=> ( line_equal(X0,a1b1)
| ~ incident(ab,X0)
| ~ incident(b1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f2285,plain,
! [X0] :
( ~ sQ318_spl
| line_equal(X0,a1b1)
| ~ incident(ab,X0)
| ~ incident(b1,X0) ),
inference(component_clause,[status(thm)],[f2284]) ).
fof(f2302,plain,
! [X0] :
( line_equal(X0,a2c2)
| point_equal(c2,ac)
| ~ incident(ac,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f431,f70]) ).
fof(f2312,definition,
! [X0] :
( sQ323_spl
<=> ( line_equal(X0,a2c2)
| ~ incident(ac,X0)
| ~ incident(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f2313,plain,
! [X0] :
( ~ sQ323_spl
| line_equal(X0,a2c2)
| ~ incident(ac,X0)
| ~ incident(c2,X0) ),
inference(component_clause,[status(thm)],[f2312]) ).
fof(f2315,definition,
( sQ324_spl
<=> point_equal(c2,ac) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f2316,plain,
( ~ sQ324_spl
| point_equal(c2,ac) ),
inference(component_clause,[status(thm)],[f2315]) ).
fof(f2318,plain,
( sQ324_spl
| sQ323_spl ),
inference(split_clause,[status(thm)],[f2302,f2312,f2315]) ).
fof(f2366,plain,
( ~ sQ175_spl
| line_equal(b1c1,a2b2) ),
inference(resolution,[status(thm)],[f1257,f120]) ).
fof(f2367,plain,
( ~ sQ175_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f2366,f1215,f1256]) ).
fof(f2368,plain,
( ~ sQ166_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f2121,f146,f1215]) ).
fof(f2373,plain,
! [X0] :
( line_equal(X0,b2c2)
| point_equal(c2,bc)
| ~ incident(bc,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f433,f73]) ).
fof(f2374,plain,
! [X0] :
( line_equal(X0,b2c2)
| point_equal(b2,bc)
| ~ incident(bc,X0)
| ~ incident(b2,X0) ),
inference(resolution,[status(thm)],[f433,f74]) ).
fof(f2383,definition,
! [X0] :
( sQ335_spl
<=> ( line_equal(X0,b2c2)
| ~ incident(bc,X0)
| ~ incident(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f2384,plain,
! [X0] :
( ~ sQ335_spl
| line_equal(X0,b2c2)
| ~ incident(bc,X0)
| ~ incident(c2,X0) ),
inference(component_clause,[status(thm)],[f2383]) ).
fof(f2386,definition,
( sQ336_spl
<=> point_equal(c2,bc) ),
introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition]) ).
fof(f2387,plain,
( ~ sQ336_spl
| point_equal(c2,bc) ),
inference(component_clause,[status(thm)],[f2386]) ).
fof(f2389,plain,
( sQ336_spl
| sQ335_spl ),
inference(split_clause,[status(thm)],[f2373,f2383,f2386]) ).
fof(f2390,definition,
! [X0] :
( sQ337_spl
<=> ( line_equal(X0,b2c2)
| ~ incident(bc,X0)
| ~ incident(b2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f2391,plain,
! [X0] :
( ~ sQ337_spl
| line_equal(X0,b2c2)
| ~ incident(bc,X0)
| ~ incident(b2,X0) ),
inference(component_clause,[status(thm)],[f2390]) ).
fof(f2393,definition,
( sQ338_spl
<=> point_equal(b2,bc) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f2394,plain,
( ~ sQ338_spl
| point_equal(b2,bc) ),
inference(component_clause,[status(thm)],[f2393]) ).
fof(f2396,plain,
( sQ338_spl
| sQ337_spl ),
inference(split_clause,[status(thm)],[f2374,f2390,f2393]) ).
fof(f2418,definition,
! [X0] :
( sQ342_spl
<=> ( line_equal(X0,b1c1)
| ~ incident(bc,X0)
| ~ incident(c1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition]) ).
fof(f2419,plain,
! [X0] :
( ~ sQ342_spl
| line_equal(X0,b1c1)
| ~ incident(bc,X0)
| ~ incident(c1,X0) ),
inference(component_clause,[status(thm)],[f2418]) ).
fof(f2441,plain,
( ~ sQ238_spl
| incident(a2,b1c1) ),
inference(resolution,[status(thm)],[f1547,f304]) ).
fof(f2445,plain,
( ~ sQ238_spl
| line_equal(b1c1,a2c2) ),
inference(resolution,[status(thm)],[f1547,f120]) ).
fof(f2448,plain,
! [X0] :
( line_equal(X0,oc)
| point_equal(c2,o)
| ~ incident(o,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f435,f83]) ).
fof(f2458,definition,
! [X0] :
( sQ349_spl
<=> ( line_equal(X0,oc)
| ~ incident(o,X0)
| ~ incident(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f2459,plain,
! [X0] :
( ~ sQ349_spl
| line_equal(X0,oc)
| ~ incident(o,X0)
| ~ incident(c2,X0) ),
inference(component_clause,[status(thm)],[f2458]) ).
fof(f2461,definition,
( sQ350_spl
<=> point_equal(c2,o) ),
introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition]) ).
fof(f2462,plain,
( ~ sQ350_spl
| point_equal(c2,o) ),
inference(component_clause,[status(thm)],[f2461]) ).
fof(f2464,plain,
( sQ350_spl
| sQ349_spl ),
inference(split_clause,[status(thm)],[f2448,f2458,f2461]) ).
fof(f2478,plain,
! [X0] :
( line_equal(X0,ob)
| point_equal(b1,o)
| ~ incident(o,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f436,f80]) ).
fof(f2487,definition,
! [X0] :
( sQ354_spl
<=> ( line_equal(X0,ob)
| ~ incident(o,X0)
| ~ incident(b2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition]) ).
fof(f2488,plain,
! [X0] :
( ~ sQ354_spl
| line_equal(X0,ob)
| ~ incident(o,X0)
| ~ incident(b2,X0) ),
inference(component_clause,[status(thm)],[f2487]) ).
fof(f2494,definition,
! [X0] :
( sQ356_spl
<=> ( line_equal(X0,ob)
| ~ incident(o,X0)
| ~ incident(b1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f2495,plain,
! [X0] :
( ~ sQ356_spl
| line_equal(X0,ob)
| ~ incident(o,X0)
| ~ incident(b1,X0) ),
inference(component_clause,[status(thm)],[f2494]) ).
fof(f2497,definition,
( sQ357_spl
<=> point_equal(b1,o) ),
introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition]) ).
fof(f2498,plain,
( ~ sQ357_spl
| point_equal(b1,o) ),
inference(component_clause,[status(thm)],[f2497]) ).
fof(f2500,plain,
( sQ357_spl
| sQ356_spl ),
inference(split_clause,[status(thm)],[f2478,f2494,f2497]) ).
fof(f2506,plain,
! [X0] :
( line_equal(X0,oa)
| point_equal(a2,o)
| ~ incident(o,X0)
| ~ incident(a2,X0) ),
inference(resolution,[status(thm)],[f437,f79]) ).
fof(f2516,definition,
! [X0] :
( sQ359_spl
<=> ( line_equal(X0,oa)
| ~ incident(o,X0)
| ~ incident(a2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f2517,plain,
! [X0] :
( ~ sQ359_spl
| line_equal(X0,oa)
| ~ incident(o,X0)
| ~ incident(a2,X0) ),
inference(component_clause,[status(thm)],[f2516]) ).
fof(f2519,definition,
( sQ360_spl
<=> point_equal(a2,o) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f2520,plain,
( ~ sQ360_spl
| point_equal(a2,o) ),
inference(component_clause,[status(thm)],[f2519]) ).
fof(f2522,plain,
( sQ360_spl
| sQ359_spl ),
inference(split_clause,[status(thm)],[f2506,f2516,f2519]) ).
fof(f2540,definition,
( sQ363_spl
<=> point_equal(o,c2) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f2541,plain,
( ~ sQ363_spl
| point_equal(o,c2) ),
inference(component_clause,[status(thm)],[f2540]) ).
fof(f2549,definition,
! [X0] :
( sQ365_spl
<=> ( line_equal(X0,oc)
| ~ incident(c2,X0)
| ~ incident(c1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition]) ).
fof(f2550,plain,
! [X0] :
( ~ sQ365_spl
| line_equal(X0,oc)
| ~ incident(c2,X0)
| ~ incident(c1,X0) ),
inference(component_clause,[status(thm)],[f2549]) ).
fof(f2560,plain,
( ~ sQ149_spl
| incident(ab,b1c1) ),
inference(resolution,[status(thm)],[f1141,f279]) ).
fof(f2563,plain,
( ~ sQ149_spl
| point_equal(b1,ab) ),
inference(resolution,[status(thm)],[f1141,f112]) ).
fof(f2564,plain,
( ~ sQ270_spl
| incident(a1,b2c2) ),
inference(resolution,[status(thm)],[f1829,f311]) ).
fof(f2565,plain,
( ~ sQ270_spl
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[f1829,f299]) ).
fof(f2569,plain,
( ~ sQ270_spl
| sQ212_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2565,f1427]) ).
fof(f2570,plain,
( ~ sQ270_spl
| sQ212_spl ),
inference(contradiction_clause,[status(thm)],[f2569]) ).
fof(f2571,plain,
( ~ sQ152_spl
| incident(a1,b2c2) ),
inference(resolution,[status(thm)],[f1156,f312]) ).
fof(f2688,plain,
( ~ sQ215_spl
| incident(bc,a1b1) ),
inference(resolution,[status(thm)],[f1436,f280]) ).
fof(f2753,plain,
! [X0] :
( line_equal(X0,b2c2)
| point_equal(bc,c2)
| ~ incident(c2,X0)
| ~ incident(bc,X0) ),
inference(resolution,[status(thm)],[f439,f85]) ).
fof(f2758,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(a1b1,b2c2)
| point_equal(X0,c2)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f439,f157]) ).
fof(f2762,definition,
( sQ372_spl
<=> point_equal(bc,c2) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f2763,plain,
( ~ sQ372_spl
| point_equal(bc,c2) ),
inference(component_clause,[status(thm)],[f2762]) ).
fof(f2765,plain,
( sQ372_spl
| sQ335_spl ),
inference(split_clause,[status(thm)],[f2753,f2383,f2762]) ).
fof(f2771,definition,
! [X0] :
( sQ374_spl
<=> ( line_equal(X0,b2c2)
| ~ incident(c2,X0)
| ~ incident(b2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition]) ).
fof(f2772,plain,
! [X0] :
( ~ sQ374_spl
| line_equal(X0,b2c2)
| ~ incident(c2,X0)
| ~ incident(b2,X0) ),
inference(component_clause,[status(thm)],[f2771]) ).
fof(f2781,definition,
( sQ377_spl
<=> point_equal(a1,c2) ),
introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition]) ).
fof(f2782,plain,
( ~ sQ377_spl
| point_equal(a1,c2) ),
inference(component_clause,[status(thm)],[f2781]) ).
fof(f2785,plain,
( ~ sQ7_spl
| sQ152_spl
| sQ262_spl ),
inference(split_clause,[status(thm)],[f2758,f1747,f1155,f156]) ).
fof(f2821,plain,
( ~ sQ158_spl
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[f1182,f309]) ).
fof(f2827,plain,
( ~ sQ278_spl
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[f1896,f308]) ).
fof(f2828,plain,
( ~ sQ278_spl
| incident(c1,a2c2) ),
inference(resolution,[status(thm)],[f1896,f298]) ).
fof(f2829,plain,
( ~ sQ278_spl
| incident(bc,a2c2) ),
inference(resolution,[status(thm)],[f1896,f289]) ).
fof(f2832,plain,
( ~ sQ278_spl
| sQ184_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2828,f1301]) ).
fof(f2833,plain,
( ~ sQ278_spl
| sQ184_spl ),
inference(contradiction_clause,[status(thm)],[f2832]) ).
fof(f2834,plain,
! [X0] :
( line_equal(X0,a2c2)
| point_equal(ac,c2)
| ~ incident(c2,X0)
| ~ incident(ac,X0) ),
inference(resolution,[status(thm)],[f440,f87]) ).
fof(f2837,plain,
! [X0] :
( line_equal(X0,a2c2)
| point_equal(a2,c2)
| ~ incident(c2,X0)
| ~ incident(a2,X0) ),
inference(resolution,[status(thm)],[f440,f69]) ).
fof(f2842,definition,
( sQ378_spl
<=> point_equal(ac,c2) ),
introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition]) ).
fof(f2843,plain,
( ~ sQ378_spl
| point_equal(ac,c2) ),
inference(component_clause,[status(thm)],[f2842]) ).
fof(f2845,plain,
( sQ378_spl
| sQ323_spl ),
inference(split_clause,[status(thm)],[f2834,f2312,f2842]) ).
fof(f2851,definition,
! [X0] :
( sQ380_spl
<=> ( line_equal(X0,a2c2)
| ~ incident(c2,X0)
| ~ incident(a2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition]) ).
fof(f2852,plain,
! [X0] :
( ~ sQ380_spl
| line_equal(X0,a2c2)
| ~ incident(c2,X0)
| ~ incident(a2,X0) ),
inference(component_clause,[status(thm)],[f2851]) ).
fof(f2854,definition,
( sQ381_spl
<=> point_equal(a2,c2) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f2855,plain,
( ~ sQ381_spl
| point_equal(a2,c2) ),
inference(component_clause,[status(thm)],[f2854]) ).
fof(f2857,plain,
( sQ381_spl
| sQ380_spl ),
inference(split_clause,[status(thm)],[f2837,f2851,f2854]) ).
fof(f2861,definition,
( sQ383_spl
<=> point_equal(b1,c2) ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f2862,plain,
( ~ sQ383_spl
| point_equal(b1,c2) ),
inference(component_clause,[status(thm)],[f2861]) ).
fof(f2869,plain,
! [X0] :
( line_equal(X0,oc)
| point_equal(c2,c1)
| ~ incident(c1,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f442,f83]) ).
fof(f2875,definition,
( sQ384_spl
<=> point_equal(o,c1) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f2876,plain,
( ~ sQ384_spl
| point_equal(o,c1) ),
inference(component_clause,[status(thm)],[f2875]) ).
fof(f2879,plain,
( sQ12_spl
| sQ365_spl ),
inference(split_clause,[status(thm)],[f2869,f2549,f179]) ).
fof(f2888,plain,
! [X0] :
( line_equal(X0,b1c1)
| point_equal(bc,c1)
| ~ incident(c1,X0)
| ~ incident(bc,X0) ),
inference(resolution,[status(thm)],[f443,f84]) ).
fof(f2892,plain,
! [X0] :
( line_equal(X0,b1c1)
| point_equal(b1,c1)
| ~ incident(c1,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f443,f72]) ).
fof(f2896,plain,
( sQ213_spl
| sQ342_spl ),
inference(split_clause,[status(thm)],[f2888,f2418,f1428]) ).
fof(f2902,definition,
! [X0] :
( sQ387_spl
<=> ( line_equal(X0,b1c1)
| ~ incident(c1,X0)
| ~ incident(a2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f2903,plain,
! [X0] :
( ~ sQ387_spl
| line_equal(X0,b1c1)
| ~ incident(c1,X0)
| ~ incident(a2,X0) ),
inference(component_clause,[status(thm)],[f2902]) ).
fof(f2905,definition,
( sQ388_spl
<=> point_equal(a2,c1) ),
introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition]) ).
fof(f2906,plain,
( ~ sQ388_spl
| point_equal(a2,c1) ),
inference(component_clause,[status(thm)],[f2905]) ).
fof(f2909,definition,
! [X0] :
( sQ389_spl
<=> ( line_equal(X0,b1c1)
| ~ incident(c1,X0)
| ~ incident(b1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f2910,plain,
! [X0] :
( ~ sQ389_spl
| line_equal(X0,b1c1)
| ~ incident(c1,X0)
| ~ incident(b1,X0) ),
inference(component_clause,[status(thm)],[f2909]) ).
fof(f2912,definition,
( sQ390_spl
<=> point_equal(b1,c1) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f2913,plain,
( ~ sQ390_spl
| point_equal(b1,c1) ),
inference(component_clause,[status(thm)],[f2912]) ).
fof(f2915,plain,
( sQ390_spl
| sQ389_spl ),
inference(split_clause,[status(thm)],[f2892,f2909,f2912]) ).
fof(f2923,plain,
! [X0] :
( line_equal(X0,a1c1)
| point_equal(a1,c1)
| ~ incident(c1,X0)
| ~ incident(a1,X0) ),
inference(resolution,[status(thm)],[f444,f67]) ).
fof(f2940,definition,
! [X0] :
( sQ394_spl
<=> ( line_equal(X0,a1c1)
| ~ incident(c1,X0)
| ~ incident(a1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition]) ).
fof(f2941,plain,
! [X0] :
( ~ sQ394_spl
| line_equal(X0,a1c1)
| ~ incident(c1,X0)
| ~ incident(a1,X0) ),
inference(component_clause,[status(thm)],[f2940]) ).
fof(f2943,definition,
( sQ395_spl
<=> point_equal(a1,c1) ),
introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition]) ).
fof(f2944,plain,
( ~ sQ395_spl
| point_equal(a1,c1) ),
inference(component_clause,[status(thm)],[f2943]) ).
fof(f2946,plain,
( sQ395_spl
| sQ394_spl ),
inference(split_clause,[status(thm)],[f2923,f2940,f2943]) ).
fof(f2950,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(a1b1,a2c2)
| point_equal(X0,c2)
| ~ incident(X0,a2c2)
| ~ incident(X0,a1b1) ),
inference(resolution,[status(thm)],[f157,f440]) ).
fof(f2972,plain,
( ~ sQ7_spl
| sQ158_spl
| sQ264_spl ),
inference(split_clause,[status(thm)],[f2950,f1761,f1181,f156]) ).
fof(f3051,plain,
! [X0] :
( line_equal(X0,ob)
| point_equal(o,b2)
| ~ incident(b2,X0)
| ~ incident(o,X0) ),
inference(resolution,[status(thm)],[f445,f76]) ).
fof(f3059,definition,
( sQ396_spl
<=> point_equal(o,b2) ),
introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition]) ).
fof(f3060,plain,
( ~ sQ396_spl
| point_equal(o,b2) ),
inference(component_clause,[status(thm)],[f3059]) ).
fof(f3062,plain,
( sQ396_spl
| sQ354_spl ),
inference(split_clause,[status(thm)],[f3051,f2487,f3059]) ).
fof(f3068,definition,
! [X0] :
( sQ398_spl
<=> ( line_equal(X0,ob)
| ~ incident(b2,X0)
| ~ incident(b1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ398_spl])],[split_symbol_definition]) ).
fof(f3069,plain,
! [X0] :
( ~ sQ398_spl
| line_equal(X0,ob)
| ~ incident(b2,X0)
| ~ incident(b1,X0) ),
inference(component_clause,[status(thm)],[f3068]) ).
fof(f3071,definition,
( sQ399_spl
<=> point_equal(b1,b2) ),
introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition]) ).
fof(f3072,plain,
( ~ sQ399_spl
| point_equal(b1,b2) ),
inference(component_clause,[status(thm)],[f3071]) ).
fof(f3079,plain,
( ~ sQ158_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2821,f143,f1181]) ).
fof(f3143,definition,
( sQ409_spl
<=> incident(c2,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition]) ).
fof(f3149,plain,
( ~ sQ278_spl
| sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2829,f748]) ).
fof(f3150,plain,
( ~ sQ278_spl
| sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f3149]) ).
fof(f3151,plain,
( ~ sQ278_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2827,f143,f1895]) ).
fof(f3190,definition,
( sQ414_spl
<=> incident(ab,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition]) ).
fof(f3205,definition,
( sQ418_spl
<=> incident(ac,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f3207,plain,
( sQ418_spl
| ~ incident(ac,b2c2) ),
inference(component_clause,[status(thm)],[f3205]) ).
fof(f3212,definition,
( sQ420_spl
<=> incident(ac,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f3214,plain,
( sQ420_spl
| ~ incident(ac,b1c1) ),
inference(component_clause,[status(thm)],[f3212]) ).
fof(f3218,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f84]) ).
fof(f3219,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f3218]) ).
fof(f3318,plain,
! [X0] :
( line_equal(X0,b2c2)
| point_equal(c2,b2)
| ~ incident(b2,X0)
| ~ incident(c2,X0) ),
inference(resolution,[status(thm)],[f446,f73]) ).
fof(f3329,definition,
( sQ422_spl
<=> point_equal(c2,b2) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f3330,plain,
( ~ sQ422_spl
| point_equal(c2,b2) ),
inference(component_clause,[status(thm)],[f3329]) ).
fof(f3332,plain,
( sQ422_spl
| sQ374_spl ),
inference(split_clause,[status(thm)],[f3318,f2771,f3329]) ).
fof(f3341,definition,
( sQ425_spl
<=> point_equal(a1,b2) ),
introduced(definition,[new_symbols(definition,[sQ425_spl])],[split_symbol_definition]) ).
fof(f3342,plain,
( ~ sQ425_spl
| point_equal(a1,b2) ),
inference(component_clause,[status(thm)],[f3341]) ).
fof(f3348,plain,
! [X0] :
( line_equal(X0,a2b2)
| point_equal(ab,b2)
| ~ incident(b2,X0)
| ~ incident(ab,X0) ),
inference(resolution,[status(thm)],[f447,f89]) ).
fof(f3351,plain,
! [X0] :
( line_equal(X0,a2b2)
| point_equal(a2,b2)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(resolution,[status(thm)],[f447,f65]) ).
fof(f3355,definition,
( sQ426_spl
<=> point_equal(ab,b2) ),
introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition]) ).
fof(f3356,plain,
( ~ sQ426_spl
| point_equal(ab,b2) ),
inference(component_clause,[status(thm)],[f3355]) ).
fof(f3358,plain,
( sQ426_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f3348,f2257,f3355]) ).
fof(f3364,definition,
! [X0] :
( sQ428_spl
<=> ( line_equal(X0,a2b2)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f3365,plain,
! [X0] :
( ~ sQ428_spl
| line_equal(X0,a2b2)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(component_clause,[status(thm)],[f3364]) ).
fof(f3367,definition,
( sQ429_spl
<=> point_equal(a2,b2) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f3368,plain,
( ~ sQ429_spl
| point_equal(a2,b2) ),
inference(component_clause,[status(thm)],[f3367]) ).
fof(f3370,plain,
( sQ429_spl
| sQ428_spl ),
inference(split_clause,[status(thm)],[f3351,f3364,f3367]) ).
fof(f3396,definition,
! [X0] :
( sQ432_spl
<=> ( line_equal(X0,oa)
| ~ incident(a2,X0)
| ~ incident(a1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f3397,plain,
! [X0] :
( ~ sQ432_spl
| line_equal(X0,oa)
| ~ incident(a2,X0)
| ~ incident(a1,X0) ),
inference(component_clause,[status(thm)],[f3396]) ).
fof(f3411,plain,
! [X0] :
( ~ sQ3_spl
| line_equal(X0,a2c2)
| point_equal(b1,a2)
| ~ incident(a2,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f449,f144]) ).
fof(f3420,definition,
( sQ435_spl
<=> point_equal(c2,a2) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f3421,plain,
( ~ sQ435_spl
| point_equal(c2,a2) ),
inference(component_clause,[status(thm)],[f3420]) ).
fof(f3429,definition,
! [X0] :
( sQ437_spl
<=> ( line_equal(X0,a2c2)
| ~ incident(a2,X0)
| ~ incident(b1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f3432,definition,
( sQ438_spl
<=> point_equal(b1,a2) ),
introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition]) ).
fof(f3433,plain,
( ~ sQ438_spl
| point_equal(b1,a2) ),
inference(component_clause,[status(thm)],[f3432]) ).
fof(f3435,plain,
( ~ sQ3_spl
| sQ438_spl
| sQ437_spl ),
inference(split_clause,[status(thm)],[f3411,f3429,f3432,f143]) ).
fof(f3446,plain,
( ~ sQ0_spl
| ~ sQ149_spl
| ~ incident(ac,b1c1)
| ~ incident(bc,b1c1) ),
inference(resolution,[status(thm)],[f2560,f741]) ).
fof(f3449,plain,
( ~ sQ126_spl
| ~ sQ149_spl
| point_equal(bc,ab)
| ~ incident(ab,b2c2) ),
inference(resolution,[status(thm)],[f2560,f1032]) ).
fof(f3478,plain,
( ~ sQ0_spl
| ~ sQ149_spl
| ~ sQ420_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f3446,f502,f3212,f1140,f133]) ).
fof(f3482,definition,
( sQ444_spl
<=> point_equal(ab,c1) ),
introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition]) ).
fof(f3483,plain,
( ~ sQ444_spl
| point_equal(ab,c1) ),
inference(component_clause,[status(thm)],[f3482]) ).
fof(f3489,definition,
( sQ446_spl
<=> point_equal(ab,bc) ),
introduced(definition,[new_symbols(definition,[sQ446_spl])],[split_symbol_definition]) ).
fof(f3490,plain,
( ~ sQ446_spl
| point_equal(ab,bc) ),
inference(component_clause,[status(thm)],[f3489]) ).
fof(f3493,definition,
( sQ447_spl
<=> incident(ab,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ447_spl])],[split_symbol_definition]) ).
fof(f3496,definition,
( sQ448_spl
<=> point_equal(bc,ab) ),
introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition]) ).
fof(f3497,plain,
( ~ sQ448_spl
| point_equal(bc,ab) ),
inference(component_clause,[status(thm)],[f3496]) ).
fof(f3499,plain,
( ~ sQ126_spl
| ~ sQ149_spl
| sQ448_spl
| ~ sQ447_spl ),
inference(split_clause,[status(thm)],[f3449,f3493,f3496,f1140,f1031]) ).
fof(f3570,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(oc,a2b2)
| point_equal(X0,c1)
| ~ incident(X0,a2b2)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f147,f398]) ).
fof(f3592,plain,
( ~ sQ4_spl
| sQ164_spl
| sQ265_spl ),
inference(split_clause,[status(thm)],[f3570,f1773,f1208,f146]) ).
fof(f3600,definition,
( sQ460_spl
<=> point_equal(c1,b2) ),
introduced(definition,[new_symbols(definition,[sQ460_spl])],[split_symbol_definition]) ).
fof(f3601,plain,
( ~ sQ460_spl
| point_equal(c1,b2) ),
inference(component_clause,[status(thm)],[f3600]) ).
fof(f3604,definition,
! [X0] :
( sQ461_spl
<=> ( line_equal(X0,a2b2)
| ~ incident(ab,X0)
| ~ incident(c1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ461_spl])],[split_symbol_definition]) ).
fof(f3605,plain,
! [X0] :
( ~ sQ461_spl
| line_equal(X0,a2b2)
| ~ incident(ab,X0)
| ~ incident(c1,X0) ),
inference(component_clause,[status(thm)],[f3604]) ).
fof(f3646,plain,
( ~ sQ149_spl
| incident(b1,a2b2) ),
inference(resolution,[status(thm)],[f2563,f255]) ).
fof(f3651,plain,
( ~ sQ213_spl
| incident(bc,oc) ),
inference(resolution,[status(thm)],[f1429,f268]) ).
fof(f3656,plain,
! [X0] :
( line_equal(X0,ob)
| point_equal(b2,b1)
| ~ incident(b1,X0)
| ~ incident(b2,X0) ),
inference(resolution,[status(thm)],[f452,f81]) ).
fof(f3666,definition,
( sQ469_spl
<=> point_equal(o,b1) ),
introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition]) ).
fof(f3667,plain,
( ~ sQ469_spl
| point_equal(o,b1) ),
inference(component_clause,[status(thm)],[f3666]) ).
fof(f3670,plain,
( sQ11_spl
| sQ398_spl ),
inference(split_clause,[status(thm)],[f3656,f3068,f175]) ).
fof(f3704,plain,
! [X0] :
( line_equal(X0,a1b1)
| point_equal(ab,b1)
| ~ incident(b1,X0)
| ~ incident(ab,X0) ),
inference(resolution,[status(thm)],[f454,f88]) ).
fof(f3708,plain,
! [X0] :
( line_equal(X0,a1b1)
| point_equal(a1,b1)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(resolution,[status(thm)],[f454,f63]) ).
fof(f3712,plain,
( sQ149_spl
| sQ318_spl ),
inference(split_clause,[status(thm)],[f3704,f2284,f1140]) ).
fof(f3713,definition,
! [X0] :
( sQ474_spl
<=> ( line_equal(X0,a1b1)
| ~ incident(b1,X0)
| ~ incident(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition]) ).
fof(f3714,plain,
! [X0] :
( ~ sQ474_spl
| line_equal(X0,a1b1)
| ~ incident(b1,X0)
| ~ incident(c2,X0) ),
inference(component_clause,[status(thm)],[f3713]) ).
fof(f3716,definition,
( sQ475_spl
<=> point_equal(c2,b1) ),
introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition]) ).
fof(f3717,plain,
( ~ sQ475_spl
| point_equal(c2,b1) ),
inference(component_clause,[status(thm)],[f3716]) ).
fof(f3725,definition,
! [X0] :
( sQ477_spl
<=> ( line_equal(X0,a1b1)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ477_spl])],[split_symbol_definition]) ).
fof(f3726,plain,
! [X0] :
( ~ sQ477_spl
| line_equal(X0,a1b1)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(component_clause,[status(thm)],[f3725]) ).
fof(f3728,definition,
( sQ478_spl
<=> point_equal(a1,b1) ),
introduced(definition,[new_symbols(definition,[sQ478_spl])],[split_symbol_definition]) ).
fof(f3729,plain,
( ~ sQ478_spl
| point_equal(a1,b1) ),
inference(component_clause,[status(thm)],[f3728]) ).
fof(f3731,plain,
( sQ478_spl
| sQ477_spl ),
inference(split_clause,[status(thm)],[f3708,f3725,f3728]) ).
fof(f3736,plain,
! [X0] :
( line_equal(X0,oa)
| point_equal(a2,a1)
| ~ incident(a1,X0)
| ~ incident(a2,X0) ),
inference(resolution,[status(thm)],[f455,f79]) ).
fof(f3747,plain,
( sQ10_spl
| sQ432_spl ),
inference(split_clause,[status(thm)],[f3736,f3396,f171]) ).
fof(f3789,definition,
! [X0] :
( sQ483_spl
<=> ( line_equal(X0,a1b1)
| ~ incident(a1,X0)
| ~ incident(c2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ483_spl])],[split_symbol_definition]) ).
fof(f3790,plain,
! [X0] :
( ~ sQ483_spl
| line_equal(X0,a1b1)
| ~ incident(a1,X0)
| ~ incident(c2,X0) ),
inference(component_clause,[status(thm)],[f3789]) ).
fof(f3792,definition,
( sQ484_spl
<=> point_equal(c2,a1) ),
introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition]) ).
fof(f3793,plain,
( ~ sQ484_spl
| point_equal(c2,a1) ),
inference(component_clause,[status(thm)],[f3792]) ).
fof(f3812,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(X0,a1b1)
| point_equal(b1,c2)
| ~ incident(c2,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f858,f64]) ).
fof(f3813,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(X0,a1b1)
| point_equal(a1,c2)
| ~ incident(c2,X0)
| ~ incident(a1,X0) ),
inference(resolution,[status(thm)],[f858,f63]) ).
fof(f3824,plain,
( ~ sQ7_spl
| sQ383_spl
| sQ474_spl ),
inference(split_clause,[status(thm)],[f3812,f3713,f2861,f156]) ).
fof(f3825,plain,
( ~ sQ7_spl
| sQ377_spl
| sQ483_spl ),
inference(split_clause,[status(thm)],[f3813,f3789,f2781,f156]) ).
fof(f3851,plain,
( ~ sQ118_spl
| ~ sQ215_spl
| point_equal(ab,bc)
| ~ incident(bc,a2b2) ),
inference(resolution,[status(thm)],[f2688,f991]) ).
fof(f3899,plain,
( ~ sQ118_spl
| ~ sQ215_spl
| sQ446_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f3851,f760,f3489,f1435,f990]) ).
fof(f3904,plain,
( ~ sQ185_spl
| incident(ac,b1c1) ),
inference(resolution,[status(thm)],[f1303,f269]) ).
fof(f3909,plain,
! [X0] :
( ~ sQ7_spl
| line_equal(oc,a1b1)
| point_equal(c2,X0)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f862,f83]) ).
fof(f3916,plain,
( ~ sQ7_spl
| sQ259_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f3909,f1105,f1730,f156]) ).
fof(f3920,plain,
( ~ sQ152_spl
| incident(b1,b2c2) ),
inference(resolution,[status(thm)],[f1156,f309]) ).
fof(f4070,plain,
! [X0] :
( ~ sQ4_spl
| line_equal(X0,a2b2)
| point_equal(ab,c1)
| ~ incident(c1,X0)
| ~ incident(ab,X0) ),
inference(resolution,[status(thm)],[f441,f89]) ).
fof(f4079,plain,
( ~ sQ4_spl
| sQ444_spl
| sQ461_spl ),
inference(split_clause,[status(thm)],[f4070,f3604,f3482,f146]) ).
fof(f4096,plain,
( ~ sQ172_spl
| incident(b1,oc) ),
inference(resolution,[status(thm)],[f1242,f308]) ).
fof(f4098,plain,
( ~ sQ172_spl
| incident(bc,oc) ),
inference(resolution,[status(thm)],[f1242,f289]) ).
fof(f4103,plain,
( ~ sQ176_spl
| incident(o,b1c1) ),
inference(resolution,[status(thm)],[f1261,f290]) ).
fof(f4105,plain,
( ~ sQ176_spl
| line_equal(b1c1,oc) ),
inference(resolution,[status(thm)],[f1261,f120]) ).
fof(f4193,plain,
( ~ sQ182_spl
| incident(b1,a1c1) ),
inference(resolution,[status(thm)],[f1288,f308]) ).
fof(f4198,plain,
( ~ sQ182_spl
| sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4193,f813]) ).
fof(f4199,plain,
( ~ sQ182_spl
| sQ107_spl ),
inference(contradiction_clause,[status(thm)],[f4198]) ).
fof(f4201,plain,
( ~ sQ226_spl
| incident(c1,a1b1) ),
inference(resolution,[status(thm)],[f1486,f298]) ).
fof(f4205,plain,
( ~ sQ226_spl
| sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4201,f794]) ).
fof(f4206,plain,
( ~ sQ226_spl
| sQ102_spl ),
inference(contradiction_clause,[status(thm)],[f4205]) ).
fof(f4207,plain,
( ~ sQ224_spl
| incident(a1,b1c1) ),
inference(resolution,[status(thm)],[f1475,f312]) ).
fof(f4212,plain,
( ~ sQ224_spl
| sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4207,f790]) ).
fof(f4213,plain,
( ~ sQ224_spl
| sQ101_spl ),
inference(contradiction_clause,[status(thm)],[f4212]) ).
fof(f4215,plain,
! [X0] :
( ~ sQ6_spl
| line_equal(a1c1,b2c2)
| point_equal(X0,b2)
| ~ incident(X0,b2c2)
| ~ incident(X0,a1c1) ),
inference(resolution,[status(thm)],[f154,f446]) ).
fof(f4239,plain,
( ~ sQ6_spl
| sQ270_spl
| sQ289_spl ),
inference(split_clause,[status(thm)],[f4215,f1969,f1828,f153]) ).
fof(f4248,definition,
! [X0] :
( sQ519_spl
<=> ( line_equal(X0,a1c1)
| ~ incident(a1,X0)
| ~ incident(b2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition]) ).
fof(f4251,definition,
( sQ520_spl
<=> point_equal(b2,a1) ),
introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition]) ).
fof(f4252,plain,
( ~ sQ520_spl
| point_equal(b2,a1) ),
inference(component_clause,[status(thm)],[f4251]) ).
fof(f4262,plain,
( ~ sQ270_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2564,f140,f1828]) ).
fof(f4265,plain,
( ~ sQ225_spl
| incident(b2,a1b1) ),
inference(resolution,[status(thm)],[f1482,f300]) ).
fof(f4297,plain,
( ~ sQ426_spl
| incident(ab,b2c2) ),
inference(resolution,[status(thm)],[f3356,f272]) ).
fof(f4398,plain,
( ~ sQ446_spl
| incident(ab,b1c1) ),
inference(resolution,[status(thm)],[f3490,f260]) ).
fof(f4403,plain,
( ~ sQ448_spl
| incident(bc,a2b2) ),
inference(resolution,[status(thm)],[f3497,f255]) ).
fof(f4406,plain,
( ~ sQ448_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f4403,f760,f3496]) ).
fof(f4407,plain,
( ~ sQ7_spl
| ~ sQ372_spl
| incident(bc,a1b1) ),
inference(resolution,[status(thm)],[f2763,f1573]) ).
fof(f4408,plain,
( ~ sQ372_spl
| incident(bc,a2c2) ),
inference(resolution,[status(thm)],[f2763,f266]) ).
fof(f4410,plain,
( ~ sQ372_spl
| incident(bc,oc) ),
inference(resolution,[status(thm)],[f2763,f264]) ).
fof(f4414,plain,
( ~ sQ383_spl
| incident(b1,a2c2) ),
inference(resolution,[status(thm)],[f2862,f266]) ).
fof(f4416,plain,
( ~ sQ383_spl
| incident(b1,oc) ),
inference(resolution,[status(thm)],[f2862,f264]) ).
fof(f4419,plain,
( ~ sQ383_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f4414,f143,f2861]) ).
fof(f4424,plain,
( ~ sQ399_spl
| point_equal(b2,b1) ),
inference(resolution,[status(thm)],[f3072,f112]) ).
fof(f4425,plain,
( ~ sQ399_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4424,f177]) ).
fof(f4426,plain,
( ~ sQ399_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f4425]) ).
fof(f4468,plain,
( ~ sQ187_spl
| incident(ac,a1b1) ),
inference(resolution,[status(thm)],[f1310,f283]) ).
fof(f4474,plain,
( ~ sQ444_spl
| incident(ab,a1c1) ),
inference(resolution,[status(thm)],[f3483,f270]) ).
fof(f4479,plain,
( ~ sQ444_spl
| sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4474,f758]) ).
fof(f4480,plain,
( ~ sQ444_spl
| sQ94_spl ),
inference(contradiction_clause,[status(thm)],[f4479]) ).
fof(f4481,plain,
! [X0] :
( ~ sQ172_spl
| line_equal(oc,a1b1)
| point_equal(X0,b1)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f4096,f454]) ).
fof(f4487,plain,
! [X0] :
( ~ sQ172_spl
| line_equal(oc,a1b1)
| point_equal(b1,X0)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ),
inference(resolution,[status(thm)],[f4096,f364]) ).
fof(f4490,plain,
( ~ sQ8_spl
| ~ sQ172_spl
| ~ incident(c1,oc)
| ~ incident(a1,oc) ),
inference(resolution,[status(thm)],[f4096,f164]) ).
fof(f4491,plain,
! [X0] :
( ~ sQ172_spl
| line_equal(X0,oc)
| point_equal(b1,c1)
| ~ incident(c1,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f4096,f442]) ).
fof(f4504,definition,
! [X0] :
( sQ521_spl
<=> ( point_equal(X0,b1)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition]) ).
fof(f4507,plain,
( ~ sQ172_spl
| sQ259_spl
| sQ521_spl ),
inference(split_clause,[status(thm)],[f4481,f4504,f1730,f1241]) ).
fof(f4519,definition,
! [X0] :
( sQ524_spl
<=> ( point_equal(b1,X0)
| ~ incident(X0,a1b1)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[sQ524_spl])],[split_symbol_definition]) ).
fof(f4522,plain,
( ~ sQ172_spl
| sQ259_spl
| sQ524_spl ),
inference(split_clause,[status(thm)],[f4487,f4519,f1730,f1241]) ).
fof(f4531,plain,
( ~ sQ8_spl
| ~ sQ172_spl
| ~ sQ43_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f4490,f803,f552,f1241,f163]) ).
fof(f4532,definition,
! [X0] :
( sQ527_spl
<=> ( line_equal(X0,oc)
| ~ incident(c1,X0)
| ~ incident(b1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ527_spl])],[split_symbol_definition]) ).
fof(f4535,plain,
( ~ sQ172_spl
| sQ390_spl
| sQ527_spl ),
inference(split_clause,[status(thm)],[f4491,f4532,f2912,f1241]) ).
fof(f4551,plain,
! [X0] :
( ~ sQ6_spl
| line_equal(X0,a1c1)
| point_equal(a1,b2)
| ~ incident(b2,X0)
| ~ incident(a1,X0) ),
inference(resolution,[status(thm)],[f1812,f67]) ).
fof(f4563,plain,
( ~ sQ6_spl
| sQ425_spl
| sQ519_spl ),
inference(split_clause,[status(thm)],[f4551,f4248,f3341,f153]) ).
fof(f4595,plain,
( ~ sQ118_spl
| ~ sQ225_spl
| point_equal(ab,b2)
| ~ incident(b2,a2b2) ),
inference(resolution,[status(thm)],[f4265,f991]) ).
fof(f4655,plain,
( ~ sQ118_spl
| ~ sQ225_spl
| sQ426_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f4595,f575,f3355,f1481,f990]) ).
fof(f4677,plain,
( ~ sQ0_spl
| ~ sQ426_spl
| ~ incident(ac,b2c2)
| ~ incident(bc,b2c2) ),
inference(resolution,[status(thm)],[f4297,f741]) ).
fof(f4709,plain,
( ~ sQ0_spl
| ~ sQ426_spl
| ~ sQ418_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f4677,f492,f3205,f3355,f133]) ).
fof(f4727,plain,
( ~ sQ192_spl
| incident(a2,ob) ),
inference(resolution,[status(thm)],[f1331,f305]) ).
fof(f4735,plain,
( ~ sQ390_spl
| incident(b1,a1c1) ),
inference(resolution,[status(thm)],[f2913,f270]) ).
fof(f4740,plain,
( ~ sQ390_spl
| sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4735,f813]) ).
fof(f4741,plain,
( ~ sQ390_spl
| sQ107_spl ),
inference(contradiction_clause,[status(thm)],[f4740]) ).
fof(f4742,plain,
( ~ sQ438_spl
| incident(b1,a2b2) ),
inference(resolution,[status(thm)],[f3433,f276]) ).
fof(f4787,plain,
( ~ sQ7_spl
| ~ sQ372_spl
| sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4407,f769]) ).
fof(f4788,plain,
( ~ sQ7_spl
| ~ sQ372_spl
| sQ97_spl ),
inference(contradiction_clause,[status(thm)],[f4787]) ).
fof(f4789,plain,
( ~ sQ4_spl
| ~ sQ213_spl
| incident(bc,a2b2) ),
inference(resolution,[status(thm)],[f1429,f267]) ).
fof(f4790,plain,
( ~ sQ213_spl
| incident(bc,a1c1) ),
inference(resolution,[status(thm)],[f1429,f270]) ).
fof(f4795,plain,
( ~ sQ4_spl
| ~ sQ213_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f4789,f760,f1428,f146]) ).
fof(f4796,plain,
( ~ sQ213_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f4790,f753,f1428]) ).
fof(f4855,plain,
( ~ sQ132_spl
| point_equal(o,c2)
| ~ incident(c2,oa) ),
inference(resolution,[status(thm)],[f1062,f83]) ).
fof(f4856,plain,
( ~ sQ132_spl
| point_equal(o,c1)
| ~ incident(c1,oa) ),
inference(resolution,[status(thm)],[f1062,f82]) ).
fof(f4858,definition,
( sQ559_spl
<=> incident(c2,oa) ),
introduced(definition,[new_symbols(definition,[sQ559_spl])],[split_symbol_definition]) ).
fof(f4860,plain,
( sQ559_spl
| ~ incident(c2,oa) ),
inference(component_clause,[status(thm)],[f4858]) ).
fof(f4861,plain,
( ~ sQ132_spl
| sQ363_spl
| ~ sQ559_spl ),
inference(split_clause,[status(thm)],[f4855,f4858,f2540,f1061]) ).
fof(f4862,definition,
( sQ560_spl
<=> incident(c1,oa) ),
introduced(definition,[new_symbols(definition,[sQ560_spl])],[split_symbol_definition]) ).
fof(f4864,plain,
( sQ560_spl
| ~ incident(c1,oa) ),
inference(component_clause,[status(thm)],[f4862]) ).
fof(f4865,plain,
( ~ sQ132_spl
| sQ384_spl
| ~ sQ560_spl ),
inference(split_clause,[status(thm)],[f4856,f4862,f2875,f1061]) ).
fof(f4866,plain,
( ~ sQ176_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f4105,f1241,f1260]) ).
fof(f4868,plain,
( ~ sQ136_spl
| point_equal(o,o)
| ~ incident(o,oa) ),
inference(resolution,[status(thm)],[f1080,f76]) ).
fof(f4878,plain,
( ~ sQ136_spl
| sQ32_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f4868,f526,f512,f1079]) ).
fof(f4883,definition,
( sQ564_spl
<=> incident(b1,oa) ),
introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition]) ).
fof(f4885,plain,
( sQ564_spl
| ~ incident(b1,oa) ),
inference(component_clause,[status(thm)],[f4883]) ).
fof(f4887,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f528,f75]) ).
fof(f4888,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f4887]) ).
fof(f4891,plain,
( ~ sQ146_spl
| point_equal(c2,a2)
| ~ incident(a2,oc) ),
inference(resolution,[status(thm)],[f1124,f69]) ).
fof(f4897,plain,
( ~ sQ146_spl
| sQ435_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f4891,f840,f3420,f1123]) ).
fof(f4898,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f535,f83]) ).
fof(f4899,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f4898]) ).
fof(f4900,plain,
( ~ sQ144_spl
| point_equal(c2,bc)
| ~ incident(bc,oc) ),
inference(resolution,[status(thm)],[f1117,f85]) ).
fof(f4902,plain,
( ~ sQ144_spl
| point_equal(c2,b2)
| ~ incident(b2,oc) ),
inference(resolution,[status(thm)],[f1117,f74]) ).
fof(f4903,definition,
( sQ566_spl
<=> incident(bc,oc) ),
introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition]) ).
fof(f4905,plain,
( sQ566_spl
| ~ incident(bc,oc) ),
inference(component_clause,[status(thm)],[f4903]) ).
fof(f4906,plain,
( ~ sQ144_spl
| sQ336_spl
| ~ sQ566_spl ),
inference(split_clause,[status(thm)],[f4900,f4903,f2386,f1116]) ).
fof(f4908,plain,
( ~ sQ144_spl
| sQ422_spl
| ~ sQ113_spl ),
inference(split_clause,[status(thm)],[f4902,f843,f3329,f1116]) ).
fof(f4973,plain,
( ~ sQ187_spl
| sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4468,f772]) ).
fof(f4974,plain,
( ~ sQ187_spl
| sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f4973]) ).
fof(f4975,plain,
( ~ sQ259_spl
| incident(c1,a1b1) ),
inference(resolution,[status(thm)],[f1731,f297]) ).
fof(f4980,plain,
( ~ sQ259_spl
| sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4975,f794]) ).
fof(f4981,plain,
( ~ sQ259_spl
| sQ102_spl ),
inference(contradiction_clause,[status(thm)],[f4980]) ).
fof(f4983,plain,
( ~ sQ155_spl
| point_equal(c2,c2)
| ~ incident(c2,b2c2) ),
inference(resolution,[status(thm)],[f1168,f70]) ).
fof(f4986,plain,
( ~ sQ155_spl
| sQ39_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f4983,f540,f536,f1167]) ).
fof(f4996,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f554,f82]) ).
fof(f4997,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f4996]) ).
fof(f5004,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f566,f81]) ).
fof(f5005,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f5004]) ).
fof(f5008,plain,
( ~ sQ195_spl
| point_equal(b2,b2)
| ~ incident(b2,b2c2) ),
inference(resolution,[status(thm)],[f1346,f66]) ).
fof(f5010,plain,
( ~ sQ149_spl
| ~ sQ195_spl
| point_equal(b2,b1)
| ~ incident(b1,b2c2) ),
inference(resolution,[status(thm)],[f1346,f3646]) ).
fof(f5013,plain,
( ~ sQ195_spl
| sQ47_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f5008,f571,f567,f1345]) ).
fof(f5015,plain,
( ~ sQ149_spl
| ~ sQ195_spl
| sQ11_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f5010,f1432,f175,f1345,f1140]) ).
fof(f5016,plain,
( ~ sQ168_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f2093,f146,f1222]) ).
fof(f5017,plain,
( ~ sQ119_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1660,f193]) ).
fof(f5018,plain,
( ~ sQ119_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f5017]) ).
fof(f5019,plain,
( ~ sQ185_spl
| sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3904,f3214]) ).
fof(f5020,plain,
( ~ sQ185_spl
| sQ420_spl ),
inference(contradiction_clause,[status(thm)],[f5019]) ).
fof(f5021,plain,
( ~ sQ248_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f1789,f1155,f1632]) ).
fof(f5024,plain,
( ~ sQ152_spl
| sQ214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3920,f1434]) ).
fof(f5025,plain,
( ~ sQ152_spl
| sQ214_spl ),
inference(contradiction_clause,[status(thm)],[f5024]) ).
fof(f5027,plain,
( ~ sQ236_spl
| sQ158_spl ),
inference(split_clause,[status(thm)],[f1796,f1181,f1539]) ).
fof(f5028,plain,
( ~ sQ438_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f4742,f799,f3432]) ).
fof(f5029,plain,
( ~ sQ446_spl
| sQ414_spl ),
inference(split_clause,[status(thm)],[f4398,f3190,f3489]) ).
fof(f5031,plain,
( ~ sQ134_spl
| incident(c2,ob) ),
inference(resolution,[status(thm)],[f1072,f293]) ).
fof(f5035,plain,
( ~ sQ134_spl
| sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5031,f830]) ).
fof(f5036,plain,
( ~ sQ134_spl
| sQ109_spl ),
inference(contradiction_clause,[status(thm)],[f5035]) ).
fof(f5119,plain,
( ~ sQ142_spl
| incident(a1,oc) ),
inference(resolution,[status(thm)],[f1109,f312]) ).
fof(f5120,plain,
( ~ sQ142_spl
| incident(b1,oc) ),
inference(resolution,[status(thm)],[f1109,f309]) ).
fof(f5124,plain,
( ~ sQ142_spl
| sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5119,f805]) ).
fof(f5125,plain,
( ~ sQ142_spl
| sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f5124]) ).
fof(f5127,plain,
( ~ sQ131_spl
| incident(b2,oc) ),
inference(resolution,[status(thm)],[f1058,f300]) ).
fof(f5131,plain,
( ~ sQ131_spl
| sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5127,f845]) ).
fof(f5132,plain,
( ~ sQ131_spl
| sQ113_spl ),
inference(contradiction_clause,[status(thm)],[f5131]) ).
fof(f5177,plain,
( ~ sQ250_spl
| incident(c1,a1b1) ),
inference(resolution,[status(thm)],[f1641,f299]) ).
fof(f5181,plain,
( ~ sQ250_spl
| sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5177,f794]) ).
fof(f5182,plain,
( ~ sQ250_spl
| sQ102_spl ),
inference(contradiction_clause,[status(thm)],[f5181]) ).
fof(f5184,plain,
( ~ sQ246_spl
| incident(b1,a1c1) ),
inference(resolution,[status(thm)],[f1622,f309]) ).
fof(f5188,plain,
( ~ sQ246_spl
| sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5184,f813]) ).
fof(f5189,plain,
( ~ sQ246_spl
| sQ107_spl ),
inference(contradiction_clause,[status(thm)],[f5188]) ).
fof(f5232,plain,
( ~ sQ195_spl
| ~ sQ95_spl
| point_equal(b2,bc)
| ~ incident(bc,b2c2) ),
inference(resolution,[status(thm)],[f761,f1346]) ).
fof(f5252,plain,
( ~ sQ195_spl
| ~ sQ95_spl
| sQ338_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f5232,f492,f2393,f760,f1345]) ).
fof(f5280,plain,
( ~ sQ196_spl
| incident(a2,b2c2) ),
inference(resolution,[status(thm)],[f1349,f305]) ).
fof(f5285,plain,
( ~ sQ196_spl
| sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5280,f834]) ).
fof(f5286,plain,
( ~ sQ196_spl
| sQ110_spl ),
inference(contradiction_clause,[status(thm)],[f5285]) ).
fof(f5291,plain,
( ~ sQ127_spl
| line_equal(b1c1,b2c2) ),
inference(resolution,[status(thm)],[f1038,f120]) ).
fof(f5292,plain,
( ~ sQ127_spl
| sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5291,f185]) ).
fof(f5293,plain,
( ~ sQ127_spl
| sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f5292]) ).
fof(f5295,plain,
( ~ sQ148_spl
| incident(ab,a2c2) ),
inference(resolution,[status(thm)],[f1137,f266]) ).
fof(f5300,plain,
( ~ sQ148_spl
| sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5295,f751]) ).
fof(f5301,plain,
( ~ sQ148_spl
| sQ92_spl ),
inference(contradiction_clause,[status(thm)],[f5300]) ).
fof(f5354,plain,
( ~ sQ180_spl
| incident(a2,a1c1) ),
inference(resolution,[status(thm)],[f1280,f305]) ).
fof(f5358,plain,
( ~ sQ180_spl
| line_equal(a1c1,a2b2) ),
inference(resolution,[status(thm)],[f1280,f120]) ).
fof(f5359,plain,
( ~ sQ180_spl
| sQ273_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5354,f1841]) ).
fof(f5360,plain,
( ~ sQ180_spl
| sQ273_spl ),
inference(contradiction_clause,[status(thm)],[f5359]) ).
fof(f5361,plain,
( ~ sQ180_spl
| sQ168_spl ),
inference(split_clause,[status(thm)],[f5358,f1222,f1279]) ).
fof(f5362,plain,
( ~ sQ168_spl
| sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2094,f765]) ).
fof(f5363,plain,
( ~ sQ168_spl
| sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f5362]) ).
fof(f5367,plain,
( ~ sQ190_spl
| incident(c2,ob) ),
inference(resolution,[status(thm)],[f1324,f294]) ).
fof(f5370,plain,
( ~ sQ190_spl
| line_equal(ob,b2c2) ),
inference(resolution,[status(thm)],[f1324,f120]) ).
fof(f5371,plain,
( ~ sQ190_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f5370,f1337,f1323]) ).
fof(f5373,plain,
( ~ sQ179_spl
| incident(a1,b1c1) ),
inference(resolution,[status(thm)],[f1272,f311]) ).
fof(f5378,plain,
( ~ sQ179_spl
| sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5373,f790]) ).
fof(f5379,plain,
( ~ sQ179_spl
| sQ101_spl ),
inference(contradiction_clause,[status(thm)],[f5378]) ).
fof(f5380,plain,
( ~ sQ133_spl
| incident(a1,oc) ),
inference(resolution,[status(thm)],[f1065,f310]) ).
fof(f5381,plain,
( ~ sQ133_spl
| incident(a2,oc) ),
inference(resolution,[status(thm)],[f1065,f303]) ).
fof(f5385,plain,
( ~ sQ133_spl
| sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5380,f805]) ).
fof(f5386,plain,
( ~ sQ133_spl
| sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f5385]) ).
fof(f5391,plain,
( ~ sQ138_spl
| line_equal(oa,oc) ),
inference(resolution,[status(thm)],[f1090,f120]) ).
fof(f5392,plain,
( ~ sQ138_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f5391,f1064,f1089]) ).
fof(f5393,plain,
( ~ sQ133_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f5381,f840,f1064]) ).
fof(f5475,plain,
( ~ sQ384_spl
| incident(o,a1c1) ),
inference(resolution,[status(thm)],[f2876,f270]) ).
fof(f5476,plain,
( ~ sQ384_spl
| incident(o,b1c1) ),
inference(resolution,[status(thm)],[f2876,f269]) ).
fof(f5481,plain,
( ~ sQ363_spl
| incident(o,a2c2) ),
inference(resolution,[status(thm)],[f2541,f266]) ).
fof(f5482,plain,
( ~ sQ363_spl
| incident(o,b2c2) ),
inference(resolution,[status(thm)],[f2541,f265]) ).
fof(f5487,plain,
( ~ sQ396_spl
| incident(o,a2b2) ),
inference(resolution,[status(thm)],[f3060,f273]) ).
fof(f5496,plain,
( ~ sQ469_spl
| point_equal(b1,o) ),
inference(resolution,[status(thm)],[f3667,f112]) ).
fof(f5497,plain,
( ~ sQ147_spl
| incident(a2,oc) ),
inference(resolution,[status(thm)],[f1127,f304]) ).
fof(f5502,plain,
( ~ sQ147_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f5497,f840,f1126]) ).
fof(f5503,plain,
( ~ sQ159_spl
| incident(c1,a2c2) ),
inference(resolution,[status(thm)],[f1186,f297]) ).
fof(f5505,plain,
( ~ sQ159_spl
| incident(o,a2c2) ),
inference(resolution,[status(thm)],[f1186,f290]) ).
fof(f5508,plain,
( ~ sQ159_spl
| sQ184_spl ),
inference(split_clause,[status(thm)],[f5503,f1299,f1185]) ).
fof(f5510,plain,
( ~ sQ324_spl
| incident(c2,a1c1) ),
inference(resolution,[status(thm)],[f2316,f258]) ).
fof(f5514,plain,
( ~ sQ324_spl
| sQ274_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5510,f1844]) ).
fof(f5515,plain,
( ~ sQ324_spl
| sQ274_spl ),
inference(contradiction_clause,[status(thm)],[f5514]) ).
fof(f5583,plain,
( ~ sQ336_spl
| point_equal(bc,c2) ),
inference(resolution,[status(thm)],[f2387,f112]) ).
fof(f5584,plain,
( ~ sQ336_spl
| sQ372_spl ),
inference(split_clause,[status(thm)],[f5583,f2762,f2386]) ).
fof(f5585,plain,
( ~ sQ145_spl
| incident(b2,oc) ),
inference(resolution,[status(thm)],[f1120,f301]) ).
fof(f5589,plain,
( ~ sQ145_spl
| line_equal(oc,b2c2) ),
inference(resolution,[status(thm)],[f1120,f120]) ).
fof(f5600,plain,
( ~ sQ195_spl
| ~ sQ103_spl
| point_equal(b2,a1)
| ~ incident(a1,b2c2) ),
inference(resolution,[status(thm)],[f797,f1346]) ).
fof(f5645,plain,
( ~ sQ195_spl
| ~ sQ103_spl
| sQ520_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f5600,f140,f4251,f796,f1345]) ).
fof(f5734,plain,
( ~ sQ153_spl
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[f1160,f297]) ).
fof(f5736,plain,
( ~ sQ153_spl
| incident(o,b2c2) ),
inference(resolution,[status(thm)],[f1160,f290]) ).
fof(f5739,plain,
( ~ sQ153_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f5734,f1425,f1159]) ).
fof(f5740,plain,
( ~ sQ372_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f4408,f746,f2762]) ).
fof(f5742,plain,
( ~ sQ422_spl
| incident(c2,a2b2) ),
inference(resolution,[status(thm)],[f3330,f273]) ).
fof(f5747,plain,
( ~ sQ422_spl
| sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5742,f838]) ).
fof(f5748,plain,
( ~ sQ422_spl
| sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f5747]) ).
fof(f5750,plain,
( ~ sQ164_spl
| incident(c2,a2b2) ),
inference(resolution,[status(thm)],[f1209,f293]) ).
fof(f5754,plain,
( ~ sQ164_spl
| sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5750,f838]) ).
fof(f5755,plain,
( ~ sQ164_spl
| sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f5754]) ).
fof(f5791,plain,
! [X0] :
( ~ sQ91_spl
| line_equal(a2c2,b1c1)
| point_equal(X0,bc)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f747,f434]) ).
fof(f5792,plain,
! [X0] :
( ~ sQ91_spl
| line_equal(a2c2,b2c2)
| point_equal(X0,bc)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f747,f433]) ).
fof(f5795,plain,
! [X0] :
( ~ sQ91_spl
| line_equal(a2c2,b1c1)
| point_equal(bc,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f747,f324]) ).
fof(f5796,plain,
! [X0] :
( ~ sQ91_spl
| line_equal(a2c2,b2c2)
| point_equal(bc,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f747,f322]) ).
fof(f5810,definition,
! [X0] :
( sQ616_spl
<=> ( point_equal(X0,bc)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition]) ).
fof(f5813,plain,
( ~ sQ91_spl
| sQ238_spl
| sQ616_spl ),
inference(split_clause,[status(thm)],[f5791,f5810,f1546,f746]) ).
fof(f5814,definition,
! [X0] :
( sQ617_spl
<=> ( point_equal(X0,bc)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition]) ).
fof(f5817,plain,
( ~ sQ91_spl
| sQ156_spl
| sQ617_spl ),
inference(split_clause,[status(thm)],[f5792,f5814,f1170,f746]) ).
fof(f5820,definition,
! [X0] :
( sQ618_spl
<=> ( point_equal(bc,X0)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition]) ).
fof(f5823,plain,
( ~ sQ91_spl
| sQ238_spl
| sQ618_spl ),
inference(split_clause,[status(thm)],[f5795,f5820,f1546,f746]) ).
fof(f5824,definition,
! [X0] :
( sQ619_spl
<=> ( point_equal(bc,X0)
| ~ incident(X0,b2c2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition]) ).
fof(f5827,plain,
( ~ sQ91_spl
| sQ156_spl
| sQ619_spl ),
inference(split_clause,[status(thm)],[f5796,f5824,f1170,f746]) ).
fof(f5844,plain,
( ~ sQ201_spl
| point_equal(a2,c2)
| ~ incident(c2,oa) ),
inference(resolution,[status(thm)],[f1375,f70]) ).
fof(f5850,plain,
( ~ sQ201_spl
| sQ381_spl
| ~ sQ559_spl ),
inference(split_clause,[status(thm)],[f5844,f4858,f2854,f1374]) ).
fof(f5866,plain,
( ~ sQ156_spl
| incident(a2,b2c2) ),
inference(resolution,[status(thm)],[f1171,f304]) ).
fof(f5871,plain,
( ~ sQ156_spl
| sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5866,f834]) ).
fof(f5872,plain,
( ~ sQ156_spl
| sQ110_spl ),
inference(contradiction_clause,[status(thm)],[f5871]) ).
fof(f5873,plain,
( ~ sQ160_spl
| incident(b2,a2c2) ),
inference(resolution,[status(thm)],[f1190,f301]) ).
fof(f5878,plain,
( ~ sQ160_spl
| sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5873,f850]) ).
fof(f5879,plain,
( ~ sQ160_spl
| sQ114_spl ),
inference(contradiction_clause,[status(thm)],[f5878]) ).
fof(f5882,plain,
( ~ sQ460_spl
| incident(c1,b2c2) ),
inference(resolution,[status(thm)],[f3601,f272]) ).
fof(f5883,plain,
( ~ sQ460_spl
| incident(c1,ob) ),
inference(resolution,[status(thm)],[f3601,f271]) ).
fof(f5886,plain,
( ~ sQ460_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f5882,f1425,f3600]) ).
fof(f5887,plain,
( ~ sQ460_spl
| sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5883,f786]) ).
fof(f5888,plain,
( ~ sQ460_spl
| sQ100_spl ),
inference(contradiction_clause,[status(thm)],[f5887]) ).
fof(f5915,plain,
( ~ sQ257_spl
| point_equal(b1,o)
| ~ incident(b1,oa) ),
inference(resolution,[status(thm)],[f1712,f80]) ).
fof(f5918,plain,
( ~ sQ257_spl
| sQ357_spl
| ~ sQ564_spl ),
inference(split_clause,[status(thm)],[f5915,f4883,f2497,f1711]) ).
fof(f5920,plain,
( ~ sQ256_spl
| point_equal(c2,o)
| ~ incident(c2,oa) ),
inference(resolution,[status(thm)],[f1698,f83]) ).
fof(f5923,plain,
( ~ sQ256_spl
| sQ350_spl
| ~ sQ559_spl ),
inference(split_clause,[status(thm)],[f5920,f4858,f2461,f1697]) ).
fof(f5973,plain,
( ~ sQ190_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f5367,f828,f1323]) ).
fof(f5974,plain,
( ~ sQ338_spl
| incident(b2,b1c1) ),
inference(resolution,[status(thm)],[f2394,f260]) ).
fof(f6113,plain,
( ~ sQ6_spl
| ~ sQ313_spl
| line_equal(a1c1,a2b2)
| ~ incident(ab,a1c1) ),
inference(resolution,[status(thm)],[f2258,f154]) ).
fof(f6117,plain,
( ~ sQ6_spl
| ~ sQ313_spl
| sQ168_spl
| ~ sQ94_spl ),
inference(split_clause,[status(thm)],[f6113,f756,f1222,f2257,f153]) ).
fof(f6121,plain,
( ~ sQ7_spl
| ~ sQ323_spl
| line_equal(a1b1,a2c2)
| ~ incident(ac,a1b1) ),
inference(resolution,[status(thm)],[f2313,f157]) ).
fof(f6125,plain,
( ~ sQ7_spl
| ~ sQ323_spl
| sQ158_spl
| ~ sQ98_spl ),
inference(split_clause,[status(thm)],[f6121,f770,f1181,f2312,f156]) ).
fof(f6140,plain,
( ~ sQ337_spl
| line_equal(a2b2,b2c2)
| ~ incident(bc,a2b2) ),
inference(resolution,[status(thm)],[f2391,f66]) ).
fof(f6144,plain,
( ~ sQ337_spl
| sQ196_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f6140,f760,f1348,f2390]) ).
fof(f6146,plain,
( ~ sQ342_spl
| line_equal(oc,b1c1)
| ~ incident(bc,oc) ),
inference(resolution,[status(thm)],[f2419,f82]) ).
fof(f6150,plain,
( ~ sQ342_spl
| sQ176_spl
| ~ sQ566_spl ),
inference(split_clause,[status(thm)],[f6146,f4903,f1260,f2418]) ).
fof(f6156,plain,
( ~ sQ426_spl
| sQ447_spl ),
inference(split_clause,[status(thm)],[f4297,f3493,f3355]) ).
fof(f6158,plain,
( ~ sQ238_spl
| sQ278_spl ),
inference(split_clause,[status(thm)],[f2445,f1895,f1546]) ).
fof(f6160,plain,
( ~ sQ238_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2441,f150,f1546]) ).
fof(f6239,definition,
( sQ634_spl
<=> incident(o,a2b2) ),
introduced(definition,[new_symbols(definition,[sQ634_spl])],[split_symbol_definition]) ).
fof(f6241,plain,
( sQ634_spl
| ~ incident(o,a2b2) ),
inference(component_clause,[status(thm)],[f6239]) ).
fof(f6244,definition,
( sQ635_spl
<=> incident(o,b1c1) ),
introduced(definition,[new_symbols(definition,[sQ635_spl])],[split_symbol_definition]) ).
fof(f6246,plain,
( sQ635_spl
| ~ incident(o,b1c1) ),
inference(component_clause,[status(thm)],[f6244]) ).
fof(f6248,definition,
( sQ636_spl
<=> incident(o,a1c1) ),
introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition]) ).
fof(f6250,plain,
( sQ636_spl
| ~ incident(o,a1c1) ),
inference(component_clause,[status(thm)],[f6248]) ).
fof(f6253,plain,
( ~ sQ356_spl
| line_equal(b1c1,ob)
| ~ incident(o,b1c1) ),
inference(resolution,[status(thm)],[f2495,f72]) ).
fof(f6256,plain,
( ~ sQ356_spl
| sQ218_spl
| ~ sQ635_spl ),
inference(split_clause,[status(thm)],[f6253,f6244,f1449,f2494]) ).
fof(f6257,definition,
( sQ637_spl
<=> incident(o,a1b1) ),
introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition]) ).
fof(f6261,plain,
( ~ sQ6_spl
| ~ sQ354_spl
| line_equal(a1c1,ob)
| ~ incident(o,a1c1) ),
inference(resolution,[status(thm)],[f2488,f154]) ).
fof(f6263,plain,
( ~ sQ354_spl
| line_equal(b2c2,ob)
| ~ incident(o,b2c2) ),
inference(resolution,[status(thm)],[f2488,f74]) ).
fof(f6265,plain,
( ~ sQ6_spl
| ~ sQ354_spl
| sQ272_spl
| ~ sQ636_spl ),
inference(split_clause,[status(thm)],[f6261,f6248,f1835,f2487,f153]) ).
fof(f6267,definition,
( sQ638_spl
<=> incident(o,b2c2) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f6269,plain,
( sQ638_spl
| ~ incident(o,b2c2) ),
inference(component_clause,[status(thm)],[f6267]) ).
fof(f6270,plain,
( ~ sQ354_spl
| sQ190_spl
| ~ sQ638_spl ),
inference(split_clause,[status(thm)],[f6263,f6267,f1323,f2487]) ).
fof(f6282,plain,
( ~ sQ359_spl
| line_equal(a2c2,oa)
| ~ incident(o,a2c2) ),
inference(resolution,[status(thm)],[f2517,f69]) ).
fof(f6283,plain,
( ~ sQ359_spl
| line_equal(a2b2,oa)
| ~ incident(o,a2b2) ),
inference(resolution,[status(thm)],[f2517,f65]) ).
fof(f6286,definition,
( sQ639_spl
<=> incident(o,a2c2) ),
introduced(definition,[new_symbols(definition,[sQ639_spl])],[split_symbol_definition]) ).
fof(f6288,plain,
( sQ639_spl
| ~ incident(o,a2c2) ),
inference(component_clause,[status(thm)],[f6286]) ).
fof(f6289,plain,
( ~ sQ359_spl
| sQ202_spl
| ~ sQ639_spl ),
inference(split_clause,[status(thm)],[f6282,f6286,f1377,f2516]) ).
fof(f6290,plain,
( ~ sQ359_spl
| sQ204_spl
| ~ sQ634_spl ),
inference(split_clause,[status(thm)],[f6283,f6239,f1384,f2516]) ).
fof(f6292,plain,
( ~ sQ365_spl
| line_equal(oc,oc)
| ~ incident(c1,oc) ),
inference(resolution,[status(thm)],[f2550,f83]) ).
fof(f6293,plain,
( ~ sQ365_spl
| line_equal(b2c2,oc)
| ~ incident(c1,b2c2) ),
inference(resolution,[status(thm)],[f2550,f73]) ).
fof(f6294,plain,
( ~ sQ365_spl
| line_equal(a2c2,oc)
| ~ incident(c1,a2c2) ),
inference(resolution,[status(thm)],[f2550,f70]) ).
fof(f6296,plain,
( ~ sQ365_spl
| sQ33_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f6292,f552,f515,f2549]) ).
fof(f6297,plain,
( ~ sQ365_spl
| sQ145_spl
| ~ sQ212_spl ),
inference(split_clause,[status(thm)],[f6293,f1425,f1119,f2549]) ).
fof(f6298,plain,
( ~ sQ365_spl
| sQ147_spl
| ~ sQ184_spl ),
inference(split_clause,[status(thm)],[f6294,f1299,f1126,f2549]) ).
fof(f6301,plain,
( ~ sQ389_spl
| line_equal(b1c1,b1c1)
| ~ incident(b1,b1c1) ),
inference(resolution,[status(thm)],[f2910,f71]) ).
fof(f6305,plain,
( ~ sQ389_spl
| sQ30_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f6301,f602,f505,f2909]) ).
fof(f6308,plain,
( ~ sQ398_spl
| line_equal(ob,ob)
| ~ incident(b1,ob) ),
inference(resolution,[status(thm)],[f3069,f81]) ).
fof(f6309,plain,
( ~ sQ398_spl
| line_equal(b2c2,ob)
| ~ incident(b1,b2c2) ),
inference(resolution,[status(thm)],[f3069,f74]) ).
fof(f6310,plain,
( ~ sQ398_spl
| line_equal(a2b2,ob)
| ~ incident(b1,a2b2) ),
inference(resolution,[status(thm)],[f3069,f66]) ).
fof(f6312,plain,
( ~ sQ398_spl
| sQ35_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f6308,f598,f522,f3068]) ).
fof(f6313,plain,
( ~ sQ398_spl
| sQ190_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f6309,f1432,f1323,f3068]) ).
fof(f6314,plain,
( ~ sQ398_spl
| sQ192_spl
| ~ sQ104_spl ),
inference(split_clause,[status(thm)],[f6310,f799,f1330,f3068]) ).
fof(f6316,plain,
( ~ sQ428_spl
| line_equal(ob,a2b2)
| ~ incident(a2,ob) ),
inference(resolution,[status(thm)],[f3365,f81]) ).
fof(f6318,plain,
( ~ sQ428_spl
| line_equal(a2b2,a2b2)
| ~ incident(a2,a2b2) ),
inference(resolution,[status(thm)],[f3365,f66]) ).
fof(f6320,plain,
( ~ sQ428_spl
| sQ197_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f6316,f825,f1355,f3364]) ).
fof(f6322,plain,
( ~ sQ428_spl
| sQ18_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f6318,f590,f464,f3364]) ).
fof(f6323,plain,
( ~ sQ273_spl
| ~ sQ432_spl
| line_equal(a1c1,oa)
| ~ incident(a1,a1c1) ),
inference(resolution,[status(thm)],[f3397,f1840]) ).
fof(f6324,plain,
( ~ sQ432_spl
| line_equal(oa,oa)
| ~ incident(a1,oa) ),
inference(resolution,[status(thm)],[f3397,f79]) ).
fof(f6325,plain,
( ~ sQ432_spl
| line_equal(a2c2,oa)
| ~ incident(a1,a2c2) ),
inference(resolution,[status(thm)],[f3397,f69]) ).
fof(f6327,plain,
( ~ sQ273_spl
| ~ sQ432_spl
| sQ232_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f6323,f617,f1511,f3396,f1839]) ).
fof(f6328,plain,
( ~ sQ432_spl
| sQ37_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f6324,f610,f529,f3396]) ).
fof(f6329,plain,
( ~ sQ432_spl
| sQ202_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f6325,f1306,f1377,f3396]) ).
fof(f6334,plain,
( ~ sQ163_spl
| point_equal(c1,b2)
| ~ incident(b2,oc) ),
inference(resolution,[status(thm)],[f1206,f66]) ).
fof(f6343,plain,
( ~ sQ163_spl
| sQ460_spl
| ~ sQ113_spl ),
inference(split_clause,[status(thm)],[f6334,f843,f3600,f1205]) ).
fof(f6351,plain,
( ~ sQ103_spl
| ~ sQ265_spl
| point_equal(a1,c1)
| ~ incident(a1,oc) ),
inference(resolution,[status(thm)],[f1774,f797]) ).
fof(f6357,plain,
( ~ sQ103_spl
| ~ sQ265_spl
| sQ395_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f6351,f803,f2943,f1773,f796]) ).
fof(f6458,plain,
( ~ sQ461_spl
| line_equal(b1c1,a2b2)
| ~ incident(ab,b1c1) ),
inference(resolution,[status(thm)],[f3605,f71]) ).
fof(f6462,plain,
( ~ sQ461_spl
| sQ166_spl
| ~ sQ414_spl ),
inference(split_clause,[status(thm)],[f6458,f3190,f1215,f3604]) ).
fof(f6466,plain,
( ~ sQ477_spl
| line_equal(a1b1,a1b1)
| ~ incident(a1,a1b1) ),
inference(resolution,[status(thm)],[f3726,f64]) ).
fof(f6469,plain,
( ~ sQ477_spl
| sQ20_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f6466,f621,f471,f3725]) ).
fof(f6567,plain,
( ~ sQ208_spl
| incident(b2,a2c2) ),
inference(resolution,[status(thm)],[f1403,f302]) ).
fof(f6572,plain,
( ~ sQ208_spl
| sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6567,f850]) ).
fof(f6573,plain,
( ~ sQ208_spl
| sQ114_spl ),
inference(contradiction_clause,[status(thm)],[f6572]) ).
fof(f6584,plain,
( ~ sQ150_spl
| incident(ab,a1c1) ),
inference(resolution,[status(thm)],[f1145,f282]) ).
fof(f6588,plain,
( ~ sQ150_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f6584,f756,f1144]) ).
fof(f6598,plain,
( ~ sQ474_spl
| line_equal(oc,a1b1)
| ~ incident(b1,oc) ),
inference(resolution,[status(thm)],[f3714,f83]) ).
fof(f6602,plain,
( ~ sQ474_spl
| sQ259_spl
| ~ sQ106_spl ),
inference(split_clause,[status(thm)],[f6598,f806,f1730,f3713]) ).
fof(f6605,plain,
( ~ sQ142_spl
| sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5120,f808]) ).
fof(f6606,plain,
( ~ sQ142_spl
| sQ106_spl ),
inference(contradiction_clause,[status(thm)],[f6605]) ).
fof(f6607,plain,
( ~ sQ192_spl
| sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4727,f827]) ).
fof(f6608,plain,
( ~ sQ192_spl
| sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f6607]) ).
fof(f6653,plain,
( ~ sQ359_spl
| ~ sQ5_spl
| line_equal(b1c1,oa)
| ~ incident(o,b1c1) ),
inference(resolution,[status(thm)],[f151,f2517]) ).
fof(f6680,plain,
( ~ sQ359_spl
| ~ sQ5_spl
| sQ280_spl
| ~ sQ635_spl ),
inference(split_clause,[status(thm)],[f6653,f6244,f1902,f150,f2516]) ).
fof(f6692,definition,
! [X0] :
( sQ653_spl
<=> ( line_equal(X0,b1c1)
| ~ incident(b1,X0)
| ~ incident(a2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition]) ).
fof(f6693,plain,
! [X0] :
( ~ sQ653_spl
| line_equal(X0,b1c1)
| ~ incident(b1,X0)
| ~ incident(a2,X0) ),
inference(component_clause,[status(thm)],[f6692]) ).
fof(f6711,plain,
( ~ sQ474_spl
| ~ sQ109_spl
| line_equal(ob,a1b1)
| ~ incident(b1,ob) ),
inference(resolution,[status(thm)],[f829,f3714]) ).
fof(f6741,plain,
( ~ sQ474_spl
| ~ sQ109_spl
| sQ225_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f6711,f598,f1481,f828,f3713]) ).
fof(f6809,plain,
( ~ sQ204_spl
| line_equal(oa,a2b2) ),
inference(resolution,[status(thm)],[f1385,f120]) ).
fof(f6810,plain,
( ~ sQ209_spl
| incident(a1,a2b2) ),
inference(resolution,[status(thm)],[f1410,f310]) ).
fof(f6815,plain,
( ~ sQ209_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f6810,f796,f1409]) ).
fof(f6861,plain,
( ~ sQ425_spl
| incident(a1,b2c2) ),
inference(resolution,[status(thm)],[f3342,f272]) ).
fof(f6867,plain,
( ~ sQ520_spl
| incident(b2,a1c1) ),
inference(resolution,[status(thm)],[f4252,f282]) ).
fof(f6870,plain,
( ~ sQ520_spl
| point_equal(a1,b2) ),
inference(resolution,[status(thm)],[f4252,f112]) ).
fof(f6871,plain,
( ~ sQ520_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f6867,f153,f4251]) ).
fof(f6872,plain,
( ~ sQ520_spl
| sQ425_spl ),
inference(split_clause,[status(thm)],[f6870,f3341,f4251]) ).
fof(f6874,plain,
( ~ sQ395_spl
| incident(a1,b1c1) ),
inference(resolution,[status(thm)],[f2944,f269]) ).
fof(f6878,plain,
( ~ sQ395_spl
| sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6874,f790]) ).
fof(f6879,plain,
( ~ sQ395_spl
| sQ101_spl ),
inference(contradiction_clause,[status(thm)],[f6878]) ).
fof(f6882,plain,
( ~ sQ232_spl
| incident(c1,oa) ),
inference(resolution,[status(thm)],[f1512,f299]) ).
fof(f6886,plain,
( ~ sQ388_spl
| incident(a2,a1c1) ),
inference(resolution,[status(thm)],[f2906,f270]) ).
fof(f6891,plain,
( ~ sQ388_spl
| sQ273_spl ),
inference(split_clause,[status(thm)],[f6886,f1839,f2905]) ).
fof(f6893,plain,
( ~ sQ204_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f6809,f1409,f1384]) ).
fof(f6894,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f80]) ).
fof(f6895,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f6894]) ).
fof(f6896,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f612,f78]) ).
fof(f6897,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f6896]) ).
fof(f6898,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f546,f70]) ).
fof(f6899,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f6898]) ).
fof(f6900,plain,
( ~ sQ145_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f5585,f843,f1119]) ).
fof(f6901,plain,
( ~ sQ145_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f5589,f1159,f1119]) ).
fof(f6902,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f521,f76]) ).
fof(f6903,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f6902]) ).
fof(f6904,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f581,f79]) ).
fof(f6905,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f6904]) ).
fof(f6912,plain,
( ~ sQ429_spl
| incident(a2,b2c2) ),
inference(resolution,[status(thm)],[f3368,f272]) ).
fof(f6916,plain,
( ~ sQ429_spl
| sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6912,f834]) ).
fof(f6917,plain,
( ~ sQ429_spl
| sQ110_spl ),
inference(contradiction_clause,[status(thm)],[f6916]) ).
fof(f6918,plain,
( ~ sQ435_spl
| incident(c2,a2b2) ),
inference(resolution,[status(thm)],[f3421,f276]) ).
fof(f6923,plain,
( ~ sQ435_spl
| sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6918,f838]) ).
fof(f6924,plain,
( ~ sQ435_spl
| sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f6923]) ).
fof(f6927,plain,
( ~ sQ381_spl
| incident(a2,b2c2) ),
inference(resolution,[status(thm)],[f2855,f265]) ).
fof(f6932,plain,
( ~ sQ381_spl
| sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6927,f834]) ).
fof(f6933,plain,
( ~ sQ381_spl
| sQ110_spl ),
inference(contradiction_clause,[status(thm)],[f6932]) ).
fof(f6935,plain,
( ~ sQ202_spl
| incident(c2,oa) ),
inference(resolution,[status(thm)],[f1378,f295]) ).
fof(f6939,plain,
( ~ sQ205_spl
| incident(a1,a2c2) ),
inference(resolution,[status(thm)],[f1392,f310]) ).
fof(f6944,plain,
( ~ sQ205_spl
| sQ186_spl ),
inference(split_clause,[status(thm)],[f6939,f1306,f1391]) ).
fof(f6946,plain,
( ~ sQ218_spl
| incident(c1,ob) ),
inference(resolution,[status(thm)],[f1450,f298]) ).
fof(f6959,plain,
! [X0] :
( ~ sQ5_spl
| line_equal(X0,b1c1)
| point_equal(b1,a2)
| ~ incident(a2,X0)
| ~ incident(b1,X0) ),
inference(resolution,[status(thm)],[f1879,f72]) ).
fof(f6971,plain,
( ~ sQ5_spl
| sQ438_spl
| sQ653_spl ),
inference(split_clause,[status(thm)],[f6959,f6692,f3432,f150]) ).
fof(f7004,plain,
( ~ sQ357_spl
| incident(b1,oa) ),
inference(resolution,[status(thm)],[f2498,f263]) ).
fof(f7006,plain,
( ~ sQ357_spl
| incident(b1,oc) ),
inference(resolution,[status(thm)],[f2498,f261]) ).
fof(f7009,plain,
( ~ sQ357_spl
| sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7006,f808]) ).
fof(f7010,plain,
( ~ sQ357_spl
| sQ106_spl ),
inference(contradiction_clause,[status(thm)],[f7009]) ).
fof(f7015,plain,
( ~ sQ139_spl
| line_equal(oa,ob) ),
inference(resolution,[status(thm)],[f1094,f120]) ).
fof(f7094,plain,
( ~ sQ469_spl
| sQ357_spl ),
inference(split_clause,[status(thm)],[f5496,f2497,f3666]) ).
fof(f7152,plain,
( ~ sQ137_spl
| incident(a2,ob) ),
inference(resolution,[status(thm)],[f1083,f303]) ).
fof(f7156,plain,
( ~ sQ137_spl
| sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7152,f827]) ).
fof(f7157,plain,
( ~ sQ137_spl
| sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f7156]) ).
fof(f7158,plain,
( ~ sQ428_spl
| ~ sQ338_spl
| line_equal(b1c1,a2b2)
| ~ incident(a2,b1c1) ),
inference(resolution,[status(thm)],[f5974,f3365]) ).
fof(f7159,plain,
( ~ sQ398_spl
| ~ sQ338_spl
| line_equal(b1c1,ob)
| ~ incident(b1,b1c1) ),
inference(resolution,[status(thm)],[f5974,f3069]) ).
fof(f7186,plain,
( ~ sQ428_spl
| ~ sQ338_spl
| sQ166_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f7158,f150,f1215,f2393,f3364]) ).
fof(f7187,plain,
( ~ sQ398_spl
| ~ sQ338_spl
| sQ218_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f7159,f602,f1449,f2393,f3068]) ).
fof(f7237,plain,
( ~ sQ218_spl
| sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6946,f786]) ).
fof(f7238,plain,
( ~ sQ218_spl
| sQ100_spl ),
inference(contradiction_clause,[status(thm)],[f7237]) ).
fof(f7332,plain,
( ~ sQ174_spl
| incident(a1,oc) ),
inference(resolution,[status(thm)],[f1249,f311]) ).
fof(f7337,plain,
( ~ sQ174_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f7332,f803,f1248]) ).
fof(f7479,plain,
( ~ sQ478_spl
| incident(a1,b1c1) ),
inference(resolution,[status(thm)],[f3729,f279]) ).
fof(f7483,plain,
( ~ sQ478_spl
| sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7479,f790]) ).
fof(f7484,plain,
( ~ sQ478_spl
| sQ101_spl ),
inference(contradiction_clause,[status(thm)],[f7483]) ).
fof(f7573,plain,
( ~ sQ484_spl
| incident(c2,a1c1) ),
inference(resolution,[status(thm)],[f3793,f282]) ).
fof(f7578,plain,
( ~ sQ377_spl
| incident(a1,a2c2) ),
inference(resolution,[status(thm)],[f2782,f266]) ).
fof(f7579,plain,
( ~ sQ377_spl
| incident(a1,b2c2) ),
inference(resolution,[status(thm)],[f2782,f265]) ).
fof(f7583,plain,
( ~ sQ377_spl
| sQ186_spl ),
inference(split_clause,[status(thm)],[f7578,f1306,f2781]) ).
fof(f7584,plain,
( ~ sQ377_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f7579,f140,f2781]) ).
fof(f7587,plain,
( ~ sQ178_spl
| point_equal(c1,c1)
| ~ incident(c1,b1c1) ),
inference(resolution,[status(thm)],[f1269,f68]) ).
fof(f7591,plain,
( ~ sQ178_spl
| sQ42_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f7587,f556,f548,f1268]) ).
fof(f7603,plain,
( ~ sQ7_spl
| ~ sQ223_spl
| point_equal(b1,c2)
| ~ incident(c2,b1c1) ),
inference(resolution,[status(thm)],[f1472,f157]) ).
fof(f7604,plain,
( ~ sQ223_spl
| point_equal(b1,b1)
| ~ incident(b1,b1c1) ),
inference(resolution,[status(thm)],[f1472,f64]) ).
fof(f7607,plain,
( ~ sQ7_spl
| ~ sQ223_spl
| sQ383_spl
| ~ sQ409_spl ),
inference(split_clause,[status(thm)],[f7603,f3143,f2861,f1471,f156]) ).
fof(f7608,plain,
( ~ sQ223_spl
| sQ54_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f7604,f602,f594,f1471]) ).
fof(f7618,plain,
( ~ sQ172_spl
| sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4096,f808]) ).
fof(f7619,plain,
( ~ sQ172_spl
| sQ106_spl ),
inference(contradiction_clause,[status(thm)],[f7618]) ).
fof(f7620,plain,
( ~ sQ139_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f7015,f1082,f1093]) ).
fof(f7621,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f577,f66]) ).
fof(f7622,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f7621]) ).
fof(f7623,plain,
( ~ sQ425_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f6861,f140,f3341]) ).
fof(f7624,plain,
( ~ sQ152_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2571,f140,f1155]) ).
fof(f7832,plain,
( ~ sQ232_spl
| sQ560_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6882,f4864]) ).
fof(f7833,plain,
( ~ sQ232_spl
| sQ560_spl ),
inference(contradiction_clause,[status(thm)],[f7832]) ).
fof(f7834,plain,
( ~ sQ384_spl
| sQ636_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5475,f6250]) ).
fof(f7835,plain,
( ~ sQ384_spl
| sQ636_spl ),
inference(contradiction_clause,[status(thm)],[f7834]) ).
fof(f7892,plain,
( ~ sQ202_spl
| sQ559_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6935,f4860]) ).
fof(f7893,plain,
( ~ sQ202_spl
| sQ559_spl ),
inference(contradiction_clause,[status(thm)],[f7892]) ).
fof(f8063,plain,
( ~ sQ272_spl
| incident(a1,ob) ),
inference(resolution,[status(thm)],[f1836,f311]) ).
fof(f8068,plain,
( ~ sQ272_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f8063,f781,f1835]) ).
fof(f8079,plain,
( ~ sQ4_spl
| ~ sQ288_spl
| point_equal(c1,b2)
| ~ incident(c1,ob) ),
inference(resolution,[status(thm)],[f1962,f147]) ).
fof(f8081,plain,
( ~ sQ288_spl
| point_equal(a2,b2)
| ~ incident(a2,ob) ),
inference(resolution,[status(thm)],[f1962,f65]) ).
fof(f8083,plain,
( ~ sQ4_spl
| ~ sQ288_spl
| sQ460_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f8079,f784,f3600,f1961,f146]) ).
fof(f8085,plain,
( ~ sQ288_spl
| sQ429_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f8081,f825,f3367,f1961]) ).
fof(f8089,plain,
( ~ sQ258_spl
| point_equal(a1,c2)
| ~ incident(a1,oc) ),
inference(resolution,[status(thm)],[f1728,f63]) ).
fof(f8093,plain,
( ~ sQ258_spl
| sQ377_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f8089,f803,f2781,f1727]) ).
fof(f8181,plain,
( ~ sQ318_spl
| line_equal(b1c1,a1b1)
| ~ incident(ab,b1c1) ),
inference(resolution,[status(thm)],[f2285,f72]) ).
fof(f8184,plain,
( ~ sQ318_spl
| sQ226_spl
| ~ sQ414_spl ),
inference(split_clause,[status(thm)],[f8181,f3190,f1485,f2284]) ).
fof(f8187,plain,
( ~ sQ130_spl
| point_equal(o,c2)
| ~ incident(c2,ob) ),
inference(resolution,[status(thm)],[f1055,f83]) ).
fof(f8188,plain,
( ~ sQ130_spl
| point_equal(o,c1)
| ~ incident(c1,ob) ),
inference(resolution,[status(thm)],[f1055,f82]) ).
fof(f8190,plain,
( ~ sQ130_spl
| sQ363_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f8187,f828,f2540,f1054]) ).
fof(f8191,plain,
( ~ sQ130_spl
| sQ384_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f8188,f784,f2875,f1054]) ).
fof(f8200,plain,
( ~ sQ245_spl
| point_equal(a1,b1)
| ~ incident(b1,a1c1) ),
inference(resolution,[status(thm)],[f1619,f64]) ).
fof(f8204,plain,
( ~ sQ245_spl
| sQ478_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f8200,f811,f3728,f1618]) ).
fof(f8206,plain,
( ~ sQ384_spl
| sQ635_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5476,f6246]) ).
fof(f8207,plain,
( ~ sQ384_spl
| sQ635_spl ),
inference(contradiction_clause,[status(thm)],[f8206]) ).
fof(f8294,plain,
( ~ sQ7_spl
| ~ sQ306_spl
| point_equal(c2,a1)
| ~ incident(c2,a1c1) ),
inference(resolution,[status(thm)],[f2171,f157]) ).
fof(f8296,plain,
( ~ sQ306_spl
| point_equal(a1,a1)
| ~ incident(a1,a1c1) ),
inference(resolution,[status(thm)],[f2171,f63]) ).
fof(f8298,plain,
( ~ sQ7_spl
| ~ sQ306_spl
| sQ484_spl
| ~ sQ274_spl ),
inference(split_clause,[status(thm)],[f8294,f1842,f3792,f2170,f156]) ).
fof(f8300,plain,
( ~ sQ306_spl
| sQ59_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f8296,f617,f613,f2170]) ).
fof(f8302,plain,
( ~ sQ360_spl
| incident(a2,ob) ),
inference(resolution,[status(thm)],[f2520,f262]) ).
fof(f8303,plain,
( ~ sQ360_spl
| incident(a2,oc) ),
inference(resolution,[status(thm)],[f2520,f261]) ).
fof(f8306,plain,
( ~ sQ360_spl
| sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8302,f827]) ).
fof(f8307,plain,
( ~ sQ360_spl
| sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f8306]) ).
fof(f8316,plain,
( ~ sQ7_spl
| ~ sQ374_spl
| line_equal(a1b1,b2c2)
| ~ incident(b2,a1b1) ),
inference(resolution,[status(thm)],[f2772,f157]) ).
fof(f8317,plain,
( ~ sQ374_spl
| line_equal(oc,b2c2)
| ~ incident(b2,oc) ),
inference(resolution,[status(thm)],[f2772,f83]) ).
fof(f8318,plain,
( ~ sQ374_spl
| line_equal(b2c2,b2c2)
| ~ incident(b2,b2c2) ),
inference(resolution,[status(thm)],[f2772,f73]) ).
fof(f8319,plain,
( ~ sQ374_spl
| line_equal(a2c2,b2c2)
| ~ incident(b2,a2c2) ),
inference(resolution,[status(thm)],[f2772,f70]) ).
fof(f8320,plain,
( ~ sQ7_spl
| ~ sQ374_spl
| sQ152_spl
| ~ sQ116_spl ),
inference(split_clause,[status(thm)],[f8316,f870,f1155,f2771,f156]) ).
fof(f8321,plain,
( ~ sQ374_spl
| sQ153_spl
| ~ sQ113_spl ),
inference(split_clause,[status(thm)],[f8317,f843,f1159,f2771]) ).
fof(f8322,plain,
( ~ sQ374_spl
| sQ28_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f8318,f571,f498,f2771]) ).
fof(f8323,plain,
( ~ sQ374_spl
| sQ156_spl
| ~ sQ114_spl ),
inference(split_clause,[status(thm)],[f8319,f848,f1170,f2771]) ).
fof(f8349,plain,
( ~ sQ4_spl
| ~ sQ207_spl
| point_equal(a2,c1)
| ~ incident(c1,a2c2) ),
inference(resolution,[status(thm)],[f1400,f147]) ).
fof(f8351,plain,
( ~ sQ207_spl
| point_equal(a2,a2)
| ~ incident(a2,a2c2) ),
inference(resolution,[status(thm)],[f1400,f65]) ).
fof(f8353,plain,
( ~ sQ4_spl
| ~ sQ207_spl
| sQ388_spl
| ~ sQ184_spl ),
inference(split_clause,[status(thm)],[f8349,f1299,f2905,f1399,f146]) ).
fof(f8355,plain,
( ~ sQ207_spl
| sQ51_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f8351,f586,f582,f1399]) ).
fof(f8370,plain,
( ~ sQ7_spl
| ~ sQ349_spl
| line_equal(a1b1,oc)
| ~ incident(o,a1b1) ),
inference(resolution,[status(thm)],[f2459,f157]) ).
fof(f8372,plain,
( ~ sQ349_spl
| line_equal(b2c2,oc)
| ~ incident(o,b2c2) ),
inference(resolution,[status(thm)],[f2459,f73]) ).
fof(f8374,plain,
( ~ sQ7_spl
| ~ sQ349_spl
| sQ142_spl
| ~ sQ637_spl ),
inference(split_clause,[status(thm)],[f8370,f6257,f1108,f2458,f156]) ).
fof(f8376,plain,
( ~ sQ349_spl
| sQ145_spl
| ~ sQ638_spl ),
inference(split_clause,[status(thm)],[f8372,f6267,f1119,f2458]) ).
fof(f8394,plain,
( ~ sQ396_spl
| sQ634_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5487,f6241]) ).
fof(f8395,plain,
( ~ sQ396_spl
| sQ634_spl ),
inference(contradiction_clause,[status(thm)],[f8394]) ).
fof(f8404,plain,
( ~ sQ4_spl
| ~ sQ394_spl
| line_equal(a2b2,a1c1)
| ~ incident(a1,a2b2) ),
inference(resolution,[status(thm)],[f2941,f147]) ).
fof(f8407,plain,
( ~ sQ394_spl
| line_equal(a1c1,a1c1)
| ~ incident(a1,a1c1) ),
inference(resolution,[status(thm)],[f2941,f68]) ).
fof(f8408,plain,
( ~ sQ4_spl
| ~ sQ394_spl
| sQ180_spl
| ~ sQ103_spl ),
inference(split_clause,[status(thm)],[f8404,f796,f1279,f2940,f146]) ).
fof(f8411,plain,
( ~ sQ394_spl
| sQ25_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f8407,f617,f488,f2940]) ).
fof(f8412,plain,
( ~ sQ7_spl
| ~ sQ380_spl
| line_equal(a1b1,a2c2)
| ~ incident(a2,a1b1) ),
inference(resolution,[status(thm)],[f2852,f157]) ).
fof(f8415,plain,
( ~ sQ380_spl
| line_equal(a2c2,a2c2)
| ~ incident(a2,a2c2) ),
inference(resolution,[status(thm)],[f2852,f70]) ).
fof(f8416,plain,
( ~ sQ7_spl
| ~ sQ380_spl
| sQ158_spl
| ~ sQ115_spl ),
inference(split_clause,[status(thm)],[f8412,f867,f1181,f2851,f156]) ).
fof(f8419,plain,
( ~ sQ380_spl
| sQ23_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f8415,f586,f481,f2851]) ).
fof(f8488,plain,
( ~ sQ483_spl
| line_equal(b2c2,a1b1)
| ~ incident(a1,b2c2) ),
inference(resolution,[status(thm)],[f3790,f73]) ).
fof(f8492,plain,
( ~ sQ483_spl
| sQ248_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f8488,f140,f1632,f3789]) ).
fof(f8494,plain,
( ~ sQ363_spl
| sQ638_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5482,f6269]) ).
fof(f8495,plain,
( ~ sQ363_spl
| sQ638_spl ),
inference(contradiction_clause,[status(thm)],[f8494]) ).
fof(f8496,plain,
( ~ sQ372_spl
| sQ566_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4410,f4905]) ).
fof(f8497,plain,
( ~ sQ372_spl
| sQ566_spl ),
inference(contradiction_clause,[status(thm)],[f8496]) ).
fof(f8580,plain,
( ~ sQ350_spl
| incident(c2,ob) ),
inference(resolution,[status(thm)],[f2462,f262]) ).
fof(f8584,plain,
( ~ sQ350_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f8580,f828,f2461]) ).
fof(f8772,plain,
( ~ sQ282_spl
| point_equal(bc,c1)
| ~ incident(bc,oc) ),
inference(resolution,[status(thm)],[f1918,f84]) ).
fof(f8774,plain,
( ~ sQ282_spl
| point_equal(b1,c1)
| ~ incident(b1,oc) ),
inference(resolution,[status(thm)],[f1918,f72]) ).
fof(f8775,plain,
( ~ sQ282_spl
| sQ213_spl
| ~ sQ566_spl ),
inference(split_clause,[status(thm)],[f8772,f4903,f1428,f1917]) ).
fof(f8777,plain,
( ~ sQ282_spl
| sQ390_spl
| ~ sQ106_spl ),
inference(split_clause,[status(thm)],[f8774,f806,f2912,f1917]) ).
fof(f8853,plain,
( ~ sQ335_spl
| line_equal(a2c2,b2c2)
| ~ incident(bc,a2c2) ),
inference(resolution,[status(thm)],[f2384,f70]) ).
fof(f8857,plain,
( ~ sQ335_spl
| sQ156_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f8853,f746,f1170,f2383]) ).
fof(f8932,plain,
( ~ sQ282_spl
| ~ sQ5_spl
| point_equal(a2,c1)
| ~ incident(a2,oc) ),
inference(resolution,[status(thm)],[f151,f1918]) ).
fof(f8963,plain,
( ~ sQ282_spl
| ~ sQ5_spl
| sQ388_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f8932,f840,f2905,f150,f1917]) ).
fof(f9006,plain,
( ~ sQ380_spl
| ~ sQ484_spl
| line_equal(a1c1,a2c2)
| ~ incident(a2,a1c1) ),
inference(resolution,[status(thm)],[f7573,f2852]) ).
fof(f9007,plain,
( ~ sQ374_spl
| ~ sQ484_spl
| line_equal(a1c1,b2c2)
| ~ incident(b2,a1c1) ),
inference(resolution,[status(thm)],[f7573,f2772]) ).
fof(f9042,plain,
( ~ sQ380_spl
| ~ sQ484_spl
| sQ14_spl
| ~ sQ273_spl ),
inference(split_clause,[status(thm)],[f9006,f1839,f187,f3792,f2851]) ).
fof(f9043,plain,
( ~ sQ374_spl
| ~ sQ484_spl
| sQ270_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f9007,f153,f1828,f3792,f2771]) ).
fof(f9293,plain,
( ~ sQ287_spl
| point_equal(c2,b2)
| ~ incident(c2,ob) ),
inference(resolution,[status(thm)],[f1958,f73]) ).
fof(f9296,plain,
( ~ sQ287_spl
| sQ422_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f9293,f828,f3329,f1957]) ).
fof(f9350,plain,
( ~ sQ6_spl
| ~ sQ167_spl
| point_equal(c1,b2)
| ~ incident(b2,a2b2) ),
inference(resolution,[status(thm)],[f1220,f154]) ).
fof(f9354,plain,
( ~ sQ6_spl
| ~ sQ167_spl
| sQ460_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f9350,f575,f3600,f1219,f153]) ).
fof(f9356,plain,
( ~ sQ363_spl
| sQ639_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5481,f6288]) ).
fof(f9357,plain,
( ~ sQ363_spl
| sQ639_spl ),
inference(contradiction_clause,[status(thm)],[f9356]) ).
fof(f9358,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f470,f88]) ).
fof(f9359,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f9358]) ).
fof(f9360,plain,
( ~ sQ172_spl
| sQ566_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4098,f4905]) ).
fof(f9361,plain,
( ~ sQ172_spl
| sQ566_spl ),
inference(contradiction_clause,[status(thm)],[f9360]) ).
fof(f9363,plain,
( ~ sQ383_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f4416,f806,f2861]) ).
fof(f9364,plain,
( ~ sQ153_spl
| sQ638_spl ),
inference(split_clause,[status(thm)],[f5736,f6267,f1159]) ).
fof(f9365,plain,
( ~ sQ213_spl
| sQ566_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3651,f4905]) ).
fof(f9366,plain,
( ~ sQ213_spl
| sQ566_spl ),
inference(contradiction_clause,[status(thm)],[f9365]) ).
fof(f9457,plain,
( ~ sQ477_spl
| ~ sQ3_spl
| line_equal(a2c2,a1b1)
| ~ incident(a1,a2c2) ),
inference(resolution,[status(thm)],[f144,f3726]) ).
fof(f9460,plain,
! [X0] :
( ~ sQ3_spl
| line_equal(a2c2,b1c1)
| point_equal(X0,b1)
| ~ incident(X0,b1c1)
| ~ incident(X0,a2c2) ),
inference(resolution,[status(thm)],[f144,f453]) ).
fof(f9470,plain,
( ~ sQ263_spl
| ~ sQ3_spl
| point_equal(b1,c2)
| ~ incident(b1,b2c2) ),
inference(resolution,[status(thm)],[f144,f1754]) ).
fof(f9484,plain,
( ~ sQ477_spl
| ~ sQ3_spl
| sQ236_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f9457,f1306,f1539,f143,f3725]) ).
fof(f9487,plain,
( ~ sQ3_spl
| sQ238_spl
| sQ309_spl ),
inference(split_clause,[status(thm)],[f9460,f2228,f1546,f143]) ).
fof(f9497,plain,
( ~ sQ263_spl
| ~ sQ3_spl
| sQ383_spl
| ~ sQ214_spl ),
inference(split_clause,[status(thm)],[f9470,f1432,f2861,f143,f1753]) ).
fof(f9504,plain,
( ~ sQ176_spl
| sQ635_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4103,f6246]) ).
fof(f9505,plain,
( ~ sQ176_spl
| sQ635_spl ),
inference(contradiction_clause,[status(thm)],[f9504]) ).
fof(f9506,plain,
( ~ sQ159_spl
| sQ639_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5505,f6288]) ).
fof(f9507,plain,
( ~ sQ159_spl
| sQ639_spl ),
inference(contradiction_clause,[status(thm)],[f9506]) ).
fof(f9508,plain,
( ~ sQ357_spl
| sQ564_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7004,f4885]) ).
fof(f9509,plain,
( ~ sQ357_spl
| sQ564_spl ),
inference(contradiction_clause,[status(thm)],[f9508]) ).
fof(f9561,plain,
( ~ sQ475_spl
| point_equal(b1,c2) ),
inference(resolution,[status(thm)],[f3717,f112]) ).
fof(f9564,plain,
( ~ sQ475_spl
| sQ383_spl ),
inference(split_clause,[status(thm)],[f9561,f2861,f3716]) ).
fof(f9568,plain,
( ~ sQ280_spl
| incident(b1,oa) ),
inference(resolution,[status(thm)],[f1903,f308]) ).
fof(f9573,plain,
( ~ sQ280_spl
| sQ564_spl ),
inference(split_clause,[status(thm)],[f9568,f4883,f1902]) ).
fof(f9576,plain,
( ~ sQ311_spl
| incident(b2,a2c2) ),
inference(resolution,[status(thm)],[f2236,f300]) ).
fof(f9580,plain,
( ~ sQ311_spl
| sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9576,f850]) ).
fof(f9581,plain,
( ~ sQ311_spl
| sQ114_spl ),
inference(contradiction_clause,[status(thm)],[f9580]) ).
fof(f9614,plain,
( ~ sQ378_spl
| incident(ac,b2c2) ),
inference(resolution,[status(thm)],[f2843,f265]) ).
fof(f9618,plain,
( ~ sQ378_spl
| sQ418_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9614,f3207]) ).
fof(f9619,plain,
( ~ sQ378_spl
| sQ418_spl ),
inference(contradiction_clause,[status(thm)],[f9618]) ).
fof(f9623,plain,
( ~ sQ240_spl
| incident(a2,ob) ),
inference(resolution,[status(thm)],[f1554,f304]) ).
fof(f9628,plain,
( ~ sQ240_spl
| sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9623,f827]) ).
fof(f9629,plain,
( ~ sQ240_spl
| sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f9628]) ).
fof(f9693,plain,
( ~ sQ3_spl
| ~ sQ293_spl
| point_equal(b1,a2)
| ~ incident(b1,oa) ),
inference(resolution,[status(thm)],[f2060,f144]) ).
fof(f9697,plain,
( ~ sQ3_spl
| ~ sQ293_spl
| sQ438_spl
| ~ sQ564_spl ),
inference(split_clause,[status(thm)],[f9693,f4883,f3432,f2059,f143]) ).
fof(f9739,plain,
( ~ sQ241_spl
| point_equal(a1,c1)
| ~ incident(c1,b2c2) ),
inference(resolution,[status(thm)],[f1604,f68]) ).
fof(f9742,plain,
( ~ sQ241_spl
| sQ395_spl
| ~ sQ212_spl ),
inference(split_clause,[status(thm)],[f9739,f1425,f2943,f1603]) ).
fof(f9785,plain,
( ~ sQ387_spl
| line_equal(a2b2,b1c1)
| ~ incident(c1,a2b2) ),
inference(resolution,[status(thm)],[f2903,f65]) ).
fof(f9789,plain,
( ~ sQ387_spl
| sQ175_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f9785,f146,f1256,f2902]) ).
fof(f9792,plain,
( ~ sQ653_spl
| line_equal(a2c2,b1c1)
| ~ incident(b1,a2c2) ),
inference(resolution,[status(thm)],[f6693,f69]) ).
fof(f9796,plain,
( ~ sQ653_spl
| sQ238_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f9792,f143,f1546,f6692]) ).
fof(f9800,plain,
( ~ sQ197_spl
| sQ634_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2129,f6241]) ).
fof(f9801,plain,
( ~ sQ197_spl
| sQ634_spl ),
inference(contradiction_clause,[status(thm)],[f9800]) ).
fof(f9804,plain,
( ~ sQ360_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f8303,f840,f2519]) ).
fof(f9805,plain,
$false,
inference(sat_refutation,[status(thm)],[f139,f149,f159,f160,f161,f162,f166,f170,f174,f178,f182,f186,f190,f194,f196,f752,f759,f766,f773,f787,f791,f795,f802,f816,f818,f835,f839,f846,f853,f855,f993,f1013,f1034,f1060,f1067,f1074,f1085,f1122,f1135,f1143,f1147,f1158,f1173,f1184,f1188,f1211,f1218,f1225,f1244,f1251,f1274,f1282,f1298,f1305,f1312,f1326,f1351,f1358,f1394,f1405,f1424,f1431,f1438,f1477,f1549,f1556,f1557,f1609,f1643,f1665,f1676,f1687,f1696,f1718,f1719,f1733,f1751,f1766,f1780,f1797,f1831,f1920,f1928,f1942,f1943,f1960,f1964,f1973,f1980,f1982,f1984,f1986,f1988,f1990,f1992,f2045,f2062,f2075,f2090,f2098,f2126,f2133,f2138,f2183,f2191,f2198,f2204,f2238,f2318,f2367,f2368,f2389,f2396,f2464,f2500,f2522,f2570,f2765,f2785,f2833,f2845,f2857,f2879,f2896,f2915,f2946,f2972,f3062,f3079,f3150,f3151,f3219,f3332,f3358,f3370,f3435,f3478,f3499,f3592,f3670,f3712,f3731,f3747,f3824,f3825,f3899,f3916,f4079,f4199,f4206,f4213,f4239,f4262,f4406,f4419,f4426,f4480,f4507,f4522,f4531,f4535,f4563,f4655,f4709,f4741,f4788,f4795,f4796,f4861,f4865,f4866,f4878,f4888,f4897,f4899,f4906,f4908,f4974,f4981,f4986,f4997,f5005,f5013,f5015,f5016,f5018,f5020,f5021,f5025,f5027,f5028,f5029,f5036,f5125,f5132,f5182,f5189,f5252,f5286,f5293,f5301,f5360,f5361,f5363,f5371,f5379,f5386,f5392,f5393,f5502,f5508,f5515,f5584,f5645,f5739,f5740,f5748,f5755,f5813,f5817,f5823,f5827,f5850,f5872,f5879,f5886,f5888,f5918,f5923,f5973,f6117,f6125,f6144,f6150,f6156,f6158,f6160,f6256,f6265,f6270,f6289,f6290,f6296,f6297,f6298,f6305,f6312,f6313,f6314,f6320,f6322,f6327,f6328,f6329,f6343,f6357,f6462,f6469,f6573,f6588,f6602,f6606,f6608,f6680,f6741,f6815,f6871,f6872,f6879,f6891,f6893,f6895,f6897,f6899,f6900,f6901,f6903,f6905,f6917,f6924,f6933,f6944,f6971,f7010,f7094,f7157,f7186,f7187,f7238,f7337,f7484,f7583,f7584,f7591,f7607,f7608,f7619,f7620,f7622,f7623,f7624,f7833,f7835,f7893,f8068,f8083,f8085,f8093,f8184,f8190,f8191,f8204,f8207,f8298,f8300,f8307,f8320,f8321,f8322,f8323,f8353,f8355,f8374,f8376,f8395,f8408,f8411,f8416,f8419,f8492,f8495,f8497,f8584,f8775,f8777,f8857,f8963,f9042,f9043,f9296,f9354,f9357,f9359,f9361,f9363,f9364,f9366,f9484,f9487,f9497,f9505,f9507,f9509,f9564,f9573,f9581,f9619,f9629,f9697,f9742,f9789,f9796,f9801,f9804]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.56 % Computer : n010.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.57 % CPULimit : 300
% 0.08/0.57 % WCLimit : 300
% 0.08/0.57 % DateTime : Sun Sep 20 12:52:27 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.08/0.60 % Drodi V4.1.1
% 15.11/2.77 % Refutation found
% 15.11/2.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.11/2.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.11/2.80 % Elapsed time: 2.203477 seconds
% 15.11/2.80 % CPU time: 17.099216 seconds
% 15.11/2.80 % Total memory used: 68.621 MB
% 15.11/2.80 % Net memory used: 61.126 MB
%------------------------------------------------------------------------------