%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 09:51:45 AM UTC 2026
% Result : Theorem 9.93s 2.24s
% Output : Refutation 10.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 175
% Syntax : Number of formulae : 1048 ( 132 unt; 125 def)
% Number of atoms : 2644 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 2946 (1350 ~;1434 |; 18 &)
% ( 125 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 130 ( 129 usr; 127 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 261 ( 0 sgn 261 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ( line_equal(X0,X0)
& incident(bc,X0)
& incident(ac,X0)
& incident(ab,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_normal) ).
fof(f2,axiom,
( ( incident(a1,b2c2)
& incident(b1,a2c2)
& incident(c1,a2b2) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1in2) ).
fof(f3,axiom,
( ( incident(a2,b1c1)
& incident(b2,a1c1)
& incident(c2,a1b1) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2in1) ).
fof(f4,axiom,
( incident(a1,b2c2)
| incident(b2,a1c1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap_a) ).
fof(f5,axiom,
( incident(b1,a2c2)
| incident(c2,a1b1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap_b) ).
fof(f6,axiom,
( incident(c1,a2b2)
| incident(a2,b1c1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap_c) ).
fof(f7,axiom,
incident(a1,a1b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1b1) ).
fof(f8,axiom,
incident(b1,a1b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1a1) ).
fof(f9,axiom,
incident(a2,a2b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2b2) ).
fof(f10,axiom,
incident(b2,a2b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2a2) ).
fof(f11,axiom,
incident(a1,a1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1c1) ).
fof(f12,axiom,
incident(c1,a1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic1a1) ).
fof(f13,axiom,
incident(a2,a2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2c2) ).
fof(f14,axiom,
incident(c2,a2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic2a2) ).
fof(f15,axiom,
incident(c1,b1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic1b1) ).
fof(f16,axiom,
incident(b1,b1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1c1) ).
fof(f17,axiom,
incident(c2,b2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic2b2) ).
fof(f18,axiom,
incident(b2,b2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2c2) ).
fof(f19,axiom,
incident(o,oa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iooa) ).
fof(f20,axiom,
incident(o,ob),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ioob) ).
fof(f21,axiom,
incident(o,oc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iooc) ).
fof(f22,axiom,
incident(a1,oa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1oa) ).
fof(f23,axiom,
incident(a2,oa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2oa) ).
fof(f24,axiom,
incident(b1,ob),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1ob) ).
fof(f25,axiom,
incident(b2,ob),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2ob) ).
fof(f26,axiom,
incident(c1,oc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic1oc) ).
fof(f27,axiom,
incident(c2,oc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ic2oc) ).
fof(f28,axiom,
incident(bc,b1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ibc1) ).
fof(f29,axiom,
incident(bc,b2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ibc2) ).
fof(f30,axiom,
incident(ac,a1c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iac1) ).
fof(f31,axiom,
incident(ac,a2c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iac2) ).
fof(f32,axiom,
incident(ab,a1b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iab1) ).
fof(f33,axiom,
incident(ab,a2b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iab2) ).
fof(f34,axiom,
! [X0] :
( ( incident(a1,X0)
& incident(b1,X0)
& incident(c1,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',triangle1) ).
fof(f35,axiom,
! [X0] :
( ( incident(a2,X0)
& incident(b2,X0)
& incident(c2,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',triangle2) ).
fof(f36,axiom,
( point_equal(a2,a1)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notaa) ).
fof(f37,axiom,
( point_equal(b2,b1)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notbb) ).
fof(f38,axiom,
( point_equal(c2,c1)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notcc) ).
fof(f39,axiom,
( line_equal(b1c1,b2c2)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notbc) ).
fof(f40,axiom,
( line_equal(a1c1,a2c2)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notac) ).
fof(f41,axiom,
( line_equal(a1b1,a2b2)
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notab) ).
fof(f43,axiom,
! [X0,X1] :
( point_equal(X0,X1)
=> point_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_point_equal) ).
fof(f44,axiom,
! [X0,X1,X2] :
( ( point_equal(X0,X1)
& point_equal(X1,X2) )
=> point_equal(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_point_equal) ).
fof(f45,axiom,
! [X0,X1] :
( incident(X0,X1)
=> line_equal(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_line_equal) ).
fof(f46,axiom,
! [X0,X1] :
( line_equal(X0,X1)
=> line_equal(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_line_equal) ).
fof(f47,axiom,
! [X0,X1,X2] :
( ( line_equal(X0,X1)
& line_equal(X1,X2) )
=> line_equal(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_line_equal) ).
fof(f48,axiom,
! [X0,X1,X2] :
( ( point_equal(X0,X1)
& incident(X1,X2) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pcon) ).
fof(f49,axiom,
! [X0,X1,X2] :
( ( incident(X0,X1)
& line_equal(X1,X2) )
=> incident(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lcon) ).
fof(f50,axiom,
! [X0,X1,X2,X3] :
( ( incident(X0,X2)
& incident(X0,X3)
& incident(X1,X2)
& incident(X1,X3) )
=> ( point_equal(X0,X1)
| line_equal(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique) ).
fof(f51,conjecture,
goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f52,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f53,plain,
~ goal,
inference(flattening,[],[f52]) ).
fof(f54,plain,
! [X0] :
( goal
| ~ line_equal(X0,X0)
| ~ incident(bc,X0)
| ~ incident(ac,X0)
| ~ incident(ab,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f55,plain,
! [X0] :
( goal
| ~ line_equal(X0,X0)
| ~ incident(bc,X0)
| ~ incident(ac,X0)
| ~ incident(ab,X0) ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
( goal
| ~ incident(a1,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(c1,a2b2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f57,plain,
( goal
| ~ incident(a1,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(c1,a2b2) ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
( goal
| ~ incident(a2,b1c1)
| ~ incident(b2,a1c1)
| ~ incident(c2,a1b1) ),
inference(ennf_transformation,[],[f3]) ).
fof(f59,plain,
( goal
| ~ incident(a2,b1c1)
| ~ incident(b2,a1c1)
| ~ incident(c2,a1b1) ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
! [X0] :
( goal
| ~ incident(a1,X0)
| ~ incident(b1,X0)
| ~ incident(c1,X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f61,plain,
! [X0] :
( goal
| ~ incident(a1,X0)
| ~ incident(b1,X0)
| ~ incident(c1,X0) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0] :
( goal
| ~ incident(a2,X0)
| ~ incident(b2,X0)
| ~ incident(c2,X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f63,plain,
! [X0] :
( goal
| ~ incident(a2,X0)
| ~ incident(b2,X0)
| ~ incident(c2,X0) ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
( goal
| ~ point_equal(a2,a1) ),
inference(ennf_transformation,[],[f36]) ).
fof(f65,plain,
( goal
| ~ point_equal(b2,b1) ),
inference(ennf_transformation,[],[f37]) ).
fof(f66,plain,
( goal
| ~ point_equal(c2,c1) ),
inference(ennf_transformation,[],[f38]) ).
fof(f67,plain,
( goal
| ~ line_equal(b1c1,b2c2) ),
inference(ennf_transformation,[],[f39]) ).
fof(f68,plain,
( goal
| ~ line_equal(a1c1,a2c2) ),
inference(ennf_transformation,[],[f40]) ).
fof(f69,plain,
( goal
| ~ line_equal(a1b1,a2b2) ),
inference(ennf_transformation,[],[f41]) ).
fof(f71,plain,
! [X0,X1] :
( point_equal(X1,X0)
| ~ point_equal(X0,X1) ),
inference(ennf_transformation,[],[f43]) ).
fof(f72,plain,
! [X0,X1,X2] :
( point_equal(X0,X2)
| ~ point_equal(X0,X1)
| ~ point_equal(X1,X2) ),
inference(ennf_transformation,[],[f44]) ).
fof(f73,plain,
! [X0,X1,X2] :
( point_equal(X0,X2)
| ~ point_equal(X0,X1)
| ~ point_equal(X1,X2) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1] :
( line_equal(X1,X1)
| ~ incident(X0,X1) ),
inference(ennf_transformation,[],[f45]) ).
fof(f75,plain,
! [X0,X1] :
( line_equal(X1,X0)
| ~ line_equal(X0,X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f76,plain,
! [X0,X1,X2] :
( line_equal(X0,X2)
| ~ line_equal(X0,X1)
| ~ line_equal(X1,X2) ),
inference(ennf_transformation,[],[f47]) ).
fof(f77,plain,
! [X0,X1,X2] :
( line_equal(X0,X2)
| ~ line_equal(X0,X1)
| ~ line_equal(X1,X2) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ point_equal(X0,X1)
| ~ incident(X1,X2) ),
inference(ennf_transformation,[],[f48]) ).
fof(f79,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ point_equal(X0,X1)
| ~ incident(X1,X2) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ incident(X0,X1)
| ~ line_equal(X1,X2) ),
inference(ennf_transformation,[],[f49]) ).
fof(f81,plain,
! [X0,X1,X2] :
( incident(X0,X2)
| ~ incident(X0,X1)
| ~ line_equal(X1,X2) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( point_equal(X0,X1)
| line_equal(X2,X3)
| ~ incident(X0,X2)
| ~ incident(X0,X3)
| ~ incident(X1,X2)
| ~ incident(X1,X3) ),
inference(ennf_transformation,[],[f50]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( point_equal(X0,X1)
| line_equal(X2,X3)
| ~ incident(X0,X2)
| ~ incident(X0,X3)
| ~ incident(X1,X2)
| ~ incident(X1,X3) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0] :
( goal
| ~ line_equal(X0,X0)
| ~ incident(bc,X0)
| ~ incident(ac,X0)
| ~ incident(ab,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f85,plain,
( goal
| ~ incident(a1,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(c1,a2b2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f86,plain,
( goal
| ~ incident(a2,b1c1)
| ~ incident(b2,a1c1)
| ~ incident(c2,a1b1) ),
inference(cnf_transformation,[],[f59]) ).
fof(f87,plain,
( incident(a1,b2c2)
| incident(b2,a1c1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f88,plain,
( incident(b1,a2c2)
| incident(c2,a1b1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f89,plain,
( incident(c1,a2b2)
| incident(a2,b1c1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f90,plain,
incident(a1,a1b1),
inference(cnf_transformation,[],[f7]) ).
fof(f91,plain,
incident(b1,a1b1),
inference(cnf_transformation,[],[f8]) ).
fof(f92,plain,
incident(a2,a2b2),
inference(cnf_transformation,[],[f9]) ).
fof(f93,plain,
incident(b2,a2b2),
inference(cnf_transformation,[],[f10]) ).
fof(f94,plain,
incident(a1,a1c1),
inference(cnf_transformation,[],[f11]) ).
fof(f95,plain,
incident(c1,a1c1),
inference(cnf_transformation,[],[f12]) ).
fof(f96,plain,
incident(a2,a2c2),
inference(cnf_transformation,[],[f13]) ).
fof(f97,plain,
incident(c2,a2c2),
inference(cnf_transformation,[],[f14]) ).
fof(f98,plain,
incident(c1,b1c1),
inference(cnf_transformation,[],[f15]) ).
fof(f99,plain,
incident(b1,b1c1),
inference(cnf_transformation,[],[f16]) ).
fof(f100,plain,
incident(c2,b2c2),
inference(cnf_transformation,[],[f17]) ).
fof(f101,plain,
incident(b2,b2c2),
inference(cnf_transformation,[],[f18]) ).
fof(f102,plain,
incident(o,oa),
inference(cnf_transformation,[],[f19]) ).
fof(f103,plain,
incident(o,ob),
inference(cnf_transformation,[],[f20]) ).
fof(f104,plain,
incident(o,oc),
inference(cnf_transformation,[],[f21]) ).
fof(f105,plain,
incident(a1,oa),
inference(cnf_transformation,[],[f22]) ).
fof(f106,plain,
incident(a2,oa),
inference(cnf_transformation,[],[f23]) ).
fof(f107,plain,
incident(b1,ob),
inference(cnf_transformation,[],[f24]) ).
fof(f108,plain,
incident(b2,ob),
inference(cnf_transformation,[],[f25]) ).
fof(f109,plain,
incident(c1,oc),
inference(cnf_transformation,[],[f26]) ).
fof(f110,plain,
incident(c2,oc),
inference(cnf_transformation,[],[f27]) ).
fof(f111,plain,
incident(bc,b1c1),
inference(cnf_transformation,[],[f28]) ).
fof(f112,plain,
incident(bc,b2c2),
inference(cnf_transformation,[],[f29]) ).
fof(f113,plain,
incident(ac,a1c1),
inference(cnf_transformation,[],[f30]) ).
fof(f114,plain,
incident(ac,a2c2),
inference(cnf_transformation,[],[f31]) ).
fof(f115,plain,
incident(ab,a1b1),
inference(cnf_transformation,[],[f32]) ).
fof(f116,plain,
incident(ab,a2b2),
inference(cnf_transformation,[],[f33]) ).
fof(f117,plain,
! [X0] :
( goal
| ~ incident(a1,X0)
| ~ incident(b1,X0)
| ~ incident(c1,X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f118,plain,
! [X0] :
( goal
| ~ incident(a2,X0)
| ~ incident(b2,X0)
| ~ incident(c2,X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f119,plain,
( goal
| ~ point_equal(a2,a1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f120,plain,
( goal
| ~ point_equal(b2,b1) ),
inference(cnf_transformation,[],[f65]) ).
fof(f121,plain,
( goal
| ~ point_equal(c2,c1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f122,plain,
( goal
| ~ line_equal(b1c1,b2c2) ),
inference(cnf_transformation,[],[f67]) ).
fof(f123,plain,
( goal
| ~ line_equal(a1c1,a2c2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f124,plain,
( goal
| ~ line_equal(a1b1,a2b2) ),
inference(cnf_transformation,[],[f69]) ).
fof(f126,plain,
! [X0,X1] :
( ~ point_equal(X0,X1)
| point_equal(X1,X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f127,plain,
! [X2,X0,X1] :
( ~ point_equal(X1,X2)
| ~ point_equal(X0,X1)
| point_equal(X0,X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f128,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line_equal(X1,X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f129,plain,
! [X0,X1] :
( ~ line_equal(X0,X1)
| line_equal(X1,X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ line_equal(X1,X2)
| ~ line_equal(X0,X1)
| line_equal(X0,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ point_equal(X0,X1)
| incident(X0,X2)
| ~ incident(X1,X2) ),
inference(cnf_transformation,[],[f79]) ).
fof(f132,plain,
! [X2,X0,X1] :
( ~ line_equal(X1,X2)
| ~ incident(X0,X1)
| incident(X0,X2) ),
inference(cnf_transformation,[],[f81]) ).
fof(f133,plain,
! [X2,X3,X0,X1] :
( ~ incident(X1,X3)
| line_equal(X2,X3)
| ~ incident(X0,X2)
| ~ incident(X0,X3)
| ~ incident(X1,X2)
| point_equal(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f134,plain,
~ goal,
inference(cnf_transformation,[],[f53]) ).
fof(f135,plain,
~ line_equal(a1b1,a2b2),
inference(forward_subsumption_resolution,[],[f124,f134]) ).
fof(f136,plain,
~ line_equal(a1c1,a2c2),
inference(forward_subsumption_resolution,[],[f123,f134]) ).
fof(f137,plain,
~ line_equal(b1c1,b2c2),
inference(forward_subsumption_resolution,[],[f122,f134]) ).
fof(f138,plain,
~ point_equal(c2,c1),
inference(forward_subsumption_resolution,[],[f121,f134]) ).
fof(f139,plain,
~ point_equal(b2,b1),
inference(forward_subsumption_resolution,[],[f120,f134]) ).
fof(f140,plain,
~ point_equal(a2,a1),
inference(forward_subsumption_resolution,[],[f119,f134]) ).
fof(f141,plain,
! [X0] :
( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(forward_subsumption_resolution,[],[f118,f134]) ).
fof(f142,plain,
! [X0] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(forward_subsumption_resolution,[],[f117,f134]) ).
fof(f144,definition,
( spl0_1
<=> incident(a2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f145,plain,
( incident(a2,b1c1)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,definition,
( spl0_2
<=> incident(c1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f148,plain,
( incident(c1,a2b2)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f149,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f89,f147,f144]) ).
fof(f151,definition,
( spl0_3
<=> incident(c2,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f152,plain,
( incident(c2,a1b1)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,definition,
( spl0_4
<=> incident(b1,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f155,plain,
( incident(b1,a2c2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f156,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f88,f154,f151]) ).
fof(f158,definition,
( spl0_5
<=> incident(b2,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f159,plain,
( incident(b2,a1c1)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f161,definition,
( spl0_6
<=> incident(a1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f162,plain,
( incident(a1,b2c2)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f163,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f87,f161,f158]) ).
fof(f164,plain,
( ~ incident(a2,b1c1)
| ~ incident(b2,a1c1)
| ~ incident(c2,a1b1) ),
inference(forward_subsumption_resolution,[],[f86,f134]) ).
fof(f165,plain,
( ~ incident(a1,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(c1,a2b2) ),
inference(forward_subsumption_resolution,[],[f85,f134]) ).
fof(f166,plain,
! [X0] :
( ~ line_equal(X0,X0)
| ~ incident(bc,X0)
| ~ incident(ac,X0)
| ~ incident(ab,X0) ),
inference(forward_subsumption_resolution,[],[f84,f134]) ).
fof(f167,plain,
( ~ incident(c2,a1b1)
| spl0_3 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f168,plain,
( ~ incident(b2,a1c1)
| spl0_5 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f170,plain,
( ~ spl0_3
| ~ spl0_5
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f164,f144,f158,f151]) ).
fof(f171,plain,
( ~ incident(c1,a2b2)
| spl0_2 ),
inference(avatar_component_clause,[],[f147]) ).
fof(f173,plain,
( ~ incident(a1,b2c2)
| spl0_6 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f174,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f165,f161,f154,f147]) ).
fof(f175,plain,
! [X0] :
( ~ incident(ab,X0)
| ~ incident(ac,X0)
| ~ incident(bc,X0) ),
inference(forward_subsumption_resolution,[],[f166,f128]) ).
fof(f178,plain,
( ~ incident(ac,a2b2)
| ~ incident(bc,a2b2) ),
inference(resolution,[],[f116,f175]) ).
fof(f181,definition,
( spl0_7
<=> incident(bc,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f182,plain,
( ~ incident(bc,a2b2)
| spl0_7 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f184,definition,
( spl0_8
<=> incident(ac,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f185,plain,
( ~ incident(ac,a2b2)
| spl0_8 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f186,plain,
( ~ spl0_7
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f178,f184,f181]) ).
fof(f189,plain,
( ~ incident(ac,a1b1)
| ~ incident(bc,a1b1) ),
inference(resolution,[],[f115,f175]) ).
fof(f192,definition,
( spl0_9
<=> incident(bc,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f193,plain,
( ~ incident(bc,a1b1)
| spl0_9 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,definition,
( spl0_10
<=> incident(ac,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f196,plain,
( ~ incident(ac,a1b1)
| spl0_10 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f197,plain,
( ~ spl0_9
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f189,f195,f192]) ).
fof(f198,plain,
( ~ incident(b2,a2c2)
| ~ incident(a2,a2c2) ),
inference(resolution,[],[f97,f141]) ).
fof(f200,plain,
~ incident(b2,a2c2),
inference(forward_subsumption_resolution,[],[f198,f96]) ).
fof(f202,plain,
( ~ incident(b2,b2c2)
| ~ incident(a2,b2c2) ),
inference(resolution,[],[f100,f141]) ).
fof(f204,plain,
~ incident(a2,b2c2),
inference(forward_subsumption_resolution,[],[f202,f101]) ).
fof(f207,plain,
( ~ incident(b1,b1c1)
| ~ incident(a1,b1c1) ),
inference(resolution,[],[f98,f142]) ).
fof(f209,plain,
~ incident(a1,b1c1),
inference(forward_subsumption_resolution,[],[f207,f99]) ).
fof(f212,plain,
( ~ incident(b1,a1c1)
| ~ incident(a1,a1c1) ),
inference(resolution,[],[f95,f142]) ).
fof(f214,plain,
~ incident(b1,a1c1),
inference(forward_subsumption_resolution,[],[f212,f94]) ).
fof(f225,definition,
( spl0_11
<=> incident(a1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f226,plain,
( ~ incident(a1,a2b2)
| spl0_11 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,definition,
( spl0_12
<=> incident(b1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f229,plain,
( ~ incident(b1,a2b2)
| spl0_12 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f234,definition,
( spl0_13
<=> incident(a2,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f235,plain,
( ~ incident(a2,a1b1)
| spl0_13 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f240,plain,
( ~ incident(b2,oc)
| ~ incident(a2,oc) ),
inference(resolution,[],[f110,f141]) ).
fof(f243,definition,
( spl0_15
<=> incident(a2,oc) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f244,plain,
( ~ incident(a2,oc)
| spl0_15 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f246,definition,
( spl0_16
<=> incident(b2,oc) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f247,plain,
( ~ incident(b2,oc)
| spl0_16 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f240,f246,f243]) ).
fof(f250,plain,
( ~ incident(b1,oc)
| ~ incident(a1,oc) ),
inference(resolution,[],[f109,f142]) ).
fof(f253,definition,
( spl0_17
<=> incident(a1,oc) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f254,plain,
( ~ incident(a1,oc)
| spl0_17 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,definition,
( spl0_18
<=> incident(b1,oc) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f257,plain,
( ~ incident(b1,oc)
| spl0_18 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( ~ spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f250,f256,f253]) ).
fof(f262,plain,
! [X0,X1] :
( ~ incident(bc,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b1c1)
| line_equal(X0,b1c1)
| point_equal(X1,bc) ),
inference(resolution,[],[f133,f111]) ).
fof(f264,plain,
! [X0,X1] :
( ~ incident(ac,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2c2)
| line_equal(X0,a2c2)
| point_equal(X1,ac) ),
inference(resolution,[],[f133,f114]) ).
fof(f266,plain,
! [X0,X1] :
( ~ incident(ab,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2b2)
| line_equal(X0,a2b2)
| point_equal(X1,ab) ),
inference(resolution,[],[f133,f116]) ).
fof(f268,plain,
! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1c1)
| line_equal(X0,a1c1)
| point_equal(X1,a1) ),
inference(resolution,[],[f133,f94]) ).
fof(f269,plain,
! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1b1)
| line_equal(X0,a1b1)
| point_equal(X1,a1) ),
inference(resolution,[],[f133,f90]) ).
fof(f270,plain,
! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,oa)
| line_equal(X0,oa)
| point_equal(X1,a1) ),
inference(resolution,[],[f133,f105]) ).
fof(f273,plain,
! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,ob)
| line_equal(X0,ob)
| point_equal(X1,b1) ),
inference(resolution,[],[f133,f107]) ).
fof(f274,plain,
( ! [X0,X1] :
( ~ incident(c1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2b2)
| line_equal(X0,a2b2)
| point_equal(X1,c1) )
| ~ spl0_2 ),
inference(resolution,[],[f133,f148]) ).
fof(f275,plain,
! [X0,X1] :
( ~ incident(X1,b1c1)
| ~ incident(X1,X0)
| line_equal(X0,b1c1)
| ~ incident(c1,X0)
| point_equal(X1,c1) ),
inference(resolution,[],[f133,f98]) ).
fof(f276,plain,
! [X0,X1] :
( ~ incident(c1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1c1)
| line_equal(X0,a1c1)
| point_equal(X1,c1) ),
inference(resolution,[],[f133,f95]) ).
fof(f277,plain,
! [X0,X1] :
( ~ incident(X1,oc)
| ~ incident(X1,X0)
| line_equal(X0,oc)
| ~ incident(c1,X0)
| point_equal(X1,c1) ),
inference(resolution,[],[f133,f109]) ).
fof(f278,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2c2)
| line_equal(X0,a2c2)
| point_equal(X1,a2) ),
inference(resolution,[],[f133,f96]) ).
fof(f279,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2b2)
| line_equal(X0,a2b2)
| point_equal(X1,a2) ),
inference(resolution,[],[f133,f92]) ).
fof(f280,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,oa)
| line_equal(X0,oa)
| point_equal(X1,a2) ),
inference(resolution,[],[f133,f106]) ).
fof(f281,plain,
! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2c2)
| line_equal(X0,b2c2)
| point_equal(X1,b2) ),
inference(resolution,[],[f133,f101]) ).
fof(f282,plain,
! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2b2)
| line_equal(X0,a2b2)
| point_equal(X1,b2) ),
inference(resolution,[],[f133,f93]) ).
fof(f283,plain,
( ! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1c1)
| line_equal(X0,a1c1)
| point_equal(X1,b2) )
| ~ spl0_5 ),
inference(resolution,[],[f133,f159]) ).
fof(f284,plain,
! [X0,X1] :
( ~ incident(X1,ob)
| ~ incident(X1,X0)
| line_equal(X0,ob)
| ~ incident(b2,X0)
| point_equal(X1,b2) ),
inference(resolution,[],[f133,f108]) ).
fof(f285,plain,
! [X0,X1] :
( ~ incident(c2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2c2)
| line_equal(X0,b2c2)
| point_equal(X1,c2) ),
inference(resolution,[],[f133,f100]) ).
fof(f286,plain,
! [X0,X1] :
( ~ incident(c2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2c2)
| line_equal(X0,a2c2)
| point_equal(X1,c2) ),
inference(resolution,[],[f133,f97]) ).
fof(f288,plain,
! [X0,X1] :
( ~ incident(X1,oc)
| ~ incident(X1,X0)
| line_equal(X0,oc)
| ~ incident(c2,X0)
| point_equal(X1,c2) ),
inference(resolution,[],[f133,f110]) ).
fof(f289,plain,
! [X0,X1] :
( ~ incident(o,X0)
| ~ incident(X1,X0)
| ~ incident(X1,oc)
| line_equal(X0,oc)
| point_equal(X1,o) ),
inference(resolution,[],[f133,f104]) ).
fof(f320,plain,
! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,oc)
| line_equal(ob,oc)
| point_equal(X0,o) ),
inference(resolution,[],[f289,f103]) ).
fof(f331,definition,
( spl0_21
<=> line_equal(ob,oc) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f332,plain,
( line_equal(ob,oc)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f334,definition,
( spl0_22
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,o)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f335,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,o)
| ~ incident(X0,ob) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f336,plain,
( spl0_21
| spl0_22 ),
inference(avatar_split_clause,[],[f320,f334,f331]) ).
fof(f349,plain,
( $false
| spl0_18
| ~ spl0_21 ),
inference(unit_resulting_resolution,[],[f132,f332,f107,f257]) ).
fof(f350,plain,
( spl0_18
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f349]) ).
fof(f359,definition,
( spl0_24
<=> point_equal(c2,o) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f360,plain,
( point_equal(c2,o)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f390,plain,
! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,oa)
| line_equal(a1c1,oa)
| point_equal(X0,a1) ),
inference(resolution,[],[f270,f94]) ).
fof(f391,plain,
! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,oa)
| line_equal(a1b1,oa)
| point_equal(X0,a1) ),
inference(resolution,[],[f270,f90]) ).
fof(f395,definition,
( spl0_29
<=> line_equal(a1b1,oa) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f396,plain,
( line_equal(a1b1,oa)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f398,definition,
( spl0_30
<=> ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,a1)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f399,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a1)
| ~ incident(X0,a1b1) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f400,plain,
( spl0_29
| spl0_30 ),
inference(avatar_split_clause,[],[f391,f398,f395]) ).
fof(f402,definition,
( spl0_31
<=> line_equal(a1c1,oa) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f403,plain,
( line_equal(a1c1,oa)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f405,definition,
( spl0_32
<=> ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,a1)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f406,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a1)
| ~ incident(X0,a1c1) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f407,plain,
( spl0_31
| spl0_32 ),
inference(avatar_split_clause,[],[f390,f405,f402]) ).
fof(f411,plain,
( line_equal(oa,a1c1)
| ~ spl0_31 ),
inference(resolution,[],[f403,f129]) ).
fof(f422,plain,
( point_equal(c2,o)
| ~ incident(c2,ob)
| ~ spl0_22 ),
inference(resolution,[],[f335,f110]) ).
fof(f426,definition,
( spl0_33
<=> incident(c2,ob) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f427,plain,
( ~ incident(c2,ob)
| spl0_33 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f437,plain,
! [X0] :
( ~ incident(c2,X0)
| line_equal(X0,oc)
| ~ incident(c1,X0)
| point_equal(c2,c1) ),
inference(resolution,[],[f277,f110]) ).
fof(f441,definition,
( spl0_35
<=> point_equal(o,c1) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f442,plain,
( point_equal(o,c1)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f447,plain,
! [X0] :
( ~ incident(c2,X0)
| line_equal(X0,oc)
| ~ incident(c1,X0) ),
inference(forward_subsumption_resolution,[],[f437,f138]) ).
fof(f455,plain,
( line_equal(b2c2,oc)
| ~ incident(c1,b2c2) ),
inference(resolution,[],[f447,f100]) ).
fof(f456,plain,
( line_equal(a2c2,oc)
| ~ incident(c1,a2c2) ),
inference(resolution,[],[f447,f97]) ).
fof(f467,definition,
( spl0_41
<=> incident(c1,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f468,plain,
( ~ incident(c1,a2c2)
| spl0_41 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f470,definition,
( spl0_42
<=> line_equal(a2c2,oc) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f471,plain,
( line_equal(a2c2,oc)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( ~ spl0_41
| spl0_42 ),
inference(avatar_split_clause,[],[f456,f470,f467]) ).
fof(f474,definition,
( spl0_43
<=> incident(c1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f475,plain,
( ~ incident(c1,b2c2)
| spl0_43 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f477,definition,
( spl0_44
<=> line_equal(b2c2,oc) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f478,plain,
( line_equal(b2c2,oc)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f479,plain,
( ~ spl0_43
| spl0_44 ),
inference(avatar_split_clause,[],[f455,f477,f474]) ).
fof(f494,plain,
! [X0] :
( ~ incident(o,X0)
| line_equal(X0,oc)
| ~ incident(c2,X0)
| point_equal(o,c2) ),
inference(resolution,[],[f288,f104]) ).
fof(f497,definition,
( spl0_45
<=> point_equal(o,c2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f498,plain,
( point_equal(o,c2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f500,definition,
( spl0_46
<=> ! [X0] :
( ~ incident(o,X0)
| ~ incident(c2,X0)
| line_equal(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f501,plain,
( ! [X0] :
( ~ incident(o,X0)
| ~ incident(c2,X0)
| line_equal(X0,oc) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f502,plain,
( spl0_45
| spl0_46 ),
inference(avatar_split_clause,[],[f494,f500,f497]) ).
fof(f515,plain,
( point_equal(c2,o)
| ~ spl0_45 ),
inference(resolution,[],[f498,f126]) ).
fof(f516,plain,
( spl0_24
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f515,f497,f359]) ).
fof(f518,plain,
( $false
| ~ spl0_24
| ~ spl0_35 ),
inference(unit_resulting_resolution,[],[f127,f138,f442,f360]) ).
fof(f523,plain,
( ~ spl0_24
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f518]) ).
fof(f527,plain,
! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,ob)
| line_equal(a1b1,ob)
| point_equal(X0,b1) ),
inference(resolution,[],[f273,f91]) ).
fof(f531,definition,
( spl0_49
<=> line_equal(a1b1,ob) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f532,plain,
( line_equal(a1b1,ob)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f534,definition,
( spl0_50
<=> ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,b1)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f535,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b1)
| ~ incident(X0,a1b1) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f536,plain,
( spl0_49
| spl0_50 ),
inference(avatar_split_clause,[],[f527,f534,f531]) ).
fof(f558,plain,
( $false
| ~ spl0_3
| spl0_33
| ~ spl0_49 ),
inference(unit_resulting_resolution,[],[f132,f532,f152,f427]) ).
fof(f559,plain,
( ~ spl0_3
| spl0_33
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f558]) ).
fof(f567,definition,
( spl0_54
<=> ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,b1)
| ~ incident(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f568,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b1)
| ~ incident(X0,a2c2) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f589,plain,
! [X0] :
( ~ incident(X0,b2c2)
| ~ incident(X0,b1c1)
| line_equal(b2c2,b1c1)
| point_equal(X0,bc) ),
inference(resolution,[],[f262,f112]) ).
fof(f592,definition,
( spl0_55
<=> line_equal(b2c2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f593,plain,
( line_equal(b2c2,b1c1)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f595,definition,
( spl0_56
<=> ! [X0] :
( ~ incident(X0,b2c2)
| point_equal(X0,bc)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f596,plain,
( ! [X0] :
( ~ incident(X0,b2c2)
| point_equal(X0,bc)
| ~ incident(X0,b1c1) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f597,plain,
( spl0_55
| spl0_56 ),
inference(avatar_split_clause,[],[f589,f595,f592]) ).
fof(f601,plain,
( line_equal(b1c1,b2c2)
| ~ spl0_55 ),
inference(resolution,[],[f593,f129]) ).
fof(f603,plain,
( $false
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f601,f137]) ).
fof(f604,plain,
~ spl0_55,
inference(avatar_contradiction_clause,[],[f603]) ).
fof(f606,plain,
! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,a2c2)
| line_equal(a1c1,a2c2)
| point_equal(X0,ac) ),
inference(resolution,[],[f264,f113]) ).
fof(f608,plain,
! [X0] :
( ~ incident(X0,a2c2)
| ~ incident(X0,a1c1)
| point_equal(X0,ac) ),
inference(forward_subsumption_resolution,[],[f606,f136]) ).
fof(f610,plain,
( ~ incident(a2,a1c1)
| point_equal(a2,ac) ),
inference(resolution,[],[f608,f96]) ).
fof(f611,plain,
( ~ incident(c2,a1c1)
| point_equal(c2,ac) ),
inference(resolution,[],[f608,f97]) ).
fof(f613,definition,
( spl0_57
<=> point_equal(c2,ac) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f614,plain,
( point_equal(c2,ac)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f616,definition,
( spl0_58
<=> incident(c2,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f617,plain,
( ~ incident(c2,a1c1)
| spl0_58 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f618,plain,
( spl0_57
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f611,f616,f613]) ).
fof(f620,definition,
( spl0_59
<=> point_equal(a2,ac) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f621,plain,
( point_equal(a2,ac)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,definition,
( spl0_60
<=> incident(a2,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f624,plain,
( ~ incident(a2,a1c1)
| spl0_60 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f625,plain,
( spl0_59
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f610,f623,f620]) ).
fof(f630,plain,
! [X0] :
( ~ incident(b1,X0)
| line_equal(X0,ob)
| ~ incident(b2,X0)
| point_equal(b1,b2) ),
inference(resolution,[],[f284,f107]) ).
fof(f632,plain,
! [X0] :
( ~ incident(o,X0)
| line_equal(X0,ob)
| ~ incident(b2,X0)
| point_equal(o,b2) ),
inference(resolution,[],[f284,f103]) ).
fof(f635,definition,
( spl0_61
<=> point_equal(o,b2) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f636,plain,
( point_equal(o,b2)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f635]) ).
fof(f638,definition,
( spl0_62
<=> ! [X0] :
( ~ incident(o,X0)
| ~ incident(b2,X0)
| line_equal(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f639,plain,
( ! [X0] :
( ~ incident(o,X0)
| ~ incident(b2,X0)
| line_equal(X0,ob) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f640,plain,
( spl0_61
| spl0_62 ),
inference(avatar_split_clause,[],[f632,f638,f635]) ).
fof(f649,definition,
( spl0_65
<=> point_equal(b1,b2) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f650,plain,
( point_equal(b1,b2)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f652,definition,
( spl0_66
<=> ! [X0] :
( ~ incident(b1,X0)
| ~ incident(b2,X0)
| line_equal(X0,ob) ) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f653,plain,
( ! [X0] :
( ~ incident(b2,X0)
| ~ incident(b1,X0)
| line_equal(X0,ob) )
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f654,plain,
( spl0_65
| spl0_66 ),
inference(avatar_split_clause,[],[f630,f652,f649]) ).
fof(f663,plain,
( point_equal(b2,b1)
| ~ spl0_65 ),
inference(resolution,[],[f650,f126]) ).
fof(f666,plain,
( $false
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f663,f139]) ).
fof(f667,plain,
~ spl0_65,
inference(avatar_contradiction_clause,[],[f666]) ).
fof(f680,plain,
( ~ incident(b2,oc)
| line_equal(oc,ob)
| ~ spl0_62 ),
inference(resolution,[],[f639,f104]) ).
fof(f684,plain,
! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,a2b2)
| line_equal(a1b1,a2b2)
| point_equal(X0,ab) ),
inference(resolution,[],[f266,f115]) ).
fof(f686,plain,
! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,a2b2)
| point_equal(X0,ab) ),
inference(forward_subsumption_resolution,[],[f684,f135]) ).
fof(f688,plain,
( ~ incident(a1,a2b2)
| point_equal(a1,ab) ),
inference(resolution,[],[f686,f90]) ).
fof(f689,plain,
( ~ incident(b1,a2b2)
| point_equal(b1,ab) ),
inference(resolution,[],[f686,f91]) ).
fof(f690,plain,
( ~ incident(c2,a2b2)
| point_equal(c2,ab)
| ~ spl0_3 ),
inference(resolution,[],[f686,f152]) ).
fof(f692,definition,
( spl0_67
<=> point_equal(c2,ab) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f693,plain,
( point_equal(c2,ab)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f695,definition,
( spl0_68
<=> incident(c2,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f696,plain,
( ~ incident(c2,a2b2)
| spl0_68 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f697,plain,
( spl0_67
| ~ spl0_68
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f690,f151,f695,f692]) ).
fof(f699,definition,
( spl0_69
<=> point_equal(b1,ab) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f700,plain,
( point_equal(b1,ab)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f701,plain,
( spl0_69
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f689,f228,f699]) ).
fof(f713,plain,
! [X0] :
( ~ incident(X0,a2b2)
| ~ incident(X0,oa)
| line_equal(a2b2,oa)
| point_equal(X0,a2) ),
inference(resolution,[],[f280,f92]) ).
fof(f717,definition,
( spl0_70
<=> line_equal(a2b2,oa) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f718,plain,
( line_equal(a2b2,oa)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f720,definition,
( spl0_71
<=> ! [X0] :
( ~ incident(X0,a2b2)
| point_equal(X0,a2)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f721,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a2)
| ~ incident(X0,a2b2) )
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f722,plain,
( spl0_70
| spl0_71 ),
inference(avatar_split_clause,[],[f713,f720,f717]) ).
fof(f732,plain,
( line_equal(oa,a2b2)
| ~ spl0_70 ),
inference(resolution,[],[f718,f129]) ).
fof(f745,plain,
( ! [X0] :
( ~ incident(ab,X0)
| incident(b1,X0) )
| ~ spl0_69 ),
inference(resolution,[],[f700,f131]) ).
fof(f757,plain,
( incident(b1,a2b2)
| ~ spl0_69 ),
inference(resolution,[],[f745,f116]) ).
fof(f788,plain,
( ! [X0] :
( ~ incident(X0,a2b2)
| ~ incident(X0,a1c1)
| line_equal(a2b2,a1c1)
| point_equal(X0,b2) )
| ~ spl0_5 ),
inference(resolution,[],[f283,f93]) ).
fof(f793,definition,
( spl0_76
<=> line_equal(a2b2,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f794,plain,
( line_equal(a2b2,a1c1)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f796,definition,
( spl0_77
<=> ! [X0] :
( ~ incident(X0,a2b2)
| point_equal(X0,b2)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f797,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,b2)
| ~ incident(X0,a2b2) )
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f798,plain,
( spl0_76
| spl0_77
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f788,f158,f796,f793]) ).
fof(f800,definition,
( spl0_78
<=> line_equal(b2c2,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f801,plain,
( line_equal(b2c2,a1c1)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f809,plain,
( line_equal(a1c1,b2c2)
| ~ spl0_78 ),
inference(resolution,[],[f801,f129]) ).
fof(f811,plain,
( ! [X0] :
( ~ incident(X0,b2c2)
| ~ incident(X0,a1b1)
| line_equal(b2c2,a1b1)
| point_equal(X0,a1) )
| ~ spl0_6 ),
inference(resolution,[],[f162,f269]) ).
fof(f812,plain,
( ! [X0] :
( ~ incident(X0,b2c2)
| ~ incident(X0,a1c1)
| line_equal(b2c2,a1c1)
| point_equal(X0,a1) )
| ~ spl0_6 ),
inference(resolution,[],[f162,f268]) ).
fof(f813,plain,
( ! [X0] :
( ~ incident(X0,b2c2)
| ~ incident(X0,oa)
| line_equal(b2c2,oa)
| point_equal(X0,a1) )
| ~ spl0_6 ),
inference(resolution,[],[f162,f270]) ).
fof(f817,definition,
( spl0_80
<=> line_equal(b2c2,oa) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f818,plain,
( line_equal(b2c2,oa)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f820,definition,
( spl0_81
<=> ! [X0] :
( ~ incident(X0,b2c2)
| point_equal(X0,a1)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f821,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f822,plain,
( spl0_80
| spl0_81
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f813,f161,f820,f817]) ).
fof(f824,definition,
( spl0_82
<=> ! [X0] :
( ~ incident(X0,b2c2)
| point_equal(X0,a1)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f825,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f826,plain,
( spl0_78
| spl0_82
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f812,f161,f824,f800]) ).
fof(f828,definition,
( spl0_83
<=> line_equal(b2c2,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f829,plain,
( line_equal(b2c2,a1b1)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f831,definition,
( spl0_84
<=> ! [X0] :
( ~ incident(X0,b2c2)
| point_equal(X0,a1)
| ~ incident(X0,a1b1) ) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f832,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f833,plain,
( spl0_83
| spl0_84
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f811,f161,f831,f828]) ).
fof(f837,plain,
( line_equal(oa,b2c2)
| ~ spl0_80 ),
inference(resolution,[],[f818,f129]) ).
fof(f840,plain,
( point_equal(a1,b2)
| ~ incident(a1,a2b2)
| ~ spl0_77 ),
inference(resolution,[],[f797,f94]) ).
fof(f841,plain,
( point_equal(c1,b2)
| ~ incident(c1,a2b2)
| ~ spl0_77 ),
inference(resolution,[],[f797,f95]) ).
fof(f842,plain,
( point_equal(c1,b2)
| ~ spl0_2
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f841,f148]) ).
fof(f847,plain,
( $false
| ~ spl0_2
| spl0_43
| ~ spl0_77 ),
inference(unit_resulting_resolution,[],[f131,f101,f475,f842]) ).
fof(f851,plain,
( ~ spl0_2
| spl0_43
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f847]) ).
fof(f854,plain,
( point_equal(o,a1)
| ~ incident(o,b2c2)
| ~ spl0_81 ),
inference(resolution,[],[f821,f102]) ).
fof(f856,definition,
( spl0_86
<=> incident(o,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f857,plain,
( ~ incident(o,b2c2)
| spl0_86 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f859,definition,
( spl0_87
<=> point_equal(o,a1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f860,plain,
( point_equal(o,a1)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f881,plain,
( ~ incident(b1,b2c2)
| line_equal(b2c2,ob)
| ~ spl0_66 ),
inference(resolution,[],[f653,f101]) ).
fof(f885,definition,
( spl0_90
<=> line_equal(b2c2,ob) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f886,plain,
( line_equal(b2c2,ob)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f885]) ).
fof(f888,definition,
( spl0_91
<=> incident(b1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f889,plain,
( ~ incident(b1,b2c2)
| spl0_91 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f890,plain,
( spl0_90
| ~ spl0_91
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f881,f652,f888,f885]) ).
fof(f895,definition,
( spl0_92
<=> incident(ac,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f896,plain,
( ~ incident(ac,b2c2)
| spl0_92 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f898,definition,
( spl0_93
<=> point_equal(ac,a1) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f899,plain,
( point_equal(ac,a1)
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f904,plain,
( point_equal(c2,a1)
| ~ incident(c2,b2c2)
| ~ spl0_3
| ~ spl0_84 ),
inference(resolution,[],[f832,f152]) ).
fof(f905,plain,
( point_equal(c2,a1)
| ~ spl0_3
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f904,f100]) ).
fof(f907,definition,
( spl0_94
<=> incident(ab,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f908,plain,
( ~ incident(ab,b2c2)
| spl0_94 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f910,definition,
( spl0_95
<=> point_equal(ab,a1) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f911,plain,
( point_equal(ab,a1)
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f914,plain,
( $false
| ~ spl0_3
| spl0_58
| ~ spl0_84 ),
inference(unit_resulting_resolution,[],[f131,f94,f617,f905]) ).
fof(f919,plain,
( ~ spl0_3
| spl0_58
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f914]) ).
fof(f921,plain,
( $false
| spl0_60
| ~ spl0_76 ),
inference(unit_resulting_resolution,[],[f132,f624,f92,f794]) ).
fof(f924,plain,
( line_equal(a1c1,a2b2)
| ~ spl0_76 ),
inference(resolution,[],[f794,f129]) ).
fof(f926,plain,
( spl0_60
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f921]) ).
fof(f927,plain,
( ! [X0] :
( ~ incident(ac,X0)
| incident(a2,X0) )
| ~ spl0_59 ),
inference(resolution,[],[f621,f131]) ).
fof(f929,plain,
( point_equal(ac,a2)
| ~ spl0_59 ),
inference(resolution,[],[f621,f126]) ).
fof(f932,plain,
( ! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1c1)
| line_equal(X0,a1c1)
| point_equal(X1,b2) )
| ~ spl0_5 ),
inference(resolution,[],[f159,f133]) ).
fof(f935,plain,
( $false
| spl0_8
| ~ spl0_76 ),
inference(unit_resulting_resolution,[],[f132,f185,f113,f924]) ).
fof(f940,plain,
( spl0_8
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f935]) ).
fof(f943,definition,
( spl0_96
<=> point_equal(a1,ab) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f944,plain,
( point_equal(a1,ab)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f943]) ).
fof(f945,plain,
( spl0_96
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f688,f225,f943]) ).
fof(f948,plain,
( point_equal(ab,a1)
| ~ spl0_96 ),
inference(resolution,[],[f944,f126]) ).
fof(f949,plain,
( spl0_95
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f948,f943,f910]) ).
fof(f974,plain,
( $false
| ~ spl0_6
| spl0_94
| ~ spl0_95 ),
inference(unit_resulting_resolution,[],[f131,f911,f908,f162]) ).
fof(f981,plain,
( ~ spl0_6
| spl0_94
| ~ spl0_95 ),
inference(avatar_contradiction_clause,[],[f974]) ).
fof(f991,plain,
( $false
| ~ spl0_6
| spl0_17
| ~ spl0_44 ),
inference(unit_resulting_resolution,[],[f132,f254,f162,f478]) ).
fof(f994,plain,
( line_equal(oc,b2c2)
| ~ spl0_44 ),
inference(resolution,[],[f478,f129]) ).
fof(f995,plain,
( ~ spl0_6
| spl0_17
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f991]) ).
fof(f996,plain,
( ! [X0] :
( ~ incident(ab,X0)
| incident(a1,X0) )
| ~ spl0_96 ),
inference(resolution,[],[f944,f131]) ).
fof(f1010,plain,
( $false
| spl0_9
| ~ spl0_83 ),
inference(unit_resulting_resolution,[],[f132,f193,f112,f829]) ).
fof(f1013,plain,
( line_equal(a1b1,b2c2)
| ~ spl0_83 ),
inference(resolution,[],[f829,f129]) ).
fof(f1014,plain,
( spl0_9
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f1010]) ).
fof(f1028,plain,
( incident(a1,a2b2)
| ~ spl0_96 ),
inference(resolution,[],[f996,f116]) ).
fof(f1043,plain,
( incident(a2,a1c1)
| ~ spl0_59 ),
inference(resolution,[],[f927,f113]) ).
fof(f1051,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,a2b2)
| line_equal(oc,a2b2)
| point_equal(X0,c1) )
| ~ spl0_2 ),
inference(resolution,[],[f274,f109]) ).
fof(f1054,definition,
( spl0_102
<=> line_equal(oc,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f1055,plain,
( line_equal(oc,a2b2)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1057,definition,
( spl0_103
<=> ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f1058,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) )
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f1057]) ).
fof(f1059,plain,
( spl0_102
| spl0_103
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1051,f147,f1057,f1054]) ).
fof(f1061,definition,
( spl0_104
<=> line_equal(b1c1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f1062,plain,
( line_equal(b1c1,a2b2)
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f1061]) ).
fof(f1076,plain,
( point_equal(o,c1)
| ~ incident(o,a2b2)
| ~ spl0_103 ),
inference(resolution,[],[f1058,f104]) ).
fof(f1085,definition,
( spl0_106
<=> line_equal(a1b1,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f1086,plain,
( line_equal(a1b1,b1c1)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1091,plain,
( $false
| ~ spl0_106 ),
inference(unit_resulting_resolution,[],[f132,f209,f90,f1086]) ).
fof(f1095,plain,
~ spl0_106,
inference(avatar_contradiction_clause,[],[f1091]) ).
fof(f1100,plain,
! [X0] :
( ~ incident(bc,X0)
| line_equal(X0,b1c1)
| ~ incident(c1,X0)
| point_equal(bc,c1) ),
inference(resolution,[],[f275,f111]) ).
fof(f1101,plain,
! [X0] :
( ~ incident(b1,X0)
| line_equal(X0,b1c1)
| ~ incident(c1,X0)
| point_equal(b1,c1) ),
inference(resolution,[],[f275,f99]) ).
fof(f1105,definition,
( spl0_108
<=> point_equal(b1,c1) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f1106,plain,
( point_equal(b1,c1)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1108,definition,
( spl0_109
<=> ! [X0] :
( ~ incident(b1,X0)
| ~ incident(c1,X0)
| line_equal(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f1109,plain,
( ! [X0] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| line_equal(X0,b1c1) )
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f1108]) ).
fof(f1110,plain,
( spl0_108
| spl0_109 ),
inference(avatar_split_clause,[],[f1101,f1108,f1105]) ).
fof(f1112,definition,
( spl0_110
<=> point_equal(bc,c1) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f1113,plain,
( point_equal(bc,c1)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1115,definition,
( spl0_111
<=> ! [X0] :
( ~ incident(bc,X0)
| ~ incident(c1,X0)
| line_equal(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f1116,plain,
( ! [X0] :
( ~ incident(bc,X0)
| ~ incident(c1,X0)
| line_equal(X0,b1c1) )
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f1115]) ).
fof(f1117,plain,
( spl0_110
| spl0_111 ),
inference(avatar_split_clause,[],[f1100,f1115,f1112]) ).
fof(f1118,plain,
( $false
| ~ spl0_2
| spl0_7
| ~ spl0_110 ),
inference(unit_resulting_resolution,[],[f131,f148,f182,f1113]) ).
fof(f1123,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f1118]) ).
fof(f1131,plain,
( $false
| spl0_8
| ~ spl0_59 ),
inference(unit_resulting_resolution,[],[f131,f92,f929,f185]) ).
fof(f1132,plain,
( spl0_8
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f1131]) ).
fof(f1133,plain,
( ! [X0] :
( ~ incident(a2,X0)
| line_equal(X0,b1c1)
| ~ incident(c1,X0)
| point_equal(a2,c1) )
| ~ spl0_1 ),
inference(resolution,[],[f145,f275]) ).
fof(f1136,plain,
( ! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b1c1)
| line_equal(X0,b1c1)
| point_equal(X1,a2) )
| ~ spl0_1 ),
inference(resolution,[],[f145,f133]) ).
fof(f1142,definition,
( spl0_114
<=> ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,a2)
| ~ incident(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f1143,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) )
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1147,definition,
( spl0_115
<=> point_equal(a2,c1) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f1148,plain,
( point_equal(a2,c1)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1150,definition,
( spl0_116
<=> ! [X0] :
( ~ incident(a2,X0)
| ~ incident(c1,X0)
| line_equal(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f1151,plain,
( ! [X0] :
( ~ incident(c1,X0)
| ~ incident(a2,X0)
| line_equal(X0,b1c1) )
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f1150]) ).
fof(f1152,plain,
( spl0_115
| spl0_116
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1133,f144,f1150,f1147]) ).
fof(f1158,plain,
( ! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2c2)
| line_equal(X0,a2c2)
| point_equal(X1,b1) )
| ~ spl0_4 ),
inference(resolution,[],[f155,f133]) ).
fof(f1161,definition,
( spl0_117
<=> line_equal(a2c2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f1162,plain,
( line_equal(a2c2,b1c1)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f1161]) ).
fof(f1164,definition,
( spl0_118
<=> ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,b1)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f1165,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,b1)
| ~ incident(X0,a2c2) )
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1191,plain,
( ~ incident(a2,oc)
| line_equal(oc,b1c1)
| ~ spl0_116 ),
inference(resolution,[],[f1151,f109]) ).
fof(f1200,definition,
( spl0_121
<=> incident(o,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1201,plain,
( ~ incident(o,a2c2)
| spl0_121 ),
inference(avatar_component_clause,[],[f1200]) ).
fof(f1203,definition,
( spl0_122
<=> point_equal(o,b1) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f1204,plain,
( point_equal(o,b1)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f1203]) ).
fof(f1213,plain,
( point_equal(a2,b1)
| ~ incident(a2,a2c2)
| ~ spl0_1
| ~ spl0_118 ),
inference(resolution,[],[f1165,f145]) ).
fof(f1214,plain,
( point_equal(a2,b1)
| ~ spl0_1
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f1213,f96]) ).
fof(f1232,definition,
( spl0_126
<=> point_equal(a1,b1) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f1233,plain,
( point_equal(a1,b1)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f1232]) ).
fof(f1244,plain,
( ~ incident(b1,oc)
| line_equal(oc,b1c1)
| ~ spl0_109 ),
inference(resolution,[],[f1109,f109]) ).
fof(f1246,definition,
( spl0_129
<=> line_equal(oc,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f1247,plain,
( line_equal(oc,b1c1)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f1246]) ).
fof(f1252,plain,
( $false
| ~ spl0_1
| spl0_13
| ~ spl0_118 ),
inference(unit_resulting_resolution,[],[f131,f91,f235,f1214]) ).
fof(f1256,plain,
( ~ spl0_1
| spl0_13
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f1252]) ).
fof(f1260,plain,
! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,a1c1)
| line_equal(b1c1,a1c1)
| point_equal(X0,c1) ),
inference(resolution,[],[f276,f98]) ).
fof(f1262,plain,
! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,a1c1)
| line_equal(oc,a1c1)
| point_equal(X0,c1) ),
inference(resolution,[],[f276,f109]) ).
fof(f1265,definition,
( spl0_130
<=> line_equal(oc,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f1266,plain,
( line_equal(oc,a1c1)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f1265]) ).
fof(f1268,definition,
( spl0_131
<=> ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c1)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1269,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c1)
| ~ incident(X0,a1c1) )
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f1268]) ).
fof(f1270,plain,
( spl0_130
| spl0_131 ),
inference(avatar_split_clause,[],[f1262,f1268,f1265]) ).
fof(f1272,definition,
( spl0_132
<=> line_equal(b1c1,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1273,plain,
( line_equal(b1c1,a1c1)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f1272]) ).
fof(f1275,definition,
( spl0_133
<=> ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,c1)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1276,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,c1)
| ~ incident(X0,b1c1) )
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1277,plain,
( spl0_132
| spl0_133 ),
inference(avatar_split_clause,[],[f1260,f1275,f1272]) ).
fof(f1278,plain,
( $false
| ~ spl0_132 ),
inference(unit_resulting_resolution,[],[f132,f214,f99,f1273]) ).
fof(f1283,plain,
~ spl0_132,
inference(avatar_contradiction_clause,[],[f1278]) ).
fof(f1288,plain,
! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a2b2)
| line_equal(ob,a2b2)
| point_equal(X0,b2) ),
inference(resolution,[],[f282,f108]) ).
fof(f1309,plain,
! [X0] :
( ~ incident(X0,b2c2)
| ~ incident(X0,a2c2)
| line_equal(b2c2,a2c2)
| point_equal(X0,c2) ),
inference(resolution,[],[f286,f100]) ).
fof(f1314,definition,
( spl0_136
<=> line_equal(oc,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1315,plain,
( line_equal(oc,a2c2)
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1321,definition,
( spl0_138
<=> line_equal(b2c2,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1322,plain,
( line_equal(b2c2,a2c2)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1324,definition,
( spl0_139
<=> ! [X0] :
( ~ incident(X0,b2c2)
| point_equal(X0,c2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1325,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,c2)
| ~ incident(X0,b2c2) )
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1326,plain,
( spl0_138
| spl0_139 ),
inference(avatar_split_clause,[],[f1309,f1324,f1321]) ).
fof(f1329,plain,
( $false
| ~ spl0_138 ),
inference(unit_resulting_resolution,[],[f132,f200,f101,f1322]) ).
fof(f1335,plain,
~ spl0_138,
inference(avatar_contradiction_clause,[],[f1329]) ).
fof(f1337,plain,
( $false
| spl0_121
| ~ spl0_136 ),
inference(unit_resulting_resolution,[],[f132,f1201,f104,f1315]) ).
fof(f1342,plain,
( spl0_121
| ~ spl0_136 ),
inference(avatar_contradiction_clause,[],[f1337]) ).
fof(f1346,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,a2b2)
| line_equal(b1c1,a2b2)
| point_equal(X0,a2) )
| ~ spl0_1 ),
inference(resolution,[],[f279,f145]) ).
fof(f1350,definition,
( spl0_140
<=> ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,a2)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1351,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,a2)
| ~ incident(X0,a2b2) )
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f1350]) ).
fof(f1352,plain,
( spl0_104
| spl0_140
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1346,f144,f1350,f1061]) ).
fof(f1361,plain,
( point_equal(b1,a2)
| ~ incident(b1,a2b2)
| ~ spl0_140 ),
inference(resolution,[],[f1351,f99]) ).
fof(f1379,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,a2c2)
| line_equal(b1c1,a2c2)
| point_equal(X0,a2) )
| ~ spl0_1 ),
inference(resolution,[],[f278,f145]) ).
fof(f1385,plain,
! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,b2c2)
| line_equal(ob,b2c2)
| point_equal(X0,b2) ),
inference(resolution,[],[f281,f108]) ).
fof(f1388,definition,
( spl0_144
<=> line_equal(ob,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1389,plain,
( line_equal(ob,b2c2)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1391,definition,
( spl0_145
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1392,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,b2c2) )
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f1391]) ).
fof(f1393,plain,
( spl0_144
| spl0_145 ),
inference(avatar_split_clause,[],[f1385,f1391,f1388]) ).
fof(f1394,plain,
( $false
| spl0_91
| ~ spl0_144 ),
inference(unit_resulting_resolution,[],[f132,f889,f107,f1389]) ).
fof(f1395,plain,
( $false
| spl0_86
| ~ spl0_144 ),
inference(unit_resulting_resolution,[],[f132,f857,f103,f1389]) ).
fof(f1399,plain,
( spl0_91
| ~ spl0_144 ),
inference(avatar_contradiction_clause,[],[f1394]) ).
fof(f1400,plain,
( spl0_86
| ~ spl0_144 ),
inference(avatar_contradiction_clause,[],[f1395]) ).
fof(f1404,plain,
! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b2c2)
| line_equal(oc,b2c2)
| point_equal(X0,c2) ),
inference(resolution,[],[f285,f110]) ).
fof(f1407,definition,
( spl0_146
<=> line_equal(oc,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1408,plain,
( line_equal(oc,b2c2)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f1407]) ).
fof(f1410,definition,
( spl0_147
<=> ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c2)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1411,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c2)
| ~ incident(X0,b2c2) )
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1410]) ).
fof(f1412,plain,
( spl0_146
| spl0_147 ),
inference(avatar_split_clause,[],[f1404,f1410,f1407]) ).
fof(f1413,plain,
( $false
| spl0_43
| ~ spl0_146 ),
inference(unit_resulting_resolution,[],[f132,f475,f109,f1408]) ).
fof(f1414,plain,
( $false
| spl0_86
| ~ spl0_146 ),
inference(unit_resulting_resolution,[],[f132,f857,f104,f1408]) ).
fof(f1417,plain,
( line_equal(b2c2,oc)
| ~ spl0_146 ),
inference(resolution,[],[f1408,f129]) ).
fof(f1418,plain,
( spl0_43
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f1413]) ).
fof(f1419,plain,
( spl0_86
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f1414]) ).
fof(f1420,plain,
( spl0_44
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f1417,f1407,f477]) ).
fof(f1437,definition,
( spl0_148
<=> line_equal(a1b1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1438,plain,
( line_equal(a1b1,b2c2)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f1437]) ).
fof(f1458,definition,
( spl0_150
<=> line_equal(oa,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1459,plain,
( line_equal(oa,b2c2)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1458]) ).
fof(f1467,plain,
( $false
| spl0_91
| ~ spl0_148 ),
inference(unit_resulting_resolution,[],[f132,f889,f91,f1438]) ).
fof(f1470,plain,
( line_equal(b2c2,a1b1)
| ~ spl0_148 ),
inference(resolution,[],[f1438,f129]) ).
fof(f1471,plain,
( spl0_91
| ~ spl0_148 ),
inference(avatar_contradiction_clause,[],[f1467]) ).
fof(f1472,plain,
( spl0_83
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f1470,f1437,f828]) ).
fof(f1527,plain,
( point_equal(a1,b2)
| ~ spl0_77
| ~ spl0_96 ),
inference(forward_subsumption_resolution,[],[f840,f1028]) ).
fof(f1533,plain,
( ! [X0] :
( ~ incident(ac,X0)
| incident(c2,X0) )
| ~ spl0_57 ),
inference(resolution,[],[f614,f131]) ).
fof(f1535,plain,
( point_equal(ac,c2)
| ~ spl0_57 ),
inference(resolution,[],[f614,f126]) ).
fof(f1543,plain,
( $false
| spl0_43
| ~ spl0_78 ),
inference(unit_resulting_resolution,[],[f132,f475,f95,f809]) ).
fof(f1548,plain,
( spl0_43
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f1543]) ).
fof(f1550,plain,
( $false
| spl0_6
| ~ spl0_77
| ~ spl0_96 ),
inference(unit_resulting_resolution,[],[f131,f101,f1527,f173]) ).
fof(f1551,plain,
( spl0_6
| ~ spl0_77
| ~ spl0_96 ),
inference(avatar_contradiction_clause,[],[f1550]) ).
fof(f1555,plain,
( $false
| ~ spl0_57
| spl0_92 ),
inference(unit_resulting_resolution,[],[f131,f100,f896,f1535]) ).
fof(f1559,plain,
( ~ spl0_57
| spl0_92 ),
inference(avatar_contradiction_clause,[],[f1555]) ).
fof(f1564,plain,
( incident(c2,a1c1)
| ~ spl0_57 ),
inference(resolution,[],[f1533,f113]) ).
fof(f1569,plain,
( line_equal(a1c1,oc)
| ~ incident(c1,a1c1)
| ~ spl0_57 ),
inference(resolution,[],[f1564,f447]) ).
fof(f1574,plain,
( line_equal(a1c1,oc)
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f1569,f95]) ).
fof(f1586,plain,
( line_equal(oc,a1c1)
| ~ spl0_57 ),
inference(resolution,[],[f1574,f129]) ).
fof(f1588,plain,
( spl0_130
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f1586,f613,f1265]) ).
fof(f1605,plain,
( ~ incident(c1,b2c2)
| line_equal(b2c2,b1c1)
| ~ spl0_111 ),
inference(resolution,[],[f1116,f112]) ).
fof(f1620,plain,
( point_equal(c2,bc)
| ~ incident(c2,b1c1)
| ~ spl0_56 ),
inference(resolution,[],[f596,f100]) ).
fof(f1622,definition,
( spl0_161
<=> incident(c2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1623,plain,
( ~ incident(c2,b1c1)
| spl0_161 ),
inference(avatar_component_clause,[],[f1622]) ).
fof(f1625,definition,
( spl0_162
<=> point_equal(c2,bc) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1626,plain,
( point_equal(c2,bc)
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1627,plain,
( ~ spl0_161
| spl0_162
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f1620,f595,f1625,f1622]) ).
fof(f1633,plain,
( $false
| ~ spl0_129
| spl0_161 ),
inference(unit_resulting_resolution,[],[f132,f1247,f110,f1623]) ).
fof(f1635,plain,
( ~ spl0_129
| spl0_161 ),
inference(avatar_contradiction_clause,[],[f1633]) ).
fof(f1650,definition,
( spl0_163
<=> line_equal(ob,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1651,plain,
( line_equal(ob,a2b2)
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f1650]) ).
fof(f1653,definition,
( spl0_164
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1654,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,a2b2) )
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f1653]) ).
fof(f1655,plain,
( spl0_163
| spl0_164 ),
inference(avatar_split_clause,[],[f1288,f1653,f1650]) ).
fof(f1657,plain,
( $false
| spl0_12
| ~ spl0_163 ),
inference(unit_resulting_resolution,[],[f132,f229,f107,f1651]) ).
fof(f1662,plain,
( spl0_12
| ~ spl0_163 ),
inference(avatar_contradiction_clause,[],[f1657]) ).
fof(f1668,definition,
( spl0_165
<=> incident(o,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1669,plain,
( ~ incident(o,b1c1)
| spl0_165 ),
inference(avatar_component_clause,[],[f1668]) ).
fof(f1672,plain,
( $false
| ~ spl0_129
| spl0_165 ),
inference(unit_resulting_resolution,[],[f132,f1247,f104,f1669]) ).
fof(f1673,plain,
( $false
| ~ spl0_35
| spl0_165 ),
inference(unit_resulting_resolution,[],[f131,f98,f442,f1669]) ).
fof(f1674,plain,
( ~ spl0_129
| spl0_165 ),
inference(avatar_contradiction_clause,[],[f1672]) ).
fof(f1675,plain,
( ~ spl0_35
| spl0_165 ),
inference(avatar_contradiction_clause,[],[f1673]) ).
fof(f1682,plain,
( point_equal(a2,a1)
| ~ incident(a2,a1c1)
| ~ spl0_32 ),
inference(resolution,[],[f406,f106]) ).
fof(f1683,plain,
( point_equal(o,a1)
| ~ incident(o,a1c1)
| ~ spl0_32 ),
inference(resolution,[],[f406,f102]) ).
fof(f1685,definition,
( spl0_166
<=> incident(o,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1686,plain,
( ~ incident(o,a1c1)
| spl0_166 ),
inference(avatar_component_clause,[],[f1685]) ).
fof(f1704,definition,
( spl0_167
<=> point_equal(o,a2) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1705,plain,
( point_equal(o,a2)
| ~ spl0_167 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1709,plain,
( point_equal(a2,o)
| ~ spl0_167 ),
inference(resolution,[],[f1705,f126]) ).
fof(f1711,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,a2c2)
| line_equal(b1c1,a2c2)
| point_equal(X0,b1) )
| ~ spl0_4 ),
inference(resolution,[],[f1158,f99]) ).
fof(f1713,plain,
( ! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a2c2)
| line_equal(ob,a2c2)
| point_equal(X0,b1) )
| ~ spl0_4 ),
inference(resolution,[],[f1158,f107]) ).
fof(f1726,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| ~ incident(X0,b1c1)
| line_equal(a2c2,b1c1)
| point_equal(X0,a2) )
| ~ spl0_1 ),
inference(resolution,[],[f1136,f96]) ).
fof(f1729,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,b1c1)
| line_equal(oa,b1c1)
| point_equal(X0,a2) )
| ~ spl0_1 ),
inference(resolution,[],[f1136,f106]) ).
fof(f1732,plain,
( point_equal(a2,a1)
| ~ incident(a2,a1b1)
| ~ spl0_30 ),
inference(resolution,[],[f399,f106]) ).
fof(f1735,definition,
( spl0_168
<=> incident(o,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1736,plain,
( ~ incident(o,a1b1)
| spl0_168 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1744,plain,
( $false
| spl0_121
| ~ spl0_167 ),
inference(unit_resulting_resolution,[],[f131,f96,f1705,f1201]) ).
fof(f1745,plain,
( spl0_121
| ~ spl0_167 ),
inference(avatar_contradiction_clause,[],[f1744]) ).
fof(f1748,definition,
( spl0_169
<=> line_equal(ob,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1749,plain,
( line_equal(ob,a2c2)
| ~ spl0_169 ),
inference(avatar_component_clause,[],[f1748]) ).
fof(f1750,plain,
( spl0_169
| spl0_54
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1713,f154,f567,f1748]) ).
fof(f1751,plain,
( $false
| ~ spl0_169 ),
inference(unit_resulting_resolution,[],[f132,f200,f108,f1749]) ).
fof(f1755,plain,
~ spl0_169,
inference(avatar_contradiction_clause,[],[f1751]) ).
fof(f1766,plain,
( point_equal(o,b1)
| ~ incident(o,a2c2)
| ~ spl0_54 ),
inference(resolution,[],[f568,f103]) ).
fof(f1770,plain,
( ! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a1c1)
| line_equal(ob,a1c1)
| point_equal(X0,b2) )
| ~ spl0_5 ),
inference(resolution,[],[f932,f108]) ).
fof(f1773,definition,
( spl0_170
<=> line_equal(ob,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1774,plain,
( line_equal(ob,a1c1)
| ~ spl0_170 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1776,definition,
( spl0_171
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,a1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1777,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,a1c1) )
| ~ spl0_171 ),
inference(avatar_component_clause,[],[f1776]) ).
fof(f1778,plain,
( spl0_170
| spl0_171
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1770,f158,f1776,f1773]) ).
fof(f1779,plain,
( $false
| ~ spl0_170 ),
inference(unit_resulting_resolution,[],[f132,f214,f107,f1774]) ).
fof(f1783,plain,
~ spl0_170,
inference(avatar_contradiction_clause,[],[f1779]) ).
fof(f1786,plain,
( point_equal(o,b2)
| ~ incident(o,a1c1)
| ~ spl0_171 ),
inference(resolution,[],[f1777,f103]) ).
fof(f1787,plain,
( ~ spl0_166
| spl0_61
| ~ spl0_171 ),
inference(avatar_split_clause,[],[f1786,f1776,f635,f1685]) ).
fof(f1788,plain,
( $false
| ~ spl0_61
| spl0_86 ),
inference(unit_resulting_resolution,[],[f131,f101,f857,f636]) ).
fof(f1791,plain,
( point_equal(b2,o)
| ~ spl0_61 ),
inference(resolution,[],[f636,f126]) ).
fof(f1792,plain,
( ~ spl0_61
| spl0_86 ),
inference(avatar_contradiction_clause,[],[f1788]) ).
fof(f1799,plain,
( point_equal(b1,b2)
| ~ incident(b1,a2b2)
| ~ spl0_164 ),
inference(resolution,[],[f1654,f107]) ).
fof(f1804,plain,
( point_equal(o,b2)
| ~ incident(o,b2c2)
| ~ spl0_145 ),
inference(resolution,[],[f1392,f103]) ).
fof(f1807,plain,
( point_equal(o,c2)
| ~ incident(o,b2c2)
| ~ spl0_147 ),
inference(resolution,[],[f1411,f104]) ).
fof(f1808,plain,
( ~ spl0_86
| spl0_45
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1807,f1410,f497,f856]) ).
fof(f1811,definition,
( spl0_172
<=> incident(o,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f1812,plain,
( ~ incident(o,a2b2)
| spl0_172 ),
inference(avatar_component_clause,[],[f1811]) ).
fof(f1818,plain,
( point_equal(o,a2)
| ~ incident(o,b1c1)
| ~ spl0_114 ),
inference(resolution,[],[f1143,f102]) ).
fof(f1820,plain,
( $false
| ~ spl0_108 ),
inference(unit_resulting_resolution,[],[f131,f95,f214,f1106]) ).
fof(f1824,plain,
~ spl0_108,
inference(avatar_contradiction_clause,[],[f1820]) ).
fof(f1825,plain,
( spl0_129
| ~ spl0_18
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f1244,f1108,f256,f1246]) ).
fof(f1827,plain,
( $false
| spl0_15
| ~ spl0_42 ),
inference(unit_resulting_resolution,[],[f132,f244,f96,f471]) ).
fof(f1830,plain,
( line_equal(oc,a2c2)
| ~ spl0_42 ),
inference(resolution,[],[f471,f129]) ).
fof(f1831,plain,
( spl0_15
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f1827]) ).
fof(f1845,plain,
( $false
| ~ spl0_167
| spl0_172 ),
inference(unit_resulting_resolution,[],[f131,f92,f1812,f1705]) ).
fof(f1849,plain,
( ~ spl0_167
| spl0_172 ),
inference(avatar_contradiction_clause,[],[f1845]) ).
fof(f1852,plain,
( point_equal(b1,a2)
| ~ spl0_69
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f1361,f757]) ).
fof(f1856,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(b1,X0) )
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1852,f131]) ).
fof(f1858,plain,
( point_equal(a2,b1)
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1852,f126]) ).
fof(f1922,plain,
( ~ spl0_86
| spl0_61
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f1804,f1391,f635,f856]) ).
fof(f1923,plain,
( $false
| ~ spl0_5
| ~ spl0_61
| spl0_166 ),
inference(unit_resulting_resolution,[],[f131,f159,f1686,f636]) ).
fof(f1927,plain,
( ~ spl0_5
| ~ spl0_61
| spl0_166 ),
inference(avatar_contradiction_clause,[],[f1923]) ).
fof(f1937,plain,
( incident(b1,oa)
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1856,f106]) ).
fof(f1945,plain,
( ! [X0,X1] :
( ~ incident(X1,oa)
| ~ incident(X1,X0)
| line_equal(X0,oa)
| ~ incident(b1,X0)
| point_equal(X1,b1) )
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1937,f133]) ).
fof(f1948,definition,
( spl0_178
<=> line_equal(oa,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1949,plain,
( line_equal(oa,b1c1)
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f1948]) ).
fof(f1971,plain,
( $false
| ~ spl0_178 ),
inference(unit_resulting_resolution,[],[f132,f209,f105,f1949]) ).
fof(f1975,plain,
~ spl0_178,
inference(avatar_contradiction_clause,[],[f1971]) ).
fof(f1978,plain,
( $false
| ~ spl0_126 ),
inference(unit_resulting_resolution,[],[f131,f99,f209,f1233]) ).
fof(f1983,plain,
~ spl0_126,
inference(avatar_contradiction_clause,[],[f1978]) ).
fof(f1990,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(a2,X0) )
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1858,f131]) ).
fof(f2010,plain,
( ! [X0] :
( ~ incident(a1,X0)
| line_equal(X0,oa)
| ~ incident(b1,X0)
| point_equal(a1,b1) )
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1945,f105]) ).
fof(f2016,definition,
( spl0_183
<=> ! [X0] :
( ~ incident(a1,X0)
| ~ incident(b1,X0)
| line_equal(X0,oa) ) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f2017,plain,
( ! [X0] :
( ~ incident(a1,X0)
| ~ incident(b1,X0)
| line_equal(X0,oa) )
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f2016]) ).
fof(f2018,plain,
( spl0_126
| spl0_183
| ~ spl0_69
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f2010,f1350,f699,f2016,f1232]) ).
fof(f2025,plain,
( $false
| spl0_2
| ~ spl0_104 ),
inference(unit_resulting_resolution,[],[f132,f171,f98,f1062]) ).
fof(f2029,plain,
( spl0_2
| ~ spl0_104 ),
inference(avatar_contradiction_clause,[],[f2025]) ).
fof(f2048,plain,
( ~ incident(b1,a1b1)
| line_equal(a1b1,oa)
| ~ spl0_183 ),
inference(resolution,[],[f2017,f90]) ).
fof(f2066,plain,
( $false
| ~ spl0_61
| ~ spl0_122 ),
inference(unit_resulting_resolution,[],[f127,f139,f1204,f1791]) ).
fof(f2070,plain,
( ~ spl0_61
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f2066]) ).
fof(f2072,definition,
( spl0_184
<=> point_equal(b1,a1) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f2073,plain,
( point_equal(b1,a1)
| ~ spl0_184 ),
inference(avatar_component_clause,[],[f2072]) ).
fof(f2078,plain,
( line_equal(ob,b2c2)
| ~ spl0_90 ),
inference(resolution,[],[f886,f129]) ).
fof(f2084,plain,
( $false
| ~ spl0_87
| spl0_166 ),
inference(unit_resulting_resolution,[],[f131,f94,f860,f1686]) ).
fof(f2085,plain,
( ~ spl0_87
| spl0_166 ),
inference(avatar_contradiction_clause,[],[f2084]) ).
fof(f2102,plain,
( point_equal(o,b1)
| ~ incident(o,a1b1)
| ~ spl0_50 ),
inference(resolution,[],[f535,f103]) ).
fof(f2107,plain,
( point_equal(o,c1)
| ~ incident(o,a1c1)
| ~ spl0_131 ),
inference(resolution,[],[f1269,f104]) ).
fof(f2111,plain,
( $false
| ~ spl0_29
| ~ spl0_70 ),
inference(unit_resulting_resolution,[],[f130,f135,f396,f732]) ).
fof(f2112,plain,
( $false
| spl0_11
| ~ spl0_70 ),
inference(unit_resulting_resolution,[],[f132,f226,f105,f732]) ).
fof(f2116,plain,
( ~ spl0_29
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f2111]) ).
fof(f2117,plain,
( spl0_11
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f2112]) ).
fof(f2121,plain,
( point_equal(o,a2)
| ~ incident(o,a2b2)
| ~ spl0_71 ),
inference(resolution,[],[f721,f102]) ).
fof(f2122,plain,
( $false
| spl0_15
| ~ spl0_167 ),
inference(unit_resulting_resolution,[],[f131,f104,f244,f1709]) ).
fof(f2126,plain,
( spl0_15
| ~ spl0_167 ),
inference(avatar_contradiction_clause,[],[f2122]) ).
fof(f2128,plain,
( ~ spl0_33
| spl0_24
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f422,f334,f359,f426]) ).
fof(f2129,plain,
( spl0_136
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1830,f470,f1314]) ).
fof(f2132,plain,
( spl0_144
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f2078,f885,f1388]) ).
fof(f2143,plain,
( ~ incident(c2,ob)
| line_equal(ob,oc)
| ~ spl0_46 ),
inference(resolution,[],[f501,f103]) ).
fof(f2153,plain,
( incident(a2,a1b1)
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f1990,f91]) ).
fof(f2158,plain,
( ~ incident(a2,a2b2)
| point_equal(a2,ab)
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f2153,f686]) ).
fof(f2160,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,b1c1)
| line_equal(a1b1,b1c1)
| point_equal(X0,a2) )
| ~ spl0_1
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f2153,f1136]) ).
fof(f2175,definition,
( spl0_187
<=> ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f2176,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) )
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f2175]) ).
fof(f2177,plain,
( spl0_106
| spl0_187
| ~ spl0_1
| ~ spl0_69
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f2160,f1350,f699,f144,f2175,f1085]) ).
fof(f2178,plain,
( point_equal(a2,ab)
| ~ spl0_69
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f2158,f92]) ).
fof(f2189,plain,
( point_equal(ab,a2)
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f2178,f126]) ).
fof(f2232,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(ab,X0) )
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f2189,f131]) ).
fof(f2255,plain,
( incident(ab,b1c1)
| ~ spl0_1
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f2232,f145]) ).
fof(f2296,plain,
( ~ incident(ac,b1c1)
| ~ incident(bc,b1c1)
| ~ spl0_1
| ~ spl0_69
| ~ spl0_140 ),
inference(resolution,[],[f2255,f175]) ).
fof(f2299,plain,
( ~ incident(ac,b1c1)
| ~ spl0_1
| ~ spl0_69
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f2296,f111]) ).
fof(f2318,plain,
( $false
| ~ spl0_1
| ~ spl0_69
| ~ spl0_117
| ~ spl0_140 ),
inference(unit_resulting_resolution,[],[f132,f1162,f114,f2299]) ).
fof(f2319,plain,
( ~ spl0_1
| ~ spl0_69
| ~ spl0_117
| ~ spl0_140 ),
inference(avatar_contradiction_clause,[],[f2318]) ).
fof(f2325,definition,
( spl0_203
<=> line_equal(b1c1,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f2326,plain,
( line_equal(b1c1,a2c2)
| ~ spl0_203 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2328,definition,
( spl0_204
<=> ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,a2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f2329,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) )
| ~ spl0_204 ),
inference(avatar_component_clause,[],[f2328]) ).
fof(f2330,plain,
( spl0_203
| spl0_204
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1379,f144,f2328,f2325]) ).
fof(f2331,plain,
( spl0_117
| spl0_204
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1726,f144,f2328,f1161]) ).
fof(f2344,plain,
( spl0_146
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f994,f477,f1407]) ).
fof(f2350,plain,
( spl0_203
| spl0_118
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1711,f154,f1164,f2325]) ).
fof(f2351,plain,
( spl0_55
| ~ spl0_43
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1605,f1115,f474,f592]) ).
fof(f2356,plain,
( ~ incident(a2,a1b1)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1732,f140]) ).
fof(f2359,plain,
( spl0_148
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1013,f828,f1437]) ).
fof(f2378,plain,
( line_equal(a1b1,oa)
| ~ spl0_183 ),
inference(forward_subsumption_resolution,[],[f2048,f91]) ).
fof(f2386,plain,
( spl0_29
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f2378,f2016,f395]) ).
fof(f2393,plain,
( spl0_178
| spl0_114
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1729,f144,f1142,f1948]) ).
fof(f2396,plain,
( ~ spl0_13
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f2356,f398,f234]) ).
fof(f2401,plain,
( ~ spl0_165
| spl0_167
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1818,f1142,f1704,f1668]) ).
fof(f2402,plain,
( spl0_129
| ~ spl0_15
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1191,f1150,f243,f1246]) ).
fof(f2423,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,b2c2)
| line_equal(a1b1,b2c2)
| point_equal(X0,c2) )
| ~ spl0_3 ),
inference(resolution,[],[f152,f285]) ).
fof(f2434,definition,
( spl0_210
<=> ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,c2)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f2435,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,c2)
| ~ incident(X0,b2c2) )
| ~ spl0_210 ),
inference(avatar_component_clause,[],[f2434]) ).
fof(f2436,plain,
( spl0_148
| spl0_210
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f2423,f151,f2434,f1437]) ).
fof(f2491,plain,
( $false
| spl0_10
| ~ spl0_93 ),
inference(unit_resulting_resolution,[],[f131,f90,f196,f899]) ).
fof(f2495,plain,
( spl0_10
| ~ spl0_93 ),
inference(avatar_contradiction_clause,[],[f2491]) ).
fof(f2499,plain,
( $false
| spl0_60
| ~ spl0_115 ),
inference(unit_resulting_resolution,[],[f131,f95,f624,f1148]) ).
fof(f2503,plain,
( spl0_60
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f2499]) ).
fof(f2504,plain,
( ~ incident(a2,a1c1)
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1682,f140]) ).
fof(f2510,plain,
( $false
| ~ spl0_59
| ~ spl0_93 ),
inference(unit_resulting_resolution,[],[f127,f140,f899,f621]) ).
fof(f2514,plain,
( ~ spl0_59
| ~ spl0_93 ),
inference(avatar_contradiction_clause,[],[f2510]) ).
fof(f2517,plain,
( $false
| spl0_16
| ~ spl0_44 ),
inference(unit_resulting_resolution,[],[f132,f247,f101,f478]) ).
fof(f2521,plain,
( spl0_16
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f2517]) ).
fof(f2524,plain,
( spl0_21
| ~ spl0_33
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f2143,f500,f426,f331]) ).
fof(f2525,plain,
( $false
| spl0_58
| ~ spl0_130 ),
inference(unit_resulting_resolution,[],[f132,f1266,f110,f617]) ).
fof(f2526,plain,
( spl0_58
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f2525]) ).
fof(f2527,plain,
( spl0_150
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f837,f817,f1458]) ).
fof(f2594,plain,
( $false
| ~ spl0_150 ),
inference(unit_resulting_resolution,[],[f132,f204,f106,f1459]) ).
fof(f2598,plain,
~ spl0_150,
inference(avatar_contradiction_clause,[],[f2594]) ).
fof(f2602,plain,
( ~ spl0_166
| spl0_87
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f1683,f405,f859,f1685]) ).
fof(f2603,plain,
( ~ spl0_60
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f2504,f405,f623]) ).
fof(f2604,plain,
( ~ spl0_86
| spl0_87
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f854,f820,f859,f856]) ).
fof(f2621,plain,
( $false
| ~ spl0_184 ),
inference(unit_resulting_resolution,[],[f131,f94,f214,f2073]) ).
fof(f2625,plain,
~ spl0_184,
inference(avatar_contradiction_clause,[],[f2621]) ).
fof(f2640,plain,
( $false
| ~ spl0_61
| spl0_172 ),
inference(unit_resulting_resolution,[],[f131,f93,f1812,f636]) ).
fof(f2644,plain,
( ~ spl0_61
| spl0_172 ),
inference(avatar_contradiction_clause,[],[f2640]) ).
fof(f2645,plain,
( ~ spl0_172
| spl0_167
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f2121,f720,f1704,f1811]) ).
fof(f2660,plain,
( $false
| ~ spl0_45
| spl0_121 ),
inference(unit_resulting_resolution,[],[f131,f97,f498,f1201]) ).
fof(f2661,plain,
( ~ spl0_45
| spl0_121 ),
inference(avatar_contradiction_clause,[],[f2660]) ).
fof(f2672,plain,
( $false
| ~ spl0_87
| spl0_168 ),
inference(unit_resulting_resolution,[],[f131,f90,f860,f1736]) ).
fof(f2674,plain,
( ~ spl0_87
| spl0_168 ),
inference(avatar_contradiction_clause,[],[f2672]) ).
fof(f2706,plain,
( point_equal(c2,a1)
| ~ incident(c2,b2c2)
| ~ spl0_57
| ~ spl0_82 ),
inference(resolution,[],[f825,f1564]) ).
fof(f2709,plain,
( point_equal(b1,a1)
| ~ incident(b1,b2c2)
| ~ spl0_84 ),
inference(resolution,[],[f832,f91]) ).
fof(f2714,plain,
( point_equal(ab,c2)
| ~ incident(ab,b2c2)
| ~ spl0_210 ),
inference(resolution,[],[f2435,f115]) ).
fof(f2719,definition,
( spl0_214
<=> point_equal(ab,c2) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f2720,plain,
( point_equal(ab,c2)
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f2719]) ).
fof(f2721,plain,
( ~ spl0_94
| spl0_214
| ~ spl0_210 ),
inference(avatar_split_clause,[],[f2714,f2434,f2719,f907]) ).
fof(f2724,plain,
( point_equal(c2,ab)
| ~ spl0_214 ),
inference(resolution,[],[f2720,f126]) ).
fof(f2725,plain,
( spl0_67
| ~ spl0_214 ),
inference(avatar_split_clause,[],[f2724,f2719,f692]) ).
fof(f2727,plain,
( ! [X0] :
( ~ incident(ab,X0)
| incident(c2,X0) )
| ~ spl0_67 ),
inference(resolution,[],[f693,f131]) ).
fof(f2740,definition,
( spl0_215
<=> point_equal(c2,a2) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f2741,plain,
( point_equal(c2,a2)
| ~ spl0_215 ),
inference(avatar_component_clause,[],[f2740]) ).
fof(f2744,definition,
( spl0_216
<=> incident(ac,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f2745,plain,
( ~ incident(ac,b1c1)
| spl0_216 ),
inference(avatar_component_clause,[],[f2744]) ).
fof(f2754,plain,
( point_equal(a2,c2)
| ~ spl0_215 ),
inference(resolution,[],[f2741,f126]) ).
fof(f2768,plain,
( incident(c2,a2b2)
| ~ spl0_67 ),
inference(resolution,[],[f2727,f116]) ).
fof(f2774,plain,
( ~ incident(b2,a2b2)
| ~ incident(a2,a2b2)
| ~ spl0_67 ),
inference(resolution,[],[f2768,f141]) ).
fof(f2778,plain,
( ~ incident(a2,a2b2)
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f2774,f93]) ).
fof(f2790,plain,
( $false
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f2778,f92]) ).
fof(f2791,plain,
~ spl0_67,
inference(avatar_contradiction_clause,[],[f2790]) ).
fof(f2801,definition,
( spl0_221
<=> line_equal(oc,ob) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f2802,plain,
( line_equal(oc,ob)
| ~ spl0_221 ),
inference(avatar_component_clause,[],[f2801]) ).
fof(f2804,plain,
( point_equal(c2,a1)
| ~ spl0_57
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f2706,f100]) ).
fof(f2808,plain,
( point_equal(b1,a2)
| ~ incident(b1,b1c1)
| ~ spl0_4
| ~ spl0_204 ),
inference(resolution,[],[f155,f2329]) ).
fof(f2817,plain,
( point_equal(b1,a2)
| ~ spl0_4
| ~ spl0_204 ),
inference(forward_subsumption_resolution,[],[f2808,f99]) ).
fof(f2818,plain,
( $false
| ~ spl0_117
| spl0_216 ),
inference(unit_resulting_resolution,[],[f132,f2745,f114,f1162]) ).
fof(f2822,plain,
( ~ spl0_117
| spl0_216 ),
inference(avatar_contradiction_clause,[],[f2818]) ).
fof(f2826,plain,
( $false
| ~ spl0_110
| ~ spl0_162 ),
inference(unit_resulting_resolution,[],[f127,f138,f1626,f1113]) ).
fof(f2830,plain,
( ~ spl0_110
| ~ spl0_162 ),
inference(avatar_contradiction_clause,[],[f2826]) ).
fof(f2837,plain,
( $false
| spl0_5
| ~ spl0_78 ),
inference(unit_resulting_resolution,[],[f132,f168,f101,f801]) ).
fof(f2841,plain,
( spl0_5
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f2837]) ).
fof(f2843,plain,
( ~ spl0_121
| spl0_122
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1766,f567,f1203,f1200]) ).
fof(f2844,plain,
( spl0_221
| ~ spl0_16
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f680,f638,f246,f2801]) ).
fof(f2853,plain,
( ~ spl0_91
| spl0_184
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f2709,f831,f2072,f888]) ).
fof(f2867,plain,
( line_equal(ob,oc)
| ~ spl0_221 ),
inference(resolution,[],[f2802,f129]) ).
fof(f2869,plain,
( spl0_21
| ~ spl0_221 ),
inference(avatar_split_clause,[],[f2867,f2801,f331]) ).
fof(f2881,plain,
( $false
| spl0_41
| ~ spl0_203 ),
inference(unit_resulting_resolution,[],[f132,f468,f98,f2326]) ).
fof(f2886,plain,
( spl0_41
| ~ spl0_203 ),
inference(avatar_contradiction_clause,[],[f2881]) ).
fof(f2909,plain,
( $false
| spl0_3
| ~ spl0_57
| ~ spl0_82 ),
inference(unit_resulting_resolution,[],[f131,f90,f167,f2804]) ).
fof(f2913,plain,
( spl0_3
| ~ spl0_57
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f2909]) ).
fof(f2914,plain,
( ~ spl0_166
| spl0_35
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f2107,f1268,f441,f1685]) ).
fof(f2939,plain,
( point_equal(ac,a1)
| ~ incident(ac,b2c2)
| ~ spl0_82 ),
inference(resolution,[],[f825,f113]) ).
fof(f2951,plain,
( point_equal(c2,a2)
| ~ incident(c2,b1c1)
| ~ spl0_204 ),
inference(resolution,[],[f2329,f97]) ).
fof(f2997,plain,
( point_equal(o,b2)
| ~ incident(o,a2b2)
| ~ spl0_164 ),
inference(resolution,[],[f1654,f103]) ).
fof(f3015,plain,
( point_equal(b1,a2)
| ~ incident(b1,b1c1)
| ~ spl0_187 ),
inference(resolution,[],[f2176,f91]) ).
fof(f3021,plain,
( point_equal(b1,c2)
| ~ incident(b1,b2c2)
| ~ spl0_4
| ~ spl0_139 ),
inference(resolution,[],[f1325,f155]) ).
fof(f3037,plain,
( point_equal(ac,c1)
| ~ incident(ac,b1c1)
| ~ spl0_133 ),
inference(resolution,[],[f1276,f113]) ).
fof(f3095,plain,
( ~ spl0_168
| spl0_122
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f2102,f534,f1203,f1735]) ).
fof(f3098,plain,
( point_equal(b1,b2)
| ~ spl0_69
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f1799,f757]) ).
fof(f3100,plain,
( spl0_65
| ~ spl0_69
| ~ spl0_164 ),
inference(avatar_split_clause,[],[f3098,f1653,f699,f649]) ).
fof(f3127,plain,
( $false
| ~ spl0_163
| spl0_172 ),
inference(unit_resulting_resolution,[],[f132,f1812,f103,f1651]) ).
fof(f3131,plain,
( ~ spl0_163
| spl0_172 ),
inference(avatar_contradiction_clause,[],[f3127]) ).
fof(f3133,plain,
( ~ spl0_172
| spl0_35
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f1076,f1057,f441,f1811]) ).
fof(f3136,definition,
( spl0_225
<=> point_equal(a2,c2) ),
introduced(definition,[new_symbols(definition,[spl0_225])],[avatar_definition]) ).
fof(f3137,plain,
( point_equal(a2,c2)
| ~ spl0_225 ),
inference(avatar_component_clause,[],[f3136]) ).
fof(f3140,definition,
( spl0_226
<=> point_equal(ac,c1) ),
introduced(definition,[new_symbols(definition,[spl0_226])],[avatar_definition]) ).
fof(f3141,plain,
( point_equal(ac,c1)
| ~ spl0_226 ),
inference(avatar_component_clause,[],[f3140]) ).
fof(f3142,plain,
( ~ spl0_216
| spl0_226
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f3037,f1275,f3140,f2744]) ).
fof(f3144,plain,
( point_equal(b1,a2)
| ~ spl0_187 ),
inference(forward_subsumption_resolution,[],[f3015,f99]) ).
fof(f3158,plain,
( $false
| spl0_68
| ~ spl0_102 ),
inference(unit_resulting_resolution,[],[f132,f1055,f110,f696]) ).
fof(f3159,plain,
( spl0_68
| ~ spl0_102 ),
inference(avatar_contradiction_clause,[],[f3158]) ).
fof(f3194,definition,
( spl0_229
<=> point_equal(c2,b1) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f3195,plain,
( point_equal(c2,b1)
| ~ spl0_229 ),
inference(avatar_component_clause,[],[f3194]) ).
fof(f3234,plain,
( ~ spl0_161
| spl0_215
| ~ spl0_204 ),
inference(avatar_split_clause,[],[f2951,f2328,f2740,f1622]) ).
fof(f3244,definition,
( spl0_230
<=> point_equal(b1,c2) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f3245,plain,
( point_equal(b1,c2)
| ~ spl0_230 ),
inference(avatar_component_clause,[],[f3244]) ).
fof(f3246,plain,
( ~ spl0_91
| spl0_230
| ~ spl0_4
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f3021,f1324,f154,f3244,f888]) ).
fof(f3307,plain,
( $false
| ~ spl0_225 ),
inference(unit_resulting_resolution,[],[f131,f100,f204,f3137]) ).
fof(f3311,plain,
~ spl0_225,
inference(avatar_contradiction_clause,[],[f3307]) ).
fof(f3312,plain,
( spl0_225
| ~ spl0_215 ),
inference(avatar_split_clause,[],[f2754,f2740,f3136]) ).
fof(f3318,plain,
( ~ spl0_172
| spl0_61
| ~ spl0_164 ),
inference(avatar_split_clause,[],[f2997,f1653,f635,f1811]) ).
fof(f3395,plain,
( $false
| spl0_3
| ~ spl0_229 ),
inference(unit_resulting_resolution,[],[f131,f91,f167,f3195]) ).
fof(f3399,plain,
( spl0_3
| ~ spl0_229 ),
inference(avatar_contradiction_clause,[],[f3395]) ).
fof(f3403,plain,
( point_equal(c2,b1)
| ~ spl0_230 ),
inference(resolution,[],[f3245,f126]) ).
fof(f3405,plain,
( spl0_229
| ~ spl0_230 ),
inference(avatar_split_clause,[],[f3403,f3244,f3194]) ).
fof(f3409,plain,
( $false
| ~ spl0_4
| spl0_12
| ~ spl0_204 ),
inference(unit_resulting_resolution,[],[f131,f92,f229,f2817]) ).
fof(f3414,plain,
( ~ spl0_4
| spl0_12
| ~ spl0_204 ),
inference(avatar_contradiction_clause,[],[f3409]) ).
fof(f3418,plain,
( $false
| ~ spl0_59
| ~ spl0_187 ),
inference(unit_resulting_resolution,[],[f131,f1043,f214,f3144]) ).
fof(f3423,plain,
( ~ spl0_59
| ~ spl0_187 ),
inference(avatar_contradiction_clause,[],[f3418]) ).
fof(f3514,plain,
( $false
| ~ spl0_31
| spl0_166 ),
inference(unit_resulting_resolution,[],[f132,f1686,f102,f411]) ).
fof(f3518,plain,
( ~ spl0_31
| spl0_166 ),
inference(avatar_contradiction_clause,[],[f3514]) ).
fof(f3522,plain,
( ~ spl0_92
| spl0_93
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f2939,f824,f898,f895]) ).
fof(f3548,plain,
( $false
| ~ spl0_31
| spl0_60 ),
inference(unit_resulting_resolution,[],[f132,f411,f106,f624]) ).
fof(f3549,plain,
( ~ spl0_31
| spl0_60 ),
inference(avatar_contradiction_clause,[],[f3548]) ).
fof(f3559,plain,
( $false
| ~ spl0_57
| ~ spl0_226 ),
inference(unit_resulting_resolution,[],[f127,f138,f614,f3141]) ).
fof(f3563,plain,
( ~ spl0_57
| ~ spl0_226 ),
inference(avatar_contradiction_clause,[],[f3559]) ).
fof(f3578,plain,
( $false
| ~ spl0_6
| spl0_86
| ~ spl0_87 ),
inference(unit_resulting_resolution,[],[f131,f162,f857,f860]) ).
fof(f3582,plain,
( ~ spl0_6
| spl0_86
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f3578]) ).
fof(f3590,plain,
( $false
| ~ spl0_130
| spl0_166 ),
inference(unit_resulting_resolution,[],[f132,f1266,f104,f1686]) ).
fof(f3591,plain,
( ~ spl0_130
| spl0_166 ),
inference(avatar_contradiction_clause,[],[f3590]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f149]) ).
cnf(s2,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f156]) ).
cnf(s3,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f163]) ).
cnf(s4,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(sat_conversion,[],[f170]) ).
cnf(s5,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_6 ),
inference(sat_conversion,[],[f174]) ).
cnf(s6,plain,
( ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f186]) ).
cnf(s7,plain,
( ~ spl0_9
| ~ spl0_10 ),
inference(sat_conversion,[],[f197]) ).
cnf(s10,plain,
( ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f248]) ).
cnf(s11,plain,
( ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f258]) ).
cnf(s13,plain,
( spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f336]) ).
cnf(s17,plain,
( spl0_18
| ~ spl0_21 ),
inference(sat_conversion,[],[f350]) ).
cnf(s21,plain,
( spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f400]) ).
cnf(s22,plain,
( spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f407]) ).
cnf(s30,plain,
( ~ spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f472]) ).
cnf(s31,plain,
( ~ spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f479]) ).
cnf(s34,plain,
( spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f502]) ).
cnf(s36,plain,
( spl0_24
| ~ spl0_45 ),
inference(sat_conversion,[],[f516]) ).
cnf(s38,plain,
( ~ spl0_24
| ~ spl0_35 ),
inference(sat_conversion,[],[f523]) ).
cnf(s40,plain,
( spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f536]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_33
| ~ spl0_49 ),
inference(sat_conversion,[],[f559]) ).
cnf(s48,plain,
( spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f597]) ).
cnf(s50,plain,
~ spl0_55,
inference(sat_conversion,[],[f604]) ).
cnf(s51,plain,
( spl0_57
| ~ spl0_58 ),
inference(sat_conversion,[],[f618]) ).
cnf(s52,plain,
( spl0_59
| ~ spl0_60 ),
inference(sat_conversion,[],[f625]) ).
cnf(s53,plain,
( spl0_61
| spl0_62 ),
inference(sat_conversion,[],[f640]) ).
cnf(s55,plain,
( spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f654]) ).
cnf(s58,plain,
~ spl0_65,
inference(sat_conversion,[],[f667]) ).
cnf(s59,plain,
( ~ spl0_3
| spl0_67
| ~ spl0_68 ),
inference(sat_conversion,[],[f697]) ).
cnf(s60,plain,
( ~ spl0_12
| spl0_69 ),
inference(sat_conversion,[],[f701]) ).
cnf(s61,plain,
( spl0_70
| spl0_71 ),
inference(sat_conversion,[],[f722]) ).
cnf(s69,plain,
( ~ spl0_5
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f798]) ).
cnf(s72,plain,
( ~ spl0_6
| spl0_80
| spl0_81 ),
inference(sat_conversion,[],[f822]) ).
cnf(s73,plain,
( ~ spl0_6
| spl0_78
| spl0_82 ),
inference(sat_conversion,[],[f826]) ).
cnf(s74,plain,
( ~ spl0_6
| spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f833]) ).
cnf(s77,plain,
( ~ spl0_2
| spl0_43
| ~ spl0_77 ),
inference(sat_conversion,[],[f851]) ).
cnf(s81,plain,
( ~ spl0_66
| spl0_90
| ~ spl0_91 ),
inference(sat_conversion,[],[f890]) ).
cnf(s85,plain,
( ~ spl0_3
| spl0_58
| ~ spl0_84 ),
inference(sat_conversion,[],[f919]) ).
cnf(s87,plain,
( spl0_60
| ~ spl0_76 ),
inference(sat_conversion,[],[f926]) ).
cnf(s88,plain,
( spl0_8
| ~ spl0_76 ),
inference(sat_conversion,[],[f940]) ).
cnf(s90,plain,
( ~ spl0_11
| spl0_96 ),
inference(sat_conversion,[],[f945]) ).
cnf(s91,plain,
( spl0_95
| ~ spl0_96 ),
inference(sat_conversion,[],[f949]) ).
cnf(s94,plain,
( ~ spl0_6
| spl0_94
| ~ spl0_95 ),
inference(sat_conversion,[],[f981]) ).
cnf(s99,plain,
( ~ spl0_6
| spl0_17
| ~ spl0_44 ),
inference(sat_conversion,[],[f995]) ).
cnf(s101,plain,
( spl0_9
| ~ spl0_83 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s105,plain,
( ~ spl0_2
| spl0_102
| spl0_103 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s110,plain,
~ spl0_106,
inference(sat_conversion,[],[f1095]) ).
cnf(s111,plain,
( spl0_108
| spl0_109 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s112,plain,
( spl0_110
| spl0_111 ),
inference(sat_conversion,[],[f1117]) ).
cnf(s113,plain,
( ~ spl0_2
| spl0_7
| ~ spl0_110 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s117,plain,
( spl0_8
| ~ spl0_59 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s119,plain,
( ~ spl0_1
| spl0_115
| spl0_116 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s131,plain,
( ~ spl0_1
| spl0_13
| ~ spl0_118 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s132,plain,
( spl0_130
| spl0_131 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s133,plain,
( spl0_132
| spl0_133 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s134,plain,
~ spl0_132,
inference(sat_conversion,[],[f1283]) ).
cnf(s141,plain,
( spl0_138
| spl0_139 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s144,plain,
~ spl0_138,
inference(sat_conversion,[],[f1335]) ).
cnf(s146,plain,
( spl0_121
| ~ spl0_136 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s148,plain,
( ~ spl0_1
| spl0_104
| spl0_140 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s152,plain,
( spl0_144
| spl0_145 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s153,plain,
( spl0_91
| ~ spl0_144 ),
inference(sat_conversion,[],[f1399]) ).
cnf(s154,plain,
( spl0_86
| ~ spl0_144 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s156,plain,
( spl0_146
| spl0_147 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s157,plain,
( spl0_43
| ~ spl0_146 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s158,plain,
( spl0_86
| ~ spl0_146 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s159,plain,
( spl0_44
| ~ spl0_146 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s163,plain,
( spl0_91
| ~ spl0_148 ),
inference(sat_conversion,[],[f1471]) ).
cnf(s164,plain,
( spl0_83
| ~ spl0_148 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s172,plain,
( spl0_43
| ~ spl0_78 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s174,plain,
( spl0_6
| ~ spl0_77
| ~ spl0_96 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s175,plain,
( ~ spl0_57
| spl0_92 ),
inference(sat_conversion,[],[f1559]) ).
cnf(s179,plain,
( ~ spl0_57
| spl0_130 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s186,plain,
( ~ spl0_56
| ~ spl0_161
| spl0_162 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s188,plain,
( ~ spl0_129
| spl0_161 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s191,plain,
( spl0_163
| spl0_164 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s193,plain,
( spl0_12
| ~ spl0_163 ),
inference(sat_conversion,[],[f1662]) ).
cnf(s196,plain,
( ~ spl0_129
| spl0_165 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s197,plain,
( ~ spl0_35
| spl0_165 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s205,plain,
( spl0_121
| ~ spl0_167 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s206,plain,
( ~ spl0_4
| spl0_54
| spl0_169 ),
inference(sat_conversion,[],[f1750]) ).
cnf(s207,plain,
~ spl0_169,
inference(sat_conversion,[],[f1755]) ).
cnf(s210,plain,
( ~ spl0_5
| spl0_170
| spl0_171 ),
inference(sat_conversion,[],[f1778]) ).
cnf(s211,plain,
~ spl0_170,
inference(sat_conversion,[],[f1783]) ).
cnf(s212,plain,
( spl0_61
| ~ spl0_166
| ~ spl0_171 ),
inference(sat_conversion,[],[f1787]) ).
cnf(s213,plain,
( ~ spl0_61
| spl0_86 ),
inference(sat_conversion,[],[f1792]) ).
cnf(s214,plain,
( spl0_45
| ~ spl0_86
| ~ spl0_147 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s219,plain,
~ spl0_108,
inference(sat_conversion,[],[f1824]) ).
cnf(s220,plain,
( ~ spl0_18
| ~ spl0_109
| spl0_129 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s222,plain,
( spl0_15
| ~ spl0_42 ),
inference(sat_conversion,[],[f1831]) ).
cnf(s226,plain,
( ~ spl0_167
| spl0_172 ),
inference(sat_conversion,[],[f1849]) ).
cnf(s241,plain,
( spl0_61
| ~ spl0_86
| ~ spl0_145 ),
inference(sat_conversion,[],[f1922]) ).
cnf(s242,plain,
( ~ spl0_5
| ~ spl0_61
| spl0_166 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s248,plain,
~ spl0_178,
inference(sat_conversion,[],[f1975]) ).
cnf(s251,plain,
~ spl0_126,
inference(sat_conversion,[],[f1983]) ).
cnf(s255,plain,
( ~ spl0_69
| spl0_126
| ~ spl0_140
| spl0_183 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s258,plain,
( spl0_2
| ~ spl0_104 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s259,plain,
( ~ spl0_61
| ~ spl0_122 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s263,plain,
( ~ spl0_87
| spl0_166 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s265,plain,
( ~ spl0_29
| ~ spl0_70 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s266,plain,
( spl0_11
| ~ spl0_70 ),
inference(sat_conversion,[],[f2117]) ).
cnf(s267,plain,
( spl0_15
| ~ spl0_167 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s269,plain,
( ~ spl0_22
| spl0_24
| ~ spl0_33 ),
inference(sat_conversion,[],[f2128]) ).
cnf(s270,plain,
( ~ spl0_42
| spl0_136 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s272,plain,
( ~ spl0_90
| spl0_144 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s274,plain,
( ~ spl0_1
| ~ spl0_69
| spl0_106
| ~ spl0_140
| spl0_187 ),
inference(sat_conversion,[],[f2177]) ).
cnf(s292,plain,
( ~ spl0_1
| ~ spl0_69
| ~ spl0_117
| ~ spl0_140 ),
inference(sat_conversion,[],[f2319]) ).
cnf(s294,plain,
( ~ spl0_1
| spl0_203
| spl0_204 ),
inference(sat_conversion,[],[f2330]) ).
cnf(s295,plain,
( ~ spl0_1
| spl0_117
| spl0_204 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s301,plain,
( ~ spl0_44
| spl0_146 ),
inference(sat_conversion,[],[f2344]) ).
cnf(s306,plain,
( ~ spl0_4
| spl0_118
| spl0_203 ),
inference(sat_conversion,[],[f2350]) ).
cnf(s307,plain,
( ~ spl0_43
| spl0_55
| ~ spl0_111 ),
inference(sat_conversion,[],[f2351]) ).
cnf(s311,plain,
( ~ spl0_83
| spl0_148 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s322,plain,
( spl0_29
| ~ spl0_183 ),
inference(sat_conversion,[],[f2386]) ).
cnf(s333,plain,
( ~ spl0_1
| spl0_114
| spl0_178 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s335,plain,
( ~ spl0_13
| ~ spl0_30 ),
inference(sat_conversion,[],[f2396]) ).
cnf(s338,plain,
( ~ spl0_114
| ~ spl0_165
| spl0_167 ),
inference(sat_conversion,[],[f2401]) ).
cnf(s339,plain,
( ~ spl0_15
| ~ spl0_116
| spl0_129 ),
inference(sat_conversion,[],[f2402]) ).
cnf(s343,plain,
( ~ spl0_3
| spl0_148
| spl0_210 ),
inference(sat_conversion,[],[f2436]) ).
cnf(s353,plain,
( spl0_10
| ~ spl0_93 ),
inference(sat_conversion,[],[f2495]) ).
cnf(s354,plain,
( spl0_60
| ~ spl0_115 ),
inference(sat_conversion,[],[f2503]) ).
cnf(s357,plain,
( ~ spl0_59
| ~ spl0_93 ),
inference(sat_conversion,[],[f2514]) ).
cnf(s361,plain,
( spl0_16
| ~ spl0_44 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s368,plain,
( spl0_21
| ~ spl0_33
| ~ spl0_46 ),
inference(sat_conversion,[],[f2524]) ).
cnf(s369,plain,
( spl0_58
| ~ spl0_130 ),
inference(sat_conversion,[],[f2526]) ).
cnf(s370,plain,
( ~ spl0_80
| spl0_150 ),
inference(sat_conversion,[],[f2527]) ).
cnf(s382,plain,
~ spl0_150,
inference(sat_conversion,[],[f2598]) ).
cnf(s386,plain,
( ~ spl0_32
| spl0_87
| ~ spl0_166 ),
inference(sat_conversion,[],[f2602]) ).
cnf(s387,plain,
( ~ spl0_32
| ~ spl0_60 ),
inference(sat_conversion,[],[f2603]) ).
cnf(s391,plain,
( ~ spl0_81
| ~ spl0_86
| spl0_87 ),
inference(sat_conversion,[],[f2604]) ).
cnf(s396,plain,
~ spl0_184,
inference(sat_conversion,[],[f2625]) ).
cnf(s398,plain,
( ~ spl0_61
| spl0_172 ),
inference(sat_conversion,[],[f2644]) ).
cnf(s399,plain,
( ~ spl0_71
| spl0_167
| ~ spl0_172 ),
inference(sat_conversion,[],[f2645]) ).
cnf(s402,plain,
( ~ spl0_45
| spl0_121 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s405,plain,
( ~ spl0_87
| spl0_168 ),
inference(sat_conversion,[],[f2674]) ).
cnf(s409,plain,
( ~ spl0_94
| ~ spl0_210
| spl0_214 ),
inference(sat_conversion,[],[f2721]) ).
cnf(s410,plain,
( spl0_67
| ~ spl0_214 ),
inference(sat_conversion,[],[f2725]) ).
cnf(s420,plain,
~ spl0_67,
inference(sat_conversion,[],[f2791]) ).
cnf(s433,plain,
( ~ spl0_117
| spl0_216 ),
inference(sat_conversion,[],[f2822]) ).
cnf(s434,plain,
( ~ spl0_110
| ~ spl0_162 ),
inference(sat_conversion,[],[f2830]) ).
cnf(s447,plain,
( spl0_5
| ~ spl0_78 ),
inference(sat_conversion,[],[f2841]) ).
cnf(s449,plain,
( ~ spl0_54
| ~ spl0_121
| spl0_122 ),
inference(sat_conversion,[],[f2843]) ).
cnf(s450,plain,
( ~ spl0_16
| ~ spl0_62
| spl0_221 ),
inference(sat_conversion,[],[f2844]) ).
cnf(s459,plain,
( ~ spl0_84
| ~ spl0_91
| spl0_184 ),
inference(sat_conversion,[],[f2853]) ).
cnf(s463,plain,
( spl0_21
| ~ spl0_221 ),
inference(sat_conversion,[],[f2869]) ).
cnf(s466,plain,
( spl0_41
| ~ spl0_203 ),
inference(sat_conversion,[],[f2886]) ).
cnf(s473,plain,
( spl0_3
| ~ spl0_57
| ~ spl0_82 ),
inference(sat_conversion,[],[f2913]) ).
cnf(s474,plain,
( spl0_35
| ~ spl0_131
| ~ spl0_166 ),
inference(sat_conversion,[],[f2914]) ).
cnf(s491,plain,
( ~ spl0_50
| spl0_122
| ~ spl0_168 ),
inference(sat_conversion,[],[f3095]) ).
cnf(s500,plain,
( spl0_65
| ~ spl0_69
| ~ spl0_164 ),
inference(sat_conversion,[],[f3100]) ).
cnf(s502,plain,
( ~ spl0_163
| spl0_172 ),
inference(sat_conversion,[],[f3131]) ).
cnf(s509,plain,
( spl0_35
| ~ spl0_103
| ~ spl0_172 ),
inference(sat_conversion,[],[f3133]) ).
cnf(s517,plain,
( ~ spl0_133
| ~ spl0_216
| spl0_226 ),
inference(sat_conversion,[],[f3142]) ).
cnf(s518,plain,
( spl0_68
| ~ spl0_102 ),
inference(sat_conversion,[],[f3159]) ).
cnf(s545,plain,
( ~ spl0_161
| ~ spl0_204
| spl0_215 ),
inference(sat_conversion,[],[f3234]) ).
cnf(s547,plain,
( ~ spl0_4
| ~ spl0_91
| ~ spl0_139
| spl0_230 ),
inference(sat_conversion,[],[f3246]) ).
cnf(s553,plain,
~ spl0_225,
inference(sat_conversion,[],[f3311]) ).
cnf(s554,plain,
( ~ spl0_215
| spl0_225 ),
inference(sat_conversion,[],[f3312]) ).
cnf(s563,plain,
( spl0_61
| ~ spl0_164
| ~ spl0_172 ),
inference(sat_conversion,[],[f3318]) ).
cnf(s572,plain,
( spl0_3
| ~ spl0_229 ),
inference(sat_conversion,[],[f3399]) ).
cnf(s574,plain,
( spl0_229
| ~ spl0_230 ),
inference(sat_conversion,[],[f3405]) ).
cnf(s575,plain,
( ~ spl0_4
| spl0_12
| ~ spl0_204 ),
inference(sat_conversion,[],[f3414]) ).
cnf(s578,plain,
( ~ spl0_59
| ~ spl0_187 ),
inference(sat_conversion,[],[f3423]) ).
cnf(s586,plain,
( ~ spl0_31
| spl0_166 ),
inference(sat_conversion,[],[f3518]) ).
cnf(s600,plain,
( ~ spl0_82
| ~ spl0_92
| spl0_93 ),
inference(sat_conversion,[],[f3522]) ).
cnf(s605,plain,
( ~ spl0_31
| spl0_60 ),
inference(sat_conversion,[],[f3549]) ).
cnf(s606,plain,
( ~ spl0_57
| ~ spl0_226 ),
inference(sat_conversion,[],[f3563]) ).
cnf(s607,plain,
( ~ spl0_6
| spl0_86
| ~ spl0_87 ),
inference(sat_conversion,[],[f3582]) ).
cnf(s608,plain,
( ~ spl0_130
| spl0_166 ),
inference(sat_conversion,[],[f3591]) ).
cnf(s609,plain,
~ spl0_215,
inference(rat,[],[s554,s553]) ).
cnf(s610,plain,
( ~ spl0_161
| ~ spl0_204 ),
inference(rat,[],[s545,s609]) ).
cnf(s621,plain,
~ spl0_214,
inference(rat,[],[s410,s420]) ).
cnf(s622,plain,
( ~ spl0_94
| ~ spl0_210 ),
inference(rat,[],[s409,s621]) ).
cnf(s626,plain,
~ spl0_80,
inference(rat,[],[s370,s382]) ).
cnf(s637,plain,
( ~ spl0_5
| spl0_171 ),
inference(rat,[],[s210,s211]) ).
cnf(s639,plain,
( ~ spl0_4
| spl0_54 ),
inference(rat,[],[s206,s207]) ).
cnf(s642,plain,
spl0_139,
inference(rat,[],[s141,s144]) ).
cnf(s644,plain,
spl0_133,
inference(rat,[],[s133,s134]) ).
cnf(s647,plain,
spl0_109,
inference(rat,[],[s111,s219]) ).
cnf(s651,plain,
( ~ spl0_6
| spl0_81 ),
inference(rat,[],[s72,s626]) ).
cnf(s653,plain,
( ~ spl0_3
| ~ spl0_68 ),
inference(rat,[],[s59,s420]) ).
cnf(s654,plain,
spl0_66,
inference(rat,[],[s55,s58]) ).
cnf(s655,plain,
spl0_56,
inference(rat,[],[s48,s50]) ).
cnf(s657,plain,
( spl0_43
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s402,s214,s449,s213,s259,s212,s586,s22,s387,s87,s69,s156,s77,s157,s639,s637,s3,s5]) ).
cnf(s658,plain,
( spl0_3
| ~ spl0_2 ),
inference(rat,[],[s266,s90,s61,s174,s399,s69,s398,s88,s241,s267,s6,s158,s10,s113,s301,s361,s112,s31,s307,s657,s152,s3,s153,s5,s547,s574,s2,s572,s50,s642]) ).
cnf(s660,plain,
( spl0_43
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s36,s38,s214,s509,s213,s398,s212,s586,s22,s387,s87,s69,s156,s77,s157,s105,s518,s653,s658,s637]) ).
cnf(s661,plain,
( ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s40,s44,s491,s269,s405,s38,s386,s509,s242,s259,s398,s53,s450,s22,s13,s463,s605,s17,s52,s220,s117,s188,s6,s186,s113,s434,s361,s112,s31,s307,s660,s105,s518,s653,s658,s647,s655,s50]) ).
cnf(s662,plain,
( ~ spl0_61
| ~ spl0_147
| ~ spl0_103 ),
inference(rat,[],[s36,s38,s214,s509,s213,s398]) ).
cnf(s664,plain,
( ~ spl0_86
| spl0_61
| ~ spl0_147
| spl0_5 ),
inference(rat,[],[s600,s353,s175,s7,s51,s101,s369,s74,s132,s459,s474,s153,s38,s152,s36,s263,s241,s214,s391,s73,s447,s651,s3,s396]) ).
cnf(s665,plain,
( spl0_86
| ~ spl0_2 ),
inference(rat,[],[s605,s52,s22,s357,s386,s600,s608,s175,s179,s51,s85,s74,s311,s163,s81,s272,s607,s154,s658,s73,s3,s447,s661,s654]) ).
cnf(s666,plain,
( spl0_61
| ~ spl0_2 ),
inference(rat,[],[s17,s463,s11,s450,s99,s361,s159,s156,s664,s53,s3,s661,s665]) ).
cnf(s667,plain,
~ spl0_2,
inference(rat,[],[s17,s11,s368,s34,s99,s44,s36,s159,s40,s38,s156,s491,s509,s662,s259,s398,s666,s405,s391,s665,s651,s3,s661,s105,s518,s653,s658]) ).
cnf(s669,plain,
~ spl0_104,
inference(rat,[],[s258,s667]) ).
cnf(s670,plain,
spl0_1,
inference(rat,[],[s1,s667]) ).
cnf(s672,plain,
spl0_114,
inference(rat,[],[s333,s248,s670]) ).
cnf(s673,plain,
spl0_140,
inference(rat,[],[s148,s669,s670]) ).
cnf(s674,plain,
( spl0_5
| ~ spl0_86
| spl0_61 ),
inference(rat,[],[s17,s463,s11,s450,s99,s361,s159,s156,s664,s3,s53]) ).
cnf(s675,plain,
( ~ spl0_86
| spl0_61 ),
inference(rat,[],[s547,s574,s2,s572,s4,s674,s153,s152,s241,s670,s642]) ).
cnf(s676,plain,
( ~ spl0_166
| ~ spl0_6
| spl0_61 ),
inference(rat,[],[s197,s338,s474,s226,s132,s563,s369,s191,s51,s193,s175,s60,s600,s274,s357,s578,s52,s605,s22,s386,s73,s172,s31,s301,s158,s607,s675,s672,s110,s670,s673]) ).
cnf(s677,plain,
( spl0_172
| ~ spl0_116
| ~ spl0_4 ),
inference(rat,[],[s466,s30,s294,s222,s575,s339,s60,s196,s500,s338,s191,s226,s502,s670,s58,s672]) ).
cnf(s678,plain,
( ~ spl0_6
| spl0_61 ),
inference(rat,[],[s267,s399,s339,s61,s188,s265,s610,s322,s295,s255,s292,s60,s193,s191,s563,s677,s119,s2,s354,s85,s387,s51,s22,s179,s586,s608,s676,s74,s311,s163,s81,s272,s154,s675,s670,s251,s673,s654]) ).
cnf(s679,plain,
spl0_61,
inference(rat,[],[s188,s610,s339,s295,s267,s292,s399,s60,s61,s193,s266,s191,s90,s563,s174,s677,s69,s119,s87,s354,s387,s22,s586,s2,s212,s4,s637,s3,s678,s670,s673]) ).
cnf(s680,plain,
spl0_172,
inference(rat,[],[s398,s679]) ).
cnf(s681,plain,
~ spl0_122,
inference(rat,[],[s259,s679]) ).
cnf(s682,plain,
spl0_86,
inference(rat,[],[s213,s679]) ).
cnf(s683,plain,
~ spl0_35,
inference(rat,[],[s159,s361,s156,s10,s214,s267,s36,s338,s38,s197,s682,s672]) ).
cnf(s687,plain,
( ~ spl0_6
| spl0_78 ),
inference(rat,[],[s90,s266,s91,s61,s94,s399,s622,s267,s343,s339,s164,s119,s188,s101,s354,s610,s7,s52,s295,s353,s357,s433,s600,s517,s175,s473,s606,s51,s369,s132,s474,s263,s391,s651,s73,s682,s683,s644,s670,s680]) ).
cnf(s688,plain,
spl0_5,
inference(rat,[],[s687,s3,s447]) ).
cnf(s690,plain,
~ spl0_3,
inference(rat,[],[s4,s670,s688]) ).
cnf(s695,plain,
spl0_4,
inference(rat,[],[s2,s690]) ).
cnf(s700,plain,
spl0_54,
inference(rat,[],[s639,s695]) ).
cnf(s704,plain,
~ spl0_121,
inference(rat,[],[s449,s681,s700]) ).
cnf(s709,plain,
~ spl0_167,
inference(rat,[],[s205,s704]) ).
cnf(s710,plain,
~ spl0_136,
inference(rat,[],[s146,s704]) ).
cnf(s718,plain,
~ spl0_71,
inference(rat,[],[s399,s680,s709]) ).
cnf(s720,plain,
~ spl0_42,
inference(rat,[],[s270,s710]) ).
cnf(s731,plain,
spl0_70,
inference(rat,[],[s61,s718]) ).
cnf(s733,plain,
~ spl0_41,
inference(rat,[],[s30,s720]) ).
cnf(s740,plain,
~ spl0_29,
inference(rat,[],[s265,s731]) ).
cnf(s742,plain,
~ spl0_203,
inference(rat,[],[s466,s733]) ).
cnf(s750,plain,
spl0_30,
inference(rat,[],[s21,s740]) ).
cnf(s752,plain,
spl0_118,
inference(rat,[],[s306,s695,s742]) ).
cnf(s763,plain,
~ spl0_13,
inference(rat,[],[s335,s750]) ).
cnf(s769,plain,
$false,
inference(rat,[],[s131,s670,s752,s763]) ).
fof(f3592,plain,
$false,
inference(avatar_sat_refutation,[],[s769]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 07:21:31 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.41 Running first-order theorem proving
% 0.14/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.93/2.24 % (608054)Detected formulas, will run a generic FOF schedule.
% 9.93/2.24 % (608061)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=986289243:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.93/2.24 % (608064)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3579055716:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.93/2.24 % (608063)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=627227919:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.93/2.24 % (608065)dis-21_1_sil=8000:lcm=predicate:random_seed=1565578421:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.93/2.24 % (608062)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3708273236:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.93/2.24 % (608059)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=391272848:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.93/2.24 % (608060)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3672414436:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.93/2.24 % (608063)Refutation not found, incomplete strategy
% 9.93/2.24 % (608063)------------------------------
% 9.93/2.24 % (608063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608063)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608062)Refutation not found, incomplete strategy
% 9.93/2.24 % (608062)------------------------------
% 9.93/2.24 % (608062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608063)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608063)Time elapsed: 0.001 s
% 9.93/2.24 % (608063)Peak memory usage: 86 MB
% 9.93/2.24 % (608062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608062)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608062)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608062)Time elapsed: 0.001 s
% 9.93/2.24 % (608062)Peak memory usage: 86 MB
% 9.93/2.24 % (608065)Instruction limit reached!
% 9.93/2.24 % (608065)------------------------------
% 9.93/2.24 % (608065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608065)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608065)Termination reason: Instruction limit
% 9.93/2.24 % (608065)Termination phase: Saturation
% 9.93/2.24 % (608065)Time elapsed: 0.079 s
% 9.93/2.24 % (608065)Peak memory usage: 89 MB
% 9.93/2.24 % (608065)Instructions burned: 129 (million)
% 9.93/2.24 % (608064)Instruction limit reached!
% 9.93/2.24 % (608064)------------------------------
% 9.93/2.24 % (608064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608064)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608064)Termination reason: Instruction limit
% 9.93/2.24 % (608064)Termination phase: Saturation
% 9.93/2.24 % (608064)Time elapsed: 0.081 s
% 9.93/2.24 % (608064)Peak memory usage: 88 MB
% 9.93/2.24 % (608064)Instructions burned: 140 (million)
% 9.93/2.24 % (608073)lrs+10_1_sil=8000:sp=occurrence:random_seed=3083577469:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.93/2.24 % (608074)lrs+10_1_sil=32000:urr=on:br=off:random_seed=616422757:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.93/2.24 % (608062)------------------------------
% 9.93/2.24 % (608062)------------------------------
% 9.93/2.24 % (608063)------------------------------
% 9.93/2.24 % (608063)------------------------------
% 9.93/2.24 % (608073)Refutation not found, incomplete strategy
% 9.93/2.24 % (608073)------------------------------
% 9.93/2.24 % (608073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608073)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608073)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608073)Time elapsed: 0.001 s
% 9.93/2.24 % (608073)Peak memory usage: 87 MB
% 9.93/2.24 % (608074)Refutation not found, incomplete strategy
% 9.93/2.24 % (608074)------------------------------
% 9.93/2.24 % (608074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608074)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608074)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608074)Time elapsed: 0.001 s
% 9.93/2.24 % (608074)Peak memory usage: 87 MB
% 9.93/2.24 % (608077)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1451782160:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 9.93/2.24 % (608078)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2527600727:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.93/2.24 % (608077)Refutation not found, incomplete strategy
% 9.93/2.24 % (608077)------------------------------
% 9.93/2.24 % (608077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608077)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608077)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608077)Time elapsed: 0.001 s
% 9.93/2.24 % (608077)Peak memory usage: 87 MB
% 9.93/2.24 % (608078)Refutation not found, incomplete strategy
% 9.93/2.24 % (608078)------------------------------
% 9.93/2.24 % (608078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608078)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608078)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608078)Time elapsed: 0.024 s
% 9.93/2.24 % (608078)Peak memory usage: 89 MB
% 9.93/2.24 % (608078)Instructions burned: 48 (million)
% 9.93/2.24 % (608074)------------------------------
% 9.93/2.24 % (608074)------------------------------
% 9.93/2.24 % (608073)------------------------------
% 9.93/2.24 % (608073)------------------------------
% 9.93/2.24 % (608077)------------------------------
% 9.93/2.24 % (608077)------------------------------
% 9.93/2.24 % (608082)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=585827598:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 9.93/2.24 % (608081)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=342325763:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 9.93/2.24 % (608081)Refutation not found, incomplete strategy
% 9.93/2.24 % (608081)------------------------------
% 9.93/2.24 % (608081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608081)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608081)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608081)Time elapsed: 0.001 s
% 9.93/2.24 % (608081)Peak memory usage: 87 MB
% 9.93/2.24 % (608081)Instructions burned: 1 (million)
% 9.93/2.24 % (608078)------------------------------
% 9.93/2.24 % (608078)------------------------------
% 9.93/2.24 % (608085)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2796481946:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 9.93/2.24 % (608086)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1940408981:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 9.93/2.24 % (608081)------------------------------
% 9.93/2.24 % (608081)------------------------------
% 9.93/2.24 % (608085)Instruction limit reached!
% 9.93/2.24 % (608085)------------------------------
% 9.93/2.24 % (608085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608085)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608085)Termination reason: Instruction limit
% 9.93/2.24 % (608085)Termination phase: Saturation
% 9.93/2.24 % (608085)Time elapsed: 0.068 s
% 9.93/2.24 % (608085)Peak memory usage: 89 MB
% 9.93/2.24 % (608085)Instructions burned: 113 (million)
% 9.93/2.24 % (608086)Instruction limit reached!
% 9.93/2.24 % (608086)------------------------------
% 9.93/2.24 % (608086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608086)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608086)Termination reason: Instruction limit
% 9.93/2.24 % (608086)Termination phase: Saturation
% 9.93/2.24 % (608086)Time elapsed: 0.067 s
% 9.93/2.24 % (608086)Peak memory usage: 89 MB
% 9.93/2.24 % (608086)Instructions burned: 128 (million)
% 9.93/2.24 % (608060)First to succeed.
% 9.93/2.24 % (608060)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-608054"
% 9.93/2.24 % (608059)Also succeeded, but the first one will report.
% 9.93/2.24 % (608090)lrs+10_1_sil=8000:sp=occurrence:random_seed=2842102762:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 9.93/2.24 % (608089)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3783066616:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 9.93/2.24 % (608089)Refutation not found, incomplete strategy
% 9.93/2.24 % (608089)------------------------------
% 9.93/2.24 % (608089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608089)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608089)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608089)Time elapsed: 0.001 s
% 9.93/2.24 % (608089)Peak memory usage: 87 MB
% 9.93/2.24 % (608091)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=129575994:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 9.93/2.24 % (608091)Refutation not found, incomplete strategy
% 9.93/2.24 % (608091)------------------------------
% 9.93/2.24 % (608091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.24 % (608091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.24 % (608091)CaDiCaL version: 2.1.3
% 9.93/2.24 % (608091)Termination reason: Refutation not found, incomplete strategy
% 9.93/2.24 % (608091)Time elapsed: 0.001 s
% 9.93/2.24 % (608091)Peak memory usage: 87 MB
% 9.93/2.24 % (608091)Instructions burned: 1 (million)
% 9.93/2.24 % (608090)Also succeeded, but the first one will report.
% 9.93/2.24 % (608060)Refutation found. Thanks to Tanya!
% 9.93/2.24 % SZS status Theorem for theBenchmark
% 9.93/2.24 % SZS output start Proof for theBenchmark
% See solution above
% 10.37/2.44 % (608060)------------------------------
% 10.37/2.44 % (608060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.37/2.44 % (608060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/2.44 % (608060)CaDiCaL version: 2.1.3
% 10.37/2.44 % (608060)Termination reason: Refutation
% 10.37/2.44 % (608060)Time elapsed: 0.937 s
% 10.37/2.44 % (608060)Peak memory usage: 131 MB
% 10.37/2.44 % (608060)Instructions burned: 1336 (million)
% 10.37/2.44 % (608060)------------------------------
% 10.37/2.44 % (608060)------------------------------
% 10.37/2.44 % (608054)Success in time 1.385 s
% 10.37/2.44 % Vampire exiting
%------------------------------------------------------------------------------