%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n012.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:44 AM UTC 2026
% Result : Theorem 45.87s 6.78s
% Output : Refutation 45.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 33
% Syntax : Number of formulae : 124 ( 59 unt; 4 def)
% Number of atoms : 272 ( 9 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 256 ( 108 ~; 104 |; 31 &)
% ( 7 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 5 prp; 0-4 aty)
% Number of functors : 23 ( 23 usr; 20 con; 0-2 aty)
% Number of variables : 104 ( 0 sgn 104 !; 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/Axioms/AGT001+0.ax',a1_1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( accept_number(X0,X1)
& less(X2,X1) )
=> accept_number(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_2) ).
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/Axioms/AGT001+0.ax',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/Axioms/AGT001+0.ax',a2_1) ).
fof(f59,axiom,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_39) ).
fof(f60,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_40) ).
fof(f255,axiom,
accept_number(countryccivilorganization,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_235) ).
fof(f307,axiom,
accept_population(countrybcivilorganization,native,n85),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_38) ).
fof(f313,axiom,
accept_population(countrybcivilorganization,other,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_44) ).
fof(f314,axiom,
accept_population(countrybcivilorganization,muslim,n65),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_45) ).
fof(f320,axiom,
accept_population(countrybcivilorganization,christian,n20),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_51) ).
fof(f327,axiom,
~ accept_number(countryccivilorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_58) ).
fof(f561,axiom,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_292) ).
fof(f568,axiom,
accept_population(countrybcivilorganization,atheist,n75),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_299) ).
fof(f596,axiom,
accept_number(countrybcivilorganization,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_327) ).
fof(f641,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn4) ).
fof(f644,axiom,
rdn_translate(n7,rdn_pos(rdnn(n7))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn7) ).
fof(f702,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn65) ).
fof(f712,axiom,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn75) ).
fof(f722,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn85) ).
fof(f898,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit6) ).
fof(f900,axiom,
rdn_non_zero_digit(rdnn(n8)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit8) ).
fof(f908,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',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/Axioms/NUM005+1.ax',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/Axioms/NUM005+1.ax',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/Axioms/NUM005+1.ax',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/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
fof(f920,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_property) ).
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(f930,plain,
! [X0,X1,X2] :
( accept_number(X0,X2)
| ~ accept_number(X0,X1)
| ~ less(X2,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f931,plain,
! [X0,X1,X2] :
( accept_number(X0,X2)
| ~ accept_number(X0,X1)
| ~ less(X2,X1) ),
inference(flattening,[],[f930]) ).
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(f980,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f920]) ).
fof(f981,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f980]) ).
fof(f985,plain,
! [X2,X3,X0,X1] :
( ~ accept_number(X0,X2)
| ~ accept_city(X0,X1)
| ~ accept_leader(X0,X3)
| accept_team(X0,X3,X1,X2) ),
inference(cnf_transformation,[],[f953]) ).
fof(f986,plain,
! [X2,X0,X1] :
( ~ less(X2,X1)
| ~ accept_number(X0,X1)
| accept_number(X0,X2) ),
inference(cnf_transformation,[],[f931]) ).
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(f1108,plain,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n4),
inference(cnf_transformation,[],[f59]) ).
fof(f1109,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
inference(cnf_transformation,[],[f60]) ).
fof(f1304,plain,
accept_number(countryccivilorganization,n4),
inference(cnf_transformation,[],[f255]) ).
fof(f1356,plain,
accept_population(countrybcivilorganization,native,n85),
inference(cnf_transformation,[],[f307]) ).
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(f1376,plain,
~ accept_number(countryccivilorganization,n5),
inference(cnf_transformation,[],[f327]) ).
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(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(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_non_zero(X2)
| rdn_positive_less(rdnn(X0),rdn(rdnn(X1),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(f1971,plain,
! [X0,X1] :
( less(X1,X0)
| less(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f981]) ).
fof(f1972,plain,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(cnf_transformation,[],[f925]) ).
fof(f1979,plain,
rdn_non_zero(rdnn(n8)),
inference(unit_resulting_resolution,[],[f1964,f1949]) ).
fof(f1982,plain,
rdn_non_zero(rdnn(n6)),
inference(unit_resulting_resolution,[],[f1964,f1947]) ).
fof(f3279,plain,
~ less(n5,n4),
inference(unit_resulting_resolution,[],[f986,f1376,f1304]) ).
fof(f3292,plain,
! [X0,X1] : rdn_positive_less(rdnn(X0),rdn(rdnn(X1),rdnn(n8))),
inference(unit_resulting_resolution,[],[f1963,f1979]) ).
fof(f3295,plain,
! [X0,X1] : rdn_positive_less(rdnn(X0),rdn(rdnn(X1),rdnn(n6))),
inference(unit_resulting_resolution,[],[f1963,f1982]) ).
fof(f3747,plain,
! [X0] :
( ~ less(X0,n75)
| accept_population(countrybcivilorganization,atheist,X0) ),
inference(resolution,[],[f987,f1617]) ).
fof(f3754,plain,
! [X0] :
( ~ less(X0,n65)
| accept_population(countrybcivilorganization,muslim,X0) ),
inference(resolution,[],[f987,f1363]) ).
fof(f3756,plain,
! [X0] :
( ~ less(X0,n85)
| accept_population(countrybcivilorganization,native,X0) ),
inference(resolution,[],[f987,f1356]) ).
fof(f3758,plain,
! [X0] :
( ~ less(X0,n5)
| accept_population(countrybcivilorganization,other,X0) ),
inference(resolution,[],[f987,f1362]) ).
fof(f9531,definition,
( spl0_7
<=> n4 = n5 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f9532,plain,
( n4 != n5
| spl0_7 ),
inference(avatar_component_clause,[],[f9531]) ).
fof(f9533,plain,
( n4 = n5
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f9531]) ).
fof(f9544,plain,
( accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5)
| ~ spl0_7 ),
inference(superposition,[],[f1108,f9533]) ).
fof(f9616,plain,
( $false
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f9544,f1109]) ).
fof(f9617,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f9616]) ).
fof(f9618,plain,
( less(n4,n5)
| spl0_7 ),
inference(unit_resulting_resolution,[],[f1971,f3279,f9532]) ).
fof(f9629,plain,
( accept_population(countrybcivilorganization,other,n4)
| spl0_7 ),
inference(unit_resulting_resolution,[],[f3758,f9618]) ).
fof(f66388,plain,
~ accept_city(countrybcivilorganization,suffertown),
inference(unit_resulting_resolution,[],[f985,f1610,f1972,f1645]) ).
fof(f88183,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_7 ),
inference(resolution,[],[f992,f9629]) ).
fof(f88188,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f88183,f1369]) ).
fof(f88196,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f88188,f66388]) ).
fof(f88198,definition,
( spl0_11
<=> accept_population(countrybcivilorganization,native,n4) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f88200,plain,
( ~ accept_population(countrybcivilorganization,native,n4)
| spl0_11 ),
inference(avatar_component_clause,[],[f88198]) ).
fof(f88202,definition,
( spl0_12
<=> accept_population(countrybcivilorganization,muslim,n7) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f88204,plain,
( ~ accept_population(countrybcivilorganization,muslim,n7)
| spl0_12 ),
inference(avatar_component_clause,[],[f88202]) ).
fof(f88206,definition,
( spl0_13
<=> accept_population(countrybcivilorganization,atheist,n65) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f88208,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| spl0_13 ),
inference(avatar_component_clause,[],[f88206]) ).
fof(f88209,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| spl0_7 ),
inference(avatar_split_clause,[],[f88196,f9531,f88206,f88202,f88198]) ).
fof(f88211,plain,
( ~ less(n4,n85)
| spl0_11 ),
inference(unit_resulting_resolution,[],[f3756,f88200]) ).
fof(f88252,plain,
( ~ rdn_positive_less(rdnn(n4),rdn(rdnn(n5),rdnn(n8)))
| spl0_11 ),
inference(unit_resulting_resolution,[],[f1966,f1771,f1690,f88211]) ).
fof(f88267,plain,
( $false
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f88252,f3292]) ).
fof(f88268,plain,
spl0_11,
inference(avatar_contradiction_clause,[],[f88267]) ).
fof(f88399,plain,
( ~ less(n7,n65)
| spl0_12 ),
inference(unit_resulting_resolution,[],[f3754,f88204]) ).
fof(f88431,plain,
( ~ rdn_positive_less(rdnn(n7),rdn(rdnn(n5),rdnn(n6)))
| spl0_12 ),
inference(unit_resulting_resolution,[],[f1966,f1751,f1693,f88399]) ).
fof(f88435,plain,
( $false
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f88431,f3295]) ).
fof(f88436,plain,
spl0_12,
inference(avatar_contradiction_clause,[],[f88435]) ).
fof(f88569,plain,
( ~ less(n65,n75)
| spl0_13 ),
inference(unit_resulting_resolution,[],[f3747,f88208]) ).
fof(f88605,plain,
( ~ rdn_positive_less(rdn(rdnn(n5),rdnn(n6)),rdn(rdnn(n5),rdnn(n7)))
| spl0_13 ),
inference(unit_resulting_resolution,[],[f1966,f1761,f1751,f88569]) ).
fof(f307859,plain,
( ~ rdn_positive_less(rdnn(n6),rdnn(n7))
| spl0_13 ),
inference(unit_resulting_resolution,[],[f1961,f88605]) ).
fof(f307865,plain,
( $false
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f307859,f1957]) ).
fof(f307866,plain,
spl0_13,
inference(avatar_contradiction_clause,[],[f307865]) ).
cnf(s9,plain,
~ spl0_7,
inference(sat_conversion,[],[f9617]) ).
cnf(s12,plain,
( spl0_7
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f88209]) ).
cnf(s14,plain,
spl0_11,
inference(sat_conversion,[],[f88268]) ).
cnf(s16,plain,
spl0_12,
inference(sat_conversion,[],[f88436]) ).
cnf(s27,plain,
spl0_13,
inference(sat_conversion,[],[f307866]) ).
cnf(s28,plain,
spl0_7,
inference(rat,[],[s12,s27,s16,s14]) ).
cnf(s30,plain,
$false,
inference(rat,[],[s9,s28]) ).
fof(f307867,plain,
$false,
inference(avatar_sat_refutation,[],[s30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : AGT006+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 19:08:19 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.12 Running first-order model finding
% 0.00/0.12 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
% 14.47/2.23 % (3653495)Will run a generic schedule for satisfiability detection.
% 14.47/2.23 % (3653501)% WARNING: option uhcvi not known.
% 14.47/2.23 % (3653501)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2059103258:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.47/2.23 % (3653500)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4087930011_2999 on theBenchmark for (2999ds/0Mi)
% 14.47/2.23 % (3653502)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=792774410:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.47/2.23 % (3653503)dis+10_1_sil=32000:sp=arity:random_seed=3824599906:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.47/2.23 % (3653504)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3980734335:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.47/2.23 % (3653505)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4215195733:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.47/2.23 % (3653506)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=758227207:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.47/2.23 % TRYING [1]
% 14.47/2.23 % TRYING [2]
% 14.47/2.23 % (3653503)Instruction limit reached!
% 14.47/2.23 % (3653503)------------------------------
% 14.47/2.23 % (3653503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.23 % (3653503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.23 % (3653503)CaDiCaL version: 2.1.3
% 14.47/2.23 % (3653503)Termination reason: Instruction limit
% 14.47/2.23 % (3653503)Termination phase: Saturation
% 14.47/2.23 % (3653503)Time elapsed: 0.027 s
% 14.47/2.23 % (3653503)Peak memory usage: 13 MB
% 14.47/2.23 % (3653503)Instructions burned: 105 (million)
% 14.47/2.23 % (3653504)Instruction limit reached!
% 14.47/2.23 % (3653504)------------------------------
% 14.47/2.23 % (3653504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.23 % (3653504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.23 % (3653504)CaDiCaL version: 2.1.3
% 14.47/2.23 % (3653504)Termination reason: Instruction limit
% 14.47/2.23 % (3653504)Termination phase: Saturation
% 14.47/2.23 % (3653504)Time elapsed: 0.030 s
% 14.47/2.23 % (3653504)Peak memory usage: 14 MB
% 14.47/2.23 % (3653504)Instructions burned: 119 (million)
% 14.47/2.23 % TRYING [3]
% 14.47/2.23 % (3653505)Instruction limit reached!
% 14.47/2.23 % (3653505)------------------------------
% 14.47/2.23 % (3653505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.23 % (3653505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.23 % (3653505)CaDiCaL version: 2.1.3
% 14.47/2.23 % (3653505)Termination reason: Instruction limit
% 14.47/2.23 % (3653505)Termination phase: Saturation
% 14.47/2.23 % (3653505)Time elapsed: 0.034 s
% 14.47/2.23 % (3653505)Peak memory usage: 15 MB
% 14.47/2.23 % (3653505)Instructions burned: 135 (million)
% 14.47/2.23 % (3653514)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1033560087:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.47/2.23 % (3653515)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1736041054:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.47/2.23 % (3653506)Instruction limit reached!
% 14.47/2.23 % (3653506)------------------------------
% 14.47/2.23 % (3653506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.23 % (3653506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.47/2.23 % (3653506)CaDiCaL version: 2.1.3
% 14.47/2.23 % (3653506)Termination reason: Instruction limit
% 14.47/2.23 % (3653506)Termination phase: Saturation
% 14.47/2.23 % (3653506)Time elapsed: 0.045 s
% 14.47/2.23 % (3653506)Peak memory usage: 15 MB
% 14.47/2.23 % (3653506)Instructions burned: 160 (million)
% 14.47/2.23 % (3653516)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=3429514901:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 14.47/2.23 % (3653520)ott-21_1_sil=16000:fs=off:random_seed=3897867477:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 14.47/2.23 % TRYING [1]
% 14.47/2.23 % TRYING [4]
% 14.47/2.23 % TRYING [2]
% 14.47/2.23 % TRYING [3]
% 14.47/2.23 % (3653515)Instruction limit reached!
% 14.47/2.23 % (3653515)------------------------------
% 14.47/2.23 % (3653515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.47/2.23 % (3653515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/3.87 % (3653515)CaDiCaL version: 2.1.3
% 25.77/3.87 % (3653515)Termination reason: Instruction limit
% 25.77/3.87 % (3653515)Termination phase: Saturation
% 25.77/3.87 % (3653515)Time elapsed: 0.036 s
% 25.77/3.87 % (3653515)Peak memory usage: 14 MB
% 25.77/3.87 % (3653515)Instructions burned: 133 (million)
% 25.77/3.87 % (3653522)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3292248314:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 25.77/3.87 % (3653520)Instruction limit reached!
% 25.77/3.87 % (3653520)------------------------------
% 25.77/3.87 % (3653520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.77/3.87 % (3653520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/3.87 % (3653520)CaDiCaL version: 2.1.3
% 25.77/3.87 % (3653520)Termination reason: Instruction limit
% 25.77/3.87 % (3653520)Termination phase: Saturation
% 25.77/3.87 % (3653520)Time elapsed: 0.044 s
% 25.77/3.87 % (3653520)Peak memory usage: 13 MB
% 25.77/3.87 % (3653520)Instructions burned: 181 (million)
% 25.77/3.87 % TRYING [4]
% 25.77/3.87 % (3653524)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2558069765:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 25.77/3.87 % TRYING [1]
% 25.77/3.87 % TRYING [2]
% 25.77/3.87 % TRYING [5]
% 25.77/3.87 % TRYING [3]
% 25.77/3.87 % (3653514)Instruction limit reached!
% 25.77/3.87 % (3653514)------------------------------
% 25.77/3.87 % (3653514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.77/3.87 % (3653514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/3.87 % (3653514)CaDiCaL version: 2.1.3
% 25.77/3.87 % (3653514)Termination reason: Instruction limit
% 25.77/3.87 % (3653514)Termination phase: Finite model building SAT solving
% 25.77/3.87 % (3653514)Time elapsed: 0.175 s
% 25.77/3.87 % (3653514)Peak memory usage: 36 MB
% 25.77/3.87 % (3653514)Instructions burned: 715 (million)
% 25.77/3.87 % (3653522)Instruction limit reached!
% 25.77/3.87 % (3653522)------------------------------
% 25.77/3.87 % (3653522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.77/3.87 % (3653522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/3.87 % (3653522)CaDiCaL version: 2.1.3
% 25.77/3.87 % (3653522)Termination reason: Instruction limit
% 25.77/3.87 % (3653522)Termination phase: Saturation
% 25.77/3.87 % (3653522)Time elapsed: 0.131 s
% 25.77/3.87 % (3653522)Peak memory usage: 17 MB
% 25.77/3.87 % (3653522)Instructions burned: 479 (million)
% 25.77/3.87 % (3653526)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2882984846:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 25.77/3.87 % (3653527)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4245383519:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 25.77/3.87 % (3653516)Instruction limit reached!
% 25.77/3.87 % (3653516)------------------------------
% 25.77/3.87 % (3653516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.77/3.87 % (3653516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/3.87 % (3653516)CaDiCaL version: 2.1.3
% 25.77/3.87 % (3653516)Termination reason: Instruction limit
% 25.77/3.87 % (3653516)Termination phase: Saturation
% 25.77/3.87 % (3653516)Time elapsed: 0.204 s
% 25.77/3.87 % (3653516)Peak memory usage: 23 MB
% 25.77/3.87 % (3653516)Instructions burned: 687 (million)
% 25.77/3.87 % (3653530)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=815927667:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 25.77/3.87 % TRYING [14]
% 25.77/3.87 % (3653524)Instruction limit reached!
% 25.77/3.87 % (3653524)------------------------------
% 25.77/3.87 % (3653524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.77/3.87 % (3653524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/3.87 % (3653524)CaDiCaL version: 2.1.3
% 25.77/3.87 % (3653524)Termination reason: Instruction limit
% 25.77/3.87 % (3653524)Termination phase: Finite model building SAT solving
% 25.77/3.87 % (3653524)Time elapsed: 0.175 s
% 25.77/3.87 % (3653524)Peak memory usage: 21 MB
% 25.77/3.87 % (3653524)Instructions burned: 870 (million)
% 25.77/3.87 % (3653532)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3941401947:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 25.77/3.87 % (3653527)Instruction limit reached!
% 25.77/3.87 % (3653527)------------------------------
% 25.77/3.87 % (3653527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653527)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653527)Termination reason: Instruction limit
% 45.87/6.78 % (3653527)Termination phase: Finite model building constraint generation
% 45.87/6.78 % (3653527)Time elapsed: 0.185 s
% 45.87/6.78 % (3653527)Peak memory usage: 75 MB
% 45.87/6.78 % (3653527)Instructions burned: 893 (million)
% 45.87/6.78 % (3653534)fmb+10_1_sil=64000:random_seed=509559750:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 45.87/6.78 % TRYING [6]
% 45.87/6.78 % (3653530)Instruction limit reached!
% 45.87/6.78 % (3653530)------------------------------
% 45.87/6.78 % (3653530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653530)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653530)Termination reason: Instruction limit
% 45.87/6.78 % (3653530)Termination phase: Saturation
% 45.87/6.78 % (3653530)Time elapsed: 0.193 s
% 45.87/6.78 % (3653530)Peak memory usage: 25 MB
% 45.87/6.78 % (3653530)Instructions burned: 693 (million)
% 45.87/6.78 % TRYING [1]
% 45.87/6.78 % TRYING [2]
% 45.87/6.78 % (3653536)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1358975759:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 45.87/6.78 % TRYING [20]
% 45.87/6.78 % TRYING [3]
% 45.87/6.78 % (3653532)Instruction limit reached!
% 45.87/6.78 % (3653532)------------------------------
% 45.87/6.78 % (3653532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653532)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653532)Termination reason: Instruction limit
% 45.87/6.78 % (3653532)Termination phase: Saturation
% 45.87/6.78 % (3653532)Time elapsed: 0.222 s
% 45.87/6.78 % (3653532)Peak memory usage: 24 MB
% 45.87/6.78 % (3653532)Instructions burned: 883 (million)
% 45.87/6.78 % (3653538)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=8046991:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 45.87/6.78 % TRYING [8]
% 45.87/6.78 % (3653526)Instruction limit reached!
% 45.87/6.78 % (3653526)------------------------------
% 45.87/6.78 % (3653526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653526)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653526)Termination reason: Instruction limit
% 45.87/6.78 % (3653526)Termination phase: Saturation
% 45.87/6.78 % (3653526)Time elapsed: 0.354 s
% 45.87/6.78 % (3653526)Peak memory usage: 33 MB
% 45.87/6.78 % (3653526)Instructions burned: 1182 (million)
% 45.87/6.78 % (3653540)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2208086284:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 45.87/6.78 % TRYING [4]
% 45.87/6.78 % (3653538)Instruction limit reached!
% 45.87/6.78 % (3653538)------------------------------
% 45.87/6.78 % (3653538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653538)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653538)Termination reason: Instruction limit
% 45.87/6.78 % (3653538)Termination phase: Finite model building constraint generation
% 45.87/6.78 % (3653538)Time elapsed: 0.181 s
% 45.87/6.78 % (3653538)Peak memory usage: 68 MB
% 45.87/6.78 % (3653538)Instructions burned: 924 (million)
% 45.87/6.78 % (3653542)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3479408493:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 45.87/6.78 % TRYING [7]
% 45.87/6.78 % TRYING [5]
% 45.87/6.78 % (3653542)Instruction limit reached!
% 45.87/6.78 % (3653542)------------------------------
% 45.87/6.78 % (3653542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653542)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653542)Termination reason: Instruction limit
% 45.87/6.78 % (3653542)Termination phase: Saturation
% 45.87/6.78 % (3653542)Time elapsed: 0.437 s
% 45.87/6.78 % (3653542)Peak memory usage: 30 MB
% 45.87/6.78 % (3653542)Instructions burned: 1475 (million)
% 45.87/6.78 % (3653544)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2932082054:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 45.87/6.78 % TRYING [77]
% 45.87/6.78 % TRYING [8]
% 45.87/6.78 % TRYING [6]
% 45.87/6.78 % (3653540)Instruction limit reached!
% 45.87/6.78 % (3653540)------------------------------
% 45.87/6.78 % (3653540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653540)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653540)Termination reason: Instruction limit
% 45.87/6.78 % (3653540)Termination phase: Saturation
% 45.87/6.78 % (3653540)Time elapsed: 1.473 s
% 45.87/6.78 % (3653540)Peak memory usage: 47 MB
% 45.87/6.78 % (3653540)Instructions burned: 5132 (million)
% 45.87/6.78 % (3653546)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2543753600:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 45.87/6.78 % TRYING [16]
% 45.87/6.78 % (3653536)Instruction limit reached!
% 45.87/6.78 % (3653536)------------------------------
% 45.87/6.78 % (3653536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653536)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653536)Termination reason: Instruction limit
% 45.87/6.78 % (3653536)Termination phase: Finite model building constraint generation
% 45.87/6.78 % (3653536)Time elapsed: 2.006 s
% 45.87/6.78 % (3653536)Peak memory usage: 565 MB
% 45.87/6.78 % (3653536)Instructions burned: 9518 (million)
% 45.87/6.78 % (3653544)Instruction limit reached!
% 45.87/6.78 % (3653544)------------------------------
% 45.87/6.78 % (3653544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653544)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653544)Termination reason: Instruction limit
% 45.87/6.78 % (3653544)Termination phase: Finite model building constraint generation
% 45.87/6.78 % (3653544)Time elapsed: 1.335 s
% 45.87/6.78 % (3653544)Peak memory usage: 525 MB
% 45.87/6.78 % (3653544)Instructions burned: 6324 (million)
% 45.87/6.78 % (3653546)Instruction limit reached!
% 45.87/6.78 % (3653546)------------------------------
% 45.87/6.78 % (3653546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653546)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653546)Termination reason: Instruction limit
% 45.87/6.78 % (3653546)Termination phase: Finite model building constraint generation
% 45.87/6.78 % (3653546)Time elapsed: 0.445 s
% 45.87/6.78 % (3653546)Peak memory usage: 153 MB
% 45.87/6.78 % (3653546)Instructions burned: 2178 (million)
% 45.87/6.78 % (3653548)ott-2_1_sil=16000:newcnf=on:random_seed=3826432545:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi)
% 45.87/6.78 % (3653550)ott+10_1_sil=32000:tgt=ground:random_seed=1162615292:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 45.87/6.78 % (3653552)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2414455749:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 45.87/6.78 % TRYING [1]
% 45.87/6.78 % TRYING [2]
% 45.87/6.78 % TRYING [3]
% 45.87/6.78 % TRYING [4]
% 45.87/6.78 % TRYING [5]
% 45.87/6.78 % (3653548)Instruction limit reached!
% 45.87/6.78 % (3653548)------------------------------
% 45.87/6.78 % (3653548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653548)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653548)Termination reason: Instruction limit
% 45.87/6.78 % (3653548)Termination phase: Saturation
% 45.87/6.78 % (3653548)Time elapsed: 0.267 s
% 45.87/6.78 % (3653548)Peak memory usage: 21 MB
% 45.87/6.78 % (3653548)Instructions burned: 870 (million)
% 45.87/6.78 % TRYING [7]
% 45.87/6.78 % (3653554)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3391165245:i=3512:aac=none_2971 on theBenchmark for (2971ds/3512Mi)
% 45.87/6.78 % TRYING [9]
% 45.87/6.78 % TRYING [6]
% 45.87/6.78 % TRYING [7]
% 45.87/6.78 % (3653554)Instruction limit reached!
% 45.87/6.78 % (3653554)------------------------------
% 45.87/6.78 % (3653554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653554)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653554)Termination reason: Instruction limit
% 45.87/6.78 % (3653554)Termination phase: Saturation
% 45.87/6.78 % (3653554)Time elapsed: 0.861 s
% 45.87/6.78 % (3653554)Peak memory usage: 35 MB
% 45.87/6.78 % (3653554)Instructions burned: 3514 (million)
% 45.87/6.78 % (3653556)dis+21_1_sil=32000:sas=cadical:random_seed=3269950588:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi)
% 45.87/6.78 % (3653550)Instruction limit reached!
% 45.87/6.78 % (3653550)------------------------------
% 45.87/6.78 % (3653550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653550)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653550)Termination reason: Instruction limit
% 45.87/6.78 % (3653550)Termination phase: Saturation
% 45.87/6.78 % (3653550)Time elapsed: 1.340 s
% 45.87/6.78 % (3653550)Peak memory usage: 65 MB
% 45.87/6.78 % (3653550)Instructions burned: 5118 (million)
% 45.87/6.78 % (3653558)ott+11_1_sil=16000:gs=on:random_seed=2557814062:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2960 on theBenchmark for (2960ds/2251Mi)
% 45.87/6.78 % TRYING [8]
% 45.87/6.78 % (3653558)Instruction limit reached!
% 45.87/6.78 % (3653558)------------------------------
% 45.87/6.78 % (3653558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653558)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653558)Termination reason: Instruction limit
% 45.87/6.78 % (3653558)Termination phase: Saturation
% 45.87/6.78 % (3653558)Time elapsed: 0.709 s
% 45.87/6.78 % (3653558)Peak memory usage: 44 MB
% 45.87/6.78 % (3653558)Instructions burned: 2254 (million)
% 45.87/6.78 % (3653560)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=462481533:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi)
% 45.87/6.78 % TRYING [7]
% 45.87/6.78 % (3653556)Instruction limit reached!
% 45.87/6.78 % (3653556)------------------------------
% 45.87/6.78 % (3653556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653556)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653556)Termination reason: Instruction limit
% 45.87/6.78 % (3653556)Termination phase: Saturation
% 45.87/6.78 % (3653556)Time elapsed: 1.021 s
% 45.87/6.78 % (3653556)Peak memory usage: 48 MB
% 45.87/6.78 % (3653556)Instructions burned: 3773 (million)
% 45.87/6.78 % (3653562)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=530093426:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2952 on theBenchmark for (2952ds/4591Mi)
% 45.87/6.78 % TRYING [8]
% 45.87/6.78 % (3653534)Instruction limit reached!
% 45.87/6.78 % (3653534)------------------------------
% 45.87/6.78 % (3653534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653534)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653534)Termination reason: Instruction limit
% 45.87/6.78 % (3653534)Termination phase: Finite model building constraint generation
% 45.87/6.78 % (3653534)Time elapsed: 4.486 s
% 45.87/6.78 % (3653534)Peak memory usage: 105 MB
% 45.87/6.78 % (3653534)Instructions burned: 22065 (million)
% 45.87/6.78 % (3653564)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1279259780:i=29340_2950 on theBenchmark for (2950ds/29340Mi)
% 45.87/6.78 % TRYING [10]
% 45.87/6.78 % TRYING [9]
% 45.87/6.78 % (3653562)Instruction limit reached!
% 45.87/6.78 % (3653562)------------------------------
% 45.87/6.78 % (3653562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653562)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653562)Termination reason: Instruction limit
% 45.87/6.78 % (3653562)Termination phase: Saturation
% 45.87/6.78 % (3653562)Time elapsed: 1.421 s
% 45.87/6.78 % (3653562)Peak memory usage: 59 MB
% 45.87/6.78 % (3653562)Instructions burned: 4593 (million)
% 45.87/6.78 % (3653566)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2903415059:i=5211_2937 on theBenchmark for (2937ds/5211Mi)
% 45.87/6.78 % (3653564) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3653495-3653564"...
% 45.87/6.78 % (3653564)...printing done.
% 45.87/6.78 % (3653564)Refutation found. Thanks to Tanya!
% 45.87/6.78 % SZS status Theorem for theBenchmark
% 45.87/6.78 % SZS output start Proof for theBenchmark
% See solution above
% 45.87/6.78 % (3653564)------------------------------
% 45.87/6.78 % (3653564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.87/6.78 % (3653564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/6.78 % (3653564)CaDiCaL version: 2.1.3
% 45.87/6.78 % (3653564)Termination reason: Refutation
% 45.87/6.78 % (3653564)Time elapsed: 1.606 s
% 45.87/6.78 % (3653564)Peak memory usage: 70 MB
% 45.87/6.78 % (3653564)Instructions burned: 6718 (million)
% 45.87/6.78 % (3653495)Success in time 6.654 s
% 45.87/6.78 % Vampire exiting
%------------------------------------------------------------------------------