%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP125-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 : n011.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.33s 1.59s
% Output : Saturation 7.04s
% 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,
chevy(skc5,skc7) = sF7 ).
cnf(u288,axiom,
white(skc5,skc7) = sF8 ).
cnf(u293,axiom,
dirty(skc5,skc7) = sF9 ).
cnf(u298,axiom,
old(skc5,skc7) = sF10 ).
cnf(u303,axiom,
barrel(skc5,skc6) = sF11 ).
cnf(u308,axiom,
present(skc5,skc6) = sF12 ).
cnf(u313,axiom,
event(skc5,skc6) = sF13 ).
cnf(u318,axiom,
lonely(skc5,skc8) = sF14 ).
cnf(u323,axiom,
street(skc5,skc8) = sF15 ).
cnf(u328,axiom,
city(skc5,skc8) = sF16 ).
cnf(u333,axiom,
of(skc5,skc9,skc8) = sF17 ).
cnf(u338,axiom,
agent(skc5,skc6,skc7) = sF18 ).
cnf(u343,axiom,
in(skc5,skc6,skc8) = sF19 ).
cnf(u348,axiom,
down(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(u2822,negated_conjecture,
sF4 = eventuality(skc5,skc6) ).
cnf(u3027,negated_conjecture,
sF4 = thing(skc5,skc6) ).
cnf(u3039,negated_conjecture,
sF4 = singleton(skc5,skc6) ).
cnf(u3271,negated_conjecture,
sF4 = specific(skc5,skc6) ).
cnf(u3467,negated_conjecture,
sF4 = nonexistent(skc5,skc6) ).
cnf(u3692,negated_conjecture,
sF4 = unisex(skc5,skc6) ).
cnf(u3910,negated_conjecture,
sF4 = way(skc5,skc8) ).
cnf(u4122,negated_conjecture,
sF4 = artifact(skc5,skc8) ).
cnf(u4323,negated_conjecture,
sF4 = object(skc5,skc8) ).
cnf(u4340,negated_conjecture,
sF4 = nonliving(skc5,skc8) ).
cnf(u4345,negated_conjecture,
sF4 = impartial(skc5,skc8) ).
cnf(u4620,negated_conjecture,
sF4 = entity(skc5,skc8) ).
cnf(u4833,negated_conjecture,
sF4 = ifeq2(entity(skc5,skc6),sF4,sF4,sF4) ).
cnf(u4839,negated_conjecture,
sF4 = thing(skc5,skc8) ).
cnf(u4852,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc8),sF4,sF4,sF4) ).
cnf(u4859,negated_conjecture,
sF4 = singleton(skc5,skc8) ).
cnf(u5132,negated_conjecture,
sF4 = specific(skc5,skc8) ).
cnf(u5375,negated_conjecture,
sF4 = existent(skc5,skc8) ).
cnf(u5593,negated_conjecture,
sF4 = ifeq2(object(skc5,skc6),sF4,sF4,sF4) ).
cnf(u5599,negated_conjecture,
sF4 = unisex(skc5,skc8) ).
cnf(u5821,negated_conjecture,
sF4 = relname(skc5,skc9) ).
cnf(u6024,negated_conjecture,
sF4 = relation(skc5,skc9) ).
cnf(u6220,negated_conjecture,
sF4 = abstraction(skc5,skc9) ).
cnf(u6232,negated_conjecture,
sF4 = nonhuman(skc5,skc9) ).
cnf(u6506,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc8),sF4,sF4,sF4) ).
cnf(u6511,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc6),sF4,sF4,sF4) ).
cnf(u6517,negated_conjecture,
sF4 = thing(skc5,skc9) ).
cnf(u6529,negated_conjecture,
sF4 = ifeq2(entity(skc5,skc9),sF4,sF4,sF4) ).
cnf(u6534,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc9),sF4,sF4,sF4) ).
cnf(u6544,negated_conjecture,
sF4 = singleton(skc5,skc9) ).
cnf(u6818,negated_conjecture,
sF4 = general(skc5,skc9) ).
cnf(u7057,negated_conjecture,
sF4 = unisex(skc5,skc9) ).
cnf(u7119,negated_conjecture,
sF4 = ifeq2(object(skc5,skc9),sF4,sF4,sF4) ).
cnf(u7326,negated_conjecture,
placename(skc5,skc9) = sF4 ).
cnf(u7503,negated_conjecture,
sF4 = location(skc5,skc8) ).
cnf(u7916,negated_conjecture,
sF4 = car(skc5,skc7) ).
cnf(u8120,negated_conjecture,
sF4 = vehicle(skc5,skc7) ).
cnf(u8325,negated_conjecture,
sF4 = transport(skc5,skc7) ).
cnf(u8526,negated_conjecture,
sF4 = instrumentality(skc5,skc7) ).
cnf(u8748,negated_conjecture,
sF4 = ifeq2(instrumentality(skc5,skc8),sF4,sF4,sF4) ).
cnf(u8754,negated_conjecture,
sF4 = artifact(skc5,skc7) ).
cnf(u8766,negated_conjecture,
sF4 = ifeq2(way(skc5,skc7),sF4,sF4,sF4) ).
cnf(u8775,negated_conjecture,
sF4 = object(skc5,skc7) ).
cnf(u8852,negated_conjecture,
sF4 = unisex(skc5,skc7) ).
cnf(u8857,negated_conjecture,
sF4 = entity(skc5,skc7) ).
cnf(u8862,negated_conjecture,
sF4 = impartial(skc5,skc7) ).
cnf(u8867,negated_conjecture,
sF4 = nonliving(skc5,skc7) ).
cnf(u8970,negated_conjecture,
sF4 = ifeq2(location(skc5,skc7),sF4,sF4,sF4) ).
cnf(u8989,negated_conjecture,
sF4 = ifeq2(eventuality(skc5,skc7),sF4,sF4,sF4) ).
cnf(u8997,negated_conjecture,
sF4 = ifeq2(abstraction(skc5,skc7),sF4,sF4,sF4) ).
cnf(u9069,negated_conjecture,
sF4 = existent(skc5,skc7) ).
cnf(u9074,negated_conjecture,
sF4 = specific(skc5,skc7) ).
cnf(u9079,negated_conjecture,
sF4 = thing(skc5,skc7) ).
cnf(u9485,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc9),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9490,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc7)),tuple(sF4,sF4),a,b) ).
cnf(u9495,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc8)),tuple(sF4,sF4),a,b) ).
cnf(u9500,negated_conjecture,
b = ifeq(tuple(sF4,general(skc5,skc6)),tuple(sF4,sF4),a,b) ).
cnf(u9521,negated_conjecture,
sF4 = singleton(skc5,skc7) ).
cnf(u9832,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc7),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9837,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc8),sF4),tuple(sF4,sF4),a,b) ).
cnf(u9842,negated_conjecture,
b = ifeq(tuple(sF4,existent(skc5,skc6)),tuple(sF4,sF4),a,b) ).
cnf(u10461,negated_conjecture,
skc9 = ifeq3(of(skc5,skc9,skc7),sF4,ifeq3(of(skc5,skc9,skc7),sF4,skc9,skc9),skc9) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u7562,negated_conjecture,
sF4 = ifeq2(location(X0,X1),sF4,object(X0,X1),sF4) ).
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(u10150,negated_conjecture,
ifeq3(of(skc5,X0,skc8),sF4,ifeq3(placename(skc5,X0),sF4,skc9,X0),X0) = X0 ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u10149,negated_conjecture,
skc9 = ifeq3(of(skc5,X0,skc8),sF4,ifeq3(placename(skc5,X0),sF4,X0,skc9),skc9) ).
cnf(u25,axiom,
true = ifeq2(object(X0,X1),true,entity(X0,X1),true) ).
cnf(u5866,negated_conjecture,
sF4 = ifeq2(relname(X0,X1),sF4,relation(X0,X1),sF4) ).
cnf(u2869,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u116,negated_conjecture,
true = sF2(X0,X1) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u6062,negated_conjecture,
sF4 = ifeq2(relation(X0,X1),sF4,abstraction(X0,X1),sF4) ).
cnf(u7758,negated_conjecture,
sF4 = ifeq2(chevy(X0,X1),sF4,car(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(u55,axiom,
true = ifeq2(city(X0,X1),true,location(X0,X1),true) ).
cnf(u8368,negated_conjecture,
sF4 = ifeq2(transport(X0,X1),sF4,instrumentality(X0,X1),sF4) ).
cnf(u5419,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,unisex(X0,X1),sF4) ).
cnf(u5,axiom,
true = ifeq2(barrel(X0,X1),true,event(X0,X1),true) ).
cnf(u5217,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,existent(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(u6863,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,unisex(X0,X1),sF4) ).
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(u8574,negated_conjecture,
sF4 = ifeq2(instrumentality(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u10291,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(u10281,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(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(u10134,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(u67,axiom,
true = ifeq2(instrumentality(X0,X1),true,artifact(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(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u3964,negated_conjecture,
sF4 = ifeq2(way(X0,X1),sF4,artifact(X0,X1),sF4) ).
cnf(u10135,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(u2664,negated_conjecture,
sF4 = ifeq2(event(X0,X1),sF4,eventuality(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(u10136,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(u9641,negated_conjecture,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u10342,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(u3534,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,unisex(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(u4462,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,entity(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(u3309,negated_conjecture,
sF4 = ifeq2(eventuality(X0,X1),sF4,nonexistent(X0,X1),sF4) ).
cnf(u119,negated_conjecture,
true = sF3(X0,X1) ).
cnf(u7149,negated_conjecture,
sF4 = ifeq2(hollywood_placename(X0,X1),sF4,placename(X0,X1),sF4) ).
cnf(u1848,negated_conjecture,
sF4 = ifeq2(thing(X0,X1),sF4,singleton(X0,X1),sF4) ).
cnf(u263,negated_conjecture,
true = ifeq2(object(X0,X1),true,impartial(X0,X1),true) ).
cnf(u10133,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(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(u5663,negated_conjecture,
sF4 = ifeq2(placename(X0,X1),sF4,relname(X0,X1),sF4) ).
cnf(u2154,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,impartial(X0,X1),sF4) ).
cnf(u9894,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(u3113,negated_conjecture,
sF4 = ifeq2(eventuality(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(u6315,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u2001,negated_conjecture,
sF4 = ifeq2(object(X0,X1),sF4,nonliving(X0,X1),sF4) ).
cnf(u8167,negated_conjecture,
sF4 = ifeq2(vehicle(X0,X1),sF4,transport(X0,X1),sF4) ).
cnf(u39,axiom,
true = ifeq2(placename(X0,X1),true,relname(X0,X1),true) ).
cnf(u4659,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,thing(X0,X1),sF4) ).
cnf(u57,axiom,
true = ifeq2(location(X0,X1),true,object(X0,X1),true) ).
cnf(u4165,negated_conjecture,
sF4 = ifeq2(artifact(X0,X1),sF4,object(X0,X1),sF4) ).
cnf(u7962,negated_conjecture,
sF4 = ifeq2(car(X0,X1),sF4,vehicle(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(u4956,negated_conjecture,
sF4 = ifeq2(entity(X0,X1),sF4,specific(X0,X1),sF4) ).
cnf(u63,axiom,
true = ifeq2(vehicle(X0,X1),true,transport(X0,X1),true) ).
cnf(u9277,negated_conjecture,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(sF4,sF4),a,b) ).
cnf(u6660,negated_conjecture,
sF4 = ifeq2(abstraction(X0,X1),sF4,general(X0,X1),sF4) ).
cnf(u61,axiom,
true = ifeq2(car(X0,X1),true,vehicle(X0,X1),true) ).
cnf(u7345,negated_conjecture,
sF4 = ifeq2(city(X0,X1),sF4,location(X0,X1),sF4) ).
cnf(u262,negated_conjecture,
true = ifeq2(object(X0,X1),true,nonliving(X0,X1),true) ).
cnf(u3752,negated_conjecture,
sF4 = ifeq2(street(X0,X1),sF4,way(X0,X1),sF4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP125-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.11/0.39 % Computer : n011.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 18:06:30 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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.33/1.59 % (2663956)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.33/1.59 % (2663966)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3062791834:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.33/1.59 % (2663962)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=787284217:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.33/1.59 % (2663967)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=4187507014:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.33/1.59 % (2663963)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3045214504:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.33/1.59 % (2663964)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1581163596:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.33/1.59 % (2663965)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2633198374:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.33/1.59 % (2663961)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=3571270206:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.33/1.59 % (2663967)Refutation not found, incomplete strategy
% 5.33/1.59 % (2663967)------------------------------
% 5.33/1.59 % (2663967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.59 % (2663967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.59 % (2663967)CaDiCaL version: 2.1.3
% 5.33/1.59 % (2663967)Termination reason: Refutation not found, incomplete strategy
% 5.33/1.59 % (2663967)Time elapsed: 0.014 s
% 5.33/1.59 % (2663967)Peak memory usage: 87 MB
% 5.33/1.59 % (2663967)Instructions burned: 22 (million)
% 5.33/1.59 % (2663965)Refutation not found, incomplete strategy
% 5.33/1.59 % (2663965)------------------------------
% 5.33/1.59 % (2663965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.59 % (2663965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.59 % (2663965)CaDiCaL version: 2.1.3
% 5.33/1.59 % (2663965)Termination reason: Refutation not found, incomplete strategy
% 5.33/1.59 % (2663965)Time elapsed: 0.018 s
% 5.33/1.59 % (2663965)Peak memory usage: 88 MB
% 5.33/1.59 % (2663965)Instructions burned: 29 (million)
% 5.33/1.59 % (2663966)Refutation not found, incomplete strategy
% 5.33/1.59 % (2663966)------------------------------
% 5.33/1.59 % (2663966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.59 % (2663966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.59 % (2663966)CaDiCaL version: 2.1.3
% 5.33/1.59 % (2663966)Termination reason: Refutation not found, incomplete strategy
% 5.33/1.59 % (2663966)Time elapsed: 0.032 s
% 5.33/1.59 % (2663966)Peak memory usage: 89 MB
% 5.33/1.59 % (2663966)Instructions burned: 103 (million)
% 5.33/1.59 % (2663964)Refutation not found, incomplete strategy
% 5.33/1.59 % (2663964)------------------------------
% 5.33/1.59 % (2663964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.59 % (2663964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.59 % (2663964)CaDiCaL version: 2.1.3
% 5.33/1.59 % (2663964)Termination reason: Refutation not found, incomplete strategy
% 5.33/1.59 % (2663964)Time elapsed: 0.056 s
% 5.33/1.59 % (2663964)Peak memory usage: 88 MB
% 5.33/1.59 % (2663964)Instructions burned: 109 (million)
% 5.33/1.59 % (2663966)------------------------------
% 5.33/1.59 % (2663966)------------------------------
% 5.33/1.59 % (2663967)------------------------------
% 5.33/1.59 % (2663967)------------------------------
% 5.33/1.59 % (2663965)------------------------------
% 5.33/1.59 % (2663965)------------------------------
% 5.33/1.59 % (2663964)------------------------------
% 5.33/1.59 % (2663964)------------------------------
% 5.33/1.59 % (2663975)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=17136922:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 5.33/1.59 % (2663976)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=665247171:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 5.33/1.59 % (2663977)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1054597472:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.33/1.59 % (2663978)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=1537176211: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.33/1.59 % (2663977)Instruction limit reached!
% 5.33/1.59 % (2663977)------------------------------
% 5.33/1.59 % (2663977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.59 % (2663977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.59 % (2663977)CaDiCaL version: 2.1.3
% 5.33/1.59 % (2663977)Termination reason: Instruction limit
% 5.33/1.59 % (2663977)Termination phase: Saturation
% 5.33/1.59 % (2663977)Time elapsed: 0.108 s
% 5.33/1.59 % (2663977)Peak memory usage: 92 MB
% 5.33/1.59 % (2663977)Instructions burned: 217 (million)
% 5.33/1.59 % (2663978)First to succeed.
% 5.33/1.59 % (2663978)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2663956"
% 5.33/1.59 % (2663963)Also succeeded, but the first one will report.
% 5.33/1.59 % (2663962)Also succeeded, but the first one will report.
% 5.33/1.59 % (2663983)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=3459649404:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/12125Mi)
% 5.33/1.59 % (2663961)Refutation not found, incomplete strategy
% 5.33/1.59 % (2663961)------------------------------
% 5.33/1.59 % (2663961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.59 % (2663961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.59 % (2663961)CaDiCaL version: 2.1.3
% 5.33/1.59 % (2663961)Termination reason: Refutation not found, incomplete strategy
% 5.33/1.59 % (2663961)Time elapsed: 0.756 s
% 5.33/1.59 % (2663961)Peak memory usage: 130 MB
% 5.33/1.59 % (2663961)Instructions burned: 1138 (million)
% 5.33/1.59 % (2663976)Also succeeded, but the first one will report.
% 5.33/1.59 % SZS status Satisfiable for theBenchmark
% 5.33/1.59 % SZS output start Saturation.
% See solution above
% 7.04/1.69 % SZS output start Definitions and Model Updates.
% 7.04/1.69 % SZS output end Definitions and Model Updates.
% 7.04/1.69 % (2663978)------------------------------
% 7.04/1.69 % (2663978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/1.69 % (2663978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/1.69 % (2663978)CaDiCaL version: 2.1.3
% 7.04/1.69 % (2663978)Termination reason: Satisfiable
% 7.04/1.69 % (2663978)Time elapsed: 0.103 s
% 7.04/1.69 % (2663978)Peak memory usage: 92 MB
% 7.04/1.69 % (2663978)Instructions burned: 187 (million)
% 7.04/1.69 % (2663978)------------------------------
% 7.04/1.69 % (2663978)------------------------------
% 7.04/1.69 % (2663956)Success in time 0.967 s
% 7.04/1.69 % Vampire exiting
%------------------------------------------------------------------------------