%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP220-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:07:58 PM UTC 2026
% Result : Satisfiable 4.42s 1.76s
% Output : Saturation 6.68s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1809,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skf1(X1)),true) ).
cnf(u1582,negated_conjecture,
ifeq3(of(skc6,X0,skc9),true,ifeq3(of(skc6,X1,skc9),true,ifeq3(forename(skc6,X0),true,ifeq3(forename(skc6,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u1783,negated_conjecture,
true = specific(skc6,skc7) ).
cnf(u1386,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,nonhuman(X0,skc8),true) ).
cnf(u1416,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonhuman(X0,skc8),true,true,true),true) ).
cnf(u723,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(eventuality(X0,skf1(X1)),true,true,true),true) ).
cnf(u1935,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc7),true,true,true),true) ).
cnf(u1775,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonexistent(X0,skf1(X1)),true) ).
cnf(u1756,negated_conjecture,
b = ifeq(tuple(true,existent(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u1583,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,entity(X0,skc9),true) ).
cnf(u1410,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,general(X0,skc8),true) ).
cnf(u63,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(eventuality(X0,X2),true,eventuality(X1,X2),true),true) ).
cnf(u1600,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(living(X0,skc9),true,true,true),true) ).
cnf(u1524,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,animate(X0,skc9),true) ).
cnf(u1214,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,abstraction(X0,skc6),true) ).
cnf(u1293,negated_conjecture,
b = ifeq(tuple(human(skc6,skc6),true),tuple(true,true),a,b) ).
cnf(u1454,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(abstraction(X0,skc8),true,true,true),true) ).
cnf(u1213,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(abstraction(X0,skc6),true,true,true),true) ).
cnf(u1547,negated_conjecture,
true = entity(skc5,skc9) ).
cnf(u3091,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(agent(skc6,X1,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,X1),true,skc6,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u526,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(eventuality(X0,skc7),true,true,true),true) ).
cnf(u1765,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(nonexistent(X0,skc7),true,true,true),true) ).
cnf(u1362,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,relation(X0,skc8),true) ).
cnf(u1623,negated_conjecture,
b = ifeq(tuple(nonexistent(skc6,skc9),true),tuple(true,true),a,b) ).
cnf(u1616,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(existent(X0,skc9),true,true,true),true) ).
cnf(u310,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1435,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc8),true) ).
cnf(u751,negated_conjecture,
true = ifeq2(of(X0,skc8,skc9),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u588,negated_conjecture,
true = vincent_forename(skc6,skc8) ).
cnf(u1615,negated_conjecture,
b = ifeq(tuple(nonexistent(skc5,skc9),true),tuple(true,true),a,b) ).
cnf(u634,negated_conjecture,
true = proposition(skc6,skc6) ).
cnf(u1433,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc8),true,true,true),true) ).
cnf(u1705,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u1281,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,general(X0,skc6),true) ).
cnf(u506,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,male(X0,skc9),true) ).
cnf(u2041,negated_conjecture,
true = ifeq2(accessible_world(skc6,skc6),true,true,true) ).
cnf(u3096,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1561,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,entity(X0,skc9),true) ).
cnf(u508,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(human_person(X0,skc9),true,true,true),true) ).
cnf(u1893,negated_conjecture,
true = thing(skc5,skc7) ).
cnf(u1902,negated_conjecture,
true = singleton(skc6,skc7) ).
cnf(u540,negated_conjecture,
true = ifeq2(think_believe_consider(X0,skc7),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u1714,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u489,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,man(X0,skc9),true) ).
cnf(u502,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,smoke(X0,skf1(X1)),true) ).
cnf(u1542,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,impartial(X0,skc9),true) ).
cnf(u781,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u139,negated_conjecture,
true = proposition(skc5,skc6) ).
cnf(u271,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,X2),true,ifeq3(agent(skc5,X1,skc9),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1399,negated_conjecture,
b = ifeq(tuple(true,male(skc5,skc8)),tuple(true,true),a,b) ).
cnf(u3126,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u3093,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(agent(skc6,X1,X2),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u141,negated_conjecture,
true = of(skc5,skc8,skc9) ).
cnf(u449,negated_conjecture,
true = ifeq2(singleton(skc5,X0),true,singleton(skc6,X0),true) ).
cnf(u1923,negated_conjecture,
true = singleton(skc5,skc7) ).
cnf(u1693,negated_conjecture,
true = singleton(skc5,skc9) ).
cnf(u977,negated_conjecture,
true = ifeq2(agent(skc5,skf1(skc9),skc9),true,true,true) ).
cnf(u135,negated_conjecture,
true = think_believe_consider(skc5,skc7) ).
cnf(u1363,negated_conjecture,
true = abstraction(skc5,skc8) ).
cnf(u91,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human(X0,X2),true,human(X1,X2),true),true) ).
cnf(u1602,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,living(X0,skc9),true) ).
cnf(u249,negated_conjecture,
true = ifeq2(man(skc5,X0),true,man(skc6,X0),true) ).
cnf(u440,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,male(X0,skc9),true) ).
cnf(u1700,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc9),true) ).
cnf(u93,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(animate(X0,X2),true,animate(X1,X2),true),true) ).
cnf(u1860,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,unisex(X0,skc7),true) ).
cnf(u243,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,forename(X0,skc8),true) ).
cnf(u1337,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,human(X0,skc9),true) ).
cnf(u668,negated_conjecture,
true = ifeq2(accessible_world(skc5,skc5),true,true,true) ).
cnf(u725,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,eventuality(X0,skf1(X1)),true) ).
cnf(u49,axiom,
true = ifeq2(abstraction(X0,X1),true,general(X0,X1),true) ).
cnf(u464,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,relation(X0,skc6),true) ).
cnf(u87,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(impartial(X0,X2),true,impartial(X1,X2),true),true) ).
cnf(u1752,negated_conjecture,
true = nonexistent(skc6,skc7) ).
cnf(u436,negated_conjecture,
true = male(skc5,skc9) ).
cnf(u43,axiom,
true = ifeq2(relation(X0,X1),true,abstraction(X0,X1),true) ).
cnf(u1759,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonexistent(X0,skc7),true) ).
cnf(u73,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(unisex(X0,X2),true,unisex(X1,X2),true),true) ).
cnf(u1471,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc8),true,true,true),true) ).
cnf(u239,negated_conjecture,
true = ifeq2(smoke(skc5,X0),true,smoke(skc6,X0),true) ).
cnf(u866,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,X1,skc6),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(agent(skc5,X1,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(think_believe_consider(skc5,X1),true,skc6,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u45,axiom,
true = ifeq2(abstraction(X0,X1),true,thing(X0,X1),true) ).
cnf(u1856,negated_conjecture,
true = ifeq2(abstraction(skc5,skc7),true,true,true) ).
cnf(u67,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(singleton(X0,X2),true,singleton(X1,X2),true),true) ).
cnf(u258,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(theme(skc5,X2,skc6),true,ifeq3(agent(skc5,X0,X3),true,ifeq3(agent(skc5,X2,X3),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(think_believe_consider(skc5,X2),true,ifeq3(proposition(skc5,X1),true,skc6,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1088,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,X0,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u557,negated_conjecture,
ifeq3(of(skc6,skc8,X0),true,ifeq3(of(skc6,X1,X0),true,ifeq3(forename(skc6,X1),true,ifeq3(entity(skc6,X0),true,skc8,X1),X1),X1),X1) = X1 ).
cnf(u416,negated_conjecture,
true = ifeq2(existent(skc5,X0),true,existent(skc6,X0),true) ).
cnf(u39,axiom,
true = ifeq2(man(X0,X1),true,male(X0,X1),true) ).
cnf(u69,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(specific(X0,X2),true,specific(X1,X2),true),true) ).
cnf(u1511,negated_conjecture,
true = animate(skc6,skc9) ).
cnf(u260,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(theme(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,X3),true,ifeq3(agent(skc5,skc7,X3),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,ifeq3(proposition(skc5,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1798,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(specific(X0,skc7),true,true,true),true) ).
cnf(u25,axiom,
true = ifeq2(entity(X0,X1),true,thing(X0,X1),true) ).
cnf(u658,negated_conjecture,
true = ifeq2(present(X0,skc7),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u1344,negated_conjecture,
true = relation(skc6,skc8) ).
cnf(u1494,negated_conjecture,
true = organism(skc5,skc9) ).
cnf(u1875,negated_conjecture,
skc8 = ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,X0,skc8),skc8) ).
cnf(u630,negated_conjecture,
true = of(skc6,skc8,skc9) ).
cnf(u19,axiom,
true = ifeq2(man(X0,X1),true,human_person(X0,X1),true) ).
cnf(u1684,negated_conjecture,
true = thing(skc6,skc9) ).
cnf(u1466,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc8),true) ).
cnf(u3125,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u1844,negated_conjecture,
true = unisex(skc5,skc7) ).
cnf(u180,negated_conjecture,
true = ifeq2(agent(skc5,X0,X1),true,agent(skc6,X0,X1),true) ).
cnf(u21,axiom,
true = ifeq2(human_person(X0,X1),true,organism(X0,X1),true) ).
cnf(u495,negated_conjecture,
true = agent(skc6,skf1(skc9),skc9) ).
cnf(u1441,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skc8)),tuple(true,true),a,b) ).
cnf(u1279,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(general(X0,skc6),true,true,true),true) ).
cnf(u15,axiom,
true = ifeq2(eventuality(X0,X1),true,nonexistent(X0,X1),true) ).
cnf(u1418,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonhuman(X0,skc8),true) ).
cnf(u1680,negated_conjecture,
true = ifeq2(entity(skc5,skc6),true,true,true) ).
cnf(ifeq_axiom_001,axiom,
ifeq2(X0,X0,X1,X2) = X1 ).
cnf(u1840,negated_conjecture,
true = ifeq2(eventuality(skc5,skc8),true,true,true) ).
cnf(u1636,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(specific(X0,skc9),true,true,true),true) ).
cnf(u1643,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skc9)),tuple(true,true),a,b) ).
cnf(ifeq_axiom,axiom,
ifeq3(X0,X0,X1,X2) = X1 ).
cnf(u762,negated_conjecture,
ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,ifeq3(entity(skc6,skc9),true,skc8,X0),X0),X0) = X0 ).
cnf(u983,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1922,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc7),true) ).
cnf(u1404,negated_conjecture,
true = unisex(skc6,skc8) ).
cnf(u782,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,X2),true,ifeq3(agent(skc6,skc7,X2),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1),X1) = X1 ).
cnf(u1788,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u519,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,relname(X0,skc8),true) ).
cnf(u605,negated_conjecture,
skc8 = ifeq3(of(skc5,skc8,X0),true,ifeq3(of(skc5,skc8,X0),true,ifeq3(entity(skc5,X0),true,skc8,skc8),skc8),skc8) ).
cnf(u1238,negated_conjecture,
b = ifeq(tuple(human(skc5,skc6),true),tuple(true,true),a,b) ).
cnf(u1780,negated_conjecture,
true = ifeq2(eventuality(skc5,skc9),true,true,true) ).
cnf(u1515,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(animate(X0,skc9),true,true,true),true) ).
cnf(u1632,negated_conjecture,
true = specific(skc5,skc9) ).
cnf(u1402,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,unisex(X0,skc8),true) ).
cnf(u1940,negated_conjecture,
true = ifeq2(singleton(skc5,skf1(X0)),true,true,true) ).
cnf(u1375,negated_conjecture,
true = unisex(skc5,skc8) ).
cnf(u1517,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,animate(X0,skc9),true) ).
cnf(u277,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1247,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(general(X0,skc6),true,true,true),true) ).
cnf(u3260,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skf1(skc9),X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u558,negated_conjecture,
skc8 = ifeq3(of(skc6,X0,X1),true,ifeq3(of(skc6,skc8,X1),true,ifeq3(forename(skc6,X0),true,ifeq3(entity(skc6,X1),true,X0,skc8),skc8),skc8),skc8) ).
cnf(u909,negated_conjecture,
true = ifeq2(accessible_world(skc6,X1),true,present(X1,skf1(X0)),true) ).
cnf(u1612,negated_conjecture,
true = existent(skc5,skc9) ).
cnf(u1394,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,general(X0,skc8),true) ).
cnf(u1233,negated_conjecture,
true = thing(skc5,skc6) ).
cnf(u1424,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc8),true,true,true),true) ).
cnf(u1388,negated_conjecture,
true = nonhuman(skc6,skc8) ).
cnf(u2026,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6) ).
cnf(u460,negated_conjecture,
true = relation(skc5,skc6) ).
cnf(u1839,negated_conjecture,
true = ifeq2(eventuality(skc6,skc6),true,true,true) ).
cnf(u3068,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,skc7,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6) ).
cnf(u663,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relation(X0,skc6),true,true,true),true) ).
cnf(u1327,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(human(X0,skc9),true,true,true),true) ).
cnf(u1374,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,abstraction(X0,skc8),true) ).
cnf(u1912,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skf1(X1)),true) ).
cnf(u517,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(relname(X0,skc8),true,true,true),true) ).
cnf(u1313,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc6),true) ).
cnf(u644,negated_conjecture,
true = relation(skc6,skc6) ).
cnf(u222,negated_conjecture,
true = ifeq2(proposition(skc5,X0),true,proposition(skc6,X0),true) ).
cnf(u1384,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(nonhuman(X0,skc8),true,true,true),true) ).
cnf(u763,negated_conjecture,
skc8 = ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,ifeq3(entity(skc6,skc9),true,X0,skc8),skc8),skc8) ).
cnf(u221,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,proposition(X0,skc6),true) ).
cnf(u1593,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(living(X0,skc9),true,true,true),true) ).
cnf(u412,negated_conjecture,
true = ifeq2(nonhuman(skc5,X0),true,nonhuman(skc6,X0),true) ).
cnf(u236,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,vincent_forename(X0,skc8),true) ).
cnf(u208,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,theme(X0,skc7,skc6),true) ).
cnf(u1560,negated_conjecture,
ifeq3(of(skc5,X0,skc9),true,ifeq3(of(skc5,X1,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(forename(skc5,X1),true,X0,X1),X1),X1),X1) = X1 ).
cnf(u95,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(male(X0,X2),true,male(X1,X2),true),true) ).
cnf(u215,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(event(X0,skc7),true,true,true),true) ).
cnf(u563,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relname(X0,skc8),true,true,true),true) ).
cnf(u406,negated_conjecture,
true = ifeq2(organism(skc5,X0),true,organism(skc6,X0),true) ).
cnf(u171,negated_conjecture,
true = ifeq2(present(skc5,X0),true,present(skc6,X0),true) ).
cnf(u362,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,X1),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u1215,negated_conjecture,
true = unisex(skc6,skc6) ).
cnf(u174,negated_conjecture,
true = ifeq2(of(skc5,X0,X1),true,of(skc6,X0,X1),true) ).
cnf(u1892,negated_conjecture,
true = thing(skc6,skc7) ).
cnf(u204,negated_conjecture,
true = ifeq2(think_believe_consider(skc5,X0),true,think_believe_consider(skc6,X0),true) ).
cnf(u552,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(forename(X0,skc8),true,true,true),true) ).
cnf(u1803,negated_conjecture,
true = ifeq2(specific(skc5,skf1(X0)),true,true,true) ).
cnf(u559,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,forename(X0,skc8),true) ).
cnf(u1901,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc7),true) ).
cnf(u167,negated_conjecture,
ifeq3(of(skc5,skc8,X0),true,ifeq3(of(skc5,X1,X0),true,ifeq3(forename(skc5,X1),true,ifeq3(entity(skc5,X0),true,skc8,X1),X1),X1),X1) = X1 ).
cnf(u984,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skf1(skc9),X2),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u123,negated_conjecture,
true = actual_world(skc5) ).
cnf(u447,negated_conjecture,
true = ifeq2(impartial(skc5,X0),true,impartial(skc6,X0),true) ).
cnf(u1849,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc7),true,true,true),true) ).
cnf(u510,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,human_person(X0,skc9),true) ).
cnf(u125,negated_conjecture,
true = man(skc5,skc9) ).
cnf(u147,negated_conjecture,
true = ifeq2(man(skc6,X0),true,smoke(skc6,skf1(X1)),true) ).
cnf(u757,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,of(X0,skc8,skc9),true) ).
cnf(u1334,negated_conjecture,
b = ifeq(tuple(true,nonhuman(skc5,skc9)),tuple(true,true),a,b) ).
cnf(u119,axiom,
true = ifeq2(of(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,of(X3,X1,X2),true),true) ).
cnf(u1343,negated_conjecture,
true = ifeq2(relname(skc6,skc6),true,true,true) ).
cnf(u528,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,eventuality(X0,skc7),true) ).
cnf(u149,negated_conjecture,
true = ifeq2(man(skc6,X0),true,present(skc6,skf1(X1)),true) ).
cnf(u2083,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1589,negated_conjecture,
true = living(skc5,skc9) ).
cnf(u457,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,human_person(X0,skc9),true) ).
cnf(u1791,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skc7),true) ).
cnf(u1863,negated_conjecture,
true = ifeq2(unisex(skc5,skf1(X0)),true,true,true) ).
cnf(u105,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonhuman(X0,X2),true,nonhuman(X1,X2),true),true) ).
cnf(u143,negated_conjecture,
true = agent(skc5,skc7,skc9) ).
cnf(u188,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,of(X0,skc8,skc9),true) ).
cnf(u451,negated_conjecture,
true = ifeq2(entity(skc5,X0),true,entity(skc6,X0),true) ).
cnf(u99,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(proposition(X0,X2),true,proposition(X1,X2),true),true) ).
cnf(u1764,negated_conjecture,
b = ifeq(tuple(true,existent(skc5,skc7)),tuple(true,true),a,b) ).
cnf(u129,negated_conjecture,
true = vincent_forename(skc5,skc8) ).
cnf(u1796,negated_conjecture,
true = ifeq2(entity(skc5,skc7),true,true,true) ).
cnf(u453,negated_conjecture,
true = human_person(skc5,skc9) ).
cnf(u179,negated_conjecture,
true = ifeq2(agent(X0,skc7,skc9),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u101,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relation(X0,X2),true,relation(X1,X2),true),true) ).
cnf(u182,negated_conjecture,
true = ifeq2(of(X0,skc8,skc9),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u292,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0) = X0 ).
cnf(u720,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,event(X0,skf1(X1)),true) ).
cnf(u1797,negated_conjecture,
b = ifeq(tuple(true,general(skc5,skc7)),tuple(true,true),a,b) ).
cnf(u1216,negated_conjecture,
true = general(skc6,skc6) ).
cnf(u57,axiom,
true = ifeq2(vincent_forename(X0,X1),true,forename(X0,X1),true) ).
cnf(u2303,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,skc6,skc6),skc6) ).
cnf(u1376,negated_conjecture,
true = general(skc5,skc8) ).
cnf(u474,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,event(X0,skc7),true) ).
cnf(u1241,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,nonhuman(X0,skc6),true) ).
cnf(u51,axiom,
true = ifeq2(abstraction(X0,X1),true,unisex(X0,X1),true) ).
cnf(u1767,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,nonexistent(X0,skc7),true) ).
cnf(u2534,negated_conjecture,
skc8 = ifeq3(of(skc6,skc8,X0),true,ifeq3(of(skc6,skc8,X0),true,ifeq3(entity(skc6,X0),true,skc8,skc8),skc8),skc8) ).
cnf(u81,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(organism(X0,X2),true,organism(X1,X2),true),true) ).
cnf(u714,negated_conjecture,
true = ifeq2(event(skc5,skf1(X0)),true,true,true) ).
cnf(u1707,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc9),true) ).
cnf(u2085,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(u53,axiom,
true = ifeq2(forename(X0,X1),true,relname(X0,X1),true) ).
cnf(u716,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(event(X0,skf1(X1)),true,true,true),true) ).
cnf(u511,negated_conjecture,
true = ifeq2(smoke(skc5,skf1(X0)),true,true,true) ).
cnf(u1567,negated_conjecture,
ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,skc8,X0),X0) = X0 ).
cnf(u1522,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(animate(X0,skc9),true,true,true),true) ).
cnf(u980,negated_conjecture,
true = ifeq2(agent(X0,skf1(skc9),skc9),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u47,axiom,
true = ifeq2(abstraction(X0,X1),true,nonhuman(X0,X1),true) ).
cnf(u1350,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(relation(X0,skc8),true,true,true),true) ).
cnf(u1712,negated_conjecture,
true = ifeq2(abstraction(skc6,skc9),true,true,true) ).
cnf(u1847,negated_conjecture,
true = ifeq2(abstraction(skc6,skc7),true,true,true) ).
cnf(u471,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(event(X0,skc7),true,true,true),true) ).
cnf(u1322,negated_conjecture,
true = human(skc6,skc9) ).
cnf(u1455,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,abstraction(X0,skc8),true) ).
cnf(u1352,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relation(X0,skc8),true) ).
cnf(u1117,negated_conjecture,
skc8 = ifeq3(entity(skc6,skc9),true,skc8,skc8) ).
cnf(u1692,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc9),true) ).
cnf(u1504,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(organism(X0,skc9),true,true,true),true) ).
cnf(u1302,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc6),true,true,true),true) ).
cnf(u1865,negated_conjecture,
true = ifeq2(abstraction(skc6,skf1(X0)),true,true,true) ).
cnf(u1407,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc8),true),tuple(true,true),a,b) ).
cnf(u1304,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc6),true) ).
cnf(u1100,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0) = X0 ).
cnf(u617,negated_conjecture,
true = ifeq2(agent(X0,skc7,skc9),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u1702,negated_conjecture,
true = singleton(skc6,skc9) ).
cnf(u1910,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skf1(X1)),true,true,true),true) ).
cnf(u1266,negated_conjecture,
true = singleton(skc5,skc6) ).
cnf(u490,negated_conjecture,
true = male(skc6,skc9) ).
cnf(u1265,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc6),true) ).
cnf(u549,negated_conjecture,
true = forename(skc6,skc8) ).
cnf(u1690,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc9),true,true,true),true) ).
cnf(u1930,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc7),true) ).
cnf(u1271,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc6),true,true,true),true) ).
cnf(u492,negated_conjecture,
true = smoke(skc6,skf1(X0)) ).
cnf(u1415,negated_conjecture,
b = ifeq(tuple(human(skc6,skc8),true),tuple(true,true),a,b) ).
cnf(u127,negated_conjecture,
true = forename(skc5,skc8) ).
cnf(u524,negated_conjecture,
true = eventuality(skc5,skc7) ).
cnf(u1373,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(abstraction(X0,skc8),true,true,true),true) ).
cnf(u515,negated_conjecture,
true = relname(skc5,skc8) ).
cnf(u1391,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc8),true),tuple(true,true),a,b) ).
cnf(u1090,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1) = X1 ).
cnf(u2187,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skf1(skc9),X1),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0) = X0 ).
cnf(u1089,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0) = X0 ).
cnf(u1204,negated_conjecture,
true = abstraction(skc6,skc6) ).
cnf(u1323,negated_conjecture,
true = human(skc5,skc9) ).
cnf(u639,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(proposition(X0,skc6),true,true,true),true) ).
cnf(u565,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relname(X0,skc8),true) ).
cnf(u1326,negated_conjecture,
b = ifeq(tuple(true,nonhuman(skc6,skc9)),tuple(true,true),a,b) ).
cnf(u247,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(man(X0,skc9),true,true,true),true) ).
cnf(u438,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(male(X0,skc9),true,true,true),true) ).
cnf(u75,axiom,
true = ifeq2(present(X0,X1),true,ifeq2(accessible_world(X0,X2),true,present(X2,X1),true),true) ).
cnf(u628,negated_conjecture,
true = present(skc6,skc7) ).
cnf(u1646,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,specific(X0,skc9),true) ).
cnf(u1335,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(human(X0,skc9),true,true,true),true) ).
cnf(u1349,negated_conjecture,
true = ifeq2(proposition(skc6,skc8),true,true,true) ).
cnf(u619,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,agent(X0,skc7,skc9),true) ).
cnf(u462,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(relation(X0,skc6),true,true,true),true) ).
cnf(u77,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(man(X0,X2),true,man(X1,X2),true),true) ).
cnf(u33,axiom,
true = ifeq2(organism(X0,X1),true,living(X0,X1),true) ).
cnf(u445,negated_conjecture,
true = ifeq2(animate(skc5,X0),true,animate(skc6,X0),true) ).
cnf(u71,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(nonexistent(X0,X2),true,nonexistent(X1,X2),true),true) ).
cnf(u404,negated_conjecture,
true = agent(skc6,skc7,skc9) ).
cnf(u27,axiom,
true = ifeq2(entity(X0,X1),true,specific(X0,X1),true) ).
cnf(u216,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,event(X0,skc7),true) ).
cnf(u1626,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,existent(X0,skc9),true) ).
cnf(u1683,negated_conjecture,
true = ifeq2(entity(skc6,skc8),true,true,true) ).
cnf(u414,negated_conjecture,
true = ifeq2(specific(skc5,X0),true,specific(skc6,X0),true) ).
cnf(u29,axiom,
true = ifeq2(entity(X0,X1),true,existent(X0,X1),true) ).
cnf(u1294,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonhuman(X0,skc6),true,true,true),true) ).
cnf(u1920,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc7),true,true,true),true) ).
cnf(u157,axiom,
b = ifeq(tuple(specific(X0,X1),general(X0,X1)),tuple(true,true),a,b) ).
cnf(u1773,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonexistent(X0,skf1(X1)),true,true,true),true) ).
cnf(u400,negated_conjecture,
true = ifeq2(relname(skc5,X0),true,relname(skc6,X0),true) ).
cnf(u23,axiom,
true = ifeq2(organism(X0,X1),true,entity(X0,X1),true) ).
cnf(u560,negated_conjecture,
true = relname(skc6,skc8) ).
cnf(u181,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,agent(X0,skc7,skc9),true) ).
cnf(u203,negated_conjecture,
true = ifeq2(think_believe_consider(X0,skc7),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u531,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(eventuality(X0,skc7),true,true,true),true) ).
cnf(u1644,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skc9),true,true,true),true) ).
cnf(u9,axiom,
true = ifeq2(eventuality(X0,X1),true,thing(X0,X1),true) ).
cnf(u642,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,X0,X3),true,ifeq3(agent(skc6,X1,X3),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,skc6),skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u1635,negated_conjecture,
b = ifeq(tuple(true,general(skc5,skc9)),tuple(true,true),a,b) ).
cnf(u1273,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,singleton(X0,skc6),true) ).
cnf(u1770,negated_conjecture,
true = ifeq2(nonexistent(skc5,skf1(X0)),true,true,true) ).
cnf(u641,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,proposition(X0,skc6),true) ).
cnf(goal,negated_conjecture,
a != b ).
cnf(u176,negated_conjecture,
true = ifeq2(theme(skc5,X0,X1),true,theme(skc6,X0,X1),true) ).
cnf(ifeq_axiom_002,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u161,axiom,
b = ifeq(tuple(nonexistent(X0,X1),existent(X0,X1)),tuple(true,true),a,b) ).
cnf(u1246,negated_conjecture,
b = ifeq(tuple(specific(skc5,skc6),true),tuple(true,true),a,b) ).
cnf(u5,axiom,
true = ifeq2(smoke(X0,X1),true,event(X0,X1),true) ).
cnf(u1787,negated_conjecture,
true = ifeq2(entity(skc6,skc7),true,true,true) ).
cnf(u1681,negated_conjecture,
true = ifeq2(entity(skc6,skc6),true,true,true) ).
cnf(u1288,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc6),true) ).
cnf(u283,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,X0,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u1436,negated_conjecture,
true = singleton(skc6,skc8) ).
cnf(u2673,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0) = X0 ).
cnf(clause63,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(u479,negated_conjecture,
true = man(skc6,skc9) ).
cnf(u594,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,vincent_forename(X0,skc8),true) ).
cnf(u285,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,skc6,X1),X1),X1),X1) = X1 ).
cnf(u1255,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(unisex(X0,skc6),true,true,true),true) ).
cnf(u1784,negated_conjecture,
true = specific(skc5,skc7) ).
cnf(u85,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(existent(X0,X2),true,existent(X1,X2),true),true) ).
cnf(u113,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(vincent_forename(X0,X2),true,vincent_forename(X1,X2),true),true) ).
cnf(u1535,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,impartial(X0,skc9),true) ).
cnf(u1611,negated_conjecture,
true = existent(skc6,skc9) ).
cnf(u1228,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(abstraction(X0,skc6),true,true,true),true) ).
cnf(u590,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(vincent_forename(X0,skc8),true,true,true),true) ).
cnf(u1772,negated_conjecture,
b = ifeq(tuple(true,existent(skc6,skf1(X0))),tuple(true,true),a,b) ).
cnf(u1953,negated_conjecture,
skc6 = ifeq3(theme(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6) ).
cnf(u1426,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,thing(X0,skc8),true) ).
cnf(u1805,negated_conjecture,
true = ifeq2(entity(skc6,skf1(X0)),true,true,true) ).
cnf(u1499,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,organism(X0,skc9),true) ).
cnf(u259,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,X1,X2),true,ifeq3(agent(skc5,X0,X3),true,ifeq3(agent(skc5,X1,X3),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X2),true,X2,skc6),skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u1392,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(general(X0,skc8),true,true,true),true) ).
cnf(u321,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u1359,negated_conjecture,
true = ifeq2(proposition(skc5,skc8),true,true,true) ).
cnf(u261,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,X2),true,ifeq3(agent(skc5,skc7,X3),true,ifeq3(agent(skc5,X1,X3),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1231,negated_conjecture,
true = general(skc5,skc6) ).
cnf(u1858,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(unisex(X0,skc7),true,true,true),true) ).
cnf(u1782,negated_conjecture,
true = specific(skc6,skf1(X0)) ).
cnf(u542,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,think_believe_consider(X0,skc7),true) ).
cnf(u1218,negated_conjecture,
true = thing(skc6,skc6) ).
cnf(u1345,negated_conjecture,
true = relation(skc5,skc8) ).
cnf(u1781,negated_conjecture,
true = ifeq2(eventuality(skc6,skc9),true,true,true) ).
cnf(u1843,negated_conjecture,
true = unisex(skc6,skc7) ).
cnf(u1217,negated_conjecture,
true = nonhuman(skc6,skc6) ).
cnf(u3336,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1408,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(general(X0,skc8),true,true,true),true) ).
cnf(u1464,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc8),true,true,true),true) ).
cnf(u1173,negated_conjecture,
b = ifeq(tuple(unisex(skc6,skc9),true),tuple(true,true),a,b) ).
cnf(u1568,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,X0,skc8),skc8) ).
cnf(u1497,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(organism(X0,skc9),true,true,true),true) ).
cnf(u734,negated_conjecture,
true = ifeq2(accessible_world(skc6,skc5),true,true,true) ).
cnf(u1311,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc6),true,true,true),true) ).
cnf(u1296,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,nonhuman(X0,skc6),true) ).
cnf(u1624,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(existent(X0,skc9),true,true,true),true) ).
cnf(u845,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(proposition(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u394,negated_conjecture,
true = ifeq2(abstraction(skc5,X0),true,abstraction(skc6,X0),true) ).
cnf(u206,negated_conjecture,
true = ifeq2(theme(X0,skc7,skc6),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u1806,negated_conjecture,
b = ifeq(tuple(true,general(skc6,skf1(X0))),tuple(true,true),a,b) ).
cnf(u205,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,think_believe_consider(X0,skc7),true) ).
cnf(u1275,negated_conjecture,
true = singleton(skc6,skc6) ).
cnf(u192,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,skc9),true,X0,skc8),skc8),skc8) ).
cnf(u768,negated_conjecture,
true = ifeq2(theme(X0,skc7,skc6),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u352,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6) ).
cnf(u199,negated_conjecture,
skc8 = ifeq3(entity(skc5,skc9),true,skc8,skc8) ).
cnf(u1172,negated_conjecture,
b = ifeq(tuple(unisex(skc5,skc9),true),tuple(true,true),a,b) ).
cnf(u1427,negated_conjecture,
true = singleton(skc5,skc8) ).
cnf(u1905,negated_conjecture,
true = ifeq2(thing(skc5,skf1(X0)),true,true,true) ).
cnf(u1579,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(entity(X0,skc9),true,true,true),true) ).
cnf(u155,axiom,
b = ifeq(tuple(unisex(X0,X1),male(X0,X1)),tuple(true,true),a,b) ).
cnf(u1557,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(entity(X0,skc9),true,true,true),true) ).
cnf(u1838,negated_conjecture,
true = ifeq2(eventuality(skc5,skc6),true,true,true) ).
cnf(u504,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(male(X0,skc9),true,true,true),true) ).
cnf(u79,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(human_person(X0,X2),true,human_person(X1,X2),true),true) ).
cnf(u536,negated_conjecture,
true = think_believe_consider(skc6,skc7) ).
cnf(u1753,negated_conjecture,
true = nonexistent(skc5,skc7) ).
cnf(u434,negated_conjecture,
true = ifeq2(eventuality(skc5,X0),true,eventuality(skc6,X0),true) ).
cnf(u1618,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,existent(X0,skc9),true) ).
cnf(u543,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,skc7,X3),true,ifeq3(agent(skc6,X1,X3),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,X2,X0),X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u498,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(smoke(X0,skf1(X1)),true,true,true),true) ).
cnf(u1716,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,thing(X0,skc9),true) ).
cnf(u151,negated_conjecture,
true = ifeq2(man(skc6,X0),true,event(skc6,skf1(X1)),true) ).
cnf(u3444,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u107,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(general(X0,X2),true,general(X1,X2),true),true) ).
cnf(u137,negated_conjecture,
true = accessible_world(skc5,skc6) ).
cnf(u328,negated_conjecture,
skc6 = ifeq3(theme(skc5,skc7,X0),true,ifeq3(proposition(skc5,X0),true,X0,skc6),skc6) ).
cnf(u523,negated_conjecture,
true = eventuality(skc6,skc7) ).
cnf(u494,negated_conjecture,
true = present(skc6,skf1(X0)) ).
cnf(u153,negated_conjecture,
true = ifeq2(man(skc6,X0),true,agent(skc6,skf1(X0),X0),true) ).
cnf(u109,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(forename(X0,X2),true,forename(X1,X2),true),true) ).
cnf(u131,negated_conjecture,
true = event(skc5,skc7) ).
cnf(u455,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(human_person(X0,skc9),true,true,true),true) ).
cnf(u1956,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6) ).
cnf(u103,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(abstraction(X0,X2),true,abstraction(X1,X2),true),true) ).
cnf(u294,negated_conjecture,
skc6 = ifeq3(agent(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X0),true,skc6,skc6),skc6) ).
cnf(u133,negated_conjecture,
true = present(skc5,skc7) ).
cnf(u643,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,X2,skc6),true,ifeq3(agent(skc6,X0,X3),true,ifeq3(agent(skc6,X2,X3),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,X2),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u59,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(smoke(X0,X2),true,smoke(X1,X2),true),true) ).
cnf(u248,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,man(X0,skc9),true) ).
cnf(u1257,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,unisex(X0,skc6),true) ).
cnf(u89,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(living(X0,X2),true,living(X1,X2),true),true) ).
cnf(u1848,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skc7)),tuple(true,true),a,b) ).
cnf(u721,negated_conjecture,
true = eventuality(skc6,skf1(X0)) ).
cnf(u61,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(event(X0,X2),true,event(X1,X2),true),true) ).
cnf(u242,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(forename(X0,skc8),true,true,true),true) ).
cnf(u83,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(entity(X0,X2),true,entity(X1,X2),true),true) ).
cnf(u1530,negated_conjecture,
true = impartial(skc6,skc9) ).
cnf(u432,negated_conjecture,
true = ifeq2(human_person(skc5,X0),true,human_person(skc6,X0),true) ).
cnf(u1891,negated_conjecture,
true = thing(skc6,skf1(X0)) ).
cnf(u55,axiom,
true = ifeq2(relname(X0,X1),true,relation(X0,X1),true) ).
cnf(u244,negated_conjecture,
true = ifeq2(forename(skc5,X0),true,forename(skc6,X0),true) ).
cnf(u363,negated_conjecture,
skc6 = ifeq3(theme(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,X0,skc6),skc6),skc6),skc6) ).
cnf(u172,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,present(X0,skc7),true) ).
cnf(u276,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,skc6,X1),X1),X1),X1),X1) = X1 ).
cnf(u1548,negated_conjecture,
true = entity(skc6,skc9) ).
cnf(u665,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,relation(X0,skc6),true) ).
cnf(u41,axiom,
true = ifeq2(proposition(X0,X1),true,relation(X0,X1),true) ).
cnf(u1383,negated_conjecture,
b = ifeq(tuple(human(skc5,skc8),true),tuple(true,true),a,b) ).
cnf(u1360,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(relation(X0,skc8),true,true,true),true) ).
cnf(u270,negated_conjecture,
ifeq3(theme(skc5,X0,X1),true,ifeq3(theme(skc5,skc7,X2),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,ifeq3(proposition(skc5,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u35,axiom,
true = ifeq2(human_person(X0,X1),true,human(X0,X1),true) ).
cnf(u1751,negated_conjecture,
true = nonexistent(skc6,skf1(X0)) ).
cnf(u65,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(thing(X0,X2),true,thing(X1,X2),true),true) ).
cnf(u1278,negated_conjecture,
b = ifeq(tuple(specific(skc6,skc6),true),tuple(true,true),a,b) ).
cnf(u1512,negated_conjecture,
true = animate(skc5,skc9) ).
cnf(u37,axiom,
true = ifeq2(human_person(X0,X1),true,animate(X0,X1),true) ).
cnf(u3404,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,skf1(skc9),X1),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1944,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skf1(X1)),true) ).
cnf(u1928,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc7),true,true,true),true) ).
cnf(u1473,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc8),true) ).
cnf(u1506,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,organism(X0,skc9),true) ).
cnf(u626,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u964,negated_conjecture,
true = ifeq2(eventuality(skc5,skf1(X0)),true,true,true) ).
cnf(u31,axiom,
true = ifeq2(organism(X0,X1),true,impartial(X0,X1),true) ).
cnf(u2095,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,skc7,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,X0),X0),X0),X0) = X0 ).
cnf(u625,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,X2),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,ifeq3(proposition(skc6,X2),true,X2,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1442,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skc8),true,true,true),true) ).
cnf(u1698,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(singleton(X0,skc9),true,true,true),true) ).
cnf(u3262,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,X0,X1),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u17,axiom,
true = ifeq2(eventuality(X0,X1),true,unisex(X0,X1),true) ).
cnf(u1102,negated_conjecture,
skc6 = ifeq3(agent(skc6,skc7,X0),true,ifeq3(agent(skc6,skc7,X0),true,skc6,skc6),skc6) ).
cnf(u2184,negated_conjecture,
ifeq3(theme(skc6,skc7,X0),true,ifeq3(theme(skc6,X1,skc6),true,ifeq3(agent(skc6,X1,skc9),true,ifeq3(think_believe_consider(skc6,X1),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0) = X0 ).
cnf(u341,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,skc6),true,ifeq3(agent(skc5,X1,skc9),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0),X0),X0),X0) = X0 ).
cnf(u1867,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(unisex(X0,skf1(X1)),true,true,true),true) ).
cnf(u1254,negated_conjecture,
b = ifeq(tuple(true,male(skc5,skc6)),tuple(true,true),a,b) ).
cnf(u1286,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skc6),true,true,true),true) ).
cnf(u1444,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc8),true) ).
cnf(u3536,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1310,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skc6)),tuple(true,true),a,b) ).
cnf(u1097,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0) = X0 ).
cnf(u1533,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(impartial(X0,skc9),true,true,true),true) ).
cnf(u1595,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,living(X0,skc9),true) ).
cnf(u1263,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(thing(X0,skc6),true,true,true),true) ).
cnf(u1952,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(agent(skc6,skc7,X1),true,ifeq3(agent(skc6,X0,X1),true,ifeq3(think_believe_consider(skc6,X0),true,skc6,skc6),skc6),skc6),skc6) ).
cnf(u284,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(agent(skc5,skc7,X1),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0),X0),X0) = X0 ).
cnf(u1807,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skf1(X1)),true,true,true),true) ).
cnf(u770,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,theme(X0,skc7,skc6),true) ).
cnf(u1377,negated_conjecture,
true = nonhuman(skc5,skc8) ).
cnf(u1685,negated_conjecture,
true = thing(skc5,skc9) ).
cnf(u1249,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,general(X0,skc6),true) ).
cnf(u868,negated_conjecture,
ifeq3(theme(skc5,skc7,X0),true,ifeq3(theme(skc5,X1,skc6),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(agent(skc5,X1,X2),true,ifeq3(think_believe_consider(skc5,X1),true,ifeq3(proposition(skc5,X0),true,skc6,X0),X0),X0),X0),X0),X0) = X0 ).
cnf(u1205,negated_conjecture,
true = abstraction(skc5,skc6) ).
cnf(u1396,negated_conjecture,
true = general(skc6,skc8) ).
cnf(u1529,negated_conjecture,
true = impartial(skc5,skc9) ).
cnf(u1899,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(thing(X0,skc7),true,true,true),true) ).
cnf(u1400,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(unisex(X0,skc8),true,true,true),true) ).
cnf(u554,negated_conjecture,
true = ifeq2(vincent_forename(skc6,skc8),true,true,true) ).
cnf(u1682,negated_conjecture,
true = ifeq2(entity(skc5,skc8),true,true,true) ).
cnf(u533,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,eventuality(X0,skc7),true) ).
cnf(u410,negated_conjecture,
true = ifeq2(unisex(skc5,X0),true,unisex(skc6,X0),true) ).
cnf(u1842,negated_conjecture,
true = unisex(skc6,skf1(X0)) ).
cnf(u1638,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,specific(X0,skc9),true) ).
cnf(u235,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(vincent_forename(X0,skc8),true,true,true),true) ).
cnf(u1329,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,human(X0,skc9),true) ).
cnf(u660,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,present(X0,skc7),true) ).
cnf(u3094,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X1),true,skc6,X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u1961,negated_conjecture,
skc6 = ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6),skc6) ).
cnf(u430,negated_conjecture,
true = ifeq2(nonexistent(skc5,X0),true,nonexistent(skc6,X0),true) ).
cnf(u1866,negated_conjecture,
b = ifeq(tuple(true,male(skc6,skf1(X0))),tuple(true,true),a,b) ).
cnf(u237,negated_conjecture,
true = ifeq2(vincent_forename(skc5,X0),true,vincent_forename(skc6,X0),true) ).
cnf(u1942,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(singleton(X0,skf1(X1)),true,true,true),true) ).
cnf(u1493,negated_conjecture,
true = organism(skc6,skc9) ).
cnf(u1353,negated_conjecture,
true = abstraction(skc6,skc8) ).
cnf(u1789,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(specific(X0,skc7),true,true,true),true) ).
cnf(u1851,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skc7),true) ).
cnf(u844,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(theme(skc5,skc7,X1),true,ifeq3(agent(skc5,X0,X2),true,ifeq3(agent(skc5,skc7,X2),true,ifeq3(think_believe_consider(skc5,X0),true,ifeq3(proposition(skc5,X1),true,X1,skc6),skc6),skc6),skc6),skc6),skc6) ).
cnf(u1342,negated_conjecture,
true = ifeq2(relname(skc5,skc6),true,true,true) ).
cnf(u1429,negated_conjecture,
true = thing(skc6,skc8) ).
cnf(u1590,negated_conjecture,
true = living(skc6,skc9) ).
cnf(u396,negated_conjecture,
true = ifeq2(relation(skc5,X0),true,relation(skc6,X0),true) ).
cnf(u97,axiom,
true = ifeq2(think_believe_consider(X0,X1),true,ifeq2(accessible_world(X0,X2),true,think_believe_consider(X2,X1),true),true) ).
cnf(u1688,negated_conjecture,
true = ifeq2(abstraction(skc5,skc9),true,true,true) ).
cnf(u378,negated_conjecture,
skc6 = ifeq3(theme(skc5,X0,skc6),true,ifeq3(agent(skc5,X0,skc9),true,ifeq3(think_believe_consider(skc5,X0),true,skc6,skc6),skc6),skc6) ).
cnf(u217,negated_conjecture,
true = ifeq2(event(skc5,X0),true,event(skc6,X0),true) ).
cnf(u408,negated_conjecture,
true = ifeq2(human(skc5,X0),true,human(skc6,X0),true) ).
cnf(u1540,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(impartial(X0,skc9),true,true,true),true) ).
cnf(u1913,negated_conjecture,
true = singleton(skc6,skf1(X0)) ).
cnf(u220,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(proposition(X0,skc6),true,true,true),true) ).
cnf(u568,negated_conjecture,
true = theme(skc6,skc7,skc6) ).
cnf(u497,negated_conjecture,
true = ifeq2(man(skc6,X0),true,true,true) ).
cnf(u402,negated_conjecture,
true = ifeq2(male(skc5,X0),true,male(skc6,X0),true) ).
cnf(u392,negated_conjecture,
true = ifeq2(general(skc5,X0),true,general(skc6,X0),true) ).
cnf(u1857,negated_conjecture,
b = ifeq(tuple(true,male(skc5,skc7)),tuple(true,true),a,b) ).
cnf(u1586,negated_conjecture,
ifeq3(of(skc6,X0,skc9),true,ifeq3(forename(skc6,X0),true,skc8,X0),X0) = X0 ).
cnf(u1937,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,singleton(X0,skc7),true) ).
cnf(u491,negated_conjecture,
true = human_person(skc6,skc9) ).
cnf(u170,negated_conjecture,
true = ifeq2(present(X0,skc7),true,ifeq2(accessible_world(X0,skc5),true,true,true),true) ).
cnf(u11,axiom,
true = ifeq2(thing(X0,X1),true,singleton(X0,X1),true) ).
cnf(u907,negated_conjecture,
true = ifeq2(present(X0,skf1(X1)),true,ifeq2(accessible_world(X0,skc6),true,true,true),true) ).
cnf(u493,negated_conjecture,
true = event(skc6,skf1(X0)) ).
cnf(u398,negated_conjecture,
true = ifeq2(thing(skc5,X0),true,thing(skc6,X0),true) ).
cnf(u13,axiom,
true = ifeq2(eventuality(X0,X1),true,specific(X0,X1),true) ).
cnf(u163,negated_conjecture,
true = ifeq2(smoke(skc5,skc7),true,true,true) ).
cnf(u1378,negated_conjecture,
true = thing(skc5,skc8) ).
cnf(u487,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(man(X0,skc9),true,true,true),true) ).
cnf(u166,negated_conjecture,
skc8 = ifeq3(of(skc5,X0,X1),true,ifeq3(of(skc5,skc8,X1),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,X1),true,X0,skc8),skc8),skc8),skc8) ).
cnf(u7,axiom,
true = ifeq2(event(X0,X1),true,eventuality(X0,X1),true) ).
cnf(u544,negated_conjecture,
ifeq3(theme(skc6,X0,X1),true,ifeq3(theme(skc6,skc7,X2),true,ifeq3(agent(skc6,X0,X3),true,ifeq3(agent(skc6,skc7,X3),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(proposition(skc6,X1),true,ifeq3(proposition(skc6,X2),true,X2,X1),X1),X1),X1),X1),X1),X1) = X1 ).
cnf(u443,negated_conjecture,
true = ifeq2(living(skc5,X0),true,living(skc6,X0),true) ).
cnf(u473,negated_conjecture,
true = ifeq2(smoke(skc6,skc7),true,true,true) ).
cnf(clause64,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(u1757,negated_conjecture,
true = ifeq2(accessible_world(X0,skc6),true,ifeq2(nonexistent(X0,skc7),true,true,true),true) ).
cnf(u159,axiom,
b = ifeq(tuple(human(X0,X1),nonhuman(X0,X1)),tuple(true,true),a,b) ).
cnf(u3334,negated_conjecture,
skc6 = ifeq3(theme(skc6,X0,skc6),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(agent(skc6,X0,skc9),true,ifeq3(think_believe_consider(skc6,X0),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,skc6,skc6),skc6),skc6),skc6),skc6) ).
cnf(u1869,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,unisex(X0,skf1(X1)),true) ).
cnf(u115,axiom,
true = ifeq2(agent(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,agent(X3,X1,X2),true),true) ).
cnf(u982,negated_conjecture,
true = ifeq2(accessible_world(skc6,X0),true,agent(X0,skf1(skc9),skc9),true) ).
cnf(u145,negated_conjecture,
true = theme(skc5,skc7,skc6) ).
cnf(u1230,negated_conjecture,
true = unisex(skc5,skc6) ).
cnf(u3466,negated_conjecture,
ifeq3(theme(skc6,skf1(skc9),X0),true,ifeq3(theme(skc6,skf1(skc9),skc6),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(think_believe_consider(skc6,skf1(skc9)),true,ifeq3(proposition(skc6,X0),true,skc6,X0),X0),X0),X0),X0) = X0 ).
cnf(u469,negated_conjecture,
true = event(skc6,skc7) ).
cnf(u1841,negated_conjecture,
true = ifeq2(eventuality(skc6,skc8),true,true,true) ).
cnf(u1229,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,abstraction(X0,skc6),true) ).
cnf(u117,axiom,
true = ifeq2(theme(X0,X1,X2),true,ifeq2(accessible_world(X0,X3),true,theme(X3,X1,X2),true),true) ).
cnf(u1800,negated_conjecture,
true = ifeq2(accessible_world(skc5,X0),true,specific(X0,skc7),true) ).
cnf(u1631,negated_conjecture,
true = specific(skc6,skc9) ).
cnf(u1232,negated_conjecture,
true = nonhuman(skc5,skc6) ).
cnf(u191,negated_conjecture,
ifeq3(of(skc5,X0,skc9),true,ifeq3(forename(skc5,X0),true,ifeq3(entity(skc5,skc9),true,skc8,X0),X0),X0) = X0 ).
cnf(u1964,negated_conjecture,
skc6 = ifeq3(theme(skc6,skc7,X0),true,ifeq3(proposition(skc6,X0),true,X0,skc6),skc6) ).
cnf(u111,axiom,
true = ifeq2(accessible_world(X0,X1),true,ifeq2(relname(X0,X2),true,relname(X1,X2),true),true) ).
cnf(u1239,negated_conjecture,
true = ifeq2(accessible_world(X0,skc5),true,ifeq2(nonhuman(X0,skc6),true,true,true),true) ).
cnf(u906,negated_conjecture,
true = ifeq2(present(skc5,skf1(X0)),true,true,true) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP220-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 % Computer : n008.cluster.edu
% 0.12/0.42 % Model : x86_64 x86_64
% 0.12/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.42 % Memory : 8046.5625MB
% 0.12/0.42 % OS : Linux 6.8.0-71-generic
% 0.12/0.42 % CPULimit : 300
% 0.12/0.42 % WCLimit : 300
% 0.12/0.42 % DateTime : Sun Sep 27 18:31:25 UTC 2026
% 0.12/0.42 % CPUTime :
% 0.12/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.46 Running first-order theorem proving
% 0.12/0.46 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.42/1.76 % (1518108)Detected a unit-equality problem, will run specialized UEQ schedule.
% 4.42/1.76 % (1518114)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=2174300720:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 4.42/1.76 % (1518116)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1891131093:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 4.42/1.76 % (1518117)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4218910897:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 4.42/1.76 % (1518119)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3169056420:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 4.42/1.76 % (1518115)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=758701934:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 4.42/1.76 % (1518113)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=4132605911:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 4.42/1.76 % (1518118)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1167129165:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 4.42/1.76 % (1518116)Instruction limit reached!
% 4.42/1.76 % (1518116)------------------------------
% 4.42/1.76 % (1518116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.76 % (1518116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.76 % (1518116)CaDiCaL version: 2.1.3
% 4.42/1.76 % (1518116)Termination reason: Instruction limit
% 4.42/1.76 % (1518116)Termination phase: Saturation
% 4.42/1.76 % (1518116)Time elapsed: 0.066 s
% 4.42/1.76 % (1518116)Peak memory usage: 87 MB
% 4.42/1.76 % (1518116)Instructions burned: 136 (million)
% 4.42/1.76 % (1518117)Instruction limit reached!
% 4.42/1.76 % (1518117)------------------------------
% 4.42/1.76 % (1518117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.76 % (1518117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.76 % (1518117)CaDiCaL version: 2.1.3
% 4.42/1.76 % (1518117)Termination reason: Instruction limit
% 4.42/1.76 % (1518117)Termination phase: Saturation
% 4.42/1.76 % (1518117)Time elapsed: 0.106 s
% 4.42/1.76 % (1518117)Peak memory usage: 89 MB
% 4.42/1.76 % (1518117)Instructions burned: 182 (million)
% 4.42/1.76 % (1518119)Refutation not found, incomplete strategy
% 4.42/1.76 % (1518119)------------------------------
% 4.42/1.76 % (1518119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.76 % (1518119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.76 % (1518119)CaDiCaL version: 2.1.3
% 4.42/1.76 % (1518119)Termination reason: Refutation not found, incomplete strategy
% 4.42/1.76 % (1518119)Time elapsed: 0.118 s
% 4.42/1.76 % (1518119)Peak memory usage: 89 MB
% 4.42/1.76 % (1518119)Instructions burned: 204 (million)
% 4.42/1.76 % (1518118)Instruction limit reached!
% 4.42/1.76 % (1518118)------------------------------
% 4.42/1.76 % (1518118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.76 % (1518118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.76 % (1518118)CaDiCaL version: 2.1.3
% 4.42/1.76 % (1518118)Termination reason: Instruction limit
% 4.42/1.76 % (1518118)Termination phase: Saturation
% 4.42/1.76 % (1518118)Time elapsed: 0.145 s
% 4.42/1.76 % (1518118)Peak memory usage: 91 MB
% 4.42/1.76 % (1518118)Instructions burned: 258 (million)
% 4.42/1.76 % (1518127)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1961533607:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 4.42/1.76 % (1518128)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1099633274:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 4.42/1.76 % (1518129)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2525049173:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 4.42/1.76 % (1518119)------------------------------
% 4.42/1.76 % (1518119)------------------------------
% 4.42/1.76 % (1518129)Instruction limit reached!
% 4.42/1.76 % (1518129)------------------------------
% 4.42/1.76 % (1518129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.76 % (1518129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.76 % (1518129)CaDiCaL version: 2.1.3
% 4.42/1.76 % (1518129)Termination reason: Instruction limit
% 4.42/1.76 % (1518129)Termination phase: Saturation
% 4.42/1.76 % (1518129)Time elapsed: 0.108 s
% 4.42/1.76 % (1518129)Peak memory usage: 93 MB
% 4.42/1.76 % (1518129)Instructions burned: 215 (million)
% 4.42/1.76 % (1518133)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=1155548210: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.42/1.76 % (1518134)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=1776235642:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 4.42/1.76 % (1518114)First to succeed.
% 4.42/1.76 % (1518114)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1518108"
% 4.42/1.76 % (1518133)Instruction limit reached!
% 4.42/1.76 % (1518133)------------------------------
% 4.42/1.76 % (1518133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.42/1.76 % (1518133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.42/1.76 % (1518133)CaDiCaL version: 2.1.3
% 4.42/1.76 % (1518133)Termination reason: Instruction limit
% 4.42/1.76 % (1518133)Termination phase: Saturation
% 4.42/1.76 % (1518133)Time elapsed: 0.185 s
% 4.42/1.76 % (1518133)Peak memory usage: 95 MB
% 4.42/1.76 % (1518133)Instructions burned: 318 (million)
% 4.42/1.76 % SZS status Satisfiable for theBenchmark
% 4.42/1.76 % SZS output start Saturation.
% See solution above
% 6.68/1.93 % SZS output start Definitions and Model Updates.
% 6.68/1.93 % SZS output end Definitions and Model Updates.
% 6.68/1.93 % (1518114)------------------------------
% 6.68/1.93 % (1518114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.68/1.93 % (1518114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.93 % (1518114)CaDiCaL version: 2.1.3
% 6.68/1.93 % (1518114)Termination reason: Satisfiable
% 6.68/1.93 % (1518114)Time elapsed: 0.584 s
% 6.68/1.93 % (1518114)Peak memory usage: 133 MB
% 6.68/1.93 % (1518114)Instructions burned: 1541 (million)
% 6.68/1.93 % (1518114)------------------------------
% 6.68/1.93 % (1518114)------------------------------
% 6.68/1.93 % (1518108)Success in time 0.862 s
% 6.68/1.93 % Vampire exiting
%------------------------------------------------------------------------------