%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP042-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:07 PM UTC 2026
% Result : Satisfiable 5.26s 1.88s
% Output : Saturation 7.73s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u166,negated_conjecture,
a != b ).
cnf(u171,negated_conjecture,
true = sF12 ).
cnf(u176,negated_conjecture,
true = sF11 ).
cnf(u181,negated_conjecture,
true = sF10 ).
cnf(u186,negated_conjecture,
true = sF9 ).
cnf(u191,negated_conjecture,
true = sF8 ).
cnf(u196,negated_conjecture,
true = sF7 ).
cnf(u201,negated_conjecture,
true = sF6 ).
cnf(u206,negated_conjecture,
true = sF5 ).
cnf(u211,negated_conjecture,
true = sF4 ).
cnf(u216,negated_conjecture,
true = sF3 ).
cnf(u221,negated_conjecture,
true = sF2 ).
cnf(u226,negated_conjecture,
true = sF1 ).
cnf(u232,axiom,
actual_world(skc5) = sF1 ).
cnf(u237,axiom,
woman(skc5,skc9) = sF2 ).
cnf(u242,axiom,
shake_beverage(skc5,skc7) = sF3 ).
cnf(u247,axiom,
order(skc5,skc6) = sF4 ).
cnf(u252,axiom,
nonreflexive(skc5,skc6) = sF5 ).
cnf(u257,axiom,
past(skc5,skc6) = sF6 ).
cnf(u262,axiom,
event(skc5,skc6) = sF7 ).
cnf(u267,axiom,
forename(skc5,skc8) = sF8 ).
cnf(u272,axiom,
mia_forename(skc5,skc8) = sF9 ).
cnf(u277,axiom,
of(skc5,skc8,skc9) = sF10 ).
cnf(u282,axiom,
agent(skc5,skc6,skc9) = sF11 ).
cnf(u287,axiom,
patient(skc5,skc6,skc7) = sF12 ).
cnf(u292,axiom,
tuple(true,true,true) = sF14 ).
cnf(u299,negated_conjecture,
sF14 = tuple(sF12,sF12,sF12) ).
cnf(u306,negated_conjecture,
sF11 = sF12 ).
cnf(u315,negated_conjecture,
sF10 = sF12 ).
cnf(u320,negated_conjecture,
sF10 = sF11 ).
cnf(u331,negated_conjecture,
sF9 = sF12 ).
cnf(u336,negated_conjecture,
sF9 = sF11 ).
cnf(u341,negated_conjecture,
sF9 = sF10 ).
cnf(u354,negated_conjecture,
sF8 = sF12 ).
cnf(u359,negated_conjecture,
sF8 = sF11 ).
cnf(u364,negated_conjecture,
sF8 = sF10 ).
cnf(u369,negated_conjecture,
sF8 = sF9 ).
cnf(u384,negated_conjecture,
sF7 = sF12 ).
cnf(u389,negated_conjecture,
sF7 = sF11 ).
cnf(u394,negated_conjecture,
sF7 = sF10 ).
cnf(u399,negated_conjecture,
sF7 = sF9 ).
cnf(u404,negated_conjecture,
sF7 = sF8 ).
cnf(u421,negated_conjecture,
sF6 = sF7 ).
cnf(u426,negated_conjecture,
sF6 = sF8 ).
cnf(u431,negated_conjecture,
sF6 = sF9 ).
cnf(u436,negated_conjecture,
sF6 = sF10 ).
cnf(u441,negated_conjecture,
sF6 = sF11 ).
cnf(u446,negated_conjecture,
sF6 = sF12 ).
cnf(u465,negated_conjecture,
sF5 = sF6 ).
cnf(u470,negated_conjecture,
sF5 = sF7 ).
cnf(u475,negated_conjecture,
sF5 = sF8 ).
cnf(u480,negated_conjecture,
sF5 = sF9 ).
cnf(u485,negated_conjecture,
sF5 = sF10 ).
cnf(u490,negated_conjecture,
sF5 = sF11 ).
cnf(u495,negated_conjecture,
sF5 = sF12 ).
cnf(u516,negated_conjecture,
sF4 = sF5 ).
cnf(u521,negated_conjecture,
sF4 = sF6 ).
cnf(u526,negated_conjecture,
sF4 = sF7 ).
cnf(u531,negated_conjecture,
sF4 = sF8 ).
cnf(u536,negated_conjecture,
sF4 = sF9 ).
cnf(u541,negated_conjecture,
sF4 = sF10 ).
cnf(u546,negated_conjecture,
sF4 = sF11 ).
cnf(u551,negated_conjecture,
sF4 = sF12 ).
cnf(u574,negated_conjecture,
sF3 = sF4 ).
cnf(u579,negated_conjecture,
sF3 = sF5 ).
cnf(u584,negated_conjecture,
sF3 = sF6 ).
cnf(u589,negated_conjecture,
sF3 = sF7 ).
cnf(u594,negated_conjecture,
sF3 = sF8 ).
cnf(u599,negated_conjecture,
sF3 = sF9 ).
cnf(u604,negated_conjecture,
sF3 = sF10 ).
cnf(u609,negated_conjecture,
sF3 = sF11 ).
cnf(u614,negated_conjecture,
sF3 = sF12 ).
cnf(u639,negated_conjecture,
sF2 = sF3 ).
cnf(u644,negated_conjecture,
sF2 = sF4 ).
cnf(u649,negated_conjecture,
sF2 = sF5 ).
cnf(u654,negated_conjecture,
sF2 = sF6 ).
cnf(u659,negated_conjecture,
sF2 = sF7 ).
cnf(u664,negated_conjecture,
sF2 = sF8 ).
cnf(u669,negated_conjecture,
sF2 = sF9 ).
cnf(u674,negated_conjecture,
sF2 = sF10 ).
cnf(u679,negated_conjecture,
sF2 = sF11 ).
cnf(u684,negated_conjecture,
sF2 = sF12 ).
cnf(u711,negated_conjecture,
sF1 = sF2 ).
cnf(u716,negated_conjecture,
sF1 = sF3 ).
cnf(u721,negated_conjecture,
sF1 = sF4 ).
cnf(u726,negated_conjecture,
sF1 = sF5 ).
cnf(u731,negated_conjecture,
sF1 = sF6 ).
cnf(u736,negated_conjecture,
sF1 = sF7 ).
cnf(u741,negated_conjecture,
sF1 = sF8 ).
cnf(u746,negated_conjecture,
sF1 = sF9 ).
cnf(u751,negated_conjecture,
sF1 = sF10 ).
cnf(u756,negated_conjecture,
sF1 = sF11 ).
cnf(u761,negated_conjecture,
sF1 = sF12 ).
cnf(u777,negated_conjecture,
sF14 = tuple(sF1,sF1,sF1) ).
cnf(u1320,negated_conjecture,
sF1 = act(skc5,skc6) ).
cnf(u1458,negated_conjecture,
event(skc5,skc6) = sF1 ).
cnf(u1566,negated_conjecture,
sF1 = eventuality(skc5,skc6) ).
cnf(u1699,negated_conjecture,
sF1 = thing(skc5,skc6) ).
cnf(u1711,negated_conjecture,
sF1 = singleton(skc5,skc6) ).
cnf(u1853,negated_conjecture,
sF1 = specific(skc5,skc6) ).
cnf(u1969,negated_conjecture,
sF1 = nonexistent(skc5,skc6) ).
cnf(u2080,negated_conjecture,
sF1 = unisex(skc5,skc6) ).
cnf(u2330,negated_conjecture,
sF1 = beverage(skc5,skc7) ).
cnf(u2451,negated_conjecture,
sF1 = food(skc5,skc7) ).
cnf(u2567,negated_conjecture,
sF1 = substance_matter(skc5,skc7) ).
cnf(u2683,negated_conjecture,
sF1 = object(skc5,skc7) ).
cnf(u2799,negated_conjecture,
sF1 = entity(skc5,skc7) ).
cnf(u2927,negated_conjecture,
sF1 = ifeq3(entity(skc5,skc6),sF1,sF1,sF1) ).
cnf(u2933,negated_conjecture,
sF1 = thing(skc5,skc7) ).
cnf(u2946,negated_conjecture,
sF1 = ifeq3(eventuality(skc5,skc7),sF1,sF1,sF1) ).
cnf(u2953,negated_conjecture,
sF1 = singleton(skc5,skc7) ).
cnf(u3123,negated_conjecture,
sF1 = specific(skc5,skc7) ).
cnf(u3257,negated_conjecture,
sF1 = existent(skc5,skc7) ).
cnf(u3373,negated_conjecture,
sF1 = nonliving(skc5,skc7) ).
cnf(u3489,negated_conjecture,
sF1 = impartial(skc5,skc7) ).
cnf(u3598,negated_conjecture,
sF1 = ifeq3(object(skc5,skc6),sF1,sF1,sF1) ).
cnf(u3604,negated_conjecture,
sF1 = unisex(skc5,skc7) ).
cnf(u3757,negated_conjecture,
sF1 = relname(skc5,skc8) ).
cnf(u3893,negated_conjecture,
sF1 = relation(skc5,skc8) ).
cnf(u4009,negated_conjecture,
sF1 = abstraction(skc5,skc8) ).
cnf(u4150,negated_conjecture,
sF1 = ifeq3(abstraction(skc5,skc7),sF1,sF1,sF1) ).
cnf(u4155,negated_conjecture,
sF1 = ifeq3(abstraction(skc5,skc6),sF1,sF1,sF1) ).
cnf(u4161,negated_conjecture,
sF1 = thing(skc5,skc8) ).
cnf(u4173,negated_conjecture,
sF1 = ifeq3(entity(skc5,skc8),sF1,sF1,sF1) ).
cnf(u4178,negated_conjecture,
sF1 = ifeq3(eventuality(skc5,skc8),sF1,sF1,sF1) ).
cnf(u4188,negated_conjecture,
sF1 = singleton(skc5,skc8) ).
cnf(u4359,negated_conjecture,
sF1 = nonhuman(skc5,skc8) ).
cnf(u4475,negated_conjecture,
sF1 = general(skc5,skc8) ).
cnf(u4619,negated_conjecture,
sF1 = unisex(skc5,skc8) ).
cnf(u4738,negated_conjecture,
forename(skc5,skc8) = sF1 ).
cnf(u4759,negated_conjecture,
sF1 = ifeq3(object(skc5,skc8),sF1,sF1,sF1) ).
cnf(u4928,negated_conjecture,
sF1 = human_person(skc5,skc9) ).
cnf(u5046,negated_conjecture,
sF1 = organism(skc5,skc9) ).
cnf(u5174,negated_conjecture,
sF1 = ifeq3(organism(skc5,skc7),sF1,sF1,sF1) ).
cnf(u5180,negated_conjecture,
sF1 = entity(skc5,skc9) ).
cnf(u5197,negated_conjecture,
sF1 = ifeq3(object(skc5,skc9),sF1,sF1,sF1) ).
cnf(u5207,negated_conjecture,
sF1 = existent(skc5,skc9) ).
cnf(u5212,negated_conjecture,
sF1 = specific(skc5,skc9) ).
cnf(u5217,negated_conjecture,
sF1 = thing(skc5,skc9) ).
cnf(u5306,negated_conjecture,
sF1 = ifeq3(eventuality(skc5,skc9),sF1,sF1,sF1) ).
cnf(u5345,negated_conjecture,
sF1 = ifeq3(abstraction(skc5,skc9),sF1,sF1,sF1) ).
cnf(u5357,negated_conjecture,
sF1 = singleton(skc5,skc9) ).
cnf(u5540,negated_conjecture,
sF1 = impartial(skc5,skc9) ).
cnf(u5674,negated_conjecture,
sF1 = living(skc5,skc9) ).
cnf(u5790,negated_conjecture,
sF1 = human(skc5,skc9) ).
cnf(u5906,negated_conjecture,
sF1 = animate(skc5,skc9) ).
cnf(u6022,negated_conjecture,
sF1 = female(skc5,skc9) ).
cnf(u6178,negated_conjecture,
b = ifeq2(tuple2(unisex(skc5,skc9),sF1),tuple2(sF1,sF1),a,b) ).
cnf(u6183,negated_conjecture,
b = ifeq2(tuple2(sF1,female(skc5,skc8)),tuple2(sF1,sF1),a,b) ).
cnf(u6188,negated_conjecture,
b = ifeq2(tuple2(sF1,female(skc5,skc7)),tuple2(sF1,sF1),a,b) ).
cnf(u6193,negated_conjecture,
b = ifeq2(tuple2(sF1,female(skc5,skc6)),tuple2(sF1,sF1),a,b) ).
cnf(u6336,negated_conjecture,
b = ifeq2(tuple2(specific(skc5,skc8),sF1),tuple2(sF1,sF1),a,b) ).
cnf(u6341,negated_conjecture,
b = ifeq2(tuple2(sF1,general(skc5,skc9)),tuple2(sF1,sF1),a,b) ).
cnf(u6346,negated_conjecture,
b = ifeq2(tuple2(sF1,general(skc5,skc7)),tuple2(sF1,sF1),a,b) ).
cnf(u6351,negated_conjecture,
b = ifeq2(tuple2(sF1,general(skc5,skc6)),tuple2(sF1,sF1),a,b) ).
cnf(u6468,negated_conjecture,
b = ifeq2(tuple2(nonliving(skc5,skc9),sF1),tuple2(sF1,sF1),a,b) ).
cnf(u6473,negated_conjecture,
b = ifeq2(tuple2(sF1,living(skc5,skc7)),tuple2(sF1,sF1),a,b) ).
cnf(u6586,negated_conjecture,
b = ifeq2(tuple2(nonhuman(skc5,skc9),sF1),tuple2(sF1,sF1),a,b) ).
cnf(u6591,negated_conjecture,
b = ifeq2(tuple2(sF1,human(skc5,skc8)),tuple2(sF1,sF1),a,b) ).
cnf(u6717,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc5,skc9),sF1),tuple2(sF1,sF1),a,b) ).
cnf(u6722,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc5,skc7),sF1),tuple2(sF1,sF1),a,b) ).
cnf(u6727,negated_conjecture,
b = ifeq2(tuple2(sF1,existent(skc5,skc6)),tuple2(sF1,sF1),a,b) ).
cnf(u6843,negated_conjecture,
b = ifeq2(tuple2(sF1,animate(skc5,skc7)),tuple2(sF1,sF1),a,b) ).
cnf(u6889,negated_conjecture,
sF13(skc5,skc6,skc9) = tuple(patient(skc5,skc6,skc9),sF1,sF1) ).
cnf(u6895,negated_conjecture,
sF13(skc5,skc6,skc7) = tuple(sF1,sF1,agent(skc5,skc6,skc7)) ).
cnf(u7374,negated_conjecture,
skc8 = ifeq4(of(skc5,skc8,skc7),sF1,ifeq4(of(skc5,skc8,skc7),sF1,skc8,skc8),skc8) ).
cnf(u228,negated_conjecture,
true = ifeq3(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(ifeq_axiom_002,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u3810,negated_conjecture,
sF1 = ifeq3(relname(X0,X1),sF1,relation(X0,X1),sF1) ).
cnf(u1616,negated_conjecture,
sF1 = ifeq3(eventuality(X0,X1),sF1,thing(X0,X1),sF1) ).
cnf(u22,axiom,
true = ifeq3(order(X0,X1),true,event(X0,X1),true) ).
cnf(u3290,negated_conjecture,
sF1 = ifeq3(object(X0,X1),sF1,nonliving(X0,X1),sF1) ).
cnf(u66,axiom,
true = ifeq3(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u6937,negated_conjecture,
ifeq4(of(X0,X1,X2),sF1,ifeq4(of(X0,X3,X2),sF1,ifeq4(forename(X0,X1),sF1,ifeq4(forename(X0,X3),sF1,ifeq4(entity(X0,X2),sF1,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u40,axiom,
true = ifeq3(object(X0,X1),true,nonliving(X0,X1),true) ).
cnf(u2247,negated_conjecture,
sF1 = ifeq3(shake_beverage(X0,X1),sF1,beverage(X0,X1),sF1) ).
cnf(u4276,negated_conjecture,
sF1 = ifeq3(abstraction(X0,X1),sF1,nonhuman(X0,X1),sF1) ).
cnf(u7186,negated_conjecture,
skc8 = ifeq4(of(skc5,X0,skc7),sF1,ifeq4(of(skc5,skc8,skc7),sF1,ifeq4(forename(skc5,X0),sF1,X0,skc8),skc8),skc8) ).
cnf(u5080,negated_conjecture,
sF1 = ifeq3(organism(X0,X1),sF1,entity(X0,X1),sF1) ).
cnf(u6374,negated_conjecture,
b = ifeq2(tuple2(nonliving(X0,X1),living(X0,X1)),tuple2(sF1,sF1),a,b) ).
cnf(u1997,negated_conjecture,
sF1 = ifeq3(eventuality(X0,X1),sF1,unisex(X0,X1),sF1) ).
cnf(u10,axiom,
true = ifeq3(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u70,axiom,
true = ifeq3(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u2119,negated_conjecture,
sF1 = ifeq3(order(X0,X1),sF1,event(X0,X1),sF1) ).
cnf(u4845,negated_conjecture,
sF1 = ifeq3(woman(X0,X1),sF1,human_person(X0,X1),sF1) ).
cnf(u44,axiom,
true = ifeq3(object(X0,X1),true,unisex(X0,X1),true) ).
cnf(u107,axiom,
b = ifeq2(tuple2(nonliving(X0,X1),living(X0,X1)),tuple2(true,true),a,b) ).
cnf(u7102,negated_conjecture,
skc8 = ifeq4(of(skc5,X0,skc9),sF1,ifeq4(forename(skc5,X0),sF1,X0,skc8),skc8) ).
cnf(u4963,negated_conjecture,
sF1 = ifeq3(human_person(X0,X1),sF1,organism(X0,X1),sF1) ).
cnf(ifeq_axiom,axiom,
ifeq4(X0,X0,X1,X2) = X1 ).
cnf(u6748,negated_conjecture,
b = ifeq2(tuple2(nonliving(X0,X1),animate(X0,X1)),tuple2(sF1,sF1),a,b) ).
cnf(u7215,negated_conjecture,
skc8 = ifeq4(of(skc5,skc8,X0),sF1,ifeq4(of(skc5,skc8,X0),sF1,ifeq4(entity(skc5,X0),sF1,skc8,skc8),skc8),skc8) ).
cnf(u32,axiom,
true = ifeq3(object(X0,X1),true,entity(X0,X1),true) ).
cnf(u3027,negated_conjecture,
sF1 = ifeq3(entity(X0,X1),sF1,specific(X0,X1),sF1) ).
cnf(u5707,negated_conjecture,
sF1 = ifeq3(human_person(X0,X1),sF1,human(X0,X1),sF1) ).
cnf(u58,axiom,
true = ifeq3(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u294,negated_conjecture,
b = ifeq(sF13(X0,X1,X2),sF14,a,b) ).
cnf(u162,negated_conjecture,
b = sF15(X0,X1,X2) ).
cnf(u1770,negated_conjecture,
sF1 = ifeq3(eventuality(X0,X1),sF1,specific(X0,X1),sF1) ).
cnf(clause44,axiom,
ifeq4(of(X0,X1,X2),true,ifeq4(of(X0,X3,X2),true,ifeq4(forename(X0,X1),true,ifeq4(forename(X0,X3),true,ifeq4(entity(X0,X2),true,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u8,axiom,
true = ifeq3(act(X0,X1),true,event(X0,X1),true) ).
cnf(u36,axiom,
true = ifeq3(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u68,axiom,
true = ifeq3(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u6862,negated_conjecture,
sF13(skc5,skc6,X0) = tuple(patient(skc5,skc6,X0),sF1,agent(skc5,skc6,X0)) ).
cnf(u103,axiom,
b = ifeq2(tuple2(unisex(X0,X1),female(X0,X1)),tuple2(true,true),a,b) ).
cnf(u34,axiom,
true = ifeq3(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u62,axiom,
true = ifeq3(woman(X0,X1),true,human_person(X0,X1),true) ).
cnf(u56,axiom,
true = ifeq3(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u2600,negated_conjecture,
sF1 = ifeq3(substance_matter(X0,X1),sF1,object(X0,X1),sF1) ).
cnf(u2484,negated_conjecture,
sF1 = ifeq3(food(X0,X1),sF1,substance_matter(X0,X1),sF1) ).
cnf(u4044,negated_conjecture,
sF1 = ifeq3(abstraction(X0,X1),sF1,thing(X0,X1),sF1) ).
cnf(u3926,negated_conjecture,
sF1 = ifeq3(relation(X0,X1),sF1,abstraction(X0,X1),sF1) ).
cnf(u6492,negated_conjecture,
b = ifeq2(tuple2(nonhuman(X0,X1),human(X0,X1)),tuple2(sF1,sF1),a,b) ).
cnf(u6060,negated_conjecture,
b = ifeq2(tuple2(unisex(X0,X1),female(X0,X1)),tuple2(sF1,sF1),a,b) ).
cnf(u12,axiom,
true = ifeq3(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u7245,negated_conjecture,
ifeq4(of(skc5,skc8,skc7),sF1,ifeq4(of(skc5,X0,skc7),sF1,ifeq4(forename(skc5,X0),sF1,skc8,X0),X0),X0) = X0 ).
cnf(u1483,negated_conjecture,
sF1 = ifeq3(event(X0,X1),sF1,eventuality(X0,X1),sF1) ).
cnf(u3674,negated_conjecture,
sF1 = ifeq3(forename(X0,X1),sF1,relname(X0,X1),sF1) ).
cnf(u38,axiom,
true = ifeq3(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u7103,negated_conjecture,
ifeq4(of(skc5,X0,skc9),sF1,ifeq4(forename(skc5,X0),sF1,skc8,X0),X0) = X0 ).
cnf(u30,axiom,
true = ifeq3(substance_matter(X0,X1),true,object(X0,X1),true) ).
cnf(u119,negated_conjecture,
true = sF0(X0,X1) ).
cnf(u26,axiom,
true = ifeq3(beverage(X0,X1),true,food(X0,X1),true) ).
cnf(u1237,negated_conjecture,
sF1 = ifeq3(order(X0,X1),sF1,act(X0,X1),sF1) ).
cnf(u48,axiom,
true = ifeq3(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u7076,negated_conjecture,
ifeq4(of(skc5,X0,skc9),sF1,ifeq4(of(skc5,X1,skc9),sF1,ifeq4(forename(skc5,X0),sF1,ifeq4(forename(skc5,X1),sF1,X0,X1),X1),X1),X1) = X1 ).
cnf(u60,axiom,
true = ifeq3(mia_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u3504,negated_conjecture,
sF1 = ifeq3(object(X0,X1),sF1,unisex(X0,X1),sF1) ).
cnf(ifeq_axiom_003,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u2368,negated_conjecture,
sF1 = ifeq3(beverage(X0,X1),sF1,food(X0,X1),sF1) ).
cnf(ifeq_axiom_001,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u74,axiom,
true = ifeq3(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u5823,negated_conjecture,
sF1 = ifeq3(human_person(X0,X1),sF1,animate(X0,X1),sF1) ).
cnf(u2833,negated_conjecture,
sF1 = ifeq3(entity(X0,X1),sF1,thing(X0,X1),sF1) ).
cnf(u3174,negated_conjecture,
sF1 = ifeq3(entity(X0,X1),sF1,existent(X0,X1),sF1) ).
cnf(u5444,negated_conjecture,
sF1 = ifeq3(organism(X0,X1),sF1,impartial(X0,X1),sF1) ).
cnf(u5591,negated_conjecture,
sF1 = ifeq3(organism(X0,X1),sF1,living(X0,X1),sF1) ).
cnf(u72,axiom,
true = ifeq3(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u6,axiom,
true = ifeq3(order(X0,X1),true,act(X0,X1),true) ).
cnf(u7079,negated_conjecture,
ifeq4(of(skc5,skc8,X0),sF1,ifeq4(of(skc5,X1,X0),sF1,ifeq4(forename(skc5,X1),sF1,ifeq4(entity(skc5,X0),sF1,skc8,X1),X1),X1),X1) = X1 ).
cnf(u3406,negated_conjecture,
sF1 = ifeq3(object(X0,X1),sF1,impartial(X0,X1),sF1) ).
cnf(u6611,negated_conjecture,
b = ifeq2(tuple2(nonexistent(X0,X1),existent(X0,X1)),tuple2(sF1,sF1),a,b) ).
cnf(u24,axiom,
true = ifeq3(shake_beverage(X0,X1),true,beverage(X0,X1),true) ).
cnf(u52,axiom,
true = ifeq3(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u50,axiom,
true = ifeq3(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u28,axiom,
true = ifeq3(food(X0,X1),true,substance_matter(X0,X1),true) ).
cnf(u1886,negated_conjecture,
sF1 = ifeq3(eventuality(X0,X1),sF1,nonexistent(X0,X1),sF1) ).
cnf(u4392,negated_conjecture,
sF1 = ifeq3(abstraction(X0,X1),sF1,general(X0,X1),sF1) ).
cnf(u7078,negated_conjecture,
skc8 = ifeq4(of(skc5,X0,X1),sF1,ifeq4(of(skc5,skc8,X1),sF1,ifeq4(forename(skc5,X0),sF1,ifeq4(entity(skc5,X1),sF1,X0,skc8),skc8),skc8),skc8) ).
cnf(u5939,negated_conjecture,
sF1 = ifeq3(woman(X0,X1),sF1,female(X0,X1),sF1) ).
cnf(u54,axiom,
true = ifeq3(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u4510,negated_conjecture,
sF1 = ifeq3(abstraction(X0,X1),sF1,unisex(X0,X1),sF1) ).
cnf(u113,axiom,
b = ifeq2(tuple2(nonliving(X0,X1),animate(X0,X1)),tuple2(true,true),a,b) ).
cnf(u2716,negated_conjecture,
sF1 = ifeq3(object(X0,X1),sF1,entity(X0,X1),sF1) ).
cnf(u157,axiom,
tuple(patient(X0,X1,X2),nonreflexive(X0,X1),agent(X0,X1,X2)) = sF13(X0,X1,X2) ).
cnf(u16,axiom,
true = ifeq3(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u109,axiom,
b = ifeq2(tuple2(nonhuman(X0,X1),human(X0,X1)),tuple2(true,true),a,b) ).
cnf(u7077,negated_conjecture,
ifeq4(of(skc5,X0,skc7),sF1,ifeq4(of(skc5,X1,skc7),sF1,ifeq4(forename(skc5,X0),sF1,ifeq4(forename(skc5,X1),sF1,X0,X1),X1),X1),X1) = X1 ).
cnf(u76,axiom,
true = ifeq3(woman(X0,X1),true,female(X0,X1),true) ).
cnf(u6218,negated_conjecture,
b = ifeq2(tuple2(specific(X0,X1),general(X0,X1)),tuple2(sF1,sF1),a,b) ).
cnf(u1158,negated_conjecture,
sF1 = ifeq3(thing(X0,X1),sF1,singleton(X0,X1),sF1) ).
cnf(u42,axiom,
true = ifeq3(object(X0,X1),true,impartial(X0,X1),true) ).
cnf(u20,axiom,
true = ifeq3(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u64,axiom,
true = ifeq3(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u111,axiom,
b = ifeq2(tuple2(nonexistent(X0,X1),existent(X0,X1)),tuple2(true,true),a,b) ).
cnf(u18,axiom,
true = ifeq3(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u46,axiom,
true = ifeq3(forename(X0,X1),true,relname(X0,X1),true) ).
cnf(u105,axiom,
b = ifeq2(tuple2(specific(X0,X1),general(X0,X1)),tuple2(true,true),a,b) ).
cnf(u1362,negated_conjecture,
sF1 = ifeq3(act(X0,X1),sF1,event(X0,X1),sF1) ).
cnf(u4641,negated_conjecture,
sF1 = ifeq3(mia_forename(X0,X1),sF1,forename(X0,X1),sF1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP042-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n005.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 17:51:02 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.26/1.88 % (63995)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.26/1.88 % (64004)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1427615846:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.26/1.88 % (64004)Refutation not found, incomplete strategy
% 5.26/1.88 % (64004)------------------------------
% 5.26/1.88 % (64004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64004)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64004)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.88 % (64004)Time elapsed: 0.012 s
% 5.26/1.88 % (64004)Peak memory usage: 88 MB
% 5.26/1.88 % (64004)Instructions burned: 34 (million)
% 5.26/1.88 % (64001)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=1671697383:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.26/1.88 % (64002)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2382264037:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.26/1.88 % (64003)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=378666424:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.26/1.88 % (64005)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3232690371:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.26/1.88 % (64006)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2006605777:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.26/1.88 % (64000)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=3495611975:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.26/1.88 % (64006)Refutation not found, incomplete strategy
% 5.26/1.88 % (64006)------------------------------
% 5.26/1.88 % (64006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64006)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64006)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.88 % (64006)Time elapsed: 0.016 s
% 5.26/1.88 % (64006)Peak memory usage: 87 MB
% 5.26/1.88 % (64006)Instructions burned: 26 (million)
% 5.26/1.88 % (64005)Refutation not found, incomplete strategy
% 5.26/1.88 % (64005)------------------------------
% 5.26/1.88 % (64005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64005)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64005)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.88 % (64005)Time elapsed: 0.052 s
% 5.26/1.88 % (64005)Peak memory usage: 89 MB
% 5.26/1.88 % (64005)Instructions burned: 87 (million)
% 5.26/1.88 % (64003)Refutation not found, incomplete strategy
% 5.26/1.88 % (64003)------------------------------
% 5.26/1.88 % (64003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64003)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64003)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.88 % (64003)Time elapsed: 0.067 s
% 5.26/1.88 % (64003)Peak memory usage: 88 MB
% 5.26/1.88 % (64003)Instructions burned: 130 (million)
% 5.26/1.88 % (64004)------------------------------
% 5.26/1.88 % (64004)------------------------------
% 5.26/1.88 % (64014)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2091356639:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.26/1.88 % (64006)------------------------------
% 5.26/1.88 % (64006)------------------------------
% 5.26/1.88 % (64005)------------------------------
% 5.26/1.88 % (64005)------------------------------
% 5.26/1.88 % (64003)------------------------------
% 5.26/1.88 % (64003)------------------------------
% 5.26/1.88 % (64016)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2458386583:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 5.26/1.88 % (64017)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1509726343:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.26/1.88 % (64018)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=2657275939: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.26/1.88 % (64018)First to succeed.
% 5.26/1.88 % (64018)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-63995"
% 5.26/1.88 % (64017)Instruction limit reached!
% 5.26/1.88 % (64017)------------------------------
% 5.26/1.88 % (64017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64017)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64017)Termination reason: Instruction limit
% 5.26/1.88 % (64017)Termination phase: Saturation
% 5.26/1.88 % (64017)Time elapsed: 0.109 s
% 5.26/1.88 % (64017)Peak memory usage: 92 MB
% 5.26/1.88 % (64017)Instructions burned: 216 (million)
% 5.26/1.88 % (64014)Refutation not found, incomplete strategy
% 5.26/1.88 % (64014)------------------------------
% 5.26/1.88 % (64014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64014)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64014)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.88 % (64014)Time elapsed: 0.377 s
% 5.26/1.88 % (64014)Peak memory usage: 129 MB
% 5.26/1.88 % (64014)Instructions burned: 1020 (million)
% 5.26/1.88 % (64001)Also succeeded, but the first one will report.
% 5.26/1.88 % (64002)Also succeeded, but the first one will report.
% 5.26/1.88 % (64022)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=4224189460:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 5.26/1.88 % (64000)Refutation not found, incomplete strategy
% 5.26/1.88 % (64000)------------------------------
% 5.26/1.88 % (64000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.88 % (64000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.88 % (64000)CaDiCaL version: 2.1.3
% 5.26/1.88 % (64000)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.88 % (64000)Time elapsed: 0.765 s
% 5.26/1.88 % (64000)Peak memory usage: 129 MB
% 5.26/1.88 % (64000)Instructions burned: 1126 (million)
% 5.26/1.88 % (64014)------------------------------
% 5.26/1.88 % (64014)------------------------------
% 5.26/1.88 % SZS status Satisfiable for theBenchmark
% 5.26/1.88 % SZS output start Saturation.
% See solution above
% 7.73/2.08 % SZS output start Definitions and Model Updates.
% 7.73/2.08 % SZS output end Definitions and Model Updates.
% 7.73/2.08 % (64018)------------------------------
% 7.73/2.08 % (64018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.73/2.08 % (64018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.73/2.08 % (64018)CaDiCaL version: 2.1.3
% 7.73/2.08 % (64018)Termination reason: Satisfiable
% 7.73/2.08 % (64018)Time elapsed: 0.087 s
% 7.73/2.08 % (64018)Peak memory usage: 91 MB
% 7.73/2.08 % (64018)Instructions burned: 150 (million)
% 7.73/2.08 % (64018)------------------------------
% 7.73/2.08 % (64018)------------------------------
% 7.73/2.08 % (63995)Success in time 1.016 s
% 7.73/2.08 % Vampire exiting
%------------------------------------------------------------------------------