%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : AGT006+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:06:32 AM UTC 2026
% Result : Theorem 8.90s 2.17s
% Output : Refutation 11.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 31
% Syntax : Number of formulae : 138 ( 55 unt; 5 def)
% Number of atoms : 341 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 359 ( 156 ~; 151 |; 39 &)
% ( 8 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 6 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-2 aty)
% Number of variables : 105 ( 0 sgn 105 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2,X3] :
( accept_team(X0,X3,X1,X2)
<=> ( accept_city(X0,X1)
& accept_leader(X0,X3)
& accept_number(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_1) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( accept_population(X0,X3,X1)
& less(X2,X1) )
=> accept_population(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_3) ).
fof(f8,axiom,
! [X0] :
( ( accept_population(X0,atheist,n65)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n7)
& accept_population(X0,native,n4)
& accept_population(X0,other,n4) )
<=> accept_city(X0,suffertown) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_1) ).
fof(f14,axiom,
! [X0] :
( ( accept_population(X0,atheist,n12)
& accept_population(X0,christian,n3)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n85)
& accept_population(X0,other,n0) )
<=> accept_city(X0,coastvillage) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_7) ).
fof(f311,axiom,
accept_city(countrybcivilorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_42) ).
fof(f313,axiom,
accept_population(countrybcivilorganization,other,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_44) ).
fof(f314,axiom,
accept_population(countrybcivilorganization,muslim,n65),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_45) ).
fof(f320,axiom,
accept_population(countrybcivilorganization,christian,n20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_51) ).
fof(f561,axiom,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_292) ).
fof(f568,axiom,
accept_population(countrybcivilorganization,atheist,n75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_299) ).
fof(f596,axiom,
accept_number(countrybcivilorganization,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_327) ).
fof(f641,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn4) ).
fof(f642,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn5) ).
fof(f644,axiom,
rdn_translate(n7,rdn_pos(rdnn(n7))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn7) ).
fof(f702,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn65) ).
fof(f712,axiom,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn75) ).
fof(f722,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn85) ).
fof(f898,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit6) ).
fof(f900,axiom,
rdn_non_zero_digit(rdnn(n8)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit8) ).
fof(f906,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less45) ).
fof(f908,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less67) ).
fof(f912,axiom,
! [X0,X1,X2,X3] :
( rdn_positive_less(X1,X3)
=> rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less_multi_digit_high) ).
fof(f914,axiom,
! [X0,X1,X2] :
( rdn_non_zero(X2)
=> rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_extra_digits_positive_less) ).
fof(f915,axiom,
! [X0] :
( rdn_non_zero_digit(rdnn(X0))
=> rdn_non_zero(rdnn(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_non_zero_by_digit) ).
fof(f917,axiom,
! [X0,X1,X2,X3] :
( ( rdn_translate(X0,rdn_pos(X2))
& rdn_translate(X1,rdn_pos(X3))
& rdn_positive_less(X2,X3) )
=> less(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_entry_point_pos_pos) ).
fof(f923,conjecture,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_6) ).
fof(f924,negated_conjecture,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(negated_conjecture,[status(cth)],[f923]) ).
fof(f925,plain,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(flattening,[],[f924]) ).
fof(f932,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(ennf_transformation,[],[f3]) ).
fof(f933,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(flattening,[],[f932]) ).
fof(f940,plain,
! [X0,X1,X2,X3] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3))
| ~ rdn_positive_less(X1,X3) ),
inference(ennf_transformation,[],[f912]) ).
fof(f943,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2) ),
inference(ennf_transformation,[],[f914]) ).
fof(f944,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(ennf_transformation,[],[f915]) ).
fof(f946,plain,
! [X0,X1,X2,X3] :
( less(X0,X1)
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_positive_less(X2,X3) ),
inference(ennf_transformation,[],[f917]) ).
fof(f947,plain,
! [X0,X1,X2,X3] :
( less(X0,X1)
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_positive_less(X2,X3) ),
inference(flattening,[],[f946]) ).
fof(f952,plain,
! [X0,X1,X2,X3] :
( ( accept_team(X0,X3,X1,X2)
| ~ accept_city(X0,X1)
| ~ accept_leader(X0,X3)
| ~ accept_number(X0,X2) )
& ( ( accept_city(X0,X1)
& accept_leader(X0,X3)
& accept_number(X0,X2) )
| ~ accept_team(X0,X3,X1,X2) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f953,plain,
! [X0,X1,X2,X3] :
( ( accept_team(X0,X3,X1,X2)
| ~ accept_city(X0,X1)
| ~ accept_leader(X0,X3)
| ~ accept_number(X0,X2) )
& ( ( accept_city(X0,X1)
& accept_leader(X0,X3)
& accept_number(X0,X2) )
| ~ accept_team(X0,X3,X1,X2) ) ),
inference(flattening,[],[f952]) ).
fof(f954,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n65)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n7)
& accept_population(X0,native,n4)
& accept_population(X0,other,n4) )
| ~ accept_city(X0,suffertown) )
& ( accept_city(X0,suffertown)
| ~ accept_population(X0,atheist,n65)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n7)
| ~ accept_population(X0,native,n4)
| ~ accept_population(X0,other,n4) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f955,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n65)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n7)
& accept_population(X0,native,n4)
& accept_population(X0,other,n4) )
| ~ accept_city(X0,suffertown) )
& ( accept_city(X0,suffertown)
| ~ accept_population(X0,atheist,n65)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n7)
| ~ accept_population(X0,native,n4)
| ~ accept_population(X0,other,n4) ) ),
inference(flattening,[],[f954]) ).
fof(f966,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n12)
& accept_population(X0,christian,n3)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n85)
& accept_population(X0,other,n0) )
| ~ accept_city(X0,coastvillage) )
& ( accept_city(X0,coastvillage)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,other,n0) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f967,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n12)
& accept_population(X0,christian,n3)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n85)
& accept_population(X0,other,n0) )
| ~ accept_city(X0,coastvillage) )
& ( accept_city(X0,coastvillage)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,other,n0) ) ),
inference(flattening,[],[f966]) ).
fof(f985,plain,
! [X2,X3,X0,X1] :
( accept_team(X0,X3,X1,X2)
| ~ accept_city(X0,X1)
| ~ accept_leader(X0,X3)
| ~ accept_number(X0,X2) ),
inference(cnf_transformation,[],[f953]) ).
fof(f987,plain,
! [X2,X3,X0,X1] :
( ~ accept_population(X0,X3,X1)
| accept_population(X0,X3,X2)
| ~ less(X2,X1) ),
inference(cnf_transformation,[],[f933]) ).
fof(f992,plain,
! [X0] :
( ~ accept_population(X0,other,n4)
| ~ accept_population(X0,atheist,n65)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n7)
| ~ accept_population(X0,native,n4)
| accept_city(X0,suffertown) ),
inference(cnf_transformation,[],[f955]) ).
fof(f1030,plain,
! [X0] :
( accept_population(X0,native,n85)
| ~ accept_city(X0,coastvillage) ),
inference(cnf_transformation,[],[f967]) ).
fof(f1360,plain,
accept_city(countrybcivilorganization,coastvillage),
inference(cnf_transformation,[],[f311]) ).
fof(f1362,plain,
accept_population(countrybcivilorganization,other,n5),
inference(cnf_transformation,[],[f313]) ).
fof(f1363,plain,
accept_population(countrybcivilorganization,muslim,n65),
inference(cnf_transformation,[],[f314]) ).
fof(f1369,plain,
accept_population(countrybcivilorganization,christian,n20),
inference(cnf_transformation,[],[f320]) ).
fof(f1610,plain,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization),
inference(cnf_transformation,[],[f561]) ).
fof(f1617,plain,
accept_population(countrybcivilorganization,atheist,n75),
inference(cnf_transformation,[],[f568]) ).
fof(f1645,plain,
accept_number(countrybcivilorganization,n4),
inference(cnf_transformation,[],[f596]) ).
fof(f1690,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(cnf_transformation,[],[f641]) ).
fof(f1691,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(cnf_transformation,[],[f642]) ).
fof(f1693,plain,
rdn_translate(n7,rdn_pos(rdnn(n7))),
inference(cnf_transformation,[],[f644]) ).
fof(f1751,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(cnf_transformation,[],[f702]) ).
fof(f1761,plain,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
inference(cnf_transformation,[],[f712]) ).
fof(f1771,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(cnf_transformation,[],[f722]) ).
fof(f1947,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(cnf_transformation,[],[f898]) ).
fof(f1949,plain,
rdn_non_zero_digit(rdnn(n8)),
inference(cnf_transformation,[],[f900]) ).
fof(f1955,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f906]) ).
fof(f1957,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(cnf_transformation,[],[f908]) ).
fof(f1961,plain,
! [X2,X3,X0,X1] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3))
| ~ rdn_positive_less(X1,X3) ),
inference(cnf_transformation,[],[f940]) ).
fof(f1963,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2) ),
inference(cnf_transformation,[],[f943]) ).
fof(f1964,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(X0))
| rdn_non_zero(rdnn(X0)) ),
inference(cnf_transformation,[],[f944]) ).
fof(f1966,plain,
! [X2,X3,X0,X1] :
( ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| less(X0,X1)
| ~ rdn_positive_less(X2,X3) ),
inference(cnf_transformation,[],[f947]) ).
fof(f1972,plain,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(cnf_transformation,[],[f925]) ).
fof(f1974,plain,
( ~ accept_city(countrybcivilorganization,suffertown)
| ~ accept_leader(countrybcivilorganization,countrybhumanitarianorganization)
| ~ accept_number(countrybcivilorganization,n4) ),
inference(resolution,[],[f985,f1972]) ).
fof(f1975,plain,
( ~ accept_city(countrybcivilorganization,suffertown)
| ~ accept_number(countrybcivilorganization,n4) ),
inference(forward_subsumption_resolution,[],[f1974,f1610]) ).
fof(f1976,plain,
~ accept_city(countrybcivilorganization,suffertown),
inference(forward_subsumption_resolution,[],[f1975,f1645]) ).
fof(f1980,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n5),rdnn(n6)))
| less(X0,n65)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1966,f1751]) ).
fof(f1992,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdnn(n5))
| less(X0,n5)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1691,f1966]) ).
fof(f2001,definition,
( spl0_1
<=> rdn_non_zero(rdnn(n6)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f2002,plain,
( rdn_non_zero(rdnn(n6))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2003,plain,
( ~ rdn_non_zero(rdnn(n6))
| spl0_1 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2012,plain,
! [X0,X1] :
( ~ rdn_non_zero(rdnn(n6))
| less(X0,n65)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1))) ),
inference(resolution,[],[f1963,f1980]) ).
fof(f2035,plain,
rdn_non_zero(rdnn(n8)),
inference(resolution,[],[f1949,f1964]) ).
fof(f2094,plain,
rdn_non_zero(rdnn(n6)),
inference(resolution,[],[f1947,f1964]) ).
fof(f2095,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f2094,f2003]) ).
fof(f2096,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f2095]) ).
fof(f2097,plain,
( ! [X0,X1] :
( ~ rdn_translate(X0,rdn_pos(rdnn(X1)))
| less(X0,n65) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2012,f2002]) ).
fof(f2100,plain,
( less(n7,n65)
| ~ spl0_1 ),
inference(resolution,[],[f2097,f1693]) ).
fof(f2139,plain,
! [X0] :
( accept_population(countrybcivilorganization,muslim,X0)
| ~ less(X0,n65) ),
inference(resolution,[],[f987,f1363]) ).
fof(f2154,definition,
( spl0_11
<=> accept_population(countrybcivilorganization,muslim,n7) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f2155,plain,
( accept_population(countrybcivilorganization,muslim,n7)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f2154]) ).
fof(f2156,plain,
( ~ accept_population(countrybcivilorganization,muslim,n7)
| spl0_11 ),
inference(avatar_component_clause,[],[f2154]) ).
fof(f2158,definition,
( spl0_12
<=> accept_population(countrybcivilorganization,atheist,n65) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f2159,plain,
( accept_population(countrybcivilorganization,atheist,n65)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f2158]) ).
fof(f2160,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| spl0_12 ),
inference(avatar_component_clause,[],[f2158]) ).
fof(f2169,plain,
! [X0] :
( accept_population(countrybcivilorganization,other,X0)
| ~ less(X0,n5) ),
inference(resolution,[],[f1362,f987]) ).
fof(f2170,plain,
( ~ less(n4,n5)
| ~ accept_population(countrybcivilorganization,atheist,n65)
| ~ accept_population(countrybcivilorganization,christian,n20)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown) ),
inference(resolution,[],[f2169,f992]) ).
fof(f2217,plain,
( ~ less(n7,n65)
| spl0_11 ),
inference(resolution,[],[f2139,f2156]) ).
fof(f2219,plain,
( $false
| ~ spl0_1
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f2217,f2100]) ).
fof(f2220,plain,
( ~ spl0_1
| spl0_11 ),
inference(avatar_contradiction_clause,[],[f2219]) ).
fof(f2228,plain,
! [X0] :
( accept_population(countrybcivilorganization,atheist,X0)
| ~ less(X0,n75) ),
inference(resolution,[],[f1617,f987]) ).
fof(f2229,plain,
( ~ less(n65,n75)
| spl0_12 ),
inference(resolution,[],[f2228,f2160]) ).
fof(f2301,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n5),rdnn(n7)))
| less(X0,n75)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1761,f1966]) ).
fof(f2331,plain,
! [X2,X0,X1] :
( ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2)))
| less(X0,n75)
| ~ rdn_positive_less(X2,rdnn(n7)) ),
inference(resolution,[],[f2301,f1961]) ).
fof(f2363,plain,
! [X0] :
( ~ rdn_translate(X0,rdn_pos(rdnn(n4)))
| less(X0,n5) ),
inference(resolution,[],[f1992,f1955]) ).
fof(f2373,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n5),rdnn(n8)))
| less(X0,n85)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1771,f1966]) ).
fof(f2401,plain,
! [X0,X1] :
( less(X0,n85)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1)))
| ~ rdn_non_zero(rdnn(n8)) ),
inference(resolution,[],[f2373,f1963]) ).
fof(f2405,plain,
! [X0,X1] :
( ~ rdn_translate(X0,rdn_pos(rdnn(X1)))
| less(X0,n85) ),
inference(forward_subsumption_resolution,[],[f2401,f2035]) ).
fof(f2407,plain,
less(n4,n85),
inference(resolution,[],[f2405,f1690]) ).
fof(f2558,definition,
( spl0_42
<=> less(n4,n5) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f2559,plain,
( less(n4,n5)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2560,plain,
( ~ less(n4,n5)
| spl0_42 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2579,plain,
! [X0,X1] :
( accept_population(X0,native,X1)
| ~ accept_city(X0,coastvillage)
| ~ less(X1,n85) ),
inference(resolution,[],[f1030,f987]) ).
fof(f2776,plain,
( less(n65,n75)
| ~ rdn_positive_less(rdnn(n6),rdnn(n7)) ),
inference(resolution,[],[f2331,f1751]) ).
fof(f2821,plain,
( ~ rdn_positive_less(rdnn(n6),rdnn(n7))
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f2776,f2229]) ).
fof(f2823,plain,
( $false
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f2821,f1957]) ).
fof(f2824,plain,
spl0_12,
inference(avatar_contradiction_clause,[],[f2823]) ).
fof(f2831,definition,
( spl0_73
<=> accept_population(countrybcivilorganization,native,n4) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f2832,plain,
( accept_population(countrybcivilorganization,native,n4)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f2831]) ).
fof(f2833,plain,
( ~ accept_population(countrybcivilorganization,native,n4)
| spl0_73 ),
inference(avatar_component_clause,[],[f2831]) ).
fof(f2842,plain,
( ~ accept_city(countrybcivilorganization,coastvillage)
| ~ less(n4,n85)
| spl0_73 ),
inference(resolution,[],[f2833,f2579]) ).
fof(f2845,plain,
( ~ less(n4,n85)
| spl0_73 ),
inference(forward_subsumption_resolution,[],[f2842,f1360]) ).
fof(f2848,plain,
( $false
| spl0_73 ),
inference(forward_subsumption_resolution,[],[f2845,f2407]) ).
fof(f2849,plain,
spl0_73,
inference(avatar_contradiction_clause,[],[f2848]) ).
fof(f4513,plain,
less(n4,n5),
inference(resolution,[],[f2363,f1690]) ).
fof(f4514,plain,
( $false
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f4513,f2560]) ).
fof(f4515,plain,
spl0_42,
inference(avatar_contradiction_clause,[],[f4514]) ).
fof(f4516,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| ~ accept_population(countrybcivilorganization,christian,n20)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown)
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f2170,f2559]) ).
fof(f4521,plain,
( ~ accept_population(countrybcivilorganization,christian,n20)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown)
| ~ spl0_12
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f4516,f2159]) ).
fof(f4526,plain,
( ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown)
| ~ spl0_12
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f4521,f1369]) ).
fof(f4575,plain,
( ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f4526,f2155]) ).
fof(f4581,plain,
( accept_city(countrybcivilorganization,suffertown)
| ~ spl0_11
| ~ spl0_12
| ~ spl0_42
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f4575,f2832]) ).
fof(f4582,plain,
( $false
| ~ spl0_11
| ~ spl0_12
| ~ spl0_42
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f4581,f1976]) ).
fof(f4583,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_42
| ~ spl0_73 ),
inference(avatar_contradiction_clause,[],[f4582]) ).
cnf(s5,plain,
spl0_1,
inference(sat_conversion,[],[f2096]) ).
cnf(s10,plain,
( ~ spl0_1
| spl0_11 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s49,plain,
spl0_12,
inference(sat_conversion,[],[f2824]) ).
cnf(s52,plain,
spl0_73,
inference(sat_conversion,[],[f2849]) ).
cnf(s107,plain,
spl0_42,
inference(sat_conversion,[],[f4515]) ).
cnf(s112,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_42
| ~ spl0_73 ),
inference(sat_conversion,[],[f4583]) ).
cnf(s129,plain,
~ spl0_11,
inference(rat,[],[s112,s52,s107,s49]) ).
cnf(s139,plain,
~ spl0_1,
inference(rat,[],[s10,s129]) ).
cnf(s140,plain,
$false,
inference(rat,[],[s5,s139]) ).
fof(f4584,plain,
$false,
inference(avatar_sat_refutation,[],[s140]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT006+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:08:37 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 7.49/1.91 % (666090)Detected formulas, will run a generic FOF schedule.
% 7.49/1.91 % (666096)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2867151923:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.49/1.91 % (666100)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2904132157:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.49/1.91 % (666098)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1525513005:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.49/1.91 % (666101)dis-21_1_sil=8000:lcm=predicate:random_seed=3681275240:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 7.49/1.91 % (666099)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1455223681:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.49/1.91 % (666097)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4034369311:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.49/1.91 % (666095)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=2923113243:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.49/1.91 % (666098)Refutation not found, incomplete strategy
% 7.49/1.91 % (666098)------------------------------
% 7.49/1.91 % (666098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.49/1.91 % (666098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.91 % (666098)CaDiCaL version: 2.1.3
% 7.49/1.91 % (666098)Termination reason: Refutation not found, incomplete strategy
% 7.49/1.91 % (666098)Time elapsed: 0.002 s
% 7.49/1.91 % (666098)Peak memory usage: 88 MB
% 7.49/1.91 % (666098)Instructions burned: 3 (million)
% 7.49/1.91 % (666099)Refutation not found, incomplete strategy
% 7.49/1.91 % (666099)------------------------------
% 7.49/1.91 % (666099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.49/1.91 % (666099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.91 % (666099)CaDiCaL version: 2.1.3
% 7.49/1.91 % (666099)Termination reason: Refutation not found, incomplete strategy
% 7.49/1.91 % (666099)Time elapsed: 0.009 s
% 7.49/1.91 % (666099)Peak memory usage: 88 MB
% 7.49/1.91 % (666099)Instructions burned: 16 (million)
% 7.49/1.91 % (666101)Instruction limit reached!
% 7.49/1.91 % (666101)------------------------------
% 7.49/1.91 % (666101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.49/1.91 % (666101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.91 % (666101)CaDiCaL version: 2.1.3
% 7.49/1.91 % (666101)Termination reason: Instruction limit
% 7.49/1.91 % (666101)Termination phase: Saturation
% 7.49/1.91 % (666101)Time elapsed: 0.061 s
% 7.49/1.91 % (666101)Peak memory usage: 90 MB
% 7.49/1.91 % (666101)Instructions burned: 129 (million)
% 7.49/1.91 % (666100)Instruction limit reached!
% 7.49/1.91 % (666100)------------------------------
% 7.49/1.91 % (666100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.49/1.91 % (666100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.91 % (666100)CaDiCaL version: 2.1.3
% 7.49/1.91 % (666100)Termination reason: Instruction limit
% 7.49/1.91 % (666100)Termination phase: Saturation
% 7.49/1.91 % (666100)Time elapsed: 0.084 s
% 7.49/1.91 % (666100)Peak memory usage: 90 MB
% 7.49/1.91 % (666100)Instructions burned: 140 (million)
% 7.49/1.91 % (666109)lrs+10_1_sil=8000:sp=occurrence:random_seed=924449505:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.49/1.91 % (666109)Refutation not found, incomplete strategy
% 7.49/1.91 % (666109)------------------------------
% 7.49/1.91 % (666109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.49/1.91 % (666109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.49/1.91 % (666109)CaDiCaL version: 2.1.3
% 7.49/1.91 % (666109)Termination reason: Refutation not found, incomplete strategy
% 7.49/1.91 % (666109)Time elapsed: 0.009 s
% 7.49/1.91 % (666109)Peak memory usage: 88 MB
% 7.49/1.91 % (666109)Instructions burned: 15 (million)
% 7.49/1.91 % (666098)------------------------------
% 7.49/1.91 % (666098)------------------------------
% 8.90/2.17 % (666099)------------------------------
% 8.90/2.17 % (666099)------------------------------
% 8.90/2.17 % (666110)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3613423195:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.90/2.17 % (666110)Refutation not found, incomplete strategy
% 8.90/2.17 % (666110)------------------------------
% 8.90/2.17 % (666110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666110)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666110)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666110)Time elapsed: 0.005 s
% 8.90/2.17 % (666110)Peak memory usage: 88 MB
% 8.90/2.17 % (666110)Instructions burned: 8 (million)
% 8.90/2.17 % (666112)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2557874776:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 8.90/2.17 % (666112)Refutation not found, incomplete strategy
% 8.90/2.17 % (666112)------------------------------
% 8.90/2.17 % (666112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666112)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666112)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666112)Time elapsed: 0.003 s
% 8.90/2.17 % (666112)Peak memory usage: 88 MB
% 8.90/2.17 % (666112)Instructions burned: 3 (million)
% 8.90/2.17 % (666114)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1740477428:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.90/2.17 % (666109)------------------------------
% 8.90/2.17 % (666109)------------------------------
% 8.90/2.17 % (666096)Refutation not found, incomplete strategy
% 8.90/2.17 % (666096)------------------------------
% 8.90/2.17 % (666096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666096)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666096)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666096)Time elapsed: 0.515 s
% 8.90/2.17 % (666096)Peak memory usage: 132 MB
% 8.90/2.17 % (666096)Instructions burned: 1309 (million)
% 8.90/2.17 % (666110)------------------------------
% 8.90/2.17 % (666110)------------------------------
% 8.90/2.17 % (666114)Instruction limit reached!
% 8.90/2.17 % (666114)------------------------------
% 8.90/2.17 % (666114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666114)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666114)Termination reason: Instruction limit
% 8.90/2.17 % (666114)Termination phase: Saturation
% 8.90/2.17 % (666114)Time elapsed: 0.126 s
% 8.90/2.17 % (666114)Peak memory usage: 92 MB
% 8.90/2.17 % (666114)Instructions burned: 250 (million)
% 8.90/2.17 % (666097)Refutation not found, incomplete strategy
% 8.90/2.17 % (666097)------------------------------
% 8.90/2.17 % (666097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666097)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666097)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666097)Time elapsed: 0.594 s
% 8.90/2.17 % (666097)Peak memory usage: 129 MB
% 8.90/2.17 % (666097)Instructions burned: 896 (million)
% 8.90/2.17 % (666096)------------------------------
% 8.90/2.17 % (666096)------------------------------
% 8.90/2.17 % (666117)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1150082626:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 8.90/2.17 % (666117)Refutation not found, incomplete strategy
% 8.90/2.17 % (666117)------------------------------
% 8.90/2.17 % (666117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666117)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666117)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666117)Time elapsed: 0.007 s
% 8.90/2.17 % (666117)Peak memory usage: 88 MB
% 8.90/2.17 % (666117)Instructions burned: 12 (million)
% 8.90/2.17 % (666112)------------------------------
% 8.90/2.17 % (666112)------------------------------
% 8.90/2.17 % (666118)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4249978149:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.90/2.17 % (666119)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=171023752:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 8.90/2.17 % (666119)Refutation not found, incomplete strategy
% 8.90/2.17 % (666119)------------------------------
% 8.90/2.17 % (666119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666119)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666119)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666119)Time elapsed: 0.007 s
% 8.90/2.17 % (666119)Peak memory usage: 89 MB
% 8.90/2.17 % (666119)Instructions burned: 10 (million)
% 8.90/2.17 % (666121)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=868870104:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 8.90/2.17 % (666121)Instruction limit reached!
% 8.90/2.17 % (666121)------------------------------
% 8.90/2.17 % (666121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666121)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666121)Termination reason: Instruction limit
% 8.90/2.17 % (666121)Termination phase: Saturation
% 8.90/2.17 % (666121)Time elapsed: 0.033 s
% 8.90/2.17 % (666121)Peak memory usage: 89 MB
% 8.90/2.17 % (666121)Instructions burned: 131 (million)
% 8.90/2.17 % (666122)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=102288989:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.90/2.17 % (666122)Refutation not found, incomplete strategy
% 8.90/2.17 % (666122)------------------------------
% 8.90/2.17 % (666122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666122)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666122)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666122)Time elapsed: 0.026 s
% 8.90/2.17 % (666122)Peak memory usage: 89 MB
% 8.90/2.17 % (666122)Instructions burned: 44 (million)
% 8.90/2.17 % (666097)------------------------------
% 8.90/2.17 % (666097)------------------------------
% 8.90/2.17 % (666117)------------------------------
% 8.90/2.17 % (666117)------------------------------
% 8.90/2.17 % (666126)lrs+10_1_sil=8000:sp=occurrence:random_seed=348552240:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 8.90/2.17 % (666126)Refutation not found, incomplete strategy
% 8.90/2.17 % (666126)------------------------------
% 8.90/2.17 % (666126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666126)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666126)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666126)Time elapsed: 0.006 s
% 8.90/2.17 % (666126)Peak memory usage: 88 MB
% 8.90/2.17 % (666126)Instructions burned: 19 (million)
% 8.90/2.17 % (666119)------------------------------
% 8.90/2.17 % (666119)------------------------------
% 8.90/2.17 % (666128)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=280863520:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 8.90/2.17 % (666128)Refutation not found, incomplete strategy
% 8.90/2.17 % (666128)------------------------------
% 8.90/2.17 % (666128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666128)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666128)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666128)Time elapsed: 0.003 s
% 8.90/2.17 % (666128)Peak memory usage: 88 MB
% 8.90/2.17 % (666128)Instructions burned: 3 (million)
% 8.90/2.17 % (666095)First to succeed.
% 8.90/2.17 % (666095)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-666090"
% 8.90/2.17 % (666129)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1597262496:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 8.90/2.17 % (666126)------------------------------
% 8.90/2.17 % (666126)------------------------------
% 8.90/2.17 % (666122)------------------------------
% 8.90/2.17 % (666122)------------------------------
% 8.90/2.17 % (666131)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1376741854:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 8.90/2.17 % (666131)Refutation not found, incomplete strategy
% 8.90/2.17 % (666131)------------------------------
% 8.90/2.17 % (666131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666131)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666131)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666131)Time elapsed: 0.044 s
% 8.90/2.17 % (666131)Peak memory usage: 90 MB
% 8.90/2.17 % (666131)Instructions burned: 89 (million)
% 8.90/2.17 % (666134)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2996600826:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 8.90/2.17 % (666134)Refutation not found, incomplete strategy
% 8.90/2.17 % (666134)------------------------------
% 8.90/2.17 % (666134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.90/2.17 % (666134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.90/2.17 % (666134)CaDiCaL version: 2.1.3
% 8.90/2.17 % (666134)Termination reason: Refutation not found, incomplete strategy
% 8.90/2.17 % (666134)Time elapsed: 0.006 s
% 8.90/2.17 % (666134)Peak memory usage: 88 MB
% 8.90/2.17 % (666134)Instructions burned: 20 (million)
% 8.90/2.17 % (666128)------------------------------
% 8.90/2.17 % (666128)------------------------------
% 8.90/2.17 % (666135)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3822366682:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 8.90/2.17 % (666095)Refutation found. Thanks to Tanya!
% 8.90/2.17 % SZS status Theorem for theBenchmark
% 8.90/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 11.07/2.36 % (666095)------------------------------
% 11.07/2.36 % (666095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.07/2.36 % (666095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.07/2.36 % (666095)CaDiCaL version: 2.1.3
% 11.07/2.36 % (666095)Termination reason: Refutation
% 11.07/2.36 % (666095)Time elapsed: 1.030 s
% 11.07/2.36 % (666095)Peak memory usage: 138 MB
% 11.07/2.36 % (666095)Instructions burned: 1529 (million)
% 11.07/2.36 % (666095)------------------------------
% 11.07/2.36 % (666095)------------------------------
% 11.07/2.36 % (666090)Success in time 1.497 s
% 11.07/2.36 % Vampire exiting
%------------------------------------------------------------------------------