%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : AGT014+1 : TPTP v9.2.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:03:47 PM UTC 2026
% Result : Theorem 0.47s 1.66s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_630)
% Comments :
%------------------------------------------------------------------------------
fof(query_14,conjecture,
? [X7,X8,X9] : ~ accept_population(X7,X8,X9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_14) ).
fof(less_property,axiom,
! [X7,X8] :
( less(X7,X8)
<=> ( ~ less(X8,X7)
& X8 != X7 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_property) ).
fof(a2_13,axiom,
! [X1] :
( ( accept_population(X1,atheist,n30)
& accept_population(X1,christian,n0)
& accept_population(X1,muslim,n65)
& accept_population(X1,native,n0)
& accept_population(X1,other,n5) )
<=> accept_city(X1,townc) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_13) ).
fof(a2_12,axiom,
! [X1] :
( ( accept_population(X1,atheist,n78)
& accept_population(X1,christian,n20)
& accept_population(X1,muslim,n1)
& accept_population(X1,native,n0)
& accept_population(X1,other,n1) )
<=> accept_city(X1,cityb) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_12) ).
fof(a2_11,axiom,
! [X1] :
( ( accept_population(X1,atheist,n70)
& accept_population(X1,christian,n20)
& accept_population(X1,muslim,n8)
& accept_population(X1,native,n0)
& accept_population(X1,other,n2) )
<=> accept_city(X1,townb) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_11) ).
fof(a2_10,axiom,
! [X1] :
( ( accept_population(X1,atheist,n75)
& accept_population(X1,christian,n25)
& accept_population(X1,muslim,n0)
& accept_population(X1,native,n0)
& accept_population(X1,other,n0) )
<=> accept_city(X1,citya) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_10) ).
fof(a2_9,axiom,
! [X1] :
( ( accept_population(X1,atheist,n75)
& accept_population(X1,christian,n24)
& accept_population(X1,muslim,n1)
& accept_population(X1,native,n0)
& accept_population(X1,other,n0) )
<=> accept_city(X1,towna) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_9) ).
fof(a2_8,axiom,
! [X1] :
( ( accept_population(X1,atheist,n0)
& accept_population(X1,christian,n0)
& accept_population(X1,muslim,n0)
& accept_population(X1,native,n100)
& accept_population(X1,other,n0) )
<=> accept_city(X1,sunsetpoint) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_8) ).
fof(a2_7,axiom,
! [X1] :
( ( accept_population(X1,atheist,n12)
& accept_population(X1,christian,n3)
& accept_population(X1,muslim,n0)
& accept_population(X1,native,n85)
& accept_population(X1,other,n0) )
<=> accept_city(X1,coastvillage) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_7) ).
fof(a2_6,axiom,
! [X1] :
( ( accept_population(X1,atheist,n70)
& accept_population(X1,christian,n13)
& accept_population(X1,muslim,n0)
& accept_population(X1,native,n15)
& accept_population(X1,other,n2) )
<=> accept_city(X1,northport) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_6) ).
fof(a2_5,axiom,
! [X1] :
( ( accept_population(X1,atheist,n68)
& accept_population(X1,christian,n16)
& accept_population(X1,muslim,n1)
& accept_population(X1,native,n11)
& accept_population(X1,other,n4) )
<=> accept_city(X1,stjosephburgh) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_5) ).
fof(a2_4,axiom,
! [X1] :
( ( accept_population(X1,atheist,n70)
& accept_population(X1,christian,n15)
& accept_population(X1,muslim,n1)
& accept_population(X1,native,n10)
& accept_population(X1,other,n4) )
<=> accept_city(X1,centrallakecity) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_4) ).
fof(a2_3,axiom,
! [X1] :
( ( accept_population(X1,atheist,n30)
& accept_population(X1,christian,n8)
& accept_population(X1,muslim,n60)
& accept_population(X1,native,n1)
& accept_population(X1,other,n1) )
<=> accept_city(X1,sunnysideport) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_3) ).
fof(a2_2,axiom,
! [X1] :
( ( accept_population(X1,atheist,n54)
& accept_population(X1,christian,n23)
& accept_population(X1,muslim,n3)
& accept_population(X1,native,n1)
& accept_population(X1,other,n9) )
<=> accept_city(X1,centraltown) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_2) ).
fof(a2_1,axiom,
! [X1] :
( ( accept_population(X1,atheist,n65)
& accept_population(X1,christian,n20)
& accept_population(X1,muslim,n7)
& accept_population(X1,native,n4)
& accept_population(X1,other,n4) )
<=> accept_city(X1,suffertown) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_1) ).
fof(a1_1,axiom,
! [X1,X2,X3,X4] :
( accept_team(X1,X4,X2,X3)
<=> ( accept_city(X1,X2)
& accept_leader(X1,X4)
& accept_number(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_1) ).
fof(event_213,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_213) ).
fof(event_212,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_212) ).
fof(event_33,axiom,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_33) ).
fof(event_32,axiom,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_32) ).
fof(event_36,axiom,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_36) ).
fof(event_30,axiom,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_30) ).
fof(event_35,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_35) ).
fof(event_31,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_31) ).
fof(event_34,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_34) ).
fof(event_29,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_29) ).
fof(event_185,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_185) ).
fof(event_174,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_174) ).
fof(event_178,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_178) ).
fof(event_246,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_246) ).
fof(event_10,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_10) ).
fof(event_175,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_175) ).
fof(event_180,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_180) ).
fof(event_9,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_9) ).
fof(event_186,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_186) ).
fof(event_182,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_182) ).
fof(event_177,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_177) ).
fof(event_181,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_181) ).
fof(event_184,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_184) ).
fof(event_187,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_187) ).
fof(event_176,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_176) ).
fof(event_179,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_179) ).
fof(event_116,axiom,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_116) ).
fof(event_216,axiom,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_216) ).
fof(event_119,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_119) ).
fof(event_219,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_219) ).
fof(event_40,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_40) ).
fof(event_115,axiom,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_115) ).
fof(event_117,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_117) ).
fof(event_144,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_144) ).
fof(event_143,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_143) ).
fof(event_217,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_217) ).
fof(event_118,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_118) ).
fof(event_218,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_218) ).
fof(event_72,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_72) ).
fof(event_71,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_71) ).
fof(rdn_positive_less_multi_digit_low,axiom,
! [X10,X14,X12] :
( ( rdn_positive_less(rdnn(X10),rdnn(X12))
& rdn_non_zero(X14) )
=> rdn_positive_less(rdn(rdnn(X10),X14),rdn(rdnn(X12),X14)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_multi_digit_low) ).
fof(a1_6,axiom,
! [X1,X4,X2] :
( the_agent_not_in_any_proposed_teams(X1,X4,X2)
=> ~ ( accept_city(X1,X2)
& accept_leader(X1,X4) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_6) ).
fof(less_successor,axiom,
! [X7,X8,X9] :
( ( sum(X7,n1,X8)
& less(X9,X8) )
=> less_or_equal(X9,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_successor) ).
fof(rdn_positive_less_multi_digit_high,axiom,
! [X10,X11,X12,X13] :
( rdn_positive_less(X11,X13)
=> rdn_positive_less(rdn(rdnn(X10),X11),rdn(rdnn(X12),X13)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_multi_digit_high) ).
fof(rdn_positive_less_transitivity,axiom,
! [X7,X8,X9] :
( ( rdn_positive_less(rdnn(X7),rdnn(X8))
& rdn_positive_less(rdnn(X8),rdnn(X9)) )
=> rdn_positive_less(rdnn(X7),rdnn(X9)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_transitivity) ).
fof(less_entry_point_pos_pos,axiom,
! [X7,X8,X16,X17] :
( ( rdn_translate(X7,rdn_pos(X16))
& rdn_translate(X8,rdn_pos(X17))
& rdn_positive_less(X16,X17) )
=> less(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
fof(less_entry_point_neg_neg,axiom,
! [X7,X8,X16,X17] :
( ( rdn_translate(X7,rdn_neg(X16))
& rdn_translate(X8,rdn_neg(X17))
& rdn_positive_less(X17,X16) )
=> less(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_neg_neg) ).
fof(a1_5,axiom,
! [X1,X4,X2] :
( any_agent_in_all_proposed_teams(X1,X4,X2)
=> accept_leader(X1,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_5) ).
fof(a1_4,axiom,
! [X1,X4,X2] :
( the_agent_in_all_proposed_teams(X1,X4,X2)
=> ( accept_leader(X1,X4)
& accept_city(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_4) ).
fof(less_entry_point_neg_pos,axiom,
! [X7,X8,X16,X17] :
( ( rdn_translate(X7,rdn_neg(X16))
& rdn_translate(X8,rdn_pos(X17)) )
=> less(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_neg_pos) ).
fof(rdn_extra_digits_positive_less,axiom,
! [X15,X12,X13] :
( rdn_non_zero(X13)
=> rdn_positive_less(rdnn(X15),rdn(rdnn(X12),X13)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_extra_digits_positive_less) ).
fof(a1_2,axiom,
! [X1,X3,X5] :
( ( accept_number(X1,X3)
& less(X5,X3) )
=> accept_number(X1,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_2) ).
fof(rdn_non_zero_by_structure,axiom,
! [X15,X14] :
( rdn_non_zero(X14)
=> rdn_non_zero(rdn(rdnn(X15),X14)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_structure) ).
fof(less_or_equal,axiom,
! [X7,X8] :
( less_or_equal(X7,X8)
<=> ( less(X7,X8)
| X7 = X8 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_or_equal) ).
fof(a1_7,axiom,
! [X1,X3] :
( min_number_of_proposed_agents(X1,X3)
=> accept_number(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_7) ).
fof(rdn_non_zero_by_digit,axiom,
! [X7] :
( rdn_non_zero_digit(rdnn(X7))
=> rdn_non_zero(rdnn(X7)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_digit) ).
fof(event_85,axiom,
accept_team(sufferterragovernment,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_85) ).
fof(event_20,axiom,
accept_team(sufferterragovernment,countryacivilorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_20) ).
fof(event_48,axiom,
accept_team(sufferterragovernment,countryacivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_48) ).
fof(event_84,axiom,
accept_team(sufferterragovernment,countryacivilorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_84) ).
fof(event_124,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_124) ).
fof(event_145,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_145) ).
fof(event_83,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_83) ).
fof(event_82,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_82) ).
fof(event_93,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_93) ).
fof(event_19,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_19) ).
fof(event_26,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_26) ).
fof(event_92,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_92) ).
fof(event_125,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_125) ).
fof(event_139,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_139) ).
fof(event_91,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_91) ).
fof(event_90,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_90) ).
fof(event_79,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_79) ).
fof(event_208,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_208) ).
fof(event_44,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_44) ).
fof(event_43,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_43) ).
fof(event_76,axiom,
accept_team(countrybcivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_76) ).
fof(event_77,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_77) ).
fof(event_161,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_161) ).
fof(event_160,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_160) ).
fof(event_18,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_18) ).
fof(event_206,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_206) ).
fof(event_205,axiom,
accept_team(countrybcivilorganization,countryccivilorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_205) ).
fof(event_78,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_78) ).
fof(event_207,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_207) ).
fof(event_75,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_75) ).
fof(event_74,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_74) ).
fof(event_189,axiom,
accept_team(countryamedicalorganization,sufferterragovernment,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_189) ).
fof(event_188,axiom,
accept_team(countryamedicalorganization,sufferterragovernment,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_188) ).
fof(event_14,axiom,
accept_team(countryamedicalorganization,countryacivilorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_14) ).
fof(event_27,axiom,
accept_team(countryamedicalorganization,countryacivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_27) ).
fof(event_126,axiom,
accept_team(countryamedicalorganization,countryahumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_126) ).
fof(event_156,axiom,
accept_team(countryamedicalorganization,countryahumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_156) ).
fof(event_129,axiom,
accept_team(countrycmedicalorganization,countrybcivilorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_129) ).
fof(event_229,axiom,
accept_team(countrycmedicalorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_229) ).
fof(event_128,axiom,
accept_team(countrycmedicalorganization,muslimcountrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_128) ).
fof(event_130,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_130) ).
fof(event_155,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_155) ).
fof(event_154,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_154) ).
fof(event_230,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_230) ).
fof(event_127,axiom,
accept_team(countrycmedicalorganization,countryccivilorganization,townc,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_127) ).
fof(event_228,axiom,
accept_team(countrycmedicalorganization,countryccivilorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_228) ).
fof(event_131,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_131) ).
fof(event_231,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_231) ).
fof(event_96,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_96) ).
fof(event_51,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_51) ).
fof(event_100,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_100) ).
fof(event_103,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_103) ).
fof(event_101,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_101) ).
fof(event_173,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_173) ).
fof(event_172,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_172) ).
fof(event_8,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_8) ).
fof(event_99,axiom,
accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,townc,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_99) ).
fof(event_102,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_102) ).
fof(event_97,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_97) ).
fof(event_13,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_13) ).
fof(event_134,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_134) ).
fof(event_122,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_122) ).
fof(event_198,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_198) ).
fof(event_193,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_193) ).
fof(event_136,axiom,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_136) ).
fof(event_200,axiom,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_200) ).
fof(event_195,axiom,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_195) ).
fof(event_123,axiom,
accept_team(countrybhumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_123) ).
fof(event_196,axiom,
accept_team(countrybhumanitarianorganization,countryccivilorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_196) ).
fof(event_135,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_135) ).
fof(event_199,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_199) ).
fof(event_194,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_194) ).
fof(event_25,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_25) ).
fof(event_24,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_24) ).
fof(event_39,axiom,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_39) ).
fof(event_7,axiom,
accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_7) ).
fof(event_110,axiom,
accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_110) ).
fof(event_238,axiom,
accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_238) ).
fof(event_112,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_112) ).
fof(event_241,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_241) ).
fof(event_55,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_55) ).
fof(event_53,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_53) ).
fof(event_109,axiom,
accept_team(christiancountrychumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_109) ).
fof(event_111,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_111) ).
fof(event_163,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_163) ).
fof(event_162,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_162) ).
fof(event_15,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_15) ).
fof(event_240,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_240) ).
fof(event_108,axiom,
accept_team(christiancountrychumanitarianorganization,countryccivilorganization,townc,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_108) ).
fof(event_236,axiom,
accept_team(christiancountrychumanitarianorganization,countryccivilorganization,towna,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_236) ).
fof(event_153,axiom,
accept_team(countryafirstaidorganization,sufferterragovernment,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_153) ).
fof(event_152,axiom,
accept_team(countryafirstaidorganization,sufferterragovernment,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_152) ).
fof(event_16,axiom,
accept_team(countryafirstaidorganization,countryacivilorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_16) ).
fof(event_58,axiom,
accept_team(countryafirstaidorganization,countryacivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_58) ).
fof(event_68,axiom,
accept_team(countryafirstaidorganization,countryacivilorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_68) ).
fof(event_107,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_107) ).
fof(event_148,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_148) ).
fof(event_67,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_67) ).
fof(event_66,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_66) ).
fof(event_225,axiom,
accept_team(countryacivilorganization,sufferterragovernment,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_225) ).
fof(event_223,axiom,
accept_team(countryacivilorganization,sufferterragovernment,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_223) ).
fof(event_62,axiom,
accept_team(countryacivilorganization,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_62) ).
fof(event_106,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,townc,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_106) ).
fof(event_167,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_167) ).
fof(event_61,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_61) ).
fof(event_60,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_60) ).
fof(event_191,axiom,
accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_191) ).
fof(event_190,axiom,
accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_190) ).
fof(event_4,axiom,
accept_team(countryahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_4) ).
fof(event_1,axiom,
accept_team(countryahumanitarianorganization,countryacivilorganization,cityb,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_1) ).
fof(event_2,axiom,
accept_team(countryahumanitarianorganization,countryacivilorganization,towna,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_2) ).
fof(event_3,axiom,
accept_team(countryahumanitarianorganization,countryacivilorganization,coastvillage,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_3) ).
fof(rdnn128,axiom,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn128) ).
fof(rdnn127,axiom,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn127) ).
fof(rdnn126,axiom,
rdn_translate(nn126,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn126) ).
fof(rdnn125,axiom,
rdn_translate(nn125,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn125) ).
fof(rdnn124,axiom,
rdn_translate(nn124,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn124) ).
fof(rdnn123,axiom,
rdn_translate(nn123,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn123) ).
fof(rdnn122,axiom,
rdn_translate(nn122,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn122) ).
fof(rdnn121,axiom,
rdn_translate(nn121,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn121) ).
fof(rdnn120,axiom,
rdn_translate(nn120,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn120) ).
fof(rdnn119,axiom,
rdn_translate(nn119,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn119) ).
fof(rdnn118,axiom,
rdn_translate(nn118,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn118) ).
fof(rdnn117,axiom,
rdn_translate(nn117,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn117) ).
fof(rdnn116,axiom,
rdn_translate(nn116,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn116) ).
fof(rdnn115,axiom,
rdn_translate(nn115,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn115) ).
fof(rdnn114,axiom,
rdn_translate(nn114,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn114) ).
fof(rdnn113,axiom,
rdn_translate(nn113,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn113) ).
fof(rdnn112,axiom,
rdn_translate(nn112,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn112) ).
fof(rdnn111,axiom,
rdn_translate(nn111,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn111) ).
fof(rdnn110,axiom,
rdn_translate(nn110,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn110) ).
fof(rdnn109,axiom,
rdn_translate(nn109,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn109) ).
fof(rdnn108,axiom,
rdn_translate(nn108,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn108) ).
fof(rdnn107,axiom,
rdn_translate(nn107,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn107) ).
fof(rdnn106,axiom,
rdn_translate(nn106,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn106) ).
fof(rdnn105,axiom,
rdn_translate(nn105,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn105) ).
fof(rdnn104,axiom,
rdn_translate(nn104,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn104) ).
fof(rdnn103,axiom,
rdn_translate(nn103,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn103) ).
fof(rdnn102,axiom,
rdn_translate(nn102,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn102) ).
fof(rdnn101,axiom,
rdn_translate(nn101,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn101) ).
fof(rdnn100,axiom,
rdn_translate(nn100,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn100) ).
fof(rdn127,axiom,
rdn_translate(n127,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn127) ).
fof(rdn126,axiom,
rdn_translate(n126,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn126) ).
fof(rdn125,axiom,
rdn_translate(n125,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn125) ).
fof(rdn124,axiom,
rdn_translate(n124,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn124) ).
fof(rdn123,axiom,
rdn_translate(n123,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn123) ).
fof(rdn122,axiom,
rdn_translate(n122,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn122) ).
fof(rdn121,axiom,
rdn_translate(n121,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn121) ).
fof(rdn120,axiom,
rdn_translate(n120,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn120) ).
fof(rdn119,axiom,
rdn_translate(n119,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn119) ).
fof(rdn118,axiom,
rdn_translate(n118,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn118) ).
fof(rdn117,axiom,
rdn_translate(n117,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn117) ).
fof(rdn116,axiom,
rdn_translate(n116,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn116) ).
fof(rdn115,axiom,
rdn_translate(n115,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn115) ).
fof(rdn114,axiom,
rdn_translate(n114,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn114) ).
fof(rdn113,axiom,
rdn_translate(n113,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn113) ).
fof(rdn112,axiom,
rdn_translate(n112,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn112) ).
fof(rdn111,axiom,
rdn_translate(n111,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn111) ).
fof(rdn110,axiom,
rdn_translate(n110,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn110) ).
fof(rdn109,axiom,
rdn_translate(n109,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn109) ).
fof(rdn108,axiom,
rdn_translate(n108,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn108) ).
fof(rdn107,axiom,
rdn_translate(n107,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn107) ).
fof(rdn106,axiom,
rdn_translate(n106,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn106) ).
fof(rdn105,axiom,
rdn_translate(n105,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn105) ).
fof(rdn104,axiom,
rdn_translate(n104,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn104) ).
fof(rdn103,axiom,
rdn_translate(n103,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn103) ).
fof(rdn102,axiom,
rdn_translate(n102,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn102) ).
fof(rdn101,axiom,
rdn_translate(n101,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn101) ).
fof(rdn100,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(rdnn99,axiom,
rdn_translate(nn99,rdn_neg(rdn(rdnn(n9),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn99) ).
fof(rdnn98,axiom,
rdn_translate(nn98,rdn_neg(rdn(rdnn(n8),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn98) ).
fof(rdnn97,axiom,
rdn_translate(nn97,rdn_neg(rdn(rdnn(n7),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn97) ).
fof(rdnn96,axiom,
rdn_translate(nn96,rdn_neg(rdn(rdnn(n6),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn96) ).
fof(rdnn95,axiom,
rdn_translate(nn95,rdn_neg(rdn(rdnn(n5),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn95) ).
fof(rdnn94,axiom,
rdn_translate(nn94,rdn_neg(rdn(rdnn(n4),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn94) ).
fof(rdnn93,axiom,
rdn_translate(nn93,rdn_neg(rdn(rdnn(n3),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn93) ).
fof(rdnn92,axiom,
rdn_translate(nn92,rdn_neg(rdn(rdnn(n2),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn92) ).
fof(rdnn91,axiom,
rdn_translate(nn91,rdn_neg(rdn(rdnn(n1),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn91) ).
fof(rdnn90,axiom,
rdn_translate(nn90,rdn_neg(rdn(rdnn(n0),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn90) ).
fof(rdnn89,axiom,
rdn_translate(nn89,rdn_neg(rdn(rdnn(n9),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn89) ).
fof(rdnn88,axiom,
rdn_translate(nn88,rdn_neg(rdn(rdnn(n8),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn88) ).
fof(rdnn87,axiom,
rdn_translate(nn87,rdn_neg(rdn(rdnn(n7),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn87) ).
fof(rdnn86,axiom,
rdn_translate(nn86,rdn_neg(rdn(rdnn(n6),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn86) ).
fof(rdnn85,axiom,
rdn_translate(nn85,rdn_neg(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn85) ).
fof(rdnn84,axiom,
rdn_translate(nn84,rdn_neg(rdn(rdnn(n4),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn84) ).
fof(rdnn83,axiom,
rdn_translate(nn83,rdn_neg(rdn(rdnn(n3),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn83) ).
fof(rdnn82,axiom,
rdn_translate(nn82,rdn_neg(rdn(rdnn(n2),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn82) ).
fof(rdnn81,axiom,
rdn_translate(nn81,rdn_neg(rdn(rdnn(n1),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn81) ).
fof(rdnn80,axiom,
rdn_translate(nn80,rdn_neg(rdn(rdnn(n0),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn80) ).
fof(rdnn79,axiom,
rdn_translate(nn79,rdn_neg(rdn(rdnn(n9),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn79) ).
fof(rdnn78,axiom,
rdn_translate(nn78,rdn_neg(rdn(rdnn(n8),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn78) ).
fof(rdnn77,axiom,
rdn_translate(nn77,rdn_neg(rdn(rdnn(n7),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn77) ).
fof(rdnn76,axiom,
rdn_translate(nn76,rdn_neg(rdn(rdnn(n6),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn76) ).
fof(rdnn75,axiom,
rdn_translate(nn75,rdn_neg(rdn(rdnn(n5),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn75) ).
fof(rdnn74,axiom,
rdn_translate(nn74,rdn_neg(rdn(rdnn(n4),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn74) ).
fof(rdnn73,axiom,
rdn_translate(nn73,rdn_neg(rdn(rdnn(n3),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn73) ).
fof(rdnn72,axiom,
rdn_translate(nn72,rdn_neg(rdn(rdnn(n2),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn72) ).
fof(rdnn71,axiom,
rdn_translate(nn71,rdn_neg(rdn(rdnn(n1),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn71) ).
fof(rdnn70,axiom,
rdn_translate(nn70,rdn_neg(rdn(rdnn(n0),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn70) ).
fof(rdnn69,axiom,
rdn_translate(nn69,rdn_neg(rdn(rdnn(n9),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn69) ).
fof(rdnn68,axiom,
rdn_translate(nn68,rdn_neg(rdn(rdnn(n8),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn68) ).
fof(rdnn67,axiom,
rdn_translate(nn67,rdn_neg(rdn(rdnn(n7),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn67) ).
fof(rdnn66,axiom,
rdn_translate(nn66,rdn_neg(rdn(rdnn(n6),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn66) ).
fof(rdnn65,axiom,
rdn_translate(nn65,rdn_neg(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn65) ).
fof(rdnn64,axiom,
rdn_translate(nn64,rdn_neg(rdn(rdnn(n4),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn64) ).
fof(rdnn63,axiom,
rdn_translate(nn63,rdn_neg(rdn(rdnn(n3),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn63) ).
fof(rdnn62,axiom,
rdn_translate(nn62,rdn_neg(rdn(rdnn(n2),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn62) ).
fof(rdnn61,axiom,
rdn_translate(nn61,rdn_neg(rdn(rdnn(n1),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn61) ).
fof(rdnn60,axiom,
rdn_translate(nn60,rdn_neg(rdn(rdnn(n0),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn60) ).
fof(rdnn59,axiom,
rdn_translate(nn59,rdn_neg(rdn(rdnn(n9),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn59) ).
fof(rdnn58,axiom,
rdn_translate(nn58,rdn_neg(rdn(rdnn(n8),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn58) ).
fof(rdnn57,axiom,
rdn_translate(nn57,rdn_neg(rdn(rdnn(n7),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn57) ).
fof(rdnn56,axiom,
rdn_translate(nn56,rdn_neg(rdn(rdnn(n6),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn56) ).
fof(rdnn55,axiom,
rdn_translate(nn55,rdn_neg(rdn(rdnn(n5),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn55) ).
fof(rdnn54,axiom,
rdn_translate(nn54,rdn_neg(rdn(rdnn(n4),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn54) ).
fof(rdnn53,axiom,
rdn_translate(nn53,rdn_neg(rdn(rdnn(n3),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn53) ).
fof(rdnn52,axiom,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn52) ).
fof(rdnn51,axiom,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn51) ).
fof(rdnn50,axiom,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn50) ).
fof(rdnn49,axiom,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn49) ).
fof(rdnn48,axiom,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn48) ).
fof(rdnn47,axiom,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn47) ).
fof(rdnn46,axiom,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn46) ).
fof(rdnn45,axiom,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn45) ).
fof(rdnn44,axiom,
rdn_translate(nn44,rdn_neg(rdn(rdnn(n4),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn44) ).
fof(rdnn43,axiom,
rdn_translate(nn43,rdn_neg(rdn(rdnn(n3),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn43) ).
fof(rdnn42,axiom,
rdn_translate(nn42,rdn_neg(rdn(rdnn(n2),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn42) ).
fof(rdnn41,axiom,
rdn_translate(nn41,rdn_neg(rdn(rdnn(n1),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn41) ).
fof(rdnn40,axiom,
rdn_translate(nn40,rdn_neg(rdn(rdnn(n0),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn40) ).
fof(rdnn39,axiom,
rdn_translate(nn39,rdn_neg(rdn(rdnn(n9),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn39) ).
fof(rdnn38,axiom,
rdn_translate(nn38,rdn_neg(rdn(rdnn(n8),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn38) ).
fof(rdnn37,axiom,
rdn_translate(nn37,rdn_neg(rdn(rdnn(n7),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn37) ).
fof(rdnn36,axiom,
rdn_translate(nn36,rdn_neg(rdn(rdnn(n6),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn36) ).
fof(rdnn35,axiom,
rdn_translate(nn35,rdn_neg(rdn(rdnn(n5),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn35) ).
fof(rdnn34,axiom,
rdn_translate(nn34,rdn_neg(rdn(rdnn(n4),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn34) ).
fof(rdnn33,axiom,
rdn_translate(nn33,rdn_neg(rdn(rdnn(n3),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn33) ).
fof(rdnn32,axiom,
rdn_translate(nn32,rdn_neg(rdn(rdnn(n2),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn32) ).
fof(rdnn31,axiom,
rdn_translate(nn31,rdn_neg(rdn(rdnn(n1),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn31) ).
fof(rdnn30,axiom,
rdn_translate(nn30,rdn_neg(rdn(rdnn(n0),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn30) ).
fof(rdnn29,axiom,
rdn_translate(nn29,rdn_neg(rdn(rdnn(n9),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn29) ).
fof(rdnn28,axiom,
rdn_translate(nn28,rdn_neg(rdn(rdnn(n8),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn28) ).
fof(rdnn27,axiom,
rdn_translate(nn27,rdn_neg(rdn(rdnn(n7),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn27) ).
fof(rdnn26,axiom,
rdn_translate(nn26,rdn_neg(rdn(rdnn(n6),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn26) ).
fof(rdnn25,axiom,
rdn_translate(nn25,rdn_neg(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn25) ).
fof(rdnn24,axiom,
rdn_translate(nn24,rdn_neg(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn24) ).
fof(rdnn23,axiom,
rdn_translate(nn23,rdn_neg(rdn(rdnn(n3),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn23) ).
fof(rdnn22,axiom,
rdn_translate(nn22,rdn_neg(rdn(rdnn(n2),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn22) ).
fof(rdnn21,axiom,
rdn_translate(nn21,rdn_neg(rdn(rdnn(n1),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn21) ).
fof(rdnn20,axiom,
rdn_translate(nn20,rdn_neg(rdn(rdnn(n0),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn20) ).
fof(rdnn19,axiom,
rdn_translate(nn19,rdn_neg(rdn(rdnn(n9),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn19) ).
fof(rdnn18,axiom,
rdn_translate(nn18,rdn_neg(rdn(rdnn(n8),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn18) ).
fof(rdnn17,axiom,
rdn_translate(nn17,rdn_neg(rdn(rdnn(n7),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn17) ).
fof(rdnn16,axiom,
rdn_translate(nn16,rdn_neg(rdn(rdnn(n6),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn16) ).
fof(rdnn15,axiom,
rdn_translate(nn15,rdn_neg(rdn(rdnn(n5),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn15) ).
fof(rdnn14,axiom,
rdn_translate(nn14,rdn_neg(rdn(rdnn(n4),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn14) ).
fof(rdnn13,axiom,
rdn_translate(nn13,rdn_neg(rdn(rdnn(n3),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn13) ).
fof(rdnn12,axiom,
rdn_translate(nn12,rdn_neg(rdn(rdnn(n2),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn12) ).
fof(rdnn11,axiom,
rdn_translate(nn11,rdn_neg(rdn(rdnn(n1),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn11) ).
fof(rdnn10,axiom,
rdn_translate(nn10,rdn_neg(rdn(rdnn(n0),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn10) ).
fof(rdn99,axiom,
rdn_translate(n99,rdn_pos(rdn(rdnn(n9),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn99) ).
fof(rdn98,axiom,
rdn_translate(n98,rdn_pos(rdn(rdnn(n8),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn98) ).
fof(rdn97,axiom,
rdn_translate(n97,rdn_pos(rdn(rdnn(n7),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn97) ).
fof(rdn96,axiom,
rdn_translate(n96,rdn_pos(rdn(rdnn(n6),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn96) ).
fof(rdn95,axiom,
rdn_translate(n95,rdn_pos(rdn(rdnn(n5),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn95) ).
fof(rdn94,axiom,
rdn_translate(n94,rdn_pos(rdn(rdnn(n4),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn94) ).
fof(rdn93,axiom,
rdn_translate(n93,rdn_pos(rdn(rdnn(n3),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn93) ).
fof(rdn92,axiom,
rdn_translate(n92,rdn_pos(rdn(rdnn(n2),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn92) ).
fof(rdn91,axiom,
rdn_translate(n91,rdn_pos(rdn(rdnn(n1),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn91) ).
fof(rdn90,axiom,
rdn_translate(n90,rdn_pos(rdn(rdnn(n0),rdnn(n9)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn90) ).
fof(rdn89,axiom,
rdn_translate(n89,rdn_pos(rdn(rdnn(n9),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn89) ).
fof(rdn88,axiom,
rdn_translate(n88,rdn_pos(rdn(rdnn(n8),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn88) ).
fof(rdn87,axiom,
rdn_translate(n87,rdn_pos(rdn(rdnn(n7),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn87) ).
fof(rdn86,axiom,
rdn_translate(n86,rdn_pos(rdn(rdnn(n6),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn86) ).
fof(rdn84,axiom,
rdn_translate(n84,rdn_pos(rdn(rdnn(n4),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn84) ).
fof(rdn83,axiom,
rdn_translate(n83,rdn_pos(rdn(rdnn(n3),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn83) ).
fof(rdn82,axiom,
rdn_translate(n82,rdn_pos(rdn(rdnn(n2),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn82) ).
fof(rdn81,axiom,
rdn_translate(n81,rdn_pos(rdn(rdnn(n1),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn81) ).
fof(rdn80,axiom,
rdn_translate(n80,rdn_pos(rdn(rdnn(n0),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn80) ).
fof(rdn79,axiom,
rdn_translate(n79,rdn_pos(rdn(rdnn(n9),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn79) ).
fof(rdn77,axiom,
rdn_translate(n77,rdn_pos(rdn(rdnn(n7),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn77) ).
fof(rdn76,axiom,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn76) ).
fof(rdn74,axiom,
rdn_translate(n74,rdn_pos(rdn(rdnn(n4),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn74) ).
fof(rdn73,axiom,
rdn_translate(n73,rdn_pos(rdn(rdnn(n3),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn73) ).
fof(rdn72,axiom,
rdn_translate(n72,rdn_pos(rdn(rdnn(n2),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn72) ).
fof(rdn71,axiom,
rdn_translate(n71,rdn_pos(rdn(rdnn(n1),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn71) ).
fof(rdn69,axiom,
rdn_translate(n69,rdn_pos(rdn(rdnn(n9),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn69) ).
fof(rdn67,axiom,
rdn_translate(n67,rdn_pos(rdn(rdnn(n7),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn67) ).
fof(rdn66,axiom,
rdn_translate(n66,rdn_pos(rdn(rdnn(n6),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn66) ).
fof(rdn64,axiom,
rdn_translate(n64,rdn_pos(rdn(rdnn(n4),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn64) ).
fof(rdn63,axiom,
rdn_translate(n63,rdn_pos(rdn(rdnn(n3),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn63) ).
fof(rdn62,axiom,
rdn_translate(n62,rdn_pos(rdn(rdnn(n2),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn62) ).
fof(rdn61,axiom,
rdn_translate(n61,rdn_pos(rdn(rdnn(n1),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn61) ).
fof(rdn59,axiom,
rdn_translate(n59,rdn_pos(rdn(rdnn(n9),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn59) ).
fof(rdn58,axiom,
rdn_translate(n58,rdn_pos(rdn(rdnn(n8),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn58) ).
fof(rdn57,axiom,
rdn_translate(n57,rdn_pos(rdn(rdnn(n7),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn57) ).
fof(rdn56,axiom,
rdn_translate(n56,rdn_pos(rdn(rdnn(n6),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn56) ).
fof(rdn55,axiom,
rdn_translate(n55,rdn_pos(rdn(rdnn(n5),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn55) ).
fof(rdn53,axiom,
rdn_translate(n53,rdn_pos(rdn(rdnn(n3),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn53) ).
fof(rdn52,axiom,
rdn_translate(n52,rdn_pos(rdn(rdnn(n2),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn52) ).
fof(rdn51,axiom,
rdn_translate(n51,rdn_pos(rdn(rdnn(n1),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn51) ).
fof(rdn50,axiom,
rdn_translate(n50,rdn_pos(rdn(rdnn(n0),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn50) ).
fof(rdn49,axiom,
rdn_translate(n49,rdn_pos(rdn(rdnn(n9),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn49) ).
fof(rdn48,axiom,
rdn_translate(n48,rdn_pos(rdn(rdnn(n8),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn48) ).
fof(rdn47,axiom,
rdn_translate(n47,rdn_pos(rdn(rdnn(n7),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn47) ).
fof(rdn46,axiom,
rdn_translate(n46,rdn_pos(rdn(rdnn(n6),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn46) ).
fof(rdn45,axiom,
rdn_translate(n45,rdn_pos(rdn(rdnn(n5),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn45) ).
fof(rdn44,axiom,
rdn_translate(n44,rdn_pos(rdn(rdnn(n4),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn44) ).
fof(rdn43,axiom,
rdn_translate(n43,rdn_pos(rdn(rdnn(n3),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn43) ).
fof(rdn42,axiom,
rdn_translate(n42,rdn_pos(rdn(rdnn(n2),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn42) ).
fof(rdn41,axiom,
rdn_translate(n41,rdn_pos(rdn(rdnn(n1),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn41) ).
fof(rdn40,axiom,
rdn_translate(n40,rdn_pos(rdn(rdnn(n0),rdnn(n4)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn40) ).
fof(rdn39,axiom,
rdn_translate(n39,rdn_pos(rdn(rdnn(n9),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn39) ).
fof(rdn38,axiom,
rdn_translate(n38,rdn_pos(rdn(rdnn(n8),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn38) ).
fof(rdn37,axiom,
rdn_translate(n37,rdn_pos(rdn(rdnn(n7),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn37) ).
fof(rdn36,axiom,
rdn_translate(n36,rdn_pos(rdn(rdnn(n6),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn36) ).
fof(rdn35,axiom,
rdn_translate(n35,rdn_pos(rdn(rdnn(n5),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn35) ).
fof(rdn34,axiom,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn34) ).
fof(rdn33,axiom,
rdn_translate(n33,rdn_pos(rdn(rdnn(n3),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn33) ).
fof(rdn32,axiom,
rdn_translate(n32,rdn_pos(rdn(rdnn(n2),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn32) ).
fof(rdn31,axiom,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn31) ).
fof(rdn29,axiom,
rdn_translate(n29,rdn_pos(rdn(rdnn(n9),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn29) ).
fof(rdn28,axiom,
rdn_translate(n28,rdn_pos(rdn(rdnn(n8),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn28) ).
fof(rdn27,axiom,
rdn_translate(n27,rdn_pos(rdn(rdnn(n7),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn27) ).
fof(rdn26,axiom,
rdn_translate(n26,rdn_pos(rdn(rdnn(n6),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn26) ).
fof(rdn22,axiom,
rdn_translate(n22,rdn_pos(rdn(rdnn(n2),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn22) ).
fof(rdn21,axiom,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn21) ).
fof(rdn19,axiom,
rdn_translate(n19,rdn_pos(rdn(rdnn(n9),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn19) ).
fof(rdn18,axiom,
rdn_translate(n18,rdn_pos(rdn(rdnn(n8),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn18) ).
fof(rdn17,axiom,
rdn_translate(n17,rdn_pos(rdn(rdnn(n7),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn17) ).
fof(rdn14,axiom,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn14) ).
fof(rdn78,axiom,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn78) ).
fof(rdn25,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn25) ).
fof(rdn24,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn24) ).
fof(rdn75,axiom,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn75) ).
fof(rdn85,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn85) ).
fof(rdn12,axiom,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn12) ).
fof(rdn13,axiom,
rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn13) ).
fof(rdn11,axiom,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn11) ).
fof(rdn16,axiom,
rdn_translate(n16,rdn_pos(rdn(rdnn(n6),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn16) ).
fof(rdn68,axiom,
rdn_translate(n68,rdn_pos(rdn(rdnn(n8),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn68) ).
fof(rdn10,axiom,
rdn_translate(n10,rdn_pos(rdn(rdnn(n0),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn10) ).
fof(rdn15,axiom,
rdn_translate(n15,rdn_pos(rdn(rdnn(n5),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn15) ).
fof(rdn70,axiom,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn70) ).
fof(rdn60,axiom,
rdn_translate(n60,rdn_pos(rdn(rdnn(n0),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn60) ).
fof(rdn30,axiom,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn30) ).
fof(rdn23,axiom,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn23) ).
fof(rdn54,axiom,
rdn_translate(n54,rdn_pos(rdn(rdnn(n4),rdnn(n5)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn54) ).
fof(rdn20,axiom,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn20) ).
fof(rdn65,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn65) ).
fof(event_37,axiom,
the_agent_not_in_any_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_37) ).
fof(event_248,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_248) ).
fof(event_11,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_11) ).
fof(event_147,axiom,
any_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_147) ).
fof(event_87,axiom,
any_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_87) ).
fof(event_142,axiom,
any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_142) ).
fof(event_95,axiom,
any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_95) ).
fof(event_210,axiom,
any_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_210) ).
fof(event_47,axiom,
any_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_47) ).
fof(event_81,axiom,
any_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_81) ).
fof(event_159,axiom,
any_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_159) ).
fof(event_38,axiom,
any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_38) ).
fof(event_233,axiom,
any_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_233) ).
fof(event_50,axiom,
any_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_50) ).
fof(event_133,axiom,
any_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_133) ).
fof(event_249,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_249) ).
fof(event_12,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_12) ).
fof(event_105,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_105) ).
fof(event_202,axiom,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_202) ).
fof(event_23,axiom,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_23) ).
fof(event_138,axiom,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_138) ).
fof(event_221,axiom,
any_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_221) ).
fof(event_42,axiom,
any_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_42) ).
fof(event_121,axiom,
any_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_121) ).
fof(event_244,axiom,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_244) ).
fof(event_57,axiom,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_57) ).
fof(event_114,axiom,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_114) ).
fof(event_151,axiom,
any_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_151) ).
fof(event_70,axiom,
any_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_70) ).
fof(event_170,axiom,
any_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_170) ).
fof(event_64,axiom,
any_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_64) ).
fof(event_165,axiom,
any_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_165) ).
fof(event_6,axiom,
any_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_6) ).
fof(event_146,axiom,
the_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_146) ).
fof(event_86,axiom,
the_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_86) ).
fof(event_141,axiom,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_141) ).
fof(event_94,axiom,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_94) ).
fof(event_209,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_209) ).
fof(event_46,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_46) ).
fof(event_80,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_80) ).
fof(event_158,axiom,
the_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_158) ).
fof(event_232,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_232) ).
fof(event_49,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_49) ).
fof(event_132,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_132) ).
fof(event_104,axiom,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_104) ).
fof(event_201,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_201) ).
fof(event_22,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_22) ).
fof(event_137,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_137) ).
fof(event_220,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_220) ).
fof(event_41,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_41) ).
fof(event_120,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_120) ).
fof(event_243,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_243) ).
fof(event_56,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_56) ).
fof(event_113,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_113) ).
fof(event_150,axiom,
the_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_150) ).
fof(event_69,axiom,
the_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_69) ).
fof(event_169,axiom,
the_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_169) ).
fof(event_63,axiom,
the_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_63) ).
fof(event_164,axiom,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_164) ).
fof(event_5,axiom,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_5) ).
fof(rdnn9,axiom,
rdn_translate(nn9,rdn_neg(rdnn(n9))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn9) ).
fof(rdnn8,axiom,
rdn_translate(nn8,rdn_neg(rdnn(n8))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn8) ).
fof(rdnn7,axiom,
rdn_translate(nn7,rdn_neg(rdnn(n7))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn7) ).
fof(rdnn6,axiom,
rdn_translate(nn6,rdn_neg(rdnn(n6))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn6) ).
fof(rdnn5,axiom,
rdn_translate(nn5,rdn_neg(rdnn(n5))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn5) ).
fof(rdnn4,axiom,
rdn_translate(nn4,rdn_neg(rdnn(n4))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn4) ).
fof(rdnn3,axiom,
rdn_translate(nn3,rdn_neg(rdnn(n3))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn3) ).
fof(rdnn2,axiom,
rdn_translate(nn2,rdn_neg(rdnn(n2))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn2) ).
fof(rdnn1,axiom,
rdn_translate(nn1,rdn_neg(rdnn(n1))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdnn1) ).
fof(rdn6,axiom,
rdn_translate(n6,rdn_pos(rdnn(n6))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn6) ).
fof(rdn5,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn5) ).
fof(rdn2,axiom,
rdn_translate(n2,rdn_pos(rdnn(n2))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn2) ).
fof(rdn0,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn0) ).
fof(rdn8,axiom,
rdn_translate(n8,rdn_pos(rdnn(n8))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn8) ).
fof(rdn9,axiom,
rdn_translate(n9,rdn_pos(rdnn(n9))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn9) ).
fof(rdn1,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn1) ).
fof(rdn3,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn3) ).
fof(rdn4,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn4) ).
fof(rdn7,axiom,
rdn_translate(n7,rdn_pos(rdnn(n7))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn7) ).
fof(rdn_positive_less67,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less67) ).
fof(rdn_positive_less56,axiom,
rdn_positive_less(rdnn(n5),rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less56) ).
fof(rdn_positive_less23,axiom,
rdn_positive_less(rdnn(n2),rdnn(n3)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less23) ).
fof(rdn_positive_less01,axiom,
rdn_positive_less(rdnn(n0),rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less01) ).
fof(rdn_positive_less89,axiom,
rdn_positive_less(rdnn(n8),rdnn(n9)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less89) ).
fof(rdn_positive_less12,axiom,
rdn_positive_less(rdnn(n1),rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less12) ).
fof(rdn_positive_less34,axiom,
rdn_positive_less(rdnn(n3),rdnn(n4)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less34) ).
fof(rdn_positive_less45,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less45) ).
fof(rdn_positive_less78,axiom,
rdn_positive_less(rdnn(n7),rdnn(n8)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less78) ).
fof(event_224,axiom,
accept_number(sufferterragovernment,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_224) ).
fof(event_222,axiom,
accept_number(sufferterragovernment,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_222) ).
fof(event_211,axiom,
accept_number(sufferterragovernment,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_211) ).
fof(event_140,axiom,
accept_number(christiansufferterrahumanitarianorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_140) ).
fof(event_88,axiom,
accept_number(christiansufferterrahumanitarianorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_88) ).
fof(event_237,axiom,
accept_number(countrybcivilorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_237) ).
fof(event_45,axiom,
accept_number(countrybcivilorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_45) ).
fof(event_203,axiom,
accept_number(countrybcivilorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_203) ).
fof(event_204,axiom,
accept_number(countrybcivilorganization,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_204) ).
fof(event_157,axiom,
accept_number(countryamedicalorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_157) ).
fof(event_245,axiom,
accept_number(countrycmedicalorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_245) ).
fof(event_54,axiom,
accept_number(countrycmedicalorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_54) ).
fof(event_226,axiom,
accept_number(countrycmedicalorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_226) ).
fof(event_227,axiom,
accept_number(countrycmedicalorganization,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_227) ).
fof(event_52,axiom,
accept_number(countrycmedicalorganization,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_52) ).
fof(event_247,axiom,
accept_number(muslimcountrybhumanitarianorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_247) ).
fof(event_183,axiom,
accept_number(muslimcountrybhumanitarianorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_183) ).
fof(event_98,axiom,
accept_number(muslimcountrybhumanitarianorganization,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_98) ).
fof(event_239,axiom,
accept_number(countrybhumanitarianorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_239) ).
fof(event_171,axiom,
accept_number(countrybhumanitarianorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_171) ).
fof(event_197,axiom,
accept_number(countrybhumanitarianorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_197) ).
fof(event_21,axiom,
accept_number(countrybhumanitarianorganization,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_21) ).
fof(event_17,axiom,
accept_number(countrybhumanitarianorganization,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_17) ).
fof(event_214,axiom,
accept_number(countryccivilorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_214) ).
fof(event_215,axiom,
accept_number(countryccivilorganization,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_215) ).
fof(event_235,axiom,
accept_number(countryccivilorganization,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_235) ).
fof(event_242,axiom,
accept_number(christiancountrychumanitarianorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_242) ).
fof(event_73,axiom,
accept_number(christiancountrychumanitarianorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_73) ).
fof(event_192,axiom,
accept_number(christiancountrychumanitarianorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_192) ).
fof(event_234,axiom,
accept_number(christiancountrychumanitarianorganization,n3),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_234) ).
fof(event_149,axiom,
accept_number(countryafirstaidorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_149) ).
fof(event_65,axiom,
accept_number(countryafirstaidorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_65) ).
fof(event_168,axiom,
accept_number(countryacivilorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_168) ).
fof(event_59,axiom,
accept_number(countryacivilorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_59) ).
fof(event_166,axiom,
accept_number(countryahumanitarianorganization,n6),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_166) ).
fof(event_89,axiom,
accept_number(countryahumanitarianorganization,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_89) ).
fof(event_28,axiom,
accept_number(countryahumanitarianorganization,n2),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_28) ).
fof(rdn_digit6,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit6) ).
fof(rdn_digit5,axiom,
rdn_non_zero_digit(rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit5) ).
fof(rdn_digit2,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit2) ).
fof(rdn_digit8,axiom,
rdn_non_zero_digit(rdnn(n8)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit8) ).
fof(rdn_digit9,axiom,
rdn_non_zero_digit(rdnn(n9)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit9) ).
fof(rdn_digit1,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit1) ).
fof(rdn_digit3,axiom,
rdn_non_zero_digit(rdnn(n3)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit3) ).
fof(rdn_digit4,axiom,
rdn_non_zero_digit(rdnn(n4)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit4) ).
fof(rdn_digit7,axiom,
rdn_non_zero_digit(rdnn(n7)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit7) ).
fof(i_0_555,negated_conjecture,
~ ? [X7,X8,X9] : ~ accept_population(X7,X8,X9),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[query_14])]) ).
fof(i_0_556,plain,
! [X7,X8] :
( less(X7,X8)
<=> ( ~ less(X8,X7)
& X8 != X7 ) ),
inference(fof_simplification,[status(thm)],[less_property]) ).
fof(i_0_557,plain,
! [X125] :
( ( ~ accept_population(X125,atheist,n30)
| ~ accept_population(X125,christian,n0)
| ~ accept_population(X125,muslim,n65)
| ~ accept_population(X125,native,n0)
| ~ accept_population(X125,other,n5)
| accept_city(X125,townc) )
& ( accept_population(X125,atheist,n30)
| ~ accept_city(X125,townc) )
& ( accept_population(X125,christian,n0)
| ~ accept_city(X125,townc) )
& ( accept_population(X125,muslim,n65)
| ~ accept_city(X125,townc) )
& ( accept_population(X125,native,n0)
| ~ accept_city(X125,townc) )
& ( accept_population(X125,other,n5)
| ~ accept_city(X125,townc) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_13])])]) ).
fof(i_0_558,negated_conjecture,
! [X161,X162,X163] : accept_population(X161,X162,X163),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_555])]) ).
fof(i_0_559,plain,
! [X124] :
( ( ~ accept_population(X124,atheist,n78)
| ~ accept_population(X124,christian,n20)
| ~ accept_population(X124,muslim,n1)
| ~ accept_population(X124,native,n0)
| ~ accept_population(X124,other,n1)
| accept_city(X124,cityb) )
& ( accept_population(X124,atheist,n78)
| ~ accept_city(X124,cityb) )
& ( accept_population(X124,christian,n20)
| ~ accept_city(X124,cityb) )
& ( accept_population(X124,muslim,n1)
| ~ accept_city(X124,cityb) )
& ( accept_population(X124,native,n0)
| ~ accept_city(X124,cityb) )
& ( accept_population(X124,other,n1)
| ~ accept_city(X124,cityb) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_12])])]) ).
fof(i_0_560,plain,
! [X123] :
( ( ~ accept_population(X123,atheist,n70)
| ~ accept_population(X123,christian,n20)
| ~ accept_population(X123,muslim,n8)
| ~ accept_population(X123,native,n0)
| ~ accept_population(X123,other,n2)
| accept_city(X123,townb) )
& ( accept_population(X123,atheist,n70)
| ~ accept_city(X123,townb) )
& ( accept_population(X123,christian,n20)
| ~ accept_city(X123,townb) )
& ( accept_population(X123,muslim,n8)
| ~ accept_city(X123,townb) )
& ( accept_population(X123,native,n0)
| ~ accept_city(X123,townb) )
& ( accept_population(X123,other,n2)
| ~ accept_city(X123,townb) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_11])])]) ).
fof(i_0_561,plain,
! [X122] :
( ( ~ accept_population(X122,atheist,n75)
| ~ accept_population(X122,christian,n25)
| ~ accept_population(X122,muslim,n0)
| ~ accept_population(X122,native,n0)
| ~ accept_population(X122,other,n0)
| accept_city(X122,citya) )
& ( accept_population(X122,atheist,n75)
| ~ accept_city(X122,citya) )
& ( accept_population(X122,christian,n25)
| ~ accept_city(X122,citya) )
& ( accept_population(X122,muslim,n0)
| ~ accept_city(X122,citya) )
& ( accept_population(X122,native,n0)
| ~ accept_city(X122,citya) )
& ( accept_population(X122,other,n0)
| ~ accept_city(X122,citya) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_10])])]) ).
fof(i_0_562,plain,
! [X121] :
( ( ~ accept_population(X121,atheist,n75)
| ~ accept_population(X121,christian,n24)
| ~ accept_population(X121,muslim,n1)
| ~ accept_population(X121,native,n0)
| ~ accept_population(X121,other,n0)
| accept_city(X121,towna) )
& ( accept_population(X121,atheist,n75)
| ~ accept_city(X121,towna) )
& ( accept_population(X121,christian,n24)
| ~ accept_city(X121,towna) )
& ( accept_population(X121,muslim,n1)
| ~ accept_city(X121,towna) )
& ( accept_population(X121,native,n0)
| ~ accept_city(X121,towna) )
& ( accept_population(X121,other,n0)
| ~ accept_city(X121,towna) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_9])])]) ).
fof(i_0_563,plain,
! [X120] :
( ( ~ accept_population(X120,atheist,n0)
| ~ accept_population(X120,christian,n0)
| ~ accept_population(X120,muslim,n0)
| ~ accept_population(X120,native,n100)
| ~ accept_population(X120,other,n0)
| accept_city(X120,sunsetpoint) )
& ( accept_population(X120,atheist,n0)
| ~ accept_city(X120,sunsetpoint) )
& ( accept_population(X120,christian,n0)
| ~ accept_city(X120,sunsetpoint) )
& ( accept_population(X120,muslim,n0)
| ~ accept_city(X120,sunsetpoint) )
& ( accept_population(X120,native,n100)
| ~ accept_city(X120,sunsetpoint) )
& ( accept_population(X120,other,n0)
| ~ accept_city(X120,sunsetpoint) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_8])])]) ).
fof(i_0_564,plain,
! [X119] :
( ( ~ accept_population(X119,atheist,n12)
| ~ accept_population(X119,christian,n3)
| ~ accept_population(X119,muslim,n0)
| ~ accept_population(X119,native,n85)
| ~ accept_population(X119,other,n0)
| accept_city(X119,coastvillage) )
& ( accept_population(X119,atheist,n12)
| ~ accept_city(X119,coastvillage) )
& ( accept_population(X119,christian,n3)
| ~ accept_city(X119,coastvillage) )
& ( accept_population(X119,muslim,n0)
| ~ accept_city(X119,coastvillage) )
& ( accept_population(X119,native,n85)
| ~ accept_city(X119,coastvillage) )
& ( accept_population(X119,other,n0)
| ~ accept_city(X119,coastvillage) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_7])])]) ).
fof(i_0_565,plain,
! [X118] :
( ( ~ accept_population(X118,atheist,n70)
| ~ accept_population(X118,christian,n13)
| ~ accept_population(X118,muslim,n0)
| ~ accept_population(X118,native,n15)
| ~ accept_population(X118,other,n2)
| accept_city(X118,northport) )
& ( accept_population(X118,atheist,n70)
| ~ accept_city(X118,northport) )
& ( accept_population(X118,christian,n13)
| ~ accept_city(X118,northport) )
& ( accept_population(X118,muslim,n0)
| ~ accept_city(X118,northport) )
& ( accept_population(X118,native,n15)
| ~ accept_city(X118,northport) )
& ( accept_population(X118,other,n2)
| ~ accept_city(X118,northport) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_6])])]) ).
fof(i_0_566,plain,
! [X117] :
( ( ~ accept_population(X117,atheist,n68)
| ~ accept_population(X117,christian,n16)
| ~ accept_population(X117,muslim,n1)
| ~ accept_population(X117,native,n11)
| ~ accept_population(X117,other,n4)
| accept_city(X117,stjosephburgh) )
& ( accept_population(X117,atheist,n68)
| ~ accept_city(X117,stjosephburgh) )
& ( accept_population(X117,christian,n16)
| ~ accept_city(X117,stjosephburgh) )
& ( accept_population(X117,muslim,n1)
| ~ accept_city(X117,stjosephburgh) )
& ( accept_population(X117,native,n11)
| ~ accept_city(X117,stjosephburgh) )
& ( accept_population(X117,other,n4)
| ~ accept_city(X117,stjosephburgh) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_5])])]) ).
fof(i_0_567,plain,
! [X116] :
( ( ~ accept_population(X116,atheist,n70)
| ~ accept_population(X116,christian,n15)
| ~ accept_population(X116,muslim,n1)
| ~ accept_population(X116,native,n10)
| ~ accept_population(X116,other,n4)
| accept_city(X116,centrallakecity) )
& ( accept_population(X116,atheist,n70)
| ~ accept_city(X116,centrallakecity) )
& ( accept_population(X116,christian,n15)
| ~ accept_city(X116,centrallakecity) )
& ( accept_population(X116,muslim,n1)
| ~ accept_city(X116,centrallakecity) )
& ( accept_population(X116,native,n10)
| ~ accept_city(X116,centrallakecity) )
& ( accept_population(X116,other,n4)
| ~ accept_city(X116,centrallakecity) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_4])])]) ).
fof(i_0_568,plain,
! [X115] :
( ( ~ accept_population(X115,atheist,n30)
| ~ accept_population(X115,christian,n8)
| ~ accept_population(X115,muslim,n60)
| ~ accept_population(X115,native,n1)
| ~ accept_population(X115,other,n1)
| accept_city(X115,sunnysideport) )
& ( accept_population(X115,atheist,n30)
| ~ accept_city(X115,sunnysideport) )
& ( accept_population(X115,christian,n8)
| ~ accept_city(X115,sunnysideport) )
& ( accept_population(X115,muslim,n60)
| ~ accept_city(X115,sunnysideport) )
& ( accept_population(X115,native,n1)
| ~ accept_city(X115,sunnysideport) )
& ( accept_population(X115,other,n1)
| ~ accept_city(X115,sunnysideport) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_3])])]) ).
fof(i_0_569,plain,
! [X114] :
( ( ~ accept_population(X114,atheist,n54)
| ~ accept_population(X114,christian,n23)
| ~ accept_population(X114,muslim,n3)
| ~ accept_population(X114,native,n1)
| ~ accept_population(X114,other,n9)
| accept_city(X114,centraltown) )
& ( accept_population(X114,atheist,n54)
| ~ accept_city(X114,centraltown) )
& ( accept_population(X114,christian,n23)
| ~ accept_city(X114,centraltown) )
& ( accept_population(X114,muslim,n3)
| ~ accept_city(X114,centraltown) )
& ( accept_population(X114,native,n1)
| ~ accept_city(X114,centraltown) )
& ( accept_population(X114,other,n9)
| ~ accept_city(X114,centraltown) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_2])])]) ).
fof(i_0_570,plain,
! [X113] :
( ( ~ accept_population(X113,atheist,n65)
| ~ accept_population(X113,christian,n20)
| ~ accept_population(X113,muslim,n7)
| ~ accept_population(X113,native,n4)
| ~ accept_population(X113,other,n4)
| accept_city(X113,suffertown) )
& ( accept_population(X113,atheist,n65)
| ~ accept_city(X113,suffertown) )
& ( accept_population(X113,christian,n20)
| ~ accept_city(X113,suffertown) )
& ( accept_population(X113,muslim,n7)
| ~ accept_city(X113,suffertown) )
& ( accept_population(X113,native,n4)
| ~ accept_city(X113,suffertown) )
& ( accept_population(X113,other,n4)
| ~ accept_city(X113,suffertown) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_1])])]) ).
fof(i_0_571,plain,
! [X91,X92,X93,X94] :
( ( accept_city(X91,X92)
| ~ accept_team(X91,X94,X92,X93) )
& ( accept_leader(X91,X94)
| ~ accept_team(X91,X94,X92,X93) )
& ( accept_number(X91,X93)
| ~ accept_team(X91,X94,X92,X93) )
& ( ~ accept_city(X91,X92)
| ~ accept_leader(X91,X94)
| ~ accept_number(X91,X93)
| accept_team(X91,X94,X92,X93) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_1])])]) ).
fof(i_0_572,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
inference(fof_simplification,[status(thm)],[event_213]) ).
fof(i_0_573,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
inference(fof_simplification,[status(thm)],[event_212]) ).
fof(i_0_574,plain,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
inference(fof_simplification,[status(thm)],[event_33]) ).
fof(i_0_575,plain,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
inference(fof_simplification,[status(thm)],[event_32]) ).
fof(i_0_576,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
inference(fof_simplification,[status(thm)],[event_36]) ).
fof(i_0_577,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
inference(fof_simplification,[status(thm)],[event_30]) ).
fof(i_0_578,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
inference(fof_simplification,[status(thm)],[event_35]) ).
fof(i_0_579,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
inference(fof_simplification,[status(thm)],[event_31]) ).
fof(i_0_580,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
inference(fof_simplification,[status(thm)],[event_34]) ).
fof(i_0_581,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
inference(fof_simplification,[status(thm)],[event_29]) ).
fof(i_0_582,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_185]) ).
fof(i_0_583,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
inference(fof_simplification,[status(thm)],[event_174]) ).
fof(i_0_584,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
inference(fof_simplification,[status(thm)],[event_178]) ).
fof(i_0_585,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_246]) ).
fof(i_0_586,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
inference(fof_simplification,[status(thm)],[event_10]) ).
fof(i_0_587,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
inference(fof_simplification,[status(thm)],[event_175]) ).
fof(i_0_588,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
inference(fof_simplification,[status(thm)],[event_180]) ).
fof(i_0_589,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
inference(fof_simplification,[status(thm)],[event_9]) ).
fof(i_0_590,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_186]) ).
fof(i_0_591,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
inference(fof_simplification,[status(thm)],[event_182]) ).
fof(i_0_592,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
inference(fof_simplification,[status(thm)],[event_177]) ).
fof(i_0_593,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
inference(fof_simplification,[status(thm)],[event_181]) ).
fof(i_0_594,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
inference(fof_simplification,[status(thm)],[event_184]) ).
fof(i_0_595,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_187]) ).
fof(i_0_596,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
inference(fof_simplification,[status(thm)],[event_176]) ).
fof(i_0_597,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
inference(fof_simplification,[status(thm)],[event_179]) ).
fof(i_0_598,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
inference(fof_simplification,[status(thm)],[event_116]) ).
fof(i_0_599,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_216]) ).
fof(i_0_600,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
inference(fof_simplification,[status(thm)],[event_119]) ).
fof(i_0_601,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_219]) ).
fof(i_0_602,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
inference(fof_simplification,[status(thm)],[event_40]) ).
fof(i_0_603,plain,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(fof_simplification,[status(thm)],[event_115]) ).
fof(i_0_604,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
inference(fof_simplification,[status(thm)],[event_117]) ).
fof(i_0_605,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
inference(fof_simplification,[status(thm)],[event_144]) ).
fof(i_0_606,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
inference(fof_simplification,[status(thm)],[event_143]) ).
fof(i_0_607,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_217]) ).
fof(i_0_608,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
inference(fof_simplification,[status(thm)],[event_118]) ).
fof(i_0_609,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
inference(fof_simplification,[status(thm)],[event_218]) ).
fof(i_0_610,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(fof_simplification,[status(thm)],[event_72]) ).
fof(i_0_611,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(fof_simplification,[status(thm)],[event_71]) ).
fof(i_0_612,plain,
! [X133,X134,X135] :
( ~ rdn_positive_less(rdnn(X133),rdnn(X135))
| ~ rdn_non_zero(X134)
| rdn_positive_less(rdn(rdnn(X133),X134),rdn(rdnn(X135),X134)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdn_positive_less_multi_digit_low])]) ).
fof(i_0_613,plain,
! [X108,X109,X110] :
( ~ the_agent_not_in_any_proposed_teams(X108,X109,X110)
| ~ accept_city(X108,X110)
| ~ accept_leader(X108,X109) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_6])]) ).
fof(i_0_614,plain,
! [X158,X159,X160] :
( ~ sum(X158,n1,X159)
| ~ less(X160,X159)
| less_or_equal(X160,X158) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[less_successor])]) ).
fof(i_0_615,plain,
! [X129,X130,X131,X132] :
( ~ rdn_positive_less(X130,X132)
| rdn_positive_less(rdn(rdnn(X129),X130),rdn(rdnn(X131),X132)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdn_positive_less_multi_digit_high])]) ).
fof(i_0_616,plain,
! [X126,X127,X128] :
( ~ rdn_positive_less(rdnn(X126),rdnn(X127))
| ~ rdn_positive_less(rdnn(X127),rdnn(X128))
| rdn_positive_less(rdnn(X126),rdnn(X128)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdn_positive_less_transitivity])]) ).
fof(i_0_617,plain,
! [X142,X143,X144,X145] :
( ~ rdn_translate(X142,rdn_pos(X144))
| ~ rdn_translate(X143,rdn_pos(X145))
| ~ rdn_positive_less(X144,X145)
| less(X142,X143) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[less_entry_point_pos_pos])]) ).
fof(i_0_618,plain,
! [X150,X151,X152,X153] :
( ~ rdn_translate(X150,rdn_neg(X152))
| ~ rdn_translate(X151,rdn_neg(X153))
| ~ rdn_positive_less(X153,X152)
| less(X150,X151) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[less_entry_point_neg_neg])]) ).
fof(i_0_619,plain,
! [X105,X106,X107] :
( ~ any_agent_in_all_proposed_teams(X105,X106,X107)
| accept_leader(X105,X106) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_5])]) ).
fof(i_0_620,plain,
! [X102,X103,X104] :
( ( accept_leader(X102,X103)
| ~ the_agent_in_all_proposed_teams(X102,X103,X104) )
& ( accept_city(X102,X104)
| ~ the_agent_in_all_proposed_teams(X102,X103,X104) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_4])])]) ).
fof(i_0_621,plain,
! [X146,X147,X148,X149] :
( ~ rdn_translate(X146,rdn_neg(X148))
| ~ rdn_translate(X147,rdn_pos(X149))
| less(X146,X147) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[less_entry_point_neg_pos])]) ).
fof(i_0_622,plain,
! [X136,X137,X138] :
( ~ rdn_non_zero(X138)
| rdn_positive_less(rdnn(X136),rdn(rdnn(X137),X138)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdn_extra_digits_positive_less])]) ).
fof(i_0_623,plain,
! [X95,X96,X97] :
( ~ accept_number(X95,X96)
| ~ less(X97,X96)
| accept_number(X95,X97) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_2])]) ).
fof(i_0_624,plain,
! [X140,X141] :
( ~ rdn_non_zero(X141)
| rdn_non_zero(rdn(rdnn(X140),X141)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdn_non_zero_by_structure])]) ).
fof(i_0_625,plain,
! [X154,X155] :
( ( ~ less(X155,X154)
| ~ less(X154,X155) )
& ( X155 != X154
| ~ less(X154,X155) )
& ( less(X155,X154)
| X155 = X154
| less(X154,X155) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_556])])]) ).
fof(i_0_626,plain,
! [X156,X157] :
( ( ~ less_or_equal(X156,X157)
| less(X156,X157)
| X156 = X157 )
& ( ~ less(X156,X157)
| less_or_equal(X156,X157) )
& ( X156 != X157
| less_or_equal(X156,X157) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[less_or_equal])])]) ).
fof(i_0_627,plain,
! [X111,X112] :
( ~ min_number_of_proposed_agents(X111,X112)
| accept_number(X111,X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_7])]) ).
fof(i_0_628,plain,
! [X139] :
( ~ rdn_non_zero_digit(rdnn(X139))
| rdn_non_zero(rdnn(X139)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdn_non_zero_by_digit])]) ).
cnf(i_0_629,plain,
( accept_city(X1,townc)
| ~ accept_population(X1,atheist,n30)
| ~ accept_population(X1,christian,n0)
| ~ accept_population(X1,muslim,n65)
| ~ accept_population(X1,native,n0)
| ~ accept_population(X1,other,n5) ),
inference(split_conjunct,[status(thm)],[i_0_557]) ).
cnf(i_0_630,negated_conjecture,
accept_population(X1,X2,X3),
inference(split_conjunct,[status(thm)],[i_0_558]) ).
cnf(i_0_631,plain,
( accept_city(X1,cityb)
| ~ accept_population(X1,atheist,n78)
| ~ accept_population(X1,christian,n20)
| ~ accept_population(X1,muslim,n1)
| ~ accept_population(X1,native,n0)
| ~ accept_population(X1,other,n1) ),
inference(split_conjunct,[status(thm)],[i_0_559]) ).
cnf(i_0_632,plain,
( accept_city(X1,townb)
| ~ accept_population(X1,atheist,n70)
| ~ accept_population(X1,christian,n20)
| ~ accept_population(X1,muslim,n8)
| ~ accept_population(X1,native,n0)
| ~ accept_population(X1,other,n2) ),
inference(split_conjunct,[status(thm)],[i_0_560]) ).
cnf(i_0_633,plain,
( accept_city(X1,citya)
| ~ accept_population(X1,atheist,n75)
| ~ accept_population(X1,christian,n25)
| ~ accept_population(X1,muslim,n0)
| ~ accept_population(X1,native,n0)
| ~ accept_population(X1,other,n0) ),
inference(split_conjunct,[status(thm)],[i_0_561]) ).
cnf(i_0_634,plain,
( accept_city(X1,towna)
| ~ accept_population(X1,atheist,n75)
| ~ accept_population(X1,christian,n24)
| ~ accept_population(X1,muslim,n1)
| ~ accept_population(X1,native,n0)
| ~ accept_population(X1,other,n0) ),
inference(split_conjunct,[status(thm)],[i_0_562]) ).
cnf(i_0_635,plain,
( accept_city(X1,sunsetpoint)
| ~ accept_population(X1,atheist,n0)
| ~ accept_population(X1,christian,n0)
| ~ accept_population(X1,muslim,n0)
| ~ accept_population(X1,native,n100)
| ~ accept_population(X1,other,n0) ),
inference(split_conjunct,[status(thm)],[i_0_563]) ).
cnf(i_0_636,plain,
( accept_city(X1,coastvillage)
| ~ accept_population(X1,atheist,n12)
| ~ accept_population(X1,christian,n3)
| ~ accept_population(X1,muslim,n0)
| ~ accept_population(X1,native,n85)
| ~ accept_population(X1,other,n0) ),
inference(split_conjunct,[status(thm)],[i_0_564]) ).
cnf(i_0_637,plain,
( accept_city(X1,northport)
| ~ accept_population(X1,atheist,n70)
| ~ accept_population(X1,christian,n13)
| ~ accept_population(X1,muslim,n0)
| ~ accept_population(X1,native,n15)
| ~ accept_population(X1,other,n2) ),
inference(split_conjunct,[status(thm)],[i_0_565]) ).
cnf(i_0_638,plain,
( accept_city(X1,stjosephburgh)
| ~ accept_population(X1,atheist,n68)
| ~ accept_population(X1,christian,n16)
| ~ accept_population(X1,muslim,n1)
| ~ accept_population(X1,native,n11)
| ~ accept_population(X1,other,n4) ),
inference(split_conjunct,[status(thm)],[i_0_566]) ).
cnf(i_0_639,plain,
( accept_city(X1,centrallakecity)
| ~ accept_population(X1,atheist,n70)
| ~ accept_population(X1,christian,n15)
| ~ accept_population(X1,muslim,n1)
| ~ accept_population(X1,native,n10)
| ~ accept_population(X1,other,n4) ),
inference(split_conjunct,[status(thm)],[i_0_567]) ).
cnf(i_0_640,plain,
( accept_city(X1,sunnysideport)
| ~ accept_population(X1,atheist,n30)
| ~ accept_population(X1,christian,n8)
| ~ accept_population(X1,muslim,n60)
| ~ accept_population(X1,native,n1)
| ~ accept_population(X1,other,n1) ),
inference(split_conjunct,[status(thm)],[i_0_568]) ).
cnf(i_0_641,plain,
( accept_city(X1,centraltown)
| ~ accept_population(X1,atheist,n54)
| ~ accept_population(X1,christian,n23)
| ~ accept_population(X1,muslim,n3)
| ~ accept_population(X1,native,n1)
| ~ accept_population(X1,other,n9) ),
inference(split_conjunct,[status(thm)],[i_0_569]) ).
cnf(i_0_642,plain,
( accept_city(X1,suffertown)
| ~ accept_population(X1,atheist,n65)
| ~ accept_population(X1,christian,n20)
| ~ accept_population(X1,muslim,n7)
| ~ accept_population(X1,native,n4)
| ~ accept_population(X1,other,n4) ),
inference(split_conjunct,[status(thm)],[i_0_570]) ).
cnf(i_0_643,plain,
( accept_number(X1,X2)
| ~ accept_team(X1,X3,X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_571]),
[final] ).
cnf(i_0_644,plain,
( accept_leader(X1,X2)
| ~ accept_team(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_571]),
[final] ).
cnf(i_0_645,plain,
( accept_city(X1,X2)
| ~ accept_team(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_571]),
[final] ).
cnf(i_0_646,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_572]),
[final] ).
cnf(i_0_647,plain,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2),
inference(split_conjunct,[status(thm)],[i_0_573]),
[final] ).
cnf(i_0_648,plain,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2),
inference(split_conjunct,[status(thm)],[i_0_574]),
[final] ).
cnf(i_0_649,plain,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2),
inference(split_conjunct,[status(thm)],[i_0_575]),
[final] ).
cnf(i_0_650,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[i_0_576]),
[final] ).
cnf(i_0_651,plain,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2),
inference(split_conjunct,[status(thm)],[i_0_577]),
[final] ).
cnf(i_0_652,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[i_0_578]),
[final] ).
cnf(i_0_653,plain,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2),
inference(split_conjunct,[status(thm)],[i_0_579]),
[final] ).
cnf(i_0_654,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[i_0_580]),
[final] ).
cnf(i_0_655,plain,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2),
inference(split_conjunct,[status(thm)],[i_0_581]),
[final] ).
cnf(i_0_656,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_582]),
[final] ).
cnf(i_0_657,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2),
inference(split_conjunct,[status(thm)],[i_0_583]),
[final] ).
cnf(i_0_658,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3),
inference(split_conjunct,[status(thm)],[i_0_584]),
[final] ).
cnf(i_0_659,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_585]),
[final] ).
cnf(i_0_660,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5),
inference(split_conjunct,[status(thm)],[i_0_586]),
[final] ).
cnf(i_0_661,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2),
inference(split_conjunct,[status(thm)],[i_0_587]),
[final] ).
cnf(i_0_662,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
inference(split_conjunct,[status(thm)],[i_0_588]),
[final] ).
cnf(i_0_663,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4),
inference(split_conjunct,[status(thm)],[i_0_589]),
[final] ).
cnf(i_0_664,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_590]),
[final] ).
cnf(i_0_665,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2),
inference(split_conjunct,[status(thm)],[i_0_591]),
[final] ).
cnf(i_0_666,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2),
inference(split_conjunct,[status(thm)],[i_0_592]),
[final] ).
cnf(i_0_667,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3),
inference(split_conjunct,[status(thm)],[i_0_593]),
[final] ).
cnf(i_0_668,plain,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4),
inference(split_conjunct,[status(thm)],[i_0_594]),
[final] ).
cnf(i_0_669,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_595]),
[final] ).
cnf(i_0_670,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2),
inference(split_conjunct,[status(thm)],[i_0_596]),
[final] ).
cnf(i_0_671,plain,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
inference(split_conjunct,[status(thm)],[i_0_597]),
[final] ).
cnf(i_0_672,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6),
inference(split_conjunct,[status(thm)],[i_0_598]),
[final] ).
cnf(i_0_673,plain,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_599]),
[final] ).
cnf(i_0_674,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6),
inference(split_conjunct,[status(thm)],[i_0_600]),
[final] ).
cnf(i_0_675,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_601]),
[final] ).
cnf(i_0_676,plain,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5),
inference(split_conjunct,[status(thm)],[i_0_602]),
[final] ).
cnf(i_0_677,plain,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[i_0_603]),
[final] ).
cnf(i_0_678,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[i_0_604]),
[final] ).
cnf(i_0_679,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[i_0_605]),
[final] ).
cnf(i_0_680,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5),
inference(split_conjunct,[status(thm)],[i_0_606]),
[final] ).
cnf(i_0_681,plain,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_607]),
[final] ).
cnf(i_0_682,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[i_0_608]),
[final] ).
cnf(i_0_683,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[i_0_609]),
[final] ).
cnf(i_0_684,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[i_0_610]),
[final] ).
cnf(i_0_685,plain,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[i_0_611]),
[final] ).
cnf(i_0_686,plain,
( accept_team(X1,X3,X2,X4)
| ~ accept_city(X1,X2)
| ~ accept_leader(X1,X3)
| ~ accept_number(X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_571]),
[final] ).
cnf(i_0_687,plain,
accept_team(sufferterragovernment,countryafirstaidorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_85]),
[final] ).
cnf(i_0_688,plain,
accept_team(sufferterragovernment,countryacivilorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_20]),
[final] ).
cnf(i_0_689,plain,
accept_team(sufferterragovernment,countryacivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_48]),
[final] ).
cnf(i_0_690,plain,
accept_team(sufferterragovernment,countryacivilorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_84]),
[final] ).
cnf(i_0_691,plain,
accept_team(sufferterragovernment,countryahumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_124]),
[final] ).
cnf(i_0_692,plain,
accept_team(sufferterragovernment,countryahumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_145]),
[final] ).
cnf(i_0_693,plain,
accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_83]),
[final] ).
cnf(i_0_694,plain,
accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_82]),
[final] ).
cnf(i_0_695,plain,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_93]),
[final] ).
cnf(i_0_696,plain,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_19]),
[final] ).
cnf(i_0_697,plain,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_26]),
[final] ).
cnf(i_0_698,plain,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_92]),
[final] ).
cnf(i_0_699,plain,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_125]),
[final] ).
cnf(i_0_700,plain,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_139]),
[final] ).
cnf(i_0_701,plain,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_91]),
[final] ).
cnf(i_0_702,plain,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_90]),
[final] ).
cnf(i_0_703,plain,
accept_team(countrybcivilorganization,countrycmedicalorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_79]),
[final] ).
cnf(i_0_704,plain,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_208]),
[final] ).
cnf(i_0_705,plain,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n5),
inference(split_conjunct,[status(thm)],[event_44]),
[final] ).
cnf(i_0_706,plain,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n4),
inference(split_conjunct,[status(thm)],[event_43]),
[final] ).
cnf(i_0_707,plain,
accept_team(countrybcivilorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_76]),
[final] ).
cnf(i_0_708,plain,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_77]),
[final] ).
cnf(i_0_709,plain,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_161]),
[final] ).
cnf(i_0_710,plain,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n5),
inference(split_conjunct,[status(thm)],[event_160]),
[final] ).
cnf(i_0_711,plain,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n4),
inference(split_conjunct,[status(thm)],[event_18]),
[final] ).
cnf(i_0_712,plain,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_206]),
[final] ).
cnf(i_0_713,plain,
accept_team(countrybcivilorganization,countryccivilorganization,towna,n4),
inference(split_conjunct,[status(thm)],[event_205]),
[final] ).
cnf(i_0_714,plain,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_78]),
[final] ).
cnf(i_0_715,plain,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_207]),
[final] ).
cnf(i_0_716,plain,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_75]),
[final] ).
cnf(i_0_717,plain,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_74]),
[final] ).
cnf(i_0_718,plain,
accept_team(countryamedicalorganization,sufferterragovernment,towna,n6),
inference(split_conjunct,[status(thm)],[event_189]),
[final] ).
cnf(i_0_719,plain,
accept_team(countryamedicalorganization,sufferterragovernment,towna,n5),
inference(split_conjunct,[status(thm)],[event_188]),
[final] ).
cnf(i_0_720,plain,
accept_team(countryamedicalorganization,countryacivilorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_14]),
[final] ).
cnf(i_0_721,plain,
accept_team(countryamedicalorganization,countryacivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_27]),
[final] ).
cnf(i_0_722,plain,
accept_team(countryamedicalorganization,countryahumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_126]),
[final] ).
cnf(i_0_723,plain,
accept_team(countryamedicalorganization,countryahumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_156]),
[final] ).
cnf(i_0_724,plain,
accept_team(countrycmedicalorganization,countrybcivilorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_129]),
[final] ).
cnf(i_0_725,plain,
accept_team(countrycmedicalorganization,countrybcivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_229]),
[final] ).
cnf(i_0_726,plain,
accept_team(countrycmedicalorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_128]),
[final] ).
cnf(i_0_727,plain,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_130]),
[final] ).
cnf(i_0_728,plain,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_155]),
[final] ).
cnf(i_0_729,plain,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n5),
inference(split_conjunct,[status(thm)],[event_154]),
[final] ).
cnf(i_0_730,plain,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_230]),
[final] ).
cnf(i_0_731,plain,
accept_team(countrycmedicalorganization,countryccivilorganization,townc,n4),
inference(split_conjunct,[status(thm)],[event_127]),
[final] ).
cnf(i_0_732,plain,
accept_team(countrycmedicalorganization,countryccivilorganization,towna,n4),
inference(split_conjunct,[status(thm)],[event_228]),
[final] ).
cnf(i_0_733,plain,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_131]),
[final] ).
cnf(i_0_734,plain,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_231]),
[final] ).
cnf(i_0_735,plain,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_96]),
[final] ).
cnf(i_0_736,plain,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_51]),
[final] ).
cnf(i_0_737,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_100]),
[final] ).
cnf(i_0_738,plain,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_103]),
[final] ).
cnf(i_0_739,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_101]),
[final] ).
cnf(i_0_740,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_173]),
[final] ).
cnf(i_0_741,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n5),
inference(split_conjunct,[status(thm)],[event_172]),
[final] ).
cnf(i_0_742,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
inference(split_conjunct,[status(thm)],[event_8]),
[final] ).
cnf(i_0_743,plain,
accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,townc,n4),
inference(split_conjunct,[status(thm)],[event_99]),
[final] ).
cnf(i_0_744,plain,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_102]),
[final] ).
cnf(i_0_745,plain,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_97]),
[final] ).
cnf(i_0_746,plain,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_13]),
[final] ).
cnf(i_0_747,plain,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_134]),
[final] ).
cnf(i_0_748,plain,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n2),
inference(split_conjunct,[status(thm)],[event_122]),
[final] ).
cnf(i_0_749,plain,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_198]),
[final] ).
cnf(i_0_750,plain,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n3),
inference(split_conjunct,[status(thm)],[event_193]),
[final] ).
cnf(i_0_751,plain,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_136]),
[final] ).
cnf(i_0_752,plain,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_200]),
[final] ).
cnf(i_0_753,plain,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n3),
inference(split_conjunct,[status(thm)],[event_195]),
[final] ).
cnf(i_0_754,plain,
accept_team(countrybhumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_123]),
[final] ).
cnf(i_0_755,plain,
accept_team(countrybhumanitarianorganization,countryccivilorganization,towna,n3),
inference(split_conjunct,[status(thm)],[event_196]),
[final] ).
cnf(i_0_756,plain,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_135]),
[final] ).
cnf(i_0_757,plain,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_199]),
[final] ).
cnf(i_0_758,plain,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3),
inference(split_conjunct,[status(thm)],[event_194]),
[final] ).
cnf(i_0_759,plain,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_25]),
[final] ).
cnf(i_0_760,plain,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_24]),
[final] ).
cnf(i_0_761,plain,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n4),
inference(split_conjunct,[status(thm)],[event_39]),
[final] ).
cnf(i_0_762,plain,
accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n2),
inference(split_conjunct,[status(thm)],[event_7]),
[final] ).
cnf(i_0_763,plain,
accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_110]),
[final] ).
cnf(i_0_764,plain,
accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_238]),
[final] ).
cnf(i_0_765,plain,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_112]),
[final] ).
cnf(i_0_766,plain,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_241]),
[final] ).
cnf(i_0_767,plain,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n5),
inference(split_conjunct,[status(thm)],[event_55]),
[final] ).
cnf(i_0_768,plain,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n4),
inference(split_conjunct,[status(thm)],[event_53]),
[final] ).
cnf(i_0_769,plain,
accept_team(christiancountrychumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_109]),
[final] ).
cnf(i_0_770,plain,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_111]),
[final] ).
cnf(i_0_771,plain,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_163]),
[final] ).
cnf(i_0_772,plain,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n5),
inference(split_conjunct,[status(thm)],[event_162]),
[final] ).
cnf(i_0_773,plain,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
inference(split_conjunct,[status(thm)],[event_15]),
[final] ).
cnf(i_0_774,plain,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_240]),
[final] ).
cnf(i_0_775,plain,
accept_team(christiancountrychumanitarianorganization,countryccivilorganization,townc,n4),
inference(split_conjunct,[status(thm)],[event_108]),
[final] ).
cnf(i_0_776,plain,
accept_team(christiancountrychumanitarianorganization,countryccivilorganization,towna,n4),
inference(split_conjunct,[status(thm)],[event_236]),
[final] ).
cnf(i_0_777,plain,
accept_team(countryafirstaidorganization,sufferterragovernment,towna,n6),
inference(split_conjunct,[status(thm)],[event_153]),
[final] ).
cnf(i_0_778,plain,
accept_team(countryafirstaidorganization,sufferterragovernment,towna,n5),
inference(split_conjunct,[status(thm)],[event_152]),
[final] ).
cnf(i_0_779,plain,
accept_team(countryafirstaidorganization,countryacivilorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_16]),
[final] ).
cnf(i_0_780,plain,
accept_team(countryafirstaidorganization,countryacivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_58]),
[final] ).
cnf(i_0_781,plain,
accept_team(countryafirstaidorganization,countryacivilorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_68]),
[final] ).
cnf(i_0_782,plain,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_107]),
[final] ).
cnf(i_0_783,plain,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_148]),
[final] ).
cnf(i_0_784,plain,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_67]),
[final] ).
cnf(i_0_785,plain,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_66]),
[final] ).
cnf(i_0_786,plain,
accept_team(countryacivilorganization,sufferterragovernment,towna,n6),
inference(split_conjunct,[status(thm)],[event_225]),
[final] ).
cnf(i_0_787,plain,
accept_team(countryacivilorganization,sufferterragovernment,towna,n5),
inference(split_conjunct,[status(thm)],[event_223]),
[final] ).
cnf(i_0_788,plain,
accept_team(countryacivilorganization,countryafirstaidorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_62]),
[final] ).
cnf(i_0_789,plain,
accept_team(countryacivilorganization,countryahumanitarianorganization,townc,n6),
inference(split_conjunct,[status(thm)],[event_106]),
[final] ).
cnf(i_0_790,plain,
accept_team(countryacivilorganization,countryahumanitarianorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_167]),
[final] ).
cnf(i_0_791,plain,
accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_61]),
[final] ).
cnf(i_0_792,plain,
accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n5),
inference(split_conjunct,[status(thm)],[event_60]),
[final] ).
cnf(i_0_793,plain,
accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n6),
inference(split_conjunct,[status(thm)],[event_191]),
[final] ).
cnf(i_0_794,plain,
accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n5),
inference(split_conjunct,[status(thm)],[event_190]),
[final] ).
cnf(i_0_795,plain,
accept_team(countryahumanitarianorganization,countryafirstaidorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_4]),
[final] ).
cnf(i_0_796,plain,
accept_team(countryahumanitarianorganization,countryacivilorganization,cityb,n6),
inference(split_conjunct,[status(thm)],[event_1]),
[final] ).
cnf(i_0_797,plain,
accept_team(countryahumanitarianorganization,countryacivilorganization,towna,n6),
inference(split_conjunct,[status(thm)],[event_2]),
[final] ).
cnf(i_0_798,plain,
accept_team(countryahumanitarianorganization,countryacivilorganization,coastvillage,n6),
inference(split_conjunct,[status(thm)],[event_3]),
[final] ).
cnf(i_0_799,plain,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn128]),
[final] ).
cnf(i_0_800,plain,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn127]),
[final] ).
cnf(i_0_801,plain,
rdn_translate(nn126,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn126]),
[final] ).
cnf(i_0_802,plain,
rdn_translate(nn125,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn125]),
[final] ).
cnf(i_0_803,plain,
rdn_translate(nn124,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn124]),
[final] ).
cnf(i_0_804,plain,
rdn_translate(nn123,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn123]),
[final] ).
cnf(i_0_805,plain,
rdn_translate(nn122,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn122]),
[final] ).
cnf(i_0_806,plain,
rdn_translate(nn121,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn121]),
[final] ).
cnf(i_0_807,plain,
rdn_translate(nn120,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn120]),
[final] ).
cnf(i_0_808,plain,
rdn_translate(nn119,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn119]),
[final] ).
cnf(i_0_809,plain,
rdn_translate(nn118,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn118]),
[final] ).
cnf(i_0_810,plain,
rdn_translate(nn117,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn117]),
[final] ).
cnf(i_0_811,plain,
rdn_translate(nn116,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn116]),
[final] ).
cnf(i_0_812,plain,
rdn_translate(nn115,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn115]),
[final] ).
cnf(i_0_813,plain,
rdn_translate(nn114,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn114]),
[final] ).
cnf(i_0_814,plain,
rdn_translate(nn113,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn113]),
[final] ).
cnf(i_0_815,plain,
rdn_translate(nn112,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn112]),
[final] ).
cnf(i_0_816,plain,
rdn_translate(nn111,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn111]),
[final] ).
cnf(i_0_817,plain,
rdn_translate(nn110,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn110]),
[final] ).
cnf(i_0_818,plain,
rdn_translate(nn109,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn109]),
[final] ).
cnf(i_0_819,plain,
rdn_translate(nn108,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn108]),
[final] ).
cnf(i_0_820,plain,
rdn_translate(nn107,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn107]),
[final] ).
cnf(i_0_821,plain,
rdn_translate(nn106,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn106]),
[final] ).
cnf(i_0_822,plain,
rdn_translate(nn105,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn105]),
[final] ).
cnf(i_0_823,plain,
rdn_translate(nn104,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn104]),
[final] ).
cnf(i_0_824,plain,
rdn_translate(nn103,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn103]),
[final] ).
cnf(i_0_825,plain,
rdn_translate(nn102,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn102]),
[final] ).
cnf(i_0_826,plain,
rdn_translate(nn101,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn101]),
[final] ).
cnf(i_0_827,plain,
rdn_translate(nn100,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdnn100]),
[final] ).
cnf(i_0_828,plain,
rdn_translate(n127,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn127]),
[final] ).
cnf(i_0_829,plain,
rdn_translate(n126,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn126]),
[final] ).
cnf(i_0_830,plain,
rdn_translate(n125,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn125]),
[final] ).
cnf(i_0_831,plain,
rdn_translate(n124,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn124]),
[final] ).
cnf(i_0_832,plain,
rdn_translate(n123,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn123]),
[final] ).
cnf(i_0_833,plain,
rdn_translate(n122,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn122]),
[final] ).
cnf(i_0_834,plain,
rdn_translate(n121,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn121]),
[final] ).
cnf(i_0_835,plain,
rdn_translate(n120,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn120]),
[final] ).
cnf(i_0_836,plain,
rdn_translate(n119,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn119]),
[final] ).
cnf(i_0_837,plain,
rdn_translate(n118,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn118]),
[final] ).
cnf(i_0_838,plain,
rdn_translate(n117,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn117]),
[final] ).
cnf(i_0_839,plain,
rdn_translate(n116,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn116]),
[final] ).
cnf(i_0_840,plain,
rdn_translate(n115,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn115]),
[final] ).
cnf(i_0_841,plain,
rdn_translate(n114,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn114]),
[final] ).
cnf(i_0_842,plain,
rdn_translate(n113,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn113]),
[final] ).
cnf(i_0_843,plain,
rdn_translate(n112,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn112]),
[final] ).
cnf(i_0_844,plain,
rdn_translate(n111,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn111]),
[final] ).
cnf(i_0_845,plain,
rdn_translate(n110,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn110]),
[final] ).
cnf(i_0_846,plain,
rdn_translate(n109,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn109]),
[final] ).
cnf(i_0_847,plain,
rdn_translate(n108,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn108]),
[final] ).
cnf(i_0_848,plain,
rdn_translate(n107,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn107]),
[final] ).
cnf(i_0_849,plain,
rdn_translate(n106,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn106]),
[final] ).
cnf(i_0_850,plain,
rdn_translate(n105,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn105]),
[final] ).
cnf(i_0_851,plain,
rdn_translate(n104,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn104]),
[final] ).
cnf(i_0_852,plain,
rdn_translate(n103,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn103]),
[final] ).
cnf(i_0_853,plain,
rdn_translate(n102,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn102]),
[final] ).
cnf(i_0_854,plain,
rdn_translate(n101,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn101]),
[final] ).
cnf(i_0_855,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(split_conjunct,[status(thm)],[rdn100]),
[final] ).
cnf(i_0_856,plain,
( rdn_positive_less(rdn(rdnn(X1),X3),rdn(rdnn(X2),X3))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2))
| ~ rdn_non_zero(X3) ),
inference(split_conjunct,[status(thm)],[i_0_612]),
[final] ).
cnf(i_0_857,plain,
( ~ the_agent_not_in_any_proposed_teams(X1,X2,X3)
| ~ accept_city(X1,X3)
| ~ accept_leader(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_613]),
[final] ).
cnf(i_0_858,plain,
( less_or_equal(X3,X1)
| ~ sum(X1,n1,X2)
| ~ less(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_614]),
[final] ).
cnf(i_0_859,plain,
( rdn_positive_less(rdn(rdnn(X3),X1),rdn(rdnn(X4),X2))
| ~ rdn_positive_less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_615]),
[final] ).
cnf(i_0_860,plain,
( rdn_positive_less(rdnn(X1),rdnn(X3))
| ~ rdn_positive_less(rdnn(X1),rdnn(X2))
| ~ rdn_positive_less(rdnn(X2),rdnn(X3)) ),
inference(split_conjunct,[status(thm)],[i_0_616]),
[final] ).
cnf(i_0_861,plain,
( less(X1,X3)
| ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(X3,rdn_pos(X4))
| ~ rdn_positive_less(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_617]),
[final] ).
cnf(i_0_862,plain,
( less(X1,X3)
| ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_translate(X3,rdn_neg(X4))
| ~ rdn_positive_less(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_618]),
[final] ).
cnf(i_0_863,plain,
( accept_leader(X1,X2)
| ~ any_agent_in_all_proposed_teams(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_619]),
[final] ).
cnf(i_0_864,plain,
( accept_leader(X1,X2)
| ~ the_agent_in_all_proposed_teams(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_620]),
[final] ).
cnf(i_0_865,plain,
( accept_city(X1,X2)
| ~ the_agent_in_all_proposed_teams(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_620]),
[final] ).
cnf(i_0_866,plain,
rdn_translate(nn99,rdn_neg(rdn(rdnn(n9),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn99]),
[final] ).
cnf(i_0_867,plain,
rdn_translate(nn98,rdn_neg(rdn(rdnn(n8),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn98]),
[final] ).
cnf(i_0_868,plain,
rdn_translate(nn97,rdn_neg(rdn(rdnn(n7),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn97]),
[final] ).
cnf(i_0_869,plain,
rdn_translate(nn96,rdn_neg(rdn(rdnn(n6),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn96]),
[final] ).
cnf(i_0_870,plain,
rdn_translate(nn95,rdn_neg(rdn(rdnn(n5),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn95]),
[final] ).
cnf(i_0_871,plain,
rdn_translate(nn94,rdn_neg(rdn(rdnn(n4),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn94]),
[final] ).
cnf(i_0_872,plain,
rdn_translate(nn93,rdn_neg(rdn(rdnn(n3),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn93]),
[final] ).
cnf(i_0_873,plain,
rdn_translate(nn92,rdn_neg(rdn(rdnn(n2),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn92]),
[final] ).
cnf(i_0_874,plain,
rdn_translate(nn91,rdn_neg(rdn(rdnn(n1),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn91]),
[final] ).
cnf(i_0_875,plain,
rdn_translate(nn90,rdn_neg(rdn(rdnn(n0),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdnn90]),
[final] ).
cnf(i_0_876,plain,
rdn_translate(nn89,rdn_neg(rdn(rdnn(n9),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn89]),
[final] ).
cnf(i_0_877,plain,
rdn_translate(nn88,rdn_neg(rdn(rdnn(n8),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn88]),
[final] ).
cnf(i_0_878,plain,
rdn_translate(nn87,rdn_neg(rdn(rdnn(n7),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn87]),
[final] ).
cnf(i_0_879,plain,
rdn_translate(nn86,rdn_neg(rdn(rdnn(n6),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn86]),
[final] ).
cnf(i_0_880,plain,
rdn_translate(nn85,rdn_neg(rdn(rdnn(n5),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn85]),
[final] ).
cnf(i_0_881,plain,
rdn_translate(nn84,rdn_neg(rdn(rdnn(n4),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn84]),
[final] ).
cnf(i_0_882,plain,
rdn_translate(nn83,rdn_neg(rdn(rdnn(n3),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn83]),
[final] ).
cnf(i_0_883,plain,
rdn_translate(nn82,rdn_neg(rdn(rdnn(n2),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn82]),
[final] ).
cnf(i_0_884,plain,
rdn_translate(nn81,rdn_neg(rdn(rdnn(n1),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn81]),
[final] ).
cnf(i_0_885,plain,
rdn_translate(nn80,rdn_neg(rdn(rdnn(n0),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdnn80]),
[final] ).
cnf(i_0_886,plain,
rdn_translate(nn79,rdn_neg(rdn(rdnn(n9),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn79]),
[final] ).
cnf(i_0_887,plain,
rdn_translate(nn78,rdn_neg(rdn(rdnn(n8),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn78]),
[final] ).
cnf(i_0_888,plain,
rdn_translate(nn77,rdn_neg(rdn(rdnn(n7),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn77]),
[final] ).
cnf(i_0_889,plain,
rdn_translate(nn76,rdn_neg(rdn(rdnn(n6),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn76]),
[final] ).
cnf(i_0_890,plain,
rdn_translate(nn75,rdn_neg(rdn(rdnn(n5),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn75]),
[final] ).
cnf(i_0_891,plain,
rdn_translate(nn74,rdn_neg(rdn(rdnn(n4),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn74]),
[final] ).
cnf(i_0_892,plain,
rdn_translate(nn73,rdn_neg(rdn(rdnn(n3),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn73]),
[final] ).
cnf(i_0_893,plain,
rdn_translate(nn72,rdn_neg(rdn(rdnn(n2),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn72]),
[final] ).
cnf(i_0_894,plain,
rdn_translate(nn71,rdn_neg(rdn(rdnn(n1),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn71]),
[final] ).
cnf(i_0_895,plain,
rdn_translate(nn70,rdn_neg(rdn(rdnn(n0),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdnn70]),
[final] ).
cnf(i_0_896,plain,
rdn_translate(nn69,rdn_neg(rdn(rdnn(n9),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn69]),
[final] ).
cnf(i_0_897,plain,
rdn_translate(nn68,rdn_neg(rdn(rdnn(n8),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn68]),
[final] ).
cnf(i_0_898,plain,
rdn_translate(nn67,rdn_neg(rdn(rdnn(n7),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn67]),
[final] ).
cnf(i_0_899,plain,
rdn_translate(nn66,rdn_neg(rdn(rdnn(n6),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn66]),
[final] ).
cnf(i_0_900,plain,
rdn_translate(nn65,rdn_neg(rdn(rdnn(n5),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn65]),
[final] ).
cnf(i_0_901,plain,
rdn_translate(nn64,rdn_neg(rdn(rdnn(n4),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn64]),
[final] ).
cnf(i_0_902,plain,
rdn_translate(nn63,rdn_neg(rdn(rdnn(n3),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn63]),
[final] ).
cnf(i_0_903,plain,
rdn_translate(nn62,rdn_neg(rdn(rdnn(n2),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn62]),
[final] ).
cnf(i_0_904,plain,
rdn_translate(nn61,rdn_neg(rdn(rdnn(n1),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn61]),
[final] ).
cnf(i_0_905,plain,
rdn_translate(nn60,rdn_neg(rdn(rdnn(n0),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdnn60]),
[final] ).
cnf(i_0_906,plain,
rdn_translate(nn59,rdn_neg(rdn(rdnn(n9),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn59]),
[final] ).
cnf(i_0_907,plain,
rdn_translate(nn58,rdn_neg(rdn(rdnn(n8),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn58]),
[final] ).
cnf(i_0_908,plain,
rdn_translate(nn57,rdn_neg(rdn(rdnn(n7),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn57]),
[final] ).
cnf(i_0_909,plain,
rdn_translate(nn56,rdn_neg(rdn(rdnn(n6),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn56]),
[final] ).
cnf(i_0_910,plain,
rdn_translate(nn55,rdn_neg(rdn(rdnn(n5),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn55]),
[final] ).
cnf(i_0_911,plain,
rdn_translate(nn54,rdn_neg(rdn(rdnn(n4),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn54]),
[final] ).
cnf(i_0_912,plain,
rdn_translate(nn53,rdn_neg(rdn(rdnn(n3),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn53]),
[final] ).
cnf(i_0_913,plain,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn52]),
[final] ).
cnf(i_0_914,plain,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn51]),
[final] ).
cnf(i_0_915,plain,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdnn50]),
[final] ).
cnf(i_0_916,plain,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn49]),
[final] ).
cnf(i_0_917,plain,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn48]),
[final] ).
cnf(i_0_918,plain,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn47]),
[final] ).
cnf(i_0_919,plain,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn46]),
[final] ).
cnf(i_0_920,plain,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn45]),
[final] ).
cnf(i_0_921,plain,
rdn_translate(nn44,rdn_neg(rdn(rdnn(n4),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn44]),
[final] ).
cnf(i_0_922,plain,
rdn_translate(nn43,rdn_neg(rdn(rdnn(n3),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn43]),
[final] ).
cnf(i_0_923,plain,
rdn_translate(nn42,rdn_neg(rdn(rdnn(n2),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn42]),
[final] ).
cnf(i_0_924,plain,
rdn_translate(nn41,rdn_neg(rdn(rdnn(n1),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn41]),
[final] ).
cnf(i_0_925,plain,
rdn_translate(nn40,rdn_neg(rdn(rdnn(n0),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdnn40]),
[final] ).
cnf(i_0_926,plain,
rdn_translate(nn39,rdn_neg(rdn(rdnn(n9),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn39]),
[final] ).
cnf(i_0_927,plain,
rdn_translate(nn38,rdn_neg(rdn(rdnn(n8),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn38]),
[final] ).
cnf(i_0_928,plain,
rdn_translate(nn37,rdn_neg(rdn(rdnn(n7),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn37]),
[final] ).
cnf(i_0_929,plain,
rdn_translate(nn36,rdn_neg(rdn(rdnn(n6),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn36]),
[final] ).
cnf(i_0_930,plain,
rdn_translate(nn35,rdn_neg(rdn(rdnn(n5),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn35]),
[final] ).
cnf(i_0_931,plain,
rdn_translate(nn34,rdn_neg(rdn(rdnn(n4),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn34]),
[final] ).
cnf(i_0_932,plain,
rdn_translate(nn33,rdn_neg(rdn(rdnn(n3),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn33]),
[final] ).
cnf(i_0_933,plain,
rdn_translate(nn32,rdn_neg(rdn(rdnn(n2),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn32]),
[final] ).
cnf(i_0_934,plain,
rdn_translate(nn31,rdn_neg(rdn(rdnn(n1),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn31]),
[final] ).
cnf(i_0_935,plain,
rdn_translate(nn30,rdn_neg(rdn(rdnn(n0),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdnn30]),
[final] ).
cnf(i_0_936,plain,
rdn_translate(nn29,rdn_neg(rdn(rdnn(n9),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn29]),
[final] ).
cnf(i_0_937,plain,
rdn_translate(nn28,rdn_neg(rdn(rdnn(n8),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn28]),
[final] ).
cnf(i_0_938,plain,
rdn_translate(nn27,rdn_neg(rdn(rdnn(n7),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn27]),
[final] ).
cnf(i_0_939,plain,
rdn_translate(nn26,rdn_neg(rdn(rdnn(n6),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn26]),
[final] ).
cnf(i_0_940,plain,
rdn_translate(nn25,rdn_neg(rdn(rdnn(n5),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn25]),
[final] ).
cnf(i_0_941,plain,
rdn_translate(nn24,rdn_neg(rdn(rdnn(n4),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn24]),
[final] ).
cnf(i_0_942,plain,
rdn_translate(nn23,rdn_neg(rdn(rdnn(n3),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn23]),
[final] ).
cnf(i_0_943,plain,
rdn_translate(nn22,rdn_neg(rdn(rdnn(n2),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn22]),
[final] ).
cnf(i_0_944,plain,
rdn_translate(nn21,rdn_neg(rdn(rdnn(n1),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn21]),
[final] ).
cnf(i_0_945,plain,
rdn_translate(nn20,rdn_neg(rdn(rdnn(n0),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdnn20]),
[final] ).
cnf(i_0_946,plain,
rdn_translate(nn19,rdn_neg(rdn(rdnn(n9),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn19]),
[final] ).
cnf(i_0_947,plain,
rdn_translate(nn18,rdn_neg(rdn(rdnn(n8),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn18]),
[final] ).
cnf(i_0_948,plain,
rdn_translate(nn17,rdn_neg(rdn(rdnn(n7),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn17]),
[final] ).
cnf(i_0_949,plain,
rdn_translate(nn16,rdn_neg(rdn(rdnn(n6),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn16]),
[final] ).
cnf(i_0_950,plain,
rdn_translate(nn15,rdn_neg(rdn(rdnn(n5),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn15]),
[final] ).
cnf(i_0_951,plain,
rdn_translate(nn14,rdn_neg(rdn(rdnn(n4),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn14]),
[final] ).
cnf(i_0_952,plain,
rdn_translate(nn13,rdn_neg(rdn(rdnn(n3),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn13]),
[final] ).
cnf(i_0_953,plain,
rdn_translate(nn12,rdn_neg(rdn(rdnn(n2),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn12]),
[final] ).
cnf(i_0_954,plain,
rdn_translate(nn11,rdn_neg(rdn(rdnn(n1),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn11]),
[final] ).
cnf(i_0_955,plain,
rdn_translate(nn10,rdn_neg(rdn(rdnn(n0),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdnn10]),
[final] ).
cnf(i_0_956,plain,
rdn_translate(n99,rdn_pos(rdn(rdnn(n9),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn99]),
[final] ).
cnf(i_0_957,plain,
rdn_translate(n98,rdn_pos(rdn(rdnn(n8),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn98]),
[final] ).
cnf(i_0_958,plain,
rdn_translate(n97,rdn_pos(rdn(rdnn(n7),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn97]),
[final] ).
cnf(i_0_959,plain,
rdn_translate(n96,rdn_pos(rdn(rdnn(n6),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn96]),
[final] ).
cnf(i_0_960,plain,
rdn_translate(n95,rdn_pos(rdn(rdnn(n5),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn95]),
[final] ).
cnf(i_0_961,plain,
rdn_translate(n94,rdn_pos(rdn(rdnn(n4),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn94]),
[final] ).
cnf(i_0_962,plain,
rdn_translate(n93,rdn_pos(rdn(rdnn(n3),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn93]),
[final] ).
cnf(i_0_963,plain,
rdn_translate(n92,rdn_pos(rdn(rdnn(n2),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn92]),
[final] ).
cnf(i_0_964,plain,
rdn_translate(n91,rdn_pos(rdn(rdnn(n1),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn91]),
[final] ).
cnf(i_0_965,plain,
rdn_translate(n90,rdn_pos(rdn(rdnn(n0),rdnn(n9)))),
inference(split_conjunct,[status(thm)],[rdn90]),
[final] ).
cnf(i_0_966,plain,
rdn_translate(n89,rdn_pos(rdn(rdnn(n9),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn89]),
[final] ).
cnf(i_0_967,plain,
rdn_translate(n88,rdn_pos(rdn(rdnn(n8),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn88]),
[final] ).
cnf(i_0_968,plain,
rdn_translate(n87,rdn_pos(rdn(rdnn(n7),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn87]),
[final] ).
cnf(i_0_969,plain,
rdn_translate(n86,rdn_pos(rdn(rdnn(n6),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn86]),
[final] ).
cnf(i_0_970,plain,
rdn_translate(n84,rdn_pos(rdn(rdnn(n4),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn84]),
[final] ).
cnf(i_0_971,plain,
rdn_translate(n83,rdn_pos(rdn(rdnn(n3),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn83]),
[final] ).
cnf(i_0_972,plain,
rdn_translate(n82,rdn_pos(rdn(rdnn(n2),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn82]),
[final] ).
cnf(i_0_973,plain,
rdn_translate(n81,rdn_pos(rdn(rdnn(n1),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn81]),
[final] ).
cnf(i_0_974,plain,
rdn_translate(n80,rdn_pos(rdn(rdnn(n0),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn80]),
[final] ).
cnf(i_0_975,plain,
rdn_translate(n79,rdn_pos(rdn(rdnn(n9),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn79]),
[final] ).
cnf(i_0_976,plain,
rdn_translate(n77,rdn_pos(rdn(rdnn(n7),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn77]),
[final] ).
cnf(i_0_977,plain,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn76]),
[final] ).
cnf(i_0_978,plain,
rdn_translate(n74,rdn_pos(rdn(rdnn(n4),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn74]),
[final] ).
cnf(i_0_979,plain,
rdn_translate(n73,rdn_pos(rdn(rdnn(n3),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn73]),
[final] ).
cnf(i_0_980,plain,
rdn_translate(n72,rdn_pos(rdn(rdnn(n2),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn72]),
[final] ).
cnf(i_0_981,plain,
rdn_translate(n71,rdn_pos(rdn(rdnn(n1),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn71]),
[final] ).
cnf(i_0_982,plain,
rdn_translate(n69,rdn_pos(rdn(rdnn(n9),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn69]),
[final] ).
cnf(i_0_983,plain,
rdn_translate(n67,rdn_pos(rdn(rdnn(n7),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn67]),
[final] ).
cnf(i_0_984,plain,
rdn_translate(n66,rdn_pos(rdn(rdnn(n6),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn66]),
[final] ).
cnf(i_0_985,plain,
rdn_translate(n64,rdn_pos(rdn(rdnn(n4),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn64]),
[final] ).
cnf(i_0_986,plain,
rdn_translate(n63,rdn_pos(rdn(rdnn(n3),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn63]),
[final] ).
cnf(i_0_987,plain,
rdn_translate(n62,rdn_pos(rdn(rdnn(n2),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn62]),
[final] ).
cnf(i_0_988,plain,
rdn_translate(n61,rdn_pos(rdn(rdnn(n1),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn61]),
[final] ).
cnf(i_0_989,plain,
rdn_translate(n59,rdn_pos(rdn(rdnn(n9),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn59]),
[final] ).
cnf(i_0_990,plain,
rdn_translate(n58,rdn_pos(rdn(rdnn(n8),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn58]),
[final] ).
cnf(i_0_991,plain,
rdn_translate(n57,rdn_pos(rdn(rdnn(n7),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn57]),
[final] ).
cnf(i_0_992,plain,
rdn_translate(n56,rdn_pos(rdn(rdnn(n6),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn56]),
[final] ).
cnf(i_0_993,plain,
rdn_translate(n55,rdn_pos(rdn(rdnn(n5),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn55]),
[final] ).
cnf(i_0_994,plain,
rdn_translate(n53,rdn_pos(rdn(rdnn(n3),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn53]),
[final] ).
cnf(i_0_995,plain,
rdn_translate(n52,rdn_pos(rdn(rdnn(n2),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn52]),
[final] ).
cnf(i_0_996,plain,
rdn_translate(n51,rdn_pos(rdn(rdnn(n1),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn51]),
[final] ).
cnf(i_0_997,plain,
rdn_translate(n50,rdn_pos(rdn(rdnn(n0),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn50]),
[final] ).
cnf(i_0_998,plain,
rdn_translate(n49,rdn_pos(rdn(rdnn(n9),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn49]),
[final] ).
cnf(i_0_999,plain,
rdn_translate(n48,rdn_pos(rdn(rdnn(n8),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn48]),
[final] ).
cnf(i_0_1000,plain,
rdn_translate(n47,rdn_pos(rdn(rdnn(n7),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn47]),
[final] ).
cnf(i_0_1001,plain,
rdn_translate(n46,rdn_pos(rdn(rdnn(n6),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn46]),
[final] ).
cnf(i_0_1002,plain,
rdn_translate(n45,rdn_pos(rdn(rdnn(n5),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn45]),
[final] ).
cnf(i_0_1003,plain,
rdn_translate(n44,rdn_pos(rdn(rdnn(n4),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn44]),
[final] ).
cnf(i_0_1004,plain,
rdn_translate(n43,rdn_pos(rdn(rdnn(n3),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn43]),
[final] ).
cnf(i_0_1005,plain,
rdn_translate(n42,rdn_pos(rdn(rdnn(n2),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn42]),
[final] ).
cnf(i_0_1006,plain,
rdn_translate(n41,rdn_pos(rdn(rdnn(n1),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn41]),
[final] ).
cnf(i_0_1007,plain,
rdn_translate(n40,rdn_pos(rdn(rdnn(n0),rdnn(n4)))),
inference(split_conjunct,[status(thm)],[rdn40]),
[final] ).
cnf(i_0_1008,plain,
rdn_translate(n39,rdn_pos(rdn(rdnn(n9),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn39]),
[final] ).
cnf(i_0_1009,plain,
rdn_translate(n38,rdn_pos(rdn(rdnn(n8),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn38]),
[final] ).
cnf(i_0_1010,plain,
rdn_translate(n37,rdn_pos(rdn(rdnn(n7),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn37]),
[final] ).
cnf(i_0_1011,plain,
rdn_translate(n36,rdn_pos(rdn(rdnn(n6),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn36]),
[final] ).
cnf(i_0_1012,plain,
rdn_translate(n35,rdn_pos(rdn(rdnn(n5),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn35]),
[final] ).
cnf(i_0_1013,plain,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn34]),
[final] ).
cnf(i_0_1014,plain,
rdn_translate(n33,rdn_pos(rdn(rdnn(n3),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn33]),
[final] ).
cnf(i_0_1015,plain,
rdn_translate(n32,rdn_pos(rdn(rdnn(n2),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn32]),
[final] ).
cnf(i_0_1016,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn31]),
[final] ).
cnf(i_0_1017,plain,
rdn_translate(n29,rdn_pos(rdn(rdnn(n9),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn29]),
[final] ).
cnf(i_0_1018,plain,
rdn_translate(n28,rdn_pos(rdn(rdnn(n8),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn28]),
[final] ).
cnf(i_0_1019,plain,
rdn_translate(n27,rdn_pos(rdn(rdnn(n7),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn27]),
[final] ).
cnf(i_0_1020,plain,
rdn_translate(n26,rdn_pos(rdn(rdnn(n6),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn26]),
[final] ).
cnf(i_0_1021,plain,
rdn_translate(n22,rdn_pos(rdn(rdnn(n2),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn22]),
[final] ).
cnf(i_0_1022,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn21]),
[final] ).
cnf(i_0_1023,plain,
rdn_translate(n19,rdn_pos(rdn(rdnn(n9),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn19]),
[final] ).
cnf(i_0_1024,plain,
rdn_translate(n18,rdn_pos(rdn(rdnn(n8),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn18]),
[final] ).
cnf(i_0_1025,plain,
rdn_translate(n17,rdn_pos(rdn(rdnn(n7),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn17]),
[final] ).
cnf(i_0_1026,plain,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn14]),
[final] ).
cnf(i_0_1027,plain,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn78]),
[final] ).
cnf(i_0_1028,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn25]),
[final] ).
cnf(i_0_1029,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn24]),
[final] ).
cnf(i_0_1030,plain,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn75]),
[final] ).
cnf(i_0_1031,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(split_conjunct,[status(thm)],[rdn85]),
[final] ).
cnf(i_0_1032,plain,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn12]),
[final] ).
cnf(i_0_1033,plain,
rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn13]),
[final] ).
cnf(i_0_1034,plain,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn11]),
[final] ).
cnf(i_0_1035,plain,
rdn_translate(n16,rdn_pos(rdn(rdnn(n6),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn16]),
[final] ).
cnf(i_0_1036,plain,
rdn_translate(n68,rdn_pos(rdn(rdnn(n8),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn68]),
[final] ).
cnf(i_0_1037,plain,
rdn_translate(n10,rdn_pos(rdn(rdnn(n0),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn10]),
[final] ).
cnf(i_0_1038,plain,
rdn_translate(n15,rdn_pos(rdn(rdnn(n5),rdnn(n1)))),
inference(split_conjunct,[status(thm)],[rdn15]),
[final] ).
cnf(i_0_1039,plain,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
inference(split_conjunct,[status(thm)],[rdn70]),
[final] ).
cnf(i_0_1040,plain,
rdn_translate(n60,rdn_pos(rdn(rdnn(n0),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn60]),
[final] ).
cnf(i_0_1041,plain,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
inference(split_conjunct,[status(thm)],[rdn30]),
[final] ).
cnf(i_0_1042,plain,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn23]),
[final] ).
cnf(i_0_1043,plain,
rdn_translate(n54,rdn_pos(rdn(rdnn(n4),rdnn(n5)))),
inference(split_conjunct,[status(thm)],[rdn54]),
[final] ).
cnf(i_0_1044,plain,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
inference(split_conjunct,[status(thm)],[rdn20]),
[final] ).
cnf(i_0_1045,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(split_conjunct,[status(thm)],[rdn65]),
[final] ).
cnf(i_0_1046,plain,
( less(X1,X3)
| ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_translate(X3,rdn_pos(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_621]),
[final] ).
cnf(i_0_1047,plain,
( rdn_positive_less(rdnn(X2),rdn(rdnn(X3),X1))
| ~ rdn_non_zero(X1) ),
inference(split_conjunct,[status(thm)],[i_0_622]),
[final] ).
cnf(i_0_1048,plain,
( accept_number(X1,X3)
| ~ accept_number(X1,X2)
| ~ less(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_623]),
[final] ).
cnf(i_0_1049,plain,
the_agent_not_in_any_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_37]),
[final] ).
cnf(i_0_1050,plain,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_248]),
[final] ).
cnf(i_0_1051,plain,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_11]),
[final] ).
cnf(i_0_1052,plain,
any_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_147]),
[final] ).
cnf(i_0_1053,plain,
any_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_87]),
[final] ).
cnf(i_0_1054,plain,
any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_142]),
[final] ).
cnf(i_0_1055,plain,
any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_95]),
[final] ).
cnf(i_0_1056,plain,
any_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_210]),
[final] ).
cnf(i_0_1057,plain,
any_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_47]),
[final] ).
cnf(i_0_1058,plain,
any_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_81]),
[final] ).
cnf(i_0_1059,plain,
any_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_159]),
[final] ).
cnf(i_0_1060,plain,
any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_38]),
[final] ).
cnf(i_0_1061,plain,
any_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_233]),
[final] ).
cnf(i_0_1062,plain,
any_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_50]),
[final] ).
cnf(i_0_1063,plain,
any_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_133]),
[final] ).
cnf(i_0_1064,plain,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_249]),
[final] ).
cnf(i_0_1065,plain,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_12]),
[final] ).
cnf(i_0_1066,plain,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_105]),
[final] ).
cnf(i_0_1067,plain,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_202]),
[final] ).
cnf(i_0_1068,plain,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_23]),
[final] ).
cnf(i_0_1069,plain,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_138]),
[final] ).
cnf(i_0_1070,plain,
any_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_221]),
[final] ).
cnf(i_0_1071,plain,
any_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_42]),
[final] ).
cnf(i_0_1072,plain,
any_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_121]),
[final] ).
cnf(i_0_1073,plain,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_244]),
[final] ).
cnf(i_0_1074,plain,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_57]),
[final] ).
cnf(i_0_1075,plain,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_114]),
[final] ).
cnf(i_0_1076,plain,
any_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_151]),
[final] ).
cnf(i_0_1077,plain,
any_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_70]),
[final] ).
cnf(i_0_1078,plain,
any_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_170]),
[final] ).
cnf(i_0_1079,plain,
any_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_64]),
[final] ).
cnf(i_0_1080,plain,
any_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_165]),
[final] ).
cnf(i_0_1081,plain,
any_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_6]),
[final] ).
cnf(i_0_1082,plain,
the_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_146]),
[final] ).
cnf(i_0_1083,plain,
the_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_86]),
[final] ).
cnf(i_0_1084,plain,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_141]),
[final] ).
cnf(i_0_1085,plain,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_94]),
[final] ).
cnf(i_0_1086,plain,
the_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_209]),
[final] ).
cnf(i_0_1087,plain,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_46]),
[final] ).
cnf(i_0_1088,plain,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_80]),
[final] ).
cnf(i_0_1089,plain,
the_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_158]),
[final] ).
cnf(i_0_1090,plain,
the_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_232]),
[final] ).
cnf(i_0_1091,plain,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_49]),
[final] ).
cnf(i_0_1092,plain,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_132]),
[final] ).
cnf(i_0_1093,plain,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_104]),
[final] ).
cnf(i_0_1094,plain,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_201]),
[final] ).
cnf(i_0_1095,plain,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_22]),
[final] ).
cnf(i_0_1096,plain,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_137]),
[final] ).
cnf(i_0_1097,plain,
the_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_220]),
[final] ).
cnf(i_0_1098,plain,
the_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_41]),
[final] ).
cnf(i_0_1099,plain,
the_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_120]),
[final] ).
cnf(i_0_1100,plain,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna),
inference(split_conjunct,[status(thm)],[event_243]),
[final] ).
cnf(i_0_1101,plain,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna),
inference(split_conjunct,[status(thm)],[event_56]),
[final] ).
cnf(i_0_1102,plain,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc),
inference(split_conjunct,[status(thm)],[event_113]),
[final] ).
cnf(i_0_1103,plain,
the_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_150]),
[final] ).
cnf(i_0_1104,plain,
the_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_69]),
[final] ).
cnf(i_0_1105,plain,
the_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_169]),
[final] ).
cnf(i_0_1106,plain,
the_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_63]),
[final] ).
cnf(i_0_1107,plain,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb),
inference(split_conjunct,[status(thm)],[event_164]),
[final] ).
cnf(i_0_1108,plain,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage),
inference(split_conjunct,[status(thm)],[event_5]),
[final] ).
cnf(i_0_1109,plain,
( rdn_non_zero(rdn(rdnn(X2),X1))
| ~ rdn_non_zero(X1) ),
inference(split_conjunct,[status(thm)],[i_0_624]),
[final] ).
cnf(i_0_1110,plain,
( ~ less(X1,X2)
| ~ less(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_625]),
[final] ).
cnf(i_0_1111,plain,
( less(X1,X2)
| X1 = X2
| ~ less_or_equal(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_626]),
[final] ).
cnf(i_0_1112,plain,
( less_or_equal(X1,X2)
| ~ less(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_626]),
[final] ).
cnf(i_0_1113,plain,
( accept_number(X1,X2)
| ~ min_number_of_proposed_agents(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_627]),
[final] ).
cnf(i_0_1114,plain,
( less(X1,X2)
| X1 = X2
| less(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_625]),
[final] ).
cnf(i_0_1115,plain,
( rdn_non_zero(rdnn(X1))
| ~ rdn_non_zero_digit(rdnn(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_628]),
[final] ).
cnf(i_0_1116,plain,
( X1 != X2
| ~ less(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_625]),
[final] ).
cnf(i_0_1117,plain,
rdn_translate(nn9,rdn_neg(rdnn(n9))),
inference(split_conjunct,[status(thm)],[rdnn9]),
[final] ).
cnf(i_0_1118,plain,
rdn_translate(nn8,rdn_neg(rdnn(n8))),
inference(split_conjunct,[status(thm)],[rdnn8]),
[final] ).
cnf(i_0_1119,plain,
rdn_translate(nn7,rdn_neg(rdnn(n7))),
inference(split_conjunct,[status(thm)],[rdnn7]),
[final] ).
cnf(i_0_1120,plain,
rdn_translate(nn6,rdn_neg(rdnn(n6))),
inference(split_conjunct,[status(thm)],[rdnn6]),
[final] ).
cnf(i_0_1121,plain,
rdn_translate(nn5,rdn_neg(rdnn(n5))),
inference(split_conjunct,[status(thm)],[rdnn5]),
[final] ).
cnf(i_0_1122,plain,
rdn_translate(nn4,rdn_neg(rdnn(n4))),
inference(split_conjunct,[status(thm)],[rdnn4]),
[final] ).
cnf(i_0_1123,plain,
rdn_translate(nn3,rdn_neg(rdnn(n3))),
inference(split_conjunct,[status(thm)],[rdnn3]),
[final] ).
cnf(i_0_1124,plain,
rdn_translate(nn2,rdn_neg(rdnn(n2))),
inference(split_conjunct,[status(thm)],[rdnn2]),
[final] ).
cnf(i_0_1125,plain,
rdn_translate(nn1,rdn_neg(rdnn(n1))),
inference(split_conjunct,[status(thm)],[rdnn1]),
[final] ).
cnf(i_0_1126,plain,
rdn_translate(n6,rdn_pos(rdnn(n6))),
inference(split_conjunct,[status(thm)],[rdn6]),
[final] ).
cnf(i_0_1127,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(split_conjunct,[status(thm)],[rdn5]),
[final] ).
cnf(i_0_1128,plain,
rdn_translate(n2,rdn_pos(rdnn(n2))),
inference(split_conjunct,[status(thm)],[rdn2]),
[final] ).
cnf(i_0_1129,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(split_conjunct,[status(thm)],[rdn0]),
[final] ).
cnf(i_0_1130,plain,
rdn_translate(n8,rdn_pos(rdnn(n8))),
inference(split_conjunct,[status(thm)],[rdn8]),
[final] ).
cnf(i_0_1131,plain,
rdn_translate(n9,rdn_pos(rdnn(n9))),
inference(split_conjunct,[status(thm)],[rdn9]),
[final] ).
cnf(i_0_1132,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(split_conjunct,[status(thm)],[rdn1]),
[final] ).
cnf(i_0_1133,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(split_conjunct,[status(thm)],[rdn3]),
[final] ).
cnf(i_0_1134,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(split_conjunct,[status(thm)],[rdn4]),
[final] ).
cnf(i_0_1135,plain,
rdn_translate(n7,rdn_pos(rdnn(n7))),
inference(split_conjunct,[status(thm)],[rdn7]),
[final] ).
cnf(i_0_1136,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(split_conjunct,[status(thm)],[rdn_positive_less67]),
[final] ).
cnf(i_0_1137,plain,
rdn_positive_less(rdnn(n5),rdnn(n6)),
inference(split_conjunct,[status(thm)],[rdn_positive_less56]),
[final] ).
cnf(i_0_1138,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(split_conjunct,[status(thm)],[rdn_positive_less23]),
[final] ).
cnf(i_0_1139,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(split_conjunct,[status(thm)],[rdn_positive_less01]),
[final] ).
cnf(i_0_1140,plain,
rdn_positive_less(rdnn(n8),rdnn(n9)),
inference(split_conjunct,[status(thm)],[rdn_positive_less89]),
[final] ).
cnf(i_0_1141,plain,
rdn_positive_less(rdnn(n1),rdnn(n2)),
inference(split_conjunct,[status(thm)],[rdn_positive_less12]),
[final] ).
cnf(i_0_1142,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(split_conjunct,[status(thm)],[rdn_positive_less34]),
[final] ).
cnf(i_0_1143,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(split_conjunct,[status(thm)],[rdn_positive_less45]),
[final] ).
cnf(i_0_1144,plain,
rdn_positive_less(rdnn(n7),rdnn(n8)),
inference(split_conjunct,[status(thm)],[rdn_positive_less78]),
[final] ).
cnf(i_0_1145,plain,
( less_or_equal(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_626]),
[final] ).
cnf(i_0_1146,negated_conjecture,
accept_city(X1,townc),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_629,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1147,negated_conjecture,
accept_city(X1,cityb),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_631,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1148,negated_conjecture,
accept_city(X1,townb),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_632,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1149,negated_conjecture,
accept_city(X1,citya),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_633,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1150,negated_conjecture,
accept_city(X1,towna),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_634,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1151,negated_conjecture,
accept_city(X1,sunsetpoint),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_635,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1152,negated_conjecture,
accept_city(X1,coastvillage),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_636,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1153,negated_conjecture,
accept_city(X1,northport),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_637,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1154,negated_conjecture,
accept_city(X1,stjosephburgh),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_638,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1155,negated_conjecture,
accept_city(X1,centrallakecity),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_639,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1156,negated_conjecture,
accept_city(X1,sunnysideport),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_640,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1157,negated_conjecture,
accept_city(X1,centraltown),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_641,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1158,negated_conjecture,
accept_city(X1,suffertown),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_642,c_0_630]),c_0_630]),c_0_630]),c_0_630]),c_0_630])]),
[final] ).
cnf(i_0_1159,plain,
accept_number(sufferterragovernment,n6),
inference(split_conjunct,[status(thm)],[event_224]),
[final] ).
cnf(i_0_1160,plain,
accept_number(sufferterragovernment,n5),
inference(split_conjunct,[status(thm)],[event_222]),
[final] ).
cnf(i_0_1161,plain,
accept_number(sufferterragovernment,n2),
inference(split_conjunct,[status(thm)],[event_211]),
[final] ).
cnf(i_0_1162,plain,
accept_number(christiansufferterrahumanitarianorganization,n6),
inference(split_conjunct,[status(thm)],[event_140]),
[final] ).
cnf(i_0_1163,plain,
accept_number(christiansufferterrahumanitarianorganization,n2),
inference(split_conjunct,[status(thm)],[event_88]),
[final] ).
cnf(i_0_1164,plain,
accept_number(countrybcivilorganization,n6),
inference(split_conjunct,[status(thm)],[event_237]),
[final] ).
cnf(i_0_1165,plain,
accept_number(countrybcivilorganization,n5),
inference(split_conjunct,[status(thm)],[event_45]),
[final] ).
cnf(i_0_1166,plain,
accept_number(countrybcivilorganization,n2),
inference(split_conjunct,[status(thm)],[event_203]),
[final] ).
cnf(i_0_1167,plain,
accept_number(countrybcivilorganization,n3),
inference(split_conjunct,[status(thm)],[event_204]),
[final] ).
cnf(i_0_1168,plain,
accept_number(countryamedicalorganization,n6),
inference(split_conjunct,[status(thm)],[event_157]),
[final] ).
cnf(i_0_1169,plain,
accept_number(countrycmedicalorganization,n6),
inference(split_conjunct,[status(thm)],[event_245]),
[final] ).
cnf(i_0_1170,plain,
accept_number(countrycmedicalorganization,n5),
inference(split_conjunct,[status(thm)],[event_54]),
[final] ).
cnf(i_0_1171,plain,
accept_number(countrycmedicalorganization,n2),
inference(split_conjunct,[status(thm)],[event_226]),
[final] ).
cnf(i_0_1172,plain,
accept_number(countrycmedicalorganization,n3),
inference(split_conjunct,[status(thm)],[event_227]),
[final] ).
cnf(i_0_1173,plain,
accept_number(countrycmedicalorganization,n4),
inference(split_conjunct,[status(thm)],[event_52]),
[final] ).
cnf(i_0_1174,plain,
accept_number(muslimcountrybhumanitarianorganization,n6),
inference(split_conjunct,[status(thm)],[event_247]),
[final] ).
cnf(i_0_1175,plain,
accept_number(muslimcountrybhumanitarianorganization,n2),
inference(split_conjunct,[status(thm)],[event_183]),
[final] ).
cnf(i_0_1176,plain,
accept_number(muslimcountrybhumanitarianorganization,n3),
inference(split_conjunct,[status(thm)],[event_98]),
[final] ).
cnf(i_0_1177,plain,
accept_number(countrybhumanitarianorganization,n6),
inference(split_conjunct,[status(thm)],[event_239]),
[final] ).
cnf(i_0_1178,plain,
accept_number(countrybhumanitarianorganization,n5),
inference(split_conjunct,[status(thm)],[event_171]),
[final] ).
cnf(i_0_1179,plain,
accept_number(countrybhumanitarianorganization,n2),
inference(split_conjunct,[status(thm)],[event_197]),
[final] ).
cnf(i_0_1180,plain,
accept_number(countrybhumanitarianorganization,n1),
inference(split_conjunct,[status(thm)],[event_21]),
[final] ).
cnf(i_0_1181,plain,
accept_number(countrybhumanitarianorganization,n4),
inference(split_conjunct,[status(thm)],[event_17]),
[final] ).
cnf(i_0_1182,plain,
accept_number(countryccivilorganization,n2),
inference(split_conjunct,[status(thm)],[event_214]),
[final] ).
cnf(i_0_1183,plain,
accept_number(countryccivilorganization,n3),
inference(split_conjunct,[status(thm)],[event_215]),
[final] ).
cnf(i_0_1184,plain,
accept_number(countryccivilorganization,n4),
inference(split_conjunct,[status(thm)],[event_235]),
[final] ).
cnf(i_0_1185,plain,
accept_number(christiancountrychumanitarianorganization,n6),
inference(split_conjunct,[status(thm)],[event_242]),
[final] ).
cnf(i_0_1186,plain,
accept_number(christiancountrychumanitarianorganization,n5),
inference(split_conjunct,[status(thm)],[event_73]),
[final] ).
cnf(i_0_1187,plain,
accept_number(christiancountrychumanitarianorganization,n2),
inference(split_conjunct,[status(thm)],[event_192]),
[final] ).
cnf(i_0_1188,plain,
accept_number(christiancountrychumanitarianorganization,n3),
inference(split_conjunct,[status(thm)],[event_234]),
[final] ).
cnf(i_0_1189,plain,
accept_number(countryafirstaidorganization,n6),
inference(split_conjunct,[status(thm)],[event_149]),
[final] ).
cnf(i_0_1190,plain,
accept_number(countryafirstaidorganization,n2),
inference(split_conjunct,[status(thm)],[event_65]),
[final] ).
cnf(i_0_1191,plain,
accept_number(countryacivilorganization,n6),
inference(split_conjunct,[status(thm)],[event_168]),
[final] ).
cnf(i_0_1192,plain,
accept_number(countryacivilorganization,n2),
inference(split_conjunct,[status(thm)],[event_59]),
[final] ).
cnf(i_0_1193,plain,
accept_number(countryahumanitarianorganization,n6),
inference(split_conjunct,[status(thm)],[event_166]),
[final] ).
cnf(i_0_1194,plain,
accept_number(countryahumanitarianorganization,n5),
inference(split_conjunct,[status(thm)],[event_89]),
[final] ).
cnf(i_0_1195,plain,
accept_number(countryahumanitarianorganization,n2),
inference(split_conjunct,[status(thm)],[event_28]),
[final] ).
cnf(i_0_1196,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(split_conjunct,[status(thm)],[rdn_digit6]),
[final] ).
cnf(i_0_1197,plain,
rdn_non_zero_digit(rdnn(n5)),
inference(split_conjunct,[status(thm)],[rdn_digit5]),
[final] ).
cnf(i_0_1198,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(split_conjunct,[status(thm)],[rdn_digit2]),
[final] ).
cnf(i_0_1199,plain,
rdn_non_zero_digit(rdnn(n8)),
inference(split_conjunct,[status(thm)],[rdn_digit8]),
[final] ).
cnf(i_0_1200,plain,
rdn_non_zero_digit(rdnn(n9)),
inference(split_conjunct,[status(thm)],[rdn_digit9]),
[final] ).
cnf(i_0_1201,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(split_conjunct,[status(thm)],[rdn_digit1]),
[final] ).
cnf(i_0_1202,plain,
rdn_non_zero_digit(rdnn(n3)),
inference(split_conjunct,[status(thm)],[rdn_digit3]),
[final] ).
cnf(i_0_1203,plain,
rdn_non_zero_digit(rdnn(n4)),
inference(split_conjunct,[status(thm)],[rdn_digit4]),
[final] ).
cnf(i_0_1204,plain,
rdn_non_zero_digit(rdnn(n7)),
inference(split_conjunct,[status(thm)],[rdn_digit7]),
[final] ).
cnf(i_0_1205,axiom,
X1 = X1 ).
cnf(i_0_1206,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_1207,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_1208,axiom,
( X1 != X2
| ~ accept_number(X1,X3)
| accept_number(X2,X3) ) ).
cnf(i_0_1209,axiom,
( X1 != X2
| ~ accept_number(X3,X1)
| accept_number(X3,X2) ) ).
cnf(i_0_1210,axiom,
( X1 != X2
| ~ sum(X1,X3,X4)
| sum(X2,X3,X4) ) ).
cnf(i_0_1211,axiom,
( X1 != X2
| ~ sum(X3,X1,X4)
| sum(X3,X2,X4) ) ).
cnf(i_0_1212,axiom,
( X1 != X2
| ~ sum(X3,X4,X1)
| sum(X3,X4,X2) ) ).
cnf(i_0_1213,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_1214,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_1215,axiom,
( X1 != X2
| ~ any_agent_in_all_proposed_teams(X1,X3,X4)
| any_agent_in_all_proposed_teams(X2,X3,X4) ) ).
cnf(i_0_1216,axiom,
( X1 != X2
| ~ any_agent_in_all_proposed_teams(X3,X1,X4)
| any_agent_in_all_proposed_teams(X3,X2,X4) ) ).
cnf(i_0_1217,axiom,
( X1 != X2
| ~ any_agent_in_all_proposed_teams(X3,X4,X1)
| any_agent_in_all_proposed_teams(X3,X4,X2) ) ).
cnf(i_0_1218,axiom,
( X1 != X2
| ~ the_agent_in_all_proposed_teams(X1,X3,X4)
| the_agent_in_all_proposed_teams(X2,X3,X4) ) ).
cnf(i_0_1219,axiom,
( X1 != X2
| ~ the_agent_in_all_proposed_teams(X3,X1,X4)
| the_agent_in_all_proposed_teams(X3,X2,X4) ) ).
cnf(i_0_1220,axiom,
( X1 != X2
| ~ the_agent_in_all_proposed_teams(X3,X4,X1)
| the_agent_in_all_proposed_teams(X3,X4,X2) ) ).
cnf(i_0_1221,axiom,
( X1 != X2
| ~ min_number_of_proposed_agents(X1,X3)
| min_number_of_proposed_agents(X2,X3) ) ).
cnf(i_0_1222,axiom,
( X1 != X2
| ~ min_number_of_proposed_agents(X3,X1)
| min_number_of_proposed_agents(X3,X2) ) ).
cnf(i_0_1223,axiom,
( X1 != X2
| ~ rdn_non_zero_digit(X1)
| rdn_non_zero_digit(X2) ) ).
cnf(i_0_1224,axiom,
( X1 != X2
| ~ accept_team(X1,X3,X4,X5)
| accept_team(X2,X3,X4,X5) ) ).
cnf(i_0_1225,axiom,
( X1 != X2
| ~ accept_team(X3,X1,X4,X5)
| accept_team(X3,X2,X4,X5) ) ).
cnf(i_0_1226,axiom,
( X1 != X2
| ~ accept_team(X3,X4,X1,X5)
| accept_team(X3,X4,X2,X5) ) ).
cnf(i_0_1227,axiom,
( X1 != X2
| ~ accept_team(X3,X4,X5,X1)
| accept_team(X3,X4,X5,X2) ) ).
cnf(i_0_1228,axiom,
( X1 != X2
| ~ accept_leader(X1,X3)
| accept_leader(X2,X3) ) ).
cnf(i_0_1229,axiom,
( X1 != X2
| ~ accept_leader(X3,X1)
| accept_leader(X3,X2) ) ).
cnf(i_0_1230,axiom,
( X1 != X2
| ~ accept_city(X1,X3)
| accept_city(X2,X3) ) ).
cnf(i_0_1231,axiom,
( X1 != X2
| ~ accept_city(X3,X1)
| accept_city(X3,X2) ) ).
cnf(i_0_1232,axiom,
( X1 != X2
| ~ rdn_translate(X1,X3)
| rdn_translate(X2,X3) ) ).
cnf(i_0_1233,axiom,
( X1 != X2
| ~ rdn_translate(X3,X1)
| rdn_translate(X3,X2) ) ).
cnf(i_0_1234,axiom,
( X1 != X2
| ~ rdn_positive_less(X1,X3)
| rdn_positive_less(X2,X3) ) ).
cnf(i_0_1235,axiom,
( X1 != X2
| ~ rdn_positive_less(X3,X1)
| rdn_positive_less(X3,X2) ) ).
cnf(i_0_1236,axiom,
( X1 != X2
| ~ rdn_non_zero(X1)
| rdn_non_zero(X2) ) ).
cnf(i_0_1237,axiom,
( X1 != X2
| ~ the_agent_not_in_any_proposed_teams(X1,X3,X4)
| the_agent_not_in_any_proposed_teams(X2,X3,X4) ) ).
cnf(i_0_1238,axiom,
( X1 != X2
| ~ the_agent_not_in_any_proposed_teams(X3,X1,X4)
| the_agent_not_in_any_proposed_teams(X3,X2,X4) ) ).
cnf(i_0_1239,axiom,
( X1 != X2
| ~ the_agent_not_in_any_proposed_teams(X3,X4,X1)
| the_agent_not_in_any_proposed_teams(X3,X4,X2) ) ).
cnf(i_0_1240,axiom,
( X1 != X2
| ~ less_or_equal(X1,X3)
| less_or_equal(X2,X3) ) ).
cnf(i_0_1241,axiom,
( X1 != X2
| ~ less_or_equal(X3,X1)
| less_or_equal(X3,X2) ) ).
cnf(i_0_1205_001,axiom,
X1 = X1 ).
cnf(i_0_1206_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_1207_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_1208_004,axiom,
( X1 != X2
| ~ accept_number(X1,X3)
| accept_number(X2,X3) ) ).
cnf(i_0_1209_005,axiom,
( X1 != X2
| ~ accept_number(X3,X1)
| accept_number(X3,X2) ) ).
cnf(i_0_1210_006,axiom,
( X1 != X2
| ~ sum(X1,X3,X4)
| sum(X2,X3,X4) ) ).
cnf(i_0_1211_007,axiom,
( X1 != X2
| ~ sum(X3,X1,X4)
| sum(X3,X2,X4) ) ).
cnf(i_0_1212_008,axiom,
( X1 != X2
| ~ sum(X3,X4,X1)
| sum(X3,X4,X2) ) ).
cnf(i_0_1213_009,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_1214_010,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_1215_011,axiom,
( X1 != X2
| ~ any_agent_in_all_proposed_teams(X1,X3,X4)
| any_agent_in_all_proposed_teams(X2,X3,X4) ) ).
cnf(i_0_1216_012,axiom,
( X1 != X2
| ~ any_agent_in_all_proposed_teams(X3,X1,X4)
| any_agent_in_all_proposed_teams(X3,X2,X4) ) ).
cnf(i_0_1217_013,axiom,
( X1 != X2
| ~ any_agent_in_all_proposed_teams(X3,X4,X1)
| any_agent_in_all_proposed_teams(X3,X4,X2) ) ).
cnf(i_0_1218_014,axiom,
( X1 != X2
| ~ the_agent_in_all_proposed_teams(X1,X3,X4)
| the_agent_in_all_proposed_teams(X2,X3,X4) ) ).
cnf(i_0_1219_015,axiom,
( X1 != X2
| ~ the_agent_in_all_proposed_teams(X3,X1,X4)
| the_agent_in_all_proposed_teams(X3,X2,X4) ) ).
cnf(i_0_1220_016,axiom,
( X1 != X2
| ~ the_agent_in_all_proposed_teams(X3,X4,X1)
| the_agent_in_all_proposed_teams(X3,X4,X2) ) ).
cnf(i_0_1221_017,axiom,
( X1 != X2
| ~ min_number_of_proposed_agents(X1,X3)
| min_number_of_proposed_agents(X2,X3) ) ).
cnf(i_0_1222_018,axiom,
( X1 != X2
| ~ min_number_of_proposed_agents(X3,X1)
| min_number_of_proposed_agents(X3,X2) ) ).
cnf(i_0_1223_019,axiom,
( X1 != X2
| ~ rdn_non_zero_digit(X1)
| rdn_non_zero_digit(X2) ) ).
cnf(i_0_1224_020,axiom,
( X1 != X2
| ~ accept_team(X1,X3,X4,X5)
| accept_team(X2,X3,X4,X5) ) ).
cnf(i_0_1225_021,axiom,
( X1 != X2
| ~ accept_team(X3,X1,X4,X5)
| accept_team(X3,X2,X4,X5) ) ).
cnf(i_0_1226_022,axiom,
( X1 != X2
| ~ accept_team(X3,X4,X1,X5)
| accept_team(X3,X4,X2,X5) ) ).
cnf(i_0_1227_023,axiom,
( X1 != X2
| ~ accept_team(X3,X4,X5,X1)
| accept_team(X3,X4,X5,X2) ) ).
cnf(i_0_1228_024,axiom,
( X1 != X2
| ~ accept_leader(X1,X3)
| accept_leader(X2,X3) ) ).
cnf(i_0_1229_025,axiom,
( X1 != X2
| ~ accept_leader(X3,X1)
| accept_leader(X3,X2) ) ).
cnf(i_0_1230_026,axiom,
( X1 != X2
| ~ accept_city(X1,X3)
| accept_city(X2,X3) ) ).
cnf(i_0_1231_027,axiom,
( X1 != X2
| ~ accept_city(X3,X1)
| accept_city(X3,X2) ) ).
cnf(i_0_1232_028,axiom,
( X1 != X2
| ~ rdn_translate(X1,X3)
| rdn_translate(X2,X3) ) ).
cnf(i_0_1233_029,axiom,
( X1 != X2
| ~ rdn_translate(X3,X1)
| rdn_translate(X3,X2) ) ).
cnf(i_0_1234_030,axiom,
( X1 != X2
| ~ rdn_positive_less(X1,X3)
| rdn_positive_less(X2,X3) ) ).
cnf(i_0_1235_031,axiom,
( X1 != X2
| ~ rdn_positive_less(X3,X1)
| rdn_positive_less(X3,X2) ) ).
cnf(i_0_1236_032,axiom,
( X1 != X2
| ~ rdn_non_zero(X1)
| rdn_non_zero(X2) ) ).
cnf(i_0_1237_033,axiom,
( X1 != X2
| ~ the_agent_not_in_any_proposed_teams(X1,X3,X4)
| the_agent_not_in_any_proposed_teams(X2,X3,X4) ) ).
cnf(i_0_1238_034,axiom,
( X1 != X2
| ~ the_agent_not_in_any_proposed_teams(X3,X1,X4)
| the_agent_not_in_any_proposed_teams(X3,X2,X4) ) ).
cnf(i_0_1239_035,axiom,
( X1 != X2
| ~ the_agent_not_in_any_proposed_teams(X3,X4,X1)
| the_agent_not_in_any_proposed_teams(X3,X4,X2) ) ).
cnf(i_0_1240_036,axiom,
( X1 != X2
| ~ less_or_equal(X1,X3)
| less_or_equal(X2,X3) ) ).
cnf(i_0_1241_037,axiom,
( X1 != X2
| ~ less_or_equal(X3,X1)
| less_or_equal(X3,X2) ) ).
cnf(i_0_1242,plain,
~ less(X1,X1),
inference(equality_inference,[],[1116]) ).
cnf(i_0_1243,plain,
less_or_equal(X1,X1),
inference(equality_inference,[],[1145]) ).
cnf(i_0_1244,plain,
~ accept_leader(muslimcountrybhumanitarianorganization,sufferterragovernment),
inference(scs_inference,[],[i_0_1150,i_0_1050,i_0_857]) ).
cnf(i_0_1245,plain,
accept_city(X1,towna),
inference(rename_variables,[],[i_0_1150]) ).
cnf(i_0_1246,plain,
( ~ accept_city(X1,X2)
| ~ accept_leader(X1,X3)
| ~ the_agent_not_in_any_proposed_teams(X1,X3,X2) ),
inference(rename_variables,[],[i_0_857]) ).
cnf(i_0_1247,plain,
countryamedicalorganization != christiansufferterrahumanitarianorganization,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_1050,i_0_718,i_0_857,i_0_1224]) ).
cnf(i_0_1248,plain,
countryacivilorganization != sufferterragovernment,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_1050,i_0_697,i_0_718,i_0_857,i_0_1224,i_0_1225]) ).
cnf(i_0_1249,plain,
cityb != coastvillage,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_1050,i_0_697,i_0_718,i_0_720,i_0_857,i_0_1224,i_0_1225,i_0_1226]) ).
cnf(i_0_1250,plain,
n4 != n6,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_697,i_0_718,i_0_720,i_0_761,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227]) ).
cnf(i_0_1251,plain,
less(nn9,n6),
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046]) ).
cnf(i_0_1252,plain,
( ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_translate(X3,rdn_pos(X4))
| less(X1,X3) ),
inference(rename_variables,[],[i_0_1046]) ).
cnf(i_0_1253,plain,
nn9 != n6,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_1242,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046,i_0_1213]) ).
cnf(i_0_1254,plain,
~ less(X1,X1),
inference(rename_variables,[],[i_0_1242]) ).
cnf(i_0_1255,plain,
n6 != nn9,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_1242,i_0_1254,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046,i_0_1213,i_0_1214]) ).
cnf(i_0_1256,plain,
~ less(X1,X1),
inference(rename_variables,[],[i_0_1242]) ).
cnf(i_0_1257,plain,
~ rdn_positive_less(rdnn(n6),rdnn(n6)),
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_1242,i_0_1254,i_0_1256,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046,i_0_1213,i_0_1214,i_0_861]) ).
cnf(i_0_1258,plain,
~ less(X1,X1),
inference(rename_variables,[],[i_0_1242]) ).
cnf(i_0_1259,plain,
( ~ rdn_translate(X1,rdn_pos(X2))
| ~ rdn_translate(X3,rdn_pos(X4))
| ~ rdn_positive_less(X2,X4)
| less(X1,X3) ),
inference(rename_variables,[],[i_0_861]) ).
cnf(i_0_1260,plain,
~ rdn_positive_less(rdnn(n9),rdnn(n9)),
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_1242,i_0_1254,i_0_1256,i_0_1258,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046,i_0_1213,i_0_1214,i_0_861,i_0_862]) ).
cnf(i_0_1261,plain,
~ less(X1,X1),
inference(rename_variables,[],[i_0_1242]) ).
cnf(i_0_1262,plain,
( ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_translate(X3,rdn_neg(X4))
| ~ rdn_positive_less(X4,X2)
| less(X1,X3) ),
inference(rename_variables,[],[i_0_862]) ).
cnf(i_0_1263,plain,
~ accept_team(muslimcountrybhumanitarianorganization,sufferterragovernment,X1,X2),
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_1242,i_0_1254,i_0_1256,i_0_1258,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046,i_0_1213,i_0_1214,i_0_861,i_0_862,i_0_644]) ).
cnf(i_0_1264,plain,
( accept_leader(X1,X2)
| ~ accept_team(X1,X2,X3,X4) ),
inference(rename_variables,[],[i_0_644]) ).
cnf(i_0_1265,plain,
$false,
inference(scs_inference,[],[i_0_1150,i_0_646,i_0_652,i_0_675,i_0_1050,i_0_1242,i_0_1254,i_0_1256,i_0_1258,i_0_697,i_0_718,i_0_720,i_0_761,i_0_1064,i_0_1117,i_0_1126,i_0_857,i_0_1224,i_0_1225,i_0_1226,i_0_1227,i_0_1046,i_0_1213,i_0_1214,i_0_861,i_0_862,i_0_644,i_0_863]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : AGT014+1 : TPTP v9.2.1. Bugfixed v3.1.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n014.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 10:10:21 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 0.47/1.66 % Version : CSE_E---1.7
% 0.47/1.66 % Problem : theBenchmark.p
% 0.47/1.66 % SZS status Theorem for theBenchmark.p
% 0.47/1.66 % SZS output start CNFRefutation
% See solution above
% 0.52/1.79 % Total time : 1.323s
%------------------------------------------------------------------------------