%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP020-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:06:59 PM UTC 2026
% Result : Satisfiable 5.99s 1.92s
% Output : Saturation 8.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u212,negated_conjecture,
a != b ).
cnf(u217,negated_conjecture,
true = sF20 ).
cnf(u222,negated_conjecture,
true = sF19 ).
cnf(u227,negated_conjecture,
true = sF18 ).
cnf(u232,negated_conjecture,
true = sF17 ).
cnf(u237,negated_conjecture,
true = sF16 ).
cnf(u242,negated_conjecture,
true = sF15 ).
cnf(u247,negated_conjecture,
true = sF14 ).
cnf(u252,negated_conjecture,
true = sF13 ).
cnf(u257,negated_conjecture,
true = sF12 ).
cnf(u262,negated_conjecture,
true = sF11 ).
cnf(u267,negated_conjecture,
true = sF10 ).
cnf(u272,negated_conjecture,
true = sF9 ).
cnf(u277,negated_conjecture,
true = sF8 ).
cnf(u282,negated_conjecture,
true = sF7 ).
cnf(u287,negated_conjecture,
true = sF6 ).
cnf(u292,negated_conjecture,
true = sF5 ).
cnf(u297,negated_conjecture,
true = sF4 ).
cnf(u302,negated_conjecture,
true = sF3 ).
cnf(u307,negated_conjecture,
true = sF2 ).
cnf(u312,negated_conjecture,
true = sF1 ).
cnf(u317,negated_conjecture,
true = sF0 ).
cnf(u322,axiom,
city(skc11) = sF0 ).
cnf(u327,axiom,
hollywood(skc11) = sF1 ).
cnf(u332,axiom,
event(skc10) = sF2 ).
cnf(u337,axiom,
lonely(skc9) = sF3 ).
cnf(u342,axiom,
way(skc9) = sF4 ).
cnf(u347,axiom,
street(skc9) = sF5 ).
cnf(u352,axiom,
seat(skc7) = sF6 ).
cnf(u357,axiom,
furniture(skc7) = sF7 ).
cnf(u362,axiom,
front(skc7) = sF8 ).
cnf(u367,axiom,
young(skc6) = sF9 ).
cnf(u372,axiom,
man(skc6) = sF10 ).
cnf(u377,axiom,
fellow(skc6) = sF11 ).
cnf(u382,axiom,
chevy(skc8) = sF12 ).
cnf(u387,axiom,
car(skc8) = sF13 ).
cnf(u392,axiom,
white(skc8) = sF14 ).
cnf(u397,axiom,
dirty(skc8) = sF15 ).
cnf(u402,axiom,
old(skc8) = sF16 ).
cnf(u407,axiom,
in(skc10,skc11) = sF17 ).
cnf(u412,axiom,
barrel(skc10,skc8) = sF18 ).
cnf(u417,axiom,
down(skc10,skc9) = sF19 ).
cnf(u422,axiom,
in(skc6,skc7) = sF20 ).
cnf(u427,axiom,
tuple(true,true) = sF22 ).
cnf(u434,negated_conjecture,
sF22 = tuple(sF20,sF20) ).
cnf(u441,negated_conjecture,
sF19 = sF20 ).
cnf(u450,negated_conjecture,
sF18 = sF20 ).
cnf(u455,negated_conjecture,
sF18 = sF19 ).
cnf(u466,negated_conjecture,
sF17 = sF20 ).
cnf(u471,negated_conjecture,
sF17 = sF19 ).
cnf(u476,negated_conjecture,
sF17 = sF18 ).
cnf(u489,negated_conjecture,
sF16 = sF20 ).
cnf(u494,negated_conjecture,
sF16 = sF19 ).
cnf(u499,negated_conjecture,
sF16 = sF18 ).
cnf(u504,negated_conjecture,
sF16 = sF17 ).
cnf(u519,negated_conjecture,
sF15 = sF20 ).
cnf(u524,negated_conjecture,
sF15 = sF19 ).
cnf(u529,negated_conjecture,
sF15 = sF18 ).
cnf(u534,negated_conjecture,
sF15 = sF17 ).
cnf(u539,negated_conjecture,
sF15 = sF16 ).
cnf(u556,negated_conjecture,
sF14 = sF15 ).
cnf(u561,negated_conjecture,
sF14 = sF16 ).
cnf(u566,negated_conjecture,
sF14 = sF17 ).
cnf(u571,negated_conjecture,
sF14 = sF18 ).
cnf(u576,negated_conjecture,
sF14 = sF19 ).
cnf(u581,negated_conjecture,
sF14 = sF20 ).
cnf(u600,negated_conjecture,
sF13 = sF14 ).
cnf(u605,negated_conjecture,
sF13 = sF15 ).
cnf(u610,negated_conjecture,
sF13 = sF16 ).
cnf(u615,negated_conjecture,
sF13 = sF17 ).
cnf(u620,negated_conjecture,
sF13 = sF18 ).
cnf(u625,negated_conjecture,
sF13 = sF19 ).
cnf(u630,negated_conjecture,
sF13 = sF20 ).
cnf(u651,negated_conjecture,
sF12 = sF13 ).
cnf(u656,negated_conjecture,
sF12 = sF14 ).
cnf(u661,negated_conjecture,
sF12 = sF15 ).
cnf(u666,negated_conjecture,
sF12 = sF16 ).
cnf(u671,negated_conjecture,
sF12 = sF17 ).
cnf(u676,negated_conjecture,
sF12 = sF18 ).
cnf(u681,negated_conjecture,
sF12 = sF19 ).
cnf(u686,negated_conjecture,
sF12 = sF20 ).
cnf(u709,negated_conjecture,
sF11 = sF12 ).
cnf(u714,negated_conjecture,
sF11 = sF13 ).
cnf(u719,negated_conjecture,
sF11 = sF14 ).
cnf(u724,negated_conjecture,
sF11 = sF15 ).
cnf(u729,negated_conjecture,
sF11 = sF16 ).
cnf(u734,negated_conjecture,
sF11 = sF17 ).
cnf(u739,negated_conjecture,
sF11 = sF18 ).
cnf(u744,negated_conjecture,
sF11 = sF19 ).
cnf(u749,negated_conjecture,
sF11 = sF20 ).
cnf(u774,negated_conjecture,
sF10 = sF11 ).
cnf(u779,negated_conjecture,
sF10 = sF12 ).
cnf(u784,negated_conjecture,
sF10 = sF13 ).
cnf(u789,negated_conjecture,
sF10 = sF14 ).
cnf(u794,negated_conjecture,
sF10 = sF15 ).
cnf(u799,negated_conjecture,
sF10 = sF16 ).
cnf(u804,negated_conjecture,
sF10 = sF17 ).
cnf(u809,negated_conjecture,
sF10 = sF18 ).
cnf(u814,negated_conjecture,
sF10 = sF19 ).
cnf(u819,negated_conjecture,
sF10 = sF20 ).
cnf(u846,negated_conjecture,
sF9 = sF10 ).
cnf(u851,negated_conjecture,
sF9 = sF11 ).
cnf(u856,negated_conjecture,
sF9 = sF12 ).
cnf(u861,negated_conjecture,
sF9 = sF13 ).
cnf(u866,negated_conjecture,
sF9 = sF14 ).
cnf(u871,negated_conjecture,
sF9 = sF15 ).
cnf(u876,negated_conjecture,
sF9 = sF16 ).
cnf(u881,negated_conjecture,
sF9 = sF17 ).
cnf(u886,negated_conjecture,
sF9 = sF18 ).
cnf(u891,negated_conjecture,
sF9 = sF19 ).
cnf(u896,negated_conjecture,
sF9 = sF20 ).
cnf(u925,negated_conjecture,
sF8 = sF9 ).
cnf(u930,negated_conjecture,
sF8 = sF10 ).
cnf(u935,negated_conjecture,
sF8 = sF11 ).
cnf(u940,negated_conjecture,
sF8 = sF12 ).
cnf(u945,negated_conjecture,
sF8 = sF13 ).
cnf(u950,negated_conjecture,
sF8 = sF14 ).
cnf(u955,negated_conjecture,
sF8 = sF15 ).
cnf(u960,negated_conjecture,
sF8 = sF16 ).
cnf(u965,negated_conjecture,
sF8 = sF17 ).
cnf(u970,negated_conjecture,
sF8 = sF18 ).
cnf(u975,negated_conjecture,
sF8 = sF19 ).
cnf(u980,negated_conjecture,
sF8 = sF20 ).
cnf(u1011,negated_conjecture,
sF7 = sF8 ).
cnf(u1016,negated_conjecture,
sF7 = sF9 ).
cnf(u1021,negated_conjecture,
sF7 = sF10 ).
cnf(u1026,negated_conjecture,
sF7 = sF11 ).
cnf(u1031,negated_conjecture,
sF7 = sF12 ).
cnf(u1036,negated_conjecture,
sF7 = sF13 ).
cnf(u1041,negated_conjecture,
sF7 = sF14 ).
cnf(u1046,negated_conjecture,
sF7 = sF15 ).
cnf(u1051,negated_conjecture,
sF7 = sF16 ).
cnf(u1056,negated_conjecture,
sF7 = sF17 ).
cnf(u1061,negated_conjecture,
sF7 = sF18 ).
cnf(u1066,negated_conjecture,
sF7 = sF19 ).
cnf(u1071,negated_conjecture,
sF7 = sF20 ).
cnf(u1104,negated_conjecture,
sF6 = sF7 ).
cnf(u1109,negated_conjecture,
sF6 = sF8 ).
cnf(u1114,negated_conjecture,
sF6 = sF9 ).
cnf(u1119,negated_conjecture,
sF6 = sF10 ).
cnf(u1124,negated_conjecture,
sF6 = sF11 ).
cnf(u1129,negated_conjecture,
sF6 = sF12 ).
cnf(u1134,negated_conjecture,
sF6 = sF13 ).
cnf(u1139,negated_conjecture,
sF6 = sF14 ).
cnf(u1144,negated_conjecture,
sF6 = sF15 ).
cnf(u1149,negated_conjecture,
sF6 = sF16 ).
cnf(u1154,negated_conjecture,
sF6 = sF17 ).
cnf(u1159,negated_conjecture,
sF6 = sF18 ).
cnf(u1164,negated_conjecture,
sF6 = sF19 ).
cnf(u1169,negated_conjecture,
sF6 = sF20 ).
cnf(u1204,negated_conjecture,
sF5 = sF6 ).
cnf(u1209,negated_conjecture,
sF5 = sF7 ).
cnf(u1214,negated_conjecture,
sF5 = sF8 ).
cnf(u1219,negated_conjecture,
sF5 = sF9 ).
cnf(u1224,negated_conjecture,
sF5 = sF10 ).
cnf(u1229,negated_conjecture,
sF5 = sF11 ).
cnf(u1234,negated_conjecture,
sF5 = sF12 ).
cnf(u1239,negated_conjecture,
sF5 = sF13 ).
cnf(u1244,negated_conjecture,
sF5 = sF14 ).
cnf(u1249,negated_conjecture,
sF5 = sF15 ).
cnf(u1254,negated_conjecture,
sF5 = sF16 ).
cnf(u1259,negated_conjecture,
sF5 = sF17 ).
cnf(u1264,negated_conjecture,
sF5 = sF18 ).
cnf(u1269,negated_conjecture,
sF5 = sF19 ).
cnf(u1274,negated_conjecture,
sF5 = sF20 ).
cnf(u1311,negated_conjecture,
sF4 = sF5 ).
cnf(u1316,negated_conjecture,
sF4 = sF6 ).
cnf(u1321,negated_conjecture,
sF4 = sF7 ).
cnf(u1326,negated_conjecture,
sF4 = sF8 ).
cnf(u1331,negated_conjecture,
sF4 = sF9 ).
cnf(u1336,negated_conjecture,
sF4 = sF10 ).
cnf(u1341,negated_conjecture,
sF4 = sF11 ).
cnf(u1346,negated_conjecture,
sF4 = sF12 ).
cnf(u1351,negated_conjecture,
sF4 = sF13 ).
cnf(u1356,negated_conjecture,
sF4 = sF14 ).
cnf(u1361,negated_conjecture,
sF4 = sF15 ).
cnf(u1366,negated_conjecture,
sF4 = sF16 ).
cnf(u1371,negated_conjecture,
sF4 = sF17 ).
cnf(u1376,negated_conjecture,
sF4 = sF18 ).
cnf(u1381,negated_conjecture,
sF4 = sF19 ).
cnf(u1386,negated_conjecture,
sF4 = sF20 ).
cnf(u1425,negated_conjecture,
sF3 = sF4 ).
cnf(u1430,negated_conjecture,
sF3 = sF5 ).
cnf(u1435,negated_conjecture,
sF3 = sF6 ).
cnf(u1440,negated_conjecture,
sF3 = sF7 ).
cnf(u1445,negated_conjecture,
sF3 = sF8 ).
cnf(u1450,negated_conjecture,
sF3 = sF9 ).
cnf(u1455,negated_conjecture,
sF3 = sF10 ).
cnf(u1460,negated_conjecture,
sF3 = sF11 ).
cnf(u1465,negated_conjecture,
sF3 = sF12 ).
cnf(u1470,negated_conjecture,
sF3 = sF13 ).
cnf(u1475,negated_conjecture,
sF3 = sF14 ).
cnf(u1480,negated_conjecture,
sF3 = sF15 ).
cnf(u1485,negated_conjecture,
sF3 = sF16 ).
cnf(u1490,negated_conjecture,
sF3 = sF17 ).
cnf(u1495,negated_conjecture,
sF3 = sF18 ).
cnf(u1500,negated_conjecture,
sF3 = sF19 ).
cnf(u1505,negated_conjecture,
sF3 = sF20 ).
cnf(u1546,negated_conjecture,
sF2 = sF3 ).
cnf(u1551,negated_conjecture,
sF2 = sF4 ).
cnf(u1556,negated_conjecture,
sF2 = sF5 ).
cnf(u1561,negated_conjecture,
sF2 = sF6 ).
cnf(u1566,negated_conjecture,
sF2 = sF7 ).
cnf(u1571,negated_conjecture,
sF2 = sF8 ).
cnf(u1576,negated_conjecture,
sF2 = sF9 ).
cnf(u1581,negated_conjecture,
sF2 = sF10 ).
cnf(u1586,negated_conjecture,
sF2 = sF11 ).
cnf(u1591,negated_conjecture,
sF2 = sF12 ).
cnf(u1596,negated_conjecture,
sF2 = sF13 ).
cnf(u1601,negated_conjecture,
sF2 = sF14 ).
cnf(u1606,negated_conjecture,
sF2 = sF15 ).
cnf(u1611,negated_conjecture,
sF2 = sF16 ).
cnf(u1616,negated_conjecture,
sF2 = sF17 ).
cnf(u1621,negated_conjecture,
sF2 = sF18 ).
cnf(u1626,negated_conjecture,
sF2 = sF19 ).
cnf(u1631,negated_conjecture,
sF2 = sF20 ).
cnf(u1674,negated_conjecture,
sF1 = sF2 ).
cnf(u1679,negated_conjecture,
sF1 = sF3 ).
cnf(u1684,negated_conjecture,
sF1 = sF4 ).
cnf(u1689,negated_conjecture,
sF1 = sF5 ).
cnf(u1694,negated_conjecture,
sF1 = sF6 ).
cnf(u1699,negated_conjecture,
sF1 = sF7 ).
cnf(u1704,negated_conjecture,
sF1 = sF8 ).
cnf(u1709,negated_conjecture,
sF1 = sF9 ).
cnf(u1714,negated_conjecture,
sF1 = sF10 ).
cnf(u1719,negated_conjecture,
sF1 = sF11 ).
cnf(u1724,negated_conjecture,
sF1 = sF12 ).
cnf(u1729,negated_conjecture,
sF1 = sF13 ).
cnf(u1734,negated_conjecture,
sF1 = sF14 ).
cnf(u1739,negated_conjecture,
sF1 = sF15 ).
cnf(u1744,negated_conjecture,
sF1 = sF16 ).
cnf(u1749,negated_conjecture,
sF1 = sF17 ).
cnf(u1754,negated_conjecture,
sF1 = sF18 ).
cnf(u1759,negated_conjecture,
sF1 = sF19 ).
cnf(u1764,negated_conjecture,
sF1 = sF20 ).
cnf(u1809,negated_conjecture,
sF0 = sF1 ).
cnf(u1814,negated_conjecture,
sF0 = sF2 ).
cnf(u1819,negated_conjecture,
sF0 = sF3 ).
cnf(u1824,negated_conjecture,
sF0 = sF4 ).
cnf(u1829,negated_conjecture,
sF0 = sF5 ).
cnf(u1834,negated_conjecture,
sF0 = sF6 ).
cnf(u1839,negated_conjecture,
sF0 = sF7 ).
cnf(u1844,negated_conjecture,
sF0 = sF8 ).
cnf(u1849,negated_conjecture,
sF0 = sF9 ).
cnf(u1854,negated_conjecture,
sF0 = sF10 ).
cnf(u1859,negated_conjecture,
sF0 = sF11 ).
cnf(u1864,negated_conjecture,
sF0 = sF12 ).
cnf(u1869,negated_conjecture,
sF0 = sF13 ).
cnf(u1874,negated_conjecture,
sF0 = sF14 ).
cnf(u1879,negated_conjecture,
sF0 = sF15 ).
cnf(u1884,negated_conjecture,
sF0 = sF16 ).
cnf(u1889,negated_conjecture,
sF0 = sF17 ).
cnf(u1894,negated_conjecture,
sF0 = sF18 ).
cnf(u1899,negated_conjecture,
sF0 = sF19 ).
cnf(u1904,negated_conjecture,
sF0 = sF20 ).
cnf(u1929,negated_conjecture,
sF22 = tuple(sF0,sF0) ).
cnf(u2715,negated_conjecture,
sF21(skc8) = tuple(sF0,new(skc8)) ).
cnf(u4360,negated_conjecture,
sF0 = male(skc6) ).
cnf(u4873,negated_conjecture,
sF0 = human(skc6) ).
cnf(u5142,negated_conjecture,
sF0 = location(skc11) ).
cnf(u5193,negated_conjecture,
sF0 = object(skc11) ).
cnf(u5242,negated_conjecture,
sF0 = ifeq2(female(skc6),sF0,sF0,sF0) ).
cnf(u5294,negated_conjecture,
sF0 = entity(skc11) ).
cnf(u5304,negated_conjecture,
sF0 = ifeq2(nonhuman(skc11),sF0,sF0,sF0) ).
cnf(u5907,negated_conjecture,
sF0 = eventuality(skc10) ).
cnf(u6234,negated_conjecture,
sF0 = ifeq2(artifact(skc11),sF0,sF0,sF0) ).
cnf(u7188,negated_conjecture,
sF0 = vehicle(skc8) ).
cnf(u7239,negated_conjecture,
sF0 = transport(skc8) ).
cnf(u7303,negated_conjecture,
sF0 = instrumentality(skc8) ).
cnf(u7354,negated_conjecture,
sF0 = artifact(skc8) ).
cnf(u7405,negated_conjecture,
sF0 = object(skc8) ).
cnf(u7482,negated_conjecture,
sF0 = ifeq2(location(skc8),sF0,sF0,sF0) ).
cnf(u7488,negated_conjecture,
sF0 = entity(skc8) ).
cnf(u7498,negated_conjecture,
sF0 = ifeq2(nonhuman(skc8),sF0,sF0,sF0) ).
cnf(u7823,negated_conjecture,
car(skc8) = sF0 ).
cnf(u8114,negated_conjecture,
sF0 = ifeq2(way(skc8),sF0,sF0,sF0) ).
cnf(u8120,negated_conjecture,
sF0 = artifact(skc9) ).
cnf(u8192,negated_conjecture,
sF0 = ifeq2(instrumentality(skc9),sF0,sF0,sF0) ).
cnf(u8198,negated_conjecture,
sF0 = object(skc9) ).
cnf(u8274,negated_conjecture,
sF0 = ifeq2(location(skc9),sF0,sF0,sF0) ).
cnf(u8280,negated_conjecture,
sF0 = entity(skc9) ).
cnf(u8314,negated_conjecture,
sF0 = ifeq2(nonhuman(skc9),sF0,sF0,sF0) ).
cnf(u8639,negated_conjecture,
way(skc9) = sF0 ).
cnf(u8938,negated_conjecture,
sF0 = ifeq2(furniture(skc8),sF0,sF0,sF0) ).
cnf(u8944,negated_conjecture,
sF0 = instrumentality(skc7) ).
cnf(u9016,negated_conjecture,
sF0 = ifeq2(transport(skc7),sF0,sF0,sF0) ).
cnf(u9022,negated_conjecture,
sF0 = artifact(skc7) ).
cnf(u9102,negated_conjecture,
sF0 = ifeq2(way(skc7),sF0,sF0,sF0) ).
cnf(u9107,negated_conjecture,
sF0 = object(skc7) ).
cnf(u9123,negated_conjecture,
sF0 = entity(skc7) ).
cnf(u9186,negated_conjecture,
sF0 = ifeq2(location(skc7),sF0,sF0,sF0) ).
cnf(u9199,negated_conjecture,
sF0 = ifeq2(nonhuman(skc7),sF0,sF0,sF0) ).
cnf(u9525,negated_conjecture,
furniture(skc7) = sF0 ).
cnf(u9800,negated_conjecture,
sF0 = nonhuman(skc7) ).
cnf(u10183,negated_conjecture,
sF0 = ifeq2(organism(skc8),sF0,sF0,sF0) ).
cnf(u10188,negated_conjecture,
sF0 = ifeq2(organism(skc7),sF0,sF0,sF0) ).
cnf(u10193,negated_conjecture,
sF0 = ifeq2(organism(skc9),sF0,sF0,sF0) ).
cnf(u10198,negated_conjecture,
sF0 = ifeq2(organism(skc11),sF0,sF0,sF0) ).
cnf(u10462,negated_conjecture,
sF0 = organism(skc6) ).
cnf(u10513,negated_conjecture,
sF0 = entity(skc6) ).
cnf(u10525,negated_conjecture,
sF0 = ifeq2(nonhuman(skc6),sF0,sF0,sF0) ).
cnf(u10530,negated_conjecture,
sF0 = ifeq2(object(skc6),sF0,sF0,sF0) ).
cnf(u11162,negated_conjecture,
man(skc6) = sF0 ).
cnf(u11316,negated_conjecture,
b = ifeq(tuple(nonhuman(skc6),sF0),sF22,a,b) ).
cnf(u11321,negated_conjecture,
b = ifeq(tuple(sF0,human(skc7)),sF22,a,b) ).
cnf(u11713,negated_conjecture,
b = ifeq(tuple(woman(skc6),sF0),sF22,a,b) ).
cnf(u11828,negated_conjecture,
b = ifeq(tuple(female(skc6),sF0),sF22,a,b) ).
cnf(u12083,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skc10)),sF22,a,b) ).
cnf(u12342,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skc8)),sF22,a,b) ).
cnf(u12347,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skc6)),sF22,a,b) ).
cnf(u12352,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skc7)),sF22,a,b) ).
cnf(u12357,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skc9)),sF22,a,b) ).
cnf(u12362,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skc11)),sF22,a,b) ).
cnf(u12625,negated_conjecture,
b = ifeq(tuple(entity(skc10),sF0),sF22,a,b) ).
cnf(u12630,negated_conjecture,
b = ifeq(tuple(sF0,eventuality(skc8)),sF22,a,b) ).
cnf(u12635,negated_conjecture,
b = ifeq(tuple(sF0,eventuality(skc6)),sF22,a,b) ).
cnf(u12640,negated_conjecture,
b = ifeq(tuple(sF0,eventuality(skc7)),sF22,a,b) ).
cnf(u12645,negated_conjecture,
b = ifeq(tuple(sF0,eventuality(skc9)),sF22,a,b) ).
cnf(u12650,negated_conjecture,
b = ifeq(tuple(sF0,eventuality(skc11)),sF22,a,b) ).
cnf(u12899,negated_conjecture,
b = ifeq(tuple(location(skc7),sF0),sF22,a,b) ).
cnf(u12904,negated_conjecture,
b = ifeq(tuple(location(skc9),sF0),sF22,a,b) ).
cnf(u12909,negated_conjecture,
b = ifeq(tuple(location(skc8),sF0),sF22,a,b) ).
cnf(u12914,negated_conjecture,
b = ifeq(tuple(sF0,artifact(skc11)),sF22,a,b) ).
cnf(u13191,negated_conjecture,
b = ifeq(tuple(sF0,way(skc7)),sF22,a,b) ).
cnf(u13196,negated_conjecture,
b = ifeq(tuple(sF0,way(skc8)),sF22,a,b) ).
cnf(u13266,negated_conjecture,
b = ifeq(tuple(instrumentality(skc9),sF0),sF22,a,b) ).
cnf(u13490,negated_conjecture,
b = ifeq(tuple(sF0,furniture(skc8)),sF22,a,b) ).
cnf(u13599,negated_conjecture,
b = ifeq(tuple(transport(skc7),sF0),sF22,a,b) ).
cnf(u13769,negated_conjecture,
b = ifeq(tuple(object(skc6),sF0),sF22,a,b) ).
cnf(u13774,negated_conjecture,
b = ifeq(tuple(sF0,organism(skc8)),sF22,a,b) ).
cnf(u13779,negated_conjecture,
b = ifeq(tuple(sF0,organism(skc7)),sF22,a,b) ).
cnf(u13784,negated_conjecture,
b = ifeq(tuple(sF0,organism(skc9)),sF22,a,b) ).
cnf(u13789,negated_conjecture,
b = ifeq(tuple(sF0,organism(skc11)),sF22,a,b) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u7564,negated_conjecture,
sF0 = ifeq2(chevy(X0),sF0,car(X0),sF0) ).
cnf(u5649,negated_conjecture,
sF0 = ifeq2(event(X0),sF0,eventuality(X0),sF0) ).
cnf(u6952,negated_conjecture,
sF0 = ifeq2(car(X0),sF0,vehicle(X0),sF0) ).
cnf(u2968,negated_conjecture,
sF0 = ifeq2(drs(X0),sF0,proposition(X0),sF0) ).
cnf(u11515,negated_conjecture,
b = ifeq(tuple(woman(X0),man(X0)),sF22,a,b) ).
cnf(u44,axiom,
true = ifeq2(street(X0),true,way(X0),true) ).
cnf(u40,axiom,
true = ifeq2(chevy(X0),true,car(X0),true) ).
cnf(u73,axiom,
true = ifeq2(have(X0,X1,X2),true,ifeq2(nonhuman(X1),true,ifeq2(nonhuman(X2),true,partof(X2,X1),true),true),true) ).
cnf(u11251,negated_conjecture,
b = ifeq(tuple(nonhuman(X0),human(X0)),sF22,a,b) ).
cnf(u10,axiom,
true = ifeq2(proposition(X0),true,drs(X0),true) ).
cnf(u16076,negated_conjecture,
sF0 = ifeq2(have(X0,X1,skc7),sF0,ifeq2(nonhuman(X1),sF0,partof(skc7,X1),sF0),sF0) ).
cnf(u11765,negated_conjecture,
b = ifeq(tuple(female(X0),male(X0)),sF22,a,b) ).
cnf(u15296,negated_conjecture,
sF0 = ifeq2(have(skf1(X0,X1),X2,X3),sF0,of(X2,X3),sF0) ).
cnf(u8380,negated_conjecture,
sF0 = ifeq2(street(X0),sF0,way(X0),sF0) ).
cnf(u123,axiom,
b = ifeq(tuple(eventuality(X0),abstraction(X0)),tuple(true,true),a,b) ).
cnf(u14218,negated_conjecture,
sF0 = ifeq2(of(X0,X1),sF0,ifeq2(owner(X0),sF0,human(X0),sF0),sF0) ).
cnf(u14,axiom,
true = ifeq2(female(X0),true,human(X0),true) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u6720,negated_conjecture,
sF0 = ifeq2(vehicle(X0),sF0,transport(X0),sF0) ).
cnf(u133,axiom,
b = ifeq(tuple(instrumentality(X0),way(X0)),tuple(true,true),a,b) ).
cnf(u32,axiom,
true = ifeq2(instrumentality(X0),true,artifact(X0),true) ).
cnf(u135,axiom,
b = ifeq(tuple(transport(X0),furniture(X0)),tuple(true,true),a,b) ).
cnf(u208,negated_conjecture,
b = sF23(X0) ).
cnf(u15043,negated_conjecture,
sF0 = ifeq2(have(X0,X1,X2),sF0,ifeq2(event(X0),sF0,of(X1,X2),sF0),sF0) ).
cnf(u58,axiom,
true = ifeq2(fellow(X0),true,man(X0),true) ).
cnf(u10226,negated_conjecture,
sF0 = ifeq2(human(X0),sF0,organism(X0),sF0) ).
cnf(u15000,negated_conjecture,
sF0 = ifeq2(have(X0,skc6,X1),sF0,owner(skc6),sF0) ).
cnf(u12271,negated_conjecture,
b = ifeq(tuple(entity(X0),abstraction(X0)),sF22,a,b) ).
cnf(u10903,negated_conjecture,
sF0 = ifeq2(fellow(X0),sF0,man(X0),sF0) ).
cnf(u9564,negated_conjecture,
sF0 = ifeq2(front(X0),sF0,nonhuman(X0),sF0) ).
cnf(u14490,negated_conjecture,
ifeq3(partof(X0,X1),sF0,ifeq3(partof(X0,X2),sF0,X1,X2),X2) = X2 ).
cnf(u3661,negated_conjecture,
sF0 = ifeq2(female(X0),sF0,human(X0),sF0) ).
cnf(u8,axiom,
true = ifeq2(drs(X0),true,proposition(X0),true) ).
cnf(u36,axiom,
true = ifeq2(vehicle(X0),true,transport(X0),true) ).
cnf(u13123,negated_conjecture,
b = ifeq(tuple(instrumentality(X0),way(X0)),sF22,a,b) ).
cnf(u34,axiom,
true = ifeq2(transport(X0),true,instrumentality(X0),true) ).
cnf(u62,axiom,
true = ifeq2(of(X0,X1),true,have(skf1(X0,X1),X1,X0),true) ).
cnf(u67,axiom,
true = ifeq2(have(X0,X1,X2),true,ifeq2(event(X0),true,of(X1,X2),true),true) ).
cnf(u121,axiom,
b = ifeq(tuple(female(X0),male(X0)),tuple(true,true),a,b) ).
cnf(u15585,negated_conjecture,
sF0 = ifeq2(of(X0,X1),sF0,ifeq2(owner(X0),sF0,have(X2,X0,X1),sF0),sF0) ).
cnf(u15319,negated_conjecture,
sF0 = ifeq2(have(X0,X1,X2),sF0,ifeq2(human(X1),sF0,of(X1,X2),sF0),sF0) ).
cnf(u14722,negated_conjecture,
ifeq3(partof(X1,ifeq3(partof(X1,X0),sF0,X0,X0)),sF0,X0,X0) = X0 ).
cnf(u12,axiom,
true = ifeq2(woman(X0),true,female(X0),true) ).
cnf(u16077,negated_conjecture,
sF0 = ifeq2(have(X0,skc7,X1),sF0,ifeq2(nonhuman(X1),sF0,partof(X1,skc7),sF0),sF0) ).
cnf(u15551,negated_conjecture,
sF0 = ifeq2(have(X0,skc6,X1),sF0,of(skc6,X1),sF0) ).
cnf(u14449,negated_conjecture,
sF0 = ifeq2(of(skc6,X0),sF0,ifeq2(owner(skc6),sF0,sF0,sF0),sF0) ).
cnf(u3892,negated_conjecture,
sF0 = ifeq2(male(X0),sF0,human(X0),sF0) ).
cnf(u137,axiom,
b = ifeq(tuple(object(X0),organism(X0)),tuple(true,true),a,b) ).
cnf(u38,axiom,
true = ifeq2(car(X0),true,vehicle(X0),true) ).
cnf(clause43,axiom,
ifeq3(partof(X0,X1),true,ifeq3(partof(X0,X2),true,X1,X2),X2) = X2 ).
cnf(u4613,negated_conjecture,
sF0 = ifeq2(location(X0),sF0,object(X0),sF0) ).
cnf(u125,axiom,
b = ifeq(tuple(entity(X0),abstraction(X0)),tuple(true,true),a,b) ).
cnf(u3430,negated_conjecture,
sF0 = ifeq2(woman(X0),sF0,female(X0),sF0) ).
cnf(u56,axiom,
true = ifeq2(man(X0),true,human(X0),true) ).
cnf(u5902,negated_conjecture,
sF0 = eventuality(skf1(X0,X1)) ).
cnf(u69,axiom,
true = ifeq2(have(X0,X1,X2),true,ifeq2(human(X1),true,of(X1,X2),true),true) ).
cnf(u26,axiom,
true = ifeq2(hollywood(X0),true,city(X0),true) ).
cnf(u6487,negated_conjecture,
sF0 = ifeq2(transport(X0),sF0,instrumentality(X0),sF0) ).
cnf(u5370,negated_conjecture,
sF0 = ifeq2(hollywood(X0),sF0,city(X0),sF0) ).
cnf(u60,axiom,
true = ifeq2(of(X0,X1),true,ifeq2(owner(X0),true,human(X0),true),true) ).
cnf(clause1,axiom,
event(skf1(X0,X1)) = true ).
cnf(u24,axiom,
true = ifeq2(city(X0),true,location(X0),true) ).
cnf(u127,axiom,
b = ifeq(tuple(entity(X0),eventuality(X0)),tuple(true,true),a,b) ).
cnf(u71,axiom,
true = ifeq2(of(X0,X1),true,ifeq2(owner(X0),true,have(X2,X0,X1),true),true) ).
cnf(u15297,negated_conjecture,
sF0 = ifeq2(have(skc10,X0,X1),sF0,of(X0,X1),sF0) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u30,axiom,
true = ifeq2(artifact(X0),true,object(X0),true) ).
cnf(u5999,negated_conjecture,
sF0 = ifeq2(artifact(X0),sF0,object(X0),sF0) ).
cnf(u9885,negated_conjecture,
sF0 = ifeq2(organism(X0),sF0,entity(X0),sF0) ).
cnf(u13698,negated_conjecture,
b = ifeq(tuple(object(X0),organism(X0)),sF22,a,b) ).
cnf(u48,axiom,
true = ifeq2(seat(X0),true,furniture(X0),true) ).
cnf(u4124,negated_conjecture,
sF0 = ifeq2(man(X0),sF0,male(X0),sF0) ).
cnf(u12060,negated_conjecture,
b = ifeq(tuple(sF0,abstraction(skf1(X0,X1))),sF22,a,b) ).
cnf(u6,axiom,
true = ifeq2(nonhuman(X0),true,entity(X0),true) ).
cnf(u13424,negated_conjecture,
b = ifeq(tuple(transport(X0),furniture(X0)),sF22,a,b) ).
cnf(u6256,negated_conjecture,
sF0 = ifeq2(instrumentality(X0),sF0,artifact(X0),sF0) ).
cnf(u429,negated_conjecture,
b = ifeq(sF21(X0),sF22,a,b) ).
cnf(u14768,negated_conjecture,
sF0 = ifeq2(have(X0,X1,X2),sF0,ifeq2(human(X1),sF0,owner(X1),sF0),sF0) ).
cnf(u52,axiom,
true = ifeq2(organism(X0),true,entity(X0),true) ).
cnf(u3199,negated_conjecture,
sF0 = ifeq2(proposition(X0),sF0,drs(X0),sF0) ).
cnf(u12018,negated_conjecture,
b = ifeq(tuple(eventuality(X0),abstraction(X0)),sF22,a,b) ).
cnf(u2737,negated_conjecture,
sF0 = ifeq2(nonhuman(X0),sF0,entity(X0),sF0) ).
cnf(u119,axiom,
b = ifeq(tuple(woman(X0),man(X0)),tuple(true,true),a,b) ).
cnf(u10618,negated_conjecture,
sF0 = ifeq2(man(X0),sF0,human(X0),sF0) ).
cnf(u50,axiom,
true = ifeq2(front(X0),true,nonhuman(X0),true) ).
cnf(u9266,negated_conjecture,
sF0 = ifeq2(seat(X0),sF0,furniture(X0),sF0) ).
cnf(u12550,negated_conjecture,
b = ifeq(tuple(entity(X0),eventuality(X0)),sF22,a,b) ).
cnf(u28,axiom,
true = ifeq2(event(X0),true,eventuality(X0),true) ).
cnf(u7858,negated_conjecture,
sF0 = ifeq2(way(X0),sF0,artifact(X0),sF0) ).
cnf(u42,axiom,
true = ifeq2(way(X0),true,artifact(X0),true) ).
cnf(u54,axiom,
true = ifeq2(human(X0),true,organism(X0),true) ).
cnf(u13986,negated_conjecture,
sF0 = ifeq2(of(X0,X1),sF0,have(skf1(X0,X1),X1,X0),sF0) ).
cnf(u8682,negated_conjecture,
sF0 = ifeq2(furniture(X0),sF0,instrumentality(X0),sF0) ).
cnf(u16,axiom,
true = ifeq2(male(X0),true,human(X0),true) ).
cnf(u203,axiom,
tuple(old(X0),new(X0)) = sF21(X0) ).
cnf(u4382,negated_conjecture,
sF0 = ifeq2(object(X0),sF0,entity(X0),sF0) ).
cnf(u4906,negated_conjecture,
sF0 = ifeq2(city(X0),sF0,location(X0),sF0) ).
cnf(u15823,negated_conjecture,
sF0 = ifeq2(have(X0,X1,X2),sF0,ifeq2(nonhuman(X1),sF0,ifeq2(nonhuman(X2),sF0,partof(X2,X1),sF0),sF0),sF0) ).
cnf(u12830,negated_conjecture,
b = ifeq(tuple(location(X0),artifact(X0)),sF22,a,b) ).
cnf(u117,axiom,
b = ifeq(tuple(nonhuman(X0),human(X0)),tuple(true,true),a,b) ).
cnf(u20,axiom,
true = ifeq2(object(X0),true,entity(X0),true) ).
cnf(u64,axiom,
true = ifeq2(have(X0,X1,X2),true,ifeq2(human(X1),true,owner(X1),true),true) ).
cnf(u131,axiom,
b = ifeq(tuple(location(X0),artifact(X0)),tuple(true,true),a,b) ).
cnf(u18,axiom,
true = ifeq2(man(X0),true,male(X0),true) ).
cnf(u46,axiom,
true = ifeq2(furniture(X0),true,instrumentality(X0),true) ).
cnf(u16265,negated_conjecture,
sF0 = ifeq2(have(X0,skc7,skc7),sF0,partof(skc7,skc7),sF0) ).
cnf(u12597,negated_conjecture,
b = ifeq(tuple(entity(skf1(X0,X1)),sF0),sF22,a,b) ).
cnf(u22,axiom,
true = ifeq2(location(X0),true,object(X0),true) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP020-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 17:51:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/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.99/1.92 % (3105906)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.99/1.92 % (3105915)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1713628208:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.99/1.92 % (3105915)Refutation not found, incomplete strategy
% 5.99/1.92 % (3105915)------------------------------
% 5.99/1.92 % (3105915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105915)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105915)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.92 % (3105915)Time elapsed: 0.010 s
% 5.99/1.92 % (3105915)Peak memory usage: 88 MB
% 5.99/1.92 % (3105915)Instructions burned: 31 (million)
% 5.99/1.92 % (3105917)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1294170983:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.99/1.92 % (3105912)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2342278424:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.99/1.92 % (3105911)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1148218285:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.99/1.92 % (3105913)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3905194484:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.99/1.92 % (3105914)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3671696050:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.99/1.92 % (3105916)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1656071487:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.99/1.92 % (3105917)Refutation not found, incomplete strategy
% 5.99/1.92 % (3105917)------------------------------
% 5.99/1.92 % (3105917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105917)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105917)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.92 % (3105917)Time elapsed: 0.014 s
% 5.99/1.92 % (3105917)Peak memory usage: 87 MB
% 5.99/1.92 % (3105917)Instructions burned: 23 (million)
% 5.99/1.92 % (3105914)Instruction limit reached!
% 5.99/1.92 % (3105914)------------------------------
% 5.99/1.92 % (3105914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105914)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105914)Termination reason: Instruction limit
% 5.99/1.92 % (3105914)Termination phase: Saturation
% 5.99/1.92 % (3105914)Time elapsed: 0.082 s
% 5.99/1.92 % (3105914)Peak memory usage: 88 MB
% 5.99/1.92 % (3105914)Instructions burned: 137 (million)
% 5.99/1.92 % (3105916)Refutation not found, incomplete strategy
% 5.99/1.92 % (3105916)------------------------------
% 5.99/1.92 % (3105916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105916)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105916)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.92 % (3105916)Time elapsed: 0.115 s
% 5.99/1.92 % (3105916)Peak memory usage: 90 MB
% 5.99/1.92 % (3105916)Instructions burned: 177 (million)
% 5.99/1.92 % (3105915)------------------------------
% 5.99/1.92 % (3105915)------------------------------
% 5.99/1.92 % (3105925)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3638700279:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.99/1.92 % (3105926)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=823892497:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 5.99/1.92 % (3105917)------------------------------
% 5.99/1.92 % (3105917)------------------------------
% 5.99/1.92 % (3105916)------------------------------
% 5.99/1.92 % (3105916)------------------------------
% 5.99/1.92 % (3105929)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=4218799368:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.99/1.92 % (3105929)Instruction limit reached!
% 5.99/1.92 % (3105929)------------------------------
% 5.99/1.92 % (3105929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105929)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105929)Termination reason: Instruction limit
% 5.99/1.92 % (3105929)Termination phase: Saturation
% 5.99/1.92 % (3105929)Time elapsed: 0.112 s
% 5.99/1.92 % (3105929)Peak memory usage: 93 MB
% 5.99/1.92 % (3105929)Instructions burned: 215 (million)
% 5.99/1.92 % (3105930)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2444318375:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 5.99/1.92 % (3105926)Refutation not found, incomplete strategy
% 5.99/1.92 % (3105926)------------------------------
% 5.99/1.92 % (3105926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105926)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105926)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.92 % (3105926)Time elapsed: 0.373 s
% 5.99/1.92 % (3105926)Peak memory usage: 128 MB
% 5.99/1.92 % (3105926)Instructions burned: 1010 (million)
% 5.99/1.92 % (3105933)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=1726466885:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/12125Mi)
% 5.99/1.92 % (3105930)First to succeed.
% 5.99/1.92 % (3105930)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3105906"
% 5.99/1.92 % (3105912)Also succeeded, but the first one will report.
% 5.99/1.92 % (3105913)Also succeeded, but the first one will report.
% 5.99/1.92 % (3105926)------------------------------
% 5.99/1.92 % (3105926)------------------------------
% 5.99/1.92 % (3105911)Refutation not found, incomplete strategy
% 5.99/1.92 % (3105911)------------------------------
% 5.99/1.92 % (3105911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.92 % (3105911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.92 % (3105911)CaDiCaL version: 2.1.3
% 5.99/1.92 % (3105911)Termination reason: Refutation not found, incomplete strategy
% 5.99/1.92 % (3105911)Time elapsed: 0.828 s
% 5.99/1.92 % (3105911)Peak memory usage: 130 MB
% 5.99/1.92 % (3105911)Instructions burned: 1242 (million)
% 5.99/1.92 % (3105935)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1306202196:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 5.99/1.92 % (3105935)Also succeeded, but the first one will report.
% 5.99/1.92 % SZS status Satisfiable for theBenchmark
% 5.99/1.92 % SZS output start Saturation.
% See solution above
% 8.16/2.12 % SZS output start Definitions and Model Updates.
% 8.16/2.12 % SZS output end Definitions and Model Updates.
% 8.16/2.12 % (3105930)------------------------------
% 8.16/2.12 % (3105930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.16/2.12 % (3105930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.16/2.12 % (3105930)CaDiCaL version: 2.1.3
% 8.16/2.12 % (3105930)Termination reason: Satisfiable
% 8.16/2.12 % (3105930)Time elapsed: 0.153 s
% 8.16/2.12 % (3105930)Peak memory usage: 94 MB
% 8.16/2.12 % (3105930)Instructions burned: 285 (million)
% 8.16/2.12 % (3105930)------------------------------
% 8.16/2.12 % (3105930)------------------------------
% 8.16/2.12 % (3105906)Success in time 1.077 s
% 8.16/2.12 % Vampire exiting
%------------------------------------------------------------------------------