%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : AGT042+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:53 AM UTC 2026
% Result : Satisfiable 0.21s 0.30s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2022,axiom,
~ accept_population(countryamedicalorganization,atheist,n12) ).
cnf(u2044,axiom,
~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ).
cnf(u1326,axiom,
accept_population(christiancountrychumanitarianorganization,native,n0) ).
cnf(u1179,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1455,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,towna,n6) ).
cnf(u1439,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1386,axiom,
( accept_population(X0,native,n15)
| accept_city(X0,northport) ) ).
cnf(u1182,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1) ).
cnf(u1416,axiom,
( accept_population(X0,native,n0)
| accept_city(X0,townb) ) ).
cnf(u1636,axiom,
~ accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1181,axiom,
accept_population(muslimcountrybhumanitarianorganization,native,n0) ).
cnf(u1576,axiom,
~ accept_team(countryacivilorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1345,axiom,
accept_leader(muslimcountrybhumanitarianorganization,sufferterragovernment) ).
cnf(u1095,axiom,
accept_leader(countrybhumanitarianorganization,countryacivilorganization) ).
cnf(u1238,axiom,
accept_population(countryccivilorganization,other,n0) ).
cnf(u1184,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n78) ).
cnf(u1009,axiom,
accept_leader(countrycmedicalorganization,countryacivilorganization) ).
cnf(u1620,axiom,
~ accept_number(countryccivilorganization,n2) ).
cnf(u1291,axiom,
accept_population(countryacivilorganization,other,n0) ).
cnf(u1483,axiom,
~ accept_number(countryacivilorganization,n2) ).
cnf(u1600,axiom,
~ accept_number(christiancountrychumanitarianorganization,n2) ).
cnf(u1211,axiom,
accept_leader(countryahumanitarianorganization,countryacivilorganization) ).
cnf(u1598,axiom,
~ accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n5) ).
cnf(u1131,axiom,
accept_leader(sufferterragovernment,countryahumanitarianorganization) ).
cnf(u1556,axiom,
accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1519,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,townc,n6) ).
cnf(u1134,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countrybcivilorganization) ).
cnf(u1485,axiom,
~ accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u809,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1164,axiom,
accept_population(countrycmedicalorganization,christian,n0) ).
cnf(u1426,axiom,
( accept_population(X0,christian,n0)
| accept_city(X0,townc) ) ).
cnf(u1133,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countryccivilorganization) ).
cnf(u1766,axiom,
~ accept_number(muslimcountrybhumanitarianorganization,n1) ).
cnf(u1155,axiom,
accept_population(countryccivilorganization,other,n5) ).
cnf(u1708,axiom,
~ accept_city(countryahumanitarianorganization,towna) ).
cnf(u1136,axiom,
accept_population(christiansufferterrahumanitarianorganization,muslim,n65) ).
cnf(u996,axiom,
accept_population(countryamedicalorganization,atheist,n30) ).
cnf(u833,axiom,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1233,axiom,
accept_population(sufferterragovernment,muslim,n1) ).
cnf(u1318,axiom,
accept_leader(christiancountrychumanitarianorganization,countrycmedicalorganization) ).
cnf(u1157,axiom,
accept_population(countryccivilorganization,christian,n0) ).
cnf(u1552,axiom,
~ any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1348,axiom,
( accept_team(X0,X3,X1,X2)
| accept_leader(X0,X3) ) ).
cnf(u1083,axiom,
accept_population(countryafirstaidorganization,other,n5) ).
cnf(u751,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1559,axiom,
~ any_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb) ).
cnf(u1160,axiom,
accept_leader(countryccivilorganization,countryahumanitarianorganization) ).
cnf(u1062,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryafirstaidorganization) ).
cnf(u1086,axiom,
accept_population(countryafirstaidorganization,atheist,n30) ).
cnf(u1762,axiom,
~ accept_number(muslimcountrybhumanitarianorganization,n5) ).
cnf(u1167,axiom,
accept_leader(countrycmedicalorganization,countryahumanitarianorganization) ).
cnf(u1085,axiom,
accept_population(countryafirstaidorganization,christian,n0) ).
cnf(u1718,axiom,
~ accept_city(countrycmedicalorganization,towna) ).
cnf(u1107,axiom,
accept_leader(countrybhumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1717,axiom,
~ accept_city(countryafirstaidorganization,towna) ).
cnf(u1542,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u1110,axiom,
accept_leader(countrybhumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u785,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1268,axiom,
accept_leader(countrycmedicalorganization,sufferterragovernment) ).
cnf(u1407,axiom,
( accept_population(X0,atheist,n75)
| accept_city(X0,citya) ) ).
cnf(u1109,axiom,
accept_leader(countrybhumanitarianorganization,countrybcivilorganization) ).
cnf(u1561,axiom,
~ accept_number(countryafirstaidorganization,n6) ).
cnf(u1259,axiom,
accept_leader(countrycmedicalorganization,countrybcivilorganization) ).
cnf(u1082,axiom,
accept_leader(countryafirstaidorganization,christiancountrychumanitarianorganization) ).
cnf(u1433,axiom,
~ accept_team(countryahumanitarianorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1741,axiom,
~ accept_number(countrybcivilorganization,n1) ).
cnf(u1112,axiom,
accept_population(countrybhumanitarianorganization,other,n0) ).
cnf(u1011,axiom,
accept_population(countrycmedicalorganization,muslim,n0) ).
cnf(u1389,axiom,
( accept_population(X0,atheist,n12)
| accept_city(X0,coastvillage) ) ).
cnf(u1119,axiom,
accept_leader(sufferterragovernment,countryafirstaidorganization) ).
cnf(u1411,axiom,
( accept_population(X0,other,n0)
| accept_city(X0,citya) ) ).
cnf(u1713,axiom,
~ accept_number(countryafirstaidorganization,n3) ).
cnf(u1520,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1059,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n75) ).
cnf(u1612,axiom,
~ accept_team(countrybcivilorganization,countryccivilorganization,towna,n4) ).
cnf(u1541,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u1623,axiom,
accept_team(countryccivilorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1105,axiom,
accept_population(countrybhumanitarianorganization,atheist,n30) ).
cnf(u1738,axiom,
~ accept_number(countrybcivilorganization,n4) ).
cnf(u1092,axiom,
accept_population(countryafirstaidorganization,atheist,n78) ).
cnf(u1007,axiom,
accept_leader(countryafirstaidorganization,countryamedicalorganization) ).
cnf(u1352,axiom,
( the_agent_not_in_any_proposed_teams(X0,X1,X2)
| ~ accept_leader(X0,X1)
| accept_city(X0,X2) ) ).
cnf(u1419,axiom,
( accept_population(X0,atheist,n78)
| accept_city(X0,cityb) ) ).
cnf(u972,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1693,axiom,
~ accept_number(countryamedicalorganization,n5) ).
cnf(u1064,axiom,
accept_population(christiansufferterrahumanitarianorganization,native,n85) ).
cnf(u1538,axiom,
~ accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n2) ).
cnf(u1661,axiom,
~ accept_city(countrybcivilorganization,cityb) ).
cnf(u1071,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n0) ).
cnf(u1328,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n24) ).
cnf(u1537,axiom,
~ any_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1058,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n24) ).
cnf(u1360,axiom,
( accept_population(X0,christian,n23)
| accept_city(X0,centraltown) ) ).
cnf(u987,axiom,
accept_population(christiancountrychumanitarianorganization,other,n1) ).
cnf(u1690,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,townc) ).
cnf(u1478,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n4) ).
cnf(u1601,axiom,
~ accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n3) ).
cnf(u1588,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n3) ).
cnf(u1689,axiom,
~ accept_city(countrycmedicalorganization,cityb) ).
cnf(u1521,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1297,axiom,
accept_leader(countryacivilorganization,sufferterragovernment) ).
cnf(u1645,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1853,axiom,
accept_team(countryamedicalorganization,X0,coastvillage,X1) ).
cnf(u1534,axiom,
accept_team(countryccivilorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1630,axiom,
~ accept_team(countryacivilorganization,sufferterragovernment,towna,n6) ).
cnf(u983,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n0) ).
cnf(u1148,axiom,
accept_population(christiansufferterrahumanitarianorganization,other,n1) ).
cnf(u1471,axiom,
~ accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1317,axiom,
accept_leader(christiancountrychumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u1699,axiom,
~ accept_city(countryamedicalorganization,towna) ).
cnf(u866,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1641,axiom,
~ accept_number(countrybcivilorganization,n6) ).
cnf(u1732,axiom,
~ accept_city(countryacivilorganization,towna) ).
cnf(u1597,axiom,
~ accept_team(countryamedicalorganization,sufferterragovernment,towna,n6) ).
cnf(u1514,axiom,
~ any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1583,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n2) ).
cnf(u1892,axiom,
accept_leader(countryccivilorganization,countrycmedicalorganization) ).
cnf(u1346,axiom,
( ~ accept_team(X0,X3,X1,X2)
| ~ accept_leader(X0,X3)
| accept_city(X0,X1)
| accept_number(X0,X2) ) ).
cnf(u1018,axiom,
accept_population(countrybcivilorganization,christian,n3) ).
cnf(u1501,axiom,
~ accept_team(countrybcivilorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1704,axiom,
~ accept_number(countryahumanitarianorganization,n3) ).
cnf(u1500,axiom,
~ accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1660,axiom,
~ accept_city(countrybcivilorganization,townc) ).
cnf(u1594,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1651,axiom,
~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1241,axiom,
accept_population(countryccivilorganization,christian,n24) ).
cnf(u1728,axiom,
~ accept_number(countryacivilorganization,n3) ).
cnf(u2053,axiom,
accept_team(muslimcountrybhumanitarianorganization,X0,citya,X1) ).
cnf(u1454,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,towna,n6) ).
cnf(u981,axiom,
accept_population(christiancountrychumanitarianorganization,other,n5) ).
cnf(u1735,axiom,
~ accept_number(countryccivilorganization,n1) ).
cnf(u1457,axiom,
accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n2) ).
cnf(u1466,axiom,
~ any_agent_in_all_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1262,axiom,
accept_population(countrycmedicalorganization,other,n0) ).
cnf(u649,axiom,
( ~ the_agent_in_all_proposed_teams(X0,X1,X2)
| accept_leader(X0,X1) ) ).
cnf(u1675,axiom,
~ accept_city(countrybhumanitarianorganization,townc) ).
cnf(u842,axiom,
the_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1137,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n0) ).
cnf(u1656,axiom,
~ accept_city(countryamedicalorganization,townc) ).
cnf(u1452,axiom,
~ accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1548,axiom,
~ any_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc) ).
cnf(u1663,axiom,
accept_number(countryccivilorganization,n5) ).
cnf(u1264,axiom,
accept_population(countrycmedicalorganization,muslim,n1) ).
cnf(u1441,axiom,
~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u961,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna) ).
cnf(u1446,axiom,
~ accept_number(countrybhumanitarianorganization,n4) ).
cnf(u1680,axiom,
~ accept_number(christiansufferterrahumanitarianorganization,n5) ).
cnf(u1325,axiom,
accept_population(christiancountrychumanitarianorganization,other,n0) ).
cnf(u1432,axiom,
~ accept_team(countryahumanitarianorganization,countryacivilorganization,towna,n6) ).
cnf(u1258,axiom,
accept_leader(countrycmedicalorganization,countryccivilorganization) ).
cnf(u1687,axiom,
~ accept_city(countryccivilorganization,townc) ).
cnf(u1214,axiom,
accept_population(countryahumanitarianorganization,atheist,n78) ).
cnf(u1357,axiom,
( accept_population(X0,other,n4)
| accept_city(X0,suffertown) ) ).
cnf(u1627,axiom,
~ accept_number(sufferterragovernment,n5) ).
cnf(u1244,axiom,
accept_leader(countryccivilorganization,sufferterragovernment) ).
cnf(u1213,axiom,
accept_population(countryahumanitarianorganization,christian,n20) ).
cnf(u1404,axiom,
( accept_population(X0,native,n0)
| accept_city(X0,towna) ) ).
cnf(u1235,axiom,
accept_population(sufferterragovernment,atheist,n78) ).
cnf(u1409,axiom,
( accept_population(X0,muslim,n0)
| accept_city(X0,citya) ) ).
cnf(u1265,axiom,
accept_population(countrycmedicalorganization,christian,n24) ).
cnf(u1442,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1231,axiom,
accept_population(sufferterragovernment,other,n1) ).
cnf(u1608,axiom,
~ accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1472,axiom,
~ accept_number(countrybcivilorganization,n5) ).
cnf(u1044,axiom,
accept_leader(countryacivilorganization,countryamedicalorganization) ).
cnf(u1237,axiom,
accept_leader(sufferterragovernment,countrybhumanitarianorganization) ).
cnf(u1632,axiom,
~ accept_number(countrycmedicalorganization,n3) ).
cnf(u1428,axiom,
( accept_population(X0,native,n0)
| accept_city(X0,townc) ) ).
cnf(u1210,axiom,
accept_leader(countryacivilorganization,countrybhumanitarianorganization) ).
cnf(u1639,axiom,
~ accept_number(countryccivilorganization,n4) ).
cnf(u1240,axiom,
accept_population(countryccivilorganization,muslim,n1) ).
cnf(u1453,axiom,
~ accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1038,axiom,
accept_population(countryccivilorganization,christian,n20) ).
cnf(u1517,axiom,
~ accept_number(muslimcountrybhumanitarianorganization,n3) ).
cnf(u1579,axiom,
~ accept_number(countrybhumanitarianorganization,n5) ).
cnf(u1422,axiom,
( accept_population(X0,native,n0)
| accept_city(X0,cityb) ) ).
cnf(u1353,axiom,
( accept_population(X0,atheist,n65)
| accept_city(X0,suffertown) ) ).
cnf(u1037,axiom,
accept_population(countryccivilorganization,other,n1) ).
cnf(u1670,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,coastvillage) ).
cnf(u1187,axiom,
accept_leader(countryamedicalorganization,countryacivilorganization) ).
cnf(u1580,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1669,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,coastvillage) ).
cnf(u1394,axiom,
( ~ accept_city(X0,coastvillage)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n85)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n3)
| ~ accept_population(X0,atheist,n12) ) ).
cnf(u1190,axiom,
accept_population(countryamedicalorganization,atheist,n78) ).
cnf(u1163,axiom,
accept_population(countrycmedicalorganization,muslim,n65) ).
cnf(u1688,axiom,
~ accept_city(countrycmedicalorganization,townc) ).
cnf(u1047,axiom,
accept_population(countryacivilorganization,muslim,n0) ).
cnf(u1189,axiom,
accept_population(countryamedicalorganization,christian,n20) ).
cnf(u1584,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n2) ).
cnf(u1380,axiom,
( accept_population(X0,native,n11)
| accept_city(X0,stjosephburgh) ) ).
cnf(u1008,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryamedicalorganization) ).
cnf(u1034,axiom,
accept_population(sufferterragovernment,atheist,n75) ).
cnf(u1513,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u1591,axiom,
~ accept_number(muslimcountrybhumanitarianorganization,n2) ).
cnf(u1192,axiom,
accept_leader(countryamedicalorganization,countrybhumanitarianorganization) ).
cnf(u1033,axiom,
accept_population(sufferterragovernment,christian,n24) ).
cnf(u1004,axiom,
accept_population(countryahumanitarianorganization,atheist,n12) ).
cnf(u1349,axiom,
( ~ accept_number(X0,X2)
| accept_team(X0,X3,X1,X2) ) ).
cnf(u1199,axiom,
accept_population(countryamedicalorganization,native,n0) ).
cnf(u1491,axiom,
~ accept_team(countryafirstaidorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1382,axiom,
( ~ accept_city(X0,stjosephburgh)
| ~ accept_population(X0,other,n4)
| ~ accept_population(X0,native,n11)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n16)
| ~ accept_population(X0,atheist,n68) ) ).
cnf(u1665,axiom,
~ accept_city(countryccivilorganization,cityb) ).
cnf(u1638,axiom,
~ accept_number(christiancountrychumanitarianorganization,n3) ).
cnf(u1139,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1621,axiom,
~ accept_number(countryccivilorganization,n3) ).
cnf(u1185,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u1493,axiom,
accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1384,axiom,
( accept_population(X0,christian,n13)
| accept_city(X0,northport) ) ).
cnf(u1172,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countrycmedicalorganization) ).
cnf(u1141,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countryacivilorganization) ).
cnf(u1593,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n6) ).
cnf(u984,axiom,
accept_population(christiancountrychumanitarianorganization,atheist,n30) ).
cnf(u1465,axiom,
~ the_agent_not_in_any_proposed_teams(countryamedicalorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1293,axiom,
accept_population(countryacivilorganization,muslim,n1) ).
cnf(u1151,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n20) ).
cnf(u1443,axiom,
~ accept_team(countryamedicalorganization,countryacivilorganization,cityb,n6) ).
cnf(u1617,axiom,
~ accept_number(sufferterragovernment,n2) ).
cnf(u1138,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n30) ).
cnf(u1550,axiom,
~ accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1510,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1633,axiom,
~ accept_team(countrycmedicalorganization,countryccivilorganization,towna,n4) ).
cnf(u1303,axiom,
accept_leader(christiancountrychumanitarianorganization,countryccivilorganization) ).
cnf(u1445,axiom,
~ accept_team(countryafirstaidorganization,countryacivilorganization,cityb,n6) ).
cnf(u994,axiom,
accept_population(countryamedicalorganization,muslim,n65) ).
cnf(u1726,axiom,
~ accept_number(countryacivilorganization,n5) ).
cnf(u1072,axiom,
accept_population(muslimcountrybhumanitarianorganization,native,n85) ).
cnf(u1124,axiom,
accept_population(sufferterragovernment,atheist,n12) ).
cnf(u1415,axiom,
( accept_population(X0,muslim,n8)
| accept_city(X0,townb) ) ).
cnf(u1274,axiom,
accept_population(countrybcivilorganization,native,n0) ).
cnf(u1570,axiom,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1395,axiom,
( accept_population(X0,atheist,n0)
| accept_city(X0,sunsetpoint) ) ).
cnf(u1569,axiom,
~ any_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1115,axiom,
accept_population(countrybhumanitarianorganization,christian,n24) ).
cnf(u1413,axiom,
( accept_population(X0,atheist,n70)
| accept_city(X0,townb) ) ).
cnf(u1118,axiom,
accept_leader(countrybhumanitarianorganization,sufferterragovernment) ).
cnf(u1019,axiom,
accept_population(countrybcivilorganization,atheist,n12) ).
cnf(u1722,axiom,
~ accept_number(sufferterragovernment,n3) ).
cnf(u1358,axiom,
( ~ accept_city(X0,suffertown)
| ~ accept_population(X0,other,n4)
| ~ accept_population(X0,native,n4)
| ~ accept_population(X0,muslim,n7)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n65) ) ).
cnf(u1531,axiom,
~ any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1721,axiom,
~ accept_number(sufferterragovernment,n4) ).
cnf(u1566,axiom,
~ accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1549,axiom,
~ accept_team(countrybhumanitarianorganization,countrybcivilorganization,townc,n6) ).
cnf(u1366,axiom,
( accept_population(X0,christian,n8)
| accept_city(X0,sunnysideport) ) ).
cnf(u1533,axiom,
accept_team(countryccivilorganization,countrybcivilorganization,townc,n6) ).
cnf(u1644,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1590,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,towna,n2) ).
cnf(u1406,axiom,
( ~ accept_city(X0,towna)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n24)
| ~ accept_population(X0,atheist,n75) ) ).
cnf(u1512,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1070,axiom,
accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ).
cnf(u1135,axiom,
accept_population(christiansufferterrahumanitarianorganization,other,n5) ).
cnf(u1387,axiom,
( accept_population(X0,other,n2)
| accept_city(X0,northport) ) ).
cnf(u1546,axiom,
~ accept_team(countrycmedicalorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1603,axiom,
~ accept_team(countrybhumanitarianorganization,countrycmedicalorganization,towna,n3) ).
cnf(u770,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna) ).
cnf(u815,axiom,
the_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1625,axiom,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1486,axiom,
~ accept_team(countryacivilorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u1609,axiom,
~ any_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1418,axiom,
( ~ accept_city(X0,townb)
| ~ accept_population(X0,other,n2)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n8)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n70) ) ).
cnf(u1755,axiom,
~ accept_city(christiancountrychumanitarianorganization,towna) ).
cnf(u1263,axiom,
accept_population(countrycmedicalorganization,native,n0) ).
cnf(u1381,axiom,
( accept_population(X0,other,n4)
| accept_city(X0,stjosephburgh) ) ).
cnf(u1532,axiom,
accept_team(countryccivilorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u1017,axiom,
accept_population(countrybcivilorganization,muslim,n0) ).
cnf(u734,axiom,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1448,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryacivilorganization,cityb,n6) ).
cnf(u1619,axiom,
accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n6) ).
cnf(u1564,axiom,
~ accept_team(countryafirstaidorganization,sufferterragovernment,towna,n6) ).
cnf(u1216,axiom,
accept_leader(countryahumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u1467,axiom,
~ accept_team(countryccivilorganization,countrycmedicalorganization,towna,n4) ).
cnf(u1400,axiom,
( ~ accept_city(X0,sunsetpoint)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n100)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n0) ) ).
cnf(u1555,axiom,
~ any_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1223,axiom,
accept_population(countryahumanitarianorganization,native,n0) ).
cnf(u1760,axiom,
~ accept_number(countrycmedicalorganization,n1) ).
cnf(u1094,axiom,
accept_leader(countryafirstaidorganization,countrybhumanitarianorganization) ).
cnf(u1013,axiom,
accept_population(countrycmedicalorganization,atheist,n12) ).
cnf(u1370,axiom,
( ~ accept_city(X0,sunnysideport)
| ~ accept_population(X0,other,n1)
| ~ accept_population(X0,native,n1)
| ~ accept_population(X0,muslim,n60)
| ~ accept_population(X0,christian,n8)
| ~ accept_population(X0,atheist,n30) ) ).
cnf(u1503,axiom,
~ accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1528,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,townc,n6) ).
cnf(u1067,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n12) ).
cnf(u1165,axiom,
accept_population(countrycmedicalorganization,atheist,n30) ).
cnf(u1560,axiom,
~ accept_team(countryafirstaidorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1356,axiom,
( accept_population(X0,native,n4)
| accept_city(X0,suffertown) ) ).
cnf(u1310,axiom,
accept_leader(christiancountrychumanitarianorganization,countrybcivilorganization) ).
cnf(u1567,axiom,
~ accept_team(countryamedicalorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1168,axiom,
accept_population(countrycmedicalorganization,other,n1) ).
cnf(u993,axiom,
accept_population(countryamedicalorganization,other,n5) ).
cnf(u1234,axiom,
accept_population(sufferterragovernment,christian,n20) ).
cnf(u1175,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n65) ).
cnf(u1712,axiom,
~ accept_number(countryafirstaidorganization,n4) ).
cnf(u1090,axiom,
accept_population(countryafirstaidorganization,other,n1) ).
cnf(u1162,axiom,
accept_population(countrycmedicalorganization,other,n5) ).
cnf(u1719,axiom,
~ accept_city(countrybcivilorganization,towna) ).
cnf(u1161,axiom,
accept_leader(countrycmedicalorganization,muslimcountrybhumanitarianorganization) ).
cnf(u1659,axiom,
~ accept_city(countrybcivilorganization,coastvillage) ).
cnf(u1276,axiom,
accept_population(countrybcivilorganization,christian,n24) ).
cnf(u1604,axiom,
~ accept_team(countrybhumanitarianorganization,countryccivilorganization,towna,n3) ).
cnf(u1750,axiom,
~ accept_number(christiancountrychumanitarianorganization,n4) ).
cnf(u861,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryahumanitarianorganization,townc) ).
cnf(u989,axiom,
accept_population(christiancountrychumanitarianorganization,atheist,n78) ).
cnf(u1425,axiom,
( accept_population(X0,atheist,n30)
| accept_city(X0,townc) ) ).
cnf(u1692,axiom,
~ accept_city(countryamedicalorganization,cityb) ).
cnf(u1120,axiom,
accept_population(sufferterragovernment,other,n0) ).
cnf(u1270,axiom,
accept_leader(countrybcivilorganization,countrybhumanitarianorganization) ).
cnf(u1504,axiom,
~ accept_team(sufferterragovernment,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u1438,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n4) ).
cnf(u1127,axiom,
accept_population(sufferterragovernment,other,n5) ).
cnf(u1269,axiom,
accept_leader(countrybcivilorganization,countryccivilorganization) ).
cnf(u1536,axiom,
accept_team(countryccivilorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1460,axiom,
accept_team(countryamedicalorganization,christiansufferterrahumanitarianorganization,coastvillage,n2) ).
cnf(u1114,axiom,
accept_population(countrybhumanitarianorganization,muslim,n1) ).
cnf(u1543,axiom,
~ accept_team(countrycmedicalorganization,countryccivilorganization,townc,n4) ).
cnf(u1272,axiom,
accept_leader(countrybcivilorganization,countrycmedicalorganization) ).
cnf(u1052,axiom,
accept_population(countryacivilorganization,other,n5) ).
cnf(u1113,axiom,
accept_population(countrybhumanitarianorganization,native,n0) ).
cnf(u1421,axiom,
( accept_population(X0,muslim,n1)
| accept_city(X0,cityb) ) ).
cnf(u980,axiom,
accept_leader(christiancountrychumanitarianorganization,muslimcountrybhumanitarianorganization) ).
cnf(u1279,axiom,
accept_leader(countrybcivilorganization,sufferterragovernment) ).
cnf(u1069,axiom,
accept_leader(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u1745,axiom,
~ accept_number(countrybhumanitarianorganization,n3) ).
cnf(u1091,axiom,
accept_population(countryafirstaidorganization,christian,n20) ).
cnf(u1393,axiom,
( accept_population(X0,other,n0)
| accept_city(X0,coastvillage) ) ).
cnf(u1701,axiom,
~ accept_city(countryahumanitarianorganization,cityb) ).
cnf(u1015,axiom,
accept_leader(countrybcivilorganization,countryacivilorganization) ).
cnf(u1043,axiom,
accept_leader(countryccivilorganization,countryacivilorganization) ).
cnf(u1046,axiom,
accept_population(countryacivilorganization,native,n85) ).
cnf(u1252,axiom,
accept_population(countryafirstaidorganization,muslim,n1) ).
cnf(u1079,axiom,
accept_population(countryafirstaidorganization,christian,n3) ).
cnf(u1371,axiom,
( accept_population(X0,atheist,n70)
| accept_city(X0,centrallakecity) ) ).
cnf(u1066,axiom,
accept_population(christiansufferterrahumanitarianorganization,christian,n3) ).
cnf(u1417,axiom,
( accept_population(X0,other,n2)
| accept_city(X0,townb) ) ).
cnf(u1096,axiom,
accept_population(countrybhumanitarianorganization,native,n85) ).
cnf(u995,axiom,
accept_population(countryamedicalorganization,christian,n0) ).
cnf(u1065,axiom,
accept_population(christiansufferterrahumanitarianorganization,muslim,n0) ).
cnf(u1373,axiom,
( accept_population(X0,muslim,n1)
| accept_city(X0,centrallakecity) ) ).
cnf(u1103,axiom,
accept_population(countrybhumanitarianorganization,muslim,n65) ).
cnf(u1523,axiom,
~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc) ).
cnf(u1697,axiom,
~ accept_number(countryamedicalorganization,n1) ).
cnf(u893,axiom,
the_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1599,axiom,
~ accept_team(countryahumanitarianorganization,sufferterragovernment,towna,n6) ).
cnf(u1653,axiom,
~ accept_city(christiancountrychumanitarianorganization,townc) ).
cnf(u1089,axiom,
accept_leader(countryafirstaidorganization,countryacivilorganization) ).
cnf(u1489,axiom,
~ accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1204,axiom,
accept_leader(countryamedicalorganization,sufferterragovernment) ).
cnf(u1045,axiom,
accept_leader(countryacivilorganization,countryafirstaidorganization) ).
cnf(u1678,axiom,
~ accept_city(sufferterragovernment,townc) ).
cnf(u1016,axiom,
accept_population(countrybcivilorganization,native,n85) ).
cnf(u1427,axiom,
( accept_population(X0,muslim,n65)
| accept_city(X0,townc) ) ).
cnf(u1369,axiom,
( accept_population(X0,other,n1)
| accept_city(X0,sunnysideport) ) ).
cnf(u1677,axiom,
~ accept_city(sufferterragovernment,coastvillage) ).
cnf(u1048,axiom,
accept_population(countryacivilorganization,christian,n3) ).
cnf(u1525,axiom,
~ accept_team(countryafirstaidorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u1650,axiom,
~ accept_number(muslimcountrybhumanitarianorganization,n6) ).
cnf(u1055,axiom,
accept_population(countryacivilorganization,atheist,n30) ).
cnf(u1347,axiom,
( ~ accept_city(X0,X1)
| accept_team(X0,X3,X1,X2) ) ).
cnf(u1649,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1968,axiom,
accept_team(countryccivilorganization,X0,X1,n6) ).
cnf(u1390,axiom,
( accept_population(X0,christian,n3)
| accept_city(X0,coastvillage) ) ).
cnf(u1967,axiom,
accept_team(countryccivilorganization,X0,X1,n5) ).
cnf(u1646,axiom,
~ accept_number(christiancountrychumanitarianorganization,n6) ).
cnf(u1547,axiom,
~ accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1674,axiom,
~ accept_city(countrybhumanitarianorganization,coastvillage) ).
cnf(u1295,axiom,
accept_population(countryacivilorganization,atheist,n75) ).
cnf(u898,axiom,
the_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1673,axiom,
~ accept_city(countryafirstaidorganization,cityb) ).
cnf(u1170,axiom,
accept_population(countrycmedicalorganization,atheist,n78) ).
cnf(u1629,axiom,
~ accept_number(sufferterragovernment,n6) ).
cnf(u1367,axiom,
( accept_population(X0,muslim,n60)
| accept_city(X0,sunnysideport) ) ).
cnf(u1524,axiom,
~ accept_team(countryacivilorganization,countryahumanitarianorganization,townc,n6) ).
cnf(u1684,axiom,
~ accept_number(christiansufferterrahumanitarianorganization,n1) ).
cnf(u1355,axiom,
( accept_population(X0,muslim,n7)
| accept_city(X0,suffertown) ) ).
cnf(u1505,axiom,
~ accept_team(sufferterragovernment,countryacivilorganization,coastvillage,n6) ).
cnf(u1022,axiom,
accept_population(countrybcivilorganization,other,n5) ).
cnf(u1642,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybcivilorganization,towna,n6) ).
cnf(u1502,axiom,
~ any_agent_in_all_proposed_teams(countrybcivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1626,axiom,
~ any_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna) ).
cnf(u1518,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,townc,n4) ).
cnf(u1277,axiom,
accept_population(countrybcivilorganization,atheist,n75) ).
cnf(u1582,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n2) ).
cnf(u1581,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1498,axiom,
~ accept_team(countrybcivilorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u1440,axiom,
~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1002,axiom,
accept_population(countryahumanitarianorganization,muslim,n0) ).
cnf(u887,axiom,
the_agent_in_all_proposed_teams(countryamedicalorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1484,axiom,
~ accept_team(countryacivilorganization,countryahumanitarianorganization,coastvillage,n5) ).
cnf(u1695,axiom,
~ accept_number(countryamedicalorganization,n3) ).
cnf(u875,axiom,
the_agent_in_all_proposed_teams(sufferterragovernment,countrybhumanitarianorganization,cityb) ).
cnf(u870,axiom,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1578,axiom,
~ any_agent_in_all_proposed_teams(countryacivilorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1126,axiom,
accept_leader(sufferterragovernment,christiancountrychumanitarianorganization) ).
cnf(u1273,axiom,
accept_population(countrybcivilorganization,other,n0) ).
cnf(u1232,axiom,
accept_population(sufferterragovernment,native,n0) ).
cnf(u1495,axiom,
~ accept_number(christiancountrychumanitarianorganization,n5) ).
cnf(u1668,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,towna) ).
cnf(u1652,axiom,
~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1450,axiom,
~ accept_number(countrybhumanitarianorganization,n1) ).
cnf(u1480,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1361,axiom,
( accept_population(X0,muslim,n3)
| accept_city(X0,centraltown) ) ).
cnf(u1640,axiom,
~ accept_team(christiancountrychumanitarianorganization,countryccivilorganization,towna,n4) ).
cnf(u1078,axiom,
accept_population(countryafirstaidorganization,muslim,n0) ).
cnf(u1075,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n12) ).
cnf(u798,axiom,
the_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1474,axiom,
~ accept_team(sufferterragovernment,countryacivilorganization,towna,n6) ).
cnf(u1535,axiom,
accept_team(countryccivilorganization,christiancountrychumanitarianorganization,townc,n6) ).
cnf(u1226,axiom,
accept_population(countryahumanitarianorganization,atheist,n75) ).
cnf(u1587,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3) ).
cnf(u1430,axiom,
( ~ accept_city(X0,townc)
| ~ accept_population(X0,other,n5)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n65)
| ~ accept_population(X0,christian,n0)
| ~ accept_population(X0,atheist,n30) ) ).
cnf(u1664,axiom,
accept_number(countryccivilorganization,n6) ).
cnf(u1481,axiom,
~ any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1242,axiom,
accept_population(countryccivilorganization,atheist,n75) ).
cnf(u1671,axiom,
~ accept_city(countryafirstaidorganization,coastvillage) ).
cnf(u1402,axiom,
( accept_population(X0,christian,n24)
| accept_city(X0,towna) ) ).
cnf(u1198,axiom,
accept_population(countryamedicalorganization,other,n0) ).
cnf(u1611,axiom,
~ accept_number(countrybcivilorganization,n3) ).
cnf(u1228,axiom,
accept_leader(countryahumanitarianorganization,sufferterragovernment) ).
cnf(u778,axiom,
the_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna) ).
cnf(u1592,axiom,
accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n4) ).
cnf(u1388,axiom,
( ~ accept_city(X0,northport)
| ~ accept_population(X0,other,n2)
| ~ accept_population(X0,native,n15)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n13)
| ~ accept_population(X0,atheist,n70) ) ).
cnf(u1028,axiom,
accept_population(countrybcivilorganization,other,n1) ).
cnf(u1470,axiom,
~ accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n4) ).
cnf(u1200,axiom,
accept_population(countryamedicalorganization,muslim,n1) ).
cnf(u1222,axiom,
accept_population(countryahumanitarianorganization,other,n0) ).
cnf(u1041,axiom,
accept_leader(countryccivilorganization,countrybhumanitarianorganization) ).
cnf(u1012,axiom,
accept_population(countrycmedicalorganization,christian,n3) ).
cnf(u1207,axiom,
accept_population(countryacivilorganization,christian,n20) ).
cnf(u1499,axiom,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1616,axiom,
~ any_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna) ).
cnf(u1412,axiom,
( ~ accept_city(X0,citya)
| ~ accept_population(X0,other,n0)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n0)
| ~ accept_population(X0,christian,n25)
| ~ accept_population(X0,atheist,n75) ) ).
cnf(u1392,axiom,
( accept_population(X0,native,n85)
| accept_city(X0,coastvillage) ) ).
cnf(u1572,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1224,axiom,
accept_population(countryahumanitarianorganization,muslim,n1) ).
cnf(u1410,axiom,
( accept_population(X0,native,n0)
| accept_city(X0,citya) ) ).
cnf(u1150,axiom,
accept_population(christiansufferterrahumanitarianorganization,muslim,n1) ).
cnf(u1666,axiom,
~ accept_city(countryacivilorganization,coastvillage) ).
cnf(u1563,axiom,
~ accept_team(countryafirstaidorganization,sufferterragovernment,towna,n5) ).
cnf(u1180,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n1) ).
cnf(u1423,axiom,
( accept_population(X0,other,n1)
| accept_city(X0,cityb) ) ).
cnf(u1149,axiom,
accept_population(christiansufferterrahumanitarianorganization,native,n0) ).
cnf(u1435,axiom,
~ any_agent_in_all_proposed_teams(countryahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1021,axiom,
accept_leader(countrybcivilorganization,muslimcountrybhumanitarianorganization) ).
cnf(u1724,axiom,
~ accept_number(sufferterragovernment,n1) ).
cnf(u1024,axiom,
accept_population(countrybcivilorganization,christian,n0) ).
cnf(u1174,axiom,
accept_population(muslimcountrybhumanitarianorganization,other,n5) ).
cnf(u849,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,countryahumanitarianorganization,townc) ).
cnf(u1447,axiom,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n4) ).
cnf(u1173,axiom,
accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u1568,axiom,
~ accept_number(countryamedicalorganization,n6) ).
cnf(u1364,axiom,
( ~ accept_city(X0,centraltown)
| ~ accept_population(X0,other,n9)
| ~ accept_population(X0,native,n1)
| ~ accept_population(X0,muslim,n3)
| ~ accept_population(X0,christian,n23)
| ~ accept_population(X0,atheist,n54) ) ).
cnf(u792,axiom,
the_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1497,axiom,
~ accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1575,axiom,
~ accept_number(countryahumanitarianorganization,n6) ).
cnf(u1176,axiom,
accept_population(muslimcountrybhumanitarianorganization,christian,n0) ).
cnf(u1431,axiom,
~ accept_team(countryahumanitarianorganization,countryacivilorganization,cityb,n6) ).
cnf(u988,axiom,
accept_population(christiancountrychumanitarianorganization,christian,n20) ).
cnf(u1183,axiom,
accept_population(muslimcountrybhumanitarianorganization,christian,n20) ).
cnf(u1475,axiom,
~ any_agent_in_all_proposed_teams(countrycmedicalorganization,countryacivilorganization,towna) ).
cnf(u1372,axiom,
( accept_population(X0,christian,n15)
| accept_city(X0,centrallakecity) ) ).
cnf(u1606,axiom,
~ accept_team(countrybhumanitarianorganization,countrybcivilorganization,towna,n6) ).
cnf(u1123,axiom,
accept_population(sufferterragovernment,christian,n3) ).
cnf(u992,axiom,
accept_leader(countryamedicalorganization,christiancountrychumanitarianorganization) ).
cnf(u1605,axiom,
~ accept_number(countrybhumanitarianorganization,n2) ).
cnf(u1169,axiom,
accept_population(countrycmedicalorganization,christian,n20) ).
cnf(u1477,axiom,
~ accept_number(countrycmedicalorganization,n4) ).
cnf(u1424,axiom,
( ~ accept_city(X0,cityb)
| ~ accept_population(X0,other,n1)
| ~ accept_population(X0,native,n0)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n20)
| ~ accept_population(X0,atheist,n78) ) ).
cnf(u1156,axiom,
accept_population(countryccivilorganization,muslim,n65) ).
cnf(u1553,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,cityb,n6) ).
cnf(u1403,axiom,
( accept_population(X0,muslim,n1)
| accept_city(X0,towna) ) ).
cnf(u1577,axiom,
~ accept_number(countryacivilorganization,n6) ).
cnf(u1275,axiom,
accept_population(countrybcivilorganization,muslim,n1) ).
cnf(u1449,axiom,
~ accept_team(sufferterragovernment,countryacivilorganization,cityb,n6) ).
cnf(u1128,axiom,
accept_population(sufferterragovernment,muslim,n65) ).
cnf(u1487,axiom,
~ any_agent_in_all_proposed_teams(countryacivilorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1511,axiom,
~ accept_team(christiansufferterrahumanitarianorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u1602,axiom,
~ accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n3) ).
cnf(u1084,axiom,
accept_population(countryafirstaidorganization,muslim,n65) ).
cnf(u1368,axiom,
( accept_population(X0,native,n1)
| accept_city(X0,sunnysideport) ) ).
cnf(u1558,axiom,
~ accept_team(sufferterragovernment,countryahumanitarianorganization,cityb,n6) ).
cnf(u1122,axiom,
accept_population(sufferterragovernment,muslim,n0) ).
cnf(u1557,axiom,
accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1121,axiom,
accept_population(sufferterragovernment,native,n85) ).
cnf(u1429,axiom,
( accept_population(X0,other,n5)
| accept_city(X0,townc) ) ).
cnf(u1108,axiom,
accept_leader(countrybhumanitarianorganization,countryccivilorganization) ).
cnf(u1023,axiom,
accept_population(countrybcivilorganization,muslim,n65) ).
cnf(u1077,axiom,
accept_population(countryafirstaidorganization,native,n85) ).
cnf(u1710,axiom,
~ accept_city(countryccivilorganization,towna) ).
cnf(u1362,axiom,
( accept_population(X0,native,n1)
| accept_city(X0,centraltown) ) ).
cnf(u1201,axiom,
accept_population(countryamedicalorganization,christian,n24) ).
cnf(u1618,axiom,
accept_team(christiansufferterrahumanitarianorganization,sufferterragovernment,towna,n2) ).
cnf(u1401,axiom,
( accept_population(X0,atheist,n75)
| accept_city(X0,towna) ) ).
cnf(u1709,axiom,
~ accept_city(sufferterragovernment,cityb) ).
cnf(u1080,axiom,
accept_population(countryafirstaidorganization,atheist,n12) ).
cnf(u1494,axiom,
accept_team(countryccivilorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1554,axiom,
~ accept_number(christiansufferterrahumanitarianorganization,n6) ).
cnf(u1087,axiom,
accept_leader(countryafirstaidorganization,countryahumanitarianorganization) ).
cnf(u1379,axiom,
( accept_population(X0,muslim,n1)
| accept_city(X0,stjosephburgh) ) ).
cnf(u1456,axiom,
~ accept_number(countryahumanitarianorganization,n2) ).
cnf(u823,axiom,
the_agent_in_all_proposed_teams(christiansufferterrahumanitarianorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1074,axiom,
accept_population(muslimcountrybhumanitarianorganization,christian,n3) ).
cnf(u1496,axiom,
~ accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1399,axiom,
( accept_population(X0,other,n0)
| accept_city(X0,sunsetpoint) ) ).
cnf(u1003,axiom,
accept_population(countryahumanitarianorganization,christian,n3) ).
cnf(u1551,axiom,
~ accept_team(countrybhumanitarianorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1706,axiom,
~ accept_number(countryahumanitarianorganization,n1) ).
cnf(u930,axiom,
the_agent_in_all_proposed_teams(countrybhumanitarianorganization,sufferterragovernment,towna) ).
cnf(u1662,axiom,
~ accept_city(sufferterragovernment,towna) ).
cnf(u1099,axiom,
accept_population(countrybhumanitarianorganization,atheist,n12) ).
cnf(u1490,axiom,
~ accept_team(countryafirstaidorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u1331,axiom,
accept_leader(christiancountrychumanitarianorganization,sufferterragovernment) ).
cnf(u1768,axiom,
accept_city(muslimcountrybhumanitarianorganization,towna) ).
cnf(u1515,axiom,
~ accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1385,axiom,
( accept_population(X0,muslim,n0)
| accept_city(X0,northport) ) ).
cnf(u1658,axiom,
~ accept_city(countrycmedicalorganization,coastvillage) ).
cnf(u1715,axiom,
~ accept_number(countryafirstaidorganization,n1) ).
cnf(u1574,axiom,
~ any_agent_in_all_proposed_teams(countryahumanitarianorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1391,axiom,
( accept_population(X0,muslim,n0)
| accept_city(X0,coastvillage) ) ).
cnf(u1657,axiom,
~ accept_city(countryahumanitarianorganization,coastvillage) ).
cnf(u1476,axiom,
~ accept_team(countrycmedicalorganization,christiancountrychumanitarianorganization,coastvillage,n5) ).
cnf(u1573,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1530,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1527,axiom,
~ accept_team(christiancountrychumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u1539,axiom,
~ accept_team(countrybhumanitarianorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u1001,axiom,
accept_population(countryahumanitarianorganization,native,n85) ).
cnf(u1350,axiom,
( ~ the_agent_in_all_proposed_teams(X0,X1,X2)
| ~ accept_city(X0,X2) ) ).
cnf(u1097,axiom,
accept_population(countrybhumanitarianorganization,muslim,n0) ).
cnf(u1628,axiom,
~ accept_team(countryacivilorganization,sufferterragovernment,towna,n5) ).
cnf(u1516,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n6) ).
cnf(u1436,axiom,
~ accept_team(countryccivilorganization,countrybhumanitarianorganization,cityb,n2) ).
cnf(u1727,axiom,
~ accept_number(countryacivilorganization,n4) ).
cnf(u1363,axiom,
( accept_population(X0,other,n9)
| accept_city(X0,centraltown) ) ).
cnf(u1383,axiom,
( accept_population(X0,atheist,n70)
| accept_city(X0,northport) ) ).
cnf(u1051,axiom,
accept_leader(countryacivilorganization,christiancountrychumanitarianorganization) ).
cnf(u1694,axiom,
~ accept_number(countryamedicalorganization,n4) ).
cnf(u1365,axiom,
( accept_population(X0,atheist,n30)
| accept_city(X0,sunnysideport) ) ).
cnf(u997,axiom,
accept_leader(countryamedicalorganization,countryahumanitarianorganization) ).
cnf(u1700,axiom,
~ accept_city(countryacivilorganization,cityb) ).
cnf(u1354,axiom,
( accept_population(X0,christian,n20)
| accept_city(X0,suffertown) ) ).
cnf(u1691,axiom,
~ accept_city(muslimcountrybhumanitarianorganization,cityb) ).
cnf(u2050,axiom,
accept_city(muslimcountrybhumanitarianorganization,citya) ).
cnf(u1060,axiom,
~ accept_leader(christiansufferterrahumanitarianorganization,sufferterragovernment) ).
cnf(u1544,axiom,
~ accept_team(countrycmedicalorganization,muslimcountrybhumanitarianorganization,townc,n6) ).
cnf(u1468,axiom,
accept_team(countryccivilorganization,countrycmedicalorganization,towna,n5) ).
cnf(u1615,axiom,
~ accept_team(countrybcivilorganization,countrycmedicalorganization,towna,n6) ).
cnf(u1473,axiom,
~ any_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna) ).
cnf(u1225,axiom,
accept_population(countryahumanitarianorganization,christian,n24) ).
cnf(u1152,axiom,
accept_population(christiansufferterrahumanitarianorganization,atheist,n78) ).
cnf(u1463,axiom,
accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n6) ).
cnf(u1462,axiom,
accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n6) ).
cnf(u1451,axiom,
~ any_agent_in_all_proposed_teams(countrybhumanitarianorganization,countryacivilorganization,towna) ).
cnf(u1696,axiom,
~ accept_number(countryamedicalorganization,n2) ).
cnf(u1492,axiom,
~ any_agent_in_all_proposed_teams(countryafirstaidorganization,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1375,axiom,
( accept_population(X0,other,n4)
| accept_city(X0,centrallakecity) ) ).
cnf(u949,axiom,
the_agent_in_all_proposed_teams(countryccivilorganization,sufferterragovernment,towna) ).
cnf(u1703,axiom,
~ accept_number(countryahumanitarianorganization,n4) ).
cnf(u1294,axiom,
accept_population(countryacivilorganization,christian,n24) ).
cnf(u1102,axiom,
accept_population(countrybhumanitarianorganization,other,n5) ).
cnf(u1711,axiom,
~ accept_number(countryafirstaidorganization,n5) ).
cnf(u1643,axiom,
~ accept_number(countrybhumanitarianorganization,n6) ).
cnf(u1260,axiom,
accept_leader(countrycmedicalorganization,countrybhumanitarianorganization) ).
cnf(u1101,axiom,
accept_leader(countrybhumanitarianorganization,muslimcountrybhumanitarianorganization) ).
cnf(u1545,axiom,
~ accept_team(countrycmedicalorganization,countrybcivilorganization,townc,n6) ).
cnf(u1292,axiom,
accept_population(countryacivilorganization,native,n0) ).
cnf(u1251,axiom,
accept_population(countryafirstaidorganization,native,n0) ).
cnf(u1676,axiom,
~ accept_city(countrybhumanitarianorganization,towna) ).
cnf(u1104,axiom,
accept_population(countrybhumanitarianorganization,christian,n0) ).
cnf(u1254,axiom,
accept_population(countryafirstaidorganization,atheist,n75) ).
cnf(u1073,axiom,
accept_population(muslimcountrybhumanitarianorganization,muslim,n0) ).
cnf(u1488,axiom,
~ accept_number(countryafirstaidorganization,n2) ).
cnf(u1437,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ).
cnf(u1111,axiom,
accept_leader(countrybhumanitarianorganization,countrycmedicalorganization) ).
cnf(u1253,axiom,
accept_population(countryafirstaidorganization,christian,n24) ).
cnf(u1648,axiom,
~ accept_number(countrycmedicalorganization,n6) ).
cnf(u1444,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ).
cnf(u1098,axiom,
accept_population(countrybhumanitarianorganization,christian,n3) ).
cnf(u1854,axiom,
accept_team(muslimcountrybhumanitarianorganization,X0,towna,X1) ).
cnf(u1655,axiom,
accept_city(countryamedicalorganization,coastvillage) ).
cnf(u1256,axiom,
accept_leader(countryafirstaidorganization,sufferterragovernment) ).
cnf(u1054,axiom,
accept_population(countryacivilorganization,christian,n0) ).
cnf(u1730,axiom,
~ accept_number(countryacivilorganization,n1) ).
cnf(u1595,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1212,axiom,
accept_population(countryahumanitarianorganization,other,n1) ).
cnf(u1053,axiom,
accept_population(countryacivilorganization,muslim,n65) ).
cnf(u1686,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,cityb) ).
cnf(u1250,axiom,
accept_population(countryafirstaidorganization,other,n0) ).
cnf(u1506,axiom,
~ accept_team(sufferterragovernment,countryafirstaidorganization,coastvillage,n6) ).
cnf(u1377,axiom,
( accept_population(X0,atheist,n68)
| accept_city(X0,stjosephburgh) ) ).
cnf(u1056,axiom,
accept_leader(countryacivilorganization,countryahumanitarianorganization) ).
cnf(u1206,axiom,
accept_population(countryacivilorganization,other,n1) ).
cnf(u1397,axiom,
( accept_population(X0,muslim,n0)
| accept_city(X0,sunsetpoint) ) ).
cnf(u1398,axiom,
( accept_population(X0,native,n100)
| accept_city(X0,sunsetpoint) ) ).
cnf(u1063,axiom,
accept_population(christiansufferterrahumanitarianorganization,other,n0) ).
cnf(u1654,axiom,
~ accept_city(christiancountrychumanitarianorganization,cityb) ).
cnf(u1396,axiom,
( accept_population(X0,christian,n0)
| accept_city(X0,sunsetpoint) ) ).
cnf(u1529,axiom,
~ accept_team(christiancountrychumanitarianorganization,countrybhumanitarianorganization,townc,n6) ).
cnf(u1208,axiom,
accept_population(countryacivilorganization,atheist,n78) ).
cnf(u979,axiom,
accept_leader(christiancountrychumanitarianorganization,countryacivilorganization) ).
cnf(u1049,axiom,
accept_population(countryacivilorganization,atheist,n12) ).
cnf(u1682,axiom,
~ accept_number(christiansufferterrahumanitarianorganization,n3) ).
cnf(u1027,axiom,
accept_leader(countrybcivilorganization,countryahumanitarianorganization) ).
cnf(u1032,axiom,
accept_leader(sufferterragovernment,countryamedicalorganization) ).
cnf(u1507,axiom,
~ any_agent_in_all_proposed_teams(sufferterragovernment,christiancountrychumanitarianorganization,coastvillage) ).
cnf(u1177,axiom,
accept_population(muslimcountrybhumanitarianorganization,atheist,n30) ).
cnf(u1681,axiom,
~ accept_number(christiansufferterrahumanitarianorganization,n4) ).
cnf(u1607,axiom,
~ accept_team(countrybhumanitarianorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1202,axiom,
accept_population(countryamedicalorganization,atheist,n75) ).
cnf(u1329,axiom,
accept_population(christiancountrychumanitarianorganization,atheist,n75) ).
cnf(u1637,axiom,
~ any_agent_in_all_proposed_teams(countrycmedicalorganization,sufferterragovernment,towna) ).
cnf(u1030,axiom,
accept_population(countrybcivilorganization,atheist,n78) ).
cnf(u1509,axiom,
~ accept_number(countryahumanitarianorganization,n5) ).
cnf(u1188,axiom,
accept_population(countryamedicalorganization,other,n1) ).
cnf(u1029,axiom,
accept_population(countrybcivilorganization,christian,n20) ).
cnf(u1408,axiom,
( accept_population(X0,christian,n25)
| accept_city(X0,citya) ) ).
cnf(u1000,axiom,
accept_leader(countryahumanitarianorganization,countryafirstaidorganization) ).
cnf(u1526,axiom,
~ accept_team(christiancountrychumanitarianorganization,countryccivilorganization,townc,n4) ).
cnf(u999,axiom,
accept_leader(countryahumanitarianorganization,countryamedicalorganization) ).
cnf(u1763,axiom,
~ accept_number(muslimcountrybhumanitarianorganization,n4) ).
cnf(u1634,axiom,
~ accept_team(countrycmedicalorganization,countrybcivilorganization,towna,n6) ).
cnf(u1039,axiom,
accept_population(countryccivilorganization,atheist,n78) ).
cnf(u1459,axiom,
accept_team(countryamedicalorganization,countryacivilorganization,coastvillage,n2) ).
cnf(u1596,axiom,
~ accept_team(countryamedicalorganization,sufferterragovernment,towna,n5) ).
cnf(u775,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,countryacivilorganization,towna) ).
cnf(u1158,axiom,
accept_population(countryccivilorganization,atheist,n30) ).
cnf(u1589,axiom,
accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n3) ).
cnf(u1025,axiom,
accept_population(countrybcivilorganization,atheist,n30) ).
cnf(u1461,axiom,
accept_team(countryamedicalorganization,sufferterragovernment,coastvillage,n2) ).
cnf(u1540,axiom,
~ accept_team(sufferterragovernment,countryahumanitarianorganization,townc,n6) ).
cnf(u1414,axiom,
( accept_population(X0,christian,n20)
| accept_city(X0,townb) ) ).
cnf(u1010,axiom,
accept_population(countrycmedicalorganization,native,n85) ).
cnf(u1614,axiom,
~ accept_team(countrybcivilorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1622,axiom,
accept_team(countryccivilorganization,countrybcivilorganization,towna,n6) ).
cnf(u1522,axiom,
~ accept_team(muslimcountrybhumanitarianorganization,countrycmedicalorganization,townc,n6) ).
cnf(u1613,axiom,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1374,axiom,
( accept_population(X0,native,n10)
| accept_city(X0,centrallakecity) ) ).
cnf(u1586,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybcivilorganization,towna,n3) ).
cnf(u1585,axiom,
accept_team(muslimcountrybhumanitarianorganization,countryccivilorganization,towna,n2) ).
cnf(u1154,axiom,
accept_leader(christiansufferterrahumanitarianorganization,countrybhumanitarianorganization) ).
cnf(u1006,axiom,
accept_leader(countryahumanitarianorganization,christiancountrychumanitarianorganization) ).
cnf(u1405,axiom,
( accept_population(X0,other,n0)
| accept_city(X0,towna) ) ).
cnf(u1610,axiom,
~ accept_number(countrybcivilorganization,n2) ).
cnf(u1667,axiom,
~ accept_city(countryacivilorganization,townc) ).
cnf(u1508,axiom,
~ accept_number(christiansufferterrahumanitarianorganization,n2) ).
cnf(u879,axiom,
the_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1130,axiom,
accept_population(sufferterragovernment,atheist,n30) ).
cnf(u1378,axiom,
( accept_population(X0,christian,n16)
| accept_city(X0,stjosephburgh) ) ).
cnf(u1565,axiom,
~ accept_team(countrycmedicalorganization,countrybhumanitarianorganization,cityb,n5) ).
cnf(u1482,axiom,
~ accept_team(countryafirstaidorganization,countryacivilorganization,towna,n6) ).
cnf(u1129,axiom,
accept_population(sufferterragovernment,christian,n0) ).
cnf(u1469,axiom,
~ any_agent_in_all_proposed_teams(countryccivilorganization,countryacivilorganization,towna) ).
cnf(u1464,axiom,
accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u986,axiom,
accept_leader(christiancountrychumanitarianorganization,countryahumanitarianorganization) ).
cnf(u1672,axiom,
~ accept_city(countryafirstaidorganization,townc) ).
cnf(u1261,axiom,
accept_leader(countrycmedicalorganization,christiancountrychumanitarianorganization) ).
cnf(u1271,axiom,
accept_leader(countrybcivilorganization,christiancountrychumanitarianorganization) ).
cnf(u1679,axiom,
~ accept_city(christiansufferterrahumanitarianorganization,townc) ).
cnf(u1562,axiom,
~ any_agent_in_all_proposed_teams(countryafirstaidorganization,countrybhumanitarianorganization,cityb) ).
cnf(u1116,axiom,
accept_population(countrybhumanitarianorganization,atheist,n75) ).
cnf(u1327,axiom,
accept_population(christiancountrychumanitarianorganization,muslim,n1) ).
cnf(u1635,axiom,
~ accept_team(countrycmedicalorganization,countrybhumanitarianorganization,towna,n6) ).
cnf(u1359,axiom,
( accept_population(X0,atheist,n54)
| accept_city(X0,centraltown) ) ).
cnf(u982,axiom,
accept_population(christiancountrychumanitarianorganization,muslim,n65) ).
cnf(u1458,axiom,
accept_team(countryamedicalorganization,countryafirstaidorganization,coastvillage,n2) ).
cnf(u1434,axiom,
~ accept_team(countryahumanitarianorganization,countryafirstaidorganization,coastvillage,n6) ).
cnf(u1230,axiom,
accept_leader(sufferterragovernment,countryacivilorganization) ).
cnf(u1266,axiom,
accept_population(countrycmedicalorganization,atheist,n75) ).
cnf(u1647,axiom,
~ any_agent_in_all_proposed_teams(christiancountrychumanitarianorganization,sufferterragovernment,towna) ).
cnf(u938,axiom,
the_agent_in_all_proposed_teams(countrybcivilorganization,sufferterragovernment,towna) ).
cnf(u1624,axiom,
accept_team(countryccivilorganization,christiancountrychumanitarianorganization,towna,n6) ).
cnf(u1420,axiom,
( accept_population(X0,christian,n20)
| accept_city(X0,cityb) ) ).
cnf(u1351,axiom,
( any_agent_in_all_proposed_teams(X0,X1,X2)
| accept_leader(X0,X1) ) ).
cnf(u1631,axiom,
~ accept_number(countrycmedicalorganization,n2) ).
cnf(u1479,axiom,
~ accept_number(countrycmedicalorganization,n5) ).
cnf(u1753,axiom,
~ accept_number(christiancountrychumanitarianorganization,n1) ).
cnf(u1571,axiom,
~ accept_team(countrybcivilorganization,countrybhumanitarianorganization,cityb,n6) ).
cnf(u1239,axiom,
accept_population(countryccivilorganization,native,n0) ).
cnf(u1376,axiom,
( ~ accept_city(X0,centrallakecity)
| ~ accept_population(X0,other,n4)
| ~ accept_population(X0,native,n10)
| ~ accept_population(X0,muslim,n1)
| ~ accept_population(X0,christian,n15)
| ~ accept_population(X0,atheist,n70) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT042+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n016.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 19:21:19 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.29 % (3910836)Will run a generic schedule for satisfiability detection.
% 0.21/0.29 % (3910847)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3065690950:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.29 % (3910842)% WARNING: option uhcvi not known.
% 0.21/0.29 % (3910841)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3344724447_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.29 % (3910843)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1626376876:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.29 % (3910842)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=709265867:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.29 % (3910844)dis+10_1_sil=32000:sp=arity:random_seed=2816170547:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.29 % (3910845)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2711639532:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.29 % (3910846)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3647020545:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % (3910842) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3910836-3910842"...
% 0.21/0.30 % (3910842)...printing done.
% 0.21/0.30 % (3910847) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3910836-3910847"...
% 0.21/0.30 % Detected minimum model sizes of [1]
% 0.21/0.30 % Detected maximum model sizes of [60]
% 0.21/0.30 % TRYING [1]
% 0.21/0.30 % SZS status Satisfiable for theBenchmark
% 0.21/0.30 % SZS output start Saturation.
% See solution above
% 0.21/0.31 % SZS output start Definitions and Model Updates.
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "the_agent_not_in_any_proposed_teams"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "any_agent_in_all_proposed_teams"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "accept_number"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "accept_city"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "accept_team"
% 0.21/0.31 for all inputs,
% 0.21/0.31 define less(X0,X1) := $false
% 0.21/0.31 for all inputs,
% 0.21/0.31 define min_number_of_proposed_agents(X0,X1) := $false
% 0.21/0.31 % SZS output end Definitions and Model Updates.
% 0.21/0.31 % (3910842)------------------------------
% 0.21/0.31 % (3910842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (3910842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (3910842)CaDiCaL version: 2.1.3
% 0.21/0.31 % (3910842)Termination reason: Satisfiable
% 0.21/0.31 % (3910842)Time elapsed: 0.018 s
% 0.21/0.31 % (3910842)Peak memory usage: 13 MB
% 0.21/0.31 % (3910842)Instructions burned: 30 (million)
% 0.21/0.31 % (3910836)Success in time 0.056 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------