Vampire---5.0.1.SAT-Sat.s

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

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

% Result   : Satisfiable 4.11s 2.31s
% Output   : Saturation 0.16s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,negated_conjecture,
    true = ifeq2(abstraction(skc12,skc15),true,true,true) ).

cnf(u1816,negated_conjecture,
    true = ifeq2(forename(skc8,X0),true,forename(skc12,X0),true) ).

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

cnf(u248,negated_conjecture,
    true = think_believe_consider(skc8,skc13) ).

cnf(u1415,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,organism(X0,skc10),true) ).

cnf(u3082,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0) = X0 ).

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

cnf(u659,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(thing(X0,skc15),true,true,true),true) ).

cnf(u2289,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,think_believe_consider(X0,skc13),true) ).

cnf(u1677,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human(X0,skc10),true,true,true),true) ).

cnf(u1567,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,impartial(X0,skc10),true) ).

cnf(u289,negated_conjecture,
    true = singleton(skc8,skc13) ).

cnf(u3301,negated_conjecture,
    ifeq3(theme(skc12,skc13,X0),true,ifeq3(theme(skc12,skf1(skc15),X1),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).

cnf(u1566,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,impartial(X0,skc15),true) ).

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

cnf(u1327,negated_conjecture,
    true = impartial(skc12,skc15) ).

cnf(u1298,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,thing(X1,skf1(X0)),true) ).

cnf(u1681,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,human(X0,skc10),true) ).

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

cnf(u295,negated_conjecture,
    true = organism(skc8,skc10) ).

cnf(u1570,negated_conjecture,
    true = ifeq2(impartial(skc8,X0),true,impartial(skc12,X0),true) ).

cnf(u2089,negated_conjecture,
    true = ifeq2(nonhuman(skc8,X0),true,nonhuman(skc12,X0),true) ).

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

cnf(u1819,negated_conjecture,
    true = forename(skc12,skc11) ).

cnf(u2079,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonhuman(X0,skc12),true,true,true),true) ).

cnf(u1825,negated_conjecture,
    true = relname(skc12,skc11) ).

cnf(u2990,negated_conjecture,
    ifeq3(theme(skc8,skc13,X0),true,ifeq3(proposition(skc8,X0),true,skc12,X0),X0) = X0 ).

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

cnf(u2614,negated_conjecture,
    skc11 = ifeq3(of(skc8,X0,skc15),true,ifeq3(of(skc8,skc11,skc15),true,ifeq3(forename(skc8,X0),true,X0,skc11),skc11),skc11) ).

cnf(u293,negated_conjecture,
    true = human_person(skc8,skc15) ).

cnf(u3224,negated_conjecture,
    ifeq3(theme(skc8,skc13,X0),true,ifeq3(theme(skc8,X1,skc12),true,ifeq3(agent(skc8,X1,skc15),true,ifeq3(think_believe_consider(skc8,X1),true,ifeq3(proposition(skc8,X0),true,skc12,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u3492,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0),X0) = X0 ).

cnf(u1715,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,animate(X0,skc15),true) ).

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

cnf(u2564,negated_conjecture,
    ifeq3(of(skc12,X0,skc15),true,ifeq3(forename(skc12,X0),true,skc14,X0),X0) = X0 ).

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

cnf(u1338,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human_person(X0,skc10),true,true,true),true) ).

cnf(u666,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,thing(X0,skc15),true) ).

cnf(u1332,negated_conjecture,
    true = existent(skc12,skc15) ).

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

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

cnf(u672,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,singleton(X0,skc10),true) ).

cnf(u306,negated_conjecture,
    true = thing(skc8,skc10) ).

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

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

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

cnf(u3283,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(theme(skc12,skc13,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12),skc12),skc12) ).

cnf(u2415,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,agent(X0,skc13,skc15),true) ).

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

cnf(u434,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc8,skc10)),tuple(true,true),a,b) ).

cnf(u1209,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,man(X0,skc10),true) ).

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

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

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

cnf(u578,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc10),true) ).

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

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

cnf(u432,negated_conjecture,
    b = ifeq(tuple(specific(skc8,skc12),true),tuple(true,true),a,b) ).

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

cnf(u833,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,nonexistent(X0,skc13),true) ).

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

cnf(u1987,negated_conjecture,
    true = nonhuman(skc12,skc12) ).

cnf(u1117,negated_conjecture,
    true = ifeq2(smoke(skc12,skc13),true,true,true) ).

cnf(u1498,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,entity(X0,skc10),true) ).

cnf(u1949,negated_conjecture,
    true = ifeq2(relation(skc8,X0),true,relation(skc12,X0),true) ).

cnf(u2419,negated_conjecture,
    true = ifeq2(agent(X0,skc13,skc15),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

cnf(u2263,negated_conjecture,
    true = ifeq2(present(X0,skc13),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

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

cnf(u1107,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,event(X0,skc9),true) ).

cnf(u1245,negated_conjecture,
    true = living(skc12,skc10) ).

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

cnf(u1226,negated_conjecture,
    true = smoke(skc12,skf1(X0)) ).

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

cnf(u2669,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc15),X2),true,ifeq3(theme(skc12,X1,X0),true,ifeq3(agent(skc12,X1,skc15),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,X1),true,ifeq3(proposition(skc12,X2),true,ifeq3(proposition(skc12,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

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

cnf(u2256,negated_conjecture,
    true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

cnf(u3551,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(theme(skc12,X0,X1),true,ifeq3(agent(skc12,X0,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12),skc12),skc12) ).

cnf(u474,negated_conjecture,
    b = ifeq(tuple(true,existent(skc12,skc9)),tuple(true,true),a,b) ).

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

cnf(u2761,negated_conjecture,
    ifeq3(of(skc8,skc11,skc15),true,ifeq3(of(skc8,X0,skc15),true,ifeq3(forename(skc8,X0),true,skc11,X0),X0),X0) = X0 ).

cnf(u2516,negated_conjecture,
    ifeq3(of(skc12,X1,skc15),true,ifeq3(of(skc12,X0,skc15),true,ifeq3(forename(skc12,X1),true,ifeq3(forename(skc12,X0),true,X1,X0),X0),X0),X0) = X0 ).

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

cnf(u2157,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(general(X0,skc12),true,true,true),true) ).

cnf(u1224,negated_conjecture,
    true = male(skc12,skc10) ).

cnf(u2911,negated_conjecture,
    ifeq3(of(skc12,skc11,skc15),true,ifeq3(of(skc12,X0,skc15),true,ifeq3(forename(skc12,X0),true,skc11,X0),X0),X0) = X0 ).

cnf(u217,negated_conjecture,
    true = sF9 ).

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

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

cnf(u1543,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,existent(X0,skc10),true) ).

cnf(u2262,negated_conjecture,
    true = present(skc12,skc13) ).

cnf(u472,negated_conjecture,
    b = ifeq(tuple(true,general(skc12,skc9)),tuple(true,true),a,b) ).

cnf(u1255,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(event(X1,skf1(X0)),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(u624,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc14),true) ).

cnf(u731,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc15),true) ).

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

cnf(u641,negated_conjecture,
    true = singleton(skc12,skc10) ).

cnf(u223,negated_conjecture,
    true = sF11 ).

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

cnf(u1260,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,event(X1,skf1(X0)),true) ).

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

cnf(u256,negated_conjecture,
    true = agent(skc8,skc13,skc15) ).

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

cnf(u2418,negated_conjecture,
    true = agent(skc12,skc13,skc15) ).

cnf(u515,negated_conjecture,
    true = singleton(skc12,skc13) ).

cnf(u3104,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,skc12,skc12),skc12),skc12) ).

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

cnf(u2562,negated_conjecture,
    skc11 = ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,X0,skc11),skc11) ).

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

cnf(u2291,negated_conjecture,
    true = think_believe_consider(skc12,skc13) ).

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

cnf(u232,negated_conjecture,
    true = sF14 ).

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

cnf(u1772,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,male(X0,skc15),true) ).

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

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

cnf(u273,negated_conjecture,
    true = ifeq2(state(skc8,skc13),true,true,true) ).

cnf(u1770,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(male(X0,skc10),true,true,true),true) ).

cnf(u633,negated_conjecture,
    true = singleton(skc12,skc12) ).

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

cnf(u1776,negated_conjecture,
    true = ifeq2(male(skc8,X0),true,male(skc12,X0),true) ).

cnf(u3167,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skc13,X0),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12) ).

cnf(u2312,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,proposition(X0,skc12),true) ).

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

cnf(u1679,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(human(X0,skc15),true,true,true),true) ).

cnf(u401,negated_conjecture,
    true = abstraction(skc8,skc12) ).

cnf(u1678,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(human(X0,skc10),true,true,true),true) ).

cnf(u522,negated_conjecture,
    true = ifeq2(accessible_world(skc12,skc8),true,true,true) ).

cnf(u1684,negated_conjecture,
    true = ifeq2(human(skc8,X0),true,human(skc12,X0),true) ).

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

cnf(u407,negated_conjecture,
    true = nonhuman(skc8,skc12) ).

cnf(u1682,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,human(X0,skc10),true) ).

cnf(u301,negated_conjecture,
    true = entity(skc8,skc10) ).

cnf(u300,negated_conjecture,
    true = entity(skc8,skc15) ).

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

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

cnf(u2456,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,be(X0,skc9,skc10,skc10),true) ).

cnf(u1322,negated_conjecture,
    b = ifeq(tuple(unisex(skc12,skc15),true),tuple(true,true),a,b) ).

cnf(u1408,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(organism(X0,skc10),true,true,true),true) ).

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

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

cnf(u1845,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(relname(X0,skc11),true,true,true),true) ).

cnf(u319,negated_conjecture,
    true = specific(skc8,skc15) ).

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

cnf(u2345,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,vincent_forename(X0,skc14),true) ).

cnf(u428,negated_conjecture,
    b = ifeq(tuple(true,general(skc8,skc10)),tuple(true,true),a,b) ).

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

cnf(u2462,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,theme(X0,skc13,skc12),true) ).

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

cnf(u1849,negated_conjecture,
    true = ifeq2(relname(skc8,X0),true,relname(skc12,X0),true) ).

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

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

cnf(u2585,negated_conjecture,
    skc11 = ifeq3(of(skc8,skc11,skc15),true,skc14,skc11) ).

cnf(u3616,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12),skc12),skc12),skc12) ).

cnf(u2473,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,be(X0,skc9,skc10,skc10),true) ).

cnf(u190,negated_conjecture,
    true = sF0 ).

cnf(u831,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(nonexistent(X0,skc9),true,true,true),true) ).

cnf(u1977,negated_conjecture,
    true = ifeq2(relname(skc12,skc12),true,true,true) ).

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

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

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

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

cnf(u2992,negated_conjecture,
    skc12 = ifeq3(agent(skc8,skc13,X0),true,ifeq3(agent(skc8,skc13,X0),true,skc12,skc12),skc12) ).

cnf(u1210,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,man(X0,skc15),true) ).

cnf(u2369,negated_conjecture,
    true = of(skc12,skc11,skc10) ).

cnf(u3418,negated_conjecture,
    ifeq3(theme(skc12,X0,X1),true,ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(agent(skc12,X0,skc10),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X1),true,skc12,X1),X1),X1),X1),X1),X1) = X1 ).

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

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

cnf(u2372,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,of(X0,skc11,skc10),true) ).

cnf(u1229,negated_conjecture,
    true = agent(skc12,skf1(skc10),skc10) ).

cnf(u1208,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(man(X0,skc10),true,true,true),true) ).

cnf(u2665,negated_conjecture,
    ifeq3(theme(skc12,X2,X1),true,ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(agent(skc12,X2,skc15),true,ifeq3(think_believe_consider(skc12,X2),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X1),true,ifeq3(proposition(skc12,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u328,negated_conjecture,
    true = impartial(skc8,skc15) ).

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

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

cnf(u2746,negated_conjecture,
    skc14 = ifeq3(of(skc8,skc14,skc10),true,ifeq3(of(skc8,skc14,skc10),true,skc14,skc14),skc14) ).

cnf(u1219,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(man(X0,skc10),true,true,true),true) ).

cnf(u974,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,unisex(X0,skc9),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(u2666,negated_conjecture,
    ifeq3(theme(skc12,X2,X1),true,ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(agent(skc12,X2,skc10),true,ifeq3(think_believe_consider(skc12,X2),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X1),true,ifeq3(proposition(skc12,X0),true,X0,X1),X1),X1),X1),X1),X1),X1) = X1 ).

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

cnf(u456,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,state(X0,skc9),true) ).

cnf(u1239,negated_conjecture,
    b = ifeq(tuple(unisex(skc12,skc10),true),tuple(true,true),a,b) ).

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

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

cnf(u2874,negated_conjecture,
    skc11 = ifeq3(of(skc12,skc11,skc15),true,ifeq3(of(skc12,skc11,skc15),true,skc11,skc11),skc11) ).

cnf(u345,negated_conjecture,
    true = male(skc8,skc15) ).

cnf(u612,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).

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

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

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

cnf(u2517,negated_conjecture,
    ifeq3(of(skc12,X1,skc10),true,ifeq3(of(skc12,X0,skc10),true,ifeq3(forename(skc12,X1),true,ifeq3(forename(skc12,X0),true,X1,X0),X0),X0),X0) = X0 ).

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

cnf(u2783,negated_conjecture,
    ifeq3(of(skc8,skc14,skc10),true,ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,skc14,X0),X0),X0) = X0 ).

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

cnf(u1314,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,man(X0,skc15),true) ).

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

cnf(u2413,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,agent(X0,skf1(skc15),skc15),true) ).

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

cnf(u2230,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(smoke(X1,skf1(X0)),true,true,true),true) ).

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

cnf(u1632,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(living(X0,skc10),true,true,true),true) ).

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

cnf(u3036,negated_conjecture,
    skc12 = ifeq3(theme(skc8,skc13,X0),true,ifeq3(proposition(skc8,X0),true,X0,skc12),skc12) ).

cnf(u1113,negated_conjecture,
    true = event(skc12,skc13) ).

cnf(u1773,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,male(X0,skc10),true) ).

cnf(u247,negated_conjecture,
    true = present(skc8,skc13) ).

cnf(u2426,negated_conjecture,
    true = ifeq2(agent(skc8,skf1(skc15),skc15),true,true,true) ).

cnf(u257,negated_conjecture,
    true = theme(skc8,skc13,skc12) ).

cnf(u617,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,singleton(X0,skc13),true) ).

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

cnf(u1771,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(male(X0,skc15),true,true,true),true) ).

cnf(u502,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,eventuality(X0,skc13),true) ).

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

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

cnf(u1540,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(existent(X0,skc10),true,true,true),true) ).

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

cnf(u2721,negated_conjecture,
    skc14 = ifeq3(of(skc8,skc11,X0),true,ifeq3(of(skc8,skc14,X0),true,ifeq3(entity(skc8,X0),true,skc11,skc14),skc14),skc14) ).

cnf(u245,negated_conjecture,
    true = vincent_forename(skc8,skc14) ).

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

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

cnf(u1538,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(existent(X0,skc10),true,true,true),true) ).

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

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

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

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

cnf(u1302,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,singleton(X1,skf1(X0)),true) ).

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

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

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

cnf(u391,negated_conjecture,
    true = ifeq2(jules_forename(skc8,skc14),true,true,true) ).

cnf(u3450,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,skc12,skc12),skc12),skc12),skc12) ).

cnf(u284,negated_conjecture,
    true = thing(skc8,skc13) ).

cnf(u1683,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,human(X0,skc15),true) ).

cnf(u2318,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(proposition(X0,skc12),true,true,true),true) ).

cnf(u2522,negated_conjecture,
    skc11 = ifeq3(of(skc8,X1,X0),true,ifeq3(of(skc8,skc11,X0),true,ifeq3(forename(skc8,X1),true,ifeq3(entity(skc8,X0),true,X1,skc11),skc11),skc11),skc11) ).

cnf(u3088,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0) = X0 ).

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

cnf(u1300,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(singleton(X1,skf1(X0)),true,true,true),true) ).

cnf(u285,negated_conjecture,
    true = specific(skc8,skc13) ).

cnf(u2590,negated_conjecture,
    skc14 = ifeq3(of(skc12,skc11,skc15),true,skc11,skc14) ).

cnf(u1829,negated_conjecture,
    true = ifeq2(proposition(skc12,skc11),true,true,true) ).

cnf(u2336,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(vincent_forename(X0,skc14),true,true,true),true) ).

cnf(u2983,negated_conjecture,
    ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc15),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,skc12,X1),X1),X1),X1) = X1 ).

cnf(u2287,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc13),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

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

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

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

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

cnf(u3594,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(theme(skc12,skc13,X0),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12),skc12),skc12),skc12) ).

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

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

cnf(u3251,negated_conjecture,
    ifeq3(theme(skc12,skc13,X1),true,ifeq3(theme(skc12,skc13,X0),true,ifeq3(proposition(skc12,X1),true,ifeq3(proposition(skc12,X0),true,X0,X1),X1),X1),X1) = X1 ).

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

cnf(u569,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc10),true,true,true),true) ).

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

cnf(u2848,negated_conjecture,
    skc11 = ifeq3(of(skc12,X0,skc15),true,ifeq3(of(skc12,skc11,skc15),true,ifeq3(forename(skc12,X0),true,X0,skc11),skc11),skc11) ).

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

cnf(u1340,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(human_person(X0,skc10),true,true,true),true) ).

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

cnf(u2470,negated_conjecture,
    true = ifeq2(be(X0,skc9,skc10,skc10),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

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

cnf(u2231,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,smoke(X1,skf1(X0)),true) ).

cnf(u400,negated_conjecture,
    true = ifeq2(relname(skc8,skc12),true,true,true) ).

cnf(u1321,negated_conjecture,
    true = animate(skc12,skc15) ).

cnf(u830,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(nonexistent(X0,skc13),true,true,true),true) ).

cnf(u2570,negated_conjecture,
    skc11 = ifeq3(of(skc8,skc14,skc10),true,skc14,skc11) ).

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

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

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

cnf(u1846,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,relname(X0,skc11),true) ).

cnf(u573,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(thing(X0,skc13),true,true,true),true) ).

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

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

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

cnf(u2605,negated_conjecture,
    skc14 = ifeq3(of(skc12,skc14,skc10),true,skc11,skc14) ).

cnf(u1344,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,human_person(X0,skc15),true) ).

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

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

cnf(u2632,negated_conjecture,
    skc11 = ifeq3(of(skc8,skc11,skc15),true,ifeq3(of(skc8,skc11,skc15),true,skc11,skc11),skc11) ).

cnf(u318,negated_conjecture,
    true = specific(skc8,skc10) ).

cnf(u440,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc8,skc10),true),tuple(true,true),a,b) ).

cnf(u2375,negated_conjecture,
    true = of(skc12,skc14,skc15) ).

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

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

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

cnf(u3013,negated_conjecture,
    skc12 = ifeq3(theme(skc8,X0,skc12),true,ifeq3(agent(skc8,X0,skc15),true,ifeq3(think_believe_consider(skc8,X0),true,skc12,skc12),skc12),skc12) ).

cnf(u1978,negated_conjecture,
    true = abstraction(skc12,skc12) ).

cnf(u1230,negated_conjecture,
    true = ifeq2(man(skc12,X0),true,true,true) ).

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

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

cnf(u1223,negated_conjecture,
    true = human_person(skc12,skc10) ).

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

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

cnf(u3676,negated_conjecture,
    ifeq3(theme(skc12,skc13,X0),true,ifeq3(theme(skc12,skf1(skc10),X1),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1115,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(event(X0,skc13),true,true,true),true) ).

cnf(u1347,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc12,skc15),true),tuple(true,true),a,b) ).

cnf(u1104,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(event(X0,skc13),true,true,true),true) ).

cnf(u329,negated_conjecture,
    true = impartial(skc8,skc10) ).

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

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

cnf(u352,negated_conjecture,
    true = relation(skc8,skc14) ).

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

cnf(u202,negated_conjecture,
    true = sF4 ).

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

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

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

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

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

cnf(u3151,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,X1),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12) ).

cnf(u724,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(specific(X0,skc9),true,true,true),true) ).

cnf(u2259,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,present(X0,skc13),true) ).

cnf(u741,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(specific(X0,skc10),true,true,true),true) ).

cnf(u2449,negated_conjecture,
    true = ifeq2(theme(X0,skc13,skc12),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u973,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,unisex(X0,skc13),true) ).

cnf(u1495,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(entity(X0,skc15),true,true,true),true) ).

cnf(u1633,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(living(X0,skc15),true,true,true),true) ).

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

cnf(u630,negated_conjecture,
    true = ifeq2(entity(skc12,skc12),true,true,true) ).

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

cnf(u2525,negated_conjecture,
    ifeq3(of(skc12,skc11,X1),true,ifeq3(of(skc12,X0,X1),true,ifeq3(forename(skc12,X0),true,ifeq3(entity(skc12,X1),true,skc11,X0),X0),X0),X0) = X0 ).

cnf(u2410,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc10),skc10),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

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

cnf(u463,negated_conjecture,
    true = specific(skc12,skc9) ).

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

cnf(u486,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,eventuality(X0,skc9),true) ).

cnf(u3198,negated_conjecture,
    skc12 = ifeq3(theme(skc8,X0,skc12),true,ifeq3(theme(skc8,skc13,X1),true,ifeq3(agent(skc8,X0,skc15),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc12),skc12),skc12),skc12),skc12) ).

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

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

cnf(u986,negated_conjecture,
    true = unisex(skc12,skc12) ).

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

cnf(u1541,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(existent(X0,skc15),true,true,true),true) ).

cnf(u229,negated_conjecture,
    true = sF13 ).

cnf(u1775,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,male(X0,skc10),true) ).

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

cnf(u1539,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(existent(X0,skc15),true,true,true),true) ).

cnf(u729,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc10),true) ).

cnf(u1847,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,relname(X0,skc14),true) ).

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

cnf(u3079,negated_conjecture,
    ifeq3(theme(skc12,X0,X1),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(proposition(skc12,X1),true,skc12,X1),X1),X1),X1) = X1 ).

cnf(u743,negated_conjecture,
    b = ifeq(tuple(true,general(skc12,skc10)),tuple(true,true),a,b) ).

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

cnf(u1286,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(specific(X1,skf1(X0)),true,true,true),true) ).

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

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

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

cnf(u503,negated_conjecture,
    true = unisex(skc12,skc13) ).

cnf(u1249,negated_conjecture,
    true = existent(skc12,skc10) ).

cnf(u246,negated_conjecture,
    true = event(skc8,skc13) ).

cnf(u1290,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,specific(X1,skf1(X0)),true) ).

cnf(u1564,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(impartial(X0,skc10),true,true,true),true) ).

cnf(u746,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,specific(X0,skc10),true) ).

cnf(u1284,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,nonexistent(X1,skf1(X0)),true) ).

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

cnf(u1414,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,organism(X0,skc15),true) ).

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

cnf(u2320,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,proposition(X0,skc12),true) ).

cnf(u287,negated_conjecture,
    true = unisex(skc8,skc13) ).

cnf(u501,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(eventuality(X0,skc13),true,true,true),true) ).

cnf(u752,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,specific(X0,skc15),true) ).

cnf(u258,negated_conjecture,
    true = of(skc8,skc11,skc10) ).

cnf(u2313,negated_conjecture,
    true = ifeq2(proposition(skc8,X0),true,proposition(skc12,X0),true) ).

cnf(u396,negated_conjecture,
    true = ifeq2(proposition(skc8,skc14),true,true,true) ).

cnf(u2258,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,present(X0,skf1(X1)),true) ).

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

cnf(u244,negated_conjecture,
    true = forename(skc8,skc14) ).

cnf(u1288,negated_conjecture,
    b = ifeq(tuple(true,general(skc12,skf1(X0))),tuple(true,true),a,b) ).

cnf(u2595,negated_conjecture,
    skc11 = ifeq3(of(skc12,skc14,skc10),true,skc14,skc11) ).

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

cnf(u1412,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,organism(X0,skc15),true) ).

cnf(u2566,negated_conjecture,
    ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X0),true,skc11,X0),X0) = X0 ).

cnf(u1941,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relation(X0,skc12),true,true,true),true) ).

cnf(u1831,negated_conjecture,
    true = abstraction(skc12,skc11) ).

cnf(u386,negated_conjecture,
    true = unisex(skc8,skc14) ).

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

cnf(u1275,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(unisex(X1,skf1(X0)),true,true,true),true) ).

cnf(u1416,negated_conjecture,
    true = ifeq2(organism(skc8,X0),true,organism(skc12,X0),true) ).

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

cnf(u2337,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,vincent_forename(X0,skc14),true) ).

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

cnf(u3299,negated_conjecture,
    ifeq3(theme(skc12,skc13,X0),true,ifeq3(theme(skc12,X1,skc12),true,ifeq3(agent(skc12,X1,skc15),true,ifeq3(think_believe_consider(skc12,X1),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0),X0) = X0 ).

cnf(u2454,negated_conjecture,
    true = ifeq2(be(X0,skc9,skc10,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

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

cnf(u664,negated_conjecture,
    true = ifeq2(eventuality(skc12,skc15),true,true,true) ).

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

cnf(u2341,negated_conjecture,
    true = vincent_forename(skc12,skc14) ).

cnf(u1305,negated_conjecture,
    true = man(skc12,skc15) ).

cnf(u1328,negated_conjecture,
    true = living(skc12,skc15) ).

cnf(u3438,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,skc12,skc12),skc12),skc12),skc12),skc12) ).

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

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

cnf(u286,negated_conjecture,
    true = nonexistent(skc8,skc13) ).

cnf(u2086,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,nonhuman(X0,skc12),true) ).

cnf(u426,negated_conjecture,
    b = ifeq(tuple(true,general(skc8,skc15)),tuple(true,true),a,b) ).

cnf(u1836,negated_conjecture,
    true = general(skc12,skc11) ).

cnf(u2560,negated_conjecture,
    skc14 = ifeq3(of(skc12,X0,skc15),true,ifeq3(forename(skc12,X0),true,X0,skc14),skc14) ).

cnf(u1341,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(human_person(X0,skc15),true,true,true),true) ).

cnf(u2616,negated_conjecture,
    skc11 = ifeq3(of(skc8,skc14,X0),true,ifeq3(of(skc8,skc11,X0),true,ifeq3(entity(skc8,X0),true,skc14,skc11),skc11),skc11) ).

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

cnf(u2364,negated_conjecture,
    true = ifeq2(of(skc8,X1,X0),true,of(skc12,X1,X0),true) ).

cnf(u1214,negated_conjecture,
    true = man(skc12,skc10) ).

cnf(u1958,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(abstraction(X0,skc12),true,true,true),true) ).

cnf(u424,negated_conjecture,
    b = ifeq(tuple(unisex(skc8,skc10),true),tuple(true,true),a,b) ).

cnf(u1207,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(man(X0,skc15),true,true,true),true) ).

cnf(u972,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(unisex(X0,skc13),true,true,true),true) ).

cnf(u2378,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,of(X0,skc14,skc15),true) ).

cnf(u574,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,thing(X0,skc13),true) ).

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

cnf(u2720,negated_conjecture,
    skc14 = ifeq3(of(skc8,X0,skc10),true,ifeq3(of(skc8,skc14,skc10),true,ifeq3(forename(skc8,X0),true,X0,skc14),skc14),skc14) ).

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

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

cnf(u2615,negated_conjecture,
    skc11 = ifeq3(of(skc8,skc11,X0),true,ifeq3(of(skc8,skc11,X0),true,ifeq3(entity(skc8,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u2518,negated_conjecture,
    ifeq3(of(skc8,X1,skc10),true,ifeq3(of(skc8,X0,skc10),true,ifeq3(forename(skc8,X1),true,ifeq3(forename(skc8,X0),true,X1,X0),X0),X0),X0) = X0 ).

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

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

cnf(u1345,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,human_person(X0,skc10),true) ).

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

cnf(u441,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc8,skc15),true),tuple(true,true),a,b) ).

cnf(u580,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,thing(X0,skc13),true) ).

cnf(u597,negated_conjecture,
    true = thing(skc12,skc15) ).

cnf(u336,negated_conjecture,
    true = human(skc8,skc15) ).

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

cnf(u2370,negated_conjecture,
    true = ifeq2(of(X0,skc11,skc10),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

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

cnf(u2225,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(jules_forename(X0,skc11),true,true,true),true) ).

cnf(u3004,negated_conjecture,
    skc12 = ifeq3(theme(skc8,X0,X1),true,ifeq3(agent(skc8,X0,skc15),true,ifeq3(think_believe_consider(skc8,X0),true,ifeq3(proposition(skc8,X1),true,X1,skc12),skc12),skc12),skc12) ).

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

cnf(u725,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(specific(X0,skc13),true,true,true),true) ).

cnf(u3420,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(theme(skc12,X1,skc12),true,ifeq3(agent(skc12,X1,skc15),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,X1),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0),X0),X0) = X0 ).

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

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

cnf(u1631,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(living(X0,skc10),true,true,true),true) ).

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

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

cnf(u340,negated_conjecture,
    true = animate(skc8,skc15) ).

cnf(u1630,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(living(X0,skc15),true,true,true),true) ).

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

cnf(u1544,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,existent(X0,skc15),true) ).

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

cnf(u3417,negated_conjecture,
    ifeq3(theme(skc12,X0,X1),true,ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X1),true,skc12,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1636,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,living(X0,skc10),true) ).

cnf(u1499,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,entity(X0,skc15),true) ).

cnf(u740,negated_conjecture,
    true = specific(skc12,skc15) ).

cnf(u1634,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,living(X0,skc15),true) ).

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

cnf(u468,negated_conjecture,
    true = ifeq2(abstraction(skc12,skc9),true,true,true) ).

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

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

cnf(u727,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,specific(X0,skc9),true) ).

cnf(u1774,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,male(X0,skc15),true) ).

cnf(u2411,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc15),skc15),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

cnf(u357,negated_conjecture,
    true = abstraction(skc8,skc14) ).

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

cnf(u487,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,eventuality(X0,skc13),true) ).

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

cnf(u380,negated_conjecture,
    true = general(skc8,skc14) ).

cnf(u1542,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,existent(X0,skc15),true) ).

cnf(u2414,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,agent(X0,skf1(skc10),skc10),true) ).

cnf(u1768,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(male(X0,skc10),true,true,true),true) ).

cnf(u730,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,specific(X0,skc13),true) ).

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

cnf(u253,negated_conjecture,
    true = accessible_world(skc8,skc12) ).

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

cnf(u485,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(eventuality(X0,skc9),true,true,true),true) ).

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

cnf(u2425,negated_conjecture,
    true = ifeq2(agent(skc8,skf1(skc10),skc10),true,true,true) ).

cnf(u508,negated_conjecture,
    true = ifeq2(abstraction(skc12,skc13),true,true,true) ).

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

cnf(u1269,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,eventuality(X1,skf1(X0)),true) ).

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

cnf(u243,negated_conjecture,
    true = man(skc8,skc15) ).

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

cnf(u1815,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,forename(X0,skc14),true) ).

cnf(u1273,negated_conjecture,
    true = thing(skc12,skf1(X0)) ).

cnf(u1259,negated_conjecture,
    true = eventuality(skc12,skf1(X0)) ).

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

cnf(u455,negated_conjecture,
    true = event(skc12,skc9) ).

cnf(u642,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,thing(X0,skc10),true) ).

cnf(u1308,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(man(X0,skc15),true,true,true),true) ).

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

cnf(u241,negated_conjecture,
    true = sF17 ).

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

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

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

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

cnf(u1279,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X1),true,unisex(X1,skf1(X0)),true) ).

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

cnf(u1289,negated_conjecture,
    true = ifeq2(entity(skc12,skf1(X0)),true,true,true) ).

cnf(u1312,negated_conjecture,
    true = human_person(skc12,skc15) ).

cnf(u1413,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,organism(X0,skc10),true) ).

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

cnf(u3243,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(theme(skc12,skc13,X1),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12),skc12) ).

cnf(u309,negated_conjecture,
    true = ifeq2(eventuality(skc8,skc10),true,true,true) ).

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

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

cnf(u2343,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(vincent_forename(X0,skc14),true,true,true),true) ).

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

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

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

cnf(u1820,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(forename(X0,skc11),true,true,true),true) ).

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

cnf(u2561,negated_conjecture,
    skc11 = ifeq3(of(skc12,X0,skc10),true,ifeq3(forename(skc12,X0),true,X0,skc11),skc11) ).

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

cnf(u310,negated_conjecture,
    true = singleton(skc8,skc10) ).

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

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

cnf(u408,negated_conjecture,
    true = general(skc8,skc12) ).

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

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

cnf(u1315,negated_conjecture,
    true = agent(skc12,skf1(skc15),skc15) ).

cnf(u1946,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,relation(X0,skc12),true) ).

cnf(u297,negated_conjecture,
    true = organism(skc8,skc15) ).

cnf(u427,negated_conjecture,
    b = ifeq(tuple(true,general(skc8,skc13)),tuple(true,true),a,b) ).

cnf(u2469,negated_conjecture,
    true = be(skc12,skc9,skc10,skc10) ).

cnf(u1211,negated_conjecture,
    true = ifeq2(man(skc8,X0),true,man(skc12,X0),true) ).

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

cnf(u2365,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,of(X0,skc11,skc10),true) ).

cnf(u425,negated_conjecture,
    b = ifeq(tuple(unisex(skc8,skc15),true),tuple(true,true),a,b) ).

cnf(u2227,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,jules_forename(X0,skc11),true) ).

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

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

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

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

cnf(u1708,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(animate(X0,skc15),true,true,true),true) ).

cnf(u1342,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,human_person(X0,skc15),true) ).

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

cnf(u1244,negated_conjecture,
    true = impartial(skc12,skc10) ).

cnf(u3149,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skc13,X1),true,ifeq3(agent(skc12,skc13,X0),true,ifeq3(agent(skc12,skc13,X0),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12) ).

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

cnf(u1712,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,animate(X0,skc15),true) ).

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

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

cnf(u832,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(nonexistent(X0,skc13),true,true,true),true) ).

cnf(u199,negated_conjecture,
    true = sF3 ).

cnf(u1986,negated_conjecture,
    true = general(skc12,skc12) ).

cnf(u337,negated_conjecture,
    true = human(skc8,skc10) ).

cnf(u324,negated_conjecture,
    true = existent(skc8,skc10) ).

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

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

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

cnf(u1346,negated_conjecture,
    true = ifeq2(human_person(skc8,X0),true,human_person(skc12,X0),true) ).

cnf(u726,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,specific(X0,skc13),true) ).

cnf(u1637,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,living(X0,skc15),true) ).

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

cnf(u376,negated_conjecture,
    true = nonhuman(skc8,skc14) ).

cnf(u1635,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,living(X0,skc10),true) ).

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

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

cnf(u3421,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(theme(skc12,X1,skc12),true,ifeq3(agent(skc12,X1,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,X1),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u208,negated_conjecture,
    true = sF6 ).

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

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

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

cnf(u341,negated_conjecture,
    true = animate(skc8,skc10) ).

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

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

cnf(u2265,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,present(X0,skc13),true) ).

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

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

cnf(u214,negated_conjecture,
    true = sF8 ).

cnf(u3549,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(theme(skc12,skf1(skc10),X1),true,ifeq3(agent(skc12,X0,skc10),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12),skc12),skc12) ).

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

cnf(u623,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc13),true) ).

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

cnf(u2255,negated_conjecture,
    true = ifeq2(present(X0,skc13),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u1106,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(event(X0,skc9),true,true,true),true) ).

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

cnf(u2670,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc10),X2),true,ifeq3(theme(skc12,X1,X0),true,ifeq3(agent(skc12,X1,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,X1),true,ifeq3(proposition(skc12,X2),true,ifeq3(proposition(skc12,X0),true,X0,X2),X2),X2),X2),X2),X2),X2) = X2 ).

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

cnf(u720,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc15),true,true,true),true) ).

cnf(u2409,negated_conjecture,
    true = ifeq2(agent(X0,skc13,skc15),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u492,negated_conjecture,
    true = eventuality(skc12,skc13) ).

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

cnf(u2565,negated_conjecture,
    ifeq3(of(skc12,X0,skc10),true,ifeq3(forename(skc12,X0),true,skc11,X0),X0) = X0 ).

cnf(u2526,negated_conjecture,
    ifeq3(of(skc8,skc11,X1),true,ifeq3(of(skc8,X0,X1),true,ifeq3(forename(skc8,X0),true,ifeq3(entity(skc8,X1),true,skc11,X0),X0),X0),X0) = X0 ).

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

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

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

cnf(u632,negated_conjecture,
    true = ifeq2(eventuality(skc12,skc12),true,true,true) ).

cnf(u511,negated_conjecture,
    true = ifeq2(entity(skc12,skc13),true,true,true) ).

cnf(u3092,negated_conjecture,
    skc12 = ifeq3(agent(skc12,skc13,X0),true,ifeq3(agent(skc12,skc13,X0),true,skc12,skc12),skc12) ).

cnf(u484,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(eventuality(X0,skc13),true,true,true),true) ).

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

cnf(u254,negated_conjecture,
    true = proposition(skc8,skc12) ).

cnf(u1243,negated_conjecture,
    true = entity(skc12,skc10) ).

cnf(u3575,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(theme(skc12,skc13,X1),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).

cnf(u1292,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(thing(X1,skf1(X0)),true,true,true),true) ).

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

cnf(u1270,negated_conjecture,
    true = unisex(skc12,skf1(X0)) ).

cnf(u509,negated_conjecture,
    b = ifeq(tuple(true,existent(skc12,skc13)),tuple(true,true),a,b) ).

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

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

cnf(u3440,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(theme(skc12,X0,skc12),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,X0),true,skc12,skc12),skc12),skc12),skc12),skc12) ).

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

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

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

cnf(u1268,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(eventuality(X1,skf1(X0)),true,true,true),true) ).

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

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

cnf(u523,negated_conjecture,
    true = ifeq2(accessible_world(skc12,skc12),true,true,true) ).

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

cnf(u2850,negated_conjecture,
    skc11 = ifeq3(of(skc12,skc11,X0),true,ifeq3(of(skc12,skc11,X0),true,ifeq3(entity(skc12,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u1272,negated_conjecture,
    true = specific(skc12,skf1(X0)) ).

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

cnf(u3458,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,skc12,skc12),skc12),skc12),skc12) ).

cnf(u3313,negated_conjecture,
    ifeq3(theme(skc12,skc13,X0),true,ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0) = X0 ).

cnf(u2455,negated_conjecture,
    true = ifeq2(be(skc8,X2,X1,X0),true,be(skc12,X2,X1,X0),true) ).

cnf(u1313,negated_conjecture,
    true = male(skc12,skc15) ).

cnf(u3628,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12),skc12),skc12),skc12) ).

cnf(u1545,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,existent(X0,skc10),true) ).

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

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

cnf(u3090,negated_conjecture,
    ifeq3(theme(skc12,skc13,X0),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0) = X0 ).

cnf(u2460,negated_conjecture,
    true = ifeq2(theme(X0,skc13,skc12),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

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

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

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

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

cnf(u398,negated_conjecture,
    true = relation(skc8,skc12) ).

cnf(u1319,negated_conjecture,
    true = organism(skc12,skc15) ).

cnf(u2338,negated_conjecture,
    true = ifeq2(vincent_forename(skc8,X0),true,vincent_forename(skc12,X0),true) ).

cnf(u1844,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(relname(X0,skc14),true,true,true),true) ).

cnf(u670,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(singleton(X0,skc10),true,true,true),true) ).

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

cnf(u1562,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(impartial(X0,skc15),true,true,true),true) ).

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

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

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

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

cnf(u1568,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,impartial(X0,skc10),true) ).

cnf(u1339,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human_person(X0,skc15),true,true,true),true) ).

cnf(u1326,negated_conjecture,
    true = entity(skc12,skc15) ).

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

cnf(u3510,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u2220,negated_conjecture,
    true = ifeq2(jules_forename(skc8,X0),true,jules_forename(skc12,X0),true) ).

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

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

cnf(u567,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(thing(X0,skc13),true,true,true),true) ).

cnf(u1330,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc12,skc15)),tuple(true,true),a,b) ).

cnf(u1713,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,animate(X0,skc10),true) ).

cnf(u1228,negated_conjecture,
    true = event(skc12,skf1(X0)) ).

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

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

cnf(u3128,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,skc12,skc12),skc12),skc12) ).

cnf(u3099,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,skc12,skc12),skc12) ).

cnf(u681,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,singleton(X0,skc15),true) ).

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

cnf(u1410,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(organism(X0,skc10),true,true,true),true) ).

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

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

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

cnf(u835,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,nonexistent(X0,skc13),true) ).

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

cnf(u449,negated_conjecture,
    true = state(skc12,skc9) ).

cnf(u3548,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(theme(skc12,skf1(skc15),X1),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12),skc12),skc12) ).

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

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

cnf(u2376,negated_conjecture,
    true = ifeq2(of(X0,skc14,skc15),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

cnf(u3148,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(agent(skc12,skc13,X1),true,ifeq3(agent(skc12,X0,X1),true,ifeq3(think_believe_consider(skc12,X0),true,skc12,skc12),skc12),skc12),skc12) ).

cnf(u1970,negated_conjecture,
    true = relation(skc12,skc12) ).

cnf(u2421,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,agent(X0,skc13,skc15),true) ).

cnf(u325,negated_conjecture,
    true = existent(skc8,skc15) ).

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

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

cnf(u593,negated_conjecture,
    true = thing(skc12,skc10) ).

cnf(u348,negated_conjecture,
    true = relname(skc8,skc11) ).

cnf(u3163,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12),skc12) ).

cnf(u1638,negated_conjecture,
    true = ifeq2(living(skc8,X0),true,living(skc12,X0),true) ).

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

cnf(u1109,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,event(X0,skc13),true) ).

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

cnf(u978,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,unisex(X0,skc13),true) ).

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

cnf(u1494,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(entity(X0,skc10),true,true,true),true) ).

cnf(u721,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc13),true,true,true),true) ).

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

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

cnf(u196,negated_conjecture,
    true = sF2 ).

cnf(u1237,negated_conjecture,
    true = human(skc12,skc10) ).

cnf(u610,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(singleton(X0,skc13),true,true,true),true) ).

cnf(u967,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(unisex(X0,skc13),true,true,true),true) ).

cnf(u1492,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(entity(X0,skc15),true,true,true),true) ).

cnf(u211,negated_conjecture,
    true = sF7 ).

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

cnf(u616,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(singleton(X0,skc13),true,true,true),true) ).

cnf(u2167,negated_conjecture,
    true = ifeq2(general(skc8,X0),true,general(skc12,X0),true) ).

cnf(u1119,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,event(X0,skc13),true) ).

cnf(u2521,negated_conjecture,
    skc11 = ifeq3(of(skc12,X1,X0),true,ifeq3(of(skc12,skc11,X0),true,ifeq3(forename(skc12,X1),true,ifeq3(entity(skc12,X0),true,X1,skc11),skc11),skc11),skc11) ).

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

cnf(u238,negated_conjecture,
    true = sF16 ).

cnf(u1227,negated_conjecture,
    true = present(skc12,skf1(X0)) ).

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

cnf(u1496,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,entity(X0,skc15),true) ).

cnf(u2451,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,theme(X0,skc13,skc12),true) ).

cnf(u738,negated_conjecture,
    true = specific(skc12,skc10) ).

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

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

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

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

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

cnf(u464,negated_conjecture,
    true = nonexistent(skc12,skc9) ).

cnf(u1247,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc12,skc10)),tuple(true,true),a,b) ).

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

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

cnf(u2806,negated_conjecture,
    skc14 = ifeq3(of(skc12,X0,skc10),true,ifeq3(of(skc12,skc14,skc10),true,ifeq3(forename(skc12,X0),true,X0,skc14),skc14),skc14) ).

cnf(u1277,negated_conjecture,
    b = ifeq(tuple(true,male(skc12,skf1(X0))),tuple(true,true),a,b) ).

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

cnf(u1258,negated_conjecture,
    true = ifeq2(state(skc12,skf1(X0)),true,true,true) ).

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

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

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

cnf(u637,negated_conjecture,
    true = ifeq2(abstraction(skc12,skc10),true,true,true) ).

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

cnf(u2311,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(proposition(X0,skc12),true,true,true),true) ).

cnf(u506,negated_conjecture,
    true = thing(skc12,skc13) ).

cnf(u226,negated_conjecture,
    true = sF12 ).

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

cnf(u635,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(thing(X0,skc10),true,true,true),true) ).

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

cnf(u249,negated_conjecture,
    true = jules_forename(skc8,skc11) ).

cnf(u2316,negated_conjecture,
    true = proposition(skc12,skc12) ).

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

cnf(u2294,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,think_believe_consider(X0,skc13),true) ).

cnf(u504,negated_conjecture,
    true = nonexistent(skc12,skc13) ).

cnf(u2575,negated_conjecture,
    skc14 = ifeq3(of(skc8,skc11,skc15),true,skc11,skc14) ).

cnf(u3441,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(theme(skc12,X0,skc12),true,ifeq3(agent(skc12,X0,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,X0),true,skc12,skc12),skc12),skc12),skc12),skc12) ).

cnf(u1297,negated_conjecture,
    true = singleton(skc12,skf1(X0)) ).

cnf(u1283,negated_conjecture,
    b = ifeq(tuple(true,existent(skc12,skf1(X0))),tuple(true,true),a,b) ).

cnf(u3720,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc10),X1),true,ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X1),true,ifeq3(proposition(skc12,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

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

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

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

cnf(u1822,negated_conjecture,
    true = ifeq2(vincent_forename(skc12,skc11),true,true,true) ).

cnf(u510,negated_conjecture,
    b = ifeq(tuple(true,general(skc12,skc13)),tuple(true,true),a,b) ).

cnf(u1828,negated_conjecture,
    true = relation(skc12,skc11) ).

cnf(u1411,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(organism(X0,skc15),true,true,true),true) ).

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

cnf(u1565,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(impartial(X0,skc15),true,true,true),true) ).

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

cnf(u1826,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,forename(X0,skc11),true) ).

cnf(u1546,negated_conjecture,
    true = ifeq2(existent(skc8,X0),true,existent(skc12,X0),true) ).

cnf(u393,negated_conjecture,
    true = ifeq2(smoke(skc8,skc13),true,true,true) ).

cnf(u1563,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(impartial(X0,skc10),true,true,true),true) ).

cnf(u2600,negated_conjecture,
    skc11 = ifeq3(of(skc12,skc11,skc15),true,skc14,skc11) ).

cnf(u2450,negated_conjecture,
    true = ifeq2(theme(skc8,X1,X0),true,theme(skc12,X1,X0),true) ).

cnf(u1569,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,impartial(X0,skc15),true) ).

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

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

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

cnf(u1676,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(human(X0,skc15),true,true,true),true) ).

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

cnf(u3480,negated_conjecture,
    ifeq3(theme(skc12,skc13,X0),true,ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,skc12,X0),X0),X0),X0),X0) = X0 ).

cnf(u1320,negated_conjecture,
    true = human(skc12,skc15) ).

cnf(u2722,negated_conjecture,
    skc14 = ifeq3(of(skc8,skc14,X0),true,ifeq3(of(skc8,skc14,X0),true,ifeq3(entity(skc8,X0),true,skc14,skc14),skc14),skc14) ).

cnf(u305,negated_conjecture,
    true = ifeq2(entity(skc8,skc13),true,true,true) ).

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

cnf(u292,negated_conjecture,
    true = human_person(skc8,skc10) ).

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

cnf(u3245,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc15),X1),true,ifeq3(theme(skc12,skc13,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X1),true,ifeq3(proposition(skc12,X0),true,X0,X1),X1),X1),X1),X1) = X1 ).

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

cnf(u1343,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,human_person(X0,skc10),true) ).

cnf(u1680,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,human(X0,skc15),true) ).

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

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

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

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

cnf(u1711,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(animate(X0,skc15),true,true,true),true) ).

cnf(u433,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc8,skc15)),tuple(true,true),a,b) ).

cnf(u2580,negated_conjecture,
    skc14 = ifeq3(of(skc8,skc14,skc10),true,skc11,skc14) ).

cnf(u665,negated_conjecture,
    true = singleton(skc12,skc15) ).

cnf(u420,negated_conjecture,
    b = ifeq(tuple(true,male(skc8,skc13)),tuple(true,true),a,b) ).

cnf(u1835,negated_conjecture,
    true = nonhuman(skc12,skc11) ).

cnf(u1710,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(animate(X0,skc10),true,true,true),true) ).

cnf(u679,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(singleton(X0,skc15),true,true,true),true) ).

cnf(u1716,negated_conjecture,
    true = ifeq2(animate(skc8,X0),true,animate(skc12,X0),true) ).

cnf(u2363,negated_conjecture,
    true = ifeq2(of(X0,skc11,skc10),true,ifeq2(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u333,negated_conjecture,
    true = living(skc8,skc10) ).

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

cnf(u439,negated_conjecture,
    b = ifeq(tuple(true,existent(skc8,skc13)),tuple(true,true),a,b) ).

cnf(u1714,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,animate(X0,skc10),true) ).

cnf(u3150,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc10),X0),true,ifeq3(agent(skc12,skc13,skc10),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,ifeq3(proposition(skc12,X0),true,X0,skc12),skc12),skc12),skc12) ).

cnf(u1963,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,abstraction(X0,skc12),true) ).

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

cnf(u834,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,nonexistent(X0,skc9),true) ).

cnf(u2889,negated_conjecture,
    ifeq3(of(skc12,skc14,skc10),true,ifeq3(of(skc12,X0,skc10),true,ifeq3(forename(skc12,X0),true,skc14,X0),X0),X0) = X0 ).

cnf(u2223,negated_conjecture,
    true = jules_forename(skc12,skc11) ).

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

cnf(u1709,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(animate(X0,skc10),true,true,true),true) ).

cnf(u437,negated_conjecture,
    b = ifeq(tuple(human(skc8,skc12),true),tuple(true,true),a,b) ).

cnf(u2412,negated_conjecture,
    true = ifeq2(agent(skc8,X1,X0),true,agent(skc12,X1,X0),true) ).

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

cnf(u332,negated_conjecture,
    true = living(skc8,skc15) ).

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

cnf(u344,negated_conjecture,
    true = male(skc8,skc10) ).

cnf(u591,negated_conjecture,
    true = thing(skc12,skc12) ).

cnf(u205,negated_conjecture,
    true = sF5 ).

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

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

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

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

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

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

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

cnf(u349,negated_conjecture,
    true = relname(skc8,skc14) ).

cnf(u450,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(state(X0,skc9),true,true,true),true) ).

cnf(u1225,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,man(X0,skc10),true) ).

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

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

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

cnf(u722,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(specific(X0,skc10),true,true,true),true) ).

cnf(u193,negated_conjecture,
    true = sF1 ).

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

cnf(u1238,negated_conjecture,
    true = animate(skc12,skc10) ).

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

cnf(u3439,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(theme(skc12,skf1(skc10),skc12),true,ifeq3(agent(skc12,X0,skc10),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(think_believe_consider(skc12,skf1(skc10)),true,skc12,skc12),skc12),skc12),skc12),skc12) ).

cnf(u362,negated_conjecture,
    true = ifeq2(abstraction(skc8,skc10),true,true,true) ).

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

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

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

cnf(u220,negated_conjecture,
    true = sF10 ).

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

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

cnf(u1493,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(entity(X0,skc10),true,true,true),true) ).

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

cnf(u2459,negated_conjecture,
    true = theme(skc12,skc13,skc12) ).

cnf(u235,negated_conjecture,
    true = sF15 ).

cnf(u1236,negated_conjecture,
    true = organism(skc12,skc10) ).

cnf(u467,negated_conjecture,
    true = ifeq2(smoke(skc12,skc9),true,true,true) ).

cnf(u3550,negated_conjecture,
    skc12 = ifeq3(theme(skc12,skf1(skc15),skc12),true,ifeq3(theme(skc12,X0,X1),true,ifeq3(agent(skc12,X0,skc15),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,X0),true,ifeq3(proposition(skc12,X1),true,X1,skc12),skc12),skc12),skc12),skc12),skc12) ).

cnf(u621,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,singleton(X0,skc10),true) ).

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

cnf(u3698,negated_conjecture,
    ifeq3(theme(skc12,skf1(skc15),X1),true,ifeq3(theme(skc12,skf1(skc15),X0),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(think_believe_consider(skc12,skf1(skc15)),true,ifeq3(proposition(skc12,X1),true,ifeq3(proposition(skc12,X0),true,X0,X1),X1),X1),X1),X1),X1) = X1 ).

cnf(u1497,negated_conjecture,
    true = ifeq2(accessible_world(skc12,X0),true,entity(X0,skc10),true) ).

cnf(u1251,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc12,skc10),true),tuple(true,true),a,b) ).

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

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

cnf(u1278,negated_conjecture,
    true = ifeq2(abstraction(skc12,skf1(X0)),true,true,true) ).

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

cnf(u2824,negated_conjecture,
    skc14 = ifeq3(of(skc12,skc14,skc10),true,ifeq3(of(skc12,skc14,skc10),true,skc14,skc14),skc14) ).

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

cnf(u749,negated_conjecture,
    b = ifeq(tuple(true,general(skc12,skc15)),tuple(true,true),a,b) ).

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

cnf(u1271,negated_conjecture,
    true = nonexistent(skc12,skf1(X0)) ).

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

cnf(u1281,negated_conjecture,
    true = ifeq2(accessible_world(X1,skc12),true,ifeq2(nonexistent(X1,skf1(X0)),true,true,true),true) ).

cnf(u2164,negated_conjecture,
    true = ifeq2(accessible_world(skc8,X0),true,general(X0,skc12),true) ).

cnf(u747,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc12),true,ifeq2(specific(X0,skc15),true,true,true),true) ).

cnf(u3077,negated_conjecture,
    skc12 = ifeq3(theme(skc12,X0,skc12),true,ifeq3(agent(skc12,X0,X1),true,ifeq3(agent(skc12,skc13,X1),true,ifeq3(think_believe_consider(skc12,X0),true,skc12,skc12),skc12),skc12),skc12) ).

cnf(u640,negated_conjecture,
    true = ifeq2(eventuality(skc12,skc10),true,true,true) ).

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

cnf(u507,negated_conjecture,
    b = ifeq(tuple(true,male(skc12,skc13)),tuple(true,true),a,b) ).

cnf(u494,negated_conjecture,
    true = ifeq2(state(skc12,skc13),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 = forename(skc8,skc11) ).

cnf(u1409,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(organism(X0,skc15),true,true,true),true) ).

cnf(u1812,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(forename(X0,skc14),true,true,true),true) ).

cnf(u1769,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc8),true,ifeq2(male(X0,skc15),true,true,true),true) ).

cnf(u2292,negated_conjecture,
    true = ifeq2(think_believe_consider(X0,skc13),true,ifeq2(accessible_world(X0,skc12),true,true,true),true) ).

cnf(u3078,negated_conjecture,
    ifeq3(theme(skc12,skc13,X1),true,ifeq3(agent(skc12,skc13,X0),true,ifeq3(agent(skc12,skc13,X0),true,ifeq3(proposition(skc12,X1),true,skc12,X1),X1),X1),X1) = X1 ).

cnf(u3205,negated_conjecture,
    ifeq3(theme(skc8,skc13,X1),true,ifeq3(theme(skc8,skc13,X0),true,ifeq3(proposition(skc8,X1),true,ifeq3(proposition(skc8,X0),true,X0,X1),X1),X1),X1) = X1 ).

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(u505,negated_conjecture,
    true = specific(skc12,skc13) ).

cnf(u278,negated_conjecture,
    true = eventuality(skc8,skc13) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : NLP226-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38  % Computer : n019.cluster.edu
% 0.10/0.38  % Model    : x86_64 x86_64
% 0.10/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38  % Memory   : 8046.5625MB
% 0.10/0.38  % OS       : Linux 6.8.0-71-generic
% 0.10/0.38  % CPULimit : 300
% 0.10/0.38  % WCLimit  : 300
% 0.10/0.38  % DateTime : Sun Sep 27 18:32:57 UTC 2026
% 0.10/0.38  % CPUTime  : 
% 0.10/0.38  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41  Running first-order theorem proving
% 0.10/0.42  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.11/2.31  % (3319937)Detected a unit-equality problem, will run specialized UEQ schedule.
% 4.11/2.31  % (3319942)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1096176376:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 4.11/2.31  % (3319943)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=393007193:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 4.11/2.31  % (3319944)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1109844566:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 4.11/2.31  % (3319945)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2023440729:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 4.11/2.31  % (3319946)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2517821751:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 4.11/2.31  % (3319947)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2508606872:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 4.11/2.31  % (3319948)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1210045926:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 4.11/2.31  % (3319945)Instruction limit reached! 
% 4.11/2.31  % (3319945)------------------------------
% 4.11/2.31  % (3319945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319945)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319945)Termination reason: Instruction limit
% 4.11/2.31  % (3319945)Termination phase: Saturation
% 4.11/2.31  % (3319945)Time elapsed: 0.066 s
% 4.11/2.31  % (3319945)Peak memory usage: 87 MB
% 4.11/2.31  % (3319945)Instructions burned: 137 (million)
% 4.11/2.31  % (3319946)Instruction limit reached! 
% 4.11/2.31  % (3319946)------------------------------
% 4.11/2.31  % (3319946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319946)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319946)Termination reason: Instruction limit
% 4.11/2.31  % (3319946)Termination phase: Saturation
% 4.11/2.31  % (3319946)Time elapsed: 0.103 s
% 4.11/2.31  % (3319946)Peak memory usage: 89 MB
% 4.11/2.31  % (3319946)Instructions burned: 182 (million)
% 4.11/2.31  % (3319947)Instruction limit reached! 
% 4.11/2.31  % (3319947)------------------------------
% 4.11/2.31  % (3319947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319947)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319947)Termination reason: Instruction limit
% 4.11/2.31  % (3319947)Termination phase: Saturation
% 4.11/2.31  % (3319947)Time elapsed: 0.159 s
% 4.11/2.31  % (3319947)Peak memory usage: 92 MB
% 4.11/2.31  % (3319947)Instructions burned: 258 (million)
% 4.11/2.31  % (3319948)Refutation not found, incomplete strategy
% 4.11/2.31  % (3319948)------------------------------
% 4.11/2.31  % (3319948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319948)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319948)Termination reason: Refutation not found, incomplete strategy
% 4.11/2.31  % (3319948)Time elapsed: 0.182 s
% 4.11/2.31  % (3319948)Peak memory usage: 91 MB
% 4.11/2.31  % (3319948)Instructions burned: 314 (million)
% 4.11/2.31  % (3319956)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=432118000:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 4.11/2.31  % (3319957)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=415685564:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 4.11/2.31  % (3319958)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=341103501:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 4.11/2.31  % (3319958)Instruction limit reached! 
% 4.11/2.31  % (3319958)------------------------------
% 4.11/2.31  % (3319958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319958)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319958)Termination reason: Instruction limit
% 4.11/2.31  % (3319958)Termination phase: Saturation
% 4.11/2.31  % (3319958)Time elapsed: 0.110 s
% 4.11/2.31  % (3319958)Peak memory usage: 93 MB
% 4.11/2.31  % (3319958)Instructions burned: 216 (million)
% 4.11/2.31  % (3319948)------------------------------
% 4.11/2.31  % (3319948)------------------------------
% 4.11/2.31  % (3319962)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=353760546:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 4.11/2.31  % (3319963)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=113641244:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 4.11/2.31  % (3319962)Instruction limit reached! 
% 4.11/2.31  % (3319962)------------------------------
% 4.11/2.31  % (3319962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319962)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319962)Termination reason: Instruction limit
% 4.11/2.31  % (3319962)Termination phase: Saturation
% 4.11/2.31  % (3319962)Time elapsed: 0.168 s
% 4.11/2.31  % (3319962)Peak memory usage: 95 MB
% 4.11/2.31  % (3319962)Instructions burned: 318 (million)
% 4.11/2.31  % (3319942)Refutation not found, incomplete strategy
% 4.11/2.31  % (3319942)------------------------------
% 4.11/2.31  % (3319942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319942)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319942)Termination reason: Refutation not found, incomplete strategy
% 4.11/2.31  % (3319942)Time elapsed: 0.814 s
% 4.11/2.31  % (3319942)Peak memory usage: 140 MB
% 4.11/2.31  % (3319942)Instructions burned: 2126 (million)
% 4.11/2.31  % (3319966)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1926926247:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 4.11/2.31  % (3319942)------------------------------
% 4.11/2.31  % (3319942)------------------------------
% 4.11/2.31  % (3319968)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2422063198:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 4.11/2.31  % (3319966)First to succeed.
% 4.11/2.31  % (3319966)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3319937"
% 4.11/2.31  % (3319943)Also succeeded, but the first one will report.
% 4.11/2.31  % (3319944)Also succeeded, but the first one will report.
% 4.11/2.31  % SZS status Satisfiable for theBenchmark
% 4.11/2.31  % SZS output start Saturation.
% See solution above
% 0.16/2.50  % SZS output start Definitions and Model Updates.
% 0.16/2.50  % SZS output end Definitions and Model Updates.
% 0.16/2.50  % (3319966)------------------------------
% 0.16/2.50  % (3319966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.50  % (3319966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.50  % (3319966)CaDiCaL version: 2.1.3
% 0.16/2.50  % (3319966)Termination reason: Satisfiable
% 0.16/2.50  % (3319966)Time elapsed: 0.219 s
% 0.16/2.50  % (3319966)Peak memory usage: 93 MB
% 0.16/2.50  % (3319966)Instructions burned: 353 (million)
% 0.16/2.50  % (3319966)------------------------------
% 0.16/2.50  % (3319966)------------------------------
% 0.16/2.50  % (3319937)Success in time 1.457 s
% 0.16/2.50  % Vampire exiting
%------------------------------------------------------------------------------