%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : AGT011+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 11:47:12 AM UTC 2026
% Result : Theorem 108.02s 14.62s
% Output : CNFRefutation 69.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 39
% Syntax : Number of formulae : 153 ( 52 unt; 9 def)
% Number of atoms : 397 ( 11 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 447 ( 203 ~; 204 |; 23 &)
% ( 11 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 10 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 24 con; 0-2 aty)
% Number of variables : 173 ( 173 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A,N,M] :
( ( less(M,N)
& accept_number(A,N) )
=> accept_number(A,M) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,N,M,P] :
( ( less(M,N)
& accept_population(A,P,N) )
=> accept_population(A,P,M) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( ( accept_population(A,other,n0)
& accept_population(A,native,n85)
& accept_population(A,muslim,n0)
& accept_population(A,christian,n3)
& accept_population(A,atheist,n12) )
<=> accept_city(A,coastvillage) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f235,axiom,
accept_number(countryccivilorganization,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f282,axiom,
~ accept_city(countryamedicalorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,axiom,
accept_population(countryamedicalorganization,muslim,n65),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f287,axiom,
accept_population(countryamedicalorganization,atheist,n30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f331,axiom,
~ accept_number(countryccivilorganization,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f480,axiom,
accept_population(countryamedicalorganization,christian,n20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f489,axiom,
accept_population(countryamedicalorganization,other,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f637,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f643,axiom,
rdn_translate(n6,rdn_pos(rdnn(n6))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f649,axiom,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f651,axiom,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f657,axiom,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f662,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f667,axiom,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f702,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f722,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f737,axiom,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f893,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f898,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f903,axiom,
rdn_positive_less(rdnn(n1),rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f904,axiom,
rdn_positive_less(rdnn(n2),rdnn(n3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f912,axiom,
! [Ds,Os,Db,Ob] :
( rdn_positive_less(Os,Ob)
=> rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f914,axiom,
! [D,Db,Ob] :
( rdn_non_zero(Ob)
=> rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f915,axiom,
! [X] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f917,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_positive_less(RDN_X,RDN_Y)
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> less(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f920,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f923,conjecture,
~ accept_population(countryamedicalorganization,native,n100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f924,negated_conjecture,
~ ~ accept_population(countryamedicalorganization,native,n100),
inference(negated_conjecture,[status(cth)],[f923]) ).
fof(f931,plain,
! [A,N,M] :
( accept_number(A,M)
| ~ less(M,N)
| ~ accept_number(A,N) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f932,plain,
! [A,M] :
( accept_number(A,M)
| ! [N] :
( ~ less(M,N)
| ~ accept_number(A,N) ) ),
inference(miniscoping,[status(thm)],[f931]) ).
fof(f933,plain,
! [X0,X1,X2] :
( accept_number(X0,X2)
| ~ less(X2,X1)
| ~ accept_number(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f932]) ).
fof(f934,plain,
! [A,N,M,P] :
( accept_population(A,P,M)
| ~ less(M,N)
| ~ accept_population(A,P,N) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f935,plain,
! [A,M,P] :
( accept_population(A,P,M)
| ! [N] :
( ~ less(M,N)
| ~ accept_population(A,P,N) ) ),
inference(miniscoping,[status(thm)],[f934]) ).
fof(f936,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X1,X3)
| ~ less(X3,X2)
| ~ accept_population(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f935]) ).
fof(f995,plain,
! [A] :
( ( ~ accept_city(A,coastvillage)
| ( accept_population(A,other,n0)
& accept_population(A,native,n85)
& accept_population(A,muslim,n0)
& accept_population(A,christian,n3)
& accept_population(A,atheist,n12) ) )
& ( accept_city(A,coastvillage)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,atheist,n12) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f996,plain,
( ! [A] :
( ~ accept_city(A,coastvillage)
| ( accept_population(A,other,n0)
& accept_population(A,native,n85)
& accept_population(A,muslim,n0)
& accept_population(A,christian,n3)
& accept_population(A,atheist,n12) ) )
& ! [A] :
( accept_city(A,coastvillage)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,atheist,n12) ) ),
inference(miniscoping,[status(thm)],[f995]) ).
fof(f997,plain,
! [X0] :
( accept_city(X0,coastvillage)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(cnf_transformation,[status(thm)],[f996]) ).
fof(f1265,plain,
accept_number(countryccivilorganization,n3),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f1312,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f1315,plain,
accept_population(countryamedicalorganization,muslim,n65),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f1317,plain,
accept_population(countryamedicalorganization,atheist,n30),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f1361,plain,
~ accept_number(countryccivilorganization,n6),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f1510,plain,
accept_population(countryamedicalorganization,christian,n20),
inference(cnf_transformation,[status(thm)],[f480]) ).
fof(f1519,plain,
accept_population(countryamedicalorganization,other,n0),
inference(cnf_transformation,[status(thm)],[f489]) ).
fof(f1667,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(cnf_transformation,[status(thm)],[f637]) ).
fof(f1673,plain,
rdn_translate(n6,rdn_pos(rdnn(n6))),
inference(cnf_transformation,[status(thm)],[f643]) ).
fof(f1679,plain,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
inference(cnf_transformation,[status(thm)],[f649]) ).
fof(f1681,plain,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
inference(cnf_transformation,[status(thm)],[f651]) ).
fof(f1687,plain,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
inference(cnf_transformation,[status(thm)],[f657]) ).
fof(f1692,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(cnf_transformation,[status(thm)],[f662]) ).
fof(f1697,plain,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f1732,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(cnf_transformation,[status(thm)],[f702]) ).
fof(f1752,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(cnf_transformation,[status(thm)],[f722]) ).
fof(f1767,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(cnf_transformation,[status(thm)],[f737]) ).
fof(f1923,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[status(thm)],[f893]) ).
fof(f1928,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(cnf_transformation,[status(thm)],[f898]) ).
fof(f1933,plain,
rdn_positive_less(rdnn(n1),rdnn(n2)),
inference(cnf_transformation,[status(thm)],[f903]) ).
fof(f1934,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(cnf_transformation,[status(thm)],[f904]) ).
fof(f1944,plain,
! [Ds,Os,Db,Ob] :
( rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob))
| ~ rdn_positive_less(Os,Ob) ),
inference(pre_NNF_transformation,[status(thm)],[f912]) ).
fof(f1945,plain,
! [Os,Ob] :
( ! [Ds,Db] : rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob))
| ~ rdn_positive_less(Os,Ob) ),
inference(miniscoping,[status(thm)],[f1944]) ).
fof(f1946,plain,
! [X0,X1,X2,X3] :
( rdn_positive_less(rdn(rdnn(X2),X0),rdn(rdnn(X3),X1))
| ~ rdn_positive_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1945]) ).
fof(f1949,plain,
! [D,Db,Ob] :
( rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(pre_NNF_transformation,[status(thm)],[f914]) ).
fof(f1950,plain,
! [Ob] :
( ! [D,Db] : rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(miniscoping,[status(thm)],[f1949]) ).
fof(f1951,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X1),rdn(rdnn(X2),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1950]) ).
fof(f1952,plain,
! [X] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f915]) ).
fof(f1953,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[status(thm)],[f1952]) ).
fof(f1957,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(pre_NNF_transformation,[status(thm)],[f917]) ).
fof(f1958,plain,
! [X,Y] :
( less(X,Y)
| ! [RDN_X,RDN_Y] :
( ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ) ),
inference(miniscoping,[status(thm)],[f1957]) ).
fof(f1959,plain,
! [X0,X1,X2,X3] :
( less(X0,X2)
| ~ rdn_positive_less(X1,X3)
| ~ rdn_translate(X2,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(cnf_transformation,[status(thm)],[f1958]) ).
fof(f1966,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f920]) ).
fof(f1967,plain,
( ! [X,Y] :
( Y = X
| less(Y,X)
| less(X,Y) )
& ! [X,Y] :
( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1966]) ).
fof(f1970,plain,
! [X0,X1] :
( X1 = X0
| less(X1,X0)
| less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1967]) ).
fof(f1979,plain,
accept_population(countryamedicalorganization,native,n100),
inference(cnf_transformation,[status(thm)],[f924]) ).
fof(f2194,plain,
( ~ accept_population(countryamedicalorganization,other,n0)
| ~ accept_population(countryamedicalorganization,native,n85)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(resolution,[status(thm)],[f997,f1312]) ).
fof(f2195,definition,
( sQ31_spl
<=> accept_population(countryamedicalorganization,atheist,n12) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f2197,plain,
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(component_clause,[status(thm)],[f2195]) ).
fof(f2198,definition,
( sQ32_spl
<=> accept_population(countryamedicalorganization,christian,n3) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f2200,plain,
( sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,n3) ),
inference(component_clause,[status(thm)],[f2198]) ).
fof(f2201,definition,
( sQ33_spl
<=> accept_population(countryamedicalorganization,muslim,n0) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f2203,plain,
( sQ33_spl
| ~ accept_population(countryamedicalorganization,muslim,n0) ),
inference(component_clause,[status(thm)],[f2201]) ).
fof(f2204,definition,
( sQ34_spl
<=> accept_population(countryamedicalorganization,native,n85) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f2206,plain,
( sQ34_spl
| ~ accept_population(countryamedicalorganization,native,n85) ),
inference(component_clause,[status(thm)],[f2204]) ).
fof(f2207,definition,
( sQ35_spl
<=> accept_population(countryamedicalorganization,other,n0) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f2209,plain,
( sQ35_spl
| ~ accept_population(countryamedicalorganization,other,n0) ),
inference(component_clause,[status(thm)],[f2207]) ).
fof(f2210,plain,
( ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2194,f2195,f2198,f2201,f2204,f2207]) ).
fof(f2211,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2209,f1519]) ).
fof(f2212,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f2211]) ).
fof(f2816,plain,
! [X0,X1,X2] :
( accept_number(X2,X1)
| ~ accept_number(X2,X0)
| X1 = X0
| less(X0,X1) ),
inference(resolution,[status(thm)],[f1970,f933]) ).
fof(f2821,plain,
! [X0] :
( ~ accept_number(countryccivilorganization,X0)
| n6 = X0
| less(X0,n6) ),
inference(resolution,[status(thm)],[f2816,f1361]) ).
fof(f2825,plain,
( n6 = n3
| less(n3,n6) ),
inference(resolution,[status(thm)],[f2821,f1265]) ).
fof(f2842,definition,
( sQ76_spl
<=> less(n3,n6) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f2843,plain,
( ~ sQ76_spl
| less(n3,n6) ),
inference(component_clause,[status(thm)],[f2842]) ).
fof(f2845,definition,
( sQ77_spl
<=> n6 = n3 ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2846,plain,
( ~ sQ77_spl
| n6 = n3 ),
inference(component_clause,[status(thm)],[f2845]) ).
fof(f2848,plain,
( sQ77_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f2825,f2842,f2845]) ).
fof(f2862,plain,
! [X0,X1] :
( ~ sQ76_spl
| accept_population(X0,X1,n3)
| ~ accept_population(X0,X1,n6) ),
inference(resolution,[status(thm)],[f2843,f936]) ).
fof(f3015,plain,
( ~ sQ77_spl
| accept_number(countryccivilorganization,n6) ),
inference(backward_demodulation,[status(thm)],[f2846,f1265]) ).
fof(f4254,plain,
! [X0,X1,X2,X3,X4,X5] :
( accept_population(X4,X5,X0)
| ~ accept_population(X4,X5,X2)
| ~ rdn_positive_less(X1,X3)
| ~ rdn_translate(X2,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1959,f936]) ).
fof(f4303,definition,
( sQ113_spl
<=> rdn_non_zero(rdnn(n1)) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f4304,plain,
( ~ sQ113_spl
| rdn_non_zero(rdnn(n1)) ),
inference(component_clause,[status(thm)],[f4303]) ).
fof(f4305,plain,
( sQ113_spl
| ~ rdn_non_zero(rdnn(n1)) ),
inference(component_clause,[status(thm)],[f4303]) ).
fof(f4335,plain,
( sQ113_spl
| ~ rdn_non_zero_digit(rdnn(n1)) ),
inference(resolution,[status(thm)],[f4305,f1953]) ).
fof(f4336,plain,
( sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4335,f1923]) ).
fof(f4337,plain,
sQ113_spl,
inference(contradiction_clause,[status(thm)],[f4336]) ).
fof(f5982,plain,
! [X0,X1,X2] :
( sQ34_spl
| ~ accept_population(countryamedicalorganization,native,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n85,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f4254,f2206]) ).
fof(f5983,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ76_spl
| accept_population(X3,X4,n3)
| ~ accept_population(X3,X4,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n6,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f4254,f2862]) ).
fof(f5996,plain,
! [X0,X1] :
( sQ34_spl
| ~ accept_population(countryamedicalorganization,native,X0)
| ~ rdn_positive_less(rdn(rdnn(n5),rdnn(n8)),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f5982,f1752]) ).
fof(f6013,plain,
! [X0,X1,X2] :
( sQ34_spl
| ~ rdn_positive_less(rdnn(n8),X2)
| ~ accept_population(countryamedicalorganization,native,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f5996,f1946]) ).
fof(f6023,plain,
! [X0,X1,X2] :
( sQ33_spl
| ~ accept_population(countryamedicalorganization,muslim,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n0,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f2203,f4254]) ).
fof(f6024,plain,
! [X0,X1] :
( sQ33_spl
| ~ accept_population(countryamedicalorganization,muslim,X0)
| ~ rdn_positive_less(rdnn(n0),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f6023,f1667]) ).
fof(f6042,plain,
! [X0,X1,X2,X3] :
( ~ sQ76_spl
| accept_population(X2,X3,n3)
| ~ accept_population(X2,X3,X0)
| ~ rdn_positive_less(rdnn(n6),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f5983,f1673]) ).
fof(f6076,plain,
! [X0,X1,X2] :
( sQ33_spl
| ~ rdn_non_zero(X2)
| ~ accept_population(countryamedicalorganization,muslim,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f6024,f1951]) ).
fof(f6081,plain,
! [X0,X1,X2] :
( sQ33_spl
| ~ rdn_non_zero_digit(rdnn(X2))
| ~ accept_population(countryamedicalorganization,muslim,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(X2)))) ),
inference(resolution,[status(thm)],[f6076,f1953]) ).
fof(f6154,plain,
! [X0,X1] :
( sQ33_spl
| ~ accept_population(countryamedicalorganization,muslim,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n6)))) ),
inference(resolution,[status(thm)],[f6081,f1928]) ).
fof(f6182,plain,
( sQ33_spl
| ~ accept_population(countryamedicalorganization,muslim,n65) ),
inference(resolution,[status(thm)],[f6154,f1732]) ).
fof(f6188,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6182,f1315]) ).
fof(f6189,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f6188]) ).
fof(f6191,plain,
! [X0,X1] :
( ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,X0)
| ~ rdn_positive_less(rdnn(n6),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f2200,f6042]) ).
fof(f6198,plain,
! [X0,X1,X2] :
( ~ sQ76_spl
| sQ32_spl
| ~ rdn_non_zero(X2)
| ~ accept_population(countryamedicalorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f6191,f1951]) ).
fof(f6202,plain,
! [X0,X1] :
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n1)))) ),
inference(resolution,[status(thm)],[f6198,f4304]) ).
fof(f6230,plain,
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,n14) ),
inference(resolution,[status(thm)],[f6202,f1681]) ).
fof(f6240,plain,
! [X0,X1,X2] :
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n14,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f6230,f4254]) ).
fof(f6356,plain,
! [X0,X1] :
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,X0)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n1)),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f6240,f1681]) ).
fof(f6358,plain,
! [X0,X1,X2] :
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ rdn_positive_less(rdnn(n1),X2)
| ~ accept_population(countryamedicalorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f6356,f1946]) ).
fof(f6364,plain,
! [X0,X1,X2] :
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n12,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f2197,f4254]) ).
fof(f6366,plain,
! [X0,X1] :
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ rdn_positive_less(rdn(rdnn(n2),rdnn(n1)),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f6364,f1679]) ).
fof(f6368,plain,
! [X0,X1,X2] :
( sQ31_spl
| ~ rdn_positive_less(rdnn(n1),X2)
| ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f6366,f1946]) ).
fof(f6482,plain,
! [X0,X1] :
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n2)))) ),
inference(resolution,[status(thm)],[f6358,f1933]) ).
fof(f6487,plain,
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| ~ accept_population(countryamedicalorganization,christian,n20) ),
inference(resolution,[status(thm)],[f6482,f1687]) ).
fof(f6496,plain,
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6487,f1510]) ).
fof(f6497,plain,
( ~ sQ113_spl
| ~ sQ76_spl
| sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f6496]) ).
fof(f6498,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3015,f1361]) ).
fof(f6499,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f6498]) ).
fof(f6502,plain,
! [X0,X1] :
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n2)))) ),
inference(resolution,[status(thm)],[f6368,f1933]) ).
fof(f6505,plain,
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,n25) ),
inference(resolution,[status(thm)],[f6502,f1692]) ).
fof(f6515,plain,
! [X0,X1,X2] :
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n25,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f6505,f4254]) ).
fof(f6622,plain,
! [X0,X1] :
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ rdn_positive_less(rdn(rdnn(n5),rdnn(n2)),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f6515,f1692]) ).
fof(f6624,plain,
! [X0,X1,X2] :
( sQ31_spl
| ~ rdn_positive_less(rdnn(n2),X2)
| ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f6622,f1946]) ).
fof(f6632,plain,
! [X0,X1] :
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n3)))) ),
inference(resolution,[status(thm)],[f6624,f1934]) ).
fof(f6637,plain,
( sQ31_spl
| ~ accept_population(countryamedicalorganization,atheist,n30) ),
inference(resolution,[status(thm)],[f6632,f1697]) ).
fof(f6645,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6637,f1317]) ).
fof(f6646,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f6645]) ).
fof(f8037,plain,
! [X0,X1,X2,X3] :
( sQ34_spl
| ~ rdn_non_zero(X3)
| ~ accept_population(countryamedicalorganization,native,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdn(rdnn(X2),X3)))) ),
inference(resolution,[status(thm)],[f6013,f1951]) ).
fof(f8795,plain,
( sQ34_spl
| ~ rdn_non_zero(rdnn(n1))
| ~ accept_population(countryamedicalorganization,native,n100) ),
inference(resolution,[status(thm)],[f8037,f1767]) ).
fof(f8796,definition,
( sQ255_spl
<=> accept_population(countryamedicalorganization,native,n100) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f8798,plain,
( sQ255_spl
| ~ accept_population(countryamedicalorganization,native,n100) ),
inference(component_clause,[status(thm)],[f8796]) ).
fof(f8799,plain,
( sQ34_spl
| ~ sQ113_spl
| ~ sQ255_spl ),
inference(split_clause,[status(thm)],[f8795,f8796,f4303,f2204]) ).
fof(f8800,plain,
( sQ255_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8798,f1979]) ).
fof(f8801,plain,
sQ255_spl,
inference(contradiction_clause,[status(thm)],[f8800]) ).
fof(f8802,plain,
$false,
inference(sat_refutation,[status(thm)],[f2210,f2212,f2848,f4337,f6189,f6497,f6499,f6646,f8799,f8801]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : AGT011+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.48 % Computer : n005.cluster.edu
% 0.17/0.48 % Model : x86_64 x86_64
% 0.17/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.48 % Memory : 8046.5625MB
% 0.17/0.48 % OS : Linux 6.8.0-71-generic
% 0.17/0.48 % CPULimit : 300
% 0.17/0.48 % WCLimit : 300
% 0.17/0.48 % DateTime : Mon Sep 21 12:48:33 UTC 2026
% 0.17/0.48 % CPUTime :
% 0.21/0.55 % Drodi V4.1.1
% 108.02/14.62 % Refutation found
% 108.02/14.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 108.02/14.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 59.24/15.82 % Elapsed time: 15.104271 seconds
% 59.24/15.82 % CPU time: 106.814107 seconds
% 59.24/15.82 % Total memory used: 359.083 MB
% 59.24/15.82 % Net memory used: 346.504 MB
%------------------------------------------------------------------------------