%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : AGT007+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 : n009.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:33 AM UTC 2026
% Result : Theorem 10.47s 2.17s
% Output : Refutation 11.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 39
% Syntax : Number of formulae : 165 ( 76 unt; 7 def)
% Number of atoms : 344 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 323 ( 144 ~; 137 |; 27 &)
% ( 9 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 8 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-2 aty)
% Number of variables : 114 ( 0 sgn 114 !; 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(f18,axiom,
! [X0] :
( ( accept_population(X0,atheist,n70)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n8)
& accept_population(X0,native,n0)
& accept_population(X0,other,n2) )
<=> accept_city(X0,townb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_11) ).
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(f321,axiom,
accept_population(countrybcivilorganization,atheist,n78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_52) ).
fof(f561,axiom,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_292) ).
fof(f565,axiom,
accept_population(countrybcivilorganization,native,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_296) ).
fof(f597,axiom,
accept_number(countrybcivilorganization,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_328) ).
fof(f639,axiom,
rdn_translate(n2,rdn_pos(rdnn(n2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn2) ).
fof(f642,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn5) ).
fof(f645,axiom,
rdn_translate(n8,rdn_pos(rdnn(n8))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn8) ).
fof(f702,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn65) ).
fof(f707,axiom,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn70) ).
fof(f715,axiom,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn78) ).
fof(f898,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit6) ).
fof(f899,axiom,
rdn_non_zero_digit(rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit7) ).
fof(f902,axiom,
rdn_positive_less(rdnn(n0),rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less01) ).
fof(f903,axiom,
rdn_positive_less(rdnn(n1),rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less12) ).
fof(f904,axiom,
rdn_positive_less(rdnn(n2),rdnn(n3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less23) ).
fof(f905,axiom,
rdn_positive_less(rdnn(n3),rdnn(n4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less34) ).
fof(f906,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less45) ).
fof(f907,axiom,
rdn_positive_less(rdnn(n5),rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less56) ).
fof(f908,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less67) ).
fof(f909,axiom,
rdn_positive_less(rdnn(n7),rdnn(n8)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less78) ).
fof(f911,axiom,
! [X0,X1,X2] :
( ( rdn_positive_less(rdnn(X0),rdnn(X1))
& rdn_positive_less(rdnn(X1),rdnn(X2)) )
=> rdn_positive_less(rdnn(X0),rdnn(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less_transitivity) ).
fof(f913,axiom,
! [X0,X1,X2] :
( ( rdn_positive_less(rdnn(X0),rdnn(X2))
& rdn_non_zero(X1) )
=> rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_positive_less_multi_digit_low) ).
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,townb,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_7) ).
fof(f924,negated_conjecture,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,townb,n3),
inference(negated_conjecture,[status(cth)],[f923]) ).
fof(f925,plain,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,townb,n3),
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(f938,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2)) ),
inference(ennf_transformation,[],[f911]) ).
fof(f939,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2)) ),
inference(flattening,[],[f938]) ).
fof(f941,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(ennf_transformation,[],[f913]) ).
fof(f942,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(flattening,[],[f941]) ).
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(f974,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n70)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n8)
& accept_population(X0,native,n0)
& accept_population(X0,other,n2) )
| ~ accept_city(X0,townb) )
& ( accept_city(X0,townb)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n2) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f975,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n70)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n8)
& accept_population(X0,native,n0)
& accept_population(X0,other,n2) )
| ~ accept_city(X0,townb) )
& ( accept_city(X0,townb)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n2) ) ),
inference(flattening,[],[f974]) ).
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(f1052,plain,
! [X0] :
( ~ accept_population(X0,other,n2)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,native,n0)
| accept_city(X0,townb) ),
inference(cnf_transformation,[],[f975]) ).
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(f1370,plain,
accept_population(countrybcivilorganization,atheist,n78),
inference(cnf_transformation,[],[f321]) ).
fof(f1610,plain,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization),
inference(cnf_transformation,[],[f561]) ).
fof(f1614,plain,
accept_population(countrybcivilorganization,native,n0),
inference(cnf_transformation,[],[f565]) ).
fof(f1646,plain,
accept_number(countrybcivilorganization,n3),
inference(cnf_transformation,[],[f597]) ).
fof(f1688,plain,
rdn_translate(n2,rdn_pos(rdnn(n2))),
inference(cnf_transformation,[],[f639]) ).
fof(f1691,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(cnf_transformation,[],[f642]) ).
fof(f1694,plain,
rdn_translate(n8,rdn_pos(rdnn(n8))),
inference(cnf_transformation,[],[f645]) ).
fof(f1751,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(cnf_transformation,[],[f702]) ).
fof(f1756,plain,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
inference(cnf_transformation,[],[f707]) ).
fof(f1764,plain,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
inference(cnf_transformation,[],[f715]) ).
fof(f1947,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(cnf_transformation,[],[f898]) ).
fof(f1948,plain,
rdn_non_zero_digit(rdnn(n7)),
inference(cnf_transformation,[],[f899]) ).
fof(f1951,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(cnf_transformation,[],[f902]) ).
fof(f1952,plain,
rdn_positive_less(rdnn(n1),rdnn(n2)),
inference(cnf_transformation,[],[f903]) ).
fof(f1953,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(cnf_transformation,[],[f904]) ).
fof(f1954,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(cnf_transformation,[],[f905]) ).
fof(f1955,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f906]) ).
fof(f1956,plain,
rdn_positive_less(rdnn(n5),rdnn(n6)),
inference(cnf_transformation,[],[f907]) ).
fof(f1957,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(cnf_transformation,[],[f908]) ).
fof(f1958,plain,
rdn_positive_less(rdnn(n7),rdnn(n8)),
inference(cnf_transformation,[],[f909]) ).
fof(f1960,plain,
! [X2,X0,X1] :
( ~ rdn_positive_less(rdnn(X1),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| rdn_positive_less(rdnn(X0),rdnn(X2)) ),
inference(cnf_transformation,[],[f939]) ).
fof(f1962,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(cnf_transformation,[],[f942]) ).
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,townb,n3),
inference(cnf_transformation,[],[f925]) ).
fof(f1974,plain,
( ~ accept_city(countrybcivilorganization,townb)
| ~ accept_leader(countrybcivilorganization,countrybhumanitarianorganization)
| ~ accept_number(countrybcivilorganization,n3) ),
inference(resolution,[],[f985,f1972]) ).
fof(f1975,plain,
( ~ accept_city(countrybcivilorganization,townb)
| ~ accept_number(countrybcivilorganization,n3) ),
inference(forward_subsumption_resolution,[],[f1974,f1610]) ).
fof(f1976,plain,
~ accept_city(countrybcivilorganization,townb),
inference(forward_subsumption_resolution,[],[f1975,f1646]) ).
fof(f1988,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdnn(n5))
| less(X0,n5)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1691,f1966]) ).
fof(f1999,definition,
( spl0_1
<=> rdn_non_zero(rdnn(n7)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f2000,plain,
( rdn_non_zero(rdnn(n7))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f1999]) ).
fof(f2001,plain,
( ~ rdn_non_zero(rdnn(n7))
| spl0_1 ),
inference(avatar_component_clause,[],[f1999]) ).
fof(f2018,plain,
rdn_non_zero(rdnn(n7)),
inference(resolution,[],[f1948,f1964]) ).
fof(f2019,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f2018,f2001]) ).
fof(f2020,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f2019]) ).
fof(f2027,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n7))
| rdn_positive_less(rdnn(X0),rdnn(n8)) ),
inference(resolution,[],[f1960,f1958]) ).
fof(f2028,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n4))
| rdn_positive_less(rdnn(X0),rdnn(n5)) ),
inference(resolution,[],[f1960,f1955]) ).
fof(f2029,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n3))
| rdn_positive_less(rdnn(X0),rdnn(n4)) ),
inference(resolution,[],[f1960,f1954]) ).
fof(f2032,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n2))
| rdn_positive_less(rdnn(X0),rdnn(n3)) ),
inference(resolution,[],[f1960,f1953]) ).
fof(f2033,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n5))
| rdn_positive_less(rdnn(X0),rdnn(n6)) ),
inference(resolution,[],[f1960,f1956]) ).
fof(f2034,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n6))
| rdn_positive_less(rdnn(X0),rdnn(n7)) ),
inference(resolution,[],[f1960,f1957]) ).
fof(f2037,plain,
rdn_positive_less(rdnn(n2),rdnn(n4)),
inference(resolution,[],[f2029,f1953]) ).
fof(f2048,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n1))
| rdn_positive_less(rdnn(X0),rdnn(n2)) ),
inference(resolution,[],[f1952,f1960]) ).
fof(f2053,plain,
rdn_positive_less(rdnn(n0),rdnn(n2)),
inference(resolution,[],[f2048,f1951]) ).
fof(f2054,plain,
rdn_positive_less(rdnn(n0),rdnn(n3)),
inference(resolution,[],[f2053,f2032]) ).
fof(f2058,plain,
rdn_positive_less(rdnn(n3),rdnn(n5)),
inference(resolution,[],[f2028,f1954]) ).
fof(f2059,plain,
rdn_positive_less(rdnn(n2),rdnn(n5)),
inference(resolution,[],[f2028,f2037]) ).
fof(f2060,plain,
rdn_positive_less(rdnn(n3),rdnn(n6)),
inference(resolution,[],[f2058,f2033]) ).
fof(f2062,plain,
rdn_non_zero(rdnn(n6)),
inference(resolution,[],[f1947,f1964]) ).
fof(f2112,plain,
! [X0] :
( accept_population(countrybcivilorganization,other,X0)
| ~ less(X0,n5) ),
inference(resolution,[],[f1362,f987]) ).
fof(f2113,plain,
( ~ less(n2,n5)
| ~ accept_population(countrybcivilorganization,atheist,n70)
| ~ accept_population(countrybcivilorganization,christian,n20)
| ~ accept_population(countrybcivilorganization,muslim,n8)
| ~ accept_population(countrybcivilorganization,native,n0)
| accept_city(countrybcivilorganization,townb) ),
inference(resolution,[],[f2112,f1052]) ).
fof(f2117,plain,
( ~ less(n2,n5)
| ~ accept_population(countrybcivilorganization,atheist,n70)
| ~ accept_population(countrybcivilorganization,muslim,n8)
| ~ accept_population(countrybcivilorganization,native,n0)
| accept_city(countrybcivilorganization,townb) ),
inference(forward_subsumption_resolution,[],[f2113,f1369]) ).
fof(f2118,plain,
( ~ less(n2,n5)
| ~ accept_population(countrybcivilorganization,atheist,n70)
| ~ accept_population(countrybcivilorganization,muslim,n8)
| accept_city(countrybcivilorganization,townb) ),
inference(forward_subsumption_resolution,[],[f2117,f1614]) ).
fof(f2119,plain,
( ~ less(n2,n5)
| ~ accept_population(countrybcivilorganization,atheist,n70)
| ~ accept_population(countrybcivilorganization,muslim,n8) ),
inference(forward_subsumption_resolution,[],[f2118,f1976]) ).
fof(f2121,definition,
( spl0_7
<=> accept_population(countrybcivilorganization,muslim,n8) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f2123,plain,
( ~ accept_population(countrybcivilorganization,muslim,n8)
| spl0_7 ),
inference(avatar_component_clause,[],[f2121]) ).
fof(f2125,definition,
( spl0_8
<=> accept_population(countrybcivilorganization,atheist,n70) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f2127,plain,
( ~ accept_population(countrybcivilorganization,atheist,n70)
| spl0_8 ),
inference(avatar_component_clause,[],[f2125]) ).
fof(f2129,definition,
( spl0_9
<=> less(n2,n5) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f2131,plain,
( ~ less(n2,n5)
| spl0_9 ),
inference(avatar_component_clause,[],[f2129]) ).
fof(f2132,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f2119,f2129,f2125,f2121]) ).
fof(f2139,plain,
! [X0] :
( accept_population(countrybcivilorganization,muslim,X0)
| ~ less(X0,n65) ),
inference(resolution,[],[f1363,f987]) ).
fof(f2153,plain,
( ~ less(n8,n65)
| spl0_7 ),
inference(resolution,[],[f2139,f2123]) ).
fof(f2163,plain,
! [X0] :
( accept_population(countrybcivilorganization,atheist,X0)
| ~ less(X0,n78) ),
inference(resolution,[],[f1370,f987]) ).
fof(f2245,definition,
( spl0_17
<=> rdn_positive_less(rdnn(n3),rdnn(n7)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f2246,plain,
( rdn_positive_less(rdnn(n3),rdnn(n7))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f2245]) ).
fof(f2247,plain,
( ~ rdn_positive_less(rdnn(n3),rdnn(n7))
| spl0_17 ),
inference(avatar_component_clause,[],[f2245]) ).
fof(f2345,plain,
! [X0] :
( ~ rdn_translate(X0,rdn_pos(rdnn(n2)))
| less(X0,n5) ),
inference(resolution,[],[f1988,f2059]) ).
fof(f2414,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n8),rdnn(n7)))
| less(X0,n78)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1764,f1966]) ).
fof(f2434,plain,
! [X0,X1] :
( less(X0,n78)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n7))))
| ~ rdn_positive_less(rdnn(X1),rdnn(n8))
| ~ rdn_non_zero(rdnn(n7)) ),
inference(resolution,[],[f2414,f1962]) ).
fof(f2436,plain,
( ! [X0,X1] :
( ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n7))))
| less(X0,n78)
| ~ rdn_positive_less(rdnn(X1),rdnn(n8)) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2434,f2000]) ).
fof(f2447,plain,
( less(n70,n78)
| ~ rdn_positive_less(rdnn(n0),rdnn(n8))
| ~ spl0_1 ),
inference(resolution,[],[f2436,f1756]) ).
fof(f2453,definition,
( spl0_33
<=> rdn_positive_less(rdnn(n0),rdnn(n8)) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f2455,plain,
( ~ rdn_positive_less(rdnn(n0),rdnn(n8))
| spl0_33 ),
inference(avatar_component_clause,[],[f2453]) ).
fof(f2457,definition,
( spl0_34
<=> less(n70,n78) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f2460,plain,
( ~ spl0_33
| spl0_34
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f2447,f1999,f2457,f2453]) ).
fof(f2478,plain,
rdn_positive_less(rdnn(n3),rdnn(n7)),
inference(resolution,[],[f2060,f2034]) ).
fof(f2480,plain,
( $false
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f2478,f2247]) ).
fof(f2481,plain,
spl0_17,
inference(avatar_contradiction_clause,[],[f2480]) ).
fof(f2542,plain,
( ! [X0] :
( ~ rdn_positive_less(rdnn(X0),rdnn(n3))
| rdn_positive_less(rdnn(X0),rdnn(n7)) )
| ~ spl0_17 ),
inference(resolution,[],[f2246,f1960]) ).
fof(f2557,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n5),rdnn(n6)))
| less(X0,n65)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[],[f1751,f1966]) ).
fof(f2582,plain,
! [X0,X1] :
( less(X0,n65)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1)))
| ~ rdn_non_zero(rdnn(n6)) ),
inference(resolution,[],[f2557,f1963]) ).
fof(f2586,plain,
! [X0,X1] :
( ~ rdn_translate(X0,rdn_pos(rdnn(X1)))
| less(X0,n65) ),
inference(forward_subsumption_resolution,[],[f2582,f2062]) ).
fof(f2591,plain,
less(n8,n65),
inference(resolution,[],[f2586,f1694]) ).
fof(f2596,plain,
( $false
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f2591,f2153]) ).
fof(f2597,plain,
spl0_7,
inference(avatar_contradiction_clause,[],[f2596]) ).
fof(f2598,plain,
( ~ less(n70,n78)
| spl0_8 ),
inference(resolution,[],[f2127,f2163]) ).
fof(f2610,plain,
( ~ spl0_34
| spl0_8 ),
inference(avatar_split_clause,[],[f2598,f2125,f2457]) ).
fof(f3176,plain,
( rdn_positive_less(rdnn(n0),rdnn(n7))
| ~ spl0_17 ),
inference(resolution,[],[f2542,f2054]) ).
fof(f3181,plain,
( rdn_positive_less(rdnn(n0),rdnn(n8))
| ~ spl0_17 ),
inference(resolution,[],[f3176,f2027]) ).
fof(f3184,plain,
( $false
| ~ spl0_17
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f3181,f2455]) ).
fof(f3185,plain,
( ~ spl0_17
| spl0_33 ),
inference(avatar_contradiction_clause,[],[f3184]) ).
fof(f4403,plain,
less(n2,n5),
inference(resolution,[],[f2345,f1688]) ).
fof(f4404,plain,
( $false
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f4403,f2131]) ).
fof(f4405,plain,
spl0_9,
inference(avatar_contradiction_clause,[],[f4404]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f2020]) ).
cnf(s5,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s18,plain,
( ~ spl0_1
| ~ spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f2460]) ).
cnf(s20,plain,
spl0_17,
inference(sat_conversion,[],[f2481]) ).
cnf(s28,plain,
spl0_7,
inference(sat_conversion,[],[f2597]) ).
cnf(s31,plain,
( spl0_8
| ~ spl0_34 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s78,plain,
( ~ spl0_17
| spl0_33 ),
inference(sat_conversion,[],[f3185]) ).
cnf(s113,plain,
spl0_9,
inference(sat_conversion,[],[f4405]) ).
cnf(s123,plain,
spl0_33,
inference(rat,[],[s78,s20]) ).
cnf(s131,plain,
( ~ spl0_1
| spl0_34 ),
inference(rat,[],[s18,s123]) ).
cnf(s134,plain,
~ spl0_8,
inference(rat,[],[s5,s113,s28]) ).
cnf(s135,plain,
~ spl0_34,
inference(rat,[],[s31,s134]) ).
cnf(s138,plain,
~ spl0_1,
inference(rat,[],[s131,s135]) ).
cnf(s141,plain,
$false,
inference(rat,[],[s2,s138]) ).
fof(f4406,plain,
$false,
inference(avatar_sat_refutation,[],[s141]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT007+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n009.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Mon Sep 28 19:09:00 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.25 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.87/1.92 % (3359940)Detected formulas, will run a generic FOF schedule.
% 7.87/1.92 % (3359949)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=555388698:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.87/1.92 % (3359949)Refutation not found, incomplete strategy
% 7.87/1.92 % (3359949)------------------------------
% 7.87/1.92 % (3359949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/1.92 % (3359949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.92 % (3359949)CaDiCaL version: 2.1.3
% 7.87/1.92 % (3359949)Termination reason: Refutation not found, incomplete strategy
% 7.87/1.92 % (3359949)Time elapsed: 0.005 s
% 7.87/1.92 % (3359949)Peak memory usage: 88 MB
% 7.87/1.92 % (3359949)Instructions burned: 15 (million)
% 7.87/1.92 % (3359945)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=1925163528:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.87/1.92 % (3359947)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=498723781:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.87/1.92 % (3359946)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=4032638860:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.87/1.92 % (3359948)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1168026928:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.87/1.92 % (3359951)dis-21_1_sil=8000:lcm=predicate:random_seed=2920467217: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.87/1.92 % (3359950)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4004231465:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.87/1.92 % (3359948)Refutation not found, incomplete strategy
% 7.87/1.92 % (3359948)------------------------------
% 7.87/1.92 % (3359948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/1.92 % (3359948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.92 % (3359948)CaDiCaL version: 2.1.3
% 7.87/1.92 % (3359948)Termination reason: Refutation not found, incomplete strategy
% 7.87/1.92 % (3359948)Time elapsed: 0.003 s
% 7.87/1.92 % (3359948)Peak memory usage: 88 MB
% 7.87/1.92 % (3359948)Instructions burned: 3 (million)
% 7.87/1.92 % (3359951)Instruction limit reached!
% 7.87/1.92 % (3359951)------------------------------
% 7.87/1.92 % (3359951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/1.92 % (3359951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.92 % (3359951)CaDiCaL version: 2.1.3
% 7.87/1.92 % (3359951)Termination reason: Instruction limit
% 7.87/1.92 % (3359951)Termination phase: Saturation
% 7.87/1.92 % (3359951)Time elapsed: 0.069 s
% 7.87/1.92 % (3359951)Peak memory usage: 91 MB
% 7.87/1.92 % (3359951)Instructions burned: 131 (million)
% 7.87/1.92 % (3359950)Instruction limit reached!
% 7.87/1.92 % (3359950)------------------------------
% 7.87/1.92 % (3359950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/1.92 % (3359950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.92 % (3359950)CaDiCaL version: 2.1.3
% 7.87/1.92 % (3359950)Termination reason: Instruction limit
% 7.87/1.92 % (3359950)Termination phase: Saturation
% 7.87/1.92 % (3359950)Time elapsed: 0.085 s
% 7.87/1.92 % (3359950)Peak memory usage: 90 MB
% 7.87/1.92 % (3359950)Instructions burned: 140 (million)
% 7.87/1.92 % (3359949)------------------------------
% 7.87/1.92 % (3359949)------------------------------
% 7.87/1.92 % (3359961)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2208483016:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.87/1.92 % (3359961)Refutation not found, incomplete strategy
% 7.87/1.92 % (3359961)------------------------------
% 7.87/1.92 % (3359961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.87/1.92 % (3359961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.92 % (3359961)CaDiCaL version: 2.1.3
% 7.87/1.92 % (3359961)Termination reason: Refutation not found, incomplete strategy
% 7.87/1.92 % (3359961)Time elapsed: 0.002 s
% 7.87/1.92 % (3359961)Peak memory usage: 88 MB
% 10.47/2.17 % (3359961)Instructions burned: 3 (million)
% 10.47/2.17 % (3359960)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1657398895:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.47/2.17 % (3359959)lrs+10_1_sil=8000:sp=occurrence:random_seed=1910252853:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.47/2.17 % (3359960)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359960)------------------------------
% 10.47/2.17 % (3359960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359960)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359960)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359960)Time elapsed: 0.005 s
% 10.47/2.17 % (3359960)Peak memory usage: 88 MB
% 10.47/2.17 % (3359960)Instructions burned: 8 (million)
% 10.47/2.17 % (3359959)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359959)------------------------------
% 10.47/2.17 % (3359959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359959)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359959)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359959)Time elapsed: 0.008 s
% 10.47/2.17 % (3359959)Peak memory usage: 89 MB
% 10.47/2.17 % (3359959)Instructions burned: 14 (million)
% 10.47/2.17 % (3359948)------------------------------
% 10.47/2.17 % (3359948)------------------------------
% 10.47/2.17 % (3359961)------------------------------
% 10.47/2.17 % (3359961)------------------------------
% 10.47/2.17 % (3359965)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=4290039664:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 10.47/2.17 % (3359960)------------------------------
% 10.47/2.17 % (3359960)------------------------------
% 10.47/2.17 % (3359959)------------------------------
% 10.47/2.17 % (3359959)------------------------------
% 10.47/2.17 % (3359966)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2665835300:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.47/2.17 % (3359966)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359966)------------------------------
% 10.47/2.17 % (3359966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359966)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359966)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359966)Time elapsed: 0.004 s
% 10.47/2.17 % (3359966)Peak memory usage: 88 MB
% 10.47/2.17 % (3359966)Instructions burned: 13 (million)
% 10.47/2.17 % (3359965)Instruction limit reached!
% 10.47/2.17 % (3359965)------------------------------
% 10.47/2.17 % (3359965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359965)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359965)Termination reason: Instruction limit
% 10.47/2.17 % (3359965)Termination phase: Saturation
% 10.47/2.17 % (3359965)Time elapsed: 0.129 s
% 10.47/2.17 % (3359965)Peak memory usage: 93 MB
% 10.47/2.17 % (3359965)Instructions burned: 249 (million)
% 10.47/2.17 % (3359947)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359947)------------------------------
% 10.47/2.17 % (3359947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359947)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359947)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359947)Time elapsed: 0.610 s
% 10.47/2.17 % (3359947)Peak memory usage: 128 MB
% 10.47/2.17 % (3359947)Instructions burned: 900 (million)
% 10.47/2.17 % (3359968)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1249074611:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.47/2.17 % (3359969)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=927211380:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.47/2.17 % (3359969)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359969)------------------------------
% 10.47/2.17 % (3359969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359969)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359969)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359969)Time elapsed: 0.007 s
% 10.47/2.17 % (3359969)Peak memory usage: 88 MB
% 10.47/2.17 % (3359969)Instructions burned: 10 (million)
% 10.47/2.17 % (3359966)------------------------------
% 10.47/2.17 % (3359966)------------------------------
% 10.47/2.17 % (3359972)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1685100143:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 10.47/2.17 % (3359975)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=18368881:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 10.47/2.17 % (3359972)Instruction limit reached!
% 10.47/2.17 % (3359972)------------------------------
% 10.47/2.17 % (3359972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359972)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359972)Termination reason: Instruction limit
% 10.47/2.17 % (3359972)Termination phase: Saturation
% 10.47/2.17 % (3359972)Time elapsed: 0.061 s
% 10.47/2.17 % (3359972)Peak memory usage: 89 MB
% 10.47/2.17 % (3359972)Instructions burned: 128 (million)
% 10.47/2.17 % (3359975)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359975)------------------------------
% 10.47/2.17 % (3359975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359975)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359975)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359975)Time elapsed: 0.013 s
% 10.47/2.17 % (3359975)Peak memory usage: 90 MB
% 10.47/2.17 % (3359975)Instructions burned: 46 (million)
% 10.47/2.17 % (3359947)------------------------------
% 10.47/2.17 % (3359947)------------------------------
% 10.47/2.17 % (3359946)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359946)------------------------------
% 10.47/2.17 % (3359946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359946)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359946)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359946)Time elapsed: 0.868 s
% 10.47/2.17 % (3359946)Peak memory usage: 131 MB
% 10.47/2.17 % (3359946)Instructions burned: 1266 (million)
% 10.47/2.17 % (3359969)------------------------------
% 10.47/2.17 % (3359969)------------------------------
% 10.47/2.17 % (3359975)------------------------------
% 10.47/2.17 % (3359975)------------------------------
% 10.47/2.17 % (3359978)lrs+10_1_sil=8000:sp=occurrence:random_seed=2475769995:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.47/2.17 % (3359978)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359978)------------------------------
% 10.47/2.17 % (3359978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359978)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359978)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359978)Time elapsed: 0.012 s
% 10.47/2.17 % (3359978)Peak memory usage: 89 MB
% 10.47/2.17 % (3359978)Instructions burned: 20 (million)
% 10.47/2.17 % (3359979)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=718443254:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 10.47/2.17 % (3359979)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359979)------------------------------
% 10.47/2.17 % (3359979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359979)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359979)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359979)Time elapsed: 0.003 s
% 10.47/2.17 % (3359979)Peak memory usage: 88 MB
% 10.47/2.17 % (3359979)Instructions burned: 3 (million)
% 10.47/2.17 % (3359945)First to succeed.
% 10.47/2.17 % (3359945)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3359940"
% 10.47/2.17 % (3359980)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1779160891:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 10.47/2.17 % (3359981)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3844389339:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 10.47/2.17 % (3359981)Refutation not found, incomplete strategy
% 10.47/2.17 % (3359981)------------------------------
% 10.47/2.17 % (3359981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.47/2.17 % (3359981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.47/2.17 % (3359981)CaDiCaL version: 2.1.3
% 10.47/2.17 % (3359981)Termination reason: Refutation not found, incomplete strategy
% 10.47/2.17 % (3359981)Time elapsed: 0.023 s
% 10.47/2.17 % (3359981)Peak memory usage: 90 MB
% 10.47/2.17 % (3359981)Instructions burned: 85 (million)
% 10.47/2.17 % (3359946)------------------------------
% 10.47/2.17 % (3359946)------------------------------
% 10.47/2.17 % (3359978)------------------------------
% 10.47/2.17 % (3359978)------------------------------
% 10.47/2.17 % (3359981)------------------------------
% 10.47/2.17 % (3359981)------------------------------
% 10.47/2.17 % (3359979)------------------------------
% 10.47/2.17 % (3359979)------------------------------
% 10.47/2.17 % (3359945)Refutation found. Thanks to Tanya!
% 10.47/2.17 % SZS status Theorem for theBenchmark
% 10.47/2.17 % SZS output start Proof for theBenchmark
% See solution above
% 11.05/2.37 % (3359945)------------------------------
% 11.05/2.37 % (3359945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.37 % (3359945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.37 % (3359945)CaDiCaL version: 2.1.3
% 11.05/2.37 % (3359945)Termination reason: Refutation
% 11.05/2.37 % (3359945)Time elapsed: 1.028 s
% 11.05/2.37 % (3359945)Peak memory usage: 139 MB
% 11.05/2.37 % (3359945)Instructions burned: 1509 (million)
% 11.05/2.37 % (3359945)------------------------------
% 11.05/2.37 % (3359945)------------------------------
% 11.05/2.37 % (3359940)Success in time 1.49 s
% 11.05/2.37 % Vampire exiting
%------------------------------------------------------------------------------