%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : AGT013+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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:46 AM UTC 2026
% Result : Theorem 23.06s 3.59s
% Output : Refutation 23.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 36
% Syntax : Number of formulae : 187 ( 53 unt; 12 def)
% Number of atoms : 430 ( 16 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 475 ( 232 ~; 214 |; 10 &)
% ( 14 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 13 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 20 con; 0-2 aty)
% Number of variables : 108 ( 0 sgn 108 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( accept_population(X0,X3,X1)
& less(X2,X1) )
=> accept_population(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_3) ).
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(f362,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_93) ).
fof(f472,axiom,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_203) ).
fof(f473,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_204) ).
fof(f475,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n78),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_206) ).
fof(f635,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_366) ).
fof(f661,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn24) ).
fof(f662,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn25) ).
fof(f712,axiom,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn75) ).
fof(f713,axiom,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn76) ).
fof(f715,axiom,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn78) ).
fof(f894,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit2) ).
fof(f899,axiom,
rdn_non_zero_digit(rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit7) ).
fof(f906,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less45) ).
fof(f907,axiom,
rdn_positive_less(rdnn(n5),rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less56) ).
fof(f908,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less67) ).
fof(f909,axiom,
rdn_positive_less(rdnn(n7),rdnn(n8)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less78) ).
fof(f911,axiom,
! [X0,X1,X2] :
( ( rdn_positive_less(rdnn(X0),rdnn(X1))
& rdn_positive_less(rdnn(X1),rdnn(X2)) )
=> rdn_positive_less(rdnn(X0),rdnn(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_transitivity) ).
fof(f913,axiom,
! [X0,X1,X2] :
( ( rdn_positive_less(rdnn(X0),rdnn(X2))
& rdn_non_zero(X1) )
=> rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_multi_digit_low) ).
fof(f915,axiom,
! [X0] :
( rdn_non_zero_digit(rdnn(X0))
=> rdn_non_zero(rdnn(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_digit) ).
fof(f917,axiom,
! [X0,X1,X2,X3] :
( ( rdn_translate(X0,rdn_pos(X2))
& rdn_translate(X1,rdn_pos(X3))
& rdn_positive_less(X2,X3) )
=> less(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
fof(f920,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_property) ).
fof(f923,conjecture,
~ accept_population(muslimcountrybhumanitarianorganization,christian,n25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_13) ).
fof(f924,negated_conjecture,
~ ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25),
inference(negated_conjecture,[status(cth)],[f923]) ).
fof(f925,plain,
accept_population(muslimcountrybhumanitarianorganization,christian,n25),
inference(flattening,[],[f924]) ).
fof(f932,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(ennf_transformation,[],[f3]) ).
fof(f933,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(flattening,[],[f932]) ).
fof(f938,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2)) ),
inference(ennf_transformation,[],[f911]) ).
fof(f939,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2)) ),
inference(flattening,[],[f938]) ).
fof(f941,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(ennf_transformation,[],[f913]) ).
fof(f942,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(flattening,[],[f941]) ).
fof(f944,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(ennf_transformation,[],[f915]) ).
fof(f946,plain,
! [X0,X1,X2,X3] :
( less(X0,X1)
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_positive_less(X2,X3) ),
inference(ennf_transformation,[],[f917]) ).
fof(f947,plain,
! [X0,X1,X2,X3] :
( less(X0,X1)
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_positive_less(X2,X3) ),
inference(flattening,[],[f946]) ).
fof(f957,plain,
! [X2,X3,X0,X1] :
( accept_population(X0,X3,X2)
| ~ accept_population(X0,X3,X1)
| ~ less(X2,X1) ),
inference(cnf_transformation,[],[f933]) ).
fof(f1010,plain,
! [X0] :
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,other,n0)
| accept_city(X0,towna)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75) ),
inference(cnf_transformation,[],[f16]) ).
fof(f1381,plain,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
inference(cnf_transformation,[],[f362]) ).
fof(f1491,plain,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
inference(cnf_transformation,[],[f472]) ).
fof(f1492,plain,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1),
inference(cnf_transformation,[],[f473]) ).
fof(f1494,plain,
accept_population(muslimcountrybhumanitarianorganization,atheist,n78),
inference(cnf_transformation,[],[f475]) ).
fof(f1654,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(cnf_transformation,[],[f635]) ).
fof(f1680,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(cnf_transformation,[],[f661]) ).
fof(f1681,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(cnf_transformation,[],[f662]) ).
fof(f1731,plain,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
inference(cnf_transformation,[],[f712]) ).
fof(f1732,plain,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
inference(cnf_transformation,[],[f713]) ).
fof(f1734,plain,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
inference(cnf_transformation,[],[f715]) ).
fof(f1913,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(cnf_transformation,[],[f894]) ).
fof(f1918,plain,
rdn_non_zero_digit(rdnn(n7)),
inference(cnf_transformation,[],[f899]) ).
fof(f1925,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f906]) ).
fof(f1926,plain,
rdn_positive_less(rdnn(n5),rdnn(n6)),
inference(cnf_transformation,[],[f907]) ).
fof(f1927,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(cnf_transformation,[],[f908]) ).
fof(f1928,plain,
rdn_positive_less(rdnn(n7),rdnn(n8)),
inference(cnf_transformation,[],[f909]) ).
fof(f1930,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_positive_less(rdnn(X0),rdnn(X1))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2)) ),
inference(cnf_transformation,[],[f939]) ).
fof(f1932,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X1))
| ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_non_zero(X1) ),
inference(cnf_transformation,[],[f942]) ).
fof(f1934,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[],[f944]) ).
fof(f1936,plain,
! [X2,X3,X0,X1] :
( less(X0,X1)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_positive_less(X2,X3) ),
inference(cnf_transformation,[],[f947]) ).
fof(f1939,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f920]) ).
fof(f1940,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f920]) ).
fof(f1941,plain,
! [X0,X1] :
( less(X1,X0)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f920]) ).
fof(f1942,plain,
accept_population(muslimcountrybhumanitarianorganization,christian,n25),
inference(cnf_transformation,[],[f925]) ).
fof(f1943,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f1939]) ).
fof(f2282,plain,
! [X2,X0,X1] :
( ~ rdn_translate(X0,rdn_pos(X1))
| ~ rdn_translate(X0,rdn_pos(X2))
| ~ rdn_positive_less(X2,X1) ),
inference(resolution,[],[f1936,f1943]) ).
fof(f2283,plain,
! [X2,X3,X0,X1] :
( ~ rdn_translate(X0,rdn_pos(X1))
| ~ rdn_translate(X2,rdn_pos(X3))
| ~ rdn_positive_less(X3,X1)
| ~ less(X0,X2) ),
inference(resolution,[],[f1936,f1940]) ).
fof(f2331,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(resolution,[],[f1010,f1491]) ).
fof(f2337,plain,
( accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(forward_subsumption_resolution,[],[f2331,f1381]) ).
fof(f2340,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(forward_subsumption_resolution,[],[f2337,f1654]) ).
fof(f2342,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(forward_subsumption_resolution,[],[f2340,f1492]) ).
fof(f2397,definition,
( spl0_1
<=> accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f2398,plain,
( accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f2397]) ).
fof(f2399,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| spl0_1 ),
inference(avatar_component_clause,[],[f2397]) ).
fof(f2437,plain,
( ! [X0] :
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,X0)
| ~ less(n75,X0) )
| spl0_1 ),
inference(resolution,[],[f2399,f957]) ).
fof(f2503,plain,
( ~ less(n75,n78)
| spl0_1 ),
inference(resolution,[],[f2437,f1494]) ).
fof(f3162,plain,
! [X2,X3,X0,X1] :
( ~ rdn_positive_less(rdnn(X0),rdnn(X2))
| ~ rdn_translate(X3,rdn_pos(rdn(rdnn(X2),X1)))
| ~ rdn_translate(X3,rdn_pos(rdn(rdnn(X0),X1)))
| ~ rdn_non_zero(X1) ),
inference(resolution,[],[f2282,f1932]) ).
fof(f3514,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n8),rdnn(n7)))
| ~ rdn_translate(X0,rdn_pos(X1))
| ~ less(n78,X0) ),
inference(resolution,[],[f2283,f1734]) ).
fof(f3519,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n6),rdnn(n7)))
| ~ rdn_translate(X0,rdn_pos(X1))
| ~ less(n76,X0) ),
inference(resolution,[],[f2283,f1732]) ).
fof(f3575,plain,
! [X0,X1] :
( ~ rdn_positive_less(X1,rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(X0,rdn_pos(X1))
| ~ less(n25,X0) ),
inference(resolution,[],[f2283,f1681]) ).
fof(f4134,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2342,f2398]) ).
fof(f4136,plain,
( ! [X0] :
( ~ accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| ~ less(n24,X0) )
| ~ spl0_1 ),
inference(resolution,[],[f4134,f957]) ).
fof(f4140,plain,
( ~ less(n24,n25)
| ~ spl0_1 ),
inference(resolution,[],[f4136,f1942]) ).
fof(f4620,plain,
( n75 = n78
| less(n78,n75)
| spl0_1 ),
inference(resolution,[],[f2503,f1941]) ).
fof(f4690,definition,
( spl0_107
<=> less(n78,n75) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f4692,plain,
( less(n78,n75)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f4690]) ).
fof(f4694,definition,
( spl0_108
<=> n75 = n78 ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f4696,plain,
( n75 = n78
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f4694]) ).
fof(f4697,plain,
( spl0_107
| spl0_108
| spl0_1 ),
inference(avatar_split_clause,[],[f4620,f2397,f4694,f4690]) ).
fof(f5247,definition,
( spl0_119
<=> less(n25,n24) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f5248,plain,
( ~ less(n25,n24)
| spl0_119 ),
inference(avatar_component_clause,[],[f5247]) ).
fof(f5249,plain,
( less(n25,n24)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f5247]) ).
fof(f5251,definition,
( spl0_120
<=> n24 = n25 ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f5253,plain,
( n24 = n25
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f5251]) ).
fof(f5952,plain,
( n24 = n25
| less(n24,n25)
| spl0_119 ),
inference(resolution,[],[f5248,f1941]) ).
fof(f5954,definition,
( spl0_141
<=> less(n24,n25) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f5956,plain,
( less(n24,n25)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f5954]) ).
fof(f5957,plain,
( spl0_141
| spl0_120
| spl0_119 ),
inference(avatar_split_clause,[],[f5952,f5247,f5251,f5954]) ).
fof(f38519,definition,
( spl0_419
<=> rdn_non_zero(rdnn(n7)) ),
introduced(definition,[new_symbols(definition,[spl0_419])],[avatar_definition]) ).
fof(f38520,plain,
( rdn_non_zero(rdnn(n7))
| ~ spl0_419 ),
inference(avatar_component_clause,[],[f38519]) ).
fof(f38521,plain,
( ~ rdn_non_zero(rdnn(n7))
| spl0_419 ),
inference(avatar_component_clause,[],[f38519]) ).
fof(f38654,plain,
( ~ rdn_non_zero_digit(rdnn(n7))
| spl0_419 ),
inference(resolution,[],[f38521,f1934]) ).
fof(f38655,plain,
( $false
| spl0_419 ),
inference(forward_subsumption_resolution,[],[f38654,f1918]) ).
fof(f38656,plain,
spl0_419,
inference(avatar_contradiction_clause,[],[f38655]) ).
fof(f41735,definition,
( spl0_439
<=> rdn_non_zero(rdnn(n2)) ),
introduced(definition,[new_symbols(definition,[spl0_439])],[avatar_definition]) ).
fof(f41736,plain,
( rdn_non_zero(rdnn(n2))
| ~ spl0_439 ),
inference(avatar_component_clause,[],[f41735]) ).
fof(f41737,plain,
( ~ rdn_non_zero(rdnn(n2))
| spl0_439 ),
inference(avatar_component_clause,[],[f41735]) ).
fof(f41742,plain,
( ~ rdn_non_zero_digit(rdnn(n2))
| spl0_439 ),
inference(resolution,[],[f41737,f1934]) ).
fof(f41743,plain,
( $false
| spl0_439 ),
inference(forward_subsumption_resolution,[],[f41742,f1913]) ).
fof(f41744,plain,
spl0_439,
inference(avatar_contradiction_clause,[],[f41743]) ).
fof(f43788,plain,
( $false
| ~ spl0_1
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f4140,f5956]) ).
fof(f43789,plain,
( ~ spl0_1
| ~ spl0_141 ),
inference(avatar_contradiction_clause,[],[f43788]) ).
fof(f49188,plain,
! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdn(rdnn(X0),rdnn(n7))))
| ~ less(n78,X1)
| ~ rdn_positive_less(rdnn(X0),rdnn(n8))
| ~ rdn_non_zero(rdnn(n7)) ),
inference(resolution,[],[f3514,f1932]) ).
fof(f49189,plain,
( ! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdn(rdnn(X0),rdnn(n7))))
| ~ less(n78,X1)
| ~ rdn_positive_less(rdnn(X0),rdnn(n8)) )
| ~ spl0_419 ),
inference(forward_subsumption_resolution,[],[f49188,f38520]) ).
fof(f49225,plain,
! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdn(rdnn(X0),rdnn(n7))))
| ~ less(n76,X1)
| ~ rdn_positive_less(rdnn(X0),rdnn(n6))
| ~ rdn_non_zero(rdnn(n7)) ),
inference(resolution,[],[f3519,f1932]) ).
fof(f49226,plain,
( ! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdn(rdnn(X0),rdnn(n7))))
| ~ less(n76,X1)
| ~ rdn_positive_less(rdnn(X0),rdnn(n6)) )
| ~ spl0_419 ),
inference(forward_subsumption_resolution,[],[f49225,f38520]) ).
fof(f49518,plain,
! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdn(rdnn(X0),rdnn(n2))))
| ~ less(n25,X1)
| ~ rdn_positive_less(rdnn(X0),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2)) ),
inference(resolution,[],[f3575,f1932]) ).
fof(f49519,plain,
( ! [X0,X1] :
( ~ rdn_translate(X1,rdn_pos(rdn(rdnn(X0),rdnn(n2))))
| ~ less(n25,X1)
| ~ rdn_positive_less(rdnn(X0),rdnn(n5)) )
| ~ spl0_439 ),
inference(forward_subsumption_resolution,[],[f49518,f41736]) ).
fof(f54505,plain,
! [X0] :
( ~ rdn_positive_less(rdnn(n4),rdnn(X0))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(X0),rdnn(n2))))
| ~ rdn_non_zero(rdnn(n2)) ),
inference(resolution,[],[f3162,f1680]) ).
fof(f54569,plain,
( ! [X0] :
( ~ rdn_translate(n24,rdn_pos(rdn(rdnn(X0),rdnn(n2))))
| ~ rdn_positive_less(rdnn(n4),rdnn(X0)) )
| ~ spl0_439 ),
inference(forward_subsumption_resolution,[],[f54505,f41736]) ).
fof(f58713,plain,
( ~ less(n78,n76)
| ~ rdn_positive_less(rdnn(n6),rdnn(n8))
| ~ spl0_419 ),
inference(resolution,[],[f49189,f1732]) ).
fof(f58783,plain,
( ~ less(n76,n75)
| ~ rdn_positive_less(rdnn(n5),rdnn(n6))
| ~ spl0_419 ),
inference(resolution,[],[f49226,f1731]) ).
fof(f58792,plain,
( ~ less(n76,n75)
| ~ spl0_419 ),
inference(forward_subsumption_resolution,[],[f58783,f1926]) ).
fof(f58880,plain,
( ~ less(n25,n24)
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ spl0_439 ),
inference(resolution,[],[f49519,f1680]) ).
fof(f58888,plain,
( ~ less(n25,n24)
| ~ spl0_439 ),
inference(forward_subsumption_resolution,[],[f58880,f1925]) ).
fof(f60041,plain,
( n75 = n76
| less(n75,n76)
| ~ spl0_419 ),
inference(resolution,[],[f58792,f1941]) ).
fof(f60668,plain,
( ! [X0] :
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,X0)
| ~ less(n75,X0) )
| spl0_1 ),
inference(resolution,[],[f2399,f957]) ).
fof(f61107,plain,
( ! [X0,X1] :
( ~ less(n75,X0)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,X1)
| ~ less(X0,X1) )
| spl0_1 ),
inference(resolution,[],[f60668,f957]) ).
fof(f61404,plain,
( ! [X0] :
( ~ less(n75,X0)
| ~ less(X0,n78) )
| spl0_1 ),
inference(resolution,[],[f61107,f1494]) ).
fof(f73688,plain,
( $false
| ~ spl0_119
| ~ spl0_439 ),
inference(forward_subsumption_resolution,[],[f58888,f5249]) ).
fof(f73689,plain,
( ~ spl0_119
| ~ spl0_439 ),
inference(avatar_contradiction_clause,[],[f73688]) ).
fof(f73703,plain,
( rdn_translate(n24,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| ~ spl0_120 ),
inference(superposition,[],[f1681,f5253]) ).
fof(f88002,definition,
( spl0_1464
<=> less(n75,n76) ),
introduced(definition,[new_symbols(definition,[spl0_1464])],[avatar_definition]) ).
fof(f88004,plain,
( less(n75,n76)
| ~ spl0_1464 ),
inference(avatar_component_clause,[],[f88002]) ).
fof(f88006,definition,
( spl0_1465
<=> n75 = n76 ),
introduced(definition,[new_symbols(definition,[spl0_1465])],[avatar_definition]) ).
fof(f88008,plain,
( n75 = n76
| ~ spl0_1465 ),
inference(avatar_component_clause,[],[f88006]) ).
fof(f88009,plain,
( spl0_1464
| spl0_1465
| ~ spl0_419 ),
inference(avatar_split_clause,[],[f60041,f38519,f88006,f88002]) ).
fof(f89431,definition,
( spl0_1537
<=> n78 = n76 ),
introduced(definition,[new_symbols(definition,[spl0_1537])],[avatar_definition]) ).
fof(f89432,plain,
( n78 != n76
| spl0_1537 ),
inference(avatar_component_clause,[],[f89431]) ).
fof(f89433,plain,
( n78 = n76
| ~ spl0_1537 ),
inference(avatar_component_clause,[],[f89431]) ).
fof(f89435,definition,
( spl0_1538
<=> less(n76,n78) ),
introduced(definition,[new_symbols(definition,[spl0_1538])],[avatar_definition]) ).
fof(f89436,plain,
( ~ less(n76,n78)
| spl0_1538 ),
inference(avatar_component_clause,[],[f89435]) ).
fof(f89437,plain,
( less(n76,n78)
| ~ spl0_1538 ),
inference(avatar_component_clause,[],[f89435]) ).
fof(f89443,plain,
( ~ less(n75,n76)
| spl0_1
| ~ spl0_1538 ),
inference(resolution,[],[f89437,f61404]) ).
fof(f89446,plain,
( $false
| spl0_1
| ~ spl0_1464
| ~ spl0_1538 ),
inference(forward_subsumption_resolution,[],[f89443,f88004]) ).
fof(f89447,plain,
( spl0_1
| ~ spl0_1464
| ~ spl0_1538 ),
inference(avatar_contradiction_clause,[],[f89446]) ).
fof(f89484,plain,
( ~ less(n78,n75)
| ~ spl0_419
| ~ spl0_1537 ),
inference(superposition,[],[f58792,f89433]) ).
fof(f89511,plain,
( $false
| ~ spl0_107
| ~ spl0_419
| ~ spl0_1537 ),
inference(forward_subsumption_resolution,[],[f89484,f4692]) ).
fof(f89512,plain,
( ~ spl0_107
| ~ spl0_419
| ~ spl0_1537 ),
inference(avatar_contradiction_clause,[],[f89511]) ).
fof(f89535,plain,
( accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ spl0_108 ),
inference(superposition,[],[f1494,f4696]) ).
fof(f89599,plain,
( $false
| spl0_1
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f89535,f2399]) ).
fof(f89600,plain,
( spl0_1
| ~ spl0_108 ),
inference(avatar_contradiction_clause,[],[f89599]) ).
fof(f89634,plain,
( n78 = n76
| less(n78,n76)
| spl0_1538 ),
inference(resolution,[],[f89436,f1941]) ).
fof(f89635,plain,
( less(n78,n76)
| spl0_1537
| spl0_1538 ),
inference(forward_subsumption_resolution,[],[f89634,f89432]) ).
fof(f93377,plain,
( ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ spl0_120
| ~ spl0_439 ),
inference(resolution,[],[f73703,f54569]) ).
fof(f93553,plain,
( $false
| ~ spl0_120
| ~ spl0_439 ),
inference(forward_subsumption_resolution,[],[f93377,f1925]) ).
fof(f93554,plain,
( ~ spl0_120
| ~ spl0_439 ),
inference(avatar_contradiction_clause,[],[f93553]) ).
fof(f96024,plain,
( less(n75,n78)
| ~ spl0_1465
| ~ spl0_1538 ),
inference(forward_demodulation,[],[f89437,f88008]) ).
fof(f96025,plain,
( $false
| spl0_1
| ~ spl0_1465
| ~ spl0_1538 ),
inference(forward_subsumption_resolution,[],[f96024,f2503]) ).
fof(f96026,plain,
( spl0_1
| ~ spl0_1465
| ~ spl0_1538 ),
inference(avatar_contradiction_clause,[],[f96025]) ).
fof(f96364,plain,
( ~ rdn_positive_less(rdnn(n6),rdnn(n8))
| ~ spl0_419
| spl0_1537
| spl0_1538 ),
inference(forward_subsumption_resolution,[],[f58713,f89635]) ).
fof(f96369,plain,
( ! [X0] :
( ~ rdn_positive_less(rdnn(n6),rdnn(X0))
| ~ rdn_positive_less(rdnn(X0),rdnn(n8)) )
| ~ spl0_419
| spl0_1537
| spl0_1538 ),
inference(resolution,[],[f96364,f1930]) ).
fof(f118043,plain,
( ~ rdn_positive_less(rdnn(n6),rdnn(n7))
| ~ spl0_419
| spl0_1537
| spl0_1538 ),
inference(resolution,[],[f96369,f1928]) ).
fof(f118048,plain,
( $false
| ~ spl0_419
| spl0_1537
| spl0_1538 ),
inference(forward_subsumption_resolution,[],[f118043,f1927]) ).
fof(f118049,plain,
( ~ spl0_419
| spl0_1537
| spl0_1538 ),
inference(avatar_contradiction_clause,[],[f118048]) ).
cnf(s41,plain,
( spl0_1
| spl0_107
| spl0_108 ),
inference(sat_conversion,[],[f4697]) ).
cnf(s101,plain,
( spl0_119
| spl0_120
| spl0_141 ),
inference(sat_conversion,[],[f5957]) ).
cnf(s271,plain,
spl0_419,
inference(sat_conversion,[],[f38656]) ).
cnf(s295,plain,
spl0_439,
inference(sat_conversion,[],[f41744]) ).
cnf(s334,plain,
( ~ spl0_1
| ~ spl0_141 ),
inference(sat_conversion,[],[f43789]) ).
cnf(s789,plain,
( ~ spl0_119
| ~ spl0_439 ),
inference(sat_conversion,[],[f73689]) ).
cnf(s1222,plain,
( ~ spl0_419
| spl0_1464
| spl0_1465 ),
inference(sat_conversion,[],[f88009]) ).
cnf(s1283,plain,
( spl0_1
| ~ spl0_1464
| ~ spl0_1538 ),
inference(sat_conversion,[],[f89447]) ).
cnf(s1285,plain,
( ~ spl0_107
| ~ spl0_419
| ~ spl0_1537 ),
inference(sat_conversion,[],[f89512]) ).
cnf(s1287,plain,
( spl0_1
| ~ spl0_108 ),
inference(sat_conversion,[],[f89600]) ).
cnf(s1345,plain,
( ~ spl0_120
| ~ spl0_439 ),
inference(sat_conversion,[],[f93554]) ).
cnf(s1414,plain,
( spl0_1
| ~ spl0_1465
| ~ spl0_1538 ),
inference(sat_conversion,[],[f96026]) ).
cnf(s1893,plain,
( ~ spl0_419
| spl0_1537
| spl0_1538 ),
inference(sat_conversion,[],[f118049]) ).
cnf(s2002,plain,
~ spl0_120,
inference(rat,[],[s1345,s295]) ).
cnf(s2039,plain,
~ spl0_119,
inference(rat,[],[s789,s295]) ).
cnf(s2602,plain,
spl0_141,
inference(rat,[],[s101,s2002,s2039]) ).
cnf(s2606,plain,
~ spl0_1,
inference(rat,[],[s334,s2602]) ).
cnf(s2610,plain,
~ spl0_108,
inference(rat,[],[s1287,s2606]) ).
cnf(s2635,plain,
spl0_107,
inference(rat,[],[s41,s2610,s2606]) ).
cnf(s2638,plain,
~ spl0_1537,
inference(rat,[],[s1285,s271,s2635]) ).
cnf(s2641,plain,
spl0_1538,
inference(rat,[],[s1893,s271,s2638]) ).
cnf(s2644,plain,
~ spl0_1465,
inference(rat,[],[s1414,s2606,s2641]) ).
cnf(s2645,plain,
~ spl0_1464,
inference(rat,[],[s1283,s2606,s2641]) ).
cnf(s2649,plain,
$false,
inference(rat,[],[s1222,s271,s2644,s2645]) ).
fof(f118050,plain,
$false,
inference(avatar_sat_refutation,[],[s2649]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT013+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n019.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:10:48 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 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
% 18.17/2.95 % (131941)Will run a generic schedule for satisfiability detection.
% 18.17/2.95 % (131950)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3995096241:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 18.17/2.95 % (131947)% WARNING: option uhcvi not known.
% 18.17/2.95 % (131946)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3672171525_2999 on theBenchmark for (2999ds/0Mi)
% 18.17/2.95 % (131947)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1974593189:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 18.17/2.95 % (131948)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1881656430:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 18.17/2.95 % (131949)dis+10_1_sil=32000:sp=arity:random_seed=4196795564:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 18.17/2.95 % (131951)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=770943154:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 18.17/2.95 % (131952)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2185407073:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 18.17/2.95 % (131950)Instruction limit reached!
% 18.17/2.95 % (131950)------------------------------
% 18.17/2.95 % (131950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.17/2.95 % (131950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.17/2.95 % (131950)CaDiCaL version: 2.1.3
% 18.17/2.95 % (131950)Termination reason: Instruction limit
% 18.17/2.95 % (131950)Termination phase: Saturation
% 18.17/2.95 % (131950)Time elapsed: 0.033 s
% 18.17/2.95 % (131950)Peak memory usage: 14 MB
% 18.17/2.95 % (131950)Instructions burned: 120 (million)
% 18.17/2.95 % (131960)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1262278139:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 18.17/2.95 % TRYING [1]
% 18.17/2.95 % TRYING [2]
% 18.17/2.95 % (131949)Instruction limit reached!
% 18.17/2.95 % (131949)------------------------------
% 18.17/2.95 % (131949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.17/2.95 % (131949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.17/2.95 % (131949)CaDiCaL version: 2.1.3
% 18.17/2.95 % (131949)Termination reason: Instruction limit
% 18.17/2.95 % (131949)Termination phase: Saturation
% 18.17/2.95 % (131949)Time elapsed: 0.052 s
% 18.17/2.95 % (131949)Peak memory usage: 13 MB
% 18.17/2.95 % (131949)Instructions burned: 105 (million)
% 18.17/2.95 % TRYING [1]
% 18.17/2.95 % TRYING [2]
% 18.17/2.95 % (131951)Instruction limit reached!
% 18.17/2.95 % (131951)------------------------------
% 18.17/2.95 % (131951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.17/2.95 % (131951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.17/2.95 % (131951)CaDiCaL version: 2.1.3
% 18.17/2.95 % (131951)Termination reason: Instruction limit
% 18.17/2.95 % (131951)Termination phase: Saturation
% 18.17/2.95 % (131951)Time elapsed: 0.065 s
% 18.17/2.95 % (131951)Peak memory usage: 15 MB
% 18.17/2.95 % (131951)Instructions burned: 132 (million)
% 18.17/2.95 % TRYING [3]
% 18.17/2.95 % TRYING [3]
% 18.17/2.95 % (131962)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1251932452:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 18.17/2.95 % (131952)Instruction limit reached!
% 18.17/2.95 % (131952)------------------------------
% 18.17/2.95 % (131952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.17/2.95 % (131952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.17/2.95 % (131952)CaDiCaL version: 2.1.3
% 18.17/2.95 % (131952)Termination reason: Instruction limit
% 18.17/2.95 % (131952)Termination phase: Saturation
% 18.17/2.95 % (131952)Time elapsed: 0.085 s
% 18.17/2.95 % (131952)Peak memory usage: 15 MB
% 18.17/2.95 % (131952)Instructions burned: 160 (million)
% 18.17/2.95 % (131963)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=2270656012:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 18.17/2.95 % TRYING [4]
% 18.17/2.95 % (131966)ott-21_1_sil=16000:fs=off:random_seed=1000854281:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 18.17/2.95 % TRYING [4]
% 18.17/2.95 % (131962)Instruction limit reached!
% 18.17/2.95 % (131962)------------------------------
% 18.17/2.95 % (131962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.17/2.95 % (131962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131962)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131962)Termination reason: Instruction limit
% 23.06/3.59 % (131962)Termination phase: Saturation
% 23.06/3.59 % (131962)Time elapsed: 0.069 s
% 23.06/3.59 % (131962)Peak memory usage: 14 MB
% 23.06/3.59 % (131962)Instructions burned: 133 (million)
% 23.06/3.59 % (131968)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2664471646:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 23.06/3.59 % (131966)Instruction limit reached!
% 23.06/3.59 % (131966)------------------------------
% 23.06/3.59 % (131966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131966)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131966)Termination reason: Instruction limit
% 23.06/3.59 % (131966)Termination phase: Saturation
% 23.06/3.59 % (131966)Time elapsed: 0.083 s
% 23.06/3.59 % (131966)Peak memory usage: 13 MB
% 23.06/3.59 % (131966)Instructions burned: 180 (million)
% 23.06/3.59 % (131960)Instruction limit reached!
% 23.06/3.59 % (131960)------------------------------
% 23.06/3.59 % (131960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131960)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131960)Termination reason: Instruction limit
% 23.06/3.59 % (131960)Termination phase: Finite model building SAT solving
% 23.06/3.59 % (131960)Time elapsed: 0.160 s
% 23.06/3.59 % (131960)Peak memory usage: 32 MB
% 23.06/3.59 % (131960)Instructions burned: 716 (million)
% 23.06/3.59 % (131971)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1655963821:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 23.06/3.59 % (131970)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=998873538:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 23.06/3.59 % TRYING [1]
% 23.06/3.59 % TRYING [2]
% 23.06/3.59 % TRYING [5]
% 23.06/3.59 % TRYING [3]
% 23.06/3.59 % (131968)Instruction limit reached!
% 23.06/3.59 % (131968)------------------------------
% 23.06/3.59 % (131968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131968)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131968)Termination reason: Instruction limit
% 23.06/3.59 % (131968)Termination phase: Saturation
% 23.06/3.59 % (131968)Time elapsed: 0.237 s
% 23.06/3.59 % (131968)Peak memory usage: 17 MB
% 23.06/3.59 % (131968)Instructions burned: 478 (million)
% 23.06/3.59 % (131974)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3727945678:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 23.06/3.59 % (131963)Instruction limit reached!
% 23.06/3.59 % (131963)------------------------------
% 23.06/3.59 % (131963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131963)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131963)Termination reason: Instruction limit
% 23.06/3.59 % (131963)Termination phase: Saturation
% 23.06/3.59 % (131963)Time elapsed: 0.361 s
% 23.06/3.59 % (131963)Peak memory usage: 24 MB
% 23.06/3.59 % (131963)Instructions burned: 685 (million)
% 23.06/3.59 % (131976)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=2211341299: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)
% 23.06/3.59 % (131971)Instruction limit reached!
% 23.06/3.59 % (131971)------------------------------
% 23.06/3.59 % (131971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131971)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131971)Termination reason: Instruction limit
% 23.06/3.59 % (131971)Termination phase: Saturation
% 23.06/3.59 % (131971)Time elapsed: 0.262 s
% 23.06/3.59 % (131971)Peak memory usage: 25 MB
% 23.06/3.59 % (131971)Instructions burned: 1181 (million)
% 23.06/3.59 % (131978)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1509640220:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 23.06/3.59 % TRYING [14]
% 23.06/3.59 % (131970)Instruction limit reached!
% 23.06/3.59 % (131970)------------------------------
% 23.06/3.59 % (131970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131970)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131970)Termination reason: Instruction limit
% 23.06/3.59 % (131970)Termination phase: Finite model building SAT solving
% 23.06/3.59 % (131970)Time elapsed: 0.315 s
% 23.06/3.59 % (131970)Peak memory usage: 21 MB
% 23.06/3.59 % (131970)Instructions burned: 865 (million)
% 23.06/3.59 % (131980)fmb+10_1_sil=64000:random_seed=4115757320:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 23.06/3.59 % TRYING [1]
% 23.06/3.59 % TRYING [2]
% 23.06/3.59 % TRYING [3]
% 23.06/3.59 % (131978)Instruction limit reached!
% 23.06/3.59 % (131978)------------------------------
% 23.06/3.59 % (131978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131978)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131978)Termination reason: Instruction limit
% 23.06/3.59 % (131978)Termination phase: Saturation
% 23.06/3.59 % (131978)Time elapsed: 0.219 s
% 23.06/3.59 % (131978)Peak memory usage: 24 MB
% 23.06/3.59 % (131978)Instructions burned: 881 (million)
% 23.06/3.59 % (131982)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1346275190:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 23.06/3.59 % TRYING [6]
% 23.06/3.59 % TRYING [20]
% 23.06/3.59 % (131974)Instruction limit reached!
% 23.06/3.59 % (131974)------------------------------
% 23.06/3.59 % (131974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131974)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131974)Termination reason: Instruction limit
% 23.06/3.59 % (131974)Termination phase: Finite model building constraint generation
% 23.06/3.59 % (131974)Time elapsed: 0.328 s
% 23.06/3.59 % (131974)Peak memory usage: 75 MB
% 23.06/3.59 % (131974)Instructions burned: 889 (million)
% 23.06/3.59 % (131984)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2372380331:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 23.06/3.59 % TRYING [8]
% 23.06/3.59 % (131976)Instruction limit reached!
% 23.06/3.59 % (131976)------------------------------
% 23.06/3.59 % (131976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131976)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131976)Termination reason: Instruction limit
% 23.06/3.59 % (131976)Termination phase: Saturation
% 23.06/3.59 % (131976)Time elapsed: 0.362 s
% 23.06/3.59 % (131976)Peak memory usage: 22 MB
% 23.06/3.59 % (131976)Instructions burned: 693 (million)
% 23.06/3.59 % (131986)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=649059283:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 23.06/3.59 % TRYING [4]
% 23.06/3.59 % (131984)Instruction limit reached!
% 23.06/3.59 % (131984)------------------------------
% 23.06/3.59 % (131984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131984)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131984)Termination reason: Instruction limit
% 23.06/3.59 % (131984)Termination phase: Finite model building constraint generation
% 23.06/3.59 % (131984)Time elapsed: 0.325 s
% 23.06/3.59 % (131984)Peak memory usage: 68 MB
% 23.06/3.59 % (131984)Instructions burned: 920 (million)
% 23.06/3.59 % (131988)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2634097852:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 23.06/3.59 % TRYING [7]
% 23.06/3.59 % TRYING [5]
% 23.06/3.59 % (131988)Instruction limit reached!
% 23.06/3.59 % (131988)------------------------------
% 23.06/3.59 % (131988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131988)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131988)Termination reason: Instruction limit
% 23.06/3.59 % (131988)Termination phase: Saturation
% 23.06/3.59 % (131988)Time elapsed: 0.790 s
% 23.06/3.59 % (131988)Peak memory usage: 30 MB
% 23.06/3.59 % (131988)Instructions burned: 1473 (million)
% 23.06/3.59 % (131990)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=431583793:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 23.06/3.59 % TRYING [77]
% 23.06/3.59 % TRYING [8]
% 23.06/3.59 % (131982)Instruction limit reached!
% 23.06/3.59 % (131982)------------------------------
% 23.06/3.59 % (131982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131982)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131982)Termination reason: Instruction limit
% 23.06/3.59 % (131982)Termination phase: Finite model building constraint generation
% 23.06/3.59 % (131982)Time elapsed: 1.954 s
% 23.06/3.59 % (131982)Peak memory usage: 563 MB
% 23.06/3.59 % (131982)Instructions burned: 9521 (million)
% 23.06/3.59 % (131992)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3039287049:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi)
% 23.06/3.59 % TRYING [16]
% 23.06/3.59 % TRYING [6]
% 23.06/3.59 % (131992)Instruction limit reached!
% 23.06/3.59 % (131992)------------------------------
% 23.06/3.59 % (131992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.59 % (131992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.59 % (131992)CaDiCaL version: 2.1.3
% 23.06/3.59 % (131992)Termination reason: Instruction limit
% 23.06/3.59 % (131992)Termination phase: Finite model building constraint generation
% 23.06/3.59 % (131992)Time elapsed: 0.434 s
% 23.06/3.59 % (131992)Peak memory usage: 153 MB
% 23.06/3.59 % (131992)Instructions burned: 2179 (million)
% 23.06/3.59 % (131994)ott-2_1_sil=16000:newcnf=on:random_seed=805018920:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 23.06/3.59 % (131986) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-131941-131986"...
% 23.06/3.59 % (131986)...printing done.
% 23.06/3.59 % (131986)Refutation found. Thanks to Tanya!
% 23.06/3.59 % SZS status Theorem for theBenchmark
% 23.06/3.59 % SZS output start Proof for theBenchmark
% See solution above
% 23.06/3.60 % (131986)------------------------------
% 23.06/3.60 % (131986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.06/3.60 % (131986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.06/3.60 % (131986)CaDiCaL version: 2.1.3
% 23.06/3.60 % (131986)Termination reason: Refutation
% 23.06/3.60 % (131986)Time elapsed: 2.410 s
% 23.06/3.60 % (131986)Peak memory usage: 45 MB
% 23.06/3.60 % (131986)Instructions burned: 4495 (million)
% 23.06/3.60 % (131941)Success in time 3.366 s
% 23.06/3.60 % Vampire exiting
%------------------------------------------------------------------------------