%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP248-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 : n009.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:11 PM UTC 2026
% Result : Satisfiable 8.82s 2.65s
% Output : Saturation 10.70s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u114,negated_conjecture,
event(skc16,skf1(X1)) ).
cnf(u121,negated_conjecture,
present(skc16,skf1(X1)) ).
cnf(u125,negated_conjecture,
smoke(skc16,skf1(X1)) ).
cnf(u130,negated_conjecture,
be(skc13,skc22,skc23,skc23) ).
cnf(u135,negated_conjecture,
theme(skc13,skc15,skc14) ).
cnf(u140,negated_conjecture,
theme(skc13,skc17,skc16) ).
cnf(u145,negated_conjecture,
agent(skc13,skc15,skc19) ).
cnf(u150,negated_conjecture,
agent(skc13,skc17,skc19) ).
cnf(u155,negated_conjecture,
of(skc13,skc18,skc19) ).
cnf(u160,negated_conjecture,
of(skc13,skc20,skc19) ).
cnf(u165,negated_conjecture,
agent(skc14,skc26,skc23) ).
cnf(u170,negated_conjecture,
of(skc13,skc24,skc23) ).
cnf(u175,negated_conjecture,
of(skc13,skc25,skc23) ).
cnf(u180,negated_conjecture,
state(skc13,skc22) ).
cnf(u185,negated_conjecture,
accessible_world(skc13,skc14) ).
cnf(u190,negated_conjecture,
proposition(skc13,skc14) ).
cnf(u195,negated_conjecture,
proposition(skc13,skc16) ).
cnf(u200,negated_conjecture,
accessible_world(skc13,skc16) ).
cnf(u205,negated_conjecture,
event(skc13,skc15) ).
cnf(u210,negated_conjecture,
present(skc13,skc15) ).
cnf(u215,negated_conjecture,
think_believe_consider(skc13,skc15) ).
cnf(u220,negated_conjecture,
think_believe_consider(skc13,skc17) ).
cnf(u225,negated_conjecture,
present(skc13,skc17) ).
cnf(u230,negated_conjecture,
event(skc13,skc17) ).
cnf(u235,negated_conjecture,
vincent_forename(skc13,skc18) ).
cnf(u240,negated_conjecture,
forename(skc13,skc18) ).
cnf(u245,negated_conjecture,
man(skc13,skc19) ).
cnf(u250,negated_conjecture,
vincent_forename(skc13,skc20) ).
cnf(u255,negated_conjecture,
forename(skc13,skc20) ).
cnf(u260,negated_conjecture,
man(skc13,skc23) ).
cnf(u265,negated_conjecture,
smoke(skc14,skc26) ).
cnf(u270,negated_conjecture,
present(skc14,skc26) ).
cnf(u275,negated_conjecture,
forename(skc13,skc25) ).
cnf(u280,negated_conjecture,
jules_forename(skc13,skc25) ).
cnf(u285,negated_conjecture,
forename(skc13,skc24) ).
cnf(u290,negated_conjecture,
jules_forename(skc13,skc24) ).
cnf(u295,negated_conjecture,
event(skc14,skc26) ).
cnf(u304,negated_conjecture,
eventuality(skc14,skc26) ).
cnf(u309,negated_conjecture,
eventuality(skc13,skc17) ).
cnf(u314,negated_conjecture,
eventuality(skc13,skc15) ).
cnf(u320,negated_conjecture,
thing(skc14,skc26) ).
cnf(u326,negated_conjecture,
thing(skc13,skc17) ).
cnf(u332,negated_conjecture,
thing(skc13,skc15) ).
cnf(u340,negated_conjecture,
specific(skc13,skc15) ).
cnf(u345,negated_conjecture,
specific(skc13,skc17) ).
cnf(u350,negated_conjecture,
specific(skc14,skc26) ).
cnf(u356,negated_conjecture,
singleton(skc14,skc26) ).
cnf(u364,negated_conjecture,
nonexistent(skc13,skc15) ).
cnf(u369,negated_conjecture,
nonexistent(skc13,skc17) ).
cnf(u374,negated_conjecture,
nonexistent(skc14,skc26) ).
cnf(u380,negated_conjecture,
singleton(skc13,skc17) ).
cnf(u388,negated_conjecture,
unisex(skc13,skc15) ).
cnf(u393,negated_conjecture,
unisex(skc13,skc17) ).
cnf(u398,negated_conjecture,
unisex(skc14,skc26) ).
cnf(u404,negated_conjecture,
singleton(skc13,skc15) ).
cnf(u411,negated_conjecture,
relation(skc13,skc16) ).
cnf(u416,negated_conjecture,
relation(skc13,skc14) ).
cnf(u422,negated_conjecture,
abstraction(skc13,skc16) ).
cnf(u428,negated_conjecture,
abstraction(skc13,skc14) ).
cnf(u434,negated_conjecture,
eventuality(skc13,skc22) ).
cnf(u443,negated_conjecture,
thing(skc13,skc22) ).
cnf(u448,negated_conjecture,
specific(skc13,skc22) ).
cnf(u453,negated_conjecture,
nonexistent(skc13,skc22) ).
cnf(u458,negated_conjecture,
unisex(skc13,skc22) ).
cnf(u464,negated_conjecture,
event(skc13,skc22) ).
cnf(u472,negated_conjecture,
human_person(skc13,skc23) ).
cnf(u477,negated_conjecture,
human_person(skc13,skc19) ).
cnf(u483,negated_conjecture,
organism(skc13,skc23) ).
cnf(u489,negated_conjecture,
organism(skc13,skc19) ).
cnf(u498,negated_conjecture,
thing(skc13,skc16) ).
cnf(u503,negated_conjecture,
nonhuman(skc13,skc16) ).
cnf(u508,negated_conjecture,
general(skc13,skc16) ).
cnf(u513,negated_conjecture,
unisex(skc13,skc16) ).
cnf(u520,negated_conjecture,
human(skc13,skc19) ).
cnf(u525,negated_conjecture,
human(skc13,skc23) ).
cnf(u534,negated_conjecture,
thing(skc13,skc14) ).
cnf(u539,negated_conjecture,
nonhuman(skc13,skc14) ).
cnf(u544,negated_conjecture,
general(skc13,skc14) ).
cnf(u549,negated_conjecture,
unisex(skc13,skc14) ).
cnf(u556,negated_conjecture,
animate(skc13,skc19) ).
cnf(u561,negated_conjecture,
animate(skc13,skc23) ).
cnf(u567,negated_conjecture,
singleton(skc13,skc22) ).
cnf(u574,negated_conjecture,
male(skc13,skc23) ).
cnf(u579,negated_conjecture,
male(skc13,skc19) ).
cnf(u588,negated_conjecture,
relname(skc13,skc18) ).
cnf(u593,negated_conjecture,
relname(skc13,skc20) ).
cnf(u598,negated_conjecture,
relname(skc13,skc25) ).
cnf(u603,negated_conjecture,
relname(skc13,skc24) ).
cnf(u609,negated_conjecture,
relation(skc13,skc18) ).
cnf(u617,negated_conjecture,
relation(skc13,skc20) ).
cnf(u625,negated_conjecture,
relation(skc13,skc25) ).
cnf(u632,negated_conjecture,
~ unisex(skc13,skc19) ).
cnf(u637,negated_conjecture,
~ unisex(skc13,skc23) ).
cnf(u643,negated_conjecture,
relation(skc13,skc24) ).
cnf(u652,negated_conjecture,
entity(skc13,skc23) ).
cnf(u657,negated_conjecture,
impartial(skc13,skc23) ).
cnf(u662,negated_conjecture,
living(skc13,skc23) ).
cnf(u672,negated_conjecture,
entity(skc13,skc19) ).
cnf(u677,negated_conjecture,
impartial(skc13,skc19) ).
cnf(u682,negated_conjecture,
living(skc13,skc19) ).
cnf(u690,negated_conjecture,
~ nonhuman(skc13,skc19) ).
cnf(u698,negated_conjecture,
~ nonhuman(skc13,skc23) ).
cnf(u710,negated_conjecture,
abstraction(skc13,skc18) ).
cnf(u718,negated_conjecture,
abstraction(skc13,skc20) ).
cnf(u726,negated_conjecture,
abstraction(skc13,skc25) ).
cnf(u739,negated_conjecture,
abstraction(skc13,skc24) ).
cnf(u753,negated_conjecture,
singleton(skc13,skc16) ).
cnf(u769,negated_conjecture,
~ specific(skc13,skc16) ).
cnf(u777,negated_conjecture,
singleton(skc13,skc14) ).
cnf(u787,negated_conjecture,
~ specific(skc13,skc14) ).
cnf(u801,negated_conjecture,
thing(skc13,skc23) ).
cnf(u806,negated_conjecture,
specific(skc13,skc23) ).
cnf(u811,negated_conjecture,
existent(skc13,skc23) ).
cnf(u825,negated_conjecture,
thing(skc13,skc19) ).
cnf(u830,negated_conjecture,
specific(skc13,skc19) ).
cnf(u835,negated_conjecture,
existent(skc13,skc19) ).
cnf(u854,negated_conjecture,
thing(skc13,skc18) ).
cnf(u859,negated_conjecture,
nonhuman(skc13,skc18) ).
cnf(u864,negated_conjecture,
general(skc13,skc18) ).
cnf(u869,negated_conjecture,
unisex(skc13,skc18) ).
cnf(u882,negated_conjecture,
thing(skc13,skc20) ).
cnf(u887,negated_conjecture,
nonhuman(skc13,skc20) ).
cnf(u892,negated_conjecture,
general(skc13,skc20) ).
cnf(u897,negated_conjecture,
unisex(skc13,skc20) ).
cnf(u908,negated_conjecture,
thing(skc13,skc25) ).
cnf(u913,negated_conjecture,
nonhuman(skc13,skc25) ).
cnf(u918,negated_conjecture,
general(skc13,skc25) ).
cnf(u923,negated_conjecture,
unisex(skc13,skc25) ).
cnf(u936,negated_conjecture,
thing(skc13,skc24) ).
cnf(u941,negated_conjecture,
nonhuman(skc13,skc24) ).
cnf(u946,negated_conjecture,
general(skc13,skc24) ).
cnf(u951,negated_conjecture,
unisex(skc13,skc24) ).
cnf(u980,negated_conjecture,
singleton(skc13,skc23) ).
cnf(u988,negated_conjecture,
event(skc14,skc22) ).
cnf(u993,negated_conjecture,
event(skc14,skc17) ).
cnf(u998,negated_conjecture,
event(skc14,skc15) ).
cnf(u1004,negated_conjecture,
eventuality(skc14,skc22) ).
cnf(u1012,negated_conjecture,
event(skc16,skc22) ).
cnf(u1017,negated_conjecture,
event(skc16,skc17) ).
cnf(u1022,negated_conjecture,
event(skc16,skc15) ).
cnf(u1028,negated_conjecture,
eventuality(skc14,skc17) ).
cnf(u1036,negated_conjecture,
eventuality(skc14,skc15) ).
cnf(u1045,negated_conjecture,
eventuality(skc16,skc22) ).
cnf(u1050,negated_conjecture,
eventuality(skc16,skc15) ).
cnf(u1055,negated_conjecture,
eventuality(skc16,skc17) ).
cnf(u1067,negated_conjecture,
thing(skc14,skc22) ).
cnf(u1072,negated_conjecture,
thing(skc14,skc16) ).
cnf(u1077,negated_conjecture,
thing(skc14,skc15) ).
cnf(u1082,negated_conjecture,
thing(skc14,skc17) ).
cnf(u1087,negated_conjecture,
thing(skc14,skc23) ).
cnf(u1092,negated_conjecture,
thing(skc14,skc14) ).
cnf(u1104,negated_conjecture,
thing(skc16,skc22) ).
cnf(u1109,negated_conjecture,
thing(skc16,skc16) ).
cnf(u1114,negated_conjecture,
thing(skc16,skc15) ).
cnf(u1119,negated_conjecture,
thing(skc16,skc17) ).
cnf(u1124,negated_conjecture,
thing(skc16,skc23) ).
cnf(u1129,negated_conjecture,
thing(skc16,skc14) ).
cnf(u1140,negated_conjecture,
singleton(skc14,skc22) ).
cnf(u1145,negated_conjecture,
singleton(skc14,skc16) ).
cnf(u1150,negated_conjecture,
singleton(skc14,skc15) ).
cnf(u1155,negated_conjecture,
singleton(skc14,skc17) ).
cnf(u1160,negated_conjecture,
singleton(skc14,skc14) ).
cnf(u1169,negated_conjecture,
specific(skc14,skc15) ).
cnf(u1174,negated_conjecture,
nonexistent(skc14,skc15) ).
cnf(u1179,negated_conjecture,
unisex(skc14,skc15) ).
cnf(u1189,negated_conjecture,
singleton(skc16,skc22) ).
cnf(u1194,negated_conjecture,
singleton(skc16,skc16) ).
cnf(u1199,negated_conjecture,
singleton(skc16,skc15) ).
cnf(u1204,negated_conjecture,
singleton(skc16,skc17) ).
cnf(u1209,negated_conjecture,
singleton(skc16,skc14) ).
cnf(u1218,negated_conjecture,
specific(skc16,skc22) ).
cnf(u1223,negated_conjecture,
nonexistent(skc16,skc22) ).
cnf(u1228,negated_conjecture,
unisex(skc16,skc22) ).
cnf(u1237,negated_conjecture,
specific(skc14,skc22) ).
cnf(u1242,negated_conjecture,
specific(skc14,skc17) ).
cnf(u1247,negated_conjecture,
specific(skc14,skc23) ).
cnf(u1256,negated_conjecture,
specific(skc16,skc15) ).
cnf(u1261,negated_conjecture,
nonexistent(skc16,skc15) ).
cnf(u1266,negated_conjecture,
unisex(skc16,skc15) ).
cnf(u1275,negated_conjecture,
specific(skc16,skc17) ).
cnf(u1280,negated_conjecture,
specific(skc16,skc23) ).
cnf(u1289,negated_conjecture,
nonexistent(skc16,skc17) ).
cnf(u1294,negated_conjecture,
unisex(skc16,skc17) ).
cnf(u1302,negated_conjecture,
nonexistent(skc14,skc22) ).
cnf(u1307,negated_conjecture,
nonexistent(skc14,skc17) ).
cnf(u1316,negated_conjecture,
unisex(skc14,skc22) ).
cnf(u1328,negated_conjecture,
unisex(skc14,skc17) ).
cnf(u1338,negated_conjecture,
unisex(skc14,skc16) ).
cnf(u1343,negated_conjecture,
unisex(skc14,skc14) ).
cnf(u1354,negated_conjecture,
unisex(skc16,skc16) ).
cnf(u1359,negated_conjecture,
unisex(skc16,skc14) ).
cnf(u1367,negated_conjecture,
present(skc16,skc15) ).
cnf(u1372,negated_conjecture,
present(skc14,skc15) ).
cnf(u1380,negated_conjecture,
present(skc16,skc17) ).
cnf(u1385,negated_conjecture,
present(skc14,skc17) ).
cnf(u1394,negated_conjecture,
think_believe_consider(skc16,skc15) ).
cnf(u1399,negated_conjecture,
think_believe_consider(skc14,skc15) ).
cnf(u1407,negated_conjecture,
think_believe_consider(skc16,skc17) ).
cnf(u1412,negated_conjecture,
think_believe_consider(skc14,skc17) ).
cnf(u1420,negated_conjecture,
proposition(skc14,skc16) ).
cnf(u1425,negated_conjecture,
proposition(skc14,skc14) ).
cnf(u1433,negated_conjecture,
proposition(skc16,skc16) ).
cnf(u1438,negated_conjecture,
proposition(skc16,skc14) ).
cnf(u1450,negated_conjecture,
relation(skc14,skc16) ).
cnf(u1455,negated_conjecture,
relation(skc14,skc18) ).
cnf(u1460,negated_conjecture,
relation(skc14,skc20) ).
cnf(u1465,negated_conjecture,
relation(skc14,skc25) ).
cnf(u1470,negated_conjecture,
relation(skc14,skc24) ).
cnf(u1475,negated_conjecture,
relation(skc14,skc14) ).
cnf(u1487,negated_conjecture,
relation(skc16,skc16) ).
cnf(u1492,negated_conjecture,
relation(skc16,skc18) ).
cnf(u1497,negated_conjecture,
relation(skc16,skc20) ).
cnf(u1502,negated_conjecture,
relation(skc16,skc25) ).
cnf(u1507,negated_conjecture,
relation(skc16,skc24) ).
cnf(u1512,negated_conjecture,
relation(skc16,skc14) ).
cnf(u1524,negated_conjecture,
abstraction(skc14,skc16) ).
cnf(u1529,negated_conjecture,
abstraction(skc14,skc18) ).
cnf(u1534,negated_conjecture,
abstraction(skc14,skc20) ).
cnf(u1539,negated_conjecture,
abstraction(skc14,skc25) ).
cnf(u1544,negated_conjecture,
abstraction(skc14,skc24) ).
cnf(u1549,negated_conjecture,
abstraction(skc14,skc14) ).
cnf(u1561,negated_conjecture,
abstraction(skc16,skc16) ).
cnf(u1566,negated_conjecture,
abstraction(skc16,skc18) ).
cnf(u1571,negated_conjecture,
abstraction(skc16,skc20) ).
cnf(u1576,negated_conjecture,
abstraction(skc16,skc25) ).
cnf(u1581,negated_conjecture,
abstraction(skc16,skc24) ).
cnf(u1586,negated_conjecture,
abstraction(skc16,skc14) ).
cnf(u1594,negated_conjecture,
nonhuman(skc14,skc14) ).
cnf(u1599,negated_conjecture,
nonhuman(skc14,skc16) ).
cnf(u1607,negated_conjecture,
nonhuman(skc16,skc14) ).
cnf(u1612,negated_conjecture,
nonhuman(skc16,skc16) ).
cnf(u1620,negated_conjecture,
general(skc14,skc14) ).
cnf(u1625,negated_conjecture,
general(skc14,skc16) ).
cnf(u1633,negated_conjecture,
general(skc16,skc14) ).
cnf(u1638,negated_conjecture,
general(skc16,skc16) ).
cnf(u1645,negated_conjecture,
state(skc14,skc22) ).
cnf(u1652,negated_conjecture,
state(skc16,skc22) ).
cnf(u1661,negated_conjecture,
man(skc14,skc23) ).
cnf(u1666,negated_conjecture,
man(skc14,skc19) ).
cnf(u1675,negated_conjecture,
man(skc16,skc23) ).
cnf(u1680,negated_conjecture,
man(skc16,skc19) ).
cnf(u1687,negated_conjecture,
human_person(skc14,skc23) ).
cnf(u1692,negated_conjecture,
male(skc14,skc23) ).
cnf(u1699,negated_conjecture,
human_person(skc14,skc19) ).
cnf(u1706,negated_conjecture,
male(skc14,skc19) ).
cnf(u1713,negated_conjecture,
human_person(skc16,skc19) ).
cnf(u1718,negated_conjecture,
human_person(skc16,skc23) ).
cnf(u1725,negated_conjecture,
male(skc16,skc23) ).
cnf(u1732,negated_conjecture,
organism(skc14,skc19) ).
cnf(u1737,negated_conjecture,
organism(skc14,skc23) ).
cnf(u1744,negated_conjecture,
male(skc16,skc19) ).
cnf(u1751,negated_conjecture,
organism(skc16,skc19) ).
cnf(u1756,negated_conjecture,
organism(skc16,skc23) ).
cnf(u1764,negated_conjecture,
human(skc14,skc19) ).
cnf(u1769,negated_conjecture,
animate(skc14,skc19) ).
cnf(u1776,negated_conjecture,
entity(skc14,skc19) ).
cnf(u1781,negated_conjecture,
entity(skc14,skc23) ).
cnf(u1789,negated_conjecture,
human(skc16,skc19) ).
cnf(u1794,negated_conjecture,
animate(skc16,skc19) ).
cnf(u1801,negated_conjecture,
entity(skc16,skc19) ).
cnf(u1806,negated_conjecture,
entity(skc16,skc23) ).
cnf(u1814,negated_conjecture,
human(skc16,skc23) ).
cnf(u1819,negated_conjecture,
animate(skc16,skc23) ).
cnf(u1828,negated_conjecture,
impartial(skc14,skc19) ).
cnf(u1833,negated_conjecture,
impartial(skc14,skc23) ).
cnf(u1841,negated_conjecture,
impartial(skc16,skc19) ).
cnf(u1846,negated_conjecture,
impartial(skc16,skc23) ).
cnf(u1854,negated_conjecture,
living(skc14,skc19) ).
cnf(u1859,negated_conjecture,
living(skc14,skc23) ).
cnf(u1866,negated_conjecture,
living(skc16,skc19) ).
cnf(u1871,negated_conjecture,
living(skc16,skc23) ).
cnf(u1878,negated_conjecture,
human(skc14,skc23) ).
cnf(u1887,negated_conjecture,
animate(skc14,skc23) ).
cnf(u1902,negated_conjecture,
forename(skc14,skc18) ).
cnf(u1907,negated_conjecture,
forename(skc14,skc20) ).
cnf(u1912,negated_conjecture,
forename(skc14,skc25) ).
cnf(u1917,negated_conjecture,
forename(skc14,skc24) ).
cnf(u1923,negated_conjecture,
relname(skc14,skc18) ).
cnf(u1932,negated_conjecture,
forename(skc16,skc18) ).
cnf(u1937,negated_conjecture,
forename(skc16,skc20) ).
cnf(u1942,negated_conjecture,
forename(skc16,skc25) ).
cnf(u1947,negated_conjecture,
forename(skc16,skc24) ).
cnf(u1953,negated_conjecture,
relname(skc14,skc20) ).
cnf(u1962,negated_conjecture,
relname(skc14,skc25) ).
cnf(u1967,negated_conjecture,
relname(skc14,skc24) ).
cnf(u1977,negated_conjecture,
relname(skc16,skc18) ).
cnf(u1982,negated_conjecture,
relname(skc16,skc20) ).
cnf(u1987,negated_conjecture,
relname(skc16,skc25) ).
cnf(u1992,negated_conjecture,
relname(skc16,skc24) ).
cnf(u2000,negated_conjecture,
vincent_forename(skc14,skc20) ).
cnf(u2005,negated_conjecture,
vincent_forename(skc14,skc18) ).
cnf(u2013,negated_conjecture,
vincent_forename(skc16,skc20) ).
cnf(u2018,negated_conjecture,
vincent_forename(skc16,skc18) ).
cnf(u2026,negated_conjecture,
jules_forename(skc14,skc24) ).
cnf(u2031,negated_conjecture,
jules_forename(skc14,skc25) ).
cnf(u2039,negated_conjecture,
jules_forename(skc16,skc24) ).
cnf(u2044,negated_conjecture,
jules_forename(skc16,skc25) ).
cnf(u2091,negated_conjecture,
skc24 = skc25 ).
cnf(u2109,negated_conjecture,
skc20 = skc18 ).
cnf(u2156,negated_conjecture,
skc14 = skc16 ).
cnf(u2226,negated_conjecture,
unisex(skc16,skc26) ).
cnf(u2231,negated_conjecture,
nonexistent(skc16,skc26) ).
cnf(u2236,negated_conjecture,
singleton(skc16,skc26) ).
cnf(u2241,negated_conjecture,
specific(skc16,skc26) ).
cnf(u2246,negated_conjecture,
thing(skc16,skc26) ).
cnf(u2251,negated_conjecture,
eventuality(skc16,skc26) ).
cnf(u2256,negated_conjecture,
event(skc16,skc26) ).
cnf(u2261,negated_conjecture,
present(skc16,skc26) ).
cnf(u2266,negated_conjecture,
smoke(skc16,skc26) ).
cnf(u2271,negated_conjecture,
agent(skc16,skc26,skc23) ).
cnf(u2276,negated_conjecture,
theme(skc13,skc15,skc16) ).
cnf(u2402,negated_conjecture,
~ unisex(skc16,skc23) ).
cnf(u2418,negated_conjecture,
~ unisex(skc16,skc19) ).
cnf(u2442,negated_conjecture,
~ nonhuman(skc16,skc19) ).
cnf(u2450,negated_conjecture,
~ nonhuman(skc16,skc23) ).
cnf(u2476,negated_conjecture,
~ nonexistent(skc13,skc23) ).
cnf(u2482,negated_conjecture,
existent(skc16,skc23) ).
cnf(u2503,negated_conjecture,
singleton(skc13,skc19) ).
cnf(u2509,negated_conjecture,
thing(skc16,skc19) ).
cnf(u2518,negated_conjecture,
specific(skc16,skc19) ).
cnf(u2527,negated_conjecture,
~ nonexistent(skc13,skc19) ).
cnf(u2533,negated_conjecture,
existent(skc16,skc19) ).
cnf(u2547,negated_conjecture,
singleton(skc13,skc20) ).
cnf(u2553,negated_conjecture,
thing(skc16,skc20) ).
cnf(u2565,negated_conjecture,
nonhuman(skc16,skc20) ).
cnf(u2579,negated_conjecture,
~ specific(skc13,skc20) ).
cnf(u2585,negated_conjecture,
general(skc16,skc20) ).
cnf(u2597,negated_conjecture,
unisex(skc16,skc20) ).
cnf(u2637,negated_conjecture,
singleton(skc13,skc24) ).
cnf(u2643,negated_conjecture,
thing(skc16,skc24) ).
cnf(u2656,negated_conjecture,
nonhuman(skc16,skc24) ).
cnf(u2670,negated_conjecture,
~ specific(skc13,skc24) ).
cnf(u2676,negated_conjecture,
general(skc16,skc24) ).
cnf(u2698,negated_conjecture,
unisex(skc16,skc24) ).
cnf(u2836,negated_conjecture,
~ specific(skc16,skc16) ).
cnf(u2874,negated_conjecture,
singleton(skc16,skc23) ).
cnf(u2908,negated_conjecture,
~ nonexistent(skc16,skc23) ).
cnf(u2929,negated_conjecture,
singleton(skc16,skc19) ).
cnf(u2984,negated_conjecture,
~ nonexistent(skc16,skc19) ).
cnf(u2992,negated_conjecture,
singleton(skc16,skc20) ).
cnf(u3000,negated_conjecture,
~ specific(skc16,skc20) ).
cnf(u3008,negated_conjecture,
singleton(skc16,skc24) ).
cnf(u3016,negated_conjecture,
~ specific(skc16,skc24) ).
cnf(u730,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc26) ) ).
cnf(u729,negated_conjecture,
( ~ accessible_world(skc13,X0)
| present(X0,skc17) ) ).
cnf(u702,negated_conjecture,
( ~ singleton(skc13,X0)
| singleton(skc14,X0) ) ).
cnf(u741,negated_conjecture,
( ~ relation(skc13,X0)
| relation(skc14,X0) ) ).
cnf(clause56,axiom,
( ~ accessible_world(X0,X1)
| ~ existent(X0,X2)
| existent(X1,X2) ) ).
cnf(u701,negated_conjecture,
( ~ thing(skc13,X0)
| thing(skc16,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(u755,negated_conjecture,
( ~ state(skc13,X0)
| state(skc14,X0) ) ).
cnf(u2688,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc16)
| ~ accessible_world(skc16,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc15,X3)
| ~ agent(X0,X1,X3)
| skc16 = X2 ) ).
cnf(clause49,axiom,
( ~ accessible_world(X0,X1)
| ~ nonhuman(X0,X2)
| nonhuman(X1,X2) ) ).
cnf(u744,negated_conjecture,
( ~ abstraction(skc13,X0)
| abstraction(skc16,X0) ) ).
cnf(u972,negated_conjecture,
unisex(skc16,skf1(X0)) ).
cnf(u928,negated_conjecture,
( of(X0,skc25,skc23)
| ~ accessible_world(skc13,X0) ) ).
cnf(u731,negated_conjecture,
( ~ accessible_world(skc13,X0)
| think_believe_consider(X0,skc15) ) ).
cnf(u1387,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc15) ) ).
cnf(u720,negated_conjecture,
( ~ unisex(skc13,X0)
| unisex(skc14,X0) ) ).
cnf(u781,negated_conjecture,
( ~ organism(skc13,X0)
| organism(skc14,X0) ) ).
cnf(u692,negated_conjecture,
( ~ eventuality(skc13,X0)
| eventuality(skc14,X0) ) ).
cnf(u962,negated_conjecture,
( ~ of(skc13,X0,skc23)
| ~ forename(skc13,X0)
| skc25 = X0 ) ).
cnf(clause43,axiom,
( ~ accessible_world(X0,X1)
| ~ unisex(X0,X2)
| unisex(X1,X2) ) ).
cnf(u757,negated_conjecture,
( ~ man(skc13,X0)
| man(skc14,X0) ) ).
cnf(clause52,axiom,
( ~ accessible_world(X0,X1)
| ~ man(X0,X2)
| man(X1,X2) ) ).
cnf(clause26,axiom,
( ~ man(X0,X1)
| male(X0,X1) ) ).
cnf(clause46,axiom,
( ~ accessible_world(X0,X1)
| ~ proposition(X0,X2)
| proposition(X1,X2) ) ).
cnf(u705,negated_conjecture,
( ~ specific(skc13,X0)
| specific(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(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(u2057,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc14)
| ~ accessible_world(skc13,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc15,X3)
| ~ agent(X0,X1,X3)
| skc14 = X2 ) ).
cnf(clause25,axiom,
( ~ human_person(X0,X1)
| animate(X0,X1) ) ).
cnf(clause28,axiom,
( ~ relname(X0,X1)
| relation(X0,X1) ) ).
cnf(u2053,negated_conjecture,
( ~ accessible_world(skc14,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc26,skc23) ) ).
cnf(u2051,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc17,skc19) ) ).
cnf(clause19,axiom,
( ~ entity(X0,X1)
| thing(X0,X1) ) ).
cnf(clause22,axiom,
( ~ organism(X0,X1)
| impartial(X0,X1) ) ).
cnf(u2469,negated_conjecture,
( agent(X0,skc26,skc23)
| ~ accessible_world(skc16,X0) ) ).
cnf(clause21,axiom,
( ~ entity(X0,X1)
| existent(X0,X1) ) ).
cnf(clause8,axiom,
( ~ proposition(X0,X1)
| relation(X0,X1) ) ).
cnf(u2717,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc20,skc19) ) ).
cnf(clause15,axiom,
( ~ state(X0,X1)
| event(X0,X1) ) ).
cnf(clause2,axiom,
( ~ event(X0,X1)
| eventuality(X0,X1) ) ).
cnf(u838,negated_conjecture,
( ~ male(skc13,X0)
| male(skc16,X0) ) ).
cnf(clause1,axiom,
( ~ smoke(X0,X1)
| event(X0,X1) ) ).
cnf(u794,negated_conjecture,
( ~ impartial(skc13,X0)
| impartial(skc16,X0) ) ).
cnf(u900,negated_conjecture,
( theme(X0,skc17,skc16)
| ~ accessible_world(skc13,X0) ) ).
cnf(u790,negated_conjecture,
( ~ entity(skc13,X0)
| entity(skc16,X0) ) ).
cnf(u743,negated_conjecture,
( ~ abstraction(skc13,X0)
| abstraction(skc14,X0) ) ).
cnf(u2305,negated_conjecture,
( theme(X0,skc17,skc16)
| ~ accessible_world(skc16,X0) ) ).
cnf(u963,negated_conjecture,
( ~ of(skc13,X0,skc23)
| ~ forename(skc13,X0)
| skc24 = X0 ) ).
cnf(u1374,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc15) ) ).
cnf(u817,negated_conjecture,
( ~ animate(skc13,X0)
| animate(skc14,X0) ) ).
cnf(u813,negated_conjecture,
( ~ living(skc13,X0)
| living(skc14,X0) ) ).
cnf(u748,negated_conjecture,
( ~ general(skc13,X0)
| general(skc16,X0) ) ).
cnf(u780,negated_conjecture,
( ~ human_person(skc13,X0)
| human_person(skc16,X0) ) ).
cnf(clause4,axiom,
( ~ thing(X0,X1)
| singleton(X0,X1) ) ).
cnf(u758,negated_conjecture,
( ~ man(skc13,X0)
| man(skc16,X0) ) ).
cnf(u2061,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc16)
| ~ accessible_world(skc13,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc17,X3)
| ~ agent(X0,X1,X3)
| skc16 = X2 ) ).
cnf(u970,negated_conjecture,
( ~ theme(skc13,X0,X1)
| ~ think_believe_consider(skc13,X0)
| ~ proposition(skc13,X1)
| ~ agent(skc13,skc17,X2)
| ~ agent(skc13,X0,X2)
| skc16 = X1 ) ).
cnf(u843,negated_conjecture,
( ~ vincent_forename(skc13,X0)
| vincent_forename(skc14,X0) ) ).
cnf(u2290,negated_conjecture,
( agent(X0,skc17,skc19)
| ~ accessible_world(skc16,X0) ) ).
cnf(u815,negated_conjecture,
( ~ human(skc13,X0)
| human(skc14,X0) ) ).
cnf(u842,negated_conjecture,
( ~ relname(skc13,X0)
| relname(skc16,X0) ) ).
cnf(u2646,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc15,skc19) ) ).
cnf(u818,negated_conjecture,
( ~ animate(skc13,X0)
| animate(skc16,X0) ) ).
cnf(u734,negated_conjecture,
( ~ proposition(skc13,X0)
| proposition(skc16,X0) ) ).
cnf(clause58,axiom,
( ~ accessible_world(X0,X1)
| ~ living(X0,X2)
| living(X1,X2) ) ).
cnf(u733,negated_conjecture,
( ~ proposition(skc13,X0)
| proposition(skc14,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(u703,negated_conjecture,
( ~ singleton(skc13,X0)
| singleton(skc16,X0) ) ).
cnf(u2066,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc20)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc19)
| skc20 = X1 ) ).
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(u841,negated_conjecture,
( ~ relname(skc13,X0)
| relname(skc14,X0) ) ).
cnf(u874,negated_conjecture,
( agent(X0,skf1(X1),X1)
| ~ accessible_world(skc16,X0)
| ~ man(skc16,X1) ) ).
cnf(u713,negated_conjecture,
( ~ nonexistent(skc13,X0)
| nonexistent(skc16,X0) ) ).
cnf(clause53,axiom,
( ~ accessible_world(X0,X1)
| ~ human_person(X0,X2)
| human_person(X1,X2) ) ).
cnf(u2047,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| present(X1,skf1(X2)) ) ).
cnf(u2072,negated_conjecture,
( ~ of(X0,X1,skc23)
| ~ forename(X0,X1)
| ~ forename(X0,skc25)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc23)
| skc25 = X1 ) ).
cnf(clause40,axiom,
( ~ accessible_world(X0,X1)
| ~ singleton(X0,X2)
| singleton(X1,X2) ) ).
cnf(u685,negated_conjecture,
( ~ event(skc13,X0)
| event(skc16,X0) ) ).
cnf(clause47,axiom,
( ~ accessible_world(X0,X1)
| ~ relation(X0,X2)
| relation(X1,X2) ) ).
cnf(clause34,axiom,
( ~ existent(X0,X1)
| ~ nonexistent(X0,X1) ) ).
cnf(u837,negated_conjecture,
( ~ male(skc13,X0)
| male(skc14,X0) ) ).
cnf(u2334,negated_conjecture,
( be(X0,skc22,skc23,skc23)
| ~ accessible_world(skc16,X0) ) ).
cnf(u793,negated_conjecture,
( ~ impartial(skc13,X0)
| impartial(skc14,X0) ) ).
cnf(u871,negated_conjecture,
( agent(X0,skc15,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u665,negated_conjecture,
( ~ smoke(skc13,X0)
| smoke(skc16,X0) ) ).
cnf(u728,negated_conjecture,
( ~ accessible_world(skc13,X0)
| present(X0,skc15) ) ).
cnf(u2284,negated_conjecture,
singleton(skc16,skf1(X0)) ).
cnf(u789,negated_conjecture,
( ~ entity(skc13,X0)
| entity(skc14,X0) ) ).
cnf(u700,negated_conjecture,
( ~ thing(skc13,X0)
| thing(skc14,X0) ) ).
cnf(u704,negated_conjecture,
( ~ specific(skc13,X0)
| specific(skc14,X0) ) ).
cnf(u2496,negated_conjecture,
( ~ theme(skc13,X0,X1)
| ~ think_believe_consider(skc13,X0)
| ~ proposition(skc13,X1)
| ~ agent(skc13,skc15,X2)
| ~ agent(skc13,X0,X2)
| skc16 = X1 ) ).
cnf(u839,negated_conjecture,
( ~ forename(skc13,X0)
| forename(skc14,X0) ) ).
cnf(u2286,negated_conjecture,
( agent(X0,skc15,skc19)
| ~ accessible_world(skc16,X0) ) ).
cnf(clause33,axiom,
( ~ human(X0,X1)
| ~ nonhuman(X0,X1) ) ).
cnf(u2709,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc16)
| ~ accessible_world(skc16,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc17,X3)
| ~ agent(X0,X1,X3)
| skc16 = X2 ) ).
cnf(u791,negated_conjecture,
( ~ existent(skc13,X0)
| existent(skc14,X0) ) ).
cnf(u816,negated_conjecture,
( ~ human(skc13,X0)
| human(skc16,X0) ) ).
cnf(u971,negated_conjecture,
( ~ theme(skc13,X0,X1)
| ~ think_believe_consider(skc13,X0)
| ~ proposition(skc13,X1)
| ~ agent(skc13,skc15,X2)
| ~ agent(skc13,X0,X2)
| skc14 = X1 ) ).
cnf(clause64,axiom,
( ~ accessible_world(X0,X1)
| ~ vincent_forename(X0,X2)
| vincent_forename(X1,X2) ) ).
cnf(u771,negated_conjecture,
( present(X0,skf1(X1))
| ~ accessible_world(skc16,X0) ) ).
cnf(u71,axiom,
( ~ of(X0,X2,X3)
| ~ forename(X0,X1)
| ~ forename(X0,X2)
| ~ of(X0,X1,X3)
| ~ entity(X0,X3)
| X1 = X2 ) ).
cnf(clause36,axiom,
( ~ accessible_world(X0,X1)
| ~ smoke(X0,X2)
| smoke(X1,X2) ) ).
cnf(clause27,axiom,
( ~ forename(X0,X1)
| relname(X0,X1) ) ).
cnf(clause30,axiom,
( ~ jules_forename(X0,X1)
| forename(X0,X1) ) ).
cnf(clause29,axiom,
( ~ vincent_forename(X0,X1)
| forename(X0,X1) ) ).
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(u846,negated_conjecture,
( ~ jules_forename(skc13,X0)
| jules_forename(skc16,X0) ) ).
cnf(clause9,axiom,
( ~ relation(X0,X1)
| abstraction(X0,X1) ) ).
cnf(clause12,axiom,
( ~ abstraction(X0,X1)
| general(X0,X1) ) ).
cnf(u965,negated_conjecture,
( ~ of(skc13,X0,skc19)
| ~ forename(skc13,X0)
| skc18 = X0 ) ).
cnf(clause3,axiom,
( ~ eventuality(X0,X1)
| thing(X0,X1) ) ).
cnf(clause6,axiom,
( ~ eventuality(X0,X1)
| nonexistent(X0,X1) ) ).
cnf(u2070,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc24,skc23) ) ).
cnf(clause5,axiom,
( ~ eventuality(X0,X1)
| specific(X0,X1) ) ).
cnf(u2626,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc16)
| ~ accessible_world(skc13,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc15,X3)
| ~ agent(X0,X1,X3)
| skc16 = X2 ) ).
cnf(u2063,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc18)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc19)
| skc18 = X1 ) ).
cnf(u2704,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc17,skc16) ) ).
cnf(u746,negated_conjecture,
( ~ nonhuman(skc13,X0)
| nonhuman(skc16,X0) ) ).
cnf(u873,negated_conjecture,
( agent(X0,skc26,skc23)
| ~ accessible_world(skc14,X0) ) ).
cnf(u745,negated_conjecture,
( ~ nonhuman(skc13,X0)
| nonhuman(skc14,X0) ) ).
cnf(u1388,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc17) ) ).
cnf(u840,negated_conjecture,
( ~ forename(skc13,X0)
| forename(skc16,X0) ) ).
cnf(u792,negated_conjecture,
( ~ existent(skc13,X0)
| existent(skc16,X0) ) ).
cnf(u845,negated_conjecture,
( ~ jules_forename(skc13,X0)
| jules_forename(skc14,X0) ) ).
cnf(u756,negated_conjecture,
( ~ state(skc13,X0)
| state(skc16,X0) ) ).
cnf(u747,negated_conjecture,
( ~ general(skc13,X0)
| general(skc14,X0) ) ).
cnf(u899,negated_conjecture,
( theme(X0,skc15,skc14)
| ~ accessible_world(skc13,X0) ) ).
cnf(u1427,negated_conjecture,
( ~ accessible_world(skc14,X0)
| think_believe_consider(X0,skc15) ) ).
cnf(clause62,axiom,
( ~ accessible_world(X0,X1)
| ~ forename(X0,X2)
| forename(X1,X2) ) ).
cnf(u2049,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc15,skc19) ) ).
cnf(u1401,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc17) ) ).
cnf(u2067,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc20,skc19) ) ).
cnf(u2727,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc24,skc23) ) ).
cnf(clause66,axiom,
( ~ agent(X0,X2,X3)
| ~ accessible_world(X0,X1)
| agent(X1,X2,X3) ) ).
cnf(u974,negated_conjecture,
specific(skc16,skf1(X0)) ).
cnf(u742,negated_conjecture,
( ~ relation(skc13,X0)
| relation(skc16,X0) ) ).
cnf(u684,negated_conjecture,
( ~ event(skc13,X0)
| event(skc14,X0) ) ).
cnf(clause41,axiom,
( ~ accessible_world(X0,X1)
| ~ specific(X0,X2)
| specific(X1,X2) ) ).
cnf(clause44,axiom,
( ~ present(X0,X2)
| ~ accessible_world(X0,X1)
| present(X1,X2) ) ).
cnf(u2293,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc26,skc23) ) ).
cnf(u2073,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc25,skc23) ) ).
cnf(clause59,axiom,
( ~ accessible_world(X0,X1)
| ~ human(X0,X2)
| human(X1,X2) ) ).
cnf(u926,negated_conjecture,
( of(X0,skc20,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2312,negated_conjecture,
( of(X0,skc20,skc19)
| ~ accessible_world(skc16,X0) ) ).
cnf(u721,negated_conjecture,
( ~ unisex(skc13,X0)
| unisex(skc16,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(u693,negated_conjecture,
( ~ eventuality(skc13,X0)
| eventuality(skc16,X0) ) ).
cnf(clause55,axiom,
( ~ accessible_world(X0,X1)
| ~ entity(X0,X2)
| entity(X1,X2) ) ).
cnf(u2069,negated_conjecture,
( ~ of(X0,X1,skc23)
| ~ forename(X0,X1)
| ~ forename(X0,skc24)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc23)
| skc24 = X1 ) ).
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(u779,negated_conjecture,
( ~ human_person(skc13,X0)
| human_person(skc14,X0) ) ).
cnf(u1477,negated_conjecture,
( ~ accessible_world(skc14,X0)
| think_believe_consider(X0,skc17) ) ).
cnf(u2056,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc15,skc14) ) ).
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(clause68,axiom,
( ~ of(X0,X2,X3)
| ~ accessible_world(X0,X1)
| of(X1,X2,X3) ) ).
cnf(clause37,axiom,
( ~ accessible_world(X0,X1)
| ~ event(X0,X2)
| event(X1,X2) ) ).
cnf(clause24,axiom,
( ~ human_person(X0,X1)
| human(X0,X1) ) ).
cnf(u814,negated_conjecture,
( ~ living(skc13,X0)
| living(skc16,X0) ) ).
cnf(u964,negated_conjecture,
( ~ of(skc13,X0,skc19)
| ~ forename(skc13,X0)
| skc20 = X0 ) ).
cnf(clause31,axiom,
( ~ male(X0,X1)
| ~ unisex(X0,X1) ) ).
cnf(clause18,axiom,
( ~ organism(X0,X1)
| entity(X0,X1) ) ).
cnf(clause17,axiom,
( ~ human_person(X0,X1)
| organism(X0,X1) ) ).
cnf(u2682,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc15,skc16) ) ).
cnf(u973,negated_conjecture,
nonexistent(skc16,skf1(X0)) ).
cnf(u2323,negated_conjecture,
( of(X0,skc24,skc23)
| ~ accessible_world(skc16,X0) ) ).
cnf(u712,negated_conjecture,
( ~ nonexistent(skc13,X0)
| nonexistent(skc14,X0) ) ).
cnf(u872,negated_conjecture,
( agent(X0,skc17,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u925,negated_conjecture,
( of(X0,skc18,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u953,negated_conjecture,
( be(X0,skc22,skc23,skc23)
| ~ accessible_world(skc13,X0) ) ).
cnf(u664,negated_conjecture,
( ~ smoke(skc13,X0)
| smoke(skc14,X0) ) ).
cnf(u2735,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| be(X1,skc22,skc23,skc23) ) ).
cnf(u2659,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc17,skc19) ) ).
cnf(u2726,negated_conjecture,
( ~ of(X0,X1,skc23)
| ~ forename(X0,X1)
| ~ forename(X0,skc24)
| ~ accessible_world(skc16,X0)
| ~ entity(X0,skc23)
| skc24 = X1 ) ).
cnf(u2299,negated_conjecture,
( theme(X0,skc15,skc16)
| ~ accessible_world(skc16,X0) ) ).
cnf(u975,negated_conjecture,
thing(skc16,skf1(X0)) ).
cnf(u844,negated_conjecture,
( ~ vincent_forename(skc13,X0)
| vincent_forename(skc16,X0) ) ).
cnf(u927,negated_conjecture,
( of(X0,skc24,skc23)
| ~ accessible_world(skc13,X0) ) ).
cnf(u764,negated_conjecture,
eventuality(skc16,skf1(X0)) ).
cnf(clause20,axiom,
( ~ entity(X0,X1)
| specific(X0,X1) ) ).
cnf(clause11,axiom,
( ~ abstraction(X0,X1)
| nonhuman(X0,X1) ) ).
cnf(u2075,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| be(X1,skc22,skc23,skc23) ) ).
cnf(clause14,axiom,
( ~ state(X0,X1)
| eventuality(X0,X1) ) ).
cnf(u2181,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc26) ) ).
cnf(u2619,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc15,skc16) ) ).
cnf(clause13,axiom,
( ~ abstraction(X0,X1)
| unisex(X0,X1) ) ).
cnf(u2064,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc18,skc19) ) ).
cnf(clause7,axiom,
( ~ eventuality(X0,X1)
| unisex(X0,X1) ) ).
cnf(u2184,negated_conjecture,
( theme(X0,skc15,skc16)
| ~ accessible_world(skc13,X0) ) ).
cnf(u1440,negated_conjecture,
( ~ accessible_world(skc16,X0)
| think_believe_consider(X0,skc17) ) ).
cnf(u2060,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc17,skc16) ) ).
cnf(u2716,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc20)
| ~ accessible_world(skc16,X0)
| ~ entity(X0,skc19)
| skc20 = X1 ) ).
cnf(u782,negated_conjecture,
( ~ organism(skc13,X0)
| organism(skc16,X0) ) ).
cnf(clause110,negated_conjecture,
( agent(skc16,skf1(X0),X0)
| ~ man(skc16,X0) ) ).
cnf(u1414,negated_conjecture,
( ~ accessible_world(skc16,X0)
| think_believe_consider(X0,skc15) ) ).
cnf(u732,negated_conjecture,
( ~ accessible_world(skc13,X0)
| think_believe_consider(X0,skc17) ) ).
cnf(u2130,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ man(skc16,X1)
| ~ accessible_world(X0,X2)
| agent(X2,skf1(X1),X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP248-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.45 % Computer : n009.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sun Sep 27 18:37:00 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.51 Running first-order theorem proving
% 0.24/0.51 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
% 8.82/2.64 % (2318656)Input is clausal, will run a generic CNF schedule.
% 8.82/2.64 % (2318674)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4247398592:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.82/2.64 % (2318669)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=1459163457:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.82/2.64 % (2318670)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2063296754:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.82/2.64 % (2318671)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1831218619:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.82/2.64 % (2318674)Refutation not found, incomplete strategy
% 8.82/2.64 % (2318674)------------------------------
% 8.82/2.64 % (2318674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.64 % (2318674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.64 % (2318674)CaDiCaL version: 2.1.3
% 8.82/2.64 % (2318674)Termination reason: Refutation not found, incomplete strategy
% 8.82/2.64 % (2318674)Time elapsed: 0.046 s
% 8.82/2.64 % (2318674)Peak memory usage: 89 MB
% 8.82/2.64 % (2318674)Instructions burned: 71 (million)
% 8.82/2.64 % (2318673)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2599339943:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.82/2.64 % (2318672)lrs+10_1_sil=8000:sp=occurrence:random_seed=3179971802:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.82/2.64 % (2318675)dis-21_1_sil=8000:lcm=predicate:random_seed=3190441970: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)
% 8.82/2.64 % (2318672)Refutation not found, incomplete strategy
% 8.82/2.64 % (2318672)------------------------------
% 8.82/2.64 % (2318672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.64 % (2318672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.64 % (2318672)CaDiCaL version: 2.1.3
% 8.82/2.64 % (2318672)Termination reason: Refutation not found, incomplete strategy
% 8.82/2.64 % (2318672)Time elapsed: 0.026 s
% 8.82/2.64 % (2318672)Peak memory usage: 88 MB
% 8.82/2.64 % (2318672)Instructions burned: 22 (million)
% 8.82/2.64 % (2318675)Instruction limit reached!
% 8.82/2.64 % (2318675)------------------------------
% 8.82/2.64 % (2318675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.64 % (2318675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.64 % (2318675)CaDiCaL version: 2.1.3
% 8.82/2.64 % (2318675)Termination reason: Instruction limit
% 8.82/2.64 % (2318675)Termination phase: Saturation
% 8.82/2.64 % (2318675)Time elapsed: 0.082 s
% 8.82/2.64 % (2318675)Peak memory usage: 88 MB
% 8.82/2.64 % (2318675)Instructions burned: 118 (million)
% 8.82/2.64 % (2318673)Instruction limit reached!
% 8.82/2.64 % (2318673)------------------------------
% 8.82/2.64 % (2318673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.64 % (2318673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.64 % (2318673)CaDiCaL version: 2.1.3
% 8.82/2.64 % (2318673)Termination reason: Instruction limit
% 8.82/2.64 % (2318673)Termination phase: Saturation
% 8.82/2.64 % (2318673)Time elapsed: 0.111 s
% 8.82/2.64 % (2318673)Peak memory usage: 88 MB
% 8.82/2.64 % (2318673)Instructions burned: 114 (million)
% 8.82/2.64 % (2318674)------------------------------
% 8.82/2.64 % (2318674)------------------------------
% 8.82/2.64 % (2318683)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=2416322576:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 8.82/2.64 % (2318684)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3532579737:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 8.82/2.64 % (2318672)------------------------------
% 8.82/2.64 % (2318672)------------------------------
% 8.82/2.64 % (2318684)Refutation not found, incomplete strategy
% 8.82/2.64 % (2318684)------------------------------
% 8.82/2.64 % (2318684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.65 % (2318684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.65 % (2318684)CaDiCaL version: 2.1.3
% 8.82/2.65 % (2318684)Termination reason: Refutation not found, incomplete strategy
% 8.82/2.65 % (2318684)Time elapsed: 0.019 s
% 8.82/2.65 % (2318684)Peak memory usage: 89 MB
% 8.82/2.65 % (2318684)Instructions burned: 19 (million)
% 8.82/2.65 % (2318685)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1118307878:st=4:i=219:sd=3:ss=axioms_2994 on theBenchmark for (2994ds/219Mi)
% 8.82/2.65 % (2318683)Instruction limit reached!
% 8.82/2.65 % (2318683)------------------------------
% 8.82/2.65 % (2318683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.65 % (2318683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.65 % (2318683)CaDiCaL version: 2.1.3
% 8.82/2.65 % (2318683)Termination reason: Instruction limit
% 8.82/2.65 % (2318683)Termination phase: Saturation
% 8.82/2.65 % (2318683)Time elapsed: 0.124 s
% 8.82/2.65 % (2318683)Peak memory usage: 89 MB
% 8.82/2.65 % (2318683)Instructions burned: 143 (million)
% 8.82/2.65 % (2318685)Instruction limit reached!
% 8.82/2.65 % (2318685)------------------------------
% 8.82/2.65 % (2318685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.65 % (2318685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.65 % (2318685)CaDiCaL version: 2.1.3
% 8.82/2.65 % (2318685)Termination reason: Instruction limit
% 8.82/2.65 % (2318685)Termination phase: Saturation
% 8.82/2.65 % (2318685)Time elapsed: 0.080 s
% 8.82/2.65 % (2318685)Peak memory usage: 88 MB
% 8.82/2.65 % (2318685)Instructions burned: 219 (million)
% 8.82/2.65 % (2318688)lrs+10_64_to=lpo:sil=8000:random_seed=715256229:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 8.82/2.65 % (2318691)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=85709186:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 8.82/2.65 % (2318684)------------------------------
% 8.82/2.65 % (2318684)------------------------------
% 8.82/2.65 % (2318691)First to succeed.
% 8.82/2.65 % (2318691)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2318656"
% 8.82/2.65 % (2318690)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2937965959:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 8.82/2.65 % (2318688)Instruction limit reached!
% 8.82/2.65 % (2318688)------------------------------
% 8.82/2.65 % (2318688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.65 % (2318688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.65 % (2318688)CaDiCaL version: 2.1.3
% 8.82/2.65 % (2318688)Termination reason: Instruction limit
% 8.82/2.65 % (2318688)Termination phase: Saturation
% 8.82/2.65 % (2318688)Time elapsed: 0.092 s
% 8.82/2.65 % (2318688)Peak memory usage: 88 MB
% 8.82/2.65 % (2318688)Instructions burned: 127 (million)
% 8.82/2.65 % (2318690)Refutation not found, incomplete strategy
% 8.82/2.65 % (2318690)------------------------------
% 8.82/2.65 % (2318690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.65 % (2318690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.65 % (2318690)CaDiCaL version: 2.1.3
% 8.82/2.65 % (2318690)Termination reason: Refutation not found, incomplete strategy
% 8.82/2.65 % (2318690)Time elapsed: 0.048 s
% 8.82/2.65 % (2318690)Peak memory usage: 88 MB
% 8.82/2.65 % (2318690)Instructions burned: 38 (million)
% 8.82/2.65 % SZS status Satisfiable for theBenchmark
% 8.82/2.65 % SZS output start Saturation.
% See solution above
% 10.70/3.03 % SZS output start Definitions and Model Updates.
% 10.70/3.03 for all inputs,
% 10.70/3.03 define actual_world(X0) := $true
% 10.70/3.03 % SZS output end Definitions and Model Updates.
% 10.70/3.03 % (2318691)------------------------------
% 10.70/3.03 % (2318691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/3.03 % (2318691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/3.03 % (2318691)CaDiCaL version: 2.1.3
% 10.70/3.03 % (2318691)Termination reason: Satisfiable
% 10.70/3.03 % (2318691)Time elapsed: 0.037 s
% 10.70/3.03 % (2318691)Peak memory usage: 90 MB
% 10.70/3.03 % (2318691)Instructions burned: 59 (million)
% 10.70/3.03 % (2318691)------------------------------
% 10.70/3.03 % (2318691)------------------------------
% 10.70/3.03 % (2318656)Success in time 1.387 s
% 10.70/3.03 % Vampire exiting
%------------------------------------------------------------------------------