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

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

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

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

% Comments : 
%------------------------------------------------------------------------------
cnf(u3183,negated_conjecture,
    true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u2291,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,living(X0,skc17),true) ).

cnf(u1415,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc15),true) ).

cnf(u2434,negated_conjecture,
    true = ifeq2(animate(skc9,X0),true,animate(skc14,X0),true) ).

cnf(u3356,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,of(X0,skc12,skc13),true) ).

cnf(u2075,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,entity(X0,skc17),true) ).

cnf(u2289,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,living(X0,skc17),true) ).

cnf(u3885,negated_conjecture,
    ifeq3(of(skc9,skc12,skc17),true,ifeq3(of(skc9,X0,skc17),true,ifeq3(forename(skc9,X0),true,skc12,X0),X0),X0) = X0 ).

cnf(u4486,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(agent(skc14,X0,skc17),true,ifeq3(think_believe_consider(skc14,X0),true,skc14,skc14),skc14),skc14) ).

cnf(u1677,negated_conjecture,
    true = impartial(skc14,skc13) ).

cnf(u1567,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,event(X0,skc15),true) ).

cnf(u1938,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,human_person(X0,skc13),true) ).

cnf(u289,negated_conjecture,
    true = thing(skc9,skc17) ).

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

cnf(u276,negated_conjecture,
    true = entity(skc9,skc13) ).

cnf(u1566,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,event(X0,skc10),true) ).

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

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

cnf(u232,negated_conjecture,
    true = specific(skc9,skc15) ).

cnf(u462,negated_conjecture,
    true = general(skc9,skc12) ).

cnf(u3353,negated_conjecture,
    true = ifeq2(of(X0,skc16,skc17),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

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

cnf(u2862,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,abstraction(X0,skc12),true) ).

cnf(u1422,negated_conjecture,
    true = ifeq2(unisex(skc9,X0),true,unisex(skc14,X0),true) ).

cnf(u1821,negated_conjecture,
    true = existent(skc14,skc17) ).

cnf(u295,negated_conjecture,
    true = singleton(skc9,skc17) ).

cnf(u277,negated_conjecture,
    true = entity(skc9,skc17) ).

cnf(u404,negated_conjecture,
    true = relname(skc9,skc12) ).

cnf(u933,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(singleton(X0,skc12),true,true,true),true) ).

cnf(u160,negated_conjecture,
    true = accessible_world(skc9,skc14) ).

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

cnf(u931,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

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

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

cnf(u4655,negated_conjecture,
    ifeq3(theme(skc9,skc15,X0),true,ifeq3(theme(skc9,skc15,X1),true,ifeq3(proposition(skc9,X0),true,ifeq3(proposition(skc9,X1),true,X1,X0),X0),X0),X0) = X0 ).

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

cnf(u5107,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(theme(skc14,X1,skc14),true,ifeq3(agent(skc14,X0,X2),true,ifeq3(agent(skc14,X1,X2),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(think_believe_consider(skc14,X1),true,skc14,skc14),skc14),skc14),skc14),skc14),skc14) ).

cnf(u166,negated_conjecture,
    true = agent(skc9,skc15,skc17) ).

cnf(u3501,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,theme(X0,skc15,skc14),true) ).

cnf(u1704,negated_conjecture,
    true = ifeq2(event(skc9,skf1(X0)),true,true,true) ).

cnf(u946,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc10),true) ).

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

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

cnf(u952,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,singleton(X0,skc14),true) ).

cnf(u421,negated_conjecture,
    true = abstraction(skc9,skc16) ).

cnf(u689,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc15)),tuple(true,true),a,b) ).

cnf(u444,negated_conjecture,
    true = ifeq2(eventuality(skc9,skc12),true,true,true) ).

cnf(u164,negated_conjecture,
    true = of(skc9,skc16,skc17) ).

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

cnf(u3987,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc16,skc13),true,ifeq3(of(skc14,skc16,skc13),true,skc16,skc16),skc16) ).

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

cnf(u1940,negated_conjecture,
    true = ifeq2(human_person(skc9,X0),true,human_person(skc14,X0),true) ).

cnf(u2750,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,relation(X0,skc14),true) ).

cnf(u335,negated_conjecture,
    true = existent(skc9,skc11) ).

cnf(u434,negated_conjecture,
    true = thing(skc9,skc12) ).

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

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

cnf(u578,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,state(X0,skc10),true) ).

cnf(u956,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,singleton(X0,skc13),true) ).

cnf(u333,negated_conjecture,
    true = existent(skc9,skc17) ).

cnf(u584,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(state(X0,skc10),true,true,true),true) ).

cnf(u432,negated_conjecture,
    true = ifeq2(abstraction(skc9,skc10),true,true,true) ).

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

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

cnf(u948,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc13),true) ).

cnf(u1349,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,nonexistent(X0,skc15),true) ).

cnf(u1766,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skf1(X1)),true) ).

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

cnf(u2502,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,male(X0,skc13),true) ).

cnf(u461,negated_conjecture,
    true = general(skc9,skc16) ).

cnf(u346,negated_conjecture,
    true = impartial(skc9,skc13) ).

cnf(u3674,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc12,skc17),true,skc12,skc16) ).

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

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

cnf(u3364,negated_conjecture,
    true = ifeq2(of(X0,skc12,skc13),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u1226,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,specific(X0,skc17),true) ).

cnf(u1220,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc15),true) ).

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

cnf(u3699,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc12,skc17),true,skc12,skc16) ).

cnf(u603,negated_conjecture,
    true = ifeq2(smoke(skc14,skc10),true,true,true) ).

cnf(u3045,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(general(X0,skc12),true,true,true),true) ).

cnf(u1224,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,specific(X0,skc13),true) ).

cnf(u3043,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(general(X0,skc12),true,true,true),true) ).

cnf(u2216,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(impartial(X0,skc13),true,true,true),true) ).

cnf(u2006,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,organism(X0,skc13),true) ).

cnf(u733,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(thing(X0,skc14),true,true,true),true) ).

cnf(u472,negated_conjecture,
    true = unisex(skc9,skc12) ).

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

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

cnf(u4303,negated_conjecture,
    ifeq3(theme(skc9,skc15,X0),true,ifeq3(agent(skc9,skc15,X1),true,ifeq3(agent(skc9,skc15,X1),true,ifeq3(proposition(skc9,X0),true,skc14,X0),X0),X0),X0) = X0 ).

cnf(u3189,negated_conjecture,
    true = present(skc14,skc15) ).

cnf(u3816,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc16,X0),true,ifeq3(of(skc9,skc16,X0),true,ifeq3(entity(skc9,X0),true,skc16,skc16),skc16),skc16) ).

cnf(u3552,negated_conjecture,
    true = be(skc14,skc10,skc13,skc13) ).

cnf(u2010,negated_conjecture,
    true = ifeq2(organism(skc9,X0),true,organism(skc14,X0),true) ).

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

cnf(u1747,negated_conjecture,
    true = ifeq2(entity(skc14,skf1(X0)),true,true,true) ).

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

cnf(u234,negated_conjecture,
    true = unisex(skc9,skc15) ).

cnf(u3193,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,present(X0,skc15),true) ).

cnf(u1796,negated_conjecture,
    true = human(skc14,skc17) ).

cnf(u658,negated_conjecture,
    true = ifeq2(eventuality(skc9,X0),true,eventuality(skc14,X0),true) ).

cnf(u5145,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(agent(skc14,X0,skc17),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,skc14,skc14),skc14),skc14),skc14),skc14) ).

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

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

cnf(u2562,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,forename(X0,skc12),true) ).

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

cnf(u1642,negated_conjecture,
    true = man(skc14,skc13) ).

cnf(u489,negated_conjecture,
    true = relation(skc9,skc14) ).

cnf(u1659,negated_conjecture,
    true = agent(skc14,skf1(skc13),skc13) ).

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

cnf(u1648,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(man(X0,skc13),true,true,true),true) ).

cnf(u3052,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,general(X0,skc12),true) ).

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

cnf(u3236,negated_conjecture,
    true = ifeq2(think_believe_consider(skc9,X0),true,think_believe_consider(skc14,X0),true) ).

cnf(u789,negated_conjecture,
    true = singleton(skc14,skc12) ).

cnf(u3661,negated_conjecture,
    ifeq3(of(skc9,X0,skc13),true,ifeq3(forename(skc9,X0),true,skc12,X0),X0) = X0 ).

cnf(u3322,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(vincent_forename(X0,skc16),true,true,true),true) ).

cnf(u1665,negated_conjecture,
    true = organism(skc14,skc13) ).

cnf(u1419,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,unisex(X0,skc12),true) ).

cnf(u2284,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(living(X0,skc13),true,true,true),true) ).

cnf(u3659,negated_conjecture,
    ifeq3(of(skc14,X0,skc17),true,ifeq3(forename(skc14,X0),true,skc16,X0),X0) = X0 ).

cnf(u1805,negated_conjecture,
    true = entity(skc14,skc17) ).

cnf(u1679,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc14,skc13)),tuple(true,true),a,b) ).

cnf(u2073,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(entity(X0,skc17),true,true,true),true) ).

cnf(u1571,negated_conjecture,
    true = event(skc14,skc15) ).

cnf(u216,negated_conjecture,
    true = event(skc9,skc10) ).

cnf(u2571,negated_conjecture,
    true = ifeq2(vincent_forename(skc14,skc12),true,true,true) ).

cnf(u1678,negated_conjecture,
    true = living(skc14,skc13) ).

cnf(u3357,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,of(X0,skc16,skc17),true) ).

cnf(u144,negated_conjecture,
    true = event(skc9,skc15) ).

cnf(u4386,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,skc14),true,ifeq3(agent(skc9,skc15,X1),true,ifeq3(agent(skc9,X0,X1),true,ifeq3(think_believe_consider(skc9,X0),true,skc14,skc14),skc14),skc14),skc14) ).

cnf(u2857,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(abstraction(X0,skc12),true,true,true),true) ).

cnf(u522,negated_conjecture,
    true = ifeq2(vincent_forename(skc9,skc12),true,true,true) ).

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

cnf(u808,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc16),true,true,true) ).

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

cnf(u528,negated_conjecture,
    true = be(skc9,skc10,skc13,skc13) ).

cnf(u2574,negated_conjecture,
    true = relname(skc14,skc12) ).

cnf(u545,negated_conjecture,
    b = ifeq(tuple(true,male(skc9,skc15)),tuple(true,true),a,b) ).

cnf(u300,negated_conjecture,
    true = singleton(skc9,skc13) ).

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

cnf(u1931,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(human_person(X0,skc17),true,true,true),true) ).

cnf(u150,negated_conjecture,
    true = man(skc9,skc13) ).

cnf(u4389,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,X1),true,ifeq3(agent(skc9,X0,skc17),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,X1,skc14),skc14),skc14),skc14) ).

cnf(u3239,negated_conjecture,
    true = think_believe_consider(skc14,skc15) ).

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

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

cnf(u1937,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,human_person(X0,skc17),true) ).

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

cnf(u2356,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human(X0,skc13),true,true,true),true) ).

cnf(u319,negated_conjecture,
    true = specific(skc9,skc13) ).

cnf(u405,negated_conjecture,
    true = relname(skc9,skc16) ).

cnf(u656,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,eventuality(X0,skc15),true) ).

cnf(u290,negated_conjecture,
    true = thing(skc9,skc13) ).

cnf(u673,negated_conjecture,
    true = ifeq2(event(skc14,skc15),true,true,true) ).

cnf(u428,negated_conjecture,
    true = ifeq2(abstraction(skc9,skc17),true,true,true) ).

cnf(u3243,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,think_believe_consider(X0,skc15),true) ).

cnf(u148,negated_conjecture,
    true = think_believe_consider(skc9,skc15) ).

cnf(u806,negated_conjecture,
    true = ifeq2(entity(skc14,skc16),true,true,true) ).

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

cnf(u562,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc9,skc17)),tuple(true,true),a,b) ).

cnf(u3610,negated_conjecture,
    ifeq3(of(skc14,X0,skc13),true,ifeq3(of(skc14,X1,skc13),true,ifeq3(forename(skc14,X0),true,ifeq3(forename(skc14,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u3506,negated_conjecture,
    true = theme(skc14,skc15,skc14) ).

cnf(u3616,negated_conjecture,
    skc12 = ifeq3(of(skc9,X0,X1),true,ifeq3(of(skc9,skc12,X1),true,ifeq3(forename(skc9,X0),true,ifeq3(entity(skc9,X1),true,X0,skc12),skc12),skc12),skc12) ).

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

cnf(u4387,negated_conjecture,
    skc14 = ifeq3(theme(skc9,skc15,X0),true,ifeq3(agent(skc9,skc15,X1),true,ifeq3(agent(skc9,skc15,X1),true,ifeq3(proposition(skc9,X0),true,X0,skc14),skc14),skc14),skc14) ).

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

cnf(u690,negated_conjecture,
    true = ifeq2(entity(skc14,skc15),true,true,true) ).

cnf(u3738,negated_conjecture,
    skc12 = ifeq3(of(skc9,skc12,X0),true,ifeq3(of(skc9,skc12,X0),true,ifeq3(entity(skc9,X0),true,skc12,skc12),skc12),skc12) ).

cnf(u940,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc13),true,true,true),true) ).

cnf(u4470,negated_conjecture,
    skc14 = ifeq3(agent(skc14,skc15,X0),true,ifeq3(agent(skc14,skc15,X0),true,skc14,skc14),skc14) ).

cnf(u445,negated_conjecture,
    true = singleton(skc9,skc12) ).

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

cnf(u548,negated_conjecture,
    b = ifeq(tuple(true,male(skc9,skc14)),tuple(true,true),a,b) ).

cnf(u2617,negated_conjecture,
    true = ifeq2(proposition(skc14,skc16),true,true,true) ).

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

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

cnf(u2630,negated_conjecture,
    true = nonhuman(skc14,skc16) ).

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

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

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

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

cnf(u4468,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0) = X0 ).

cnf(u178,negated_conjecture,
    true = ifeq2(man(skc14,X0),true,event(skc14,skf1(X1)),true) ).

cnf(u2745,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(relation(X0,skc14),true,true,true),true) ).

cnf(u3662,negated_conjecture,
    ifeq3(of(skc9,X0,skc17),true,ifeq3(forename(skc9,X0),true,skc16,X0),X0) = X0 ).

cnf(u2901,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(nonhuman(X0,skc12),true,true,true),true) ).

cnf(u4029,negated_conjecture,
    skc12 = ifeq3(of(skc14,skc12,X0),true,ifeq3(of(skc14,skc12,X0),true,ifeq3(entity(skc14,X0),true,skc12,skc12),skc12),skc12) ).

cnf(u2631,negated_conjecture,
    true = general(skc14,skc16) ).

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

cnf(u4904,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,skc14),true,ifeq3(theme(skc9,X1,skc14),true,ifeq3(agent(skc9,X0,X2),true,ifeq3(agent(skc9,X1,X2),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(think_believe_consider(skc9,X1),true,skc14,skc14),skc14),skc14),skc14),skc14),skc14) ).

cnf(u589,negated_conjecture,
    true = event(skc14,skc10) ).

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

cnf(u2746,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relation(X0,skc12),true,true,true),true) ).

cnf(u2500,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,male(X0,skc13),true) ).

cnf(u3658,negated_conjecture,
    skc16 = ifeq3(of(skc9,X0,skc17),true,ifeq3(forename(skc9,X0),true,X0,skc16),skc16) ).

cnf(u2772,negated_conjecture,
    true = abstraction(skc14,skc14) ).

cnf(u347,negated_conjecture,
    true = impartial(skc9,skc17) ).

cnf(u3813,negated_conjecture,
    skc16 = ifeq3(of(skc9,X0,skc13),true,ifeq3(of(skc9,skc16,skc13),true,ifeq3(forename(skc9,X0),true,X0,skc16),skc16),skc16) ).

cnf(u4466,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc17),X0),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0) = X0 ).

cnf(u334,negated_conjecture,
    true = existent(skc9,skc13) ).

cnf(u4864,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0) = X0 ).

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

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

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

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

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

cnf(u207,negated_conjecture,
    true = nonexistent(skc9,skc10) ).

cnf(u345,negated_conjecture,
    true = impartial(skc9,skc11) ).

cnf(u1244,negated_conjecture,
    true = specific(skc14,skc17) ).

cnf(u2147,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(existent(X0,skc17),true,true,true),true) ).

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

cnf(u1731,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skf1(X0))),tuple(true,true),a,b) ).

cnf(u2902,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(nonhuman(X0,skc14),true,true,true),true) ).

cnf(u2000,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(organism(X0,skc13),true,true,true),true) ).

cnf(u2783,negated_conjecture,
    true = nonhuman(skc14,skc14) ).

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

cnf(u1737,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonexistent(X0,skf1(X1)),true,true,true),true) ).

cnf(u2908,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonhuman(X0,skc12),true) ).

cnf(u734,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc10),true,true,true),true) ).

cnf(u4296,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,X1),true,ifeq3(agent(skc9,skc15,X2),true,ifeq3(agent(skc9,X0,X2),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,X1,skc14),skc14),skc14),skc14),skc14) ).

cnf(u1751,negated_conjecture,
    true = ifeq2(thing(skc9,skf1(X0)),true,true,true) ).

cnf(u740,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,thing(X0,skc10),true) ).

cnf(u1576,negated_conjecture,
    true = ifeq2(smoke(skc14,skc15),true,true,true) ).

cnf(u2680,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(relname(X0,skc12),true,true,true),true) ).

cnf(u1632,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(man(X0,skc13),true,true,true),true) ).

cnf(u3445,negated_conjecture,
    true = agent(skc14,skc15,skc17) ).

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

cnf(u2426,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(animate(X0,skc13),true,true,true),true) ).

cnf(u4089,negated_conjecture,
    ifeq3(of(skc14,skc16,skc13),true,ifeq3(of(skc14,X0,skc13),true,ifeq3(forename(skc14,X0),true,skc16,X0),X0),X0) = X0 ).

cnf(u1772,negated_conjecture,
    true = man(skc14,skc17) ).

cnf(u3188,negated_conjecture,
    true = ifeq2(present(skc9,skf1(X0)),true,true,true) ).

cnf(u502,negated_conjecture,
    true = nonhuman(skc9,skc14) ).

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

cnf(u4798,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(theme(skc14,skc15,X0),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14) ).

cnf(u1760,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skf1(X1)),true) ).

cnf(u4311,negated_conjecture,
    ifeq3(theme(skc9,skc15,X0),true,ifeq3(proposition(skc9,X0),true,skc14,X0),X0) = X0 ).

cnf(u3449,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,agent(X0,skc15,skc17),true) ).

cnf(u2685,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relname(X0,skc12),true) ).

cnf(u263,negated_conjecture,
    true = organism(skc9,skc17) ).

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

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

cnf(u3316,negated_conjecture,
    true = ifeq2(vincent_forename(skc9,X0),true,vincent_forename(skc14,X0),true) ).

cnf(u2683,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relname(X0,skc16),true,true,true),true) ).

cnf(u1790,negated_conjecture,
    true = agent(skc14,skf1(skc17),skc17) ).

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

cnf(u786,negated_conjecture,
    true = ifeq2(entity(skc14,skc12),true,true,true) ).

cnf(u2290,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,living(X0,skc13),true) ).

cnf(u1668,negated_conjecture,
    b = ifeq(tuple(unisex(skc14,skc13),true),tuple(true,true),a,b) ).

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

cnf(u4124,negated_conjecture,
    ifeq3(of(skc14,skc12,skc17),true,ifeq3(of(skc14,X0,skc17),true,ifeq3(forename(skc14,X0),true,skc12,X0),X0),X0) = X0 ).

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

cnf(u1807,negated_conjecture,
    true = living(skc14,skc17) ).

cnf(u1666,negated_conjecture,
    true = human(skc14,skc13) ).

cnf(u1574,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skc15),true,true,true),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(u1580,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skc15),true) ).

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

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

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

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

cnf(u657,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,eventuality(X0,skc10),true) ).

cnf(u412,negated_conjecture,
    true = relation(skc9,skc16) ).

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(u3715,negated_conjecture,
    skc12 = ifeq3(of(skc14,skc12,skc17),true,skc16,skc12) ).

cnf(u790,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc12),true) ).

cnf(u2072,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(entity(X0,skc13),true,true,true),true) ).

cnf(u215,negated_conjecture,
    true = ifeq2(state(skc9,skc15),true,true,true) ).

cnf(u546,negated_conjecture,
    b = ifeq(tuple(true,male(skc9,skc12)),tuple(true,true),a,b) ).

cnf(u4570,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc17),X0),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14) ).

cnf(u2611,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,forename(X0,skc16),true) ).

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

cnf(u796,negated_conjecture,
    true = ifeq2(entity(skc14,skc13),true,true,true) ).

cnf(u3611,negated_conjecture,
    ifeq3(of(skc9,X0,skc17),true,ifeq3(of(skc9,X1,skc17),true,ifeq3(forename(skc9,X0),true,ifeq3(forename(skc9,X1),true,X0,X1),X1),X1),X1) = X1 ).

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

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

cnf(u569,negated_conjecture,
    b = ifeq(tuple(true,existent(skc9,skc10)),tuple(true,true),a,b) ).

cnf(u3735,negated_conjecture,
    skc12 = ifeq3(of(skc9,X0,skc17),true,ifeq3(of(skc9,skc12,skc17),true,ifeq3(forename(skc9,X0),true,X0,skc12),skc12),skc12) ).

cnf(u3617,negated_conjecture,
    skc16 = ifeq3(of(skc9,X0,X1),true,ifeq3(of(skc9,skc16,X1),true,ifeq3(forename(skc9,X0),true,ifeq3(entity(skc9,X1),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u174,negated_conjecture,
    true = ifeq2(man(skc14,X0),true,smoke(skc14,skf1(X1)),true) ).

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

cnf(u2353,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(human(X0,skc17),true,true,true),true) ).

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

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

cnf(u3374,negated_conjecture,
    true = ifeq2(of(X0,skc16,skc17),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u429,negated_conjecture,
    true = ifeq2(abstraction(skc9,skc15),true,true,true) ).

cnf(u680,negated_conjecture,
    true = thing(skc14,skc15) ).

cnf(u788,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc12),true,true,true) ).

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

cnf(u172,negated_conjecture,
    true = be(skc9,skc10,skc13,skc11) ).

cnf(u3499,negated_conjecture,
    true = ifeq2(theme(X0,skc15,skc14),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

cnf(u1213,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(specific(X0,skc15),true,true,true),true) ).

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

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

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

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

cnf(u2224,negated_conjecture,
    true = ifeq2(impartial(skc9,X0),true,impartial(skc14,X0),true) ).

cnf(u442,negated_conjecture,
    true = ifeq2(entity(skc9,skc12),true,true,true) ).

cnf(u162,negated_conjecture,
    true = proposition(skc9,skc14) ).

cnf(u571,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc9,skc17),true),tuple(true,true),a,b) ).

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

cnf(u1344,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(nonexistent(X0,skc15),true,true,true),true) ).

cnf(u4756,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc17),X0),true,ifeq3(theme(skc14,skc15,X1),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u2608,negated_conjecture,
    true = ifeq2(jules_forename(skc14,skc16),true,true,true) ).

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

cnf(u2504,negated_conjecture,
    true = ifeq2(male(skc9,X0),true,male(skc14,X0),true) ).

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

cnf(u559,negated_conjecture,
    b = ifeq(tuple(specific(skc9,skc12),true),tuple(true,true),a,b) ).

cnf(u318,negated_conjecture,
    true = specific(skc9,skc17) ).

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

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

cnf(u3667,negated_conjecture,
    skc12 = ifeq3(of(skc9,skc16,skc13),true,skc16,skc12) ).

cnf(u3656,negated_conjecture,
    skc12 = ifeq3(of(skc14,X0,skc13),true,ifeq3(forename(skc14,X0),true,X0,skc12),skc12) ).

cnf(u191,negated_conjecture,
    true = eventuality(skc9,skc10) ).

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

cnf(u1721,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(eventuality(X0,skf1(X1)),true,true,true),true) ).

cnf(u1347,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonexistent(X0,skc15),true) ).

cnf(u590,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,state(X0,skc10),true) ).

cnf(u2753,negated_conjecture,
    true = ifeq2(relation(skc9,X0),true,relation(skc14,X0),true) ).

cnf(u613,negated_conjecture,
    true = singleton(skc14,skc10) ).

cnf(u3434,negated_conjecture,
    true = ifeq2(agent(X0,skc15,skc17),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

cnf(u2501,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,male(X0,skc17),true) ).

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

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

cnf(u3314,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(vincent_forename(X0,skc16),true,true,true),true) ).

cnf(u1735,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skf1(X1)),true) ).

cnf(u358,negated_conjecture,
    true = living(skc9,skc13) ).

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

cnf(u3436,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc17),skc17),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u739,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,thing(X0,skc14),true) ).

cnf(u2286,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(living(X0,skc13),true,true,true),true) ).

cnf(u3544,negated_conjecture,
    true = ifeq2(be(skc9,X0,X1,X2),true,be(skc14,X0,X1,X2),true) ).

cnf(u231,negated_conjecture,
    true = thing(skc9,skc15) ).

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

cnf(u369,negated_conjecture,
    true = human(skc9,skc17) ).

cnf(u601,negated_conjecture,
    true = nonexistent(skc14,skc10) ).

cnf(u4838,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(theme(skc14,skf1(skc17),X1),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u1744,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skf1(X1)),true,true,true),true) ).

cnf(u2146,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(existent(X0,skc13),true,true,true),true) ).

cnf(u1761,negated_conjecture,
    true = ifeq2(singleton(skc9,skf1(X0)),true,true,true) ).

cnf(u1652,negated_conjecture,
    true = human_person(skc14,skc13) ).

cnf(u3609,negated_conjecture,
    ifeq3(of(skc14,X0,skc17),true,ifeq3(of(skc14,X1,skc17),true,ifeq3(forename(skc14,X0),true,ifeq3(forename(skc14,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u2771,negated_conjecture,
    true = ifeq2(relname(skc14,skc14),true,true,true) ).

cnf(u3557,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,be(X0,skc10,skc13,skc13),true) ).

cnf(u729,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(thing(X0,skc13),true,true,true),true) ).

cnf(u484,negated_conjecture,
    true = ifeq2(smoke(skc9,skc15),true,true,true) ).

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

cnf(u2424,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(animate(X0,skc13),true,true,true),true) ).

cnf(u770,negated_conjecture,
    true = thing(skc14,skc17) ).

cnf(u743,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,thing(X0,skc13),true) ).

cnf(u618,negated_conjecture,
    b = ifeq(tuple(true,existent(skc14,skc10)),tuple(true,true),a,b) ).

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

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

cnf(u776,negated_conjecture,
    true = ifeq2(entity(skc14,skc14),true,true,true) ).

cnf(u4326,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,skc14),true,ifeq3(agent(skc9,X0,skc17),true,ifeq3(think_believe_consider(skc9,X0),true,skc14,skc14),skc14),skc14) ).

cnf(u503,negated_conjecture,
    true = general(skc9,skc14) ).

cnf(u2688,negated_conjecture,
    true = ifeq2(relname(skc9,X0),true,relname(skc14,X0),true) ).

cnf(u1667,negated_conjecture,
    true = animate(skc14,skc13) ).

cnf(u1249,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc13)),tuple(true,true),a,b) ).

cnf(u2430,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,animate(X0,skc13),true) ).

cnf(u1784,negated_conjecture,
    true = male(skc14,skc17) ).

cnf(u2287,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(living(X0,skc17),true,true,true),true) ).

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

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

cnf(u1414,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u287,negated_conjecture,
    true = ifeq2(entity(skc9,skc10),true,true,true) ).

cnf(u501,negated_conjecture,
    true = thing(skc9,skc14) ).

cnf(u3457,negated_conjecture,
    true = ifeq2(agent(skc9,skf1(skc17),skc17),true,true,true) ).

cnf(u2580,negated_conjecture,
    true = relation(skc14,skc12) ).

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

cnf(u2597,negated_conjecture,
    b = ifeq(tuple(human(skc14,skc12),true),tuple(true,true),a,b) ).

cnf(u2563,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,forename(X0,skc16),true) ).

cnf(u655,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,eventuality(X0,skc10),true) ).

cnf(u1418,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,unisex(X0,skc10),true) ).

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

cnf(u2595,negated_conjecture,
    true = general(skc14,skc12) ).

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

cnf(u1412,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(unisex(X0,skc14),true,true,true),true) ).

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

cnf(u553,negated_conjecture,
    b = ifeq(tuple(true,general(skc9,skc17)),tuple(true,true),a,b) ).

cnf(u785,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc12),true,true,true) ).

cnf(u3355,negated_conjecture,
    true = ifeq2(of(skc9,X0,X1),true,of(skc14,X0,X1),true) ).

cnf(u158,negated_conjecture,
    true = state(skc9,skc10) ).

cnf(u1416,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc10),true) ).

cnf(u799,negated_conjecture,
    true = singleton(skc14,skc13) ).

cnf(u3235,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc15),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

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

cnf(u275,negated_conjecture,
    true = entity(skc9,skc11) ).

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

cnf(u413,negated_conjecture,
    true = relation(skc9,skc12) ).

cnf(u2080,negated_conjecture,
    true = ifeq2(entity(skc9,X0),true,entity(skc14,X0),true) ).

cnf(u2215,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(impartial(X0,skc17),true,true,true),true) ).

cnf(u2585,negated_conjecture,
    true = abstraction(skc14,skc12) ).

cnf(u156,negated_conjecture,
    true = man(skc9,skc11) ).

cnf(u2599,negated_conjecture,
    b = ifeq(tuple(specific(skc14,skc12),true),tuple(true,true),a,b) ).

cnf(u3362,negated_conjecture,
    true = of(skc14,skc12,skc13) ).

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

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

cnf(u557,negated_conjecture,
    b = ifeq(tuple(true,general(skc9,skc10)),tuple(true,true),a,b) ).

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

cnf(u146,negated_conjecture,
    true = present(skc9,skc15) ).

cnf(u1410,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(unisex(X0,skc12),true,true,true),true) ).

cnf(u555,negated_conjecture,
    b = ifeq(tuple(true,general(skc9,skc13)),tuple(true,true),a,b) ).

cnf(u942,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).

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

cnf(u550,negated_conjecture,
    b = ifeq(tuple(unisex(skc9,skc13),true),tuple(true,true),a,b) ).

cnf(u1450,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc12)),tuple(true,true),a,b) ).

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

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

cnf(u2364,negated_conjecture,
    true = ifeq2(human(skc9,X0),true,human(skc14,X0),true) ).

cnf(u1214,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(specific(X0,skc13),true,true,true),true) ).

cnf(u668,negated_conjecture,
    true = ifeq2(state(skc14,skc15),true,true,true) ).

cnf(u2214,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(impartial(X0,skc13),true,true,true),true) ).

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

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

cnf(u3762,negated_conjecture,
    skc12 = ifeq3(of(skc9,skc12,skc17),true,ifeq3(of(skc9,skc12,skc17),true,skc12,skc12),skc12) ).

cnf(u953,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,singleton(X0,skc10),true) ).

cnf(u683,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc15),true,true,true) ).

cnf(u3510,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,theme(X0,skc15,skc14),true) ).

cnf(u1448,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc12),true,true,true),true) ).

cnf(u1222,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,specific(X0,skc10),true) ).

cnf(u1212,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(specific(X0,skc17),true,true,true),true) ).

cnf(u430,negated_conjecture,
    true = ifeq2(abstraction(skc9,skc13),true,true,true) ).

cnf(u1411,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(unisex(X0,skc10),true,true,true),true) ).

cnf(u2751,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,relation(X0,skc12),true) ).

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

cnf(u1345,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonexistent(X0,skc10),true,true,true),true) ).

cnf(u3660,negated_conjecture,
    ifeq3(of(skc14,X0,skc13),true,ifeq3(forename(skc14,X0),true,skc12,X0),X0) = X0 ).

cnf(u1705,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skf1(X1)),true,true,true),true) ).

cnf(u819,negated_conjecture,
    true = singleton(skc14,skc17) ).

cnf(u936,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(singleton(X0,skc14),true,true,true),true) ).

cnf(u3722,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc16,skc13),true,skc12,skc16) ).

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

cnf(u957,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,singleton(X0,skc15),true) ).

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

cnf(u1351,negated_conjecture,
    true = ifeq2(nonexistent(skc9,X0),true,nonexistent(skc14,X0),true) ).

cnf(u1724,negated_conjecture,
    true = unisex(skc14,skf1(X0)) ).

cnf(u955,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,singleton(X0,skc12),true) ).

cnf(u1216,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(specific(X0,skc10),true,true,true),true) ).

cnf(u1722,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,eventuality(X0,skf1(X1)),true) ).

cnf(u4753,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(theme(skc14,skc15,X1),true,ifeq3(agent(skc14,X0,skc17),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,skc14),skc14),skc14),skc14),skc14) ).

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

cnf(u614,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc10)),tuple(true,true),a,b) ).

cnf(u1631,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(man(X0,skc17),true,true,true),true) ).

cnf(u2002,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(organism(X0,skc13),true,true,true),true) ).

cnf(u2433,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,animate(X0,skc17),true) ).

cnf(u1739,negated_conjecture,
    b = ifeq(tuple(true,existent(skc14,skf1(X0))),tuple(true,true),a,b) ).

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

cnf(u1728,negated_conjecture,
    true = ifeq2(unisex(skc9,skf1(X0)),true,true,true) ).

cnf(u599,negated_conjecture,
    true = thing(skc14,skc10) ).

cnf(u1636,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,man(X0,skc13),true) ).

cnf(u2769,negated_conjecture,
    true = ifeq2(proposition(skc14,skc14),true,true,true) ).

cnf(u742,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,thing(X0,skc12),true) ).

cnf(u1653,negated_conjecture,
    true = male(skc14,skc13) ).

cnf(u359,negated_conjecture,
    true = living(skc9,skc17) ).

cnf(u2153,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,existent(X0,skc17),true) ).

cnf(u170,negated_conjecture,
    true = of(skc9,skc12,skc13) ).

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

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

cnf(u3437,negated_conjecture,
    true = ifeq2(agent(skc9,X0,X1),true,agent(skc14,X0,X1),true) ).

cnf(u224,negated_conjecture,
    true = eventuality(skc9,skc15) ).

cnf(u3191,negated_conjecture,
    true = ifeq2(present(X0,skc15),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u2143,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(existent(X0,skc17),true,true,true),true) ).

cnf(u602,negated_conjecture,
    true = unisex(skc14,skc10) ).

cnf(u5277,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc17),X0),true,ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0),X0) = X0 ).

cnf(u3054,negated_conjecture,
    true = ifeq2(general(skc9,X0),true,general(skc14,X0),true) ).

cnf(u203,negated_conjecture,
    true = specific(skc9,skc10) ).

cnf(u357,negated_conjecture,
    true = living(skc9,skc11) ).

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

cnf(u487,negated_conjecture,
    true = ifeq2(proposition(skc9,skc16),true,true,true) ).

cnf(u2154,negated_conjecture,
    true = ifeq2(existent(skc9,X0),true,existent(skc14,X0),true) ).

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

cnf(u3326,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,vincent_forename(X0,skc16),true) ).

cnf(u3184,negated_conjecture,
    true = ifeq2(present(skc9,X0),true,present(skc14,X0),true) ).

cnf(u3319,negated_conjecture,
    true = vincent_forename(skc14,skc16) ).

cnf(u730,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(thing(X0,skc12),true,true,true),true) ).

cnf(u2686,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,relname(X0,skc16),true) ).

cnf(u1797,negated_conjecture,
    true = animate(skc14,skc17) ).

cnf(u485,negated_conjecture,
    true = ifeq2(smoke(skc9,skc10),true,true,true) ).

cnf(u4064,negated_conjecture,
    skc12 = ifeq3(of(skc14,skc12,skc17),true,ifeq3(of(skc14,skc12,skc17),true,skc12,skc12),skc12) ).

cnf(u370,negated_conjecture,
    true = human(skc9,skc13) ).

cnf(u2564,negated_conjecture,
    true = ifeq2(forename(skc9,X0),true,forename(skc14,X0),true) ).

cnf(u1795,negated_conjecture,
    true = organism(skc14,skc17) ).

cnf(u2581,negated_conjecture,
    true = ifeq2(proposition(skc14,skc12),true,true,true) ).

cnf(u767,negated_conjecture,
    true = thing(skc14,skc13) ).

cnf(u4294,negated_conjecture,
    ifeq3(theme(skc9,X0,X1),true,ifeq3(agent(skc9,X0,X2),true,ifeq3(agent(skc9,skc15,X2),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,skc14,X1),X1),X1),X1),X1) = X1 ).

cnf(u3690,negated_conjecture,
    skc12 = ifeq3(of(skc9,skc12,skc17),true,skc16,skc12) ).

cnf(u2071,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(entity(X0,skc17),true,true,true),true) ).

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

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

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

cnf(u142,negated_conjecture,
    true = vincent_forename(skc9,skc16) ).

cnf(u3051,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,general(X0,skc14),true) ).

cnf(u4304,negated_conjecture,
    ifeq3(theme(skc9,X0,X1),true,ifeq3(agent(skc9,X0,skc17),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,skc14,X1),X1),X1),X1) = X1 ).

cnf(u783,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc12),true,true,true),true) ).

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

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

cnf(u5146,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(agent(skc14,X0,skc13),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,skc14,skc14),skc14),skc14),skc14),skc14) ).

cnf(u5420,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(theme(skc14,skf1(skc17),X0),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14),skc14) ).

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

cnf(u2569,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(forename(X0,skc12),true,true,true),true) ).

cnf(u140,negated_conjecture,
    true = forename(skc9,skc16) ).

cnf(u798,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc13),true,true,true) ).

cnf(u1413,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skc10),true,true,true),true) ).

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

cnf(u1436,negated_conjecture,
    true = unisex(skc14,skc12) ).

cnf(u3456,negated_conjecture,
    true = ifeq2(agent(skc9,skf1(skc13),skc13),true,true,true) ).

cnf(u2070,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(entity(X0,skc13),true,true,true),true) ).

cnf(u3618,negated_conjecture,
    ifeq3(of(skc14,skc16,X0),true,ifeq3(of(skc14,X1,X0),true,ifeq3(forename(skc14,X1),true,ifeq3(entity(skc14,X0),true,skc16,X1),X1),X1),X1) = X1 ).

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

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

cnf(u1417,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,unisex(X0,skc14),true) ).

cnf(u5148,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(theme(skc14,X0,skc14),true,ifeq3(agent(skc14,X0,skc17),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(think_believe_consider(skc14,X0),true,skc14,skc14),skc14),skc14),skc14),skc14) ).

cnf(u3366,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,of(X0,skc12,skc13),true) ).

cnf(u3167,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,smoke(X0,skf1(X1)),true) ).

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

cnf(u2866,negated_conjecture,
    true = ifeq2(abstraction(skc9,X0),true,abstraction(skc14,X0),true) ).

cnf(u1656,negated_conjecture,
    true = smoke(skc14,skf1(X0)) ).

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

cnf(u932,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(singleton(X0,skc13),true,true,true),true) ).

cnf(u299,negated_conjecture,
    true = ifeq2(eventuality(skc9,skc13),true,true,true) ).

cnf(u652,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(eventuality(X0,skc10),true,true,true),true) ).

cnf(u2594,negated_conjecture,
    true = nonhuman(skc14,skc12) ).

cnf(u2607,negated_conjecture,
    true = ifeq2(vincent_forename(skc14,skc16),true,true,true) ).

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

cnf(u1434,negated_conjecture,
    true = unisex(skc14,skc14) ).

cnf(u566,negated_conjecture,
    b = ifeq(tuple(human(skc9,skc12),true),tuple(true,true),a,b) ).

cnf(u4644,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,skc14),true,ifeq3(theme(skc9,skc15,X1),true,ifeq3(agent(skc9,X0,skc17),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,X1,skc14),skc14),skc14),skc14),skc14) ).

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

cnf(u2221,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,impartial(X0,skc17),true) ).

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

cnf(u3683,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc16,skc13),true,skc12,skc16) ).

cnf(u2854,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(abstraction(X0,skc12),true,true,true),true) ).

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

cnf(u2354,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(human(X0,skc13),true,true,true),true) ).

cnf(u3129,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,jules_forename(X0,skc12),true) ).

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

cnf(u3706,negated_conjecture,
    skc12 = ifeq3(of(skc14,skc16,skc13),true,skc16,skc12) ).

cnf(u686,negated_conjecture,
    b = ifeq(tuple(true,existent(skc14,skc15)),tuple(true,true),a,b) ).

cnf(u2495,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(male(X0,skc17),true,true,true),true) ).

cnf(u4282,negated_conjecture,
    ifeq3(theme(skc9,X0,X1),true,ifeq3(theme(skc9,skc15,X2),true,ifeq3(agent(skc9,X0,skc17),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,ifeq3(proposition(skc9,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u4906,negated_conjecture,
    ifeq3(theme(skc9,skc15,X0),true,ifeq3(theme(skc9,X1,skc14),true,ifeq3(agent(skc9,skc15,X2),true,ifeq3(agent(skc9,X1,X2),true,ifeq3(think_believe_consider(skc9,X1),true,ifeq3(proposition(skc9,X0),true,skc14,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u2865,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,abstraction(X0,skc12),true) ).

cnf(u3508,negated_conjecture,
    true = ifeq2(theme(X0,skc15,skc14),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u4563,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc13),X0),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14) ).

cnf(u581,negated_conjecture,
    true = ifeq2(accessible_world(skc9,skc9),true,true,true) ).

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

cnf(u778,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc14),true,true,true) ).

cnf(u941,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc12),true,true,true),true) ).

cnf(u168,negated_conjecture,
    true = theme(skc9,skc15,skc14) ).

cnf(u3130,negated_conjecture,
    true = ifeq2(jules_forename(skc9,X0),true,jules_forename(skc14,X0),true) ).

cnf(u579,negated_conjecture,
    true = ifeq2(state(skc9,X0),true,state(skc14,X0),true) ).

cnf(u939,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

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

cnf(u3927,negated_conjecture,
    ifeq3(of(skc9,skc16,skc13),true,ifeq3(of(skc9,X0,skc13),true,ifeq3(forename(skc9,X0),true,skc16,X0),X0),X0) = X0 ).

cnf(u3278,negated_conjecture,
    true = ifeq2(proposition(skc9,X0),true,proposition(skc14,X0),true) ).

cnf(u1712,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skf1(X1)),true) ).

cnf(u199,negated_conjecture,
    true = singleton(skc9,skc10) ).

cnf(u5554,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(theme(skc14,skf1(skc13),X1),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u3140,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,jules_forename(X0,skc12),true) ).

cnf(u454,negated_conjecture,
    true = nonhuman(skc9,skc12) ).

cnf(u3277,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,proposition(X0,skc14),true) ).

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

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

cnf(u1346,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonexistent(X0,skc15),true,true,true),true) ).

cnf(u1729,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(unisex(X0,skf1(X1)),true,true,true),true) ).

cnf(u2910,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,nonhuman(X0,skc12),true) ).

cnf(u1637,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,man(X0,skc17),true) ).

cnf(u3739,negated_conjecture,
    skc12 = ifeq3(of(skc9,skc16,X0),true,ifeq3(of(skc9,skc12,X0),true,ifeq3(entity(skc9,X0),true,skc16,skc12),skc12),skc12) ).

cnf(u1564,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skc10),true,true,true),true) ).

cnf(u960,negated_conjecture,
    true = ifeq2(singleton(skc9,X0),true,singleton(skc14,X0),true) ).

cnf(u1743,negated_conjecture,
    true = ifeq2(specific(skc9,skf1(X0)),true,true,true) ).

cnf(u3182,negated_conjecture,
    true = ifeq2(present(X0,skc15),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

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

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

cnf(u4455,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(agent(skc14,X0,X1),true,ifeq3(agent(skc14,skc15,X1),true,ifeq3(think_believe_consider(skc14,X0),true,skc14,skc14),skc14),skc14),skc14) ).

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

cnf(u382,negated_conjecture,
    true = animate(skc9,skc13) ).

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

cnf(u471,negated_conjecture,
    true = unisex(skc9,skc16) ).

cnf(u1746,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skf1(X0))),tuple(true,true),a,b) ).

cnf(u609,negated_conjecture,
    true = ifeq2(entity(skc14,skc10),true,true,true) ).

cnf(u3044,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(general(X0,skc14),true,true,true),true) ).

cnf(u1217,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc10),true,true,true),true) ).

cnf(u2763,negated_conjecture,
    true = relation(skc14,skc14) ).

cnf(u3615,negated_conjecture,
    skc12 = ifeq3(of(skc14,X0,X1),true,ifeq3(of(skc14,skc12,X1),true,ifeq3(forename(skc14,X0),true,ifeq3(entity(skc14,X1),true,X0,skc12),skc12),skc12),skc12) ).

cnf(u3168,negated_conjecture,
    true = ifeq2(smoke(skc9,X0),true,smoke(skc14,X0),true) ).

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

cnf(u4572,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skc15,X0),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14) ).

cnf(u1762,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(singleton(X0,skf1(X1)),true,true,true),true) ).

cnf(u383,negated_conjecture,
    true = animate(skc9,skc11) ).

cnf(u2909,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,nonhuman(X0,skc14),true) ).

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

cnf(u737,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc15),true) ).

cnf(u492,negated_conjecture,
    true = ifeq2(relname(skc9,skc14),true,true,true) ).

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

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

cnf(u2152,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,existent(X0,skc13),true) ).

cnf(u3447,negated_conjecture,
    true = ifeq2(agent(X0,skc15,skc17),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u678,negated_conjecture,
    true = nonexistent(skc14,skc15) ).

cnf(u381,negated_conjecture,
    true = animate(skc9,skc17) ).

cnf(u2432,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,animate(X0,skc13),true) ).

cnf(u1257,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc17)),tuple(true,true),a,b) ).

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

cnf(u2572,negated_conjecture,
    true = ifeq2(jules_forename(skc14,skc12),true,true,true) ).

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

cnf(u5149,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(theme(skc14,X0,skc14),true,ifeq3(agent(skc14,X0,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(think_believe_consider(skc14,X0),true,skc14,skc14),skc14),skc14),skc14),skc14) ).

cnf(u371,negated_conjecture,
    true = human(skc9,skc11) ).

cnf(u509,negated_conjecture,
    true = singleton(skc9,skc14) ).

cnf(u480,negated_conjecture,
    true = ifeq2(jules_forename(skc9,skc16),true,true,true) ).

cnf(u3050,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,general(X0,skc12),true) ).

cnf(u2681,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(relname(X0,skc16),true,true,true),true) ).

cnf(u3440,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,agent(X0,skc15,skc17),true) ).

cnf(u3965,negated_conjecture,
    skc16 = ifeq3(of(skc14,X0,skc13),true,ifeq3(of(skc14,skc16,skc13),true,ifeq3(forename(skc14,X0),true,X0,skc16),skc16),skc16) ).

cnf(u2567,negated_conjecture,
    true = forename(skc14,skc12) ).

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

cnf(u1420,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,unisex(X0,skc15),true) ).

cnf(u3621,negated_conjecture,
    ifeq3(of(skc9,skc16,X0),true,ifeq3(of(skc9,X1,X0),true,ifeq3(forename(skc9,X1),true,ifeq3(entity(skc9,X0),true,skc16,X1),X1),X1),X1) = X1 ).

cnf(u1798,negated_conjecture,
    b = ifeq(tuple(unisex(skc14,skc17),true),tuple(true,true),a,b) ).

cnf(u264,negated_conjecture,
    true = organism(skc9,skc13) ).

cnf(u394,negated_conjecture,
    true = male(skc9,skc13) ).

cnf(u793,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc13),true,true,true),true) ).

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

cnf(u2682,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(relname(X0,skc12),true,true,true),true) ).

cnf(u2496,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(male(X0,skc13),true,true,true),true) ).

cnf(u2077,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,entity(X0,skc17),true) ).

cnf(u2560,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(forename(X0,skc16),true,true,true),true) ).

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

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

cnf(u2856,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(abstraction(X0,skc14),true,true,true),true) ).

cnf(u653,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(eventuality(X0,skc15),true,true,true),true) ).

cnf(u1808,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc14,skc17)),tuple(true,true),a,b) ).

cnf(u249,negated_conjecture,
    true = human_person(skc9,skc11) ).

cnf(u3354,negated_conjecture,
    true = ifeq2(of(X0,skc12,skc13),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

cnf(u4395,negated_conjecture,
    skc14 = ifeq3(theme(skc9,skc15,X0),true,ifeq3(proposition(skc9,X0),true,X0,skc14),skc14) ).

cnf(u1932,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human_person(X0,skc13),true,true,true),true) ).

cnf(u4765,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(theme(skc14,skc15,X1),true,ifeq3(proposition(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,X0),X0),X0),X0) = X0 ).

cnf(u935,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).

cnf(u5297,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc13),X0),true,ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u744,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,thing(X0,skc15),true) ).

cnf(u1930,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(human_person(X0,skc13),true,true,true),true) ).

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

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

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

cnf(u1936,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human_person(X0,skc13),true) ).

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

cnf(u154,negated_conjecture,
    true = jules_forename(skc9,skc12) ).

cnf(u563,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc9,skc13)),tuple(true,true),a,b) ).

cnf(u795,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc13),true,true,true) ).

cnf(u2360,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human(X0,skc13),true) ).

cnf(u3237,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,think_believe_consider(X0,skc15),true) ).

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

cnf(u2610,negated_conjecture,
    true = relname(skc14,skc16) ).

cnf(u2363,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,human(X0,skc17),true) ).

cnf(u1562,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(event(X0,skc15),true,true,true),true) ).

cnf(u676,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,eventuality(X0,skc15),true) ).

cnf(u3133,negated_conjecture,
    true = jules_forename(skc14,skc12) ).

cnf(u2616,negated_conjecture,
    true = relation(skc14,skc16) ).

cnf(u152,negated_conjecture,
    true = forename(skc9,skc12) ).

cnf(u2863,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,abstraction(X0,skc14),true) ).

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

cnf(u3241,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc15),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u1692,negated_conjecture,
    true = existent(skc14,skc13) ).

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

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

cnf(u2362,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,human(X0,skc13),true) ).

cnf(u2220,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,impartial(X0,skc13),true) ).

cnf(u438,negated_conjecture,
    true = ifeq2(eventuality(skc9,skc16),true,true,true) ).

cnf(u2744,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(relation(X0,skc12),true,true,true),true) ).

cnf(u567,negated_conjecture,
    b = ifeq(tuple(human(skc9,skc14),true),tuple(true,true),a,b) ).

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

cnf(u1713,negated_conjecture,
    true = ifeq2(eventuality(skc9,skf1(X0)),true,true,true) ).

cnf(u582,negated_conjecture,
    true = state(skc14,skc10) ).

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

cnf(u2621,negated_conjecture,
    true = abstraction(skc14,skc16) ).

cnf(u3128,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(jules_forename(X0,skc12),true,true,true),true) ).

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

cnf(u588,negated_conjecture,
    true = eventuality(skc14,skc10) ).

cnf(u436,negated_conjecture,
    true = ifeq2(entity(skc9,skc16),true,true,true) ).

cnf(u1726,negated_conjecture,
    true = specific(skc14,skf1(X0)) ).

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

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

cnf(u570,negated_conjecture,
    b = ifeq(tuple(true,existent(skc9,skc15)),tuple(true,true),a,b) ).

cnf(u5174,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,skc14,skc14),skc14),skc14),skc14) ).

cnf(u2749,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relation(X0,skc12),true) ).

cnf(u5442,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(theme(skc14,skf1(skc13),X0),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14),skc14) ).

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

cnf(u3166,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(smoke(X0,skf1(X1)),true,true,true),true) ).

cnf(u4028,negated_conjecture,
    skc12 = ifeq3(of(skc14,skc16,X0),true,ifeq3(of(skc14,skc12,X0),true,ifeq3(entity(skc14,X0),true,skc16,skc12),skc12),skc12) ).

cnf(u3315,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,vincent_forename(X0,skc16),true) ).

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

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

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

cnf(u698,negated_conjecture,
    true = singleton(skc14,skc15) ).

cnf(u1732,negated_conjecture,
    true = ifeq2(abstraction(skc14,skf1(X0)),true,true,true) ).

cnf(u3966,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc16,X0),true,ifeq3(of(skc14,skc16,X0),true,ifeq3(entity(skc14,X0),true,skc16,skc16),skc16),skc16) ).

cnf(u1638,negated_conjecture,
    true = ifeq2(man(skc9,X0),true,man(skc14,X0),true) ).

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

cnf(u1736,negated_conjecture,
    true = ifeq2(nonexistent(skc9,skf1(X0)),true,true,true) ).

cnf(u4705,negated_conjecture,
    ifeq3(theme(skc9,skc15,X0),true,ifeq3(theme(skc9,X1,skc14),true,ifeq3(agent(skc9,X1,skc17),true,ifeq3(think_believe_consider(skc9,X1),true,ifeq3(proposition(skc9,X0),true,skc14,X0),X0),X0),X0),X0) = X0 ).

cnf(u4460,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc13),X0),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0) = X0 ).

cnf(u3657,negated_conjecture,
    skc12 = ifeq3(of(skc9,X0,skc13),true,ifeq3(forename(skc9,X0),true,X0,skc12),skc12) ).

cnf(u3276,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(proposition(X0,skc14),true,true,true),true) ).

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

cnf(u1742,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonexistent(X0,skf1(X1)),true) ).

cnf(u453,negated_conjecture,
    true = nonhuman(skc9,skc16) ).

cnf(u1999,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(organism(X0,skc17),true,true,true),true) ).

cnf(u508,negated_conjecture,
    true = ifeq2(eventuality(skc9,skc14),true,true,true) ).

cnf(u3614,negated_conjecture,
    skc16 = ifeq3(of(skc14,X0,X1),true,ifeq3(of(skc14,skc16,X1),true,ifeq3(forename(skc14,X0),true,ifeq3(entity(skc14,X1),true,X0,skc16),skc16),skc16),skc16) ).

cnf(u110,axiom,
    true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).

cnf(u3620,negated_conjecture,
    ifeq3(of(skc9,skc12,X0),true,ifeq3(of(skc9,X1,X0),true,ifeq3(forename(skc9,X1),true,ifeq3(entity(skc9,X0),true,skc12,X1),X1),X1),X1) = X1 ).

cnf(u735,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u1752,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skf1(X1)),true,true,true),true) ).

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

cnf(u4026,negated_conjecture,
    skc12 = ifeq3(of(skc14,X0,skc17),true,ifeq3(of(skc14,skc12,skc17),true,ifeq3(forename(skc14,X0),true,X0,skc12),skc12),skc12) ).

cnf(u211,negated_conjecture,
    true = unisex(skc9,skc10) ).

cnf(u4986,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,skc14),true,ifeq3(theme(skc9,skc15,X1),true,ifeq3(agent(skc9,X0,X2),true,ifeq3(agent(skc9,skc15,X2),true,ifeq3(think_believe_consider(skc9,X0),true,ifeq3(proposition(skc9,X1),true,X1,skc14),skc14),skc14),skc14),skc14),skc14) ).

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

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

cnf(u3435,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc13),skc13),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u3815,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc12,X0),true,ifeq3(of(skc9,skc16,X0),true,ifeq3(entity(skc9,X0),true,skc12,skc16),skc16),skc16) ).

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

cnf(u2912,negated_conjecture,
    true = ifeq2(nonhuman(skc9,X0),true,nonhuman(skc14,X0),true) ).

cnf(u738,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc10),true) ).

cnf(u2684,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,relname(X0,skc16),true) ).

cnf(u3438,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,agent(X0,skf1(skc17),skc17),true) ).

cnf(u493,negated_conjecture,
    true = abstraction(skc9,skc14) ).

cnf(u3185,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X1),true,present(X1,skf1(X0)),true) ).

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

cnf(u1247,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc13),true,true,true),true) ).

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

cnf(u4302,negated_conjecture,
    skc14 = ifeq3(theme(skc9,X0,skc14),true,ifeq3(agent(skc9,X0,X1),true,ifeq3(agent(skc9,skc15,X1),true,ifeq3(think_believe_consider(skc9,X0),true,skc14,skc14),skc14),skc14),skc14) ).

cnf(u4456,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(agent(skc14,skc15,X1),true,ifeq3(agent(skc14,skc15,X1),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0) = X0 ).

cnf(u251,negated_conjecture,
    true = human_person(skc9,skc17) ).

cnf(u1252,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc13),true) ).

cnf(u5392,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(theme(skc14,skc15,X0),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14),skc14) ).

cnf(u506,negated_conjecture,
    true = ifeq2(entity(skc9,skc14),true,true,true) ).

cnf(u2008,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,organism(X0,skc13),true) ).

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

cnf(u5244,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0),X0) = X0 ).

cnf(u635,negated_conjecture,
    true = ifeq2(accessible_world(skc14,skc14),true,true,true) ).

cnf(u3967,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc12,X0),true,ifeq3(of(skc14,skc16,X0),true,ifeq3(entity(skc14,X0),true,skc12,skc16),skc16),skc16) ).

cnf(u2561,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(forename(X0,skc12),true,true,true),true) ).

cnf(u2294,negated_conjecture,
    true = ifeq2(living(skc9,X0),true,living(skc14,X0),true) ).

cnf(u504,negated_conjecture,
    true = unisex(skc9,skc14) ).

cnf(u2575,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,forename(X0,skc12),true) ).

cnf(u3169,negated_conjecture,
    true = ifeq2(smoke(skc9,skf1(X0)),true,true,true) ).

cnf(u3612,negated_conjecture,
    ifeq3(of(skc9,X0,skc13),true,ifeq3(of(skc9,X1,skc13),true,ifeq3(forename(skc9,X0),true,ifeq3(forename(skc9,X1),true,X0,X1),X1),X1),X1) = X1 ).

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

cnf(u763,negated_conjecture,
    true = thing(skc14,skc14) ).

cnf(u526,negated_conjecture,
    skc13 = skc11 ).

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

cnf(u1654,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,man(X0,skc13),true) ).

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

cnf(u265,negated_conjecture,
    true = organism(skc9,skc11) ).

cnf(u395,negated_conjecture,
    true = male(skc9,skc17) ).

cnf(u288,negated_conjecture,
    true = ifeq2(entity(skc9,skc15),true,true,true) ).

cnf(u4284,negated_conjecture,
    ifeq3(theme(skc9,skc15,X0),true,ifeq3(theme(skc9,X1,X2),true,ifeq3(agent(skc9,X1,skc17),true,ifeq3(think_believe_consider(skc9,X1),true,ifeq3(proposition(skc9,X0),true,ifeq3(proposition(skc9,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u138,negated_conjecture,
    true = man(skc9,skc17) ).

cnf(u547,negated_conjecture,
    b = ifeq(tuple(true,male(skc9,skc10)),tuple(true,true),a,b) ).

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

cnf(u779,negated_conjecture,
    true = singleton(skc14,skc14) ).

cnf(u654,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(eventuality(X0,skc10),true,true,true),true) ).

cnf(u1565,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skc10),true) ).

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

cnf(u1826,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc14,skc17),true),tuple(true,true),a,b) ).

cnf(u393,negated_conjecture,
    true = male(skc9,skc11) ).

cnf(u2076,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,entity(X0,skc13),true) ).

cnf(u1563,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(event(X0,skc10),true,true,true),true) ).

cnf(u294,negated_conjecture,
    true = ifeq2(eventuality(skc9,skc17),true,true,true) ).

cnf(u677,negated_conjecture,
    true = unisex(skc14,skc15) ).

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

cnf(u5497,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc13),X0),true,ifeq3(theme(skc14,skc15,X1),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(proposition(skc14,X0),true,ifeq3(proposition(skc14,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

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

cnf(u3372,negated_conjecture,
    true = of(skc14,skc16,skc17) ).

cnf(u675,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(eventuality(X0,skc15),true,true,true),true) ).

cnf(u2222,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,impartial(X0,skc13),true) ).

cnf(u1676,negated_conjecture,
    true = entity(skc14,skc13) ).

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

cnf(u800,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc13),true) ).

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

cnf(u572,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc9,skc13),true),tuple(true,true),a,b) ).

cnf(u3376,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,of(X0,skc16,skc17),true) ).

cnf(u1343,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(nonexistent(X0,skc10),true,true,true),true) ).

cnf(u551,negated_conjecture,
    b = ifeq(tuple(unisex(skc9,skc17),true),tuple(true,true),a,b) ).

cnf(u1697,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc14,skc13),true),tuple(true,true),a,b) ).

cnf(u3500,negated_conjecture,
    true = ifeq2(theme(skc9,X0,X1),true,theme(skc14,X0,X1),true) ).

cnf(u1453,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,unisex(X0,skc12),true) ).

cnf(u1438,negated_conjecture,
    true = unisex(skc14,skc16) ).

cnf(u2605,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(forename(X0,skc16),true,true,true),true) ).

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

cnf(u433,negated_conjecture,
    true = thing(skc9,skc16) ).

cnf(u665,negated_conjecture,
    true = eventuality(skc14,skc15) ).

cnf(u420,negated_conjecture,
    true = abstraction(skc9,skc12) ).

cnf(u2603,negated_conjecture,
    true = forename(skc14,skc16) ).

cnf(u1710,negated_conjecture,
    true = eventuality(skc14,skf1(X0)) ).

cnf(u949,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc15),true) ).

cnf(u176,negated_conjecture,
    true = ifeq2(man(skc14,X0),true,present(skc14,skf1(X1)),true) ).

cnf(u679,negated_conjecture,
    true = specific(skc14,skc15) ).

cnf(u554,negated_conjecture,
    b = ifeq(tuple(true,general(skc9,skc15)),tuple(true,true),a,b) ).

cnf(u2144,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(existent(X0,skc13),true,true,true),true) ).

cnf(u947,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,singleton(X0,skc12),true) ).

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

cnf(u560,negated_conjecture,
    b = ifeq(tuple(specific(skc9,skc14),true),tuple(true,true),a,b) ).

cnf(u439,negated_conjecture,
    true = singleton(skc9,skc16) ).

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

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

cnf(u682,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc15)),tuple(true,true),a,b) ).

cnf(u1350,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,nonexistent(X0,skc10),true) ).

cnf(u1709,negated_conjecture,
    true = ifeq2(state(skc14,skf1(X0)),true,true,true) ).

cnf(u2903,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(nonhuman(X0,skc12),true,true,true),true) ).

cnf(u577,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(state(X0,skc10),true,true,true),true) ).

cnf(u180,negated_conjecture,
    true = ifeq2(man(skc14,X0),true,agent(skc14,skf1(X0),X0),true) ).

cnf(u2494,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(male(X0,skc13),true,true,true),true) ).

cnf(u3136,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(jules_forename(X0,skc12),true,true,true),true) ).

cnf(u1348,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,nonexistent(X0,skc10),true) ).

cnf(u3655,negated_conjecture,
    skc16 = ifeq3(of(skc14,X0,skc17),true,ifeq3(forename(skc14,X0),true,X0,skc16),skc16) ).

cnf(u1750,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skf1(X1)),true) ).

cnf(u1221,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc10),true) ).

cnf(u4559,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(agent(skc14,skc15,X1),true,ifeq3(agent(skc14,X0,X1),true,ifeq3(think_believe_consider(skc14,X0),true,skc14,skc14),skc14),skc14),skc14) ).

cnf(u195,negated_conjecture,
    true = thing(skc9,skc10) ).

cnf(u3619,negated_conjecture,
    ifeq3(of(skc14,skc12,X0),true,ifeq3(of(skc14,X1,X0),true,ifeq3(forename(skc14,X1),true,ifeq3(entity(skc14,X0),true,skc12,X1),X1),X1),X1) = X1 ).

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

cnf(u600,negated_conjecture,
    true = specific(skc14,skc10) ).

cnf(u608,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc10),true,true,true) ).

cnf(u1225,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,specific(X0,skc15),true) ).

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

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

cnf(u3543,negated_conjecture,
    true = ifeq2(be(X0,skc10,skc13,skc13),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

cnf(u2009,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,organism(X0,skc17),true) ).

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

cnf(u2149,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,existent(X0,skc17),true) ).

cnf(u728,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u3439,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,agent(X0,skf1(skc13),skc13),true) ).

cnf(u4834,negated_conjecture,
    ifeq3(theme(skc14,skc15,X0),true,ifeq3(theme(skc14,X1,skc14),true,ifeq3(agent(skc14,X1,skc17),true,ifeq3(think_believe_consider(skc14,X1),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0),X0) = X0 ).

cnf(u5192,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,skc14,skc14),skc14),skc14),skc14) ).

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

cnf(u4527,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc13),skc14),true,ifeq3(agent(skc14,skc15,skc13),true,ifeq3(think_believe_consider(skc14,skf1(skc13)),true,skc14,skc14),skc14),skc14) ).

cnf(u3547,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,be(X0,skc10,skc13,skc13),true) ).

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

cnf(u4560,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skc15,X0),true,ifeq3(agent(skc14,skc15,X1),true,ifeq3(agent(skc14,skc15,X1),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14) ).

cnf(u1242,negated_conjecture,
    true = specific(skc14,skc13) ).

cnf(u2150,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,existent(X0,skc13),true) ).

cnf(u621,negated_conjecture,
    b = ifeq(tuple(true,male(skc14,skc10)),tuple(true,true),a,b) ).

cnf(u2423,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(animate(X0,skc17),true,true,true),true) ).

cnf(u4313,negated_conjecture,
    skc14 = ifeq3(agent(skc9,skc15,X0),true,ifeq3(agent(skc9,skc15,X0),true,skc14,skc14),skc14) ).

cnf(u634,negated_conjecture,
    true = ifeq2(accessible_world(skc14,skc9),true,true,true) ).

cnf(u775,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc14),true,true,true) ).

cnf(u3554,negated_conjecture,
    true = ifeq2(be(X0,skc10,skc13,skc13),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u233,negated_conjecture,
    true = nonexistent(skc9,skc15) ).

cnf(u3281,negated_conjecture,
    true = proposition(skc14,skc14) ).

cnf(u732,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(thing(X0,skc10),true,true,true),true) ).

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

cnf(u488,negated_conjecture,
    true = ifeq2(proposition(skc9,skc12),true,true,true) ).

cnf(u2687,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,relname(X0,skc12),true) ).

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

cnf(u1568,negated_conjecture,
    true = ifeq2(event(skc9,X0),true,event(skc14,X0),true) ).

cnf(u747,negated_conjecture,
    true = ifeq2(thing(skc9,X0),true,thing(skc14,X0),true) ).

cnf(u2784,negated_conjecture,
    true = general(skc14,skc14) ).

cnf(u239,negated_conjecture,
    true = singleton(skc9,skc15) ).

cnf(u3186,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,present(X0,skc15),true) ).

cnf(u1806,negated_conjecture,
    true = impartial(skc14,skc17) ).

cnf(u2285,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(living(X0,skc17),true,true,true),true) ).

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

cnf(u250,negated_conjecture,
    true = human_person(skc9,skc13) ).

cnf(u1409,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(unisex(X0,skc15),true,true,true),true) ).

cnf(u3859,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc16,skc13),true,ifeq3(of(skc9,skc16,skc13),true,skc16,skc16),skc16) ).

cnf(u2078,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,entity(X0,skc13),true) ).

cnf(u2292,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,living(X0,skc13),true) ).

cnf(u766,negated_conjecture,
    true = thing(skc14,skc12) ).

cnf(u4480,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc17),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc17)),true,skc14,skc14),skc14) ).

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

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

cnf(u1783,negated_conjecture,
    true = human_person(skc14,skc17) ).

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


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP224-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.35  % Computer : n005.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Sun Sep 27 18:32:17 UTC 2026
% 0.08/0.36  % CPUTime  : 
% 0.08/0.36  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38  Running first-order model finding
% 0.11/0.38  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.54  % (81363)Will run a generic schedule for satisfiability detection.
% 0.42/0.54  % (81370)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3296683750:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.42/0.54  % (81369)% WARNING: option uhcvi not known.
% 0.42/0.54  % (81368)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3701356658_2999 on theBenchmark for (2999ds/0Mi)
% 0.42/0.54  % (81369)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3397282271:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.42/0.54  % (81371)dis+10_1_sil=32000:sp=arity:random_seed=1232999759:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.42/0.54  % (81372)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2749254357:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.42/0.54  % (81373)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=601656624:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.42/0.54  % (81374)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2539423225:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.42/0.54  % TRYING [1]
% 0.42/0.54  % TRYING [2]
% 0.42/0.54  % TRYING [3]
% 0.42/0.54  % (81371)Instruction limit reached! 
% 0.42/0.54  % (81371)------------------------------
% 0.42/0.54  % (81371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.54  % (81371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.54  % (81371)CaDiCaL version: 2.1.3
% 0.42/0.54  % (81371)Termination reason: Instruction limit
% 0.42/0.54  % (81371)Termination phase: Saturation
% 0.42/0.54  % (81371)Time elapsed: 0.057 s
% 0.42/0.54  % (81371)Peak memory usage: 12 MB
% 0.42/0.54  % (81371)Instructions burned: 104 (million)
% 0.42/0.54  % (81372)Instruction limit reached! 
% 0.42/0.54  % (81372)------------------------------
% 0.42/0.54  % (81372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.54  % (81372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.54  % (81372)CaDiCaL version: 2.1.3
% 0.42/0.54  % (81372)Termination reason: Instruction limit
% 0.42/0.54  % (81372)Termination phase: Saturation
% 0.42/0.54  % (81372)Time elapsed: 0.066 s
% 0.42/0.54  % (81372)Peak memory usage: 13 MB
% 0.42/0.54  % (81372)Instructions burned: 117 (million)
% 0.42/0.54  % (81373)Instruction limit reached! 
% 0.42/0.54  % (81373)------------------------------
% 0.42/0.54  % (81373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.54  % (81373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.54  % (81373)CaDiCaL version: 2.1.3
% 0.42/0.54  % (81373)Termination reason: Instruction limit
% 0.42/0.54  % (81373)Termination phase: Saturation
% 0.42/0.54  % (81373)Time elapsed: 0.074 s
% 0.42/0.54  % (81373)Peak memory usage: 13 MB
% 0.42/0.54  % (81373)Instructions burned: 132 (million)
% 0.42/0.54  % (81382)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2646305098:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.42/0.54  % (81383)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=974089907:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.42/0.54  % (81374)Instruction limit reached! 
% 0.42/0.54  % (81374)------------------------------
% 0.42/0.54  % (81374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.54  % (81374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.54  % (81374)CaDiCaL version: 2.1.3
% 0.42/0.54  % (81374)Termination reason: Instruction limit
% 0.42/0.54  % (81374)Termination phase: Saturation
% 0.42/0.54  % (81374)Time elapsed: 0.090 s
% 0.42/0.54  % (81374)Peak memory usage: 12 MB
% 0.42/0.54  % (81374)Instructions burned: 160 (million)
% 0.42/0.54  % (81384)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=70951011:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.42/0.54  % TRYING [1]
% 0.42/0.54  % TRYING [2]
% 0.42/0.54  % (81370) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-81363-81370"...
% 0.42/0.54  % (81370)...printing done.
% 0.42/0.54  % (81387)ott-21_1_sil=16000:fs=off:random_seed=1791272856:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.42/0.54  % SZS status Satisfiable for theBenchmark
% 0.42/0.54  % SZS output start Saturation.
% See solution above
% 0.42/0.55  % SZS output start Definitions and Model Updates.
% 0.42/0.55  % SZS output end Definitions and Model Updates.
% 0.42/0.55  % (81370)------------------------------
% 0.42/0.55  % (81370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.55  % (81370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.55  % (81370)CaDiCaL version: 2.1.3
% 0.42/0.55  % (81370)Termination reason: Satisfiable
% 0.42/0.55  % (81370)Time elapsed: 0.117 s
% 0.42/0.55  % (81370)Peak memory usage: 15 MB
% 0.42/0.55  % (81370)Instructions burned: 384 (million)
% 0.42/0.55  % (81363)Success in time 0.147 s
% 0.42/0.55  % Vampire exiting
%------------------------------------------------------------------------------