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

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

% Computer : n001.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:29 PM UTC 2026

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

% Comments : 
%------------------------------------------------------------------------------
cnf(u1021,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc10),true) ).

cnf(u778,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc10),true,true,true),true) ).

cnf(u2206,negated_conjecture,
    true = mia_forename(skc10,skc11) ).

cnf(u524,negated_conjecture,
    true = ifeq3(vincent_forename(skc8,skc11),true,true,true) ).

cnf(u1019,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc11),true) ).

cnf(u1294,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,nonexistent(X0,skc9),true) ).

cnf(u784,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc9),true) ).

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

cnf(u1786,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(abstraction(X0,skc11),true,true,true),true) ).

cnf(u2323,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,human_person(X0,skc15),true) ).

cnf(u1566,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,desire_want(X0,skc9),true) ).

cnf(u805,negated_conjecture,
    true = thing(skc10,skc11) ).

cnf(u32,axiom,
    true = ifeq3(abstraction(X0,X1),true,unisex(X0,X1),true) ).

cnf(u535,negated_conjecture,
    true = ifeq3(woman(skc8,skc15),true,true,true) ).

cnf(u1681,negated_conjecture,
    true = ifeq3(relname(skc10,skc11),true,true,true) ).

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

cnf(u678,negated_conjecture,
    b = ifeq2(tuple2(true,existent(skc10,skc9)),tuple2(true,true),a,b) ).

cnf(u2613,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,impartial(X0,skc12),true) ).

cnf(u3096,negated_conjecture,
    true = ifeq3(of(X0,skc14,skc15),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u1695,negated_conjecture,
    true = nonhuman(skc10,skc14) ).

cnf(u2345,negated_conjecture,
    true = organism(skc10,skc15) ).

cnf(u404,negated_conjecture,
    true = ifeq3(proposition(skc8,skc11),true,true,true) ).

cnf(u38,axiom,
    true = ifeq3(mia_forename(X0,X1),true,forename(X0,X1),true) ).

cnf(u2344,negated_conjecture,
    true = human(skc10,skc15) ).

cnf(u3201,negated_conjecture,
    ifeq4(of(skc10,X0,skc15),true,ifeq4(of(skc10,X1,skc15),true,ifeq4(forename(skc10,X0),true,ifeq4(forename(skc10,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u1593,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,proposition(X0,skc10),true) ).

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

cnf(u316,negated_conjecture,
    true = ifeq3(desire_want(skc10,skc13),true,true,true) ).

cnf(u1715,negated_conjecture,
    b = ifeq2(tuple2(specific(skc10,skc11),true),tuple2(true,true),a,b) ).

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

cnf(u3514,negated_conjecture,
    skc11 = ifeq4(of(skc10,X0,skc15),true,ifeq4(of(skc10,skc11,skc15),true,ifeq4(forename(skc10,X0),true,X0,skc11),skc11),skc11) ).

cnf(u1338,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc13),true,true,true),true) ).

cnf(u3001,negated_conjecture,
    true = ifeq3(agent(X0,skc9,skc12),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).

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

cnf(u3244,negated_conjecture,
    ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X0),true,skc14,X0),X0) = X0 ).

cnf(u3379,negated_conjecture,
    skc11 = ifeq4(of(skc8,skc11,X0),true,ifeq4(of(skc8,skc11,X0),true,ifeq4(entity(skc8,X0),true,skc11,skc11),skc11),skc11) ).

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

cnf(u2887,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,vincent_forename(X0,skc14),true) ).

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

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

cnf(u822,negated_conjecture,
    true = ifeq3(entity(skc10,skc14),true,true,true) ).

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

cnf(u3248,negated_conjecture,
    skc11 = ifeq4(of(skc8,skc14,skc12),true,skc14,skc11) ).

cnf(u1186,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc9),true,true,true),true) ).

cnf(u2368,negated_conjecture,
    true = existent(skc10,skc15) ).

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

cnf(u434,negated_conjecture,
    true = ifeq3(eventuality(skc8,skc11),true,true,true) ).

cnf(u78,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(specific(X0,X2),true,specific(X1,X2),true),true) ).

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

cnf(u584,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc8,skc9)),tuple2(true,true),a,b) ).

cnf(u1879,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonhuman(X0,skc11),true,true,true),true) ).

cnf(u3002,negated_conjecture,
    true = ifeq3(agent(X0,skc13,skc12),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(u833,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc11),true,true,true) ).

cnf(u76,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(singleton(X0,X2),true,singleton(X1,X2),true),true) ).

cnf(u2426,negated_conjecture,
    true = ifeq3(organism(skc8,X0),true,organism(skc10,X0),true) ).

cnf(u1349,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc13),true) ).

cnf(u847,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc12),true) ).

cnf(u2263,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc10,skc12)),tuple2(true,true),a,b) ).

cnf(u2201,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(mia_forename(X0,skc11),true,true,true),true) ).

cnf(u66,axiom,
    true = ifeq3(man(X0,X1),true,male(X0,X1),true) ).

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

cnf(u1376,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc10,skc14)),tuple2(true,true),a,b) ).

cnf(u385,negated_conjecture,
    true = unisex(skc8,skc10) ).

cnf(u1477,negated_conjecture,
    true = ifeq3(present(X0,skc13),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(u1878,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonhuman(X0,skc10),true,true,true),true) ).

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

cnf(u2937,negated_conjecture,
    true = male(skc10,skc15) ).

cnf(u474,negated_conjecture,
    true = entity(skc8,skc12) ).

cnf(u116,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(living(X0,X2),true,living(X1,X2),true),true) ).

cnf(u1481,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,present(X0,skc13),true) ).

cnf(u1884,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,nonhuman(X0,skc11),true) ).

cnf(u603,negated_conjecture,
    b = ifeq2(tuple2(nonhuman(skc8,skc12),true),tuple2(true,true),a,b) ).

cnf(u1389,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc11),true) ).

cnf(u1882,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonhuman(X0,skc14),true,true,true),true) ).

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

cnf(u1888,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,nonhuman(X0,skc11),true) ).

cnf(u2671,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(living(X0,skc15),true,true,true),true) ).

cnf(u106,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(human_person(X0,X2),true,human_person(X1,X2),true),true) ).

cnf(u731,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,eventuality(X0,skc13),true) ).

cnf(u1015,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc9),true,true,true),true) ).

cnf(u2059,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,forename(X0,skc11),true) ).

cnf(u730,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,eventuality(X0,skc9),true) ).

cnf(u3845,negated_conjecture,
    ifeq4(theme(skc8,skc9,X0),true,ifeq4(proposition(skc8,X0),true,skc10,X0),X0) = X0 ).

cnf(u2925,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,man(X0,skc15),true) ).

cnf(u2732,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human(X0,skc12),true,true,true),true) ).

cnf(u104,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(woman(X0,X2),true,woman(X1,X2),true),true) ).

cnf(u2799,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,animate(X0,skc12),true) ).

cnf(u2418,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(organism(X0,skc12),true,true,true),true) ).

cnf(u1592,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(proposition(X0,skc10),true,true,true),true) ).

cnf(u2145,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,relname(X0,skc14),true) ).

cnf(u2924,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(man(X0,skc15),true,true,true),true) ).

cnf(u3317,negated_conjecture,
    skc14 = ifeq4(of(skc8,skc11,X0),true,ifeq4(of(skc8,skc14,X0),true,ifeq4(entity(skc8,X0),true,skc11,skc14),skc14),skc14) ).

cnf(u1783,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(abstraction(X0,skc14),true,true,true),true) ).

cnf(u2929,negated_conjecture,
    true = man(skc10,skc15) ).

cnf(u645,negated_conjecture,
    true = ifeq3(desire_want(skc10,skc9),true,true,true) ).

cnf(u1005,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc10),true,true,true),true) ).

cnf(u1788,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,abstraction(X0,skc14),true) ).

cnf(u2546,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(existent(X0,skc12),true,true,true),true) ).

cnf(u643,negated_conjecture,
    true = ifeq3(dance(skc10,skc9),true,true,true) ).

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

cnf(u1789,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,abstraction(X0,skc10),true) ).

cnf(clause72,axiom,
    ifeq4(of(X0,X1,X2),true,ifeq4(of(X0,X3,X2),true,ifeq4(entity(X0,X2),true,ifeq4(forename(X0,X1),true,ifeq4(forename(X0,X3),true,X1,X3),X3),X3),X3),X3) = X3 ).

cnf(u495,negated_conjecture,
    true = specific(skc8,skc12) ).

cnf(u633,negated_conjecture,
    true = ifeq3(event(skc8,X0),true,event(skc10,X0),true) ).

cnf(u1787,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,abstraction(X0,skc11),true) ).

cnf(u789,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc9),true) ).

cnf(u16,axiom,
    true = ifeq3(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).

cnf(u2063,negated_conjecture,
    true = forename(skc10,skc14) ).

cnf(u1556,negated_conjecture,
    true = ifeq3(desire_want(skc8,X0),true,desire_want(skc10,X0),true) ).

cnf(u787,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc10),true) ).

cnf(u1679,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relation(X0,skc11),true,true,true),true) ).

cnf(u1554,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(desire_want(X0,skc9),true,true,true),true) ).

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

cnf(u1025,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc11),true) ).

cnf(u3204,negated_conjecture,
    ifeq4(of(skc8,X0,skc12),true,ifeq4(of(skc8,X1,skc12),true,ifeq4(forename(skc8,X0),true,ifeq4(forename(skc8,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u22,axiom,
    true = ifeq3(proposition(X0,X1),true,relation(X0,X1),true) ).

cnf(u144,negated_conjecture,
    true = woman(skc8,skc12) ).

cnf(u2857,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,female(X0,skc12),true) ).

cnf(u647,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(event(X0,skc9),true,true,true),true) ).

cnf(u3100,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,of(X0,skc14,skc15),true) ).

cnf(u808,negated_conjecture,
    true = thing(skc10,skc15) ).

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

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

cnf(u3115,negated_conjecture,
    true = of(skc10,skc14,skc15) ).

cnf(u150,negated_conjecture,
    true = forename(skc8,skc11) ).

cnf(u3239,negated_conjecture,
    skc11 = ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X0),true,X0,skc11),skc11) ).

cnf(u1371,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc10),true) ).

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

cnf(u3984,negated_conjecture,
    skc10 = ifeq4(theme(skc8,X0,skc10),true,ifeq4(theme(skc8,X1,skc10),true,ifeq4(desire_want(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,skc10,skc10),skc10),skc10),skc10) ).

cnf(u2202,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,mia_forename(X0,skc11),true) ).

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

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

cnf(u3243,negated_conjecture,
    ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X0),true,skc11,X0),X0) = X0 ).

cnf(u62,axiom,
    true = ifeq3(vincent_forename(X0,X1),true,forename(X0,X1),true) ).

cnf(u148,negated_conjecture,
    true = dance(skc10,skc13) ).

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

cnf(u1189,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(specific(X0,skc15),true,true,true),true) ).

cnf(u2088,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,forename(X0,skc11),true) ).

cnf(u727,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(eventuality(X0,skc9),true,true,true),true) ).

cnf(u812,negated_conjecture,
    true = ifeq3(entity(skc10,skc10),true,true,true) ).

cnf(u2358,negated_conjecture,
    true = impartial(skc10,skc15) ).

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

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

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

cnf(u2968,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(male(X0,skc15),true,true,true),true) ).

cnf(u2858,negated_conjecture,
    true = ifeq3(female(skc8,X0),true,female(skc10,X0),true) ).

cnf(u1193,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc9),true) ).

cnf(u60,axiom,
    true = ifeq3(woman(X0,X1),true,female(X0,X1),true) ).

cnf(u1971,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(general(X0,skc14),true,true,true),true) ).

cnf(u4030,negated_conjecture,
    ifeq4(theme(skc10,skc9,X0),true,ifeq4(theme(skc10,skc9,X1),true,ifeq4(proposition(skc10,X0),true,ifeq4(proposition(skc10,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u2241,negated_conjecture,
    true = ifeq3(woman(skc8,X0),true,woman(skc10,X0),true) ).

cnf(u2971,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,male(X0,skc15),true) ).

cnf(u318,negated_conjecture,
    b = ifeq(tuple(dance(skc8,skc9),true,desire_want(skc8,X0),proposition(skc8,skc8),accessible_world(skc8,skc8),true,present(skc8,X0),agent(skc8,skc9,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc8)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u690,negated_conjecture,
    true = ifeq3(accessible_world(skc8,skc8),true,true,true) ).

cnf(u1977,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,general(X0,skc10),true) ).

cnf(u2486,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,entity(X0,skc15),true) ).

cnf(u1199,negated_conjecture,
    true = ifeq3(specific(skc8,skc13),true,true,true) ).

cnf(u50,axiom,
    true = ifeq3(entity(X0,X1),true,existent(X0,X1),true) ).

cnf(u188,negated_conjecture,
    b = ifeq(tuple(dance(X0,X1),event(X0,X1),desire_want(skc8,X2),proposition(skc8,X0),accessible_world(skc8,X0),present(X0,X1),present(skc8,X2),agent(X0,X1,skc15),agent(skc8,X2,skc15),theme(skc8,X2,X0)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u605,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc8,skc12)),tuple2(true,true),a,b) ).

cnf(u1210,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc10,skc15)),tuple2(true,true),a,b) ).

cnf(u1204,negated_conjecture,
    true = specific(skc10,skc15) ).

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

cnf(u178,axiom,
    b = ifeq2(tuple2(unisex(X0,X1),female(X0,X1)),tuple2(true,true),a,b) ).

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

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

cnf(u1208,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc15),true,true,true),true) ).

cnf(u1973,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(general(X0,skc14),true,true,true),true) ).

cnf(u1218,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc10,skc12)),tuple2(true,true),a,b) ).

cnf(u1484,negated_conjecture,
    true = present(skc10,skc9) ).

cnf(u2424,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,organism(X0,skc15),true) ).

cnf(u589,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc8,skc11)),tuple2(true,true),a,b) ).

cnf(u2240,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,woman(X0,skc12),true) ).

cnf(u4116,negated_conjecture,
    skc10 = ifeq4(theme(skc10,X0,skc10),true,ifeq4(theme(skc10,X1,skc10),true,ifeq4(desire_want(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,skc10,skc10),skc10),skc10),skc10) ).

cnf(u857,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc15),true) ).

cnf(u100,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(relname(X0,X2),true,relname(X1,X2),true),true) ).

cnf(u587,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc10,skc13)),tuple2(true,true),a,b) ).

cnf(u2141,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relname(X0,skc11),true,true,true),true) ).

cnf(u174,negated_conjecture,
    true = theme(skc8,skc9,skc10) ).

cnf(u2246,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(woman(X0,skc12),true,true,true),true) ).

cnf(u90,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(relation(X0,X2),true,relation(X1,X2),true),true) ).

cnf(u1377,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc10,skc14)),tuple2(true,true),a,b) ).

cnf(u1609,negated_conjecture,
    true = abstraction(skc10,skc10) ).

cnf(u1363,negated_conjecture,
    true = unisex(skc10,skc10) ).

cnf(u606,negated_conjecture,
    b = ifeq2(tuple2(female(skc8,skc15),true),tuple2(true,true),a,b) ).

cnf(u3800,negated_conjecture,
    ifeq4(theme(skc8,X0,skc10),true,ifeq4(theme(skc8,X1,X2),true,ifeq4(proposition(skc8,X2),true,ifeq4(desire_want(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,skc10,X2),X2),X2),X2),X2) = X2 ).

cnf(u1623,negated_conjecture,
    b = ifeq2(tuple2(specific(skc10,skc10),true),tuple2(true,true),a,b) ).

cnf(u728,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(eventuality(X0,skc9),true,true,true),true) ).

cnf(u629,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(event(X0,skc13),true,true,true),true) ).

cnf(u462,negated_conjecture,
    true = ifeq3(mia_forename(skc8,skc14),true,true,true) ).

cnf(u88,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(proposition(X0,X2),true,proposition(X1,X2),true),true) ).

cnf(u1383,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc11),true,true,true),true) ).

cnf(u2260,negated_conjecture,
    true = organism(skc10,skc12) ).

cnf(u734,negated_conjecture,
    true = ifeq3(eventuality(skc8,skc13),true,true,true) ).

cnf(u2674,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,living(X0,skc15),true) ).

cnf(u1028,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc10),true) ).

cnf(u2275,negated_conjecture,
    b = ifeq2(tuple2(nonhuman(skc10,skc12),true),tuple2(true,true),a,b) ).

cnf(u3197,negated_conjecture,
    ifeq4(of(skc10,skc11,X0),true,ifeq4(of(skc10,X1,X0),true,ifeq4(entity(skc10,X0),true,ifeq4(forename(skc10,X1),true,skc11,X1),X1),X1),X1) = X1 ).

cnf(u216,negated_conjecture,
    b = ifeq(tuple(true,true,desire_want(skc8,X0),true,true,true,present(skc8,X0),agent(skc10,skc13,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc10)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u3305,negated_conjecture,
    skc14 = ifeq4(of(skc10,skc14,skc12),true,skc11,skc14) ).

cnf(u2802,negated_conjecture,
    true = ifeq3(animate(skc8,X0),true,animate(skc10,X0),true) ).

cnf(u479,negated_conjecture,
    true = ifeq3(entity(skc8,skc10),true,true,true) ).

cnf(u617,negated_conjecture,
    true = ifeq3(dance(skc8,skc13),true,true,true) ).

cnf(u2419,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(organism(X0,skc15),true,true,true),true) ).

cnf(u2057,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(forename(X0,skc14),true,true,true),true) ).

cnf(u1295,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,nonexistent(X0,skc9),true) ).

cnf(u3055,negated_conjecture,
    true = ifeq3(theme(skc8,X0,X1),true,theme(skc10,X0,X1),true) ).

cnf(u1008,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc11),true,true,true),true) ).

cnf(u1791,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,abstraction(X0,skc11),true) ).

cnf(u2554,negated_conjecture,
    true = ifeq3(existent(skc8,X0),true,existent(skc10,X0),true) ).

cnf(u6,axiom,
    true = ifeq3(dance(X0,X1),true,event(X0,X1),true) ).

cnf(u1555,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,desire_want(X0,skc9),true) ).

cnf(u500,negated_conjecture,
    true = existent(skc8,skc12) ).

cnf(u2547,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(existent(X0,skc15),true,true,true),true) ).

cnf(u1790,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,abstraction(X0,skc14),true) ).

cnf(u128,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(male(X0,X2),true,male(X1,X2),true),true) ).

cnf(u786,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc12),true) ).

cnf(u2084,negated_conjecture,
    true = ifeq3(vincent_forename(skc10,skc11),true,true,true) ).

cnf(u1793,negated_conjecture,
    true = ifeq3(abstraction(skc8,X0),true,abstraction(skc10,X0),true) ).

cnf(u3203,negated_conjecture,
    ifeq4(of(skc8,X0,skc15),true,ifeq4(of(skc8,X1,skc15),true,ifeq4(forename(skc8,X0),true,ifeq4(forename(skc8,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u2796,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(animate(X0,skc12),true,true,true),true) ).

cnf(u2855,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(female(X0,skc12),true,true,true),true) ).

cnf(u512,negated_conjecture,
    true = human(skc8,skc12) ).

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

cnf(u2058,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,forename(X0,skc14),true) ).

cnf(u529,negated_conjecture,
    true = ifeq3(man(skc8,skc12),true,true,true) ).

cnf(u1683,negated_conjecture,
    true = ifeq3(proposition(skc10,skc11),true,true,true) ).

cnf(u2213,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,mia_forename(X0,skc11),true) ).

cnf(u3319,negated_conjecture,
    skc14 = ifeq4(of(skc8,X0,skc12),true,ifeq4(of(skc8,skc14,skc12),true,ifeq4(forename(skc8,X0),true,X0,skc14),skc14),skc14) ).

cnf(u134,axiom,
    true = ifeq3(of(X0,X1,X2),true,ifeq3(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).

cnf(u1672,negated_conjecture,
    true = ifeq3(relname(skc10,skc14),true,true,true) ).

cnf(u2969,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(male(X0,skc15),true,true,true),true) ).

cnf(u1026,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc12),true) ).

cnf(u726,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(eventuality(X0,skc13),true,true,true),true) ).

cnf(u46,axiom,
    true = ifeq3(entity(X0,X1),true,thing(X0,X1),true) ).

cnf(u132,axiom,
    true = ifeq3(theme(X0,X1,X2),true,ifeq3(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).

cnf(u2341,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human_person(X0,skc15),true,true,true),true) ).

cnf(u790,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc13),true) ).

cnf(u3613,negated_conjecture,
    skc14 = ifeq4(of(skc10,skc14,skc12),true,ifeq4(of(skc10,skc14,skc12),true,skc14,skc14),skc14) ).

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

cnf(u2611,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(impartial(X0,skc15),true,true,true),true) ).

cnf(u2342,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,human_person(X0,skc15),true) ).

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

cnf(u2422,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,organism(X0,skc15),true) ).

cnf(u44,axiom,
    true = ifeq3(organism(X0,X1),true,entity(X0,X1),true) ).

cnf(u2614,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,impartial(X0,skc15),true) ).

cnf(u815,negated_conjecture,
    true = ifeq3(eventuality(skc10,skc10),true,true,true) ).

cnf(u674,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc10,skc9)),tuple2(true,true),a,b) ).

cnf(u1340,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc10),true,true,true),true) ).

cnf(u2739,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,human(X0,skc12),true) ).

cnf(u1190,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,specific(X0,skc15),true) ).

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

cnf(u1975,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,general(X0,skc11),true) ).

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

cnf(u34,axiom,
    true = ifeq3(forename(X0,X1),true,relname(X0,X1),true) ).

cnf(u172,negated_conjecture,
    true = agent(skc10,skc13,skc12) ).

cnf(u830,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc11),true,true,true),true) ).

cnf(u1213,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc15),true) ).

cnf(u2615,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,impartial(X0,skc12),true) ).

cnf(u3378,negated_conjecture,
    skc11 = ifeq4(of(skc8,skc14,X0),true,ifeq4(of(skc8,skc11,X0),true,ifeq4(entity(skc8,X0),true,skc14,skc11),skc11),skc11) ).

cnf(u2481,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(entity(X0,skc15),true,true,true),true) ).

cnf(u1684,negated_conjecture,
    true = abstraction(skc10,skc11) ).

cnf(u1188,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(specific(X0,skc12),true,true,true),true) ).

cnf(u419,negated_conjecture,
    true = nonhuman(skc8,skc11) ).

cnf(u312,negated_conjecture,
    true = unisex(skc10,skc13) ).

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

cnf(u2484,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,entity(X0,skc15),true) ).

cnf(u1344,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc14),true) ).

cnf(u2608,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(impartial(X0,skc12),true,true,true),true) ).

cnf(u836,negated_conjecture,
    true = singleton(skc10,skc11) ).

cnf(u1974,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(general(X0,skc11),true,true,true),true) ).

cnf(u84,axiom,
    true = ifeq3(present(X0,X1),true,ifeq3(accessible_world(X0,X2),true,present(X2,X1),true),true) ).

cnf(u1980,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,general(X0,skc10),true) ).

cnf(u3013,negated_conjecture,
    true = agent(skc10,skc9,skc12) ).

cnf(u855,negated_conjecture,
    true = ifeq3(eventuality(skc10,skc15),true,true,true) ).

cnf(u2898,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,vincent_forename(X0,skc14),true) ).

cnf(u2736,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,human(X0,skc15),true) ).

cnf(u1978,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,general(X0,skc14),true) ).

cnf(u3797,negated_conjecture,
    skc10 = ifeq4(theme(skc10,X0,X1),true,ifeq4(theme(skc10,X2,skc10),true,ifeq4(proposition(skc10,X1),true,ifeq4(desire_want(skc10,X0),true,ifeq4(desire_want(skc10,X2),true,X1,skc10),skc10),skc10),skc10),skc10) ).

cnf(u446,negated_conjecture,
    true = ifeq3(eventuality(skc8,skc14),true,true,true) ).

cnf(u2373,negated_conjecture,
    b = ifeq2(tuple2(nonexistent(skc10,skc15),true),tuple2(true,true),a,b) ).

cnf(u3534,negated_conjecture,
    skc11 = ifeq4(of(skc10,skc11,skc15),true,ifeq4(of(skc10,skc11,skc15),true,skc11,skc11),skc11) ).

cnf(u74,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(thing(X0,X2),true,thing(X1,X2),true),true) ).

cnf(u1347,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc10),true) ).

cnf(u590,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc8,skc9)),tuple2(true,true),a,b) ).

cnf(u3796,negated_conjecture,
    ifeq4(theme(skc8,skc9,X0),true,ifeq4(theme(skc8,X1,X2),true,ifeq4(proposition(skc8,X0),true,ifeq4(proposition(skc8,X2),true,ifeq4(desire_want(skc8,X1),true,X0,X2),X2),X2),X2),X2) = X2 ).

cnf(u596,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc8,skc15)),tuple2(true,true),a,b) ).

cnf(u1886,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,nonhuman(X0,skc10),true) ).

cnf(u613,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(dance(X0,skc13),true,true,true),true) ).

cnf(u2886,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(vincent_forename(X0,skc14),true,true,true),true) ).

cnf(u845,negated_conjecture,
    true = ifeq3(eventuality(skc10,skc12),true,true,true) ).

cnf(u72,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).

cnf(u1367,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc10,skc10)),tuple2(true,true),a,b) ).

cnf(u202,negated_conjecture,
    b = ifeq(tuple(dance(skc10,X0),event(skc10,X0),desire_want(skc8,X1),true,true,present(skc10,X0),present(skc8,X1),agent(skc10,X0,skc15),agent(skc8,X1,skc15),theme(skc8,X1,skc10)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u3794,negated_conjecture,
    ifeq4(theme(skc8,X0,X1),true,ifeq4(theme(skc8,skc9,X2),true,ifeq4(proposition(skc8,X1),true,ifeq4(proposition(skc8,X2),true,ifeq4(desire_want(skc8,X0),true,X1,X2),X2),X2),X2),X2) = X2 ).

cnf(u2244,negated_conjecture,
    true = woman(skc10,skc12) ).

cnf(u843,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc12),true,true,true) ).

cnf(u3416,negated_conjecture,
    skc11 = ifeq4(of(skc8,skc11,skc15),true,ifeq4(of(skc8,skc11,skc15),true,skc11,skc11),skc11) ).

cnf(u1890,negated_conjecture,
    true = ifeq3(nonhuman(skc8,X0),true,nonhuman(skc10,X0),true) ).

cnf(u3015,negated_conjecture,
    true = ifeq3(agent(X0,skc9,skc12),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(u2140,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relname(X0,skc14),true,true,true),true) ).

cnf(u852,negated_conjecture,
    true = ifeq3(entity(skc10,skc15),true,true,true) ).

cnf(u200,negated_conjecture,
    b = ifeq(tuple(dance(X0,X1),event(X0,X1),true,proposition(skc8,X0),accessible_world(skc8,X0),present(X0,X1),true,agent(X0,X1,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,X0)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u3289,negated_conjecture,
    skc11 = ifeq4(of(skc10,skc14,skc12),true,skc14,skc11) ).

cnf(u630,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(event(X0,skc9),true,true,true),true) ).

cnf(u1374,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc14),true,true,true),true) ).

cnf(u369,negated_conjecture,
    true = ifeq3(eventuality(skc8,skc10),true,true,true) ).

cnf(u636,negated_conjecture,
    true = ifeq3(event(skc8,skc13),true,true,true) ).

cnf(u601,negated_conjecture,
    b = ifeq2(tuple2(true,human(skc8,skc11)),tuple2(true,true),a,b) ).

cnf(u356,negated_conjecture,
    true = relation(skc8,skc10) ).

cnf(u112,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(existent(X0,X2),true,existent(X1,X2),true),true) ).

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

cnf(u615,negated_conjecture,
    true = ifeq3(dance(skc8,X0),true,dance(skc10,X0),true) ).

cnf(u2146,negated_conjecture,
    true = ifeq3(relname(skc8,X0),true,relname(skc10,X0),true) ).

cnf(u1652,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relation(X0,skc14),true,true,true),true) ).

cnf(u375,negated_conjecture,
    true = nonhuman(skc8,skc10) ).

cnf(u1650,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relation(X0,skc10),true,true,true),true) ).

cnf(u729,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,eventuality(X0,skc9),true) ).

cnf(u118,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(human(X0,X2),true,human(X1,X2),true),true) ).

cnf(u1013,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc12),true,true,true),true) ).

cnf(u1656,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,relation(X0,skc11),true) ).

cnf(u2068,negated_conjecture,
    true = ifeq3(mia_forename(skc10,skc14),true,true,true) ).

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

cnf(u3196,negated_conjecture,
    skc11 = ifeq4(of(skc8,X0,X1),true,ifeq4(of(skc8,skc11,X1),true,ifeq4(entity(skc8,X1),true,ifeq4(forename(skc8,X0),true,X0,skc11),skc11),skc11),skc11) ).

cnf(u1011,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc15),true,true,true),true) ).

cnf(u2970,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,male(X0,skc15),true) ).

cnf(u776,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc9),true,true,true),true) ).

cnf(u2797,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(animate(X0,skc15),true,true,true),true) ).

cnf(u1667,negated_conjecture,
    true = relation(skc10,skc11) ).

cnf(u2795,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(animate(X0,skc15),true,true,true),true) ).

cnf(u1029,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc15),true) ).

cnf(u2552,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,existent(X0,skc15),true) ).

cnf(u2065,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(forename(X0,skc14),true,true,true),true) ).

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

cnf(u3193,negated_conjecture,
    skc11 = ifeq4(of(skc10,X0,X1),true,ifeq4(of(skc10,skc11,X1),true,ifeq4(entity(skc10,X1),true,ifeq4(forename(skc10,X0),true,X0,skc11),skc11),skc11),skc11) ).

cnf(u2056,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(forename(X0,skc11),true,true,true),true) ).

cnf(u2320,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human_person(X0,skc15),true,true,true),true) ).

cnf(u2941,negated_conjecture,
    b = ifeq2(tuple2(unisex(skc10,skc15),true),tuple2(true,true),a,b) ).

cnf(u641,negated_conjecture,
    b = ifeq(tuple(dance(skc10,skc9),true,desire_want(skc8,X0),true,true,present(skc10,skc9),present(skc8,X0),agent(skc10,skc9,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc10)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u30,axiom,
    true = ifeq3(abstraction(X0,X1),true,general(X0,X1),true) ).

cnf(u3199,negated_conjecture,
    ifeq4(of(skc8,skc14,X0),true,ifeq4(of(skc8,X1,X0),true,ifeq4(entity(skc8,X0),true,ifeq4(forename(skc8,X1),true,skc14,X1),X1),X1),X1) = X1 ).

cnf(u3200,negated_conjecture,
    ifeq4(of(skc8,skc11,X0),true,ifeq4(of(skc8,X1,X0),true,ifeq4(entity(skc8,X0),true,ifeq4(forename(skc8,X1),true,skc11,X1),X1),X1),X1) = X1 ).

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

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

cnf(u780,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc11),true,true,true),true) ).

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

cnf(u2087,negated_conjecture,
    true = relname(skc10,skc11) ).

cnf(u1039,negated_conjecture,
    true = ifeq3(singleton(skc8,skc13),true,true,true) ).

cnf(u785,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc11),true) ).

cnf(u28,axiom,
    true = ifeq3(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).

cnf(u158,negated_conjecture,
    true = desire_want(skc8,skc9) ).

cnf(u2085,negated_conjecture,
    true = ifeq3(mia_forename(skc10,skc11),true,true,true) ).

cnf(u2080,negated_conjecture,
    true = forename(skc10,skc11) ).

cnf(u18,axiom,
    true = ifeq3(eventuality(X0,X1),true,unisex(X0,X1),true) ).

cnf(u156,negated_conjecture,
    true = accessible_world(skc8,skc10) ).

cnf(u820,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc14),true,true,true),true) ).

cnf(u1685,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,relation(X0,skc11),true) ).

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

cnf(u296,negated_conjecture,
    true = thing(skc10,skc13) ).

cnf(u2359,negated_conjecture,
    true = living(skc10,skc15) ).

cnf(u825,negated_conjecture,
    true = ifeq3(eventuality(skc10,skc14),true,true,true) ).

cnf(u146,negated_conjecture,
    true = present(skc10,skc13) ).

cnf(u1187,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(specific(X0,skc9),true,true,true),true) ).

cnf(u1341,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc11),true,true,true),true) ).

cnf(u1368,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc10,skc10)),tuple2(true,true),a,b) ).

cnf(u2609,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(impartial(X0,skc15),true,true,true),true) ).

cnf(u1666,negated_conjecture,
    true = relation(skc10,skc14) ).

cnf(u668,negated_conjecture,
    true = ifeq3(entity(skc10,skc9),true,true,true) ).

cnf(u2357,negated_conjecture,
    true = entity(skc10,skc15) ).

cnf(u2487,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,entity(X0,skc12),true) ).

cnf(u58,axiom,
    true = ifeq3(human_person(X0,X1),true,animate(X0,X1),true) ).

cnf(u2737,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,human(X0,skc12),true) ).

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

cnf(u2485,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,entity(X0,skc12),true) ).

cnf(u56,axiom,
    true = ifeq3(human_person(X0,X1),true,human(X0,X1),true) ).

cnf(u186,axiom,
    b = ifeq2(tuple2(nonexistent(X0,X1),existent(X0,X1)),tuple2(true,true),a,b) ).

cnf(u1345,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc9),true) ).

cnf(u827,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc14),true) ).

cnf(u1594,negated_conjecture,
    true = ifeq3(proposition(skc8,X0),true,proposition(skc10,X0),true) ).

cnf(u3107,negated_conjecture,
    true = ifeq3(of(X0,skc11,skc12),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(u597,negated_conjecture,
    b = ifeq2(tuple2(specific(skc8,skc10),true),tuple2(true,true),a,b) ).

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

cnf(u184,axiom,
    b = ifeq2(tuple2(female(X0,X1),male(X0,X1)),tuple2(true,true),a,b) ).

cnf(u1291,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonexistent(X0,skc13),true,true,true),true) ).

cnf(u595,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc8,skc12)),tuple2(true,true),a,b) ).

cnf(u2142,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,relname(X0,skc11),true) ).

cnf(u3004,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,agent(X0,skc13,skc12),true) ).

cnf(u1216,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc12),true,true,true),true) ).

cnf(u3798,negated_conjecture,
    skc10 = ifeq4(theme(skc8,X0,X1),true,ifeq4(theme(skc8,X2,skc10),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X0),true,ifeq4(desire_want(skc8,X2),true,X1,skc10),skc10),skc10),skc10),skc10) ).

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

cnf(u1880,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonhuman(X0,skc14),true,true,true),true) ).

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

cnf(u1479,negated_conjecture,
    true = ifeq3(present(skc8,X0),true,present(skc10,X0),true) ).

cnf(u842,negated_conjecture,
    true = ifeq3(entity(skc10,skc12),true,true,true) ).

cnf(u3273,negated_conjecture,
    skc11 = ifeq4(of(skc8,skc11,skc15),true,skc14,skc11) ).

cnf(u2139,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relname(X0,skc11),true,true,true),true) ).

cnf(u614,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,dance(X0,skc13),true) ).

cnf(u215,negated_conjecture,
    b = ifeq(tuple(dance(skc10,X0),event(skc10,X0),true,true,true,present(skc10,X0),true,agent(skc10,X0,skc15),agent(skc8,skc9,skc15),true),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u585,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc8,skc14)),tuple2(true,true),a,b) ).

cnf(u2252,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,woman(X0,skc12),true) ).

cnf(u470,negated_conjecture,
    true = organism(skc8,skc12) ).

cnf(u96,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(general(X0,X2),true,general(X1,X2),true),true) ).

cnf(u599,negated_conjecture,
    b = ifeq2(tuple2(specific(skc8,skc14),true),tuple2(true,true),a,b) ).

cnf(u1362,negated_conjecture,
    true = unisex(skc10,skc11) ).

cnf(u2926,negated_conjecture,
    true = ifeq3(man(skc8,X0),true,man(skc10,X0),true) ).

cnf(u1653,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relation(X0,skc10),true,true,true),true) ).

cnf(u1885,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,nonhuman(X0,skc14),true) ).

cnf(u3577,negated_conjecture,
    skc14 = ifeq4(of(skc10,X0,skc12),true,ifeq4(of(skc10,skc14,skc12),true,ifeq4(forename(skc10,X0),true,X0,skc14),skc14),skc14) ).

cnf(u481,negated_conjecture,
    true = ifeq3(entity(skc8,skc9),true,true,true) ).

cnf(u2932,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(man(X0,skc15),true,true,true),true) ).

cnf(u1651,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relation(X0,skc11),true,true,true),true) ).

cnf(u3198,negated_conjecture,
    ifeq4(of(skc10,skc14,X0),true,ifeq4(of(skc10,X1,X0),true,ifeq4(entity(skc10,X0),true,ifeq4(forename(skc10,X1),true,skc14,X1),X1),X1),X1) = X1 ).

cnf(u1883,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonhuman(X0,skc11),true,true,true),true) ).

cnf(u102,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(mia_forename(X0,X2),true,mia_forename(X1,X2),true),true) ).

cnf(u2254,negated_conjecture,
    true = ifeq3(man(skc10,skc12),true,true,true) ).

cnf(u2480,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(entity(X0,skc12),true,true,true),true) ).

cnf(u2143,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,relname(X0,skc14),true) ).

cnf(u602,negated_conjecture,
    b = ifeq2(tuple2(true,human(skc8,skc14)),tuple2(true,true),a,b) ).

cnf(u1889,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,nonhuman(X0,skc10),true) ).

cnf(u3054,negated_conjecture,
    true = ifeq3(theme(X0,skc9,skc10),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u1781,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(abstraction(X0,skc10),true,true,true),true) ).

cnf(u608,negated_conjecture,
    b = ifeq2(tuple2(true,existent(skc8,skc9)),tuple2(true,true),a,b) ).

cnf(u487,negated_conjecture,
    true = ifeq3(eventuality(skc8,skc12),true,true,true) ).

cnf(u3195,negated_conjecture,
    skc14 = ifeq4(of(skc8,X0,X1),true,ifeq4(of(skc8,skc14,X1),true,ifeq4(entity(skc8,X1),true,ifeq4(forename(skc8,X0),true,X0,skc14),skc14),skc14),skc14) ).

cnf(u1784,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(abstraction(X0,skc10),true,true,true),true) ).

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

cnf(u1010,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc14),true,true,true),true) ).

cnf(u3065,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,theme(X0,skc9,skc10),true) ).

cnf(u2071,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,forename(X0,skc14),true) ).

cnf(u1675,negated_conjecture,
    true = abstraction(skc10,skc14) ).

cnf(u3443,negated_conjecture,
    ifeq4(of(skc8,skc14,skc12),true,ifeq4(of(skc8,X0,skc12),true,ifeq4(forename(skc8,X0),true,skc14,X0),X0),X0) = X0 ).

cnf(u485,negated_conjecture,
    true = ifeq3(abstraction(skc8,skc12),true,true,true) ).

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

cnf(u2425,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,organism(X0,skc12),true) ).

cnf(u508,negated_conjecture,
    true = living(skc8,skc12) ).

cnf(u14,axiom,
    true = ifeq3(eventuality(X0,X1),true,specific(X0,X1),true) ).

cnf(u3860,negated_conjecture,
    skc10 = ifeq4(theme(skc10,skc9,X0),true,ifeq4(proposition(skc10,X0),true,X0,skc10),skc10) ).

cnf(u3817,negated_conjecture,
    skc10 = ifeq4(theme(skc10,X0,X1),true,ifeq4(proposition(skc10,X1),true,ifeq4(desire_want(skc10,X0),true,X1,skc10),skc10),skc10) ).

cnf(u1030,negated_conjecture,
    true = ifeq3(singleton(skc8,X0),true,singleton(skc10,X0),true) ).

cnf(u520,negated_conjecture,
    true = female(skc8,skc12) ).

cnf(u399,negated_conjecture,
    true = ifeq3(relname(skc8,skc10),true,true,true) ).

cnf(u3194,negated_conjecture,
    skc14 = ifeq4(of(skc10,X0,X1),true,ifeq4(of(skc10,skc14,X1),true,ifeq4(entity(skc10,X1),true,ifeq4(forename(skc10,X0),true,X0,skc14),skc14),skc14),skc14) ).

cnf(u2938,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,man(X0,skc15),true) ).

cnf(u2553,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,existent(X0,skc12),true) ).

cnf(u12,axiom,
    true = ifeq3(thing(X0,X1),true,singleton(X0,X1),true) ).

cnf(u3339,negated_conjecture,
    skc14 = ifeq4(of(skc8,skc14,skc12),true,ifeq4(of(skc8,skc14,skc12),true,skc14,skc14),skc14) ).

cnf(u142,negated_conjecture,
    true = event(skc10,skc13) ).

cnf(u3820,negated_conjecture,
    ifeq4(theme(skc8,X0,X1),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X0),true,skc10,X1),X1),X1) = X1 ).

cnf(u1014,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc11),true,true,true),true) ).

cnf(u783,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc14),true) ).

cnf(u642,negated_conjecture,
    b = ifeq(tuple(dance(skc10,skc9),true,true,true,true,present(skc10,skc9),true,agent(skc10,skc9,skc15),agent(skc8,skc9,skc15),true),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u2321,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human_person(X0,skc12),true,true,true),true) ).

cnf(u3818,negated_conjecture,
    skc10 = ifeq4(theme(skc8,X0,X1),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X0),true,X1,skc10),skc10),skc10) ).

cnf(u1020,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc12),true) ).

cnf(u3824,negated_conjecture,
    skc10 = ifeq4(theme(skc8,skc9,X0),true,ifeq4(proposition(skc8,X0),true,X0,skc10),skc10) ).

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

cnf(u2324,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,human_person(X0,skc12),true) ).

cnf(u798,negated_conjecture,
    true = ifeq3(thing(skc8,skc13),true,true,true) ).

cnf(u2070,negated_conjecture,
    true = relname(skc10,skc14) ).

cnf(u1192,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,specific(X0,skc9),true) ).

cnf(u2343,negated_conjecture,
    true = animate(skc10,skc15) ).

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

cnf(u52,axiom,
    true = ifeq3(organism(X0,X1),true,impartial(X0,X1),true) ).

cnf(u130,axiom,
    true = ifeq3(agent(X0,X1,X2),true,ifeq3(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).

cnf(u2349,negated_conjecture,
    b = ifeq2(tuple2(nonhuman(skc10,skc15),true),tuple2(true,true),a,b) ).

cnf(u823,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc14),true,true,true) ).

cnf(u3638,negated_conjecture,
    ifeq4(of(skc10,skc11,skc15),true,ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X0),true,skc11,X0),X0),X0) = X0 ).

cnf(u652,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,event(X0,skc9),true) ).

cnf(u669,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc9),true,true,true) ).

cnf(u1191,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,specific(X0,skc12),true) ).

cnf(u42,axiom,
    true = ifeq3(human_person(X0,X1),true,organism(X0,X1),true) ).

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

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

cnf(u3380,negated_conjecture,
    skc11 = ifeq4(of(skc8,X0,skc15),true,ifeq4(of(skc8,skc11,skc15),true,ifeq4(forename(skc8,X0),true,X0,skc11),skc11),skc11) ).

cnf(u2854,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(female(X0,skc12),true,true,true),true) ).

cnf(u813,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc10),true,true,true) ).

cnf(u40,axiom,
    true = ifeq3(woman(X0,X1),true,human_person(X0,X1),true) ).

cnf(u2735,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human(X0,skc15),true,true,true),true) ).

cnf(u170,negated_conjecture,
    true = agent(skc8,skc9,skc12) ).

cnf(u1597,negated_conjecture,
    true = proposition(skc10,skc10) ).

cnf(u3119,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,of(X0,skc14,skc15),true) ).

cnf(u126,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(man(X0,X2),true,man(X1,X2),true),true) ).

cnf(u581,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc10,skc13)),tuple2(true,true),a,b) ).

cnf(u168,negated_conjecture,
    true = of(skc8,skc11,skc12) ).

cnf(u2482,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(entity(X0,skc12),true,true,true),true) ).

cnf(u3257,negated_conjecture,
    skc14 = ifeq4(of(skc8,skc11,skc15),true,skc11,skc14) ).

cnf(u2209,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(mia_forename(X0,skc11),true,true,true),true) ).

cnf(u1342,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc9),true,true,true),true) ).

cnf(u3512,negated_conjecture,
    skc11 = ifeq4(of(skc10,skc11,X0),true,ifeq4(of(skc10,skc11,X0),true,ifeq4(entity(skc10,X0),true,skc11,skc11),skc11),skc11) ).

cnf(u1706,negated_conjecture,
    true = nonhuman(skc10,skc11) ).

cnf(u326,negated_conjecture,
    b = ifeq(tuple(dance(skc8,skc9),true,true,proposition(skc8,skc8),accessible_world(skc8,skc8),true,true,agent(skc8,skc9,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,skc8)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u1355,negated_conjecture,
    true = ifeq3(unisex(skc8,skc13),true,true,true) ).

cnf(u598,negated_conjecture,
    b = ifeq2(tuple2(specific(skc8,skc11),true),tuple2(true,true),a,b) ).

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

cnf(u832,negated_conjecture,
    true = ifeq3(entity(skc10,skc11),true,true,true) ).

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

cnf(u604,negated_conjecture,
    b = ifeq2(tuple2(nonhuman(skc8,skc15),true),tuple2(true,true),a,b) ).

cnf(u1018,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc9),true) ).

cnf(u853,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc15),true,true,true) ).

cnf(u80,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).

cnf(u583,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc8,skc11)),tuple2(true,true),a,b) ).

cnf(u1346,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,unisex(X0,skc11),true) ).

cnf(u2251,negated_conjecture,
    true = female(skc10,skc12) ).

cnf(u3316,negated_conjecture,
    skc14 = ifeq4(of(skc8,skc14,X0),true,ifeq4(of(skc8,skc14,X0),true,ifeq4(entity(skc8,X0),true,skc14,skc14),skc14),skc14) ).

cnf(u1618,negated_conjecture,
    true = nonhuman(skc10,skc10) ).

cnf(u86,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(desire_want(X0,X2),true,desire_want(X1,X2),true),true) ).

cnf(u586,negated_conjecture,
    b = ifeq2(tuple2(unisex(skc8,skc15),true),tuple2(true,true),a,b) ).

cnf(u592,negated_conjecture,
    b = ifeq2(tuple2(unisex(skc8,skc12),true),tuple2(true,true),a,b) ).

cnf(u1887,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,nonhuman(X0,skc14),true) ).

cnf(u2138,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(relname(X0,skc14),true,true,true),true) ).

cnf(u609,negated_conjecture,
    b = ifeq2(tuple2(nonexistent(skc8,skc12),true),tuple2(true,true),a,b) ).

cnf(u364,negated_conjecture,
    true = ifeq3(abstraction(skc10,skc13),true,true,true) ).

cnf(u1654,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,relation(X0,skc10),true) ).

cnf(u1386,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc10,skc11)),tuple2(true,true),a,b) ).

cnf(u1380,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc14),true) ).

cnf(u2670,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(living(X0,skc12),true,true,true),true) ).

cnf(u2676,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,living(X0,skc15),true) ).

cnf(u1782,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(abstraction(X0,skc11),true,true,true),true) ).

cnf(u3795,negated_conjecture,
    ifeq4(theme(skc10,skc9,X0),true,ifeq4(theme(skc10,X1,X2),true,ifeq4(proposition(skc10,X0),true,ifeq4(proposition(skc10,X2),true,ifeq4(desire_want(skc10,X1),true,X0,X2),X2),X2),X2),X2) = X2 ).

cnf(u3296,negated_conjecture,
    skc11 = ifeq4(of(skc10,skc11,skc15),true,skc14,skc11) ).

cnf(u2798,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,animate(X0,skc15),true) ).

cnf(u632,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,event(X0,skc13),true) ).

cnf(u482,negated_conjecture,
    true = ifeq3(entity(skc8,skc14),true,true,true) ).

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

cnf(u3575,negated_conjecture,
    skc14 = ifeq4(of(skc10,skc14,X0),true,ifeq4(of(skc10,skc14,X0),true,ifeq4(entity(skc10,X0),true,skc14,skc14),skc14),skc14) ).

cnf(u1292,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonexistent(X0,skc9),true,true,true),true) ).

cnf(u225,negated_conjecture,
    b = ifeq(tuple(true,true,true,true,true,true,true,agent(skc10,skc13,skc15),agent(skc8,skc9,skc15),true),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u1004,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc15),true,true,true),true) ).

cnf(u3819,negated_conjecture,
    ifeq4(theme(skc10,X0,X1),true,ifeq4(proposition(skc10,X1),true,ifeq4(desire_want(skc10,X0),true,skc10,X1),X1),X1) = X1 ).

cnf(u2550,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,existent(X0,skc15),true) ).

cnf(u480,negated_conjecture,
    true = ifeq3(entity(skc8,skc11),true,true,true) ).

cnf(u114,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(impartial(X0,X2),true,impartial(X1,X2),true),true) ).

cnf(u1009,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc9),true,true,true),true) ).

cnf(u1027,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc13),true) ).

cnf(u782,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc14),true,true,true),true) ).

cnf(u1296,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,nonexistent(X0,skc13),true) ).

cnf(u3056,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,theme(X0,skc9,skc10),true) ).

cnf(u1023,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc14),true) ).

cnf(u788,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,thing(X0,skc15),true) ).

cnf(u2264,negated_conjecture,
    b = ifeq2(tuple2(unisex(skc10,skc12),true),tuple2(true,true),a,b) ).

cnf(u36,axiom,
    true = ifeq3(relname(X0,X1),true,relation(X0,X1),true) ).

cnf(u242,negated_conjecture,
    b = ifeq(tuple(dance(skc8,skc9),event(skc8,skc9),true,proposition(skc8,skc8),accessible_world(skc8,skc8),true,true,agent(skc8,skc9,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,skc8)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u807,negated_conjecture,
    true = thing(skc10,skc10) ).

cnf(u2332,negated_conjecture,
    true = human_person(skc10,skc15) ).

cnf(u2856,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,female(X0,skc12),true) ).

cnf(u2325,negated_conjecture,
    true = ifeq3(human_person(skc8,X0),true,human_person(skc10,X0),true) ).

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

cnf(u26,axiom,
    true = ifeq3(abstraction(X0,X1),true,thing(X0,X1),true) ).

cnf(u1299,negated_conjecture,
    true = ifeq3(nonexistent(skc8,skc13),true,true,true) ).

cnf(u3478,negated_conjecture,
    ifeq4(of(skc8,skc11,skc15),true,ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X0),true,skc11,X0),X0),X0) = X0 ).

cnf(u3109,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,of(X0,skc11,skc12),true) ).

cnf(u1559,negated_conjecture,
    true = desire_want(skc10,skc9) ).

cnf(u1670,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(relation(X0,skc14),true,true,true),true) ).

cnf(u565,negated_conjecture,
    true = ifeq3(abstraction(skc8,skc15),true,true,true) ).

cnf(u304,negated_conjecture,
    true = specific(skc10,skc13) ).

cnf(u24,axiom,
    true = ifeq3(relation(X0,X1),true,abstraction(X0,X1),true) ).

cnf(u154,negated_conjecture,
    true = proposition(skc8,skc10) ).

cnf(u1195,negated_conjecture,
    true = ifeq3(specific(skc8,X0),true,specific(skc10,X0),true) ).

cnf(u3237,negated_conjecture,
    skc14 = ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X0),true,X0,skc14),skc14) ).

cnf(u1194,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc13),true) ).

cnf(u2610,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(impartial(X0,skc12),true,true,true),true) ).

cnf(u1562,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(desire_want(X0,skc9),true,true,true),true) ).

cnf(u409,negated_conjecture,
    true = ifeq3(proposition(skc8,skc14),true,true,true) ).

cnf(u2616,negated_conjecture,
    true = ifeq3(impartial(skc8,X0),true,impartial(skc10,X0),true) ).

cnf(u152,negated_conjecture,
    true = mia_forename(skc8,skc11) ).

cnf(u810,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc10),true,true,true),true) ).

cnf(u3241,negated_conjecture,
    ifeq4(of(skc10,X0,skc15),true,ifeq4(forename(skc10,X0),true,skc14,X0),X0) = X0 ).

cnf(u1972,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(general(X0,skc10),true,true,true),true) ).

cnf(u1339,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc9),true,true,true),true) ).

cnf(u2972,negated_conjecture,
    true = ifeq3(male(skc8,X0),true,male(skc10,X0),true) ).

cnf(u3238,negated_conjecture,
    skc11 = ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X0),true,X0,skc11),skc11) ).

cnf(u1709,negated_conjecture,
    b = ifeq2(tuple2(true,human(skc10,skc14)),tuple2(true,true),a,b) ).

cnf(u816,negated_conjecture,
    true = singleton(skc10,skc10) ).

cnf(u1599,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(proposition(X0,skc10),true,true,true),true) ).

cnf(u2738,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,human(X0,skc15),true) ).

cnf(u308,negated_conjecture,
    true = nonexistent(skc10,skc13) ).

cnf(u1707,negated_conjecture,
    true = general(skc10,skc11) ).

cnf(u1976,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,general(X0,skc14),true) ).

cnf(u1696,negated_conjecture,
    true = general(skc10,skc14) ).

cnf(u567,negated_conjecture,
    true = ifeq3(eventuality(skc8,skc15),true,true,true) ).

cnf(u3242,negated_conjecture,
    ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X0),true,skc11,X0),X0) = X0 ).

cnf(u1713,negated_conjecture,
    b = ifeq2(tuple2(true,human(skc10,skc11)),tuple2(true,true),a,b) ).

cnf(u582,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc8,skc10)),tuple2(true,true),a,b) ).

cnf(u3099,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,of(X0,skc11,skc12),true) ).

cnf(u588,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc8,skc10)),tuple2(true,true),a,b) ).

cnf(u681,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc10,skc9)),tuple2(true,true),a,b) ).

cnf(u3900,negated_conjecture,
    ifeq4(theme(skc8,X0,skc10),true,ifeq4(theme(skc8,skc9,X1),true,ifeq4(proposition(skc8,X1),true,ifeq4(desire_want(skc8,X0),true,skc10,X1),X1),X1),X1) = X1 ).

cnf(u2483,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(entity(X0,skc15),true,true,true),true) ).

cnf(u837,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc11),true) ).

cnf(u64,axiom,
    true = ifeq3(man(X0,X1),true,human_person(X0,X1),true) ).

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

cnf(u3898,negated_conjecture,
    ifeq4(theme(skc8,skc9,X0),true,ifeq4(theme(skc8,skc9,X1),true,ifeq4(proposition(skc8,X0),true,ifeq4(proposition(skc8,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u3513,negated_conjecture,
    skc11 = ifeq4(of(skc10,skc14,X0),true,ifeq4(of(skc10,skc11,X0),true,ifeq4(entity(skc10,X0),true,skc14,skc11),skc11),skc11) ).

cnf(u835,negated_conjecture,
    true = ifeq3(eventuality(skc10,skc11),true,true,true) ).

cnf(u2894,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(vincent_forename(X0,skc14),true,true,true),true) ).

cnf(u1621,negated_conjecture,
    b = ifeq2(tuple2(true,human(skc10,skc10)),tuple2(true,true),a,b) ).

cnf(u1981,negated_conjecture,
    true = ifeq3(general(skc8,X0),true,general(skc10,X0),true) ).

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

cnf(u1602,negated_conjecture,
    true = relation(skc10,skc10) ).

cnf(u1619,negated_conjecture,
    true = general(skc10,skc10) ).

cnf(u1979,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,general(X0,skc11),true) ).

cnf(u70,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(event(X0,X2),true,event(X1,X2),true),true) ).

cnf(u817,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,thing(X0,skc10),true) ).

cnf(u850,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc15),true,true,true),true) ).

cnf(u2239,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(woman(X0,skc12),true,true,true),true) ).

cnf(u1970,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(general(X0,skc11),true,true,true),true) ).

cnf(u856,negated_conjecture,
    true = singleton(skc10,skc15) ).

cnf(u593,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc10,skc13)),tuple2(true,true),a,b) ).

cnf(u68,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(dance(X0,X2),true,dance(X1,X2),true),true) ).

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

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

cnf(u607,negated_conjecture,
    b = ifeq2(tuple2(true,existent(skc10,skc13)),tuple2(true,true),a,b) ).

cnf(u1490,negated_conjecture,
    true = ifeq3(present(X0,skc9),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(u2888,negated_conjecture,
    true = ifeq3(vincent_forename(skc8,X0),true,vincent_forename(skc10,X0),true) ).

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

cnf(u110,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(entity(X0,X2),true,entity(X1,X2),true),true) ).

cnf(u196,negated_conjecture,
    b = ifeq(tuple(dance(skc8,skc9),event(skc8,skc9),desire_want(skc8,X0),proposition(skc8,skc8),accessible_world(skc8,skc8),true,present(skc8,X0),agent(skc8,skc9,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc8)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u2891,negated_conjecture,
    true = vincent_forename(skc10,skc14) ).

cnf(u3280,negated_conjecture,
    skc14 = ifeq4(of(skc10,skc11,skc15),true,skc11,skc14) ).

cnf(u1498,negated_conjecture,
    b = ifeq(tuple(dance(skc10,skc9),true,desire_want(skc8,X0),true,true,true,present(skc8,X0),agent(skc10,skc9,skc15),agent(skc8,X0,skc15),theme(skc8,X0,skc10)),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u2675,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,living(X0,skc12),true) ).

cnf(u3675,negated_conjecture,
    ifeq4(of(skc10,skc14,skc12),true,ifeq4(of(skc10,X0,skc12),true,ifeq4(forename(skc10,X0),true,skc14,X0),X0),X0) = X0 ).

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

cnf(u365,negated_conjecture,
    true = ifeq3(abstraction(skc8,skc9),true,true,true) ).

cnf(u616,negated_conjecture,
    true = ifeq3(accessible_world(skc10,skc10),true,true,true) ).

cnf(u3799,negated_conjecture,
    ifeq4(theme(skc10,X0,skc10),true,ifeq4(theme(skc10,X1,X2),true,ifeq4(proposition(skc10,X2),true,ifeq4(desire_want(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,skc10,X2),X2),X2),X2),X2) = X2 ).

cnf(u466,negated_conjecture,
    true = human_person(skc8,skc12) ).

cnf(u108,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(organism(X0,X2),true,organism(X1,X2),true),true) ).

cnf(u2678,negated_conjecture,
    true = ifeq3(living(skc8,X0),true,living(skc10,X0),true) ).

cnf(u1496,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,present(X0,skc9),true) ).

cnf(u4032,negated_conjecture,
    ifeq4(theme(skc10,X0,skc10),true,ifeq4(theme(skc10,skc9,X1),true,ifeq4(proposition(skc10,X1),true,ifeq4(desire_want(skc10,X0),true,skc10,X1),X1),X1),X1) = X1 ).

cnf(u3825,negated_conjecture,
    skc10 = ifeq4(theme(skc8,X0,skc10),true,ifeq4(desire_want(skc8,X0),true,skc10,skc10),skc10) ).

cnf(u98,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(forename(X0,X2),true,forename(X1,X2),true),true) ).

cnf(u1385,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc10,skc11)),tuple2(true,true),a,b) ).

cnf(u2420,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(organism(X0,skc12),true,true,true),true) ).

cnf(u3949,negated_conjecture,
    skc10 = ifeq4(theme(skc8,skc9,X0),true,ifeq4(theme(skc8,X1,skc10),true,ifeq4(proposition(skc8,X0),true,ifeq4(desire_want(skc8,X1),true,X0,skc10),skc10),skc10),skc10) ).

cnf(u1007,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc12),true,true,true),true) ).

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

cnf(u2293,negated_conjecture,
    b = ifeq2(tuple2(nonexistent(skc10,skc12),true),tuple2(true,true),a,b) ).

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

cnf(u2734,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(human(X0,skc12),true,true,true),true) ).

cnf(u777,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc15),true,true,true),true) ).

cnf(u20,axiom,
    true = ifeq3(desire_want(X0,X1),true,event(X0,X1),true) ).

cnf(u2740,negated_conjecture,
    true = ifeq3(human(skc8,X0),true,human(skc10,X0),true) ).

cnf(u2548,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(existent(X0,skc12),true,true,true),true) ).

cnf(u1022,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc15),true) ).

cnf(u1293,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(nonexistent(X0,skc9),true,true,true),true) ).

cnf(u791,negated_conjecture,
    true = ifeq3(thing(skc8,X0),true,thing(skc10,X0),true) ).

cnf(u2672,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(living(X0,skc12),true,true,true),true) ).

cnf(u4081,negated_conjecture,
    skc10 = ifeq4(theme(skc10,skc9,X0),true,ifeq4(theme(skc10,X1,skc10),true,ifeq4(proposition(skc10,X0),true,ifeq4(desire_want(skc10,X1),true,X0,skc10),skc10),skc10),skc10) ).

cnf(u504,negated_conjecture,
    true = impartial(skc8,skc12) ).

cnf(u10,axiom,
    true = ifeq3(eventuality(X0,X1),true,thing(X0,X1),true) ).

cnf(u1297,negated_conjecture,
    true = ifeq3(nonexistent(skc8,X0),true,nonexistent(skc10,X0),true) ).

cnf(u2794,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(animate(X0,skc12),true,true,true),true) ).

cnf(u1657,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,relation(X0,skc10),true) ).

cnf(u2203,negated_conjecture,
    true = ifeq3(mia_forename(skc8,X0),true,mia_forename(skc10,X0),true) ).

cnf(u2335,negated_conjecture,
    true = ifeq3(woman(skc10,skc15),true,true,true) ).

cnf(u2800,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,animate(X0,skc15),true) ).

cnf(u2067,negated_conjecture,
    true = ifeq3(vincent_forename(skc10,skc14),true,true,true) ).

cnf(u781,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc9),true,true,true),true) ).

cnf(u8,axiom,
    true = ifeq3(event(X0,X1),true,eventuality(X0,X1),true) ).

cnf(u2322,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,human_person(X0,skc12),true) ).

cnf(u3097,negated_conjecture,
    true = ifeq3(of(X0,skc11,skc12),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).

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

cnf(u1785,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(abstraction(X0,skc14),true,true,true),true) ).

cnf(u779,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(thing(X0,skc12),true,true,true),true) ).

cnf(u2677,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,living(X0,skc12),true) ).

cnf(u1016,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc14),true,true,true),true) ).

cnf(u3202,negated_conjecture,
    ifeq4(of(skc10,X0,skc12),true,ifeq4(of(skc10,X1,skc12),true,ifeq4(forename(skc10,X0),true,ifeq4(forename(skc10,X1),true,X0,X1),X1),X1),X1) = X1 ).

cnf(u3117,negated_conjecture,
    true = ifeq3(of(X0,skc14,skc15),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(clause73,axiom,
    ifeq4(theme(X0,X1,X2),true,ifeq4(theme(X0,X3,X4),true,ifeq4(proposition(X0,X2),true,ifeq4(proposition(X0,X4),true,ifeq4(desire_want(X0,X1),true,ifeq4(desire_want(X0,X3),true,X2,X4),X4),X4),X4),X4),X4) = X4 ).

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

cnf(u1676,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,relation(X0,skc14),true) ).

cnf(u478,negated_conjecture,
    true = ifeq3(entity(skc10,skc13),true,true,true) ).

cnf(u1674,negated_conjecture,
    true = ifeq3(proposition(skc10,skc14),true,true,true) ).

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

cnf(u292,negated_conjecture,
    true = eventuality(skc10,skc13) ).

cnf(u2339,negated_conjecture,
    true = ifeq3(man(skc10,skc15),true,true,true) ).

cnf(u48,axiom,
    true = ifeq3(entity(X0,X1),true,specific(X0,X1),true) ).

cnf(u1343,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(unisex(X0,skc14),true,true,true),true) ).

cnf(u2082,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(forename(X0,skc11),true,true,true),true) ).

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

cnf(u694,negated_conjecture,
    true = ifeq3(accessible_world(skc10,skc8),true,true,true) ).

cnf(u2612,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,impartial(X0,skc15),true) ).

cnf(u1711,negated_conjecture,
    b = ifeq2(tuple2(specific(skc10,skc14),true),tuple2(true,true),a,b) ).

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

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

cnf(u54,axiom,
    true = ifeq3(organism(X0,X1),true,living(X0,X1),true) ).

cnf(u176,axiom,
    b = ifeq2(tuple2(unisex(X0,X1),male(X0,X1)),tuple2(true,true),a,b) ).

cnf(u1605,negated_conjecture,
    true = ifeq3(relname(skc10,skc10),true,true,true) ).

cnf(u2733,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human(X0,skc15),true,true,true),true) ).

cnf(u3240,negated_conjecture,
    skc14 = ifeq4(of(skc8,X0,skc15),true,ifeq4(forename(skc8,X0),true,X0,skc14),skc14) ).

cnf(u1603,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,proposition(X0,skc10),true) ).

cnf(u1185,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(specific(X0,skc13),true,true,true),true) ).

cnf(u182,axiom,
    b = ifeq2(tuple2(nonhuman(X0,X1),human(X0,X1)),tuple2(true,true),a,b) ).

cnf(u2488,negated_conjecture,
    true = ifeq3(entity(skc8,X0),true,entity(skc10,X0),true) ).

cnf(u610,negated_conjecture,
    b = ifeq2(tuple2(nonexistent(skc8,skc15),true),tuple2(true,true),a,b) ).

cnf(u682,negated_conjecture,
    b = ifeq2(tuple2(true,male(skc10,skc9)),tuple2(true,true),a,b) ).

cnf(u1969,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(general(X0,skc10),true,true,true),true) ).

cnf(u1350,negated_conjecture,
    true = ifeq3(unisex(skc8,X0),true,unisex(skc10,X0),true) ).

cnf(u840,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc12),true,true,true),true) ).

cnf(u180,axiom,
    b = ifeq2(tuple2(specific(X0,X1),general(X0,X1)),tuple2(true,true),a,b) ).

cnf(u1483,negated_conjecture,
    true = ifeq3(present(skc8,skc13),true,true,true) ).

cnf(u591,negated_conjecture,
    b = ifeq2(tuple2(true,female(skc8,skc14)),tuple2(true,true),a,b) ).

cnf(u3017,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,agent(X0,skc9,skc12),true) ).

cnf(u1348,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,unisex(X0,skc9),true) ).

cnf(u1478,negated_conjecture,
    true = ifeq3(present(X0,skc9),true,ifeq3(accessible_world(X0,skc8),true,true,true),true) ).

cnf(u3005,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,agent(X0,skc9,skc12),true) ).

cnf(u322,negated_conjecture,
    true = ifeq3(dance(skc8,skc9),true,true,true) ).

cnf(u94,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).

cnf(u3003,negated_conjecture,
    true = ifeq3(agent(skc8,X0,X1),true,agent(skc10,X0,X1),true) ).

cnf(u1221,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,specific(X0,skc12),true) ).

cnf(u3264,negated_conjecture,
    skc14 = ifeq4(of(skc8,skc14,skc12),true,skc11,skc14) ).

cnf(u594,negated_conjecture,
    b = ifeq2(tuple2(true,general(skc8,skc9)),tuple2(true,true),a,b) ).

cnf(u1881,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(nonhuman(X0,skc10),true,true,true),true) ).

cnf(u600,negated_conjecture,
    b = ifeq2(tuple2(true,human(skc8,skc10)),tuple2(true,true),a,b) ).

cnf(u92,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).

cnf(u160,negated_conjecture,
    true = present(skc8,skc9) ).

cnf(u1365,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(unisex(X0,skc10),true,true,true),true) ).

cnf(u1480,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,present(X0,skc9),true) ).

cnf(u2144,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,relname(X0,skc11),true) ).

cnf(u82,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(unisex(X0,X2),true,unisex(X1,X2),true),true) ).

cnf(u3793,negated_conjecture,
    ifeq4(theme(skc10,X0,X1),true,ifeq4(theme(skc10,skc9,X2),true,ifeq4(proposition(skc10,X1),true,ifeq4(proposition(skc10,X2),true,ifeq4(desire_want(skc10,X0),true,X1,X2),X2),X2),X2),X2) = X2 ).

cnf(u631,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,event(X0,skc9),true) ).

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

cnf(u360,negated_conjecture,
    true = abstraction(skc8,skc10) ).

cnf(u2423,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,organism(X0,skc12),true) ).

cnf(u3881,negated_conjecture,
    ifeq4(theme(skc10,skc9,X0),true,ifeq4(proposition(skc10,X0),true,skc10,X0),X0) = X0 ).

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

cnf(u1497,negated_conjecture,
    b = ifeq(tuple(dance(skc10,skc9),true,true,true,true,true,true,agent(skc10,skc9,skc15),agent(skc8,skc9,skc15),true),tuple(true,true,true,true,true,true,true,true,true,true),a,b) ).

cnf(u1006,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(singleton(X0,skc13),true,true,true),true) ).

cnf(u3061,negated_conjecture,
    true = theme(skc10,skc9,skc10) ).

cnf(u775,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(thing(X0,skc13),true,true,true),true) ).

cnf(u1792,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,abstraction(X0,skc10),true) ).

cnf(u2673,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(living(X0,skc15),true,true,true),true) ).

cnf(u1012,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(singleton(X0,skc10),true,true,true),true) ).

cnf(u379,negated_conjecture,
    true = general(skc8,skc10) ).

cnf(u732,negated_conjecture,
    true = ifeq3(eventuality(skc8,X0),true,eventuality(skc10,X0),true) ).

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

cnf(u2421,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(organism(X0,skc15),true,true,true),true) ).

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

cnf(u2551,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,existent(X0,skc12),true) ).

cnf(u122,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(female(X0,X2),true,female(X1,X2),true),true) ).

cnf(u1017,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,singleton(X0,skc14),true) ).

cnf(u3574,negated_conjecture,
    skc14 = ifeq4(of(skc10,skc11,X0),true,ifeq4(of(skc10,skc14,X0),true,ifeq4(entity(skc10,X0),true,skc11,skc14),skc14),skc14) ).

cnf(u1024,negated_conjecture,
    true = ifeq3(accessible_world(skc10,X0),true,singleton(X0,skc9),true) ).

cnf(u2319,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc8),true,ifeq3(human_person(X0,skc12),true,true,true),true) ).

cnf(u1655,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,relation(X0,skc14),true) ).

cnf(u2801,negated_conjecture,
    true = ifeq3(accessible_world(skc8,X0),true,animate(X0,skc12),true) ).

cnf(u516,negated_conjecture,
    true = animate(skc8,skc12) ).

cnf(u3861,negated_conjecture,
    skc10 = ifeq4(theme(skc10,X0,skc10),true,ifeq4(desire_want(skc10,X0),true,skc10,skc10),skc10) ).

cnf(u2549,negated_conjecture,
    true = ifeq3(accessible_world(X0,skc10),true,ifeq3(existent(X0,skc15),true,true,true),true) ).

cnf(u120,axiom,
    true = ifeq3(accessible_world(X0,X1),true,ifeq3(animate(X0,X2),true,animate(X1,X2),true),true) ).

cnf(u2940,negated_conjecture,
    b = ifeq2(tuple2(female(skc10,skc15),true),tuple2(true,true),a,b) ).

cnf(u3063,negated_conjecture,
    true = ifeq3(theme(X0,skc9,skc10),true,ifeq3(accessible_world(X0,skc10),true,true,true),true) ).

cnf(u1658,negated_conjecture,
    true = ifeq3(relation(skc8,X0),true,relation(skc10,X0),true) ).

cnf(u2060,negated_conjecture,
    true = ifeq3(forename(skc8,X0),true,forename(skc10,X0),true) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : NLP024-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.36  % Computer : n001.cluster.edu
% 0.04/0.36  % Model    : x86_64 x86_64
% 0.04/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.36  % Memory   : 8046.5625MB
% 0.04/0.36  % OS       : Linux 6.8.0-71-generic
% 0.04/0.36  % CPULimit : 300
% 0.04/0.36  % WCLimit  : 300
% 0.04/0.36  % DateTime : Sun Sep 27 17:55:01 UTC 2026
% 0.04/0.36  % CPUTime  : 
% 0.04/0.36  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.39  Running first-order model finding
% 0.04/0.39  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.12/0.60  % (3840239)Will run a generic schedule for satisfiability detection.
% 1.12/0.60  % (3840244)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=295430003_2999 on theBenchmark for (2999ds/0Mi)
% 1.12/0.60  % (3840245)% WARNING: option uhcvi not known.
% 1.12/0.60  % (3840246)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1518736507:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.12/0.60  % (3840250)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4089095411:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.12/0.60  % (3840247)dis+10_1_sil=32000:sp=arity:random_seed=96268984:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.12/0.60  % (3840248)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1818681691:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.12/0.60  % (3840249)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3478768934:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.12/0.60  % (3840245)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=55290963:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.12/0.60  % TRYING [1]
% 1.12/0.60  % TRYING [2]
% 1.12/0.60  % TRYING [3]
% 1.12/0.60  % (3840247)Instruction limit reached! 
% 1.12/0.60  % (3840247)------------------------------
% 1.12/0.60  % (3840247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.60  % (3840247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.60  % (3840247)CaDiCaL version: 2.1.3
% 1.12/0.60  % (3840247)Termination reason: Instruction limit
% 1.12/0.60  % (3840247)Termination phase: Saturation
% 1.12/0.60  % (3840247)Time elapsed: 0.060 s
% 1.12/0.60  % (3840247)Peak memory usage: 12 MB
% 1.12/0.60  % (3840247)Instructions burned: 104 (million)
% 1.12/0.60  % (3840248)Instruction limit reached! 
% 1.12/0.60  % (3840248)------------------------------
% 1.12/0.60  % (3840248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.60  % (3840248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.60  % (3840248)CaDiCaL version: 2.1.3
% 1.12/0.60  % (3840248)Termination reason: Instruction limit
% 1.12/0.60  % (3840248)Termination phase: Saturation
% 1.12/0.60  % (3840248)Time elapsed: 0.067 s
% 1.12/0.60  % (3840248)Peak memory usage: 13 MB
% 1.12/0.60  % (3840248)Instructions burned: 116 (million)
% 1.12/0.60  % (3840249)Instruction limit reached! 
% 1.12/0.60  % (3840249)------------------------------
% 1.12/0.60  % (3840249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.60  % (3840249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.60  % (3840249)CaDiCaL version: 2.1.3
% 1.12/0.60  % (3840249)Termination reason: Instruction limit
% 1.12/0.60  % (3840249)Termination phase: Saturation
% 1.12/0.60  % (3840249)Time elapsed: 0.075 s
% 1.12/0.60  % (3840249)Peak memory usage: 12 MB
% 1.12/0.60  % (3840249)Instructions burned: 132 (million)
% 1.12/0.60  % (3840258)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2421227037:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.12/0.60  % (3840250)Instruction limit reached! 
% 1.12/0.60  % (3840250)------------------------------
% 1.12/0.60  % (3840250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.60  % (3840250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.60  % (3840250)CaDiCaL version: 2.1.3
% 1.12/0.60  % (3840250)Termination reason: Instruction limit
% 1.12/0.60  % (3840250)Termination phase: Saturation
% 1.12/0.60  % (3840250)Time elapsed: 0.087 s
% 1.12/0.60  % (3840250)Peak memory usage: 12 MB
% 1.12/0.60  % (3840250)Instructions burned: 160 (million)
% 1.12/0.60  % (3840259)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=693881887:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.12/0.60  % (3840260)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3147633795:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.12/0.60  % TRYING [1]
% 1.12/0.60  % TRYING [2]
% 1.12/0.60  % (3840263)ott-21_1_sil=16000:fs=off:random_seed=3413155907:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.12/0.60  % TRYING [3]
% 1.12/0.60  % (3840246) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3840239-3840246"...
% 1.12/0.60  % (3840246)...printing done.
% 1.12/0.60  % SZS status Satisfiable for theBenchmark
% 1.12/0.60  % SZS output start Saturation.
% See solution above
% 1.12/0.61  % SZS output start Definitions and Model Updates.
% 1.12/0.61  % SZS output end Definitions and Model Updates.
% 1.12/0.61  % (3840246)------------------------------
% 1.12/0.61  % (3840246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.12/0.61  % (3840246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.12/0.61  % (3840246)CaDiCaL version: 2.1.3
% 1.12/0.61  % (3840246)Termination reason: Satisfiable
% 1.12/0.61  % (3840246)Time elapsed: 0.154 s
% 1.12/0.61  % (3840246)Peak memory usage: 14 MB
% 1.12/0.61  % (3840246)Instructions burned: 276 (million)
% 1.12/0.61  % (3840239)Success in time 0.196 s
% 1.12/0.61  % Vampire exiting
%------------------------------------------------------------------------------