%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP220-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:09:29 PM UTC 2026
% Result : Satisfiable 0.15s 0.56s
% Output : Saturation 0.95s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2641,negated_conjecture,
true = existent(skc5,skc9) ).
cnf(u3815,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonexistent(X0,skf1(X1)),true) ).
cnf(u263,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(human_person(X0,skc9),true,true,true),true) ).
cnf(u321,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,human(X0,skc9),true) ).
cnf(u2808,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc6),true),tuple(true,true),a,b) ).
cnf(u255,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(nonexistent(X0,skc7),true,true,true),true) ).
cnf(u1181,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc7),true) ).
cnf(u702,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u377,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,X2),true,ifeq3(agent(skc5,skc7,X3),true,ifeq3(agent(skc5,X1,X3),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u3570,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc6),true) ).
cnf(u1768,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,animate(X0,skc9),true) ).
cnf(u3779,negated_conjecture,
true = ifeq2(true,true,singleton(skc6,skf1(X0)),true) ).
cnf(u1916,negated_conjecture,
true = ifeq2(man(skc6,X0),true,true,true) ).
cnf(u1747,negated_conjecture,
true = animate(skc6,skc9) ).
cnf(u63,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).
cnf(u529,negated_conjecture,
true = think_believe_consider(skc6,skc7) ).
cnf(u1211,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(living(X0,skc9),true,true,true),true) ).
cnf(u3680,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc8),true) ).
cnf(u3195,negated_conjecture,
true = unisex(skc5,skc8) ).
cnf(u1338,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6) ).
cnf(u1009,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,human_person(X0,skc9),true) ).
cnf(u2990,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1368,negated_conjecture,
true = ifeq2(true,true,thing(skc6,skc6),true) ).
cnf(u2785,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,X1),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u3126,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(nonhuman(X0,skc8),true,true,true),true) ).
cnf(u526,negated_conjecture,
true = ifeq2(human(skc5,X0),true,human(skc6,X0),true) ).
cnf(u2493,negated_conjecture,
true = ifeq2(true,true,thing(skc6,skc9),true) ).
cnf(u695,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(agent(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X0),true,skc6,skc6),skc6),skc6) ).
cnf(u2589,negated_conjecture,
true = ifeq2(eventuality(skc5,skc9),true,true,true) ).
cnf(u948,negated_conjecture,
ifeq3(true,true,ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,ifeq3(entity(skc6,skc9),true,skc8,X0),X0),X0),X0) = X0 ).
cnf(u310,negated_conjecture,
true = ifeq2(true,true,ifeq2(general(skc5,X0),true,general(skc6,X0),true),true) ).
cnf(u1435,negated_conjecture,
true = general(skc5,skc6) ).
cnf(u3778,negated_conjecture,
true = ifeq2(entity(skc6,skf1(X0)),true,true,true) ).
cnf(u805,negated_conjecture,
ifeq3(of(skc6,skc8,X0),true,ifeq3(of(skc6,X1,X0),true,ifeq3(forename(skc6,X1),true,ifeq3(entity(skc6,X0),true,skc8,X1),X1),X1),X1) = X1 ).
cnf(u234,negated_conjecture,
true = ifeq2(true,true,ifeq2(nonexistent(skc5,X0),true,nonexistent(skc6,X0),true),true) ).
cnf(u588,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(proposition(X0,skc6),true,true,true),true) ).
cnf(u1370,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc6),true,true,true),true) ).
cnf(u972,negated_conjecture,
true = ifeq2(true,true,relation(skc6,skc8),true) ).
cnf(u2140,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6),skc6) ).
cnf(u2768,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonhuman(X0,skc6),true,true,true),true) ).
cnf(u903,negated_conjecture,
true = ifeq2(agent(X0,skc7,skc9),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u1839,negated_conjecture,
true = relation(skc6,skc8) ).
cnf(u3825,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skf1(X1)),true) ).
cnf(u1314,negated_conjecture,
true = ifeq2(true,true,existent(skc5,skc9),true) ).
cnf(u1447,negated_conjecture,
true = unisex(skc5,skc6) ).
cnf(u3898,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc8),true) ).
cnf(u2499,negated_conjecture,
ifeq3(of(skc6,X0,skc9),true,ifeq3(of(skc6,X1,skc9),true,ifeq3(forename(skc6,X0),true,ifeq3(forename(skc6,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u2718,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc6),true,true,true),true) ).
cnf(u3113,negated_conjecture,
true = ifeq2(eventuality(skc5,skc8),true,true,true) ).
cnf(u3775,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skf1(X1)),true,true,true),true) ).
cnf(u879,negated_conjecture,
true = vincent_forename(skc6,skc8) ).
cnf(u336,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc5,X0),true,theme(X0,skc7,skc6),true),true) ).
cnf(u2988,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,skc6,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1542,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc7),true) ).
cnf(u139,negated_conjecture,
true = proposition(skc5,skc6) ).
cnf(u271,negated_conjecture,
true = ifeq2(true,true,ifeq2(living(skc5,X0),true,living(skc6,X0),true),true) ).
cnf(u330,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc5,X0),true,agent(X0,skc7,skc9),true),true) ).
cnf(u2725,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc6),true) ).
cnf(u1062,negated_conjecture,
true = relation(skc6,skc6) ).
cnf(u488,negated_conjecture,
true = man(skc6,skc9) ).
cnf(u3076,negated_conjecture,
true = ifeq2(true,true,general(skc6,skc8),true) ).
cnf(u141,negated_conjecture,
true = of(skc5,skc8,skc9) ).
cnf(u43,axiom,
true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u904,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X0),true,agent(X0,skc7,skc9),true),true) ).
cnf(u449,negated_conjecture,
true = ifeq2(singleton(skc5,X0),true,singleton(skc6,X0),true) ).
cnf(u2591,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc9),true) ).
cnf(u288,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc5,X0),true,think_believe_consider(X0,skc7),true),true) ).
cnf(u707,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u2078,negated_conjecture,
skc8 = ifeq3(true,true,ifeq3(entity(skc6,skc9),true,skc8,skc8),skc8) ).
cnf(u326,negated_conjecture,
true = ifeq2(true,true,ifeq2(vincent_forename(skc5,X0),true,vincent_forename(skc6,X0),true),true) ).
cnf(u3678,negated_conjecture,
true = ifeq2(eventuality(skc6,skc8),true,true,true) ).
cnf(u1537,negated_conjecture,
true = ifeq2(abstraction(skc6,skc7),true,true,true) ).
cnf(u250,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(man(X0,skc9),true,true,true),true) ).
cnf(u216,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(eventuality(X0,skc7),true,true,true),true) ).
cnf(u91,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human(X0,X2),true,human(X1,X2),true),true) ).
cnf(u516,negated_conjecture,
true = ifeq2(true,true,organism(skc6,skc9),true) ).
cnf(u415,negated_conjecture,
true = ifeq2(true,true,agent(skc6,skc7,skc9),true) ).
cnf(u1365,negated_conjecture,
true = thing(skc5,skc6) ).
cnf(u2679,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(existent(X0,skc9),true,true,true),true) ).
cnf(u252,negated_conjecture,
true = nonexistent(skc5,skc7) ).
cnf(u93,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(animate(X0,X2),true,animate(X1,X2),true),true) ).
cnf(u1997,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,think_believe_consider(X0,skc7),true) ).
cnf(u284,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(male(X0,skc9),true,true,true),true) ).
cnf(u401,negated_conjecture,
true = ifeq2(true,true,nonhuman(skc5,skc6),true) ).
cnf(u2757,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc6),true,true,true),true) ).
cnf(u2819,negated_conjecture,
skc6 = ifeq3(theme(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6) ).
cnf(u49,axiom,
true = ifeq2(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u464,negated_conjecture,
true = ifeq2(true,true,unisex(skc6,skc7),true) ).
cnf(u2628,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,specific(X0,skc9),true) ).
cnf(u87,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(impartial(X0,X2),true,impartial(X1,X2),true),true) ).
cnf(u3015,negated_conjecture,
true = ifeq2(true,true,specific(skc6,skf1(X0)),true) ).
cnf(u1833,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(abstraction(X0,skc8),true,true,true),true) ).
cnf(u395,negated_conjecture,
true = ifeq2(true,true,present(skc6,skc7),true) ).
cnf(u436,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(event(X0,skc7),true,true,true),true) ).
cnf(u2377,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc7),true,true,true),true) ).
cnf(u1912,negated_conjecture,
true = ifeq2(accessible_world(skc6,skc6),true,true,true) ).
cnf(u232,negated_conjecture,
true = specific(skc5,skc7) ).
cnf(u3894,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc8),true,true,true),true) ).
cnf(u73,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(unisex(X0,X2),true,unisex(X1,X2),true),true) ).
cnf(u264,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,human_person(X0,skc9),true) ).
cnf(u239,negated_conjecture,
b = ifeq(tuple(true,general(skc5,skc7)),tuple(true,true),a,b) ).
cnf(u2241,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u3673,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc8),true,true,true),true) ).
cnf(u705,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,X0,skc6),skc6),skc6),skc6),skc6) ).
cnf(u45,axiom,
true = ifeq2(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u226,negated_conjecture,
true = ifeq2(entity(skc5,skc7),true,true,true) ).
cnf(u67,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(singleton(X0,X2),true,singleton(X1,X2),true),true) ).
cnf(u3287,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc9),true) ).
cnf(u391,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u2096,negated_conjecture,
skc8 = ifeq3(of(skc6,skc8,X0),true,ifeq3(of(skc6,skc8,X0),true,ifeq3(entity(skc6,X0),true,skc8,skc8),skc8),skc8) ).
cnf(u416,negated_conjecture,
true = ifeq2(true,true,theme(skc6,skc7,skc6),true) ).
cnf(u39,axiom,
true = ifeq2(man(X0,X1),true,male(X0,X1),true) ).
cnf(u400,negated_conjecture,
true = ifeq2(true,true,thing(skc5,skc6),true) ).
cnf(u69,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(specific(X0,X2),true,specific(X1,X2),true),true) ).
cnf(u3740,negated_conjecture,
true = unisex(skc6,skc8) ).
cnf(u260,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,nonexistent(X0,skc7),true) ).
cnf(u219,negated_conjecture,
true = thing(skc5,skc7) ).
cnf(u3221,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(unisex(X0,skc8),true,true,true),true) ).
cnf(u25,axiom,
true = ifeq2(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u349,negated_conjecture,
true = abstraction(skc5,skc6) ).
cnf(u1494,negated_conjecture,
true = thing(skc6,skc7) ).
cnf(u185,negated_conjecture,
true = male(skc5,skc9) ).
cnf(u153,negated_conjecture,
true = ifeq2(man(skc6,X0),true,agent(skc6,skf1(X0),X0),true) ).
cnf(u2752,negated_conjecture,
true = singleton(skc5,skc6) ).
cnf(u19,axiom,
true = ifeq2(man(X0,X1),true,human_person(X0,X1),true) ).
cnf(u2584,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u177,negated_conjecture,
true = human_person(skc5,skc9) ).
cnf(u3389,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0) = X0 ).
cnf(u501,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,man(X0,skc9),true) ).
cnf(u180,negated_conjecture,
true = ifeq2(true,true,animate(skc5,skc9),true) ).
cnf(u3079,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(abstraction(X0,skc8),true,true,true),true) ).
cnf(u21,axiom,
true = ifeq2(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u1452,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(unisex(X0,skc6),true,true,true),true) ).
cnf(u329,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,vincent_forename(X0,skc8),true) ).
cnf(u3810,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonexistent(X0,skf1(X1)),true,true,true),true) ).
cnf(u351,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc5,X0),true,of(X0,skc8,skc9),true),true) ).
cnf(u495,negated_conjecture,
true = ifeq2(true,true,smoke(skc6,skf1(X0)),true) ).
cnf(u15,axiom,
true = ifeq2(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u1271,negated_conjecture,
true = entity(skc5,skc9) ).
cnf(u3759,negated_conjecture,
true = singleton(skc5,skc8) ).
cnf(u1680,negated_conjecture,
true = organism(skc6,skc9) ).
cnf(u1325,negated_conjecture,
ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,skc8,X0),X0) = X0 ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u933,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u3322,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skc9),true) ).
cnf(u3745,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc8),true,true,true),true) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u1438,negated_conjecture,
true = ifeq2(true,true,general(skc6,skc6),true) ).
cnf(u325,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,relname(X0,skc8),true) ).
cnf(u143,negated_conjecture,
true = agent(skc5,skc7,skc9) ).
cnf(u3782,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skf1(X1)),true) ).
cnf(u281,negated_conjecture,
true = ifeq2(true,true,ifeq2(animate(skc5,X0),true,animate(skc6,X0),true),true) ).
cnf(u1409,negated_conjecture,
b = ifeq(tuple(human(skc5,skc6),true),tuple(true,true),a,b) ).
cnf(u605,negated_conjecture,
true = ifeq2(relname(skc5,X0),true,relname(skc6,X0),true) ).
cnf(u913,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u914,negated_conjecture,
true = of(skc6,skc8,skc9) ).
cnf(u1950,negated_conjecture,
true = ifeq2(agent(X0,skf1(skc9),skc9),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u885,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(vincent_forename(X0,skc8),true,true,true),true) ).
cnf(u2806,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(general(X0,skc6),true,true,true),true) ).
cnf(u1209,negated_conjecture,
true = ifeq2(true,true,living(skc6,skc9),true) ).
cnf(u519,negated_conjecture,
true = ifeq2(existent(skc5,X0),true,existent(skc6,X0),true) ).
cnf(u129,negated_conjecture,
true = vincent_forename(skc5,skc8) ).
cnf(u3311,negated_conjecture,
true = specific(skc6,skc9) ).
cnf(u1919,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(event(X0,skf1(X1)),true,true,true),true) ).
cnf(u3284,negated_conjecture,
true = ifeq2(true,true,singleton(skc6,skc9),true) ).
cnf(u3855,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc9),true) ).
cnf(u2944,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skc6)),tuple(true,true),a,b) ).
cnf(u458,negated_conjecture,
true = ifeq2(nonexistent(skc5,X0),true,nonexistent(skc6,X0),true) ).
cnf(u3764,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc8),true,true,true),true) ).
cnf(u1190,negated_conjecture,
true = living(skc5,skc9) ).
cnf(u4001,negated_conjecture,
true = ifeq2(singleton(skc5,skf1(X0)),true,true,true) ).
cnf(u2116,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,X0,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u309,negated_conjecture,
true = ifeq2(true,true,ifeq2(nonhuman(skc5,X0),true,nonhuman(skc6,X0),true),true) ).
cnf(u648,negated_conjecture,
skc8 = ifeq3(true,true,ifeq3(entity(skc5,skc9),true,skc8,skc8),skc8) ).
cnf(u2410,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(living(X0,skc9),true,true,true),true) ).
cnf(u460,negated_conjecture,
true = ifeq2(true,true,nonexistent(skc6,skc7),true) ).
cnf(u2137,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u3826,negated_conjecture,
true = singleton(skc6,skc9) ).
cnf(u538,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,X3),true,ifeq3(agent(skc6,skc7,X3),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1374,negated_conjecture,
true = ifeq2(true,true,singleton(skc5,skc6),true) ).
cnf(u454,negated_conjecture,
true = ifeq2(specific(skc5,X0),true,specific(skc6,X0),true) ).
cnf(u537,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,skc7,X3),true,ifeq3(agent(skc6,X1,X3),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u935,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1),X1) = X1 ).
cnf(u3729,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(general(X0,skc8),true,true,true),true) ).
cnf(u1313,negated_conjecture,
true = ifeq2(true,true,specific(skc5,skc9),true) ).
cnf(u3333,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6),skc6) ).
cnf(u653,negated_conjecture,
ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,skc9),true,skc8,X0),X0),X0) = X0 ).
cnf(u804,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,forename(X0,skc8),true) ).
cnf(u3173,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,general(X0,skc8),true) ).
cnf(u2495,negated_conjecture,
true = ifeq2(true,true,existent(skc6,skc9),true) ).
cnf(u517,negated_conjecture,
true = ifeq2(entity(skc5,X0),true,entity(skc6,X0),true) ).
cnf(u607,negated_conjecture,
true = ifeq2(true,true,relname(skc6,skc8),true) ).
cnf(u3785,negated_conjecture,
true = nonexistent(skc6,skf1(X0)) ).
cnf(u776,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,skc6),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,X1,X2),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u2272,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u396,negated_conjecture,
true = ifeq2(true,true,man(skc6,skc9),true) ).
cnf(u563,negated_conjecture,
true = ifeq2(proposition(skc5,X0),true,proposition(skc6,X0),true) ).
cnf(u406,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,abstraction(X0,skc6),true) ).
cnf(u3170,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc8),true),tuple(true,true),a,b) ).
cnf(u171,negated_conjecture,
true = ifeq2(true,true,specific(skc5,skc7),true) ).
cnf(u431,negated_conjecture,
true = ifeq2(true,true,eventuality(skc6,skc7),true) ).
cnf(u230,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc7),true) ).
cnf(u2426,negated_conjecture,
skc8 = ifeq3(entity(skc6,skc9),true,skc8,skc8) ).
cnf(u174,negated_conjecture,
true = ifeq2(true,true,human_person(skc5,skc9),true) ).
cnf(u2481,negated_conjecture,
true = entity(skc6,skc9) ).
cnf(u3516,negated_conjecture,
true = singleton(skc5,skc9) ).
cnf(u1802,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,abstraction(X0,skc6),true) ).
cnf(u173,negated_conjecture,
true = ifeq2(true,true,unisex(skc5,skc7),true) ).
cnf(u364,negated_conjecture,
ifeq3(true,true,ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,skc9),true,skc8,X0),X0),X0),X0) = X0 ).
cnf(u3128,negated_conjecture,
b = ifeq(tuple(human(skc5,skc8),true),tuple(true,true),a,b) ).
cnf(u386,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(theme(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,ifeq3(proposition(skc5,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u81,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(organism(X0,X2),true,organism(X1,X2),true),true) ).
cnf(u285,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,male(X0,skc9),true) ).
cnf(u2622,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(specific(X0,skc9),true,true,true),true) ).
cnf(u1091,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relname(X0,skc8),true,true,true),true) ).
cnf(u3677,negated_conjecture,
true = ifeq2(true,true,singleton(skc6,skc8),true) ).
cnf(u576,negated_conjecture,
true = proposition(skc6,skc6) ).
cnf(u197,negated_conjecture,
b = ifeq(tuple(unisex(skc5,skc9),true),tuple(true,true),a,b) ).
cnf(u2422,negated_conjecture,
true = impartial(skc6,skc9) ).
cnf(u417,negated_conjecture,
true = ifeq2(true,true,of(skc6,skc8,skc9),true) ).
cnf(u123,negated_conjecture,
true = actual_world(skc5) ).
cnf(u1307,negated_conjecture,
true = ifeq2(true,true,entity(skc6,skc9),true) ).
cnf(u314,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,forename(X0,skc8),true) ).
cnf(u1019,negated_conjecture,
true = male(skc6,skc9) ).
cnf(u344,negated_conjecture,
true = ifeq2(true,true,impartial(skc5,skc9),true) ).
cnf(u3318,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skc9)),tuple(true,true),a,b) ).
cnf(u1849,negated_conjecture,
true = ifeq2(proposition(skc6,skc8),true,true,true) ).
cnf(u510,negated_conjecture,
true = ifeq2(human_person(skc5,X0),true,human_person(skc6,X0),true) ).
cnf(u125,negated_conjecture,
true = man(skc5,skc9) ).
cnf(u3794,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skf1(X0))),tuple(true,true),a,b) ).
cnf(u316,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(human(X0,skc9),true,true,true),true) ).
cnf(u147,negated_conjecture,
true = ifeq2(man(skc6,X0),true,smoke(skc6,skf1(X1)),true) ).
cnf(u1613,negated_conjecture,
b = ifeq(tuple(true,existent(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u338,negated_conjecture,
true = ifeq2(theme(X0,skc7,skc6),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u819,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u2151,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6) ).
cnf(u3692,negated_conjecture,
true = nonhuman(skc6,skc8) ).
cnf(u119,axiom,
true = ifeq2(of(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).
cnf(u592,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,X0,X3),true,ifeq3(agent(skc6,X1,X3),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,skc6),skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u528,negated_conjecture,
true = ifeq2(true,true,human(skc6,skc9),true) ).
cnf(u149,negated_conjecture,
true = ifeq2(man(skc6,X0),true,present(skc6,skf1(X1)),true) ).
cnf(u1830,negated_conjecture,
true = ifeq2(true,true,general(skc5,skc8),true) ).
cnf(u1829,negated_conjecture,
true = ifeq2(true,true,nonhuman(skc5,skc8),true) ).
cnf(u535,negated_conjecture,
true = ifeq2(think_believe_consider(X0,skc7),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u942,negated_conjecture,
true = ifeq2(of(X0,skc8,skc9),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u2770,negated_conjecture,
b = ifeq(tuple(human(skc6,skc6),true),tuple(true,true),a,b) ).
cnf(u105,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).
cnf(u429,negated_conjecture,
true = ifeq2(eventuality(skc5,X0),true,eventuality(skc6,X0),true) ).
cnf(u334,negated_conjecture,
true = organism(skc5,skc9) ).
cnf(u451,negated_conjecture,
true = present(skc6,skc7) ).
cnf(u99,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(proposition(X0,X2),true,proposition(X1,X2),true),true) ).
cnf(u2217,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u290,negated_conjecture,
true = ifeq2(think_believe_consider(X0,skc7),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u423,negated_conjecture,
true = ifeq2(event(skc5,X0),true,event(skc6,X0),true) ).
cnf(u1248,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(impartial(X0,skc9),true,true,true),true) ).
cnf(u1825,negated_conjecture,
true = ifeq2(true,true,abstraction(skc6,skc8),true) ).
cnf(u922,negated_conjecture,
true = ifeq2(theme(X0,skc7,skc6),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u3889,negated_conjecture,
true = singleton(skc6,skc8) ).
cnf(u101,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relation(X0,X2),true,relation(X1,X2),true),true) ).
cnf(u734,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u292,negated_conjecture,
true = ifeq2(true,true,ifeq2(proposition(skc5,X0),true,proposition(skc6,X0),true),true) ).
cnf(u409,negated_conjecture,
true = ifeq2(true,true,proposition(skc6,skc6),true) ).
cnf(u2722,negated_conjecture,
true = ifeq2(true,true,singleton(skc6,skc6),true) ).
cnf(u57,axiom,
true = ifeq2(vincent_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u2700,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,skc6,skc6),skc6) ).
cnf(u1706,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(organism(X0,skc9),true,true,true),true) ).
cnf(u95,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(male(X0,X2),true,male(X1,X2),true),true) ).
cnf(u2435,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,impartial(X0,skc9),true) ).
cnf(u286,negated_conjecture,
true = animate(skc5,skc9) ).
cnf(u403,negated_conjecture,
true = ifeq2(true,true,unisex(skc5,skc6),true) ).
cnf(u2596,negated_conjecture,
skc6 = ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6) ).
cnf(u1316,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(entity(X0,skc9),true,true,true),true) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u3227,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,unisex(X0,skc8),true) ).
cnf(u375,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,X1,X2),true,ifeq3(agent(skc5,X0,X3),true,ifeq3(agent(skc5,X1,X3),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X2),true,X2,skc6),skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u3751,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc8),true) ).
cnf(u175,negated_conjecture,
true = ifeq2(true,true,male(skc5,skc9),true) ).
cnf(u1442,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc6),true),tuple(true,true),a,b) ).
cnf(u713,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc5,skc7,X0),true,ifeq3(proposition(skc5,X0),true,X0,skc6),skc6),skc6) ).
cnf(u53,axiom,
true = ifeq2(forename(X0,X1),true,relname(X0,X1),true) ).
cnf(u686,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0),X0),X0) = X0 ).
cnf(u685,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,X0,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u1713,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,organism(X0,skc9),true) ).
cnf(u514,negated_conjecture,
true = ifeq2(organism(skc5,X0),true,organism(skc6,X0),true) ).
cnf(u47,axiom,
true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u1175,negated_conjecture,
true = ifeq2(true,true,singleton(skc6,skc7),true) ).
cnf(u2215,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,X1,X2),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u3531,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u3111,negated_conjecture,
true = ifeq2(entity(skc5,skc8),true,true,true) ).
cnf(u2139,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,X1),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6),skc6) ).
cnf(u151,negated_conjecture,
true = ifeq2(man(skc6,X0),true,event(skc6,skf1(X1)),true) ).
cnf(u3697,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonhuman(X0,skc8),true,true,true),true) ).
cnf(u3016,negated_conjecture,
true = ifeq2(true,true,nonexistent(skc6,skf1(X0)),true) ).
cnf(u666,negated_conjecture,
skc8 = ifeq3(of(skc5,skc8,X0),true,ifeq3(of(skc5,skc8,X0),true,ifeq3(entity(skc5,X0),true,skc8,skc8),skc8),skc8) ).
cnf(u3316,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skc9),true,true,true),true) ).
cnf(u2884,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,skc7,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6) ).
cnf(u3017,negated_conjecture,
true = ifeq2(true,true,unisex(skc6,skf1(X0)),true) ).
cnf(u989,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,eventuality(X0,skc7),true) ).
cnf(u313,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(forename(X0,skc8),true,true,true),true) ).
cnf(u3115,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc8),true) ).
cnf(u3817,negated_conjecture,
true = ifeq2(unisex(skc5,skf1(X0)),true,true,true) ).
cnf(u3108,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc8),true,true,true),true) ).
cnf(u359,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,X1),true,ifeq3(of(skc5,skc8,X1),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,X1),true,X0,skc8),skc8),skc8),skc8) ).
cnf(u1419,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6) ).
cnf(u307,negated_conjecture,
true = human(skc5,skc9) ).
cnf(u2128,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0) = X0 ).
cnf(u888,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,vincent_forename(X0,skc8),true) ).
cnf(u1934,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X1),true,present(X1,skf1(X0)),true),true) ).
cnf(u3131,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,nonhuman(X0,skc8),true) ).
cnf(u3553,negated_conjecture,
true = singleton(skc6,skc6) ).
cnf(u1407,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(nonhuman(X0,skc6),true,true,true),true) ).
cnf(u2267,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(agent(skc6,X1,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,X1),true,skc6,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u1454,negated_conjecture,
b = ifeq(tuple(true,male(skc5,skc6)),tuple(true,true),a,b) ).
cnf(u3787,negated_conjecture,
true = unisex(skc6,skf1(X0)) ).
cnf(u294,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(proposition(X0,skc6),true,true,true),true) ).
cnf(u912,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1616,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonexistent(X0,skc7),true) ).
cnf(u1072,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relation(X0,skc6),true,true,true),true) ).
cnf(u1318,negated_conjecture,
ifeq3(of(skc5,X0,skc9),true,ifeq3(of(skc5,X1,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(forename(skc5,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u3077,negated_conjecture,
true = ifeq2(true,true,unisex(skc6,skc8),true) ).
cnf(u1252,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,impartial(X0,skc9),true) ).
cnf(u1952,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u2872,negated_conjecture,
true = unisex(skc6,skc6) ).
cnf(u1243,negated_conjecture,
true = impartial(skc5,skc9) ).
cnf(u687,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,skc6,X1),X1),X1),X1) = X1 ).
cnf(u1096,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relname(X0,skc8),true) ).
cnf(u2735,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6) ).
cnf(u2588,negated_conjecture,
true = ifeq2(true,true,singleton(skc5,skc9),true) ).
cnf(u1373,negated_conjecture,
true = ifeq2(entity(skc5,skc6),true,true,true) ).
cnf(u339,negated_conjecture,
true = ifeq2(theme(skc5,X0,X1),true,theme(skc6,X0,X1),true) ).
cnf(u1052,negated_conjecture,
b = ifeq(tuple(unisex(skc6,skc9),true),tuple(true,true),a,b) ).
cnf(u704,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,X1),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6),skc6),skc6) ).
cnf(u2431,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(impartial(X0,skc9),true,true,true),true) ).
cnf(u3075,negated_conjecture,
true = ifeq2(true,true,nonhuman(skc6,skc8),true) ).
cnf(u2118,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1) = X1 ).
cnf(u893,negated_conjecture,
true = agent(skc6,skc7,skc9) ).
cnf(u251,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,man(X0,skc9),true) ).
cnf(u442,negated_conjecture,
true = ifeq2(accessible_world(skc6,skc5),true,true,true) ).
cnf(u1907,negated_conjecture,
true = present(skc6,skf1(X0)) ).
cnf(u29,axiom,
true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u1977,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,present(X0,skc7),true) ).
cnf(u3020,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,eventuality(X0,skf1(X1)),true) ).
cnf(u3080,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,abstraction(X0,skc8),true) ).
cnf(u2497,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(entity(X0,skc9),true,true,true),true) ).
cnf(u272,negated_conjecture,
true = ifeq2(true,true,ifeq2(human(skc5,X0),true,human(skc6,X0),true),true) ).
cnf(u247,negated_conjecture,
true = ifeq2(present(skc5,X0),true,present(skc6,X0),true) ).
cnf(u1055,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,male(X0,skc9),true) ).
cnf(u2500,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,entity(X0,skc9),true) ).
cnf(u3074,negated_conjecture,
true = ifeq2(true,true,thing(skc6,skc8),true) ).
cnf(u468,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X0),true,present(X0,skc7),true),true) ).
cnf(u75,axiom,
true = ifeq2(present(X0,X1),true,ifeq2(accessible_world(X0,X2),true,present(X2,X1),true),true) ).
cnf(u311,negated_conjecture,
true = ifeq2(true,true,ifeq2(forename(skc5,X0),true,forename(skc6,X0),true),true) ).
cnf(u266,negated_conjecture,
true = unisex(skc5,skc7) ).
cnf(u971,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,relation(X0,skc8),true) ).
cnf(u2721,negated_conjecture,
true = ifeq2(entity(skc6,skc6),true,true,true) ).
cnf(u1801,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(abstraction(X0,skc6),true,true,true),true) ).
cnf(u462,negated_conjecture,
true = ifeq2(unisex(skc5,X0),true,unisex(skc6,X0),true) ).
cnf(u1834,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,abstraction(X0,skc8),true) ).
cnf(u77,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(man(X0,X2),true,man(X1,X2),true),true) ).
cnf(u1312,negated_conjecture,
true = ifeq2(true,true,thing(skc5,skc9),true) ).
cnf(u268,negated_conjecture,
true = ifeq2(true,true,ifeq2(entity(skc5,X0),true,entity(skc6,X0),true),true) ).
cnf(u227,negated_conjecture,
true = ifeq2(true,true,singleton(skc5,skc7),true) ).
cnf(u418,negated_conjecture,
true = event(skc6,skc7) ).
cnf(u402,negated_conjecture,
true = ifeq2(true,true,general(skc5,skc6),true) ).
cnf(u33,axiom,
true = ifeq2(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u448,negated_conjecture,
true = ifeq2(true,true,thing(skc6,skc7),true) ).
cnf(u71,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).
cnf(u3699,negated_conjecture,
b = ifeq(tuple(human(skc6,skc8),true),tuple(true,true),a,b) ).
cnf(u1736,negated_conjecture,
b = ifeq(tuple(true,nonhuman(skc6,skc9)),tuple(true,true),a,b) ).
cnf(u1909,negated_conjecture,
true = smoke(skc6,skf1(X0)) ).
cnf(u3275,negated_conjecture,
true = thing(skc6,skc9) ).
cnf(u27,axiom,
true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u190,negated_conjecture,
true = ifeq2(true,true,relname(skc5,skc8),true) ).
cnf(u923,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X0),true,theme(X0,skc7,skc6),true),true) ).
cnf(u376,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(theme(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,X3),true,ifeq3(agent(skc5,skc7,X3),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,ifeq3(proposition(skc5,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u223,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc7),true,true,true),true) ).
cnf(u571,negated_conjecture,
true = ifeq2(true,true,relation(skc6,skc6),true) ).
cnf(u895,negated_conjecture,
true = theme(skc6,skc7,skc6) ).
cnf(u210,negated_conjecture,
true = ifeq2(true,true,ifeq2(event(skc5,X0),true,event(skc6,X0),true),true) ).
cnf(u209,negated_conjecture,
true = ifeq2(true,true,ifeq2(smoke(skc5,X0),true,smoke(skc6,X0),true),true) ).
cnf(u1440,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(general(X0,skc6),true,true,true),true) ).
cnf(u182,negated_conjecture,
true = ifeq2(true,true,organism(skc5,skc9),true) ).
cnf(u969,negated_conjecture,
true = ifeq2(proposition(skc5,skc8),true,true,true) ).
cnf(u23,axiom,
true = ifeq2(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u212,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(event(X0,skc7),true,true,true),true) ).
cnf(u181,negated_conjecture,
true = ifeq2(true,true,human(skc5,skc9),true) ).
cnf(u1484,negated_conjecture,
skc6 = ifeq3(theme(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,X0,skc6),skc6),skc6),skc6) ).
cnf(u203,negated_conjecture,
true = relname(skc5,skc8) ).
cnf(u168,negated_conjecture,
true = ifeq2(true,true,thing(skc5,skc7),true) ).
cnf(u9,axiom,
true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u333,negated_conjecture,
true = ifeq2(agent(skc5,X0,X1),true,agent(skc6,X0,X1),true) ).
cnf(u4007,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skf1(X1)),true) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u965,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(relation(X0,skc8),true,true,true),true) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u998,negated_conjecture,
true = human_person(skc6,skc9) ).
cnf(u2353,negated_conjecture,
true = singleton(skc6,skc7) ).
cnf(u161,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u1246,negated_conjecture,
true = ifeq2(true,true,impartial(skc6,skc9),true) ).
cnf(u5,axiom,
true = ifeq2(smoke(X0,X1),true,event(X0,X1),true) ).
cnf(u485,negated_conjecture,
true = ifeq2(man(skc5,X0),true,man(skc6,X0),true) ).
cnf(u2070,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,of(X0,skc8,skc9),true) ).
cnf(u164,negated_conjecture,
true = ifeq2(true,true,eventuality(skc5,skc7),true) ).
cnf(u3062,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,agent(X0,skf1(skc9),skc9),true) ).
cnf(u569,negated_conjecture,
true = ifeq2(relation(skc5,X0),true,relation(skc6,X0),true) ).
cnf(u2494,negated_conjecture,
true = ifeq2(true,true,specific(skc6,skc9),true) ).
cnf(u3734,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,general(X0,skc8),true) ).
cnf(clause63,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(u765,negated_conjecture,
true = forename(skc6,skc8) ).
cnf(u3974,negated_conjecture,
true = singleton(skc6,skf1(X0)) ).
cnf(u1002,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(human_person(X0,skc9),true,true,true),true) ).
cnf(u127,negated_conjecture,
true = forename(skc5,skc8) ).
cnf(u943,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X0),true,of(X0,skc8,skc9),true),true) ).
cnf(u318,negated_conjecture,
b = ifeq(tuple(true,nonhuman(skc5,skc9)),tuple(true,true),a,b) ).
cnf(u593,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,X2,skc6),true,ifeq3(agent(skc6,X0,X3),true,ifeq3(agent(skc6,X2,X3),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,X2),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1538,negated_conjecture,
true = ifeq2(entity(skc6,skc7),true,true,true) ).
cnf(u1620,negated_conjecture,
true = unisex(skc6,skc7) ).
cnf(u405,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(abstraction(X0,skc6),true,true,true),true) ).
cnf(u113,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(vincent_forename(X0,X2),true,vincent_forename(X1,X2),true),true) ).
cnf(u1535,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc7),true,true,true),true) ).
cnf(u609,negated_conjecture,
true = ifeq2(vincent_forename(skc5,X0),true,vincent_forename(skc6,X0),true) ).
cnf(u1611,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonexistent(X0,skc7),true,true,true),true) ).
cnf(u2777,negated_conjecture,
true = general(skc6,skc6) ).
cnf(u3768,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc8),true) ).
cnf(u3112,negated_conjecture,
true = ifeq2(true,true,singleton(skc5,skc8),true) ).
cnf(u133,negated_conjecture,
true = present(skc5,skc7) ).
cnf(u3668,negated_conjecture,
true = thing(skc6,skc8) ).
cnf(u265,negated_conjecture,
true = ifeq2(true,true,ifeq2(organism(skc5,X0),true,organism(skc6,X0),true),true) ).
cnf(u2164,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skf1(skc9),X1),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(u547,negated_conjecture,
true = ifeq2(true,true,male(skc6,skc9),true) ).
cnf(u1627,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u2117,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0) = X0 ).
cnf(u2845,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6) ).
cnf(u545,negated_conjecture,
true = ifeq2(male(skc5,X0),true,male(skc6,X0),true) ).
cnf(u1412,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,nonhuman(X0,skc6),true) ).
cnf(u2609,negated_conjecture,
true = specific(skc5,skc9) ).
cnf(u2299,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u774,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,X1,skc6),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(agent(skc5,X1,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(think_believe_consider(skc5,X1),true,skc6,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u3007,negated_conjecture,
true = eventuality(skc6,skf1(X0)) ).
cnf(u3819,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skf1(X1)),true,true,true),true) ).
cnf(u2381,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc7),true) ).
cnf(u261,negated_conjecture,
true = ifeq2(true,true,ifeq2(human_person(skc5,X0),true,human_person(skc6,X0),true),true) ).
cnf(u2684,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,existent(X0,skc9),true) ).
cnf(u2301,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1764,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(animate(X0,skc9),true,true,true),true) ).
cnf(u541,negated_conjecture,
true = ifeq2(animate(skc5,X0),true,animate(skc6,X0),true) ).
cnf(u2506,negated_conjecture,
skc8 = ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,X0,skc8),skc8) ).
cnf(u2605,negated_conjecture,
skc6 = ifeq3(agent(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X0),true,skc6,skc6),skc6) ).
cnf(u3566,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc6),true,true,true),true) ).
cnf(u3770,negated_conjecture,
true = thing(skc6,skf1(X0)) ).
cnf(u246,negated_conjecture,
true = ifeq2(present(X0,skc7),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u1933,negated_conjecture,
true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u3378,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,existent(X0,skc9),true) ).
cnf(u2270,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skf1(skc9),X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u3368,negated_conjecture,
true = existent(skc6,skc9) ).
cnf(u988,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(eventuality(X0,skc7),true,true,true),true) ).
cnf(u2586,negated_conjecture,
true = ifeq2(abstraction(skc5,skc9),true,true,true) ).
cnf(u2681,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc9),true),tuple(true,true),a,b) ).
cnf(u89,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(living(X0,X2),true,living(X1,X2),true),true) ).
cnf(u521,negated_conjecture,
true = ifeq2(impartial(skc5,X0),true,impartial(skc6,X0),true) ).
cnf(u1606,negated_conjecture,
true = nonexistent(skc6,skc7) ).
cnf(u845,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u394,negated_conjecture,
true = ifeq2(accessible_world(skc5,skc5),true,true,true) ).
cnf(u2405,negated_conjecture,
true = living(skc6,skc9) ).
cnf(u206,negated_conjecture,
true = ifeq2(true,true,relation(skc5,skc8),true) ).
cnf(u747,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,skc6),true,ifeq3(agent(skc5,X1,skc9),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0),X0),X0),X0) = X0 ).
cnf(u3790,negated_conjecture,
true = ifeq2(specific(skc5,skf1(X0)),true,true,true) ).
cnf(u2811,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,general(X0,skc6),true) ).
cnf(u1577,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skc7),true) ).
cnf(u968,negated_conjecture,
true = ifeq2(true,true,abstraction(skc5,skc8),true) ).
cnf(u591,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,proposition(X0,skc6),true) ).
cnf(u2143,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u439,negated_conjecture,
true = ifeq2(smoke(skc6,skc7),true,true,true) ).
cnf(u3821,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skf1(X0))),tuple(true,true),a,b) ).
cnf(u1405,negated_conjecture,
true = ifeq2(true,true,nonhuman(skc6,skc6),true) ).
cnf(u199,negated_conjecture,
true = ifeq2(relname(skc5,skc6),true,true,true) ).
cnf(u1084,negated_conjecture,
true = relname(skc6,skc8) ).
cnf(u440,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,event(X0,skc7),true) ).
cnf(u1905,negated_conjecture,
true = event(skc6,skf1(X0)) ).
cnf(u1939,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(smoke(X0,skf1(X1)),true,true,true),true) ).
cnf(u155,axiom,
b = ifeq(tuple(unisex(X0,X1),male(X0,X1)),tuple(true,true),a,b) ).
cnf(u580,negated_conjecture,
true = ifeq2(general(skc5,X0),true,general(skc6,X0),true) ).
cnf(u2190,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(u1078,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relation(X0,skc6),true) ).
cnf(u79,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human_person(X0,X2),true,human_person(X1,X2),true),true) ).
cnf(u536,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X0),true,think_believe_consider(X0,skc7),true),true) ).
cnf(u157,axiom,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).
cnf(u348,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,organism(X0,skc9),true) ).
cnf(u543,negated_conjecture,
true = ifeq2(true,true,animate(skc6,skc9),true) ).
cnf(u3773,negated_conjecture,
true = ifeq2(thing(skc5,skf1(X0)),true,true,true) ).
cnf(u420,negated_conjecture,
true = ifeq2(smoke(skc5,X0),true,smoke(skc6,X0),true) ).
cnf(u304,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(relation(X0,skc6),true,true,true),true) ).
cnf(u723,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1379,negated_conjecture,
true = nonhuman(skc5,skc6) ).
cnf(u2624,negated_conjecture,
b = ifeq(tuple(true,general(skc5,skc9)),tuple(true,true),a,b) ).
cnf(u1074,negated_conjecture,
true = ifeq2(relname(skc6,skc6),true,true,true) ).
cnf(u107,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(general(X0,X2),true,general(X1,X2),true),true) ).
cnf(u2033,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,agent(X0,skc7,skc9),true) ).
cnf(u137,negated_conjecture,
true = accessible_world(skc5,skc6) ).
cnf(u3535,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc9),true) ).
cnf(u328,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(vincent_forename(X0,skc8),true,true,true),true) ).
cnf(u523,negated_conjecture,
true = ifeq2(living(skc5,X0),true,living(skc6,X0),true) ).
cnf(u494,negated_conjecture,
true = ifeq2(true,true,present(skc6,skf1(X0)),true) ).
cnf(u109,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(forename(X0,X2),true,forename(X1,X2),true),true) ).
cnf(u3731,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc8),true),tuple(true,true),a,b) ).
cnf(u2173,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u131,negated_conjecture,
true = event(skc5,skc7) ).
cnf(u2773,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonhuman(X0,skc6),true) ).
cnf(u322,negated_conjecture,
true = ifeq2(true,true,ifeq2(relname(skc5,X0),true,relname(skc6,X0),true),true) ).
cnf(u1450,negated_conjecture,
true = ifeq2(true,true,unisex(skc6,skc6),true) ).
cnf(u103,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).
cnf(u3747,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skc8)),tuple(true,true),a,b) ).
cnf(u512,negated_conjecture,
true = ifeq2(true,true,human_person(skc6,skc9),true) ).
cnf(u411,negated_conjecture,
true = ifeq2(true,true,forename(skc6,skc8),true) ).
cnf(u3375,negated_conjecture,
b = ifeq(tuple(nonexistent(skc6,skc9),true),tuple(true,true),a,b) ).
cnf(u324,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(relname(X0,skc8),true,true,true),true) ).
cnf(u59,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(smoke(X0,X2),true,smoke(X1,X2),true),true) ).
cnf(u248,negated_conjecture,
true = ifeq2(true,true,ifeq2(man(skc5,X0),true,man(skc6,X0),true),true) ).
cnf(u955,negated_conjecture,
true = relation(skc5,skc8) ).
cnf(u3792,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skf1(X1)),true,true,true),true) ).
cnf(u280,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,unisex(X0,skc7),true) ).
cnf(u413,negated_conjecture,
true = ifeq2(true,true,vincent_forename(skc6,skc8),true) ).
cnf(u446,negated_conjecture,
true = ifeq2(thing(skc5,X0),true,thing(skc6,X0),true) ).
cnf(u61,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(event(X0,X2),true,event(X1,X2),true),true) ).
cnf(u694,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0) = X0 ).
cnf(u83,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(entity(X0,X2),true,entity(X1,X2),true),true) ).
cnf(u1573,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u274,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(unisex(X0,skc7),true,true,true),true) ).
cnf(u3014,negated_conjecture,
true = ifeq2(true,true,thing(skc6,skf1(X0)),true) ).
cnf(u1739,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,human(X0,skc9),true) ).
cnf(u55,axiom,
true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u244,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc5,X0),true,present(X0,skc7),true),true) ).
cnf(u392,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,skc6,X1),X1),X1),X1),X1) = X1 ).
cnf(u85,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(existent(X0,X2),true,existent(X1,X2),true),true) ).
cnf(u276,negated_conjecture,
b = ifeq(tuple(true,male(skc5,skc7)),tuple(true,true),a,b) ).
cnf(u393,negated_conjecture,
true = ifeq2(true,true,event(skc6,skc7),true) ).
cnf(u332,negated_conjecture,
true = ifeq2(agent(X0,skc7,skc9),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u41,axiom,
true = ifeq2(proposition(X0,X1),true,relation(X0,X1),true) ).
cnf(u1932,negated_conjecture,
true = ifeq2(present(skc5,skf1(X0)),true,true,true) ).
cnf(u2761,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc6),true) ).
cnf(u365,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,skc9),true,X0,skc8),skc8),skc8) ).
cnf(u2723,negated_conjecture,
true = ifeq2(eventuality(skc6,skc6),true,true,true) ).
cnf(u270,negated_conjecture,
true = ifeq2(true,true,ifeq2(impartial(skc5,X0),true,impartial(skc6,X0),true),true) ).
cnf(u387,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,X2),true,ifeq3(agent(skc5,X1,skc9),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1917,negated_conjecture,
true = ifeq2(event(skc5,skf1(X0)),true,true,true) ).
cnf(u3783,negated_conjecture,
true = specific(skc6,skf1(X0)) ).
cnf(u35,axiom,
true = ifeq2(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u65,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(thing(X0,X2),true,thing(X1,X2),true),true) ).
cnf(u1828,negated_conjecture,
true = ifeq2(true,true,thing(skc5,skc8),true) ).
cnf(u2129,negated_conjecture,
skc6 = ifeq3(true,true,ifeq3(agent(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X0),true,skc6,skc6),skc6),skc6) ).
cnf(u1942,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,smoke(X0,skf1(X1)),true) ).
cnf(u1921,negated_conjecture,
true = ifeq2(true,true,eventuality(skc6,skf1(X0)),true) ).
cnf(u37,axiom,
true = ifeq2(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u3117,negated_conjecture,
true = nonhuman(skc5,skc8) ).
cnf(u345,negated_conjecture,
true = ifeq2(true,true,entity(skc5,skc9),true) ).
cnf(u191,negated_conjecture,
true = relation(skc5,skc6) ).
cnf(u626,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,theme(X0,skc7,skc6),true) ).
cnf(u977,negated_conjecture,
true = eventuality(skc6,skc7) ).
cnf(u31,axiom,
true = ifeq2(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u353,negated_conjecture,
true = ifeq2(of(X0,skc8,skc9),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u2414,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,living(X0,skc9),true) ).
cnf(u1831,negated_conjecture,
true = ifeq2(true,true,unisex(skc5,skc8),true) ).
cnf(u1274,negated_conjecture,
skc6 = ifeq3(agent(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X0),true,skc6,skc6),skc6) ).
cnf(u17,axiom,
true = ifeq2(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u341,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(organism(X0,skc9),true,true,true),true) ).
cnf(u1734,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(human(X0,skc9),true,true,true),true) ).
cnf(u3798,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skf1(X1)),true) ).
cnf(u297,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(animate(X0,skc9),true,true,true),true) ).
cnf(u1458,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,unisex(X0,skc6),true) ).
cnf(u2948,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc6),true) ).
cnf(u3168,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(general(X0,skc8),true,true,true),true) ).
cnf(u1787,negated_conjecture,
true = abstraction(skc6,skc6) ).
cnf(u3285,negated_conjecture,
true = ifeq2(eventuality(skc6,skc9),true,true,true) ).
cnf(u291,negated_conjecture,
true = ifeq2(think_believe_consider(skc5,X0),true,think_believe_consider(skc6,X0),true) ).
cnf(u806,negated_conjecture,
skc8 = ifeq3(of(skc6,X0,X1),true,ifeq3(of(skc6,skc8,X1),true,ifeq3(forename(skc6,X0),true,ifeq3(entity(skc6,X1),true,X0,skc8),skc8),skc8),skc8) ).
cnf(u282,negated_conjecture,
true = ifeq2(true,true,ifeq2(male(skc5,X0),true,male(skc6,X0),true),true) ).
cnf(u3851,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u2541,negated_conjecture,
true = thing(skc5,skc9) ).
cnf(u1263,negated_conjecture,
skc6 = ifeq3(theme(skc5,skc7,X0),true,ifeq3(proposition(skc5,X0),true,X0,skc6),skc6) ).
cnf(u3777,negated_conjecture,
true = ifeq2(abstraction(skc6,skf1(X0)),true,true,true) ).
cnf(u343,negated_conjecture,
true = ifeq2(true,true,living(skc5,skc9),true) ).
cnf(u3282,negated_conjecture,
true = ifeq2(abstraction(skc6,skc9),true,true,true) ).
cnf(u221,negated_conjecture,
true = ifeq2(true,true,ifeq2(singleton(skc5,X0),true,singleton(skc6,X0),true),true) ).
cnf(u1465,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,X1),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u1377,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc6),true) ).
cnf(u573,negated_conjecture,
true = ifeq2(abstraction(skc5,X0),true,abstraction(skc6,X0),true) ).
cnf(u1206,negated_conjecture,
skc8 = ifeq3(entity(skc5,skc9),true,skc8,skc8) ).
cnf(u3260,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u3223,negated_conjecture,
b = ifeq(tuple(true,male(skc5,skc8)),tuple(true,true),a,b) ).
cnf(u2763,negated_conjecture,
true = nonhuman(skc6,skc6) ).
cnf(u257,negated_conjecture,
b = ifeq(tuple(true,existent(skc5,skc7)),tuple(true,true),a,b) ).
cnf(u1050,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(male(X0,skc9),true,true,true),true) ).
cnf(u3808,negated_conjecture,
true = ifeq2(nonexistent(skc5,skf1(X0)),true,true,true) ).
cnf(u3011,negated_conjecture,
true = ifeq2(eventuality(skc5,skf1(X0)),true,true,true) ).
cnf(u636,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,of(X0,skc8,skc9),true) ).
cnf(u1215,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,living(X0,skc9),true) ).
cnf(u1566,negated_conjecture,
true = specific(skc6,skc7) ).
cnf(u1177,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc7),true,true,true),true) ).
cnf(u951,negated_conjecture,
skc8 = ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,ifeq3(entity(skc6,skc9),true,X0,skc8),skc8),skc8) ).
cnf(u3702,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonhuman(X0,skc8),true) ).
cnf(u235,negated_conjecture,
true = ifeq2(true,true,ifeq2(unisex(skc5,X0),true,unisex(skc6,X0),true),true) ).
cnf(u4003,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skf1(X1)),true,true,true),true) ).
cnf(u1951,negated_conjecture,
true = ifeq2(true,true,ifeq2(accessible_world(skc6,X0),true,agent(X0,skf1(skc9),skc9),true),true) ).
cnf(u111,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relname(X0,X2),true,relname(X1,X2),true),true) ).
cnf(u305,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,relation(X0,skc6),true) ).
cnf(u456,negated_conjecture,
true = ifeq2(true,true,specific(skc6,skc7),true) ).
cnf(u3137,negated_conjecture,
true = general(skc5,skc8) ).
cnf(u2648,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6) ).
cnf(u616,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,agent(X0,skc7,skc9),true) ).
cnf(u237,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(specific(X0,skc7),true,true,true),true) ).
cnf(u1445,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,general(X0,skc6),true) ).
cnf(u243,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,specific(X0,skc7),true) ).
cnf(u1375,negated_conjecture,
true = ifeq2(eventuality(skc5,skc6),true,true,true) ).
cnf(u1822,negated_conjecture,
true = abstraction(skc5,skc8) ).
cnf(u1851,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relation(X0,skc8),true) ).
cnf(u3280,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u231,negated_conjecture,
true = ifeq2(true,true,ifeq2(specific(skc5,X0),true,specific(skc6,X0),true),true) ).
cnf(u3373,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(existent(X0,skc9),true,true,true),true) ).
cnf(u3103,negated_conjecture,
true = thing(skc5,skc8) ).
cnf(u2704,negated_conjecture,
true = thing(skc6,skc6) ).
cnf(u218,negated_conjecture,
true = ifeq2(true,true,ifeq2(thing(skc5,X0),true,thing(skc6,X0),true),true) ).
cnf(u800,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(forename(X0,skc8),true,true,true),true) ).
cnf(u97,axiom,
true = ifeq2(think_believe_consider(X0,X1),true,ifeq2(accessible_world(X0,X2),true,think_believe_consider(X2,X1),true),true) ).
cnf(u301,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,animate(X0,skc9),true) ).
cnf(u217,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,eventuality(X0,skc7),true) ).
cnf(u1319,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,entity(X0,skc9),true) ).
cnf(u408,negated_conjecture,
true = ifeq2(true,true,think_believe_consider(skc6,skc7),true) ).
cnf(u1913,negated_conjecture,
true = agent(skc6,skf1(skc9),skc9) ).
cnf(u1571,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skc7),true,true,true),true) ).
cnf(u3039,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,present(X0,skf1(X1)),true) ).
cnf(u1160,negated_conjecture,
true = singleton(skc5,skc7) ).
cnf(u2125,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0) = X0 ).
cnf(u497,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(man(X0,skc9),true,true,true),true) ).
cnf(u575,negated_conjecture,
true = ifeq2(true,true,abstraction(skc6,skc6),true) ).
cnf(u176,negated_conjecture,
true = ifeq2(true,true,relation(skc5,skc6),true) ).
cnf(u11,axiom,
true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u295,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,proposition(X0,skc6),true) ).
cnf(u214,negated_conjecture,
true = ifeq2(true,true,ifeq2(eventuality(skc5,X0),true,eventuality(skc6,X0),true),true) ).
cnf(u1937,negated_conjecture,
true = ifeq2(smoke(skc5,skf1(X0)),true,true,true) ).
cnf(u2860,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0) = X0 ).
cnf(u374,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(theme(skc5,X2,skc6),true,ifeq3(agent(skc5,X0,X3),true,ifeq3(agent(skc5,X2,X3),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(think_believe_consider(skc5,X2),true,ifeq3(proposition(skc5,X1),true,skc6,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u213,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,event(X0,skc7),true) ).
cnf(u3724,negated_conjecture,
true = general(skc6,skc8) ).
cnf(u599,negated_conjecture,
true = ifeq2(forename(skc5,X0),true,forename(skc6,X0),true) ).
cnf(u200,negated_conjecture,
true = ifeq2(true,true,abstraction(skc5,skc6),true) ).
cnf(u1947,negated_conjecture,
true = ifeq2(agent(skc5,skf1(skc9),skc9),true,true,true) ).
cnf(u1725,negated_conjecture,
true = human(skc6,skc9) ).
cnf(u360,negated_conjecture,
ifeq3(of(skc5,skc8,X0),true,ifeq3(of(skc5,X1,X0),true,ifeq3(forename(skc5,X1),true,ifeq3(entity(skc5,X0),true,skc8,X1),X1),X1),X1) = X1 ).
cnf(u225,negated_conjecture,
true = ifeq2(abstraction(skc5,skc7),true,true,true) ).
cnf(u172,negated_conjecture,
true = ifeq2(true,true,nonexistent(skc5,skc7),true) ).
cnf(u13,axiom,
true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u163,negated_conjecture,
true = ifeq2(smoke(skc5,skc7),true,true,true) ).
cnf(u354,negated_conjecture,
true = ifeq2(of(skc5,X0,X1),true,of(skc6,X0,X1),true) ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u3676,negated_conjecture,
true = ifeq2(entity(skc6,skc8),true,true,true) ).
cnf(u3019,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(eventuality(X0,skf1(X1)),true,true,true),true) ).
cnf(u165,negated_conjecture,
true = eventuality(skc5,skc7) ).
cnf(u1625,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc7),true,true,true),true) ).
cnf(u1845,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relation(X0,skc8),true,true,true),true) ).
cnf(u473,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,present(X0,skc7),true) ).
cnf(u551,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,think_believe_consider(X0,skc7),true) ).
cnf(clause64,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(u159,axiom,
b = ifeq(tuple(human(X0,X1),nonhuman(X0,X1)),tuple(true,true),a,b) ).
cnf(u1327,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,X0,skc8),skc8) ).
cnf(u1953,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skf1(skc9),X2),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u467,negated_conjecture,
true = ifeq2(present(X0,skc7),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u3812,negated_conjecture,
b = ifeq(tuple(true,existent(skc6,skf1(X0))),tuple(true,true),a,b) ).
cnf(u115,axiom,
true = ifeq2(agent(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).
cnf(u493,negated_conjecture,
true = ifeq2(true,true,event(skc6,skf1(X0)),true) ).
cnf(u306,negated_conjecture,
true = ifeq2(true,true,ifeq2(abstraction(skc5,X0),true,abstraction(skc6,X0),true),true) ).
cnf(u145,negated_conjecture,
true = theme(skc5,skc7,skc6) ).
cnf(u3065,negated_conjecture,
true = abstraction(skc6,skc8) ).
cnf(u135,negated_conjecture,
true = think_believe_consider(skc5,skc7) ).
cnf(u2054,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,theme(X0,skc7,skc6),true) ).
cnf(u2612,negated_conjecture,
ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,skc8,X0),X0) = X0 ).
cnf(u117,axiom,
true = ifeq2(theme(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).
cnf(u3433,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,skf1(skc9),X1),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u2188,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u2942,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc6),true,true,true),true) ).
cnf(u1631,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc7),true) ).
cnf(u1923,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,event(X0,skf1(X1)),true) ).
cnf(u492,negated_conjecture,
true = ifeq2(true,true,agent(skc6,skf1(skc9),skc9),true) ).
cnf(u578,negated_conjecture,
true = ifeq2(nonhuman(skc5,X0),true,nonhuman(skc6,X0),true) ).
cnf(u269,negated_conjecture,
true = ifeq2(true,true,ifeq2(existent(skc5,X0),true,existent(skc6,X0),true),true) ).
cnf(u2161,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0) = X0 ).
cnf(u302,negated_conjecture,
true = ifeq2(true,true,ifeq2(relation(skc5,X0),true,relation(skc6,X0),true),true) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP220-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n002.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 18:33:22 UTC 2026
% 0.10/0.40 % CPUTime :
% 0.10/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.43 Running first-order model finding
% 0.10/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.56 % (3799226)Will run a generic schedule for satisfiability detection.
% 0.15/0.56 % (3799232)% WARNING: option uhcvi not known.
% 0.15/0.56 % (3799232)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2159967775:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.15/0.56 % (3799234)dis+10_1_sil=32000:sp=arity:random_seed=3127684098:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.15/0.56 % (3799231)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1799854488_2999 on theBenchmark for (2999ds/0Mi)
% 0.15/0.56 % (3799233)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1123366020:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.15/0.56 % (3799235)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3634957678:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.15/0.56 % (3799236)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1326762352:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.15/0.56 % (3799237)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1615575347:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.15/0.56 % TRYING [1]
% 0.15/0.56 % TRYING [2]
% 0.15/0.56 % TRYING [3]
% 0.15/0.56 % (3799234)Instruction limit reached!
% 0.15/0.56 % (3799234)------------------------------
% 0.15/0.56 % (3799234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/0.56 % (3799234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/0.56 % (3799234)CaDiCaL version: 2.1.3
% 0.15/0.56 % (3799234)Termination reason: Instruction limit
% 0.15/0.56 % (3799234)Termination phase: Saturation
% 0.15/0.56 % (3799234)Time elapsed: 0.060 s
% 0.15/0.56 % (3799234)Peak memory usage: 12 MB
% 0.15/0.56 % (3799234)Instructions burned: 104 (million)
% 0.15/0.56 % (3799235)Instruction limit reached!
% 0.15/0.56 % (3799235)------------------------------
% 0.15/0.56 % (3799235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/0.56 % (3799235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/0.56 % (3799235)CaDiCaL version: 2.1.3
% 0.15/0.56 % (3799235)Termination reason: Instruction limit
% 0.15/0.56 % (3799235)Termination phase: Saturation
% 0.15/0.56 % (3799235)Time elapsed: 0.067 s
% 0.15/0.56 % (3799235)Peak memory usage: 12 MB
% 0.15/0.56 % (3799235)Instructions burned: 116 (million)
% 0.15/0.56 % (3799236)Instruction limit reached!
% 0.15/0.56 % (3799236)------------------------------
% 0.15/0.56 % (3799236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/0.56 % (3799236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/0.56 % (3799236)CaDiCaL version: 2.1.3
% 0.15/0.56 % (3799236)Termination reason: Instruction limit
% 0.15/0.56 % (3799236)Termination phase: Saturation
% 0.15/0.56 % (3799236)Time elapsed: 0.077 s
% 0.15/0.56 % (3799236)Peak memory usage: 12 MB
% 0.15/0.56 % (3799236)Instructions burned: 132 (million)
% 0.15/0.56 % (3799245)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=53803660:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.15/0.56 % (3799232) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3799226-3799232"...
% 0.15/0.56 % (3799246)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1238496432:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.15/0.56 % (3799232)...printing done.
% 0.15/0.56 % SZS status Satisfiable for theBenchmark
% 0.15/0.56 % SZS output start Saturation.
% See solution above
% 0.95/0.57 % SZS output start Definitions and Model Updates.
% 0.95/0.57 % SZS output end Definitions and Model Updates.
% 0.95/0.57 % (3799232)------------------------------
% 0.95/0.57 % (3799232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.95/0.57 % (3799232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.95/0.57 % (3799232)CaDiCaL version: 2.1.3
% 0.95/0.57 % (3799232)Termination reason: Satisfiable
% 0.95/0.57 % (3799232)Time elapsed: 0.096 s
% 0.95/0.57 % (3799232)Peak memory usage: 14 MB
% 0.95/0.57 % (3799232)Instructions burned: 298 (million)
% 0.95/0.57 % (3799226)Success in time 0.123 s
% 0.95/0.57 % Vampire exiting
%------------------------------------------------------------------------------