%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : AGT006+1 : 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 : n015.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 116.11s 19.46s
% Output : Refutation 116.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 28
% Syntax : Number of formulae : 121 ( 59 unt; 3 def)
% Number of atoms : 321 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 321 ( 121 ~; 117 |; 69 &)
% ( 8 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 4 prp; 0-4 aty)
% Number of functors : 30 ( 30 usr; 27 con; 0-2 aty)
% Number of variables : 117 ( 0 sgn 117 !; 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/sandbox/benchmark/Axioms/AGT001+0.ax',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/sandbox/benchmark/Axioms/AGT001+0.ax',a1_3) ).
fof(f4,axiom,
! [X0,X1,X2] :
( the_agent_in_all_proposed_teams(X0,X1,X2)
=> ( accept_leader(X0,X1)
& accept_city(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax',a1_4) ).
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/sandbox/benchmark/Axioms/AGT001+0.ax',a2_1) ).
fof(f14,axiom,
! [X0] :
( ( accept_population(X0,atheist,n12)
& accept_population(X0,christian,n3)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n85)
& accept_population(X0,other,n0) )
<=> accept_city(X0,coastvillage) ),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax',a2_7) ).
fof(f19,axiom,
! [X0] :
( ( accept_population(X0,atheist,n78)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n1)
& accept_population(X0,native,n0)
& accept_population(X0,other,n1) )
<=> accept_city(X0,cityb) ),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax',a2_12) ).
fof(f20,axiom,
! [X0] :
( ( accept_population(X0,atheist,n30)
& accept_population(X0,christian,n0)
& accept_population(X0,muslim,n65)
& accept_population(X0,native,n0)
& accept_population(X0,other,n5) )
<=> accept_city(X0,townc) ),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax',a2_13) ).
fof(f38,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax',event_18) ).
fof(f94,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax',event_74) ).
fof(f100,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax',event_80) ).
fof(f274,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn4) ).
fof(f275,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn5) ).
fof(f277,axiom,
rdn_translate(n7,rdn_pos(rdnn(n7))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn7) ).
fof(f335,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn65) ).
fof(f348,axiom,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn78) ).
fof(f355,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax',rdn85) ).
fof(f531,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_digit6) ).
fof(f533,axiom,
rdn_non_zero_digit(rdnn(n8)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_digit8) ).
fof(f539,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_positive_less45) ).
fof(f541,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax',rdn_positive_less67) ).
fof(f545,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(f547,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(f548,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(f550,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(f556,conjecture,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query_6) ).
fof(f557,negated_conjecture,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(negated_conjecture,[status(cth)],[f556]) ).
fof(f558,plain,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(flattening,[],[f557]) ).
fof(f565,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(ennf_transformation,[],[f3]) ).
fof(f566,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(flattening,[],[f565]) ).
fof(f567,plain,
! [X0,X1,X2] :
( ( accept_leader(X0,X1)
& accept_city(X0,X2) )
| ~ the_agent_in_all_proposed_teams(X0,X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f573,plain,
! [X0,X1,X2,X3] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3))
| ~ rdn_positive_less(X1,X3) ),
inference(ennf_transformation,[],[f545]) ).
fof(f576,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2) ),
inference(ennf_transformation,[],[f547]) ).
fof(f577,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(ennf_transformation,[],[f548]) ).
fof(f579,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,[],[f550]) ).
fof(f580,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,[],[f579]) ).
fof(f585,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(f586,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,[],[f585]) ).
fof(f587,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(f588,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,[],[f587]) ).
fof(f599,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n12)
& accept_population(X0,christian,n3)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n85)
& accept_population(X0,other,n0) )
| ~ accept_city(X0,coastvillage) )
& ( accept_city(X0,coastvillage)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,other,n0) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f600,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n12)
& accept_population(X0,christian,n3)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n85)
& accept_population(X0,other,n0) )
| ~ accept_city(X0,coastvillage) )
& ( accept_city(X0,coastvillage)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,other,n0) ) ),
inference(flattening,[],[f599]) ).
fof(f609,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n78)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n1)
& accept_population(X0,native,n0)
& accept_population(X0,other,n1) )
| ~ accept_city(X0,cityb) )
& ( accept_city(X0,cityb)
| ~ accept_population(X0,atheist,n78)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n1) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f610,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n78)
& accept_population(X0,christian,n20)
& accept_population(X0,muslim,n1)
& accept_population(X0,native,n0)
& accept_population(X0,other,n1) )
| ~ accept_city(X0,cityb) )
& ( accept_city(X0,cityb)
| ~ accept_population(X0,atheist,n78)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n1) ) ),
inference(flattening,[],[f609]) ).
fof(f611,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n30)
& accept_population(X0,christian,n0)
& accept_population(X0,muslim,n65)
& accept_population(X0,native,n0)
& accept_population(X0,other,n5) )
| ~ accept_city(X0,townc) )
& ( accept_city(X0,townc)
| ~ accept_population(X0,atheist,n30)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,muslim,n65)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n5) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f612,plain,
! [X0] :
( ( ( accept_population(X0,atheist,n30)
& accept_population(X0,christian,n0)
& accept_population(X0,muslim,n65)
& accept_population(X0,native,n0)
& accept_population(X0,other,n5) )
| ~ accept_city(X0,townc) )
& ( accept_city(X0,townc)
| ~ accept_population(X0,atheist,n30)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,muslim,n65)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n5) ) ),
inference(flattening,[],[f611]) ).
fof(f615,plain,
! [X2,X3,X0,X1] :
( ~ accept_team(X0,X3,X1,X2)
| accept_number(X0,X2) ),
inference(cnf_transformation,[],[f586]) ).
fof(f616,plain,
! [X2,X3,X0,X1] :
( ~ accept_team(X0,X3,X1,X2)
| accept_leader(X0,X3) ),
inference(cnf_transformation,[],[f586]) ).
fof(f617,plain,
! [X2,X3,X0,X1] :
( ~ accept_team(X0,X3,X1,X2)
| accept_city(X0,X1) ),
inference(cnf_transformation,[],[f586]) ).
fof(f618,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,[],[f586]) ).
fof(f620,plain,
! [X2,X3,X0,X1] :
( ~ accept_population(X0,X3,X1)
| accept_population(X0,X3,X2)
| ~ less(X2,X1) ),
inference(cnf_transformation,[],[f566]) ).
fof(f621,plain,
! [X2,X0,X1] :
( ~ the_agent_in_all_proposed_teams(X0,X1,X2)
| accept_city(X0,X2) ),
inference(cnf_transformation,[],[f567]) ).
fof(f625,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,[],[f588]) ).
fof(f663,plain,
! [X0] :
( ~ accept_city(X0,coastvillage)
| accept_population(X0,native,n85) ),
inference(cnf_transformation,[],[f600]) ).
fof(f695,plain,
! [X0] :
( ~ accept_city(X0,cityb)
| accept_population(X0,christian,n20) ),
inference(cnf_transformation,[],[f610]) ).
fof(f696,plain,
! [X0] :
( ~ accept_city(X0,cityb)
| accept_population(X0,atheist,n78) ),
inference(cnf_transformation,[],[f610]) ).
fof(f698,plain,
! [X0] :
( ~ accept_city(X0,townc)
| accept_population(X0,other,n5) ),
inference(cnf_transformation,[],[f612]) ).
fof(f700,plain,
! [X0] :
( ~ accept_city(X0,townc)
| accept_population(X0,muslim,n65) ),
inference(cnf_transformation,[],[f612]) ).
fof(f720,plain,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n4),
inference(cnf_transformation,[],[f38]) ).
fof(f776,plain,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(cnf_transformation,[],[f94]) ).
fof(f782,plain,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc),
inference(cnf_transformation,[],[f100]) ).
fof(f956,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(cnf_transformation,[],[f274]) ).
fof(f957,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(cnf_transformation,[],[f275]) ).
fof(f959,plain,
rdn_translate(n7,rdn_pos(rdnn(n7))),
inference(cnf_transformation,[],[f277]) ).
fof(f1017,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(cnf_transformation,[],[f335]) ).
fof(f1030,plain,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
inference(cnf_transformation,[],[f348]) ).
fof(f1037,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(cnf_transformation,[],[f355]) ).
fof(f1213,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(cnf_transformation,[],[f531]) ).
fof(f1215,plain,
rdn_non_zero_digit(rdnn(n8)),
inference(cnf_transformation,[],[f533]) ).
fof(f1221,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f539]) ).
fof(f1223,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(cnf_transformation,[],[f541]) ).
fof(f1227,plain,
! [X2,X3,X0,X1] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3))
| ~ rdn_positive_less(X1,X3) ),
inference(cnf_transformation,[],[f573]) ).
fof(f1229,plain,
! [X2,X0,X1] :
( ~ rdn_non_zero(X2)
| rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2)) ),
inference(cnf_transformation,[],[f576]) ).
fof(f1230,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(X0))
| rdn_non_zero(rdnn(X0)) ),
inference(cnf_transformation,[],[f577]) ).
fof(f1232,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,[],[f580]) ).
fof(f1238,plain,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,suffertown,n4),
inference(cnf_transformation,[],[f558]) ).
fof(f1245,plain,
rdn_non_zero(rdnn(n8)),
inference(unit_resulting_resolution,[],[f1230,f1215]) ).
fof(f1248,plain,
rdn_non_zero(rdnn(n6)),
inference(unit_resulting_resolution,[],[f1230,f1213]) ).
fof(f1279,plain,
accept_city(countrybcivilorganization,townc),
inference(unit_resulting_resolution,[],[f621,f782]) ).
fof(f1591,plain,
accept_population(countrybcivilorganization,other,n5),
inference(unit_resulting_resolution,[],[f698,f1279]) ).
fof(f1615,plain,
accept_population(countrybcivilorganization,muslim,n65),
inference(unit_resulting_resolution,[],[f700,f1279]) ).
fof(f1745,plain,
accept_number(countrybcivilorganization,n4),
inference(unit_resulting_resolution,[],[f615,f720]) ).
fof(f1969,plain,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization),
inference(unit_resulting_resolution,[],[f616,f720]) ).
fof(f2193,plain,
accept_city(countrybcivilorganization,cityb),
inference(unit_resulting_resolution,[],[f617,f720]) ).
fof(f2197,plain,
accept_city(countrybcivilorganization,coastvillage),
inference(unit_resulting_resolution,[],[f617,f776]) ).
fof(f2476,plain,
accept_population(countrybcivilorganization,atheist,n78),
inference(unit_resulting_resolution,[],[f696,f2193]) ).
fof(f2477,plain,
accept_population(countrybcivilorganization,christian,n20),
inference(unit_resulting_resolution,[],[f695,f2193]) ).
fof(f2489,plain,
accept_population(countrybcivilorganization,native,n85),
inference(unit_resulting_resolution,[],[f663,f2197]) ).
fof(f2541,plain,
! [X0,X1] : rdn_positive_less(rdnn(X0),rdn(rdnn(X1),rdnn(n8))),
inference(unit_resulting_resolution,[],[f1229,f1245]) ).
fof(f2544,plain,
! [X0,X1] : rdn_positive_less(rdnn(X0),rdn(rdnn(X1),rdnn(n6))),
inference(unit_resulting_resolution,[],[f1229,f1248]) ).
fof(f50234,plain,
! [X0,X1] : rdn_positive_less(rdn(rdnn(X0),rdnn(n6)),rdn(rdnn(X1),rdnn(n7))),
inference(unit_resulting_resolution,[],[f1227,f1223]) ).
fof(f51348,plain,
~ accept_city(countrybcivilorganization,suffertown),
inference(unit_resulting_resolution,[],[f618,f1969,f1238,f1745]) ).
fof(f52214,plain,
less(n4,n5),
inference(unit_resulting_resolution,[],[f1232,f956,f1221,f957]) ).
fof(f52821,plain,
less(n4,n85),
inference(unit_resulting_resolution,[],[f1232,f956,f2541,f1037]) ).
fof(f53180,plain,
less(n7,n65),
inference(unit_resulting_resolution,[],[f1232,f959,f2544,f1017]) ).
fof(f191597,plain,
accept_population(countrybcivilorganization,other,n4),
inference(unit_resulting_resolution,[],[f620,f1591,f52214]) ).
fof(f310125,plain,
less(n65,n78),
inference(unit_resulting_resolution,[],[f1232,f1030,f1017,f50234]) ).
fof(f560604,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) ),
inference(resolution,[],[f191597,f625]) ).
fof(f560606,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4)
| accept_city(countrybcivilorganization,suffertown) ),
inference(forward_subsumption_resolution,[],[f560604,f2477]) ).
fof(f560609,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| ~ accept_population(countrybcivilorganization,muslim,n7)
| ~ accept_population(countrybcivilorganization,native,n4) ),
inference(forward_subsumption_resolution,[],[f560606,f51348]) ).
fof(f560611,definition,
( spl0_1
<=> accept_population(countrybcivilorganization,native,n4) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f560613,plain,
( ~ accept_population(countrybcivilorganization,native,n4)
| spl0_1 ),
inference(avatar_component_clause,[],[f560611]) ).
fof(f560615,definition,
( spl0_2
<=> accept_population(countrybcivilorganization,muslim,n7) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f560617,plain,
( ~ accept_population(countrybcivilorganization,muslim,n7)
| spl0_2 ),
inference(avatar_component_clause,[],[f560615]) ).
fof(f560619,definition,
( spl0_3
<=> accept_population(countrybcivilorganization,atheist,n65) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f560621,plain,
( ~ accept_population(countrybcivilorganization,atheist,n65)
| spl0_3 ),
inference(avatar_component_clause,[],[f560619]) ).
fof(f560622,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f560609,f560619,f560615,f560611]) ).
fof(f560721,plain,
( ~ less(n4,n85)
| spl0_1 ),
inference(unit_resulting_resolution,[],[f620,f2489,f560613]) ).
fof(f560857,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f560721,f52821]) ).
fof(f560858,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f560857]) ).
fof(f561088,plain,
( ~ less(n7,n65)
| spl0_2 ),
inference(unit_resulting_resolution,[],[f620,f1615,f560617]) ).
fof(f561226,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f561088,f53180]) ).
fof(f561227,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f561226]) ).
fof(f561383,plain,
( ~ less(n65,n78)
| spl0_3 ),
inference(unit_resulting_resolution,[],[f620,f2476,f560621]) ).
fof(f561527,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f561383,f310125]) ).
fof(f561528,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f561527]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f560622]) ).
cnf(s6,plain,
spl0_1,
inference(sat_conversion,[],[f560858]) ).
cnf(s11,plain,
spl0_2,
inference(sat_conversion,[],[f561227]) ).
cnf(s21,plain,
spl0_3,
inference(sat_conversion,[],[f561528]) ).
cnf(s22,plain,
$false,
inference(rat,[],[s1,s21,s11,s6]) ).
fof(f561529,plain,
$false,
inference(avatar_sat_refutation,[],[s22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : AGT006+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n015.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 19:12:02 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 Running first-order model finding
% 0.10/0.20 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
% 21.12/3.26 % (2922373)Will run a generic schedule for satisfiability detection.
% 21.12/3.26 % (2922380)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1240485442:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 21.12/3.26 % (2922379)% WARNING: option uhcvi not known.
% 21.12/3.26 % (2922378)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=277419368_2999 on theBenchmark for (2999ds/0Mi)
% 21.12/3.26 % (2922381)dis+10_1_sil=32000:sp=arity:random_seed=1543180917:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 21.12/3.26 % (2922382)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=740275645:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 21.12/3.26 % (2922383)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3888672236:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 21.12/3.26 % (2922384)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3532934868:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 21.12/3.26 % (2922379)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1393811949:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 21.12/3.26 % TRYING [1]
% 21.12/3.26 % TRYING [2]
% 21.12/3.26 % (2922381)Instruction limit reached!
% 21.12/3.26 % (2922381)------------------------------
% 21.12/3.26 % (2922381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.12/3.26 % (2922381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.12/3.26 % (2922381)CaDiCaL version: 2.1.3
% 21.12/3.26 % (2922381)Termination reason: Instruction limit
% 21.12/3.26 % (2922381)Termination phase: Saturation
% 21.12/3.26 % (2922381)Time elapsed: 0.050 s
% 21.12/3.26 % (2922381)Peak memory usage: 13 MB
% 21.12/3.26 % (2922381)Instructions burned: 103 (million)
% 21.12/3.26 % TRYING [3]
% 21.12/3.26 % (2922382)Instruction limit reached!
% 21.12/3.26 % (2922382)------------------------------
% 21.12/3.26 % (2922382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.12/3.26 % (2922382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.12/3.26 % (2922382)CaDiCaL version: 2.1.3
% 21.12/3.26 % (2922382)Termination reason: Instruction limit
% 21.12/3.26 % (2922382)Termination phase: Saturation
% 21.12/3.26 % (2922382)Time elapsed: 0.060 s
% 21.12/3.26 % (2922382)Peak memory usage: 13 MB
% 21.12/3.26 % (2922382)Instructions burned: 117 (million)
% 21.12/3.26 % (2922383)Instruction limit reached!
% 21.12/3.26 % (2922383)------------------------------
% 21.12/3.26 % (2922383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.12/3.26 % (2922383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.12/3.26 % (2922383)CaDiCaL version: 2.1.3
% 21.12/3.26 % (2922383)Termination reason: Instruction limit
% 21.12/3.26 % (2922383)Termination phase: Saturation
% 21.12/3.26 % (2922383)Time elapsed: 0.065 s
% 21.12/3.26 % (2922383)Peak memory usage: 14 MB
% 21.12/3.26 % (2922383)Instructions burned: 132 (million)
% 21.12/3.26 % (2922392)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2368064547:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 21.12/3.26 % (2922393)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2411364164:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 21.12/3.26 % (2922394)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=3691297875:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 21.12/3.26 % (2922384)Instruction limit reached!
% 21.12/3.26 % (2922384)------------------------------
% 21.12/3.26 % (2922384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.12/3.26 % (2922384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.12/3.26 % (2922384)CaDiCaL version: 2.1.3
% 21.12/3.26 % (2922384)Termination reason: Instruction limit
% 21.12/3.26 % (2922384)Termination phase: Saturation
% 21.12/3.26 % (2922384)Time elapsed: 0.087 s
% 21.12/3.26 % (2922384)Peak memory usage: 14 MB
% 21.12/3.26 % (2922384)Instructions burned: 159 (million)
% 21.12/3.26 % TRYING [1]
% 21.12/3.26 % TRYING [2]
% 21.12/3.26 % (2922398)ott-21_1_sil=16000:fs=off:random_seed=145523336:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 21.12/3.26 % TRYING [4]
% 21.12/3.26 % TRYING [3]
% 21.12/3.26 % (2922393)Instruction limit reached!
% 21.12/3.26 % (2922393)------------------------------
% 21.12/3.26 % (2922393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.12/3.26 % (2922393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.95/6.71 % (2922393)CaDiCaL version: 2.1.3
% 45.95/6.71 % (2922393)Termination reason: Instruction limit
% 45.95/6.71 % (2922393)Termination phase: Saturation
% 45.95/6.71 % (2922393)Time elapsed: 0.071 s
% 45.95/6.71 % (2922393)Peak memory usage: 14 MB
% 45.95/6.71 % (2922393)Instructions burned: 131 (million)
% 45.95/6.71 % (2922400)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3143907403:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 45.95/6.71 % (2922398)Instruction limit reached!
% 45.95/6.71 % (2922398)------------------------------
% 45.95/6.71 % (2922398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.95/6.71 % (2922398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.95/6.71 % (2922398)CaDiCaL version: 2.1.3
% 45.95/6.71 % (2922398)Termination reason: Instruction limit
% 45.95/6.71 % (2922398)Termination phase: Saturation
% 45.95/6.71 % (2922398)Time elapsed: 0.078 s
% 45.95/6.71 % (2922398)Peak memory usage: 12 MB
% 45.95/6.71 % (2922398)Instructions burned: 180 (million)
% 45.95/6.71 % (2922402)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3893333514:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 45.95/6.71 % TRYING [1]
% 45.95/6.71 % TRYING [2]
% 45.95/6.71 % TRYING [4]
% 45.95/6.71 % TRYING [3]
% 45.95/6.71 % TRYING [5]
% 45.95/6.71 % (2922392)Instruction limit reached!
% 45.95/6.71 % (2922392)------------------------------
% 45.95/6.71 % (2922392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.95/6.71 % (2922392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.95/6.71 % (2922392)CaDiCaL version: 2.1.3
% 45.95/6.71 % (2922392)Termination reason: Instruction limit
% 45.95/6.71 % (2922392)Termination phase: Finite model building SAT solving
% 45.95/6.71 % (2922392)Time elapsed: 0.314 s
% 45.95/6.71 % (2922392)Peak memory usage: 30 MB
% 45.95/6.71 % (2922392)Instructions burned: 714 (million)
% 45.95/6.71 % (2922404)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3572481917:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 45.95/6.71 % (2922400)Instruction limit reached!
% 45.95/6.71 % (2922400)------------------------------
% 45.95/6.71 % (2922400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.95/6.71 % (2922400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.95/6.71 % (2922400)CaDiCaL version: 2.1.3
% 45.95/6.71 % (2922400)Termination reason: Instruction limit
% 45.95/6.71 % (2922400)Termination phase: Saturation
% 45.95/6.71 % (2922400)Time elapsed: 0.245 s
% 45.95/6.71 % (2922400)Peak memory usage: 17 MB
% 45.95/6.71 % (2922400)Instructions burned: 477 (million)
% 45.95/6.71 % (2922406)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3335462033:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 45.95/6.71 % (2922394)Instruction limit reached!
% 45.95/6.71 % (2922394)------------------------------
% 45.95/6.71 % (2922394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.95/6.71 % (2922394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.95/6.71 % (2922394)CaDiCaL version: 2.1.3
% 45.95/6.71 % (2922394)Termination reason: Instruction limit
% 45.95/6.71 % (2922394)Termination phase: Saturation
% 45.95/6.71 % (2922394)Time elapsed: 0.355 s
% 45.95/6.71 % (2922394)Peak memory usage: 23 MB
% 45.95/6.71 % (2922394)Instructions burned: 685 (million)
% 45.95/6.71 % (2922408)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=2504308610: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)
% 45.95/6.71 % TRYING [4]
% 45.95/6.71 % (2922402)Instruction limit reached!
% 45.95/6.71 % (2922402)------------------------------
% 45.95/6.71 % (2922402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.95/6.71 % (2922402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.95/6.71 % (2922402)CaDiCaL version: 2.1.3
% 45.95/6.71 % (2922402)Termination reason: Instruction limit
% 45.95/6.71 % (2922402)Termination phase: Finite model building constraint generation
% 45.95/6.71 % (2922402)Time elapsed: 0.307 s
% 45.95/6.71 % (2922402)Peak memory usage: 21 MB
% 45.95/6.71 % (2922402)Instructions burned: 868 (million)
% 45.95/6.71 % TRYING [14]
% 45.95/6.71 % (2922410)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=559639464:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 45.95/6.71 % (2922406)Instruction limit reached!
% 45.95/6.71 % (2922406)------------------------------
% 94.94/13.68 % (2922406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.94/13.68 % (2922406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.94/13.68 % (2922406)CaDiCaL version: 2.1.3
% 94.94/13.68 % (2922406)Termination reason: Instruction limit
% 94.94/13.68 % (2922406)Termination phase: Finite model building constraint generation
% 94.94/13.68 % (2922406)Time elapsed: 0.326 s
% 94.94/13.68 % (2922406)Peak memory usage: 73 MB
% 94.94/13.68 % (2922406)Instructions burned: 889 (million)
% 94.94/13.68 % (2922412)fmb+10_1_sil=64000:random_seed=1110666375:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 94.94/13.68 % (2922408)Instruction limit reached!
% 94.94/13.68 % (2922408)------------------------------
% 94.94/13.68 % (2922408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.94/13.68 % (2922408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.94/13.68 % (2922408)CaDiCaL version: 2.1.3
% 94.94/13.68 % (2922408)Termination reason: Instruction limit
% 94.94/13.68 % (2922408)Termination phase: Saturation
% 94.94/13.68 % (2922408)Time elapsed: 0.348 s
% 94.94/13.68 % (2922408)Peak memory usage: 23 MB
% 94.94/13.68 % (2922408)Instructions burned: 694 (million)
% 94.94/13.68 % TRYING [1]
% 94.94/13.68 % TRYING [2]
% 94.94/13.68 % (2922414)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1216372118:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 94.94/13.68 % TRYING [20]
% 94.94/13.68 % (2922410)Instruction limit reached!
% 94.94/13.68 % (2922410)------------------------------
% 94.94/13.68 % (2922410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.94/13.68 % (2922410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.94/13.68 % (2922410)CaDiCaL version: 2.1.3
% 94.94/13.68 % (2922410)Termination reason: Instruction limit
% 94.94/13.68 % (2922410)Termination phase: Saturation
% 94.94/13.68 % (2922410)Time elapsed: 0.355 s
% 94.94/13.68 % (2922410)Peak memory usage: 20 MB
% 94.94/13.68 % (2922410)Instructions burned: 880 (million)
% 94.94/13.68 % TRYING [3]
% 94.94/13.68 % (2922416)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1937170912:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 94.94/13.68 % TRYING [8]
% 94.94/13.68 % TRYING [6]
% 94.94/13.68 % (2922404)Instruction limit reached!
% 94.94/13.68 % (2922404)------------------------------
% 94.94/13.68 % (2922404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.94/13.68 % (2922404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.94/13.68 % (2922404)CaDiCaL version: 2.1.3
% 94.94/13.68 % (2922404)Termination reason: Instruction limit
% 94.94/13.68 % (2922404)Termination phase: Saturation
% 94.94/13.68 % (2922404)Time elapsed: 0.623 s
% 94.94/13.68 % (2922404)Peak memory usage: 34 MB
% 94.94/13.68 % (2922404)Instructions burned: 1180 (million)
% 94.94/13.68 % (2922418)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=48710625:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 94.94/13.68 % TRYING [4]
% 94.94/13.68 % (2922416)Instruction limit reached!
% 94.94/13.68 % (2922416)------------------------------
% 94.94/13.68 % (2922416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.94/13.68 % (2922416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.94/13.68 % (2922416)CaDiCaL version: 2.1.3
% 94.94/13.68 % (2922416)Termination reason: Instruction limit
% 94.94/13.68 % (2922416)Termination phase: Finite model building constraint generation
% 94.94/13.68 % (2922416)Time elapsed: 0.331 s
% 94.94/13.68 % (2922416)Peak memory usage: 68 MB
% 94.94/13.68 % (2922416)Instructions burned: 921 (million)
% 94.94/13.68 % (2922420)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2866349014:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 94.94/13.68 % TRYING [5]
% 94.94/13.68 % TRYING [7]
% 94.94/13.68 % (2922420)Instruction limit reached!
% 94.94/13.68 % (2922420)------------------------------
% 94.94/13.68 % (2922420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.94/13.68 % (2922420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.94/13.68 % (2922420)CaDiCaL version: 2.1.3
% 94.94/13.68 % (2922420)Termination reason: Instruction limit
% 94.94/13.68 % (2922420)Termination phase: Saturation
% 94.94/13.68 % (2922420)Time elapsed: 0.772 s
% 94.94/13.68 % (2922420)Peak memory usage: 30 MB
% 94.94/13.68 % (2922420)Instructions burned: 1473 (million)
% 94.94/13.68 % (2922422)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=505807373:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 94.94/13.68 % TRYING [77]
% 94.94/13.68 % TRYING [6]
% 94.94/13.68 % TRYING [8]
% 116.11/19.46 % TRYING [7]
% 116.11/19.46 % (2922418)Instruction limit reached!
% 116.11/19.46 % (2922418)------------------------------
% 116.11/19.46 % (2922418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922418)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922418)Termination reason: Instruction limit
% 116.11/19.46 % (2922418)Termination phase: Saturation
% 116.11/19.46 % (2922418)Time elapsed: 2.684 s
% 116.11/19.46 % (2922418)Peak memory usage: 47 MB
% 116.11/19.46 % (2922418)Instructions burned: 5133 (million)
% 116.11/19.46 % (2922424)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3583881311:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 116.11/19.46 % TRYING [16]
% 116.11/19.46 % (2922414)Instruction limit reached!
% 116.11/19.46 % (2922414)------------------------------
% 116.11/19.46 % (2922414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922414)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922414)Termination reason: Instruction limit
% 116.11/19.46 % (2922414)Termination phase: Finite model building constraint generation
% 116.11/19.46 % (2922414)Time elapsed: 3.484 s
% 116.11/19.46 % (2922414)Peak memory usage: 554 MB
% 116.11/19.46 % (2922414)Instructions burned: 9516 (million)
% 116.11/19.46 % (2922426)ott-2_1_sil=16000:newcnf=on:random_seed=3135332734:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 116.11/19.46 % (2922422)Instruction limit reached!
% 116.11/19.46 % (2922422)------------------------------
% 116.11/19.46 % (2922422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922422)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922422)Termination reason: Instruction limit
% 116.11/19.46 % (2922422)Termination phase: Finite model building constraint generation
% 116.11/19.46 % (2922422)Time elapsed: 2.352 s
% 116.11/19.46 % (2922422)Peak memory usage: 524 MB
% 116.11/19.46 % (2922422)Instructions burned: 6327 (million)
% 116.11/19.46 % (2922428)ott+10_1_sil=32000:tgt=ground:random_seed=3903825533:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 116.11/19.46 % (2922424)Instruction limit reached!
% 116.11/19.46 % (2922424)------------------------------
% 116.11/19.46 % (2922424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922424)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922424)Termination reason: Instruction limit
% 116.11/19.46 % (2922424)Termination phase: Finite model building constraint generation
% 116.11/19.46 % (2922424)Time elapsed: 0.789 s
% 116.11/19.46 % (2922424)Peak memory usage: 153 MB
% 116.11/19.46 % (2922424)Instructions burned: 2176 (million)
% 116.11/19.46 % (2922430)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=786667768:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 116.11/19.46 % TRYING [1]
% 116.11/19.46 % TRYING [2]
% 116.11/19.46 % TRYING [3]
% 116.11/19.46 % TRYING [4]
% 116.11/19.46 % TRYING [9]
% 116.11/19.46 % (2922426)Instruction limit reached!
% 116.11/19.46 % (2922426)------------------------------
% 116.11/19.46 % (2922426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922426)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922426)Termination reason: Instruction limit
% 116.11/19.46 % (2922426)Termination phase: Saturation
% 116.11/19.46 % (2922426)Time elapsed: 0.424 s
% 116.11/19.46 % (2922426)Peak memory usage: 25 MB
% 116.11/19.46 % (2922426)Instructions burned: 870 (million)
% 116.11/19.46 % (2922432)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=248240793:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 116.11/19.46 % TRYING [5]
% 116.11/19.46 % TRYING [6]
% 116.11/19.46 % TRYING [8]
% 116.11/19.46 % TRYING [7]
% 116.11/19.46 % (2922432)Instruction limit reached!
% 116.11/19.46 % (2922432)------------------------------
% 116.11/19.46 % (2922432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922432)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922432)Termination reason: Instruction limit
% 116.11/19.46 % (2922432)Termination phase: Saturation
% 116.11/19.46 % (2922432)Time elapsed: 1.561 s
% 116.11/19.46 % (2922432)Peak memory usage: 38 MB
% 116.11/19.46 % (2922432)Instructions burned: 3512 (million)
% 116.11/19.46 % (2922434)dis+21_1_sil=32000:sas=cadical:random_seed=2469638231:i=3773:amm=off_2935 on theBenchmark for (2935ds/3773Mi)
% 116.11/19.46 % (2922428)Instruction limit reached!
% 116.11/19.46 % (2922428)------------------------------
% 116.11/19.46 % (2922428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922428)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922428)Termination reason: Instruction limit
% 116.11/19.46 % (2922428)Termination phase: Saturation
% 116.11/19.46 % (2922428)Time elapsed: 2.316 s
% 116.11/19.46 % (2922428)Peak memory usage: 73 MB
% 116.11/19.46 % (2922428)Instructions burned: 5114 (million)
% 116.11/19.46 % (2922436)ott+11_1_sil=16000:gs=on:random_seed=1458729774:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 116.11/19.46 % TRYING [10]
% 116.11/19.46 % TRYING [8]
% 116.11/19.46 % (2922436)Instruction limit reached!
% 116.11/19.46 % (2922436)------------------------------
% 116.11/19.46 % (2922436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922436)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922436)Termination reason: Instruction limit
% 116.11/19.46 % (2922436)Termination phase: Saturation
% 116.11/19.46 % (2922436)Time elapsed: 1.245 s
% 116.11/19.46 % (2922436)Peak memory usage: 43 MB
% 116.11/19.46 % (2922436)Instructions burned: 2251 (million)
% 116.11/19.46 % (2922438)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4091844780:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi)
% 116.11/19.46 % TRYING [7]
% 116.11/19.46 % (2922434)Instruction limit reached!
% 116.11/19.46 % (2922434)------------------------------
% 116.11/19.46 % (2922434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922434)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922434)Termination reason: Instruction limit
% 116.11/19.46 % (2922434)Termination phase: Saturation
% 116.11/19.46 % (2922434)Time elapsed: 1.849 s
% 116.11/19.46 % (2922434)Peak memory usage: 74 MB
% 116.11/19.46 % (2922434)Instructions burned: 3774 (million)
% 116.11/19.46 % (2922440)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4248671228:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 116.11/19.46 % (2922412)Instruction limit reached!
% 116.11/19.46 % (2922412)------------------------------
% 116.11/19.46 % (2922412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922412)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922412)Termination reason: Instruction limit
% 116.11/19.46 % (2922412)Termination phase: Finite model building SAT solving
% 116.11/19.46 % (2922412)Time elapsed: 7.868 s
% 116.11/19.46 % (2922412)Peak memory usage: 125 MB
% 116.11/19.46 % (2922412)Instructions burned: 22062 (million)
% 116.11/19.46 % (2922442)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3799868652:i=29340_2912 on theBenchmark for (2912ds/29340Mi)
% 116.11/19.46 % TRYING [9]
% 116.11/19.46 % (2922440)Instruction limit reached!
% 116.11/19.46 % (2922440)------------------------------
% 116.11/19.46 % (2922440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922440)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922440)Termination reason: Instruction limit
% 116.11/19.46 % (2922440)Termination phase: Saturation
% 116.11/19.46 % (2922440)Time elapsed: 2.715 s
% 116.11/19.46 % (2922440)Peak memory usage: 74 MB
% 116.11/19.46 % (2922440)Instructions burned: 4592 (million)
% 116.11/19.46 % (2922444)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=886953423:i=5211_2888 on theBenchmark for (2888ds/5211Mi)
% 116.11/19.46 % TRYING [11]
% 116.11/19.46 % TRYING [10]
% 116.11/19.46 % (2922444)Instruction limit reached!
% 116.11/19.46 % (2922444)------------------------------
% 116.11/19.46 % (2922444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922444)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922444)Termination reason: Instruction limit
% 116.11/19.46 % (2922444)Termination phase: Saturation
% 116.11/19.46 % (2922444)Time elapsed: 2.298 s
% 116.11/19.46 % (2922444)Peak memory usage: 69 MB
% 116.11/19.46 % (2922444)Instructions burned: 5212 (million)
% 116.11/19.46 % (2922446)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=671552154:i=5497:nm=2_2865 on theBenchmark for (2865ds/5497Mi)
% 116.11/19.46 % TRYING [17]
% 116.11/19.46 % (2922446)Instruction limit reached!
% 116.11/19.46 % (2922446)------------------------------
% 116.11/19.46 % (2922446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922446)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922446)Termination reason: Instruction limit
% 116.11/19.46 % (2922446)Termination phase: Finite model building constraint generation
% 116.11/19.46 % (2922446)Time elapsed: 1.933 s
% 116.11/19.46 % (2922446)Peak memory usage: 343 MB
% 116.11/19.46 % (2922446)Instructions burned: 5498 (million)
% 116.11/19.46 % (2922448)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3596022178:fmbsr=2:i=46332_2845 on theBenchmark for (2845ds/46332Mi)
% 116.11/19.46 % TRYING [15]
% 116.11/19.46 % (2922442) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2922373-2922442"...
% 116.11/19.46 % (2922442)...printing done.
% 116.11/19.46 % (2922442)Refutation found. Thanks to Tanya!
% 116.11/19.46 % SZS status Theorem for theBenchmark
% 116.11/19.46 % SZS output start Proof for theBenchmark
% See solution above
% 116.11/19.46 % (2922442)------------------------------
% 116.11/19.46 % (2922442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.11/19.46 % (2922442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.11/19.46 % (2922442)CaDiCaL version: 2.1.3
% 116.11/19.46 % (2922442)Termination reason: Refutation
% 116.11/19.46 % (2922442)Time elapsed: 10.276 s
% 116.11/19.46 % (2922442)Peak memory usage: 132 MB
% 116.11/19.46 % (2922442)Instructions burned: 19489 (million)
% 116.11/19.46 % (2922373)Success in time 19.254 s
% 116.11/19.46 % Vampire exiting
%------------------------------------------------------------------------------