%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n018.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:53:45 AM UTC 2026
% Result : Theorem 1.50s 0.77s
% Output : Refutation 1.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 138
% Syntax : Number of formulae : 1137 ( 112 unt; 89 def)
% Number of atoms : 3017 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 3498 (1618 ~;1756 |; 17 &)
% ( 89 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 94 ( 93 usr; 91 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 273 ( 0 sgn 273 !; 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(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(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(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] :
( ~ incident(X0,X1)
| incident(X0,X2)
| ~ line_equal(X1,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(global_subsumption,[],[f124,f134]) ).
fof(f136,plain,
~ line_equal(a1c1,a2c2),
inference(global_subsumption,[],[f123,f134]) ).
fof(f137,plain,
~ line_equal(b1c1,b2c2),
inference(global_subsumption,[],[f122,f134]) ).
fof(f138,plain,
~ point_equal(c2,c1),
inference(global_subsumption,[],[f121,f134]) ).
fof(f139,plain,
~ point_equal(b2,b1),
inference(global_subsumption,[],[f120,f134]) ).
fof(f140,plain,
~ point_equal(a2,a1),
inference(global_subsumption,[],[f119,f134]) ).
fof(f141,plain,
! [X0] :
( ~ incident(c2,X0)
| ~ incident(b2,X0)
| ~ incident(a2,X0) ),
inference(global_subsumption,[],[f118,f134]) ).
fof(f142,plain,
! [X0] :
( ~ incident(c1,X0)
| ~ incident(b1,X0)
| ~ incident(a1,X0) ),
inference(global_subsumption,[],[f117,f134]) ).
fof(f143,plain,
( ~ incident(a2,b1c1)
| ~ incident(b2,a1c1)
| ~ incident(c2,a1b1) ),
inference(global_subsumption,[],[f86,f134]) ).
fof(f144,plain,
( ~ incident(a1,b2c2)
| ~ incident(b1,a2c2)
| ~ incident(c1,a2b2) ),
inference(global_subsumption,[],[f85,f134]) ).
fof(f145,plain,
! [X0] :
( ~ incident(ab,X0)
| ~ incident(bc,X0)
| ~ incident(ac,X0)
| ~ line_equal(X0,X0) ),
inference(global_subsumption,[],[f84,f134]) ).
fof(f187,definition,
( spl0_11
<=> incident(c1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f188,plain,
( incident(c1,a2b2)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f189,plain,
( ~ incident(c1,a2b2)
| spl0_11 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f191,definition,
( spl0_12
<=> incident(b1,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f192,plain,
( incident(b1,a2c2)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( ~ incident(b1,a2c2)
| spl0_12 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f195,definition,
( spl0_13
<=> incident(a1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f196,plain,
( incident(a1,b2c2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f144,f195,f191,f187]) ).
fof(f199,plain,
( ~ incident(b1,a1c1)
| ~ incident(a1,a1c1) ),
inference(resolution,[],[f95,f142]) ).
fof(f200,plain,
~ incident(b1,a1c1),
inference(forward_subsumption_resolution,[],[f199,f94]) ).
fof(f204,definition,
( spl0_14
<=> incident(c2,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f205,plain,
( incident(c2,a1b1)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f206,plain,
( ~ incident(c2,a1b1)
| spl0_14 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f208,definition,
( spl0_15
<=> incident(b2,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f209,plain,
( incident(b2,a1c1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( ~ incident(b2,a1c1)
| spl0_15 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f212,definition,
( spl0_16
<=> incident(a2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f213,plain,
( incident(a2,b1c1)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f214,plain,
( ~ incident(a2,b1c1)
| spl0_16 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f143,f212,f208,f204]) ).
fof(f216,plain,
( ~ incident(b2,a2c2)
| ~ incident(a2,a2c2) ),
inference(resolution,[],[f97,f141]) ).
fof(f217,plain,
~ incident(b2,a2c2),
inference(forward_subsumption_resolution,[],[f216,f96]) ).
fof(f218,plain,
( ~ incident(b1,b1c1)
| ~ incident(a1,b1c1) ),
inference(resolution,[],[f98,f142]) ).
fof(f219,plain,
~ incident(a1,b1c1),
inference(global_subsumption,[],[f218,f99]) ).
fof(f220,plain,
( ~ incident(b2,b2c2)
| ~ incident(a2,b2c2) ),
inference(resolution,[],[f100,f141]) ).
fof(f221,plain,
~ incident(a2,b2c2),
inference(global_subsumption,[],[f220,f101]) ).
fof(f224,definition,
( spl0_17
<=> incident(a1,oc) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f225,plain,
( incident(a1,oc)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( ~ incident(a1,oc)
| spl0_17 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f228,definition,
( spl0_18
<=> incident(b1,oc) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f229,plain,
( incident(b1,oc)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f230,plain,
( ~ incident(b1,oc)
| spl0_18 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f234,definition,
( spl0_19
<=> incident(a2,oc) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f235,plain,
( incident(a2,oc)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f236,plain,
( ~ incident(a2,oc)
| spl0_19 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f249,plain,
( ~ incident(bc,a2b2)
| ~ incident(ac,a2b2)
| ~ line_equal(a2b2,a2b2) ),
inference(resolution,[],[f116,f145]) ).
fof(f250,plain,
( spl0_15
| spl0_13 ),
inference(avatar_split_clause,[],[f87,f195,f208]) ).
fof(f251,plain,
( incident(b1,a2c2)
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f88,f206]) ).
fof(f252,plain,
( spl0_12
| spl0_14 ),
inference(avatar_split_clause,[],[f251,f204,f191]) ).
fof(f255,definition,
( spl0_21
<=> incident(a2,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f256,plain,
( incident(a2,a1b1)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f257,plain,
( ~ incident(a2,a1b1)
| spl0_21 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f263,plain,
( incident(a2,b1c1)
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f89,f189]) ).
fof(f264,plain,
( $false
| spl0_11
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f263,f214]) ).
fof(f265,plain,
( spl0_11
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f264]) ).
fof(f449,definition,
( spl0_28
<=> incident(ac,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f450,plain,
( incident(ac,a1b1)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f451,plain,
( ~ incident(ac,a1b1)
| spl0_28 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f458,definition,
( spl0_30
<=> line_equal(a2b2,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f460,plain,
( ~ line_equal(a2b2,a2b2)
| spl0_30 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f462,definition,
( spl0_31
<=> incident(ac,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f464,plain,
( ~ incident(ac,a2b2)
| spl0_31 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f466,definition,
( spl0_32
<=> incident(bc,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f467,plain,
( incident(bc,a2b2)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f468,plain,
( ~ incident(bc,a2b2)
| spl0_32 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f469,plain,
( ~ spl0_30
| ~ spl0_31
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f249,f466,f462,f458]) ).
fof(f486,plain,
line_equal(a2b2,a2b2),
inference(resolution,[],[f128,f92]) ).
fof(f521,plain,
( $false
| spl0_30 ),
inference(forward_subsumption_resolution,[],[f486,f460]) ).
fof(f522,plain,
spl0_30,
inference(avatar_contradiction_clause,[],[f521]) ).
fof(f683,plain,
! [X0] :
( ~ line_equal(b2c2,X0)
| incident(b2,X0) ),
inference(resolution,[],[f132,f101]) ).
fof(f684,plain,
! [X0] :
( ~ line_equal(b2c2,X0)
| incident(c2,X0) ),
inference(resolution,[],[f132,f100]) ).
fof(f685,plain,
! [X0] :
( ~ line_equal(a2c2,X0)
| incident(a2,X0) ),
inference(resolution,[],[f132,f96]) ).
fof(f686,plain,
! [X0] :
( ~ line_equal(a2c2,X0)
| incident(c2,X0) ),
inference(resolution,[],[f132,f97]) ).
fof(f688,plain,
! [X0] :
( ~ line_equal(a2b2,X0)
| incident(a2,X0) ),
inference(resolution,[],[f132,f92]) ).
fof(f689,plain,
! [X0] :
( ~ line_equal(a2b2,X0)
| incident(b2,X0) ),
inference(resolution,[],[f132,f93]) ).
fof(f692,plain,
! [X0] :
( ~ line_equal(b1c1,X0)
| incident(b1,X0) ),
inference(resolution,[],[f132,f99]) ).
fof(f693,plain,
! [X0] :
( ~ line_equal(b1c1,X0)
| incident(c1,X0) ),
inference(resolution,[],[f132,f98]) ).
fof(f695,plain,
! [X0] :
( ~ line_equal(a1c1,X0)
| incident(a1,X0) ),
inference(resolution,[],[f132,f94]) ).
fof(f697,plain,
! [X0] :
( ~ line_equal(a1c1,X0)
| incident(ac,X0) ),
inference(resolution,[],[f132,f113]) ).
fof(f698,plain,
! [X0] :
( ~ line_equal(a1b1,X0)
| incident(ab,X0) ),
inference(resolution,[],[f132,f115]) ).
fof(f700,plain,
! [X0] :
( ~ line_equal(a1b1,X0)
| incident(b1,X0) ),
inference(resolution,[],[f132,f91]) ).
fof(f702,plain,
! [X0] :
( ~ line_equal(oa,X0)
| incident(o,X0) ),
inference(resolution,[],[f132,f102]) ).
fof(f703,plain,
! [X0] :
( ~ line_equal(oa,X0)
| incident(a1,X0) ),
inference(resolution,[],[f132,f105]) ).
fof(f704,plain,
! [X0] :
( ~ line_equal(oa,X0)
| incident(a2,X0) ),
inference(resolution,[],[f132,f106]) ).
fof(f705,plain,
! [X0] :
( ~ line_equal(ob,X0)
| incident(o,X0) ),
inference(resolution,[],[f132,f103]) ).
fof(f706,plain,
! [X0] :
( ~ line_equal(ob,X0)
| incident(b1,X0) ),
inference(resolution,[],[f132,f107]) ).
fof(f707,plain,
! [X0] :
( ~ line_equal(ob,X0)
| incident(b2,X0) ),
inference(resolution,[],[f132,f108]) ).
fof(f708,plain,
! [X0] :
( ~ line_equal(oc,X0)
| incident(o,X0) ),
inference(resolution,[],[f132,f104]) ).
fof(f709,plain,
! [X0] :
( ~ line_equal(oc,X0)
| incident(c1,X0) ),
inference(resolution,[],[f132,f109]) ).
fof(f710,plain,
! [X0] :
( ~ line_equal(oc,X0)
| incident(c2,X0) ),
inference(resolution,[],[f132,f110]) ).
fof(f769,definition,
( spl0_43
<=> incident(a1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f770,plain,
( incident(a1,a2b2)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f771,plain,
( ~ incident(a1,a2b2)
| spl0_43 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f773,definition,
( spl0_44
<=> incident(b1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f774,plain,
( incident(b1,a2b2)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f775,plain,
( ~ incident(b1,a2b2)
| spl0_44 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f895,plain,
( ! [X0] :
( ~ line_equal(a1b1,X0)
| incident(ac,X0) )
| ~ spl0_28 ),
inference(resolution,[],[f450,f132]) ).
fof(f982,plain,
! [X0,X1] :
( ~ incident(bc,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2c2)
| line_equal(X0,b2c2)
| point_equal(X1,bc) ),
inference(resolution,[],[f133,f112]) ).
fof(f983,plain,
( ! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2c2)
| line_equal(X0,b2c2)
| point_equal(X1,a1) )
| ~ spl0_13 ),
inference(resolution,[],[f133,f196]) ).
fof(f984,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(f985,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(f986,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(f987,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(f988,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(f990,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(f991,plain,
( ! [X0,X1] :
( ~ incident(c1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2b2)
| line_equal(X0,a2b2)
| point_equal(X1,c1) )
| ~ spl0_11 ),
inference(resolution,[],[f133,f188]) ).
fof(f992,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(f993,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(f994,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(f1031,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,b2c2)
| line_equal(a1c1,b2c2)
| point_equal(X0,a1) )
| ~ spl0_13 ),
inference(resolution,[],[f983,f94]) ).
fof(f1032,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,b2c2)
| line_equal(a1b1,b2c2)
| point_equal(X0,a1) )
| ~ spl0_13 ),
inference(resolution,[],[f983,f90]) ).
fof(f1092,definition,
( spl0_61
<=> line_equal(a1c1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f1094,plain,
( line_equal(a1c1,b2c2)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f1092]) ).
fof(f1099,definition,
( spl0_63
<=> ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f1100,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1101,plain,
( spl0_61
| spl0_63
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1031,f195,f1099,f1092]) ).
fof(f1116,plain,
( line_equal(b2c2,a1c1)
| ~ spl0_61 ),
inference(resolution,[],[f1094,f129]) ).
fof(f1131,plain,
( incident(b2,a1c1)
| ~ spl0_61 ),
inference(resolution,[],[f1116,f683]) ).
fof(f1136,plain,
( $false
| spl0_15
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f1131,f210]) ).
fof(f1137,plain,
( spl0_15
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f1136]) ).
fof(f1275,definition,
( spl0_70
<=> line_equal(a1b1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f1277,plain,
( line_equal(a1b1,b2c2)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1282,definition,
( spl0_72
<=> ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f1283,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1284,plain,
( spl0_70
| spl0_72
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1032,f195,f1282,f1275]) ).
fof(f1367,plain,
( ! [X0] :
( ~ line_equal(oc,X0)
| incident(a1,X0) )
| ~ spl0_17 ),
inference(resolution,[],[f225,f132]) ).
fof(f1379,plain,
( incident(ab,b2c2)
| ~ spl0_70 ),
inference(resolution,[],[f1277,f698]) ).
fof(f1382,plain,
( incident(ac,b2c2)
| ~ spl0_28
| ~ spl0_70 ),
inference(resolution,[],[f1277,f895]) ).
fof(f1394,plain,
( ~ incident(bc,b2c2)
| ~ incident(ac,b2c2)
| ~ line_equal(b2c2,b2c2)
| ~ spl0_70 ),
inference(resolution,[],[f1379,f145]) ).
fof(f1399,plain,
( ~ incident(bc,b2c2)
| ~ incident(ac,b2c2)
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f1394,f128]) ).
fof(f1400,plain,
( ~ incident(ac,b2c2)
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f1399,f112]) ).
fof(f1407,plain,
( $false
| ~ spl0_28
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f1382,f1400]) ).
fof(f1408,plain,
( ~ spl0_28
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f1407]) ).
fof(f1563,plain,
( point_equal(c1,a1)
| ~ incident(c1,b2c2)
| ~ spl0_63 ),
inference(resolution,[],[f1100,f95]) ).
fof(f1599,definition,
( spl0_75
<=> incident(ac,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f1600,plain,
( incident(ac,b2c2)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f1599]) ).
fof(f1601,plain,
( ~ incident(ac,b2c2)
| spl0_75 ),
inference(avatar_component_clause,[],[f1599]) ).
fof(f1603,definition,
( spl0_76
<=> point_equal(ac,a1) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f1604,plain,
( ~ point_equal(ac,a1)
| spl0_76 ),
inference(avatar_component_clause,[],[f1603]) ).
fof(f1605,plain,
( point_equal(ac,a1)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f1603]) ).
fof(f1608,definition,
( spl0_77
<=> incident(c1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f1609,plain,
( incident(c1,b2c2)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f1608]) ).
fof(f1610,plain,
( ~ incident(c1,b2c2)
| spl0_77 ),
inference(avatar_component_clause,[],[f1608]) ).
fof(f1612,definition,
( spl0_78
<=> point_equal(c1,a1) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f1613,plain,
( ~ point_equal(c1,a1)
| spl0_78 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1614,plain,
( point_equal(c1,a1)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1615,plain,
( ~ spl0_77
| spl0_78
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f1563,f1099,f1612,f1608]) ).
fof(f1649,plain,
( point_equal(b1,a1)
| ~ incident(b1,b2c2)
| ~ spl0_72 ),
inference(resolution,[],[f1283,f91]) ).
fof(f1664,definition,
( spl0_80
<=> point_equal(ab,a1) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f1665,plain,
( ~ point_equal(ab,a1)
| spl0_80 ),
inference(avatar_component_clause,[],[f1664]) ).
fof(f1666,plain,
( point_equal(ab,a1)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f1664]) ).
fof(f1669,definition,
( spl0_81
<=> incident(b1,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f1670,plain,
( incident(b1,b2c2)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f1669]) ).
fof(f1671,plain,
( ~ incident(b1,b2c2)
| spl0_81 ),
inference(avatar_component_clause,[],[f1669]) ).
fof(f1673,definition,
( spl0_82
<=> point_equal(b1,a1) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f1675,plain,
( point_equal(b1,a1)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f1673]) ).
fof(f1676,plain,
( ~ spl0_81
| spl0_82
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1649,f1282,f1673,f1669]) ).
fof(f1727,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,a2b2)
| line_equal(b1c1,a2b2)
| point_equal(X0,c1) )
| ~ spl0_11 ),
inference(resolution,[],[f991,f98]) ).
fof(f1798,definition,
( spl0_87
<=> line_equal(b1c1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f1800,plain,
( line_equal(b1c1,a2b2)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f1798]) ).
fof(f1805,definition,
( spl0_89
<=> ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f1806,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) )
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f1805]) ).
fof(f1807,plain,
( spl0_87
| spl0_89
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1727,f187,f1805,f1798]) ).
fof(f1815,plain,
( incident(b1,a2b2)
| ~ spl0_87 ),
inference(resolution,[],[f1800,f692]) ).
fof(f1818,plain,
( line_equal(a2b2,b1c1)
| ~ spl0_87 ),
inference(resolution,[],[f1800,f129]) ).
fof(f1825,plain,
( spl0_44
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f1815,f1798,f773]) ).
fof(f1832,plain,
( incident(a2,b1c1)
| ~ spl0_87 ),
inference(resolution,[],[f1818,f688]) ).
fof(f1836,plain,
( $false
| spl0_16
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f1832,f214]) ).
fof(f1837,plain,
( spl0_16
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f1836]) ).
fof(f1842,plain,
( point_equal(bc,c1)
| ~ incident(bc,a2b2)
| ~ spl0_89 ),
inference(resolution,[],[f1806,f111]) ).
fof(f1843,plain,
( point_equal(b1,c1)
| ~ incident(b1,a2b2)
| ~ spl0_89 ),
inference(resolution,[],[f1806,f99]) ).
fof(f1845,plain,
( point_equal(b1,c1)
| ~ spl0_44
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f1843,f774]) ).
fof(f1846,plain,
( point_equal(bc,c1)
| ~ spl0_32
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f1842,f467]) ).
fof(f1847,plain,
( ! [X0] :
( ~ incident(c1,X0)
| incident(b1,X0) )
| ~ spl0_44
| ~ spl0_89 ),
inference(resolution,[],[f1845,f131]) ).
fof(f1852,plain,
( point_equal(c1,bc)
| ~ spl0_32
| ~ spl0_89 ),
inference(resolution,[],[f1846,f126]) ).
fof(f1856,plain,
( ! [X0] :
( ~ incident(bc,X0)
| incident(c1,X0) )
| ~ spl0_32
| ~ spl0_89 ),
inference(resolution,[],[f1852,f131]) ).
fof(f1861,plain,
( incident(b1,a1c1)
| ~ spl0_44
| ~ spl0_89 ),
inference(resolution,[],[f1847,f95]) ).
fof(f1865,plain,
( $false
| ~ spl0_44
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f1861,f200]) ).
fof(f1866,plain,
( ~ spl0_44
| ~ spl0_89 ),
inference(avatar_contradiction_clause,[],[f1865]) ).
fof(f1912,plain,
( incident(c1,b2c2)
| ~ spl0_32
| ~ spl0_89 ),
inference(resolution,[],[f1856,f112]) ).
fof(f1918,plain,
( $false
| ~ spl0_32
| spl0_77
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f1912,f1610]) ).
fof(f1919,plain,
( ~ spl0_32
| spl0_77
| ~ spl0_89 ),
inference(avatar_contradiction_clause,[],[f1918]) ).
fof(f1920,plain,
( ! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b1c1)
| line_equal(X0,b1c1)
| point_equal(X1,a2) )
| ~ spl0_16 ),
inference(resolution,[],[f213,f133]) ).
fof(f1985,plain,
( ! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2c2)
| line_equal(X0,b2c2)
| point_equal(X1,a1) )
| ~ spl0_13 ),
inference(resolution,[],[f196,f133]) ).
fof(f1996,plain,
( incident(b1,b2c2)
| ~ spl0_70 ),
inference(resolution,[],[f1277,f700]) ).
fof(f1999,plain,
( line_equal(b2c2,a1b1)
| ~ spl0_70 ),
inference(resolution,[],[f1277,f129]) ).
fof(f2000,plain,
( $false
| ~ spl0_70
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f1996,f1671]) ).
fof(f2001,plain,
( ~ spl0_70
| spl0_81 ),
inference(avatar_contradiction_clause,[],[f2000]) ).
fof(f2010,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(ac,X0) )
| ~ spl0_76 ),
inference(resolution,[],[f1605,f131]) ).
fof(f2013,plain,
( ~ incident(b1,b2c2)
| ~ incident(a1,b2c2)
| ~ spl0_77 ),
inference(resolution,[],[f1609,f142]) ).
fof(f2018,plain,
( ~ incident(b1,b2c2)
| ~ spl0_13
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f2013,f196]) ).
fof(f2019,plain,
( ~ spl0_81
| ~ spl0_13
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2018,f1608,f195,f1669]) ).
fof(f2036,plain,
( incident(c2,a1b1)
| ~ spl0_70 ),
inference(resolution,[],[f1999,f684]) ).
fof(f2041,plain,
( $false
| spl0_14
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f2036,f206]) ).
fof(f2042,plain,
( spl0_14
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f2041]) ).
fof(f2066,plain,
( incident(ac,b2c2)
| ~ spl0_13
| ~ spl0_76 ),
inference(resolution,[],[f2010,f196]) ).
fof(f2068,plain,
( incident(ac,a1b1)
| ~ spl0_76 ),
inference(resolution,[],[f2010,f90]) ).
fof(f2071,plain,
( $false
| spl0_28
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f2068,f451]) ).
fof(f2072,plain,
( spl0_28
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f2071]) ).
fof(f2073,plain,
( $false
| ~ spl0_13
| spl0_75
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f2066,f1601]) ).
fof(f2074,plain,
( ~ spl0_13
| spl0_75
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f2073]) ).
fof(f2110,plain,
! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,b2c2)
| line_equal(b1c1,b2c2)
| point_equal(X0,bc) ),
inference(resolution,[],[f982,f111]) ).
fof(f2113,plain,
! [X0] :
( ~ incident(X0,b1c1)
| ~ incident(X0,b2c2)
| point_equal(X0,bc) ),
inference(forward_subsumption_resolution,[],[f2110,f137]) ).
fof(f2123,plain,
( ~ incident(b1,b2c2)
| point_equal(b1,bc) ),
inference(resolution,[],[f2113,f99]) ).
fof(f2124,plain,
( ~ incident(c1,b2c2)
| point_equal(c1,bc) ),
inference(resolution,[],[f2113,f98]) ).
fof(f2126,plain,
( point_equal(b1,bc)
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2123,f1670]) ).
fof(f2127,plain,
( ! [X0] :
( ~ incident(bc,X0)
| incident(b1,X0) )
| ~ spl0_81 ),
inference(resolution,[],[f2126,f131]) ).
fof(f2129,plain,
( point_equal(bc,b1)
| ~ spl0_81 ),
inference(resolution,[],[f2126,f126]) ).
fof(f2130,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(bc,X0) )
| ~ spl0_81 ),
inference(resolution,[],[f2129,f131]) ).
fof(f2134,plain,
( incident(b1,a2b2)
| ~ spl0_32
| ~ spl0_81 ),
inference(resolution,[],[f2127,f467]) ).
fof(f2137,plain,
( $false
| ~ spl0_32
| spl0_44
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2134,f775]) ).
fof(f2138,plain,
( ~ spl0_32
| spl0_44
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2137]) ).
fof(f2155,plain,
( incident(bc,a2c2)
| ~ spl0_12
| ~ spl0_81 ),
inference(resolution,[],[f2130,f192]) ).
fof(f2161,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| ~ incident(X0,b2c2)
| line_equal(a2c2,b2c2)
| point_equal(X0,bc) )
| ~ spl0_12
| ~ spl0_81 ),
inference(resolution,[],[f2155,f982]) ).
fof(f2188,definition,
( spl0_97
<=> line_equal(a2b2,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f2189,plain,
( ~ line_equal(a2b2,b2c2)
| spl0_97 ),
inference(avatar_component_clause,[],[f2188]) ).
fof(f2190,plain,
( line_equal(a2b2,b2c2)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f2188]) ).
fof(f2199,plain,
( incident(a2,b2c2)
| ~ spl0_97 ),
inference(resolution,[],[f2190,f688]) ).
fof(f2203,plain,
( $false
| ~ spl0_97 ),
inference(forward_subsumption_resolution,[],[f2199,f221]) ).
fof(f2204,plain,
~ spl0_97,
inference(avatar_contradiction_clause,[],[f2203]) ).
fof(f2213,plain,
! [X0] :
( ~ incident(X0,a2b2)
| ~ incident(X0,b2c2)
| line_equal(a2b2,b2c2)
| point_equal(X0,b2) ),
inference(resolution,[],[f984,f93]) ).
fof(f2215,plain,
! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,b2c2)
| line_equal(ob,b2c2)
| point_equal(X0,b2) ),
inference(resolution,[],[f984,f108]) ).
fof(f2217,plain,
( ! [X0] :
( ~ incident(X0,a2b2)
| ~ incident(X0,b2c2)
| point_equal(X0,b2) )
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f2213,f2189]) ).
fof(f2280,definition,
( spl0_102
<=> line_equal(a2c2,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f2281,plain,
( ~ line_equal(a2c2,b2c2)
| spl0_102 ),
inference(avatar_component_clause,[],[f2280]) ).
fof(f2282,plain,
( line_equal(a2c2,b2c2)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f2280]) ).
fof(f2287,definition,
( spl0_104
<=> ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,bc)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f2288,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,bc)
| ~ incident(X0,b2c2) )
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f2287]) ).
fof(f2289,plain,
( spl0_102
| spl0_104
| ~ spl0_12
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f2161,f1669,f191,f2287,f2280]) ).
fof(f2304,plain,
( incident(a2,b2c2)
| ~ spl0_102 ),
inference(resolution,[],[f2282,f685]) ).
fof(f2308,plain,
( $false
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f2304,f221]) ).
fof(f2309,plain,
~ spl0_102,
inference(avatar_contradiction_clause,[],[f2308]) ).
fof(f2377,definition,
( spl0_105
<=> line_equal(ob,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f2379,plain,
( line_equal(ob,b2c2)
| ~ spl0_105 ),
inference(avatar_component_clause,[],[f2377]) ).
fof(f2384,definition,
( spl0_107
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f2385,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b2)
| ~ incident(X0,b2c2) )
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f2384]) ).
fof(f2386,plain,
( spl0_105
| spl0_107 ),
inference(avatar_split_clause,[],[f2215,f2384,f2377]) ).
fof(f2407,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| ~ incident(X0,b1c1)
| line_equal(a2c2,b1c1)
| point_equal(X0,a2) )
| ~ spl0_16 ),
inference(resolution,[],[f1920,f96]) ).
fof(f2410,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,b1c1)
| line_equal(oa,b1c1)
| point_equal(X0,a2) )
| ~ spl0_16 ),
inference(resolution,[],[f1920,f106]) ).
fof(f2411,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b1c1)
| line_equal(oc,b1c1)
| point_equal(X0,a2) )
| ~ spl0_16
| ~ spl0_19 ),
inference(resolution,[],[f1920,f235]) ).
fof(f2477,definition,
( spl0_111
<=> line_equal(a2c2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f2479,plain,
( line_equal(a2c2,b1c1)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f2477]) ).
fof(f2481,definition,
( spl0_112
<=> ! [X0] :
( ~ incident(X0,a2c2)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f2482,plain,
( ! [X0] :
( ~ incident(X0,b1c1)
| point_equal(X0,a2)
| ~ incident(X0,a2c2) )
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f2481]) ).
fof(f2483,plain,
( spl0_111
| spl0_112
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f2407,f212,f2481,f2477]) ).
fof(f2488,plain,
( line_equal(b1c1,a2c2)
| ~ spl0_111 ),
inference(resolution,[],[f2479,f129]) ).
fof(f2491,plain,
( incident(o,b2c2)
| ~ spl0_105 ),
inference(resolution,[],[f2379,f705]) ).
fof(f2512,plain,
( incident(b1,a2c2)
| ~ spl0_111 ),
inference(resolution,[],[f2488,f692]) ).
fof(f2516,plain,
( $false
| spl0_12
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f2512,f193]) ).
fof(f2517,plain,
( spl0_12
| ~ spl0_111 ),
inference(avatar_contradiction_clause,[],[f2516]) ).
fof(f2662,plain,
( point_equal(b1,a2)
| ~ incident(b1,a2c2)
| ~ spl0_112 ),
inference(resolution,[],[f2482,f99]) ).
fof(f2666,definition,
( spl0_115
<=> incident(bc,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f2668,plain,
( ~ incident(bc,a2c2)
| spl0_115 ),
inference(avatar_component_clause,[],[f2666]) ).
fof(f2675,definition,
( spl0_117
<=> incident(c1,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f2676,plain,
( incident(c1,a2c2)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f2675]) ).
fof(f2677,plain,
( ~ incident(c1,a2c2)
| spl0_117 ),
inference(avatar_component_clause,[],[f2675]) ).
fof(f2679,definition,
( spl0_118
<=> point_equal(c1,a2) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f2681,plain,
( point_equal(c1,a2)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f2679]) ).
fof(f2707,definition,
( spl0_121
<=> line_equal(oa,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f2709,plain,
( line_equal(oa,b1c1)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f2707]) ).
fof(f2714,definition,
( spl0_123
<=> ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f2715,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) )
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f2714]) ).
fof(f2716,plain,
( spl0_121
| spl0_123
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f2410,f212,f2714,f2707]) ).
fof(f2724,plain,
( incident(a1,b1c1)
| ~ spl0_121 ),
inference(resolution,[],[f2709,f703]) ).
fof(f2728,plain,
( $false
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f2724,f219]) ).
fof(f2729,plain,
~ spl0_121,
inference(avatar_contradiction_clause,[],[f2728]) ).
fof(f2732,plain,
( point_equal(o,a2)
| ~ incident(o,b1c1)
| ~ spl0_123 ),
inference(resolution,[],[f2715,f102]) ).
fof(f2734,definition,
( spl0_124
<=> incident(o,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f2736,plain,
( ~ incident(o,b1c1)
| spl0_124 ),
inference(avatar_component_clause,[],[f2734]) ).
fof(f2738,definition,
( spl0_125
<=> point_equal(o,a2) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f2739,plain,
( ~ point_equal(o,a2)
| spl0_125 ),
inference(avatar_component_clause,[],[f2738]) ).
fof(f2740,plain,
( point_equal(o,a2)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f2738]) ).
fof(f2741,plain,
( ~ spl0_124
| spl0_125
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f2732,f2714,f2738,f2734]) ).
fof(f2743,definition,
( spl0_126
<=> line_equal(oc,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f2744,plain,
( ~ line_equal(oc,b1c1)
| spl0_126 ),
inference(avatar_component_clause,[],[f2743]) ).
fof(f2745,plain,
( line_equal(oc,b1c1)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f2743]) ).
fof(f2747,definition,
( spl0_127
<=> ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) ) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f2748,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,a2)
| ~ incident(X0,b1c1) )
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2749,plain,
( spl0_126
| spl0_127
| ~ spl0_16
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f2411,f234,f212,f2747,f2743]) ).
fof(f2753,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,b2c2)
| line_equal(oa,b2c2)
| point_equal(X0,a1) )
| ~ spl0_13 ),
inference(resolution,[],[f1985,f105]) ).
fof(f2755,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b2c2)
| line_equal(oc,b2c2)
| point_equal(X0,a1) )
| ~ spl0_13
| ~ spl0_17 ),
inference(resolution,[],[f1985,f225]) ).
fof(f2758,plain,
( incident(o,b1c1)
| ~ spl0_126 ),
inference(resolution,[],[f2745,f708]) ).
fof(f2759,plain,
( incident(a1,b1c1)
| ~ spl0_17
| ~ spl0_126 ),
inference(resolution,[],[f2745,f1367]) ).
fof(f2764,plain,
( $false
| ~ spl0_17
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f2759,f219]) ).
fof(f2765,plain,
( ~ spl0_17
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f2764]) ).
fof(f2766,plain,
( $false
| spl0_124
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f2758,f2736]) ).
fof(f2767,plain,
( spl0_124
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f2766]) ).
fof(f2769,plain,
( point_equal(c1,a2)
| ~ incident(c1,b1c1)
| ~ spl0_127 ),
inference(resolution,[],[f2748,f109]) ).
fof(f2773,plain,
( point_equal(c1,a2)
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f2769,f98]) ).
fof(f2774,plain,
( spl0_118
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f2773,f2747,f2679]) ).
fof(f2775,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(c1,X0) )
| ~ spl0_118 ),
inference(resolution,[],[f2681,f131]) ).
fof(f2782,definition,
( spl0_128
<=> incident(c2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f2783,plain,
( incident(c2,b1c1)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f2782]) ).
fof(f2784,plain,
( ~ incident(c2,b1c1)
| spl0_128 ),
inference(avatar_component_clause,[],[f2782]) ).
fof(f2786,definition,
( spl0_129
<=> point_equal(c2,a2) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f2787,plain,
( ~ point_equal(c2,a2)
| spl0_129 ),
inference(avatar_component_clause,[],[f2786]) ).
fof(f2788,plain,
( point_equal(c2,a2)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f2786]) ).
fof(f2791,plain,
( incident(c1,a2b2)
| ~ spl0_118 ),
inference(resolution,[],[f2775,f92]) ).
fof(f2795,plain,
( $false
| spl0_11
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2791,f189]) ).
fof(f2796,plain,
( spl0_11
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f2795]) ).
fof(f2801,plain,
( ! [X0,X1] :
( ~ incident(c1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2b2)
| line_equal(X0,a2b2)
| point_equal(X1,c1) )
| ~ spl0_11 ),
inference(resolution,[],[f188,f133]) ).
fof(f2861,definition,
( spl0_132
<=> line_equal(oa,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f2863,plain,
( line_equal(oa,b2c2)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f2861]) ).
fof(f2865,definition,
( spl0_133
<=> ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f2866,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f2865]) ).
fof(f2867,plain,
( spl0_132
| spl0_133
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f2753,f195,f2865,f2861]) ).
fof(f2869,plain,
( incident(a2,b2c2)
| ~ spl0_132 ),
inference(resolution,[],[f2863,f704]) ).
fof(f2876,plain,
( $false
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f2869,f221]) ).
fof(f2877,plain,
~ spl0_132,
inference(avatar_contradiction_clause,[],[f2876]) ).
fof(f2883,plain,
( point_equal(o,a1)
| ~ incident(o,b2c2)
| ~ spl0_133 ),
inference(resolution,[],[f2866,f102]) ).
fof(f2884,plain,
( point_equal(o,a1)
| ~ spl0_105
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2883,f2491]) ).
fof(f2887,plain,
( point_equal(a1,o)
| ~ spl0_105
| ~ spl0_133 ),
inference(resolution,[],[f2884,f126]) ).
fof(f2888,plain,
( ! [X0] :
( ~ incident(o,X0)
| incident(a1,X0) )
| ~ spl0_105
| ~ spl0_133 ),
inference(resolution,[],[f2887,f131]) ).
fof(f2919,plain,
( incident(a1,oc)
| ~ spl0_105
| ~ spl0_133 ),
inference(resolution,[],[f2888,f104]) ).
fof(f2944,definition,
( spl0_137
<=> line_equal(oc,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f2945,plain,
( ~ line_equal(oc,b2c2)
| spl0_137 ),
inference(avatar_component_clause,[],[f2944]) ).
fof(f2946,plain,
( line_equal(oc,b2c2)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f2944]) ).
fof(f2948,definition,
( spl0_138
<=> ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f2949,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,a1)
| ~ incident(X0,b2c2) )
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f2948]) ).
fof(f2950,plain,
( spl0_137
| spl0_138
| ~ spl0_13
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f2755,f224,f195,f2948,f2944]) ).
fof(f2955,plain,
( incident(c1,b2c2)
| ~ spl0_137 ),
inference(resolution,[],[f2946,f709]) ).
fof(f2960,plain,
( $false
| spl0_77
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f2955,f1610]) ).
fof(f2961,plain,
( spl0_77
| ~ spl0_137 ),
inference(avatar_contradiction_clause,[],[f2960]) ).
fof(f3083,plain,
( $false
| spl0_17
| ~ spl0_105
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2919,f226]) ).
fof(f3084,plain,
( spl0_17
| ~ spl0_105
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f3083]) ).
fof(f3098,definition,
( spl0_142
<=> incident(o,b2c2) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f3099,plain,
( incident(o,b2c2)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f3098]) ).
fof(f3100,plain,
( ~ incident(o,b2c2)
| spl0_142 ),
inference(avatar_component_clause,[],[f3098]) ).
fof(f3102,definition,
( spl0_143
<=> point_equal(o,a1) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f3103,plain,
( ~ point_equal(o,a1)
| spl0_143 ),
inference(avatar_component_clause,[],[f3102]) ).
fof(f3104,plain,
( point_equal(o,a1)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f3102]) ).
fof(f3105,plain,
( ~ spl0_142
| spl0_143
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2883,f2865,f3102,f3098]) ).
fof(f3121,plain,
( ! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,oc)
| line_equal(X0,oc)
| point_equal(X1,a1) )
| ~ spl0_17 ),
inference(resolution,[],[f225,f133]) ).
fof(f3245,plain,
( point_equal(b1,b2)
| ~ incident(b1,b2c2)
| ~ spl0_107 ),
inference(resolution,[],[f2385,f107]) ).
fof(f3251,plain,
( point_equal(b1,b2)
| ~ spl0_81
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f3245,f1670]) ).
fof(f3261,plain,
( point_equal(b2,b1)
| ~ spl0_81
| ~ spl0_107 ),
inference(resolution,[],[f3251,f126]) ).
fof(f3262,plain,
( $false
| ~ spl0_81
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f3261,f139]) ).
fof(f3263,plain,
( ~ spl0_81
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f3262]) ).
fof(f3267,plain,
( point_equal(c2,a1)
| ~ incident(c2,b2c2)
| ~ spl0_138 ),
inference(resolution,[],[f2949,f110]) ).
fof(f3269,plain,
( point_equal(c2,a1)
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f3267,f100]) ).
fof(f3271,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(c2,X0) )
| ~ spl0_138 ),
inference(resolution,[],[f3269,f131]) ).
fof(f3272,plain,
( ! [X0] :
( ~ point_equal(X0,c2)
| point_equal(X0,a1) )
| ~ spl0_138 ),
inference(resolution,[],[f3269,f127]) ).
fof(f3285,plain,
( incident(c2,a1c1)
| ~ spl0_138 ),
inference(resolution,[],[f3271,f94]) ).
fof(f3419,definition,
( spl0_148
<=> incident(ab,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f3420,plain,
( incident(ab,a2c2)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f3419]) ).
fof(f3421,plain,
( ~ incident(ab,a2c2)
| spl0_148 ),
inference(avatar_component_clause,[],[f3419]) ).
fof(f3454,definition,
( spl0_152
<=> incident(c1,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f3455,plain,
( incident(c1,a1b1)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f3454]) ).
fof(f3456,plain,
( ~ incident(c1,a1b1)
| spl0_152 ),
inference(avatar_component_clause,[],[f3454]) ).
fof(f3458,definition,
( spl0_153
<=> point_equal(c1,c2) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f3459,plain,
( ~ point_equal(c1,c2)
| spl0_153 ),
inference(avatar_component_clause,[],[f3458]) ).
fof(f3460,plain,
( point_equal(c1,c2)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f3458]) ).
fof(f3496,definition,
( spl0_156
<=> incident(bc,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f3500,definition,
( spl0_157
<=> point_equal(bc,c2) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f3501,plain,
( ~ point_equal(bc,c2)
| spl0_157 ),
inference(avatar_component_clause,[],[f3500]) ).
fof(f3502,plain,
( point_equal(bc,c2)
| ~ spl0_157 ),
inference(avatar_component_clause,[],[f3500]) ).
fof(f3505,definition,
( spl0_158
<=> incident(ab,a1c1) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f3506,plain,
( incident(ab,a1c1)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f3505]) ).
fof(f3615,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,a2b2)
| line_equal(a1c1,a2b2)
| point_equal(X0,c1) )
| ~ spl0_11 ),
inference(resolution,[],[f2801,f95]) ).
fof(f3617,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,a2b2)
| line_equal(oc,a2b2)
| point_equal(X0,c1) )
| ~ spl0_11 ),
inference(resolution,[],[f2801,f109]) ).
fof(f3620,definition,
( spl0_161
<=> line_equal(a1c1,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f3622,plain,
( line_equal(a1c1,a2b2)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f3620]) ).
fof(f3624,definition,
( spl0_162
<=> ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f3625,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) )
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f3624]) ).
fof(f3626,plain,
( spl0_161
| spl0_162
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f3615,f187,f3624,f3620]) ).
fof(f3630,plain,
( incident(ac,a2b2)
| ~ spl0_161 ),
inference(resolution,[],[f3622,f697]) ).
fof(f3632,plain,
( incident(a1,a2b2)
| ~ spl0_161 ),
inference(resolution,[],[f3622,f695]) ).
fof(f3635,plain,
( $false
| spl0_43
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f3632,f771]) ).
fof(f3636,plain,
( spl0_43
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f3635]) ).
fof(f3637,plain,
( $false
| spl0_31
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f3630,f464]) ).
fof(f3638,plain,
( spl0_31
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f3637]) ).
fof(f3647,definition,
( spl0_163
<=> incident(o,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f3648,plain,
( incident(o,a2b2)
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f3647]) ).
fof(f3649,plain,
( ~ incident(o,a2b2)
| spl0_163 ),
inference(avatar_component_clause,[],[f3647]) ).
fof(f3651,definition,
( spl0_164
<=> point_equal(o,c1) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f3652,plain,
( ~ point_equal(o,c1)
| spl0_164 ),
inference(avatar_component_clause,[],[f3651]) ).
fof(f3653,plain,
( point_equal(o,c1)
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f3651]) ).
fof(f3656,definition,
( spl0_165
<=> line_equal(oc,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f3658,plain,
( line_equal(oc,a2b2)
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f3656]) ).
fof(f3660,definition,
( spl0_166
<=> ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f3661,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,c1)
| ~ incident(X0,a2b2) )
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f3660]) ).
fof(f3662,plain,
( spl0_165
| spl0_166
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f3617,f187,f3660,f3656]) ).
fof(f3734,plain,
( incident(c2,a2b2)
| ~ spl0_165 ),
inference(resolution,[],[f3658,f710]) ).
fof(f3759,plain,
( ~ incident(b2,a2b2)
| ~ incident(a2,a2b2)
| ~ spl0_165 ),
inference(resolution,[],[f3734,f141]) ).
fof(f3765,plain,
( ~ incident(a2,a2b2)
| ~ spl0_165 ),
inference(forward_subsumption_resolution,[],[f3759,f93]) ).
fof(f3767,plain,
( $false
| ~ spl0_165 ),
inference(forward_subsumption_resolution,[],[f3765,f92]) ).
fof(f3768,plain,
~ spl0_165,
inference(avatar_contradiction_clause,[],[f3767]) ).
fof(f3794,plain,
( ! [X0] :
( ~ line_equal(b1c1,X0)
| incident(a2,X0) )
| ~ spl0_16 ),
inference(resolution,[],[f213,f132]) ).
fof(f3865,plain,
! [X0] :
( ~ incident(X0,a2c2)
| ~ incident(X0,b2c2)
| line_equal(a2c2,b2c2)
| point_equal(X0,c2) ),
inference(resolution,[],[f985,f97]) ).
fof(f3870,plain,
! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b2c2)
| line_equal(oc,b2c2)
| point_equal(X0,c2) ),
inference(resolution,[],[f985,f110]) ).
fof(f3875,plain,
( ! [X0] :
( ~ incident(X0,a2c2)
| ~ incident(X0,b2c2)
| point_equal(X0,c2) )
| spl0_102 ),
inference(forward_subsumption_resolution,[],[f3865,f2281]) ).
fof(f3880,plain,
( ~ incident(ac,b2c2)
| point_equal(ac,c2)
| spl0_102 ),
inference(resolution,[],[f3875,f114]) ).
fof(f3898,plain,
! [X0] :
( ~ incident(X0,a2b2)
| ~ incident(X0,a2c2)
| line_equal(a2b2,a2c2)
| point_equal(X0,a2) ),
inference(resolution,[],[f986,f92]) ).
fof(f3900,plain,
! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,a2c2)
| line_equal(oa,a2c2)
| point_equal(X0,a2) ),
inference(resolution,[],[f986,f106]) ).
fof(f4030,definition,
( spl0_172
<=> incident(ab,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f4031,plain,
( incident(ab,b1c1)
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f4030]) ).
fof(f4032,plain,
( ~ incident(ab,b1c1)
| spl0_172 ),
inference(avatar_component_clause,[],[f4030]) ).
fof(f4039,definition,
( spl0_174
<=> incident(b2,b1c1) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f4040,plain,
( incident(b2,b1c1)
| ~ spl0_174 ),
inference(avatar_component_clause,[],[f4039]) ).
fof(f4041,plain,
( ~ incident(b2,b1c1)
| spl0_174 ),
inference(avatar_component_clause,[],[f4039]) ).
fof(f4043,definition,
( spl0_175
<=> point_equal(b2,bc) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f4044,plain,
( ~ point_equal(b2,bc)
| spl0_175 ),
inference(avatar_component_clause,[],[f4043]) ).
fof(f4045,plain,
( point_equal(b2,bc)
| ~ spl0_175 ),
inference(avatar_component_clause,[],[f4043]) ).
fof(f4048,definition,
( spl0_176
<=> line_equal(a2b2,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f4050,plain,
( line_equal(a2b2,a2c2)
| ~ spl0_176 ),
inference(avatar_component_clause,[],[f4048]) ).
fof(f4052,definition,
( spl0_177
<=> ! [X0] :
( ~ incident(X0,a2b2)
| point_equal(X0,a2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f4053,plain,
( ! [X0] :
( ~ incident(X0,a2b2)
| point_equal(X0,a2)
| ~ incident(X0,a2c2) )
| ~ spl0_177 ),
inference(avatar_component_clause,[],[f4052]) ).
fof(f4054,plain,
( spl0_176
| spl0_177 ),
inference(avatar_split_clause,[],[f3898,f4052,f4048]) ).
fof(f4069,plain,
( incident(b2,a2c2)
| ~ spl0_176 ),
inference(resolution,[],[f4050,f689]) ).
fof(f4075,plain,
( $false
| ~ spl0_176 ),
inference(forward_subsumption_resolution,[],[f4069,f217]) ).
fof(f4076,plain,
~ spl0_176,
inference(avatar_contradiction_clause,[],[f4075]) ).
fof(f4101,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,oc)
| line_equal(a1c1,oc)
| point_equal(X0,a1) )
| ~ spl0_17 ),
inference(resolution,[],[f3121,f94]) ).
fof(f4111,definition,
( spl0_180
<=> line_equal(a1c1,oc) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f4113,plain,
( line_equal(a1c1,oc)
| ~ spl0_180 ),
inference(avatar_component_clause,[],[f4111]) ).
fof(f4115,definition,
( spl0_181
<=> ! [X0] :
( ~ incident(X0,a1c1)
| point_equal(X0,a1)
| ~ incident(X0,oc) ) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f4116,plain,
( ! [X0] :
( ~ incident(X0,oc)
| point_equal(X0,a1)
| ~ incident(X0,a1c1) )
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f4115]) ).
fof(f4117,plain,
( spl0_180
| spl0_181
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f4101,f224,f4115,f4111]) ).
fof(f4120,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,a2c2)
| line_equal(a1c1,a2c2)
| point_equal(X0,c2) )
| ~ spl0_138 ),
inference(resolution,[],[f987,f3285]) ).
fof(f4124,plain,
! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,a2c2)
| line_equal(oc,a2c2)
| point_equal(X0,c2) ),
inference(resolution,[],[f987,f110]) ).
fof(f4126,plain,
( ! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,a2c2)
| point_equal(X0,c2) )
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f4120,f136]) ).
fof(f4165,plain,
( ~ incident(ac,a2c2)
| point_equal(ac,c2)
| ~ spl0_138 ),
inference(resolution,[],[f4126,f113]) ).
fof(f4170,plain,
( point_equal(ac,c2)
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f4165,f114]) ).
fof(f4172,plain,
( point_equal(ac,a1)
| ~ spl0_138 ),
inference(resolution,[],[f4170,f3272]) ).
fof(f4176,plain,
( $false
| spl0_76
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f4172,f1604]) ).
fof(f4177,plain,
( spl0_76
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f4176]) ).
fof(f4192,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(ab,X0) )
| ~ spl0_80 ),
inference(resolution,[],[f1666,f131]) ).
fof(f4211,plain,
! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,a2c2)
| line_equal(a1c1,a2c2)
| point_equal(X0,ac) ),
inference(resolution,[],[f988,f113]) ).
fof(f4213,plain,
! [X0] :
( ~ incident(X0,a1c1)
| ~ incident(X0,a2c2)
| point_equal(X0,ac) ),
inference(forward_subsumption_resolution,[],[f4211,f136]) ).
fof(f4270,definition,
( spl0_186
<=> incident(o,a1b1) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f4271,plain,
( incident(o,a1b1)
| ~ spl0_186 ),
inference(avatar_component_clause,[],[f4270]) ).
fof(f4272,plain,
( ~ incident(o,a1b1)
| spl0_186 ),
inference(avatar_component_clause,[],[f4270]) ).
fof(f4274,definition,
( spl0_187
<=> point_equal(o,c2) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f4275,plain,
( ~ point_equal(o,c2)
| spl0_187 ),
inference(avatar_component_clause,[],[f4274]) ).
fof(f4276,plain,
( point_equal(o,c2)
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f4274]) ).
fof(f4279,definition,
( spl0_188
<=> incident(c2,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f4280,plain,
( incident(c2,a2b2)
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f4279]) ).
fof(f4281,plain,
( ~ incident(c2,a2b2)
| spl0_188 ),
inference(avatar_component_clause,[],[f4279]) ).
fof(f4288,plain,
( incident(ab,a1c1)
| ~ spl0_80 ),
inference(resolution,[],[f4192,f94]) ).
fof(f4293,plain,
( spl0_158
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f4288,f1664,f3505]) ).
fof(f4354,definition,
( spl0_192
<=> incident(a1,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f4355,plain,
( incident(a1,a2c2)
| ~ spl0_192 ),
inference(avatar_component_clause,[],[f4354]) ).
fof(f4356,plain,
( ~ incident(a1,a2c2)
| spl0_192 ),
inference(avatar_component_clause,[],[f4354]) ).
fof(f4358,definition,
( spl0_193
<=> point_equal(a1,c2) ),
introduced(definition,[new_symbols(definition,[spl0_193])],[avatar_definition]) ).
fof(f4360,plain,
( point_equal(a1,c2)
| ~ spl0_193 ),
inference(avatar_component_clause,[],[f4358]) ).
fof(f4379,plain,
( ~ incident(b1,a1b1)
| ~ incident(a1,a1b1)
| ~ spl0_152 ),
inference(resolution,[],[f3455,f142]) ).
fof(f4385,plain,
( ~ incident(a1,a1b1)
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f4379,f91]) ).
fof(f4386,plain,
( $false
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f4385,f90]) ).
fof(f4387,plain,
~ spl0_152,
inference(avatar_contradiction_clause,[],[f4386]) ).
fof(f4390,plain,
( point_equal(c2,c1)
| ~ spl0_153 ),
inference(resolution,[],[f3460,f126]) ).
fof(f4391,plain,
( $false
| ~ spl0_153 ),
inference(forward_subsumption_resolution,[],[f4390,f138]) ).
fof(f4392,plain,
~ spl0_153,
inference(avatar_contradiction_clause,[],[f4391]) ).
fof(f4400,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(c2,X0) )
| ~ spl0_129 ),
inference(resolution,[],[f2788,f131]) ).
fof(f4426,plain,
( point_equal(b1,a2)
| ~ spl0_12
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f2662,f192]) ).
fof(f4427,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(b1,X0) )
| ~ spl0_12
| ~ spl0_112 ),
inference(resolution,[],[f4426,f131]) ).
fof(f4434,plain,
( incident(c2,a2b2)
| ~ spl0_129 ),
inference(resolution,[],[f4400,f92]) ).
fof(f4442,plain,
( $false
| ~ spl0_129
| spl0_188 ),
inference(forward_subsumption_resolution,[],[f4434,f4281]) ).
fof(f4443,plain,
( ~ spl0_129
| spl0_188 ),
inference(avatar_contradiction_clause,[],[f4442]) ).
fof(f4445,plain,
( point_equal(c2,a2)
| ~ incident(c2,a2c2)
| ~ spl0_112
| ~ spl0_128 ),
inference(resolution,[],[f2783,f2482]) ).
fof(f4460,plain,
( ~ incident(b2,a2b2)
| ~ incident(a2,a2b2)
| ~ spl0_188 ),
inference(resolution,[],[f4280,f141]) ).
fof(f4466,plain,
( ~ incident(a2,a2b2)
| ~ spl0_188 ),
inference(forward_subsumption_resolution,[],[f4460,f93]) ).
fof(f4470,plain,
( $false
| ~ spl0_188 ),
inference(forward_subsumption_resolution,[],[f4466,f92]) ).
fof(f4471,plain,
~ spl0_188,
inference(avatar_contradiction_clause,[],[f4470]) ).
fof(f4472,plain,
( point_equal(c2,a2)
| ~ spl0_112
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f4445,f97]) ).
fof(f4476,plain,
( $false
| ~ spl0_112
| ~ spl0_128
| spl0_129 ),
inference(forward_subsumption_resolution,[],[f4472,f2787]) ).
fof(f4477,plain,
( ~ spl0_112
| ~ spl0_128
| spl0_129 ),
inference(avatar_contradiction_clause,[],[f4476]) ).
fof(f4479,plain,
( incident(b1,a2b2)
| ~ spl0_12
| ~ spl0_112 ),
inference(resolution,[],[f4427,f92]) ).
fof(f4482,plain,
( $false
| ~ spl0_12
| spl0_44
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f4479,f775]) ).
fof(f4483,plain,
( ~ spl0_12
| spl0_44
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f4482]) ).
fof(f4565,plain,
( point_equal(c2,a1)
| ~ incident(c2,b2c2)
| ~ spl0_14
| ~ spl0_72 ),
inference(resolution,[],[f1283,f205]) ).
fof(f4566,plain,
( point_equal(c2,a1)
| ~ spl0_14
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f4565,f100]) ).
fof(f4569,plain,
( point_equal(a1,c2)
| ~ spl0_14
| ~ spl0_72 ),
inference(resolution,[],[f4566,f126]) ).
fof(f4570,plain,
( spl0_193
| ~ spl0_14
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f4569,f1282,f204,f4358]) ).
fof(f4571,plain,
( ! [X0] :
( ~ incident(c2,X0)
| incident(a1,X0) )
| ~ spl0_193 ),
inference(resolution,[],[f4360,f131]) ).
fof(f4602,plain,
( incident(a1,a2c2)
| ~ spl0_193 ),
inference(resolution,[],[f4571,f97]) ).
fof(f4606,plain,
( incident(a1,oc)
| ~ spl0_193 ),
inference(resolution,[],[f4571,f110]) ).
fof(f4607,plain,
( $false
| spl0_17
| ~ spl0_193 ),
inference(forward_subsumption_resolution,[],[f4606,f226]) ).
fof(f4608,plain,
( spl0_17
| ~ spl0_193 ),
inference(avatar_contradiction_clause,[],[f4607]) ).
fof(f4609,plain,
( $false
| spl0_192
| ~ spl0_193 ),
inference(forward_subsumption_resolution,[],[f4602,f4356]) ).
fof(f4610,plain,
( spl0_192
| ~ spl0_193 ),
inference(avatar_contradiction_clause,[],[f4609]) ).
fof(f4612,plain,
( ! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2c2)
| line_equal(X0,a2c2)
| point_equal(X1,b1) )
| ~ spl0_12 ),
inference(resolution,[],[f192,f133]) ).
fof(f4616,plain,
( point_equal(b1,a2)
| ~ incident(b1,a2c2)
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f774,f4053]) ).
fof(f4622,plain,
( point_equal(b1,a2)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(forward_subsumption_resolution,[],[f4616,f192]) ).
fof(f4625,plain,
( point_equal(a2,b1)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f4622,f126]) ).
fof(f4626,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(a2,X0) )
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f4625,f131]) ).
fof(f4648,plain,
( incident(a2,a1b1)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f4626,f91]) ).
fof(f4651,plain,
( $false
| ~ spl0_12
| spl0_21
| ~ spl0_44
| ~ spl0_177 ),
inference(forward_subsumption_resolution,[],[f4648,f257]) ).
fof(f4652,plain,
( ~ spl0_12
| spl0_21
| ~ spl0_44
| ~ spl0_177 ),
inference(avatar_contradiction_clause,[],[f4651]) ).
fof(f4678,plain,
( ~ incident(a1,a2c2)
| point_equal(a1,ac) ),
inference(resolution,[],[f4213,f94]) ).
fof(f4683,plain,
( point_equal(o,b2)
| ~ incident(o,b2c2)
| ~ spl0_107 ),
inference(resolution,[],[f2385,f103]) ).
fof(f4833,plain,
( incident(c2,b1c1)
| ~ spl0_111 ),
inference(resolution,[],[f2479,f686]) ).
fof(f4836,plain,
( line_equal(b1c1,a2c2)
| ~ spl0_111 ),
inference(resolution,[],[f2479,f129]) ).
fof(f4837,plain,
( $false
| ~ spl0_111
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f4833,f2784]) ).
fof(f4838,plain,
( ~ spl0_111
| spl0_128 ),
inference(avatar_contradiction_clause,[],[f4837]) ).
fof(f4855,plain,
( incident(c1,a2c2)
| ~ spl0_111 ),
inference(resolution,[],[f4836,f693]) ).
fof(f4862,plain,
( $false
| ~ spl0_111
| spl0_117 ),
inference(forward_subsumption_resolution,[],[f4855,f2677]) ).
fof(f4863,plain,
( ~ spl0_111
| spl0_117 ),
inference(avatar_contradiction_clause,[],[f4862]) ).
fof(f4896,plain,
! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,a2b2)
| line_equal(a1b1,a2b2)
| point_equal(X0,ab) ),
inference(resolution,[],[f990,f115]) ).
fof(f4898,plain,
! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,a2b2)
| point_equal(X0,ab) ),
inference(forward_subsumption_resolution,[],[f4896,f135]) ).
fof(f4957,plain,
( ~ incident(c1,b2c2)
| point_equal(c1,c2)
| spl0_102
| ~ spl0_117 ),
inference(resolution,[],[f2676,f3875]) ).
fof(f4964,plain,
( ~ incident(c2,b2c2)
| point_equal(c2,bc)
| ~ spl0_128 ),
inference(resolution,[],[f2783,f2113]) ).
fof(f4973,plain,
( point_equal(c2,bc)
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f4964,f100]) ).
fof(f4984,plain,
( point_equal(bc,c2)
| ~ spl0_128 ),
inference(resolution,[],[f4973,f126]) ).
fof(f4988,plain,
( spl0_157
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f4984,f2782,f3500]) ).
fof(f4994,plain,
( ! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a2c2)
| line_equal(ob,a2c2)
| point_equal(X0,b1) )
| ~ spl0_12 ),
inference(resolution,[],[f4612,f107]) ).
fof(f5102,plain,
( ~ incident(a1,a2b2)
| point_equal(a1,ab) ),
inference(resolution,[],[f4898,f90]) ).
fof(f5103,plain,
( ~ incident(b1,a2b2)
| point_equal(b1,ab) ),
inference(resolution,[],[f4898,f91]) ).
fof(f5166,plain,
( point_equal(c2,bc)
| ~ incident(c2,b2c2)
| ~ spl0_104 ),
inference(resolution,[],[f2288,f97]) ).
fof(f5177,definition,
( spl0_201
<=> line_equal(oa,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f5179,plain,
( line_equal(oa,a2c2)
| ~ spl0_201 ),
inference(avatar_component_clause,[],[f5177]) ).
fof(f5181,definition,
( spl0_202
<=> ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a2)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f5182,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,a2)
| ~ incident(X0,a2c2) )
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f5181]) ).
fof(f5183,plain,
( spl0_201
| spl0_202 ),
inference(avatar_split_clause,[],[f3900,f5181,f5177]) ).
fof(f5195,definition,
( spl0_203
<=> line_equal(ob,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f5197,plain,
( line_equal(ob,a2c2)
| ~ spl0_203 ),
inference(avatar_component_clause,[],[f5195]) ).
fof(f5199,definition,
( spl0_204
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b1)
| ~ incident(X0,a2c2) ) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f5200,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,b1)
| ~ incident(X0,a2c2) )
| ~ spl0_204 ),
inference(avatar_component_clause,[],[f5199]) ).
fof(f5201,plain,
( spl0_203
| spl0_204
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f4994,f191,f5199,f5195]) ).
fof(f5204,plain,
( incident(b2,a2c2)
| ~ spl0_203 ),
inference(resolution,[],[f5197,f707]) ).
fof(f5208,plain,
( $false
| ~ spl0_203 ),
inference(forward_subsumption_resolution,[],[f5204,f217]) ).
fof(f5209,plain,
~ spl0_203,
inference(avatar_contradiction_clause,[],[f5208]) ).
fof(f5212,plain,
( point_equal(o,b1)
| ~ incident(o,a2c2)
| ~ spl0_204 ),
inference(resolution,[],[f5200,f103]) ).
fof(f5214,definition,
( spl0_205
<=> incident(o,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f5215,plain,
( incident(o,a2c2)
| ~ spl0_205 ),
inference(avatar_component_clause,[],[f5214]) ).
fof(f5216,plain,
( ~ incident(o,a2c2)
| spl0_205 ),
inference(avatar_component_clause,[],[f5214]) ).
fof(f5218,definition,
( spl0_206
<=> point_equal(o,b1) ),
introduced(definition,[new_symbols(definition,[spl0_206])],[avatar_definition]) ).
fof(f5219,plain,
( ~ point_equal(o,b1)
| spl0_206 ),
inference(avatar_component_clause,[],[f5218]) ).
fof(f5220,plain,
( point_equal(o,b1)
| ~ spl0_206 ),
inference(avatar_component_clause,[],[f5218]) ).
fof(f5221,plain,
( ~ spl0_205
| spl0_206
| ~ spl0_204 ),
inference(avatar_split_clause,[],[f5212,f5199,f5218,f5214]) ).
fof(f5223,definition,
( spl0_207
<=> line_equal(oc,a2c2) ),
introduced(definition,[new_symbols(definition,[spl0_207])],[avatar_definition]) ).
fof(f5224,plain,
( ~ line_equal(oc,a2c2)
| spl0_207 ),
inference(avatar_component_clause,[],[f5223]) ).
fof(f5225,plain,
( line_equal(oc,a2c2)
| ~ spl0_207 ),
inference(avatar_component_clause,[],[f5223]) ).
fof(f5258,plain,
( incident(o,a2c2)
| ~ spl0_207 ),
inference(resolution,[],[f5225,f708]) ).
fof(f5266,plain,
( $false
| spl0_205
| ~ spl0_207 ),
inference(forward_subsumption_resolution,[],[f5258,f5216]) ).
fof(f5267,plain,
( spl0_205
| ~ spl0_207 ),
inference(avatar_contradiction_clause,[],[f5266]) ).
fof(f5275,plain,
( line_equal(b1c1,oc)
| ~ spl0_126 ),
inference(resolution,[],[f2745,f129]) ).
fof(f5283,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(o,X0) )
| ~ spl0_125 ),
inference(resolution,[],[f2740,f131]) ).
fof(f5284,plain,
( ! [X0] :
( ~ point_equal(X0,o)
| point_equal(X0,a2) )
| ~ spl0_125 ),
inference(resolution,[],[f2740,f127]) ).
fof(f5285,plain,
( point_equal(a2,o)
| ~ spl0_125 ),
inference(resolution,[],[f2740,f126]) ).
fof(f5292,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(o,X0) )
| ~ spl0_206 ),
inference(resolution,[],[f5220,f131]) ).
fof(f5297,plain,
( incident(a2,oc)
| ~ spl0_16
| ~ spl0_126 ),
inference(resolution,[],[f5275,f3794]) ).
fof(f5299,plain,
( incident(b1,oc)
| ~ spl0_126 ),
inference(resolution,[],[f5275,f692]) ).
fof(f5303,plain,
( $false
| spl0_18
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f5299,f230]) ).
fof(f5304,plain,
( spl0_18
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f5303]) ).
fof(f5305,plain,
( $false
| ~ spl0_16
| spl0_19
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f5297,f236]) ).
fof(f5306,plain,
( ~ spl0_16
| spl0_19
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f5305]) ).
fof(f5329,plain,
( ! [X0] :
( ~ incident(o,X0)
| incident(a2,X0) )
| ~ spl0_125 ),
inference(resolution,[],[f5285,f131]) ).
fof(f5370,plain,
( incident(o,a2b2)
| ~ spl0_125 ),
inference(resolution,[],[f5283,f92]) ).
fof(f5376,plain,
( spl0_163
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f5370,f2738,f3647]) ).
fof(f5398,plain,
( incident(o,a1b1)
| ~ spl0_206 ),
inference(resolution,[],[f5292,f91]) ).
fof(f5401,plain,
( $false
| spl0_186
| ~ spl0_206 ),
inference(forward_subsumption_resolution,[],[f5398,f4272]) ).
fof(f5402,plain,
( spl0_186
| ~ spl0_206 ),
inference(avatar_contradiction_clause,[],[f5401]) ).
fof(f5414,plain,
( point_equal(c2,o)
| ~ spl0_187 ),
inference(resolution,[],[f4276,f126]) ).
fof(f5418,plain,
( point_equal(c2,a2)
| ~ spl0_125
| ~ spl0_187 ),
inference(resolution,[],[f5414,f5284]) ).
fof(f5422,plain,
( $false
| ~ spl0_125
| spl0_129
| ~ spl0_187 ),
inference(forward_subsumption_resolution,[],[f5418,f2787]) ).
fof(f5423,plain,
( ~ spl0_125
| spl0_129
| ~ spl0_187 ),
inference(avatar_contradiction_clause,[],[f5422]) ).
fof(f5453,plain,
( incident(a2,a1b1)
| ~ spl0_125
| ~ spl0_186 ),
inference(resolution,[],[f5329,f4271]) ).
fof(f5457,plain,
( $false
| spl0_21
| ~ spl0_125
| ~ spl0_186 ),
inference(forward_subsumption_resolution,[],[f5453,f257]) ).
fof(f5458,plain,
( spl0_21
| ~ spl0_125
| ~ spl0_186 ),
inference(avatar_contradiction_clause,[],[f5457]) ).
fof(f5459,plain,
( point_equal(c2,bc)
| ~ spl0_104 ),
inference(forward_subsumption_resolution,[],[f5166,f100]) ).
fof(f5460,plain,
( ~ incident(c1,b2c2)
| spl0_102
| ~ spl0_117
| spl0_153 ),
inference(forward_subsumption_resolution,[],[f4957,f3459]) ).
fof(f5461,plain,
( ~ spl0_77
| spl0_102
| ~ spl0_117
| spl0_153 ),
inference(avatar_split_clause,[],[f5460,f3458,f2675,f2280,f1608]) ).
fof(f5470,plain,
( point_equal(c2,a1)
| ~ incident(c2,b2c2)
| ~ spl0_14
| ~ spl0_72 ),
inference(resolution,[],[f205,f1283]) ).
fof(f5483,plain,
( point_equal(c2,a1)
| ~ spl0_14
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f5470,f100]) ).
fof(f5506,plain,
( incident(o,b2c2)
| ~ spl0_137 ),
inference(resolution,[],[f2946,f708]) ).
fof(f5511,plain,
( $false
| ~ spl0_137
| spl0_142 ),
inference(forward_subsumption_resolution,[],[f5506,f3100]) ).
fof(f5512,plain,
( ~ spl0_137
| spl0_142 ),
inference(avatar_contradiction_clause,[],[f5511]) ).
fof(f5553,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(c1,X0) )
| ~ spl0_78 ),
inference(resolution,[],[f1614,f131]) ).
fof(f5559,plain,
( incident(a2,b2c2)
| ~ spl0_125
| ~ spl0_142 ),
inference(resolution,[],[f3099,f5329]) ).
fof(f5564,plain,
( $false
| ~ spl0_125
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f5559,f221]) ).
fof(f5565,plain,
( ~ spl0_125
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f5564]) ).
fof(f5566,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(o,X0) )
| ~ spl0_143 ),
inference(resolution,[],[f3104,f131]) ).
fof(f5582,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(c2,X0) )
| ~ spl0_14
| ~ spl0_72 ),
inference(resolution,[],[f5483,f131]) ).
fof(f5652,plain,
( point_equal(bc,c2)
| ~ spl0_104 ),
inference(resolution,[],[f5459,f126]) ).
fof(f5653,plain,
( $false
| ~ spl0_104
| spl0_157 ),
inference(forward_subsumption_resolution,[],[f5652,f3501]) ).
fof(f5654,plain,
( ~ spl0_104
| spl0_157 ),
inference(avatar_contradiction_clause,[],[f5653]) ).
fof(f5674,plain,
( point_equal(c1,bc)
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f2124,f1609]) ).
fof(f5677,plain,
( point_equal(bc,c1)
| ~ spl0_77 ),
inference(resolution,[],[f5674,f126]) ).
fof(f5678,plain,
( ! [X0] :
( ~ incident(c1,X0)
| incident(bc,X0) )
| ~ spl0_77 ),
inference(resolution,[],[f5677,f131]) ).
fof(f5681,plain,
( point_equal(ac,c2)
| ~ spl0_75
| spl0_102 ),
inference(forward_subsumption_resolution,[],[f3880,f1600]) ).
fof(f5683,plain,
( ! [X0] :
( ~ point_equal(X0,ac)
| point_equal(X0,c2) )
| ~ spl0_75
| spl0_102 ),
inference(resolution,[],[f5681,f127]) ).
fof(f5688,plain,
( point_equal(o,b2)
| ~ spl0_107
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f4683,f3099]) ).
fof(f5689,plain,
( ! [X0] :
( ~ incident(b2,X0)
| incident(o,X0) )
| ~ spl0_107
| ~ spl0_142 ),
inference(resolution,[],[f5688,f131]) ).
fof(f5695,plain,
( point_equal(a1,ab)
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f5102,f770]) ).
fof(f5698,plain,
( point_equal(ab,a1)
| ~ spl0_43 ),
inference(resolution,[],[f5695,f126]) ).
fof(f5699,plain,
( $false
| ~ spl0_43
| spl0_80 ),
inference(forward_subsumption_resolution,[],[f5698,f1665]) ).
fof(f5700,plain,
( ~ spl0_43
| spl0_80 ),
inference(avatar_contradiction_clause,[],[f5699]) ).
fof(f5774,plain,
( incident(c1,a1b1)
| ~ spl0_78 ),
inference(resolution,[],[f5553,f90]) ).
fof(f5777,plain,
( $false
| ~ spl0_78
| spl0_152 ),
inference(forward_subsumption_resolution,[],[f5774,f3456]) ).
fof(f5778,plain,
( ~ spl0_78
| spl0_152 ),
inference(avatar_contradiction_clause,[],[f5777]) ).
fof(f5828,plain,
( point_equal(a1,ac)
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f4678,f4355]) ).
fof(f5872,plain,
( point_equal(ac,a1)
| ~ spl0_192 ),
inference(resolution,[],[f5828,f126]) ).
fof(f5873,plain,
( $false
| spl0_76
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f5872,f1604]) ).
fof(f5874,plain,
( spl0_76
| ~ spl0_192 ),
inference(avatar_contradiction_clause,[],[f5873]) ).
fof(f5876,plain,
( ! [X0] :
( ~ point_equal(X0,ac)
| point_equal(X0,a1) )
| ~ spl0_76 ),
inference(resolution,[],[f1605,f127]) ).
fof(f5965,plain,
( incident(o,a1b1)
| ~ spl0_143 ),
inference(resolution,[],[f5566,f90]) ).
fof(f5968,plain,
( $false
| ~ spl0_143
| spl0_186 ),
inference(forward_subsumption_resolution,[],[f5965,f4272]) ).
fof(f5969,plain,
( ~ spl0_143
| spl0_186 ),
inference(avatar_contradiction_clause,[],[f5968]) ).
fof(f6026,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(b1,X0) )
| ~ spl0_82 ),
inference(resolution,[],[f1675,f131]) ).
fof(f6068,plain,
( incident(c2,oa)
| ~ spl0_14
| ~ spl0_72 ),
inference(resolution,[],[f5582,f105]) ).
fof(f6106,plain,
( point_equal(bc,b2)
| ~ spl0_175 ),
inference(resolution,[],[f4045,f126]) ).
fof(f6107,plain,
( ! [X0] :
( ~ incident(b2,X0)
| incident(bc,X0) )
| ~ spl0_175 ),
inference(resolution,[],[f6106,f131]) ).
fof(f6120,plain,
( incident(o,a2b2)
| ~ spl0_107
| ~ spl0_142 ),
inference(resolution,[],[f5689,f93]) ).
fof(f6124,plain,
( $false
| ~ spl0_107
| ~ spl0_142
| spl0_163 ),
inference(forward_subsumption_resolution,[],[f6120,f3649]) ).
fof(f6125,plain,
( ~ spl0_107
| ~ spl0_142
| spl0_163 ),
inference(avatar_contradiction_clause,[],[f6124]) ).
fof(f6138,plain,
( incident(b1,b2c2)
| ~ spl0_105 ),
inference(resolution,[],[f2379,f706]) ).
fof(f6144,plain,
( $false
| spl0_81
| ~ spl0_105 ),
inference(forward_subsumption_resolution,[],[f6138,f1671]) ).
fof(f6145,plain,
( spl0_81
| ~ spl0_105 ),
inference(avatar_contradiction_clause,[],[f6144]) ).
fof(f6229,plain,
( incident(b1,a1c1)
| ~ spl0_82 ),
inference(resolution,[],[f6026,f94]) ).
fof(f6235,plain,
( $false
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f6229,f200]) ).
fof(f6236,plain,
~ spl0_82,
inference(avatar_contradiction_clause,[],[f6235]) ).
fof(f6242,plain,
( incident(bc,a2b2)
| ~ spl0_11
| ~ spl0_77 ),
inference(resolution,[],[f5678,f188]) ).
fof(f6247,plain,
( $false
| ~ spl0_11
| spl0_32
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f6242,f468]) ).
fof(f6248,plain,
( ~ spl0_11
| spl0_32
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f6247]) ).
fof(f6319,plain,
! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a2b2)
| line_equal(ob,a2b2)
| point_equal(X0,b2) ),
inference(resolution,[],[f993,f108]) ).
fof(f6324,plain,
( ~ incident(b2,b2c2)
| point_equal(b2,bc)
| ~ spl0_174 ),
inference(resolution,[],[f4040,f2113]) ).
fof(f6356,plain,
( incident(bc,a2b2)
| ~ spl0_175 ),
inference(resolution,[],[f6107,f93]) ).
fof(f6491,plain,
( $false
| spl0_32
| ~ spl0_175 ),
inference(forward_subsumption_resolution,[],[f6356,f468]) ).
fof(f6492,plain,
( spl0_32
| ~ spl0_175 ),
inference(avatar_contradiction_clause,[],[f6491]) ).
fof(f6493,plain,
( point_equal(b2,bc)
| ~ spl0_174 ),
inference(forward_subsumption_resolution,[],[f6324,f101]) ).
fof(f6497,plain,
( $false
| ~ spl0_174
| spl0_175 ),
inference(forward_subsumption_resolution,[],[f6493,f4044]) ).
fof(f6498,plain,
( ~ spl0_174
| spl0_175 ),
inference(avatar_contradiction_clause,[],[f6497]) ).
fof(f6542,plain,
( point_equal(o,c1)
| ~ incident(o,a2b2)
| ~ spl0_166 ),
inference(resolution,[],[f3661,f104]) ).
fof(f6543,plain,
( ~ incident(o,a2b2)
| spl0_164
| ~ spl0_166 ),
inference(forward_subsumption_resolution,[],[f6542,f3652]) ).
fof(f6544,plain,
( ~ spl0_163
| spl0_164
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f6543,f3660,f3651,f3647]) ).
fof(f6545,plain,
( ! [X0] :
( ~ incident(c1,X0)
| incident(o,X0) )
| ~ spl0_164 ),
inference(resolution,[],[f3653,f131]) ).
fof(f6552,plain,
( incident(o,b1c1)
| ~ spl0_164 ),
inference(resolution,[],[f6545,f98]) ).
fof(f6555,plain,
( $false
| spl0_124
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f6552,f2736]) ).
fof(f6556,plain,
( spl0_124
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f6555]) ).
fof(f6565,plain,
( point_equal(o,a2)
| ~ incident(o,a2c2)
| ~ spl0_163
| ~ spl0_177 ),
inference(resolution,[],[f3648,f4053]) ).
fof(f6618,plain,
( point_equal(c2,a2)
| ~ incident(c2,a2c2)
| ~ spl0_14
| ~ spl0_72
| ~ spl0_202 ),
inference(resolution,[],[f5182,f6068]) ).
fof(f6620,plain,
( ~ incident(c2,a2c2)
| ~ spl0_14
| ~ spl0_72
| spl0_129
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f6618,f2787]) ).
fof(f6623,plain,
( $false
| ~ spl0_14
| ~ spl0_72
| spl0_129
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f6620,f97]) ).
fof(f6624,plain,
( ~ spl0_14
| ~ spl0_72
| spl0_129
| ~ spl0_202 ),
inference(avatar_contradiction_clause,[],[f6623]) ).
fof(f6632,plain,
( incident(o,a2c2)
| ~ spl0_201 ),
inference(resolution,[],[f5179,f702]) ).
fof(f6635,plain,
( $false
| ~ spl0_201
| spl0_205 ),
inference(forward_subsumption_resolution,[],[f6632,f5216]) ).
fof(f6636,plain,
( ~ spl0_201
| spl0_205 ),
inference(avatar_contradiction_clause,[],[f6635]) ).
fof(f6639,plain,
( ~ incident(o,a2c2)
| spl0_125
| ~ spl0_163
| ~ spl0_177 ),
inference(forward_subsumption_resolution,[],[f6565,f2739]) ).
fof(f6640,plain,
( ~ spl0_205
| spl0_125
| ~ spl0_163
| ~ spl0_177 ),
inference(avatar_split_clause,[],[f6639,f4052,f3647,f2738,f5214]) ).
fof(f6652,plain,
( point_equal(a2,o)
| ~ spl0_125 ),
inference(resolution,[],[f2740,f126]) ).
fof(f6660,plain,
( ! [X0] :
( ~ incident(o,X0)
| incident(a2,X0) )
| ~ spl0_125 ),
inference(resolution,[],[f6652,f131]) ).
fof(f6761,plain,
( incident(a2,oc)
| ~ spl0_125 ),
inference(resolution,[],[f6660,f104]) ).
fof(f6762,plain,
( $false
| spl0_19
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f6761,f236]) ).
fof(f6763,plain,
( spl0_19
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f6762]) ).
fof(f6780,plain,
( point_equal(c1,a1)
| ~ incident(c1,a1c1)
| ~ spl0_181 ),
inference(resolution,[],[f4116,f109]) ).
fof(f6784,plain,
( ~ incident(c1,a1c1)
| spl0_78
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f6780,f1613]) ).
fof(f6785,plain,
( $false
| spl0_78
| ~ spl0_181 ),
inference(forward_subsumption_resolution,[],[f6784,f95]) ).
fof(f6786,plain,
( spl0_78
| ~ spl0_181 ),
inference(avatar_contradiction_clause,[],[f6785]) ).
fof(f6792,plain,
( line_equal(oc,a1c1)
| ~ spl0_180 ),
inference(resolution,[],[f4113,f129]) ).
fof(f6793,plain,
( incident(o,a1c1)
| ~ spl0_180 ),
inference(resolution,[],[f6792,f708]) ).
fof(f6802,plain,
( ~ incident(o,a2c2)
| point_equal(o,ac)
| ~ spl0_180 ),
inference(resolution,[],[f6793,f4213]) ).
fof(f6807,plain,
( point_equal(o,ac)
| ~ spl0_180
| ~ spl0_205 ),
inference(forward_subsumption_resolution,[],[f6802,f5215]) ).
fof(f6808,plain,
( point_equal(o,a1)
| ~ spl0_76
| ~ spl0_180
| ~ spl0_205 ),
inference(resolution,[],[f6807,f5876]) ).
fof(f6809,plain,
( point_equal(o,c2)
| ~ spl0_75
| spl0_102
| ~ spl0_180
| ~ spl0_205 ),
inference(resolution,[],[f6807,f5683]) ).
fof(f6813,plain,
( $false
| ~ spl0_75
| spl0_102
| ~ spl0_180
| spl0_187
| ~ spl0_205 ),
inference(forward_subsumption_resolution,[],[f6809,f4275]) ).
fof(f6814,plain,
( ~ spl0_75
| spl0_102
| ~ spl0_180
| spl0_187
| ~ spl0_205 ),
inference(avatar_contradiction_clause,[],[f6813]) ).
fof(f6815,plain,
( $false
| ~ spl0_76
| spl0_143
| ~ spl0_180
| ~ spl0_205 ),
inference(forward_subsumption_resolution,[],[f6808,f3103]) ).
fof(f6816,plain,
( ~ spl0_76
| spl0_143
| ~ spl0_180
| ~ spl0_205 ),
inference(avatar_contradiction_clause,[],[f6815]) ).
fof(f6819,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(o,X0) )
| ~ spl0_143 ),
inference(resolution,[],[f3104,f131]) ).
fof(f6848,plain,
( incident(o,b2c2)
| ~ spl0_13
| ~ spl0_143 ),
inference(resolution,[],[f6819,f196]) ).
fof(f6854,plain,
( $false
| ~ spl0_13
| spl0_142
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f6848,f3100]) ).
fof(f6855,plain,
( ~ spl0_13
| spl0_142
| ~ spl0_143 ),
inference(avatar_contradiction_clause,[],[f6854]) ).
fof(f6861,plain,
( ~ incident(a2,a2b2)
| point_equal(a2,ab)
| ~ spl0_21 ),
inference(resolution,[],[f256,f4898]) ).
fof(f6863,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,a2b2)
| line_equal(a1b1,a2b2)
| point_equal(X0,a2) )
| ~ spl0_21 ),
inference(resolution,[],[f256,f992]) ).
fof(f6870,plain,
( ! [X0] :
( ~ incident(X0,a1b1)
| ~ incident(X0,a2b2)
| point_equal(X0,a2) )
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f6863,f135]) ).
fof(f6871,plain,
( point_equal(a2,ab)
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f6861,f92]) ).
fof(f6881,plain,
( point_equal(b1,a2)
| ~ incident(b1,a2c2)
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f774,f4053]) ).
fof(f6887,plain,
( point_equal(b1,a2)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(forward_subsumption_resolution,[],[f6881,f192]) ).
fof(f6888,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(o,X0) )
| ~ spl0_206 ),
inference(resolution,[],[f5220,f131]) ).
fof(f6893,plain,
( point_equal(ab,a2)
| ~ spl0_21 ),
inference(resolution,[],[f6871,f126]) ).
fof(f6896,plain,
( point_equal(a2,b1)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f6887,f126]) ).
fof(f6900,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(ab,X0) )
| ~ spl0_21 ),
inference(resolution,[],[f6893,f131]) ).
fof(f6901,plain,
( ! [X0] :
( ~ point_equal(X0,ab)
| point_equal(X0,a2) )
| ~ spl0_21 ),
inference(resolution,[],[f6893,f127]) ).
fof(f6903,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(a2,X0) )
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f6896,f131]) ).
fof(f6904,plain,
( ! [X0] :
( ~ point_equal(X0,a2)
| point_equal(X0,b1) )
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f6896,f127]) ).
fof(f6937,plain,
( point_equal(b1,ab)
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f5103,f774]) ).
fof(f6940,plain,
( point_equal(ab,b1)
| ~ spl0_44 ),
inference(resolution,[],[f6937,f126]) ).
fof(f6942,plain,
( ! [X0] :
( ~ point_equal(X0,ab)
| point_equal(X0,b1) )
| ~ spl0_44 ),
inference(resolution,[],[f6940,f127]) ).
fof(f6962,plain,
( incident(o,b1c1)
| ~ spl0_206 ),
inference(resolution,[],[f6888,f99]) ).
fof(f6965,plain,
( $false
| spl0_124
| ~ spl0_206 ),
inference(forward_subsumption_resolution,[],[f6962,f2736]) ).
fof(f6966,plain,
( spl0_124
| ~ spl0_206 ),
inference(avatar_contradiction_clause,[],[f6965]) ).
fof(f7024,plain,
( incident(ab,a2c2)
| ~ spl0_21 ),
inference(resolution,[],[f6900,f96]) ).
fof(f7026,plain,
( incident(ab,b1c1)
| ~ spl0_16
| ~ spl0_21 ),
inference(resolution,[],[f6900,f213]) ).
fof(f7028,plain,
( incident(ab,oa)
| ~ spl0_21 ),
inference(resolution,[],[f6900,f106]) ).
fof(f7029,plain,
( $false
| ~ spl0_16
| ~ spl0_21
| spl0_172 ),
inference(forward_subsumption_resolution,[],[f7026,f4032]) ).
fof(f7030,plain,
( ~ spl0_16
| ~ spl0_21
| spl0_172 ),
inference(avatar_contradiction_clause,[],[f7029]) ).
fof(f7031,plain,
( $false
| ~ spl0_21
| spl0_148 ),
inference(forward_subsumption_resolution,[],[f7024,f3421]) ).
fof(f7032,plain,
( ~ spl0_21
| spl0_148 ),
inference(avatar_contradiction_clause,[],[f7031]) ).
fof(f7038,plain,
( ~ incident(bc,a2c2)
| ~ incident(ac,a2c2)
| ~ line_equal(a2c2,a2c2)
| ~ spl0_148 ),
inference(resolution,[],[f3420,f145]) ).
fof(f7066,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,a2b2)
| line_equal(oa,a2b2)
| point_equal(X0,ab) )
| ~ spl0_21 ),
inference(resolution,[],[f7028,f990]) ).
fof(f7083,plain,
( incident(a2,ob)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f6903,f107]) ).
fof(f7087,plain,
( ! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a2b2)
| line_equal(ob,a2b2)
| point_equal(X0,a2) )
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(resolution,[],[f7083,f992]) ).
fof(f7155,plain,
( ~ incident(o,a2b2)
| point_equal(o,a2)
| ~ spl0_21
| ~ spl0_186 ),
inference(resolution,[],[f6870,f4271]) ).
fof(f7210,definition,
( spl0_211
<=> line_equal(oa,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_211])],[avatar_definition]) ).
fof(f7211,plain,
( ~ line_equal(oa,a2b2)
| spl0_211 ),
inference(avatar_component_clause,[],[f7210]) ).
fof(f7212,plain,
( line_equal(oa,a2b2)
| ~ spl0_211 ),
inference(avatar_component_clause,[],[f7210]) ).
fof(f7214,definition,
( spl0_212
<=> ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,ab)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f7215,plain,
( ! [X0] :
( ~ incident(X0,oa)
| point_equal(X0,ab)
| ~ incident(X0,a2b2) )
| ~ spl0_212 ),
inference(avatar_component_clause,[],[f7214]) ).
fof(f7216,plain,
( spl0_211
| spl0_212
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f7066,f255,f7214,f7210]) ).
fof(f7220,plain,
( incident(a1,a2b2)
| ~ spl0_211 ),
inference(resolution,[],[f7212,f703]) ).
fof(f7221,plain,
( incident(o,a2b2)
| ~ spl0_211 ),
inference(resolution,[],[f7212,f702]) ).
fof(f7224,plain,
( $false
| spl0_163
| ~ spl0_211 ),
inference(forward_subsumption_resolution,[],[f7221,f3649]) ).
fof(f7225,plain,
( spl0_163
| ~ spl0_211 ),
inference(avatar_contradiction_clause,[],[f7224]) ).
fof(f7226,plain,
( $false
| spl0_43
| ~ spl0_211 ),
inference(forward_subsumption_resolution,[],[f7220,f771]) ).
fof(f7227,plain,
( spl0_43
| ~ spl0_211 ),
inference(avatar_contradiction_clause,[],[f7226]) ).
fof(f7232,plain,
( point_equal(o,ab)
| ~ incident(o,a2b2)
| ~ spl0_212 ),
inference(resolution,[],[f7215,f102]) ).
fof(f7233,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b2c2)
| point_equal(X0,c2) )
| spl0_137 ),
inference(forward_subsumption_resolution,[],[f3870,f2945]) ).
fof(f7234,plain,
( ~ incident(c1,b2c2)
| point_equal(c1,c2)
| spl0_137 ),
inference(resolution,[],[f7233,f109]) ).
fof(f7242,definition,
( spl0_213
<=> line_equal(ob,a2b2) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f7243,plain,
( ~ line_equal(ob,a2b2)
| spl0_213 ),
inference(avatar_component_clause,[],[f7242]) ).
fof(f7244,plain,
( line_equal(ob,a2b2)
| ~ spl0_213 ),
inference(avatar_component_clause,[],[f7242]) ).
fof(f7246,definition,
( spl0_214
<=> ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,a2)
| ~ incident(X0,a2b2) ) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f7247,plain,
( ! [X0] :
( ~ incident(X0,ob)
| point_equal(X0,a2)
| ~ incident(X0,a2b2) )
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f7246]) ).
fof(f7248,plain,
( spl0_213
| spl0_214
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177 ),
inference(avatar_split_clause,[],[f7087,f4052,f773,f191,f7246,f7242]) ).
fof(f7249,plain,
( incident(o,a2b2)
| ~ spl0_213 ),
inference(resolution,[],[f7244,f705]) ).
fof(f7256,plain,
( $false
| spl0_163
| ~ spl0_213 ),
inference(forward_subsumption_resolution,[],[f7249,f3649]) ).
fof(f7257,plain,
( spl0_163
| ~ spl0_213 ),
inference(avatar_contradiction_clause,[],[f7256]) ).
fof(f7261,plain,
( point_equal(b2,a2)
| ~ incident(b2,a2b2)
| ~ spl0_214 ),
inference(resolution,[],[f7247,f108]) ).
fof(f7263,plain,
( point_equal(b2,a2)
| ~ spl0_214 ),
inference(forward_subsumption_resolution,[],[f7261,f93]) ).
fof(f7264,plain,
( point_equal(b2,b1)
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177
| ~ spl0_214 ),
inference(resolution,[],[f7263,f6904]) ).
fof(f7269,plain,
( $false
| ~ spl0_12
| ~ spl0_44
| ~ spl0_177
| ~ spl0_214 ),
inference(forward_subsumption_resolution,[],[f7264,f139]) ).
fof(f7270,plain,
( ~ spl0_12
| ~ spl0_44
| ~ spl0_177
| ~ spl0_214 ),
inference(avatar_contradiction_clause,[],[f7269]) ).
fof(f7271,plain,
( ~ incident(o,a2b2)
| ~ spl0_21
| spl0_125
| ~ spl0_186 ),
inference(forward_subsumption_resolution,[],[f7155,f2739]) ).
fof(f7272,plain,
( ~ spl0_163
| ~ spl0_21
| spl0_125
| ~ spl0_186 ),
inference(avatar_split_clause,[],[f7271,f4270,f2738,f255,f3647]) ).
fof(f7281,plain,
( incident(b1,a2b2)
| ~ spl0_213 ),
inference(resolution,[],[f7244,f706]) ).
fof(f7296,plain,
( point_equal(o,ab)
| ~ spl0_163
| ~ spl0_212 ),
inference(forward_subsumption_resolution,[],[f7232,f3648]) ).
fof(f7297,plain,
( point_equal(o,b1)
| ~ spl0_44
| ~ spl0_163
| ~ spl0_212 ),
inference(resolution,[],[f7296,f6942]) ).
fof(f7298,plain,
( point_equal(o,a2)
| ~ spl0_21
| ~ spl0_163
| ~ spl0_212 ),
inference(resolution,[],[f7296,f6901]) ).
fof(f7302,plain,
( $false
| ~ spl0_21
| spl0_125
| ~ spl0_163
| ~ spl0_212 ),
inference(forward_subsumption_resolution,[],[f7298,f2739]) ).
fof(f7303,plain,
( ~ spl0_21
| spl0_125
| ~ spl0_163
| ~ spl0_212 ),
inference(avatar_contradiction_clause,[],[f7302]) ).
fof(f7304,plain,
( $false
| ~ spl0_44
| ~ spl0_163
| spl0_206
| ~ spl0_212 ),
inference(forward_subsumption_resolution,[],[f7297,f5219]) ).
fof(f7305,plain,
( ~ spl0_44
| ~ spl0_163
| spl0_206
| ~ spl0_212 ),
inference(avatar_contradiction_clause,[],[f7304]) ).
fof(f7330,plain,
( incident(c2,b1c1)
| ~ spl0_126 ),
inference(resolution,[],[f2745,f710]) ).
fof(f7333,plain,
( $false
| ~ spl0_126
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f7330,f2784]) ).
fof(f7334,plain,
( ~ spl0_126
| spl0_128 ),
inference(avatar_contradiction_clause,[],[f7333]) ).
fof(f7337,plain,
( ~ incident(bc,a2c2)
| ~ incident(ac,a2c2)
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f7038,f128]) ).
fof(f7338,plain,
( ~ incident(bc,a2c2)
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f7337,f114]) ).
fof(f7339,plain,
( ~ spl0_115
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f7338,f3419,f2666]) ).
fof(f7404,plain,
( ! [X0] :
( ~ incident(a2,X0)
| incident(o,X0) )
| ~ spl0_125 ),
inference(resolution,[],[f2740,f131]) ).
fof(f7431,plain,
( point_equal(c1,o)
| ~ spl0_164 ),
inference(resolution,[],[f3653,f126]) ).
fof(f7432,plain,
( ! [X0] :
( ~ incident(c2,X0)
| incident(bc,X0) )
| ~ spl0_157 ),
inference(resolution,[],[f3502,f131]) ).
fof(f7435,plain,
( ! [X0] :
( ~ incident(o,X0)
| incident(c1,X0) )
| ~ spl0_164 ),
inference(resolution,[],[f7431,f131]) ).
fof(f7436,plain,
( ! [X0] :
( ~ point_equal(X0,c1)
| point_equal(X0,o) )
| ~ spl0_164 ),
inference(resolution,[],[f7431,f127]) ).
fof(f7438,plain,
( $false
| spl0_44
| ~ spl0_213 ),
inference(forward_subsumption_resolution,[],[f7281,f775]) ).
fof(f7439,plain,
( spl0_44
| ~ spl0_213 ),
inference(avatar_contradiction_clause,[],[f7438]) ).
fof(f7453,plain,
( incident(o,a2c2)
| ~ spl0_125 ),
inference(resolution,[],[f7404,f96]) ).
fof(f7457,plain,
( $false
| ~ spl0_125
| spl0_205 ),
inference(forward_subsumption_resolution,[],[f7453,f5216]) ).
fof(f7458,plain,
( ~ spl0_125
| spl0_205 ),
inference(avatar_contradiction_clause,[],[f7457]) ).
fof(f7489,definition,
( spl0_216
<=> incident(bc,oc) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f7490,plain,
( incident(bc,oc)
| ~ spl0_216 ),
inference(avatar_component_clause,[],[f7489]) ).
fof(f7555,plain,
( incident(bc,a2c2)
| ~ spl0_157 ),
inference(resolution,[],[f7432,f97]) ).
fof(f7557,plain,
( incident(bc,oc)
| ~ spl0_157 ),
inference(resolution,[],[f7432,f110]) ).
fof(f7558,plain,
( $false
| spl0_115
| ~ spl0_157 ),
inference(forward_subsumption_resolution,[],[f7555,f2668]) ).
fof(f7559,plain,
( spl0_115
| ~ spl0_157 ),
inference(avatar_contradiction_clause,[],[f7558]) ).
fof(f7568,plain,
( spl0_216
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f7557,f3500,f7489]) ).
fof(f7586,plain,
( incident(c1,oa)
| ~ spl0_164 ),
inference(resolution,[],[f7435,f102]) ).
fof(f7618,plain,
( incident(c1,a1b1)
| ~ spl0_164
| ~ spl0_186 ),
inference(resolution,[],[f4271,f7435]) ).
fof(f7623,plain,
( $false
| spl0_152
| ~ spl0_164
| ~ spl0_186 ),
inference(forward_subsumption_resolution,[],[f7618,f3456]) ).
fof(f7624,plain,
( spl0_152
| ~ spl0_164
| ~ spl0_186 ),
inference(avatar_contradiction_clause,[],[f7623]) ).
fof(f7668,plain,
( point_equal(b2,c1)
| ~ incident(b2,a2b2)
| ~ spl0_15
| ~ spl0_162 ),
inference(resolution,[],[f3625,f209]) ).
fof(f7670,plain,
( point_equal(b2,c1)
| ~ spl0_15
| ~ spl0_162 ),
inference(forward_subsumption_resolution,[],[f7668,f93]) ).
fof(f7671,plain,
( point_equal(b2,o)
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164 ),
inference(resolution,[],[f7670,f7436]) ).
fof(f7672,plain,
( ! [X0] :
( ~ incident(c1,X0)
| incident(b2,X0) )
| ~ spl0_15
| ~ spl0_162 ),
inference(resolution,[],[f7670,f131]) ).
fof(f7680,plain,
( ! [X0] :
( ~ point_equal(X0,b2)
| point_equal(X0,o) )
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164 ),
inference(resolution,[],[f7671,f127]) ).
fof(f7686,plain,
( incident(b2,b1c1)
| ~ spl0_15
| ~ spl0_162 ),
inference(resolution,[],[f7672,f98]) ).
fof(f7688,plain,
( incident(b2,oa)
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164 ),
inference(resolution,[],[f7672,f7586]) ).
fof(f7693,plain,
( $false
| ~ spl0_15
| ~ spl0_162
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f7686,f4041]) ).
fof(f7694,plain,
( ~ spl0_15
| ~ spl0_162
| spl0_174 ),
inference(avatar_contradiction_clause,[],[f7693]) ).
fof(f7695,plain,
( ~ incident(c1,b2c2)
| spl0_137
| spl0_153 ),
inference(forward_subsumption_resolution,[],[f7234,f3459]) ).
fof(f7697,plain,
( ~ spl0_77
| spl0_137
| spl0_153 ),
inference(avatar_split_clause,[],[f7695,f3458,f2944,f1608]) ).
fof(f7706,plain,
( ~ incident(bc,b2c2)
| point_equal(bc,b2)
| ~ spl0_32
| spl0_97 ),
inference(resolution,[],[f467,f2217]) ).
fof(f7716,plain,
( point_equal(bc,b2)
| ~ spl0_32
| spl0_97 ),
inference(forward_subsumption_resolution,[],[f7706,f112]) ).
fof(f7740,plain,
( incident(c1,b2c2)
| ~ spl0_142
| ~ spl0_164 ),
inference(resolution,[],[f3099,f7435]) ).
fof(f7745,plain,
( ! [X0] :
( ~ incident(b2,X0)
| incident(bc,X0) )
| ~ spl0_32
| spl0_97 ),
inference(resolution,[],[f7716,f131]) ).
fof(f7776,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b1c1)
| line_equal(oc,b1c1)
| point_equal(X0,bc) )
| ~ spl0_216 ),
inference(resolution,[],[f994,f7490]) ).
fof(f7778,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,b1c1)
| point_equal(X0,bc) )
| spl0_126
| ~ spl0_216 ),
inference(forward_subsumption_resolution,[],[f7776,f2744]) ).
fof(f7808,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,a2b2)
| line_equal(oa,a2b2)
| point_equal(X0,b2) )
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164 ),
inference(resolution,[],[f7688,f993]) ).
fof(f7815,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,a2b2)
| point_equal(X0,b2) )
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(forward_subsumption_resolution,[],[f7808,f7211]) ).
fof(f7852,plain,
( incident(bc,a1c1)
| ~ spl0_15
| ~ spl0_32
| spl0_97 ),
inference(resolution,[],[f7745,f209]) ).
fof(f7858,plain,
( spl0_156
| ~ spl0_15
| ~ spl0_32
| spl0_97 ),
inference(avatar_split_clause,[],[f7852,f2188,f466,f208,f3496]) ).
fof(f8023,plain,
( ~ incident(c1,b1c1)
| point_equal(c1,bc)
| spl0_126
| ~ spl0_216 ),
inference(resolution,[],[f7778,f109]) ).
fof(f8066,plain,
( ~ incident(a2,a2b2)
| point_equal(a2,b2)
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(resolution,[],[f7815,f106]) ).
fof(f8069,plain,
( point_equal(a2,b2)
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(forward_subsumption_resolution,[],[f8066,f92]) ).
fof(f8070,plain,
( point_equal(a2,o)
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(resolution,[],[f8069,f7680]) ).
fof(f8081,plain,
( point_equal(o,a2)
| ~ spl0_15
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(resolution,[],[f8070,f126]) ).
fof(f8082,plain,
( $false
| ~ spl0_15
| spl0_125
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(forward_subsumption_resolution,[],[f8081,f2739]) ).
fof(f8083,plain,
( ~ spl0_15
| spl0_125
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(avatar_contradiction_clause,[],[f8082]) ).
fof(f8094,plain,
( point_equal(c1,bc)
| spl0_126
| ~ spl0_216 ),
inference(forward_subsumption_resolution,[],[f8023,f98]) ).
fof(f8125,plain,
( ! [X0] :
( ~ incident(a1,X0)
| incident(ab,X0) )
| ~ spl0_80 ),
inference(resolution,[],[f1666,f131]) ).
fof(f8126,plain,
( ! [X0] :
( ~ point_equal(X0,ab)
| point_equal(X0,a1) )
| ~ spl0_80 ),
inference(resolution,[],[f1666,f127]) ).
fof(f8127,plain,
( point_equal(a1,ab)
| ~ spl0_80 ),
inference(resolution,[],[f1666,f126]) ).
fof(f8148,plain,
( ! [X0] :
( ~ incident(ab,X0)
| incident(a1,X0) )
| ~ spl0_80 ),
inference(resolution,[],[f8127,f131]) ).
fof(f8185,plain,
( ~ incident(bc,a1c1)
| ~ incident(ac,a1c1)
| ~ line_equal(a1c1,a1c1)
| ~ spl0_158 ),
inference(resolution,[],[f3506,f145]) ).
fof(f8196,plain,
( ! [X0] :
( ~ incident(bc,X0)
| incident(c1,X0) )
| spl0_126
| ~ spl0_216 ),
inference(resolution,[],[f8094,f131]) ).
fof(f8203,plain,
( $false
| spl0_77
| ~ spl0_142
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f7740,f1610]) ).
fof(f8204,plain,
( spl0_77
| ~ spl0_142
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f8203]) ).
fof(f8235,plain,
( incident(ab,oa)
| ~ spl0_80 ),
inference(resolution,[],[f8125,f105]) ).
fof(f8237,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,a2b2)
| line_equal(oa,a2b2)
| point_equal(X0,ab) )
| ~ spl0_80 ),
inference(resolution,[],[f8235,f990]) ).
fof(f8243,plain,
( ! [X0] :
( ~ incident(X0,oa)
| ~ incident(X0,a2b2)
| point_equal(X0,ab) )
| ~ spl0_80
| spl0_211 ),
inference(forward_subsumption_resolution,[],[f8237,f7211]) ).
fof(f8294,plain,
( incident(c1,b2c2)
| spl0_126
| ~ spl0_216 ),
inference(resolution,[],[f8196,f112]) ).
fof(f8297,plain,
( $false
| spl0_77
| spl0_126
| ~ spl0_216 ),
inference(forward_subsumption_resolution,[],[f8294,f1610]) ).
fof(f8298,plain,
( spl0_77
| spl0_126
| ~ spl0_216 ),
inference(avatar_contradiction_clause,[],[f8297]) ).
fof(f8313,plain,
( spl0_212
| ~ spl0_80
| spl0_211 ),
inference(avatar_split_clause,[],[f8243,f7210,f1664,f7214]) ).
fof(f8396,plain,
( ! [X0] :
( ~ incident(X0,oc)
| ~ incident(X0,a2c2)
| point_equal(X0,c2) )
| spl0_207 ),
inference(forward_subsumption_resolution,[],[f4124,f5224]) ).
fof(f8400,plain,
( ! [X0] :
( ~ incident(X0,ob)
| ~ incident(X0,a2b2)
| point_equal(X0,b2) )
| spl0_213 ),
inference(forward_subsumption_resolution,[],[f6319,f7243]) ).
fof(f8404,plain,
( ~ incident(o,a2b2)
| point_equal(o,b2)
| spl0_213 ),
inference(resolution,[],[f8400,f103]) ).
fof(f8405,plain,
( point_equal(o,b2)
| ~ spl0_163
| spl0_213 ),
inference(forward_subsumption_resolution,[],[f8404,f3648]) ).
fof(f8407,plain,
( ! [X0] :
( ~ incident(b2,X0)
| incident(o,X0) )
| ~ spl0_163
| spl0_213 ),
inference(resolution,[],[f8405,f131]) ).
fof(f8421,plain,
( incident(o,b2c2)
| ~ spl0_163
| spl0_213 ),
inference(resolution,[],[f8407,f101]) ).
fof(f8426,plain,
( $false
| spl0_142
| ~ spl0_163
| spl0_213 ),
inference(forward_subsumption_resolution,[],[f8421,f3100]) ).
fof(f8427,plain,
( spl0_142
| ~ spl0_163
| spl0_213 ),
inference(avatar_contradiction_clause,[],[f8426]) ).
fof(f8429,plain,
( ~ incident(bc,a1c1)
| ~ incident(ac,a1c1)
| ~ spl0_158 ),
inference(forward_subsumption_resolution,[],[f8185,f128]) ).
fof(f8430,plain,
( ~ incident(bc,a1c1)
| ~ spl0_158 ),
inference(forward_subsumption_resolution,[],[f8429,f113]) ).
fof(f8431,plain,
( ~ spl0_156
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f8430,f3505,f3496]) ).
fof(f8432,plain,
( ~ incident(b1,a2c2)
| point_equal(b1,c2)
| ~ spl0_18
| spl0_207 ),
inference(resolution,[],[f229,f8396]) ).
fof(f8438,plain,
( point_equal(b1,c2)
| ~ spl0_12
| ~ spl0_18
| spl0_207 ),
inference(forward_subsumption_resolution,[],[f8432,f192]) ).
fof(f8506,plain,
( point_equal(c2,b1)
| ~ spl0_12
| ~ spl0_18
| spl0_207 ),
inference(resolution,[],[f8438,f126]) ).
fof(f8527,plain,
( incident(a1,b1c1)
| ~ spl0_80
| ~ spl0_172 ),
inference(resolution,[],[f4031,f8148]) ).
fof(f8536,plain,
( $false
| ~ spl0_80
| ~ spl0_172 ),
inference(forward_subsumption_resolution,[],[f8527,f219]) ).
fof(f8537,plain,
( ~ spl0_80
| ~ spl0_172 ),
inference(avatar_contradiction_clause,[],[f8536]) ).
fof(f8582,plain,
( ! [X0] :
( ~ incident(b1,X0)
| incident(c2,X0) )
| ~ spl0_12
| ~ spl0_18
| spl0_207 ),
inference(resolution,[],[f8506,f131]) ).
fof(f8711,plain,
( incident(c2,a1b1)
| ~ spl0_12
| ~ spl0_18
| spl0_207 ),
inference(resolution,[],[f8582,f91]) ).
fof(f8714,plain,
( $false
| ~ spl0_12
| spl0_14
| ~ spl0_18
| spl0_207 ),
inference(forward_subsumption_resolution,[],[f8711,f206]) ).
fof(f8715,plain,
( ~ spl0_12
| spl0_14
| ~ spl0_18
| spl0_207 ),
inference(avatar_contradiction_clause,[],[f8714]) ).
fof(f8725,plain,
( ! [X0] :
( ~ incident(c2,X0)
| incident(o,X0) )
| ~ spl0_187 ),
inference(resolution,[],[f4276,f131]) ).
fof(f8739,plain,
( incident(o,b2c2)
| ~ spl0_187 ),
inference(resolution,[],[f8725,f100]) ).
fof(f8744,plain,
( $false
| spl0_142
| ~ spl0_187 ),
inference(forward_subsumption_resolution,[],[f8739,f3100]) ).
fof(f8745,plain,
( spl0_142
| ~ spl0_187 ),
inference(avatar_contradiction_clause,[],[f8744]) ).
fof(f8787,plain,
( point_equal(a2,ab)
| ~ incident(a2,a2b2)
| ~ spl0_212 ),
inference(resolution,[],[f7215,f106]) ).
fof(f8789,plain,
( point_equal(a2,ab)
| ~ spl0_212 ),
inference(forward_subsumption_resolution,[],[f8787,f92]) ).
fof(f8791,plain,
( point_equal(a2,a1)
| ~ spl0_80
| ~ spl0_212 ),
inference(resolution,[],[f8789,f8126]) ).
fof(f8795,plain,
( $false
| ~ spl0_80
| ~ spl0_212 ),
inference(forward_subsumption_resolution,[],[f8791,f140]) ).
fof(f8796,plain,
( ~ spl0_80
| ~ spl0_212 ),
inference(avatar_contradiction_clause,[],[f8795]) ).
cnf(s110,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f198]) ).
cnf(s121,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f215]) ).
cnf(s169,plain,
( spl0_13
| spl0_15 ),
inference(sat_conversion,[],[f250]) ).
cnf(s174,plain,
( spl0_12
| spl0_14 ),
inference(sat_conversion,[],[f252]) ).
cnf(s185,plain,
( spl0_11
| spl0_16 ),
inference(sat_conversion,[],[f265]) ).
cnf(s340,plain,
( ~ spl0_30
| ~ spl0_31
| ~ spl0_32 ),
inference(sat_conversion,[],[f469]) ).
cnf(s372,plain,
spl0_30,
inference(sat_conversion,[],[f522]) ).
cnf(s768,plain,
( ~ spl0_13
| spl0_61
| spl0_63 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s797,plain,
( spl0_15
| ~ spl0_61 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s859,plain,
( ~ spl0_13
| spl0_70
| spl0_72 ),
inference(sat_conversion,[],[f1284]) ).
cnf(s951,plain,
( ~ spl0_28
| ~ spl0_70 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s1100,plain,
( ~ spl0_63
| ~ spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s1141,plain,
( ~ spl0_72
| ~ spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f1676]) ).
cnf(s1214,plain,
( ~ spl0_11
| spl0_87
| spl0_89 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s1234,plain,
( spl0_44
| ~ spl0_87 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s1241,plain,
( spl0_16
| ~ spl0_87 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s1268,plain,
( ~ spl0_44
| ~ spl0_89 ),
inference(sat_conversion,[],[f1866]) ).
cnf(s1311,plain,
( ~ spl0_32
| spl0_77
| ~ spl0_89 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s1385,plain,
( ~ spl0_70
| spl0_81 ),
inference(sat_conversion,[],[f2001]) ).
cnf(s1406,plain,
( ~ spl0_13
| ~ spl0_77
| ~ spl0_81 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s1425,plain,
( spl0_14
| ~ spl0_70 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s1444,plain,
( spl0_28
| ~ spl0_76 ),
inference(sat_conversion,[],[f2072]) ).
cnf(s1445,plain,
( ~ spl0_13
| spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f2074]) ).
cnf(s1492,plain,
( ~ spl0_32
| spl0_44
| ~ spl0_81 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s1531,plain,
~ spl0_97,
inference(sat_conversion,[],[f2204]) ).
cnf(s1588,plain,
( ~ spl0_12
| ~ spl0_81
| spl0_102
| spl0_104 ),
inference(sat_conversion,[],[f2289]) ).
cnf(s1601,plain,
~ spl0_102,
inference(sat_conversion,[],[f2309]) ).
cnf(s1649,plain,
( spl0_105
| spl0_107 ),
inference(sat_conversion,[],[f2386]) ).
cnf(s1699,plain,
( ~ spl0_16
| spl0_111
| spl0_112 ),
inference(sat_conversion,[],[f2483]) ).
cnf(s1723,plain,
( spl0_12
| ~ spl0_111 ),
inference(sat_conversion,[],[f2517]) ).
cnf(s1806,plain,
( ~ spl0_16
| spl0_121
| spl0_123 ),
inference(sat_conversion,[],[f2716]) ).
cnf(s1817,plain,
~ spl0_121,
inference(sat_conversion,[],[f2729]) ).
cnf(s1824,plain,
( ~ spl0_123
| ~ spl0_124
| spl0_125 ),
inference(sat_conversion,[],[f2741]) ).
cnf(s1828,plain,
( ~ spl0_16
| ~ spl0_19
| spl0_126
| spl0_127 ),
inference(sat_conversion,[],[f2749]) ).
cnf(s1837,plain,
( ~ spl0_17
| ~ spl0_126 ),
inference(sat_conversion,[],[f2765]) ).
cnf(s1838,plain,
( spl0_124
| ~ spl0_126 ),
inference(sat_conversion,[],[f2767]) ).
cnf(s1846,plain,
( spl0_118
| ~ spl0_127 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s1861,plain,
( spl0_11
| ~ spl0_118 ),
inference(sat_conversion,[],[f2796]) ).
cnf(s1901,plain,
( ~ spl0_13
| spl0_132
| spl0_133 ),
inference(sat_conversion,[],[f2867]) ).
cnf(s1908,plain,
~ spl0_132,
inference(sat_conversion,[],[f2877]) ).
cnf(s1948,plain,
( ~ spl0_13
| ~ spl0_17
| spl0_137
| spl0_138 ),
inference(sat_conversion,[],[f2950]) ).
cnf(s1955,plain,
( spl0_77
| ~ spl0_137 ),
inference(sat_conversion,[],[f2961]) ).
cnf(s2026,plain,
( spl0_17
| ~ spl0_105
| ~ spl0_133 ),
inference(sat_conversion,[],[f3084]) ).
cnf(s2037,plain,
( ~ spl0_133
| ~ spl0_142
| spl0_143 ),
inference(sat_conversion,[],[f3105]) ).
cnf(s2125,plain,
( ~ spl0_81
| ~ spl0_107 ),
inference(sat_conversion,[],[f3263]) ).
cnf(s2350,plain,
( ~ spl0_11
| spl0_161
| spl0_162 ),
inference(sat_conversion,[],[f3626]) ).
cnf(s2355,plain,
( spl0_43
| ~ spl0_161 ),
inference(sat_conversion,[],[f3636]) ).
cnf(s2356,plain,
( spl0_31
| ~ spl0_161 ),
inference(sat_conversion,[],[f3638]) ).
cnf(s2371,plain,
( ~ spl0_11
| spl0_165
| spl0_166 ),
inference(sat_conversion,[],[f3662]) ).
cnf(s2458,plain,
~ spl0_165,
inference(sat_conversion,[],[f3768]) ).
cnf(s2615,plain,
( spl0_176
| spl0_177 ),
inference(sat_conversion,[],[f4054]) ).
cnf(s2625,plain,
~ spl0_176,
inference(sat_conversion,[],[f4076]) ).
cnf(s2648,plain,
( ~ spl0_17
| spl0_180
| spl0_181 ),
inference(sat_conversion,[],[f4117]) ).
cnf(s2678,plain,
( spl0_76
| ~ spl0_138 ),
inference(sat_conversion,[],[f4177]) ).
cnf(s2802,plain,
( ~ spl0_80
| spl0_158 ),
inference(sat_conversion,[],[f4293]) ).
cnf(s2869,plain,
~ spl0_152,
inference(sat_conversion,[],[f4387]) ).
cnf(s2877,plain,
~ spl0_153,
inference(sat_conversion,[],[f4392]) ).
cnf(s2928,plain,
( ~ spl0_129
| spl0_188 ),
inference(sat_conversion,[],[f4443]) ).
cnf(s2945,plain,
~ spl0_188,
inference(sat_conversion,[],[f4471]) ).
cnf(s2959,plain,
( ~ spl0_112
| ~ spl0_128
| spl0_129 ),
inference(sat_conversion,[],[f4477]) ).
cnf(s2964,plain,
( ~ spl0_12
| spl0_44
| ~ spl0_112 ),
inference(sat_conversion,[],[f4483]) ).
cnf(s3034,plain,
( ~ spl0_14
| ~ spl0_72
| spl0_193 ),
inference(sat_conversion,[],[f4570]) ).
cnf(s3056,plain,
( spl0_17
| ~ spl0_193 ),
inference(sat_conversion,[],[f4608]) ).
cnf(s3057,plain,
( spl0_192
| ~ spl0_193 ),
inference(sat_conversion,[],[f4610]) ).
cnf(s3091,plain,
( ~ spl0_12
| spl0_21
| ~ spl0_44
| ~ spl0_177 ),
inference(sat_conversion,[],[f4652]) ).
cnf(s3233,plain,
( ~ spl0_111
| spl0_128 ),
inference(sat_conversion,[],[f4838]) ).
cnf(s3252,plain,
( ~ spl0_111
| spl0_117 ),
inference(sat_conversion,[],[f4863]) ).
cnf(s3346,plain,
( ~ spl0_128
| spl0_157 ),
inference(sat_conversion,[],[f4988]) ).
cnf(s3462,plain,
( spl0_201
| spl0_202 ),
inference(sat_conversion,[],[f5183]) ).
cnf(s3474,plain,
( ~ spl0_12
| spl0_203
| spl0_204 ),
inference(sat_conversion,[],[f5201]) ).
cnf(s3480,plain,
~ spl0_203,
inference(sat_conversion,[],[f5209]) ).
cnf(s3488,plain,
( ~ spl0_204
| ~ spl0_205
| spl0_206 ),
inference(sat_conversion,[],[f5221]) ).
cnf(s3532,plain,
( spl0_205
| ~ spl0_207 ),
inference(sat_conversion,[],[f5267]) ).
cnf(s3560,plain,
( spl0_18
| ~ spl0_126 ),
inference(sat_conversion,[],[f5304]) ).
cnf(s3561,plain,
( ~ spl0_16
| spl0_19
| ~ spl0_126 ),
inference(sat_conversion,[],[f5306]) ).
cnf(s3605,plain,
( ~ spl0_125
| spl0_163 ),
inference(sat_conversion,[],[f5376]) ).
cnf(s3620,plain,
( spl0_186
| ~ spl0_206 ),
inference(sat_conversion,[],[f5402]) ).
cnf(s3640,plain,
( ~ spl0_125
| spl0_129
| ~ spl0_187 ),
inference(sat_conversion,[],[f5423]) ).
cnf(s3667,plain,
( spl0_21
| ~ spl0_125
| ~ spl0_186 ),
inference(sat_conversion,[],[f5458]) ).
cnf(s3731,plain,
( ~ spl0_77
| spl0_102
| ~ spl0_117
| spl0_153 ),
inference(sat_conversion,[],[f5461]) ).
cnf(s3789,plain,
( ~ spl0_137
| spl0_142 ),
inference(sat_conversion,[],[f5512]) ).
cnf(s3855,plain,
( ~ spl0_125
| ~ spl0_142 ),
inference(sat_conversion,[],[f5565]) ).
cnf(s3936,plain,
( ~ spl0_104
| spl0_157 ),
inference(sat_conversion,[],[f5654]) ).
cnf(s3975,plain,
( ~ spl0_43
| spl0_80 ),
inference(sat_conversion,[],[f5700]) ).
cnf(s4032,plain,
( ~ spl0_78
| spl0_152 ),
inference(sat_conversion,[],[f5778]) ).
cnf(s4135,plain,
( spl0_76
| ~ spl0_192 ),
inference(sat_conversion,[],[f5874]) ).
cnf(s4202,plain,
( ~ spl0_143
| spl0_186 ),
inference(sat_conversion,[],[f5969]) ).
cnf(s4315,plain,
( ~ spl0_107
| ~ spl0_142
| spl0_163 ),
inference(sat_conversion,[],[f6125]) ).
cnf(s4334,plain,
( spl0_81
| ~ spl0_105 ),
inference(sat_conversion,[],[f6145]) ).
cnf(s4411,plain,
~ spl0_82,
inference(sat_conversion,[],[f6236]) ).
cnf(s4420,plain,
( ~ spl0_11
| spl0_32
| ~ spl0_77 ),
inference(sat_conversion,[],[f6248]) ).
cnf(s4589,plain,
( spl0_32
| ~ spl0_175 ),
inference(sat_conversion,[],[f6492]) ).
cnf(s4595,plain,
( ~ spl0_174
| spl0_175 ),
inference(sat_conversion,[],[f6498]) ).
cnf(s4623,plain,
( ~ spl0_163
| spl0_164
| ~ spl0_166 ),
inference(sat_conversion,[],[f6544]) ).
cnf(s4635,plain,
( spl0_124
| ~ spl0_164 ),
inference(sat_conversion,[],[f6556]) ).
cnf(s4672,plain,
( ~ spl0_14
| ~ spl0_72
| spl0_129
| ~ spl0_202 ),
inference(sat_conversion,[],[f6624]) ).
cnf(s4681,plain,
( ~ spl0_201
| spl0_205 ),
inference(sat_conversion,[],[f6636]) ).
cnf(s4697,plain,
( spl0_125
| ~ spl0_163
| ~ spl0_177
| ~ spl0_205 ),
inference(sat_conversion,[],[f6640]) ).
cnf(s4752,plain,
( spl0_19
| ~ spl0_125 ),
inference(sat_conversion,[],[f6763]) ).
cnf(s4765,plain,
( spl0_78
| ~ spl0_181 ),
inference(sat_conversion,[],[f6786]) ).
cnf(s4781,plain,
( ~ spl0_75
| spl0_102
| ~ spl0_180
| spl0_187
| ~ spl0_205 ),
inference(sat_conversion,[],[f6814]) ).
cnf(s4782,plain,
( ~ spl0_76
| spl0_143
| ~ spl0_180
| ~ spl0_205 ),
inference(sat_conversion,[],[f6816]) ).
cnf(s4813,plain,
( ~ spl0_13
| spl0_142
| ~ spl0_143 ),
inference(sat_conversion,[],[f6855]) ).
cnf(s4944,plain,
( spl0_124
| ~ spl0_206 ),
inference(sat_conversion,[],[f6966]) ).
cnf(s4984,plain,
( ~ spl0_16
| ~ spl0_21
| spl0_172 ),
inference(sat_conversion,[],[f7030]) ).
cnf(s4985,plain,
( ~ spl0_21
| spl0_148 ),
inference(sat_conversion,[],[f7032]) ).
cnf(s5075,plain,
( ~ spl0_21
| spl0_211
| spl0_212 ),
inference(sat_conversion,[],[f7216]) ).
cnf(s5080,plain,
( spl0_163
| ~ spl0_211 ),
inference(sat_conversion,[],[f7225]) ).
cnf(s5081,plain,
( spl0_43
| ~ spl0_211 ),
inference(sat_conversion,[],[f7227]) ).
cnf(s5091,plain,
( ~ spl0_12
| ~ spl0_44
| ~ spl0_177
| spl0_213
| spl0_214 ),
inference(sat_conversion,[],[f7248]) ).
cnf(s5096,plain,
( spl0_163
| ~ spl0_213 ),
inference(sat_conversion,[],[f7257]) ).
cnf(s5107,plain,
( ~ spl0_12
| ~ spl0_44
| ~ spl0_177
| ~ spl0_214 ),
inference(sat_conversion,[],[f7270]) ).
cnf(s5114,plain,
( ~ spl0_21
| spl0_125
| ~ spl0_163
| ~ spl0_186 ),
inference(sat_conversion,[],[f7272]) ).
cnf(s5131,plain,
( ~ spl0_21
| spl0_125
| ~ spl0_163
| ~ spl0_212 ),
inference(sat_conversion,[],[f7303]) ).
cnf(s5132,plain,
( ~ spl0_44
| ~ spl0_163
| spl0_206
| ~ spl0_212 ),
inference(sat_conversion,[],[f7305]) ).
cnf(s5161,plain,
( ~ spl0_126
| spl0_128 ),
inference(sat_conversion,[],[f7334]) ).
cnf(s5205,plain,
( ~ spl0_115
| ~ spl0_148 ),
inference(sat_conversion,[],[f7339]) ).
cnf(s5322,plain,
( spl0_44
| ~ spl0_213 ),
inference(sat_conversion,[],[f7439]) ).
cnf(s5334,plain,
( ~ spl0_125
| spl0_205 ),
inference(sat_conversion,[],[f7458]) ).
cnf(s5393,plain,
( spl0_115
| ~ spl0_157 ),
inference(sat_conversion,[],[f7559]) ).
cnf(s5401,plain,
( ~ spl0_157
| spl0_216 ),
inference(sat_conversion,[],[f7568]) ).
cnf(s5431,plain,
( spl0_152
| ~ spl0_164
| ~ spl0_186 ),
inference(sat_conversion,[],[f7624]) ).
cnf(s5482,plain,
( ~ spl0_15
| ~ spl0_162
| spl0_174 ),
inference(sat_conversion,[],[f7694]) ).
cnf(s5499,plain,
( ~ spl0_77
| spl0_137
| spl0_153 ),
inference(sat_conversion,[],[f7697]) ).
cnf(s5629,plain,
( ~ spl0_15
| ~ spl0_32
| spl0_97
| spl0_156 ),
inference(sat_conversion,[],[f7858]) ).
cnf(s5693,plain,
( ~ spl0_15
| spl0_125
| ~ spl0_162
| ~ spl0_164
| spl0_211 ),
inference(sat_conversion,[],[f8083]) ).
cnf(s5833,plain,
( spl0_77
| ~ spl0_142
| ~ spl0_164 ),
inference(sat_conversion,[],[f8204]) ).
cnf(s5892,plain,
( spl0_77
| spl0_126
| ~ spl0_216 ),
inference(sat_conversion,[],[f8298]) ).
cnf(s5898,plain,
( ~ spl0_80
| spl0_211
| spl0_212 ),
inference(sat_conversion,[],[f8313]) ).
cnf(s5949,plain,
( spl0_142
| ~ spl0_163
| spl0_213 ),
inference(sat_conversion,[],[f8427]) ).
cnf(s5988,plain,
( ~ spl0_156
| ~ spl0_158 ),
inference(sat_conversion,[],[f8431]) ).
cnf(s6100,plain,
( ~ spl0_80
| ~ spl0_172 ),
inference(sat_conversion,[],[f8537]) ).
cnf(s6213,plain,
( ~ spl0_12
| spl0_14
| ~ spl0_18
| spl0_207 ),
inference(sat_conversion,[],[f8715]) ).
cnf(s6274,plain,
( spl0_142
| ~ spl0_187 ),
inference(sat_conversion,[],[f8745]) ).
cnf(s6297,plain,
( ~ spl0_80
| ~ spl0_212 ),
inference(sat_conversion,[],[f8796]) ).
cnf(s6299,plain,
( ~ spl0_12
| spl0_204 ),
inference(rat,[],[s3474,s3480]) ).
cnf(s6301,plain,
~ spl0_129,
inference(rat,[],[s2928,s2945]) ).
cnf(s6303,plain,
~ spl0_78,
inference(rat,[],[s4032,s2869]) ).
cnf(s6305,plain,
~ spl0_181,
inference(rat,[],[s4765,s6303]) ).
cnf(s6306,plain,
( ~ spl0_17
| spl0_180 ),
inference(rat,[],[s2648,s6305]) ).
cnf(s6308,plain,
spl0_177,
inference(rat,[],[s2615,s2625]) ).
cnf(s6312,plain,
( ~ spl0_11
| spl0_166 ),
inference(rat,[],[s2371,s2458]) ).
cnf(s6318,plain,
( ~ spl0_13
| spl0_133 ),
inference(rat,[],[s1901,s1908]) ).
cnf(s6320,plain,
( ~ spl0_16
| spl0_123 ),
inference(rat,[],[s1806,s1817]) ).
cnf(s6321,plain,
( ~ spl0_12
| ~ spl0_81
| spl0_104 ),
inference(rat,[],[s1588,s1601]) ).
cnf(s6323,plain,
( ~ spl0_72
| ~ spl0_81 ),
inference(rat,[],[s1141,s4411]) ).
cnf(s6324,plain,
( ~ spl0_63
| ~ spl0_77 ),
inference(rat,[],[s1100,s6303]) ).
cnf(s6329,plain,
( ~ spl0_31
| ~ spl0_32 ),
inference(rat,[],[s340,s372]) ).
cnf(s6334,plain,
( spl0_17
| ~ spl0_13
| ~ spl0_14 ),
inference(rat,[],[s1385,s2125,s859,s1649,s3034,s2026,s3056,s6318]) ).
cnf(s6335,plain,
( spl0_12
| spl0_11 ),
inference(rat,[],[s4813,s4315,s4782,s4697,s1649,s4681,s4334,s3462,s6323,s4672,s859,s951,s1444,s2678,s1948,s6306,s6334,s1955,s4752,s6324,s1828,s768,s5161,s169,s797,s2959,s121,s1699,s174,s1723,s185,s1846,s1861,s6308,s6301]) ).
cnf(s6336,plain,
( ~ spl0_14
| ~ spl0_13
| spl0_11 ),
inference(rat,[],[s4672,s859,s3462,s1385,s4681,s6321,s3488,s3936,s4944,s5401,s1824,s5892,s4752,s6324,s1828,s768,s1837,s797,s6334,s121,s1846,s1861,s6320,s185,s6299,s6335,s6301]) ).
cnf(s6337,plain,
( spl0_19
| spl0_77
| spl0_11 ),
inference(rat,[],[s5081,s3975,s5075,s6100,s5132,s4984,s5096,s3091,s5091,s5107,s2964,s1699,s3233,s3346,s5401,s4944,s5892,s1824,s3561,s4752,s6320,s185,s6335,s6308]) ).
cnf(s6338,plain,
( ~ spl0_126
| spl0_14
| spl0_11 ),
inference(rat,[],[s3667,s3620,s4985,s3488,s5205,s3532,s5393,s1824,s6213,s3346,s1838,s3560,s5161,s6320,s185,s6299,s6335]) ).
cnf(s6339,plain,
( ~ spl0_13
| spl0_11 ),
inference(rat,[],[s3091,s5114,s2964,s4202,s1699,s2037,s4315,s3252,s3789,s3731,s5499,s6337,s4752,s1828,s6338,s1649,s4334,s6323,s859,s1425,s6336,s6318,s185,s1846,s1861,s6335,s6308,s1601,s2877]) ).
cnf(s6340,plain,
spl0_11,
inference(rat,[],[s5081,s3975,s5075,s6100,s5131,s4984,s5096,s3091,s5091,s5107,s2964,s1699,s3252,s3731,s6337,s4752,s1828,s6338,s121,s169,s6339,s6335,s1846,s185,s1861,s6308,s1601,s2877]) ).
cnf(s6341,plain,
spl0_166,
inference(rat,[],[s6312,s6340]) ).
cnf(s6343,plain,
( ~ spl0_76
| spl0_125
| ~ spl0_13
| ~ spl0_14 ),
inference(rat,[],[s6274,s4315,s4781,s4697,s1649,s4681,s4334,s3462,s6323,s4672,s859,s951,s1445,s1444,s6306,s6334,s1601,s6308,s6301]) ).
cnf(s6344,plain,
( spl0_76
| ~ spl0_13
| ~ spl0_14 ),
inference(rat,[],[s1385,s1406,s859,s1955,s3034,s1948,s3057,s2678,s4135,s6334]) ).
cnf(s6345,plain,
( ~ spl0_13
| ~ spl0_14 ),
inference(rat,[],[s4781,s3640,s5334,s6343,s1445,s6344,s6306,s6334,s6301,s1601]) ).
cnf(s6347,plain,
( spl0_77
| ~ spl0_14 ),
inference(rat,[],[s5833,s4623,s5949,s5080,s5898,s6297,s3975,s2355,s2350,s5482,s4595,s4589,s1311,s5322,s1268,s1214,s1241,s121,s169,s6345,s6341,s6340]) ).
cnf(s6348,plain,
( ~ spl0_15
| ~ spl0_14 ),
inference(rat,[],[s3855,s5693,s4623,s5081,s4315,s3975,s2350,s1649,s2802,s2356,s4334,s5988,s6329,s1492,s5629,s3789,s4420,s5499,s6347,s1268,s1214,s1241,s121,s2877,s1531,s6340,s6341]) ).
cnf(s6349,plain,
~ spl0_14,
inference(rat,[],[s6348,s169,s6345]) ).
cnf(s6352,plain,
spl0_12,
inference(rat,[],[s174,s6349]) ).
cnf(s6354,plain,
spl0_204,
inference(rat,[],[s6299,s6352]) ).
cnf(s6355,plain,
~ spl0_13,
inference(rat,[],[s110,s6340,s6352]) ).
cnf(s6357,plain,
spl0_15,
inference(rat,[],[s169,s6355]) ).
cnf(s6361,plain,
( ~ spl0_89
| spl0_77 ),
inference(rat,[],[s5833,s4623,s5949,s5080,s5898,s6297,s3975,s2355,s2350,s5482,s4595,s4589,s5322,s1311,s1268,s6341,s6340,s6357]) ).
cnf(s6362,plain,
( ~ spl0_87
| spl0_125 ),
inference(rat,[],[s4623,s4635,s5096,s1824,s5091,s5107,s6320,s1234,s1241,s6341,s6308,s6352]) ).
cnf(s6363,plain,
spl0_125,
inference(rat,[],[s5693,s4623,s5081,s4315,s3975,s2350,s1649,s2802,s2356,s4334,s5988,s6329,s1492,s5629,s3789,s4420,s5499,s6361,s1268,s1214,s6362,s6357,s6341,s6340,s1531,s2877]) ).
cnf(s6364,plain,
spl0_205,
inference(rat,[],[s5334,s6363]) ).
cnf(s6368,plain,
spl0_163,
inference(rat,[],[s3605,s6363]) ).
cnf(s6369,plain,
spl0_206,
inference(rat,[],[s3488,s6354,s6364]) ).
cnf(s6374,plain,
spl0_164,
inference(rat,[],[s4623,s6341,s6368]) ).
cnf(s6377,plain,
spl0_186,
inference(rat,[],[s3620,s6369]) ).
cnf(s6382,plain,
$false,
inference(rat,[],[s5431,s2869,s6377,s6374]) ).
fof(f8797,plain,
$false,
inference(avatar_sat_refutation,[],[s6382]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO169+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.17/0.41 % Computer : n018.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.41 % CPULimit : 300
% 0.17/0.41 % WCLimit : 300
% 0.17/0.41 % DateTime : Sun Sep 27 07:23:23 UTC 2026
% 0.17/0.41 % CPUTime :
% 0.17/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.17/0.46 Running first-order model finding
% 0.17/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.50/0.77 % (1988110)Will run a generic schedule for satisfiability detection.
% 1.50/0.77 % (1988116)% WARNING: option uhcvi not known.
% 1.50/0.77 % (1988116)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3501403970:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.50/0.77 % (1988115)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3956837581_2999 on theBenchmark for (2999ds/0Mi)
% 1.50/0.77 % Detected minimum model sizes of [1]
% 1.50/0.77 % Detected maximum model sizes of [19]
% 1.50/0.77 % TRYING [1]
% 1.50/0.77 % TRYING [2]
% 1.50/0.77 % TRYING [3]
% 1.50/0.77 % TRYING [4]
% 1.50/0.77 % (1988119)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2793736552:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.50/0.77 % (1988118)dis+10_1_sil=32000:sp=arity:random_seed=2196616978:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.50/0.77 % (1988121)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1274849633:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.50/0.77 % (1988120)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1845242101:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.50/0.77 % (1988117)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2683967642:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.50/0.77 % TRYING [5]
% 1.50/0.77 % TRYING [6]
% 1.50/0.77 % (1988119)Instruction limit reached!
% 1.50/0.77 % (1988119)------------------------------
% 1.50/0.77 % (1988119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.77 % (1988119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.77 % (1988119)CaDiCaL version: 2.1.3
% 1.50/0.77 % (1988119)Termination reason: Instruction limit
% 1.50/0.77 % (1988119)Termination phase: Saturation
% 1.50/0.77 % (1988119)Time elapsed: 0.097 s
% 1.50/0.77 % (1988119)Peak memory usage: 12 MB
% 1.50/0.77 % (1988119)Instructions burned: 116 (million)
% 1.50/0.77 % (1988118)Instruction limit reached!
% 1.50/0.77 % (1988118)------------------------------
% 1.50/0.77 % (1988118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.77 % (1988118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.77 % (1988118)CaDiCaL version: 2.1.3
% 1.50/0.77 % (1988118)Termination reason: Instruction limit
% 1.50/0.77 % (1988118)Termination phase: Saturation
% 1.50/0.77 % (1988118)Time elapsed: 0.106 s
% 1.50/0.77 % (1988118)Peak memory usage: 12 MB
% 1.50/0.77 % (1988118)Instructions burned: 103 (million)
% 1.50/0.77 % (1988129)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1741980123:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.50/0.77 % Detected minimum model sizes of [1]
% 1.50/0.77 % Detected maximum model sizes of [19]
% 1.50/0.77 % TRYING [1]
% 1.50/0.77 % TRYING [2]
% 1.50/0.77 % (1988130)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2871881300:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.50/0.77 % TRYING [3]
% 1.50/0.77 % TRYING [4]
% 1.50/0.77 % (1988120)Instruction limit reached!
% 1.50/0.77 % (1988120)------------------------------
% 1.50/0.77 % (1988120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.77 % (1988120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.77 % (1988120)CaDiCaL version: 2.1.3
% 1.50/0.77 % (1988120)Termination reason: Instruction limit
% 1.50/0.77 % (1988120)Termination phase: Saturation
% 1.50/0.77 % (1988120)Time elapsed: 0.146 s
% 1.50/0.77 % (1988120)Peak memory usage: 12 MB
% 1.50/0.77 % (1988120)Instructions burned: 131 (million)
% 1.50/0.77 % TRYING [5]
% 1.50/0.77 % (1988121)Instruction limit reached!
% 1.50/0.77 % (1988121)------------------------------
% 1.50/0.77 % (1988121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.77 % (1988121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.77 % (1988121)CaDiCaL version: 2.1.3
% 1.50/0.77 % (1988121)Termination reason: Instruction limit
% 1.50/0.77 % (1988121)Termination phase: Saturation
% 1.50/0.77 % (1988121)Time elapsed: 0.159 s
% 1.50/0.77 % (1988121)Peak memory usage: 13 MB
% 1.50/0.77 % (1988121)Instructions burned: 160 (million)
% 1.50/0.77 % (1988133)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=788343500:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.50/0.77 % (1988134)ott-21_1_sil=16000:fs=off:random_seed=996574512:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.50/0.77 % TRYING [6]
% 1.50/0.77 % TRYING [7]
% 1.50/0.77 % (1988117) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1988110-1988117"...
% 1.50/0.77 % (1988117)...printing done.
% 1.50/0.77 % (1988117)Refutation found. Thanks to Tanya!
% 1.50/0.77 % SZS status Theorem for theBenchmark
% 1.50/0.77 % SZS output start Proof for theBenchmark
% See solution above
% 1.50/0.80 % (1988117)------------------------------
% 1.50/0.80 % (1988117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.80 % (1988117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.80 % (1988117)CaDiCaL version: 2.1.3
% 1.50/0.80 % (1988117)Termination reason: Refutation
% 1.50/0.80 % (1988117)Time elapsed: 0.252 s
% 1.50/0.80 % (1988117)Peak memory usage: 15 MB
% 1.50/0.80 % (1988117)Instructions burned: 234 (million)
% 1.50/0.80 % (1988110)Success in time 0.295 s
% 1.50/0.80 % Vampire exiting
%------------------------------------------------------------------------------