%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : AGT010+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:45 AM UTC 2026
% Result : Theorem 8.44s 1.79s
% Output : Refutation 10.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 28
% Syntax : Number of formulae : 111 ( 44 unt; 5 def)
% Number of atoms : 226 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 214 ( 99 ~; 95 |; 8 &)
% ( 6 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 6 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( accept_population(X0,X3,X1)
& less(X2,X1) )
=> accept_population(X0,X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax',a1_3) ).
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/sandbox/benchmark/Axioms/AGT001+0.ax',a2_7) ).
fof(f282,axiom,
~ accept_city(countryamedicalorganization,coastvillage),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax',deduced_13) ).
fof(f287,axiom,
accept_population(countryamedicalorganization,atheist,n30),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax',deduced_18) ).
fof(f489,axiom,
accept_population(countryamedicalorganization,other,n0),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax',deduced_220) ).
fof(f491,axiom,
accept_population(countryamedicalorganization,muslim,n1),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax',deduced_222) ).
fof(f492,axiom,
accept_population(countryamedicalorganization,christian,n24),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax',deduced_223) ).
fof(f637,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn0) ).
fof(f638,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn1) ).
fof(f640,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn3) ).
fof(f649,axiom,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn12) ).
fof(f661,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn24) ).
fof(f667,axiom,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn30) ).
fof(f894,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_digit2) ).
fof(f902,axiom,
rdn_positive_less(rdnn(n0),rdnn(n1)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_positive_less01) ).
fof(f903,axiom,
rdn_positive_less(rdnn(n1),rdnn(n2)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_positive_less12) ).
fof(f904,axiom,
rdn_positive_less(rdnn(n2),rdnn(n3)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_positive_less23) ).
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/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_transitivity) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
fof(f923,conjecture,
~ accept_population(countryamedicalorganization,native,n85),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query_10) ).
fof(f924,negated_conjecture,
~ ~ accept_population(countryamedicalorganization,native,n85),
inference(negated_conjecture,[status(cth)],[f923]) ).
fof(f925,plain,
accept_population(countryamedicalorganization,native,n85),
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(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(f957,plain,
! [X2,X3,X0,X1] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(cnf_transformation,[],[f933]) ).
fof(f998,plain,
! [X0] :
( ~ accept_population(X0,native,n85)
| ~ accept_population(X0,other,n0)
| accept_city(X0,coastvillage)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(cnf_transformation,[],[f14]) ).
fof(f1301,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(cnf_transformation,[],[f282]) ).
fof(f1306,plain,
accept_population(countryamedicalorganization,atheist,n30),
inference(cnf_transformation,[],[f287]) ).
fof(f1508,plain,
accept_population(countryamedicalorganization,other,n0),
inference(cnf_transformation,[],[f489]) ).
fof(f1510,plain,
accept_population(countryamedicalorganization,muslim,n1),
inference(cnf_transformation,[],[f491]) ).
fof(f1511,plain,
accept_population(countryamedicalorganization,christian,n24),
inference(cnf_transformation,[],[f492]) ).
fof(f1656,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(cnf_transformation,[],[f637]) ).
fof(f1657,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(cnf_transformation,[],[f638]) ).
fof(f1659,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(cnf_transformation,[],[f640]) ).
fof(f1668,plain,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
inference(cnf_transformation,[],[f649]) ).
fof(f1680,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(cnf_transformation,[],[f661]) ).
fof(f1686,plain,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
inference(cnf_transformation,[],[f667]) ).
fof(f1913,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(cnf_transformation,[],[f894]) ).
fof(f1921,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(cnf_transformation,[],[f902]) ).
fof(f1922,plain,
rdn_positive_less(rdnn(n1),rdnn(n2)),
inference(cnf_transformation,[],[f903]) ).
fof(f1923,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(cnf_transformation,[],[f904]) ).
fof(f1930,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2)) ),
inference(cnf_transformation,[],[f939]) ).
fof(f1931,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(f1933,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2) ),
inference(cnf_transformation,[],[f943]) ).
fof(f1934,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[],[f944]) ).
fof(f1936,plain,
! [X2,X3,X0,X1] :
( less(X0,X1)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_positive_less(X2,X3) ),
inference(cnf_transformation,[],[f947]) ).
fof(f1942,plain,
accept_population(countryamedicalorganization,native,n85),
inference(cnf_transformation,[],[f925]) ).
fof(f2314,plain,
( ~ accept_population(countryamedicalorganization,other,n0)
| accept_city(countryamedicalorganization,coastvillage)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(resolution,[],[f998,f1942]) ).
fof(f2318,plain,
( accept_city(countryamedicalorganization,coastvillage)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(forward_subsumption_resolution,[],[f2314,f1508]) ).
fof(f2319,plain,
( ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(forward_subsumption_resolution,[],[f2318,f1301]) ).
fof(f2321,definition,
( spl0_1
<=> accept_population(countryamedicalorganization,atheist,n12) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f2323,plain,
( ~ accept_population(countryamedicalorganization,atheist,n12)
| spl0_1 ),
inference(avatar_component_clause,[],[f2321]) ).
fof(f2325,definition,
( spl0_2
<=> accept_population(countryamedicalorganization,christian,n3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f2327,plain,
( ~ accept_population(countryamedicalorganization,christian,n3)
| spl0_2 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2329,definition,
( spl0_3
<=> accept_population(countryamedicalorganization,muslim,n0) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f2331,plain,
( ~ accept_population(countryamedicalorganization,muslim,n0)
| spl0_3 ),
inference(avatar_component_clause,[],[f2329]) ).
fof(f2332,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f2319,f2329,f2325,f2321]) ).
fof(f2336,plain,
( ! [X0] :
( ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ less(n12,X0) )
| spl0_1 ),
inference(resolution,[],[f2323,f957]) ).
fof(f2361,plain,
( ~ less(n12,n30)
| spl0_1 ),
inference(resolution,[],[f2336,f1306]) ).
fof(f3484,plain,
( ! [X0] :
( ~ accept_population(countryamedicalorganization,muslim,X0)
| ~ less(n0,X0) )
| spl0_3 ),
inference(resolution,[],[f2331,f957]) ).
fof(f4141,plain,
( ~ less(n0,n1)
| spl0_3 ),
inference(resolution,[],[f3484,f1510]) ).
fof(f4340,plain,
( ! [X0] :
( ~ accept_population(countryamedicalorganization,christian,X0)
| ~ less(n3,X0) )
| spl0_2 ),
inference(resolution,[],[f2327,f957]) ).
fof(f4585,plain,
( ~ less(n3,n24)
| spl0_2 ),
inference(resolution,[],[f4340,f1511]) ).
fof(f5852,definition,
( spl0_145
<=> less(n3,n24) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f5853,plain,
( ~ less(n3,n24)
| spl0_145 ),
inference(avatar_component_clause,[],[f5852]) ).
fof(f40042,plain,
( ! [X0,X1] :
( ~ rdn_translate(n1,rdn_pos(X0))
| ~ rdn_translate(n0,rdn_pos(X1))
| ~ rdn_positive_less(X1,X0) )
| spl0_3 ),
inference(resolution,[],[f4141,f1936]) ).
fof(f42663,plain,
( ~ rdn_translate(n1,rdn_pos(rdnn(n1)))
| ~ rdn_translate(n0,rdn_pos(rdnn(n0)))
| spl0_3 ),
inference(resolution,[],[f40042,f1921]) ).
fof(f42670,plain,
( ~ rdn_translate(n0,rdn_pos(rdnn(n0)))
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f42663,f1657]) ).
fof(f42671,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f42670,f1656]) ).
fof(f42672,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f42671]) ).
fof(f42718,plain,
( ~ spl0_145
| spl0_2 ),
inference(avatar_split_clause,[],[f4585,f2325,f5852]) ).
fof(f42740,plain,
( ! [X0,X1] :
( ~ rdn_translate(n24,rdn_pos(X0))
| ~ rdn_translate(n3,rdn_pos(X1))
| ~ rdn_positive_less(X1,X0) )
| spl0_145 ),
inference(resolution,[],[f5853,f1936]) ).
fof(f43713,definition,
( spl0_571
<=> rdn_non_zero(rdnn(n2)) ),
introduced(definition,[new_symbols(definition,[spl0_571])],[avatar_definition]) ).
fof(f43714,plain,
( rdn_non_zero(rdnn(n2))
| ~ spl0_571 ),
inference(avatar_component_clause,[],[f43713]) ).
fof(f43715,plain,
( ~ rdn_non_zero(rdnn(n2))
| spl0_571 ),
inference(avatar_component_clause,[],[f43713]) ).
fof(f43722,plain,
( ~ rdn_non_zero_digit(rdnn(n2))
| spl0_571 ),
inference(resolution,[],[f43715,f1934]) ).
fof(f43723,plain,
( $false
| spl0_571 ),
inference(forward_subsumption_resolution,[],[f43722,f1913]) ).
fof(f43724,plain,
spl0_571,
inference(avatar_contradiction_clause,[],[f43723]) ).
fof(f44162,plain,
( ! [X0,X1] :
( ~ rdn_translate(n30,rdn_pos(X0))
| ~ rdn_translate(n12,rdn_pos(X1))
| ~ rdn_positive_less(X1,X0) )
| spl0_1 ),
inference(resolution,[],[f2361,f1936]) ).
fof(f44521,plain,
( ! [X0] :
( ~ rdn_positive_less(X0,rdn(rdnn(n0),rdnn(n3)))
| ~ rdn_translate(n12,rdn_pos(X0)) )
| spl0_1 ),
inference(resolution,[],[f44162,f1686]) ).
fof(f44638,plain,
( ! [X0,X1] :
( ~ rdn_translate(n12,rdn_pos(rdn(rdnn(X0),X1)))
| ~ rdn_positive_less(X1,rdnn(n3)) )
| spl0_1 ),
inference(resolution,[],[f44521,f1931]) ).
fof(f44680,plain,
( ! [X0] :
( ~ rdn_positive_less(rdnn(n3),X0)
| ~ rdn_translate(n24,rdn_pos(X0)) )
| spl0_145 ),
inference(resolution,[],[f42740,f1659]) ).
fof(f44705,plain,
( ! [X0,X1] :
( ~ rdn_translate(n24,rdn_pos(rdn(rdnn(X0),X1)))
| ~ rdn_non_zero(X1) )
| spl0_145 ),
inference(resolution,[],[f44680,f1933]) ).
fof(f44709,plain,
( ~ rdn_non_zero(rdnn(n2))
| spl0_145 ),
inference(resolution,[],[f44705,f1680]) ).
fof(f44710,plain,
( $false
| spl0_145
| ~ spl0_571 ),
inference(forward_subsumption_resolution,[],[f44709,f43714]) ).
fof(f44711,plain,
( spl0_145
| ~ spl0_571 ),
inference(avatar_contradiction_clause,[],[f44710]) ).
fof(f45958,plain,
( ~ rdn_positive_less(rdnn(n1),rdnn(n3))
| spl0_1 ),
inference(resolution,[],[f44638,f1668]) ).
fof(f45965,plain,
( ! [X0] :
( ~ rdn_positive_less(rdnn(n1),rdnn(X0))
| ~ rdn_positive_less(rdnn(X0),rdnn(n3)) )
| spl0_1 ),
inference(resolution,[],[f45958,f1930]) ).
fof(f45974,plain,
( ~ rdn_positive_less(rdnn(n1),rdnn(n2))
| spl0_1 ),
inference(resolution,[],[f45965,f1923]) ).
fof(f45975,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f45974,f1922]) ).
fof(f45976,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f45975]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f2332]) ).
cnf(s340,plain,
spl0_3,
inference(sat_conversion,[],[f42672]) ).
cnf(s347,plain,
( spl0_2
| ~ spl0_145 ),
inference(sat_conversion,[],[f42718]) ).
cnf(s398,plain,
spl0_571,
inference(sat_conversion,[],[f43724]) ).
cnf(s424,plain,
( spl0_145
| ~ spl0_571 ),
inference(sat_conversion,[],[f44711]) ).
cnf(s454,plain,
spl0_1,
inference(sat_conversion,[],[f45976]) ).
cnf(s464,plain,
spl0_145,
inference(rat,[],[s424,s398]) ).
cnf(s480,plain,
spl0_2,
inference(rat,[],[s347,s464]) ).
cnf(s507,plain,
$false,
inference(rat,[],[s1,s340,s480,s454]) ).
fof(f45977,plain,
$false,
inference(avatar_sat_refutation,[],[s507]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT010+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:11:13 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.44/1.79 % (1888772)Will run a generic schedule for satisfiability detection.
% 8.44/1.79 % (1888777)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2533554588_2999 on theBenchmark for (2999ds/0Mi)
% 8.44/1.79 % (1888778)% WARNING: option uhcvi not known.
% 8.44/1.79 % (1888781)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3810952035:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.44/1.79 % (1888779)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3533494417:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.44/1.79 % (1888778)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=748905445:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.44/1.79 % (1888780)dis+10_1_sil=32000:sp=arity:random_seed=3321869245:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.44/1.79 % (1888782)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1947977447:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.44/1.79 % (1888783)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1417687640:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.44/1.79 % TRYING [1]
% 8.44/1.79 % TRYING [2]
% 8.44/1.79 % TRYING [3]
% 8.44/1.79 % (1888780)Instruction limit reached!
% 8.44/1.79 % (1888780)------------------------------
% 8.44/1.79 % (1888780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888780)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888780)Termination reason: Instruction limit
% 8.44/1.79 % (1888780)Termination phase: Saturation
% 8.44/1.79 % (1888780)Time elapsed: 0.051 s
% 8.44/1.79 % (1888780)Peak memory usage: 13 MB
% 8.44/1.79 % (1888780)Instructions burned: 104 (million)
% 8.44/1.79 % TRYING [4]
% 8.44/1.79 % (1888781)Instruction limit reached!
% 8.44/1.79 % (1888781)------------------------------
% 8.44/1.79 % (1888781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888781)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888781)Termination reason: Instruction limit
% 8.44/1.79 % (1888781)Termination phase: Saturation
% 8.44/1.79 % (1888781)Time elapsed: 0.058 s
% 8.44/1.79 % (1888781)Peak memory usage: 14 MB
% 8.44/1.79 % (1888781)Instructions burned: 117 (million)
% 8.44/1.79 % (1888783)Instruction limit reached!
% 8.44/1.79 % (1888783)------------------------------
% 8.44/1.79 % (1888783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888783)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888783)Termination reason: Instruction limit
% 8.44/1.79 % (1888783)Termination phase: Saturation
% 8.44/1.79 % (1888783)Time elapsed: 0.062 s
% 8.44/1.79 % (1888783)Peak memory usage: 13 MB
% 8.44/1.79 % (1888783)Instructions burned: 159 (million)
% 8.44/1.79 % (1888782)Instruction limit reached!
% 8.44/1.79 % (1888782)------------------------------
% 8.44/1.79 % (1888782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888782)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888782)Termination reason: Instruction limit
% 8.44/1.79 % (1888782)Termination phase: Saturation
% 8.44/1.79 % (1888782)Time elapsed: 0.064 s
% 8.44/1.79 % (1888782)Peak memory usage: 15 MB
% 8.44/1.79 % (1888782)Instructions burned: 131 (million)
% 8.44/1.79 % (1888791)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3952365664:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.44/1.79 % (1888792)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1976747441:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.44/1.79 % (1888793)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=354694052:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.44/1.79 % (1888794)ott-21_1_sil=16000:fs=off:random_seed=3506780934:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.44/1.79 % TRYING [1]
% 8.44/1.79 % TRYING [2]
% 8.44/1.79 % TRYING [3]
% 8.44/1.79 % TRYING [5]
% 8.44/1.79 % (1888792)Instruction limit reached!
% 8.44/1.79 % (1888792)------------------------------
% 8.44/1.79 % (1888792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888792)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888792)Termination reason: Instruction limit
% 8.44/1.79 % (1888792)Termination phase: Saturation
% 8.44/1.79 % (1888792)Time elapsed: 0.067 s
% 8.44/1.79 % (1888792)Peak memory usage: 15 MB
% 8.44/1.79 % (1888792)Instructions burned: 134 (million)
% 8.44/1.79 % (1888799)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2482999931:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.44/1.79 % (1888794)Instruction limit reached!
% 8.44/1.79 % (1888794)------------------------------
% 8.44/1.79 % (1888794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888794)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888794)Termination reason: Instruction limit
% 8.44/1.79 % (1888794)Termination phase: Saturation
% 8.44/1.79 % (1888794)Time elapsed: 0.084 s
% 8.44/1.79 % (1888794)Peak memory usage: 13 MB
% 8.44/1.79 % (1888794)Instructions burned: 182 (million)
% 8.44/1.79 % (1888801)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3425376802:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.44/1.79 % TRYING [4]
% 8.44/1.79 % TRYING [1]
% 8.44/1.79 % TRYING [2]
% 8.44/1.79 % TRYING [3]
% 8.44/1.79 % (1888791)Instruction limit reached!
% 8.44/1.79 % (1888791)------------------------------
% 8.44/1.79 % (1888791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888791)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888791)Termination reason: Instruction limit
% 8.44/1.79 % (1888791)Termination phase: Finite model building SAT solving
% 8.44/1.79 % (1888791)Time elapsed: 0.303 s
% 8.44/1.79 % (1888791)Peak memory usage: 32 MB
% 8.44/1.79 % (1888791)Instructions burned: 715 (million)
% 8.44/1.79 % TRYING [6]
% 8.44/1.79 % (1888803)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4189325534:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 8.44/1.79 % (1888799)Instruction limit reached!
% 8.44/1.79 % (1888799)------------------------------
% 8.44/1.79 % (1888799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888799)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888799)Termination reason: Instruction limit
% 8.44/1.79 % (1888799)Termination phase: Saturation
% 8.44/1.79 % (1888799)Time elapsed: 0.236 s
% 8.44/1.79 % (1888799)Peak memory usage: 17 MB
% 8.44/1.79 % (1888799)Instructions burned: 477 (million)
% 8.44/1.79 % (1888805)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4139015605:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 8.44/1.79 % (1888793)Instruction limit reached!
% 8.44/1.79 % (1888793)------------------------------
% 8.44/1.79 % (1888793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888793)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888793)Termination reason: Instruction limit
% 8.44/1.79 % (1888793)Termination phase: Saturation
% 8.44/1.79 % (1888793)Time elapsed: 0.357 s
% 8.44/1.79 % (1888793)Peak memory usage: 23 MB
% 8.44/1.79 % (1888793)Instructions burned: 685 (million)
% 8.44/1.79 % (1888807)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=3129581328:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 8.44/1.79 % TRYING [14]
% 8.44/1.79 % (1888801)Instruction limit reached!
% 8.44/1.79 % (1888801)------------------------------
% 8.44/1.79 % (1888801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888801)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888801)Termination reason: Instruction limit
% 8.44/1.79 % (1888801)Termination phase: Finite model building SAT solving
% 8.44/1.79 % (1888801)Time elapsed: 0.320 s
% 8.44/1.79 % (1888801)Peak memory usage: 21 MB
% 8.44/1.79 % (1888801)Instructions burned: 868 (million)
% 8.44/1.79 % (1888809)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3690984079:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 8.44/1.79 % TRYING [7]
% 8.44/1.79 % (1888805)Instruction limit reached!
% 8.44/1.79 % (1888805)------------------------------
% 8.44/1.79 % (1888805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888805)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888805)Termination reason: Instruction limit
% 8.44/1.79 % (1888805)Termination phase: Finite model building constraint generation
% 8.44/1.79 % (1888805)Time elapsed: 0.328 s
% 8.44/1.79 % (1888805)Peak memory usage: 75 MB
% 8.44/1.79 % (1888805)Instructions burned: 890 (million)
% 8.44/1.79 % (1888811)fmb+10_1_sil=64000:random_seed=1900430016:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 8.44/1.79 % TRYING [1]
% 8.44/1.79 % (1888807)Instruction limit reached!
% 8.44/1.79 % (1888807)------------------------------
% 8.44/1.79 % (1888807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888807)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888807)Termination reason: Instruction limit
% 8.44/1.79 % (1888807)Termination phase: Saturation
% 8.44/1.79 % (1888807)Time elapsed: 0.362 s
% 8.44/1.79 % (1888807)Peak memory usage: 24 MB
% 8.44/1.79 % (1888807)Instructions burned: 692 (million)
% 8.44/1.79 % TRYING [2]
% 8.44/1.79 % (1888813)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3989977960:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 8.44/1.79 % TRYING [3]
% 8.44/1.79 % TRYING [20]
% 8.44/1.79 % (1888803)Instruction limit reached!
% 8.44/1.79 % (1888803)------------------------------
% 8.44/1.79 % (1888803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888803)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888803)Termination reason: Instruction limit
% 8.44/1.79 % (1888803)Termination phase: Saturation
% 8.44/1.79 % (1888803)Time elapsed: 0.509 s
% 8.44/1.79 % (1888803)Peak memory usage: 26 MB
% 8.44/1.79 % (1888803)Instructions burned: 1179 (million)
% 8.44/1.79 % (1888815)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2728872594:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 8.44/1.79 % (1888809)Instruction limit reached!
% 8.44/1.79 % (1888809)------------------------------
% 8.44/1.79 % (1888809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888809)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888809)Termination reason: Instruction limit
% 8.44/1.79 % (1888809)Termination phase: Saturation
% 8.44/1.79 % (1888809)Time elapsed: 0.405 s
% 8.44/1.79 % (1888809)Peak memory usage: 24 MB
% 8.44/1.79 % (1888809)Instructions burned: 880 (million)
% 8.44/1.79 % (1888817)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4064190538:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 8.44/1.79 % TRYING [8]
% 8.44/1.79 % TRYING [4]
% 8.44/1.79 % (1888815)Instruction limit reached!
% 8.44/1.79 % (1888815)------------------------------
% 8.44/1.79 % (1888815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.44/1.79 % (1888815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.44/1.79 % (1888815)CaDiCaL version: 2.1.3
% 8.44/1.79 % (1888815)Termination reason: Instruction limit
% 8.44/1.79 % (1888815)Termination phase: Finite model building constraint generation
% 8.44/1.79 % (1888815)Time elapsed: 0.327 s
% 8.44/1.79 % (1888815)Peak memory usage: 68 MB
% 8.44/1.79 % (1888815)Instructions burned: 921 (million)
% 8.44/1.79 % (1888819)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=784872626:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 8.44/1.79 % (1888817) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1888772-1888817"...
% 8.44/1.79 % (1888817)...printing done.
% 8.44/1.79 % (1888817)Refutation found. Thanks to Tanya!
% 8.44/1.79 % SZS status Theorem for theBenchmark
% 8.44/1.79 % SZS output start Proof for theBenchmark
% See solution above
% 10.97/1.80 % (1888817)------------------------------
% 10.97/1.80 % (1888817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.97/1.80 % (1888817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/1.80 % (1888817)CaDiCaL version: 2.1.3
% 10.97/1.80 % (1888817)Termination reason: Refutation
% 10.97/1.80 % (1888817)Time elapsed: 0.520 s
% 10.97/1.80 % (1888817)Peak memory usage: 26 MB
% 10.97/1.80 % (1888817)Instructions burned: 1017 (million)
% 10.97/1.80 % (1888772)Success in time 1.557 s
% 10.97/1.80 % Vampire exiting
%------------------------------------------------------------------------------