%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP128-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:07:31 PM UTC 2026
% Result : Satisfiable 5.29s 1.88s
% Output : Saturation 7.72s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u174,negated_conjecture,
a != b ).
cnf(u179,negated_conjecture,
true = sF20 ).
cnf(u184,negated_conjecture,
true = sF19 ).
cnf(u189,negated_conjecture,
true = sF18 ).
cnf(u194,negated_conjecture,
true = sF17 ).
cnf(u199,negated_conjecture,
true = sF16 ).
cnf(u204,negated_conjecture,
true = sF15 ).
cnf(u209,negated_conjecture,
true = sF14 ).
cnf(u214,negated_conjecture,
true = sF13 ).
cnf(u219,negated_conjecture,
true = sF12 ).
cnf(u224,negated_conjecture,
true = sF11 ).
cnf(u229,negated_conjecture,
true = sF10 ).
cnf(u234,negated_conjecture,
true = sF9 ).
cnf(u239,negated_conjecture,
true = sF8 ).
cnf(u244,negated_conjecture,
true = sF7 ).
cnf(u249,negated_conjecture,
true = sF6 ).
cnf(u254,negated_conjecture,
true = sF5 ).
cnf(u259,negated_conjecture,
true = sF4 ).
cnf(u268,axiom,
actual_world(skc5) = sF4 ).
cnf(u273,axiom,
hollywood_placename(skc5,skc9) = sF5 ).
cnf(u278,axiom,
placename(skc5,skc9) = sF6 ).
cnf(u283,axiom,
street(skc5,skc7) = sF7 ).
cnf(u288,axiom,
lonely(skc5,skc7) = sF8 ).
cnf(u293,axiom,
barrel(skc5,skc6) = sF9 ).
cnf(u298,axiom,
present(skc5,skc6) = sF10 ).
cnf(u303,axiom,
event(skc5,skc6) = sF11 ).
cnf(u308,axiom,
old(skc5,skc8) = sF12 ).
cnf(u313,axiom,
dirty(skc5,skc8) = sF13 ).
cnf(u318,axiom,
white(skc5,skc8) = sF14 ).
cnf(u323,axiom,
chevy(skc5,skc8) = sF15 ).
cnf(u328,axiom,
city(skc5,skc8) = sF16 ).
cnf(u333,axiom,
of(skc5,skc9,skc8) = sF17 ).
cnf(u338,axiom,
down(skc5,skc6,skc7) = sF18 ).
cnf(u343,axiom,
in(skc5,skc6,skc8) = sF19 ).
cnf(u348,axiom,
agent(skc5,skc6,skc8) = sF20 ).
cnf(u355,negated_conjecture,
sF19 = sF20 ).
cnf(u364,negated_conjecture,
sF18 = sF20 ).
cnf(u369,negated_conjecture,
sF18 = sF19 ).
cnf(u380,negated_conjecture,
sF17 = sF20 ).
cnf(u385,negated_conjecture,
sF17 = sF19 ).
cnf(u390,negated_conjecture,
sF17 = sF18 ).
cnf(u403,negated_conjecture,
sF16 = sF20 ).
cnf(u408,negated_conjecture,
sF16 = sF19 ).
cnf(u413,negated_conjecture,
sF16 = sF18 ).
cnf(u418,negated_conjecture,
sF16 = sF17 ).
cnf(u433,negated_conjecture,
sF15 = sF20 ).
cnf(u438,negated_conjecture,
sF15 = sF19 ).
cnf(u443,negated_conjecture,
sF15 = sF18 ).
cnf(u448,negated_conjecture,
sF15 = sF17 ).
cnf(u453,negated_conjecture,
sF15 = sF16 ).
cnf(u470,negated_conjecture,
sF14 = sF15 ).
cnf(u475,negated_conjecture,
sF14 = sF16 ).
cnf(u480,negated_conjecture,
sF14 = sF17 ).
cnf(u485,negated_conjecture,
sF14 = sF18 ).
cnf(u490,negated_conjecture,
sF14 = sF19 ).
cnf(u495,negated_conjecture,
sF14 = sF20 ).
cnf(u514,negated_conjecture,
sF13 = sF14 ).
cnf(u519,negated_conjecture,
sF13 = sF15 ).
cnf(u524,negated_conjecture,
sF13 = sF16 ).
cnf(u529,negated_conjecture,
sF13 = sF17 ).
cnf(u534,negated_conjecture,
sF13 = sF18 ).
cnf(u539,negated_conjecture,
sF13 = sF19 ).
cnf(u544,negated_conjecture,
sF13 = sF20 ).
cnf(u565,negated_conjecture,
sF12 = sF13 ).
cnf(u570,negated_conjecture,
sF12 = sF14 ).
cnf(u575,negated_conjecture,
sF12 = sF15 ).
cnf(u580,negated_conjecture,
sF12 = sF16 ).
cnf(u585,negated_conjecture,
sF12 = sF17 ).
cnf(u590,negated_conjecture,
sF12 = sF18 ).
cnf(u595,negated_conjecture,
sF12 = sF19 ).
cnf(u600,negated_conjecture,
sF12 = sF20 ).
cnf(u623,negated_conjecture,
sF11 = sF12 ).
cnf(u628,negated_conjecture,
sF11 = sF13 ).
cnf(u633,negated_conjecture,
sF11 = sF14 ).
cnf(u638,negated_conjecture,
sF11 = sF15 ).
cnf(u643,negated_conjecture,
sF11 = sF16 ).
cnf(u648,negated_conjecture,
sF11 = sF17 ).
cnf(u653,negated_conjecture,
sF11 = sF18 ).
cnf(u658,negated_conjecture,
sF11 = sF19 ).
cnf(u663,negated_conjecture,
sF11 = sF20 ).
cnf(u688,negated_conjecture,
sF10 = sF11 ).
cnf(u693,negated_conjecture,
sF10 = sF12 ).
cnf(u698,negated_conjecture,
sF10 = sF13 ).
cnf(u703,negated_conjecture,
sF10 = sF14 ).
cnf(u708,negated_conjecture,
sF10 = sF15 ).
cnf(u713,negated_conjecture,
sF10 = sF16 ).
cnf(u718,negated_conjecture,
sF10 = sF17 ).
cnf(u723,negated_conjecture,
sF10 = sF18 ).
cnf(u728,negated_conjecture,
sF10 = sF19 ).
cnf(u733,negated_conjecture,
sF10 = sF20 ).
cnf(u760,negated_conjecture,
sF9 = sF10 ).
cnf(u765,negated_conjecture,
sF9 = sF11 ).
cnf(u770,negated_conjecture,
sF9 = sF12 ).
cnf(u775,negated_conjecture,
sF9 = sF13 ).
cnf(u780,negated_conjecture,
sF9 = sF14 ).
cnf(u785,negated_conjecture,
sF9 = sF15 ).
cnf(u790,negated_conjecture,
sF9 = sF16 ).
cnf(u795,negated_conjecture,
sF9 = sF17 ).
cnf(u800,negated_conjecture,
sF9 = sF18 ).
cnf(u805,negated_conjecture,
sF9 = sF19 ).
cnf(u810,negated_conjecture,
sF9 = sF20 ).
cnf(u839,negated_conjecture,
sF8 = sF9 ).
cnf(u844,negated_conjecture,
sF8 = sF10 ).
cnf(u849,negated_conjecture,
sF8 = sF11 ).
cnf(u854,negated_conjecture,
sF8 = sF12 ).
cnf(u859,negated_conjecture,
sF8 = sF13 ).
cnf(u864,negated_conjecture,
sF8 = sF14 ).
cnf(u869,negated_conjecture,
sF8 = sF15 ).
cnf(u874,negated_conjecture,
sF8 = sF16 ).
cnf(u879,negated_conjecture,
sF8 = sF17 ).
cnf(u884,negated_conjecture,
sF8 = sF18 ).
cnf(u889,negated_conjecture,
sF8 = sF19 ).
cnf(u894,negated_conjecture,
sF8 = sF20 ).
cnf(u925,negated_conjecture,
sF7 = sF8 ).
cnf(u930,negated_conjecture,
sF7 = sF9 ).
cnf(u935,negated_conjecture,
sF7 = sF10 ).
cnf(u940,negated_conjecture,
sF7 = sF11 ).
cnf(u945,negated_conjecture,
sF7 = sF12 ).
cnf(u950,negated_conjecture,
sF7 = sF13 ).
cnf(u955,negated_conjecture,
sF7 = sF14 ).
cnf(u960,negated_conjecture,
sF7 = sF15 ).
cnf(u965,negated_conjecture,
sF7 = sF16 ).
cnf(u970,negated_conjecture,
sF7 = sF17 ).
cnf(u975,negated_conjecture,
sF7 = sF18 ).
cnf(u980,negated_conjecture,
sF7 = sF19 ).
cnf(u985,negated_conjecture,
sF7 = sF20 ).
cnf(u1018,negated_conjecture,
sF6 = sF7 ).
cnf(u1023,negated_conjecture,
sF6 = sF8 ).
cnf(u1028,negated_conjecture,
sF6 = sF9 ).
cnf(u1033,negated_conjecture,
sF6 = sF10 ).
cnf(u1038,negated_conjecture,
sF6 = sF11 ).
cnf(u1043,negated_conjecture,
sF6 = sF12 ).
cnf(u1048,negated_conjecture,
sF6 = sF13 ).
cnf(u1053,negated_conjecture,
sF6 = sF14 ).
cnf(u1058,negated_conjecture,
sF6 = sF15 ).
cnf(u1063,negated_conjecture,
sF6 = sF16 ).
cnf(u1068,negated_conjecture,
sF6 = sF17 ).
cnf(u1073,negated_conjecture,
sF6 = sF18 ).
cnf(u1078,negated_conjecture,
sF6 = sF19 ).
cnf(u1083,negated_conjecture,
sF6 = sF20 ).
cnf(u1118,negated_conjecture,
sF5 = sF6 ).
cnf(u1123,negated_conjecture,
sF5 = sF7 ).
cnf(u1128,negated_conjecture,
sF5 = sF8 ).
cnf(u1133,negated_conjecture,
sF5 = sF9 ).
cnf(u1138,negated_conjecture,
sF5 = sF10 ).
cnf(u1143,negated_conjecture,
sF5 = sF11 ).
cnf(u1148,negated_conjecture,
sF5 = sF12 ).
cnf(u1153,negated_conjecture,
sF5 = sF13 ).
cnf(u1158,negated_conjecture,
sF5 = sF14 ).
cnf(u1163,negated_conjecture,
sF5 = sF15 ).
cnf(u1168,negated_conjecture,
sF5 = sF16 ).
cnf(u1173,negated_conjecture,
sF5 = sF17 ).
cnf(u1178,negated_conjecture,
sF5 = sF18 ).
cnf(u1183,negated_conjecture,
sF5 = sF19 ).
cnf(u1188,negated_conjecture,
sF5 = sF20 ).
cnf(u1225,negated_conjecture,
sF4 = sF5 ).
cnf(u1230,negated_conjecture,
sF4 = sF6 ).
cnf(u1235,negated_conjecture,
sF4 = sF7 ).
cnf(u1240,negated_conjecture,
sF4 = sF8 ).
cnf(u1245,negated_conjecture,
sF4 = sF9 ).
cnf(u1250,negated_conjecture,
sF4 = sF10 ).
cnf(u1255,negated_conjecture,
sF4 = sF11 ).
cnf(u1260,negated_conjecture,
sF4 = sF12 ).
cnf(u1265,negated_conjecture,
sF4 = sF13 ).
cnf(u1270,negated_conjecture,
sF4 = sF14 ).
cnf(u1275,negated_conjecture,
sF4 = sF15 ).
cnf(u1280,negated_conjecture,
sF4 = sF16 ).
cnf(u1285,negated_conjecture,
sF4 = sF17 ).
cnf(u1290,negated_conjecture,
sF4 = sF18 ).
cnf(u1295,negated_conjecture,
sF4 = sF19 ).
cnf(u1300,negated_conjecture,
sF4 = sF20 ).
cnf(u2639,negated_conjecture,
event(skc5,skc6) = sF4 ).
cnf(u2820,negated_conjecture,
sF4 = eventuality(skc5,skc6) ).
cnf(u3023,negated_conjecture,
sF4 = thing(skc5,skc6) ).
cnf(u3035,negated_conjecture,
sF4 = singleton(skc5,skc6) ).
cnf(u3267,negated_conjecture,
sF4 = specific(skc5,skc6) ).
cnf(u3463,negated_conjecture,
sF4 = nonexistent(skc5,skc6) ).
cnf(u3682,negated_conjecture,
sF4 = unisex(skc5,skc6) ).
cnf(u3896,negated_conjecture,
sF4 = way(skc5,skc7) ).
cnf(u4100,negated_conjecture,
sF4 = artifact(skc5,skc7) ).
cnf(u4301,negated_conjecture,
sF4 = object(skc5,skc7) ).
cnf(u4318,negated_conjecture,
sF4 = nonliving(skc5,skc7) ).
cnf(u4323,negated_conjecture,
sF4 = impartial(skc5,skc7) ).
cnf(u4598,negated_conjecture,
sF4 = entity(skc5,skc7) ).
cnf(u4811,negated_conjecture,
sF4 = ifeq2(entity(skc5,skc6),sF4,sF4,sF4) ).
cnf(u4817,negated_conjecture,
sF4 = thing(skc5,skc7) ).
cnf(u4830,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc7),sF4,sF4,sF4) ).
cnf(u4837,negated_conjecture,
sF4 = singleton(skc5,skc7) ).
cnf(u5110,negated_conjecture,
sF4 = specific(skc5,skc7) ).
cnf(u5337,negated_conjecture,
sF4 = existent(skc5,skc7) ).
cnf(u5555,negated_conjecture,
sF4 = ifeq2(object(skc5,skc6),sF4,sF4,sF4) ).
cnf(u5561,negated_conjecture,
sF4 = unisex(skc5,skc7) ).
cnf(u5783,negated_conjecture,
sF4 = relname(skc5,skc9) ).
cnf(u5986,negated_conjecture,
sF4 = relation(skc5,skc9) ).
cnf(u6182,negated_conjecture,
sF4 = abstraction(skc5,skc9) ).
cnf(u6194,negated_conjecture,
sF4 = nonhuman(skc5,skc9) ).
cnf(u6468,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc7),sF4,sF4,sF4) ).
cnf(u6473,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc6),sF4,sF4,sF4) ).
cnf(u6479,negated_conjecture,
sF4 = thing(skc5,skc9) ).
cnf(u6491,negated_conjecture,
sF4 = ifeq2(entity(skc5,skc9),sF4,sF4,sF4) ).
cnf(u6496,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc9),sF4,sF4,sF4) ).
cnf(u6506,negated_conjecture,
sF4 = singleton(skc5,skc9) ).
cnf(u6780,negated_conjecture,
sF4 = general(skc5,skc9) ).
cnf(u7019,negated_conjecture,
sF4 = unisex(skc5,skc9) ).
cnf(u7081,negated_conjecture,
sF4 = ifeq2(object(skc5,skc9),sF4,sF4,sF4) ).
cnf(u7288,negated_conjecture,
placename(skc5,skc9) = sF4 ).
cnf(u7465,negated_conjecture,
sF4 = location(skc5,skc8) ).
cnf(u7698,negated_conjecture,
sF4 = ifeq2(location(skc5,skc7),sF4,sF4,sF4) ).
cnf(u7704,negated_conjecture,
sF4 = object(skc5,skc8) ).
cnf(u7722,negated_conjecture,
sF4 = ifeq2(artifact(skc5,skc8),sF4,sF4,sF4) ).
cnf(u7735,negated_conjecture,
sF4 = unisex(skc5,skc8) ).
cnf(u7740,negated_conjecture,
sF4 = entity(skc5,skc8) ).
cnf(u7745,negated_conjecture,
sF4 = impartial(skc5,skc8) ).
cnf(u7750,negated_conjecture,
sF4 = nonliving(skc5,skc8) ).
cnf(u7867,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc8),sF4,sF4,sF4) ).
cnf(u7925,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc8),sF4,sF4,sF4) ).
cnf(u7946,negated_conjecture,
sF4 = existent(skc5,skc8) ).
cnf(u7951,negated_conjecture,
sF4 = specific(skc5,skc8) ).
cnf(u7956,negated_conjecture,
sF4 = thing(skc5,skc8) ).
cnf(u8156,negated_conjecture,
sF4 = singleton(skc5,skc8) ).
cnf(u8402,negated_conjecture,
sF4 = car(skc5,skc8) ).
cnf(u8630,negated_conjecture,
sF4 = vehicle(skc5,skc8) ).
cnf(u8831,negated_conjecture,
sF4 = transport(skc5,skc8) ).
cnf(u9038,negated_conjecture,
sF4 = instrumentality(skc5,skc8) ).
cnf(u9256,negated_conjecture,
sF4 = ifeq2(instrumentality(skc5,skc7),sF4,sF4,sF4) ).
cnf(u9262,negated_conjecture,
sF4 = artifact(skc5,skc8) ).
cnf(u9275,negated_conjecture,
sF4 = ifeq2(way(skc5,skc8),sF4,sF4,sF4) ).
cnf(u9571,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc9),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9576,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc8)),tuple(sF4,sF4),a,b) ).
cnf(u9581,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc7)),tuple(sF4,sF4),a,b) ).
cnf(u9586,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc6)),tuple(sF4,sF4),a,b) ).
cnf(u9807,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc8),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9812,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc7),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9817,negated_conjecture,
b = ifeq(tuple(sF4,existent(skc5,skc6)),tuple(sF4,sF4),a,b) ).
cnf(u10453,negated_conjecture,
skc9 = ifeq3(of(skc5,skc9,skc7),sF4,ifeq3(of(skc5,skc9,skc7),sF4,skc9,skc9),skc9) ).
cnf(u10282,negated_conjecture,
skc9 = ifeq3(of(skc5,skc9,X0),sF4,ifeq3(of(skc5,skc9,X0),sF4,ifeq3(entity(skc5,X0),sF4,skc9,skc9),skc9),skc9) ).
cnf(u5625,negated_conjecture,
sF4 = ifeq2(placename(X0,X1),sF4,relname(X0,X1),sF4) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u37,axiom,
true = ifeq2(object(X0,X1),true,unisex(X0,X1),true) ).
cnf(u49,axiom,
true = ifeq2(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u6825,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u5828,negated_conjecture,
sF4 = ifeq2(relname(X0,X1),sF4,relation(X0,X1),sF4) ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u4934,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,specific(X0,X1),sF4) ).
cnf(u25,axiom,
true = ifeq2(object(X0,X1),true,entity(X0,X1),true) ).
cnf(u10108,negated_conjecture,
ifeq3(of(skc5,X0,skc8),sF4,ifeq3(of(skc5,X1,skc8),sF4,ifeq3(placename(skc5,X0),sF4,ifeq3(placename(skc5,X1),sF4,X0,X1),X1),X1),X1) = X1 ).
cnf(u4440,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,entity(X0,X1),sF4) ).
cnf(u116,negated_conjecture,
true = sF2(X0,X1) ).
cnf(u9616,negated_conjecture,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(clause35,axiom,
ifeq3(of(X0,X1,X2),true,ifeq3(of(X0,X3,X2),true,ifeq3(placename(X0,X1),true,ifeq3(placename(X0,X3),true,ifeq3(entity(X0,X2),true,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u8244,negated_conjecture,
sF4 = ifeq2(chevy(X0,X1),sF4,car(X0,X1),sF4) ).
cnf(u3305,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,nonexistent(X0,X1),sF4) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u29,axiom,
true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u2462,negated_conjecture,
sF4 = ifeq2(barrel(X0,X1),sF4,event(X0,X1),sF4) ).
cnf(u263,negated_conjecture,
true = ifeq2(object(X0,X1),true,impartial(X0,X1),true) ).
cnf(u55,axiom,
true = ifeq2(city(X0,X1),true,location(X0,X1),true) ).
cnf(u9869,negated_conjecture,
ifeq3(of(X0,X1,X2),sF4,ifeq3(of(X0,X3,X2),sF4,ifeq3(placename(X0,X1),sF4,ifeq3(placename(X0,X3),sF4,ifeq3(entity(X0,X2),sF4,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u10273,negated_conjecture,
skc9 = ifeq3(of(skc5,X0,skc7),sF4,ifeq3(of(skc5,skc9,skc7),sF4,ifeq3(placename(skc5,X0),sF4,X0,skc9),skc9),skc9) ).
cnf(u8880,negated_conjecture,
sF4 = ifeq2(transport(X0,X1),sF4,instrumentality(X0,X1),sF4) ).
cnf(u5,axiom,
true = ifeq2(barrel(X0,X1),true,event(X0,X1),true) ).
cnf(u2662,negated_conjecture,
sF4 = ifeq2(event(X0,X1),sF4,eventuality(X0,X1),sF4) ).
cnf(u31,axiom,
true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u43,axiom,
true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u9363,negated_conjecture,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u23,axiom,
true = ifeq2(artifact(X0,X1),true,object(X0,X1),true) ).
cnf(u106,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u6024,negated_conjecture,
sF4 = ifeq2(relation(X0,X1),sF4,abstraction(X0,X1),sF4) ).
cnf(u7111,negated_conjecture,
sF4 = ifeq2(hollywood_placename(X0,X1),sF4,placename(X0,X1),sF4) ).
cnf(u10124,negated_conjecture,
skc9 = ifeq3(of(skc5,X0,skc8),sF4,ifeq3(placename(skc5,X0),sF4,X0,skc9),skc9) ).
cnf(u19,axiom,
true = ifeq2(street(X0,X1),true,way(X0,X1),true) ).
cnf(u110,negated_conjecture,
true = sF0(X0,X1) ).
cnf(u261,negated_conjecture,
true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u53,axiom,
true = ifeq2(hollywood_placename(X0,X1),true,placename(X0,X1),true) ).
cnf(u67,axiom,
true = ifeq2(instrumentality(X0,X1),true,artifact(X0,X1),true) ).
cnf(u262,negated_conjecture,
true = ifeq2(object(X0,X1),true,nonliving(X0,X1),true) ).
cnf(u41,axiom,
true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u104,axiom,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).
cnf(u10111,negated_conjecture,
ifeq3(of(skc5,skc9,X0),sF4,ifeq3(of(skc5,X1,X0),sF4,ifeq3(placename(skc5,X1),sF4,ifeq3(entity(skc5,X0),sF4,skc9,X1),X1),X1),X1) = X1 ).
cnf(u4143,negated_conjecture,
sF4 = ifeq2(artifact(X0,X1),sF4,object(X0,X1),sF4) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u10109,negated_conjecture,
ifeq3(of(skc5,X0,skc7),sF4,ifeq3(of(skc5,X1,skc7),sF4,ifeq3(placename(skc5,X0),sF4,ifeq3(placename(skc5,X1),sF4,X0,X1),X1),X1),X1) = X1 ).
cnf(u9082,negated_conjecture,
sF4 = ifeq2(instrumentality(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u17,axiom,
true = ifeq2(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u45,axiom,
true = ifeq2(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u8472,negated_conjecture,
sF4 = ifeq2(car(X0,X1),sF4,vehicle(X0,X1),sF4) ).
cnf(u10334,negated_conjecture,
ifeq3(of(skc5,skc9,skc7),sF4,ifeq3(of(skc5,X0,skc7),sF4,ifeq3(placename(skc5,X0),sF4,skc9,X0),X0),X0) = X0 ).
cnf(u21,axiom,
true = ifeq2(way(X0,X1),true,artifact(X0,X1),true) ).
cnf(u264,negated_conjecture,
true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u7524,negated_conjecture,
sF4 = ifeq2(location(X0,X1),sF4,object(X0,X1),sF4) ).
cnf(u4637,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u7307,negated_conjecture,
sF4 = ifeq2(city(X0,X1),sF4,location(X0,X1),sF4) ).
cnf(u65,axiom,
true = ifeq2(transport(X0,X1),true,instrumentality(X0,X1),true) ).
cnf(u59,axiom,
true = ifeq2(chevy(X0,X1),true,car(X0,X1),true) ).
cnf(u119,negated_conjecture,
true = sF3(X0,X1) ).
cnf(u1848,negated_conjecture,
sF4 = ifeq2(thing(X0,X1),sF4,singleton(X0,X1),sF4) ).
cnf(u2307,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,nonhuman(X0,X1),sF4) ).
cnf(u3942,negated_conjecture,
sF4 = ifeq2(way(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u9,axiom,
true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u2154,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,impartial(X0,X1),sF4) ).
cnf(u13,axiom,
true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u113,negated_conjecture,
true = sF1(X0,X1) ).
cnf(u5179,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,existent(X0,X1),sF4) ).
cnf(u6622,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,general(X0,X1),sF4) ).
cnf(u39,axiom,
true = ifeq2(placename(X0,X1),true,relname(X0,X1),true) ).
cnf(u3738,negated_conjecture,
sF4 = ifeq2(street(X0,X1),sF4,way(X0,X1),sF4) ).
cnf(u5381,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u57,axiom,
true = ifeq2(location(X0,X1),true,object(X0,X1),true) ).
cnf(u3109,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,specific(X0,X1),sF4) ).
cnf(u2001,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,nonliving(X0,X1),sF4) ).
cnf(u2865,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u8673,negated_conjecture,
sF4 = ifeq2(vehicle(X0,X1),sF4,transport(X0,X1),sF4) ).
cnf(u15,axiom,
true = ifeq2(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u27,axiom,
true = ifeq2(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u6277,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u10110,negated_conjecture,
skc9 = ifeq3(of(skc5,X0,X1),sF4,ifeq3(of(skc5,skc9,X1),sF4,ifeq3(placename(skc5,X0),sF4,ifeq3(entity(skc5,X1),sF4,X0,skc9),skc9),skc9),skc9) ).
cnf(u3524,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u63,axiom,
true = ifeq2(vehicle(X0,X1),true,transport(X0,X1),true) ).
cnf(u61,axiom,
true = ifeq2(car(X0,X1),true,vehicle(X0,X1),true) ).
cnf(u10125,negated_conjecture,
ifeq3(of(skc5,X0,skc8),sF4,ifeq3(placename(skc5,X0),sF4,skc9,X0),X0) = X0 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP128-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n018.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 18:09:23 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.88 % (2644175)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.29/1.88 % (2644183)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2506293285:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.29/1.88 % (2644183)Refutation not found, incomplete strategy
% 5.29/1.88 % (2644183)------------------------------
% 5.29/1.88 % (2644183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644183)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644183)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.88 % (2644183)Time elapsed: 0.028 s
% 5.29/1.88 % (2644183)Peak memory usage: 88 MB
% 5.29/1.88 % (2644183)Instructions burned: 100 (million)
% 5.29/1.88 % (2644186)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1035994909:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.29/1.88 % (2644182)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1772297205:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.29/1.88 % (2644180)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=293512972:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.29/1.88 % (2644184)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1840788730:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.29/1.88 % (2644181)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=4258195824:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.29/1.88 % (2644185)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1499053259:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.29/1.88 % (2644186)Refutation not found, incomplete strategy
% 5.29/1.88 % (2644186)------------------------------
% 5.29/1.88 % (2644186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644186)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644186)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.88 % (2644186)Time elapsed: 0.014 s
% 5.29/1.88 % (2644186)Peak memory usage: 87 MB
% 5.29/1.88 % (2644186)Instructions burned: 22 (million)
% 5.29/1.88 % (2644184)Refutation not found, incomplete strategy
% 5.29/1.88 % (2644184)------------------------------
% 5.29/1.88 % (2644184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644184)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644184)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.88 % (2644184)Time elapsed: 0.018 s
% 5.29/1.88 % (2644184)Peak memory usage: 88 MB
% 5.29/1.88 % (2644184)Instructions burned: 29 (million)
% 5.29/1.88 % (2644185)Refutation not found, incomplete strategy
% 5.29/1.88 % (2644185)------------------------------
% 5.29/1.88 % (2644185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644185)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644185)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.88 % (2644185)Time elapsed: 0.065 s
% 5.29/1.88 % (2644185)Peak memory usage: 89 MB
% 5.29/1.88 % (2644185)Instructions burned: 114 (million)
% 5.29/1.88 % (2644183)------------------------------
% 5.29/1.88 % (2644183)------------------------------
% 5.29/1.88 % (2644184)------------------------------
% 5.29/1.88 % (2644184)------------------------------
% 5.29/1.88 % (2644186)------------------------------
% 5.29/1.88 % (2644186)------------------------------
% 5.29/1.88 % (2644194)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2407742779:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 5.29/1.88 % (2644185)------------------------------
% 5.29/1.88 % (2644185)------------------------------
% 5.29/1.88 % (2644196)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1386699230:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.29/1.88 % (2644195)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=401149243:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 5.29/1.88 % (2644198)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=2737698391:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 5.29/1.88 % (2644196)Instruction limit reached!
% 5.29/1.88 % (2644196)------------------------------
% 5.29/1.88 % (2644196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644196)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644196)Termination reason: Instruction limit
% 5.29/1.88 % (2644196)Termination phase: Saturation
% 5.29/1.88 % (2644196)Time elapsed: 0.108 s
% 5.29/1.88 % (2644196)Peak memory usage: 92 MB
% 5.29/1.88 % (2644196)Instructions burned: 215 (million)
% 5.29/1.88 % (2644198)First to succeed.
% 5.29/1.88 % (2644198)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2644175"
% 5.29/1.88 % (2644194)Refutation not found, incomplete strategy
% 5.29/1.88 % (2644194)------------------------------
% 5.29/1.88 % (2644194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644194)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644194)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.88 % (2644194)Time elapsed: 0.371 s
% 5.29/1.88 % (2644194)Peak memory usage: 129 MB
% 5.29/1.88 % (2644194)Instructions burned: 1001 (million)
% 5.29/1.88 % (2644181)Also succeeded, but the first one will report.
% 5.29/1.88 % (2644182)Also succeeded, but the first one will report.
% 5.29/1.88 % (2644202)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=3980203618:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 5.29/1.88 % (2644180)Refutation not found, incomplete strategy
% 5.29/1.88 % (2644180)------------------------------
% 5.29/1.88 % (2644180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.29/1.88 % (2644180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.29/1.88 % (2644180)CaDiCaL version: 2.1.3
% 5.29/1.88 % (2644180)Termination reason: Refutation not found, incomplete strategy
% 5.29/1.88 % (2644180)Time elapsed: 0.761 s
% 5.29/1.88 % (2644180)Peak memory usage: 130 MB
% 5.29/1.88 % (2644180)Instructions burned: 1138 (million)
% 5.29/1.88 % (2644194)------------------------------
% 5.29/1.88 % (2644194)------------------------------
% 5.29/1.88 % SZS status Satisfiable for theBenchmark
% 5.29/1.88 % SZS output start Saturation.
% See solution above
% 7.72/1.98 % SZS output start Definitions and Model Updates.
% 7.72/1.98 % SZS output end Definitions and Model Updates.
% 7.72/1.98 % (2644198)------------------------------
% 7.72/1.98 % (2644198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.72/1.98 % (2644198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.72/1.98 % (2644198)CaDiCaL version: 2.1.3
% 7.72/1.98 % (2644198)Termination reason: Satisfiable
% 7.72/1.98 % (2644198)Time elapsed: 0.105 s
% 7.72/1.98 % (2644198)Peak memory usage: 92 MB
% 7.72/1.98 % (2644198)Instructions burned: 188 (million)
% 7.72/1.98 % (2644198)------------------------------
% 7.72/1.98 % (2644198)------------------------------
% 7.72/1.98 % (2644175)Success in time 1.03 s
% 7.72/1.98 % Vampire exiting
%------------------------------------------------------------------------------