%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : AGT009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 11:47:12 AM UTC 2026
% Result : Theorem 2.23s 0.75s
% Output : CNFRefutation 2.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 26
% Syntax : Number of formulae : 105 ( 31 unt; 8 def)
% Number of atoms : 310 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 344 ( 139 ~; 132 |; 55 &)
% ( 12 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 9 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-2 aty)
% Number of variables : 121 ( 121 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,C,N,L] :
( accept_team(A,L,C,N)
<=> ( accept_number(A,N)
& accept_leader(A,L)
& accept_city(A,C) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,L,C] :
( any_agent_in_all_proposed_teams(A,L,C)
=> accept_leader(A,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,L,C] :
( the_agent_not_in_any_proposed_teams(A,L,C)
=> ~ ( accept_leader(A,L)
& accept_city(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n24)
& accept_population(A,atheist,n75) )
<=> accept_city(A,towna) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n0)
& accept_population(A,christian,n25)
& accept_population(A,atheist,n75) )
<=> accept_city(A,citya) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( ( accept_population(A,other,n1)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n20)
& accept_population(A,atheist,n78) )
<=> accept_city(A,cityb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f527,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f539,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f546,axiom,
! [Ds,O,Db] :
( ( rdn_non_zero(O)
& rdn_positive_less(rdnn(Ds),rdnn(Db)) )
=> rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f548,axiom,
! [X] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f550,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/sandbox/benchmark/theBenchmark.p') ).
fof(f556,conjecture,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f557,negated_conjecture,
~ ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
inference(negated_conjecture,[status(cth)],[f556]) ).
fof(f558,plain,
! [A,C,N,L] :
( ( ~ accept_number(A,N)
| ~ accept_leader(A,L)
| ~ accept_city(A,C)
| accept_team(A,L,C,N) )
& ( ( accept_number(A,N)
& accept_leader(A,L)
& accept_city(A,C) )
| ~ accept_team(A,L,C,N) ) ),
inference(NNF_transformation,[status(thm)],[f1]) ).
fof(f559,plain,
( ! [A,C,N,L] :
( ~ accept_number(A,N)
| ~ accept_leader(A,L)
| ~ accept_city(A,C)
| accept_team(A,L,C,N) )
& ! [A,C,N,L] :
( ( accept_number(A,N)
& accept_leader(A,L)
& accept_city(A,C) )
| ~ accept_team(A,L,C,N) ) ),
inference(miniscoping,[status(thm)],[f558]) ).
fof(f560,plain,
! [X0,X1,X2,X3] :
( accept_city(X0,X2)
| ~ accept_team(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f559]) ).
fof(f567,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(f568,plain,
! [A,M,P] :
( accept_population(A,P,M)
| ! [N] :
( ~ less(M,N)
| ~ accept_population(A,P,N) ) ),
inference(miniscoping,[status(thm)],[f567]) ).
fof(f569,plain,
! [X0,X1,X2,X3] :
( accept_population(X0,X1,X3)
| ~ less(X3,X2)
| ~ accept_population(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f568]) ).
fof(f573,plain,
! [A,L,C] :
( accept_leader(A,L)
| ~ any_agent_in_all_proposed_teams(A,L,C) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f574,plain,
! [A,L] :
( accept_leader(A,L)
| ! [C] : ~ any_agent_in_all_proposed_teams(A,L,C) ),
inference(miniscoping,[status(thm)],[f573]) ).
fof(f575,plain,
! [X0,X1,X2] :
( accept_leader(X0,X1)
| ~ any_agent_in_all_proposed_teams(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f574]) ).
fof(f576,plain,
! [A,L,C] :
( ~ accept_leader(A,L)
| ~ accept_city(A,C)
| ~ the_agent_not_in_any_proposed_teams(A,L,C) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f577,plain,
! [X0,X1,X2] :
( ~ accept_leader(X0,X1)
| ~ accept_city(X0,X2)
| ~ the_agent_not_in_any_proposed_teams(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f576]) ).
fof(f644,plain,
! [A] :
( ( ~ accept_city(A,towna)
| ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n24)
& accept_population(A,atheist,n75) ) )
& ( accept_city(A,towna)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,atheist,n75) ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f645,plain,
( ! [A] :
( ~ accept_city(A,towna)
| ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n24)
& accept_population(A,atheist,n75) ) )
& ! [A] :
( accept_city(A,towna)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,atheist,n75) ) ),
inference(miniscoping,[status(thm)],[f644]) ).
fof(f646,plain,
! [X0] :
( accept_city(X0,towna)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75) ),
inference(cnf_transformation,[status(thm)],[f645]) ).
fof(f652,plain,
! [A] :
( ( ~ accept_city(A,citya)
| ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n0)
& accept_population(A,christian,n25)
& accept_population(A,atheist,n75) ) )
& ( accept_city(A,citya)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,atheist,n75) ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f653,plain,
( ! [A] :
( ~ accept_city(A,citya)
| ( accept_population(A,other,n0)
& accept_population(A,native,n0)
& accept_population(A,muslim,n0)
& accept_population(A,christian,n25)
& accept_population(A,atheist,n75) ) )
& ! [A] :
( accept_city(A,citya)
| ~ accept_population(A,other,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,atheist,n75) ) ),
inference(miniscoping,[status(thm)],[f652]) ).
fof(f655,plain,
! [X0] :
( ~ accept_city(X0,citya)
| accept_population(X0,atheist,n75) ),
inference(cnf_transformation,[status(thm)],[f653]) ).
fof(f656,plain,
! [X0] :
( ~ accept_city(X0,citya)
| accept_population(X0,christian,n25) ),
inference(cnf_transformation,[status(thm)],[f653]) ).
fof(f658,plain,
! [X0] :
( ~ accept_city(X0,citya)
| accept_population(X0,native,n0) ),
inference(cnf_transformation,[status(thm)],[f653]) ).
fof(f659,plain,
! [X0] :
( ~ accept_city(X0,citya)
| accept_population(X0,other,n0) ),
inference(cnf_transformation,[status(thm)],[f653]) ).
fof(f668,plain,
! [A] :
( ( ~ accept_city(A,cityb)
| ( accept_population(A,other,n1)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n20)
& accept_population(A,atheist,n78) ) )
& ( accept_city(A,cityb)
| ~ accept_population(A,other,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,atheist,n78) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f669,plain,
( ! [A] :
( ~ accept_city(A,cityb)
| ( accept_population(A,other,n1)
& accept_population(A,native,n0)
& accept_population(A,muslim,n1)
& accept_population(A,christian,n20)
& accept_population(A,atheist,n78) ) )
& ! [A] :
( accept_city(A,cityb)
| ~ accept_population(A,other,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,atheist,n78) ) ),
inference(miniscoping,[status(thm)],[f668]) ).
fof(f673,plain,
! [X0] :
( ~ accept_city(X0,cityb)
| accept_population(X0,muslim,n1) ),
inference(cnf_transformation,[status(thm)],[f669]) ).
fof(f691,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f694,plain,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f695,plain,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f957,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f958,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f1190,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(cnf_transformation,[status(thm)],[f527]) ).
fof(f1202,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[status(thm)],[f539]) ).
fof(f1213,plain,
! [Ds,O,Db] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_non_zero(O)
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db)) ),
inference(pre_NNF_transformation,[status(thm)],[f546]) ).
fof(f1214,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdn(rdnn(X0),X2),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2)
| ~ rdn_positive_less(rdnn(X0),rdnn(X1)) ),
inference(cnf_transformation,[status(thm)],[f1213]) ).
fof(f1218,plain,
! [X] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f548]) ).
fof(f1219,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[status(thm)],[f1218]) ).
fof(f1223,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)],[f550]) ).
fof(f1224,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)],[f1223]) ).
fof(f1225,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)],[f1224]) ).
fof(f1245,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
inference(cnf_transformation,[status(thm)],[f557]) ).
fof(f1248,plain,
accept_city(muslimcountrybhumanitarianorganization,cityb),
inference(resolution,[status(thm)],[f560,f691]) ).
fof(f1249,plain,
accept_city(muslimcountrybhumanitarianorganization,citya),
inference(resolution,[status(thm)],[f560,f1245]) ).
fof(f1250,plain,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
inference(resolution,[status(thm)],[f1249,f659]) ).
fof(f1251,plain,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
inference(resolution,[status(thm)],[f1249,f658]) ).
fof(f1268,plain,
( ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,towna) ),
inference(resolution,[status(thm)],[f694,f577]) ).
fof(f1269,definition,
( sQ0_spl
<=> accept_city(muslimcountrybhumanitarianorganization,towna) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1272,definition,
( sQ1_spl
<=> accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1274,plain,
( sQ1_spl
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ),
inference(component_clause,[status(thm)],[f1272]) ).
fof(f1275,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1268,f1269,f1272]) ).
fof(f1276,plain,
accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization),
inference(resolution,[status(thm)],[f695,f575]) ).
fof(f1373,plain,
accept_population(muslimcountrybhumanitarianorganization,atheist,n75),
inference(resolution,[status(thm)],[f655,f1249]) ).
fof(f1374,plain,
( accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24) ),
inference(resolution,[status(thm)],[f1373,f646]) ).
fof(f1375,definition,
( sQ4_spl
<=> accept_population(muslimcountrybhumanitarianorganization,christian,n24) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
( sQ4_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24) ),
inference(component_clause,[status(thm)],[f1375]) ).
fof(f1378,definition,
( sQ5_spl
<=> accept_population(muslimcountrybhumanitarianorganization,muslim,n1) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1380,plain,
( sQ5_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1) ),
inference(component_clause,[status(thm)],[f1378]) ).
fof(f1381,definition,
( sQ6_spl
<=> accept_population(muslimcountrybhumanitarianorganization,native,n0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1383,plain,
( sQ6_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0) ),
inference(component_clause,[status(thm)],[f1381]) ).
fof(f1384,definition,
( sQ7_spl
<=> accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1386,plain,
( sQ7_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(component_clause,[status(thm)],[f1384]) ).
fof(f1387,plain,
( sQ0_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1374,f1375,f1378,f1381,f1384,f1269]) ).
fof(f1388,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1274,f1276]) ).
fof(f1389,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1388]) ).
fof(f1390,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1386,f1250]) ).
fof(f1391,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1390]) ).
fof(f1392,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1383,f1251]) ).
fof(f1393,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1392]) ).
fof(f1401,plain,
accept_population(muslimcountrybhumanitarianorganization,christian,n25),
inference(resolution,[status(thm)],[f656,f1249]) ).
fof(f1680,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)],[f1225,f569]) ).
fof(f1889,plain,
( sQ5_spl
| ~ accept_city(muslimcountrybhumanitarianorganization,cityb) ),
inference(resolution,[status(thm)],[f1380,f673]) ).
fof(f1895,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1889,f1248]) ).
fof(f1896,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1895]) ).
fof(f1898,plain,
! [X0,X1,X2] :
( sQ4_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,X1)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(n24,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1377,f1680]) ).
fof(f2227,plain,
! [X0,X1] :
( sQ4_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),X1)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f957,f1898]) ).
fof(f2242,plain,
! [X0,X1] :
( sQ4_spl
| ~ rdn_non_zero(rdnn(n2))
| ~ rdn_positive_less(rdnn(n4),rdnn(X1))
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n2)))) ),
inference(resolution,[status(thm)],[f2227,f1214]) ).
fof(f2244,definition,
! [X0,X1] :
( sQ89_spl
<=> ( ~ rdn_positive_less(rdnn(n4),rdnn(X1))
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2245,plain,
! [X0,X1] :
( ~ sQ89_spl
| ~ rdn_positive_less(rdnn(n4),rdnn(X1))
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(n2)))) ),
inference(component_clause,[status(thm)],[f2244]) ).
fof(f2247,definition,
( sQ90_spl
<=> rdn_non_zero(rdnn(n2)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2249,plain,
( sQ90_spl
| ~ rdn_non_zero(rdnn(n2)) ),
inference(component_clause,[status(thm)],[f2247]) ).
fof(f2250,plain,
( sQ4_spl
| ~ sQ90_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f2242,f2244,f2247,f1375]) ).
fof(f2251,plain,
( sQ90_spl
| ~ rdn_non_zero_digit(rdnn(n2)) ),
inference(resolution,[status(thm)],[f2249,f1219]) ).
fof(f2252,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2251,f1190]) ).
fof(f2253,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f2252]) ).
fof(f2518,plain,
! [X0] :
( ~ sQ89_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ),
inference(resolution,[status(thm)],[f2245,f1202]) ).
fof(f2769,plain,
( ~ sQ89_spl
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25) ),
inference(resolution,[status(thm)],[f2518,f958]) ).
fof(f2770,plain,
( ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2769,f1401]) ).
fof(f2771,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f2770]) ).
fof(f2772,plain,
$false,
inference(sat_refutation,[status(thm)],[f1275,f1387,f1389,f1391,f1393,f1896,f2250,f2253,f2771]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : AGT009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 12:46:22 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.41 % Drodi V4.1.1
% 2.23/0.75 % Refutation found
% 2.23/0.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.23/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.23/0.79 % Elapsed time: 0.390164 seconds
% 2.23/0.79 % CPU time: 2.639803 seconds
% 2.23/0.79 % Total memory used: 150.000 MB
% 2.23/0.79 % Net memory used: 148.369 MB
%------------------------------------------------------------------------------