Vampire---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NLP247-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 12:08:11 PM UTC 2026

% Result   : Satisfiable 12.53s 2.68s
% Output   : Saturation 13.64s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u11239,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(theme(skc17,X1,skc17),true,ifeq3(agent(skc17,X1,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u918,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc20),true) ).

cnf(u1639,negated_conjecture,
    true = unisex(skc17,skc19) ).

cnf(u11069,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(theme(skc14,skc16,X2),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2903,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,man(X0,skc20),true) ).

cnf(u11953,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skf1(skc24),X1),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u10615,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X1),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1) = X1 ).

cnf(u1958,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,proposition(X0,skc17),true) ).

cnf(u631,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc19),true,true,true) ).

cnf(u4192,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(forename(X0,skc28),true,true,true),true) ).

cnf(u10845,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u322,negated_conjecture,
    true = sF32 ).

cnf(u996,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc26),true) ).

cnf(u722,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skc26),true) ).

cnf(u5150,negated_conjecture,
    ifeq3(of(skc17,X1,skc27),true,ifeq3(of(skc17,X0,skc27),true,ifeq3(forename(skc17,X1),true,ifeq3(forename(skc17,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u3184,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc17,skc27),true),tuple(true,true),a,b) ).

cnf(u4464,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc24),skc24),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u2169,negated_conjecture,
    true = ifeq2(proposition(skc17,skc23),true,true,true) ).

cnf(u8620,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(eventuality(X0,skc25),true,true,true),true) ).

cnf(u7943,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc23,skc20),true,skc19,skc23) ).

cnf(u2948,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(smoke(X1,skf1(X0)),true,true,true),true) ).

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

cnf(u4197,negated_conjecture,
    true = relname(skc17,skc28) ).

cnf(u10751,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u7896,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc28,skc20),true,skc28,skc19) ).

cnf(u11277,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(agent(skc17,X0,skc27),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u2161,negated_conjecture,
    true = relation(skc17,skc19) ).

cnf(u10776,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u745,negated_conjecture,
    true = eventuality(skc17,skc16) ).

cnf(u3047,negated_conjecture,
    true = agent(skc17,skf1(skc24),skc24) ).

cnf(u4423,negated_conjecture,
    true = jules_forename(skc17,skc28) ).

cnf(u2000,negated_conjecture,
    true = proposition(skc17,skc17) ).

cnf(u3087,negated_conjecture,
    true = existent(skc17,skc24) ).

cnf(u4354,negated_conjecture,
    true = vincent_forename(skc17,skc19) ).

cnf(u2975,negated_conjecture,
    true = specific(skc17,skf1(X0)) ).

cnf(u383,negated_conjecture,
    true = thing(skc14,skc16) ).

cnf(u11126,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(theme(skc14,skc18,X2),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u387,negated_conjecture,
    true = singleton(skc14,skc16) ).

cnf(u11493,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u8572,negated_conjecture,
    true = eventuality(skc17,skc25) ).

cnf(u11539,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u334,negated_conjecture,
    true = jules_forename(skc14,skc28) ).

cnf(u8228,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc23,skc20),true,ifeq3(of(skc14,skc28,skc20),true,skc23,skc28),skc28) ).

cnf(u2079,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relation(X0,skc19),true) ).

cnf(u2922,negated_conjecture,
    true = human(skc17,skc20) ).

cnf(u2581,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(general(X0,skc17),true,true,true),true) ).

cnf(u11236,negated_conjecture,
    ifeq3(theme(skc17,X0,X1),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u5684,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1) = X1 ).

cnf(u2395,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonhuman(X0,skc19),true) ).

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

cnf(u1333,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc28),true) ).

cnf(u8753,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc25),true) ).

cnf(u481,negated_conjecture,
    true = organism(skc14,skc24) ).

cnf(u3100,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(organism(X0,skc20),true,true,true),true) ).

cnf(u4804,negated_conjecture,
    true = of(skc17,skc28,skc27) ).

cnf(u4777,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,of(X0,skc23,skc24),true) ).

cnf(u1336,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc17),true) ).

cnf(u2173,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relation(X0,skc19),true,true,true),true) ).

cnf(u2177,negated_conjecture,
    true = ifeq2(proposition(skc17,skc19),true,true,true) ).

cnf(u9192,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,skc17),true,ifeq3(agent(skc14,X0,X1),true,ifeq3(agent(skc14,skc16,X1),true,ifeq3(think_believe_consider(skc14,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u11952,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skf1(skc27),X1),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u5648,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(agent(skc17,X2,skc20),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2971,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(eventuality(X1,skf1(X0)),true,true,true),true) ).

cnf(u4766,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,of(X0,skc28,skc27),true) ).

cnf(u598,negated_conjecture,
    true = general(skc14,skc23) ).

cnf(u1831,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc18),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

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

cnf(u1291,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc19),true,true,true) ).

cnf(u8206,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc28,X0),true,ifeq3(of(skc14,skc28,X0),true,ifeq3(entity(skc14,X0),true,skc28,skc28),skc28),skc28) ).

cnf(u9517,negated_conjecture,
    skc17 = ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc18,X0),true,skc17,skc17),skc17) ).

cnf(u8506,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc23,skc27),true,ifeq3(of(skc17,skc19,skc27),true,skc23,skc19),skc19) ).

cnf(u823,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,event(X0,skc18),true) ).

cnf(u11468,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u3549,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(impartial(X0,skc24),true,true,true),true) ).

cnf(u5654,negated_conjecture,
    ifeq3(theme(skc17,skc16,X2),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc20),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X0),true,X0,X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u1739,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,present(X0,skc18),true) ).

cnf(u8129,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc19,X0),true,ifeq3(of(skc14,skc19,X0),true,ifeq3(entity(skc14,X0),true,skc19,skc19),skc19),skc19) ).

cnf(u2936,negated_conjecture,
    true = entity(skc17,skc20) ).

cnf(u5584,negated_conjecture,
    ifeq3(theme(skc14,X3,X2),true,ifeq3(theme(skc14,skc16,X1),true,ifeq3(agent(skc14,X3,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(think_believe_consider(skc14,X3),true,ifeq3(proposition(skc14,X2),true,ifeq3(proposition(skc14,X1),true,X1,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u9540,negated_conjecture,
    ifeq3(of(skc17,skc23,skc27),true,ifeq3(of(skc17,X0,skc27),true,ifeq3(forename(skc17,X0),true,skc23,X0),X0),X0) = X0 ).

cnf(u5573,negated_conjecture,
    ifeq3(theme(skc14,X3,X2),true,ifeq3(theme(skc14,X1,skc17),true,ifeq3(agent(skc14,X3,X0),true,ifeq3(agent(skc14,X1,X0),true,ifeq3(think_believe_consider(skc14,X3),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X2),true,skc17,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u621,negated_conjecture,
    true = nonhuman(skc14,skc28) ).

cnf(u9990,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0) = X0 ).

cnf(u9993,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0) = X0 ).

cnf(u4762,negated_conjecture,
    true = ifeq2(of(skc14,X1,X0),true,of(skc17,X1,X0),true) ).

cnf(u1661,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc19),true,true,true),true) ).

cnf(u8580,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc25),true,true,true) ).

cnf(u10057,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,skc17,skc17),skc17),skc17) ).

cnf(u1000,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc25),true,true,true) ).

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

cnf(u691,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc14,skc20),true),tuple(true,true),a,b) ).

cnf(u8202,negated_conjecture,
    skc28 = ifeq3(of(skc14,X0,skc24),true,ifeq3(of(skc14,skc28,skc24),true,ifeq3(forename(skc14,X0),true,X0,skc28),skc28),skc28) ).

cnf(u3682,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(living(X0,skc24),true,true,true),true) ).

cnf(u9976,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u2223,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(abstraction(X0,skc28),true,true,true),true) ).

cnf(u819,negated_conjecture,
    true = ifeq2(state(skc17,skc18),true,true,true) ).

cnf(u3113,negated_conjecture,
    true = ifeq2(organism(skc14,X0),true,organism(skc17,X0),true) ).

cnf(u1497,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc28),true,true,true),true) ).

cnf(u1358,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc28),true,true,true),true) ).

cnf(u2952,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,smoke(X1,skf1(X0)),true) ).

cnf(u2880,negated_conjecture,
    true = ifeq2(man(skc14,X0),true,man(skc17,X0),true) ).

cnf(u2256,negated_conjecture,
    true = ifeq2(abstraction(skc14,X0),true,abstraction(skc17,X0),true) ).

cnf(u436,negated_conjecture,
    true = general(skc14,skc17) ).

cnf(u9624,negated_conjecture,
    ifeq3(of(skc17,skc28,skc24),true,ifeq3(of(skc17,X0,skc24),true,ifeq3(forename(skc17,X0),true,skc28,X0),X0),X0) = X0 ).

cnf(u1732,negated_conjecture,
    true = present(skc17,skc16) ).

cnf(u1348,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc20),true) ).

cnf(u990,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc26),true,true,true),true) ).

cnf(u2226,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(abstraction(X0,skc19),true,true,true),true) ).

cnf(u259,negated_conjecture,
    true = sF11 ).

cnf(u606,negated_conjecture,
    true = general(skc14,skc19) ).

cnf(u3134,negated_conjecture,
    true = male(skc17,skc27) ).

cnf(u2159,negated_conjecture,
    true = relation(skc17,skc23) ).

cnf(u2030,negated_conjecture,
    b = ifeq(tuple(specific(skc17,skc17),true),tuple(true,true),a,b) ).

cnf(u11835,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(theme(skc17,skc16,X2),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

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

cnf(u1299,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc20),true,true,true) ).

cnf(u707,negated_conjecture,
    true = ifeq2(smoke(skc14,skc25),true,true,true) ).

cnf(u1733,negated_conjecture,
    true = present(skc17,skc18) ).

cnf(u394,negated_conjecture,
    true = specific(skc14,skc18) ).

cnf(u3251,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,entity(X0,skc27),true) ).

cnf(u1853,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,think_believe_consider(X0,skc16),true) ).

cnf(u10100,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u4468,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,agent(X0,skf1(skc27),skc27),true) ).

cnf(u3969,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,animate(X0,skc24),true) ).

cnf(u8407,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc19,X0),true,ifeq3(of(skc17,skc23,X0),true,ifeq3(entity(skc17,X0),true,skc19,skc23),skc23),skc23) ).

cnf(u501,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc27),true,true,true) ).

cnf(u2901,negated_conjecture,
    true = human_person(skc17,skc20) ).

cnf(u5606,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X2),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc20),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u2268,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,abstraction(X0,skc28),true) ).

cnf(u432,negated_conjecture,
    true = nonhuman(skc14,skc17) ).

cnf(u5171,negated_conjecture,
    ifeq3(of(skc17,skc23,X1),true,ifeq3(of(skc17,X0,X1),true,ifeq3(forename(skc17,X0),true,ifeq3(entity(skc17,X1),true,skc23,X0),X0),X0),X0) = X0 ).

cnf(u11689,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u3827,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(human(X0,skc24),true,true,true),true) ).

cnf(u8480,negated_conjecture,
    skc19 = ifeq3(of(skc17,X0,skc27),true,ifeq3(of(skc17,skc19,skc27),true,ifeq3(forename(skc17,X0),true,X0,skc19),skc19),skc19) ).

cnf(u986,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc26),true,true,true) ).

cnf(u9433,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc28,X0),true,ifeq3(of(skc17,skc28,X0),true,ifeq3(entity(skc17,X0),true,skc28,skc28),skc28),skc28) ).

cnf(u11426,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u9967,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,X1),true,ifeq3(agent(skc17,skc18,X1),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u11279,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u9363,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc28,skc24),true,ifeq3(of(skc17,skc19,skc24),true,skc28,skc19),skc19) ).

cnf(u406,negated_conjecture,
    true = unisex(skc14,skc18) ).

cnf(u11839,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u680,negated_conjecture,
    b = ifeq(tuple(specific(skc14,skc19),true),tuple(true,true),a,b) ).

cnf(u3014,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human_person(X0,skc20),true,true,true),true) ).

cnf(u10946,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(theme(skc14,X2,skc17),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u365,negated_conjecture,
    true = theme(skc14,skc18,skc17) ).

cnf(u903,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc18),true,true,true),true) ).

cnf(u4054,negated_conjecture,
    true = ifeq2(male(skc14,X0),true,male(skc17,X0),true) ).

cnf(u2944,negated_conjecture,
    true = existent(skc17,skc20) ).

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

cnf(u2973,negated_conjecture,
    true = unisex(skc17,skf1(X0)) ).

cnf(u10896,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u10256,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u1256,negated_conjecture,
    true = thing(skc17,skc20) ).

cnf(u9916,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,skc17),true,ifeq3(agent(skc14,skc16,X1),true,ifeq3(agent(skc14,X0,X1),true,ifeq3(think_believe_consider(skc14,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u5580,negated_conjecture,
    ifeq3(theme(skc17,X3,X2),true,ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,X3,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(think_believe_consider(skc17,X3),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X1),true,X1,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u2983,negated_conjecture,
    true = ifeq2(nonexistent(skc14,skf1(X0)),true,true,true) ).

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

cnf(u11838,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u8707,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc25),true) ).

cnf(u809,negated_conjecture,
    true = event(skc17,skc18) ).

cnf(u4495,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,agent(X0,skc16,skc20),true) ).

cnf(u8565,negated_conjecture,
    true = event(skc17,skc25) ).

cnf(u2607,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,general(X0,skc23),true) ).

cnf(u3136,negated_conjecture,
    true = agent(skc17,skf1(skc27),skc27) ).

cnf(u3559,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,impartial(X0,skc20),true) ).

cnf(u2068,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relation(X0,skc23),true,true,true),true) ).

cnf(u4469,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,agent(X0,skf1(skc24),skc24),true) ).

cnf(u2200,negated_conjecture,
    true = general(skc17,skc23) ).

cnf(u899,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc24),true,true,true),true) ).

cnf(u8170,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc28,skc24),true,ifeq3(of(skc14,skc19,skc24),true,skc28,skc19),skc19) ).

cnf(u3106,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,organism(X0,skc20),true) ).

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

cnf(u3681,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(living(X0,skc20),true,true,true),true) ).

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

cnf(u9455,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc23,skc20),true,ifeq3(of(skc17,skc28,skc20),true,skc23,skc28),skc28) ).

cnf(u2410,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonhuman(X0,skc28),true) ).

cnf(u1120,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc20),true) ).

cnf(u4155,negated_conjecture,
    true = relname(skc17,skc19) ).

cnf(u8763,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonexistent(X0,skc25),true,true,true),true) ).

cnf(u9115,negated_conjecture,
    true = ifeq2(theme(X0,skc16,skc17),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u693,negated_conjecture,
    b = ifeq(tuple(true,existent(skc14,skc18)),tuple(true,true),a,b) ).

cnf(u7619,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc23,skc20),true,skc23,skc19) ).

cnf(u8602,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,event(X0,skc25),true) ).

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

cnf(u132,axiom,
    true = ifeq2(be(X0,X1,X2,X3),true,ifeq2(accessible_world(X0,X4),true,be(X4,X1,X2,X3),true),true) ).

cnf(u821,negated_conjecture,
    true = ifeq2(smoke(skc17,skc18),true,true,true) ).

cnf(u335,negated_conjecture,
    true = man(skc14,skc27) ).

cnf(u467,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc26),true,true,true) ).

cnf(u9917,negated_conjecture,
    skc17 = ifeq3(theme(skc14,skc16,X1),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u414,negated_conjecture,
    true = abstraction(skc14,skc17) ).

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

cnf(u9099,negated_conjecture,
    true = ifeq2(agent(X0,skc25,skc24),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u1507,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc18),true,true,true),true) ).

cnf(u3002,negated_conjecture,
    true = ifeq2(singleton(skc14,skf1(X0)),true,true,true) ).

cnf(u688,negated_conjecture,
    b = ifeq(tuple(true,human(skc14,skc23)),tuple(true,true),a,b) ).

cnf(u1226,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc26),true) ).

cnf(u8203,negated_conjecture,
    skc28 = ifeq3(of(skc14,X0,skc20),true,ifeq3(of(skc14,skc28,skc20),true,ifeq3(forename(skc14,X0),true,X0,skc28),skc28),skc28) ).

cnf(u911,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc16),true) ).

cnf(u5657,negated_conjecture,
    ifeq3(theme(skc14,skc16,X2),true,ifeq3(theme(skc14,X1,X0),true,ifeq3(agent(skc14,X1,skc20),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X2),true,ifeq3(proposition(skc14,X0),true,X0,X2),X2),X2),X2),X2),X2) = X2 ).

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

cnf(u3252,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,entity(X0,skc24),true) ).

cnf(u2766,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,state(X0,skc26),true) ).

cnf(u1285,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc23),true) ).

cnf(u8517,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc19,skc24),true,ifeq3(of(skc17,skc19,skc24),true,skc19,skc19),skc19) ).

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

cnf(u858,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc18),true,true,true) ).

cnf(u508,negated_conjecture,
    true = singleton(skc14,skc24) ).

cnf(u11300,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u689,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc14,skc27),true),tuple(true,true),a,b) ).

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

cnf(u817,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(event(X0,skc18),true,true,true),true) ).

cnf(u331,negated_conjecture,
    true = sF35 ).

cnf(u1560,negated_conjecture,
    true = ifeq2(nonexistent(skc14,skc25),true,true,true) ).

cnf(u241,negated_conjecture,
    true = sF5 ).

cnf(u1318,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc27),true,true,true),true) ).

cnf(u775,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc16),true,true,true) ).

cnf(u907,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc26),true,true,true),true) ).

cnf(u1512,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc26),true) ).

cnf(u4931,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,be(X0,skc26,skc27,skc27),true) ).

cnf(u8128,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc23,X0),true,ifeq3(of(skc14,skc19,X0),true,ifeq3(entity(skc14,X0),true,skc23,skc19),skc19),skc19) ).

cnf(u11645,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u1223,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc26),true) ).

cnf(u10897,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u870,negated_conjecture,
    true = ifeq2(event(skc14,skc25),true,true,true) ).

cnf(u504,negated_conjecture,
    true = singleton(skc14,skc27) ).

cnf(u553,negated_conjecture,
    true = animate(skc14,skc27) ).

cnf(u9496,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,skc17),true,ifeq3(agent(skc14,X0,X1),true,ifeq3(agent(skc14,skc18,X1),true,ifeq3(think_believe_consider(skc14,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u5294,negated_conjecture,
    ifeq3(of(skc17,X0,skc27),true,ifeq3(forename(skc17,X0),true,skc28,X0),X0) = X0 ).

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

cnf(u4511,negated_conjecture,
    true = ifeq2(agent(skc14,skc25,skc24),true,true,true) ).

cnf(u8700,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc25),true,true,true),true) ).

cnf(u3065,negated_conjecture,
    true = animate(skc17,skc24) ).

cnf(u343,negated_conjecture,
    true = vincent_forename(skc14,skc19) ).

cnf(u2025,negated_conjecture,
    true = nonhuman(skc17,skc17) ).

cnf(u274,negated_conjecture,
    true = sF16 ).

cnf(u674,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc18)),tuple(true,true),a,b) ).

cnf(u512,negated_conjecture,
    true = singleton(skc14,skc20) ).

cnf(u1536,negated_conjecture,
    true = specific(skc17,skc20) ).

cnf(u10103,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,X1),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u720,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skc16),true,true,true),true) ).

cnf(u3968,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,animate(X0,skc20),true) ).

cnf(u8576,negated_conjecture,
    true = nonexistent(skc17,skc25) ).

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

cnf(u3548,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(impartial(X0,skc20),true,true,true),true) ).

cnf(u226,negated_conjecture,
    true = sF0 ).

cnf(u1705,negated_conjecture,
    true = ifeq2(accessible_world(skc17,skc17),true,true,true) ).

cnf(u9839,negated_conjecture,
    skc17 = ifeq3(theme(skc14,skc16,X0),true,ifeq3(proposition(skc14,X0),true,X0,skc17),skc17) ).

cnf(u2960,negated_conjecture,
    true = ifeq2(state(skc17,skf1(X0)),true,true,true) ).

cnf(u388,negated_conjecture,
    true = singleton(skc14,skc18) ).

cnf(u8274,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc28,skc24),true,ifeq3(of(skc14,skc28,skc24),true,skc28,skc28),skc28) ).

cnf(u4152,negated_conjecture,
    true = ifeq2(jules_forename(skc17,skc19),true,true,true) ).

cnf(u697,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc14,skc24),true),tuple(true,true),a,b) ).

cnf(u10404,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(theme(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X0),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u3242,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(entity(X0,skc20),true,true,true),true) ).

cnf(u2178,negated_conjecture,
    true = abstraction(skc17,skc19) ).

cnf(u4156,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,forename(X0,skc19),true) ).

cnf(u1251,negated_conjecture,
    true = thing(skc17,skc23) ).

cnf(u286,negated_conjecture,
    true = sF20 ).

cnf(u686,negated_conjecture,
    b = ifeq(tuple(true,human(skc14,skc19)),tuple(true,true),a,b) ).

cnf(u1379,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonexistent(X0,skc26),true,true,true),true) ).

cnf(u2874,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(man(X0,skc24),true,true,true),true) ).

cnf(u560,negated_conjecture,
    true = male(skc14,skc24) ).

cnf(u1098,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc23),true,true,true),true) ).

cnf(u4141,negated_conjecture,
    true = forename(skc17,skc19) ).

cnf(u8009,negated_conjecture,
    skc23 = ifeq3(of(skc14,X0,skc27),true,ifeq3(of(skc14,skc23,skc27),true,ifeq3(forename(skc14,X0),true,X0,skc23),skc23),skc23) ).

cnf(u474,negated_conjecture,
    true = human_person(skc14,skc20) ).

cnf(u3022,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human_person(X0,skc24),true) ).

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

cnf(u1520,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc28),true) ).

cnf(u4400,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(jules_forename(X0,skc28),true,true,true),true) ).

cnf(u3259,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,entity(X0,skc20),true) ).

cnf(u1231,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc27),true) ).

cnf(u2972,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,eventuality(X1,skf1(X0)),true) ).

cnf(u2582,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(general(X0,skc23),true,true,true),true) ).

cnf(u9432,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc19,X0),true,ifeq3(of(skc17,skc28,X0),true,ifeq3(entity(skc17,X0),true,skc19,skc28),skc28),skc28) ).

cnf(u561,negated_conjecture,
    true = male(skc14,skc27) ).

cnf(u10393,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,skc17),true,ifeq3(theme(skc14,skc16,X1),true,ifeq3(agent(skc14,X0,skc20),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u3109,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,organism(X0,skc20),true) ).

cnf(u1292,negated_conjecture,
    true = singleton(skc17,skc19) ).

cnf(u2923,negated_conjecture,
    true = animate(skc17,skc20) ).

cnf(u3835,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human(X0,skc20),true) ).

cnf(u1115,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc23),true) ).

cnf(u682,negated_conjecture,
    b = ifeq(tuple(specific(skc14,skc23),true),tuple(true,true),a,b) ).

cnf(u9994,negated_conjecture,
    skc17 = ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc18,X0),true,skc17,skc17),skc17) ).

cnf(u3963,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,animate(X0,skc24),true) ).

cnf(u10559,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X1),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u486,negated_conjecture,
    true = entity(skc14,skc20) ).

cnf(u2589,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(general(X0,skc28),true,true,true),true) ).

cnf(u10604,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skc25),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u8094,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc28,skc20),true,ifeq3(of(skc14,skc23,skc20),true,skc28,skc23),skc23) ).

cnf(u1384,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonexistent(X0,skc18),true) ).

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

cnf(u10626,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u1526,negated_conjecture,
    true = ifeq2(unisex(skc14,X0),true,unisex(skc17,X0),true) ).

cnf(u1095,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc18),true,true,true),true) ).

cnf(u376,negated_conjecture,
    true = eventuality(skc14,skc18) ).

cnf(u1357,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc27),true) ).

cnf(u10261,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u8404,negated_conjecture,
    skc23 = ifeq3(of(skc17,X0,skc27),true,ifeq3(of(skc17,skc23,skc27),true,ifeq3(forename(skc17,X0),true,X0,skc23),skc23),skc23) ).

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

cnf(u1326,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc28),true,true,true),true) ).

cnf(u8566,negated_conjecture,
    true = present(skc17,skc25) ).

cnf(u3175,negated_conjecture,
    true = living(skc17,skc27) ).

cnf(u10008,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,skc17,skc17),skc17) ).

cnf(u663,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc16)),tuple(true,true),a,b) ).

cnf(u4224,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relname(X0,skc19),true,true,true),true) ).

cnf(u2273,negated_conjecture,
    b = ifeq(tuple(true,human(skc17,skc19)),tuple(true,true),a,b) ).

cnf(u1106,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc26),true,true,true),true) ).

cnf(u4349,negated_conjecture,
    true = ifeq2(vincent_forename(skc14,X0),true,vincent_forename(skc17,X0),true) ).

cnf(u482,negated_conjecture,
    true = organism(skc14,skc20) ).

cnf(u4229,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relname(X0,skc28),true) ).

cnf(u3099,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(organism(X0,skc24),true,true,true),true) ).

cnf(u8448,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc28,skc20),true,ifeq3(of(skc17,skc23,skc20),true,skc28,skc23),skc23) ).

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

cnf(u2904,negated_conjecture,
    true = smoke(skc17,skf1(X0)) ).

cnf(u5174,negated_conjecture,
    ifeq3(of(skc17,skc28,X1),true,ifeq3(of(skc17,X0,X1),true,ifeq3(forename(skc17,X0),true,ifeq3(entity(skc17,X1),true,skc28,X0),X0),X0),X0) = X0 ).

cnf(u2595,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,general(X0,skc23),true) ).

cnf(u979,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(eventuality(X0,skc26),true,true,true),true) ).

cnf(u4465,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc27),skc27),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u10097,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,skc18,X1),true,ifeq3(agent(skc17,X0,X1),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u8275,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc28,skc20),true,ifeq3(of(skc14,skc28,skc20),true,skc28,skc28),skc28) ).

cnf(u3114,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc17,skc24),true),tuple(true,true),a,b) ).

cnf(u1300,negated_conjecture,
    true = singleton(skc17,skc20) ).

cnf(u1663,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc19)),tuple(true,true),a,b) ).

cnf(u11912,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skf1(skc27),X1),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u645,negated_conjecture,
    true = ifeq2(vincent_forename(skc14,skc28),true,true,true) ).

cnf(u2393,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonhuman(X0,skc23),true) ).

cnf(u1354,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc24),true) ).

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

cnf(u2254,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,abstraction(X0,skc28),true) ).

cnf(u8824,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,present(X0,skc25),true) ).

cnf(u3692,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,living(X0,skc20),true) ).

cnf(u346,negated_conjecture,
    true = present(skc14,skc18) ).

cnf(u494,negated_conjecture,
    true = ifeq2(entity(skc14,skc18),true,true,true) ).

cnf(u4115,negated_conjecture,
    true = ifeq2(forename(skc14,X0),true,forename(skc17,X0),true) ).

cnf(u1252,negated_conjecture,
    true = thing(skc17,skc17) ).

cnf(u2239,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,abstraction(X0,skc23),true) ).

cnf(u4518,negated_conjecture,
    true = ifeq2(agent(skc14,skf1(skc27),skc27),true,true,true) ).

cnf(u2954,negated_conjecture,
    true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u11234,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(theme(skc17,X2,skc17),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4134,negated_conjecture,
    true = relname(skc17,skc23) ).

cnf(u325,negated_conjecture,
    true = sF33 ).

cnf(u1237,negated_conjecture,
    true = ifeq2(specific(skc14,X0),true,specific(skc17,X0),true) ).

cnf(u5595,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(agent(skc17,X2,skc24),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u9582,negated_conjecture,
    ifeq3(of(skc17,skc19,skc27),true,ifeq3(of(skc17,X0,skc27),true,ifeq3(forename(skc17,X0),true,skc19,X0),X0),X0) = X0 ).

cnf(u5695,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,X1),true,ifeq3(agent(skc14,skc18,X2),true,ifeq3(agent(skc14,X0,X2),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u2277,negated_conjecture,
    b = ifeq(tuple(specific(skc17,skc28),true),tuple(true,true),a,b) ).

cnf(u10865,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u641,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc28),true,true,true) ).

cnf(u2405,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonhuman(X0,skc23),true) ).

cnf(u554,negated_conjecture,
    true = animate(skc14,skc24) ).

cnf(u1500,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc19),true,true,true),true) ).

cnf(u411,negated_conjecture,
    true = relation(skc14,skc17) ).

cnf(u358,negated_conjecture,
    true = of(skc14,skc28,skc27) ).

cnf(u3836,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human(X0,skc24),true) ).

cnf(u1116,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc17),true) ).

cnf(u4043,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(male(X0,skc27),true,true,true),true) ).

cnf(u9174,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X2,X1),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u632,negated_conjecture,
    true = singleton(skc14,skc19) ).

cnf(u4345,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(vincent_forename(X0,skc19),true,true,true),true) ).

cnf(u987,negated_conjecture,
    b = ifeq(tuple(true,existent(skc17,skc26)),tuple(true,true),a,b) ).

cnf(u3837,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human(X0,skc27),true) ).

cnf(u11685,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(theme(skc17,skc18,X2),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u277,negated_conjecture,
    true = sF17 ).

cnf(u802,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,eventuality(X0,skc16),true) ).

cnf(u4108,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(forename(X0,skc19),true,true,true),true) ).

cnf(u653,negated_conjecture,
    true = ifeq2(jules_forename(skc14,skc19),true,true,true) ).

cnf(u5288,negated_conjecture,
    skc19 = ifeq3(of(skc14,X0,skc20),true,ifeq3(forename(skc14,X0),true,X0,skc19),skc19) ).

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

cnf(u3544,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(impartial(X0,skc27),true,true,true),true) ).

cnf(u535,negated_conjecture,
    true = impartial(skc14,skc20) ).

cnf(u781,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc16)),tuple(true,true),a,b) ).

cnf(u8793,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc25),true) ).

cnf(u4225,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relname(X0,skc23),true,true,true),true) ).

cnf(u1321,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc27),true,true,true) ).

cnf(u3683,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(living(X0,skc27),true,true,true),true) ).

cnf(u10284,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,skc17,skc17),skc17),skc17) ).

cnf(u313,negated_conjecture,
    true = sF29 ).

cnf(u2375,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonhuman(X0,skc28),true,true,true),true) ).

cnf(u1556,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc27),true) ).

cnf(u5167,negated_conjecture,
    skc23 = ifeq3(of(skc14,X1,X0),true,ifeq3(of(skc14,skc23,X0),true,ifeq3(forename(skc14,X1),true,ifeq3(entity(skc14,X0),true,X1,skc23),skc23),skc23),skc23) ).

cnf(u2980,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skf1(X0))),tuple(true,true),a,b) ).

cnf(u9196,negated_conjecture,
    ifeq3(theme(skc14,skc16,X0),true,ifeq3(proposition(skc14,X0),true,skc17,X0),X0) = X0 ).

cnf(u2596,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,general(X0,skc17),true) ).

cnf(u1214,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc27),true,true,true),true) ).

cnf(u8623,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,eventuality(X0,skc25),true) ).

cnf(u10204,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(theme(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X0),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u8822,negated_conjecture,
    true = ifeq2(present(X0,skc25),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u10254,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u1854,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc18),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u3119,negated_conjecture,
    true = man(skc17,skc27) ).

cnf(u419,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc18),true,true,true) ).

cnf(u3962,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,animate(X0,skc27),true) ).

cnf(u1648,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc17),true) ).

cnf(u896,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc28),true,true,true),true) ).

cnf(u8264,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc19,skc24),true,ifeq3(of(skc14,skc28,skc24),true,skc19,skc28),skc28) ).

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

cnf(u5182,negated_conjecture,
    ifeq3(of(skc14,skc28,X1),true,ifeq3(of(skc14,X0,X1),true,ifeq3(forename(skc14,X0),true,ifeq3(entity(skc14,X1),true,skc28,X0),X0),X0),X0) = X0 ).

cnf(u1297,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc20),true,true,true) ).

cnf(u981,negated_conjecture,
    true = unisex(skc17,skc26) ).

cnf(u2164,negated_conjecture,
    true = relation(skc17,skc28) ).

cnf(u1678,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc28),true) ).

cnf(u1109,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc16),true) ).

cnf(u5300,negated_conjecture,
    ifeq3(of(skc14,X0,skc20),true,ifeq3(forename(skc14,X0),true,skc19,X0),X0) = X0 ).

cnf(u9161,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,X2,skc24),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u11337,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X1,skc17),true,ifeq3(theme(skc17,skc18,X2),true,ifeq3(agent(skc17,X1,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,X2,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u332,negated_conjecture,
    true = actual_world(skc14) ).

cnf(u8152,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc23,skc27),true,ifeq3(of(skc14,skc19,skc27),true,skc23,skc19),skc19) ).

cnf(u464,negated_conjecture,
    true = nonexistent(skc14,skc26) ).

cnf(u11232,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X1,skc17),true,ifeq3(theme(skc17,X2,skc17),true,ifeq3(agent(skc17,X1,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(think_believe_consider(skc17,X2),true,skc17,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u3003,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(singleton(X1,skf1(X0)),true,true,true),true) ).

cnf(u283,negated_conjecture,
    true = sF19 ).

cnf(u908,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc16),true,true,true),true) ).

cnf(u762,negated_conjecture,
    true = specific(skc17,skc16) ).

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

cnf(u1323,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc27),true,true,true) ).

cnf(u10337,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u1407,negated_conjecture,
    true = ifeq2(singleton(skc14,skc25),true,true,true) ).

cnf(u4786,negated_conjecture,
    true = ifeq2(of(X0,skc19,skc20),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u4217,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relname(X0,skc23),true,true,true),true) ).

cnf(u1734,negated_conjecture,
    true = ifeq2(present(X0,skc16),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u859,negated_conjecture,
    b = ifeq(tuple(true,existent(skc17,skc18)),tuple(true,true),a,b) ).

cnf(u9810,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X1,skc17),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,X1,X0),true,ifeq3(think_believe_consider(skc14,X1),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u9173,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X2,X1),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u822,negated_conjecture,
    true = eventuality(skc17,skc18) ).

cnf(u328,negated_conjecture,
    true = sF34 ).

cnf(u1094,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc19),true,true,true),true) ).

cnf(u8483,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc19,X0),true,ifeq3(of(skc17,skc19,X0),true,ifeq3(entity(skc17,X0),true,skc19,skc19),skc19),skc19) ).

cnf(u8362,negated_conjecture,
    ifeq3(of(skc14,skc28,skc20),true,ifeq3(of(skc14,X0,skc20),true,ifeq3(forename(skc14,X0),true,skc28,X0),X0),X0) = X0 ).

cnf(u3058,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(human_person(X0,skc24),true,true,true),true) ).

cnf(u11282,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u10126,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17) ).

cnf(u801,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,eventuality(X0,skc18),true) ).

cnf(u295,negated_conjecture,
    true = sF23 ).

cnf(u4045,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,male(X0,skc24),true) ).

cnf(u626,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc23),true,true,true) ).

cnf(u904,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc16),true,true,true),true) ).

cnf(u3970,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,animate(X0,skc27),true) ).

cnf(u7769,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc19,skc24),true,skc23,skc19) ).

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

cnf(u4928,negated_conjecture,
    true = ifeq2(be(X0,skc26,skc27,skc27),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u989,negated_conjecture,
    true = ifeq2(entity(skc17,skc26),true,true,true) ).

cnf(u2962,negated_conjecture,
    true = eventuality(skc17,skf1(X0)) ).

cnf(u4214,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relname(X0,skc28),true,true,true),true) ).

cnf(u2594,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(general(X0,skc23),true,true,true),true) ).

cnf(u1635,negated_conjecture,
    true = unisex(skc17,skc23) ).

cnf(u3831,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,human(X0,skc20),true) ).

cnf(u2029,negated_conjecture,
    b = ifeq(tuple(true,human(skc17,skc17)),tuple(true,true),a,b) ).

cnf(u9169,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1) = X1 ).

cnf(u724,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skc18),true) ).

cnf(u2984,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(nonexistent(X1,skf1(X0)),true,true,true),true) ).

cnf(u5651,negated_conjecture,
    ifeq3(theme(skc14,X2,X1),true,ifeq3(theme(skc14,skc16,X0),true,ifeq3(agent(skc14,X2,skc20),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1107,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc26),true) ).

cnf(u1657,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc23)),tuple(true,true),a,b) ).

cnf(u2921,negated_conjecture,
    true = organism(skc17,skc20) ).

cnf(u2751,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,state(X0,skc26),true) ).

cnf(u521,negated_conjecture,
    true = specific(skc14,skc24) ).

cnf(u11686,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(theme(skc17,skc18,X2),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u7783,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc23,skc27),true,skc28,skc23) ).

cnf(u1022,negated_conjecture,
    true = ifeq2(thing(skc14,skc25),true,true,true) ).

cnf(u1503,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc17),true,true,true),true) ).

cnf(u4775,negated_conjecture,
    true = ifeq2(of(X0,skc23,skc24),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u10614,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u607,negated_conjecture,
    true = unisex(skc14,skc19) ).

cnf(u1331,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc28),true,true,true) ).

cnf(u11372,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u11447,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u4051,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,male(X0,skc24),true) ).

cnf(u5650,negated_conjecture,
    ifeq3(theme(skc14,X2,X1),true,ifeq3(theme(skc14,skc18,X0),true,ifeq3(agent(skc14,X2,skc20),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1550,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc24),true) ).

cnf(u4763,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,of(X0,skc23,skc24),true) ).

cnf(u2171,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relation(X0,skc23),true) ).

cnf(u2974,negated_conjecture,
    true = nonexistent(skc17,skf1(X0)) ).

cnf(u3155,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,human_person(X0,skc27),true) ).

cnf(u7610,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc19,skc24),true,skc19,skc23) ).

cnf(u547,negated_conjecture,
    true = human(skc14,skc27) ).

cnf(u2924,negated_conjecture,
    b = ifeq(tuple(unisex(skc17,skc20),true),tuple(true,true),a,b) ).

cnf(u10844,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u2026,negated_conjecture,
    true = general(skc17,skc17) ).

cnf(u4429,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(jules_forename(X0,skc28),true,true,true),true) ).

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

cnf(u2993,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,specific(X1,skf1(X0)),true) ).

cnf(u4360,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(vincent_forename(X0,skc19),true,true,true),true) ).

cnf(u3964,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,animate(X0,skc20),true) ).

cnf(u1642,negated_conjecture,
    true = unisex(skc17,skc28) ).

cnf(u9429,negated_conjecture,
    skc28 = ifeq3(of(skc17,X0,skc24),true,ifeq3(of(skc17,skc28,skc24),true,ifeq3(forename(skc17,X0),true,X0,skc28),skc28),skc28) ).

cnf(u2875,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(man(X0,skc20),true,true,true),true) ).

cnf(u4042,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(male(X0,skc24),true,true,true),true) ).

cnf(u721,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skc26),true,true,true),true) ).

cnf(u780,negated_conjecture,
    b = ifeq(tuple(true,existent(skc17,skc16)),tuple(true,true),a,b) ).

cnf(u8077,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc23,skc20),true,ifeq3(of(skc14,skc23,skc20),true,skc23,skc23),skc23) ).

cnf(u4606,negated_conjecture,
    true = theme(skc17,skc18,skc17) ).

cnf(u2006,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(proposition(X0,skc17),true,true,true),true) ).

cnf(u3110,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,organism(X0,skc24),true) ).

cnf(u3397,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(existent(X0,skc27),true,true,true),true) ).

cnf(u10775,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u1643,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc17),true,true,true),true) ).

cnf(u2274,negated_conjecture,
    b = ifeq(tuple(specific(skc17,skc19),true),tuple(true,true),a,b) ).

cnf(u5586,negated_conjecture,
    ifeq3(theme(skc17,skc18,X3),true,ifeq3(theme(skc17,X2,X1),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X3),true,ifeq3(proposition(skc17,X1),true,X1,X3),X3),X3),X3),X3),X3),X3) = X3 ).

cnf(u584,negated_conjecture,
    true = ifeq2(proposition(skc14,skc19),true,true,true) ).

cnf(u3046,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,man(X0,skc24),true) ).

cnf(u732,negated_conjecture,
    true = event(skc17,skc16) ).

cnf(u8484,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc28,X0),true,ifeq3(of(skc17,skc19,X0),true,ifeq3(entity(skc17,X0),true,skc28,skc19),skc19),skc19) ).

cnf(u4517,negated_conjecture,
    true = ifeq2(agent(skc14,skf1(skc24),skc24),true,true,true) ).

cnf(u11347,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(theme(skc17,X0,X1),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

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

cnf(u3005,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,singleton(X1,skf1(X0)),true) ).

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

cnf(u4195,negated_conjecture,
    true = ifeq2(vincent_forename(skc17,skc28),true,true,true) ).

cnf(u902,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc19),true,true,true),true) ).

cnf(u1849,negated_conjecture,
    true = think_believe_consider(skc17,skc16) ).

cnf(u1511,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc16),true) ).

cnf(u10560,negated_conjecture,
    ifeq3(theme(skc17,skc25,X1),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u10293,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,skc17,skc17),skc17),skc17) ).

cnf(u4757,negated_conjecture,
    true = ifeq2(of(X0,skc28,skc27),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u4470,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,agent(X0,skf1(skc20),skc20),true) ).

cnf(u861,negated_conjecture,
    true = ifeq2(entity(skc17,skc18),true,true,true) ).

cnf(u503,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc27),true,true,true) ).

cnf(u8784,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc25),true,true,true),true) ).

cnf(u10557,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u980,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,eventuality(X0,skc26),true) ).

cnf(u1832,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc16),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u3168,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(organism(X0,skc27),true,true,true),true) ).

cnf(u596,negated_conjecture,
    true = thing(skc14,skc23) ).

cnf(u265,negated_conjecture,
    true = sF13 ).

cnf(u4403,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,jules_forename(X0,skc28),true) ).

cnf(u1636,negated_conjecture,
    true = unisex(skc17,skc17) ).

cnf(u3153,negated_conjecture,
    true = human(skc17,skc27) ).

cnf(u10481,negated_conjecture,
    ifeq3(theme(skc14,skc16,X0),true,ifeq3(theme(skc14,X1,skc17),true,ifeq3(agent(skc14,X1,skc20),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u1737,negated_conjecture,
    true = ifeq2(present(X0,skc18),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u3972,negated_conjecture,
    true = ifeq2(animate(skc14,X0),true,animate(skc17,X0),true) ).

cnf(u597,negated_conjecture,
    true = nonhuman(skc14,skc23) ).

cnf(u2580,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(general(X0,skc19),true,true,true),true) ).

cnf(u1835,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,think_believe_consider(X0,skc16),true) ).

cnf(u8205,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc19,X0),true,ifeq3(of(skc14,skc28,X0),true,ifeq3(entity(skc14,X0),true,skc19,skc28),skc28),skc28) ).

cnf(u367,negated_conjecture,
    true = be(skc14,skc26,skc27,skc27) ).

cnf(u499,negated_conjecture,
    true = thing(skc14,skc24) ).

cnf(u298,negated_conjecture,
    true = sF24 ).

cnf(u1264,negated_conjecture,
    true = ifeq2(entity(skc17,skc17),true,true,true) ).

cnf(u9465,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc19,skc24),true,ifeq3(of(skc17,skc28,skc24),true,skc19,skc28),skc28) ).

cnf(u2906,negated_conjecture,
    true = event(skc17,skf1(X0)) ).

cnf(u1258,negated_conjecture,
    true = thing(skc17,skc24) ).

cnf(u289,negated_conjecture,
    true = sF21 ).

cnf(u2251,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,abstraction(X0,skc19),true) ).

cnf(u250,negated_conjecture,
    true = sF8 ).

cnf(u2398,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonhuman(X0,skc28),true) ).

cnf(u3156,negated_conjecture,
    b = ifeq(tuple(unisex(skc17,skc27),true),tuple(true,true),a,b) ).

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

cnf(u1317,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc24),true) ).

cnf(u463,negated_conjecture,
    true = specific(skc14,skc26) ).

cnf(u465,negated_conjecture,
    true = unisex(skc14,skc26) ).

cnf(u11688,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u11345,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(theme(skc17,X0,X1),true,ifeq3(agent(skc17,X0,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u4923,negated_conjecture,
    true = be(skc17,skc26,skc27,skc27) ).

cnf(u235,negated_conjecture,
    true = sF3 ).

cnf(u9498,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u5655,negated_conjecture,
    ifeq3(theme(skc17,skc18,X2),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc20),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X0),true,X0,X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u4044,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,male(X0,skc27),true) ).

cnf(u4478,negated_conjecture,
    true = agent(skc17,skc18,skc20) ).

cnf(u363,negated_conjecture,
    true = agent(skc14,skc18,skc20) ).

cnf(u10793,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skc25),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u7777,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc28,skc20),true,skc19,skc28) ).

cnf(u310,negated_conjecture,
    true = sF28 ).

cnf(u2278,negated_conjecture,
    b = ifeq(tuple(true,human(skc17,skc28)),tuple(true,true),a,b) ).

cnf(u582,negated_conjecture,
    true = abstraction(skc14,skc23) ).

cnf(u988,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc26)),tuple(true,true),a,b) ).

cnf(u5160,negated_conjecture,
    skc19 = ifeq3(of(skc17,X1,X0),true,ifeq3(of(skc17,skc19,X0),true,ifeq3(forename(skc17,X1),true,ifeq3(entity(skc17,X0),true,X1,skc19),skc19),skc19),skc19) ).

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

cnf(u1104,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc16),true,true,true),true) ).

cnf(u11836,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(theme(skc17,skc16,X2),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u7620,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc28,skc20),true,skc28,skc19) ).

cnf(u8127,negated_conjecture,
    skc19 = ifeq3(of(skc14,X0,skc24),true,ifeq3(of(skc14,skc19,skc24),true,ifeq3(forename(skc14,X0),true,X0,skc19),skc19),skc19) ).

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(u9195,negated_conjecture,
    ifeq3(theme(skc14,X0,X1),true,ifeq3(agent(skc14,X0,skc20),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u11338,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X1,skc17),true,ifeq3(theme(skc17,skc16,X2),true,ifeq3(agent(skc17,X1,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,X2,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u1255,negated_conjecture,
    true = thing(skc17,skc19) ).

cnf(u10048,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,skc17,skc17),skc17),skc17) ).

cnf(u774,negated_conjecture,
    true = ifeq2(entity(skc17,skc16),true,true,true) ).

cnf(u7776,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc23,skc20),true,skc19,skc23) ).

cnf(u8076,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc23,skc27),true,ifeq3(of(skc14,skc23,skc27),true,skc23,skc23),skc23) ).

cnf(u1383,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonexistent(X0,skc26),true) ).

cnf(u605,negated_conjecture,
    true = nonhuman(skc14,skc19) ).

cnf(u247,negated_conjecture,
    true = sF7 ).

cnf(u1517,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc19),true) ).

cnf(u10518,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u375,negated_conjecture,
    true = eventuality(skc14,skc16) ).

cnf(u1645,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc17)),tuple(true,true),a,b) ).

cnf(u984,negated_conjecture,
    true = thing(skc17,skc26) ).

cnf(u4050,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,male(X0,skc27),true) ).

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

cnf(u675,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc16)),tuple(true,true),a,b) ).

cnf(u2199,negated_conjecture,
    true = nonhuman(skc17,skc23) ).

cnf(u3391,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(existent(X0,skc20),true,true,true),true) ).

cnf(u1715,negated_conjecture,
    true = ifeq2(present(skc14,X0),true,present(skc17,X0),true) ).

cnf(u5590,negated_conjecture,
    ifeq3(theme(skc14,skc16,X3),true,ifeq3(theme(skc14,X2,X1),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X3),true,ifeq3(proposition(skc14,X1),true,X1,X3),X3),X3),X3),X3),X3),X3) = X3 ).

cnf(u1280,negated_conjecture,
    true = ifeq2(entity(skc17,skc23),true,true,true) ).

cnf(u5287,negated_conjecture,
    skc23 = ifeq3(of(skc14,X0,skc24),true,ifeq3(forename(skc14,X0),true,X0,skc23),skc23) ).

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

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

cnf(u9583,negated_conjecture,
    ifeq3(of(skc17,skc19,skc24),true,ifeq3(of(skc17,X0,skc24),true,ifeq3(forename(skc17,X0),true,skc19,X0),X0),X0) = X0 ).

cnf(u3064,negated_conjecture,
    true = human(skc17,skc24) ).

cnf(u10726,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,X1,skc17),true,ifeq3(agent(skc17,X1,skc20),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u2992,negated_conjecture,
    true = ifeq2(entity(skc17,skf1(X0)),true,true,true) ).

cnf(u4585,negated_conjecture,
    true = ifeq2(theme(X0,skc18,skc17),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u2240,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,abstraction(X0,skc17),true) ).

cnf(u420,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc16),true,true,true) ).

cnf(u8575,negated_conjecture,
    true = specific(skc17,skc25) ).

cnf(u2608,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,general(X0,skc17),true) ).

cnf(u3561,negated_conjecture,
    true = ifeq2(impartial(skc14,X0),true,impartial(skc17,X0),true) ).

cnf(u1856,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,think_believe_consider(X0,skc18),true) ).

cnf(u2078,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relation(X0,skc17),true) ).

cnf(u9970,negated_conjecture,
    ifeq3(theme(skc17,X0,X1),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u4610,negated_conjecture,
    true = ifeq2(theme(X0,skc18,skc17),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u3689,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(living(X0,skc27),true,true,true),true) ).

cnf(u9518,negated_conjecture,
    skc17 = ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc18,X0),true,skc17,skc17),skc17) ).

cnf(u1514,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc17),true) ).

cnf(u590,negated_conjecture,
    true = ifeq2(proposition(skc14,skc28),true,true,true) ).

cnf(u229,negated_conjecture,
    true = sF1 ).

cnf(u21,axiom,
    true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).

cnf(u687,negated_conjecture,
    b = ifeq(tuple(true,human(skc14,skc17)),tuple(true,true),a,b) ).

cnf(u1283,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc23),true,true,true) ).

cnf(u8567,negated_conjecture,
    true = smoke(skc17,skc25) ).

cnf(u2195,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relation(X0,skc28),true) ).

cnf(u2609,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,general(X0,skc19),true) ).

cnf(u1345,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc19),true) ).

cnf(u2271,negated_conjecture,
    b = ifeq(tuple(true,human(skc17,skc23)),tuple(true,true),a,b) ).

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

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

cnf(u337,negated_conjecture,
    true = man(skc14,skc24) ).

cnf(u11125,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(theme(skc14,skc18,X2),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1504,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc23),true,true,true),true) ).

cnf(u1324,negated_conjecture,
    true = singleton(skc17,skc27) ).

cnf(u970,negated_conjecture,
    true = ifeq2(smoke(skc17,skc26),true,true,true) ).

cnf(u10895,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

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

cnf(u860,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc18)),tuple(true,true),a,b) ).

cnf(u2981,negated_conjecture,
    true = ifeq2(abstraction(skc17,skf1(X0)),true,true,true) ).

cnf(u683,negated_conjecture,
    b = ifeq(tuple(true,human(skc14,skc28)),tuple(true,true),a,b) ).

cnf(u778,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc16)),tuple(true,true),a,b) ).

cnf(u7770,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc28,skc24),true,skc23,skc28) ).

cnf(u3405,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,existent(X0,skc24),true) ).

cnf(u10015,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17) ).

cnf(u10727,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skf1(skc20),X1),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u8126,negated_conjecture,
    skc19 = ifeq3(of(skc14,X0,skc27),true,ifeq3(of(skc14,skc19,skc27),true,ifeq3(forename(skc14,X0),true,X0,skc19),skc19),skc19) ).

cnf(u1288,negated_conjecture,
    true = ifeq2(entity(skc17,skc19),true,true,true) ).

cnf(u3542,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(impartial(X0,skc20),true,true,true),true) ).

cnf(u664,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc17)),tuple(true,true),a,b) ).

cnf(u1127,negated_conjecture,
    true = ifeq2(singleton(skc14,X0),true,singleton(skc17,X0),true) ).

cnf(u1851,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc16),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u349,negated_conjecture,
    true = present(skc14,skc16) ).

cnf(u11233,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(theme(skc17,X2,skc17),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1261,negated_conjecture,
    true = thing(skc17,skc28) ).

cnf(u280,negated_conjecture,
    true = sF18 ).

cnf(u2957,negated_conjecture,
    true = ifeq2(event(skc14,skf1(X0)),true,true,true) ).

cnf(u2267,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(abstraction(X0,skc28),true,true,true),true) ).

cnf(u982,negated_conjecture,
    true = nonexistent(skc17,skc26) ).

cnf(u3079,negated_conjecture,
    true = entity(skc17,skc24) ).

cnf(u3406,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,existent(X0,skc27),true) ).

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

cnf(u232,negated_conjecture,
    true = sF2 ).

cnf(u1506,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc16),true,true,true),true) ).

cnf(u793,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(eventuality(X0,skc26),true,true,true),true) ).

cnf(u695,negated_conjecture,
    b = ifeq(tuple(true,existent(skc14,skc26)),tuple(true,true),a,b) ).

cnf(u1225,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc16),true) ).

cnf(u455,negated_conjecture,
    true = event(skc14,skc26) ).

cnf(u1551,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc27),true,true,true),true) ).

cnf(u8163,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc19,skc24),true,ifeq3(of(skc14,skc19,skc24),true,skc19,skc19),skc19) ).

cnf(u5159,negated_conjecture,
    skc23 = ifeq3(of(skc17,X1,X0),true,ifeq3(of(skc17,skc23,X0),true,ifeq3(forename(skc17,X1),true,ifeq3(entity(skc17,X0),true,X1,skc23),skc23),skc23),skc23) ).

cnf(u3248,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(entity(X0,skc20),true,true,true),true) ).

cnf(u3543,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(impartial(X0,skc24),true,true,true),true) ).

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

cnf(u676,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc26)),tuple(true,true),a,b) ).

cnf(u8319,negated_conjecture,
    ifeq3(of(skc14,skc19,skc27),true,ifeq3(of(skc14,X0,skc27),true,ifeq3(forename(skc14,X0),true,skc19,X0),X0),X0) = X0 ).

cnf(u8481,negated_conjecture,
    skc19 = ifeq3(of(skc17,X0,skc24),true,ifeq3(of(skc17,skc19,skc24),true,ifeq3(forename(skc17,X0),true,X0,skc19),skc19),skc19) ).

cnf(u8013,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc28,X0),true,ifeq3(of(skc14,skc23,X0),true,ifeq3(entity(skc14,X0),true,skc28,skc23),skc23),skc23) ).

cnf(u345,negated_conjecture,
    true = think_believe_consider(skc14,skc18) ).

cnf(u2873,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(man(X0,skc27),true,true,true),true) ).

cnf(u292,negated_conjecture,
    true = sF22 ).

cnf(u1716,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,present(X0,skc16),true) ).

cnf(u8406,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc23,X0),true,ifeq3(of(skc17,skc23,X0),true,ifeq3(entity(skc17,X0),true,skc23,skc23),skc23),skc23) ).

cnf(u2394,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonhuman(X0,skc17),true) ).

cnf(u1332,negated_conjecture,
    true = singleton(skc17,skc28) ).

cnf(u846,negated_conjecture,
    true = specific(skc17,skc18) ).

cnf(u2082,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relation(X0,skc28),true) ).

cnf(u11341,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skf1(skc20),X1),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u677,negated_conjecture,
    b = ifeq(tuple(specific(skc14,skc28),true),tuple(true,true),a,b) ).

cnf(u2963,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,event(X1,skf1(X0)),true) ).

cnf(u1386,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonexistent(X0,skc26),true) ).

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

cnf(u5179,negated_conjecture,
    ifeq3(of(skc14,skc23,X1),true,ifeq3(of(skc14,X0,X1),true,ifeq3(forename(skc14,X0),true,ifeq3(entity(skc14,X1),true,skc23,X0),X0),X0),X0) = X0 ).

cnf(u244,negated_conjecture,
    true = sF6 ).

cnf(u559,negated_conjecture,
    true = male(skc14,skc20) ).

cnf(u4418,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,jules_forename(X0,skc23),true) ).

cnf(u3839,negated_conjecture,
    true = ifeq2(human(skc14,X0),true,human(skc17,X0),true) ).

cnf(u447,negated_conjecture,
    true = ifeq2(state(skc14,skc16),true,true,true) ).

cnf(u2067,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relation(X0,skc17),true,true,true),true) ).

cnf(u1717,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,present(X0,skc18),true) ).

cnf(u11311,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u2986,negated_conjecture,
    b = ifeq(tuple(true,existent(skc17,skf1(X0))),tuple(true,true),a,b) ).

cnf(u672,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc24)),tuple(true,true),a,b) ).

cnf(u8574,negated_conjecture,
    true = singleton(skc17,skc25) ).

cnf(u3953,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(animate(X0,skc27),true,true,true),true) ).

cnf(u4052,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,male(X0,skc20),true) ).

cnf(u357,negated_conjecture,
    true = state(skc14,skc26) ).

cnf(u2876,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,man(X0,skc20),true) ).

cnf(u4132,negated_conjecture,
    true = ifeq2(vincent_forename(skc17,skc23),true,true,true) ).

cnf(u1269,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc17),true) ).

cnf(u5168,negated_conjecture,
    skc19 = ifeq3(of(skc14,X1,X0),true,ifeq3(of(skc14,skc19,X0),true,ifeq3(forename(skc14,X1),true,ifeq3(entity(skc14,X0),true,X1,skc19),skc19),skc19),skc19) ).

cnf(u1262,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc17),true,true,true),true) ).

cnf(u7784,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc19,skc27),true,skc28,skc19) ).

cnf(u2406,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonhuman(X0,skc17),true) ).

cnf(u842,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(eventuality(X0,skc18),true,true,true),true) ).

cnf(u10192,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,skc17),true,ifeq3(theme(skc14,skc18,X1),true,ifeq3(agent(skc14,X0,skc20),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u2237,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(abstraction(X0,skc17),true,true,true),true) ).

cnf(u2241,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,abstraction(X0,skc19),true) ).

cnf(u673,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc20)),tuple(true,true),a,b) ).

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

cnf(u4410,negated_conjecture,
    true = jules_forename(skc17,skc23) ).

cnf(u555,negated_conjecture,
    true = animate(skc14,skc20) ).

cnf(u443,negated_conjecture,
    true = unisex(skc14,skc17) ).

cnf(u1544,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc20),true) ).

cnf(u262,negated_conjecture,
    true = sF12 ).

cnf(u662,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc18)),tuple(true,true),a,b) ).

cnf(u8644,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc25),true,true,true),true) ).

cnf(u10445,negated_conjecture,
    ifeq3(theme(skc14,skc18,X0),true,ifeq3(theme(skc14,X1,skc17),true,ifeq3(agent(skc14,X1,skc20),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u1355,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc27),true,true,true),true) ).

cnf(u536,negated_conjecture,
    true = impartial(skc14,skc24) ).

cnf(u8570,negated_conjecture,
    true = agent(skc17,skc25,skc24) ).

cnf(u214,negated_conjecture,
    true = ifeq2(man(skc17,X0),true,agent(skc17,skf1(X0),X0),true) ).

cnf(u9101,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,agent(X0,skc25,skc24),true) ).

cnf(u1260,negated_conjecture,
    true = thing(skc17,skc27) ).

cnf(u488,negated_conjecture,
    true = entity(skc14,skc27) ).

cnf(u1394,negated_conjecture,
    true = ifeq2(nonexistent(skc14,X0),true,nonexistent(skc17,X0),true) ).

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

cnf(u1666,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc19),true) ).

cnf(u567,negated_conjecture,
    true = relname(skc14,skc19) ).

cnf(u1097,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc17),true,true,true),true) ).

cnf(u2009,negated_conjecture,
    true = relation(skc17,skc17) ).

cnf(u8084,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc19,skc27),true,ifeq3(of(skc14,skc23,skc27),true,skc19,skc23),skc23) ).

cnf(u658,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc28)),tuple(true,true),a,b) ).

cnf(u11015,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X1,skc17),true,ifeq3(theme(skc14,skc16,X2),true,ifeq3(agent(skc14,X1,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X2),true,X2,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u548,negated_conjecture,
    true = human(skc14,skc24) ).

cnf(u4113,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,forename(X0,skc28),true) ).

cnf(u1218,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc16),true,true,true),true) ).

cnf(u9112,negated_conjecture,
    true = theme(skc17,skc16,skc17) ).

cnf(u3040,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(man(X0,skc24),true,true,true),true) ).

cnf(u2407,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonhuman(X0,skc19),true) ).

cnf(u1360,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc28),true) ).

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

cnf(u3105,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,organism(X0,skc24),true) ).

cnf(u5585,negated_conjecture,
    ifeq3(theme(skc14,X3,X2),true,ifeq3(theme(skc14,skc18,X1),true,ifeq3(agent(skc14,X3,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(think_believe_consider(skc14,X3),true,ifeq3(proposition(skc14,X2),true,ifeq3(proposition(skc14,X1),true,X1,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u3016,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human_person(X0,skc27),true,true,true),true) ).

cnf(u3696,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,living(X0,skc27),true) ).

cnf(u4234,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relname(X0,skc23),true) ).

cnf(u2953,negated_conjecture,
    true = ifeq2(present(skc14,skf1(X0)),true,true,true) ).

cnf(u352,negated_conjecture,
    true = accessible_world(skc14,skc17) ).

cnf(u1118,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc18),true) ).

cnf(u500,negated_conjecture,
    true = thing(skc14,skc20) ).

cnf(u549,negated_conjecture,
    true = human(skc14,skc20) ).

cnf(u681,negated_conjecture,
    b = ifeq(tuple(specific(skc14,skc17),true),tuple(true,true),a,b) ).

cnf(u10252,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,X1),true,ifeq3(agent(skc17,skc16,X1),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u11346,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,X0,X1),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u319,negated_conjecture,
    true = sF31 ).

cnf(u928,negated_conjecture,
    true = ifeq2(thing(skc14,X0),true,thing(skc17,X0),true) ).

cnf(u3697,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,living(X0,skc24),true) ).

cnf(u10338,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u5180,negated_conjecture,
    ifeq3(of(skc14,skc19,X1),true,ifeq3(of(skc14,X0,X1),true,ifeq3(forename(skc14,X0),true,ifeq3(entity(skc14,X1),true,skc19,X0),X0),X0),X0) = X0 ).

cnf(u4915,negated_conjecture,
    true = ifeq2(be(X0,skc26,skc27,skc27),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u2380,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonhuman(X0,skc23),true,true,true),true) ).

cnf(u1310,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc24),true,true,true),true) ).

cnf(u5170,negated_conjecture,
    skc28 = ifeq3(of(skc14,X1,X0),true,ifeq3(of(skc14,skc28,X0),true,ifeq3(forename(skc14,X1),true,ifeq3(entity(skc14,X0),true,X1,skc28),skc28),skc28),skc28) ).

cnf(u9995,negated_conjecture,
    skc17 = ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,X0),true,skc17,skc17),skc17) ).

cnf(u2203,negated_conjecture,
    true = nonhuman(skc17,skc19) ).

cnf(u5290,negated_conjecture,
    skc28 = ifeq3(of(skc14,X0,skc27),true,ifeq3(forename(skc14,X0),true,X0,skc28),skc28) ).

cnf(u1850,negated_conjecture,
    true = think_believe_consider(skc17,skc18) ).

cnf(u4431,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,jules_forename(X0,skc28),true) ).

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

cnf(u4129,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(forename(X0,skc23),true,true,true),true) ).

cnf(u2750,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(state(X0,skc26),true,true,true),true) ).

cnf(u1553,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc27)),tuple(true,true),a,b) ).

cnf(u3243,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(entity(X0,skc24),true,true,true),true) ).

cnf(u4046,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,male(X0,skc20),true) ).

cnf(u10335,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u2238,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(abstraction(X0,skc23),true,true,true),true) ).

cnf(u2956,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,present(X0,skf1(X1)),true) ).

cnf(u364,negated_conjecture,
    true = of(skc14,skc19,skc20) ).

cnf(u496,negated_conjecture,
    true = ifeq2(entity(skc14,skc17),true,true,true) ).

cnf(u3025,negated_conjecture,
    true = ifeq2(human_person(skc14,X0),true,human_person(skc17,X0),true) ).

cnf(u2907,negated_conjecture,
    true = agent(skc17,skf1(skc20),skc20) ).

cnf(u1105,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc18),true,true,true),true) ).

cnf(u1099,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc26),true,true,true),true) ).

cnf(u2017,negated_conjecture,
    true = abstraction(skc17,skc17) ).

cnf(u792,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(eventuality(X0,skc18),true,true,true),true) ).

cnf(u666,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc26)),tuple(true,true),a,b) ).

cnf(u9625,negated_conjecture,
    ifeq3(of(skc17,skc28,skc20),true,ifeq3(of(skc17,X0,skc20),true,ifeq3(forename(skc17,X0),true,skc28,X0),X0),X0) = X0 ).

cnf(u5594,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(agent(skc17,X2,skc27),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u763,negated_conjecture,
    true = nonexistent(skc17,skc16) ).

cnf(u3557,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,impartial(X0,skc27),true) ).

cnf(u1228,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc18),true) ).

cnf(u11660,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u1675,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc28)),tuple(true,true),a,b) ).

cnf(u7763,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc19,skc27),true,skc19,skc28) ).

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

cnf(u744,negated_conjecture,
    true = ifeq2(smoke(skc17,skc16),true,true,true) ).

cnf(u1510,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc18),true) ).

cnf(u7895,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc23,skc20),true,skc23,skc19) ).

cnf(u4110,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,forename(X0,skc23),true) ).

cnf(u5605,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X2),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u9476,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc28,skc20),true,ifeq3(of(skc17,skc28,skc20),true,skc28,skc28),skc28) ).

cnf(u9971,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(agent(skc17,skc18,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u10279,negated_conjecture,
    skc17 = ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,X0),true,skc17,skc17),skc17) ).

cnf(u7951,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc19,skc27),true,skc28,skc19) ).

cnf(u1538,negated_conjecture,
    true = specific(skc17,skc27) ).

cnf(u914,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc17),true) ).

cnf(u4227,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relname(X0,skc19),true) ).

cnf(u804,negated_conjecture,
    true = ifeq2(eventuality(skc14,X0),true,eventuality(skc17,X0),true) ).

cnf(u530,negated_conjecture,
    true = existent(skc14,skc24) ).

cnf(u627,negated_conjecture,
    true = singleton(skc14,skc23) ).

cnf(u271,negated_conjecture,
    true = sF15 ).

cnf(u466,negated_conjecture,
    true = ifeq2(smoke(skc14,skc26),true,true,true) ).

cnf(u2994,negated_conjecture,
    true = ifeq2(thing(skc14,skf1(X0)),true,true,true) ).

cnf(u1539,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc20),true,true,true),true) ).

cnf(u3961,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(animate(X0,skc27),true,true,true),true) ).

cnf(u4484,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,agent(X0,skc18,skc20),true) ).

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

cnf(u3551,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,impartial(X0,skc27),true) ).

cnf(u9541,negated_conjecture,
    ifeq3(of(skc17,skc23,skc20),true,ifeq3(of(skc17,X0,skc20),true,ifeq3(forename(skc17,X0),true,skc23,X0),X0),X0) = X0 ).

cnf(u4106,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(forename(X0,skc28),true,true,true),true) ).

cnf(u963,negated_conjecture,
    true = event(skc17,skc26) ).

cnf(u5579,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X3,skc17),true,ifeq3(theme(skc14,X2,X1),true,ifeq3(agent(skc14,X3,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X3),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u4235,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relname(X0,skc19),true) ).

cnf(u10294,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,skc17,skc17),skc17),skc17) ).

cnf(u9170,negated_conjecture,
    ifeq3(theme(skc14,X2,X1),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1),X1) = X1 ).

cnf(u3098,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(organism(X0,skc27),true,true,true),true) ).

cnf(u11913,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skf1(skc24),X1),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2249,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,abstraction(X0,skc23),true) ).

cnf(u1284,negated_conjecture,
    true = singleton(skc17,skc23) ).

cnf(u4239,negated_conjecture,
    true = ifeq2(relname(skc14,X0),true,relname(skc17,X0),true) ).

cnf(u8587,negated_conjecture,
    true = ifeq2(state(skc17,skc25),true,true,true) ).

cnf(u543,negated_conjecture,
    true = living(skc14,skc27) ).

cnf(u800,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,eventuality(X0,skc26),true) ).

cnf(u542,negated_conjecture,
    true = living(skc14,skc24) ).

cnf(u639,negated_conjecture,
    true = ifeq2(entity(skc14,skc28),true,true,true) ).

cnf(u4788,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,of(X0,skc19,skc20),true) ).

cnf(u12017,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X1),true,ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u3690,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,living(X0,skc27),true) ).

cnf(u620,negated_conjecture,
    true = thing(skc14,skc28) ).

cnf(u3066,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,human_person(X0,skc24),true) ).

cnf(u4771,negated_conjecture,
    true = of(skc17,skc23,skc24) ).

cnf(u1215,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc24),true,true,true),true) ).

cnf(u1221,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc18),true,true,true),true) ).

cnf(u2204,negated_conjecture,
    true = general(skc17,skc19) ).

cnf(u1660,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc23),true) ).

cnf(u4461,negated_conjecture,
    true = ifeq2(agent(X0,skc16,skc20),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

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

cnf(u2897,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(man(X0,skc20),true,true,true),true) ).

cnf(u9430,negated_conjecture,
    skc28 = ifeq3(of(skc17,X0,skc20),true,ifeq3(of(skc17,skc28,skc20),true,ifeq3(forename(skc17,X0),true,X0,skc28),skc28),skc28) ).

cnf(u5158,negated_conjecture,
    ifeq3(of(skc14,X1,skc20),true,ifeq3(of(skc14,X0,skc20),true,ifeq3(forename(skc14,X1),true,ifeq3(forename(skc14,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u3244,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(entity(X0,skc27),true,true,true),true) ).

cnf(u2758,negated_conjecture,
    true = state(skc17,skc26) ).

cnf(u922,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc27),true) ).

cnf(u8564,negated_conjecture,
    skc15 = skc17 ).

cnf(u3691,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,living(X0,skc24),true) ).

cnf(u2189,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relation(X0,skc28),true,true,true),true) ).

cnf(u10847,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(theme(skc17,skf1(skc24),X1),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1117,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc16),true) ).

cnf(u3398,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,existent(X0,skc27),true) ).

cnf(u9497,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u8361,negated_conjecture,
    ifeq3(of(skc14,skc28,skc24),true,ifeq3(of(skc14,X0,skc24),true,ifeq3(forename(skc14,X0),true,skc28,X0),X0),X0) = X0 ).

cnf(u395,negated_conjecture,
    true = specific(skc14,skc16) ).

cnf(u342,negated_conjecture,
    true = man(skc14,skc20) ).

cnf(u3820,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human(X0,skc27),true,true,true),true) ).

cnf(u742,negated_conjecture,
    true = ifeq2(state(skc17,skc16),true,true,true) ).

cnf(u1547,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc24)),tuple(true,true),a,b) ).

cnf(u7937,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc28,skc24),true,skc23,skc28) ).

cnf(u8591,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc25)),tuple(true,true),a,b) ).

cnf(u1382,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonexistent(X0,skc26),true,true,true),true) ).

cnf(u764,negated_conjecture,
    true = unisex(skc17,skc16) ).

cnf(u5587,negated_conjecture,
    ifeq3(theme(skc17,skc16,X3),true,ifeq3(theme(skc17,X2,X1),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X3),true,ifeq3(proposition(skc17,X1),true,X1,X3),X3),X3),X3),X3),X3),X3) = X3 ).

cnf(u301,negated_conjecture,
    true = sF25 ).

cnf(u971,negated_conjecture,
    true = eventuality(skc17,skc26) ).

cnf(u3104,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(organism(X0,skc24),true,true,true),true) ).

cnf(u11560,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u3821,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human(X0,skc24),true,true,true),true) ).

cnf(u7902,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc23,skc27),true,skc23,skc28) ).

cnf(u1655,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc23),true,true,true),true) ).

cnf(u10843,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(theme(skc17,X1,skc17),true,ifeq3(agent(skc17,X1,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1346,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc20),true,true,true),true) ).

cnf(u5656,negated_conjecture,
    ifeq3(theme(skc14,skc18,X2),true,ifeq3(theme(skc14,X1,X0),true,ifeq3(agent(skc14,X1,skc20),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X2),true,ifeq3(proposition(skc14,X0),true,X0,X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u407,negated_conjecture,
    true = unisex(skc14,skc16) ).

cnf(u4917,negated_conjecture,
    true = ifeq2(be(skc14,X2,X1,X0),true,be(skc17,X2,X1,X0),true) ).

cnf(u11990,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X1),true,ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4362,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,vincent_forename(X0,skc19),true) ).

cnf(u8244,negated_conjecture,
    ifeq3(of(skc14,skc23,skc20),true,ifeq3(of(skc14,X0,skc20),true,ifeq3(forename(skc14,X0),true,skc23,X0),X0),X0) = X0 ).

cnf(u3826,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(human(X0,skc20),true,true,true),true) ).

cnf(u3257,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,entity(X0,skc27),true) ).

cnf(u983,negated_conjecture,
    true = specific(skc17,skc26) ).

cnf(u4041,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(male(X0,skc20),true,true,true),true) ).

cnf(u10253,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u2964,negated_conjecture,
    true = ifeq2(eventuality(skc14,skf1(X0)),true,true,true) ).

cnf(u4808,negated_conjecture,
    true = ifeq2(of(X0,skc28,skc27),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u4111,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,forename(X0,skc19),true) ).

cnf(u4216,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relname(X0,skc19),true,true,true),true) ).

cnf(u629,negated_conjecture,
    true = ifeq2(entity(skc14,skc19),true,true,true) ).

cnf(u569,negated_conjecture,
    true = relname(skc14,skc28) ).

cnf(u761,negated_conjecture,
    true = thing(skc17,skc16) ).

cnf(u3063,negated_conjecture,
    true = organism(skc17,skc24) ).

cnf(u10203,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(theme(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X0),true,X0,X1),X1),X1),X1) = X1 ).

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

cnf(u3103,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(organism(X0,skc20),true,true,true),true) ).

cnf(u2991,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skf1(X0))),tuple(true,true),a,b) ).

cnf(u1541,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc20)),tuple(true,true),a,b) ).

cnf(u2597,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,general(X0,skc19),true) ).

cnf(u350,negated_conjecture,
    true = think_believe_consider(skc14,skc16) ).

cnf(u2878,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,man(X0,skc27),true) ).

cnf(u1108,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc18),true) ).

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

cnf(u2379,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonhuman(X0,skc17),true,true,true),true) ).

cnf(u719,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skc18),true,true,true),true) ).

cnf(u2938,negated_conjecture,
    true = living(skc17,skc20) ).

cnf(u624,negated_conjecture,
    true = ifeq2(entity(skc14,skc23),true,true,true) ).

cnf(u847,negated_conjecture,
    true = thing(skc17,skc18) ).

cnf(u1505,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc26),true,true,true),true) ).

cnf(u1093,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc20),true,true,true),true) ).

cnf(u2072,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relation(X0,skc17),true,true,true),true) ).

cnf(u9391,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,skc17),true,ifeq3(agent(skc14,X0,skc20),true,ifeq3(think_believe_consider(skc14,X0),true,skc17,skc17),skc17),skc17) ).

cnf(u497,negated_conjecture,
    true = ifeq2(entity(skc14,skc26),true,true,true) ).

cnf(u3395,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(existent(X0,skc20),true,true,true),true) ).

cnf(u10679,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skf1(skc20),X1),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u448,negated_conjecture,
    true = ifeq2(state(skc14,skc18),true,true,true) ).

cnf(u2193,negated_conjecture,
    true = ifeq2(proposition(skc17,skc28),true,true,true) ).

cnf(u3173,negated_conjecture,
    true = entity(skc17,skc27) ).

cnf(u2987,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,nonexistent(X1,skf1(X0)),true) ).

cnf(u5581,negated_conjecture,
    ifeq3(theme(skc17,X3,X2),true,ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,X3,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(think_believe_consider(skc17,X3),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X1),true,X1,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u10102,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u746,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,event(X0,skc16),true) ).

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

cnf(u1325,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc27),true) ).

cnf(u3960,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(animate(X0,skc24),true,true,true),true) ).

cnf(u1220,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc16),true,true,true),true) ).

cnf(u843,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,eventuality(X0,skc18),true) ).

cnf(u1328,negated_conjecture,
    true = ifeq2(entity(skc17,skc28),true,true,true) ).

cnf(u8516,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc19,skc27),true,ifeq3(of(skc17,skc19,skc27),true,skc19,skc19),skc19) ).

cnf(u509,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc20),true,true,true) ).

cnf(u730,negated_conjecture,
    true = ifeq2(accessible_world(skc14,skc14),true,true,true) ).

cnf(u8320,negated_conjecture,
    ifeq3(of(skc14,skc19,skc24),true,ifeq3(of(skc14,X0,skc24),true,ifeq3(forename(skc14,X0),true,skc19,X0),X0),X0) = X0 ).

cnf(u3400,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,existent(X0,skc20),true) ).

cnf(u11237,negated_conjecture,
    ifeq3(theme(skc17,X0,X1),true,ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u10777,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u10136,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc18,X0),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17) ).

cnf(u3955,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(animate(X0,skc20),true,true,true),true) ).

cnf(u2392,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonhuman(X0,skc23),true,true,true),true) ).

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

cnf(u579,negated_conjecture,
    true = relation(skc14,skc28) ).

cnf(u727,negated_conjecture,
    true = ifeq2(event(skc14,X0),true,event(skc17,X0),true) ).

cnf(u4782,negated_conjecture,
    true = of(skc17,skc19,skc20) ).

cnf(u238,negated_conjecture,
    true = sF4 ).

cnf(u2946,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc17,skc20),true),tuple(true,true),a,b) ).

cnf(u3129,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(man(X0,skc27),true,true,true),true) ).

cnf(u1513,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc23),true) ).

cnf(u11241,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(theme(skc17,X1,skc17),true,ifeq3(agent(skc17,X1,skc20),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u11339,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skf1(skc27),X1),true,ifeq3(agent(skc17,X0,skc27),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u9838,negated_conjecture,
    skc17 = ifeq3(theme(skc14,skc18,X0),true,ifeq3(proposition(skc14,X0),true,X0,skc17),skc17) ).

cnf(u4472,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,agent(X0,skc16,skc20),true) ).

cnf(u505,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc24),true,true,true) ).

cnf(u2905,negated_conjecture,
    true = present(skc17,skf1(X0)) ).

cnf(u304,negated_conjecture,
    true = sF26 ).

cnf(u2272,negated_conjecture,
    b = ifeq(tuple(specific(skc17,skc23),true),tuple(true,true),a,b) ).

cnf(u3250,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(entity(X0,skc27),true,true,true),true) ).

cnf(u11016,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X1,skc17),true,ifeq3(theme(skc14,skc18,X2),true,ifeq3(agent(skc14,X1,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X2),true,X2,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u3178,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc17,skc27),true),tuple(true,true),a,b) ).

cnf(u7950,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc23,skc27),true,skc28,skc23) ).

cnf(u3001,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,thing(X1,skf1(X0)),true) ).

cnf(u9193,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u2170,negated_conjecture,
    true = abstraction(skc17,skc23) ).

cnf(u622,negated_conjecture,
    true = general(skc14,skc28) ).

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

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

cnf(u591,negated_conjecture,
    true = abstraction(skc14,skc28) ).

cnf(u1315,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc24),true,true,true) ).

cnf(u723,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skc16),true) ).

cnf(u2227,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(abstraction(X0,skc17),true,true,true),true) ).

cnf(u4035,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(male(X0,skc20),true,true,true),true) ).

cnf(u2958,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(event(X1,skf1(X0)),true,true,true),true) ).

cnf(u1377,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonexistent(X0,skc18),true,true,true),true) ).

cnf(u8430,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc23,skc27),true,ifeq3(of(skc17,skc23,skc27),true,skc23,skc23),skc23) ).

cnf(u3018,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(human_person(X0,skc20),true,true,true),true) ).

cnf(u8598,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,smoke(X0,skc25),true) ).

cnf(u369,negated_conjecture,
    true = ifeq2(smoke(skc14,skc18),true,true,true) ).

cnf(u4198,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,forename(X0,skc28),true) ).

cnf(u2908,negated_conjecture,
    true = ifeq2(man(skc17,X0),true,true,true) ).

cnf(u316,negated_conjecture,
    true = sF30 ).

cnf(u3829,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,human(X0,skc27),true) ).

cnf(u2010,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,proposition(X0,skc17),true) ).

cnf(u7888,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc19,skc24),true,skc19,skc23) ).

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

cnf(u2977,negated_conjecture,
    true = ifeq2(unisex(skc14,skf1(X0)),true,true,true) ).

cnf(u4183,negated_conjecture,
    true = forename(skc17,skc28) ).

cnf(u2269,negated_conjecture,
    true = general(skc17,skc28) ).

cnf(u705,negated_conjecture,
    true = ifeq2(smoke(skc14,X0),true,smoke(skc17,X0),true) ).

cnf(u9198,negated_conjecture,
    skc17 = ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc16,X0),true,skc17,skc17),skc17) ).

cnf(u475,negated_conjecture,
    true = human_person(skc14,skc24) ).

cnf(u1704,negated_conjecture,
    true = ifeq2(accessible_world(skc17,skc14),true,true,true) ).

cnf(u422,negated_conjecture,
    true = thing(skc14,skc17) ).

cnf(u4759,negated_conjecture,
    true = ifeq2(of(X0,skc19,skc20),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u253,negated_conjecture,
    true = sF9 ).

cnf(u1515,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc16),true) ).

cnf(u9812,negated_conjecture,
    skc17 = ifeq3(theme(skc14,skc18,X1),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u696,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc14,skc27),true),tuple(true,true),a,b) ).

cnf(u3030,negated_conjecture,
    true = man(skc17,skc24) ).

cnf(u7936,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc19,skc24),true,skc23,skc19) ).

cnf(u4405,negated_conjecture,
    true = ifeq2(jules_forename(skc14,X0),true,jules_forename(skc17,X0),true) ).

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

cnf(u2989,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(specific(X1,skf1(X0)),true,true,true),true) ).

cnf(u1293,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc19),true) ).

cnf(u8130,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc28,X0),true,ifeq3(of(skc14,skc19,X0),true,ifeq3(entity(skc14,X0),true,skc28,skc19),skc19),skc19) ).

cnf(u3111,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,organism(X0,skc27),true) ).

cnf(u10703,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u3954,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(animate(X0,skc24),true,true,true),true) ).

cnf(u11516,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u9194,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u599,negated_conjecture,
    true = unisex(skc14,skc23) ).

cnf(u845,negated_conjecture,
    true = nonexistent(skc17,skc18) ).

cnf(u487,negated_conjecture,
    true = entity(skc14,skc24) ).

cnf(u1385,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonexistent(X0,skc16),true) ).

cnf(u3687,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(living(X0,skc20),true,true,true),true) ).

cnf(u3152,negated_conjecture,
    true = organism(skc17,skc27) ).

cnf(u4590,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,theme(X0,skc18,skc17),true) ).

cnf(u2084,negated_conjecture,
    true = ifeq2(relation(skc14,X0),true,relation(skc17,X0),true) ).

cnf(u2885,negated_conjecture,
    true = man(skc17,skc20) ).

cnf(u915,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc16),true) ).

cnf(u4401,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(jules_forename(X0,skc23),true,true,true),true) ).

cnf(u10333,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,skc16,X1),true,ifeq3(agent(skc17,X0,X1),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u3044,negated_conjecture,
    true = human_person(skc17,skc24) ).

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

cnf(u1955,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(proposition(X0,skc17),true,true,true),true) ).

cnf(u8573,negated_conjecture,
    true = thing(skc17,skc25) ).

cnf(u1278,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc23),true,true,true),true) ).

cnf(u581,negated_conjecture,
    true = ifeq2(proposition(skc14,skc23),true,true,true) ).

cnf(u2995,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(thing(X1,skf1(X0)),true,true,true),true) ).

cnf(u3015,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human_person(X0,skc24),true,true,true),true) ).

cnf(u11492,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u3700,negated_conjecture,
    true = ifeq2(living(skc14,X0),true,living(skc17,X0),true) ).

cnf(u351,negated_conjecture,
    true = proposition(skc14,skc17) ).

cnf(u5596,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(agent(skc17,X2,skc20),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1712,negated_conjecture,
    true = ifeq2(present(X0,skc18),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u2250,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,abstraction(X0,skc17),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(u3249,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(entity(X0,skc24),true,true,true),true) ).

cnf(u8438,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc19,skc27),true,ifeq3(of(skc17,skc23,skc27),true,skc19,skc23),skc23) ).

cnf(u576,negated_conjecture,
    true = relation(skc14,skc23) ).

cnf(u2228,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(abstraction(X0,skc23),true,true,true),true) ).

cnf(u9431,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc23,X0),true,ifeq3(of(skc17,skc28,X0),true,ifeq3(entity(skc17,X0),true,skc23,skc28),skc28),skc28) ).

cnf(u10678,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,X1,skc17),true,ifeq3(agent(skc17,X1,skc20),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u10531,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1) = X1 ).

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

cnf(u1713,negated_conjecture,
    true = ifeq2(present(X0,skc16),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u1301,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc20),true) ).

cnf(u10336,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u3822,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human(X0,skc20),true,true,true),true) ).

cnf(u577,negated_conjecture,
    true = relation(skc14,skc19) ).

cnf(u1960,negated_conjecture,
    true = ifeq2(proposition(skc14,X0),true,proposition(skc17,X0),true) ).

cnf(u4037,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(male(X0,skc27),true,true,true),true) ).

cnf(u10135,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc16,X0),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17) ).

cnf(u3067,negated_conjecture,
    b = ifeq(tuple(unisex(skc17,skc24),true),tuple(true,true),a,b) ).

cnf(u347,negated_conjecture,
    true = event(skc14,skc18) ).

cnf(u495,negated_conjecture,
    true = ifeq2(entity(skc14,skc16),true,true,true) ).

cnf(u694,negated_conjecture,
    b = ifeq(tuple(true,existent(skc14,skc16)),tuple(true,true),a,b) ).

cnf(u972,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,event(X0,skc26),true) ).

cnf(u1340,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc23),true,true,true),true) ).

cnf(u1387,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonexistent(X0,skc16),true) ).

cnf(u2902,negated_conjecture,
    true = male(skc17,skc20) ).

cnf(u1334,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc17),true,true,true),true) ).

cnf(u11240,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(theme(skc17,X1,skc17),true,ifeq3(agent(skc17,X1,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u791,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(eventuality(X0,skc16),true,true,true),true) ).

cnf(u9918,negated_conjecture,
    skc17 = ifeq3(theme(skc14,skc18,X1),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u4612,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,theme(X0,skc18,skc17),true) ).

cnf(u923,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc28),true) ).

cnf(u10257,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u8596,negated_conjecture,
    b = ifeq(tuple(true,existent(skc17,skc25)),tuple(true,true),a,b) ).

cnf(u9969,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u10627,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u3698,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,living(X0,skc20),true) ).

cnf(u2077,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relation(X0,skc23),true) ).

cnf(u4416,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(jules_forename(X0,skc23),true,true,true),true) ).

cnf(u1501,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc18),true,true,true),true) ).

cnf(u10405,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(theme(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X0),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u8588,negated_conjecture,
    true = ifeq2(entity(skc17,skc25),true,true,true) ).

cnf(u359,negated_conjecture,
    true = of(skc14,skc23,skc24) ).

cnf(u3408,negated_conjecture,
    true = ifeq2(existent(skc14,X0),true,existent(skc17,X0),true) ).

cnf(u8011,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc23,X0),true,ifeq3(of(skc14,skc23,X0),true,ifeq3(entity(skc14,X0),true,skc23,skc23),skc23),skc23) ).

cnf(u5604,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc27),X2),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u690,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc14,skc24),true),tuple(true,true),a,b) ).

cnf(u8204,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc23,X0),true,ifeq3(of(skc14,skc28,X0),true,ifeq3(entity(skc14,X0),true,skc23,skc28),skc28),skc28) ).

cnf(u9110,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,theme(X0,skc16,skc17),true) ).

cnf(u4462,negated_conjecture,
    true = ifeq2(agent(X0,skc18,skc20),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u905,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc17),true,true,true),true) ).

cnf(u9197,negated_conjecture,
    ifeq3(theme(skc14,skc18,X0),true,ifeq3(proposition(skc14,X0),true,skc17,X0),X0) = X0 ).

cnf(u10555,negated_conjecture,
    ifeq3(theme(skc17,X0,X1),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u10846,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,ifeq3(proposition(skc17,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u7903,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc19,skc27),true,skc19,skc28) ).

cnf(u3081,negated_conjecture,
    true = living(skc17,skc24) ).

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

cnf(u4918,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,be(X0,skc26,skc27,skc27),true) ).

cnf(u7625,negated_conjecture,
    skc21 = skc19 ).

cnf(u8431,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc23,skc20),true,ifeq3(of(skc17,skc23,skc20),true,skc23,skc23),skc23) ).

cnf(u1721,negated_conjecture,
    true = ifeq2(present(skc14,skc25),true,true,true) ).

cnf(u2073,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relation(X0,skc17),true) ).

cnf(u2976,negated_conjecture,
    true = thing(skc17,skf1(X0)) ).

cnf(u256,negated_conjecture,
    true = sF10 ).

cnf(u10334,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u2614,negated_conjecture,
    true = ifeq2(general(skc14,X0),true,general(skc17,X0),true) ).

cnf(u585,negated_conjecture,
    true = abstraction(skc14,skc19) ).

cnf(u2592,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(general(X0,skc19),true,true,true),true) ).

cnf(u3258,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,entity(X0,skc24),true) ).

cnf(u1216,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc20),true,true,true),true) ).

cnf(u2194,negated_conjecture,
    true = abstraction(skc17,skc28) ).

cnf(u1508,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc26),true,true,true),true) ).

cnf(u355,negated_conjecture,
    true = forename(skc14,skc23) ).

cnf(u4463,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc20),skc20),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u1267,negated_conjecture,
    true = ifeq2(eventuality(skc17,skc17),true,true,true) ).

cnf(u3552,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,impartial(X0,skc24),true) ).

cnf(u5282,negated_conjecture,
    skc28 = ifeq3(of(skc17,X0,skc27),true,ifeq3(forename(skc17,X0),true,X0,skc28),skc28) ).

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

cnf(u671,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc27)),tuple(true,true),a,b) ).

cnf(u917,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc19),true) ).

cnf(u2412,negated_conjecture,
    true = ifeq2(nonhuman(skc14,X0),true,nonhuman(skc17,X0),true) ).

cnf(u2179,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relation(X0,skc19),true) ).

cnf(u1114,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc26),true) ).

cnf(u1342,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,singleton(X0,skc23),true) ).

cnf(u8482,negated_conjecture,
    skc19 = ifeq3(of(skc17,skc23,X0),true,ifeq3(of(skc17,skc19,X0),true,ifeq3(entity(skc17,X0),true,skc23,skc19),skc19),skc19) ).

cnf(u2593,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(general(X0,skc17),true,true,true),true) ).

cnf(u5280,negated_conjecture,
    skc19 = ifeq3(of(skc17,X0,skc20),true,ifeq3(forename(skc17,X0),true,X0,skc19),skc19) ).

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

cnf(u4489,negated_conjecture,
    true = agent(skc17,skc16,skc20) ).

cnf(u3147,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(human_person(X0,skc27),true,true,true),true) ).

cnf(u9968,negated_conjecture,
    ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1) = X1 ).

cnf(u469,negated_conjecture,
    true = singleton(skc14,skc26) ).

cnf(u2988,negated_conjecture,
    true = ifeq2(specific(skc14,skf1(X0)),true,true,true) ).

cnf(u268,negated_conjecture,
    true = sF14 ).

cnf(u400,negated_conjecture,
    true = nonexistent(skc14,skc18) ).

cnf(u4493,negated_conjecture,
    true = ifeq2(agent(X0,skc16,skc20),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u1509,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,unisex(X0,skc26),true) ).

cnf(u5299,negated_conjecture,
    ifeq3(of(skc14,X0,skc24),true,ifeq3(forename(skc14,X0),true,skc23,X0),X0) = X0 ).

cnf(u1545,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc24),true,true,true),true) ).

cnf(u10058,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,skc17,skc17),skc17),skc17) ).

cnf(u566,negated_conjecture,
    true = relname(skc14,skc23) ).

cnf(u844,negated_conjecture,
    true = unisex(skc17,skc18) ).

cnf(u3558,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,impartial(X0,skc24),true) ).

cnf(u698,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc14,skc20),true),tuple(true,true),a,b) ).

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

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

cnf(u667,negated_conjecture,
    b = ifeq(tuple(unisex(skc14,skc20),true),tuple(true,true),a,b) ).

cnf(u913,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc23),true) ).

cnf(u3174,negated_conjecture,
    true = impartial(skc17,skc27) ).

cnf(u8746,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc25),true,true,true),true) ).

cnf(u11235,negated_conjecture,
    ifeq3(theme(skc17,X0,X1),true,ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(agent(skc17,X0,skc27),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u8770,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,nonexistent(X0,skc25),true) ).

cnf(u5279,negated_conjecture,
    skc23 = ifeq3(of(skc17,X0,skc24),true,ifeq3(forename(skc17,X0),true,X0,skc23),skc23) ).

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

cnf(u9475,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc28,skc24),true,ifeq3(of(skc17,skc28,skc24),true,skc28,skc28),skc28) ).

cnf(u3828,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(human(X0,skc27),true,true,true),true) ).

cnf(u333,negated_conjecture,
    true = forename(skc14,skc28) ).

cnf(u3083,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc17,skc24),true),tuple(true,true),a,b) ).

cnf(u10519,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X1),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1) = X1 ).

cnf(u10601,negated_conjecture,
    ifeq3(theme(skc17,skc25,X0),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u11278,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u10774,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skc25,skc17),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skc25),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u1224,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,specific(X0,skc18),true) ).

cnf(u966,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(event(X0,skc26),true,true,true),true) ).

cnf(u10813,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u11427,negated_conjecture,
    ifeq3(theme(skc17,skc18,X0),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u8651,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc25),true) ).

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

cnf(u1343,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc19),true,true,true),true) ).

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

cnf(u531,negated_conjecture,
    true = existent(skc14,skc20) ).

cnf(u777,negated_conjecture,
    true = singleton(skc17,skc16) ).

cnf(u1122,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc24),true) ).

cnf(u1124,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc27),true) ).

cnf(u498,negated_conjecture,
    true = thing(skc14,skc27) ).

cnf(u4150,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(forename(X0,skc19),true,true,true),true) ).

cnf(u9199,negated_conjecture,
    skc17 = ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc16,X0),true,skc17,skc17),skc17) ).

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

cnf(u3550,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(impartial(X0,skc27),true,true,true),true) ).

cnf(u995,negated_conjecture,
    true = singleton(skc17,skc26) ).

cnf(u4135,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,forename(X0,skc23),true) ).

cnf(u522,negated_conjecture,
    true = specific(skc14,skc20) ).

cnf(u2378,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonhuman(X0,skc19),true,true,true),true) ).

cnf(u1088,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc28),true,true,true),true) ).

cnf(u1316,negated_conjecture,
    true = singleton(skc17,skc24) ).

cnf(u2066,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relation(X0,skc19),true,true,true),true) ).

cnf(u1230,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc24),true) ).

cnf(u4036,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(male(X0,skc24),true,true,true),true) ).

cnf(u661,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc19)),tuple(true,true),a,b) ).

cnf(u2947,negated_conjecture,
    true = ifeq2(smoke(skc14,skf1(X0)),true,true,true) ).

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

cnf(u11283,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,skc20),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u2270,negated_conjecture,
    true = nonhuman(skc17,skc28) ).

cnf(u3023,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human_person(X0,skc20),true) ).

cnf(u362,negated_conjecture,
    true = agent(skc14,skc16,skc20) ).

cnf(u1268,negated_conjecture,
    true = singleton(skc17,skc17) ).

cnf(u8408,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc28,X0),true,ifeq3(of(skc17,skc23,X0),true,ifeq3(entity(skc17,X0),true,skc28,skc23),skc23),skc23) ).

cnf(u2015,negated_conjecture,
    true = ifeq2(relname(skc17,skc17),true,true,true) ).

cnf(u4237,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relname(X0,skc28),true) ).

cnf(u1119,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc19),true) ).

cnf(u2236,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(abstraction(X0,skc19),true,true,true),true) ).

cnf(u10558,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(agent(skc17,skc16,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1381,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonexistent(X0,skc18),true,true,true),true) ).

cnf(u2390,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonhuman(X0,skc19),true,true,true),true) ).

cnf(u7944,negated_conjecture,
    skc28 = ifeq3(of(skc17,skc28,skc20),true,skc19,skc28) ).

cnf(u476,negated_conjecture,
    true = human_person(skc14,skc27) ).

cnf(u11469,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u9108,negated_conjecture,
    true = ifeq2(theme(X0,skc16,skc17),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

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

cnf(u1516,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc18),true) ).

cnf(u3261,negated_conjecture,
    true = ifeq2(entity(skc14,X0),true,entity(skc17,X0),true) ).

cnf(u3019,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,human_person(X0,skc20),true) ).

cnf(u427,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc17),true,true,true) ).

cnf(u1217,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc18),true,true,true),true) ).

cnf(u5591,negated_conjecture,
    ifeq3(theme(skc14,skc18,X3),true,ifeq3(theme(skc14,X2,X1),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X3),true,ifeq3(proposition(skc14,X1),true,X1,X3),X3),X3),X3),X3),X3),X3) = X3 ).

cnf(u646,negated_conjecture,
    true = ifeq2(vincent_forename(skc14,skc23),true,true,true) ).

cnf(u3389,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(existent(X0,skc27),true,true,true),true) ).

cnf(u1579,negated_conjecture,
    true = ifeq2(unisex(skc14,skc25),true,true,true) ).

cnf(u10583,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u5156,negated_conjecture,
    ifeq3(of(skc14,X1,skc27),true,ifeq3(of(skc14,X0,skc27),true,ifeq3(forename(skc14,X1),true,ifeq3(forename(skc14,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u5151,negated_conjecture,
    ifeq3(of(skc17,X1,skc24),true,ifeq3(of(skc17,X0,skc24),true,ifeq3(forename(skc17,X1),true,ifeq3(forename(skc17,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u520,negated_conjecture,
    true = specific(skc14,skc27) ).

cnf(u2982,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X1),true,unisex(X1,skf1(X0)),true) ).

cnf(u1286,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc19),true,true,true),true) ).

cnf(u668,negated_conjecture,
    b = ifeq(tuple(unisex(skc14,skc24),true),tuple(true,true),a,b) ).

cnf(u10099,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc16,X1),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u4346,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,vincent_forename(X0,skc19),true) ).

cnf(u2063,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relation(X0,skc28),true,true,true),true) ).

cnf(u8405,negated_conjecture,
    skc23 = ifeq3(of(skc17,X0,skc20),true,ifeq3(of(skc17,skc23,skc20),true,ifeq3(forename(skc17,X0),true,X0,skc23),skc23),skc23) ).

cnf(u3959,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(animate(X0,skc20),true,true,true),true) ).

cnf(u7889,negated_conjecture,
    skc23 = ifeq3(of(skc17,skc28,skc24),true,skc28,skc23) ).

cnf(u10112,negated_conjecture,
    skc17 = ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc16,X0),true,skc17,skc17),skc17) ).

cnf(u1096,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc16),true,true,true),true) ).

cnf(u2600,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,general(X0,skc28),true) ).

cnf(u12042,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X1),true,ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u669,negated_conjecture,
    b = ifeq(tuple(unisex(skc14,skc27),true),tuple(true,true),a,b) ).

cnf(u1378,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonexistent(X0,skc16),true,true,true),true) ).

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

cnf(u11340,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skf1(skc24),X1),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u797,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,eventuality(X0,skc16),true) ).

cnf(u5152,negated_conjecture,
    ifeq3(of(skc17,X1,skc20),true,ifeq3(of(skc17,X0,skc20),true,ifeq3(forename(skc17,X1),true,ifeq3(forename(skc17,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u11630,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(theme(skc17,skf1(skc27),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u370,negated_conjecture,
    true = ifeq2(smoke(skc14,skc16),true,true,true) ).

cnf(u916,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc18),true) ).

cnf(u3176,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,organism(X0,skc27),true) ).

cnf(u642,negated_conjecture,
    true = singleton(skc14,skc28) ).

cnf(u8010,negated_conjecture,
    skc23 = ifeq3(of(skc14,X0,skc20),true,ifeq3(of(skc14,skc23,skc20),true,ifeq3(forename(skc14,X0),true,X0,skc23),skc23),skc23) ).

cnf(u3399,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,existent(X0,skc24),true) ).

cnf(u985,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc26)),tuple(true,true),a,b) ).

cnf(u3390,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(existent(X0,skc24),true,true,true),true) ).

cnf(u3080,negated_conjecture,
    true = impartial(skc17,skc24) ).

cnf(u2391,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonhuman(X0,skc17),true,true,true),true) ).

cnf(u1229,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc20),true) ).

cnf(u10655,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc20),skc17),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u1673,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(unisex(X0,skc28),true,true,true),true) ).

cnf(u2612,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,general(X0,skc28),true) ).

cnf(u4120,negated_conjecture,
    true = forename(skc17,skc23) ).

cnf(u665,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc23)),tuple(true,true),a,b) ).

cnf(u9116,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,theme(X0,skc16,skc17),true) ).

cnf(u3135,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,man(X0,skc27),true) ).

cnf(u1313,negated_conjecture,
    true = ifeq2(abstraction(skc17,skc24),true,true,true) ).

cnf(u3553,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,impartial(X0,skc20),true) ).

cnf(u11446,negated_conjecture,
    ifeq3(theme(skc17,skc16,X0),true,ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(agent(skc17,skc16,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0),X0) = X0 ).

cnf(u1219,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc26),true,true,true),true) ).

cnf(u382,negated_conjecture,
    true = thing(skc14,skc18) ).

cnf(u912,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc26),true) ).

cnf(u3182,negated_conjecture,
    true = existent(skc17,skc27) ).

cnf(u4810,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,of(X0,skc28,skc27),true) ).

cnf(u3045,negated_conjecture,
    true = male(skc17,skc24) ).

cnf(u4109,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(forename(X0,skc23),true,true,true),true) ).

cnf(u9811,negated_conjecture,
    skc17 = ifeq3(theme(skc14,skc16,X1),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u4222,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relname(X0,skc28),true,true,true),true) ).

cnf(u4226,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,relname(X0,skc23),true) ).

cnf(u1125,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc28),true) ).

cnf(u8571,negated_conjecture,
    true = theme(skc14,skc16,skc17) ).

cnf(u2387,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonhuman(X0,skc28),true,true,true),true) ).

cnf(u1834,negated_conjecture,
    true = ifeq2(think_believe_consider(skc14,X0),true,think_believe_consider(skc17,X0),true) ).

cnf(u3404,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,existent(X0,skc20),true) ).

cnf(u2577,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(general(X0,skc28),true,true,true),true) ).

cnf(u1537,negated_conjecture,
    true = specific(skc17,skc24) ).

cnf(u401,negated_conjecture,
    true = nonexistent(skc14,skc16) ).

cnf(u2165,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(relation(X0,skc23),true,true,true),true) ).

cnf(u5649,negated_conjecture,
    ifeq3(theme(skc17,X2,X1),true,ifeq3(theme(skc17,skc18,X0),true,ifeq3(agent(skc17,X2,skc20),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u5689,negated_conjecture,
    ifeq3(theme(skc14,X2,X1),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1),X1) = X1 ).

cnf(u348,negated_conjecture,
    true = event(skc14,skc16) ).

cnf(u480,negated_conjecture,
    true = organism(skc14,skc27) ).

cnf(u11281,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc27),skc17),true,ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,skc27),true,ifeq3(think_believe_consider(skc17,skf1(skc27)),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u428,negated_conjecture,
    true = singleton(skc14,skc17) ).

cnf(u529,negated_conjecture,
    true = existent(skc14,skc27) ).

cnf(u8597,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(smoke(X0,skc25),true,true,true),true) ).

cnf(u4467,negated_conjecture,
    true = ifeq2(agent(skc14,X1,X0),true,agent(skc17,X1,X0),true) ).

cnf(u1388,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonexistent(X0,skc18),true) ).

cnf(u3133,negated_conjecture,
    true = human_person(skc17,skc27) ).

cnf(u5172,negated_conjecture,
    ifeq3(of(skc17,skc19,X1),true,ifeq3(of(skc17,X0,X1),true,ifeq3(forename(skc17,X0),true,ifeq3(entity(skc17,X1),true,skc19,X0),X0),X0),X0) = X0 ).

cnf(u1089,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc27),true,true,true),true) ).

cnf(u10864,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,X0,skc17),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,X0),true,skc17,skc17),skc17),skc17),skc17),skc17) ).

cnf(u4471,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,agent(X0,skc18,skc20),true) ).

cnf(u5291,negated_conjecture,
    ifeq3(of(skc17,X0,skc24),true,ifeq3(forename(skc17,X0),true,skc23,X0),X0) = X0 ).

cnf(u4402,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,jules_forename(X0,skc23),true) ).

cnf(u5157,negated_conjecture,
    ifeq3(of(skc14,X1,skc24),true,ifeq3(of(skc14,X0,skc24),true,ifeq3(forename(skc14,X1),true,ifeq3(forename(skc14,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u1736,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,present(X0,skc16),true) ).

cnf(u8601,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(event(X0,skc25),true,true,true),true) ).

cnf(u7762,negated_conjecture,
    skc28 = ifeq3(of(skc14,skc23,skc27),true,skc23,skc28) ).

cnf(u1352,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(singleton(X0,skc24),true,true,true),true) ).

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

cnf(u9984,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc20),X0),true,ifeq3(think_believe_consider(skc17,skf1(skc20)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0) = X0 ).

cnf(u7612,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc28,skc24),true,skc28,skc23) ).

cnf(u3830,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,human(X0,skc24),true) ).

cnf(u344,negated_conjecture,
    true = forename(skc14,skc19) ).

cnf(u8012,negated_conjecture,
    skc23 = ifeq3(of(skc14,skc19,X0),true,ifeq3(of(skc14,skc23,X0),true,ifeq3(entity(skc14,X0),true,skc19,skc23),skc23),skc23) ).

cnf(u541,negated_conjecture,
    true = living(skc14,skc20) ).

cnf(u3021,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human_person(X0,skc27),true) ).

cnf(u4516,negated_conjecture,
    true = ifeq2(agent(skc14,skf1(skc20),skc20),true,true,true) ).

cnf(u10944,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X1,skc17),true,ifeq3(theme(skc14,X2,skc17),true,ifeq3(agent(skc14,X1,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(think_believe_consider(skc14,X2),true,skc17,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u8593,negated_conjecture,
    b = ifeq(tuple(true,general(skc17,skc25)),tuple(true,true),a,b) ).

cnf(u1227,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc16),true) ).

cnf(u920,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc24),true) ).

cnf(u10101,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17) ).

cnf(u857,negated_conjecture,
    b = ifeq(tuple(true,male(skc17,skc18)),tuple(true,true),a,b) ).

cnf(u450,negated_conjecture,
    true = eventuality(skc14,skc26) ).

cnf(u2978,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc17),true,ifeq2(unisex(X1,skf1(X0)),true,true,true),true) ).

cnf(u10945,negated_conjecture,
    ifeq3(theme(skc14,skc16,X1),true,ifeq3(theme(skc14,X2,skc17),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(agent(skc14,X2,X0),true,ifeq3(think_believe_consider(skc14,X2),true,ifeq3(proposition(skc14,X1),true,skc17,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4760,negated_conjecture,
    true = ifeq2(of(X0,skc23,skc24),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

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

cnf(u740,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(event(X0,skc16),true,true,true),true) ).

cnf(u3000,negated_conjecture,
    true = singleton(skc17,skf1(X0)) ).

cnf(u9162,negated_conjecture,
    ifeq3(theme(skc17,skc25,X2),true,ifeq3(theme(skc17,X1,X0),true,ifeq3(agent(skc17,X1,skc24),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,X1),true,ifeq3(proposition(skc17,X2),true,ifeq3(proposition(skc17,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u5162,negated_conjecture,
    skc28 = ifeq3(of(skc17,X1,X0),true,ifeq3(of(skc17,skc28,X0),true,ifeq3(forename(skc17,X1),true,ifeq3(entity(skc17,X0),true,X1,skc28),skc28),skc28),skc28) ).

cnf(u10877,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,skf1(skc24),skc17),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,skc17,skc17),skc17),skc17),skc17) ).

cnf(u4764,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,of(X0,skc19,skc20),true) ).

cnf(u2937,negated_conjecture,
    true = impartial(skc17,skc20) ).

cnf(u356,negated_conjecture,
    true = jules_forename(skc14,skc23) ).

cnf(u10602,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc25,skc17),true,ifeq3(theme(skc17,skc25,X0),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X0),true,X0,skc17),skc17),skc17),skc17),skc17) ).

cnf(u3154,negated_conjecture,
    true = animate(skc17,skc27) ).

cnf(u901,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc20),true,true,true),true) ).

cnf(u537,negated_conjecture,
    true = impartial(skc14,skc27) ).

cnf(u1222,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(specific(X0,skc26),true,true,true),true) ).

cnf(u910,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,thing(X0,skc18),true) ).

cnf(u307,negated_conjecture,
    true = sF27 ).

cnf(u1091,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc24),true,true,true),true) ).

cnf(u1450,negated_conjecture,
    true = ifeq2(specific(skc14,skc25),true,true,true) ).

cnf(u5292,negated_conjecture,
    ifeq3(of(skc17,X0,skc20),true,ifeq3(forename(skc17,X0),true,skc19,X0),X0) = X0 ).

cnf(u623,negated_conjecture,
    true = unisex(skc14,skc28) ).

cnf(u4482,negated_conjecture,
    true = ifeq2(agent(X0,skc18,skc20),true,ifeq2(accessible_world(X0,skc17),true,true,true),true) ).

cnf(u511,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc20),true,true,true) ).

cnf(u11070,negated_conjecture,
    ifeq3(theme(skc14,skc18,X1),true,ifeq3(theme(skc14,skc16,X2),true,ifeq3(agent(skc14,skc18,X0),true,ifeq3(agent(skc14,skc16,X0),true,ifeq3(proposition(skc14,X1),true,ifeq3(proposition(skc14,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1294,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc20),true,true,true),true) ).

cnf(u462,negated_conjecture,
    true = thing(skc14,skc26) ).

cnf(u10098,negated_conjecture,
    skc17 = ifeq3(theme(skc17,skc18,X1),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u604,negated_conjecture,
    true = thing(skc14,skc19) ).

cnf(u1502,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc16),true,true,true),true) ).

cnf(u2753,negated_conjecture,
    true = ifeq2(state(skc14,X0),true,state(skc17,X0),true) ).

cnf(u2940,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc17,skc20),true),tuple(true,true),a,b) ).

cnf(u3253,negated_conjecture,
    true = ifeq2(accessible_world(skc17,X0),true,entity(X0,skc20),true) ).

cnf(u2877,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,man(X0,skc24),true) ).

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

cnf(u897,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc27),true,true,true),true) ).

cnf(u906,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc23),true,true,true),true) ).

cnf(u9972,negated_conjecture,
    ifeq3(theme(skc17,skf1(skc24),X0),true,ifeq3(agent(skc17,skc18,skc24),true,ifeq3(think_believe_consider(skc17,skf1(skc24)),true,ifeq3(proposition(skc17,X0),true,skc17,X0),X0),X0),X0) = X0 ).

cnf(u796,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(eventuality(X0,skc16),true,true,true),true) ).

cnf(u9813,negated_conjecture,
    skc17 = ifeq3(theme(skc14,X0,X1),true,ifeq3(agent(skc14,X0,skc20),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc17),skc17),skc17),skc17) ).

cnf(u2764,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(state(X0,skc26),true,true,true),true) ).

cnf(u575,negated_conjecture,
    true = ifeq2(relname(skc14,skc17),true,true,true) ).

cnf(u3396,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(existent(X0,skc24),true,true,true),true) ).

cnf(u8577,negated_conjecture,
    true = unisex(skc17,skc25) ).

cnf(u10530,negated_conjecture,
    ifeq3(theme(skc17,skc16,X1),true,ifeq3(theme(skc17,skc16,X0),true,ifeq3(proposition(skc17,X1),true,ifeq3(proposition(skc17,X0),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u865,negated_conjecture,
    true = singleton(skc17,skc18) ).

cnf(u507,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc24),true,true,true) ).

cnf(u1836,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,think_believe_consider(X0,skc18),true) ).

cnf(u5302,negated_conjecture,
    ifeq3(of(skc14,X0,skc27),true,ifeq3(forename(skc14,X0),true,skc28,X0),X0) = X0 ).

cnf(u10556,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X0,skc17),true,ifeq3(theme(skc17,skc25,X1),true,ifeq3(agent(skc17,X0,skc24),true,ifeq3(think_believe_consider(skc17,X0),true,ifeq3(think_believe_consider(skc17,skc25),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17),skc17) ).

cnf(u8243,negated_conjecture,
    ifeq3(of(skc14,skc23,skc27),true,ifeq3(of(skc14,X0,skc27),true,ifeq3(forename(skc14,X0),true,skc23,X0),X0),X0) = X0 ).

cnf(u909,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(thing(X0,skc18),true,true,true),true) ).

cnf(u3688,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(living(X0,skc24),true,true,true),true) ).

cnf(u8162,negated_conjecture,
    skc19 = ifeq3(of(skc14,skc19,skc27),true,ifeq3(of(skc14,skc19,skc27),true,skc19,skc19),skc19) ).

cnf(u5690,negated_conjecture,
    skc17 = ifeq3(theme(skc17,X2,X1),true,ifeq3(agent(skc17,skc18,X0),true,ifeq3(agent(skc17,X2,X0),true,ifeq3(think_believe_consider(skc17,X2),true,ifeq3(proposition(skc17,X1),true,X1,skc17),skc17),skc17),skc17),skc17) ).

cnf(u1380,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc17),true,ifeq2(nonexistent(X0,skc16),true,true,true),true) ).

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

cnf(u4588,negated_conjecture,
    true = ifeq2(theme(skc14,X1,X0),true,theme(skc17,X1,X0),true) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : NLP247-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37  % Computer : n010.cluster.edu
% 0.11/0.37  % Model    : x86_64 x86_64
% 0.11/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37  % Memory   : 8046.5625MB
% 0.11/0.37  % OS       : Linux 6.8.0-71-generic
% 0.11/0.37  % CPULimit : 300
% 0.11/0.37  % WCLimit  : 300
% 0.11/0.37  % DateTime : Sun Sep 27 18:36:32 UTC 2026
% 0.11/0.37  % CPUTime  : 
% 0.11/0.37  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40  Running first-order theorem proving
% 0.11/0.40  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.53/2.68  % (1234815)Detected a unit-equality problem, will run specialized UEQ schedule.
% 12.53/2.68  % (1234824)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3653309336:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 12.53/2.68  % (1234823)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1565987897:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 12.53/2.68  % (1234825)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1353808969:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 12.53/2.68  % (1234822)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1805256980:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 12.53/2.68  % (1234820)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1061771661:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 12.53/2.68  % (1234821)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=572482207:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 12.53/2.68  % (1234826)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1946594343:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 12.53/2.68  % (1234824)Instruction limit reached! 
% 12.53/2.68  % (1234824)------------------------------
% 12.53/2.68  % (1234824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234824)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234824)Termination reason: Instruction limit
% 12.53/2.68  % (1234824)Termination phase: Saturation
% 12.53/2.68  % (1234824)Time elapsed: 0.057 s
% 12.53/2.68  % (1234824)Peak memory usage: 89 MB
% 12.53/2.68  % (1234824)Instructions burned: 183 (million)
% 12.53/2.68  % (1234823)Instruction limit reached! 
% 12.53/2.68  % (1234823)------------------------------
% 12.53/2.68  % (1234823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234823)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234823)Termination reason: Instruction limit
% 12.53/2.68  % (1234823)Termination phase: Saturation
% 12.53/2.68  % (1234823)Time elapsed: 0.073 s
% 12.53/2.68  % (1234823)Peak memory usage: 89 MB
% 12.53/2.68  % (1234823)Instructions burned: 136 (million)
% 12.53/2.68  % (1234834)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1805390562:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 12.53/2.68  % (1234825)Instruction limit reached! 
% 12.53/2.68  % (1234825)------------------------------
% 12.53/2.68  % (1234825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234825)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234825)Termination reason: Instruction limit
% 12.53/2.68  % (1234825)Termination phase: Saturation
% 12.53/2.68  % (1234825)Time elapsed: 0.147 s
% 12.53/2.68  % (1234825)Peak memory usage: 92 MB
% 12.53/2.68  % (1234825)Instructions burned: 257 (million)
% 12.53/2.68  % (1234835)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3029909108:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 12.53/2.68  % (1234837)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=4265170459:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 12.53/2.68  % (1234837)Instruction limit reached! 
% 12.53/2.68  % (1234837)------------------------------
% 12.53/2.68  % (1234837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234837)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234837)Termination reason: Instruction limit
% 12.53/2.68  % (1234837)Termination phase: Saturation
% 12.53/2.68  % (1234837)Time elapsed: 0.110 s
% 12.53/2.68  % (1234837)Peak memory usage: 93 MB
% 12.53/2.68  % (1234837)Instructions burned: 217 (million)
% 12.53/2.68  % (1234826)Refutation not found, incomplete strategy
% 12.53/2.68  % (1234826)------------------------------
% 12.53/2.68  % (1234826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234826)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234826)Termination reason: Refutation not found, incomplete strategy
% 12.53/2.68  % (1234826)Time elapsed: 0.490 s
% 12.53/2.68  % (1234826)Peak memory usage: 95 MB
% 12.53/2.68  % (1234826)Instructions burned: 893 (million)
% 12.53/2.68  % (1234840)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=642664924:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 12.53/2.68  % (1234840)Instruction limit reached! 
% 12.53/2.68  % (1234840)------------------------------
% 12.53/2.68  % (1234840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234840)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234840)Termination reason: Instruction limit
% 12.53/2.68  % (1234840)Termination phase: Saturation
% 12.53/2.68  % (1234840)Time elapsed: 0.160 s
% 12.53/2.68  % (1234840)Peak memory usage: 96 MB
% 12.53/2.68  % (1234840)Instructions burned: 319 (million)
% 12.53/2.68  % (1234826)------------------------------
% 12.53/2.68  % (1234826)------------------------------
% 12.53/2.68  % (1234842)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2593853580:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 12.53/2.68  % (1234843)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=939173814:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 12.53/2.68  % (1234834)Instruction limit reached! 
% 12.53/2.68  % (1234834)------------------------------
% 12.53/2.68  % (1234834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.53/2.68  % (1234834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.53/2.68  % (1234834)CaDiCaL version: 2.1.3
% 12.53/2.68  % (1234834)Termination reason: Instruction limit
% 12.53/2.68  % (1234834)Termination phase: Saturation
% 12.53/2.68  % (1234834)Time elapsed: 1.105 s
% 12.53/2.68  % (1234834)Peak memory usage: 140 MB
% 12.53/2.68  % (1234834)Instructions burned: 2052 (million)
% 12.53/2.68  % (1234846)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1591656154:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2986 on theBenchmark for (2986ds/14534Mi)
% 12.53/2.68  % (1234843)First to succeed.
% 12.53/2.68  % (1234843)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1234815"
% 12.53/2.68  % SZS status Satisfiable for theBenchmark
% 12.53/2.68  % SZS output start Saturation.
% See solution above
% 13.64/2.88  % SZS output start Definitions and Model Updates.
% 13.64/2.88  % SZS output end Definitions and Model Updates.
% 13.64/2.88  % (1234843)------------------------------
% 13.64/2.88  % (1234843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.88  % (1234843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.88  % (1234843)CaDiCaL version: 2.1.3
% 13.64/2.88  % (1234843)Termination reason: Satisfiable
% 13.64/2.88  % (1234843)Time elapsed: 0.575 s
% 13.64/2.88  % (1234843)Peak memory usage: 101 MB
% 13.64/2.88  % (1234843)Instructions burned: 976 (million)
% 13.64/2.88  % (1234843)------------------------------
% 13.64/2.88  % (1234843)------------------------------
% 13.64/2.88  % (1234815)Success in time 1.847 s
% 13.64/2.88  % Vampire exiting
%------------------------------------------------------------------------------