%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP241-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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 12:08:07 PM UTC 2026
% Result : Satisfiable 6.02s 1.86s
% Output : Saturation 7.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u116,negated_conjecture,
event(skc26,skf1(X1)) ).
cnf(u123,negated_conjecture,
present(skc26,skf1(X1)) ).
cnf(u127,negated_conjecture,
smoke(skc26,skf1(X1)) ).
cnf(u132,negated_conjecture,
be(skc15,skc23,skc24,skc24) ).
cnf(u137,negated_conjecture,
theme(skc15,skc17,skc16) ).
cnf(u142,negated_conjecture,
agent(skc15,skc17,skc19) ).
cnf(u147,negated_conjecture,
of(skc15,skc18,skc19) ).
cnf(u152,negated_conjecture,
agent(skc16,skc22,skc21) ).
cnf(u157,negated_conjecture,
of(skc15,skc20,skc21) ).
cnf(u162,negated_conjecture,
of(skc15,skc25,skc24) ).
cnf(u167,negated_conjecture,
theme(skc15,skc27,skc26) ).
cnf(u172,negated_conjecture,
agent(skc15,skc27,skc29) ).
cnf(u177,negated_conjecture,
of(skc15,skc28,skc29) ).
cnf(u182,negated_conjecture,
proposition(skc15,skc26) ).
cnf(u187,negated_conjecture,
accessible_world(skc15,skc26) ).
cnf(u192,negated_conjecture,
state(skc15,skc23) ).
cnf(u197,negated_conjecture,
accessible_world(skc15,skc16) ).
cnf(u202,negated_conjecture,
proposition(skc15,skc16) ).
cnf(u207,negated_conjecture,
jules_forename(skc15,skc20) ).
cnf(u212,negated_conjecture,
forename(skc15,skc20) ).
cnf(u217,negated_conjecture,
vincent_forename(skc15,skc18) ).
cnf(u222,negated_conjecture,
forename(skc15,skc18) ).
cnf(u227,negated_conjecture,
event(skc15,skc17) ).
cnf(u232,negated_conjecture,
present(skc15,skc17) ).
cnf(u237,negated_conjecture,
think_believe_consider(skc15,skc17) ).
cnf(u242,negated_conjecture,
man(skc15,skc19) ).
cnf(u247,negated_conjecture,
smoke(skc16,skc22) ).
cnf(u252,negated_conjecture,
present(skc16,skc22) ).
cnf(u257,negated_conjecture,
man(skc15,skc21) ).
cnf(u262,negated_conjecture,
event(skc16,skc22) ).
cnf(u267,negated_conjecture,
man(skc15,skc24) ).
cnf(u272,negated_conjecture,
forename(skc15,skc25) ).
cnf(u277,negated_conjecture,
jules_forename(skc15,skc25) ).
cnf(u282,negated_conjecture,
think_believe_consider(skc15,skc27) ).
cnf(u287,negated_conjecture,
present(skc15,skc27) ).
cnf(u292,negated_conjecture,
event(skc15,skc27) ).
cnf(u297,negated_conjecture,
vincent_forename(skc15,skc28) ).
cnf(u302,negated_conjecture,
forename(skc15,skc28) ).
cnf(u307,negated_conjecture,
man(skc15,skc29) ).
cnf(u316,negated_conjecture,
eventuality(skc16,skc22) ).
cnf(u321,negated_conjecture,
eventuality(skc15,skc27) ).
cnf(u326,negated_conjecture,
eventuality(skc15,skc17) ).
cnf(u332,negated_conjecture,
thing(skc16,skc22) ).
cnf(u338,negated_conjecture,
thing(skc15,skc27) ).
cnf(u344,negated_conjecture,
thing(skc15,skc17) ).
cnf(u352,negated_conjecture,
specific(skc15,skc17) ).
cnf(u357,negated_conjecture,
specific(skc15,skc27) ).
cnf(u362,negated_conjecture,
specific(skc16,skc22) ).
cnf(u368,negated_conjecture,
singleton(skc16,skc22) ).
cnf(u376,negated_conjecture,
nonexistent(skc15,skc17) ).
cnf(u381,negated_conjecture,
nonexistent(skc15,skc27) ).
cnf(u386,negated_conjecture,
nonexistent(skc16,skc22) ).
cnf(u392,negated_conjecture,
singleton(skc15,skc27) ).
cnf(u400,negated_conjecture,
unisex(skc15,skc17) ).
cnf(u405,negated_conjecture,
unisex(skc15,skc27) ).
cnf(u410,negated_conjecture,
unisex(skc16,skc22) ).
cnf(u416,negated_conjecture,
singleton(skc15,skc17) ).
cnf(u423,negated_conjecture,
relation(skc15,skc16) ).
cnf(u428,negated_conjecture,
relation(skc15,skc26) ).
cnf(u434,negated_conjecture,
abstraction(skc15,skc16) ).
cnf(u440,negated_conjecture,
abstraction(skc15,skc26) ).
cnf(u446,negated_conjecture,
eventuality(skc15,skc23) ).
cnf(u455,negated_conjecture,
thing(skc15,skc23) ).
cnf(u460,negated_conjecture,
specific(skc15,skc23) ).
cnf(u465,negated_conjecture,
nonexistent(skc15,skc23) ).
cnf(u470,negated_conjecture,
unisex(skc15,skc23) ).
cnf(u476,negated_conjecture,
event(skc15,skc23) ).
cnf(u486,negated_conjecture,
human_person(skc15,skc19) ).
cnf(u491,negated_conjecture,
human_person(skc15,skc21) ).
cnf(u496,negated_conjecture,
human_person(skc15,skc24) ).
cnf(u501,negated_conjecture,
human_person(skc15,skc29) ).
cnf(u507,negated_conjecture,
organism(skc15,skc19) ).
cnf(u513,negated_conjecture,
organism(skc15,skc21) ).
cnf(u519,negated_conjecture,
organism(skc15,skc24) ).
cnf(u525,negated_conjecture,
organism(skc15,skc29) ).
cnf(u534,negated_conjecture,
human(skc15,skc19) ).
cnf(u539,negated_conjecture,
human(skc15,skc21) ).
cnf(u544,negated_conjecture,
human(skc15,skc24) ).
cnf(u549,negated_conjecture,
human(skc15,skc29) ).
cnf(u558,negated_conjecture,
animate(skc15,skc19) ).
cnf(u563,negated_conjecture,
animate(skc15,skc21) ).
cnf(u568,negated_conjecture,
animate(skc15,skc24) ).
cnf(u573,negated_conjecture,
animate(skc15,skc29) ).
cnf(u582,negated_conjecture,
thing(skc15,skc16) ).
cnf(u587,negated_conjecture,
nonhuman(skc15,skc16) ).
cnf(u592,negated_conjecture,
general(skc15,skc16) ).
cnf(u597,negated_conjecture,
unisex(skc15,skc16) ).
cnf(u606,negated_conjecture,
male(skc15,skc19) ).
cnf(u611,negated_conjecture,
male(skc15,skc21) ).
cnf(u616,negated_conjecture,
male(skc15,skc24) ).
cnf(u621,negated_conjecture,
male(skc15,skc29) ).
cnf(u630,negated_conjecture,
relname(skc15,skc20) ).
cnf(u635,negated_conjecture,
relname(skc15,skc18) ).
cnf(u640,negated_conjecture,
relname(skc15,skc25) ).
cnf(u645,negated_conjecture,
relname(skc15,skc28) ).
cnf(u655,negated_conjecture,
relation(skc15,skc20) ).
cnf(u664,negated_conjecture,
~ unisex(skc15,skc19) ).
cnf(u669,negated_conjecture,
~ unisex(skc15,skc21) ).
cnf(u674,negated_conjecture,
~ unisex(skc15,skc24) ).
cnf(u679,negated_conjecture,
~ unisex(skc15,skc29) ).
cnf(u685,negated_conjecture,
relation(skc15,skc18) ).
cnf(u691,negated_conjecture,
relation(skc15,skc25) ).
cnf(u697,negated_conjecture,
relation(skc15,skc28) ).
cnf(u706,negated_conjecture,
thing(skc15,skc26) ).
cnf(u711,negated_conjecture,
nonhuman(skc15,skc26) ).
cnf(u716,negated_conjecture,
general(skc15,skc26) ).
cnf(u721,negated_conjecture,
unisex(skc15,skc26) ).
cnf(u728,negated_conjecture,
singleton(skc15,skc23) ).
cnf(u744,negated_conjecture,
entity(skc15,skc19) ).
cnf(u749,negated_conjecture,
impartial(skc15,skc19) ).
cnf(u754,negated_conjecture,
living(skc15,skc19) ).
cnf(u764,negated_conjecture,
entity(skc15,skc21) ).
cnf(u769,negated_conjecture,
impartial(skc15,skc21) ).
cnf(u774,negated_conjecture,
living(skc15,skc21) ).
cnf(u784,negated_conjecture,
entity(skc15,skc24) ).
cnf(u789,negated_conjecture,
impartial(skc15,skc24) ).
cnf(u794,negated_conjecture,
living(skc15,skc24) ).
cnf(u804,negated_conjecture,
entity(skc15,skc29) ).
cnf(u809,negated_conjecture,
impartial(skc15,skc29) ).
cnf(u814,negated_conjecture,
living(skc15,skc29) ).
cnf(u822,negated_conjecture,
~ nonhuman(skc15,skc19) ).
cnf(u831,negated_conjecture,
~ nonhuman(skc15,skc21) ).
cnf(u839,negated_conjecture,
~ nonhuman(skc15,skc24) ).
cnf(u847,negated_conjecture,
~ nonhuman(skc15,skc29) ).
cnf(u863,negated_conjecture,
abstraction(skc15,skc20) ).
cnf(u887,negated_conjecture,
abstraction(skc15,skc18) ).
cnf(u895,negated_conjecture,
abstraction(skc15,skc25) ).
cnf(u903,negated_conjecture,
abstraction(skc15,skc28) ).
cnf(u917,negated_conjecture,
singleton(skc15,skc16) ).
cnf(u927,negated_conjecture,
~ specific(skc15,skc16) ).
cnf(u937,negated_conjecture,
singleton(skc15,skc26) ).
cnf(u949,negated_conjecture,
~ specific(skc15,skc26) ).
cnf(u964,negated_conjecture,
thing(skc15,skc19) ).
cnf(u969,negated_conjecture,
specific(skc15,skc19) ).
cnf(u974,negated_conjecture,
existent(skc15,skc19) ).
cnf(u1004,negated_conjecture,
thing(skc15,skc21) ).
cnf(u1009,negated_conjecture,
specific(skc15,skc21) ).
cnf(u1014,negated_conjecture,
existent(skc15,skc21) ).
cnf(u1022,negated_conjecture,
event(skc26,skc23) ).
cnf(u1027,negated_conjecture,
event(skc26,skc27) ).
cnf(u1032,negated_conjecture,
event(skc26,skc17) ).
cnf(u1038,negated_conjecture,
eventuality(skc26,skc23) ).
cnf(u1046,negated_conjecture,
event(skc16,skc23) ).
cnf(u1051,negated_conjecture,
event(skc16,skc27) ).
cnf(u1056,negated_conjecture,
event(skc16,skc17) ).
cnf(u1062,negated_conjecture,
eventuality(skc26,skc27) ).
cnf(u1070,negated_conjecture,
eventuality(skc26,skc17) ).
cnf(u1079,negated_conjecture,
eventuality(skc16,skc23) ).
cnf(u1084,negated_conjecture,
eventuality(skc16,skc17) ).
cnf(u1089,negated_conjecture,
eventuality(skc16,skc27) ).
cnf(u1100,negated_conjecture,
thing(skc26,skc26) ).
cnf(u1105,negated_conjecture,
thing(skc26,skc23) ).
cnf(u1110,negated_conjecture,
thing(skc26,skc17) ).
cnf(u1115,negated_conjecture,
thing(skc26,skc16) ).
cnf(u1120,negated_conjecture,
thing(skc26,skc27) ).
cnf(u1131,negated_conjecture,
thing(skc16,skc26) ).
cnf(u1136,negated_conjecture,
thing(skc16,skc23) ).
cnf(u1141,negated_conjecture,
thing(skc16,skc17) ).
cnf(u1146,negated_conjecture,
thing(skc16,skc16) ).
cnf(u1151,negated_conjecture,
thing(skc16,skc27) ).
cnf(u1160,negated_conjecture,
singleton(skc26,skc23) ).
cnf(u1165,negated_conjecture,
singleton(skc26,skc17) ).
cnf(u1170,negated_conjecture,
singleton(skc26,skc27) ).
cnf(u1179,negated_conjecture,
specific(skc26,skc17) ).
cnf(u1184,negated_conjecture,
nonexistent(skc26,skc17) ).
cnf(u1189,negated_conjecture,
unisex(skc26,skc17) ).
cnf(u1197,negated_conjecture,
singleton(skc16,skc23) ).
cnf(u1202,negated_conjecture,
singleton(skc16,skc17) ).
cnf(u1207,negated_conjecture,
singleton(skc16,skc27) ).
cnf(u1216,negated_conjecture,
specific(skc16,skc23) ).
cnf(u1221,negated_conjecture,
nonexistent(skc16,skc23) ).
cnf(u1226,negated_conjecture,
unisex(skc16,skc23) ).
cnf(u1234,negated_conjecture,
specific(skc26,skc23) ).
cnf(u1239,negated_conjecture,
specific(skc26,skc27) ).
cnf(u1248,negated_conjecture,
specific(skc16,skc17) ).
cnf(u1253,negated_conjecture,
nonexistent(skc16,skc17) ).
cnf(u1258,negated_conjecture,
unisex(skc16,skc17) ).
cnf(u1266,negated_conjecture,
specific(skc16,skc27) ).
cnf(u1275,negated_conjecture,
nonexistent(skc16,skc27) ).
cnf(u1280,negated_conjecture,
unisex(skc16,skc27) ).
cnf(u1288,negated_conjecture,
nonexistent(skc26,skc23) ).
cnf(u1293,negated_conjecture,
nonexistent(skc26,skc27) ).
cnf(u1301,negated_conjecture,
thing(skc15,skc24) ).
cnf(u1306,negated_conjecture,
specific(skc15,skc24) ).
cnf(u1311,negated_conjecture,
existent(skc15,skc24) ).
cnf(u1324,negated_conjecture,
unisex(skc26,skc26) ).
cnf(u1329,negated_conjecture,
unisex(skc26,skc23) ).
cnf(u1334,negated_conjecture,
unisex(skc26,skc16) ).
cnf(u1339,negated_conjecture,
unisex(skc26,skc27) ).
cnf(u1349,negated_conjecture,
unisex(skc16,skc26) ).
cnf(u1354,negated_conjecture,
unisex(skc16,skc16) ).
cnf(u1362,negated_conjecture,
thing(skc15,skc29) ).
cnf(u1367,negated_conjecture,
specific(skc15,skc29) ).
cnf(u1372,negated_conjecture,
existent(skc15,skc29) ).
cnf(u1379,negated_conjecture,
present(skc16,skc17) ).
cnf(u1384,negated_conjecture,
present(skc26,skc17) ).
cnf(u1392,negated_conjecture,
present(skc16,skc27) ).
cnf(u1397,negated_conjecture,
present(skc26,skc27) ).
cnf(u1406,negated_conjecture,
think_believe_consider(skc16,skc17) ).
cnf(u1411,negated_conjecture,
think_believe_consider(skc26,skc17) ).
cnf(u1419,negated_conjecture,
think_believe_consider(skc16,skc27) ).
cnf(u1424,negated_conjecture,
think_believe_consider(skc26,skc27) ).
cnf(u1432,negated_conjecture,
proposition(skc26,skc16) ).
cnf(u1437,negated_conjecture,
proposition(skc26,skc26) ).
cnf(u1445,negated_conjecture,
proposition(skc16,skc16) ).
cnf(u1450,negated_conjecture,
proposition(skc16,skc26) ).
cnf(u1462,negated_conjecture,
relation(skc26,skc26) ).
cnf(u1467,negated_conjecture,
relation(skc26,skc20) ).
cnf(u1472,negated_conjecture,
relation(skc26,skc18) ).
cnf(u1477,negated_conjecture,
relation(skc26,skc16) ).
cnf(u1482,negated_conjecture,
relation(skc26,skc25) ).
cnf(u1487,negated_conjecture,
relation(skc26,skc28) ).
cnf(u1499,negated_conjecture,
relation(skc16,skc26) ).
cnf(u1504,negated_conjecture,
relation(skc16,skc20) ).
cnf(u1509,negated_conjecture,
relation(skc16,skc18) ).
cnf(u1514,negated_conjecture,
relation(skc16,skc16) ).
cnf(u1519,negated_conjecture,
relation(skc16,skc25) ).
cnf(u1524,negated_conjecture,
relation(skc16,skc28) ).
cnf(u1532,negated_conjecture,
abstraction(skc26,skc26) ).
cnf(u1537,negated_conjecture,
abstraction(skc26,skc16) ).
cnf(u1545,negated_conjecture,
abstraction(skc16,skc26) ).
cnf(u1550,negated_conjecture,
abstraction(skc16,skc16) ).
cnf(u1558,negated_conjecture,
nonhuman(skc26,skc26) ).
cnf(u1563,negated_conjecture,
nonhuman(skc26,skc16) ).
cnf(u1571,negated_conjecture,
nonhuman(skc16,skc26) ).
cnf(u1576,negated_conjecture,
nonhuman(skc16,skc16) ).
cnf(u1584,negated_conjecture,
general(skc26,skc26) ).
cnf(u1589,negated_conjecture,
general(skc26,skc16) ).
cnf(u1597,negated_conjecture,
general(skc16,skc26) ).
cnf(u1602,negated_conjecture,
general(skc16,skc16) ).
cnf(u1609,negated_conjecture,
state(skc26,skc23) ).
cnf(u1616,negated_conjecture,
state(skc16,skc23) ).
cnf(u1627,negated_conjecture,
man(skc26,skc19) ).
cnf(u1632,negated_conjecture,
man(skc26,skc21) ).
cnf(u1637,negated_conjecture,
man(skc26,skc24) ).
cnf(u1642,negated_conjecture,
man(skc26,skc29) ).
cnf(u1653,negated_conjecture,
man(skc16,skc19) ).
cnf(u1658,negated_conjecture,
man(skc16,skc21) ).
cnf(u1663,negated_conjecture,
man(skc16,skc24) ).
cnf(u1668,negated_conjecture,
man(skc16,skc29) ).
cnf(u1675,negated_conjecture,
human_person(skc26,skc19) ).
cnf(u1680,negated_conjecture,
male(skc26,skc19) ).
cnf(u1689,negated_conjecture,
human_person(skc26,skc21) ).
cnf(u1694,negated_conjecture,
human_person(skc26,skc24) ).
cnf(u1699,negated_conjecture,
human_person(skc26,skc29) ).
cnf(u1706,negated_conjecture,
male(skc26,skc21) ).
cnf(u1715,negated_conjecture,
human_person(skc16,skc19) ).
cnf(u1720,negated_conjecture,
human_person(skc16,skc21) ).
cnf(u1725,negated_conjecture,
human_person(skc16,skc24) ).
cnf(u1730,negated_conjecture,
human_person(skc16,skc29) ).
cnf(u1737,negated_conjecture,
male(skc26,skc24) ).
cnf(u1746,negated_conjecture,
organism(skc26,skc19) ).
cnf(u1751,negated_conjecture,
organism(skc26,skc21) ).
cnf(u1756,negated_conjecture,
organism(skc26,skc24) ).
cnf(u1761,negated_conjecture,
organism(skc26,skc29) ).
cnf(u1768,negated_conjecture,
male(skc26,skc29) ).
cnf(u1777,negated_conjecture,
organism(skc16,skc19) ).
cnf(u1782,negated_conjecture,
organism(skc16,skc21) ).
cnf(u1787,negated_conjecture,
organism(skc16,skc24) ).
cnf(u1792,negated_conjecture,
organism(skc16,skc29) ).
cnf(u1799,negated_conjecture,
male(skc16,skc19) ).
cnf(u1808,negated_conjecture,
entity(skc26,skc19) ).
cnf(u1813,negated_conjecture,
entity(skc26,skc21) ).
cnf(u1818,negated_conjecture,
entity(skc26,skc24) ).
cnf(u1823,negated_conjecture,
entity(skc26,skc29) ).
cnf(u1830,negated_conjecture,
male(skc16,skc21) ).
cnf(u1839,negated_conjecture,
entity(skc16,skc19) ).
cnf(u1844,negated_conjecture,
entity(skc16,skc21) ).
cnf(u1849,negated_conjecture,
entity(skc16,skc24) ).
cnf(u1854,negated_conjecture,
entity(skc16,skc29) ).
cnf(u1861,negated_conjecture,
male(skc16,skc24) ).
cnf(u1868,negated_conjecture,
male(skc16,skc29) ).
cnf(u1876,negated_conjecture,
human(skc26,skc21) ).
cnf(u1881,negated_conjecture,
animate(skc26,skc21) ).
cnf(u1889,negated_conjecture,
impartial(skc26,skc24) ).
cnf(u1894,negated_conjecture,
impartial(skc26,skc21) ).
cnf(u1899,negated_conjecture,
impartial(skc26,skc19) ).
cnf(u1907,negated_conjecture,
human(skc26,skc24) ).
cnf(u1912,negated_conjecture,
animate(skc26,skc24) ).
cnf(u1920,negated_conjecture,
impartial(skc16,skc24) ).
cnf(u1925,negated_conjecture,
impartial(skc16,skc21) ).
cnf(u1930,negated_conjecture,
impartial(skc16,skc19) ).
cnf(u1938,negated_conjecture,
human(skc26,skc29) ).
cnf(u1943,negated_conjecture,
animate(skc26,skc29) ).
cnf(u1951,negated_conjecture,
living(skc26,skc24) ).
cnf(u1956,negated_conjecture,
living(skc26,skc21) ).
cnf(u1961,negated_conjecture,
living(skc26,skc19) ).
cnf(u1969,negated_conjecture,
human(skc16,skc19) ).
cnf(u1974,negated_conjecture,
animate(skc16,skc19) ).
cnf(u1982,negated_conjecture,
living(skc16,skc24) ).
cnf(u1987,negated_conjecture,
living(skc16,skc21) ).
cnf(u1992,negated_conjecture,
living(skc16,skc19) ).
cnf(u2000,negated_conjecture,
human(skc16,skc21) ).
cnf(u2005,negated_conjecture,
animate(skc16,skc21) ).
cnf(u2014,negated_conjecture,
human(skc26,skc19) ).
cnf(u2022,negated_conjecture,
human(skc16,skc24) ).
cnf(u2027,negated_conjecture,
animate(skc16,skc24) ).
cnf(u2036,negated_conjecture,
human(skc16,skc29) ).
cnf(u2044,negated_conjecture,
animate(skc16,skc29) ).
cnf(u2053,negated_conjecture,
animate(skc26,skc19) ).
cnf(u2060,negated_conjecture,
impartial(skc26,skc29) ).
cnf(u2065,negated_conjecture,
impartial(skc16,skc29) ).
cnf(u2076,negated_conjecture,
living(skc26,skc29) ).
cnf(u2081,negated_conjecture,
living(skc16,skc29) ).
cnf(u2098,negated_conjecture,
forename(skc26,skc20) ).
cnf(u2103,negated_conjecture,
forename(skc26,skc18) ).
cnf(u2108,negated_conjecture,
forename(skc26,skc25) ).
cnf(u2113,negated_conjecture,
forename(skc26,skc28) ).
cnf(u2119,negated_conjecture,
relname(skc26,skc20) ).
cnf(u2128,negated_conjecture,
forename(skc16,skc20) ).
cnf(u2133,negated_conjecture,
forename(skc16,skc18) ).
cnf(u2138,negated_conjecture,
forename(skc16,skc25) ).
cnf(u2143,negated_conjecture,
forename(skc16,skc28) ).
cnf(u2149,negated_conjecture,
relname(skc26,skc18) ).
cnf(u2158,negated_conjecture,
relname(skc26,skc25) ).
cnf(u2163,negated_conjecture,
relname(skc26,skc28) ).
cnf(u2173,negated_conjecture,
relname(skc16,skc20) ).
cnf(u2178,negated_conjecture,
relname(skc16,skc18) ).
cnf(u2183,negated_conjecture,
relname(skc16,skc25) ).
cnf(u2188,negated_conjecture,
relname(skc16,skc28) ).
cnf(u2196,negated_conjecture,
vincent_forename(skc26,skc28) ).
cnf(u2201,negated_conjecture,
vincent_forename(skc26,skc18) ).
cnf(u2209,negated_conjecture,
vincent_forename(skc16,skc28) ).
cnf(u2214,negated_conjecture,
vincent_forename(skc16,skc18) ).
cnf(u2222,negated_conjecture,
jules_forename(skc26,skc25) ).
cnf(u2227,negated_conjecture,
jules_forename(skc26,skc20) ).
cnf(u2235,negated_conjecture,
jules_forename(skc16,skc25) ).
cnf(u2240,negated_conjecture,
jules_forename(skc16,skc20) ).
cnf(u2303,negated_conjecture,
skc16 = skc26 ).
cnf(u2370,negated_conjecture,
unisex(skc26,skc22) ).
cnf(u2375,negated_conjecture,
nonexistent(skc26,skc22) ).
cnf(u2380,negated_conjecture,
singleton(skc26,skc22) ).
cnf(u2385,negated_conjecture,
specific(skc26,skc22) ).
cnf(u2390,negated_conjecture,
thing(skc26,skc22) ).
cnf(u2395,negated_conjecture,
eventuality(skc26,skc22) ).
cnf(u2400,negated_conjecture,
event(skc26,skc22) ).
cnf(u2405,negated_conjecture,
present(skc26,skc22) ).
cnf(u2410,negated_conjecture,
smoke(skc26,skc22) ).
cnf(u2415,negated_conjecture,
agent(skc26,skc22,skc21) ).
cnf(u2420,negated_conjecture,
theme(skc15,skc17,skc26) ).
cnf(u2437,negated_conjecture,
thing(skc15,skc20) ).
cnf(u2442,negated_conjecture,
nonhuman(skc15,skc20) ).
cnf(u2447,negated_conjecture,
general(skc15,skc20) ).
cnf(u2452,negated_conjecture,
unisex(skc15,skc20) ).
cnf(u2457,negated_conjecture,
abstraction(skc26,skc20) ).
cnf(u2470,negated_conjecture,
thing(skc15,skc18) ).
cnf(u2475,negated_conjecture,
nonhuman(skc15,skc18) ).
cnf(u2480,negated_conjecture,
general(skc15,skc18) ).
cnf(u2485,negated_conjecture,
unisex(skc15,skc18) ).
cnf(u2490,negated_conjecture,
abstraction(skc26,skc18) ).
cnf(u2503,negated_conjecture,
thing(skc15,skc25) ).
cnf(u2508,negated_conjecture,
nonhuman(skc15,skc25) ).
cnf(u2513,negated_conjecture,
general(skc15,skc25) ).
cnf(u2518,negated_conjecture,
unisex(skc15,skc25) ).
cnf(u2523,negated_conjecture,
abstraction(skc26,skc25) ).
cnf(u2536,negated_conjecture,
thing(skc15,skc28) ).
cnf(u2541,negated_conjecture,
nonhuman(skc15,skc28) ).
cnf(u2546,negated_conjecture,
general(skc15,skc28) ).
cnf(u2551,negated_conjecture,
unisex(skc15,skc28) ).
cnf(u2556,negated_conjecture,
abstraction(skc26,skc28) ).
cnf(u2691,negated_conjecture,
~ unisex(skc26,skc19) ).
cnf(u2697,negated_conjecture,
~ unisex(skc26,skc21) ).
cnf(u2703,negated_conjecture,
~ unisex(skc26,skc24) ).
cnf(u2721,negated_conjecture,
~ unisex(skc26,skc29) ).
cnf(u2755,negated_conjecture,
~ nonhuman(skc26,skc21) ).
cnf(u2761,negated_conjecture,
~ nonhuman(skc26,skc24) ).
cnf(u2767,negated_conjecture,
~ nonhuman(skc26,skc29) ).
cnf(u2775,negated_conjecture,
~ nonhuman(skc26,skc19) ).
cnf(u2810,negated_conjecture,
singleton(skc26,skc26) ).
cnf(u2836,negated_conjecture,
singleton(skc15,skc19) ).
cnf(u2841,negated_conjecture,
thing(skc26,skc19) ).
cnf(u2851,negated_conjecture,
specific(skc26,skc19) ).
cnf(u2861,negated_conjecture,
~ nonexistent(skc15,skc19) ).
cnf(u2866,negated_conjecture,
existent(skc26,skc19) ).
cnf(u2877,negated_conjecture,
singleton(skc15,skc21) ).
cnf(u2882,negated_conjecture,
thing(skc26,skc21) ).
cnf(u2891,negated_conjecture,
specific(skc26,skc21) ).
cnf(u2902,negated_conjecture,
~ nonexistent(skc15,skc21) ).
cnf(u2907,negated_conjecture,
existent(skc26,skc21) ).
cnf(u2982,negated_conjecture,
singleton(skc15,skc24) ).
cnf(u2987,negated_conjecture,
thing(skc26,skc24) ).
cnf(u2998,negated_conjecture,
specific(skc26,skc24) ).
cnf(u3008,negated_conjecture,
~ nonexistent(skc15,skc24) ).
cnf(u3013,negated_conjecture,
existent(skc26,skc24) ).
cnf(u3026,negated_conjecture,
singleton(skc15,skc29) ).
cnf(u3031,negated_conjecture,
thing(skc26,skc29) ).
cnf(u3040,negated_conjecture,
specific(skc26,skc29) ).
cnf(u3050,negated_conjecture,
~ nonexistent(skc15,skc29) ).
cnf(u3055,negated_conjecture,
existent(skc26,skc29) ).
cnf(u3066,negated_conjecture,
~ specific(skc26,skc26) ).
cnf(u3131,negated_conjecture,
singleton(skc15,skc20) ).
cnf(u3136,negated_conjecture,
thing(skc26,skc20) ).
cnf(u3145,negated_conjecture,
nonhuman(skc26,skc20) ).
cnf(u3155,negated_conjecture,
~ specific(skc15,skc20) ).
cnf(u3160,negated_conjecture,
general(skc26,skc20) ).
cnf(u3169,negated_conjecture,
unisex(skc26,skc20) ).
cnf(u3183,negated_conjecture,
singleton(skc15,skc18) ).
cnf(u3188,negated_conjecture,
thing(skc26,skc18) ).
cnf(u3197,negated_conjecture,
nonhuman(skc26,skc18) ).
cnf(u3207,negated_conjecture,
~ specific(skc15,skc18) ).
cnf(u3212,negated_conjecture,
general(skc26,skc18) ).
cnf(u3221,negated_conjecture,
unisex(skc26,skc18) ).
cnf(u3235,negated_conjecture,
singleton(skc15,skc25) ).
cnf(u3240,negated_conjecture,
thing(skc26,skc25) ).
cnf(u3249,negated_conjecture,
nonhuman(skc26,skc25) ).
cnf(u3259,negated_conjecture,
~ specific(skc15,skc25) ).
cnf(u3264,negated_conjecture,
general(skc26,skc25) ).
cnf(u3273,negated_conjecture,
unisex(skc26,skc25) ).
cnf(u3287,negated_conjecture,
singleton(skc15,skc28) ).
cnf(u3292,negated_conjecture,
thing(skc26,skc28) ).
cnf(u3301,negated_conjecture,
nonhuman(skc26,skc28) ).
cnf(u3311,negated_conjecture,
~ specific(skc15,skc28) ).
cnf(u3316,negated_conjecture,
general(skc26,skc28) ).
cnf(u3325,negated_conjecture,
unisex(skc26,skc28) ).
cnf(u3342,negated_conjecture,
singleton(skc26,skc19) ).
cnf(u3351,negated_conjecture,
~ nonexistent(skc26,skc19) ).
cnf(u3358,negated_conjecture,
singleton(skc26,skc21) ).
cnf(u3367,negated_conjecture,
~ nonexistent(skc26,skc21) ).
cnf(u3380,negated_conjecture,
singleton(skc26,skc24) ).
cnf(u3420,negated_conjecture,
~ nonexistent(skc26,skc24) ).
cnf(u3444,negated_conjecture,
singleton(skc26,skc29) ).
cnf(u3483,negated_conjecture,
~ nonexistent(skc26,skc29) ).
cnf(u3490,negated_conjecture,
singleton(skc26,skc20) ).
cnf(u3499,negated_conjecture,
~ specific(skc26,skc20) ).
cnf(u3506,negated_conjecture,
singleton(skc26,skc18) ).
cnf(u3515,negated_conjecture,
~ specific(skc26,skc18) ).
cnf(u3522,negated_conjecture,
singleton(skc26,skc25) ).
cnf(u3531,negated_conjecture,
~ specific(skc26,skc25) ).
cnf(u3538,negated_conjecture,
singleton(skc26,skc28) ).
cnf(u3547,negated_conjecture,
~ specific(skc26,skc28) ).
cnf(u730,negated_conjecture,
( ~ smoke(skc15,X0)
| smoke(skc26,X0) ) ).
cnf(u857,negated_conjecture,
( ~ state(skc15,X0)
| state(skc26,X0) ) ).
cnf(u890,negated_conjecture,
( ~ entity(skc15,X0)
| entity(skc16,X0) ) ).
cnf(clause56,axiom,
( ~ accessible_world(X0,X1)
| ~ existent(X0,X2)
| existent(X1,X2) ) ).
cnf(u996,negated_conjecture,
specific(skc26,skf1(X0)) ).
cnf(clause63,axiom,
( ~ accessible_world(X0,X1)
| ~ relname(X0,X2)
| relname(X1,X2) ) ).
cnf(clause50,axiom,
( ~ accessible_world(X0,X1)
| ~ general(X0,X2)
| general(X1,X2) ) ).
cnf(u952,negated_conjecture,
( theme(X0,skc27,skc26)
| ~ accessible_world(skc15,X0) ) ).
cnf(u2973,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc20,skc21) ) ).
cnf(u833,negated_conjecture,
( ~ accessible_world(skc15,X0)
| think_believe_consider(X0,skc17) ) ).
cnf(u2285,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ man(skc26,X1)
| ~ accessible_world(X0,X2)
| agent(X2,skf1(X1),X1) ) ).
cnf(u776,negated_conjecture,
( ~ specific(skc15,X0)
| specific(skc26,X0) ) ).
cnf(u957,negated_conjecture,
( be(X0,skc23,skc24,skc24)
| ~ accessible_world(skc15,X0) ) ).
cnf(u731,negated_conjecture,
( ~ smoke(skc15,X0)
| smoke(skc16,X0) ) ).
cnf(u2253,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc16)
| ~ accessible_world(skc15,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc17,X3)
| ~ agent(X0,X1,X3)
| skc16 = X2 ) ).
cnf(u2328,negated_conjecture,
( ~ accessible_world(skc26,X0)
| present(X0,skc22) ) ).
cnf(u879,negated_conjecture,
( ~ human_person(skc15,X0)
| human_person(skc26,X0) ) ).
cnf(u855,negated_conjecture,
( ~ general(skc15,X0)
| general(skc26,X0) ) ).
cnf(u880,negated_conjecture,
( ~ human_person(skc15,X0)
| human_person(skc16,X0) ) ).
cnf(clause25,axiom,
( ~ human_person(X0,X1)
| animate(X0,X1) ) ).
cnf(clause43,axiom,
( ~ accessible_world(X0,X1)
| ~ unisex(X0,X2)
| unisex(X1,X2) ) ).
cnf(u841,negated_conjecture,
( ~ proposition(skc15,X0)
| proposition(skc26,X0) ) ).
cnf(u2591,negated_conjecture,
( of(X0,skc28,skc29)
| ~ accessible_world(skc26,X0) ) ).
cnf(u876,negated_conjecture,
eventuality(skc26,skf1(X0)) ).
cnf(u987,negated_conjecture,
( ~ of(skc15,X0,skc29)
| ~ forename(skc15,X0)
| skc28 = X0 ) ).
cnf(clause22,axiom,
( ~ organism(X0,X1)
| impartial(X0,X1) ) ).
cnf(clause49,axiom,
( ~ accessible_world(X0,X1)
| ~ nonhuman(X0,X2)
| nonhuman(X1,X2) ) ).
cnf(clause52,axiom,
( ~ accessible_world(X0,X1)
| ~ man(X0,X2)
| man(X1,X2) ) ).
cnf(u2560,negated_conjecture,
singleton(skc26,skf1(X0)) ).
cnf(u910,negated_conjecture,
( ~ human(skc15,X0)
| human(skc16,X0) ) ).
cnf(u939,negated_conjecture,
( ~ jules_forename(skc15,X0)
| jules_forename(skc26,X0) ) ).
cnf(clause46,axiom,
( ~ accessible_world(X0,X1)
| ~ proposition(X0,X2)
| proposition(X1,X2) ) ).
cnf(u866,negated_conjecture,
( ~ man(skc15,X0)
| man(skc16,X0) ) ).
cnf(clause45,axiom,
( ~ think_believe_consider(X0,X2)
| ~ accessible_world(X0,X1)
| think_believe_consider(X1,X2) ) ).
cnf(clause67,axiom,
( ~ theme(X0,X2,X3)
| ~ accessible_world(X0,X1)
| theme(X1,X2,X3) ) ).
cnf(clause32,axiom,
( ~ general(X0,X1)
| ~ specific(X0,X1) ) ).
cnf(u985,negated_conjecture,
( ~ of(skc15,X0,skc19)
| ~ forename(skc15,X0)
| skc18 = X0 ) ).
cnf(clause39,axiom,
( ~ accessible_world(X0,X1)
| ~ thing(X0,X2)
| thing(X1,X2) ) ).
cnf(clause69,axiom,
( ~ be(X0,X2,X3,X4)
| ~ accessible_world(X0,X1)
| be(X1,X2,X3,X4) ) ).
cnf(clause26,axiom,
( ~ man(X0,X1)
| male(X0,X1) ) ).
cnf(clause28,axiom,
( ~ relname(X0,X1)
| relation(X0,X1) ) ).
cnf(clause19,axiom,
( ~ entity(X0,X1)
| thing(X0,X1) ) ).
cnf(clause8,axiom,
( ~ proposition(X0,X1)
| relation(X0,X1) ) ).
cnf(u842,negated_conjecture,
( ~ proposition(skc15,X0)
| proposition(skc16,X0) ) ).
cnf(clause21,axiom,
( ~ entity(X0,X1)
| existent(X0,X1) ) ).
cnf(u1452,negated_conjecture,
( ~ accessible_world(skc16,X0)
| think_believe_consider(X0,skc27) ) ).
cnf(clause15,axiom,
( ~ state(X0,X1)
| event(X0,X1) ) ).
cnf(clause2,axiom,
( ~ event(X0,X1)
| eventuality(X0,X1) ) ).
cnf(clause1,axiom,
( ~ smoke(X0,X1)
| event(X0,X1) ) ).
cnf(u2961,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc25,skc24) ) ).
cnf(u856,negated_conjecture,
( ~ general(skc15,X0)
| general(skc16,X0) ) ).
cnf(u2262,negated_conjecture,
( ~ of(X0,X1,skc24)
| ~ forename(X0,X1)
| ~ forename(X0,skc25)
| ~ accessible_world(skc15,X0)
| ~ entity(X0,skc24)
| skc25 = X1 ) ).
cnf(u909,negated_conjecture,
( ~ human(skc15,X0)
| human(skc26,X0) ) ).
cnf(u2929,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc17,skc19) ) ).
cnf(u2582,negated_conjecture,
( theme(X0,skc17,skc26)
| ~ accessible_world(skc26,X0) ) ).
cnf(u2602,negated_conjecture,
( of(X0,skc20,skc21)
| ~ accessible_world(skc26,X0) ) ).
cnf(u2967,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc18,skc19) ) ).
cnf(u2954,negated_conjecture,
( ~ of(X0,X1,skc29)
| ~ forename(X0,X1)
| ~ forename(X0,skc28)
| ~ accessible_world(skc26,X0)
| ~ entity(X0,skc29)
| skc28 = X1 ) ).
cnf(u2925,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc26)
| ~ accessible_world(skc15,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc17,X3)
| ~ agent(X0,X1,X3)
| skc26 = X2 ) ).
cnf(u817,negated_conjecture,
( ~ unisex(skc15,X0)
| unisex(skc16,X0) ) ).
cnf(u984,negated_conjecture,
( ~ of(skc15,X0,skc21)
| ~ forename(skc15,X0)
| skc20 = X0 ) ).
cnf(u2947,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc27,skc26) ) ).
cnf(u2247,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc27,skc29) ) ).
cnf(u2266,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc18,skc19) ) ).
cnf(u994,negated_conjecture,
unisex(skc26,skf1(X0)) ).
cnf(u911,negated_conjecture,
( ~ animate(skc15,X0)
| animate(skc26,X0) ) ).
cnf(clause58,axiom,
( ~ accessible_world(X0,X1)
| ~ living(X0,X2)
| living(X1,X2) ) ).
cnf(clause4,axiom,
( ~ thing(X0,X1)
| singleton(X0,X1) ) ).
cnf(u757,negated_conjecture,
( ~ singleton(skc15,X0)
| singleton(skc16,X0) ) ).
cnf(u889,negated_conjecture,
( ~ entity(skc15,X0)
| entity(skc26,X0) ) ).
cnf(u853,negated_conjecture,
( ~ nonhuman(skc15,X0)
| nonhuman(skc26,X0) ) ).
cnf(u942,negated_conjecture,
( agent(X0,skc27,skc29)
| ~ accessible_world(skc15,X0) ) ).
cnf(u956,negated_conjecture,
( of(X0,skc20,skc21)
| ~ accessible_world(skc15,X0) ) ).
cnf(u737,negated_conjecture,
( ~ thing(skc15,X0)
| thing(skc16,X0) ) ).
cnf(u2599,negated_conjecture,
( of(X0,skc18,skc19)
| ~ accessible_world(skc26,X0) ) ).
cnf(u733,negated_conjecture,
( ~ event(skc15,X0)
| event(skc16,X0) ) ).
cnf(clause57,axiom,
( ~ accessible_world(X0,X1)
| ~ impartial(X0,X2)
| impartial(X1,X2) ) ).
cnf(clause60,axiom,
( ~ accessible_world(X0,X1)
| ~ animate(X0,X2)
| animate(X1,X2) ) ).
cnf(u2596,negated_conjecture,
( of(X0,skc25,skc24)
| ~ accessible_world(skc26,X0) ) ).
cnf(clause51,axiom,
( ~ accessible_world(X0,X1)
| ~ state(X0,X2)
| state(X1,X2) ) ).
cnf(clause54,axiom,
( ~ accessible_world(X0,X1)
| ~ organism(X0,X2)
| organism(X1,X2) ) ).
cnf(clause53,axiom,
( ~ accessible_world(X0,X1)
| ~ human_person(X0,X2)
| human_person(X1,X2) ) ).
cnf(u865,negated_conjecture,
( ~ man(skc15,X0)
| man(skc26,X0) ) ).
cnf(clause40,axiom,
( ~ accessible_world(X0,X1)
| ~ singleton(X0,X2)
| singleton(X1,X2) ) ).
cnf(u993,negated_conjecture,
( ~ theme(skc15,X0,X1)
| ~ think_believe_consider(skc15,X0)
| ~ proposition(skc15,X1)
| ~ agent(skc15,skc17,X2)
| ~ agent(skc15,X0,X2)
| skc16 = X1 ) ).
cnf(clause47,axiom,
( ~ accessible_world(X0,X1)
| ~ relation(X0,X2)
| relation(X1,X2) ) ).
cnf(clause34,axiom,
( ~ existent(X0,X1)
| ~ nonexistent(X0,X1) ) ).
cnf(u852,negated_conjecture,
( ~ abstraction(skc15,X0)
| abstraction(skc16,X0) ) ).
cnf(u826,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc22) ) ).
cnf(u2573,negated_conjecture,
( agent(X0,skc27,skc29)
| ~ accessible_world(skc26,X0) ) ).
cnf(u932,negated_conjecture,
( ~ vincent_forename(skc15,X0)
| vincent_forename(skc16,X0) ) ).
cnf(u735,negated_conjecture,
( ~ eventuality(skc15,X0)
| eventuality(skc16,X0) ) ).
cnf(u941,negated_conjecture,
( agent(X0,skc17,skc19)
| ~ accessible_world(skc15,X0) ) ).
cnf(u2269,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc20,skc21) ) ).
cnf(u922,negated_conjecture,
( ~ forename(skc15,X0)
| forename(skc16,X0) ) ).
cnf(u995,negated_conjecture,
nonexistent(skc26,skf1(X0)) ).
cnf(u908,negated_conjecture,
( ~ living(skc15,X0)
| living(skc16,X0) ) ).
cnf(u1489,negated_conjecture,
( ~ accessible_world(skc26,X0)
| think_believe_consider(X0,skc27) ) ).
cnf(clause29,axiom,
( ~ vincent_forename(X0,X1)
| forename(X0,X1) ) ).
cnf(clause36,axiom,
( ~ accessible_world(X0,X1)
| ~ smoke(X0,X2)
| smoke(X1,X2) ) ).
cnf(u2252,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc17,skc16) ) ).
cnf(u816,negated_conjecture,
( ~ unisex(skc15,X0)
| unisex(skc26,X0) ) ).
cnf(u2265,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc18)
| ~ accessible_world(skc15,X0)
| ~ entity(X0,skc19)
| skc18 = X1 ) ).
cnf(clause30,axiom,
( ~ jules_forename(X0,X1)
| forename(X0,X1) ) ).
cnf(u898,negated_conjecture,
( ~ existent(skc15,X0)
| existent(skc16,X0) ) ).
cnf(u943,negated_conjecture,
( agent(X0,skc22,skc21)
| ~ accessible_world(skc16,X0) ) ).
cnf(u2259,negated_conjecture,
( ~ of(X0,X1,skc29)
| ~ forename(X0,X1)
| ~ forename(X0,skc28)
| ~ accessible_world(skc15,X0)
| ~ entity(X0,skc29)
| skc28 = X1 ) ).
cnf(clause64,axiom,
( ~ accessible_world(X0,X1)
| ~ vincent_forename(X0,X2)
| vincent_forename(X1,X2) ) ).
cnf(clause33,axiom,
( ~ human(X0,X1)
| ~ nonhuman(X0,X1) ) ).
cnf(u71,axiom,
( ~ of(X0,X2,X3)
| ~ forename(X0,X1)
| ~ forename(X0,X2)
| ~ of(X0,X1,X3)
| ~ entity(X0,X3)
| X1 = X2 ) ).
cnf(clause27,axiom,
( ~ forename(X0,X1)
| relname(X0,X1) ) ).
cnf(u2955,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc28,skc29) ) ).
cnf(u850,negated_conjecture,
( ~ relation(skc15,X0)
| relation(skc16,X0) ) ).
cnf(clause16,axiom,
( ~ man(X0,X1)
| human_person(X0,X1) ) ).
cnf(clause23,axiom,
( ~ organism(X0,X1)
| living(X0,X1) ) ).
cnf(clause10,axiom,
( ~ abstraction(X0,X1)
| thing(X0,X1) ) ).
cnf(u912,negated_conjecture,
( ~ animate(skc15,X0)
| animate(skc16,X0) ) ).
cnf(clause9,axiom,
( ~ relation(X0,X1)
| abstraction(X0,X1) ) ).
cnf(u2972,negated_conjecture,
( ~ of(X0,X1,skc21)
| ~ forename(X0,X1)
| ~ forename(X0,skc20)
| ~ accessible_world(skc26,X0)
| ~ entity(X0,skc21)
| skc20 = X1 ) ).
cnf(clause12,axiom,
( ~ abstraction(X0,X1)
| general(X0,X1) ) ).
cnf(clause3,axiom,
( ~ eventuality(X0,X1)
| thing(X0,X1) ) ).
cnf(clause6,axiom,
( ~ eventuality(X0,X1)
| nonexistent(X0,X1) ) ).
cnf(u954,negated_conjecture,
( of(X0,skc25,skc24)
| ~ accessible_world(skc15,X0) ) ).
cnf(clause5,axiom,
( ~ eventuality(X0,X1)
| specific(X0,X1) ) ).
cnf(clause112,negated_conjecture,
( agent(skc26,skf1(X0),X0)
| ~ man(skc26,X0) ) ).
cnf(u1426,negated_conjecture,
( ~ accessible_world(skc16,X0)
| think_believe_consider(X0,skc17) ) ).
cnf(u2801,negated_conjecture,
( agent(X0,skc22,skc21)
| ~ accessible_world(skc26,X0) ) ).
cnf(u897,negated_conjecture,
( ~ existent(skc15,X0)
| existent(skc26,X0) ) ).
cnf(u992,negated_conjecture,
( ~ theme(skc15,X0,X1)
| ~ think_believe_consider(skc15,X0)
| ~ proposition(skc15,X1)
| ~ agent(skc15,skc27,X2)
| ~ agent(skc15,X0,X2)
| skc26 = X1 ) ).
cnf(u1386,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc17) ) ).
cnf(u2605,negated_conjecture,
( be(X0,skc23,skc24,skc24)
| ~ accessible_world(skc26,X0) ) ).
cnf(u849,negated_conjecture,
( ~ relation(skc15,X0)
| relation(skc26,X0) ) ).
cnf(u2824,negated_conjecture,
( ~ theme(skc15,X0,X1)
| ~ think_believe_consider(skc15,X0)
| ~ proposition(skc15,X1)
| ~ agent(skc15,skc17,X2)
| ~ agent(skc15,X0,X2)
| skc26 = X1 ) ).
cnf(u734,negated_conjecture,
( ~ eventuality(skc15,X0)
| eventuality(skc26,X0) ) ).
cnf(u2586,negated_conjecture,
( theme(X0,skc27,skc26)
| ~ accessible_world(skc26,X0) ) ).
cnf(u919,negated_conjecture,
( ~ male(skc15,X0)
| male(skc26,X0) ) ).
cnf(u944,negated_conjecture,
( agent(X0,skf1(X1),X1)
| ~ accessible_world(skc26,X0)
| ~ man(skc26,X1) ) ).
cnf(u756,negated_conjecture,
( ~ singleton(skc15,X0)
| singleton(skc26,X0) ) ).
cnf(u921,negated_conjecture,
( ~ forename(skc15,X0)
| forename(skc26,X0) ) ).
cnf(u2256,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc27,skc26) ) ).
cnf(u736,negated_conjecture,
( ~ thing(skc15,X0)
| thing(skc26,X0) ) ).
cnf(clause62,axiom,
( ~ accessible_world(X0,X1)
| ~ forename(X0,X2)
| forename(X1,X2) ) ).
cnf(u797,negated_conjecture,
( ~ nonexistent(skc15,X0)
| nonexistent(skc16,X0) ) ).
cnf(u920,negated_conjecture,
( ~ male(skc15,X0)
| male(skc16,X0) ) ).
cnf(u732,negated_conjecture,
( ~ event(skc15,X0)
| event(skc26,X0) ) ).
cnf(u1413,negated_conjecture,
( ~ accessible_world(skc26,X0)
| present(X0,skc27) ) ).
cnf(u851,negated_conjecture,
( ~ abstraction(skc15,X0)
| abstraction(skc26,X0) ) ).
cnf(u2271,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| be(X1,skc23,skc24,skc24) ) ).
cnf(u2243,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| present(X1,skf1(X2)) ) ).
cnf(u1399,negated_conjecture,
( ~ accessible_world(skc26,X0)
| present(X0,skc17) ) ).
cnf(clause68,axiom,
( ~ of(X0,X2,X3)
| ~ accessible_world(X0,X1)
| of(X1,X2,X3) ) ).
cnf(u930,negated_conjecture,
( ~ relname(skc15,X0)
| relname(skc16,X0) ) ).
cnf(u2260,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc28,skc29) ) ).
cnf(clause44,axiom,
( ~ present(X0,X2)
| ~ accessible_world(X0,X1)
| present(X1,X2) ) ).
cnf(clause59,axiom,
( ~ accessible_world(X0,X1)
| ~ human(X0,X2)
| human(X1,X2) ) ).
cnf(u955,negated_conjecture,
( of(X0,skc18,skc19)
| ~ accessible_world(skc15,X0) ) ).
cnf(u2569,negated_conjecture,
( agent(X0,skc17,skc19)
| ~ accessible_world(skc26,X0) ) ).
cnf(clause61,axiom,
( ~ accessible_world(X0,X1)
| ~ male(X0,X2)
| male(X1,X2) ) ).
cnf(clause48,axiom,
( ~ accessible_world(X0,X1)
| ~ abstraction(X0,X2)
| abstraction(X1,X2) ) ).
cnf(u940,negated_conjecture,
( ~ jules_forename(skc15,X0)
| jules_forename(skc16,X0) ) ).
cnf(clause55,axiom,
( ~ accessible_world(X0,X1)
| ~ entity(X0,X2)
| entity(X1,X2) ) ).
cnf(u906,negated_conjecture,
( ~ impartial(skc15,X0)
| impartial(skc16,X0) ) ).
cnf(clause42,axiom,
( ~ accessible_world(X0,X1)
| ~ nonexistent(X0,X2)
| nonexistent(X1,X2) ) ).
cnf(clause71,axiom,
( ~ theme(X0,X4,X2)
| ~ proposition(X0,X2)
| ~ theme(X0,X3,X1)
| ~ think_believe_consider(X0,X3)
| ~ think_believe_consider(X0,X4)
| ~ proposition(X0,X1)
| ~ agent(X0,X4,X5)
| ~ agent(X0,X3,X5)
| X1 = X2 ) ).
cnf(clause41,axiom,
( ~ accessible_world(X0,X1)
| ~ specific(X0,X2)
| specific(X1,X2) ) ).
cnf(clause66,axiom,
( ~ agent(X0,X2,X3)
| ~ accessible_world(X0,X1)
| agent(X1,X2,X3) ) ).
cnf(u997,negated_conjecture,
thing(skc26,skf1(X0)) ).
cnf(clause35,axiom,
( ~ be(X0,X1,X2,X3)
| X2 = X3 ) ).
cnf(clause65,axiom,
( ~ accessible_world(X0,X1)
| ~ jules_forename(X0,X2)
| jules_forename(X1,X2) ) ).
cnf(clause38,axiom,
( ~ accessible_world(X0,X1)
| ~ eventuality(X0,X2)
| eventuality(X1,X2) ) ).
cnf(u953,negated_conjecture,
( of(X0,skc28,skc29)
| ~ accessible_world(skc15,X0) ) ).
cnf(u858,negated_conjecture,
( ~ state(skc15,X0)
| state(skc16,X0) ) ).
cnf(clause37,axiom,
( ~ accessible_world(X0,X1)
| ~ event(X0,X2)
| event(X1,X2) ) ).
cnf(clause24,axiom,
( ~ human_person(X0,X1)
| human(X0,X1) ) ).
cnf(clause31,axiom,
( ~ male(X0,X1)
| ~ unisex(X0,X1) ) ).
cnf(clause18,axiom,
( ~ organism(X0,X1)
| entity(X0,X1) ) ).
cnf(u2952,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc26)
| ~ accessible_world(skc26,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc27,X3)
| ~ agent(X0,X1,X3)
| skc26 = X2 ) ).
cnf(u854,negated_conjecture,
( ~ nonhuman(skc15,X0)
| nonhuman(skc16,X0) ) ).
cnf(clause17,axiom,
( ~ human_person(X0,X1)
| organism(X0,X1) ) ).
cnf(u1439,negated_conjecture,
( ~ accessible_world(skc26,X0)
| think_believe_consider(X0,skc17) ) ).
cnf(u777,negated_conjecture,
( ~ specific(skc15,X0)
| specific(skc16,X0) ) ).
cnf(u2329,negated_conjecture,
( theme(X0,skc17,skc26)
| ~ accessible_world(skc15,X0) ) ).
cnf(u825,negated_conjecture,
( ~ accessible_world(skc15,X0)
| present(X0,skc27) ) ).
cnf(u929,negated_conjecture,
( ~ relname(skc15,X0)
| relname(skc26,X0) ) ).
cnf(u2933,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc27,skc29) ) ).
cnf(u2960,negated_conjecture,
( ~ of(X0,X1,skc24)
| ~ forename(X0,X1)
| ~ forename(X0,skc25)
| ~ accessible_world(skc26,X0)
| ~ entity(X0,skc24)
| skc25 = X1 ) ).
cnf(u881,negated_conjecture,
( ~ organism(skc15,X0)
| organism(skc26,X0) ) ).
cnf(u824,negated_conjecture,
( ~ accessible_world(skc15,X0)
| present(X0,skc17) ) ).
cnf(u2268,negated_conjecture,
( ~ of(X0,X1,skc21)
| ~ forename(X0,X1)
| ~ forename(X0,skc20)
| ~ accessible_world(skc15,X0)
| ~ entity(X0,skc21)
| skc20 = X1 ) ).
cnf(u1400,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc27) ) ).
cnf(u951,negated_conjecture,
( theme(X0,skc17,skc16)
| ~ accessible_world(skc15,X0) ) ).
cnf(u877,negated_conjecture,
( present(X0,skf1(X1))
| ~ accessible_world(skc26,X0) ) ).
cnf(u2966,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc18)
| ~ accessible_world(skc26,X0)
| ~ entity(X0,skc19)
| skc18 = X1 ) ).
cnf(u882,negated_conjecture,
( ~ organism(skc15,X0)
| organism(skc16,X0) ) ).
cnf(u2577,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc22,skc21) ) ).
cnf(u931,negated_conjecture,
( ~ vincent_forename(skc15,X0)
| vincent_forename(skc26,X0) ) ).
cnf(u2263,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc25,skc24) ) ).
cnf(u2249,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc22,skc21) ) ).
cnf(u2991,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| be(X1,skc23,skc24,skc24) ) ).
cnf(clause14,axiom,
( ~ state(X0,X1)
| eventuality(X0,X1) ) ).
cnf(u796,negated_conjecture,
( ~ nonexistent(skc15,X0)
| nonexistent(skc26,X0) ) ).
cnf(u2245,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc17,skc19) ) ).
cnf(clause20,axiom,
( ~ entity(X0,X1)
| specific(X0,X1) ) ).
cnf(clause11,axiom,
( ~ abstraction(X0,X1)
| nonhuman(X0,X1) ) ).
cnf(u907,negated_conjecture,
( ~ living(skc15,X0)
| living(skc26,X0) ) ).
cnf(u834,negated_conjecture,
( ~ accessible_world(skc15,X0)
| think_believe_consider(X0,skc27) ) ).
cnf(u2937,negated_conjecture,
( ~ accessible_world(skc26,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc17,skc26) ) ).
cnf(clause13,axiom,
( ~ abstraction(X0,X1)
| unisex(X0,X1) ) ).
cnf(u2943,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc26)
| ~ accessible_world(skc26,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc17,X3)
| ~ agent(X0,X1,X3)
| skc26 = X2 ) ).
cnf(u2257,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc26)
| ~ accessible_world(skc15,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc27,X3)
| ~ agent(X0,X1,X3)
| skc26 = X2 ) ).
cnf(clause7,axiom,
( ~ eventuality(X0,X1)
| unisex(X0,X1) ) ).
cnf(u986,negated_conjecture,
( ~ of(skc15,X0,skc24)
| ~ forename(skc15,X0)
| skc25 = X0 ) ).
cnf(u2918,negated_conjecture,
( ~ accessible_world(skc15,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc17,skc26) ) ).
cnf(u905,negated_conjecture,
( ~ impartial(skc15,X0)
| impartial(skc26,X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP241-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 18:37:39 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.02/1.86 % (2657325)Input is clausal, will run a generic CNF schedule.
% 6.02/1.86 % (2657330)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3666060377:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.02/1.86 % (2657335)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1108604466:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.02/1.86 % (2657331)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2291585702:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.02/1.86 % (2657333)lrs+10_1_sil=8000:sp=occurrence:random_seed=2726325993:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.02/1.86 % (2657334)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3082903069:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.02/1.86 % (2657336)dis-21_1_sil=8000:lcm=predicate:random_seed=3862880567:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.02/1.86 % (2657332)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1468383572:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.02/1.86 % (2657333)Refutation not found, incomplete strategy
% 6.02/1.86 % (2657333)------------------------------
% 6.02/1.86 % (2657333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657333)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657333)Termination reason: Refutation not found, incomplete strategy
% 6.02/1.86 % (2657333)Time elapsed: 0.014 s
% 6.02/1.86 % (2657333)Peak memory usage: 88 MB
% 6.02/1.86 % (2657333)Instructions burned: 21 (million)
% 6.02/1.86 % (2657336)Instruction limit reached!
% 6.02/1.86 % (2657336)------------------------------
% 6.02/1.86 % (2657336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657336)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657336)Termination reason: Instruction limit
% 6.02/1.86 % (2657336)Termination phase: Saturation
% 6.02/1.86 % (2657336)Time elapsed: 0.047 s
% 6.02/1.86 % (2657336)Peak memory usage: 88 MB
% 6.02/1.86 % (2657336)Instructions burned: 117 (million)
% 6.02/1.86 % (2657335)Refutation not found, incomplete strategy
% 6.02/1.86 % (2657335)------------------------------
% 6.02/1.86 % (2657335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657335)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657335)Termination reason: Refutation not found, incomplete strategy
% 6.02/1.86 % (2657335)Time elapsed: 0.060 s
% 6.02/1.86 % (2657335)Peak memory usage: 89 MB
% 6.02/1.86 % (2657335)Instructions burned: 91 (million)
% 6.02/1.86 % (2657334)Instruction limit reached!
% 6.02/1.86 % (2657334)------------------------------
% 6.02/1.86 % (2657334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657334)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657334)Termination reason: Instruction limit
% 6.02/1.86 % (2657334)Termination phase: Saturation
% 6.02/1.86 % (2657334)Time elapsed: 0.069 s
% 6.02/1.86 % (2657334)Peak memory usage: 88 MB
% 6.02/1.86 % (2657334)Instructions burned: 115 (million)
% 6.02/1.86 % (2657344)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3462156127:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.02/1.86 % (2657345)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=459297202:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 6.02/1.86 % (2657345)Refutation not found, incomplete strategy
% 6.02/1.86 % (2657345)------------------------------
% 6.02/1.86 % (2657345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657345)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657345)Termination reason: Refutation not found, incomplete strategy
% 6.02/1.86 % (2657345)Time elapsed: 0.014 s
% 6.02/1.86 % (2657345)Peak memory usage: 88 MB
% 6.02/1.86 % (2657345)Instructions burned: 25 (million)
% 6.02/1.86 % (2657333)------------------------------
% 6.02/1.86 % (2657333)------------------------------
% 6.02/1.86 % (2657344)Instruction limit reached!
% 6.02/1.86 % (2657344)------------------------------
% 6.02/1.86 % (2657344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657344)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657344)Termination reason: Instruction limit
% 6.02/1.86 % (2657344)Termination phase: Saturation
% 6.02/1.86 % (2657344)Time elapsed: 0.076 s
% 6.02/1.86 % (2657344)Peak memory usage: 89 MB
% 6.02/1.86 % (2657344)Instructions burned: 144 (million)
% 6.02/1.86 % (2657335)------------------------------
% 6.02/1.86 % (2657335)------------------------------
% 6.02/1.86 % (2657348)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=899790900:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 6.02/1.86 % (2657349)lrs+10_64_to=lpo:sil=8000:random_seed=31189397:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.02/1.86 % (2657350)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3180252837:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.02/1.86 % (2657349)Instruction limit reached!
% 6.02/1.86 % (2657349)------------------------------
% 6.02/1.86 % (2657349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657349)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657349)Termination reason: Instruction limit
% 6.02/1.86 % (2657349)Termination phase: Saturation
% 6.02/1.86 % (2657349)Time elapsed: 0.050 s
% 6.02/1.86 % (2657349)Peak memory usage: 88 MB
% 6.02/1.86 % (2657349)Instructions burned: 128 (million)
% 6.02/1.86 % (2657330)Refutation not found, incomplete strategy
% 6.02/1.86 % (2657330)------------------------------
% 6.02/1.86 % (2657330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657330)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657330)Termination reason: Refutation not found, incomplete strategy
% 6.02/1.86 % (2657330)Time elapsed: 0.505 s
% 6.02/1.86 % (2657330)Peak memory usage: 129 MB
% 6.02/1.86 % (2657330)Instructions burned: 1098 (million)
% 6.02/1.86 % (2657345)------------------------------
% 6.02/1.86 % (2657345)------------------------------
% 6.02/1.86 % (2657350)Refutation not found, incomplete strategy
% 6.02/1.86 % (2657350)------------------------------
% 6.02/1.86 % (2657350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657350)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657350)Termination reason: Refutation not found, incomplete strategy
% 6.02/1.86 % (2657350)Time elapsed: 0.043 s
% 6.02/1.86 % (2657350)Peak memory usage: 89 MB
% 6.02/1.86 % (2657350)Instructions burned: 64 (million)
% 6.02/1.86 % (2657348)Instruction limit reached!
% 6.02/1.86 % (2657348)------------------------------
% 6.02/1.86 % (2657348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657348)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657348)Termination reason: Instruction limit
% 6.02/1.86 % (2657348)Termination phase: Saturation
% 6.02/1.86 % (2657348)Time elapsed: 0.092 s
% 6.02/1.86 % (2657348)Peak memory usage: 89 MB
% 6.02/1.86 % (2657348)Instructions burned: 221 (million)
% 6.02/1.86 % (2657354)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1495929962:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.02/1.86 % (2657356)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3411943798:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 6.02/1.86 % (2657355)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2422456827:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.02/1.86 % (2657330)------------------------------
% 6.02/1.86 % (2657330)------------------------------
% 6.02/1.86 % (2657354)First to succeed.
% 6.02/1.86 % (2657354)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2657325"
% 6.02/1.86 % (2657356)Refutation not found, incomplete strategy
% 6.02/1.86 % (2657356)------------------------------
% 6.02/1.86 % (2657356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657356)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657356)Termination reason: Refutation not found, incomplete strategy
% 6.02/1.86 % (2657356)Time elapsed: 0.033 s
% 6.02/1.86 % (2657356)Peak memory usage: 89 MB
% 6.02/1.86 % (2657356)Instructions burned: 59 (million)
% 6.02/1.86 % (2657350)------------------------------
% 6.02/1.86 % (2657350)------------------------------
% 6.02/1.86 % (2657360)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=335570132:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.02/1.86 % (2657360)Instruction limit reached!
% 6.02/1.86 % (2657360)------------------------------
% 6.02/1.86 % (2657360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.02/1.86 % (2657360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.86 % (2657360)CaDiCaL version: 2.1.3
% 6.02/1.86 % (2657360)Termination reason: Instruction limit
% 6.02/1.86 % (2657360)Termination phase: Saturation
% 6.02/1.86 % (2657360)Time elapsed: 0.059 s
% 6.02/1.86 % (2657360)Peak memory usage: 89 MB
% 6.02/1.86 % (2657360)Instructions burned: 108 (million)
% 6.02/1.86 % (2657361)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4256012750:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 6.02/1.86 % SZS status Satisfiable for theBenchmark
% 6.02/1.86 % SZS output start Saturation.
% See solution above
% 7.60/1.95 % SZS output start Definitions and Model Updates.
% 7.60/1.95 for all inputs,
% 7.60/1.95 define actual_world(X0) := $true
% 7.60/1.95 % SZS output end Definitions and Model Updates.
% 7.60/1.95 % (2657354)------------------------------
% 7.60/1.95 % (2657354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.95 % (2657354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.95 % (2657354)CaDiCaL version: 2.1.3
% 7.60/1.95 % (2657354)Termination reason: Satisfiable
% 7.60/1.95 % (2657354)Time elapsed: 0.051 s
% 7.60/1.95 % (2657354)Peak memory usage: 90 MB
% 7.60/1.95 % (2657354)Instructions burned: 77 (million)
% 7.60/1.95 % (2657354)------------------------------
% 7.60/1.95 % (2657354)------------------------------
% 7.60/1.95 % (2657325)Success in time 1.011 s
% 7.60/1.95 % Vampire exiting
%------------------------------------------------------------------------------