%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO012-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:51:11 AM UTC 2026
% Result : Unsatisfiable 1.80s 1.47s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 57
% Syntax : Number of formulae : 372 ( 29 unt; 28 def)
% Number of atoms : 1030 ( 27 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1144 ( 486 ~; 630 |; 0 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 29 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 121 ( 0 sgn 121 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity1) ).
fof(f20,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity2) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity3) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| between(X0,X1,X2)
| between(X1,X2,X0)
| between(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity4) ).
fof(f56,axiom,
! [X0,X1] : between(X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3) ).
fof(f58,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| between(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1) ).
fof(f59,axiom,
! [X0,X1] : between(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2) ).
fof(f60,axiom,
! [X2,X0,X1] :
( ~ between(X1,X0,X2)
| ~ between(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b2) ).
fof(f65,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X2,X3)
| ~ between(X0,X1,X2)
| between(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b5) ).
fof(f67,axiom,
! [X2,X3,X0,X1] :
( ~ between(X1,X2,X3)
| ~ between(X0,X1,X2)
| between(X0,X1,X3)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b7) ).
fof(f68,axiom,
! [X2,X3,X0,X1] :
( ~ between(X1,X3,X2)
| ~ between(X0,X1,X2)
| between(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b8) ).
fof(f69,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X2,X3)
| ~ between(X0,X1,X2)
| between(X0,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b9) ).
fof(f90,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X1,X3)
| ~ between(X0,X1,X2)
| X0 = X1
| between(X0,X2,X3)
| between(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b12) ).
fof(f91,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X1,X3)
| ~ between(X0,X1,X2)
| X0 = X1
| between(X1,X2,X3)
| between(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b13) ).
fof(f92,axiom,
! [X2,X3,X0,X1] :
( ~ between(X3,X1,X2)
| ~ between(X0,X1,X2)
| X1 = X2
| between(X0,X3,X1)
| between(X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7) ).
fof(f93,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X3,X2)
| ~ between(X0,X1,X2)
| between(X0,X1,X3)
| between(X0,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9) ).
fof(f94,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X3,X2)
| ~ between(X0,X1,X2)
| between(X1,X3,X2)
| between(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b14) ).
fof(f95,axiom,
! [X2,X3,X0,X1,X4] :
( ~ between(X1,X3,X4)
| ~ between(X0,X1,X2)
| ~ between(X0,X4,X2)
| between(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8) ).
fof(f97,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2_1) ).
fof(f98,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2_2) ).
fof(f99,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2_3) ).
fof(f100,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| colinear(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_1) ).
fof(f101,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| colinear(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_2) ).
fof(f102,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| colinear(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_3) ).
fof(f107,axiom,
! [X0,X1] : colinear(X0,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c3_2) ).
fof(f111,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_b) ).
fof(f112,axiom,
colinear(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abc_colinear) ).
fof(f113,axiom,
colinear(a,b,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abd_colinear) ).
fof(f114,negated_conjecture,
( ~ colinear(a,c,d)
| ~ colinear(b,c,d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_colinearity) ).
fof(f118,definition,
( spl0_1
<=> colinear(b,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f120,plain,
( ~ colinear(b,c,d)
| spl0_1 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f122,definition,
( spl0_2
<=> colinear(a,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f123,plain,
( colinear(a,c,d)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f124,plain,
( ~ colinear(a,c,d)
| spl0_2 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f125,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f114,f122,f118]) ).
fof(f146,plain,
colinear(d,b,a),
inference(resolution,[],[f100,f113]) ).
fof(f151,plain,
colinear(b,c,a),
inference(resolution,[],[f101,f112]) ).
fof(f157,plain,
colinear(b,a,d),
inference(resolution,[],[f146,f101]) ).
fof(f162,plain,
colinear(a,c,b),
inference(resolution,[],[f102,f112]) ).
fof(f163,plain,
colinear(a,d,b),
inference(resolution,[],[f102,f113]) ).
fof(f279,plain,
( between(a,b,c)
| between(b,c,a)
| between(c,a,b) ),
inference(resolution,[],[f22,f112]) ).
fof(f280,plain,
( between(a,b,d)
| between(b,d,a)
| between(d,a,b) ),
inference(resolution,[],[f22,f113]) ).
fof(f281,plain,
( between(a,c,b)
| between(c,b,a)
| between(b,a,c) ),
inference(resolution,[],[f22,f162]) ).
fof(f282,plain,
( between(a,d,b)
| between(d,b,a)
| between(b,a,d) ),
inference(resolution,[],[f22,f163]) ).
fof(f292,definition,
( spl0_3
<=> between(b,d,a) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f293,plain,
( ~ between(b,d,a)
| spl0_3 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f294,plain,
( between(b,d,a)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f296,definition,
( spl0_4
<=> between(a,b,d) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f298,plain,
( between(a,b,d)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl0_5
<=> between(d,a,b) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f302,plain,
( between(d,a,b)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f305,definition,
( spl0_6
<=> between(a,d,b) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f307,plain,
( between(a,d,b)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f309,definition,
( spl0_7
<=> between(b,a,d) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f311,plain,
( between(b,a,d)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f313,definition,
( spl0_8
<=> between(d,b,a) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f315,plain,
( between(d,b,a)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f318,definition,
( spl0_9
<=> between(b,c,a) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f319,plain,
( ~ between(b,c,a)
| spl0_9 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( between(b,c,a)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f322,definition,
( spl0_10
<=> between(a,b,c) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f324,plain,
( between(a,b,c)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f326,definition,
( spl0_11
<=> between(c,a,b) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f327,plain,
( ~ between(c,a,b)
| spl0_11 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f328,plain,
( between(c,a,b)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f331,definition,
( spl0_12
<=> between(a,c,b) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f333,plain,
( between(a,c,b)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f335,definition,
( spl0_13
<=> between(b,a,c) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f337,plain,
( between(b,a,c)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl0_14
<=> between(c,b,a) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f341,plain,
( between(c,b,a)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f347,plain,
( spl0_7
| spl0_8
| spl0_6 ),
inference(avatar_split_clause,[],[f282,f305,f313,f309]) ).
fof(f348,plain,
( spl0_13
| spl0_14
| spl0_12 ),
inference(avatar_split_clause,[],[f281,f331,f339,f335]) ).
fof(f349,plain,
( spl0_5
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f280,f296,f292,f300]) ).
fof(f350,plain,
( spl0_11
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f279,f322,f318,f326]) ).
fof(f363,plain,
( ! [X0] :
( ~ between(X0,a,d)
| between(X0,a,b)
| a = d )
| ~ spl0_6 ),
inference(resolution,[],[f307,f67]) ).
fof(f371,definition,
( spl0_15
<=> a = d ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f372,plain,
( a != d
| spl0_15 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f373,plain,
( a = d
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f375,definition,
( spl0_16
<=> ! [X0] :
( ~ between(X0,a,d)
| between(X0,a,b) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f376,plain,
( ! [X0] :
( ~ between(X0,a,d)
| between(X0,a,b) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f377,plain,
( spl0_15
| spl0_16
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f363,f305,f375,f371]) ).
fof(f383,definition,
( spl0_18
<=> b = d ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f385,plain,
( b = d
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f395,plain,
( between(d,a,b)
| ~ spl0_7 ),
inference(resolution,[],[f311,f58]) ).
fof(f413,plain,
( spl0_5
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f395,f309,f300]) ).
fof(f429,plain,
( ~ between(b,d,a)
| b = d
| ~ spl0_8 ),
inference(resolution,[],[f315,f60]) ).
fof(f451,plain,
( b = d
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f429,f294]) ).
fof(f454,plain,
( spl0_18
| ~ spl0_3
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f451,f313,f292,f383]) ).
fof(f458,plain,
( ~ colinear(b,c,a)
| spl0_1
| ~ spl0_15 ),
inference(superposition,[],[f120,f373]) ).
fof(f467,plain,
( $false
| spl0_1
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f458,f151]) ).
fof(f468,plain,
( spl0_1
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f467]) ).
fof(f476,plain,
( between(b,d,a)
| ~ spl0_6 ),
inference(resolution,[],[f307,f58]) ).
fof(f479,plain,
( ! [X0] :
( ~ between(a,X0,d)
| between(X0,d,b) )
| ~ spl0_6 ),
inference(resolution,[],[f307,f65]) ).
fof(f482,plain,
( ! [X0] :
( ~ between(X0,a,b)
| between(X0,d,b) )
| ~ spl0_6 ),
inference(resolution,[],[f307,f68]) ).
fof(f487,plain,
( ! [X0] :
( ~ between(a,X0,b)
| between(a,X0,d)
| between(a,d,X0) )
| ~ spl0_6 ),
inference(resolution,[],[f307,f93]) ).
fof(f488,plain,
( ! [X0] :
( ~ between(a,X0,b)
| between(X0,d,b)
| between(d,X0,b) )
| ~ spl0_6 ),
inference(resolution,[],[f307,f94]) ).
fof(f489,plain,
( ! [X0,X1] :
( ~ between(X0,b,X1)
| ~ between(X0,a,X1)
| between(X0,d,X1) )
| ~ spl0_6 ),
inference(resolution,[],[f307,f95]) ).
fof(f517,plain,
( ! [X0] :
( ~ between(a,c,X0)
| a = c
| between(c,X0,b)
| between(c,b,X0) )
| ~ spl0_12 ),
inference(resolution,[],[f333,f91]) ).
fof(f518,plain,
( ! [X0] :
( ~ between(X0,c,b)
| b = c
| between(X0,a,c)
| between(a,X0,c) )
| ~ spl0_12 ),
inference(resolution,[],[f333,f92]) ).
fof(f526,definition,
( spl0_22
<=> b = c ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f527,plain,
( b != c
| spl0_22 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f528,plain,
( b = c
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f530,definition,
( spl0_23
<=> ! [X0] :
( ~ between(X0,c,b)
| between(a,X0,c)
| between(X0,a,c) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f531,plain,
( ! [X0] :
( ~ between(X0,c,b)
| between(a,X0,c)
| between(X0,a,c) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f532,plain,
( spl0_22
| spl0_23
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f518,f331,f530,f526]) ).
fof(f534,definition,
( spl0_24
<=> a = c ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f536,plain,
( a = c
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f538,definition,
( spl0_25
<=> ! [X0] :
( ~ between(a,c,X0)
| between(c,b,X0)
| between(c,X0,b) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f539,plain,
( ! [X0] :
( ~ between(a,c,X0)
| between(c,b,X0)
| between(c,X0,b) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( spl0_24
| spl0_25
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f517,f331,f538,f534]) ).
fof(f565,plain,
( between(c,a,b)
| ~ spl0_13 ),
inference(resolution,[],[f337,f58]) ).
fof(f592,plain,
( spl0_11
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f565,f335,f326]) ).
fof(f600,plain,
( ~ colinear(b,a,d)
| spl0_1
| ~ spl0_24 ),
inference(superposition,[],[f120,f536]) ).
fof(f610,plain,
( $false
| spl0_1
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f600,f157]) ).
fof(f611,plain,
( spl0_1
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f610]) ).
fof(f660,plain,
( ~ colinear(b,c,b)
| spl0_1
| ~ spl0_18 ),
inference(superposition,[],[f120,f385]) ).
fof(f673,plain,
( $false
| spl0_1
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f660,f107]) ).
fof(f674,plain,
( spl0_1
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f673]) ).
fof(f706,plain,
( between(b,a,c)
| ~ spl0_11 ),
inference(resolution,[],[f328,f58]) ).
fof(f752,plain,
( between(c,d,b)
| ~ spl0_6
| ~ spl0_11 ),
inference(resolution,[],[f482,f328]) ).
fof(f801,definition,
( spl0_39
<=> between(d,c,b) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f802,plain,
( between(d,c,b)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f803,plain,
( ~ between(d,c,b)
| spl0_39 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f846,plain,
( between(a,c,b)
| ~ spl0_9 ),
inference(resolution,[],[f320,f58]) ).
fof(f944,plain,
( between(a,c,d)
| between(a,d,c)
| ~ spl0_6
| ~ spl0_12 ),
inference(resolution,[],[f487,f333]) ).
fof(f949,definition,
( spl0_44
<=> between(a,d,c) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f950,plain,
( ~ between(a,d,c)
| spl0_44 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f951,plain,
( between(a,d,c)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f953,definition,
( spl0_45
<=> between(a,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f954,plain,
( ~ between(a,c,d)
| spl0_45 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f955,plain,
( between(a,c,d)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f956,plain,
( spl0_44
| spl0_45
| ~ spl0_6
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f944,f331,f305,f953,f949]) ).
fof(f977,plain,
( colinear(a,c,d)
| ~ spl0_44 ),
inference(resolution,[],[f951,f98]) ).
fof(f979,plain,
( spl0_2
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f977,f949,f122]) ).
fof(f992,plain,
( between(c,d,b)
| between(d,c,b)
| ~ spl0_6
| ~ spl0_12 ),
inference(resolution,[],[f488,f333]) ).
fof(f997,definition,
( spl0_47
<=> between(c,d,b) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f998,plain,
( ~ between(c,d,b)
| spl0_47 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f999,plain,
( between(c,d,b)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f1000,plain,
( spl0_39
| spl0_47
| ~ spl0_6
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f992,f331,f305,f997,f801]) ).
fof(f1004,plain,
( between(c,d,b)
| ~ spl0_6
| ~ spl0_45 ),
inference(resolution,[],[f955,f479]) ).
fof(f1005,plain,
( colinear(a,c,d)
| ~ spl0_45 ),
inference(resolution,[],[f955,f19]) ).
fof(f1008,plain,
( between(d,c,a)
| ~ spl0_45 ),
inference(resolution,[],[f955,f58]) ).
fof(f1034,plain,
( spl0_2
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1005,f953,f122]) ).
fof(f1035,plain,
( spl0_47
| ~ spl0_6
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1004,f953,f305,f997]) ).
fof(f1036,plain,
( between(a,c,d)
| between(c,d,a)
| between(d,a,c)
| ~ spl0_2 ),
inference(resolution,[],[f123,f22]) ).
fof(f1043,plain,
( colinear(b,c,d)
| ~ spl0_47 ),
inference(resolution,[],[f999,f20]) ).
fof(f1069,plain,
( $false
| spl0_1
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f1043,f120]) ).
fof(f1070,plain,
( spl0_1
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[],[f1069]) ).
fof(f1112,plain,
( between(a,d,c)
| between(d,a,c)
| ~ spl0_23
| ~ spl0_39 ),
inference(resolution,[],[f802,f531]) ).
fof(f1130,plain,
( colinear(b,c,d)
| ~ spl0_39 ),
inference(resolution,[],[f802,f97]) ).
fof(f1133,plain,
( $false
| spl0_1
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1130,f120]) ).
fof(f1134,plain,
( spl0_1
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1133]) ).
fof(f1164,plain,
( ~ between(c,a,a)
| between(c,d,a)
| ~ spl0_6
| ~ spl0_14 ),
inference(resolution,[],[f341,f489]) ).
fof(f1194,plain,
( between(c,b,a)
| ~ spl0_10 ),
inference(resolution,[],[f324,f58]) ).
fof(f1280,definition,
( spl0_57
<=> between(d,c,a) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f1281,plain,
( between(d,c,a)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1282,plain,
( ~ between(d,c,a)
| spl0_57 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1284,plain,
( between(c,d,a)
| between(d,a,c)
| ~ spl0_2
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f1036,f954]) ).
fof(f1285,plain,
( between(c,d,a)
| ~ spl0_6
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1164,f56]) ).
fof(f1288,definition,
( spl0_58
<=> between(d,a,c) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f1289,plain,
( ~ between(d,a,c)
| spl0_58 ),
inference(avatar_component_clause,[],[f1288]) ).
fof(f1290,plain,
( between(d,a,c)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f1288]) ).
fof(f1292,definition,
( spl0_59
<=> between(c,d,a) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f1293,plain,
( ~ between(c,d,a)
| spl0_59 ),
inference(avatar_component_clause,[],[f1292]) ).
fof(f1294,plain,
( between(c,d,a)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f1292]) ).
fof(f1295,plain,
( spl0_58
| spl0_59
| ~ spl0_2
| spl0_45 ),
inference(avatar_split_clause,[],[f1284,f953,f122,f1292,f1288]) ).
fof(f1296,plain,
( spl0_59
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1285,f339,f305,f1292]) ).
fof(f1399,plain,
( colinear(a,c,d)
| ~ spl0_59 ),
inference(resolution,[],[f1294,f20]) ).
fof(f1412,plain,
( ! [X0] :
( ~ between(c,X0,a)
| between(c,X0,d)
| between(c,d,X0) )
| ~ spl0_59 ),
inference(resolution,[],[f1294,f93]) ).
fof(f1424,plain,
( between(c,b,d)
| between(c,d,b)
| ~ spl0_14
| ~ spl0_59 ),
inference(resolution,[],[f1412,f341]) ).
fof(f1429,plain,
( between(c,b,d)
| ~ spl0_14
| spl0_47
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f1424,f998]) ).
fof(f1457,plain,
( colinear(b,c,d)
| ~ spl0_14
| spl0_47
| ~ spl0_59 ),
inference(resolution,[],[f1429,f99]) ).
fof(f1458,plain,
( $false
| spl0_1
| ~ spl0_14
| spl0_47
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f1457,f120]) ).
fof(f1459,plain,
( spl0_1
| ~ spl0_14
| spl0_47
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f1458]) ).
fof(f1466,plain,
( spl0_13
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f706,f326,f335]) ).
fof(f1467,plain,
( $false
| ~ spl0_6
| ~ spl0_11
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f752,f998]) ).
fof(f1468,plain,
( ~ spl0_6
| ~ spl0_11
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f1467]) ).
fof(f1472,plain,
( $false
| spl0_2
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f1399,f124]) ).
fof(f1473,plain,
( spl0_2
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f1472]) ).
fof(f1487,plain,
( ! [X0] :
( ~ between(b,X0,a)
| between(X0,a,c) )
| ~ spl0_13 ),
inference(resolution,[],[f337,f65]) ).
fof(f1531,plain,
( between(d,a,c)
| ~ spl0_3
| ~ spl0_13 ),
inference(resolution,[],[f1487,f294]) ).
fof(f1534,plain,
( $false
| ~ spl0_3
| ~ spl0_13
| spl0_58 ),
inference(forward_subsumption_resolution,[],[f1531,f1289]) ).
fof(f1535,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_58 ),
inference(avatar_contradiction_clause,[],[f1534]) ).
fof(f1539,plain,
( colinear(a,c,d)
| ~ spl0_58 ),
inference(resolution,[],[f1290,f21]) ).
fof(f1540,plain,
( between(c,a,d)
| ~ spl0_58 ),
inference(resolution,[],[f1290,f58]) ).
fof(f1562,plain,
( $false
| spl0_2
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1539,f124]) ).
fof(f1563,plain,
( spl0_2
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1562]) ).
fof(f1571,plain,
( $false
| spl0_3
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f476,f293]) ).
fof(f1572,plain,
( spl0_3
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f1571]) ).
fof(f1575,plain,
( spl0_14
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1194,f322,f339]) ).
fof(f1640,plain,
( between(c,a,b)
| ~ spl0_16
| ~ spl0_58 ),
inference(resolution,[],[f1540,f376]) ).
fof(f1666,plain,
( $false
| spl0_11
| ~ spl0_16
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1640,f327]) ).
fof(f1667,plain,
( spl0_11
| ~ spl0_16
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1666]) ).
fof(f1714,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,b,d)
| a = b )
| ~ spl0_7 ),
inference(resolution,[],[f311,f67]) ).
fof(f1715,plain,
( ! [X0] :
( ~ between(X0,b,d)
| between(X0,a,d) )
| ~ spl0_7 ),
inference(resolution,[],[f311,f68]) ).
fof(f1716,plain,
( ! [X0] :
( ~ between(b,X0,a)
| between(b,X0,d) )
| ~ spl0_7 ),
inference(resolution,[],[f311,f69]) ).
fof(f1718,plain,
( ! [X0] :
( ~ between(b,a,X0)
| a = b
| between(a,X0,d)
| between(a,d,X0) )
| ~ spl0_7 ),
inference(resolution,[],[f311,f91]) ).
fof(f1727,plain,
( ! [X0] :
( ~ between(b,a,X0)
| between(a,X0,d)
| between(a,d,X0) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1718,f111]) ).
fof(f1729,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,b,d) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1714,f111]) ).
fof(f1799,plain,
( $false
| ~ spl0_45
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f1008,f1282]) ).
fof(f1800,plain,
( ~ spl0_45
| spl0_57 ),
inference(avatar_contradiction_clause,[],[f1799]) ).
fof(f1816,plain,
( between(b,a,d)
| ~ spl0_5 ),
inference(resolution,[],[f302,f58]) ).
fof(f1823,plain,
( ! [X0] :
( ~ between(d,X0,a)
| between(d,X0,b) )
| ~ spl0_5 ),
inference(resolution,[],[f302,f69]) ).
fof(f1893,plain,
( between(c,b,d)
| ~ spl0_7
| ~ spl0_14 ),
inference(resolution,[],[f1729,f341]) ).
fof(f1894,plain,
( between(c,a,d)
| ~ spl0_7
| ~ spl0_14 ),
inference(resolution,[],[f1893,f1715]) ).
fof(f1914,plain,
( colinear(b,c,d)
| ~ spl0_7
| ~ spl0_14 ),
inference(resolution,[],[f1893,f99]) ).
fof(f1915,plain,
( $false
| spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1914,f120]) ).
fof(f1916,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1915]) ).
fof(f2022,plain,
( between(a,c,d)
| ~ spl0_57 ),
inference(resolution,[],[f1281,f58]) ).
fof(f2036,plain,
( colinear(a,c,d)
| ~ spl0_57 ),
inference(resolution,[],[f1281,f97]) ).
fof(f2049,plain,
( between(c,b,d)
| between(c,d,b)
| ~ spl0_25
| ~ spl0_45 ),
inference(resolution,[],[f539,f955]) ).
fof(f2051,plain,
( between(c,b,d)
| ~ spl0_25
| ~ spl0_45
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f2049,f998]) ).
fof(f2072,plain,
( colinear(b,c,d)
| ~ spl0_25
| ~ spl0_45
| spl0_47 ),
inference(resolution,[],[f2051,f99]) ).
fof(f2073,plain,
( $false
| spl0_1
| ~ spl0_25
| ~ spl0_45
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f2072,f120]) ).
fof(f2074,plain,
( spl0_1
| ~ spl0_25
| ~ spl0_45
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f2073]) ).
fof(f2120,plain,
( between(a,c,d)
| between(a,d,c)
| ~ spl0_7
| ~ spl0_13 ),
inference(resolution,[],[f1727,f337]) ).
fof(f2123,plain,
( between(d,c,b)
| ~ spl0_5
| ~ spl0_57 ),
inference(resolution,[],[f1823,f1281]) ).
fof(f2126,plain,
( $false
| ~ spl0_5
| spl0_39
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f2123,f803]) ).
fof(f2127,plain,
( ~ spl0_5
| spl0_39
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f2126]) ).
fof(f2128,plain,
( between(a,d,c)
| ~ spl0_7
| ~ spl0_13
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f2120,f954]) ).
fof(f2129,plain,
( $false
| ~ spl0_7
| ~ spl0_13
| spl0_44
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f2128,f950]) ).
fof(f2130,plain,
( ~ spl0_7
| ~ spl0_13
| spl0_44
| spl0_45 ),
inference(avatar_contradiction_clause,[],[f2129]) ).
fof(f2148,plain,
( ! [X0,X1] :
( ~ between(X0,c,X1)
| ~ between(X0,a,X1)
| between(X0,d,X1) )
| ~ spl0_59 ),
inference(resolution,[],[f1294,f95]) ).
fof(f2167,plain,
( ! [X0] :
( ~ between(c,a,X0)
| between(c,d,X0) )
| ~ spl0_59 ),
inference(resolution,[],[f2148,f59]) ).
fof(f2173,plain,
( between(c,d,b)
| ~ spl0_11
| ~ spl0_59 ),
inference(resolution,[],[f2167,f328]) ).
fof(f2175,plain,
( $false
| ~ spl0_11
| spl0_47
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f2173,f998]) ).
fof(f2176,plain,
( ~ spl0_11
| spl0_47
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f2175]) ).
fof(f2178,plain,
( spl0_12
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f846,f318,f331]) ).
fof(f2191,plain,
( ! [X0] :
( ~ between(d,a,X0)
| a = d
| between(d,X0,c)
| between(d,c,X0) )
| ~ spl0_58 ),
inference(resolution,[],[f1290,f90]) ).
fof(f2202,plain,
( ! [X0] :
( ~ between(d,a,X0)
| between(d,X0,c)
| between(d,c,X0) )
| spl0_15
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2191,f372]) ).
fof(f2266,plain,
( between(d,b,c)
| between(d,c,b)
| ~ spl0_5
| spl0_15
| ~ spl0_58 ),
inference(resolution,[],[f2202,f302]) ).
fof(f2270,plain,
( between(d,b,c)
| ~ spl0_5
| spl0_15
| spl0_39
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2266,f803]) ).
fof(f2276,plain,
( colinear(b,c,d)
| ~ spl0_5
| spl0_15
| spl0_39
| ~ spl0_58 ),
inference(resolution,[],[f2270,f21]) ).
fof(f2300,plain,
( $false
| spl0_1
| ~ spl0_5
| spl0_15
| spl0_39
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2276,f120]) ).
fof(f2301,plain,
( spl0_1
| ~ spl0_5
| spl0_15
| spl0_39
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f2300]) ).
fof(f2311,plain,
( between(b,c,a)
| ~ spl0_12 ),
inference(resolution,[],[f333,f58]) ).
fof(f2329,plain,
( between(b,c,d)
| ~ spl0_7
| ~ spl0_9 ),
inference(resolution,[],[f320,f1716]) ).
fof(f2340,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,c,a) )
| ~ spl0_9 ),
inference(resolution,[],[f320,f68]) ).
fof(f2358,plain,
( colinear(b,c,d)
| ~ spl0_7
| ~ spl0_9 ),
inference(resolution,[],[f2329,f19]) ).
fof(f2361,plain,
( between(d,c,b)
| ~ spl0_7
| ~ spl0_9 ),
inference(resolution,[],[f2329,f58]) ).
fof(f2385,plain,
( $false
| ~ spl0_7
| ~ spl0_9
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f2361,f803]) ).
fof(f2386,plain,
( ~ spl0_7
| ~ spl0_9
| spl0_39 ),
inference(avatar_contradiction_clause,[],[f2385]) ).
fof(f2387,plain,
( $false
| spl0_1
| ~ spl0_7
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f2358,f120]) ).
fof(f2388,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f2387]) ).
fof(f2402,plain,
( ! [X0] :
( ~ between(X0,b,a)
| a = b
| between(X0,d,b)
| between(d,X0,b) )
| ~ spl0_8 ),
inference(resolution,[],[f315,f92]) ).
fof(f2409,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,d,b)
| between(d,X0,b) )
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f2402,f111]) ).
fof(f2421,plain,
( ! [X0] :
( ~ between(X0,a,b)
| between(X0,a,d)
| a = b )
| ~ spl0_4 ),
inference(resolution,[],[f298,f67]) ).
fof(f2436,plain,
( ! [X0] :
( ~ between(X0,a,b)
| between(X0,a,d) )
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2421,f111]) ).
fof(f2499,plain,
( between(d,c,a)
| ~ spl0_8
| ~ spl0_9 ),
inference(resolution,[],[f2340,f315]) ).
fof(f2500,plain,
( $false
| ~ spl0_8
| ~ spl0_9
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f2499,f1282]) ).
fof(f2501,plain,
( ~ spl0_8
| ~ spl0_9
| spl0_57 ),
inference(avatar_contradiction_clause,[],[f2500]) ).
fof(f2502,plain,
( $false
| spl0_45
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f2022,f954]) ).
fof(f2503,plain,
( spl0_45
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f2502]) ).
fof(f2504,plain,
( $false
| spl0_2
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f2036,f124]) ).
fof(f2505,plain,
( spl0_2
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f2504]) ).
fof(f2622,plain,
( between(c,d,b)
| between(d,c,b)
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f2409,f341]) ).
fof(f2625,plain,
( between(d,c,b)
| ~ spl0_8
| ~ spl0_14
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f2622,f998]) ).
fof(f2653,plain,
( between(c,a,d)
| ~ spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f328,f2436]) ).
fof(f2683,plain,
( between(d,a,c)
| ~ spl0_4
| ~ spl0_11 ),
inference(resolution,[],[f2653,f58]) ).
fof(f2707,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| spl0_58 ),
inference(forward_subsumption_resolution,[],[f2683,f1289]) ).
fof(f2708,plain,
( ~ spl0_4
| ~ spl0_11
| spl0_58 ),
inference(avatar_contradiction_clause,[],[f2707]) ).
fof(f2726,plain,
( ! [X0] :
( ~ between(d,X0,a)
| between(d,X0,c) )
| ~ spl0_58 ),
inference(resolution,[],[f1290,f69]) ).
fof(f2745,plain,
( between(d,b,c)
| ~ spl0_8
| ~ spl0_58 ),
inference(resolution,[],[f2726,f315]) ).
fof(f2750,plain,
( colinear(b,c,d)
| ~ spl0_8
| ~ spl0_58 ),
inference(resolution,[],[f2745,f21]) ).
fof(f2774,plain,
( $false
| spl0_1
| ~ spl0_8
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f2750,f120]) ).
fof(f2775,plain,
( spl0_1
| ~ spl0_8
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f2774]) ).
fof(f2779,plain,
( spl0_7
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1816,f300,f309]) ).
fof(f2784,plain,
( $false
| spl0_9
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f2311,f319]) ).
fof(f2785,plain,
( spl0_9
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f2784]) ).
fof(f2860,plain,
( ! [X0] :
( ~ between(X0,c,b)
| between(X0,c,a)
| b = c )
| ~ spl0_14 ),
inference(resolution,[],[f341,f67]) ).
fof(f2862,plain,
( ! [X0] :
( ~ between(c,X0,b)
| between(c,X0,a) )
| ~ spl0_14 ),
inference(resolution,[],[f341,f69]) ).
fof(f2875,plain,
( ! [X0] :
( ~ between(X0,c,b)
| between(X0,c,a) )
| ~ spl0_14
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f2860,f527]) ).
fof(f2957,plain,
( between(d,a,c)
| ~ spl0_7
| ~ spl0_14 ),
inference(resolution,[],[f1894,f58]) ).
fof(f2973,plain,
( colinear(a,c,d)
| ~ spl0_7
| ~ spl0_14 ),
inference(resolution,[],[f1894,f99]) ).
fof(f2974,plain,
( $false
| spl0_2
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f2973,f124]) ).
fof(f2975,plain,
( spl0_2
| ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f2974]) ).
fof(f2981,plain,
( $false
| ~ spl0_7
| ~ spl0_14
| spl0_58 ),
inference(forward_subsumption_resolution,[],[f2957,f1289]) ).
fof(f2982,plain,
( ~ spl0_7
| ~ spl0_14
| spl0_58 ),
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f2984,plain,
( spl0_39
| ~ spl0_8
| ~ spl0_14
| spl0_47 ),
inference(avatar_split_clause,[],[f2625,f997,f339,f313,f801]) ).
fof(f2985,plain,
( between(d,a,c)
| ~ spl0_23
| ~ spl0_39
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f1112,f950]) ).
fof(f2986,plain,
( $false
| ~ spl0_23
| ~ spl0_39
| spl0_44
| spl0_58 ),
inference(forward_subsumption_resolution,[],[f2985,f1289]) ).
fof(f2987,plain,
( ~ spl0_23
| ~ spl0_39
| spl0_44
| spl0_58 ),
inference(avatar_contradiction_clause,[],[f2986]) ).
fof(f3091,plain,
( between(d,c,a)
| ~ spl0_14
| spl0_22
| ~ spl0_39 ),
inference(resolution,[],[f2875,f802]) ).
fof(f3092,plain,
( $false
| ~ spl0_14
| spl0_22
| ~ spl0_39
| spl0_57 ),
inference(forward_subsumption_resolution,[],[f3091,f1282]) ).
fof(f3093,plain,
( ~ spl0_14
| spl0_22
| ~ spl0_39
| spl0_57 ),
inference(avatar_contradiction_clause,[],[f3092]) ).
fof(f3096,plain,
( ~ colinear(a,b,d)
| spl0_2
| ~ spl0_22 ),
inference(superposition,[],[f124,f528]) ).
fof(f3135,plain,
( $false
| spl0_2
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f3096,f113]) ).
fof(f3136,plain,
( spl0_2
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f3135]) ).
fof(f3142,plain,
( between(c,d,a)
| ~ spl0_14
| ~ spl0_47 ),
inference(resolution,[],[f999,f2862]) ).
fof(f3171,plain,
( $false
| ~ spl0_14
| ~ spl0_47
| spl0_59 ),
inference(forward_subsumption_resolution,[],[f3142,f1293]) ).
fof(f3172,plain,
( ~ spl0_14
| ~ spl0_47
| spl0_59 ),
inference(avatar_contradiction_clause,[],[f3171]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f125]) ).
cnf(s10,plain,
( spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f347]) ).
cnf(s11,plain,
( spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f348]) ).
cnf(s12,plain,
( spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f349]) ).
cnf(s13,plain,
( spl0_9
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f350]) ).
cnf(s14,plain,
( ~ spl0_6
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f377]) ).
cnf(s18,plain,
( spl0_5
| ~ spl0_7 ),
inference(sat_conversion,[],[f413]) ).
cnf(s25,plain,
( ~ spl0_3
| ~ spl0_8
| spl0_18 ),
inference(sat_conversion,[],[f454]) ).
cnf(s27,plain,
( spl0_1
| ~ spl0_15 ),
inference(sat_conversion,[],[f468]) ).
cnf(s29,plain,
( ~ spl0_12
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f532]) ).
cnf(s30,plain,
( ~ spl0_12
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f540]) ).
cnf(s37,plain,
( spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f592]) ).
cnf(s41,plain,
( spl0_1
| ~ spl0_24 ),
inference(sat_conversion,[],[f611]) ).
cnf(s47,plain,
( spl0_1
| ~ spl0_18 ),
inference(sat_conversion,[],[f674]) ).
cnf(s62,plain,
( ~ spl0_6
| ~ spl0_12
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f956]) ).
cnf(s63,plain,
( spl0_2
| ~ spl0_44 ),
inference(sat_conversion,[],[f979]) ).
cnf(s67,plain,
( ~ spl0_6
| ~ spl0_12
| spl0_39
| spl0_47 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s69,plain,
( spl0_2
| ~ spl0_45 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s70,plain,
( ~ spl0_6
| ~ spl0_45
| spl0_47 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s75,plain,
( spl0_1
| ~ spl0_47 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s77,plain,
( spl0_1
| ~ spl0_39 ),
inference(sat_conversion,[],[f1134]) ).
cnf(s91,plain,
( ~ spl0_2
| spl0_45
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s92,plain,
( ~ spl0_6
| ~ spl0_14
| spl0_59 ),
inference(sat_conversion,[],[f1296]) ).
cnf(s105,plain,
( spl0_1
| ~ spl0_14
| spl0_47
| ~ spl0_59 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s107,plain,
( ~ spl0_11
| spl0_13 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s108,plain,
( ~ spl0_6
| ~ spl0_11
| spl0_47 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s110,plain,
( spl0_2
| ~ spl0_59 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s111,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_58 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s112,plain,
( spl0_2
| ~ spl0_58 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s116,plain,
( spl0_3
| ~ spl0_6 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s118,plain,
( ~ spl0_10
| spl0_14 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s120,plain,
( spl0_11
| ~ spl0_16
| ~ spl0_58 ),
inference(sat_conversion,[],[f1667]) ).
cnf(s122,plain,
( ~ spl0_45
| spl0_57 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s126,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s134,plain,
( spl0_1
| ~ spl0_25
| ~ spl0_45
| spl0_47 ),
inference(sat_conversion,[],[f2074]) ).
cnf(s140,plain,
( ~ spl0_5
| spl0_39
| ~ spl0_57 ),
inference(sat_conversion,[],[f2127]) ).
cnf(s141,plain,
( ~ spl0_7
| ~ spl0_13
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s144,plain,
( ~ spl0_11
| spl0_47
| ~ spl0_59 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s145,plain,
( ~ spl0_9
| spl0_12 ),
inference(sat_conversion,[],[f2178]) ).
cnf(s147,plain,
( spl0_1
| ~ spl0_5
| spl0_15
| spl0_39
| ~ spl0_58 ),
inference(sat_conversion,[],[f2301]) ).
cnf(s150,plain,
( ~ spl0_7
| ~ spl0_9
| spl0_39 ),
inference(sat_conversion,[],[f2386]) ).
cnf(s151,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_9 ),
inference(sat_conversion,[],[f2388]) ).
cnf(s155,plain,
( ~ spl0_8
| ~ spl0_9
| spl0_57 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s156,plain,
( spl0_45
| ~ spl0_57 ),
inference(sat_conversion,[],[f2503]) ).
cnf(s157,plain,
( spl0_2
| ~ spl0_57 ),
inference(sat_conversion,[],[f2505]) ).
cnf(s169,plain,
( ~ spl0_4
| ~ spl0_11
| spl0_58 ),
inference(sat_conversion,[],[f2708]) ).
cnf(s171,plain,
( spl0_1
| ~ spl0_8
| ~ spl0_58 ),
inference(sat_conversion,[],[f2775]) ).
cnf(s172,plain,
( ~ spl0_5
| spl0_7 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s178,plain,
( spl0_9
| ~ spl0_12 ),
inference(sat_conversion,[],[f2785]) ).
cnf(s181,plain,
( spl0_2
| ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s182,plain,
( ~ spl0_7
| ~ spl0_14
| spl0_58 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s184,plain,
( ~ spl0_8
| ~ spl0_14
| spl0_39
| spl0_47 ),
inference(sat_conversion,[],[f2984]) ).
cnf(s185,plain,
( ~ spl0_23
| ~ spl0_39
| spl0_44
| spl0_58 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s186,plain,
( ~ spl0_14
| spl0_22
| ~ spl0_39
| spl0_57 ),
inference(sat_conversion,[],[f3093]) ).
cnf(s191,plain,
( spl0_2
| ~ spl0_22 ),
inference(sat_conversion,[],[f3136]) ).
cnf(s193,plain,
( ~ spl0_14
| ~ spl0_47
| spl0_59 ),
inference(sat_conversion,[],[f3172]) ).
cnf(s194,plain,
( ~ spl0_7
| spl0_2
| spl0_1 ),
inference(rat,[],[s107,s13,s118,s141,s151,s182,s112,s69,s63]) ).
cnf(s195,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s13,s118,s169,s184,s155,s12,s10,s116,s77,s75,s157,s112,s172,s194]) ).
cnf(s196,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s11,s67,s92,s10,s25,s111,s195,s194,s110,s112,s77,s75,s47]) ).
cnf(s197,plain,
( ~ spl0_7
| spl0_1 ),
inference(rat,[],[s91,s144,s122,s13,s140,s147,s118,s18,s126,s151,s77,s75,s27,s196]) ).
cnf(s198,plain,
( spl0_3
| spl0_1 ),
inference(rat,[],[s134,s156,s30,s155,s11,s13,s37,s118,s169,s184,s171,s12,s10,s116,s77,s75,s41,s172,s197]) ).
cnf(s199,plain,
spl0_1,
inference(rat,[],[s105,s91,s11,s120,s37,s14,s67,s70,s108,s10,s25,s198,s197,s196,s27,s47,s75,s77]) ).
cnf(s200,plain,
~ spl0_2,
inference(rat,[],[s1,s199]) ).
cnf(s201,plain,
~ spl0_22,
inference(rat,[],[s191,s200]) ).
cnf(s202,plain,
~ spl0_57,
inference(rat,[],[s157,s200]) ).
cnf(s203,plain,
~ spl0_58,
inference(rat,[],[s112,s200]) ).
cnf(s204,plain,
~ spl0_59,
inference(rat,[],[s110,s200]) ).
cnf(s205,plain,
~ spl0_45,
inference(rat,[],[s69,s200]) ).
cnf(s206,plain,
~ spl0_44,
inference(rat,[],[s63,s200]) ).
cnf(s208,plain,
~ spl0_7,
inference(rat,[],[s185,s150,s29,s13,s11,s107,s118,s141,s181,s206,s203,s201,s205,s200]) ).
cnf(s209,plain,
~ spl0_5,
inference(rat,[],[s172,s208]) ).
cnf(s211,plain,
( spl0_9
| spl0_14 ),
inference(rat,[],[s12,s111,s169,s11,s13,s178,s118,s209,s203]) ).
cnf(s212,plain,
~ spl0_9,
inference(rat,[],[s62,s10,s145,s155,s206,s205,s208,s202]) ).
cnf(s215,plain,
spl0_14,
inference(rat,[],[s211,s212]) ).
cnf(s218,plain,
~ spl0_47,
inference(rat,[],[s193,s204,s215]) ).
cnf(s219,plain,
~ spl0_39,
inference(rat,[],[s186,s202,s201,s215]) ).
cnf(s220,plain,
~ spl0_8,
inference(rat,[],[s184,s218,s219,s215]) ).
cnf(s221,plain,
~ spl0_6,
inference(rat,[],[s92,s204,s215]) ).
cnf(s226,plain,
$false,
inference(rat,[],[s10,s208,s221,s220]) ).
fof(f3173,plain,
$false,
inference(avatar_sat_refutation,[],[s226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO012-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 % Computer : n019.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 27 06:35:03 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.45 Running first-order theorem proving
% 0.14/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.80/1.46 % (2744378)Input is clausal, will run a generic CNF schedule.
% 1.80/1.46 % (2744388)lrs+10_1_sil=8000:sp=occurrence:random_seed=1515826790:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 1.80/1.46 % (2744390)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2857030925:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 1.80/1.46 % (2744388)First to succeed.
% 1.80/1.46 % (2744388)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2744378"
% 1.80/1.46 % (2744385)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1321403882:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 1.80/1.46 % (2744386)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=271644567:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 1.80/1.46 % (2744387)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3369018565:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 1.80/1.46 % (2744391)dis-21_1_sil=8000:lcm=predicate:random_seed=3568649369:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 1.80/1.46 % (2744389)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=398152327:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 1.80/1.46 % (2744390)Instruction limit reached!
% 1.80/1.46 % (2744390)------------------------------
% 1.80/1.46 % (2744390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.80/1.46 % (2744390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/1.46 % (2744390)CaDiCaL version: 2.1.3
% 1.80/1.46 % (2744390)Termination reason: Instruction limit
% 1.80/1.46 % (2744390)Termination phase: Saturation
% 1.80/1.46 % (2744390)Time elapsed: 0.140 s
% 1.80/1.46 % (2744390)Peak memory usage: 90 MB
% 1.80/1.46 % (2744390)Instructions burned: 180 (million)
% 1.80/1.46 % (2744391)Instruction limit reached!
% 1.80/1.46 % (2744391)------------------------------
% 1.80/1.46 % (2744391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.80/1.47 % (2744391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/1.47 % (2744391)CaDiCaL version: 2.1.3
% 1.80/1.47 % (2744391)Termination reason: Instruction limit
% 1.80/1.47 % (2744391)Termination phase: Saturation
% 1.80/1.47 % (2744391)Time elapsed: 0.107 s
% 1.80/1.47 % (2744391)Peak memory usage: 89 MB
% 1.80/1.47 % (2744391)Instructions burned: 117 (million)
% 1.80/1.47 % (2744389)Instruction limit reached!
% 1.80/1.47 % (2744389)------------------------------
% 1.80/1.47 % (2744389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.80/1.47 % (2744389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.80/1.47 % (2744389)CaDiCaL version: 2.1.3
% 1.80/1.47 % (2744389)Termination reason: Instruction limit
% 1.80/1.47 % (2744389)Termination phase: Saturation
% 1.80/1.47 % (2744389)Time elapsed: 0.108 s
% 1.80/1.47 % (2744389)Peak memory usage: 88 MB
% 1.80/1.47 % (2744389)Instructions burned: 114 (million)
% 1.80/1.47 % (2744388)Refutation found. Thanks to Tanya!
% 1.80/1.47 % SZS status Unsatisfiable for theBenchmark
% 1.80/1.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/1.71 % (2744388)------------------------------
% 0.21/1.71 % (2744388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/1.71 % (2744388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/1.71 % (2744388)CaDiCaL version: 2.1.3
% 0.21/1.71 % (2744388)Termination reason: Refutation
% 0.21/1.71 % (2744388)Time elapsed: 0.053 s
% 0.21/1.71 % (2744388)Peak memory usage: 90 MB
% 0.21/1.71 % (2744388)Instructions burned: 97 (million)
% 0.21/1.71 % (2744388)------------------------------
% 0.21/1.71 % (2744388)------------------------------
% 0.21/1.71 % (2744378)Success in time 0.461 s
% 0.21/1.71 % Vampire exiting
%------------------------------------------------------------------------------