Vampire---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NLP224-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 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:00 PM UTC 2026

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

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,thing(X0,skc17),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1422,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,organism(X0,skc11),true) ).

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

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

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

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

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

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

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

cnf(u1825,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,male(X0,skc11),true) ).

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

cnf(u1334,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(human_person(X0,skc11),true,true,true),true) ).

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

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

cnf(u3510,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,skc14,skc14),skc14),skc14),skc14) ).

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

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

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

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

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

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

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

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

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

cnf(u1336,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human_person(X0,skc11),true,true,true),true) ).

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

cnf(u828,negated_conjecture,
    b = ifeq(tuple(true,general(skc14,skc11)),tuple(true,true),a,b) ).

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

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

cnf(u2368,negated_conjecture,
    true = proposition(skc14,skc14) ).

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

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

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

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

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

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

cnf(u1734,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,human(X0,skc11),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1222,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(event(X0,skc15),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(u1353,negated_conjecture,
    true = agent(skc14,skf1(skc17),skc17) ).

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

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

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

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

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

cnf(u1226,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,event(X0,skc15),true) ).

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

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

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

cnf(u474,negated_conjecture,
    b = ifeq(tuple(true,male(skc9,skc10)),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(u1339,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,human_person(X0,skc11),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u234,negated_conjecture,
    true = sF14 ).

cnf(u515,negated_conjecture,
    true = specific(skc14,skc10) ).

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

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

cnf(u1264,negated_conjecture,
    true = human(skc14,skc11) ).

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

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

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

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

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

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

cnf(u2981,negated_conjecture,
    ifeq3(of(skc14,skc16,skc11),true,ifeq3(of(skc14,X0,skc11),true,ifeq3(forename(skc14,X0),true,skc16,X0),X0),X0) = X0 ).

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

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

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

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

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

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

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

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

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

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

cnf(u2696,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc16,skc11),true,skc12,skc16) ).

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

cnf(u1776,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(animate(X0,skc11),true,true,true),true) ).

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

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

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

cnf(u1419,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(organism(X0,skc17),true,true,true),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(u279,negated_conjecture,
    true = ifeq2(state(skc9,skc15),true,true,true) ).

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

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

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

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

cnf(u2571,negated_conjecture,
    ifeq3(of(skc9,X1,skc11),true,ifeq3(of(skc9,X0,skc11),true,ifeq3(forename(skc9,X1),true,ifeq3(forename(skc9,X0),true,X1,X0),X0),X0),X0) = X0 ).

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

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

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

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

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

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

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

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

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

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

cnf(u1596,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,existent(X0,skc11),true) ).

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

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

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

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

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

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

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

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

cnf(u246,negated_conjecture,
    true = sF18 ).

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

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

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

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

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

cnf(u3491,negated_conjecture,
    skc14 = ifeq3(theme(skc14,X0,skc14),true,ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(agent(skc14,X0,skc11),true,ifeq3(think_believe_consider(skc14,X0),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,skc14,skc14),skc14),skc14),skc14),skc14) ).

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

cnf(u568,negated_conjecture,
    true = specific(skc14,skc15) ).

cnf(u2858,negated_conjecture,
    skc16 = ifeq3(of(skc14,X0,skc11),true,ifeq3(of(skc14,skc16,skc11),true,ifeq3(forename(skc14,X0),true,X0,skc16),skc16),skc16) ).

cnf(u1677,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,living(X0,skc11),true) ).

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

cnf(u831,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,specific(X0,skc11),true) ).

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

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

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

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

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

cnf(u1337,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human_person(X0,skc11),true) ).

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

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

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

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

cnf(u2618,negated_conjecture,
    ifeq3(of(skc9,X0,skc11),true,ifeq3(forename(skc9,X0),true,skc12,X0),X0) = X0 ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u201,negated_conjecture,
    true = sF3 ).

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

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

cnf(u1246,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(man(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u2415,negated_conjecture,
    true = ifeq2(of(X0,skc12,skc11),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

cnf(u207,negated_conjecture,
    true = sF5 ).

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

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

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

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

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

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

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

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

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

cnf(u1643,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,impartial(X0,skc11),true) ).

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

cnf(u216,negated_conjecture,
    true = sF8 ).

cnf(u2530,negated_conjecture,
    true = be(skc14,skc10,skc11,skc11) ).

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

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

cnf(u479,negated_conjecture,
    b = ifeq(tuple(true,general(skc9,skc15)),tuple(true,true),a,b) ).

cnf(u617,negated_conjecture,
    true = thing(skc14,skc11) ).

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

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

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

cnf(u1531,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,entity(X0,skc11),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u240,negated_conjecture,
    true = sF16 ).

cnf(u1265,negated_conjecture,
    true = animate(skc14,skc11) ).

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

cnf(u1672,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(living(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u1827,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,male(X0,skc11),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(u1304,negated_conjecture,
    true = ifeq2(abstraction(skc14,skf1(X0)),true,true,true) ).

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

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

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

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

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

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

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

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

cnf(u402,negated_conjecture,
    true = singleton(skc9,skc16) ).

cnf(u2614,negated_conjecture,
    skc12 = ifeq3(of(skc9,X0,skc11),true,ifeq3(forename(skc9,X0),true,X0,skc12),skc12) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3562,negated_conjecture,
    ifeq3(theme(skc14,skf1(skc11),X0),true,ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,ifeq3(proposition(skc14,X0),true,skc14,X0),X0),X0),X0),X0) = X0 ).

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

cnf(u1232,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,man(X0,skc11),true) ).

cnf(u2527,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,be(X0,skc10,skc11,skc11),true) ).

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

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

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

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

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

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

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

cnf(u2525,negated_conjecture,
    true = ifeq2(be(X0,skc10,skc11,skc11),true,ifeq2(accessible_world(X0,skc9),true,true,true),true) ).

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

cnf(u231,negated_conjecture,
    true = sF13 ).

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

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

cnf(u636,negated_conjecture,
    true = singleton(skc14,skc11) ).

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

cnf(u486,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc9,skc11)),tuple(true,true),a,b) ).

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 = thing(skc14,skc14) ).

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

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

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

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

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

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

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

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

cnf(u2531,negated_conjecture,
    true = ifeq2(be(X0,skc10,skc11,skc11),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

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

cnf(u2424,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,of(X0,skc12,skc11),true) ).

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

cnf(u1780,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,animate(X0,skc11),true) ).

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

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

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

cnf(u219,negated_conjecture,
    true = sF9 ).

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

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

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

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

cnf(u1284,negated_conjecture,
    true = ifeq2(state(skc14,skf1(X0)),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u1418,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(organism(X0,skc11),true,true,true),true) ).

cnf(u1266,negated_conjecture,
    b = ifeq(tuple(unisex(skc14,skc11),true),tuple(true,true),a,b) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u814,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,specific(X0,skc11),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1591,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(existent(X0,skc11),true,true,true),true) ).

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

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

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

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

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

cnf(u430,negated_conjecture,
    true = ifeq2(proposition(skc9,skc12),true,true,true) ).

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

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

cnf(u2876,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc16,skc11),true,ifeq3(of(skc14,skc16,skc11),true,skc16,skc16),skc16) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u595,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,thing(X0,skc11),true) ).

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

cnf(u1679,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,living(X0,skc11),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1636,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(impartial(X0,skc11),true,true,true),true) ).

cnf(u213,negated_conjecture,
    true = sF7 ).

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

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

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

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

cnf(u1775,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(animate(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u1779,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,animate(X0,skc11),true) ).

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

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

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

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

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

cnf(u1526,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(entity(X0,skc11),true,true,true),true) ).

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

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

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

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

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

cnf(u228,negated_conjecture,
    true = sF12 ).

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

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

cnf(u1250,negated_conjecture,
    true = human_person(skc14,skc11) ).

cnf(u237,negated_conjecture,
    true = sF15 ).

cnf(u1524,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(entity(X0,skc11),true,true,true),true) ).

cnf(u243,negated_conjecture,
    true = sF17 ).

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

cnf(u269,negated_conjecture,
    true = thing(skc9,skc10) ).

cnf(u520,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc10),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u2569,negated_conjecture,
    ifeq3(of(skc14,X1,skc11),true,ifeq3(of(skc14,X0,skc11),true,ifeq3(forename(skc14,X1),true,ifeq3(forename(skc14,X0),true,X1,X0),X0),X0),X0) = X0 ).

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

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

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

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

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

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

cnf(u2534,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,be(X0,skc10,skc11,skc11),true) ).

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

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

cnf(u2772,negated_conjecture,
    skc16 = ifeq3(of(skc9,X0,skc11),true,ifeq3(of(skc9,skc16,skc11),true,ifeq3(forename(skc9,X0),true,X0,skc16),skc16),skc16) ).

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

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

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

cnf(u809,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc10),true,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(u1417,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(organism(X0,skc11),true,true,true),true) ).

cnf(u1820,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(male(X0,skc11),true,true,true),true) ).

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

cnf(u823,negated_conjecture,
    true = specific(skc14,skc11) ).

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

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

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

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

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

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

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

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

cnf(u3644,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(theme(skc14,skf1(skc11),X0),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,ifeq3(proposition(skc14,X0),true,X0,skc14),skc14),skc14),skc14),skc14) ).

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

cnf(u2721,negated_conjecture,
    skc16 = ifeq3(of(skc14,skc16,skc11),true,skc12,skc16) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1595,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,existent(X0,skc11),true) ).

cnf(u826,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(specific(X0,skc11),true,true,true),true) ).

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

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

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

cnf(u2617,negated_conjecture,
    ifeq3(of(skc14,X0,skc11),true,ifeq3(forename(skc14,X0),true,skc12,X0),X0) = X0 ).

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

cnf(u2417,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,of(X0,skc12,skc11),true) ).

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

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

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

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

cnf(u454,negated_conjecture,
    true = of(skc9,skc12,skc11) ).

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

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

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

cnf(u1729,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(human(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u452,negated_conjecture,
    skc13 = skc11 ).

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(skc9,skc15,X1),true,ifeq3(theme(skc9,skc15,X2),true,ifeq3(agent(skc9,skc15,X0),true,ifeq3(agent(skc9,skc15,X0),true,ifeq3(proposition(skc9,X1),true,ifeq3(proposition(skc9,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).

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

cnf(u2444,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,agent(X0,skf1(skc11),skc11),true) ).

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

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

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

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

cnf(u1217,negated_conjecture,
    true = ifeq2(event(skc9,X0),true,event(skc14,X0),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2422,negated_conjecture,
    true = ifeq2(of(X0,skc12,skc11),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

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

cnf(u632,negated_conjecture,
    true = ifeq2(abstraction(skc14,skc11),true,true,true) ).

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

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

cnf(u1257,negated_conjecture,
    true = ifeq2(man(skc14,X0),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(u2572,negated_conjecture,
    skc16 = ifeq3(of(skc14,X1,X0),true,ifeq3(of(skc14,skc16,X0),true,ifeq3(forename(skc14,X1),true,ifeq3(entity(skc14,X0),true,X1,skc16),skc16),skc16),skc16) ).

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

cnf(u225,negated_conjecture,
    true = sF11 ).

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

cnf(u1270,negated_conjecture,
    true = entity(skc14,skc11) ).

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

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

cnf(u2440,negated_conjecture,
    true = ifeq2(agent(X0,skf1(skc11),skc11),true,ifeq2(accessible_world(X0,skc14),true,true,true),true) ).

cnf(u480,negated_conjecture,
    b = ifeq(tuple(true,general(skc9,skc11)),tuple(true,true),a,b) ).

cnf(u1263,negated_conjecture,
    true = organism(skc14,skc11) ).

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

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

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

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

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

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

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

cnf(u1274,negated_conjecture,
    b = ifeq(tuple(true,nonhuman(skc14,skc11)),tuple(true,true),a,b) ).

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

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

cnf(u2835,negated_conjecture,
    ifeq3(of(skc9,skc16,skc11),true,ifeq3(of(skc9,X0,skc11),true,ifeq3(forename(skc9,X0),true,skc16,X0),X0),X0) = X0 ).

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

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

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

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

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

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

cnf(u1529,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,entity(X0,skc11),true) ).

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

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

cnf(u807,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(specific(X0,skc11),true,true,true),true) ).

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

cnf(u1272,negated_conjecture,
    true = living(skc14,skc11) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2613,negated_conjecture,
    skc12 = ifeq3(of(skc14,X0,skc11),true,ifeq3(forename(skc14,X0),true,X0,skc12),skc12) ).

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

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

cnf(u292,negated_conjecture,
    true = nonexistent(skc9,skc15) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u588,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(thing(X0,skc11),true,true,true),true) ).

cnf(u681,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(singleton(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u192,negated_conjecture,
    true = sF0 ).

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

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

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

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

cnf(u1730,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(human(X0,skc11),true,true,true),true) ).

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

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

cnf(u1638,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(impartial(X0,skc11),true,true,true),true) ).

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

cnf(u198,negated_conjecture,
    true = sF2 ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u476,negated_conjecture,
    b = ifeq(tuple(unisex(skc9,skc11),true),tuple(true,true),a,b) ).

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

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

cnf(u1368,negated_conjecture,
    true = impartial(skc14,skc17) ).

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

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

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

cnf(u1241,negated_conjecture,
    true = man(skc14,skc11) ).

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

cnf(u2019,negated_conjecture,
    true = general(skc14,skc14) ).

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

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

cnf(u493,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc9,skc11),true),tuple(true,true),a,b) ).

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

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

cnf(u1277,negated_conjecture,
    b = ifeq(tuple(nonexistent(skc14,skc11),true),tuple(true,true),a,b) ).

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

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

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

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

cnf(u1252,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,man(X0,skc11),true) ).

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

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

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

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

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

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

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

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

cnf(u635,negated_conjecture,
    true = ifeq2(eventuality(skc14,skc11),true,true,true) ).

cnf(u1256,negated_conjecture,
    true = agent(skc14,skf1(skc11),skc11) ).

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

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

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

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

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

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

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

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

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

cnf(u1421,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,organism(X0,skc11),true) ).

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

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

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

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

cnf(u1822,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(male(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u654,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(thing(X0,skc17),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(skc9,X0),true,male(X0,skc17),true) ).

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

cnf(u3202,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(agent(skc14,skc15,skc11),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,skc14,skc14),skc14),skc14) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1674,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(living(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

cnf(u3493,negated_conjecture,
    skc14 = ifeq3(theme(skc14,skf1(skc11),skc14),true,ifeq3(theme(skc14,X0,skc14),true,ifeq3(agent(skc14,X0,skc11),true,ifeq3(think_believe_consider(skc14,skf1(skc11)),true,ifeq3(think_believe_consider(skc14,X0),true,skc14,skc14),skc14),skc14),skc14),skc14) ).

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

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

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

cnf(u700,negated_conjecture,
    true = ifeq2(accessible_world(skc9,X0),true,singleton(X0,skc11),true) ).

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

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

cnf(u1592,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc14),true,ifeq2(existent(X0,skc11),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u1350,negated_conjecture,
    true = human_person(skc14,skc17) ).

cnf(u1733,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,human(X0,skc11),true) ).

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

cnf(u180,negated_conjecture,
    true = ifeq2(man(skc14,X0),true,agent(skc14,skf1(X0),X0),true) ).

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

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

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

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

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

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

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

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

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

cnf(u2711,negated_conjecture,
    skc12 = ifeq3(of(skc14,skc16,skc11),true,skc16,skc12) ).

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

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

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

cnf(u195,negated_conjecture,
    true = sF1 ).

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

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

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

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

cnf(u2798,negated_conjecture,
    skc16 = ifeq3(of(skc9,skc16,skc11),true,ifeq3(of(skc9,skc16,skc11),true,skc16,skc16),skc16) ).

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

cnf(u222,negated_conjecture,
    true = sF10 ).

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

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

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

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

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

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

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

cnf(u1231,negated_conjecture,
    true = ifeq2(accessible_world(X0,skc9),true,ifeq2(man(X0,skc11),true,true,true),true) ).

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

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

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

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

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

cnf(u2686,negated_conjecture,
    skc12 = ifeq3(of(skc9,skc16,skc11),true,skc16,skc12) ).

cnf(u2459,negated_conjecture,
    true = ifeq2(agent(skc9,skf1(skc11),skc11),true,true,true) ).

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

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

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

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

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

cnf(u210,negated_conjecture,
    true = sF6 ).

cnf(u1251,negated_conjecture,
    true = male(skc14,skc11) ).

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

cnf(u2421,negated_conjecture,
    true = of(skc14,skc12,skc11) ).

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

cnf(u1271,negated_conjecture,
    true = impartial(skc14,skc11) ).

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,skc14),true,ifeq2(event(X1,skf1(X0)),true,true,true),true) ).

cnf(u1641,negated_conjecture,
    true = ifeq2(accessible_world(skc14,X0),true,impartial(X0,skc11),true) ).

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

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

cnf(u204,negated_conjecture,
    true = sF4 ).

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

cnf(u1276,negated_conjecture,
    true = existent(skc14,skc11) ).

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

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(u1287,negated_conjecture,
    true = ifeq2(eventuality(skc9,skf1(X0)),true,true,true) ).

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

cnf(u531,negated_conjecture,
    true = ifeq2(accessible_world(skc14,skc9),true,true,true) ).

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

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

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

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

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

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

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


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP224-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39  % Computer : n019.cluster.edu
% 0.13/0.39  % Model    : x86_64 x86_64
% 0.13/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39  % Memory   : 8046.5625MB
% 0.13/0.39  % OS       : Linux 6.8.0-71-generic
% 0.13/0.39  % CPULimit : 300
% 0.13/0.39  % WCLimit  : 300
% 0.13/0.39  % DateTime : Sun Sep 27 18:32:34 UTC 2026
% 0.13/0.39  % CPUTime  : 
% 0.13/0.39  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43  Running first-order theorem proving
% 0.13/0.43  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  % (3319508)Detected a unit-equality problem, will run specialized UEQ schedule.
% 4.11/2.31  % (3319513)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=2637646553:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 4.11/2.31  % (3319517)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2396342493:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 4.11/2.31  % (3319515)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1732789305:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 4.11/2.31  % (3319516)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2632133006:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 4.11/2.31  % (3319514)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=90137631:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 4.11/2.31  % (3319518)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3067574253:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 4.11/2.31  % (3319519)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2021547030:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 4.11/2.31  % (3319516)Instruction limit reached! 
% 4.11/2.31  % (3319516)------------------------------
% 4.11/2.31  % (3319516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319516)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319516)Termination reason: Instruction limit
% 4.11/2.31  % (3319516)Termination phase: Saturation
% 4.11/2.31  % (3319516)Time elapsed: 0.067 s
% 4.11/2.31  % (3319516)Peak memory usage: 87 MB
% 4.11/2.31  % (3319516)Instructions burned: 138 (million)
% 4.11/2.31  % (3319517)Instruction limit reached! 
% 4.11/2.31  % (3319517)------------------------------
% 4.11/2.31  % (3319517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319517)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319517)Termination reason: Instruction limit
% 4.11/2.31  % (3319517)Termination phase: Saturation
% 4.11/2.31  % (3319517)Time elapsed: 0.103 s
% 4.11/2.31  % (3319517)Peak memory usage: 89 MB
% 4.11/2.31  % (3319517)Instructions burned: 183 (million)
% 4.11/2.31  % (3319518)Instruction limit reached! 
% 4.11/2.31  % (3319518)------------------------------
% 4.11/2.31  % (3319518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319518)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319518)Termination reason: Instruction limit
% 4.11/2.31  % (3319518)Termination phase: Saturation
% 4.11/2.31  % (3319518)Time elapsed: 0.146 s
% 4.11/2.31  % (3319518)Peak memory usage: 91 MB
% 4.11/2.31  % (3319518)Instructions burned: 258 (million)
% 4.11/2.31  % (3319519)Refutation not found, incomplete strategy
% 4.11/2.31  % (3319519)------------------------------
% 4.11/2.31  % (3319519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319519)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319519)Termination reason: Refutation not found, incomplete strategy
% 4.11/2.31  % (3319519)Time elapsed: 0.186 s
% 4.11/2.31  % (3319519)Peak memory usage: 91 MB
% 4.11/2.31  % (3319519)Instructions burned: 321 (million)
% 4.11/2.31  % (3319527)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1869587656:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 4.11/2.31  % (3319528)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3793344530:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 4.11/2.31  % (3319529)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=32158576:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 4.11/2.31  % (3319529)Instruction limit reached! 
% 4.11/2.31  % (3319529)------------------------------
% 4.11/2.31  % (3319529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319529)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319529)Termination reason: Instruction limit
% 4.11/2.31  % (3319529)Termination phase: Saturation
% 4.11/2.31  % (3319529)Time elapsed: 0.110 s
% 4.11/2.31  % (3319529)Peak memory usage: 93 MB
% 4.11/2.31  % (3319529)Instructions burned: 217 (million)
% 4.11/2.31  % (3319519)------------------------------
% 4.11/2.31  % (3319519)------------------------------
% 4.11/2.31  % (3319533)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=1784061668: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  % (3319534)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=1964664316:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 4.11/2.31  % (3319533)Instruction limit reached! 
% 4.11/2.31  % (3319533)------------------------------
% 4.11/2.31  % (3319533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319533)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319533)Termination reason: Instruction limit
% 4.11/2.31  % (3319533)Termination phase: Saturation
% 4.11/2.31  % (3319533)Time elapsed: 0.167 s
% 4.11/2.31  % (3319533)Peak memory usage: 95 MB
% 4.11/2.31  % (3319533)Instructions burned: 318 (million)
% 4.11/2.31  % (3319513)Refutation not found, incomplete strategy
% 4.11/2.31  % (3319513)------------------------------
% 4.11/2.31  % (3319513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.11/2.31  % (3319513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.11/2.31  % (3319513)CaDiCaL version: 2.1.3
% 4.11/2.31  % (3319513)Termination reason: Refutation not found, incomplete strategy
% 4.11/2.31  % (3319513)Time elapsed: 0.813 s
% 4.11/2.31  % (3319513)Peak memory usage: 140 MB
% 4.11/2.31  % (3319513)Instructions burned: 2149 (million)
% 4.11/2.31  % (3319537)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3276470158:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 4.11/2.31  % (3319513)------------------------------
% 4.11/2.31  % (3319513)------------------------------
% 4.11/2.31  % (3319539)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=141032466:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 4.11/2.31  % (3319537)First to succeed.
% 4.11/2.31  % (3319537)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3319508"
% 4.11/2.31  % (3319514)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.18/2.40  % SZS output start Definitions and Model Updates.
% 0.18/2.40  % SZS output end Definitions and Model Updates.
% 0.18/2.40  % (3319537)------------------------------
% 0.18/2.40  % (3319537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/2.40  % (3319537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/2.40  % (3319537)CaDiCaL version: 2.1.3
% 0.18/2.40  % (3319537)Termination reason: Satisfiable
% 0.18/2.40  % (3319537)Time elapsed: 0.220 s
% 0.18/2.40  % (3319537)Peak memory usage: 93 MB
% 0.18/2.40  % (3319537)Instructions burned: 357 (million)
% 0.18/2.40  % (3319537)------------------------------
% 0.18/2.40  % (3319537)------------------------------
% 0.18/2.40  % (3319508)Success in time 1.44 s
% 0.18/2.40  % Vampire exiting
%------------------------------------------------------------------------------