%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP259+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n011.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:18 EDT 2022
% Result : CounterSatisfiable 1.25s 1.44s
% Output : Saturation 1.29s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 94)
% Comments :
%------------------------------------------------------------------------------
cnf(1582,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,u)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ proposition(skc12,w)
| ~ accessible_world(skc12,w)
| ~ think_believe_consider(skc12,x)
| ~ present(skc12,x)
| ~ event(skc12,x)
| ~ jules_forename(skc12,y)
| ~ smoke(v,z)
| ~ present(v,z)
| ~ man(skc12,x1)
| ~ vincent_forename(skc12,x2)
| ~ event(skc12,x3)
| ~ present(skc12,x3)
| ~ think_believe_consider(skc12,x3)
| ~ theme(skc12,x,w)
| ~ of(skc12,y,x1)
| ~ agent(v,z,x1)
| ~ agent(skc12,x3,x1)
| ~ agent(skc12,x,x1)
| ~ of(skc12,x2,x1)
| ~ theme(skc12,x3,v)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[139,869]),
[iquote('0:Res:139.1,869.20')] ).
cnf(1539,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,u)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ jules_forename(skc12,x)
| ~ man(skc12,y)
| ~ vincent_forename(skc12,z)
| ~ event(skc12,x1)
| ~ present(skc12,x1)
| ~ think_believe_consider(skc12,x1)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(skc12,w,v)
| ~ of(skc12,x,y)
| ~ agent(skc12,x1,y)
| ~ agent(skc12,w,y)
| ~ of(skc12,z,y)
| ~ theme(skc12,x1,skc8)
| ~ agent(skc8,skc13,y)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[139,868]),
[iquote('0:Res:139.1,868.19')] ).
cnf(1663,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ vincent_forename(u,skc14)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13) ),
inference(obv,[status(thm),theory(equality)],[1660]),
[iquote('0:Obv:1660.1')] ).
cnf(1655,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ vincent_forename(u,v)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ of(u,v,skc15) ),
inference(mrr,[status(thm)],[1654,825]),
[iquote('0:MRR:1654.14,825.1')] ).
cnf(1583,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ jules_forename(u,y)
| ~ smoke(v,z)
| ~ present(v,z)
| ~ man(u,x1)
| ~ vincent_forename(u,x2)
| ~ event(u,x3)
| ~ present(u,x3)
| ~ think_believe_consider(u,x3)
| ~ theme(u,x,w)
| ~ of(u,y,x1)
| ~ agent(v,z,x1)
| ~ agent(u,x3,x1)
| ~ agent(u,x,x1)
| ~ of(u,x2,x1)
| ~ theme(u,x3,v)
| man(w,skf4(w)) ),
inference(obv,[status(thm),theory(equality)],[1580]),
[iquote('0:Obv:1580.1')] ).
cnf(1615,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,skc11)
| ~ smoke(v,skf2(skc10))
| ~ present(v,skf2(skc10))
| ~ man(u,skc10)
| ~ vincent_forename(u,w)
| ~ event(u,x)
| ~ present(u,x)
| ~ think_believe_consider(u,x)
| ~ agent(u,x,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,x,v) ),
inference(mrr,[status(thm)],[1610,71]),
[iquote('0:MRR:1610.1,71.2')] ).
cnf(1622,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,skc11)
| ~ man(u,skc10)
| ~ vincent_forename(u,v)
| ~ event(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(u,skf2(skc10))
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc12) ),
inference(mrr,[status(thm)],[1621,71]),
[iquote('0:MRR:1621.1,71.2')] ).
cnf(1614,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,skc11)
| ~ man(u,skc10)
| ~ vincent_forename(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ agent(u,w,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10)
| ~ theme(u,w,skc12) ),
inference(mrr,[status(thm)],[1613,71,216,220]),
[iquote('0:MRR:1613.1,1613.10,1613.11,71.2,216.0,220.0')] ).
cnf(1574,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,u)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ jules_forename(skc12,x)
| ~ smoke(v,y)
| ~ present(v,y)
| ~ man(skc12,z)
| ~ vincent_forename(skc12,x1)
| ~ event(skc12,x2)
| ~ present(skc12,x2)
| ~ think_believe_consider(skc12,x2)
| ~ theme(skc12,w,skc12)
| ~ of(skc12,x,z)
| ~ agent(v,y,z)
| ~ agent(skc12,x2,z)
| ~ agent(skc12,w,z)
| ~ of(skc12,x1,z)
| ~ theme(skc12,x2,v) ),
inference(obv,[status(thm),theory(equality)],[1572]),
[iquote('0:Obv:1572.2')] ).
cnf(1607,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,skc11)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ man(u,skc10)
| ~ vincent_forename(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ agent(v,w,skc10)
| ~ agent(u,y,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,x,skc10)
| ~ theme(u,y,v) ),
inference(obv,[status(thm),theory(equality)],[1598]),
[iquote('0:Obv:1598.5')] ).
cnf(1594,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,w)
| ~ smoke(v,x)
| ~ present(v,x)
| ~ man(u,y)
| ~ vincent_forename(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ of(u,w,y)
| ~ agent(v,x,y)
| ~ agent(u,x1,y)
| ~ agent(u,skc13,y)
| ~ of(u,z,y)
| ~ theme(u,x1,v) ),
inference(obv,[status(thm),theory(equality)],[1591]),
[iquote('0:Obv:1591.1')] ).
cnf(1573,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ jules_forename(u,x)
| ~ smoke(v,y)
| ~ present(v,y)
| ~ man(u,z)
| ~ vincent_forename(u,x1)
| ~ event(u,x2)
| ~ present(u,x2)
| ~ think_believe_consider(u,x2)
| ~ theme(u,w,skc12)
| ~ of(u,x,z)
| ~ agent(v,y,z)
| ~ agent(u,x2,z)
| ~ agent(u,w,z)
| ~ of(u,x1,z)
| ~ theme(u,x2,v) ),
inference(obv,[status(thm),theory(equality)],[1570]),
[iquote('0:Obv:1570.1')] ).
cnf(1540,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ jules_forename(u,x)
| ~ man(u,y)
| ~ vincent_forename(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,x1,y)
| ~ agent(u,w,y)
| ~ of(u,z,y)
| ~ theme(u,x1,skc8)
| ~ agent(skc8,skc13,y)
| man(v,skf4(v)) ),
inference(obv,[status(thm),theory(equality)],[1537]),
[iquote('0:Obv:1537.1')] ).
cnf(869,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| ~ proposition(u,w)
| ~ proposition(u,x)
| ~ accessible_world(u,x)
| ~ think_believe_consider(u,y)
| ~ present(u,y)
| ~ event(u,y)
| ~ jules_forename(u,z)
| ~ smoke(w,x1)
| ~ present(w,x1)
| ~ man(u,x2)
| ~ vincent_forename(u,x3)
| ~ event(u,x4)
| ~ present(u,x4)
| ~ think_believe_consider(u,x4)
| ~ of(u,v,skc10)
| ~ theme(u,y,x)
| ~ of(u,z,x2)
| ~ agent(w,x1,x2)
| ~ agent(u,x4,x2)
| ~ agent(u,y,x2)
| ~ of(u,x3,x2)
| ~ theme(u,x4,w)
| man(x,skf4(x)) ),
inference(res,[status(thm),theory(equality)],[860,96]),
[iquote('0:Res:860.1,96.27')] ).
cnf(1514,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,u)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,v)
| ~ present(skc12,v)
| ~ event(skc12,v)
| ~ jules_forename(skc12,w)
| ~ man(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ event(skc12,z)
| ~ present(skc12,z)
| ~ think_believe_consider(skc12,z)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(skc12,v,skc12)
| ~ of(skc12,w,x)
| ~ agent(skc12,z,x)
| ~ agent(skc12,v,x)
| ~ of(skc12,y,x)
| ~ theme(skc12,z,skc8)
| ~ agent(skc8,skc13,x) ),
inference(obv,[status(thm),theory(equality)],[1512]),
[iquote('0:Obv:1512.2')] ).
cnf(1522,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc11)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ jules_forename(skc12,v)
| ~ man(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ event(skc12,y)
| ~ present(skc12,y)
| ~ think_believe_consider(skc12,y)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,w)
| ~ agent(skc12,y,w)
| ~ agent(skc12,u,w)
| ~ of(skc12,x,w)
| ~ theme(skc12,y,skc8)
| ~ agent(skc8,skc13,w) ),
inference(obv,[status(thm),theory(equality)],[1518]),
[iquote('0:Obv:1518.2')] ).
cnf(867,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| ~ proposition(u,w)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ jules_forename(u,y)
| ~ smoke(w,z)
| ~ present(w,z)
| ~ man(u,x1)
| ~ vincent_forename(u,x2)
| ~ event(u,x3)
| ~ present(u,x3)
| ~ think_believe_consider(u,x3)
| ~ of(u,v,skc10)
| ~ theme(u,x,skc12)
| ~ of(u,y,x1)
| ~ agent(w,z,x1)
| ~ agent(u,x3,x1)
| ~ agent(u,x,x1)
| ~ of(u,x2,x1)
| ~ theme(u,x3,w) ),
inference(res,[status(thm),theory(equality)],[860,578]),
[iquote('0:Res:860.1,578.27')] ).
cnf(1547,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,skc11)
| ~ man(u,skc10)
| ~ vincent_forename(u,v)
| ~ event(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(u,skf2(skc10))
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1546,71]),
[iquote('0:MRR:1546.1,71.2')] ).
cnf(1534,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,skc11)
| ~ man(u,skc10)
| ~ vincent_forename(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,w,skc10)
| ~ of(u,v,skc10)
| ~ theme(u,w,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(obv,[status(thm),theory(equality)],[1525]),
[iquote('0:Obv:1525.5')] ).
cnf(868,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ jules_forename(u,y)
| ~ man(u,z)
| ~ vincent_forename(u,x1)
| ~ event(u,x2)
| ~ present(u,x2)
| ~ think_believe_consider(u,x2)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,x,w)
| ~ of(u,y,z)
| ~ agent(u,x2,z)
| ~ agent(u,x,z)
| ~ of(u,x1,z)
| ~ theme(u,x2,skc8)
| ~ agent(skc8,skc13,z)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[860,177]),
[iquote('0:Res:860.1,177.26')] ).
cnf(1521,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ vincent_forename(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,w)
| ~ agent(u,y,w)
| ~ of(u,x,w)
| ~ theme(u,y,skc8)
| ~ agent(skc8,skc13,w) ),
inference(mrr,[status(thm)],[1520,613]),
[iquote('0:MRR:1520.21,613.2')] ).
cnf(1513,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ jules_forename(u,w)
| ~ man(u,x)
| ~ vincent_forename(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,z,x)
| ~ agent(u,v,x)
| ~ of(u,y,x)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,x) ),
inference(obv,[status(thm),theory(equality)],[1510]),
[iquote('0:Obv:1510.1')] ).
cnf(1241,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ state(u,skc9)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ jules_forename(u,x)
| ~ man(u,y)
| ~ vincent_forename(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,w,skc12)
| ~ of(u,x,y)
| ~ agent(u,x1,y)
| ~ agent(u,w,y)
| ~ of(u,z,y)
| ~ theme(u,x1,skc8)
| ~ agent(skc8,skc13,y) ),
inference(res,[status(thm),theory(equality)],[860,1031]),
[iquote('0:Res:860.1,1031.26')] ).
cnf(1508,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,v)
| ~ accessible_world(skc12,w)
| ~ proposition(skc12,w)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ jules_forename(skc12,x)
| ~ smoke(w,y)
| ~ present(w,y)
| ~ man(skc12,z)
| ~ vincent_forename(skc12,x1)
| ~ event(skc12,x2)
| ~ present(skc12,x2)
| ~ think_believe_consider(skc12,x2)
| ~ of(skc12,x,z)
| ~ agent(w,y,z)
| ~ agent(skc12,x2,z)
| ~ agent(skc12,u,z)
| ~ of(skc12,x1,z)
| ~ theme(skc12,x2,w)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1506,12]),
[iquote('0:MRR:1506.2,12.0')] ).
cnf(1243,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ state(skc12,u)
| ~ man(skc12,v)
| ~ jules_forename(skc12,w)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,x)
| ~ present(skc12,x)
| ~ event(skc12,x)
| ~ jules_forename(skc12,y)
| ~ man(skc12,z)
| ~ vincent_forename(skc12,x1)
| ~ event(skc12,x2)
| ~ present(skc12,x2)
| ~ think_believe_consider(skc12,x2)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,w,v)
| ~ theme(skc12,x,skc12)
| ~ of(skc12,y,z)
| ~ agent(skc12,x2,z)
| ~ agent(skc12,x,z)
| ~ of(skc12,x1,z)
| ~ theme(skc12,x2,skc8)
| ~ agent(skc8,skc13,z) ),
inference(res,[status(thm),theory(equality)],[143,1031]),
[iquote('0:Res:143.1,1031.26')] ).
cnf(1223,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ jules_forename(u,y)
| ~ smoke(v,z)
| ~ present(v,z)
| ~ man(u,x1)
| ~ vincent_forename(u,x2)
| ~ event(u,x3)
| ~ present(u,x3)
| ~ think_believe_consider(u,x3)
| ~ theme(u,x,w)
| ~ of(u,y,x1)
| ~ agent(v,z,x1)
| ~ agent(u,x3,x1)
| ~ agent(u,x,x1)
| ~ of(u,x2,x1)
| ~ theme(u,x3,v)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[1222,162]),
[iquote('0:MRR:1222.2,162.1')] ).
cnf(1156,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ jules_forename(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,x)
| ~ accessible_world(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,v)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ of(skc8,w,skc10)
| ~ theme(skc8,y,x)
| ~ of(skc8,z,v)
| ~ agent(skc8,x1,v)
| ~ agent(skc8,y,v)
| ~ theme(skc8,x1,u)
| ~ of(skc8,skc14,v)
| man(x,skf4(x)) ),
inference(mrr,[status(thm)],[1149,122]),
[iquote('0:MRR:1149.0,122.1')] ).
cnf(1126,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ jules_forename(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,x)
| ~ accessible_world(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ man(skc8,v)
| ~ vincent_forename(skc8,z)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ of(skc8,w,skc10)
| ~ theme(skc8,y,x)
| ~ agent(skc8,x1,v)
| ~ agent(skc8,y,v)
| ~ of(skc8,z,v)
| ~ theme(skc8,x1,u)
| ~ of(skc8,skc11,v)
| man(x,skf4(x)) ),
inference(mrr,[status(thm)],[1119,122]),
[iquote('0:MRR:1119.0,122.1')] ).
cnf(1486,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,v)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,u)
| ~ man(skc12,v)
| ~ vincent_forename(skc12,w)
| ~ event(skc12,x)
| ~ present(skc12,x)
| ~ think_believe_consider(skc12,x)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc12,x,v)
| ~ of(skc12,w,v)
| ~ theme(skc12,x,skc8)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[1480,12]),
[iquote('0:MRR:1480.2,12.0')] ).
cnf(635,plain,
( ~ actual_world(u)
| ~ man(skc12,skf4(v))
| ~ accessible_world(skc12,v)
| ~ state(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ accessible_world(u,z)
| ~ proposition(u,z)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ jules_forename(u,x2)
| ~ smoke(z,x3)
| ~ present(z,x3)
| ~ man(u,x4)
| ~ vincent_forename(u,x5)
| ~ event(u,x6)
| ~ present(u,x6)
| ~ think_believe_consider(u,x6)
| ~ smoke(v,skf2(skf4(v)))
| ~ present(v,skf2(skf4(v)))
| ~ of(u,y,x)
| ~ theme(u,x1,v)
| ~ of(u,x2,x4)
| ~ agent(z,x3,x4)
| ~ agent(u,x6,x4)
| ~ agent(u,x1,x4)
| ~ of(u,x5,x4)
| ~ theme(u,x6,z)
| ~ be(u,w,x,x) ),
inference(res,[status(thm),theory(equality)],[511,97]),
[iquote('0:Res:511.2,97.29')] ).
cnf(1496,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,skf2(skc10),skc8)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,u,skc10)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1495,151,12,217,220]),
[iquote('0:MRR:1495.2,1495.3,1495.6,1495.7,151.1,12.0,217.0,220.0')] ).
cnf(1488,plain,
( ~ actual_world(u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ event(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(u,skf2(skc10))
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(res,[status(thm),theory(equality)],[511,1485]),
[iquote('0:Res:511.2,1485.10')] ).
cnf(1490,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,v)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,skc10)
| ~ theme(skc12,u,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1489,12]),
[iquote('0:MRR:1489.2,12.0')] ).
cnf(1491,plain,
( ~ actual_world(skc12)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,u,skc10)
| ~ theme(skc12,skf2(skc10),skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1487,151,12,217,220]),
[iquote('0:MRR:1487.1,1487.2,1487.5,1487.6,151.1,12.0,217.0,220.0')] ).
cnf(1038,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(v,w,x3)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x5,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,x5,v)
| ~ be(skc8,x,y,y) ),
inference(res,[status(thm),theory(equality)],[511,98]),
[iquote('0:Res:511.2,98.21')] ).
cnf(1485,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,w,skc10)
| ~ of(u,v,skc10)
| ~ theme(u,w,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1484,162,151]),
[iquote('0:MRR:1484.3,1484.4,162.1,151.1')] ).
cnf(1461,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ vincent_forename(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,w)
| ~ agent(u,y,w)
| ~ of(u,x,w)
| ~ theme(u,y,skc8)
| ~ agent(skc8,skc13,w) ),
inference(mrr,[status(thm)],[1460,170,176,184,90]),
[iquote('0:MRR:1460.3,1460.4,1460.5,1460.17,170.1,176.1,184.1,90.2')] ).
cnf(1473,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,skc8)
| ~ vincent_forename(skc8,u)
| ~ event(skc8,skf2(skc10))
| ~ present(skc8,skf2(skc10))
| ~ think_believe_consider(skc8,skf2(skc10))
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,skf2(skc10),skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(res,[status(thm),theory(equality)],[511,1468]),
[iquote('0:Res:511.2,1468.7')] ).
cnf(1468,plain,
( ~ vincent_forename(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc8,v,skc10)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,v,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1462,162,151]),
[iquote('0:MRR:1462.0,1462.1,162.1,151.1')] ).
cnf(1029,plain,
( ~ actual_world(u)
| ~ man(skc12,skf4(v))
| ~ accessible_world(skc12,v)
| ~ state(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ jules_forename(u,x1)
| ~ man(u,x2)
| ~ vincent_forename(u,x3)
| ~ event(u,x4)
| ~ present(u,x4)
| ~ think_believe_consider(u,x4)
| ~ smoke(v,skf2(skf4(v)))
| ~ present(v,skf2(skf4(v)))
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,y,x)
| ~ theme(u,z,v)
| ~ of(u,x1,x2)
| ~ agent(u,x4,x2)
| ~ agent(u,z,x2)
| ~ of(u,x3,x2)
| ~ theme(u,x4,skc8)
| ~ agent(skc8,skc13,x2)
| ~ be(u,w,x,x) ),
inference(res,[status(thm),theory(equality)],[511,182]),
[iquote('0:Res:511.2,182.27')] ).
cnf(1459,plain,
( ~ jules_forename(skc8,u)
| ~ man(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc8,u,v)
| ~ agent(skc8,x,v)
| ~ of(skc8,w,v)
| ~ theme(skc8,x,skc8)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[1458,12,170,176,48]),
[iquote('0:MRR:1458.0,1458.1,1458.2,1458.3,12.0,170.1,176.1,48.1')] ).
cnf(1420,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,v)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ jules_forename(skc12,w)
| ~ man(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ event(skc12,z)
| ~ present(skc12,z)
| ~ think_believe_consider(skc12,z)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,w,x)
| ~ agent(skc12,z,x)
| ~ agent(skc12,u,x)
| ~ of(skc12,y,x)
| ~ theme(skc12,z,skc8)
| ~ agent(skc8,skc13,x)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1416,12]),
[iquote('0:MRR:1416.2,12.0')] ).
cnf(986,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(v,w,x3)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x4,x3)
| ~ agent(skc8,x1,x3)
| ~ theme(skc8,x4,v)
| ~ of(skc8,skc14,x3)
| ~ be(skc8,x,y,y) ),
inference(res,[status(thm),theory(equality)],[511,203]),
[iquote('0:Res:511.2,203.20')] ).
cnf(967,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(v,w,x2)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,x4,x2)
| ~ agent(skc8,z,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,x4,v)
| ~ of(skc8,skc11,y)
| ~ be(skc8,x,y,y) ),
inference(res,[status(thm),theory(equality)],[511,206]),
[iquote('0:Res:511.2,206.20')] ).
cnf(1216,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ jules_forename(u,x)
| ~ man(u,y)
| ~ vincent_forename(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,x1,y)
| ~ agent(u,w,y)
| ~ of(u,z,y)
| ~ theme(u,x1,skc8)
| ~ agent(skc8,skc13,y)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1215,162]),
[iquote('0:MRR:1215.2,162.1')] ).
cnf(948,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(v,w,x2)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,u)
| ~ agent(skc8,x4,x2)
| ~ agent(skc8,x1,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,x4,v)
| ~ of(skc8,skc11,x2)
| ~ be(skc8,x,y,y) ),
inference(res,[status(thm),theory(equality)],[511,207]),
[iquote('0:Res:511.2,207.20')] ).
cnf(1335,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ jules_forename(skc12,w)
| ~ smoke(v,x)
| ~ present(v,x)
| ~ man(skc12,y)
| ~ vincent_forename(skc12,z)
| ~ event(skc12,x1)
| ~ present(skc12,x1)
| ~ think_believe_consider(skc12,x1)
| ~ of(skc12,w,y)
| ~ agent(v,x,y)
| ~ agent(skc12,x1,y)
| ~ agent(skc12,u,y)
| ~ of(skc12,z,y)
| ~ theme(skc12,x1,v) ),
inference(mrr,[status(thm)],[1332,12]),
[iquote('0:MRR:1332.2,12.0')] ).
cnf(1351,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,v)
| ~ accessible_world(skc12,w)
| ~ proposition(skc12,w)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,u)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ man(skc12,v)
| ~ vincent_forename(skc12,y)
| ~ event(skc12,z)
| ~ present(skc12,z)
| ~ think_believe_consider(skc12,z)
| ~ agent(w,x,v)
| ~ agent(skc12,z,v)
| ~ agent(skc12,skc13,v)
| ~ of(skc12,y,v)
| ~ theme(skc12,z,w) ),
inference(mrr,[status(thm)],[1346,12]),
[iquote('0:MRR:1346.2,12.0')] ).
cnf(1353,plain,
( ~ actual_world(u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ accessible_world(u,skc12)
| ~ smoke(v,skf2(skc10))
| ~ present(v,skf2(skc10))
| ~ vincent_forename(u,w)
| ~ event(u,x)
| ~ present(u,x)
| ~ think_believe_consider(u,x)
| ~ agent(u,x,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,x,v) ),
inference(res,[status(thm),theory(equality)],[511,1350]),
[iquote('0:Res:511.2,1350.11')] ).
cnf(1404,plain,
( ~ actual_world(skc12)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,skc14) ),
inference(mrr,[status(thm)],[1403,2,12]),
[iquote('0:MRR:1403.1,1403.2,2.0,12.0')] ).
cnf(926,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(v,w,x2)
| ~ of(skc8,y,x)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,x4,x2)
| ~ agent(skc8,z,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,x4,v)
| ~ be(skc8,skc9,x,x) ),
inference(res,[status(thm),theory(equality)],[511,210]),
[iquote('0:Res:511.2,210.20')] ).
cnf(1401,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15) ),
inference(mrr,[status(thm)],[1400,189]),
[iquote('0:MRR:1400.5,189.1')] ).
cnf(910,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ jules_forename(skc8,y)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(v,w,x2)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,x4,x2)
| ~ agent(skc8,z,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,x4,v)
| ~ of(skc8,y,skc10)
| ~ be(skc8,x,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[511,208]),
[iquote('0:Res:511.2,208.20')] ).
cnf(1356,plain,
( ~ actual_world(u)
| ~ agent(skc8,v,skc10)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ smoke(skc12,v)
| ~ present(skc12,v)
| ~ vincent_forename(u,w)
| ~ event(u,x)
| ~ present(u,x)
| ~ think_believe_consider(u,x)
| ~ agent(u,x,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,x,skc12) ),
inference(mrr,[status(thm)],[1355,101]),
[iquote('0:MRR:1355.3,101.1')] ).
cnf(1370,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,skf2(skc10),skc12)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ agent(skc12,skc13,skc10)
| ~ of(skc12,u,skc10) ),
inference(mrr,[status(thm)],[1369,151,12,217,220]),
[iquote('0:MRR:1369.2,1369.3,1369.6,1369.7,151.1,12.0,217.0,220.0')] ).
cnf(1365,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ event(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(u,skf2(skc10))
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc12) ),
inference(obv,[status(thm),theory(equality)],[1360]),
[iquote('0:Obv:1360.1')] ).
cnf(1362,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,v)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ agent(skc12,skc13,skc10)
| ~ of(skc12,v,skc10)
| ~ theme(skc12,u,skc12) ),
inference(mrr,[status(thm)],[1361,151,12]),
[iquote('0:MRR:1361.2,1361.3,151.1,12.0')] ).
cnf(896,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(v,w,skc10)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,u)
| ~ theme(skc8,x4,v)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x4,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ be(skc8,x,y,y) ),
inference(res,[status(thm),theory(equality)],[511,209]),
[iquote('0:Res:511.2,209.20')] ).
cnf(1364,plain,
( ~ actual_world(skc12)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ agent(skc12,skc13,skc10)
| ~ of(skc12,u,skc10)
| ~ theme(skc12,skf2(skc10),skc12) ),
inference(mrr,[status(thm)],[1363,151,12,217,220]),
[iquote('0:MRR:1363.1,1363.2,1363.5,1363.6,151.1,12.0,217.0,220.0')] ).
cnf(1358,plain,
( ~ actual_world(u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ agent(u,w,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10)
| ~ theme(u,w,skc12) ),
inference(mrr,[status(thm)],[1357,101,216,220]),
[iquote('0:MRR:1357.3,1357.5,1357.6,101.1,216.0,220.0')] ).
cnf(1350,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ accessible_world(u,skc12)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ vincent_forename(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ agent(v,w,skc10)
| ~ agent(u,y,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,x,skc10)
| ~ theme(u,y,v) ),
inference(mrr,[status(thm)],[1349,162,151]),
[iquote('0:MRR:1349.5,1349.8,162.1,151.1')] ).
cnf(1334,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,w)
| ~ smoke(v,x)
| ~ present(v,x)
| ~ man(u,y)
| ~ vincent_forename(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ of(u,w,y)
| ~ agent(v,x,y)
| ~ agent(u,x1,y)
| ~ agent(u,skc13,y)
| ~ of(u,z,y)
| ~ theme(u,x1,v) ),
inference(mrr,[status(thm)],[1333,170,176,184]),
[iquote('0:MRR:1333.5,1333.6,1333.7,170.1,176.1,184.1')] ).
cnf(873,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,v)
| ~ man(skc8,w)
| ~ jules_forename(skc8,x)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ jules_forename(skc8,z)
| ~ smoke(skc12,x1)
| ~ present(skc12,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ of(skc8,x,w)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,x2)
| ~ agent(skc12,x1,x2)
| ~ agent(skc8,x4,x2)
| ~ agent(skc8,y,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,x4,skc12)
| ~ be(skc8,v,w,w) ),
inference(res,[status(thm),theory(equality)],[511,212]),
[iquote('0:Res:511.2,212.18')] ).
cnf(1205,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ jules_forename(u,x)
| ~ smoke(v,y)
| ~ present(v,y)
| ~ man(u,z)
| ~ vincent_forename(u,x1)
| ~ event(u,x2)
| ~ present(u,x2)
| ~ think_believe_consider(u,x2)
| ~ theme(u,w,skc12)
| ~ of(u,x,z)
| ~ agent(v,y,z)
| ~ agent(u,x2,z)
| ~ agent(u,w,z)
| ~ of(u,x1,z)
| ~ theme(u,x2,v) ),
inference(mrr,[status(thm)],[1204,162]),
[iquote('0:MRR:1204.2,162.1')] ).
cnf(1325,plain,
( ~ smoke(u,skc13)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ jules_forename(skc8,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ of(skc8,v,skc15)
| ~ agent(skc8,w,skc15)
| ~ theme(skc8,w,u) ),
inference(mrr,[status(thm)],[1322,7,6,5,15]),
[iquote('0:MRR:1322.3,1322.4,1322.5,1322.12,7.0,6.0,5.0,15.0')] ).
cnf(808,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ state(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ agent(v,w,x3)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ agent(skc8,skc13,x3)
| ~ theme(skc8,skc13,v)
| ~ be(skc8,x,y,y) ),
inference(res,[status(thm),theory(equality)],[511,205]),
[iquote('0:Res:511.2,205.18')] ).
cnf(1315,plain,
( ~ agent(skc8,skc13,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1309,8,10]),
[iquote('0:MRR:1309.0,1309.1,8.0,10.0')] ).
cnf(1308,plain,
( ~ jules_forename(skc8,u)
| ~ man(skc8,v)
| ~ of(skc8,u,v)
| ~ agent(skc8,skc13,v)
| ~ of(skc8,skc14,v) ),
inference(mrr,[status(thm)],[1305,7,6,5]),
[iquote('0:MRR:1305.0,1305.1,1305.2,7.0,6.0,5.0')] ).
cnf(1304,plain,
( ~ think_believe_consider(skc8,u)
| ~ present(skc8,u)
| ~ event(skc8,u)
| ~ jules_forename(skc8,v)
| ~ man(skc8,w)
| ~ theme(skc8,u,skc12)
| ~ of(skc8,v,w)
| ~ agent(skc8,u,w)
| ~ of(skc8,skc14,w) ),
inference(mrr,[status(thm)],[1301,8]),
[iquote('0:MRR:1301.0,8.0')] ).
cnf(621,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ state(skc12,u)
| ~ man(skc12,v)
| ~ jules_forename(skc12,w)
| ~ accessible_world(skc12,x)
| ~ proposition(skc12,x)
| ~ proposition(skc12,y)
| ~ accessible_world(skc12,y)
| ~ think_believe_consider(skc12,z)
| ~ present(skc12,z)
| ~ event(skc12,z)
| ~ jules_forename(skc12,x1)
| ~ smoke(x,x2)
| ~ present(x,x2)
| ~ man(skc12,x3)
| ~ vincent_forename(skc12,x4)
| ~ event(skc12,x5)
| ~ present(skc12,x5)
| ~ think_believe_consider(skc12,x5)
| ~ of(skc12,w,v)
| ~ theme(skc12,z,y)
| ~ of(skc12,x1,x3)
| ~ agent(x,x2,x3)
| ~ agent(skc12,x5,x3)
| ~ agent(skc12,z,x3)
| ~ of(skc12,x4,x3)
| ~ theme(skc12,x5,x)
| man(y,skf4(y)) ),
inference(res,[status(thm),theory(equality)],[143,96]),
[iquote('0:Res:143.1,96.27')] ).
cnf(1287,plain,
~ of(skc8,skc11,skc15),
inference(mrr,[status(thm)],[1284,4]),
[iquote('0:MRR:1284.0,4.0')] ).
cnf(1279,plain,
( ~ man(skc8,u)
| ~ vincent_forename(skc8,v)
| ~ agent(skc8,skc13,u)
| ~ of(skc8,v,u)
| ~ of(skc8,skc11,u) ),
inference(mrr,[status(thm)],[1276,7,6,5]),
[iquote('0:MRR:1276.0,1276.1,1276.2,7.0,6.0,5.0')] ).
cnf(851,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ state(skc12,u)
| ~ man(skc12,v)
| ~ jules_forename(skc12,w)
| ~ accessible_world(skc12,x)
| ~ proposition(skc12,x)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,y)
| ~ present(skc12,y)
| ~ event(skc12,y)
| ~ jules_forename(skc12,z)
| ~ smoke(x,x1)
| ~ present(x,x1)
| ~ man(skc12,x2)
| ~ vincent_forename(skc12,x3)
| ~ event(skc12,x4)
| ~ present(skc12,x4)
| ~ think_believe_consider(skc12,x4)
| ~ of(skc12,w,v)
| ~ theme(skc12,y,skc12)
| ~ of(skc12,z,x2)
| ~ agent(x,x1,x2)
| ~ agent(skc12,x4,x2)
| ~ agent(skc12,y,x2)
| ~ of(skc12,x3,x2)
| ~ theme(skc12,x4,x) ),
inference(res,[status(thm),theory(equality)],[143,578]),
[iquote('0:Res:143.1,578.27')] ).
cnf(1275,plain,
( ~ think_believe_consider(skc8,u)
| ~ present(skc8,u)
| ~ event(skc8,u)
| ~ man(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ theme(skc8,u,skc12)
| ~ agent(skc8,u,v)
| ~ of(skc8,w,v)
| ~ of(skc8,skc11,v) ),
inference(mrr,[status(thm)],[1272,8]),
[iquote('0:MRR:1272.0,8.0')] ).
cnf(835,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ state(skc12,u)
| ~ man(skc12,v)
| ~ jules_forename(skc12,w)
| ~ proposition(skc12,x)
| ~ accessible_world(skc12,x)
| ~ think_believe_consider(skc12,y)
| ~ present(skc12,y)
| ~ event(skc12,y)
| ~ jules_forename(skc12,z)
| ~ man(skc12,x1)
| ~ vincent_forename(skc12,x2)
| ~ event(skc12,x3)
| ~ present(skc12,x3)
| ~ think_believe_consider(skc12,x3)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,w,v)
| ~ theme(skc12,y,x)
| ~ of(skc12,z,x1)
| ~ agent(skc12,x3,x1)
| ~ agent(skc12,y,x1)
| ~ of(skc12,x2,x1)
| ~ theme(skc12,x3,skc8)
| ~ agent(skc8,skc13,x1)
| man(x,skf4(x)) ),
inference(res,[status(thm),theory(equality)],[143,177]),
[iquote('0:Res:143.1,177.26')] ).
cnf(1031,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,y)
| ~ present(u,y)
| ~ event(u,y)
| ~ jules_forename(u,z)
| ~ man(u,x1)
| ~ vincent_forename(u,x2)
| ~ event(u,x3)
| ~ present(u,x3)
| ~ think_believe_consider(u,x3)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,x,w)
| ~ theme(u,y,skc12)
| ~ of(u,z,x1)
| ~ agent(u,x3,x1)
| ~ agent(u,y,x1)
| ~ of(u,x2,x1)
| ~ theme(u,x3,skc8)
| ~ agent(skc8,skc13,x1)
| ~ be(u,v,w,w) ),
inference(mrr,[status(thm)],[1028,177,216,220]),
[iquote('0:MRR:1028.1,1028.16,1028.17,177.27,216.0,220.0')] ).
cnf(899,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ state(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ event(skc8,x3)
| ~ present(skc8,x3)
| ~ think_believe_consider(skc8,x3)
| ~ agent(u,v,skc10)
| ~ of(skc8,y,x)
| ~ theme(skc8,z,skc12)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,x3,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| ~ be(skc8,w,x,x) ),
inference(mrr,[status(thm)],[895,199,216,220,13,12]),
[iquote('0:MRR:895.0,895.3,895.4,895.10,895.11,199.26,216.0,220.0,13.0,12.0')] ).
cnf(793,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ jules_forename(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,x)
| ~ accessible_world(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ agent(u,v,x1)
| ~ of(skc8,w,skc10)
| ~ theme(skc8,y,x)
| ~ of(skc8,z,x1)
| ~ agent(skc8,x2,x1)
| ~ agent(skc8,y,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,skc14,x1)
| man(x,skf4(x)) ),
inference(mrr,[status(thm)],[791,11,10]),
[iquote('0:MRR:791.2,791.3,11.0,10.0')] ).
cnf(778,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ jules_forename(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,x)
| ~ accessible_world(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ man(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ agent(u,v,z)
| ~ of(skc8,w,skc10)
| ~ theme(skc8,y,x)
| ~ agent(skc8,x2,z)
| ~ agent(skc8,y,z)
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,u)
| ~ of(skc8,skc11,z)
| man(x,skf4(x)) ),
inference(mrr,[status(thm)],[776,11,10]),
[iquote('0:MRR:776.2,776.3,11.0,10.0')] ).
cnf(1099,plain,
( ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ jules_forename(skc8,w)
| ~ smoke(skc12,x)
| ~ present(skc12,x)
| ~ man(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,y)
| ~ agent(skc12,x,y)
| ~ agent(skc8,x1,y)
| ~ agent(skc8,v,y)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,skc12)
| man(u,skf4(u)) ),
inference(mrr,[status(thm)],[1096,8]),
[iquote('0:MRR:1096.0,8.0')] ).
cnf(1108,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ vincent_forename(skc8,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ agent(skc8,w,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ of(skc8,v,skc10)
| ~ theme(skc8,w,u) ),
inference(res,[status(thm),theory(equality)],[511,1106]),
[iquote('0:Res:511.2,1106.8')] ).
cnf(1106,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ smoke(u,v)
| ~ present(u,v)
| ~ vincent_forename(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ agent(u,v,skc10)
| ~ agent(skc8,x,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ of(skc8,w,skc10)
| ~ theme(skc8,x,u) ),
inference(mrr,[status(thm)],[1100,8,10]),
[iquote('0:MRR:1100.2,1100.5,8.0,10.0')] ).
cnf(1095,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ jules_forename(skc8,v)
| ~ smoke(u,w)
| ~ present(u,w)
| ~ man(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ of(skc8,v,x)
| ~ agent(u,w,x)
| ~ agent(skc8,z,x)
| ~ agent(skc8,skc13,x)
| ~ of(skc8,y,x)
| ~ theme(skc8,z,u) ),
inference(mrr,[status(thm)],[1092,7,6,5]),
[iquote('0:MRR:1092.2,1092.3,1092.4,7.0,6.0,5.0')] ).
cnf(1060,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ jules_forename(skc8,w)
| ~ smoke(u,x)
| ~ present(u,x)
| ~ man(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ theme(skc8,v,skc12)
| ~ of(skc8,w,y)
| ~ agent(u,x,y)
| ~ agent(skc8,x1,y)
| ~ agent(skc8,v,y)
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,u) ),
inference(mrr,[status(thm)],[1057,8]),
[iquote('0:MRR:1057.0,8.0')] ).
cnf(1088,plain,
( ~ smoke(u,skc13)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ jules_forename(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ theme(skc8,w,v)
| ~ of(skc8,x,skc15)
| ~ agent(skc8,w,skc15)
| ~ of(skc8,y,skc15)
| ~ theme(skc8,skc13,u)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1085,8]),
[iquote('0:MRR:1085.1,8.0')] ).
cnf(1079,plain,
( ~ vincent_forename(skc8,skc11)
| ~ agent(skc8,skc13,skc10)
| man(skc12,skf4(skc12)) ),
inference(res,[status(thm),theory(equality)],[17,1078]),
[iquote('0:Res:17.0,1078.1')] ).
cnf(700,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ jules_forename(skc8,x)
| ~ smoke(u,y)
| ~ present(u,y)
| ~ man(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ theme(skc8,w,v)
| ~ of(skc8,x,z)
| ~ agent(u,y,z)
| ~ agent(skc8,x2,z)
| ~ agent(skc8,w,z)
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,u)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[698,8]),
[iquote('0:MRR:698.0,8.0')] ).
cnf(1078,plain,
( ~ vincent_forename(skc8,u)
| ~ of(skc8,u,skc10)
| ~ agent(skc8,skc13,skc10)
| man(skc12,skf4(skc12)) ),
inference(mrr,[status(thm)],[1072,8,10]),
[iquote('0:MRR:1072.0,1072.1,8.0,10.0')] ).
cnf(1069,plain,
( ~ jules_forename(skc8,u)
| ~ man(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ of(skc8,u,v)
| ~ of(skc8,w,v)
| ~ agent(skc8,skc13,v)
| man(skc12,skf4(skc12)) ),
inference(mrr,[status(thm)],[1068,13,12,7,6,5]),
[iquote('0:MRR:1068.0,1068.1,1068.2,1068.3,1068.4,13.0,12.0,7.0,6.0,5.0')] ).
cnf(1064,plain,
( ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ jules_forename(skc8,w)
| ~ man(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ of(skc8,y,x)
| ~ agent(skc8,skc13,x)
| man(u,skf4(u)) ),
inference(mrr,[status(thm)],[1061,8]),
[iquote('0:MRR:1061.0,8.0')] ).
cnf(876,plain,
( ~ agent(skc8,u,skf4(skc12))
| ~ smoke(skc12,u)
| ~ present(skc12,u)
| ~ state(skc8,v)
| ~ man(skc8,w)
| ~ jules_forename(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ jules_forename(skc8,z)
| ~ smoke(skc12,x1)
| ~ present(skc12,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ of(skc8,x,w)
| ~ theme(skc8,y,skc12)
| ~ of(skc8,z,x2)
| ~ agent(skc12,x1,x2)
| ~ agent(skc8,y,x2)
| ~ of(skc8,x3,x2)
| ~ be(skc8,v,w,w) ),
inference(mrr,[status(thm)],[875,13,12]),
[iquote('0:MRR:875.6,875.7,13.0,12.0')] ).
cnf(1006,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ jules_forename(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ jules_forename(skc8,x)
| ~ man(skc8,v)
| ~ vincent_forename(skc8,y)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ of(skc8,w,skc10)
| ~ of(skc8,x,v)
| ~ agent(skc8,z,v)
| ~ of(skc8,y,v)
| ~ theme(skc8,z,u)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[999,122]),
[iquote('0:MRR:999.0,122.1')] ).
cnf(98,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ event(skc8,x6)
| ~ present(skc8,x6)
| ~ think_believe_consider(skc8,x6)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,w)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x6,x4)
| ~ agent(skc8,x2,x4)
| ~ of(skc8,x5,x4)
| ~ theme(skc8,x6,u)
| ~ be(skc8,y,z,z) ),
inference(res,[status(thm),theory(equality)],[1,97]),
[iquote('0:Res:1.0,97.0')] ).
cnf(1032,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,skc8)
| ~ vincent_forename(skc8,u)
| ~ event(skc8,skf2(skc10))
| ~ present(skc8,skf2(skc10))
| ~ think_believe_consider(skc8,skf2(skc10))
| ~ of(skc8,u,skc10)
| ~ theme(skc8,skf2(skc10),skc12)
| ~ agent(skc8,skc13,skc10) ),
inference(res,[status(thm),theory(equality)],[511,1018]),
[iquote('0:Res:511.2,1018.4')] ).
cnf(1018,plain,
( ~ vincent_forename(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ agent(skc8,v,skc10)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,v,skc12)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1011,8,10]),
[iquote('0:MRR:1011.0,1011.1,8.0,10.0')] ).
cnf(1027,plain,
~ jules_forename(skc8,skc14),
inference(mrr,[status(thm)],[1024,4]),
[iquote('0:MRR:1024.1,4.0')] ).
cnf(182,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ proposition(u,y)
| ~ accessible_world(u,y)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ jules_forename(u,x1)
| ~ man(u,x2)
| ~ vincent_forename(u,x3)
| ~ event(u,x4)
| ~ present(u,x4)
| ~ think_believe_consider(u,x4)
| ~ smoke(y,x5)
| ~ present(y,x5)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,x,w)
| ~ theme(u,z,y)
| ~ of(u,x1,x2)
| ~ agent(u,x4,x2)
| ~ agent(u,z,x2)
| ~ of(u,x3,x2)
| ~ theme(u,x4,skc8)
| ~ agent(y,x5,skf4(y))
| ~ agent(skc8,skc13,x2)
| ~ be(u,v,w,w) ),
inference(res,[status(thm),theory(equality)],[6,97]),
[iquote('0:Res:6.0,97.14')] ).
cnf(1010,plain,
( ~ jules_forename(skc8,u)
| ~ man(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ of(skc8,u,v)
| ~ agent(skc8,x,v)
| ~ of(skc8,w,v)
| ~ theme(skc8,x,skc12)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[1007,8]),
[iquote('0:MRR:1007.0,8.0')] ).
cnf(181,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ jules_forename(u,x1)
| ~ smoke(y,x2)
| ~ present(y,x2)
| ~ man(u,x3)
| ~ vincent_forename(u,x4)
| ~ event(u,x5)
| ~ present(u,x5)
| ~ think_believe_consider(u,x5)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,x,w)
| ~ of(u,x1,x3)
| ~ agent(y,x2,x3)
| ~ agent(u,x5,x3)
| ~ agent(u,z,x3)
| ~ of(u,x4,x3)
| ~ theme(u,x5,y)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,skf4(skc8))
| ~ be(u,v,w,w) ),
inference(res,[status(thm),theory(equality)],[6,97]),
[iquote('0:Res:6.0,97.2')] ).
cnf(990,plain,
( ~ man(skc8,skf4(skc12))
| ~ jules_forename(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ jules_forename(skc8,w)
| ~ smoke(skc12,x)
| ~ present(skc12,x)
| ~ man(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,v,skc12)
| ~ of(skc8,w,y)
| ~ agent(skc12,x,y)
| ~ agent(skc8,v,y)
| ~ of(skc8,z,y) ),
inference(res,[status(thm),theory(equality)],[122,984]),
[iquote('0:Res:122.1,984.0')] ).
cnf(984,plain,
( ~ man(skc12,skf4(skc12))
| ~ jules_forename(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ jules_forename(skc8,w)
| ~ smoke(skc12,x)
| ~ present(skc12,x)
| ~ man(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,v,skc12)
| ~ of(skc8,w,y)
| ~ agent(skc12,x,y)
| ~ agent(skc8,v,y)
| ~ of(skc8,z,y) ),
inference(mrr,[status(thm)],[981,11,10]),
[iquote('0:MRR:981.1,981.2,11.0,10.0')] ).
cnf(203,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,w)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x5,x4)
| ~ agent(skc8,x2,x4)
| ~ theme(skc8,x5,u)
| ~ of(skc8,skc14,x4)
| ~ be(skc8,y,z,z) ),
inference(mrr,[status(thm)],[192,1]),
[iquote('0:MRR:192.0,1.0')] ).
cnf(878,plain,
( ~ man(skc12,skf4(skc12))
| ~ state(skc8,u)
| ~ man(skc8,v)
| ~ jules_forename(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ jules_forename(skc8,y)
| ~ smoke(skc12,z)
| ~ present(skc12,z)
| ~ man(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ of(skc8,w,v)
| ~ theme(skc8,x,skc12)
| ~ of(skc8,y,x1)
| ~ agent(skc12,z,x1)
| ~ agent(skc8,x,x1)
| ~ of(skc8,x2,x1)
| ~ be(skc8,u,v,v) ),
inference(mrr,[status(thm)],[877,216,220,13,12]),
[iquote('0:MRR:877.1,877.2,877.6,877.7,216.0,220.0,13.0,12.0')] ).
cnf(975,plain,
( ~ proposition(skc12,skc12)
| ~ proposition(skc12,u)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,v)
| ~ theme(skc12,v,u)
| ~ agent(skc12,v,w)
| ~ agent(skc12,skc13,w)
| equal(skc12,u) ),
inference(res,[status(thm),theory(equality)],[16,596]),
[iquote('0:Res:16.0,596.0')] ).
cnf(596,plain,
( ~ theme(skc8,u,v)
| ~ proposition(skc12,v)
| ~ proposition(skc12,w)
| ~ think_believe_consider(skc12,u)
| ~ think_believe_consider(skc12,x)
| ~ theme(skc12,x,w)
| ~ agent(skc12,x,y)
| ~ agent(skc12,u,y)
| equal(v,w) ),
inference(res,[status(thm),theory(equality)],[140,93]),
[iquote('0:Res:140.1,93.4')] ).
cnf(827,plain,
( ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ proposition(u,v)
| ~ think_believe_consider(u,skc13)
| ~ think_believe_consider(u,w)
| ~ theme(u,w,v)
| ~ agent(u,w,x)
| ~ agent(u,skc13,x)
| equal(skc12,v) ),
inference(res,[status(thm),theory(equality)],[825,93]),
[iquote('0:Res:825.1,93.4')] ).
cnf(206,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,x1,w)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x5,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,x5,u)
| ~ of(skc8,skc11,z)
| ~ be(skc8,y,z,z) ),
inference(mrr,[status(thm)],[167,1]),
[iquote('0:MRR:167.0,1.0')] ).
cnf(962,plain,
( ~ theme(skc8,u,v)
| ~ proposition(skc12,v)
| ~ think_believe_consider(skc12,u)
| ~ agent(skc12,u,w)
| ~ agent(skc12,skc13,w)
| equal(skc12,v) ),
inference(mrr,[status(thm)],[961,12]),
[iquote('0:MRR:961.1,12.0')] ).
cnf(549,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(u,v)
| ~ think_believe_consider(u,w)
| ~ theme(u,w,v)
| ~ agent(u,w,x)
| ~ agent(u,skc13,x)
| equal(skc12,v) ),
inference(mrr,[status(thm)],[547,101,170]),
[iquote('0:MRR:547.1,547.3,101.1,170.1')] ).
cnf(941,plain,
( ~ forename(skc12,u)
| ~ forename(skc12,skc11)
| ~ entity(skc12,skc10)
| ~ of(skc12,u,skc10)
| equal(skc11,u) ),
inference(res,[status(thm),theory(equality)],[17,603]),
[iquote('0:Res:17.0,603.0')] ).
cnf(942,plain,
( ~ forename(skc12,u)
| ~ forename(skc12,skc14)
| ~ entity(skc12,skc15)
| ~ of(skc12,u,skc15)
| equal(skc14,u) ),
inference(res,[status(thm),theory(equality)],[14,603]),
[iquote('0:Res:14.0,603.0')] ).
cnf(207,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,w)
| ~ agent(skc8,x5,x3)
| ~ agent(skc8,x2,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,x5,u)
| ~ of(skc8,skc11,x3)
| ~ be(skc8,y,z,z) ),
inference(mrr,[status(thm)],[165,1]),
[iquote('0:MRR:165.0,1.0')] ).
cnf(603,plain,
( ~ of(skc8,u,v)
| ~ forename(skc12,w)
| ~ forename(skc12,u)
| ~ entity(skc12,v)
| ~ of(skc12,w,v)
| equal(u,w) ),
inference(res,[status(thm),theory(equality)],[139,92]),
[iquote('0:Res:139.1,92.3')] ).
cnf(846,plain,
( ~ accessible_world(skc12,u)
| ~ forename(u,v)
| ~ forename(u,skc14)
| ~ entity(u,skc15)
| ~ of(u,v,skc15)
| equal(skc14,v) ),
inference(res,[status(thm),theory(equality)],[843,92]),
[iquote('0:Res:843.1,92.3')] ).
cnf(841,plain,
( ~ accessible_world(skc12,u)
| ~ forename(u,v)
| ~ forename(u,skc11)
| ~ entity(u,skc10)
| ~ of(u,v,skc10)
| equal(skc11,v) ),
inference(res,[status(thm),theory(equality)],[832,92]),
[iquote('0:Res:832.1,92.3')] ).
cnf(924,plain,
( ~ of(skc8,u,skc15)
| ~ forename(skc12,u)
| ~ forename(skc12,skc14)
| ~ entity(skc12,skc15)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[923,12]),
[iquote('0:MRR:923.1,12.0')] ).
cnf(210,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ of(skc8,z,y)
| ~ theme(skc8,x1,w)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x5,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,x5,u)
| ~ be(skc8,skc9,y,y) ),
inference(mrr,[status(thm)],[150,1]),
[iquote('0:MRR:150.0,1.0')] ).
cnf(527,plain,
( ~ accessible_world(skc8,u)
| ~ forename(u,v)
| ~ forename(u,skc14)
| ~ entity(u,skc15)
| ~ of(u,v,skc15)
| equal(skc14,v) ),
inference(res,[status(thm),theory(equality)],[499,92]),
[iquote('0:Res:499.1,92.3')] ).
cnf(916,plain,
( ~ of(skc8,u,skc10)
| ~ forename(skc12,u)
| ~ entity(skc12,skc10)
| equal(skc11,u) ),
inference(mrr,[status(thm)],[915,12]),
[iquote('0:MRR:915.1,12.0')] ).
cnf(530,plain,
( ~ accessible_world(skc8,u)
| ~ forename(u,v)
| ~ entity(u,skc10)
| ~ of(u,v,skc10)
| equal(skc11,v) ),
inference(mrr,[status(thm)],[526,158]),
[iquote('0:MRR:526.2,158.1')] ).
cnf(907,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skf2(skc15),skc15) ),
inference(res,[status(thm),theory(equality)],[2,903]),
[iquote('0:Res:2.0,903.0')] ).
cnf(208,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ jules_forename(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,x1,w)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x5,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,x5,u)
| ~ of(skc8,z,skc10)
| ~ be(skc8,y,skc10,skc10) ),
inference(mrr,[status(thm)],[157,1]),
[iquote('0:MRR:157.0,1.0')] ).
cnf(903,plain,
( ~ man(skc8,u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(v,w)
| agent(w,skf2(u),u) ),
inference(res,[status(thm),theory(equality)],[122,634]),
[iquote('0:Res:122.1,634.0')] ).
cnf(905,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skf2(skc10),skc10) ),
inference(mrr,[status(thm)],[904,12]),
[iquote('0:MRR:904.0,12.0')] ).
cnf(634,plain,
( ~ man(skc12,u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(v,w)
| agent(w,skf2(u),u) ),
inference(res,[status(thm),theory(equality)],[511,90]),
[iquote('0:Res:511.2,90.1')] ).
cnf(689,plain,
( ~ proposition(skc8,u)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,v)
| equal(skc12,u) ),
inference(mrr,[status(thm)],[688,13,7]),
[iquote('0:MRR:688.0,688.2,13.0,7.0')] ).
cnf(209,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,skc10)
| ~ agent(w,x,skf4(w))
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,w)
| ~ theme(skc8,x5,u)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x5,skc10)
| ~ agent(skc8,x2,skc10)
| ~ of(skc8,x4,skc10)
| ~ be(skc8,y,z,z) ),
inference(mrr,[status(thm)],[156,1]),
[iquote('0:MRR:156.0,1.0')] ).
cnf(622,plain,
( ~ be(skc8,u,v,w)
| ~ accessible_world(skc12,x)
| be(x,u,v,w) ),
inference(res,[status(thm),theory(equality)],[143,91]),
[iquote('0:Res:143.1,91.1')] ).
cnf(613,plain,
( ~ agent(skc8,u,v)
| ~ accessible_world(skc12,w)
| agent(w,u,v) ),
inference(res,[status(thm),theory(equality)],[141,90]),
[iquote('0:Res:141.1,90.1')] ).
cnf(604,plain,
( ~ of(skc8,u,v)
| ~ accessible_world(skc12,w)
| of(w,u,v) ),
inference(res,[status(thm),theory(equality)],[139,88]),
[iquote('0:Res:139.1,88.1')] ).
cnf(595,plain,
( ~ theme(skc8,u,v)
| ~ accessible_world(skc12,w)
| theme(w,u,v) ),
inference(res,[status(thm),theory(equality)],[140,89]),
[iquote('0:Res:140.1,89.1')] ).
cnf(212,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ state(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ smoke(skc12,x2)
| ~ present(skc12,x2)
| ~ man(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ event(skc8,x5)
| ~ present(skc8,x5)
| ~ think_believe_consider(skc8,x5)
| ~ agent(u,v,skf4(u))
| ~ of(skc8,y,x)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,x3)
| ~ agent(skc12,x2,x3)
| ~ agent(skc8,x5,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,x5,skc12)
| ~ be(skc8,w,x,x) ),
inference(mrr,[status(thm)],[142,1,13]),
[iquote('0:MRR:142.0,142.24,1.0,13.0')] ).
cnf(870,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| be(v,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[860,91]),
[iquote('0:Res:860.1,91.1')] ).
cnf(860,plain,
( ~ accessible_world(skc12,u)
| be(u,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[12,588]),
[iquote('0:Res:12.0,588.0')] ).
cnf(588,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| be(v,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[516,91]),
[iquote('0:Res:516.1,91.1')] ).
cnf(855,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[848,90]),
[iquote('0:Res:848.1,90.1')] ).
cnf(847,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| of(v,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[843,88]),
[iquote('0:Res:843.1,88.1')] ).
cnf(842,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| of(v,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[832,88]),
[iquote('0:Res:832.1,88.1')] ).
cnf(826,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| theme(v,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[825,89]),
[iquote('0:Res:825.1,89.1')] ).
cnf(848,plain,
( ~ accessible_world(skc12,u)
| agent(u,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[12,523]),
[iquote('0:Res:12.0,523.0')] ).
cnf(578,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ jules_forename(u,x1)
| ~ smoke(y,x2)
| ~ present(y,x2)
| ~ man(u,x3)
| ~ vincent_forename(u,x4)
| ~ event(u,x5)
| ~ present(u,x5)
| ~ think_believe_consider(u,x5)
| ~ of(u,x,w)
| ~ theme(u,z,skc12)
| ~ of(u,x1,x3)
| ~ agent(y,x2,x3)
| ~ agent(u,x5,x3)
| ~ agent(u,z,x3)
| ~ of(u,x4,x3)
| ~ theme(u,x5,y)
| ~ be(u,v,w,w) ),
inference(mrr,[status(thm)],[577,96,216,220]),
[iquote('0:MRR:577.1,577.20,577.21,96.28,216.0,220.0')] ).
cnf(523,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| agent(v,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[510,90]),
[iquote('0:Res:510.1,90.1')] ).
cnf(843,plain,
( ~ accessible_world(skc12,u)
| of(u,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[12,513]),
[iquote('0:Res:12.0,513.0')] ).
cnf(513,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| of(v,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[499,88]),
[iquote('0:Res:499.1,88.1')] ).
cnf(832,plain,
( ~ accessible_world(skc12,u)
| of(u,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[12,512]),
[iquote('0:Res:12.0,512.0')] ).
cnf(177,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ proposition(u,y)
| ~ accessible_world(u,y)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ jules_forename(u,x1)
| ~ man(u,x2)
| ~ vincent_forename(u,x3)
| ~ event(u,x4)
| ~ present(u,x4)
| ~ think_believe_consider(u,x4)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,x,w)
| ~ theme(u,z,y)
| ~ of(u,x1,x2)
| ~ agent(u,x4,x2)
| ~ agent(u,z,x2)
| ~ of(u,x3,x2)
| ~ theme(u,x4,skc8)
| ~ agent(skc8,skc13,x2)
| ~ be(u,v,w,w)
| man(y,skf4(y)) ),
inference(res,[status(thm),theory(equality)],[6,96]),
[iquote('0:Res:6.0,96.11')] ).
cnf(512,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| of(v,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[498,88]),
[iquote('0:Res:498.1,88.1')] ).
cnf(825,plain,
( ~ accessible_world(skc12,u)
| theme(u,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[12,504]),
[iquote('0:Res:12.0,504.0')] ).
cnf(504,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| theme(v,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[489,89]),
[iquote('0:Res:489.1,89.1')] ).
cnf(818,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc14) ),
inference(res,[status(thm),theory(equality)],[189,806]),
[iquote('0:Res:189.1,806.0')] ).
cnf(806,plain,
( ~ vincent_forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[20,800]),
[iquote('0:Res:20.1,800.0')] ).
cnf(805,plain,
( ~ jules_forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[19,800]),
[iquote('0:Res:19.1,800.0')] ).
cnf(804,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc11) ),
inference(res,[status(thm),theory(equality)],[158,800]),
[iquote('0:Res:158.1,800.0')] ).
cnf(205,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ state(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ of(skc8,x1,z)
| ~ theme(skc8,x2,w)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x2,x4)
| ~ of(skc8,x5,x4)
| ~ agent(skc8,skc13,x4)
| ~ theme(skc8,skc13,u)
| ~ be(skc8,y,z,z) ),
inference(mrr,[status(thm)],[187,1,7,6]),
[iquote('0:MRR:187.0,187.4,187.5,1.0,7.0,6.0')] ).
cnf(800,plain,
( ~ forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[22,775]),
[iquote('0:Res:22.1,775.0')] ).
cnf(775,plain,
( ~ relname(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[21,744]),
[iquote('0:Res:21.1,744.0')] ).
cnf(796,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(u,skc9) ),
inference(res,[status(thm),theory(equality)],[146,774]),
[iquote('0:Res:146.1,774.1')] ).
cnf(774,plain,
( ~ proposition(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[41,744]),
[iquote('0:Res:41.1,744.0')] ).
cnf(193,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ state(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,z)
| ~ accessible_world(skc8,z)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(u,v,x3)
| ~ of(skc8,y,x)
| ~ theme(skc8,x1,z)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x4,x3)
| ~ agent(skc8,x1,x3)
| ~ theme(skc8,x4,u)
| ~ of(skc8,skc14,x3)
| ~ be(skc8,w,x,x)
| man(z,skf4(z)) ),
inference(mrr,[status(thm)],[191,1]),
[iquote('0:MRR:191.0,1.0')] ).
cnf(770,plain,
( ~ human_person(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[32,742]),
[iquote('0:Res:32.1,742.0')] ).
cnf(768,plain,
( ~ human_person(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[32,740]),
[iquote('0:Res:32.1,740.0')] ).
cnf(782,plain,
( ~ accessible_world(skc8,u)
| ~ general(u,skc10) ),
inference(res,[status(thm),theory(equality)],[151,746]),
[iquote('0:Res:151.1,746.0')] ).
cnf(746,plain,
( ~ man(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[33,717]),
[iquote('0:Res:33.1,717.0')] ).
cnf(197,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ state(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,z)
| ~ accessible_world(skc8,z)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ man(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(u,v,x2)
| ~ of(skc8,y,x)
| ~ theme(skc8,x1,z)
| ~ agent(skc8,x4,x2)
| ~ agent(skc8,x1,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,x4,u)
| ~ of(skc8,skc11,x2)
| ~ be(skc8,w,x,x)
| man(z,skf4(z)) ),
inference(mrr,[status(thm)],[164,1]),
[iquote('0:MRR:164.0,1.0')] ).
cnf(744,plain,
( ~ relation(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[40,684]),
[iquote('0:Res:40.1,684.0')] ).
cnf(742,plain,
( ~ organism(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[31,616]),
[iquote('0:Res:31.1,616.0')] ).
cnf(740,plain,
( ~ organism(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[31,592]),
[iquote('0:Res:31.1,592.0')] ).
cnf(762,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc10) ),
inference(res,[status(thm),theory(equality)],[151,729]),
[iquote('0:Res:151.1,729.0')] ).
cnf(199,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ state(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ proposition(skc8,z)
| ~ accessible_world(skc8,z)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ event(skc8,x4)
| ~ present(skc8,x4)
| ~ think_believe_consider(skc8,x4)
| ~ agent(u,v,skc10)
| ~ of(skc8,y,x)
| ~ theme(skc8,x1,z)
| ~ theme(skc8,x4,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x4,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ be(skc8,w,x,x)
| man(z,skf4(z)) ),
inference(mrr,[status(thm)],[154,1]),
[iquote('0:MRR:154.0,1.0')] ).
cnf(729,plain,
( ~ man(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[23,554]),
[iquote('0:Res:23.1,554.1')] ).
cnf(755,plain,
( ~ accessible_world(skc8,u)
| ~ man(u,skc13) ),
inference(res,[status(thm),theory(equality)],[184,721]),
[iquote('0:Res:184.1,721.1')] ).
cnf(754,plain,
~ man(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[217,721]),
[iquote('0:Res:217.0,721.1')] ).
cnf(721,plain,
( ~ man(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[23,553]),
[iquote('0:Res:23.1,553.1')] ).
cnf(717,plain,
( ~ human_person(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[32,545]),
[iquote('0:Res:32.1,545.0')] ).
cnf(684,plain,
( ~ abstraction(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[37,543]),
[iquote('0:Res:37.1,543.1')] ).
cnf(616,plain,
( ~ entity(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[28,538]),
[iquote('0:Res:28.1,538.1')] ).
cnf(592,plain,
( ~ entity(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[28,537]),
[iquote('0:Res:28.1,537.1')] ).
cnf(557,plain,
( ~ man(u,v)
| ~ abstraction(u,v) ),
inference(res,[status(thm),theory(equality)],[23,247]),
[iquote('0:Res:23.1,247.1')] ).
cnf(728,plain,
( ~ male(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[113,554]),
[iquote('0:Res:113.1,554.1')] ).
cnf(554,plain,
( ~ state(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[35,246]),
[iquote('0:Res:35.1,246.0')] ).
cnf(720,plain,
( ~ male(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[113,553]),
[iquote('0:Res:113.1,553.1')] ).
cnf(553,plain,
( ~ event(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[47,246]),
[iquote('0:Res:47.1,246.0')] ).
cnf(545,plain,
( ~ organism(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[31,239]),
[iquote('0:Res:31.1,239.0')] ).
cnf(708,plain,
( ~ vincent_forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[20,702]),
[iquote('0:Res:20.1,702.0')] ).
cnf(707,plain,
( ~ jules_forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[19,702]),
[iquote('0:Res:19.1,702.0')] ).
cnf(705,plain,
~ state(skc12,skc14),
inference(res,[status(thm),theory(equality)],[3,702]),
[iquote('0:Res:3.0,702.0')] ).
cnf(702,plain,
( ~ forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[22,694]),
[iquote('0:Res:22.1,694.0')] ).
cnf(701,plain,
~ state(skc12,skc11),
inference(res,[status(thm),theory(equality)],[159,694]),
[iquote('0:Res:159.0,694.0')] ).
cnf(694,plain,
( ~ relname(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[21,691]),
[iquote('0:Res:21.1,691.0')] ).
cnf(693,plain,
( ~ proposition(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[41,691]),
[iquote('0:Res:41.1,691.0')] ).
cnf(692,plain,
~ state(skc12,skc12),
inference(res,[status(thm),theory(equality)],[102,691]),
[iquote('0:Res:102.0,691.0')] ).
cnf(691,plain,
( ~ relation(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[40,685]),
[iquote('0:Res:40.1,685.0')] ).
cnf(685,plain,
( ~ abstraction(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[37,683]),
[iquote('0:Res:37.1,683.0')] ).
cnf(172,plain,
( ~ proposition(skc8,u)
| ~ proposition(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ theme(skc8,w,u)
| ~ agent(skc8,w,x)
| ~ theme(skc8,skc13,v)
| ~ agent(skc8,skc13,x)
| equal(u,v) ),
inference(res,[status(thm),theory(equality)],[7,93]),
[iquote('0:Res:7.0,93.3')] ).
cnf(683,plain,
( ~ general(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[124,543]),
[iquote('0:Res:124.1,543.1')] ).
cnf(543,plain,
( ~ state(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[35,238]),
[iquote('0:Res:35.1,238.0')] ).
cnf(678,plain,
( ~ vincent_forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,675]),
[iquote('0:Res:20.1,675.0')] ).
cnf(677,plain,
( ~ jules_forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,675]),
[iquote('0:Res:19.1,675.0')] ).
cnf(105,plain,
( ~ proposition(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ theme(skc8,w,u)
| ~ agent(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ theme(skc8,v,skc12)
| equal(skc12,u) ),
inference(res,[status(thm),theory(equality)],[13,93]),
[iquote('0:Res:13.0,93.7')] ).
cnf(675,plain,
( ~ forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[22,672]),
[iquote('0:Res:22.1,672.0')] ).
cnf(672,plain,
( ~ relname(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[21,667]),
[iquote('0:Res:21.1,667.0')] ).
cnf(671,plain,
( ~ proposition(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[41,667]),
[iquote('0:Res:41.1,667.0')] ).
cnf(667,plain,
( ~ relation(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[40,665]),
[iquote('0:Res:40.1,665.0')] ).
cnf(548,plain,
( ~ proposition(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ theme(skc8,v,u)
| ~ agent(skc8,v,w)
| ~ agent(skc8,skc13,w)
| equal(skc12,u) ),
inference(mrr,[status(thm)],[546,13,7]),
[iquote('0:MRR:546.0,546.2,13.0,7.0')] ).
cnf(665,plain,
( ~ abstraction(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[37,629]),
[iquote('0:Res:37.1,629.1')] ).
cnf(629,plain,
( ~ accessible_world(skc8,u)
| ~ general(u,skc13) ),
inference(res,[status(thm),theory(equality)],[184,542]),
[iquote('0:Res:184.1,542.0')] ).
cnf(656,plain,
~ vincent_forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[20,649]),
[iquote('0:Res:20.1,649.0')] ).
cnf(655,plain,
~ jules_forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[19,649]),
[iquote('0:Res:19.1,649.0')] ).
cnf(161,plain,
( ~ forename(skc8,u)
| ~ entity(skc8,v)
| ~ of(skc8,u,v)
| ~ of(skc8,skc11,v)
| equal(u,skc11) ),
inference(res,[status(thm),theory(equality)],[9,92]),
[iquote('0:Res:9.0,92.4')] ).
cnf(654,plain,
~ vincent_forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[20,648]),
[iquote('0:Res:20.1,648.0')] ).
cnf(653,plain,
~ jules_forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[19,648]),
[iquote('0:Res:19.1,648.0')] ).
cnf(649,plain,
~ forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[22,643]),
[iquote('0:Res:22.1,643.0')] ).
cnf(648,plain,
~ forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[22,641]),
[iquote('0:Res:22.1,641.0')] ).
cnf(529,plain,
( ~ forename(skc8,u)
| ~ entity(skc8,skc10)
| ~ of(skc8,u,skc10)
| equal(skc11,u) ),
inference(mrr,[status(thm)],[524,9]),
[iquote('0:MRR:524.1,9.0')] ).
cnf(643,plain,
~ relname(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[21,638]),
[iquote('0:Res:21.1,638.0')] ).
cnf(642,plain,
~ proposition(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[41,638]),
[iquote('0:Res:41.1,638.0')] ).
cnf(641,plain,
~ relname(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[21,637]),
[iquote('0:Res:21.1,637.0')] ).
cnf(640,plain,
~ proposition(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[41,637]),
[iquote('0:Res:41.1,637.0')] ).
cnf(528,plain,
( ~ forename(skc8,u)
| ~ entity(skc8,skc15)
| ~ of(skc8,u,skc15)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[525,3]),
[iquote('0:MRR:525.1,3.0')] ).
cnf(638,plain,
~ relation(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[40,633]),
[iquote('0:Res:40.1,633.0')] ).
cnf(637,plain,
~ relation(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[40,632]),
[iquote('0:Res:40.1,632.0')] ).
cnf(633,plain,
~ abstraction(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[37,631]),
[iquote('0:Res:37.1,631.0')] ).
cnf(632,plain,
~ abstraction(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[37,628]),
[iquote('0:Res:37.1,628.0')] ).
cnf(511,plain,
( ~ man(skc12,u)
| ~ accessible_world(skc12,v)
| agent(v,skf2(u),u) ),
inference(res,[status(thm),theory(equality)],[56,90]),
[iquote('0:Res:56.1,90.1')] ).
cnf(631,plain,
~ general(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[124,628]),
[iquote('0:Res:124.1,628.0')] ).
cnf(628,plain,
~ general(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[217,542]),
[iquote('0:Res:217.0,542.0')] ).
cnf(542,plain,
( ~ event(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[47,238]),
[iquote('0:Res:47.1,238.0')] ).
cnf(619,plain,
( ~ human_person(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[32,618]),
[iquote('0:Res:32.1,618.0')] ).
cnf(143,plain,
( ~ be(skc8,u,v,w)
| be(skc12,u,v,w) ),
inference(res,[status(thm),theory(equality)],[12,91]),
[iquote('0:Res:12.0,91.1')] ).
cnf(618,plain,
( ~ organism(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[31,617]),
[iquote('0:Res:31.1,617.0')] ).
cnf(617,plain,
( ~ entity(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[28,615]),
[iquote('0:Res:28.1,615.0')] ).
cnf(615,plain,
( ~ existent(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[118,538]),
[iquote('0:Res:118.1,538.1')] ).
cnf(538,plain,
( ~ state(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[35,229]),
[iquote('0:Res:35.1,229.0')] ).
cnf(141,plain,
( ~ agent(skc8,u,v)
| agent(skc12,u,v) ),
inference(res,[status(thm),theory(equality)],[12,90]),
[iquote('0:Res:12.0,90.1')] ).
cnf(610,plain,
~ state(skc12,skc15),
inference(res,[status(thm),theory(equality)],[2,608]),
[iquote('0:Res:2.0,608.1')] ).
cnf(608,plain,
( ~ state(skc12,u)
| ~ man(skc8,u) ),
inference(res,[status(thm),theory(equality)],[34,599]),
[iquote('0:Res:34.1,599.1')] ).
cnf(606,plain,
~ man(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[217,599]),
[iquote('0:Res:217.0,599.1')] ).
cnf(599,plain,
( ~ man(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[33,597]),
[iquote('0:Res:33.1,597.0')] ).
cnf(139,plain,
( ~ of(skc8,u,v)
| of(skc12,u,v) ),
inference(res,[status(thm),theory(equality)],[12,88]),
[iquote('0:Res:12.0,88.1')] ).
cnf(601,plain,
~ state(skc12,skc10),
inference(res,[status(thm),theory(equality)],[34,598]),
[iquote('0:Res:34.1,598.0')] ).
cnf(598,plain,
~ event(skc12,skc10),
inference(res,[status(thm),theory(equality)],[153,597]),
[iquote('0:Res:153.0,597.0')] ).
cnf(597,plain,
( ~ human_person(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[32,594]),
[iquote('0:Res:32.1,594.0')] ).
cnf(594,plain,
( ~ organism(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[31,593]),
[iquote('0:Res:31.1,593.0')] ).
cnf(140,plain,
( ~ theme(skc8,u,v)
| theme(skc12,u,v) ),
inference(res,[status(thm),theory(equality)],[12,89]),
[iquote('0:Res:12.0,89.1')] ).
cnf(593,plain,
( ~ entity(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[28,591]),
[iquote('0:Res:28.1,591.0')] ).
cnf(591,plain,
( ~ existent(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[118,537]),
[iquote('0:Res:118.1,537.1')] ).
cnf(537,plain,
( ~ event(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[47,229]),
[iquote('0:Res:47.1,229.0')] ).
cnf(584,plain,
( ~ vincent_forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,581]),
[iquote('0:Res:20.1,581.0')] ).
cnf(516,plain,
( ~ accessible_world(skc8,u)
| be(u,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[18,91]),
[iquote('0:Res:18.0,91.1')] ).
cnf(583,plain,
( ~ jules_forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,581]),
[iquote('0:Res:19.1,581.0')] ).
cnf(581,plain,
( ~ forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[22,576]),
[iquote('0:Res:22.1,576.0')] ).
cnf(576,plain,
( ~ relname(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[21,573]),
[iquote('0:Res:21.1,573.0')] ).
cnf(575,plain,
( ~ proposition(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[41,573]),
[iquote('0:Res:41.1,573.0')] ).
cnf(97,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ proposition(u,z)
| ~ accessible_world(u,z)
| ~ think_believe_consider(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ jules_forename(u,x2)
| ~ smoke(y,x3)
| ~ present(y,x3)
| ~ man(u,x4)
| ~ vincent_forename(u,x5)
| ~ event(u,x6)
| ~ present(u,x6)
| ~ think_believe_consider(u,x6)
| ~ smoke(z,x7)
| ~ present(z,x7)
| ~ of(u,x,w)
| ~ theme(u,x1,z)
| ~ of(u,x2,x4)
| ~ agent(y,x3,x4)
| ~ agent(u,x6,x4)
| ~ agent(u,x1,x4)
| ~ of(u,x5,x4)
| ~ theme(u,x6,y)
| ~ agent(z,x7,skf4(z))
| ~ be(u,v,w,w) ),
inference(mrr,[status(thm)],[95,48,20,19]),
[iquote('0:MRR:95.4,95.9,95.15,95.21,95.32,48.1,20.1,48.1,19.1,19.1')] ).
cnf(573,plain,
( ~ relation(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[40,571]),
[iquote('0:Res:40.1,571.0')] ).
cnf(571,plain,
( ~ abstraction(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[38,569]),
[iquote('0:Res:38.1,569.1')] ).
cnf(569,plain,
( ~ accessible_world(skc8,u)
| ~ nonhuman(u,skc10) ),
inference(res,[status(thm),theory(equality)],[151,532]),
[iquote('0:Res:151.1,532.0')] ).
cnf(532,plain,
( ~ man(u,v)
| ~ nonhuman(u,v) ),
inference(res,[status(thm),theory(equality)],[33,222]),
[iquote('0:Res:33.1,222.0')] ).
cnf(96,plain,
( ~ actual_world(u)
| ~ state(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ proposition(u,z)
| ~ accessible_world(u,z)
| ~ think_believe_consider(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ jules_forename(u,x2)
| ~ smoke(y,x3)
| ~ present(y,x3)
| ~ man(u,x4)
| ~ vincent_forename(u,x5)
| ~ event(u,x6)
| ~ present(u,x6)
| ~ think_believe_consider(u,x6)
| ~ of(u,x,w)
| ~ theme(u,x1,z)
| ~ of(u,x2,x4)
| ~ agent(y,x3,x4)
| ~ agent(u,x6,x4)
| ~ agent(u,x1,x4)
| ~ of(u,x5,x4)
| ~ theme(u,x6,y)
| ~ be(u,v,w,w)
| man(z,skf4(z)) ),
inference(mrr,[status(thm)],[94,20,48,19]),
[iquote('0:MRR:94.5,94.11,94.17,94.28,20.1,48.1,19.1,19.1')] ).
cnf(559,plain,
( ~ man(skc8,u)
| ~ abstraction(skc12,u) ),
inference(res,[status(thm),theory(equality)],[23,556]),
[iquote('0:Res:23.1,556.0')] ).
cnf(556,plain,
( ~ male(skc8,u)
| ~ abstraction(skc12,u) ),
inference(res,[status(thm),theory(equality)],[113,247]),
[iquote('0:Res:113.1,247.1')] ).
cnf(247,plain,
( ~ abstraction(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[36,55]),
[iquote('0:Res:36.1,55.1')] ).
cnf(246,plain,
( ~ eventuality(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[42,55]),
[iquote('0:Res:42.1,55.1')] ).
cnf(93,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('NLP259+1.p',unknown),
[] ).
cnf(239,plain,
( ~ entity(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[29,54]),
[iquote('0:Res:29.1,54.1')] ).
cnf(238,plain,
( ~ eventuality(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[44,54]),
[iquote('0:Res:44.1,54.1')] ).
cnf(229,plain,
( ~ eventuality(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[43,52]),
[iquote('0:Res:43.1,52.0')] ).
cnf(222,plain,
( ~ human_person(u,v)
| ~ nonhuman(u,v) ),
inference(res,[status(thm),theory(equality)],[25,53]),
[iquote('0:Res:25.1,53.0')] ).
cnf(92,axiom,
( ~ forename(u,v)
| ~ forename(u,w)
| ~ entity(u,x)
| ~ of(u,w,x)
| ~ of(u,v,x)
| equal(w,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(510,plain,
( ~ accessible_world(skc8,u)
| agent(u,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[15,90]),
[iquote('0:Res:15.0,90.1')] ).
cnf(503,plain,
( ~ vincent_forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,488]),
[iquote('0:Res:20.1,488.0')] ).
cnf(91,axiom,
( ~ accessible_world(u,v)
| ~ be(u,w,x,y)
| be(v,w,x,y) ),
file('NLP259+1.p',unknown),
[] ).
cnf(502,plain,
( ~ jules_forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,488]),
[iquote('0:Res:19.1,488.0')] ).
cnf(499,plain,
( ~ accessible_world(skc8,u)
| of(u,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[14,88]),
[iquote('0:Res:14.0,88.1')] ).
cnf(498,plain,
( ~ accessible_world(skc8,u)
| of(u,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[17,88]),
[iquote('0:Res:17.0,88.1')] ).
cnf(506,plain,
~ state(skc8,skc14),
inference(res,[status(thm),theory(equality)],[3,497]),
[iquote('0:Res:3.0,497.0')] ).
cnf(90,axiom,
( ~ accessible_world(u,v)
| ~ agent(u,w,x)
| agent(v,w,x) ),
file('NLP259+1.p',unknown),
[] ).
cnf(489,plain,
( ~ accessible_world(skc8,u)
| theme(u,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[16,89]),
[iquote('0:Res:16.0,89.1')] ).
cnf(488,plain,
( ~ forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[22,459]),
[iquote('0:Res:22.1,459.0')] ).
cnf(496,plain,
~ state(skc8,skc11),
inference(res,[status(thm),theory(equality)],[159,484]),
[iquote('0:Res:159.0,484.0')] ).
cnf(88,axiom,
( ~ accessible_world(u,v)
| ~ of(u,w,x)
| of(v,w,x) ),
file('NLP259+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ accessible_world(u,v)
| ~ theme(u,w,x)
| theme(v,w,x) ),
file('NLP259+1.p',unknown),
[] ).
cnf(459,plain,
( ~ relname(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[21,426]),
[iquote('0:Res:21.1,426.0')] ).
cnf(458,plain,
( ~ proposition(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[41,426]),
[iquote('0:Res:41.1,426.0')] ).
cnf(482,plain,
~ state(skc8,skc12),
inference(res,[status(thm),theory(equality)],[102,456]),
[iquote('0:Res:102.0,456.0')] ).
cnf(79,axiom,
( ~ accessible_world(u,v)
| ~ present(u,w)
| present(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(453,plain,
( ~ human_person(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[32,422]),
[iquote('0:Res:32.1,422.0')] ).
cnf(450,plain,
( ~ human_person(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[32,419]),
[iquote('0:Res:32.1,419.0')] ).
cnf(71,axiom,
( ~ accessible_world(u,v)
| ~ man(u,w)
| man(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(472,plain,
~ state(skc8,skc15),
inference(res,[status(thm),theory(equality)],[2,442]),
[iquote('0:Res:2.0,442.0')] ).
cnf(463,plain,
~ general(skc8,skc15),
inference(res,[status(thm),theory(equality)],[124,461]),
[iquote('0:Res:124.1,461.0')] ).
cnf(77,axiom,
( ~ accessible_world(u,v)
| ~ proposition(u,w)
| proposition(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(461,plain,
~ general(skc12,skc15),
inference(res,[status(thm),theory(equality)],[2,428]),
[iquote('0:Res:2.0,428.0')] ).
cnf(428,plain,
( ~ man(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[33,409]),
[iquote('0:Res:33.1,409.0')] ).
cnf(426,plain,
( ~ relation(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[40,407]),
[iquote('0:Res:40.1,407.0')] ).
cnf(78,axiom,
( ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| think_believe_consider(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(422,plain,
( ~ organism(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[31,401]),
[iquote('0:Res:31.1,401.0')] ).
cnf(419,plain,
( ~ organism(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[31,399]),
[iquote('0:Res:31.1,399.0')] ).
cnf(86,axiom,
( ~ accessible_world(u,v)
| ~ event(u,w)
| event(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(413,plain,
( ~ man(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[23,387]),
[iquote('0:Res:23.1,387.1')] ).
cnf(411,plain,
( ~ man(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[23,386]),
[iquote('0:Res:23.1,386.1')] ).
cnf(58,axiom,
( ~ accessible_world(u,v)
| ~ jules_forename(u,w)
| jules_forename(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(435,plain,
~ state(skc8,skc10),
inference(res,[status(thm),theory(equality)],[34,433]),
[iquote('0:Res:34.1,433.0')] ).
cnf(433,plain,
~ event(skc8,skc10),
inference(res,[status(thm),theory(equality)],[152,410]),
[iquote('0:Res:152.0,410.0')] ).
cnf(429,plain,
~ general(skc8,skc10),
inference(res,[status(thm),theory(equality)],[124,427]),
[iquote('0:Res:124.1,427.0')] ).
cnf(87,axiom,
( ~ accessible_world(u,v)
| ~ smoke(u,w)
| smoke(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(427,plain,
~ general(skc12,skc10),
inference(res,[status(thm),theory(equality)],[153,409]),
[iquote('0:Res:153.0,409.0')] ).
cnf(409,plain,
( ~ human_person(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[32,383]),
[iquote('0:Res:32.1,383.0')] ).
cnf(407,plain,
( ~ abstraction(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[37,330]),
[iquote('0:Res:37.1,330.1')] ).
cnf(72,axiom,
( ~ accessible_world(u,v)
| ~ state(u,w)
| state(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(401,plain,
( ~ entity(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[28,294]),
[iquote('0:Res:28.1,294.1')] ).
cnf(399,plain,
( ~ entity(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[28,293]),
[iquote('0:Res:28.1,293.1')] ).
cnf(59,axiom,
( ~ accessible_world(u,v)
| ~ vincent_forename(u,w)
| vincent_forename(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(396,plain,
( ~ man(skc12,u)
| ~ abstraction(skc8,u) ),
inference(res,[status(thm),theory(equality)],[23,290]),
[iquote('0:Res:23.1,290.1')] ).
cnf(387,plain,
( ~ state(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[35,289]),
[iquote('0:Res:35.1,289.0')] ).
cnf(386,plain,
( ~ event(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[47,289]),
[iquote('0:Res:47.1,289.0')] ).
cnf(383,plain,
( ~ organism(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[31,288]),
[iquote('0:Res:31.1,288.0')] ).
cnf(61,axiom,
( ~ accessible_world(u,v)
| ~ forename(u,w)
| forename(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(330,plain,
( ~ state(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[35,287]),
[iquote('0:Res:35.1,287.0')] ).
cnf(329,plain,
( ~ event(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[47,287]),
[iquote('0:Res:47.1,287.0')] ).
cnf(294,plain,
( ~ state(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[35,286]),
[iquote('0:Res:35.1,286.0')] ).
cnf(293,plain,
( ~ event(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[47,286]),
[iquote('0:Res:47.1,286.0')] ).
cnf(85,axiom,
( ~ accessible_world(u,v)
| ~ eventuality(u,w)
| eventuality(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(290,plain,
( ~ abstraction(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[36,245]),
[iquote('0:Res:36.1,245.0')] ).
cnf(391,plain,
~ male(skc8,skc9),
inference(res,[status(thm),theory(equality)],[113,385]),
[iquote('0:Res:113.1,385.0')] ).
cnf(388,plain,
~ male(skc8,skc13),
inference(res,[status(thm),theory(equality)],[113,384]),
[iquote('0:Res:113.1,384.0')] ).
cnf(385,plain,
~ male(skc12,skc9),
inference(res,[status(thm),theory(equality)],[148,289]),
[iquote('0:Res:148.0,289.0')] ).
cnf(68,axiom,
( ~ accessible_world(u,v)
| ~ entity(u,w)
| entity(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(384,plain,
~ male(skc12,skc13),
inference(res,[status(thm),theory(equality)],[185,289]),
[iquote('0:Res:185.0,289.0')] ).
cnf(289,plain,
( ~ eventuality(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[42,245]),
[iquote('0:Res:42.1,245.0')] ).
cnf(288,plain,
( ~ entity(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[29,237]),
[iquote('0:Res:29.1,237.0')] ).
cnf(378,plain,
~ vincent_forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[20,368]),
[iquote('0:Res:20.1,368.0')] ).
cnf(70,axiom,
( ~ accessible_world(u,v)
| ~ human_person(u,w)
| human_person(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(377,plain,
~ jules_forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[19,368]),
[iquote('0:Res:19.1,368.0')] ).
cnf(373,plain,
~ vincent_forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[20,363]),
[iquote('0:Res:20.1,363.0')] ).
cnf(372,plain,
~ jules_forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[19,363]),
[iquote('0:Res:19.1,363.0')] ).
cnf(371,plain,
~ vincent_forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[20,362]),
[iquote('0:Res:20.1,362.0')] ).
cnf(75,axiom,
( ~ accessible_world(u,v)
| ~ abstraction(u,w)
| abstraction(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(370,plain,
~ jules_forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[19,362]),
[iquote('0:Res:19.1,362.0')] ).
cnf(368,plain,
~ forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[22,358]),
[iquote('0:Res:22.1,358.0')] ).
cnf(366,plain,
~ vincent_forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[20,356]),
[iquote('0:Res:20.1,356.0')] ).
cnf(365,plain,
~ jules_forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[19,356]),
[iquote('0:Res:19.1,356.0')] ).
cnf(69,axiom,
( ~ accessible_world(u,v)
| ~ organism(u,w)
| organism(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(363,plain,
~ forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[22,352]),
[iquote('0:Res:22.1,352.0')] ).
cnf(362,plain,
~ forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[22,350]),
[iquote('0:Res:22.1,350.0')] ).
cnf(358,plain,
~ relname(skc8,skc9),
inference(res,[status(thm),theory(equality)],[21,347]),
[iquote('0:Res:21.1,347.0')] ).
cnf(357,plain,
~ proposition(skc8,skc9),
inference(res,[status(thm),theory(equality)],[41,347]),
[iquote('0:Res:41.1,347.0')] ).
cnf(76,axiom,
( ~ accessible_world(u,v)
| ~ relation(u,w)
| relation(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(356,plain,
~ forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[22,346]),
[iquote('0:Res:22.1,346.0')] ).
cnf(352,plain,
~ relname(skc8,skc13),
inference(res,[status(thm),theory(equality)],[21,342]),
[iquote('0:Res:21.1,342.0')] ).
cnf(351,plain,
~ proposition(skc8,skc13),
inference(res,[status(thm),theory(equality)],[41,342]),
[iquote('0:Res:41.1,342.0')] ).
cnf(350,plain,
~ relname(skc12,skc9),
inference(res,[status(thm),theory(equality)],[21,341]),
[iquote('0:Res:21.1,341.0')] ).
cnf(84,axiom,
( ~ accessible_world(u,v)
| ~ thing(u,w)
| thing(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(349,plain,
~ proposition(skc12,skc9),
inference(res,[status(thm),theory(equality)],[41,341]),
[iquote('0:Res:41.1,341.0')] ).
cnf(347,plain,
~ relation(skc8,skc9),
inference(res,[status(thm),theory(equality)],[40,339]),
[iquote('0:Res:40.1,339.0')] ).
cnf(346,plain,
~ relname(skc12,skc13),
inference(res,[status(thm),theory(equality)],[21,338]),
[iquote('0:Res:21.1,338.0')] ).
cnf(345,plain,
~ proposition(skc12,skc13),
inference(res,[status(thm),theory(equality)],[41,338]),
[iquote('0:Res:41.1,338.0')] ).
cnf(60,axiom,
( ~ accessible_world(u,v)
| ~ relname(u,w)
| relname(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(342,plain,
~ relation(skc8,skc13),
inference(res,[status(thm),theory(equality)],[40,335]),
[iquote('0:Res:40.1,335.0')] ).
cnf(341,plain,
~ relation(skc12,skc9),
inference(res,[status(thm),theory(equality)],[40,334]),
[iquote('0:Res:40.1,334.0')] ).
cnf(339,plain,
~ abstraction(skc8,skc9),
inference(res,[status(thm),theory(equality)],[37,333]),
[iquote('0:Res:37.1,333.0')] ).
cnf(338,plain,
~ relation(skc12,skc13),
inference(res,[status(thm),theory(equality)],[40,332]),
[iquote('0:Res:40.1,332.0')] ).
cnf(62,axiom,
( ~ accessible_world(u,v)
| ~ male(u,w)
| male(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(335,plain,
~ abstraction(skc8,skc13),
inference(res,[status(thm),theory(equality)],[37,331]),
[iquote('0:Res:37.1,331.0')] ).
cnf(334,plain,
~ abstraction(skc12,skc9),
inference(res,[status(thm),theory(equality)],[37,328]),
[iquote('0:Res:37.1,328.0')] ).
cnf(333,plain,
~ general(skc8,skc9),
inference(res,[status(thm),theory(equality)],[124,328]),
[iquote('0:Res:124.1,328.0')] ).
cnf(332,plain,
~ abstraction(skc12,skc13),
inference(res,[status(thm),theory(equality)],[37,327]),
[iquote('0:Res:37.1,327.0')] ).
cnf(80,axiom,
( ~ accessible_world(u,v)
| ~ unisex(u,w)
| unisex(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(331,plain,
~ general(skc8,skc13),
inference(res,[status(thm),theory(equality)],[124,327]),
[iquote('0:Res:124.1,327.0')] ).
cnf(328,plain,
~ general(skc12,skc9),
inference(res,[status(thm),theory(equality)],[148,287]),
[iquote('0:Res:148.0,287.0')] ).
cnf(327,plain,
~ general(skc12,skc13),
inference(res,[status(thm),theory(equality)],[185,287]),
[iquote('0:Res:185.0,287.0')] ).
cnf(287,plain,
( ~ eventuality(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[44,237]),
[iquote('0:Res:44.1,237.0')] ).
cnf(82,axiom,
( ~ accessible_world(u,v)
| ~ specific(u,w)
| specific(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(324,plain,
~ man(skc8,skc9),
inference(res,[status(thm),theory(equality)],[33,318]),
[iquote('0:Res:33.1,318.0')] ).
cnf(321,plain,
~ man(skc8,skc13),
inference(res,[status(thm),theory(equality)],[33,314]),
[iquote('0:Res:33.1,314.0')] ).
cnf(319,plain,
~ man(skc12,skc9),
inference(res,[status(thm),theory(equality)],[33,312]),
[iquote('0:Res:33.1,312.0')] ).
cnf(318,plain,
~ human_person(skc8,skc9),
inference(res,[status(thm),theory(equality)],[32,311]),
[iquote('0:Res:32.1,311.0')] ).
cnf(64,axiom,
( ~ accessible_world(u,v)
| ~ human(u,w)
| human(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(315,plain,
~ man(skc12,skc13),
inference(res,[status(thm),theory(equality)],[33,308]),
[iquote('0:Res:33.1,308.0')] ).
cnf(314,plain,
~ human_person(skc8,skc13),
inference(res,[status(thm),theory(equality)],[32,307]),
[iquote('0:Res:32.1,307.0')] ).
cnf(312,plain,
~ human_person(skc12,skc9),
inference(res,[status(thm),theory(equality)],[32,306]),
[iquote('0:Res:32.1,306.0')] ).
cnf(311,plain,
~ organism(skc8,skc9),
inference(res,[status(thm),theory(equality)],[31,304]),
[iquote('0:Res:31.1,304.0')] ).
cnf(67,axiom,
( ~ accessible_world(u,v)
| ~ existent(u,w)
| existent(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(308,plain,
~ human_person(skc12,skc13),
inference(res,[status(thm),theory(equality)],[32,302]),
[iquote('0:Res:32.1,302.0')] ).
cnf(307,plain,
~ organism(skc8,skc13),
inference(res,[status(thm),theory(equality)],[31,300]),
[iquote('0:Res:31.1,300.0')] ).
cnf(306,plain,
~ organism(skc12,skc9),
inference(res,[status(thm),theory(equality)],[31,299]),
[iquote('0:Res:31.1,299.0')] ).
cnf(304,plain,
~ entity(skc8,skc9),
inference(res,[status(thm),theory(equality)],[28,298]),
[iquote('0:Res:28.1,298.0')] ).
cnf(73,axiom,
( ~ accessible_world(u,v)
| ~ general(u,w)
| general(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(302,plain,
~ organism(skc12,skc13),
inference(res,[status(thm),theory(equality)],[31,297]),
[iquote('0:Res:31.1,297.0')] ).
cnf(300,plain,
~ entity(skc8,skc13),
inference(res,[status(thm),theory(equality)],[28,296]),
[iquote('0:Res:28.1,296.0')] ).
cnf(299,plain,
~ entity(skc12,skc9),
inference(res,[status(thm),theory(equality)],[28,292]),
[iquote('0:Res:28.1,292.0')] ).
cnf(298,plain,
~ existent(skc8,skc9),
inference(res,[status(thm),theory(equality)],[118,292]),
[iquote('0:Res:118.1,292.0')] ).
cnf(74,axiom,
( ~ accessible_world(u,v)
| ~ nonhuman(u,w)
| nonhuman(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(297,plain,
~ entity(skc12,skc13),
inference(res,[status(thm),theory(equality)],[28,291]),
[iquote('0:Res:28.1,291.0')] ).
cnf(296,plain,
~ existent(skc8,skc13),
inference(res,[status(thm),theory(equality)],[118,291]),
[iquote('0:Res:118.1,291.0')] ).
cnf(292,plain,
~ existent(skc12,skc9),
inference(res,[status(thm),theory(equality)],[148,286]),
[iquote('0:Res:148.0,286.0')] ).
cnf(291,plain,
~ existent(skc12,skc13),
inference(res,[status(thm),theory(equality)],[185,286]),
[iquote('0:Res:185.0,286.0')] ).
cnf(81,axiom,
( ~ accessible_world(u,v)
| ~ nonexistent(u,w)
| nonexistent(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(286,plain,
( ~ eventuality(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[43,228]),
[iquote('0:Res:43.1,228.0')] ).
cnf(245,plain,
( ~ unisex(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[131,55]),
[iquote('0:Res:131.1,55.1')] ).
cnf(237,plain,
( ~ specific(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[133,54]),
[iquote('0:Res:133.1,54.1')] ).
cnf(228,plain,
( ~ nonexistent(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[132,52]),
[iquote('0:Res:132.1,52.0')] ).
cnf(63,axiom,
( ~ accessible_world(u,v)
| ~ animate(u,w)
| animate(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(281,plain,
~ vincent_forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[20,276]),
[iquote('0:Res:20.1,276.0')] ).
cnf(280,plain,
~ jules_forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[19,276]),
[iquote('0:Res:19.1,276.0')] ).
cnf(279,plain,
~ vincent_forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[20,274]),
[iquote('0:Res:20.1,274.0')] ).
cnf(278,plain,
~ jules_forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[19,274]),
[iquote('0:Res:19.1,274.0')] ).
cnf(65,axiom,
( ~ accessible_world(u,v)
| ~ living(u,w)
| living(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(276,plain,
~ forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[22,271]),
[iquote('0:Res:22.1,271.0')] ).
cnf(274,plain,
~ forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[22,269]),
[iquote('0:Res:22.1,269.0')] ).
cnf(271,plain,
~ relname(skc8,skc15),
inference(res,[status(thm),theory(equality)],[21,265]),
[iquote('0:Res:21.1,265.0')] ).
cnf(270,plain,
~ proposition(skc8,skc15),
inference(res,[status(thm),theory(equality)],[41,265]),
[iquote('0:Res:41.1,265.0')] ).
cnf(66,axiom,
( ~ accessible_world(u,v)
| ~ impartial(u,w)
| impartial(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(269,plain,
~ relname(skc12,skc15),
inference(res,[status(thm),theory(equality)],[21,264]),
[iquote('0:Res:21.1,264.0')] ).
cnf(268,plain,
~ proposition(skc12,skc15),
inference(res,[status(thm),theory(equality)],[41,264]),
[iquote('0:Res:41.1,264.0')] ).
cnf(265,plain,
~ relation(skc8,skc15),
inference(res,[status(thm),theory(equality)],[40,262]),
[iquote('0:Res:40.1,262.0')] ).
cnf(264,plain,
~ relation(skc12,skc15),
inference(res,[status(thm),theory(equality)],[40,261]),
[iquote('0:Res:40.1,261.0')] ).
cnf(83,axiom,
( ~ accessible_world(u,v)
| ~ singleton(u,w)
| singleton(v,w) ),
file('NLP259+1.p',unknown),
[] ).
cnf(262,plain,
~ abstraction(skc8,skc15),
inference(res,[status(thm),theory(equality)],[38,260]),
[iquote('0:Res:38.1,260.0')] ).
cnf(261,plain,
~ abstraction(skc12,skc15),
inference(res,[status(thm),theory(equality)],[38,257]),
[iquote('0:Res:38.1,257.0')] ).
cnf(260,plain,
~ nonhuman(skc8,skc15),
inference(res,[status(thm),theory(equality)],[125,257]),
[iquote('0:Res:125.1,257.0')] ).
cnf(257,plain,
~ nonhuman(skc12,skc15),
inference(res,[status(thm),theory(equality)],[2,225]),
[iquote('0:Res:2.0,225.0')] ).
cnf(57,axiom,
( ~ be(u,v,w,x)
| equal(w,x) ),
file('NLP259+1.p',unknown),
[] ).
cnf(225,plain,
( ~ man(skc8,u)
| ~ nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[33,223]),
[iquote('0:Res:33.1,223.0')] ).
cnf(253,plain,
~ vincent_forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[20,248]),
[iquote('0:Res:20.1,248.0')] ).
cnf(252,plain,
~ jules_forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[19,248]),
[iquote('0:Res:19.1,248.0')] ).
cnf(251,plain,
~ vincent_forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[20,244]),
[iquote('0:Res:20.1,244.0')] ).
cnf(56,axiom,
( ~ man(skc12,u)
| agent(skc12,skf2(u),u) ),
file('NLP259+1.p',unknown),
[] ).
cnf(250,plain,
~ jules_forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[19,244]),
[iquote('0:Res:19.1,244.0')] ).
cnf(248,plain,
~ forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[22,241]),
[iquote('0:Res:22.1,241.0')] ).
cnf(244,plain,
~ forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[22,236]),
[iquote('0:Res:22.1,236.0')] ).
cnf(241,plain,
~ relname(skc8,skc10),
inference(res,[status(thm),theory(equality)],[21,233]),
[iquote('0:Res:21.1,233.0')] ).
cnf(55,axiom,
( ~ male(u,v)
| ~ unisex(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(240,plain,
~ proposition(skc8,skc10),
inference(res,[status(thm),theory(equality)],[41,233]),
[iquote('0:Res:41.1,233.0')] ).
cnf(236,plain,
~ relname(skc12,skc10),
inference(res,[status(thm),theory(equality)],[21,232]),
[iquote('0:Res:21.1,232.0')] ).
cnf(235,plain,
~ proposition(skc12,skc10),
inference(res,[status(thm),theory(equality)],[41,232]),
[iquote('0:Res:41.1,232.0')] ).
cnf(233,plain,
~ relation(skc8,skc10),
inference(res,[status(thm),theory(equality)],[40,230]),
[iquote('0:Res:40.1,230.0')] ).
cnf(54,axiom,
( ~ general(u,v)
| ~ specific(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(232,plain,
~ relation(skc12,skc10),
inference(res,[status(thm),theory(equality)],[40,227]),
[iquote('0:Res:40.1,227.0')] ).
cnf(230,plain,
~ abstraction(skc8,skc10),
inference(res,[status(thm),theory(equality)],[38,226]),
[iquote('0:Res:38.1,226.0')] ).
cnf(227,plain,
~ abstraction(skc12,skc10),
inference(res,[status(thm),theory(equality)],[38,224]),
[iquote('0:Res:38.1,224.0')] ).
cnf(226,plain,
~ nonhuman(skc8,skc10),
inference(res,[status(thm),theory(equality)],[125,224]),
[iquote('0:Res:125.1,224.0')] ).
cnf(52,axiom,
( ~ nonexistent(u,v)
| ~ existent(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(224,plain,
~ nonhuman(skc12,skc10),
inference(res,[status(thm),theory(equality)],[153,223]),
[iquote('0:Res:153.0,223.0')] ).
cnf(223,plain,
( ~ human_person(skc8,u)
| ~ nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[25,221]),
[iquote('0:Res:25.1,221.0')] ).
cnf(221,plain,
( ~ human(skc8,u)
| ~ nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[115,53]),
[iquote('0:Res:115.1,53.0')] ).
cnf(220,plain,
present(skc12,skf2(u)),
inference(mrr,[status(thm)],[219,12]),
[iquote('0:MRR:219.0,12.0')] ).
cnf(53,axiom,
( ~ human(u,v)
| ~ nonhuman(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(213,plain,
( ~ smoke(skc8,u)
| event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[138,48]),
[iquote('0:Res:138.1,48.0')] ).
cnf(217,plain,
event(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[216,48]),
[iquote('0:Res:216.0,48.0')] ).
cnf(216,plain,
smoke(skc12,skf2(u)),
inference(mrr,[status(thm)],[215,12]),
[iquote('0:MRR:215.0,12.0')] ).
cnf(48,axiom,
( ~ smoke(u,v)
| event(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ state(u,v)
| event(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ jules_forename(u,v)
| forename(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ vincent_forename(u,v)
| forename(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ event(u,v)
| eventuality(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ state(u,v)
| eventuality(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ organism(u,v)
| entity(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ man(u,v)
| human_person(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ relation(u,v)
| abstraction(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ proposition(u,v)
| relation(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ eventuality(u,v)
| thing(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ entity(u,v)
| thing(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ human_person(u,v)
| organism(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ abstraction(u,v)
| thing(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ relname(u,v)
| relation(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ man(u,v)
| male(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ forename(u,v)
| relname(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ eventuality(u,v)
| unisex(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ eventuality(u,v)
| specific(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ entity(u,v)
| specific(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ abstraction(u,v)
| unisex(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(176,plain,
( ~ accessible_world(skc8,u)
| present(u,skc13) ),
inference(res,[status(thm),theory(equality)],[6,79]),
[iquote('0:Res:6.0,79.0')] ).
cnf(151,plain,
( ~ accessible_world(skc8,u)
| man(u,skc10) ),
inference(res,[status(thm),theory(equality)],[10,71]),
[iquote('0:Res:10.0,71.0')] ).
cnf(101,plain,
( ~ accessible_world(skc8,u)
| proposition(u,skc12) ),
inference(res,[status(thm),theory(equality)],[13,77]),
[iquote('0:Res:13.0,77.0')] ).
cnf(43,axiom,
( ~ eventuality(u,v)
| nonexistent(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(170,plain,
( ~ accessible_world(skc8,u)
| think_believe_consider(u,skc13) ),
inference(res,[status(thm),theory(equality)],[7,78]),
[iquote('0:Res:7.0,78.0')] ).
cnf(184,plain,
( ~ accessible_world(skc8,u)
| event(u,skc13) ),
inference(res,[status(thm),theory(equality)],[5,86]),
[iquote('0:Res:5.0,86.0')] ).
cnf(162,plain,
( ~ accessible_world(skc8,u)
| jules_forename(u,skc11) ),
inference(res,[status(thm),theory(equality)],[8,58]),
[iquote('0:Res:8.0,58.0')] ).
cnf(146,plain,
( ~ accessible_world(skc8,u)
| state(u,skc9) ),
inference(res,[status(thm),theory(equality)],[11,72]),
[iquote('0:Res:11.0,72.0')] ).
cnf(28,axiom,
( ~ entity(u,v)
| existent(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(189,plain,
( ~ accessible_world(skc8,u)
| vincent_forename(u,skc14) ),
inference(res,[status(thm),theory(equality)],[4,59]),
[iquote('0:Res:4.0,59.0')] ).
cnf(158,plain,
( ~ accessible_world(skc8,u)
| forename(u,skc11) ),
inference(res,[status(thm),theory(equality)],[9,61]),
[iquote('0:Res:9.0,61.0')] ).
cnf(130,plain,
( ~ present(skc8,u)
| present(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,79]),
[iquote('0:Res:12.0,79.1')] ).
cnf(122,plain,
( ~ man(skc8,u)
| man(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,71]),
[iquote('0:Res:12.0,71.1')] ).
cnf(25,axiom,
( ~ human_person(u,v)
| human(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(128,plain,
( ~ proposition(skc8,u)
| proposition(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,77]),
[iquote('0:Res:12.0,77.1')] ).
cnf(129,plain,
( ~ think_believe_consider(skc8,u)
| think_believe_consider(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,78]),
[iquote('0:Res:12.0,78.1')] ).
cnf(137,plain,
( ~ event(skc8,u)
| event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,86]),
[iquote('0:Res:12.0,86.1')] ).
cnf(109,plain,
( ~ jules_forename(skc8,u)
| jules_forename(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,58]),
[iquote('0:Res:12.0,58.1')] ).
cnf(37,axiom,
( ~ abstraction(u,v)
| general(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(138,plain,
( ~ smoke(skc8,u)
| smoke(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,87]),
[iquote('0:Res:12.0,87.1')] ).
cnf(123,plain,
( ~ state(skc8,u)
| state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,72]),
[iquote('0:Res:12.0,72.1')] ).
cnf(110,plain,
( ~ vincent_forename(skc8,u)
| vincent_forename(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,59]),
[iquote('0:Res:12.0,59.1')] ).
cnf(112,plain,
( ~ forename(skc8,u)
| forename(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,61]),
[iquote('0:Res:12.0,61.1')] ).
cnf(38,axiom,
( ~ abstraction(u,v)
| nonhuman(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(136,plain,
( ~ eventuality(skc8,u)
| eventuality(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,85]),
[iquote('0:Res:12.0,85.1')] ).
cnf(119,plain,
( ~ entity(skc8,u)
| entity(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,68]),
[iquote('0:Res:12.0,68.1')] ).
cnf(121,plain,
( ~ human_person(skc8,u)
| human_person(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,70]),
[iquote('0:Res:12.0,70.1')] ).
cnf(126,plain,
( ~ abstraction(skc8,u)
| abstraction(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,75]),
[iquote('0:Res:12.0,75.1')] ).
cnf(24,axiom,
( ~ human_person(u,v)
| animate(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(120,plain,
( ~ organism(skc8,u)
| organism(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,69]),
[iquote('0:Res:12.0,69.1')] ).
cnf(127,plain,
( ~ relation(skc8,u)
| relation(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,76]),
[iquote('0:Res:12.0,76.1')] ).
cnf(135,plain,
( ~ thing(skc8,u)
| thing(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,84]),
[iquote('0:Res:12.0,84.1')] ).
cnf(111,plain,
( ~ relname(skc8,u)
| relname(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,60]),
[iquote('0:Res:12.0,60.1')] ).
cnf(26,axiom,
( ~ organism(u,v)
| living(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(113,plain,
( ~ male(skc8,u)
| male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,62]),
[iquote('0:Res:12.0,62.1')] ).
cnf(131,plain,
( ~ unisex(skc8,u)
| unisex(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,80]),
[iquote('0:Res:12.0,80.1')] ).
cnf(133,plain,
( ~ specific(skc8,u)
| specific(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,82]),
[iquote('0:Res:12.0,82.1')] ).
cnf(115,plain,
( ~ human(skc8,u)
| human(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,64]),
[iquote('0:Res:12.0,64.1')] ).
cnf(27,axiom,
( ~ organism(u,v)
| impartial(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(118,plain,
( ~ existent(skc8,u)
| existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,67]),
[iquote('0:Res:12.0,67.1')] ).
cnf(124,plain,
( ~ general(skc8,u)
| general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,73]),
[iquote('0:Res:12.0,73.1')] ).
cnf(125,plain,
( ~ nonhuman(skc8,u)
| nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,74]),
[iquote('0:Res:12.0,74.1')] ).
cnf(132,plain,
( ~ nonexistent(skc8,u)
| nonexistent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,81]),
[iquote('0:Res:12.0,81.1')] ).
cnf(45,axiom,
( ~ thing(u,v)
| singleton(u,v) ),
file('NLP259+1.p',unknown),
[] ).
cnf(114,plain,
( ~ animate(skc8,u)
| animate(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,63]),
[iquote('0:Res:12.0,63.1')] ).
cnf(116,plain,
( ~ living(skc8,u)
| living(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,65]),
[iquote('0:Res:12.0,65.1')] ).
cnf(117,plain,
( ~ impartial(skc8,u)
| impartial(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,66]),
[iquote('0:Res:12.0,66.1')] ).
cnf(134,plain,
( ~ singleton(skc8,u)
| singleton(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,83]),
[iquote('0:Res:12.0,83.1')] ).
cnf(18,axiom,
be(skc8,skc9,skc10,skc10),
file('NLP259+1.p',unknown),
[] ).
cnf(15,axiom,
agent(skc8,skc13,skc15),
file('NLP259+1.p',unknown),
[] ).
cnf(14,axiom,
of(skc8,skc14,skc15),
file('NLP259+1.p',unknown),
[] ).
cnf(147,plain,
event(skc8,skc9),
inference(res,[status(thm),theory(equality)],[11,34]),
[iquote('0:Res:11.0,34.0')] ).
cnf(148,plain,
eventuality(skc8,skc9),
inference(res,[status(thm),theory(equality)],[11,35]),
[iquote('0:Res:11.0,35.0')] ).
cnf(17,axiom,
of(skc8,skc11,skc10),
file('NLP259+1.p',unknown),
[] ).
cnf(185,plain,
eventuality(skc8,skc13),
inference(res,[status(thm),theory(equality)],[5,47]),
[iquote('0:Res:5.0,47.0')] ).
cnf(153,plain,
human_person(skc8,skc10),
inference(res,[status(thm),theory(equality)],[10,33]),
[iquote('0:Res:10.0,33.0')] ).
cnf(102,plain,
relation(skc8,skc12),
inference(res,[status(thm),theory(equality)],[13,41]),
[iquote('0:Res:13.0,41.0')] ).
cnf(152,plain,
male(skc8,skc10),
inference(res,[status(thm),theory(equality)],[10,23]),
[iquote('0:Res:10.0,23.0')] ).
cnf(16,axiom,
theme(skc8,skc13,skc12),
file('NLP259+1.p',unknown),
[] ).
cnf(159,plain,
relname(skc8,skc11),
inference(res,[status(thm),theory(equality)],[9,22]),
[iquote('0:Res:9.0,22.0')] ).
cnf(6,axiom,
present(skc8,skc13),
file('NLP259+1.p',unknown),
[] ).
cnf(12,axiom,
accessible_world(skc8,skc12),
file('NLP259+1.p',unknown),
[] ).
cnf(2,axiom,
man(skc8,skc15),
file('NLP259+1.p',unknown),
[] ).
cnf(10,axiom,
man(skc8,skc10),
file('NLP259+1.p',unknown),
[] ).
cnf(13,axiom,
proposition(skc8,skc12),
file('NLP259+1.p',unknown),
[] ).
cnf(5,axiom,
event(skc8,skc13),
file('NLP259+1.p',unknown),
[] ).
cnf(7,axiom,
think_believe_consider(skc8,skc13),
file('NLP259+1.p',unknown),
[] ).
cnf(8,axiom,
jules_forename(skc8,skc11),
file('NLP259+1.p',unknown),
[] ).
cnf(11,axiom,
state(skc8,skc9),
file('NLP259+1.p',unknown),
[] ).
cnf(4,axiom,
vincent_forename(skc8,skc14),
file('NLP259+1.p',unknown),
[] ).
cnf(3,axiom,
forename(skc8,skc14),
file('NLP259+1.p',unknown),
[] ).
cnf(9,axiom,
forename(skc8,skc11),
file('NLP259+1.p',unknown),
[] ).
cnf(1,axiom,
actual_world(skc8),
file('NLP259+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NLP259+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n011.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 1 03:47:18 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.25/1.44
% 1.25/1.44 SPASS V 3.9
% 1.25/1.44 SPASS beiseite: Completion found.
% 1.25/1.44 % SZS status CounterSatisfiable
% 1.25/1.44 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.25/1.44 SPASS derived 1265 clauses, backtracked 0 clauses, performed 0 splits and kept 701 clauses.
% 1.25/1.44 SPASS allocated 100637 KBytes.
% 1.25/1.44 SPASS spent 0:00:01.10 on the problem.
% 1.25/1.44 0:00:00.03 for the input.
% 1.25/1.44 0:00:00.16 for the FLOTTER CNF translation.
% 1.25/1.44 0:00:00.06 for inferences.
% 1.25/1.44 0:00:00.00 for the backtracking.
% 1.25/1.44 0:00:00.67 for the reduction.
% 1.25/1.44
% 1.25/1.44
% 1.25/1.44 The saturated set of worked-off clauses is :
% 1.25/1.44 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------