%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP126-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 : n012.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:30 PM UTC 2026
% Result : Satisfiable 3.96s 1.13s
% Output : Saturation 4.44s
% 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,
street(skc5,skc9) = sF5 ).
cnf(u278,axiom,
placename(skc5,skc8) = sF6 ).
cnf(u283,axiom,
hollywood_placename(skc5,skc8) = sF7 ).
cnf(u288,axiom,
city(skc5,skc7) = sF8 ).
cnf(u293,axiom,
chevy(skc5,skc7) = sF9 ).
cnf(u298,axiom,
white(skc5,skc7) = sF10 ).
cnf(u303,axiom,
dirty(skc5,skc7) = sF11 ).
cnf(u308,axiom,
old(skc5,skc7) = sF12 ).
cnf(u313,axiom,
lonely(skc5,skc9) = sF13 ).
cnf(u318,axiom,
barrel(skc5,skc6) = sF14 ).
cnf(u323,axiom,
present(skc5,skc6) = sF15 ).
cnf(u328,axiom,
event(skc5,skc6) = sF16 ).
cnf(u333,axiom,
of(skc5,skc8,skc7) = sF17 ).
cnf(u338,axiom,
agent(skc5,skc6,skc7) = sF18 ).
cnf(u343,axiom,
in(skc5,skc6,skc7) = sF19 ).
cnf(u348,axiom,
down(skc5,skc6,skc9) = 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(u2825,negated_conjecture,
sF4 = eventuality(skc5,skc6) ).
cnf(u3033,negated_conjecture,
sF4 = thing(skc5,skc6) ).
cnf(u3045,negated_conjecture,
sF4 = singleton(skc5,skc6) ).
cnf(u3277,negated_conjecture,
sF4 = specific(skc5,skc6) ).
cnf(u3473,negated_conjecture,
sF4 = nonexistent(skc5,skc6) ).
cnf(u3707,negated_conjecture,
sF4 = unisex(skc5,skc6) ).
cnf(u3931,negated_conjecture,
sF4 = way(skc5,skc9) ).
cnf(u4133,negated_conjecture,
sF4 = artifact(skc5,skc9) ).
cnf(u4334,negated_conjecture,
sF4 = object(skc5,skc9) ).
cnf(u4351,negated_conjecture,
sF4 = nonliving(skc5,skc9) ).
cnf(u4356,negated_conjecture,
sF4 = impartial(skc5,skc9) ).
cnf(u4631,negated_conjecture,
sF4 = entity(skc5,skc9) ).
cnf(u4844,negated_conjecture,
sF4 = ifeq2(entity(skc5,skc6),sF4,sF4,sF4) ).
cnf(u4850,negated_conjecture,
sF4 = thing(skc5,skc9) ).
cnf(u4863,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc9),sF4,sF4,sF4) ).
cnf(u4870,negated_conjecture,
sF4 = singleton(skc5,skc9) ).
cnf(u5143,negated_conjecture,
sF4 = specific(skc5,skc9) ).
cnf(u5366,negated_conjecture,
sF4 = existent(skc5,skc9) ).
cnf(u5584,negated_conjecture,
sF4 = ifeq2(object(skc5,skc6),sF4,sF4,sF4) ).
cnf(u5590,negated_conjecture,
sF4 = unisex(skc5,skc9) ).
cnf(u5812,negated_conjecture,
sF4 = relname(skc5,skc8) ).
cnf(u6015,negated_conjecture,
sF4 = relation(skc5,skc8) ).
cnf(u6211,negated_conjecture,
sF4 = abstraction(skc5,skc8) ).
cnf(u6223,negated_conjecture,
sF4 = nonhuman(skc5,skc8) ).
cnf(u6497,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc9),sF4,sF4,sF4) ).
cnf(u6502,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc6),sF4,sF4,sF4) ).
cnf(u6508,negated_conjecture,
sF4 = thing(skc5,skc8) ).
cnf(u6520,negated_conjecture,
sF4 = ifeq2(entity(skc5,skc8),sF4,sF4,sF4) ).
cnf(u6525,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc8),sF4,sF4,sF4) ).
cnf(u6535,negated_conjecture,
sF4 = singleton(skc5,skc8) ).
cnf(u6809,negated_conjecture,
sF4 = general(skc5,skc8) ).
cnf(u7048,negated_conjecture,
sF4 = unisex(skc5,skc8) ).
cnf(u7110,negated_conjecture,
sF4 = ifeq2(object(skc5,skc8),sF4,sF4,sF4) ).
cnf(u7317,negated_conjecture,
placename(skc5,skc8) = sF4 ).
cnf(u7496,negated_conjecture,
sF4 = location(skc5,skc7) ).
cnf(u7721,negated_conjecture,
sF4 = ifeq2(location(skc5,skc9),sF4,sF4,sF4) ).
cnf(u7727,negated_conjecture,
sF4 = object(skc5,skc7) ).
cnf(u7745,negated_conjecture,
sF4 = ifeq2(artifact(skc5,skc7),sF4,sF4,sF4) ).
cnf(u7758,negated_conjecture,
sF4 = unisex(skc5,skc7) ).
cnf(u7763,negated_conjecture,
sF4 = entity(skc5,skc7) ).
cnf(u7768,negated_conjecture,
sF4 = impartial(skc5,skc7) ).
cnf(u7773,negated_conjecture,
sF4 = nonliving(skc5,skc7) ).
cnf(u7890,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc7),sF4,sF4,sF4) ).
cnf(u7948,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc7),sF4,sF4,sF4) ).
cnf(u7969,negated_conjecture,
sF4 = existent(skc5,skc7) ).
cnf(u7974,negated_conjecture,
sF4 = specific(skc5,skc7) ).
cnf(u7979,negated_conjecture,
sF4 = thing(skc5,skc7) ).
cnf(u8179,negated_conjecture,
sF4 = singleton(skc5,skc7) ).
cnf(u8425,negated_conjecture,
sF4 = car(skc5,skc7) ).
cnf(u8647,negated_conjecture,
sF4 = vehicle(skc5,skc7) ).
cnf(u8848,negated_conjecture,
sF4 = transport(skc5,skc7) ).
cnf(u9055,negated_conjecture,
sF4 = instrumentality(skc5,skc7) ).
cnf(u9273,negated_conjecture,
sF4 = ifeq2(instrumentality(skc5,skc9),sF4,sF4,sF4) ).
cnf(u9279,negated_conjecture,
sF4 = artifact(skc5,skc7) ).
cnf(u9292,negated_conjecture,
sF4 = ifeq2(way(skc5,skc7),sF4,sF4,sF4) ).
cnf(u9588,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc8),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9593,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc7)),tuple(sF4,sF4),a,b) ).
cnf(u9598,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc9)),tuple(sF4,sF4),a,b) ).
cnf(u9603,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc6)),tuple(sF4,sF4),a,b) ).
cnf(u9829,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc7),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9834,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc9),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9839,negated_conjecture,
b = ifeq(tuple(sF4,existent(skc5,skc6)),tuple(sF4,sF4),a,b) ).
cnf(u10447,negated_conjecture,
skc8 = ifeq3(of(skc5,skc8,skc9),sF4,ifeq3(of(skc5,skc8,skc9),sF4,skc8,skc8),skc8) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u5208,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,existent(X0,X1),sF4) ).
cnf(u9875,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(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(u7547,negated_conjecture,
sF4 = ifeq2(location(X0,X1),sF4,object(X0,X1),sF4) ).
cnf(u10267,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,skc9),sF4,ifeq3(of(skc5,skc8,skc9),sF4,ifeq3(placename(skc5,X0),sF4,X0,skc8),skc8),skc8) ).
cnf(u1848,negated_conjecture,
sF4 = ifeq2(thing(X0,X1),sF4,singleton(X0,X1),sF4) ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u264,negated_conjecture,
true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u25,axiom,
true = ifeq2(object(X0,X1),true,entity(X0,X1),true) ).
cnf(u106,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u10328,negated_conjecture,
ifeq3(of(skc5,skc8,skc9),sF4,ifeq3(of(skc5,X0,skc9),sF4,ifeq3(placename(skc5,X0),sF4,skc8,X0),X0),X0) = X0 ).
cnf(u10130,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,skc7),sF4,ifeq3(placename(skc5,X0),sF4,X0,skc8),skc8) ).
cnf(u116,negated_conjecture,
true = sF2(X0,X1) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u3975,negated_conjecture,
sF4 = ifeq2(way(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u10131,negated_conjecture,
ifeq3(of(skc5,X0,skc7),sF4,ifeq3(placename(skc5,X0),sF4,skc8,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(u2667,negated_conjecture,
sF4 = ifeq2(event(X0,X1),sF4,eventuality(X0,X1),sF4) ).
cnf(u5857,negated_conjecture,
sF4 = ifeq2(relname(X0,X1),sF4,relation(X0,X1),sF4) ).
cnf(u9380,negated_conjecture,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u2462,negated_conjecture,
sF4 = ifeq2(barrel(X0,X1),sF4,event(X0,X1),sF4) ).
cnf(u55,axiom,
true = ifeq2(city(X0,X1),true,location(X0,X1),true) ).
cnf(u8690,negated_conjecture,
sF4 = ifeq2(vehicle(X0,X1),sF4,transport(X0,X1),sF4) ).
cnf(u5,axiom,
true = ifeq2(barrel(X0,X1),true,event(X0,X1),true) ).
cnf(u2875,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,thing(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(u9099,negated_conjecture,
sF4 = ifeq2(instrumentality(X0,X1),sF4,artifact(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(u19,axiom,
true = ifeq2(street(X0,X1),true,way(X0,X1),true) ).
cnf(u4967,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,specific(X0,X1),sF4) ).
cnf(u4473,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,entity(X0,X1),sF4) ).
cnf(u8897,negated_conjecture,
sF4 = ifeq2(transport(X0,X1),sF4,instrumentality(X0,X1),sF4) ).
cnf(u5410,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,unisex(X0,X1),sF4) ).
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(u4176,negated_conjecture,
sF4 = ifeq2(artifact(X0,X1),sF4,object(X0,X1),sF4) ).
cnf(u5654,negated_conjecture,
sF4 = ifeq2(placename(X0,X1),sF4,relname(X0,X1),sF4) ).
cnf(u3549,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,unisex(X0,X1),sF4) ).
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(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(u6651,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,general(X0,X1),sF4) ).
cnf(u104,axiom,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).
cnf(u10116,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,X1),sF4,ifeq3(of(skc5,skc8,X1),sF4,ifeq3(placename(skc5,X0),sF4,ifeq3(entity(skc5,X1),sF4,X0,skc8),skc8),skc8),skc8) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u10276,negated_conjecture,
skc8 = ifeq3(of(skc5,skc8,X0),sF4,ifeq3(of(skc5,skc8,X0),sF4,ifeq3(entity(skc5,X0),sF4,skc8,skc8),skc8),skc8) ).
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(u8267,negated_conjecture,
sF4 = ifeq2(chevy(X0,X1),sF4,car(X0,X1),sF4) ).
cnf(u21,axiom,
true = ifeq2(way(X0,X1),true,artifact(X0,X1),true) ).
cnf(u10114,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(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(u3119,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,specific(X0,X1),sF4) ).
cnf(u263,negated_conjecture,
true = ifeq2(object(X0,X1),true,impartial(X0,X1),true) ).
cnf(u2307,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,nonhuman(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(u6053,negated_conjecture,
sF4 = ifeq2(relation(X0,X1),sF4,abstraction(X0,X1),sF4) ).
cnf(u4670,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u10115,negated_conjecture,
ifeq3(of(skc5,X0,skc9),sF4,ifeq3(of(skc5,X1,skc9),sF4,ifeq3(placename(skc5,X0),sF4,ifeq3(placename(skc5,X1),sF4,X0,X1),X1),X1),X1) = X1 ).
cnf(u7338,negated_conjecture,
sF4 = ifeq2(city(X0,X1),sF4,location(X0,X1),sF4) ).
cnf(u10117,negated_conjecture,
ifeq3(of(skc5,skc8,X0),sF4,ifeq3(of(skc5,X1,X0),sF4,ifeq3(placename(skc5,X1),sF4,ifeq3(entity(skc5,X0),sF4,skc8,X1),X1),X1),X1) = X1 ).
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(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(u3315,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,nonexistent(X0,X1),sF4) ).
cnf(u3773,negated_conjecture,
sF4 = ifeq2(street(X0,X1),sF4,way(X0,X1),sF4) ).
cnf(u6854,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,unisex(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(u8489,negated_conjecture,
sF4 = ifeq2(car(X0,X1),sF4,vehicle(X0,X1),sF4) ).
cnf(u63,axiom,
true = ifeq2(vehicle(X0,X1),true,transport(X0,X1),true) ).
cnf(u7140,negated_conjecture,
sF4 = ifeq2(hollywood_placename(X0,X1),sF4,placename(X0,X1),sF4) ).
cnf(u61,axiom,
true = ifeq2(car(X0,X1),true,vehicle(X0,X1),true) ).
cnf(u9638,negated_conjecture,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u6306,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,thing(X0,X1),sF4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NLP126-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 18:05:49 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.33 Running first-order theorem proving
% 0.08/0.33 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
% 3.96/1.13 % (2637481)Detected a unit-equality problem, will run specialized UEQ schedule.
% 3.96/1.13 % (2637489)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3972631415:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 3.96/1.13 % (2637488)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3111629217:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 3.96/1.13 % (2637487)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=576447658:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 3.96/1.13 % (2637490)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3986656299:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 3.96/1.13 % (2637486)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=2940758538:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 3.96/1.13 % (2637491)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1652839228:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 3.96/1.13 % (2637490)Refutation not found, incomplete strategy
% 3.96/1.13 % (2637490)------------------------------
% 3.96/1.13 % (2637490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.13 % (2637490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.13 % (2637490)CaDiCaL version: 2.1.3
% 3.96/1.13 % (2637490)Termination reason: Refutation not found, incomplete strategy
% 3.96/1.13 % (2637490)Time elapsed: 0.010 s
% 3.96/1.13 % (2637490)Peak memory usage: 88 MB
% 3.96/1.13 % (2637490)Instructions burned: 29 (million)
% 3.96/1.13 % (2637492)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1247896629:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 3.96/1.13 % (2637492)Refutation not found, incomplete strategy
% 3.96/1.13 % (2637492)------------------------------
% 3.96/1.13 % (2637492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.13 % (2637492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.13 % (2637492)CaDiCaL version: 2.1.3
% 3.96/1.13 % (2637492)Termination reason: Refutation not found, incomplete strategy
% 3.96/1.13 % (2637492)Time elapsed: 0.007 s
% 3.96/1.13 % (2637492)Peak memory usage: 87 MB
% 3.96/1.13 % (2637492)Instructions burned: 22 (million)
% 3.96/1.13 % (2637489)Refutation not found, incomplete strategy
% 3.96/1.13 % (2637489)------------------------------
% 3.96/1.13 % (2637489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.13 % (2637489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.13 % (2637489)CaDiCaL version: 2.1.3
% 3.96/1.13 % (2637489)Termination reason: Refutation not found, incomplete strategy
% 3.96/1.13 % (2637489)Time elapsed: 0.029 s
% 3.96/1.13 % (2637489)Peak memory usage: 88 MB
% 3.96/1.13 % (2637489)Instructions burned: 108 (million)
% 3.96/1.13 % (2637491)Refutation not found, incomplete strategy
% 3.96/1.13 % (2637491)------------------------------
% 3.96/1.13 % (2637491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.13 % (2637491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.13 % (2637491)CaDiCaL version: 2.1.3
% 3.96/1.13 % (2637491)Termination reason: Refutation not found, incomplete strategy
% 3.96/1.13 % (2637491)Time elapsed: 0.042 s
% 3.96/1.13 % (2637491)Peak memory usage: 89 MB
% 3.96/1.13 % (2637491)Instructions burned: 98 (million)
% 3.96/1.13 % (2637490)------------------------------
% 3.96/1.13 % (2637490)------------------------------
% 3.96/1.13 % (2637489)------------------------------
% 3.96/1.13 % (2637489)------------------------------
% 3.96/1.13 % (2637492)------------------------------
% 3.96/1.13 % (2637492)------------------------------
% 3.96/1.13 % (2637491)------------------------------
% 3.96/1.13 % (2637491)------------------------------
% 3.96/1.13 % (2637500)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=374657333:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 3.96/1.13 % (2637502)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=929548205:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 3.96/1.13 % (2637501)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2550643787:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 3.96/1.13 % (2637503)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=2065146138:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2997 on theBenchmark for (2997ds/317Mi)
% 3.96/1.13 % (2637502)Instruction limit reached!
% 3.96/1.13 % (2637502)------------------------------
% 3.96/1.13 % (2637502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.13 % (2637502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.13 % (2637502)CaDiCaL version: 2.1.3
% 3.96/1.13 % (2637502)Termination reason: Instruction limit
% 3.96/1.13 % (2637502)Termination phase: Saturation
% 3.96/1.13 % (2637502)Time elapsed: 0.059 s
% 3.96/1.13 % (2637502)Peak memory usage: 92 MB
% 3.96/1.13 % (2637502)Instructions burned: 219 (million)
% 3.96/1.13 % (2637503)First to succeed.
% 3.96/1.13 % (2637503)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2637481"
% 3.96/1.13 % (2637487)Also succeeded, but the first one will report.
% 3.96/1.13 % (2637488)Also succeeded, but the first one will report.
% 3.96/1.13 % (2637508)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=1275828438:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2995 on theBenchmark for (2995ds/12125Mi)
% 3.96/1.13 % (2637486)Refutation not found, incomplete strategy
% 3.96/1.13 % (2637486)------------------------------
% 3.96/1.13 % (2637486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.13 % (2637486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.13 % (2637486)CaDiCaL version: 2.1.3
% 3.96/1.13 % (2637486)Termination reason: Refutation not found, incomplete strategy
% 3.96/1.13 % (2637486)Time elapsed: 0.431 s
% 3.96/1.13 % (2637486)Peak memory usage: 130 MB
% 3.96/1.13 % (2637486)Instructions burned: 1136 (million)
% 3.96/1.13 % SZS status Satisfiable for theBenchmark
% 3.96/1.13 % SZS output start Saturation.
% See solution above
% 4.44/1.23 % SZS output start Definitions and Model Updates.
% 4.44/1.23 % SZS output end Definitions and Model Updates.
% 4.44/1.23 % (2637503)------------------------------
% 4.44/1.23 % (2637503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.23 % (2637503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.23 % (2637503)CaDiCaL version: 2.1.3
% 4.44/1.23 % (2637503)Termination reason: Satisfiable
% 4.44/1.23 % (2637503)Time elapsed: 0.057 s
% 4.44/1.23 % (2637503)Peak memory usage: 92 MB
% 4.44/1.23 % (2637503)Instructions burned: 188 (million)
% 4.44/1.23 % (2637503)------------------------------
% 4.44/1.23 % (2637503)------------------------------
% 4.44/1.23 % (2637481)Success in time 0.605 s
% 4.44/1.23 % Vampire exiting
%------------------------------------------------------------------------------