Vampire---5.0.1.SAT-Sat.s

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

% Computer : n011.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:12 PM UTC 2026

% Result   : Satisfiable 14.32s 2.83s
% Output   : Saturation 14.60s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u991,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

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

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

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

cnf(u1458,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc19),true) ).

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

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

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

cnf(u1161,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc24),true,true,true),true) ).

cnf(u7479,negated_conjecture,
    skc18 = ifeq3(of(skc13,skc18,skc25),true,ifeq3(of(skc13,skc18,skc25),true,skc18,skc18),skc18) ).

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

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

cnf(u2776,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,man(X0,skc25),true) ).

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

cnf(u612,negated_conjecture,
    true = ifeq2(entity(skc13,skc26),true,true,true) ).

cnf(u9525,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(u281,negated_conjecture,
    true = sF19 ).

cnf(u947,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skc24)),tuple(true,true),a,b) ).

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

cnf(u5208,negated_conjecture,
    ifeq3(of(skc16,skc18,X1),true,ifeq3(of(skc16,X0,X1),true,ifeq3(forename(skc16,X0),true,ifeq3(entity(skc16,X1),true,skc18,X0),X0),X0),X0) = X0 ).

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

cnf(u4950,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,be(X0,skc24,skc25,skc25),true) ).

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

cnf(u9389,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(u782,negated_conjecture,
    true = ifeq2(state(skc16,skc17),true,true,true) ).

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

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

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

cnf(u7707,negated_conjecture,
    true = smoke(skc16,skc21) ).

cnf(u2975,negated_conjecture,
    true = impartial(skc16,skc25) ).

cnf(u314,negated_conjecture,
    true = sF30 ).

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

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

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

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

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

cnf(u2132,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(abstraction(X0,skc18),true,true,true),true) ).

cnf(u293,negated_conjecture,
    true = sF23 ).

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

cnf(u1914,negated_conjecture,
    true = relation(skc16,skc16) ).

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

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

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

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

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

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

cnf(u2177,negated_conjecture,
    b = ifeq(tuple(specific(skc16,skc18),true),tuple(true,true),a,b) ).

cnf(u251,negated_conjecture,
    true = sF9 ).

cnf(u3654,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,male(X0,skc25),true) ).

cnf(u1468,negated_conjecture,
    true = ifeq2(nonexistent(skc13,skc21),true,true,true) ).

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

cnf(u4781,negated_conjecture,
    true = ifeq2(of(X0,skc26,skc25),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

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

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

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

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

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

cnf(u955,negated_conjecture,
    true = singleton(skc16,skc24) ).

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

cnf(u9466,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(u4460,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skc15,skc19),true) ).

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

cnf(u7887,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skc21),true,true,true),true) ).

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

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

cnf(u561,negated_conjecture,
    true = ifeq2(vincent_forename(skc13,skc26),true,true,true) ).

cnf(u263,negated_conjecture,
    true = sF13 ).

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

cnf(u868,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc26),true) ).

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

cnf(u594,negated_conjecture,
    true = nonhuman(skc13,skc26) ).

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

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

cnf(u7712,negated_conjecture,
    true = eventuality(skc16,skc21) ).

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

cnf(u2820,negated_conjecture,
    true = human(skc16,skc19) ).

cnf(u1625,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,present(X0,skc17),true) ).

cnf(u2105,negated_conjecture,
    true = general(skc16,skc18) ).

cnf(u489,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc25),true,true,true) ).

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

cnf(u3546,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,human(X0,skc25),true) ).

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

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

cnf(u7544,negated_conjecture,
    ifeq3(of(skc13,skc18,skc25),true,ifeq3(of(skc13,X0,skc25),true,ifeq3(forename(skc13,X0),true,skc18,X0),X0),X0) = X0 ).

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

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

cnf(u9137,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(u1171,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc19),true) ).

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

cnf(u864,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc19),true) ).

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

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

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

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

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

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

cnf(u2773,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(man(X0,skc25),true,true,true),true) ).

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

cnf(u9465,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(u2873,negated_conjecture,
    true = specific(skc16,skf1(X0)) ).

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

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

cnf(u2892,negated_conjecture,
    true = ifeq2(thing(skc13,skf1(X0)),true,true,true) ).

cnf(u3598,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,animate(X0,skc25),true) ).

cnf(u2961,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,human_person(X0,skc25),true) ).

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

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

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

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

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

cnf(u3493,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,living(X0,skc25),true) ).

cnf(u1164,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc24),true,true,true),true) ).

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

cnf(u296,negated_conjecture,
    true = sF24 ).

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

cnf(u3384,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(impartial(X0,skc25),true,true,true),true) ).

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

cnf(u7706,negated_conjecture,
    true = present(skc16,skc21) ).

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

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

cnf(u3938,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relname(X0,skc26),true) ).

cnf(u248,negated_conjecture,
    true = sF8 ).

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

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

cnf(u5196,negated_conjecture,
    skc18 = ifeq3(of(skc16,X1,X0),true,ifeq3(of(skc16,skc18,X0),true,ifeq3(forename(skc16,X1),true,ifeq3(entity(skc16,X0),true,X1,skc18),skc18),skc18),skc18) ).

cnf(u471,negated_conjecture,
    true = organism(skc13,skc25) ).

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

cnf(u7727,negated_conjecture,
    true = ifeq2(state(skc16,skc21),true,true,true) ).

cnf(u233,negated_conjecture,
    true = sF3 ).

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

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

cnf(u361,negated_conjecture,
    true = be(skc13,skc24,skc25,skc25) ).

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

cnf(u2128,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(abstraction(X0,skc26),true,true,true),true) ).

cnf(u308,negated_conjecture,
    true = sF28 ).

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

cnf(u9469,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skc21,X1),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u862,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc18),true) ).

cnf(u2098,negated_conjecture,
    true = ifeq2(proposition(skc16,skc26),true,true,true) ).

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

cnf(u693,negated_conjecture,
    true = ifeq2(accessible_world(skc13,skc13),true,true,true) ).

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

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

cnf(u7566,negated_conjecture,
    ifeq3(of(skc13,skc26,skc19),true,ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X0),true,skc26,X0),X0),X0) = X0 ).

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

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

cnf(u4834,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,of(X0,skc26,skc25),true) ).

cnf(u4284,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(jules_forename(X0,skc26),true,true,true),true) ).

cnf(u467,negated_conjecture,
    true = human_person(skc13,skc19) ).

cnf(u266,negated_conjecture,
    true = sF14 ).

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

cnf(u2942,negated_conjecture,
    true = agent(skc16,skf1(skc25),skc25) ).

cnf(u1172,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc25),true) ).

cnf(u2159,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,abstraction(X0,skc26),true) ).

cnf(u245,negated_conjecture,
    true = sF7 ).

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

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

cnf(u1157,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc25),true,true,true),true) ).

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

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

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

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

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

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

cnf(u1487,negated_conjecture,
    true = ifeq2(unisex(skc13,skc21),true,true,true) ).

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

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

cnf(u571,negated_conjecture,
    true = general(skc13,skc18) ).

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

cnf(u278,negated_conjecture,
    true = sF18 ).

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

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

cnf(u7717,negated_conjecture,
    true = unisex(skc16,skc21) ).

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

cnf(u5729,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(u3926,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relname(X0,skc18),true,true,true),true) ).

cnf(u1612,negated_conjecture,
    true = ifeq2(accessible_world(skc16,skc13),true,true,true) ).

cnf(u230,negated_conjecture,
    true = sF2 ).

cnf(u1223,negated_conjecture,
    true = singleton(skc16,skc18) ).

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

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

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

cnf(u2284,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonhuman(X0,skc18),true,true,true),true) ).

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

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

cnf(u343,negated_conjecture,
    true = think_believe_consider(skc13,skc17) ).

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

cnf(u7716,negated_conjecture,
    true = nonexistent(skc16,skc21) ).

cnf(u948,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc24)),tuple(true,true),a,b) ).

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

cnf(u9612,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,skc16),true,ifeq3(theme(skc16,skc21,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

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

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

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

cnf(u2900,negated_conjecture,
    true = ifeq2(singleton(skc13,skf1(X0)),true,true,true) ).

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

cnf(u2960,negated_conjecture,
    true = animate(skc16,skc25) ).

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

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

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

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

cnf(u2851,negated_conjecture,
    true = ifeq2(present(skc13,skf1(X0)),true,true,true) ).

cnf(u2174,negated_conjecture,
    true = general(skc16,skc26) ).

cnf(u2069,negated_conjecture,
    true = relation(skc16,skc26) ).

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

cnf(u339,negated_conjecture,
    true = forename(skc13,skc18) ).

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

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

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

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

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

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

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

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

cnf(u7376,negated_conjecture,
    skc18 = ifeq3(of(skc16,skc18,skc25),true,skc26,skc18) ).

cnf(u6932,negated_conjecture,
    true = jules_forename(skc13,skc18) ).

cnf(u4258,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,jules_forename(X0,skc26),true) ).

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

cnf(u7657,negated_conjecture,
    skc26 = ifeq3(of(skc16,skc26,skc19),true,ifeq3(of(skc16,skc26,skc19),true,skc26,skc26),skc26) ).

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

cnf(u3137,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,entity(X0,skc25),true) ).

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

cnf(u453,negated_conjecture,
    true = unisex(skc13,skc24) ).

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

cnf(u7714,negated_conjecture,
    true = singleton(skc16,skc21) ).

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

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

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

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

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

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

cnf(u7423,negated_conjecture,
    skc18 = ifeq3(of(skc13,skc26,X0),true,ifeq3(of(skc13,skc18,X0),true,ifeq3(entity(skc13,X0),true,skc26,skc18),skc18),skc18) ).

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

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

cnf(u10347,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(u102,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(organism(X0,X2),true,organism(X1,X2),true),true) ).

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

cnf(u7710,negated_conjecture,
    true = agent(skc16,skc21,skc19) ).

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

cnf(u4255,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(jules_forename(X0,skc26),true,true,true),true) ).

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

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

cnf(u5199,negated_conjecture,
    skc26 = ifeq3(of(skc16,X1,X0),true,ifeq3(of(skc16,skc26,X0),true,ifeq3(forename(skc16,X1),true,ifeq3(entity(skc16,X0),true,X1,skc26),skc26),skc26),skc26) ).

cnf(u930,negated_conjecture,
    true = ifeq2(smoke(skc16,skc24),true,true,true) ).

cnf(u4801,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,of(X0,skc18,skc19),true) ).

cnf(u8965,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(u3935,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,relname(X0,skc18),true) ).

cnf(u4093,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(vincent_forename(X0,skc18),true,true,true),true) ).

cnf(u546,negated_conjecture,
    true = relation(skc13,skc26) ).

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

cnf(u482,negated_conjecture,
    true = ifeq2(entity(skc13,skc15),true,true,true) ).

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

cnf(u7421,negated_conjecture,
    skc18 = ifeq3(of(skc13,X0,skc25),true,ifeq3(of(skc13,skc18,skc25),true,ifeq3(forename(skc13,X0),true,X0,skc18),skc18),skc18) ).

cnf(u10138,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(u7715,negated_conjecture,
    true = specific(skc16,skc21) ).

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

cnf(u5195,negated_conjecture,
    ifeq3(of(skc13,X1,skc19),true,ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X1),true,ifeq3(forename(skc13,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u2280,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonhuman(X0,skc26),true,true,true),true) ).

cnf(u7037,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,jules_forename(X0,skc18),true) ).

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

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

cnf(u260,negated_conjecture,
    true = sF12 ).

cnf(u4465,negated_conjecture,
    true = agent(skc16,skc17,skc19) ).

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

cnf(u1200,negated_conjecture,
    true = thing(skc16,skc26) ).

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

cnf(u942,negated_conjecture,
    true = nonexistent(skc16,skc24) ).

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

cnf(u2652,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,state(X0,skc24),true) ).

cnf(u558,negated_conjecture,
    true = abstraction(skc13,skc26) ).

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

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

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

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

cnf(u8824,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,skc16),true,ifeq3(think_believe_consider(skc16,skc21),true,skc16,skc16),skc16) ).

cnf(u9590,negated_conjecture,
    ifeq3(theme(skc16,skc21,X1),true,ifeq3(theme(skc16,skc21,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

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

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

cnf(u1252,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc25),true,true,true) ).

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

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

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

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

cnf(u3934,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relname(X0,skc18),true,true,true),true) ).

cnf(u305,negated_conjecture,
    true = sF27 ).

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

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

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

cnf(u2667,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,state(X0,skc24),true) ).

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

cnf(u3260,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(existent(X0,skc25),true,true,true),true) ).

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

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

cnf(u641,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc24)),tuple(true,true),a,b) ).

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

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

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

cnf(u523,negated_conjecture,
    true = animate(skc13,skc25) ).

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

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

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

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

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

cnf(u632,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc16)),tuple(true,true),a,b) ).

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

cnf(u652,negated_conjecture,
    b = ifeq(tuple(true,human(skc13,skc18)),tuple(true,true),a,b) ).

cnf(u317,negated_conjecture,
    true = sF31 ).

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

cnf(u1039,negated_conjecture,
    true = ifeq2(thing(skc13,skc21),true,true,true) ).

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

cnf(u3592,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(animate(X0,skc25),true,true,true),true) ).

cnf(u2925,negated_conjecture,
    true = man(skc16,skc25) ).

cnf(u4492,negated_conjecture,
    true = ifeq2(agent(skc13,skf1(skc25),skc25),true,true,true) ).

cnf(u3943,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relname(X0,skc18),true) ).

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

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

cnf(u9429,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,skc16),true,ifeq3(theme(skc16,skc15,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

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

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

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

cnf(u2935,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(man(X0,skc25),true,true,true),true) ).

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

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

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

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

cnf(u4790,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,of(X0,skc26,skc25),true) ).

cnf(u5640,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X2),true,ifeq3(theme(skc16,X1,X0),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,X2),true,ifeq3(proposition(skc16,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u516,negated_conjecture,
    true = living(skc13,skc25) ).

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

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

cnf(u851,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc18),true,true,true),true) ).

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

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

cnf(u4087,negated_conjecture,
    true = vincent_forename(skc16,skc18) ).

cnf(u320,negated_conjecture,
    true = sF32 ).

cnf(u468,negated_conjecture,
    true = human_person(skc13,skc25) ).

cnf(u9393,negated_conjecture,
    ifeq3(theme(skc16,skc21,X1),true,ifeq3(theme(skc16,skc15,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X0),true,X0,X1),X1),X1),X1),X1) = X1 ).

cnf(u8994,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16) ).

cnf(u287,negated_conjecture,
    true = sF21 ).

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

cnf(u3843,negated_conjecture,
    true = relname(skc16,skc18) ).

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

cnf(u10406,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(theme(skc16,skf1(skc25),X0),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16),skc16) ).

cnf(u4443,negated_conjecture,
    true = ifeq2(agent(skc13,X1,X0),true,agent(skc16,X1,X0),true) ).

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

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

cnf(u10421,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(u735,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,eventuality(X0,skc15),true) ).

cnf(u1459,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc25),true,true,true),true) ).

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

cnf(u512,negated_conjecture,
    true = impartial(skc13,skc25) ).

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

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

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

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

cnf(u3132,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(entity(X0,skc25),true,true,true),true) ).

cnf(u810,negated_conjecture,
    true = thing(skc16,skc17) ).

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

cnf(u2480,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(general(X0,skc26),true,true,true),true) ).

cnf(u7039,negated_conjecture,
    true = jules_forename(skc16,skc18) ).

cnf(u7529,negated_conjecture,
    skc26 = ifeq3(of(skc13,skc26,skc19),true,ifeq3(of(skc13,skc26,skc19),true,skc26,skc26),skc26) ).

cnf(u3003,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,organism(X0,skc25),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u1464,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc25),true) ).

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

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

cnf(u328,negated_conjecture,
    true = jules_forename(skc13,skc26) ).

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

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

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

cnf(u1565,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc18)),tuple(true,true),a,b) ).

cnf(u3255,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(existent(X0,skc25),true,true,true),true) ).

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

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

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

cnf(u595,negated_conjecture,
    true = general(skc13,skc26) ).

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

cnf(u8912,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(u2962,negated_conjecture,
    b = ifeq(tuple(unisex(skc16,skc25),true),tuple(true,true),a,b) ).

cnf(u7741,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skc21),true,true,true),true) ).

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

cnf(u2912,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(human_person(X0,skc25),true,true,true),true) ).

cnf(u340,negated_conjecture,
    true = vincent_forename(skc13,skc18) ).

cnf(u3892,negated_conjecture,
    true = forename(skc16,skc26) ).

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

cnf(u2511,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,general(X0,skc18),true) ).

cnf(u3392,negated_conjecture,
    true = ifeq2(impartial(skc13,X0),true,impartial(skc16,X0),true) ).

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

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

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

cnf(u8238,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(u1203,negated_conjecture,
    true = ifeq2(entity(skc16,skc16),true,true,true) ).

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

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

cnf(u1934,negated_conjecture,
    b = ifeq(tuple(true,human(skc16,skc16)),tuple(true,true),a,b) ).

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

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

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

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

cnf(u1550,negated_conjecture,
    true = unisex(skc16,skc26) ).

cnf(u2974,negated_conjecture,
    true = entity(skc16,skc25) ).

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

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

cnf(u257,negated_conjecture,
    true = sF11 ).

cnf(u405,negated_conjecture,
    true = relation(skc13,skc16) ).

cnf(u5207,negated_conjecture,
    skc26 = ifeq3(of(skc13,X1,X0),true,ifeq3(of(skc13,skc26,X0),true,ifeq3(forename(skc13,X1),true,ifeq3(entity(skc13,X0),true,X1,skc26),skc26),skc26),skc26) ).

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

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

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

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

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

cnf(u3901,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(forename(X0,skc26),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u849,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc19),true,true,true),true) ).

cnf(u491,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc19),true,true,true) ).

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

cnf(u8799,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(u7738,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,smoke(X0,skc21),true) ).

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

cnf(u269,negated_conjecture,
    true = sF15 ).

cnf(u2880,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X1),true,unisex(X1,skf1(X0)),true) ).

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

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

cnf(u10176,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(u1160,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(specific(X0,skc15),true,true,true),true) ).

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

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

cnf(u733,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,eventuality(X0,skc24),true) ).

cnf(u7043,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,jules_forename(X0,skc18),true) ).

cnf(u615,negated_conjecture,
    true = singleton(skc13,skc26) ).

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

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

cnf(u2834,negated_conjecture,
    true = entity(skc16,skc19) ).

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

cnf(u596,negated_conjecture,
    true = unisex(skc13,skc26) ).

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

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

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

cnf(u7704,negated_conjecture,
    skc14 = skc16 ).

cnf(u931,negated_conjecture,
    true = eventuality(skc16,skc24) ).

cnf(u254,negated_conjecture,
    true = sF10 ).

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

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

cnf(u4095,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,vincent_forename(X0,skc18),true) ).

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

cnf(u597,negated_conjecture,
    true = ifeq2(entity(skc13,skc18),true,true,true) ).

cnf(u2959,negated_conjecture,
    true = human(skc16,skc25) ).

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

cnf(u3923,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relname(X0,skc26),true,true,true),true) ).

cnf(u976,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc26),true,true,true),true) ).

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

cnf(u1411,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc18),true,true,true),true) ).

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

cnf(u4286,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,jules_forename(X0,skc26),true) ).

cnf(u3540,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(human(X0,skc25),true,true,true),true) ).

cnf(u943,negated_conjecture,
    true = specific(skc16,skc24) ).

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

cnf(u9275,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(u47,axiom,
    true = ifeq2(organism(X0,X1),true,impartial(X0,X1),true) ).

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

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

cnf(u3838,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(forename(X0,skc18),true,true,true),true) ).

cnf(u593,negated_conjecture,
    true = thing(skc13,skc26) ).

cnf(u8169,negated_conjecture,
    true = theme(skc16,skc15,skc16) ).

cnf(u1452,negated_conjecture,
    true = specific(skc16,skc25) ).

cnf(u363,negated_conjecture,
    true = ifeq2(smoke(skc13,skc17),true,true,true) ).

cnf(u1008,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc25),true) ).

cnf(u8802,negated_conjecture,
    ifeq3(theme(skc16,skc21,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0) = X0 ).

cnf(u3380,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(impartial(X0,skc25),true,true,true),true) ).

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

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

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

cnf(u939,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skc24),true,true,true),true) ).

cnf(u10143,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(u1416,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u4963,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,be(X0,skc24,skc25,skc25),true) ).

cnf(clause71,axiom,
    ifeq3(theme(X0,X1,X2),true,ifeq3(theme(X0,X3,X4),true,ifeq3(agent(X0,X1,X5),true,ifeq3(agent(X0,X3,X5),true,ifeq3(think_believe_consider(X0,X1),true,ifeq3(think_believe_consider(X0,X3),true,ifeq3(proposition(X0,X2),true,ifeq3(proposition(X0,X4),true,X4,X2),X2),X2),X2),X2),X2),X2),X2) = X2 ).

cnf(u1255,negated_conjecture,
    true = singleton(skc16,skc25) ).

cnf(u7870,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc21),true,true,true),true) ).

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

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

cnf(u7591,negated_conjecture,
    skc18 = ifeq3(of(skc16,skc26,X0),true,ifeq3(of(skc16,skc18,X0),true,ifeq3(entity(skc16,X0),true,skc26,skc18),skc18),skc18) ).

cnf(u8782,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(u1645,negated_conjecture,
    true = ifeq2(present(X0,skc17),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u5194,negated_conjecture,
    ifeq3(of(skc13,X1,skc25),true,ifeq3(of(skc13,X0,skc25),true,ifeq3(forename(skc13,X1),true,ifeq3(forename(skc13,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u8785,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(u7422,negated_conjecture,
    skc18 = ifeq3(of(skc13,skc18,X0),true,ifeq3(of(skc13,skc18,X0),true,ifeq3(entity(skc13,X0),true,skc18,skc18),skc18),skc18) ).

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

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

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

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

cnf(u9526,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(u126,axiom,
    true = ifeq2(agent(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).

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

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

cnf(u8447,negated_conjecture,
    ifeq3(of(skc16,skc18,skc25),true,ifeq3(of(skc16,X0,skc25),true,ifeq3(forename(skc16,X0),true,skc18,X0),X0),X0) = X0 ).

cnf(u4828,negated_conjecture,
    true = of(skc16,skc26,skc25) ).

cnf(u2992,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(organism(X0,skc25),true,true,true),true) ).

cnf(u272,negated_conjecture,
    true = sF16 ).

cnf(u3844,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,forename(X0,skc18),true) ).

cnf(u4444,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skf1(skc25),skc25),true) ).

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

cnf(u224,negated_conjecture,
    true = sF0 ).

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

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

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

cnf(u8567,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(u1973,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relation(X0,skc16),true,true,true),true) ).

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

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

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

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

cnf(u485,negated_conjecture,
    true = thing(skc13,skc25) ).

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

cnf(u284,negated_conjecture,
    true = sF20 ).

cnf(u4784,negated_conjecture,
    true = ifeq2(of(X0,skc18,skc19),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u416,negated_conjecture,
    true = thing(skc13,skc16) ).

cnf(u9353,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,skc16),true,ifeq3(theme(skc16,skc17,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u5324,negated_conjecture,
    skc18 = ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X0),true,X0,skc18),skc18) ).

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

cnf(u236,negated_conjecture,
    true = sF4 ).

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

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

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

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

cnf(u10178,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,skc25),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

cnf(u1430,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc26),true) ).

cnf(u7742,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skc21),true) ).

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

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

cnf(u982,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc18),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(u5615,negated_conjecture,
    skc16 = ifeq3(theme(skc13,X3,skc16),true,ifeq3(theme(skc13,X2,X1),true,ifeq3(agent(skc13,X3,X0),true,ifeq3(agent(skc13,X2,X0),true,ifeq3(think_believe_consider(skc13,X3),true,ifeq3(think_believe_consider(skc13,X2),true,ifeq3(proposition(skc13,X1),true,X1,skc16),skc16),skc16),skc16),skc16),skc16),skc16) ).

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

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

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

cnf(u3266,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,existent(X0,skc25),true) ).

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

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

cnf(u345,negated_conjecture,
    true = present(skc13,skc15) ).

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

cnf(u4832,negated_conjecture,
    true = ifeq2(of(X0,skc26,skc25),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u7720,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc21),true,true,true) ).

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

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

cnf(u7036,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(jules_forename(X0,skc18),true,true,true),true) ).

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

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

cnf(u846,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc25),true,true,true),true) ).

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

cnf(u8413,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(u96,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(state(X0,X2),true,state(X1,X2),true),true) ).

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

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

cnf(u451,negated_conjecture,
    true = specific(skc13,skc24) ).

cnf(u8876,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(agent(skc16,skc17,skc25),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,skc16,skc16),skc16),skc16) ).

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

cnf(u9614,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,skc16),true,ifeq3(theme(skc16,skc21,skc16),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(think_believe_consider(skc16,skc21),true,skc16,skc16),skc16),skc16),skc16) ).

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

cnf(u2876,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc16),true,ifeq2(unisex(X1,skf1(X0)),true,true,true),true) ).

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

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

cnf(u1262,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc26),true,true,true) ).

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

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

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

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

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

cnf(u463,negated_conjecture,
    true = ifeq2(smoke(skc13,skc24),true,true,true) ).

cnf(u8732,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(u536,negated_conjecture,
    true = relname(skc13,skc26) ).

cnf(u2998,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,organism(X0,skc25),true) ).

cnf(u1302,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skc24),true) ).

cnf(u684,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(event(X0,skc24),true,true,true),true) ).

cnf(u7503,negated_conjecture,
    skc26 = ifeq3(of(skc13,X0,skc19),true,ifeq3(of(skc13,skc26,skc19),true,ifeq3(forename(skc13,X0),true,X0,skc26),skc26),skc26) ).

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

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

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

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

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

cnf(u1254,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc25),true,true,true) ).

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

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

cnf(u7705,negated_conjecture,
    true = event(skc16,skc21) ).

cnf(u685,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,event(X0,skc24),true) ).

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

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

cnf(u10095,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(u327,negated_conjecture,
    true = actual_world(skc13) ).

cnf(u932,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,event(X0,skc24),true) ).

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

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

cnf(u548,negated_conjecture,
    true = ifeq2(proposition(skc13,skc18),true,true,true) ).

cnf(u1972,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relation(X0,skc18),true,true,true),true) ).

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

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

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

cnf(u2953,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(human_person(X0,skc25),true,true,true),true) ).

cnf(u352,negated_conjecture,
    true = of(skc13,skc26,skc25) ).

cnf(u549,negated_conjecture,
    true = abstraction(skc13,skc18) ).

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

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

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

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

cnf(u323,negated_conjecture,
    true = sF33 ).

cnf(u8156,negated_conjecture,
    true = ifeq2(agent(X0,skc21,skc19),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u670,negated_conjecture,
    true = ifeq2(smoke(skc13,skc21),true,true,true) ).

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

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

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

cnf(u3492,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(living(X0,skc25),true,true,true),true) ).

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

cnf(u4947,negated_conjecture,
    true = ifeq2(be(X0,skc24,skc25,skc25),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

cnf(u3818,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(forename(X0,skc18),true,true,true),true) ).

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

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

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

cnf(u8834,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(u9065,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc25),X0),true,ifeq3(agent(skc16,skc15,skc25),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

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

cnf(u3819,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,forename(X0,skc18),true) ).

cnf(u4799,negated_conjecture,
    true = ifeq2(of(X0,skc18,skc19),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

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

cnf(u940,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skc24),true) ).

cnf(u9625,negated_conjecture,
    ifeq3(theme(skc16,skc21,X0),true,ifeq3(theme(skc16,skf1(skc19),X1),true,ifeq3(think_believe_consider(skc16,skc21),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(u763,negated_conjecture,
    true = ifeq2(entity(skc16,skc15),true,true,true) ).

cnf(u1009,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc26),true) ).

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

cnf(u9656,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skc21,skc16),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

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

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

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

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

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

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

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

cnf(u557,negated_conjecture,
    true = ifeq2(proposition(skc13,skc26),true,true,true) ).

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

cnf(u3136,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(entity(X0,skc25),true,true,true),true) ).

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

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

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

cnf(u7589,negated_conjecture,
    skc18 = ifeq3(of(skc16,X0,skc25),true,ifeq3(of(skc16,skc18,skc25),true,ifeq3(forename(skc16,X0),true,X0,skc18),skc18),skc18) ).

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

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

cnf(u5316,negated_conjecture,
    skc26 = ifeq3(of(skc16,X0,skc25),true,ifeq3(forename(skc16,X0),true,X0,skc26),skc26) ).

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

cnf(u9187,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(u82,axiom,
    true = ifeq2(present(X0,X1),true,ifeq2(accessible_world(X0,X2),true,present(X2,X1),true),true) ).

cnf(u3551,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,human(X0,skc25),true) ).

cnf(u9560,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(u9529,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skc21,X1),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,ifeq3(proposition(skc16,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u926,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(event(X0,skc24),true,true,true),true) ).

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

cnf(u10725,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc19),X1),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,X1),true,ifeq3(proposition(skc16,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u543,negated_conjecture,
    true = relation(skc13,skc18) ).

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

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

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

cnf(u885,negated_conjecture,
    true = ifeq2(event(skc13,skc21),true,true,true) ).

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

cnf(u330,negated_conjecture,
    true = man(skc13,skc25) ).

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

cnf(u4795,negated_conjecture,
    true = of(skc16,skc18,skc19) ).

cnf(u2075,negated_conjecture,
    true = abstraction(skc16,skc18) ).

cnf(u3006,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc16,skc25),true),tuple(true,true),a,b) ).

cnf(u1236,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc19),true,true,true) ).

cnf(u7631,negated_conjecture,
    skc26 = ifeq3(of(skc16,X0,skc19),true,ifeq3(of(skc16,skc26,skc19),true,ifeq3(forename(skc16,X0),true,X0,skc26),skc26),skc26) ).

cnf(u437,negated_conjecture,
    true = unisex(skc13,skc16) ).

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

cnf(u2651,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(state(X0,skc24),true,true,true),true) ).

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

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

cnf(u1546,negated_conjecture,
    true = unisex(skc16,skc18) ).

cnf(u8599,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(u7894,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,nonexistent(X0,skc21),true) ).

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

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

cnf(u635,negated_conjecture,
    b = ifeq(tuple(unisex(skc13,skc25),true),tuple(true,true),a,b) ).

cnf(u1219,negated_conjecture,
    true = ifeq2(entity(skc16,skc18),true,true,true) ).

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

cnf(u7042,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(jules_forename(X0,skc18),true,true,true),true) ).

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

cnf(u342,negated_conjecture,
    true = present(skc13,skc17) ).

cnf(u9489,negated_conjecture,
    ifeq3(theme(skc16,skc17,X0),true,ifeq3(theme(skc16,skc21,skc16),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

cnf(u7361,negated_conjecture,
    skc18 = ifeq3(of(skc16,skc26,skc19),true,skc26,skc18) ).

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

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

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

cnf(u5216,negated_conjecture,
    ifeq3(of(skc13,skc18,X1),true,ifeq3(of(skc13,X0,X1),true,ifeq3(forename(skc13,X0),true,ifeq3(entity(skc13,X1),true,skc18,X0),X0),X0),X0) = X0 ).

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

cnf(u7261,negated_conjecture,
    skc18 = ifeq3(of(skc13,skc18,skc25),true,skc26,skc18) ).

cnf(u519,negated_conjecture,
    true = human(skc13,skc25) ).

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

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

cnf(u1305,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonexistent(X0,skc24),true) ).

cnf(u8991,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(u7736,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skc21)),tuple(true,true),a,b) ).

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

cnf(u5319,negated_conjecture,
    skc18 = ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X0),true,X0,skc18),skc18) ).

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

cnf(u3385,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,impartial(X0,skc25),true) ).

cnf(u6931,negated_conjecture,
    skc20 = skc18 ).

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

cnf(u452,negated_conjecture,
    true = nonexistent(skc13,skc24) ).

cnf(u1407,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(unisex(X0,skc26),true,true,true),true) ).

cnf(u629,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc18)),tuple(true,true),a,b) ).

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

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

cnf(u761,negated_conjecture,
    b = ifeq(tuple(true,existent(skc16,skc15)),tuple(true,true),a,b) ).

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

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

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

cnf(u3946,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relname(X0,skc26),true) ).

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

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

cnf(u3649,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(male(X0,skc25),true,true,true),true) ).

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

cnf(u1983,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relation(X0,skc18),true) ).

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

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

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

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

cnf(u10175,negated_conjecture,
    skc16 = ifeq3(theme(skc16,X0,skc16),true,ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(agent(skc16,X0,skc25),true,ifeq3(think_believe_consider(skc16,X0),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

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

cnf(u444,negated_conjecture,
    true = eventuality(skc13,skc24) ).

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

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

cnf(u625,negated_conjecture,
    b = ifeq(tuple(true,male(skc13,skc26)),tuple(true,true),a,b) ).

cnf(u7728,negated_conjecture,
    true = ifeq2(entity(skc16,skc21),true,true,true) ).

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

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

cnf(u7632,negated_conjecture,
    skc26 = ifeq3(of(skc16,skc18,X0),true,ifeq3(of(skc16,skc26,X0),true,ifeq3(entity(skc16,X0),true,skc18,skc26),skc26),skc26) ).

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

cnf(u2182,negated_conjecture,
    b = ifeq(tuple(specific(skc16,skc26),true),tuple(true,true),a,b) ).

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

cnf(u7737,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(smoke(X0,skc21),true,true,true),true) ).

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

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

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

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

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

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

cnf(u8969,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(u2292,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonhuman(X0,skc26),true,true,true),true) ).

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

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

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

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

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

cnf(u637,negated_conjecture,
    b = ifeq(tuple(true,general(skc13,skc25)),tuple(true,true),a,b) ).

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

cnf(u8158,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,agent(X0,skc21,skc19),true) ).

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

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

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

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

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

cnf(u7381,negated_conjecture,
    skc26 = ifeq3(of(skc16,skc26,skc19),true,skc18,skc26) ).

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

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

cnf(u3904,negated_conjecture,
    true = ifeq2(vincent_forename(skc16,skc26),true,true,true) ).

cnf(u3815,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(forename(X0,skc26),true,true,true),true) ).

cnf(u5191,negated_conjecture,
    ifeq3(of(skc16,X1,skc19),true,ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X1),true,ifeq3(forename(skc16,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u2836,negated_conjecture,
    true = living(skc16,skc19) ).

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

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

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

cnf(u2659,negated_conjecture,
    true = state(skc16,skc24) ).

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

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

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

cnf(u275,negated_conjecture,
    true = sF17 ).

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

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

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

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

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

cnf(u5211,negated_conjecture,
    ifeq3(of(skc16,skc26,X1),true,ifeq3(of(skc16,X0,X1),true,ifeq3(forename(skc16,X0),true,ifeq3(entity(skc16,X1),true,skc26,X0),X0),X0),X0) = X0 ).

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

cnf(u2155,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,abstraction(X0,skc18),true) ).

cnf(u2958,negated_conjecture,
    true = organism(skc16,skc25) ).

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

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

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

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

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

cnf(u389,negated_conjecture,
    true = specific(skc13,skc15) ).

cnf(u2917,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,human_person(X0,skc25),true) ).

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

cnf(u3829,negated_conjecture,
    true = forename(skc16,skc18) ).

cnf(u2845,negated_conjecture,
    true = ifeq2(smoke(skc13,skf1(X0)),true,true,true) ).

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

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

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

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

cnf(u7504,negated_conjecture,
    skc26 = ifeq3(of(skc13,skc18,X0),true,ifeq3(of(skc13,skc26,X0),true,ifeq3(entity(skc13,X0),true,skc18,skc26),skc26),skc26) ).

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

cnf(u9722,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc21,skc16),true,ifeq3(theme(skc16,X0,skc16),true,ifeq3(agent(skc16,X0,skc19),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(think_believe_consider(skc16,X0),true,skc16,skc16),skc16),skc16),skc16),skc16) ).

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

cnf(u475,negated_conjecture,
    true = entity(skc13,skc19) ).

cnf(u10196,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,skc16,skc16),skc16),skc16),skc16) ).

cnf(u422,negated_conjecture,
    true = singleton(skc13,skc16) ).

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

cnf(u381,negated_conjecture,
    true = singleton(skc13,skc15) ).

cnf(u1165,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc24),true) ).

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

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

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

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

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

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

cnf(u1426,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,unisex(X0,skc18),true) ).

cnf(u570,negated_conjecture,
    true = nonhuman(skc13,skc18) ).

cnf(u5219,negated_conjecture,
    ifeq3(of(skc13,skc26,X1),true,ifeq3(of(skc13,X0,X1),true,ifeq3(forename(skc13,X0),true,ifeq3(entity(skc13,X1),true,skc26,X0),X0),X0),X0) = X0 ).

cnf(u524,negated_conjecture,
    true = animate(skc13,skc19) ).

cnf(u599,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc18),true,true,true) ).

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

cnf(u845,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(thing(X0,skc26),true,true,true),true) ).

cnf(u487,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc25),true,true,true) ).

cnf(u5339,negated_conjecture,
    ifeq3(of(skc13,X0,skc25),true,ifeq3(forename(skc13,X0),true,skc26,X0),X0) = X0 ).

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

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

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

cnf(u1620,negated_conjecture,
    true = ifeq2(present(X0,skc17),true,ifeq2(accessible_world(X0,skc13),true,true,true),true) ).

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

cnf(u4079,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,vincent_forename(X0,skc18),true) ).

cnf(u7356,negated_conjecture,
    skc26 = ifeq3(of(skc16,skc18,skc25),true,skc18,skc26) ).

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

cnf(u351,negated_conjecture,
    true = state(skc13,skc24) ).

cnf(u2099,negated_conjecture,
    true = abstraction(skc16,skc26) ).

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

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

cnf(u3907,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,forename(X0,skc26),true) ).

cnf(u430,negated_conjecture,
    true = general(skc13,skc16) ).

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

cnf(u2175,negated_conjecture,
    true = nonhuman(skc16,skc26) ).

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

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

cnf(clause70,axiom,
    ifeq3(of(X0,X1,X2),true,ifeq3(of(X0,X3,X2),true,ifeq3(forename(X0,X1),true,ifeq3(forename(X0,X3),true,ifeq3(entity(X0,X2),true,X1,X3),X3),X3),X3),X3) = X3 ).

cnf(u572,negated_conjecture,
    true = unisex(skc13,skc18) ).

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

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

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

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

cnf(u1301,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(nonexistent(X0,skc24),true,true,true),true) ).

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

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

cnf(u3822,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,forename(X0,skc26),true) ).

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

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

cnf(u2065,negated_conjecture,
    true = relation(skc16,skc18) ).

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

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

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

cnf(u9313,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(u1334,negated_conjecture,
    true = ifeq2(singleton(skc13,skc21),true,true,true) ).

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

cnf(u7607,negated_conjecture,
    skc18 = ifeq3(of(skc16,skc18,skc25),true,ifeq3(of(skc16,skc18,skc25),true,skc18,skc18),skc18) ).

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

cnf(u923,negated_conjecture,
    true = event(skc16,skc24) ).

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

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

cnf(u9440,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(u1239,negated_conjecture,
    true = singleton(skc16,skc19) ).

cnf(u461,negated_conjecture,
    true = event(skc13,skc24) ).

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

cnf(u569,negated_conjecture,
    true = thing(skc13,skc18) ).

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

cnf(u1298,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(nonexistent(X0,skc24),true,true,true),true) ).

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

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

cnf(u359,negated_conjecture,
    true = theme(skc13,skc17,skc16) ).

cnf(u1629,negated_conjecture,
    true = ifeq2(present(skc13,skc21),true,true,true) ).

cnf(u290,negated_conjecture,
    true = sF22 ).

cnf(u7633,negated_conjecture,
    skc26 = ifeq3(of(skc16,skc26,X0),true,ifeq3(of(skc16,skc26,X0),true,ifeq3(entity(skc16,X0),true,skc26,skc26),skc26),skc26) ).

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

cnf(u5327,negated_conjecture,
    skc26 = ifeq3(of(skc13,X0,skc25),true,ifeq3(forename(skc13,X0),true,X0,skc26),skc26) ).

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

cnf(u659,negated_conjecture,
    b = ifeq(tuple(true,existent(skc13,skc24)),tuple(true,true),a,b) ).

cnf(u2183,negated_conjecture,
    b = ifeq(tuple(true,human(skc16,skc26)),tuple(true,true),a,b) ).

cnf(u3650,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,male(X0,skc25),true) ).

cnf(u4278,negated_conjecture,
    true = jules_forename(skc16,skc26) ).

cnf(u2311,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonhuman(X0,skc18),true) ).

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

cnf(u242,negated_conjecture,
    true = sF6 ).

cnf(u10326,negated_conjecture,
    ifeq3(theme(skc16,skf1(skc25),X0),true,ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

cnf(u9500,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(u2976,negated_conjecture,
    true = living(skc16,skc25) ).

cnf(u227,negated_conjecture,
    true = sF1 ).

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

cnf(u3545,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(human(X0,skc25),true,true,true),true) ).

cnf(u1968,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(relation(X0,skc26),true,true,true),true) ).

cnf(u355,negated_conjecture,
    true = of(skc13,skc18,skc19) ).

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

cnf(u302,negated_conjecture,
    true = sF26 ).

cnf(u2484,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(general(X0,skc18),true,true,true),true) ).

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

cnf(u2665,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(state(X0,skc24),true,true,true),true) ).

cnf(u490,negated_conjecture,
    true = singleton(skc13,skc25) ).

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

cnf(u4955,negated_conjecture,
    true = be(skc16,skc24,skc25,skc25) ).

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

cnf(u4078,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(vincent_forename(X0,skc18),true,true,true),true) ).

cnf(u9364,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(u2997,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(organism(X0,skc25),true,true,true),true) ).

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

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

cnf(u7877,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,specific(X0,skc21),true) ).

cnf(u239,negated_conjecture,
    true = sF5 ).

cnf(u5190,negated_conjecture,
    ifeq3(of(skc16,X1,skc25),true,ifeq3(of(skc16,X0,skc25),true,ifeq3(forename(skc16,X1),true,ifeq3(forename(skc16,X0),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u2939,negated_conjecture,
    true = human_person(skc16,skc25) ).

cnf(u9239,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(u7910,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,unisex(X0,skc21),true) ).

cnf(u7731,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc21)),tuple(true,true),a,b) ).

cnf(u5331,negated_conjecture,
    ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X0),true,skc18,X0),X0) = X0 ).

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

cnf(u977,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(singleton(X0,skc25),true,true,true),true) ).

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

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

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

cnf(u7251,negated_conjecture,
    skc26 = ifeq3(of(skc13,skc18,skc25),true,skc18,skc26) ).

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

cnf(u648,negated_conjecture,
    b = ifeq(tuple(true,human(skc13,skc26)),tuple(true,true),a,b) ).

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

cnf(u3645,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(male(X0,skc25),true,true,true),true) ).

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

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

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

cnf(u1373,negated_conjecture,
    true = ifeq2(specific(skc13,skc21),true,true,true) ).

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

cnf(u946,negated_conjecture,
    true = ifeq2(abstraction(skc16,skc24),true,true,true) ).

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

cnf(u7505,negated_conjecture,
    skc26 = ifeq3(of(skc13,skc26,X0),true,ifeq3(of(skc13,skc26,X0),true,ifeq3(entity(skc13,X0),true,skc26,skc26),skc26),skc26) ).

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

cnf(u3906,negated_conjecture,
    true = relname(skc16,skc26) ).

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

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

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

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

cnf(u660,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc13,skc25),true),tuple(true,true),a,b) ).

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

cnf(u1018,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc21),true,true,true) ).

cnf(u329,negated_conjecture,
    true = forename(skc13,skc26) ).

cnf(u9549,negated_conjecture,
    ifeq3(theme(skc16,skc15,X0),true,ifeq3(theme(skc16,skc21,skc16),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0) = X0 ).

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

cnf(u7938,negated_conjecture,
    true = ifeq2(present(X0,skc21),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

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

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

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

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

cnf(u7590,negated_conjecture,
    skc18 = ifeq3(of(skc16,skc18,X0),true,ifeq3(of(skc16,skc18,X0),true,ifeq3(entity(skc16,X0),true,skc18,skc18),skc18),skc18) ).

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

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

cnf(u3141,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,entity(X0,skc25),true) ).

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

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

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

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

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

cnf(u5204,negated_conjecture,
    skc18 = ifeq3(of(skc13,X1,X0),true,ifeq3(of(skc13,skc18,X0),true,ifeq3(forename(skc13,X1),true,ifeq3(entity(skc13,X0),true,X1,skc18),skc18),skc18),skc18) ).

cnf(u476,negated_conjecture,
    true = entity(skc13,skc25) ).

cnf(u9100,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skf1(skc25),skc16),true,ifeq3(agent(skc16,skc15,skc25),true,ifeq3(think_believe_consider(skc16,skf1(skc25)),true,skc16,skc16),skc16),skc16) ).

cnf(u657,negated_conjecture,
    b = ifeq(tuple(true,existent(skc13,skc17)),tuple(true,true),a,b) ).

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

cnf(u3261,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,existent(X0,skc25),true) ).

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

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

cnf(u646,negated_conjecture,
    b = ifeq(tuple(specific(skc13,skc18),true),tuple(true,true),a,b) ).

cnf(u3389,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,impartial(X0,skc25),true) ).

cnf(u6930,negated_conjecture,
    skc22 = skc18 ).

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

cnf(u2982,negated_conjecture,
    true = existent(skc16,skc25) ).

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

cnf(u1003,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,singleton(X0,skc18),true) ).

cnf(u10207,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(u9001,negated_conjecture,
    skc16 = ifeq3(theme(skc16,skc15,X0),true,ifeq3(proposition(skc16,X0),true,X0,skc16),skc16) ).

cnf(u2941,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,man(X0,skc25),true) ).

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

cnf(u1238,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc19),true,true,true) ).

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

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

cnf(u3488,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(living(X0,skc25),true,true,true),true) ).

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

cnf(u642,negated_conjecture,
    b = ifeq(tuple(specific(skc13,skc26),true),tuple(true,true),a,b) ).

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

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

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

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

cnf(u867,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,thing(X0,skc25),true) ).

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

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

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

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

cnf(u533,negated_conjecture,
    true = relname(skc13,skc18) ).

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

cnf(u7733,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc21)),tuple(true,true),a,b) ).

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

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

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

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

cnf(u2104,negated_conjecture,
    true = nonhuman(skc16,skc18) ).

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

cnf(u654,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc13,skc25),true),tuple(true,true),a,b) ).

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

cnf(u528,negated_conjecture,
    true = male(skc13,skc25) ).

cnf(u1194,negated_conjecture,
    true = thing(skc16,skc18) ).

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

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

cnf(u2315,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,nonhuman(X0,skc26),true) ).

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

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

cnf(u7757,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,eventuality(X0,skc21),true) ).

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

cnf(u5328,negated_conjecture,
    ifeq3(of(skc16,X0,skc25),true,ifeq3(forename(skc16,X0),true,skc26,X0),X0) = X0 ).

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

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

cnf(u299,negated_conjecture,
    true = sF25 ).

cnf(u7713,negated_conjecture,
    true = thing(skc16,skc21) ).

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

cnf(u3931,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(relname(X0,skc26),true,true,true),true) ).

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

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

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

cnf(u454,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc24),true,true,true) ).

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

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

cnf(u728,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc13),true,ifeq2(eventuality(X0,skc24),true,true,true),true) ).

cnf(u3597,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(animate(X0,skc25),true,true,true),true) ).

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

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

cnf(u413,negated_conjecture,
    true = ifeq2(abstraction(skc13,skc17),true,true,true) ).

cnf(u9317,negated_conjecture,
    ifeq3(theme(skc16,skc21,X1),true,ifeq3(theme(skc16,skc17,X0),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X1),true,ifeq3(proposition(skc16,X0),true,X0,X1),X1),X1),X1),X1) = X1 ).

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

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

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

cnf(u6923,negated_conjecture,
    skc18 = ifeq3(of(skc13,skc26,skc19),true,skc26,skc18) ).

cnf(u1453,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(specific(X0,skc19),true,true,true),true) ).

cnf(u7940,negated_conjecture,
    true = ifeq2(accessible_world(skc16,X0),true,present(X0,skc21),true) ).

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

cnf(u4960,negated_conjecture,
    true = ifeq2(be(X0,skc24,skc25,skc25),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

cnf(u311,negated_conjecture,
    true = sF29 ).

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

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

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

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

cnf(u759,negated_conjecture,
    b = ifeq(tuple(true,male(skc16,skc15)),tuple(true,true),a,b) ).

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

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

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

cnf(u2978,negated_conjecture,
    b = ifeq(tuple(nonhuman(skc16,skc25),true),tuple(true,true),a,b) ).

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

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

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

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

cnf(u7754,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc16),true,ifeq2(eventuality(X0,skc21),true,true,true),true) ).

cnf(u501,negated_conjecture,
    true = specific(skc13,skc25) ).

cnf(u2176,negated_conjecture,
    b = ifeq(tuple(true,human(skc16,skc18)),tuple(true,true),a,b) ).

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

cnf(u5336,negated_conjecture,
    ifeq3(of(skc13,X0,skc19),true,ifeq3(forename(skc13,X0),true,skc18,X0),X0) = X0 ).

cnf(u3603,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,animate(X0,skc25),true) ).

cnf(u3497,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,living(X0,skc25),true) ).

cnf(u1987,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,relation(X0,skc26),true) ).

cnf(u1222,negated_conjecture,
    true = ifeq2(eventuality(skc16,skc18),true,true,true) ).

cnf(u1168,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,specific(X0,skc24),true) ).

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

cnf(u2074,negated_conjecture,
    true = ifeq2(proposition(skc16,skc18),true,true,true) ).

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

cnf(u9611,negated_conjecture,
    ifeq3(theme(skc16,skc21,X0),true,ifeq3(theme(skc16,skc21,skc16),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(think_believe_consider(skc16,skc21),true,ifeq3(proposition(skc16,X0),true,skc16,X0),X0),X0),X0),X0) = X0 ).

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

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

cnf(u4486,negated_conjecture,
    true = ifeq2(agent(skc13,skc21,skc19),true,true,true) ).

cnf(u10092,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(u1199,negated_conjecture,
    true = thing(skc16,skc25) ).

cnf(u8235,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(u421,negated_conjecture,
    true = ifeq2(eventuality(skc13,skc16),true,true,true) ).

cnf(u2940,negated_conjecture,
    true = male(skc16,skc25) ).

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

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

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

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

cnf(u8469,negated_conjecture,
    ifeq3(of(skc16,skc26,skc19),true,ifeq3(of(skc16,X0,skc19),true,ifeq3(forename(skc16,X0),true,skc26,X0),X0),X0) = X0 ).

cnf(u1461,negated_conjecture,
    b = ifeq(tuple(true,general(skc16,skc25)),tuple(true,true),a,b) ).

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

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

cnf(u4787,negated_conjecture,
    true = ifeq2(accessible_world(skc13,X0),true,of(X0,skc18,skc19),true) ).

cnf(u10179,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(u7256,negated_conjecture,
    skc26 = ifeq3(of(skc13,skc26,skc19),true,skc18,skc26) ).

cnf(u507,negated_conjecture,
    true = existent(skc13,skc25) ).

cnf(u326,negated_conjecture,
    true = sF34 ).

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

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

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

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

cnf(u9061,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(u600,negated_conjecture,
    true = singleton(skc13,skc18) ).

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

cnf(u4441,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc25),skc25),true,ifeq2(accessible_world(X0,skc16),true,true,true),true) ).

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

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


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : NLP249-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.35  % Computer : n011.cluster.edu
% 0.11/0.35  % Model    : x86_64 x86_64
% 0.11/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35  % Memory   : 8046.5625MB
% 0.11/0.35  % OS       : Linux 6.8.0-71-generic
% 0.11/0.35  % CPULimit : 300
% 0.11/0.35  % WCLimit  : 300
% 0.11/0.35  % DateTime : Sun Sep 27 18:37:00 UTC 2026
% 0.11/0.35  % CPUTime  : 
% 0.11/0.35  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39  Running first-order theorem proving
% 0.13/0.39  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
% 14.32/2.83  % (2678729)Detected a unit-equality problem, will run specialized UEQ schedule.
% 14.32/2.83  % (2678782)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=107508172:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 14.32/2.83  % (2678783)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=3947250774:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 14.32/2.83  % (2678785)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3684700881:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 14.32/2.83  % (2678784)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1681476528:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 14.32/2.83  % (2678787)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2127791534:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 14.32/2.83  % (2678786)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3976532968:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 14.32/2.83  % (2678788)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2866233516:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 14.32/2.83  % (2678785)Instruction limit reached! 
% 14.32/2.83  % (2678785)------------------------------
% 14.32/2.83  % (2678785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.32/2.83  % (2678785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.32/2.83  % (2678785)CaDiCaL version: 2.1.3
% 14.32/2.83  % (2678785)Termination reason: Instruction limit
% 14.32/2.83  % (2678785)Termination phase: Saturation
% 14.32/2.83  % (2678785)Time elapsed: 0.071 s
% 14.32/2.83  % (2678785)Peak memory usage: 88 MB
% 14.32/2.83  % (2678785)Instructions burned: 137 (million)
% 14.32/2.83  % (2678786)Instruction limit reached! 
% 14.32/2.83  % (2678786)------------------------------
% 14.32/2.83  % (2678786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.32/2.83  % (2678786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.32/2.83  % (2678786)CaDiCaL version: 2.1.3
% 14.32/2.83  % (2678786)Termination reason: Instruction limit
% 14.32/2.83  % (2678786)Termination phase: Saturation
% 14.32/2.83  % (2678786)Time elapsed: 0.101 s
% 14.32/2.83  % (2678786)Peak memory usage: 89 MB
% 14.32/2.83  % (2678786)Instructions burned: 181 (million)
% 14.32/2.83  % (2678787)Instruction limit reached! 
% 14.32/2.83  % (2678787)------------------------------
% 14.32/2.83  % (2678787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.32/2.83  % (2678787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.32/2.83  % (2678787)CaDiCaL version: 2.1.3
% 14.32/2.83  % (2678787)Termination reason: Instruction limit
% 14.32/2.83  % (2678787)Termination phase: Saturation
% 14.32/2.83  % (2678787)Time elapsed: 0.195 s
% 14.32/2.83  % (2678787)Peak memory usage: 91 MB
% 14.32/2.83  % (2678787)Instructions burned: 257 (million)
% 14.32/2.83  % (2678796)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=959844560:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 14.32/2.83  % (2678797)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1301145686:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 14.32/2.83  % (2678798)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=4255508412:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 14.32/2.83  % (2678788)Refutation not found, incomplete strategy
% 14.32/2.83  % (2678788)------------------------------
% 14.32/2.83  % (2678788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.32/2.83  % (2678788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.32/2.83  % (2678788)CaDiCaL version: 2.1.3
% 14.32/2.83  % (2678788)Termination reason: Refutation not found, incomplete strategy
% 14.32/2.83  % (2678788)Time elapsed: 0.499 s
% 14.32/2.83  % (2678788)Peak memory usage: 95 MB
% 14.32/2.83  % (2678788)Instructions burned: 788 (million)
% 14.32/2.83  % (2678798)Instruction limit reached! 
% 14.32/2.83  % (2678798)------------------------------
% 14.32/2.83  % (2678798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.32/2.83  % (2678798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.32/2.83  % (2678798)CaDiCaL version: 2.1.3
% 14.32/2.83  % (2678798)Termination reason: Instruction limit
% 14.32/2.83  % (2678798)Termination phase: Saturation
% 14.32/2.83  % (2678798)Time elapsed: 0.170 s
% 14.32/2.83  % (2678798)Peak memory usage: 93 MB
% 14.32/2.83  % (2678798)Instructions burned: 216 (million)
% 14.32/2.83  % (2678818)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=1995583417:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2992 on theBenchmark for (2992ds/317Mi)
% 14.32/2.83  % (2678788)------------------------------
% 14.32/2.83  % (2678788)------------------------------
% 14.32/2.83  % (2678818)Instruction limit reached! 
% 14.32/2.83  % (2678818)------------------------------
% 14.32/2.83  % (2678818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.32/2.83  % (2678818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.32/2.83  % (2678818)CaDiCaL version: 2.1.3
% 14.32/2.83  % (2678818)Termination reason: Instruction limit
% 14.32/2.83  % (2678818)Termination phase: Saturation
% 14.32/2.83  % (2678818)Time elapsed: 0.167 s
% 14.32/2.83  % (2678818)Peak memory usage: 95 MB
% 14.32/2.83  % (2678818)Instructions burned: 318 (million)
% 14.32/2.83  % (2678826)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=3268803823:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/12125Mi)
% 14.32/2.83  % (2678829)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=716383668:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2988 on theBenchmark for (2988ds/2836Mi)
% 14.32/2.83  % (2678829)First to succeed.
% 14.32/2.83  % (2678829)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2678729"
% 14.32/2.83  % SZS status Satisfiable for theBenchmark
% 14.32/2.83  % SZS output start Saturation.
% See solution above
% 14.60/2.93  % SZS output start Definitions and Model Updates.
% 14.60/2.93  % SZS output end Definitions and Model Updates.
% 14.60/2.93  % (2678829)------------------------------
% 14.60/2.93  % (2678829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.60/2.93  % (2678829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.60/2.93  % (2678829)CaDiCaL version: 2.1.3
% 14.60/2.93  % (2678829)Termination reason: Satisfiable
% 14.60/2.93  % (2678829)Time elapsed: 0.464 s
% 14.60/2.93  % (2678829)Peak memory usage: 100 MB
% 14.60/2.93  % (2678829)Instructions burned: 851 (million)
% 14.60/2.93  % (2678829)------------------------------
% 14.60/2.93  % (2678829)------------------------------
% 14.60/2.93  % (2678729)Success in time 2.008 s
% 14.60/2.93  % Vampire exiting
%------------------------------------------------------------------------------