%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n014.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:16 AM UTC 2026
% Result : Unsatisfiable 151.99s 41.18s
% Output : Refutation 151.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 61
% Syntax : Number of formulae : 391 ( 29 unt; 27 def)
% Number of atoms : 1067 ( 54 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1171 ( 495 ~; 649 |; 0 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 28 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-5 aty)
% Number of variables : 202 ( 0 sgn 202 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction1) ).
fof(f7,axiom,
! [X0,X1] :
( ~ between(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',identity_for_betweeness) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4] :
( ~ between(X3,X4,X2)
| ~ between(X0,X1,X2)
| between(X1,inner_pasch(X0,X1,X2,X4,X3),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',inner_pasch1) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4] :
( ~ between(X3,X4,X2)
| ~ between(X0,X1,X2)
| between(X4,inner_pasch(X0,X1,X2,X4,X3),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',inner_pasch2) ).
fof(f19,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-1.ax',colinearity1) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| colinear(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-1.ax',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/Axioms/GEO002-1.ax',colinearity4) ).
fof(f34,axiom,
! [X2,X0,X1] : X0 = extension(X1,X0,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e1) ).
fof(f35,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(reorient_equations,[],[f34]) ).
fof(f49,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| X0 = X1
| X2 = extension(X0,X1,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_1) ).
fof(f50,plain,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| X0 = X1
| extension(X0,X1,X1,X2) = X2 ),
inference(reorient_equations,[],[f49]) ).
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(f61,axiom,
! [X2,X0,X1] :
( ~ between(X0,X2,X1)
| ~ between(X0,X1,X2)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b3) ).
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(f66,axiom,
! [X2,X3,X0,X1] :
( ~ between(X1,X2,X3)
| ~ between(X0,X1,X2)
| between(X0,X2,X3)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b6) ).
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(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(X0,X4,X2)
| ~ between(X1,X3,X4)
| ~ between(X0,X1,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(f103,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| colinear(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_4) ).
fof(f104,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| colinear(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_5) ).
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(f132,definition,
( spl0_1
<=> colinear(b,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f133,plain,
( colinear(b,c,d)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f134,plain,
( ~ colinear(b,c,d)
| spl0_1 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f136,definition,
( spl0_2
<=> colinear(a,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f137,plain,
( colinear(a,c,d)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f138,plain,
( ~ colinear(a,c,d)
| spl0_2 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f139,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f114,f136,f132]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : between(extension(X0,X1,X2,X3),X1,X0),
inference(resolution,[],[f58,f4]) ).
fof(f168,plain,
colinear(d,b,a),
inference(resolution,[],[f100,f113]) ).
fof(f177,plain,
colinear(b,c,a),
inference(resolution,[],[f101,f112]) ).
fof(f180,plain,
colinear(b,a,d),
inference(resolution,[],[f101,f168]) ).
fof(f182,plain,
colinear(a,c,b),
inference(resolution,[],[f177,f100]) ).
fof(f383,plain,
! [X2,X3,X0,X1] :
( ~ between(X0,extension(X0,X1,X2,X3),X1)
| extension(X0,X1,X2,X3) = X1 ),
inference(resolution,[],[f61,f4]) ).
fof(f387,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| between(X1,X2,extension(X0,X2,X3,X4)) ),
inference(resolution,[],[f65,f4]) ).
fof(f1099,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| between(X0,X1,extension(X1,X2,X3,X4))
| X1 = X2 ),
inference(resolution,[],[f67,f4]) ).
fof(f1608,plain,
( between(a,b,c)
| between(b,c,a)
| between(c,a,b) ),
inference(resolution,[],[f22,f112]) ).
fof(f1609,plain,
( between(a,b,d)
| between(b,d,a)
| between(d,a,b) ),
inference(resolution,[],[f22,f113]) ).
fof(f1621,definition,
( spl0_3
<=> between(c,a,b) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1623,plain,
( between(c,a,b)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f1621]) ).
fof(f1625,definition,
( spl0_4
<=> between(b,c,a) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f1627,plain,
( between(b,c,a)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1629,definition,
( spl0_5
<=> between(a,b,c) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1631,plain,
( between(a,b,c)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1629]) ).
fof(f1632,plain,
( spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f1608,f1629,f1625,f1621]) ).
fof(f1636,plain,
( a = c
| b = extension(c,a,a,b)
| ~ spl0_3 ),
inference(resolution,[],[f1623,f50]) ).
fof(f1637,plain,
( between(b,a,c)
| ~ spl0_3 ),
inference(resolution,[],[f1623,f58]) ).
fof(f1676,definition,
( spl0_6
<=> a = c ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f1677,plain,
( a != c
| spl0_6 ),
inference(avatar_component_clause,[],[f1676]) ).
fof(f1678,plain,
( a = c
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f1676]) ).
fof(f1680,definition,
( spl0_7
<=> between(a,c,b) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f1681,plain,
( between(a,c,b)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f1680]) ).
fof(f1682,plain,
( ~ between(a,c,b)
| spl0_7 ),
inference(avatar_component_clause,[],[f1680]) ).
fof(f2063,plain,
! [X2,X3,X0,X1] :
( ~ between(X2,X0,X3)
| ~ between(X0,X1,X2)
| between(X2,X1,X3) ),
inference(resolution,[],[f95,f59]) ).
fof(f2182,plain,
! [X2,X3,X0,X1] :
( ~ between(X0,X1,X2)
| between(X1,inner_pasch(X0,X1,X2,X2,X3),X3) ),
inference(resolution,[],[f8,f56]) ).
fof(f2267,plain,
! [X2,X3,X0,X1] :
( ~ between(X0,X1,X2)
| between(X2,inner_pasch(X0,X1,X2,X2,X3),X0) ),
inference(resolution,[],[f9,f56]) ).
fof(f2631,definition,
( spl0_8
<=> b = extension(c,a,a,b) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f2633,plain,
( b = extension(c,a,a,b)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2634,plain,
( spl0_8
| spl0_6
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f1636,f1621,f1676,f2631]) ).
fof(f2636,plain,
( ~ colinear(b,a,d)
| spl0_1
| ~ spl0_6 ),
inference(superposition,[],[f134,f1678]) ).
fof(f2709,plain,
( $false
| spl0_1
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2636,f180]) ).
fof(f2710,plain,
( spl0_1
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f2709]) ).
fof(f2726,plain,
( between(c,b,a)
| ~ spl0_5 ),
inference(resolution,[],[f1631,f58]) ).
fof(f4046,plain,
( between(a,c,b)
| ~ spl0_4 ),
inference(resolution,[],[f1627,f58]) ).
fof(f4068,plain,
( $false
| ~ spl0_4
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f4046,f1682]) ).
fof(f4069,plain,
( ~ spl0_4
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f4068]) ).
fof(f4085,plain,
( ! [X0] :
( ~ between(X0,a,b)
| between(X0,c,b) )
| ~ spl0_7 ),
inference(resolution,[],[f1681,f68]) ).
fof(f4105,definition,
( spl0_11
<=> between(c,b,a) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f4106,plain,
( between(c,b,a)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f4105]) ).
fof(f4926,definition,
( spl0_12
<=> between(d,a,b) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f4928,plain,
( between(d,a,b)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f4926]) ).
fof(f4930,definition,
( spl0_13
<=> between(b,d,a) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f4932,plain,
( between(b,d,a)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f4930]) ).
fof(f4934,definition,
( spl0_14
<=> between(a,b,d) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f4936,plain,
( between(a,b,d)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f4934]) ).
fof(f4937,plain,
( spl0_12
| spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f1609,f4934,f4930,f4926]) ).
fof(f4938,plain,
( between(d,c,b)
| ~ spl0_7
| ~ spl0_12 ),
inference(resolution,[],[f4928,f4085]) ).
fof(f4948,plain,
( between(b,a,d)
| ~ spl0_12 ),
inference(resolution,[],[f4928,f58]) ).
fof(f5017,plain,
( between(b,c,d)
| ~ spl0_7
| ~ spl0_12 ),
inference(resolution,[],[f4938,f58]) ).
fof(f5089,plain,
( ! [X0] :
( ~ between(b,X0,a)
| between(X0,a,c) )
| ~ spl0_3 ),
inference(resolution,[],[f1637,f65]) ).
fof(f5090,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,a,c)
| a = b )
| ~ spl0_3 ),
inference(resolution,[],[f1637,f66]) ).
fof(f5091,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,b,c)
| a = b )
| ~ spl0_3 ),
inference(resolution,[],[f1637,f67]) ).
fof(f5093,plain,
( ! [X0] :
( ~ between(b,X0,a)
| between(b,X0,c) )
| ~ spl0_3 ),
inference(resolution,[],[f1637,f69]) ).
fof(f5110,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,b,c) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f5091,f111]) ).
fof(f5111,plain,
( ! [X0] :
( ~ between(X0,b,a)
| between(X0,a,c) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f5090,f111]) ).
fof(f5183,definition,
( spl0_15
<=> a = d ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f5184,plain,
( a != d
| spl0_15 ),
inference(avatar_component_clause,[],[f5183]) ).
fof(f5185,plain,
( a = d
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f5183]) ).
fof(f5187,definition,
( spl0_16
<=> between(a,d,b) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f5188,plain,
( between(a,d,b)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f5187]) ).
fof(f5189,plain,
( ~ between(a,d,b)
| spl0_16 ),
inference(avatar_component_clause,[],[f5187]) ).
fof(f7472,plain,
! [X2,X3,X0,X1,X4,X5] :
( between(extension(X0,X1,X2,X3),X1,extension(X1,X0,X4,X5))
| X0 = X1 ),
inference(resolution,[],[f1099,f157]) ).
fof(f30777,plain,
( between(b,d,c)
| ~ spl0_3
| ~ spl0_13 ),
inference(resolution,[],[f4932,f5093]) ).
fof(f30788,plain,
( between(a,d,b)
| ~ spl0_13 ),
inference(resolution,[],[f4932,f58]) ).
fof(f30833,plain,
( $false
| ~ spl0_13
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f30788,f5189]) ).
fof(f30834,plain,
( ~ spl0_13
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f30833]) ).
fof(f30844,plain,
( between(d,b,a)
| ~ spl0_14 ),
inference(resolution,[],[f4936,f58]) ).
fof(f30906,plain,
( between(d,a,c)
| ~ spl0_3
| ~ spl0_14 ),
inference(resolution,[],[f30844,f5111]) ).
fof(f30907,plain,
( between(d,b,c)
| ~ spl0_3
| ~ spl0_14 ),
inference(resolution,[],[f30844,f5110]) ).
fof(f30977,plain,
( colinear(a,c,d)
| ~ spl0_3
| ~ spl0_14 ),
inference(resolution,[],[f30906,f21]) ).
fof(f31041,plain,
( colinear(b,c,d)
| ~ spl0_3
| ~ spl0_14 ),
inference(resolution,[],[f30907,f21]) ).
fof(f31093,plain,
( $false
| spl0_1
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f31041,f134]) ).
fof(f31094,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f31093]) ).
fof(f31136,definition,
( spl0_19
<=> between(b,d,c) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f31137,plain,
( ~ between(b,d,c)
| spl0_19 ),
inference(avatar_component_clause,[],[f31136]) ).
fof(f31138,plain,
( between(b,d,c)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f31136]) ).
fof(f31140,definition,
( spl0_20
<=> between(c,b,d) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f31141,plain,
( ~ between(c,b,d)
| spl0_20 ),
inference(avatar_component_clause,[],[f31140]) ).
fof(f31142,plain,
( between(c,b,d)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f31140]) ).
fof(f31145,plain,
( ~ colinear(b,c,a)
| spl0_1
| ~ spl0_15 ),
inference(superposition,[],[f134,f5185]) ).
fof(f31160,plain,
( $false
| spl0_1
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f31145,f177]) ).
fof(f31161,plain,
( spl0_1
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f31160]) ).
fof(f31163,plain,
( between(d,a,c)
| ~ spl0_3
| ~ spl0_13 ),
inference(resolution,[],[f4932,f5089]) ).
fof(f31293,plain,
( spl0_19
| ~ spl0_3
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f30777,f4930,f1621,f31136]) ).
fof(f39192,definition,
( spl0_22
<=> between(d,c,a) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f39196,plain,
( $false
| spl0_2
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f30977,f138]) ).
fof(f39197,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f39196]) ).
fof(f39206,plain,
( between(b,c,d)
| between(c,d,b)
| between(d,b,c)
| ~ spl0_1 ),
inference(resolution,[],[f133,f22]) ).
fof(f39357,definition,
( spl0_23
<=> between(d,b,c) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f39358,plain,
( ~ between(d,b,c)
| spl0_23 ),
inference(avatar_component_clause,[],[f39357]) ).
fof(f39359,plain,
( between(d,b,c)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f39357]) ).
fof(f39361,definition,
( spl0_24
<=> between(c,d,b) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f39362,plain,
( ~ between(c,d,b)
| spl0_24 ),
inference(avatar_component_clause,[],[f39361]) ).
fof(f39363,plain,
( between(c,d,b)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f39361]) ).
fof(f39365,definition,
( spl0_25
<=> between(b,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f39366,plain,
( ~ between(b,c,d)
| spl0_25 ),
inference(avatar_component_clause,[],[f39365]) ).
fof(f39367,plain,
( between(b,c,d)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f39365]) ).
fof(f39368,plain,
( spl0_23
| spl0_24
| spl0_25
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f39206,f132,f39365,f39361,f39357]) ).
fof(f39424,plain,
( between(b,d,c)
| ~ spl0_24 ),
inference(resolution,[],[f39363,f58]) ).
fof(f43490,plain,
( ! [X0,X1] :
( ~ between(X0,X1,d)
| between(X1,inner_pasch(X0,X1,d,c,b),b) )
| ~ spl0_25 ),
inference(resolution,[],[f39367,f8]) ).
fof(f43491,plain,
( ! [X0,X1] :
( ~ between(X0,X1,d)
| between(c,inner_pasch(X0,X1,d,c,b),X0) )
| ~ spl0_25 ),
inference(resolution,[],[f39367,f9]) ).
fof(f43505,plain,
( ! [X0] :
( ~ between(X0,b,d)
| between(X0,c,d) )
| ~ spl0_25 ),
inference(resolution,[],[f39367,f68]) ).
fof(f52194,plain,
( ! [X0] : between(d,inner_pasch(X0,d,d,c,b),b)
| ~ spl0_25 ),
inference(resolution,[],[f43490,f56]) ).
fof(f52278,plain,
( ! [X0] : colinear(b,inner_pasch(X0,d,d,c,b),d)
| ~ spl0_25 ),
inference(resolution,[],[f52194,f97]) ).
fof(f52569,plain,
( ! [X0] : between(c,inner_pasch(X0,d,d,c,b),X0)
| ~ spl0_25 ),
inference(resolution,[],[f43491,f56]) ).
fof(f52636,plain,
( c = inner_pasch(c,d,d,c,b)
| ~ spl0_25 ),
inference(resolution,[],[f52569,f7]) ).
fof(f55724,plain,
( colinear(b,c,d)
| ~ spl0_25 ),
inference(superposition,[],[f52278,f52636]) ).
fof(f57284,plain,
( spl0_11
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f2726,f1629,f4105]) ).
fof(f59704,definition,
( spl0_45
<=> b = d ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f59705,plain,
( b != d
| spl0_45 ),
inference(avatar_component_clause,[],[f59704]) ).
fof(f59706,plain,
( b = d
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f59704]) ).
fof(f60952,plain,
( between(a,c,d)
| ~ spl0_14
| ~ spl0_25 ),
inference(resolution,[],[f4936,f43505]) ).
fof(f61043,plain,
( colinear(a,c,d)
| ~ spl0_14
| ~ spl0_25 ),
inference(resolution,[],[f60952,f19]) ).
fof(f61113,plain,
( $false
| spl0_2
| ~ spl0_14
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f61043,f138]) ).
fof(f61114,plain,
( spl0_2
| ~ spl0_14
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f61113]) ).
fof(f61286,plain,
( ! [X0] :
( ~ between(X0,d,b)
| between(X0,d,c)
| b = d )
| ~ spl0_23 ),
inference(resolution,[],[f39359,f67]) ).
fof(f61305,plain,
( ! [X0] : between(b,inner_pasch(d,b,c,c,X0),X0)
| ~ spl0_23 ),
inference(resolution,[],[f39359,f2182]) ).
fof(f61307,plain,
( ! [X0] : between(c,inner_pasch(d,b,c,c,X0),d)
| ~ spl0_23 ),
inference(resolution,[],[f39359,f2267]) ).
fof(f61364,plain,
( ! [X0] : between(b,inner_pasch(c,b,d,d,X0),X0)
| ~ spl0_20 ),
inference(resolution,[],[f31142,f2182]) ).
fof(f61366,plain,
( ! [X0] : between(d,inner_pasch(c,b,d,d,X0),c)
| ~ spl0_20 ),
inference(resolution,[],[f31142,f2267]) ).
fof(f61392,plain,
( $false
| spl0_19
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f39424,f31137]) ).
fof(f61393,plain,
( spl0_19
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f61392]) ).
fof(f61409,plain,
( ! [X0] :
( ~ between(X0,b,c)
| between(X0,d,c) )
| ~ spl0_19 ),
inference(resolution,[],[f31138,f68]) ).
fof(f62689,plain,
( between(a,d,c)
| ~ spl0_5
| ~ spl0_19 ),
inference(resolution,[],[f61409,f1631]) ).
fof(f62718,plain,
( colinear(a,c,d)
| ~ spl0_5
| ~ spl0_19 ),
inference(resolution,[],[f62689,f98]) ).
fof(f62760,plain,
( $false
| spl0_2
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f62718,f138]) ).
fof(f62761,plain,
( spl0_2
| ~ spl0_5
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f62760]) ).
fof(f62968,plain,
( b = inner_pasch(d,b,c,c,b)
| ~ spl0_23 ),
inference(resolution,[],[f61305,f7]) ).
fof(f63507,plain,
( ! [X0] : colinear(inner_pasch(d,b,c,c,X0),c,d)
| ~ spl0_23 ),
inference(resolution,[],[f61307,f99]) ).
fof(f63617,plain,
( b = inner_pasch(c,b,d,d,b)
| ~ spl0_20 ),
inference(resolution,[],[f61364,f7]) ).
fof(f63772,plain,
( ! [X0] : colinear(inner_pasch(c,b,d,d,X0),c,d)
| ~ spl0_20 ),
inference(resolution,[],[f61366,f21]) ).
fof(f64420,definition,
( spl0_49
<=> ! [X0] :
( ~ between(X0,d,b)
| between(X0,d,c) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f64421,plain,
( ! [X0] :
( ~ between(X0,d,b)
| between(X0,d,c) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f64420]) ).
fof(f64422,plain,
( spl0_45
| spl0_49
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f61286,f39357,f64420,f59704]) ).
fof(f65536,plain,
( colinear(b,c,d)
| ~ spl0_23 ),
inference(superposition,[],[f63507,f62968]) ).
fof(f68238,plain,
( colinear(b,c,d)
| ~ spl0_20 ),
inference(superposition,[],[f63772,f63617]) ).
fof(f73360,plain,
( ~ colinear(a,c,b)
| spl0_2
| ~ spl0_45 ),
inference(superposition,[],[f138,f59706]) ).
fof(f73980,plain,
( $false
| spl0_2
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f73360,f182]) ).
fof(f73981,plain,
( spl0_2
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f73980]) ).
fof(f74340,plain,
( ! [X0] :
( ~ between(b,X0,a)
| between(b,X0,c)
| between(b,c,X0) )
| ~ spl0_4 ),
inference(resolution,[],[f1627,f93]) ).
fof(f78667,definition,
( spl0_66
<=> between(d,a,c) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f78668,plain,
( ~ between(d,a,c)
| spl0_66 ),
inference(avatar_component_clause,[],[f78667]) ).
fof(f78669,plain,
( between(d,a,c)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f78667]) ).
fof(f78686,plain,
( colinear(a,c,d)
| ~ spl0_66 ),
inference(resolution,[],[f78669,f21]) ).
fof(f78759,plain,
( $false
| spl0_2
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f78686,f138]) ).
fof(f78760,plain,
( spl0_2
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f78759]) ).
fof(f79066,plain,
( b = d
| a = extension(b,d,d,a)
| ~ spl0_13 ),
inference(resolution,[],[f4932,f50]) ).
fof(f79132,plain,
( a = extension(b,d,d,a)
| ~ spl0_13
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f79066,f59705]) ).
fof(f91818,plain,
( between(b,d,c)
| between(b,c,d)
| ~ spl0_4
| ~ spl0_13 ),
inference(resolution,[],[f74340,f4932]) ).
fof(f91838,plain,
( between(b,c,d)
| ~ spl0_4
| ~ spl0_13
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f91818,f31137]) ).
fof(f91839,plain,
( $false
| ~ spl0_4
| ~ spl0_13
| spl0_19
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f91838,f39366]) ).
fof(f91840,plain,
( ~ spl0_4
| ~ spl0_13
| spl0_19
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f91839]) ).
fof(f91911,plain,
( $false
| spl0_1
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f55724,f134]) ).
fof(f91912,plain,
( spl0_1
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f91911]) ).
fof(f92001,plain,
( ! [X0,X1] : between(c,d,extension(b,d,X0,X1))
| ~ spl0_25 ),
inference(resolution,[],[f39367,f387]) ).
fof(f92353,plain,
( ! [X0,X1] : colinear(c,d,extension(b,d,X0,X1))
| ~ spl0_25 ),
inference(resolution,[],[f92001,f19]) ).
fof(f93826,plain,
( colinear(c,d,a)
| ~ spl0_13
| ~ spl0_25
| spl0_45 ),
inference(superposition,[],[f92353,f79132]) ).
fof(f93837,plain,
( colinear(a,c,d)
| ~ spl0_13
| ~ spl0_25
| spl0_45 ),
inference(resolution,[],[f93826,f103]) ).
fof(f93841,plain,
( $false
| spl0_2
| ~ spl0_13
| ~ spl0_25
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f93837,f138]) ).
fof(f93842,plain,
( spl0_2
| ~ spl0_13
| ~ spl0_25
| spl0_45 ),
inference(avatar_contradiction_clause,[],[f93841]) ).
fof(f93854,plain,
( $false
| ~ spl0_3
| ~ spl0_13
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f31163,f78668]) ).
fof(f93855,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f93854]) ).
fof(f93871,plain,
( colinear(c,a,d)
| ~ spl0_2 ),
inference(resolution,[],[f137,f104]) ).
fof(f93991,plain,
( between(c,d,b)
| ~ spl0_19 ),
inference(resolution,[],[f31138,f58]) ).
fof(f94007,plain,
( colinear(b,c,d)
| ~ spl0_19 ),
inference(resolution,[],[f31138,f98]) ).
fof(f94049,plain,
( $false
| spl0_1
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f94007,f134]) ).
fof(f94050,plain,
( spl0_1
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f94049]) ).
fof(f94056,plain,
( $false
| ~ spl0_19
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f93991,f39362]) ).
fof(f94057,plain,
( ~ spl0_19
| spl0_24 ),
inference(avatar_contradiction_clause,[],[f94056]) ).
fof(f94066,definition,
( spl0_74
<=> between(a,c,d) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f94067,plain,
( ~ between(a,c,d)
| spl0_74 ),
inference(avatar_component_clause,[],[f94066]) ).
fof(f94068,plain,
( between(a,c,d)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f94066]) ).
fof(f94082,plain,
( a = d
| c = extension(d,a,a,c)
| ~ spl0_66 ),
inference(resolution,[],[f78669,f50]) ).
fof(f94153,plain,
( c = extension(d,a,a,c)
| spl0_15
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f94082,f5184]) ).
fof(f94274,plain,
( ~ between(d,c,a)
| a = c
| spl0_15
| ~ spl0_66 ),
inference(superposition,[],[f383,f94153]) ).
fof(f94350,plain,
( ~ between(d,c,a)
| spl0_6
| spl0_15
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f94274,f1677]) ).
fof(f94351,plain,
( ~ spl0_22
| spl0_6
| spl0_15
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f94350,f78667,f5183,f1676,f39192]) ).
fof(f94450,definition,
( spl0_75
<=> between(b,a,c) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f94452,plain,
( between(b,a,c)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f94450]) ).
fof(f95424,plain,
( colinear(a,c,d)
| ~ spl0_74 ),
inference(resolution,[],[f94068,f19]) ).
fof(f95496,definition,
( spl0_76
<=> between(a,d,c) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f95497,plain,
( ~ between(a,d,c)
| spl0_76 ),
inference(avatar_component_clause,[],[f95496]) ).
fof(f95498,plain,
( between(a,d,c)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f95496]) ).
fof(f95500,definition,
( spl0_77
<=> between(c,a,d) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f95501,plain,
( ~ between(c,a,d)
| spl0_77 ),
inference(avatar_component_clause,[],[f95500]) ).
fof(f95502,plain,
( between(c,a,d)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f95500]) ).
fof(f96356,plain,
( between(d,a,c)
| ~ spl0_77 ),
inference(resolution,[],[f95502,f58]) ).
fof(f96425,plain,
( $false
| spl0_66
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f96356,f78668]) ).
fof(f96426,plain,
( spl0_66
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f96425]) ).
fof(f96443,plain,
( ! [X0] :
( ~ between(X0,a,d)
| between(X0,d,c)
| a = d )
| ~ spl0_76 ),
inference(resolution,[],[f95498,f66]) ).
fof(f96445,plain,
( ! [X0] :
( ~ between(X0,a,c)
| between(X0,d,c) )
| ~ spl0_76 ),
inference(resolution,[],[f95498,f68]) ).
fof(f96501,plain,
( ! [X0] :
( ~ between(X0,a,d)
| between(X0,d,c) )
| spl0_15
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f96443,f5184]) ).
fof(f96803,plain,
( ! [X0,X1] : between(extension(c,a,X0,X1),d,c)
| ~ spl0_76 ),
inference(resolution,[],[f96445,f157]) ).
fof(f97804,plain,
( ! [X0,X1] : colinear(extension(c,a,X0,X1),c,d)
| ~ spl0_76 ),
inference(resolution,[],[f96803,f98]) ).
fof(f98543,plain,
( spl0_75
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f1637,f1621,f94450]) ).
fof(f98544,plain,
( between(b,d,c)
| ~ spl0_75
| ~ spl0_76 ),
inference(resolution,[],[f94452,f96445]) ).
fof(f98623,plain,
( $false
| spl0_19
| ~ spl0_75
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f98544,f31137]) ).
fof(f98624,plain,
( spl0_19
| ~ spl0_75
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f98623]) ).
fof(f98777,plain,
( colinear(a,c,d)
| ~ spl0_76 ),
inference(superposition,[],[f97804,f35]) ).
fof(f98826,plain,
( ! [X0] :
( ~ between(a,b,X0)
| a = b
| between(b,X0,c)
| between(b,c,X0) )
| ~ spl0_5 ),
inference(resolution,[],[f1631,f91]) ).
fof(f98872,plain,
( ! [X0] :
( ~ between(a,b,X0)
| between(b,X0,c)
| between(b,c,X0) )
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f98826,f111]) ).
fof(f99332,plain,
( between(b,d,c)
| ~ spl0_12
| spl0_15
| ~ spl0_76 ),
inference(resolution,[],[f4948,f96501]) ).
fof(f99416,plain,
( $false
| ~ spl0_12
| spl0_15
| spl0_19
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f99332,f31137]) ).
fof(f99417,plain,
( ~ spl0_12
| spl0_15
| spl0_19
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f99416]) ).
fof(f99438,plain,
( ! [X0] :
( ~ between(c,X0,a)
| between(c,X0,d) )
| ~ spl0_77 ),
inference(resolution,[],[f95502,f69]) ).
fof(f99827,plain,
( between(c,b,d)
| ~ spl0_11
| ~ spl0_77 ),
inference(resolution,[],[f99438,f4106]) ).
fof(f99846,plain,
( $false
| ~ spl0_11
| spl0_20
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f99827,f31141]) ).
fof(f99847,plain,
( ~ spl0_11
| spl0_20
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f99846]) ).
fof(f99872,plain,
( $false
| spl0_1
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f68238,f134]) ).
fof(f99873,plain,
( spl0_1
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f99872]) ).
fof(f99908,plain,
( $false
| spl0_1
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f65536,f134]) ).
fof(f99909,plain,
( spl0_1
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f99908]) ).
fof(f100371,plain,
( ! [X0] :
( ~ between(b,X0,a)
| between(a,X0,d) )
| ~ spl0_14 ),
inference(resolution,[],[f4936,f2063]) ).
fof(f116526,plain,
( between(b,d,c)
| between(b,c,d)
| ~ spl0_5
| ~ spl0_14 ),
inference(resolution,[],[f98872,f4936]) ).
fof(f116536,plain,
( between(b,c,d)
| ~ spl0_5
| ~ spl0_14
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f116526,f31137]) ).
fof(f116537,plain,
( $false
| ~ spl0_5
| ~ spl0_14
| spl0_19
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f116536,f39366]) ).
fof(f116538,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_19
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f116537]) ).
fof(f116865,plain,
( between(a,c,d)
| ~ spl0_4
| ~ spl0_14 ),
inference(resolution,[],[f1627,f100371]) ).
fof(f116934,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f116865,f94067]) ).
fof(f116935,plain,
( ~ spl0_4
| ~ spl0_14
| spl0_74 ),
inference(avatar_contradiction_clause,[],[f116934]) ).
fof(f116942,plain,
( $false
| ~ spl0_7
| ~ spl0_12
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f5017,f39366]) ).
fof(f116943,plain,
( ~ spl0_7
| ~ spl0_12
| spl0_25 ),
inference(avatar_contradiction_clause,[],[f116942]) ).
fof(f117026,plain,
( ! [X0] :
( ~ between(b,X0,d)
| between(X0,c,d)
| between(c,X0,d) )
| ~ spl0_25 ),
inference(resolution,[],[f39367,f94]) ).
fof(f117184,plain,
( ! [X0,X1] :
( between(d,a,extension(a,b,X0,X1))
| a = b )
| ~ spl0_12 ),
inference(resolution,[],[f4928,f1099]) ).
fof(f117222,plain,
( ! [X0,X1] : between(d,a,extension(a,b,X0,X1))
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f117184,f111]) ).
fof(f130393,plain,
( between(a,c,d)
| between(c,a,d)
| ~ spl0_12
| ~ spl0_25 ),
inference(resolution,[],[f4948,f117026]) ).
fof(f130482,plain,
( between(c,a,d)
| ~ spl0_12
| ~ spl0_25
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f130393,f94067]) ).
fof(f130483,plain,
( $false
| ~ spl0_12
| ~ spl0_25
| spl0_74
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f130482,f95501]) ).
fof(f130484,plain,
( ~ spl0_12
| ~ spl0_25
| spl0_74
| spl0_77 ),
inference(avatar_contradiction_clause,[],[f130483]) ).
fof(f130792,plain,
( a = b
| c = extension(a,b,b,c)
| ~ spl0_5 ),
inference(resolution,[],[f1631,f50]) ).
fof(f130796,plain,
( ! [X0] :
( ~ between(a,X0,b)
| between(X0,b,c) )
| ~ spl0_5 ),
inference(resolution,[],[f1631,f65]) ).
fof(f130853,plain,
( c = extension(a,b,b,c)
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f130792,f111]) ).
fof(f134959,plain,
( between(d,a,c)
| ~ spl0_5
| ~ spl0_12 ),
inference(superposition,[],[f117222,f130853]) ).
fof(f134968,plain,
( $false
| ~ spl0_5
| ~ spl0_12
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f134959,f78668]) ).
fof(f134969,plain,
( ~ spl0_5
| ~ spl0_12
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f134968]) ).
fof(f136618,plain,
( between(d,b,c)
| ~ spl0_5
| ~ spl0_16 ),
inference(resolution,[],[f130796,f5188]) ).
fof(f136637,plain,
( $false
| ~ spl0_5
| ~ spl0_16
| spl0_23 ),
inference(forward_subsumption_resolution,[],[f136618,f39358]) ).
fof(f136638,plain,
( ~ spl0_5
| ~ spl0_16
| spl0_23 ),
inference(avatar_contradiction_clause,[],[f136637]) ).
fof(f137074,plain,
( between(a,d,c)
| ~ spl0_16
| ~ spl0_49 ),
inference(resolution,[],[f64421,f5188]) ).
fof(f137075,plain,
( $false
| ~ spl0_16
| ~ spl0_49
| spl0_76 ),
inference(forward_subsumption_resolution,[],[f137074,f95497]) ).
fof(f137076,plain,
( ~ spl0_16
| ~ spl0_49
| spl0_76 ),
inference(avatar_contradiction_clause,[],[f137075]) ).
fof(f137095,plain,
( $false
| spl0_2
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f98777,f138]) ).
fof(f137096,plain,
( spl0_2
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f137095]) ).
fof(f137111,plain,
( $false
| spl0_2
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f95424,f138]) ).
fof(f137112,plain,
( spl0_2
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f137111]) ).
fof(f137142,plain,
( ! [X0] :
( ~ between(b,a,X0)
| a = b
| between(a,X0,c)
| between(a,c,X0) )
| ~ spl0_75 ),
inference(resolution,[],[f94452,f91]) ).
fof(f137196,plain,
( ! [X0] :
( ~ between(b,a,X0)
| between(a,X0,c)
| between(a,c,X0) )
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f137142,f111]) ).
fof(f176505,plain,
( between(a,d,c)
| between(a,c,d)
| ~ spl0_12
| ~ spl0_75 ),
inference(resolution,[],[f137196,f4948]) ).
fof(f176526,plain,
( between(a,c,d)
| ~ spl0_12
| ~ spl0_75
| spl0_76 ),
inference(forward_subsumption_resolution,[],[f176505,f95497]) ).
fof(f176527,plain,
( $false
| ~ spl0_12
| spl0_74
| ~ spl0_75
| spl0_76 ),
inference(forward_subsumption_resolution,[],[f176526,f94067]) ).
fof(f176528,plain,
( ~ spl0_12
| spl0_74
| ~ spl0_75
| spl0_76 ),
inference(avatar_contradiction_clause,[],[f176527]) ).
fof(f176536,plain,
( between(c,a,d)
| between(a,d,c)
| between(d,c,a)
| ~ spl0_2 ),
inference(resolution,[],[f93871,f22]) ).
fof(f176542,plain,
( between(a,d,c)
| between(d,c,a)
| ~ spl0_2
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f176536,f95501]) ).
fof(f176543,plain,
( between(d,c,a)
| ~ spl0_2
| spl0_76
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f176542,f95497]) ).
fof(f176585,plain,
( a = c
| d = extension(a,c,c,d)
| ~ spl0_74 ),
inference(resolution,[],[f94068,f50]) ).
fof(f176592,plain,
( ! [X0] :
( ~ between(X0,a,d)
| between(X0,c,d) )
| ~ spl0_74 ),
inference(resolution,[],[f94068,f68]) ).
fof(f176599,plain,
( ! [X0] :
( ~ between(a,X0,d)
| between(X0,c,d)
| between(c,X0,d) )
| ~ spl0_74 ),
inference(resolution,[],[f94068,f94]) ).
fof(f176653,plain,
( d = extension(a,c,c,d)
| spl0_6
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f176585,f1677]) ).
fof(f176682,plain,
( spl0_22
| ~ spl0_2
| spl0_76
| spl0_77 ),
inference(avatar_split_clause,[],[f176543,f95500,f95496,f136,f39192]) ).
fof(f176800,plain,
( ! [X0,X1] :
( between(extension(c,a,X0,X1),a,d)
| a = c )
| spl0_6
| ~ spl0_74 ),
inference(superposition,[],[f7472,f176653]) ).
fof(f176831,plain,
( ! [X0,X1] : between(extension(c,a,X0,X1),a,d)
| spl0_6
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f176800,f1677]) ).
fof(f178276,plain,
( between(b,a,d)
| spl0_6
| ~ spl0_8
| ~ spl0_74 ),
inference(superposition,[],[f176831,f2633]) ).
fof(f178302,plain,
( between(b,c,d)
| spl0_6
| ~ spl0_8
| ~ spl0_74 ),
inference(resolution,[],[f178276,f176592]) ).
fof(f178390,plain,
( $false
| spl0_6
| ~ spl0_8
| spl0_25
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f178302,f39366]) ).
fof(f178391,plain,
( spl0_6
| ~ spl0_8
| spl0_25
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f178390]) ).
fof(f180714,plain,
( between(b,c,d)
| between(c,b,d)
| ~ spl0_14
| ~ spl0_74 ),
inference(resolution,[],[f176599,f4936]) ).
fof(f180750,plain,
( between(c,b,d)
| ~ spl0_14
| spl0_25
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f180714,f39366]) ).
fof(f180753,plain,
( $false
| ~ spl0_14
| spl0_20
| spl0_25
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f180750,f31141]) ).
fof(f180754,plain,
( ~ spl0_14
| spl0_20
| spl0_25
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f180753]) ).
fof(f180826,plain,
( ! [X0] :
( ~ between(X0,d,b)
| b = d
| between(X0,c,d)
| between(c,X0,d) )
| ~ spl0_24 ),
inference(resolution,[],[f39363,f92]) ).
fof(f180877,plain,
( ! [X0] :
( ~ between(X0,d,b)
| between(X0,c,d)
| between(c,X0,d) )
| ~ spl0_24
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f180826,f59705]) ).
fof(f191740,plain,
( between(a,c,d)
| between(c,a,d)
| ~ spl0_16
| ~ spl0_24
| spl0_45 ),
inference(resolution,[],[f5188,f180877]) ).
fof(f191829,plain,
( between(c,a,d)
| ~ spl0_16
| ~ spl0_24
| spl0_45
| spl0_74 ),
inference(forward_subsumption_resolution,[],[f191740,f94067]) ).
fof(f191830,plain,
( $false
| ~ spl0_16
| ~ spl0_24
| spl0_45
| spl0_74
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f191829,f95501]) ).
fof(f191831,plain,
( ~ spl0_16
| ~ spl0_24
| spl0_45
| spl0_74
| spl0_77 ),
inference(avatar_contradiction_clause,[],[f191830]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f139]) ).
cnf(s2,plain,
( spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_6
| spl0_8 ),
inference(sat_conversion,[],[f2634]) ).
cnf(s9,plain,
( spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f2710]) ).
cnf(s11,plain,
( ~ spl0_4
| spl0_7 ),
inference(sat_conversion,[],[f4069]) ).
cnf(s13,plain,
( spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f4937]) ).
cnf(s19,plain,
( ~ spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f30834]) ).
cnf(s20,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_14 ),
inference(sat_conversion,[],[f31094]) ).
cnf(s25,plain,
( spl0_1
| ~ spl0_15 ),
inference(sat_conversion,[],[f31161]) ).
cnf(s26,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_19 ),
inference(sat_conversion,[],[f31293]) ).
cnf(s28,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_14 ),
inference(sat_conversion,[],[f39197]) ).
cnf(s29,plain,
( ~ spl0_1
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f39368]) ).
cnf(s106,plain,
( ~ spl0_5
| spl0_11 ),
inference(sat_conversion,[],[f57284]) ).
cnf(s112,plain,
( spl0_2
| ~ spl0_14
| ~ spl0_25 ),
inference(sat_conversion,[],[f61114]) ).
cnf(s118,plain,
( spl0_19
| ~ spl0_24 ),
inference(sat_conversion,[],[f61393]) ).
cnf(s149,plain,
( spl0_2
| ~ spl0_5
| ~ spl0_19 ),
inference(sat_conversion,[],[f62761]) ).
cnf(s152,plain,
( ~ spl0_23
| spl0_45
| spl0_49 ),
inference(sat_conversion,[],[f64422]) ).
cnf(s171,plain,
( spl0_2
| ~ spl0_45 ),
inference(sat_conversion,[],[f73981]) ).
cnf(s178,plain,
( spl0_2
| ~ spl0_66 ),
inference(sat_conversion,[],[f78760]) ).
cnf(s212,plain,
( ~ spl0_4
| ~ spl0_13
| spl0_19
| spl0_25 ),
inference(sat_conversion,[],[f91840]) ).
cnf(s248,plain,
( spl0_1
| ~ spl0_25 ),
inference(sat_conversion,[],[f91912]) ).
cnf(s258,plain,
( spl0_2
| ~ spl0_13
| ~ spl0_25
| spl0_45 ),
inference(sat_conversion,[],[f93842]) ).
cnf(s264,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_66 ),
inference(sat_conversion,[],[f93855]) ).
cnf(s269,plain,
( spl0_1
| ~ spl0_19 ),
inference(sat_conversion,[],[f94050]) ).
cnf(s270,plain,
( ~ spl0_19
| spl0_24 ),
inference(sat_conversion,[],[f94057]) ).
cnf(s278,plain,
( spl0_6
| spl0_15
| ~ spl0_22
| ~ spl0_66 ),
inference(sat_conversion,[],[f94351]) ).
cnf(s292,plain,
( spl0_66
| ~ spl0_77 ),
inference(sat_conversion,[],[f96426]) ).
cnf(s306,plain,
( ~ spl0_3
| spl0_75 ),
inference(sat_conversion,[],[f98543]) ).
cnf(s307,plain,
( spl0_19
| ~ spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f98624]) ).
cnf(s313,plain,
( ~ spl0_12
| spl0_15
| spl0_19
| ~ spl0_76 ),
inference(sat_conversion,[],[f99417]) ).
cnf(s328,plain,
( ~ spl0_11
| spl0_20
| ~ spl0_77 ),
inference(sat_conversion,[],[f99847]) ).
cnf(s339,plain,
( spl0_1
| ~ spl0_20 ),
inference(sat_conversion,[],[f99873]) ).
cnf(s357,plain,
( spl0_1
| ~ spl0_23 ),
inference(sat_conversion,[],[f99909]) ).
cnf(s375,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_19
| spl0_25 ),
inference(sat_conversion,[],[f116538]) ).
cnf(s376,plain,
( ~ spl0_4
| ~ spl0_14
| spl0_74 ),
inference(sat_conversion,[],[f116935]) ).
cnf(s378,plain,
( ~ spl0_7
| ~ spl0_12
| spl0_25 ),
inference(sat_conversion,[],[f116943]) ).
cnf(s402,plain,
( ~ spl0_12
| ~ spl0_25
| spl0_74
| spl0_77 ),
inference(sat_conversion,[],[f130484]) ).
cnf(s406,plain,
( ~ spl0_5
| ~ spl0_12
| spl0_66 ),
inference(sat_conversion,[],[f134969]) ).
cnf(s407,plain,
( ~ spl0_5
| ~ spl0_16
| spl0_23 ),
inference(sat_conversion,[],[f136638]) ).
cnf(s408,plain,
( ~ spl0_16
| ~ spl0_49
| spl0_76 ),
inference(sat_conversion,[],[f137076]) ).
cnf(s418,plain,
( spl0_2
| ~ spl0_76 ),
inference(sat_conversion,[],[f137096]) ).
cnf(s419,plain,
( spl0_2
| ~ spl0_74 ),
inference(sat_conversion,[],[f137112]) ).
cnf(s438,plain,
( ~ spl0_12
| spl0_74
| ~ spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f176528]) ).
cnf(s441,plain,
( ~ spl0_2
| spl0_22
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f176682]) ).
cnf(s459,plain,
( spl0_6
| ~ spl0_8
| spl0_25
| ~ spl0_74 ),
inference(sat_conversion,[],[f178391]) ).
cnf(s469,plain,
( ~ spl0_14
| spl0_20
| spl0_25
| ~ spl0_74 ),
inference(sat_conversion,[],[f180754]) ).
cnf(s474,plain,
( ~ spl0_16
| ~ spl0_24
| spl0_45
| spl0_74
| spl0_77 ),
inference(sat_conversion,[],[f191831]) ).
cnf(s475,plain,
( ~ spl0_5
| spl0_66
| spl0_1 ),
inference(rat,[],[s13,s19,s375,s406,s407,s357,s269,s248]) ).
cnf(s476,plain,
( ~ spl0_4
| spl0_74
| spl0_1 ),
inference(rat,[],[s378,s13,s11,s212,s376,s269,s248]) ).
cnf(s477,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s13,s438,s28,s264,s306,s2,s476,s475,s178,s418,s419]) ).
cnf(s478,plain,
( ~ spl0_5
| spl0_1 ),
inference(rat,[],[s441,s313,s278,s328,s13,s19,s475,s106,s375,s407,s357,s339,s269,s248,s25,s9,s477]) ).
cnf(s479,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s13,s469,s378,s476,s11,s212,s339,s269,s248]) ).
cnf(s480,plain,
spl0_1,
inference(rat,[],[s438,s459,s13,s307,s6,s20,s26,s306,s2,s479,s478,s9,s248,s269]) ).
cnf(s481,plain,
~ spl0_2,
inference(rat,[],[s1,s480]) ).
cnf(s482,plain,
~ spl0_74,
inference(rat,[],[s419,s481]) ).
cnf(s483,plain,
~ spl0_76,
inference(rat,[],[s418,s481]) ).
cnf(s484,plain,
~ spl0_66,
inference(rat,[],[s178,s481]) ).
cnf(s485,plain,
~ spl0_45,
inference(rat,[],[s171,s481]) ).
cnf(s488,plain,
~ spl0_77,
inference(rat,[],[s292,s484]) ).
cnf(s489,plain,
( ~ spl0_14
| spl0_19
| ~ spl0_5 ),
inference(rat,[],[s112,s375,s481]) ).
cnf(s490,plain,
~ spl0_5,
inference(rat,[],[s152,s408,s29,s19,s258,s13,s489,s118,s406,s149,s485,s483,s480,s481,s484]) ).
cnf(s491,plain,
( spl0_25
| spl0_19
| ~ spl0_4 ),
inference(rat,[],[s13,s212,s378,s11,s376,s482]) ).
cnf(s492,plain,
( ~ spl0_25
| spl0_14 ),
inference(rat,[],[s13,s258,s402,s481,s485,s488,s482]) ).
cnf(s493,plain,
~ spl0_4,
inference(rat,[],[s474,s19,s270,s13,s491,s378,s492,s376,s11,s485,s482,s488]) ).
cnf(s495,plain,
spl0_3,
inference(rat,[],[s2,s490,s493]) ).
cnf(s497,plain,
spl0_75,
inference(rat,[],[s306,s495]) ).
cnf(s498,plain,
~ spl0_14,
inference(rat,[],[s28,s481,s495]) ).
cnf(s501,plain,
~ spl0_13,
inference(rat,[],[s264,s484,s495]) ).
cnf(s503,plain,
~ spl0_12,
inference(rat,[],[s438,s483,s482,s497]) ).
cnf(s506,plain,
$false,
inference(rat,[],[s13,s498,s503,s501]) ).
fof(f191832,plain,
$false,
inference(avatar_sat_refutation,[],[s506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO012-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n014.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 06:34:32 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.60/1.77 % (450874)Will run a generic schedule for satisfiability detection.
% 7.60/1.77 % (450882)dis+10_1_sil=32000:sp=arity:random_seed=3642103209:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.60/1.77 % (450880)% WARNING: option uhcvi not known.
% 7.60/1.77 % (450879)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1436161013_2999 on theBenchmark for (2999ds/0Mi)
% 7.60/1.77 % (450880)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3026105824:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.60/1.77 % (450881)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3035230931:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.60/1.77 % (450884)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2738945820:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.60/1.77 % (450883)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1227093934:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.60/1.77 % (450885)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=847120495:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.60/1.77 % Detected minimum model sizes of [3]
% 7.60/1.77 % Detected maximum model sizes of [max]
% 7.60/1.77 % TRYING [3]
% 7.60/1.77 % (450882)Instruction limit reached!
% 7.60/1.77 % (450882)------------------------------
% 7.60/1.77 % (450882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.77 % (450882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.77 % (450882)CaDiCaL version: 2.1.3
% 7.60/1.77 % (450882)Termination reason: Instruction limit
% 7.60/1.77 % (450882)Termination phase: Saturation
% 7.60/1.77 % (450882)Time elapsed: 0.035 s
% 7.60/1.77 % (450882)Peak memory usage: 12 MB
% 7.60/1.77 % (450882)Instructions burned: 103 (million)
% 7.60/1.77 % (450893)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=10382696:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.60/1.77 % Detected minimum model sizes of [3]
% 7.60/1.77 % Detected maximum model sizes of [max]
% 7.60/1.77 % TRYING [3]
% 7.60/1.77 % (450883)Instruction limit reached!
% 7.60/1.77 % (450883)------------------------------
% 7.60/1.77 % (450883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.77 % (450883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.77 % (450883)CaDiCaL version: 2.1.3
% 7.60/1.77 % (450883)Termination reason: Instruction limit
% 7.60/1.77 % (450883)Termination phase: Saturation
% 7.60/1.77 % (450883)Time elapsed: 0.059 s
% 7.60/1.77 % (450883)Peak memory usage: 12 MB
% 7.60/1.77 % (450883)Instructions burned: 118 (million)
% 7.60/1.77 % TRYING [4]
% 7.60/1.77 % (450895)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3247243783:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.60/1.77 % (450884)Instruction limit reached!
% 7.60/1.77 % (450884)------------------------------
% 7.60/1.77 % (450884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.77 % (450884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.77 % (450884)CaDiCaL version: 2.1.3
% 7.60/1.77 % (450884)Termination reason: Instruction limit
% 7.60/1.77 % (450884)Termination phase: Saturation
% 7.60/1.77 % (450884)Time elapsed: 0.083 s
% 7.60/1.77 % (450884)Peak memory usage: 12 MB
% 7.60/1.77 % (450884)Instructions burned: 132 (million)
% 7.60/1.77 % TRYING [4]
% 7.60/1.77 % (450885)Instruction limit reached!
% 7.60/1.77 % (450885)------------------------------
% 7.60/1.77 % (450885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.60/1.77 % (450885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.77 % (450885)CaDiCaL version: 2.1.3
% 7.60/1.77 % (450885)Termination reason: Instruction limit
% 7.60/1.77 % (450885)Termination phase: Saturation
% 7.60/1.77 % (450885)Time elapsed: 0.090 s
% 7.60/1.77 % (450885)Peak memory usage: 13 MB
% 7.60/1.77 % (450885)Instructions burned: 160 (million)
% 7.60/1.77 % (450897)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=3210444965:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.60/1.77 % (450898)ott-21_1_sil=16000:fs=off:random_seed=1797889545:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.60/1.77 % (450895)Instruction limit reached!
% 7.60/1.77 % (450895)------------------------------
% 7.60/1.77 % (450895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.52/5.35 % (450895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.52/5.35 % (450895)CaDiCaL version: 2.1.3
% 34.52/5.35 % (450895)Termination reason: Instruction limit
% 34.52/5.35 % (450895)Termination phase: Saturation
% 34.52/5.35 % (450895)Time elapsed: 0.081 s
% 34.52/5.35 % (450895)Peak memory usage: 12 MB
% 34.52/5.35 % (450895)Instructions burned: 132 (million)
% 34.52/5.35 % (450893)Instruction limit reached!
% 34.52/5.35 % (450893)------------------------------
% 34.52/5.35 % (450893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.52/5.35 % (450893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.52/5.35 % (450893)CaDiCaL version: 2.1.3
% 34.52/5.35 % (450893)Termination reason: Instruction limit
% 34.52/5.35 % (450893)Termination phase: Finite model building constraint generation
% 34.52/5.35 % (450893)Time elapsed: 0.129 s
% 34.52/5.35 % (450893)Peak memory usage: 28 MB
% 34.52/5.35 % (450893)Instructions burned: 718 (million)
% 34.52/5.35 % (450902)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1989382615:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.52/5.35 % (450901)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1716724977:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 34.52/5.35 % Detected minimum model sizes of [3]
% 34.52/5.35 % Detected maximum model sizes of [max]
% 34.52/5.35 % TRYING [3]
% 34.52/5.35 % (450898)Instruction limit reached!
% 34.52/5.35 % (450898)------------------------------
% 34.52/5.35 % (450898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.52/5.35 % (450898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.52/5.35 % (450898)CaDiCaL version: 2.1.3
% 34.52/5.35 % (450898)Termination reason: Instruction limit
% 34.52/5.35 % (450898)Termination phase: Saturation
% 34.52/5.35 % (450898)Time elapsed: 0.096 s
% 34.52/5.35 % (450898)Peak memory usage: 12 MB
% 34.52/5.35 % (450898)Instructions burned: 181 (million)
% 34.52/5.35 % (450905)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2539910992:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 34.52/5.35 % TRYING [4]
% 34.52/5.35 % (450902)Instruction limit reached!
% 34.52/5.35 % (450902)------------------------------
% 34.52/5.35 % (450902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.52/5.35 % (450902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.52/5.35 % (450902)CaDiCaL version: 2.1.3
% 34.52/5.35 % (450902)Termination reason: Instruction limit
% 34.52/5.35 % (450902)Termination phase: Finite model building constraint generation
% 34.52/5.35 % (450902)Time elapsed: 0.169 s
% 34.52/5.35 % (450902)Peak memory usage: 39 MB
% 34.52/5.35 % (450902)Instructions burned: 867 (million)
% 34.52/5.35 % (450907)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2747217062:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 34.52/5.35 % (450901)Instruction limit reached!
% 34.52/5.35 % (450901)------------------------------
% 34.52/5.35 % (450901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.52/5.35 % (450901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.52/5.35 % (450901)CaDiCaL version: 2.1.3
% 34.52/5.35 % (450901)Termination reason: Instruction limit
% 34.52/5.35 % (450901)Termination phase: Saturation
% 34.52/5.35 % (450901)Time elapsed: 0.291 s
% 34.52/5.35 % (450901)Peak memory usage: 14 MB
% 34.52/5.35 % (450901)Instructions burned: 477 (million)
% 34.52/5.35 % (450897)Instruction limit reached!
% 34.52/5.35 % (450897)------------------------------
% 34.52/5.35 % (450897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.52/5.35 % (450897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.52/5.35 % (450897)CaDiCaL version: 2.1.3
% 34.52/5.35 % (450897)Termination reason: Instruction limit
% 34.52/5.35 % (450897)Termination phase: Saturation
% 34.52/5.35 % (450897)Time elapsed: 0.389 s
% 34.52/5.35 % (450897)Peak memory usage: 17 MB
% 34.52/5.35 % (450897)Instructions burned: 684 (million)
% 34.52/5.35 % (450909)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1308527439:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 34.52/5.35 % (450910)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2523474425:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 34.52/5.35 % TRYING [5]
% 34.52/5.35 % (450907)Instruction limit reached!
% 85.58/12.55 % (450907)------------------------------
% 85.58/12.55 % (450907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.58/12.55 % (450907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.58/12.55 % (450907)CaDiCaL version: 2.1.3
% 85.58/12.55 % (450907)Termination reason: Instruction limit
% 85.58/12.55 % (450907)Termination phase: Finite model building constraint generation
% 85.58/12.55 % (450907)Time elapsed: 0.236 s
% 85.58/12.55 % (450907)Peak memory usage: 106 MB
% 85.58/12.55 % (450907)Instructions burned: 893 (million)
% 85.58/12.55 % (450913)fmb+10_1_sil=64000:random_seed=502174949:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 85.58/12.55 % Detected minimum model sizes of [3]
% 85.58/12.55 % Detected maximum model sizes of [max]
% 85.58/12.55 % TRYING [3]
% 85.58/12.55 % TRYING [4]
% 85.58/12.55 % (450909)Instruction limit reached!
% 85.58/12.55 % (450909)------------------------------
% 85.58/12.55 % (450909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.58/12.55 % (450909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.58/12.55 % (450909)CaDiCaL version: 2.1.3
% 85.58/12.56 % (450909)Termination reason: Instruction limit
% 85.58/12.56 % (450909)Termination phase: Saturation
% 85.58/12.56 % (450909)Time elapsed: 0.427 s
% 85.58/12.56 % (450909)Peak memory usage: 16 MB
% 85.58/12.56 % (450909)Instructions burned: 693 (million)
% 85.58/12.56 % (450915)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2888408808:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 85.58/12.56 % Detected minimum model sizes of [3]
% 85.58/12.56 % Detected maximum model sizes of [max]
% 85.58/12.56 % (450915)Cannot represent all propositional literals internally
% 85.58/12.56 % (450915)Refutation not found, incomplete strategy
% 85.58/12.56 % (450915)------------------------------
% 85.58/12.56 % (450915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.58/12.56 % (450915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.58/12.56 % (450915)CaDiCaL version: 2.1.3
% 85.58/12.56 % (450915)Termination reason: Refutation not found, incomplete strategy
% 85.58/12.56 % (450915)Time elapsed: 0.005 s
% 85.58/12.56 % (450915)Peak memory usage: 10 MB
% 85.58/12.56 % (450915)Instructions burned: 8 (million)
% 85.58/12.56 % (450915)------------------------------
% 85.58/12.56 % (450915)------------------------------
% 85.58/12.56 % (450917)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2948014824:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 85.58/12.56 % Detected minimum model sizes of [3]
% 85.58/12.56 % Detected maximum model sizes of [max]
% 85.58/12.56 % TRYING [8]
% 85.58/12.56 % (450905)Instruction limit reached!
% 85.58/12.56 % (450905)------------------------------
% 85.58/12.56 % (450905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.58/12.56 % (450905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.58/12.56 % (450905)CaDiCaL version: 2.1.3
% 85.58/12.56 % (450905)Termination reason: Instruction limit
% 85.58/12.56 % (450905)Termination phase: Saturation
% 85.58/12.56 % (450905)Time elapsed: 0.752 s
% 85.58/12.56 % (450905)Peak memory usage: 21 MB
% 85.58/12.56 % (450905)Instructions burned: 1180 (million)
% 85.58/12.56 % (450910)Instruction limit reached!
% 85.58/12.56 % (450910)------------------------------
% 85.58/12.56 % (450910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.58/12.56 % (450910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.58/12.56 % (450910)CaDiCaL version: 2.1.3
% 85.58/12.56 % (450910)Termination reason: Instruction limit
% 85.58/12.56 % (450910)Termination phase: Saturation
% 85.58/12.56 % (450910)Time elapsed: 0.473 s
% 85.58/12.56 % (450910)Peak memory usage: 17 MB
% 85.58/12.56 % (450910)Instructions burned: 880 (million)
% 85.58/12.56 % (450919)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4033601878:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 85.58/12.56 % (450920)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3399681921:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 85.58/12.56 % (450917)Instruction limit reached!
% 85.58/12.56 % (450917)------------------------------
% 85.58/12.56 % (450917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.58/12.56 % (450917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.58/12.56 % (450917)CaDiCaL version: 2.1.3
% 85.58/12.56 % (450917)Termination reason: Instruction limit
% 85.58/12.56 % (450917)Termination phase: Finite model building constraint generation
% 85.58/12.56 % (450917)Time elapsed: 0.337 s
% 199.97/28.78 % (450917)Peak memory usage: 71 MB
% 199.97/28.78 % (450917)Instructions burned: 920 (million)
% 199.97/28.78 % (450923)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3976356033:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 199.97/28.78 % Detected minimum model sizes of [3]
% 199.97/28.78 % Detected maximum model sizes of [max]
% 199.97/28.78 % (450923)Cannot represent all propositional literals internally
% 199.97/28.78 % (450923)Refutation not found, incomplete strategy
% 199.97/28.78 % (450923)------------------------------
% 199.97/28.78 % (450923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.97/28.78 % (450923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.97/28.78 % (450923)CaDiCaL version: 2.1.3
% 199.97/28.78 % (450923)Termination reason: Refutation not found, incomplete strategy
% 199.97/28.78 % (450923)Time elapsed: 0.006 s
% 199.97/28.78 % (450923)Peak memory usage: 11 MB
% 199.97/28.78 % (450923)Instructions burned: 11 (million)
% 199.97/28.78 % (450923)------------------------------
% 199.97/28.78 % (450923)------------------------------
% 199.97/28.78 % (450925)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1333860681:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi)
% 199.97/28.78 % TRYING [5]
% 199.97/28.78 % Detected minimum model sizes of [3]
% 199.97/28.78 % Detected maximum model sizes of [max]
% 199.97/28.78 % (450925)Cannot represent all propositional literals internally
% 199.97/28.78 % (450925)Refutation not found, incomplete strategy
% 199.97/28.78 % (450925)------------------------------
% 199.97/28.78 % (450925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.97/28.78 % (450925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.97/28.78 % (450925)CaDiCaL version: 2.1.3
% 199.97/28.78 % (450925)Termination reason: Refutation not found, incomplete strategy
% 199.97/28.78 % (450925)Time elapsed: 0.046 s
% 199.97/28.78 % (450925)Peak memory usage: 11 MB
% 199.97/28.78 % (450925)Instructions burned: 93 (million)
% 199.97/28.78 % (450925)------------------------------
% 199.97/28.78 % (450925)------------------------------
% 199.97/28.78 % (450927)ott-2_1_sil=16000:newcnf=on:random_seed=1993506904:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2985 on theBenchmark for (2985ds/869Mi)
% 199.97/28.78 % (450920)Instruction limit reached!
% 199.97/28.78 % (450920)------------------------------
% 199.97/28.78 % (450920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.97/28.78 % (450920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.97/28.78 % (450920)CaDiCaL version: 2.1.3
% 199.97/28.78 % (450920)Termination reason: Instruction limit
% 199.97/28.78 % (450920)Termination phase: Saturation
% 199.97/28.78 % (450920)Time elapsed: 0.833 s
% 199.97/28.78 % (450920)Peak memory usage: 31 MB
% 199.97/28.78 % (450920)Instructions burned: 1480 (million)
% 199.97/28.78 % (450929)ott+10_1_sil=32000:tgt=ground:random_seed=2805614515:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi)
% 199.97/28.78 % (450927)Instruction limit reached!
% 199.97/28.78 % (450927)------------------------------
% 199.97/28.78 % (450927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.97/28.78 % (450927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.97/28.78 % (450927)CaDiCaL version: 2.1.3
% 199.97/28.78 % (450927)Termination reason: Instruction limit
% 199.97/28.78 % (450927)Termination phase: Saturation
% 199.97/28.78 % (450927)Time elapsed: 0.492 s
% 199.97/28.78 % (450927)Peak memory usage: 15 MB
% 199.97/28.78 % (450927)Instructions burned: 869 (million)
% 199.97/28.78 % (450931)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1862902446:i=54282_2980 on theBenchmark for (2980ds/54282Mi)
% 199.97/28.78 % Detected minimum model sizes of [3]
% 199.97/28.78 % Detected maximum model sizes of [max]
% 199.97/28.78 % TRYING [3]
% 199.97/28.78 % TRYING [4]
% 199.97/28.78 % TRYING [5]
% 199.97/28.78 % TRYING [6]
% 199.97/28.78 % (450919)Instruction limit reached!
% 199.97/28.78 % (450919)------------------------------
% 199.97/28.78 % (450919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.97/28.78 % (450919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.97/28.78 % (450919)CaDiCaL version: 2.1.3
% 199.97/28.78 % (450919)Termination reason: Instruction limit
% 199.97/28.78 % (450919)Termination phase: Saturation
% 199.97/28.78 % (450919)Time elapsed: 2.465 s
% 199.97/28.78 % (450919)Peak memory usage: 20 MB
% 199.97/28.78 % (450919)Instructions burned: 5133 (million)
% 199.97/28.78 % (450933)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2219922703:i=3512:aac=none_2964 on theBenchmark for (2964ds/3512Mi)
% 199.97/28.78 % (450929)Instruction limit reached!
% 199.97/28.78 % (450929)------------------------------
% 278.44/39.78 % (450929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 278.44/39.78 % (450929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 278.44/39.78 % (450929)CaDiCaL version: 2.1.3
% 278.44/39.78 % (450929)Termination reason: Instruction limit
% 278.44/39.78 % (450929)Termination phase: Saturation
% 278.44/39.78 % (450929)Time elapsed: 3.026 s
% 278.44/39.78 % (450929)Peak memory usage: 33 MB
% 278.44/39.78 % (450929)Instructions burned: 5114 (million)
% 278.44/39.78 % (450935)dis+21_1_sil=32000:sas=cadical:random_seed=3107027440:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi)
% 278.44/39.78 % TRYING [6]
% 278.44/39.78 % (450933)Instruction limit reached!
% 278.44/39.78 % (450933)------------------------------
% 278.44/39.78 % (450933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 278.44/39.78 % (450933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 278.44/39.78 % (450933)CaDiCaL version: 2.1.3
% 278.44/39.78 % (450933)Termination reason: Instruction limit
% 278.44/39.78 % (450933)Termination phase: Saturation
% 278.44/39.78 % (450933)Time elapsed: 1.801 s
% 278.44/39.78 % (450933)Peak memory usage: 20 MB
% 278.44/39.78 % (450933)Instructions burned: 3513 (million)
% 278.44/39.78 % (450937)ott+11_1_sil=16000:gs=on:random_seed=2221833607:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2946 on theBenchmark for (2946ds/2251Mi)
% 278.44/39.78 % (450913)Instruction limit reached!
% 278.44/39.78 % (450913)------------------------------
% 278.44/39.78 % (450913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 278.44/39.78 % (450913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 278.44/39.78 % (450913)CaDiCaL version: 2.1.3
% 278.44/39.78 % (450913)Termination reason: Instruction limit
% 278.44/39.78 % (450913)Termination phase: Finite model building SAT solving
% 278.44/39.78 % (450913)Time elapsed: 5.706 s
% 278.44/39.78 % (450913)Peak memory usage: 286 MB
% 278.44/39.78 % (450913)Instructions burned: 22063 (million)
% 278.44/39.78 % (450939)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1227437365:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi)
% 278.44/39.78 % Detected minimum model sizes of [3]
% 278.44/39.78 % Detected maximum model sizes of [max]
% 278.44/39.78 % (450937)Instruction limit reached!
% 278.44/39.78 % (450937)------------------------------
% 278.44/39.78 % (450937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 278.44/39.78 % (450937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 278.44/39.78 % (450937)CaDiCaL version: 2.1.3
% 278.44/39.78 % (450937)Termination reason: Instruction limit
% 278.44/39.78 % (450937)Termination phase: Saturation
% 278.44/39.78 % (450937)Time elapsed: 1.372 s
% 278.44/39.78 % (450937)Peak memory usage: 24 MB
% 278.44/39.78 % (450937)Instructions burned: 2251 (million)
% 278.44/39.78 % (450941)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1509725688:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2932 on theBenchmark for (2932ds/4591Mi)
% 278.44/39.78 % TRYING [7]
% 278.44/39.78 % (450935)Instruction limit reached!
% 278.44/39.78 % (450935)------------------------------
% 278.44/39.78 % (450935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 278.44/39.78 % (450935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 278.44/39.78 % (450935)CaDiCaL version: 2.1.3
% 278.44/39.78 % (450935)Termination reason: Instruction limit
% 278.44/39.78 % (450935)Termination phase: Saturation
% 278.44/39.78 % (450935)Time elapsed: 2.239 s
% 278.44/39.78 % (450935)Peak memory usage: 29 MB
% 278.44/39.78 % (450935)Instructions burned: 3773 (million)
% 278.44/39.78 % (450943)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2514149514:i=29340_2928 on theBenchmark for (2928ds/29340Mi)
% 278.44/39.78 % (450941)Instruction limit reached!
% 278.44/39.78 % (450941)------------------------------
% 278.44/39.78 % (450941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 278.44/39.78 % (450941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 278.44/39.78 % (450941)CaDiCaL version: 2.1.3
% 278.44/39.78 % (450941)Termination reason: Instruction limit
% 278.44/39.78 % (450941)Termination phase: Saturation
% 278.44/39.78 % (450941)Time elapsed: 2.695 s
% 278.44/39.78 % (450941)Peak memory usage: 53 MB
% 278.44/39.78 % (450941)Instructions burned: 4592 (million)
% 278.44/39.78 % (450945)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1031323598:i=5211_2905 on theBenchmark for (2905ds/5211Mi)
% 278.44/39.78 % TRYING [7]
% 278.44/39.78 % (450945)Instruction limit reached!
% 278.44/39.78 % (450945)------------------------------
% 151.99/41.18 % (450945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450945)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450945)Termination reason: Instruction limit
% 151.99/41.18 % (450945)Termination phase: Saturation
% 151.99/41.18 % (450945)Time elapsed: 2.663 s
% 151.99/41.18 % (450945)Peak memory usage: 28 MB
% 151.99/41.18 % (450945)Instructions burned: 5212 (million)
% 151.99/41.18 % (450947)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1415030292:i=5497:nm=2_2878 on theBenchmark for (2878ds/5497Mi)
% 151.99/41.18 % Detected minimum model sizes of [3]
% 151.99/41.18 % Detected maximum model sizes of [max]
% 151.99/41.18 % TRYING [17]
% 151.99/41.18 % TRYING [7]
% 151.99/41.18 % (450947)Instruction limit reached!
% 151.99/41.18 % (450947)------------------------------
% 151.99/41.18 % (450947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450947)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450947)Termination reason: Instruction limit
% 151.99/41.18 % (450947)Termination phase: Finite model building constraint generation
% 151.99/41.18 % (450947)Time elapsed: 2.021 s
% 151.99/41.18 % (450947)Peak memory usage: 385 MB
% 151.99/41.18 % (450947)Instructions burned: 5499 (million)
% 151.99/41.18 % (450949)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4134517946:fmbsr=2:i=46332_2857 on theBenchmark for (2857ds/46332Mi)
% 151.99/41.18 % Detected minimum model sizes of [3]
% 151.99/41.18 % Detected maximum model sizes of [max]
% 151.99/41.18 % TRYING [15]
% 151.99/41.18 % (450943)Instruction limit reached!
% 151.99/41.18 % (450943)------------------------------
% 151.99/41.18 % (450943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450943)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450943)Termination reason: Instruction limit
% 151.99/41.18 % (450943)Termination phase: Saturation
% 151.99/41.18 % (450943)Time elapsed: 15.061 s
% 151.99/41.18 % (450943)Peak memory usage: 144 MB
% 151.99/41.18 % (450943)Instructions burned: 29340 (million)
% 151.99/41.18 % (450951)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=764316720:i=14071_2777 on theBenchmark for (2777ds/14071Mi)
% 151.99/41.18 % Detected minimum model sizes of [3]
% 151.99/41.18 % Detected maximum model sizes of [max]
% 151.99/41.18 % TRYING [12]
% 151.99/41.18 % (450931)Instruction limit reached!
% 151.99/41.18 % (450931)------------------------------
% 151.99/41.18 % (450931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450931)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450931)Termination reason: Instruction limit
% 151.99/41.18 % (450931)Termination phase: Finite model building constraint generation
% 151.99/41.18 % (450931)Time elapsed: 22.859 s
% 151.99/41.18 % (450931)Peak memory usage: 1734 MB
% 151.99/41.18 % (450931)Instructions burned: 54283 (million)
% 151.99/41.18 % (450953)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3974387689:i=22565:add=on:rawr=on_2749 on theBenchmark for (2749ds/22565Mi)
% 151.99/41.18 % (450951)Instruction limit reached!
% 151.99/41.18 % (450951)------------------------------
% 151.99/41.18 % (450951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450951)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450951)Termination reason: Instruction limit
% 151.99/41.18 % (450951)Termination phase: Finite model building constraint generation
% 151.99/41.18 % (450951)Time elapsed: 5.372 s
% 151.99/41.18 % (450951)Peak memory usage: 993 MB
% 151.99/41.18 % (450951)Instructions burned: 14072 (million)
% 151.99/41.18 % (450955)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1875465006:i=8173:av=off_2722 on theBenchmark for (2722ds/8173Mi)
% 151.99/41.18 % (450939)Instruction limit reached!
% 151.99/41.18 % (450939)------------------------------
% 151.99/41.18 % (450939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450939)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450939)Termination reason: Instruction limit
% 151.99/41.18 % (450939)Termination phase: Finite model building SAT solving
% 151.99/41.18 % (450939)Time elapsed: 21.957 s
% 151.99/41.18 % (450939)Peak memory usage: 2291 MB
% 151.99/41.18 % (450939)Instructions burned: 67535 (million)
% 151.99/41.18 % (450957)dis+10_16:1_sil=16000:random_seed=2967365498:i=9155:fsr=off_2714 on theBenchmark for (2714ds/9155Mi)
% 151.99/41.18 % (450949)Instruction limit reached!
% 151.99/41.18 % (450949)------------------------------
% 151.99/41.18 % (450949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450949)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450949)Termination reason: Instruction limit
% 151.99/41.18 % (450949)Termination phase: Finite model building constraint generation
% 151.99/41.18 % (450949)Time elapsed: 15.191 s
% 151.99/41.18 % (450949)Peak memory usage: 2084 MB
% 151.99/41.18 % (450949)Instructions burned: 46335 (million)
% 151.99/41.18 % (450959)ott-3_8_sil=64000:random_seed=2396148782:i=20139:bs=on_2702 on theBenchmark for (2702ds/20139Mi)
% 151.99/41.18 % (450957)Instruction limit reached!
% 151.99/41.18 % (450957)------------------------------
% 151.99/41.18 % (450957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450957)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450957)Termination reason: Instruction limit
% 151.99/41.18 % (450957)Termination phase: Saturation
% 151.99/41.18 % (450957)Time elapsed: 2.627 s
% 151.99/41.18 % (450957)Peak memory usage: 48 MB
% 151.99/41.18 % (450957)Instructions burned: 9157 (million)
% 151.99/41.18 % (450961)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4137129693:fmbsr=2:i=32576_2687 on theBenchmark for (2687ds/32576Mi)
% 151.99/41.18 % Detected minimum model sizes of [3]
% 151.99/41.18 % Detected maximum model sizes of [max]
% 151.99/41.18 % TRYING [9]
% 151.99/41.18 % (450955)Instruction limit reached!
% 151.99/41.18 % (450955)------------------------------
% 151.99/41.18 % (450955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450955)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450955)Termination reason: Instruction limit
% 151.99/41.18 % (450955)Termination phase: Saturation
% 151.99/41.18 % (450955)Time elapsed: 4.860 s
% 151.99/41.18 % (450955)Peak memory usage: 50 MB
% 151.99/41.18 % (450955)Instructions burned: 8174 (million)
% 151.99/41.18 % (450963)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2091586773:i=11404_2673 on theBenchmark for (2673ds/11404Mi)
% 151.99/41.18 % (450953)Instruction limit reached!
% 151.99/41.18 % (450953)------------------------------
% 151.99/41.18 % (450953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450953)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450953)Termination reason: Instruction limit
% 151.99/41.18 % (450953)Termination phase: Saturation
% 151.99/41.18 % (450953)Time elapsed: 11.493 s
% 151.99/41.18 % (450953)Peak memory usage: 89 MB
% 151.99/41.18 % (450953)Instructions burned: 22565 (million)
% 151.99/41.18 % (450965)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2648918853:i=14134_2633 on theBenchmark for (2633ds/14134Mi)
% 151.99/41.18 % (450961)Instruction limit reached!
% 151.99/41.18 % (450961)------------------------------
% 151.99/41.18 % (450961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450961)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450961)Termination reason: Instruction limit
% 151.99/41.18 % (450961)Termination phase: Finite model building constraint generation
% 151.99/41.18 % (450961)Time elapsed: 6.336 s
% 151.99/41.18 % (450961)Peak memory usage: 1635 MB
% 151.99/41.18 % (450961)Instructions burned: 32577 (million)
% 151.99/41.18 % (450967)dis+33_16_sil=32000:sac=on:random_seed=3025881907:i=15851:nm=0_2623 on theBenchmark for (2623ds/15851Mi)
% 151.99/41.18 % TRYING [8]
% 151.99/41.18 % (450963)Instruction limit reached!
% 151.99/41.18 % (450963)------------------------------
% 151.99/41.18 % (450963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.18 % (450963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.18 % (450963)CaDiCaL version: 2.1.3
% 151.99/41.18 % (450963)Termination reason: Instruction limit
% 151.99/41.18 % (450963)Termination phase: Saturation
% 151.99/41.18 % (450963)Time elapsed: 6.626 s
% 151.99/41.18 % (450963)Peak memory usage: 53 MB
% 151.99/41.18 % (450963)Instructions burned: 11404 (million)
% 151.99/41.18 % (450969)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=277844322:avsq=on:i=17627:add=on:amm=off_2606 on theBenchmark for (2606ds/17627Mi)
% 151.99/41.18 % (450967) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-450874-450967"...
% 151.99/41.18 % (450967)...printing done.
% 151.99/41.18 % (450967)Refutation found. Thanks to Tanya!
% 151.99/41.18 % SZS status Unsatisfiable for theBenchmark
% 151.99/41.18 % SZS output start Proof for theBenchmark
% See solution above
% 151.99/41.19 % (450967)------------------------------
% 151.99/41.19 % (450967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 151.99/41.19 % (450967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.99/41.19 % (450967)CaDiCaL version: 2.1.3
% 151.99/41.19 % (450967)Termination reason: Refutation
% 151.99/41.19 % (450967)Time elapsed: 2.633 s
% 151.99/41.19 % (450967)Peak memory usage: 63 MB
% 151.99/41.19 % (450967)Instructions burned: 8391 (million)
% 151.99/41.19 % (450874)Success in time 40.757 s
% 151.99/41.19 % Vampire exiting
%------------------------------------------------------------------------------