%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO169+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:53:45 AM UTC 2026
% Result : Theorem 1.73s 0.77s
% Output : Refutation 1.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 137
% Syntax : Number of formulae : 977 ( 114 unt; 89 def)
% Number of atoms : 2769 ( 361 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 3273 (1481 ~;1669 |; 17 &)
% ( 89 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 95 ( 93 usr; 91 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 19 con; 0-2 aty)
% Number of variables : 198 ( 0 sgn 192 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ( incident(p3,X0)
& incident(p1,X0)
& incident(p2,X0) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_normal) ).
fof(f2,axiom,
( ( incident(a1,b2b3)
& incident(a2,b3b1)
& incident(a3,b1b2) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_a_in_b) ).
fof(f3,axiom,
( ( incident(b1,a2a3)
& incident(b2,a3a1)
& incident(b3,a1a2) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_b_in_a) ).
fof(f4,axiom,
( incident(a1,b2b3)
| incident(b3,a1a2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gap1) ).
fof(f5,axiom,
( incident(a2,b3b1)
| incident(b1,a2a3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gap2) ).
fof(f6,axiom,
( incident(a3,b1b2)
| incident(b2,a3a1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gap3) ).
fof(f7,axiom,
incident(a1,a1a2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia1a2) ).
fof(f8,axiom,
incident(a2,a1a2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia2a1) ).
fof(f9,axiom,
incident(a2,a2a3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia2a3) ).
fof(f10,axiom,
incident(a3,a2a3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia3a2) ).
fof(f11,axiom,
incident(a3,a3a1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia3a1) ).
fof(f12,axiom,
incident(a1,a3a1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia1a3) ).
fof(f13,axiom,
incident(b1,b1b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib1b2) ).
fof(f14,axiom,
incident(b2,b1b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib2b1) ).
fof(f15,axiom,
incident(b2,b2b3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib2b3) ).
fof(f16,axiom,
incident(b3,b2b3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib3b2) ).
fof(f17,axiom,
incident(b3,b3b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib3b1) ).
fof(f18,axiom,
incident(b1,b3b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib1b3) ).
fof(f19,axiom,
incident(s,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',iss1) ).
fof(f20,axiom,
incident(s,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',iss2) ).
fof(f21,axiom,
incident(s,s3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',iss3) ).
fof(f22,axiom,
incident(a1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia1s1) ).
fof(f23,axiom,
incident(a2,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia2s2) ).
fof(f24,axiom,
incident(a3,s3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ia3s3) ).
fof(f25,axiom,
incident(b1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib1s1) ).
fof(f26,axiom,
incident(b2,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib2s2) ).
fof(f27,axiom,
incident(b3,s3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ib3s3) ).
fof(f28,axiom,
incident(p3,a1a2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ip3a) ).
fof(f29,axiom,
incident(p3,b1b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ip3b) ).
fof(f30,axiom,
incident(p1,a2a3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ip1a) ).
fof(f31,axiom,
incident(p1,b2b3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ip1b) ).
fof(f32,axiom,
incident(p2,a3a1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ip2a) ).
fof(f33,axiom,
incident(p2,b3b1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ip2b) ).
fof(f34,axiom,
! [X0,X1] :
( incident(X0,X1)
=> point(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_point) ).
fof(f35,axiom,
! [X0,X1] :
( incident(X0,X1)
=> line(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sort_line) ).
fof(f36,axiom,
( a1 = a2
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_a1_a2) ).
fof(f37,axiom,
( a2 = a3
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_a2_a3) ).
fof(f38,axiom,
( a3 = a1
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_a3_a1) ).
fof(f39,axiom,
( b1 = b2
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_b1_b2) ).
fof(f40,axiom,
( b2 = b3
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_b2_b3) ).
fof(f41,axiom,
( b3 = b1
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_b3_b1) ).
fof(f42,axiom,
( a1a2 = b1b2
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not12) ).
fof(f43,axiom,
( a2a3 = b2b3
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not23) ).
fof(f44,axiom,
( a3a1 = b3b1
=> goal ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',unique) ).
fof(f51,axiom,
! [X0,X1] :
( ( point(X0)
& point(X1) )
=> ? [X2] :
( incident(X0,X2)
& incident(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join) ).
fof(f52,axiom,
! [X0,X1] :
( ( line(X0)
& line(X1) )
=> ? [X2] :
( incident(X2,X0)
& incident(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet) ).
fof(f53,conjecture,
goal,
file('/export/starexec/sandbox/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(f68,plain,
( goal
| b2 != b3 ),
inference(ennf_transformation,[],[f40]) ).
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] :
( ~ incident(p2,X0)
| ~ incident(p1,X0)
| ~ incident(p3,X0)
| goal ),
inference(cnf_transformation,[],[f57]) ).
fof(f87,plain,
( ~ incident(a3,b1b2)
| ~ incident(a2,b3b1)
| ~ incident(a1,b2b3)
| goal ),
inference(cnf_transformation,[],[f59]) ).
fof(f88,plain,
( ~ incident(b3,a1a2)
| ~ incident(b2,a3a1)
| ~ incident(b1,a2a3)
| goal ),
inference(cnf_transformation,[],[f61]) ).
fof(f89,plain,
( incident(b3,a1a2)
| incident(a1,b2b3) ),
inference(cnf_transformation,[],[f4]) ).
fof(f90,plain,
( incident(b1,a2a3)
| incident(a2,b3b1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
( incident(b2,a3a1)
| incident(a3,b1b2) ),
inference(cnf_transformation,[],[f6]) ).
fof(f92,plain,
incident(a1,a1a2),
inference(cnf_transformation,[],[f7]) ).
fof(f93,plain,
incident(a2,a1a2),
inference(cnf_transformation,[],[f8]) ).
fof(f94,plain,
incident(a2,a2a3),
inference(cnf_transformation,[],[f9]) ).
fof(f95,plain,
incident(a3,a2a3),
inference(cnf_transformation,[],[f10]) ).
fof(f96,plain,
incident(a3,a3a1),
inference(cnf_transformation,[],[f11]) ).
fof(f97,plain,
incident(a1,a3a1),
inference(cnf_transformation,[],[f12]) ).
fof(f98,plain,
incident(b1,b1b2),
inference(cnf_transformation,[],[f13]) ).
fof(f99,plain,
incident(b2,b1b2),
inference(cnf_transformation,[],[f14]) ).
fof(f100,plain,
incident(b2,b2b3),
inference(cnf_transformation,[],[f15]) ).
fof(f101,plain,
incident(b3,b2b3),
inference(cnf_transformation,[],[f16]) ).
fof(f102,plain,
incident(b3,b3b1),
inference(cnf_transformation,[],[f17]) ).
fof(f103,plain,
incident(b1,b3b1),
inference(cnf_transformation,[],[f18]) ).
fof(f104,plain,
incident(s,s1),
inference(cnf_transformation,[],[f19]) ).
fof(f105,plain,
incident(s,s2),
inference(cnf_transformation,[],[f20]) ).
fof(f106,plain,
incident(s,s3),
inference(cnf_transformation,[],[f21]) ).
fof(f107,plain,
incident(a1,s1),
inference(cnf_transformation,[],[f22]) ).
fof(f108,plain,
incident(a2,s2),
inference(cnf_transformation,[],[f23]) ).
fof(f109,plain,
incident(a3,s3),
inference(cnf_transformation,[],[f24]) ).
fof(f110,plain,
incident(b1,s1),
inference(cnf_transformation,[],[f25]) ).
fof(f111,plain,
incident(b2,s2),
inference(cnf_transformation,[],[f26]) ).
fof(f112,plain,
incident(b3,s3),
inference(cnf_transformation,[],[f27]) ).
fof(f113,plain,
incident(p3,a1a2),
inference(cnf_transformation,[],[f28]) ).
fof(f114,plain,
incident(p3,b1b2),
inference(cnf_transformation,[],[f29]) ).
fof(f115,plain,
incident(p1,a2a3),
inference(cnf_transformation,[],[f30]) ).
fof(f116,plain,
incident(p1,b2b3),
inference(cnf_transformation,[],[f31]) ).
fof(f117,plain,
incident(p2,a3a1),
inference(cnf_transformation,[],[f32]) ).
fof(f118,plain,
incident(p2,b3b1),
inference(cnf_transformation,[],[f33]) ).
fof(f119,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| point(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f120,plain,
! [X0,X1] :
( ~ incident(X0,X1)
| line(X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f121,plain,
( a1 != a2
| goal ),
inference(cnf_transformation,[],[f64]) ).
fof(f122,plain,
( a2 != a3
| goal ),
inference(cnf_transformation,[],[f65]) ).
fof(f123,plain,
( a1 != a3
| goal ),
inference(cnf_transformation,[],[f66]) ).
fof(f124,plain,
( b1 != b2
| goal ),
inference(cnf_transformation,[],[f67]) ).
fof(f125,plain,
( b2 != b3
| goal ),
inference(cnf_transformation,[],[f68]) ).
fof(f126,plain,
( b1 != b3
| goal ),
inference(cnf_transformation,[],[f69]) ).
fof(f127,plain,
( b1b2 != a1a2
| goal ),
inference(cnf_transformation,[],[f70]) ).
fof(f128,plain,
( b2b3 != a2a3
| goal ),
inference(cnf_transformation,[],[f71]) ).
fof(f129,plain,
( b3b1 != a3a1
| goal ),
inference(cnf_transformation,[],[f72]) ).
fof(f134,plain,
! [X2,X3,X0,X1] :
( ~ incident(X1,X3)
| ~ incident(X1,X2)
| ~ incident(X0,X3)
| ~ incident(X0,X2)
| X2 = X3
| X0 = X1 ),
inference(cnf_transformation,[],[f81]) ).
fof(f135,plain,
! [X0,X1] :
( incident(X1,sK0(X0,X1))
| ~ point(X0)
| ~ point(X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f136,plain,
! [X0,X1] :
( incident(X0,sK0(X0,X1))
| ~ point(X0)
| ~ point(X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f137,plain,
! [X0,X1] :
( incident(sK1(X0,X1),X1)
| ~ line(X0)
| ~ line(X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f138,plain,
! [X0,X1] :
( incident(sK1(X0,X1),X0)
| ~ line(X0)
| ~ line(X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f139,plain,
~ goal,
inference(cnf_transformation,[],[f55]) ).
fof(f145,definition,
( spl2_1
<=> goal ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f147,plain,
( goal
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f149,definition,
( spl2_2
<=> b3b1 = a3a1 ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f151,plain,
( b3b1 != a3a1
| spl2_2 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f152,plain,
( spl2_1
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f129,f149,f145]) ).
fof(f154,definition,
( spl2_3
<=> b2b3 = a2a3 ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f156,plain,
( b2b3 != a2a3
| spl2_3 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,plain,
( spl2_1
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f128,f154,f145]) ).
fof(f159,definition,
( spl2_4
<=> b1b2 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f161,plain,
( b1b2 != a1a2
| spl2_4 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f162,plain,
( spl2_1
| ~ spl2_4 ),
inference(avatar_split_clause,[],[f127,f159,f145]) ).
fof(f164,definition,
( spl2_5
<=> b1 = b3 ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f166,plain,
( b1 != b3
| spl2_5 ),
inference(avatar_component_clause,[],[f164]) ).
fof(f167,plain,
( spl2_1
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f126,f164,f145]) ).
fof(f169,definition,
( spl2_6
<=> b2 = b3 ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f171,plain,
( b2 != b3
| spl2_6 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f172,plain,
( spl2_1
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f125,f169,f145]) ).
fof(f174,definition,
( spl2_7
<=> b1 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f176,plain,
( b1 != b2
| spl2_7 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f177,plain,
( spl2_1
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f124,f174,f145]) ).
fof(f179,definition,
( spl2_8
<=> a1 = a3 ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f181,plain,
( a1 != a3
| spl2_8 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f182,plain,
( spl2_1
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f123,f179,f145]) ).
fof(f184,definition,
( spl2_9
<=> a2 = a3 ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f186,plain,
( a2 != a3
| spl2_9 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f187,plain,
( spl2_1
| ~ spl2_9 ),
inference(avatar_split_clause,[],[f122,f184,f145]) ).
fof(f189,definition,
( spl2_10
<=> a1 = a2 ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f191,plain,
( a1 != a2
| spl2_10 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f192,plain,
( spl2_1
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f121,f189,f145]) ).
fof(f194,definition,
( spl2_11
<=> incident(a3,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f195,plain,
( ~ incident(a3,b1b2)
| spl2_11 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f196,plain,
( incident(a3,b1b2)
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f198,definition,
( spl2_12
<=> incident(b2,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f199,plain,
( ~ incident(b2,a3a1)
| spl2_12 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f200,plain,
( incident(b2,a3a1)
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f201,plain,
( spl2_11
| spl2_12 ),
inference(avatar_split_clause,[],[f91,f198,f194]) ).
fof(f203,definition,
( spl2_13
<=> incident(a2,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f204,plain,
( ~ incident(a2,b3b1)
| spl2_13 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f205,plain,
( incident(a2,b3b1)
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f207,definition,
( spl2_14
<=> incident(b1,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f209,plain,
( incident(b1,a2a3)
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,plain,
( spl2_13
| spl2_14 ),
inference(avatar_split_clause,[],[f90,f207,f203]) ).
fof(f212,definition,
( spl2_15
<=> incident(a1,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition]) ).
fof(f213,plain,
( ~ incident(a1,b2b3)
| spl2_15 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f214,plain,
( incident(a1,b2b3)
| ~ spl2_15 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f216,definition,
( spl2_16
<=> incident(b3,a1a2) ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
fof(f218,plain,
( incident(b3,a1a2)
| ~ spl2_16 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,plain,
( spl2_15
| spl2_16 ),
inference(avatar_split_clause,[],[f89,f216,f212]) ).
fof(f220,plain,
( spl2_1
| ~ spl2_14
| ~ spl2_12
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f88,f216,f198,f207,f145]) ).
fof(f221,plain,
( spl2_1
| ~ spl2_15
| ~ spl2_13
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f87,f194,f203,f212,f145]) ).
fof(f223,definition,
( spl2_17
<=> ! [X0] :
( ~ incident(p2,X0)
| ~ incident(p3,X0)
| ~ incident(p1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f224,plain,
( ! [X0] :
( ~ incident(p2,X0)
| ~ incident(p3,X0)
| ~ incident(p1,X0) )
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( spl2_1
| spl2_17 ),
inference(avatar_split_clause,[],[f86,f223,f145]) ).
fof(f226,plain,
( $false
| ~ spl2_1 ),
inference(forward_subsumption_resolution,[],[f139,f147]) ).
fof(f227,plain,
~ spl2_1,
inference(avatar_contradiction_clause,[],[f226]) ).
fof(f230,plain,
point(p1),
inference(resolution,[],[f119,f116]) ).
fof(f231,plain,
point(p2),
inference(resolution,[],[f119,f118]) ).
fof(f235,plain,
point(p3),
inference(resolution,[],[f119,f114]) ).
fof(f239,plain,
point(a2),
inference(resolution,[],[f119,f94]) ).
fof(f240,plain,
point(a3),
inference(resolution,[],[f119,f95]) ).
fof(f243,plain,
point(a1),
inference(resolution,[],[f119,f97]) ).
fof(f258,plain,
line(b2b3),
inference(resolution,[],[f120,f100]) ).
fof(f261,plain,
line(b3b1),
inference(resolution,[],[f120,f118]) ).
fof(f269,plain,
line(a2a3),
inference(resolution,[],[f120,f94]) ).
fof(f285,plain,
line(s3),
inference(resolution,[],[f120,f106]) ).
fof(f297,plain,
( ~ incident(p3,a3a1)
| ~ incident(p1,a3a1)
| ~ spl2_17 ),
inference(resolution,[],[f224,f117]) ).
fof(f298,plain,
( ! [X0] :
( ~ incident(p3,sK0(X0,p2))
| ~ incident(p1,sK0(X0,p2))
| ~ point(X0)
| ~ point(p2) )
| ~ spl2_17 ),
inference(resolution,[],[f224,f135]) ).
fof(f299,plain,
( ! [X0] :
( ~ incident(p3,sK0(p2,X0))
| ~ incident(p1,sK0(p2,X0))
| ~ point(p2)
| ~ point(X0) )
| ~ spl2_17 ),
inference(resolution,[],[f224,f136]) ).
fof(f300,plain,
( ! [X0] :
( ~ incident(p1,sK0(p2,X0))
| ~ incident(p3,sK0(p2,X0))
| ~ point(X0) )
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f299,f231]) ).
fof(f301,plain,
( ! [X0] :
( ~ incident(p1,sK0(X0,p2))
| ~ incident(p3,sK0(X0,p2))
| ~ point(X0) )
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f298,f231]) ).
fof(f303,definition,
( spl2_18
<=> incident(p1,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f305,plain,
( ~ incident(p1,a3a1)
| spl2_18 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl2_19
<=> incident(p3,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f309,plain,
( ~ incident(p3,a3a1)
| spl2_19 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( ~ spl2_18
| ~ spl2_19
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f297,f223,f307,f303]) ).
fof(f320,plain,
( ~ incident(p3,sK0(p2,p1))
| ~ point(p1)
| ~ point(p2)
| ~ point(p1)
| ~ spl2_17 ),
inference(resolution,[],[f300,f135]) ).
fof(f321,plain,
( ~ incident(p3,sK0(p2,p1))
| ~ point(p1)
| ~ point(p2)
| ~ spl2_17 ),
inference(duplicate_literal_removal,[],[f320]) ).
fof(f322,plain,
( ~ incident(p3,sK0(p2,p1))
| ~ point(p2)
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f321,f230]) ).
fof(f323,plain,
( ~ incident(p3,sK0(p2,p1))
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f322,f231]) ).
fof(f324,plain,
( ~ incident(p3,sK0(p1,p2))
| ~ point(p1)
| ~ point(p1)
| ~ point(p2)
| ~ spl2_17 ),
inference(resolution,[],[f301,f136]) ).
fof(f325,plain,
( ~ incident(p3,sK0(p1,p2))
| ~ point(p1)
| ~ point(p2)
| ~ spl2_17 ),
inference(duplicate_literal_removal,[],[f324]) ).
fof(f326,plain,
( ~ incident(p3,sK0(p1,p2))
| ~ point(p2)
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f325,f230]) ).
fof(f327,plain,
( ~ incident(p3,sK0(p1,p2))
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f326,f231]) ).
fof(f330,plain,
! [X0,X1] :
( ~ incident(b2,X0)
| ~ incident(X1,b2b3)
| ~ incident(X1,X0)
| b2b3 = X0
| b2 = X1 ),
inference(resolution,[],[f134,f100]) ).
fof(f331,plain,
! [X0,X1] :
( ~ incident(b3,X0)
| ~ incident(X1,b2b3)
| ~ incident(X1,X0)
| b2b3 = X0
| b3 = X1 ),
inference(resolution,[],[f134,f101]) ).
fof(f332,plain,
! [X0,X1] :
( ~ incident(p1,X0)
| ~ incident(X1,b2b3)
| ~ incident(X1,X0)
| b2b3 = X0
| p1 = X1 ),
inference(resolution,[],[f134,f116]) ).
fof(f333,plain,
! [X0,X1] :
( ~ incident(p2,X0)
| ~ incident(X1,b3b1)
| ~ incident(X1,X0)
| b3b1 = X0
| p2 = X1 ),
inference(resolution,[],[f134,f118]) ).
fof(f335,plain,
! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,b3b1)
| ~ incident(X1,X0)
| b3b1 = X0
| b1 = X1 ),
inference(resolution,[],[f134,f103]) ).
fof(f336,plain,
! [X0,X1] :
( ~ incident(b3,X0)
| ~ incident(X1,b3b1)
| ~ incident(X1,X0)
| b3b1 = X0
| b3 = X1 ),
inference(resolution,[],[f134,f102]) ).
fof(f337,plain,
! [X0,X1] :
( ~ incident(p3,X0)
| ~ incident(X1,b1b2)
| ~ incident(X1,X0)
| b1b2 = X0
| p3 = X1 ),
inference(resolution,[],[f134,f114]) ).
fof(f339,plain,
! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,b1b2)
| ~ incident(X1,X0)
| b1b2 = X0
| b1 = X1 ),
inference(resolution,[],[f134,f98]) ).
fof(f341,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,a2a3)
| ~ incident(X1,X0)
| a2a3 = X0
| a2 = X1 ),
inference(resolution,[],[f134,f94]) ).
fof(f345,plain,
! [X0,X1] :
( ~ incident(X1,a3a1)
| ~ incident(a1,X0)
| ~ incident(X1,X0)
| a3a1 = X0
| a1 = X1 ),
inference(resolution,[],[f134,f97]) ).
fof(f348,plain,
! [X0,X1] :
( ~ incident(X1,a1a2)
| ~ incident(a1,X0)
| ~ incident(X1,X0)
| a1a2 = X0
| a1 = X1 ),
inference(resolution,[],[f134,f92]) ).
fof(f349,plain,
! [X0,X1] :
( ~ incident(a2,X0)
| ~ incident(X1,a1a2)
| ~ incident(X1,X0)
| a1a2 = X0
| a2 = X1 ),
inference(resolution,[],[f134,f93]) ).
fof(f353,plain,
! [X0,X1] :
( ~ incident(b1,X0)
| ~ incident(X1,s1)
| ~ incident(X1,X0)
| s1 = X0
| b1 = X1 ),
inference(resolution,[],[f134,f110]) ).
fof(f358,plain,
! [X0,X1] :
( ~ incident(a3,X0)
| ~ incident(X1,s3)
| ~ incident(X1,X0)
| s3 = X0
| a3 = X1 ),
inference(resolution,[],[f134,f109]) ).
fof(f361,plain,
! [X2,X3,X0,X1] :
( ~ incident(X0,X1)
| ~ incident(X2,sK0(X0,X3))
| ~ incident(X2,X1)
| sK0(X0,X3) = X1
| X0 = X2
| ~ point(X0)
| ~ point(X3) ),
inference(resolution,[],[f134,f136]) ).
fof(f362,plain,
! [X2,X3,X0,X1] :
( ~ incident(X2,sK0(X0,X3))
| ~ incident(X0,X1)
| ~ incident(X2,X1)
| sK0(X0,X3) = X1
| X0 = X2
| ~ point(X3) ),
inference(forward_subsumption_resolution,[],[f361,f119]) ).
fof(f367,plain,
! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,b1b2)
| b2b3 = b1b2
| b2 = X0 ),
inference(resolution,[],[f330,f99]) ).
fof(f368,plain,
! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,s2)
| b2b3 = s2
| b2 = X0 ),
inference(resolution,[],[f330,f111]) ).
fof(f375,definition,
( spl2_22
<=> b2b3 = s2 ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
fof(f377,plain,
( b2b3 = s2
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f379,definition,
( spl2_23
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b2 = X0
| ~ incident(X0,s2) ) ),
introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition]) ).
fof(f380,plain,
( ! [X0] :
( ~ incident(X0,s2)
| b2 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_23 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f381,plain,
( spl2_22
| spl2_23 ),
inference(avatar_split_clause,[],[f368,f379,f375]) ).
fof(f383,definition,
( spl2_24
<=> b2b3 = b1b2 ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f385,plain,
( b2b3 = b1b2
| ~ spl2_24 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f387,definition,
( spl2_25
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b2 = X0
| ~ incident(X0,b1b2) ) ),
introduced(definition,[new_symbols(definition,[spl2_25])],[avatar_definition]) ).
fof(f388,plain,
( ! [X0] :
( ~ incident(X0,b1b2)
| b2 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_25 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f389,plain,
( spl2_24
| spl2_25 ),
inference(avatar_split_clause,[],[f367,f387,f383]) ).
fof(f392,plain,
( incident(a2,b2b3)
| ~ spl2_22 ),
inference(superposition,[],[f108,f377]) ).
fof(f393,plain,
( incident(s,b2b3)
| ~ spl2_22 ),
inference(superposition,[],[f105,f377]) ).
fof(f402,plain,
( b1 = b2
| ~ incident(b1,b2b3)
| ~ spl2_25 ),
inference(resolution,[],[f388,f98]) ).
fof(f408,plain,
( ~ incident(b1,b2b3)
| spl2_7
| ~ spl2_25 ),
inference(forward_subsumption_resolution,[],[f402,f176]) ).
fof(f410,definition,
( spl2_26
<=> incident(a3,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_26])],[avatar_definition]) ).
fof(f411,plain,
( incident(a3,b2b3)
| ~ spl2_26 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f412,plain,
( ~ incident(a3,b2b3)
| spl2_26 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f414,definition,
( spl2_27
<=> a3 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f415,plain,
( a3 != b2
| spl2_27 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f416,plain,
( a3 = b2
| ~ spl2_27 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f419,definition,
( spl2_28
<=> incident(p3,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_28])],[avatar_definition]) ).
fof(f420,plain,
( incident(p3,b2b3)
| ~ spl2_28 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f421,plain,
( ~ incident(p3,b2b3)
| spl2_28 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f423,definition,
( spl2_29
<=> p3 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_29])],[avatar_definition]) ).
fof(f424,plain,
( p3 != b2
| spl2_29 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f425,plain,
( p3 = b2
| ~ spl2_29 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f467,plain,
! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,s3)
| b2b3 = s3
| b3 = X0 ),
inference(resolution,[],[f331,f112]) ).
fof(f474,definition,
( spl2_30
<=> b2b3 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_30])],[avatar_definition]) ).
fof(f476,plain,
( b2b3 = s3
| ~ spl2_30 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f478,definition,
( spl2_31
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b3 = X0
| ~ incident(X0,s3) ) ),
introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition]) ).
fof(f479,plain,
( ! [X0] :
( ~ incident(X0,s3)
| b3 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_31 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( spl2_30
| spl2_31 ),
inference(avatar_split_clause,[],[f467,f478,f474]) ).
fof(f482,definition,
( spl2_32
<=> b2b3 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_32])],[avatar_definition]) ).
fof(f484,plain,
( b2b3 = a1a2
| ~ spl2_32 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f486,definition,
( spl2_33
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b3 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f487,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| b3 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_33 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f499,plain,
( incident(a3,b2b3)
| ~ spl2_30 ),
inference(superposition,[],[f109,f476]) ).
fof(f500,plain,
( incident(s,b2b3)
| ~ spl2_30 ),
inference(superposition,[],[f106,f476]) ).
fof(f503,plain,
( a2 = b3
| ~ incident(a2,b2b3)
| ~ spl2_33 ),
inference(resolution,[],[f487,f93]) ).
fof(f509,plain,
( a2 = b3
| ~ spl2_22
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f503,f392]) ).
fof(f513,plain,
( a2 != b1
| spl2_5
| ~ spl2_22
| ~ spl2_33 ),
inference(superposition,[],[f166,f509]) ).
fof(f534,definition,
( spl2_37
<=> incident(p2,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f535,plain,
( incident(p2,b2b3)
| ~ spl2_37 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f536,plain,
( ~ incident(p2,b2b3)
| spl2_37 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f550,plain,
! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,a2a3)
| b2b3 = a2a3
| p1 = X0 ),
inference(resolution,[],[f332,f115]) ).
fof(f556,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,b2b3)
| p1 = X0 )
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f550,f156]) ).
fof(f557,plain,
( ~ incident(a2,b2b3)
| p1 = a2
| spl2_3 ),
inference(resolution,[],[f556,f94]) ).
fof(f558,plain,
( ~ incident(a3,b2b3)
| p1 = a3
| spl2_3 ),
inference(resolution,[],[f556,f95]) ).
fof(f560,plain,
( ! [X0] :
( ~ incident(sK1(a2a3,X0),b2b3)
| p1 = sK1(a2a3,X0)
| ~ line(a2a3)
| ~ line(X0) )
| spl2_3 ),
inference(resolution,[],[f556,f138]) ).
fof(f561,plain,
( ! [X0] :
( ~ incident(sK1(X0,a2a3),b2b3)
| p1 = sK1(X0,a2a3)
| ~ line(X0)
| ~ line(a2a3) )
| spl2_3 ),
inference(resolution,[],[f556,f137]) ).
fof(f562,plain,
( ! [X0] :
( ~ incident(sK1(X0,a2a3),b2b3)
| p1 = sK1(X0,a2a3)
| ~ line(X0) )
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f561,f269]) ).
fof(f563,plain,
( ! [X0] :
( ~ incident(sK1(a2a3,X0),b2b3)
| p1 = sK1(a2a3,X0)
| ~ line(X0) )
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f560,f269]) ).
fof(f565,plain,
( p1 = a2
| spl2_3
| ~ spl2_22 ),
inference(forward_subsumption_resolution,[],[f557,f392]) ).
fof(f605,plain,
( a2 = a3
| ~ incident(a3,b2b3)
| spl2_3
| ~ spl2_22 ),
inference(forward_demodulation,[],[f558,f565]) ).
fof(f607,definition,
( spl2_38
<=> p3 = a2 ),
introduced(definition,[new_symbols(definition,[spl2_38])],[avatar_definition]) ).
fof(f609,plain,
( p3 = a2
| ~ spl2_38 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f611,plain,
( ~ incident(a3,b2b3)
| spl2_3
| spl2_9
| ~ spl2_22 ),
inference(forward_subsumption_resolution,[],[f605,f186]) ).
fof(f627,plain,
( $false
| spl2_26
| ~ spl2_30 ),
inference(forward_subsumption_resolution,[],[f499,f412]) ).
fof(f628,plain,
( spl2_26
| ~ spl2_30 ),
inference(avatar_contradiction_clause,[],[f627]) ).
fof(f629,plain,
( ! [X0] :
( ~ incident(X0,s3)
| ~ incident(X0,b2b3)
| a2 = X0 )
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33 ),
inference(forward_demodulation,[],[f479,f509]) ).
fof(f636,plain,
( ~ incident(a2,sK0(p2,p1))
| ~ spl2_17
| ~ spl2_38 ),
inference(superposition,[],[f323,f609]) ).
fof(f652,plain,
( incident(a1,b2b3)
| ~ spl2_32 ),
inference(superposition,[],[f92,f484]) ).
fof(f659,plain,
( $false
| spl2_15
| ~ spl2_32 ),
inference(forward_subsumption_resolution,[],[f652,f213]) ).
fof(f660,plain,
( spl2_15
| ~ spl2_32 ),
inference(avatar_contradiction_clause,[],[f659]) ).
fof(f691,plain,
! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,s1)
| b3b1 = s1
| b1 = X0 ),
inference(resolution,[],[f335,f110]) ).
fof(f698,definition,
( spl2_40
<=> b3b1 = s1 ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f700,plain,
( b3b1 = s1
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f702,definition,
( spl2_41
<=> ! [X0] :
( ~ incident(X0,b3b1)
| b1 = X0
| ~ incident(X0,s1) ) ),
introduced(definition,[new_symbols(definition,[spl2_41])],[avatar_definition]) ).
fof(f703,plain,
( ! [X0] :
( ~ incident(X0,s1)
| b1 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_41 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f704,plain,
( spl2_40
| spl2_41 ),
inference(avatar_split_clause,[],[f691,f702,f698]) ).
fof(f715,plain,
( incident(a1,b3b1)
| ~ spl2_40 ),
inference(superposition,[],[f107,f700]) ).
fof(f716,plain,
( incident(s,b3b1)
| ~ spl2_40 ),
inference(superposition,[],[f104,f700]) ).
fof(f741,definition,
( spl2_44
<=> incident(a3,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_44])],[avatar_definition]) ).
fof(f742,plain,
( incident(a3,b3b1)
| ~ spl2_44 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f743,plain,
( ~ incident(a3,b3b1)
| spl2_44 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f745,definition,
( spl2_45
<=> a3 = b1 ),
introduced(definition,[new_symbols(definition,[spl2_45])],[avatar_definition]) ).
fof(f746,plain,
( a3 != b1
| spl2_45 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( a3 = b1
| ~ spl2_45 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f749,plain,
( incident(a3,b1b2)
| ~ spl2_45 ),
inference(superposition,[],[f98,f747]) ).
fof(f750,plain,
( incident(a3,b3b1)
| ~ spl2_45 ),
inference(superposition,[],[f103,f747]) ).
fof(f761,plain,
! [X0] :
( ~ incident(X0,b1b2)
| ~ incident(X0,a1a2)
| b1b2 = a1a2
| p3 = X0 ),
inference(resolution,[],[f337,f113]) ).
fof(f767,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,b1b2)
| p3 = X0 )
| spl2_4 ),
inference(forward_subsumption_resolution,[],[f761,f161]) ).
fof(f769,plain,
( ~ incident(a1,b1b2)
| p3 = a1
| spl2_4 ),
inference(resolution,[],[f767,f92]) ).
fof(f770,plain,
( ~ incident(a2,b1b2)
| p3 = a2
| spl2_4 ),
inference(resolution,[],[f767,f93]) ).
fof(f779,definition,
( spl2_46
<=> p3 = a1 ),
introduced(definition,[new_symbols(definition,[spl2_46])],[avatar_definition]) ).
fof(f781,plain,
( p3 = a1
| ~ spl2_46 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f783,definition,
( spl2_47
<=> incident(a1,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_47])],[avatar_definition]) ).
fof(f784,plain,
( incident(a1,b1b2)
| ~ spl2_47 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f785,plain,
( ~ incident(a1,b1b2)
| spl2_47 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f786,plain,
( spl2_46
| ~ spl2_47
| spl2_4 ),
inference(avatar_split_clause,[],[f769,f159,f783,f779]) ).
fof(f792,plain,
( ~ incident(a1,a3a1)
| spl2_19
| ~ spl2_46 ),
inference(superposition,[],[f309,f781]) ).
fof(f809,plain,
( $false
| spl2_19
| ~ spl2_46 ),
inference(forward_subsumption_resolution,[],[f792,f97]) ).
fof(f810,plain,
( spl2_19
| ~ spl2_46 ),
inference(avatar_contradiction_clause,[],[f809]) ).
fof(f839,plain,
! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,a3a1)
| b3b1 = a3a1
| p2 = X0 ),
inference(resolution,[],[f333,f117]) ).
fof(f845,plain,
( ! [X0] :
( ~ incident(X0,a3a1)
| ~ incident(X0,b3b1)
| p2 = X0 )
| spl2_2 ),
inference(forward_subsumption_resolution,[],[f839,f151]) ).
fof(f847,plain,
( ~ incident(a1,b3b1)
| p2 = a1
| spl2_2 ),
inference(resolution,[],[f845,f97]) ).
fof(f848,plain,
( ~ incident(a3,b3b1)
| p2 = a3
| spl2_2 ),
inference(resolution,[],[f845,f96]) ).
fof(f853,plain,
( p2 = a1
| spl2_2
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f847,f715]) ).
fof(f856,plain,
( ! [X0] :
( ~ incident(a1,X0)
| ~ incident(p3,X0)
| ~ incident(p1,X0) )
| spl2_2
| ~ spl2_17
| ~ spl2_40 ),
inference(superposition,[],[f224,f853]) ).
fof(f871,plain,
( ! [X0] :
( ~ incident(a2,X0)
| ~ incident(a1,X0)
| ~ incident(p3,X0) )
| spl2_2
| spl2_3
| ~ spl2_17
| ~ spl2_22
| ~ spl2_40 ),
inference(forward_demodulation,[],[f856,f565]) ).
fof(f893,plain,
( ~ incident(s,b2b3)
| a2 = s
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33 ),
inference(resolution,[],[f629,f106]) ).
fof(f1001,plain,
( ~ incident(a1,a1a2)
| ~ incident(p3,a1a2)
| spl2_2
| spl2_3
| ~ spl2_17
| ~ spl2_22
| ~ spl2_40 ),
inference(resolution,[],[f871,f93]) ).
fof(f1013,definition,
( spl2_49
<=> incident(a1,s3) ),
introduced(definition,[new_symbols(definition,[spl2_49])],[avatar_definition]) ).
fof(f1015,plain,
( ~ incident(a1,s3)
| spl2_49 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1018,plain,
( ~ incident(p3,a1a2)
| spl2_2
| spl2_3
| ~ spl2_17
| ~ spl2_22
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f1001,f92]) ).
fof(f1020,definition,
( spl2_50
<=> incident(p3,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_50])],[avatar_definition]) ).
fof(f1022,plain,
( ~ incident(p3,a2a3)
| spl2_50 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1028,plain,
( $false
| spl2_2
| spl2_3
| ~ spl2_17
| ~ spl2_22
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f1018,f113]) ).
fof(f1029,plain,
( spl2_2
| spl2_3
| ~ spl2_17
| ~ spl2_22
| ~ spl2_40 ),
inference(avatar_contradiction_clause,[],[f1028]) ).
fof(f1031,definition,
( spl2_52
<=> p2 = a1 ),
introduced(definition,[new_symbols(definition,[spl2_52])],[avatar_definition]) ).
fof(f1033,plain,
( p2 = a1
| ~ spl2_52 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1035,definition,
( spl2_53
<=> incident(a1,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_53])],[avatar_definition]) ).
fof(f1037,plain,
( ~ incident(a1,b3b1)
| spl2_53 ),
inference(avatar_component_clause,[],[f1035]) ).
fof(f1038,plain,
( spl2_52
| ~ spl2_53
| spl2_2 ),
inference(avatar_split_clause,[],[f847,f149,f1035,f1031]) ).
fof(f1039,plain,
( a2 = s
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f893,f393]) ).
fof(f1073,plain,
( b1 = s
| ~ incident(s,b3b1)
| ~ spl2_41 ),
inference(resolution,[],[f703,f104]) ).
fof(f1078,plain,
( a2 = b1
| ~ incident(s,b3b1)
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33
| ~ spl2_41 ),
inference(forward_demodulation,[],[f1073,f1039]) ).
fof(f1081,plain,
( ~ incident(s,b3b1)
| spl2_5
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33
| ~ spl2_41 ),
inference(forward_subsumption_resolution,[],[f1078,f513]) ).
fof(f1084,plain,
( ~ incident(a2,b3b1)
| spl2_5
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33
| ~ spl2_41 ),
inference(forward_demodulation,[],[f1081,f1039]) ).
fof(f1085,plain,
( $false
| spl2_5
| ~ spl2_13
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33
| ~ spl2_41 ),
inference(forward_subsumption_resolution,[],[f1084,f205]) ).
fof(f1086,plain,
( spl2_5
| ~ spl2_13
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33
| ~ spl2_41 ),
inference(avatar_contradiction_clause,[],[f1085]) ).
fof(f1088,definition,
( spl2_54
<=> incident(s,b3b1) ),
introduced(definition,[new_symbols(definition,[spl2_54])],[avatar_definition]) ).
fof(f1090,plain,
( ~ incident(s,b3b1)
| spl2_54 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1092,definition,
( spl2_55
<=> b1 = s ),
introduced(definition,[new_symbols(definition,[spl2_55])],[avatar_definition]) ).
fof(f1094,plain,
( b1 = s
| ~ spl2_55 ),
inference(avatar_component_clause,[],[f1092]) ).
fof(f1100,plain,
( incident(p3,b2b3)
| ~ spl2_24 ),
inference(superposition,[],[f114,f385]) ).
fof(f1118,plain,
( $false
| ~ spl2_24
| spl2_28 ),
inference(forward_subsumption_resolution,[],[f1100,f421]) ).
fof(f1119,plain,
( ~ spl2_24
| spl2_28 ),
inference(avatar_contradiction_clause,[],[f1118]) ).
fof(f1128,definition,
( spl2_56
<=> a1 = b1 ),
introduced(definition,[new_symbols(definition,[spl2_56])],[avatar_definition]) ).
fof(f1130,plain,
( a1 = b1
| ~ spl2_56 ),
inference(avatar_component_clause,[],[f1128]) ).
fof(f1133,definition,
( spl2_57
<=> p1 = a2 ),
introduced(definition,[new_symbols(definition,[spl2_57])],[avatar_definition]) ).
fof(f1134,plain,
( p1 != a2
| spl2_57 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1135,plain,
( p1 = a2
| ~ spl2_57 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1137,definition,
( spl2_58
<=> incident(a2,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_58])],[avatar_definition]) ).
fof(f1139,plain,
( ~ incident(a2,b2b3)
| spl2_58 ),
inference(avatar_component_clause,[],[f1137]) ).
fof(f1140,plain,
( spl2_57
| ~ spl2_58
| spl2_3 ),
inference(avatar_split_clause,[],[f557,f154,f1137,f1133]) ).
fof(f1142,definition,
( spl2_59
<=> p1 = a3 ),
introduced(definition,[new_symbols(definition,[spl2_59])],[avatar_definition]) ).
fof(f1143,plain,
( p1 != a3
| spl2_59 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1144,plain,
( p1 = a3
| ~ spl2_59 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1145,plain,
( spl2_59
| ~ spl2_26
| spl2_3 ),
inference(avatar_split_clause,[],[f558,f154,f410,f1142]) ).
fof(f1154,definition,
( spl2_60
<=> b2b3 = a3a1 ),
introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition]) ).
fof(f1156,plain,
( b2b3 = a3a1
| ~ spl2_60 ),
inference(avatar_component_clause,[],[f1154]) ).
fof(f1158,definition,
( spl2_61
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b2 = X0
| ~ incident(X0,a3a1) ) ),
introduced(definition,[new_symbols(definition,[spl2_61])],[avatar_definition]) ).
fof(f1159,plain,
( ! [X0] :
( ~ incident(X0,a3a1)
| b2 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_61 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1167,definition,
( spl2_62
<=> p1 = b1 ),
introduced(definition,[new_symbols(definition,[spl2_62])],[avatar_definition]) ).
fof(f1169,plain,
( p1 = b1
| ~ spl2_62 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1171,definition,
( spl2_63
<=> incident(b1,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_63])],[avatar_definition]) ).
fof(f1173,plain,
( ~ incident(b1,b2b3)
| spl2_63 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1176,definition,
( spl2_64
<=> b3b1 = a2a3 ),
introduced(definition,[new_symbols(definition,[spl2_64])],[avatar_definition]) ).
fof(f1178,plain,
( b3b1 = a2a3
| ~ spl2_64 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1180,definition,
( spl2_65
<=> ! [X0] :
( ~ incident(X0,b3b1)
| b1 = X0
| ~ incident(X0,a2a3) ) ),
introduced(definition,[new_symbols(definition,[spl2_65])],[avatar_definition]) ).
fof(f1181,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| b1 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_65 ),
inference(avatar_component_clause,[],[f1180]) ).
fof(f1202,definition,
( spl2_66
<=> incident(s,b2b3) ),
introduced(definition,[new_symbols(definition,[spl2_66])],[avatar_definition]) ).
fof(f1204,plain,
( ~ incident(s,b2b3)
| spl2_66 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1206,definition,
( spl2_67
<=> b2 = s ),
introduced(definition,[new_symbols(definition,[spl2_67])],[avatar_definition]) ).
fof(f1207,plain,
( b2 != s
| spl2_67 ),
inference(avatar_component_clause,[],[f1206]) ).
fof(f1208,plain,
( b2 = s
| ~ spl2_67 ),
inference(avatar_component_clause,[],[f1206]) ).
fof(f1232,plain,
( a1 = b2
| ~ incident(a1,b2b3)
| ~ spl2_61 ),
inference(resolution,[],[f1159,f97]) ).
fof(f1239,plain,
( a1 = b2
| ~ spl2_15
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f1232,f214]) ).
fof(f1240,plain,
( incident(a1,b1b2)
| ~ spl2_15
| ~ spl2_61 ),
inference(superposition,[],[f99,f1239]) ).
fof(f1249,plain,
( $false
| ~ spl2_15
| spl2_47
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f1240,f785]) ).
fof(f1250,plain,
( ~ spl2_15
| spl2_47
| ~ spl2_61 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1251,plain,
( incident(a3,b2b3)
| ~ spl2_60 ),
inference(superposition,[],[f96,f1156]) ).
fof(f1253,plain,
( incident(p2,b2b3)
| ~ spl2_60 ),
inference(superposition,[],[f117,f1156]) ).
fof(f1259,plain,
( $false
| spl2_37
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f1253,f536]) ).
fof(f1260,plain,
( spl2_37
| ~ spl2_60 ),
inference(avatar_contradiction_clause,[],[f1259]) ).
fof(f1261,plain,
( $false
| spl2_26
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f1251,f412]) ).
fof(f1262,plain,
( spl2_26
| ~ spl2_60 ),
inference(avatar_contradiction_clause,[],[f1261]) ).
fof(f1269,definition,
( spl2_69
<=> a3 = b3 ),
introduced(definition,[new_symbols(definition,[spl2_69])],[avatar_definition]) ).
fof(f1270,plain,
( a3 != b3
| spl2_69 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1271,plain,
( a3 = b3
| ~ spl2_69 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1277,plain,
( ~ incident(p3,b2b3)
| ~ incident(p1,b2b3)
| ~ spl2_17
| ~ spl2_37 ),
inference(resolution,[],[f535,f224]) ).
fof(f1311,plain,
( incident(a3,b3b1)
| ~ spl2_69 ),
inference(superposition,[],[f102,f1271]) ).
fof(f1318,plain,
( $false
| spl2_44
| ~ spl2_69 ),
inference(forward_subsumption_resolution,[],[f1311,f743]) ).
fof(f1319,plain,
( spl2_44
| ~ spl2_69 ),
inference(avatar_contradiction_clause,[],[f1318]) ).
fof(f1342,definition,
( spl2_71
<=> a2 = b1 ),
introduced(definition,[new_symbols(definition,[spl2_71])],[avatar_definition]) ).
fof(f1343,plain,
( a2 != b1
| spl2_71 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1344,plain,
( a2 = b1
| ~ spl2_71 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1353,plain,
( incident(a2,b3b1)
| ~ spl2_64 ),
inference(superposition,[],[f94,f1178]) ).
fof(f1359,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,b2b3)
| p1 = X0 )
| spl2_3
| ~ spl2_64 ),
inference(superposition,[],[f556,f1178]) ).
fof(f1360,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| a3 = X0
| ~ incident(X0,b2b3) )
| spl2_3
| ~ spl2_59
| ~ spl2_64 ),
inference(forward_demodulation,[],[f1359,f1144]) ).
fof(f1368,plain,
( p2 = a3
| ~ incident(p2,b2b3)
| spl2_3
| ~ spl2_59
| ~ spl2_64 ),
inference(resolution,[],[f1360,f118]) ).
fof(f1377,plain,
( p2 = a3
| spl2_3
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(forward_subsumption_resolution,[],[f1368,f535]) ).
fof(f1381,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(p3,X0)
| ~ incident(p1,X0) )
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(superposition,[],[f224,f1377]) ).
fof(f1395,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(a3,X0)
| ~ incident(p3,X0) )
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(forward_demodulation,[],[f1381,f1144]) ).
fof(f1396,plain,
( ! [X0] :
( ~ incident(p3,X0)
| ~ incident(a3,X0) )
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(duplicate_literal_removal,[],[f1395]) ).
fof(f1400,plain,
( ! [X0] :
( ~ incident(a3,sK0(p3,X0))
| ~ point(p3)
| ~ point(X0) )
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(resolution,[],[f1396,f136]) ).
fof(f1401,plain,
( ! [X0] :
( ~ incident(a3,sK0(p3,X0))
| ~ point(X0) )
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(forward_subsumption_resolution,[],[f1400,f235]) ).
fof(f1403,plain,
( ~ point(a3)
| ~ point(p3)
| ~ point(a3)
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(resolution,[],[f1401,f135]) ).
fof(f1404,plain,
( ~ point(a3)
| ~ point(p3)
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(duplicate_literal_removal,[],[f1403]) ).
fof(f1405,plain,
( ~ point(p3)
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(forward_subsumption_resolution,[],[f1404,f240]) ).
fof(f1406,plain,
( $false
| spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(forward_subsumption_resolution,[],[f1405,f235]) ).
fof(f1407,plain,
( spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(avatar_contradiction_clause,[],[f1406]) ).
fof(f1408,plain,
( $false
| spl2_11
| ~ spl2_45 ),
inference(forward_subsumption_resolution,[],[f749,f195]) ).
fof(f1409,plain,
( spl2_11
| ~ spl2_45 ),
inference(avatar_contradiction_clause,[],[f1408]) ).
fof(f1421,plain,
( $false
| ~ spl2_30
| spl2_66 ),
inference(forward_subsumption_resolution,[],[f500,f1204]) ).
fof(f1422,plain,
( ~ spl2_30
| spl2_66 ),
inference(avatar_contradiction_clause,[],[f1421]) ).
fof(f1434,plain,
( incident(b2,s1)
| ~ spl2_67 ),
inference(superposition,[],[f104,f1208]) ).
fof(f1436,plain,
( incident(b2,s3)
| ~ spl2_67 ),
inference(superposition,[],[f106,f1208]) ).
fof(f1441,plain,
( ! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,s1)
| b2b3 = s1
| b2 = X0 )
| ~ spl2_67 ),
inference(resolution,[],[f1434,f330]) ).
fof(f1447,definition,
( spl2_72
<=> b2b3 = s1 ),
introduced(definition,[new_symbols(definition,[spl2_72])],[avatar_definition]) ).
fof(f1449,plain,
( b2b3 = s1
| ~ spl2_72 ),
inference(avatar_component_clause,[],[f1447]) ).
fof(f1451,definition,
( spl2_73
<=> ! [X0] :
( ~ incident(X0,b2b3)
| b2 = X0
| ~ incident(X0,s1) ) ),
introduced(definition,[new_symbols(definition,[spl2_73])],[avatar_definition]) ).
fof(f1452,plain,
( ! [X0] :
( ~ incident(X0,s1)
| b2 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_73 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1453,plain,
( spl2_72
| spl2_73
| ~ spl2_67 ),
inference(avatar_split_clause,[],[f1441,f1206,f1451,f1447]) ).
fof(f1456,plain,
! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,s3)
| b3b1 = s3
| b3 = X0 ),
inference(resolution,[],[f336,f112]) ).
fof(f1474,plain,
( a1 = b2
| ~ incident(a1,b2b3)
| ~ spl2_73 ),
inference(resolution,[],[f1452,f107]) ).
fof(f1482,plain,
( a1 = b2
| ~ spl2_15
| ~ spl2_73 ),
inference(forward_subsumption_resolution,[],[f1474,f214]) ).
fof(f1483,plain,
( incident(a1,b1b2)
| ~ spl2_15
| ~ spl2_73 ),
inference(superposition,[],[f99,f1482]) ).
fof(f1493,plain,
( $false
| ~ spl2_15
| spl2_47
| ~ spl2_73 ),
inference(forward_subsumption_resolution,[],[f1483,f785]) ).
fof(f1494,plain,
( ~ spl2_15
| spl2_47
| ~ spl2_73 ),
inference(avatar_contradiction_clause,[],[f1493]) ).
fof(f1497,plain,
( incident(b1,b2b3)
| ~ spl2_72 ),
inference(superposition,[],[f110,f1449]) ).
fof(f1502,plain,
( $false
| spl2_63
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f1497,f1173]) ).
fof(f1503,plain,
( spl2_63
| ~ spl2_72 ),
inference(avatar_contradiction_clause,[],[f1502]) ).
fof(f1504,plain,
( a3 = b1
| ~ spl2_59
| ~ spl2_62 ),
inference(forward_demodulation,[],[f1169,f1144]) ).
fof(f1507,plain,
( $false
| spl2_45
| ~ spl2_59
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f1504,f746]) ).
fof(f1508,plain,
( spl2_45
| ~ spl2_59
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f1507]) ).
fof(f1509,plain,
( $false
| ~ spl2_22
| spl2_58 ),
inference(forward_subsumption_resolution,[],[f392,f1139]) ).
fof(f1510,plain,
( ~ spl2_22
| spl2_58 ),
inference(avatar_contradiction_clause,[],[f1509]) ).
fof(f1513,plain,
( $false
| spl2_3
| spl2_9
| ~ spl2_22
| ~ spl2_26 ),
inference(forward_subsumption_resolution,[],[f611,f411]) ).
fof(f1514,plain,
( spl2_3
| spl2_9
| ~ spl2_22
| ~ spl2_26 ),
inference(avatar_contradiction_clause,[],[f1513]) ).
fof(f1520,definition,
( spl2_74
<=> b3 = s ),
introduced(definition,[new_symbols(definition,[spl2_74])],[avatar_definition]) ).
fof(f1522,plain,
( b3 = s
| ~ spl2_74 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1529,plain,
( $false
| ~ spl2_40
| spl2_53 ),
inference(forward_subsumption_resolution,[],[f715,f1037]) ).
fof(f1530,plain,
( ~ spl2_40
| spl2_53 ),
inference(avatar_contradiction_clause,[],[f1529]) ).
fof(f1531,plain,
( $false
| ~ spl2_40
| spl2_54 ),
inference(forward_subsumption_resolution,[],[f716,f1090]) ).
fof(f1532,plain,
( ~ spl2_40
| spl2_54 ),
inference(avatar_contradiction_clause,[],[f1531]) ).
fof(f1535,definition,
( spl2_76
<=> b3b1 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_76])],[avatar_definition]) ).
fof(f1537,plain,
( b3b1 = s3
| ~ spl2_76 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f1539,definition,
( spl2_77
<=> ! [X0] :
( ~ incident(X0,b3b1)
| b3 = X0
| ~ incident(X0,s3) ) ),
introduced(definition,[new_symbols(definition,[spl2_77])],[avatar_definition]) ).
fof(f1540,plain,
( ! [X0] :
( ~ incident(X0,s3)
| b3 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_77 ),
inference(avatar_component_clause,[],[f1539]) ).
fof(f1541,plain,
( spl2_76
| spl2_77 ),
inference(avatar_split_clause,[],[f1456,f1539,f1535]) ).
fof(f1563,definition,
( spl2_79
<=> b3b1 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_79])],[avatar_definition]) ).
fof(f1565,plain,
( b3b1 = a1a2
| ~ spl2_79 ),
inference(avatar_component_clause,[],[f1563]) ).
fof(f1567,definition,
( spl2_80
<=> ! [X0] :
( ~ incident(X0,b3b1)
| b3 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_80])],[avatar_definition]) ).
fof(f1568,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| b3 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_80 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1576,definition,
( spl2_82
<=> a1 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_82])],[avatar_definition]) ).
fof(f1578,plain,
( a1 = b2
| ~ spl2_82 ),
inference(avatar_component_clause,[],[f1576]) ).
fof(f1586,definition,
( spl2_83
<=> p2 = a3 ),
introduced(definition,[new_symbols(definition,[spl2_83])],[avatar_definition]) ).
fof(f1588,plain,
( p2 = a3
| ~ spl2_83 ),
inference(avatar_component_clause,[],[f1586]) ).
fof(f1589,plain,
( spl2_83
| ~ spl2_44
| spl2_2 ),
inference(avatar_split_clause,[],[f848,f149,f741,f1586]) ).
fof(f1621,definition,
( spl2_84
<=> b1b2 = s1 ),
introduced(definition,[new_symbols(definition,[spl2_84])],[avatar_definition]) ).
fof(f1623,plain,
( b1b2 = s1
| ~ spl2_84 ),
inference(avatar_component_clause,[],[f1621]) ).
fof(f1625,definition,
( spl2_85
<=> ! [X0] :
( ~ incident(X0,b1b2)
| b1 = X0
| ~ incident(X0,s1) ) ),
introduced(definition,[new_symbols(definition,[spl2_85])],[avatar_definition]) ).
fof(f1626,plain,
( ! [X0] :
( ~ incident(X0,s1)
| b1 = X0
| ~ incident(X0,b1b2) )
| ~ spl2_85 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1629,definition,
( spl2_86
<=> b1b2 = a2a3 ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
fof(f1631,plain,
( b1b2 = a2a3
| ~ spl2_86 ),
inference(avatar_component_clause,[],[f1629]) ).
fof(f1633,definition,
( spl2_87
<=> ! [X0] :
( ~ incident(X0,b1b2)
| b1 = X0
| ~ incident(X0,a2a3) ) ),
introduced(definition,[new_symbols(definition,[spl2_87])],[avatar_definition]) ).
fof(f1634,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| b1 = X0
| ~ incident(X0,b1b2) )
| ~ spl2_87 ),
inference(avatar_component_clause,[],[f1633]) ).
fof(f1679,definition,
( spl2_89
<=> a2 = b2 ),
introduced(definition,[new_symbols(definition,[spl2_89])],[avatar_definition]) ).
fof(f1681,plain,
( a2 = b2
| ~ spl2_89 ),
inference(avatar_component_clause,[],[f1679]) ).
fof(f1719,plain,
( ~ incident(p1,b2b3)
| spl2_18
| ~ spl2_60 ),
inference(superposition,[],[f305,f1156]) ).
fof(f1721,plain,
( $false
| spl2_18
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f1719,f116]) ).
fof(f1722,plain,
( spl2_18
| ~ spl2_60 ),
inference(avatar_contradiction_clause,[],[f1721]) ).
fof(f1749,definition,
( spl2_91
<=> incident(a2,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_91])],[avatar_definition]) ).
fof(f1750,plain,
( incident(a2,b1b2)
| ~ spl2_91 ),
inference(avatar_component_clause,[],[f1749]) ).
fof(f1751,plain,
( ~ incident(a2,b1b2)
| spl2_91 ),
inference(avatar_component_clause,[],[f1749]) ).
fof(f1752,plain,
( spl2_38
| ~ spl2_91
| spl2_4 ),
inference(avatar_split_clause,[],[f770,f159,f1749,f607]) ).
fof(f1787,definition,
( spl2_93
<=> b1b2 = a3a1 ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
fof(f1789,plain,
( b1b2 = a3a1
| ~ spl2_93 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1826,plain,
( incident(a1,s2)
| ~ spl2_82 ),
inference(superposition,[],[f111,f1578]) ).
fof(f1827,plain,
( a1 != b1
| spl2_7
| ~ spl2_82 ),
inference(superposition,[],[f176,f1578]) ).
fof(f1849,plain,
! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,s2)
| a2a3 = s2
| a2 = X0 ),
inference(resolution,[],[f341,f108]) ).
fof(f1856,definition,
( spl2_95
<=> a2a3 = s2 ),
introduced(definition,[new_symbols(definition,[spl2_95])],[avatar_definition]) ).
fof(f1858,plain,
( a2a3 = s2
| ~ spl2_95 ),
inference(avatar_component_clause,[],[f1856]) ).
fof(f1860,definition,
( spl2_96
<=> ! [X0] :
( ~ incident(X0,a2a3)
| a2 = X0
| ~ incident(X0,s2) ) ),
introduced(definition,[new_symbols(definition,[spl2_96])],[avatar_definition]) ).
fof(f1861,plain,
( ! [X0] :
( ~ incident(X0,s2)
| a2 = X0
| ~ incident(X0,a2a3) )
| ~ spl2_96 ),
inference(avatar_component_clause,[],[f1860]) ).
fof(f1862,plain,
( spl2_95
| spl2_96 ),
inference(avatar_split_clause,[],[f1849,f1860,f1856]) ).
fof(f1864,definition,
( spl2_97
<=> a2a3 = a1a2 ),
introduced(definition,[new_symbols(definition,[spl2_97])],[avatar_definition]) ).
fof(f1866,plain,
( a2a3 = a1a2
| ~ spl2_97 ),
inference(avatar_component_clause,[],[f1864]) ).
fof(f1868,definition,
( spl2_98
<=> ! [X0] :
( ~ incident(X0,a2a3)
| a2 = X0
| ~ incident(X0,a1a2) ) ),
introduced(definition,[new_symbols(definition,[spl2_98])],[avatar_definition]) ).
fof(f1869,plain,
( ! [X0] :
( ~ incident(X0,a1a2)
| a2 = X0
| ~ incident(X0,a2a3) )
| ~ spl2_98 ),
inference(avatar_component_clause,[],[f1868]) ).
fof(f1914,plain,
( ! [X0] :
( ~ incident(X0,a3a1)
| a1 = X0
| ~ incident(X0,b2b3) )
| ~ spl2_61
| ~ spl2_82 ),
inference(forward_demodulation,[],[f1159,f1578]) ).
fof(f1917,plain,
( a3 = b1
| ~ incident(a3,b3b1)
| ~ spl2_65 ),
inference(resolution,[],[f1181,f95]) ).
fof(f1919,plain,
( ! [X0] :
( b1 = sK1(a2a3,X0)
| ~ incident(sK1(a2a3,X0),b3b1)
| ~ line(a2a3)
| ~ line(X0) )
| ~ spl2_65 ),
inference(resolution,[],[f1181,f138]) ).
fof(f1922,plain,
( ! [X0] :
( ~ incident(sK1(a2a3,X0),b3b1)
| b1 = sK1(a2a3,X0)
| ~ line(X0) )
| ~ spl2_65 ),
inference(forward_subsumption_resolution,[],[f1919,f269]) ).
fof(f1927,plain,
( ! [X0] :
( b3 = sK1(X0,s3)
| ~ incident(sK1(X0,s3),b3b1)
| ~ line(X0)
| ~ line(s3) )
| ~ spl2_77 ),
inference(resolution,[],[f1540,f137]) ).
fof(f1928,plain,
( ! [X0] :
( ~ incident(sK1(X0,s3),b3b1)
| b3 = sK1(X0,s3)
| ~ line(X0) )
| ~ spl2_77 ),
inference(forward_subsumption_resolution,[],[f1927,f285]) ).
fof(f1930,plain,
( a1 = b1
| ~ incident(a1,b1b2)
| ~ spl2_85 ),
inference(resolution,[],[f1626,f107]) ).
fof(f1938,definition,
( spl2_99
<=> incident(s,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_99])],[avatar_definition]) ).
fof(f1940,plain,
( ~ incident(s,b1b2)
| spl2_99 ),
inference(avatar_component_clause,[],[f1938]) ).
fof(f1942,plain,
( ~ incident(a1,b1b2)
| spl2_7
| ~ spl2_82
| ~ spl2_85 ),
inference(forward_subsumption_resolution,[],[f1930,f1827]) ).
fof(f1943,plain,
( $false
| spl2_7
| ~ spl2_47
| ~ spl2_82
| ~ spl2_85 ),
inference(forward_subsumption_resolution,[],[f1942,f784]) ).
fof(f1944,plain,
( spl2_7
| ~ spl2_47
| ~ spl2_82
| ~ spl2_85 ),
inference(avatar_contradiction_clause,[],[f1943]) ).
fof(f1945,plain,
( incident(s,b1b2)
| ~ spl2_84 ),
inference(superposition,[],[f104,f1623]) ).
fof(f1946,plain,
( incident(a1,b1b2)
| ~ spl2_84 ),
inference(superposition,[],[f107,f1623]) ).
fof(f1957,plain,
( p1 = b1
| ~ incident(p1,b1b2)
| ~ spl2_87 ),
inference(resolution,[],[f1634,f115]) ).
fof(f1959,plain,
( a3 = b1
| ~ incident(a3,b1b2)
| ~ spl2_87 ),
inference(resolution,[],[f1634,f95]) ).
fof(f1962,plain,
( ! [X0] :
( b1 = sK1(X0,a2a3)
| ~ incident(sK1(X0,a2a3),b1b2)
| ~ line(X0)
| ~ line(a2a3) )
| ~ spl2_87 ),
inference(resolution,[],[f1634,f137]) ).
fof(f1963,plain,
( ! [X0] :
( ~ incident(sK1(X0,a2a3),b1b2)
| b1 = sK1(X0,a2a3)
| ~ line(X0) )
| ~ spl2_87 ),
inference(forward_subsumption_resolution,[],[f1962,f269]) ).
fof(f1977,definition,
( spl2_100
<=> incident(s,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_100])],[avatar_definition]) ).
fof(f1978,plain,
( incident(s,a2a3)
| ~ spl2_100 ),
inference(avatar_component_clause,[],[f1977]) ).
fof(f1979,plain,
( ~ incident(s,a2a3)
| spl2_100 ),
inference(avatar_component_clause,[],[f1977]) ).
fof(f2052,plain,
( p2 = a1
| ~ incident(p2,b2b3)
| ~ spl2_61
| ~ spl2_82 ),
inference(resolution,[],[f1914,f117]) ).
fof(f2082,plain,
( p1 = sK1(b2b3,a2a3)
| ~ line(b2b3)
| ~ line(b2b3)
| ~ line(a2a3)
| spl2_3 ),
inference(resolution,[],[f562,f138]) ).
fof(f2083,plain,
( p1 = sK1(b2b3,a2a3)
| ~ line(b2b3)
| ~ line(a2a3)
| spl2_3 ),
inference(duplicate_literal_removal,[],[f2082]) ).
fof(f2084,plain,
( p1 = sK1(b2b3,a2a3)
| ~ line(a2a3)
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f2083,f258]) ).
fof(f2085,plain,
( p1 = sK1(b2b3,a2a3)
| spl2_3 ),
inference(forward_subsumption_resolution,[],[f2084,f269]) ).
fof(f2155,definition,
( spl2_107
<=> a3a1 = s3 ),
introduced(definition,[new_symbols(definition,[spl2_107])],[avatar_definition]) ).
fof(f2157,plain,
( a3a1 = s3
| ~ spl2_107 ),
inference(avatar_component_clause,[],[f2155]) ).
fof(f2159,definition,
( spl2_108
<=> ! [X0] :
( ~ incident(X0,a3a1)
| a3 = X0
| ~ incident(X0,s3) ) ),
introduced(definition,[new_symbols(definition,[spl2_108])],[avatar_definition]) ).
fof(f2160,plain,
( ! [X0] :
( ~ incident(X0,s3)
| a3 = X0
| ~ incident(X0,a3a1) )
| ~ spl2_108 ),
inference(avatar_component_clause,[],[f2159]) ).
fof(f2166,plain,
( ! [X0] :
( a3 = sK1(X0,s3)
| ~ incident(sK1(X0,s3),a3a1)
| ~ line(X0)
| ~ line(s3) )
| ~ spl2_108 ),
inference(resolution,[],[f2160,f137]) ).
fof(f2167,plain,
( ! [X0] :
( ~ incident(sK1(X0,s3),a3a1)
| a3 = sK1(X0,s3)
| ~ line(X0) )
| ~ spl2_108 ),
inference(forward_subsumption_resolution,[],[f2166,f285]) ).
fof(f2170,definition,
( spl2_109
<=> incident(s,a3a1) ),
introduced(definition,[new_symbols(definition,[spl2_109])],[avatar_definition]) ).
fof(f2171,plain,
( incident(s,a3a1)
| ~ spl2_109 ),
inference(avatar_component_clause,[],[f2170]) ).
fof(f2172,plain,
( ~ incident(s,a3a1)
| spl2_109 ),
inference(avatar_component_clause,[],[f2170]) ).
fof(f2174,definition,
( spl2_110
<=> a3 = s ),
introduced(definition,[new_symbols(definition,[spl2_110])],[avatar_definition]) ).
fof(f2175,plain,
( a3 != s
| spl2_110 ),
inference(avatar_component_clause,[],[f2174]) ).
fof(f2176,plain,
( a3 = s
| ~ spl2_110 ),
inference(avatar_component_clause,[],[f2174]) ).
fof(f2205,plain,
( b1 = sK1(a2a3,b3b1)
| ~ line(b3b1)
| ~ line(a2a3)
| ~ line(b3b1)
| ~ spl2_65 ),
inference(resolution,[],[f1922,f137]) ).
fof(f2207,plain,
( b1 = sK1(a2a3,b3b1)
| ~ line(b3b1)
| ~ line(a2a3)
| ~ spl2_65 ),
inference(duplicate_literal_removal,[],[f2205]) ).
fof(f2208,plain,
( b1 = sK1(a2a3,b3b1)
| ~ line(a2a3)
| ~ spl2_65 ),
inference(forward_subsumption_resolution,[],[f2207,f261]) ).
fof(f2209,plain,
( b1 = sK1(a2a3,b3b1)
| ~ spl2_65 ),
inference(forward_subsumption_resolution,[],[f2208,f269]) ).
fof(f2210,plain,
( ~ incident(b1,b2b3)
| p1 = b1
| ~ line(b3b1)
| spl2_3
| ~ spl2_65 ),
inference(superposition,[],[f563,f2209]) ).
fof(f2215,plain,
( b3 = sK1(b3b1,s3)
| ~ line(b3b1)
| ~ line(b3b1)
| ~ line(s3)
| ~ spl2_77 ),
inference(resolution,[],[f1928,f138]) ).
fof(f2216,plain,
( b3 = sK1(b3b1,s3)
| ~ line(b3b1)
| ~ line(s3)
| ~ spl2_77 ),
inference(duplicate_literal_removal,[],[f2215]) ).
fof(f2217,plain,
( b3 = sK1(b3b1,s3)
| ~ line(s3)
| ~ spl2_77 ),
inference(forward_subsumption_resolution,[],[f2216,f261]) ).
fof(f2218,plain,
( b3 = sK1(b3b1,s3)
| ~ spl2_77 ),
inference(forward_subsumption_resolution,[],[f2217,f285]) ).
fof(f2230,plain,
( ~ incident(p1,b1b2)
| p1 = b1
| ~ line(b2b3)
| spl2_3
| ~ spl2_87 ),
inference(superposition,[],[f1963,f2085]) ).
fof(f2359,plain,
( ~ incident(b3,a3a1)
| a3 = b3
| ~ line(b3b1)
| ~ spl2_77
| ~ spl2_108 ),
inference(superposition,[],[f2167,f2218]) ).
fof(f2398,plain,
! [X0] :
( ~ incident(a1,X0)
| ~ incident(a3,X0)
| a3a1 = X0
| a1 = a3 ),
inference(resolution,[],[f345,f96]) ).
fof(f2405,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(a1,X0)
| a3a1 = X0 )
| spl2_8 ),
inference(forward_subsumption_resolution,[],[f2398,f181]) ).
fof(f2416,plain,
( ~ incident(a1,s3)
| a3a1 = s3
| spl2_8 ),
inference(resolution,[],[f2405,f109]) ).
fof(f2421,plain,
( spl2_107
| ~ spl2_49
| spl2_8 ),
inference(avatar_split_clause,[],[f2416,f179,f1013,f2155]) ).
fof(f2523,plain,
! [X0] :
( ~ incident(a1,X0)
| ~ incident(a2,X0)
| a1a2 = X0
| a1 = a2 ),
inference(resolution,[],[f348,f93]) ).
fof(f2529,plain,
( ! [X0] :
( ~ incident(a2,X0)
| ~ incident(a1,X0)
| a1a2 = X0 )
| spl2_10 ),
inference(forward_subsumption_resolution,[],[f2523,f191]) ).
fof(f2532,plain,
( ~ incident(a1,s2)
| a1a2 = s2
| spl2_10 ),
inference(resolution,[],[f2529,f108]) ).
fof(f2537,plain,
( a1a2 = s2
| spl2_10
| ~ spl2_82 ),
inference(forward_subsumption_resolution,[],[f2532,f1826]) ).
fof(f2538,plain,
( incident(s,a1a2)
| spl2_10
| ~ spl2_82 ),
inference(superposition,[],[f105,f2537]) ).
fof(f2557,plain,
( ~ incident(s,b1b2)
| p3 = s
| spl2_4
| spl2_10
| ~ spl2_82 ),
inference(resolution,[],[f2538,f767]) ).
fof(f2561,plain,
( p3 = s
| spl2_4
| spl2_10
| ~ spl2_82
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f2557,f1945]) ).
fof(f2570,plain,
( b2 = s
| spl2_4
| spl2_10
| ~ spl2_29
| ~ spl2_82
| ~ spl2_84 ),
inference(forward_demodulation,[],[f2561,f425]) ).
fof(f2571,plain,
( $false
| spl2_4
| spl2_10
| ~ spl2_29
| spl2_67
| ~ spl2_82
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f2570,f1207]) ).
fof(f2572,plain,
( spl2_4
| spl2_10
| ~ spl2_29
| spl2_67
| ~ spl2_82
| ~ spl2_84 ),
inference(avatar_contradiction_clause,[],[f2571]) ).
fof(f2576,plain,
( incident(a1,s3)
| ~ spl2_67
| ~ spl2_82 ),
inference(forward_demodulation,[],[f1436,f1578]) ).
fof(f2582,plain,
( $false
| spl2_49
| ~ spl2_67
| ~ spl2_82 ),
inference(forward_subsumption_resolution,[],[f2576,f1015]) ).
fof(f2583,plain,
( spl2_49
| ~ spl2_67
| ~ spl2_82 ),
inference(avatar_contradiction_clause,[],[f2582]) ).
fof(f2585,plain,
( incident(s,a3a1)
| ~ spl2_107 ),
inference(superposition,[],[f106,f2157]) ).
fof(f2587,plain,
( incident(b3,a3a1)
| ~ spl2_107 ),
inference(superposition,[],[f112,f2157]) ).
fof(f2607,plain,
( $false
| ~ spl2_107
| spl2_109 ),
inference(forward_subsumption_resolution,[],[f2585,f2172]) ).
fof(f2608,plain,
( ~ spl2_107
| spl2_109 ),
inference(avatar_contradiction_clause,[],[f2607]) ).
fof(f2626,plain,
( ~ incident(b3,b3b1)
| p2 = b3
| spl2_2
| ~ spl2_107 ),
inference(resolution,[],[f2587,f845]) ).
fof(f2630,plain,
( p2 = b3
| spl2_2
| ~ spl2_107 ),
inference(forward_subsumption_resolution,[],[f2626,f102]) ).
fof(f2672,plain,
( ~ incident(b3,b2b3)
| spl2_2
| spl2_37
| ~ spl2_107 ),
inference(superposition,[],[f536,f2630]) ).
fof(f2681,plain,
( $false
| spl2_2
| spl2_37
| ~ spl2_107 ),
inference(forward_subsumption_resolution,[],[f2672,f101]) ).
fof(f2682,plain,
( spl2_2
| spl2_37
| ~ spl2_107 ),
inference(avatar_contradiction_clause,[],[f2681]) ).
fof(f2694,plain,
( ~ incident(p1,b2b3)
| ~ spl2_17
| ~ spl2_28
| ~ spl2_37 ),
inference(forward_subsumption_resolution,[],[f1277,f420]) ).
fof(f2703,plain,
( $false
| ~ spl2_17
| ~ spl2_28
| ~ spl2_37 ),
inference(forward_subsumption_resolution,[],[f2694,f116]) ).
fof(f2704,plain,
( ~ spl2_17
| ~ spl2_28
| ~ spl2_37 ),
inference(avatar_contradiction_clause,[],[f2703]) ).
fof(f2716,plain,
( p3 != a1
| spl2_29
| ~ spl2_82 ),
inference(forward_demodulation,[],[f424,f1578]) ).
fof(f2725,plain,
( ~ incident(b3,a3a1)
| ~ line(b3b1)
| spl2_69
| ~ spl2_77
| ~ spl2_108 ),
inference(forward_subsumption_resolution,[],[f2359,f1270]) ).
fof(f2741,plain,
( $false
| spl2_29
| ~ spl2_46
| ~ spl2_82 ),
inference(forward_subsumption_resolution,[],[f2716,f781]) ).
fof(f2742,plain,
( spl2_29
| ~ spl2_46
| ~ spl2_82 ),
inference(avatar_contradiction_clause,[],[f2741]) ).
fof(f2746,plain,
( ~ incident(b3,a3a1)
| spl2_69
| ~ spl2_77
| ~ spl2_108 ),
inference(forward_subsumption_resolution,[],[f2725,f261]) ).
fof(f2840,plain,
( ~ incident(a1,b1b2)
| b1b2 = a3a1
| spl2_8
| ~ spl2_11 ),
inference(resolution,[],[f196,f2405]) ).
fof(f2854,plain,
( spl2_93
| ~ spl2_47
| spl2_8
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f2840,f194,f179,f783,f1787]) ).
fof(f2866,plain,
( ~ incident(b1,b2b3)
| p1 = b1
| spl2_3
| ~ spl2_65 ),
inference(forward_subsumption_resolution,[],[f2210,f261]) ).
fof(f2953,plain,
( incident(s,b3b1)
| ~ spl2_76 ),
inference(superposition,[],[f106,f1537]) ).
fof(f2954,plain,
( incident(a3,b3b1)
| ~ spl2_76 ),
inference(superposition,[],[f109,f1537]) ).
fof(f2958,plain,
( $false
| spl2_44
| ~ spl2_76 ),
inference(forward_subsumption_resolution,[],[f2954,f743]) ).
fof(f2959,plain,
( spl2_44
| ~ spl2_76 ),
inference(avatar_contradiction_clause,[],[f2958]) ).
fof(f2960,plain,
( $false
| spl2_54
| ~ spl2_76 ),
inference(forward_subsumption_resolution,[],[f2953,f1090]) ).
fof(f2961,plain,
( spl2_54
| ~ spl2_76 ),
inference(avatar_contradiction_clause,[],[f2960]) ).
fof(f3018,plain,
( incident(a1,b3b1)
| ~ spl2_79 ),
inference(superposition,[],[f92,f1565]) ).
fof(f3051,plain,
( incident(a2,b1b2)
| ~ spl2_86 ),
inference(superposition,[],[f94,f1631]) ).
fof(f3066,plain,
( $false
| ~ spl2_86
| spl2_91 ),
inference(forward_subsumption_resolution,[],[f3051,f1751]) ).
fof(f3067,plain,
( ~ spl2_86
| spl2_91 ),
inference(avatar_contradiction_clause,[],[f3066]) ).
fof(f3074,plain,
( ~ incident(b2,b1b2)
| spl2_12
| ~ spl2_93 ),
inference(superposition,[],[f199,f1789]) ).
fof(f3085,plain,
( $false
| spl2_12
| ~ spl2_93 ),
inference(forward_subsumption_resolution,[],[f3074,f99]) ).
fof(f3086,plain,
( spl2_12
| ~ spl2_93 ),
inference(avatar_contradiction_clause,[],[f3085]) ).
fof(f3097,plain,
( ~ spl2_37
| spl2_52
| ~ spl2_61
| ~ spl2_82 ),
inference(avatar_split_clause,[],[f2052,f1576,f1158,f1031,f534]) ).
fof(f3152,definition,
( spl2_126
<=> a2 = b3 ),
introduced(definition,[new_symbols(definition,[spl2_126])],[avatar_definition]) ).
fof(f3154,plain,
( a2 = b3
| ~ spl2_126 ),
inference(avatar_component_clause,[],[f3152]) ).
fof(f3215,definition,
( spl2_127
<=> incident(b2,a2a3) ),
introduced(definition,[new_symbols(definition,[spl2_127])],[avatar_definition]) ).
fof(f3216,plain,
( incident(b2,a2a3)
| ~ spl2_127 ),
inference(avatar_component_clause,[],[f3215]) ).
fof(f3217,plain,
( ~ incident(b2,a2a3)
| spl2_127 ),
inference(avatar_component_clause,[],[f3215]) ).
fof(f3325,plain,
( ! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,a3a1)
| b2b3 = a3a1
| b2 = X0 )
| ~ spl2_12 ),
inference(resolution,[],[f200,f330]) ).
fof(f3333,plain,
( spl2_60
| spl2_61
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f3325,f198,f1158,f1154]) ).
fof(f3340,definition,
( spl2_130
<=> ! [X0] :
( ~ incident(X0,a2a3)
| a2 = X0
| ~ incident(X0,b3b1) ) ),
introduced(definition,[new_symbols(definition,[spl2_130])],[avatar_definition]) ).
fof(f3341,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| a2 = X0
| ~ incident(X0,b3b1) )
| ~ spl2_130 ),
inference(avatar_component_clause,[],[f3340]) ).
fof(f3455,plain,
! [X0] :
( ~ incident(X0,a1a2)
| ~ incident(X0,a2a3)
| a2a3 = a1a2
| a2 = X0 ),
inference(resolution,[],[f349,f94]) ).
fof(f3467,plain,
( spl2_97
| spl2_98 ),
inference(avatar_split_clause,[],[f3455,f1868,f1864]) ).
fof(f3493,plain,
( a2 = b2
| ~ incident(a2,b2b3)
| ~ spl2_23 ),
inference(resolution,[],[f380,f108]) ).
fof(f3495,plain,
( b2 = s
| ~ incident(s,b2b3)
| ~ spl2_23 ),
inference(resolution,[],[f380,f105]) ).
fof(f3507,plain,
( a3 = b3
| ~ incident(a3,b2b3)
| ~ spl2_31 ),
inference(resolution,[],[f479,f109]) ).
fof(f3509,plain,
( b3 = s
| ~ incident(s,b2b3)
| ~ spl2_31 ),
inference(resolution,[],[f479,f106]) ).
fof(f3562,plain,
( a1 = b2
| ~ incident(a1,b2b3)
| ~ spl2_61 ),
inference(resolution,[],[f1159,f97]) ).
fof(f3569,plain,
( a3 = b3
| ~ incident(a3,b3b1)
| ~ spl2_77 ),
inference(resolution,[],[f1540,f109]) ).
fof(f3571,plain,
( b3 = s
| ~ incident(s,b3b1)
| ~ spl2_77 ),
inference(resolution,[],[f1540,f106]) ).
fof(f3578,plain,
( a2 = b3
| ~ incident(a2,b3b1)
| ~ spl2_80 ),
inference(resolution,[],[f1568,f93]) ).
fof(f3584,plain,
( a2 = b3
| ~ spl2_13
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f3578,f205]) ).
fof(f3585,plain,
( incident(a2,b2b3)
| ~ spl2_13
| ~ spl2_80 ),
inference(superposition,[],[f101,f3584]) ).
fof(f3600,plain,
( $false
| ~ spl2_13
| spl2_58
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f3585,f1139]) ).
fof(f3601,plain,
( ~ spl2_13
| spl2_58
| ~ spl2_80 ),
inference(avatar_contradiction_clause,[],[f3600]) ).
fof(f3651,plain,
( $false
| spl2_53
| ~ spl2_79 ),
inference(forward_subsumption_resolution,[],[f3018,f1037]) ).
fof(f3652,plain,
( spl2_53
| ~ spl2_79 ),
inference(avatar_contradiction_clause,[],[f3651]) ).
fof(f3677,plain,
! [X0] :
( ~ incident(X0,s1)
| ~ incident(X0,b3b1)
| b3b1 = s1
| b1 = X0 ),
inference(resolution,[],[f353,f103]) ).
fof(f3678,plain,
! [X0] :
( ~ incident(X0,s1)
| ~ incident(X0,b1b2)
| b1b2 = s1
| b1 = X0 ),
inference(resolution,[],[f353,f98]) ).
fof(f3685,plain,
( spl2_84
| spl2_85 ),
inference(avatar_split_clause,[],[f3678,f1625,f1621]) ).
fof(f3738,plain,
( incident(a1,b1b2)
| ~ spl2_56 ),
inference(superposition,[],[f98,f1130]) ).
fof(f3748,plain,
( $false
| spl2_47
| ~ spl2_56 ),
inference(forward_subsumption_resolution,[],[f3738,f785]) ).
fof(f3749,plain,
( spl2_47
| ~ spl2_56 ),
inference(avatar_contradiction_clause,[],[f3748]) ).
fof(f3751,plain,
( spl2_40
| spl2_41 ),
inference(avatar_split_clause,[],[f3677,f702,f698]) ).
fof(f3796,plain,
( b2 = b3
| ~ incident(s,b2b3)
| ~ spl2_23
| ~ spl2_74 ),
inference(forward_demodulation,[],[f3495,f1522]) ).
fof(f3800,plain,
( ~ incident(s,b2b3)
| spl2_6
| ~ spl2_23
| ~ spl2_74 ),
inference(forward_subsumption_resolution,[],[f3796,f171]) ).
fof(f3802,plain,
( ~ incident(b3,b2b3)
| spl2_6
| ~ spl2_23
| ~ spl2_74 ),
inference(forward_demodulation,[],[f3800,f1522]) ).
fof(f3805,plain,
( $false
| spl2_6
| ~ spl2_23
| ~ spl2_74 ),
inference(forward_subsumption_resolution,[],[f3802,f101]) ).
fof(f3806,plain,
( spl2_6
| ~ spl2_23
| ~ spl2_74 ),
inference(avatar_contradiction_clause,[],[f3805]) ).
fof(f3808,plain,
( a1 = a3
| ~ spl2_52
| ~ spl2_83 ),
inference(forward_demodulation,[],[f1588,f1033]) ).
fof(f3816,plain,
( $false
| spl2_8
| ~ spl2_52
| ~ spl2_83 ),
inference(forward_subsumption_resolution,[],[f3808,f181]) ).
fof(f3817,plain,
( spl2_8
| ~ spl2_52
| ~ spl2_83 ),
inference(avatar_contradiction_clause,[],[f3816]) ).
fof(f3835,plain,
( $false
| spl2_7
| ~ spl2_25
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f1497,f408]) ).
fof(f3836,plain,
( spl2_7
| ~ spl2_25
| ~ spl2_72 ),
inference(avatar_contradiction_clause,[],[f3835]) ).
fof(f3849,plain,
( $false
| spl2_47
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f1946,f785]) ).
fof(f3850,plain,
( spl2_47
| ~ spl2_84 ),
inference(avatar_contradiction_clause,[],[f3849]) ).
fof(f4003,plain,
( incident(a3,b2b3)
| ~ spl2_69 ),
inference(superposition,[],[f101,f1271]) ).
fof(f4033,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(p3,X0)
| ~ incident(p1,X0) )
| ~ spl2_17
| ~ spl2_83 ),
inference(superposition,[],[f224,f1588]) ).
fof(f4048,plain,
( ! [X0] :
( ~ incident(a3,X0)
| ~ incident(a3,X0)
| ~ incident(p3,X0) )
| ~ spl2_17
| ~ spl2_59
| ~ spl2_83 ),
inference(forward_demodulation,[],[f4033,f1144]) ).
fof(f4049,plain,
( ! [X0] :
( ~ incident(p3,X0)
| ~ incident(a3,X0) )
| ~ spl2_17
| ~ spl2_59
| ~ spl2_83 ),
inference(duplicate_literal_removal,[],[f4048]) ).
fof(f4050,plain,
( incident(s,b2b3)
| ~ spl2_60
| ~ spl2_109 ),
inference(forward_demodulation,[],[f2171,f1156]) ).
fof(f4051,plain,
( $false
| ~ spl2_60
| spl2_66
| ~ spl2_109 ),
inference(forward_subsumption_resolution,[],[f4050,f1204]) ).
fof(f4052,plain,
( ~ spl2_60
| spl2_66
| ~ spl2_109 ),
inference(avatar_contradiction_clause,[],[f4051]) ).
fof(f4062,plain,
( a3 != b2
| spl2_67
| ~ spl2_110 ),
inference(superposition,[],[f1207,f2176]) ).
fof(f4166,plain,
( ~ incident(a3,b1b2)
| ~ spl2_17
| ~ spl2_59
| ~ spl2_83 ),
inference(resolution,[],[f4049,f114]) ).
fof(f4172,plain,
( a1 = b1
| ~ incident(a1,b3b1)
| ~ spl2_41 ),
inference(resolution,[],[f703,f107]) ).
fof(f4174,plain,
( b1 = s
| ~ incident(s,b3b1)
| ~ spl2_41 ),
inference(resolution,[],[f703,f104]) ).
fof(f4182,plain,
( b1 = s
| ~ incident(s,b1b2)
| ~ spl2_85 ),
inference(resolution,[],[f1626,f104]) ).
fof(f4188,plain,
( a2 = b2
| ~ incident(b2,a2a3)
| ~ spl2_96 ),
inference(resolution,[],[f1861,f111]) ).
fof(f4189,plain,
( a2 = s
| ~ incident(s,a2a3)
| ~ spl2_96 ),
inference(resolution,[],[f1861,f105]) ).
fof(f4194,plain,
( p3 = a2
| ~ incident(p3,a2a3)
| ~ spl2_98 ),
inference(resolution,[],[f1869,f113]) ).
fof(f4221,plain,
( a2 = a3
| ~ incident(a3,b3b1)
| ~ spl2_130 ),
inference(resolution,[],[f3341,f95]) ).
fof(f4226,plain,
( ~ incident(a3,b3b1)
| spl2_9
| ~ spl2_130 ),
inference(forward_subsumption_resolution,[],[f4221,f186]) ).
fof(f4228,plain,
( $false
| spl2_9
| ~ spl2_44
| ~ spl2_130 ),
inference(forward_subsumption_resolution,[],[f4226,f742]) ).
fof(f4229,plain,
( spl2_9
| ~ spl2_44
| ~ spl2_130 ),
inference(avatar_contradiction_clause,[],[f4228]) ).
fof(f4251,plain,
( ~ incident(b3,b2b3)
| ~ spl2_60
| spl2_69
| ~ spl2_77
| ~ spl2_108 ),
inference(forward_demodulation,[],[f2746,f1156]) ).
fof(f4285,plain,
( $false
| ~ spl2_60
| spl2_69
| ~ spl2_77
| ~ spl2_108 ),
inference(forward_subsumption_resolution,[],[f4251,f101]) ).
fof(f4286,plain,
( ~ spl2_60
| spl2_69
| ~ spl2_77
| ~ spl2_108 ),
inference(avatar_contradiction_clause,[],[f4285]) ).
fof(f4430,plain,
( incident(a1,a2a3)
| ~ spl2_97 ),
inference(superposition,[],[f92,f1866]) ).
fof(f4620,plain,
( ~ incident(b1,b3b1)
| spl2_54
| ~ spl2_55 ),
inference(superposition,[],[f1090,f1094]) ).
fof(f4621,plain,
( $false
| spl2_54
| ~ spl2_55 ),
inference(forward_subsumption_resolution,[],[f4620,f103]) ).
fof(f4622,plain,
( spl2_54
| ~ spl2_55 ),
inference(avatar_contradiction_clause,[],[f4621]) ).
fof(f4645,plain,
( a2 = b1
| ~ spl2_57
| ~ spl2_62 ),
inference(forward_demodulation,[],[f1169,f1135]) ).
fof(f4679,plain,
( ~ incident(b2,b2b3)
| spl2_66
| ~ spl2_67 ),
inference(superposition,[],[f1204,f1208]) ).
fof(f4680,plain,
( $false
| spl2_66
| ~ spl2_67 ),
inference(forward_subsumption_resolution,[],[f4679,f100]) ).
fof(f4681,plain,
( spl2_66
| ~ spl2_67 ),
inference(avatar_contradiction_clause,[],[f4680]) ).
fof(f4703,plain,
( incident(a2,b1b2)
| ~ spl2_71 ),
inference(superposition,[],[f98,f1344]) ).
fof(f4718,plain,
( $false
| ~ spl2_71
| spl2_91 ),
inference(forward_subsumption_resolution,[],[f4703,f1751]) ).
fof(f4719,plain,
( ~ spl2_71
| spl2_91 ),
inference(avatar_contradiction_clause,[],[f4718]) ).
fof(f4758,plain,
( ~ incident(a2,sK0(p2,a2))
| ~ spl2_17
| ~ spl2_38
| ~ spl2_57 ),
inference(forward_demodulation,[],[f636,f1135]) ).
fof(f4788,plain,
( ~ spl2_54
| spl2_55
| ~ spl2_41 ),
inference(avatar_split_clause,[],[f4174,f702,f1092,f1088]) ).
fof(f4841,plain,
( $false
| spl2_44
| ~ spl2_45 ),
inference(forward_subsumption_resolution,[],[f750,f743]) ).
fof(f4842,plain,
( spl2_44
| ~ spl2_45 ),
inference(avatar_contradiction_clause,[],[f4841]) ).
fof(f4860,plain,
( ~ spl2_15
| spl2_82
| ~ spl2_61 ),
inference(avatar_split_clause,[],[f3562,f1158,f1576,f212]) ).
fof(f4919,plain,
( incident(a2,b1b2)
| ~ spl2_89 ),
inference(superposition,[],[f99,f1681]) ).
fof(f4997,plain,
( ~ spl2_53
| spl2_56
| ~ spl2_41 ),
inference(avatar_split_clause,[],[f4172,f702,f1128,f1035]) ).
fof(f5225,plain,
( a1 = a2
| ~ spl2_38
| ~ spl2_46 ),
inference(superposition,[],[f781,f609]) ).
fof(f5245,plain,
( $false
| spl2_10
| ~ spl2_38
| ~ spl2_46 ),
inference(forward_subsumption_resolution,[],[f5225,f191]) ).
fof(f5246,plain,
( spl2_10
| ~ spl2_38
| ~ spl2_46 ),
inference(avatar_contradiction_clause,[],[f5245]) ).
fof(f5266,plain,
( ~ incident(p3,sK0(p1,a1))
| ~ spl2_17
| ~ spl2_52 ),
inference(superposition,[],[f327,f1033]) ).
fof(f5274,plain,
( ~ incident(a1,sK0(p1,a1))
| ~ spl2_17
| ~ spl2_46
| ~ spl2_52 ),
inference(forward_demodulation,[],[f5266,f781]) ).
fof(f5290,plain,
( incident(s,a2a3)
| ~ spl2_95 ),
inference(superposition,[],[f105,f1858]) ).
fof(f5322,plain,
( ~ incident(a3,a3a1)
| spl2_18
| ~ spl2_59 ),
inference(superposition,[],[f305,f1144]) ).
fof(f5331,plain,
( $false
| spl2_18
| ~ spl2_59 ),
inference(forward_subsumption_resolution,[],[f5322,f96]) ).
fof(f5332,plain,
( spl2_18
| ~ spl2_59 ),
inference(avatar_contradiction_clause,[],[f5331]) ).
fof(f5366,plain,
( $false
| ~ spl2_27
| spl2_67
| ~ spl2_110 ),
inference(forward_subsumption_resolution,[],[f4062,f416]) ).
fof(f5367,plain,
( ~ spl2_27
| spl2_67
| ~ spl2_110 ),
inference(avatar_contradiction_clause,[],[f5366]) ).
fof(f5485,plain,
( $false
| ~ spl2_95
| spl2_100 ),
inference(forward_subsumption_resolution,[],[f5290,f1979]) ).
fof(f5486,plain,
( ~ spl2_95
| spl2_100 ),
inference(avatar_contradiction_clause,[],[f5485]) ).
fof(f5514,plain,
! [X0] :
( ~ incident(X0,s3)
| ~ incident(X0,a3a1)
| a3a1 = s3
| a3 = X0 ),
inference(resolution,[],[f358,f96]) ).
fof(f5612,plain,
( ~ point(p1)
| ~ point(a1)
| ~ spl2_17
| ~ spl2_46
| ~ spl2_52 ),
inference(resolution,[],[f5274,f135]) ).
fof(f5613,plain,
( ~ point(a1)
| ~ spl2_17
| ~ spl2_46
| ~ spl2_52 ),
inference(forward_subsumption_resolution,[],[f5612,f230]) ).
fof(f5614,plain,
( $false
| ~ spl2_17
| ~ spl2_46
| ~ spl2_52 ),
inference(forward_subsumption_resolution,[],[f5613,f243]) ).
fof(f5615,plain,
( ~ spl2_17
| ~ spl2_46
| ~ spl2_52 ),
inference(avatar_contradiction_clause,[],[f5614]) ).
fof(f5621,plain,
( $false
| ~ spl2_57
| ~ spl2_62
| spl2_71 ),
inference(forward_subsumption_resolution,[],[f4645,f1343]) ).
fof(f5622,plain,
( ~ spl2_57
| ~ spl2_62
| spl2_71 ),
inference(avatar_contradiction_clause,[],[f5621]) ).
fof(f5639,definition,
( spl2_164
<=> incident(p1,b1b2) ),
introduced(definition,[new_symbols(definition,[spl2_164])],[avatar_definition]) ).
fof(f5641,plain,
( ~ incident(p1,b1b2)
| spl2_164 ),
inference(avatar_component_clause,[],[f5639]) ).
fof(f5644,plain,
( ~ incident(a3,b1b2)
| spl2_45
| ~ spl2_87 ),
inference(forward_subsumption_resolution,[],[f1959,f746]) ).
fof(f5647,plain,
( ~ incident(p1,b1b2)
| p1 = b1
| spl2_3
| ~ spl2_87 ),
inference(forward_subsumption_resolution,[],[f2230,f258]) ).
fof(f5665,plain,
( ~ spl2_66
| spl2_74
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f3509,f478,f1520,f1202]) ).
fof(f5735,plain,
( ~ spl2_58
| spl2_89
| ~ spl2_23 ),
inference(avatar_split_clause,[],[f3493,f379,f1679,f1137]) ).
fof(f5736,plain,
( ~ spl2_66
| spl2_67
| ~ spl2_23 ),
inference(avatar_split_clause,[],[f3495,f379,f1206,f1202]) ).
fof(f5767,plain,
( spl2_107
| spl2_108 ),
inference(avatar_split_clause,[],[f5514,f2159,f2155]) ).
fof(f5785,plain,
( ! [X0] :
( ~ incident(X0,a2a3)
| ~ incident(X0,b3b1)
| b3b1 = a2a3
| a2 = X0 )
| ~ spl2_13 ),
inference(resolution,[],[f205,f341]) ).
fof(f5792,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,a1a2)
| b3b1 = a1a2
| b3 = X0 )
| ~ spl2_16 ),
inference(resolution,[],[f218,f336]) ).
fof(f5802,plain,
( spl2_79
| spl2_80
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f5792,f216,f1567,f1563]) ).
fof(f5812,plain,
( incident(b2,a2a3)
| ~ spl2_95 ),
inference(superposition,[],[f111,f1858]) ).
fof(f5857,plain,
( $false
| spl2_26
| ~ spl2_69 ),
inference(forward_subsumption_resolution,[],[f4003,f412]) ).
fof(f5858,plain,
( spl2_26
| ~ spl2_69 ),
inference(avatar_contradiction_clause,[],[f5857]) ).
fof(f5874,plain,
( spl2_64
| spl2_130
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f5785,f203,f3340,f1176]) ).
fof(f5897,plain,
( $false
| ~ spl2_11
| spl2_45
| ~ spl2_87 ),
inference(forward_subsumption_resolution,[],[f5644,f196]) ).
fof(f5898,plain,
( ~ spl2_11
| spl2_45
| ~ spl2_87 ),
inference(avatar_contradiction_clause,[],[f5897]) ).
fof(f5931,plain,
( ~ spl2_54
| spl2_74
| ~ spl2_77 ),
inference(avatar_split_clause,[],[f3571,f1539,f1520,f1088]) ).
fof(f5967,plain,
( ~ spl2_50
| spl2_38
| ~ spl2_98 ),
inference(avatar_split_clause,[],[f4194,f1868,f607,f1020]) ).
fof(f6097,plain,
( a3 = s
| ~ spl2_45
| ~ spl2_55 ),
inference(forward_demodulation,[],[f1094,f747]) ).
fof(f6176,plain,
( $false
| ~ spl2_45
| ~ spl2_55
| spl2_110 ),
inference(forward_subsumption_resolution,[],[f6097,f2175]) ).
fof(f6177,plain,
( ~ spl2_45
| ~ spl2_55
| spl2_110 ),
inference(avatar_contradiction_clause,[],[f6176]) ).
fof(f6181,plain,
( $false
| ~ spl2_95
| spl2_127 ),
inference(forward_subsumption_resolution,[],[f5812,f3217]) ).
fof(f6182,plain,
( ~ spl2_95
| spl2_127 ),
inference(avatar_contradiction_clause,[],[f6181]) ).
fof(f6253,plain,
( ~ incident(b2,b2b3)
| p1 = b2
| spl2_3
| ~ spl2_127 ),
inference(resolution,[],[f3216,f556]) ).
fof(f6257,plain,
( p1 = b2
| spl2_3
| ~ spl2_127 ),
inference(forward_subsumption_resolution,[],[f6253,f100]) ).
fof(f6273,plain,
( ~ incident(b2,b1b2)
| spl2_3
| ~ spl2_127
| spl2_164 ),
inference(superposition,[],[f5641,f6257]) ).
fof(f6274,plain,
( $false
| spl2_3
| ~ spl2_127
| spl2_164 ),
inference(forward_subsumption_resolution,[],[f6273,f99]) ).
fof(f6275,plain,
( spl2_3
| ~ spl2_127
| spl2_164 ),
inference(avatar_contradiction_clause,[],[f6274]) ).
fof(f6282,plain,
( a2 != b2
| spl2_3
| spl2_57
| ~ spl2_127 ),
inference(forward_demodulation,[],[f1134,f6257]) ).
fof(f6283,plain,
( p1 = a3
| ~ spl2_45
| ~ spl2_62 ),
inference(forward_demodulation,[],[f1169,f747]) ).
fof(f6285,plain,
( $false
| ~ spl2_45
| spl2_59
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f6283,f1143]) ).
fof(f6286,plain,
( ~ spl2_45
| spl2_59
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f6285]) ).
fof(f6303,plain,
( $false
| ~ spl2_89
| spl2_91 ),
inference(forward_subsumption_resolution,[],[f4919,f1751]) ).
fof(f6304,plain,
( ~ spl2_89
| spl2_91 ),
inference(avatar_contradiction_clause,[],[f6303]) ).
fof(f6324,plain,
( ~ spl2_99
| spl2_55
| ~ spl2_85 ),
inference(avatar_split_clause,[],[f4182,f1625,f1092,f1938]) ).
fof(f6346,plain,
( $false
| ~ spl2_11
| ~ spl2_17
| ~ spl2_59
| ~ spl2_83 ),
inference(forward_subsumption_resolution,[],[f4166,f196]) ).
fof(f6347,plain,
( ~ spl2_11
| ~ spl2_17
| ~ spl2_59
| ~ spl2_83 ),
inference(avatar_contradiction_clause,[],[f6346]) ).
fof(f6353,plain,
( ~ spl2_164
| spl2_62
| ~ spl2_87 ),
inference(avatar_split_clause,[],[f1957,f1633,f1167,f5639]) ).
fof(f6363,plain,
( spl2_62
| ~ spl2_164
| spl2_3
| ~ spl2_87 ),
inference(avatar_split_clause,[],[f5647,f1633,f154,f5639,f1167]) ).
fof(f6367,plain,
( ~ spl2_127
| spl2_89
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f4188,f1860,f1679,f3215]) ).
fof(f6395,plain,
( ~ spl2_44
| spl2_69
| ~ spl2_77 ),
inference(avatar_split_clause,[],[f3569,f1539,f1269,f741]) ).
fof(f6430,plain,
( ~ spl2_26
| spl2_69
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f3507,f478,f1269,f410]) ).
fof(f6468,plain,
( spl2_62
| ~ spl2_63
| spl2_3
| ~ spl2_65 ),
inference(avatar_split_clause,[],[f2866,f1180,f154,f1171,f1167]) ).
fof(f6474,plain,
( ~ spl2_13
| spl2_126
| ~ spl2_80 ),
inference(avatar_split_clause,[],[f3578,f1567,f3152,f203]) ).
fof(f6512,plain,
( ! [X0] :
( ~ incident(X0,b1b2)
| ~ incident(X0,a2a3)
| b1b2 = a2a3
| b1 = X0 )
| ~ spl2_14 ),
inference(resolution,[],[f209,f339]) ).
fof(f6513,plain,
( ! [X0] :
( ~ incident(X0,b3b1)
| ~ incident(X0,a2a3)
| b3b1 = a2a3
| b1 = X0 )
| ~ spl2_14 ),
inference(resolution,[],[f209,f335]) ).
fof(f6519,plain,
( spl2_64
| spl2_65
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f6513,f207,f1180,f1176]) ).
fof(f6520,plain,
( spl2_86
| spl2_87
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f6512,f207,f1633,f1629]) ).
fof(f6523,plain,
( ! [X0] :
( ~ incident(X0,b2b3)
| ~ incident(X0,a1a2)
| b2b3 = a1a2
| b3 = X0 )
| ~ spl2_16 ),
inference(resolution,[],[f218,f331]) ).
fof(f6531,plain,
( spl2_32
| spl2_33
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f6523,f216,f486,f482]) ).
fof(f6542,plain,
( ~ incident(p3,b1b2)
| spl2_50
| ~ spl2_86 ),
inference(superposition,[],[f1022,f1631]) ).
fof(f6546,plain,
( $false
| spl2_50
| ~ spl2_86 ),
inference(forward_subsumption_resolution,[],[f6542,f114]) ).
fof(f6547,plain,
( spl2_50
| ~ spl2_86 ),
inference(avatar_contradiction_clause,[],[f6546]) ).
fof(f6631,plain,
( incident(s,b1b2)
| ~ spl2_86
| ~ spl2_100 ),
inference(forward_demodulation,[],[f1978,f1631]) ).
fof(f6632,plain,
( $false
| ~ spl2_86
| spl2_99
| ~ spl2_100 ),
inference(forward_subsumption_resolution,[],[f6631,f1940]) ).
fof(f6633,plain,
( ~ spl2_86
| spl2_99
| ~ spl2_100 ),
inference(avatar_contradiction_clause,[],[f6632]) ).
fof(f6679,plain,
( a2 != b2
| spl2_6
| ~ spl2_126 ),
inference(superposition,[],[f171,f3154]) ).
fof(f6689,plain,
( $false
| spl2_6
| ~ spl2_89
| ~ spl2_126 ),
inference(forward_subsumption_resolution,[],[f6679,f1681]) ).
fof(f6690,plain,
( spl2_6
| ~ spl2_89
| ~ spl2_126 ),
inference(avatar_contradiction_clause,[],[f6689]) ).
fof(f6838,plain,
! [X2,X0,X1] :
( ~ incident(X0,X1)
| ~ incident(X2,X1)
| sK0(X0,X2) = X1
| X0 = X2
| ~ point(X2)
| ~ point(X0)
| ~ point(X2) ),
inference(resolution,[],[f362,f135]) ).
fof(f6847,plain,
! [X2,X0,X1] :
( ~ incident(X0,X1)
| ~ incident(X2,X1)
| sK0(X0,X2) = X1
| X0 = X2
| ~ point(X2)
| ~ point(X0) ),
inference(duplicate_literal_removal,[],[f6838]) ).
fof(f6848,plain,
! [X2,X0,X1] :
( ~ incident(X0,X1)
| ~ incident(X2,X1)
| sK0(X0,X2) = X1
| X0 = X2
| ~ point(X2) ),
inference(forward_subsumption_resolution,[],[f6847,f119]) ).
fof(f6849,plain,
! [X2,X0,X1] :
( ~ incident(X2,X1)
| ~ incident(X0,X1)
| sK0(X0,X2) = X1
| X0 = X2 ),
inference(forward_subsumption_resolution,[],[f6848,f119]) ).
fof(f6904,plain,
( ~ point(p2)
| ~ point(a2)
| ~ spl2_17
| ~ spl2_38
| ~ spl2_57 ),
inference(resolution,[],[f4758,f135]) ).
fof(f6905,plain,
( ~ point(a2)
| ~ spl2_17
| ~ spl2_38
| ~ spl2_57 ),
inference(forward_subsumption_resolution,[],[f6904,f231]) ).
fof(f6906,plain,
( $false
| ~ spl2_17
| ~ spl2_38
| ~ spl2_57 ),
inference(forward_subsumption_resolution,[],[f6905,f239]) ).
fof(f6907,plain,
( ~ spl2_17
| ~ spl2_38
| ~ spl2_57 ),
inference(avatar_contradiction_clause,[],[f6906]) ).
fof(f6927,plain,
( $false
| spl2_3
| spl2_57
| ~ spl2_89
| ~ spl2_127 ),
inference(forward_subsumption_resolution,[],[f6282,f1681]) ).
fof(f6928,plain,
( spl2_3
| spl2_57
| ~ spl2_89
| ~ spl2_127 ),
inference(avatar_contradiction_clause,[],[f6927]) ).
fof(f6948,plain,
( ~ incident(b2,b1b2)
| ~ spl2_86
| spl2_127 ),
inference(forward_demodulation,[],[f3217,f1631]) ).
fof(f6956,plain,
( $false
| ~ spl2_86
| spl2_127 ),
inference(forward_subsumption_resolution,[],[f6948,f99]) ).
fof(f6957,plain,
( ~ spl2_86
| spl2_127 ),
inference(avatar_contradiction_clause,[],[f6956]) ).
fof(f6974,plain,
( $false
| spl2_13
| ~ spl2_64 ),
inference(forward_subsumption_resolution,[],[f1353,f204]) ).
fof(f6975,plain,
( spl2_13
| ~ spl2_64 ),
inference(avatar_contradiction_clause,[],[f6974]) ).
fof(f7008,plain,
( incident(a1,b1b2)
| ~ spl2_86
| ~ spl2_97 ),
inference(forward_demodulation,[],[f4430,f1631]) ).
fof(f7084,plain,
( $false
| spl2_47
| ~ spl2_86
| ~ spl2_97 ),
inference(forward_subsumption_resolution,[],[f7008,f785]) ).
fof(f7085,plain,
( spl2_47
| ~ spl2_86
| ~ spl2_97 ),
inference(avatar_contradiction_clause,[],[f7084]) ).
fof(f7140,plain,
( ~ spl2_44
| spl2_45
| ~ spl2_65 ),
inference(avatar_split_clause,[],[f1917,f1180,f745,f741]) ).
fof(f7520,plain,
( ~ incident(a2,sK0(p2,b2))
| spl2_3
| ~ spl2_17
| ~ spl2_38
| ~ spl2_127 ),
inference(forward_demodulation,[],[f636,f6257]) ).
fof(f7521,plain,
( ~ incident(a2,sK0(a3,b2))
| spl2_3
| ~ spl2_17
| ~ spl2_38
| ~ spl2_83
| ~ spl2_127 ),
inference(forward_demodulation,[],[f7520,f1588]) ).
fof(f8091,plain,
! [X0] :
( ~ incident(X0,b1b2)
| b1b2 = sK0(X0,b2)
| b2 = X0 ),
inference(resolution,[],[f6849,f99]) ).
fof(f8239,plain,
( b1b2 = sK0(a3,b2)
| a3 = b2
| ~ spl2_11 ),
inference(resolution,[],[f8091,f196]) ).
fof(f8249,plain,
( b1b2 = sK0(a3,b2)
| ~ spl2_11
| spl2_27 ),
inference(forward_subsumption_resolution,[],[f8239,f415]) ).
fof(f8256,plain,
( ~ incident(a2,b1b2)
| spl2_3
| ~ spl2_11
| ~ spl2_17
| spl2_27
| ~ spl2_38
| ~ spl2_83
| ~ spl2_127 ),
inference(superposition,[],[f7521,f8249]) ).
fof(f8263,plain,
( $false
| spl2_3
| ~ spl2_11
| ~ spl2_17
| spl2_27
| ~ spl2_38
| ~ spl2_83
| ~ spl2_91
| ~ spl2_127 ),
inference(forward_subsumption_resolution,[],[f8256,f1750]) ).
fof(f8264,plain,
( spl2_3
| ~ spl2_11
| ~ spl2_17
| spl2_27
| ~ spl2_38
| ~ spl2_83
| ~ spl2_91
| ~ spl2_127 ),
inference(avatar_contradiction_clause,[],[f8263]) ).
fof(f8301,plain,
( a2 = a3
| ~ incident(s,a2a3)
| ~ spl2_96
| ~ spl2_110 ),
inference(forward_demodulation,[],[f4189,f2176]) ).
fof(f8367,plain,
( ~ incident(s,a2a3)
| spl2_9
| ~ spl2_96
| ~ spl2_110 ),
inference(forward_subsumption_resolution,[],[f8301,f186]) ).
fof(f8388,plain,
( ~ incident(a3,a2a3)
| spl2_9
| ~ spl2_96
| ~ spl2_110 ),
inference(forward_demodulation,[],[f8367,f2176]) ).
fof(f8392,plain,
( $false
| spl2_9
| ~ spl2_96
| ~ spl2_110 ),
inference(forward_subsumption_resolution,[],[f8388,f95]) ).
fof(f8393,plain,
( spl2_9
| ~ spl2_96
| ~ spl2_110 ),
inference(avatar_contradiction_clause,[],[f8392]) ).
cnf(s1,plain,
( spl2_1
| ~ spl2_2 ),
inference(sat_conversion,[],[f152]) ).
cnf(s2,plain,
( spl2_1
| ~ spl2_3 ),
inference(sat_conversion,[],[f157]) ).
cnf(s3,plain,
( spl2_1
| ~ spl2_4 ),
inference(sat_conversion,[],[f162]) ).
cnf(s4,plain,
( spl2_1
| ~ spl2_5 ),
inference(sat_conversion,[],[f167]) ).
cnf(s5,plain,
( spl2_1
| ~ spl2_6 ),
inference(sat_conversion,[],[f172]) ).
cnf(s6,plain,
( spl2_1
| ~ spl2_7 ),
inference(sat_conversion,[],[f177]) ).
cnf(s7,plain,
( spl2_1
| ~ spl2_8 ),
inference(sat_conversion,[],[f182]) ).
cnf(s8,plain,
( spl2_1
| ~ spl2_9 ),
inference(sat_conversion,[],[f187]) ).
cnf(s9,plain,
( spl2_1
| ~ spl2_10 ),
inference(sat_conversion,[],[f192]) ).
cnf(s10,plain,
( spl2_11
| spl2_12 ),
inference(sat_conversion,[],[f201]) ).
cnf(s11,plain,
( spl2_13
| spl2_14 ),
inference(sat_conversion,[],[f210]) ).
cnf(s12,plain,
( spl2_15
| spl2_16 ),
inference(sat_conversion,[],[f219]) ).
cnf(s13,plain,
( spl2_1
| ~ spl2_12
| ~ spl2_14
| ~ spl2_16 ),
inference(sat_conversion,[],[f220]) ).
cnf(s14,plain,
( spl2_1
| ~ spl2_11
| ~ spl2_13
| ~ spl2_15 ),
inference(sat_conversion,[],[f221]) ).
cnf(s15,plain,
( spl2_1
| spl2_17 ),
inference(sat_conversion,[],[f225]) ).
cnf(s16,plain,
~ spl2_1,
inference(sat_conversion,[],[f227]) ).
cnf(s17,plain,
( ~ spl2_17
| ~ spl2_18
| ~ spl2_19 ),
inference(sat_conversion,[],[f310]) ).
cnf(s19,plain,
( spl2_22
| spl2_23 ),
inference(sat_conversion,[],[f381]) ).
cnf(s20,plain,
( spl2_24
| spl2_25 ),
inference(sat_conversion,[],[f389]) ).
cnf(s24,plain,
( spl2_30
| spl2_31 ),
inference(sat_conversion,[],[f480]) ).
cnf(s31,plain,
( spl2_26
| ~ spl2_30 ),
inference(sat_conversion,[],[f628]) ).
cnf(s34,plain,
( spl2_15
| ~ spl2_32 ),
inference(sat_conversion,[],[f660]) ).
cnf(s39,plain,
( spl2_40
| spl2_41 ),
inference(sat_conversion,[],[f704]) ).
cnf(s43,plain,
( spl2_4
| spl2_46
| ~ spl2_47 ),
inference(sat_conversion,[],[f786]) ).
cnf(s45,plain,
( spl2_19
| ~ spl2_46 ),
inference(sat_conversion,[],[f810]) ).
cnf(s50,plain,
( spl2_2
| spl2_3
| ~ spl2_17
| ~ spl2_22
| ~ spl2_40 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s51,plain,
( spl2_2
| spl2_52
| ~ spl2_53 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s53,plain,
( spl2_5
| ~ spl2_13
| ~ spl2_22
| ~ spl2_31
| ~ spl2_33
| ~ spl2_41 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s56,plain,
( ~ spl2_24
| spl2_28 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s60,plain,
( spl2_3
| spl2_57
| ~ spl2_58 ),
inference(sat_conversion,[],[f1140]) ).
cnf(s61,plain,
( spl2_3
| ~ spl2_26
| spl2_59 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s66,plain,
( ~ spl2_15
| spl2_47
| ~ spl2_61 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s67,plain,
( spl2_37
| ~ spl2_60 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s68,plain,
( spl2_26
| ~ spl2_60 ),
inference(sat_conversion,[],[f1262]) ).
cnf(s72,plain,
( spl2_44
| ~ spl2_69 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s76,plain,
( spl2_3
| ~ spl2_17
| ~ spl2_37
| ~ spl2_59
| ~ spl2_64 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s77,plain,
( spl2_11
| ~ spl2_45 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s80,plain,
( ~ spl2_30
| spl2_66 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s85,plain,
( ~ spl2_67
| spl2_72
| spl2_73 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s86,plain,
( ~ spl2_15
| spl2_47
| ~ spl2_73 ),
inference(sat_conversion,[],[f1494]) ).
cnf(s87,plain,
( spl2_63
| ~ spl2_72 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s88,plain,
( spl2_45
| ~ spl2_59
| ~ spl2_62 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s89,plain,
( ~ spl2_22
| spl2_58 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s90,plain,
( spl2_3
| spl2_9
| ~ spl2_22
| ~ spl2_26 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s94,plain,
( ~ spl2_40
| spl2_53 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s95,plain,
( ~ spl2_40
| spl2_54 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s97,plain,
( spl2_76
| spl2_77 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s103,plain,
( spl2_2
| ~ spl2_44
| spl2_83 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s124,plain,
( spl2_18
| ~ spl2_60 ),
inference(sat_conversion,[],[f1722]) ).
cnf(s131,plain,
( spl2_4
| spl2_38
| ~ spl2_91 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s143,plain,
( spl2_95
| spl2_96 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s146,plain,
( spl2_7
| ~ spl2_47
| ~ spl2_82
| ~ spl2_85 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s154,plain,
( spl2_8
| ~ spl2_49
| spl2_107 ),
inference(sat_conversion,[],[f2421]) ).
cnf(s156,plain,
( spl2_4
| spl2_10
| ~ spl2_29
| spl2_67
| ~ spl2_82
| ~ spl2_84 ),
inference(sat_conversion,[],[f2572]) ).
cnf(s157,plain,
( spl2_49
| ~ spl2_67
| ~ spl2_82 ),
inference(sat_conversion,[],[f2583]) ).
cnf(s158,plain,
( ~ spl2_107
| spl2_109 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s163,plain,
( spl2_2
| spl2_37
| ~ spl2_107 ),
inference(sat_conversion,[],[f2682]) ).
cnf(s164,plain,
( ~ spl2_17
| ~ spl2_28
| ~ spl2_37 ),
inference(sat_conversion,[],[f2704]) ).
cnf(s174,plain,
( spl2_29
| ~ spl2_46
| ~ spl2_82 ),
inference(sat_conversion,[],[f2742]) ).
cnf(s204,plain,
( spl2_8
| ~ spl2_11
| ~ spl2_47
| spl2_93 ),
inference(sat_conversion,[],[f2854]) ).
cnf(s227,plain,
( spl2_44
| ~ spl2_76 ),
inference(sat_conversion,[],[f2959]) ).
cnf(s228,plain,
( spl2_54
| ~ spl2_76 ),
inference(sat_conversion,[],[f2961]) ).
cnf(s250,plain,
( ~ spl2_86
| spl2_91 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s253,plain,
( spl2_12
| ~ spl2_93 ),
inference(sat_conversion,[],[f3086]) ).
cnf(s259,plain,
( ~ spl2_37
| spl2_52
| ~ spl2_61
| ~ spl2_82 ),
inference(sat_conversion,[],[f3097]) ).
cnf(s349,plain,
( ~ spl2_12
| spl2_60
| spl2_61 ),
inference(sat_conversion,[],[f3333]) ).
cnf(s356,plain,
( spl2_97
| spl2_98 ),
inference(sat_conversion,[],[f3467]) ).
cnf(s362,plain,
( ~ spl2_13
| spl2_58
| ~ spl2_80 ),
inference(sat_conversion,[],[f3601]) ).
cnf(s370,plain,
( spl2_53
| ~ spl2_79 ),
inference(sat_conversion,[],[f3652]) ).
cnf(s377,plain,
( spl2_84
| spl2_85 ),
inference(sat_conversion,[],[f3685]) ).
cnf(s380,plain,
( spl2_47
| ~ spl2_56 ),
inference(sat_conversion,[],[f3749]) ).
cnf(s382,plain,
( spl2_40
| spl2_41 ),
inference(sat_conversion,[],[f3751]) ).
cnf(s388,plain,
( spl2_6
| ~ spl2_23
| ~ spl2_74 ),
inference(sat_conversion,[],[f3806]) ).
cnf(s392,plain,
( spl2_8
| ~ spl2_52
| ~ spl2_83 ),
inference(sat_conversion,[],[f3817]) ).
cnf(s397,plain,
( spl2_7
| ~ spl2_25
| ~ spl2_72 ),
inference(sat_conversion,[],[f3836]) ).
cnf(s409,plain,
( spl2_47
| ~ spl2_84 ),
inference(sat_conversion,[],[f3850]) ).
cnf(s441,plain,
( ~ spl2_60
| spl2_66
| ~ spl2_109 ),
inference(sat_conversion,[],[f4052]) ).
cnf(s450,plain,
( spl2_9
| ~ spl2_44
| ~ spl2_130 ),
inference(sat_conversion,[],[f4229]) ).
cnf(s467,plain,
( ~ spl2_60
| spl2_69
| ~ spl2_77
| ~ spl2_108 ),
inference(sat_conversion,[],[f4286]) ).
cnf(s518,plain,
( spl2_54
| ~ spl2_55 ),
inference(sat_conversion,[],[f4622]) ).
cnf(s522,plain,
( spl2_66
| ~ spl2_67 ),
inference(sat_conversion,[],[f4681]) ).
cnf(s525,plain,
( ~ spl2_71
| spl2_91 ),
inference(sat_conversion,[],[f4719]) ).
cnf(s530,plain,
( ~ spl2_41
| ~ spl2_54
| spl2_55 ),
inference(sat_conversion,[],[f4788]) ).
cnf(s539,plain,
( spl2_44
| ~ spl2_45 ),
inference(sat_conversion,[],[f4842]) ).
cnf(s546,plain,
( ~ spl2_15
| ~ spl2_61
| spl2_82 ),
inference(sat_conversion,[],[f4860]) ).
cnf(s588,plain,
( ~ spl2_41
| ~ spl2_53
| spl2_56 ),
inference(sat_conversion,[],[f4997]) ).
cnf(s624,plain,
( spl2_10
| ~ spl2_38
| ~ spl2_46 ),
inference(sat_conversion,[],[f5246]) ).
cnf(s629,plain,
( spl2_18
| ~ spl2_59 ),
inference(sat_conversion,[],[f5332]) ).
cnf(s632,plain,
( ~ spl2_27
| spl2_67
| ~ spl2_110 ),
inference(sat_conversion,[],[f5367]) ).
cnf(s641,plain,
( ~ spl2_95
| spl2_100 ),
inference(sat_conversion,[],[f5486]) ).
cnf(s647,plain,
( ~ spl2_17
| ~ spl2_46
| ~ spl2_52 ),
inference(sat_conversion,[],[f5615]) ).
cnf(s651,plain,
( ~ spl2_57
| ~ spl2_62
| spl2_71 ),
inference(sat_conversion,[],[f5622]) ).
cnf(s664,plain,
( ~ spl2_31
| ~ spl2_66
| spl2_74 ),
inference(sat_conversion,[],[f5665]) ).
cnf(s690,plain,
( ~ spl2_23
| ~ spl2_58
| spl2_89 ),
inference(sat_conversion,[],[f5735]) ).
cnf(s691,plain,
( ~ spl2_23
| ~ spl2_66
| spl2_67 ),
inference(sat_conversion,[],[f5736]) ).
cnf(s714,plain,
( spl2_107
| spl2_108 ),
inference(sat_conversion,[],[f5767]) ).
cnf(s721,plain,
( ~ spl2_16
| spl2_79
| spl2_80 ),
inference(sat_conversion,[],[f5802]) ).
cnf(s727,plain,
( spl2_26
| ~ spl2_69 ),
inference(sat_conversion,[],[f5858]) ).
cnf(s737,plain,
( ~ spl2_13
| spl2_64
| spl2_130 ),
inference(sat_conversion,[],[f5874]) ).
cnf(s749,plain,
( ~ spl2_11
| spl2_45
| ~ spl2_87 ),
inference(sat_conversion,[],[f5898]) ).
cnf(s767,plain,
( ~ spl2_54
| spl2_74
| ~ spl2_77 ),
inference(sat_conversion,[],[f5931]) ).
cnf(s794,plain,
( spl2_38
| ~ spl2_50
| ~ spl2_98 ),
inference(sat_conversion,[],[f5967]) ).
cnf(s826,plain,
( ~ spl2_45
| ~ spl2_55
| spl2_110 ),
inference(sat_conversion,[],[f6177]) ).
cnf(s828,plain,
( ~ spl2_95
| spl2_127 ),
inference(sat_conversion,[],[f6182]) ).
cnf(s833,plain,
( spl2_3
| ~ spl2_127
| spl2_164 ),
inference(sat_conversion,[],[f6275]) ).
cnf(s834,plain,
( ~ spl2_45
| spl2_59
| ~ spl2_62 ),
inference(sat_conversion,[],[f6286]) ).
cnf(s837,plain,
( ~ spl2_89
| spl2_91 ),
inference(sat_conversion,[],[f6304]) ).
cnf(s842,plain,
( spl2_55
| ~ spl2_85
| ~ spl2_99 ),
inference(sat_conversion,[],[f6324]) ).
cnf(s849,plain,
( ~ spl2_11
| ~ spl2_17
| ~ spl2_59
| ~ spl2_83 ),
inference(sat_conversion,[],[f6347]) ).
cnf(s851,plain,
( spl2_62
| ~ spl2_87
| ~ spl2_164 ),
inference(sat_conversion,[],[f6353]) ).
cnf(s855,plain,
( spl2_3
| spl2_62
| ~ spl2_87
| ~ spl2_164 ),
inference(sat_conversion,[],[f6363]) ).
cnf(s859,plain,
( spl2_89
| ~ spl2_96
| ~ spl2_127 ),
inference(sat_conversion,[],[f6367]) ).
cnf(s882,plain,
( ~ spl2_44
| spl2_69
| ~ spl2_77 ),
inference(sat_conversion,[],[f6395]) ).
cnf(s900,plain,
( ~ spl2_26
| ~ spl2_31
| spl2_69 ),
inference(sat_conversion,[],[f6430]) ).
cnf(s915,plain,
( spl2_3
| spl2_62
| ~ spl2_63
| ~ spl2_65 ),
inference(sat_conversion,[],[f6468]) ).
cnf(s921,plain,
( ~ spl2_13
| ~ spl2_80
| spl2_126 ),
inference(sat_conversion,[],[f6474]) ).
cnf(s942,plain,
( ~ spl2_14
| spl2_64
| spl2_65 ),
inference(sat_conversion,[],[f6519]) ).
cnf(s943,plain,
( ~ spl2_14
| spl2_86
| spl2_87 ),
inference(sat_conversion,[],[f6520]) ).
cnf(s946,plain,
( ~ spl2_16
| spl2_32
| spl2_33 ),
inference(sat_conversion,[],[f6531]) ).
cnf(s947,plain,
( spl2_50
| ~ spl2_86 ),
inference(sat_conversion,[],[f6547]) ).
cnf(s948,plain,
( ~ spl2_86
| spl2_99
| ~ spl2_100 ),
inference(sat_conversion,[],[f6633]) ).
cnf(s950,plain,
( spl2_6
| ~ spl2_89
| ~ spl2_126 ),
inference(sat_conversion,[],[f6690]) ).
cnf(s957,plain,
( ~ spl2_17
| ~ spl2_38
| ~ spl2_57 ),
inference(sat_conversion,[],[f6907]) ).
cnf(s962,plain,
( spl2_3
| spl2_57
| ~ spl2_89
| ~ spl2_127 ),
inference(sat_conversion,[],[f6928]) ).
cnf(s971,plain,
( ~ spl2_86
| spl2_127 ),
inference(sat_conversion,[],[f6957]) ).
cnf(s974,plain,
( spl2_13
| ~ spl2_64 ),
inference(sat_conversion,[],[f6975]) ).
cnf(s984,plain,
( spl2_47
| ~ spl2_86
| ~ spl2_97 ),
inference(sat_conversion,[],[f7085]) ).
cnf(s1000,plain,
( ~ spl2_44
| spl2_45
| ~ spl2_65 ),
inference(sat_conversion,[],[f7140]) ).
cnf(s1057,plain,
( spl2_3
| ~ spl2_11
| ~ spl2_17
| spl2_27
| ~ spl2_38
| ~ spl2_83
| ~ spl2_91
| ~ spl2_127 ),
inference(sat_conversion,[],[f8264]) ).
cnf(s1083,plain,
( spl2_9
| ~ spl2_96
| ~ spl2_110 ),
inference(sat_conversion,[],[f8393]) ).
cnf(s1084,plain,
spl2_17,
inference(rat,[],[s15,s16]) ).
cnf(s1085,plain,
( ~ spl2_11
| ~ spl2_13
| ~ spl2_15 ),
inference(rat,[],[s14,s16]) ).
cnf(s1086,plain,
( ~ spl2_12
| ~ spl2_14
| ~ spl2_16 ),
inference(rat,[],[s13,s16]) ).
cnf(s1087,plain,
~ spl2_10,
inference(rat,[],[s9,s16]) ).
cnf(s1088,plain,
~ spl2_9,
inference(rat,[],[s8,s16]) ).
cnf(s1089,plain,
~ spl2_8,
inference(rat,[],[s7,s16]) ).
cnf(s1090,plain,
~ spl2_7,
inference(rat,[],[s6,s16]) ).
cnf(s1091,plain,
~ spl2_6,
inference(rat,[],[s5,s16]) ).
cnf(s1092,plain,
~ spl2_5,
inference(rat,[],[s4,s16]) ).
cnf(s1093,plain,
~ spl2_4,
inference(rat,[],[s3,s16]) ).
cnf(s1094,plain,
~ spl2_3,
inference(rat,[],[s2,s16]) ).
cnf(s1095,plain,
~ spl2_2,
inference(rat,[],[s1,s16]) ).
cnf(s1096,plain,
( ~ spl2_61
| ~ spl2_15 ),
inference(rat,[],[s154,s157,s163,s156,s259,s174,s647,s377,s43,s146,s66,s546,s1090,s1084,s1093,s1087,s1095,s1089]) ).
cnf(s1097,plain,
( spl2_13
| spl2_11 ),
inference(rat,[],[s85,s87,s86,s691,s915,s43,s441,s19,s88,s45,s158,s90,s61,s17,s714,s68,s124,s467,s349,s1096,s97,s72,s227,s12,s1000,s1086,s942,s11,s974,s77,s10,s1094,s1093,s1088,s1084]) ).
cnf(s1099,plain,
( ~ spl2_15
| spl2_11 ),
inference(rat,[],[s80,s24,s691,s900,s85,s72,s397,s450,s86,s20,s737,s43,s56,s19,s76,s45,s164,s90,s61,s17,s67,s68,s124,s349,s1096,s10,s1097,s1090,s1088,s1093,s1084,s1094]) ).
cnf(s1100,plain,
( ~ spl2_46
| spl2_11 ),
inference(rat,[],[s53,s19,s24,s690,s31,s362,s61,s382,s721,s837,s629,s94,s370,s131,s17,s51,s624,s45,s647,s1097,s946,s12,s34,s1099,s1092,s1094,s1093,s1084,s1095,s1087]) ).
cnf(s1101,plain,
( ~ spl2_80
| ~ spl2_23
| ~ spl2_13 ),
inference(rat,[],[s690,s950,s362,s921,s1091]) ).
cnf(s1102,plain,
( ~ spl2_23
| spl2_11 ),
inference(rat,[],[s97,s227,s767,s103,s95,s392,s382,s51,s588,s370,s721,s1101,s388,s1097,s12,s1099,s380,s43,s1100,s1095,s1089,s1091,s1093]) ).
cnf(s1103,plain,
spl2_11,
inference(rat,[],[s24,s31,s53,s90,s39,s50,s19,s1102,s946,s12,s34,s1099,s1097,s1092,s1088,s1094,s1084,s1095]) ).
cnf(s1104,plain,
( ~ spl2_23
| ~ spl2_13 ),
inference(rat,[],[s95,s382,s767,s588,s97,s380,s227,s43,s103,s647,s392,s51,s370,s721,s1101,s388,s12,s1085,s1093,s1095,s1084,s1089,s1091,s1103]) ).
cnf(s1105,plain,
~ spl2_13,
inference(rat,[],[s53,s24,s382,s31,s50,s90,s19,s1104,s946,s12,s34,s1085,s1092,s1084,s1094,s1095,s1088,s1103]) ).
cnf(s1106,plain,
~ spl2_64,
inference(rat,[],[s974,s1105]) ).
cnf(s1108,plain,
spl2_14,
inference(rat,[],[s11,s1105]) ).
cnf(s1109,plain,
spl2_65,
inference(rat,[],[s942,s1106,s1108]) ).
cnf(s1110,plain,
( spl2_44
| spl2_47
| spl2_74 ),
inference(rat,[],[s143,s859,s641,s962,s948,s957,s842,s794,s356,s518,s947,s971,s984,s767,s943,s97,s749,s227,s539,s377,s409,s1094,s1084,s1108,s1103]) ).
cnf(s1111,plain,
( spl2_47
| spl2_74 ),
inference(rat,[],[s1057,s794,s356,s250,s947,s984,s943,s855,s833,s828,s143,s632,s1083,s826,s530,s522,s228,s664,s97,s24,s882,s382,s31,s727,s94,s61,s834,s51,s849,s392,s103,s1000,s1110,s1109,s1089,s1095,s1088,s1108,s1103,s1094,s1084]) ).
cnf(s1112,plain,
~ spl2_47,
inference(rat,[],[s349,s1096,s124,s12,s17,s1086,s45,s253,s43,s204,s1084,s1108,s1093,s1089,s1103]) ).
cnf(s1115,plain,
spl2_74,
inference(rat,[],[s1111,s1112]) ).
cnf(s1118,plain,
~ spl2_23,
inference(rat,[],[s388,s1091,s1115]) ).
cnf(s1120,plain,
spl2_22,
inference(rat,[],[s19,s1118]) ).
cnf(s1121,plain,
spl2_58,
inference(rat,[],[s89,s1120]) ).
cnf(s1123,plain,
~ spl2_26,
inference(rat,[],[s90,s1094,s1088,s1120]) ).
cnf(s1125,plain,
~ spl2_40,
inference(rat,[],[s50,s1095,s1094,s1084,s1120]) ).
cnf(s1127,plain,
spl2_57,
inference(rat,[],[s60,s1094,s1121]) ).
cnf(s1128,plain,
~ spl2_69,
inference(rat,[],[s727,s1123]) ).
cnf(s1133,plain,
spl2_41,
inference(rat,[],[s382,s1125]) ).
cnf(s1135,plain,
~ spl2_38,
inference(rat,[],[s957,s1084,s1127]) ).
cnf(s1140,plain,
~ spl2_91,
inference(rat,[],[s131,s1093,s1135]) ).
cnf(s1147,plain,
~ spl2_71,
inference(rat,[],[s525,s1140]) ).
cnf(s1148,plain,
~ spl2_86,
inference(rat,[],[s250,s1140]) ).
cnf(s1153,plain,
~ spl2_62,
inference(rat,[],[s651,s1127,s1147]) ).
cnf(s1154,plain,
spl2_87,
inference(rat,[],[s943,s1108,s1148]) ).
cnf(s1158,plain,
~ spl2_164,
inference(rat,[],[s851,s1153,s1154]) ).
cnf(s1159,plain,
spl2_45,
inference(rat,[],[s749,s1103,s1154]) ).
cnf(s1160,plain,
~ spl2_127,
inference(rat,[],[s833,s1094,s1158]) ).
cnf(s1165,plain,
spl2_44,
inference(rat,[],[s539,s1159]) ).
cnf(s1166,plain,
~ spl2_95,
inference(rat,[],[s828,s1160]) ).
cnf(s1170,plain,
~ spl2_77,
inference(rat,[],[s882,s1128,s1165]) ).
cnf(s1172,plain,
spl2_96,
inference(rat,[],[s143,s1166]) ).
cnf(s1174,plain,
spl2_76,
inference(rat,[],[s97,s1170]) ).
cnf(s1175,plain,
~ spl2_110,
inference(rat,[],[s1083,s1088,s1172]) ).
cnf(s1178,plain,
spl2_54,
inference(rat,[],[s228,s1174]) ).
cnf(s1180,plain,
~ spl2_55,
inference(rat,[],[s826,s1159,s1175]) ).
cnf(s1185,plain,
$false,
inference(rat,[],[s530,s1133,s1180,s1178]) ).
fof(f8394,plain,
$false,
inference(avatar_sat_refutation,[],[s1185]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO169+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 07:21:30 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.73/0.77 % (4080141)Will run a generic schedule for satisfiability detection.
% 1.73/0.77 % (4080147)% WARNING: option uhcvi not known.
% 1.73/0.77 % (4080147)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2036632461:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.73/0.77 % (4080146)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2657058888_2999 on theBenchmark for (2999ds/0Mi)
% 1.73/0.77 % (4080148)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=24170492:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.73/0.77 % (4080149)dis+10_1_sil=32000:sp=arity:random_seed=1495107576:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.73/0.77 % (4080151)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=41322473:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.73/0.77 % (4080150)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2316592843:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.73/0.77 % (4080152)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3697511733:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.73/0.77 % TRYING [1]
% 1.73/0.77 % TRYING [2]
% 1.73/0.77 % TRYING [3]
% 1.73/0.77 % TRYING [4]
% 1.73/0.77 % TRYING [5]
% 1.73/0.77 % TRYING [6]
% 1.73/0.77 % TRYING [7]
% 1.73/0.77 % (4080150)Instruction limit reached!
% 1.73/0.77 % (4080150)------------------------------
% 1.73/0.77 % (4080150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.77 % (4080150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.77 % (4080150)CaDiCaL version: 2.1.3
% 1.73/0.77 % (4080150)Termination reason: Instruction limit
% 1.73/0.77 % (4080150)Termination phase: Saturation
% 1.73/0.77 % (4080150)Time elapsed: 0.063 s
% 1.73/0.77 % (4080150)Peak memory usage: 12 MB
% 1.73/0.77 % (4080150)Instructions burned: 117 (million)
% 1.73/0.77 % (4080149)Instruction limit reached!
% 1.73/0.77 % (4080149)------------------------------
% 1.73/0.77 % (4080149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.77 % (4080149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.77 % (4080149)CaDiCaL version: 2.1.3
% 1.73/0.77 % (4080149)Termination reason: Instruction limit
% 1.73/0.77 % (4080149)Termination phase: Saturation
% 1.73/0.77 % (4080149)Time elapsed: 0.066 s
% 1.73/0.77 % (4080149)Peak memory usage: 12 MB
% 1.73/0.77 % (4080149)Instructions burned: 104 (million)
% 1.73/0.77 % (4080151)Instruction limit reached!
% 1.73/0.77 % (4080151)------------------------------
% 1.73/0.77 % (4080151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.77 % (4080151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.77 % (4080151)CaDiCaL version: 2.1.3
% 1.73/0.77 % (4080151)Termination reason: Instruction limit
% 1.73/0.77 % (4080151)Termination phase: Saturation
% 1.73/0.77 % (4080151)Time elapsed: 0.080 s
% 1.73/0.77 % (4080151)Peak memory usage: 12 MB
% 1.73/0.77 % (4080151)Instructions burned: 136 (million)
% 1.73/0.77 % (4080160)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=71682494:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.73/0.77 % (4080161)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=158977299:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.73/0.77 % TRYING [1]
% 1.73/0.77 % TRYING [2]
% 1.73/0.77 % TRYING [3]
% 1.73/0.77 % TRYING [4]
% 1.73/0.77 % (4080162)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3177392171:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.73/0.77 % (4080152)Instruction limit reached!
% 1.73/0.77 % (4080152)------------------------------
% 1.73/0.77 % (4080152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.77 % (4080152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.77 % (4080152)CaDiCaL version: 2.1.3
% 1.73/0.77 % (4080152)Termination reason: Instruction limit
% 1.73/0.77 % (4080152)Termination phase: Saturation
% 1.73/0.77 % (4080152)Time elapsed: 0.104 s
% 1.73/0.77 % (4080152)Peak memory usage: 13 MB
% 1.73/0.77 % (4080152)Instructions burned: 159 (million)
% 1.73/0.77 % TRYING [8]
% 1.73/0.77 % (4080166)ott-21_1_sil=16000:fs=off:random_seed=854647534:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.73/0.77 % TRYING [5]
% 1.73/0.77 % TRYING [9]
% 1.73/0.77 % (4080161)Instruction limit reached!
% 1.73/0.77 % (4080161)------------------------------
% 1.73/0.77 % (4080161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.77 % (4080161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.77 % (4080161)CaDiCaL version: 2.1.3
% 1.73/0.77 % (4080161)Termination reason: Instruction limit
% 1.73/0.77 % (4080161)Termination phase: Saturation
% 1.73/0.77 % (4080161)Time elapsed: 0.083 s
% 1.73/0.77 % (4080161)Peak memory usage: 12 MB
% 1.73/0.77 % (4080161)Instructions burned: 131 (million)
% 1.73/0.77 % (4080168)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2186066452:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.73/0.77 % (4080166)Instruction limit reached!
% 1.73/0.77 % (4080166)------------------------------
% 1.73/0.77 % (4080166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.77 % (4080166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.77 % (4080166)CaDiCaL version: 2.1.3
% 1.73/0.77 % (4080166)Termination reason: Instruction limit
% 1.73/0.77 % (4080166)Termination phase: Saturation
% 1.73/0.77 % (4080166)Time elapsed: 0.086 s
% 1.73/0.77 % (4080166)Peak memory usage: 12 MB
% 1.73/0.77 % (4080166)Instructions burned: 181 (million)
% 1.73/0.77 % TRYING [10]
% 1.73/0.77 % (4080170)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4217788253:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.73/0.77 % TRYING [1]
% 1.73/0.77 % TRYING [2]
% 1.73/0.77 % TRYING [3]
% 1.73/0.77 % TRYING [4]
% 1.73/0.77 % TRYING [5]
% 1.73/0.77 % TRYING [6]
% 1.73/0.77 % TRYING [11]
% 1.73/0.77 % TRYING [7]
% 1.73/0.77 % (4080162) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4080141-4080162"...
% 1.73/0.77 % (4080162)...printing done.
% 1.73/0.77 % (4080162)Refutation found. Thanks to Tanya!
% 1.73/0.77 % SZS status Theorem for theBenchmark
% 1.73/0.77 % SZS output start Proof for theBenchmark
% See solution above
% 1.73/0.78 % (4080162)------------------------------
% 1.73/0.78 % (4080162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.78 % (4080162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.78 % (4080162)CaDiCaL version: 2.1.3
% 1.73/0.78 % (4080162)Termination reason: Refutation
% 1.73/0.78 % (4080162)Time elapsed: 0.213 s
% 1.73/0.78 % (4080162)Peak memory usage: 15 MB
% 1.73/0.78 % (4080162)Instructions burned: 342 (million)
% 1.73/0.78 % (4080141)Success in time 0.356 s
% 1.73/0.78 % Vampire exiting
%------------------------------------------------------------------------------