%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEG001+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:50:01 AM UTC 2026
% Result : Satisfiable 4.85s 1.18s
% Output : Saturation 5.41s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1170,axiom,
~ relation(sK155,of,sK240) ).
cnf(u1179,axiom,
~ relation(sK289,of,sK174) ).
cnf(u1182,axiom,
object(sK289,part,countable,na,eq,n1) ).
cnf(u1187,axiom,
~ predicate(X460,appreciate,X459,sK169) ).
cnf(u1274,axiom,
~ object(X552,dwarf_planet,countable,na,eq,n1) ).
cnf(u1277,axiom,
~ object(X554,moon,countable,na,eq,n1) ).
cnf(u1355,axiom,
sK461(X584) = X584 ).
cnf(u1385,axiom,
sK444(X540) = X540 ).
cnf(u1469,axiom,
sK433(X515) = X515 ).
cnf(u1484,axiom,
sK455(X571) = X571 ).
cnf(u1607,axiom,
sK415(X473,X474) = X474 ).
cnf(u1619,axiom,
sK394(X421,X422) = X421 ).
cnf(u1631,axiom,
sK465(X594) = X594 ).
cnf(u1634,axiom,
~ object(X594,multilingual_country,countable,na,eq,n1) ).
cnf(u1637,axiom,
sK464(X592) = X592 ).
cnf(u1652,axiom,
sK463(X590) = X590 ).
cnf(u1658,axiom,
sK462(X588) = X588 ).
cnf(u1664,axiom,
sK460(X580) = X580 ).
cnf(u1670,axiom,
sK446(X547) = X547 ).
cnf(u1787,axiom,
sK429(X503) = X503 ).
cnf(u1820,axiom,
sK412(X469) = X469 ).
cnf(u1838,axiom,
sK410(X463) = X463 ).
cnf(u1849,axiom,
sK408(X457) = X457 ).
cnf(u1853,axiom,
sK403(X443) = X443 ).
cnf(u1876,axiom,
sK398(X433) = X433 ).
cnf(u1886,axiom,
sK397(X431) = X431 ).
cnf(u1896,axiom,
sK396(X429) = X429 ).
cnf(u1905,axiom,
sK393(X419) = X419 ).
cnf(u1917,axiom,
sK392(X416) = X416 ).
cnf(u1932,axiom,
sK390(X410) = X410 ).
cnf(u1943,axiom,
sK387(X398) = X398 ).
cnf(u1954,axiom,
sK384(X388) = X388 ).
cnf(u1960,axiom,
predicate(sK468(X600),control,X600,sK467(X600)) ).
cnf(u2077,axiom,
predicate(sK432(X511,X512),overlap_with,X512,X511) ).
cnf(u2108,axiom,
~ predicate(X487,locate,X485,X486) ).
cnf(u2125,axiom,
sK414(X469) = X469 ).
cnf(u2132,axiom,
predicate(sK411(X465,X466),govern,X465,X466) ).
cnf(u2153,axiom,
relation(X433,of,sK372) ).
cnf(u2267,axiom,
object(X584,river,countable,na,eq,n1) ).
cnf(u2324,axiom,
object(X540,area,countable,na,eq,n1) ).
cnf(u2401,axiom,
relation(X443,of,sK404(X443)) ).
cnf(u2424,axiom,
predicate(sK453(X564),orbit,X564,sK187) ).
cnf(u2436,axiom,
predicate(sK448(X555),orbit,X555,sK447(X555)) ).
cnf(u2448,axiom,
predicate(sK442(X531),contain,sK439(X531),X531) ).
cnf(u2487,axiom,
predicate(sK438(X528),have,X528,sK437(X528)) ).
cnf(u2523,axiom,
predicate(sK436(X525),contain,X525,sK435(X525)) ).
cnf(u2562,axiom,
predicate(sK431(X506),have,X506,sK430(X506)) ).
cnf(u2586,axiom,
property(X503,located_in,pos,sK428(X503)) ).
cnf(u2612,axiom,
predicate(sK427(X500),have,X500,sK426(X500)) ).
cnf(u2635,axiom,
predicate(sK425(X497),have,X497,sK424(X497)) ).
cnf(u2658,axiom,
predicate(sK423(X494),have,X494,sK422(X494)) ).
cnf(u2681,axiom,
predicate(sK420(X489),contain,sK419(X489),X489) ).
cnf(u2691,axiom,
object(X474,part,countable,na,eq,n1) ).
cnf(u2702,axiom,
property(X469,located_in,pos,sK413(X469)) ).
cnf(u2731,axiom,
sK405(X447) = X447 ).
cnf(u2831,axiom,
object(X592,nATO_country,countable,na,eq,n1) ).
cnf(u2867,axiom,
relation(sK383(X386),of,sK174) ).
cnf(u2879,axiom,
sK451(X561) = X561 ).
cnf(u2882,axiom,
sK452(X561) = X561 ).
cnf(u2894,axiom,
object(sK447(X555),star,countable,na,eq,n1) ).
cnf(u2899,axiom,
~ object(sK447(X0),planet,countable,na,eq,n1) ).
cnf(u2905,axiom,
object(X547,celestial_body,countable,na,eq,n1) ).
cnf(u2917,axiom,
predicate(sK441(X531),contain,sK440(X531),sK439(X531)) ).
cnf(u2928,axiom,
object(sK440(X531),country,countable,na,eq,n1) ).
cnf(u2949,axiom,
object(sK439(X531),subregion,countable,na,eq,n1) ).
cnf(u2954,axiom,
object(sK437(X528),mayor,countable,na,exactly,n1) ).
cnf(u2957,axiom,
object(sK435(X525),person,countable,na,greater,n1) ).
cnf(u2960,axiom,
object(sK430(X506),capital,countable,na,eq,n1) ).
cnf(u2967,axiom,
~ object(sK430(X0),country,countable,na,eq,n1) ).
cnf(u2982,axiom,
~ object(sK428(X0),island,countable,na,eq,n1) ).
cnf(u2990,axiom,
object(sK426(X500),capital,countable,na,eq,n1) ).
cnf(u2997,axiom,
~ object(sK426(X0),country,countable,na,eq,n1) ).
cnf(u3004,axiom,
object(sK422(X494),city,countable,na,geq,n1) ).
cnf(u3007,axiom,
object(sK419(X489),country,countable,na,eq,n1) ).
cnf(u3026,axiom,
object(sK413(X469),country,countable,na,eq,n1) ).
cnf(u3046,axiom,
object(X469,subregion,countable,na,eq,n1) ).
cnf(u3082,axiom,
~ object(sK404(X0),island,countable,na,eq,n1) ).
cnf(u3105,axiom,
sK456(X574) = X574 ).
cnf(u3163,axiom,
predicate(sK409(X461),dislike,X461,sK169) ).
cnf(u3331,axiom,
relation(sK174,of,sK174) ).
cnf(u3339,axiom,
relation(sK230,of,sK174) ).
cnf(u3347,axiom,
relation(sK262,of,sK174) ).
cnf(u3350,axiom,
~ predicate(X0,border,sK293,sK250) ).
cnf(u3355,axiom,
relation(sK310,of,sK174) ).
cnf(u3358,axiom,
~ predicate(X0,border,sK238,sK250) ).
cnf(u3363,axiom,
relation(sK317,of,sK174) ).
cnf(u3371,axiom,
relation(sK380,of,sK174) ).
cnf(u3379,axiom,
relation(sK11,of,sK174) ).
cnf(u3382,axiom,
~ predicate(X0,border,sK250,sK250) ).
cnf(u3387,axiom,
relation(sK51,of,sK174) ).
cnf(u3390,axiom,
~ predicate(X0,border,sK176,sK250) ).
cnf(u3400,axiom,
relation(sK87,of,sK174) ).
cnf(u3408,axiom,
relation(sK188,of,sK174) ).
cnf(u3415,axiom,
sK385(X391) = X391 ).
cnf(u3610,axiom,
relation(sK237,of,sK174) ).
cnf(u3618,axiom,
relation(sK238,of,sK174) ).
cnf(u3621,axiom,
~ predicate(X0,border,sK310,sK250) ).
cnf(u3631,axiom,
relation(sK271,of,sK174) ).
cnf(u3634,axiom,
~ predicate(X0,border,sK262,sK250) ).
cnf(u3639,axiom,
relation(sK293,of,sK174) ).
cnf(u3649,axiom,
relation(sK401(X1),of,sK174) ).
cnf(u3661,axiom,
sK388(X401) = X401 ).
cnf(u3676,axiom,
sK389(X406) = X406 ).
cnf(u3691,axiom,
sK386(X395,X396) = X395 ).
cnf(u3707,axiom,
sK323 = sK445(X545) ).
cnf(u3716,axiom,
predicate(sK400(X435),contain,X435,sK399(X435)) ).
cnf(u5936,axiom,
sK449(X558) = X558 ).
cnf(u5939,axiom,
predicate(sK450(X558),orbit,X558,sK187) ).
cnf(u5952,axiom,
sK457(X576) = X576 ).
cnf(u6013,axiom,
object(sK399(X435),country,countable,na,geq,n2) ).
cnf(u6044,axiom,
property(sK323,larger_than,pos,X545) ).
cnf(u6769,axiom,
~ predicate(sK459(sK141),border,sK141,sK458(sK141)) ).
cnf(u6774,axiom,
object(sK141,landlocked_country,countable,na,eq,n1) ).
cnf(u6794,axiom,
relation(sK458(sK141),of,sK174) ).
cnf(u6801,axiom,
~ predicate(sK459(sK147),border,sK147,sK458(sK147)) ).
cnf(u6806,axiom,
object(sK147,landlocked_country,countable,na,eq,n1) ).
cnf(u6826,axiom,
relation(sK458(sK147),of,sK174) ).
cnf(u6833,axiom,
~ predicate(sK459(sK159),border,sK159,sK458(sK159)) ).
cnf(u6838,axiom,
object(sK159,landlocked_country,countable,na,eq,n1) ).
cnf(u6858,axiom,
relation(sK458(sK159),of,sK174) ).
cnf(u6865,axiom,
~ predicate(sK459(sK172),border,sK172,sK458(sK172)) ).
cnf(u6870,axiom,
object(sK172,landlocked_country,countable,na,eq,n1) ).
cnf(u6890,axiom,
relation(sK458(sK172),of,sK174) ).
cnf(u6898,axiom,
predicate(sK459(sK176),border,sK176,sK458(sK176)) ).
cnf(u6902,axiom,
object(sK176,landlocked_country,countable,na,eq,n1) ).
cnf(u6922,axiom,
predicate(sK459(sK193),border,sK193,sK458(sK193)) ).
cnf(u6926,axiom,
object(sK193,landlocked_country,countable,na,eq,n1) ).
cnf(u6946,axiom,
relation(sK458(sK193),of,sK174) ).
cnf(u6954,axiom,
predicate(sK459(sK238),border,sK238,sK458(sK238)) ).
cnf(u6958,axiom,
object(sK238,landlocked_country,countable,na,eq,n1) ).
cnf(u6983,axiom,
predicate(sK459(sK240),border,sK240,sK458(sK240)) ).
cnf(u6987,axiom,
object(sK240,landlocked_country,countable,na,eq,n1) ).
cnf(u7007,axiom,
relation(sK458(sK240),of,sK174) ).
cnf(u7016,axiom,
predicate(sK459(sK250),border,sK250,sK458(sK250)) ).
cnf(u7020,axiom,
object(sK250,landlocked_country,countable,na,eq,n1) ).
cnf(u7043,axiom,
relation(sK159,of,sK174) ).
cnf(u7051,axiom,
relation(sK193,of,sK174) ).
cnf(u7058,axiom,
~ predicate(sK459(sK260),border,sK260,sK458(sK260)) ).
cnf(u7063,axiom,
object(sK260,landlocked_country,countable,na,eq,n1) ).
cnf(u7083,axiom,
relation(sK260,of,sK174) ).
cnf(u7091,axiom,
relation(sK458(sK260),of,sK174) ).
cnf(u7098,axiom,
~ predicate(sK459(sK262),border,sK262,sK458(sK262)) ).
cnf(u7103,axiom,
object(sK262,landlocked_country,countable,na,eq,n1) ).
cnf(u7123,axiom,
predicate(sK459(sK287),border,sK287,sK458(sK287)) ).
cnf(u7127,axiom,
object(sK287,landlocked_country,countable,na,eq,n1) ).
cnf(u7147,axiom,
relation(sK287,of,sK174) ).
cnf(u7155,axiom,
relation(sK458(sK287),of,sK174) ).
cnf(u7163,axiom,
predicate(sK459(sK289),border,sK289,sK458(sK289)) ).
cnf(u7167,axiom,
object(sK289,landlocked_country,countable,na,eq,n1) ).
cnf(u7188,axiom,
relation(sK458(sK289),of,sK174) ).
cnf(u7196,axiom,
predicate(sK459(sK293),border,sK293,sK458(sK293)) ).
cnf(u7200,axiom,
object(sK293,landlocked_country,countable,na,eq,n1) ).
cnf(u7228,axiom,
~ predicate(sK459(sK305),border,sK305,sK458(sK305)) ).
cnf(u7233,axiom,
object(sK305,landlocked_country,countable,na,eq,n1) ).
cnf(u7253,axiom,
relation(sK458(sK305),of,sK174) ).
cnf(u7260,axiom,
predicate(sK459(sK310),border,sK310,sK458(sK310)) ).
cnf(u7264,axiom,
object(sK310,landlocked_country,countable,na,eq,n1) ).
cnf(u7289,axiom,
predicate(sK459(sK313),border,sK313,sK458(sK313)) ).
cnf(u7293,axiom,
object(sK313,landlocked_country,countable,na,eq,n1) ).
cnf(u7313,axiom,
relation(sK313,of,sK174) ).
cnf(u7321,axiom,
relation(sK458(sK313),of,sK174) ).
cnf(u7329,axiom,
predicate(sK459(sK315),border,sK315,sK458(sK315)) ).
cnf(u7333,axiom,
object(sK315,landlocked_country,countable,na,eq,n1) ).
cnf(u7353,axiom,
relation(sK458(sK315),of,sK174) ).
cnf(u7361,axiom,
predicate(sK459(sK367),border,sK367,sK458(sK367)) ).
cnf(u7365,axiom,
object(sK367,landlocked_country,countable,na,eq,n1) ).
cnf(u7385,axiom,
relation(sK458(sK367),of,sK174) ).
cnf(u7393,axiom,
predicate(sK459(sK380),border,sK380,sK458(sK380)) ).
cnf(u7397,axiom,
object(sK380,landlocked_country,countable,na,eq,n1) ).
cnf(u7417,axiom,
relation(sK458(sK380),of,sK174) ).
cnf(u7425,axiom,
predicate(sK459(sK152),border,sK152,sK458(sK152)) ).
cnf(u7429,axiom,
object(sK152,landlocked_country,countable,na,eq,n1) ).
cnf(u7449,axiom,
relation(sK458(sK152),of,sK174) ).
cnf(u7457,axiom,
predicate(sK459(sK317),border,sK317,sK458(sK317)) ).
cnf(u7461,axiom,
object(sK317,landlocked_country,countable,na,eq,n1) ).
cnf(u7482,axiom,
relation(sK458(sK317),of,sK174) ).
cnf(u7490,axiom,
predicate(sK459(sK368),border,sK368,sK458(sK368)) ).
cnf(u7494,axiom,
object(sK368,landlocked_country,countable,na,eq,n1) ).
cnf(u7514,axiom,
relation(sK458(sK368),of,sK174) ).
cnf(u7522,axiom,
predicate(sK459(sK369),border,sK369,sK458(sK369)) ).
cnf(u7526,axiom,
object(sK369,landlocked_country,countable,na,eq,n1) ).
cnf(u7546,axiom,
relation(sK458(sK369),of,sK174) ).
cnf(u7554,axiom,
predicate(sK459(sK370),border,sK370,sK458(sK370)) ).
cnf(u7558,axiom,
object(sK370,landlocked_country,countable,na,eq,n1) ).
cnf(u7578,axiom,
relation(sK458(sK370),of,sK174) ).
cnf(u7586,axiom,
predicate(sK459(sK372),border,sK372,sK458(sK372)) ).
cnf(u7590,axiom,
object(sK372,landlocked_country,countable,na,eq,n1) ).
cnf(u7610,axiom,
relation(sK372,of,sK174) ).
cnf(u7618,axiom,
relation(sK458(sK372),of,sK174) ).
cnf(u7625,axiom,
~ predicate(X0,border,sK458(sK404(sK430(X1))),sK250) ).
cnf(u7628,axiom,
relation(sK404(sK430(X1)),of,sK174) ).
cnf(u7631,axiom,
~ predicate(X0,border,sK458(sK404(sK426(X1))),sK250) ).
cnf(u7634,axiom,
relation(sK404(sK426(X1)),of,sK174) ).
cnf(u7637,axiom,
~ predicate(X0,border,sK458(sK428(sK430(X1))),sK250) ).
cnf(u7640,axiom,
relation(sK428(sK430(X1)),of,sK174) ).
cnf(u7643,axiom,
~ predicate(X0,border,sK458(sK428(sK426(X1))),sK250) ).
cnf(u7646,axiom,
relation(sK428(sK426(X1)),of,sK174) ).
cnf(u7654,axiom,
~ predicate(X0,border,sK404(sK430(X1)),sK250) ).
cnf(u7657,axiom,
relation(sK458(sK404(sK430(X1))),of,sK174) ).
cnf(u7665,axiom,
~ predicate(X0,border,sK404(sK426(X1)),sK250) ).
cnf(u7668,axiom,
relation(sK458(sK404(sK426(X1))),of,sK174) ).
cnf(u7676,axiom,
~ predicate(X0,border,sK428(sK430(X1)),sK250) ).
cnf(u7679,axiom,
relation(sK458(sK428(sK430(X1))),of,sK174) ).
cnf(u7687,axiom,
~ predicate(X0,border,sK428(sK426(X1)),sK250) ).
cnf(u7690,axiom,
relation(sK458(sK428(sK426(X1))),of,sK174) ).
cnf(u7713,axiom,
object(sK413(X0),landlocked_country,countable,na,eq,n1) ).
cnf(u7716,axiom,
predicate(sK459(sK413(X0)),border,sK413(X0),sK458(sK413(X0))) ).
cnf(u7738,axiom,
~ predicate(X0,border,sK458(sK413(X1)),sK250) ).
cnf(u7741,axiom,
relation(sK413(X1),of,sK174) ).
cnf(u7749,axiom,
~ predicate(X0,border,sK413(X1),sK250) ).
cnf(u7752,axiom,
relation(sK458(sK413(X1)),of,sK174) ).
cnf(u7760,axiom,
object(sK419(X0),landlocked_country,countable,na,eq,n1) ).
cnf(u7785,axiom,
~ predicate(X0,border,sK458(sK419(X1)),sK250) ).
cnf(u7788,axiom,
relation(sK419(X1),of,sK174) ).
cnf(u7796,axiom,
~ predicate(X0,border,sK419(X1),sK250) ).
cnf(u7799,axiom,
relation(sK458(sK419(X1)),of,sK174) ).
cnf(u7807,axiom,
object(sK440(X0),landlocked_country,countable,na,eq,n1) ).
cnf(u7810,axiom,
predicate(sK459(sK440(X0)),border,sK440(X0),sK458(sK440(X0))) ).
cnf(u7832,axiom,
~ predicate(X0,border,sK458(sK440(X1)),sK250) ).
cnf(u7835,axiom,
relation(sK440(X1),of,sK174) ).
cnf(u7843,axiom,
~ predicate(X0,border,sK440(X1),sK250) ).
cnf(u7846,axiom,
relation(sK458(sK440(X1)),of,sK174) ).
cnf(u7988,axiom,
~ predicate(X0,border,sK317,sK401(sK404(X1))) ).
cnf(u7991,axiom,
~ predicate(X0,border,sK317,sK401(sK428(X1))) ).
cnf(u7994,axiom,
~ predicate(X0,border,sK250,sK401(sK404(X1))) ).
cnf(u7997,axiom,
~ predicate(X0,border,sK250,sK401(sK428(X1))) ).
cnf(u8159,axiom,
~ object(sK458(sK401(sK404(X0))),landlocked_country,countable,na,eq,n1) ).
cnf(u8162,axiom,
~ object(sK458(sK401(sK428(X0))),landlocked_country,countable,na,eq,n1) ).
cnf(u8209,axiom,
relation(sK168,of,sK174) ).
cnf(u8217,axiom,
relation(sK202,of,sK174) ).
cnf(u8225,axiom,
relation(sK219,of,sK174) ).
cnf(u8232,axiom,
relation(sK458(X1),of,sK174) ).
cnf(u8250,axiom,
predicate(sK402(sK428(X0)),border,sK428(X0),sK401(sK428(X0))) ).
cnf(u8260,axiom,
~ object(sK428(X0),landlocked_country,countable,na,eq,n1) ).
cnf(u8269,axiom,
~ predicate(X0,border,sK401(sK428(X1)),sK250) ).
cnf(u8272,axiom,
relation(sK428(X1),of,sK174) ).
cnf(u8286,axiom,
predicate(sK402(sK404(X0)),border,sK404(X0),sK401(sK404(X0))) ).
cnf(u8296,axiom,
~ object(sK404(X0),landlocked_country,countable,na,eq,n1) ).
cnf(u8305,axiom,
~ predicate(X0,border,sK401(sK404(X1)),sK250) ).
cnf(u8308,axiom,
relation(sK404(X1),of,sK174) ).
cnf(u8918,axiom,
object(sK439(sK426(X0)),landlocked_country,countable,na,eq,n1) ).
cnf(u8921,axiom,
~ predicate(X1,border,sK317,sK458(sK439(sK426(X0)))) ).
cnf(u8933,axiom,
object(sK439(sK430(X0)),landlocked_country,countable,na,eq,n1) ).
cnf(u8936,axiom,
~ predicate(X1,border,sK317,sK458(sK439(sK430(X0)))) ).
cnf(u9179,axiom,
object(X561,gas_giant,countable,na,eq,n1) ).
cnf(u9182,axiom,
object(X561,terrestrial_planet,countable,na,eq,n1) ).
cnf(u9194,axiom,
sK395(X425) = X425 ).
cnf(u9197,axiom,
~ object(X426,island_country,countable,na,eq,n1) ).
cnf(u9271,axiom,
~ predicate(X0,contain,sK141,sK275) ).
cnf(u9283,axiom,
~ predicate(X0,contain,sK147,sK275) ).
cnf(u9295,axiom,
~ predicate(X0,contain,sK152,sK275) ).
cnf(u9307,axiom,
~ predicate(X0,contain,sK159,sK275) ).
cnf(u9319,axiom,
~ predicate(X0,contain,sK172,sK275) ).
cnf(u9331,axiom,
~ predicate(X0,contain,sK176,sK275) ).
cnf(u9343,axiom,
~ predicate(X0,contain,sK193,sK275) ).
cnf(u9355,axiom,
~ predicate(X0,contain,sK238,sK275) ).
cnf(u9367,axiom,
~ predicate(X0,contain,sK240,sK275) ).
cnf(u9379,axiom,
~ predicate(X0,contain,sK250,sK275) ).
cnf(u9391,axiom,
~ predicate(X0,contain,sK260,sK275) ).
cnf(u9403,axiom,
~ predicate(X0,contain,sK262,sK275) ).
cnf(u9415,axiom,
~ predicate(X0,contain,sK287,sK275) ).
cnf(u9427,axiom,
~ predicate(X0,contain,sK289,sK275) ).
cnf(u9439,axiom,
~ predicate(X0,contain,sK293,sK275) ).
cnf(u9451,axiom,
~ predicate(X0,contain,sK305,sK275) ).
cnf(u9463,axiom,
~ predicate(X0,contain,sK310,sK275) ).
cnf(u9475,axiom,
~ predicate(X0,contain,sK313,sK275) ).
cnf(u9487,axiom,
~ predicate(X0,contain,sK315,sK275) ).
cnf(u9499,axiom,
~ predicate(X0,contain,sK317,sK275) ).
cnf(u9511,axiom,
~ predicate(X0,contain,sK367,sK275) ).
cnf(u9523,axiom,
~ predicate(X0,contain,sK380,sK275) ).
cnf(u9535,axiom,
~ predicate(X0,contain,sK368,sK275) ).
cnf(u9547,axiom,
~ predicate(X0,contain,sK369,sK275) ).
cnf(u9559,axiom,
~ predicate(X0,contain,sK370,sK275) ).
cnf(u9575,axiom,
predicate(sK391(sK372),appreciate,sK146,sK372) ).
cnf(u9588,axiom,
predicate(sK391(sK413(X0)),appreciate,sK146,sK413(X0)) ).
cnf(u9605,axiom,
predicate(sK391(sK419(X0)),appreciate,sK146,sK419(X0)) ).
cnf(u9623,axiom,
predicate(sK391(sK440(X0)),appreciate,sK146,sK440(X0)) ).
cnf(u9626,axiom,
~ predicate(X1,contain,sK440(X0),sK275) ).
cnf(u9649,axiom,
predicate(sK391(sK439(sK275)),appreciate,sK146,sK439(sK275)) ).
cnf(u9681,axiom,
~ relation(sK275,of,sK169) ).
cnf(u9685,axiom,
~ relation(sK125,of,sK169) ).
cnf(u9761,axiom,
~ property(sK275,located_in,pos,sK169) ).
cnf(u9768,axiom,
~ relation(sK126,of,sK169) ).
cnf(u9836,axiom,
object(X419,object_c,countable,na,eq,n1) ).
cnf(u9862,axiom,
predicate(sK391(sK404(sK426(X0))),appreciate,sK146,sK404(sK426(X0))) ).
cnf(u9865,axiom,
~ predicate(X1,contain,sK404(sK426(X0)),sK275) ).
cnf(u9877,axiom,
predicate(sK391(sK404(sK430(X0))),appreciate,sK146,sK404(sK430(X0))) ).
cnf(u9880,axiom,
~ predicate(X1,contain,sK404(sK430(X0)),sK275) ).
cnf(u9892,axiom,
predicate(sK391(sK439(sK426(X0))),appreciate,sK146,sK439(sK426(X0))) ).
cnf(u9895,axiom,
~ predicate(X1,contain,sK439(sK426(X0)),sK275) ).
cnf(u9907,axiom,
predicate(sK391(sK439(sK430(X0))),appreciate,sK146,sK439(sK430(X0))) ).
cnf(u9910,axiom,
~ predicate(X1,contain,sK439(sK430(X0)),sK275) ).
cnf(u9922,axiom,
predicate(sK391(sK428(sK426(X0))),appreciate,sK146,sK428(sK426(X0))) ).
cnf(u9925,axiom,
~ predicate(X1,contain,sK428(sK426(X0)),sK275) ).
cnf(u9937,axiom,
predicate(sK391(sK428(sK430(X0))),appreciate,sK146,sK428(sK430(X0))) ).
cnf(u9940,axiom,
~ predicate(X1,contain,sK428(sK430(X0)),sK275) ).
cnf(u10120,axiom,
~ predicate(X1,border,sK141,sK458(X0)) ).
cnf(u10241,axiom,
~ predicate(X1,border,sK147,sK458(X0)) ).
cnf(u10306,axiom,
~ predicate(X1,border,sK159,sK458(X0)) ).
cnf(u10371,axiom,
~ predicate(X1,border,sK172,sK458(X0)) ).
cnf(u11272,axiom,
~ predicate(X1,border,sK260,sK458(X0)) ).
cnf(u11337,axiom,
~ predicate(X1,border,sK262,sK458(X0)) ).
cnf(u12029,axiom,
~ predicate(X1,border,sK305,sK458(X0)) ).
cnf(u12195,axiom,
sK466(X598) = X598 ).
cnf(u12198,axiom,
~ object(X597,language,countable,na,greater,n1) ).
cnf(u12201,axiom,
~ object(X597,national_language,countable,na,eq,n1) ).
cnf(u17008,axiom,
~ predicate(X1,border,sK419(X2),sK458(X0)) ).
cnf(u17264,axiom,
~ predicate(X1,border,sK439(sK426(X2)),sK458(X0)) ).
cnf(u17315,axiom,
~ predicate(X1,border,sK439(sK430(X2)),sK458(X0)) ).
cnf(u8465,axiom,
~ predicate(X0,border,sK159,sK401(sK202)) ).
cnf(u1995,axiom,
predicate(sK443(sK305,sK87),border,sK87,sK305) ).
cnf(u7595,axiom,
predicate(sK443(sK372,sK458(sK372)),border,sK458(sK372),sK372) ).
cnf(u918,axiom,
predicate(sK162,speak,sK161,sK160) ).
cnf(u11069,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u9808,axiom,
sK299 = sK434(sK299) ).
cnf(u8926,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK202)) ).
cnf(u168,axiom,
object(sK325,city,countable,na,eq,n1) ).
cnf(u2863,axiom,
sK370 = sK383(sK370) ).
cnf(u12407,axiom,
~ predicate(X1,border,sK313,sK458(sK428(sK430(X0)))) ).
cnf(u631,axiom,
relation(sK125,of,sK10) ).
cnf(u1161,axiom,
( ~ object(X554,moon,countable,na,eq,n1)
| ~ object(X554,planet,countable,na,eq,n1) ) ).
cnf(u877,axiom,
object(sK355,geneva,named,na,eq,n1) ).
cnf(u1074,axiom,
predicate(sK312,border,sK310,sK238) ).
cnf(u1076,axiom,
sK313 = sK314 ).
cnf(u322,axiom,
object(sK250,part,countable,na,eq,n1) ).
cnf(u2850,axiom,
object(sK368,eU_country,countable,na,eq,n1) ).
cnf(u9397,axiom,
~ relation(sK275,of,sK260) ).
cnf(u9800,axiom,
sK125 = sK434(sK125) ).
cnf(u8518,axiom,
~ predicate(X0,border,sK238,sK401(sK219)) ).
cnf(u9176,axiom,
( ~ object(X561,planet,countable,na,eq,n1)
| object(X561,terrestrial_planet,countable,na,eq,n1)
| object(X561,gas_giant,countable,na,eq,n1) ) ).
cnf(u8455,axiom,
~ predicate(X0,border,sK152,sK401(sK237)) ).
cnf(u947,axiom,
~ predicate(X452,border,sK51,sK238) ).
cnf(u2583,axiom,
( ~ object(X503,country,countable,na,eq,n1)
| property(X503,located_in,pos,sK428(X503)) ) ).
cnf(u8620,axiom,
~ predicate(X0,border,sK305,sK401(sK188)) ).
cnf(u8049,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK219)) ).
cnf(u820,axiom,
object(sK293,russia,named,na,eq,n1) ).
cnf(u552,axiom,
object(sK156,planet,countable,na,eq,n1) ).
cnf(u51,axiom,
object(sK364,planet,countable,na,eq,n1) ).
cnf(u8949,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u1040,axiom,
sK276 = sK282 ).
cnf(u9930,axiom,
~ relation(sK275,of,sK428(sK426(X0))) ).
cnf(u8571,axiom,
~ predicate(X0,border,sK262,sK401(sK230)) ).
cnf(u1391,axiom,
sK174 = sK444(sK174) ).
cnf(u8436,axiom,
~ predicate(X0,border,sK147,sK401(sK168)) ).
cnf(u1322,axiom,
~ object(sK230,island,countable,na,eq,n1) ).
cnf(u32,axiom,
object(sK371,language,countable,na,eq,n1) ).
cnf(u14525,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u14297,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u2222,axiom,
sK367 = sK415(sK174,sK367) ).
cnf(u9483,axiom,
~ property(sK275,located_in,pos,sK313) ).
cnf(u2975,axiom,
( predicate(sK402(sK428(X0)),border,sK428(X0),sK401(sK428(X0)))
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u383,axiom,
( object(sK419(X489),country,countable,na,eq,n1)
| ~ object(X489,subregion,countable,na,eq,n1) ) ).
cnf(u2859,axiom,
sK368 = sK383(sK368) ).
cnf(u8941,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK202)) ).
cnf(u992,axiom,
property(sK233,located_in,pos,sK228) ).
cnf(u1092,axiom,
sK304 = sK331 ).
cnf(u12362,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u13208,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u14341,axiom,
~ predicate(X1,border,sK370,sK458(sK404(sK426(X0)))) ).
cnf(u8583,axiom,
~ predicate(X0,border,sK287,sK401(sK219)) ).
cnf(u1071,axiom,
predicate(sK309,speak,sK305,sK374) ).
cnf(u12366,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u959,axiom,
property(sK198,located_in,pos,sK207) ).
cnf(u9481,axiom,
~ relation(sK275,of,sK313) ).
cnf(u12785,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u1989,axiom,
predicate(sK443(sK250,sK317),border,sK317,sK250) ).
cnf(u11450,axiom,
~ predicate(X1,border,sK287,sK458(sK428(sK426(X0)))) ).
cnf(u1333,axiom,
object(sK176,part,countable,na,eq,n1) ).
cnf(u9693,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK126,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u6931,axiom,
predicate(sK443(sK193,sK458(sK193)),border,sK458(sK193),sK193) ).
cnf(u14518,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u8594,axiom,
~ predicate(X0,border,sK289,sK401(sK188)) ).
cnf(u609,axiom,
( ~ object(X398,capital,countable,na,eq,n1)
| sK387(X398) = X398 ) ).
cnf(u251,axiom,
( ~ predicate(X517,overlap_with,X515,X516)
| sK433(X515) = X515 ) ).
cnf(u8608,axiom,
~ predicate(X0,border,sK293,sK401(sK202)) ).
cnf(u856,axiom,
object(sK262,china,named,na,eq,n1) ).
cnf(u2294,axiom,
relation(sK198,of,sK207) ).
cnf(u598,axiom,
object(sK134,city_state,countable,na,eq,n1) ).
cnf(u1004,axiom,
predicate(sK246,contain,sK240,sK164) ).
cnf(u1291,axiom,
object(sK131,city,countable,na,eq,n1) ).
cnf(u10856,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u10189,axiom,
predicate(sK459(sK428(sK426(X0))),border,sK428(sK426(X0)),sK458(sK428(sK426(X0)))) ).
cnf(u8579,axiom,
~ predicate(X0,border,sK287,sK401(sK168)) ).
cnf(u8506,axiom,
~ predicate(X0,border,sK193,sK401(sK230)) ).
cnf(u823,axiom,
object(sK168,africa,named,na,eq,n1) ).
cnf(u9249,axiom,
( ~ predicate(X1,contain,sK413(X0),sK275)
| predicate(sK391(sK413(X0)),appreciate,sK146,sK413(X0)) ) ).
cnf(u1069,axiom,
predicate(sK308,border,sK305,sK87) ).
cnf(u955,axiom,
property(sK193,located_in,pos,sK230) ).
cnf(u12577,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u7439,axiom,
predicate(sK443(sK458(sK152),sK152),border,sK152,sK458(sK152)) ).
cnf(u8357,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u8129,axiom,
predicate(sK443(sK401(sK202),sK202),border,sK202,sK401(sK202)) ).
cnf(u6149,axiom,
~ relation(sK137,of,sK125) ).
cnf(u8437,axiom,
~ predicate(X0,border,sK147,sK401(sK174)) ).
cnf(u9966,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK289,sK458(X0)) ) ).
cnf(u493,axiom,
object(sK176,country,countable,na,eq,n1) ).
cnf(u1048,axiom,
sK289 = sK290 ).
cnf(u790,axiom,
object(sK126,vienna,named,na,eq,n1) ).
cnf(u1986,axiom,
predicate(sK443(sK250,sK11),border,sK11,sK250) ).
cnf(u13845,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u6265,axiom,
~ relation(sK299,of,sK137) ).
cnf(u9373,axiom,
~ relation(sK275,of,sK240) ).
cnf(u6193,axiom,
~ relation(sK177,of,sK323) ).
cnf(u40,axiom,
object(sK369,baltic_state,countable,na,eq,n1) ).
cnf(u6113,axiom,
~ relation(sK126,of,sK137) ).
cnf(u978,axiom,
property(sK214,located_in,pos,sK193) ).
cnf(u11407,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u8043,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK188)) ).
cnf(u868,axiom,
object(sK323,paris,named,na,eq,n1) ).
cnf(u594,axiom,
object(sK136,city_state,countable,na,eq,n1) ).
cnf(u1000,axiom,
predicate(sK243,border,sK240,sK250) ).
cnf(u7865,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK137,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u25,axiom,
object(sK375,language,countable,na,eq,n1) ).
cnf(u937,axiom,
predicate(sK179,border,sK176,sK293) ).
cnf(u2304,axiom,
relation(sK223,of,sK207) ).
cnf(u2215,axiom,
sK323 = sK415(sK305,sK323) ).
cnf(u9717,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK276,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u1154,axiom,
( predicate(sK417(X483,X482),contain,X482,X483)
| ~ property(X483,located_in,pos,X482) ) ).
cnf(u819,axiom,
object(sK166,pestovo,named,na,eq,n1) ).
cnf(u6371,axiom,
object(sK439(sK426(X0)),country,countable,na,eq,n1) ).
cnf(u8492,axiom,
~ predicate(X0,border,sK176,sK401(sK219)) ).
cnf(u9957,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK172,sK458(X0)) ) ).
cnf(u1296,axiom,
object(sK327,part,countable,na,eq,n1) ).
cnf(u1686,axiom,
sK124 = sK434(sK124) ).
cnf(u1997,axiom,
predicate(sK443(sK317,sK11),border,sK11,sK317) ).
cnf(u6299,axiom,
~ relation(sK323,of,sK125) ).
cnf(u9872,axiom,
~ property(sK275,located_in,pos,sK404(sK426(X0))) ).
cnf(u13214,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u8527,axiom,
~ predicate(X0,border,sK240,sK401(sK168)) ).
cnf(u13846,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u10441,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u288,axiom,
object(sK271,country,countable,na,geq,n6) ).
cnf(u896,axiom,
predicate(sK122,flow_through,sK123,sK240) ).
cnf(u1054,axiom,
predicate(sK295,overlap_with,sK293,sK174) ).
cnf(u2719,axiom,
predicate(sK402(sK237),border,sK237,sK401(sK237)) ).
cnf(u6190,axiom,
~ relation(sK177,of,sK177) ).
cnf(u131,axiom,
object(sK340,city,countable,na,eq,n1) ).
cnf(u7472,axiom,
predicate(sK443(sK458(sK317),sK317),border,sK317,sK458(sK317)) ).
cnf(u1348,axiom,
~ object(sK276,country,countable,na,eq,n1) ).
cnf(u990,axiom,
predicate(sK231,border,sK230,sK237) ).
cnf(u1711,axiom,
sK340 = sK434(sK340) ).
cnf(u8327,axiom,
( ~ object(X2,landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X2,sK458(X0)) ) ).
cnf(u864,axiom,
object(sK310,brazil,named,na,eq,n1) ).
cnf(u9725,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK299,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u3134,axiom,
~ predicate(X0,border,sK250,sK401(sK174)) ).
cnf(u11613,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u1299,axiom,
object(sK313,part,countable,na,eq,n1) ).
cnf(u949,axiom,
( ~ object(X461,entity,countable,na,eq,n1)
| predicate(sK409(X461),dislike,X461,sK169) ) ).
cnf(u2316,axiom,
relation(sK357,of,sK174) ).
cnf(u2211,axiom,
sK250 = sK415(sK174,sK250) ).
cnf(u9638,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK125,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u8048,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK202)) ).
cnf(u394,axiom,
( ~ predicate(X475,contain,X473,X474)
| relation(sK415(X473,X474),of,X473) ) ).
cnf(u831,axiom,
object(sK177,oslo,named,na,eq,n1) ).
cnf(u2287,axiom,
relation(sK171,of,sK289) ).
cnf(u8488,axiom,
~ predicate(X0,border,sK176,sK401(sK168)) ).
cnf(u6076,axiom,
~ relation(sK125,of,sK177) ).
cnf(u9254,axiom,
( ~ predicate(X1,contain,sK428(sK430(X0)),sK275)
| predicate(sK391(sK428(sK430(X0))),appreciate,sK146,sK428(sK430(X0))) ) ).
cnf(u10649,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u1279,axiom,
object(sK350,part,countable,na,eq,n1) ).
cnf(u1994,axiom,
predicate(sK443(sK305,sK152),border,sK152,sK305) ).
cnf(u6345,axiom,
~ relation(sK327,of,sK426(X0)) ).
cnf(u2715,axiom,
predicate(sK402(sK188),border,sK188,sK401(sK188)) ).
cnf(u8478,axiom,
~ predicate(X0,border,sK172,sK401(sK202)) ).
cnf(u8440,axiom,
~ predicate(X0,border,sK147,sK401(sK219)) ).
cnf(u8480,axiom,
~ predicate(X0,border,sK172,sK401(sK230)) ).
cnf(u986,axiom,
object(sK225,province,countable,na,eq,n1) ).
cnf(u9433,axiom,
~ relation(sK275,of,sK289) ).
cnf(u8663,axiom,
~ predicate(X0,border,sK315,sK401(sK237)) ).
cnf(u9218,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK299,of,X0) ) ).
cnf(u876,axiom,
object(sK353,berne,named,na,eq,n1) ).
cnf(u11658,axiom,
~ predicate(X1,border,sK289,sK458(sK428(sK430(X0)))) ).
cnf(u602,axiom,
( ~ object(X410,capital,countable,na,eq,n1)
| sK390(X410) = X410 ) ).
cnf(u14070,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u12618,axiom,
~ predicate(X1,border,sK315,sK458(sK404(sK430(X0)))) ).
cnf(u8425,axiom,
~ predicate(X0,border,sK141,sK401(sK188)) ).
cnf(u8451,axiom,
~ predicate(X0,border,sK152,sK401(sK188)) ).
cnf(u9363,axiom,
~ property(sK275,located_in,pos,sK238) ).
cnf(u1164,axiom,
( ~ property(X572,located_in,pos,X571)
| sK455(X571) = X571 ) ).
cnf(u8553,axiom,
~ predicate(X0,border,sK260,sK401(sK168)) ).
cnf(u827,axiom,
object(sK172,croatia,named,na,eq,n1) ).
cnf(u10855,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u2039,axiom,
predicate(sK443(sK271,sK262),border,sK262,sK271) ).
cnf(u1611,axiom,
sK164 = sK415(sK240,sK164) ).
cnf(u12363,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u1304,axiom,
object(sK137,city,countable,na,eq,n1) ).
cnf(u22,axiom,
( ~ object(X594,multilingual_country,countable,na,eq,n1)
| sK465(X594) = X594 ) ).
cnf(u8057,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK237)) ).
cnf(u365,axiom,
object(sK230,continent,countable,na,eq,n1) ).
cnf(u903,axiom,
sK135 = sK138 ).
cnf(u9553,axiom,
~ relation(sK275,of,sK369) ).
cnf(u296,axiom,
object(sK265,part,countable,na,eq,n1) ).
cnf(u6912,axiom,
predicate(sK443(sK458(sK176),sK176),border,sK176,sK458(sK176)) ).
cnf(u850,axiom,
object(sK237,south_America,named,na,eq,n1) ).
cnf(u1256,axiom,
property(sK250,located_in,pos,sK174) ).
cnf(u12102,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u998,axiom,
sK240 = sK241 ).
cnf(u7872,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK276,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u8606,axiom,
~ predicate(X0,border,sK293,sK401(sK174)) ).
cnf(u1410,axiom,
sK305 = sK444(sK305) ).
cnf(u809,axiom,
object(sK153,sihl,named,na,eq,n1) ).
cnf(u1241,axiom,
relation(sK347,of,sK289) ).
cnf(u957,axiom,
sK168 = sK196 ).
cnf(u1026,axiom,
sK262 = sK268 ).
cnf(u13202,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u14071,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u9349,axiom,
~ relation(sK275,of,sK193) ).
cnf(u6304,axiom,
~ relation(sK323,of,sK299) ).
cnf(u3136,axiom,
~ predicate(X0,border,sK250,sK401(sK202)) ).
cnf(u1988,axiom,
predicate(sK443(sK250,sK152),border,sK152,sK250) ).
cnf(u2200,axiom,
sK204 = sK415(sK193,sK204) ).
cnf(u899,axiom,
sK129 = sK130 ).
cnf(u8429,axiom,
~ predicate(X0,border,sK141,sK401(sK237)) ).
cnf(u9691,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK126,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u11868,axiom,
~ predicate(X1,border,sK293,sK458(sK428(sK426(X0)))) ).
cnf(u222,axiom,
object(sK304,city,countable,na,eq,n1) ).
cnf(u6680,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u6300,axiom,
~ relation(sK323,of,sK126) ).
cnf(u8997,axiom,
~ predicate(X1,border,sK250,sK458(sK404(sK430(X0)))) ).
cnf(u8557,axiom,
~ predicate(X0,border,sK260,sK401(sK219)) ).
cnf(u2185,axiom,
sK137 = sK415(sK152,sK137) ).
cnf(u9469,axiom,
~ relation(sK275,of,sK310) ).
cnf(u862,axiom,
object(sK304,milano,named,na,eq,n1) ).
cnf(u7887,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK327,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u1043,axiom,
sK276 = sK285 ).
cnf(u211,axiom,
object(sK310,country,countable,na,eq,n1) ).
cnf(u2313,axiom,
relation(sK325,of,sK250) ).
cnf(u2979,axiom,
( ~ object(sK428(X0),island,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u3167,axiom,
( ~ object(X416,alpine_country,countable,na,eq,n1)
| object(X416,country,countable,na,eq,n1) ) ).
cnf(u2302,axiom,
relation(sK214,of,sK193) ).
cnf(u821,axiom,
object(sK167,mexico,named,na,eq,n1) ).
cnf(u11869,axiom,
~ predicate(X1,border,sK293,sK458(sK404(sK430(X0)))) ).
cnf(u467,axiom,
object(sK187,star,countable,na,eq,n1) ).
cnf(u1696,axiom,
sK204 = sK434(sK204) ).
cnf(u2047,axiom,
predicate(sK443(sK87,sK305),border,sK305,sK87) ).
cnf(u6232,axiom,
~ relation(sK276,of,sK327) ).
cnf(u3123,axiom,
( ~ predicate(X0,border,sK317,sK401(sK404(X1)))
| ~ object(X1,country,countable,na,eq,n1) ) ).
cnf(u1226,axiom,
relation(sK152,of,sK174) ).
cnf(u1324,axiom,
object(sK207,canadian_province,countable,na,eq,n1) ).
cnf(u2212,axiom,
sK262 = sK415(sK188,sK262) ).
cnf(u373,axiom,
object(sK226,city,countable,na,eq,n1) ).
cnf(u911,axiom,
sK147 = sK148 ).
cnf(u8696,axiom,
~ predicate(X0,border,sK380,sK401(sK168)) ).
cnf(u3252,axiom,
( ~ predicate(X450,border,X447,X448)
| ~ predicate(X449,border,X448,sK250)
| relation(X447,of,sK174) ) ).
cnf(u1697,axiom,
sK211 = sK434(sK211) ).
cnf(u1285,axiom,
object(sK276,part,countable,na,eq,n1) ).
cnf(u8312,axiom,
predicate(sK443(sK401(sK404(X0)),sK404(X0)),border,sK404(X0),sK401(sK404(X0))) ).
cnf(u2197,axiom,
sK198 = sK415(sK207,sK198) ).
cnf(u858,axiom,
object(sK276,beijing,named,na,eq,n1) ).
cnf(u6338,axiom,
~ relation(sK327,of,sK126) ).
cnf(u8051,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK219)) ).
cnf(u571,axiom,
object(sK147,country,countable,na,eq,n1) ).
cnf(u817,axiom,
object(sK372,earth,named,na,eq,n1) ).
cnf(u1249,axiom,
property(sK198,located_in,pos,sK193) ).
cnf(u7745,axiom,
predicate(sK443(sK458(sK413(X0)),sK413(X0)),border,sK413(X0),sK458(sK413(X0))) ).
cnf(u6079,axiom,
~ relation(sK125,of,sK323) ).
cnf(u1036,axiom,
sK262 = sK278 ).
cnf(u8923,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK168)) ).
cnf(u1068,axiom,
predicate(sK307,border,sK305,sK152) ).
cnf(u241,axiom,
object(sK293,country,countable,na,eq,n1) ).
cnf(u1318,axiom,
object(sK238,part,countable,na,eq,n1) ).
cnf(u9981,axiom,
( ~ predicate(X1,border,sK439(sK426(X2)),sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u1718,axiom,
sK361 = sK434(sK361) ).
cnf(u1996,axiom,
predicate(sK443(sK310,sK238),border,sK238,sK310) ).
cnf(u2717,axiom,
predicate(sK402(sK219),border,sK219,sK401(sK219)) ).
cnf(u1149,axiom,
( ~ object(X405,capital,countable,na,eq,n1)
| sK389(X406) = X406
| ~ relation(X405,of,X406) ) ).
cnf(u907,axiom,
predicate(sK143,border,sK141,sK240) ).
cnf(u8580,axiom,
~ predicate(X0,border,sK287,sK401(sK174)) ).
cnf(u1612,axiom,
sK321 = sK415(sK320,sK321) ).
cnf(u1223,axiom,
relation(sK262,of,sK372) ).
cnf(u1128,axiom,
sK357 = sK358 ).
cnf(u870,axiom,
object(sK332,new_York,named,na,eq,n1) ).
cnf(u7269,axiom,
predicate(sK443(sK310,sK458(sK310)),border,sK458(sK310),sK310) ).
cnf(u9983,axiom,
( ~ predicate(X1,border,sK440(X2),sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u8700,axiom,
~ predicate(X0,border,sK380,sK401(sK219)) ).
cnf(u7402,axiom,
predicate(sK443(sK380,sK458(sK380)),border,sK458(sK380),sK380) ).
cnf(u343,axiom,
( ~ object(X506,country,countable,na,eq,n1)
| predicate(sK431(X506),have,X506,sK430(X506)) ) ).
cnf(u6112,axiom,
~ relation(sK126,of,sK126) ).
cnf(u948,axiom,
( ~ object(X459,entity,countable,na,eq,n1)
| ~ predicate(X460,appreciate,X459,sK169) ) ).
cnf(u3056,axiom,
object(sK125,city,countable,na,eq,n1) ).
cnf(u9447,axiom,
~ property(sK275,located_in,pos,sK293) ).
cnf(u8042,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK174)) ).
cnf(u11825,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u643,axiom,
( ~ object(X388,eU_country,countable,na,eq,n1)
| sK384(X388) = X388 ) ).
cnf(u9975,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK369,sK458(X0)) ) ).
cnf(u6191,axiom,
~ relation(sK177,of,sK276) ).
cnf(u8567,axiom,
~ predicate(X0,border,sK262,sK401(sK174)) ).
cnf(u894,axiom,
predicate(sK120,flow_through,sK123,sK128) ).
cnf(u1234,axiom,
relation(sK332,of,sK289) ).
cnf(u10438,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u8645,axiom,
~ predicate(X0,border,sK313,sK401(sK174)) ).
cnf(u12780,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u8301,axiom,
predicate(sK443(sK404(X0),sK401(sK404(X0))),border,sK401(sK404(X0)),sK404(X0)) ).
cnf(u9213,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK125,of,X0) ) ).
cnf(u3121,axiom,
~ predicate(X0,border,sK317,sK401(sK237)) ).
cnf(u11870,axiom,
~ predicate(X1,border,sK293,sK458(sK404(sK426(X0)))) ).
cnf(u8753,axiom,
~ predicate(X0,border,sK372,sK401(sK230)) ).
cnf(u10188,axiom,
predicate(sK459(sK404(sK430(X0))),border,sK404(sK430(X0)),sK458(sK404(sK430(X0)))) ).
cnf(u1705,axiom,
sK319 = sK434(sK319) ).
cnf(u1134,axiom,
predicate(sK365,orbit,sK364,sK187) ).
cnf(u6229,axiom,
~ relation(sK276,of,sK276) ).
cnf(u565,axiom,
object(sK150,planet,countable,na,eq,n1) ).
cnf(u7132,axiom,
predicate(sK443(sK287,sK458(sK287)),border,sK458(sK287),sK287) ).
cnf(u6157,axiom,
~ relation(sK137,of,sK426(X0)) ).
cnf(u6057,axiom,
( ~ relation(sK426(X1),of,X0)
| object(X0,country,countable,na,eq,n1) ) ).
cnf(u10653,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u9543,axiom,
~ property(sK275,located_in,pos,sK368) ).
cnf(u1251,axiom,
property(sK204,located_in,pos,sK193) ).
cnf(u1225,axiom,
relation(sK289,of,sK230) ).
cnf(u944,axiom,
sK176 = sK185 ).
cnf(u901,axiom,
predicate(sK133,orbit,sK132,sK187) ).
cnf(u560,axiom,
object(sK152,alpine_country,countable,na,eq,n1) ).
cnf(u1098,axiom,
sK323 = sK336 ).
cnf(u1326,axiom,
object(sK214,canadian_province,countable,na,eq,n1) ).
cnf(u8466,axiom,
~ predicate(X0,border,sK159,sK401(sK219)) ).
cnf(u2219,axiom,
sK357 = sK415(sK174,sK357) ).
cnf(u1029,axiom,
sK262 = sK273 ).
cnf(u7839,axiom,
predicate(sK443(sK458(sK440(X0)),sK440(X0)),border,sK440(X0),sK458(sK440(X0))) ).
cnf(u8568,axiom,
~ predicate(X0,border,sK262,sK401(sK188)) ).
cnf(u6271,axiom,
~ relation(sK299,of,sK426(X0)) ).
cnf(u6992,axiom,
predicate(sK443(sK240,sK458(sK240)),border,sK458(sK240),sK240) ).
cnf(u14299,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u3137,axiom,
~ predicate(X0,border,sK250,sK401(sK219)) ).
cnf(u433,axiom,
( ~ predicate(X467,govern,X465,X466)
| predicate(sK411(X465,X466),govern,X465,X466) ) ).
cnf(u1231,axiom,
relation(sK327,of,sK240) ).
cnf(u12993,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u10197,axiom,
predicate(sK443(sK404(sK430(X0)),sK458(sK404(sK430(X0)))),border,sK458(sK404(sK430(X0))),sK404(sK430(X0))) ).
cnf(u9961,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK240,sK458(X0)) ) ).
cnf(u561,axiom,
( ~ object(X416,alpine_country,countable,na,eq,n1)
| sK392(X416) = X416 ) ).
cnf(u10439,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u14293,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u1292,axiom,
object(sK332,part,countable,na,eq,n1) ).
cnf(u1690,axiom,
sK131 = sK434(sK131) ).
cnf(u6266,axiom,
~ relation(sK299,of,sK177) ).
cnf(u7568,axiom,
predicate(sK443(sK458(sK370),sK370),border,sK370,sK458(sK370)) ).
cnf(u1121,axiom,
sK350 = sK351 ).
cnf(u808,axiom,
object(sK150,uranus,named,na,eq,n1) ).
cnf(u2118,axiom,
relation(sK321,of,sK320) ).
cnf(u956,axiom,
predicate(sK195,have,sK193,sK194) ).
cnf(u682,axiom,
object(sK84,britney_Spears,named,na,eq,n1) ).
cnf(u11071,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u113,axiom,
object(sK347,city,countable,na,eq,n1) ).
cnf(u11408,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u897,axiom,
sK126 = sK127 ).
cnf(u8531,axiom,
~ predicate(X0,border,sK240,sK401(sK219)) ).
cnf(u7468,axiom,
( object(sK458(X576),sea,countable,na,eq,n1)
| ~ object(X576,country,countable,na,eq,n1)
| object(X576,landlocked_country,countable,na,eq,n1) ) ).
cnf(u1244,axiom,
property(sK172,located_in,pos,sK174) ).
cnf(u9953,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK141,sK458(X0)) ) ).
cnf(u12992,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u1691,axiom,
sK137 = sK434(sK137) ).
cnf(u8452,axiom,
~ predicate(X0,border,sK152,sK401(sK202)) ).
cnf(u11066,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u102,axiom,
( ~ object(X555,planet,countable,na,eq,n1)
| predicate(sK448(X555),orbit,X555,sK447(X555)) ) ).
cnf(u8752,axiom,
~ predicate(X0,border,sK372,sK401(sK219)) ).
cnf(u7722,axiom,
sK413(X0) = sK460(sK413(X0)) ).
cnf(u8000,axiom,
( ~ object(X2,continent,countable,na,eq,n1)
| ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(X2)) ) ).
cnf(u1095,axiom,
sK131 = sK334 ).
cnf(u11867,axiom,
~ predicate(X1,border,sK293,sK458(sK428(sK430(X0)))) ).
cnf(u9633,axiom,
~ property(sK275,located_in,pos,sK440(X0)) ).
cnf(u12782,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u1142,axiom,
( ~ object(X391,capital,countable,na,eq,n1)
| sK385(X391) = X391
| ~ relation(X391,of,X392) ) ).
cnf(u8044,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK188)) ).
cnf(u8956,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u9315,axiom,
~ property(sK275,located_in,pos,sK159) ).
cnf(u573,axiom,
object(sK146,ceramics_collector,countable,na,eq,n1) ).
cnf(u8359,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u930,axiom,
predicate(sK175,border,sK174,sK188) ).
cnf(u8572,axiom,
~ predicate(X0,border,sK262,sK401(sK237)) ).
cnf(u8995,axiom,
~ predicate(X1,border,sK250,sK458(sK428(sK430(X0)))) ).
cnf(u7274,axiom,
predicate(sK443(sK458(sK310),sK310),border,sK310,sK458(sK310)) ).
cnf(u1259,axiom,
property(sK262,larger_than,pos,sK315) ).
cnf(u1046,axiom,
sK287 = sK288 ).
cnf(u200,axiom,
object(sK315,country,countable,na,eq,n1) ).
cnf(u1990,axiom,
predicate(sK443(sK262,sK293),border,sK293,sK262) ).
cnf(u889,axiom,
predicate(sK116,orbit,sK115,sK187) ).
cnf(u12141,axiom,
~ predicate(X1,border,sK310,sK458(sK428(sK430(X0)))) ).
cnf(u909,axiom,
sK144 = sK145 ).
cnf(u8505,axiom,
~ predicate(X0,border,sK193,sK401(sK219)) ).
cnf(u482,axiom,
object(sK182,country,countable,na,exactly,n3) ).
cnf(u6428,axiom,
object(sK439(sK430(X0)),country,countable,na,eq,n1) ).
cnf(u8517,axiom,
~ predicate(X0,border,sK238,sK401(sK202)) ).
cnf(u8467,axiom,
~ predicate(X0,border,sK159,sK401(sK230)) ).
cnf(u8711,axiom,
~ predicate(X0,border,sK368,sK401(sK188)) ).
cnf(u11661,axiom,
~ predicate(X1,border,sK289,sK458(sK404(sK426(X0)))) ).
cnf(u1015,axiom,
( ~ object(X509,sea,countable,na,eq,n1)
| ~ predicate(X510,border,sK250,X509) ) ).
cnf(u9739,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK327,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u14566,axiom,
~ predicate(X1,border,sK372,sK458(sK404(sK430(X0)))) ).
cnf(u2280,axiom,
relation(sK30,of,sK289) ).
cnf(u13241,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u14519,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u979,axiom,
sK214 = sK215 ).
cnf(u2208,axiom,
sK225 = sK415(sK193,sK225) ).
cnf(u8532,axiom,
~ predicate(X0,border,sK240,sK401(sK230)) ).
cnf(u13232,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u11659,axiom,
~ predicate(X1,border,sK289,sK458(sK428(sK426(X0)))) ).
cnf(u2559,axiom,
relation(sK435(X0),of,X0) ).
cnf(u11821,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u8637,axiom,
~ predicate(X0,border,sK310,sK401(sK237)) ).
cnf(u1300,axiom,
object(sK310,part,countable,na,eq,n1) ).
cnf(u942,axiom,
sK177 = sK184 ).
cnf(u8715,axiom,
~ predicate(X0,border,sK368,sK401(sK237)) ).
cnf(u8053,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK230)) ).
cnf(u1123,axiom,
property(sK353,located_in,pos,sK250) ).
cnf(u645,axiom,
( ~ object(X386,eU_country,countable,na,eq,n1)
| sK383(X386) = X386 ) ).
cnf(u816,axiom,
object(sK164,saxony,named,na,eq,n1) ).
cnf(u558,axiom,
object(sK153,river,countable,na,eq,n1) ).
cnf(u64,axiom,
( ~ object(X574,sea,countable,na,eq,n1)
| sK456(X574) = X574 ) ).
cnf(u9731,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK323,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u1982,axiom,
predicate(sK443(sK240,sK250),border,sK250,sK240) ).
cnf(u6150,axiom,
~ relation(sK137,of,sK126) ).
cnf(u10904,axiom,
~ predicate(X1,border,sK238,sK458(sK404(sK426(X0)))) ).
cnf(u8953,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u346,axiom,
( object(sK428(X503),continent,countable,na,eq,n1)
| ~ object(X503,country,countable,na,eq,n1) ) ).
cnf(u8738,axiom,
~ predicate(X0,border,sK370,sK401(sK202)) ).
cnf(u1252,axiom,
property(sK211,located_in,pos,sK193) ).
cnf(u6936,axiom,
predicate(sK443(sK458(sK193),sK193),border,sK193,sK458(sK193)) ).
cnf(u3075,axiom,
( predicate(sK402(sK404(X0)),border,sK404(X0),sK401(sK404(X0)))
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u636,axiom,
object(sK123,river,countable,na,eq,n1) ).
cnf(u2292,axiom,
relation(sK190,of,sK193) ).
cnf(u1103,axiom,
predicate(sK339,speak,sK323,sK374) ).
cnf(u991,axiom,
object(sK233,town,countable,na,eq,n1) ).
cnf(u1237,axiom,
relation(sK340,of,sK287) ).
cnf(u2220,axiom,
sK357 = sK415(sK250,sK357) ).
cnf(u9982,axiom,
( ~ predicate(X1,border,sK439(sK430(X2)),sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u95,axiom,
object(sK349,planet,countable,na,eq,n1) ).
cnf(u8633,axiom,
~ predicate(X0,border,sK310,sK401(sK188)) ).
cnf(u938,axiom,
predicate(sK180,border,sK176,sK51) ).
cnf(u8727,axiom,
~ predicate(X0,border,sK369,sK401(sK230)) ).
cnf(u9385,axiom,
~ relation(sK275,of,sK250) ).
cnf(u2205,axiom,
sK214 = sK415(sK193,sK214) ).
cnf(u9885,axiom,
~ relation(sK275,of,sK404(sK430(X0))) ).
cnf(u828,axiom,
object(sK188,asia,named,na,eq,n1) ).
cnf(u554,axiom,
object(sK155,city,countable,na,eq,n1) ).
cnf(u13287,axiom,
~ predicate(X1,border,sK152,sK458(sK404(sK430(X0)))) ).
cnf(u8050,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK219)) ).
cnf(u358,axiom,
~ predicate(X493,control,sK73,sK421) ).
cnf(u1116,axiom,
sK347 = sK348 ).
cnf(u8750,axiom,
~ predicate(X0,border,sK372,sK401(sK188)) ).
cnf(u13840,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u189,axiom,
( ~ object(X523,city,countable,na,eq,n1)
| sK434(X523) = X523 ) ).
cnf(u8607,axiom,
~ predicate(X0,border,sK293,sK401(sK188)) ).
cnf(u632,axiom,
object(sK125,capital,countable,na,eq,n1) ).
cnf(u8618,axiom,
~ predicate(X0,border,sK305,sK401(sK168)) ).
cnf(u8686,axiom,
~ predicate(X0,border,sK367,sK401(sK202)) ).
cnf(u855,axiom,
object(sK260,nigeria,named,na,eq,n1) ).
cnf(u9505,axiom,
~ relation(sK275,of,sK317) ).
cnf(u987,axiom,
property(sK225,located_in,pos,sK193) ).
cnf(u8660,axiom,
~ predicate(X0,border,sK315,sK401(sK202)) ).
cnf(u6309,axiom,
~ relation(sK323,of,sK430(X0)) ).
cnf(u8709,axiom,
~ predicate(X0,border,sK368,sK401(sK168)) ).
cnf(u2925,axiom,
relation(sK439(X0),of,sK440(X0)) ).
cnf(u10443,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u8276,axiom,
predicate(sK443(sK401(sK428(X0)),sK428(X0)),border,sK428(X0),sK401(sK428(X0))) ).
cnf(u802,axiom,
object(sK139,limmat,named,na,eq,n1) ).
cnf(u12098,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u950,axiom,
object(sK190,city,countable,na,eq,n1) ).
cnf(u6051,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u1222,axiom,
relation(sK260,of,sK168) ).
cnf(u8611,axiom,
~ predicate(X0,border,sK293,sK401(sK237)) ).
cnf(u8998,axiom,
~ predicate(X1,border,sK250,sK458(sK404(sK426(X0)))) ).
cnf(u653,axiom,
object(sK113,jiangXi,named,na,eq,n1) ).
cnf(u6225,axiom,
~ relation(sK276,of,sK125) ).
cnf(u12368,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u12783,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u11452,axiom,
~ predicate(X1,border,sK287,sK458(sK404(sK426(X0)))) ).
cnf(u6684,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u535,axiom,
( ~ object(X429,area,countable,na,eq,n1)
| sK396(X429) = X429 ) ).
cnf(u7875,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK276,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u1693,axiom,
sK163 = sK434(sK163) ).
cnf(u354,axiom,
object(sK237,continent,countable,na,eq,n1) ).
cnf(u900,axiom,
property(sK131,the_capital_of,pos,sK315) ).
cnf(u1688,axiom,
sK128 = sK434(sK128) ).
cnf(u1321,axiom,
~ object(sK237,island,countable,na,eq,n1) ).
cnf(u185,axiom,
( ~ object(X525,city,countable,na,eq,n1)
| predicate(sK436(X525),contain,X525,sK435(X525)) ) ).
cnf(u969,axiom,
object(sK207,province,countable,na,eq,n1) ).
cnf(u516,axiom,
( ~ object(X443,country,countable,na,eq,n1)
| sK403(X443) = X443 ) ).
cnf(u7825,axiom,
( ~ predicate(X0,border,sK458(sK440(X1)),sK250)
| relation(sK440(X1),of,sK174) ) ).
cnf(u851,axiom,
object(sK233,stein_am_Rhein,named,na,eq,n1) ).
cnf(u174,axiom,
( ~ object(X531,city,countable,na,eq,n1)
| predicate(sK442(X531),contain,sK439(X531),X531) ) ).
cnf(u2306,axiom,
relation(sK228,of,sK250) ).
cnf(u10860,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u814,axiom,
object(sK160,english,named,na,eq,n1) ).
cnf(u12827,axiom,
~ predicate(X1,border,sK367,sK458(sK404(sK430(X0)))) ).
cnf(u468,axiom,
( ~ object(X457,star,countable,na,eq,n1)
| sK408(X457) = X457 ) ).
cnf(u1295,axiom,
object(sK327,capital,countable,na,eq,n1) ).
cnf(u8623,axiom,
~ predicate(X0,border,sK305,sK401(sK230)) ).
cnf(u12617,axiom,
~ predicate(X1,border,sK315,sK458(sK428(sK426(X0)))) ).
cnf(u3119,axiom,
~ predicate(X0,border,sK317,sK401(sK219)) ).
cnf(u1057,axiom,
sK137 = sK297 ).
cnf(u8257,axiom,
( ~ object(sK428(X0),landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u8648,axiom,
~ predicate(X0,border,sK313,sK401(sK219)) ).
cnf(u6056,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u2186,axiom,
sK152 = sK415(sK174,sK152) ).
cnf(u9954,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK147,sK458(X0)) ) ).
cnf(u981,axiom,
sK207 = sK218 ).
cnf(u1406,axiom,
sK262 = sK444(sK262) ).
cnf(u2299,axiom,
relation(sK209,of,sK193) ).
cnf(u863,axiom,
object(sK374,french,named,na,eq,n1) ).
cnf(u8008,axiom,
predicate(sK443(sK168,sK401(sK168)),border,sK401(sK168),sK168) ).
cnf(u14115,axiom,
~ predicate(X1,border,sK369,sK458(sK404(sK426(X0)))) ).
cnf(u2318,axiom,
relation(sK361,of,sK238) ).
cnf(u2718,axiom,
predicate(sK402(sK230),border,sK230,sK401(sK230)) ).
cnf(u8038,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK168)) ).
cnf(u7298,axiom,
predicate(sK443(sK313,sK458(sK313)),border,sK458(sK313),sK313) ).
cnf(u810,axiom,
object(sK155,bonn,named,na,eq,n1) ).
cnf(u9257,axiom,
( ~ predicate(X1,contain,sK440(X0),sK275)
| predicate(sK391(sK440(X0)),appreciate,sK146,sK440(X0)) ) ).
cnf(u2209,axiom,
sK228 = sK415(sK250,sK228) ).
cnf(u805,axiom,
object(sK144,greenland,named,na,eq,n1) ).
cnf(u14072,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u3117,axiom,
~ predicate(X0,border,sK317,sK401(sK188)) ).
cnf(u10190,axiom,
predicate(sK459(sK428(sK430(X0))),border,sK428(sK430(X0)),sK458(sK428(sK430(X0)))) ).
cnf(u1985,axiom,
predicate(sK443(sK250,sK240),border,sK240,sK250) ).
cnf(u888,axiom,
object(sK377,mars,named,na,eq,n1) ).
cnf(u2198,axiom,
sK198 = sK415(sK193,sK198) ).
cnf(u908,axiom,
relation(sK144,of,sK141) ).
cnf(u61,axiom,
( ~ object(X576,country,countable,na,eq,n1)
| sK457(X576) = X576
| predicate(sK459(X576),border,X576,sK458(X576)) ) ).
cnf(u1323,axiom,
~ object(sK219,island,countable,na,eq,n1) ).
cnf(u8479,axiom,
~ predicate(X0,border,sK172,sK401(sK219)) ).
cnf(u14523,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u977,axiom,
object(sK214,province,countable,na,eq,n1) ).
cnf(u9840,axiom,
object(X588,entity,countable,na,eq,n1) ).
cnf(u6053,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u8942,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK219)) ).
cnf(u859,axiom,
object(sK280,qingdao,named,na,eq,n1) ).
cnf(u8927,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK219)) ).
cnf(u6678,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u8355,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u1080,axiom,
( ~ object(X521,sea,countable,na,eq,n1)
| ~ predicate(X522,border,sK317,X521) ) ).
cnf(u9301,axiom,
~ relation(sK275,of,sK152) ).
cnf(u822,axiom,
object(sK230,north_America,named,na,eq,n1) ).
cnf(u10213,axiom,
predicate(sK443(sK458(sK404(sK430(X0))),sK404(sK430(X0))),border,sK404(sK430(X0)),sK458(sK404(sK430(X0)))) ).
cnf(u1094,axiom,
sK332 = sK333 ).
cnf(u1303,axiom,
~ object(sK299,country,countable,na,eq,n1) ).
cnf(u525,axiom,
object(sK165,continent,countable,na,exactly,n7) ).
cnf(u6302,axiom,
~ relation(sK323,of,sK177) ).
cnf(u8047,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK202)) ).
cnf(u1010,axiom,
predicate(sK253,border,sK250,sK240) ).
cnf(u6230,axiom,
~ relation(sK276,of,sK299) ).
cnf(u1065,axiom,
predicate(sK303,border,sK152,sK11) ).
cnf(u1977,axiom,
predicate(sK443(sK176,sK51),border,sK51,sK176) ).
cnf(u8439,axiom,
~ predicate(X0,border,sK147,sK401(sK202)) ).
cnf(u8494,axiom,
~ predicate(X0,border,sK176,sK401(sK237)) ).
cnf(u904,axiom,
predicate(sK140,flow_through,sK139,sK325) ).
cnf(u7769,axiom,
sK419(X0) = sK460(sK419(X0)) ).
cnf(u57,axiom,
( ~ object(X580,landlocked_country,countable,na,eq,n1)
| sK460(X580) = X580 ) ).
cnf(u9971,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK315,sK458(X0)) ) ).
cnf(u841,axiom,
object(sK209,british_Columbia,named,na,eq,n1) ).
cnf(u8475,axiom,
~ predicate(X0,border,sK172,sK401(sK168)) ).
cnf(u2119,axiom,
relation(sK164,of,sK240) ).
cnf(u989,axiom,
property(sK228,located_in,pos,sK250) ).
cnf(u9387,axiom,
~ property(sK275,located_in,pos,sK250) ).
cnf(u6347,axiom,
~ relation(sK327,of,sK430(X0)) ).
cnf(u8449,axiom,
~ predicate(X0,border,sK152,sK401(sK168)) ).
cnf(u8954,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u8528,axiom,
~ predicate(X0,border,sK240,sK401(sK174)) ).
cnf(u2029,axiom,
predicate(sK443(sK11,sK250),border,sK250,sK11) ).
cnf(u2852,axiom,
object(sK370,eU_country,countable,na,eq,n1) ).
cnf(u178,axiom,
( ~ object(X528,city,countable,na,eq,n1)
| predicate(sK438(X528),have,X528,sK437(X528)) ) ).
cnf(u8052,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK230)) ).
cnf(u12409,axiom,
~ predicate(X1,border,sK313,sK458(sK404(sK430(X0)))) ).
cnf(u6050,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u10861,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u393,axiom,
( ~ predicate(X475,contain,X473,X474)
| sK415(X473,X474) = X474 ) ).
cnf(u2288,axiom,
relation(sK172,of,sK174) ).
cnf(u3138,axiom,
~ predicate(X0,border,sK250,sK401(sK230)) ).
cnf(u521,axiom,
( object(sK401(X440),sea,countable,na,eq,n1)
| ~ object(X440,continent,countable,na,eq,n1) ) ).
cnf(u1152,axiom,
( ~ object(X439,continent,countable,na,eq,n1)
| ~ object(X439,island,countable,na,eq,n1) ) ).
cnf(u11111,axiom,
~ predicate(X1,border,sK240,sK458(sK428(sK426(X0)))) ).
cnf(u1022,axiom,
predicate(sK263,border,sK262,sK293) ).
cnf(u8520,axiom,
~ predicate(X0,border,sK238,sK401(sK237)) ).
cnf(u291,axiom,
object(sK269,long_history,countable,na,eq,n1) ).
cnf(u8124,axiom,
predicate(sK443(sK401(sK188),sK188),border,sK188,sK401(sK188)) ).
cnf(u8751,axiom,
~ predicate(X0,border,sK372,sK401(sK202)) ).
cnf(u6151,axiom,
~ relation(sK137,of,sK137) ).
cnf(u9723,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK299,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u853,axiom,
object(sK317,liechtenstein,named,na,eq,n1) ).
cnf(u8924,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK174)) ).
cnf(u2171,axiom,
( ~ property(X0,located_in,pos,X1)
| sK415(X1,X0) = X0 ) ).
cnf(u2191,axiom,
sK172 = sK415(sK174,sK172) ).
cnf(u7880,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK299,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u42,axiom,
object(sK368,baltic_state,countable,na,eq,n1) ).
cnf(u9964,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK262,sK458(X0)) ) ).
cnf(u8622,axiom,
~ predicate(X0,border,sK305,sK401(sK219)) ).
cnf(u2300,axiom,
relation(sK211,of,sK209) ).
cnf(u2861,axiom,
sK369 = sK383(sK369) ).
cnf(u13037,axiom,
~ predicate(X1,border,sK380,sK458(sK404(sK426(X0)))) ).
cnf(u27,axiom,
object(sK374,language,countable,na,eq,n1) ).
cnf(u8925,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK188)) ).
cnf(u175,axiom,
( predicate(sK441(X531),contain,sK440(X531),sK439(X531))
| ~ object(X531,city,countable,na,eq,n1) ) ).
cnf(u8585,axiom,
~ predicate(X0,border,sK287,sK401(sK237)) ).
cnf(u306,axiom,
object(sK260,country,countable,na,eq,n1) ).
cnf(u1018,axiom,
sK250 = sK259 ).
cnf(u1067,axiom,
sK305 = sK306 ).
cnf(u9493,axiom,
~ relation(sK275,of,sK315) ).
cnf(u634,axiom,
object(sK124,city,countable,na,eq,n1) ).
cnf(u8083,axiom,
predicate(sK443(sK230,sK401(sK230)),border,sK401(sK230),sK230) ).
cnf(u9214,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK126,of,X0) ) ).
cnf(u849,axiom,
object(sK229,winterthur,named,na,eq,n1) ).
cnf(u491,axiom,
object(sK177,capital,countable,na,eq,n1) ).
cnf(u3110,axiom,
( ~ object(X0,continent,countable,na,eq,n1)
| ~ predicate(X1,border,sK317,sK401(X0)) ) ).
cnf(u6111,axiom,
~ relation(sK126,of,sK125) ).
cnf(u10647,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u8033,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK230)) ) ).
cnf(u1336,axiom,
object(sK169,person,countable,na,eq,n1) ).
cnf(u584,axiom,
object(sK141,country,countable,na,eq,n1) ).
cnf(u1350,axiom,
~ object(sK327,country,countable,na,eq,n1) ).
cnf(u6682,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u9216,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK177,of,X0) ) ).
cnf(u8401,axiom,
~ predicate(X1,border,sK317,sK458(sK404(sK426(X0)))) ).
cnf(u1309,axiom,
object(sK276,area,countable,na,eq,n1) ).
cnf(u9375,axiom,
~ property(sK275,located_in,pos,sK240) ).
cnf(u7172,axiom,
predicate(sK443(sK289,sK458(sK289)),border,sK458(sK289),sK289) ).
cnf(u882,axiom,
object(sK368,estonia,named,na,eq,n1) ).
cnf(u1160,axiom,
( ~ object(X552,dwarf_planet,countable,na,eq,n1)
| ~ object(X552,planet,countable,na,eq,n1) ) ).
cnf(u9715,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK276,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u902,axiom,
relation(sK137,of,sK152) ).
cnf(u11822,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u13246,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u9279,axiom,
~ property(sK275,located_in,pos,sK141) ).
cnf(u10646,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u11404,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u14294,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u861,axiom,
object(sK299,foo,named,na,eq,n1) ).
cnf(u503,axiom,
object(sK172,country,countable,na,eq,n1) ).
cnf(u12365,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u980,axiom,
sK209 = sK216 ).
cnf(u8683,axiom,
~ predicate(X0,border,sK367,sK401(sK168)) ).
cnf(u596,axiom,
object(sK135,city_state,countable,na,eq,n1) ).
cnf(u2202,axiom,
sK209 = sK415(sK193,sK209) ).
cnf(u3225,axiom,
object(sK368,country,countable,na,eq,n1) ).
cnf(u8046,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK202)) ).
cnf(u6367,axiom,
object(sK404(sK426(X0)),country,countable,na,eq,n1) ).
cnf(u3135,axiom,
~ predicate(X0,border,sK250,sK401(sK188)) ).
cnf(u35,axiom,
( ~ object(X590,baltic_state,countable,na,eq,n1)
| sK463(X590) = X590 ) ).
cnf(u11068,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u2314,axiom,
relation(sK353,of,sK250) ).
cnf(u2217,axiom,
sK353 = sK415(sK250,sK353) ).
cnf(u1024,axiom,
relation(sK265,of,sK262) ).
cnf(u7025,axiom,
predicate(sK443(sK250,sK458(sK250)),border,sK458(sK250),sK250) ).
cnf(u1166,axiom,
( ~ object(X598,country,countable,na,eq,n1)
| ~ object(X597,language,countable,na,greater,n1)
| ~ object(X597,national_language,countable,na,eq,n1)
| sK466(X598) = X598
| ~ relation(X597,of,X598) ) ).
cnf(u804,axiom,
object(sK141,denmark,named,na,eq,n1) ).
cnf(u14066,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u8502,axiom,
~ predicate(X0,border,sK193,sK401(sK174)) ).
cnf(u13242,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u1306,axiom,
object(sK287,part,countable,na,eq,n1) ).
cnf(u16,axiom,
object(sK377,planet,countable,na,eq,n1) ).
cnf(u8582,axiom,
~ predicate(X0,border,sK287,sK401(sK202)) ).
cnf(u1984,axiom,
predicate(sK443(sK250,sK251),border,sK251,sK250) ).
cnf(u164,axiom,
object(sK327,city,countable,na,eq,n1) ).
cnf(u2851,axiom,
object(sK369,eU_country,countable,na,eq,n1) ).
cnf(u2206,axiom,
sK221 = sK415(sK217,sK221) ).
cnf(u11619,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u367,axiom,
object(sK229,city,countable,na,eq,n1) ).
cnf(u12573,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u499,axiom,
object(sK174,continent,countable,na,eq,n1) ).
cnf(u6119,axiom,
~ relation(sK126,of,sK426(X0)) ).
cnf(u446,axiom,
( ~ object(X463,capital,countable,na,eq,n1)
| sK410(X463) = X463 ) ).
cnf(u976,axiom,
sK211 = sK212 ).
cnf(u6264,axiom,
~ relation(sK299,of,sK126) ).
cnf(u592,axiom,
object(sK137,capital,countable,na,eq,n1) ).
cnf(u1258,axiom,
property(sK262,located_in,pos,sK188) ).
cnf(u1055,axiom,
sK137 = sK296 ).
cnf(u1413,axiom,
sK317 = sK444(sK317) ).
cnf(u250,axiom,
object(sK289,country,countable,na,eq,n1) ).
cnf(u2398,axiom,
( ~ object(X443,country,countable,na,eq,n1)
| relation(X443,of,sK404(X443)) ) ).
cnf(u14114,axiom,
~ predicate(X1,border,sK369,sK458(sK404(sK430(X0)))) ).
cnf(u1317,axiom,
object(sK240,part,countable,na,eq,n1) ).
cnf(u465,axiom,
object(sK188,continent,countable,na,eq,n1) ).
cnf(u8713,axiom,
~ predicate(X0,border,sK368,sK401(sK219)) ).
cnf(u890,axiom,
( ~ object(X386,eU_country,countable,na,eq,n1)
| relation(sK383(X386),of,sK174) ) ).
cnf(u8055,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK237)) ).
cnf(u14524,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u6370,axiom,
object(sK428(sK426(X0)),country,countable,na,eq,n1) ).
cnf(u1976,axiom,
predicate(sK443(sK176,sK293),border,sK293,sK176) ).
cnf(u8728,axiom,
~ predicate(X0,border,sK369,sK401(sK237)) ).
cnf(u9567,axiom,
~ property(sK275,located_in,pos,sK370) ).
cnf(u7407,axiom,
predicate(sK443(sK458(sK380),sK380),border,sK380,sK458(sK380)) ).
cnf(u840,axiom,
object(sK204,toronto,named,na,eq,n1) ).
cnf(u2278,axiom,
( ~ property(X0,located_in,pos,X1)
| relation(X0,of,X1) ) ).
cnf(u988,axiom,
object(sK228,canton,countable,na,eq,n1) ).
cnf(u714,axiom,
object(sK52,finland,named,na,eq,n1) ).
cnf(u13,axiom,
object(sK379,person,countable,na,eq,n1) ).
cnf(u10437,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u9829,axiom,
sK426(X0) = sK434(sK426(X0)) ).
cnf(u1993,axiom,
predicate(sK443(sK152,sK11),border,sK11,sK152) ).
cnf(u8490,axiom,
~ predicate(X0,border,sK176,sK401(sK188)) ).
cnf(u12361,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u807,axiom,
object(sK305,france,named,na,eq,n1) ).
cnf(u1053,axiom,
predicate(sK294,overlap_with,sK293,sK188) ).
cnf(u939,axiom,
predicate(sK181,border,sK176,sK52) ).
cnf(u6052,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u9204,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ predicate(X1,contain,X0,sK275) ) ).
cnf(u1707,axiom,
sK323 = sK434(sK323) ).
cnf(u1979,axiom,
predicate(sK443(sK176,sK182),border,sK182,sK176) ).
cnf(u7870,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK177,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u1032,axiom,
property(sK276,located_in,pos,sK262) ).
cnf(u11660,axiom,
~ predicate(X1,border,sK289,sK458(sK404(sK430(X0)))) ).
cnf(u8442,axiom,
~ predicate(X0,border,sK147,sK401(sK237)) ).
cnf(u8657,axiom,
~ predicate(X0,border,sK315,sK401(sK168)) ).
cnf(u1714,axiom,
sK350 = sK434(sK350) ).
cnf(u1992,axiom,
predicate(sK443(sK152,sK250),border,sK250,sK152) ).
cnf(u1145,axiom,
( ~ object(X395,capital,countable,na,eq,n1)
| sK386(X395,X396) = X395
| ~ relation(X395,of,X396) ) ).
cnf(u6685,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u8570,axiom,
~ predicate(X0,border,sK262,sK401(sK219)) ).
cnf(u8427,axiom,
~ predicate(X0,border,sK141,sK401(sK219)) ).
cnf(u852,axiom,
object(sK380,poland,named,na,eq,n1) ).
cnf(u578,axiom,
object(sK144,part,countable,na,eq,n1) ).
cnf(u984,axiom,
object(sK223,city,countable,na,eq,n1) ).
cnf(u12828,axiom,
~ predicate(X1,border,sK367,sK458(sK404(sK426(X0)))) ).
cnf(u921,axiom,
( object(sK399(X435),country,countable,na,geq,n2)
| ~ object(X435,continent,countable,na,eq,n1)
| sK219 = X435 ) ).
cnf(u8555,axiom,
~ predicate(X0,border,sK260,sK401(sK188)) ).
cnf(u2199,axiom,
sK204 = sK415(sK207,sK204) ).
cnf(u8741,axiom,
~ predicate(X0,border,sK370,sK401(sK237)) ).
cnf(u7499,axiom,
predicate(sK443(sK368,sK458(sK368)),border,sK458(sK368),sK368) ).
cnf(u1266,axiom,
property(sK355,located_in,pos,sK250) ).
cnf(u803,axiom,
object(sK325,zurich,named,na,eq,n1) ).
cnf(u1715,axiom,
sK353 = sK434(sK353) ).
cnf(u8476,axiom,
~ predicate(X0,border,sK172,sK401(sK174)) ).
cnf(u1280,axiom,
object(sK347,part,countable,na,eq,n1) ).
cnf(u3064,axiom,
object(sK426(X0),city,countable,na,eq,n1) ).
cnf(u1257,axiom,
property(sK262,larger_than,pos,sK289) ).
cnf(u272,axiom,
object(sK280,city,countable,na,eq,n1) ).
cnf(u1038,axiom,
sK262 = sK279 ).
cnf(u9217,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK276,of,X0) ) ).
cnf(u8326,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK250,sK458(X0)) ) ).
cnf(u601,axiom,
object(sK132,planet,countable,na,eq,n1) ).
cnf(u6189,axiom,
~ relation(sK177,of,sK137) ).
cnf(u8428,axiom,
~ predicate(X0,border,sK141,sK401(sK230)) ).
cnf(u9970,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK313,sK458(X0)) ) ).
cnf(u974,axiom,
property(sK211,located_in,pos,sK209) ).
cnf(u2210,axiom,
sK233 = sK415(sK228,sK233) ).
cnf(u1695,axiom,
sK198 = sK434(sK198) ).
cnf(u318,axiom,
object(sK251,country,countable,na,exactly,n5) ).
cnf(u848,axiom,
object(sK228,schaffhausen,named,na,eq,n1) ).
cnf(u9709,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK177,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u8944,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK237)) ).
cnf(u3118,axiom,
~ predicate(X0,border,sK317,sK401(sK202)) ).
cnf(u14567,axiom,
~ predicate(X1,border,sK372,sK458(sK404(sK426(X0)))) ).
cnf(u9915,axiom,
~ relation(sK275,of,sK439(sK430(X0))) ).
cnf(u687,axiom,
object(sK79,olympic_Games_2008,named,na,eq,n1) ).
cnf(u9337,axiom,
~ relation(sK275,of,sK176) ).
cnf(u933,axiom,
( ~ predicate(X450,border,X447,X448)
| ~ predicate(X449,border,X448,sK250)
| sK405(X447) = X447 ) ).
cnf(u2195,axiom,
sK190 = sK415(sK193,sK190) ).
cnf(u1130,axiom,
sK357 = sK359 ).
cnf(u8041,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK174)) ).
cnf(u8737,axiom,
~ predicate(X0,border,sK370,sK401(sK188)) ).
cnf(u815,axiom,
object(sK163,dresden,named,na,eq,n1) ).
cnf(u1345,axiom,
object(sK129,part,countable,na,eq,n1) ).
cnf(u1061,axiom,
sK152 = sK300 ).
cnf(u1973,axiom,
predicate(sK443(sK141,sK240),border,sK240,sK141) ).
cnf(u6337,axiom,
~ relation(sK327,of,sK125) ).
cnf(u1263,axiom,
property(sK152,located_in,pos,sK174) ).
cnf(u12825,axiom,
~ predicate(X1,border,sK367,sK458(sK428(sK430(X0)))) ).
cnf(u12576,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u2699,axiom,
( ~ object(X469,province,countable,na,eq,n1)
| property(X469,located_in,pos,sK413(X469)) ) ).
cnf(u107,axiom,
( ~ object(X547,planet,countable,na,eq,n1)
| sK446(X547) = X547 ) ).
cnf(u8533,axiom,
~ predicate(X0,border,sK240,sK401(sK237)) ).
cnf(u8424,axiom,
~ predicate(X0,border,sK141,sK401(sK174)) ).
cnf(u8739,axiom,
~ predicate(X0,border,sK370,sK401(sK219)) ).
cnf(u7600,axiom,
predicate(sK443(sK458(sK372),sK372),border,sK372,sK458(sK372)) ).
cnf(u970,axiom,
property(sK207,located_in,pos,sK193) ).
cnf(u1025,axiom,
predicate(sK267,overlap_with,sK266,sK262) ).
cnf(u11410,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u1147,axiom,
( ~ object(X401,capital,countable,na,eq,n1)
| sK388(X401) = X401
| ~ relation(X401,of,X402) ) ).
cnf(u7828,axiom,
predicate(sK443(sK440(X0),sK458(sK440(X0))),border,sK458(sK440(X0)),sK440(X0)) ).
cnf(u2150,axiom,
( ~ object(X433,continent,countable,na,eq,n1)
| relation(X433,of,sK372) ) ).
cnf(u860,axiom,
object(sK287,australia,named,na,eq,n1) ).
cnf(u6227,axiom,
~ relation(sK276,of,sK137) ).
cnf(u14069,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u9652,axiom,
( ~ object(X419,person,countable,na,eq,n1)
| object(X419,object_c,countable,na,eq,n1) ) ).
cnf(u17,axiom,
( ~ predicate(X602,appreciate,X601,X600)
| predicate(sK468(X600),control,X600,sK467(X600)) ) ).
cnf(u9963,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK260,sK458(X0)) ) ).
cnf(u6155,axiom,
~ relation(sK137,of,sK323) ).
cnf(u929,axiom,
sK172 = sK173 ).
cnf(u6303,axiom,
~ relation(sK323,of,sK276) ).
cnf(u1900,axiom,
sK276 = sK396(sK276) ).
cnf(u390,axiom,
( ~ predicate(X487,locate,X485,X486)
| predicate(sK418(X485,X486),contain,X485,X486) ) ).
cnf(u6231,axiom,
~ relation(sK276,of,sK323) ).
cnf(u811,axiom,
object(sK156,neptune,named,na,eq,n1) ).
cnf(u2023,axiom,
predicate(sK443(sK147,sK240),border,sK240,sK147) ).
cnf(u1288,axiom,
object(sK323,capital,countable,na,eq,n1) ).
cnf(u8032,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK219)) ) ).
cnf(u8698,axiom,
~ predicate(X0,border,sK380,sK401(sK188)) ).
cnf(u1127,axiom,
property(sK357,located_in,pos,sK174) ).
cnf(u11823,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u349,axiom,
( ~ object(X497,country,countable,na,eq,n1)
| predicate(sK425(X497),have,X497,sK424(X497)) ) ).
cnf(u7742,axiom,
( ~ predicate(X0,border,sK413(X1),sK250)
| relation(sK458(sK413(X1)),of,sK174) ) ).
cnf(u1261,axiom,
property(sK137,located_in,pos,sK152) ).
cnf(u8454,axiom,
~ predicate(X0,border,sK152,sK401(sK230)) ).
cnf(u6344,axiom,
~ relation(sK327,of,sK327) ).
cnf(u7033,axiom,
predicate(sK443(sK458(sK250),sK250),border,sK250,sK458(sK250)) ).
cnf(u10862,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u1389,axiom,
sK141 = sK444(sK141) ).
cnf(u8529,axiom,
~ predicate(X0,border,sK240,sK401(sK188)) ).
cnf(u14068,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u1298,axiom,
object(sK315,part,countable,na,eq,n1) ).
cnf(u834,axiom,
object(sK225,quebec,named,na,eq,n1) ).
cnf(u1240,axiom,
relation(sK345,of,sK313) ).
cnf(u7178,axiom,
predicate(sK443(sK458(sK289),sK289),border,sK289,sK458(sK289)) ).
cnf(u8662,axiom,
~ predicate(X0,border,sK315,sK401(sK230)) ).
cnf(u6083,axiom,
~ relation(sK125,of,sK430(X0)) ).
cnf(u1703,axiom,
sK280 = sK434(sK280) ).
cnf(u3079,axiom,
( ~ object(sK404(X0),island,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u9701,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK137,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u9459,axiom,
~ property(sK275,located_in,pos,sK305) ).
cnf(u793,axiom,
object(sK240,germany,named,na,eq,n1) ).
cnf(u1138,axiom,
predicate(sK378,orbit,sK377,sK187) ).
cnf(u9327,axiom,
~ property(sK275,located_in,pos,sK172) ).
cnf(u9215,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK137,of,X0) ) ).
cnf(u9565,axiom,
~ relation(sK275,of,sK370) ).
cnf(u1981,axiom,
predicate(sK443(sK240,sK380),border,sK380,sK240) ).
cnf(u3059,axiom,
object(sK177,city,countable,na,eq,n1) ).
cnf(u572,axiom,
( ~ object(X413,ceramic,countable,na,eq,n1)
| ~ object(X412,country,countable,na,eq,n1)
| predicate(sK391(X412),appreciate,sK146,X412)
| ~ predicate(X414,contain,X412,X413) ) ).
cnf(u8394,axiom,
( ~ predicate(X1,border,sK317,sK458(sK439(sK426(X0))))
| object(sK439(sK426(X0)),landlocked_country,countable,na,eq,n1) ) ).
cnf(u806,axiom,
object(sK147,belgium,named,na,eq,n1) ).
cnf(u2184,axiom,
sK84 = sK415(sK289,sK84) ).
cnf(u1011,axiom,
predicate(sK254,border,sK250,sK11) ).
cnf(u8684,axiom,
~ predicate(X0,border,sK367,sK401(sK174)) ).
cnf(u9956,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK159,sK458(X0)) ) ).
cnf(u1716,axiom,
sK355 = sK434(sK355) ).
cnf(u1044,axiom,
sK276 = sK286 ).
cnf(u2297,axiom,
relation(sK204,of,sK193) ).
cnf(u8029,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK174)) ) ).
cnf(u1332,axiom,
~ object(sK187,planet,countable,na,eq,n1) ).
cnf(u846,axiom,
object(sK223,guelph,named,na,eq,n1) ).
cnf(u1246,axiom,
property(sK176,located_in,pos,sK174) ).
cnf(u8635,axiom,
~ predicate(X0,border,sK310,sK401(sK219)) ).
cnf(u6566,axiom,
( ~ object(X576,country,countable,na,eq,n1)
| object(X576,landlocked_country,countable,na,eq,n1)
| predicate(sK459(X576),border,X576,sK458(X576)) ) ).
cnf(u1027,axiom,
predicate(sK272,border,sK262,sK271) ).
cnf(u8658,axiom,
~ predicate(X0,border,sK315,sK401(sK174)) ).
cnf(u2688,axiom,
( ~ predicate(X475,contain,X473,X474)
| object(X474,part,countable,na,eq,n1) ) ).
cnf(u96,axiom,
( ~ object(X561,planet,countable,na,eq,n1)
| sK452(X561) = X561
| sK451(X561) = X561 ) ).
cnf(u12994,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u2286,axiom,
relation(sK167,of,sK230) ).
cnf(u14073,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u1717,axiom,
sK357 = sK434(sK357) ).
cnf(u451,axiom,
object(sK194,official_language,countable,na,exactly,n2) ).
cnf(u1156,axiom,
~ object(sK305,planet,countable,na,eq,n1) ).
cnf(u2143,axiom,
( ~ predicate(X423,live,X421,X422)
| property(X421,located_in,pos,X422) ) ).
cnf(u6968,axiom,
predicate(sK443(sK458(sK238),sK238),border,sK238,sK458(sK238)) ).
cnf(u2031,axiom,
predicate(sK443(sK305,sK250),border,sK250,sK305) ).
cnf(u540,axiom,
object(sK161,person,countable,na,geq,n100) ).
cnf(u12779,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u8647,axiom,
~ predicate(X0,border,sK313,sK401(sK202)) ).
cnf(u2196,axiom,
sK193 = sK415(sK230,sK193) ).
cnf(u1135,axiom,
object(sK367,country,countable,na,eq,n1) ).
cnf(u1023,axiom,
predicate(sK264,manage,sK262,sK79) ).
cnf(u1978,axiom,
predicate(sK443(sK176,sK52),border,sK52,sK176) ).
cnf(u1397,axiom,
sK240 = sK444(sK240) ).
cnf(u11065,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u842,axiom,
object(sK211,vancouver,named,na,eq,n1) ).
cnf(u12784,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u8938,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK168)) ).
cnf(u8450,axiom,
~ predicate(X0,border,sK152,sK401(sK174)) ).
cnf(u801,axiom,
object(sK152,italy,named,na,eq,n1) ).
cnf(u1233,axiom,
relation(sK304,of,sK152) ).
cnf(u9219,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK323,of,X0) ) ).
cnf(u6054,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u11067,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u8644,axiom,
~ predicate(X0,border,sK313,sK401(sK168)) ).
cnf(u6681,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u8584,axiom,
~ predicate(X0,border,sK287,sK401(sK230)) ).
cnf(u1302,axiom,
object(sK152,part,countable,na,eq,n1) ).
cnf(u6156,axiom,
~ relation(sK137,of,sK327) ).
cnf(u1702,axiom,
sK276 = sK434(sK276) ).
cnf(u887,axiom,
object(sK376,lushan,named,na,eq,n1) ).
cnf(u1133,axiom,
predicate(sK363,orbit,sK362,sK187) ).
cnf(u14565,axiom,
~ predicate(X1,border,sK372,sK458(sK428(sK426(X0)))) ).
cnf(u9519,axiom,
~ property(sK275,located_in,pos,sK367) ).
cnf(u6679,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u6269,axiom,
~ relation(sK299,of,sK323) ).
cnf(u7531,axiom,
predicate(sK443(sK369,sK458(sK369)),border,sK458(sK369),sK369) ).
cnf(u6273,axiom,
~ relation(sK299,of,sK430(X0)) ).
cnf(u1112,axiom,
sK276 = sK344 ).
cnf(u854,axiom,
object(sK379,dalai_Lama,named,na,eq,n1) ).
cnf(u9967,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK293,sK458(X0)) ) ).
cnf(u9965,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK287,sK458(X0)) ) ).
cnf(u5933,axiom,
relation(sK399(X0),of,X0) ).
cnf(u10651,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u8462,axiom,
~ predicate(X0,border,sK159,sK401(sK168)) ).
cnf(u9220,axiom,
( ~ predicate(X1,contain,X0,sK275)
| predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK327,of,X0) ) ).
cnf(u11826,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u6716,axiom,
( predicate(sK459(sK419(X0)),border,sK419(X0),sK458(sK419(X0)))
| object(sK419(X0),landlocked_country,countable,na,eq,n1) ) ).
cnf(u12619,axiom,
~ predicate(X1,border,sK315,sK458(sK404(sK426(X0)))) ).
cnf(u1097,axiom,
sK131 = sK335 ).
cnf(u813,axiom,
object(sK159,new_Zealand,named,na,eq,n1) ).
cnf(u2009,axiom,
predicate(sK443(sK293,sK176),border,sK176,sK293) ).
cnf(u258,axiom,
object(sK287,country,countable,na,eq,n1) ).
cnf(u8035,axiom,
( ~ predicate(X1,border,X0,sK401(sK404(X2)))
| ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X2,country,countable,na,eq,n1) ) ).
cnf(u755,axiom,
object(sK11,austria,named,na,eq,n1) ).
cnf(u1001,axiom,
predicate(sK244,border,sK240,sK147) ).
cnf(u548,axiom,
( ~ object(X419,person,countable,na,eq,n1)
| sK393(X419) = X419 ) ).
cnf(u13243,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u1218,axiom,
relation(sK147,of,sK174) ).
cnf(u883,axiom,
object(sK369,latvia,named,na,eq,n1) ).
cnf(u8556,axiom,
~ predicate(X0,border,sK260,sK401(sK202)) ).
cnf(u906,axiom,
sK141 = sK142 ).
cnf(u1689,axiom,
sK129 = sK434(sK129) ).
cnf(u6027,axiom,
( predicate(sK416(X478,X479),contain,X479,X478)
| ~ relation(X478,of,X479) ) ).
cnf(u2707,axiom,
relation(X0,of,sK413(X0)) ).
cnf(u9325,axiom,
~ relation(sK275,of,sK172) ).
cnf(u352,axiom,
( object(sK422(X494),city,countable,na,geq,n1)
| ~ object(X494,country,countable,na,eq,n1) ) ).
cnf(u1118,axiom,
( ~ object(X558,planet,countable,na,eq,n1)
| sK449(X558) = X558
| predicate(sK450(X558),orbit,X558,sK187) ) ).
cnf(u8507,axiom,
~ predicate(X0,border,sK193,sK401(sK237)) ).
cnf(u1327,axiom,
~ object(sK202,island,countable,na,eq,n1) ).
cnf(u6152,axiom,
~ relation(sK137,of,sK177) ).
cnf(u12991,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u3226,axiom,
object(sK369,country,countable,na,eq,n1) ).
cnf(u7536,axiom,
predicate(sK443(sK458(sK369),sK369),border,sK369,sK458(sK369)) ).
cnf(u13226,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u1412,axiom,
sK310 = sK444(sK310) ).
cnf(u8955,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u13288,axiom,
~ predicate(X1,border,sK152,sK458(sK404(sK426(X0)))) ).
cnf(u14521,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u8748,axiom,
~ predicate(X0,border,sK372,sK401(sK168)) ).
cnf(u1235,axiom,
relation(sK131,of,sK315) ).
cnf(u2218,axiom,
sK355 = sK415(sK250,sK355) ).
cnf(u3052,axiom,
( ~ object(X463,capital,countable,na,eq,n1)
| object(X463,city,countable,na,eq,n1) ) ).
cnf(u9289,axiom,
~ relation(sK275,of,sK147) ).
cnf(u1013,axiom,
predicate(sK256,border,sK250,sK152) ).
cnf(u8519,axiom,
~ predicate(X0,border,sK238,sK401(sK230)) ).
cnf(u544,axiom,
object(sK159,country,countable,na,eq,n1) ).
cnf(u9917,axiom,
~ property(sK275,located_in,pos,sK439(sK430(X0))) ).
cnf(u1710,axiom,
sK332 = sK434(sK332) ).
cnf(u9887,axiom,
~ property(sK275,located_in,pos,sK404(sK430(X0))) ).
cnf(u2203,axiom,
sK211 = sK415(sK209,sK211) ).
cnf(u895,axiom,
predicate(sK121,flow_through,sK123,sK129) ).
cnf(u622,axiom,
object(sK129,city,countable,na,eq,n1) ).
cnf(u8040,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK174)) ).
cnf(u8740,axiom,
~ predicate(X0,border,sK370,sK401(sK230)) ).
cnf(u9435,axiom,
~ property(sK275,located_in,pos,sK289) ).
cnf(u8395,axiom,
( ~ predicate(X1,border,sK317,sK458(sK439(sK430(X0))))
| object(sK439(sK430(X0)),landlocked_country,countable,na,eq,n1) ) ).
cnf(u545,axiom,
( ~ predicate(X423,live,X421,X422)
| sK394(X421,X422) = X421 ) ).
cnf(u10858,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u2017,axiom,
predicate(sK443(sK237,sK230),border,sK230,sK237) ).
cnf(u6424,axiom,
object(sK404(sK430(X0)),country,countable,na,eq,n1) ).
cnf(u792,axiom,
object(sK129,ulm,named,na,eq,n1) ).
cnf(u534,axiom,
object(sK163,city,countable,na,eq,n1) ).
cnf(u940,axiom,
predicate(sK183,border,sK176,sK182) ).
cnf(u1009,axiom,
predicate(sK252,border,sK250,sK251) ).
cnf(u8515,axiom,
~ predicate(X0,border,sK238,sK401(sK174)) ).
cnf(u1980,axiom,
predicate(sK443(sK230,sK237),border,sK237,sK230) ).
cnf(u7954,axiom,
( ~ predicate(X1,border,sK419(X0),sK401(X2))
| ~ object(X2,continent,countable,na,eq,n1) ) ).
cnf(u1228,axiom,
relation(sK310,of,sK237) ).
cnf(u891,axiom,
predicate(sK117,flow_through,sK123,sK124) ).
cnf(u8293,axiom,
( ~ object(sK404(X0),landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u9555,axiom,
~ property(sK275,located_in,pos,sK369) ).
cnf(u2872,axiom,
relation(sK369,of,sK174) ).
cnf(u8736,axiom,
~ predicate(X0,border,sK370,sK401(sK174)) ).
cnf(u9902,axiom,
~ property(sK275,located_in,pos,sK439(sK426(X0))) ).
cnf(u8530,axiom,
~ predicate(X0,border,sK240,sK401(sK202)) ).
cnf(u1126,axiom,
sK355 = sK356 ).
cnf(u8037,axiom,
~ predicate(X0,border,sK413(X1),sK401(sK168)) ).
cnf(u1335,axiom,
~ object(sK174,island,countable,na,eq,n1) ).
cnf(u10217,axiom,
predicate(sK443(sK458(sK428(sK426(X0))),sK428(sK426(X0))),border,sK428(sK426(X0)),sK458(sK428(sK426(X0)))) ).
cnf(u8609,axiom,
~ predicate(X0,border,sK293,sK401(sK219)) ).
cnf(u6049,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u914,axiom,
predicate(sK154,flow_through,sK153,sK325) ).
cnf(u9980,axiom,
( ~ predicate(X1,border,sK419(X2),sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u12781,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u1243,axiom,
predicate(sK270,have,sK262,sK269) ).
cnf(u8399,axiom,
~ predicate(X1,border,sK317,sK458(sK428(sK426(X0)))) ).
cnf(u936,axiom,
sK176 = sK178 ).
cnf(u873,axiom,
object(sK347,los_Angeles,named,na,eq,n1) ).
cnf(u1021,axiom,
relation(sK262,of,sK188) ).
cnf(u10209,axiom,
predicate(sK443(sK458(sK404(sK426(X0))),sK404(sK426(X0))),border,sK404(sK426(X0)),sK458(sK404(sK426(X0)))) ).
cnf(u1090,axiom,
sK304 = sK330 ).
cnf(u12097,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u8726,axiom,
~ predicate(X0,border,sK369,sK401(sK219)) ).
cnf(u2994,axiom,
( ~ object(sK426(X0),country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u6307,axiom,
~ relation(sK323,of,sK426(X0)) ).
cnf(u7836,axiom,
( ~ predicate(X0,border,sK440(X1),sK250)
| relation(sK458(sK440(X1)),of,sK174) ) ).
cnf(u6235,axiom,
~ relation(sK276,of,sK430(X0)) ).
cnf(u13196,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u756,axiom,
object(sK10,hungary,named,na,eq,n1) ).
cnf(u2264,axiom,
( ~ predicate(X586,flow_through,X584,X585)
| object(X584,river,countable,na,eq,n1) ) ).
cnf(u9541,axiom,
~ relation(sK275,of,sK368) ).
cnf(u963,axiom,
sK198 = sK200 ).
cnf(u2192,axiom,
sK176 = sK415(sK174,sK176) ).
cnf(u11113,axiom,
~ predicate(X1,border,sK240,sK458(sK404(sK426(X0)))) ).
cnf(u8078,axiom,
predicate(sK443(sK219,sK401(sK219)),border,sK401(sK219),sK219) ).
cnf(u8697,axiom,
~ predicate(X0,border,sK380,sK401(sK174)) ).
cnf(u6997,axiom,
predicate(sK443(sK458(sK240),sK240),border,sK240,sK458(sK240)) ).
cnf(u6963,axiom,
predicate(sK443(sK238,sK458(sK238)),border,sK458(sK238),sK238) ).
cnf(u13286,axiom,
~ predicate(X1,border,sK152,sK458(sK428(sK426(X0)))) ).
cnf(u9399,axiom,
~ property(sK275,located_in,pos,sK260) ).
cnf(u2003,axiom,
predicate(sK443(sK240,sK141),border,sK141,sK240) ).
cnf(u8621,axiom,
~ predicate(X0,border,sK305,sK401(sK202)) ).
cnf(u1284,axiom,
object(sK276,capital,countable,na,eq,n1) ).
cnf(u926,axiom,
sK169 = sK170 ).
cnf(u8028,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK168)) ) ).
cnf(u1107,axiom,
sK340 = sK341 ).
cnf(u8749,axiom,
~ predicate(X0,border,sK372,sK401(sK174)) ).
cnf(u800,axiom,
object(sK137,rome,named,na,eq,n1) ).
cnf(u542,axiom,
object(sK160,language,countable,na,eq,n1) ).
cnf(u176,axiom,
( object(sK440(X531),country,countable,na,eq,n1)
| ~ object(X531,city,countable,na,eq,n1) ) ).
cnf(u10483,axiom,
~ predicate(X1,border,sK176,sK458(sK428(sK430(X0)))) ).
cnf(u2305,axiom,
relation(sK225,of,sK193) ).
cnf(u8056,axiom,
~ predicate(X0,border,sK419(X1),sK401(sK237)) ).
cnf(u885,axiom,
object(sK371,german,named,na,eq,n1) ).
cnf(u399,axiom,
object(sK217,canadian_province,countable,na,eq,n1) ).
cnf(u2147,axiom,
property(sK30,located_in,pos,sK289) ).
cnf(u1082,axiom,
predicate(sK322,contain,sK320,sK321) ).
cnf(u8996,axiom,
~ predicate(X1,border,sK250,sK458(sK428(sK426(X0)))) ).
cnf(u9974,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK368,sK458(X0)) ) ).
cnf(u8722,axiom,
~ predicate(X0,border,sK369,sK401(sK168)) ).
cnf(u11451,axiom,
~ predicate(X1,border,sK287,sK458(sK404(sK430(X0)))) ).
cnf(u1236,axiom,
relation(sK323,of,sK305) ).
cnf(u2223,axiom,
sK376 = sK415(sK113,sK376) ).
cnf(u7174,axiom,
~ predicate(X0,border,sK458(sK289),sK250) ).
cnf(u2295,axiom,
relation(sK198,of,sK193) ).
cnf(u8463,axiom,
~ predicate(X0,border,sK159,sK401(sK174)) ).
cnf(u3066,axiom,
object(sK430(X0),city,countable,na,eq,n1) ).
cnf(u3115,axiom,
~ predicate(X0,border,sK317,sK401(sK168)) ).
cnf(u11616,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u1215,axiom,
relation(sK126,of,sK11) ).
cnf(u2828,axiom,
( ~ object(X592,baltic_state,countable,na,eq,n1)
| object(X592,nATO_country,countable,na,eq,n1) ) ).
cnf(u1221,axiom,
relation(sK240,of,sK174) ).
cnf(u2204,axiom,
sK211 = sK415(sK193,sK211) ).
cnf(u10859,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u79,axiom,
object(sK355,city,countable,na,eq,n1) ).
cnf(u1349,axiom,
~ object(sK323,country,countable,na,eq,n1) ).
cnf(u922,axiom,
( ~ object(X435,continent,countable,na,eq,n1)
| predicate(sK400(X435),contain,X435,sK399(X435))
| sK219 = X435 ) ).
cnf(u2189,axiom,
sK167 = sK415(sK230,sK167) ).
cnf(u7857,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK126,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u8358,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u812,axiom,
object(sK289,uSA,named,na,eq,n1) ).
cnf(u188,axiom,
object(sK319,city,countable,na,eq,n1) ).
cnf(u8554,axiom,
~ predicate(X0,border,sK260,sK401(sK174)) ).
cnf(u13847,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u2317,axiom,
relation(sK357,of,sK250) ).
cnf(u881,axiom,
object(sK367,andorra,named,na,eq,n1) ).
cnf(u8724,axiom,
~ predicate(X0,border,sK369,sK401(sK188)) ).
cnf(u342,axiom,
( object(sK430(X506),capital,countable,na,eq,n1)
| ~ object(X506,country,countable,na,eq,n1) ) ).
cnf(u1100,axiom,
sK323 = sK337 ).
cnf(u8489,axiom,
~ predicate(X0,border,sK176,sK401(sK174)) ).
cnf(u13245,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u1975,axiom,
predicate(sK443(sK174,sK188),border,sK188,sK174) ).
cnf(u9421,axiom,
~ relation(sK275,of,sK287) ).
cnf(u9361,axiom,
~ relation(sK275,of,sK238) ).
cnf(u2291,axiom,
relation(sK190,of,sK225) ).
cnf(u6714,axiom,
( predicate(sK459(sK413(X0)),border,sK413(X0),sK458(sK413(X0)))
| object(sK413(X0),landlocked_country,countable,na,eq,n1) ) ).
cnf(u1079,axiom,
sK169 != sK315 ).
cnf(u301,axiom,
object(sK262,part,countable,na,eq,n1) ).
cnf(u839,axiom,
object(sK202,australian_Continent,named,na,eq,n1) ).
cnf(u971,axiom,
object(sK209,province,countable,na,eq,n1) ).
cnf(u8353,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u10901,axiom,
~ predicate(X1,border,sK238,sK458(sK428(sK430(X0)))) ).
cnf(u12408,axiom,
~ predicate(X1,border,sK313,sK458(sK428(sK426(X0)))) ).
cnf(u1341,axiom,
object(sK144,island,countable,na,eq,n1) ).
cnf(u9959,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK193,sK458(X0)) ) ).
cnf(u8481,axiom,
~ predicate(X0,border,sK172,sK401(sK237)) ).
cnf(u2011,axiom,
predicate(sK443(sK51,sK176),border,sK176,sK51) ).
cnf(u786,axiom,
object(sK174,europe,named,na,eq,n1) ).
cnf(u934,axiom,
relation(sK177,of,sK176) ).
cnf(u9733,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK323,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u10695,axiom,
~ predicate(X1,border,sK193,sK458(sK404(sK426(X0)))) ).
cnf(u8687,axiom,
~ predicate(X0,border,sK367,sK401(sK219)) ).
cnf(u6194,axiom,
~ relation(sK177,of,sK327) ).
cnf(u52,axiom,
( ~ predicate(X586,flow_through,X584,X585)
| sK461(X584) = X584 ) ).
cnf(u1346,axiom,
object(sK126,capital,countable,na,eq,n1) ).
cnf(u184,axiom,
object(sK320,city,countable,na,eq,n1) ).
cnf(u1974,axiom,
predicate(sK443(sK147,sK305),border,sK305,sK147) ).
cnf(u8354,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u8034,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK237)) ) ).
cnf(u893,axiom,
predicate(sK119,flow_through,sK123,sK126) ).
cnf(u10652,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u7906,axiom,
( ~ predicate(X0,border,sK460(X1),sK401(X2))
| ~ object(X1,landlocked_country,countable,na,eq,n1)
| ~ object(X2,continent,countable,na,eq,n1) ) ).
cnf(u3141,axiom,
( ~ predicate(X0,border,sK250,sK401(sK404(X1)))
| ~ object(X1,country,countable,na,eq,n1) ) ).
cnf(u1012,axiom,
predicate(sK255,border,sK250,sK305) ).
cnf(u8501,axiom,
~ predicate(X0,border,sK193,sK401(sK168)) ).
cnf(u169,axiom,
( ~ predicate(X542,border,X540,X541)
| sK444(X540) = X540 ) ).
cnf(u1991,axiom,
predicate(sK443(sK262,sK271),border,sK271,sK262) ).
cnf(u11827,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u835,axiom,
object(sK193,canada,named,na,eq,n1) ).
cnf(u983,axiom,
property(sK221,located_in,pos,sK217) ).
cnf(u2964,axiom,
( ~ object(sK430(X0),country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u6907,axiom,
predicate(sK443(sK176,sK458(sK176)),border,sK458(sK176),sK176) ).
cnf(u8493,axiom,
~ predicate(X0,border,sK176,sK401(sK230)) ).
cnf(u6683,axiom,
( predicate(sK459(X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u798,axiom,
object(sK135,vatican_City,named,na,eq,n1) ).
cnf(u12574,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u2049,axiom,
predicate(sK443(sK238,sK310),border,sK310,sK238) ).
cnf(u14296,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u629,axiom,
object(sK126,city,countable,na,eq,n1) ).
cnf(u1338,axiom,
object(sK147,part,countable,na,eq,n1) ).
cnf(u6121,axiom,
~ relation(sK126,of,sK430(X0)) ).
cnf(u1041,axiom,
sK276 = sK283 ).
cnf(u14292,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u9495,axiom,
~ property(sK275,located_in,pos,sK315) ).
cnf(u2298,axiom,
relation(sK207,of,sK193) ).
cnf(u8244,axiom,
( ~ object(X580,landlocked_country,countable,na,eq,n1)
| object(X580,country,countable,na,eq,n1) ) ).
cnf(u1108,axiom,
sK276 = sK342 ).
cnf(u33,axiom,
( ~ object(X592,baltic_state,countable,na,eq,n1)
| sK464(X592) = X592 ) ).
cnf(u1983,axiom,
predicate(sK443(sK240,sK147),border,sK147,sK240) ).
cnf(u181,axiom,
object(sK323,city,countable,na,eq,n1) ).
cnf(u6342,axiom,
~ relation(sK327,of,sK299) ).
cnf(u965,axiom,
object(sK204,city,countable,na,eq,n1) ).
cnf(u2713,axiom,
predicate(sK402(sK168),border,sK168,sK401(sK168)) ).
cnf(u624,axiom,
object(sK128,city,countable,na,eq,n1) ).
cnf(u1162,axiom,
( predicate(sK454(X568,X567),contain,X567,X568)
| ~ property(X568,located_in,pos,X567) ) ).
cnf(u1390,axiom,
sK147 = sK444(sK147) ).
cnf(u8073,axiom,
predicate(sK443(sK202,sK401(sK202)),border,sK401(sK202),sK202) ).
cnf(u2148,axiom,
property(sK84,located_in,pos,sK289) ).
cnf(u1087,axiom,
sK327 = sK328 ).
cnf(u847,axiom,
object(sK226,washington_DC,named,na,eq,n1) ).
cnf(u9256,axiom,
( ~ predicate(X1,contain,sK439(sK430(X0)),sK275)
| predicate(sK391(sK439(sK430(X0))),appreciate,sK146,sK439(sK430(X0))) ) ).
cnf(u6722,axiom,
( predicate(sK459(sK440(X0)),border,sK440(X0),sK458(sK440(X0)))
| object(sK440(X0),landlocked_country,countable,na,eq,n1) ) ).
cnf(u8632,axiom,
~ predicate(X0,border,sK310,sK401(sK174)) ).
cnf(u2005,axiom,
predicate(sK443(sK305,sK147),border,sK147,sK305) ).
cnf(u6153,axiom,
~ relation(sK137,of,sK276) ).
cnf(u11618,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u11615,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u8031,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK202)) ) ).
cnf(u3116,axiom,
~ predicate(X0,border,sK317,sK401(sK174)) ).
cnf(u11449,axiom,
~ predicate(X1,border,sK287,sK458(sK428(sK430(X0)))) ).
cnf(u794,axiom,
object(sK131,london,named,na,eq,n1) ).
cnf(u12570,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u9741,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK327,of,X0)
| ~ property(sK275,located_in,pos,X0) ) ).
cnf(u2193,axiom,
sK177 = sK415(sK176,sK177) ).
cnf(u6270,axiom,
~ relation(sK299,of,sK327) ).
cnf(u2025,axiom,
predicate(sK443(sK251,sK250),border,sK250,sK251) ).
cnf(u3173,axiom,
object(sK317,country,countable,na,eq,n1) ).
cnf(u8950,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u8624,axiom,
~ predicate(X0,border,sK305,sK401(sK237)) ).
cnf(u1008,axiom,
relation(sK250,of,sK174) ).
cnf(u872,axiom,
object(sK345,tokyo,named,na,eq,n1) ).
cnf(u1020,axiom,
sK260 = sK261 ).
cnf(u12096,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u177,axiom,
( object(sK439(X531),subregion,countable,na,eq,n1)
| ~ object(X531,city,countable,na,eq,n1) ) ).
cnf(u715,axiom,
object(sK51,sweden,named,na,eq,n1) ).
cnf(u961,axiom,
sK198 = sK199 ).
cnf(u8595,axiom,
~ predicate(X0,border,sK289,sK401(sK202)) ).
cnf(u1220,axiom,
relation(sK238,of,sK237) ).
cnf(u9833,axiom,
sK430(X0) = sK434(sK430(X0)) ).
cnf(u8569,axiom,
~ predicate(X0,border,sK262,sK401(sK202)) ).
cnf(u1085,axiom,
sK325 = sK326 ).
cnf(u843,axiom,
object(sK214,alberta,named,na,eq,n1) ).
cnf(u8516,axiom,
~ predicate(X0,border,sK238,sK401(sK188)) ).
cnf(u1159,axiom,
( ~ object(X550,star,countable,na,eq,n1)
| ~ object(X550,planet,countable,na,eq,n1) ) ).
cnf(u1064,axiom,
predicate(sK302,border,sK152,sK250) ).
cnf(u7137,axiom,
predicate(sK443(sK458(sK287),sK287),border,sK287,sK458(sK287)) ).
cnf(u7205,axiom,
predicate(sK443(sK293,sK458(sK293)),border,sK458(sK293),sK293) ).
cnf(u13240,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u1287,axiom,
object(sK340,part,countable,na,eq,n1) ).
cnf(u151,axiom,
object(sK332,city,countable,na,eq,n1) ).
cnf(u8036,axiom,
( ~ predicate(X1,border,X0,sK401(sK428(X2)))
| ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X2,country,countable,na,eq,n1) ) ).
cnf(u56,axiom,
object(sK362,planet,countable,na,eq,n1) ).
cnf(u8754,axiom,
~ predicate(X0,border,sK372,sK401(sK237)) ).
cnf(u994,axiom,
predicate(sK235,govern,sK30,sK289) ).
cnf(u8636,axiom,
~ predicate(X0,border,sK310,sK401(sK230)) ).
cnf(u9507,axiom,
~ property(sK275,located_in,pos,sK317) ).
cnf(u7338,axiom,
predicate(sK443(sK315,sK458(sK315)),border,sK458(sK315),sK315) ).
cnf(u9932,axiom,
~ property(sK275,located_in,pos,sK428(sK426(X0))) ).
cnf(u6048,axiom,
( ~ object(X405,capital,countable,na,eq,n1)
| object(X406,country,countable,na,eq,n1)
| ~ relation(X405,of,X406) ) ).
cnf(u10205,axiom,
predicate(sK443(sK428(sK430(X0)),sK458(sK428(sK430(X0)))),border,sK458(sK428(sK430(X0))),sK428(sK430(X0))) ).
cnf(u30,axiom,
object(sK372,planet,countable,na,eq,n1) ).
cnf(u884,axiom,
object(sK370,lithuania,named,na,eq,n1) ).
cnf(u1016,axiom,
sK250 = sK258 ).
cnf(u2307,axiom,
relation(sK233,of,sK228) ).
cnf(u14522,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u9955,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK152,sK458(X0)) ) ).
cnf(u953,axiom,
sK190 = sK191 ).
cnf(u2320,axiom,
relation(sK376,of,sK113) ).
cnf(u14298,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u973,axiom,
object(sK211,city,countable,na,eq,n1) ).
cnf(u8581,axiom,
~ predicate(X0,border,sK287,sK401(sK188)) ).
cnf(u1312,axiom,
object(sK262,country,countable,na,eq,n1) ).
cnf(u7898,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u2013,axiom,
predicate(sK443(sK52,sK176),border,sK176,sK52) ).
cnf(u14338,axiom,
~ predicate(X1,border,sK370,sK458(sK428(sK430(X0)))) ).
cnf(u11612,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u9277,axiom,
~ relation(sK275,of,sK141) ).
cnf(u9947,axiom,
~ property(sK275,located_in,pos,sK428(sK430(X0))) ).
cnf(u7867,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK177,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u9351,axiom,
~ property(sK275,located_in,pos,sK193) ).
cnf(u8701,axiom,
~ predicate(X0,border,sK380,sK401(sK230)) ).
cnf(u1264,axiom,
property(sK325,located_in,pos,sK250) ).
cnf(u1006,axiom,
predicate(sK248,govern,sK169,sK240) ).
cnf(u797,axiom,
object(sK134,singapore,named,na,eq,n1) ).
cnf(u2716,axiom,
predicate(sK402(sK202),border,sK202,sK401(sK202)) ).
cnf(u880,axiom,
object(sK362,mercury,named,na,eq,n1) ).
cnf(u7434,axiom,
predicate(sK443(sK152,sK458(sK152)),border,sK458(sK152),sK152) ).
cnf(u8714,axiom,
~ predicate(X0,border,sK368,sK401(sK230)) ).
cnf(u12367,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u13841,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u8325,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK317,sK458(X0)) ) ).
cnf(u1315,axiom,
object(sK260,part,countable,na,eq,n1) ).
cnf(u837,axiom,
object(sK207,ontario,named,na,eq,n1) ).
cnf(u13035,axiom,
~ predicate(X1,border,sK380,sK458(sK428(sK426(X0)))) ).
cnf(u1034,axiom,
sK262 = sK277 ).
cnf(u11403,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u2303,axiom,
relation(sK221,of,sK217) ).
cnf(u8504,axiom,
~ predicate(X0,border,sK193,sK401(sK202)) ).
cnf(u3139,axiom,
~ predicate(X0,border,sK250,sK401(sK237)) ).
cnf(u389,axiom,
object(sK219,continent,countable,na,eq,n1) ).
cnf(u7731,axiom,
( ~ predicate(X0,border,sK458(sK413(X1)),sK250)
| relation(sK413(X1),of,sK174) ) ).
cnf(u7852,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK125,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u11,axiom,
object(sK380,country,countable,na,eq,n1) ).
cnf(u9517,axiom,
~ relation(sK275,of,sK367) ).
cnf(u7816,axiom,
sK440(X0) = sK460(sK440(X0)) ).
cnf(u1083,axiom,
sK129 = sK324 ).
cnf(u7504,axiom,
predicate(sK443(sK458(sK368),sK368),border,sK368,sK458(sK368)) ).
cnf(u1051,axiom,
sK226 = sK291 ).
cnf(u6078,axiom,
~ relation(sK125,of,sK299) ).
cnf(u7860,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK126,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u892,axiom,
predicate(sK118,flow_through,sK123,sK125) ).
cnf(u829,axiom,
object(sK250,switzerland,named,na,eq,n1) ).
cnf(u587,axiom,
object(sK139,river,countable,na,eq,n1) ).
cnf(u6187,axiom,
~ relation(sK177,of,sK125) ).
cnf(u833,axiom,
object(sK190,montreal,named,na,eq,n1) ).
cnf(u8114,axiom,
predicate(sK443(sK401(sK168),sK168),border,sK168,sK401(sK168)) ).
cnf(u1704,axiom,
sK304 = sK434(sK304) ).
cnf(u6263,axiom,
~ relation(sK299,of,sK125) ).
cnf(u253,axiom,
( ~ predicate(X513,overlap_with,X511,X512)
| predicate(sK432(X511,X512),overlap_with,X512,X511) ) ).
cnf(u8030,axiom,
( ~ object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,X0,sK401(sK188)) ) ).
cnf(u13244,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u38,axiom,
object(sK370,baltic_state,countable,na,eq,n1) ).
cnf(u13843,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u1031,axiom,
property(sK275,located_in,pos,sK276) ).
cnf(u919,axiom,
property(sK164,located_in,pos,sK240) ).
cnf(u1078,axiom,
sK315 = sK316 ).
cnf(u9251,axiom,
( ~ predicate(X1,contain,sK419(X0),sK275)
| predicate(sK391(sK419(X0)),appreciate,sK146,sK419(X0)) ) ).
cnf(u6195,axiom,
~ relation(sK177,of,sK426(X0)) ).
cnf(u1293,axiom,
object(sK304,part,countable,na,eq,n1) ).
cnf(u6301,axiom,
~ relation(sK323,of,sK137) ).
cnf(u7563,axiom,
predicate(sK443(sK370,sK458(sK370)),border,sK458(sK370),sK370) ).
cnf(u866,axiom,
object(sK319,chicago,named,na,eq,n1) ).
cnf(u8723,axiom,
~ predicate(X0,border,sK369,sK401(sK174)) ).
cnf(u1014,axiom,
predicate(sK257,border,sK250,sK317) ).
cnf(u9804,axiom,
sK177 = sK434(sK177) ).
cnf(u6115,axiom,
~ relation(sK126,of,sK276) ).
cnf(u3111,axiom,
( ~ object(X0,continent,countable,na,eq,n1)
| ~ predicate(X1,border,sK250,sK401(X0)) ) ).
cnf(u10442,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u8045,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK188)) ).
cnf(u9699,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK137,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u825,axiom,
object(sK169,angela_Merkel,named,na,eq,n1) ).
cnf(u12144,axiom,
~ predicate(X1,border,sK310,sK458(sK404(sK426(X0)))) ).
cnf(u845,axiom,
object(sK221,winnepeg,named,na,eq,n1) ).
cnf(u13842,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u1042,axiom,
sK276 = sK284 ).
cnf(u7343,axiom,
predicate(sK443(sK458(sK315),sK315),border,sK315,sK458(sK315)) ).
cnf(u8139,axiom,
predicate(sK443(sK401(sK230),sK230),border,sK230,sK401(sK230)) ).
cnf(u418,axiom,
( ~ object(X469,province,countable,na,eq,n1)
| sK412(X469) = X469 ) ).
cnf(u964,axiom,
property(sK201,mayor_of,pos,sK198) ).
cnf(u3224,axiom,
( ~ object(X388,eU_country,countable,na,eq,n1)
| object(X388,country,countable,na,eq,n1) ) ).
cnf(u8453,axiom,
~ predicate(X0,border,sK152,sK401(sK219)) ).
cnf(u11828,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u13886,axiom,
~ predicate(X1,border,sK368,sK458(sK428(sK430(X0)))) ).
cnf(u9960,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK238,sK458(X0)) ) ).
cnf(u2216,axiom,
sK325 = sK415(sK250,sK325) ).
cnf(u9471,axiom,
~ property(sK275,located_in,pos,sK310) ).
cnf(u7877,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK299,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u8039,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK168)) ).
cnf(u9707,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK177,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u11614,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u2607,axiom,
relation(X0,of,sK428(X0)) ).
cnf(u19,axiom,
property(sK376,located_in,pos,sK113) ).
cnf(u14520,axiom,
( ~ predicate(X1,border,sK372,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u2201,axiom,
sK207 = sK415(sK193,sK207) ).
cnf(u1136,axiom,
property(sK367,located_in,pos,sK174) ).
cnf(u878,axiom,
object(sK357,lucerne,named,na,eq,n1) ).
cnf(u1278,axiom,
object(sK357,city,countable,na,eq,n1) ).
cnf(u9457,axiom,
~ relation(sK275,of,sK305) ).
cnf(u14113,axiom,
~ predicate(X1,border,sK369,sK458(sK428(sK426(X0)))) ).
cnf(u1059,axiom,
sK137 = sK298 ).
cnf(u1290,axiom,
object(sK131,part,countable,na,eq,n1) ).
cnf(u2190,axiom,
sK171 = sK415(sK289,sK171) ).
cnf(u788,axiom,
object(sK124,belgrad,named,na,eq,n1) ).
cnf(u351,axiom,
( ~ object(X494,country,countable,na,eq,n1)
| predicate(sK423(X494),have,X494,sK422(X494)) ) ).
cnf(u14112,axiom,
~ predicate(X1,border,sK369,sK458(sK428(sK430(X0)))) ).
cnf(u12364,axiom,
( ~ predicate(X1,border,sK313,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u11406,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u10692,axiom,
~ predicate(X1,border,sK193,sK458(sK428(sK430(X0)))) ).
cnf(u1712,axiom,
sK345 = sK434(sK345) ).
cnf(u14295,axiom,
( ~ predicate(X1,border,sK370,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u6343,axiom,
~ relation(sK327,of,sK323) ).
cnf(u12571,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u12616,axiom,
~ predicate(X1,border,sK315,sK458(sK428(sK430(X0)))) ).
cnf(u996,axiom,
sK238 = sK239 ).
cnf(u8438,axiom,
~ predicate(X0,border,sK147,sK401(sK188)) ).
cnf(u1242,axiom,
relation(sK350,of,sK310) ).
cnf(u8144,axiom,
predicate(sK443(sK401(sK237),sK237),border,sK237,sK401(sK237)) ).
cnf(u8610,axiom,
~ predicate(X0,border,sK293,sK401(sK230)) ).
cnf(u1039,axiom,
sK262 = sK281 ).
cnf(u8468,axiom,
~ predicate(X0,border,sK159,sK401(sK237)) ).
cnf(u927,axiom,
property(sK171,located_in,pos,sK289) ).
cnf(u1248,axiom,
property(sK190,located_in,pos,sK193) ).
cnf(u8441,axiom,
~ predicate(X0,border,sK147,sK401(sK230)) ).
cnf(u13034,axiom,
~ predicate(X1,border,sK380,sK458(sK428(sK430(X0)))) ).
cnf(u8423,axiom,
~ predicate(X0,border,sK141,sK401(sK168)) ).
cnf(u1713,axiom,
sK347 = sK434(sK347) ).
cnf(u1301,axiom,
object(sK305,part,countable,na,eq,n1) ).
cnf(u2310,axiom,
relation(sK275,of,sK276) ).
cnf(u2213,axiom,
sK275 = sK415(sK276,sK275) ).
cnf(u874,axiom,
object(sK349,tPTP,named,na,eq,n1) ).
cnf(u3120,axiom,
~ predicate(X0,border,sK317,sK401(sK230)) ).
cnf(u8939,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK174)) ).
cnf(u347,axiom,
( ~ object(X500,country,countable,na,eq,n1)
| predicate(sK427(X500),have,X500,sK426(X500)) ) ).
cnf(u1265,axiom,
property(sK323,located_in,pos,sK305) ).
cnf(u6014,axiom,
( predicate(sK382(X383,X384),contain,X384,X383)
| ~ relation(X383,of,X384) ) ).
cnf(u1052,axiom,
predicate(sK292,live,sK84,sK289) ).
cnf(u972,axiom,
property(sK209,located_in,pos,sK193) ).
cnf(u9313,axiom,
~ relation(sK275,of,sK159) ).
cnf(u2902,axiom,
( ~ object(X547,planet,countable,na,eq,n1)
| object(X547,celestial_body,countable,na,eq,n1) ) ).
cnf(u1334,axiom,
~ object(sK177,country,countable,na,eq,n1) ).
cnf(u12099,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u6188,axiom,
~ relation(sK177,of,sK126) ).
cnf(u6117,axiom,
~ relation(sK126,of,sK323) ).
cnf(u791,axiom,
object(sK128,bratislava,named,na,eq,n1) ).
cnf(u923,axiom,
property(sK166,located_in,pos,sK293) ).
cnf(u8596,axiom,
~ predicate(X0,border,sK289,sK401(sK219)) ).
cnf(u2873,axiom,
relation(sK368,of,sK174) ).
cnf(u7466,axiom,
predicate(sK443(sK317,sK458(sK317)),border,sK458(sK317),sK317) ).
cnf(u6427,axiom,
object(sK428(sK430(X0)),country,countable,na,eq,n1) ).
cnf(u9969,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK310,sK458(X0)) ) ).
cnf(u6305,axiom,
~ relation(sK323,of,sK323) ).
cnf(u886,axiom,
object(sK375,italian,named,na,eq,n1) ).
cnf(u8951,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u6233,axiom,
~ relation(sK276,of,sK426(X0)) ).
cnf(u8426,axiom,
~ predicate(X0,border,sK141,sK401(sK202)) ).
cnf(u2871,axiom,
relation(sK370,of,sK174) ).
cnf(u231,axiom,
object(sK299,capital,countable,na,eq,n1) ).
cnf(u6366,axiom,
object(sK372,country,countable,na,eq,n1) ).
cnf(u8400,axiom,
~ predicate(X1,border,sK317,sK458(sK404(sK430(X0)))) ).
cnf(u1698,axiom,
sK221 = sK434(sK221) ).
cnf(u6081,axiom,
~ relation(sK125,of,sK426(X0)) ).
cnf(u10902,axiom,
~ predicate(X1,border,sK238,sK458(sK428(sK426(X0)))) ).
cnf(u10857,axiom,
( ~ predicate(X1,border,sK238,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u2285,axiom,
relation(sK166,of,sK293) ).
cnf(u836,axiom,
object(sK198,ottawa,named,na,eq,n1) ).
cnf(u12575,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u968,axiom,
sK204 = sK205 ).
cnf(u6059,axiom,
( ~ relation(sK430(X1),of,X0)
| object(X0,country,countable,na,eq,n1) ) ).
cnf(u2183,axiom,
sK30 = sK415(sK289,sK30) ).
cnf(u1250,axiom,
property(sK198,the_capital_of,pos,sK193) ).
cnf(u6339,axiom,
~ relation(sK327,of,sK137) ).
cnf(u1699,axiom,
sK223 = sK434(sK223) ).
cnf(u3061,axiom,
object(sK299,city,countable,na,eq,n1) ).
cnf(u1392,axiom,
sK176 = sK444(sK176) ).
cnf(u8592,axiom,
~ predicate(X0,border,sK289,sK401(sK168)) ).
cnf(u12990,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u6114,axiom,
~ relation(sK126,of,sK177) ).
cnf(u7882,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK323,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u12101,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u1150,axiom,
( ~ object(X409,capital,countable,na,eq,n1)
| ~ object(X409,country,countable,na,eq,n1) ) ).
cnf(u8559,axiom,
~ predicate(X0,border,sK260,sK401(sK237)) ).
cnf(u1216,axiom,
relation(sK129,of,sK240) ).
cnf(u2194,axiom,
sK190 = sK415(sK225,sK190) ).
cnf(u435,axiom,
object(sK202,continent,countable,na,eq,n1) ).
cnf(u355,axiom,
predicate(sK236,appreciate,sK30,sK73) ).
cnf(u1267,axiom,
property(sK357,located_in,pos,sK250) ).
cnf(u2122,axiom,
( ~ object(X469,province,countable,na,eq,n1)
| sK414(X469) = X469 ) ).
cnf(u14067,axiom,
( ~ predicate(X1,border,sK369,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u832,axiom,
object(sK238,argentina,named,na,eq,n1) ).
cnf(u2484,axiom,
relation(X0,of,sK439(X0)) ).
cnf(u1998,axiom,
predicate(sK443(sK380,sK240),border,sK240,sK380) ).
cnf(u8088,axiom,
predicate(sK443(sK237,sK401(sK237)),border,sK401(sK237),sK237) ).
cnf(u917,axiom,
predicate(sK158,live,sK30,sK289) ).
cnf(u1114,axiom,
sK345 = sK346 ).
cnf(u1342,axiom,
object(sK141,part,countable,na,eq,n1) ).
cnf(u9303,axiom,
~ property(sK275,located_in,pos,sK152) ).
cnf(u8928,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK230)) ).
cnf(u799,axiom,
object(sK136,monaco,named,na,eq,n1) ).
cnf(u1408,axiom,
sK152 = sK444(sK152) ).
cnf(u8605,axiom,
~ predicate(X0,border,sK293,sK401(sK168)) ).
cnf(u1247,axiom,
property(sK177,the_capital_of,pos,sK176) ).
cnf(u9968,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK305,sK458(X0)) ) ).
cnf(u2714,axiom,
predicate(sK402(sK174),border,sK174,sK401(sK174)) ).
cnf(u13239,axiom,
( ~ predicate(X1,border,sK152,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u10484,axiom,
~ predicate(X1,border,sK176,sK458(sK428(sK426(X0)))) ).
cnf(u3125,axiom,
( ~ predicate(X0,border,sK317,sK401(sK428(X1)))
| ~ object(X1,country,countable,na,eq,n1) ) ).
cnf(u8929,axiom,
~ predicate(X0,border,sK439(sK426(X1)),sK401(sK237)) ).
cnf(u8649,axiom,
~ predicate(X0,border,sK313,sK401(sK230)) ).
cnf(u1706,axiom,
sK320 = sK434(sK320) ).
cnf(u1137,axiom,
predicate(sK373,orbit,sK372,sK187) ).
cnf(u1131,axiom,
object(sK361,city,countable,na,eq,n1) ).
cnf(u824,axiom,
object(sK364,venus,named,na,eq,n1) ).
cnf(u844,axiom,
object(sK217,manitoba,named,na,eq,n1) ).
cnf(u6073,axiom,
~ relation(sK125,of,sK125) ).
cnf(u220,axiom,
object(sK305,country,countable,na,eq,n1) ).
cnf(u13887,axiom,
~ predicate(X1,border,sK368,sK458(sK428(sK426(X0)))) ).
cnf(u9636,axiom,
( predicate(sK391(X0),appreciate,sK146,X0)
| ~ relation(sK125,of,X0)
| ~ relation(sK275,of,X0) ) ).
cnf(u913,axiom,
predicate(sK151,orbit,sK150,sK187) ).
cnf(u11112,axiom,
~ predicate(X1,border,sK240,sK458(sK404(sK430(X0)))) ).
cnf(u1260,axiom,
property(sK226,the_capital_of,pos,sK289) ).
cnf(u795,axiom,
object(sK315,united_Kingdom,named,na,eq,n1) ).
cnf(u13220,axiom,
( predicate(sK443(sK458(X0),X0),border,X0,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u2007,axiom,
predicate(sK443(sK188,sK174),border,sK174,sK188) ).
cnf(u205,axiom,
object(sK313,country,countable,na,eq,n1) ).
cnf(u1400,axiom,
sK250 = sK444(sK250) ).
cnf(u118,axiom,
object(sK345,city,countable,na,eq,n1) ).
cnf(u1414,axiom,
sK380 = sK444(sK380) ).
cnf(u999,axiom,
predicate(sK242,border,sK240,sK380) ).
cnf(u787,axiom,
object(sK123,danube,named,na,eq,n1) ).
cnf(u1245,axiom,
property(sK177,located_in,pos,sK176) ).
cnf(u7855,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK125,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u1030,axiom,
object(sK275,ceramic,countable,na,eq,n1) ).
cnf(u8298,axiom,
( ~ predicate(X0,border,sK401(sK404(X1)),sK250)
| relation(sK404(X1),of,sK174) ) ).
cnf(u103,axiom,
( object(sK447(X555),star,countable,na,eq,n1)
| ~ object(X555,planet,countable,na,eq,n1) ) ).
cnf(u8661,axiom,
~ predicate(X0,border,sK315,sK401(sK219)) ).
cnf(u946,axiom,
sK177 = sK186 ).
cnf(u1224,axiom,
relation(sK287,of,sK202) ).
cnf(u966,axiom,
property(sK204,located_in,pos,sK207) ).
cnf(u1687,axiom,
sK126 = sK434(sK126) ).
cnf(u6226,axiom,
~ relation(sK276,of,sK126) ).
cnf(u1692,axiom,
sK155 = sK434(sK155) ).
cnf(u6154,axiom,
~ relation(sK137,of,sK299) ).
cnf(u679,axiom,
object(sK87,spain,named,na,eq,n1) ).
cnf(u925,axiom,
~ predicate(X446,control,sK168,sK364) ).
cnf(u1122,axiom,
object(sK353,city,countable,na,eq,n1) ).
cnf(u1124,axiom,
predicate(sK354,dislike,sK265,sK30) ).
cnf(u10221,axiom,
predicate(sK443(sK458(sK428(sK430(X0))),sK428(sK430(X0))),border,sK428(sK430(X0)),sK458(sK428(sK430(X0)))) ).
cnf(u8464,axiom,
~ predicate(X0,border,sK159,sK401(sK188)) ).
cnf(u6267,axiom,
~ relation(sK299,of,sK276) ).
cnf(u2296,axiom,
relation(sK204,of,sK207) ).
cnf(u10485,axiom,
~ predicate(X1,border,sK176,sK458(sK404(sK430(X0)))) ).
cnf(u8650,axiom,
~ predicate(X0,border,sK313,sK401(sK237)) ).
cnf(u3043,axiom,
( ~ object(X469,province,countable,na,eq,n1)
| object(X469,subregion,countable,na,eq,n1) ) ).
cnf(u6340,axiom,
~ relation(sK327,of,sK177) ).
cnf(u1700,axiom,
sK226 = sK434(sK226) ).
cnf(u2687,axiom,
relation(X0,of,sK419(X0)) ).
cnf(u9870,axiom,
~ relation(sK275,of,sK404(sK426(X0))) ).
cnf(u2035,axiom,
predicate(sK443(sK317,sK250),border,sK250,sK317) ).
cnf(u2281,axiom,
relation(sK84,of,sK289) ).
cnf(u1316,axiom,
object(sK250,country,countable,na,eq,n1) ).
cnf(u958,axiom,
object(sK198,city,countable,na,eq,n1) ).
cnf(u1230,axiom,
relation(sK315,of,sK174) ).
cnf(u194,axiom,
object(sK317,alpine_country,countable,na,eq,n1) ).
cnf(u9409,axiom,
~ relation(sK275,of,sK262) ).
cnf(u1139,axiom,
predicate(sK381,border,sK380,sK240) ).
cnf(u8566,axiom,
~ predicate(X0,border,sK262,sK401(sK168)) ).
cnf(u9977,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK372,sK458(X0)) ) ).
cnf(u789,axiom,
object(sK125,budapest,named,na,eq,n1) ).
cnf(u2051,axiom,
predicate(sK443(sK11,sK317),border,sK317,sK11) ).
cnf(u1701,axiom,
sK229 = sK434(sK229) ).
cnf(u1329,axiom,
~ object(sK188,island,countable,na,eq,n1) ).
cnf(u2015,axiom,
predicate(sK443(sK182,sK176),border,sK176,sK182) ).
cnf(u13889,axiom,
~ predicate(X1,border,sK368,sK458(sK404(sK426(X0)))) ).
cnf(u9900,axiom,
~ relation(sK275,of,sK439(sK426(X0))) ).
cnf(u8558,axiom,
~ predicate(X0,border,sK260,sK401(sK230)) ).
cnf(u12572,axiom,
( ~ predicate(X1,border,sK315,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u1119,axiom,
( ~ object(X564,planet,countable,na,eq,n1)
| predicate(sK453(X564),orbit,X564,sK187) ) ).
cnf(u341,axiom,
object(sK238,country,countable,na,eq,n1) ).
cnf(u1007,axiom,
object(sK250,alpine_country,countable,na,eq,n1) ).
cnf(u1253,axiom,
property(sK240,larger_than,pos,sK317) ).
cnf(u11824,axiom,
( ~ predicate(X1,border,sK293,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u9339,axiom,
~ property(sK275,located_in,pos,sK176) ).
cnf(u2293,axiom,
relation(sK193,of,sK230) ).
cnf(u954,axiom,
object(sK193,country,countable,na,eq,n1) ).
cnf(u8119,axiom,
predicate(sK443(sK401(sK174),sK174),border,sK174,sK401(sK174)) ).
cnf(u7885,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK323,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u2221,axiom,
sK361 = sK415(sK238,sK361) ).
cnf(u11409,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u92,axiom,
object(sK350,city,countable,na,eq,n1) ).
cnf(u13888,axiom,
~ predicate(X1,border,sK368,sK458(sK404(sK430(X0)))) ).
cnf(u785,axiom,
object(sK187,sun,named,na,eq,n1) ).
cnf(u1217,axiom,
relation(sK141,of,sK174) ).
cnf(u9631,axiom,
~ relation(sK275,of,sK440(X0)) ).
cnf(u6192,axiom,
~ relation(sK177,of,sK299) ).
cnf(u1132,axiom,
property(sK361,located_in,pos,sK238) ).
cnf(u12143,axiom,
~ predicate(X1,border,sK310,sK458(sK404(sK430(X0)))) ).
cnf(u8735,axiom,
~ predicate(X0,border,sK370,sK401(sK168)) ).
cnf(u520,axiom,
( ~ object(X440,continent,countable,na,eq,n1)
| predicate(sK402(X440),border,X440,sK401(X440)) ) ).
cnf(u1286,axiom,
object(sK276,city,countable,na,eq,n1) ).
cnf(u14339,axiom,
~ predicate(X1,border,sK370,sK458(sK428(sK426(X0)))) ).
cnf(u8702,axiom,
~ predicate(X0,border,sK380,sK401(sK237)) ).
cnf(u871,axiom,
object(sK340,sydney,named,na,eq,n1) ).
cnf(u1003,axiom,
sK240 = sK245 ).
cnf(u9248,axiom,
( ~ predicate(X1,contain,sK404(sK430(X0)),sK275)
| predicate(sK391(sK404(sK430(X0))),appreciate,sK146,sK404(sK430(X0))) ) ).
cnf(u12100,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u1708,axiom,
sK325 = sK434(sK325) ).
cnf(u12142,axiom,
~ predicate(X1,border,sK310,sK458(sK428(sK426(X0)))) ).
cnf(u2043,axiom,
predicate(sK443(sK11,sK152),border,sK152,sK11) ).
cnf(u818,axiom,
object(sK219,antarctica,named,na,eq,n1) ).
cnf(u8503,axiom,
~ predicate(X0,border,sK193,sK401(sK188)) ).
cnf(u9445,axiom,
~ relation(sK275,of,sK293) ).
cnf(u838,axiom,
object(sK201,larry_OBrien,named,na,eq,n1) ).
cnf(u1238,axiom,
relation(sK276,of,sK262) ).
cnf(u7862,axiom,
( ~ predicate(X1,border,sK458(X0),sK250)
| ~ relation(sK137,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1)
| relation(X0,of,sK174) ) ).
cnf(u10486,axiom,
~ predicate(X1,border,sK176,sK458(sK404(sK426(X0)))) ).
cnf(u8068,axiom,
predicate(sK443(sK188,sK401(sK188)),border,sK401(sK188),sK188) ).
cnf(u12988,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u8943,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK230)) ).
cnf(u8688,axiom,
~ predicate(X0,border,sK367,sK401(sK230)) ).
cnf(u7370,axiom,
predicate(sK443(sK367,sK458(sK367)),border,sK458(sK367),sK367) ).
cnf(u6080,axiom,
~ relation(sK125,of,sK327) ).
cnf(u1709,axiom,
sK327 = sK434(sK327) ).
cnf(u916,axiom,
predicate(sK157,orbit,sK156,sK187) ).
cnf(u6116,axiom,
~ relation(sK126,of,sK299) ).
cnf(u1337,axiom,
~ object(sK168,island,countable,na,eq,n1) ).
cnf(u985,axiom,
property(sK223,located_in,pos,sK207) ).
cnf(u8619,axiom,
~ predicate(X0,border,sK305,sK401(sK174)) ).
cnf(u6159,axiom,
~ relation(sK137,of,sK430(X0)) ).
cnf(u8398,axiom,
~ predicate(X1,border,sK317,sK458(sK428(sK430(X0)))) ).
cnf(u8054,axiom,
~ predicate(X0,border,sK440(X1),sK401(sK230)) ).
cnf(u867,axiom,
object(sK320,fortaleza,named,na,eq,n1) ).
cnf(u13036,axiom,
~ predicate(X1,border,sK380,sK458(sK404(sK430(X0)))) ).
cnf(u1229,axiom,
relation(sK313,of,sK188) ).
cnf(u1344,axiom,
~ object(sK137,country,countable,na,eq,n1) ).
cnf(u14340,axiom,
~ predicate(X1,border,sK370,sK458(sK404(sK430(X0)))) ).
cnf(u8712,axiom,
~ predicate(X0,border,sK368,sK401(sK202)) ).
cnf(u2319,axiom,
relation(sK367,of,sK174) ).
cnf(u9423,axiom,
~ property(sK275,located_in,pos,sK287) ).
cnf(u6268,axiom,
~ relation(sK299,of,sK299) ).
cnf(u830,axiom,
object(sK176,norway,named,na,eq,n1) ).
cnf(u336,axiom,
object(sK240,country,countable,na,eq,n1) ).
cnf(u1102,axiom,
sK323 = sK338 ).
cnf(u14564,axiom,
~ predicate(X1,border,sK372,sK458(sK428(sK430(X0)))) ).
cnf(u9770,axiom,
( ~ predicate(X517,overlap_with,X515,X516)
| object(X515,area,countable,na,eq,n1) ) ).
cnf(u10693,axiom,
~ predicate(X1,border,sK193,sK458(sK428(sK426(X0)))) ).
cnf(u7303,axiom,
predicate(sK443(sK458(sK313),sK313),border,sK313,sK458(sK313)) ).
cnf(u1073,axiom,
sK310 = sK311 ).
cnf(u8598,axiom,
~ predicate(X0,border,sK289,sK401(sK237)) ).
cnf(u2837,axiom,
( ~ object(X590,baltic_state,countable,na,eq,n1)
| object(X590,eU_country,countable,na,eq,n1) ) ).
cnf(u1219,axiom,
relation(sK176,of,sK174) ).
cnf(u6055,axiom,
( object(X0,country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u382,axiom,
( ~ object(X489,subregion,countable,na,eq,n1)
| predicate(sK420(X489),contain,sK419(X489),X489) ) ).
cnf(u912,axiom,
predicate(sK149,border,sK147,sK305) ).
cnf(u8659,axiom,
~ predicate(X0,border,sK315,sK401(sK188)) ).
cnf(u9979,axiom,
( ~ predicate(X1,border,sK413(X2),sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ object(X0,country,countable,na,eq,n1) ) ).
cnf(u1347,axiom,
~ object(sK125,country,countable,na,eq,n1) ).
cnf(u179,axiom,
( object(sK437(X528),mayor,countable,na,exactly,n1)
| ~ object(X528,city,countable,na,eq,n1) ) ).
cnf(u8631,axiom,
~ predicate(X0,border,sK310,sK401(sK168)) ).
cnf(u1694,axiom,
sK190 = sK434(sK190) ).
cnf(u6341,axiom,
~ relation(sK327,of,sK276) ).
cnf(u879,axiom,
object(sK361,buenos_Aires,named,na,eq,n1) ).
cnf(u9529,axiom,
~ relation(sK275,of,sK380) ).
cnf(u10444,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u8265,axiom,
predicate(sK443(sK428(X0),sK401(sK428(X0))),border,sK401(sK428(X0)),sK428(X0)) ).
cnf(u2037,axiom,
predicate(sK443(sK293,sK262),border,sK262,sK293) ).
cnf(u186,axiom,
( object(sK435(X525),person,countable,na,greater,n1)
| ~ object(X525,city,countable,na,eq,n1) ) ).
cnf(u2315,axiom,
relation(sK355,of,sK250) ).
cnf(u3227,axiom,
object(sK370,country,countable,na,eq,n1) ).
cnf(u8063,axiom,
predicate(sK443(sK174,sK401(sK174)),border,sK401(sK174),sK174) ).
cnf(u826,axiom,
object(sK171,norfolk,named,na,eq,n1) ).
cnf(u348,axiom,
( object(sK426(X500),capital,countable,na,eq,n1)
| ~ object(X500,country,countable,na,eq,n1) ) ).
cnf(u6075,axiom,
~ relation(sK125,of,sK137) ).
cnf(u9531,axiom,
~ property(sK275,located_in,pos,sK380) ).
cnf(u529,axiom,
( ~ object(X431,continent,countable,na,eq,n1)
| sK397(X431) = X431 ) ).
cnf(u171,axiom,
( ~ predicate(X538,border,X536,X537)
| predicate(sK443(X536,X537),border,X537,X536) ) ).
cnf(u6306,axiom,
~ relation(sK323,of,sK327) ).
cnf(u8597,axiom,
~ predicate(X0,border,sK289,sK401(sK230)) ).
cnf(u8356,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u3133,axiom,
~ predicate(X0,border,sK250,sK401(sK168)) ).
cnf(u1089,axiom,
sK327 = sK329 ).
cnf(u8725,axiom,
~ predicate(X0,border,sK369,sK401(sK202)) ).
cnf(u2214,axiom,
sK276 = sK415(sK262,sK276) ).
cnf(u518,axiom,
( object(sK404(X443),continent,countable,na,eq,n1)
| ~ object(X443,country,countable,na,eq,n1) ) ).
cnf(u924,axiom,
property(sK167,located_in,pos,sK230) ).
cnf(u650,axiom,
object(sK115,planet,countable,na,eq,n1) ).
cnf(u9976,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK370,sK458(X0)) ) ).
cnf(u993,axiom,
predicate(sK234,dislike,sK73,sK169) ).
cnf(u9411,axiom,
~ property(sK275,located_in,pos,sK262) ).
cnf(u13285,axiom,
~ predicate(X1,border,sK152,sK458(sK428(sK430(X0)))) ).
cnf(u875,axiom,
object(sK350,rio_de_Janeiro,named,na,eq,n1) ).
cnf(u10903,axiom,
~ predicate(X1,border,sK238,sK458(sK404(sK430(X0)))) ).
cnf(u12095,axiom,
( ~ predicate(X1,border,sK310,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u1352,axiom,
~ object(sK126,country,countable,na,eq,n1) ).
cnf(u10650,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u9247,axiom,
( ~ predicate(X1,contain,sK404(sK426(X0)),sK275)
| predicate(sK391(sK404(sK426(X0))),appreciate,sK146,sK404(sK426(X0))) ) ).
cnf(u344,axiom,
( ~ object(X503,country,countable,na,eq,n1)
| sK429(X503) = X503 ) ).
cnf(u1110,axiom,
sK276 = sK343 ).
cnf(u7734,axiom,
predicate(sK443(sK413(X0),sK458(sK413(X0))),border,sK458(sK413(X0)),sK413(X0)) ).
cnf(u10201,axiom,
predicate(sK443(sK428(sK426(X0)),sK458(sK428(sK426(X0)))),border,sK458(sK428(sK426(X0))),sK428(sK426(X0))) ).
cnf(u7940,axiom,
( ~ predicate(X1,border,sK413(X0),sK401(X2))
| ~ object(X2,continent,countable,na,eq,n1) ) ).
cnf(u8593,axiom,
~ predicate(X0,border,sK289,sK401(sK174)) ).
cnf(u9253,axiom,
( ~ predicate(X1,contain,sK428(sK426(X0)),sK275)
| predicate(sK391(sK428(sK426(X0))),appreciate,sK146,sK428(sK426(X0))) ) ).
cnf(u8685,axiom,
~ predicate(X0,border,sK367,sK401(sK188)) ).
cnf(u1081,axiom,
predicate(sK318,border,sK317,sK11) ).
cnf(u3143,axiom,
( ~ predicate(X0,border,sK250,sK401(sK428(X1)))
| ~ object(X1,country,countable,na,eq,n1) ) ).
cnf(u9973,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK367,sK458(X0)) ) ).
cnf(u1227,axiom,
relation(sK305,of,sK174) ).
cnf(u12826,axiom,
~ predicate(X1,border,sK367,sK458(sK428(sK426(X0)))) ).
cnf(u9978,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK380,sK458(X0)) ) ).
cnf(u857,axiom,
object(sK265,tibet,named,na,eq,n1) ).
cnf(u8491,axiom,
~ predicate(X0,border,sK176,sK401(sK202)) ).
cnf(u1005,axiom,
predicate(sK247,appreciate,sK379,sK240) ).
cnf(u10193,axiom,
predicate(sK443(sK404(sK426(X0)),sK458(sK404(sK426(X0)))),border,sK458(sK404(sK426(X0))),sK404(sK426(X0))) ).
cnf(u693,axiom,
object(sK73,linux_User,named,na,eq,n1) ).
cnf(u7375,axiom,
predicate(sK443(sK458(sK367),sK367),border,sK367,sK458(sK367)) ).
cnf(u8710,axiom,
~ predicate(X0,border,sK368,sK401(sK174)) ).
cnf(u8689,axiom,
~ predicate(X0,border,sK367,sK401(sK237)) ).
cnf(u2045,axiom,
predicate(sK443(sK152,sK305),border,sK305,sK152) ).
cnf(u8646,axiom,
~ predicate(X0,border,sK313,sK401(sK188)) ).
cnf(u12410,axiom,
~ predicate(X1,border,sK313,sK458(sK404(sK426(X0)))) ).
cnf(u11110,axiom,
~ predicate(X1,border,sK240,sK458(sK428(sK430(X0)))) ).
cnf(u7890,axiom,
( predicate(sK443(X0,sK458(X0)),border,sK458(X0),X0)
| ~ relation(sK327,of,X0)
| object(X0,landlocked_country,countable,na,eq,n1) ) ).
cnf(u6197,axiom,
~ relation(sK177,of,sK430(X0)) ).
cnf(u8262,axiom,
( ~ predicate(X0,border,sK401(sK428(X1)),sK250)
| relation(sK428(X1),of,sK174) ) ).
cnf(u537,axiom,
( ~ object(X426,island_country,countable,na,eq,n1)
| ~ object(X425,country,countable,na,eq,n1)
| sK395(X425) = X425
| ~ predicate(X427,border,X425,X426) ) ).
cnf(u1987,axiom,
predicate(sK443(sK250,sK305),border,sK305,sK250) ).
cnf(u1396,axiom,
sK230 = sK444(sK230) ).
cnf(u11405,axiom,
( ~ predicate(X1,border,sK287,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u8699,axiom,
~ predicate(X0,border,sK380,sK401(sK202)) ).
cnf(u12786,axiom,
( ~ predicate(X1,border,sK367,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u784,axiom,
object(sK115,jupiter,named,na,eq,n1) ).
cnf(u526,axiom,
( ~ object(X433,continent,countable,na,eq,n1)
| sK398(X433) = X433 ) ).
cnf(u869,axiom,
object(sK327,berlin,named,na,eq,n1) ).
cnf(u511,axiom,
object(sK168,continent,countable,na,eq,n1) ).
cnf(u11070,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK323,of,X0) ) ).
cnf(u8940,axiom,
~ predicate(X0,border,sK439(sK430(X1)),sK401(sK188)) ).
cnf(u9255,axiom,
( ~ predicate(X1,contain,sK439(sK426(X0)),sK275)
| predicate(sK391(sK439(sK426(X0))),appreciate,sK146,sK439(sK426(X0))) ) ).
cnf(u6077,axiom,
~ relation(sK125,of,sK276) ).
cnf(u8477,axiom,
~ predicate(X0,border,sK172,sK401(sK188)) ).
cnf(u1281,axiom,
object(sK345,part,countable,na,eq,n1) ).
cnf(u2207,axiom,
sK223 = sK415(sK207,sK223) ).
cnf(u3171,axiom,
object(sK152,country,countable,na,eq,n1) ).
cnf(u58,axiom,
( ~ object(X582,sea,countable,na,eq,n1)
| ~ predicate(X583,border,sK460(X580),X582)
| ~ object(X580,landlocked_country,countable,na,eq,n1) ) ).
cnf(u12989,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK126,of,X0) ) ).
cnf(u7210,axiom,
predicate(sK443(sK458(sK293),sK293),border,sK293,sK458(sK293)) ).
cnf(u736,axiom,
object(sK30,barack_Obama,named,na,eq,n1) ).
cnf(u9958,axiom,
( ~ object(X0,country,countable,na,eq,n1)
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ predicate(X1,border,sK176,sK458(X0)) ) ).
cnf(u10187,axiom,
predicate(sK459(sK404(sK426(X0))),border,sK404(sK426(X0)),sK458(sK404(sK426(X0)))) ).
cnf(u421,axiom,
( object(sK413(X469),country,countable,na,eq,n1)
| ~ object(X469,province,countable,na,eq,n1) ) ).
cnf(u2188,axiom,
sK166 = sK415(sK293,sK166) ).
cnf(u13844,axiom,
( ~ predicate(X1,border,sK368,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK276,of,X0) ) ).
cnf(u43,axiom,
( ~ object(X588,object_c,countable,na,eq,n1)
| sK462(X588) = X588 ) ).
cnf(u9291,axiom,
~ property(sK275,located_in,pos,sK147) ).
cnf(u10440,axiom,
( ~ predicate(X1,border,sK176,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u8134,axiom,
predicate(sK443(sK401(sK219),sK219),border,sK219,sK401(sK219)) ).
cnf(u10648,axiom,
( ~ predicate(X1,border,sK193,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK137,of,X0) ) ).
cnf(u2301,axiom,
relation(sK211,of,sK193) ).
cnf(u8514,axiom,
~ predicate(X0,border,sK238,sK401(sK168)) ).
cnf(u796,axiom,
object(sK132,saturn,named,na,eq,n1) ).
cnf(u11617,axiom,
( ~ predicate(X1,border,sK289,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK299,of,X0) ) ).
cnf(u865,axiom,
object(sK313,japan,named,na,eq,n1) ).
cnf(u11064,axiom,
( ~ predicate(X1,border,sK240,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u6118,axiom,
~ relation(sK126,of,sK327) ).
cnf(u10694,axiom,
~ predicate(X1,border,sK193,sK458(sK404(sK430(X0)))) ).
cnf(u8352,axiom,
( ~ predicate(X1,border,sK317,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK125,of,X0) ) ).
cnf(u2896,axiom,
( ~ object(sK447(X0),planet,countable,na,eq,n1)
| ~ object(X0,planet,countable,na,eq,n1) ) ).
cnf(u7968,axiom,
( ~ predicate(X1,border,sK440(X0),sK401(X2))
| ~ object(X2,continent,countable,na,eq,n1) ) ).
cnf(u8634,axiom,
~ predicate(X0,border,sK310,sK401(sK202)) ).
cnf(u1063,axiom,
sK152 = sK301 ).
cnf(u6074,axiom,
~ relation(sK125,of,sK126) ).
cnf(u9945,axiom,
~ relation(sK275,of,sK428(sK430(X0))) ).
cnf(u951,axiom,
property(sK190,located_in,pos,sK225) ).
cnf(u982,axiom,
object(sK221,city,countable,na,eq,n1) ).
cnf(u6228,axiom,
~ relation(sK276,of,sK177) ).
cnf(u8952,axiom,
( ~ predicate(X1,border,sK250,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK177,of,X0) ) ).
cnf(u12995,axiom,
( ~ predicate(X1,border,sK380,sK458(X0))
| object(X0,landlocked_country,countable,na,eq,n1)
| ~ relation(sK327,of,X0) ) ).
cnf(u1325,axiom,
object(sK209,canadian_province,countable,na,eq,n1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEG001+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n001.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 06:34:45 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 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
% 4.85/1.18 % (3195363)Will run a generic schedule for satisfiability detection.
% 4.85/1.18 % (3195383)dis+10_1_sil=32000:sp=arity:random_seed=691012056:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.85/1.18 % (3195381)% WARNING: option uhcvi not known.
% 4.85/1.18 % (3195381)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3300853651:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.85/1.18 % (3195379)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2096949721_2999 on theBenchmark for (2999ds/0Mi)
% 4.85/1.18 % (3195382)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2675606280:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.85/1.18 % (3195385)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3818110128:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.85/1.18 % (3195386)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2117163194:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.85/1.18 % (3195384)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3311725887:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.85/1.18 % (3195383)Instruction limit reached!
% 4.85/1.18 % (3195383)------------------------------
% 4.85/1.18 % (3195383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195383)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195383)Termination reason: Instruction limit
% 4.85/1.18 % (3195383)Termination phase: Saturation
% 4.85/1.18 % (3195383)Time elapsed: 0.029 s
% 4.85/1.18 % (3195383)Peak memory usage: 13 MB
% 4.85/1.18 % (3195383)Instructions burned: 104 (million)
% 4.85/1.18 % (3195417)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3418364563:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.85/1.18 % (3195384)Instruction limit reached!
% 4.85/1.18 % (3195384)------------------------------
% 4.85/1.18 % (3195384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % TRYING [1]
% 4.85/1.18 % (3195384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195384)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195384)Termination reason: Instruction limit
% 4.85/1.18 % (3195384)Termination phase: Saturation
% 4.85/1.18 % (3195384)Time elapsed: 0.059 s
% 4.85/1.18 % (3195384)Peak memory usage: 14 MB
% 4.85/1.18 % (3195384)Instructions burned: 116 (million)
% 4.85/1.18 % TRYING [2]
% 4.85/1.18 % (3195385)Instruction limit reached!
% 4.85/1.18 % (3195385)------------------------------
% 4.85/1.18 % (3195385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195385)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195385)Termination reason: Instruction limit
% 4.85/1.18 % (3195385)Termination phase: Saturation
% 4.85/1.18 % (3195385)Time elapsed: 0.066 s
% 4.85/1.18 % (3195385)Peak memory usage: 14 MB
% 4.85/1.18 % (3195385)Instructions burned: 132 (million)
% 4.85/1.18 % (3195423)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=530051345:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.85/1.18 % TRYING [1]
% 4.85/1.18 % TRYING [2]
% 4.85/1.18 % (3195424)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1605875359:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.85/1.18 % (3195386)Instruction limit reached!
% 4.85/1.18 % (3195386)------------------------------
% 4.85/1.18 % (3195386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195386)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195386)Termination reason: Instruction limit
% 4.85/1.18 % (3195386)Termination phase: Saturation
% 4.85/1.18 % (3195386)Time elapsed: 0.089 s
% 4.85/1.18 % (3195386)Peak memory usage: 15 MB
% 4.85/1.18 % (3195386)Instructions burned: 160 (million)
% 4.85/1.18 % TRYING [3]
% 4.85/1.18 % TRYING [3]
% 4.85/1.18 % (3195427)ott-21_1_sil=16000:fs=off:random_seed=1651039981:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.85/1.18 % (3195423)Instruction limit reached!
% 4.85/1.18 % (3195423)------------------------------
% 4.85/1.18 % (3195423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195423)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195423)Termination reason: Instruction limit
% 4.85/1.18 % (3195423)Termination phase: Saturation
% 4.85/1.18 % (3195423)Time elapsed: 0.070 s
% 4.85/1.18 % (3195423)Peak memory usage: 14 MB
% 4.85/1.18 % (3195423)Instructions burned: 132 (million)
% 4.85/1.18 % (3195429)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4237328459:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.85/1.18 % TRYING [4]
% 4.85/1.18 % (3195427)Instruction limit reached!
% 4.85/1.18 % (3195427)------------------------------
% 4.85/1.18 % (3195427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195427)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195427)Termination reason: Instruction limit
% 4.85/1.18 % (3195427)Termination phase: Saturation
% 4.85/1.18 % (3195427)Time elapsed: 0.090 s
% 4.85/1.18 % (3195427)Peak memory usage: 14 MB
% 4.85/1.18 % (3195427)Instructions burned: 180 (million)
% 4.85/1.18 % (3195417)Instruction limit reached!
% 4.85/1.18 % (3195417)------------------------------
% 4.85/1.18 % (3195417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195417)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195417)Termination reason: Instruction limit
% 4.85/1.18 % (3195417)Termination phase: Finite model building constraint generation
% 4.85/1.18 % (3195417)Time elapsed: 0.164 s
% 4.85/1.18 % (3195417)Peak memory usage: 28 MB
% 4.85/1.18 % (3195417)Instructions burned: 719 (million)
% 4.85/1.18 % (3195432)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2263331224:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.85/1.18 % (3195431)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=618657816:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.85/1.18 % TRYING [1]
% 4.85/1.18 % TRYING [2]
% 4.85/1.18 % TRYING [4]
% 4.85/1.18 % TRYING [3]
% 4.85/1.18 % (3195429)Instruction limit reached!
% 4.85/1.18 % (3195429)------------------------------
% 4.85/1.18 % (3195429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195429)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195429)Termination reason: Instruction limit
% 4.85/1.18 % (3195429)Termination phase: Saturation
% 4.85/1.18 % (3195429)Time elapsed: 0.269 s
% 4.85/1.18 % (3195429)Peak memory usage: 16 MB
% 4.85/1.18 % (3195429)Instructions burned: 479 (million)
% 4.85/1.18 % (3195435)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2208909218:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.85/1.18 % (3195424)Instruction limit reached!
% 4.85/1.18 % (3195424)------------------------------
% 4.85/1.18 % (3195424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195424)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195424)Termination reason: Instruction limit
% 4.85/1.18 % (3195424)Termination phase: Saturation
% 4.85/1.18 % (3195424)Time elapsed: 0.391 s
% 4.85/1.18 % (3195424)Peak memory usage: 21 MB
% 4.85/1.18 % (3195424)Instructions burned: 685 (million)
% 4.85/1.18 % (3195437)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=234927823:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.85/1.18 % (3195431)Instruction limit reached!
% 4.85/1.18 % (3195431)------------------------------
% 4.85/1.18 % (3195431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195431)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195431)Termination reason: Instruction limit
% 4.85/1.18 % (3195431)Termination phase: Finite model building SAT solving
% 4.85/1.18 % (3195431)Time elapsed: 0.346 s
% 4.85/1.18 % (3195431)Peak memory usage: 27 MB
% 4.85/1.18 % (3195431)Instructions burned: 865 (million)
% 4.85/1.18 % (3195432)Instruction limit reached!
% 4.85/1.18 % (3195432)------------------------------
% 4.85/1.18 % (3195432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.85/1.18 % (3195432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.18 % (3195432)CaDiCaL version: 2.1.3
% 4.85/1.18 % (3195432)Termination reason: Instruction limit
% 4.85/1.18 % (3195432)Termination phase: Saturation
% 4.85/1.18 % (3195432)Time elapsed: 0.356 s
% 4.85/1.18 % (3195432)Peak memory usage: 27 MB
% 4.85/1.18 % (3195432)Instructions burned: 1181 (million)
% 4.85/1.18 % (3195440)fmb+10_1_sil=64000:random_seed=1926115407:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 4.85/1.18 % (3195439)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3330347123:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 4.85/1.18 % TRYING [1]
% 4.85/1.18 % TRYING [2]
% 4.85/1.18 % TRYING [3]
% 4.85/1.18 % (3195382) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3195363-3195382"...
% 4.85/1.18 % (3195382)...printing done.
% 4.85/1.18 % SZS status Satisfiable for theBenchmark
% 4.85/1.18 % SZS output start Saturation.
% See solution above
% 5.41/1.21 % SZS output start Definitions and Model Updates.
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK61 := sK204
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK60 := sK202
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK59 := sK201
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK58 := sK207
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK57 := sK198
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK56 := sK193
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK55 := sK225
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK54 := sK190
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK53 := sK238
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK50 := sK177
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK49 := sK176
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK48 := sK250
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK47 := sK188
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK46 := sK172
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK45 := sK171
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK44 := sK169
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK43 := sK364
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK42 := sK168
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK41 := sK230
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK40 := sK167
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK39 := sK293
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK38 := sK166
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK37 := sK219
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK36 := sK372
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK35 := sK164
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK34 := sK163
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK33 := sK160
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK32 := sK159
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK31 := sK289
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK29 := sK156
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK28 := sK155
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK27 := sK153
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK26 := sK150
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK25 := sK305
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK24 := sK147
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK274 := sK275
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK22 := sK141
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK21 := sK325
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK20 := sK139
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK19 := sK152
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK18 := sK137
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK17 := sK136
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK16 := sK135
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK15 := sK134
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK14 := sK132
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK13 := sK315
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK12 := sK131
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK9 := sK240
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK8 := sK129
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK7 := sK128
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK6 := sK126
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK5 := sK125
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK4 := sK124
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK3 := sK123
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK2 := sK174
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK1 := sK187
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK0 := sK115
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK249 := sK250
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK23 := sK144
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK224 := sK225
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK206 := sK207
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK203 := sK204
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK197 := sK198
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK192 := sK193
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK189 := sK190
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK101 := sK353
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK109 := sK370
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK114 := sK377
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK112 := sK376
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK111 := sK375
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK110 := sK371
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK108 := sK369
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK107 := sK368
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK106 := sK367
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK366 := sK367
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK105 := sK362
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK104 := sK361
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK360 := sK361
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK103 := sK357
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK102 := sK355
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK352 := sK353
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK100 := sK350
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK99 := sK349
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK98 := sK347
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK97 := sK345
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK96 := sK340
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK95 := sK332
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK94 := sK327
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK93 := sK323
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK92 := sK320
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK91 := sK319
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK90 := sK313
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK89 := sK310
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK88 := sK374
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK86 := sK304
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK85 := sK299
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK83 := sK287
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK82 := sK280
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK81 := sK276
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK80 := sK265
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK78 := sK262
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK77 := sK260
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK76 := sK379
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK75 := sK317
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK74 := sK380
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK72 := sK233
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK232 := sK233
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK71 := sK237
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK70 := sK229
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK69 := sK228
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK227 := sK228
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK68 := sK226
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK67 := sK223
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK222 := sK223
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK66 := sK221
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK220 := sK221
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK65 := sK217
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK64 := sK214
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK213 := sK214
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK63 := sK211
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK210 := sK211
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK62 := sK209
% 5.41/1.21 for all inputs,
% 5.41/1.21 define sK208 := sK209
% 5.41/1.21 % SZS output end Definitions and Model Updates.
% 5.41/1.21 % (3195382)------------------------------
% 5.41/1.21 % (3195382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.41/1.21 % (3195382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.21 % (3195382)CaDiCaL version: 2.1.3
% 5.41/1.21 % (3195382)Termination reason: Satisfiable
% 5.41/1.21 % (3195382)Time elapsed: 0.705 s
% 5.41/1.21 % (3195382)Peak memory usage: 38 MB
% 5.41/1.21 % (3195382)Instructions burned: 1230 (million)
% 5.41/1.21 % (3195363)Success in time 0.751 s
% 5.41/1.21 % Vampire exiting
%------------------------------------------------------------------------------