%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP124-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 : n008.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:29 PM UTC 2026
% Result : Satisfiable 5.53s 1.92s
% Output : Saturation 7.85s
% 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(skc6) = sF4 ).
cnf(u273,axiom,
street(skc6,skc11) = sF5 ).
cnf(u278,axiom,
city(skc6,skc10) = sF6 ).
cnf(u283,axiom,
old(skc6,skc8) = sF7 ).
cnf(u288,axiom,
dirty(skc6,skc8) = sF8 ).
cnf(u293,axiom,
white(skc6,skc8) = sF9 ).
cnf(u298,axiom,
chevy(skc6,skc8) = sF10 ).
cnf(u303,axiom,
placename(skc6,skc9) = sF11 ).
cnf(u308,axiom,
hollywood_placename(skc6,skc9) = sF12 ).
cnf(u313,axiom,
event(skc6,skc7) = sF13 ).
cnf(u318,axiom,
present(skc6,skc7) = sF14 ).
cnf(u323,axiom,
barrel(skc6,skc7) = sF15 ).
cnf(u328,axiom,
lonely(skc6,skc11) = sF16 ).
cnf(u333,axiom,
of(skc6,skc9,skc10) = sF17 ).
cnf(u338,axiom,
in(skc6,skc7,skc10) = sF18 ).
cnf(u343,axiom,
agent(skc6,skc7,skc8) = sF19 ).
cnf(u348,axiom,
down(skc6,skc7,skc11) = 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(skc6,skc7) = sF4 ).
cnf(u2826,negated_conjecture,
sF4 = eventuality(skc6,skc7) ).
cnf(u3031,negated_conjecture,
sF4 = thing(skc6,skc7) ).
cnf(u3043,negated_conjecture,
sF4 = singleton(skc6,skc7) ).
cnf(u3275,negated_conjecture,
sF4 = specific(skc6,skc7) ).
cnf(u3471,negated_conjecture,
sF4 = nonexistent(skc6,skc7) ).
cnf(u3711,negated_conjecture,
sF4 = unisex(skc6,skc7) ).
cnf(u3929,negated_conjecture,
sF4 = way(skc6,skc11) ).
cnf(u4131,negated_conjecture,
sF4 = artifact(skc6,skc11) ).
cnf(u4332,negated_conjecture,
sF4 = object(skc6,skc11) ).
cnf(u4349,negated_conjecture,
sF4 = nonliving(skc6,skc11) ).
cnf(u4354,negated_conjecture,
sF4 = impartial(skc6,skc11) ).
cnf(u4629,negated_conjecture,
sF4 = entity(skc6,skc11) ).
cnf(u4842,negated_conjecture,
sF4 = ifeq2(entity(skc6,skc7),sF4,sF4,sF4) ).
cnf(u4848,negated_conjecture,
sF4 = thing(skc6,skc11) ).
cnf(u4861,negated_conjecture,
sF4 = ifeq2(eventuality(skc6,skc11),sF4,sF4,sF4) ).
cnf(u4868,negated_conjecture,
sF4 = singleton(skc6,skc11) ).
cnf(u5141,negated_conjecture,
sF4 = specific(skc6,skc11) ).
cnf(u5364,negated_conjecture,
sF4 = existent(skc6,skc11) ).
cnf(u5582,negated_conjecture,
sF4 = ifeq2(object(skc6,skc7),sF4,sF4,sF4) ).
cnf(u5588,negated_conjecture,
sF4 = unisex(skc6,skc11) ).
cnf(u5810,negated_conjecture,
sF4 = relname(skc6,skc9) ).
cnf(u6018,negated_conjecture,
sF4 = relation(skc6,skc9) ).
cnf(u6214,negated_conjecture,
sF4 = abstraction(skc6,skc9) ).
cnf(u6226,negated_conjecture,
sF4 = nonhuman(skc6,skc9) ).
cnf(u6500,negated_conjecture,
sF4 = ifeq2(abstraction(skc6,skc11),sF4,sF4,sF4) ).
cnf(u6505,negated_conjecture,
sF4 = ifeq2(abstraction(skc6,skc7),sF4,sF4,sF4) ).
cnf(u6511,negated_conjecture,
sF4 = thing(skc6,skc9) ).
cnf(u6523,negated_conjecture,
sF4 = ifeq2(entity(skc6,skc9),sF4,sF4,sF4) ).
cnf(u6528,negated_conjecture,
sF4 = ifeq2(eventuality(skc6,skc9),sF4,sF4,sF4) ).
cnf(u6538,negated_conjecture,
sF4 = singleton(skc6,skc9) ).
cnf(u6812,negated_conjecture,
sF4 = general(skc6,skc9) ).
cnf(u7051,negated_conjecture,
sF4 = unisex(skc6,skc9) ).
cnf(u7113,negated_conjecture,
sF4 = ifeq2(object(skc6,skc9),sF4,sF4,sF4) ).
cnf(u7320,negated_conjecture,
placename(skc6,skc9) = sF4 ).
cnf(u7504,negated_conjecture,
sF4 = location(skc6,skc10) ).
cnf(u7737,negated_conjecture,
sF4 = ifeq2(location(skc6,skc11),sF4,sF4,sF4) ).
cnf(u7743,negated_conjecture,
sF4 = object(skc6,skc10) ).
cnf(u7761,negated_conjecture,
sF4 = ifeq2(artifact(skc6,skc10),sF4,sF4,sF4) ).
cnf(u7774,negated_conjecture,
sF4 = unisex(skc6,skc10) ).
cnf(u7779,negated_conjecture,
sF4 = entity(skc6,skc10) ).
cnf(u7784,negated_conjecture,
sF4 = impartial(skc6,skc10) ).
cnf(u7789,negated_conjecture,
sF4 = nonliving(skc6,skc10) ).
cnf(u7906,negated_conjecture,
sF4 = ifeq2(eventuality(skc6,skc10),sF4,sF4,sF4) ).
cnf(u7964,negated_conjecture,
sF4 = ifeq2(abstraction(skc6,skc10),sF4,sF4,sF4) ).
cnf(u7985,negated_conjecture,
sF4 = existent(skc6,skc10) ).
cnf(u7990,negated_conjecture,
sF4 = specific(skc6,skc10) ).
cnf(u7995,negated_conjecture,
sF4 = thing(skc6,skc10) ).
cnf(u8195,negated_conjecture,
sF4 = singleton(skc6,skc10) ).
cnf(u8441,negated_conjecture,
sF4 = car(skc6,skc8) ).
cnf(u8664,negated_conjecture,
sF4 = vehicle(skc6,skc8) ).
cnf(u8865,negated_conjecture,
sF4 = transport(skc6,skc8) ).
cnf(u9072,negated_conjecture,
sF4 = instrumentality(skc6,skc8) ).
cnf(u9290,negated_conjecture,
sF4 = ifeq2(instrumentality(skc6,skc11),sF4,sF4,sF4) ).
cnf(u9296,negated_conjecture,
sF4 = artifact(skc6,skc8) ).
cnf(u9308,negated_conjecture,
sF4 = ifeq2(way(skc6,skc8),sF4,sF4,sF4) ).
cnf(u9317,negated_conjecture,
sF4 = object(skc6,skc8) ).
cnf(u9394,negated_conjecture,
sF4 = unisex(skc6,skc8) ).
cnf(u9399,negated_conjecture,
sF4 = entity(skc6,skc8) ).
cnf(u9404,negated_conjecture,
sF4 = impartial(skc6,skc8) ).
cnf(u9409,negated_conjecture,
sF4 = nonliving(skc6,skc8) ).
cnf(u9512,negated_conjecture,
sF4 = ifeq2(location(skc6,skc8),sF4,sF4,sF4) ).
cnf(u9530,negated_conjecture,
sF4 = ifeq2(eventuality(skc6,skc8),sF4,sF4,sF4) ).
cnf(u9588,negated_conjecture,
sF4 = ifeq2(abstraction(skc6,skc8),sF4,sF4,sF4) ).
cnf(u9609,negated_conjecture,
sF4 = existent(skc6,skc8) ).
cnf(u9614,negated_conjecture,
sF4 = specific(skc6,skc8) ).
cnf(u9619,negated_conjecture,
sF4 = thing(skc6,skc8) ).
cnf(u10056,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc9),sF4),tuple(sF4,sF4),a,b) ).
cnf(u10061,negated_conjecture,
b = ifeq(tuple(sF4,general(skc6,skc7)),tuple(sF4,sF4),a,b) ).
cnf(u10066,negated_conjecture,
b = ifeq(tuple(sF4,general(skc6,skc8)),tuple(sF4,sF4),a,b) ).
cnf(u10071,negated_conjecture,
b = ifeq(tuple(sF4,general(skc6,skc10)),tuple(sF4,sF4),a,b) ).
cnf(u10076,negated_conjecture,
b = ifeq(tuple(sF4,general(skc6,skc11)),tuple(sF4,sF4),a,b) ).
cnf(u10097,negated_conjecture,
sF4 = singleton(skc6,skc8) ).
cnf(u10417,negated_conjecture,
b = ifeq(tuple(nonexistent(skc6,skc8),sF4),tuple(sF4,sF4),a,b) ).
cnf(u10422,negated_conjecture,
b = ifeq(tuple(nonexistent(skc6,skc10),sF4),tuple(sF4,sF4),a,b) ).
cnf(u10427,negated_conjecture,
b = ifeq(tuple(nonexistent(skc6,skc11),sF4),tuple(sF4,sF4),a,b) ).
cnf(u10432,negated_conjecture,
b = ifeq(tuple(sF4,existent(skc6,skc7)),tuple(sF4,sF4),a,b) ).
cnf(u11174,negated_conjecture,
skc9 = ifeq3(of(skc6,skc9,skc8),sF4,ifeq3(of(skc6,skc9,skc8),sF4,skc9,skc9),skc9) ).
cnf(u11180,negated_conjecture,
skc9 = ifeq3(of(skc6,skc9,skc11),sF4,ifeq3(of(skc6,skc9,skc11),sF4,skc9,skc9),skc9) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u9831,negated_conjecture,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(sF4,sF4),a,b) ).
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(u8914,negated_conjecture,
sF4 = ifeq2(transport(X0,X1),sF4,instrumentality(X0,X1),sF4) ).
cnf(u4668,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u8506,negated_conjecture,
sF4 = ifeq2(car(X0,X1),sF4,vehicle(X0,X1),sF4) ).
cnf(u8283,negated_conjecture,
sF4 = ifeq2(chevy(X0,X1),sF4,car(X0,X1),sF4) ).
cnf(u6056,negated_conjecture,
sF4 = ifeq2(relation(X0,X1),sF4,abstraction(X0,X1),sF4) ).
cnf(u25,axiom,
true = ifeq2(object(X0,X1),true,entity(X0,X1),true) ).
cnf(u10491,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(u7143,negated_conjecture,
sF4 = ifeq2(hollywood_placename(X0,X1),sF4,placename(X0,X1),sF4) ).
cnf(u116,negated_conjecture,
true = sF2(X0,X1) ).
cnf(u10774,negated_conjecture,
skc9 = ifeq3(of(skc6,X0,skc10),sF4,ifeq3(placename(skc6,X0),sF4,X0,skc9),skc9) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u10750,negated_conjecture,
skc9 = ifeq3(of(skc6,X0,X1),sF4,ifeq3(of(skc6,skc9,X1),sF4,ifeq3(placename(skc6,X0),sF4,ifeq3(entity(skc6,X1),sF4,X0,skc9),skc9),skc9),skc9) ).
cnf(u10775,negated_conjecture,
ifeq3(of(skc6,X0,skc10),sF4,ifeq3(placename(skc6,X0),sF4,skc9,X0),X0) = X0 ).
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(u5,axiom,
true = ifeq2(barrel(X0,X1),true,event(X0,X1),true) ).
cnf(u3117,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,specific(X0,X1),sF4) ).
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(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(u19,axiom,
true = ifeq2(street(X0,X1),true,way(X0,X1),true) ).
cnf(u10949,negated_conjecture,
skc9 = ifeq3(of(skc6,X0,skc11),sF4,ifeq3(of(skc6,skc9,skc11),sF4,ifeq3(placename(skc6,X0),sF4,X0,skc9),skc9),skc9) ).
cnf(u106,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u10751,negated_conjecture,
ifeq3(of(skc6,skc9,X0),sF4,ifeq3(of(skc6,X1,X0),sF4,ifeq3(placename(skc6,X1),sF4,ifeq3(entity(skc6,X0),sF4,skc9,X1),X1),X1),X1) = X1 ).
cnf(u3553,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u3771,negated_conjecture,
sF4 = ifeq2(street(X0,X1),sF4,way(X0,X1),sF4) ).
cnf(u5652,negated_conjecture,
sF4 = ifeq2(placename(X0,X1),sF4,relname(X0,X1),sF4) ).
cnf(u11020,negated_conjecture,
ifeq3(of(skc6,skc9,skc8),sF4,ifeq3(of(skc6,X0,skc8),sF4,ifeq3(placename(skc6,X0),sF4,skc9,X0),X0),X0) = X0 ).
cnf(u10947,negated_conjecture,
skc9 = ifeq3(of(skc6,X0,skc8),sF4,ifeq3(of(skc6,skc9,skc8),sF4,ifeq3(placename(skc6,X0),sF4,X0,skc9),skc9),skc9) ).
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(u10978,negated_conjecture,
skc9 = ifeq3(of(skc6,skc9,X0),sF4,ifeq3(of(skc6,skc9,X0),sF4,ifeq3(entity(skc6,X0),sF4,skc9,skc9),skc9),skc9) ).
cnf(u23,axiom,
true = ifeq2(artifact(X0,X1),true,object(X0,X1),true) ).
cnf(u67,axiom,
true = ifeq2(instrumentality(X0,X1),true,artifact(X0,X1),true) ).
cnf(u7563,negated_conjecture,
sF4 = ifeq2(location(X0,X1),sF4,object(X0,X1),sF4) ).
cnf(u262,negated_conjecture,
true = ifeq2(object(X0,X1),true,nonliving(X0,X1),true) ).
cnf(u4174,negated_conjecture,
sF4 = ifeq2(artifact(X0,X1),sF4,object(X0,X1),sF4) ).
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(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
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(u3973,negated_conjecture,
sF4 = ifeq2(way(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u6654,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,general(X0,X1),sF4) ).
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(u5408,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u10749,negated_conjecture,
ifeq3(of(skc6,X0,skc11),sF4,ifeq3(of(skc6,X1,skc11),sF4,ifeq3(placename(skc6,X0),sF4,ifeq3(placename(skc6,X1),sF4,X0,X1),X1),X1),X1) = X1 ).
cnf(u65,axiom,
true = ifeq2(transport(X0,X1),true,instrumentality(X0,X1),true) ).
cnf(u6857,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u59,axiom,
true = ifeq2(chevy(X0,X1),true,car(X0,X1),true) ).
cnf(u6309,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u119,negated_conjecture,
true = sF3(X0,X1) ).
cnf(u1848,negated_conjecture,
sF4 = ifeq2(thing(X0,X1),sF4,singleton(X0,X1),sF4) ).
cnf(u9,axiom,
true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u2307,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,nonhuman(X0,X1),sF4) ).
cnf(u2668,negated_conjecture,
sF4 = ifeq2(event(X0,X1),sF4,eventuality(X0,X1),sF4) ).
cnf(u2154,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,impartial(X0,X1),sF4) ).
cnf(u7346,negated_conjecture,
sF4 = ifeq2(city(X0,X1),sF4,location(X0,X1),sF4) ).
cnf(u4965,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,specific(X0,X1),sF4) ).
cnf(u113,negated_conjecture,
true = sF1(X0,X1) ).
cnf(u13,axiom,
true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u2001,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,nonliving(X0,X1),sF4) ).
cnf(u5860,negated_conjecture,
sF4 = ifeq2(relname(X0,X1),sF4,relation(X0,X1),sF4) ).
cnf(u39,axiom,
true = ifeq2(placename(X0,X1),true,relname(X0,X1),true) ).
cnf(u57,axiom,
true = ifeq2(location(X0,X1),true,object(X0,X1),true) ).
cnf(u3313,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,nonexistent(X0,X1),sF4) ).
cnf(u10748,negated_conjecture,
ifeq3(of(skc6,X0,skc10),sF4,ifeq3(of(skc6,X1,skc10),sF4,ifeq3(placename(skc6,X0),sF4,ifeq3(placename(skc6,X1),sF4,X0,X1),X1),X1),X1) = X1 ).
cnf(u4471,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,entity(X0,X1),sF4) ).
cnf(u10209,negated_conjecture,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u5206,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,existent(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(u9116,negated_conjecture,
sF4 = ifeq2(instrumentality(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u63,axiom,
true = ifeq2(vehicle(X0,X1),true,transport(X0,X1),true) ).
cnf(u2873,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u11022,negated_conjecture,
ifeq3(of(skc6,skc9,skc11),sF4,ifeq3(of(skc6,X0,skc11),sF4,ifeq3(placename(skc6,X0),sF4,skc9,X0),X0),X0) = X0 ).
cnf(u61,axiom,
true = ifeq2(car(X0,X1),true,vehicle(X0,X1),true) ).
cnf(u10747,negated_conjecture,
ifeq3(of(skc6,X0,skc8),sF4,ifeq3(of(skc6,X1,skc8),sF4,ifeq3(placename(skc6,X0),sF4,ifeq3(placename(skc6,X1),sF4,X0,X1),X1),X1),X1) = X1 ).
cnf(u8707,negated_conjecture,
sF4 = ifeq2(vehicle(X0,X1),sF4,transport(X0,X1),sF4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP124-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n008.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 18:07:24 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 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.53/1.91 % (1507385)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.53/1.91 % (1507394)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2584093392:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.53/1.91 % (1507394)Refutation not found, incomplete strategy
% 5.53/1.91 % (1507394)------------------------------
% 5.53/1.91 % (1507394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.91 % (1507394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.91 % (1507394)CaDiCaL version: 2.1.3
% 5.53/1.91 % (1507394)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.91 % (1507394)Time elapsed: 0.012 s
% 5.53/1.91 % (1507394)Peak memory usage: 88 MB
% 5.53/1.91 % (1507394)Instructions burned: 34 (million)
% 5.53/1.91 % (1507390)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=764155851:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.53/1.91 % (1507392)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3756314231:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.53/1.91 % (1507391)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=3386781421:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.53/1.91 % (1507393)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2074523071:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.53/1.91 % (1507396)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1019742972:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.53/1.91 % (1507395)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3047780895:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.53/1.92 % (1507396)Refutation not found, incomplete strategy
% 5.53/1.92 % (1507396)------------------------------
% 5.53/1.92 % (1507396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.92 % (1507396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.92 % (1507396)CaDiCaL version: 2.1.3
% 5.53/1.92 % (1507396)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.92 % (1507396)Time elapsed: 0.016 s
% 5.53/1.92 % (1507396)Peak memory usage: 87 MB
% 5.53/1.92 % (1507396)Instructions burned: 27 (million)
% 5.53/1.92 % (1507393)Refutation not found, incomplete strategy
% 5.53/1.92 % (1507393)------------------------------
% 5.53/1.92 % (1507393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.92 % (1507393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.92 % (1507393)CaDiCaL version: 2.1.3
% 5.53/1.92 % (1507393)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.92 % (1507393)Time elapsed: 0.060 s
% 5.53/1.92 % (1507393)Peak memory usage: 87 MB
% 5.53/1.92 % (1507393)Instructions burned: 116 (million)
% 5.53/1.92 % (1507395)Refutation not found, incomplete strategy
% 5.53/1.92 % (1507395)------------------------------
% 5.53/1.92 % (1507395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.92 % (1507395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.92 % (1507395)CaDiCaL version: 2.1.3
% 5.53/1.92 % (1507395)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.92 % (1507395)Time elapsed: 0.061 s
% 5.53/1.92 % (1507395)Peak memory usage: 89 MB
% 5.53/1.92 % (1507395)Instructions burned: 105 (million)
% 5.53/1.92 % (1507394)------------------------------
% 5.53/1.92 % (1507394)------------------------------
% 5.53/1.92 % (1507396)------------------------------
% 5.53/1.92 % (1507396)------------------------------
% 5.53/1.92 % (1507404)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1200172129:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 5.53/1.92 % (1507393)------------------------------
% 5.53/1.92 % (1507393)------------------------------
% 5.53/1.92 % (1507395)------------------------------
% 5.53/1.92 % (1507395)------------------------------
% 5.53/1.92 % (1507405)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1399750555:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 5.53/1.92 % (1507407)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2383301679:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.53/1.92 % (1507408)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=1547286091: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.53/1.92 % (1507407)Instruction limit reached!
% 5.53/1.92 % (1507407)------------------------------
% 5.53/1.92 % (1507407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.92 % (1507407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.92 % (1507407)CaDiCaL version: 2.1.3
% 5.53/1.92 % (1507407)Termination reason: Instruction limit
% 5.53/1.92 % (1507407)Termination phase: Saturation
% 5.53/1.92 % (1507407)Time elapsed: 0.107 s
% 5.53/1.92 % (1507407)Peak memory usage: 92 MB
% 5.53/1.92 % (1507407)Instructions burned: 216 (million)
% 5.53/1.92 % (1507408)First to succeed.
% 5.53/1.92 % (1507408)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1507385"
% 5.53/1.92 % (1507391)Also succeeded, but the first one will report.
% 5.53/1.92 % (1507392)Also succeeded, but the first one will report.
% 5.53/1.92 % (1507404)Refutation not found, incomplete strategy
% 5.53/1.92 % (1507404)------------------------------
% 5.53/1.92 % (1507404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.92 % (1507404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.92 % (1507404)CaDiCaL version: 2.1.3
% 5.53/1.92 % (1507404)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.92 % (1507404)Time elapsed: 0.419 s
% 5.53/1.92 % (1507404)Peak memory usage: 129 MB
% 5.53/1.92 % (1507404)Instructions burned: 1022 (million)
% 5.53/1.92 % (1507412)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=2401867356:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 5.53/1.92 % (1507390)Refutation not found, incomplete strategy
% 5.53/1.92 % (1507390)------------------------------
% 5.53/1.92 % (1507390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.92 % (1507390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.92 % (1507390)CaDiCaL version: 2.1.3
% 5.53/1.92 % (1507390)Termination reason: Refutation not found, incomplete strategy
% 5.53/1.92 % (1507390)Time elapsed: 0.773 s
% 5.53/1.92 % (1507390)Peak memory usage: 130 MB
% 5.53/1.92 % (1507390)Instructions burned: 1155 (million)
% 5.53/1.92 % (1507404)------------------------------
% 5.53/1.92 % (1507404)------------------------------
% 5.53/1.92 % SZS status Satisfiable for theBenchmark
% 5.53/1.92 % SZS output start Saturation.
% See solution above
% 7.85/2.11 % SZS output start Definitions and Model Updates.
% 7.85/2.11 % SZS output end Definitions and Model Updates.
% 7.85/2.11 % (1507408)------------------------------
% 7.85/2.11 % (1507408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.85/2.11 % (1507408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.85/2.11 % (1507408)CaDiCaL version: 2.1.3
% 7.85/2.11 % (1507408)Termination reason: Satisfiable
% 7.85/2.11 % (1507408)Time elapsed: 0.112 s
% 7.85/2.11 % (1507408)Peak memory usage: 93 MB
% 7.85/2.11 % (1507408)Instructions burned: 204 (million)
% 7.85/2.11 % (1507408)------------------------------
% 7.85/2.11 % (1507408)------------------------------
% 7.85/2.11 % (1507385)Success in time 1.034 s
% 7.85/2.11 % Vampire exiting
%------------------------------------------------------------------------------