%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP255+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.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:14 EDT 2022
% Result : CounterSatisfiable 1.08s 1.33s
% Output : Saturation 1.16s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 95)
% Comments :
%------------------------------------------------------------------------------
cnf(635,plain,
( ~ actual_world(u)
| ~ man(skc12,skf4(v))
| ~ accessible_world(skc12,v)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ accessible_world(u,z)
| ~ proposition(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ state(u,x2)
| ~ vincent_forename(u,x3)
| ~ man(u,x4)
| ~ smoke(z,x5)
| ~ present(z,x5)
| ~ jules_forename(u,x6)
| ~ smoke(v,skf2(skf4(v)))
| ~ present(v,skf2(skf4(v)))
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ theme(u,x1,z)
| ~ of(u,x3,x4)
| ~ agent(u,x1,x4)
| ~ agent(z,x5,x4)
| ~ of(u,x6,x4)
| ~ be(u,x2,x4,x4) ),
inference(res,[status(thm),theory(equality)],[511,97]),
[iquote('0:Res:511.2,97.29')] ).
cnf(1082,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(v,w,x4)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,v)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ be(skc8,x2,x4,x4) ),
inference(res,[status(thm),theory(equality)],[511,98]),
[iquote('0:Res:511.2,98.21')] ).
cnf(1063,plain,
( ~ actual_world(u)
| ~ man(skc12,skf4(v))
| ~ accessible_world(skc12,v)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,x1)
| ~ vincent_forename(u,x2)
| ~ man(u,x3)
| ~ jules_forename(u,x4)
| ~ smoke(v,skf2(skf4(v)))
| ~ present(v,skf2(skf4(v)))
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ of(u,x2,x3)
| ~ agent(u,z,x3)
| ~ of(u,x4,x3)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,x3)
| ~ be(u,x1,x3,x3) ),
inference(res,[status(thm),theory(equality)],[511,180]),
[iquote('0:Res:511.2,180.27')] ).
cnf(867,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ accessible_world(u,z)
| ~ proposition(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ state(u,skc9)
| ~ vincent_forename(u,x2)
| ~ man(u,skc10)
| ~ smoke(z,x3)
| ~ present(z,x3)
| ~ jules_forename(u,x4)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ theme(u,x1,z)
| ~ of(u,x2,skc10)
| ~ agent(u,x1,skc10)
| ~ agent(z,x3,skc10)
| ~ of(u,x4,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[856,96]),
[iquote('0:Res:856.1,96.27')] ).
cnf(1035,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ agent(v,w,x4)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,v)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,skc11,x4)
| ~ be(skc8,x2,x4,x4) ),
inference(res,[status(thm),theory(equality)],[511,207]),
[iquote('0:Res:511.2,207.20')] ).
cnf(1400,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc15)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ vincent_forename(skc12,u)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ event(skc12,w)
| ~ present(skc12,w)
| ~ think_believe_consider(skc12,w)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,skc10)
| ~ smoke(v,y)
| ~ present(v,y)
| ~ jules_forename(skc12,z)
| ~ theme(skc12,w,v)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ agent(v,y,skc10)
| ~ of(skc12,z,skc10) ),
inference(obv,[status(thm),theory(equality)],[1398]),
[iquote('0:Obv:1398.2')] ).
cnf(1415,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ smoke(skc12,v)
| ~ present(skc12,v)
| ~ jules_forename(u,w)
| ~ agent(u,skc13,skc10)
| ~ agent(skc12,v,skc10)
| ~ of(u,w,skc10) ),
inference(obv,[status(thm),theory(equality)],[1412]),
[iquote('0:Obv:1412.1')] ).
cnf(1409,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ state(u,skc9)
| ~ vincent_forename(u,v)
| ~ man(u,skc10)
| ~ smoke(skc12,w)
| ~ present(skc12,w)
| ~ jules_forename(u,x)
| ~ of(u,v,skc10)
| ~ agent(u,skc13,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(u,x,skc10) ),
inference(obv,[status(thm),theory(equality)],[1404]),
[iquote('0:Obv:1404.7')] ).
cnf(1399,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ state(u,skc9)
| ~ vincent_forename(u,x)
| ~ man(u,skc10)
| ~ smoke(v,y)
| ~ present(v,y)
| ~ jules_forename(u,z)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ agent(v,y,skc10)
| ~ of(u,z,skc10) ),
inference(obv,[status(thm),theory(equality)],[1396]),
[iquote('0:Obv:1396.1')] ).
cnf(1010,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(v,w,x3)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,y)
| ~ theme(skc8,z,v)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,x4,x3)
| ~ of(skc8,skc14,y)
| ~ be(skc8,x1,x3,x3) ),
inference(res,[status(thm),theory(equality)],[511,203]),
[iquote('0:Res:511.2,203.20')] ).
cnf(1384,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,v)
| ~ man(u,skc15)
| ~ accessible_world(u,w)
| ~ proposition(u,w)
| ~ event(u,x)
| ~ present(u,x)
| ~ think_believe_consider(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ smoke(w,z)
| ~ present(w,z)
| ~ jules_forename(u,x1)
| ~ of(u,v,skc15)
| ~ theme(u,x,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ agent(w,z,skc10)
| ~ of(u,x1,skc10) ),
inference(obv,[status(thm),theory(equality)],[1379]),
[iquote('0:Obv:1379.1')] ).
cnf(1389,plain,
( ~ accessible_world(skc12,skc8)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ smoke(u,x)
| ~ present(u,x)
| ~ jules_forename(skc8,y)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,skc10)
| ~ agent(skc8,v,skc10)
| ~ agent(u,x,skc10)
| ~ of(skc8,y,skc10) ),
inference(mrr,[status(thm)],[1386,4]),
[iquote('0:MRR:1386.1,4.0')] ).
cnf(1374,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ accessible_world(u,x)
| ~ proposition(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ state(u,skc9)
| ~ vincent_forename(u,z)
| ~ man(u,skc10)
| ~ smoke(x,x1)
| ~ present(x,x1)
| ~ jules_forename(u,x2)
| ~ agent(u,skc13,w)
| ~ of(u,v,w)
| ~ theme(u,y,x)
| ~ of(u,z,skc10)
| ~ agent(u,y,skc10)
| ~ agent(x,x1,skc10)
| ~ of(u,x2,skc10) ),
inference(obv,[status(thm),theory(equality)],[1371]),
[iquote('0:Obv:1371.1')] ).
cnf(994,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(v,w,x3)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,v)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ of(skc8,skc14,x3)
| ~ be(skc8,x2,x3,x3) ),
inference(res,[status(thm),theory(equality)],[511,204]),
[iquote('0:Res:511.2,204.20')] ).
cnf(871,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,skc9)
| ~ vincent_forename(u,x1)
| ~ man(u,skc10)
| ~ smoke(y,x2)
| ~ present(y,x2)
| ~ jules_forename(u,x3)
| ~ theme(u,v,skc12)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ theme(u,z,y)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ agent(y,x2,skc10)
| ~ of(u,x3,skc10) ),
inference(res,[status(thm),theory(equality)],[856,578]),
[iquote('0:Res:856.1,578.27')] ).
cnf(868,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,skc9)
| ~ vincent_forename(u,x1)
| ~ man(u,skc10)
| ~ jules_forename(u,x2)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[856,174]),
[iquote('0:Res:856.1,174.26')] ).
cnf(1256,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,y)
| ~ event(skc12,z)
| ~ present(skc12,z)
| ~ think_believe_consider(skc12,z)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x1)
| ~ man(skc12,v)
| ~ jules_forename(skc12,x2)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(skc12,w,skc12)
| ~ agent(skc12,w,y)
| ~ of(skc12,x,y)
| ~ of(skc12,x1,v)
| ~ agent(skc12,z,v)
| ~ of(skc12,x2,v)
| ~ theme(skc12,z,skc8)
| ~ agent(skc8,skc13,v) ),
inference(res,[status(thm),theory(equality)],[142,1065]),
[iquote('0:Res:142.1,1065.26')] ).
cnf(1359,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ event(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(u,skf2(skc10))
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ 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)],[1358,71]),
[iquote('0:MRR:1358.1,71.2')] ).
cnf(983,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(v,w,x3)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,v)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ be(skc8,skc9,x3,x3) ),
inference(res,[status(thm),theory(equality)],[511,210]),
[iquote('0:Res:511.2,210.20')] ).
cnf(1351,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,w)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,v,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,v,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(obv,[status(thm),theory(equality)],[1348]),
[iquote('0:Obv:1348.1')] ).
cnf(1345,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,w)
| ~ man(u,skc10)
| ~ jules_forename(u,x)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10)
| ~ theme(u,v,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(obv,[status(thm),theory(equality)],[1342]),
[iquote('0:Obv:1342.1')] ).
cnf(1335,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,v)
| ~ man(u,skc15)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ state(u,skc9)
| ~ vincent_forename(u,x)
| ~ man(u,skc10)
| ~ jules_forename(u,y)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc15)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10)
| ~ theme(u,w,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(obv,[status(thm),theory(equality)],[1332]),
[iquote('0:Obv:1332.1')] ).
cnf(1338,plain,
( ~ actual_world(skc12)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,w)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,skc10)
| ~ agent(skc12,u,skc10)
| ~ of(skc12,w,skc10)
| ~ theme(skc12,u,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1337,213]),
[iquote('0:MRR:1337.5,213.1')] ).
cnf(964,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(v,w,x3)
| ~ theme(skc8,x,u)
| ~ theme(skc8,z,v)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,x4,x3)
| ~ agent(skc8,x,skc10)
| ~ of(skc8,y,skc10)
| ~ be(skc8,x1,x3,x3) ),
inference(res,[status(thm),theory(equality)],[511,208]),
[iquote('0:Res:511.2,208.20')] ).
cnf(1329,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ event(u,x)
| ~ present(u,x)
| ~ think_believe_consider(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ jules_forename(u,z)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,skc13,w)
| ~ of(u,v,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10)
| ~ theme(u,x,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(obv,[status(thm),theory(equality)],[1325]),
[iquote('0:Obv:1325.1')] ).
cnf(1254,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ state(u,skc9)
| ~ vincent_forename(u,z)
| ~ man(u,skc10)
| ~ jules_forename(u,x1)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ of(u,z,skc10)
| ~ agent(u,y,skc10)
| ~ of(u,x1,skc10)
| ~ theme(u,y,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(res,[status(thm),theory(equality)],[856,1065]),
[iquote('0:Res:856.1,1065.26')] ).
cnf(1238,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)
| ~ vincent_forename(skc12,w)
| ~ man(skc12,x)
| ~ accessible_world(skc12,y)
| ~ proposition(skc12,y)
| ~ event(skc12,z)
| ~ present(skc12,z)
| ~ think_believe_consider(skc12,z)
| ~ vincent_forename(skc12,x1)
| ~ smoke(y,x2)
| ~ present(y,x2)
| ~ jules_forename(skc12,x3)
| ~ agent(skc12,u,x)
| ~ of(skc12,w,x)
| ~ theme(skc12,z,y)
| ~ of(skc12,x1,skc10)
| ~ agent(skc12,z,skc10)
| ~ agent(y,x2,skc10)
| ~ of(skc12,x3,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1236,12]),
[iquote('0:MRR:1236.2,12.0')] ).
cnf(1094,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ theme(skc8,w,v)
| ~ agent(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10)
| ~ of(skc8,skc14,x)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[511,809]),
[iquote('0:Res:511.2,809.15')] ).
cnf(947,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(v,w,skc10)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,v)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x4,skc10)
| ~ be(skc8,x2,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[511,209]),
[iquote('0:Res:511.2,209.20')] ).
cnf(1089,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ theme(skc8,w,v)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x1,skc10)
| ~ of(skc8,skc14,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[511,793]),
[iquote('0:Res:511.2,793.15')] ).
cnf(1224,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)
| ~ vincent_forename(skc12,w)
| ~ man(skc12,x)
| ~ event(skc12,y)
| ~ present(skc12,y)
| ~ think_believe_consider(skc12,y)
| ~ vincent_forename(skc12,z)
| ~ jules_forename(skc12,x1)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc12,u,x)
| ~ of(skc12,w,x)
| ~ of(skc12,z,skc10)
| ~ agent(skc12,y,skc10)
| ~ of(skc12,x1,skc10)
| ~ theme(skc12,y,skc8)
| ~ agent(skc8,skc13,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1220,12]),
[iquote('0:MRR:1220.2,12.0')] ).
cnf(1282,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,w)
| ~ event(skc12,x)
| ~ present(skc12,x)
| ~ think_believe_consider(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ jules_forename(skc12,z)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc12,u,w)
| ~ of(skc12,v,w)
| ~ of(skc12,y,skc10)
| ~ agent(skc12,x,skc10)
| ~ of(skc12,z,skc10)
| ~ theme(skc12,x,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1278,12]),
[iquote('0:MRR:1278.2,12.0')] ).
cnf(1289,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,u)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,u)
| ~ event(skc12,w)
| ~ present(skc12,w)
| ~ think_believe_consider(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ jules_forename(skc12,y)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,u)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10)
| ~ theme(skc12,w,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1286,12]),
[iquote('0:MRR:1286.2,12.0')] ).
cnf(923,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ state(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ smoke(skc12,x3)
| ~ present(skc12,x3)
| ~ jules_forename(skc8,x4)
| ~ theme(skc8,v,u)
| ~ agent(skc8,v,x)
| ~ of(skc8,w,x)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,y,x2)
| ~ agent(skc12,x3,x2)
| ~ of(skc8,x4,x2)
| ~ theme(skc8,y,skc12)
| ~ be(skc8,z,x2,x2) ),
inference(res,[status(thm),theory(equality)],[511,212]),
[iquote('0:Res:511.2,212.18')] ).
cnf(1313,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,skf2(skc10),skc8)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,u,skc10)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1312,151,12,217,220]),
[iquote('0:MRR:1312.2,1312.3,1312.6,1312.7,151.1,12.0,217.0,220.0')] ).
cnf(1305,plain,
( ~ actual_world(u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ event(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(u,skf2(skc10))
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ 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,1302]),
[iquote('0:Res:511.2,1302.12')] ).
cnf(1303,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ event(skc12,v)
| ~ present(skc12,v)
| ~ think_believe_consider(skc12,v)
| ~ vincent_forename(skc12,u)
| ~ jules_forename(skc12,w)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc12,v,skc10)
| ~ of(skc12,w,skc10)
| ~ theme(skc12,v,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1300,12]),
[iquote('0:MRR:1300.2,12.0')] ).
cnf(1307,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,v)
| ~ 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)],[1306,12]),
[iquote('0:MRR:1306.2,12.0')] ).
cnf(830,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)))
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(v,w,x3)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ of(skc8,x2,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,skc13,v)
| ~ agent(skc8,skc13,x3)
| ~ be(skc8,x1,x3,x3) ),
inference(res,[status(thm),theory(equality)],[511,206]),
[iquote('0:Res:511.2,206.18')] ).
cnf(1308,plain,
( ~ actual_world(skc12)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ 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)],[1304,151,12,217,220]),
[iquote('0:MRR:1304.1,1304.2,1304.5,1304.6,151.1,12.0,217.0,220.0')] ).
cnf(1302,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,w)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,v,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,v,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(obv,[status(thm),theory(equality)],[1299]),
[iquote('0:Obv:1299.1')] ).
cnf(1296,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ jules_forename(u,x)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10)
| ~ theme(u,v,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1295,187]),
[iquote('0:MRR:1295.3,187.1')] ).
cnf(622,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ proposition(skc12,w)
| ~ accessible_world(skc12,w)
| ~ think_believe_consider(skc12,x)
| ~ present(skc12,x)
| ~ event(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ man(skc12,z)
| ~ accessible_world(skc12,x1)
| ~ proposition(skc12,x1)
| ~ event(skc12,x2)
| ~ present(skc12,x2)
| ~ think_believe_consider(skc12,x2)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x3)
| ~ man(skc12,v)
| ~ smoke(x1,x4)
| ~ present(x1,x4)
| ~ jules_forename(skc12,x5)
| ~ theme(skc12,x,w)
| ~ agent(skc12,x,z)
| ~ of(skc12,y,z)
| ~ theme(skc12,x2,x1)
| ~ of(skc12,x3,v)
| ~ agent(skc12,x2,v)
| ~ agent(x1,x4,v)
| ~ of(skc12,x5,v)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[142,96]),
[iquote('0:Res:142.1,96.27')] ).
cnf(1281,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ event(u,x)
| ~ present(u,x)
| ~ think_believe_consider(u,x)
| ~ vincent_forename(u,y)
| ~ jules_forename(u,z)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,skc13,w)
| ~ of(u,v,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10)
| ~ theme(u,x,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1280,167,173,181]),
[iquote('0:MRR:1280.3,1280.4,1280.5,167.1,173.1,181.1')] ).
cnf(1257,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ vincent_forename(u,z)
| ~ jules_forename(u,x1)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ of(u,z,skc10)
| ~ agent(u,y,skc10)
| ~ of(u,x1,skc10)
| ~ theme(u,y,skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1255,101,146,151]),
[iquote('0:MRR:1255.2,1255.12,1255.14,101.1,146.1,151.1')] ).
cnf(1174,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,w)
| ~ accessible_world(skc12,x)
| ~ proposition(skc12,x)
| ~ event(skc12,y)
| ~ present(skc12,y)
| ~ think_believe_consider(skc12,y)
| ~ vincent_forename(skc12,z)
| ~ smoke(x,x1)
| ~ present(x,x1)
| ~ jules_forename(skc12,x2)
| ~ agent(skc12,u,w)
| ~ of(skc12,v,w)
| ~ theme(skc12,y,x)
| ~ of(skc12,z,skc10)
| ~ agent(skc12,y,skc10)
| ~ agent(x,x1,skc10)
| ~ of(skc12,x2,skc10) ),
inference(mrr,[status(thm)],[1171,12]),
[iquote('0:MRR:1171.2,12.0')] ).
cnf(1152,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ theme(skc8,v,skc12)
| ~ agent(skc8,v,x)
| ~ of(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10) ),
inference(res,[status(thm),theory(equality)],[511,1150]),
[iquote('0:Res:511.2,1150.13')] ).
cnf(873,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,y)
| ~ accessible_world(skc12,z)
| ~ proposition(skc12,z)
| ~ event(skc12,x1)
| ~ present(skc12,x1)
| ~ think_believe_consider(skc12,x1)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x2)
| ~ man(skc12,v)
| ~ smoke(z,x3)
| ~ present(z,x3)
| ~ jules_forename(skc12,x4)
| ~ theme(skc12,w,skc12)
| ~ agent(skc12,w,y)
| ~ of(skc12,x,y)
| ~ theme(skc12,x1,z)
| ~ of(skc12,x2,v)
| ~ agent(skc12,x1,v)
| ~ agent(z,x3,v)
| ~ of(skc12,x4,v) ),
inference(res,[status(thm),theory(equality)],[142,578]),
[iquote('0:Res:142.1,578.27')] ).
cnf(852,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ proposition(skc12,w)
| ~ accessible_world(skc12,w)
| ~ think_believe_consider(skc12,x)
| ~ present(skc12,x)
| ~ event(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ man(skc12,z)
| ~ event(skc12,x1)
| ~ present(skc12,x1)
| ~ think_believe_consider(skc12,x1)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x2)
| ~ man(skc12,v)
| ~ jules_forename(skc12,x3)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(skc12,x,w)
| ~ agent(skc12,x,z)
| ~ of(skc12,y,z)
| ~ of(skc12,x2,v)
| ~ agent(skc12,x1,v)
| ~ of(skc12,x3,v)
| ~ theme(skc12,x1,skc8)
| ~ agent(skc8,skc13,v)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[142,174]),
[iquote('0:Res:142.1,174.26')] ).
cnf(1065,plain,
( ~ actual_world(u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ state(u,z)
| ~ vincent_forename(u,x1)
| ~ man(u,x2)
| ~ jules_forename(u,x3)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ of(u,x1,x2)
| ~ agent(u,y,x2)
| ~ of(u,x3,x2)
| ~ theme(u,y,skc8)
| ~ agent(skc8,skc13,x2)
| ~ be(u,z,x2,x2) ),
inference(mrr,[status(thm)],[1062,174,216,220]),
[iquote('0:MRR:1062.1,1062.16,1062.17,174.27,216.0,220.0')] ).
cnf(1189,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,u)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,u)
| ~ accessible_world(skc12,w)
| ~ proposition(skc12,w)
| ~ event(skc12,x)
| ~ present(skc12,x)
| ~ think_believe_consider(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ smoke(w,z)
| ~ present(w,z)
| ~ jules_forename(skc12,x1)
| ~ of(skc12,v,u)
| ~ theme(skc12,x,w)
| ~ of(skc12,y,skc10)
| ~ agent(skc12,x,skc10)
| ~ agent(w,z,skc10)
| ~ of(skc12,x1,skc10) ),
inference(mrr,[status(thm)],[1185,12]),
[iquote('0:MRR:1185.2,12.0')] ).
cnf(1216,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,v)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ vincent_forename(skc12,w)
| ~ smoke(v,x)
| ~ present(v,x)
| ~ jules_forename(skc12,y)
| ~ of(skc12,w,skc10)
| ~ agent(skc12,u,skc10)
| ~ agent(v,x,skc10)
| ~ of(skc12,y,skc10) ),
inference(mrr,[status(thm)],[1211,12]),
[iquote('0:MRR:1211.2,12.0')] ).
cnf(589,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)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ accessible_world(u,z)
| ~ proposition(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ vincent_forename(u,x2)
| ~ smoke(z,x3)
| ~ present(z,x3)
| ~ jules_forename(u,x4)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ theme(u,x1,z)
| ~ of(u,x2,skc10)
| ~ agent(u,x1,skc10)
| ~ agent(z,x3,skc10)
| ~ of(u,x4,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[588,146,151]),
[iquote('0:MRR:588.14,588.16,146.1,151.1')] ).
cnf(1230,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ smoke(skc12,v)
| ~ present(skc12,v)
| ~ jules_forename(skc12,w)
| ~ agent(skc12,skc13,skc10)
| ~ agent(skc12,v,skc10)
| ~ of(skc12,w,skc10) ),
inference(mrr,[status(thm)],[1228,12]),
[iquote('0:MRR:1228.2,12.0')] ).
cnf(1232,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,skc11)
| ~ smoke(skc12,u)
| ~ present(skc12,u)
| ~ jules_forename(skc12,v)
| ~ agent(skc12,u,skc10)
| ~ of(skc12,v,skc10) ),
inference(mrr,[status(thm)],[1231,12]),
[iquote('0:MRR:1231.2,12.0')] ).
cnf(1229,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,skc11)
| ~ smoke(skc12,v)
| ~ present(skc12,v)
| ~ jules_forename(u,w)
| ~ agent(u,skc13,skc10)
| ~ agent(skc12,v,skc10)
| ~ of(u,w,skc10) ),
inference(obv,[status(thm),theory(equality)],[1227]),
[iquote('0:Obv:1227.1')] ).
cnf(1214,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ smoke(skc12,w)
| ~ present(skc12,w)
| ~ jules_forename(u,x)
| ~ of(u,v,skc10)
| ~ agent(u,skc13,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(u,x,skc10) ),
inference(mrr,[status(thm)],[1213,101,181,173,167]),
[iquote('0:MRR:1213.4,1213.5,1213.6,1213.7,101.1,181.1,173.1,167.1')] ).
cnf(855,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)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ vincent_forename(u,x1)
| ~ jules_forename(u,x2)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[851,146,151]),
[iquote('0:MRR:851.12,851.14,146.1,151.1')] ).
cnf(1207,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ smoke(v,y)
| ~ present(v,y)
| ~ jules_forename(u,z)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ agent(v,y,skc10)
| ~ of(u,z,skc10) ),
inference(mrr,[status(thm)],[1206,187]),
[iquote('0:MRR:1206.3,187.1')] ).
cnf(1196,plain,
( ~ accessible_world(skc8,skc8)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ smoke(u,x)
| ~ present(u,x)
| ~ jules_forename(skc8,y)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,skc10)
| ~ agent(skc8,v,skc10)
| ~ agent(u,x,skc10)
| ~ of(skc8,y,skc10) ),
inference(mrr,[status(thm)],[1193,187]),
[iquote('0:MRR:1193.1,187.1')] ).
cnf(908,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x3)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,w,skc12)
| ~ be(skc8,x1,x3,x3) ),
inference(mrr,[status(thm)],[905,201,216,220]),
[iquote('0:MRR:905.0,905.17,905.18,201.25,216.0,220.0')] ).
cnf(1173,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ accessible_world(u,x)
| ~ proposition(u,x)
| ~ event(u,y)
| ~ present(u,y)
| ~ think_believe_consider(u,y)
| ~ vincent_forename(u,z)
| ~ smoke(x,x1)
| ~ present(x,x1)
| ~ jules_forename(u,x2)
| ~ agent(u,skc13,w)
| ~ of(u,v,w)
| ~ theme(u,y,x)
| ~ of(u,z,skc10)
| ~ agent(u,y,skc10)
| ~ agent(x,x1,skc10)
| ~ of(u,x2,skc10) ),
inference(mrr,[status(thm)],[1172,167,173,181]),
[iquote('0:MRR:1172.3,1172.4,1172.5,167.1,173.1,181.1')] ).
cnf(1179,plain,
( ~ vincent_forename(skc8,skc11)
| ~ agent(skc8,skc13,skc10) ),
inference(res,[status(thm),theory(equality)],[17,1178]),
[iquote('0:Res:17.0,1178.1')] ).
cnf(1178,plain,
( ~ vincent_forename(skc8,u)
| ~ of(skc8,u,skc10)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1175,5,6,7]),
[iquote('0:MRR:1175.0,1175.1,1175.2,5.0,6.0,7.0')] ).
cnf(1167,plain,
( ~ event(skc8,u)
| ~ present(skc8,u)
| ~ think_believe_consider(skc8,u)
| ~ vincent_forename(skc8,v)
| ~ theme(skc8,u,skc12)
| ~ of(skc8,v,skc10)
| ~ agent(skc8,u,skc10) ),
inference(mrr,[status(thm)],[1164,4]),
[iquote('0:MRR:1164.0,4.0')] ).
cnf(876,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ vincent_forename(u,x1)
| ~ smoke(y,x2)
| ~ present(y,x2)
| ~ jules_forename(u,x3)
| ~ theme(u,v,skc12)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ theme(u,z,y)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ agent(y,x2,skc10)
| ~ of(u,x3,skc10) ),
inference(mrr,[status(thm)],[872,101,146,151]),
[iquote('0:MRR:872.2,872.14,872.16,101.1,146.1,151.1')] ).
cnf(1150,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ agent(u,v,skc10)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10) ),
inference(mrr,[status(thm)],[1147,11,10,17]),
[iquote('0:MRR:1147.12,1147.14,1147.22,11.0,10.0,17.0')] ).
cnf(1038,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ agent(u,v,x3)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,skc11,x3)
| ~ be(skc8,x1,x3,x3) ),
inference(mrr,[status(thm)],[1034,197,216,220,13,12]),
[iquote('0:MRR:1034.0,1034.3,1034.4,1034.5,1034.6,197.26,216.0,220.0,13.0,12.0')] ).
cnf(1141,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ man(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ jules_forename(skc8,z)
| ~ theme(skc8,v,skc12)
| ~ agent(skc8,v,w)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,skc10)
| ~ agent(skc8,x,skc10)
| ~ of(skc8,z,skc10)
| ~ of(skc8,skc14,w) ),
inference(res,[status(thm),theory(equality)],[511,1136]),
[iquote('0:Res:511.2,1136.13')] ).
cnf(1121,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ jules_forename(skc8,z)
| ~ theme(skc8,v,skc12)
| ~ agent(skc8,v,x)
| ~ of(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,z,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(res,[status(thm),theory(equality)],[511,1119]),
[iquote('0:Res:511.2,1119.13')] ).
cnf(1136,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(u,v,skc10)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10)
| ~ of(skc8,skc14,x) ),
inference(mrr,[status(thm)],[1133,11,10]),
[iquote('0:MRR:1133.11,1133.13,11.0,10.0')] ).
cnf(1132,plain,
( ~ vincent_forename(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ jules_forename(skc8,w)
| ~ of(skc8,u,skc15)
| ~ theme(skc8,v,skc12)
| ~ agent(skc8,v,skc10)
| ~ of(skc8,w,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1129,2]),
[iquote('0:MRR:1129.1,2.0')] ).
cnf(1013,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ state(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,x2)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,y,x2)
| ~ of(skc8,x3,x2)
| ~ of(skc8,skc14,x)
| ~ be(skc8,z,x2,x2) ),
inference(mrr,[status(thm)],[1009,193,216,220,13,12]),
[iquote('0:MRR:1009.0,1009.3,1009.4,1009.5,1009.6,193.26,216.0,220.0,13.0,12.0')] ).
cnf(1128,plain,
( ~ vincent_forename(skc8,u)
| ~ man(skc8,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ jules_forename(skc8,x)
| ~ agent(skc8,skc13,v)
| ~ of(skc8,u,v)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,skc10)
| ~ of(skc8,x,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1125,7,6,5]),
[iquote('0:MRR:1125.0,1125.1,1125.2,7.0,6.0,5.0')] ).
cnf(1124,plain,
( ~ think_believe_consider(skc8,u)
| ~ present(skc8,u)
| ~ event(skc8,u)
| ~ vincent_forename(skc8,v)
| ~ man(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ jules_forename(skc8,y)
| ~ theme(skc8,u,skc12)
| ~ agent(skc8,u,w)
| ~ of(skc8,v,w)
| ~ theme(skc8,x,skc12)
| ~ agent(skc8,x,skc10)
| ~ of(skc8,y,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1120,151,216,220,12,13]),
[iquote('0:MRR:1120.0,1120.1,1120.2,1120.8,1120.9,151.1,216.0,220.0,12.0,13.0')] ).
cnf(1119,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(u,v,skc10)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x1,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1116,11,10]),
[iquote('0:MRR:1116.12,1116.13,11.0,10.0')] ).
cnf(997,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ man(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,x2)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ agent(skc8,z,x2)
| ~ of(skc8,x3,x2)
| ~ of(skc8,skc14,x2)
| ~ be(skc8,x1,x2,x2) ),
inference(mrr,[status(thm)],[993,194,216,220,13,12]),
[iquote('0:MRR:993.0,993.3,993.4,993.5,993.6,194.26,216.0,220.0,13.0,12.0')] ).
cnf(986,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,x2)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,z,x2)
| ~ of(skc8,x3,x2)
| ~ be(skc8,skc9,x2,x2) ),
inference(mrr,[status(thm)],[982,200,216,220,13,12]),
[iquote('0:MRR:982.0,982.3,982.4,982.5,982.6,200.26,216.0,220.0,13.0,12.0')] ).
cnf(1092,plain,
( ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ jules_forename(skc8,z)
| ~ theme(skc8,v,u)
| ~ agent(skc8,v,x)
| ~ of(skc8,w,x)
| ~ theme(skc8,y,skc12)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,z,skc10)
| ~ of(skc8,skc14,skc10)
| man(u,skf4(u)) ),
inference(mrr,[status(thm)],[1088,151,216,220,12,13]),
[iquote('0:MRR:1088.0,1088.1,1088.2,1088.10,1088.11,151.1,216.0,220.0,12.0,13.0')] ).
cnf(809,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ agent(u,v,skc10)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc14,y)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[807,11,10]),
[iquote('0:MRR:807.13,807.15,11.0,10.0')] ).
cnf(793,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ agent(u,v,skc10)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc14,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[791,11,10]),
[iquote('0:MRR:791.14,791.15,11.0,10.0')] ).
cnf(1054,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ theme(skc8,w,v)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[511,820]),
[iquote('0:Res:511.2,820.15')] ).
cnf(1045,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ jules_forename(skc8,z)
| ~ theme(skc8,w,v)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,skc10)
| ~ agent(skc8,x,skc10)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,w,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[511,766]),
[iquote('0:Res:511.2,766.14')] ).
cnf(98,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x5)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,x1)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[1,97]),
[iquote('0:Res:1.0,97.0')] ).
cnf(180,plain,
( ~ actual_world(u)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,x1)
| ~ vincent_forename(u,x2)
| ~ man(u,x3)
| ~ jules_forename(u,x4)
| ~ smoke(v,x5)
| ~ present(v,x5)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ of(u,x2,x3)
| ~ agent(u,z,x3)
| ~ of(u,x4,x3)
| ~ theme(u,z,skc8)
| ~ agent(v,x5,skf4(v))
| ~ agent(skc8,skc13,x3)
| ~ be(u,x1,x3,x3) ),
inference(res,[status(thm),theory(equality)],[6,97]),
[iquote('0:Res:6.0,97.7')] ).
cnf(820,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ agent(u,v,skc10)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[818,11,10,17]),
[iquote('0:MRR:818.14,818.16,818.24,11.0,10.0,17.0')] ).
cnf(833,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ state(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,x2)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ of(skc8,x1,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,x2)
| ~ be(skc8,z,x2,x2) ),
inference(mrr,[status(thm)],[829,196,216,220,13,12]),
[iquote('0:MRR:829.0,829.3,829.4,829.5,829.6,196.24,216.0,220.0,13.0,12.0')] ).
cnf(179,plain,
( ~ actual_world(u)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,x1)
| ~ vincent_forename(u,x2)
| ~ man(u,x3)
| ~ smoke(y,x4)
| ~ present(y,x4)
| ~ jules_forename(u,x5)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ theme(u,z,y)
| ~ of(u,x2,x3)
| ~ agent(u,z,x3)
| ~ agent(y,x4,x3)
| ~ of(u,x5,x3)
| ~ theme(u,v,skc8)
| ~ agent(skc8,skc13,skf4(skc8))
| ~ be(u,x1,x3,x3) ),
inference(res,[status(thm),theory(equality)],[6,97]),
[iquote('0:Res:6.0,97.2')] ).
cnf(766,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(u,v,skc10)
| ~ theme(skc8,x,w)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,x,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[765,11,10]),
[iquote('0:MRR:765.12,765.14,11.0,10.0')] ).
cnf(1019,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ vincent_forename(skc8,v)
| ~ man(skc8,w)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ jules_forename(skc8,z)
| ~ of(skc8,v,w)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,skc10)
| ~ agent(skc8,x,skc10)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,skc13,w) ),
inference(res,[status(thm),theory(equality)],[511,1017]),
[iquote('0:Res:511.2,1017.11')] ).
cnf(207,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ agent(u,v,x5)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,x1)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,skc11,x5)
| ~ be(skc8,x3,x5,x5) ),
inference(mrr,[status(thm)],[165,1]),
[iquote('0:MRR:165.0,1.0')] ).
cnf(1017,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(u,v,skc10)
| ~ of(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,skc13,x) ),
inference(mrr,[status(thm)],[1014,11,10]),
[iquote('0:MRR:1014.9,1014.11,11.0,10.0')] ).
cnf(848,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ state(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,x2)
| ~ of(skc8,w,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,y,x2)
| ~ of(skc8,x3,x2)
| ~ agent(skc8,skc13,x)
| ~ be(skc8,z,x2,x2) ),
inference(mrr,[status(thm)],[844,195,216,220,13,12,16]),
[iquote('0:MRR:844.0,844.3,844.4,844.5,844.6,844.24,195.24,216.0,220.0,13.0,12.0,16.0')] ).
cnf(203,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ of(skc8,skc14,z)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[192,1]),
[iquote('0:MRR:192.0,1.0')] ).
cnf(1001,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ smoke(u,x)
| ~ present(u,x)
| ~ jules_forename(skc8,y)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,skc10)
| ~ agent(skc8,v,skc10)
| ~ agent(u,x,skc10)
| ~ of(skc8,y,skc10)
| man(skc12,skf4(skc12)) ),
inference(mrr,[status(thm)],[998,4]),
[iquote('0:MRR:998.0,4.0')] ).
cnf(204,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ state(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,x1)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ agent(skc8,x2,x4)
| ~ of(skc8,x5,x4)
| ~ of(skc8,skc14,x4)
| ~ be(skc8,x3,x4,x4) ),
inference(mrr,[status(thm)],[191,1]),
[iquote('0:MRR:191.0,1.0')] ).
cnf(926,plain,
( ~ agent(skc8,u,skf4(skc12))
| ~ smoke(skc12,u)
| ~ present(skc12,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ state(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ smoke(skc12,z)
| ~ present(skc12,z)
| ~ jules_forename(skc8,x1)
| ~ of(skc8,x,y)
| ~ agent(skc8,v,y)
| ~ agent(skc12,z,y)
| ~ of(skc8,x1,y)
| ~ theme(skc8,v,skc12)
| ~ be(skc8,w,y,y) ),
inference(mrr,[status(thm)],[925,13,12]),
[iquote('0:MRR:925.3,925.4,13.0,12.0')] ).
cnf(210,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,x1)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x2,x4)
| ~ of(skc8,x5,x4)
| ~ be(skc8,skc9,x4,x4) ),
inference(mrr,[status(thm)],[150,1]),
[iquote('0:MRR:150.0,1.0')] ).
cnf(928,plain,
( ~ man(skc12,skf4(skc12))
| ~ event(skc8,u)
| ~ present(skc8,u)
| ~ think_believe_consider(skc8,u)
| ~ state(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ smoke(skc12,y)
| ~ present(skc12,y)
| ~ jules_forename(skc8,z)
| ~ of(skc8,w,x)
| ~ agent(skc8,u,x)
| ~ agent(skc12,y,x)
| ~ of(skc8,z,x)
| ~ theme(skc8,u,skc12)
| ~ be(skc8,v,x,x) ),
inference(mrr,[status(thm)],[927,216,220,13,12]),
[iquote('0:MRR:927.1,927.2,927.3,927.4,216.0,220.0,13.0,12.0')] ).
cnf(972,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(823,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)],[821,93]),
[iquote('0:Res:821.1,93.4')] ).
cnf(208,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,z,skc10)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[157,1]),
[iquote('0:MRR:157.0,1.0')] ).
cnf(959,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)],[958,12]),
[iquote('0:MRR:958.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,167]),
[iquote('0:MRR:547.1,547.3,101.1,167.1')] ).
cnf(940,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(941,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(209,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x2)
| ~ present(skc8,x2)
| ~ think_believe_consider(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,skc10)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,x1)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,skc10)
| ~ agent(skc8,x2,skc10)
| ~ of(skc8,x5,skc10)
| ~ be(skc8,x3,skc10,skc10) ),
inference(mrr,[status(thm)],[156,1]),
[iquote('0:MRR:156.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(841,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)],[838,92]),
[iquote('0:Res:838.1,92.3')] ).
cnf(836,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)],[828,92]),
[iquote('0:Res:828.1,92.3')] ).
cnf(921,plain,
( ~ of(skc8,u,skc15)
| ~ forename(skc12,u)
| ~ forename(skc12,skc14)
| ~ entity(skc12,skc15)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[920,12]),
[iquote('0:MRR:920.1,12.0')] ).
cnf(212,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ smoke(skc12,x4)
| ~ present(skc12,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,skf4(u))
| ~ theme(skc8,w,u)
| ~ agent(skc8,w,y)
| ~ of(skc8,x,y)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ agent(skc12,x4,x3)
| ~ of(skc8,x5,x3)
| ~ theme(skc8,z,skc12)
| ~ be(skc8,x1,x3,x3) ),
inference(mrr,[status(thm)],[144,1,13]),
[iquote('0:MRR:144.0,144.19,1.0,13.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(913,plain,
( ~ of(skc8,u,skc10)
| ~ forename(skc12,u)
| ~ entity(skc12,skc10)
| equal(skc11,u) ),
inference(mrr,[status(thm)],[912,12]),
[iquote('0:MRR:912.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(903,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skf2(skc15),skc15) ),
inference(res,[status(thm),theory(equality)],[2,899]),
[iquote('0:Res:2.0,899.0')] ).
cnf(899,plain,
( ~ man(skc8,u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(v,w)
| agent(w,skf2(u),u) ),
inference(res,[status(thm),theory(equality)],[121,634]),
[iquote('0:Res:121.1,634.0')] ).
cnf(901,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skf2(skc10),skc10) ),
inference(mrr,[status(thm)],[900,12]),
[iquote('0:MRR:900.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(99,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ be(skc8,x2,x4,x4)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[1,96]),
[iquote('0:Res:1.0,96.0')] ).
cnf(621,plain,
( ~ be(skc8,u,v,w)
| ~ accessible_world(skc12,x)
| be(x,u,v,w) ),
inference(res,[status(thm),theory(equality)],[142,91]),
[iquote('0:Res:142.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(578,plain,
( ~ actual_world(u)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ accessible_world(u,y)
| ~ proposition(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,x1)
| ~ vincent_forename(u,x2)
| ~ man(u,x3)
| ~ smoke(y,x4)
| ~ present(y,x4)
| ~ jules_forename(u,x5)
| ~ theme(u,v,skc12)
| ~ agent(u,v,x)
| ~ of(u,w,x)
| ~ theme(u,z,y)
| ~ of(u,x2,x3)
| ~ agent(u,z,x3)
| ~ agent(y,x4,x3)
| ~ of(u,x5,x3)
| ~ be(u,x1,x3,x3) ),
inference(mrr,[status(thm)],[577,96,216,220]),
[iquote('0:MRR:577.1,577.20,577.21,96.28,216.0,220.0')] ).
cnf(866,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| be(v,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[856,91]),
[iquote('0:Res:856.1,91.1')] ).
cnf(856,plain,
( ~ accessible_world(skc12,u)
| be(u,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[12,587]),
[iquote('0:Res:12.0,587.0')] ).
cnf(587,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(849,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[843,90]),
[iquote('0:Res:843.1,90.1')] ).
cnf(174,plain,
( ~ actual_world(u)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ event(u,z)
| ~ present(u,z)
| ~ think_believe_consider(u,z)
| ~ state(u,x1)
| ~ vincent_forename(u,x2)
| ~ man(u,x3)
| ~ jules_forename(u,x4)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ of(u,x2,x3)
| ~ agent(u,z,x3)
| ~ of(u,x4,x3)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,x3)
| ~ be(u,x1,x3,x3)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[6,96]),
[iquote('0:Res:6.0,96.4')] ).
cnf(842,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| of(v,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[838,88]),
[iquote('0:Res:838.1,88.1')] ).
cnf(837,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| of(v,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[828,88]),
[iquote('0:Res:828.1,88.1')] ).
cnf(822,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| theme(v,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[821,89]),
[iquote('0:Res:821.1,89.1')] ).
cnf(843,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(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(838,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(828,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(206,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x4)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,x1)
| ~ of(skc8,z,x1)
| ~ of(skc8,x3,x4)
| ~ of(skc8,x5,x4)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,x4)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[185,1,7,6]),
[iquote('0:MRR:185.0,185.15,185.16,1.0,7.0,6.0')] ).
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(821,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(663,plain,
( ~ entity(skc8,skc15)
| ~ of(skc8,skc11,skc15)
| equal(skc14,skc11) ),
inference(mrr,[status(thm)],[660,3]),
[iquote('0:MRR:660.0,3.0')] ).
cnf(197,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ agent(u,v,x4)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,skc11,x4)
| ~ be(skc8,x2,x4,x4)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[162,1]),
[iquote('0:MRR:162.0,1.0')] ).
cnf(806,plain,
( ~ jules_forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[19,800]),
[iquote('0:Res:19.1,800.0')] ).
cnf(813,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc14) ),
inference(res,[status(thm),theory(equality)],[187,805]),
[iquote('0:Res:187.1,805.0')] ).
cnf(805,plain,
( ~ vincent_forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[20,800]),
[iquote('0:Res:20.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(193,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ man(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x3)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,x4,x3)
| ~ of(skc8,skc14,y)
| ~ be(skc8,x1,x3,x3)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[190,1]),
[iquote('0:MRR:190.0,1.0')] ).
cnf(800,plain,
( ~ forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[22,776]),
[iquote('0:Res:22.1,776.0')] ).
cnf(776,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,775]),
[iquote('0:Res:146.1,775.1')] ).
cnf(775,plain,
( ~ proposition(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[41,744]),
[iquote('0:Res:41.1,744.0')] ).
cnf(194,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ state(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x3)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ of(skc8,skc14,x3)
| ~ be(skc8,x2,x3,x3)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[189,1]),
[iquote('0:MRR:189.0,1.0')] ).
cnf(771,plain,
( ~ human_person(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[32,742]),
[iquote('0:Res:32.1,742.0')] ).
cnf(769,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(200,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x1)
| ~ present(skc8,x1)
| ~ think_believe_consider(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x3)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,x1,x3)
| ~ of(skc8,x4,x3)
| ~ be(skc8,skc9,x3,x3)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[149,1]),
[iquote('0:MRR:149.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(198,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,z)
| ~ present(skc8,z)
| ~ think_believe_consider(skc8,z)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x3)
| ~ theme(skc8,x,w)
| ~ theme(skc8,z,u)
| ~ of(skc8,x2,x3)
| ~ agent(skc8,z,x3)
| ~ of(skc8,x4,x3)
| ~ agent(skc8,x,skc10)
| ~ of(skc8,y,skc10)
| ~ be(skc8,x1,x3,x3)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[155,1]),
[iquote('0:MRR:155.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)],[181,721]),
[iquote('0:Res:181.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(202,plain,
( ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ state(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ smoke(skc12,x3)
| ~ present(skc12,x3)
| ~ jules_forename(skc8,x4)
| ~ theme(skc8,v,u)
| ~ agent(skc8,v,x)
| ~ of(skc8,w,x)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,y,x2)
| ~ agent(skc12,x3,x2)
| ~ of(skc8,x4,x2)
| ~ theme(skc8,y,skc12)
| ~ be(skc8,z,x2,x2)
| man(u,skf4(u)) ),
inference(mrr,[status(thm)],[138,1,13]),
[iquote('0:MRR:138.0,138.16,1.0,13.0')] ).
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)],[112,554]),
[iquote('0:Res:112.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)],[112,553]),
[iquote('0:Res:112.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,
( ~ jules_forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[19,702]),
[iquote('0:Res:19.1,702.0')] ).
cnf(707,plain,
( ~ vincent_forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[20,702]),
[iquote('0:Res:20.1,702.0')] ).
cnf(196,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ proposition(skc8,w)
| ~ accessible_world(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ state(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x3)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,z)
| ~ of(skc8,y,z)
| ~ of(skc8,x2,x3)
| ~ of(skc8,x4,x3)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,x3)
| ~ be(skc8,x1,x3,x3)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[183,1,7,6]),
[iquote('0:MRR:183.0,183.12,183.13,1.0,7.0,6.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(168,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)],[123,543]),
[iquote('0:Res:123.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,
( ~ jules_forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,675]),
[iquote('0:Res:19.1,675.0')] ).
cnf(677,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(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)],[181,542]),
[iquote('0:Res:181.1,542.0')] ).
cnf(656,plain,
~ jules_forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[19,649]),
[iquote('0:Res:19.1,649.0')] ).
cnf(655,plain,
~ vincent_forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[20,649]),
[iquote('0:Res:20.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,
~ jules_forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[19,648]),
[iquote('0:Res:19.1,648.0')] ).
cnf(653,plain,
~ vincent_forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[20,648]),
[iquote('0:Res:20.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)],[123,628]),
[iquote('0:Res:123.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(142,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)],[117,538]),
[iquote('0:Res:117.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)],[117,537]),
[iquote('0:Res:117.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,
( ~ jules_forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,581]),
[iquote('0:Res:19.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,
( ~ vincent_forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,581]),
[iquote('0:Res:20.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)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ accessible_world(u,z)
| ~ proposition(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ state(u,x2)
| ~ vincent_forename(u,x3)
| ~ man(u,x4)
| ~ smoke(z,x5)
| ~ present(z,x5)
| ~ jules_forename(u,x6)
| ~ smoke(v,x7)
| ~ present(v,x7)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ theme(u,x1,z)
| ~ of(u,x3,x4)
| ~ agent(u,x1,x4)
| ~ agent(z,x5,x4)
| ~ of(u,x6,x4)
| ~ agent(v,x7,skf4(v))
| ~ be(u,x2,x4,x4) ),
inference(mrr,[status(thm)],[95,48,19,20]),
[iquote('0:MRR:95.4,95.7,95.8,95.15,95.28,48.1,19.1,48.1,20.1,20.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)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ accessible_world(u,z)
| ~ proposition(u,z)
| ~ event(u,x1)
| ~ present(u,x1)
| ~ think_believe_consider(u,x1)
| ~ state(u,x2)
| ~ vincent_forename(u,x3)
| ~ man(u,x4)
| ~ smoke(z,x5)
| ~ present(z,x5)
| ~ jules_forename(u,x6)
| ~ theme(u,w,v)
| ~ agent(u,w,y)
| ~ of(u,x,y)
| ~ theme(u,x1,z)
| ~ of(u,x3,x4)
| ~ agent(u,x1,x4)
| ~ agent(z,x5,x4)
| ~ of(u,x6,x4)
| ~ be(u,x2,x4,x4)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[94,19,48,20]),
[iquote('0:MRR:94.3,94.4,94.11,94.24,19.1,48.1,20.1,20.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)],[112,247]),
[iquote('0:Res:112.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('NLP255+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('NLP255+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,
( ~ jules_forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,488]),
[iquote('0:Res:19.1,488.0')] ).
cnf(91,axiom,
( ~ accessible_world(u,v)
| ~ be(u,w,x,y)
| be(v,w,x,y) ),
file('NLP255+1.p',unknown),
[] ).
cnf(502,plain,
( ~ vincent_forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,488]),
[iquote('0:Res:20.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('NLP255+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('NLP255+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ accessible_world(u,v)
| ~ theme(u,w,x)
| theme(v,w,x) ),
file('NLP255+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('NLP255+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('NLP255+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)],[123,461]),
[iquote('0:Res:123.1,461.0')] ).
cnf(77,axiom,
( ~ accessible_world(u,v)
| ~ proposition(u,w)
| proposition(v,w) ),
file('NLP255+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('NLP255+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('NLP255+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(59,axiom,
( ~ accessible_world(u,v)
| ~ vincent_forename(u,w)
| vincent_forename(v,w) ),
file('NLP255+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)],[123,427]),
[iquote('0:Res:123.1,427.0')] ).
cnf(87,axiom,
( ~ accessible_world(u,v)
| ~ smoke(u,w)
| smoke(v,w) ),
file('NLP255+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('NLP255+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(58,axiom,
( ~ accessible_world(u,v)
| ~ jules_forename(u,w)
| jules_forename(v,w) ),
file('NLP255+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('NLP255+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('NLP255+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)],[112,385]),
[iquote('0:Res:112.1,385.0')] ).
cnf(388,plain,
~ male(skc8,skc13),
inference(res,[status(thm),theory(equality)],[112,384]),
[iquote('0:Res:112.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('NLP255+1.p',unknown),
[] ).
cnf(384,plain,
~ male(skc12,skc13),
inference(res,[status(thm),theory(equality)],[182,289]),
[iquote('0:Res:182.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,
~ jules_forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[19,368]),
[iquote('0:Res:19.1,368.0')] ).
cnf(70,axiom,
( ~ accessible_world(u,v)
| ~ human_person(u,w)
| human_person(v,w) ),
file('NLP255+1.p',unknown),
[] ).
cnf(377,plain,
~ vincent_forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[20,368]),
[iquote('0:Res:20.1,368.0')] ).
cnf(373,plain,
~ jules_forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[19,363]),
[iquote('0:Res:19.1,363.0')] ).
cnf(372,plain,
~ vincent_forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[20,363]),
[iquote('0:Res:20.1,363.0')] ).
cnf(371,plain,
~ jules_forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[19,362]),
[iquote('0:Res:19.1,362.0')] ).
cnf(75,axiom,
( ~ accessible_world(u,v)
| ~ abstraction(u,w)
| abstraction(v,w) ),
file('NLP255+1.p',unknown),
[] ).
cnf(370,plain,
~ vincent_forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[20,362]),
[iquote('0:Res:20.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,
~ jules_forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[19,356]),
[iquote('0:Res:19.1,356.0')] ).
cnf(365,plain,
~ vincent_forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[20,356]),
[iquote('0:Res:20.1,356.0')] ).
cnf(69,axiom,
( ~ accessible_world(u,v)
| ~ organism(u,w)
| organism(v,w) ),
file('NLP255+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('NLP255+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('NLP255+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('NLP255+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('NLP255+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)],[123,328]),
[iquote('0:Res:123.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('NLP255+1.p',unknown),
[] ).
cnf(331,plain,
~ general(skc8,skc13),
inference(res,[status(thm),theory(equality)],[123,327]),
[iquote('0:Res:123.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)],[182,287]),
[iquote('0:Res:182.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('NLP255+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('NLP255+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('NLP255+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('NLP255+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)],[117,292]),
[iquote('0:Res:117.1,292.0')] ).
cnf(74,axiom,
( ~ accessible_world(u,v)
| ~ nonhuman(u,w)
| nonhuman(v,w) ),
file('NLP255+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)],[117,291]),
[iquote('0:Res:117.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)],[182,286]),
[iquote('0:Res:182.0,286.0')] ).
cnf(81,axiom,
( ~ accessible_world(u,v)
| ~ nonexistent(u,w)
| nonexistent(v,w) ),
file('NLP255+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)],[130,55]),
[iquote('0:Res:130.1,55.1')] ).
cnf(237,plain,
( ~ specific(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[132,54]),
[iquote('0:Res:132.1,54.1')] ).
cnf(228,plain,
( ~ nonexistent(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[131,52]),
[iquote('0:Res:131.1,52.0')] ).
cnf(63,axiom,
( ~ accessible_world(u,v)
| ~ animate(u,w)
| animate(v,w) ),
file('NLP255+1.p',unknown),
[] ).
cnf(281,plain,
~ jules_forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[19,276]),
[iquote('0:Res:19.1,276.0')] ).
cnf(280,plain,
~ vincent_forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[20,276]),
[iquote('0:Res:20.1,276.0')] ).
cnf(279,plain,
~ jules_forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[19,274]),
[iquote('0:Res:19.1,274.0')] ).
cnf(278,plain,
~ vincent_forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[20,274]),
[iquote('0:Res:20.1,274.0')] ).
cnf(65,axiom,
( ~ accessible_world(u,v)
| ~ living(u,w)
| living(v,w) ),
file('NLP255+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('NLP255+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('NLP255+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)],[124,257]),
[iquote('0:Res:124.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('NLP255+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,
~ jules_forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[19,248]),
[iquote('0:Res:19.1,248.0')] ).
cnf(252,plain,
~ vincent_forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[20,248]),
[iquote('0:Res:20.1,248.0')] ).
cnf(251,plain,
~ jules_forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[19,244]),
[iquote('0:Res:19.1,244.0')] ).
cnf(56,axiom,
( ~ man(skc12,u)
| agent(skc12,skf2(u),u) ),
file('NLP255+1.p',unknown),
[] ).
cnf(250,plain,
~ vincent_forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[20,244]),
[iquote('0:Res:20.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('NLP255+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('NLP255+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)],[124,224]),
[iquote('0:Res:124.1,224.0')] ).
cnf(52,axiom,
( ~ nonexistent(u,v)
| ~ existent(u,v) ),
file('NLP255+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)],[114,53]),
[iquote('0:Res:114.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('NLP255+1.p',unknown),
[] ).
cnf(213,plain,
( ~ smoke(skc8,u)
| event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[137,48]),
[iquote('0:Res:137.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('NLP255+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ state(u,v)
| event(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ vincent_forename(u,v)
| forename(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ jules_forename(u,v)
| forename(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ event(u,v)
| eventuality(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ state(u,v)
| eventuality(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ organism(u,v)
| entity(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ man(u,v)
| human_person(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ relation(u,v)
| abstraction(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ proposition(u,v)
| relation(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ eventuality(u,v)
| thing(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ entity(u,v)
| thing(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ human_person(u,v)
| organism(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ abstraction(u,v)
| thing(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ relname(u,v)
| relation(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ man(u,v)
| male(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ forename(u,v)
| relname(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ eventuality(u,v)
| unisex(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ eventuality(u,v)
| specific(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ entity(u,v)
| specific(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ abstraction(u,v)
| unisex(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(173,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('NLP255+1.p',unknown),
[] ).
cnf(167,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(181,plain,
( ~ accessible_world(skc8,u)
| event(u,skc13) ),
inference(res,[status(thm),theory(equality)],[5,86]),
[iquote('0:Res:5.0,86.0')] ).
cnf(187,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(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('NLP255+1.p',unknown),
[] ).
cnf(163,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(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(129,plain,
( ~ present(skc8,u)
| present(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,79]),
[iquote('0:Res:12.0,79.1')] ).
cnf(121,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('NLP255+1.p',unknown),
[] ).
cnf(127,plain,
( ~ proposition(skc8,u)
| proposition(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,77]),
[iquote('0:Res:12.0,77.1')] ).
cnf(128,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(136,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,
( ~ vincent_forename(skc8,u)
| vincent_forename(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,59]),
[iquote('0:Res:12.0,59.1')] ).
cnf(37,axiom,
( ~ abstraction(u,v)
| general(u,v) ),
file('NLP255+1.p',unknown),
[] ).
cnf(137,plain,
( ~ smoke(skc8,u)
| smoke(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,87]),
[iquote('0:Res:12.0,87.1')] ).
cnf(122,plain,
( ~ state(skc8,u)
| state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,72]),
[iquote('0:Res:12.0,72.1')] ).
cnf(108,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(111,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('NLP255+1.p',unknown),
[] ).
cnf(135,plain,
( ~ eventuality(skc8,u)
| eventuality(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,85]),
[iquote('0:Res:12.0,85.1')] ).
cnf(118,plain,
( ~ entity(skc8,u)
| entity(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,68]),
[iquote('0:Res:12.0,68.1')] ).
cnf(120,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(125,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('NLP255+1.p',unknown),
[] ).
cnf(119,plain,
( ~ organism(skc8,u)
| organism(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,69]),
[iquote('0:Res:12.0,69.1')] ).
cnf(126,plain,
( ~ relation(skc8,u)
| relation(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,76]),
[iquote('0:Res:12.0,76.1')] ).
cnf(134,plain,
( ~ thing(skc8,u)
| thing(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,84]),
[iquote('0:Res:12.0,84.1')] ).
cnf(110,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('NLP255+1.p',unknown),
[] ).
cnf(112,plain,
( ~ male(skc8,u)
| male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,62]),
[iquote('0:Res:12.0,62.1')] ).
cnf(130,plain,
( ~ unisex(skc8,u)
| unisex(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,80]),
[iquote('0:Res:12.0,80.1')] ).
cnf(132,plain,
( ~ specific(skc8,u)
| specific(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,82]),
[iquote('0:Res:12.0,82.1')] ).
cnf(114,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('NLP255+1.p',unknown),
[] ).
cnf(117,plain,
( ~ existent(skc8,u)
| existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,67]),
[iquote('0:Res:12.0,67.1')] ).
cnf(123,plain,
( ~ general(skc8,u)
| general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,73]),
[iquote('0:Res:12.0,73.1')] ).
cnf(124,plain,
( ~ nonhuman(skc8,u)
| nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,74]),
[iquote('0:Res:12.0,74.1')] ).
cnf(131,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('NLP255+1.p',unknown),
[] ).
cnf(113,plain,
( ~ animate(skc8,u)
| animate(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,63]),
[iquote('0:Res:12.0,63.1')] ).
cnf(115,plain,
( ~ living(skc8,u)
| living(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,65]),
[iquote('0:Res:12.0,65.1')] ).
cnf(116,plain,
( ~ impartial(skc8,u)
| impartial(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,66]),
[iquote('0:Res:12.0,66.1')] ).
cnf(133,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('NLP255+1.p',unknown),
[] ).
cnf(15,axiom,
agent(skc8,skc13,skc15),
file('NLP255+1.p',unknown),
[] ).
cnf(14,axiom,
of(skc8,skc14,skc15),
file('NLP255+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('NLP255+1.p',unknown),
[] ).
cnf(182,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('NLP255+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('NLP255+1.p',unknown),
[] ).
cnf(12,axiom,
accessible_world(skc8,skc12),
file('NLP255+1.p',unknown),
[] ).
cnf(2,axiom,
man(skc8,skc15),
file('NLP255+1.p',unknown),
[] ).
cnf(10,axiom,
man(skc8,skc10),
file('NLP255+1.p',unknown),
[] ).
cnf(13,axiom,
proposition(skc8,skc12),
file('NLP255+1.p',unknown),
[] ).
cnf(5,axiom,
event(skc8,skc13),
file('NLP255+1.p',unknown),
[] ).
cnf(7,axiom,
think_believe_consider(skc8,skc13),
file('NLP255+1.p',unknown),
[] ).
cnf(4,axiom,
vincent_forename(skc8,skc14),
file('NLP255+1.p',unknown),
[] ).
cnf(11,axiom,
state(skc8,skc9),
file('NLP255+1.p',unknown),
[] ).
cnf(8,axiom,
jules_forename(skc8,skc11),
file('NLP255+1.p',unknown),
[] ).
cnf(3,axiom,
forename(skc8,skc14),
file('NLP255+1.p',unknown),
[] ).
cnf(9,axiom,
forename(skc8,skc11),
file('NLP255+1.p',unknown),
[] ).
cnf(1,axiom,
actual_world(skc8),
file('NLP255+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NLP255+1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n020.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 09:30:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.08/1.33
% 1.08/1.33 SPASS V 3.9
% 1.08/1.33 SPASS beiseite: Completion found.
% 1.08/1.33 % SZS status CounterSatisfiable
% 1.08/1.33 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.08/1.33 SPASS derived 1125 clauses, backtracked 0 clauses, performed 0 splits and kept 632 clauses.
% 1.08/1.33 SPASS allocated 100202 KBytes.
% 1.08/1.33 SPASS spent 0:00:00.99 on the problem.
% 1.08/1.33 0:00:00.03 for the input.
% 1.08/1.33 0:00:00.17 for the FLOTTER CNF translation.
% 1.08/1.33 0:00:00.06 for inferences.
% 1.08/1.33 0:00:00.00 for the backtracking.
% 1.08/1.33 0:00:00.58 for the reduction.
% 1.08/1.33
% 1.08/1.33
% 1.08/1.33 The saturated set of worked-off clauses is :
% 1.08/1.33 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------