%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP249-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:08:12 PM UTC 2026
% Result : Satisfiable 8.87s 2.28s
% Output : Saturation 10.33s
% 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,skc24,skc25,skc25) ).
cnf(u135,negated_conjecture,
theme(skc13,skc15,skc14) ).
cnf(u140,negated_conjecture,
theme(skc13,skc17,skc16) ).
cnf(u145,negated_conjecture,
agent(skc14,skc21,skc19) ).
cnf(u150,negated_conjecture,
agent(skc13,skc15,skc19) ).
cnf(u155,negated_conjecture,
agent(skc13,skc17,skc19) ).
cnf(u160,negated_conjecture,
of(skc13,skc18,skc19) ).
cnf(u165,negated_conjecture,
of(skc13,skc20,skc19) ).
cnf(u170,negated_conjecture,
of(skc13,skc22,skc19) ).
cnf(u175,negated_conjecture,
of(skc13,skc26,skc25) ).
cnf(u180,negated_conjecture,
state(skc13,skc24) ).
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,
forename(skc13,skc22) ).
cnf(u250,negated_conjecture,
jules_forename(skc13,skc22) ).
cnf(u255,negated_conjecture,
smoke(skc14,skc21) ).
cnf(u260,negated_conjecture,
present(skc14,skc21) ).
cnf(u265,negated_conjecture,
man(skc13,skc19) ).
cnf(u270,negated_conjecture,
vincent_forename(skc13,skc20) ).
cnf(u275,negated_conjecture,
forename(skc13,skc20) ).
cnf(u280,negated_conjecture,
event(skc14,skc21) ).
cnf(u285,negated_conjecture,
man(skc13,skc25) ).
cnf(u290,negated_conjecture,
forename(skc13,skc26) ).
cnf(u295,negated_conjecture,
jules_forename(skc13,skc26) ).
cnf(u304,negated_conjecture,
eventuality(skc14,skc21) ).
cnf(u309,negated_conjecture,
eventuality(skc13,skc17) ).
cnf(u314,negated_conjecture,
eventuality(skc13,skc15) ).
cnf(u320,negated_conjecture,
thing(skc14,skc21) ).
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,skc21) ).
cnf(u356,negated_conjecture,
singleton(skc14,skc21) ).
cnf(u364,negated_conjecture,
nonexistent(skc13,skc15) ).
cnf(u369,negated_conjecture,
nonexistent(skc13,skc17) ).
cnf(u374,negated_conjecture,
nonexistent(skc14,skc21) ).
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,skc21) ).
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,skc24) ).
cnf(u443,negated_conjecture,
thing(skc13,skc24) ).
cnf(u448,negated_conjecture,
specific(skc13,skc24) ).
cnf(u453,negated_conjecture,
nonexistent(skc13,skc24) ).
cnf(u458,negated_conjecture,
unisex(skc13,skc24) ).
cnf(u464,negated_conjecture,
event(skc13,skc24) ).
cnf(u472,negated_conjecture,
human_person(skc13,skc25) ).
cnf(u477,negated_conjecture,
human_person(skc13,skc19) ).
cnf(u483,negated_conjecture,
organism(skc13,skc25) ).
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,skc25) ).
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,skc25) ).
cnf(u567,negated_conjecture,
singleton(skc13,skc24) ).
cnf(u574,negated_conjecture,
male(skc13,skc25) ).
cnf(u579,negated_conjecture,
male(skc13,skc19) ).
cnf(u588,negated_conjecture,
relname(skc13,skc18) ).
cnf(u593,negated_conjecture,
relname(skc13,skc22) ).
cnf(u598,negated_conjecture,
relname(skc13,skc20) ).
cnf(u603,negated_conjecture,
relname(skc13,skc26) ).
cnf(u609,negated_conjecture,
relation(skc13,skc18) ).
cnf(u617,negated_conjecture,
relation(skc13,skc22) ).
cnf(u625,negated_conjecture,
relation(skc13,skc20) ).
cnf(u632,negated_conjecture,
~ unisex(skc13,skc19) ).
cnf(u637,negated_conjecture,
~ unisex(skc13,skc25) ).
cnf(u643,negated_conjecture,
relation(skc13,skc26) ).
cnf(u652,negated_conjecture,
entity(skc13,skc25) ).
cnf(u657,negated_conjecture,
impartial(skc13,skc25) ).
cnf(u662,negated_conjecture,
living(skc13,skc25) ).
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,skc25) ).
cnf(u710,negated_conjecture,
abstraction(skc13,skc18) ).
cnf(u718,negated_conjecture,
abstraction(skc13,skc22) ).
cnf(u726,negated_conjecture,
abstraction(skc13,skc20) ).
cnf(u739,negated_conjecture,
abstraction(skc13,skc26) ).
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,skc25) ).
cnf(u806,negated_conjecture,
specific(skc13,skc25) ).
cnf(u811,negated_conjecture,
existent(skc13,skc25) ).
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,skc22) ).
cnf(u887,negated_conjecture,
nonhuman(skc13,skc22) ).
cnf(u892,negated_conjecture,
general(skc13,skc22) ).
cnf(u897,negated_conjecture,
unisex(skc13,skc22) ).
cnf(u908,negated_conjecture,
thing(skc13,skc20) ).
cnf(u913,negated_conjecture,
nonhuman(skc13,skc20) ).
cnf(u918,negated_conjecture,
general(skc13,skc20) ).
cnf(u923,negated_conjecture,
unisex(skc13,skc20) ).
cnf(u936,negated_conjecture,
thing(skc13,skc26) ).
cnf(u941,negated_conjecture,
nonhuman(skc13,skc26) ).
cnf(u946,negated_conjecture,
general(skc13,skc26) ).
cnf(u951,negated_conjecture,
unisex(skc13,skc26) ).
cnf(u980,negated_conjecture,
singleton(skc13,skc25) ).
cnf(u988,negated_conjecture,
event(skc14,skc24) ).
cnf(u993,negated_conjecture,
event(skc14,skc17) ).
cnf(u998,negated_conjecture,
event(skc14,skc15) ).
cnf(u1004,negated_conjecture,
eventuality(skc14,skc24) ).
cnf(u1012,negated_conjecture,
event(skc16,skc24) ).
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,skc24) ).
cnf(u1050,negated_conjecture,
eventuality(skc16,skc15) ).
cnf(u1055,negated_conjecture,
eventuality(skc16,skc17) ).
cnf(u1067,negated_conjecture,
thing(skc14,skc24) ).
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,skc14) ).
cnf(u1092,negated_conjecture,
thing(skc14,skc25) ).
cnf(u1104,negated_conjecture,
thing(skc16,skc24) ).
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,skc14) ).
cnf(u1129,negated_conjecture,
thing(skc16,skc25) ).
cnf(u1140,negated_conjecture,
singleton(skc14,skc24) ).
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,skc24) ).
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,skc24) ).
cnf(u1223,negated_conjecture,
nonexistent(skc16,skc24) ).
cnf(u1228,negated_conjecture,
unisex(skc16,skc24) ).
cnf(u1237,negated_conjecture,
specific(skc14,skc24) ).
cnf(u1242,negated_conjecture,
specific(skc14,skc17) ).
cnf(u1247,negated_conjecture,
specific(skc14,skc25) ).
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,skc25) ).
cnf(u1289,negated_conjecture,
nonexistent(skc16,skc17) ).
cnf(u1294,negated_conjecture,
unisex(skc16,skc17) ).
cnf(u1302,negated_conjecture,
nonexistent(skc14,skc24) ).
cnf(u1307,negated_conjecture,
nonexistent(skc14,skc17) ).
cnf(u1316,negated_conjecture,
unisex(skc14,skc24) ).
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,skc22) ).
cnf(u1465,negated_conjecture,
relation(skc14,skc20) ).
cnf(u1470,negated_conjecture,
relation(skc14,skc14) ).
cnf(u1475,negated_conjecture,
relation(skc14,skc26) ).
cnf(u1487,negated_conjecture,
relation(skc16,skc16) ).
cnf(u1492,negated_conjecture,
relation(skc16,skc18) ).
cnf(u1497,negated_conjecture,
relation(skc16,skc22) ).
cnf(u1502,negated_conjecture,
relation(skc16,skc20) ).
cnf(u1507,negated_conjecture,
relation(skc16,skc14) ).
cnf(u1512,negated_conjecture,
relation(skc16,skc26) ).
cnf(u1524,negated_conjecture,
abstraction(skc14,skc16) ).
cnf(u1529,negated_conjecture,
abstraction(skc14,skc18) ).
cnf(u1534,negated_conjecture,
abstraction(skc14,skc22) ).
cnf(u1539,negated_conjecture,
abstraction(skc14,skc20) ).
cnf(u1544,negated_conjecture,
abstraction(skc14,skc14) ).
cnf(u1549,negated_conjecture,
abstraction(skc14,skc26) ).
cnf(u1561,negated_conjecture,
abstraction(skc16,skc16) ).
cnf(u1566,negated_conjecture,
abstraction(skc16,skc18) ).
cnf(u1571,negated_conjecture,
abstraction(skc16,skc22) ).
cnf(u1576,negated_conjecture,
abstraction(skc16,skc20) ).
cnf(u1581,negated_conjecture,
abstraction(skc16,skc14) ).
cnf(u1586,negated_conjecture,
abstraction(skc16,skc26) ).
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,skc24) ).
cnf(u1652,negated_conjecture,
state(skc16,skc24) ).
cnf(u1661,negated_conjecture,
man(skc14,skc25) ).
cnf(u1666,negated_conjecture,
man(skc14,skc19) ).
cnf(u1675,negated_conjecture,
man(skc16,skc25) ).
cnf(u1680,negated_conjecture,
man(skc16,skc19) ).
cnf(u1687,negated_conjecture,
human_person(skc14,skc25) ).
cnf(u1692,negated_conjecture,
male(skc14,skc25) ).
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,skc25) ).
cnf(u1725,negated_conjecture,
male(skc16,skc25) ).
cnf(u1732,negated_conjecture,
organism(skc14,skc19) ).
cnf(u1737,negated_conjecture,
organism(skc14,skc25) ).
cnf(u1744,negated_conjecture,
male(skc16,skc19) ).
cnf(u1751,negated_conjecture,
organism(skc16,skc19) ).
cnf(u1756,negated_conjecture,
organism(skc16,skc25) ).
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,skc25) ).
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,skc25) ).
cnf(u1814,negated_conjecture,
human(skc16,skc25) ).
cnf(u1819,negated_conjecture,
animate(skc16,skc25) ).
cnf(u1828,negated_conjecture,
impartial(skc14,skc19) ).
cnf(u1833,negated_conjecture,
impartial(skc14,skc25) ).
cnf(u1841,negated_conjecture,
impartial(skc16,skc19) ).
cnf(u1846,negated_conjecture,
impartial(skc16,skc25) ).
cnf(u1854,negated_conjecture,
living(skc14,skc19) ).
cnf(u1859,negated_conjecture,
living(skc14,skc25) ).
cnf(u1866,negated_conjecture,
living(skc16,skc19) ).
cnf(u1871,negated_conjecture,
living(skc16,skc25) ).
cnf(u1878,negated_conjecture,
human(skc14,skc25) ).
cnf(u1887,negated_conjecture,
animate(skc14,skc25) ).
cnf(u1902,negated_conjecture,
forename(skc14,skc18) ).
cnf(u1907,negated_conjecture,
forename(skc14,skc22) ).
cnf(u1912,negated_conjecture,
forename(skc14,skc20) ).
cnf(u1917,negated_conjecture,
forename(skc14,skc26) ).
cnf(u1923,negated_conjecture,
relname(skc14,skc18) ).
cnf(u1932,negated_conjecture,
forename(skc16,skc18) ).
cnf(u1937,negated_conjecture,
forename(skc16,skc22) ).
cnf(u1942,negated_conjecture,
forename(skc16,skc20) ).
cnf(u1947,negated_conjecture,
forename(skc16,skc26) ).
cnf(u1953,negated_conjecture,
relname(skc14,skc22) ).
cnf(u1962,negated_conjecture,
relname(skc14,skc20) ).
cnf(u1967,negated_conjecture,
relname(skc14,skc26) ).
cnf(u1977,negated_conjecture,
relname(skc16,skc18) ).
cnf(u1982,negated_conjecture,
relname(skc16,skc22) ).
cnf(u1987,negated_conjecture,
relname(skc16,skc20) ).
cnf(u1992,negated_conjecture,
relname(skc16,skc26) ).
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,skc26) ).
cnf(u2031,negated_conjecture,
jules_forename(skc14,skc22) ).
cnf(u2039,negated_conjecture,
jules_forename(skc16,skc26) ).
cnf(u2044,negated_conjecture,
jules_forename(skc16,skc22) ).
cnf(u2098,negated_conjecture,
skc20 = skc22 ).
cnf(u2103,negated_conjecture,
skc22 = skc18 ).
cnf(u2111,negated_conjecture,
skc20 = skc18 ).
cnf(u2146,negated_conjecture,
jules_forename(skc16,skc20) ).
cnf(u2151,negated_conjecture,
jules_forename(skc14,skc20) ).
cnf(u2156,negated_conjecture,
jules_forename(skc13,skc20) ).
cnf(u2184,negated_conjecture,
skc14 = skc16 ).
cnf(u2254,negated_conjecture,
unisex(skc16,skc21) ).
cnf(u2259,negated_conjecture,
nonexistent(skc16,skc21) ).
cnf(u2264,negated_conjecture,
singleton(skc16,skc21) ).
cnf(u2269,negated_conjecture,
specific(skc16,skc21) ).
cnf(u2274,negated_conjecture,
thing(skc16,skc21) ).
cnf(u2279,negated_conjecture,
eventuality(skc16,skc21) ).
cnf(u2284,negated_conjecture,
event(skc16,skc21) ).
cnf(u2289,negated_conjecture,
present(skc16,skc21) ).
cnf(u2294,negated_conjecture,
smoke(skc16,skc21) ).
cnf(u2299,negated_conjecture,
agent(skc16,skc21,skc19) ).
cnf(u2304,negated_conjecture,
theme(skc13,skc15,skc16) ).
cnf(u2452,negated_conjecture,
~ unisex(skc16,skc25) ).
cnf(u2468,negated_conjecture,
~ unisex(skc16,skc19) ).
cnf(u2492,negated_conjecture,
~ nonhuman(skc16,skc19) ).
cnf(u2500,negated_conjecture,
~ nonhuman(skc16,skc25) ).
cnf(u2532,negated_conjecture,
~ nonexistent(skc13,skc25) ).
cnf(u2538,negated_conjecture,
existent(skc16,skc25) ).
cnf(u2548,negated_conjecture,
singleton(skc13,skc19) ).
cnf(u2554,negated_conjecture,
thing(skc16,skc19) ).
cnf(u2575,negated_conjecture,
specific(skc16,skc19) ).
cnf(u2584,negated_conjecture,
~ nonexistent(skc13,skc19) ).
cnf(u2590,negated_conjecture,
existent(skc16,skc19) ).
cnf(u2603,negated_conjecture,
singleton(skc13,skc20) ).
cnf(u2609,negated_conjecture,
thing(skc16,skc20) ).
cnf(u2622,negated_conjecture,
nonhuman(skc16,skc20) ).
cnf(u2635,negated_conjecture,
~ specific(skc13,skc20) ).
cnf(u2641,negated_conjecture,
general(skc16,skc20) ).
cnf(u2654,negated_conjecture,
unisex(skc16,skc20) ).
cnf(u2730,negated_conjecture,
singleton(skc13,skc26) ).
cnf(u2736,negated_conjecture,
thing(skc16,skc26) ).
cnf(u2754,negated_conjecture,
nonhuman(skc16,skc26) ).
cnf(u2772,negated_conjecture,
~ specific(skc13,skc26) ).
cnf(u2778,negated_conjecture,
general(skc16,skc26) ).
cnf(u2792,negated_conjecture,
unisex(skc16,skc26) ).
cnf(u2893,negated_conjecture,
~ specific(skc16,skc16) ).
cnf(u2930,negated_conjecture,
singleton(skc16,skc25) ).
cnf(u2959,negated_conjecture,
~ nonexistent(skc16,skc25) ).
cnf(u2973,negated_conjecture,
singleton(skc16,skc19) ).
cnf(u3041,negated_conjecture,
~ nonexistent(skc16,skc19) ).
cnf(u3049,negated_conjecture,
singleton(skc16,skc20) ).
cnf(u3057,negated_conjecture,
~ specific(skc16,skc20) ).
cnf(u3065,negated_conjecture,
singleton(skc16,skc26) ).
cnf(u3073,negated_conjecture,
~ specific(skc16,skc26) ).
cnf(u730,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc21) ) ).
cnf(u2761,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc20,skc19) ) ).
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(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,skc26,skc25)
| ~ 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,skc25)
| ~ forename(skc13,X0)
| skc26 = 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(skc13,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc17,skc19) ) ).
cnf(u2051,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc15,skc19) ) ).
cnf(clause19,axiom,
( ~ entity(X0,X1)
| thing(X0,X1) ) ).
cnf(clause22,axiom,
( ~ organism(X0,X1)
| impartial(X0,X1) ) ).
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)
| theme(X1,skc15,skc16) ) ).
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(u963,negated_conjecture,
( ~ of(skc13,X0,skc19)
| ~ forename(skc13,X0)
| skc22 = X0 ) ).
cnf(u2747,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(u1374,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc15) ) ).
cnf(u2705,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc15,skc19) ) ).
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(u2158,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ man(skc16,X1)
| ~ accessible_world(X0,X2)
| agent(X2,skf1(X1),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(u2694,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc15,skc16) ) ).
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(u815,negated_conjecture,
( ~ human(skc13,X0)
| human(skc14,X0) ) ).
cnf(u842,negated_conjecture,
( ~ relname(skc13,X0)
| relname(skc16,X0) ) ).
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(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,skc25)
| ~ forename(X0,X1)
| ~ forename(X0,skc26)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc25)
| skc26 = 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(u793,negated_conjecture,
( ~ impartial(skc13,X0)
| impartial(skc14,X0) ) ).
cnf(u871,negated_conjecture,
( agent(X0,skc21,skc19)
| ~ accessible_world(skc14,X0) ) ).
cnf(u665,negated_conjecture,
( ~ smoke(skc13,X0)
| smoke(skc16,X0) ) ).
cnf(u2358,negated_conjecture,
( of(X0,skc26,skc25)
| ~ accessible_world(skc16,X0) ) ).
cnf(u728,negated_conjecture,
( ~ accessible_world(skc13,X0)
| present(X0,skc15) ) ).
cnf(u789,negated_conjecture,
( ~ entity(skc13,X0)
| entity(skc14,X0) ) ).
cnf(u700,negated_conjecture,
( ~ thing(skc13,X0)
| thing(skc14,X0) ) ).
cnf(u2723,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(u2742,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc17,skc16) ) ).
cnf(u704,negated_conjecture,
( ~ specific(skc13,X0)
| specific(skc14,X0) ) ).
cnf(u839,negated_conjecture,
( ~ forename(skc13,X0)
| forename(skc14,X0) ) ).
cnf(clause33,axiom,
( ~ human(X0,X1)
| ~ nonhuman(X0,X1) ) ).
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(u841,negated_conjecture,
( ~ relname(skc13,X0)
| relname(skc14,X0) ) ).
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,skc22,skc19) ) ).
cnf(clause5,axiom,
( ~ eventuality(X0,X1)
| specific(X0,X1) ) ).
cnf(u2701,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(u2795,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| be(X1,skc24,skc25,skc25) ) ).
cnf(u2063,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc18)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc19)
| skc18 = X1 ) ).
cnf(u746,negated_conjecture,
( ~ nonhuman(skc13,X0)
| nonhuman(skc16,X0) ) ).
cnf(u873,negated_conjecture,
( agent(X0,skc17,skc19)
| ~ accessible_world(skc13,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(u2327,negated_conjecture,
( theme(X0,skc15,skc16)
| ~ accessible_world(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(u2313,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc21,skc19) ) ).
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(u2568,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(u2334,negated_conjecture,
( theme(X0,skc17,skc16)
| ~ accessible_world(skc16,X0) ) ).
cnf(u2049,negated_conjecture,
( ~ accessible_world(skc14,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc21,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(clause66,axiom,
( ~ agent(X0,X2,X3)
| ~ accessible_world(X0,X1)
| agent(X1,X2,X3) ) ).
cnf(u974,negated_conjecture,
specific(skc16,skf1(X0)) ).
cnf(u2362,negated_conjecture,
( be(X0,skc24,skc25,skc25)
| ~ accessible_world(skc16,X0) ) ).
cnf(u742,negated_conjecture,
( ~ relation(skc13,X0)
| relation(skc16,X0) ) ).
cnf(u2760,negated_conjecture,
( ~ of(X0,X1,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc20)
| ~ accessible_world(skc16,X0)
| ~ entity(X0,skc19)
| skc20 = X1 ) ).
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(u2073,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc26,skc25) ) ).
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,
singleton(skc16,skf1(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,skc19)
| ~ forename(X0,X1)
| ~ forename(X0,skc22)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc19)
| skc22 = 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(u973,negated_conjecture,
nonexistent(skc16,skf1(X0)) ).
cnf(u712,negated_conjecture,
( ~ nonexistent(skc13,X0)
| nonexistent(skc14,X0) ) ).
cnf(u872,negated_conjecture,
( agent(X0,skc15,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2541,negated_conjecture,
( agent(X0,skc21,skc19)
| ~ accessible_world(skc16,X0) ) ).
cnf(u925,negated_conjecture,
( of(X0,skc18,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2212,negated_conjecture,
( theme(X0,skc15,skc16)
| ~ accessible_world(skc13,X0) ) ).
cnf(u953,negated_conjecture,
( be(X0,skc24,skc25,skc25)
| ~ accessible_world(skc13,X0) ) ).
cnf(u664,negated_conjecture,
( ~ smoke(skc13,X0)
| smoke(skc14,X0) ) ).
cnf(u975,negated_conjecture,
thing(skc16,skf1(X0)) ).
cnf(u844,negated_conjecture,
( ~ vincent_forename(skc13,X0)
| vincent_forename(skc16,X0) ) ).
cnf(u2320,negated_conjecture,
( agent(X0,skc17,skc19)
| ~ accessible_world(skc16,X0) ) ).
cnf(u927,negated_conjecture,
( of(X0,skc22,skc19)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2316,negated_conjecture,
( agent(X0,skc15,skc19)
| ~ accessible_world(skc16,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,skc24,skc25,skc25) ) ).
cnf(clause14,axiom,
( ~ state(X0,X1)
| eventuality(X0,X1) ) ).
cnf(u2783,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc26,skc25) ) ).
cnf(clause13,axiom,
( ~ abstraction(X0,X1)
| unisex(X0,X1) ) ).
cnf(u2710,negated_conjecture,
( ~ accessible_world(skc16,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc17,skc19) ) ).
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(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(u2209,negated_conjecture,
( ~ accessible_world(skc16,X0)
| present(X0,skc21) ) ).
cnf(u2782,negated_conjecture,
( ~ of(X0,X1,skc25)
| ~ forename(X0,X1)
| ~ forename(X0,skc26)
| ~ accessible_world(skc16,X0)
| ~ entity(X0,skc25)
| skc26 = X1 ) ).
cnf(u2340,negated_conjecture,
( of(X0,skc20,skc19)
| ~ accessible_world(skc16,X0) ) ).
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) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP249-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n011.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 18:37:00 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.87/2.28 % (2678777)Input is clausal, will run a generic CNF schedule.
% 8.87/2.28 % (2678808)dis-21_1_sil=8000:lcm=predicate:random_seed=2509514515: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.87/2.28 % (2678808)Instruction limit reached!
% 8.87/2.28 % (2678808)------------------------------
% 8.87/2.28 % (2678808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678808)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678808)Termination reason: Instruction limit
% 8.87/2.28 % (2678808)Termination phase: Saturation
% 8.87/2.28 % (2678808)Time elapsed: 0.028 s
% 8.87/2.28 % (2678808)Peak memory usage: 88 MB
% 8.87/2.28 % (2678808)Instructions burned: 119 (million)
% 8.87/2.28 % (2678803)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3870901119:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.87/2.28 % (2678807)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3951026630:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.87/2.28 % (2678806)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=238948465:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.87/2.28 % (2678805)lrs+10_1_sil=8000:sp=occurrence:random_seed=2770560335:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.87/2.28 % (2678802)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=553492204:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.87/2.28 % (2678804)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3310268759:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.87/2.28 % (2678805)Refutation not found, incomplete strategy
% 8.87/2.28 % (2678805)------------------------------
% 8.87/2.28 % (2678805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678805)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678805)Termination reason: Refutation not found, incomplete strategy
% 8.87/2.28 % (2678805)Time elapsed: 0.025 s
% 8.87/2.28 % (2678805)Peak memory usage: 88 MB
% 8.87/2.28 % (2678805)Instructions burned: 22 (million)
% 8.87/2.28 % (2678807)Refutation not found, incomplete strategy
% 8.87/2.28 % (2678807)------------------------------
% 8.87/2.28 % (2678807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678807)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678807)Termination reason: Refutation not found, incomplete strategy
% 8.87/2.28 % (2678807)Time elapsed: 0.090 s
% 8.87/2.28 % (2678807)Peak memory usage: 89 MB
% 8.87/2.28 % (2678807)Instructions burned: 81 (million)
% 8.87/2.28 % (2678806)Instruction limit reached!
% 8.87/2.28 % (2678806)------------------------------
% 8.87/2.28 % (2678806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678806)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678806)Termination reason: Instruction limit
% 8.87/2.28 % (2678806)Termination phase: Saturation
% 8.87/2.28 % (2678806)Time elapsed: 0.108 s
% 8.87/2.28 % (2678806)Peak memory usage: 88 MB
% 8.87/2.28 % (2678806)Instructions burned: 115 (million)
% 8.87/2.28 % (2678811)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=1922314632:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.87/2.28 % (2678811)Instruction limit reached!
% 8.87/2.28 % (2678811)------------------------------
% 8.87/2.28 % (2678811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678811)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678811)Termination reason: Instruction limit
% 8.87/2.28 % (2678811)Termination phase: Saturation
% 8.87/2.28 % (2678811)Time elapsed: 0.052 s
% 8.87/2.28 % (2678811)Peak memory usage: 89 MB
% 8.87/2.28 % (2678811)Instructions burned: 145 (million)
% 8.87/2.28 % (2678821)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2976363980:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 8.87/2.28 % (2678820)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2286686935:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 8.87/2.28 % (2678820)Refutation not found, incomplete strategy
% 8.87/2.28 % (2678820)------------------------------
% 8.87/2.28 % (2678820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678820)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678820)Termination reason: Refutation not found, incomplete strategy
% 8.87/2.28 % (2678820)Time elapsed: 0.021 s
% 8.87/2.28 % (2678820)Peak memory usage: 88 MB
% 8.87/2.28 % (2678820)Instructions burned: 19 (million)
% 8.87/2.28 % (2678821)Instruction limit reached!
% 8.87/2.28 % (2678821)------------------------------
% 8.87/2.28 % (2678821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678821)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678821)Termination reason: Instruction limit
% 8.87/2.28 % (2678821)Termination phase: Saturation
% 8.87/2.28 % (2678821)Time elapsed: 0.074 s
% 8.87/2.28 % (2678821)Peak memory usage: 88 MB
% 8.87/2.28 % (2678821)Instructions burned: 220 (million)
% 8.87/2.28 % (2678805)------------------------------
% 8.87/2.28 % (2678805)------------------------------
% 8.87/2.28 % (2678807)------------------------------
% 8.87/2.28 % (2678807)------------------------------
% 8.87/2.28 % (2678825)lrs+10_64_to=lpo:sil=8000:random_seed=1315245881:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 8.87/2.28 % (2678825)Instruction limit reached!
% 8.87/2.28 % (2678825)------------------------------
% 8.87/2.28 % (2678825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678825)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678825)Termination reason: Instruction limit
% 8.87/2.28 % (2678825)Termination phase: Saturation
% 8.87/2.28 % (2678825)Time elapsed: 0.035 s
% 8.87/2.28 % (2678825)Peak memory usage: 88 MB
% 8.87/2.28 % (2678825)Instructions burned: 130 (million)
% 8.87/2.28 % (2678827)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1507175668:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 8.87/2.28 % (2678828)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4119035807:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 8.87/2.28 % (2678827)Refutation not found, incomplete strategy
% 8.87/2.28 % (2678827)------------------------------
% 8.87/2.28 % (2678827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678827)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678827)Termination reason: Refutation not found, incomplete strategy
% 8.87/2.28 % (2678827)Time elapsed: 0.044 s
% 8.87/2.28 % (2678827)Peak memory usage: 88 MB
% 8.87/2.28 % (2678827)Instructions burned: 39 (million)
% 8.87/2.28 % (2678831)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2625274655:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 8.87/2.28 % (2678828)First to succeed.
% 8.87/2.28 % (2678828)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2678777"
% 8.87/2.28 % (2678820)------------------------------
% 8.87/2.28 % (2678820)------------------------------
% 8.87/2.28 % (2678837)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=3804374283:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 8.87/2.28 % (2678837)Refutation not found, incomplete strategy
% 8.87/2.28 % (2678837)------------------------------
% 8.87/2.28 % (2678837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.87/2.28 % (2678837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.87/2.28 % (2678837)CaDiCaL version: 2.1.3
% 8.87/2.28 % (2678837)Termination reason: Refutation not found, incomplete strategy
% 8.87/2.28 % (2678837)Time elapsed: 0.060 s
% 8.87/2.28 % (2678837)Peak memory usage: 89 MB
% 8.87/2.28 % (2678837)Instructions burned: 54 (million)
% 8.87/2.28 % (2678827)------------------------------
% 8.87/2.28 % (2678827)------------------------------
% 8.87/2.28 % SZS status Satisfiable for theBenchmark
% 8.87/2.28 % SZS output start Saturation.
% See solution above
% 10.33/2.50 % SZS output start Definitions and Model Updates.
% 10.33/2.50 for all inputs,
% 10.33/2.50 define actual_world(X0) := $true
% 10.33/2.50 % SZS output end Definitions and Model Updates.
% 10.33/2.50 % (2678828)------------------------------
% 10.33/2.50 % (2678828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.33/2.50 % (2678828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.50 % (2678828)CaDiCaL version: 2.1.3
% 10.33/2.50 % (2678828)Termination reason: Satisfiable
% 10.33/2.50 % (2678828)Time elapsed: 0.071 s
% 10.33/2.50 % (2678828)Peak memory usage: 90 MB
% 10.33/2.50 % (2678828)Instructions burned: 60 (million)
% 10.33/2.50 % (2678828)------------------------------
% 10.33/2.50 % (2678828)------------------------------
% 10.33/2.50 % (2678777)Success in time 1.348 s
% 10.33/2.50 % Vampire exiting
%------------------------------------------------------------------------------