%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP249+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 05:29:07 EDT 2022
% Result : CounterSatisfiable 0.38s 0.56s
% Output : Saturation 0.40s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 1226)
% Comments :
%------------------------------------------------------------------------------
cnf(1557,plain,
( ~ accessible_world(skc14,u)
| ~ proposition(u,skc14)
| ~ proposition(u,v)
| ~ think_believe_consider(u,skc17)
| ~ think_believe_consider(u,w)
| ~ theme(u,w,v)
| ~ agent(u,w,x)
| ~ agent(u,skc17,x)
| equal(skc14,v) ),
inference(res,[status(thm),theory(equality)],[1435,110]),
[iquote('0:Res:1435.1,110.4')] ).
cnf(1520,plain,
( ~ accessible_world(skc14,u)
| ~ proposition(u,skc14)
| ~ proposition(u,v)
| ~ think_believe_consider(u,skc15)
| ~ think_believe_consider(u,w)
| ~ theme(u,w,v)
| ~ agent(u,w,x)
| ~ agent(u,skc15,x)
| equal(skc14,v) ),
inference(res,[status(thm),theory(equality)],[1177,110]),
[iquote('0:Res:1177.1,110.4')] ).
cnf(1494,plain,
( ~ accessible_world(skc14,u)
| ~ forename(u,v)
| ~ forename(u,skc26)
| ~ entity(u,skc25)
| ~ of(u,v,skc25)
| equal(skc26,v) ),
inference(res,[status(thm),theory(equality)],[1164,109]),
[iquote('0:Res:1164.1,109.3')] ).
cnf(1490,plain,
( ~ accessible_world(skc14,u)
| ~ forename(u,v)
| ~ forename(u,skc18)
| ~ entity(u,skc19)
| ~ of(u,v,skc19)
| equal(skc18,v) ),
inference(res,[status(thm),theory(equality)],[1157,109]),
[iquote('0:Res:1157.1,109.3')] ).
cnf(1771,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skf1(skc25),skc25) ),
inference(res,[status(thm),theory(equality)],[4,1602]),
[iquote('0:Res:4.0,1602.0')] ).
cnf(1689,plain,
( ~ proposition(skc14,skc14)
| ~ proposition(skc14,u)
| ~ think_believe_consider(skc14,skc15)
| ~ think_believe_consider(skc14,v)
| ~ theme(skc14,v,u)
| ~ agent(skc14,v,w)
| ~ agent(skc14,skc15,w)
| equal(skc14,u) ),
inference(res,[status(thm),theory(equality)],[34,816]),
[iquote('0:Res:34.0,816.0')] ).
cnf(1734,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| be(v,skc24,skc25,skc25) ),
inference(res,[status(thm),theory(equality)],[1506,108]),
[iquote('0:Res:1506.1,108.1')] ).
cnf(1556,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| theme(v,skc17,skc14) ),
inference(res,[status(thm),theory(equality)],[1435,106]),
[iquote('0:Res:1435.1,106.1')] ).
cnf(1548,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skc17,skc19) ),
inference(res,[status(thm),theory(equality)],[1223,107]),
[iquote('0:Res:1223.1,107.1')] ).
cnf(1528,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skc15,skc19) ),
inference(res,[status(thm),theory(equality)],[1208,107]),
[iquote('0:Res:1208.1,107.1')] ).
cnf(1690,plain,
( ~ proposition(skc14,skc14)
| ~ proposition(skc14,u)
| ~ think_believe_consider(skc14,skc17)
| ~ think_believe_consider(skc14,v)
| ~ theme(skc14,v,u)
| ~ agent(skc14,v,w)
| ~ agent(skc14,skc17,w)
| equal(skc14,u) ),
inference(res,[status(thm),theory(equality)],[1232,816]),
[iquote('0:Res:1232.0,816.0')] ).
cnf(1519,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| theme(v,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[1177,106]),
[iquote('0:Res:1177.1,106.1')] ).
cnf(1495,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| of(v,skc26,skc25) ),
inference(res,[status(thm),theory(equality)],[1164,105]),
[iquote('0:Res:1164.1,105.1')] ).
cnf(1491,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| of(v,skc18,skc19) ),
inference(res,[status(thm),theory(equality)],[1157,105]),
[iquote('0:Res:1157.1,105.1')] ).
cnf(1846,plain,
( ~ accessible_world(skc14,u)
| ~ proposition(u,skc21) ),
inference(res,[status(thm),theory(equality)],[214,1808]),
[iquote('0:Res:214.1,1808.0')] ).
cnf(1677,plain,
( ~ theme(skc13,u,v)
| ~ proposition(skc14,v)
| ~ think_believe_consider(skc14,u)
| ~ agent(skc14,u,w)
| ~ agent(skc14,skc17,w)
| equal(skc14,v) ),
inference(mrr,[status(thm)],[1676,24]),
[iquote('0:MRR:1676.1,24.0')] ).
cnf(1808,plain,
( ~ smoke(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[65,1741]),
[iquote('0:Res:65.1,1741.0')] ).
cnf(1783,plain,
( ~ jules_forename(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[36,1718]),
[iquote('0:Res:36.1,1718.0')] ).
cnf(1782,plain,
( ~ vincent_forename(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[37,1718]),
[iquote('0:Res:37.1,1718.0')] ).
cnf(1751,plain,
( ~ jules_forename(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[36,1699]),
[iquote('0:Res:36.1,1699.0')] ).
cnf(1661,plain,
( ~ theme(skc13,u,v)
| ~ proposition(skc14,v)
| ~ think_believe_consider(skc14,u)
| ~ agent(skc14,u,w)
| ~ agent(skc14,skc15,w)
| equal(skc14,v) ),
inference(mrr,[status(thm)],[1660,24]),
[iquote('0:MRR:1660.1,24.0')] ).
cnf(1750,plain,
( ~ vincent_forename(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[37,1699]),
[iquote('0:Res:37.1,1699.0')] ).
cnf(1744,plain,
( ~ organism(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[48,1651]),
[iquote('0:Res:48.1,1651.0')] ).
cnf(1821,plain,
( ~ accessible_world(skc13,u)
| ~ proposition(u,skc24) ),
inference(res,[status(thm),theory(equality)],[111,1742]),
[iquote('0:Res:111.1,1742.0')] ).
cnf(1742,plain,
( ~ state(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[52,1650]),
[iquote('0:Res:52.1,1650.0')] ).
cnf(1640,plain,
( ~ forename(skc14,u)
| ~ forename(skc14,skc18)
| ~ entity(skc14,skc19)
| ~ of(skc14,u,skc19)
| equal(skc18,u) ),
inference(res,[status(thm),theory(equality)],[29,795]),
[iquote('0:Res:29.0,795.0')] ).
cnf(1806,plain,
( ~ accessible_world(skc13,u)
| ~ proposition(u,skc15) ),
inference(res,[status(thm),theory(equality)],[190,1741]),
[iquote('0:Res:190.1,1741.0')] ).
cnf(1805,plain,
( ~ accessible_world(skc13,u)
| ~ proposition(u,skc17) ),
inference(res,[status(thm),theory(equality)],[200,1741]),
[iquote('0:Res:200.1,1741.0')] ).
cnf(1803,plain,
~ proposition(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[1305,1741]),
[iquote('0:Res:1305.0,1741.0')] ).
cnf(1802,plain,
~ proposition(skc14,skc21),
inference(res,[status(thm),theory(equality)],[5,1741]),
[iquote('0:Res:5.0,1741.0')] ).
cnf(1641,plain,
( ~ forename(skc14,u)
| ~ forename(skc14,skc26)
| ~ entity(skc14,skc25)
| ~ of(skc14,u,skc25)
| equal(skc26,u) ),
inference(res,[status(thm),theory(equality)],[26,795]),
[iquote('0:Res:26.0,795.0')] ).
cnf(1741,plain,
( ~ event(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[64,1650]),
[iquote('0:Res:64.1,1650.0')] ).
cnf(1736,plain,
( ~ human_person(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[49,1647]),
[iquote('0:Res:49.1,1647.0')] ).
cnf(1727,plain,
( ~ jules_forename(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[36,1622]),
[iquote('0:Res:36.1,1622.0')] ).
cnf(1726,plain,
( ~ vincent_forename(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[37,1622]),
[iquote('0:Res:37.1,1622.0')] ).
cnf(1631,plain,
( ~ of(skc13,u,skc25)
| ~ forename(skc14,u)
| ~ forename(skc14,skc26)
| ~ entity(skc14,skc25)
| equal(skc26,u) ),
inference(mrr,[status(thm)],[1630,24]),
[iquote('0:MRR:1630.1,24.0')] ).
cnf(1781,plain,
( ~ accessible_world(skc13,u)
| ~ male(u,skc18) ),
inference(res,[status(thm),theory(equality)],[204,1718]),
[iquote('0:Res:204.1,1718.0')] ).
cnf(1718,plain,
( ~ forename(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[39,1146]),
[iquote('0:Res:39.1,1146.0')] ).
cnf(1776,plain,
( ~ accessible_world(skc13,u)
| ~ proposition(u,skc19) ),
inference(res,[status(thm),theory(equality)],[217,1713]),
[iquote('0:Res:217.1,1713.0')] ).
cnf(1713,plain,
( ~ man(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[40,1145]),
[iquote('0:Res:40.1,1145.1')] ).
cnf(1602,plain,
( ~ man(skc13,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| agent(w,skf1(u),u) ),
inference(res,[status(thm),theory(equality)],[127,1438]),
[iquote('0:Res:127.1,1438.0')] ).
cnf(1765,plain,
( ~ smoke(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[65,1755]),
[iquote('0:Res:65.1,1755.0')] ).
cnf(1758,plain,
( ~ organism(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[48,1754]),
[iquote('0:Res:48.1,1754.0')] ).
cnf(1756,plain,
( ~ state(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[52,1753]),
[iquote('0:Res:52.1,1753.0')] ).
cnf(1755,plain,
( ~ event(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[64,1753]),
[iquote('0:Res:64.1,1753.0')] ).
cnf(1615,plain,
( ~ of(skc13,u,skc19)
| ~ forename(skc14,u)
| ~ entity(skc14,skc19)
| equal(skc18,u) ),
inference(mrr,[status(thm)],[1614,24]),
[iquote('0:MRR:1614.1,24.0')] ).
cnf(1754,plain,
( ~ entity(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[46,1749]),
[iquote('0:Res:46.1,1749.1')] ).
cnf(1753,plain,
( ~ eventuality(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[61,1749]),
[iquote('0:Res:61.1,1749.1')] ).
cnf(1749,plain,
( ~ accessible_world(skc13,u)
| ~ specific(u,skc18) ),
inference(res,[status(thm),theory(equality)],[204,1699]),
[iquote('0:Res:204.1,1699.0')] ).
cnf(1699,plain,
( ~ forename(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[39,1110]),
[iquote('0:Res:39.1,1110.0')] ).
cnf(1604,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skf1(skc19),skc19) ),
inference(mrr,[status(thm)],[1603,24]),
[iquote('0:MRR:1603.0,24.0')] ).
cnf(1651,plain,
( ~ entity(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[46,1109]),
[iquote('0:Res:46.1,1109.1')] ).
cnf(1650,plain,
( ~ eventuality(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[61,1109]),
[iquote('0:Res:61.1,1109.1')] ).
cnf(1647,plain,
( ~ organism(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[48,1099]),
[iquote('0:Res:48.1,1099.0')] ).
cnf(1730,plain,
( ~ man(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[50,1729]),
[iquote('0:Res:50.1,1729.0')] ).
cnf(1506,plain,
( ~ accessible_world(skc14,u)
| be(u,skc24,skc25,skc25) ),
inference(res,[status(thm),theory(equality)],[24,771]),
[iquote('0:Res:24.0,771.0')] ).
cnf(1729,plain,
( ~ human_person(u,skc18)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[42,1725]),
[iquote('0:Res:42.1,1725.1')] ).
cnf(1725,plain,
( ~ accessible_world(skc13,u)
| ~ human(u,skc18) ),
inference(res,[status(thm),theory(equality)],[204,1622]),
[iquote('0:Res:204.1,1622.0')] ).
cnf(1622,plain,
( ~ forename(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[39,1069]),
[iquote('0:Res:39.1,1069.0')] ).
cnf(1606,plain,
( ~ human_person(u,v)
| ~ proposition(u,v) ),
inference(res,[status(thm),theory(equality)],[42,1068]),
[iquote('0:Res:42.1,1068.1')] ).
cnf(1146,plain,
( ~ relname(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[38,757]),
[iquote('0:Res:38.1,757.0')] ).
cnf(1712,plain,
( ~ male(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[118,1145]),
[iquote('0:Res:118.1,1145.1')] ).
cnf(1145,plain,
( ~ proposition(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[58,757]),
[iquote('0:Res:58.1,757.0')] ).
cnf(1707,plain,
( ~ accessible_world(skc13,u)
| ~ state(u,skc19) ),
inference(res,[status(thm),theory(equality)],[217,1135]),
[iquote('0:Res:217.1,1135.0')] ).
cnf(1701,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skc21) ),
inference(res,[status(thm),theory(equality)],[214,1124]),
[iquote('0:Res:214.1,1124.0')] ).
cnf(1135,plain,
( ~ man(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[40,743]),
[iquote('0:Res:40.1,743.1')] ).
cnf(1124,plain,
( ~ smoke(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[65,742]),
[iquote('0:Res:65.1,742.0')] ).
cnf(1110,plain,
( ~ relname(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[38,726]),
[iquote('0:Res:38.1,726.0')] ).
cnf(1685,plain,
( ~ smoke(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[65,1665]),
[iquote('0:Res:65.1,1665.0')] ).
cnf(816,plain,
( ~ theme(skc13,u,v)
| ~ proposition(skc14,v)
| ~ proposition(skc14,w)
| ~ think_believe_consider(skc14,u)
| ~ think_believe_consider(skc14,x)
| ~ theme(skc14,x,w)
| ~ agent(skc14,x,y)
| ~ agent(skc14,u,y)
| equal(v,w) ),
inference(res,[status(thm),theory(equality)],[145,110]),
[iquote('0:Res:145.1,110.4')] ).
cnf(1678,plain,
( ~ organism(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[48,1653]),
[iquote('0:Res:48.1,1653.0')] ).
cnf(1666,plain,
( ~ state(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[52,1652]),
[iquote('0:Res:52.1,1652.0')] ).
cnf(1665,plain,
( ~ event(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[64,1652]),
[iquote('0:Res:64.1,1652.0')] ).
cnf(1653,plain,
( ~ entity(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[46,1649]),
[iquote('0:Res:46.1,1649.0')] ).
cnf(1411,plain,
( ~ accessible_world(skc13,u)
| ~ proposition(u,v)
| ~ think_believe_consider(u,w)
| ~ theme(u,w,v)
| ~ agent(u,w,x)
| ~ agent(u,skc17,x)
| equal(skc14,v) ),
inference(rew,[status(thm),theory(equality)],[1228,660]),
[iquote('0:Rew:1228.0,660.6')] ).
cnf(1664,plain,
~ proposition(skc14,skc24),
inference(res,[status(thm),theory(equality)],[113,1652]),
[iquote('0:Res:113.0,1652.0')] ).
cnf(1663,plain,
~ proposition(skc14,skc15),
inference(res,[status(thm),theory(equality)],[191,1652]),
[iquote('0:Res:191.0,1652.0')] ).
cnf(1662,plain,
~ proposition(skc14,skc17),
inference(res,[status(thm),theory(equality)],[201,1652]),
[iquote('0:Res:201.0,1652.0')] ).
cnf(1652,plain,
( ~ eventuality(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[61,1649]),
[iquote('0:Res:61.1,1649.0')] ).
cnf(652,plain,
( ~ accessible_world(skc13,u)
| ~ proposition(u,v)
| ~ think_believe_consider(u,w)
| ~ theme(u,w,v)
| ~ agent(u,w,x)
| ~ agent(u,skc15,x)
| equal(skc14,v) ),
inference(mrr,[status(thm)],[651,148,194]),
[iquote('0:MRR:651.1,651.3,148.1,194.1')] ).
cnf(1649,plain,
( ~ specific(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[138,1109]),
[iquote('0:Res:138.1,1109.1')] ).
cnf(1109,plain,
( ~ proposition(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[58,726]),
[iquote('0:Res:58.1,726.0')] ).
cnf(1099,plain,
( ~ entity(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[45,712]),
[iquote('0:Res:45.1,712.1')] ).
cnf(1638,plain,
( ~ man(u,skc21)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[50,1636]),
[iquote('0:Res:50.1,1636.0')] ).
cnf(795,plain,
( ~ of(skc13,u,v)
| ~ forename(skc14,w)
| ~ forename(skc14,u)
| ~ entity(skc14,v)
| ~ of(skc14,w,v)
| equal(u,w) ),
inference(res,[status(thm),theory(equality)],[144,109]),
[iquote('0:Res:144.1,109.3')] ).
cnf(1636,plain,
( ~ human_person(u,skc21)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[49,1634]),
[iquote('0:Res:49.1,1634.0')] ).
cnf(1634,plain,
( ~ organism(u,skc21)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[48,1633]),
[iquote('0:Res:48.1,1633.0')] ).
cnf(1633,plain,
( ~ entity(u,skc21)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[45,1624]),
[iquote('0:Res:45.1,1624.1')] ).
cnf(1624,plain,
( ~ accessible_world(skc14,u)
| ~ existent(u,skc21) ),
inference(res,[status(thm),theory(equality)],[214,1088]),
[iquote('0:Res:214.1,1088.0')] ).
cnf(640,plain,
( ~ accessible_world(skc13,u)
| ~ forename(u,v)
| ~ forename(u,skc26)
| ~ entity(u,skc25)
| ~ of(u,v,skc25)
| equal(skc26,v) ),
inference(res,[status(thm),theory(equality)],[545,109]),
[iquote('0:Res:545.1,109.3')] ).
cnf(1088,plain,
( ~ smoke(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[65,711]),
[iquote('0:Res:65.1,711.0')] ).
cnf(1069,plain,
( ~ relname(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[38,698]),
[iquote('0:Res:38.1,698.0')] ).
cnf(1617,plain,
~ proposition(skc14,skc25),
inference(res,[status(thm),theory(equality)],[4,1609]),
[iquote('0:Res:4.0,1609.0')] ).
cnf(1609,plain,
( ~ man(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[50,1607]),
[iquote('0:Res:50.1,1607.0')] ).
cnf(609,plain,
( ~ accessible_world(skc13,u)
| ~ forename(u,v)
| ~ entity(u,skc19)
| ~ of(u,v,skc19)
| equal(skc18,v) ),
inference(mrr,[status(thm)],[607,204]),
[iquote('0:MRR:607.2,204.1')] ).
cnf(1608,plain,
~ proposition(skc14,skc19),
inference(res,[status(thm),theory(equality)],[219,1607]),
[iquote('0:Res:219.0,1607.0')] ).
cnf(1607,plain,
( ~ human_person(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[42,1605]),
[iquote('0:Res:42.1,1605.0')] ).
cnf(1605,plain,
( ~ human(skc13,u)
| ~ proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[120,1068]),
[iquote('0:Res:120.1,1068.1')] ).
cnf(1068,plain,
( ~ proposition(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[58,698]),
[iquote('0:Res:58.1,698.0')] ).
cnf(1438,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| agent(w,skf1(u),u) ),
inference(rew,[status(thm),theory(equality)],[1228,1410]),
[iquote('0:Rew:1228.0,1410.1')] ).
cnf(1595,plain,
( ~ human_person(skc13,u)
| ~ state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[49,1571]),
[iquote('0:Res:49.1,1571.0')] ).
cnf(1590,plain,
( ~ human_person(u,skc15)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[49,1569]),
[iquote('0:Res:49.1,1569.0')] ).
cnf(1588,plain,
( ~ human_person(u,skc17)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[49,1567]),
[iquote('0:Res:49.1,1567.0')] ).
cnf(1571,plain,
( ~ organism(skc13,u)
| ~ state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[48,1476]),
[iquote('0:Res:48.1,1476.0')] ).
cnf(1418,plain,
( ~ proposition(skc13,u)
| ~ theme(skc13,skc17,u)
| ~ agent(skc13,skc17,v)
| equal(skc14,u) ),
inference(rew,[status(thm),theory(equality)],[1228,1048]),
[iquote('0:Rew:1228.0,1048.3')] ).
cnf(1569,plain,
( ~ organism(u,skc15)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[48,1475]),
[iquote('0:Res:48.1,1475.0')] ).
cnf(1567,plain,
( ~ organism(u,skc17)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[48,1472]),
[iquote('0:Res:48.1,1472.0')] ).
cnf(1503,plain,
( ~ smoke(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[65,1167]),
[iquote('0:Res:65.1,1167.0')] ).
cnf(1032,plain,
( ~ proposition(skc13,u)
| ~ theme(skc13,skc15,u)
| ~ agent(skc13,skc15,v)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[1031,23,18]),
[iquote('0:MRR:1031.0,1031.2,23.0,18.0')] ).
cnf(1579,plain,
~ state(skc13,skc25),
inference(res,[status(thm),theory(equality)],[128,1577]),
[iquote('0:Res:128.1,1577.0')] ).
cnf(1577,plain,
~ state(skc14,skc25),
inference(res,[status(thm),theory(equality)],[4,1486]),
[iquote('0:Res:4.0,1486.0')] ).
cnf(1486,plain,
( ~ man(skc13,u)
| ~ state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[40,1134]),
[iquote('0:Res:40.1,1134.0')] ).
cnf(1480,plain,
( ~ man(u,skc15)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[40,1122]),
[iquote('0:Res:40.1,1122.1')] ).
cnf(843,plain,
( ~ be(skc13,u,v,w)
| ~ accessible_world(skc14,x)
| be(x,u,v,w) ),
inference(res,[status(thm),theory(equality)],[147,108]),
[iquote('0:Res:147.1,108.1')] ).
cnf(1478,plain,
( ~ man(u,skc17)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[40,1121]),
[iquote('0:Res:40.1,1121.1')] ).
cnf(1476,plain,
( ~ entity(skc13,u)
| ~ state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[45,1098]),
[iquote('0:Res:45.1,1098.0')] ).
cnf(1475,plain,
( ~ entity(u,skc15)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[45,1086]),
[iquote('0:Res:45.1,1086.1')] ).
cnf(1472,plain,
( ~ entity(u,skc17)
| ~ accessible_world(skc13,u) ),
inference(res,[status(thm),theory(equality)],[45,1085]),
[iquote('0:Res:45.1,1085.1')] ).
cnf(829,plain,
( ~ agent(skc13,u,v)
| ~ accessible_world(skc14,w)
| agent(w,u,v) ),
inference(res,[status(thm),theory(equality)],[146,107]),
[iquote('0:Res:146.1,107.1')] ).
cnf(1435,plain,
( ~ accessible_world(skc14,u)
| theme(u,skc17,skc14) ),
inference(rew,[status(thm),theory(equality)],[1228,1428]),
[iquote('0:Rew:1228.0,1428.1')] ).
cnf(1223,plain,
( ~ accessible_world(skc14,u)
| agent(u,skc17,skc19) ),
inference(res,[status(thm),theory(equality)],[24,685]),
[iquote('0:Res:24.0,685.0')] ).
cnf(815,plain,
( ~ theme(skc13,u,v)
| ~ accessible_world(skc14,w)
| theme(w,u,v) ),
inference(res,[status(thm),theory(equality)],[145,106]),
[iquote('0:Res:145.1,106.1')] ).
cnf(1215,plain,
( ~ jules_forename(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[36,1036]),
[iquote('0:Res:36.1,1036.0')] ).
cnf(1214,plain,
( ~ vincent_forename(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[37,1036]),
[iquote('0:Res:37.1,1036.0')] ).
cnf(1208,plain,
( ~ accessible_world(skc14,u)
| agent(u,skc15,skc19) ),
inference(res,[status(thm),theory(equality)],[24,681]),
[iquote('0:Res:24.0,681.0')] ).
cnf(796,plain,
( ~ of(skc13,u,v)
| ~ accessible_world(skc14,w)
| of(w,u,v) ),
inference(res,[status(thm),theory(equality)],[144,105]),
[iquote('0:Res:144.1,105.1')] ).
cnf(1177,plain,
( ~ accessible_world(skc14,u)
| theme(u,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[24,650]),
[iquote('0:Res:24.0,650.0')] ).
cnf(1176,plain,
( ~ jules_forename(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[36,841]),
[iquote('0:Res:36.1,841.0')] ).
cnf(1175,plain,
( ~ vincent_forename(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[37,841]),
[iquote('0:Res:37.1,841.0')] ).
cnf(1170,plain,
( ~ organism(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[48,838]),
[iquote('0:Res:48.1,838.0')] ).
cnf(771,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| be(v,skc24,skc25,skc25) ),
inference(res,[status(thm),theory(equality)],[578,108]),
[iquote('0:Res:578.1,108.1')] ).
cnf(1168,plain,
( ~ state(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[52,837]),
[iquote('0:Res:52.1,837.0')] ).
cnf(1498,plain,
~ proposition(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[1305,1167]),
[iquote('0:Res:1305.0,1167.0')] ).
cnf(1497,plain,
~ proposition(skc13,skc21),
inference(res,[status(thm),theory(equality)],[5,1167]),
[iquote('0:Res:5.0,1167.0')] ).
cnf(1167,plain,
( ~ event(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[64,837]),
[iquote('0:Res:64.1,837.0')] ).
cnf(1408,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| theme(v,skc17,skc14) ),
inference(rew,[status(thm),theory(equality)],[1228,658]),
[iquote('0:Rew:1228.0,658.2')] ).
cnf(1164,plain,
( ~ accessible_world(skc14,u)
| of(u,skc26,skc25) ),
inference(res,[status(thm),theory(equality)],[24,641]),
[iquote('0:Res:24.0,641.0')] ).
cnf(1157,plain,
( ~ accessible_world(skc14,u)
| of(u,skc18,skc19) ),
inference(res,[status(thm),theory(equality)],[24,608]),
[iquote('0:Res:24.0,608.0')] ).
cnf(1485,plain,
~ state(skc14,skc19),
inference(res,[status(thm),theory(equality)],[218,1134]),
[iquote('0:Res:218.0,1134.0')] ).
cnf(1134,plain,
( ~ male(skc13,u)
| ~ state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[118,743]),
[iquote('0:Res:118.1,743.1')] ).
cnf(1392,plain,
( ~ proposition(skc13,u)
| ~ think_believe_consider(skc13,v)
| ~ theme(skc13,v,u)
| ~ agent(skc13,v,w)
| ~ agent(skc13,skc17,w)
| equal(skc14,u) ),
inference(rew,[status(thm),theory(equality)],[1228,601]),
[iquote('0:Rew:1228.0,601.5')] ).
cnf(1122,plain,
( ~ accessible_world(skc13,u)
| ~ male(u,skc15) ),
inference(res,[status(thm),theory(equality)],[190,742]),
[iquote('0:Res:190.1,742.0')] ).
cnf(1121,plain,
( ~ accessible_world(skc13,u)
| ~ male(u,skc17) ),
inference(res,[status(thm),theory(equality)],[200,742]),
[iquote('0:Res:200.1,742.0')] ).
cnf(1098,plain,
( ~ existent(skc13,u)
| ~ state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[123,712]),
[iquote('0:Res:123.1,712.1')] ).
cnf(1086,plain,
( ~ accessible_world(skc13,u)
| ~ existent(u,skc15) ),
inference(res,[status(thm),theory(equality)],[190,711]),
[iquote('0:Res:190.1,711.0')] ).
cnf(1437,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,v)
| agent(v,skf1(u),u) ),
inference(rew,[status(thm),theory(equality)],[1228,1295]),
[iquote('0:Rew:1228.0,1295.1')] ).
cnf(1085,plain,
( ~ accessible_world(skc13,u)
| ~ existent(u,skc17) ),
inference(res,[status(thm),theory(equality)],[200,711]),
[iquote('0:Res:200.1,711.0')] ).
cnf(1407,plain,
~ human_person(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,1159]),
[iquote('0:Rew:1228.0,1159.0')] ).
cnf(1406,plain,
~ organism(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,1152]),
[iquote('0:Rew:1228.0,1152.0')] ).
cnf(1405,plain,
~ man(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,1150]),
[iquote('0:Rew:1228.0,1150.0')] ).
cnf(1372,plain,
( ~ accessible_world(skc13,u)
| theme(u,skc17,skc14) ),
inference(rew,[status(thm),theory(equality)],[1228,557]),
[iquote('0:Rew:1228.0,557.1')] ).
cnf(1404,plain,
~ entity(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,1148]),
[iquote('0:Rew:1228.0,1148.0')] ).
cnf(1403,plain,
~ male(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,1125]),
[iquote('0:Rew:1228.0,1125.0')] ).
cnf(1402,plain,
~ existent(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,1089]),
[iquote('0:Rew:1228.0,1089.0')] ).
cnf(1305,plain,
event(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,230]),
[iquote('0:Rew:1228.0,230.0')] ).
cnf(1436,plain,
( ~ man(skc14,u)
| agent(skc14,skf1(u),u) ),
inference(rew,[status(thm),theory(equality)],[1228,1296]),
[iquote('0:Rew:1228.0,1296.1')] ).
cnf(1304,plain,
present(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,227]),
[iquote('0:Rew:1228.0,227.0')] ).
cnf(1303,plain,
smoke(skc14,skf1(u)),
inference(rew,[status(thm),theory(equality)],[1228,224]),
[iquote('0:Rew:1228.0,224.0')] ).
cnf(1232,plain,
theme(skc13,skc17,skc14),
inference(rew,[status(thm),theory(equality)],[1228,33]),
[iquote('0:Rew:1228.0,33.0')] ).
cnf(1228,plain,
equal(skc16,skc14),
inference(mrr,[status(thm)],[1226,31]),
[iquote('0:MRR:1226.0,31.0')] ).
cnf(1220,plain,
~ proposition(skc13,skc24),
inference(res,[status(thm),theory(equality)],[113,1041]),
[iquote('0:Res:113.0,1041.0')] ).
cnf(1219,plain,
~ proposition(skc13,skc15),
inference(res,[status(thm),theory(equality)],[191,1041]),
[iquote('0:Res:191.0,1041.0')] ).
cnf(1218,plain,
~ proposition(skc13,skc17),
inference(res,[status(thm),theory(equality)],[201,1041]),
[iquote('0:Res:201.0,1041.0')] ).
cnf(685,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| agent(v,skc17,skc19) ),
inference(res,[status(thm),theory(equality)],[569,107]),
[iquote('0:Res:569.1,107.1')] ).
cnf(1212,plain,
~ male(skc14,skc26),
inference(res,[status(thm),theory(equality)],[3,1036]),
[iquote('0:Res:3.0,1036.0')] ).
cnf(1036,plain,
( ~ forename(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[39,763]),
[iquote('0:Res:39.1,763.0')] ).
cnf(1206,plain,
~ male(skc13,skc26),
inference(res,[status(thm),theory(equality)],[160,1202]),
[iquote('0:Res:160.1,1202.0')] ).
cnf(681,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| agent(v,skc15,skc19) ),
inference(res,[status(thm),theory(equality)],[568,107]),
[iquote('0:Res:568.1,107.1')] ).
cnf(1197,plain,
~ proposition(skc13,skc25),
inference(res,[status(thm),theory(equality)],[4,962]),
[iquote('0:Res:4.0,962.0')] ).
cnf(674,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skc21,skc19) ),
inference(res,[status(thm),theory(equality)],[567,107]),
[iquote('0:Res:567.1,107.1')] ).
cnf(1189,plain,
~ smoke(skc14,skc26),
inference(res,[status(thm),theory(equality)],[65,1182]),
[iquote('0:Res:65.1,1182.0')] ).
cnf(1185,plain,
~ organism(skc14,skc26),
inference(res,[status(thm),theory(equality)],[48,1181]),
[iquote('0:Res:48.1,1181.0')] ).
cnf(1183,plain,
~ state(skc14,skc26),
inference(res,[status(thm),theory(equality)],[52,1180]),
[iquote('0:Res:52.1,1180.0')] ).
cnf(1182,plain,
~ event(skc14,skc26),
inference(res,[status(thm),theory(equality)],[64,1180]),
[iquote('0:Res:64.1,1180.0')] ).
cnf(1181,plain,
~ entity(skc14,skc26),
inference(res,[status(thm),theory(equality)],[46,1173]),
[iquote('0:Res:46.1,1173.0')] ).
cnf(1180,plain,
~ eventuality(skc14,skc26),
inference(res,[status(thm),theory(equality)],[61,1173]),
[iquote('0:Res:61.1,1173.0')] ).
cnf(1173,plain,
~ specific(skc14,skc26),
inference(res,[status(thm),theory(equality)],[3,841]),
[iquote('0:Res:3.0,841.0')] ).
cnf(650,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| theme(v,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[556,106]),
[iquote('0:Res:556.1,106.1')] ).
cnf(841,plain,
( ~ forename(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[39,614]),
[iquote('0:Res:39.1,614.0')] ).
cnf(838,plain,
( ~ entity(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[46,613]),
[iquote('0:Res:46.1,613.1')] ).
cnf(837,plain,
( ~ eventuality(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[61,613]),
[iquote('0:Res:61.1,613.1')] ).
cnf(1161,plain,
~ human_person(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[49,1156]),
[iquote('0:Res:49.1,1156.0')] ).
cnf(641,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| of(v,skc26,skc25) ),
inference(res,[status(thm),theory(equality)],[545,105]),
[iquote('0:Res:545.1,105.1')] ).
cnf(1156,plain,
~ organism(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[48,1151]),
[iquote('0:Res:48.1,1151.0')] ).
cnf(1154,plain,
~ man(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[40,1149]),
[iquote('0:Res:40.1,1149.0')] ).
cnf(608,plain,
( ~ accessible_world(skc13,u)
| ~ accessible_world(u,v)
| of(v,skc18,skc19) ),
inference(res,[status(thm),theory(equality)],[542,105]),
[iquote('0:Res:542.1,105.1')] ).
cnf(1151,plain,
~ entity(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[45,1147]),
[iquote('0:Res:45.1,1147.0')] ).
cnf(1149,plain,
~ male(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[160,1125]),
[iquote('0:Res:160.1,1125.0')] ).
cnf(969,plain,
( ~ entity(skc13,skc25)
| ~ of(skc13,skc18,skc25)
| equal(skc26,skc18) ),
inference(mrr,[status(thm)],[966,3]),
[iquote('0:MRR:966.0,3.0')] ).
cnf(1147,plain,
~ existent(skc13,skf1(u)),
inference(res,[status(thm),theory(equality)],[165,1089]),
[iquote('0:Res:165.1,1089.0')] ).
cnf(1138,plain,
~ man(skc13,skc21),
inference(res,[status(thm),theory(equality)],[40,1129]),
[iquote('0:Res:40.1,1129.0')] ).
cnf(757,plain,
( ~ relation(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[57,256]),
[iquote('0:Res:57.1,256.0')] ).
cnf(1131,plain,
~ human_person(skc13,skc21),
inference(res,[status(thm),theory(equality)],[49,1126]),
[iquote('0:Res:49.1,1126.0')] ).
cnf(1130,plain,
~ man(skc14,skc21),
inference(res,[status(thm),theory(equality)],[40,1118]),
[iquote('0:Res:40.1,1118.0')] ).
cnf(1129,plain,
~ male(skc13,skc21),
inference(res,[status(thm),theory(equality)],[118,1118]),
[iquote('0:Res:118.1,1118.0')] ).
cnf(1127,plain,
~ human_person(skc14,skc21),
inference(res,[status(thm),theory(equality)],[49,1113]),
[iquote('0:Res:49.1,1113.0')] ).
cnf(743,plain,
( ~ state(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[52,255]),
[iquote('0:Res:52.1,255.0')] ).
cnf(1126,plain,
~ organism(skc13,skc21),
inference(res,[status(thm),theory(equality)],[48,1112]),
[iquote('0:Res:48.1,1112.0')] ).
cnf(1118,plain,
~ male(skc14,skc21),
inference(res,[status(thm),theory(equality)],[5,742]),
[iquote('0:Res:5.0,742.0')] ).
cnf(1113,plain,
~ organism(skc14,skc21),
inference(res,[status(thm),theory(equality)],[48,1103]),
[iquote('0:Res:48.1,1103.0')] ).
cnf(1112,plain,
~ entity(skc13,skc21),
inference(res,[status(thm),theory(equality)],[45,1102]),
[iquote('0:Res:45.1,1102.0')] ).
cnf(742,plain,
( ~ event(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[64,255]),
[iquote('0:Res:64.1,255.0')] ).
cnf(1103,plain,
~ entity(skc14,skc21),
inference(res,[status(thm),theory(equality)],[45,1082]),
[iquote('0:Res:45.1,1082.0')] ).
cnf(1102,plain,
~ existent(skc13,skc21),
inference(res,[status(thm),theory(equality)],[123,1082]),
[iquote('0:Res:123.1,1082.0')] ).
cnf(1101,plain,
~ smoke(skc13,skc26),
inference(res,[status(thm),theory(equality)],[65,1077]),
[iquote('0:Res:65.1,1077.0')] ).
cnf(726,plain,
( ~ relation(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[57,243]),
[iquote('0:Res:57.1,243.0')] ).
cnf(1090,plain,
~ organism(skc13,skc26),
inference(res,[status(thm),theory(equality)],[48,1071]),
[iquote('0:Res:48.1,1071.0')] ).
cnf(1082,plain,
~ existent(skc14,skc21),
inference(res,[status(thm),theory(equality)],[5,711]),
[iquote('0:Res:5.0,711.0')] ).
cnf(1078,plain,
~ state(skc13,skc26),
inference(res,[status(thm),theory(equality)],[52,1070]),
[iquote('0:Res:52.1,1070.0')] ).
cnf(1077,plain,
~ event(skc13,skc26),
inference(res,[status(thm),theory(equality)],[64,1070]),
[iquote('0:Res:64.1,1070.0')] ).
cnf(712,plain,
( ~ state(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[52,236]),
[iquote('0:Res:52.1,236.0')] ).
cnf(1071,plain,
~ entity(skc13,skc26),
inference(res,[status(thm),theory(equality)],[46,1061]),
[iquote('0:Res:46.1,1061.0')] ).
cnf(711,plain,
( ~ event(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[64,236]),
[iquote('0:Res:64.1,236.0')] ).
cnf(1070,plain,
~ eventuality(skc13,skc26),
inference(res,[status(thm),theory(equality)],[61,1061]),
[iquote('0:Res:61.1,1061.0')] ).
cnf(1061,plain,
~ specific(skc13,skc26),
inference(res,[status(thm),theory(equality)],[180,1057]),
[iquote('0:Res:180.1,1057.0')] ).
cnf(698,plain,
( ~ relation(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[57,233]),
[iquote('0:Res:57.1,233.0')] ).
cnf(198,plain,
( ~ proposition(skc13,u)
| ~ proposition(skc13,v)
| ~ think_believe_consider(skc13,w)
| ~ theme(skc13,w,u)
| ~ agent(skc13,w,x)
| ~ theme(skc13,skc17,v)
| ~ agent(skc13,skc17,x)
| equal(u,v) ),
inference(res,[status(thm),theory(equality)],[17,110]),
[iquote('0:Res:17.0,110.3')] ).
cnf(768,plain,
( ~ human_person(skc14,u)
| ~ state(skc13,u) ),
inference(res,[status(thm),theory(equality)],[49,533]),
[iquote('0:Res:49.1,533.0')] ).
cnf(1035,plain,
~ male(skc14,skc18),
inference(res,[status(thm),theory(equality)],[205,763]),
[iquote('0:Res:205.0,763.0')] ).
cnf(763,plain,
( ~ relname(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[38,518]),
[iquote('0:Res:38.1,518.0')] ).
cnf(195,plain,
( ~ proposition(skc13,u)
| ~ proposition(skc13,v)
| ~ think_believe_consider(skc13,w)
| ~ theme(skc13,w,u)
| ~ agent(skc13,w,x)
| ~ theme(skc13,skc15,v)
| ~ agent(skc13,skc15,x)
| equal(u,v) ),
inference(res,[status(thm),theory(equality)],[18,110]),
[iquote('0:Res:18.0,110.3')] ).
cnf(762,plain,
( ~ proposition(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[58,518]),
[iquote('0:Res:58.1,518.0')] ).
cnf(756,plain,
( ~ man(skc14,u)
| ~ state(skc13,u) ),
inference(res,[status(thm),theory(equality)],[40,509]),
[iquote('0:Res:40.1,509.1')] ).
cnf(754,plain,
( ~ smoke(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[65,508]),
[iquote('0:Res:65.1,508.0')] ).
cnf(1010,plain,
~ male(skc13,skc18),
inference(res,[status(thm),theory(equality)],[160,1008]),
[iquote('0:Res:160.1,1008.0')] ).
cnf(151,plain,
( ~ proposition(skc13,u)
| ~ think_believe_consider(skc13,v)
| ~ think_believe_consider(skc13,w)
| ~ theme(skc13,w,u)
| ~ agent(skc13,w,x)
| ~ agent(skc13,v,x)
| ~ theme(skc13,v,skc14)
| equal(skc14,u) ),
inference(res,[status(thm),theory(equality)],[23,110]),
[iquote('0:Res:23.0,110.7')] ).
cnf(1000,plain,
~ state(skc13,skc19),
inference(mrr,[status(thm)],[999,21]),
[iquote('0:MRR:999.0,21.0')] ).
cnf(602,plain,
( ~ proposition(skc13,u)
| ~ think_believe_consider(skc13,v)
| ~ theme(skc13,v,u)
| ~ agent(skc13,v,w)
| ~ agent(skc13,skc15,w)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[599,23,18]),
[iquote('0:MRR:599.0,599.2,23.0,18.0')] ).
cnf(695,plain,
( ~ jules_forename(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[36,448]),
[iquote('0:Res:36.1,448.0')] ).
cnf(694,plain,
( ~ vincent_forename(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[37,448]),
[iquote('0:Res:37.1,448.0')] ).
cnf(686,plain,
( ~ man(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[50,445]),
[iquote('0:Res:50.1,445.0')] ).
cnf(207,plain,
( ~ forename(skc13,u)
| ~ entity(skc13,v)
| ~ of(skc13,u,v)
| ~ of(skc13,skc18,v)
| equal(u,skc18) ),
inference(res,[status(thm),theory(equality)],[13,109]),
[iquote('0:Res:13.0,109.4')] ).
cnf(961,plain,
~ proposition(skc13,skc19),
inference(res,[status(thm),theory(equality)],[219,655]),
[iquote('0:Res:219.0,655.0')] ).
cnf(942,plain,
equal(skc20,skc18),
inference(mrr,[status(thm)],[941,219]),
[iquote('0:MRR:941.0,219.0')] ).
cnf(903,plain,
( ~ accessible_world(skc13,u)
| jules_forename(u,skc18) ),
inference(rew,[status(thm),theory(equality)],[898,212]),
[iquote('0:Rew:898.0,212.1')] ).
cnf(899,plain,
jules_forename(skc13,skc18),
inference(rew,[status(thm),theory(equality)],[898,11]),
[iquote('0:Rew:898.0,11.0')] ).
cnf(898,plain,
equal(skc22,skc18),
inference(mrr,[status(thm)],[897,219]),
[iquote('0:MRR:897.0,219.0')] ).
cnf(593,plain,
( ~ forename(skc13,u)
| ~ entity(skc13,skc19)
| ~ of(skc13,u,skc19)
| equal(skc18,u) ),
inference(mrr,[status(thm)],[586,13]),
[iquote('0:MRR:586.1,13.0')] ).
cnf(871,plain,
~ smoke(skc14,skc18),
inference(res,[status(thm),theory(equality)],[65,856]),
[iquote('0:Res:65.1,856.0')] ).
cnf(859,plain,
~ organism(skc14,skc18),
inference(res,[status(thm),theory(equality)],[48,849]),
[iquote('0:Res:48.1,849.0')] ).
cnf(857,plain,
~ state(skc14,skc18),
inference(res,[status(thm),theory(equality)],[52,848]),
[iquote('0:Res:52.1,848.0')] ).
cnf(856,plain,
~ event(skc14,skc18),
inference(res,[status(thm),theory(equality)],[64,848]),
[iquote('0:Res:64.1,848.0')] ).
cnf(590,plain,
( ~ forename(skc13,u)
| ~ entity(skc13,skc25)
| ~ of(skc13,u,skc25)
| equal(skc26,u) ),
inference(mrr,[status(thm)],[589,3]),
[iquote('0:MRR:589.1,3.0')] ).
cnf(849,plain,
~ entity(skc14,skc18),
inference(res,[status(thm),theory(equality)],[46,840]),
[iquote('0:Res:46.1,840.0')] ).
cnf(848,plain,
~ eventuality(skc14,skc18),
inference(res,[status(thm),theory(equality)],[61,840]),
[iquote('0:Res:61.1,840.0')] ).
cnf(840,plain,
~ specific(skc14,skc18),
inference(res,[status(thm),theory(equality)],[205,614]),
[iquote('0:Res:205.0,614.0')] ).
cnf(147,plain,
( ~ be(skc13,u,v,w)
| be(skc14,u,v,w) ),
inference(res,[status(thm),theory(equality)],[24,108]),
[iquote('0:Res:24.0,108.1')] ).
cnf(614,plain,
( ~ relname(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[38,416]),
[iquote('0:Res:38.1,416.0')] ).
cnf(613,plain,
( ~ proposition(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[58,416]),
[iquote('0:Res:58.1,416.0')] ).
cnf(831,plain,
~ smoke(skc13,skc18),
inference(res,[status(thm),theory(equality)],[65,813]),
[iquote('0:Res:65.1,813.0')] ).
cnf(817,plain,
~ organism(skc13,skc18),
inference(res,[status(thm),theory(equality)],[48,794]),
[iquote('0:Res:48.1,794.0')] ).
cnf(814,plain,
~ state(skc13,skc18),
inference(res,[status(thm),theory(equality)],[52,793]),
[iquote('0:Res:52.1,793.0')] ).
cnf(813,plain,
~ event(skc13,skc18),
inference(res,[status(thm),theory(equality)],[64,793]),
[iquote('0:Res:64.1,793.0')] ).
cnf(146,plain,
( ~ agent(skc13,u,v)
| agent(skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[24,107]),
[iquote('0:Res:24.0,107.1')] ).
cnf(794,plain,
~ entity(skc13,skc18),
inference(res,[status(thm),theory(equality)],[46,781]),
[iquote('0:Res:46.1,781.0')] ).
cnf(145,plain,
( ~ theme(skc13,u,v)
| theme(skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[24,106]),
[iquote('0:Res:24.0,106.1')] ).
cnf(793,plain,
~ eventuality(skc13,skc18),
inference(res,[status(thm),theory(equality)],[61,781]),
[iquote('0:Res:61.1,781.0')] ).
cnf(144,plain,
( ~ of(skc13,u,v)
| of(skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[24,105]),
[iquote('0:Res:24.0,105.1')] ).
cnf(781,plain,
~ specific(skc13,skc18),
inference(res,[status(thm),theory(equality)],[180,776]),
[iquote('0:Res:180.1,776.0')] ).
cnf(578,plain,
( ~ accessible_world(skc13,u)
| be(u,skc24,skc25,skc25) ),
inference(res,[status(thm),theory(equality)],[35,108]),
[iquote('0:Res:35.0,108.1')] ).
cnf(533,plain,
( ~ organism(skc14,u)
| ~ state(skc13,u) ),
inference(res,[status(thm),theory(equality)],[48,414]),
[iquote('0:Res:48.1,414.0')] ).
cnf(761,plain,
~ male(skc14,skc14),
inference(res,[status(thm),theory(equality)],[149,518]),
[iquote('0:Res:149.0,518.0')] ).
cnf(518,plain,
( ~ relation(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[57,403]),
[iquote('0:Res:57.1,403.0')] ).
cnf(256,plain,
( ~ abstraction(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[53,72]),
[iquote('0:Res:53.1,72.1')] ).
cnf(509,plain,
( ~ state(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[52,402]),
[iquote('0:Res:52.1,402.0')] ).
cnf(508,plain,
( ~ event(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[64,402]),
[iquote('0:Res:64.1,402.0')] ).
cnf(737,plain,
~ male(skc13,skc14),
inference(res,[status(thm),theory(equality)],[160,732]),
[iquote('0:Res:160.1,732.0')] ).
cnf(255,plain,
( ~ eventuality(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[59,72]),
[iquote('0:Res:59.1,72.1')] ).
cnf(243,plain,
( ~ abstraction(u,v)
| ~ specific(u,v) ),
inference(res,[status(thm),theory(equality)],[54,71]),
[iquote('0:Res:54.1,71.0')] ).
cnf(705,plain,
~ man(skc14,skc26),
inference(res,[status(thm),theory(equality)],[50,702]),
[iquote('0:Res:50.1,702.0')] ).
cnf(236,plain,
( ~ eventuality(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[60,69]),
[iquote('0:Res:60.1,69.0')] ).
cnf(702,plain,
~ human_person(skc14,skc26),
inference(res,[status(thm),theory(equality)],[42,691]),
[iquote('0:Res:42.1,691.0')] ).
cnf(691,plain,
~ human(skc14,skc26),
inference(res,[status(thm),theory(equality)],[3,448]),
[iquote('0:Res:3.0,448.0')] ).
cnf(233,plain,
( ~ abstraction(u,v)
| ~ human(u,v) ),
inference(res,[status(thm),theory(equality)],[55,70]),
[iquote('0:Res:55.1,70.1')] ).
cnf(448,plain,
( ~ forename(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[39,376]),
[iquote('0:Res:39.1,376.0')] ).
cnf(445,plain,
( ~ human_person(skc14,u)
| ~ proposition(skc13,u) ),
inference(res,[status(thm),theory(equality)],[42,375]),
[iquote('0:Res:42.1,375.1')] ).
cnf(683,plain,
~ man(skc13,skc26),
inference(res,[status(thm),theory(equality)],[50,677]),
[iquote('0:Res:50.1,677.0')] ).
cnf(569,plain,
( ~ accessible_world(skc13,u)
| agent(u,skc17,skc19) ),
inference(res,[status(thm),theory(equality)],[30,107]),
[iquote('0:Res:30.0,107.1')] ).
cnf(677,plain,
~ human_person(skc13,skc26),
inference(res,[status(thm),theory(equality)],[42,671]),
[iquote('0:Res:42.1,671.0')] ).
cnf(568,plain,
( ~ accessible_world(skc13,u)
| agent(u,skc15,skc19) ),
inference(res,[status(thm),theory(equality)],[31,107]),
[iquote('0:Res:31.0,107.1')] ).
cnf(671,plain,
~ human(skc13,skc26),
inference(res,[status(thm),theory(equality)],[162,664]),
[iquote('0:Res:162.1,664.0')] ).
cnf(567,plain,
( ~ accessible_world(skc14,u)
| agent(u,skc21,skc19) ),
inference(res,[status(thm),theory(equality)],[32,107]),
[iquote('0:Res:32.0,107.1')] ).
cnf(646,plain,
~ smoke(skc14,skc14),
inference(res,[status(thm),theory(equality)],[65,631]),
[iquote('0:Res:65.1,631.0')] ).
cnf(556,plain,
( ~ accessible_world(skc13,u)
| theme(u,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[34,106]),
[iquote('0:Res:34.0,106.1')] ).
cnf(634,plain,
~ organism(skc14,skc14),
inference(res,[status(thm),theory(equality)],[48,622]),
[iquote('0:Res:48.1,622.0')] ).
cnf(632,plain,
~ state(skc14,skc14),
inference(res,[status(thm),theory(equality)],[52,621]),
[iquote('0:Res:52.1,621.0')] ).
cnf(631,plain,
~ event(skc14,skc14),
inference(res,[status(thm),theory(equality)],[64,621]),
[iquote('0:Res:64.1,621.0')] ).
cnf(545,plain,
( ~ accessible_world(skc13,u)
| of(u,skc26,skc25) ),
inference(res,[status(thm),theory(equality)],[26,105]),
[iquote('0:Res:26.0,105.1')] ).
cnf(622,plain,
~ entity(skc14,skc14),
inference(res,[status(thm),theory(equality)],[46,612]),
[iquote('0:Res:46.1,612.0')] ).
cnf(621,plain,
~ eventuality(skc14,skc14),
inference(res,[status(thm),theory(equality)],[61,612]),
[iquote('0:Res:61.1,612.0')] ).
cnf(612,plain,
~ specific(skc14,skc14),
inference(res,[status(thm),theory(equality)],[149,416]),
[iquote('0:Res:149.0,416.0')] ).
cnf(416,plain,
( ~ relation(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[57,346]),
[iquote('0:Res:57.1,346.0')] ).
cnf(605,plain,
~ smoke(skc13,skc14),
inference(res,[status(thm),theory(equality)],[65,579]),
[iquote('0:Res:65.1,579.0')] ).
cnf(542,plain,
( ~ accessible_world(skc13,u)
| of(u,skc18,skc19) ),
inference(res,[status(thm),theory(equality)],[29,105]),
[iquote('0:Res:29.0,105.1')] ).
cnf(581,plain,
~ organism(skc13,skc14),
inference(res,[status(thm),theory(equality)],[48,559]),
[iquote('0:Res:48.1,559.0')] ).
cnf(580,plain,
~ state(skc13,skc14),
inference(res,[status(thm),theory(equality)],[52,558]),
[iquote('0:Res:52.1,558.0')] ).
cnf(579,plain,
~ event(skc13,skc14),
inference(res,[status(thm),theory(equality)],[64,558]),
[iquote('0:Res:64.1,558.0')] ).
cnf(110,axiom,
( ~ proposition(u,v)
| ~ proposition(u,w)
| ~ think_believe_consider(u,x)
| ~ think_believe_consider(u,y)
| ~ theme(u,x,v)
| ~ theme(u,y,w)
| ~ agent(u,y,z)
| ~ agent(u,x,z)
| equal(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ forename(u,v)
| ~ forename(u,w)
| ~ entity(u,x)
| ~ of(u,w,x)
| ~ of(u,v,x)
| equal(w,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(559,plain,
~ entity(skc13,skc14),
inference(res,[status(thm),theory(equality)],[46,546]),
[iquote('0:Res:46.1,546.0')] ).
cnf(558,plain,
~ eventuality(skc13,skc14),
inference(res,[status(thm),theory(equality)],[61,546]),
[iquote('0:Res:61.1,546.0')] ).
cnf(108,axiom,
( ~ accessible_world(u,v)
| ~ be(u,w,x,y)
| be(v,w,x,y) ),
file('NLP249+1.p',unknown),
[] ).
cnf(107,axiom,
( ~ accessible_world(u,v)
| ~ agent(u,w,x)
| agent(v,w,x) ),
file('NLP249+1.p',unknown),
[] ).
cnf(546,plain,
~ specific(skc13,skc14),
inference(res,[status(thm),theory(equality)],[180,536]),
[iquote('0:Res:180.1,536.0')] ).
cnf(106,axiom,
( ~ accessible_world(u,v)
| ~ theme(u,w,x)
| theme(v,w,x) ),
file('NLP249+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ accessible_world(u,v)
| ~ of(u,w,x)
| of(v,w,x) ),
file('NLP249+1.p',unknown),
[] ).
cnf(414,plain,
( ~ entity(skc14,u)
| ~ state(skc13,u) ),
inference(res,[status(thm),theory(equality)],[45,309]),
[iquote('0:Res:45.1,309.1')] ).
cnf(78,axiom,
( ~ accessible_world(u,v)
| ~ forename(u,w)
| forename(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ accessible_world(u,v)
| ~ proposition(u,w)
| proposition(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(410,plain,
( ~ smoke(skc13,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[65,308]),
[iquote('0:Res:65.1,308.0')] ).
cnf(403,plain,
( ~ abstraction(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[53,254]),
[iquote('0:Res:53.1,254.0')] ).
cnf(507,plain,
~ male(skc14,skc24),
inference(res,[status(thm),theory(equality)],[113,402]),
[iquote('0:Res:113.0,402.0')] ).
cnf(506,plain,
~ male(skc14,skc15),
inference(res,[status(thm),theory(equality)],[191,402]),
[iquote('0:Res:191.0,402.0')] ).
cnf(95,axiom,
( ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| think_believe_consider(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(505,plain,
~ male(skc14,skc17),
inference(res,[status(thm),theory(equality)],[201,402]),
[iquote('0:Res:201.0,402.0')] ).
cnf(402,plain,
( ~ eventuality(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[59,254]),
[iquote('0:Res:59.1,254.0')] ).
cnf(497,plain,
~ male(skc13,skc24),
inference(res,[status(thm),theory(equality)],[160,488]),
[iquote('0:Res:160.1,488.0')] ).
cnf(103,axiom,
( ~ accessible_world(u,v)
| ~ event(u,w)
| event(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(495,plain,
~ male(skc13,skc15),
inference(res,[status(thm),theory(equality)],[160,487]),
[iquote('0:Res:160.1,487.0')] ).
cnf(491,plain,
~ male(skc13,skc17),
inference(res,[status(thm),theory(equality)],[160,486]),
[iquote('0:Res:160.1,486.0')] ).
cnf(88,axiom,
( ~ accessible_world(u,v)
| ~ man(u,w)
| man(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ accessible_world(u,v)
| ~ eventuality(u,w)
| eventuality(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ accessible_world(u,v)
| ~ entity(u,w)
| entity(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(96,axiom,
( ~ accessible_world(u,v)
| ~ present(u,w)
| present(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(457,plain,
~ man(skc14,skc18),
inference(res,[status(thm),theory(equality)],[50,454]),
[iquote('0:Res:50.1,454.0')] ).
cnf(76,axiom,
( ~ accessible_world(u,v)
| ~ vincent_forename(u,w)
| vincent_forename(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(454,plain,
~ human_person(skc14,skc18),
inference(res,[status(thm),theory(equality)],[42,447]),
[iquote('0:Res:42.1,447.0')] ).
cnf(447,plain,
~ human(skc14,skc18),
inference(res,[status(thm),theory(equality)],[205,376]),
[iquote('0:Res:205.0,376.0')] ).
cnf(87,axiom,
( ~ accessible_world(u,v)
| ~ human_person(u,w)
| human_person(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(376,plain,
( ~ relname(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[38,245]),
[iquote('0:Res:38.1,245.0')] ).
cnf(375,plain,
( ~ proposition(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[58,245]),
[iquote('0:Res:58.1,245.0')] ).
cnf(440,plain,
~ man(skc13,skc18),
inference(res,[status(thm),theory(equality)],[50,433]),
[iquote('0:Res:50.1,433.0')] ).
cnf(92,axiom,
( ~ accessible_world(u,v)
| ~ abstraction(u,w)
| abstraction(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(433,plain,
~ human_person(skc13,skc18),
inference(res,[status(thm),theory(equality)],[42,426]),
[iquote('0:Res:42.1,426.0')] ).
cnf(93,axiom,
( ~ accessible_world(u,v)
| ~ relation(u,w)
| relation(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(426,plain,
~ human(skc13,skc18),
inference(res,[status(thm),theory(equality)],[162,422]),
[iquote('0:Res:162.1,422.0')] ).
cnf(75,axiom,
( ~ accessible_world(u,v)
| ~ jules_forename(u,w)
| jules_forename(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(77,axiom,
( ~ accessible_world(u,v)
| ~ relname(u,w)
| relname(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(346,plain,
( ~ abstraction(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[54,242]),
[iquote('0:Res:54.1,242.0')] ).
cnf(309,plain,
( ~ state(skc13,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[52,240]),
[iquote('0:Res:52.1,240.0')] ).
cnf(86,axiom,
( ~ accessible_world(u,v)
| ~ organism(u,w)
| organism(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(308,plain,
( ~ event(skc13,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[64,240]),
[iquote('0:Res:64.1,240.0')] ).
cnf(254,plain,
( ~ unisex(skc13,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[136,72]),
[iquote('0:Res:136.1,72.1')] ).
cnf(89,axiom,
( ~ accessible_world(u,v)
| ~ state(u,w)
| state(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(385,plain,
~ man(skc14,skc14),
inference(res,[status(thm),theory(equality)],[50,380]),
[iquote('0:Res:50.1,380.0')] ).
cnf(380,plain,
~ human_person(skc14,skc14),
inference(res,[status(thm),theory(equality)],[42,374]),
[iquote('0:Res:42.1,374.0')] ).
cnf(101,axiom,
( ~ accessible_world(u,v)
| ~ thing(u,w)
| thing(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(374,plain,
~ human(skc14,skc14),
inference(res,[status(thm),theory(equality)],[149,245]),
[iquote('0:Res:149.0,245.0')] ).
cnf(245,plain,
( ~ relation(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[57,238]),
[iquote('0:Res:57.1,238.0')] ).
cnf(104,axiom,
( ~ accessible_world(u,v)
| ~ smoke(u,w)
| smoke(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(369,plain,
~ man(skc13,skc14),
inference(res,[status(thm),theory(equality)],[50,362]),
[iquote('0:Res:50.1,362.0')] ).
cnf(362,plain,
~ human_person(skc13,skc14),
inference(res,[status(thm),theory(equality)],[42,355]),
[iquote('0:Res:42.1,355.0')] ).
cnf(79,axiom,
( ~ accessible_world(u,v)
| ~ male(u,w)
| male(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(355,plain,
~ human(skc13,skc14),
inference(res,[status(thm),theory(equality)],[162,348]),
[iquote('0:Res:162.1,348.0')] ).
cnf(97,axiom,
( ~ accessible_world(u,v)
| ~ unisex(u,w)
| unisex(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(99,axiom,
( ~ accessible_world(u,v)
| ~ specific(u,w)
| specific(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(242,plain,
( ~ general(skc13,u)
| ~ specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[129,71]),
[iquote('0:Res:129.1,71.0')] ).
cnf(338,plain,
~ man(skc14,skc24),
inference(res,[status(thm),theory(equality)],[50,330]),
[iquote('0:Res:50.1,330.0')] ).
cnf(81,axiom,
( ~ accessible_world(u,v)
| ~ human(u,w)
| human(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(336,plain,
~ man(skc14,skc15),
inference(res,[status(thm),theory(equality)],[50,328]),
[iquote('0:Res:50.1,328.0')] ).
cnf(332,plain,
~ man(skc14,skc17),
inference(res,[status(thm),theory(equality)],[50,326]),
[iquote('0:Res:50.1,326.0')] ).
cnf(330,plain,
~ human_person(skc14,skc24),
inference(res,[status(thm),theory(equality)],[49,322]),
[iquote('0:Res:49.1,322.0')] ).
cnf(328,plain,
~ human_person(skc14,skc15),
inference(res,[status(thm),theory(equality)],[49,320]),
[iquote('0:Res:49.1,320.0')] ).
cnf(84,axiom,
( ~ accessible_world(u,v)
| ~ existent(u,w)
| existent(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(326,plain,
~ human_person(skc14,skc17),
inference(res,[status(thm),theory(equality)],[49,318]),
[iquote('0:Res:49.1,318.0')] ).
cnf(322,plain,
~ organism(skc14,skc24),
inference(res,[status(thm),theory(equality)],[48,317]),
[iquote('0:Res:48.1,317.0')] ).
cnf(320,plain,
~ organism(skc14,skc15),
inference(res,[status(thm),theory(equality)],[48,313]),
[iquote('0:Res:48.1,313.0')] ).
cnf(318,plain,
~ organism(skc14,skc17),
inference(res,[status(thm),theory(equality)],[48,311]),
[iquote('0:Res:48.1,311.0')] ).
cnf(90,axiom,
( ~ accessible_world(u,v)
| ~ general(u,w)
| general(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(317,plain,
~ entity(skc14,skc24),
inference(res,[status(thm),theory(equality)],[45,307]),
[iquote('0:Res:45.1,307.0')] ).
cnf(313,plain,
~ entity(skc14,skc15),
inference(res,[status(thm),theory(equality)],[45,306]),
[iquote('0:Res:45.1,306.0')] ).
cnf(311,plain,
~ entity(skc14,skc17),
inference(res,[status(thm),theory(equality)],[45,305]),
[iquote('0:Res:45.1,305.0')] ).
cnf(307,plain,
~ existent(skc14,skc24),
inference(res,[status(thm),theory(equality)],[113,240]),
[iquote('0:Res:113.0,240.0')] ).
cnf(91,axiom,
( ~ accessible_world(u,v)
| ~ nonhuman(u,w)
| nonhuman(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(306,plain,
~ existent(skc14,skc15),
inference(res,[status(thm),theory(equality)],[191,240]),
[iquote('0:Res:191.0,240.0')] ).
cnf(305,plain,
~ existent(skc14,skc17),
inference(res,[status(thm),theory(equality)],[201,240]),
[iquote('0:Res:201.0,240.0')] ).
cnf(240,plain,
( ~ eventuality(skc13,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[60,235]),
[iquote('0:Res:60.1,235.0')] ).
cnf(301,plain,
~ man(skc13,skc24),
inference(res,[status(thm),theory(equality)],[50,290]),
[iquote('0:Res:50.1,290.0')] ).
cnf(98,axiom,
( ~ accessible_world(u,v)
| ~ nonexistent(u,w)
| nonexistent(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(297,plain,
~ man(skc13,skc15),
inference(res,[status(thm),theory(equality)],[50,287]),
[iquote('0:Res:50.1,287.0')] ).
cnf(295,plain,
~ man(skc13,skc17),
inference(res,[status(thm),theory(equality)],[50,282]),
[iquote('0:Res:50.1,282.0')] ).
cnf(290,plain,
~ human_person(skc13,skc24),
inference(res,[status(thm),theory(equality)],[49,279]),
[iquote('0:Res:49.1,279.0')] ).
cnf(80,axiom,
( ~ accessible_world(u,v)
| ~ animate(u,w)
| animate(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(287,plain,
~ human_person(skc13,skc15),
inference(res,[status(thm),theory(equality)],[49,274]),
[iquote('0:Res:49.1,274.0')] ).
cnf(282,plain,
~ human_person(skc13,skc17),
inference(res,[status(thm),theory(equality)],[49,271]),
[iquote('0:Res:49.1,271.0')] ).
cnf(82,axiom,
( ~ accessible_world(u,v)
| ~ living(u,w)
| living(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(279,plain,
~ organism(skc13,skc24),
inference(res,[status(thm),theory(equality)],[48,267]),
[iquote('0:Res:48.1,267.0')] ).
cnf(274,plain,
~ organism(skc13,skc15),
inference(res,[status(thm),theory(equality)],[48,264]),
[iquote('0:Res:48.1,264.0')] ).
cnf(83,axiom,
( ~ accessible_world(u,v)
| ~ impartial(u,w)
| impartial(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(271,plain,
~ organism(skc13,skc17),
inference(res,[status(thm),theory(equality)],[48,261]),
[iquote('0:Res:48.1,261.0')] ).
cnf(267,plain,
~ entity(skc13,skc24),
inference(res,[status(thm),theory(equality)],[45,259]),
[iquote('0:Res:45.1,259.0')] ).
cnf(100,axiom,
( ~ accessible_world(u,v)
| ~ singleton(u,w)
| singleton(v,w) ),
file('NLP249+1.p',unknown),
[] ).
cnf(264,plain,
~ entity(skc13,skc15),
inference(res,[status(thm),theory(equality)],[45,257]),
[iquote('0:Res:45.1,257.0')] ).
cnf(261,plain,
~ entity(skc13,skc17),
inference(res,[status(thm),theory(equality)],[45,251]),
[iquote('0:Res:45.1,251.0')] ).
cnf(74,axiom,
( ~ be(u,v,w,x)
| equal(w,x) ),
file('NLP249+1.p',unknown),
[] ).
cnf(259,plain,
~ existent(skc13,skc24),
inference(res,[status(thm),theory(equality)],[165,248]),
[iquote('0:Res:165.1,248.0')] ).
cnf(257,plain,
~ existent(skc13,skc15),
inference(res,[status(thm),theory(equality)],[165,247]),
[iquote('0:Res:165.1,247.0')] ).
cnf(251,plain,
~ existent(skc13,skc17),
inference(res,[status(thm),theory(equality)],[165,246]),
[iquote('0:Res:165.1,246.0')] ).
cnf(72,axiom,
( ~ male(u,v)
| ~ unisex(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(238,plain,
( ~ abstraction(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[55,232]),
[iquote('0:Res:55.1,232.0')] ).
cnf(71,axiom,
( ~ general(u,v)
| ~ specific(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(235,plain,
( ~ nonexistent(skc13,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[137,69]),
[iquote('0:Res:137.1,69.0')] ).
cnf(232,plain,
( ~ nonhuman(skc13,u)
| ~ human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[130,70]),
[iquote('0:Res:130.1,70.1')] ).
cnf(69,axiom,
( ~ nonexistent(u,v)
| ~ existent(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(70,axiom,
( ~ human(u,v)
| ~ nonhuman(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ vincent_forename(u,v)
| forename(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ jules_forename(u,v)
| forename(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ state(u,v)
| event(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ smoke(u,v)
| event(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ event(u,v)
| eventuality(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ state(u,v)
| eventuality(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(48,axiom,
( ~ organism(u,v)
| entity(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ proposition(u,v)
| relation(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ man(u,v)
| human_person(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ relation(u,v)
| abstraction(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ relname(u,v)
| relation(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(148,plain,
( ~ accessible_world(skc13,u)
| proposition(u,skc14) ),
inference(res,[status(thm),theory(equality)],[23,94]),
[iquote('0:Res:23.0,94.0')] ).
cnf(39,axiom,
( ~ forename(u,v)
| relname(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(204,plain,
( ~ accessible_world(skc13,u)
| forename(u,skc18) ),
inference(res,[status(thm),theory(equality)],[13,78]),
[iquote('0:Res:13.0,78.0')] ).
cnf(194,plain,
( ~ accessible_world(skc13,u)
| think_believe_consider(u,skc15) ),
inference(res,[status(thm),theory(equality)],[18,95]),
[iquote('0:Res:18.0,95.0')] ).
cnf(63,axiom,
( ~ eventuality(u,v)
| thing(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(197,plain,
( ~ accessible_world(skc13,u)
| think_believe_consider(u,skc17) ),
inference(res,[status(thm),theory(equality)],[17,95]),
[iquote('0:Res:17.0,95.0')] ).
cnf(190,plain,
( ~ accessible_world(skc13,u)
| event(u,skc15) ),
inference(res,[status(thm),theory(equality)],[20,103]),
[iquote('0:Res:20.0,103.0')] ).
cnf(200,plain,
( ~ accessible_world(skc13,u)
| event(u,skc17) ),
inference(res,[status(thm),theory(equality)],[15,103]),
[iquote('0:Res:15.0,103.0')] ).
cnf(217,plain,
( ~ accessible_world(skc13,u)
| man(u,skc19) ),
inference(res,[status(thm),theory(equality)],[8,88]),
[iquote('0:Res:8.0,88.0')] ).
cnf(47,axiom,
( ~ entity(u,v)
| thing(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(192,plain,
( ~ accessible_world(skc13,u)
| present(u,skc15) ),
inference(res,[status(thm),theory(equality)],[19,96]),
[iquote('0:Res:19.0,96.0')] ).
cnf(199,plain,
( ~ accessible_world(skc13,u)
| present(u,skc17) ),
inference(res,[status(thm),theory(equality)],[16,96]),
[iquote('0:Res:16.0,96.0')] ).
cnf(216,plain,
( ~ accessible_world(skc14,u)
| present(u,skc21) ),
inference(res,[status(thm),theory(equality)],[9,96]),
[iquote('0:Res:9.0,96.0')] ).
cnf(202,plain,
( ~ accessible_world(skc13,u)
| vincent_forename(u,skc18) ),
inference(res,[status(thm),theory(equality)],[14,76]),
[iquote('0:Res:14.0,76.0')] ).
cnf(49,axiom,
( ~ human_person(u,v)
| organism(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(111,plain,
( ~ accessible_world(skc13,u)
| state(u,skc24) ),
inference(res,[status(thm),theory(equality)],[25,89]),
[iquote('0:Res:25.0,89.0')] ).
cnf(214,plain,
( ~ accessible_world(skc14,u)
| smoke(u,skc21) ),
inference(res,[status(thm),theory(equality)],[10,104]),
[iquote('0:Res:10.0,104.0')] ).
cnf(56,axiom,
( ~ abstraction(u,v)
| thing(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(117,plain,
( ~ forename(skc13,u)
| forename(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,78]),
[iquote('0:Res:24.0,78.1')] ).
cnf(133,plain,
( ~ proposition(skc13,u)
| proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,94]),
[iquote('0:Res:24.0,94.1')] ).
cnf(40,axiom,
( ~ man(u,v)
| male(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(134,plain,
( ~ think_believe_consider(skc13,u)
| think_believe_consider(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,95]),
[iquote('0:Res:24.0,95.1')] ).
cnf(142,plain,
( ~ event(skc13,u)
| event(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,103]),
[iquote('0:Res:24.0,103.1')] ).
cnf(59,axiom,
( ~ eventuality(u,v)
| unisex(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(127,plain,
( ~ man(skc13,u)
| man(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,88]),
[iquote('0:Res:24.0,88.1')] ).
cnf(141,plain,
( ~ eventuality(skc13,u)
| eventuality(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,102]),
[iquote('0:Res:24.0,102.1')] ).
cnf(61,axiom,
( ~ eventuality(u,v)
| specific(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(124,plain,
( ~ entity(skc13,u)
| entity(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,85]),
[iquote('0:Res:24.0,85.1')] ).
cnf(135,plain,
( ~ present(skc13,u)
| present(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,96]),
[iquote('0:Res:24.0,96.1')] ).
cnf(46,axiom,
( ~ entity(u,v)
| specific(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(115,plain,
( ~ vincent_forename(skc13,u)
| vincent_forename(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,76]),
[iquote('0:Res:24.0,76.1')] ).
cnf(126,plain,
( ~ human_person(skc13,u)
| human_person(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,87]),
[iquote('0:Res:24.0,87.1')] ).
cnf(131,plain,
( ~ abstraction(skc13,u)
| abstraction(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,92]),
[iquote('0:Res:24.0,92.1')] ).
cnf(132,plain,
( ~ relation(skc13,u)
| relation(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,93]),
[iquote('0:Res:24.0,93.1')] ).
cnf(53,axiom,
( ~ abstraction(u,v)
| unisex(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ eventuality(u,v)
| nonexistent(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(114,plain,
( ~ jules_forename(skc13,u)
| jules_forename(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,75]),
[iquote('0:Res:24.0,75.1')] ).
cnf(116,plain,
( ~ relname(skc13,u)
| relname(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,77]),
[iquote('0:Res:24.0,77.1')] ).
cnf(125,plain,
( ~ organism(skc13,u)
| organism(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,86]),
[iquote('0:Res:24.0,86.1')] ).
cnf(128,plain,
( ~ state(skc13,u)
| state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,89]),
[iquote('0:Res:24.0,89.1')] ).
cnf(45,axiom,
( ~ entity(u,v)
| existent(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(140,plain,
( ~ thing(skc13,u)
| thing(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,101]),
[iquote('0:Res:24.0,101.1')] ).
cnf(143,plain,
( ~ smoke(skc13,u)
| smoke(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,104]),
[iquote('0:Res:24.0,104.1')] ).
cnf(42,axiom,
( ~ human_person(u,v)
| human(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ abstraction(u,v)
| general(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(118,plain,
( ~ male(skc13,u)
| male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,79]),
[iquote('0:Res:24.0,79.1')] ).
cnf(136,plain,
( ~ unisex(skc13,u)
| unisex(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,97]),
[iquote('0:Res:24.0,97.1')] ).
cnf(138,plain,
( ~ specific(skc13,u)
| specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,99]),
[iquote('0:Res:24.0,99.1')] ).
cnf(55,axiom,
( ~ abstraction(u,v)
| nonhuman(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(120,plain,
( ~ human(skc13,u)
| human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,81]),
[iquote('0:Res:24.0,81.1')] ).
cnf(123,plain,
( ~ existent(skc13,u)
| existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,84]),
[iquote('0:Res:24.0,84.1')] ).
cnf(41,axiom,
( ~ human_person(u,v)
| animate(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(129,plain,
( ~ general(skc13,u)
| general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,90]),
[iquote('0:Res:24.0,90.1')] ).
cnf(130,plain,
( ~ nonhuman(skc13,u)
| nonhuman(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,91]),
[iquote('0:Res:24.0,91.1')] ).
cnf(137,plain,
( ~ nonexistent(skc13,u)
| nonexistent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,98]),
[iquote('0:Res:24.0,98.1')] ).
cnf(43,axiom,
( ~ organism(u,v)
| living(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ organism(u,v)
| impartial(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(119,plain,
( ~ animate(skc13,u)
| animate(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,80]),
[iquote('0:Res:24.0,80.1')] ).
cnf(121,plain,
( ~ living(skc13,u)
| living(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,82]),
[iquote('0:Res:24.0,82.1')] ).
cnf(122,plain,
( ~ impartial(skc13,u)
| impartial(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,83]),
[iquote('0:Res:24.0,83.1')] ).
cnf(139,plain,
( ~ singleton(skc13,u)
| singleton(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,100]),
[iquote('0:Res:24.0,100.1')] ).
cnf(62,axiom,
( ~ thing(u,v)
| singleton(u,v) ),
file('NLP249+1.p',unknown),
[] ).
cnf(35,axiom,
be(skc13,skc24,skc25,skc25),
file('NLP249+1.p',unknown),
[] ).
cnf(30,axiom,
agent(skc13,skc17,skc19),
file('NLP249+1.p',unknown),
[] ).
cnf(31,axiom,
agent(skc13,skc15,skc19),
file('NLP249+1.p',unknown),
[] ).
cnf(32,axiom,
agent(skc14,skc21,skc19),
file('NLP249+1.p',unknown),
[] ).
cnf(34,axiom,
theme(skc13,skc15,skc14),
file('NLP249+1.p',unknown),
[] ).
cnf(26,axiom,
of(skc13,skc26,skc25),
file('NLP249+1.p',unknown),
[] ).
cnf(112,plain,
event(skc13,skc24),
inference(res,[status(thm),theory(equality)],[25,51]),
[iquote('0:Res:25.0,51.0')] ).
cnf(113,plain,
eventuality(skc13,skc24),
inference(res,[status(thm),theory(equality)],[25,52]),
[iquote('0:Res:25.0,52.0')] ).
cnf(191,plain,
eventuality(skc13,skc15),
inference(res,[status(thm),theory(equality)],[20,64]),
[iquote('0:Res:20.0,64.0')] ).
cnf(201,plain,
eventuality(skc13,skc17),
inference(res,[status(thm),theory(equality)],[15,64]),
[iquote('0:Res:15.0,64.0')] ).
cnf(149,plain,
relation(skc13,skc14),
inference(res,[status(thm),theory(equality)],[23,58]),
[iquote('0:Res:23.0,58.0')] ).
cnf(29,axiom,
of(skc13,skc18,skc19),
file('NLP249+1.p',unknown),
[] ).
cnf(219,plain,
human_person(skc13,skc19),
inference(res,[status(thm),theory(equality)],[8,50]),
[iquote('0:Res:8.0,50.0')] ).
cnf(205,plain,
relname(skc13,skc18),
inference(res,[status(thm),theory(equality)],[13,39]),
[iquote('0:Res:13.0,39.0')] ).
cnf(218,plain,
male(skc13,skc19),
inference(res,[status(thm),theory(equality)],[8,40]),
[iquote('0:Res:8.0,40.0')] ).
cnf(24,axiom,
accessible_world(skc13,skc14),
file('NLP249+1.p',unknown),
[] ).
cnf(3,axiom,
forename(skc13,skc26),
file('NLP249+1.p',unknown),
[] ).
cnf(13,axiom,
forename(skc13,skc18),
file('NLP249+1.p',unknown),
[] ).
cnf(23,axiom,
proposition(skc13,skc14),
file('NLP249+1.p',unknown),
[] ).
cnf(17,axiom,
think_believe_consider(skc13,skc17),
file('NLP249+1.p',unknown),
[] ).
cnf(18,axiom,
think_believe_consider(skc13,skc15),
file('NLP249+1.p',unknown),
[] ).
cnf(5,axiom,
event(skc14,skc21),
file('NLP249+1.p',unknown),
[] ).
cnf(15,axiom,
event(skc13,skc17),
file('NLP249+1.p',unknown),
[] ).
cnf(20,axiom,
event(skc13,skc15),
file('NLP249+1.p',unknown),
[] ).
cnf(4,axiom,
man(skc13,skc25),
file('NLP249+1.p',unknown),
[] ).
cnf(8,axiom,
man(skc13,skc19),
file('NLP249+1.p',unknown),
[] ).
cnf(9,axiom,
present(skc14,skc21),
file('NLP249+1.p',unknown),
[] ).
cnf(16,axiom,
present(skc13,skc17),
file('NLP249+1.p',unknown),
[] ).
cnf(19,axiom,
present(skc13,skc15),
file('NLP249+1.p',unknown),
[] ).
cnf(14,axiom,
vincent_forename(skc13,skc18),
file('NLP249+1.p',unknown),
[] ).
cnf(2,axiom,
jules_forename(skc13,skc26),
file('NLP249+1.p',unknown),
[] ).
cnf(10,axiom,
smoke(skc14,skc21),
file('NLP249+1.p',unknown),
[] ).
cnf(25,axiom,
state(skc13,skc24),
file('NLP249+1.p',unknown),
[] ).
cnf(1,axiom,
actual_world(skc13),
file('NLP249+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP249+1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Fri Jul 1 07:27:53 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.38/0.56
% 0.38/0.56 SPASS V 3.9
% 0.38/0.56 SPASS beiseite: Completion found.
% 0.38/0.56 % SZS status CounterSatisfiable
% 0.38/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.56 SPASS derived 1724 clauses, backtracked 0 clauses, performed 0 splits and kept 821 clauses.
% 0.38/0.56 SPASS allocated 86194 KBytes.
% 0.38/0.56 SPASS spent 0:00:00.22 on the problem.
% 0.38/0.56 0:00:00.04 for the input.
% 0.38/0.56 0:00:00.04 for the FLOTTER CNF translation.
% 0.38/0.56 0:00:00.02 for inferences.
% 0.38/0.56 0:00:00.00 for the backtracking.
% 0.38/0.56 0:00:00.07 for the reduction.
% 0.38/0.56
% 0.38/0.56
% 0.38/0.56 The saturated set of worked-off clauses is :
% 0.38/0.56 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------