Vampire---5.0.1.SAT-Sat.s

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

% Computer : n017.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 9.92s 2.27s
% Output   : Saturation 10.56s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u2584,negated_conjecture,
    true = human(skc16,skc19) ).

cnf(u3062,negated_conjecture,
    b = ifeq(tuple(specific(skc16,skc24),true),sF35,a,b) ).

cnf(u248,negated_conjecture,
    true = sF8 ).

cnf(u1415,negated_conjecture,
    true = ifeq2(agent(X0,skc17,skc19),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u1911,negated_conjecture,
    b = ifeq(tuple(specific(skc13,skc24),true),sF35,a,b) ).

cnf(u1553,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,of(X0,skc20,skc19),true) ).

cnf(u8823,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,skc16,skc16),skc16),skc16),skc16) ).

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

cnf(u2387,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skc22),true) ).

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

cnf(u2340,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skc15),true,true,true),true) ).

cnf(u2330,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skc15),true) ).

cnf(u556,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc15),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u1786,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc19),true) ).

cnf(u1675,negated_conjecture,
    ifeq3(theme(skc13,skc17,X0),true,ifeq3(theme(skc13,X1,skc16),true,ifeq3(agent(skc13,X1,skc19),true,ifeq3(think_believe_consider(skc13,X1),true,ifeq3(proposition(skc13,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u535,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(vincent_forename(X0,skc20),true,true,true),true) ).

cnf(u906,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,smoke(X0,skc26),true) ).

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

cnf(u2273,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skc17),true) ).

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

cnf(u2691,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skf1(X1)),true,true,true),true) ).

cnf(u2613,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(male(X0,skc19),true,true,true),true) ).

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

cnf(u2825,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc23),true,true,true),true) ).

cnf(u5684,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,skc16,skc16),skc16),skc16) ).

cnf(u3134,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(forename(X0,skc24),true,true,true),true) ).

cnf(u404,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,event(X0,skc17),true) ).

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

cnf(u2344,negated_conjecture,
    true = specific(skc16,skc15) ).

cnf(u3127,negated_conjecture,
    ifeq3(of(skc16,X0,skc23),true,ifeq3(forename(skc16,X0),true,skc24,X0),X0) = X0 ).

cnf(u2246,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc15)),sF35,a,b) ).

cnf(u2079,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(living(X0,skc23),true,true,true),true) ).

cnf(u538,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,vincent_forename(X0,skc20),true) ).

cnf(u931,negated_conjecture,
    skc16 = ifeq3(agent(skc13,skc15,X0),true,ifeq3(agent(skc13,skc17,X0),true,skc16,skc16),skc16) ).

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

cnf(u293,negated_conjecture,
    true = sF23 ).

cnf(u423,negated_conjecture,
    true = ifeq2(man(skc13,X0),true,man(skc16,X0),true) ).

cnf(u2217,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,impartial(X0,skc23),true) ).

cnf(u3131,negated_conjecture,
    true = ifeq2(vincent_forename(skc16,skc24),true,true,true) ).

cnf(u7102,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u1947,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc24),true,true,true) ).

cnf(u2350,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u1900,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonhuman(X0,skc24),true,true,true),true) ).

cnf(u3120,negated_conjecture,
    true = forename(skc16,skc24) ).

cnf(u3054,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc24),true,true,true) ).

cnf(u6202,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skf1(skc19),X1),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u1424,negated_conjecture,
    true = male(skc13,skc19) ).

cnf(u2207,negated_conjecture,
    true = impartial(skc13,skc23) ).

cnf(u1447,negated_conjecture,
    true = ifeq2(agent(X0,skc15,skc19),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u1332,negated_conjecture,
    true = thing(skc13,skc15) ).

cnf(u2475,negated_conjecture,
    true = abstraction(skc16,skc16) ).

cnf(u421,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,man(X0,skc19),true) ).

cnf(u672,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,eventuality(X0,skc15),true) ).

cnf(u1967,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(abstraction(X0,skc16),true,true,true),true) ).

cnf(u2361,negated_conjecture,
    true = ifeq2(entity(skc16,skc15),true,true,true) ).

cnf(u444,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,forename(X0,skc24),true) ).

cnf(u4561,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,skc26,X1),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1336,negated_conjecture,
    true = ifeq2(entity(skc13,skc17),true,true,true) ).

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

cnf(u2750,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(human(X0,skc23),true,true,true),true) ).

cnf(u1861,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relation(X0,skc20),true) ).

cnf(u335,negated_conjecture,
    true = jules_forename(skc13,skc24) ).

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

cnf(u4683,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,X1,skc16),true,ifeq3(agent(skc16,X1,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1859,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relation(X0,skc20),true,true,true),true) ).

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

cnf(u2645,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(existent(X0,skc19),true,true,true),true) ).

cnf(u2232,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc22)),sF35,a,b) ).

cnf(u1865,negated_conjecture,
    true = human(skc13,skc23) ).

cnf(u4556,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X1),true,skc16,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u7082,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u613,negated_conjecture,
    ifeq3(theme(skc13,X0,X1),true,ifeq3(theme(skc13,skc15,X2),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,ifeq3(proposition(skc13,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2570,negated_conjecture,
    true = agent(skc16,skf1(skc19),skc19) ).

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

cnf(u1987,negated_conjecture,
    b = ifeq(tuple(specific(skc13,skc16),true),sF35,a,b) ).

cnf(u2773,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,male(X0,skc23),true) ).

cnf(u1349,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc22),true,true,true) ).

cnf(u1949,negated_conjecture,
    true = ifeq2(entity(skc13,skc24),true,true,true) ).

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

cnf(u323,negated_conjecture,
    true = sF33 ).

cnf(u2806,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,impartial(X0,skc23),true) ).

cnf(u461,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,agent(X0,skc15,skc19),true) ).

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

cnf(u3126,negated_conjecture,
    skc20 = ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X0),true,X0,skc20),skc20) ).

cnf(u66,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(smoke(X0,X2),true,smoke(X1,X2),true),true) ).

cnf(u1353,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc22),true) ).

cnf(u2388,negated_conjecture,
    true = eventuality(skc16,skc22) ).

cnf(u1245,negated_conjecture,
    ifeq3(of(skc13,X0,skc23),true,ifeq3(forename(skc13,X0),true,skc24,X0),X0) = X0 ).

cnf(u2178,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonexistent(X0,skc17),true,true,true),true) ).

cnf(u2647,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,existent(X0,skc19),true) ).

cnf(u3410,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,X1,X2),true,ifeq3(agent(skc16,X1,skc19),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2513,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(general(X0,skc16),true,true,true),true) ).

cnf(u868,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(proposition(skc13,X0),true,skc16,X0),X0) = X0 ).

cnf(u1134,negated_conjecture,
    skc16 = ifeq3(agent(skc13,skc15,X0),true,ifeq3(agent(skc13,skc15,X0),true,skc16,skc16),skc16) ).

cnf(u128,negated_conjecture,
    true = ifeq2(theme(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).

cnf(u2134,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc20),true) ).

cnf(u2261,negated_conjecture,
    true = ifeq2(event(skc13,skc26),true,true,true) ).

cnf(u344,negated_conjecture,
    true = man(skc13,skc19) ).

cnf(u2407,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skc22),true,true,true),true) ).

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

cnf(u2634,negated_conjecture,
    true = ifeq2(event(skc13,skf1(X0)),true,true,true) ).

cnf(u1481,negated_conjecture,
    ifeq3(theme(skc13,skc17,X0),true,ifeq3(theme(skc13,skc15,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u1884,negated_conjecture,
    true = abstraction(skc13,skc16) ).

cnf(u3430,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc15),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u3045,negated_conjecture,
    true = nonhuman(skc16,skc20) ).

cnf(u887,negated_conjecture,
    true = theme(skc13,skc15,skc16) ).

cnf(u5976,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skc15,X1),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2640,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skf1(X1)),true) ).

cnf(u2775,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(animate(X0,skc23),true,true,true),true) ).

cnf(u1882,negated_conjecture,
    true = abstraction(skc13,skc20) ).

cnf(u2657,negated_conjecture,
    true = singleton(skc16,skc19) ).

cnf(u3812,negated_conjecture,
    true = state(skc16,skc22) ).

cnf(u363,negated_conjecture,
    true = agent(skc13,skc17,skc19) ).

cnf(u3155,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relation(X0,skc24),true) ).

cnf(u350,negated_conjecture,
    true = think_believe_consider(skc13,skc15) ).

cnf(u2405,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc22),true,true,true) ).

cnf(u106,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(existent(X0,X2),true,existent(X1,X2),true),true) ).

cnf(u2723,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skf1(X1)),true,true,true),true) ).

cnf(u2285,negated_conjecture,
    true = unisex(skc16,skc17) ).

cnf(u4558,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skc26,X1),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1588,negated_conjecture,
    true = ifeq2(of(X0,skc24,skc23),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u6156,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,X1,skc16),true,ifeq3(agent(skc16,X1,skc19),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u361,negated_conjecture,
    true = of(skc13,skc20,skc19) ).

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

cnf(u1747,negated_conjecture,
    true = ifeq2(present(X0,skc15),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

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

cnf(u2799,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(living(X0,skc23),true,true,true),true) ).

cnf(u2418,negated_conjecture,
    true = ifeq2(entity(skc16,skc22),true,true,true) ).

cnf(u1796,negated_conjecture,
    true = existent(skc13,skc23) ).

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

cnf(u3076,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(general(X0,skc20),true,true,true),true) ).

cnf(u2362,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc15)),sF35,a,b) ).

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

cnf(u2562,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(man(X0,skc19),true,true,true),true) ).

cnf(u1044,negated_conjecture,
    true = ifeq2(vincent_forename(skc13,skc24),true,true,true) ).

cnf(u2172,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonexistent(X0,skc22),true,true,true),true) ).

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

cnf(u2046,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc22),true) ).

cnf(u1142,negated_conjecture,
    true = ifeq2(state(skc13,skc15),true,true,true) ).

cnf(u2568,negated_conjecture,
    true = present(skc16,skf1(X0)) ).

cnf(u3046,negated_conjecture,
    true = thing(skc16,skc20) ).

cnf(u1005,negated_conjecture,
    true = ifeq2(relation(skc13,X0),true,relation(skc16,X0),true) ).

cnf(u3194,negated_conjecture,
    true = ifeq2(accessible_world(skc16,skc16),true,true,true) ).

cnf(u3321,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc26),true,true,true) ).

cnf(u1924,negated_conjecture,
    true = unisex(skc13,skc20) ).

cnf(u2713,negated_conjecture,
    true = singleton(skc16,skf1(X0)) ).

cnf(u3052,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonhuman(X0,skc20),true) ).

cnf(u1003,negated_conjecture,
    true = ifeq2(nonexistent(skc13,X0),true,nonexistent(skc16,X0),true) ).

cnf(u5,negated_conjecture,
    true = ifeq2(smoke(X0,X1),true,event(X0,X1),true) ).

cnf(u911,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,theme(X0,skc15,skc16),true) ).

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

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

cnf(u540,negated_conjecture,
    true = ifeq2(vincent_forename(skc13,X0),true,vincent_forename(skc16,X0),true) ).

cnf(u2050,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc17)),sF35,a,b) ).

cnf(u3057,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skc24),true,true,true),true) ).

cnf(u260,negated_conjecture,
    true = sF12 ).

cnf(u2696,negated_conjecture,
    true = thing(skc16,skf1(X0)) ).

cnf(u1311,negated_conjecture,
    skc24 = ifeq3(of(skc13,skc20,skc23),true,skc20,skc24) ).

cnf(u1018,negated_conjecture,
    true = ifeq2(jules_forename(skc13,skc20),true,true,true) ).

cnf(u2299,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skc17),true,true,true),true) ).

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

cnf(u662,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,eventuality(X0,skc17),true) ).

cnf(clause70,negated_conjecture,
    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(u896,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,present(X0,skc26),true) ).

cnf(u2852,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,X1,X2),true,ifeq3(agent(skc16,X1,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1025,negated_conjecture,
    true = ifeq2(nonhuman(skc13,X0),true,nonhuman(skc16,X0),true) ).

cnf(u917,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,X1,X2),true,ifeq3(agent(skc16,X1,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2328,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skc15),true,true,true),true) ).

cnf(u2318,negated_conjecture,
    true = singleton(skc16,skc17) ).

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

cnf(u2100,negated_conjecture,
    true = singleton(skc13,skc24) ).

cnf(u1410,negated_conjecture,
    true = agent(skc16,skc15,skc19) ).

cnf(u3100,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc20),true) ).

cnf(u2331,negated_conjecture,
    true = eventuality(skc16,skc15) ).

cnf(u45,negated_conjecture,
    true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).

cnf(u1933,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonhuman(X0,skc20),true) ).

cnf(u407,negated_conjecture,
    true = ifeq2(event(skc13,X0),true,event(skc16,X0),true) ).

cnf(u2074,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(living(X0,skc19),true,true,true),true) ).

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

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

cnf(u6867,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skc26),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2699,negated_conjecture,
    true = ifeq2(abstraction(skc16,skf1(X0)),true,true,true) ).

cnf(u3104,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc20),true,true,true),true) ).

cnf(u559,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,think_believe_consider(X0,skc15),true) ).

cnf(u2097,negated_conjecture,
    true = singleton(skc13,skc19) ).

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

cnf(u1937,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc20),true,true,true),true) ).

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

cnf(u2606,negated_conjecture,
    true = impartial(skc16,skc19) ).

cnf(u296,negated_conjecture,
    true = sF24 ).

cnf(u2352,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skc15),true) ).

cnf(u656,negated_conjecture,
    true = eventuality(skc13,skc15) ).

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

cnf(u290,negated_conjecture,
    true = sF22 ).

cnf(u2345,negated_conjecture,
    true = thing(skc16,skc15) ).

cnf(u2612,negated_conjecture,
    b = ifeq(tuple(unisex(skc16,skc19),true),sF35,a,b) ).

cnf(u3092,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc24),true) ).

cnf(u3731,negated_conjecture,
    true = vincent_forename(skc16,skc20) ).

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

cnf(u1320,negated_conjecture,
    skc20 = ifeq3(of(skc13,skc24,skc19),true,skc24,skc20) ).

cnf(u1849,negated_conjecture,
    true = relation(skc13,skc20) ).

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

cnf(u3737,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,vincent_forename(X0,skc20),true) ).

cnf(u6051,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(theme(skc16,skc17,X1),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u2358,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skc15),true) ).

cnf(u317,negated_conjecture,
    true = sF31 ).

cnf(u1826,negated_conjecture,
    true = ifeq2(theme(X0,skc15,skc16),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

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

cnf(u1037,negated_conjecture,
    true = ifeq2(human(skc13,X0),true,human(skc16,X0),true) ).

cnf(u1193,negated_conjecture,
    skc20 = skc18 ).

cnf(u1971,negated_conjecture,
    true = nonhuman(skc13,skc16) ).

cnf(u6978,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u1333,negated_conjecture,
    true = thing(skc13,skc17) ).

cnf(u2864,negated_conjecture,
    skc24 = ifeq3(of(skc13,skc20,X0),true,ifeq3(of(skc13,skc24,X0),true,ifeq3(entity(skc13,X0),true,skc20,skc24),skc24),skc24) ).

cnf(u8762,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,skf1(skc23),X1),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1837,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(animate(X0,skc19),true,true,true),true) ).

cnf(u2627,negated_conjecture,
    true = thing(skc16,skc19) ).

cnf(u1922,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(abstraction(X0,skc20),true,true,true),true) ).

cnf(u2486,negated_conjecture,
    true = nonhuman(skc16,skc16) ).

cnf(u2586,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(smoke(X0,skf1(X1)),true,true,true),true) ).

cnf(u2119,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc22),true) ).

cnf(u2592,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(human(X0,skc19),true,true,true),true) ).

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

cnf(u3695,negated_conjecture,
    true = ifeq2(specific(skc13,skc26),true,true,true) ).

cnf(u2630,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(animate(X0,skc19),true,true,true),true) ).

cnf(u3775,negated_conjecture,
    skc20 = ifeq3(of(skc16,skc20,skc23),true,skc24,skc20) ).

cnf(u2129,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc23),true) ).

cnf(u1356,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc26),true,true,true) ).

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

cnf(u2117,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc22),true,true,true),true) ).

cnf(u2112,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc19),true,true,true),true) ).

cnf(u2247,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u330,negated_conjecture,
    b = ifeq(tuple(specific(X0,X1),general(X0,X1)),sF35,a,b) ).

cnf(u3056,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc24)),sF35,a,b) ).

cnf(u2745,negated_conjecture,
    true = organism(skc16,skc23) ).

cnf(u1091,negated_conjecture,
    skc16 = ifeq3(agent(skc13,skc17,X0),true,ifeq3(agent(skc13,skc15,X0),true,skc16,skc16),skc16) ).

cnf(u2758,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(organism(X0,skc23),true,true,true),true) ).

cnf(u1360,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc26),true) ).

cnf(u2722,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skf1(X0))),sF35,a,b) ).

cnf(u6729,negated_conjecture,
    skc20 = ifeq3(of(skc16,skc20,X0),true,ifeq3(of(skc16,skc20,X0),true,ifeq3(entity(skc16,X0),true,skc20,skc20),skc20),skc20) ).

cnf(u1711,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,skc16,skc16),skc16),skc16) ).

cnf(u6870,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,skc26,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u3090,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc24),true,true,true),true) ).

cnf(u328,axiom,
    tuple(true,true) = sF35 ).

cnf(u458,negated_conjecture,
    true = ifeq2(agent(X0,skc15,skc19),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

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

cnf(u2746,negated_conjecture,
    true = animate(skc16,skc23) ).

cnf(u1868,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc13,skc19),true),sF35,a,b) ).

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

cnf(u3029,negated_conjecture,
    b = ifeq(tuple(true,human(skc16,skc24)),sF35,a,b) ).

cnf(u2624,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,entity(X0,skc19),true) ).

cnf(u1866,negated_conjecture,
    true = human(skc13,skc19) ).

cnf(u2641,negated_conjecture,
    true = eventuality(skc16,skf1(X0)) ).

cnf(u3796,negated_conjecture,
    skc24 = ifeq3(of(skc16,skc24,skc19),true,skc20,skc24) ).

cnf(u347,negated_conjecture,
    true = event(skc13,skc17) ).

cnf(u1839,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,animate(X0,skc19),true) ).

cnf(u3166,negated_conjecture,
    skc20 = ifeq3(of(skc16,X0,X1),true,ifeq3(of(skc16,skc20,X1),true,ifeq3(forename(skc16,X0),true,ifeq3(entity(skc16,X1),true,X0,skc20),skc20),skc20),skc20) ).

cnf(u1990,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,general(X0,skc16),true) ).

cnf(u1533,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,be(X0,skc22,skc23,skc23),true) ).

cnf(u1239,negated_conjecture,
    skc20 = ifeq3(of(skc13,skc20,skc23),true,skc24,skc20) ).

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

cnf(u2132,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc20),true,true,true),true) ).

cnf(u3542,negated_conjecture,
    true = ifeq2(unisex(skc13,skc26),true,true,true) ).

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

cnf(u2415,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skc22),true) ).

cnf(u3042,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,abstraction(X0,skc20),true) ).

cnf(u2752,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,human(X0,skc23),true) ).

cnf(u1994,negated_conjecture,
    true = ifeq2(entity(skc13,skc16),true,true,true) ).

cnf(u8401,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X1),true,skc16,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1244,negated_conjecture,
    skc24 = ifeq3(of(skc13,X0,skc23),true,ifeq3(forename(skc13,X0),true,X0,skc24),skc24) ).

cnf(u1902,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonhuman(X0,skc24),true) ).

cnf(u462,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,agent(X0,skc17,skc19),true) ).

cnf(u88,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(relation(X0,X2),true,relation(X1,X2),true),true) ).

cnf(u2402,negated_conjecture,
    true = thing(skc16,skc22) ).

cnf(u3177,negated_conjecture,
    true = relation(skc16,skc20) ).

cnf(u1908,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc24),true) ).

cnf(u4587,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u2174,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonexistent(X0,skc22),true) ).

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

cnf(u2413,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skc22),true,true,true),true) ).

cnf(u3432,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,think_believe_consider(X0,skc15),true) ).

cnf(u2674,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc19)),sF35,a,b) ).

cnf(u3167,negated_conjecture,
    ifeq3(of(skc16,skc20,X0),true,ifeq3(of(skc16,X1,X0),true,ifeq3(forename(skc16,X1),true,ifeq3(entity(skc16,X0),true,skc20,X1),X1),X1),X1) = X1 ).

cnf(u4560,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,skc26,X1),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u3075,negated_conjecture,
    b = ifeq(tuple(specific(skc16,skc20),true),sF35,a,b) ).

cnf(u3030,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonhuman(X0,skc24),true,true,true),true) ).

cnf(u1789,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc23)),sF35,a,b) ).

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

cnf(u2171,negated_conjecture,
    b = ifeq(tuple(true,existent(skc13,skc22)),sF35,a,b) ).

cnf(u439,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(forename(X0,skc20),true,true,true),true) ).

cnf(u1805,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc13,skc23),true),sF35,a,b) ).

cnf(u8405,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,X1,skc16),true,ifeq3(agent(skc16,X1,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u257,negated_conjecture,
    true = sF11 ).

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

cnf(u2711,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skf1(X1)),true) ).

cnf(u2284,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skc17),true) ).

cnf(u3978,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,skc17,X1),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(agent(skc13,skc17,X2),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2057,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc15)),sF35,a,b) ).

cnf(u6765,negated_conjecture,
    skc20 = ifeq3(of(skc16,skc20,skc23),true,ifeq3(of(skc16,skc20,skc23),true,skc20,skc20),skc20) ).

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

cnf(u1931,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonhuman(X0,skc20),true,true,true),true) ).

cnf(u1531,negated_conjecture,
    true = ifeq2(be(X0,skc22,skc23,skc23),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u2830,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skf1(X1)),true,true,true),true) ).

cnf(u2787,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,entity(X0,skc23),true) ).

cnf(u1518,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,skc17,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u245,negated_conjecture,
    true = sF7 ).

cnf(u1008,negated_conjecture,
    true = ifeq2(smoke(skc13,skc15),true,true,true) ).

cnf(u263,negated_conjecture,
    true = sF13 ).

cnf(u2554,negated_conjecture,
    true = man(skc16,skc19) ).

cnf(u385,negated_conjecture,
    skc20 = ifeq3(of(skc13,X0,X1),true,ifeq3(of(skc13,skc20,X1),true,ifeq3(forename(skc13,X0),true,ifeq3(entity(skc13,X1),true,X0,skc20),skc20),skc20),skc20) ).

cnf(u3701,negated_conjecture,
    true = ifeq2(specific(skc13,skf1(X0)),true,true,true) ).

cnf(u3102,negated_conjecture,
    true = singleton(skc16,skc20) ).

cnf(u2283,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skc17),true,true,true),true) ).

cnf(u1790,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc23),true,true,true),true) ).

cnf(u901,negated_conjecture,
    true = ifeq2(agent(X0,skc26,skc23),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u1544,negated_conjecture,
    true = of(skc16,skc24,skc23) ).

cnf(u1423,negated_conjecture,
    true = male(skc13,skc23) ).

cnf(u4599,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0) = X0 ).

cnf(u3041,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(abstraction(X0,skc20),true,true,true),true) ).

cnf(u6393,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(theme(skc16,skc15,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u3084,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc24),true,true,true),true) ).

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

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

cnf(u2498,negated_conjecture,
    true = ifeq2(entity(skc16,skc16),true,true,true) ).

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

cnf(u512,negated_conjecture,
    true = ifeq2(jules_forename(skc13,X0),true,jules_forename(skc16,X0),true) ).

cnf(u2058,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc15),true,true,true),true) ).

cnf(u284,negated_conjecture,
    true = sF20 ).

cnf(u3293,negated_conjecture,
    skc20 = ifeq3(of(skc13,X0,skc23),true,ifeq3(of(skc13,skc20,skc23),true,ifeq3(forename(skc13,X0),true,X0,skc20),skc20),skc20) ).

cnf(u2043,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc22)),sF35,a,b) ).

cnf(clause71,negated_conjecture,
    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(u3088,negated_conjecture,
    true = singleton(skc16,skc24) ).

cnf(u2081,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,living(X0,skc23),true) ).

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

cnf(u2326,negated_conjecture,
    true = ifeq2(smoke(skc16,skc15),true,true,true) ).

cnf(u2579,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(human_person(X0,skc19),true,true,true),true) ).

cnf(u19,negated_conjecture,
    true = ifeq2(proposition(X0,X1),true,relation(X0,X1),true) ).

cnf(u2515,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,general(X0,skc16),true) ).

cnf(u640,negated_conjecture,
    true = ifeq2(abstraction(skc13,X0),true,abstraction(skc16,X0),true) ).

cnf(u2186,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonexistent(X0,skc15),true) ).

cnf(u657,negated_conjecture,
    true = eventuality(skc13,skc17) ).

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

cnf(u2827,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc23),true) ).

cnf(u1173,negated_conjecture,
    true = organism(skc13,skc19) ).

cnf(u2072,negated_conjecture,
    true = living(skc13,skc19) ).

cnf(u6441,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(theme(skc16,skc17,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u1154,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(eventuality(X0,skc22),true,true,true),true) ).

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

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

cnf(u2342,negated_conjecture,
    true = unisex(skc16,skc15) ).

cnf(u1957,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc20),true,true,true),true) ).

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

cnf(u3735,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(vincent_forename(X0,skc20),true,true,true),true) ).

cnf(u2842,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skf1(skc19),skc19),true) ).

cnf(u1435,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,male(X0,skc23),true) ).

cnf(u2837,negated_conjecture,
    true = ifeq2(agent(skc13,skf1(skc19),skc19),true,true,true) ).

cnf(u918,negated_conjecture,
    ifeq3(theme(skc13,X0,X1),true,ifeq3(agent(skc13,X0,X2),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,skc16,X1),X1),X1),X1),X1) = X1 ).

cnf(u1906,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc24),true,true,true),true) ).

cnf(u1432,negated_conjecture,
    b = ifeq(tuple(unisex(skc13,skc23),true),sF35,a,b) ).

cnf(u815,negated_conjecture,
    true = ifeq2(specific(skc13,X0),true,specific(skc16,X0),true) ).

cnf(u2804,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(impartial(X0,skc23),true,true,true),true) ).

cnf(u59,negated_conjecture,
    true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).

cnf(u2861,negated_conjecture,
    ifeq3(of(skc13,skc20,skc23),true,ifeq3(of(skc13,X0,skc23),true,ifeq3(forename(skc13,X0),true,skc20,X0),X0),X0) = X0 ).

cnf(u429,negated_conjecture,
    true = ifeq2(be(skc13,X0,X1,X2),true,be(skc16,X0,X1,X2),true) ).

cnf(u2096,negated_conjecture,
    true = singleton(skc13,skc17) ).

cnf(u1975,negated_conjecture,
    b = ifeq(tuple(true,human(skc13,skc16)),sF35,a,b) ).

cnf(u314,negated_conjecture,
    true = sF30 ).

cnf(u2356,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skc15),true,true,true),true) ).

cnf(u1075,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,X1),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,skc16),skc16),skc16),skc16) ).

cnf(u2655,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc19),true) ).

cnf(u4541,negated_conjecture,
    skc20 = ifeq3(of(skc13,skc20,skc23),true,ifeq3(of(skc13,skc20,skc23),true,skc20,skc20),skc20) ).

cnf(u4653,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u2615,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,male(X0,skc19),true) ).

cnf(u1426,negated_conjecture,
    b = ifeq(tuple(unisex(skc13,skc19),true),sF35,a,b) ).

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

cnf(u8873,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u419,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(man(X0,skc23),true,true,true),true) ).

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

cnf(u2229,negated_conjecture,
    true = unisex(skc13,skc17) ).

cnf(u442,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,forename(X0,skc20),true) ).

cnf(u2512,negated_conjecture,
    b = ifeq(tuple(specific(skc16,skc16),true),sF35,a,b) ).

cnf(u2602,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,organism(X0,skc19),true) ).

cnf(u1449,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skc15,skc19),true) ).

cnf(u2484,negated_conjecture,
    true = unisex(skc16,skc16) ).

cnf(u1344,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u2644,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc16,skc19),true),sF35,a,b) ).

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

cnf(u1850,negated_conjecture,
    true = relation(skc13,skc24) ).

cnf(u1427,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(male(X0,skc19),true,true,true),true) ).

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

cnf(u684,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(human_person(X0,skc23),true,true,true),true) ).

cnf(u2375,negated_conjecture,
    true = singleton(skc16,skc15) ).

cnf(u84,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,X1),true,ifeq2(accessible_world(X0,X2),true,think_believe_consider(X2,X1),true),true) ).

cnf(u2142,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc16),true,true,true),true) ).

cnf(u2849,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc23),skc23),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u3013,negated_conjecture,
    true = abstraction(skc16,skc24) ).

cnf(u2736,negated_conjecture,
    true = agent(skc16,skf1(skc23),skc23) ).

cnf(u1978,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonhuman(X0,skc16),true) ).

cnf(u2625,negated_conjecture,
    true = existent(skc16,skc19) ).

cnf(u331,negated_conjecture,
    b = ifeq(tuple(nonhuman(X0,X1),human(X0,X1)),sF35,a,b) ).

cnf(u446,negated_conjecture,
    true = ifeq2(forename(skc13,X0),true,forename(skc16,X0),true) ).

cnf(u2373,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc15),true) ).

cnf(u2503,negated_conjecture,
    true = singleton(skc16,skc16) ).

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

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

cnf(u2215,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(impartial(X0,skc23),true,true,true),true) ).

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

cnf(u2253,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc26)),sF35,a,b) ).

cnf(u2399,negated_conjecture,
    true = unisex(skc16,skc22) ).

cnf(u3026,negated_conjecture,
    true = thing(skc16,skc24) ).

cnf(u3138,negated_conjecture,
    ifeq3(of(skc16,skc24,X0),true,ifeq3(of(skc16,X1,X0),true,ifeq3(forename(skc16,X1),true,ifeq3(entity(skc16,X0),true,skc24,X1),X1),X1),X1) = X1 ).

cnf(u329,negated_conjecture,
    b = ifeq(tuple(unisex(X0,X1),male(X0,X1)),sF35,a,b) ).

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

cnf(u644,negated_conjecture,
    true = ifeq2(organism(skc13,X0),true,organism(skc16,X0),true) ).

cnf(u3941,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,skc15,X1),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u352,negated_conjecture,
    true = event(skc13,skc15) ).

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

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

cnf(u2184,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonexistent(X0,skc15),true,true,true),true) ).

cnf(u3161,negated_conjecture,
    true = ifeq2(jules_forename(skc16,skc20),true,true,true) ).

cnf(u1892,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,abstraction(X0,skc24),true) ).

cnf(u1783,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc19)),sF35,a,b) ).

cnf(u2397,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skc22),true,true,true),true) ).

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

cnf(u457,negated_conjecture,
    true = ifeq2(agent(X0,skc17,skc19),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u1912,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(general(X0,skc24),true,true,true),true) ).

cnf(u3181,negated_conjecture,
    true = ifeq2(proposition(skc16,skc20),true,true,true) ).

cnf(u1896,negated_conjecture,
    true = thing(skc13,skc24) ).

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

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

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

cnf(u2749,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc16,skc23),true),sF35,a,b) ).

cnf(u8918,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u3070,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skc20),true,true,true),true) ).

cnf(u4312,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u2786,negated_conjecture,
    ifeq3(of(skc16,X0,skc23),true,ifeq3(of(skc16,X1,skc23),true,ifeq3(forename(skc16,X0),true,ifeq3(forename(skc16,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u2496,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc16),true,true,true) ).

cnf(u636,negated_conjecture,
    true = ifeq2(eventuality(skc13,X0),true,eventuality(skc16,X0),true) ).

cnf(u1738,negated_conjecture,
    true = ifeq2(present(skc13,skc26),true,true,true) ).

cnf(u3025,negated_conjecture,
    true = nonhuman(skc16,skc24) ).

cnf(u2268,negated_conjecture,
    true = ifeq2(state(skc16,skc17),true,true,true) ).

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

cnf(u4309,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,skc15,X1),true,ifeq3(agent(skc16,X0,X1),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16) ).

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

cnf(u615,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,X1,X2),true,ifeq3(agent(skc13,X1,skc19),true,ifeq3(think_believe_consider(skc13,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).

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

cnf(u883,negated_conjecture,
    true = smoke(skc16,skc26) ).

cnf(u427,negated_conjecture,
    true = ifeq2(be(X0,skc22,skc23,skc23),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u3942,negated_conjecture,
    ifeq3(theme(skc13,skc17,X0),true,ifeq3(theme(skc13,skc15,X1),true,ifeq3(agent(skc13,skc17,X2),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2682,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc19),true) ).

cnf(u2169,negated_conjecture,
    true = nonexistent(skc13,skc17) ).

cnf(u2820,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc23),true,true,true),true) ).

cnf(u3086,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc24),true) ).

cnf(u1899,negated_conjecture,
    b = ifeq(tuple(true,human(skc13,skc24)),sF35,a,b) ).

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

cnf(u1013,negated_conjecture,
    true = ifeq2(singleton(skc13,X0),true,singleton(skc16,X0),true) ).

cnf(u8406,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(theme(skc16,X1,skc16),true,ifeq3(agent(skc16,X1,skc19),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2482,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(abstraction(X0,skc16),true,true,true),true) ).

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

cnf(u1905,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc24)),sF35,a,b) ).

cnf(u1780,negated_conjecture,
    true = specific(skc13,skc23) ).

cnf(u6643,negated_conjecture,
    skc24 = ifeq3(of(skc16,skc24,X0),true,ifeq3(of(skc16,skc24,X0),true,ifeq3(entity(skc16,X0),true,skc24,skc24),skc24),skc24) ).

cnf(u1286,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc23),true,true,true) ).

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

cnf(u3083,negated_conjecture,
    true = ifeq2(entity(skc16,skc24),true,true,true) ).

cnf(u2430,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc22),true) ).

cnf(u1029,negated_conjecture,
    true = ifeq2(relname(skc13,X0),true,relname(skc16,X0),true) ).

cnf(u3072,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skc20),true) ).

cnf(u1290,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc23),true) ).

cnf(u2065,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc26),true,true,true),true) ).

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

cnf(u8469,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u4604,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0) = X0 ).

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

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

cnf(u2565,negated_conjecture,
    true = human_person(skc16,skc19) ).

cnf(u287,negated_conjecture,
    true = sF21 ).

cnf(u1984,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc16),true) ).

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

cnf(u1033,negated_conjecture,
    true = ifeq2(animate(skc13,X0),true,animate(skc16,X0),true) ).

cnf(u3870,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(theme(skc13,X1,skc16),true,ifeq3(agent(skc13,X0,X2),true,ifeq3(agent(skc13,X1,X2),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(think_believe_consider(skc13,X1),true,skc16,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u1852,negated_conjecture,
    true = ifeq2(proposition(skc13,skc24),true,true,true) ).

cnf(u1288,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc23),true,true,true),true) ).

cnf(u530,negated_conjecture,
    true = ifeq2(smoke(skc13,X0),true,smoke(skc16,X0),true) ).

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

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

cnf(u2566,negated_conjecture,
    true = male(skc16,skc19) ).

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

cnf(u2448,negated_conjecture,
    true = proposition(skc16,skc16) ).

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

cnf(u1039,negated_conjecture,
    true = ifeq2(male(skc13,X0),true,male(skc16,X0),true) ).

cnf(u2708,negated_conjecture,
    true = ifeq2(entity(skc16,skf1(X0)),true,true,true) ).

cnf(u1939,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc20),true) ).

cnf(u6814,negated_conjecture,
    ifeq3(of(skc16,skc24,skc19),true,ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X0),true,skc24,X0),X0),X0) = X0 ).

cnf(u2725,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skf1(X1)),true) ).

cnf(u3067,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc20),true,true,true) ).

cnf(u6534,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u7977,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skf1(skc23),X1),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2832,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skf1(X1)),true) ).

cnf(u1945,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,general(X0,skc20),true) ).

cnf(u43,negated_conjecture,
    true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).

cnf(u8725,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(theme(skc16,skf1(skc19),X1),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u275,negated_conjecture,
    true = sF17 ).

cnf(u413,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,event(X0,skc15),true) ).

cnf(u1959,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc20),true) ).

cnf(u384,negated_conjecture,
    ifeq3(of(skc13,skc20,X0),true,ifeq3(of(skc13,X1,X0),true,ifeq3(forename(skc13,X1),true,ifeq3(entity(skc13,X0),true,skc20,X1),X1),X1),X1) = X1 ).

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

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

cnf(u3630,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,jules_forename(X0,skc24),true) ).

cnf(u1197,negated_conjecture,
    skc24 = ifeq3(of(skc13,skc24,skc19),true,skc20,skc24) ).

cnf(u1328,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc19),true,true,true) ).

cnf(u1429,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,male(X0,skc19),true) ).

cnf(u927,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skc26),true,true,true),true) ).

cnf(u1178,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,organism(X0,skc19),true) ).

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

cnf(u1172,negated_conjecture,
    true = organism(skc13,skc23) ).

cnf(u403,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(event(X0,skc17),true,true,true),true) ).

cnf(u2208,negated_conjecture,
    true = impartial(skc13,skc19) ).

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

cnf(u7737,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,skc15,X0),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2139,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc26),true) ).

cnf(u3873,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,X1,skc16),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(agent(skc13,X1,X2),true,ifeq3(think_believe_consider(skc13,X1),true,ifeq3(proposition(skc13,X0),true,skc16,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u555,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc17),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

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

cnf(u2109,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc15),true) ).

cnf(u548,negated_conjecture,
    true = ifeq2(theme(skc13,X0,X1),true,theme(skc16,X0,X1),true) ).

cnf(u5979,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(theme(skc16,skc15,X1),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u1176,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(organism(X0,skc19),true,true,true),true) ).

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

cnf(u1834,negated_conjecture,
    true = animate(skc13,skc23) ).

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

cnf(u302,negated_conjecture,
    true = sF26 ).

cnf(u8942,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2487,negated_conjecture,
    true = thing(skc16,skc16) ).

cnf(u3059,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skc24),true) ).

cnf(u1331,negated_conjecture,
    true = thing(skc13,skc22) ).

cnf(u8631,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skf1(skc19),X1),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u2822,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc23),true) ).

cnf(u1800,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(existent(X0,skc19),true,true,true),true) ).

cnf(u2621,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(entity(X0,skc19),true,true,true),true) ).

cnf(u2210,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(impartial(X0,skc19),true,true,true),true) ).

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

cnf(u430,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,be(X0,skc22,skc23,skc23),true) ).

cnf(u2485,negated_conjecture,
    true = general(skc16,skc16) ).

cnf(u567,negated_conjecture,
    true = ifeq2(state(skc13,X0),true,state(skc16,X0),true) ).

cnf(u3078,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,general(X0,skc20),true) ).

cnf(u1226,negated_conjecture,
    true = entity(skc13,skc23) ).

cnf(u2228,negated_conjecture,
    true = unisex(skc13,skc15) ).

cnf(u364,negated_conjecture,
    true = agent(skc13,skc15,skc19) ).

cnf(u2383,negated_conjecture,
    true = ifeq2(smoke(skc16,skc22),true,true,true) ).

cnf(u4685,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,skc15,X1),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1594,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,of(X0,skc24,skc23),true) ).

cnf(u2168,negated_conjecture,
    true = nonexistent(skc13,skc15) ).

cnf(u4687,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,skf1(skc23),X1),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u336,negated_conjecture,
    true = forename(skc13,skc24) ).

cnf(u3063,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(general(X0,skc24),true,true,true),true) ).

cnf(u1351,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc22),true,true,true),true) ).

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

cnf(u2422,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc22),true) ).

cnf(u1501,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(theme(skc13,skc17,X1),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,skc16),skc16),skc16),skc16),skc16) ).

cnf(u381,negated_conjecture,
    true = ifeq2(proposition(skc13,X0),true,proposition(skc16,X0),true) ).

cnf(u3400,negated_conjecture,
    true = think_believe_consider(skc16,skc15) ).

cnf(u593,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,X1,X2),true,ifeq3(agent(skc13,skc15,X3),true,ifeq3(agent(skc13,X1,X3),true,ifeq3(think_believe_consider(skc13,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1874,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc13,skc23),true),sF35,a,b) ).

cnf(u2124,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc24),true) ).

cnf(u342,negated_conjecture,
    true = forename(skc13,skc20) ).

cnf(u3146,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relname(X0,skc24),true) ).

cnf(u1371,negated_conjecture,
    skc16 = ifeq3(theme(skc13,skc15,X0),true,ifeq3(agent(skc13,skc15,X1),true,ifeq3(agent(skc13,skc15,X1),true,ifeq3(proposition(skc13,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u614,negated_conjecture,
    ifeq3(theme(skc13,X0,X1),true,ifeq3(theme(skc13,skc17,X2),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,ifeq3(proposition(skc13,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

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

cnf(u1358,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc26),true,true,true),true) ).

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

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

cnf(u2770,negated_conjecture,
    b = ifeq(tuple(unisex(skc16,skc23),true),sF35,a,b) ).

cnf(u353,negated_conjecture,
    true = accessible_world(skc13,skc16) ).

cnf(u371,negated_conjecture,
    skc24 = ifeq3(of(skc13,X0,X1),true,ifeq3(of(skc13,skc24,X1),true,ifeq3(forename(skc13,X0),true,ifeq3(entity(skc13,X1),true,X0,skc24),skc24),skc24),skc24) ).

cnf(u1739,negated_conjecture,
    true = present(skc16,skc15) ).

cnf(u470,negated_conjecture,
    true = ifeq2(of(X0,skc20,skc19),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u1968,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,abstraction(X0,skc16),true) ).

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

cnf(u3023,negated_conjecture,
    true = unisex(skc16,skc24) ).

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

cnf(u2653,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc19),true,true,true),true) ).

cnf(u8024,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u359,negated_conjecture,
    true = of(skc13,skc24,skc23) ).

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

cnf(u8965,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u1883,negated_conjecture,
    true = abstraction(skc13,skc24) ).

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

cnf(u4325,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16) ).

cnf(u224,negated_conjecture,
    true = sF0 ).

cnf(u1519,negated_conjecture,
    ifeq3(theme(skc13,skc17,X0),true,ifeq3(theme(skc13,skc17,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u882,negated_conjecture,
    true = present(skc16,skc26) ).

cnf(u2666,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X1),true,present(X1,skf1(X0)),true) ).

cnf(u4500,negated_conjecture,
    skc24 = ifeq3(of(skc13,skc24,skc19),true,ifeq3(of(skc13,skc24,skc19),true,skc24,skc24),skc24) ).

cnf(u5995,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skc15,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u1398,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relname(X0,skc24),true,true,true),true) ).

cnf(u1781,negated_conjecture,
    true = specific(skc13,skc19) ).

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

cnf(u357,negated_conjecture,
    true = state(skc13,skc22) ).

cnf(u1784,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc19),true,true,true),true) ).

cnf(u230,negated_conjecture,
    true = sF2 ).

cnf(u1141,negated_conjecture,
    true = ifeq2(state(skc13,skc17),true,true,true) ).

cnf(u3184,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relation(X0,skc20),true) ).

cnf(u3065,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,general(X0,skc24),true) ).

cnf(u2271,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skc17),true,true,true),true) ).

cnf(u8802,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u1396,negated_conjecture,
    true = relname(skc13,skc24) ).

cnf(u3443,negated_conjecture,
    true = ifeq2(nonexistent(skc13,skf1(X0)),true,true,true) ).

cnf(u660,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(eventuality(X0,skc17),true,true,true),true) ).

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

cnf(u3137,negated_conjecture,
    skc24 = ifeq3(of(skc16,X0,X1),true,ifeq3(of(skc16,skc24,X1),true,ifeq3(forename(skc16,X0),true,ifeq3(entity(skc16,X1),true,X0,skc24),skc24),skc24),skc24) ).

cnf(u370,negated_conjecture,
    ifeq3(of(skc13,skc24,X0),true,ifeq3(of(skc13,X1,X0),true,ifeq3(forename(skc13,X1),true,ifeq3(entity(skc13,X0),true,skc24,X1),X1),X1),X1) = X1 ).

cnf(u2564,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,man(X0,skc19),true) ).

cnf(u2581,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,human_person(X0,skc19),true) ).

cnf(u886,negated_conjecture,
    true = agent(skc16,skc26,skc23) ).

cnf(u1269,negated_conjecture,
    true = thing(skc13,skc19) ).

cnf(u1400,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relname(X0,skc24),true) ).

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

cnf(u1223,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(organism(X0,skc23),true,true,true),true) ).

cnf(u3817,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(state(X0,skc22),true,true,true),true) ).

cnf(u892,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skc26),true,true,true),true) ).

cnf(u2814,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,thing(X0,skc23),true) ).

cnf(u269,negated_conjecture,
    true = sF15 ).

cnf(u2064,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc26)),sF35,a,b) ).

cnf(u2071,negated_conjecture,
    true = living(skc13,skc23) ).

cnf(u1151,negated_conjecture,
    true = eventuality(skc13,skc22) ).

cnf(u498,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,of(X0,skc24,skc23),true) ).

cnf(u2553,negated_conjecture,
    true = man(skc16,skc23) ).

cnf(u2692,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skf1(X1)),true) ).

cnf(u1923,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,abstraction(X0,skc20),true) ).

cnf(u2582,negated_conjecture,
    true = organism(skc16,skc19) ).

cnf(u1053,negated_conjecture,
    true = ifeq2(living(skc13,X0),true,living(skc16,X0),true) ).

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

cnf(u679,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(human_person(X0,skc19),true,true,true),true) ).

cnf(u2816,negated_conjecture,
    true = singleton(skc16,skc23) ).

cnf(u1403,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relname(X0,skc20),true,true,true),true) ).

cnf(u2588,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,smoke(X0,skf1(X1)),true) ).

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

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

cnf(u6663,negated_conjecture,
    skc24 = ifeq3(of(skc16,skc24,skc19),true,ifeq3(of(skc16,skc24,skc19),true,skc24,skc24),skc24) ).

cnf(u397,negated_conjecture,
    true = ifeq2(present(skc13,X0),true,present(skc16,X0),true) ).

cnf(u648,negated_conjecture,
    true = ifeq2(human_person(skc13,X0),true,human_person(skc16,X0),true) ).

cnf(u1943,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(general(X0,skc20),true,true,true),true) ).

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

cnf(u2569,negated_conjecture,
    true = event(skc16,skf1(X0)) ).

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

cnf(u2853,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skf1(skc23),X2),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2583,negated_conjecture,
    true = animate(skc16,skc19) ).

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

cnf(u2716,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skf1(X0))),sF35,a,b) ).

cnf(u2851,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skf1(skc23),skc23),true) ).

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

cnf(u1156,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,eventuality(X0,skc22),true) ).

cnf(u2192,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skc26),true) ).

cnf(u2343,negated_conjecture,
    true = nonexistent(skc16,skc15) ).

cnf(u2040,negated_conjecture,
    true = specific(skc13,skc17) ).

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

cnf(u1417,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skc17,skc19),true) ).

cnf(u926,negated_conjecture,
    true = eventuality(skc16,skc26) ).

cnf(u2093,negated_conjecture,
    true = singleton(skc13,skc22) ).

cnf(u3624,negated_conjecture,
    true = jules_forename(skc16,skc24) ).

cnf(u2428,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc22),true,true,true),true) ).

cnf(u31,negated_conjecture,
    true = ifeq2(state(X0,X1),true,eventuality(X0,X1),true) ).

cnf(u2348,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc15),true,true,true) ).

cnf(u299,negated_conjecture,
    true = sF25 ).

cnf(u652,negated_conjecture,
    true = ifeq2(thing(skc13,X0),true,thing(skc16,X0),true) ).

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

cnf(u1942,negated_conjecture,
    b = ifeq(tuple(specific(skc13,skc20),true),sF35,a,b) ).

cnf(u2341,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skc15),true) ).

cnf(u2471,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relation(X0,skc16),true,true,true),true) ).

cnf(u1329,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc23),true,true,true) ).

cnf(u4377,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,X0),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u558,negated_conjecture,
    true = ifeq2(think_believe_consider(skc13,X0),true,think_believe_consider(skc16,X0),true) ).

cnf(u3125,negated_conjecture,
    ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X0),true,skc20,X0),X0) = X0 ).

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

cnf(u3106,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc20),true) ).

cnf(u80,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(unisex(X0,X2),true,unisex(X1,X2),true),true) ).

cnf(u564,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(state(X0,skc22),true,true,true),true) ).

cnf(u2099,negated_conjecture,
    true = singleton(skc13,skc23) ).

cnf(u3043,negated_conjecture,
    true = unisex(skc16,skc20) ).

cnf(u2469,negated_conjecture,
    true = ifeq2(relname(skc16,skc16),true,true,true) ).

cnf(u1952,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc24),true) ).

cnf(u2735,negated_conjecture,
    true = male(skc16,skc23) ).

cnf(u2212,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,impartial(X0,skc19),true) ).

cnf(u686,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,human_person(X0,skc23),true) ).

cnf(u2365,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc15),true) ).

cnf(u1925,negated_conjecture,
    true = general(skc13,skc20) ).

cnf(u3119,negated_conjecture,
    true = forename(skc16,skc20) ).

cnf(u2784,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(entity(X0,skc23),true,true,true),true) ).

cnf(u2227,negated_conjecture,
    true = unisex(skc13,skc22) ).

cnf(u1982,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc16),true,true,true),true) ).

cnf(u320,negated_conjecture,
    true = sF32 ).

cnf(u1463,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(theme(skc13,skc15,X1),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,skc16),skc16),skc16),skc16),skc16) ).

cnf(u6066,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skc17,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u1342,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc15),true,true,true) ).

cnf(u2493,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonhuman(X0,skc16),true) ).

cnf(u2661,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,living(X0,skc19),true) ).

cnf(u2626,negated_conjecture,
    true = specific(skc16,skc19) ).

cnf(u2183,negated_conjecture,
    b = ifeq(tuple(true,existent(skc13,skc15)),sF35,a,b) ).

cnf(u326,negated_conjecture,
    true = sF34 ).

cnf(u2632,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,animate(X0,skc19),true) ).

cnf(u3325,negated_conjecture,
    true = ifeq2(eventuality(skc13,skf1(X0)),true,true,true) ).

cnf(u2742,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(human_person(X0,skc23),true,true,true),true) ).

cnf(u1988,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(general(X0,skc16),true,true,true),true) ).

cnf(u2254,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skc26),true,true,true),true) ).

cnf(u3397,negated_conjecture,
    true = ifeq2(smoke(skc13,skc26),true,true,true) ).

cnf(u3153,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relation(X0,skc24),true,true,true),true) ).

cnf(u1264,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(entity(X0,skc19),true,true,true),true) ).

cnf(u2420,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc22),true,true,true),true) ).

cnf(u3140,negated_conjecture,
    true = relname(skc16,skc24) ).

cnf(u2371,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u2760,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,organism(X0,skc23),true) ).

cnf(u6490,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u2114,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc19),true) ).

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

cnf(u851,negated_conjecture,
    ifeq3(theme(skc13,X0,X1),true,ifeq3(agent(skc13,X0,skc19),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,skc16,X1),X1),X1),X1) = X1 ).

cnf(u1637,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,X1,skc16),true,ifeq3(agent(skc13,X1,skc19),true,ifeq3(think_believe_consider(skc13,X1),true,ifeq3(proposition(skc13,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u1869,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(human(X0,skc19),true,true,true),true) ).

cnf(u3144,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relname(X0,skc24),true,true,true),true) ).

cnf(u343,negated_conjecture,
    true = vincent_forename(skc13,skc20) ).

cnf(u2506,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc16)),sF35,a,b) ).

cnf(u2137,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc26),true,true,true),true) ).

cnf(u376,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(proposition(X0,skc16),true,true,true),true) ).

cnf(u3182,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relation(X0,skc20),true,true,true),true) ).

cnf(u3268,negated_conjecture,
    skc24 = ifeq3(of(skc13,X0,skc19),true,ifeq3(of(skc13,skc24,skc19),true,ifeq3(forename(skc13,X0),true,X0,skc24),skc24),skc24) ).

cnf(u2635,negated_conjecture,
    true = ifeq2(state(skc16,skf1(X0)),true,true,true) ).

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

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

cnf(u3175,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relname(X0,skc20),true) ).

cnf(u2127,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc23),true,true,true),true) ).

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

cnf(u6730,negated_conjecture,
    skc20 = ifeq3(of(skc16,skc24,X0),true,ifeq3(of(skc16,skc20,X0),true,ifeq3(entity(skc16,X0),true,skc24,skc20),skc20),skc20) ).

cnf(u341,negated_conjecture,
    true = man(skc13,skc23) ).

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

cnf(u2265,negated_conjecture,
    true = event(skc16,skc15) ).

cnf(u3044,negated_conjecture,
    true = general(skc16,skc20) ).

cnf(u1797,negated_conjecture,
    true = existent(skc13,skc19) ).

cnf(u2763,negated_conjecture,
    true = living(skc16,skc23) ).

cnf(u2398,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skc22),true) ).

cnf(u3549,negated_conjecture,
    true = ifeq2(unisex(skc13,skf1(X0)),true,true,true) ).

cnf(u3168,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,forename(X0,skc20),true) ).

cnf(u4583,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,X1),true,ifeq3(agent(skc16,skc15,X1),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u3049,negated_conjecture,
    b = ifeq(tuple(true,human(skc16,skc20)),sF35,a,b) ).

cnf(u2461,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(proposition(X0,skc16),true,true,true),true) ).

cnf(u2670,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,impartial(X0,skc19),true) ).

cnf(u469,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,present(X0,skc15),true) ).

cnf(u354,negated_conjecture,
    true = proposition(skc13,skc16) ).

cnf(u2409,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skc22),true) ).

cnf(u492,negated_conjecture,
    true = ifeq2(of(X0,skc24,skc23),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u3173,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relname(X0,skc20),true,true,true),true) ).

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

cnf(u212,negated_conjecture,
    true = ifeq2(man(skc16,X0),true,agent(skc16,skf1(X0),X0),true) ).

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

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

cnf(u4591,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

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

cnf(u1357,negated_conjecture,
    true = ifeq2(entity(skc16,skc26),true,true,true) ).

cnf(u1997,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc16),true) ).

cnf(u227,negated_conjecture,
    true = sF1 ).

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

cnf(u2037,negated_conjecture,
    true = specific(skc16,skc26) ).

cnf(u632,negated_conjecture,
    true = ifeq2(entity(skc13,X0),true,entity(skc16,X0),true) ).

cnf(u1799,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc13,skc19),true),sF35,a,b) ).

cnf(u3032,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonhuman(X0,skc24),true) ).

cnf(u2432,negated_conjecture,
    true = singleton(skc16,skc22) ).

cnf(u1995,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc16),true,true,true),true) ).

cnf(u881,negated_conjecture,
    true = event(skc16,skc26) ).

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

cnf(u254,negated_conjecture,
    true = sF10 ).

cnf(u2693,negated_conjecture,
    true = unisex(skc16,skf1(X0)) ).

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

cnf(u2092,negated_conjecture,
    true = singleton(skc16,skc26) ).

cnf(u895,negated_conjecture,
    true = ifeq2(present(X0,skc26),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u1146,negated_conjecture,
    true = ifeq2(smoke(skc13,skc22),true,true,true) ).

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

cnf(u2572,negated_conjecture,
    true = ifeq2(man(skc16,X0),true,true,true) ).

cnf(u11,negated_conjecture,
    true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).

cnf(u3819,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,state(X0,skc22),true) ).

cnf(u2717,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skf1(X1)),true,true,true),true) ).

cnf(u2053,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc17),true) ).

cnf(u4559,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skc26,X1),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1927,negated_conjecture,
    true = thing(skc13,skc20) ).

cnf(u266,negated_conjecture,
    true = sF14 ).

cnf(u1041,negated_conjecture,
    true = ifeq2(unisex(skc13,X0),true,unisex(skc16,X0),true) ).

cnf(u114,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(animate(X0,X2),true,animate(X1,X2),true),true) ).

cnf(u6641,negated_conjecture,
    skc24 = ifeq3(of(skc16,X0,skc19),true,ifeq3(of(skc16,skc24,skc19),true,ifeq3(forename(skc16,X0),true,X0,skc24),skc24),skc24) ).

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

cnf(u1027,negated_conjecture,
    true = ifeq2(existent(skc13,X0),true,existent(skc16,X0),true) ).

cnf(u2694,negated_conjecture,
    true = nonexistent(skc16,skf1(X0)) ).

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

cnf(u6160,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skf1(skc19),X1),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u1144,negated_conjecture,
    true = event(skc13,skc22) ).

cnf(u2567,negated_conjecture,
    true = smoke(skc16,skf1(X0)) ).

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

cnf(u2700,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skf1(X0))),sF35,a,b) ).

cnf(u1268,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,entity(X0,skc19),true) ).

cnf(u3050,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonhuman(X0,skc20),true,true,true),true) ).

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

cnf(u242,negated_conjecture,
    true = sF6 ).

cnf(u2809,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc23),true,true,true) ).

cnf(u2436,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc22),true) ).

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

cnf(u3608,negated_conjecture,
    skc20 = ifeq3(of(skc16,skc24,skc19),true,skc24,skc20) ).

cnf(u2107,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

cnf(u2695,negated_conjecture,
    true = specific(skc16,skf1(X0)) ).

cnf(u1802,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,existent(X0,skc19),true) ).

cnf(u916,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skc26,X2),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u6890,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skc26),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u450,negated_conjecture,
    true = ifeq2(of(skc13,X0,X1),true,of(skc16,X0,X1),true) ).

cnf(u1926,negated_conjecture,
    true = nonhuman(skc13,skc20) ).

cnf(u2325,negated_conjecture,
    true = ifeq2(state(skc16,skc15),true,true,true) ).

cnf(u1808,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,existent(X0,skc23),true) ).

cnf(u2591,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc16,skc19),true),sF35,a,b) ).

cnf(u3628,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(jules_forename(X0,skc24),true,true,true),true) ).

cnf(u2810,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc23),true,true,true) ).

cnf(u1545,negated_conjecture,
    true = of(skc16,skc20,skc19) ).

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

cnf(u1930,negated_conjecture,
    b = ifeq(tuple(true,human(skc13,skc20)),sF35,a,b) ).

cnf(u281,negated_conjecture,
    true = sF19 ).

cnf(u2098,negated_conjecture,
    true = singleton(skc13,skc20) ).

cnf(u411,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(event(X0,skc15),true,true,true),true) ).

cnf(u565,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,state(X0,skc22),true) ).

cnf(u8470,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2385,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skc22),true,true,true),true) ).

cnf(u1936,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc20)),sF35,a,b) ).

cnf(u2719,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skf1(X1)),true) ).

cnf(u1844,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,animate(X0,skc23),true) ).

cnf(u2844,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skf1(skc19),X2),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2761,negated_conjecture,
    true = entity(skc16,skc23) ).

cnf(u670,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(eventuality(X0,skc15),true,true,true),true) ).

cnf(u2349,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc15)),sF35,a,b) ).

cnf(u55,negated_conjecture,
    true = ifeq2(man(X0,X1),true,male(X0,X1),true) ).

cnf(u1842,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(animate(X0,skc23),true,true,true),true) ).

cnf(u8635,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(theme(skc16,X0,X1),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

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

cnf(u676,negated_conjecture,
    true = human_person(skc13,skc23) ).

cnf(u6727,negated_conjecture,
    skc20 = ifeq3(of(skc16,X0,skc23),true,ifeq3(of(skc16,skc20,skc23),true,ifeq3(forename(skc16,X0),true,X0,skc20),skc20),skc20) ).

cnf(u1848,negated_conjecture,
    true = ifeq2(relname(skc13,skc16),true,true,true) ).

cnf(u2846,negated_conjecture,
    true = ifeq2(agent(skc13,skf1(skc23),skc23),true,true,true) ).

cnf(u2863,negated_conjecture,
    skc20 = ifeq3(of(skc13,skc20,X0),true,ifeq3(of(skc13,skc20,X0),true,ifeq3(entity(skc13,X0),true,skc20,skc20),skc20),skc20) ).

cnf(u2466,negated_conjecture,
    true = relation(skc16,skc16) ).

cnf(u1972,negated_conjecture,
    true = thing(skc13,skc16) ).

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

cnf(u53,negated_conjecture,
    true = ifeq2(human_person(X0,X1),true,animate(X0,X1),true) ).

cnf(u1970,negated_conjecture,
    true = general(skc13,skc16) ).

cnf(u3231,negated_conjecture,
    true = ifeq2(thing(skc13,skf1(X0)),true,true,true) ).

cnf(u332,negated_conjecture,
    b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),sF35,a,b) ).

cnf(u308,negated_conjecture,
    true = sF28 ).

cnf(u2355,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skc15)),sF35,a,b) ).

cnf(u1433,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(male(X0,skc23),true,true,true),true) ).

cnf(u2744,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,human_person(X0,skc23),true) ).

cnf(u4407,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,skc16,skc16),skc16),skc16) ).

cnf(u1330,negated_conjecture,
    true = thing(skc16,skc26) ).

cnf(u2235,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc22),true) ).

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

cnf(u2377,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

cnf(u1853,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relation(X0,skc24),true,true,true),true) ).

cnf(u3128,negated_conjecture,
    skc24 = ifeq3(of(skc16,X0,skc23),true,ifeq3(forename(skc16,X0),true,X0,skc24),skc24) ).

cnf(u2664,negated_conjecture,
    true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u2490,negated_conjecture,
    b = ifeq(tuple(true,human(skc16,skc16)),sF35,a,b) ).

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

cnf(u681,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,human_person(X0,skc19),true) ).

cnf(u2483,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,abstraction(X0,skc16),true) ).

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

cnf(u2226,negated_conjecture,
    true = unisex(skc16,skc26) ).

cnf(u6980,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u3139,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,forename(X0,skc24),true) ).

cnf(u2812,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc23),true,true,true),true) ).

cnf(u1981,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc16)),sF35,a,b) ).

cnf(u2843,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X0),true,ifeq3(theme(skc16,X1,X2),true,ifeq3(agent(skc16,X1,skc19),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1201,negated_conjecture,
    skc20 = ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X0),true,X0,skc20),skc20) ).

cnf(u8636,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(theme(skc16,X0,X1),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u2747,negated_conjecture,
    true = human(skc16,skc23) ).

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

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

cnf(u2239,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc17)),sF35,a,b) ).

cnf(u6979,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u3148,negated_conjecture,
    true = relation(skc16,skc24) ).

cnf(u2379,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,singleton(X0,skc15),true) ).

cnf(u3022,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,abstraction(X0,skc24),true) ).

cnf(u1749,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,present(X0,skc15),true) ).

cnf(u8630,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skf1(skc23),X1),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u1284,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc19),true) ).

cnf(u1871,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,human(X0,skc19),true) ).

cnf(u2122,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc24),true,true,true),true) ).

cnf(u2249,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc15),true) ).

cnf(u348,negated_conjecture,
    true = present(skc13,skc17) ).

cnf(u3163,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(forename(X0,skc20),true,true,true),true) ).

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

cnf(u3152,negated_conjecture,
    true = ifeq2(proposition(skc16,skc24),true,true,true) ).

cnf(u1370,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(agent(skc13,skc15,X1),true,ifeq3(agent(skc13,X0,X1),true,ifeq3(think_believe_consider(skc13,X0),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u4705,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u1090,negated_conjecture,
    skc16 = ifeq3(theme(skc13,skc15,X0),true,ifeq3(proposition(skc13,X0),true,X0,skc16),skc16) ).

cnf(u3411,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skc15,X2),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4310,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc15,X0),true,ifeq3(agent(skc16,skc15,X1),true,ifeq3(agent(skc16,skc15,X1),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u1893,negated_conjecture,
    true = unisex(skc13,skc24) ).

cnf(u2400,negated_conjecture,
    true = nonexistent(skc16,skc22) ).

cnf(u367,negated_conjecture,
    true = be(skc13,skc22,skc23,skc23) ).

cnf(u2888,negated_conjecture,
    ifeq3(of(skc13,skc24,skc19),true,ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X0),true,skc24,X0),X0),X0) = X0 ).

cnf(u1113,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(agent(skc13,X0,X1),true,ifeq3(agent(skc13,skc15,X1),true,ifeq3(think_believe_consider(skc13,X0),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u476,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,of(X0,skc20,skc19),true) ).

cnf(u7079,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u110,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(living(X0,X2),true,living(X1,X2),true),true) ).

cnf(u2677,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc19),true) ).

cnf(u2434,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc22),true,true,true),true) ).

cnf(u2675,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc19),true,true,true),true) ).

cnf(u2406,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc22)),sF35,a,b) ).

cnf(u365,negated_conjecture,
    true = theme(skc13,skc17,skc16) ).

cnf(u616,negated_conjecture,
    ifeq3(theme(skc13,skc17,X0),true,ifeq3(theme(skc13,X1,X2),true,ifeq3(agent(skc13,X1,skc19),true,ifeq3(think_believe_consider(skc13,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2167,negated_conjecture,
    true = nonexistent(skc13,skc22) ).

cnf(u3021,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(abstraction(X0,skc24),true,true,true),true) ).

cnf(u3664,negated_conjecture,
    true = ifeq2(singleton(skc13,skf1(X0)),true,true,true) ).

cnf(u466,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,present(X0,skc17),true) ).

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

cnf(u2788,negated_conjecture,
    true = existent(skc16,skc23) ).

cnf(u2264,negated_conjecture,
    true = event(skc16,skc22) ).

cnf(u879,negated_conjecture,
    skc14 = skc16 ).

cnf(u3786,negated_conjecture,
    true = ifeq2(accessible_world(skc16,skc13),true,true,true) ).

cnf(u4316,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,X0),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u2764,negated_conjecture,
    true = impartial(skc16,skc23) ).

cnf(u2039,negated_conjecture,
    true = specific(skc13,skc15) ).

cnf(u464,negated_conjecture,
    true = ifeq2(present(X0,skc17),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

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

cnf(u236,negated_conjecture,
    true = sF4 ).

cnf(u1139,negated_conjecture,
    true = be(skc16,skc22,skc23,skc23) ).

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

cnf(u1277,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,entity(X0,skc23),true) ).

cnf(u1280,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc19),true,true,true) ).

cnf(u2701,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skf1(X1)),true,true,true),true) ).

cnf(u1007,negated_conjecture,
    true = ifeq2(smoke(skc13,skc17),true,true,true) ).

cnf(u4586,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,skc16,X1),X1),X1),X1) = X1 ).

cnf(u2190,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skc26),true,true,true),true) ).

cnf(u251,negated_conjecture,
    true = sF9 ).

cnf(u2166,negated_conjecture,
    true = nonexistent(skc16,skc26) ).

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

cnf(u2288,negated_conjecture,
    true = thing(skc16,skc17) ).

cnf(u1031,negated_conjecture,
    true = ifeq2(impartial(skc13,X0),true,impartial(skc16,X0),true) ).

cnf(u2734,negated_conjecture,
    true = human_person(skc16,skc23) ).

cnf(u5994,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skc15,X1),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u2793,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc16,skc23),true),sF35,a,b) ).

cnf(u1267,negated_conjecture,
    ifeq3(of(skc13,X0,skc19),true,ifeq3(of(skc13,X1,skc19),true,ifeq3(forename(skc13,X0),true,ifeq3(forename(skc13,X1),true,X0,X1),X1),X1),X1) = X1 ).

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

cnf(u4584,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(agent(skc16,skc15,X1),true,ifeq3(agent(skc16,skc15,X1),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u1914,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,general(X0,skc24),true) ).

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

cnf(u2840,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc19),skc19),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u2038,negated_conjecture,
    true = specific(skc13,skc22) ).

cnf(u1792,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc23),true) ).

cnf(u2439,negated_conjecture,
    true = ifeq2(accessible_world(skc13,skc13),true,true,true) ).

cnf(u7690,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc23),X0),true,ifeq3(theme(skc16,skc15,X1),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u905,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(smoke(X0,skc26),true,true,true),true) ).

cnf(u4335,negated_conjecture,
    skc16 = ifeq3(agent(skc16,skc15,X0),true,ifeq3(agent(skc16,skc15,X0),true,skc16,skc16),skc16) ).

cnf(u2794,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(existent(X0,skc23),true,true,true),true) ).

cnf(u2044,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc22),true,true,true),true) ).

cnf(u2189,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skc26)),sF35,a,b) ).

cnf(u919,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,X1),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(agent(skc13,X0,X2),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,skc16),skc16),skc16),skc16),skc16) ).

cnf(u33,negated_conjecture,
    true = ifeq2(state(X0,X1),true,event(X0,X1),true) ).

cnf(u5631,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,skc16,skc16),skc16),skc16) ).

cnf(u2067,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc26),true) ).

cnf(u4330,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc15,X0),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16) ).

cnf(u510,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,jules_forename(X0,skc24),true) ).

cnf(u2703,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skf1(X1)),true) ).

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

cnf(u3097,negated_conjecture,
    true = ifeq2(entity(skc16,skc20),true,true,true) ).

cnf(u5156,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,skc16,skc16),skc16) ).

cnf(u1179,negated_conjecture,
    true = entity(skc13,skc19) ).

cnf(u2094,negated_conjecture,
    true = singleton(skc13,skc16) ).

cnf(u2180,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonexistent(X0,skc17),true) ).

cnf(u1411,negated_conjecture,
    true = agent(skc16,skc17,skc19) ).

cnf(u6934,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,skc15,X0),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2463,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,proposition(X0,skc16),true) ).

cnf(u2594,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,human(X0,skc19),true) ).

cnf(u8465,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skf1(skc19),skc16),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc19)),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2076,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,living(X0,skc19),true) ).

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

cnf(u677,negated_conjecture,
    true = human_person(skc13,skc19) ).

cnf(u2600,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(organism(X0,skc19),true,true,true),true) ).

cnf(u909,negated_conjecture,
    true = ifeq2(theme(X0,skc15,skc16),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u3098,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skc20),true,true,true),true) ).

cnf(u1956,negated_conjecture,
    true = ifeq2(entity(skc13,skc20),true,true,true) ).

cnf(u2177,negated_conjecture,
    b = ifeq(tuple(true,existent(skc13,skc17)),sF35,a,b) ).

cnf(u3222,negated_conjecture,
    true = ifeq2(thing(skc13,skc26),true,true,true) ).

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

cnf(u1954,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc20),true,true,true) ).

cnf(u305,negated_conjecture,
    true = sF27 ).

cnf(u1976,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonhuman(X0,skc16),true,true,true),true) ).

cnf(u1282,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc19),true,true,true),true) ).

cnf(u1440,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relation(X0,skc16),true,true,true),true) ).

cnf(u6958,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,skc17,X0),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u1343,negated_conjecture,
    true = ifeq2(entity(skc13,skc15),true,true,true) ).

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

cnf(u3500,negated_conjecture,
    skc24 = ifeq3(of(skc16,skc20,skc23),true,skc20,skc24) ).

cnf(u2419,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc22)),sF35,a,b) ).

cnf(u1438,negated_conjecture,
    true = relation(skc13,skc16) ).

cnf(u2605,negated_conjecture,
    true = living(skc16,skc19) ).

cnf(u928,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skc26),true) ).

cnf(u311,negated_conjecture,
    true = sF29 ).

cnf(u1858,negated_conjecture,
    true = ifeq2(proposition(skc13,skc20),true,true,true) ).

cnf(u420,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,man(X0,skc23),true) ).

cnf(u2603,negated_conjecture,
    true = entity(skc16,skc19) ).

cnf(u2623,negated_conjecture,
    ifeq3(of(skc16,X0,skc19),true,ifeq3(of(skc16,X1,skc19),true,ifeq3(forename(skc16,X0),true,ifeq3(forename(skc16,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u2095,negated_conjecture,
    true = singleton(skc13,skc15) ).

cnf(u1442,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relation(X0,skc16),true) ).

cnf(u2363,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc15),true,true,true),true) ).

cnf(u333,negated_conjecture,
    true = actual_world(skc13) ).

cnf(u2733,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,man(X0,skc23),true) ).

cnf(u560,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,think_believe_consider(X0,skc17),true) ).

cnf(u1855,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relation(X0,skc24),true) ).

cnf(u2233,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc22),true,true,true),true) ).

cnf(u6787,negated_conjecture,
    ifeq3(of(skc16,skc20,skc23),true,ifeq3(of(skc16,X0,skc23),true,ifeq3(forename(skc16,X0),true,skc20,X0),X0),X0) = X0 ).

cnf(u2709,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(thing(X0,skf1(X1)),true,true,true),true) ).

cnf(u2731,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(man(X0,skc23),true,true,true),true) ).

cnf(u2796,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,existent(X0,skc23),true) ).

cnf(u2889,negated_conjecture,
    skc20 = ifeq3(of(skc13,skc24,X0),true,ifeq3(of(skc13,skc20,X0),true,ifeq3(entity(skc13,X0),true,skc24,skc20),skc20),skc20) ).

cnf(u1969,negated_conjecture,
    true = unisex(skc13,skc16) ).

cnf(u2491,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonhuman(X0,skc16),true,true,true),true) ).

cnf(u1350,negated_conjecture,
    true = ifeq2(entity(skc13,skc22),true,true,true) ).

cnf(u1950,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc24),true,true,true),true) ).

cnf(u437,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(forename(X0,skc24),true,true,true),true) ).

cnf(u2412,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skc22)),sF35,a,b) ).

cnf(u3012,negated_conjecture,
    true = abstraction(skc16,skc20) ).

cnf(u3069,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc20)),sF35,a,b) ).

cnf(u8400,negated_conjecture,
    ifeq3(theme(skc16,X0,X1),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X1),true,skc16,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u2819,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc23)),sF35,a,b) ).

cnf(u591,negated_conjecture,
    ifeq3(theme(skc13,X0,X1),true,ifeq3(theme(skc13,skc15,X2),true,ifeq3(agent(skc13,X0,X3),true,ifeq3(agent(skc13,skc15,X3),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,ifeq3(proposition(skc13,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4684,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,X0,X1),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u7124,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u1202,negated_conjecture,
    ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X0),true,skc20,X0),X0) = X0 ).

cnf(u3769,negated_conjecture,
    true = ifeq2(smoke(skc13,skf1(X0)),true,true,true) ).

cnf(u2638,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skf1(X1)),true,true,true),true) ).

cnf(u1877,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,human(X0,skc23),true) ).

cnf(u351,negated_conjecture,
    true = present(skc13,skc15) ).

cnf(u2651,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc19),true,true,true) ).

cnf(u3655,negated_conjecture,
    true = ifeq2(singleton(skc13,skc26),true,true,true) ).

cnf(u4686,negated_conjecture,
    ifeq3(theme(skc16,skc26,X0),true,ifeq3(theme(skc16,skc17,X1),true,ifeq3(agent(skc16,skc17,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u460,negated_conjecture,
    true = ifeq2(agent(skc13,X0,X1),true,agent(skc16,X0,X1),true) ).

cnf(u1875,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(human(X0,skc23),true,true,true),true) ).

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

cnf(u4317,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,X1),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16) ).

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

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

cnf(u3940,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X0,skc16),true,ifeq3(theme(skc13,skc15,X1),true,ifeq3(agent(skc13,X0,X2),true,ifeq3(agent(skc13,skc15,X2),true,ifeq3(think_believe_consider(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u2659,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(living(X0,skc19),true,true,true),true) ).

cnf(u2680,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc19),true,true,true),true) ).

cnf(u1273,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(entity(X0,skc23),true,true,true),true) ).

cnf(u349,negated_conjecture,
    true = think_believe_consider(skc13,skc17) ).

cnf(u1895,negated_conjecture,
    true = nonhuman(skc13,skc24) ).

cnf(u4706,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,skc26,X0),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u2890,negated_conjecture,
    skc24 = ifeq3(of(skc13,skc24,X0),true,ifeq3(of(skc13,skc24,X0),true,ifeq3(entity(skc13,X0),true,skc24,skc24),skc24),skc24) ).

cnf(u1225,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,organism(X0,skc23),true) ).

cnf(u92,negated_conjecture,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).

cnf(u2789,negated_conjecture,
    true = specific(skc16,skc23) ).

cnf(u4557,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skc26,X1),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(proposition(skc16,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16) ).

cnf(u1480,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(theme(skc13,skc15,X1),true,ifeq3(proposition(skc13,X0),true,ifeq3(proposition(skc13,X1),true,X1,X0),X0),X0),X0) = X0 ).

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

cnf(u1114,negated_conjecture,
    ifeq3(theme(skc13,skc15,X0),true,ifeq3(agent(skc13,skc15,X1),true,ifeq3(agent(skc13,skc15,X1),true,ifeq3(proposition(skc13,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u2401,negated_conjecture,
    true = specific(skc16,skc22) ).

cnf(u2668,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(impartial(X0,skc19),true,true,true),true) ).

cnf(u1891,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(abstraction(X0,skc24),true,true,true),true) ).

cnf(u1238,negated_conjecture,
    skc24 = skc25 ).

cnf(u2144,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc16),true) ).

cnf(u3439,negated_conjecture,
    true = ifeq2(nonexistent(skc13,skc26),true,true,true) ).

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

cnf(u1335,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc17),true,true,true) ).

cnf(u2790,negated_conjecture,
    true = thing(skc16,skc23) ).

cnf(u3024,negated_conjecture,
    true = general(skc16,skc24) ).

cnf(u2663,negated_conjecture,
    true = ifeq2(present(skc13,skf1(X0)),true,true,true) ).

cnf(u3169,negated_conjecture,
    true = relname(skc16,skc20) ).

cnf(u2771,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(male(X0,skc23),true,true,true),true) ).

cnf(u5235,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16) ).

cnf(u1150,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,event(X0,skc22),true) ).

cnf(u467,negated_conjecture,
    true = ifeq2(present(X0,skc15),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u1894,negated_conjecture,
    true = general(skc13,skc24) ).

cnf(u1143,negated_conjecture,
    true = ifeq2(state(skc16,skc26),true,true,true) ).

cnf(u1992,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc16),true,true,true) ).

cnf(u2650,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc19),true,true,true) ).

cnf(u2777,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,animate(X0,skc23),true) ).

cnf(u1828,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,theme(X0,skc15,skc16),true) ).

cnf(u8464,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skf1(skc23),skc16),true,ifeq3(agent(skc16,X0,skc23),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc23)),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u1405,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relname(X0,skc20),true) ).

cnf(u2473,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relation(X0,skc16),true) ).

cnf(u233,negated_conjecture,
    true = sF3 ).

cnf(u1148,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(event(X0,skc22),true,true,true),true) ).

cnf(u379,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,proposition(X0,skc16),true) ).

cnf(u1278,negated_conjecture,
    true = thing(skc13,skc23) ).

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

cnf(u418,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(man(X0,skc19),true,true,true),true) ).

cnf(u1035,negated_conjecture,
    true = ifeq2(general(skc13,X0),true,general(skc16,X0),true) ).

cnf(u2051,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc17),true,true,true),true) ).

cnf(u1395,negated_conjecture,
    true = relname(skc13,skc20) ).

cnf(u2301,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skc17),true) ).

cnf(u903,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skc26,skc23),true) ).

cnf(u6112,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(theme(skc16,skc26,skc16),true,ifeq3(think_believe_consider(skc16,skc26),true,ifeq3(think_believe_consider(skc16,skc26),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u239,negated_conjecture,
    true = sF5 ).

cnf(u2256,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skc26),true) ).

cnf(u2801,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,living(X0,skc23),true) ).

cnf(u1276,negated_conjecture,
    ifeq3(of(skc13,X0,skc23),true,ifeq3(of(skc13,X1,skc23),true,ifeq3(forename(skc13,X0),true,ifeq3(forename(skc13,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u507,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(jules_forename(X0,skc24),true,true,true),true) ).

cnf(u1806,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(existent(X0,skc23),true,true,true),true) ).

cnf(u1346,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc15),true) ).

cnf(u272,negated_conjecture,
    true = sF16 ).

cnf(u893,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skc26),true) ).

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

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

cnf(u1409,negated_conjecture,
    true = ifeq2(agent(skc13,skc26,skc23),true,true,true) ).

cnf(u1812,negated_conjecture,
    true = theme(skc16,skc15,skc16) ).

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

cnf(u4358,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc26,skc16),true,ifeq3(agent(skc16,skc15,skc23),true,ifeq3(think_believe_consider(skc16,skc26),true,skc16,skc16),skc16),skc16) ).

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

cnf(u1835,negated_conjecture,
    true = animate(skc13,skc19) ).

cnf(u6642,negated_conjecture,
    skc24 = ifeq3(of(skc16,skc20,X0),true,ifeq3(of(skc16,skc24,X0),true,ifeq3(entity(skc16,X0),true,skc20,skc24),skc24),skc24) ).

cnf(u2060,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc15),true) ).

cnf(u1547,negated_conjecture,
    true = ifeq2(of(X0,skc20,skc19),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u278,negated_conjecture,
    true = sF18 ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP248-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37  % Computer : n017.cluster.edu
% 0.12/0.37  % Model    : x86_64 x86_64
% 0.12/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37  % Memory   : 8046.5625MB
% 0.12/0.37  % OS       : Linux 6.8.0-71-generic
% 0.12/0.37  % CPULimit : 300
% 0.12/0.37  % WCLimit  : 300
% 0.12/0.37  % DateTime : Sun Sep 27 18:31:35 UTC 2026
% 0.12/0.38  % CPUTime  : 
% 0.12/0.38  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41  Running first-order theorem proving
% 0.12/0.41  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.92/2.27  % (2869530)Detected a unit-equality problem, will run specialized UEQ schedule.
% 9.92/2.27  % (2869540)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1106033513:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 9.92/2.27  % (2869536)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=1930012120:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 9.92/2.27  % (2869537)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=4129364336:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 9.92/2.27  % (2869538)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2973348262:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 9.92/2.27  % (2869535)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=2955902664:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 9.92/2.27  % (2869541)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1634055887:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 9.92/2.27  % (2869539)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2111363622:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 9.92/2.27  % (2869540)Instruction limit reached! 
% 9.92/2.27  % (2869540)------------------------------
% 9.92/2.27  % (2869540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.27  % (2869540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.27  % (2869540)CaDiCaL version: 2.1.3
% 9.92/2.27  % (2869540)Termination reason: Instruction limit
% 9.92/2.27  % (2869540)Termination phase: Saturation
% 9.92/2.27  % (2869540)Time elapsed: 0.080 s
% 9.92/2.27  % (2869540)Peak memory usage: 91 MB
% 9.92/2.27  % (2869540)Instructions burned: 259 (million)
% 9.92/2.27  % (2869538)Instruction limit reached! 
% 9.92/2.27  % (2869538)------------------------------
% 9.92/2.27  % (2869538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.27  % (2869538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.27  % (2869538)CaDiCaL version: 2.1.3
% 9.92/2.27  % (2869538)Termination reason: Instruction limit
% 9.92/2.27  % (2869538)Termination phase: Saturation
% 9.92/2.27  % (2869538)Time elapsed: 0.072 s
% 9.92/2.27  % (2869538)Peak memory usage: 89 MB
% 9.92/2.27  % (2869538)Instructions burned: 136 (million)
% 9.92/2.27  % (2869539)Instruction limit reached! 
% 9.92/2.27  % (2869539)------------------------------
% 9.92/2.27  % (2869539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.27  % (2869539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.27  % (2869539)CaDiCaL version: 2.1.3
% 9.92/2.27  % (2869539)Termination reason: Instruction limit
% 9.92/2.27  % (2869539)Termination phase: Saturation
% 9.92/2.27  % (2869539)Time elapsed: 0.105 s
% 9.92/2.27  % (2869539)Peak memory usage: 89 MB
% 9.92/2.27  % (2869539)Instructions burned: 181 (million)
% 9.92/2.27  % (2869549)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1623527903:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 9.92/2.27  % (2869550)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2660148094:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 9.92/2.27  % (2869551)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1429774431:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 9.92/2.27  % (2869551)Instruction limit reached! 
% 9.92/2.27  % (2869551)------------------------------
% 9.92/2.27  % (2869551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.27  % (2869551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.27  % (2869551)CaDiCaL version: 2.1.3
% 9.92/2.27  % (2869551)Termination reason: Instruction limit
% 9.92/2.27  % (2869551)Termination phase: Saturation
% 9.92/2.27  % (2869551)Time elapsed: 0.111 s
% 9.92/2.27  % (2869551)Peak memory usage: 93 MB
% 9.92/2.27  % (2869551)Instructions burned: 217 (million)
% 9.92/2.27  % (2869541)Refutation not found, incomplete strategy
% 9.92/2.27  % (2869541)------------------------------
% 9.92/2.27  % (2869541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.27  % (2869541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.27  % (2869541)CaDiCaL version: 2.1.3
% 9.92/2.27  % (2869541)Termination reason: Refutation not found, incomplete strategy
% 9.92/2.27  % (2869541)Time elapsed: 0.436 s
% 9.92/2.27  % (2869541)Peak memory usage: 94 MB
% 9.92/2.27  % (2869541)Instructions burned: 781 (million)
% 9.92/2.27  % (2869555)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=1859350623:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 9.92/2.27  % (2869555)Instruction limit reached! 
% 9.92/2.27  % (2869555)------------------------------
% 9.92/2.27  % (2869555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.92/2.27  % (2869555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.92/2.27  % (2869555)CaDiCaL version: 2.1.3
% 9.92/2.27  % (2869555)Termination reason: Instruction limit
% 9.92/2.27  % (2869555)Termination phase: Saturation
% 9.92/2.27  % (2869555)Time elapsed: 0.159 s
% 9.92/2.27  % (2869555)Peak memory usage: 95 MB
% 9.92/2.27  % (2869555)Instructions burned: 317 (million)
% 9.92/2.27  % (2869541)------------------------------
% 9.92/2.27  % (2869541)------------------------------
% 9.92/2.27  % (2869557)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=2168645138:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 9.92/2.27  % (2869558)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=973810116:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 9.92/2.27  % (2869537)First to succeed.
% 9.92/2.27  % (2869537)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2869530"
% 9.92/2.27  % SZS status Satisfiable for theBenchmark
% 9.92/2.27  % SZS output start Saturation.
% See solution above
% 10.56/2.47  % SZS output start Definitions and Model Updates.
% 10.56/2.47  % SZS output end Definitions and Model Updates.
% 10.56/2.47  % (2869537)------------------------------
% 10.56/2.47  % (2869537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.56/2.47  % (2869537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.56/2.47  % (2869537)CaDiCaL version: 2.1.3
% 10.56/2.47  % (2869537)Termination reason: Satisfiable
% 10.56/2.47  % (2869537)Time elapsed: 1.111 s
% 10.56/2.47  % (2869537)Peak memory usage: 140 MB
% 10.56/2.47  % (2869537)Instructions burned: 2429 (million)
% 10.56/2.47  % (2869537)------------------------------
% 10.56/2.47  % (2869537)------------------------------
% 10.56/2.47  % (2869530)Success in time 1.414 s
% 10.56/2.47  % Vampire exiting
%------------------------------------------------------------------------------