%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO169+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:51:45 AM UTC 2026
% Result : Theorem 8.76s 2.31s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 133
% Syntax : Number of formulae : 961 ( 95 unt; 86 def)
% Number of atoms : 2610 ( 378 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 3113 (1464 ~;1528 |; 19 &)
% ( 86 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 92 ( 90 usr; 88 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 19 con; 0-2 aty)
% Number of variables : 210 ( 0 sgn 204 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ( incident(p3,X0)
& incident(p1,X0)
& incident(p2,X0) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_normal) ).
fof(f2,axiom,
( ( incident(a1,b2b3)
& incident(a2,b3b1)
& incident(a3,b1b2) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t_a_in_b) ).
fof(f3,axiom,
( ( incident(b1,a2a3)
& incident(b2,a3a1)
& incident(b3,a1a2) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t_b_in_a) ).
fof(f4,axiom,
( incident(a1,b2b3)
| incident(b3,a1a2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap1) ).
fof(f5,axiom,
( incident(a2,b3b1)
| incident(b1,a2a3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap2) ).
fof(f6,axiom,
( incident(a3,b1b2)
| incident(b2,a3a1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gap3) ).
fof(f7,axiom,
incident(a1,a1a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1a2) ).
fof(f8,axiom,
incident(a2,a1a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2a1) ).
fof(f9,axiom,
incident(a2,a2a3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2a3) ).
fof(f10,axiom,
incident(a3,a2a3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia3a2) ).
fof(f11,axiom,
incident(a3,a3a1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia3a1) ).
fof(f12,axiom,
incident(a1,a3a1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1a3) ).
fof(f13,axiom,
incident(b1,b1b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1b2) ).
fof(f14,axiom,
incident(b2,b1b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2b1) ).
fof(f15,axiom,
incident(b2,b2b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2b3) ).
fof(f16,axiom,
incident(b3,b2b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib3b2) ).
fof(f17,axiom,
incident(b3,b3b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib3b1) ).
fof(f18,axiom,
incident(b1,b3b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1b3) ).
fof(f19,axiom,
incident(s,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iss1) ).
fof(f20,axiom,
incident(s,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iss2) ).
fof(f21,axiom,
incident(s,s3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',iss3) ).
fof(f22,axiom,
incident(a1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia1s1) ).
fof(f23,axiom,
incident(a2,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia2s2) ).
fof(f24,axiom,
incident(a3,s3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ia3s3) ).
fof(f25,axiom,
incident(b1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib1s1) ).
fof(f26,axiom,
incident(b2,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib2s2) ).
fof(f27,axiom,
incident(b3,s3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ib3s3) ).
fof(f28,axiom,
incident(p3,a1a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ip3a) ).
fof(f29,axiom,
incident(p3,b1b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ip3b) ).
fof(f30,axiom,
incident(p1,a2a3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ip1a) ).
fof(f31,axiom,
incident(p1,b2b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ip1b) ).
fof(f32,axiom,
incident(p2,a3a1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ip2a) ).
fof(f33,axiom,
incident(p2,b3b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ip2b) ).
fof(f34,axiom,
! [X0,X1] :
( incident(X0,X1)
=> point(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_point) ).
fof(f35,axiom,
! [X0,X1] :
( incident(X0,X1)
=> line(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sort_line) ).
fof(f36,axiom,
( a1 = a2
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diff_a1_a2) ).
fof(f37,axiom,
( a2 = a3
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diff_a2_a3) ).
fof(f38,axiom,
( a3 = a1
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diff_a3_a1) ).
fof(f39,axiom,
( b1 = b2
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diff_b1_b2) ).
fof(f41,axiom,
( b3 = b1
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diff_b3_b1) ).
fof(f42,axiom,
( a1a2 = b1b2
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not12) ).
fof(f43,axiom,
( a2a3 = b2b3
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not23) ).
fof(f44,axiom,
( a3a1 = b3b1
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not31) ).
fof(f50,axiom,
! [X0,X1,X2,X3] :
( ( incident(X0,X2)
& incident(X0,X3)
& incident(X1,X2)
& incident(X1,X3) )
=> ( X0 = X1
| X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique) ).
fof(f51,axiom,
! [X0,X1] :
( ( point(X0)
& point(X1) )
=> ? [X2] :
( incident(X0,X2)
& incident(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join) ).
fof(f52,axiom,
! [X0,X1] :
( ( line(X0)
& line(X1) )
=> ? [X2] :
( incident(X2,X0)
& incident(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet) ).
fof(f53,conjecture,
goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f54,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,plain,
~ goal,
inference(flattening,[],[f54]) ).
fof(f56,plain,
! [X0] :
( goal
| ~ incident(p3,X0)
| ~ incident(p1,X0)
| ~ incident(p2,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f57,plain,
! [X0] :
( goal
| ~ incident(p3,X0)
| ~ incident(p1,X0)
| ~ incident(p2,X0) ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
( goal
| ~ incident(a1,b2b3)
| ~ incident(a2,b3b1)
| ~ incident(a3,b1b2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f59,plain,
( goal
| ~ incident(a1,b2b3)
| ~ incident(a2,b3b1)
| ~ incident(a3,b1b2) ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
( goal
| ~ incident(b1,a2a3)
| ~ incident(b2,a3a1)
| ~ incident(b3,a1a2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f61,plain,
( goal
| ~ incident(b1,a2a3)
| ~ incident(b2,a3a1)
| ~ incident(b3,a1a2) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( point(X0)
| ~ incident(X0,X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f63,plain,
! [X0,X1] :
( line(X1)
| ~ incident(X0,X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f64,plain,
( goal
| a1 != a2 ),
inference(ennf_transformation,[],[f36]) ).
fof(f65,plain,
( goal
| a2 != a3 ),
inference(ennf_transformation,[],[f37]) ).
fof(f66,plain,
( goal
| a1 != a3 ),
inference(ennf_transformation,[],[f38]) ).
fof(f67,plain,
( goal
| b1 != b2 ),
inference(ennf_transformation,[],[f39]) ).
fof(f69,plain,
( goal
| b1 != b3 ),
inference(ennf_transformation,[],[f41]) ).
fof(f70,plain,
( goal
| b1b2 != a1a2 ),
inference(ennf_transformation,[],[f42]) ).
fof(f71,plain,
( goal
| b2b3 != a2a3 ),
inference(ennf_transformation,[],[f43]) ).
fof(f72,plain,
( goal
| b3b1 != a3a1 ),
inference(ennf_transformation,[],[f44]) ).
fof(f80,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| X2 = X3
| ~ incident(X0,X2)
| ~ incident(X0,X3)
| ~ incident(X1,X2)
| ~ incident(X1,X3) ),
inference(ennf_transformation,[],[f50]) ).
fof(f81,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| X2 = X3
| ~ incident(X0,X2)
| ~ incident(X0,X3)
| ~ incident(X1,X2)
| ~ incident(X1,X3) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1] :
( ? [X2] :
( incident(X0,X2)
& incident(X1,X2) )
| ~ point(X0)
| ~ point(X1) ),
inference(ennf_transformation,[],[f51]) ).
fof(f83,plain,
! [X0,X1] :
( ? [X2] :
( incident(X0,X2)
& incident(X1,X2) )
| ~ point(X0)
| ~ point(X1) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1] :
( ? [X2] :
( incident(X2,X0)
& incident(X2,X1) )
| ~ line(X0)
| ~ line(X1) ),
inference(ennf_transformation,[],[f52]) ).
fof(f85,plain,
! [X0,X1] :
( ? [X2] :
( incident(X2,X0)
& incident(X2,X1) )
| ~ line(X0)
| ~ line(X1) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( ( incident(X0,sK0(X0,X1))
& incident(X1,sK0(X0,X1)) )
| ~ point(X0)
| ~ point(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f83]) ).
fof(f87,plain,
! [X0,X1] :
( ( incident(sK1(X0,X1),X0)
& incident(sK1(X0,X1),X1) )
| ~ line(X0)
| ~ line(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f85]) ).
fof(f88,plain,
! [X0] :
( goal
| ~ incident(p3,X0)
| ~ incident(p1,X0)
| ~ incident(p2,X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f89,plain,
( goal
| ~ incident(a1,b2b3)
| ~ incident(a2,b3b1)
| ~ incident(a3,b1b2) ),
inference(cnf_transformation,[],[f59]) ).
fof(f90,plain,
( goal
| ~ incident(b1,a2a3)
| ~ incident(b2,a3a1)
| ~ incident(b3,a1a2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f91,plain,
( incident(a1,b2b3)
| incident(b3,a1a2) ),
inference(cnf_transformation,[],[f4]) ).
fof(f92,plain,
( incident(a2,b3b1)
| incident(b1,a2a3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f93,plain,
( incident(a3,b1b2)
| incident(b2,a3a1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f94,plain,
incident(a1,a1a2),
inference(cnf_transformation,[],[f7]) ).
fof(f95,plain,
incident(a2,a1a2),
inference(cnf_transformation,[],[f8]) ).
fof(f96,plain,
incident(a2,a2a3),
inference(cnf_transformation,[],[f9]) ).
fof(f97,plain,
incident(a3,a2a3),
inference(cnf_transformation,[],[f10]) ).
fof(f98,plain,
incident(a3,a3a1),
inference(cnf_transformation,[],[f11]) ).
fof(f99,plain,
incident(a1,a3a1),
inference(cnf_transformation,[],[f12]) ).
fof(f100,plain,
incident(b1,b1b2),
inference(cnf_transformation,[],[f13]) ).
fof(f101,plain,
incident(b2,b1b2),
inference(cnf_transformation,[],[f14]) ).
fof(f102,plain,
incident(b2,b2b3),
inference(cnf_transformation,[],[f15]) ).
fof(f103,plain,
incident(b3,b2b3),
inference(cnf_transformation,[],[f16]) ).
fof(f104,plain,
incident(b3,b3b1),
inference(cnf_transformation,[],[f17]) ).
fof(f105,plain,
incident(b1,b3b1),
inference(cnf_transformation,[],[f18]) ).
fof(f106,plain,
incident(s,s1),
inference(cnf_transformation,[],[f19]) ).
fof(f107,plain,
incident(s,s2),
inference(cnf_transformation,[],[f20]) ).
fof(f108,plain,
incident(s,s3),
inference(cnf_transformation,[],[f21]) ).
fof(f109,plain,
incident(a1,s1),
inference(cnf_transformation,[],[f22]) ).
fof(f110,plain,
incident(a2,s2),
inference(cnf_transformation,[],[f23]) ).
fof(f111,plain,
incident(a3,s3),
inference(cnf_transformation,[],[f24]) ).
fof(f112,plain,
incident(b1,s1),
inference(cnf_transformation,[],[f25]) ).
fof(f113,plain,
incident(b2,s2),
inference(cnf_transformation,[],[f26]) ).
fof(f114,plain,
incident(b3,s3),
inference(cnf_transformation,[],[f27]) ).
fof(f115,plain,
incident(p3,a1a2),
inference(cnf_transformation,[],[f28]) ).
fof(f116,plain,
incident(p3,b1b2),
inference(cnf_transformation,[],[f29]) ).
fof(f117,plain,
incident(p1,a2a3),
inference(cnf_transformation,[],[f30]) ).
fof(f118,plain,
incident(p1,b2b3),
inference(cnf_transformation,[],[f31]) ).
fof(f119,plain,
incident(p2,a3a1),
inference(cnf_transformation,[],[f32]) ).
fof(f120,plain,
incident(p2,b3b1),
inference(cnf_transformation,[],[f33]) ).
fof(f121,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| point(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f122,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line(X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f123,plain,
( goal
| a1 != a2 ),
inference(cnf_transformation,[],[f64]) ).
fof(f124,plain,
( goal
| a2 != a3 ),
inference(cnf_transformation,[],[f65]) ).
fof(f125,plain,
( goal
| a1 != a3 ),
inference(cnf_transformation,[],[f66]) ).
fof(f126,plain,
( goal
| b1 != b2 ),
inference(cnf_transformation,[],[f67]) ).
fof(f128,plain,
( goal
| b1 != b3 ),
inference(cnf_transformation,[],[f69]) ).
fof(f129,plain,
( goal
| b1b2 != a1a2 ),
inference(cnf_transformation,[],[f70]) ).
fof(f130,plain,
( goal
| b2b3 != a2a3 ),
inference(cnf_transformation,[],[f71]) ).
fof(f131,plain,
( goal
| b3b1 != a3a1 ),
inference(cnf_transformation,[],[f72]) ).
fof(f137,plain,
! [X2,X3,X0,X1] :
( ~ incident(X1,X3)
| X2 = X3
| ~ incident(X0,X2)
| ~ incident(X0,X3)
| ~ incident(X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f81]) ).
fof(f138,plain,
! [X0,X1] :
( incident(X1,sK0(X0,X1))
| ~ point(X0)
| ~ point(X1) ),
inference(cnf_transformation,[],[f86]) ).
fof(f139,plain,
! [X0,X1] :
( incident(X0,sK0(X0,X1))
| ~ point(X0)
| ~ point(X1) ),
inference(cnf_transformation,[],[f86]) ).
fof(f140,plain,
! [X0,X1] :
( incident(sK1(X0,X1),X1)
| ~ line(X0)
| ~ line(X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f141,plain,
! [X0,X1] :
( incident(sK1(X0,X1),X0)
| ~ line(X0)
| ~ line(X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f142,plain,
~ goal,
inference(cnf_transformation,[],[f55]) ).
fof(f148,plain,
b3b1 != a3a1,
inference(forward_subsumption_resolution,[],[f131,f142]) ).
fof(f149,plain,
b2b3 != a2a3,
inference(forward_subsumption_resolution,[],[f130,f142]) ).
fof(f150,plain,
b1b2 != a1a2,
inference(forward_subsumption_resolution,[],[f129,f142]) ).
fof(f151,plain,
b1 != b3,
inference(forward_subsumption_resolution,[],[f128,f142]) ).
fof(f153,plain,
b1 != b2,
inference(forward_subsumption_resolution,[],[f126,f142]) ).
fof(f154,plain,
a1 != a3,
inference(forward_subsumption_resolution,[],[f125,f142]) ).
fof(f155,plain,
a2 != a3,
inference(forward_subsumption_resolution,[],[f124,f142]) ).
fof(f156,plain,
a1 != a2,
inference(forward_subsumption_resolution,[],[f123,f142]) ).
fof(f158,definition,
( spl2_1
<=> incident(b2,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f159,plain,
( ~ incident(b2,a3a1)
| spl2_1 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f160,plain,
( incident(b2,a3a1)
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f162,definition,
( spl2_2
<=> incident(a3,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f164,plain,
( incident(a3,b1b2)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f165,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f93,f162,f158]) ).
fof(f167,definition,
( spl2_3
<=> incident(b1,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f168,plain,
( ~ incident(b1,a2a3)
| spl2_3 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f169,plain,
( incident(b1,a2a3)
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f171,definition,
( spl2_4
<=> incident(a2,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f172,plain,
( ~ incident(a2,b3b1)
| spl2_4 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f173,plain,
( incident(a2,b3b1)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f174,plain,
( spl2_3
| spl2_4 ),
inference(avatar_split_clause,[],[f92,f171,f167]) ).
fof(f176,definition,
( spl2_5
<=> incident(b3,a1a2) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f177,plain,
( ~ incident(b3,a1a2)
| spl2_5 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f178,plain,
( incident(b3,a1a2)
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl2_6
<=> incident(a1,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f182,plain,
( incident(a1,b2b3)
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f183,plain,
( spl2_5
| spl2_6 ),
inference(avatar_split_clause,[],[f91,f180,f176]) ).
fof(f184,plain,
( ~ incident(b1,a2a3)
| ~ incident(b2,a3a1)
| ~ incident(b3,a1a2) ),
inference(forward_subsumption_resolution,[],[f90,f142]) ).
fof(f185,plain,
( ~ incident(a1,b2b3)
| ~ incident(a2,b3b1)
| ~ incident(a3,b1b2) ),
inference(forward_subsumption_resolution,[],[f89,f142]) ).
fof(f186,plain,
! [X0] :
( ~ incident(p2,X0)
| ~ incident(p1,X0)
| ~ incident(p3,X0) ),
inference(forward_subsumption_resolution,[],[f88,f142]) ).
fof(f187,plain,
( ~ spl2_5
| ~ spl2_1
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f184,f167,f158,f176]) ).
fof(f188,plain,
( ~ spl2_2
| ~ spl2_4
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f185,f180,f171,f162]) ).
fof(f189,plain,
( ~ incident(p1,a3a1)
| ~ incident(p3,a3a1) ),
inference(resolution,[],[f119,f186]) ).
fof(f191,definition,
( spl2_7
<=> incident(p3,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f192,plain,
( incident(p3,a3a1)
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( ~ incident(p3,a3a1)
| spl2_7 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f195,definition,
( spl2_8
<=> incident(p1,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f197,plain,
( ~ incident(p1,a3a1)
| spl2_8 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,plain,
( ~ spl2_7
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f189,f195,f191]) ).
fof(f199,plain,
( ~ incident(p1,b3b1)
| ~ incident(p3,b3b1) ),
inference(resolution,[],[f120,f186]) ).
fof(f201,definition,
( spl2_9
<=> incident(p3,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f203,plain,
( ~ incident(p3,b3b1)
| spl2_9 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl2_10
<=> incident(p1,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f207,plain,
( ~ incident(p1,b3b1)
| spl2_10 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,plain,
( ~ spl2_9
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f199,f205,f201]) ).
fof(f210,plain,
! [X0,X1] :
( ~ incident(p3,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1a2)
| a1a2 = X0
| p3 = X1 ),
inference(resolution,[],[f137,f115]) ).
fof(f212,plain,
! [X0,X1] :
( ~ incident(p1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2a3)
| a2a3 = X0
| p1 = X1 ),
inference(resolution,[],[f137,f117]) ).
fof(f213,plain,
! [X0,X1] :
( ~ incident(p2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a3a1)
| a3a1 = X0
| p2 = X1 ),
inference(resolution,[],[f137,f119]) ).
fof(f215,plain,
! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a3a1)
| a3a1 = X0
| a1 = X1 ),
inference(resolution,[],[f137,f99]) ).
fof(f216,plain,
! [X0,X1] :
( ~ incident(a1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1a2)
| a1a2 = X0
| a1 = X1 ),
inference(resolution,[],[f137,f94]) ).
fof(f217,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a1a2)
| a1a2 = X0
| a2 = X1 ),
inference(resolution,[],[f137,f95]) ).
fof(f218,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2a3)
| a2a3 = X0
| a2 = X1 ),
inference(resolution,[],[f137,f96]) ).
fof(f219,plain,
! [X0,X1] :
( ~ incident(a3,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a3a1)
| a3a1 = X0
| a3 = X1 ),
inference(resolution,[],[f137,f98]) ).
fof(f220,plain,
! [X0,X1] :
( ~ incident(a3,X0)
| ~ incident(X1,X0)
| ~ incident(X1,a2a3)
| a2a3 = X0
| a3 = X1 ),
inference(resolution,[],[f137,f97]) ).
fof(f221,plain,
! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b1b2)
| b1b2 = X0
| b1 = X1 ),
inference(resolution,[],[f137,f100]) ).
fof(f222,plain,
! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b3b1)
| b3b1 = X0
| b1 = X1 ),
inference(resolution,[],[f137,f105]) ).
fof(f223,plain,
! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b1b2)
| b1b2 = X0
| b2 = X1 ),
inference(resolution,[],[f137,f101]) ).
fof(f224,plain,
! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2b3)
| b2b3 = X0
| b2 = X1 ),
inference(resolution,[],[f137,f102]) ).
fof(f225,plain,
! [X0,X1] :
( ~ incident(b3,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b2b3)
| b2b3 = X0
| b3 = X1 ),
inference(resolution,[],[f137,f103]) ).
fof(f226,plain,
! [X0,X1] :
( ~ incident(b3,X0)
| ~ incident(X1,X0)
| ~ incident(X1,b3b1)
| b3b1 = X0
| b3 = X1 ),
inference(resolution,[],[f137,f104]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( ~ line(X0)
| ~ line(X1)
| X0 = X2
| ~ incident(X3,X2)
| ~ incident(X3,X0)
| ~ incident(sK1(X0,X1),X2)
| sK1(X0,X1) = X3 ),
inference(resolution,[],[f141,f137]) ).
fof(f233,plain,
! [X2,X3,X0,X1] :
( ~ incident(sK1(X0,X1),X2)
| X0 = X2
| ~ incident(X3,X2)
| ~ incident(X3,X0)
| ~ line(X1)
| sK1(X0,X1) = X3 ),
inference(forward_subsumption_resolution,[],[f232,f122]) ).
fof(f234,plain,
! [X0] :
( ~ point(X0)
| ~ point(p2)
| ~ incident(p1,sK0(X0,p2))
| ~ incident(p3,sK0(X0,p2)) ),
inference(resolution,[],[f138,f186]) ).
fof(f238,definition,
( spl2_11
<=> point(p2) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f239,plain,
( point(p2)
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( ~ point(p2)
| spl2_11 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl2_12
<=> ! [X0] :
( ~ point(X0)
| ~ incident(p3,sK0(X0,p2))
| ~ incident(p1,sK0(X0,p2)) ) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f243,plain,
( ! [X0] :
( ~ incident(p1,sK0(X0,p2))
| ~ incident(p3,sK0(X0,p2))
| ~ point(X0) )
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f244,plain,
( ~ spl2_11
| spl2_12 ),
inference(avatar_split_clause,[],[f234,f242,f238]) ).
fof(f257,plain,
! [X0] :
( ~ incident(X0,a3a1)
| ~ incident(X0,a1a2)
| a3a1 = a1a2
| a1 = X0 ),
inference(resolution,[],[f216,f99]) ).
fof(f259,plain,
! [X0] :
( ~ incident(X0,s1)
| ~ incident(X0,a1a2)
| a1a2 = s1
| a1 = X0 ),
inference(resolution,[],[f216,f109]) ).
fof(f264,definition,
( spl2_13
<=> point(a1) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f265,plain,
( point(a1)
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( ~ point(a1)
| spl2_13 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f276,definition,
( spl2_16
<=> a1a2 = s1 ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
fof(f278,plain,
( a1a2 = s1
| ~ spl2_16 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f280,definition,
( spl2_17
<=> ! [X0] :
( ~ incident(X0,s1)
| a1 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f281,plain,
( ! [X0] :
( ~ incident(X0,s1)
| a1 = X0
| ~ incident(X0,a1a2) )
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f282,plain,
( spl2_16
| spl2_17 ),
inference(avatar_split_clause,[],[f259,f280,f276]) ).
fof(f284,definition,
( spl2_18
<=> a3a1 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f286,plain,
( a3a1 = a1a2
| ~ spl2_18 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f288,definition,
( spl2_19
<=> ! [X0] :
( ~ incident(X0,a3a1)
| a1 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f289,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| a1 = X0
| ~ incident(X0,a3a1) )
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f290,plain,
( spl2_18
| spl2_19 ),
inference(avatar_split_clause,[],[f257,f288,f284]) ).
fof(f293,plain,
( incident(a2,a3a1)
| ~ spl2_18 ),
inference(superposition,[],[f95,f286]) ).
fof(f294,plain,
( incident(p3,a3a1)
| ~ spl2_18 ),
inference(superposition,[],[f115,f286]) ).
fof(f296,plain,
( $false
| spl2_7
| ~ spl2_18 ),
inference(forward_subsumption_resolution,[],[f294,f193]) ).
fof(f297,plain,
( spl2_7
| ~ spl2_18 ),
inference(avatar_contradiction_clause,[],[f296]) ).
fof(f300,plain,
( incident(s,a1a2)
| ~ spl2_16 ),
inference(superposition,[],[f106,f278]) ).
fof(f301,plain,
( p3 = a1
| ~ incident(p3,a3a1)
| ~ spl2_19 ),
inference(resolution,[],[f289,f115]) ).
fof(f303,plain,
( a1 = a2
| ~ incident(a2,a3a1)
| ~ spl2_19 ),
inference(resolution,[],[f289,f95]) ).
fof(f320,definition,
( spl2_23
<=> incident(b3,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition]) ).
fof(f321,plain,
( incident(b3,a3a1)
| ~ spl2_23 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( ~ incident(b3,a3a1)
| spl2_23 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl2_24
<=> a1 = b3 ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f325,plain,
( a1 != b3
| spl2_24 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f326,plain,
( a1 = b3
| ~ spl2_24 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f328,plain,
( ~ incident(a2,a3a1)
| ~ spl2_19 ),
inference(forward_subsumption_resolution,[],[f303,f156]) ).
fof(f407,plain,
( ! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,a3a1)
| b2b3 = a3a1
| a1 = X0 )
| ~ spl2_6 ),
inference(resolution,[],[f182,f215]) ).
fof(f413,definition,
( spl2_25
<=> b2b3 = a3a1 ),
introduced(definition,[new_symbols(definition,[spl2_25])],[avatar_definition]) ).
fof(f415,plain,
( b2b3 = a3a1
| ~ spl2_25 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,definition,
( spl2_26
<=> ! [X0] :
( ~ incident(X0,b2b3)
| a1 = X0
| ~ incident(X0,a3a1) ) ),
introduced(definition,[new_symbols(definition,[spl2_26])],[avatar_definition]) ).
fof(f418,plain,
( ! [X0] :
( ~ incident(X0,a3a1)
| a1 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_26 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( spl2_25
| spl2_26
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f407,f180,f417,f413]) ).
fof(f423,plain,
( p3 = a1
| ~ spl2_7
| ~ spl2_19 ),
inference(forward_subsumption_resolution,[],[f301,f192]) ).
fof(f437,plain,
! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,a1a2)
| a2a3 = a1a2
| a2 = X0 ),
inference(resolution,[],[f217,f96]) ).
fof(f438,plain,
! [X0] :
( ~ incident(X0,s2)
| ~ incident(X0,a1a2)
| a1a2 = s2
| a2 = X0 ),
inference(resolution,[],[f217,f110]) ).
fof(f443,definition,
( spl2_27
<=> point(a2) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f444,plain,
( point(a2)
| ~ spl2_27 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( ~ point(a2)
| spl2_27 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f455,definition,
( spl2_30
<=> a1a2 = s2 ),
introduced(definition,[new_symbols(definition,[spl2_30])],[avatar_definition]) ).
fof(f457,plain,
( a1a2 = s2
| ~ spl2_30 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl2_31
<=> ! [X0] :
( ~ incident(X0,s2)
| a2 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition]) ).
fof(f460,plain,
( ! [X0] :
( ~ incident(X0,s2)
| a2 = X0
| ~ incident(X0,a1a2) )
| ~ spl2_31 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( spl2_30
| spl2_31 ),
inference(avatar_split_clause,[],[f438,f459,f455]) ).
fof(f463,definition,
( spl2_32
<=> a2a3 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_32])],[avatar_definition]) ).
fof(f465,plain,
( a2a3 = a1a2
| ~ spl2_32 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f467,definition,
( spl2_33
<=> ! [X0] :
( ~ incident(X0,a2a3)
| a2 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f468,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| a2 = X0
| ~ incident(X0,a2a3) )
| ~ spl2_33 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f469,plain,
( spl2_32
| spl2_33 ),
inference(avatar_split_clause,[],[f437,f467,f463]) ).
fof(f470,plain,
( incident(a1,a2a3)
| ~ spl2_32 ),
inference(superposition,[],[f94,f465]) ).
fof(f479,plain,
( incident(s,a1a2)
| ~ spl2_30 ),
inference(superposition,[],[f107,f457]) ).
fof(f482,plain,
! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,a3a1)
| a2a3 = a3a1
| a3 = X0 ),
inference(resolution,[],[f219,f97]) ).
fof(f484,plain,
! [X0] :
( ~ incident(X0,s3)
| ~ incident(X0,a3a1)
| a3a1 = s3
| a3 = X0 ),
inference(resolution,[],[f219,f111]) ).
fof(f489,definition,
( spl2_34
<=> point(a3) ),
introduced(definition,[new_symbols(definition,[spl2_34])],[avatar_definition]) ).
fof(f490,plain,
( point(a3)
| ~ spl2_34 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( ~ point(a3)
| spl2_34 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f501,definition,
( spl2_37
<=> a3a1 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f502,plain,
( a3a1 != s3
| spl2_37 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f503,plain,
( a3a1 = s3
| ~ spl2_37 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f505,definition,
( spl2_38
<=> ! [X0] :
( ~ incident(X0,s3)
| a3 = X0
| ~ incident(X0,a3a1) ) ),
introduced(definition,[new_symbols(definition,[spl2_38])],[avatar_definition]) ).
fof(f506,plain,
( ! [X0] :
( ~ incident(X0,s3)
| a3 = X0
| ~ incident(X0,a3a1) )
| ~ spl2_38 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f507,plain,
( spl2_37
| spl2_38 ),
inference(avatar_split_clause,[],[f484,f505,f501]) ).
fof(f509,definition,
( spl2_39
<=> a2a3 = a3a1 ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f511,plain,
( a2a3 = a3a1
| ~ spl2_39 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f513,definition,
( spl2_40
<=> ! [X0] :
( ~ incident(X0,a2a3)
| a3 = X0
| ~ incident(X0,a3a1) ) ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f514,plain,
( ! [X0] :
( ~ incident(X0,a3a1)
| a3 = X0
| ~ incident(X0,a2a3) )
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( spl2_39
| spl2_40 ),
inference(avatar_split_clause,[],[f482,f513,f509]) ).
fof(f530,plain,
( ~ incident(a2,a2a3)
| ~ spl2_19
| ~ spl2_39 ),
inference(superposition,[],[f328,f511]) ).
fof(f532,plain,
( $false
| ~ spl2_19
| ~ spl2_39 ),
inference(forward_subsumption_resolution,[],[f530,f96]) ).
fof(f533,plain,
( ~ spl2_19
| ~ spl2_39 ),
inference(avatar_contradiction_clause,[],[f532]) ).
fof(f538,plain,
( incident(b3,a3a1)
| ~ spl2_37 ),
inference(superposition,[],[f114,f503]) ).
fof(f539,plain,
( incident(s,a3a1)
| ~ spl2_37 ),
inference(superposition,[],[f108,f503]) ).
fof(f540,plain,
( $false
| spl2_23
| ~ spl2_37 ),
inference(forward_subsumption_resolution,[],[f538,f322]) ).
fof(f541,plain,
( spl2_23
| ~ spl2_37 ),
inference(avatar_contradiction_clause,[],[f540]) ).
fof(f543,plain,
( incident(a3,b2b3)
| ~ spl2_25 ),
inference(superposition,[],[f98,f415]) ).
fof(f545,plain,
( incident(p2,b2b3)
| ~ spl2_25 ),
inference(superposition,[],[f119,f415]) ).
fof(f555,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,a1a2)
| b3b1 = a1a2
| a2 = X0 )
| ~ spl2_4 ),
inference(resolution,[],[f173,f217]) ).
fof(f564,definition,
( spl2_44
<=> b3b1 = a2a3 ),
introduced(definition,[new_symbols(definition,[spl2_44])],[avatar_definition]) ).
fof(f565,plain,
( b3b1 != a2a3
| spl2_44 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f566,plain,
( b3b1 = a2a3
| ~ spl2_44 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f569,plain,
( ! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,a1a2)
| b2b3 = a1a2
| a1 = X0 )
| ~ spl2_6 ),
inference(resolution,[],[f182,f216]) ).
fof(f576,plain,
( a1 = a3
| ~ incident(a1,a2a3)
| ~ spl2_40 ),
inference(resolution,[],[f514,f99]) ).
fof(f585,plain,
( ~ incident(a1,a2a3)
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f576,f154]) ).
fof(f591,definition,
( spl2_46
<=> p2 = a3 ),
introduced(definition,[new_symbols(definition,[spl2_46])],[avatar_definition]) ).
fof(f592,plain,
( p2 != a3
| spl2_46 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( p2 = a3
| ~ spl2_46 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f597,plain,
( $false
| ~ spl2_32
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f585,f470]) ).
fof(f598,plain,
( ~ spl2_32
| ~ spl2_40 ),
inference(avatar_contradiction_clause,[],[f597]) ).
fof(f602,definition,
( spl2_47
<=> b3b1 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_47])],[avatar_definition]) ).
fof(f604,plain,
( b3b1 = a1a2
| ~ spl2_47 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f606,definition,
( spl2_48
<=> ! [X0] :
( ~ incident(X0,b3b1)
| a2 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_48])],[avatar_definition]) ).
fof(f607,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| a2 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_48 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f608,plain,
( spl2_47
| spl2_48
| ~ spl2_4 ),
inference(avatar_split_clause,[],[f555,f171,f606,f602]) ).
fof(f610,definition,
( spl2_49
<=> b2b3 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_49])],[avatar_definition]) ).
fof(f612,plain,
( b2b3 = a1a2
| ~ spl2_49 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f614,definition,
( spl2_50
<=> ! [X0] :
( ~ incident(X0,b2b3)
| a1 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_50])],[avatar_definition]) ).
fof(f615,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| a1 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_50 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f616,plain,
( spl2_49
| spl2_50
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f569,f180,f614,f610]) ).
fof(f622,definition,
( spl2_52
<=> a3 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_52])],[avatar_definition]) ).
fof(f624,plain,
( a3 = b2
| ~ spl2_52 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f630,plain,
( a1 = a2
| ~ incident(a2,b2b3)
| ~ spl2_50 ),
inference(resolution,[],[f615,f95]) ).
fof(f647,definition,
( spl2_54
<=> p3 = a2 ),
introduced(definition,[new_symbols(definition,[spl2_54])],[avatar_definition]) ).
fof(f648,plain,
( p3 != a2
| spl2_54 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f649,plain,
( p3 = a2
| ~ spl2_54 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f654,plain,
! [X0] :
( ~ incident(X0,s2)
| ~ incident(X0,b1b2)
| b1b2 = s2
| b2 = X0 ),
inference(resolution,[],[f223,f113]) ).
fof(f670,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| b1b2 = s2
| b2 = X0 )
| ~ spl2_30 ),
inference(forward_demodulation,[],[f654,f457]) ).
fof(f680,plain,
( ! [X0] :
( b1b2 = a1a2
| ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| b2 = X0 )
| ~ spl2_30 ),
inference(forward_demodulation,[],[f670,f457]) ).
fof(f682,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| b2 = X0 )
| ~ spl2_30 ),
inference(forward_subsumption_resolution,[],[f680,f150]) ).
fof(f694,plain,
! [X0] :
( ~ incident(X0,s2)
| ~ incident(X0,a2a3)
| a2a3 = s2
| a2 = X0 ),
inference(resolution,[],[f218,f110]) ).
fof(f701,plain,
! [X0] :
( ~ incident(X0,s3)
| ~ incident(X0,a2a3)
| a2a3 = s3
| a3 = X0 ),
inference(resolution,[],[f220,f111]) ).
fof(f708,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,b1b2)
| b1b2 = a2a3
| b1 = X0 )
| ~ spl2_3 ),
inference(resolution,[],[f221,f169]) ).
fof(f709,plain,
! [X0] :
( ~ incident(X0,s1)
| ~ incident(X0,b1b2)
| b1b2 = s1
| b1 = X0 ),
inference(resolution,[],[f221,f112]) ).
fof(f725,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| b1b2 = s1
| b1 = X0 )
| ~ spl2_16 ),
inference(forward_demodulation,[],[f709,f278]) ).
fof(f727,definition,
( spl2_63
<=> b1b2 = a2a3 ),
introduced(definition,[new_symbols(definition,[spl2_63])],[avatar_definition]) ).
fof(f728,plain,
( b1b2 != a2a3
| spl2_63 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( b1b2 = a2a3
| ~ spl2_63 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f731,definition,
( spl2_64
<=> ! [X0] :
( ~ incident(X0,a2a3)
| b1 = X0
| ~ incident(X0,b1b2) ) ),
introduced(definition,[new_symbols(definition,[spl2_64])],[avatar_definition]) ).
fof(f732,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| b1 = X0
| ~ incident(X0,b1b2) )
| ~ spl2_64 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f733,plain,
( spl2_63
| spl2_64
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f708,f167,f731,f727]) ).
fof(f742,plain,
( ! [X0] :
( b1b2 = a1a2
| ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| b1 = X0 )
| ~ spl2_16 ),
inference(forward_demodulation,[],[f725,f278]) ).
fof(f743,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| b1 = X0 )
| ~ spl2_16 ),
inference(forward_subsumption_resolution,[],[f742,f150]) ).
fof(f755,plain,
( a3 = b1
| ~ incident(a3,b1b2)
| ~ spl2_64 ),
inference(resolution,[],[f732,f97]) ).
fof(f767,plain,
! [X0] :
( ~ incident(X0,s3)
| ~ incident(X0,b3b1)
| b3b1 = s3
| b3 = X0 ),
inference(resolution,[],[f226,f114]) ).
fof(f788,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,b3b1)
| b3b1 = a2a3
| b1 = X0 )
| ~ spl2_3 ),
inference(resolution,[],[f222,f169]) ).
fof(f789,plain,
! [X0] :
( ~ incident(X0,s1)
| ~ incident(X0,b3b1)
| b3b1 = s1
| b1 = X0 ),
inference(resolution,[],[f222,f112]) ).
fof(f795,definition,
( spl2_70
<=> ! [X0] :
( ~ incident(X0,a2a3)
| b1 = X0
| ~ incident(X0,b3b1) ) ),
introduced(definition,[new_symbols(definition,[spl2_70])],[avatar_definition]) ).
fof(f796,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| b1 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_70 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f797,plain,
( spl2_44
| spl2_70
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f788,f167,f795,f564]) ).
fof(f805,plain,
( a3 = b1
| ~ incident(a3,b3b1)
| ~ spl2_70 ),
inference(resolution,[],[f796,f97]) ).
fof(f810,definition,
( spl2_72
<=> incident(a3,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_72])],[avatar_definition]) ).
fof(f811,plain,
( incident(a3,b3b1)
| ~ spl2_72 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f812,plain,
( ~ incident(a3,b3b1)
| spl2_72 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f814,definition,
( spl2_73
<=> a3 = b1 ),
introduced(definition,[new_symbols(definition,[spl2_73])],[avatar_definition]) ).
fof(f815,plain,
( a3 != b1
| spl2_73 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f816,plain,
( a3 = b1
| ~ spl2_73 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f817,plain,
( ~ spl2_72
| spl2_73
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f805,f795,f814,f810]) ).
fof(f821,plain,
! [X0] :
( ~ incident(X0,s2)
| ~ incident(X0,b2b3)
| b2b3 = s2
| b2 = X0 ),
inference(resolution,[],[f224,f113]) ).
fof(f832,plain,
! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,b2b3)
| b2b3 = b3b1
| b3 = X0 ),
inference(resolution,[],[f225,f104]) ).
fof(f833,plain,
! [X0] :
( ~ incident(X0,s3)
| ~ incident(X0,b2b3)
| b2b3 = s3
| b3 = X0 ),
inference(resolution,[],[f225,f114]) ).
fof(f841,plain,
! [X0] :
( ~ incident(X0,b1b2)
| ~ incident(X0,a1a2)
| b1b2 = a1a2
| p3 = X0 ),
inference(resolution,[],[f210,f116]) ).
fof(f848,definition,
( spl2_75
<=> point(p3) ),
introduced(definition,[new_symbols(definition,[spl2_75])],[avatar_definition]) ).
fof(f849,plain,
( point(p3)
| ~ spl2_75 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f850,plain,
( ~ point(p3)
| spl2_75 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f863,plain,
! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| p3 = X0 ),
inference(forward_subsumption_resolution,[],[f841,f150]) ).
fof(f874,definition,
( spl2_79
<=> incident(a1,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_79])],[avatar_definition]) ).
fof(f875,plain,
( incident(a1,b3b1)
| ~ spl2_79 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f876,plain,
( ~ incident(a1,b3b1)
| spl2_79 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f878,definition,
( spl2_80
<=> p3 = a1 ),
introduced(definition,[new_symbols(definition,[spl2_80])],[avatar_definition]) ).
fof(f879,plain,
( p3 != a1
| spl2_80 ),
inference(avatar_component_clause,[],[f878]) ).
fof(f880,plain,
( p3 = a1
| ~ spl2_80 ),
inference(avatar_component_clause,[],[f878]) ).
fof(f891,plain,
! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,a3a1)
| b3b1 = a3a1
| p2 = X0 ),
inference(resolution,[],[f213,f120]) ).
fof(f895,plain,
! [X0] :
( ~ incident(X0,a3a1)
| ~ incident(X0,b3b1)
| p2 = X0 ),
inference(forward_subsumption_resolution,[],[f891,f148]) ).
fof(f896,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,b2b3)
| p2 = X0 )
| ~ spl2_25 ),
inference(forward_demodulation,[],[f895,f415]) ).
fof(f900,plain,
( ~ incident(b3,b2b3)
| p2 = b3
| ~ spl2_25 ),
inference(resolution,[],[f896,f104]) ).
fof(f905,plain,
( p2 = b3
| ~ spl2_25 ),
inference(forward_subsumption_resolution,[],[f900,f103]) ).
fof(f908,plain,
( incident(b3,a3a1)
| ~ spl2_25 ),
inference(superposition,[],[f119,f905]) ).
fof(f920,plain,
! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,a2a3)
| b2b3 = a2a3
| p1 = X0 ),
inference(resolution,[],[f212,f118]) ).
fof(f926,definition,
( spl2_81
<=> point(p1) ),
introduced(definition,[new_symbols(definition,[spl2_81])],[avatar_definition]) ).
fof(f927,plain,
( point(p1)
| ~ spl2_81 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f928,plain,
( ~ point(p1)
| spl2_81 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f937,plain,
! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,b2b3)
| p1 = X0 ),
inference(forward_subsumption_resolution,[],[f920,f149]) ).
fof(f939,plain,
( ~ incident(a2,b2b3)
| p1 = a2 ),
inference(resolution,[],[f937,f96]) ).
fof(f940,plain,
( ~ incident(a3,b2b3)
| p1 = a3 ),
inference(resolution,[],[f937,f97]) ).
fof(f946,plain,
( p1 = a3
| ~ spl2_25 ),
inference(forward_subsumption_resolution,[],[f940,f543]) ).
fof(f953,plain,
point(p3),
inference(resolution,[],[f121,f116]) ).
fof(f956,plain,
point(p1),
inference(resolution,[],[f121,f118]) ).
fof(f958,plain,
point(p2),
inference(resolution,[],[f121,f119]) ).
fof(f961,plain,
point(a1),
inference(resolution,[],[f121,f99]) ).
fof(f964,plain,
point(a2),
inference(resolution,[],[f121,f96]) ).
fof(f967,plain,
point(a3),
inference(resolution,[],[f121,f97]) ).
fof(f1012,plain,
( $false
| spl2_34 ),
inference(forward_subsumption_resolution,[],[f967,f491]) ).
fof(f1013,plain,
spl2_34,
inference(avatar_contradiction_clause,[],[f1012]) ).
fof(f1018,plain,
( $false
| spl2_27 ),
inference(forward_subsumption_resolution,[],[f964,f445]) ).
fof(f1019,plain,
spl2_27,
inference(avatar_contradiction_clause,[],[f1018]) ).
fof(f1024,plain,
( $false
| spl2_13 ),
inference(forward_subsumption_resolution,[],[f961,f266]) ).
fof(f1025,plain,
spl2_13,
inference(avatar_contradiction_clause,[],[f1024]) ).
fof(f1030,plain,
( $false
| spl2_11 ),
inference(forward_subsumption_resolution,[],[f958,f240]) ).
fof(f1031,plain,
spl2_11,
inference(avatar_contradiction_clause,[],[f1030]) ).
fof(f1034,plain,
( $false
| spl2_81 ),
inference(forward_subsumption_resolution,[],[f956,f928]) ).
fof(f1035,plain,
spl2_81,
inference(avatar_contradiction_clause,[],[f1034]) ).
fof(f1040,plain,
( $false
| spl2_75 ),
inference(forward_subsumption_resolution,[],[f953,f850]) ).
fof(f1041,plain,
spl2_75,
inference(avatar_contradiction_clause,[],[f1040]) ).
fof(f1043,plain,
( ! [X0] :
( ~ incident(p3,sK0(X0,b3))
| ~ point(X0)
| ~ incident(p1,sK0(X0,p2)) )
| ~ spl2_12
| ~ spl2_25 ),
inference(forward_demodulation,[],[f243,f905]) ).
fof(f1076,plain,
( ! [X0] :
( ~ incident(p1,sK0(X0,b3))
| ~ incident(p3,sK0(X0,b3))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_25 ),
inference(forward_demodulation,[],[f1043,f905]) ).
fof(f1094,plain,
( ! [X0] :
( ~ incident(a3,sK0(X0,b3))
| ~ incident(p3,sK0(X0,b3))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_25 ),
inference(forward_demodulation,[],[f1076,f946]) ).
fof(f1193,plain,
( ~ incident(p3,b1b2)
| p3 = b1
| ~ spl2_16 ),
inference(resolution,[],[f743,f115]) ).
fof(f1202,plain,
( p3 = b1
| ~ spl2_16 ),
inference(forward_subsumption_resolution,[],[f1193,f116]) ).
fof(f1233,plain,
( ~ incident(p3,b1b2)
| p3 = b2
| ~ spl2_30 ),
inference(resolution,[],[f682,f115]) ).
fof(f1242,plain,
( p3 = b2
| ~ spl2_30 ),
inference(forward_subsumption_resolution,[],[f1233,f116]) ).
fof(f1245,plain,
( b1 = b2
| ~ spl2_16
| ~ spl2_30 ),
inference(forward_demodulation,[],[f1242,f1202]) ).
fof(f1246,plain,
( $false
| ~ spl2_16
| ~ spl2_30 ),
inference(forward_subsumption_resolution,[],[f1245,f153]) ).
fof(f1247,plain,
( ~ spl2_16
| ~ spl2_30 ),
inference(avatar_contradiction_clause,[],[f1246]) ).
fof(f1250,definition,
( spl2_84
<=> a2a3 = s2 ),
introduced(definition,[new_symbols(definition,[spl2_84])],[avatar_definition]) ).
fof(f1252,plain,
( a2a3 = s2
| ~ spl2_84 ),
inference(avatar_component_clause,[],[f1250]) ).
fof(f1254,definition,
( spl2_85
<=> ! [X0] :
( ~ incident(X0,s2)
| a2 = X0
| ~ incident(X0,a2a3) ) ),
introduced(definition,[new_symbols(definition,[spl2_85])],[avatar_definition]) ).
fof(f1255,plain,
( ! [X0] :
( ~ incident(X0,s2)
| a2 = X0
| ~ incident(X0,a2a3) )
| ~ spl2_85 ),
inference(avatar_component_clause,[],[f1254]) ).
fof(f1256,plain,
( spl2_84
| spl2_85 ),
inference(avatar_split_clause,[],[f694,f1254,f1250]) ).
fof(f1258,definition,
( spl2_86
<=> b2b3 = s2 ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
fof(f1260,plain,
( b2b3 = s2
| ~ spl2_86 ),
inference(avatar_component_clause,[],[f1258]) ).
fof(f1262,definition,
( spl2_87
<=> ! [X0] :
( ~ incident(X0,s2)
| b2 = X0
| ~ incident(X0,b2b3) ) ),
introduced(definition,[new_symbols(definition,[spl2_87])],[avatar_definition]) ).
fof(f1263,plain,
( ! [X0] :
( ~ incident(X0,s2)
| b2 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_87 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1264,plain,
( spl2_86
| spl2_87 ),
inference(avatar_split_clause,[],[f821,f1262,f1258]) ).
fof(f1295,plain,
( incident(a2,b2b3)
| ~ spl2_86 ),
inference(superposition,[],[f110,f1260]) ).
fof(f1297,plain,
( incident(s,b2b3)
| ~ spl2_86 ),
inference(superposition,[],[f107,f1260]) ).
fof(f1300,plain,
( ~ incident(a2,b2b3)
| ~ spl2_50 ),
inference(forward_subsumption_resolution,[],[f630,f156]) ).
fof(f1305,definition,
( spl2_91
<=> b2b3 = b3b1 ),
introduced(definition,[new_symbols(definition,[spl2_91])],[avatar_definition]) ).
fof(f1307,plain,
( b2b3 = b3b1
| ~ spl2_91 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1309,definition,
( spl2_92
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b3 = X0
| ~ incident(X0,b3b1) ) ),
introduced(definition,[new_symbols(definition,[spl2_92])],[avatar_definition]) ).
fof(f1310,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| b3 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_92 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1314,plain,
( spl2_91
| spl2_92 ),
inference(avatar_split_clause,[],[f832,f1309,f1305]) ).
fof(f1317,definition,
( spl2_93
<=> p1 = a3 ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
fof(f1319,plain,
( p1 = a3
| ~ spl2_93 ),
inference(avatar_component_clause,[],[f1317]) ).
fof(f1321,definition,
( spl2_94
<=> incident(a3,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_94])],[avatar_definition]) ).
fof(f1322,plain,
( incident(a3,b2b3)
| ~ spl2_94 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1323,plain,
( ~ incident(a3,b2b3)
| spl2_94 ),
inference(avatar_component_clause,[],[f1321]) ).
fof(f1324,plain,
( spl2_93
| ~ spl2_94 ),
inference(avatar_split_clause,[],[f940,f1321,f1317]) ).
fof(f1326,definition,
( spl2_95
<=> p1 = a2 ),
introduced(definition,[new_symbols(definition,[spl2_95])],[avatar_definition]) ).
fof(f1328,plain,
( p1 = a2
| ~ spl2_95 ),
inference(avatar_component_clause,[],[f1326]) ).
fof(f1330,definition,
( spl2_96
<=> incident(a2,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_96])],[avatar_definition]) ).
fof(f1331,plain,
( incident(a2,b2b3)
| ~ spl2_96 ),
inference(avatar_component_clause,[],[f1330]) ).
fof(f1332,plain,
( ~ incident(a2,b2b3)
| spl2_96 ),
inference(avatar_component_clause,[],[f1330]) ).
fof(f1333,plain,
( spl2_95
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f939,f1330,f1326]) ).
fof(f1348,plain,
( spl2_96
| ~ spl2_86 ),
inference(avatar_split_clause,[],[f1295,f1258,f1330]) ).
fof(f1349,plain,
( ~ spl2_96
| ~ spl2_50 ),
inference(avatar_split_clause,[],[f1300,f614,f1330]) ).
fof(f1374,plain,
( ~ incident(a1,b3b1)
| p2 = a1 ),
inference(resolution,[],[f895,f99]) ).
fof(f1375,plain,
( ~ incident(a3,b3b1)
| p2 = a3 ),
inference(resolution,[],[f895,f98]) ).
fof(f1393,plain,
( ~ incident(a1,b2b3)
| spl2_79
| ~ spl2_91 ),
inference(superposition,[],[f876,f1307]) ).
fof(f1394,plain,
( $false
| ~ spl2_6
| spl2_79
| ~ spl2_91 ),
inference(forward_subsumption_resolution,[],[f1393,f182]) ).
fof(f1395,plain,
( ~ spl2_6
| spl2_79
| ~ spl2_91 ),
inference(avatar_contradiction_clause,[],[f1394]) ).
fof(f1487,plain,
( ~ incident(b1,b3b1)
| spl2_9
| ~ spl2_16 ),
inference(forward_demodulation,[],[f203,f1202]) ).
fof(f1513,plain,
( $false
| spl2_9
| ~ spl2_16 ),
inference(forward_subsumption_resolution,[],[f1487,f105]) ).
fof(f1514,plain,
( spl2_9
| ~ spl2_16 ),
inference(avatar_contradiction_clause,[],[f1513]) ).
fof(f1541,plain,
( ! [X0] :
( ~ incident(a2,sK0(X0,p2))
| ~ point(X0)
| ~ incident(p3,sK0(X0,p2)) )
| ~ spl2_12
| ~ spl2_95 ),
inference(forward_demodulation,[],[f243,f1328]) ).
fof(f1555,definition,
( spl2_101
<=> b3b1 = s1 ),
introduced(definition,[new_symbols(definition,[spl2_101])],[avatar_definition]) ).
fof(f1557,plain,
( b3b1 = s1
| ~ spl2_101 ),
inference(avatar_component_clause,[],[f1555]) ).
fof(f1588,plain,
( a2 = a3
| ~ spl2_93
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1319,f1328]) ).
fof(f1591,plain,
( $false
| ~ spl2_93
| ~ spl2_95 ),
inference(forward_subsumption_resolution,[],[f1588,f155]) ).
fof(f1592,plain,
( ~ spl2_93
| ~ spl2_95 ),
inference(avatar_contradiction_clause,[],[f1591]) ).
fof(f1596,definition,
( spl2_104
<=> ! [X0] :
( ~ incident(X0,s1)
| b1 = X0
| ~ incident(X0,b3b1) ) ),
introduced(definition,[new_symbols(definition,[spl2_104])],[avatar_definition]) ).
fof(f1597,plain,
( ! [X0] :
( ~ incident(X0,s1)
| b1 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_104 ),
inference(avatar_component_clause,[],[f1596]) ).
fof(f1598,plain,
( spl2_101
| spl2_104 ),
inference(avatar_split_clause,[],[f789,f1596,f1555]) ).
fof(f1665,plain,
( ~ incident(b1,b3b1)
| spl2_3
| ~ spl2_44 ),
inference(forward_demodulation,[],[f168,f566]) ).
fof(f1668,plain,
( $false
| spl2_3
| ~ spl2_44 ),
inference(forward_subsumption_resolution,[],[f1665,f105]) ).
fof(f1669,plain,
( spl2_3
| ~ spl2_44 ),
inference(avatar_contradiction_clause,[],[f1668]) ).
fof(f1671,plain,
( ~ incident(b3,b2b3)
| spl2_5
| ~ spl2_49 ),
inference(forward_demodulation,[],[f177,f612]) ).
fof(f1672,plain,
( $false
| spl2_5
| ~ spl2_49 ),
inference(forward_subsumption_resolution,[],[f1671,f103]) ).
fof(f1673,plain,
( spl2_5
| ~ spl2_49 ),
inference(avatar_contradiction_clause,[],[f1672]) ).
fof(f1687,plain,
( ~ incident(a1,a1a2)
| spl2_5
| ~ spl2_24 ),
inference(forward_demodulation,[],[f177,f326]) ).
fof(f1692,plain,
( $false
| spl2_5
| ~ spl2_24 ),
inference(forward_subsumption_resolution,[],[f1687,f94]) ).
fof(f1693,plain,
( spl2_5
| ~ spl2_24 ),
inference(avatar_contradiction_clause,[],[f1692]) ).
fof(f1718,plain,
( ! [X0] :
( ~ incident(a2,sK0(X0,p2))
| ~ incident(a2,sK0(X0,p2))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_54
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1541,f649]) ).
fof(f1719,plain,
( ! [X0] :
( ~ incident(a2,sK0(X0,p2))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_54
| ~ spl2_95 ),
inference(duplicate_literal_removal,[],[f1718]) ).
fof(f1724,definition,
( spl2_112
<=> a2a3 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_112])],[avatar_definition]) ).
fof(f1725,plain,
( a2a3 != s3
| spl2_112 ),
inference(avatar_component_clause,[],[f1724]) ).
fof(f1726,plain,
( a2a3 = s3
| ~ spl2_112 ),
inference(avatar_component_clause,[],[f1724]) ).
fof(f1728,definition,
( spl2_113
<=> ! [X0] :
( ~ incident(X0,s3)
| a3 = X0
| ~ incident(X0,a2a3) ) ),
introduced(definition,[new_symbols(definition,[spl2_113])],[avatar_definition]) ).
fof(f1729,plain,
( ! [X0] :
( ~ incident(X0,s3)
| a3 = X0
| ~ incident(X0,a2a3) )
| ~ spl2_113 ),
inference(avatar_component_clause,[],[f1728]) ).
fof(f1730,plain,
( spl2_112
| spl2_113 ),
inference(avatar_split_clause,[],[f701,f1728,f1724]) ).
fof(f1732,definition,
( spl2_114
<=> b3b1 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_114])],[avatar_definition]) ).
fof(f1734,plain,
( b3b1 = s3
| ~ spl2_114 ),
inference(avatar_component_clause,[],[f1732]) ).
fof(f1736,definition,
( spl2_115
<=> ! [X0] :
( ~ incident(X0,s3)
| b3 = X0
| ~ incident(X0,b3b1) ) ),
introduced(definition,[new_symbols(definition,[spl2_115])],[avatar_definition]) ).
fof(f1737,plain,
( ! [X0] :
( ~ incident(X0,s3)
| b3 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_115 ),
inference(avatar_component_clause,[],[f1736]) ).
fof(f1738,plain,
( spl2_114
| spl2_115 ),
inference(avatar_split_clause,[],[f767,f1736,f1732]) ).
fof(f1740,definition,
( spl2_116
<=> b2b3 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_116])],[avatar_definition]) ).
fof(f1742,plain,
( b2b3 = s3
| ~ spl2_116 ),
inference(avatar_component_clause,[],[f1740]) ).
fof(f1744,definition,
( spl2_117
<=> ! [X0] :
( ~ incident(X0,s3)
| b3 = X0
| ~ incident(X0,b2b3) ) ),
introduced(definition,[new_symbols(definition,[spl2_117])],[avatar_definition]) ).
fof(f1745,plain,
( ! [X0] :
( ~ incident(X0,s3)
| b3 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_117 ),
inference(avatar_component_clause,[],[f1744]) ).
fof(f1746,plain,
( spl2_116
| spl2_117 ),
inference(avatar_split_clause,[],[f833,f1744,f1740]) ).
fof(f1767,plain,
( ~ point(a2)
| ~ point(a2)
| ~ point(p2)
| ~ spl2_12
| ~ spl2_54
| ~ spl2_95 ),
inference(resolution,[],[f1719,f139]) ).
fof(f1768,plain,
( ~ point(a2)
| ~ point(p2)
| ~ spl2_12
| ~ spl2_54
| ~ spl2_95 ),
inference(duplicate_literal_removal,[],[f1767]) ).
fof(f1769,plain,
( ~ point(p2)
| ~ spl2_12
| ~ spl2_27
| ~ spl2_54
| ~ spl2_95 ),
inference(forward_subsumption_resolution,[],[f1768,f444]) ).
fof(f1770,plain,
( $false
| ~ spl2_11
| ~ spl2_12
| ~ spl2_27
| ~ spl2_54
| ~ spl2_95 ),
inference(forward_subsumption_resolution,[],[f1769,f239]) ).
fof(f1771,plain,
( ~ spl2_11
| ~ spl2_12
| ~ spl2_27
| ~ spl2_54
| ~ spl2_95 ),
inference(avatar_contradiction_clause,[],[f1770]) ).
fof(f1780,definition,
( spl2_120
<=> a2 = b1 ),
introduced(definition,[new_symbols(definition,[spl2_120])],[avatar_definition]) ).
fof(f1782,plain,
( a2 = b1
| ~ spl2_120 ),
inference(avatar_component_clause,[],[f1780]) ).
fof(f1799,plain,
( incident(a3,b3b1)
| ~ spl2_73 ),
inference(superposition,[],[f105,f816]) ).
fof(f1804,plain,
( $false
| spl2_72
| ~ spl2_73 ),
inference(forward_subsumption_resolution,[],[f1799,f812]) ).
fof(f1805,plain,
( spl2_72
| ~ spl2_73 ),
inference(avatar_contradiction_clause,[],[f1804]) ).
fof(f1808,plain,
( p2 = a3
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f1375,f811]) ).
fof(f1809,plain,
( spl2_46
| ~ spl2_72 ),
inference(avatar_split_clause,[],[f1808,f810,f591]) ).
fof(f1831,plain,
( a2 = b3
| ~ incident(b3,a2a3)
| ~ spl2_5
| ~ spl2_33 ),
inference(resolution,[],[f178,f468]) ).
fof(f1877,definition,
( spl2_121
<=> incident(b3,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_121])],[avatar_definition]) ).
fof(f1881,definition,
( spl2_122
<=> a2 = b3 ),
introduced(definition,[new_symbols(definition,[spl2_122])],[avatar_definition]) ).
fof(f1883,plain,
( a2 = b3
| ~ spl2_122 ),
inference(avatar_component_clause,[],[f1881]) ).
fof(f1884,plain,
( ~ spl2_121
| spl2_122
| ~ spl2_5
| ~ spl2_33 ),
inference(avatar_split_clause,[],[f1831,f467,f176,f1881,f1877]) ).
fof(f1942,plain,
( incident(a3,b2b3)
| ~ spl2_93 ),
inference(superposition,[],[f118,f1319]) ).
fof(f1950,plain,
( incident(a1,b3b1)
| ~ spl2_47 ),
inference(superposition,[],[f94,f604]) ).
fof(f1952,plain,
( incident(p3,b3b1)
| ~ spl2_47 ),
inference(superposition,[],[f115,f604]) ).
fof(f1963,plain,
( p2 = a1
| ~ spl2_79 ),
inference(forward_subsumption_resolution,[],[f1374,f875]) ).
fof(f1964,plain,
( a1 = a3
| ~ spl2_46
| ~ spl2_79 ),
inference(forward_demodulation,[],[f1963,f593]) ).
fof(f1965,plain,
( $false
| ~ spl2_46
| ~ spl2_79 ),
inference(forward_subsumption_resolution,[],[f1964,f154]) ).
fof(f1966,plain,
( ~ spl2_46
| ~ spl2_79 ),
inference(avatar_contradiction_clause,[],[f1965]) ).
fof(f1989,plain,
( a1 = a3
| ~ incident(a3,b2b3)
| ~ spl2_26 ),
inference(resolution,[],[f418,f98]) ).
fof(f1994,plain,
( ~ incident(a3,b2b3)
| ~ spl2_26 ),
inference(forward_subsumption_resolution,[],[f1989,f154]) ).
fof(f2003,plain,
( a1 = a2
| ~ incident(a1,b3b1)
| ~ spl2_48 ),
inference(resolution,[],[f607,f94]) ).
fof(f2005,plain,
( a2 = b3
| ~ incident(b3,b3b1)
| ~ spl2_5
| ~ spl2_48 ),
inference(resolution,[],[f607,f178]) ).
fof(f2057,plain,
( a1 = b1
| ~ incident(b1,a1a2)
| ~ spl2_17 ),
inference(resolution,[],[f281,f112]) ).
fof(f2058,plain,
( a1 = s
| ~ incident(s,a1a2)
| ~ spl2_17 ),
inference(resolution,[],[f281,f106]) ).
fof(f2064,plain,
( ~ incident(b1,b3b1)
| a1 = b1
| ~ spl2_17
| ~ spl2_47 ),
inference(forward_demodulation,[],[f2057,f604]) ).
fof(f2068,definition,
( spl2_123
<=> a1 = s ),
introduced(definition,[new_symbols(definition,[spl2_123])],[avatar_definition]) ).
fof(f2069,plain,
( a1 != s
| spl2_123 ),
inference(avatar_component_clause,[],[f2068]) ).
fof(f2070,plain,
( a1 = s
| ~ spl2_123 ),
inference(avatar_component_clause,[],[f2068]) ).
fof(f2072,definition,
( spl2_124
<=> incident(s,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_124])],[avatar_definition]) ).
fof(f2073,plain,
( incident(s,b3b1)
| ~ spl2_124 ),
inference(avatar_component_clause,[],[f2072]) ).
fof(f2076,plain,
( a1 = b1
| ~ spl2_17
| ~ spl2_47 ),
inference(forward_subsumption_resolution,[],[f2064,f105]) ).
fof(f2077,plain,
( incident(a1,b1b2)
| ~ spl2_17
| ~ spl2_47 ),
inference(superposition,[],[f100,f2076]) ).
fof(f2089,plain,
( incident(s,b3b1)
| ~ spl2_16
| ~ spl2_47 ),
inference(forward_demodulation,[],[f300,f604]) ).
fof(f2110,plain,
( $false
| spl2_23
| ~ spl2_25 ),
inference(forward_subsumption_resolution,[],[f908,f322]) ).
fof(f2111,plain,
( spl2_23
| ~ spl2_25 ),
inference(avatar_contradiction_clause,[],[f2110]) ).
fof(f2141,plain,
( ~ incident(b3,b3b1)
| spl2_5
| ~ spl2_47 ),
inference(forward_demodulation,[],[f177,f604]) ).
fof(f2147,plain,
( $false
| spl2_5
| ~ spl2_47 ),
inference(forward_subsumption_resolution,[],[f2141,f104]) ).
fof(f2148,plain,
( spl2_5
| ~ spl2_47 ),
inference(avatar_contradiction_clause,[],[f2147]) ).
fof(f2154,plain,
( ~ incident(a1,b3b1)
| ~ spl2_48 ),
inference(forward_subsumption_resolution,[],[f2003,f156]) ).
fof(f2165,definition,
( spl2_127
<=> incident(s,a1a2) ),
introduced(definition,[new_symbols(definition,[spl2_127])],[avatar_definition]) ).
fof(f2168,plain,
( ~ spl2_127
| spl2_123
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f2058,f280,f2068,f2165]) ).
fof(f2173,definition,
( spl2_128
<=> incident(p2,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_128])],[avatar_definition]) ).
fof(f2174,plain,
( incident(p2,b2b3)
| ~ spl2_128 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2177,definition,
( spl2_129
<=> p2 = a1 ),
introduced(definition,[new_symbols(definition,[spl2_129])],[avatar_definition]) ).
fof(f2179,plain,
( p2 = a1
| ~ spl2_129 ),
inference(avatar_component_clause,[],[f2177]) ).
fof(f2184,plain,
( ~ incident(a1,a3a1)
| spl2_7
| ~ spl2_80 ),
inference(superposition,[],[f193,f880]) ).
fof(f2189,plain,
( $false
| spl2_7
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f2184,f99]) ).
fof(f2190,plain,
( spl2_7
| ~ spl2_80 ),
inference(avatar_contradiction_clause,[],[f2189]) ).
fof(f2210,plain,
( a1 = b2
| ~ incident(b2,b2b3)
| ~ spl2_1
| ~ spl2_26 ),
inference(resolution,[],[f418,f160]) ).
fof(f2215,plain,
( a1 = b2
| ~ spl2_1
| ~ spl2_26 ),
inference(forward_subsumption_resolution,[],[f2210,f102]) ).
fof(f2231,plain,
( a1 = s
| ~ incident(s,a1a2)
| ~ spl2_17 ),
inference(resolution,[],[f281,f106]) ).
fof(f2249,plain,
( p2 = b3
| ~ incident(p2,b2b3)
| ~ spl2_92 ),
inference(resolution,[],[f1310,f120]) ).
fof(f2263,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| a1 = X0 )
| ~ spl2_80 ),
inference(forward_demodulation,[],[f863,f880]) ).
fof(f2268,definition,
( spl2_131
<=> b1b2 = s1 ),
introduced(definition,[new_symbols(definition,[spl2_131])],[avatar_definition]) ).
fof(f2270,plain,
( b1b2 = s1
| ~ spl2_131 ),
inference(avatar_component_clause,[],[f2268]) ).
fof(f2272,definition,
( spl2_132
<=> ! [X0] :
( ~ incident(X0,s1)
| b1 = X0
| ~ incident(X0,b1b2) ) ),
introduced(definition,[new_symbols(definition,[spl2_132])],[avatar_definition]) ).
fof(f2273,plain,
( ! [X0] :
( ~ incident(X0,s1)
| b1 = X0
| ~ incident(X0,b1b2) )
| ~ spl2_132 ),
inference(avatar_component_clause,[],[f2272]) ).
fof(f2274,plain,
( spl2_131
| spl2_132 ),
inference(avatar_split_clause,[],[f709,f2272,f2268]) ).
fof(f2298,plain,
( ~ incident(a2,b1b2)
| a1 = a2
| ~ spl2_80 ),
inference(resolution,[],[f2263,f95]) ).
fof(f2303,plain,
( ~ incident(a2,b1b2)
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f2298,f156]) ).
fof(f2306,plain,
( incident(a1,b1b2)
| ~ spl2_131 ),
inference(superposition,[],[f109,f2270]) ).
fof(f2333,plain,
( a2 = b2
| ~ incident(b2,a1a2)
| ~ spl2_31 ),
inference(resolution,[],[f460,f113]) ).
fof(f2334,plain,
( a2 = s
| ~ incident(s,a1a2)
| ~ spl2_31 ),
inference(resolution,[],[f460,f107]) ).
fof(f2341,plain,
( a1 = a2
| ~ incident(b2,a1a2)
| ~ spl2_1
| ~ spl2_26
| ~ spl2_31 ),
inference(forward_demodulation,[],[f2333,f2215]) ).
fof(f2344,plain,
( ~ incident(b2,a1a2)
| ~ spl2_1
| ~ spl2_26
| ~ spl2_31 ),
inference(forward_subsumption_resolution,[],[f2341,f156]) ).
fof(f2347,plain,
( ~ incident(a1,a1a2)
| ~ spl2_1
| ~ spl2_26
| ~ spl2_31 ),
inference(forward_demodulation,[],[f2344,f2215]) ).
fof(f2350,plain,
( $false
| ~ spl2_1
| ~ spl2_26
| ~ spl2_31 ),
inference(forward_subsumption_resolution,[],[f2347,f94]) ).
fof(f2351,plain,
( ~ spl2_1
| ~ spl2_26
| ~ spl2_31 ),
inference(avatar_contradiction_clause,[],[f2350]) ).
fof(f2408,plain,
( a3 = b3
| ~ incident(b3,a3a1)
| ~ spl2_38 ),
inference(resolution,[],[f506,f114]) ).
fof(f2442,plain,
( a3 = s
| ~ incident(s,a2a3)
| ~ spl2_113 ),
inference(resolution,[],[f1729,f108]) ).
fof(f2472,plain,
( b1 = s
| ~ incident(s,b1b2)
| ~ spl2_132 ),
inference(resolution,[],[f2273,f106]) ).
fof(f2541,plain,
( ~ incident(a1,b1b2)
| p3 = a1 ),
inference(resolution,[],[f863,f94]) ).
fof(f2542,plain,
( ~ incident(a2,b1b2)
| p3 = a2 ),
inference(resolution,[],[f863,f95]) ).
fof(f2566,plain,
( a3 = b3
| ~ incident(a3,b3b1)
| ~ spl2_115 ),
inference(resolution,[],[f1737,f111]) ).
fof(f2568,plain,
( b3 = s
| ~ incident(s,b3b1)
| ~ spl2_115 ),
inference(resolution,[],[f1737,f108]) ).
fof(f2579,plain,
( b1 = s
| ~ incident(s,b3b1)
| ~ spl2_104 ),
inference(resolution,[],[f1597,f106]) ).
fof(f2589,plain,
( a3 = b3
| ~ incident(a3,b2b3)
| ~ spl2_117 ),
inference(resolution,[],[f1745,f111]) ).
fof(f2591,plain,
( b3 = s
| ~ incident(s,b2b3)
| ~ spl2_117 ),
inference(resolution,[],[f1745,f108]) ).
fof(f2596,plain,
( a1 = b3
| ~ incident(s,b2b3)
| ~ spl2_117
| ~ spl2_123 ),
inference(forward_demodulation,[],[f2591,f2070]) ).
fof(f2599,plain,
( ~ incident(s,b2b3)
| spl2_24
| ~ spl2_117
| ~ spl2_123 ),
inference(forward_subsumption_resolution,[],[f2596,f325]) ).
fof(f2602,plain,
( ~ incident(a1,b2b3)
| spl2_24
| ~ spl2_117
| ~ spl2_123 ),
inference(forward_demodulation,[],[f2599,f2070]) ).
fof(f2603,plain,
( $false
| ~ spl2_6
| spl2_24
| ~ spl2_117
| ~ spl2_123 ),
inference(forward_subsumption_resolution,[],[f2602,f182]) ).
fof(f2604,plain,
( ~ spl2_6
| spl2_24
| ~ spl2_117
| ~ spl2_123 ),
inference(avatar_contradiction_clause,[],[f2603]) ).
fof(f2606,plain,
( spl2_94
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f543,f413,f1321]) ).
fof(f2611,plain,
( spl2_93
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f946,f413,f1317]) ).
fof(f2626,definition,
( spl2_137
<=> a2 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_137])],[avatar_definition]) ).
fof(f2627,plain,
( a2 != b2
| spl2_137 ),
inference(avatar_component_clause,[],[f2626]) ).
fof(f2628,plain,
( a2 = b2
| ~ spl2_137 ),
inference(avatar_component_clause,[],[f2626]) ).
fof(f2631,definition,
( spl2_138
<=> a2 = s ),
introduced(definition,[new_symbols(definition,[spl2_138])],[avatar_definition]) ).
fof(f2632,plain,
( a2 != s
| spl2_138 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2633,plain,
( a2 = s
| ~ spl2_138 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2635,plain,
( spl2_94
| ~ spl2_93 ),
inference(avatar_split_clause,[],[f1942,f1317,f1321]) ).
fof(f2638,definition,
( spl2_139
<=> incident(s,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_139])],[avatar_definition]) ).
fof(f2640,plain,
( ~ incident(s,a2a3)
| spl2_139 ),
inference(avatar_component_clause,[],[f2638]) ).
fof(f2644,definition,
( spl2_140
<=> a3 = s ),
introduced(definition,[new_symbols(definition,[spl2_140])],[avatar_definition]) ).
fof(f2646,plain,
( a3 = s
| ~ spl2_140 ),
inference(avatar_component_clause,[],[f2644]) ).
fof(f2649,definition,
( spl2_141
<=> incident(s,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_141])],[avatar_definition]) ).
fof(f2651,plain,
( ~ incident(s,b2b3)
| spl2_141 ),
inference(avatar_component_clause,[],[f2649]) ).
fof(f2653,definition,
( spl2_142
<=> b2 = s ),
introduced(definition,[new_symbols(definition,[spl2_142])],[avatar_definition]) ).
fof(f2655,plain,
( b2 = s
| ~ spl2_142 ),
inference(avatar_component_clause,[],[f2653]) ).
fof(f2659,definition,
( spl2_143
<=> b3 = s ),
introduced(definition,[new_symbols(definition,[spl2_143])],[avatar_definition]) ).
fof(f2660,plain,
( b3 != s
| spl2_143 ),
inference(avatar_component_clause,[],[f2659]) ).
fof(f2661,plain,
( b3 = s
| ~ spl2_143 ),
inference(avatar_component_clause,[],[f2659]) ).
fof(f2663,plain,
( a3 = b3
| ~ spl2_94
| ~ spl2_117 ),
inference(forward_subsumption_resolution,[],[f2589,f1322]) ).
fof(f2673,plain,
( a3 = b3
| ~ spl2_23
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f2408,f321]) ).
fof(f2694,plain,
( ~ spl2_94
| ~ spl2_26 ),
inference(avatar_split_clause,[],[f1994,f417,f1321]) ).
fof(f2698,plain,
( spl2_127
| ~ spl2_30 ),
inference(avatar_split_clause,[],[f479,f455,f2165]) ).
fof(f2721,plain,
( spl2_128
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f545,f413,f2173]) ).
fof(f2724,plain,
( ! [X0] :
( ~ incident(a3,sK0(X0,a3))
| ~ incident(p3,sK0(X0,b3))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_38 ),
inference(forward_demodulation,[],[f1094,f2673]) ).
fof(f2766,plain,
( ! [X0] :
( ~ incident(a3,sK0(X0,a3))
| ~ incident(p3,sK0(X0,a3))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_38 ),
inference(forward_demodulation,[],[f2724,f2673]) ).
fof(f2853,plain,
( ~ incident(a3,a3a1)
| spl2_8
| ~ spl2_93 ),
inference(superposition,[],[f197,f1319]) ).
fof(f2860,plain,
( $false
| spl2_8
| ~ spl2_93 ),
inference(forward_subsumption_resolution,[],[f2853,f98]) ).
fof(f2861,plain,
( spl2_8
| ~ spl2_93 ),
inference(avatar_contradiction_clause,[],[f2860]) ).
fof(f2906,plain,
( incident(a3,b2b3)
| ~ spl2_116 ),
inference(superposition,[],[f111,f1742]) ).
fof(f2911,plain,
( $false
| spl2_94
| ~ spl2_116 ),
inference(forward_subsumption_resolution,[],[f2906,f1323]) ).
fof(f2912,plain,
( spl2_94
| ~ spl2_116 ),
inference(avatar_contradiction_clause,[],[f2911]) ).
fof(f2924,plain,
( ~ incident(a2,b1b2)
| spl2_54 ),
inference(forward_subsumption_resolution,[],[f2542,f648]) ).
fof(f2925,plain,
( ~ incident(a1,b1b2)
| spl2_80 ),
inference(forward_subsumption_resolution,[],[f2541,f879]) ).
fof(f2932,plain,
( $false
| spl2_80
| ~ spl2_131 ),
inference(forward_subsumption_resolution,[],[f2925,f2306]) ).
fof(f2933,plain,
( spl2_80
| ~ spl2_131 ),
inference(avatar_contradiction_clause,[],[f2932]) ).
fof(f2937,plain,
( b2b3 != a3a1
| spl2_37
| ~ spl2_116 ),
inference(forward_demodulation,[],[f502,f1742]) ).
fof(f2974,plain,
( $false
| ~ spl2_25
| spl2_37
| ~ spl2_116 ),
inference(forward_subsumption_resolution,[],[f2937,f415]) ).
fof(f2975,plain,
( ~ spl2_25
| spl2_37
| ~ spl2_116 ),
inference(avatar_contradiction_clause,[],[f2974]) ).
fof(f3011,plain,
( incident(s,b2b3)
| ~ spl2_25
| ~ spl2_37 ),
inference(forward_demodulation,[],[f539,f415]) ).
fof(f3070,plain,
( ~ incident(b2,a3a1)
| spl2_7
| ~ spl2_30 ),
inference(superposition,[],[f193,f1242]) ).
fof(f3075,plain,
( $false
| ~ spl2_1
| spl2_7
| ~ spl2_30 ),
inference(forward_subsumption_resolution,[],[f3070,f160]) ).
fof(f3076,plain,
( ~ spl2_1
| spl2_7
| ~ spl2_30 ),
inference(avatar_contradiction_clause,[],[f3075]) ).
fof(f3097,definition,
( spl2_144
<=> b1b2 = s2 ),
introduced(definition,[new_symbols(definition,[spl2_144])],[avatar_definition]) ).
fof(f3098,plain,
( b1b2 != s2
| spl2_144 ),
inference(avatar_component_clause,[],[f3097]) ).
fof(f3099,plain,
( b1b2 = s2
| ~ spl2_144 ),
inference(avatar_component_clause,[],[f3097]) ).
fof(f3113,plain,
( b1 = b2
| ~ incident(s,b1b2)
| ~ spl2_132
| ~ spl2_142 ),
inference(forward_demodulation,[],[f2472,f2655]) ).
fof(f3119,plain,
( ~ incident(s,b1b2)
| ~ spl2_132
| ~ spl2_142 ),
inference(forward_subsumption_resolution,[],[f3113,f153]) ).
fof(f3125,plain,
( ~ incident(b2,b1b2)
| ~ spl2_132
| ~ spl2_142 ),
inference(forward_demodulation,[],[f3119,f2655]) ).
fof(f3126,plain,
( $false
| ~ spl2_132
| ~ spl2_142 ),
inference(forward_subsumption_resolution,[],[f3125,f101]) ).
fof(f3127,plain,
( ~ spl2_132
| ~ spl2_142 ),
inference(avatar_contradiction_clause,[],[f3126]) ).
fof(f3132,definition,
( spl2_147
<=> incident(s,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_147])],[avatar_definition]) ).
fof(f3134,plain,
( ~ incident(s,b1b2)
| spl2_147 ),
inference(avatar_component_clause,[],[f3132]) ).
fof(f3136,definition,
( spl2_148
<=> b1 = s ),
introduced(definition,[new_symbols(definition,[spl2_148])],[avatar_definition]) ).
fof(f3137,plain,
( b1 != s
| spl2_148 ),
inference(avatar_component_clause,[],[f3136]) ).
fof(f3138,plain,
( b1 = s
| ~ spl2_148 ),
inference(avatar_component_clause,[],[f3136]) ).
fof(f3139,plain,
( ~ spl2_147
| spl2_148
| ~ spl2_132 ),
inference(avatar_split_clause,[],[f2472,f2272,f3136,f3132]) ).
fof(f3143,plain,
( $false
| ~ spl2_25
| ~ spl2_37
| spl2_141 ),
inference(forward_subsumption_resolution,[],[f3011,f2651]) ).
fof(f3144,plain,
( ~ spl2_25
| ~ spl2_37
| spl2_141 ),
inference(avatar_contradiction_clause,[],[f3143]) ).
fof(f3210,plain,
( a2 = b3
| ~ spl2_5
| ~ spl2_48 ),
inference(forward_subsumption_resolution,[],[f2005,f104]) ).
fof(f3217,plain,
( ~ incident(a3,b1b2)
| ~ spl2_64
| spl2_73 ),
inference(forward_subsumption_resolution,[],[f755,f815]) ).
fof(f3232,plain,
( a1 = a2
| ~ spl2_5
| ~ spl2_24
| ~ spl2_48 ),
inference(forward_demodulation,[],[f3210,f326]) ).
fof(f3234,plain,
( $false
| ~ spl2_2
| ~ spl2_64
| spl2_73 ),
inference(forward_subsumption_resolution,[],[f3217,f164]) ).
fof(f3235,plain,
( ~ spl2_2
| ~ spl2_64
| spl2_73 ),
inference(avatar_contradiction_clause,[],[f3234]) ).
fof(f3247,plain,
( $false
| ~ spl2_5
| ~ spl2_24
| ~ spl2_48 ),
inference(forward_subsumption_resolution,[],[f3232,f156]) ).
fof(f3248,plain,
( ~ spl2_5
| ~ spl2_24
| ~ spl2_48 ),
inference(avatar_contradiction_clause,[],[f3247]) ).
fof(f3257,plain,
( a3 = s
| ~ spl2_73
| ~ spl2_148 ),
inference(forward_demodulation,[],[f3138,f816]) ).
fof(f3265,plain,
( a3 = b3
| ~ spl2_72
| ~ spl2_115 ),
inference(forward_subsumption_resolution,[],[f2566,f811]) ).
fof(f3266,plain,
( spl2_140
| ~ spl2_73
| ~ spl2_148 ),
inference(avatar_split_clause,[],[f3257,f3136,f814,f2644]) ).
fof(f3318,plain,
( a1 = b3
| ~ incident(b3,a3a1)
| ~ spl2_5
| ~ spl2_19 ),
inference(resolution,[],[f178,f289]) ).
fof(f3345,plain,
( incident(a3,b3b1)
| ~ spl2_46 ),
inference(superposition,[],[f120,f593]) ).
fof(f3457,plain,
( spl2_141
| ~ spl2_86 ),
inference(avatar_split_clause,[],[f1297,f1258,f2649]) ).
fof(f3510,plain,
( ~ incident(a2,a3a1)
| spl2_8
| ~ spl2_95 ),
inference(superposition,[],[f197,f1328]) ).
fof(f3511,plain,
( ~ incident(a2,b3b1)
| spl2_10
| ~ spl2_95 ),
inference(superposition,[],[f207,f1328]) ).
fof(f3584,plain,
( incident(a1,b3b1)
| ~ spl2_101 ),
inference(superposition,[],[f109,f1557]) ).
fof(f3642,plain,
( ~ incident(s,a1a2)
| ~ spl2_31
| spl2_138 ),
inference(forward_subsumption_resolution,[],[f2334,f2632]) ).
fof(f3650,plain,
( ~ incident(s,a1a2)
| ~ spl2_17
| spl2_123 ),
inference(forward_subsumption_resolution,[],[f2231,f2069]) ).
fof(f3654,plain,
( b3 = s
| ~ spl2_115
| ~ spl2_124 ),
inference(forward_subsumption_resolution,[],[f2568,f2073]) ).
fof(f3727,plain,
( $false
| spl2_79
| ~ spl2_101 ),
inference(forward_subsumption_resolution,[],[f3584,f876]) ).
fof(f3728,plain,
( spl2_79
| ~ spl2_101 ),
inference(avatar_contradiction_clause,[],[f3727]) ).
fof(f3757,plain,
( ~ incident(s,b3b1)
| ~ spl2_104
| spl2_148 ),
inference(forward_subsumption_resolution,[],[f2579,f3137]) ).
fof(f3767,plain,
( ~ incident(b3,a1a2)
| ~ spl2_31
| spl2_138
| ~ spl2_143 ),
inference(forward_demodulation,[],[f3642,f2661]) ).
fof(f3768,plain,
( ~ incident(b3,a1a2)
| ~ spl2_17
| spl2_123
| ~ spl2_143 ),
inference(forward_demodulation,[],[f3650,f2661]) ).
fof(f3776,plain,
( $false
| ~ spl2_5
| ~ spl2_31
| spl2_138
| ~ spl2_143 ),
inference(forward_subsumption_resolution,[],[f3767,f178]) ).
fof(f3777,plain,
( ~ spl2_5
| ~ spl2_31
| spl2_138
| ~ spl2_143 ),
inference(avatar_contradiction_clause,[],[f3776]) ).
fof(f3778,plain,
( $false
| ~ spl2_5
| ~ spl2_17
| spl2_123
| ~ spl2_143 ),
inference(forward_subsumption_resolution,[],[f3768,f178]) ).
fof(f3779,plain,
( ~ spl2_5
| ~ spl2_17
| spl2_123
| ~ spl2_143 ),
inference(avatar_contradiction_clause,[],[f3778]) ).
fof(f3780,plain,
( b1 = b3
| ~ spl2_143
| ~ spl2_148 ),
inference(forward_demodulation,[],[f3138,f2661]) ).
fof(f3782,plain,
( $false
| ~ spl2_143
| ~ spl2_148 ),
inference(forward_subsumption_resolution,[],[f3780,f151]) ).
fof(f3783,plain,
( ~ spl2_143
| ~ spl2_148 ),
inference(avatar_contradiction_clause,[],[f3782]) ).
fof(f3788,plain,
( $false
| ~ spl2_115
| ~ spl2_124
| spl2_143 ),
inference(forward_subsumption_resolution,[],[f3654,f2660]) ).
fof(f3789,plain,
( ~ spl2_115
| ~ spl2_124
| spl2_143 ),
inference(avatar_contradiction_clause,[],[f3788]) ).
fof(f3795,plain,
( ~ incident(s,b3b1)
| ~ spl2_115
| spl2_143 ),
inference(forward_subsumption_resolution,[],[f2568,f2660]) ).
fof(f3798,plain,
( ~ incident(b1,b3b1)
| ~ spl2_115
| spl2_143
| ~ spl2_148 ),
inference(forward_demodulation,[],[f3795,f3138]) ).
fof(f3799,plain,
( $false
| ~ spl2_115
| spl2_143
| ~ spl2_148 ),
inference(forward_subsumption_resolution,[],[f3798,f105]) ).
fof(f3800,plain,
( ~ spl2_115
| spl2_143
| ~ spl2_148 ),
inference(avatar_contradiction_clause,[],[f3799]) ).
fof(f3801,plain,
( ~ spl2_124
| ~ spl2_104
| spl2_148 ),
inference(avatar_split_clause,[],[f3757,f3136,f1596,f2072]) ).
fof(f3802,plain,
( incident(a2,b1b2)
| ~ spl2_137 ),
inference(superposition,[],[f101,f2628]) ).
fof(f3803,plain,
( incident(a2,b2b3)
| ~ spl2_137 ),
inference(superposition,[],[f102,f2628]) ).
fof(f3810,plain,
( $false
| spl2_96
| ~ spl2_137 ),
inference(forward_subsumption_resolution,[],[f3803,f1332]) ).
fof(f3811,plain,
( spl2_96
| ~ spl2_137 ),
inference(avatar_contradiction_clause,[],[f3810]) ).
fof(f3812,plain,
( $false
| spl2_54
| ~ spl2_137 ),
inference(forward_subsumption_resolution,[],[f3802,f2924]) ).
fof(f3813,plain,
( spl2_54
| ~ spl2_137 ),
inference(avatar_contradiction_clause,[],[f3812]) ).
fof(f3835,plain,
( a2 = b2
| ~ incident(a2,b2b3)
| ~ spl2_87 ),
inference(resolution,[],[f1263,f110]) ).
fof(f3837,plain,
( b2 = s
| ~ incident(s,b2b3)
| ~ spl2_87 ),
inference(resolution,[],[f1263,f107]) ).
fof(f3862,plain,
( b3 = s
| ~ incident(s,b2b3)
| ~ spl2_117 ),
inference(resolution,[],[f1745,f108]) ).
fof(f3867,plain,
( incident(a2,b1b2)
| ~ spl2_63 ),
inference(superposition,[],[f96,f729]) ).
fof(f3876,plain,
( $false
| spl2_54
| ~ spl2_63 ),
inference(forward_subsumption_resolution,[],[f3867,f2924]) ).
fof(f3877,plain,
( spl2_54
| ~ spl2_63 ),
inference(avatar_contradiction_clause,[],[f3876]) ).
fof(f3878,plain,
( spl2_72
| ~ spl2_46 ),
inference(avatar_split_clause,[],[f3345,f591,f810]) ).
fof(f3923,plain,
( incident(a3,b2b3)
| ~ spl2_72
| ~ spl2_115 ),
inference(superposition,[],[f103,f3265]) ).
fof(f3926,plain,
( a3 != b1
| ~ spl2_72
| ~ spl2_115 ),
inference(superposition,[],[f151,f3265]) ).
fof(f3934,plain,
( $false
| ~ spl2_72
| ~ spl2_73
| ~ spl2_115 ),
inference(forward_subsumption_resolution,[],[f3926,f816]) ).
fof(f3935,plain,
( ~ spl2_72
| ~ spl2_73
| ~ spl2_115 ),
inference(avatar_contradiction_clause,[],[f3934]) ).
fof(f3936,plain,
( $false
| ~ spl2_72
| spl2_94
| ~ spl2_115 ),
inference(forward_subsumption_resolution,[],[f3923,f1323]) ).
fof(f3937,plain,
( ~ spl2_72
| spl2_94
| ~ spl2_115 ),
inference(avatar_contradiction_clause,[],[f3936]) ).
fof(f3950,plain,
( b1 = s
| ~ spl2_104
| ~ spl2_124 ),
inference(forward_subsumption_resolution,[],[f2579,f2073]) ).
fof(f3956,plain,
( incident(s,b3b1)
| ~ spl2_114 ),
inference(superposition,[],[f108,f1734]) ).
fof(f3957,plain,
( incident(a3,b3b1)
| ~ spl2_114 ),
inference(superposition,[],[f111,f1734]) ).
fof(f4026,plain,
( incident(s,b1b2)
| ~ spl2_144 ),
inference(superposition,[],[f107,f3099]) ).
fof(f4027,plain,
( incident(a2,b1b2)
| ~ spl2_144 ),
inference(superposition,[],[f110,f3099]) ).
fof(f4034,plain,
( $false
| spl2_54
| ~ spl2_144 ),
inference(forward_subsumption_resolution,[],[f4027,f2924]) ).
fof(f4035,plain,
( spl2_54
| ~ spl2_144 ),
inference(avatar_contradiction_clause,[],[f4034]) ).
fof(f4036,plain,
( $false
| ~ spl2_144
| spl2_147 ),
inference(forward_subsumption_resolution,[],[f4026,f3134]) ).
fof(f4037,plain,
( ~ spl2_144
| spl2_147 ),
inference(avatar_contradiction_clause,[],[f4036]) ).
fof(f4087,plain,
( ~ incident(a3,a2a3)
| spl2_139
| ~ spl2_140 ),
inference(superposition,[],[f2640,f2646]) ).
fof(f4088,plain,
( $false
| spl2_139
| ~ spl2_140 ),
inference(forward_subsumption_resolution,[],[f4087,f97]) ).
fof(f4089,plain,
( spl2_139
| ~ spl2_140 ),
inference(avatar_contradiction_clause,[],[f4088]) ).
fof(f4113,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ incident(X2,X1)
| ~ incident(X2,X0)
| ~ line(X1)
| sK1(X0,X1) = X2
| ~ line(X0)
| ~ line(X1) ),
inference(resolution,[],[f233,f140]) ).
fof(f4118,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ incident(X2,X1)
| ~ incident(X2,X0)
| ~ line(X1)
| sK1(X0,X1) = X2
| ~ line(X0) ),
inference(duplicate_literal_removal,[],[f4113]) ).
fof(f4119,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ incident(X2,X1)
| ~ incident(X2,X0)
| sK1(X0,X1) = X2
| ~ line(X0) ),
inference(forward_subsumption_resolution,[],[f4118,f122]) ).
fof(f4120,plain,
! [X2,X0,X1] :
( ~ incident(X2,X1)
| X0 = X1
| ~ incident(X2,X0)
| sK1(X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f4119,f122]) ).
fof(f4133,plain,
! [X0] :
( ~ incident(a2,X0)
| a2a3 = X0
| a2 = sK1(X0,a2a3) ),
inference(resolution,[],[f4120,f96]) ).
fof(f4137,plain,
( ! [X0] :
( ~ incident(a3,X0)
| b1b2 = X0
| a3 = sK1(X0,b1b2) )
| ~ spl2_2 ),
inference(resolution,[],[f4120,f164]) ).
fof(f4138,plain,
! [X0] :
( ~ incident(a3,X0)
| a2a3 = X0
| a3 = sK1(X0,a2a3) ),
inference(resolution,[],[f4120,f97]) ).
fof(f4147,plain,
! [X0] :
( ~ incident(b2,X0)
| b1b2 = X0
| b2 = sK1(X0,b1b2) ),
inference(resolution,[],[f4120,f101]) ).
fof(f4238,plain,
( b1b2 = a2a3
| a3 = sK1(a2a3,b1b2)
| ~ spl2_2 ),
inference(resolution,[],[f4137,f97]) ).
fof(f4249,plain,
( a3 = sK1(a2a3,b1b2)
| ~ spl2_2
| spl2_63 ),
inference(forward_subsumption_resolution,[],[f4238,f728]) ).
fof(f4361,plain,
( a2a3 = s2
| a2 = sK1(s2,a2a3) ),
inference(resolution,[],[f4133,f110]) ).
fof(f4400,plain,
( b3b1 = a2a3
| a3 = sK1(b3b1,a2a3)
| ~ spl2_72 ),
inference(resolution,[],[f4138,f811]) ).
fof(f4414,plain,
( a3 = sK1(b3b1,a2a3)
| spl2_44
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f4400,f565]) ).
fof(f4421,plain,
( b1b2 = s2
| b2 = sK1(s2,b1b2) ),
inference(resolution,[],[f4147,f113]) ).
fof(f4426,plain,
( b2 = sK1(s2,b1b2)
| spl2_144 ),
inference(forward_subsumption_resolution,[],[f4421,f3098]) ).
fof(f4428,plain,
( b2 = sK1(a2a3,b1b2)
| ~ spl2_84
| spl2_144 ),
inference(forward_demodulation,[],[f4426,f1252]) ).
fof(f4429,plain,
( a3 = b2
| ~ spl2_2
| spl2_63
| ~ spl2_84
| spl2_144 ),
inference(forward_demodulation,[],[f4428,f4249]) ).
fof(f4430,plain,
( spl2_52
| ~ spl2_2
| spl2_63
| ~ spl2_84
| spl2_144 ),
inference(avatar_split_clause,[],[f4429,f3097,f1250,f727,f162,f622]) ).
fof(f4435,plain,
( ~ incident(a3,a3a1)
| spl2_1
| ~ spl2_52 ),
inference(superposition,[],[f159,f624]) ).
fof(f4444,plain,
( $false
| spl2_1
| ~ spl2_52 ),
inference(forward_subsumption_resolution,[],[f4435,f98]) ).
fof(f4445,plain,
( spl2_1
| ~ spl2_52 ),
inference(avatar_contradiction_clause,[],[f4444]) ).
fof(f4490,plain,
( b3b1 = a2a3
| ~ spl2_112
| ~ spl2_114 ),
inference(forward_demodulation,[],[f1726,f1734]) ).
fof(f4501,plain,
( a2 = b1
| ~ spl2_104
| ~ spl2_124
| ~ spl2_138 ),
inference(forward_demodulation,[],[f3950,f2633]) ).
fof(f4543,plain,
( $false
| spl2_44
| ~ spl2_112
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f4490,f565]) ).
fof(f4544,plain,
( spl2_44
| ~ spl2_112
| ~ spl2_114 ),
inference(avatar_contradiction_clause,[],[f4543]) ).
fof(f4548,plain,
( spl2_120
| ~ spl2_104
| ~ spl2_124
| ~ spl2_138 ),
inference(avatar_split_clause,[],[f4501,f2631,f2072,f1596,f1780]) ).
fof(f4569,plain,
( b3b1 != a2a3
| spl2_112
| ~ spl2_114 ),
inference(forward_demodulation,[],[f1725,f1734]) ).
fof(f4571,plain,
( a2 = a3
| ~ incident(s,a2a3)
| ~ spl2_113
| ~ spl2_138 ),
inference(forward_demodulation,[],[f2442,f2633]) ).
fof(f4574,plain,
( ~ incident(s,a2a3)
| ~ spl2_113
| ~ spl2_138 ),
inference(forward_subsumption_resolution,[],[f4571,f155]) ).
fof(f4577,plain,
( ~ incident(a2,a2a3)
| ~ spl2_113
| ~ spl2_138 ),
inference(forward_demodulation,[],[f4574,f2633]) ).
fof(f4578,plain,
( $false
| ~ spl2_113
| ~ spl2_138 ),
inference(forward_subsumption_resolution,[],[f4577,f96]) ).
fof(f4579,plain,
( ~ spl2_113
| ~ spl2_138 ),
inference(avatar_contradiction_clause,[],[f4578]) ).
fof(f4700,plain,
( b3b1 = a2a3
| a2 = sK1(b3b1,a2a3)
| ~ spl2_4 ),
inference(resolution,[],[f173,f4133]) ).
fof(f4715,plain,
( a2 = sK1(b3b1,a2a3)
| ~ spl2_4
| spl2_44 ),
inference(forward_subsumption_resolution,[],[f4700,f565]) ).
fof(f4716,plain,
( a2 = a3
| ~ spl2_4
| spl2_44
| ~ spl2_72 ),
inference(forward_demodulation,[],[f4715,f4414]) ).
fof(f4717,plain,
( $false
| ~ spl2_4
| spl2_44
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f4716,f155]) ).
fof(f4718,plain,
( ~ spl2_4
| spl2_44
| ~ spl2_72 ),
inference(avatar_contradiction_clause,[],[f4717]) ).
fof(f4726,plain,
( $false
| ~ spl2_44
| spl2_112
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f4569,f566]) ).
fof(f4727,plain,
( ~ spl2_44
| spl2_112
| ~ spl2_114 ),
inference(avatar_contradiction_clause,[],[f4726]) ).
fof(f4771,plain,
( a2 = s
| ~ incident(s,a2a3)
| ~ spl2_85 ),
inference(resolution,[],[f1255,f107]) ).
fof(f4804,plain,
( incident(a2,b3b1)
| ~ spl2_44 ),
inference(superposition,[],[f96,f566]) ).
fof(f4863,plain,
( incident(a2,b1b2)
| ~ spl2_120 ),
inference(superposition,[],[f100,f1782]) ).
fof(f4873,plain,
( $false
| spl2_54
| ~ spl2_120 ),
inference(forward_subsumption_resolution,[],[f4863,f2924]) ).
fof(f4874,plain,
( spl2_54
| ~ spl2_120 ),
inference(avatar_contradiction_clause,[],[f4873]) ).
fof(f4876,plain,
( ~ incident(s,a2a3)
| ~ spl2_85
| spl2_138 ),
inference(forward_subsumption_resolution,[],[f4771,f2632]) ).
fof(f4978,plain,
( ! [X0] :
( ~ incident(p3,sK0(X0,a3))
| ~ point(X0)
| ~ point(X0)
| ~ point(a3) )
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_38 ),
inference(resolution,[],[f2766,f138]) ).
fof(f4981,plain,
( ! [X0] :
( ~ incident(p3,sK0(X0,a3))
| ~ point(X0)
| ~ point(a3) )
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_38 ),
inference(duplicate_literal_removal,[],[f4978]) ).
fof(f4982,plain,
( ! [X0] :
( ~ incident(p3,sK0(X0,a3))
| ~ point(X0) )
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f4981,f490]) ).
fof(f4983,plain,
( ~ point(p3)
| ~ point(p3)
| ~ point(a3)
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38 ),
inference(resolution,[],[f4982,f139]) ).
fof(f4984,plain,
( ~ point(p3)
| ~ point(a3)
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38 ),
inference(duplicate_literal_removal,[],[f4983]) ).
fof(f4985,plain,
( ~ point(a3)
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38
| ~ spl2_75 ),
inference(forward_subsumption_resolution,[],[f4984,f849]) ).
fof(f4986,plain,
( $false
| ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38
| ~ spl2_75 ),
inference(forward_subsumption_resolution,[],[f4985,f490]) ).
fof(f4987,plain,
( ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38
| ~ spl2_75 ),
inference(avatar_contradiction_clause,[],[f4986]) ).
fof(f5027,plain,
( $false
| spl2_4
| ~ spl2_44 ),
inference(forward_subsumption_resolution,[],[f4804,f172]) ).
fof(f5028,plain,
( spl2_4
| ~ spl2_44 ),
inference(avatar_contradiction_clause,[],[f5027]) ).
fof(f5052,plain,
( ~ spl2_139
| ~ spl2_85
| spl2_138 ),
inference(avatar_split_clause,[],[f4876,f2631,f1254,f2638]) ).
fof(f5163,plain,
( ~ incident(a2,b3b1)
| spl2_9
| ~ spl2_54 ),
inference(superposition,[],[f203,f649]) ).
fof(f5201,plain,
( a3 = s
| ~ incident(s,a3a1)
| ~ spl2_38 ),
inference(resolution,[],[f506,f108]) ).
fof(f5310,plain,
( b1b2 = s2
| a2 = sK1(s2,a2a3)
| ~ spl2_63 ),
inference(forward_demodulation,[],[f4361,f729]) ).
fof(f5315,plain,
( a2 = sK1(s2,a2a3)
| ~ spl2_63
| spl2_144 ),
inference(forward_subsumption_resolution,[],[f5310,f3098]) ).
fof(f5318,plain,
( a2 = sK1(s2,b1b2)
| ~ spl2_63
| spl2_144 ),
inference(forward_demodulation,[],[f5315,f729]) ).
fof(f5323,plain,
( a2 = b2
| ~ spl2_63
| spl2_144 ),
inference(forward_demodulation,[],[f5318,f4426]) ).
fof(f5324,plain,
( $false
| ~ spl2_63
| spl2_137
| spl2_144 ),
inference(forward_subsumption_resolution,[],[f5323,f2627]) ).
fof(f5325,plain,
( ~ spl2_63
| spl2_137
| spl2_144 ),
inference(avatar_contradiction_clause,[],[f5324]) ).
fof(f5326,plain,
( spl2_124
| ~ spl2_114 ),
inference(avatar_split_clause,[],[f3956,f1732,f2072]) ).
fof(f5327,plain,
( $false
| spl2_72
| ~ spl2_114 ),
inference(forward_subsumption_resolution,[],[f3957,f812]) ).
fof(f5328,plain,
( spl2_72
| ~ spl2_114 ),
inference(avatar_contradiction_clause,[],[f5327]) ).
fof(f5439,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(p1,X0)
| ~ incident(p3,X0) )
| ~ spl2_46 ),
inference(superposition,[],[f186,f593]) ).
fof(f5450,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(a2,X0)
| ~ incident(p1,X0) )
| ~ spl2_46
| ~ spl2_54 ),
inference(forward_demodulation,[],[f5439,f649]) ).
fof(f5452,plain,
( ~ incident(a2,a2a3)
| ~ incident(p1,a2a3)
| ~ spl2_46
| ~ spl2_54 ),
inference(resolution,[],[f5450,f97]) ).
fof(f5458,plain,
( ~ incident(p1,a2a3)
| ~ spl2_46
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f5452,f96]) ).
fof(f5460,plain,
( $false
| ~ spl2_46
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f5458,f117]) ).
fof(f5461,plain,
( ~ spl2_46
| ~ spl2_54 ),
inference(avatar_contradiction_clause,[],[f5460]) ).
fof(f5468,plain,
( ~ spl2_23
| spl2_24
| ~ spl2_5
| ~ spl2_19 ),
inference(avatar_split_clause,[],[f3318,f288,f176,f324,f320]) ).
fof(f5494,plain,
( spl2_129
| ~ spl2_79 ),
inference(avatar_split_clause,[],[f1963,f874,f2177]) ).
fof(f5499,plain,
( $false
| ~ spl2_63
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f2303,f3867]) ).
fof(f5500,plain,
( ~ spl2_63
| ~ spl2_80 ),
inference(avatar_contradiction_clause,[],[f5499]) ).
fof(f5606,plain,
( p2 = b3
| ~ spl2_92
| ~ spl2_128 ),
inference(forward_subsumption_resolution,[],[f2249,f2174]) ).
fof(f5756,plain,
( a1 = a3
| ~ incident(s,a3a1)
| ~ spl2_38
| ~ spl2_123 ),
inference(forward_demodulation,[],[f5201,f2070]) ).
fof(f5760,plain,
( spl2_122
| ~ spl2_5
| ~ spl2_48 ),
inference(avatar_split_clause,[],[f3210,f606,f176,f1881]) ).
fof(f5761,plain,
( ~ spl2_79
| ~ spl2_48 ),
inference(avatar_split_clause,[],[f2154,f606,f874]) ).
fof(f5855,plain,
( p2 = a3
| ~ spl2_92
| ~ spl2_94
| ~ spl2_117
| ~ spl2_128 ),
inference(forward_demodulation,[],[f5606,f2663]) ).
fof(f5856,plain,
( $false
| ~ spl2_4
| spl2_9
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f5163,f173]) ).
fof(f5857,plain,
( ~ spl2_4
| spl2_9
| ~ spl2_54 ),
inference(avatar_contradiction_clause,[],[f5856]) ).
fof(f5872,plain,
( ~ incident(s,a3a1)
| ~ spl2_38
| ~ spl2_123 ),
inference(forward_subsumption_resolution,[],[f5756,f154]) ).
fof(f5920,plain,
( $false
| spl2_46
| ~ spl2_92
| ~ spl2_94
| ~ spl2_117
| ~ spl2_128 ),
inference(forward_subsumption_resolution,[],[f5855,f592]) ).
fof(f5921,plain,
( spl2_46
| ~ spl2_92
| ~ spl2_94
| ~ spl2_117
| ~ spl2_128 ),
inference(avatar_contradiction_clause,[],[f5920]) ).
fof(f5924,plain,
( ~ incident(a1,a3a1)
| ~ spl2_38
| ~ spl2_123 ),
inference(forward_demodulation,[],[f5872,f2070]) ).
fof(f5941,plain,
( $false
| ~ spl2_38
| ~ spl2_123 ),
inference(forward_subsumption_resolution,[],[f5924,f99]) ).
fof(f5942,plain,
( ~ spl2_38
| ~ spl2_123 ),
inference(avatar_contradiction_clause,[],[f5941]) ).
fof(f6130,plain,
( incident(a2,b2b3)
| ~ spl2_122 ),
inference(superposition,[],[f103,f1883]) ).
fof(f6141,plain,
( $false
| spl2_96
| ~ spl2_122 ),
inference(forward_subsumption_resolution,[],[f6130,f1332]) ).
fof(f6142,plain,
( spl2_96
| ~ spl2_122 ),
inference(avatar_contradiction_clause,[],[f6141]) ).
fof(f6143,plain,
( b3b1 = a3a1
| ~ spl2_18
| ~ spl2_47 ),
inference(forward_demodulation,[],[f604,f286]) ).
fof(f6144,plain,
( spl2_79
| ~ spl2_47 ),
inference(avatar_split_clause,[],[f1950,f602,f874]) ).
fof(f6145,plain,
( $false
| spl2_9
| ~ spl2_47 ),
inference(forward_subsumption_resolution,[],[f1952,f203]) ).
fof(f6146,plain,
( spl2_9
| ~ spl2_47 ),
inference(avatar_contradiction_clause,[],[f6145]) ).
fof(f6148,plain,
( $false
| ~ spl2_17
| ~ spl2_47
| spl2_80 ),
inference(forward_subsumption_resolution,[],[f2077,f2925]) ).
fof(f6149,plain,
( ~ spl2_17
| ~ spl2_47
| spl2_80 ),
inference(avatar_contradiction_clause,[],[f6148]) ).
fof(f6181,plain,
( $false
| ~ spl2_18
| ~ spl2_47 ),
inference(forward_subsumption_resolution,[],[f6143,f148]) ).
fof(f6182,plain,
( ~ spl2_18
| ~ spl2_47 ),
inference(avatar_contradiction_clause,[],[f6181]) ).
fof(f6192,plain,
( $false
| spl2_8
| ~ spl2_18
| ~ spl2_95 ),
inference(forward_subsumption_resolution,[],[f3510,f293]) ).
fof(f6193,plain,
( spl2_8
| ~ spl2_18
| ~ spl2_95 ),
inference(avatar_contradiction_clause,[],[f6192]) ).
fof(f6205,plain,
( ~ incident(a2,b2b3)
| ~ spl2_87
| spl2_137 ),
inference(forward_subsumption_resolution,[],[f3835,f2627]) ).
fof(f6214,plain,
( $false
| ~ spl2_87
| ~ spl2_96
| spl2_137 ),
inference(forward_subsumption_resolution,[],[f6205,f1331]) ).
fof(f6215,plain,
( ~ spl2_87
| ~ spl2_96
| spl2_137 ),
inference(avatar_contradiction_clause,[],[f6214]) ).
fof(f6220,plain,
( spl2_80
| ~ spl2_7
| ~ spl2_19 ),
inference(avatar_split_clause,[],[f423,f288,f191,f878]) ).
fof(f6256,plain,
( ~ spl2_141
| spl2_142
| ~ spl2_87 ),
inference(avatar_split_clause,[],[f3837,f1262,f2653,f2649]) ).
fof(f6257,plain,
( ~ spl2_141
| spl2_143
| ~ spl2_117 ),
inference(avatar_split_clause,[],[f3862,f1744,f2659,f2649]) ).
fof(f6353,plain,
( incident(s,a2a3)
| ~ spl2_112 ),
inference(superposition,[],[f108,f1726]) ).
fof(f6355,plain,
( incident(b3,a2a3)
| ~ spl2_112 ),
inference(superposition,[],[f114,f1726]) ).
fof(f6407,plain,
( ! [X0] :
( ~ incident(a1,X0)
| ~ incident(p1,X0)
| ~ incident(p3,X0) )
| ~ spl2_129 ),
inference(superposition,[],[f186,f2179]) ).
fof(f6417,plain,
( ! [X0] :
( ~ incident(a1,X0)
| ~ incident(a1,X0)
| ~ incident(p1,X0) )
| ~ spl2_80
| ~ spl2_129 ),
inference(forward_demodulation,[],[f6407,f880]) ).
fof(f6418,plain,
( ! [X0] :
( ~ incident(a1,X0)
| ~ incident(p1,X0) )
| ~ spl2_80
| ~ spl2_129 ),
inference(duplicate_literal_removal,[],[f6417]) ).
fof(f6423,plain,
( ! [X0] :
( ~ incident(p1,sK0(X0,a1))
| ~ point(X0)
| ~ point(a1) )
| ~ spl2_80
| ~ spl2_129 ),
inference(resolution,[],[f6418,f138]) ).
fof(f6426,plain,
( ! [X0] :
( ~ incident(p1,sK0(X0,a1))
| ~ point(X0) )
| ~ spl2_13
| ~ spl2_80
| ~ spl2_129 ),
inference(forward_subsumption_resolution,[],[f6423,f265]) ).
fof(f6428,plain,
( ~ point(p1)
| ~ point(p1)
| ~ point(a1)
| ~ spl2_13
| ~ spl2_80
| ~ spl2_129 ),
inference(resolution,[],[f6426,f139]) ).
fof(f6429,plain,
( ~ point(p1)
| ~ point(a1)
| ~ spl2_13
| ~ spl2_80
| ~ spl2_129 ),
inference(duplicate_literal_removal,[],[f6428]) ).
fof(f6430,plain,
( ~ point(a1)
| ~ spl2_13
| ~ spl2_80
| ~ spl2_81
| ~ spl2_129 ),
inference(forward_subsumption_resolution,[],[f6429,f927]) ).
fof(f6431,plain,
( $false
| ~ spl2_13
| ~ spl2_80
| ~ spl2_81
| ~ spl2_129 ),
inference(forward_subsumption_resolution,[],[f6430,f265]) ).
fof(f6432,plain,
( ~ spl2_13
| ~ spl2_80
| ~ spl2_81
| ~ spl2_129 ),
inference(avatar_contradiction_clause,[],[f6431]) ).
fof(f6439,plain,
( spl2_124
| ~ spl2_16
| ~ spl2_47 ),
inference(avatar_split_clause,[],[f2089,f602,f276,f2072]) ).
fof(f6444,plain,
( $false
| ~ spl2_4
| spl2_10
| ~ spl2_95 ),
inference(forward_subsumption_resolution,[],[f3511,f173]) ).
fof(f6445,plain,
( ~ spl2_4
| spl2_10
| ~ spl2_95 ),
inference(avatar_contradiction_clause,[],[f6444]) ).
fof(f6447,plain,
( spl2_139
| ~ spl2_112 ),
inference(avatar_split_clause,[],[f6353,f1724,f2638]) ).
fof(f6448,plain,
( spl2_121
| ~ spl2_112 ),
inference(avatar_split_clause,[],[f6355,f1724,f1877]) ).
cnf(s1,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f165]) ).
cnf(s2,plain,
( spl2_3
| spl2_4 ),
inference(sat_conversion,[],[f174]) ).
cnf(s3,plain,
( spl2_5
| spl2_6 ),
inference(sat_conversion,[],[f183]) ).
cnf(s4,plain,
( ~ spl2_1
| ~ spl2_3
| ~ spl2_5 ),
inference(sat_conversion,[],[f187]) ).
cnf(s5,plain,
( ~ spl2_2
| ~ spl2_4
| ~ spl2_6 ),
inference(sat_conversion,[],[f188]) ).
cnf(s6,plain,
( ~ spl2_7
| ~ spl2_8 ),
inference(sat_conversion,[],[f198]) ).
cnf(s7,plain,
( ~ spl2_9
| ~ spl2_10 ),
inference(sat_conversion,[],[f208]) ).
cnf(s8,plain,
( ~ spl2_11
| spl2_12 ),
inference(sat_conversion,[],[f244]) ).
cnf(s11,plain,
( spl2_16
| spl2_17 ),
inference(sat_conversion,[],[f282]) ).
cnf(s12,plain,
( spl2_18
| spl2_19 ),
inference(sat_conversion,[],[f290]) ).
cnf(s13,plain,
( spl2_7
| ~ spl2_18 ),
inference(sat_conversion,[],[f297]) ).
cnf(s25,plain,
( ~ spl2_6
| spl2_25
| spl2_26 ),
inference(sat_conversion,[],[f419]) ).
cnf(s30,plain,
( spl2_30
| spl2_31 ),
inference(sat_conversion,[],[f461]) ).
cnf(s31,plain,
( spl2_32
| spl2_33 ),
inference(sat_conversion,[],[f469]) ).
cnf(s34,plain,
( spl2_37
| spl2_38 ),
inference(sat_conversion,[],[f507]) ).
cnf(s35,plain,
( spl2_39
| spl2_40 ),
inference(sat_conversion,[],[f515]) ).
cnf(s37,plain,
( ~ spl2_19
| ~ spl2_39 ),
inference(sat_conversion,[],[f533]) ).
cnf(s39,plain,
( spl2_23
| ~ spl2_37 ),
inference(sat_conversion,[],[f541]) ).
cnf(s42,plain,
( ~ spl2_32
| ~ spl2_40 ),
inference(sat_conversion,[],[f598]) ).
cnf(s43,plain,
( ~ spl2_4
| spl2_47
| spl2_48 ),
inference(sat_conversion,[],[f608]) ).
cnf(s44,plain,
( ~ spl2_6
| spl2_49
| spl2_50 ),
inference(sat_conversion,[],[f616]) ).
cnf(s53,plain,
( ~ spl2_3
| spl2_63
| spl2_64 ),
inference(sat_conversion,[],[f733]) ).
cnf(s58,plain,
( ~ spl2_3
| spl2_44
| spl2_70 ),
inference(sat_conversion,[],[f797]) ).
cnf(s60,plain,
( ~ spl2_70
| ~ spl2_72
| spl2_73 ),
inference(sat_conversion,[],[f817]) ).
cnf(s82,plain,
spl2_34,
inference(sat_conversion,[],[f1013]) ).
cnf(s85,plain,
spl2_27,
inference(sat_conversion,[],[f1019]) ).
cnf(s88,plain,
spl2_13,
inference(sat_conversion,[],[f1025]) ).
cnf(s91,plain,
spl2_11,
inference(sat_conversion,[],[f1031]) ).
cnf(s93,plain,
spl2_81,
inference(sat_conversion,[],[f1035]) ).
cnf(s96,plain,
spl2_75,
inference(sat_conversion,[],[f1041]) ).
cnf(s97,plain,
( ~ spl2_16
| ~ spl2_30 ),
inference(sat_conversion,[],[f1247]) ).
cnf(s98,plain,
( spl2_84
| spl2_85 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s99,plain,
( spl2_86
| spl2_87 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s106,plain,
( spl2_91
| spl2_92 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s107,plain,
( spl2_93
| ~ spl2_94 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s108,plain,
( spl2_95
| ~ spl2_96 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s109,plain,
( ~ spl2_86
| spl2_96 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s110,plain,
( ~ spl2_50
| ~ spl2_96 ),
inference(sat_conversion,[],[f1349]) ).
cnf(s111,plain,
( ~ spl2_6
| spl2_79
| ~ spl2_91 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s119,plain,
( spl2_9
| ~ spl2_16 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s131,plain,
( ~ spl2_93
| ~ spl2_95 ),
inference(sat_conversion,[],[f1592]) ).
cnf(s132,plain,
( spl2_101
| spl2_104 ),
inference(sat_conversion,[],[f1598]) ).
cnf(s150,plain,
( spl2_3
| ~ spl2_44 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s151,plain,
( spl2_5
| ~ spl2_49 ),
inference(sat_conversion,[],[f1673]) ).
cnf(s153,plain,
( spl2_5
| ~ spl2_24 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s156,plain,
( spl2_112
| spl2_113 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s157,plain,
( spl2_114
| spl2_115 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s158,plain,
( spl2_116
| spl2_117 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s164,plain,
( ~ spl2_11
| ~ spl2_12
| ~ spl2_27
| ~ spl2_54
| ~ spl2_95 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s176,plain,
( spl2_72
| ~ spl2_73 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s177,plain,
( spl2_46
| ~ spl2_72 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s180,plain,
( ~ spl2_5
| ~ spl2_33
| ~ spl2_121
| spl2_122 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s191,plain,
( ~ spl2_46
| ~ spl2_79 ),
inference(sat_conversion,[],[f1966]) ).
cnf(s203,plain,
( spl2_23
| ~ spl2_25 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s213,plain,
( spl2_5
| ~ spl2_47 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s215,plain,
( ~ spl2_17
| spl2_123
| ~ spl2_127 ),
inference(sat_conversion,[],[f2168]) ).
cnf(s218,plain,
( spl2_7
| ~ spl2_80 ),
inference(sat_conversion,[],[f2190]) ).
cnf(s222,plain,
( spl2_131
| spl2_132 ),
inference(sat_conversion,[],[f2274]) ).
cnf(s226,plain,
( ~ spl2_1
| ~ spl2_26
| ~ spl2_31 ),
inference(sat_conversion,[],[f2351]) ).
cnf(s240,plain,
( ~ spl2_6
| spl2_24
| ~ spl2_117
| ~ spl2_123 ),
inference(sat_conversion,[],[f2604]) ).
cnf(s241,plain,
( ~ spl2_25
| spl2_94 ),
inference(sat_conversion,[],[f2606]) ).
cnf(s243,plain,
( ~ spl2_25
| spl2_93 ),
inference(sat_conversion,[],[f2611]) ).
cnf(s246,plain,
( ~ spl2_93
| spl2_94 ),
inference(sat_conversion,[],[f2635]) ).
cnf(s252,plain,
( ~ spl2_26
| ~ spl2_94 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s253,plain,
( ~ spl2_30
| spl2_127 ),
inference(sat_conversion,[],[f2698]) ).
cnf(s258,plain,
( ~ spl2_25
| spl2_128 ),
inference(sat_conversion,[],[f2721]) ).
cnf(s269,plain,
( spl2_8
| ~ spl2_93 ),
inference(sat_conversion,[],[f2861]) ).
cnf(s279,plain,
( spl2_94
| ~ spl2_116 ),
inference(sat_conversion,[],[f2912]) ).
cnf(s288,plain,
( spl2_80
| ~ spl2_131 ),
inference(sat_conversion,[],[f2933]) ).
cnf(s289,plain,
( ~ spl2_25
| spl2_37
| ~ spl2_116 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s291,plain,
( ~ spl2_1
| spl2_7
| ~ spl2_30 ),
inference(sat_conversion,[],[f3076]) ).
cnf(s299,plain,
( ~ spl2_132
| ~ spl2_142 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s300,plain,
( ~ spl2_132
| ~ spl2_147
| spl2_148 ),
inference(sat_conversion,[],[f3139]) ).
cnf(s302,plain,
( ~ spl2_25
| ~ spl2_37
| spl2_141 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s320,plain,
( ~ spl2_2
| ~ spl2_64
| spl2_73 ),
inference(sat_conversion,[],[f3235]) ).
cnf(s324,plain,
( ~ spl2_5
| ~ spl2_24
| ~ spl2_48 ),
inference(sat_conversion,[],[f3248]) ).
cnf(s326,plain,
( ~ spl2_73
| spl2_140
| ~ spl2_148 ),
inference(sat_conversion,[],[f3266]) ).
cnf(s353,plain,
( ~ spl2_86
| spl2_141 ),
inference(sat_conversion,[],[f3457]) ).
cnf(s383,plain,
( spl2_79
| ~ spl2_101 ),
inference(sat_conversion,[],[f3728]) ).
cnf(s391,plain,
( ~ spl2_5
| ~ spl2_31
| spl2_138
| ~ spl2_143 ),
inference(sat_conversion,[],[f3777]) ).
cnf(s392,plain,
( ~ spl2_5
| ~ spl2_17
| spl2_123
| ~ spl2_143 ),
inference(sat_conversion,[],[f3779]) ).
cnf(s393,plain,
( ~ spl2_143
| ~ spl2_148 ),
inference(sat_conversion,[],[f3783]) ).
cnf(s395,plain,
( ~ spl2_115
| ~ spl2_124
| spl2_143 ),
inference(sat_conversion,[],[f3789]) ).
cnf(s397,plain,
( ~ spl2_115
| spl2_143
| ~ spl2_148 ),
inference(sat_conversion,[],[f3800]) ).
cnf(s398,plain,
( ~ spl2_104
| ~ spl2_124
| spl2_148 ),
inference(sat_conversion,[],[f3801]) ).
cnf(s400,plain,
( spl2_96
| ~ spl2_137 ),
inference(sat_conversion,[],[f3811]) ).
cnf(s401,plain,
( spl2_54
| ~ spl2_137 ),
inference(sat_conversion,[],[f3813]) ).
cnf(s402,plain,
( spl2_54
| ~ spl2_63 ),
inference(sat_conversion,[],[f3877]) ).
cnf(s403,plain,
( ~ spl2_46
| spl2_72 ),
inference(sat_conversion,[],[f3878]) ).
cnf(s407,plain,
( ~ spl2_72
| ~ spl2_73
| ~ spl2_115 ),
inference(sat_conversion,[],[f3935]) ).
cnf(s408,plain,
( ~ spl2_72
| spl2_94
| ~ spl2_115 ),
inference(sat_conversion,[],[f3937]) ).
cnf(s417,plain,
( spl2_54
| ~ spl2_144 ),
inference(sat_conversion,[],[f4035]) ).
cnf(s418,plain,
( ~ spl2_144
| spl2_147 ),
inference(sat_conversion,[],[f4037]) ).
cnf(s423,plain,
( spl2_139
| ~ spl2_140 ),
inference(sat_conversion,[],[f4089]) ).
cnf(s427,plain,
( ~ spl2_2
| spl2_52
| spl2_63
| ~ spl2_84
| spl2_144 ),
inference(sat_conversion,[],[f4430]) ).
cnf(s429,plain,
( spl2_1
| ~ spl2_52 ),
inference(sat_conversion,[],[f4445]) ).
cnf(s445,plain,
( spl2_44
| ~ spl2_112
| ~ spl2_114 ),
inference(sat_conversion,[],[f4544]) ).
cnf(s448,plain,
( ~ spl2_104
| spl2_120
| ~ spl2_124
| ~ spl2_138 ),
inference(sat_conversion,[],[f4548]) ).
cnf(s454,plain,
( ~ spl2_113
| ~ spl2_138 ),
inference(sat_conversion,[],[f4579]) ).
cnf(s460,plain,
( ~ spl2_4
| spl2_44
| ~ spl2_72 ),
inference(sat_conversion,[],[f4718]) ).
cnf(s461,plain,
( ~ spl2_44
| spl2_112
| ~ spl2_114 ),
inference(sat_conversion,[],[f4727]) ).
cnf(s472,plain,
( spl2_54
| ~ spl2_120 ),
inference(sat_conversion,[],[f4874]) ).
cnf(s477,plain,
( ~ spl2_12
| ~ spl2_23
| ~ spl2_25
| ~ spl2_34
| ~ spl2_38
| ~ spl2_75 ),
inference(sat_conversion,[],[f4987]) ).
cnf(s492,plain,
( spl2_4
| ~ spl2_44 ),
inference(sat_conversion,[],[f5028]) ).
cnf(s496,plain,
( ~ spl2_85
| spl2_138
| ~ spl2_139 ),
inference(sat_conversion,[],[f5052]) ).
cnf(s525,plain,
( ~ spl2_63
| spl2_137
| spl2_144 ),
inference(sat_conversion,[],[f5325]) ).
cnf(s526,plain,
( ~ spl2_114
| spl2_124 ),
inference(sat_conversion,[],[f5326]) ).
cnf(s527,plain,
( spl2_72
| ~ spl2_114 ),
inference(sat_conversion,[],[f5328]) ).
cnf(s545,plain,
( ~ spl2_46
| ~ spl2_54 ),
inference(sat_conversion,[],[f5461]) ).
cnf(s555,plain,
( ~ spl2_5
| ~ spl2_19
| ~ spl2_23
| spl2_24 ),
inference(sat_conversion,[],[f5468]) ).
cnf(s579,plain,
( ~ spl2_79
| spl2_129 ),
inference(sat_conversion,[],[f5494]) ).
cnf(s582,plain,
( ~ spl2_63
| ~ spl2_80 ),
inference(sat_conversion,[],[f5500]) ).
cnf(s624,plain,
( ~ spl2_5
| ~ spl2_48
| spl2_122 ),
inference(sat_conversion,[],[f5760]) ).
cnf(s625,plain,
( ~ spl2_48
| ~ spl2_79 ),
inference(sat_conversion,[],[f5761]) ).
cnf(s646,plain,
( ~ spl2_4
| spl2_9
| ~ spl2_54 ),
inference(sat_conversion,[],[f5857]) ).
cnf(s660,plain,
( spl2_46
| ~ spl2_92
| ~ spl2_94
| ~ spl2_117
| ~ spl2_128 ),
inference(sat_conversion,[],[f5921]) ).
cnf(s665,plain,
( ~ spl2_38
| ~ spl2_123 ),
inference(sat_conversion,[],[f5942]) ).
cnf(s672,plain,
( spl2_96
| ~ spl2_122 ),
inference(sat_conversion,[],[f6142]) ).
cnf(s673,plain,
( ~ spl2_47
| spl2_79 ),
inference(sat_conversion,[],[f6144]) ).
cnf(s674,plain,
( spl2_9
| ~ spl2_47 ),
inference(sat_conversion,[],[f6146]) ).
cnf(s676,plain,
( ~ spl2_17
| ~ spl2_47
| spl2_80 ),
inference(sat_conversion,[],[f6149]) ).
cnf(s692,plain,
( ~ spl2_18
| ~ spl2_47 ),
inference(sat_conversion,[],[f6182]) ).
cnf(s698,plain,
( spl2_8
| ~ spl2_18
| ~ spl2_95 ),
inference(sat_conversion,[],[f6193]) ).
cnf(s701,plain,
( ~ spl2_87
| ~ spl2_96
| spl2_137 ),
inference(sat_conversion,[],[f6215]) ).
cnf(s702,plain,
( ~ spl2_7
| ~ spl2_19
| spl2_80 ),
inference(sat_conversion,[],[f6220]) ).
cnf(s731,plain,
( ~ spl2_87
| ~ spl2_141
| spl2_142 ),
inference(sat_conversion,[],[f6256]) ).
cnf(s732,plain,
( ~ spl2_117
| ~ spl2_141
| spl2_143 ),
inference(sat_conversion,[],[f6257]) ).
cnf(s751,plain,
( ~ spl2_13
| ~ spl2_80
| ~ spl2_81
| ~ spl2_129 ),
inference(sat_conversion,[],[f6432]) ).
cnf(s753,plain,
( ~ spl2_16
| ~ spl2_47
| spl2_124 ),
inference(sat_conversion,[],[f6439]) ).
cnf(s759,plain,
( ~ spl2_4
| spl2_10
| ~ spl2_95 ),
inference(sat_conversion,[],[f6445]) ).
cnf(s761,plain,
( ~ spl2_112
| spl2_139 ),
inference(sat_conversion,[],[f6447]) ).
cnf(s762,plain,
( ~ spl2_112
| spl2_121 ),
inference(sat_conversion,[],[f6448]) ).
cnf(s787,plain,
spl2_12,
inference(rat,[],[s8,s91]) ).
cnf(s788,plain,
( spl2_9
| ~ spl2_117
| ~ spl2_19
| ~ spl2_5
| ~ spl2_4 ),
inference(rat,[],[s732,s392,s353,s665,s99,s34,s701,s39,s672,s555,s624,s324,s401,s11,s43,s646,s119,s674]) ).
cnf(s789,plain,
( spl2_122
| spl2_7
| ~ spl2_115
| ~ spl2_5
| ~ spl2_4 ),
inference(rat,[],[s391,s30,s395,s97,s753,s11,s454,s676,s156,s43,s762,s624,s180,s218,s31,s42,s35,s37,s12,s13]) ).
cnf(s790,plain,
( spl2_7
| ~ spl2_115
| ~ spl2_5
| ~ spl2_4 ),
inference(rat,[],[s158,s788,s279,s7,s107,s759,s131,s108,s672,s789,s12,s13]) ).
cnf(s791,plain,
( ~ spl2_95
| spl2_8
| ~ spl2_5
| ~ spl2_4 ),
inference(rat,[],[s788,s12,s7,s698,s759,s158,s279,s107,s269]) ).
cnf(s792,plain,
( ~ spl2_115
| ~ spl2_4
| ~ spl2_5 ),
inference(rat,[],[s751,s702,s579,s12,s673,s692,s43,s624,s672,s108,s791,s6,s790,s88,s93]) ).
cnf(s793,plain,
( spl2_3
| ~ spl2_2 ),
inference(rat,[],[s792,s157,s3,s527,s5,s460,s2,s150]) ).
cnf(s794,plain,
( ~ spl2_4
| spl2_1 ),
inference(rat,[],[s496,s448,s98,s132,s427,s761,s383,s402,s417,s472,s461,s191,s545,s460,s177,s526,s527,s157,s792,s3,s5,s429,s1]) ).
cnf(s795,plain,
( ~ spl2_95
| ~ spl2_115
| ~ spl2_2 ),
inference(rat,[],[s320,s176,s53,s408,s402,s107,s164,s131,s793,s91,s85,s787]) ).
cnf(s797,plain,
( ~ spl2_73
| ~ spl2_115 ),
inference(rat,[],[s176,s407]) ).
cnf(s798,plain,
( ~ spl2_115
| ~ spl2_2 ),
inference(rat,[],[s397,s393,s300,s222,s418,s288,s525,s582,s53,s320,s797,s400,s108,s795,s793]) ).
cnf(s799,plain,
spl2_1,
inference(rat,[],[s423,s326,s496,s398,s98,s132,s427,s383,s402,s417,s454,s191,s545,s156,s60,s177,s445,s526,s527,s157,s798,s58,s492,s794,s793,s1,s429]) ).
cnf(s800,plain,
( spl2_7
| ~ spl2_87
| ~ spl2_92
| ~ spl2_6
| spl2_46 ),
inference(rat,[],[s660,s158,s241,s258,s289,s302,s731,s25,s299,s226,s222,s30,s288,s291,s218,s799]) ).
cnf(s801,plain,
( spl2_3
| ~ spl2_115 ),
inference(rat,[],[s11,s215,s97,s253,s240,s30,s158,s226,s279,s25,s107,s243,s269,s6,s800,s99,s106,s109,s111,s110,s625,s44,s43,s3,s151,s153,s213,s403,s792,s460,s2,s150,s799]) ).
cnf(s804,plain,
( spl2_93
| spl2_5 ),
inference(rat,[],[s11,s215,s97,s253,s240,s30,s158,s226,s279,s25,s107,s243,s153,s3,s799]) ).
cnf(s805,plain,
spl2_5,
inference(rat,[],[s302,s731,s34,s299,s477,s222,s203,s288,s25,s218,s252,s6,s246,s269,s804,s99,s109,s110,s44,s3,s151,s787,s82,s96]) ).
cnf(s806,plain,
~ spl2_3,
inference(rat,[],[s4,s799,s805]) ).
cnf(s808,plain,
~ spl2_44,
inference(rat,[],[s150,s806]) ).
cnf(s809,plain,
spl2_4,
inference(rat,[],[s2,s806]) ).
cnf(s811,plain,
~ spl2_115,
inference(rat,[],[s801,s806]) ).
cnf(s812,plain,
~ spl2_72,
inference(rat,[],[s460,s808,s809]) ).
cnf(s813,plain,
spl2_114,
inference(rat,[],[s157,s811]) ).
cnf(s815,plain,
$false,
inference(rat,[],[s527,s813,s812]) ).
fof(f6519,plain,
$false,
inference(avatar_sat_refutation,[],[s815]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO169+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n010.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 07:21:16 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.76/2.31 % (607611)Detected formulas, will run a generic FOF schedule.
% 8.76/2.31 % (607622)dis-21_1_sil=8000:lcm=predicate:random_seed=335971719:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.76/2.31 % (607622)Instruction limit reached!
% 8.76/2.31 % (607622)------------------------------
% 8.76/2.31 % (607622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607622)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607622)Termination reason: Instruction limit
% 8.76/2.31 % (607622)Termination phase: Saturation
% 8.76/2.31 % (607622)Time elapsed: 0.040 s
% 8.76/2.31 % (607622)Peak memory usage: 89 MB
% 8.76/2.31 % (607622)Instructions burned: 132 (million)
% 8.76/2.31 % (607619)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2281094469:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.76/2.31 % (607617)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1696654738:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.76/2.31 % (607616)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=985519903:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.76/2.31 % (607620)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=225093710:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.76/2.31 % (607618)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2982087060:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.76/2.31 % (607621)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3806548960:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.76/2.31 % (607620)Refutation not found, incomplete strategy
% 8.76/2.31 % (607620)------------------------------
% 8.76/2.31 % (607620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607619)Refutation not found, incomplete strategy
% 8.76/2.31 % (607619)------------------------------
% 8.76/2.31 % (607619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607620)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607620)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607620)Time elapsed: 0.001 s
% 8.76/2.31 % (607620)Peak memory usage: 86 MB
% 8.76/2.31 % (607619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607619)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607619)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607619)Time elapsed: 0.001 s
% 8.76/2.31 % (607619)Peak memory usage: 86 MB
% 8.76/2.31 % (607621)Instruction limit reached!
% 8.76/2.31 % (607621)------------------------------
% 8.76/2.31 % (607621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607621)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607621)Termination reason: Instruction limit
% 8.76/2.31 % (607621)Termination phase: Saturation
% 8.76/2.31 % (607621)Time elapsed: 0.091 s
% 8.76/2.31 % (607621)Peak memory usage: 90 MB
% 8.76/2.31 % (607621)Instructions burned: 139 (million)
% 8.76/2.31 % (607630)lrs+10_1_sil=8000:sp=occurrence:random_seed=2898493130:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.76/2.31 % (607630)Refutation not found, incomplete strategy
% 8.76/2.31 % (607630)------------------------------
% 8.76/2.31 % (607630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607630)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607630)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607630)Time elapsed: 0.0000 s
% 8.76/2.31 % (607630)Peak memory usage: 86 MB
% 8.76/2.31 % (607620)------------------------------
% 8.76/2.31 % (607620)------------------------------
% 8.76/2.31 % (607619)------------------------------
% 8.76/2.31 % (607619)------------------------------
% 8.76/2.31 % (607631)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2756725260:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.76/2.31 % (607631)Refutation not found, incomplete strategy
% 8.76/2.31 % (607631)------------------------------
% 8.76/2.31 % (607631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607631)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607631)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607631)Time elapsed: 0.001 s
% 8.76/2.31 % (607631)Peak memory usage: 87 MB
% 8.76/2.31 % (607630)------------------------------
% 8.76/2.31 % (607630)------------------------------
% 8.76/2.31 % (607633)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4234449884:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 8.76/2.31 % (607634)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3089185024:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.76/2.31 % (607633)Refutation not found, incomplete strategy
% 8.76/2.31 % (607633)------------------------------
% 8.76/2.31 % (607633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607633)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607633)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607633)Time elapsed: 0.002 s
% 8.76/2.31 % (607633)Peak memory usage: 88 MB
% 8.76/2.31 % (607636)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=110267770:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.76/2.31 % (607636)Refutation not found, incomplete strategy
% 8.76/2.31 % (607636)------------------------------
% 8.76/2.31 % (607636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607636)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607636)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607636)Time elapsed: 0.001 s
% 8.76/2.31 % (607636)Peak memory usage: 88 MB
% 8.76/2.31 % (607636)Instructions burned: 1 (million)
% 8.76/2.31 % (607631)------------------------------
% 8.76/2.31 % (607631)------------------------------
% 8.76/2.31 % (607634)Instruction limit reached!
% 8.76/2.31 % (607634)------------------------------
% 8.76/2.31 % (607634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607634)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607634)Termination reason: Instruction limit
% 8.76/2.31 % (607634)Termination phase: Saturation
% 8.76/2.31 % (607634)Time elapsed: 0.121 s
% 8.76/2.31 % (607634)Peak memory usage: 90 MB
% 8.76/2.31 % (607634)Instructions burned: 249 (million)
% 8.76/2.31 % (607636)------------------------------
% 8.76/2.31 % (607636)------------------------------
% 8.76/2.31 % (607633)------------------------------
% 8.76/2.31 % (607633)------------------------------
% 8.76/2.31 % (607640)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3422910014:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.76/2.31 % (607641)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=549187835:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.76/2.31 % (607642)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=600772275:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 8.76/2.31 % (607642)Instruction limit reached!
% 8.76/2.31 % (607642)------------------------------
% 8.76/2.31 % (607642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607642)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607642)Termination reason: Instruction limit
% 8.76/2.31 % (607642)Termination phase: Saturation
% 8.76/2.31 % (607642)Time elapsed: 0.035 s
% 8.76/2.31 % (607642)Peak memory usage: 88 MB
% 8.76/2.31 % (607642)Instructions burned: 128 (million)
% 8.76/2.31 % (607641)Instruction limit reached!
% 8.76/2.31 % (607641)------------------------------
% 8.76/2.31 % (607641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607641)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607641)Termination reason: Instruction limit
% 8.76/2.31 % (607641)Termination phase: Saturation
% 8.76/2.31 % (607641)Time elapsed: 0.078 s
% 8.76/2.31 % (607641)Peak memory usage: 90 MB
% 8.76/2.31 % (607641)Instructions burned: 114 (million)
% 8.76/2.31 % (607644)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=644521776:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.76/2.31 % (607644)Refutation not found, incomplete strategy
% 8.76/2.31 % (607644)------------------------------
% 8.76/2.31 % (607644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607644)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607644)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607644)Time elapsed: 0.001 s
% 8.76/2.31 % (607644)Peak memory usage: 87 MB
% 8.76/2.31 % (607648)lrs+10_1_sil=8000:sp=occurrence:random_seed=3278904818:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 8.76/2.31 % (607648)Refutation not found, incomplete strategy
% 8.76/2.31 % (607648)------------------------------
% 8.76/2.31 % (607648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607648)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607648)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607648)Time elapsed: 0.0000 s
% 8.76/2.31 % (607648)Peak memory usage: 86 MB
% 8.76/2.31 % (607649)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1462907240:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.76/2.31 % (607649)Refutation not found, incomplete strategy
% 8.76/2.31 % (607649)------------------------------
% 8.76/2.31 % (607649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607649)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607649)Termination reason: Refutation not found, incomplete strategy
% 8.76/2.31 % (607649)Time elapsed: 0.002 s
% 8.76/2.31 % (607649)Peak memory usage: 88 MB
% 8.76/2.31 % (607649)Instructions burned: 1 (million)
% 8.76/2.31 % (607648)------------------------------
% 8.76/2.31 % (607648)------------------------------
% 8.76/2.31 % (607616)First to succeed.
% 8.76/2.31 % (607616)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-607611"
% 8.76/2.31 % (607644)------------------------------
% 8.76/2.31 % (607644)------------------------------
% 8.76/2.31 % (607653)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=967469420:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 8.76/2.31 % (607649)------------------------------
% 8.76/2.31 % (607649)------------------------------
% 8.76/2.31 % (607654)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=698314103:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 8.76/2.31 % (607654)Instruction limit reached!
% 8.76/2.31 % (607654)------------------------------
% 8.76/2.31 % (607654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.31 % (607654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.31 % (607654)CaDiCaL version: 2.1.3
% 8.76/2.31 % (607654)Termination reason: Instruction limit
% 8.76/2.31 % (607654)Termination phase: Saturation
% 8.76/2.31 % (607654)Time elapsed: 0.065 s
% 8.76/2.31 % (607654)Peak memory usage: 90 MB
% 8.76/2.31 % (607654)Instructions burned: 134 (million)
% 8.76/2.31 % (607616)Refutation found. Thanks to Tanya!
% 8.76/2.31 % SZS status Theorem for theBenchmark
% 8.76/2.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/2.51 % (607616)------------------------------
% 0.16/2.51 % (607616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.51 % (607616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.51 % (607616)CaDiCaL version: 2.1.3
% 0.16/2.51 % (607616)Termination reason: Refutation
% 0.16/2.51 % (607616)Time elapsed: 1.018 s
% 0.16/2.51 % (607616)Peak memory usage: 131 MB
% 0.16/2.51 % (607616)Instructions burned: 1484 (million)
% 0.16/2.51 % (607616)------------------------------
% 0.16/2.51 % (607616)------------------------------
% 0.16/2.51 % (607611)Success in time 1.448 s
% 0.16/2.51 % Vampire exiting
%------------------------------------------------------------------------------