%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP024-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:01 PM UTC 2026
% Result : Satisfiable 9.97s 2.23s
% Output : Saturation 10.27s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u661,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc11),true) ).
cnf(u2524,negated_conjecture,
skc10 = ifeq4(theme(skc8,X1,X0),true,ifeq4(proposition(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,X0,skc10),skc10),skc10) ).
cnf(u248,axiom,
tuple(true,true,true,true,true,true,true,true,true,true) = sF19 ).
cnf(u659,negated_conjecture,
true = ifeq3(eventuality(skc10,skc11),true,true,true) ).
cnf(u2206,negated_conjecture,
true = ifeq3(agent(X0,skc9,skc12),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u524,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(event(X0,skc9),true,true,true),true) ).
cnf(u1294,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,abstraction(X0,skc11),true) ).
cnf(u456,negated_conjecture,
true = specific(skc8,skc15) ).
cnf(u556,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(eventuality(X0,skc9),true,true,true),true) ).
cnf(u1675,negated_conjecture,
b = ifeq2(tuple2(unisex(skc10,skc12),true),tuple2(true,true),a,b) ).
cnf(u406,negated_conjecture,
true = ifeq3(entity(skc10,skc13),true,true,true) ).
cnf(u32,axiom,
true = ifeq3(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u1664,negated_conjecture,
true = human_person(skc10,skc12) ).
cnf(u535,negated_conjecture,
true = ifeq3(entity(skc10,skc9),true,true,true) ).
cnf(u1298,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,abstraction(X0,skc11),true) ).
cnf(u1681,negated_conjecture,
true = living(skc10,skc12) ).
cnf(u803,negated_conjecture,
true = specific(skc10,skc15) ).
cnf(u1821,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(entity(X0,skc12),true,true,true),true) ).
cnf(u912,negated_conjecture,
true = ifeq3(nonexistent(skc8,skc13),true,true,true) ).
cnf(u2458,negated_conjecture,
skc11 = ifeq4(of(skc8,skc11,X0),true,ifeq4(of(skc8,skc11,X0),true,ifeq4(entity(skc8,X0),true,skc11,skc11),skc11),skc11) ).
cnf(u404,negated_conjecture,
true = entity(skc8,skc12) ).
cnf(u38,axiom,
true = ifeq3(mia_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u538,negated_conjecture,
true = singleton(skc10,skc9) ).
cnf(u1825,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,entity(X0,skc15),true) ).
cnf(u316,negated_conjecture,
true = unisex(skc10,skc13) ).
cnf(u1715,negated_conjecture,
true = ifeq3(human_person(skc8,X0),true,human_person(skc10,X0),true) ).
cnf(u1077,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc11),true,true,true),true) ).
cnf(u1058,negated_conjecture,
b = ifeq2(tuple2(true,male(skc10,skc10)),tuple2(true,true),a,b) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u2887,negated_conjecture,
ifeq4(theme(skc10,skc9,X1),true,ifeq4(theme(skc10,skc9,X0),true,ifeq4(proposition(skc10,X1),true,ifeq4(proposition(skc10,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u1967,negated_conjecture,
true = ifeq3(living(skc8,X0),true,living(skc10,X0),true) ).
cnf(u306,negated_conjecture,
true = eventuality(skc10,skc13) ).
cnf(u2361,negated_conjecture,
skc11 = ifeq4(of(skc8,skc14,skc12),true,skc14,skc11) ).
cnf(u444,negated_conjecture,
true = human(skc8,skc15) ).
cnf(u703,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc9),true,true,true),true) ).
cnf(u2163,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(male(X0,skc15),true,true,true),true) ).
cnf(u2594,negated_conjecture,
ifeq4(of(skc8,skc14,skc12),true,ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X0),true,skc14,X0),X0),X0) = X0 ).
cnf(u2148,negated_conjecture,
true = man(skc10,skc15) ).
cnf(u1087,negated_conjecture,
b = ifeq(tuple(dance(skc10,skc9),true,true,true,true,true,true,agent(skc10,skc9,skc15),agent(skc8,skc9,skc15),true),sF19,a,b) ).
cnf(u434,negated_conjecture,
true = ifeq3(vincent_forename(skc8,skc11),true,true,true) ).
cnf(u1710,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human_person(X0,skc15),true,true,true),true) ).
cnf(u78,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(specific(X0,X2),true,specific(X1,X2),true),true) ).
cnf(u368,negated_conjecture,
true = abstraction(skc8,skc11) ).
cnf(u2145,negated_conjecture,
true = ifeq3(man(skc8,X0),true,man(skc10,X0),true) ).
cnf(u432,negated_conjecture,
true = female(skc8,skc12) ).
cnf(u1215,negated_conjecture,
true = abstraction(skc10,skc10) ).
cnf(u76,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(singleton(X0,X2),true,singleton(X1,X2),true),true) ).
cnf(u706,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc9),true) ).
cnf(u323,negated_conjecture,
true = ifeq3(dance(skc8,skc9),true,true,true) ).
cnf(u1222,negated_conjecture,
b = ifeq2(tuple2(specific(skc10,skc10),true),tuple2(true,true),a,b) ).
cnf(u461,negated_conjecture,
true = singleton(skc8,skc15) ).
cnf(u712,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc9),true) ).
cnf(u2007,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human(X0,skc12),true,true,true),true) ).
cnf(u346,negated_conjecture,
true = ifeq3(eventuality(skc8,skc10),true,true,true) ).
cnf(u66,axiom,
true = ifeq3(man(X0,X1),true,male(X0,X1),true) ).
cnf(u204,negated_conjecture,
true = sF4 ).
cnf(u1245,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,relation(X0,skc10),true) ).
cnf(u1477,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,general(X0,skc10),true) ).
cnf(u1220,negated_conjecture,
true = general(skc10,skc10) ).
cnf(u451,negated_conjecture,
true = living(skc8,skc15) ).
cnf(u2261,negated_conjecture,
true = of(skc10,skc11,skc12) ).
cnf(u344,negated_conjecture,
true = thing(skc8,skc10) ).
cnf(u474,negated_conjecture,
b = ifeq2(tuple2(true,female(skc8,skc9)),tuple2(true,true),a,b) ).
cnf(u116,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(living(X0,X2),true,living(X1,X2),true),true) ).
cnf(u1481,negated_conjecture,
true = ifeq3(general(skc8,X0),true,general(skc10,X0),true) ).
cnf(u1389,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,nonhuman(X0,skc14),true) ).
cnf(u363,negated_conjecture,
true = ifeq3(relname(skc8,skc10),true,true,true) ).
cnf(u1262,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,relation(X0,skc14),true) ).
cnf(u716,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc10),true) ).
cnf(u2262,negated_conjecture,
true = ifeq3(of(X0,skc11,skc12),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u472,negated_conjecture,
b = ifeq2(tuple2(true,female(skc8,skc10)),tuple2(true,true),a,b) ).
cnf(u106,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(human_person(X0,X2),true,human_person(X1,X2),true),true) ).
cnf(u1393,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,nonhuman(X0,skc10),true) ).
cnf(u2457,negated_conjecture,
skc11 = ifeq4(of(skc8,skc14,X0),true,ifeq4(of(skc8,skc11,X0),true,ifeq4(entity(skc8,X0),true,skc14,skc11),skc11),skc11) ).
cnf(u2012,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,human(X0,skc12),true) ).
cnf(u622,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc9),true) ).
cnf(u1639,negated_conjecture,
true = mia_forename(skc10,skc11) ).
cnf(u2010,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,human(X0,skc12),true) ).
cnf(u1260,negated_conjecture,
true = ifeq3(proposition(skc10,skc14),true,true,true) ).
cnf(u491,negated_conjecture,
b = ifeq2(tuple2(true,existent(skc10,skc13)),tuple2(true,true),a,b) ).
cnf(u517,negated_conjecture,
true = event(skc10,skc9) ).
cnf(u256,negated_conjecture,
true = forename(skc8,skc11) ).
cnf(u478,negated_conjecture,
b = ifeq2(tuple2(true,general(skc8,skc9)),tuple2(true,true),a,b) ).
cnf(u104,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(woman(X0,X2),true,woman(X1,X2),true),true) ).
cnf(u2799,negated_conjecture,
ifeq4(theme(skc8,skc9,X1),true,ifeq4(theme(skc8,skc9,X0),true,ifeq4(proposition(skc8,X1),true,ifeq4(proposition(skc8,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u234,negated_conjecture,
true = sF14 ).
cnf(u1753,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,organism(X0,skc15),true) ).
cnf(u1264,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relation(X0,skc11),true,true,true),true) ).
cnf(u1044,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc13),true) ).
cnf(u489,negated_conjecture,
b = ifeq2(tuple2(true,male(skc8,skc12)),tuple2(true,true),a,b) ).
cnf(u1659,negated_conjecture,
true = woman(skc10,skc12) ).
cnf(u262,negated_conjecture,
true = forename(skc8,skc14) ).
cnf(u645,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc10),true) ).
cnf(u2302,negated_conjecture,
ifeq4(of(skc8,X1,skc12),true,ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X1),true,ifeq4(forename(skc8,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u1537,negated_conjecture,
true = ifeq3(forename(skc8,X0),true,forename(skc10,X0),true) ).
cnf(u643,negated_conjecture,
true = ifeq3(eventuality(skc10,skc10),true,true,true) ).
cnf(u534,negated_conjecture,
true = unisex(skc10,skc9) ).
cnf(u2557,negated_conjecture,
skc10 = ifeq4(theme(skc10,skc9,X0),true,ifeq4(proposition(skc10,X0),true,X0,skc10),skc10) ).
cnf(clause72,axiom,
ifeq4(of(X0,X1,X2),true,ifeq4(of(X0,X3,X2),true,ifeq4(entity(X0,X2),true,ifeq4(forename(X0,X1),true,ifeq4(forename(X0,X3),true,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u273,negated_conjecture,
b = ifeq(tuple(dance(skc10,X1),event(skc10,X1),desire_want(skc8,X0),true,true,present(skc10,X1),present(skc8,X0),agent(skc10,X1,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc10)),sF19,a,b) ).
cnf(u260,negated_conjecture,
true = desire_want(skc8,skc9) ).
cnf(u789,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc9),true,true,true),true) ).
cnf(u16,axiom,
true = ifeq3(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u1091,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,present(X0,skc9),true) ).
cnf(u2255,negated_conjecture,
true = ifeq3(of(X0,skc11,skc12),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u662,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc12),true,true,true),true) ).
cnf(u1573,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,relname(X0,skc11),true) ).
cnf(u1534,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(forename(X0,skc14),true,true,true),true) ).
cnf(u1679,negated_conjecture,
true = entity(skc10,skc12) ).
cnf(u1554,negated_conjecture,
true = relname(skc10,skc14) ).
cnf(u1571,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relname(X0,skc11),true,true,true),true) ).
cnf(u22,axiom,
true = ifeq3(proposition(X0,X1),true,relation(X0,X1),true) ).
cnf(u2006,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human(X0,skc15),true,true,true),true) ).
cnf(u802,negated_conjecture,
true = ifeq3(specific(skc8,skc13),true,true,true) ).
cnf(u2230,negated_conjecture,
true = ifeq3(theme(skc8,X1,X0),true,theme(skc10,X1,X0),true) ).
cnf(u808,negated_conjecture,
b = ifeq2(tuple2(true,general(skc10,skc15)),tuple2(true,true),a,b) ).
cnf(u1823,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(entity(X0,skc12),true,true,true),true) ).
cnf(u2201,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,agent(X0,skc9,skc12),true) ).
cnf(u1061,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc10),true) ).
cnf(u559,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,eventuality(X0,skc13),true) ).
cnf(u2097,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,female(X0,skc12),true) ).
cnf(u1042,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc10),true) ).
cnf(u2459,negated_conjecture,
skc11 = ifeq4(of(skc8,X0,skc15),true,ifeq4(of(skc8,skc11,skc15),true,ifeq4(forename(skc8,X0),true,X0,skc11),skc11),skc11) ).
cnf(u319,negated_conjecture,
true = event(skc8,skc9) ).
cnf(u656,negated_conjecture,
true = ifeq3(entity(skc10,skc11),true,true,true) ).
cnf(u673,negated_conjecture,
true = ifeq3(abstraction(skc10,skc15),true,true,true) ).
cnf(u428,negated_conjecture,
true = human(skc8,skc12) ).
cnf(u62,axiom,
true = ifeq3(vincent_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u806,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc15),true,true,true),true) ).
cnf(u286,negated_conjecture,
b = ifeq(tuple(dance(skc10,X0),event(skc10,X0),true,true,true,present(skc10,X0),true,agent(skc10,X0,skc15),agent(skc8,skc9,skc15),true),sF19,a,b) ).
cnf(u562,negated_conjecture,
true = ifeq3(eventuality(skc8,skc13),true,true,true) ).
cnf(u1888,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(impartial(X0,skc15),true,true,true),true) ).
cnf(u812,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc12),true,true,true),true) ).
cnf(u817,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc12),true) ).
cnf(u60,axiom,
true = ifeq3(woman(X0,X1),true,female(X0,X1),true) ).
cnf(u1041,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc11),true) ).
cnf(u445,negated_conjecture,
true = animate(skc8,skc15) ).
cnf(u696,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc11),true,true,true),true) ).
cnf(u2119,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,vincent_forename(X0,skc14),true) ).
cnf(u50,axiom,
true = ifeq3(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u1080,negated_conjecture,
b = ifeq2(tuple2(true,male(skc10,skc11)),tuple2(true,true),a,b) ).
cnf(u1204,negated_conjecture,
true = ifeq3(proposition(skc8,X0),true,proposition(skc10,X0),true) ).
cnf(u387,negated_conjecture,
true = unisex(skc8,skc14) ).
cnf(u330,negated_conjecture,
true = specific(skc8,skc9) ).
cnf(u2162,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(male(X0,skc15),true,true,true),true) ).
cnf(u178,axiom,
b = ifeq2(tuple2(unisex(X0,X1),female(X0,X1)),tuple2(true,true),a,b) ).
cnf(u614,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc9),true,true,true),true) ).
cnf(u213,negated_conjecture,
true = sF7 ).
cnf(u1208,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(proposition(X0,skc10),true,true,true),true) ).
cnf(u2118,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(vincent_forename(X0,skc14),true,true,true),true) ).
cnf(u2391,negated_conjecture,
skc14 = ifeq4(of(skc10,skc11,skc15),true,skc11,skc14) ).
cnf(u458,negated_conjecture,
true = ifeq3(abstraction(skc8,skc15),true,true,true) ).
cnf(u100,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(relname(X0,X2),true,relname(X1,X2),true),true) ).
cnf(u1868,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(existent(X0,skc15),true,true,true),true) ).
cnf(u1219,negated_conjecture,
true = nonhuman(skc10,skc10) ).
cnf(u2914,negated_conjecture,
skc10 = ifeq4(theme(skc10,skc9,X0),true,ifeq4(theme(skc10,X1,skc10),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,X0,skc10),skc10),skc10),skc10) ).
cnf(u201,negated_conjecture,
true = sF3 ).
cnf(u2396,negated_conjecture,
skc11 = ifeq4(of(skc10,skc14,skc12),true,skc14,skc11) ).
cnf(u347,negated_conjecture,
true = singleton(skc8,skc10) ).
cnf(u1246,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,relation(X0,skc14),true) ).
cnf(u334,negated_conjecture,
true = relation(skc8,skc10) ).
cnf(u717,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc15),true) ).
cnf(u1872,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,existent(X0,skc12),true) ).
cnf(u2655,negated_conjecture,
skc11 = ifeq4(of(skc10,skc11,skc15),true,ifeq4(of(skc10,skc11,skc15),true,skc11,skc11),skc11) ).
cnf(u90,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(relation(X0,X2),true,relation(X1,X2),true),true) ).
cnf(u715,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc13),true) ).
cnf(u2415,negated_conjecture,
skc14 = ifeq4(of(skc8,skc14,X0),true,ifeq4(of(skc8,skc14,X0),true,ifeq4(entity(skc8,X0),true,skc14,skc14),skc14),skc14) ).
cnf(u207,negated_conjecture,
true = sF5 ).
cnf(u612,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc12),true,true,true),true) ).
cnf(u475,negated_conjecture,
b = ifeq2(tuple2(true,female(skc8,skc14)),tuple2(true,true),a,b) ).
cnf(u1731,negated_conjecture,
b = ifeq2(tuple2(nonhuman(skc10,skc15),true),tuple2(true,true),a,b) ).
cnf(u88,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(proposition(X0,X2),true,proposition(X1,X2),true),true) ).
cnf(u1383,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonhuman(X0,skc11),true,true,true),true) ).
cnf(u1737,negated_conjecture,
true = living(skc10,skc15) ).
cnf(u1248,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,relation(X0,skc10),true) ).
cnf(u1536,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,forename(X0,skc11),true) ).
cnf(u1751,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,organism(X0,skc15),true) ).
cnf(u473,negated_conjecture,
b = ifeq2(tuple2(true,female(skc8,skc11)),tuple2(true,true),a,b) ).
cnf(u2156,negated_conjecture,
b = ifeq2(tuple2(unisex(skc10,skc15),true),tuple2(true,true),a,b) ).
cnf(u1643,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,mia_forename(X0,skc11),true) ).
cnf(u2680,negated_conjecture,
skc14 = ifeq4(of(skc10,skc14,X0),true,ifeq4(of(skc10,skc14,X0),true,ifeq4(entity(skc10,X0),true,skc14,skc14),skc14),skc14) ).
cnf(u216,negated_conjecture,
true = sF8 ).
cnf(u2530,negated_conjecture,
skc10 = ifeq4(theme(skc8,skc9,X0),true,ifeq4(proposition(skc8,X0),true,X0,skc10),skc10) ).
cnf(u2036,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,animate(X0,skc12),true) ).
cnf(u2257,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,of(X0,skc11,skc12),true) ).
cnf(u1390,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,nonhuman(X0,skc10),true) ).
cnf(u2034,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(animate(X0,skc15),true,true,true),true) ).
cnf(u257,negated_conjecture,
true = mia_forename(skc8,skc11) ).
cnf(u479,negated_conjecture,
b = ifeq2(tuple2(true,general(skc8,skc12)),tuple2(true,true),a,b) ).
cnf(u1754,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,organism(X0,skc12),true) ).
cnf(u617,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc9),true) ).
cnf(u1295,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,abstraction(X0,skc14),true) ).
cnf(u631,negated_conjecture,
true = ifeq3(thing(skc8,skc13),true,true,true) ).
cnf(u1394,negated_conjecture,
true = ifeq3(nonhuman(skc8,X0),true,nonhuman(skc10,X0),true) ).
cnf(u669,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc12),true) ).
cnf(u2299,negated_conjecture,
ifeq4(of(skc10,X1,skc15),true,ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X1),true,ifeq4(forename(skc10,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u646,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc14),true,true,true),true) ).
cnf(u1557,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relname(X0,skc14),true,true,true),true) ).
cnf(u263,negated_conjecture,
true = vincent_forename(skc8,skc14) ).
cnf(u385,negated_conjecture,
true = nonhuman(skc8,skc14) ).
cnf(u1555,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,forename(X0,skc14),true) ).
cnf(u500,negated_conjecture,
true = ifeq3(accessible_world(skc10,skc10),true,true,true) ).
cnf(u6,axiom,
true = ifeq3(dance(X0,X1),true,event(X0,X1),true) ).
cnf(u128,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(male(X0,X2),true,male(X1,X2),true),true) ).
cnf(u692,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc15),true,true,true),true) ).
cnf(u634,negated_conjecture,
true = thing(skc10,skc11) ).
cnf(u1302,negated_conjecture,
b = ifeq2(tuple2(true,human(skc10,skc11)),tuple2(true,true),a,b) ).
cnf(u1685,negated_conjecture,
true = existent(skc10,skc12) ).
cnf(u792,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(specific(X0,skc15),true,true,true),true) ).
cnf(u261,negated_conjecture,
true = present(skc8,skc9) ).
cnf(u512,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,event(X0,skc13),true) ).
cnf(u1666,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,woman(X0,skc12),true) ).
cnf(u2297,negated_conjecture,
ifeq4(of(skc8,skc14,X1),true,ifeq4(of(skc8,X0,X1),true,ifeq4(entity(skc8,X1),true,ifeq4(forename(skc8,X0),true,skc14,X0),X0),X0),X0) = X0 ).
cnf(u1683,negated_conjecture,
b = ifeq2(tuple2(nonhuman(skc10,skc12),true),tuple2(true,true),a,b) ).
cnf(u1164,negated_conjecture,
true = desire_want(skc10,skc9) ).
cnf(u134,axiom,
true = ifeq3(of(X0,X1,X2),true,ifeq3(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).
cnf(u1045,negated_conjecture,
true = ifeq3(unisex(skc8,X0),true,unisex(skc10,X0),true) ).
cnf(u1672,negated_conjecture,
true = human(skc10,skc12) ).
cnf(u543,negated_conjecture,
b = ifeq2(tuple2(true,male(skc10,skc9)),tuple2(true,true),a,b) ).
cnf(u481,negated_conjecture,
b = ifeq2(tuple2(specific(skc8,skc10),true),tuple2(true,true),a,b) ).
cnf(u1300,negated_conjecture,
true = ifeq3(abstraction(skc8,X0),true,abstraction(skc10,X0),true) ).
cnf(u1829,negated_conjecture,
true = ifeq3(entity(skc8,X0),true,entity(skc10,X0),true) ).
cnf(u2336,negated_conjecture,
skc11 = ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X0),true,X0,skc11),skc11) ).
cnf(u389,negated_conjecture,
true = ifeq3(mia_forename(skc8,skc14),true,true,true) ).
cnf(u640,negated_conjecture,
true = ifeq3(entity(skc10,skc10),true,true,true) ).
cnf(u2298,negated_conjecture,
ifeq4(of(skc8,skc11,X1),true,ifeq4(of(skc8,X0,X1),true,ifeq4(entity(skc8,X1),true,ifeq4(forename(skc8,X0),true,skc11,X0),X0),X0),X0) = X0 ).
cnf(u274,negated_conjecture,
b = ifeq(tuple(dance(X0,X1),event(X0,X1),true,proposition(skc8,X0),accessible_world(skc8,X0),present(X0,X1),true,agent(X0,X1,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,X0)),sF19,a,b) ).
cnf(u412,negated_conjecture,
true = ifeq3(abstraction(skc8,skc12),true,true,true) ).
cnf(u1827,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,entity(X0,skc15),true) ).
cnf(u46,axiom,
true = ifeq3(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u132,axiom,
true = ifeq3(theme(X0,X1,X2),true,ifeq3(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).
cnf(u790,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(specific(X0,skc9),true,true,true),true) ).
cnf(u546,negated_conjecture,
true = ifeq3(accessible_world(skc8,skc8),true,true,true) ).
cnf(u796,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc9),true) ).
cnf(u2342,negated_conjecture,
ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X0),true,skc14,X0),X0) = X0 ).
cnf(u1055,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc10),true,true,true),true) ).
cnf(u402,negated_conjecture,
true = organism(skc8,skc12) ).
cnf(u711,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc14),true) ).
cnf(u44,axiom,
true = ifeq3(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u1085,negated_conjecture,
true = ifeq3(present(skc8,skc13),true,true,true) ).
cnf(u2200,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,agent(X0,skc13,skc12),true) ).
cnf(u1961,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(living(X0,skc12),true,true,true),true) ).
cnf(u541,negated_conjecture,
b = ifeq2(tuple2(true,existent(skc10,skc9)),tuple2(true,true),a,b) ).
cnf(u2096,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(female(X0,skc12),true,true,true),true) ).
cnf(u2231,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,theme(X0,skc9,skc10),true) ).
cnf(u314,negated_conjecture,
true = nonexistent(skc10,skc13) ).
cnf(u400,negated_conjecture,
true = human_person(skc8,skc12) ).
cnf(u34,axiom,
true = ifeq3(forename(X0,X1),true,relname(X0,X1),true) ).
cnf(u1075,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,present(X0,skc9),true) ).
cnf(u2295,negated_conjecture,
ifeq4(of(skc10,skc11,X1),true,ifeq4(of(skc10,X0,X1),true,ifeq4(entity(skc10,X1),true,ifeq4(forename(skc10,X0),true,skc11,X0),X0),X0),X0) = X0 ).
cnf(u1213,negated_conjecture,
true = ifeq3(relname(skc10,skc10),true,true,true) ).
cnf(u1665,negated_conjecture,
true = female(skc10,skc12) ).
cnf(u1064,negated_conjecture,
b = ifeq2(tuple2(true,female(skc10,skc14)),tuple2(true,true),a,b) ).
cnf(u419,negated_conjecture,
true = specific(skc8,skc12) ).
cnf(u2229,negated_conjecture,
true = ifeq3(theme(X0,skc9,skc10),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u312,negated_conjecture,
true = specific(skc10,skc13) ).
cnf(u442,negated_conjecture,
true = ifeq3(woman(skc8,skc15),true,true,true) ).
cnf(u1203,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,proposition(X0,skc10),true) ).
cnf(u2504,negated_conjecture,
skc10 = ifeq4(theme(skc8,X2,X1),true,ifeq4(theme(skc8,X0,skc10),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X2),true,ifeq4(desire_want(skc8,X0),true,X1,skc10),skc10),skc10),skc10),skc10) ).
cnf(u1076,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,present(X0,skc13),true) ).
cnf(u318,negated_conjecture,
true = ifeq3(desire_want(skc10,skc13),true,true,true) ).
cnf(u701,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc12),true,true,true),true) ).
cnf(u84,axiom,
true = ifeq3(present(X0,X1),true,ifeq3(accessible_world(X0,X2),true,present(X2,X1),true),true) ).
cnf(u699,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc15),true,true,true),true) ).
cnf(u2125,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(vincent_forename(X0,skc14),true,true,true),true) ).
cnf(u331,negated_conjecture,
true = nonexistent(skc8,skc9) ).
cnf(u2639,negated_conjecture,
skc11 = ifeq4(of(skc10,X0,skc15),true,ifeq4(of(skc10,skc11,skc15),true,ifeq4(forename(skc10,X0),true,X0,skc11),skc11),skc11) ).
cnf(u74,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(thing(X0,X2),true,thing(X1,X2),true),true) ).
cnf(u2637,negated_conjecture,
skc11 = ifeq4(of(skc10,skc11,X0),true,ifeq4(of(skc10,skc11,X0),true,ifeq4(entity(skc10,X0),true,skc11,skc11),skc11),skc11) ).
cnf(u329,negated_conjecture,
true = thing(skc8,skc9) ).
cnf(u1886,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(impartial(X0,skc15),true,true,true),true) ).
cnf(u613,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc11),true,true,true),true) ).
cnf(u2501,negated_conjecture,
ifeq4(theme(skc10,skc9,X2),true,ifeq4(theme(skc10,X1,X0),true,ifeq4(proposition(skc10,X2),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,X2,X0),X0),X0),X0),X0) = X0 ).
cnf(u72,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).
cnf(u1892,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,impartial(X0,skc12),true) ).
cnf(u611,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc10),true,true,true),true) ).
cnf(u1475,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,general(X0,skc11),true) ).
cnf(u718,negated_conjecture,
true = ifeq3(singleton(skc8,X0),true,singleton(skc10,X0),true) ).
cnf(u1890,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,impartial(X0,skc12),true) ).
cnf(u1735,negated_conjecture,
true = entity(skc10,skc15) ).
cnf(u457,negated_conjecture,
true = existent(skc8,skc15) ).
cnf(u2155,negated_conjecture,
b = ifeq2(tuple2(female(skc10,skc15),true),tuple2(true,true),a,b) ).
cnf(u1740,negated_conjecture,
true = existent(skc10,skc15) ).
cnf(u2525,negated_conjecture,
ifeq4(theme(skc10,X1,X0),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,skc10,X0),X0),X0) = X0 ).
cnf(u2888,negated_conjecture,
ifeq4(theme(skc10,X0,skc10),true,ifeq4(theme(skc10,skc9,X1),true,ifeq4(proposition(skc10,X1),true,ifeq4(desire_want(skc10,X0),true,skc10,X1),X1),X1),X1) = X1 ).
cnf(u231,negated_conjecture,
true = sF13 ).
cnf(u636,negated_conjecture,
true = thing(skc10,skc10) ).
cnf(u2268,negated_conjecture,
true = ifeq3(of(X0,skc14,skc15),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u1755,negated_conjecture,
true = ifeq3(organism(skc8,X0),true,organism(skc10,X0),true) ).
cnf(u486,negated_conjecture,
b = ifeq2(tuple2(true,human(skc8,skc14)),tuple2(true,true),a,b) ).
cnf(u112,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(existent(X0,X2),true,existent(X1,X2),true),true) ).
cnf(u615,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc14),true,true,true),true) ).
cnf(u1541,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relname(X0,skc14),true,true,true),true) ).
cnf(u497,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(dance(X0,skc13),true,true,true),true) ).
cnf(u1747,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(organism(X0,skc12),true,true,true),true) ).
cnf(u484,negated_conjecture,
b = ifeq2(tuple2(true,human(skc8,skc10)),tuple2(true,true),a,b) ).
cnf(u2531,negated_conjecture,
skc10 = ifeq4(theme(skc8,X0,skc10),true,ifeq4(desire_want(skc8,X0),true,skc10,skc10),skc10) ).
cnf(u118,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(human(X0,X2),true,human(X1,X2),true),true) ).
cnf(u240,negated_conjecture,
true = sF16 ).
cnf(u1535,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,forename(X0,skc14),true) ).
cnf(u2705,negated_conjecture,
skc14 = ifeq4(of(skc10,skc14,skc12),true,ifeq4(of(skc10,skc14,skc12),true,skc14,skc14),skc14) ).
cnf(u618,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc11),true) ).
cnf(u905,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonexistent(X0,skc9),true,true,true),true) ).
cnf(u219,negated_conjecture,
true = sF9 ).
cnf(u624,negated_conjecture,
true = ifeq3(thing(skc8,X0),true,thing(skc10,X0),true) ).
cnf(u30,axiom,
true = ifeq3(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u513,negated_conjecture,
true = ifeq3(event(skc8,X0),true,event(skc10,X0),true) ).
cnf(u268,negated_conjecture,
true = theme(skc8,skc9,skc10) ).
cnf(u1667,negated_conjecture,
true = ifeq3(man(skc10,skc12),true,true,true) ).
cnf(u1249,negated_conjecture,
true = ifeq3(relation(skc8,X0),true,relation(skc10,X0),true) ).
cnf(u246,negated_conjecture,
true = sF18 ).
cnf(u1290,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(abstraction(X0,skc14),true,true,true),true) ).
cnf(u2033,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(animate(X0,skc12),true,true,true),true) ).
cnf(ifeq_axiom_002,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u501,negated_conjecture,
true = ifeq3(dance(skc8,skc13),true,true,true) ).
cnf(u258,negated_conjecture,
true = proposition(skc8,skc10) ).
cnf(u1033,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc13),true,true,true),true) ).
cnf(u396,negated_conjecture,
true = ifeq3(eventuality(skc8,skc14),true,true,true) ).
cnf(u1686,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc10,skc12),true),tuple2(true,true),a,b) ).
cnf(u2558,negated_conjecture,
skc10 = ifeq4(theme(skc10,X0,skc10),true,ifeq4(desire_want(skc10,X0),true,skc10,skc10),skc10) ).
cnf(u1288,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(abstraction(X0,skc10),true,true,true),true) ).
cnf(u2499,negated_conjecture,
ifeq4(theme(skc10,X2,X1),true,ifeq4(theme(skc10,skc9,X0),true,ifeq4(proposition(skc10,X1),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X2),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(ifeq_axiom,axiom,
ifeq4(X0,X0,X1,X2) = X1 ).
cnf(u471,negated_conjecture,
b = ifeq2(tuple2(true,female(skc10,skc13)),tuple2(true,true),a,b) ).
cnf(u536,negated_conjecture,
true = ifeq3(abstraction(skc10,skc9),true,true,true) ).
cnf(u415,negated_conjecture,
true = singleton(skc8,skc12) ).
cnf(u1039,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc14),true) ).
cnf(u386,negated_conjecture,
true = general(skc8,skc14) ).
cnf(u1161,negated_conjecture,
true = ifeq3(desire_want(skc8,X0),true,desire_want(skc10,X0),true) ).
cnf(u28,axiom,
true = ifeq3(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u1275,negated_conjecture,
true = general(skc10,skc14) ).
cnf(u1301,negated_conjecture,
b = ifeq2(tuple2(specific(skc10,skc14),true),tuple2(true,true),a,b) ).
cnf(u1050,negated_conjecture,
true = ifeq3(unisex(skc8,skc13),true,true,true) ).
cnf(u2337,negated_conjecture,
skc11 = ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X0),true,X0,skc11),skc11) ).
cnf(u908,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,nonexistent(X0,skc9),true) ).
cnf(u1959,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(living(X0,skc12),true,true,true),true) ).
cnf(u384,negated_conjecture,
true = thing(skc8,skc14) ).
cnf(u18,axiom,
true = ifeq3(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u2340,negated_conjecture,
ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X0),true,skc11,X0),X0) = X0 ).
cnf(u814,negated_conjecture,
b = ifeq2(tuple2(true,general(skc10,skc12)),tuple2(true,true),a,b) ).
cnf(u1299,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,abstraction(X0,skc10),true) ).
cnf(u1086,negated_conjecture,
true = present(skc10,skc9) ).
cnf(u557,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,eventuality(X0,skc9),true) ).
cnf(u2208,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,agent(X0,skc9,skc12),true) ).
cnf(u1079,negated_conjecture,
b = ifeq2(tuple2(true,female(skc10,skc11)),tuple2(true,true),a,b) ).
cnf(u426,negated_conjecture,
true = living(skc8,skc12) ).
cnf(u555,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(eventuality(X0,skc9),true,true,true),true) ).
cnf(u668,negated_conjecture,
true = singleton(skc10,skc12) ).
cnf(u424,negated_conjecture,
true = impartial(skc8,skc12) ).
cnf(u1207,negated_conjecture,
true = proposition(skc10,skc10) ).
cnf(u58,axiom,
true = ifeq3(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u1964,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,living(X0,skc12),true) ).
cnf(u2237,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,theme(X0,skc9,skc10),true) ).
cnf(u1962,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(living(X0,skc15),true,true,true),true) ).
cnf(u1212,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,proposition(X0,skc10),true) ).
cnf(u443,negated_conjecture,
true = organism(skc8,skc15) ).
cnf(u430,negated_conjecture,
true = animate(skc8,skc12) ).
cnf(u56,axiom,
true = ifeq3(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u186,axiom,
b = ifeq2(tuple2(nonexistent(X0,X1),existent(X0,X1)),tuple2(true,true),a,b) ).
cnf(u702,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc11),true,true,true),true) ).
cnf(u1718,negated_conjecture,
true = human_person(skc10,skc15) ).
cnf(u1088,negated_conjecture,
b = ifeq(tuple(dance(skc10,skc9),true,desire_want(skc8,X0),true,true,true,present(skc8,X0),agent(skc10,skc9,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc10)),sF19,a,b) ).
cnf(u1870,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(existent(X0,skc15),true,true,true),true) ).
cnf(u336,negated_conjecture,
true = singleton(skc8,skc9) ).
cnf(u184,axiom,
b = ifeq2(tuple2(female(X0,X1),male(X0,X1)),tuple2(true,true),a,b) ).
cnf(u1473,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(general(X0,skc14),true,true,true),true) ).
cnf(u1291,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(abstraction(X0,skc10),true,true,true),true) ).
cnf(u1874,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,existent(X0,skc12),true) ).
cnf(u708,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc12),true) ).
cnf(u342,negated_conjecture,
true = ifeq3(abstraction(skc10,skc13),true,true,true) ).
cnf(u725,negated_conjecture,
true = ifeq3(singleton(skc8,skc13),true,true,true) ).
cnf(u1479,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,general(X0,skc11),true) ).
cnf(u2270,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,of(X0,skc14,skc15),true) ).
cnf(u1741,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc10,skc15),true),tuple2(true,true),a,b) ).
cnf(u620,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc10),true) ).
cnf(u340,negated_conjecture,
true = abstraction(skc8,skc10) ).
cnf(u470,negated_conjecture,
b = ifeq2(tuple2(unisex(skc8,skc15),true),tuple2(true,true),a,b) ).
cnf(u96,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(general(X0,X2),true,general(X1,X2),true),true) ).
cnf(u1391,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,nonhuman(X0,skc14),true) ).
cnf(u1728,negated_conjecture,
true = animate(skc10,skc15) ).
cnf(u1544,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,relname(X0,skc14),true) ).
cnf(u1636,negated_conjecture,
true = ifeq3(mia_forename(skc8,X0),true,mia_forename(skc10,X0),true) ).
cnf(u2267,negated_conjecture,
true = of(skc10,skc14,skc15) ).
cnf(u1885,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(impartial(X0,skc12),true,true,true),true) ).
cnf(u359,negated_conjecture,
true = relname(skc8,skc14) ).
cnf(u1634,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(mia_forename(X0,skc11),true,true,true),true) ).
cnf(u2153,negated_conjecture,
true = male(skc10,skc15) ).
cnf(u2932,negated_conjecture,
skc10 = ifeq4(theme(skc10,X0,skc10),true,ifeq4(theme(skc10,X1,skc10),true,ifeq4(desire_want(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,skc10,skc10),skc10),skc10),skc10) ).
cnf(u713,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc11),true) ).
cnf(u468,negated_conjecture,
b = ifeq2(tuple2(true,male(skc8,skc9)),tuple2(true,true),a,b) ).
cnf(u102,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(mia_forename(X0,X2),true,mia_forename(X1,X2),true),true) ).
cnf(u2143,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(man(X0,skc15),true,true,true),true) ).
cnf(u2258,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,of(X0,skc14,skc15),true) ).
cnf(u1889,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,impartial(X0,skc15),true) ).
cnf(u2013,negated_conjecture,
true = ifeq3(human(skc8,X0),true,human(skc10,X0),true) ).
cnf(u608,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc13),true,true,true),true) ).
cnf(u487,negated_conjecture,
b = ifeq2(tuple2(nonhuman(skc8,skc12),true),tuple2(true,true),a,b) ).
cnf(u2154,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,man(X0,skc15),true) ).
cnf(u1542,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relname(X0,skc11),true,true,true),true) ).
cnf(u2011,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,human(X0,skc15),true) ).
cnf(u1548,negated_conjecture,
true = forename(skc10,skc14) ).
cnf(u1068,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc14),true) ).
cnf(u253,negated_conjecture,
true = woman(skc8,skc12) ).
cnf(u485,negated_conjecture,
b = ifeq2(tuple2(true,human(skc8,skc11)),tuple2(true,true),a,b) ).
cnf(u2031,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(animate(X0,skc12),true,true,true),true) ).
cnf(u370,negated_conjecture,
true = ifeq3(proposition(skc8,skc14),true,true,true) ).
cnf(u14,axiom,
true = ifeq3(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u228,negated_conjecture,
true = sF12 ).
cnf(u1269,negated_conjecture,
true = abstraction(skc10,skc11) ).
cnf(u243,negated_conjecture,
true = sF17 ).
cnf(u449,negated_conjecture,
true = entity(skc8,skc15) ).
cnf(u520,negated_conjecture,
true = ifeq3(dance(skc10,skc9),true,true,true) ).
cnf(u498,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,dance(X0,skc13),true) ).
cnf(u12,axiom,
true = ifeq3(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u1053,negated_conjecture,
true = unisex(skc10,skc11) ).
cnf(u2296,negated_conjecture,
ifeq4(of(skc10,skc14,X1),true,ifeq4(of(skc10,X0,X1),true,ifeq4(entity(skc10,X1),true,ifeq4(forename(skc10,X0),true,skc14,X0),X0),X0),X0) = X0 ).
cnf(u455,negated_conjecture,
true = thing(skc8,skc15) ).
cnf(u1034,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc9),true,true,true),true) ).
cnf(u906,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonexistent(X0,skc9),true,true,true),true) ).
cnf(u259,negated_conjecture,
true = accessible_world(skc8,skc10) ).
cnf(u397,negated_conjecture,
true = singleton(skc8,skc14) ).
cnf(u648,negated_conjecture,
true = ifeq3(entity(skc10,skc14),true,true,true) ).
cnf(u2199,negated_conjecture,
true = ifeq3(agent(skc8,X1,X0),true,agent(skc10,X1,X0),true) ).
cnf(u1057,negated_conjecture,
b = ifeq2(tuple2(true,female(skc10,skc10)),tuple2(true,true),a,b) ).
cnf(u1279,negated_conjecture,
true = general(skc10,skc11) ).
cnf(ifeq_axiom_001,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u1289,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(abstraction(X0,skc11),true,true,true),true) ).
cnf(u1043,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc9),true) ).
cnf(u798,negated_conjecture,
true = ifeq3(specific(skc8,X0),true,specific(skc10,X0),true) ).
cnf(u804,negated_conjecture,
true = specific(skc10,skc12) ).
cnf(u493,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc8,skc12),true),tuple2(true,true),a,b) ).
cnf(u2197,negated_conjecture,
true = ifeq3(agent(X0,skc9,skc12),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u410,negated_conjecture,
true = ifeq3(entity(skc8,skc14),true,true,true) ).
cnf(u52,axiom,
true = ifeq3(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u130,axiom,
true = ifeq3(agent(X0,X1,X2),true,ifeq3(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).
cnf(u2293,negated_conjecture,
skc14 = ifeq4(of(skc8,X1,X0),true,ifeq4(of(skc8,skc14,X0),true,ifeq4(entity(skc8,X0),true,ifeq4(forename(skc8,X1),true,X1,skc14),skc14),skc14),skc14) ).
cnf(u539,negated_conjecture,
b = ifeq2(tuple2(true,general(skc10,skc9)),tuple2(true,true),a,b) ).
cnf(u1160,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,desire_want(X0,skc9),true) ).
cnf(u310,negated_conjecture,
true = singleton(skc10,skc13) ).
cnf(u652,negated_conjecture,
true = singleton(skc10,skc14) ).
cnf(u2198,negated_conjecture,
true = ifeq3(agent(X0,skc13,skc12),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u2341,negated_conjecture,
ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X0),true,skc11,X0),X0) = X0 ).
cnf(u408,negated_conjecture,
true = ifeq3(entity(skc8,skc11),true,true,true) ).
cnf(u42,axiom,
true = ifeq3(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u1083,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc11),true) ).
cnf(u667,negated_conjecture,
true = ifeq3(eventuality(skc10,skc12),true,true,true) ).
cnf(u558,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,eventuality(X0,skc9),true) ).
cnf(u1072,negated_conjecture,
true = ifeq3(present(X0,skc13),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u2099,negated_conjecture,
true = ifeq3(female(skc8,X0),true,female(skc10,X0),true) ).
cnf(u414,negated_conjecture,
true = ifeq3(eventuality(skc8,skc12),true,true,true) ).
cnf(u40,axiom,
true = ifeq3(woman(X0,X1),true,human_person(X0,X1),true) ).
cnf(u707,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc11),true) ).
cnf(u1211,negated_conjecture,
true = relation(skc10,skc10) ).
cnf(u2212,negated_conjecture,
true = ifeq3(agent(skc8,skc13,skc12),true,true,true) ).
cnf(u811,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc15),true) ).
cnf(u2376,negated_conjecture,
skc11 = ifeq4(of(skc8,skc11,skc15),true,skc14,skc11) ).
cnf(u320,negated_conjecture,
b = ifeq(tuple(dance(skc8,skc9),true,true,proposition(skc8,skc8),accessible_world(skc8,skc8),true,true,agent(skc8,skc9,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,skc8)),sF19,a,b) ).
cnf(u2502,negated_conjecture,
ifeq4(theme(skc8,skc9,X2),true,ifeq4(theme(skc8,X1,X0),true,ifeq4(proposition(skc8,X2),true,ifeq4(proposition(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,X2,X0),X0),X0),X0),X0) = X0 ).
cnf(u1244,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relation(X0,skc10),true,true,true),true) ).
cnf(u709,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc10),true) ).
cnf(u2638,negated_conjecture,
skc11 = ifeq4(of(skc10,skc14,X0),true,ifeq4(of(skc10,skc11,X0),true,ifeq4(entity(skc10,X0),true,skc14,skc11),skc11),skc11) ).
cnf(u1712,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,human_person(X0,skc12),true) ).
cnf(u2123,negated_conjecture,
true = vincent_forename(skc10,skc14) ).
cnf(u2254,negated_conjecture,
true = ifeq3(of(X0,skc14,skc15),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u1470,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(general(X0,skc11),true,true,true),true) ).
cnf(u697,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc9),true,true,true),true) ).
cnf(u324,negated_conjecture,
true = eventuality(skc8,skc9) ).
cnf(u2371,negated_conjecture,
skc14 = ifeq4(of(skc8,skc14,skc12),true,skc11,skc14) ).
cnf(u80,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).
cnf(u1729,negated_conjecture,
true = human(skc10,skc15) ).
cnf(u1065,negated_conjecture,
b = ifeq2(tuple2(true,male(skc10,skc14)),tuple2(true,true),a,b) ).
cnf(u1869,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(existent(X0,skc12),true,true,true),true) ).
cnf(u343,negated_conjecture,
true = ifeq3(abstraction(skc8,skc9),true,true,true) ).
cnf(u2506,negated_conjecture,
ifeq4(theme(skc8,X2,skc10),true,ifeq4(theme(skc8,X1,X0),true,ifeq4(proposition(skc8,X0),true,ifeq4(desire_want(skc8,X2),true,ifeq4(desire_want(skc8,X1),true,skc10,X0),X0),X0),X0),X0) = X0 ).
cnf(u465,negated_conjecture,
b = ifeq2(tuple2(true,male(skc10,skc13)),tuple2(true,true),a,b) ).
cnf(u1635,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,mia_forename(X0,skc11),true) ).
cnf(u1089,negated_conjecture,
true = ifeq3(present(X0,skc9),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u1867,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(existent(X0,skc12),true,true,true),true) ).
cnf(u86,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(desire_want(X0,X2),true,desire_want(X1,X2),true),true) ).
cnf(u2127,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,vincent_forename(X0,skc14),true) ).
cnf(u1474,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(general(X0,skc11),true,true,true),true) ).
cnf(u1873,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,existent(X0,skc15),true) ).
cnf(u1748,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(organism(X0,skc15),true,true,true),true) ).
cnf(u1382,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonhuman(X0,skc10),true,true,true),true) ).
cnf(u1887,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(impartial(X0,skc12),true,true,true),true) ).
cnf(u609,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc9),true,true,true),true) ).
cnf(u364,negated_conjecture,
true = relation(skc8,skc11) ).
cnf(u1654,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(woman(X0,skc12),true,true,true),true) ).
cnf(u1752,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,organism(X0,skc12),true) ).
cnf(u623,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc13),true) ).
cnf(u1386,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonhuman(X0,skc14),true,true,true),true) ).
cnf(u1472,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(general(X0,skc10),true,true,true),true) ).
cnf(u1660,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(woman(X0,skc12),true,true,true),true) ).
cnf(u714,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc12),true) ).
cnf(u2523,negated_conjecture,
skc10 = ifeq4(theme(skc10,X1,X0),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,X0,skc10),skc10),skc10) ).
cnf(u237,negated_conjecture,
true = sF15 ).
cnf(u2416,negated_conjecture,
skc14 = ifeq4(of(skc8,skc11,X0),true,ifeq4(of(skc8,skc14,X0),true,ifeq4(entity(skc8,X0),true,skc11,skc14),skc14),skc14) ).
cnf(u469,negated_conjecture,
b = ifeq2(tuple2(true,male(skc8,skc14)),tuple2(true,true),a,b) ).
cnf(u492,negated_conjecture,
b = ifeq2(tuple2(true,existent(skc8,skc9)),tuple2(true,true),a,b) ).
cnf(u126,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(man(X0,X2),true,man(X1,X2),true),true) ).
cnf(u2526,negated_conjecture,
ifeq4(theme(skc8,X0,X1),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X0),true,skc10,X1),X1),X1) = X1 ).
cnf(u1253,negated_conjecture,
true = relation(skc10,skc14) ).
cnf(u1384,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonhuman(X0,skc14),true,true,true),true) ).
cnf(u2037,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,animate(X0,skc15),true) ).
cnf(u632,negated_conjecture,
true = thing(skc10,skc14) ).
cnf(u511,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,event(X0,skc9),true) ).
cnf(u482,negated_conjecture,
b = ifeq2(tuple2(specific(skc8,skc11),true),tuple2(true,true),a,b) ).
cnf(u124,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(vincent_forename(X0,X2),true,vincent_forename(X1,X2),true),true) ).
cnf(u2035,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,animate(X0,skc15),true) ).
cnf(u254,negated_conjecture,
true = present(skc10,skc13) ).
cnf(u1037,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc9),true,true,true),true) ).
cnf(u1243,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relation(X0,skc14),true,true,true),true) ).
cnf(u1292,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(abstraction(X0,skc14),true,true,true),true) ).
cnf(u225,negated_conjecture,
true = sF11 ).
cnf(u371,negated_conjecture,
true = abstraction(skc8,skc14) ).
cnf(u1270,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,relation(X0,skc11),true) ).
cnf(u509,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(event(X0,skc13),true,true,true),true) ).
cnf(u266,negated_conjecture,
true = agent(skc8,skc9,skc12) ).
cnf(u480,negated_conjecture,
b = ifeq2(tuple2(true,general(skc8,skc15)),tuple2(true,true),a,b) ).
cnf(u114,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(impartial(X0,X2),true,impartial(X1,X2),true),true) ).
cnf(u2681,negated_conjecture,
skc14 = ifeq4(of(skc10,X0,skc12),true,ifeq4(of(skc10,skc14,skc12),true,ifeq4(forename(skc10,X0),true,X0,skc14),skc14),skc14) ).
cnf(u252,negated_conjecture,
true = event(skc10,skc13) ).
cnf(u1387,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonhuman(X0,skc11),true,true,true),true) ).
cnf(u1296,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,abstraction(X0,skc10),true) ).
cnf(u1274,negated_conjecture,
true = nonhuman(skc10,skc14) ).
cnf(u2433,negated_conjecture,
skc14 = ifeq4(of(skc8,skc14,skc12),true,ifeq4(of(skc8,skc14,skc12),true,skc14,skc14),skc14) ).
cnf(u788,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc13),true,true,true),true) ).
cnf(u1054,negated_conjecture,
true = unisex(skc10,skc10) ).
cnf(u1268,negated_conjecture,
true = ifeq3(proposition(skc10,skc11),true,true,true) ).
cnf(u499,negated_conjecture,
true = ifeq3(dance(skc8,X0),true,dance(skc10,X0),true) ).
cnf(u525,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,event(X0,skc9),true) ).
cnf(u264,negated_conjecture,
true = of(skc8,skc14,skc15) ).
cnf(u793,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,specific(X0,skc15),true) ).
cnf(u36,axiom,
true = ifeq3(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u910,negated_conjecture,
true = ifeq3(nonexistent(skc8,X0),true,nonexistent(skc10,X0),true) ).
cnf(u2856,negated_conjecture,
skc10 = ifeq4(theme(skc8,X0,skc10),true,ifeq4(theme(skc8,X1,skc10),true,ifeq4(desire_want(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,skc10,skc10),skc10),skc10),skc10) ).
cnf(u653,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc14),true) ).
cnf(u392,negated_conjecture,
true = ifeq3(eventuality(skc8,skc11),true,true,true) ).
cnf(u2294,negated_conjecture,
skc11 = ifeq4(of(skc8,X1,X0),true,ifeq4(of(skc8,skc11,X0),true,ifeq4(entity(skc8,X0),true,ifeq4(forename(skc8,X1),true,X1,skc11),skc11),skc11),skc11) ).
cnf(u26,axiom,
true = ifeq3(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u1545,negated_conjecture,
true = ifeq3(relname(skc8,X0),true,relname(skc10,X0),true) ).
cnf(u651,negated_conjecture,
true = ifeq3(eventuality(skc10,skc14),true,true,true) ).
cnf(u542,negated_conjecture,
b = ifeq2(tuple2(true,female(skc10,skc9)),tuple2(true,true),a,b) ).
cnf(u2205,negated_conjecture,
true = agent(skc10,skc9,skc12) ).
cnf(u1559,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,relname(X0,skc14),true) ).
cnf(u281,negated_conjecture,
b = ifeq(tuple(true,true,true,true,true,true,true,agent(skc10,skc13,skc15),agent(skc8,skc9,skc15),true),sF19,a,b) ).
cnf(u255,negated_conjecture,
true = dance(skc10,skc13) ).
cnf(u411,negated_conjecture,
true = thing(skc8,skc12) ).
cnf(u2838,negated_conjecture,
skc10 = ifeq4(theme(skc8,skc9,X0),true,ifeq4(theme(skc8,X1,skc10),true,ifeq4(proposition(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,X0,skc10),skc10),skc10),skc10) ).
cnf(u797,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc13),true) ).
cnf(u24,axiom,
true = ifeq3(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u2338,negated_conjecture,
skc14 = ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X0),true,X0,skc14),skc14) ).
cnf(u1673,negated_conjecture,
true = animate(skc10,skc12) ).
cnf(u795,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,specific(X0,skc9),true) ).
cnf(u670,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc15),true,true,true),true) ).
cnf(clause73,axiom,
ifeq4(theme(X0,X1,X2),true,ifeq4(theme(X0,X3,X4),true,ifeq4(proposition(X0,X2),true,ifeq4(proposition(X0,X4),true,ifeq4(desire_want(X0,X1),true,ifeq4(desire_want(X0,X3),true,X2,X4),X4),X4),X4),X4),X4) = X4 ).
cnf(u904,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonexistent(X0,skc13),true,true,true),true) ).
cnf(u1562,negated_conjecture,
true = forename(skc10,skc11) ).
cnf(u409,negated_conjecture,
true = ifeq3(entity(skc8,skc9),true,true,true) ).
cnf(u676,negated_conjecture,
true = singleton(skc10,skc15) ).
cnf(u1966,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,living(X0,skc12),true) ).
cnf(u693,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc10),true,true,true),true) ).
cnf(u2616,negated_conjecture,
ifeq4(of(skc8,skc11,skc15),true,ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X0),true,skc11,X0),X0),X0) = X0 ).
cnf(u1568,negated_conjecture,
true = relname(skc10,skc11) ).
cnf(u1709,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human_person(X0,skc12),true,true,true),true) ).
cnf(u1469,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(general(X0,skc10),true,true,true),true) ).
cnf(u308,negated_conjecture,
true = thing(skc10,skc13) ).
cnf(u438,negated_conjecture,
true = human_person(skc8,skc15) ).
cnf(u2744,negated_conjecture,
ifeq4(of(skc10,skc14,skc12),true,ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X0),true,skc14,X0),X0),X0) = X0 ).
cnf(u2098,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,female(X0,skc12),true) ).
cnf(u1713,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,human_person(X0,skc15),true) ).
cnf(u2235,negated_conjecture,
true = ifeq3(theme(X0,skc9,skc10),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).
cnf(u1727,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,human_person(X0,skc15),true) ).
cnf(u321,negated_conjecture,
b = ifeq(tuple(dance(skc8,skc9),true,desire_want(skc8,X0),proposition(skc8,skc8),accessible_world(skc8,skc8),true,present(skc8,X0),agent(skc8,skc9,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc8)),sF19,a,b) ).
cnf(u349,negated_conjecture,
true = nonhuman(skc8,skc10) ).
cnf(u2483,negated_conjecture,
skc11 = ifeq4(of(skc8,skc11,skc15),true,ifeq4(of(skc8,skc11,skc15),true,skc11,skc11),skc11) ).
cnf(u1726,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human_person(X0,skc15),true,true,true),true) ).
cnf(u2401,negated_conjecture,
skc11 = ifeq4(of(skc10,skc11,skc15),true,skc14,skc11) ).
cnf(u64,axiom,
true = ifeq3(man(X0,X1),true,human_person(X0,X1),true) ).
cnf(u695,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc12),true,true,true),true) ).
cnf(u710,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc15),true) ).
cnf(u1656,negated_conjecture,
true = ifeq3(woman(skc8,X0),true,woman(skc10,X0),true) ).
cnf(u70,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(event(X0,X2),true,event(X1,X2),true),true) ).
cnf(u192,negated_conjecture,
true = sF0 ).
cnf(u1062,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc14),true,true,true),true) ).
cnf(u698,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc14),true,true,true),true) ).
cnf(u1749,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(organism(X0,skc12),true,true,true),true) ).
cnf(u1871,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,existent(X0,skc15),true) ).
cnf(u1730,negated_conjecture,
true = organism(skc10,skc15) ).
cnf(u68,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(dance(X0,X2),true,dance(X1,X2),true),true) ).
cnf(u198,negated_conjecture,
true = sF2 ).
cnf(u1736,negated_conjecture,
true = impartial(skc10,skc15) ).
cnf(u1893,negated_conjecture,
true = ifeq3(impartial(skc8,X0),true,impartial(skc10,X0),true) ).
cnf(u367,negated_conjecture,
true = ifeq3(proposition(skc8,skc11),true,true,true) ).
cnf(u704,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc14),true,true,true),true) ).
cnf(u476,negated_conjecture,
b = ifeq2(tuple2(unisex(skc8,skc12),true),tuple2(true,true),a,b) ).
cnf(u1891,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,impartial(X0,skc15),true) ).
cnf(u110,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(entity(X0,X2),true,entity(X1,X2),true),true) ).
cnf(u1824,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(entity(X0,skc15),true,true,true),true) ).
cnf(u610,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc15),true,true,true),true) ).
cnf(u2406,negated_conjecture,
skc14 = ifeq4(of(skc10,skc14,skc12),true,skc11,skc14) ).
cnf(u365,negated_conjecture,
true = relation(skc8,skc14) ).
cnf(u616,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc14),true) ).
cnf(u466,negated_conjecture,
b = ifeq2(tuple2(true,male(skc8,skc10)),tuple2(true,true),a,b) ).
cnf(u1241,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relation(X0,skc10),true,true,true),true) ).
cnf(u108,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(organism(X0,X2),true,organism(X1,X2),true),true) ).
cnf(u182,axiom,
b = ifeq2(tuple2(nonhuman(X0,X1),human(X0,X1)),tuple2(true,true),a,b) ).
cnf(u2264,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,of(X0,skc11,skc12),true) ).
cnf(u2417,negated_conjecture,
skc14 = ifeq4(of(skc8,X0,skc12),true,ifeq4(of(skc8,skc14,skc12),true,ifeq4(forename(skc8,X0),true,X0,skc14),skc14),skc14) ).
cnf(u355,negated_conjecture,
true = unisex(skc8,skc10) ).
cnf(u1254,negated_conjecture,
true = relation(skc10,skc11) ).
cnf(u2165,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,male(X0,skc15),true) ).
cnf(u2039,negated_conjecture,
true = ifeq3(animate(skc8,X0),true,animate(skc10,X0),true) ).
cnf(u378,negated_conjecture,
true = general(skc8,skc11) ).
cnf(u464,negated_conjecture,
true = male(skc8,skc15) ).
cnf(u1247,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,relation(X0,skc11),true) ).
cnf(u98,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(forename(X0,X2),true,forename(X1,X2),true),true) ).
cnf(u1385,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonhuman(X0,skc10),true,true,true),true) ).
cnf(u1280,negated_conjecture,
b = ifeq2(tuple2(true,human(skc10,skc14)),tuple2(true,true),a,b) ).
cnf(u2679,negated_conjecture,
skc14 = ifeq4(of(skc10,skc11,X0),true,ifeq4(of(skc10,skc14,X0),true,ifeq4(entity(skc10,X0),true,skc11,skc14),skc14),skc14) ).
cnf(u2545,negated_conjecture,
ifeq4(theme(skc8,skc9,X0),true,ifeq4(proposition(skc8,X0),true,skc10,X0),X0) = X0 ).
cnf(u251,negated_conjecture,
true = man(skc8,skc15) ).
cnf(u1038,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc14),true,true,true),true) ).
cnf(u483,negated_conjecture,
b = ifeq2(tuple2(specific(skc8,skc14),true),tuple2(true,true),a,b) ).
cnf(u2166,negated_conjecture,
true = ifeq3(male(skc8,X0),true,male(skc10,X0),true) ).
cnf(u637,negated_conjecture,
true = thing(skc10,skc15) ).
cnf(u376,negated_conjecture,
true = thing(skc8,skc11) ).
cnf(u2008,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human(X0,skc15),true,true,true),true) ).
cnf(u20,axiom,
true = ifeq3(desire_want(X0,X1),true,event(X0,X1),true) ).
cnf(u635,negated_conjecture,
true = thing(skc10,skc12) ).
cnf(u1293,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(abstraction(X0,skc11),true,true,true),true) ).
cnf(u791,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(specific(X0,skc12),true,true,true),true) ).
cnf(u1256,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relation(X0,skc14),true,true,true),true) ).
cnf(u249,negated_conjecture,
b = ifeq(tuple(dance(X0,X1),event(X0,X1),desire_want(skc8,X2),proposition(skc8,X0),accessible_world(skc8,X0),present(X0,X1),present(skc8,X2),agent(X0,X1,skc15),agent(skc8,X2,skc15),theme(skc8,X2,X0)),sF19,a,b) ).
cnf(u1036,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc11),true,true,true),true) ).
cnf(u267,negated_conjecture,
true = agent(skc10,skc13,skc12) ).
cnf(u1166,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(desire_want(X0,skc9),true,true,true),true) ).
cnf(u2038,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,animate(X0,skc12),true) ).
cnf(u1159,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(desire_want(X0,skc9),true,true,true),true) ).
cnf(u10,axiom,
true = ifeq3(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u1297,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,abstraction(X0,skc14),true) ).
cnf(u1051,negated_conjecture,
true = unisex(skc10,skc14) ).
cnf(u2301,negated_conjecture,
ifeq4(of(skc8,X1,skc15),true,ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X1),true,ifeq4(forename(skc8,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u526,negated_conjecture,
true = eventuality(skc10,skc9) ).
cnf(u1040,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc9),true) ).
cnf(u2335,negated_conjecture,
skc14 = ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X0),true,X0,skc14),skc14) ).
cnf(u2800,negated_conjecture,
ifeq4(theme(skc8,X0,skc10),true,ifeq4(theme(skc8,skc9,X1),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X0),true,skc10,X1),X1),X1),X1) = X1 ).
cnf(u1543,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,relname(X0,skc11),true) ).
cnf(u265,negated_conjecture,
true = of(skc8,skc11,skc12) ).
cnf(u532,negated_conjecture,
true = specific(skc10,skc9) ).
cnf(u1822,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(entity(X0,skc15),true,true,true),true) ).
cnf(u549,negated_conjecture,
true = ifeq3(accessible_world(skc10,skc8),true,true,true) ).
cnf(u510,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(event(X0,skc9),true,true,true),true) ).
cnf(u8,axiom,
true = ifeq3(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u1303,negated_conjecture,
b = ifeq2(tuple2(specific(skc10,skc11),true),tuple2(true,true),a,b) ).
cnf(u1828,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,entity(X0,skc12),true) ).
cnf(u654,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc11),true,true,true),true) ).
cnf(u1565,negated_conjecture,
true = ifeq3(vincent_forename(skc10,skc11),true,true,true) ).
cnf(u1168,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,desire_want(X0,skc9),true) ).
cnf(u1826,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,entity(X0,skc12),true) ).
cnf(u1671,negated_conjecture,
true = organism(skc10,skc12) ).
cnf(u393,negated_conjecture,
true = singleton(skc8,skc11) ).
cnf(u660,negated_conjecture,
true = singleton(skc10,skc11) ).
cnf(u1563,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(forename(X0,skc11),true,true,true),true) ).
cnf(u677,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc15),true) ).
cnf(u909,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,nonexistent(X0,skc13),true) ).
cnf(u1552,negated_conjecture,
true = ifeq3(mia_forename(skc10,skc14),true,true,true) ).
cnf(u794,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,specific(X0,skc12),true) ).
cnf(u1569,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,forename(X0,skc11),true) ).
cnf(u675,negated_conjecture,
true = ifeq3(eventuality(skc10,skc15),true,true,true) ).
cnf(u2291,negated_conjecture,
skc11 = ifeq4(of(skc10,X1,X0),true,ifeq4(of(skc10,skc11,X0),true,ifeq4(entity(skc10,X0),true,ifeq4(forename(skc10,X1),true,X1,skc11),skc11),skc11),skc11) ).
cnf(u907,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,nonexistent(X0,skc9),true) ).
cnf(u2300,negated_conjecture,
ifeq4(of(skc10,X1,skc12),true,ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X1),true,ifeq4(forename(skc10,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u2722,negated_conjecture,
ifeq4(of(skc10,skc11,skc15),true,ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X0),true,skc11,X0),X0),X0) = X0 ).
cnf(u1674,negated_conjecture,
b = ifeq2(tuple2(true,male(skc10,skc12)),tuple2(true,true),a,b) ).
cnf(u2339,negated_conjecture,
ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X0),true,skc14,X0),X0) = X0 ).
cnf(u422,negated_conjecture,
true = existent(skc8,skc12) ).
cnf(u48,axiom,
true = ifeq3(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u94,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).
cnf(u1680,negated_conjecture,
true = impartial(skc10,skc12) ).
cnf(u694,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc13),true,true,true),true) ).
cnf(u1711,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human_person(X0,skc12),true,true,true),true) ).
cnf(u700,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc10),true,true,true),true) ).
cnf(u665,negated_conjecture,
true = ifeq3(abstraction(skc10,skc12),true,true,true) ).
cnf(u54,axiom,
true = ifeq3(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u176,axiom,
b = ifeq2(tuple2(unisex(X0,X1),male(X0,X1)),tuple2(true,true),a,b) ).
cnf(u1471,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(general(X0,skc14),true,true,true),true) ).
cnf(u2095,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(female(X0,skc12),true,true,true),true) ).
cnf(u554,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(eventuality(X0,skc13),true,true,true),true) ).
cnf(u2503,negated_conjecture,
skc10 = ifeq4(theme(skc10,X2,X1),true,ifeq4(theme(skc10,X0,skc10),true,ifeq4(proposition(skc10,X1),true,ifeq4(desire_want(skc10,X2),true,ifeq4(desire_want(skc10,X0),true,X1,skc10),skc10),skc10),skc10),skc10) ).
cnf(u1965,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,living(X0,skc15),true) ).
cnf(u560,negated_conjecture,
true = ifeq3(eventuality(skc8,X0),true,eventuality(skc10,X0),true) ).
cnf(u1714,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,human_person(X0,skc12),true) ).
cnf(u1963,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,living(X0,skc15),true) ).
cnf(u2366,negated_conjecture,
skc14 = ifeq4(of(skc8,skc11,skc15),true,skc11,skc14) ).
cnf(u1720,negated_conjecture,
true = ifeq3(woman(skc10,skc15),true,true,true) ).
cnf(u2572,negated_conjecture,
ifeq4(theme(skc10,skc9,X0),true,ifeq4(proposition(skc10,X0),true,skc10,X0),X0) = X0 ).
cnf(u1074,negated_conjecture,
true = ifeq3(present(skc8,X0),true,present(skc10,X0),true) ).
cnf(u437,negated_conjecture,
true = ifeq3(man(skc8,skc12),true,true,true) ).
cnf(u2234,negated_conjecture,
true = theme(skc10,skc9,skc10) ).
cnf(u332,negated_conjecture,
true = unisex(skc8,skc9) ).
cnf(u180,axiom,
b = ifeq2(tuple2(specific(X0,X1),general(X0,X1)),tuple2(true,true),a,b) ).
cnf(u1073,negated_conjecture,
true = ifeq3(present(X0,skc9),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u1960,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(living(X0,skc15),true,true,true),true) ).
cnf(u1202,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(proposition(X0,skc10),true,true,true),true) ).
cnf(u1478,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,general(X0,skc14),true) ).
cnf(u351,negated_conjecture,
true = general(skc8,skc10) ).
cnf(u120,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(animate(X0,X2),true,animate(X1,X2),true),true) ).
cnf(u705,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc14),true) ).
cnf(u460,negated_conjecture,
true = ifeq3(eventuality(skc8,skc15),true,true,true) ).
cnf(u1875,negated_conjecture,
true = ifeq3(existent(skc8,X0),true,existent(skc10,X0),true) ).
cnf(u1750,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(organism(X0,skc15),true,true,true),true) ).
cnf(u1221,negated_conjecture,
b = ifeq2(tuple2(true,human(skc10,skc10)),tuple2(true,true),a,b) ).
cnf(u2120,negated_conjecture,
true = ifeq3(vincent_forename(skc8,X0),true,vincent_forename(skc10,X0),true) ).
cnf(u1476,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,general(X0,skc14),true) ).
cnf(u195,negated_conjecture,
true = sF1 ).
cnf(u2005,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human(X0,skc12),true,true,true),true) ).
cnf(u450,negated_conjecture,
true = impartial(skc8,skc15) ).
cnf(u2505,negated_conjecture,
ifeq4(theme(skc10,X2,skc10),true,ifeq4(theme(skc10,X1,X0),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X2),true,ifeq4(desire_want(skc10,X1),true,skc10,X0),X0),X0),X0),X0) = X0 ).
cnf(u92,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).
cnf(u222,negated_conjecture,
true = sF10 ).
cnf(u1480,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,general(X0,skc10),true) ).
cnf(u2009,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,human(X0,skc15),true) ).
cnf(u1388,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,nonhuman(X0,skc11),true) ).
cnf(u477,negated_conjecture,
b = ifeq2(tuple2(true,general(skc10,skc13)),tuple2(true,true),a,b) ).
cnf(u2144,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,man(X0,skc15),true) ).
cnf(u82,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(unisex(X0,X2),true,unisex(X1,X2),true),true) ).
cnf(u1261,negated_conjecture,
true = abstraction(skc10,skc14) ).
cnf(u1392,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,nonhuman(X0,skc11),true) ).
cnf(u407,negated_conjecture,
true = ifeq3(entity(skc8,skc10),true,true,true) ).
cnf(u1242,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relation(X0,skc11),true,true,true),true) ).
cnf(u467,negated_conjecture,
b = ifeq2(tuple2(true,male(skc8,skc11)),tuple2(true,true),a,b) ).
cnf(u2150,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(man(X0,skc15),true,true,true),true) ).
cnf(u621,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc15),true) ).
cnf(u360,negated_conjecture,
true = relname(skc8,skc11) ).
cnf(u490,negated_conjecture,
b = ifeq2(tuple2(female(skc8,skc15),true),tuple2(true,true),a,b) ).
cnf(ifeq_axiom_003,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u210,negated_conjecture,
true = sF6 ).
cnf(u619,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc12),true) ).
cnf(u379,negated_conjecture,
true = unisex(skc8,skc11) ).
cnf(u1278,negated_conjecture,
true = nonhuman(skc10,skc11) ).
cnf(u488,negated_conjecture,
b = ifeq2(tuple2(nonhuman(skc8,skc15),true),tuple2(true,true),a,b) ).
cnf(u122,axiom,
true = ifeq3(accessible_world(X0,X1),true,ifeq3(female(X0,X2),true,female(X1,X2),true),true) ).
cnf(u1035,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc10),true,true,true),true) ).
cnf(u1641,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(mia_forename(X0,skc11),true,true,true),true) ).
cnf(u2164,negated_conjecture,
true = ifeq3(accessible_world(skc10,X0),true,male(X0,skc15),true) ).
cnf(u638,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc10),true,true,true),true) ).
cnf(u1533,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(forename(X0,skc11),true,true,true),true) ).
cnf(u1655,negated_conjecture,
true = ifeq3(accessible_world(skc8,X0),true,woman(X0,skc12),true) ).
cnf(u2256,negated_conjecture,
true = ifeq3(of(skc8,X1,X0),true,of(skc10,X1,X0),true) ).
cnf(u377,negated_conjecture,
true = nonhuman(skc8,skc11) ).
cnf(u516,negated_conjecture,
true = ifeq3(event(skc8,skc13),true,true,true) ).
cnf(u533,negated_conjecture,
true = nonexistent(skc10,skc9) ).
cnf(u494,negated_conjecture,
b = ifeq2(tuple2(nonexistent(skc8,skc15),true),tuple2(true,true),a,b) ).
cnf(u2032,negated_conjecture,
true = ifeq3(accessible_world(X0,skc8),true,ifeq3(animate(X0,skc15),true,true,true),true) ).
cnf(u250,negated_conjecture,
true = actual_world(skc8) ).
cnf(u531,negated_conjecture,
true = thing(skc10,skc9) ).
cnf(u2292,negated_conjecture,
skc14 = ifeq4(of(skc10,X1,X0),true,ifeq4(of(skc10,skc14,X0),true,ifeq4(entity(skc10,X0),true,ifeq4(forename(skc10,X1),true,X1,skc14),skc14),skc14),skc14) ).
cnf(u1549,negated_conjecture,
true = ifeq3(accessible_world(X0,skc10),true,ifeq3(forename(X0,skc14),true,true,true),true) ).
cnf(u2500,negated_conjecture,
ifeq4(theme(skc8,X2,X1),true,ifeq4(theme(skc8,skc9,X0),true,ifeq4(proposition(skc8,X1),true,ifeq4(proposition(skc8,X0),true,ifeq4(desire_want(skc8,X2),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(u644,negated_conjecture,
true = singleton(skc10,skc10) ).
cnf(u278,negated_conjecture,
b = ifeq(tuple(true,true,desire_want(skc8,X0),true,true,true,present(skc8,X0),agent(skc10,skc13,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc10)),sF19,a,b) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP024-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n004.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 17:48:52 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.97/2.23 % (3782058)Detected a unit-equality problem, will run specialized UEQ schedule.
% 9.97/2.23 % (3782140)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4102737039:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 9.97/2.23 % (3782139)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2051781778:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 9.97/2.23 % (3782138)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=557810161:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 9.97/2.23 % (3782136)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=2308544064:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 9.97/2.23 % (3782137)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=2576247763:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 9.97/2.23 % (3782142)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1282409873:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 9.97/2.23 % (3782141)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3522464603:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 9.97/2.23 % (3782140)Instruction limit reached!
% 9.97/2.23 % (3782140)------------------------------
% 9.97/2.23 % (3782140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782140)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782140)Termination reason: Instruction limit
% 9.97/2.23 % (3782140)Termination phase: Saturation
% 9.97/2.23 % (3782140)Time elapsed: 0.057 s
% 9.97/2.23 % (3782140)Peak memory usage: 89 MB
% 9.97/2.23 % (3782140)Instructions burned: 182 (million)
% 9.97/2.23 % (3782139)Instruction limit reached!
% 9.97/2.23 % (3782139)------------------------------
% 9.97/2.23 % (3782139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782139)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782139)Termination reason: Instruction limit
% 9.97/2.23 % (3782139)Termination phase: Saturation
% 9.97/2.23 % (3782139)Time elapsed: 0.068 s
% 9.97/2.23 % (3782139)Peak memory usage: 88 MB
% 9.97/2.23 % (3782139)Instructions burned: 137 (million)
% 9.97/2.23 % (3782150)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2659327748:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 9.97/2.23 % (3782142)Refutation not found, incomplete strategy
% 9.97/2.23 % (3782142)------------------------------
% 9.97/2.23 % (3782142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782142)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782142)Termination reason: Refutation not found, incomplete strategy
% 9.97/2.23 % (3782142)Time elapsed: 0.129 s
% 9.97/2.23 % (3782142)Peak memory usage: 90 MB
% 9.97/2.23 % (3782142)Instructions burned: 225 (million)
% 9.97/2.23 % (3782141)Instruction limit reached!
% 9.97/2.23 % (3782141)------------------------------
% 9.97/2.23 % (3782141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782141)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782141)Termination reason: Instruction limit
% 9.97/2.23 % (3782141)Termination phase: Saturation
% 9.97/2.23 % (3782141)Time elapsed: 0.162 s
% 9.97/2.23 % (3782141)Peak memory usage: 91 MB
% 9.97/2.23 % (3782141)Instructions burned: 257 (million)
% 9.97/2.23 % (3782151)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2479253896:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 9.97/2.23 % (3782153)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=31381353:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 9.97/2.23 % (3782142)------------------------------
% 9.97/2.23 % (3782142)------------------------------
% 9.97/2.23 % (3782153)Instruction limit reached!
% 9.97/2.23 % (3782153)------------------------------
% 9.97/2.23 % (3782153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782153)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782153)Termination reason: Instruction limit
% 9.97/2.23 % (3782153)Termination phase: Saturation
% 9.97/2.23 % (3782153)Time elapsed: 0.108 s
% 9.97/2.23 % (3782153)Peak memory usage: 93 MB
% 9.97/2.23 % (3782153)Instructions burned: 215 (million)
% 9.97/2.23 % (3782156)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=1759222836:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 9.97/2.23 % (3782157)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=3137485080:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 9.97/2.23 % (3782156)Instruction limit reached!
% 9.97/2.23 % (3782156)------------------------------
% 9.97/2.23 % (3782156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782156)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782156)Termination reason: Instruction limit
% 9.97/2.23 % (3782156)Termination phase: Saturation
% 9.97/2.23 % (3782156)Time elapsed: 0.169 s
% 9.97/2.23 % (3782156)Peak memory usage: 95 MB
% 9.97/2.23 % (3782156)Instructions burned: 318 (million)
% 9.97/2.23 % (3782150)Refutation not found, incomplete strategy
% 9.97/2.23 % (3782150)------------------------------
% 9.97/2.23 % (3782150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.97/2.23 % (3782150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.97/2.23 % (3782150)CaDiCaL version: 2.1.3
% 9.97/2.23 % (3782150)Termination reason: Refutation not found, incomplete strategy
% 9.97/2.23 % (3782150)Time elapsed: 0.633 s
% 9.97/2.23 % (3782150)Peak memory usage: 136 MB
% 9.97/2.23 % (3782150)Instructions burned: 1667 (million)
% 9.97/2.23 % (3782160)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1242327299:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 9.97/2.23 % (3782150)------------------------------
% 9.97/2.23 % (3782150)------------------------------
% 9.97/2.23 % (3782160)First to succeed.
% 9.97/2.23 % (3782160)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3782058"
% 9.97/2.23 % (3782162)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=558558148:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 9.97/2.23 % (3782137)Also succeeded, but the first one will report.
% 9.97/2.23 % (3782138)Also succeeded, but the first one will report.
% 9.97/2.23 % SZS status Satisfiable for theBenchmark
% 9.97/2.23 % SZS output start Saturation.
% See solution above
% 10.27/2.32 % SZS output start Definitions and Model Updates.
% 10.27/2.32 % SZS output end Definitions and Model Updates.
% 10.27/2.32 % (3782160)------------------------------
% 10.27/2.32 % (3782160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/2.32 % (3782160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/2.32 % (3782160)CaDiCaL version: 2.1.3
% 10.27/2.32 % (3782160)Termination reason: Satisfiable
% 10.27/2.32 % (3782160)Time elapsed: 0.157 s
% 10.27/2.32 % (3782160)Peak memory usage: 92 MB
% 10.27/2.32 % (3782160)Instructions burned: 259 (million)
% 10.27/2.32 % (3782160)------------------------------
% 10.27/2.32 % (3782160)------------------------------
% 10.27/2.32 % (3782058)Success in time 1.376 s
% 10.27/2.32 % Vampire exiting
%------------------------------------------------------------------------------