%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP110-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 : 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:25 PM UTC 2026
% Result : Satisfiable 4.02s 1.17s
% Output : Saturation 4.56s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u206,negated_conjecture,
a != b ).
cnf(u211,negated_conjecture,
true = sF10 ).
cnf(u216,negated_conjecture,
true = sF9 ).
cnf(u221,negated_conjecture,
true = sF8 ).
cnf(u226,negated_conjecture,
true = sF7 ).
cnf(u231,negated_conjecture,
true = sF6 ).
cnf(u236,negated_conjecture,
true = sF5 ).
cnf(u241,negated_conjecture,
true = sF4 ).
cnf(u246,negated_conjecture,
true = sF3 ).
cnf(u251,negated_conjecture,
true = sF2 ).
cnf(u258,axiom,
actual_world(skc4) = sF2 ).
cnf(u263,axiom,
coffee(skc4,skc8) = sF3 ).
cnf(u268,axiom,
human_person(skc4,skc6) = sF4 ).
cnf(u273,axiom,
event(skc4,skc5) = sF5 ).
cnf(u278,axiom,
past(skc4,skc5) = sF6 ).
cnf(u283,axiom,
nonreflexive(skc4,skc5) = sF7 ).
cnf(u288,axiom,
drink(skc4,skc5) = sF8 ).
cnf(u293,axiom,
agent(skc4,skc5,skc6) = sF9 ).
cnf(u298,axiom,
patient(skc4,skc5,skc8) = sF10 ).
cnf(u309,axiom,
tuple(true,true,true) = sF39 ).
cnf(u316,negated_conjecture,
sF39 = tuple(sF10,sF10,sF10) ).
cnf(u323,negated_conjecture,
sF9 = sF10 ).
cnf(u332,negated_conjecture,
sF8 = sF10 ).
cnf(u337,negated_conjecture,
sF8 = sF9 ).
cnf(u348,negated_conjecture,
sF7 = sF10 ).
cnf(u353,negated_conjecture,
sF7 = sF9 ).
cnf(u358,negated_conjecture,
sF7 = sF8 ).
cnf(u371,negated_conjecture,
sF6 = sF10 ).
cnf(u376,negated_conjecture,
sF6 = sF9 ).
cnf(u381,negated_conjecture,
sF6 = sF8 ).
cnf(u386,negated_conjecture,
sF6 = sF7 ).
cnf(u401,negated_conjecture,
sF5 = sF10 ).
cnf(u406,negated_conjecture,
sF5 = sF9 ).
cnf(u411,negated_conjecture,
sF5 = sF8 ).
cnf(u416,negated_conjecture,
sF5 = sF7 ).
cnf(u421,negated_conjecture,
sF5 = sF6 ).
cnf(u438,negated_conjecture,
sF4 = sF5 ).
cnf(u443,negated_conjecture,
sF4 = sF6 ).
cnf(u448,negated_conjecture,
sF4 = sF7 ).
cnf(u453,negated_conjecture,
sF4 = sF8 ).
cnf(u458,negated_conjecture,
sF4 = sF9 ).
cnf(u463,negated_conjecture,
sF4 = sF10 ).
cnf(u482,negated_conjecture,
sF3 = sF4 ).
cnf(u487,negated_conjecture,
sF3 = sF5 ).
cnf(u492,negated_conjecture,
sF3 = sF6 ).
cnf(u497,negated_conjecture,
sF3 = sF7 ).
cnf(u502,negated_conjecture,
sF3 = sF8 ).
cnf(u507,negated_conjecture,
sF3 = sF9 ).
cnf(u512,negated_conjecture,
sF3 = sF10 ).
cnf(u533,negated_conjecture,
sF2 = sF3 ).
cnf(u538,negated_conjecture,
sF2 = sF4 ).
cnf(u543,negated_conjecture,
sF2 = sF5 ).
cnf(u548,negated_conjecture,
sF2 = sF6 ).
cnf(u553,negated_conjecture,
sF2 = sF7 ).
cnf(u558,negated_conjecture,
sF2 = sF8 ).
cnf(u563,negated_conjecture,
sF2 = sF9 ).
cnf(u568,negated_conjecture,
sF2 = sF10 ).
cnf(u581,negated_conjecture,
sF39 = tuple(sF2,sF2,sF2) ).
cnf(u923,negated_conjecture,
sF2 = human(skc4,skc6) ).
cnf(u1340,negated_conjecture,
sF2 = ifeq3(see(skc4,skc5),sF2,sF2,sF2) ).
cnf(u1421,negated_conjecture,
sF2 = eventuality(skc4,skc5) ).
cnf(u1496,negated_conjecture,
sF2 = thing(skc4,skc5) ).
cnf(u1508,negated_conjecture,
sF2 = singleton(skc4,skc5) ).
cnf(u1616,negated_conjecture,
sF2 = specific(skc4,skc5) ).
cnf(u1693,negated_conjecture,
sF2 = nonexistent(skc4,skc5) ).
cnf(u1770,negated_conjecture,
sF2 = unisex(skc4,skc5) ).
cnf(u1869,negated_conjecture,
event(skc4,skc5) = sF2 ).
cnf(u1958,negated_conjecture,
sF2 = beverage(skc4,skc8) ).
cnf(u2037,negated_conjecture,
sF2 = food(skc4,skc8) ).
cnf(u2114,negated_conjecture,
sF2 = substance_matter(skc4,skc8) ).
cnf(u2191,negated_conjecture,
sF2 = object(skc4,skc8) ).
cnf(u2268,negated_conjecture,
sF2 = entity(skc4,skc8) ).
cnf(u2354,negated_conjecture,
sF2 = ifeq3(entity(skc4,skc5),sF2,sF2,sF2) ).
cnf(u2360,negated_conjecture,
sF2 = thing(skc4,skc8) ).
cnf(u2373,negated_conjecture,
sF2 = ifeq3(eventuality(skc4,skc8),sF2,sF2,sF2) ).
cnf(u2380,negated_conjecture,
sF2 = singleton(skc4,skc8) ).
cnf(u2499,negated_conjecture,
sF2 = specific(skc4,skc8) ).
cnf(u2591,negated_conjecture,
sF2 = existent(skc4,skc8) ).
cnf(u2668,negated_conjecture,
sF2 = nonliving(skc4,skc8) ).
cnf(u2745,negated_conjecture,
sF2 = impartial(skc4,skc8) ).
cnf(u2831,negated_conjecture,
sF2 = ifeq3(object(skc4,skc5),sF2,sF2,sF2) ).
cnf(u2837,negated_conjecture,
sF2 = unisex(skc4,skc8) ).
cnf(u2929,negated_conjecture,
sF2 = organism(skc4,skc6) ).
cnf(u3020,negated_conjecture,
sF2 = ifeq3(organism(skc4,skc8),sF2,sF2,sF2) ).
cnf(u3026,negated_conjecture,
sF2 = entity(skc4,skc6) ).
cnf(u3043,negated_conjecture,
sF2 = ifeq3(object(skc4,skc6),sF2,sF2,sF2) ).
cnf(u3053,negated_conjecture,
sF2 = existent(skc4,skc6) ).
cnf(u3058,negated_conjecture,
sF2 = specific(skc4,skc6) ).
cnf(u3063,negated_conjecture,
sF2 = thing(skc4,skc6) ).
cnf(u3141,negated_conjecture,
sF2 = ifeq3(eventuality(skc4,skc6),sF2,sF2,sF2) ).
cnf(u3179,negated_conjecture,
sF2 = singleton(skc4,skc6) ).
cnf(u3291,negated_conjecture,
sF2 = impartial(skc4,skc6) ).
cnf(u3383,negated_conjecture,
sF2 = living(skc4,skc6) ).
cnf(u3460,negated_conjecture,
sF2 = animate(skc4,skc6) ).
cnf(u3552,negated_conjecture,
sF2 = ifeq3(sF13(skc6),sF2,sF2,sF2) ).
cnf(u3722,negated_conjecture,
sF2 = ifeq3(artifact(skc4,skc8),sF2,sF2,sF2) ).
cnf(u4289,negated_conjecture,
b = ifeq2(tuple2(nonliving(skc4,skc6),sF2),tuple2(sF2,sF2),a,b) ).
cnf(u4294,negated_conjecture,
b = ifeq2(tuple2(sF2,living(skc4,skc8)),tuple2(sF2,sF2),a,b) ).
cnf(u4378,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc4,skc6),sF2),tuple2(sF2,sF2),a,b) ).
cnf(u4383,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc4,skc8),sF2),tuple2(sF2,sF2),a,b) ).
cnf(u4388,negated_conjecture,
b = ifeq2(tuple2(sF2,existent(skc4,skc5)),tuple2(sF2,sF2),a,b) ).
cnf(u4459,negated_conjecture,
b = ifeq2(tuple2(sF2,animate(skc4,skc8)),tuple2(sF2,sF2),a,b) ).
cnf(u4513,negated_conjecture,
sF38(skc4,skc5,skc6) = tuple(patient(skc4,skc5,skc6),sF2,sF2) ).
cnf(u4519,negated_conjecture,
sF38(skc4,skc5,skc8) = tuple(sF2,sF2,agent(skc4,skc5,skc8)) ).
cnf(u4775,axiom,
sF38(skc4,skf1(skc6),skc6) = tuple(sF34(skc6),sF22(skc6),sF30(skc6)) ).
cnf(u181,axiom,
ifeq3(sF13(X0),true,sF30(X0),true) = sF31(X0) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u1336,negated_conjecture,
sF2 = ifeq3(sF26(X0),sF2,sF14(X0),sF2) ).
cnf(u4833,negated_conjecture,
sF2 = ifeq3(sF30(X0),sF2,ifeq3(sF34(X0),sF2,ifeq3(drink(skc4,skf1(X0)),sF2,beverage(skc4,skc6),sF2),sF2),sF2) ).
cnf(u3627,negated_conjecture,
sF2 = ifeq3(building(X0,X1),sF2,artifact(X0,X1),sF2) ).
cnf(u37,axiom,
true = ifeq3(object(X0,X1),true,nonliving(X0,X1),true) ).
cnf(u49,axiom,
true = ifeq3(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u1272,negated_conjecture,
sF2 = ifeq3(see(X0,X1),sF2,event(X0,X1),sF2) ).
cnf(u172,axiom,
ifeq3(sF13(X0),true,sF26(X2),true) = sF27(X0,X2) ).
cnf(u1643,negated_conjecture,
sF2 = ifeq3(eventuality(X0,X1),sF2,nonexistent(X0,X1),sF2) ).
cnf(u7,axiom,
true = ifeq3(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u179,axiom,
agent(skc4,skf1(X0),X0) = sF30(X0) ).
cnf(u2141,negated_conjecture,
sF2 = ifeq3(substance_matter(X0,X1),sF2,object(X0,X1),sF2) ).
cnf(u3617,negated_conjecture,
sF2 = ifeq3(sF12(X0),sF2,building(skc4,X0),sF2) ).
cnf(u3572,negated_conjecture,
sF2 = ifeq3(restaurant(X0,X1),sF2,building(X0,X1),sF2) ).
cnf(u302,negated_conjecture,
true = ifeq3(sF11(X0,X1),true,sF24(X1,X0,X2),true) ).
cnf(u999,negated_conjecture,
sF2 = ifeq3(sF11(X0,X1),sF2,sF16(X1,X0,X2),sF2) ).
cnf(u873,negated_conjecture,
sF2 = ifeq3(human_person(X0,X1),sF2,human(X0,X1),sF2) ).
cnf(u25,axiom,
true = ifeq3(food(X0,X1),true,substance_matter(X0,X1),true) ).
cnf(u4662,negated_conjecture,
sF2 = ifeq3(agent(skc4,skc5,X0),sF2,sF2,sF2) ).
cnf(u1860,negated_conjecture,
sF2 = ifeq3(drink(skc4,skf1(X0)),sF2,sF14(X0),sF2) ).
cnf(u1566,negated_conjecture,
sF2 = ifeq3(eventuality(X0,X1),sF2,specific(X0,X1),sF2) ).
cnf(u1044,negated_conjecture,
sF2 = ifeq3(sF11(X0,X1),sF2,sF20(X1,X0,X2),sF2) ).
cnf(u3824,negated_conjecture,
sF23(X0,X1) = ifeq3(sF13(X0),sF2,sF22(X1),sF2) ).
cnf(u1179,negated_conjecture,
sF2 = ifeq3(sF11(X0,X1),sF2,sF36(X1,X0,X2),sF2) ).
cnf(u4639,negated_conjecture,
sF2 = ifeq3(agent(skc4,skf1(X0),X1),sF2,ifeq3(sF34(X0),sF2,ifeq3(drink(skc4,skf1(X0)),sF2,beverage(skc4,skc6),sF2),sF2),sF2) ).
cnf(u3673,negated_conjecture,
sF2 = ifeq3(artifact(X0,X1),sF2,object(X0,X1),sF2) ).
cnf(u186,negated_conjecture,
true = sF33(X0,X1) ).
cnf(u305,negated_conjecture,
true = ifeq3(sF11(X0,X1),true,sF36(X1,X0,X2),true) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u29,axiom,
true = ifeq3(object(X0,X1),true,entity(X0,X1),true) ).
cnf(u139,axiom,
restaurant(skc4,X1) = sF12(X1) ).
cnf(u3547,negated_conjecture,
sF2 = ifeq3(sF13(X0),sF2,human_person(skc4,X0),sF2) ).
cnf(u2218,negated_conjecture,
sF2 = ifeq3(object(X0,X1),sF2,entity(X0,X1),sF2) ).
cnf(u55,axiom,
true = ifeq3(customer(X0,X1),true,human_person(X0,X1),true) ).
cnf(u99,axiom,
b = ifeq2(tuple2(nonliving(X0,X1),animate(X0,X1)),tuple2(true,true),a,b) ).
cnf(u159,negated_conjecture,
true = sF21(X0,X1,X2) ).
cnf(u2064,negated_conjecture,
sF2 = ifeq3(food(X0,X1),sF2,substance_matter(X0,X1),sF2) ).
cnf(u4049,negated_conjecture,
sF20(X0,X1,X2) = ifeq3(sF12(X0),sF2,sF19(X1,X2),sF2) ).
cnf(u190,axiom,
ifeq3(sF13(X0),true,sF34(X2),true) = sF35(X0,X2) ).
cnf(u4661,negated_conjecture,
sF2 = ifeq3(patient(skc4,skc5,X0),sF2,beverage(skc4,X0),sF2) ).
cnf(u5,axiom,
true = ifeq3(see(X0,X1),true,event(X0,X1),true) ).
cnf(u3779,negated_conjecture,
sF19(X0,X1) = ifeq3(sF13(X0),sF2,sF18(X1),sF2) ).
cnf(u177,negated_conjecture,
true = sF29(X0,X1,X2) ).
cnf(u3333,negated_conjecture,
sF2 = ifeq3(organism(X0,X1),sF2,living(X0,X1),sF2) ).
cnf(u4184,negated_conjecture,
sF36(X0,X1,X2) = ifeq3(sF12(X0),sF2,sF35(X1,X2),sF2) ).
cnf(u1908,negated_conjecture,
sF2 = ifeq3(coffee(X0,X1),sF2,beverage(X0,X1),sF2) ).
cnf(u2962,negated_conjecture,
sF2 = ifeq3(organism(X0,X1),sF2,entity(X0,X1),sF2) ).
cnf(u31,axiom,
true = ifeq3(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u43,axiom,
true = ifeq3(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u147,axiom,
ifeq3(sF12(X1),true,sF15(X0,X2),true) = sF16(X1,X0,X2) ).
cnf(u4643,negated_conjecture,
sF2 = ifeq3(agent(skc4,skc5,X0),sF2,ifeq3(patient(skc4,skc5,X1),sF2,beverage(skc4,X1),sF2),sF2) ).
cnf(u954,negated_conjecture,
sF2 = ifeq3(sF11(X0,X1),sF2,sF32(X1,X0),sF2) ).
cnf(u3869,negated_conjecture,
sF27(X0,X1) = ifeq3(sF13(X0),sF2,sF26(X1),sF2) ).
cnf(u2879,negated_conjecture,
sF2 = ifeq3(human_person(X0,X1),sF2,organism(X0,X1),sF2) ).
cnf(u253,negated_conjecture,
true = ifeq3(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u1089,negated_conjecture,
sF2 = ifeq3(sF11(X0,X1),sF2,sF24(X1,X0,X2),sF2) ).
cnf(u311,negated_conjecture,
b = ifeq(sF38(X0,X1,X2),sF39,a,b) ).
cnf(u156,axiom,
ifeq3(sF12(X1),true,sF19(X0,X2),true) = sF20(X1,X0,X2) ).
cnf(u3231,negated_conjecture,
sF2 = ifeq3(organism(X0,X1),sF2,impartial(X0,X1),sF2) ).
cnf(u19,axiom,
true = ifeq3(drink(X0,X1),true,event(X0,X1),true) ).
cnf(u4552,negated_conjecture,
sF2 = ifeq3(agent(X0,X1,X2),sF2,ifeq3(patient(X0,X1,X3),sF2,ifeq3(drink(X0,X1),sF2,beverage(X0,X3),sF2),sF2),sF2) ).
cnf(u45,axiom,
true = ifeq3(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u195,negated_conjecture,
true = sF37(X0,X1,X2) ).
cnf(u2296,negated_conjecture,
sF2 = ifeq3(entity(X0,X1),sF2,thing(X0,X1),sF2) ).
cnf(u154,axiom,
ifeq3(sF13(X0),true,sF18(X2),true) = sF19(X0,X2) ).
cnf(u53,axiom,
true = ifeq3(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u97,axiom,
b = ifeq2(tuple2(nonexistent(X0,X1),existent(X0,X1)),tuple2(true,true),a,b) ).
cnf(u304,negated_conjecture,
true = ifeq3(sF11(X0,X1),true,sF32(X1,X0),true) ).
cnf(u188,axiom,
patient(skc4,skf1(X2),skc6) = sF34(X2) ).
cnf(u4139,negated_conjecture,
sF28(X0,X1,X2) = ifeq3(sF12(X0),sF2,sF27(X1,X2),sF2) ).
cnf(u23,axiom,
true = ifeq3(beverage(X0,X1),true,food(X0,X1),true) ).
cnf(u192,axiom,
ifeq3(sF12(X1),true,sF35(X0,X2),true) = sF36(X1,X0,X2) ).
cnf(u1446,negated_conjecture,
sF2 = ifeq3(eventuality(X0,X1),sF2,thing(X0,X1),sF2) ).
cnf(u4480,axiom,
sF38(skc4,skf1(X0),skc6) = tuple(sF34(X0),sF22(X0),agent(skc4,skf1(X0),skc6)) ).
cnf(u41,axiom,
true = ifeq3(object(X0,X1),true,unisex(X0,X1),true) ).
cnf(u202,negated_conjecture,
b = sF40(X0,X1,X2) ).
cnf(u145,axiom,
ifeq3(sF13(X0),true,sF14(X2),true) = sF15(X0,X2) ).
cnf(u303,negated_conjecture,
true = ifeq3(sF11(X0,X1),true,sF28(X1,X0,X2),true) ).
cnf(u1987,negated_conjecture,
sF2 = ifeq3(beverage(X0,X1),sF2,food(X0,X1),sF2) ).
cnf(u3410,negated_conjecture,
sF2 = ifeq3(human_person(X0,X1),sF2,animate(X0,X1),sF2) ).
cnf(u2541,negated_conjecture,
sF2 = ifeq3(entity(X0,X1),sF2,existent(X0,X1),sF2) ).
cnf(u4474,axiom,
sF38(skc4,skf1(X0),X1) = tuple(patient(skc4,skf1(X0),X1),sF22(X0),agent(skc4,skf1(X0),X1)) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u4778,negated_conjecture,
sF2 = ifeq3(sF30(X0),sF2,ifeq3(patient(skc4,skf1(X0),skc8),sF2,ifeq3(drink(skc4,skf1(X0)),sF2,sF2,sF2),sF2),sF2) ).
cnf(u17,axiom,
true = ifeq3(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u33,axiom,
true = ifeq3(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u1224,negated_conjecture,
sF31(X0) = ifeq3(sF13(X0),sF2,sF30(X0),sF2) ).
cnf(u2695,negated_conjecture,
sF2 = ifeq3(object(X0,X1),sF2,impartial(X0,X1),sF2) ).
cnf(u108,negated_conjecture,
true = sF1(X0,X1) ).
cnf(u152,axiom,
past(skc4,skf1(X2)) = sF18(X2) ).
cnf(u2773,negated_conjecture,
sF2 = ifeq3(object(X0,X1),sF2,unisex(X0,X1),sF2) ).
cnf(u4637,negated_conjecture,
sF2 = ifeq3(agent(skc4,X0,X1),sF2,ifeq3(patient(skc4,X0,skc8),sF2,ifeq3(drink(skc4,X0),sF2,sF2,sF2),sF2),sF2) ).
cnf(u1799,negated_conjecture,
sF2 = ifeq3(drink(X0,X1),sF2,event(X0,X1),sF2) ).
cnf(u4094,negated_conjecture,
sF24(X0,X1,X2) = ifeq3(sF12(X0),sF2,sF23(X1,X2),sF2) ).
cnf(u4492,negated_conjecture,
sF38(skc4,skc5,X0) = tuple(patient(skc4,skc5,X0),sF2,agent(skc4,skc5,X0)) ).
cnf(u21,axiom,
true = ifeq3(coffee(X0,X1),true,beverage(X0,X1),true) ).
cnf(u3734,negated_conjecture,
sF15(X0,X1) = ifeq3(sF13(X0),sF2,sF14(X1),sF2) ).
cnf(u137,axiom,
in(skc4,X0,X1) = sF11(X0,X1) ).
cnf(u197,axiom,
tuple(patient(X0,X1,X2),nonreflexive(X0,X1),agent(X0,X1,X2)) = sF38(X0,X1,X2) ).
cnf(u47,axiom,
true = ifeq3(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u59,axiom,
true = ifeq3(building(X0,X1),true,artifact(X0,X1),true) ).
cnf(u1134,negated_conjecture,
sF2 = ifeq3(sF11(X0,X1),sF2,sF28(X1,X0,X2),sF2) ).
cnf(u163,axiom,
ifeq3(sF13(X0),true,sF22(X2),true) = sF23(X0,X2) ).
cnf(u9,axiom,
true = ifeq3(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u4311,negated_conjecture,
b = ifeq2(tuple2(nonexistent(X0,X1),existent(X0,X1)),tuple2(sF2,sF2),a,b) ).
cnf(u301,negated_conjecture,
true = ifeq3(sF11(X0,X1),true,sF20(X1,X0,X2),true) ).
cnf(u254,negated_conjecture,
true = ifeq3(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u2439,negated_conjecture,
sF2 = ifeq3(entity(X0,X1),sF2,specific(X0,X1),sF2) ).
cnf(u141,axiom,
customer(skc4,X0) = sF13(X0) ).
cnf(u35,axiom,
true = ifeq3(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u39,axiom,
true = ifeq3(object(X0,X1),true,impartial(X0,X1),true) ).
cnf(u95,axiom,
b = ifeq2(tuple2(nonliving(X0,X1),living(X0,X1)),tuple2(true,true),a,b) ).
cnf(u1720,negated_conjecture,
sF2 = ifeq3(eventuality(X0,X1),sF2,unisex(X0,X1),sF2) ).
cnf(u170,axiom,
see(skc4,skf1(X2)) = sF26(X2) ).
cnf(u183,axiom,
ifeq3(sF12(X1),true,sF31(X0),true) = sF32(X1,X0) ).
cnf(u13,axiom,
true = ifeq3(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u3959,negated_conjecture,
sF35(X0,X1) = ifeq3(sF13(X0),sF2,sF34(X1),sF2) ).
cnf(u827,negated_conjecture,
sF2 = ifeq3(thing(X0,X1),sF2,singleton(X0,X1),sF2) ).
cnf(u4231,negated_conjecture,
b = ifeq2(tuple2(nonliving(X0,X1),living(X0,X1)),tuple2(sF2,sF2),a,b) ).
cnf(u3914,negated_conjecture,
sF32(X0,X1) = ifeq3(sF12(X0),sF2,sF31(X1),sF2) ).
cnf(u143,axiom,
event(skc4,skf1(X2)) = sF14(X2) ).
cnf(u4641,negated_conjecture,
sF2 = ifeq3(sF30(X0),sF2,ifeq3(patient(skc4,skf1(X0),X1),sF2,ifeq3(drink(skc4,skf1(X0)),sF2,beverage(skc4,X1),sF2),sF2),sF2) ).
cnf(u1415,negated_conjecture,
sF2 = ifeq3(sF14(X0),sF2,eventuality(skc4,skf1(X0)),sF2) ).
cnf(u174,axiom,
ifeq3(sF12(X1),true,sF27(X0,X2),true) = sF28(X1,X0,X2) ).
cnf(u57,axiom,
true = ifeq3(restaurant(X0,X1),true,building(X0,X1),true) ).
cnf(u161,axiom,
nonreflexive(skc4,skf1(X2)) = sF22(X2) ).
cnf(u15,axiom,
true = ifeq3(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u27,axiom,
true = ifeq3(substance_matter(X0,X1),true,object(X0,X1),true) ).
cnf(u4477,axiom,
sF38(skc4,skf1(X0),X0) = tuple(patient(skc4,skf1(X0),X0),sF22(X0),sF30(X0)) ).
cnf(u4004,negated_conjecture,
sF16(X0,X1,X2) = ifeq3(sF12(X0),sF2,sF15(X1,X2),sF2) ).
cnf(u63,axiom,
true = ifeq3(agent(X0,X1,X2),true,ifeq3(patient(X0,X1,X3),true,ifeq3(drink(X0,X1),true,beverage(X0,X3),true),true),true) ).
cnf(u4400,negated_conjecture,
b = ifeq2(tuple2(nonliving(X0,X1),animate(X0,X1)),tuple2(sF2,sF2),a,b) ).
cnf(u150,negated_conjecture,
true = sF17(X0,X1,X2) ).
cnf(u61,axiom,
true = ifeq3(artifact(X0,X1),true,object(X0,X1),true) ).
cnf(u105,negated_conjecture,
true = sF0(X0,X1) ).
cnf(u2618,negated_conjecture,
sF2 = ifeq3(object(X0,X1),sF2,nonliving(X0,X1),sF2) ).
cnf(u165,axiom,
ifeq3(sF12(X1),true,sF23(X0,X2),true) = sF24(X1,X0,X2) ).
cnf(u1362,negated_conjecture,
sF2 = ifeq3(event(X0,X1),sF2,eventuality(X0,X1),sF2) ).
cnf(u3493,negated_conjecture,
sF2 = ifeq3(customer(X0,X1),sF2,human_person(X0,X1),sF2) ).
cnf(u300,negated_conjecture,
true = ifeq3(sF11(X0,X1),true,sF16(X1,X0,X2),true) ).
cnf(u168,negated_conjecture,
true = sF25(X0,X1,X2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NLP110-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/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:04:34 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.33 Running first-order theorem proving
% 0.08/0.33 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
% 4.02/1.17 % (2634743)Detected a unit-equality problem, will run specialized UEQ schedule.
% 4.02/1.17 % (2634818)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2929631206:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 4.02/1.17 % (2634821)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3397730489:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 4.02/1.17 % (2634816)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=3201581204:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 4.02/1.17 % (2634822)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3237035640:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 4.02/1.17 % (2634817)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=708616697:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 4.02/1.17 % (2634819)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3565728554:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 4.02/1.17 % (2634820)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=959847758:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 4.02/1.17 % (2634822)Refutation not found, incomplete strategy
% 4.02/1.17 % (2634822)------------------------------
% 4.02/1.17 % (2634822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.17 % (2634822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.17 % (2634822)CaDiCaL version: 2.1.3
% 4.02/1.17 % (2634822)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.17 % (2634822)Time elapsed: 0.005 s
% 4.02/1.17 % (2634822)Peak memory usage: 87 MB
% 4.02/1.17 % (2634822)Instructions burned: 17 (million)
% 4.02/1.17 % (2634820)Refutation not found, incomplete strategy
% 4.02/1.17 % (2634820)------------------------------
% 4.02/1.17 % (2634820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.17 % (2634820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.17 % (2634820)CaDiCaL version: 2.1.3
% 4.02/1.17 % (2634820)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.17 % (2634820)Time elapsed: 0.008 s
% 4.02/1.17 % (2634820)Peak memory usage: 88 MB
% 4.02/1.17 % (2634820)Instructions burned: 25 (million)
% 4.02/1.17 % (2634819)Refutation not found, incomplete strategy
% 4.02/1.17 % (2634819)------------------------------
% 4.02/1.17 % (2634819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.17 % (2634819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.17 % (2634819)CaDiCaL version: 2.1.3
% 4.02/1.17 % (2634819)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.17 % (2634819)Time elapsed: 0.017 s
% 4.02/1.17 % (2634819)Peak memory usage: 87 MB
% 4.02/1.17 % (2634819)Instructions burned: 63 (million)
% 4.02/1.17 % (2634821)Refutation not found, incomplete strategy
% 4.02/1.17 % (2634821)------------------------------
% 4.02/1.17 % (2634821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.17 % (2634821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.17 % (2634821)CaDiCaL version: 2.1.3
% 4.02/1.17 % (2634821)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.17 % (2634821)Time elapsed: 0.024 s
% 4.02/1.17 % (2634821)Peak memory usage: 88 MB
% 4.02/1.17 % (2634821)Instructions burned: 76 (million)
% 4.02/1.17 % (2634820)------------------------------
% 4.02/1.17 % (2634820)------------------------------
% 4.02/1.17 % (2634822)------------------------------
% 4.02/1.17 % (2634822)------------------------------
% 4.02/1.17 % (2634819)------------------------------
% 4.02/1.17 % (2634819)------------------------------
% 4.02/1.17 % (2634821)------------------------------
% 4.02/1.17 % (2634821)------------------------------
% 4.02/1.17 % (2634831)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2849916075:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 4.02/1.17 % (2634830)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3782831775:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 4.02/1.17 % (2634832)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3310347690:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 4.02/1.17 % (2634833)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=622383086:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2996 on theBenchmark for (2996ds/317Mi)
% 4.02/1.17 % (2634833)First to succeed.
% 4.02/1.17 % (2634833)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2634743"
% 4.02/1.17 % (2634832)Instruction limit reached!
% 4.02/1.17 % (2634832)------------------------------
% 4.02/1.17 % (2634832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.17 % (2634832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.17 % (2634832)CaDiCaL version: 2.1.3
% 4.02/1.17 % (2634832)Termination reason: Instruction limit
% 4.02/1.17 % (2634832)Termination phase: Saturation
% 4.02/1.17 % (2634832)Time elapsed: 0.057 s
% 4.02/1.17 % (2634832)Peak memory usage: 92 MB
% 4.02/1.17 % (2634832)Instructions burned: 216 (million)
% 4.02/1.17 % (2634818)Also succeeded, but the first one will report.
% 4.02/1.17 % (2634817)Also succeeded, but the first one will report.
% 4.02/1.17 % (2634816)Refutation not found, incomplete strategy
% 4.02/1.17 % (2634816)------------------------------
% 4.02/1.17 % (2634816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.17 % (2634816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.17 % (2634816)CaDiCaL version: 2.1.3
% 4.02/1.17 % (2634816)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.17 % (2634816)Time elapsed: 0.398 s
% 4.02/1.17 % (2634816)Peak memory usage: 127 MB
% 4.02/1.17 % (2634816)Instructions burned: 1057 (million)
% 4.02/1.17 % (2634838)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=4184064935:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2995 on theBenchmark for (2995ds/12125Mi)
% 4.02/1.17 % SZS status Satisfiable for theBenchmark
% 4.02/1.17 % SZS output start Saturation.
% See solution above
% 4.56/1.27 % SZS output start Definitions and Model Updates.
% 4.56/1.27 % SZS output end Definitions and Model Updates.
% 4.56/1.27 % (2634833)------------------------------
% 4.56/1.27 % (2634833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.56/1.27 % (2634833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.56/1.27 % (2634833)CaDiCaL version: 2.1.3
% 4.56/1.27 % (2634833)Termination reason: Satisfiable
% 4.56/1.27 % (2634833)Time elapsed: 0.034 s
% 4.56/1.27 % (2634833)Peak memory usage: 90 MB
% 4.56/1.27 % (2634833)Instructions burned: 106 (million)
% 4.56/1.27 % (2634833)------------------------------
% 4.56/1.27 % (2634833)------------------------------
% 4.56/1.27 % (2634743)Success in time 0.627 s
% 4.56/1.27 % Vampire exiting
%------------------------------------------------------------------------------