%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP023-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:08:29 PM UTC 2026
% Result : Satisfiable 0.35s 0.49s
% Output : Saturation 0.35s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u550,negated_conjecture,
true = ifeq2(entity(skc8,skc9),true,true,true) ).
cnf(u1179,negated_conjecture,
true = relation(skc8,skc9) ).
cnf(u1582,negated_conjecture,
true = living(skc8,skc10) ).
cnf(u97,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(woman(X0,X2),true,woman(X1,X2),true),true) ).
cnf(u1182,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc9),true,true,true),true) ).
cnf(u421,negated_conjecture,
true = singleton(skc8,skc7) ).
cnf(u1894,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,female(X0,skc10),true) ).
cnf(u1583,negated_conjecture,
b = ifeq(tuple(nonhuman(skc8,skc10),true),tuple(true,true),a,b) ).
cnf(u1184,negated_conjecture,
true = ifeq2(relname(skc8,skc9),true,true,true) ).
cnf(u1561,negated_conjecture,
true = female(skc8,skc10) ).
cnf(u63,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(event(X0,X2),true,event(X1,X2),true),true) ).
cnf(u1140,negated_conjecture,
b = ifeq(tuple(specific(skc8,skc8),true),tuple(true,true),a,b) ).
cnf(u371,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,dance(X0,skc11),true) ).
cnf(u314,negated_conjecture,
true = ifeq2(abstraction(skc6,skc10),true,true,true) ).
cnf(u67,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(thing(X0,X2),true,thing(X1,X2),true),true) ).
cnf(u1556,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(woman(X0,skc10),true,true,true),true) ).
cnf(u91,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(forename(X0,X2),true,forename(X1,X2),true),true) ).
cnf(u682,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc11),true) ).
cnf(u373,negated_conjecture,
true = ifeq2(accessible_world(skc8,skc8),true,true,true) ).
cnf(u681,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc10),true) ).
cnf(u2294,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,skc8,X0),X0) = X0 ).
cnf(u1136,negated_conjecture,
true = general(skc8,skc8) ).
cnf(u1318,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc9),true) ).
cnf(u1435,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(forename(X0,skc9),true,true,true),true) ).
cnf(u1083,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,desire_want(X0,skc7),true) ).
cnf(u1481,negated_conjecture,
true = ifeq2(relname(skc6,X0),true,relname(skc8,X0),true) ).
cnf(u565,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc10),true) ).
cnf(u1437,negated_conjecture,
true = ifeq2(forename(skc6,X0),true,forename(skc8,X0),true) ).
cnf(u1320,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonhuman(X0,skc9),true) ).
cnf(u1116,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(proposition(X0,skc8),true,true,true),true) ).
cnf(u363,negated_conjecture,
b = ifeq(tuple(true,human(skc6,skc9)),tuple(true,true),a,b) ).
cnf(u1761,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(impartial(X0,skc10),true,true,true),true) ).
cnf(u1314,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonhuman(X0,skc8),true,true,true),true) ).
cnf(u1110,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,proposition(X0,skc8),true) ).
cnf(u1109,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(proposition(X0,skc8),true,true,true),true) ).
cnf(u73,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).
cnf(u1893,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(female(X0,skc10),true,true,true),true) ).
cnf(u540,negated_conjecture,
true = ifeq2(entity(skc8,skc8),true,true,true) ).
cnf(u1119,negated_conjecture,
true = relation(skc8,skc8) ).
cnf(u49,axiom,
true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(clause65,axiom,
ifeq3(theme(X0,X1,X2),true,ifeq3(theme(X0,X3,X4),true,ifeq3(proposition(X0,X2),true,ifeq3(proposition(X0,X4),true,ifeq3(desire_want(X0,X1),true,ifeq3(desire_want(X0,X3),true,X2,X4),X4),X4),X4),X4),X4) = X4 ).
cnf(u2021,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,of(X0,skc9,skc10),true) ).
cnf(u139,negated_conjecture,
true = proposition(skc6,skc8) ).
cnf(u683,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc8),true) ).
cnf(u520,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc8),true) ).
cnf(u141,negated_conjecture,
true = accessible_world(skc6,skc8) ).
cnf(u2273,negated_conjecture,
skc8 = ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,X0,skc8),skc8) ).
cnf(u1693,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(entity(X0,skc10),true,true,true),true) ).
cnf(u135,negated_conjecture,
true = forename(skc6,skc9) ).
cnf(u1071,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(desire_want(X0,skc7),true,true,true),true) ).
cnf(u672,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).
cnf(u1979,negated_conjecture,
true = ifeq2(theme(skc6,X0,X1),true,theme(skc8,X0,X1),true) ).
cnf(u2246,negated_conjecture,
skc8 = ifeq3(theme(skc8,X0,X1),true,ifeq3(theme(skc8,X2,skc8),true,ifeq3(proposition(skc8,X1),true,ifeq3(desire_want(skc8,X0),true,ifeq3(desire_want(skc8,X2),true,X1,skc8),skc8),skc8),skc8),skc8) ).
cnf(u679,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc7),true) ).
cnf(u516,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc7),true,true,true),true) ).
cnf(u415,negated_conjecture,
true = unisex(skc8,skc7) ).
cnf(u2479,negated_conjecture,
ifeq3(theme(skc8,skc7,X0),true,ifeq3(theme(skc8,skc7,X1),true,ifeq3(proposition(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u914,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc7),true,true,true),true) ).
cnf(u93,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relname(X0,X2),true,relname(X1,X2),true),true) ).
cnf(u668,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).
cnf(u2071,negated_conjecture,
ifeq3(of(skc6,skc9,X0),true,ifeq3(of(skc6,X1,X0),true,ifeq3(entity(skc6,X0),true,ifeq3(forename(skc6,X1),true,skc9,X1),X1),X1),X1) = X1 ).
cnf(u1480,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relname(X0,skc9),true) ).
cnf(u464,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc11),true,true,true),true) ).
cnf(u87,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).
cnf(u1315,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonhuman(X0,skc9),true,true,true),true) ).
cnf(u245,negated_conjecture,
true = general(skc6,skc8) ).
cnf(u1797,negated_conjecture,
true = ifeq2(living(skc6,X0),true,living(skc8,X0),true) ).
cnf(u43,axiom,
true = ifeq2(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u232,negated_conjecture,
true = thing(skc6,skc8) ).
cnf(u367,negated_conjecture,
b = ifeq(tuple(nonexistent(skc6,skc10),true),tuple(true,true),a,b) ).
cnf(u1317,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc9),true,true,true),true) ).
cnf(u45,axiom,
true = ifeq2(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u226,negated_conjecture,
true = abstraction(skc6,skc8) ).
cnf(u2433,negated_conjecture,
skc8 = ifeq3(theme(skc6,X0,skc8),true,ifeq3(theme(skc6,X1,skc8),true,ifeq3(desire_want(skc6,X0),true,ifeq3(desire_want(skc6,X1),true,skc8,skc8),skc8),skc8),skc8) ).
cnf(u353,negated_conjecture,
b = ifeq(tuple(true,female(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u677,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc10),true) ).
cnf(u416,negated_conjecture,
true = ifeq2(entity(skc8,skc7),true,true,true) ).
cnf(u39,axiom,
true = ifeq2(woman(X0,X1),true,human_person(X0,X1),true) ).
cnf(u1018,negated_conjecture,
true = ifeq2(present(X0,skc11),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u69,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(singleton(X0,X2),true,singleton(X1,X2),true),true) ).
cnf(u260,negated_conjecture,
true = ifeq2(relname(skc6,skc8),true,true,true) ).
cnf(u2090,negated_conjecture,
skc9 = ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,X0,skc9),skc9) ).
cnf(u184,negated_conjecture,
true = nonexistent(skc8,skc11) ).
cnf(u25,axiom,
true = ifeq2(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u349,negated_conjecture,
true = female(skc6,skc10) ).
cnf(u1728,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(existent(X0,skc10),true,true,true),true) ).
cnf(u2092,negated_conjecture,
ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,skc9,X0),X0) = X0 ).
cnf(u153,negated_conjecture,
true = theme(skc6,skc7,skc8) ).
cnf(u437,negated_conjecture,
true = ifeq2(accessible_world(skc6,skc6),true,true,true) ).
cnf(u19,axiom,
true = ifeq2(desire_want(X0,X1),true,event(X0,X1),true) ).
cnf(u1138,negated_conjecture,
b = ifeq(tuple(true,human(skc8,skc8)),tuple(true,true),a,b) ).
cnf(u180,negated_conjecture,
true = specific(skc8,skc11) ).
cnf(u21,axiom,
true = ifeq2(proposition(X0,X1),true,relation(X0,X1),true) ).
cnf(u329,negated_conjecture,
true = existent(skc6,skc10) ).
cnf(u1663,negated_conjecture,
true = ifeq2(organism(skc6,X0),true,organism(skc8,X0),true) ).
cnf(u15,axiom,
true = ifeq2(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u1446,negated_conjecture,
true = relname(skc8,skc9) ).
cnf(u1926,negated_conjecture,
true = ifeq2(agent(X0,skc11,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u2162,negated_conjecture,
skc9 = ifeq3(of(skc8,skc9,X0),true,ifeq3(of(skc8,skc9,X0),true,ifeq3(entity(skc8,X0),true,skc9,skc9),skc9),skc9) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u933,negated_conjecture,
true = unisex(skc8,skc8) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u1627,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human_person(X0,skc10),true,true,true),true) ).
cnf(u794,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skc7),true,true,true),true) ).
cnf(u2398,negated_conjecture,
skc8 = ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,skc8),true,ifeq3(proposition(skc6,X0),true,ifeq3(desire_want(skc6,X1),true,X0,skc8),skc8),skc8),skc8) ).
cnf(u1442,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(forename(X0,skc9),true,true,true),true) ).
cnf(u913,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc11),true,true,true),true) ).
cnf(u119,axiom,
true = ifeq2(theme(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).
cnf(u561,negated_conjecture,
true = ifeq2(abstraction(skc8,skc10),true,true,true) ).
cnf(u1937,negated_conjecture,
true = agent(skc8,skc7,skc10) ).
cnf(u2030,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,of(X0,skc9,skc10),true) ).
cnf(u2309,negated_conjecture,
skc8 = ifeq3(theme(skc8,skc7,X0),true,ifeq3(proposition(skc8,X0),true,X0,skc8),skc8) ).
cnf(u519,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc10),true) ).
cnf(u512,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc7),true,true,true),true) ).
cnf(u1695,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,entity(X0,skc10),true) ).
cnf(u558,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc10),true,true,true),true) ).
cnf(u1187,negated_conjecture,
true = abstraction(skc8,skc9) ).
cnf(u1827,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human(X0,skc10),true,true,true),true) ).
cnf(u309,negated_conjecture,
true = ifeq2(entity(skc6,skc7),true,true,true) ).
cnf(u2026,negated_conjecture,
true = of(skc8,skc9,skc10) ).
cnf(u1380,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc9),true) ).
cnf(u808,negated_conjecture,
true = specific(skc8,skc10) ).
cnf(u1513,negated_conjecture,
true = ifeq2(mia_forename(skc6,X0),true,mia_forename(skc8,X0),true) ).
cnf(u538,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc8),true,true,true),true) ).
cnf(u1199,negated_conjecture,
true = general(skc8,skc9) ).
cnf(u1826,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(human(X0,skc10),true,true,true),true) ).
cnf(u1186,negated_conjecture,
true = ifeq2(proposition(skc8,skc9),true,true,true) ).
cnf(u2530,negated_conjecture,
skc8 = ifeq3(theme(skc8,skc7,X0),true,ifeq3(theme(skc8,X1,skc8),true,ifeq3(proposition(skc8,X0),true,ifeq3(desire_want(skc8,X1),true,X0,skc8),skc8),skc8),skc8) ).
cnf(u222,negated_conjecture,
true = relation(skc6,skc8) ).
cnf(u1384,negated_conjecture,
true = ifeq2(general(skc6,X0),true,general(skc8,X0),true) ).
cnf(u1172,negated_conjecture,
true = ifeq2(relation(skc6,X0),true,relation(skc8,X0),true) ).
cnf(u1978,negated_conjecture,
true = ifeq2(theme(X0,skc7,skc8),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u517,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc7),true) ).
cnf(u412,negated_conjecture,
true = thing(skc8,skc7) ).
cnf(u1516,negated_conjecture,
true = mia_forename(skc8,skc9) ).
cnf(u2072,negated_conjecture,
ifeq3(of(skc8,X0,skc10),true,ifeq3(of(skc8,X1,skc10),true,ifeq3(forename(skc8,X0),true,ifeq3(forename(skc8,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u208,negated_conjecture,
true = unisex(skc6,skc7) ).
cnf(u915,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc7),true,true,true),true) ).
cnf(u2247,negated_conjecture,
skc8 = ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,X2,skc8),true,ifeq3(proposition(skc6,X1),true,ifeq3(desire_want(skc6,X0),true,ifeq3(desire_want(skc6,X2),true,X1,skc8),skc8),skc8),skc8),skc8) ).
cnf(u95,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(mia_forename(X0,X2),true,mia_forename(X1,X2),true),true) ).
cnf(u563,negated_conjecture,
true = ifeq2(eventuality(skc8,skc10),true,true,true) ).
cnf(u1378,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc8),true,true,true),true) ).
cnf(u1925,negated_conjecture,
true = ifeq2(agent(X0,skc7,skc10),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u813,negated_conjecture,
b = ifeq(tuple(true,general(skc8,skc10)),tuple(true,true),a,b) ).
cnf(u2266,negated_conjecture,
skc8 = ifeq3(theme(skc8,X0,X1),true,ifeq3(proposition(skc8,X1),true,ifeq3(desire_want(skc8,X0),true,X1,skc8),skc8),skc8) ).
cnf(u362,negated_conjecture,
b = ifeq(tuple(true,human(skc6,skc8)),tuple(true,true),a,b) ).
cnf(u2481,negated_conjecture,
ifeq3(theme(skc8,X0,skc8),true,ifeq3(theme(skc8,skc7,X1),true,ifeq3(proposition(skc8,X1),true,ifeq3(desire_want(skc8,X0),true,skc8,X1),X1),X1),X1) = X1 ).
cnf(u1892,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(female(X0,skc10),true,true,true),true) ).
cnf(u555,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc9),true) ).
cnf(u2268,negated_conjecture,
ifeq3(theme(skc8,X0,X1),true,ifeq3(proposition(skc8,X1),true,ifeq3(desire_want(skc8,X0),true,skc8,X1),X1),X1) = X1 ).
cnf(u936,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc8),true,true,true),true) ).
cnf(u386,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc11),true,true,true),true) ).
cnf(u867,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc11),true,true,true),true) ).
cnf(u2020,negated_conjecture,
true = ifeq2(of(skc6,X0,X1),true,of(skc8,X0,X1),true) ).
cnf(u1570,negated_conjecture,
true = human(skc8,skc10) ).
cnf(u358,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u197,negated_conjecture,
true = eventuality(skc6,skc7) ).
cnf(u1569,negated_conjecture,
true = organism(skc8,skc10) ).
cnf(u388,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,event(X0,skc7),true) ).
cnf(u417,negated_conjecture,
true = ifeq2(abstraction(skc8,skc7),true,true,true) ).
cnf(u57,axiom,
true = ifeq2(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u1630,negated_conjecture,
true = ifeq2(human_person(skc6,X0),true,human_person(skc8,X0),true) ).
cnf(u548,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u1019,negated_conjecture,
true = ifeq2(present(X0,skc7),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u946,negated_conjecture,
b = ifeq(tuple(true,female(skc8,skc9)),tuple(true,true),a,b) ).
cnf(u125,negated_conjecture,
true = actual_world(skc6) ).
cnf(u316,negated_conjecture,
true = ifeq2(eventuality(skc6,skc10),true,true,true) ).
cnf(u147,negated_conjecture,
true = of(skc6,skc9,skc10) ).
cnf(u1549,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(woman(X0,skc10),true,true,true),true) ).
cnf(u2565,negated_conjecture,
skc8 = ifeq3(theme(skc8,X0,skc8),true,ifeq3(theme(skc8,X1,skc8),true,ifeq3(desire_want(skc8,X0),true,ifeq3(desire_want(skc8,X1),true,skc8,skc8),skc8),skc8),skc8) ).
cnf(u1560,negated_conjecture,
true = human_person(skc8,skc10) ).
cnf(u528,negated_conjecture,
true = ifeq2(thing(skc6,skc11),true,true,true) ).
cnf(u149,negated_conjecture,
true = agent(skc6,skc7,skc10) ).
cnf(u212,negated_conjecture,
true = singleton(skc6,skc7) ).
cnf(u1829,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,human(X0,skc10),true) ).
cnf(u535,negated_conjecture,
true = thing(skc8,skc10) ).
cnf(u1863,negated_conjecture,
true = ifeq2(animate(skc6,X0),true,animate(skc8,X0),true) ).
cnf(u105,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(existent(X0,X2),true,existent(X1,X2),true),true) ).
cnf(u296,negated_conjecture,
true = human_person(skc6,skc10) ).
cnf(u143,negated_conjecture,
true = desire_want(skc6,skc7) ).
cnf(u188,negated_conjecture,
true = unisex(skc8,skc11) ).
cnf(u1126,negated_conjecture,
true = abstraction(skc8,skc8) ).
cnf(u99,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human_person(X0,X2),true,human_person(X1,X2),true),true) ).
cnf(u1764,negated_conjecture,
true = ifeq2(impartial(skc6,X0),true,impartial(skc8,X0),true) ).
cnf(u129,negated_conjecture,
true = woman(skc6,skc10) ).
cnf(u1796,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,living(X0,skc10),true) ).
cnf(u922,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc11),true) ).
cnf(u101,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(organism(X0,X2),true,organism(X1,X2),true),true) ).
cnf(u795,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skc10),true,true,true),true) ).
cnf(u690,negated_conjecture,
true = ifeq2(singleton(skc6,skc11),true,true,true) ).
cnf(u1376,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(general(X0,skc8),true,true,true),true) ).
cnf(u403,negated_conjecture,
true = eventuality(skc8,skc7) ).
cnf(u534,negated_conjecture,
true = thing(skc8,skc9) ).
cnf(u51,axiom,
true = ifeq2(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u918,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc9),true) ).
cnf(u81,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(proposition(X0,X2),true,proposition(X1,X2),true),true) ).
cnf(u1166,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relation(X0,skc8),true,true,true),true) ).
cnf(u53,axiom,
true = ifeq2(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u387,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(event(X0,skc7),true,true,true),true) ).
cnf(u361,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc9),true),tuple(true,true),a,b) ).
cnf(u1793,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(living(X0,skc10),true,true,true),true) ).
cnf(u1168,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc8),true,true,true),true) ).
cnf(u514,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc10),true,true,true),true) ).
cnf(u1731,negated_conjecture,
true = ifeq2(existent(skc6,X0),true,existent(skc8,X0),true) ).
cnf(u47,axiom,
true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u355,negated_conjecture,
b = ifeq(tuple(true,female(skc6,skc9)),tuple(true,true),a,b) ).
cnf(u870,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonexistent(X0,skc7),true) ).
cnf(u1322,negated_conjecture,
true = ifeq2(nonhuman(skc6,X0),true,nonhuman(skc8,X0),true) ).
cnf(u666,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc8),true,true,true),true) ).
cnf(u357,negated_conjecture,
b = ifeq(tuple(true,general(skc8,skc11)),tuple(true,true),a,b) ).
cnf(u1692,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(entity(X0,skc10),true,true,true),true) ).
cnf(u1562,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,woman(X0,skc10),true) ).
cnf(u1120,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,proposition(X0,skc8),true) ).
cnf(u1479,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,relname(X0,skc9),true) ).
cnf(u932,negated_conjecture,
true = unisex(skc8,skc9) ).
cnf(u1076,negated_conjecture,
true = desire_want(skc8,skc7) ).
cnf(u1694,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,entity(X0,skc10),true) ).
cnf(u1114,negated_conjecture,
true = proposition(skc8,skc8) ).
cnf(u1581,negated_conjecture,
true = impartial(skc8,skc10) ).
cnf(u941,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc8),true) ).
cnf(u2269,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(proposition(skc6,X1),true,ifeq3(desire_want(skc6,X0),true,skc8,X1),X1),X1) = X1 ).
cnf(u2122,negated_conjecture,
skc9 = ifeq3(of(skc6,skc9,X0),true,ifeq3(of(skc6,skc9,X0),true,ifeq3(entity(skc6,X0),true,skc9,skc9),skc9),skc9) ).
cnf(u1072,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,desire_want(X0,skc7),true) ).
cnf(u1252,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc9),true) ).
cnf(u1079,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(desire_want(X0,skc7),true,true,true),true) ).
cnf(u680,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc9),true) ).
cnf(u206,negated_conjecture,
true = specific(skc6,skc7) ).
cnf(u1948,negated_conjecture,
true = ifeq2(agent(skc6,skc11,skc10),true,true,true) ).
cnf(u515,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u1523,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,mia_forename(X0,skc9),true) ).
cnf(u1661,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,organism(X0,skc10),true) ).
cnf(u251,negated_conjecture,
true = unisex(skc6,skc8) ).
cnf(u676,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc9),true) ).
cnf(u1383,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,general(X0,skc8),true) ).
cnf(u472,negated_conjecture,
true = ifeq2(eventuality(skc6,skc11),true,true,true) ).
cnf(u667,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc11),true,true,true),true) ).
cnf(u1171,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relation(X0,skc8),true) ).
cnf(u113,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(animate(X0,X2),true,animate(X1,X2),true),true) ).
cnf(u317,negated_conjecture,
true = singleton(skc6,skc10) ).
cnf(u466,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(eventuality(X0,skc7),true,true,true),true) ).
cnf(u2068,negated_conjecture,
skc9 = ifeq3(of(skc8,X0,X1),true,ifeq3(of(skc8,skc9,X1),true,ifeq3(entity(skc8,X1),true,ifeq3(forename(skc8,X0),true,X0,skc9),skc9),skc9),skc9) ).
cnf(u468,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc7),true) ).
cnf(u816,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc10),true) ).
cnf(u75,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(unisex(X0,X2),true,unisex(X1,X2),true),true) ).
cnf(u311,negated_conjecture,
true = ifeq2(entity(skc6,skc9),true,true,true) ).
cnf(u1519,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(mia_forename(X0,skc9),true,true,true),true) ).
cnf(u2330,negated_conjecture,
ifeq3(theme(skc8,skc7,X0),true,ifeq3(proposition(skc8,X0),true,skc8,X0),X0) = X0 ).
cnf(u236,negated_conjecture,
true = singleton(skc6,skc8) ).
cnf(u77,axiom,
true = ifeq2(present(X0,X1),true,ifeq2(accessible_world(X0,X2),true,present(X2,X1),true),true) ).
cnf(u1321,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonhuman(X0,skc8),true) ).
cnf(u1629,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,human_person(X0,skc10),true) ).
cnf(u33,axiom,
true = ifeq2(forename(X0,X1),true,relname(X0,X1),true) ).
cnf(u230,negated_conjecture,
true = ifeq2(abstraction(skc8,skc11),true,true,true) ).
cnf(u71,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(specific(X0,X2),true,specific(X1,X2),true),true) ).
cnf(u1895,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,female(X0,skc10),true) ).
cnf(u2248,negated_conjecture,
ifeq3(theme(skc8,X0,skc8),true,ifeq3(theme(skc8,X1,X2),true,ifeq3(proposition(skc8,X2),true,ifeq3(desire_want(skc8,X0),true,ifeq3(desire_want(skc8,X1),true,skc8,X2),X2),X2),X2),X2) = X2 ).
cnf(u27,axiom,
true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u1022,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,present(X0,skc11),true) ).
cnf(u2091,negated_conjecture,
skc9 = ifeq3(of(skc6,X0,skc10),true,ifeq3(forename(skc6,X0),true,X0,skc9),skc9) ).
cnf(u923,negated_conjecture,
true = ifeq2(unisex(skc6,X0),true,unisex(skc8,X0),true) ).
cnf(u1626,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(human_person(X0,skc10),true,true,true),true) ).
cnf(u1660,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(organism(X0,skc10),true,true,true),true) ).
cnf(u414,negated_conjecture,
true = nonexistent(skc8,skc7) ).
cnf(u2242,negated_conjecture,
ifeq3(theme(skc8,X0,X1),true,ifeq3(theme(skc8,skc7,X2),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X2),true,ifeq3(desire_want(skc8,X0),true,X1,X2),X2),X2),X2),X2) = X2 ).
cnf(u29,axiom,
true = ifeq2(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u2093,negated_conjecture,
ifeq3(of(skc6,X0,skc10),true,ifeq3(forename(skc6,X0),true,skc9,X0),X0) = X0 ).
cnf(u337,negated_conjecture,
true = living(skc6,skc10) ).
cnf(u370,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(dance(X0,skc11),true,true,true),true) ).
cnf(u400,negated_conjecture,
true = ifeq2(desire_want(skc8,skc7),true,true,true) ).
cnf(u1601,negated_conjecture,
b = ifeq(tuple(nonexistent(skc8,skc10),true),tuple(true,true),a,b) ).
cnf(u23,axiom,
true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u9,axiom,
true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u560,negated_conjecture,
true = ifeq2(entity(skc8,skc10),true,true,true) ).
cnf(u372,negated_conjecture,
true = ifeq2(dance(skc6,X0),true,dance(skc8,X0),true) ).
cnf(u168,negated_conjecture,
true = eventuality(skc8,skc11) ).
cnf(u1987,negated_conjecture,
true = ifeq2(theme(X0,skc7,skc8),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u875,negated_conjecture,
true = ifeq2(nonexistent(skc6,skc11),true,true,true) ).
cnf(u2028,negated_conjecture,
true = ifeq2(of(X0,skc9,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u333,negated_conjecture,
true = impartial(skc6,skc10) ).
cnf(u1478,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relname(X0,skc9),true,true,true),true) ).
cnf(u366,negated_conjecture,
b = ifeq(tuple(true,existent(skc6,skc7)),tuple(true,true),a,b) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u176,negated_conjecture,
true = singleton(skc8,skc11) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u161,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u1828,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,human(X0,skc10),true) ).
cnf(u921,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc7),true) ).
cnf(u2070,negated_conjecture,
ifeq3(of(skc8,skc9,X0),true,ifeq3(of(skc8,X1,X0),true,ifeq3(entity(skc8,X0),true,ifeq3(forename(skc8,X1),true,skc9,X1),X1),X1),X1) = X1 ).
cnf(u5,axiom,
true = ifeq2(dance(X0,X1),true,event(X0,X1),true) ).
cnf(u1436,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,forename(X0,skc9),true) ).
cnf(u2347,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u441,negated_conjecture,
true = ifeq2(accessible_world(skc8,skc6),true,true,true) ).
cnf(u798,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc7),true) ).
cnf(u1248,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(abstraction(X0,skc8),true,true,true),true) ).
cnf(u1980,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,theme(X0,skc7,skc8),true) ).
cnf(u127,negated_conjecture,
true = event(skc8,skc11) ).
cnf(u1255,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,abstraction(X0,skc8),true) ).
cnf(u2349,negated_conjecture,
ifeq3(theme(skc6,X0,skc8),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(proposition(skc6,X1),true,ifeq3(desire_want(skc6,X0),true,skc8,X1),X1),X1),X1) = X1 ).
cnf(u1251,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc9),true,true,true),true) ).
cnf(u917,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc9),true,true,true),true) ).
cnf(u1762,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,impartial(X0,skc10),true) ).
cnf(u279,negated_conjecture,
true = ifeq2(eventuality(skc6,skc9),true,true,true) ).
cnf(u1198,negated_conjecture,
true = nonhuman(skc8,skc9) ).
cnf(u873,negated_conjecture,
true = ifeq2(nonexistent(skc6,X0),true,nonexistent(skc8,X0),true) ).
cnf(u265,negated_conjecture,
true = abstraction(skc6,skc9) ).
cnf(u1763,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,impartial(X0,skc10),true) ).
cnf(u1382,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,general(X0,skc9),true) ).
cnf(u109,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(living(X0,X2),true,living(X1,X2),true),true) ).
cnf(u545,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc8),true) ).
cnf(u1250,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc8),true,true,true),true) ).
cnf(u869,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonexistent(X0,skc7),true,true,true),true) ).
cnf(u1572,negated_conjecture,
b = ifeq(tuple(unisex(skc8,skc10),true),tuple(true,true),a,b) ).
cnf(u115,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(female(X0,X2),true,female(X1,X2),true),true) ).
cnf(u261,negated_conjecture,
true = relation(skc6,skc9) ).
cnf(u103,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(entity(X0,X2),true,entity(X1,X2),true),true) ).
cnf(u1021,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,present(X0,skc7),true) ).
cnf(u1024,negated_conjecture,
true = ifeq2(present(skc6,skc11),true,true,true) ).
cnf(u541,negated_conjecture,
true = ifeq2(abstraction(skc8,skc8),true,true,true) ).
cnf(u1511,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(mia_forename(X0,skc9),true,true,true),true) ).
cnf(u793,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc7),true,true,true),true) ).
cnf(u1447,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,forename(X0,skc9),true) ).
cnf(u792,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc11),true,true,true),true) ).
cnf(u522,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc11),true) ).
cnf(u65,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).
cnf(u521,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc7),true) ).
cnf(u919,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc8),true) ).
cnf(u1170,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relation(X0,skc9),true) ).
cnf(u1554,negated_conjecture,
true = woman(skc8,skc10) ).
cnf(u2267,negated_conjecture,
skc8 = ifeq3(theme(skc6,X0,X1),true,ifeq3(proposition(skc6,X1),true,ifeq3(desire_want(skc6,X0),true,X1,skc8),skc8),skc8) ).
cnf(u1169,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc8),true) ).
cnf(u1477,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relname(X0,skc9),true,true,true),true) ).
cnf(u1929,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,agent(X0,skc7,skc10),true) ).
cnf(u205,negated_conjecture,
true = thing(skc6,skc7) ).
cnf(u1316,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc8),true,true,true),true) ).
cnf(u396,negated_conjecture,
true = event(skc8,skc7) ).
cnf(u192,negated_conjecture,
true = ifeq2(desire_want(skc8,skc11),true,true,true) ).
cnf(u352,negated_conjecture,
b = ifeq(tuple(true,female(skc8,skc11)),tuple(true,true),a,b) ).
cnf(u1135,negated_conjecture,
true = nonhuman(skc8,skc8) ).
cnf(u390,negated_conjecture,
true = ifeq2(event(skc6,X0),true,event(skc8,X0),true) ).
cnf(u871,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc7),true) ).
cnf(u1939,negated_conjecture,
true = ifeq2(agent(X0,skc7,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u1122,negated_conjecture,
true = ifeq2(relname(skc8,skc8),true,true,true) ).
cnf(u155,axiom,
b = ifeq(tuple(unisex(X0,X1),female(X0,X1)),tuple(true,true),a,b) ).
cnf(u79,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(desire_want(X0,X2),true,desire_want(X1,X2),true),true) ).
cnf(u536,negated_conjecture,
true = thing(skc8,skc8) ).
cnf(u157,axiom,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).
cnf(u920,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc7),true) ).
cnf(u465,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc7),true,true,true),true) ).
cnf(u543,negated_conjecture,
true = ifeq2(eventuality(skc8,skc8),true,true,true) ).
cnf(u304,negated_conjecture,
true = entity(skc6,skc10) ).
cnf(u151,negated_conjecture,
true = agent(skc8,skc11,skc10) ).
cnf(u1379,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc9),true,true,true),true) ).
cnf(clause64,axiom,
ifeq3(of(X0,X1,X2),true,ifeq3(of(X0,X3,X2),true,ifeq3(entity(X0,X2),true,ifeq3(forename(X0,X1),true,ifeq3(forename(X0,X3),true,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u1861,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,animate(X0,skc10),true) ).
cnf(u107,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(impartial(X0,X2),true,impartial(X1,X2),true),true) ).
cnf(u137,negated_conjecture,
true = mia_forename(skc6,skc9) ).
cnf(u1381,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc8),true) ).
cnf(u523,negated_conjecture,
true = ifeq2(thing(skc6,X0),true,thing(skc8,X0),true) ).
cnf(u1662,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,organism(X0,skc10),true) ).
cnf(u300,negated_conjecture,
true = organism(skc6,skc10) ).
cnf(u131,negated_conjecture,
true = present(skc8,skc11) ).
cnf(u684,negated_conjecture,
true = ifeq2(singleton(skc6,X0),true,singleton(skc8,X0),true) ).
cnf(u803,negated_conjecture,
true = ifeq2(specific(skc6,skc11),true,true,true) ).
cnf(u310,negated_conjecture,
true = ifeq2(entity(skc6,skc8),true,true,true) ).
cnf(u944,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc9),true,true,true),true) ).
cnf(u133,negated_conjecture,
true = dance(skc8,skc11) ).
cnf(u2073,negated_conjecture,
ifeq3(of(skc6,X0,skc10),true,ifeq3(of(skc6,X1,skc10),true,ifeq3(forename(skc6,X0),true,ifeq3(forename(skc6,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u324,negated_conjecture,
true = specific(skc6,skc10) ).
cnf(u59,axiom,
true = ifeq2(woman(X0,X1),true,female(X0,X1),true) ).
cnf(u89,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(general(X0,X2),true,general(X1,X2),true),true) ).
cnf(u117,axiom,
true = ifeq2(agent(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).
cnf(u280,negated_conjecture,
true = singleton(skc6,skc9) ).
cnf(u413,negated_conjecture,
true = specific(skc8,skc7) ).
cnf(u2274,negated_conjecture,
skc8 = ifeq3(theme(skc6,X0,skc8),true,ifeq3(desire_want(skc6,X0),true,skc8,skc8),skc8) ).
cnf(u61,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(dance(X0,X2),true,dance(X1,X2),true),true) ).
cnf(u1927,negated_conjecture,
true = ifeq2(agent(skc6,X0,X1),true,agent(skc8,X0,X1),true) ).
cnf(u83,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relation(X0,X2),true,relation(X1,X2),true),true) ).
cnf(u274,negated_conjecture,
true = nonhuman(skc6,skc9) ).
cnf(u241,negated_conjecture,
true = nonhuman(skc6,skc8) ).
cnf(u1830,negated_conjecture,
true = ifeq2(human(skc6,X0),true,human(skc8,X0),true) ).
cnf(u1859,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(animate(X0,skc10),true,true,true),true) ).
cnf(u55,axiom,
true = ifeq2(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u85,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).
cnf(u172,negated_conjecture,
true = thing(skc8,skc11) ).
cnf(u276,negated_conjecture,
true = unisex(skc6,skc9) ).
cnf(u393,negated_conjecture,
true = ifeq2(event(skc6,skc11),true,true,true) ).
cnf(u1727,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(existent(X0,skc10),true,true,true),true) ).
cnf(u2019,negated_conjecture,
true = ifeq2(of(X0,skc9,skc10),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u41,axiom,
true = ifeq2(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u674,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc7),true,true,true),true) ).
cnf(u365,negated_conjecture,
b = ifeq(tuple(true,existent(skc8,skc11)),tuple(true,true),a,b) ).
cnf(u673,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u518,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc9),true) ).
cnf(u35,axiom,
true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u1794,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(living(X0,skc10),true,true,true),true) ).
cnf(u359,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skc10)),tuple(true,true),a,b) ).
cnf(u389,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc11),true) ).
cnf(u2069,negated_conjecture,
skc9 = ifeq3(of(skc6,X0,X1),true,ifeq3(of(skc6,skc9,X1),true,ifeq3(entity(skc6,X1),true,ifeq3(forename(skc6,X0),true,X0,skc9),skc9),skc9),skc9) ).
cnf(u37,axiom,
true = ifeq2(mia_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u670,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc7),true,true,true),true) ).
cnf(u345,negated_conjecture,
true = animate(skc6,skc10) ).
cnf(u1551,negated_conjecture,
true = ifeq2(woman(skc6,X0),true,woman(skc8,X0),true) ).
cnf(u669,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u31,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u159,axiom,
b = ifeq(tuple(nonhuman(X0,X1),human(X0,X1)),tuple(true,true),a,b) ).
cnf(u1696,negated_conjecture,
true = ifeq2(entity(skc6,X0),true,entity(skc8,X0),true) ).
cnf(u949,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc9),true) ).
cnf(u17,axiom,
true = ifeq2(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u1550,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,woman(X0,skc10),true) ).
cnf(u341,negated_conjecture,
true = human(skc6,skc10) ).
cnf(u1896,negated_conjecture,
true = ifeq2(female(skc6,X0),true,female(skc8,X0),true) ).
cnf(u678,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc8),true) ).
cnf(u1795,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,living(X0,skc10),true) ).
cnf(u1254,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,abstraction(X0,skc9),true) ).
cnf(u1073,negated_conjecture,
true = ifeq2(desire_want(skc6,X0),true,desire_want(skc8,X0),true) ).
cnf(u916,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc8),true,true,true),true) ).
cnf(u1111,negated_conjecture,
true = ifeq2(proposition(skc6,X0),true,proposition(skc8,X0),true) ).
cnf(u1253,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc8),true) ).
cnf(u1444,negated_conjecture,
true = ifeq2(mia_forename(skc8,skc9),true,true,true) ).
cnf(u872,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc11),true) ).
cnf(u1256,negated_conjecture,
true = ifeq2(abstraction(skc6,X0),true,abstraction(skc8,X0),true) ).
cnf(u121,axiom,
true = ifeq2(of(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).
cnf(u1730,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,existent(X0,skc10),true) ).
cnf(u675,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc7),true) ).
cnf(u1729,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,existent(X0,skc10),true) ).
cnf(u1203,negated_conjecture,
b = ifeq(tuple(specific(skc8,skc9),true),tuple(true,true),a,b) ).
cnf(u1377,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(general(X0,skc9),true,true,true),true) ).
cnf(u1249,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(abstraction(X0,skc9),true,true,true),true) ).
cnf(u868,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc7),true,true,true),true) ).
cnf(u1862,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,animate(X0,skc10),true) ).
cnf(u671,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc8),true,true,true),true) ).
cnf(u1512,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,mia_forename(X0,skc9),true) ).
cnf(u554,negated_conjecture,
true = singleton(skc8,skc9) ).
cnf(u1020,negated_conjecture,
true = ifeq2(present(skc6,X0),true,present(skc8,X0),true) ).
cnf(u470,negated_conjecture,
true = ifeq2(eventuality(skc6,X0),true,eventuality(skc8,X0),true) ).
cnf(u1989,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,theme(X0,skc7,skc8),true) ).
cnf(u1027,negated_conjecture,
true = ifeq2(present(X0,skc7),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u235,negated_conjecture,
true = ifeq2(eventuality(skc6,skc8),true,true,true) ).
cnf(u426,negated_conjecture,
b = ifeq(tuple(true,existent(skc8,skc7)),tuple(true,true),a,b) ).
cnf(u111,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human(X0,X2),true,human(X1,X2),true),true) ).
cnf(u1201,negated_conjecture,
b = ifeq(tuple(true,human(skc8,skc9)),tuple(true,true),a,b) ).
cnf(u1188,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc9),true) ).
cnf(u1029,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,present(X0,skc7),true) ).
cnf(u264,negated_conjecture,
true = ifeq2(proposition(skc6,skc9),true,true,true) ).
cnf(u256,negated_conjecture,
true = relname(skc6,skc9) ).
cnf(u231,negated_conjecture,
true = ifeq2(abstraction(skc6,skc7),true,true,true) ).
cnf(u422,negated_conjecture,
b = ifeq(tuple(true,general(skc8,skc7)),tuple(true,true),a,b) ).
cnf(u1596,negated_conjecture,
true = existent(skc8,skc10) ).
cnf(u1941,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,agent(X0,skc7,skc10),true) ).
cnf(u800,negated_conjecture,
true = ifeq2(specific(skc6,X0),true,specific(skc8,X0),true) ).
cnf(u1025,negated_conjecture,
true = present(skc8,skc7) ).
cnf(u2249,negated_conjecture,
ifeq3(theme(skc6,X0,skc8),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(proposition(skc6,X2),true,ifeq3(desire_want(skc6,X0),true,ifeq3(desire_want(skc6,X1),true,skc8,X2),X2),X2),X2),X2) = X2 ).
cnf(u511,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc11),true,true,true),true) ).
cnf(u1319,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc8),true) ).
cnf(u1928,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,agent(X0,skc11,skc10),true) ).
cnf(u513,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc8),true,true,true),true) ).
cnf(u797,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skc7),true) ).
cnf(u1167,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relation(X0,skc9),true,true,true),true) ).
cnf(u927,negated_conjecture,
true = ifeq2(unisex(skc6,skc11),true,true,true) ).
cnf(u2243,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skc7,X2),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,ifeq3(desire_want(skc6,X0),true,X1,X2),X2),X2),X2),X2) = X2 ).
cnf(u402,negated_conjecture,
true = ifeq2(dance(skc8,skc7),true,true,true) ).
cnf(u796,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skc10),true) ).
cnf(u1659,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(organism(X0,skc10),true,true,true),true) ).
cnf(u2245,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,ifeq3(desire_want(skc6,X1),true,X0,X2),X2),X2),X2),X2) = X2 ).
cnf(u374,negated_conjecture,
true = ifeq2(dance(skc6,skc11),true,true,true) ).
cnf(u2310,negated_conjecture,
skc8 = ifeq3(theme(skc8,X0,skc8),true,ifeq3(desire_want(skc8,X0),true,skc8,skc8),skc8) ).
cnf(u404,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc7),true) ).
cnf(u11,axiom,
true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u564,negated_conjecture,
true = singleton(skc8,skc10) ).
cnf(u360,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc8),true),tuple(true,true),a,b) ).
cnf(u207,negated_conjecture,
true = nonexistent(skc6,skc7) ).
cnf(u429,negated_conjecture,
b = ifeq(tuple(true,female(skc8,skc7)),tuple(true,true),a,b) ).
cnf(u398,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc7),true,true,true),true) ).
cnf(u1760,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(impartial(X0,skc10),true,true,true),true) ).
cnf(u13,axiom,
true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u354,negated_conjecture,
b = ifeq(tuple(true,female(skc6,skc8)),tuple(true,true),a,b) ).
cnf(u193,negated_conjecture,
true = event(skc6,skc7) ).
cnf(u1860,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(animate(X0,skc10),true,true,true),true) ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u196,negated_conjecture,
true = ifeq2(dance(skc6,skc7),true,true,true) ).
cnf(u544,negated_conjecture,
true = singleton(skc8,skc8) ).
cnf(u1985,negated_conjecture,
true = theme(skc8,skc7,skc8) ).
cnf(u364,negated_conjecture,
b = ifeq(tuple(nonhuman(skc6,skc10),true),tuple(true,true),a,b) ).
cnf(u356,negated_conjecture,
b = ifeq(tuple(unisex(skc6,skc10),true),tuple(true,true),a,b) ).
cnf(u551,negated_conjecture,
true = ifeq2(abstraction(skc8,skc9),true,true,true) ).
cnf(u1628,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,human_person(X0,skc10),true) ).
cnf(u275,negated_conjecture,
true = general(skc6,skc9) ).
cnf(u2244,negated_conjecture,
ifeq3(theme(skc8,skc7,X0),true,ifeq3(theme(skc8,X1,X2),true,ifeq3(proposition(skc8,X0),true,ifeq3(proposition(skc8,X2),true,ifeq3(desire_want(skc8,X1),true,X0,X2),X2),X2),X2),X2) = X2 ).
cnf(u312,negated_conjecture,
true = thing(skc6,skc10) ).
cnf(u1440,negated_conjecture,
true = forename(skc8,skc9) ).
cnf(u467,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,eventuality(X0,skc7),true) ).
cnf(u273,negated_conjecture,
true = thing(skc6,skc9) ).
cnf(u145,negated_conjecture,
true = present(skc6,skc7) ).
cnf(u799,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc11),true) ).
cnf(u469,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc11),true) ).
cnf(u938,negated_conjecture,
b = ifeq(tuple(true,female(skc8,skc8)),tuple(true,true),a,b) ).
cnf(u553,negated_conjecture,
true = ifeq2(eventuality(skc8,skc9),true,true,true) ).
cnf(u308,negated_conjecture,
true = ifeq2(entity(skc8,skc11),true,true,true) ).
cnf(u1580,negated_conjecture,
true = entity(skc8,skc10) ).
cnf(u811,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc10),true,true,true),true) ).
cnf(u1571,negated_conjecture,
true = animate(skc8,skc10) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP023-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:48:47 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/0.49 % (57168)Will run a generic schedule for satisfiability detection.
% 0.35/0.49 % (57177)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=734757726:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.35/0.49 % (57176)% WARNING: option uhcvi not known.
% 0.35/0.49 % (57175)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3292535638_2999 on theBenchmark for (2999ds/0Mi)
% 0.35/0.49 % (57178)dis+10_1_sil=32000:sp=arity:random_seed=263235539:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.35/0.49 % (57179)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=950841332:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.35/0.49 % (57182)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1418498368:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.35/0.49 % (57180)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1412114746:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.35/0.49 % (57176)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=806006057:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.35/0.49 % TRYING [1]
% 0.35/0.49 % TRYING [2]
% 0.35/0.49 % TRYING [3]
% 0.35/0.49 % (57177) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-57168-57177"...
% 0.35/0.49 % (57177)...printing done.
% 0.35/0.49 % SZS status Satisfiable for theBenchmark
% 0.35/0.49 % SZS output start Saturation.
% See solution above
% 0.35/0.50 % SZS output start Definitions and Model Updates.
% 0.35/0.50 % SZS output end Definitions and Model Updates.
% 0.35/0.50 % (57177)------------------------------
% 0.35/0.50 % (57177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.35/0.50 % (57177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.35/0.50 % (57177)CaDiCaL version: 2.1.3
% 0.35/0.50 % (57177)Termination reason: Satisfiable
% 0.35/0.50 % (57177)Time elapsed: 0.055 s
% 0.35/0.50 % (57177)Peak memory usage: 13 MB
% 0.35/0.50 % (57177)Instructions burned: 169 (million)
% 0.35/0.50 % (57168)Success in time 0.074 s
% 0.35/0.50 % Vampire exiting
%------------------------------------------------------------------------------