%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : AGT009+1 : 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 : n007.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 226.63s 36.81s
% Output : Refutation 226.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 35
% Syntax : Number of formulae : 159 ( 55 unt; 10 def)
% Number of atoms : 353 ( 15 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 339 ( 145 ~; 145 |; 26 &)
% ( 16 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 11 prp; 0-4 aty)
% Number of functors : 28 ( 28 usr; 25 con; 0-2 aty)
% Number of variables : 141 ( 0 sgn 141 !; 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(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(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/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_4) ).
fof(f5,axiom,
! [X0,X1,X2] :
( any_agent_in_all_proposed_teams(X0,X1,X2)
=> accept_leader(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_5) ).
fof(f6,axiom,
! [X0,X1,X2] :
( the_agent_not_in_any_proposed_teams(X0,X1,X2)
=> ~ ( accept_city(X0,X2)
& accept_leader(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_6) ).
fof(f16,axiom,
! [X0] :
( ( accept_population(X0,atheist,n75)
& accept_population(X0,christian,n24)
& accept_population(X0,muslim,n1)
& accept_population(X0,native,n0)
& accept_population(X0,other,n0) )
<=> accept_city(X0,towna) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_9) ).
fof(f17,axiom,
! [X0] :
( ( accept_population(X0,atheist,n75)
& accept_population(X0,christian,n25)
& accept_population(X0,muslim,n0)
& accept_population(X0,native,n0)
& accept_population(X0,other,n0) )
<=> accept_city(X0,citya) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_10) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_13) ).
fof(f28,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_8) ).
fof(f124,axiom,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_104) ).
fof(f268,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_248) ).
fof(f269,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_249) ).
fof(f270,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn0) ).
fof(f271,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn1) ).
fof(f294,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn24) ).
fof(f295,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn25) ).
fof(f527,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit2) ).
fof(f535,axiom,
rdn_positive_less(rdnn(n0),rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less01) ).
fof(f539,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less45) ).
fof(f546,axiom,
! [X0,X1,X2] :
( ( rdn_positive_less(rdnn(X0),rdnn(X2))
& rdn_non_zero(X1) )
=> rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_multi_digit_low) ).
fof(f548,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(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/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
fof(f553,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_property) ).
fof(f556,conjecture,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_9) ).
fof(f557,negated_conjecture,
~ ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
inference(negated_conjecture,[status(cth)],[f556]) ).
fof(f558,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
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(f568,plain,
! [X0,X1,X2] :
( accept_leader(X0,X1)
| ~ any_agent_in_all_proposed_teams(X0,X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f569,plain,
! [X0,X1,X2] :
( ~ accept_city(X0,X2)
| ~ accept_leader(X0,X1)
| ~ the_agent_not_in_any_proposed_teams(X0,X1,X2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f570,plain,
! [X0,X1,X2] :
( ~ accept_city(X0,X2)
| ~ accept_leader(X0,X1)
| ~ the_agent_not_in_any_proposed_teams(X0,X1,X2) ),
inference(flattening,[],[f569]) ).
fof(f574,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(ennf_transformation,[],[f546]) ).
fof(f575,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(flattening,[],[f574]) ).
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(f587,plain,
! [X2,X3,X0,X1] :
( ~ accept_team(X0,X3,X1,X2)
| accept_city(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f590,plain,
! [X2,X3,X0,X1] :
( ~ less(X2,X1)
| ~ accept_population(X0,X3,X1)
| accept_population(X0,X3,X2) ),
inference(cnf_transformation,[],[f566]) ).
fof(f591,plain,
! [X2,X0,X1] :
( ~ the_agent_in_all_proposed_teams(X0,X1,X2)
| accept_city(X0,X2) ),
inference(cnf_transformation,[],[f567]) ).
fof(f593,plain,
! [X2,X0,X1] :
( ~ any_agent_in_all_proposed_teams(X0,X1,X2)
| accept_leader(X0,X1) ),
inference(cnf_transformation,[],[f568]) ).
fof(f594,plain,
! [X2,X0,X1] :
( ~ the_agent_not_in_any_proposed_teams(X0,X1,X2)
| ~ accept_leader(X0,X1)
| ~ accept_city(X0,X2) ),
inference(cnf_transformation,[],[f570]) ).
fof(f643,plain,
! [X0] :
( ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| accept_city(X0,towna)
| ~ accept_population(X0,atheist,n75) ),
inference(cnf_transformation,[],[f16]) ).
fof(f653,plain,
! [X0] :
( accept_population(X0,christian,n25)
| ~ accept_city(X0,citya) ),
inference(cnf_transformation,[],[f17]) ).
fof(f654,plain,
! [X0] :
( accept_population(X0,atheist,n75)
| ~ accept_city(X0,citya) ),
inference(cnf_transformation,[],[f17]) ).
fof(f662,plain,
! [X0] :
( accept_population(X0,other,n1)
| ~ accept_city(X0,cityb) ),
inference(cnf_transformation,[],[f19]) ).
fof(f664,plain,
! [X0] :
( accept_population(X0,muslim,n1)
| ~ accept_city(X0,cityb) ),
inference(cnf_transformation,[],[f19]) ).
fof(f669,plain,
! [X0] :
( accept_population(X0,native,n0)
| ~ accept_city(X0,townc) ),
inference(cnf_transformation,[],[f20]) ).
fof(f680,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
inference(cnf_transformation,[],[f28]) ).
fof(f776,plain,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(cnf_transformation,[],[f124]) ).
fof(f920,plain,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
inference(cnf_transformation,[],[f268]) ).
fof(f921,plain,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
inference(cnf_transformation,[],[f269]) ).
fof(f922,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(cnf_transformation,[],[f270]) ).
fof(f923,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(cnf_transformation,[],[f271]) ).
fof(f946,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(cnf_transformation,[],[f294]) ).
fof(f947,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(cnf_transformation,[],[f295]) ).
fof(f1179,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(cnf_transformation,[],[f527]) ).
fof(f1187,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(cnf_transformation,[],[f535]) ).
fof(f1191,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f539]) ).
fof(f1198,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(cnf_transformation,[],[f575]) ).
fof(f1200,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(X0))
| rdn_non_zero(rdnn(X0)) ),
inference(cnf_transformation,[],[f577]) ).
fof(f1202,plain,
! [X2,X3,X0,X1] :
( ~ rdn_positive_less(X2,X3)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| less(X0,X1) ),
inference(cnf_transformation,[],[f580]) ).
fof(f1205,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f553]) ).
fof(f1206,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f553]) ).
fof(f1207,plain,
! [X0,X1] :
( less(X1,X0)
| less(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f553]) ).
fof(f1208,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
inference(cnf_transformation,[],[f558]) ).
fof(f1209,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f1205]) ).
fof(f1214,plain,
! [X2,X0,X1] :
( the_agent_in_all_proposed_teams(X0,X1,X2)
| accept_city(X0,X2) ),
inference(consistent_polarity_flipping,[],[f591]) ).
fof(f1215,plain,
! [X2,X0,X1] :
( any_agent_in_all_proposed_teams(X0,X1,X2)
| accept_leader(X0,X1) ),
inference(consistent_polarity_flipping,[],[f593]) ).
fof(f1216,plain,
! [X2,X0,X1] :
( the_agent_not_in_any_proposed_teams(X0,X1,X2)
| ~ accept_leader(X0,X1)
| ~ accept_city(X0,X2) ),
inference(consistent_polarity_flipping,[],[f594]) ).
fof(f1255,plain,
~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(consistent_polarity_flipping,[],[f776]) ).
fof(f1312,plain,
~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
inference(consistent_polarity_flipping,[],[f920]) ).
fof(f1313,plain,
~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
inference(consistent_polarity_flipping,[],[f921]) ).
fof(f1315,plain,
~ rdn_non_zero_digit(rdnn(n2)),
inference(consistent_polarity_flipping,[],[f1179]) ).
fof(f1323,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| rdn_non_zero_digit(rdnn(X0)) ),
inference(consistent_polarity_flipping,[],[f1200]) ).
fof(f1366,plain,
accept_city(muslimcountrybhumanitarianorganization,townc),
inference(resolution,[],[f1214,f1255]) ).
fof(f1395,plain,
accept_leader(muslimcountrybhumanitarianorganization,sufferterragovernment),
inference(resolution,[],[f1215,f1313]) ).
fof(f1577,plain,
accept_city(muslimcountrybhumanitarianorganization,citya),
inference(resolution,[],[f587,f1208]) ).
fof(f1578,plain,
accept_city(muslimcountrybhumanitarianorganization,cityb),
inference(resolution,[],[f587,f680]) ).
fof(f1638,plain,
( ~ accept_leader(muslimcountrybhumanitarianorganization,sufferterragovernment)
| ~ accept_city(muslimcountrybhumanitarianorganization,towna) ),
inference(resolution,[],[f1216,f1312]) ).
fof(f1641,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(forward_subsumption_resolution,[],[f1638,f1395]) ).
fof(f1643,plain,
! [X2,X3,X0,X1] :
( ~ accept_population(X0,X1,X2)
| accept_population(X0,X1,X3)
| less(X2,X3)
| X2 = X3 ),
inference(resolution,[],[f590,f1207]) ).
fof(f1778,plain,
! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdnn(n0)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n1)))
| less(X1,X0) ),
inference(resolution,[],[f1202,f1187]) ).
fof(f1828,plain,
! [X2,X3,X0,X1,X4] :
( ~ rdn_non_zero(X2)
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_translate(X3,rdn_pos(rdn(rdnn(X1),X2)))
| ~ rdn_translate(X4,rdn_pos(rdn(rdnn(X0),X2)))
| less(X4,X3) ),
inference(resolution,[],[f1198,f1202]) ).
fof(f18379,plain,
! [X0] :
( ~ rdn_translate(X0,rdn_pos(rdnn(n1)))
| less(n0,X0) ),
inference(resolution,[],[f1778,f922]) ).
fof(f18417,plain,
! [X0,X1] :
( accept_population(X0,other,X1)
| less(n1,X1)
| n1 = X1
| ~ accept_city(X0,cityb) ),
inference(resolution,[],[f1643,f662]) ).
fof(f18463,plain,
! [X0,X1] :
( ~ accept_city(X0,citya)
| less(n25,X1)
| n25 = X1
| accept_population(X0,christian,X1) ),
inference(resolution,[],[f1643,f653]) ).
fof(f18508,plain,
! [X2,X3,X0,X1,X4] :
( ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_translate(X2,rdn_pos(rdn(rdnn(X1),rdnn(X3))))
| ~ rdn_translate(X4,rdn_pos(rdn(rdnn(X0),rdnn(X3))))
| less(X4,X2)
| rdn_non_zero_digit(rdnn(X3)) ),
inference(resolution,[],[f1828,f1323]) ).
fof(f51190,plain,
less(n0,n1),
inference(resolution,[],[f18379,f923]) ).
fof(f51520,definition,
( spl0_45
<=> accept_population(muslimcountrybhumanitarianorganization,native,n0) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f51522,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| spl0_45 ),
inference(avatar_component_clause,[],[f51520]) ).
fof(f51827,definition,
( spl0_102
<=> n1 = n0 ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f51829,plain,
( n1 = n0
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f51827]) ).
fof(f51831,definition,
( spl0_103
<=> less(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f51833,plain,
( less(n0,n1)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f51831]) ).
fof(f51947,definition,
( spl0_126
<=> n24 = n25 ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f51949,plain,
( n24 = n25
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f51947]) ).
fof(f51951,definition,
( spl0_127
<=> less(n24,n25) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f51953,plain,
( less(n24,n25)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f51951]) ).
fof(f51955,plain,
! [X0] :
( accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| n25 = X0
| less(n25,X0) ),
inference(resolution,[],[f18463,f1577]) ).
fof(f52977,plain,
! [X2,X0,X1] :
( ~ rdn_translate(X2,rdn_pos(rdn(rdnn(n4),rdnn(X1))))
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(n5),rdnn(X1))))
| less(X2,X0)
| rdn_non_zero_digit(rdnn(X1)) ),
inference(resolution,[],[f18508,f1191]) ).
fof(f53047,definition,
( spl0_184
<=> accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f53049,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| spl0_184 ),
inference(avatar_component_clause,[],[f53047]) ).
fof(f53060,definition,
( spl0_187
<=> accept_population(muslimcountrybhumanitarianorganization,muslim,n1) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f53062,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| spl0_187 ),
inference(avatar_component_clause,[],[f53060]) ).
fof(f53134,plain,
( n24 = n25
| less(n25,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(resolution,[],[f51955,f643]) ).
fof(f53137,plain,
( n24 = n25
| less(n25,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(forward_subsumption_resolution,[],[f53134,f1641]) ).
fof(f53139,definition,
( spl0_201
<=> accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f53141,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| spl0_201 ),
inference(avatar_component_clause,[],[f53139]) ).
fof(f53143,definition,
( spl0_202
<=> less(n25,n24) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f53145,plain,
( less(n25,n24)
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f53143]) ).
fof(f53146,plain,
( ~ spl0_201
| ~ spl0_187
| ~ spl0_45
| ~ spl0_184
| spl0_202
| spl0_126 ),
inference(avatar_split_clause,[],[f53137,f51947,f53143,f53047,f51520,f53060,f53139]) ).
fof(f53205,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| spl0_45 ),
inference(resolution,[],[f51522,f669]) ).
fof(f53220,plain,
( $false
| spl0_45 ),
inference(forward_subsumption_resolution,[],[f53205,f1366]) ).
fof(f53221,plain,
spl0_45,
inference(avatar_contradiction_clause,[],[f53220]) ).
fof(f53274,plain,
( less(n1,n0)
| n1 = n0
| ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| spl0_184 ),
inference(resolution,[],[f53049,f18417]) ).
fof(f53275,plain,
( less(n1,n0)
| n1 = n0
| spl0_184 ),
inference(forward_subsumption_resolution,[],[f53274,f1578]) ).
fof(f53283,definition,
( spl0_204
<=> less(n1,n0) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f53286,plain,
( spl0_102
| spl0_204
| spl0_184 ),
inference(avatar_split_clause,[],[f53275,f53047,f53283,f51827]) ).
fof(f53313,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| spl0_187 ),
inference(resolution,[],[f53062,f664]) ).
fof(f53325,plain,
( $false
| spl0_187 ),
inference(forward_subsumption_resolution,[],[f53313,f1578]) ).
fof(f53326,plain,
spl0_187,
inference(avatar_contradiction_clause,[],[f53325]) ).
fof(f53340,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| spl0_201 ),
inference(resolution,[],[f53141,f654]) ).
fof(f53349,plain,
( $false
| spl0_201 ),
inference(forward_subsumption_resolution,[],[f53340,f1577]) ).
fof(f53350,plain,
spl0_201,
inference(avatar_contradiction_clause,[],[f53349]) ).
fof(f74577,plain,
( ~ less(n1,n0)
| ~ spl0_103 ),
inference(resolution,[],[f51833,f1206]) ).
fof(f74578,plain,
( ~ spl0_204
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f74577,f51831,f53283]) ).
fof(f374615,plain,
spl0_103,
inference(avatar_split_clause,[],[f51190,f51831]) ).
fof(f430822,plain,
( less(n1,n1)
| ~ spl0_102
| ~ spl0_103 ),
inference(superposition,[],[f51833,f51829]) ).
fof(f430948,plain,
( $false
| ~ spl0_102
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f430822,f1209]) ).
fof(f430949,plain,
( ~ spl0_102
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f430948]) ).
fof(f1051613,plain,
( ~ less(n24,n25)
| ~ spl0_202 ),
inference(resolution,[],[f53145,f1206]) ).
fof(f1051614,plain,
( ~ spl0_127
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f1051613,f53143,f51951]) ).
fof(f1076861,plain,
! [X0] :
( ~ rdn_translate(X0,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| less(n24,X0)
| rdn_non_zero_digit(rdnn(n2)) ),
inference(resolution,[],[f52977,f946]) ).
fof(f1076866,plain,
! [X0] :
( ~ rdn_translate(X0,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| less(n24,X0) ),
inference(forward_subsumption_resolution,[],[f1076861,f1315]) ).
fof(f1363338,plain,
less(n24,n25),
inference(resolution,[],[f1076866,f947]) ).
fof(f1363361,plain,
spl0_127,
inference(avatar_split_clause,[],[f1363338,f51951]) ).
fof(f1364288,plain,
( less(n24,n24)
| ~ spl0_126
| ~ spl0_127 ),
inference(forward_demodulation,[],[f51953,f51949]) ).
fof(f1364289,plain,
( $false
| ~ spl0_126
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f1364288,f1209]) ).
fof(f1364290,plain,
( ~ spl0_126
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f1364289]) ).
cnf(s91,plain,
( ~ spl0_45
| spl0_126
| ~ spl0_184
| ~ spl0_187
| ~ spl0_201
| spl0_202 ),
inference(sat_conversion,[],[f53146]) ).
cnf(s95,plain,
spl0_45,
inference(sat_conversion,[],[f53221]) ).
cnf(s100,plain,
( spl0_102
| spl0_184
| spl0_204 ),
inference(sat_conversion,[],[f53286]) ).
cnf(s104,plain,
spl0_187,
inference(sat_conversion,[],[f53326]) ).
cnf(s108,plain,
spl0_201,
inference(sat_conversion,[],[f53350]) ).
cnf(s428,plain,
( ~ spl0_103
| ~ spl0_204 ),
inference(sat_conversion,[],[f74578]) ).
cnf(s26003,plain,
spl0_103,
inference(sat_conversion,[],[f374615]) ).
cnf(s41265,plain,
( ~ spl0_102
| ~ spl0_103 ),
inference(sat_conversion,[],[f430949]) ).
cnf(s165951,plain,
( ~ spl0_127
| ~ spl0_202 ),
inference(sat_conversion,[],[f1051614]) ).
cnf(s240788,plain,
spl0_127,
inference(sat_conversion,[],[f1363361]) ).
cnf(s241248,plain,
( ~ spl0_126
| ~ spl0_127 ),
inference(sat_conversion,[],[f1364290]) ).
cnf(s241249,plain,
~ spl0_126,
inference(rat,[],[s241248,s240788]) ).
cnf(s244314,plain,
~ spl0_202,
inference(rat,[],[s165951,s240788]) ).
cnf(s256411,plain,
~ spl0_102,
inference(rat,[],[s41265,s26003]) ).
cnf(s260037,plain,
~ spl0_204,
inference(rat,[],[s428,s26003]) ).
cnf(s260137,plain,
spl0_184,
inference(rat,[],[s100,s260037,s256411]) ).
cnf(s260141,plain,
$false,
inference(rat,[],[s91,s244314,s108,s104,s260137,s241249,s95]) ).
fof(f1364291,plain,
$false,
inference(avatar_sat_refutation,[],[s260141]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : AGT009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n007.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 19:06:56 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 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
% 25.46/3.84 % (2720671)Will run a generic schedule for satisfiability detection.
% 25.46/3.84 % (2720678)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1220431677:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 25.46/3.84 % (2720676)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3719137765_2999 on theBenchmark for (2999ds/0Mi)
% 25.46/3.84 % (2720679)dis+10_1_sil=32000:sp=arity:random_seed=1293764458:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 25.46/3.84 % (2720680)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=128239269:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 25.46/3.84 % (2720681)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1553457257:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 25.46/3.84 % (2720682)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1622088126:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 25.46/3.84 % (2720677)% WARNING: option uhcvi not known.
% 25.46/3.84 % (2720677)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4097162519:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 25.46/3.84 % TRYING [1]
% 25.46/3.84 % TRYING [2]
% 25.46/3.84 % (2720679)Instruction limit reached!
% 25.46/3.84 % (2720679)------------------------------
% 25.46/3.84 % (2720679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.46/3.84 % (2720679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/3.84 % (2720679)CaDiCaL version: 2.1.3
% 25.46/3.84 % (2720679)Termination reason: Instruction limit
% 25.46/3.84 % (2720679)Termination phase: Saturation
% 25.46/3.84 % (2720679)Time elapsed: 0.050 s
% 25.46/3.84 % (2720679)Peak memory usage: 13 MB
% 25.46/3.84 % (2720679)Instructions burned: 104 (million)
% 25.46/3.84 % TRYING [3]
% 25.46/3.84 % (2720680)Instruction limit reached!
% 25.46/3.84 % (2720680)------------------------------
% 25.46/3.84 % (2720680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.46/3.84 % (2720680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/3.84 % (2720680)CaDiCaL version: 2.1.3
% 25.46/3.84 % (2720680)Termination reason: Instruction limit
% 25.46/3.84 % (2720680)Termination phase: Saturation
% 25.46/3.84 % (2720680)Time elapsed: 0.059 s
% 25.46/3.84 % (2720680)Peak memory usage: 14 MB
% 25.46/3.84 % (2720680)Instructions burned: 116 (million)
% 25.46/3.84 % (2720681)Instruction limit reached!
% 25.46/3.84 % (2720681)------------------------------
% 25.46/3.84 % (2720681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.46/3.84 % (2720681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/3.84 % (2720681)CaDiCaL version: 2.1.3
% 25.46/3.84 % (2720681)Termination reason: Instruction limit
% 25.46/3.84 % (2720681)Termination phase: Saturation
% 25.46/3.84 % (2720681)Time elapsed: 0.064 s
% 25.46/3.84 % (2720681)Peak memory usage: 15 MB
% 25.46/3.84 % (2720681)Instructions burned: 132 (million)
% 25.46/3.84 % (2720690)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=950086196:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 25.46/3.84 % (2720691)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3184096273:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 25.46/3.84 % (2720682)Instruction limit reached!
% 25.46/3.84 % (2720682)------------------------------
% 25.46/3.84 % (2720682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.46/3.84 % (2720682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.46/3.84 % (2720682)CaDiCaL version: 2.1.3
% 25.46/3.84 % (2720682)Termination reason: Instruction limit
% 25.46/3.84 % (2720682)Termination phase: Saturation
% 25.46/3.84 % (2720682)Time elapsed: 0.082 s
% 25.46/3.84 % (2720682)Peak memory usage: 15 MB
% 25.46/3.84 % (2720682)Instructions burned: 160 (million)
% 25.46/3.84 % (2720692)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=2076403745:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 25.46/3.84 % (2720696)ott-21_1_sil=16000:fs=off:random_seed=23835402:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 25.46/3.84 % TRYING [1]
% 25.46/3.84 % TRYING [2]
% 25.46/3.84 % TRYING [4]
% 25.46/3.84 % TRYING [3]
% 25.46/3.84 % (2720691)Instruction limit reached!
% 25.46/3.84 % (2720691)------------------------------
% 25.46/3.84 % (2720691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.46/3.84 % (2720691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.89/6.48 % (2720691)CaDiCaL version: 2.1.3
% 43.89/6.48 % (2720691)Termination reason: Instruction limit
% 43.89/6.48 % (2720691)Termination phase: Saturation
% 43.89/6.48 % (2720691)Time elapsed: 0.067 s
% 43.89/6.48 % (2720691)Peak memory usage: 14 MB
% 43.89/6.48 % (2720691)Instructions burned: 131 (million)
% 43.89/6.48 % (2720698)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2999157350:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 43.89/6.48 % (2720696)Instruction limit reached!
% 43.89/6.48 % (2720696)------------------------------
% 43.89/6.48 % (2720696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.89/6.48 % (2720696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.89/6.48 % (2720696)CaDiCaL version: 2.1.3
% 43.89/6.48 % (2720696)Termination reason: Instruction limit
% 43.89/6.48 % (2720696)Termination phase: Saturation
% 43.89/6.48 % (2720696)Time elapsed: 0.084 s
% 43.89/6.48 % (2720696)Peak memory usage: 13 MB
% 43.89/6.48 % (2720696)Instructions burned: 180 (million)
% 43.89/6.48 % (2720700)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3581405188:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 43.89/6.49 % TRYING [1]
% 43.89/6.49 % TRYING [4]
% 43.89/6.49 % TRYING [2]
% 43.89/6.49 % TRYING [3]
% 43.89/6.49 % TRYING [5]
% 43.89/6.49 % (2720690)Instruction limit reached!
% 43.89/6.49 % (2720690)------------------------------
% 43.89/6.49 % (2720690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.89/6.49 % (2720690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.89/6.49 % (2720690)CaDiCaL version: 2.1.3
% 43.89/6.49 % (2720690)Termination reason: Instruction limit
% 43.89/6.49 % (2720690)Termination phase: Finite model building SAT solving
% 43.89/6.49 % (2720690)Time elapsed: 0.318 s
% 43.89/6.49 % (2720690)Peak memory usage: 30 MB
% 43.89/6.49 % (2720690)Instructions burned: 714 (million)
% 43.89/6.49 % (2720698)Instruction limit reached!
% 43.89/6.49 % (2720698)------------------------------
% 43.89/6.49 % (2720698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.89/6.49 % (2720698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.89/6.49 % (2720698)CaDiCaL version: 2.1.3
% 43.89/6.49 % (2720698)Termination reason: Instruction limit
% 43.89/6.49 % (2720698)Termination phase: Saturation
% 43.89/6.49 % (2720698)Time elapsed: 0.244 s
% 43.89/6.49 % (2720698)Peak memory usage: 17 MB
% 43.89/6.49 % (2720698)Instructions burned: 478 (million)
% 43.89/6.49 % (2720702)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1025425110:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 43.89/6.49 % (2720704)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=736011920:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 43.89/6.49 % (2720692)Instruction limit reached!
% 43.89/6.49 % (2720692)------------------------------
% 43.89/6.49 % (2720692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.89/6.49 % (2720692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.89/6.49 % (2720692)CaDiCaL version: 2.1.3
% 43.89/6.49 % (2720692)Termination reason: Instruction limit
% 43.89/6.49 % (2720692)Termination phase: Saturation
% 43.89/6.49 % (2720692)Time elapsed: 0.357 s
% 43.89/6.49 % (2720692)Peak memory usage: 23 MB
% 43.89/6.49 % (2720692)Instructions burned: 684 (million)
% 43.89/6.49 % (2720706)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=70585797: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)
% 43.89/6.49 % TRYING [4]
% 43.89/6.49 % TRYING [14]
% 43.89/6.49 % (2720700)Instruction limit reached!
% 43.89/6.49 % (2720700)------------------------------
% 43.89/6.49 % (2720700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.89/6.49 % (2720700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.89/6.49 % (2720700)CaDiCaL version: 2.1.3
% 43.89/6.49 % (2720700)Termination reason: Instruction limit
% 43.89/6.49 % (2720700)Termination phase: Finite model building constraint generation
% 43.89/6.49 % (2720700)Time elapsed: 0.312 s
% 43.89/6.49 % (2720700)Peak memory usage: 21 MB
% 43.89/6.49 % (2720700)Instructions burned: 869 (million)
% 43.89/6.49 % (2720708)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1686755123:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 43.89/6.49 % TRYING [6]
% 43.89/6.49 % (2720704)Instruction limit reached!
% 43.89/6.49 % (2720704)------------------------------
% 93.57/13.45 % (2720704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.57/13.45 % (2720704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.57/13.45 % (2720704)CaDiCaL version: 2.1.3
% 93.57/13.45 % (2720704)Termination reason: Instruction limit
% 93.57/13.45 % (2720704)Termination phase: Finite model building constraint generation
% 93.57/13.45 % (2720704)Time elapsed: 0.327 s
% 93.57/13.45 % (2720704)Peak memory usage: 73 MB
% 93.57/13.45 % (2720704)Instructions burned: 889 (million)
% 93.57/13.45 % (2720710)fmb+10_1_sil=64000:random_seed=557498247:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 93.57/13.45 % TRYING [1]
% 93.57/13.45 % TRYING [2]
% 93.57/13.45 % (2720706)Instruction limit reached!
% 93.57/13.45 % (2720706)------------------------------
% 93.57/13.45 % (2720706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.57/13.45 % (2720706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.57/13.45 % (2720706)CaDiCaL version: 2.1.3
% 93.57/13.45 % (2720706)Termination reason: Instruction limit
% 93.57/13.45 % (2720706)Termination phase: Saturation
% 93.57/13.45 % (2720706)Time elapsed: 0.371 s
% 93.57/13.45 % (2720706)Peak memory usage: 21 MB
% 93.57/13.45 % (2720706)Instructions burned: 693 (million)
% 93.57/13.45 % (2720718)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3688243857:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 93.57/13.45 % TRYING [3]
% 93.57/13.45 % TRYING [20]
% 93.57/13.45 % (2720708)Instruction limit reached!
% 93.57/13.45 % (2720708)------------------------------
% 93.57/13.45 % (2720708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.57/13.45 % (2720708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.57/13.45 % (2720708)CaDiCaL version: 2.1.3
% 93.57/13.45 % (2720708)Termination reason: Instruction limit
% 93.57/13.45 % (2720708)Termination phase: Saturation
% 93.57/13.45 % (2720708)Time elapsed: 0.364 s
% 93.57/13.45 % (2720708)Peak memory usage: 21 MB
% 93.57/13.45 % (2720708)Instructions burned: 880 (million)
% 93.57/13.45 % (2720720)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3695793478:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 93.57/13.45 % TRYING [8]
% 93.57/13.45 % (2720702)Instruction limit reached!
% 93.57/13.45 % (2720702)------------------------------
% 93.57/13.45 % (2720702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.57/13.45 % (2720702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.57/13.45 % (2720702)CaDiCaL version: 2.1.3
% 93.57/13.45 % (2720702)Termination reason: Instruction limit
% 93.57/13.45 % (2720702)Termination phase: Saturation
% 93.57/13.45 % (2720702)Time elapsed: 0.631 s
% 93.57/13.45 % (2720702)Peak memory usage: 35 MB
% 93.57/13.45 % (2720702)Instructions burned: 1179 (million)
% 93.57/13.45 % (2720722)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2303327878:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 93.57/13.45 % TRYING [4]
% 93.57/13.45 % (2720720)Instruction limit reached!
% 93.57/13.45 % (2720720)------------------------------
% 93.57/13.45 % (2720720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.57/13.45 % (2720720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.57/13.45 % (2720720)CaDiCaL version: 2.1.3
% 93.57/13.45 % (2720720)Termination reason: Instruction limit
% 93.57/13.45 % (2720720)Termination phase: Finite model building constraint generation
% 93.57/13.45 % (2720720)Time elapsed: 0.333 s
% 93.57/13.45 % (2720720)Peak memory usage: 68 MB
% 93.57/13.45 % (2720720)Instructions burned: 920 (million)
% 93.57/13.45 % (2720724)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=995182653:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 93.57/13.45 % TRYING [5]
% 93.57/13.45 % TRYING [7]
% 93.57/13.45 % (2720724)Instruction limit reached!
% 93.57/13.45 % (2720724)------------------------------
% 93.57/13.45 % (2720724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.57/13.45 % (2720724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.57/13.45 % (2720724)CaDiCaL version: 2.1.3
% 93.57/13.45 % (2720724)Termination reason: Instruction limit
% 93.57/13.45 % (2720724)Termination phase: Saturation
% 93.57/13.45 % (2720724)Time elapsed: 0.784 s
% 93.57/13.45 % (2720724)Peak memory usage: 30 MB
% 93.57/13.45 % (2720724)Instructions burned: 1473 (million)
% 93.57/13.45 % (2720726)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=25762041:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 93.57/13.45 % TRYING [77]
% 93.57/13.45 % TRYING [6]
% 93.57/13.45 % TRYING [8]
% 93.57/13.45 % (2720722)Instruction limit reached!
% 233.65/33.17 % (2720722)------------------------------
% 233.65/33.17 % (2720722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.65/33.17 % (2720722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.65/33.17 % (2720722)CaDiCaL version: 2.1.3
% 233.65/33.17 % (2720722)Termination reason: Instruction limit
% 233.65/33.17 % (2720722)Termination phase: Saturation
% 233.65/33.17 % (2720722)Time elapsed: 2.524 s
% 233.65/33.17 % (2720722)Peak memory usage: 55 MB
% 233.65/33.17 % (2720722)Instructions burned: 5132 (million)
% 233.65/33.17 % (2720728)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2235818923:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 233.65/33.17 % TRYING [16]
% 233.65/33.17 % TRYING [7]
% 233.65/33.17 % (2720718)Instruction limit reached!
% 233.65/33.17 % (2720718)------------------------------
% 233.65/33.17 % (2720718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.65/33.17 % (2720718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.65/33.17 % (2720718)CaDiCaL version: 2.1.3
% 233.65/33.17 % (2720718)Termination reason: Instruction limit
% 233.65/33.17 % (2720718)Termination phase: Finite model building constraint generation
% 233.65/33.17 % (2720718)Time elapsed: 3.466 s
% 233.65/33.17 % (2720718)Peak memory usage: 554 MB
% 233.65/33.17 % (2720718)Instructions burned: 9517 (million)
% 233.65/33.17 % (2720730)ott-2_1_sil=16000:newcnf=on:random_seed=190514285:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 233.65/33.17 % (2720728)Instruction limit reached!
% 233.65/33.17 % (2720728)------------------------------
% 233.65/33.17 % (2720728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.65/33.17 % (2720728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.65/33.17 % (2720728)CaDiCaL version: 2.1.3
% 233.65/33.17 % (2720728)Termination reason: Instruction limit
% 233.65/33.17 % (2720728)Termination phase: Finite model building constraint generation
% 233.65/33.17 % (2720728)Time elapsed: 0.796 s
% 233.65/33.17 % (2720728)Peak memory usage: 153 MB
% 233.65/33.17 % (2720728)Instructions burned: 2176 (million)
% 233.65/33.17 % (2720732)ott+10_1_sil=32000:tgt=ground:random_seed=2259380846:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 233.65/33.17 % (2720726)Instruction limit reached!
% 233.65/33.17 % (2720726)------------------------------
% 233.65/33.17 % (2720726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.65/33.17 % (2720726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.65/33.17 % (2720726)CaDiCaL version: 2.1.3
% 233.65/33.17 % (2720726)Termination reason: Instruction limit
% 233.65/33.17 % (2720726)Termination phase: Finite model building constraint generation
% 233.65/33.17 % (2720726)Time elapsed: 2.370 s
% 233.65/33.17 % (2720726)Peak memory usage: 525 MB
% 233.65/33.17 % (2720726)Instructions burned: 6326 (million)
% 233.65/33.17 % (2720734)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1729805976:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 233.65/33.17 % TRYING [1]
% 233.65/33.17 % TRYING [2]
% 233.65/33.17 % TRYING [3]
% 233.65/33.17 % TRYING [4]
% 233.65/33.17 % TRYING [9]
% 233.65/33.17 % (2720730)Instruction limit reached!
% 233.65/33.17 % (2720730)------------------------------
% 233.65/33.17 % (2720730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.65/33.17 % (2720730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.65/33.17 % (2720730)CaDiCaL version: 2.1.3
% 233.65/33.17 % (2720730)Termination reason: Instruction limit
% 233.65/33.17 % (2720730)Termination phase: Saturation
% 233.65/33.17 % (2720730)Time elapsed: 0.425 s
% 233.65/33.17 % (2720730)Peak memory usage: 26 MB
% 233.65/33.17 % (2720730)Instructions burned: 871 (million)
% 233.65/33.17 % (2720736)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3934843467:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 233.65/33.17 % TRYING [5]
% 233.65/33.17 % TRYING [6]
% 233.65/33.17 % TRYING [8]
% 233.65/33.17 % TRYING [7]
% 233.65/33.17 % (2720736)Instruction limit reached!
% 233.65/33.17 % (2720736)------------------------------
% 233.65/33.17 % (2720736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.65/33.17 % (2720736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.65/33.17 % (2720736)CaDiCaL version: 2.1.3
% 233.65/33.17 % (2720736)Termination reason: Instruction limit
% 233.65/33.17 % (2720736)Termination phase: Saturation
% 233.65/33.17 % (2720736)Time elapsed: 1.355 s
% 233.65/33.17 % (2720736)Peak memory usage: 41 MB
% 233.65/33.17 % (2720736)Instructions burned: 3514 (million)
% 233.65/33.17 % (2720738)dis+21_1_sil=32000:sas=cadical:random_seed=2096441435:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 226.63/36.81 % (2720732)Instruction limit reached!
% 226.63/36.81 % (2720732)------------------------------
% 226.63/36.81 % (2720732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720732)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720732)Termination reason: Instruction limit
% 226.63/36.81 % (2720732)Termination phase: Saturation
% 226.63/36.81 % (2720732)Time elapsed: 2.305 s
% 226.63/36.81 % (2720732)Peak memory usage: 74 MB
% 226.63/36.81 % (2720732)Instructions burned: 5118 (million)
% 226.63/36.81 % (2720740)ott+11_1_sil=16000:gs=on:random_seed=884275381:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 226.63/36.81 % TRYING [10]
% 226.63/36.81 % TRYING [8]
% 226.63/36.81 % (2720740)Instruction limit reached!
% 226.63/36.81 % (2720740)------------------------------
% 226.63/36.81 % (2720740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720740)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720740)Termination reason: Instruction limit
% 226.63/36.81 % (2720740)Termination phase: Saturation
% 226.63/36.81 % (2720740)Time elapsed: 1.287 s
% 226.63/36.81 % (2720740)Peak memory usage: 51 MB
% 226.63/36.81 % (2720740)Instructions burned: 2251 (million)
% 226.63/36.81 % (2720738)Instruction limit reached!
% 226.63/36.81 % (2720738)------------------------------
% 226.63/36.81 % (2720738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720738)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720738)Termination reason: Instruction limit
% 226.63/36.81 % (2720738)Termination phase: Saturation
% 226.63/36.81 % (2720738)Time elapsed: 1.855 s
% 226.63/36.81 % (2720738)Peak memory usage: 75 MB
% 226.63/36.81 % (2720738)Instructions burned: 3774 (million)
% 226.63/36.81 % (2720742)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1539753345:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi)
% 226.63/36.81 % (2720744)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2028534664:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2918 on theBenchmark for (2918ds/4591Mi)
% 226.63/36.81 % TRYING [7]
% 226.63/36.81 % (2720710)Instruction limit reached!
% 226.63/36.81 % (2720710)------------------------------
% 226.63/36.81 % (2720710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720710)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720710)Termination reason: Instruction limit
% 226.63/36.81 % (2720710)Termination phase: Finite model building SAT solving
% 226.63/36.81 % (2720710)Time elapsed: 7.847 s
% 226.63/36.81 % (2720710)Peak memory usage: 125 MB
% 226.63/36.81 % (2720710)Instructions burned: 22063 (million)
% 226.63/36.81 % (2720746)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2969932425:i=29340_2913 on theBenchmark for (2913ds/29340Mi)
% 226.63/36.81 % TRYING [9]
% 226.63/36.81 % (2720744)Instruction limit reached!
% 226.63/36.81 % (2720744)------------------------------
% 226.63/36.81 % (2720744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720744)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720744)Termination reason: Instruction limit
% 226.63/36.81 % (2720744)Termination phase: Saturation
% 226.63/36.81 % (2720744)Time elapsed: 2.701 s
% 226.63/36.81 % (2720744)Peak memory usage: 74 MB
% 226.63/36.81 % (2720744)Instructions burned: 4593 (million)
% 226.63/36.81 % (2720748)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1563650280:i=5211_2891 on theBenchmark for (2891ds/5211Mi)
% 226.63/36.81 % TRYING [10]
% 226.63/36.81 % (2720748)Instruction limit reached!
% 226.63/36.81 % (2720748)------------------------------
% 226.63/36.81 % (2720748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720748)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720748)Termination reason: Instruction limit
% 226.63/36.81 % (2720748)Termination phase: Saturation
% 226.63/36.81 % (2720748)Time elapsed: 2.315 s
% 226.63/36.81 % (2720748)Peak memory usage: 69 MB
% 226.63/36.81 % (2720748)Instructions burned: 5211 (million)
% 226.63/36.81 % (2720750)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1119461975:i=5497:nm=2_2867 on theBenchmark for (2867ds/5497Mi)
% 226.63/36.81 % TRYING [17]
% 226.63/36.81 % (2720750)Instruction limit reached!
% 226.63/36.81 % (2720750)------------------------------
% 226.63/36.81 % (2720750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720750)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720750)Termination reason: Instruction limit
% 226.63/36.81 % (2720750)Termination phase: Finite model building constraint generation
% 226.63/36.81 % (2720750)Time elapsed: 1.958 s
% 226.63/36.81 % (2720750)Peak memory usage: 342 MB
% 226.63/36.81 % (2720750)Instructions burned: 5498 (million)
% 226.63/36.81 % (2720752)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3991441523:fmbsr=2:i=46332_2847 on theBenchmark for (2847ds/46332Mi)
% 226.63/36.81 % TRYING [15]
% 226.63/36.81 % TRYING [11]
% 226.63/36.81 % TRYING [11]
% 226.63/36.81 % (2720746)Instruction limit reached!
% 226.63/36.81 % (2720746)------------------------------
% 226.63/36.81 % (2720746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720746)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720746)Termination reason: Instruction limit
% 226.63/36.81 % (2720746)Termination phase: Saturation
% 226.63/36.81 % (2720746)Time elapsed: 15.309 s
% 226.63/36.81 % (2720746)Peak memory usage: 212 MB
% 226.63/36.81 % (2720746)Instructions burned: 29340 (million)
% 226.63/36.81 % (2720754)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4105653418:i=14071_2759 on theBenchmark for (2759ds/14071Mi)
% 226.63/36.81 % TRYING [12]
% 226.63/36.81 % TRYING [12]
% 226.63/36.81 % (2720734)Instruction limit reached!
% 226.63/36.81 % (2720734)------------------------------
% 226.63/36.81 % (2720734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720734)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720734)Termination reason: Instruction limit
% 226.63/36.81 % (2720734)Termination phase: Finite model building SAT solving
% 226.63/36.81 % (2720734)Time elapsed: 23.723 s
% 226.63/36.81 % (2720734)Peak memory usage: 391 MB
% 226.63/36.81 % (2720734)Instructions burned: 54283 (million)
% 226.63/36.81 % (2720756)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=651651493:i=22565:add=on:rawr=on_2716 on theBenchmark for (2716ds/22565Mi)
% 226.63/36.81 % (2720754)Instruction limit reached!
% 226.63/36.81 % (2720754)------------------------------
% 226.63/36.81 % (2720754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720754)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720754)Termination reason: Instruction limit
% 226.63/36.81 % (2720754)Termination phase: Finite model building SAT solving
% 226.63/36.81 % (2720754)Time elapsed: 5.883 s
% 226.63/36.81 % (2720754)Peak memory usage: 467 MB
% 226.63/36.81 % (2720754)Instructions burned: 14072 (million)
% 226.63/36.81 % (2720758)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2088251580:i=8173:av=off_2699 on theBenchmark for (2699ds/8173Mi)
% 226.63/36.81 % (2720678)Instruction limit reached!
% 226.63/36.81 % (2720678)------------------------------
% 226.63/36.81 % (2720678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720678)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720678)Termination reason: Instruction limit
% 226.63/36.81 % (2720678)Termination phase: Saturation
% 226.63/36.81 % (2720678)Time elapsed: 30.349 s
% 226.63/36.81 % (2720678)Peak memory usage: 2238 MB
% 226.63/36.81 % (2720678)Instructions burned: 88024 (million)
% 226.63/36.81 % (2720760)dis+10_16:1_sil=16000:random_seed=3000878995:i=9155:fsr=off_2694 on theBenchmark for (2694ds/9155Mi)
% 226.63/36.81 % (2720760)Instruction limit reached!
% 226.63/36.81 % (2720760)------------------------------
% 226.63/36.81 % (2720760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720760)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720760)Termination reason: Instruction limit
% 226.63/36.81 % (2720760)Termination phase: Saturation
% 226.63/36.81 % (2720760)Time elapsed: 2.400 s
% 226.63/36.81 % (2720760)Peak memory usage: 198 MB
% 226.63/36.81 % (2720760)Instructions burned: 9155 (million)
% 226.63/36.81 % (2720762)ott-3_8_sil=64000:random_seed=4052470535:i=20139:bs=on_2670 on theBenchmark for (2670ds/20139Mi)
% 226.63/36.81 % (2720758)Instruction limit reached!
% 226.63/36.81 % (2720758)------------------------------
% 226.63/36.81 % (2720758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.81 % (2720758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.81 % (2720758)CaDiCaL version: 2.1.3
% 226.63/36.81 % (2720758)Termination reason: Instruction limit
% 226.63/36.81 % (2720758)Termination phase: Saturation
% 226.63/36.81 % (2720758)Time elapsed: 4.398 s
% 226.63/36.81 % (2720758)Peak memory usage: 117 MB
% 226.63/36.81 % (2720758)Instructions burned: 8173 (million)
% 226.63/36.81 % (2720764)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=957802425:fmbsr=2:i=32576_2655 on theBenchmark for (2655ds/32576Mi)
% 226.63/36.81 % TRYING [9]
% 226.63/36.81 % (2720677) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2720671-2720677"...
% 226.63/36.81 % (2720677)...printing done.
% 226.63/36.81 % (2720677)Refutation found. Thanks to Tanya!
% 226.63/36.81 % SZS status Theorem for theBenchmark
% 226.63/36.81 % SZS output start Proof for theBenchmark
% See solution above
% 226.63/36.82 % (2720677)------------------------------
% 226.63/36.82 % (2720677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.63/36.82 % (2720677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.63/36.82 % (2720677)CaDiCaL version: 2.1.3
% 226.63/36.82 % (2720677)Termination reason: Refutation
% 226.63/36.82 % (2720677)Time elapsed: 36.196 s
% 226.63/36.82 % (2720677)Peak memory usage: 449 MB
% 226.63/36.82 % (2720677)Instructions burned: 63572 (million)
% 226.63/36.82 % (2720671)Success in time 36.606 s
% 226.63/36.82 % Vampire exiting
%------------------------------------------------------------------------------