%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : AGT042+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:06:43 AM UTC 2026
% Result : Satisfiable 7.46s 1.84s
% Output : Saturation 0.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1394,axiom,
~ accept_population(muslimcountrybhumanitarianorganization,christian,n24) ).
cnf(u1398,axiom,
~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ).
cnf(u1406,axiom,
~ accept_city(countryccivilorganization,coastvillage) ).
cnf(u1411,axiom,
~ accept_population(countryccivilorganization,native,n85) ).
cnf(u1415,axiom,
~ accept_population(countryccivilorganization,muslim,n0) ).
cnf(u1453,axiom,
~ accept_population(countryamedicalorganization,native,n85) ).
cnf(u1457,axiom,
~ accept_population(countryamedicalorganization,muslim,n0) ).
cnf(u1579,axiom,
~ accept_city(countryamedicalorganization,sunsetpoint) ).
cnf(u1593,axiom,
~ accept_city(countryccivilorganization,sunsetpoint) ).
cnf(u1606,axiom,
~ accept_city(sufferterragovernment,sunsetpoint) ).
cnf(u1615,axiom,
~ accept_population(sufferterragovernment,atheist,n0) ).
cnf(u1619,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,sunsetpoint) ).
cnf(u1624,axiom,
~ accept_population(christiansufferterrahumanitarianorganization,native,n100) ).
cnf(u1632,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,sunsetpoint) ).
cnf(u1641,axiom,
~ accept_population(muslimcountrybhumanitarianorganization,atheist,n0) ).
cnf(u1666,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,citya) ).
cnf(u1675,axiom,
~ accept_city(sufferterragovernment,citya) ).
cnf(u1680,axiom,
~ accept_population(sufferterragovernment,christian,n25) ).
cnf(u1684,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,citya) ).
cnf(u1689,axiom,
~ accept_population(christiansufferterrahumanitarianorganization,christian,n25) ).
cnf(u1718,axiom,
~ accept_city(countrybcivilorganization,citya) ).
cnf(u1723,axiom,
~ accept_population(countrybcivilorganization,christian,n25) ).
cnf(u1727,axiom,
~ accept_city(countrycmedicalorganization,citya) ).
cnf(u1732,axiom,
~ accept_population(countrycmedicalorganization,christian,n25) ).
cnf(u1736,axiom,
~ accept_city(countryafirstaidorganization,citya) ).
cnf(u1741,axiom,
~ accept_population(countryafirstaidorganization,christian,n25) ).
cnf(u1745,axiom,
~ accept_city(countryacivilorganization,citya) ).
cnf(u1750,axiom,
~ accept_population(countryacivilorganization,christian,n25) ).
cnf(u1754,axiom,
~ accept_city(countryahumanitarianorganization,citya) ).
cnf(u1759,axiom,
~ accept_population(countryahumanitarianorganization,christian,n25) ).
cnf(u1771,axiom,
~ accept_city(countrycmedicalorganization,sunsetpoint) ).
cnf(u1776,axiom,
~ accept_population(countrycmedicalorganization,native,n100) ).
cnf(u1790,axiom,
~ accept_city(countrybhumanitarianorganization,citya) ).
cnf(u1795,axiom,
~ accept_population(countrybhumanitarianorganization,christian,n25) ).
cnf(u1805,axiom,
~ accept_city(countryafirstaidorganization,sunsetpoint) ).
cnf(u1810,axiom,
~ accept_population(countryafirstaidorganization,native,n100) ).
cnf(u1824,axiom,
~ accept_city(countryacivilorganization,sunsetpoint) ).
cnf(u1829,axiom,
~ accept_population(countryacivilorganization,native,n100) ).
cnf(u1841,axiom,
~ accept_city(christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1844,axiom,
~ accept_city(christiancountrychumanitarianorganization,citya) ).
cnf(u1874,axiom,
~ accept_city(sufferterragovernment,sunnysideport) ).
cnf(u1879,axiom,
~ accept_population(sufferterragovernment,native,n1) ).
cnf(u1891,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,sunnysideport) ).
cnf(u1896,axiom,
~ accept_population(christiansufferterrahumanitarianorganization,native,n1) ).
cnf(u1908,axiom,
~ accept_city(countryamedicalorganization,sunnysideport) ).
cnf(u1917,axiom,
~ accept_population(countryamedicalorganization,muslim,n60) ).
cnf(u1925,axiom,
~ accept_city(countrycmedicalorganization,sunnysideport) ).
cnf(u1930,axiom,
~ accept_population(countrycmedicalorganization,native,n1) ).
cnf(u1942,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,sunnysideport) ).
cnf(u1947,axiom,
~ accept_population(muslimcountrybhumanitarianorganization,native,n1) ).
cnf(u1959,axiom,
~ accept_city(countryccivilorganization,sunnysideport) ).
cnf(u1964,axiom,
~ accept_population(countryccivilorganization,native,n1) ).
cnf(u1976,axiom,
~ accept_city(countryafirstaidorganization,sunnysideport) ).
cnf(u1989,axiom,
~ accept_population(countryafirstaidorganization,christian,n8) ).
cnf(u1993,axiom,
~ accept_city(countryacivilorganization,sunnysideport) ).
cnf(u2006,axiom,
~ accept_population(countryacivilorganization,christian,n8) ).
cnf(u2035,axiom,
~ accept_city(countryahumanitarianorganization,sunsetpoint) ).
cnf(u2040,axiom,
~ accept_population(countryahumanitarianorganization,native,n100) ).
cnf(u2054,axiom,
~ accept_city(countryahumanitarianorganization,sunnysideport) ).
cnf(u2059,axiom,
~ accept_population(countryahumanitarianorganization,native,n1) ).
cnf(u2084,axiom,
~ accept_city(countrybcivilorganization,sunsetpoint) ).
cnf(u2089,axiom,
~ accept_population(countrybcivilorganization,native,n100) ).
cnf(u2100,axiom,
~ accept_city(countrybcivilorganization,sunnysideport) ).
cnf(u2105,axiom,
~ accept_population(countrybcivilorganization,native,n1) ).
cnf(u2129,axiom,
~ accept_city(countrybhumanitarianorganization,sunsetpoint) ).
cnf(u2134,axiom,
~ accept_population(countrybhumanitarianorganization,native,n100) ).
cnf(u2156,axiom,
~ accept_population(christiancountrychumanitarianorganization,muslim,n0) ).
cnf(u2168,axiom,
~ accept_city(christiancountrychumanitarianorganization,sunsetpoint) ).
cnf(u2190,axiom,
~ accept_city(christiancountrychumanitarianorganization,sunnysideport) ).
cnf(u2195,axiom,
~ accept_population(christiancountrychumanitarianorganization,native,n1) ).
cnf(u2876,axiom,
~ accept_city(countrybhumanitarianorganization,cityb) ).
cnf(u2881,axiom,
~ accept_city(countrybhumanitarianorganization,sunnysideport) ).
cnf(u2885,axiom,
~ accept_population(countrybhumanitarianorganization,christian,n20) ).
cnf(u3067,axiom,
~ accept_city(countrybhumanitarianorganization,townb) ).
cnf(u3089,axiom,
~ accept_city(sufferterragovernment,northport) ).
cnf(u3102,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,northport) ).
cnf(u3115,axiom,
~ accept_city(countrybcivilorganization,northport) ).
cnf(u3128,axiom,
~ accept_city(countrycmedicalorganization,northport) ).
cnf(u3136,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,townb) ).
cnf(u3145,axiom,
~ accept_population(muslimcountrybhumanitarianorganization,muslim,n8) ).
cnf(u3149,axiom,
~ accept_city(countryafirstaidorganization,townb) ).
cnf(u3158,axiom,
~ accept_population(countryafirstaidorganization,muslim,n8) ).
cnf(u3167,axiom,
~ accept_city(countryacivilorganization,northport) ).
cnf(u3175,axiom,
~ accept_city(countryahumanitarianorganization,townb) ).
cnf(u3184,axiom,
~ accept_population(countryahumanitarianorganization,muslim,n8) ).
cnf(u1021,axiom,
accept_population(countryamedicalorganization,other,n5) ).
cnf(u913,axiom,
accept_team(countryamedicalorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u948,axiom,
accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n6) ).
cnf(u1307,axiom,
accept_leader(countrybcivilorganization,sufferterragovernment) ).
cnf(u1019,axiom,
~ accept_city(countryamedicalorganization,coastvillage) ).
cnf(u1294,axiom,
accept_population(countrycmedicalorganization,atheist,n75) ).
cnf(u784,axiom,
accept_team(countryamedicalorganization,countryacivilorganization,towna,n6) ).
cnf(u3192,axiom,
~ accept_city(countrybhumanitarianorganization,suffertown) ).
cnf(u805,axiom,
accept_team(sufferterragovernment,countryacivilorganization,towna,n6) ).
cnf(u1327,axiom,
accept_number(countryccivilorganization,n3) ).
cnf(u1193,axiom,
accept_population(countrycmedicalorganization,atheist,n30) ).
cnf(u1298,axiom,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization) ).
cnf(u803,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna) ).
cnf(u678,axiom,
( ~ any_agent_in_all_proposed_teams(X0,X1,X2)
| accept_leader(X0,X1) ) ).
cnf(u912,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1694,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75)
| accept_city(X0,citya)
| ~ accept_city(X0,coastvillage)
| ~ accept_city(X0,townc) ) ).
cnf(u933,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2) ).
cnf(u818,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u931,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2) ).
cnf(u1334,axiom,
accept_number(countrybcivilorganization,n3) ).
cnf(u824,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u936,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3) ).
cnf(u689,axiom,
( accept_population(X0,muslim,n3)
| ~ accept_city(X0,centraltown) ) ).
cnf(u1169,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryacivilorganization) ).
cnf(u1077,axiom,
accept_population(countryacivilorganization,atheist,n12) ).
cnf(u946,axiom,
accept_team(countryamedicalorganization,sufferterragovernment,towna,n6) ).
cnf(u1058,axiom,
accept_population(countrybcivilorganization,atheist,n78) ).
cnf(u1332,axiom,
accept_number(countrybcivilorganization,n5) ).
cnf(u952,axiom,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n3) ).
cnf(u672,axiom,
( ~ accept_team(X0,X3,X1,X2)
| accept_number(X0,X2) ) ).
cnf(u729,axiom,
( accept_population(X0,other,n0)
| ~ accept_city(X0,towna) ) ).
cnf(u1081,axiom,
accept_population(countryacivilorganization,muslim,n65) ).
cnf(u1265,axiom,
accept_leader(sufferterragovernment,countrybhumanitarianorganization) ).
cnf(u1205,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n30) ).
cnf(u1336,axiom,
accept_number(countrybcivilorganization,n1) ).
cnf(u703,axiom,
( accept_population(X0,atheist,n70)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u1186,axiom,
accept_population(countryccivilorganization,atheist,n30) ).
cnf(u828,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1087,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n75) ).
cnf(u1209,axiom,
accept_population(muslimcountrybhumanitarianorganization,native,n0) ).
cnf(u2645,axiom,
( ~ accept_population(X0,muslim,n60)
| ~ accept_population(X0,christian,n8)
| ~ accept_city(X0,centraltown)
| ~ accept_population(X0,atheist,n30)
| accept_city(X0,sunnysideport)
| ~ accept_city(X0,cityb) ) ).
cnf(u950,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n3) ).
cnf(u956,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1094,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n3) ).
cnf(u1215,axiom,
accept_leader(countryamedicalorganization,countryacivilorganization) ).
cnf(u833,axiom,
accept_team(countrybcivilorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u2646,axiom,
~ accept_city(countryahumanitarianorganization,centraltown) ).
cnf(u1117,axiom,
accept_leader(countryafirstaidorganization,countryacivilorganization) ).
cnf(u1349,axiom,
accept_number(christiancountrychumanitarianorganization,n3) ).
cnf(u847,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1098,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ).
cnf(u2652,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,centraltown) ).
cnf(u1092,axiom,
accept_population(christiansufferterrahumanitarianorganization,native,n85) ).
cnf(u1222,axiom,
accept_number(countryamedicalorganization,n4) ).
cnf(u712,axiom,
( accept_population(X0,native,n15)
| ~ accept_city(X0,northport) ) ).
cnf(u1313,axiom,
accept_number(sufferterragovernment,n6) ).
cnf(u1353,axiom,
accept_population(christiancountrychumanitarianorganization,other,n0) ).
cnf(u1107,axiom,
accept_population(countryafirstaidorganization,christian,n3) ).
cnf(u862,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1245,axiom,
accept_number(countryahumanitarianorganization,n5) ).
cnf(u1096,axiom,
accept_city(christiansufferterrahumanitarianorganization,coastvillage) ).
cnf(u975,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1226,axiom,
accept_population(countryamedicalorganization,other,n0) ).
cnf(u868,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1134,axiom,
accept_city(countrybhumanitarianorganization,townc) ).
cnf(u1220,axiom,
accept_leader(countryamedicalorganization,countrybhumanitarianorganization) ).
cnf(u1127,axiom,
accept_population(countrybhumanitarianorganization,atheist,n12) ).
cnf(u873,axiom,
~ accept_team(countryccivilorganization,countrybcivilorganization,townc,n6) ).
cnf(u970,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6) ).
cnf(u2761,axiom,
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,atheist,n75)
| ~ accept_population(X0,christian,n25)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,citya) ) ).
cnf(u1235,axiom,
accept_population(countryacivilorganization,christian,n20) ).
cnf(u990,axiom,
any_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna) ).
cnf(u3045,axiom,
( ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,christian,n20)
| ~ accept_city(X0,northport)
| accept_city(X0,townb)
| ~ accept_city(X0,towna) ) ).
cnf(u887,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1224,axiom,
accept_number(countryamedicalorganization,n2) ).
cnf(u2657,axiom,
~ accept_city(countryamedicalorganization,citya) ).
cnf(u1132,axiom,
accept_population(countrybhumanitarianorganization,christian,n0) ).
cnf(u3043,axiom,
( ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,christian,n20)
| ~ accept_city(X0,northport)
| accept_city(X0,townb)
| ~ accept_city(X0,citya) ) ).
cnf(u1262,axiom,
accept_population(sufferterragovernment,christian,n20) ).
cnf(u716,axiom,
( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n85)
| accept_city(X0,coastvillage) ) ).
cnf(u733,axiom,
( accept_population(X0,atheist,n75)
| ~ accept_city(X0,towna) ) ).
cnf(u1255,axiom,
accept_number(countryahumanitarianorganization,n6) ).
cnf(u1001,axiom,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1147,axiom,
accept_leader(sufferterragovernment,countryafirstaidorganization) ).
cnf(u731,axiom,
( accept_population(X0,muslim,n1)
| ~ accept_city(X0,towna) ) ).
cnf(u1136,axiom,
accept_leader(countrybhumanitarianorganization,countryccivilorganization) ).
cnf(u1330,axiom,
accept_number(countryccivilorganization,n4) ).
cnf(u1260,axiom,
accept_population(sufferterragovernment,native,n0) ).
cnf(u877,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc) ).
cnf(u2924,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,townb) ) ).
cnf(u875,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u750,axiom,
( accept_population(X0,christian,n20)
| ~ accept_city(X0,cityb) ) ).
cnf(u1661,axiom,
( ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n25)
| accept_city(X0,citya)
| ~ accept_city(X0,towna) ) ).
cnf(u1264,axiom,
accept_city(sufferterragovernment,cityb) ).
cnf(u723,axiom,
( accept_population(X0,other,n0)
| ~ accept_city(X0,sunsetpoint) ) ).
cnf(u1044,axiom,
accept_population(countrybcivilorganization,native,n85) ).
cnf(u756,axiom,
( accept_population(X0,christian,n0)
| ~ accept_city(X0,townc) ) ).
cnf(u1370,axiom,
accept_number(muslimcountrybhumanitarianorganization,n1) ).
cnf(u1065,axiom,
accept_population(countryccivilorganization,other,n1) ).
cnf(u1005,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u890,axiom,
any_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc) ).
cnf(u1003,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1146,axiom,
accept_leader(countrybhumanitarianorganization,sufferterragovernment) ).
cnf(u768,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u932,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2) ).
cnf(u789,axiom,
~ accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2) ).
cnf(u1311,axiom,
accept_number(sufferterragovernment,n2) ).
cnf(u683,axiom,
( accept_population(X0,muslim,n7)
| ~ accept_city(X0,suffertown) ) ).
cnf(u1282,axiom,
accept_population(countryafirstaidorganization,atheist,n75) ).
cnf(u787,axiom,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2) ).
cnf(u896,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1025,axiom,
accept_leader(countryamedicalorganization,countryahumanitarianorganization) ).
cnf(u917,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1439,axiom,
( ~ accept_population(X0,native,n85)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,muslim,n0)
| ~ accept_city(X0,towna)
| accept_city(X0,coastvillage) ) ).
cnf(u1290,axiom,
accept_population(countrycmedicalorganization,other,n0) ).
cnf(u915,axiom,
the_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1318,axiom,
accept_number(countryacivilorganization,n1) ).
cnf(u808,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1153,axiom,
accept_city(sufferterragovernment,coastvillage) ).
cnf(u829,axiom,
~ accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u740,axiom,
( ~ accept_population(X0,other,n2)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,native,n0)
| accept_city(X0,townb) ) ).
cnf(u1061,axiom,
accept_population(sufferterragovernment,christian,n24) ).
cnf(u930,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1042,axiom,
accept_city(countrycmedicalorganization,coastvillage) ).
cnf(u1316,axiom,
accept_number(countryacivilorganization,n3) ).
cnf(u2999,axiom,
( ~ accept_population(X0,native,n10)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n15)
| ~ accept_population(X0,muslim,n1)
| ~ accept_city(X0,suffertown)
| accept_city(X0,centrallakecity) ) ).
cnf(u673,axiom,
( ~ accept_team(X0,X3,X1,X2)
| accept_leader(X0,X3) ) ).
cnf(u806,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna) ).
cnf(u1189,axiom,
accept_leader(countrycmedicalorganization,muslimcountrybhumanitarianorganization) ).
cnf(u1320,axiom,
accept_population(countryacivilorganization,native,n0) ).
cnf(u687,axiom,
( accept_population(X0,other,n9)
| ~ accept_city(X0,centraltown) ) ).
cnf(u1170,axiom,
accept_number(christiansufferterrahumanitarianorganization,n5) ).
cnf(u713,axiom,
( accept_population(X0,muslim,n0)
| ~ accept_city(X0,northport) ) ).
cnf(u812,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1078,axiom,
accept_city(countryacivilorganization,coastvillage) ).
cnf(u1071,axiom,
accept_leader(countryccivilorganization,countryacivilorganization) ).
cnf(u2858,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townc) ) ).
cnf(u817,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u3267,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townb)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u769,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u934,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2) ).
cnf(u1333,axiom,
accept_number(countrybcivilorganization,n4) ).
cnf(u831,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1082,axiom,
accept_population(countryacivilorganization,christian,n0) ).
cnf(u1206,axiom,
accept_city(muslimcountrybhumanitarianorganization,townc) ).
cnf(u696,axiom,
( accept_population(X0,christian,n8)
| ~ accept_city(X0,sunnysideport) ) ).
cnf(u1199,axiom,
accept_city(countrycmedicalorganization,cityb) ).
cnf(u945,axiom,
accept_team(countryamedicalorganization,sufferterragovernment,towna,n5) ).
cnf(u1101,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n0) ).
cnf(u1080,axiom,
accept_population(countryacivilorganization,other,n5) ).
cnf(u959,axiom,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1210,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1) ).
cnf(u1356,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n24) ).
cnf(u1204,axiom,
accept_population(muslimcountrybhumanitarianorganization,christian,n0) ).
cnf(u1052,axiom,
accept_population(countrybcivilorganization,christian,n0) ).
cnf(u1241,axiom,
accept_population(countryahumanitarianorganization,christian,n20) ).
cnf(u1091,axiom,
accept_population(christiansufferterrahumanitarianorganization,other,n0) ).
cnf(u1229,axiom,
accept_population(countryamedicalorganization,christian,n24) ).
cnf(u1360,axiom,
accept_number(countrycmedicalorganization,n5) ).
cnf(u1208,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n1) ).
cnf(u852,axiom,
any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1118,axiom,
accept_population(countryafirstaidorganization,other,n1) ).
cnf(u1297,axiom,
accept_leader(countrybcivilorganization,countryccivilorganization) ).
cnf(u1111,axiom,
accept_population(countryafirstaidorganization,other,n5) ).
cnf(u857,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,townc,n6) ).
cnf(u1219,axiom,
accept_city(countryamedicalorganization,cityb) ).
cnf(u974,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1373,axiom,
accept_leader(muslimcountrybhumanitarianorganization,sufferterragovernment) ).
cnf(u871,axiom,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u2759,axiom,
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,atheist,n75)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,muslim,n1)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna) ) ).
cnf(u2766,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,townc) ) ).
cnf(u980,axiom,
accept_team(countryacivilorganization,sufferterragovernment,towna,n5) ).
cnf(u1246,axiom,
accept_number(countryahumanitarianorganization,n4) ).
cnf(u1323,axiom,
accept_population(countryacivilorganization,atheist,n75) ).
cnf(u717,axiom,
( accept_population(X0,other,n0)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u1239,axiom,
accept_leader(countryahumanitarianorganization,countryacivilorganization) ).
cnf(u985,axiom,
accept_team(countrycmedicalorganization,countryccivilorganization,towna,n4) ).
cnf(u1131,axiom,
accept_population(countrybhumanitarianorganization,muslim,n65) ).
cnf(u1363,axiom,
accept_number(countrycmedicalorganization,n2) ).
cnf(u1120,axiom,
accept_population(countryafirstaidorganization,atheist,n78) ).
cnf(u1244,axiom,
accept_leader(countryahumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u861,axiom,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1314,axiom,
accept_number(countryacivilorganization,n5) ).
cnf(u859,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u734,axiom,
( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,atheist,n75)
| ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n0)
| accept_city(X0,citya) ) ).
cnf(u1248,axiom,
accept_number(countryahumanitarianorganization,n2) ).
cnf(u1028,axiom,
accept_leader(countryahumanitarianorganization,countryafirstaidorganization) ).
cnf(u757,axiom,
( accept_population(X0,atheist,n30)
| ~ accept_city(X0,townc) ) ).
cnf(u989,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna) ).
cnf(u874,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u755,axiom,
( accept_population(X0,muslim,n65)
| ~ accept_city(X0,townc) ) ).
cnf(u881,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,townc,n6) ).
cnf(u1113,axiom,
accept_population(countryafirstaidorganization,christian,n0) ).
cnf(u880,axiom,
accept_team(countrybhumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u773,axiom,
accept_team(countryafirstaidorganization,countryacivilorganization,cityb,n6) ).
cnf(u1295,axiom,
accept_city(countrycmedicalorganization,towna) ).
cnf(u2735,axiom,
~ accept_city(christiancountrychumanitarianorganization,northport) ).
cnf(u771,axiom,
accept_team(countryamedicalorganization,countryacivilorganization,cityb,n6) ).
cnf(u714,axiom,
( accept_population(X0,christian,n13)
| ~ accept_city(X0,northport) ) ).
cnf(u1008,axiom,
accept_leader(christiancountrychumanitarianorganization,muslimcountrybhumanitarianorganization) ).
cnf(u2836,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,centrallakecity)
| ~ accept_city(X0,citya)
| accept_city(X0,towna) ) ).
cnf(u1137,axiom,
accept_leader(countrybhumanitarianorganization,countrybcivilorganization) ).
cnf(u2683,axiom,
( ~ accept_population(X0,native,n85)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_city(X0,citya)
| accept_city(X0,coastvillage) ) ).
cnf(u901,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u786,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2) ).
cnf(u759,axiom,
accept_team(countryahumanitarianorganization,countryacivilorganization,towna,n6) ).
cnf(u899,axiom,
any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1302,axiom,
accept_population(countrybcivilorganization,native,n0) ).
cnf(u792,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1369,axiom,
accept_number(muslimcountrybhumanitarianorganization,n2) ).
cnf(u3345,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,centrallakecity)
| ~ accept_city(X0,suffertown) ) ).
cnf(u1574,axiom,
( ~ accept_population(X0,native,n100)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0)
| accept_city(X0,sunsetpoint)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u1045,axiom,
accept_population(countrybcivilorganization,muslim,n0) ).
cnf(u1306,axiom,
accept_city(countrybcivilorganization,towna) ).
cnf(u1520,axiom,
accept_leader(countryccivilorganization,countrycmedicalorganization) ).
cnf(u762,axiom,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u2579,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_city(X0,townb)
| ~ accept_population(X0,atheist,n75)
| accept_city(X0,citya)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u1300,axiom,
accept_leader(countrybcivilorganization,countrycmedicalorganization) ).
cnf(u1049,axiom,
accept_leader(countrybcivilorganization,muslimcountrybhumanitarianorganization) ).
cnf(u790,axiom,
~ accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2) ).
cnf(u1173,axiom,
accept_number(christiansufferterrahumanitarianorganization,n2) ).
cnf(u1304,axiom,
accept_population(countrybcivilorganization,christian,n24) ).
cnf(u1154,axiom,
accept_leader(sufferterragovernment,christiancountrychumanitarianorganization) ).
cnf(u796,axiom,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n4) ).
cnf(u3022,axiom,
( ~ accept_population(X0,native,n4)
| ~ accept_population(X0,atheist,n65)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n7)
| ~ accept_city(X0,stjosephburgh)
| accept_city(X0,suffertown) ) ).
cnf(u1062,axiom,
accept_population(sufferterragovernment,atheist,n75) ).
cnf(u3028,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,citya)
| ~ accept_city(X0,cityb) ) ).
cnf(u1055,axiom,
accept_leader(countrybcivilorganization,countryahumanitarianorganization) ).
cnf(u801,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1085,axiom,
accept_city(countryacivilorganization,townc) ).
cnf(u2837,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,centrallakecity)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna) ) ).
cnf(u918,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1317,axiom,
accept_number(countryacivilorganization,n2) ).
cnf(u815,axiom,
accept_team(countryafirstaidorganization,countryacivilorganization,towna,n6) ).
cnf(u674,axiom,
( ~ accept_team(X0,X3,X1,X2)
| accept_city(X0,X1) ) ).
cnf(u1340,axiom,
accept_number(countrybhumanitarianorganization,n4) ).
cnf(u924,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1190,axiom,
accept_population(countrycmedicalorganization,other,n5) ).
cnf(u680,axiom,
( ~ accept_population(X0,other,n4)
| ~ accept_population(X0,atheist,n65)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n7)
| ~ accept_population(X0,native,n4)
| accept_city(X0,suffertown) ) ).
cnf(u1183,axiom,
accept_population(countryccivilorganization,other,n5) ).
cnf(u1321,axiom,
accept_population(countryacivilorganization,muslim,n1) ).
cnf(u1075,axiom,
accept_population(countryacivilorganization,muslim,n0) ).
cnf(u1213,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u2575,axiom,
( ~ accept_population(X0,native,n15)
| ~ accept_population(X0,christian,n13)
| ~ accept_population(X0,muslim,n0)
| ~ accept_city(X0,townb)
| accept_city(X0,northport) ) ).
cnf(u1064,axiom,
~ accept_number(countryccivilorganization,n5) ).
cnf(u943,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1194,axiom,
accept_city(countrycmedicalorganization,townc) ).
cnf(u1188,axiom,
accept_leader(countryccivilorganization,countryahumanitarianorganization) ).
cnf(u2602,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna)
| ~ accept_city(X0,cityb) ) ).
cnf(u1203,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n65) ).
cnf(u958,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1344,axiom,
accept_number(countrybhumanitarianorganization,n6) ).
cnf(u1192,axiom,
accept_population(countrycmedicalorganization,christian,n0) ).
cnf(u836,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1102,axiom,
accept_population(muslimcountrybhumanitarianorganization,christian,n3) ).
cnf(u684,axiom,
( accept_population(X0,christian,n20)
| ~ accept_city(X0,suffertown) ) ).
cnf(u701,axiom,
( accept_population(X0,muslim,n1)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u1095,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n12) ).
cnf(u841,axiom,
accept_team(sufferterragovernment,countryacivilorganization,coastvillage,n6) ).
cnf(u699,axiom,
( accept_population(X0,other,n4)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u1357,axiom,
accept_population(christiancountrychumanitarianorganization,atheist,n75) ).
cnf(u1281,axiom,
accept_population(countryafirstaidorganization,christian,n24) ).
cnf(u2736,axiom,
~ accept_city(countryccivilorganization,northport) ).
cnf(u964,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1230,axiom,
accept_population(countryamedicalorganization,atheist,n75) ).
cnf(u1223,axiom,
accept_number(countryamedicalorganization,n3) ).
cnf(u1361,axiom,
accept_number(countrycmedicalorganization,n4) ).
cnf(u1115,axiom,
accept_leader(countryafirstaidorganization,countryahumanitarianorganization) ).
cnf(u1347,axiom,
accept_number(christiancountrychumanitarianorganization,n5) ).
cnf(u1104,axiom,
accept_city(muslimcountrybhumanitarianorganization,coastvillage) ).
cnf(u3026,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,citya)
| ~ accept_city(X0,townb) ) ).
cnf(u1240,axiom,
accept_population(countryahumanitarianorganization,other,n1) ).
cnf(u1228,axiom,
accept_population(countryamedicalorganization,muslim,n1) ).
cnf(u835,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1367,axiom,
accept_number(muslimcountrybhumanitarianorganization,n4) ).
cnf(u843,axiom,
the_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u718,axiom,
( accept_population(X0,native,n85)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u1232,axiom,
accept_leader(countryamedicalorganization,sufferterragovernment) ).
cnf(u1140,axiom,
accept_population(countrybhumanitarianorganization,other,n0) ).
cnf(u3266,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townb)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u724,axiom,
( accept_population(X0,native,n100)
| ~ accept_city(X0,sunsetpoint) ) ).
cnf(u741,axiom,
( accept_population(X0,other,n2)
| ~ accept_city(X0,townb) ) ).
cnf(u973,axiom,
~ accept_team(countryccivilorganization,countrybcivilorganization,towna,n6) ).
cnf(u1338,axiom,
accept_leader(christiancountrychumanitarianorganization,countrybcivilorganization) ).
cnf(u858,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u739,axiom,
( accept_population(X0,atheist,n75)
| ~ accept_city(X0,citya) ) ).
cnf(u864,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u885,axiom,
accept_team(countrycmedicalorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u986,axiom,
accept_team(countrycmedicalorganization,countrybcivilorganization,towna,n6) ).
cnf(u883,axiom,
accept_team(countryamedicalorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u758,axiom,
accept_team(countryahumanitarianorganization,countryacivilorganization,cityb,n6) ).
cnf(u1121,axiom,
accept_city(countryafirstaidorganization,cityb) ).
cnf(u1372,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,towna) ).
cnf(u1013,axiom,
accept_city(christiancountrychumanitarianorganization,townc) ).
cnf(u1656,axiom,
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75)
| accept_city(X0,citya)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u770,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u900,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u743,axiom,
( accept_population(X0,muslim,n8)
| ~ accept_city(X0,townb) ) ).
cnf(u1011,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n0) ).
cnf(u1286,axiom,
accept_leader(countrycmedicalorganization,countryccivilorganization) ).
cnf(u776,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,cityb,n6) ).
cnf(u2839,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,centrallakecity)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna)
| ~ accept_city(X0,townc) ) ).
cnf(u691,axiom,
( accept_population(X0,atheist,n54)
| ~ accept_city(X0,centraltown) ) ).
cnf(u1249,axiom,
accept_number(countryahumanitarianorganization,n1) ).
cnf(u1029,axiom,
accept_population(countryahumanitarianorganization,native,n85) ).
cnf(u898,axiom,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u746,axiom,
( ~ accept_population(X0,other,n1)
| ~ accept_population(X0,atheist,n78)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,native,n0)
| accept_city(X0,cityb) ) ).
cnf(u1284,axiom,
accept_leader(countryafirstaidorganization,sufferterragovernment) ).
cnf(u752,axiom,
( ~ accept_population(X0,other,n5)
| ~ accept_population(X0,atheist,n30)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,muslim,n65)
| ~ accept_population(X0,native,n0)
| accept_city(X0,townc) ) ).
cnf(u1033,axiom,
accept_city(countryahumanitarianorganization,coastvillage) ).
cnf(u2580,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,atheist,n75)
| ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,townb)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna) ) ).
cnf(u2597,axiom,
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n8)
| ~ accept_city(X0,northport)
| accept_city(X0,townb) ) ).
cnf(u1145,axiom,
accept_city(countrybhumanitarianorganization,towna) ).
cnf(u1288,axiom,
accept_leader(countrycmedicalorganization,countrybhumanitarianorganization) ).
cnf(u1266,axiom,
accept_population(countryccivilorganization,other,n0) ).
cnf(u780,axiom,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1046,axiom,
accept_population(countrybcivilorganization,christian,n3) ).
cnf(u1039,axiom,
accept_population(countrycmedicalorganization,muslim,n0) ).
cnf(u1161,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countryccivilorganization) ).
cnf(u1069,axiom,
accept_leader(countryccivilorganization,countrybhumanitarianorganization) ).
cnf(u1275,axiom,
accept_number(countryafirstaidorganization,n3) ).
cnf(u902,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,cityb,n6) ).
cnf(u1301,axiom,
accept_population(countrybcivilorganization,other,n0) ).
cnf(u799,axiom,
any_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna) ).
cnf(u1050,axiom,
accept_population(countrybcivilorganization,other,n5) ).
cnf(u1324,axiom,
accept_number(countryacivilorganization,n6) ).
cnf(u908,axiom,
any_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1174,axiom,
accept_number(christiansufferterrahumanitarianorganization,n1) ).
cnf(u1073,axiom,
accept_leader(countryacivilorganization,countryafirstaidorganization) ).
cnf(u1167,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1305,axiom,
accept_population(countrybcivilorganization,atheist,n75) ).
cnf(u1059,axiom,
accept_city(countrybcivilorganization,cityb) ).
cnf(u814,axiom,
any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1197,axiom,
accept_population(countrycmedicalorganization,christian,n20) ).
cnf(u1328,axiom,
accept_number(countryccivilorganization,n2) ).
cnf(u1048,axiom,
accept_city(countrybcivilorganization,coastvillage) ).
cnf(u927,axiom,
any_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1178,axiom,
accept_population(christiansufferterrahumanitarianorganization,muslim,n1) ).
cnf(u820,axiom,
the_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1086,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n24) ).
cnf(u1172,axiom,
accept_number(christiansufferterrahumanitarianorganization,n3) ).
cnf(u1079,axiom,
accept_leader(countryacivilorganization,christiancountrychumanitarianorganization) ).
cnf(u738,axiom,
( accept_population(X0,christian,n25)
| ~ accept_city(X0,citya) ) ).
cnf(u825,axiom,
accept_team(countryafirstaidorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1187,axiom,
accept_city(countryccivilorganization,townc) ).
cnf(u942,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6) ).
cnf(u1341,axiom,
accept_number(countrybhumanitarianorganization,n3) ).
cnf(u1176,axiom,
accept_population(christiansufferterrahumanitarianorganization,other,n1) ).
cnf(u2727,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,citya)
| ~ accept_city(X0,towna) ) ).
cnf(u1084,axiom,
accept_leader(countryacivilorganization,countryahumanitarianorganization) ).
cnf(u1214,axiom,
accept_city(muslimcountrybhumanitarianorganization,cityb) ).
cnf(u685,axiom,
( accept_population(X0,atheist,n65)
| ~ accept_city(X0,suffertown) ) ).
cnf(u1207,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ).
cnf(u953,axiom,
accept_team(countrybhumanitarianorganization,countryccivilorganization,towna,n3) ).
cnf(u1331,axiom,
accept_leader(christiancountrychumanitarianorganization,countryccivilorganization) ).
cnf(u977,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna) ).
cnf(u839,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1012,axiom,
accept_population(christiancountrychumanitarianorganization,atheist,n30) ).
cnf(u2737,axiom,
~ accept_city(countryamedicalorganization,northport) ).
cnf(u1212,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n78) ).
cnf(u763,axiom,
any_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1345,axiom,
accept_leader(christiancountrychumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u1099,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n0) ).
cnf(u827,axiom,
any_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u702,axiom,
( accept_population(X0,christian,n15)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u1088,axiom,
~ accept_leader(christiansufferterrahumanitarianorganization,sufferterragovernment) ).
cnf(u2647,axiom,
~ accept_city(christiancountrychumanitarianorganization,centraltown) ).
cnf(u3250,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townc)
| ~ accept_city(X0,centrallakecity)
| ~ accept_city(X0,townb) ) ).
cnf(u2998,axiom,
( ~ accept_population(X0,native,n11)
| ~ accept_population(X0,atheist,n68)
| ~ accept_population(X0,christian,n16)
| ~ accept_population(X0,muslim,n1)
| ~ accept_city(X0,suffertown)
| accept_city(X0,stjosephburgh) ) ).
cnf(u957,axiom,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1351,axiom,
accept_number(christiancountrychumanitarianorganization,n1) ).
cnf(u1291,axiom,
accept_population(countrycmedicalorganization,native,n0) ).
cnf(u955,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n6) ).
cnf(u1216,axiom,
accept_population(countryamedicalorganization,other,n1) ).
cnf(u1124,axiom,
accept_population(countrybhumanitarianorganization,native,n85) ).
cnf(u708,axiom,
( accept_population(X0,christian,n16)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u725,axiom,
( accept_population(X0,muslim,n0)
| ~ accept_city(X0,sunsetpoint) ) ).
cnf(u2648,axiom,
~ accept_city(countryccivilorganization,centraltown) ).
cnf(u962,axiom,
accept_team(countrybcivilorganization,countryccivilorganization,towna,n4) ).
cnf(u842,axiom,
accept_team(sufferterragovernment,countryafirstaidorganization,coastvillage,n6) ).
cnf(u1371,axiom,
accept_number(muslimcountrybhumanitarianorganization,n6) ).
cnf(u1358,axiom,
accept_city(christiancountrychumanitarianorganization,towna) ).
cnf(u848,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u3018,axiom,
( ~ accept_population(X0,native,n11)
| ~ accept_population(X0,atheist,n68)
| ~ accept_population(X0,christian,n16)
| ~ accept_city(X0,centrallakecity)
| accept_city(X0,stjosephburgh) ) ).
cnf(u1322,axiom,
accept_population(countryacivilorganization,christian,n24) ).
cnf(u869,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,townc,n6) ).
cnf(u3023,axiom,
( ~ accept_population(X0,native,n10)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n15)
| ~ accept_city(X0,stjosephburgh)
| accept_city(X0,centrallakecity) ) ).
cnf(u1362,axiom,
accept_number(countrycmedicalorganization,n3) ).
cnf(u867,axiom,
accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,townc,n6) ).
cnf(u742,axiom,
( accept_population(X0,native,n0)
| ~ accept_city(X0,townb) ) ).
cnf(u2653,axiom,
~ accept_city(sufferterragovernment,centraltown) ).
cnf(u976,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6) ).
cnf(u849,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1105,axiom,
accept_population(countryafirstaidorganization,native,n85) ).
cnf(u2651,axiom,
~ accept_city(countrybcivilorganization,centraltown) ).
cnf(u997,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u882,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u727,axiom,
( accept_population(X0,atheist,n0)
| ~ accept_city(X0,sunsetpoint) ) ).
cnf(u995,axiom,
accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,towna,n6) ).
cnf(u888,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1337,axiom,
accept_number(countrybcivilorganization,n6) ).
cnf(u2779,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,cityb) ) ).
cnf(u1141,axiom,
accept_population(countrybhumanitarianorganization,native,n0) ).
cnf(u1010,axiom,
accept_population(christiancountrychumanitarianorganization,muslim,n65) ).
cnf(u1122,axiom,
accept_leader(countryafirstaidorganization,countrybhumanitarianorganization) ).
cnf(u2925,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,townc) ) ).
cnf(u736,axiom,
( accept_population(X0,native,n0)
| ~ accept_city(X0,citya) ) ).
cnf(u753,axiom,
( accept_population(X0,other,n5)
| ~ accept_city(X0,townc) ) ).
cnf(u2923,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_city(X0,citya)
| accept_city(X0,towna) ) ).
cnf(u886,axiom,
accept_team(countrycmedicalorganization,countrybcivilorganization,townc,n6) ).
cnf(u1269,axiom,
accept_population(countryccivilorganization,christian,n24) ).
cnf(u767,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1250,axiom,
accept_population(countryahumanitarianorganization,other,n0) ).
cnf(u892,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1030,axiom,
accept_population(countryahumanitarianorganization,muslim,n0) ).
cnf(u1151,axiom,
accept_population(sufferterragovernment,christian,n3) ).
cnf(u1273,axiom,
accept_number(countryafirstaidorganization,n5) ).
cnf(u1053,axiom,
accept_population(countrybcivilorganization,atheist,n30) ).
cnf(u1259,axiom,
accept_population(sufferterragovernment,other,n1) ).
cnf(u1014,axiom,
accept_leader(christiancountrychumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1285,axiom,
accept_city(countryafirstaidorganization,towna) ).
cnf(u783,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6) ).
cnf(u1034,axiom,
accept_leader(countryahumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u1308,axiom,
accept_number(sufferterragovernment,n5) ).
cnf(u1020,axiom,
accept_leader(countryamedicalorganization,christiancountrychumanitarianorganization) ).
cnf(u1158,axiom,
accept_population(sufferterragovernment,atheist,n30) ).
cnf(u3359,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_city(X0,suffertown) ) ).
cnf(u1057,axiom,
accept_population(countrybcivilorganization,christian,n20) ).
cnf(u1279,axiom,
accept_population(countryafirstaidorganization,native,n0) ).
cnf(u1289,axiom,
accept_leader(countrycmedicalorganization,christiancountrychumanitarianorganization) ).
cnf(u1043,axiom,
accept_leader(countrybcivilorganization,countryacivilorganization) ).
cnf(u798,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna) ).
cnf(u1181,axiom,
accept_city(christiansufferterrahumanitarianorganization,cityb) ).
cnf(u1312,axiom,
accept_number(sufferterragovernment,n1) ).
cnf(u1032,axiom,
accept_population(countryahumanitarianorganization,atheist,n12) ).
cnf(u911,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1162,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countrybcivilorganization) ).
cnf(u804,axiom,
any_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna) ).
cnf(u1070,axiom,
accept_city(countryccivilorganization,cityb) ).
cnf(u1156,axiom,
accept_population(sufferterragovernment,muslim,n65) ).
cnf(u705,axiom,
( accept_population(X0,other,n4)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u1063,axiom,
accept_city(sufferterragovernment,towna) ).
cnf(u2697,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,citya)
| accept_city(X0,towna)
| ~ accept_city(X0,cityb) ) ).
cnf(u1171,axiom,
accept_number(christiansufferterrahumanitarianorganization,n4) ).
cnf(u926,axiom,
the_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1325,axiom,
accept_leader(countryacivilorganization,sufferterragovernment) ).
cnf(u3232,axiom,
( ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u823,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1160,axiom,
accept_city(sufferterragovernment,townc) ).
cnf(u737,axiom,
( accept_population(X0,muslim,n0)
| ~ accept_city(X0,citya) ) ).
cnf(u1068,axiom,
~ accept_number(countryccivilorganization,n6) ).
cnf(u1198,axiom,
accept_population(countrycmedicalorganization,atheist,n78) ).
cnf(u2872,axiom,
( ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,towna) ) ).
cnf(u1191,axiom,
accept_population(countrycmedicalorganization,muslim,n65) ).
cnf(u1329,axiom,
accept_number(countryccivilorganization,n1) ).
cnf(u1083,axiom,
accept_population(countryacivilorganization,atheist,n30) ).
cnf(u1315,axiom,
accept_number(countryacivilorganization,n4) ).
cnf(u1072,axiom,
accept_leader(countryacivilorganization,countryamedicalorganization) ).
cnf(u951,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3) ).
cnf(u1196,axiom,
accept_population(countrycmedicalorganization,other,n1) ).
cnf(u2854,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,citya) ) ).
cnf(u813,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1335,axiom,
accept_number(countrybcivilorganization,n2) ).
cnf(u1015,axiom,
accept_population(christiancountrychumanitarianorganization,other,n1) ).
cnf(u1211,axiom,
accept_population(muslimcountrybhumanitarianorganization,christian,n20) ).
cnf(u686,axiom,
( ~ accept_population(X0,other,n9)
| ~ accept_population(X0,atheist,n54)
| ~ accept_population(X0,christian,n23)
| ~ accept_population(X0,muslim,n3)
| ~ accept_population(X0,native,n1)
| accept_city(X0,centraltown) ) ).
cnf(u1200,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countrycmedicalorganization) ).
cnf(u920,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u2873,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townb) ) ).
cnf(u692,axiom,
( ~ accept_population(X0,other,n1)
| ~ accept_population(X0,atheist,n30)
| ~ accept_population(X0,christian,n8)
| ~ accept_population(X0,muslim,n60)
| ~ accept_population(X0,native,n1)
| accept_city(X0,sunnysideport) ) ).
cnf(u941,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4) ).
cnf(u3249,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townc)
| ~ accept_city(X0,centrallakecity)
| ~ accept_city(X0,suffertown) ) ).
cnf(u826,axiom,
the_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u939,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2) ).
cnf(u1342,axiom,
accept_number(countrybhumanitarianorganization,n2) ).
cnf(u3047,axiom,
( ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,christian,n20)
| ~ accept_city(X0,northport)
| accept_city(X0,townb)
| ~ accept_city(X0,townc) ) ).
cnf(u709,axiom,
( accept_population(X0,atheist,n68)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u1355,axiom,
accept_population(christiancountrychumanitarianorganization,muslim,n1) ).
cnf(u832,axiom,
accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1018,axiom,
accept_city(christiancountrychumanitarianorganization,cityb) ).
cnf(u697,axiom,
( accept_population(X0,atheist,n30)
| ~ accept_city(X0,sunnysideport) ) ).
cnf(u853,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u2760,axiom,
( ~ accept_population(X0,native,n85)
| ~ accept_population(X0,atheist,n12)
| ~ accept_population(X0,christian,n3)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,coastvillage) ) ).
cnf(u1346,axiom,
accept_leader(christiancountrychumanitarianorganization,countrycmedicalorganization) ).
cnf(u851,axiom,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u726,axiom,
( accept_population(X0,christian,n0)
| ~ accept_city(X0,sunsetpoint) ) ).
cnf(u2926,axiom,
( ~ accept_population(X0,christian,n20)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townc) ) ).
cnf(u1089,axiom,
accept_city(christiansufferterrahumanitarianorganization,towna) ).
cnf(u866,axiom,
accept_team(christiancountrychumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u2921,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_city(X0,townb)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna) ) ).
cnf(u711,axiom,
( accept_population(X0,other,n2)
| ~ accept_city(X0,northport) ) ).
cnf(u3283,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townc)
| ~ accept_city(X0,suffertown) ) ).
cnf(u872,axiom,
~ accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u1217,axiom,
accept_population(countryamedicalorganization,christian,n20) ).
cnf(u2763,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,townb) ) ).
cnf(u1125,axiom,
accept_population(countrybhumanitarianorganization,muslim,n0) ).
cnf(u1106,axiom,
accept_population(countryafirstaidorganization,muslim,n0) ).
cnf(u720,axiom,
( accept_population(X0,christian,n3)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u1129,axiom,
accept_leader(countrybhumanitarianorganization,muslimcountrybhumanitarianorganization) ).
cnf(u1116,axiom,
accept_city(countryafirstaidorganization,townc) ).
cnf(u937,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3) ).
cnf(u2907,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,towna)
| ~ accept_city(X0,townb) ) ).
cnf(u870,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1253,axiom,
accept_population(countryahumanitarianorganization,christian,n24) ).
cnf(u1384,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna)
| ~ accept_city(X0,townc) ) ).
cnf(u751,axiom,
( accept_population(X0,atheist,n78)
| ~ accept_city(X0,cityb) ) ).
cnf(u1234,axiom,
accept_population(countryacivilorganization,other,n1) ).
cnf(u876,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1142,axiom,
accept_population(countrybhumanitarianorganization,muslim,n1) ).
cnf(u1135,axiom,
accept_leader(countrybhumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1257,axiom,
accept_city(countryahumanitarianorganization,towna) ).
cnf(u1037,axiom,
accept_leader(countrycmedicalorganization,countryacivilorganization) ).
cnf(u1243,axiom,
accept_city(countryahumanitarianorganization,cityb) ).
cnf(u998,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n6) ).
cnf(u895,axiom,
any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u754,axiom,
( accept_population(X0,native,n0)
| ~ accept_city(X0,townc) ) ).
cnf(u1292,axiom,
accept_population(countrycmedicalorganization,muslim,n1) ).
cnf(u1270,axiom,
accept_population(countryccivilorganization,atheist,n75) ).
cnf(u760,axiom,
accept_team(countryahumanitarianorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1041,axiom,
accept_population(countrycmedicalorganization,atheist,n12) ).
cnf(u1263,axiom,
accept_population(sufferterragovernment,atheist,n78) ).
cnf(u1009,axiom,
accept_population(christiancountrychumanitarianorganization,other,n5) ).
cnf(u1027,axiom,
accept_leader(countryahumanitarianorganization,countryamedicalorganization) ).
cnf(u782,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1165,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n0) ).
cnf(u1296,axiom,
accept_leader(countrycmedicalorganization,sufferterragovernment) ).
cnf(u1144,axiom,
accept_population(countrybhumanitarianorganization,atheist,n75) ).
cnf(u1023,axiom,
accept_population(countryamedicalorganization,christian,n0) ).
cnf(u1274,axiom,
accept_number(countryafirstaidorganization,n4) ).
cnf(u788,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2) ).
cnf(u2835,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,centrallakecity)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,townc) ) ).
cnf(u1054,axiom,
accept_city(countrybcivilorganization,townc) ).
cnf(u1268,axiom,
accept_population(countryccivilorganization,muslim,n1) ).
cnf(u1047,axiom,
accept_population(countrybcivilorganization,atheist,n12) ).
cnf(u793,axiom,
~ accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u1155,axiom,
accept_population(sufferterragovernment,other,n5) ).
cnf(u910,axiom,
accept_team(countryafirstaidorganization,sufferterragovernment,towna,n6) ).
cnf(u1309,axiom,
accept_number(sufferterragovernment,n4) ).
cnf(u807,axiom,
any_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna) ).
cnf(u1272,axiom,
accept_leader(countryccivilorganization,sufferterragovernment) ).
cnf(u916,axiom,
any_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1182,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u764,axiom,
accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n2) ).
cnf(u1175,axiom,
accept_number(christiansufferterrahumanitarianorganization,n6) ).
cnf(u921,axiom,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1157,axiom,
accept_population(sufferterragovernment,christian,n0) ).
cnf(u1067,axiom,
accept_population(countryccivilorganization,atheist,n78) ).
cnf(u1299,axiom,
accept_leader(countrybcivilorganization,christiancountrychumanitarianorganization) ).
cnf(u706,axiom,
( accept_population(X0,native,n11)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u1056,axiom,
accept_population(countrybcivilorganization,other,n1) ).
cnf(u935,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3) ).
cnf(u1180,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n78) ).
cnf(u1177,axiom,
accept_population(christiansufferterrahumanitarianorganization,native,n0) ).
cnf(u2838,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,centrallakecity)
| ~ accept_city(X0,townb)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna) ) ).
cnf(u797,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1319,axiom,
accept_population(countryacivilorganization,other,n0) ).
cnf(u3029,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,citya)
| ~ accept_city(X0,townc) ) ).
cnf(u1195,axiom,
accept_leader(countrycmedicalorganization,countryahumanitarianorganization) ).
cnf(u795,axiom,
any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1184,axiom,
accept_population(countryccivilorganization,muslim,n65) ).
cnf(u904,axiom,
any_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb) ).
cnf(u1562,axiom,
( ~ accept_population(X0,native,n100)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,atheist,n0)
| accept_city(X0,sunsetpoint)
| ~ accept_city(X0,towna) ) ).
cnf(u676,axiom,
( ~ the_agent_in_all_proposed_teams(X0,X1,X2)
| accept_city(X0,X2) ) ).
cnf(u693,axiom,
( accept_population(X0,other,n1)
| ~ accept_city(X0,sunnysideport) ) ).
cnf(u810,axiom,
accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n4) ).
cnf(u1339,axiom,
accept_number(countrybhumanitarianorganization,n5) ).
cnf(u1326,axiom,
accept_city(countryacivilorganization,towna) ).
cnf(u3233,axiom,
( ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u938,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3) ).
cnf(u944,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u681,axiom,
( accept_population(X0,other,n4)
| ~ accept_city(X0,suffertown) ) ).
cnf(u837,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1359,axiom,
accept_leader(christiancountrychumanitarianorganization,sufferterragovernment) ).
cnf(u695,axiom,
( accept_population(X0,muslim,n60)
| ~ accept_city(X0,sunnysideport) ) ).
cnf(u987,axiom,
accept_team(countrycmedicalorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u761,axiom,
accept_team(countryahumanitarianorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u710,axiom,
( ~ accept_population(X0,other,n2)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n13)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n15)
| accept_city(X0,northport) ) ).
cnf(u2853,axiom,
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,atheist,n78)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n1)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb) ) ).
cnf(u1201,axiom,
accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u965,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n6) ).
cnf(u850,axiom,
accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u698,axiom,
( ~ accept_population(X0,other,n4)
| ~ accept_population(X0,atheist,n70)
| ~ accept_population(X0,christian,n15)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,native,n10)
| accept_city(X0,centrallakecity) ) ).
cnf(u963,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1366,axiom,
accept_number(muslimcountrybhumanitarianorganization,n5) ).
cnf(u1026,axiom,
accept_city(countryamedicalorganization,townc) ).
cnf(u1066,axiom,
accept_population(countryccivilorganization,christian,n20) ).
cnf(u1109,axiom,
accept_city(countryafirstaidorganization,coastvillage) ).
cnf(u2920,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,stjosephburgh)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna)
| ~ accept_city(X0,townc) ) ).
cnf(u978,axiom,
any_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna) ).
cnf(u1090,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryafirstaidorganization) ).
cnf(u1364,axiom,
accept_number(countrycmedicalorganization,n1) ).
cnf(u704,axiom,
( ~ accept_population(X0,other,n4)
| ~ accept_population(X0,atheist,n68)
| ~ accept_population(X0,christian,n16)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,native,n11)
| accept_city(X0,stjosephburgh) ) ).
cnf(u721,axiom,
( accept_population(X0,atheist,n12)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u2891,axiom,
( ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,townc)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u854,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1237,axiom,
accept_city(countryacivilorganization,cityb) ).
cnf(u1368,axiom,
accept_number(muslimcountrybhumanitarianorganization,n3) ).
cnf(u735,axiom,
( accept_population(X0,other,n0)
| ~ accept_city(X0,citya) ) ).
cnf(u967,axiom,
any_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna) ).
cnf(u1218,axiom,
accept_population(countryamedicalorganization,atheist,n78) ).
cnf(u860,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1126,axiom,
accept_population(countrybhumanitarianorganization,christian,n3) ).
cnf(u1100,axiom,
accept_population(muslimcountrybhumanitarianorganization,native,n85) ).
cnf(u1119,axiom,
accept_population(countryafirstaidorganization,christian,n20) ).
cnf(u2906,axiom,
( ~ accept_population(X0,atheist,n78)
| ~ accept_city(X0,sunnysideport)
| accept_city(X0,cityb)
| ~ accept_city(X0,towna)
| ~ accept_city(X0,suffertown) ) ).
cnf(u865,axiom,
accept_team(christiancountrychumanitarianorganization,countryccivilorganization,townc,n4) ).
cnf(u1149,axiom,
accept_population(sufferterragovernment,native,n85) ).
cnf(u1227,axiom,
accept_population(countryamedicalorganization,native,n0) ).
cnf(u982,axiom,
accept_team(countryacivilorganization,sufferterragovernment,towna,n6) ).
cnf(u1381,axiom,
( ~ accept_population(X0,native,n0)
| ~ accept_population(X0,atheist,n75)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,muslim,n1)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna) ) ).
cnf(u879,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n2) ).
cnf(u1130,axiom,
accept_population(countrybhumanitarianorganization,other,n5) ).
cnf(u2684,axiom,
( ~ accept_population(X0,native,n100)
| ~ accept_population(X0,atheist,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_city(X0,citya)
| accept_city(X0,sunsetpoint) ) ).
cnf(u988,axiom,
accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1254,axiom,
accept_population(countryahumanitarianorganization,atheist,n75) ).
cnf(u744,axiom,
( accept_population(X0,christian,n20)
| ~ accept_city(X0,townb) ) ).
cnf(u1247,axiom,
accept_number(countryahumanitarianorganization,n3) ).
cnf(u993,axiom,
accept_team(christiancountrychumanitarianorganization,countryccivilorganization,towna,n4) ).
cnf(u730,axiom,
( accept_population(X0,native,n0)
| ~ accept_city(X0,towna) ) ).
cnf(u1139,axiom,
accept_leader(countrybhumanitarianorganization,countrycmedicalorganization) ).
cnf(u894,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1277,axiom,
accept_number(countryafirstaidorganization,n1) ).
cnf(u1280,axiom,
accept_population(countryafirstaidorganization,muslim,n1) ).
cnf(u1128,axiom,
accept_city(countrybhumanitarianorganization,coastvillage) ).
cnf(u1007,axiom,
accept_leader(christiancountrychumanitarianorganization,countryacivilorganization) ).
cnf(u1258,axiom,
accept_leader(sufferterragovernment,countryacivilorganization) ).
cnf(u772,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ).
cnf(u1038,axiom,
accept_population(countrycmedicalorganization,native,n85) ).
cnf(u1252,axiom,
accept_population(countryahumanitarianorganization,muslim,n1) ).
cnf(u1031,axiom,
accept_population(countryahumanitarianorganization,christian,n3) ).
cnf(u2734,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_city(X0,northport)
| accept_city(X0,citya)
| ~ accept_city(X0,towna) ) ).
cnf(u777,axiom,
accept_team(sufferterragovernment,countryacivilorganization,cityb,n6) ).
cnf(u1267,axiom,
accept_population(countryccivilorganization,native,n0) ).
cnf(u1022,axiom,
accept_population(countryamedicalorganization,muslim,n65) ).
cnf(u1293,axiom,
accept_population(countrycmedicalorganization,christian,n24) ).
cnf(u791,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u2834,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,centrallakecity)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,sunsetpoint)
| accept_city(X0,towna)
| ~ accept_city(X0,townb) ) ).
cnf(u1256,axiom,
accept_leader(countryahumanitarianorganization,sufferterragovernment) ).
cnf(u1036,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryamedicalorganization) ).
cnf(u1166,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n30) ).
cnf(u748,axiom,
( accept_population(X0,native,n0)
| ~ accept_city(X0,cityb) ) ).
cnf(u765,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ).
cnf(u690,axiom,
( accept_population(X0,christian,n23)
| ~ accept_city(X0,centraltown) ) ).
cnf(u1159,axiom,
accept_leader(sufferterragovernment,countryahumanitarianorganization) ).
cnf(u905,axiom,
accept_team(countryafirstaidorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1051,axiom,
accept_population(countrybcivilorganization,muslim,n65) ).
cnf(u1283,axiom,
accept_number(countryafirstaidorganization,n6) ).
cnf(u1114,axiom,
accept_population(countryafirstaidorganization,atheist,n30) ).
cnf(u1040,axiom,
accept_population(countrycmedicalorganization,christian,n3) ).
cnf(u919,axiom,
accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1164,axiom,
accept_population(christiansufferterrahumanitarianorganization,muslim,n65) ).
cnf(u1138,axiom,
accept_leader(countrybhumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u781,axiom,
accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1303,axiom,
accept_population(countrybcivilorganization,muslim,n1) ).
cnf(u1179,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n20) ).
cnf(u779,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u929,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1168,axiom,
accept_city(christiansufferterrahumanitarianorganization,townc) ).
cnf(u1016,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n20) ).
cnf(u1076,axiom,
accept_population(countryacivilorganization,christian,n3) ).
cnf(u677,axiom,
( ~ the_agent_in_all_proposed_teams(X0,X1,X2)
| accept_leader(X0,X1) ) ).
cnf(u2600,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,citya)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna) ) ).
cnf(u909,axiom,
accept_team(countryafirstaidorganization,sufferterragovernment,towna,n5) ).
cnf(u794,axiom,
the_agent_not_in_any_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u675,axiom,
( accept_team(X0,X3,X1,X2)
| ~ accept_city(X0,X1)
| ~ accept_leader(X0,X3)
| ~ accept_number(X0,X2) ) ).
cnf(u907,axiom,
the_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1310,axiom,
accept_number(sufferterragovernment,n3) ).
cnf(u1693,axiom,
( ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75)
| accept_city(X0,citya)
| ~ accept_city(X0,coastvillage)
| ~ accept_city(X0,cityb) ) ).
cnf(u800,axiom,
accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n4) ).
cnf(u969,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2) ).
cnf(u715,axiom,
( accept_population(X0,atheist,n70)
| ~ accept_city(X0,northport) ) ).
cnf(u821,axiom,
any_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1343,axiom,
accept_number(countrybhumanitarianorganization,n1) ).
cnf(u922,axiom,
any_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u819,axiom,
accept_team(countryacivilorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u694,axiom,
( accept_population(X0,native,n1)
| ~ accept_city(X0,sunnysideport) ) ).
cnf(u700,axiom,
( accept_population(X0,native,n10)
| ~ accept_city(X0,centrallakecity) ) ).
cnf(u1710,axiom,
( ~ accept_population(X0,christian,n25)
| accept_city(X0,citya)
| ~ accept_city(X0,coastvillage)
| ~ accept_city(X0,towna) ) ).
cnf(u679,axiom,
( ~ the_agent_not_in_any_proposed_teams(X0,X1,X2)
| ~ accept_leader(X0,X1)
| ~ accept_city(X0,X2) ) ).
cnf(u947,axiom,
accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n5) ).
cnf(u1855,axiom,
( ~ accept_population(X0,native,n1)
| ~ accept_population(X0,christian,n8)
| ~ accept_population(X0,muslim,n60)
| ~ accept_population(X0,atheist,n30)
| accept_city(X0,sunnysideport)
| ~ accept_city(X0,cityb) ) ).
cnf(u1185,axiom,
accept_population(countryccivilorganization,christian,n0) ).
cnf(u682,axiom,
( accept_population(X0,native,n4)
| ~ accept_city(X0,suffertown) ) ).
cnf(u745,axiom,
( accept_population(X0,atheist,n70)
| ~ accept_city(X0,townb) ) ).
cnf(u834,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1074,axiom,
accept_population(countryacivilorganization,native,n85) ).
cnf(u1350,axiom,
accept_number(christiancountrychumanitarianorganization,n2) ).
cnf(u840,axiom,
accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u688,axiom,
( accept_population(X0,native,n1)
| ~ accept_city(X0,centraltown) ) ).
cnf(u1093,axiom,
accept_population(christiansufferterrahumanitarianorganization,muslim,n0) ).
cnf(u1354,axiom,
accept_population(christiancountrychumanitarianorganization,native,n0) ).
cnf(u3017,axiom,
( ~ accept_population(X0,native,n4)
| ~ accept_population(X0,atheist,n65)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,muslim,n7)
| ~ accept_city(X0,centrallakecity)
| accept_city(X0,suffertown) ) ).
cnf(u1202,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n5) ).
cnf(u1348,axiom,
accept_number(christiancountrychumanitarianorganization,n4) ).
cnf(u1097,axiom,
accept_leader(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u838,axiom,
any_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1221,axiom,
accept_number(countryamedicalorganization,n5) ).
cnf(u1352,axiom,
accept_number(christiancountrychumanitarianorganization,n6) ).
cnf(u719,axiom,
( accept_population(X0,muslim,n0)
| ~ accept_city(X0,coastvillage) ) ).
cnf(u1233,axiom,
accept_city(countryamedicalorganization,towna) ).
cnf(u844,axiom,
any_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1110,axiom,
accept_leader(countryafirstaidorganization,christiancountrychumanitarianorganization) ).
cnf(u1103,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n12) ).
cnf(u1225,axiom,
accept_number(countryamedicalorganization,n1) ).
cnf(u1133,axiom,
accept_population(countrybhumanitarianorganization,atheist,n30) ).
cnf(u966,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna) ).
cnf(u1365,axiom,
accept_number(countrycmedicalorganization,n6) ).
cnf(u863,axiom,
accept_team(countryacivilorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u722,axiom,
( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,atheist,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,native,n100)
| accept_city(X0,sunsetpoint) ) ).
cnf(u1388,axiom,
( ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75)
| ~ accept_city(X0,coastvillage)
| accept_city(X0,towna)
| ~ accept_city(X0,cityb) ) ).
cnf(u856,axiom,
accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,townc,n4) ).
cnf(u1108,axiom,
accept_population(countryafirstaidorganization,atheist,n12) ).
cnf(u1238,axiom,
accept_leader(countryacivilorganization,countrybhumanitarianorganization) ).
cnf(u728,axiom,
( ~ accept_population(X0,other,n0)
| ~ accept_population(X0,atheist,n75)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,native,n0)
| accept_city(X0,towna) ) ).
cnf(u1231,axiom,
accept_number(countryamedicalorganization,n6) ).
cnf(u2685,axiom,
( ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_city(X0,citya)
| accept_city(X0,towna) ) ).
cnf(u2649,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,centraltown) ).
cnf(u1123,axiom,
accept_leader(countrybhumanitarianorganization,countryacivilorganization) ).
cnf(u878,axiom,
any_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1261,axiom,
accept_population(sufferterragovernment,muslim,n1) ).
cnf(u707,axiom,
( accept_population(X0,muslim,n1)
| ~ accept_city(X0,stjosephburgh) ) ).
cnf(u1112,axiom,
accept_population(countryafirstaidorganization,muslim,n65) ).
cnf(u1242,axiom,
accept_population(countryahumanitarianorganization,atheist,n78) ).
cnf(u884,axiom,
accept_team(countrycmedicalorganization,countryccivilorganization,townc,n4) ).
cnf(u1150,axiom,
accept_population(sufferterragovernment,muslim,n0) ).
cnf(u1236,axiom,
accept_population(countryacivilorganization,atheist,n78) ).
cnf(u1143,axiom,
accept_population(countrybhumanitarianorganization,christian,n24) ).
cnf(u889,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc) ).
cnf(u2650,axiom,
~ accept_city(countrycmedicalorganization,centraltown) ).
cnf(u1251,axiom,
accept_population(countryahumanitarianorganization,native,n0) ).
cnf(u1006,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u775,axiom,
accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n4) ).
cnf(u2656,axiom,
~ accept_city(countryccivilorganization,citya) ).
cnf(u1148,axiom,
accept_population(sufferterragovernment,other,n0) ).
cnf(u1278,axiom,
accept_population(countryafirstaidorganization,other,n0) ).
cnf(u732,axiom,
( accept_population(X0,christian,n24)
| ~ accept_city(X0,towna) ) ).
cnf(u749,axiom,
( accept_population(X0,muslim,n1)
| ~ accept_city(X0,cityb) ) ).
cnf(u1271,axiom,
accept_city(countryccivilorganization,towna) ).
cnf(u1017,axiom,
accept_population(christiancountrychumanitarianorganization,atheist,n78) ).
cnf(u1035,axiom,
accept_leader(countryafirstaidorganization,countryamedicalorganization) ).
cnf(u747,axiom,
( accept_population(X0,other,n1)
| ~ accept_city(X0,cityb) ) ).
cnf(u1024,axiom,
accept_population(countryamedicalorganization,atheist,n30) ).
cnf(u903,axiom,
the_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb) ).
cnf(u1276,axiom,
accept_number(countryafirstaidorganization,n2) ).
cnf(u893,axiom,
accept_team(countrybhumanitarianorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1287,axiom,
accept_leader(countrycmedicalorganization,countrybcivilorganization) ).
cnf(u3081,axiom,
( ~ accept_population(X0,muslim,n8)
| ~ accept_city(X0,northport)
| accept_city(X0,townb)
| ~ accept_city(X0,cityb) ) ).
cnf(u1163,axiom,
accept_population(christiansufferterrahumanitarianorganization,other,n5) ).
cnf(u891,axiom,
accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n6) ).
cnf(u766,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4) ).
cnf(u1152,axiom,
accept_population(sufferterragovernment,atheist,n12) ).
cnf(u1000,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1060,axiom,
accept_leader(sufferterragovernment,countryamedicalorganization) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : AGT042+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.16 % Computer : n011.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Mon Sep 28 19:16:31 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 Running first-order theorem proving
% 0.10/0.19 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.99/1.21 % (3680015)Detected formulas, will run a generic FOF schedule.
% 3.99/1.21 % (3680024)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2245287738:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.99/1.21 % (3680024)Refutation not found, incomplete strategy
% 3.99/1.21 % (3680024)------------------------------
% 3.99/1.21 % (3680024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.99/1.21 % (3680024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.99/1.21 % (3680024)CaDiCaL version: 2.1.3
% 3.99/1.21 % (3680024)Termination reason: Refutation not found, incomplete strategy
% 3.99/1.21 % (3680024)Time elapsed: 0.001 s
% 3.99/1.21 % (3680024)Peak memory usage: 86 MB
% 3.99/1.21 % (3680024)Instructions burned: 1 (million)
% 3.99/1.21 % (3680025)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2676432594:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.99/1.21 % (3680022)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3304690807:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.99/1.21 % (3680020)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1354368616:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.99/1.21 % (3680023)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3286065370:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.99/1.21 % (3680026)dis-21_1_sil=8000:lcm=predicate:random_seed=816442332:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.99/1.21 % (3680021)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2116276085:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.99/1.21 % (3680023)Refutation not found, incomplete strategy
% 3.99/1.21 % (3680023)------------------------------
% 3.99/1.21 % (3680023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.99/1.21 % (3680023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.99/1.21 % (3680023)CaDiCaL version: 2.1.3
% 3.99/1.21 % (3680023)Termination reason: Refutation not found, incomplete strategy
% 3.99/1.21 % (3680023)Time elapsed: 0.001 s
% 3.99/1.21 % (3680023)Peak memory usage: 86 MB
% 3.99/1.21 % (3680023)Instructions burned: 1 (million)
% 3.99/1.21 % (3680026)Refutation not found, incomplete strategy
% 3.99/1.21 % (3680026)------------------------------
% 3.99/1.21 % (3680026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.99/1.21 % (3680026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.99/1.21 % (3680026)CaDiCaL version: 2.1.3
% 3.99/1.21 % (3680026)Termination reason: Refutation not found, incomplete strategy
% 3.99/1.21 % (3680026)Time elapsed: 0.002 s
% 3.99/1.21 % (3680026)Peak memory usage: 86 MB
% 3.99/1.21 % (3680026)Instructions burned: 2 (million)
% 3.99/1.21 % (3680025)Refutation not found, incomplete strategy
% 3.99/1.21 % (3680025)------------------------------
% 3.99/1.21 % (3680025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.99/1.21 % (3680025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.99/1.21 % (3680025)CaDiCaL version: 2.1.3
% 3.99/1.21 % (3680025)Termination reason: Refutation not found, incomplete strategy
% 3.99/1.21 % (3680025)Time elapsed: 0.012 s
% 3.99/1.21 % (3680025)Peak memory usage: 88 MB
% 3.99/1.21 % (3680025)Instructions burned: 24 (million)
% 3.99/1.21 % (3680024)------------------------------
% 3.99/1.21 % (3680024)------------------------------
% 3.99/1.21 % (3680026)------------------------------
% 3.99/1.21 % (3680026)------------------------------
% 3.99/1.21 % (3680023)------------------------------
% 3.99/1.21 % (3680023)------------------------------
% 3.99/1.21 % (3680034)lrs+10_1_sil=8000:sp=occurrence:random_seed=619547044:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 3.99/1.21 % (3680034)Refutation not found, incomplete strategy
% 3.99/1.21 % (3680034)------------------------------
% 3.99/1.21 % (3680034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.99/1.21 % (3680034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.84/1.62 % (3680034)CaDiCaL version: 2.1.3
% 6.84/1.62 % (3680034)Termination reason: Refutation not found, incomplete strategy
% 6.84/1.62 % (3680034)Time elapsed: 0.001 s
% 6.84/1.62 % (3680034)Peak memory usage: 86 MB
% 6.84/1.62 % (3680034)Instructions burned: 1 (million)
% 6.84/1.62 % (3680025)------------------------------
% 6.84/1.62 % (3680025)------------------------------
% 6.84/1.62 [W928 19:16:32.008724474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008718691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008763374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008767377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008801384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008811384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008813884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008824317 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008840617 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008850957 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008852917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008872877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.84/1.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.84/1.62 [W928 19:16:32.008882497 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008894217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008899434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008910311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008918668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008930151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008942911 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008954211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008962174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008965671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008988684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 [W928 19:16:32.008999451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.46/1.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.46/1.84 % (3680036)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1124130700:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 7.46/1.84 % (3680037)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3146277937:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 7.46/1.84 % (3680037)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680037)------------------------------
% 7.46/1.84 % (3680037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680037)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680037)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680037)Time elapsed: 0.001 s
% 7.46/1.84 % (3680037)Peak memory usage: 86 MB
% 7.46/1.84 % (3680037)Instructions burned: 1 (million)
% 7.46/1.84 % (3680036)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680036)------------------------------
% 7.46/1.84 % (3680036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680036)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680036)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680036)Time elapsed: 0.002 s
% 7.46/1.84 % (3680036)Peak memory usage: 87 MB
% 7.46/1.84 % (3680036)Instructions burned: 4 (million)
% 7.46/1.84 % (3680034)------------------------------
% 7.46/1.84 % (3680034)------------------------------
% 7.46/1.84 % (3680038)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=790937380:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 7.46/1.84 % (3680038)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680038)------------------------------
% 7.46/1.84 % (3680038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680038)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680038)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680038)Time elapsed: 0.073 s
% 7.46/1.84 % (3680038)Peak memory usage: 90 MB
% 7.46/1.84 % (3680038)Instructions burned: 155 (million)
% 7.46/1.84 % (3680041)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2269278787:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 7.46/1.84 % (3680041)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680041)------------------------------
% 7.46/1.84 % (3680041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680041)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680041)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680041)Time elapsed: 0.001 s
% 7.46/1.84 % (3680041)Peak memory usage: 86 MB
% 7.46/1.84 % (3680041)Instructions burned: 2 (million)
% 7.46/1.84 % (3680022)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680022)------------------------------
% 7.46/1.84 % (3680022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680022)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680022)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680022)Time elapsed: 0.560 s
% 7.46/1.84 % (3680022)Peak memory usage: 123 MB
% 7.46/1.84 % (3680022)Instructions burned: 825 (million)
% 7.46/1.84 % (3680021)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680021)------------------------------
% 7.46/1.84 % (3680021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680021)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680021)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680021)Time elapsed: 0.584 s
% 7.46/1.84 % (3680021)Peak memory usage: 123 MB
% 7.46/1.84 % (3680021)Instructions burned: 831 (million)
% 7.46/1.84 % (3680036)------------------------------
% 7.46/1.84 % (3680036)------------------------------
% 7.46/1.84 % (3680037)------------------------------
% 7.46/1.84 % (3680037)------------------------------
% 7.46/1.84 % (3680041)------------------------------
% 7.46/1.84 % (3680041)------------------------------
% 7.46/1.84 % (3680038)------------------------------
% 7.46/1.84 % (3680038)------------------------------
% 7.46/1.84 % (3680020)First to succeed.
% 7.46/1.84 % (3680020)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3680015"
% 7.46/1.84 % (3680046)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=283716299:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 7.46/1.84 % (3680044)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2212266763:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 7.46/1.84 % (3680045)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=881166890:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 7.46/1.84 % (3680045)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680045)------------------------------
% 7.46/1.84 % (3680045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680045)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680045)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680045)Time elapsed: 0.001 s
% 7.46/1.84 % (3680045)Peak memory usage: 87 MB
% 7.46/1.84 % (3680045)Instructions burned: 1 (million)
% 7.46/1.84 % (3680046)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680046)------------------------------
% 7.46/1.84 % (3680046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680046)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680046)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680046)Time elapsed: 0.010 s
% 7.46/1.84 % (3680046)Peak memory usage: 87 MB
% 7.46/1.84 % (3680046)Instructions burned: 41 (million)
% 7.46/1.84 % (3680022)------------------------------
% 7.46/1.84 % (3680022)------------------------------
% 7.46/1.84 % (3680021)------------------------------
% 7.46/1.84 % (3680021)------------------------------
% 7.46/1.84 % (3680047)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3835770266:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 7.46/1.84 % (3680047)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680047)------------------------------
% 7.46/1.84 % (3680047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680047)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680047)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680047)Time elapsed: 0.020 s
% 7.46/1.84 % (3680047)Peak memory usage: 89 MB
% 7.46/1.84 % (3680047)Instructions burned: 36 (million)
% 7.46/1.84 % (3680046)------------------------------
% 7.46/1.84 % (3680046)------------------------------
% 7.46/1.84 % (3680051)lrs+10_1_sil=8000:sp=occurrence:random_seed=1948990544:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 7.46/1.84 % (3680051)Refutation not found, incomplete strategy
% 7.46/1.84 % (3680051)------------------------------
% 7.46/1.84 % (3680051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.46/1.84 % (3680051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.84 % (3680051)CaDiCaL version: 2.1.3
% 7.46/1.84 % (3680051)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.84 % (3680051)Time elapsed: 0.002 s
% 7.46/1.84 % (3680051)Peak memory usage: 86 MB
% 7.46/1.84 % (3680051)Instructions burned: 2 (million)
% 7.46/1.84 % (3680052)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1708090356:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 7.46/1.84 % SZS status Satisfiable for theBenchmark
% 7.46/1.84 % SZS output start Saturation.
% See solution above
% 0.16/2.03 % SZS output start Definitions and Model Updates.
% 0.16/2.03 for all inputs,
% 0.16/2.03 define less(X0,X1) := $false
% 0.16/2.03 for all inputs,
% 0.16/2.03 define min_number_of_proposed_agents(X0,X1) := $false
% 0.16/2.03 % SZS output end Definitions and Model Updates.
% 0.16/2.03 % (3680020)------------------------------
% 0.16/2.03 % (3680020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.03 % (3680020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.03 % (3680020)CaDiCaL version: 2.1.3
% 0.16/2.03 % (3680020)Termination reason: Satisfiable
% 0.16/2.03 % (3680020)Time elapsed: 0.759 s
% 0.16/2.03 % (3680020)Peak memory usage: 132 MB
% 0.16/2.03 % (3680020)Instructions burned: 1142 (million)
% 0.16/2.03 % (3680020)------------------------------
% 0.16/2.03 % (3680020)------------------------------
% 0.16/2.03 % (3680015)Success in time 1.211 s
% 0.16/2.03 % Vampire exiting
%------------------------------------------------------------------------------