%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP246-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 : n019.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:10 PM UTC 2026
% Result : Satisfiable 5.29s 1.79s
% Output : Saturation 7.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u114,negated_conjecture,
event(skc20,skf1(X1)) ).
cnf(u121,negated_conjecture,
present(skc20,skf1(X1)) ).
cnf(u125,negated_conjecture,
smoke(skc20,skf1(X1)) ).
cnf(u130,negated_conjecture,
be(skc13,skc16,skc17,skc17) ).
cnf(u135,negated_conjecture,
theme(skc13,skc15,skc14) ).
cnf(u140,negated_conjecture,
of(skc13,skc19,skc17) ).
cnf(u145,negated_conjecture,
agent(skc13,skc15,skc17) ).
cnf(u150,negated_conjecture,
of(skc13,skc18,skc17) ).
cnf(u155,negated_conjecture,
theme(skc13,skc21,skc20) ).
cnf(u160,negated_conjecture,
agent(skc14,skc24,skc23) ).
cnf(u165,negated_conjecture,
agent(skc13,skc21,skc23) ).
cnf(u170,negated_conjecture,
of(skc13,skc22,skc23) ).
cnf(u175,negated_conjecture,
of(skc13,skc25,skc23) ).
cnf(u180,negated_conjecture,
accessible_world(skc13,skc14) ).
cnf(u185,negated_conjecture,
proposition(skc13,skc14) ).
cnf(u190,negated_conjecture,
proposition(skc13,skc20) ).
cnf(u195,negated_conjecture,
accessible_world(skc13,skc20) ).
cnf(u200,negated_conjecture,
event(skc13,skc15) ).
cnf(u205,negated_conjecture,
present(skc13,skc15) ).
cnf(u210,negated_conjecture,
think_believe_consider(skc13,skc15) ).
cnf(u215,negated_conjecture,
state(skc13,skc16) ).
cnf(u220,negated_conjecture,
vincent_forename(skc13,skc19) ).
cnf(u225,negated_conjecture,
man(skc13,skc17) ).
cnf(u230,negated_conjecture,
forename(skc13,skc18) ).
cnf(u235,negated_conjecture,
jules_forename(skc13,skc18) ).
cnf(u240,negated_conjecture,
forename(skc13,skc19) ).
cnf(u245,negated_conjecture,
think_believe_consider(skc13,skc21) ).
cnf(u250,negated_conjecture,
present(skc13,skc21) ).
cnf(u255,negated_conjecture,
event(skc13,skc21) ).
cnf(u260,negated_conjecture,
vincent_forename(skc13,skc22) ).
cnf(u265,negated_conjecture,
forename(skc13,skc22) ).
cnf(u270,negated_conjecture,
forename(skc13,skc25) ).
cnf(u275,negated_conjecture,
jules_forename(skc13,skc25) ).
cnf(u280,negated_conjecture,
smoke(skc14,skc24) ).
cnf(u285,negated_conjecture,
present(skc14,skc24) ).
cnf(u290,negated_conjecture,
man(skc13,skc23) ).
cnf(u295,negated_conjecture,
event(skc14,skc24) ).
cnf(u304,negated_conjecture,
eventuality(skc14,skc24) ).
cnf(u309,negated_conjecture,
eventuality(skc13,skc21) ).
cnf(u314,negated_conjecture,
eventuality(skc13,skc15) ).
cnf(u320,negated_conjecture,
thing(skc14,skc24) ).
cnf(u326,negated_conjecture,
thing(skc13,skc21) ).
cnf(u332,negated_conjecture,
thing(skc13,skc15) ).
cnf(u340,negated_conjecture,
specific(skc13,skc15) ).
cnf(u345,negated_conjecture,
specific(skc13,skc21) ).
cnf(u350,negated_conjecture,
specific(skc14,skc24) ).
cnf(u356,negated_conjecture,
singleton(skc14,skc24) ).
cnf(u364,negated_conjecture,
nonexistent(skc13,skc15) ).
cnf(u369,negated_conjecture,
nonexistent(skc13,skc21) ).
cnf(u374,negated_conjecture,
nonexistent(skc14,skc24) ).
cnf(u380,negated_conjecture,
singleton(skc13,skc21) ).
cnf(u388,negated_conjecture,
unisex(skc13,skc15) ).
cnf(u393,negated_conjecture,
unisex(skc13,skc21) ).
cnf(u398,negated_conjecture,
unisex(skc14,skc24) ).
cnf(u404,negated_conjecture,
singleton(skc13,skc15) ).
cnf(u411,negated_conjecture,
relation(skc13,skc20) ).
cnf(u416,negated_conjecture,
relation(skc13,skc14) ).
cnf(u422,negated_conjecture,
abstraction(skc13,skc20) ).
cnf(u428,negated_conjecture,
abstraction(skc13,skc14) ).
cnf(u434,negated_conjecture,
eventuality(skc13,skc16) ).
cnf(u443,negated_conjecture,
thing(skc13,skc16) ).
cnf(u448,negated_conjecture,
specific(skc13,skc16) ).
cnf(u453,negated_conjecture,
nonexistent(skc13,skc16) ).
cnf(u458,negated_conjecture,
unisex(skc13,skc16) ).
cnf(u464,negated_conjecture,
event(skc13,skc16) ).
cnf(u472,negated_conjecture,
human_person(skc13,skc23) ).
cnf(u477,negated_conjecture,
human_person(skc13,skc17) ).
cnf(u483,negated_conjecture,
organism(skc13,skc23) ).
cnf(u489,negated_conjecture,
organism(skc13,skc17) ).
cnf(u498,negated_conjecture,
thing(skc13,skc20) ).
cnf(u503,negated_conjecture,
nonhuman(skc13,skc20) ).
cnf(u508,negated_conjecture,
general(skc13,skc20) ).
cnf(u513,negated_conjecture,
unisex(skc13,skc20) ).
cnf(u520,negated_conjecture,
human(skc13,skc17) ).
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,skc17) ).
cnf(u561,negated_conjecture,
animate(skc13,skc23) ).
cnf(u567,negated_conjecture,
singleton(skc13,skc16) ).
cnf(u574,negated_conjecture,
male(skc13,skc23) ).
cnf(u579,negated_conjecture,
male(skc13,skc17) ).
cnf(u588,negated_conjecture,
relname(skc13,skc18) ).
cnf(u593,negated_conjecture,
relname(skc13,skc19) ).
cnf(u598,negated_conjecture,
relname(skc13,skc22) ).
cnf(u603,negated_conjecture,
relname(skc13,skc25) ).
cnf(u609,negated_conjecture,
relation(skc13,skc18) ).
cnf(u617,negated_conjecture,
relation(skc13,skc19) ).
cnf(u625,negated_conjecture,
relation(skc13,skc22) ).
cnf(u632,negated_conjecture,
~ unisex(skc13,skc17) ).
cnf(u637,negated_conjecture,
~ unisex(skc13,skc23) ).
cnf(u643,negated_conjecture,
relation(skc13,skc25) ).
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,skc17) ).
cnf(u677,negated_conjecture,
impartial(skc13,skc17) ).
cnf(u682,negated_conjecture,
living(skc13,skc17) ).
cnf(u690,negated_conjecture,
~ nonhuman(skc13,skc17) ).
cnf(u698,negated_conjecture,
~ nonhuman(skc13,skc23) ).
cnf(u710,negated_conjecture,
abstraction(skc13,skc18) ).
cnf(u718,negated_conjecture,
abstraction(skc13,skc19) ).
cnf(u726,negated_conjecture,
abstraction(skc13,skc22) ).
cnf(u739,negated_conjecture,
abstraction(skc13,skc25) ).
cnf(u753,negated_conjecture,
singleton(skc13,skc20) ).
cnf(u769,negated_conjecture,
~ specific(skc13,skc20) ).
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,skc17) ).
cnf(u830,negated_conjecture,
specific(skc13,skc17) ).
cnf(u835,negated_conjecture,
existent(skc13,skc17) ).
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,skc19) ).
cnf(u887,negated_conjecture,
nonhuman(skc13,skc19) ).
cnf(u892,negated_conjecture,
general(skc13,skc19) ).
cnf(u897,negated_conjecture,
unisex(skc13,skc19) ).
cnf(u908,negated_conjecture,
thing(skc13,skc22) ).
cnf(u913,negated_conjecture,
nonhuman(skc13,skc22) ).
cnf(u918,negated_conjecture,
general(skc13,skc22) ).
cnf(u923,negated_conjecture,
unisex(skc13,skc22) ).
cnf(u936,negated_conjecture,
thing(skc13,skc25) ).
cnf(u941,negated_conjecture,
nonhuman(skc13,skc25) ).
cnf(u946,negated_conjecture,
general(skc13,skc25) ).
cnf(u951,negated_conjecture,
unisex(skc13,skc25) ).
cnf(u980,negated_conjecture,
singleton(skc13,skc23) ).
cnf(u988,negated_conjecture,
event(skc14,skc16) ).
cnf(u993,negated_conjecture,
event(skc14,skc21) ).
cnf(u998,negated_conjecture,
event(skc14,skc15) ).
cnf(u1004,negated_conjecture,
eventuality(skc14,skc16) ).
cnf(u1012,negated_conjecture,
event(skc20,skc16) ).
cnf(u1017,negated_conjecture,
event(skc20,skc21) ).
cnf(u1022,negated_conjecture,
event(skc20,skc15) ).
cnf(u1028,negated_conjecture,
eventuality(skc14,skc21) ).
cnf(u1036,negated_conjecture,
eventuality(skc14,skc15) ).
cnf(u1045,negated_conjecture,
eventuality(skc20,skc16) ).
cnf(u1050,negated_conjecture,
eventuality(skc20,skc15) ).
cnf(u1055,negated_conjecture,
eventuality(skc20,skc21) ).
cnf(u1067,negated_conjecture,
thing(skc14,skc20) ).
cnf(u1072,negated_conjecture,
thing(skc14,skc15) ).
cnf(u1077,negated_conjecture,
thing(skc14,skc16) ).
cnf(u1082,negated_conjecture,
thing(skc14,skc21) ).
cnf(u1087,negated_conjecture,
thing(skc14,skc23) ).
cnf(u1092,negated_conjecture,
thing(skc14,skc14) ).
cnf(u1104,negated_conjecture,
thing(skc20,skc20) ).
cnf(u1109,negated_conjecture,
thing(skc20,skc15) ).
cnf(u1114,negated_conjecture,
thing(skc20,skc16) ).
cnf(u1119,negated_conjecture,
thing(skc20,skc21) ).
cnf(u1124,negated_conjecture,
thing(skc20,skc23) ).
cnf(u1129,negated_conjecture,
thing(skc20,skc14) ).
cnf(u1140,negated_conjecture,
singleton(skc14,skc20) ).
cnf(u1145,negated_conjecture,
singleton(skc14,skc15) ).
cnf(u1150,negated_conjecture,
singleton(skc14,skc16) ).
cnf(u1155,negated_conjecture,
singleton(skc14,skc21) ).
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(skc20,skc20) ).
cnf(u1194,negated_conjecture,
singleton(skc20,skc15) ).
cnf(u1199,negated_conjecture,
singleton(skc20,skc16) ).
cnf(u1204,negated_conjecture,
singleton(skc20,skc21) ).
cnf(u1209,negated_conjecture,
singleton(skc20,skc14) ).
cnf(u1218,negated_conjecture,
specific(skc20,skc16) ).
cnf(u1223,negated_conjecture,
nonexistent(skc20,skc16) ).
cnf(u1228,negated_conjecture,
unisex(skc20,skc16) ).
cnf(u1237,negated_conjecture,
specific(skc14,skc16) ).
cnf(u1242,negated_conjecture,
specific(skc14,skc21) ).
cnf(u1247,negated_conjecture,
specific(skc14,skc23) ).
cnf(u1256,negated_conjecture,
specific(skc20,skc15) ).
cnf(u1261,negated_conjecture,
nonexistent(skc20,skc15) ).
cnf(u1266,negated_conjecture,
unisex(skc20,skc15) ).
cnf(u1275,negated_conjecture,
specific(skc20,skc21) ).
cnf(u1280,negated_conjecture,
specific(skc20,skc23) ).
cnf(u1289,negated_conjecture,
nonexistent(skc20,skc21) ).
cnf(u1294,negated_conjecture,
unisex(skc20,skc21) ).
cnf(u1302,negated_conjecture,
nonexistent(skc14,skc16) ).
cnf(u1307,negated_conjecture,
nonexistent(skc14,skc21) ).
cnf(u1316,negated_conjecture,
unisex(skc14,skc16) ).
cnf(u1328,negated_conjecture,
unisex(skc14,skc21) ).
cnf(u1338,negated_conjecture,
unisex(skc14,skc20) ).
cnf(u1343,negated_conjecture,
unisex(skc14,skc14) ).
cnf(u1354,negated_conjecture,
unisex(skc20,skc20) ).
cnf(u1359,negated_conjecture,
unisex(skc20,skc14) ).
cnf(u1367,negated_conjecture,
present(skc20,skc15) ).
cnf(u1372,negated_conjecture,
present(skc14,skc15) ).
cnf(u1380,negated_conjecture,
present(skc20,skc21) ).
cnf(u1385,negated_conjecture,
present(skc14,skc21) ).
cnf(u1394,negated_conjecture,
think_believe_consider(skc20,skc15) ).
cnf(u1399,negated_conjecture,
think_believe_consider(skc14,skc15) ).
cnf(u1407,negated_conjecture,
think_believe_consider(skc20,skc21) ).
cnf(u1412,negated_conjecture,
think_believe_consider(skc14,skc21) ).
cnf(u1420,negated_conjecture,
proposition(skc14,skc20) ).
cnf(u1425,negated_conjecture,
proposition(skc14,skc14) ).
cnf(u1433,negated_conjecture,
proposition(skc20,skc20) ).
cnf(u1438,negated_conjecture,
proposition(skc20,skc14) ).
cnf(u1450,negated_conjecture,
relation(skc14,skc20) ).
cnf(u1455,negated_conjecture,
relation(skc14,skc18) ).
cnf(u1460,negated_conjecture,
relation(skc14,skc19) ).
cnf(u1465,negated_conjecture,
relation(skc14,skc22) ).
cnf(u1470,negated_conjecture,
relation(skc14,skc25) ).
cnf(u1475,negated_conjecture,
relation(skc14,skc14) ).
cnf(u1487,negated_conjecture,
relation(skc20,skc20) ).
cnf(u1492,negated_conjecture,
relation(skc20,skc18) ).
cnf(u1497,negated_conjecture,
relation(skc20,skc19) ).
cnf(u1502,negated_conjecture,
relation(skc20,skc22) ).
cnf(u1507,negated_conjecture,
relation(skc20,skc25) ).
cnf(u1512,negated_conjecture,
relation(skc20,skc14) ).
cnf(u1524,negated_conjecture,
abstraction(skc14,skc20) ).
cnf(u1529,negated_conjecture,
abstraction(skc14,skc18) ).
cnf(u1534,negated_conjecture,
abstraction(skc14,skc19) ).
cnf(u1539,negated_conjecture,
abstraction(skc14,skc22) ).
cnf(u1544,negated_conjecture,
abstraction(skc14,skc25) ).
cnf(u1549,negated_conjecture,
abstraction(skc14,skc14) ).
cnf(u1561,negated_conjecture,
abstraction(skc20,skc20) ).
cnf(u1566,negated_conjecture,
abstraction(skc20,skc18) ).
cnf(u1571,negated_conjecture,
abstraction(skc20,skc19) ).
cnf(u1576,negated_conjecture,
abstraction(skc20,skc22) ).
cnf(u1581,negated_conjecture,
abstraction(skc20,skc25) ).
cnf(u1586,negated_conjecture,
abstraction(skc20,skc14) ).
cnf(u1594,negated_conjecture,
nonhuman(skc14,skc14) ).
cnf(u1599,negated_conjecture,
nonhuman(skc14,skc20) ).
cnf(u1607,negated_conjecture,
nonhuman(skc20,skc14) ).
cnf(u1612,negated_conjecture,
nonhuman(skc20,skc20) ).
cnf(u1620,negated_conjecture,
general(skc14,skc14) ).
cnf(u1625,negated_conjecture,
general(skc14,skc20) ).
cnf(u1633,negated_conjecture,
general(skc20,skc14) ).
cnf(u1638,negated_conjecture,
general(skc20,skc20) ).
cnf(u1645,negated_conjecture,
state(skc14,skc16) ).
cnf(u1652,negated_conjecture,
state(skc20,skc16) ).
cnf(u1661,negated_conjecture,
man(skc14,skc23) ).
cnf(u1666,negated_conjecture,
man(skc14,skc17) ).
cnf(u1675,negated_conjecture,
man(skc20,skc23) ).
cnf(u1680,negated_conjecture,
man(skc20,skc17) ).
cnf(u1687,negated_conjecture,
human_person(skc14,skc23) ).
cnf(u1692,negated_conjecture,
male(skc14,skc23) ).
cnf(u1699,negated_conjecture,
human_person(skc14,skc17) ).
cnf(u1706,negated_conjecture,
male(skc14,skc17) ).
cnf(u1713,negated_conjecture,
human_person(skc20,skc17) ).
cnf(u1718,negated_conjecture,
human_person(skc20,skc23) ).
cnf(u1725,negated_conjecture,
male(skc20,skc23) ).
cnf(u1732,negated_conjecture,
organism(skc14,skc17) ).
cnf(u1737,negated_conjecture,
organism(skc14,skc23) ).
cnf(u1744,negated_conjecture,
male(skc20,skc17) ).
cnf(u1751,negated_conjecture,
organism(skc20,skc17) ).
cnf(u1756,negated_conjecture,
organism(skc20,skc23) ).
cnf(u1764,negated_conjecture,
human(skc14,skc17) ).
cnf(u1769,negated_conjecture,
animate(skc14,skc17) ).
cnf(u1776,negated_conjecture,
entity(skc14,skc17) ).
cnf(u1781,negated_conjecture,
entity(skc14,skc23) ).
cnf(u1789,negated_conjecture,
human(skc20,skc17) ).
cnf(u1794,negated_conjecture,
animate(skc20,skc17) ).
cnf(u1801,negated_conjecture,
entity(skc20,skc17) ).
cnf(u1806,negated_conjecture,
entity(skc20,skc23) ).
cnf(u1814,negated_conjecture,
human(skc20,skc23) ).
cnf(u1819,negated_conjecture,
animate(skc20,skc23) ).
cnf(u1828,negated_conjecture,
impartial(skc14,skc17) ).
cnf(u1833,negated_conjecture,
impartial(skc14,skc23) ).
cnf(u1841,negated_conjecture,
impartial(skc20,skc17) ).
cnf(u1846,negated_conjecture,
impartial(skc20,skc23) ).
cnf(u1854,negated_conjecture,
living(skc14,skc17) ).
cnf(u1859,negated_conjecture,
living(skc14,skc23) ).
cnf(u1866,negated_conjecture,
living(skc20,skc17) ).
cnf(u1871,negated_conjecture,
living(skc20,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,skc19) ).
cnf(u1912,negated_conjecture,
forename(skc14,skc22) ).
cnf(u1917,negated_conjecture,
forename(skc14,skc25) ).
cnf(u1923,negated_conjecture,
relname(skc14,skc18) ).
cnf(u1932,negated_conjecture,
forename(skc20,skc18) ).
cnf(u1937,negated_conjecture,
forename(skc20,skc19) ).
cnf(u1942,negated_conjecture,
forename(skc20,skc22) ).
cnf(u1947,negated_conjecture,
forename(skc20,skc25) ).
cnf(u1953,negated_conjecture,
relname(skc14,skc19) ).
cnf(u1962,negated_conjecture,
relname(skc14,skc22) ).
cnf(u1967,negated_conjecture,
relname(skc14,skc25) ).
cnf(u1977,negated_conjecture,
relname(skc20,skc18) ).
cnf(u1982,negated_conjecture,
relname(skc20,skc19) ).
cnf(u1987,negated_conjecture,
relname(skc20,skc22) ).
cnf(u1992,negated_conjecture,
relname(skc20,skc25) ).
cnf(u2000,negated_conjecture,
vincent_forename(skc14,skc22) ).
cnf(u2005,negated_conjecture,
vincent_forename(skc14,skc19) ).
cnf(u2013,negated_conjecture,
vincent_forename(skc20,skc22) ).
cnf(u2018,negated_conjecture,
vincent_forename(skc20,skc19) ).
cnf(u2026,negated_conjecture,
jules_forename(skc14,skc25) ).
cnf(u2031,negated_conjecture,
jules_forename(skc14,skc18) ).
cnf(u2039,negated_conjecture,
jules_forename(skc20,skc25) ).
cnf(u2044,negated_conjecture,
jules_forename(skc20,skc18) ).
cnf(u2091,negated_conjecture,
skc25 = skc22 ).
cnf(u2109,negated_conjecture,
skc19 = skc18 ).
cnf(u2133,negated_conjecture,
vincent_forename(skc20,skc25) ).
cnf(u2138,negated_conjecture,
vincent_forename(skc14,skc25) ).
cnf(u2143,negated_conjecture,
vincent_forename(skc13,skc25) ).
cnf(u2161,negated_conjecture,
jules_forename(skc20,skc19) ).
cnf(u2166,negated_conjecture,
jules_forename(skc14,skc19) ).
cnf(u2171,negated_conjecture,
jules_forename(skc13,skc19) ).
cnf(u2186,negated_conjecture,
skc14 = skc20 ).
cnf(u2256,negated_conjecture,
unisex(skc20,skc24) ).
cnf(u2261,negated_conjecture,
nonexistent(skc20,skc24) ).
cnf(u2266,negated_conjecture,
singleton(skc20,skc24) ).
cnf(u2271,negated_conjecture,
specific(skc20,skc24) ).
cnf(u2276,negated_conjecture,
thing(skc20,skc24) ).
cnf(u2281,negated_conjecture,
eventuality(skc20,skc24) ).
cnf(u2286,negated_conjecture,
event(skc20,skc24) ).
cnf(u2291,negated_conjecture,
present(skc20,skc24) ).
cnf(u2296,negated_conjecture,
smoke(skc20,skc24) ).
cnf(u2301,negated_conjecture,
agent(skc20,skc24,skc23) ).
cnf(u2306,negated_conjecture,
theme(skc13,skc15,skc20) ).
cnf(u2432,negated_conjecture,
~ unisex(skc20,skc23) ).
cnf(u2448,negated_conjecture,
~ unisex(skc20,skc17) ).
cnf(u2472,negated_conjecture,
~ nonhuman(skc20,skc17) ).
cnf(u2480,negated_conjecture,
~ nonhuman(skc20,skc23) ).
cnf(u2518,negated_conjecture,
~ nonexistent(skc13,skc23) ).
cnf(u2524,negated_conjecture,
existent(skc20,skc23) ).
cnf(u2545,negated_conjecture,
singleton(skc13,skc17) ).
cnf(u2551,negated_conjecture,
thing(skc20,skc17) ).
cnf(u2560,negated_conjecture,
specific(skc20,skc17) ).
cnf(u2569,negated_conjecture,
~ nonexistent(skc13,skc17) ).
cnf(u2575,negated_conjecture,
existent(skc20,skc17) ).
cnf(u2589,negated_conjecture,
singleton(skc13,skc19) ).
cnf(u2595,negated_conjecture,
thing(skc20,skc19) ).
cnf(u2607,negated_conjecture,
nonhuman(skc20,skc19) ).
cnf(u2621,negated_conjecture,
~ specific(skc13,skc19) ).
cnf(u2627,negated_conjecture,
general(skc20,skc19) ).
cnf(u2639,negated_conjecture,
unisex(skc20,skc19) ).
cnf(u2679,negated_conjecture,
singleton(skc13,skc25) ).
cnf(u2685,negated_conjecture,
thing(skc20,skc25) ).
cnf(u2698,negated_conjecture,
nonhuman(skc20,skc25) ).
cnf(u2712,negated_conjecture,
~ specific(skc13,skc25) ).
cnf(u2718,negated_conjecture,
general(skc20,skc25) ).
cnf(u2740,negated_conjecture,
unisex(skc20,skc25) ).
cnf(u2878,negated_conjecture,
~ specific(skc20,skc20) ).
cnf(u2916,negated_conjecture,
singleton(skc20,skc23) ).
cnf(u2950,negated_conjecture,
~ nonexistent(skc20,skc23) ).
cnf(u2971,negated_conjecture,
singleton(skc20,skc17) ).
cnf(u3026,negated_conjecture,
~ nonexistent(skc20,skc17) ).
cnf(u3034,negated_conjecture,
singleton(skc20,skc19) ).
cnf(u3042,negated_conjecture,
~ specific(skc20,skc19) ).
cnf(u3050,negated_conjecture,
singleton(skc20,skc25) ).
cnf(u3058,negated_conjecture,
~ specific(skc20,skc25) ).
cnf(u730,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc24) ) ).
cnf(u729,negated_conjecture,
( ~ accessible_world(skc13,X0)
| present(X0,skc21) ) ).
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(skc20,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,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc15,skc17) ) ).
cnf(clause49,axiom,
( ~ accessible_world(X0,X1)
| ~ nonhuman(X0,X2)
| nonhuman(X1,X2) ) ).
cnf(u744,negated_conjecture,
( ~ abstraction(skc13,X0)
| abstraction(skc20,X0) ) ).
cnf(u2668,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc20)
| ~ accessible_world(skc13,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc15,X3)
| ~ agent(X0,X1,X3)
| skc20 = X2 ) ).
cnf(u972,negated_conjecture,
unisex(skc20,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(u720,negated_conjecture,
( ~ unisex(skc13,X0)
| unisex(skc14,X0) ) ).
cnf(u2759,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc19,skc17) ) ).
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(skc20,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,skc24,skc23) ) ).
cnf(u2051,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc21,skc23) ) ).
cnf(clause19,axiom,
( ~ entity(X0,X1)
| thing(X0,X1) ) ).
cnf(u2661,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc15,skc20) ) ).
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(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(skc20,X0) ) ).
cnf(clause1,axiom,
( ~ smoke(X0,X1)
| event(X0,X1) ) ).
cnf(u794,negated_conjecture,
( ~ impartial(skc13,X0)
| impartial(skc20,X0) ) ).
cnf(u2211,negated_conjecture,
( ~ accessible_world(skc20,X0)
| present(X0,skc24) ) ).
cnf(u900,negated_conjecture,
( theme(X0,skc21,skc20)
| ~ accessible_world(skc13,X0) ) ).
cnf(u790,negated_conjecture,
( ~ entity(skc13,X0)
| entity(skc20,X0) ) ).
cnf(u743,negated_conjecture,
( ~ abstraction(skc13,X0)
| abstraction(skc14,X0) ) ).
cnf(u963,negated_conjecture,
( ~ of(skc13,X0,skc23)
| ~ forename(skc13,X0)
| skc22 = X0 ) ).
cnf(u1374,negated_conjecture,
( ~ accessible_world(skc20,X0)
| present(X0,skc15) ) ).
cnf(u2354,negated_conjecture,
( of(X0,skc25,skc23)
| ~ accessible_world(skc20,X0) ) ).
cnf(u817,negated_conjecture,
( ~ animate(skc13,X0)
| animate(skc14,X0) ) ).
cnf(u2145,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ man(skc20,X1)
| ~ accessible_world(X0,X2)
| agent(X2,skf1(X1),X1) ) ).
cnf(u813,negated_conjecture,
( ~ living(skc13,X0)
| living(skc14,X0) ) ).
cnf(u748,negated_conjecture,
( ~ general(skc13,X0)
| general(skc20,X0) ) ).
cnf(u780,negated_conjecture,
( ~ human_person(skc13,X0)
| human_person(skc20,X0) ) ).
cnf(clause4,axiom,
( ~ thing(X0,X1)
| singleton(X0,X1) ) ).
cnf(u758,negated_conjecture,
( ~ man(skc13,X0)
| man(skc20,X0) ) ).
cnf(u2061,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc20)
| ~ accessible_world(skc13,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc21,X3)
| ~ agent(X0,X1,X3)
| skc20 = X2 ) ).
cnf(u2214,negated_conjecture,
( theme(X0,skc15,skc20)
| ~ accessible_world(skc13,X0) ) ).
cnf(u970,negated_conjecture,
( ~ theme(skc13,X0,X1)
| ~ think_believe_consider(skc13,X0)
| ~ proposition(skc13,X1)
| ~ agent(skc13,skc21,X2)
| ~ agent(skc13,X0,X2)
| skc20 = X1 ) ).
cnf(u1387,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc15) ) ).
cnf(u843,negated_conjecture,
( ~ vincent_forename(skc13,X0)
| vincent_forename(skc14,X0) ) ).
cnf(u2335,negated_conjecture,
( theme(X0,skc21,skc20)
| ~ accessible_world(skc20,X0) ) ).
cnf(u815,negated_conjecture,
( ~ human(skc13,X0)
| human(skc14,X0) ) ).
cnf(u842,negated_conjecture,
( ~ relname(skc13,X0)
| relname(skc20,X0) ) ).
cnf(u818,negated_conjecture,
( ~ animate(skc13,X0)
| animate(skc20,X0) ) ).
cnf(u734,negated_conjecture,
( ~ proposition(skc13,X0)
| proposition(skc20,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(skc20,X0) ) ).
cnf(u2066,negated_conjecture,
( ~ of(X0,X1,skc17)
| ~ forename(X0,X1)
| ~ forename(X0,skc18)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc17)
| skc18 = 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(u814,negated_conjecture,
( ~ living(skc13,X0)
| living(skc20,X0) ) ).
cnf(u874,negated_conjecture,
( agent(X0,skf1(X1),X1)
| ~ accessible_world(skc20,X0)
| ~ man(skc20,X1) ) ).
cnf(u713,negated_conjecture,
( ~ nonexistent(skc13,X0)
| nonexistent(skc20,X0) ) ).
cnf(clause53,axiom,
( ~ accessible_world(X0,X1)
| ~ human_person(X0,X2)
| human_person(X1,X2) ) ).
cnf(u2047,negated_conjecture,
( ~ accessible_world(skc20,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(skc20,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(u2724,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc15,skc20) ) ).
cnf(u793,negated_conjecture,
( ~ impartial(skc13,X0)
| impartial(skc14,X0) ) ).
cnf(u871,negated_conjecture,
( agent(X0,skc15,skc17)
| ~ accessible_world(skc13,X0) ) ).
cnf(u665,negated_conjecture,
( ~ smoke(skc13,X0)
| smoke(skc20,X0) ) ).
cnf(u728,negated_conjecture,
( ~ accessible_world(skc13,X0)
| present(X0,skc15) ) ).
cnf(u2769,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc25,skc23) ) ).
cnf(u789,negated_conjecture,
( ~ entity(skc13,X0)
| entity(skc14,X0) ) ).
cnf(u700,negated_conjecture,
( ~ thing(skc13,X0)
| thing(skc14,X0) ) ).
cnf(u2751,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc20)
| ~ accessible_world(skc20,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc21,X3)
| ~ agent(X0,X1,X3)
| skc20 = X2 ) ).
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(skc20,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(skc20,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(skc20,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,skc17)
| ~ forename(skc13,X0)
| skc19 = 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,skc23) ) ).
cnf(clause5,axiom,
( ~ eventuality(X0,X1)
| specific(X0,X1) ) ).
cnf(u2701,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc21,skc23) ) ).
cnf(u2063,negated_conjecture,
( ~ of(X0,X1,skc17)
| ~ forename(X0,X1)
| ~ forename(X0,skc19)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc17)
| skc19 = X1 ) ).
cnf(u746,negated_conjecture,
( ~ nonhuman(skc13,X0)
| nonhuman(skc20,X0) ) ).
cnf(u873,negated_conjecture,
( agent(X0,skc24,skc23)
| ~ accessible_world(skc14,X0) ) ).
cnf(u745,negated_conjecture,
( ~ nonhuman(skc13,X0)
| nonhuman(skc14,X0) ) ).
cnf(u1388,negated_conjecture,
( ~ accessible_world(skc20,X0)
| present(X0,skc21) ) ).
cnf(u840,negated_conjecture,
( ~ forename(skc13,X0)
| forename(skc20,X0) ) ).
cnf(u2511,negated_conjecture,
( agent(X0,skc24,skc23)
| ~ accessible_world(skc20,X0) ) ).
cnf(u792,negated_conjecture,
( ~ existent(skc13,X0)
| existent(skc20,X0) ) ).
cnf(u845,negated_conjecture,
( ~ jules_forename(skc13,X0)
| jules_forename(skc14,X0) ) ).
cnf(u756,negated_conjecture,
( ~ state(skc13,X0)
| state(skc20,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,skc17) ) ).
cnf(u1401,negated_conjecture,
( ~ accessible_world(skc14,X0)
| present(X0,skc21) ) ).
cnf(u2067,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc18,skc17) ) ).
cnf(clause66,axiom,
( ~ agent(X0,X2,X3)
| ~ accessible_world(X0,X1)
| agent(X1,X2,X3) ) ).
cnf(u974,negated_conjecture,
specific(skc20,skf1(X0)) ).
cnf(u742,negated_conjecture,
( ~ relation(skc13,X0)
| relation(skc20,X0) ) ).
cnf(u2364,negated_conjecture,
( be(X0,skc16,skc17,skc17)
| ~ accessible_world(skc20,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(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,skc18,skc17)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2730,negated_conjecture,
( ~ theme(X0,X1,X2)
| ~ proposition(X0,skc20)
| ~ accessible_world(skc20,X0)
| ~ think_believe_consider(X0,X1)
| ~ proposition(X0,X2)
| ~ agent(X0,skc15,X3)
| ~ agent(X0,X1,X3)
| skc20 = X2 ) ).
cnf(u721,negated_conjecture,
( ~ unisex(skc13,X0)
| unisex(skc20,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(skc20,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,skc22)
| ~ accessible_world(skc13,X0)
| ~ entity(X0,skc23)
| skc22 = X1 ) ).
cnf(u2768,negated_conjecture,
( ~ of(X0,X1,skc23)
| ~ forename(X0,X1)
| ~ forename(X0,skc25)
| ~ accessible_world(skc20,X0)
| ~ entity(X0,skc23)
| skc25 = 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,skc21) ) ).
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(u964,negated_conjecture,
( ~ of(skc13,X0,skc17)
| ~ forename(skc13,X0)
| skc18 = 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(u2329,negated_conjecture,
( theme(X0,skc15,skc20)
| ~ accessible_world(skc20,X0) ) ).
cnf(u973,negated_conjecture,
nonexistent(skc20,skf1(X0)) ).
cnf(u2323,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| agent(X1,skc24,skc23) ) ).
cnf(u712,negated_conjecture,
( ~ nonexistent(skc13,X0)
| nonexistent(skc14,X0) ) ).
cnf(u872,negated_conjecture,
( agent(X0,skc21,skc23)
| ~ accessible_world(skc13,X0) ) ).
cnf(u925,negated_conjecture,
( of(X0,skc19,skc17)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2538,negated_conjecture,
( ~ theme(skc13,X0,X1)
| ~ think_believe_consider(skc13,X0)
| ~ proposition(skc13,X1)
| ~ agent(skc13,skc15,X2)
| ~ agent(skc13,X0,X2)
| skc20 = X1 ) ).
cnf(u953,negated_conjecture,
( be(X0,skc16,skc17,skc17)
| ~ accessible_world(skc13,X0) ) ).
cnf(u664,negated_conjecture,
( ~ smoke(skc13,X0)
| smoke(skc14,X0) ) ).
cnf(u2341,negated_conjecture,
( of(X0,skc19,skc17)
| ~ accessible_world(skc20,X0) ) ).
cnf(u975,negated_conjecture,
thing(skc20,skf1(X0)) ).
cnf(u2777,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| be(X1,skc16,skc17,skc17) ) ).
cnf(u2746,negated_conjecture,
( ~ accessible_world(skc20,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc21,skc20) ) ).
cnf(u844,negated_conjecture,
( ~ vincent_forename(skc13,X0)
| vincent_forename(skc20,X0) ) ).
cnf(u2320,negated_conjecture,
( agent(X0,skc21,skc23)
| ~ accessible_world(skc20,X0) ) ).
cnf(u2314,negated_conjecture,
singleton(skc20,skf1(X0)) ).
cnf(u927,negated_conjecture,
( of(X0,skc22,skc23)
| ~ accessible_world(skc13,X0) ) ).
cnf(u2758,negated_conjecture,
( ~ of(X0,X1,skc17)
| ~ forename(X0,X1)
| ~ forename(X0,skc19)
| ~ accessible_world(skc20,X0)
| ~ entity(X0,skc17)
| skc19 = X1 ) ).
cnf(u2316,negated_conjecture,
( agent(X0,skc15,skc17)
| ~ accessible_world(skc20,X0) ) ).
cnf(u764,negated_conjecture,
eventuality(skc20,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,skc16,skc17,skc17) ) ).
cnf(clause14,axiom,
( ~ state(X0,X1)
| eventuality(X0,X1) ) ).
cnf(clause13,axiom,
( ~ abstraction(X0,X1)
| unisex(X0,X1) ) ).
cnf(u2064,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| of(X1,skc19,skc17) ) ).
cnf(clause7,axiom,
( ~ eventuality(X0,X1)
| unisex(X0,X1) ) ).
cnf(u1440,negated_conjecture,
( ~ accessible_world(skc20,X0)
| think_believe_consider(X0,skc21) ) ).
cnf(u2060,negated_conjecture,
( ~ accessible_world(skc13,X0)
| ~ accessible_world(X0,X1)
| theme(X1,skc21,skc20) ) ).
cnf(u782,negated_conjecture,
( ~ organism(skc13,X0)
| organism(skc20,X0) ) ).
cnf(clause110,negated_conjecture,
( agent(skc20,skf1(X0),X0)
| ~ man(skc20,X0) ) ).
cnf(u1414,negated_conjecture,
( ~ accessible_world(skc20,X0)
| think_believe_consider(X0,skc15) ) ).
cnf(u732,negated_conjecture,
( ~ accessible_world(skc13,X0)
| think_believe_consider(X0,skc21) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP246-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.37 % Computer : n019.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sun Sep 27 18:36:18 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 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
% 5.29/1.79 % (3324434)Input is clausal, will run a generic CNF schedule.
% 5.29/1.79 % (3324444)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1881098374:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.29/1.79 % (3324444)Refutation not found, incomplete strategy
% 5.29/1.79 % (3324444)------------------------------
% 5.29/1.79 % (3324444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324444)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324444)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.79 % (3324444)Time elapsed: 0.036 s
% 5.29/1.79 % (3324444)Peak memory usage: 89 MB
% 5.29/1.79 % (3324444)Instructions burned: 94 (million)
% 5.29/1.79 % (3324442)lrs+10_1_sil=8000:sp=occurrence:random_seed=1927824750:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.29/1.79 % (3324439)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=621548022:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.29/1.79 % (3324440)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1503521187:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.29/1.79 % (3324445)dis-21_1_sil=8000:lcm=predicate:random_seed=484737518: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)
% 5.29/1.79 % (3324441)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=695067237:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.29/1.79 % (3324443)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1372727526:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.29/1.79 % (3324442)Refutation not found, incomplete strategy
% 5.29/1.79 % (3324442)------------------------------
% 5.29/1.79 % (3324442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324442)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324442)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.79 % (3324442)Time elapsed: 0.016 s
% 5.29/1.79 % (3324442)Peak memory usage: 88 MB
% 5.29/1.79 % (3324442)Instructions burned: 22 (million)
% 5.29/1.79 % (3324445)Instruction limit reached!
% 5.29/1.79 % (3324445)------------------------------
% 5.29/1.79 % (3324445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324445)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324445)Termination reason: Instruction limit
% 5.29/1.79 % (3324445)Termination phase: Saturation
% 5.29/1.79 % (3324445)Time elapsed: 0.049 s
% 5.29/1.79 % (3324445)Peak memory usage: 88 MB
% 5.29/1.79 % (3324445)Instructions burned: 118 (million)
% 5.29/1.79 % (3324443)Instruction limit reached!
% 5.29/1.79 % (3324443)------------------------------
% 5.29/1.79 % (3324443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324443)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324443)Termination reason: Instruction limit
% 5.29/1.79 % (3324443)Termination phase: Saturation
% 5.29/1.79 % (3324443)Time elapsed: 0.072 s
% 5.29/1.79 % (3324443)Peak memory usage: 89 MB
% 5.29/1.79 % (3324443)Instructions burned: 114 (million)
% 5.29/1.79 % (3324444)------------------------------
% 5.29/1.79 % (3324444)------------------------------
% 5.29/1.79 % (3324453)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=1420184581:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.29/1.79 % (3324454)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3329964949:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.29/1.79 % (3324454)Refutation not found, incomplete strategy
% 5.29/1.79 % (3324454)------------------------------
% 5.29/1.79 % (3324454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324454)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324454)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.79 % (3324454)Time elapsed: 0.013 s
% 5.29/1.79 % (3324454)Peak memory usage: 88 MB
% 5.29/1.79 % (3324454)Instructions burned: 22 (million)
% 5.29/1.79 % (3324442)------------------------------
% 5.29/1.79 % (3324442)------------------------------
% 5.29/1.79 % (3324455)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=650388658:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 5.29/1.79 % (3324453)Instruction limit reached!
% 5.29/1.79 % (3324453)------------------------------
% 5.29/1.79 % (3324453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324453)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324453)Termination reason: Instruction limit
% 5.29/1.79 % (3324453)Termination phase: Saturation
% 5.29/1.79 % (3324453)Time elapsed: 0.077 s
% 5.29/1.79 % (3324453)Peak memory usage: 89 MB
% 5.29/1.79 % (3324453)Instructions burned: 147 (million)
% 5.29/1.79 % (3324455)Instruction limit reached!
% 5.29/1.79 % (3324455)------------------------------
% 5.29/1.79 % (3324455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324455)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324455)Termination reason: Instruction limit
% 5.29/1.79 % (3324455)Termination phase: Saturation
% 5.29/1.79 % (3324455)Time elapsed: 0.049 s
% 5.29/1.79 % (3324455)Peak memory usage: 88 MB
% 5.29/1.79 % (3324455)Instructions burned: 221 (million)
% 5.29/1.79 % (3324459)lrs+10_64_to=lpo:sil=8000:random_seed=2595462253:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.29/1.79 % (3324460)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1278274001:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.29/1.79 % (3324459)Instruction limit reached!
% 5.29/1.79 % (3324459)------------------------------
% 5.29/1.79 % (3324459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324459)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324459)Termination reason: Instruction limit
% 5.29/1.79 % (3324459)Termination phase: Saturation
% 5.29/1.79 % (3324459)Time elapsed: 0.050 s
% 5.29/1.79 % (3324459)Peak memory usage: 88 MB
% 5.29/1.79 % (3324459)Instructions burned: 129 (million)
% 5.29/1.79 % (3324461)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2955465210:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.29/1.79 % (3324460)Refutation not found, incomplete strategy
% 5.29/1.79 % (3324460)------------------------------
% 5.29/1.79 % (3324460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324460)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324460)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.79 % (3324460)Time elapsed: 0.036 s
% 5.29/1.79 % (3324460)Peak memory usage: 89 MB
% 5.29/1.79 % (3324460)Instructions burned: 52 (million)
% 5.29/1.79 % (3324454)------------------------------
% 5.29/1.79 % (3324454)------------------------------
% 5.29/1.79 % (3324461)First to succeed.
% 5.29/1.79 % (3324461)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3324434"
% 5.29/1.79 % (3324465)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1364767728:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.29/1.79 % (3324439)Refutation not found, incomplete strategy
% 5.29/1.79 % (3324439)------------------------------
% 5.29/1.79 % (3324439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324439)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324439)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.79 % (3324439)Time elapsed: 0.635 s
% 5.29/1.79 % (3324439)Peak memory usage: 128 MB
% 5.29/1.79 % (3324439)Instructions burned: 1071 (million)
% 5.29/1.79 % (3324466)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=2015651891:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.29/1.79 % (3324466)Refutation not found, incomplete strategy
% 5.29/1.79 % (3324466)------------------------------
% 5.29/1.79 % (3324466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.79 % (3324466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.79 % (3324466)CaDiCaL version: 2.1.3
% 5.29/1.79 % (3324466)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.79 % (3324466)Time elapsed: 0.028 s
% 5.29/1.79 % (3324466)Peak memory usage: 89 MB
% 5.29/1.79 % (3324466)Instructions burned: 48 (million)
% 5.29/1.79 % (3324460)------------------------------
% 5.29/1.79 % (3324460)------------------------------
% 5.29/1.79 % SZS status Satisfiable for theBenchmark
% 5.29/1.79 % SZS output start Saturation.
% See solution above
% 7.21/1.98 % SZS output start Definitions and Model Updates.
% 7.21/1.98 for all inputs,
% 7.21/1.98 define actual_world(X0) := $true
% 7.21/1.98 % SZS output end Definitions and Model Updates.
% 7.21/1.98 % (3324461)------------------------------
% 7.21/1.98 % (3324461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.21/1.98 % (3324461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.98 % (3324461)CaDiCaL version: 2.1.3
% 7.21/1.98 % (3324461)Termination reason: Satisfiable
% 7.21/1.98 % (3324461)Time elapsed: 0.042 s
% 7.21/1.98 % (3324461)Peak memory usage: 90 MB
% 7.21/1.98 % (3324461)Instructions burned: 60 (million)
% 7.21/1.98 % (3324461)------------------------------
% 7.21/1.98 % (3324461)------------------------------
% 7.21/1.98 % (3324434)Success in time 0.942 s
% 7.21/1.98 % Vampire exiting
%------------------------------------------------------------------------------