%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : AGT026+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:15 AM UTC 2026
% Result : Theorem 36.52s 5.07s
% Output : CNFRefutation 36.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 41
% Syntax : Number of formulae : 161 ( 48 unt; 13 def)
% Number of atoms : 361 ( 5 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 389 ( 189 ~; 152 |; 24 &)
% ( 15 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 14 prp; 0-3 aty)
% Number of functors : 33 ( 33 usr; 29 con; 0-2 aty)
% Number of variables : 248 ( 244 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
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(f5,axiom,
! [A,L,C] :
( any_agent_in_all_proposed_teams(A,L,C)
=> accept_leader(A,L) ),
file('/export/starexec/sandbox2/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/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(f57,axiom,
the_agent_not_in_any_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f270,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f282,axiom,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f355,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f370,axiom,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f442,axiom,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f443,axiom,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f444,axiom,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f445,axiom,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f446,axiom,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f447,axiom,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f448,axiom,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f449,axiom,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f526,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f545,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(f547,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(f548,axiom,
! [X] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f549,axiom,
! [D,O] :
( rdn_non_zero(O)
=> rdn_non_zero(rdn(rdnn(D),O)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f551,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_neg(RDN_X)) )
=> less(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f553,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f556,conjecture,
? [X,Y] : ~ accept_population(X,Y,n100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f557,negated_conjecture,
~ ? [X,Y] : ~ accept_population(X,Y,n100),
inference(negated_conjecture,[status(cth)],[f556]) ).
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(f628,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(f629,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)],[f628]) ).
fof(f630,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)],[f629]) ).
fof(f720,plain,
the_agent_not_in_any_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f721,plain,
any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f933,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f936,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f945,plain,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f1018,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f1033,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f1105,plain,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f1106,plain,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f1107,plain,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
inference(cnf_transformation,[status(thm)],[f444]) ).
fof(f1108,plain,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f1109,plain,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
inference(cnf_transformation,[status(thm)],[f446]) ).
fof(f1110,plain,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f1111,plain,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
inference(cnf_transformation,[status(thm)],[f448]) ).
fof(f1112,plain,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
inference(cnf_transformation,[status(thm)],[f449]) ).
fof(f1189,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f1210,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)],[f545]) ).
fof(f1211,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)],[f1210]) ).
fof(f1212,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)],[f1211]) ).
fof(f1215,plain,
! [D,Db,Ob] :
( rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(pre_NNF_transformation,[status(thm)],[f547]) ).
fof(f1216,plain,
! [Ob] :
( ! [D,Db] : rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(miniscoping,[status(thm)],[f1215]) ).
fof(f1217,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X1),rdn(rdnn(X2),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1216]) ).
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(f1220,plain,
! [D,O] :
( rdn_non_zero(rdn(rdnn(D),O))
| ~ rdn_non_zero(O) ),
inference(pre_NNF_transformation,[status(thm)],[f549]) ).
fof(f1221,plain,
! [O] :
( ! [D] : rdn_non_zero(rdn(rdnn(D),O))
| ~ rdn_non_zero(O) ),
inference(miniscoping,[status(thm)],[f1220]) ).
fof(f1222,plain,
! [X0,X1] :
( rdn_non_zero(rdn(rdnn(X1),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1221]) ).
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(f1226,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_neg(RDN_X)) ),
inference(pre_NNF_transformation,[status(thm)],[f551]) ).
fof(f1227,plain,
! [X,Y] :
( less(X,Y)
| ! [RDN_Y] : ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ! [RDN_X] : ~ rdn_translate(X,rdn_neg(RDN_X)) ),
inference(miniscoping,[status(thm)],[f1226]) ).
fof(f1228,plain,
! [X0,X1,X2,X3] :
( less(X0,X2)
| ~ rdn_translate(X2,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_neg(X1)) ),
inference(cnf_transformation,[status(thm)],[f1227]) ).
fof(f1232,plain,
! [X,Y] :
( ( Y = X
| less(Y,X)
| less(X,Y) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f553]) ).
fof(f1233,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)],[f1232]) ).
fof(f1234,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1233]) ).
fof(f1245,plain,
! [X,Y] : accept_population(X,Y,n100),
inference(pre_NNF_transformation,[status(thm)],[f557]) ).
fof(f1246,plain,
! [X0,X1] : accept_population(X0,X1,n100),
inference(cnf_transformation,[status(thm)],[f1245]) ).
fof(f1292,plain,
! [X0,X1,X2,X3] :
( ~ any_agent_in_all_proposed_teams(X0,X1,X3)
| ~ accept_city(X0,X2)
| ~ the_agent_not_in_any_proposed_teams(X0,X1,X2) ),
inference(resolution,[status(thm)],[f577,f575]) ).
fof(f1496,definition,
! [X0] :
( sQ0_spl
<=> ~ any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1497,plain,
! [X0] :
( ~ sQ0_spl
| ~ any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,X0) ),
inference(component_clause,[status(thm)],[f1496]) ).
fof(f1514,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f721,f1497]) ).
fof(f1515,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1514]) ).
fof(f1578,plain,
! [X0,X1] :
( less(nn52,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1112]) ).
fof(f1579,plain,
! [X0,X1] :
( less(nn51,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1111]) ).
fof(f1580,plain,
! [X0,X1] :
( less(nn50,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1110]) ).
fof(f1581,plain,
! [X0,X1] :
( less(nn49,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1109]) ).
fof(f1582,plain,
! [X0,X1] :
( less(nn48,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1108]) ).
fof(f1583,plain,
! [X0,X1] :
( less(nn47,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1107]) ).
fof(f1584,plain,
! [X0,X1] :
( less(nn46,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1106]) ).
fof(f1585,plain,
! [X0,X1] :
( less(nn45,X0)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1228,f1105]) ).
fof(f1830,plain,
! [X0,X1] :
( ~ less(X0,nn52)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1578,f1234]) ).
fof(f1834,plain,
! [X0,X1] :
( ~ less(X0,nn51)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1579,f1234]) ).
fof(f1838,plain,
! [X0,X1] :
( ~ less(X0,nn50)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1580,f1234]) ).
fof(f1843,plain,
! [X0,X1] :
( ~ less(X0,nn49)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1581,f1234]) ).
fof(f1847,plain,
! [X0,X1] :
( ~ less(X0,nn48)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1582,f1234]) ).
fof(f1851,plain,
! [X0,X1] :
( ~ less(X0,nn47)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1583,f1234]) ).
fof(f1855,plain,
! [X0,X1] :
( ~ less(X0,nn46)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1584,f1234]) ).
fof(f1859,plain,
! [X0,X1] :
( ~ less(X0,nn45)
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1585,f1234]) ).
fof(f2346,definition,
! [X0] :
( sQ53_spl
<=> ~ rdn_translate(nn45,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f2350,definition,
! [X0] :
( sQ54_spl
<=> ~ rdn_translate(nn46,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2354,definition,
! [X0] :
( sQ55_spl
<=> ~ rdn_translate(nn47,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f2358,definition,
! [X0] :
( sQ56_spl
<=> ~ rdn_translate(nn48,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2362,definition,
! [X0] :
( sQ57_spl
<=> ~ rdn_translate(nn49,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2366,definition,
! [X0] :
( sQ58_spl
<=> ~ rdn_translate(nn50,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2370,definition,
! [X0] :
( sQ59_spl
<=> ~ rdn_translate(nn51,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f2374,definition,
! [X0] :
( sQ60_spl
<=> ~ rdn_translate(nn52,rdn_pos(X0)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2700,plain,
! [X0,X1] :
( less(X0,n100)
| ~ rdn_positive_less(X1,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f1225,f1033]) ).
fof(f5871,plain,
! [X0,X1,X2] :
( ~ rdn_positive_less(X2,rdn(rdnn(n0),rdnn(n1)))
| less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f2700,f1212]) ).
fof(f5872,plain,
! [X0,X1] :
( ~ rdn_non_zero(rdn(rdnn(n0),rdnn(n1)))
| less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1))) ),
inference(resolution,[status(thm)],[f2700,f1217]) ).
fof(f5873,definition,
! [X0,X1] :
( sQ107_spl
<=> ( less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f5874,plain,
! [X0,X1] :
( ~ sQ107_spl
| less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1))) ),
inference(component_clause,[status(thm)],[f5873]) ).
fof(f5876,definition,
( sQ108_spl
<=> rdn_non_zero(rdn(rdnn(n0),rdnn(n1))) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f5878,plain,
( sQ108_spl
| ~ rdn_non_zero(rdn(rdnn(n0),rdnn(n1))) ),
inference(component_clause,[status(thm)],[f5876]) ).
fof(f5879,plain,
( ~ sQ108_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f5872,f5873,f5876]) ).
fof(f5881,plain,
! [X0,X1,X2,X3] :
( ~ sQ107_spl
| accept_population(X2,X3,X0)
| ~ accept_population(X2,X3,n100)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1))) ),
inference(resolution,[status(thm)],[f5874,f569]) ).
fof(f5884,plain,
! [X0,X1,X2,X3] :
( ~ sQ107_spl
| accept_population(X2,X3,X0)
| ~ rdn_translate(X0,rdn_pos(rdnn(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f5881,f1246]) ).
fof(f5891,plain,
! [X0,X1] :
( ~ sQ107_spl
| accept_population(X0,X1,n3) ),
inference(resolution,[status(thm)],[f5884,f936]) ).
fof(f5894,plain,
! [X0,X1] :
( ~ sQ107_spl
| accept_population(X0,X1,n0) ),
inference(resolution,[status(thm)],[f5884,f933]) ).
fof(f5924,plain,
! [X0] :
( ~ sQ107_spl
| accept_city(X0,coastvillage)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,atheist,n12) ),
inference(backward_subsumption_resolution,[status(thm)],[f630,f5891]) ).
fof(f5996,plain,
! [X0] :
( ~ sQ107_spl
| accept_city(X0,coastvillage)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,atheist,n12) ),
inference(forward_subsumption_resolution,[status(thm)],[f5924,f5894]) ).
fof(f8040,plain,
( sQ108_spl
| ~ rdn_non_zero(rdnn(n1)) ),
inference(resolution,[status(thm)],[f5878,f1222]) ).
fof(f8041,plain,
( sQ108_spl
| ~ rdn_non_zero_digit(rdnn(n1)) ),
inference(resolution,[status(thm)],[f8040,f1219]) ).
fof(f8042,plain,
( sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8041,f1189]) ).
fof(f8043,plain,
sQ108_spl,
inference(contradiction_clause,[status(thm)],[f8042]) ).
fof(f8078,plain,
! [X0] :
( ~ sQ107_spl
| accept_city(X0,coastvillage)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,atheist,n12) ),
inference(backward_subsumption_resolution,[status(thm)],[f5996,f5894]) ).
fof(f11718,plain,
! [X0,X1,X2] :
( ~ rdn_non_zero(rdnn(n1))
| less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(X2)))) ),
inference(resolution,[status(thm)],[f5871,f1217]) ).
fof(f11719,definition,
! [X0,X1,X2] :
( sQ118_spl
<=> ( less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(X2)))) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f11720,plain,
! [X0,X1,X2] :
( ~ sQ118_spl
| less(X0,n100)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(X2)))) ),
inference(component_clause,[status(thm)],[f11719]) ).
fof(f11722,definition,
( sQ119_spl
<=> rdn_non_zero(rdnn(n1)) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f11724,plain,
( sQ119_spl
| ~ rdn_non_zero(rdnn(n1)) ),
inference(component_clause,[status(thm)],[f11722]) ).
fof(f11725,plain,
( ~ sQ119_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f11718,f11719,f11722]) ).
fof(f13689,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ118_spl
| accept_population(X3,X4,X0)
| ~ accept_population(X3,X4,n100)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(X2)))) ),
inference(resolution,[status(thm)],[f11720,f569]) ).
fof(f13696,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ118_spl
| accept_population(X3,X4,X0)
| ~ rdn_translate(X0,rdn_pos(rdn(rdnn(X1),rdnn(X2)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f13689,f1246]) ).
fof(f13697,plain,
( sQ119_spl
| ~ rdn_non_zero_digit(rdnn(n1)) ),
inference(resolution,[status(thm)],[f11724,f1219]) ).
fof(f13698,plain,
( sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13697,f1189]) ).
fof(f13699,plain,
sQ119_spl,
inference(contradiction_clause,[status(thm)],[f13698]) ).
fof(f13763,plain,
! [X0,X1] :
( ~ rdn_translate(nn52,rdn_pos(X1))
| ~ rdn_translate(nn52,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1830,f1578]) ).
fof(f13876,plain,
sQ60_spl,
inference(split_clause,[status(thm)],[f13763,f2374]) ).
fof(f13986,plain,
! [X0,X1] :
( ~ rdn_translate(nn51,rdn_pos(X1))
| ~ rdn_translate(nn51,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1834,f1579]) ).
fof(f14099,plain,
sQ59_spl,
inference(split_clause,[status(thm)],[f13986,f2370]) ).
fof(f14209,plain,
! [X0,X1] :
( ~ rdn_translate(nn50,rdn_pos(X1))
| ~ rdn_translate(nn50,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1838,f1580]) ).
fof(f14322,plain,
sQ58_spl,
inference(split_clause,[status(thm)],[f14209,f2366]) ).
fof(f14540,plain,
! [X0,X1] :
( ~ rdn_translate(nn49,rdn_pos(X1))
| ~ rdn_translate(nn49,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1843,f1581]) ).
fof(f14654,plain,
sQ57_spl,
inference(split_clause,[status(thm)],[f14540,f2362]) ).
fof(f14765,plain,
! [X0,X1] :
( ~ rdn_translate(nn48,rdn_pos(X1))
| ~ rdn_translate(nn48,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1847,f1582]) ).
fof(f14879,plain,
sQ56_spl,
inference(split_clause,[status(thm)],[f14765,f2358]) ).
fof(f14990,plain,
! [X0,X1] :
( ~ rdn_translate(nn47,rdn_pos(X1))
| ~ rdn_translate(nn47,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1851,f1583]) ).
fof(f15104,plain,
sQ55_spl,
inference(split_clause,[status(thm)],[f14990,f2354]) ).
fof(f15215,plain,
! [X0,X1] :
( ~ rdn_translate(nn46,rdn_pos(X1))
| ~ rdn_translate(nn46,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1855,f1584]) ).
fof(f15329,plain,
sQ54_spl,
inference(split_clause,[status(thm)],[f15215,f2350]) ).
fof(f15440,plain,
! [X0,X1] :
( ~ rdn_translate(nn45,rdn_pos(X1))
| ~ rdn_translate(nn45,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f1859,f1585]) ).
fof(f15554,plain,
sQ53_spl,
inference(split_clause,[status(thm)],[f15440,f2346]) ).
fof(f15749,plain,
! [X0,X1] :
( ~ sQ118_spl
| accept_population(X0,X1,n85) ),
inference(resolution,[status(thm)],[f13696,f1018]) ).
fof(f15822,plain,
! [X0,X1] :
( ~ sQ118_spl
| accept_population(X0,X1,n12) ),
inference(resolution,[status(thm)],[f13696,f945]) ).
fof(f15825,plain,
! [X0] :
( ~ sQ107_spl
| ~ sQ118_spl
| accept_city(X0,coastvillage)
| ~ accept_population(X0,atheist,n12) ),
inference(backward_subsumption_resolution,[status(thm)],[f8078,f15749]) ).
fof(f15847,plain,
! [X0] :
( ~ sQ107_spl
| ~ sQ118_spl
| accept_city(X0,coastvillage) ),
inference(forward_subsumption_resolution,[status(thm)],[f15825,f15822]) ).
fof(f15882,plain,
! [X0,X1,X2] :
( ~ sQ107_spl
| ~ sQ118_spl
| ~ any_agent_in_all_proposed_teams(X0,X1,X2)
| ~ the_agent_not_in_any_proposed_teams(X0,X1,coastvillage) ),
inference(resolution,[status(thm)],[f15847,f1292]) ).
fof(f15927,plain,
! [X0] :
( ~ sQ107_spl
| ~ sQ118_spl
| ~ any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,X0) ),
inference(resolution,[status(thm)],[f15882,f720]) ).
fof(f15928,plain,
( ~ sQ107_spl
| ~ sQ118_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f15927,f1496,f11719,f5873]) ).
fof(f15929,plain,
$false,
inference(sat_refutation,[status(thm)],[f1515,f5879,f8043,f11725,f13699,f13876,f14099,f14322,f14654,f14879,f15104,f15329,f15554,f15928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT026+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 12:51:17 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 36.52/5.07 % Refutation found
% 36.52/5.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 36.52/5.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.12/5.14 % Elapsed time: 4.758809 seconds
% 2.12/5.14 % CPU time: 37.351489 seconds
% 2.12/5.14 % Total memory used: 269.552 MB
% 2.12/5.14 % Net memory used: 259.806 MB
%------------------------------------------------------------------------------