%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : AGT026+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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 : Fri Sep 25 12:51:00 PM UTC 2026
% Result : Theorem 262.10s 39.39s
% Output : CNFRefutation 163.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 48
% Syntax : Number of formulae : 336 ( 110 unt; 0 def)
% Number of atoms : 981 ( 128 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1214 ( 569 ~; 553 |; 79 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 32 con; 0-2 aty)
% Number of variables : 366 ( 0 sgn 362 !; 4 ?; 249 :)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( less(X2,X1)
& accept_number(X0,X1) )
=> accept_number(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_2) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( less(X2,X1)
& accept_population(X0,X3,X1) )
=> accept_population(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_3) ).
fof(f13,axiom,
! [X0] :
( ( accept_population(X0,other,n2)
& accept_population(X0,native,n15)
& accept_population(X0,muslim,n0)
& accept_population(X0,christian,n13)
& accept_population(X0,atheist,n70) )
<=> accept_city(X0,northport) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_6) ).
fof(f14,axiom,
! [X0] :
( ( 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) )
<=> accept_city(X0,coastvillage) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_7) ).
fof(f15,axiom,
! [X0] :
( ( accept_population(X0,other,n0)
& accept_population(X0,native,n100)
& accept_population(X0,muslim,n0)
& accept_population(X0,christian,n0)
& accept_population(X0,atheist,n0) )
<=> accept_city(X0,sunsetpoint) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_8) ).
fof(f16,axiom,
! [X0] :
( ( 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) )
<=> accept_city(X0,towna) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_9) ).
fof(f19,axiom,
! [X0] :
( ( accept_population(X0,other,n1)
& accept_population(X0,native,n0)
& accept_population(X0,muslim,n1)
& accept_population(X0,christian,n20)
& accept_population(X0,atheist,n78) )
<=> accept_city(X0,cityb) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_12) ).
fof(f272,axiom,
accept_population(christiancountrychumanitarianorganization,other,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_3) ).
fof(f273,axiom,
accept_population(christiancountrychumanitarianorganization,muslim,n65),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_4) ).
fof(f274,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_5) ).
fof(f281,axiom,
accept_city(christiancountrychumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_12) ).
fof(f282,axiom,
~ accept_city(countryamedicalorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_13) ).
fof(f286,axiom,
accept_population(countryamedicalorganization,christian,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_17) ).
fof(f327,axiom,
~ accept_number(countryccivilorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_58) ).
fof(f362,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_93) ).
fof(f366,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n12),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_97) ).
fof(f472,axiom,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_203) ).
fof(f473,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_204) ).
fof(f489,axiom,
accept_population(countryamedicalorganization,other,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_220) ).
fof(f491,axiom,
accept_population(countryamedicalorganization,muslim,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_222) ).
fof(f493,axiom,
accept_population(countryamedicalorganization,atheist,n75),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_224) ).
fof(f590,axiom,
accept_number(countryccivilorganization,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_321) ).
fof(f616,axiom,
accept_population(christiancountrychumanitarianorganization,other,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_347) ).
fof(f618,axiom,
accept_population(christiancountrychumanitarianorganization,muslim,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_349) ).
fof(f621,axiom,
accept_city(christiancountrychumanitarianorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_352) ).
fof(f635,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+2.ax',deduced_366) ).
fof(f637,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn0) ).
fof(f638,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn1) ).
fof(f640,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn3) ).
fof(f641,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn4) ).
fof(f642,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn5) ).
fof(f661,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn24) ).
fof(f722,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn85) ).
fof(f737,axiom,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn100) ).
fof(f893,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit1) ).
fof(f902,axiom,
rdn_positive_less(rdnn(n0),rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less01) ).
fof(f905,axiom,
rdn_positive_less(rdnn(n3),rdnn(n4)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less34) ).
fof(f906,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less45) ).
fof(f912,axiom,
! [X0,X1,X2,X3] :
( rdn_positive_less(X1,X3)
=> rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_multi_digit_high) ).
fof(f914,axiom,
! [X0,X1,X2] :
( rdn_non_zero(X2)
=> rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_extra_digits_positive_less) ).
fof(f915,axiom,
! [X0] :
( rdn_non_zero_digit(rdnn(X0))
=> rdn_non_zero(rdnn(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_digit) ).
fof(f916,axiom,
! [X0,X1] :
( rdn_non_zero(X1)
=> rdn_non_zero(rdn(rdnn(X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_structure) ).
fof(f917,axiom,
! [X0,X1,X2,X3] :
( ( rdn_positive_less(X2,X3)
& rdn_translate(X1,rdn_pos(X3))
& rdn_translate(X0,rdn_pos(X2)) )
=> less(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
fof(f920,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( X1 != X0
& ~ less(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_property) ).
fof(f923,conjecture,
? [X0,X1] : ~ accept_population(X0,X1,n100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_26) ).
fof(f924,negated_conjecture,
~ ? [X0,X1] : ~ accept_population(X0,X1,n100),
inference(negated_conjecture,[status(cth)],[f923]) ).
fof(f929,plain,
! [X0,X1,X2] :
( ~ less(X2,X1)
| ~ accept_number(X0,X1)
| accept_number(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f930,plain,
! [X0,X1,X2] :
( ~ less(X2,X1)
| ~ accept_number(X0,X1)
| accept_number(X0,X2) ),
inference(flattening,[],[f929]) ).
fof(f931,plain,
! [X0,X1,X2,X3] :
( ~ less(X2,X1)
| ~ accept_population(X0,X3,X1)
| accept_population(X0,X3,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f932,plain,
! [X0,X1,X2,X3] :
( ~ less(X2,X1)
| ~ accept_population(X0,X3,X1)
| accept_population(X0,X3,X2) ),
inference(flattening,[],[f931]) ).
fof(f939,plain,
! [X0,X1,X2,X3] :
( ~ rdn_positive_less(X1,X3)
| rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3)) ),
inference(ennf_transformation,[],[f912]) ).
fof(f942,plain,
! [X0,X1,X2] :
( ~ rdn_non_zero(X2)
| rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2)) ),
inference(ennf_transformation,[],[f914]) ).
fof(f943,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(X0))
| rdn_non_zero(rdnn(X0)) ),
inference(ennf_transformation,[],[f915]) ).
fof(f944,plain,
! [X0,X1] :
( ~ rdn_non_zero(X1)
| rdn_non_zero(rdn(rdnn(X0),X1)) ),
inference(ennf_transformation,[],[f916]) ).
fof(f945,plain,
! [X0,X1,X2,X3] :
( ~ rdn_positive_less(X2,X3)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| less(X0,X1) ),
inference(ennf_transformation,[],[f917]) ).
fof(f946,plain,
! [X0,X1,X2,X3] :
( ~ rdn_positive_less(X2,X3)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| less(X0,X1) ),
inference(flattening,[],[f945]) ).
fof(f951,plain,
! [X0,X1] : accept_population(X0,X1,n100),
inference(ennf_transformation,[],[f924]) ).
fof(f964,plain,
! [X0] :
( ( ~ accept_population(X0,other,n2)
| ~ accept_population(X0,native,n15)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n13)
| ~ accept_population(X0,atheist,n70)
| accept_city(X0,northport) )
& ( ~ accept_city(X0,northport)
| ( accept_population(X0,other,n2)
& accept_population(X0,native,n15)
& accept_population(X0,muslim,n0)
& accept_population(X0,christian,n13)
& accept_population(X0,atheist,n70) ) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f965,plain,
! [X0] :
( ( ~ accept_population(X0,other,n2)
| ~ accept_population(X0,native,n15)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n13)
| ~ accept_population(X0,atheist,n70)
| accept_city(X0,northport) )
& ( ~ accept_city(X0,northport)
| ( accept_population(X0,other,n2)
& accept_population(X0,native,n15)
& accept_population(X0,muslim,n0)
& accept_population(X0,christian,n13)
& accept_population(X0,atheist,n70) ) ) ),
inference(flattening,[],[f964]) ).
fof(f966,plain,
! [X0] :
( ( ~ 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)
| accept_city(X0,coastvillage) )
& ( ~ 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(nnf_transformation,[],[f14]) ).
fof(f967,plain,
! [X0] :
( ( ~ 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)
| accept_city(X0,coastvillage) )
& ( ~ 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(flattening,[],[f966]) ).
fof(f968,plain,
! [X0] :
( ( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n100)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0)
| accept_city(X0,sunsetpoint) )
& ( ~ accept_city(X0,sunsetpoint)
| ( accept_population(X0,other,n0)
& accept_population(X0,native,n100)
& accept_population(X0,muslim,n0)
& accept_population(X0,christian,n0)
& accept_population(X0,atheist,n0) ) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f969,plain,
! [X0] :
( ( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n100)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0)
| accept_city(X0,sunsetpoint) )
& ( ~ accept_city(X0,sunsetpoint)
| ( accept_population(X0,other,n0)
& accept_population(X0,native,n100)
& accept_population(X0,muslim,n0)
& accept_population(X0,christian,n0)
& accept_population(X0,atheist,n0) ) ) ),
inference(flattening,[],[f968]) ).
fof(f970,plain,
! [X0] :
( ( ~ 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)
| accept_city(X0,towna) )
& ( ~ 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(nnf_transformation,[],[f16]) ).
fof(f971,plain,
! [X0] :
( ( ~ 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)
| accept_city(X0,towna) )
& ( ~ 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(flattening,[],[f970]) ).
fof(f976,plain,
! [X0] :
( ( ~ accept_population(X0,other,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| accept_city(X0,cityb) )
& ( ~ accept_city(X0,cityb)
| ( accept_population(X0,other,n1)
& accept_population(X0,native,n0)
& accept_population(X0,muslim,n1)
& accept_population(X0,christian,n20)
& accept_population(X0,atheist,n78) ) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f977,plain,
! [X0] :
( ( ~ accept_population(X0,other,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| accept_city(X0,cityb) )
& ( ~ accept_city(X0,cityb)
| ( accept_population(X0,other,n1)
& accept_population(X0,native,n0)
& accept_population(X0,muslim,n1)
& accept_population(X0,christian,n20)
& accept_population(X0,atheist,n78) ) ) ),
inference(flattening,[],[f976]) ).
fof(f980,plain,
! [X0,X1] :
( ( ~ less(X0,X1)
| ( X1 != X0
& ~ less(X1,X0) ) )
& ( X0 = X1
| less(X1,X0)
| less(X0,X1) ) ),
inference(nnf_transformation,[],[f920]) ).
fof(f981,plain,
! [X0,X1] :
( ( ~ less(X0,X1)
| ( X1 != X0
& ~ less(X1,X0) ) )
& ( X0 = X1
| less(X1,X0)
| less(X0,X1) ) ),
inference(flattening,[],[f980]) ).
fof(f986,plain,
! [X2,X0,X1] :
( ~ less(X2,X1)
| ~ accept_number(X0,X1)
| accept_number(X0,X2) ),
inference(cnf_transformation,[],[f930]) ).
fof(f987,plain,
! [X2,X3,X0,X1] :
( ~ less(X2,X1)
| ~ accept_population(X0,X3,X1)
| accept_population(X0,X3,X2) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1025,plain,
! [X0] :
( ~ accept_city(X0,northport)
| accept_population(X0,muslim,n0) ),
inference(cnf_transformation,[],[f965]) ).
fof(f1028,plain,
! [X0] :
( ~ 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)
| accept_city(X0,coastvillage) ),
inference(cnf_transformation,[],[f967]) ).
fof(f1034,plain,
! [X0] :
( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n100)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0)
| accept_city(X0,sunsetpoint) ),
inference(cnf_transformation,[],[f969]) ).
fof(f1035,plain,
! [X0] :
( ~ accept_city(X0,sunsetpoint)
| accept_population(X0,other,n0) ),
inference(cnf_transformation,[],[f969]) ).
fof(f1040,plain,
! [X0] :
( ~ 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)
| accept_city(X0,towna) ),
inference(cnf_transformation,[],[f971]) ).
fof(f1041,plain,
! [X0] :
( ~ accept_city(X0,towna)
| accept_population(X0,other,n0) ),
inference(cnf_transformation,[],[f971]) ).
fof(f1042,plain,
! [X0] :
( ~ accept_city(X0,towna)
| accept_population(X0,native,n0) ),
inference(cnf_transformation,[],[f971]) ).
fof(f1058,plain,
! [X0] :
( ~ accept_population(X0,other,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| accept_city(X0,cityb) ),
inference(cnf_transformation,[],[f977]) ).
fof(f1060,plain,
! [X0] :
( ~ accept_city(X0,cityb)
| accept_population(X0,native,n0) ),
inference(cnf_transformation,[],[f977]) ).
fof(f1061,plain,
! [X0] :
( ~ accept_city(X0,cityb)
| accept_population(X0,muslim,n1) ),
inference(cnf_transformation,[],[f977]) ).
fof(f1321,plain,
accept_population(christiancountrychumanitarianorganization,other,n5),
inference(cnf_transformation,[],[f272]) ).
fof(f1322,plain,
accept_population(christiancountrychumanitarianorganization,muslim,n65),
inference(cnf_transformation,[],[f273]) ).
fof(f1323,plain,
accept_population(christiancountrychumanitarianorganization,christian,n0),
inference(cnf_transformation,[],[f274]) ).
fof(f1330,plain,
accept_city(christiancountrychumanitarianorganization,cityb),
inference(cnf_transformation,[],[f281]) ).
fof(f1331,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(cnf_transformation,[],[f282]) ).
fof(f1335,plain,
accept_population(countryamedicalorganization,christian,n0),
inference(cnf_transformation,[],[f286]) ).
fof(f1376,plain,
~ accept_number(countryccivilorganization,n5),
inference(cnf_transformation,[],[f327]) ).
fof(f1411,plain,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
inference(cnf_transformation,[],[f362]) ).
fof(f1415,plain,
accept_population(muslimcountrybhumanitarianorganization,atheist,n12),
inference(cnf_transformation,[],[f366]) ).
fof(f1521,plain,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
inference(cnf_transformation,[],[f472]) ).
fof(f1522,plain,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1),
inference(cnf_transformation,[],[f473]) ).
fof(f1538,plain,
accept_population(countryamedicalorganization,other,n0),
inference(cnf_transformation,[],[f489]) ).
fof(f1540,plain,
accept_population(countryamedicalorganization,muslim,n1),
inference(cnf_transformation,[],[f491]) ).
fof(f1542,plain,
accept_population(countryamedicalorganization,atheist,n75),
inference(cnf_transformation,[],[f493]) ).
fof(f1639,plain,
accept_number(countryccivilorganization,n3),
inference(cnf_transformation,[],[f590]) ).
fof(f1665,plain,
accept_population(christiancountrychumanitarianorganization,other,n0),
inference(cnf_transformation,[],[f616]) ).
fof(f1667,plain,
accept_population(christiancountrychumanitarianorganization,muslim,n1),
inference(cnf_transformation,[],[f618]) ).
fof(f1670,plain,
accept_city(christiancountrychumanitarianorganization,towna),
inference(cnf_transformation,[],[f621]) ).
fof(f1684,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(cnf_transformation,[],[f635]) ).
fof(f1686,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(cnf_transformation,[],[f637]) ).
fof(f1687,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(cnf_transformation,[],[f638]) ).
fof(f1689,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(cnf_transformation,[],[f640]) ).
fof(f1690,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(cnf_transformation,[],[f641]) ).
fof(f1691,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(cnf_transformation,[],[f642]) ).
fof(f1710,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(cnf_transformation,[],[f661]) ).
fof(f1771,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(cnf_transformation,[],[f722]) ).
fof(f1786,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(cnf_transformation,[],[f737]) ).
fof(f1942,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[],[f893]) ).
fof(f1951,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(cnf_transformation,[],[f902]) ).
fof(f1954,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(cnf_transformation,[],[f905]) ).
fof(f1955,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f906]) ).
fof(f1961,plain,
! [X2,X3,X0,X1] :
( ~ rdn_positive_less(X1,X3)
| rdn_positive_less(rdn(rdnn(X0),X1),rdn(rdnn(X2),X3)) ),
inference(cnf_transformation,[],[f939]) ).
fof(f1963,plain,
! [X2,X0,X1] :
( ~ rdn_non_zero(X2)
| rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2)) ),
inference(cnf_transformation,[],[f942]) ).
fof(f1964,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(X0))
| rdn_non_zero(rdnn(X0)) ),
inference(cnf_transformation,[],[f943]) ).
fof(f1965,plain,
! [X0,X1] :
( ~ rdn_non_zero(X1)
| rdn_non_zero(rdn(rdnn(X0),X1)) ),
inference(cnf_transformation,[],[f944]) ).
fof(f1966,plain,
! [X2,X3,X0,X1] :
( ~ rdn_positive_less(X2,X3)
| ~ rdn_translate(X1,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X2))
| less(X0,X1) ),
inference(cnf_transformation,[],[f946]) ).
fof(f1970,plain,
! [X0,X1] :
( ~ less(X0,X1)
| ~ less(X1,X0) ),
inference(cnf_transformation,[],[f981]) ).
fof(f1971,plain,
! [X0,X1] :
( X0 = X1
| less(X1,X0)
| less(X0,X1) ),
inference(cnf_transformation,[],[f981]) ).
fof(f1972,plain,
! [X0,X1] : accept_population(X0,X1,n100),
inference(cnf_transformation,[],[f951]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_number(X0,X2)
| ~ less(X2,X1)
| ~ accept_number(X0,X1) ),
inference(cnf_transformation,[],[f986]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( accept_population(X0,X1,X3)
| ~ less(X3,X2)
| ~ accept_population(X0,X1,X2) ),
inference(cnf_transformation,[],[f987]) ).
tcf(c_91,plain,
! [X0: $i] :
( accept_population(X0,muslim,n0)
| ~ accept_city(X0,northport) ),
inference(cnf_transformation,[],[f1025]) ).
tcf(c_100,plain,
! [X0: $i] :
( 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,[],[f1028]) ).
tcf(c_105,plain,
! [X0: $i] :
( accept_population(X0,other,n0)
| ~ accept_city(X0,sunsetpoint) ),
inference(cnf_transformation,[],[f1035]) ).
tcf(c_106,plain,
! [X0: $i] :
( accept_city(X0,sunsetpoint)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n100)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0) ),
inference(cnf_transformation,[],[f1034]) ).
tcf(c_110,plain,
! [X0: $i] :
( accept_population(X0,native,n0)
| ~ accept_city(X0,towna) ),
inference(cnf_transformation,[],[f1042]) ).
tcf(c_111,plain,
! [X0: $i] :
( accept_population(X0,other,n0)
| ~ accept_city(X0,towna) ),
inference(cnf_transformation,[],[f1041]) ).
tcf(c_112,plain,
! [X0: $i] :
( 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,[],[f1040]) ).
tcf(c_127,plain,
! [X0: $i] :
( accept_population(X0,muslim,n1)
| ~ accept_city(X0,cityb) ),
inference(cnf_transformation,[],[f1061]) ).
tcf(c_128,plain,
! [X0: $i] :
( accept_population(X0,native,n0)
| ~ accept_city(X0,cityb) ),
inference(cnf_transformation,[],[f1060]) ).
tcf(c_130,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_population(X0,other,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78) ),
inference(cnf_transformation,[],[f1058]) ).
tcf(c_388,plain,
accept_population(christiancountrychumanitarianorganization,other,n5),
inference(cnf_transformation,[],[f1321]) ).
tcf(c_389,plain,
accept_population(christiancountrychumanitarianorganization,muslim,n65),
inference(cnf_transformation,[],[f1322]) ).
tcf(c_390,plain,
accept_population(christiancountrychumanitarianorganization,christian,n0),
inference(cnf_transformation,[],[f1323]) ).
tcf(c_397,plain,
accept_city(christiancountrychumanitarianorganization,cityb),
inference(cnf_transformation,[],[f1330]) ).
tcf(c_398,plain,
~ accept_city(countryamedicalorganization,coastvillage),
inference(cnf_transformation,[],[f1331]) ).
tcf(c_402,plain,
accept_population(countryamedicalorganization,christian,n0),
inference(cnf_transformation,[],[f1335]) ).
tcf(c_443,plain,
~ accept_number(countryccivilorganization,n5),
inference(cnf_transformation,[],[f1376]) ).
tcf(c_478,plain,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
inference(cnf_transformation,[],[f1411]) ).
tcf(c_482,plain,
accept_population(muslimcountrybhumanitarianorganization,atheist,n12),
inference(cnf_transformation,[],[f1415]) ).
tcf(c_588,plain,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
inference(cnf_transformation,[],[f1521]) ).
tcf(c_589,plain,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1),
inference(cnf_transformation,[],[f1522]) ).
tcf(c_605,plain,
accept_population(countryamedicalorganization,other,n0),
inference(cnf_transformation,[],[f1538]) ).
tcf(c_607,plain,
accept_population(countryamedicalorganization,muslim,n1),
inference(cnf_transformation,[],[f1540]) ).
tcf(c_609,plain,
accept_population(countryamedicalorganization,atheist,n75),
inference(cnf_transformation,[],[f1542]) ).
tcf(c_706,plain,
accept_number(countryccivilorganization,n3),
inference(cnf_transformation,[],[f1639]) ).
tcf(c_732,plain,
accept_population(christiancountrychumanitarianorganization,other,n0),
inference(cnf_transformation,[],[f1665]) ).
tcf(c_734,plain,
accept_population(christiancountrychumanitarianorganization,muslim,n1),
inference(cnf_transformation,[],[f1667]) ).
tcf(c_737,plain,
accept_city(christiancountrychumanitarianorganization,towna),
inference(cnf_transformation,[],[f1670]) ).
tcf(c_751,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(cnf_transformation,[],[f1684]) ).
tcf(c_753,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(cnf_transformation,[],[f1686]) ).
tcf(c_754,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(cnf_transformation,[],[f1687]) ).
tcf(c_756,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(cnf_transformation,[],[f1689]) ).
tcf(c_757,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(cnf_transformation,[],[f1690]) ).
tcf(c_758,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(cnf_transformation,[],[f1691]) ).
tcf(c_777,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(cnf_transformation,[],[f1710]) ).
tcf(c_838,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(cnf_transformation,[],[f1771]) ).
tcf(c_853,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(cnf_transformation,[],[f1786]) ).
tcf(c_1009,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[],[f1942]) ).
tcf(c_1018,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(cnf_transformation,[],[f1951]) ).
tcf(c_1021,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(cnf_transformation,[],[f1954]) ).
tcf(c_1022,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(cnf_transformation,[],[f1955]) ).
tcf(c_1028,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( rdn_positive_less(rdn(rdnn(X2),X0),rdn(rdnn(X3),X1))
| ~ rdn_positive_less(X0,X1) ),
inference(cnf_transformation,[],[f1961]) ).
tcf(c_1030,plain,
! [X0: $i,X1: $i,X2: $i] :
( rdn_positive_less(rdnn(X1),rdn(rdnn(X2),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[],[f1963]) ).
tcf(c_1031,plain,
! [X0: $i] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[],[f1964]) ).
tcf(c_1032,plain,
! [X0: $i,X1: $i] :
( rdn_non_zero(rdn(rdnn(X1),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[],[f1965]) ).
tcf(c_1033,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( less(X0,X2)
| ~ rdn_positive_less(X1,X3)
| ~ rdn_translate(X2,rdn_pos(X3))
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(cnf_transformation,[],[f1966]) ).
tcf(c_1036,plain,
! [X0: $i,X1: $i] :
( less(X1,X0)
| less(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f1971]) ).
tcf(c_1037,plain,
! [X0: $i,X1: $i] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f1970]) ).
tcf(c_1039,negated_conjecture,
! [X0: $i,X1: $i] : accept_population(X0,X1,n100),
inference(cnf_transformation,[],[f1972]) ).
tcf(c_1042,plain,
( rdn_non_zero(rdnn(n1))
| ~ rdn_non_zero_digit(rdnn(n1)) ),
inference(instantiation,[status(thm)],[c_1031]) ).
tcf(c_1175,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_1179,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( accept_city(X0,X2)
| ~ accept_city(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( accept_population(X0,X2,X4)
| ~ accept_population(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1202,plain,
! [X0: $i] :
( accept_city(X0,sunsetpoint)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_106,c_1039]) ).
tcf(c_1853,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X1,X2,X0)
| ~ less(X0,n100) ),
inference(superposition,[status(thm)],[c_1039,c_54]) ).
tcf(c_2302,plain,
! [X0: $i] :
( accept_city(X0,sunsetpoint)
| ~ less(n0,n100)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n100)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0) ),
inference(superposition,[status(thm)],[c_1853,c_106]) ).
tcf(c_2349,plain,
! [X0: $i] :
( accept_city(X0,sunsetpoint)
| ~ less(n0,n100)
| ~ accept_population(X0,native,n100) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2302,c_1853,c_1853,c_1853]) ).
tcf(c_3247,plain,
! [X0: $i] :
( accept_city(X0,sunsetpoint)
| ~ less(n0,n100) ),
inference(superposition,[status(thm)],[c_1039,c_2349]) ).
tcf(c_3407,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n3),rdnn(n4))
| ~ rdn_translate(X1,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_3409,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_translate(X1,rdn_pos(rdnn(n5)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_3465,plain,
! [X0: $i,X1: $i] :
( accept_city(X0,X1)
| ~ accept_city(christiancountrychumanitarianorganization,cityb)
| ( X1 != cityb )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(instantiation,[status(thm)],[c_1179]) ).
tcf(c_6170,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_city(X0,towna)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(resolution,[status(thm)],[c_100,c_111]) ).
tcf(c_6176,plain,
( accept_city(countryamedicalorganization,coastvillage)
| ~ accept_population(countryamedicalorganization,native,n85)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(resolution,[status(thm)],[c_100,c_605]) ).
tcf(c_6250,plain,
n0 = n0,
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_6271,plain,
other = other,
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_6333,plain,
( ~ accept_population(countryamedicalorganization,atheist,n12)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,native,n85) ),
inference(global_subsumption_just,[status(thm)],[c_6176,c_398,c_6176]) ).
tcf(c_6334,plain,
( ~ accept_population(countryamedicalorganization,native,n85)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(renaming,[status(thm)],[c_6333]) ).
tcf(c_6731,plain,
muslim = muslim,
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_7460,plain,
( accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(resolution,[status(thm)],[c_112,c_478]) ).
tcf(c_7637,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24) ),
inference(global_subsumption_just,[status(thm)],[c_7460,c_751,c_589,c_588,c_7460]) ).
tcf(c_7638,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(renaming,[status(thm)],[c_7637]) ).
tcf(c_8871,plain,
! [X0: $i,X1: $i] :
( accept_number(X0,n100)
| ~ less(n100,X1)
| ~ accept_number(X0,X1) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_8873,plain,
! [X0: $i] :
( ~ less(n100,X0)
| ~ less(X0,n100) ),
inference(instantiation,[status(thm)],[c_1037]) ).
tcf(c_10875,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ( X2 != n5 )
| ( X1 != other )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_1182,c_388]) ).
tcf(c_10877,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ( X2 != n65 )
| ( X1 != muslim )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_1182,c_389]) ).
tcf(c_10879,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ( X2 != n0 )
| ( X1 != christian )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_1182,c_390]) ).
tcf(c_11123,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ( X2 != n75 )
| ( X1 != atheist )
| ( X0 != countryamedicalorganization ) ),
inference(resolution,[status(thm)],[c_1182,c_609]) ).
tcf(c_11217,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( accept_population(X0,X2,X4)
| ( X4 != n100 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1182,c_1039]) ).
tcf(c_11228,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ~ less(X2,n100)
| ~ accept_population(X0,X1,n100) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_11229,plain,
! [X0: $i,X1: $i] :
( accept_number(X0,X1)
| ~ less(X1,n100)
| ~ accept_number(X0,n100) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_12499,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( accept_population(X0,X3,X2)
| ( X2 != n100 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_11217,c_1175]) ).
tcf(c_12572,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X1,X2,X0)
| ( X0 != n100 ) ),
inference(resolution,[status(thm)],[c_12499,c_1175]) ).
tcf(c_12706,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ( n1 != n100 ) ),
inference(resolution,[status(thm)],[c_12572,c_130]) ).
tcf(c_12713,plain,
! [X0: $i] :
( accept_city(X0,towna)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ( n0 != n100 ) ),
inference(resolution,[status(thm)],[c_12572,c_112]) ).
tcf(c_12722,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( accept_population(X0,X2,X4)
| ( X5 != n100 )
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_12572,c_1182]) ).
tcf(c_15148,plain,
! [X0: $i] :
( accept_number(X0,n100)
| ~ less(n100,n3)
| ~ accept_number(X0,n3) ),
inference(instantiation,[status(thm)],[c_8871]) ).
tcf(c_17513,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ( n1 != n100 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12706,c_12572]) ).
tcf(c_17530,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_city(X0,towna)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ( n1 != n100 ) ),
inference(resolution,[status(thm)],[c_17513,c_110]) ).
tcf(c_18509,plain,
! [X0: $i] :
( accept_city(X0,towna)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ( n0 != n100 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12713,c_12572]) ).
tcf(c_19263,plain,
( ~ less(n100,n85)
| ~ less(n85,n100) ),
inference(instantiation,[status(thm)],[c_8873]) ).
tcf(c_19428,plain,
! [X0: $i] :
( accept_population(X0,muslim,n0)
| ~ less(n0,n100)
| ~ accept_population(X0,muslim,n100) ),
inference(instantiation,[status(thm)],[c_11228]) ).
tcf(c_19639,plain,
( accept_number(countryccivilorganization,n5)
| ~ less(n5,n100)
| ~ accept_number(countryccivilorganization,n100) ),
inference(instantiation,[status(thm)],[c_11229]) ).
tcf(c_19955,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_city(X0,towna)
| ~ accept_population(X0,atheist,n78)
| ( n1 != n100 )
| ( n20 != n100 ) ),
inference(resolution,[status(thm)],[c_17530,c_12572]) ).
tcf(c_21605,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_city(X0,towna)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12)
| ( n85 != n5 )
| ( native != other )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_10875,c_6170]) ).
tcf(c_37324,plain,
( accept_number(countryccivilorganization,n100)
| ~ less(n100,n3)
| ~ accept_number(countryccivilorganization,n3) ),
inference(instantiation,[status(thm)],[c_15148]) ).
tcf(c_42196,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_city(X0,towna)
| ( n78 != n65 )
| ( n1 != n100 )
| ( n20 != n100 )
| ( atheist != muslim )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_10877,c_19955]) ).
tcf(c_44100,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ~ accept_city(christiancountrychumanitarianorganization,cityb)
| ( cityb != cityb )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(instantiation,[status(thm)],[c_3465]) ).
tcf(c_44101,plain,
cityb = cityb,
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_45082,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( accept_population(X0,other,n0)
| ~ accept_population(X1,X2,X3)
| ( n0 != X3 )
| ( other != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_46011,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n0),rdnn(n1))
| ~ rdn_translate(X1,rdn_pos(rdnn(n1)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n0))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_46014,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n3),rdnn(n4))
| ~ rdn_translate(X1,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_46015,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_translate(X1,rdn_pos(rdnn(n5)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_47378,plain,
! [X0: $i] :
( accept_city(X0,cityb)
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(global_subsumption_just,[status(thm)],[c_42196,c_397,c_44100,c_44101]) ).
tcf(c_48898,plain,
! [X0: $i] :
( less(n0,X0)
| ~ rdn_positive_less(rdnn(n0),rdnn(n1))
| ~ rdn_translate(n0,rdn_pos(rdnn(n0)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n1))) ),
inference(instantiation,[status(thm)],[c_46011]) ).
tcf(c_48899,plain,
( less(n0,n1)
| ~ rdn_positive_less(rdnn(n0),rdnn(n1))
| ~ rdn_translate(n0,rdn_pos(rdnn(n0)))
| ~ rdn_translate(n1,rdn_pos(rdnn(n1))) ),
inference(instantiation,[status(thm)],[c_48898]) ).
tcf(c_48904,plain,
! [X0: $i] :
( less(X0,n4)
| ~ rdn_positive_less(rdnn(n3),rdnn(n4))
| ~ rdn_translate(n4,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(instantiation,[status(thm)],[c_46014]) ).
tcf(c_48906,plain,
! [X0: $i] :
( less(X0,n5)
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_translate(n5,rdn_pos(rdnn(n5)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(instantiation,[status(thm)],[c_46015]) ).
tcf(c_49012,plain,
towna = towna,
inference(instantiation,[status(thm)],[c_1175]) ).
tcf(c_51611,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,other,n0)
| ~ accept_population(X1,X2,n0)
| ( n0 != n0 )
| ( other != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_45082]) ).
tcf(c_68475,plain,
! [X0: $i,X1: $i] :
( accept_population(X0,other,n0)
| ~ accept_population(X1,other,n0)
| ( n0 != n0 )
| ( other != other )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_51611]) ).
tcf(c_70900,plain,
! [X0: $i] :
( accept_population(X0,other,n0)
| ~ accept_population(christiancountrychumanitarianorganization,other,n0)
| ( n0 != n0 )
| ( other != other )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(instantiation,[status(thm)],[c_68475]) ).
tcf(c_77202,plain,
( rdn_non_zero(rdn(rdnn(n0),rdnn(n1)))
| ~ rdn_non_zero(rdnn(n1)) ),
inference(instantiation,[status(thm)],[c_1032]) ).
tcf(c_80688,plain,
! [X0: $i] :
( accept_city(X0,towna)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ( n0 != n100 )
| ( n1 != n0 )
| ( muslim != christian )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_10879,c_18509]) ).
tcf(c_82094,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( accept_population(X0,muslim,n0)
| ~ accept_population(X1,X2,X3)
| ( n0 != X3 )
| ( muslim != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_1182]) ).
tcf(c_82993,plain,
! [X0: $i,X1: $i] :
( accept_city(X0,X1)
| ~ accept_city(christiancountrychumanitarianorganization,towna)
| ( X1 != towna )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(instantiation,[status(thm)],[c_1179]) ).
tcf(c_83676,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,muslim,n0)
| ~ accept_population(X1,X2,n0)
| ( n0 != n0 )
| ( muslim != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_82094]) ).
tcf(c_86192,plain,
! [X0: $i,X1: $i] :
( accept_population(X0,muslim,n0)
| ~ accept_population(X1,muslim,n0)
| ( n0 != n0 )
| ( muslim != muslim )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_83676]) ).
tcf(c_86419,plain,
! [X0: $i] :
( accept_city(X0,towna)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(global_subsumption_just,[status(thm)],[c_80688,c_732,c_128,c_127,c_112,c_6250,c_6271,c_47378,c_70900]) ).
tcf(c_86638,plain,
! [X0: $i] :
( accept_city(X0,towna)
| ~ accept_city(christiancountrychumanitarianorganization,towna)
| ( towna != towna )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(instantiation,[status(thm)],[c_82993]) ).
tcf(c_86664,plain,
! [X0: $i] :
( accept_city(X0,towna)
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(global_subsumption_just,[status(thm)],[c_86419,c_737,c_49012,c_86638]) ).
tcf(c_91012,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12)
| ( n85 != n5 )
| ( native != other )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_21605,c_86664]) ).
tcf(c_97590,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ less(n0,n100)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(superposition,[status(thm)],[c_1853,c_100]) ).
tcf(c_141199,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ~ less(X2,n4)
| ~ accept_population(X0,X1,n4) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_147778,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,n0)
| ~ less(n0,X2)
| ~ accept_population(X0,X1,X2) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_172725,plain,
! [X0: $i,X1: $i] :
( accept_population(X0,X1,n3)
| ~ less(n3,n4)
| ~ accept_population(X0,X1,n4) ),
inference(instantiation,[status(thm)],[c_141199]) ).
tcf(c_173545,plain,
! [X0: $i,X1: $i] :
( accept_population(X0,muslim,n0)
| ~ less(n0,X1)
| ~ accept_population(X0,muslim,X1) ),
inference(instantiation,[status(thm)],[c_147778]) ).
tcf(c_175936,plain,
( accept_population(countryamedicalorganization,muslim,n0)
| ~ less(n0,n1)
| ~ accept_population(countryamedicalorganization,muslim,n1) ),
inference(instantiation,[status(thm)],[c_173545]) ).
tcf(c_175944,plain,
( accept_population(christiancountrychumanitarianorganization,muslim,n0)
| ~ less(n0,n1)
| ~ accept_population(christiancountrychumanitarianorganization,muslim,n1) ),
inference(instantiation,[status(thm)],[c_173545]) ).
tcf(c_175946,plain,
! [X0: $i] : accept_population(X0,muslim,n100),
inference(instantiation,[status(thm)],[c_1039]) ).
tcf(c_179888,plain,
! [X0: $i] :
( accept_population(X0,muslim,n0)
| ~ accept_population(christiancountrychumanitarianorganization,muslim,n0)
| ( n0 != n0 )
| ( muslim != muslim )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(instantiation,[status(thm)],[c_86192]) ).
tcf(c_200965,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n3),rdnn(n4))
| ~ rdn_translate(X1,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_200966,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_translate(X1,rdn_pos(rdnn(n5)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_203205,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_translate(X0,rdn_pos(rdnn(n3)))
| ~ rdn_translate(X1,rdn_pos(rdnn(n4))) ),
inference(global_subsumption_just,[status(thm)],[c_200965,c_1021,c_3407]) ).
tcf(c_203206,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_translate(X1,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(renaming,[status(thm)],[c_203205]) ).
tcf(c_203208,plain,
! [X0: $i] :
( less(X0,n4)
| ~ rdn_translate(n4,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(instantiation,[status(thm)],[c_203206]) ).
tcf(c_203228,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_translate(X0,rdn_pos(rdnn(n4)))
| ~ rdn_translate(X1,rdn_pos(rdnn(n5))) ),
inference(global_subsumption_just,[status(thm)],[c_200966,c_1022,c_3409]) ).
tcf(c_203229,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ~ rdn_translate(X1,rdn_pos(rdnn(n5)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(renaming,[status(thm)],[c_203228]) ).
tcf(c_203231,plain,
! [X0: $i] :
( less(X0,n5)
| ~ rdn_translate(n5,rdn_pos(rdnn(n5)))
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(instantiation,[status(thm)],[c_203229]) ).
tcf(c_213248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( less(n100,X5)
| less(X5,n100)
| accept_population(X0,X2,X4)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1036,c_12722]) ).
tcf(c_222521,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( less(n100,X4)
| less(X4,n100)
| accept_population(X0,X2,X4)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_213248,c_1175]) ).
tcf(c_223381,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_city(X0,sunsetpoint)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(resolution,[status(thm)],[c_105,c_100]) ).
tcf(c_246135,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ~ less(X2,n5)
| ~ accept_population(X0,X1,n5) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_255125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( less(n100,X3)
| less(X3,n100)
| accept_population(X0,X2,X3)
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_222521,c_1175]) ).
tcf(c_274273,plain,
! [X0: $i] :
( less(X0,n4)
| ~ rdn_translate(X0,rdn_pos(rdnn(n3))) ),
inference(global_subsumption_just,[status(thm)],[c_203208,c_1021,c_757,c_48904]) ).
tcf(c_274276,plain,
( less(n3,n4)
| ~ rdn_translate(n3,rdn_pos(rdnn(n3))) ),
inference(instantiation,[status(thm)],[c_274273]) ).
tcf(c_274350,plain,
! [X0: $i] :
( less(X0,n5)
| ~ rdn_translate(X0,rdn_pos(rdnn(n4))) ),
inference(global_subsumption_just,[status(thm)],[c_203231,c_1022,c_758,c_48906]) ).
tcf(c_274353,plain,
( less(n4,n5)
| ~ rdn_translate(n4,rdn_pos(rdnn(n4))) ),
inference(instantiation,[status(thm)],[c_274350]) ).
tcf(c_277536,plain,
! [X0: $i,X1: $i] :
( accept_population(X0,X1,n3)
| ~ less(n3,n4)
| ~ accept_population(X0,X1,n4) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_281380,plain,
! [X0: $i,X1: $i] :
( accept_population(X0,X1,n3)
| ~ accept_population(X0,X1,n4) ),
inference(global_subsumption_just,[status(thm)],[c_277536,c_756,c_172725,c_274276]) ).
tcf(c_283812,plain,
! [X0: $i] :
( accept_population(countryamedicalorganization,christian,X0)
| ~ less(X0,n0) ),
inference(resolution,[status(thm)],[c_54,c_402]) ).
tcf(c_283880,plain,
! [X0: $i] :
( accept_population(muslimcountrybhumanitarianorganization,atheist,X0)
| ~ less(X0,n12) ),
inference(resolution,[status(thm)],[c_54,c_482]) ).
tcf(c_283978,plain,
! [X0: $i] :
( accept_population(countryamedicalorganization,atheist,X0)
| ~ less(X0,n75) ),
inference(resolution,[status(thm)],[c_54,c_609]) ).
tcf(c_284046,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X1,X2,X0)
| ~ less(X0,n100) ),
inference(resolution,[status(thm)],[c_54,c_1039]) ).
tcf(c_287941,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( less(n100,X3)
| accept_population(X0,X2,X3)
| ( X0 != X1 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_255125,c_284046]) ).
tcf(c_287973,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ less(n0,n100)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12)
| ( n85 != n5 )
| ( native != other )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(resolution,[status(thm)],[c_284046,c_91012]) ).
tcf(c_288199,plain,
( ~ less(n85,n100)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(resolution,[status(thm)],[c_284046,c_6334]) ).
tcf(c_288225,plain,
( ~ less(n24,n100)
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(resolution,[status(thm)],[c_284046,c_7638]) ).
tcf(c_290608,plain,
! [X0: $i,X1: $i,X2: $i] :
( less(n100,X2)
| accept_population(X0,X1,X2) ),
inference(resolution,[status(thm)],[c_287941,c_1175]) ).
tcf(c_291818,plain,
( ~ less(n85,n100)
| ~ accept_population(countryamedicalorganization,atheist,n12)
| ~ accept_population(countryamedicalorganization,christian,n3) ),
inference(global_subsumption_just,[status(thm)],[c_288199,c_607,c_1018,c_754,c_753,c_48899,c_175936,c_288199]) ).
tcf(c_291819,plain,
( ~ less(n85,n100)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(renaming,[status(thm)],[c_291818]) ).
tcf(c_292963,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ~ less(X2,n100)
| ~ accept_population(X0,X1,n100) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_296954,plain,
! [X0: $i] :
( accept_population(X0,christian,n3)
| ~ accept_population(X0,christian,n4) ),
inference(instantiation,[status(thm)],[c_281380]) ).
tcf(c_300564,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X0,X1,X2)
| ~ less(X2,n100) ),
inference(global_subsumption_just,[status(thm)],[c_292963,c_1039,c_11228]) ).
tcf(c_300565,plain,
! [X0: $i,X1: $i,X2: $i] :
( accept_population(X1,X2,X0)
| ~ less(X0,n100) ),
inference(renaming,[status(thm)],[c_300564]) ).
tcf(c_300730,plain,
! [X0: $i] :
( accept_population(X0,christian,n5)
| ~ less(n5,n100) ),
inference(instantiation,[status(thm)],[c_300565]) ).
tcf(c_304644,plain,
! [X0: $i] :
( accept_population(X0,christian,n4)
| ~ less(n4,n5)
| ~ accept_population(X0,christian,n5) ),
inference(instantiation,[status(thm)],[c_246135]) ).
tcf(c_309375,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ( X0 != christiancountrychumanitarianorganization )
| ( native != other )
| ( n85 != n5 )
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3) ),
inference(global_subsumption_just,[status(thm)],[c_287973,c_734,c_1018,c_754,c_753,c_6250,c_6731,c_21605,c_48899,c_86664,c_175944,c_179888]) ).
tcf(c_309376,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12)
| ( n85 != n5 )
| ( native != other )
| ( X0 != christiancountrychumanitarianorganization ) ),
inference(renaming,[status(thm)],[c_309375]) ).
tcf(c_314709,plain,
! [X0: $i,X1: $i] :
( less(X1,n100)
| ~ rdn_translate(X1,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(resolution,[status(thm)],[c_1033,c_853]) ).
tcf(c_369261,plain,
( less(n100,n85)
| ~ accept_population(countryamedicalorganization,muslim,n0)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(resolution,[status(thm)],[c_290608,c_6334]) ).
tcf(c_370296,plain,
( accept_city(countryamedicalorganization,coastvillage)
| ~ less(n3,n0)
| ~ accept_population(countryamedicalorganization,atheist,n12)
| ( countryamedicalorganization != christiancountrychumanitarianorganization )
| ( n85 != n5 )
| ( native != other ) ),
inference(resolution,[status(thm)],[c_283812,c_309376]) ).
tcf(c_376156,plain,
( ( native != other )
| ( n85 != n5 )
| ( countryamedicalorganization != christiancountrychumanitarianorganization )
| ~ accept_population(countryamedicalorganization,atheist,n12)
| ~ less(n3,n0) ),
inference(global_subsumption_just,[status(thm)],[c_370296,c_398,c_370296]) ).
tcf(c_376157,plain,
( ~ less(n3,n0)
| ~ accept_population(countryamedicalorganization,atheist,n12)
| ( countryamedicalorganization != christiancountrychumanitarianorganization )
| ( n85 != n5 )
| ( native != other ) ),
inference(renaming,[status(thm)],[c_376156]) ).
tcf(c_392325,plain,
( less(n100,n85)
| ~ accept_population(countryamedicalorganization,atheist,n12)
| ~ accept_population(countryamedicalorganization,christian,n3) ),
inference(global_subsumption_just,[status(thm)],[c_369261,c_607,c_1018,c_754,c_753,c_48899,c_175936,c_369261]) ).
tcf(c_392326,plain,
( less(n100,n85)
| ~ accept_population(countryamedicalorganization,christian,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(renaming,[status(thm)],[c_392325]) ).
tcf(c_392710,plain,
( less(n100,n85)
| less(n100,n3)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(resolution,[status(thm)],[c_392326,c_290608]) ).
tcf(c_421215,plain,
! [X0: $i,X1: $i] :
( less(X1,n100)
| ~ rdn_translate(X1,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))
| ~ rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))) ),
inference(instantiation,[status(thm)],[c_1033]) ).
tcf(c_422622,plain,
! [X0: $i,X1: $i] :
( less(X1,n100)
| ~ rdn_translate(X1,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(global_subsumption_just,[status(thm)],[c_421215,c_314709]) ).
tcf(c_422649,plain,
! [X0: $i] :
( less(n12,X0)
| less(X0,n12)
| ( n12 = X0 ) ),
inference(instantiation,[status(thm)],[c_1036]) ).
tcf(c_426557,plain,
! [X0: $i] :
( less(n5,n100)
| ~ rdn_translate(n5,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_422622]) ).
tcf(c_426730,plain,
! [X0: $i] :
( less(n24,n100)
| ~ rdn_translate(n24,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_422622]) ).
tcf(c_426735,plain,
! [X0: $i] :
( less(n0,n100)
| ~ rdn_translate(n0,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_422622]) ).
tcf(c_430725,plain,
! [X0: $i] :
( less(n85,n100)
| ~ rdn_translate(n85,rdn_pos(X0))
| ~ rdn_positive_less(X0,rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_422622]) ).
tcf(c_430986,plain,
( less(n5,n100)
| ~ rdn_translate(n5,rdn_pos(rdnn(n5)))
| ~ rdn_positive_less(rdnn(n5),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_426557]) ).
tcf(c_431015,plain,
( less(n24,n100)
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_426730]) ).
tcf(c_431016,plain,
( less(n0,n100)
| ~ rdn_translate(n0,rdn_pos(rdnn(n0)))
| ~ rdn_positive_less(rdnn(n0),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_426735]) ).
tcf(c_432899,plain,
( less(n5,n100)
| ~ rdn_positive_less(rdnn(n5),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(global_subsumption_just,[status(thm)],[c_430986,c_758,c_430986]) ).
tcf(c_432901,plain,
( rdn_positive_less(rdnn(n5),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))
| ~ rdn_non_zero(rdn(rdnn(n0),rdnn(n1))) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_432977,plain,
( less(n24,n100)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(global_subsumption_just,[status(thm)],[c_431015,c_777,c_431015]) ).
tcf(c_432979,plain,
( rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))
| ~ rdn_positive_less(rdnn(n2),rdn(rdnn(n0),rdnn(n1))) ),
inference(instantiation,[status(thm)],[c_1028]) ).
tcf(c_433010,plain,
( less(n0,n100)
| ~ rdn_positive_less(rdnn(n0),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(global_subsumption_just,[status(thm)],[c_431016,c_753,c_431016]) ).
tcf(c_433012,plain,
( rdn_positive_less(rdnn(n0),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))
| ~ rdn_non_zero(rdn(rdnn(n0),rdnn(n1))) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_433538,plain,
( less(n85,n100)
| ~ rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8))))
| ~ rdn_positive_less(rdn(rdnn(n5),rdnn(n8)),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(instantiation,[status(thm)],[c_430725]) ).
tcf(c_436482,plain,
( less(n85,n100)
| ~ rdn_positive_less(rdn(rdnn(n5),rdnn(n8)),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1)))) ),
inference(global_subsumption_just,[status(thm)],[c_433538,c_838,c_433538]) ).
tcf(c_436484,plain,
( rdn_positive_less(rdn(rdnn(n5),rdnn(n8)),rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))
| ~ rdn_positive_less(rdnn(n8),rdn(rdnn(n0),rdnn(n1))) ),
inference(instantiation,[status(thm)],[c_1028]) ).
tcf(c_453979,plain,
! [X0: $i,X1: $i] :
( rdn_positive_less(rdnn(n2),rdn(rdnn(X1),X0))
| ~ rdn_non_zero(X0) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_454433,plain,
! [X0: $i,X1: $i] :
( rdn_positive_less(rdnn(n8),rdn(rdnn(X1),X0))
| ~ rdn_non_zero(X0) ),
inference(instantiation,[status(thm)],[c_1030]) ).
tcf(c_503840,plain,
! [X0: $i] : accept_population(X0,muslim,n0),
inference(global_subsumption_just,[status(thm)],[c_91,c_1009,c_1042,c_19428,c_77202,c_175946,c_433010,c_433012]) ).
tcf(c_503879,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_city(X0,sunsetpoint)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(backward_subsumption_resolution,[status(thm)],[c_223381,c_503840]) ).
tcf(c_503905,plain,
! [X0: $i] :
( accept_city(X0,sunsetpoint)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1202,c_503840]) ).
tcf(c_504197,plain,
! [X0: $i] : accept_city(X0,sunsetpoint),
inference(global_subsumption_just,[status(thm)],[c_503905,c_1009,c_753,c_1042,c_3247,c_77202,c_431016,c_433012]) ).
tcf(c_504278,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ),
inference(backward_subsumption_resolution,[status(thm)],[c_503879,c_504197]) ).
tcf(c_506498,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,atheist,n12) ),
inference(global_subsumption_just,[status(thm)],[c_504278,c_1009,c_758,c_757,c_1042,c_105,c_3247,c_77202,c_97590,c_274353,c_296954,c_300730,c_304644,c_430986,c_432901,c_433010,c_433012]) ).
tcf(c_506552,plain,
! [X0: $i] :
( accept_city(X0,coastvillage)
| ~ less(n85,n100)
| ~ accept_population(X0,atheist,n12) ),
inference(resolution,[status(thm)],[c_506498,c_284046]) ).
tcf(c_618203,plain,
( ~ less(n24,n100)
| ~ less(n75,n12) ),
inference(resolution,[status(thm)],[c_283880,c_288225]) ).
tcf(c_620786,plain,
( ~ less(n85,n100)
| ~ accept_population(countryamedicalorganization,atheist,n12) ),
inference(global_subsumption_just,[status(thm)],[c_291819,c_1009,c_706,c_443,c_1042,c_19263,c_19639,c_37324,c_77202,c_392710,c_432899,c_432901]) ).
tcf(c_621220,plain,
( accept_city(countryamedicalorganization,coastvillage)
| ~ less(n85,n100)
| ~ less(n12,n75) ),
inference(resolution,[status(thm)],[c_283978,c_506552]) ).
tcf(c_640825,plain,
( rdn_positive_less(rdnn(n2),rdn(rdnn(n0),rdnn(n1)))
| ~ rdn_non_zero(rdnn(n1)) ),
inference(instantiation,[status(thm)],[c_453979]) ).
tcf(c_645836,plain,
( rdn_positive_less(rdnn(n8),rdn(rdnn(n0),rdnn(n1)))
| ~ rdn_non_zero(rdnn(n1)) ),
inference(instantiation,[status(thm)],[c_454433]) ).
tcf(c_668654,plain,
~ accept_population(countryamedicalorganization,atheist,n12),
inference(global_subsumption_just,[status(thm)],[c_376157,c_1009,c_1042,c_436482,c_436484,c_620786,c_645836]) ).
tcf(c_737627,plain,
( ( countryamedicalorganization != countryamedicalorganization )
| ( n12 != n75 )
| ( atheist != atheist ) ),
inference(resolution,[status(thm)],[c_11123,c_668654]) ).
tcf(c_737628,plain,
n12 != n75,
inference(equality_resolution_simp,[status(thm)],[c_737627]) ).
tcf(c_786793,plain,
( less(n75,n12)
| less(n12,n75)
| ( n12 = n75 ) ),
inference(instantiation,[status(thm)],[c_422649]) ).
tcf(c_786794,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_786793,c_737628,c_645836,c_640825,c_621220,c_618203,c_436484,c_436482,c_432979,c_432977,c_1042,c_398,c_1009]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : AGT026+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.20/0.65 % Computer : n014.cluster.edu
% 0.20/0.65 % Model : x86_64 x86_64
% 0.20/0.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.65 % Memory : 8046.5625MB
% 0.20/0.65 % OS : Linux 6.8.0-71-generic
% 0.20/0.65 % CPULimit : 300
% 0.20/0.65 % WCLimit : 300
% 0.20/0.65 % DateTime : Fri Sep 25 04:28:18 UTC 2026
% 0.23/0.65 % CPUTime :
% 0.23/0.66 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.24/0.72 Running first-order theorem proving
% 0.24/0.72 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.24/0.73
% 0.24/0.73 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.73
% 0.24/0.74 % Detected problem language: tptp
% 0.24/0.76 % Proving...
% 262.10/39.39 % SZS status Started for theBenchmark.p
% 262.10/39.39 % SZS status Theorem for theBenchmark.p
% 262.10/39.39
% 262.10/39.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 262.10/39.39
% 262.10/39.39 % ------ iProver source info
% 262.10/39.39
% 262.10/39.39 % git: date: 2026-07-19 20:42:38 +0200
% 262.10/39.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 262.10/39.39 % git: non_committed_changes: false
% 262.10/39.39
% 262.10/39.39 % ------ Parsing...
% 262.10/39.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 262.10/39.39
% 262.10/39.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 1 0s sf_e %
% 262.10/39.39
% 262.10/39.39 % ------ Preprocessing...%
% 262.10/39.39
% 262.10/39.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 262.10/39.39 % ------ Proving...
% 262.10/39.39 % ------ Problem Properties
% 262.10/39.39
% 262.10/39.39 %
% 262.10/39.39 % clauses 954
% 262.10/39.39 % conjectures 1
% 262.10/39.39 % EPR 671
% 262.10/39.39 % Horn 953
% 262.10/39.39 % unary 855
% 262.10/39.39 % binary 76
% 262.10/39.39 % lits 1118
% 262.10/39.39 % lits eq 1
% 262.10/39.39 % fd_pure 0
% 262.10/39.39 % fd_pseudo 0
% 262.10/39.39 % fd_cond 0
% 262.10/39.39 % fd_pseudo_cond 1
% 262.10/39.39 % AC symbols 0
% 262.10/39.39
% 262.10/39.39 % ------ Input Options Time Limit: Unbounded
% 262.10/39.39
% 262.10/39.39
% 262.10/39.39 % ------
% 262.10/39.39 % Current options:
% 262.10/39.39 % ------
% 262.10/39.39
% 262.10/39.39
% 262.10/39.39 %
% 262.10/39.39
% 262.10/39.39 % ------ Proving...
% 262.10/39.39 %
% 262.10/39.39
% 262.10/39.39 % SZS status Theorem for theBenchmark.p
% 262.10/39.39
% 262.10/39.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 163.21/39.40
% 163.21/39.40
%------------------------------------------------------------------------------