%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : AGT009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:18 AM UTC 2026
% Result : Theorem 10.32s 1.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : AGT009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n002.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 12:51:03 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 10.32/1.73 % Refutation found
% 10.32/1.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.32/1.73 % SZS output start CNFRefutation for theBenchmark
% 10.32/1.73 fof(f1,axiom,(
% 10.32/1.73 (! [A,C,N,L] :( accept_team(A,L,C,N)<=> ( accept_city(A,C)& accept_leader(A,L)& accept_number(A,N) ) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f3,axiom,(
% 10.32/1.73 (! [A,N,M,P] :( ( accept_population(A,P,N)& less(M,N) )=> accept_population(A,P,M) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f5,axiom,(
% 10.32/1.73 (! [A,L,C] :( any_agent_in_all_proposed_teams(A,L,C)=> accept_leader(A,L) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f6,axiom,(
% 10.32/1.73 (! [A,L,C] :( the_agent_not_in_any_proposed_teams(A,L,C)=> ~ ( accept_city(A,C)& accept_leader(A,L) ) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f16,axiom,(
% 10.32/1.73 (! [A] :( ( accept_population(A,atheist,n75)& accept_population(A,christian,n24)& accept_population(A,muslim,n1)& accept_population(A,native,n0)& accept_population(A,other,n0) )<=> accept_city(A,towna) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f17,axiom,(
% 10.32/1.73 (! [A] :( ( accept_population(A,atheist,n75)& accept_population(A,christian,n25)& accept_population(A,muslim,n0)& accept_population(A,native,n0)& accept_population(A,other,n0) )<=> accept_city(A,citya) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f19,axiom,(
% 10.32/1.73 (! [A] :( ( accept_population(A,atheist,n78)& accept_population(A,christian,n20)& accept_population(A,muslim,n1)& accept_population(A,native,n0)& accept_population(A,other,n1) )<=> accept_city(A,cityb) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f28,axiom,(
% 10.32/1.73 accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f31,axiom,(
% 10.32/1.73 the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f32,axiom,(
% 10.32/1.73 any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f294,axiom,(
% 10.32/1.73 rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f295,axiom,(
% 10.32/1.73 rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f527,axiom,(
% 10.32/1.73 rdn_non_zero_digit(rdnn(n2)) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f539,axiom,(
% 10.32/1.73 rdn_positive_less(rdnn(n4),rdnn(n5)) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f546,axiom,(
% 10.32/1.73 (! [Ds,O,Db] :( ( rdn_positive_less(rdnn(Ds),rdnn(Db))& rdn_non_zero(O) )=> rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f548,axiom,(
% 10.32/1.73 (! [X] :( rdn_non_zero_digit(rdnn(X))=> rdn_non_zero(rdnn(X)) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f550,axiom,(
% 10.32/1.73 (! [X,Y,RDN_X,RDN_Y] :( ( rdn_translate(X,rdn_pos(RDN_X))& rdn_translate(Y,rdn_pos(RDN_Y))& rdn_positive_less(RDN_X,RDN_Y) )=> less(X,Y) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f553,axiom,(
% 10.32/1.73 (! [X,Y] :( less(X,Y)<=> ( ~ less(Y,X)& Y != X ) ) )),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f556,conjecture,(
% 10.32/1.73 ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) ),
% 10.32/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.73 fof(f557,negated_conjecture,(
% 10.32/1.73 ~(~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) )),
% 10.32/1.73 inference(negated_conjecture,[status(cth)],[f556])).
% 10.32/1.73 fof(f558,plain,(
% 10.32/1.73 ![A,C,N,L]: ((~accept_team(A,L,C,N)|((accept_city(A,C)&accept_leader(A,L))&accept_number(A,N)))&(accept_team(A,L,C,N)|((~accept_city(A,C)|~accept_leader(A,L))|~accept_number(A,N))))),
% 10.32/1.73 inference(NNF_transformation,[status(thm)],[f1])).
% 10.32/1.73 fof(f559,plain,(
% 10.32/1.73 (![A,C,N,L]: (~accept_team(A,L,C,N)|((accept_city(A,C)&accept_leader(A,L))&accept_number(A,N))))&(![A,C,N,L]: (accept_team(A,L,C,N)|((~accept_city(A,C)|~accept_leader(A,L))|~accept_number(A,N))))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f558])).
% 10.32/1.73 fof(f560,plain,(
% 10.32/1.73 ![X0,X1,X2,X3]: (~accept_team(X0,X1,X2,X3)|accept_city(X0,X2))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f559])).
% 10.32/1.73 fof(f567,plain,(
% 10.32/1.73 ![A,N,M,P]: ((~accept_population(A,P,N)|~less(M,N))|accept_population(A,P,M))),
% 10.32/1.73 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 10.32/1.73 fof(f568,plain,(
% 10.32/1.73 ![A,M,P]: ((![N]: (~accept_population(A,P,N)|~less(M,N)))|accept_population(A,P,M))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f567])).
% 10.32/1.73 fof(f569,plain,(
% 10.32/1.73 ![X0,X1,X2,X3]: (~accept_population(X0,X1,X2)|~less(X3,X2)|accept_population(X0,X1,X3))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f568])).
% 10.32/1.73 fof(f573,plain,(
% 10.32/1.73 ![A,L,C]: (~any_agent_in_all_proposed_teams(A,L,C)|accept_leader(A,L))),
% 10.32/1.73 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 10.32/1.73 fof(f574,plain,(
% 10.32/1.73 ![A,L]: ((![C]: ~any_agent_in_all_proposed_teams(A,L,C))|accept_leader(A,L))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f573])).
% 10.32/1.73 fof(f575,plain,(
% 10.32/1.73 ![X0,X1,X2]: (~any_agent_in_all_proposed_teams(X0,X1,X2)|accept_leader(X0,X1))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f574])).
% 10.32/1.73 fof(f576,plain,(
% 10.32/1.73 ![A,L,C]: (~the_agent_not_in_any_proposed_teams(A,L,C)|(~accept_city(A,C)|~accept_leader(A,L)))),
% 10.32/1.73 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 10.32/1.73 fof(f577,plain,(
% 10.32/1.73 ![X0,X1,X2]: (~the_agent_not_in_any_proposed_teams(X0,X1,X2)|~accept_city(X0,X2)|~accept_leader(X0,X1))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f576])).
% 10.32/1.73 fof(f644,plain,(
% 10.32/1.73 ![A]: ((((((~accept_population(A,atheist,n75)|~accept_population(A,christian,n24))|~accept_population(A,muslim,n1))|~accept_population(A,native,n0))|~accept_population(A,other,n0))|accept_city(A,towna))&(((((accept_population(A,atheist,n75)&accept_population(A,christian,n24))&accept_population(A,muslim,n1))&accept_population(A,native,n0))&accept_population(A,other,n0))|~accept_city(A,towna)))),
% 10.32/1.73 inference(NNF_transformation,[status(thm)],[f16])).
% 10.32/1.73 fof(f645,plain,(
% 10.32/1.73 (![A]: (((((~accept_population(A,atheist,n75)|~accept_population(A,christian,n24))|~accept_population(A,muslim,n1))|~accept_population(A,native,n0))|~accept_population(A,other,n0))|accept_city(A,towna)))&(![A]: (((((accept_population(A,atheist,n75)&accept_population(A,christian,n24))&accept_population(A,muslim,n1))&accept_population(A,native,n0))&accept_population(A,other,n0))|~accept_city(A,towna)))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f644])).
% 10.32/1.73 fof(f646,plain,(
% 10.32/1.73 ![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))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f645])).
% 10.32/1.73 fof(f652,plain,(
% 10.32/1.73 ![A]: ((((((~accept_population(A,atheist,n75)|~accept_population(A,christian,n25))|~accept_population(A,muslim,n0))|~accept_population(A,native,n0))|~accept_population(A,other,n0))|accept_city(A,citya))&(((((accept_population(A,atheist,n75)&accept_population(A,christian,n25))&accept_population(A,muslim,n0))&accept_population(A,native,n0))&accept_population(A,other,n0))|~accept_city(A,citya)))),
% 10.32/1.73 inference(NNF_transformation,[status(thm)],[f17])).
% 10.32/1.73 fof(f653,plain,(
% 10.32/1.73 (![A]: (((((~accept_population(A,atheist,n75)|~accept_population(A,christian,n25))|~accept_population(A,muslim,n0))|~accept_population(A,native,n0))|~accept_population(A,other,n0))|accept_city(A,citya)))&(![A]: (((((accept_population(A,atheist,n75)&accept_population(A,christian,n25))&accept_population(A,muslim,n0))&accept_population(A,native,n0))&accept_population(A,other,n0))|~accept_city(A,citya)))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f652])).
% 10.32/1.73 fof(f655,plain,(
% 10.32/1.73 ![X0]: (accept_population(X0,atheist,n75)|~accept_city(X0,citya))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f653])).
% 10.32/1.73 fof(f656,plain,(
% 10.32/1.73 ![X0]: (accept_population(X0,christian,n25)|~accept_city(X0,citya))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f653])).
% 10.32/1.73 fof(f658,plain,(
% 10.32/1.73 ![X0]: (accept_population(X0,native,n0)|~accept_city(X0,citya))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f653])).
% 10.32/1.73 fof(f659,plain,(
% 10.32/1.73 ![X0]: (accept_population(X0,other,n0)|~accept_city(X0,citya))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f653])).
% 10.32/1.73 fof(f668,plain,(
% 10.32/1.73 ![A]: ((((((~accept_population(A,atheist,n78)|~accept_population(A,christian,n20))|~accept_population(A,muslim,n1))|~accept_population(A,native,n0))|~accept_population(A,other,n1))|accept_city(A,cityb))&(((((accept_population(A,atheist,n78)&accept_population(A,christian,n20))&accept_population(A,muslim,n1))&accept_population(A,native,n0))&accept_population(A,other,n1))|~accept_city(A,cityb)))),
% 10.32/1.73 inference(NNF_transformation,[status(thm)],[f19])).
% 10.32/1.73 fof(f669,plain,(
% 10.32/1.73 (![A]: (((((~accept_population(A,atheist,n78)|~accept_population(A,christian,n20))|~accept_population(A,muslim,n1))|~accept_population(A,native,n0))|~accept_population(A,other,n1))|accept_city(A,cityb)))&(![A]: (((((accept_population(A,atheist,n78)&accept_population(A,christian,n20))&accept_population(A,muslim,n1))&accept_population(A,native,n0))&accept_population(A,other,n1))|~accept_city(A,cityb)))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f668])).
% 10.32/1.73 fof(f673,plain,(
% 10.32/1.73 ![X0]: (accept_population(X0,muslim,n1)|~accept_city(X0,cityb))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f669])).
% 10.32/1.73 fof(f691,plain,(
% 10.32/1.73 accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4)),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f28])).
% 10.32/1.73 fof(f694,plain,(
% 10.32/1.73 the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f31])).
% 10.32/1.73 fof(f695,plain,(
% 10.32/1.73 any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f32])).
% 10.32/1.73 fof(f957,plain,(
% 10.32/1.73 rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f294])).
% 10.32/1.73 fof(f958,plain,(
% 10.32/1.73 rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2))))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f295])).
% 10.32/1.73 fof(f1190,plain,(
% 10.32/1.73 rdn_non_zero_digit(rdnn(n2))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f527])).
% 10.32/1.73 fof(f1202,plain,(
% 10.32/1.73 rdn_positive_less(rdnn(n4),rdnn(n5))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f539])).
% 10.32/1.73 fof(f1213,plain,(
% 10.32/1.73 ![Ds,O,Db]: ((~rdn_positive_less(rdnn(Ds),rdnn(Db))|~rdn_non_zero(O))|rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)))),
% 10.32/1.73 inference(pre_NNF_transformation,[status(thm)],[f546])).
% 10.32/1.73 fof(f1214,plain,(
% 10.32/1.73 ![X0,X1,X2]: (~rdn_positive_less(rdnn(X0),rdnn(X1))|~rdn_non_zero(X2)|rdn_positive_less(rdn(rdnn(X0),X2),rdn(rdnn(X1),X2)))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f1213])).
% 10.32/1.73 fof(f1218,plain,(
% 10.32/1.73 ![X]: (~rdn_non_zero_digit(rdnn(X))|rdn_non_zero(rdnn(X)))),
% 10.32/1.73 inference(pre_NNF_transformation,[status(thm)],[f548])).
% 10.32/1.73 fof(f1219,plain,(
% 10.32/1.73 ![X0]: (~rdn_non_zero_digit(rdnn(X0))|rdn_non_zero(rdnn(X0)))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f1218])).
% 10.32/1.73 fof(f1223,plain,(
% 10.32/1.73 ![X,Y,RDN_X,RDN_Y]: (((~rdn_translate(X,rdn_pos(RDN_X))|~rdn_translate(Y,rdn_pos(RDN_Y)))|~rdn_positive_less(RDN_X,RDN_Y))|less(X,Y))),
% 10.32/1.73 inference(pre_NNF_transformation,[status(thm)],[f550])).
% 10.32/1.73 fof(f1224,plain,(
% 10.32/1.73 ![X,Y]: ((![RDN_X,RDN_Y]: ((~rdn_translate(X,rdn_pos(RDN_X))|~rdn_translate(Y,rdn_pos(RDN_Y)))|~rdn_positive_less(RDN_X,RDN_Y)))|less(X,Y))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f1223])).
% 10.32/1.73 fof(f1225,plain,(
% 10.32/1.73 ![X0,X1,X2,X3]: (~rdn_translate(X0,rdn_pos(X1))|~rdn_translate(X2,rdn_pos(X3))|~rdn_positive_less(X1,X3)|less(X0,X2))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f1224])).
% 10.32/1.73 fof(f1232,plain,(
% 10.32/1.73 ![X,Y]: ((~less(X,Y)|(~less(Y,X)&~Y=X))&(less(X,Y)|(less(Y,X)|Y=X)))),
% 10.32/1.73 inference(NNF_transformation,[status(thm)],[f553])).
% 10.32/1.73 fof(f1233,plain,(
% 10.32/1.73 (![X,Y]: (~less(X,Y)|(~less(Y,X)&~Y=X)))&(![X,Y]: (less(X,Y)|(less(Y,X)|Y=X)))),
% 10.32/1.73 inference(miniscoping,[status(thm)],[f1232])).
% 10.32/1.73 fof(f1234,plain,(
% 10.32/1.73 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f1233])).
% 10.32/1.73 fof(f1236,plain,(
% 10.32/1.73 ![X0,X1]: (less(X0,X1)|less(X1,X0)|X1=X0)),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f1233])).
% 10.32/1.73 fof(f1245,plain,(
% 10.32/1.73 accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2)),
% 10.32/1.73 inference(cnf_transformation,[status(thm)],[f557])).
% 10.32/1.73 fof(f1253,plain,(
% 10.32/1.73 accept_city(muslimcountrybhumanitarianorganization,cityb)),
% 10.32/1.73 inference(resolution,[status(thm)],[f560,f691])).
% 10.32/1.73 fof(f1254,plain,(
% 10.32/1.73 accept_city(muslimcountrybhumanitarianorganization,citya)),
% 10.32/1.73 inference(resolution,[status(thm)],[f560,f1245])).
% 10.32/1.73 fof(f1269,plain,(
% 10.32/1.73 accept_population(muslimcountrybhumanitarianorganization,other,n0)),
% 10.32/1.73 inference(resolution,[status(thm)],[f1254,f659])).
% 10.32/1.73 fof(f1270,plain,(
% 10.32/1.73 accept_population(muslimcountrybhumanitarianorganization,native,n0)),
% 10.32/1.73 inference(resolution,[status(thm)],[f1254,f658])).
% 10.32/1.73 fof(f1357,plain,(
% 10.32/1.73 ~accept_city(muslimcountrybhumanitarianorganization,towna)|~accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)),
% 10.32/1.73 inference(resolution,[status(thm)],[f694,f577])).
% 10.32/1.73 fof(f1358,plain,(
% 10.32/1.73 accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)),
% 10.32/1.73 inference(resolution,[status(thm)],[f695,f575])).
% 10.32/1.73 fof(f1359,plain,(
% 10.32/1.73 ~accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.73 inference(backward_subsumption_resolution,[status(thm)],[f1357,f1358])).
% 10.32/1.73 fof(f1660,plain,(
% 10.32/1.73 accept_population(muslimcountrybhumanitarianorganization,atheist,n75)),
% 10.32/1.73 inference(resolution,[status(thm)],[f655,f1254])).
% 10.32/1.73 fof(f1661,plain,(
% 10.32/1.73 ~accept_population(muslimcountrybhumanitarianorganization,christian,n24)|~accept_population(muslimcountrybhumanitarianorganization,muslim,n1)|~accept_population(muslimcountrybhumanitarianorganization,native,n0)|~accept_population(muslimcountrybhumanitarianorganization,other,n0)|accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.73 inference(resolution,[status(thm)],[f1660,f646])).
% 10.32/1.73 fof(f1662,plain,(
% 10.32/1.73 ~accept_population(muslimcountrybhumanitarianorganization,christian,n24)|~accept_population(muslimcountrybhumanitarianorganization,muslim,n1)|~accept_population(muslimcountrybhumanitarianorganization,other,n0)|accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.74 inference(forward_subsumption_resolution,[status(thm)],[f1661,f1270])).
% 10.32/1.74 fof(f1674,plain,(
% 10.32/1.74 accept_population(muslimcountrybhumanitarianorganization,christian,n25)),
% 10.32/1.74 inference(resolution,[status(thm)],[f656,f1254])).
% 10.32/1.74 fof(f1860,plain,(
% 10.32/1.74 rdn_non_zero(rdnn(n2))),
% 10.32/1.74 inference(resolution,[status(thm)],[f1219,f1190])).
% 10.32/1.74 fof(f1867,plain,(
% 10.32/1.74 ![X0,X1,X2,X3]: (less(X0,X1)|X0=X1|~accept_population(X2,X3,X0)|accept_population(X2,X3,X1))),
% 10.32/1.74 inference(resolution,[status(thm)],[f1236,f569])).
% 10.32/1.74 fof(f2013,plain,(
% 10.32/1.74 ![X0]: (less(n25,X0)|n25=X0|accept_population(muslimcountrybhumanitarianorganization,christian,X0))),
% 10.32/1.74 inference(resolution,[status(thm)],[f1867,f1674])).
% 10.32/1.74 fof(f2038,plain,(
% 10.32/1.74 less(n25,n24)|n25=n24|~accept_population(muslimcountrybhumanitarianorganization,muslim,n1)|~accept_population(muslimcountrybhumanitarianorganization,other,n0)|accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.74 inference(resolution,[status(thm)],[f2013,f1662])).
% 10.32/1.74 fof(f2041,plain,(
% 10.32/1.74 less(n25,n24)|n25=n24|~accept_population(muslimcountrybhumanitarianorganization,muslim,n1)|accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.74 inference(forward_subsumption_resolution,[status(thm)],[f2038,f1269])).
% 10.32/1.74 fof(f2138,plain,(
% 10.32/1.74 less(n25,n24)|n25=n24|accept_city(muslimcountrybhumanitarianorganization,towna)|~accept_city(muslimcountrybhumanitarianorganization,cityb)),
% 10.32/1.74 inference(resolution,[status(thm)],[f2041,f673])).
% 10.32/1.74 fof(f2142,plain,(
% 10.32/1.74 less(n25,n24)|n25=n24|~accept_city(muslimcountrybhumanitarianorganization,cityb)),
% 10.32/1.74 inference(forward_subsumption_resolution,[status(thm)],[f2138,f1359])).
% 10.32/1.74 fof(f2143,plain,(
% 10.32/1.74 less(n25,n24)|n25=n24),
% 10.32/1.74 inference(resolution,[status(thm)],[f2142,f1253])).
% 10.32/1.74 fof(f2145,plain,(
% 10.32/1.74 n25=n24|~less(n24,n25)),
% 10.32/1.74 inference(resolution,[status(thm)],[f2143,f1234])).
% 10.32/1.74 fof(f2300,plain,(
% 10.32/1.74 ![X0,X1]: (~rdn_translate(n24,rdn_pos(X0))|~rdn_translate(n25,rdn_pos(X1))|~rdn_positive_less(X0,X1)|n25=n24)),
% 10.32/1.75 inference(resolution,[status(thm)],[f1225,f2145])).
% 10.32/1.75 fof(f3717,plain,(
% 10.32/1.75 ![X0]: (~rdn_translate(n25,rdn_pos(X0))|~rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),X0)|n25=n24)),
% 10.32/1.75 inference(resolution,[status(thm)],[f2300,f957])).
% 10.32/1.75 fof(f3797,plain,(
% 10.32/1.75 ~rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))|n25=n24),
% 10.32/1.75 inference(resolution,[status(thm)],[f3717,f958])).
% 10.32/1.75 fof(f3798,plain,(
% 10.32/1.75 n25=n24|~rdn_positive_less(rdnn(n4),rdnn(n5))|~rdn_non_zero(rdnn(n2))),
% 10.32/1.75 inference(resolution,[status(thm)],[f3797,f1214])).
% 10.32/1.75 fof(f3800,plain,(
% 10.32/1.75 n25=n24|~rdn_non_zero(rdnn(n2))),
% 10.32/1.75 inference(forward_subsumption_resolution,[status(thm)],[f3798,f1202])).
% 10.32/1.75 fof(f3801,plain,(
% 10.32/1.75 n25=n24),
% 10.32/1.75 inference(resolution,[status(thm)],[f3800,f1860])).
% 10.32/1.75 fof(f3824,plain,(
% 10.32/1.75 ~accept_population(muslimcountrybhumanitarianorganization,christian,n25)|~accept_population(muslimcountrybhumanitarianorganization,muslim,n1)|~accept_population(muslimcountrybhumanitarianorganization,other,n0)|accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.75 inference(backward_demodulation,[status(thm)],[f3801,f1662])).
% 10.32/1.75 fof(f3879,plain,(
% 10.32/1.75 ~accept_population(muslimcountrybhumanitarianorganization,muslim,n1)|~accept_population(muslimcountrybhumanitarianorganization,other,n0)|accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.75 inference(forward_subsumption_resolution,[status(thm)],[f3824,f1674])).
% 10.32/1.75 fof(f3919,plain,(
% 10.32/1.75 ~accept_population(muslimcountrybhumanitarianorganization,other,n0)|accept_city(muslimcountrybhumanitarianorganization,towna)|~accept_city(muslimcountrybhumanitarianorganization,cityb)),
% 10.32/1.75 inference(resolution,[status(thm)],[f3879,f673])).
% 10.32/1.75 fof(f3929,plain,(
% 10.32/1.75 accept_city(muslimcountrybhumanitarianorganization,towna)|~accept_city(muslimcountrybhumanitarianorganization,cityb)),
% 10.32/1.75 inference(forward_subsumption_resolution,[status(thm)],[f3919,f1269])).
% 10.32/1.75 fof(f3931,plain,(
% 10.32/1.75 accept_city(muslimcountrybhumanitarianorganization,towna)),
% 10.32/1.75 inference(resolution,[status(thm)],[f3929,f1253])).
% 10.32/1.75 fof(f3932,plain,(
% 10.32/1.75 $false),
% 10.32/1.75 inference(forward_subsumption_resolution,[status(thm)],[f3931,f1359])).
% 10.32/1.75 % SZS output end CNFRefutation for theBenchmark.p
% 10.32/1.78 % Elapsed time: 1.422791 seconds
% 10.32/1.78 % CPU time: 10.841705 seconds
% 10.32/1.78 % Total memory used: 230.750 MB
% 10.32/1.78 % Net memory used: 222.128 MB
%------------------------------------------------------------------------------