%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP225-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:00 PM UTC 2026
% Result : Satisfiable 12.88s 2.85s
% Output : Saturation 14.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1021,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc11),true,true,true),true) ).
cnf(u248,negated_conjecture,
true = think_believe_consider(skc8,skc12) ).
cnf(u1415,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(living(X0,skc10),true,true,true),true) ).
cnf(u659,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc13),true) ).
cnf(u1788,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonhuman(X0,skc13),true,true,true),true) ).
cnf(u1019,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc12),true) ).
cnf(u1677,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc11),true,true,true),true) ).
cnf(u1567,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,relname(X0,skc13),true) ).
cnf(u289,negated_conjecture,
true = singleton(skc8,skc12) ).
cnf(u1786,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc13),true,true,true),true) ).
cnf(u521,negated_conjecture,
true = nonexistent(skc11,skc12) ).
cnf(u2323,negated_conjecture,
true = jules_forename(skc11,skc13) ).
cnf(u406,negated_conjecture,
true = thing(skc8,skc11) ).
cnf(u2712,negated_conjecture,
skc11 = ifeq3(theme(skc11,skc12,X0),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11) ).
cnf(u1664,negated_conjecture,
true = nonhuman(skc11,skc11) ).
cnf(u1681,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,abstraction(X0,skc11),true) ).
cnf(u1821,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(general(X0,skc11),true,true,true),true) ).
cnf(u295,negated_conjecture,
true = organism(skc8,skc10) ).
cnf(u1570,negated_conjecture,
true = ifeq2(relname(skc8,X0),true,relname(skc11,X0),true) ).
cnf(u78,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(unisex(X0,X2),true,unisex(X1,X2),true),true) ).
cnf(u649,negated_conjecture,
true = ifeq2(eventuality(skc11,skc10),true,true,true) ).
cnf(u1819,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(general(X0,skc13),true,true,true),true) ).
cnf(u2194,negated_conjecture,
skc13 = ifeq3(of(skc8,X1,X0),true,ifeq3(of(skc8,skc13,X0),true,ifeq3(forename(skc8,X1),true,ifeq3(entity(skc8,X0),true,X1,skc13),skc13),skc13),skc13) ).
cnf(u1825,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc11),true) ).
cnf(u61,axiom,
true = ifeq2(proposition(X0,X1),true,relation(X0,X1),true) ).
cnf(u1949,negated_conjecture,
true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u423,negated_conjecture,
true = of(skc8,skc13,skc10) ).
cnf(u76,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).
cnf(u1169,negated_conjecture,
true = ifeq2(event(skc8,skf1(X0)),true,true,true) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u306,negated_conjecture,
true = thing(skc8,skc10) ).
cnf(u2780,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11),skc11) ).
cnf(u2859,negated_conjecture,
skc11 = ifeq3(theme(skc8,X1,skc11),true,ifeq3(theme(skc8,skc12,X2),true,ifeq3(agent(skc8,X1,X0),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X2),true,X2,skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u1205,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,specific(X1,skf1(X0)),true) ).
cnf(u1186,negated_conjecture,
true = nonexistent(skc11,skf1(X0)) ).
cnf(u2163,negated_conjecture,
true = ifeq2(be(skc8,X2,X1,X0),true,be(skc11,X2,X1,X0),true) ).
cnf(u2489,negated_conjecture,
ifeq3(theme(skc11,skc12,X2),true,ifeq3(theme(skc11,X1,X0),true,ifeq3(agent(skc11,X1,skc10),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X2),true,ifeq3(proposition(skc11,X0),true,X0,X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u1944,negated_conjecture,
true = ifeq2(smoke(skc8,skf1(X0)),true,true,true) ).
cnf(u2643,negated_conjecture,
skc11 = ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X0),true,skc11,skc11),skc11) ).
cnf(u1989,negated_conjecture,
true = think_believe_consider(skc11,skc12) ).
cnf(u584,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc11),true,true,true),true) ).
cnf(u1215,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(singleton(X1,skf1(X0)),true,true,true),true) ).
cnf(u1217,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,singleton(X1,skf1(X0)),true) ).
cnf(u1987,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,think_believe_consider(X0,skc12),true) ).
cnf(u847,negated_conjecture,
true = ifeq2(nonexistent(skc8,X0),true,nonexistent(skc11,X0),true) ).
cnf(u636,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc11),true,true,true),true) ).
cnf(u1222,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human_person(X0,skc10),true,true,true),true) ).
cnf(u461,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(state(X0,skc9),true,true,true),true) ).
cnf(u66,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(state(X0,X2),true,state(X1,X2),true),true) ).
cnf(u1226,negated_conjecture,
true = ifeq2(human_person(skc8,X0),true,human_person(skc11,X0),true) ).
cnf(u451,negated_conjecture,
b = ifeq(tuple(specific(skc8,skc11),true),tuple(true,true),a,b) ).
cnf(u344,negated_conjecture,
true = male(skc8,skc10) ).
cnf(u1127,negated_conjecture,
true = ifeq2(man(skc8,X0),true,man(skc11,X0),true) ).
cnf(u116,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(smoke(X0,X2),true,smoke(X1,X2),true),true) ).
cnf(u990,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc9),true,true,true),true) ).
cnf(u2930,negated_conjecture,
ifeq3(theme(skc11,X0,X1),true,ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1224,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,human_person(X0,skc10),true) ).
cnf(u217,negated_conjecture,
true = sF9 ).
cnf(u996,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc12),true) ).
cnf(u363,negated_conjecture,
true = ifeq2(abstraction(skc8,skc9),true,true,true) ).
cnf(u733,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc9),true) ).
cnf(u472,negated_conjecture,
true = event(skc11,skc9) ).
cnf(u106,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relation(X0,X2),true,relation(X1,X2),true),true) ).
cnf(u1393,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,impartial(X0,skc10),true) ).
cnf(u1487,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(male(X0,skc10),true,true,true),true) ).
cnf(u731,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skc12),true) ).
cnf(u1517,negated_conjecture,
true = forename(skc11,skc13) ).
cnf(u1015,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc9),true,true,true),true) ).
cnf(u223,negated_conjecture,
true = sF11 ).
cnf(u2010,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,proposition(X0,skc11),true) ).
cnf(u361,negated_conjecture,
true = ifeq2(abstraction(skc8,skc12),true,true,true) ).
cnf(u491,negated_conjecture,
b = ifeq(tuple(true,existent(skc11,skc9)),tuple(true,true),a,b) ).
cnf(u1918,negated_conjecture,
true = ifeq2(jules_forename(skc8,X0),true,jules_forename(skc11,X0),true) ).
cnf(u104,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relname(X0,X2),true,relname(X1,X2),true),true) ).
cnf(u2062,negated_conjecture,
true = of(skc11,skc13,skc10) ).
cnf(u7,axiom,
true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u2562,negated_conjecture,
skc11 = ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc10),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11) ).
cnf(u489,negated_conjecture,
b = ifeq(tuple(true,general(skc11,skc9)),tuple(true,true),a,b) ).
cnf(u1659,negated_conjecture,
true = abstraction(skc11,skc11) ).
cnf(u1142,negated_conjecture,
true = smoke(skc11,skf1(X0)) ).
cnf(u2016,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(proposition(X0,skc11),true,true,true),true) ).
cnf(u232,negated_conjecture,
true = sF14 ).
cnf(u1527,negated_conjecture,
true = ifeq2(proposition(skc11,skc13),true,true,true) ).
cnf(u643,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc11),true) ).
cnf(u2190,negated_conjecture,
ifeq3(of(skc11,X1,skc10),true,ifeq3(of(skc11,X0,skc10),true,ifeq3(forename(skc11,X1),true,ifeq3(forename(skc11,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u5,axiom,
true = ifeq2(state(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u273,negated_conjecture,
true = ifeq2(state(skc8,skc12),true,true,true) ).
cnf(u540,negated_conjecture,
true = ifeq2(accessible_world(skc11,skc11),true,true,true) ).
cnf(u1787,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc11),true,true,true),true) ).
cnf(u2696,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11) ).
cnf(u1311,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(organism(X0,skc10),true,true,true),true) ).
cnf(u519,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,eventuality(X0,skc12),true) ).
cnf(u1018,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc9),true) ).
cnf(u1665,negated_conjecture,
true = general(skc11,skc11) ).
cnf(u263,negated_conjecture,
true = thing(skc8,skc9) ).
cnf(u1534,negated_conjecture,
true = general(skc11,skc13) ).
cnf(clause70,axiom,
ifeq3(of(X0,X1,X2),true,ifeq3(of(X0,X3,X2),true,ifeq3(forename(X0,X1),true,ifeq3(forename(X0,X3),true,ifeq3(entity(X0,X2),true,X1,X3),X3),X3),X3),X3) = X3 ).
cnf(u401,negated_conjecture,
true = abstraction(skc8,skc11) ).
cnf(u1155,negated_conjecture,
b = ifeq(tuple(unisex(skc11,skc10),true),tuple(true,true),a,b) ).
cnf(u1678,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(abstraction(X0,skc13),true,true,true),true) ).
cnf(u1439,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(human(X0,skc10),true,true,true),true) ).
cnf(u2063,negated_conjecture,
true = ifeq2(of(X0,skc13,skc10),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u522,negated_conjecture,
true = specific(skc11,skc12) ).
cnf(u1684,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc11),true) ).
cnf(u45,axiom,
true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u528,negated_conjecture,
true = ifeq2(entity(skc11,skc12),true,true,true) ).
cnf(u407,negated_conjecture,
true = nonhuman(skc8,skc11) ).
cnf(u1153,negated_conjecture,
true = human(skc11,skc10) ).
cnf(u484,negated_conjecture,
true = ifeq2(smoke(skc11,skc9),true,true,true) ).
cnf(u2191,negated_conjecture,
ifeq3(of(skc8,X1,skc10),true,ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X1),true,ifeq3(forename(skc8,X0),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u650,negated_conjecture,
true = singleton(skc11,skc10) ).
cnf(u35,axiom,
true = ifeq2(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u1446,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(animate(X0,skc10),true,true,true),true) ).
cnf(u1951,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,present(X0,skf1(X1)),true) ).
cnf(u258,negated_conjecture,
true = theme(skc8,skc12,skc11) ).
cnf(u673,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc10),true) ).
cnf(u2462,negated_conjecture,
ifeq3(theme(skc8,X3,X2),true,ifeq3(theme(skc8,X1,skc11),true,ifeq3(agent(skc8,X3,X0),true,ifeq3(agent(skc8,X1,X0),true,ifeq3(think_believe_consider(skc8,X3),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X2),true,skc11,X2),X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u1189,negated_conjecture,
true = ifeq2(unisex(skc8,skf1(X0)),true,true,true) ).
cnf(u727,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc10),true,true,true),true) ).
cnf(u1450,negated_conjecture,
true = ifeq2(animate(skc8,X0),true,animate(skc11,X0),true) ).
cnf(u1170,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(event(X1,skf1(X0)),true,true,true),true) ).
cnf(u447,negated_conjecture,
b = ifeq(tuple(true,general(skc8,skc10)),tuple(true,true),a,b) ).
cnf(u1193,negated_conjecture,
true = ifeq2(abstraction(skc11,skf1(X0)),true,true,true) ).
cnf(u190,negated_conjecture,
true = sF0 ).
cnf(u2629,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(agent(skc11,X0,X1),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(think_believe_consider(skc11,X0),true,skc11,skc11),skc11),skc11),skc11) ).
cnf(u1448,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,animate(X0,skc10),true) ).
cnf(u1675,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc13),true,true,true),true) ).
cnf(u1041,negated_conjecture,
true = event(skc11,skc12) ).
cnf(u1206,negated_conjecture,
true = ifeq2(thing(skc8,skf1(X0)),true,true,true) ).
cnf(u445,negated_conjecture,
b = ifeq(tuple(unisex(skc8,skc10),true),tuple(true,true),a,b) ).
cnf(u1199,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,nonexistent(X1,skf1(X0)),true) ).
cnf(u2630,negated_conjecture,
ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1) = X1 ).
cnf(u1204,negated_conjecture,
true = ifeq2(entity(skc11,skf1(X0)),true,true,true) ).
cnf(u178,negated_conjecture,
true = ifeq2(man(skc11,X0),true,agent(skc11,skf1(X0),X0),true) ).
cnf(u2758,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).
cnf(u2631,negated_conjecture,
ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1) = X1 ).
cnf(u589,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc12),true) ).
cnf(u458,negated_conjecture,
b = ifeq(tuple(nonexistent(skc8,skc10),true),tuple(true,true),a,b) ).
cnf(u100,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(male(X0,X2),true,male(X1,X2),true),true) ).
cnf(u2500,negated_conjecture,
ifeq3(theme(skc8,X2,X1),true,ifeq3(agent(skc8,X2,X0),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(think_believe_consider(skc8,X2),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1),X1) = X1 ).
cnf(u587,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u2641,negated_conjecture,
ifeq3(theme(skc11,skc12,X0),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0) = X0 ).
cnf(u1990,negated_conjecture,
true = ifeq2(think_believe_consider(X0,skc12),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u456,negated_conjecture,
b = ifeq(tuple(true,existent(skc8,skc9)),tuple(true,true),a,b) ).
cnf(u2519,negated_conjecture,
skc11 = ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X0),true,skc11,skc11),skc11) ).
cnf(u90,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(existent(X0,X2),true,existent(X1,X2),true),true) ).
cnf(u999,negated_conjecture,
true = ifeq2(unisex(skc8,X0),true,unisex(skc11,X0),true) ).
cnf(u1310,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(organism(X0,skc10),true,true,true),true) ).
cnf(u612,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u462,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,state(X0,skc9),true) ).
cnf(u2517,negated_conjecture,
ifeq3(theme(skc8,skc12,X0),true,ifeq3(proposition(skc8,X0),true,skc11,X0),X0) = X0 ).
cnf(u88,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(entity(X0,X2),true,entity(X1,X2),true),true) ).
cnf(u2465,negated_conjecture,
ifeq3(theme(skc11,X3,X2),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,X3,X0),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(think_believe_consider(skc11,X3),true,ifeq3(proposition(skc11,X2),true,ifeq3(proposition(skc11,X1),true,X1,X2),X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u734,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc10),true) ).
cnf(u1645,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc13),true) ).
cnf(u1536,negated_conjecture,
b = ifeq(tuple(specific(skc11,skc13),true),tuple(true,true),a,b) ).
cnf(u473,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,state(X0,skc9),true) ).
cnf(u2929,negated_conjecture,
ifeq3(theme(skc11,skc12,X1),true,ifeq3(theme(skc11,X2,skc11),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,X2,X0),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1643,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,relation(X0,skc13),true) ).
cnf(u989,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc9),true,true,true),true) ).
cnf(u1511,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(forename(X0,skc13),true,true,true),true) ).
cnf(u2036,negated_conjecture,
true = ifeq2(vincent_forename(skc8,X0),true,vincent_forename(skc11,X0),true) ).
cnf(u2171,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,be(X0,skc9,skc10,skc10),true) ).
cnf(u518,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(eventuality(X0,skc12),true,true,true),true) ).
cnf(u2928,negated_conjecture,
skc11 = ifeq3(theme(skc11,X1,skc11),true,ifeq3(theme(skc11,X2,skc11),true,ifeq3(agent(skc11,X1,X0),true,ifeq3(agent(skc11,X2,X0),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(think_believe_consider(skc11,X2),true,skc11,skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u987,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc12),true,true,true),true) ).
cnf(u1390,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(impartial(X0,skc10),true,true,true),true) ).
cnf(u247,negated_conjecture,
true = forename(skc8,skc13) ).
cnf(u2034,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(vincent_forename(X0,skc13),true,true,true),true) ).
cnf(u3073,negated_conjecture,
ifeq3(theme(skc11,skc12,X1),true,ifeq3(theme(skc11,skc12,X2),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u479,negated_conjecture,
true = thing(skc11,skc9) ).
cnf(u617,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc9),true) ).
cnf(u372,negated_conjecture,
true = ifeq2(eventuality(skc8,skc13),true,true,true) ).
cnf(u502,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc12),true) ).
cnf(u631,negated_conjecture,
true = thing(skc11,skc10) ).
cnf(u2162,negated_conjecture,
true = ifeq2(be(X0,skc9,skc10,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u29,axiom,
true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u646,negated_conjecture,
true = ifeq2(abstraction(skc11,skc10),true,true,true) ).
cnf(u202,negated_conjecture,
true = sF4 ).
cnf(u1518,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(forename(X0,skc13),true,true,true),true) ).
cnf(u1008,negated_conjecture,
true = unisex(skc11,skc13) ).
cnf(u1791,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,nonhuman(X0,skc11),true) ).
cnf(u2057,negated_conjecture,
true = ifeq2(of(skc8,X1,X0),true,of(skc11,X1,X0),true) ).
cnf(u745,negated_conjecture,
b = ifeq(tuple(true,general(skc11,skc10)),tuple(true,true),a,b) ).
cnf(u500,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(eventuality(X0,skc9),true,true,true),true) ).
cnf(u1790,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonhuman(X0,skc11),true,true,true),true) ).
cnf(u128,axiom,
true = ifeq2(agent(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).
cnf(u634,negated_conjecture,
true = thing(skc11,skc13) ).
cnf(u1793,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,nonhuman(X0,skc13),true) ).
cnf(u2796,negated_conjecture,
ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,X1,skc10),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0) = X0 ).
cnf(u261,negated_conjecture,
true = eventuality(skc8,skc9) ).
cnf(u2058,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,of(X0,skc13,skc10),true) ).
cnf(u284,negated_conjecture,
true = thing(skc8,skc12) ).
cnf(u1683,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,abstraction(X0,skc13),true) ).
cnf(u2043,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,vincent_forename(X0,skc13),true) ).
cnf(clause71,axiom,
ifeq3(theme(X0,X1,X2),true,ifeq3(theme(X0,X3,X4),true,ifeq3(agent(X0,X1,X5),true,ifeq3(agent(X0,X3,X5),true,ifeq3(think_believe_consider(X0,X1),true,ifeq3(think_believe_consider(X0,X3),true,ifeq3(proposition(X0,X2),true,ifeq3(proposition(X0,X4),true,X4,X2),X2),X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u1045,negated_conjecture,
true = ifeq2(smoke(skc11,skc12),true,true,true) ).
cnf(u1026,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc11),true) ).
cnf(u19,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u2590,negated_conjecture,
skc11 = ifeq3(theme(skc8,skc12,X0),true,ifeq3(proposition(skc8,X0),true,X0,skc11),skc11) ).
cnf(u2983,negated_conjecture,
ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0) = X0 ).
cnf(u274,negated_conjecture,
true = event(skc8,skc9) ).
cnf(u657,negated_conjecture,
true = ifeq2(eventuality(skc11,skc13),true,true,true) ).
cnf(u412,negated_conjecture,
true = ifeq2(eventuality(skc8,skc11),true,true,true) ).
cnf(u132,axiom,
true = ifeq2(be(X0,X1,X2,X3),true,ifeq2(accessible_world(X0,X4),true,be(X4,X1,X2,X3),true),true) ).
cnf(u2827,negated_conjecture,
ifeq3(theme(skc8,skc12,X1),true,ifeq3(theme(skc8,X2,skc11),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,X2,X0),true,ifeq3(think_believe_consider(skc8,X2),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1173,negated_conjecture,
true = ifeq2(state(skc11,skf1(X0)),true,true,true) ).
cnf(u671,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).
cnf(u1154,negated_conjecture,
true = animate(skc11,skc10) ).
cnf(u17,axiom,
true = ifeq2(state(X0,X1),true,event(X0,X1),true) ).
cnf(u301,negated_conjecture,
true = entity(skc8,skc10) ).
cnf(u2464,negated_conjecture,
skc11 = ifeq3(theme(skc8,X3,skc11),true,ifeq3(theme(skc8,X2,X1),true,ifeq3(agent(skc8,X3,X0),true,ifeq3(agent(skc8,X2,X0),true,ifeq3(think_believe_consider(skc8,X3),true,ifeq3(think_believe_consider(skc8,X2),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u2957,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,skc11,skc11),skc11),skc11),skc11) ).
cnf(u1955,negated_conjecture,
true = present(skc11,skc12) ).
cnf(u674,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc13),true,true,true),true) ).
cnf(u59,axiom,
true = ifeq2(smoke(X0,X1),true,event(X0,X1),true) ).
cnf(u1190,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(unisex(X1,skf1(X0)),true,true,true),true) ).
cnf(u400,negated_conjecture,
true = ifeq2(relname(skc8,skc11),true,true,true) ).
cnf(u1183,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(eventuality(X1,skf1(X0)),true,true,true),true) ).
cnf(u1213,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,thing(X1,skf1(X0)),true) ).
cnf(u1194,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,unisex(X1,skf1(X0)),true) ).
cnf(u57,axiom,
true = ifeq2(jules_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u1188,negated_conjecture,
true = thing(skc11,skf1(X0)) ).
cnf(u419,negated_conjecture,
skc14 = skc10 ).
cnf(u442,negated_conjecture,
b = ifeq(tuple(true,male(skc8,skc12)),tuple(true,true),a,b) ).
cnf(u1449,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,animate(X0,skc10),true) ).
cnf(u1203,negated_conjecture,
b = ifeq(tuple(true,general(skc11,skf1(X0))),tuple(true,true),a,b) ).
cnf(u1344,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,entity(X0,skc10),true) ).
cnf(u1192,negated_conjecture,
b = ifeq(tuple(true,male(skc11,skf1(X0))),tuple(true,true),a,b) ).
cnf(u63,axiom,
true = ifeq2(vincent_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u318,negated_conjecture,
true = specific(skc8,skc10) ).
cnf(u841,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonexistent(X0,skc9),true,true,true),true) ).
cnf(u84,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human_person(X0,X2),true,human_person(X1,X2),true),true) ).
cnf(u3013,negated_conjecture,
skc11 = ifeq3(theme(skc11,X1,skc11),true,ifeq3(theme(skc11,skc12,X2),true,ifeq3(agent(skc11,X1,X0),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X2),true,X2,skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u2408,negated_conjecture,
skc13 = ifeq3(of(skc11,skc13,X0),true,ifeq3(of(skc11,skc13,X0),true,ifeq3(entity(skc11,X0),true,skc13,skc13),skc13),skc13) ).
cnf(u3121,negated_conjecture,
ifeq3(theme(skc11,skf1(skc10),X1),true,ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u446,negated_conjecture,
b = ifeq(tuple(true,general(skc8,skc12)),tuple(true,true),a,b) ).
cnf(u2639,negated_conjecture,
ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0) = X0 ).
cnf(u74,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(specific(X0,X2),true,specific(X1,X2),true),true) ).
cnf(u2116,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,agent(X0,skc12,skc10),true) ).
cnf(u590,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc9),true) ).
cnf(u1794,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc11),true) ).
cnf(u329,negated_conjecture,
true = impartial(skc8,skc10) ).
cnf(u2508,negated_conjecture,
skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(agent(skc8,X0,X1),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(think_believe_consider(skc8,X0),true,skc11,skc11),skc11),skc11),skc11) ).
cnf(u613,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u845,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc12),true) ).
cnf(u72,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(singleton(X0,X2),true,singleton(X1,X2),true),true) ).
cnf(u1367,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(existent(X0,skc10),true,true,true),true) ).
cnf(u2386,negated_conjecture,
skc13 = ifeq3(of(skc8,skc13,X0),true,ifeq3(of(skc8,skc13,X0),true,ifeq3(entity(skc8,X0),true,skc13,skc13),skc13),skc13) ).
cnf(u1489,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,male(X0,skc10),true) ).
cnf(u611,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).
cnf(u2113,negated_conjecture,
true = agent(skc11,skc12,skc10) ).
cnf(u843,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,nonexistent(X0,skc12),true) ).
cnf(u1140,negated_conjecture,
true = male(skc11,skc10) ).
cnf(u457,negated_conjecture,
b = ifeq(tuple(true,existent(skc8,skc12)),tuple(true,true),a,b) ).
cnf(u2140,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,theme(X0,skc12,skc11),true) ).
cnf(u2014,negated_conjecture,
true = proposition(skc11,skc11) ).
cnf(u741,negated_conjecture,
true = specific(skc11,skc10) ).
cnf(u1647,negated_conjecture,
true = ifeq2(relation(skc8,X0),true,relation(skc11,X0),true) ).
cnf(u2018,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,proposition(X0,skc11),true) ).
cnf(u463,negated_conjecture,
true = ifeq2(state(skc8,X0),true,state(skc11,X0),true) ).
cnf(u356,negated_conjecture,
true = abstraction(skc8,skc13) ).
cnf(u486,negated_conjecture,
true = ifeq2(entity(skc11,skc9),true,true,true) ).
cnf(u112,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(general(X0,X2),true,general(X1,X2),true),true) ).
cnf(u615,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc12),true) ).
cnf(u2146,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,theme(X0,skc12,skc11),true) ).
cnf(u229,negated_conjecture,
true = sF13 ).
cnf(u992,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc12),true) ).
cnf(u729,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skc9),true,true,true),true) ).
cnf(u2947,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,skc11,skc11),skc11),skc11),skc11),skc11) ).
cnf(u118,axiom,
true = ifeq2(present(X0,X1),true,ifeq2(accessible_world(X0,X2),true,present(X2,X1),true),true) ).
cnf(u1535,negated_conjecture,
b = ifeq(tuple(human(skc11,skc13),true),tuple(true,true),a,b) ).
cnf(u743,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skc10),true,true,true),true) ).
cnf(u618,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc10),true) ).
cnf(u13,axiom,
true = ifeq2(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u373,negated_conjecture,
true = singleton(skc8,skc13) ).
cnf(u503,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc9),true) ).
cnf(u2948,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(theme(skc11,X0,skc11),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,X0),true,skc11,skc11),skc11),skc11),skc11),skc11) ).
cnf(u1667,negated_conjecture,
b = ifeq(tuple(specific(skc11,skc11),true),tuple(true,true),a,b) ).
cnf(u246,negated_conjecture,
true = vincent_forename(skc8,skc13) ).
cnf(u1029,negated_conjecture,
b = ifeq(tuple(true,male(skc11,skc13)),tuple(true,true),a,b) ).
cnf(u527,negated_conjecture,
b = ifeq(tuple(true,general(skc11,skc12)),tuple(true,true),a,b) ).
cnf(u2065,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,of(X0,skc13,skc10),true) ).
cnf(u1564,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(relname(X0,skc13),true,true,true),true) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u1414,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(living(X0,skc10),true,true,true),true) ).
cnf(u287,negated_conjecture,
true = unisex(skc8,skc12) ).
cnf(u501,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,eventuality(X0,skc9),true) ).
cnf(u253,negated_conjecture,
true = man(skc8,skc10) ).
cnf(u96,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human(X0,X2),true,human(X1,X2),true),true) ).
cnf(u641,negated_conjecture,
true = ifeq2(eventuality(skc11,skc11),true,true,true) ).
cnf(u1686,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc13),true) ).
cnf(u2056,negated_conjecture,
true = ifeq2(of(X0,skc13,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u655,negated_conjecture,
true = ifeq2(entity(skc11,skc13),true,true,true) ).
cnf(u1418,negated_conjecture,
true = ifeq2(living(skc8,X0),true,living(skc11,X0),true) ).
cnf(u1817,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc13),true,true,true),true) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u285,negated_conjecture,
true = specific(skc8,skc12) ).
cnf(u2826,negated_conjecture,
skc11 = ifeq3(theme(skc8,X1,skc11),true,ifeq3(theme(skc8,X2,skc11),true,ifeq3(agent(skc8,X1,X0),true,ifeq3(agent(skc8,X2,X0),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(think_believe_consider(skc8,X2),true,skc11,skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u1161,negated_conjecture,
true = living(skc11,skc10) ).
cnf(u2708,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11) ).
cnf(u1416,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,living(X0,skc10),true) ).
cnf(u658,negated_conjecture,
true = singleton(skc11,skc13) ).
cnf(u43,axiom,
true = ifeq2(forename(X0,X1),true,relname(X0,X1),true) ).
cnf(u1174,negated_conjecture,
true = eventuality(skc11,skf1(X0)) ).
cnf(u413,negated_conjecture,
true = singleton(skc8,skc11) ).
cnf(u41,axiom,
true = ifeq2(man(X0,X1),true,male(X0,X1),true) ).
cnf(u286,negated_conjecture,
true = nonexistent(skc8,skc12) ).
cnf(u2468,negated_conjecture,
ifeq3(theme(skc8,skc12,X3),true,ifeq3(theme(skc8,X2,X1),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,X2,X0),true,ifeq3(think_believe_consider(skc8,X2),true,ifeq3(proposition(skc8,X3),true,ifeq3(proposition(skc8,X1),true,X1,X3),X3),X3),X3),X3),X3),X3) = X3 ).
cnf(u1187,negated_conjecture,
true = specific(skc11,skf1(X0)) ).
cnf(u2109,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,agent(X0,skf1(skc10),skc10),true) ).
cnf(u1176,negated_conjecture,
true = ifeq2(eventuality(skc8,skf1(X0)),true,true,true) ).
cnf(u47,axiom,
true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u1666,negated_conjecture,
b = ifeq(tuple(human(skc11,skc11),true),tuple(true,true),a,b) ).
cnf(u668,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc11),true,true,true),true) ).
cnf(u1958,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,present(X0,skc12),true) ).
cnf(u424,negated_conjecture,
true = be(skc8,skc9,skc10,skc10) ).
cnf(u2487,negated_conjecture,
ifeq3(theme(skc11,X2,X1),true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(agent(skc11,X2,skc10),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u2237,negated_conjecture,
ifeq3(of(skc11,X0,skc10),true,ifeq3(forename(skc11,X0),true,skc13,X0),X0) = X0 ).
cnf(u839,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc9),true,true,true),true) ).
cnf(u1212,negated_conjecture,
true = singleton(skc11,skf1(X0)) ).
cnf(u443,negated_conjecture,
b = ifeq(tuple(true,male(skc8,skc11)),tuple(true,true),a,b) ).
cnf(u1941,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(smoke(X1,skf1(X0)),true,true,true),true) ).
cnf(u186,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u1345,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,entity(X0,skc10),true) ).
cnf(u441,negated_conjecture,
b = ifeq(tuple(true,male(skc8,skc13)),tuple(true,true),a,b) ).
cnf(u597,negated_conjecture,
true = ifeq2(thing(skc8,X0),true,thing(skc11,X0),true) ).
cnf(u184,axiom,
b = ifeq(tuple(human(X0,X1),nonhuman(X0,X1)),tuple(true,true),a,b) ).
cnf(u595,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc13),true) ).
cnf(u1639,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc11),true,true,true),true) ).
cnf(u842,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonexistent(X0,skc12),true,true,true),true) ).
cnf(u2139,negated_conjecture,
true = ifeq2(theme(skc8,X1,X0),true,theme(skc11,X1,X0),true) ).
cnf(u614,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc12),true,true,true),true) ).
cnf(u2509,negated_conjecture,
ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1) = X1 ).
cnf(u353,negated_conjecture,
true = relation(skc8,skc13) ).
cnf(u620,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc12),true) ).
cnf(u585,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc10),true,true,true),true) ).
cnf(u2198,negated_conjecture,
ifeq3(of(skc8,skc13,X1),true,ifeq3(of(skc8,X0,X1),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,X1),true,skc13,X0),X0),X0),X0) = X0 ).
cnf(u1391,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(impartial(X0,skc10),true,true,true),true) ).
cnf(u1486,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(male(X0,skc10),true,true,true),true) ).
cnf(u481,negated_conjecture,
true = nonexistent(skc11,skc9) ).
cnf(u2932,negated_conjecture,
ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,X1,skc10),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1651,negated_conjecture,
true = relation(skc11,skc11) ).
cnf(u102,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(forename(X0,X2),true,forename(X1,X2),true),true) ).
cnf(u997,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc13),true) ).
cnf(u1640,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(relation(X0,skc13),true,true,true),true) ).
cnf(u2143,negated_conjecture,
true = theme(skc11,skc12,skc11) ).
cnf(u1490,negated_conjecture,
true = ifeq2(male(skc8,X0),true,male(skc11,X0),true) ).
cnf(u995,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc11),true) ).
cnf(u608,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc13),true,true,true),true) ).
cnf(u2011,negated_conjecture,
true = ifeq2(proposition(skc8,X0),true,proposition(skc11,X0),true) ).
cnf(u1141,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,man(X0,skc10),true) ).
cnf(u639,negated_conjecture,
true = ifeq2(entity(skc11,skc11),true,true,true) ).
cnf(u1488,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,male(X0,skc10),true) ).
cnf(u730,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skc12),true,true,true),true) ).
cnf(u1526,negated_conjecture,
true = relation(skc11,skc13) ).
cnf(u1797,negated_conjecture,
true = ifeq2(nonhuman(skc8,X0),true,nonhuman(skc11,X0),true) ).
cnf(u271,negated_conjecture,
true = unisex(skc8,skc9) ).
cnf(u485,negated_conjecture,
true = ifeq2(abstraction(skc11,skc9),true,true,true) ).
cnf(u736,negated_conjecture,
true = ifeq2(specific(skc8,X0),true,specific(skc11,X0),true) ).
cnf(u370,negated_conjecture,
true = ifeq2(entity(skc8,skc13),true,true,true) ).
cnf(u1145,negated_conjecture,
true = agent(skc11,skf1(skc10),skc10) ).
cnf(u1795,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc13),true) ).
cnf(u2168,negated_conjecture,
true = ifeq2(be(X0,skc9,skc10,skc10),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u2579,negated_conjecture,
ifeq3(theme(skc8,skc12,X1),true,ifeq3(theme(skc8,skc12,X0),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X0),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u1524,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,forename(X0,skc13),true) ).
cnf(u269,negated_conjecture,
true = nonexistent(skc8,skc9) ).
cnf(u520,negated_conjecture,
true = unisex(skc11,skc12) ).
cnf(u498,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc9),true,true,true),true) ).
cnf(u1014,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc12),true,true,true),true) ).
cnf(u642,negated_conjecture,
true = singleton(skc11,skc11) ).
cnf(u2321,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(jules_forename(X0,skc13),true,true,true),true) ).
cnf(u27,axiom,
true = ifeq2(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u241,negated_conjecture,
true = sF17 ).
cnf(u1020,negated_conjecture,
true = ifeq2(event(skc8,X0),true,event(skc11,X0),true) ).
cnf(u397,negated_conjecture,
true = ifeq2(proposition(skc8,skc13),true,true,true) ).
cnf(u1943,negated_conjecture,
true = ifeq2(smoke(skc8,X0),true,smoke(skc11,X0),true) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u2324,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(jules_forename(X0,skc13),true,true,true),true) ).
cnf(u1043,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(event(X0,skc12),true,true,true),true) ).
cnf(u1312,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,organism(X0,skc10),true) ).
cnf(u252,negated_conjecture,
true = accessible_world(skc8,skc11) ).
cnf(u1032,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc13),true) ).
cnf(u25,axiom,
true = ifeq2(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u309,negated_conjecture,
true = ifeq2(eventuality(skc8,skc10),true,true,true) ).
cnf(u387,negated_conjecture,
true = unisex(skc8,skc13) ).
cnf(u1394,negated_conjecture,
true = ifeq2(impartial(skc8,X0),true,impartial(skc11,X0),true) ).
cnf(u2197,negated_conjecture,
ifeq3(of(skc11,skc13,X1),true,ifeq3(of(skc11,X0,X1),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,X1),true,skc13,X0),X0),X0),X0) = X0 ).
cnf(u410,negated_conjecture,
true = ifeq2(entity(skc8,skc11),true,true,true) ).
cnf(u130,axiom,
true = ifeq2(theme(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).
cnf(u1417,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,living(X0,skc10),true) ).
cnf(u539,negated_conjecture,
true = ifeq2(accessible_world(skc11,skc8),true,true,true) ).
cnf(u2561,negated_conjecture,
skc11 = ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11) ).
cnf(u1160,negated_conjecture,
true = impartial(skc11,skc10) ).
cnf(u31,axiom,
true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u1818,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc11),true,true,true),true) ).
cnf(u1198,negated_conjecture,
b = ifeq(tuple(true,existent(skc11,skf1(X0))),tuple(true,true),a,b) ).
cnf(u652,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc13),true,true,true),true) ).
cnf(u1942,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,smoke(X1,skf1(X0)),true) ).
cnf(u408,negated_conjecture,
true = general(skc8,skc11) ).
cnf(u1948,negated_conjecture,
true = ifeq2(present(X0,skc12),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u80,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(event(X0,X2),true,event(X1,X2),true),true) ).
cnf(u1196,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(nonexistent(X1,skf1(X0)),true,true,true),true) ).
cnf(u1952,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,present(X0,skc12),true) ).
cnf(u2114,negated_conjecture,
true = ifeq2(agent(X0,skc12,skc10),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u1200,negated_conjecture,
true = ifeq2(specific(skc8,skf1(X0)),true,true,true) ).
cnf(u2108,negated_conjecture,
true = ifeq2(agent(skc8,X1,X0),true,agent(skc11,X1,X0),true) ).
cnf(u2502,negated_conjecture,
skc11 = ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,skc12,X2),true,ifeq3(agent(skc8,X0,X2),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).
cnf(u1342,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(entity(X0,skc10),true,true,true),true) ).
cnf(u199,negated_conjecture,
true = sF3 ).
cnf(u1986,negated_conjecture,
true = ifeq2(think_believe_consider(skc8,X0),true,think_believe_consider(skc11,X0),true) ).
cnf(u337,negated_conjecture,
true = human(skc8,skc10) ).
cnf(u324,negated_conjecture,
true = existent(skc8,skc10) ).
cnf(u454,negated_conjecture,
b = ifeq(tuple(human(skc8,skc13),true),tuple(true,true),a,b) ).
cnf(u2760,negated_conjecture,
ifeq3(theme(skc11,skf1(skc10),X1),true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X0),true,X0,X1),X1),X1),X1),X1) = X1 ).
cnf(u583,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc12),true,true,true),true) ).
cnf(u1346,negated_conjecture,
true = ifeq2(entity(skc8,X0),true,entity(skc11,X0),true) ).
cnf(u2251,negated_conjecture,
true = jules_forename(skc8,skc13) ).
cnf(u726,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc12),true,true,true),true) ).
cnf(u465,negated_conjecture,
true = ifeq2(accessible_world(skc8,skc8),true,true,true) ).
cnf(u452,negated_conjecture,
b = ifeq(tuple(true,nonhuman(skc8,skc10)),tuple(true,true),a,b) ).
cnf(u2499,negated_conjecture,
ifeq3(theme(skc11,X2,X1),true,ifeq3(agent(skc11,X2,X0),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1),X1) = X1 ).
cnf(u86,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(organism(X0,X2),true,organism(X1,X2),true),true) ).
cnf(u208,negated_conjecture,
true = sF6 ).
cnf(u586,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u2463,negated_conjecture,
skc11 = ifeq3(theme(skc11,X3,skc11),true,ifeq3(theme(skc11,X2,X1),true,ifeq3(agent(skc11,X3,X0),true,ifeq3(agent(skc11,X2,X0),true,ifeq3(think_believe_consider(skc11,X3),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u341,negated_conjecture,
true = animate(skc8,skc10) ).
cnf(u592,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc10),true) ).
cnf(u471,negated_conjecture,
true = eventuality(skc11,skc9) ).
cnf(u2138,negated_conjecture,
true = ifeq2(theme(X0,skc12,skc11),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u609,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc12),true,true,true),true) ).
cnf(u1654,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(relation(X0,skc11),true,true,true),true) ).
cnf(u214,negated_conjecture,
true = sF8 ).
cnf(u1125,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(man(X0,skc10),true,true,true),true) ).
cnf(u623,negated_conjecture,
true = ifeq2(singleton(skc8,X0),true,singleton(skc11,X0),true) ).
cnf(u994,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc9),true) ).
cnf(u1660,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,relation(X0,skc11),true) ).
cnf(u2461,negated_conjecture,
ifeq3(theme(skc11,X3,X2),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,X3,X0),true,ifeq3(agent(skc11,X1,X0),true,ifeq3(think_believe_consider(skc11,X3),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X2),true,skc11,X2),X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u2193,negated_conjecture,
skc13 = ifeq3(of(skc11,X1,X0),true,ifeq3(of(skc11,skc13,X0),true,ifeq3(forename(skc11,X1),true,ifeq3(entity(skc11,X0),true,X1,skc13),skc13),skc13),skc13) ).
cnf(u492,negated_conjecture,
b = ifeq(tuple(true,male(skc11,skc9)),tuple(true,true),a,b) ).
cnf(u126,axiom,
true = ifeq2(of(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).
cnf(u1514,negated_conjecture,
true = ifeq2(forename(skc8,X0),true,forename(skc11,X0),true) ).
cnf(u2798,negated_conjecture,
ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,skf1(skc10),X1),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(u381,negated_conjecture,
true = general(skc8,skc13) ).
cnf(u632,negated_conjecture,
true = thing(skc11,skc11) ).
cnf(u511,negated_conjecture,
true = ifeq2(state(skc11,skc12),true,true,true) ).
cnf(u1135,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(man(X0,skc10),true,true,true),true) ).
cnf(u482,negated_conjecture,
true = unisex(skc11,skc9) ).
cnf(u124,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(vincent_forename(X0,X2),true,vincent_forename(X1,X2),true),true) ).
cnf(u2035,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,vincent_forename(X0,skc13),true) ).
cnf(u254,negated_conjecture,
true = state(skc8,skc9) ).
cnf(u1512,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,forename(X0,skc13),true) ).
cnf(u1146,negated_conjecture,
true = ifeq2(man(skc11,X0),true,true,true) ).
cnf(u2041,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(vincent_forename(X0,skc13),true,true,true),true) ).
cnf(u2572,negated_conjecture,
skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,X0,skc10),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).
cnf(u11,axiom,
true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u509,negated_conjecture,
true = eventuality(skc11,skc12) ).
cnf(u480,negated_conjecture,
true = specific(skc11,skc9) ).
cnf(u114,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(jules_forename(X0,X2),true,jules_forename(X1,X2),true),true) ).
cnf(u1824,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,general(X0,skc13),true) ).
cnf(u1027,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc13),true,true,true),true) ).
cnf(u2694,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(agent(skc11,X0,X1),true,ifeq3(think_believe_consider(skc11,X0),true,skc11,skc11),skc11),skc11),skc11) ).
cnf(u1165,negated_conjecture,
true = existent(skc11,skc10) ).
cnf(u1144,negated_conjecture,
true = event(skc11,skf1(X0)) ).
cnf(u1023,negated_conjecture,
b = ifeq(tuple(true,male(skc11,skc11)),tuple(true,true),a,b) ).
cnf(u9,axiom,
true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u499,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc12),true,true,true),true) ).
cnf(u525,negated_conjecture,
true = ifeq2(abstraction(skc11,skc12),true,true,true) ).
cnf(u15,axiom,
true = ifeq2(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u1047,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,event(X0,skc12),true) ).
cnf(u394,negated_conjecture,
true = ifeq2(smoke(skc8,skc9),true,true,true) ).
cnf(u242,negated_conjecture,
true = actual_world(skc8) ).
cnf(u1529,negated_conjecture,
true = abstraction(skc11,skc13) ).
cnf(u523,negated_conjecture,
true = thing(skc11,skc12) ).
cnf(u2560,negated_conjecture,
skc11 = ifeq3(theme(skc8,X1,skc11),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,X1,X0),true,ifeq3(think_believe_consider(skc8,X1),true,skc11,skc11),skc11),skc11),skc11) ).
cnf(u2695,negated_conjecture,
skc11 = ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11) ).
cnf(u2325,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,jules_forename(X0,skc13),true) ).
cnf(u1175,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,event(X1,skf1(X0)),true) ).
cnf(u1313,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,organism(X0,skc10),true) ).
cnf(u2810,negated_conjecture,
ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0) = X0 ).
cnf(u651,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc10),true) ).
cnf(u49,axiom,
true = ifeq2(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u304,negated_conjecture,
true = ifeq2(entity(skc8,skc9),true,true,true) ).
cnf(u398,negated_conjecture,
true = relation(skc8,skc11) ).
cnf(u1441,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,human(X0,skc10),true) ).
cnf(u1195,negated_conjecture,
true = ifeq2(nonexistent(skc8,skf1(X0)),true,true,true) ).
cnf(u2110,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,agent(X0,skc12,skc10),true) ).
cnf(u670,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc11),true) ).
cnf(u1184,negated_conjecture,
true = ifeq2(accessible_world(skc11,X1),true,eventuality(X1,skf1(X0)),true) ).
cnf(u55,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u1687,negated_conjecture,
true = ifeq2(abstraction(skc8,X0),true,abstraction(skc11,X0),true) ).
cnf(u1562,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relname(X0,skc13),true,true,true),true) ).
cnf(u409,negated_conjecture,
true = unisex(skc8,skc11) ).
cnf(u676,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc13),true) ).
cnf(u310,negated_conjecture,
true = singleton(skc8,skc10) ).
cnf(u524,negated_conjecture,
b = ifeq(tuple(true,male(skc11,skc12)),tuple(true,true),a,b) ).
cnf(u1447,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(animate(X0,skc10),true,true,true),true) ).
cnf(u2466,negated_conjecture,
ifeq3(theme(skc8,X3,X2),true,ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,X3,X0),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(think_believe_consider(skc8,X3),true,ifeq3(proposition(skc8,X2),true,ifeq3(proposition(skc8,X1),true,X1,X2),X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u2107,negated_conjecture,
true = ifeq2(agent(X0,skf1(skc10),skc10),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u2238,negated_conjecture,
ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,skc13,X0),X0) = X0 ).
cnf(u53,axiom,
true = ifeq2(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u1223,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(human_person(X0,skc10),true,true,true),true) ).
cnf(u582,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc13),true,true,true),true) ).
cnf(u2490,negated_conjecture,
ifeq3(theme(skc8,skc12,X2),true,ifeq3(theme(skc8,X1,X0),true,ifeq3(agent(skc8,X1,skc10),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X2),true,ifeq3(proposition(skc8,X0),true,X0,X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u588,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc12),true,true,true),true) ).
cnf(clause35,axiom,
ifeq3(be(X0,X1,X2,X3),true,X2,X3) = X3 ).
cnf(u1201,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(specific(X1,skf1(X0)),true,true,true),true) ).
cnf(u70,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(thing(X0,X2),true,thing(X1,X2),true),true) ).
cnf(u1366,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(existent(X0,skc10),true,true,true),true) ).
cnf(u3041,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11),skc11),skc11) ).
cnf(u455,negated_conjecture,
b = ifeq(tuple(human(skc8,skc11),true),tuple(true,true),a,b) ).
cnf(u593,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc11),true) ).
cnf(u348,negated_conjecture,
true = relname(skc8,skc13) ).
cnf(u1638,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc13),true,true,true),true) ).
cnf(u68,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).
cnf(u846,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc9),true) ).
cnf(u1370,negated_conjecture,
true = ifeq2(existent(skc8,X0),true,existent(skc11,X0),true) ).
cnf(u1644,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc11),true) ).
cnf(u1985,negated_conjecture,
true = ifeq2(think_believe_consider(X0,skc12),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u2250,negated_conjecture,
skc15 = skc13 ).
cnf(u110,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).
cnf(u196,negated_conjecture,
true = sF2 ).
cnf(u2510,negated_conjecture,
ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc10),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1) = X1 ).
cnf(u1368,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,existent(X0,skc10),true) ).
cnf(u735,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc12),true) ).
cnf(u610,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc11),true,true,true),true) ).
cnf(u211,negated_conjecture,
true = sF7 ).
cnf(u1126,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,man(X0,skc10),true) ).
cnf(u365,negated_conjecture,
true = thing(skc8,skc13) ).
cnf(u616,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc9),true) ).
cnf(u2167,negated_conjecture,
true = be(skc11,skc9,skc10,skc10) ).
cnf(u3016,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u466,negated_conjecture,
true = state(skc11,skc9) ).
cnf(u108,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).
cnf(u238,negated_conjecture,
true = sF16 ).
cnf(u1130,negated_conjecture,
true = man(skc11,skc10) ).
cnf(u988,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc11),true,true,true),true) ).
cnf(u2039,negated_conjecture,
true = vincent_forename(skc11,skc13) ).
cnf(u444,negated_conjecture,
b = ifeq(tuple(true,male(skc8,skc9)),tuple(true,true),a,b) ).
cnf(u98,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(animate(X0,X2),true,animate(X1,X2),true),true) ).
cnf(u993,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc9),true) ).
cnf(u1139,negated_conjecture,
true = human_person(skc11,skc10) ).
cnf(u251,negated_conjecture,
true = proposition(skc8,skc11) ).
cnf(u226,negated_conjecture,
true = sF12 ).
cnf(u249,negated_conjecture,
true = present(skc8,skc12) ).
cnf(u267,negated_conjecture,
true = specific(skc8,skc9) ).
cnf(u1166,negated_conjecture,
b = ifeq(tuple(nonexistent(skc11,skc10),true),tuple(true,true),a,b) ).
cnf(u748,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skc10),true) ).
cnf(u504,negated_conjecture,
true = ifeq2(eventuality(skc8,X0),true,eventuality(skc11,X0),true) ).
cnf(u1159,negated_conjecture,
true = entity(skc11,skc10) ).
cnf(u526,negated_conjecture,
b = ifeq(tuple(true,existent(skc11,skc12)),tuple(true,true),a,b) ).
cnf(u33,axiom,
true = ifeq2(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u265,negated_conjecture,
true = singleton(skc8,skc9) ).
cnf(u532,negated_conjecture,
true = singleton(skc11,skc12) ).
cnf(u1822,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,general(X0,skc11),true) ).
cnf(u2322,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,jules_forename(X0,skc13),true) ).
cnf(u1828,negated_conjecture,
true = ifeq2(general(skc8,X0),true,general(skc11,X0),true) ).
cnf(u39,axiom,
true = ifeq2(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u1826,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc13),true) ).
cnf(u1016,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(event(X0,skc9),true,true,true),true) ).
cnf(u393,negated_conjecture,
true = ifeq2(smoke(skc8,skc12),true,true,true) ).
cnf(u1950,negated_conjecture,
true = ifeq2(present(skc8,X0),true,present(skc11,X0),true) ).
cnf(u1214,negated_conjecture,
true = ifeq2(singleton(skc8,skf1(X0)),true,true,true) ).
cnf(u1569,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,relname(X0,skc13),true) ).
cnf(u1956,negated_conjecture,
true = ifeq2(present(X0,skc12),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u1207,negated_conjecture,
true = ifeq2(accessible_world(X1,skc11),true,ifeq2(thing(X1,skf1(X0)),true,true,true),true) ).
cnf(u37,axiom,
true = ifeq2(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u1954,negated_conjecture,
true = ifeq2(present(skc8,skf1(X0)),true,true,true) ).
cnf(u305,negated_conjecture,
true = ifeq2(entity(skc8,skc12),true,true,true) ).
cnf(u292,negated_conjecture,
true = human_person(skc8,skc10) ).
cnf(u1440,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,human(X0,skc10),true) ).
cnf(u422,negated_conjecture,
true = agent(skc8,skc12,skc10) ).
cnf(u1343,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(entity(X0,skc10),true,true,true),true) ).
cnf(u1680,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(abstraction(X0,skc11),true,true,true),true) ).
cnf(u1314,negated_conjecture,
true = ifeq2(organism(skc8,X0),true,organism(skc11,X0),true) ).
cnf(u1438,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human(X0,skc10),true,true,true),true) ).
cnf(u2528,negated_conjecture,
skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(agent(skc8,X0,skc10),true,ifeq3(think_believe_consider(skc8,X0),true,skc11,skc11),skc11),skc11) ).
cnf(u2470,negated_conjecture,
ifeq3(theme(skc11,X2,X1),true,ifeq3(theme(skc11,skf1(skc10),X0),true,ifeq3(agent(skc11,X2,skc10),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u2467,negated_conjecture,
ifeq3(theme(skc11,skc12,X3),true,ifeq3(theme(skc11,X2,X1),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,X2,X0),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X3),true,ifeq3(proposition(skc11,X1),true,X1,X3),X3),X3),X3),X3),X3),X3) = X3 ).
cnf(u3015,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skf1(skc10),X1),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).
cnf(u1442,negated_conjecture,
true = ifeq2(human(skc8,X0),true,human(skc11,X0),true) ).
cnf(u2144,negated_conjecture,
true = ifeq2(theme(X0,skc12,skc11),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).
cnf(u333,negated_conjecture,
true = living(skc8,skc10) ).
cnf(u2106,negated_conjecture,
true = ifeq2(agent(X0,skc12,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).
cnf(u2233,negated_conjecture,
skc13 = ifeq3(of(skc11,X0,skc10),true,ifeq3(forename(skc11,X0),true,X0,skc13),skc13) ).
cnf(u2884,negated_conjecture,
ifeq3(theme(skc8,skc12,X1),true,ifeq3(theme(skc8,skc12,X2),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1185,negated_conjecture,
true = unisex(skc11,skf1(X0)) ).
cnf(u182,axiom,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).
cnf(u2488,negated_conjecture,
ifeq3(theme(skc8,X2,X1),true,ifeq3(theme(skc8,skc12,X0),true,ifeq3(agent(skc8,X2,skc10),true,ifeq3(think_believe_consider(skc8,X2),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u986,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc13),true,true,true),true) ).
cnf(u2501,negated_conjecture,
skc11 = ifeq3(theme(skc11,X2,X1),true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,X2,X0),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).
cnf(u840,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc12),true,true,true),true) ).
cnf(u2234,negated_conjecture,
skc13 = ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,X0,skc13),skc13) ).
cnf(u180,axiom,
b = ifeq(tuple(unisex(X0,X1),male(X0,X1)),tuple(true,true),a,b) ).
cnf(u591,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc9),true) ).
cnf(u205,negated_conjecture,
true = sF5 ).
cnf(u2655,negated_conjecture,
skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(agent(skc11,X0,skc10),true,ifeq3(think_believe_consider(skc11,X0),true,skc11,skc11),skc11),skc11) ).
cnf(u94,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(living(X0,X2),true,living(X1,X2),true),true) ).
cnf(u2120,negated_conjecture,
true = ifeq2(agent(skc8,skf1(skc10),skc10),true,true,true) ).
cnf(u594,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc12),true) ).
cnf(u844,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,nonexistent(X0,skc9),true) ).
cnf(u2766,negated_conjecture,
ifeq3(theme(skc11,skc12,X1),true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X0),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u450,negated_conjecture,
b = ifeq(tuple(specific(skc8,skc13),true),tuple(true,true),a,b) ).
cnf(u1225,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,human_person(X0,skc10),true) ).
cnf(u92,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(impartial(X0,X2),true,impartial(X1,X2),true),true) ).
cnf(u2009,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(proposition(X0,skc11),true,true,true),true) ).
cnf(u193,negated_conjecture,
true = sF1 ).
cnf(u728,negated_conjecture,
true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc9),true,true,true),true) ).
cnf(u362,negated_conjecture,
true = ifeq2(abstraction(skc8,skc10),true,true,true) ).
cnf(u448,negated_conjecture,
b = ifeq(tuple(true,general(skc8,skc9)),tuple(true,true),a,b) ).
cnf(u82,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(man(X0,X2),true,man(X1,X2),true),true) ).
cnf(u1369,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,existent(X0,skc10),true) ).
cnf(u220,negated_conjecture,
true = sF10 ).
cnf(u1392,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,impartial(X0,skc10),true) ).
cnf(u991,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc12),true,true,true),true) ).
cnf(u235,negated_conjecture,
true = sF15 ).
cnf(u467,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(state(X0,skc9),true,true,true),true) ).
cnf(u621,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc13),true) ).
cnf(u1143,negated_conjecture,
true = present(skc11,skf1(X0)) ).
cnf(u1992,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,think_believe_consider(X0,skc12),true) ).
cnf(u2650,negated_conjecture,
skc11 = ifeq3(theme(skc11,skf1(skc10),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,skc11,skc11),skc11) ).
cnf(u619,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc11),true) ).
cnf(u1006,negated_conjecture,
true = unisex(skc11,skc11) ).
cnf(u2473,negated_conjecture,
ifeq3(theme(skc11,skf1(skc10),X2),true,ifeq3(theme(skc11,X1,X0),true,ifeq3(agent(skc11,X1,skc10),true,ifeq3(think_believe_consider(skc11,skf1(skc10)),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X2),true,ifeq3(proposition(skc11,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).
cnf(u2739,negated_conjecture,
ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,X1,skc11),true,ifeq3(agent(skc8,X1,skc10),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X0),true,skc11,X0),X0),X0),X0),X0) = X0 ).
cnf(u732,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skc9),true) ).
cnf(u488,negated_conjecture,
true = singleton(skc11,skc9) ).
cnf(u122,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(proposition(X0,X2),true,proposition(X1,X2),true),true) ).
cnf(u1017,negated_conjecture,
true = ifeq2(accessible_world(skc11,X0),true,event(X0,skc9),true) ).
cnf(u2164,negated_conjecture,
true = ifeq2(accessible_world(skc8,X0),true,be(X0,skc9,skc10,skc10),true) ).
cnf(u1533,negated_conjecture,
true = nonhuman(skc11,skc13) ).
cnf(u377,negated_conjecture,
true = nonhuman(skc8,skc13) ).
cnf(u120,axiom,
true = ifeq2(think_believe_consider(X0,X1),true,ifeq2(accessible_world(X0,X2),true,think_believe_consider(X2,X1),true),true) ).
cnf(u250,negated_conjecture,
true = event(skc8,skc12) ).
cnf(u1163,negated_conjecture,
b = ifeq(tuple(true,nonhuman(skc11,skc10)),tuple(true,true),a,b) ).
cnf(u1523,negated_conjecture,
true = relname(skc11,skc13) ).
cnf(u1152,negated_conjecture,
true = organism(skc11,skc10) ).
cnf(u23,axiom,
true = ifeq2(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u21,axiom,
true = ifeq2(man(X0,X1),true,human_person(X0,X1),true) ).
cnf(u1658,negated_conjecture,
true = ifeq2(relname(skc11,skc11),true,true,true) ).
cnf(u644,negated_conjecture,
true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc10),true,true,true),true) ).
cnf(u278,negated_conjecture,
true = eventuality(skc8,skc12) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP225-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 18:33:09 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 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
% 12.88/2.85 % (1519723)Detected a unit-equality problem, will run specialized UEQ schedule.
% 12.88/2.85 % (1519741)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=1971918005:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 12.88/2.85 % (1519745)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2631895337:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 12.88/2.85 % (1519742)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=3266889596:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 12.88/2.85 % (1519743)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3636956424:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 12.88/2.85 % (1519746)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2536221846:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 12.88/2.85 % (1519747)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1399641853:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 12.88/2.85 % (1519744)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2919989175:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 12.88/2.85 % (1519745)Instruction limit reached!
% 12.88/2.85 % (1519745)------------------------------
% 12.88/2.85 % (1519745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519745)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519745)Termination reason: Instruction limit
% 12.88/2.85 % (1519745)Termination phase: Saturation
% 12.88/2.85 % (1519745)Time elapsed: 0.125 s
% 12.88/2.85 % (1519745)Peak memory usage: 89 MB
% 12.88/2.85 % (1519745)Instructions burned: 181 (million)
% 12.88/2.85 % (1519744)Instruction limit reached!
% 12.88/2.85 % (1519744)------------------------------
% 12.88/2.85 % (1519744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519744)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519744)Termination reason: Instruction limit
% 12.88/2.85 % (1519744)Termination phase: Saturation
% 12.88/2.85 % (1519744)Time elapsed: 0.116 s
% 12.88/2.85 % (1519744)Peak memory usage: 87 MB
% 12.88/2.85 % (1519744)Instructions burned: 137 (million)
% 12.88/2.85 % (1519746)Instruction limit reached!
% 12.88/2.85 % (1519746)------------------------------
% 12.88/2.85 % (1519746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519747)Refutation not found, incomplete strategy
% 12.88/2.85 % (1519747)------------------------------
% 12.88/2.85 % (1519747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519746)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519746)Termination reason: Instruction limit
% 12.88/2.85 % (1519746)Termination phase: Saturation
% 12.88/2.85 % (1519746)Time elapsed: 0.235 s
% 12.88/2.85 % (1519746)Peak memory usage: 91 MB
% 12.88/2.85 % (1519747)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519746)Instructions burned: 257 (million)
% 12.88/2.85 % (1519747)Termination reason: Refutation not found, incomplete strategy
% 12.88/2.85 % (1519747)Time elapsed: 0.235 s
% 12.88/2.85 % (1519747)Peak memory usage: 90 MB
% 12.88/2.85 % (1519747)Instructions burned: 255 (million)
% 12.88/2.85 % (1519772)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1919315640:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 12.88/2.85 % (1519765)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1725233961:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 12.88/2.85 % (1519774)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2881079108:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 12.88/2.85 % (1519774)Instruction limit reached!
% 12.88/2.85 % (1519774)------------------------------
% 12.88/2.85 % (1519774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519774)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519774)Termination reason: Instruction limit
% 12.88/2.85 % (1519774)Termination phase: Saturation
% 12.88/2.85 % (1519774)Time elapsed: 0.170 s
% 12.88/2.85 % (1519774)Peak memory usage: 92 MB
% 12.88/2.85 % (1519774)Instructions burned: 215 (million)
% 12.88/2.85 % (1519747)------------------------------
% 12.88/2.85 % (1519747)------------------------------
% 12.88/2.85 % (1519783)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=677541943:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 12.88/2.85 % (1519784)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=2767972307:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 12.88/2.85 % (1519783)Instruction limit reached!
% 12.88/2.85 % (1519783)------------------------------
% 12.88/2.85 % (1519783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519783)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519783)Termination reason: Instruction limit
% 12.88/2.85 % (1519783)Termination phase: Saturation
% 12.88/2.85 % (1519783)Time elapsed: 0.243 s
% 12.88/2.85 % (1519783)Peak memory usage: 95 MB
% 12.88/2.85 % (1519783)Instructions burned: 318 (million)
% 12.88/2.85 % (1519741)Refutation not found, incomplete strategy
% 12.88/2.85 % (1519741)------------------------------
% 12.88/2.85 % (1519741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.88/2.85 % (1519741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.88/2.85 % (1519741)CaDiCaL version: 2.1.3
% 12.88/2.85 % (1519741)Termination reason: Refutation not found, incomplete strategy
% 12.88/2.85 % (1519741)Time elapsed: 1.064 s
% 12.88/2.85 % (1519741)Peak memory usage: 139 MB
% 12.88/2.85 % (1519741)Instructions burned: 1931 (million)
% 12.88/2.85 % (1519793)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2798543151:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2988 on theBenchmark for (2988ds/2836Mi)
% 12.88/2.85 % (1519741)------------------------------
% 12.88/2.85 % (1519741)------------------------------
% 12.88/2.85 % (1519793)First to succeed.
% 12.88/2.85 % (1519793)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1519723"
% 12.88/2.85 % (1519799)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2063574048:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2985 on theBenchmark for (2985ds/14534Mi)
% 12.88/2.85 % (1519742)Also succeeded, but the first one will report.
% 12.88/2.85 % (1519743)Also succeeded, but the first one will report.
% 12.88/2.85 % SZS status Satisfiable for theBenchmark
% 12.88/2.85 % SZS output start Saturation.
% See solution above
% 14.36/3.03 % SZS output start Definitions and Model Updates.
% 14.36/3.03 % SZS output end Definitions and Model Updates.
% 14.36/3.03 % (1519793)------------------------------
% 14.36/3.03 % (1519793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.36/3.03 % (1519793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.36/3.03 % (1519793)CaDiCaL version: 2.1.3
% 14.36/3.03 % (1519793)Termination reason: Satisfiable
% 14.36/3.03 % (1519793)Time elapsed: 0.322 s
% 14.36/3.03 % (1519793)Peak memory usage: 92 MB
% 14.36/3.03 % (1519793)Instructions burned: 287 (million)
% 14.36/3.03 % (1519793)------------------------------
% 14.36/3.03 % (1519793)------------------------------
% 14.36/3.03 % (1519723)Success in time 1.992 s
% 14.36/3.03 % Vampire exiting
%------------------------------------------------------------------------------