Vampire-SAT---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : NLP225-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 : n014.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:31 PM UTC 2026

% Result   : Satisfiable 1.31s 0.68s
% Output   : Saturation 1.31s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u1021,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(theme(skc8,X1,skc11),true,ifeq3(agent(skc8,X0,X2),true,ifeq3(agent(skc8,X1,X2),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(think_believe_consider(skc8,X1),true,skc11,skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u1415,negated_conjecture,
    true = human(skc8,skc14) ).

cnf(u778,negated_conjecture,
    skc13 = ifeq3(true,true,ifeq3(entity(skc8,skc14),true,skc15,skc13),skc13) ).

cnf(u3356,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,abstraction(X0,skc11),true) ).

cnf(u1158,negated_conjecture,
    ifeq3(true,true,ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,skc14),true,skc13,X0),X0),X0),X0) = X0 ).

cnf(u5065,negated_conjecture,
    b = ifeq(tuple(true,male(skc11,skf1(X0))),tuple(true,true),a,b) ).

cnf(u21,axiom,
    true = ifeq2(man(X0,X1),true,human_person(X0,X1),true) ).

cnf(u2330,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X1),true,present(X1,skf1(X0)),true),true) ).

cnf(u289,negated_conjecture,
    true = ifeq2(true,true,ifeq2(organism(skc8,X0),true,organism(skc11,X0),true),true) ).

cnf(u556,negated_conjecture,
    true = forename(skc11,skc13) ).

cnf(u279,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(man(X0,skc14),true,true,true),true) ).

cnf(u276,negated_conjecture,
    true = ifeq2(true,true,ifeq2(man(skc8,X0),true,man(skc11,X0),true),true) ).

cnf(u406,negated_conjecture,
    true = ifeq2(true,true,abstraction(skc8,skc11),true) ).

cnf(u805,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,X1,X2),true,ifeq3(agent(skc11,X0,X3),true,ifeq3(agent(skc11,X1,X3),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X2),true,X2,skc11),skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u1327,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc12),true,true,true),true) ).

cnf(u1298,negated_conjecture,
    true = ifeq2(abstraction(skc8,skc12),true,true,true) ).

cnf(u3353,negated_conjecture,
    true = ifeq2(true,true,unisex(skc11,skc11),true) ).

cnf(u3107,negated_conjecture,
    true = ifeq2(true,true,specific(skc8,skc14),true) ).

cnf(u4398,negated_conjecture,
    true = nonhuman(skc11,skc11) ).

cnf(u3733,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,living(X0,skc14),true) ).

cnf(u3862,negated_conjecture,
    true = ifeq2(true,true,singleton(skc8,skc14),true) ).

cnf(u1821,negated_conjecture,
    true = ifeq2(relname(skc11,skc11),true,true,true) ).

cnf(u1587,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,eventuality(X0,skc9),true) ).

cnf(u160,negated_conjecture,
    true = state(skc8,skc9) ).

cnf(u538,negated_conjecture,
    true = ifeq2(true,true,event(skc11,skf1(X0)),true) ).

cnf(u3249,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(relation(X0,skc15),true,true,true),true) ).

cnf(u61,axiom,
    true = ifeq2(proposition(X0,X1),true,relation(X0,X1),true) ).

cnf(u293,negated_conjecture,
    b = ifeq(tuple(unisex(skc8,skc14),true),tuple(true,true),a,b) ).

cnf(u561,negated_conjecture,
    true = ifeq2(jules_forename(skc11,skc13),true,true,true) ).

cnf(u316,negated_conjecture,
    true = ifeq2(true,true,ifeq2(abstraction(skc8,X0),true,abstraction(skc11,X0),true),true) ).

cnf(u3131,negated_conjecture,
    skc15 = ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,X0,skc15),skc15) ).

cnf(u4387,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc11),true,true,true),true) ).

cnf(u2715,negated_conjecture,
    skc11 = ifeq3(true,true,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),skc11) ).

cnf(u166,negated_conjecture,
    true = of(skc8,skc13,skc14) ).

cnf(u2472,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc9),true,true,true),true) ).

cnf(u575,negated_conjecture,
    true = ifeq2(living(skc8,X0),true,living(skc11,X0),true) ).

cnf(u3625,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skc12,X0),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11) ).

cnf(u1332,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc12),true) ).

cnf(u51,axiom,
    true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).

cnf(u189,negated_conjecture,
    true = eventuality(skc8,skc9) ).

cnf(u421,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,X1,X2),true,ifeq3(agent(skc8,skc12,X3),true,ifeq3(agent(skc8,X1,X3),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X0),true,ifeq3(proposition(skc8,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1467,negated_conjecture,
    true = ifeq2(proposition(skc8,skc15),true,true,true) ).

cnf(u5096,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc11),true) ).

cnf(u164,negated_conjecture,
    true = agent(skc8,skc12,skc14) ).

cnf(u4007,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc14),true) ).

cnf(u5137,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc14),true,true,true),true) ).

cnf(u4642,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skc14),true,true,true),true) ).

cnf(u1460,negated_conjecture,
    true = relation(skc8,skc15) ).

cnf(u335,negated_conjecture,
    true = ifeq2(true,true,ifeq2(jules_forename(skc8,X0),true,jules_forename(skc11,X0),true),true) ).

cnf(u571,negated_conjecture,
    true = ifeq2(existent(skc8,X0),true,existent(skc11,X0),true) ).

cnf(u78,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(unisex(X0,X2),true,unisex(X1,X2),true),true) ).

cnf(u956,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc14),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).

cnf(u333,negated_conjecture,
    true = ifeq2(true,true,ifeq2(nonhuman(skc8,X0),true,nonhuman(skc11,X0),true),true) ).

cnf(u76,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).

cnf(u3403,negated_conjecture,
    skc15 = ifeq3(entity(skc11,skc14),true,skc15,skc15) ).

cnf(u1117,negated_conjecture,
    true = theme(skc11,skc12,skc11) ).

cnf(u323,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,relname(X0,skc15),true) ).

cnf(u461,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(state(X0,skc9),true,true,true),true) ).

cnf(u712,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,present(X0,skc12),true),true) ).

cnf(u346,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc12),true,ifeq2(accessible_world(X0,skc8),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(u2633,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skc9),true) ).

cnf(u204,negated_conjecture,
    true = event(skc8,skc9) ).

cnf(u3678,negated_conjecture,
    true = singleton(skc11,skc12) ).

cnf(u1376,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc12),true,true,true),true) ).

cnf(u3410,negated_conjecture,
    b = ifeq(tuple(specific(skc8,skc11),true),tuple(true,true),a,b) ).

cnf(u2915,negated_conjecture,
    b = ifeq(tuple(true,male(skc11,skc9)),tuple(true,true),a,b) ).

cnf(u451,negated_conjecture,
    true = state(skc11,skc9) ).

cnf(u344,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,think_believe_consider(X0,skc12),true),true) ).

cnf(u5087,negated_conjecture,
    true = singleton(skc11,skc11) ).

cnf(u116,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(smoke(X0,X2),true,smoke(X1,X2),true),true) ).

cnf(u3787,negated_conjecture,
    true = ifeq2(true,true,specific(skc11,skc14),true) ).

cnf(u3921,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11) ).

cnf(u2516,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,agent(X0,skc12,skc14),true) ).

cnf(u3806,negated_conjecture,
    skc15 = ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,X0,skc15),skc15) ).

cnf(u887,negated_conjecture,
    skc15 = ifeq3(of(skc8,skc13,X0),true,ifeq3(of(skc8,skc15,X0),true,ifeq3(entity(skc8,X0),true,skc13,skc15),skc15),skc15) ).

cnf(u2930,negated_conjecture,
    b = ifeq(tuple(true,male(skc11,skc12)),tuple(true,true),a,b) ).

cnf(u4552,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,general(X0,skc11),true) ).

cnf(u5081,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

cnf(u996,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,X1,skc11),true,ifeq3(agent(skc8,X1,skc14),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X0),true,skc11,X0),X0),X0),X0),X0) = X0 ).

cnf(u3043,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,human(X0,skc14),true) ).

cnf(u5013,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skf1(X1)),true) ).

cnf(u350,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(proposition(X0,skc11),true,true,true),true) ).

cnf(u106,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(relation(X0,X2),true,relation(X1,X2),true),true) ).

cnf(u622,negated_conjecture,
    true = ifeq2(relname(skc8,X0),true,relname(skc11,X0),true) ).

cnf(u1136,negated_conjecture,
    true = ifeq2(of(X0,skc15,skc14),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u4218,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc15),true,true,true),true) ).

cnf(u361,negated_conjecture,
    true = ifeq2(of(skc8,X0,X1),true,of(skc11,X0,X1),true) ).

cnf(u2540,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,be(X0,skc9,skc14,skc14),true) ).

cnf(u1552,negated_conjecture,
    skc15 = ifeq3(entity(skc8,skc14),true,skc13,skc15) ).

cnf(u478,negated_conjecture,
    true = ifeq2(accessible_world(skc11,skc8),true,true,true) ).

cnf(u104,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(relname(X0,X2),true,relname(X1,X2),true),true) ).

cnf(u1592,negated_conjecture,
    true = event(skc11,skc9) ).

cnf(u1796,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc14),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11) ).

cnf(u4569,negated_conjecture,
    true = singleton(skc8,skc11) ).

cnf(u750,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,X1,X2),true,ifeq3(agent(skc11,skc12,X3),true,ifeq3(agent(skc11,X1,X3),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u3317,negated_conjecture,
    true = ifeq2(true,true,general(skc8,skc15),true) ).

cnf(u1264,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc9),true) ).

cnf(u7,axiom,
    true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).

cnf(u5004,negated_conjecture,
    true = ifeq2(thing(skc8,skf1(X0)),true,true,true) ).

cnf(u262,negated_conjecture,
    true = ifeq2(true,true,ifeq2(singleton(skc8,X0),true,singleton(skc11,X0),true),true) ).

cnf(u3863,negated_conjecture,
    true = ifeq2(eventuality(skc8,skc14),true,true,true) ).

cnf(u1527,negated_conjecture,
    true = ifeq2(true,true,relation(skc11,skc13),true) ).

cnf(u3321,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc15),true) ).

cnf(u534,negated_conjecture,
    true = ifeq2(true,true,human_person(skc11,skc14),true) ).

cnf(u3052,negated_conjecture,
    true = ifeq2(true,true,living(skc11,skc14),true) ).

cnf(u801,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(proposition(X0,skc11),true,true,true),true) ).

cnf(u3318,negated_conjecture,
    true = ifeq2(true,true,unisex(skc8,skc15),true) ).

cnf(u5,axiom,
    true = ifeq2(state(X0,X1),true,eventuality(X0,X1),true) ).

cnf(u45,axiom,
    true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).

cnf(u2314,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(event(X0,skf1(X1)),true,true,true),true) ).

cnf(u273,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc9),true,true,true),true) ).

cnf(u540,negated_conjecture,
    true = ifeq2(true,true,smoke(skc11,skf1(X0)),true) ).

cnf(u3057,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,organism(X0,skc14),true) ).

cnf(u260,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc9),true) ).

cnf(u390,negated_conjecture,
    ifeq3(of(skc8,skc13,X0),true,ifeq3(of(skc8,X1,X0),true,ifeq3(forename(skc8,X1),true,ifeq3(entity(skc8,X0),true,skc13,X1),X1),X1),X1) = X1 ).

cnf(u1556,negated_conjecture,
    true = eventuality(skc11,skc12) ).

cnf(u2846,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skf1(skc14),X1),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u2312,negated_conjecture,
    true = ifeq2(event(skc8,skf1(X0)),true,true,true) ).

cnf(u4102,negated_conjecture,
    true = ifeq2(true,true,nonexistent(skc11,skf1(X0)),true) ).

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(u1679,negated_conjecture,
    true = male(skc11,skc14) ).

cnf(u1554,negated_conjecture,
    skc15 = ifeq3(entity(skc8,skc14),true,skc15,skc15) ).

cnf(u303,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(male(X0,skc14),true,true,true),true) ).

cnf(u388,negated_conjecture,
    skc13 = ifeq3(of(skc8,X0,X1),true,ifeq3(of(skc8,skc13,X1),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,X1),true,X0,skc13),skc13),skc13),skc13) ).

cnf(u144,negated_conjecture,
    true = vincent_forename(skc8,skc13) ).

cnf(u1439,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(organism(X0,skc14),true,true,true),true) ).

cnf(u2318,negated_conjecture,
    true = ifeq2(state(skc11,skf1(X0)),true,true,true) ).

cnf(u4608,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc14),true,true,true),true) ).

cnf(u522,negated_conjecture,
    true = ifeq2(man(skc8,X0),true,man(skc11,X0),true) ).

cnf(u2974,negated_conjecture,
    true = ifeq2(entity(skc11,skc12),true,true,true) ).

cnf(u2329,negated_conjecture,
    true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u4425,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonhuman(X0,skc11),true,true,true),true) ).

cnf(u2701,negated_conjecture,
    ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0) = X0 ).

cnf(u407,negated_conjecture,
    true = ifeq2(relname(skc8,skc11),true,true,true) ).

cnf(u5010,negated_conjecture,
    true = ifeq2(true,true,singleton(skc11,skf1(X0)),true) ).

cnf(u3202,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(vincent_forename(X0,skc15),true,true,true),true) ).

cnf(u300,negated_conjecture,
    true = ifeq2(true,true,ifeq2(animate(skc8,X0),true,animate(skc11,X0),true),true) ).

cnf(u1153,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,of(X0,skc13,skc14),true),true) ).

cnf(u150,negated_conjecture,
    true = present(skc8,skc12) ).

cnf(u1688,negated_conjecture,
    b = ifeq(tuple(unisex(skc11,skc14),true),tuple(true,true),a,b) ).

cnf(u35,axiom,
    true = ifeq2(organism(X0,X1),true,living(X0,X1),true) ).

cnf(u2356,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc14),skc14),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u2999,negated_conjecture,
    true = abstraction(skc8,skc15) ).

cnf(u656,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,think_believe_consider(X0,skc12),true) ).

cnf(u290,negated_conjecture,
    true = ifeq2(true,true,ifeq2(entity(skc8,X0),true,entity(skc11,X0),true),true) ).

cnf(u673,negated_conjecture,
    true = ifeq2(vincent_forename(skc8,X0),true,vincent_forename(skc11,X0),true) ).

cnf(u148,negated_conjecture,
    true = think_believe_consider(skc8,skc12) ).

cnf(u2843,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,X0,X2),true,ifeq3(agent(skc11,X1,X2),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,X1),true,skc11,skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u806,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(theme(skc11,X2,skc11),true,ifeq3(agent(skc11,X0,X3),true,ifeq3(agent(skc11,X2,X3),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,X2),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4648,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skc14),true) ).

cnf(u3737,negated_conjecture,
    true = impartial(skc11,skc14) ).

cnf(u2358,negated_conjecture,
    ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(theme(skc11,X1,X2),true,ifeq3(agent(skc11,X1,skc14),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u568,negated_conjecture,
    ifeq3(of(skc11,skc13,X0),true,ifeq3(of(skc11,X1,X0),true,ifeq3(forename(skc11,X1),true,ifeq3(entity(skc11,X0),true,skc13,X1),X1),X1),X1) = X1 ).

cnf(u447,negated_conjecture,
    true = ifeq2(true,true,jules_forename(skc11,skc15),true) ).

cnf(u2973,negated_conjecture,
    b = ifeq(tuple(true,general(skc11,skc12)),tuple(true,true),a,b) ).

cnf(u418,negated_conjecture,
    ifeq3(theme(skc8,X0,X1),true,ifeq3(theme(skc8,X2,skc11),true,ifeq3(agent(skc8,X0,X3),true,ifeq3(agent(skc8,X2,X3),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(think_believe_consider(skc8,X2),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2740,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,skf1(skc14),X1),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u2629,negated_conjecture,
    b = ifeq(tuple(true,general(skc11,skc9)),tuple(true,true),a,b) ).

cnf(u2971,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skc12),true,true,true),true) ).

cnf(u934,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(u804,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,proposition(X0,skc11),true) ).

cnf(u2627,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skc9),true,true,true),true) ).

cnf(u307,negated_conjecture,
    true = ifeq2(true,true,ifeq2(forename(skc8,X0),true,forename(skc11,X0),true),true) ).

cnf(u445,negated_conjecture,
    true = ifeq2(true,true,forename(skc11,skc15),true) ).

cnf(u1442,negated_conjecture,
    true = ifeq2(true,true,impartial(skc8,skc14),true) ).

cnf(u4613,negated_conjecture,
    true = ifeq2(eventuality(skc11,skc14),true,true,true) ).

cnf(u188,negated_conjecture,
    true = ifeq2(true,true,eventuality(skc8,skc9),true) ).

cnf(u2992,negated_conjecture,
    true = ifeq2(true,true,singleton(skc11,skc12),true) ).

cnf(u983,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,skc12,X1),true,ifeq3(proposition(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u1356,negated_conjecture,
    true = ifeq2(entity(skc8,skc12),true,true,true) ).

cnf(u1204,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,theme(X0,skc12,skc11),true),true) ).

cnf(u435,negated_conjecture,
    skc11 = ifeq3(true,true,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),skc11) ).

cnf(u3518,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).

cnf(u3050,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(organism(X0,skc14),true,true,true),true) ).

cnf(u178,negated_conjecture,
    true = ifeq2(man(skc11,X0),true,agent(skc11,skf1(X0),X0),true) ).

cnf(u1465,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc15),true,true,true),true) ).

cnf(u1293,negated_conjecture,
    true = ifeq2(true,true,unisex(skc11,skc12),true) ).

cnf(u2901,negated_conjecture,
    b = ifeq(tuple(true,existent(skc11,skc9)),tuple(true,true),a,b) ).

cnf(u3113,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,entity(X0,skc14),true) ).

cnf(u4984,negated_conjecture,
    true = thing(skc11,skf1(X0)) ).

cnf(u2899,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonexistent(X0,skc9),true,true,true),true) ).

cnf(u3110,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(entity(X0,skc14),true,true,true),true) ).

cnf(u482,negated_conjecture,
    true = ifeq2(eventuality(skc8,X0),true,eventuality(skc11,X0),true) ).

cnf(u1227,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc9),true) ).

cnf(u1111,negated_conjecture,
    true = of(skc11,skc15,skc14) ).

cnf(u458,negated_conjecture,
    true = ifeq2(true,true,of(skc11,skc13,skc14),true) ).

cnf(u100,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(male(X0,X2),true,male(X1,X2),true),true) ).

cnf(u3683,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc12),true,true,true),true) ).

cnf(u587,negated_conjecture,
    true = ifeq2(vincent_forename(skc11,skc15),true,true,true) ).

cnf(u3790,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(entity(X0,skc14),true,true,true),true) ).

cnf(u3029,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,animate(X0,skc14),true) ).

cnf(u871,negated_conjecture,
    skc13 = ifeq3(of(skc8,skc15,X0),true,ifeq3(of(skc8,skc13,X0),true,ifeq3(entity(skc8,X0),true,skc15,skc13),skc13),skc13) ).

cnf(u4969,negated_conjecture,
    b = ifeq(tuple(specific(skc11,skc15),true),tuple(true,true),a,b) ).

cnf(u3522,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc9),true) ).

cnf(u347,negated_conjecture,
    true = ifeq2(think_believe_consider(skc8,X0),true,think_believe_consider(skc11,X0),true) ).

cnf(u1246,negated_conjecture,
    true = nonexistent(skc8,skc9) ).

cnf(u334,negated_conjecture,
    true = ifeq2(true,true,ifeq2(general(skc8,X0),true,general(skc11,X0),true),true) ).

cnf(u90,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(existent(X0,X2),true,existent(X1,X2),true),true) ).

cnf(u4033,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc8,skc14),true),tuple(true,true),a,b) ).

cnf(u1549,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc11),true) ).

cnf(u4168,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,agent(X0,skf1(skc14),skc14),true) ).

cnf(u3802,negated_conjecture,
    ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,skc15,X0),X0) = X0 ).

cnf(u629,negated_conjecture,
    true = ifeq2(true,true,relation(skc11,skc11),true) ).

cnf(u368,negated_conjecture,
    true = ifeq2(theme(X0,skc12,skc11),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u88,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(entity(X0,X2),true,entity(X1,X2),true),true) ).

cnf(u1383,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc12),true) ).

cnf(u218,negated_conjecture,
    true = ifeq2(true,true,unisex(skc8,skc12),true) ).

cnf(u627,negated_conjecture,
    true = ifeq2(relation(skc8,X0),true,relation(skc11,X0),true) ).

cnf(u2908,negated_conjecture,
    true = unisex(skc11,skc9) ).

cnf(u4574,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc11),true,true,true),true) ).

cnf(u5069,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skf1(X1)),true) ).

cnf(u3167,negated_conjecture,
    true = vincent_forename(skc8,skc15) ).

cnf(u2913,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc9),true,true,true),true) ).

cnf(u740,negated_conjecture,
    true = think_believe_consider(skc11,skc12) ).

cnf(u4103,negated_conjecture,
    true = ifeq2(true,true,unisex(skc11,skf1(X0)),true) ).

cnf(u3393,negated_conjecture,
    b = ifeq(tuple(human(skc8,skc11),true),tuple(true,true),a,b) ).

cnf(u3178,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(vincent_forename(X0,skc15),true,true,true),true) ).

cnf(u4993,negated_conjecture,
    b = ifeq(tuple(true,male(skc11,skc15)),tuple(true,true),a,b) ).

cnf(u1773,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(relname(X0,skc15),true,true,true),true) ).

cnf(u247,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,state(X0,skc9),true) ).

cnf(u4986,negated_conjecture,
    true = specific(skc11,skf1(X0)) ).

cnf(u257,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc9),true,true,true),true) ).

cnf(u2419,negated_conjecture,
    true = thing(skc11,skc9) ).

cnf(u1823,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,relation(X0,skc11),true) ).

cnf(u4101,negated_conjecture,
    true = ifeq2(true,true,specific(skc11,skf1(X0)),true) ).

cnf(u1295,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc12),true,true,true),true) ).

cnf(u1540,negated_conjecture,
    true = ifeq2(true,true,abstraction(skc11,skc11),true) ).

cnf(u1531,negated_conjecture,
    true = ifeq2(proposition(skc8,skc13),true,true,true) ).

cnf(u646,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,present(X0,skc12),true) ).

cnf(u4615,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc14),true) ).

cnf(u1137,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,of(X0,skc15,skc14),true),true) ).

cnf(u500,negated_conjecture,
    true = ifeq2(smoke(skc11,skc12),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(u4599,negated_conjecture,
    true = thing(skc11,skc14) ).

cnf(u1522,negated_conjecture,
    skc13 = ifeq3(entity(skc8,skc14),true,skc13,skc13) ).

cnf(u3203,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,vincent_forename(X0,skc15),true) ).

cnf(u2958,negated_conjecture,
    true = animate(skc11,skc14) ).

cnf(u29,axiom,
    true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).

cnf(u792,negated_conjecture,
    skc15 = ifeq3(true,true,ifeq3(entity(skc8,skc14),true,skc15,skc15),skc15) ).

cnf(u261,negated_conjecture,
    true = ifeq2(true,true,ifeq2(thing(skc8,X0),true,thing(skc11,X0),true),true) ).

cnf(u3320,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc15),true,true,true),true) ).

cnf(u391,negated_conjecture,
    ifeq3(of(skc8,skc15,X0),true,ifeq3(of(skc8,X1,X0),true,ifeq3(forename(skc8,X1),true,ifeq3(entity(skc8,X0),true,skc15,X1),X1),X1),X1) = X1 ).

cnf(u529,negated_conjecture,
    true = man(skc11,skc14) ).

cnf(u2964,negated_conjecture,
    true = living(skc8,skc14) ).

cnf(u1574,negated_conjecture,
    true = eventuality(skc11,skc9) ).

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(u543,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(man(X0,skc14),true,true,true),true) ).

cnf(u4791,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc14),true) ).

cnf(u726,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,agent(X0,skc12,skc14),true) ).

cnf(u19,axiom,
    true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).

cnf(u2983,negated_conjecture,
    true = relation(skc11,skc15) ).

cnf(u389,negated_conjecture,
    skc15 = ifeq3(of(skc8,X0,X1),true,ifeq3(of(skc8,skc15,X1),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,X1),true,X0,skc15),skc15),skc15),skc15) ).

cnf(u274,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc9),true) ).

cnf(u1049,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,X0,X2),true,ifeq3(agent(skc8,skc12,X2),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).

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(u298,negated_conjecture,
    true = ifeq2(true,true,ifeq2(human(skc8,X0),true,human(skc11,X0),true),true) ).

cnf(u1434,negated_conjecture,
    true = organism(skc8,skc14) ).

cnf(u17,axiom,
    true = ifeq2(state(X0,X1),true,event(X0,X1),true) ).

cnf(u301,negated_conjecture,
    true = ifeq2(true,true,ifeq2(male(skc8,X0),true,male(skc11,X0),true),true) ).

cnf(u552,negated_conjecture,
    true = ifeq2(organism(skc8,X0),true,organism(skc11,X0),true) ).

cnf(u431,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,X1,X2),true,ifeq3(agent(skc8,X1,skc14),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X0),true,ifeq3(proposition(skc8,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u569,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,forename(X0,skc13),true) ).

cnf(u4177,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u2479,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc9),true) ).

cnf(u4908,negated_conjecture,
    true = nonhuman(skc11,skc15) ).

cnf(u3371,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc11),true,true,true),true) ).

cnf(u174,negated_conjecture,
    true = ifeq2(man(skc11,X0),true,present(skc11,skf1(X1)),true) ).

cnf(u3724,negated_conjecture,
    true = living(skc11,skc14) ).

cnf(u1432,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,human(X0,skc14),true) ).

cnf(u4394,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc11),true) ).

cnf(u2353,negated_conjecture,
    true = ifeq2(agent(skc8,skf1(skc14),skc14),true,true,true) ).

cnf(u59,axiom,
    true = ifeq2(smoke(X0,X1),true,event(X0,X1),true) ).

cnf(u5009,negated_conjecture,
    true = ifeq2(entity(skc11,skf1(X0)),true,true,true) ).

cnf(u291,negated_conjecture,
    true = ifeq2(true,true,ifeq2(existent(skc8,X0),true,existent(skc11,X0),true),true) ).

cnf(u498,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(event(X0,skc12),true,true,true),true) ).

cnf(u3391,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc11),true,true,true),true) ).

cnf(u314,negated_conjecture,
    true = ifeq2(true,true,ifeq2(relname(skc8,X0),true,relname(skc11,X0),true),true) ).

cnf(u400,negated_conjecture,
    skc13 = ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,skc14),true,X0,skc13),skc13),skc13) ).

cnf(u1183,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,X1,X2),true,ifeq3(agent(skc11,X1,skc14),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u172,negated_conjecture,
    true = ifeq2(man(skc11,X0),true,smoke(skc11,skf1(X1)),true) ).

cnf(u1075,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,skc12,X2),true,ifeq3(agent(skc8,skc12,X2),true,ifeq3(proposition(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u830,negated_conjecture,
    true = vincent_forename(skc11,skc13) ).

cnf(u4036,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,existent(X0,skc14),true) ).

cnf(u4392,negated_conjecture,
    true = ifeq2(eventuality(skc11,skc11),true,true,true) ).

cnf(u943,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(proposition(skc8,X0),true,skc11,X0),X0) = X0 ).

cnf(u3378,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc11),true) ).

cnf(u57,axiom,
    true = ifeq2(jules_forename(X0,X1),true,forename(X0,X1),true) ).

cnf(u1468,negated_conjecture,
    true = ifeq2(true,true,abstraction(skc8,skc15),true) ).

cnf(goal,negated_conjecture,
    a != b ).

cnf(u419,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(theme(skc8,X1,X2),true,ifeq3(agent(skc8,X0,X3),true,ifeq3(agent(skc8,X1,X3),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X2),true,X2,skc11),skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u5038,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonexistent(X0,skf1(X1)),true,true,true),true) ).

cnf(u573,negated_conjecture,
    true = ifeq2(impartial(skc8,X0),true,impartial(skc11,X0),true) ).

cnf(u312,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,forename(X0,skc13),true) ).

cnf(u4143,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,present(X0,skf1(X1)),true) ).

cnf(u162,negated_conjecture,
    true = of(skc8,skc15,skc14) ).

cnf(u1203,negated_conjecture,
    true = ifeq2(theme(X0,skc12,skc11),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u63,axiom,
    true = ifeq2(vincent_forename(X0,X1),true,forename(X0,X1),true) ).

cnf(u836,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(vincent_forename(X0,skc13),true,true,true),true) ).

cnf(u3040,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc11,skc14)),tuple(true,true),a,b) ).

cnf(u318,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relname(X0,skc15),true,true,true),true) ).

cnf(u701,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,of(X0,skc13,skc14),true) ).

cnf(u84,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(human_person(X0,X2),true,human_person(X1,X2),true),true) ).

cnf(u4896,negated_conjecture,
    true = ifeq2(true,true,singleton(skc11,skc15),true) ).

cnf(u4031,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(existent(X0,skc14),true,true,true),true) ).

cnf(u3374,negated_conjecture,
    true = ifeq2(entity(skc8,skc11),true,true,true) ).

cnf(u4967,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(general(X0,skc15),true,true,true),true) ).

cnf(u1223,negated_conjecture,
    b = ifeq(tuple(true,general(skc8,skc9)),tuple(true,true),a,b) ).

cnf(u74,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(specific(X0,X2),true,specific(X1,X2),true),true) ).

cnf(u4297,negated_conjecture,
    true = general(skc8,skc15) ).

cnf(u5076,negated_conjecture,
    true = singleton(skc8,skc15) ).

cnf(u1115,negated_conjecture,
    true = agent(skc11,skc12,skc14) ).

cnf(u329,negated_conjecture,
    true = ifeq2(true,true,relation(skc8,skc13),true) ).

cnf(u1228,negated_conjecture,
    true = ifeq2(true,true,specific(skc11,skc9),true) ).

cnf(u5026,negated_conjecture,
    b = ifeq(tuple(true,general(skc11,skf1(X0))),tuple(true,true),a,b) ).

cnf(u352,negated_conjecture,
    true = ifeq2(true,true,ifeq2(vincent_forename(skc8,X0),true,vincent_forename(skc11,X0),true),true) ).

cnf(u72,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(singleton(X0,X2),true,singleton(X1,X2),true),true) ).

cnf(u202,negated_conjecture,
    true = ifeq2(true,true,human_person(skc8,skc14),true) ).

cnf(u156,negated_conjecture,
    true = accessible_world(skc8,skc11) ).

cnf(u2397,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).

cnf(u4184,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc15),true) ).

cnf(u4314,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u1537,negated_conjecture,
    true = abstraction(skc8,skc11) ).

cnf(u457,negated_conjecture,
    true = ifeq2(true,true,of(skc11,skc15,skc14),true) ).

cnf(u1627,negated_conjecture,
    skc11 = ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X0),true,skc11,skc11),skc11) ).

cnf(u4972,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,general(X0,skc15),true) ).

cnf(u4181,negated_conjecture,
    true = ifeq2(true,true,singleton(skc8,skc15),true) ).

cnf(u200,negated_conjecture,
    true = ifeq2(true,true,eventuality(skc8,skc12),true) ).

cnf(u5331,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skf1(X1)),true) ).

cnf(u630,negated_conjecture,
    true = ifeq2(abstraction(skc8,X0),true,abstraction(skc11,X0),true) ).

cnf(u3020,negated_conjecture,
    true = general(skc8,skc11) ).

cnf(u1374,negated_conjecture,
    true = ifeq2(true,true,thing(skc11,skc12),true) ).

cnf(u5085,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc15),true) ).

cnf(u231,negated_conjecture,
    true = ifeq2(true,true,relation(skc8,skc11),true) ).

cnf(u369,negated_conjecture,
    true = ifeq2(theme(skc8,X0,X1),true,theme(skc11,X0,X1),true) ).

cnf(u3025,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(animate(X0,skc14),true,true,true),true) ).

cnf(u356,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,of(X0,skc15,skc14),true),true) ).

cnf(u486,negated_conjecture,
    true = ifeq2(thing(skc8,X0),true,thing(skc11,X0),true) ).

cnf(u112,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(general(X0,X2),true,general(X1,X2),true),true) ).

cnf(u1407,negated_conjecture,
    true = ifeq2(true,true,animate(skc11,skc14),true) ).

cnf(u4309,negated_conjecture,
    true = unisex(skc8,skc15) ).

cnf(u2942,negated_conjecture,
    true = thing(skc11,skc12) ).

cnf(u229,negated_conjecture,
    true = ifeq2(smoke(skc8,skc12),true,true,true) ).

cnf(u4320,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc15),true) ).

cnf(u375,negated_conjecture,
    true = ifeq2(be(X0,skc9,skc14,skc14),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u4978,negated_conjecture,
    true = unisex(skc11,skc15) ).

cnf(u1121,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc9),true,true,true),true) ).

cnf(u484,negated_conjecture,
    true = ifeq2(true,true,eventuality(skc11,skc12),true) ).

cnf(u118,axiom,
    true = ifeq2(present(X0,X1),true,ifeq2(accessible_world(X0,X2),true,present(X2,X1),true),true) ).

cnf(u1506,negated_conjecture,
    true = relation(skc8,skc13) ).

cnf(u3315,negated_conjecture,
    true = ifeq2(true,true,thing(skc8,skc15),true) ).

cnf(u13,axiom,
    true = ifeq2(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).

cnf(u219,negated_conjecture,
    true = ifeq2(true,true,nonexistent(skc8,skc12),true) ).

cnf(u624,negated_conjecture,
    true = ifeq2(true,true,relname(skc11,skc13),true) ).

cnf(u503,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,event(X0,skc12),true) ).

cnf(u1778,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,relname(X0,skc15),true) ).

cnf(u513,negated_conjecture,
    true = ifeq2(true,true,event(skc11,skc9),true) ).

cnf(u268,negated_conjecture,
    true = ifeq2(true,true,ifeq2(unisex(skc8,X0),true,unisex(skc11,X0),true),true) ).

cnf(u4076,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(theme(skc11,X0,skc11),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,X0),true,skc11,skc11),skc11),skc11),skc11),skc11) ).

cnf(u246,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(state(X0,skc9),true,true,true),true) ).

cnf(u1290,negated_conjecture,
    true = unisex(skc8,skc12) ).

cnf(u1353,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc12),true,true,true),true) ).

cnf(u4074,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,skc11,skc11),skc11),skc11),skc11),skc11) ).

cnf(u1284,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc9),true) ).

cnf(ifeq_axiom_002,axiom,
    ifeq(X0,X0,X1,X2) = X1 ).

cnf(u287,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human_person(X0,skc14),true,true,true),true) ).

cnf(u258,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc12),true,true,true),true) ).

cnf(u1686,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(male(X0,skc14),true,true,true),true) ).

cnf(u244,negated_conjecture,
    true = ifeq2(true,true,ifeq2(state(skc8,X0),true,state(skc11,X0),true),true) ).

cnf(u3351,negated_conjecture,
    true = ifeq2(true,true,nonhuman(skc11,skc11),true) ).

cnf(u1817,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(relation(X0,skc11),true,true,true),true) ).

cnf(ifeq_axiom,axiom,
    ifeq3(X0,X0,X1,X2) = X1 ).

cnf(u5061,negated_conjecture,
    true = ifeq2(unisex(skc8,skf1(X0)),true,true,true) ).

cnf(u285,negated_conjecture,
    true = ifeq2(true,true,ifeq2(human_person(skc8,X0),true,human_person(skc11,X0),true),true) ).

cnf(u4390,negated_conjecture,
    true = ifeq2(entity(skc11,skc11),true,true,true) ).

cnf(u3069,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,living(X0,skc14),true) ).

cnf(u3124,negated_conjecture,
    skc15 = skc13 ).

cnf(u2324,negated_conjecture,
    true = agent(skc11,skf1(skc14),skc14) ).

cnf(u1161,negated_conjecture,
    skc13 = ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,skc14),true,X0,skc13),skc13),skc13) ).

cnf(u3355,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(abstraction(X0,skc11),true,true,true),true) ).

cnf(u158,negated_conjecture,
    true = man(skc8,skc10) ).

cnf(u3836,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11) ).

cnf(u1301,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc12),true) ).

cnf(u3255,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,relation(X0,skc15),true) ).

cnf(u2337,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(smoke(X0,skf1(X1)),true,true,true),true) ).

cnf(u43,axiom,
    true = ifeq2(forename(X0,X1),true,relname(X0,X1),true) ).

cnf(u275,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc12),true) ).

cnf(u1174,negated_conjecture,
    true = ifeq2(agent(X0,skc12,skc14),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u3375,negated_conjecture,
    true = ifeq2(true,true,singleton(skc8,skc11),true) ).

cnf(u4770,negated_conjecture,
    true = singleton(skc8,skc14) ).

cnf(u5128,negated_conjecture,
    true = singleton(skc11,skc14) ).

cnf(u2954,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,nonexistent(X0,skc12),true) ).

cnf(u3729,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(living(X0,skc14),true,true,true),true) ).

cnf(u2340,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,smoke(X0,skf1(X1)),true) ).

cnf(u1429,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc8,skc14)),tuple(true,true),a,b) ).

cnf(u2960,negated_conjecture,
    true = human(skc11,skc14) ).

cnf(u2727,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11) ).

cnf(u41,axiom,
    true = ifeq2(man(X0,X1),true,male(X0,X1),true) ).

cnf(u403,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc11),true,true,true),true) ).

cnf(u296,negated_conjecture,
    true = ifeq2(true,true,ifeq2(impartial(skc8,X0),true,impartial(skc11,X0),true),true) ).

cnf(u2359,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(theme(skc11,skf1(skc14),X2),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u3634,negated_conjecture,
    skc11 = ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X0),true,skc11,skc11),skc11) ).

cnf(u146,negated_conjecture,
    true = forename(skc8,skc13) ).

cnf(u3873,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(u47,axiom,
    true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).

cnf(u5325,negated_conjecture,
    true = ifeq2(singleton(skc8,skf1(X0)),true,true,true) ).

cnf(u3764,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,skc11,skc11),skc11) ).

cnf(u315,negated_conjecture,
    true = ifeq2(true,true,ifeq2(relation(skc8,X0),true,relation(skc11,X0),true),true) ).

cnf(u1214,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(agent(skc11,X0,X2),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u2713,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(agent(skc11,X0,X2),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).

cnf(u2357,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,agent(X0,skf1(skc14),skc14),true),true) ).

cnf(u96,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(human(X0,X2),true,human(X1,X2),true),true) ).

cnf(u953,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc8,X0,skc11),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(agent(skc8,X0,X1),true,ifeq3(think_believe_consider(skc8,X0),true,skc11,skc11),skc11),skc11),skc11),skc11) ).

cnf(u972,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(theme(skc8,skc12,X1),true,ifeq3(agent(skc8,X0,skc14),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).

cnf(u3768,negated_conjecture,
    true = entity(skc11,skc14) ).

cnf(u839,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,vincent_forename(X0,skc13),true) ).

cnf(u4136,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(abstraction(X0,skc15),true,true,true),true) ).

cnf(u313,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,forename(X0,skc15),true) ).

cnf(u2492,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,of(X0,skc15,skc14),true) ).

cnf(u443,negated_conjecture,
    true = ifeq2(true,true,forename(skc11,skc13),true) ).

cnf(u4899,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc15),true) ).

cnf(u430,negated_conjecture,
    ifeq3(theme(skc8,X0,X1),true,ifeq3(theme(skc8,skc12,X2),true,ifeq3(agent(skc8,X0,skc14),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u186,axiom,
    b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).

cnf(u4427,negated_conjecture,
    b = ifeq(tuple(human(skc11,skc11),true),tuple(true,true),a,b) ).

cnf(u4542,negated_conjecture,
    true = unisex(skc11,skc11) ).

cnf(u4220,negated_conjecture,
    b = ifeq(tuple(human(skc8,skc15),true),tuple(true,true),a,b) ).

cnf(u936,negated_conjecture,
    ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc14),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1) = X1 ).

cnf(u441,negated_conjecture,
    true = ifeq2(true,true,man(skc11,skc14),true) ).

cnf(u3396,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc11),true) ).

cnf(u597,negated_conjecture,
    true = ifeq2(male(skc8,X0),true,male(skc11,X0),true) ).

cnf(u184,axiom,
    b = ifeq(tuple(human(X0,X1),nonhuman(X0,X1)),tuple(true,true),a,b) ).

cnf(u1351,negated_conjecture,
    true = ifeq2(true,true,specific(skc11,skc12),true) ).

cnf(u1473,negated_conjecture,
    true = be(skc11,skc9,skc14,skc14) ).

cnf(u1613,negated_conjecture,
    true = human_person(skc11,skc14) ).

cnf(u1216,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,X2),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1),X1) = X1 ).

cnf(u1124,negated_conjecture,
    true = ifeq2(entity(skc8,skc9),true,true,true) ).

cnf(u494,negated_conjecture,
    true = ifeq2(nonexistent(skc8,X0),true,nonexistent(skc11,X0),true) ).

cnf(u342,negated_conjecture,
    true = ifeq2(present(X0,skc12),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u4787,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc14),true,true,true),true) ).

cnf(u1318,negated_conjecture,
    true = nonexistent(skc8,skc12) ).

cnf(u3420,negated_conjecture,
    b = ifeq(tuple(true,male(skc8,skc11)),tuple(true,true),a,b) ).

cnf(u1371,negated_conjecture,
    true = thing(skc8,skc12) ).

cnf(u4001,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc14),true,true,true),true) ).

cnf(u3413,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc11),true) ).

cnf(u340,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,present(X0,skc12),true),true) ).

cnf(u3424,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc11),true) ).

cnf(u599,negated_conjecture,
    true = ifeq2(true,true,male(skc11,skc14),true) ).

cnf(u4561,negated_conjecture,
    b = ifeq(tuple(true,male(skc11,skc11)),tuple(true,true),a,b) ).

cnf(u3926,negated_conjecture,
    true = specific(skc8,skc14) ).

cnf(u213,negated_conjecture,
    true = ifeq2(true,true,relname(skc8,skc13),true) ).

cnf(u359,negated_conjecture,
    true = ifeq2(of(X0,skc15,skc14),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u1634,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(human_person(X0,skc14),true,true,true),true) ).

cnf(u468,negated_conjecture,
    true = ifeq2(true,true,theme(skc11,skc12,skc11),true) ).

cnf(u102,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(forename(X0,X2),true,forename(X1,X2),true),true) ).

cnf(u3054,negated_conjecture,
    true = ifeq2(true,true,entity(skc11,skc14),true) ).

cnf(u2764,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).

cnf(u888,negated_conjecture,
    skc15 = ifeq3(of(skc8,skc15,X0),true,ifeq3(of(skc8,skc15,X0),true,ifeq3(entity(skc8,X0),true,skc15,skc15),skc15),skc15) ).

cnf(u357,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,of(X0,skc13,skc14),true),true) ).

cnf(u625,negated_conjecture,
    true = ifeq2(true,true,relname(skc11,skc15),true) ).

cnf(u230,negated_conjecture,
    true = ifeq2(smoke(skc8,skc9),true,true,true) ).

cnf(u1768,negated_conjecture,
    true = relname(skc11,skc15) ).

cnf(u4565,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc11),true) ).

cnf(u3065,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(living(X0,skc14),true,true,true),true) ).

cnf(u1548,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc11),true,true,true),true) ).

cnf(u4349,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,skc11,skc11),skc11),skc11),skc11) ).

cnf(u4342,negated_conjecture,
    true = thing(skc11,skc11) ).

cnf(u2304,negated_conjecture,
    true = event(skc11,skf1(X0)) ).

cnf(u485,negated_conjecture,
    true = ifeq2(true,true,eventuality(skc11,skc9),true) ).

cnf(u736,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,theme(X0,skc12,skc11),true) ).

cnf(u1145,negated_conjecture,
    skc15 = ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,skc14),true,X0,skc15),skc15),skc15) ).

cnf(u2923,negated_conjecture,
    true = unisex(skc11,skc12) ).

cnf(u4097,negated_conjecture,
    true = ifeq2(eventuality(skc8,skf1(X0)),true,true,true) ).

cnf(u3418,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc11),true,true,true),true) ).

cnf(u4132,negated_conjecture,
    true = ifeq2(true,true,nonhuman(skc11,skc15),true) ).

cnf(u436,negated_conjecture,
    ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,X2),true,ifeq3(agent(skc8,skc12,X2),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,skc11,X1),X1),X1),X1),X1) = X1 ).

cnf(u3860,negated_conjecture,
    true = ifeq2(abstraction(skc8,skc14),true,true,true) ).

cnf(u1524,negated_conjecture,
    skc13 = ifeq3(entity(skc8,skc14),true,skc15,skc13) ).

cnf(u269,negated_conjecture,
    true = ifeq2(true,true,ifeq2(event(skc8,X0),true,event(skc11,X0),true),true) ).

cnf(u5043,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,nonexistent(X0,skf1(X1)),true) ).

cnf(u399,negated_conjecture,
    ifeq3(true,true,ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,skc14),true,skc15,X0),X0),X0),X0) = X0 ).

cnf(u3053,negated_conjecture,
    true = ifeq2(true,true,impartial(skc11,skc14),true) ).

cnf(u3696,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u3108,negated_conjecture,
    true = ifeq2(true,true,existent(skc8,skc14),true) ).

cnf(u2938,negated_conjecture,
    true = nonexistent(skc11,skc12) ).

cnf(u1273,negated_conjecture,
    true = unisex(skc8,skc9) ).

cnf(u2692,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(u142,negated_conjecture,
    true = man(skc8,skc14) ).

cnf(u1259,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc9),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(u642,negated_conjecture,
    true = ifeq2(smoke(skc8,X0),true,smoke(skc11,X0),true) ).

cnf(u2321,negated_conjecture,
    true = ifeq2(accessible_world(skc11,skc11),true,true,true) ).

cnf(u27,axiom,
    true = ifeq2(entity(X0,X1),true,thing(X0,X1),true) ).

cnf(u259,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc12),true) ).

cnf(u2438,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,present(X0,skc12),true) ).

cnf(u4895,negated_conjecture,
    true = ifeq2(entity(skc11,skc15),true,true,true) ).

cnf(ifeq_axiom_001,axiom,
    ifeq2(X0,X0,X1,X2) = X1 ).

cnf(u140,negated_conjecture,
    true = forename(skc8,skc15) ).

cnf(u4892,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u1413,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,animate(X0,skc14),true) ).

cnf(u2944,negated_conjecture,
    true = singleton(skc8,skc12) ).

cnf(u25,axiom,
    true = ifeq2(organism(X0,X1),true,entity(X0,X1),true) ).

cnf(u2716,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11),skc11),skc11) ).

cnf(u5006,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skf1(X1)),true,true,true),true) ).

cnf(u4137,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,abstraction(X0,skc15),true) ).

cnf(u130,axiom,
    true = ifeq2(theme(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).

cnf(u5030,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skf1(X1)),true) ).

cnf(u539,negated_conjecture,
    true = ifeq2(true,true,present(skc11,skf1(X0)),true) ).

cnf(u3742,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(impartial(X0,skc14),true,true,true),true) ).

cnf(u2981,negated_conjecture,
    true = entity(skc8,skc14) ).

cnf(u31,axiom,
    true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).

cnf(u332,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,relname(X0,skc13),true) ).

cnf(u3201,negated_conjecture,
    true = vincent_forename(skc11,skc15) ).

cnf(u2877,negated_conjecture,
    ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,X1,skc14),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u3746,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,impartial(X0,skc14),true) ).

cnf(u1329,negated_conjecture,
    b = ifeq(tuple(true,existent(skc8,skc12)),tuple(true,true),a,b) ).

cnf(u4407,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11),skc11),skc11) ).

cnf(u4644,negated_conjecture,
    b = ifeq(tuple(true,general(skc11,skc14)),tuple(true,true),a,b) ).

cnf(u3125,negated_conjecture,
    ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,skc15,X0),X0) = X0 ).

cnf(u951,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(u2704,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0) = X0 ).

cnf(u3106,negated_conjecture,
    true = ifeq2(true,true,thing(skc8,skc14),true) ).

cnf(u297,negated_conjecture,
    true = ifeq2(true,true,ifeq2(living(skc8,X0),true,living(skc11,X0),true),true) ).

cnf(u564,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(forename(X0,skc13),true,true,true),true) ).

cnf(u170,negated_conjecture,
    true = be(skc8,skc9,skc14,skc10) ).

cnf(u4915,negated_conjecture,
    b = ifeq(tuple(human(skc11,skc15),true),tuple(true,true),a,b) ).

cnf(u4505,negated_conjecture,
    ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(theme(skc11,skf1(skc14),X1),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2475,negated_conjecture,
    true = ifeq2(entity(skc11,skc9),true,true,true) ).

cnf(u1443,negated_conjecture,
    true = ifeq2(true,true,entity(skc8,skc14),true) ).

cnf(u1597,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(event(X0,skc9),true,true,true),true) ).

cnf(u692,negated_conjecture,
    true = ifeq2(true,true,be(skc11,skc9,skc14,skc14),true) ).

cnf(u581,negated_conjecture,
    true = ifeq2(animate(skc8,X0),true,animate(skc11,X0),true) ).

cnf(u320,negated_conjecture,
    true = ifeq2(true,true,relation(skc8,skc15),true) ).

cnf(u168,negated_conjecture,
    true = theme(skc8,skc12,skc11) ).

cnf(u1463,negated_conjecture,
    true = ifeq2(true,true,relation(skc11,skc15),true) ).

cnf(u579,negated_conjecture,
    true = ifeq2(human(skc8,X0),true,human(skc11,X0),true) ).

cnf(u2988,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(thing(X0,skc12),true,true,true),true) ).

cnf(u4691,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc11,skc14),true),tuple(true,true),a,b) ).

cnf(u3007,negated_conjecture,
    true = thing(skc8,skc11) ).

cnf(u954,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(proposition(skc8,X0),true,X0,skc11),skc11),skc11),skc11),skc11) ).

cnf(u5141,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc14),true) ).

cnf(u1355,negated_conjecture,
    b = ifeq(tuple(true,general(skc8,skc12)),tuple(true,true),a,b) ).

cnf(u4897,negated_conjecture,
    true = ifeq2(eventuality(skc11,skc15),true,true,true) ).

cnf(u199,negated_conjecture,
    true = ifeq2(state(skc8,skc12),true,true,true) ).

cnf(u337,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(jules_forename(X0,skc15),true,true,true),true) ).

cnf(u604,negated_conjecture,
    true = ifeq2(forename(skc8,X0),true,forename(skc11,X0),true) ).

cnf(u4913,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonhuman(X0,skc15),true,true,true),true) ).

cnf(u324,negated_conjecture,
    true = relname(skc8,skc13) ).

cnf(u3408,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc11),true,true,true),true) ).

cnf(u3316,negated_conjecture,
    true = ifeq2(true,true,nonhuman(skc8,skc15),true) ).

cnf(u197,negated_conjecture,
    true = ifeq2(true,true,unisex(skc8,skc9),true) ).

cnf(u343,negated_conjecture,
    true = ifeq2(present(skc8,X0),true,present(skc11,X0),true) ).

cnf(u1618,negated_conjecture,
    skc11 = ifeq3(theme(skc8,skc12,X0),true,ifeq3(proposition(skc8,X0),true,X0,skc11),skc11) ).

cnf(u465,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,state(X0,skc9),true) ).

cnf(u86,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(organism(X0,X2),true,organism(X1,X2),true),true) ).

cnf(u711,negated_conjecture,
    true = ifeq2(present(X0,skc12),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u4689,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(existent(X0,skc14),true,true,true),true) ).

cnf(u2395,negated_conjecture,
    true = ifeq2(true,true,singleton(skc11,skc9),true) ).

cnf(u3038,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(human(X0,skc14),true,true,true),true) ).

cnf(u592,negated_conjecture,
    skc15 = ifeq3(of(skc11,X0,X1),true,ifeq3(of(skc11,skc15,X1),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,X1),true,X0,skc15),skc15),skc15),skc15) ).

cnf(u471,negated_conjecture,
    true = ifeq2(state(skc8,X0),true,state(skc11,X0),true) ).

cnf(u364,negated_conjecture,
    true = ifeq2(agent(X0,skc12,skc14),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u3179,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,vincent_forename(X0,skc15),true) ).

cnf(u1217,negated_conjecture,
    true = specific(skc8,skc9) ).

cnf(u214,negated_conjecture,
    true = eventuality(skc8,skc12) ).

cnf(u1125,negated_conjecture,
    true = ifeq2(true,true,singleton(skc8,skc9),true) ).

cnf(u3858,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc14),true,true,true),true) ).

cnf(u1380,negated_conjecture,
    true = ifeq2(true,true,singleton(skc8,skc12),true) ).

cnf(u152,negated_conjecture,
    true = event(skc8,skc12) ).

cnf(u2904,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,nonexistent(X0,skc9),true) ).

cnf(u3687,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc12),true) ).

cnf(u354,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(vincent_forename(X0,skc13),true,true,true),true) ).

cnf(u1129,negated_conjecture,
    true = ifeq2(true,true,thing(skc11,skc9),true) ).

cnf(u492,negated_conjecture,
    true = event(skc11,skc12) ).

cnf(u126,axiom,
    true = ifeq2(of(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).

cnf(u212,negated_conjecture,
    true = ifeq2(true,true,relname(skc8,skc15),true) ).

cnf(u2474,negated_conjecture,
    true = ifeq2(abstraction(skc11,skc9),true,true,true) ).

cnf(u870,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(u4461,negated_conjecture,
    ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0) = X0 ).

cnf(u751,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(theme(skc11,skc12,X2),true,ifeq3(agent(skc11,X0,X3),true,ifeq3(agent(skc11,skc12,X3),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4094,negated_conjecture,
    true = eventuality(skc11,skf1(X0)) ).

cnf(u1142,negated_conjecture,
    ifeq3(true,true,ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,skc14),true,skc15,X0),X0),X0),X0) = X0 ).

cnf(u632,negated_conjecture,
    true = ifeq2(nonhuman(skc8,X0),true,nonhuman(skc11,X0),true) ).

cnf(u4610,negated_conjecture,
    true = ifeq2(abstraction(skc11,skc14),true,true,true) ).

cnf(u3853,negated_conjecture,
    true = thing(skc8,skc14) ).

cnf(u1257,negated_conjecture,
    true = ifeq2(true,true,nonexistent(skc11,skc9),true) ).

cnf(u124,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(vincent_forename(X0,X2),true,vincent_forename(X1,X2),true),true) ).

cnf(u254,negated_conjecture,
    true = ifeq2(true,true,ifeq2(eventuality(skc8,X0),true,eventuality(skc11,X0),true),true) ).

cnf(u2693,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0) = X0 ).

cnf(u1397,negated_conjecture,
    true = animate(skc8,skc14) ).

cnf(u2928,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc12),true,true,true),true) ).

cnf(u5008,negated_conjecture,
    true = ifeq2(abstraction(skc11,skf1(X0)),true,true,true) ).

cnf(u2572,negated_conjecture,
    ifeq3(of(skc11,X0,skc14),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,skc14),true,skc15,X0),X0),X0) = X0 ).

cnf(u11,axiom,
    true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).

cnf(u5174,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,singleton(X0,skc15),true) ).

cnf(u114,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(jules_forename(X0,X2),true,jules_forename(X1,X2),true),true) ).

cnf(u2308,negated_conjecture,
    true = smoke(skc11,skf1(X0)) ).

cnf(u4549,negated_conjecture,
    b = ifeq(tuple(specific(skc11,skc11),true),tuple(true,true),a,b) ).

cnf(u2694,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1) = X1 ).

cnf(u1023,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(theme(skc8,X1,skc11),true,ifeq3(agent(skc8,skc12,X2),true,ifeq3(agent(skc8,X1,X2),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X0),true,skc11,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u4316,negated_conjecture,
    b = ifeq(tuple(true,male(skc8,skc15)),tuple(true,true),a,b) ).

cnf(u9,axiom,
    true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).

cnf(u264,negated_conjecture,
    true = ifeq2(true,true,ifeq2(specific(skc8,X0),true,specific(skc11,X0),true),true) ).

cnf(u242,negated_conjecture,
    true = human_person(skc8,skc14) ).

cnf(u3350,negated_conjecture,
    true = ifeq2(true,true,thing(skc11,skc11),true) ).

cnf(u15,axiom,
    true = ifeq2(eventuality(X0,X1),true,unisex(X0,X1),true) ).

cnf(u4106,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(eventuality(X0,skf1(X1)),true,true,true),true) ).

cnf(u283,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,man(X0,skc14),true) ).

cnf(u5022,negated_conjecture,
    true = ifeq2(specific(skc8,skf1(X0)),true,true,true) ).

cnf(u1175,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,agent(X0,skc12,skc14),true),true) ).

cnf(u2328,negated_conjecture,
    true = ifeq2(present(skc8,skf1(X0)),true,true,true) ).

cnf(u1545,negated_conjecture,
    true = ifeq2(true,true,general(skc8,skc11),true) ).

cnf(u1437,negated_conjecture,
    true = ifeq2(true,true,organism(skc11,skc14),true) ).

cnf(u935,negated_conjecture,
    ifeq3(theme(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(proposition(skc8,X0),true,skc11,X0),X0),X0),X0) = X0 ).

cnf(u49,axiom,
    true = ifeq2(abstraction(X0,X1),true,thing(X0,X1),true) ).

cnf(u2705,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(agent(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u304,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,male(X0,skc14),true) ).

cnf(u398,negated_conjecture,
    ifeq3(true,true,ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,skc14),true,skc13,X0),X0),X0),X0) = X0 ).

cnf(u2719,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11) ).

cnf(u154,negated_conjecture,
    true = proposition(skc8,skc11) ).

cnf(u1441,negated_conjecture,
    true = ifeq2(true,true,living(skc8,skc14),true) ).

cnf(u1427,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human(X0,skc14),true,true,true),true) ).

cnf(u670,negated_conjecture,
    true = jules_forename(skc11,skc15) ).

cnf(u1184,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(theme(skc11,skc12,X2),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,ifeq3(proposition(skc11,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u55,axiom,
    true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).

cnf(u409,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc11),true) ).

cnf(u310,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(forename(X0,skc15),true,true,true),true) ).

cnf(u2966,negated_conjecture,
    true = impartial(skc8,skc14) ).

cnf(u1568,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(eventuality(X0,skc12),true,true,true),true) ).

cnf(u1446,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,organism(X0,skc14),true) ).

cnf(u505,negated_conjecture,
    true = ifeq2(unisex(skc8,X0),true,unisex(skc11,X0),true) ).

cnf(u4668,negated_conjecture,
    true = existent(skc11,skc14) ).

cnf(u53,axiom,
    true = ifeq2(abstraction(X0,X1),true,general(X0,X1),true) ).

cnf(u816,negated_conjecture,
    ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,skc14),true,skc13,X0),X0),X0) = X0 ).

cnf(u1599,negated_conjecture,
    true = ifeq2(smoke(skc11,skc9),true,true,true) ).

cnf(u351,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,proposition(X0,skc11),true) ).

cnf(u2977,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,specific(X0,skc12),true) ).

cnf(u438,negated_conjecture,
    true = ifeq2(accessible_world(skc8,skc8),true,true,true) ).

cnf(u5024,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(specific(X0,skf1(X1)),true,true,true),true) ).

cnf(u567,negated_conjecture,
    skc13 = ifeq3(of(skc11,X0,X1),true,ifeq3(of(skc11,skc13,X1),true,ifeq3(forename(skc11,X0),true,ifeq3(entity(skc11,X1),true,X0,skc13),skc13),skc13),skc13) ).

cnf(u1544,negated_conjecture,
    true = ifeq2(true,true,nonhuman(skc8,skc11),true) ).

cnf(u944,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(agent(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u1727,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(agent(skc8,X0,skc14),true,ifeq3(think_believe_consider(skc8,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u4918,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,nonhuman(X0,skc15),true) ).

cnf(u4694,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,existent(X0,skc14),true) ).

cnf(u3252,negated_conjecture,
    true = ifeq2(true,true,abstraction(skc11,skc15),true) ).

cnf(u1851,negated_conjecture,
    skc11 = ifeq3(theme(skc8,skc12,X0),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(proposition(skc8,X0),true,X0,skc11),skc11),skc11),skc11) ).

cnf(u4165,negated_conjecture,
    true = thing(skc8,skc15) ).

cnf(clause35,axiom,
    ifeq3(be(X0,X1,X2,X3),true,X2,X3) = X3 ).

cnf(u1359,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc12),true) ).

cnf(u695,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,of(X0,skc15,skc14),true) ).

cnf(u5165,negated_conjecture,
    true = singleton(skc11,skc15) ).

cnf(u3513,negated_conjecture,
    true = singleton(skc11,skc9) ).

cnf(u2894,negated_conjecture,
    true = nonexistent(skc11,skc9) ).

cnf(u2749,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u327,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relname(X0,skc13),true,true,true),true) ).

cnf(u449,negated_conjecture,
    true = ifeq2(true,true,present(skc11,skc12),true) ).

cnf(u70,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(thing(X0,X2),true,thing(X1,X2),true),true) ).

cnf(u192,negated_conjecture,
    true = ifeq2(true,true,thing(skc8,skc9),true) ).

cnf(u502,negated_conjecture,
    true = ifeq2(state(skc11,skc12),true,true,true) ).

cnf(u4182,negated_conjecture,
    true = ifeq2(eventuality(skc8,skc15),true,true,true) ).

cnf(u4304,negated_conjecture,
    b = ifeq(tuple(specific(skc8,skc15),true),tuple(true,true),a,b) ).

cnf(u2919,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc9),true) ).

cnf(u455,negated_conjecture,
    true = ifeq2(true,true,vincent_forename(skc11,skc13),true) ).

cnf(u593,negated_conjecture,
    ifeq3(of(skc11,skc15,X0),true,ifeq3(of(skc11,X1,X0),true,ifeq3(forename(skc11,X1),true,ifeq3(entity(skc11,X0),true,skc15,X1),X1),X1),X1) = X1 ).

cnf(u348,negated_conjecture,
    true = ifeq2(true,true,ifeq2(proposition(skc8,X0),true,proposition(skc11,X0),true),true) ).

cnf(u68,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).

cnf(u2737,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,X1,skc14),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0) = X0 ).

cnf(u198,negated_conjecture,
    true = ifeq2(true,true,event(skc8,skc9),true) ).

cnf(u1109,negated_conjecture,
    true = thing(skc8,skc9) ).

cnf(u3033,negated_conjecture,
    true = unisex(skc8,skc11) ).

cnf(u685,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,jules_forename(X0,skc15),true) ).

cnf(u4180,negated_conjecture,
    true = ifeq2(entity(skc8,skc15),true,true,true) ).

cnf(u1494,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,be(X0,skc9,skc14,skc14),true),true) ).

cnf(u221,negated_conjecture,
    true = ifeq2(true,true,thing(skc8,skc12),true) ).

cnf(u453,negated_conjecture,
    true = ifeq2(true,true,proposition(skc11,skc11),true) ).

cnf(u338,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,jules_forename(X0,skc15),true) ).

cnf(u1113,negated_conjecture,
    true = of(skc11,skc13,skc14) ).

cnf(u2660,negated_conjecture,
    skc15 = ifeq3(of(skc11,skc15,X0),true,ifeq3(of(skc11,skc15,X0),true,ifeq3(entity(skc11,X0),true,skc15,skc15),skc15),skc15) ).

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 = ifeq2(true,true,nonexistent(skc8,skc9),true) ).

cnf(u365,negated_conjecture,
    true = ifeq2(agent(skc8,X0,X1),true,agent(skc11,X0,X1),true) ).

cnf(u4107,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,eventuality(X0,skf1(X1)),true) ).

cnf(u3016,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc12),true) ).

cnf(u108,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).

cnf(u238,negated_conjecture,
    skc14 = skc10 ).

cnf(u3788,negated_conjecture,
    true = ifeq2(true,true,existent(skc11,skc14),true) ).

cnf(u3960,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(theme(skc11,skc12,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11),skc11) ).

cnf(u4578,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc11),true) ).

cnf(u4960,negated_conjecture,
    true = general(skc11,skc15) ).

cnf(u5327,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skf1(X1)),true,true,true),true) ).

cnf(u3786,negated_conjecture,
    true = ifeq2(true,true,thing(skc11,skc14),true) ).

cnf(u4100,negated_conjecture,
    true = ifeq2(true,true,thing(skc11,skf1(X0)),true) ).

cnf(u355,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,vincent_forename(X0,skc13),true) ).

cnf(u4991,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u378,negated_conjecture,
    true = relation(skc8,skc11) ).

cnf(u3792,negated_conjecture,
    ifeq3(of(skc11,X0,skc14),true,ifeq3(of(skc11,X1,skc14),true,ifeq3(forename(skc11,X0),true,ifeq3(forename(skc11,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u98,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(animate(X0,X2),true,animate(X1,X2),true),true) ).

cnf(u4302,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc15),true,true,true),true) ).

cnf(u1280,negated_conjecture,
    b = ifeq(tuple(true,male(skc8,skc9)),tuple(true,true),a,b) ).

cnf(u4307,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc15),true) ).

cnf(u1128,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc9),true) ).

cnf(u1532,negated_conjecture,
    true = ifeq2(true,true,abstraction(skc8,skc13),true) ).

cnf(u251,negated_conjecture,
    true = ifeq2(true,true,organism(skc8,skc14),true) ).

cnf(u637,negated_conjecture,
    true = ifeq2(jules_forename(skc8,X0),true,jules_forename(skc11,X0),true) ).

cnf(u376,negated_conjecture,
    true = ifeq2(be(skc8,X0,X1,X2),true,be(skc11,X0,X1,X2),true) ).

cnf(u2311,negated_conjecture,
    true = ifeq2(man(skc11,X0),true,true,true) ).

cnf(u777,negated_conjecture,
    skc13 = ifeq3(true,true,ifeq3(entity(skc8,skc14),true,skc13,skc13),skc13) ).

cnf(u226,negated_conjecture,
    true = ifeq2(jules_forename(skc8,skc13),true,true,true) ).

cnf(u2793,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2949,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(nonexistent(X0,skc12),true,true,true),true) ).

cnf(u791,negated_conjecture,
    skc15 = ifeq3(true,true,ifeq3(entity(skc8,skc14),true,skc13,skc15),skc15) ).

cnf(u249,negated_conjecture,
    true = ifeq2(true,true,animate(skc8,skc14),true) ).

cnf(u267,negated_conjecture,
    true = ifeq2(true,true,ifeq2(nonexistent(skc8,X0),true,nonexistent(skc11,X0),true),true) ).

cnf(u748,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc12),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u765,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,be(X0,skc9,skc14,skc14),true) ).

cnf(u1297,negated_conjecture,
    b = ifeq(tuple(true,male(skc8,skc12)),tuple(true,true),a,b) ).

cnf(u5036,negated_conjecture,
    true = ifeq2(nonexistent(skc8,skf1(X0)),true,true,true) ).

cnf(u4612,negated_conjecture,
    true = ifeq2(true,true,singleton(skc11,skc14),true) ).

cnf(u4629,negated_conjecture,
    true = specific(skc11,skc14) ).

cnf(u2335,negated_conjecture,
    true = ifeq2(smoke(skc8,skf1(X0)),true,true,true) ).

cnf(u2962,negated_conjecture,
    true = organism(skc11,skc14) ).

cnf(u33,axiom,
    true = ifeq2(organism(X0,X1),true,impartial(X0,X1),true) ).

cnf(u1543,negated_conjecture,
    true = ifeq2(true,true,thing(skc8,skc11),true) ).

cnf(u3074,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(impartial(X0,skc14),true,true,true),true) ).

cnf(u265,negated_conjecture,
    true = male(skc8,skc14) ).

cnf(u532,negated_conjecture,
    true = ifeq2(human_person(skc8,X0),true,human_person(skc11,X0),true) ).

cnf(u288,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,human_person(X0,skc14),true) ).

cnf(u510,negated_conjecture,
    true = ifeq2(event(skc8,X0),true,event(skc11,X0),true) ).

cnf(u781,negated_conjecture,
    true = proposition(skc11,skc11) ).

cnf(u4119,negated_conjecture,
    true = abstraction(skc11,skc15) ).

cnf(u138,negated_conjecture,
    true = jules_forename(skc8,skc15) ).

cnf(u1425,negated_conjecture,
    true = ifeq2(true,true,human(skc11,skc14),true) ).

cnf(u547,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,man(X0,skc14),true) ).

cnf(u250,negated_conjecture,
    true = ifeq2(true,true,human(skc8,skc14),true) ).

cnf(u3352,negated_conjecture,
    true = ifeq2(true,true,general(skc11,skc11),true) ).

cnf(u39,axiom,
    true = ifeq2(human_person(X0,X1),true,animate(X0,X1),true) ).

cnf(u2951,negated_conjecture,
    b = ifeq(tuple(true,existent(skc11,skc12)),tuple(true,true),a,b) ).

cnf(u1546,negated_conjecture,
    true = ifeq2(true,true,unisex(skc8,skc11),true) ).

cnf(u1832,negated_conjecture,
    skc11 = ifeq3(theme(skc8,X0,skc11),true,ifeq3(agent(skc8,skc12,X1),true,ifeq3(agent(skc8,X0,X1),true,ifeq3(think_believe_consider(skc8,X0),true,skc11,skc11),skc11),skc11),skc11) ).

cnf(u3895,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skc12,X0),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(agent(skc11,skc12,X1),true,ifeq3(proposition(skc11,X0),true,X0,skc11),skc11),skc11),skc11) ).

cnf(u136,negated_conjecture,
    true = actual_world(skc8) ).

cnf(u2450,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,think_believe_consider(X0,skc12),true) ).

cnf(u1569,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,eventuality(X0,skc12),true) ).

cnf(u4003,negated_conjecture,
    b = ifeq(tuple(true,general(skc8,skc14)),tuple(true,true),a,b) ).

cnf(u37,axiom,
    true = ifeq2(human_person(X0,X1),true,human(X0,X1),true) ).

cnf(u305,negated_conjecture,
    true = relname(skc8,skc15) ).

cnf(u537,negated_conjecture,
    true = ifeq2(true,true,agent(skc11,skf1(skc14),skc14),true) ).

cnf(u1691,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,male(X0,skc14),true) ).

cnf(u3376,negated_conjecture,
    true = ifeq2(eventuality(skc8,skc11),true,true,true) ).

cnf(u4872,negated_conjecture,
    true = thing(skc11,skc15) ).

cnf(u4134,negated_conjecture,
    true = ifeq2(true,true,unisex(skc11,skc15),true) ).

cnf(u2605,negated_conjecture,
    true = specific(skc11,skc9) ).

cnf(u3112,negated_conjecture,
    ifeq3(of(skc8,X0,skc14),true,ifeq3(of(skc8,X1,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(forename(skc8,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u311,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(forename(X0,skc13),true,true,true),true) ).

cnf(u1586,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(eventuality(X0,skc9),true,true,true),true) ).

cnf(u2528,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,theme(X0,skc12,skc11),true) ).

cnf(u665,negated_conjecture,
    true = ifeq2(proposition(skc8,X0),true,proposition(skc11,X0),true) ).

cnf(u420,negated_conjecture,
    ifeq3(theme(skc8,X0,X1),true,ifeq3(theme(skc8,skc12,X2),true,ifeq3(agent(skc8,X0,X3),true,ifeq3(agent(skc8,skc12,X3),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u176,negated_conjecture,
    true = ifeq2(man(skc11,X0),true,event(skc11,skf1(X1)),true) ).

cnf(u1471,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc15),true) ).

cnf(u554,negated_conjecture,
    true = ifeq2(entity(skc8,X0),true,entity(skc11,X0),true) ).

cnf(u3251,negated_conjecture,
    true = ifeq2(proposition(skc11,skc15),true,true,true) ).

cnf(u439,negated_conjecture,
    true = ifeq2(true,true,event(skc11,skc12),true) ).

cnf(u4223,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc15),true) ).

cnf(u1603,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,event(X0,skc9),true) ).

cnf(u182,axiom,
    b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).

cnf(u682,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(jules_forename(X0,skc15),true,true,true),true) ).

cnf(u4540,negated_conjecture,
    true = general(skc11,skc11) ).

cnf(u82,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(man(X0,X2),true,man(X1,X2),true),true) ).

cnf(u1709,negated_conjecture,
    true = relname(skc11,skc13) ).

cnf(u4009,negated_conjecture,
    true = existent(skc8,skc14) ).

cnf(u437,negated_conjecture,
    true = ifeq2(true,true,state(skc11,skc9),true) ).

cnf(u2848,negated_conjecture,
    skc11 = ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(theme(skc11,X0,X1),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u577,negated_conjecture,
    true = forename(skc11,skc15) ).

cnf(u3012,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc12),true,true,true),true) ).

cnf(u180,axiom,
    b = ifeq(tuple(unisex(X0,X1),male(X0,X1)),tuple(true,true),a,b) ).

cnf(u2875,negated_conjecture,
    ifeq3(theme(skc11,X0,X1),true,ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(agent(skc11,X0,skc14),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X1),true,skc11,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u962,negated_conjecture,
    skc11 = ifeq3(true,true,ifeq3(theme(skc8,skc12,X0),true,ifeq3(proposition(skc8,X0),true,X0,skc11),skc11),skc11) ).

cnf(u5170,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

cnf(u4430,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,nonhuman(X0,skc11),true) ).

cnf(u1348,negated_conjecture,
    true = specific(skc8,skc12) ).

cnf(u2384,negated_conjecture,
    true = singleton(skc8,skc9) ).

cnf(u589,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(forename(X0,skc15),true,true,true),true) ).

cnf(u3005,negated_conjecture,
    true = abstraction(skc11,skc11) ).

cnf(u705,negated_conjecture,
    true = present(skc11,skc12) ).

cnf(u94,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(living(X0,X2),true,living(X1,X2),true),true) ).

cnf(u1221,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc9),true,true,true),true) ).

cnf(u4559,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skc11),true,true,true),true) ).

cnf(u594,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,forename(X0,skc15),true) ).

cnf(u195,negated_conjecture,
    true = ifeq2(true,true,specific(skc8,skc9),true) ).

cnf(u2766,negated_conjecture,
    ifeq3(theme(skc11,skf1(skc14),X0),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u1325,negated_conjecture,
    true = ifeq2(true,true,nonexistent(skc11,skc12),true) ).

cnf(u3938,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,skf1(skc14),skc11),true,ifeq3(think_believe_consider(skc11,skf1(skc14)),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0) = X0 ).

cnf(u5063,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(unisex(X0,skf1(X1)),true,true,true),true) ).

cnf(u450,negated_conjecture,
    true = ifeq2(true,true,think_believe_consider(skc11,skc12),true) ).

cnf(u849,negated_conjecture,
    ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,skc14),true,skc15,X0),X0),X0) = X0 ).

cnf(u92,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(impartial(X0,X2),true,impartial(X1,X2),true),true) ).

cnf(u4187,negated_conjecture,
    true = nonhuman(skc8,skc15) ).

cnf(u5318,negated_conjecture,
    true = singleton(skc11,skf1(X0)) ).

cnf(u2401,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc9),true) ).

cnf(u401,negated_conjecture,
    skc15 = ifeq3(of(skc8,X0,skc14),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,skc14),true,X0,skc15),skc15),skc15) ).

cnf(u339,negated_conjecture,
    true = ifeq2(true,true,ifeq2(smoke(skc8,X0),true,smoke(skc11,X0),true),true) ).

cnf(u362,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,agent(X0,skc12,skc14),true),true) ).

cnf(u5040,negated_conjecture,
    b = ifeq(tuple(true,existent(skc11,skf1(X0))),tuple(true,true),a,b) ).

cnf(u3018,negated_conjecture,
    true = nonhuman(skc8,skc11) ).

cnf(u3793,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,entity(X0,skc14),true) ).

cnf(u220,negated_conjecture,
    true = ifeq2(true,true,specific(skc8,skc12),true) ).

cnf(u1123,negated_conjecture,
    true = ifeq2(abstraction(skc8,skc9),true,true,true) ).

cnf(u1261,negated_conjecture,
    b = ifeq(tuple(true,existent(skc8,skc9)),tuple(true,true),a,b) ).

cnf(u4547,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(general(X0,skc11),true,true,true),true) ).

cnf(u4997,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc15),true) ).

cnf(u1493,negated_conjecture,
    true = ifeq2(be(X0,skc9,skc14,skc14),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u2931,negated_conjecture,
    true = ifeq2(abstraction(skc11,skc12),true,true,true) ).

cnf(u467,negated_conjecture,
    true = ifeq2(true,true,agent(skc11,skc12,skc14),true) ).

cnf(u360,negated_conjecture,
    true = ifeq2(of(X0,skc13,skc14),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u490,negated_conjecture,
    true = ifeq2(specific(skc8,X0),true,specific(skc11,X0),true) ).

cnf(u210,negated_conjecture,
    true = ifeq2(true,true,male(skc8,skc14),true) ).

cnf(u5092,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc11),true,ifeq2(singleton(X0,skc11),true,true,true),true) ).

cnf(u634,negated_conjecture,
    true = ifeq2(general(skc8,X0),true,general(skc11,X0),true) ).

cnf(u2791,negated_conjecture,
    ifeq3(theme(skc11,skc12,X0),true,ifeq3(theme(skc11,X1,skc11),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(agent(skc11,X1,X2),true,ifeq3(think_believe_consider(skc11,X1),true,ifeq3(proposition(skc11,X0),true,skc11,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u233,negated_conjecture,
    true = ifeq2(vincent_forename(skc8,skc15),true,true,true) ).

cnf(u1278,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc9),true,true,true),true) ).

cnf(u366,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,theme(X0,skc12,skc11),true),true) ).

cnf(u749,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc11,X0),true,think_believe_consider(X0,skc12),true),true) ).

cnf(u488,negated_conjecture,
    true = ifeq2(singleton(skc8,X0),true,singleton(skc11,X0),true) ).

cnf(u2551,negated_conjecture,
    skc15 = ifeq3(true,true,ifeq3(entity(skc11,skc14),true,skc15,skc15),skc15) ).

cnf(u122,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(proposition(X0,X2),true,proposition(X1,X2),true),true) ).

cnf(u1641,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,human_person(X0,skc14),true) ).

cnf(u2319,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,event(X0,skf1(X1)),true) ).

cnf(u4131,negated_conjecture,
    true = ifeq2(true,true,thing(skc11,skc15),true) ).

cnf(u5001,negated_conjecture,
    true = nonexistent(skc11,skf1(X0)) ).

cnf(u239,negated_conjecture,
    true = be(skc8,skc9,skc14,skc14) ).

cnf(u4133,negated_conjecture,
    true = ifeq2(true,true,general(skc11,skc15),true) ).

cnf(u377,negated_conjecture,
    true = ifeq2(true,true,ifeq2(accessible_world(skc8,X0),true,be(X0,skc9,skc14,skc14),true),true) ).

cnf(u1276,negated_conjecture,
    true = ifeq2(true,true,unisex(skc11,skc9),true) ).

cnf(u5014,negated_conjecture,
    true = unisex(skc11,skf1(X0)) ).

cnf(u272,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc12),true,true,true),true) ).

cnf(u2934,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,unisex(X0,skc12),true) ).

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(u2306,negated_conjecture,
    true = present(skc11,skf1(X0)) ).

cnf(u1409,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(animate(X0,skc14),true,true,true),true) ).

cnf(u1812,negated_conjecture,
    true = relation(skc11,skc11) ).

cnf(u2940,negated_conjecture,
    true = specific(skc11,skc12) ).

cnf(u3078,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,impartial(X0,skc14),true) ).

cnf(u2317,negated_conjecture,
    true = ifeq2(true,true,eventuality(skc11,skf1(X0)),true) ).

cnf(u1152,negated_conjecture,
    true = ifeq2(of(X0,skc13,skc14),true,ifeq2(accessible_world(X0,skc11),true,true,true),true) ).

cnf(u23,axiom,
    true = ifeq2(human_person(X0,X1),true,organism(X0,X1),true) ).

cnf(u3865,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc14),true) ).

cnf(u2817,negated_conjecture,
    skc11 = ifeq3(theme(skc11,X0,skc11),true,ifeq3(theme(skc11,skc12,X1),true,ifeq3(agent(skc11,X0,X2),true,ifeq3(agent(skc11,skc12,X2),true,ifeq3(think_believe_consider(skc11,X0),true,ifeq3(proposition(skc11,X1),true,X1,skc11),skc11),skc11),skc11),skc11),skc11) ).

cnf(u4391,negated_conjecture,
    true = ifeq2(true,true,singleton(skc11,skc11),true) ).

cnf(u2995,negated_conjecture,
    true = ifeq2(accessible_world(skc11,X0),true,thing(X0,skc12),true) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP225-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39  % Computer : n014.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:32:17 UTC 2026
% 0.10/0.39  % CPUTime  : 
% 0.10/0.39  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.44  Running first-order model finding
% 0.10/0.44  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
% 1.31/0.68  % (1088788)Will run a generic schedule for satisfiability detection.
% 1.31/0.68  % (1088794)% WARNING: option uhcvi not known.
% 1.31/0.68  % (1088794)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3598804611:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.31/0.68  % (1088799)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3907851930:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.31/0.68  % (1088793)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1576541546_2999 on theBenchmark for (2999ds/0Mi)
% 1.31/0.68  % (1088796)dis+10_1_sil=32000:sp=arity:random_seed=1733472219:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.31/0.68  % (1088797)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=613010156:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.31/0.68  % (1088798)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2655904543:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.31/0.68  % (1088795)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2170290497:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.31/0.68  % TRYING [1]
% 1.31/0.68  % TRYING [2]
% 1.31/0.68  % TRYING [3]
% 1.31/0.68  % (1088796)Instruction limit reached! 
% 1.31/0.68  % (1088796)------------------------------
% 1.31/0.68  % (1088796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.68  % (1088796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.68  % (1088796)CaDiCaL version: 2.1.3
% 1.31/0.68  % (1088796)Termination reason: Instruction limit
% 1.31/0.68  % (1088796)Termination phase: Saturation
% 1.31/0.68  % (1088796)Time elapsed: 0.103 s
% 1.31/0.68  % (1088796)Peak memory usage: 12 MB
% 1.31/0.68  % (1088796)Instructions burned: 103 (million)
% 1.31/0.68  % (1088797)Instruction limit reached! 
% 1.31/0.68  % (1088797)------------------------------
% 1.31/0.68  % (1088797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.68  % (1088797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.68  % (1088797)CaDiCaL version: 2.1.3
% 1.31/0.68  % (1088797)Termination reason: Instruction limit
% 1.31/0.68  % (1088797)Termination phase: Saturation
% 1.31/0.68  % (1088797)Time elapsed: 0.107 s
% 1.31/0.68  % (1088797)Peak memory usage: 13 MB
% 1.31/0.68  % (1088797)Instructions burned: 116 (million)
% 1.31/0.68  % (1088798)Instruction limit reached! 
% 1.31/0.68  % (1088798)------------------------------
% 1.31/0.68  % (1088798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.68  % (1088798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.68  % (1088811)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2368702008:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.31/0.68  % (1088798)CaDiCaL version: 2.1.3
% 1.31/0.68  % (1088798)Termination reason: Instruction limit
% 1.31/0.68  % (1088798)Termination phase: Saturation
% 1.31/0.68  % (1088798)Time elapsed: 0.127 s
% 1.31/0.68  % (1088798)Peak memory usage: 12 MB
% 1.31/0.68  % (1088798)Instructions burned: 131 (million)
% 1.31/0.68  % (1088810)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1000863511:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.31/0.68  % (1088799)Instruction limit reached! 
% 1.31/0.68  % (1088799)------------------------------
% 1.31/0.68  % (1088799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.68  % (1088799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.68  % (1088799)CaDiCaL version: 2.1.3
% 1.31/0.68  % (1088799)Termination reason: Instruction limit
% 1.31/0.68  % (1088799)Termination phase: Saturation
% 1.31/0.68  % (1088799)Time elapsed: 0.140 s
% 1.31/0.68  % (1088799)Peak memory usage: 12 MB
% 1.31/0.68  % (1088799)Instructions burned: 159 (million)
% 1.31/0.68  % (1088813)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4244445988:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.31/0.68  % (1088815)ott-21_1_sil=16000:fs=off:random_seed=3063982767:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.31/0.68  % TRYING [1]
% 1.31/0.68  % (1088794) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1088788-1088794"...
% 1.31/0.68  % TRYING [2]
% 1.31/0.68  % (1088794)...printing done.
% 1.31/0.68  % SZS status Satisfiable for theBenchmark
% 1.31/0.68  % SZS output start Saturation.
% See solution above
% 1.31/0.70  % SZS output start Definitions and Model Updates.
% 1.31/0.70  % SZS output end Definitions and Model Updates.
% 1.31/0.70  % (1088794)------------------------------
% 1.31/0.70  % (1088794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.31/0.70  % (1088794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.31/0.70  % (1088794)CaDiCaL version: 2.1.3
% 1.31/0.70  % (1088794)Termination reason: Satisfiable
% 1.31/0.70  % (1088794)Time elapsed: 0.199 s
% 1.31/0.70  % (1088794)Peak memory usage: 14 MB
% 1.31/0.70  % (1088794)Instructions burned: 369 (million)
% 1.31/0.70  % (1088788)Success in time 0.231 s
% 1.31/0.70  % Vampire exiting
%------------------------------------------------------------------------------