%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP254+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n012.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:12 EDT 2022
% Result : CounterSatisfiable 1.82s 2.03s
% Output : Saturation 1.82s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 2021)
% Comments :
%------------------------------------------------------------------------------
cnf(2025,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ state(u,skc9)
| ~ vincent_forename(u,x)
| ~ man(u,skc10)
| ~ jules_forename(u,y)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(obv,[status(thm),theory(equality)],[2021]),
[iquote('0:Obv:2021.1')] ).
cnf(1958,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,w)
| ~ smoke(v,skf2(x))
| ~ present(v,skf2(x))
| ~ man(u,x)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,y)
| ~ present(u,y)
| ~ event(u,y)
| ~ state(u,skc9)
| ~ vincent_forename(u,z)
| ~ man(u,skc10)
| ~ jules_forename(u,x1)
| ~ of(u,w,x)
| ~ theme(u,y,v)
| ~ of(u,z,skc10)
| ~ agent(u,y,skc10)
| ~ of(u,x1,skc10) ),
inference(mrr,[status(thm)],[1947,71]),
[iquote('0:MRR:1947.1,71.2')] ).
cnf(2018,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,v)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ state(u,skc9)
| ~ vincent_forename(u,x)
| ~ man(u,skc10)
| ~ jules_forename(u,y)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(obv,[status(thm),theory(equality)],[2014]),
[iquote('0:Obv:2014.1')] ).
cnf(2026,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc15)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ vincent_forename(skc12,skc14)
| ~ jules_forename(skc12,u)
| ~ smoke(v,skc13)
| ~ man(skc12,skc15)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,y)
| ~ theme(skc12,w,v)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10) ),
inference(obv,[status(thm),theory(equality)],[2023]),
[iquote('0:Obv:2023.3')] ).
cnf(2035,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,v)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,skc14)
| ~ smoke(v,skc13)
| ~ man(skc12,skc15)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ vincent_forename(skc12,w)
| ~ jules_forename(skc12,x)
| ~ of(skc12,w,skc10)
| ~ agent(skc12,u,skc10)
| ~ of(skc12,x,skc10) ),
inference(mrr,[status(thm)],[2034,12]),
[iquote('0:MRR:2034.2,12.0')] ).
cnf(2024,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ jules_forename(u,y)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(mrr,[status(thm)],[2022,101,185,177,171,191,146,151]),
[iquote('0:MRR:2022.5,2022.6,2022.7,2022.8,2022.9,2022.18,2022.20,101.1,185.1,177.1,171.1,191.1,146.1,151.1')] ).
cnf(1954,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,w)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ jules_forename(u,z)
| ~ of(u,w,skc15)
| ~ theme(u,x,v)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10) ),
inference(mrr,[status(thm)],[1953,79]),
[iquote('0:MRR:1953.11,79.2')] ).
cnf(1952,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,v)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,w)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ jules_forename(u,z)
| ~ of(u,w,skc15)
| ~ theme(u,x,v)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10) ),
inference(mrr,[status(thm)],[1951,79]),
[iquote('0:MRR:1951.11,79.2')] ).
cnf(1972,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,v)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ vincent_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ jules_forename(skc12,u)
| ~ man(skc12,v)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,y)
| ~ theme(skc12,w,skc12)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10) ),
inference(obv,[status(thm),theory(equality)],[1965]),
[iquote('0:Obv:1965.2')] ).
cnf(2009,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10) ),
inference(obv,[status(thm),theory(equality)],[2006]),
[iquote('0:Obv:2006.1')] ).
cnf(1997,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ state(u,skc9)
| ~ vincent_forename(u,v)
| ~ man(u,skc10)
| ~ jules_forename(u,w)
| ~ of(u,v,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,w,skc10) ),
inference(obv,[status(thm),theory(equality)],[1992]),
[iquote('0:Obv:1992.5')] ).
cnf(1950,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,v)
| ~ smoke(skc8,skc13)
| ~ man(u,skc15)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ state(u,skc9)
| ~ vincent_forename(u,x)
| ~ man(u,skc10)
| ~ jules_forename(u,y)
| ~ of(u,v,skc15)
| ~ theme(u,w,skc8)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(mrr,[status(thm)],[1949,79]),
[iquote('0:MRR:1949.10,79.2')] ).
cnf(1971,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,skc11)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,w)
| ~ man(u,skc10)
| ~ jules_forename(u,x)
| ~ theme(u,v,skc12)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10) ),
inference(obv,[status(thm),theory(equality)],[1961]),
[iquote('0:Obv:1961.9')] ).
cnf(1987,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10) ),
inference(obv,[status(thm),theory(equality)],[1984]),
[iquote('0:Obv:1984.1')] ).
cnf(1981,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,skc13)
| ~ present(u,skc13)
| ~ event(u,skc13)
| ~ state(u,skc9)
| ~ vincent_forename(u,v)
| ~ man(u,skc10)
| ~ jules_forename(u,w)
| ~ of(u,v,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,w,skc10) ),
inference(obv,[status(thm),theory(equality)],[1976]),
[iquote('0:Obv:1976.5')] ).
cnf(1969,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,w)
| ~ man(u,skc10)
| ~ jules_forename(u,x)
| ~ theme(u,v,skc12)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10) ),
inference(obv,[status(thm),theory(equality)],[1963]),
[iquote('0:Obv:1963.7')] ).
cnf(1926,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ man(u,y)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ state(u,skc9)
| ~ vincent_forename(u,x1)
| ~ man(u,skc10)
| ~ jules_forename(u,x2)
| ~ agent(u,skc13,skc10)
| ~ agent(w,x,y)
| ~ of(u,v,y)
| ~ theme(u,z,w)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10) ),
inference(obv,[status(thm),theory(equality)],[1915]),
[iquote('0:Obv:1915.9')] ).
cnf(1957,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ proposition(u,skc12)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ jules_forename(u,z)
| ~ of(u,v,w)
| ~ theme(u,x,skc12)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10) ),
inference(mrr,[status(thm)],[1956,71,224,228]),
[iquote('0:MRR:1956.1,1956.9,1956.10,71.2,224.0,228.0')] ).
cnf(1924,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ man(u,y)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ state(u,skc9)
| ~ vincent_forename(u,x1)
| ~ man(u,skc10)
| ~ jules_forename(u,x2)
| ~ agent(w,x,y)
| ~ of(u,v,y)
| ~ theme(u,z,w)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10) ),
inference(mrr,[status(thm)],[1923,838]),
[iquote('0:MRR:1923.22,838.1')] ).
cnf(1940,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(skc12,skc8)
| ~ jules_forename(skc8,v)
| ~ smoke(u,skf2(w))
| ~ present(u,skf2(w))
| ~ man(skc8,w)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(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) ),
inference(mrr,[status(thm)],[1937,121]),
[iquote('0:MRR:1937.0,121.1')] ).
cnf(1921,plain,
( ~ accessible_world(skc12,skc8)
| ~ jules_forename(skc8,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ man(skc8,x)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(v,w,x)
| ~ of(skc8,u,x)
| ~ theme(skc8,y,v)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10) ),
inference(mrr,[status(thm)],[1920,12,13,5,6,7,4,2,11,10,838]),
[iquote('0:MRR:1920.1,1920.2,1920.3,1920.4,1920.5,1920.6,1920.7,1920.17,1920.19,1920.21,12.0,13.0,5.0,6.0,7.0,4.0,2.0,11.0,10.0,838.1')] ).
cnf(874,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ smoke(x1,x2)
| ~ present(x1,x2)
| ~ man(u,x3)
| ~ proposition(u,x1)
| ~ accessible_world(u,x1)
| ~ think_believe_consider(u,x4)
| ~ present(u,x4)
| ~ event(u,x4)
| ~ state(u,skc9)
| ~ vincent_forename(u,x5)
| ~ man(u,skc10)
| ~ jules_forename(u,x6)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ agent(x1,x2,x3)
| ~ of(u,z,x3)
| ~ theme(u,x4,x1)
| ~ of(u,x5,skc10)
| ~ agent(u,x4,skc10)
| ~ of(u,x6,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[861,96]),
[iquote('0:Res:861.1,96.30')] ).
cnf(1911,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ smoke(y,z)
| ~ present(y,z)
| ~ man(u,x1)
| ~ proposition(u,y)
| ~ accessible_world(u,y)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ state(u,skc9)
| ~ vincent_forename(u,x3)
| ~ man(u,skc10)
| ~ jules_forename(u,x4)
| ~ of(u,v,w)
| ~ agent(u,skc13,w)
| ~ agent(y,z,x1)
| ~ of(u,x,x1)
| ~ theme(u,x2,y)
| ~ of(u,x3,skc10)
| ~ agent(u,x2,skc10)
| ~ of(u,x4,skc10) ),
inference(obv,[status(thm),theory(equality)],[1908]),
[iquote('0:Obv:1908.1')] ).
cnf(915,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ smoke(z,x1)
| ~ present(z,x1)
| ~ man(u,x2)
| ~ proposition(u,z)
| ~ accessible_world(u,z)
| ~ think_believe_consider(u,x3)
| ~ present(u,x3)
| ~ event(u,x3)
| ~ state(u,skc9)
| ~ vincent_forename(u,x4)
| ~ man(u,skc10)
| ~ jules_forename(u,x5)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ agent(z,x1,x2)
| ~ of(u,y,x2)
| ~ theme(u,x3,z)
| ~ of(u,x4,skc10)
| ~ agent(u,x3,skc10)
| ~ of(u,x5,skc10) ),
inference(res,[status(thm),theory(equality)],[861,586]),
[iquote('0:Res:861.1,586.30')] ).
cnf(899,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ man(u,x1)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ state(u,skc9)
| ~ vincent_forename(u,x3)
| ~ man(u,skc10)
| ~ jules_forename(u,x4)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ of(u,z,x1)
| ~ of(u,x3,skc10)
| ~ agent(u,x2,skc10)
| ~ of(u,x4,skc10)
| ~ theme(u,x2,skc8)
| ~ agent(skc8,skc13,x1)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[861,182]),
[iquote('0:Res:861.1,182.29')] ).
cnf(1901,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ vincent_forename(skc12,skc11)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,w)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,skc10)
| ~ agent(skc12,u,skc10)
| ~ of(skc12,w,skc10)
| ~ theme(skc12,u,skc8) ),
inference(mrr,[status(thm)],[1900,221]),
[iquote('0:MRR:1900.4,221.1')] ).
cnf(1591,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ event(skc12,w)
| ~ present(skc12,w)
| ~ think_believe_consider(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,y)
| ~ jules_forename(skc12,z)
| ~ man(skc12,x1)
| ~ think_believe_consider(skc12,x2)
| ~ present(skc12,x2)
| ~ event(skc12,x2)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x3)
| ~ man(skc12,v)
| ~ jules_forename(skc12,x4)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(skc12,w,skc12)
| ~ of(skc12,x,y)
| ~ agent(skc12,w,y)
| ~ of(skc12,z,x1)
| ~ of(skc12,x3,v)
| ~ agent(skc12,x2,v)
| ~ of(skc12,x4,v)
| ~ theme(skc12,x2,skc8)
| ~ agent(skc8,skc13,x1) ),
inference(res,[status(thm),theory(equality)],[141,1197]),
[iquote('0:Res:141.1,1197.29')] ).
cnf(1826,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ jules_forename(u,z)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10)
| ~ theme(u,x,skc8)
| ~ agent(skc8,skc13,w) ),
inference(obv,[status(thm),theory(equality)],[1816]),
[iquote('0:Obv:1816.9')] ).
cnf(1895,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,skc11)
| ~ think_believe_consider(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ event(u,skf2(skc10))
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1894,71]),
[iquote('0:MRR:1894.1,71.2')] ).
cnf(1887,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,skc11)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,w)
| ~ proposition(u,skc8)
| ~ accessible_world(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)],[1884]),
[iquote('0:Obv:1884.1')] ).
cnf(1843,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,skc11)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,w)
| ~ man(u,skc10)
| ~ jules_forename(u,x)
| ~ proposition(u,skc8)
| ~ accessible_world(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)],[1832]),
[iquote('0:Obv:1832.11')] ).
cnf(643,plain,
( ~ actual_world(u)
| ~ man(skc12,skf4(v))
| ~ accessible_world(skc12,v)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ smoke(x1,x2)
| ~ present(x1,x2)
| ~ man(u,x3)
| ~ proposition(u,x1)
| ~ accessible_world(u,x1)
| ~ think_believe_consider(u,x4)
| ~ present(u,x4)
| ~ event(u,x4)
| ~ state(u,x5)
| ~ vincent_forename(u,x6)
| ~ man(u,x7)
| ~ jules_forename(u,x8)
| ~ smoke(v,skf2(skf4(v)))
| ~ present(v,skf2(skf4(v)))
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ agent(x1,x2,x3)
| ~ of(u,z,x3)
| ~ theme(u,x4,x1)
| ~ of(u,x6,x7)
| ~ agent(u,x4,x7)
| ~ of(u,x8,x7)
| ~ be(u,x5,x7,x7) ),
inference(res,[status(thm),theory(equality)],[507,97]),
[iquote('0:Res:507.2,97.32')] ).
cnf(1878,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ think_believe_consider(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ event(u,skf2(skc10))
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,v)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc8) ),
inference(mrr,[status(thm)],[1877,71]),
[iquote('0:MRR:1877.1,71.2')] ).
cnf(1852,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,skc11)
| ~ man(u,skc10)
| ~ jules_forename(u,w)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,v,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,v,skc8) ),
inference(obv,[status(thm),theory(equality)],[1846]),
[iquote('0:Obv:1846.1')] ).
cnf(1854,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ vincent_forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,v)
| ~ present(skc12,v)
| ~ event(skc12,v)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,u)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,w)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc12,v,skc10)
| ~ of(skc12,w,skc10)
| ~ theme(skc12,v,skc8) ),
inference(mrr,[status(thm)],[1853,221]),
[iquote('0:MRR:1853.4,221.1')] ).
cnf(1869,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,skf2(skc10),skc8)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,u,skc10) ),
inference(mrr,[status(thm)],[1868,151,12,228,225]),
[iquote('0:MRR:1868.2,1868.3,1868.8,1868.9,151.1,12.0,228.0,225.0')] ).
cnf(1217,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(v,w,x2)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,v)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ be(skc8,x4,x6,x6) ),
inference(res,[status(thm),theory(equality)],[507,98]),
[iquote('0:Res:507.2,98.23')] ).
cnf(1866,plain,
( ~ actual_world(u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc8,u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ think_believe_consider(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ event(u,skf2(skc10))
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc8) ),
inference(obv,[status(thm),theory(equality)],[1860]),
[iquote('0:Obv:1860.2')] ).
cnf(1863,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,v)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,skc10)
| ~ theme(skc12,u,skc8) ),
inference(mrr,[status(thm)],[1862,12]),
[iquote('0:MRR:1862.2,12.0')] ).
cnf(1865,plain,
( ~ actual_world(skc12)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,u,skc10)
| ~ theme(skc12,skf2(skc10),skc8) ),
inference(mrr,[status(thm)],[1864,151,12,228,225]),
[iquote('0:MRR:1864.1,1864.2,1864.7,1864.8,151.1,12.0,228.0,225.0')] ).
cnf(1851,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,w)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,v,skc10)
| ~ of(u,w,skc10)
| ~ theme(u,v,skc8) ),
inference(mrr,[status(thm)],[1847,101,185,177,171,191,146,151]),
[iquote('0:MRR:1847.4,1847.5,1847.6,1847.7,1847.8,1847.14,1847.16,101.1,185.1,177.1,171.1,191.1,146.1,151.1')] ).
cnf(1195,plain,
( ~ actual_world(u)
| ~ man(skc12,skf4(v))
| ~ accessible_world(skc12,v)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ man(u,x1)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ state(u,x3)
| ~ vincent_forename(u,x4)
| ~ man(u,x5)
| ~ jules_forename(u,x6)
| ~ smoke(v,skf2(skf4(v)))
| ~ present(v,skf2(skf4(v)))
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ of(u,z,x1)
| ~ of(u,x4,x5)
| ~ agent(u,x2,x5)
| ~ of(u,x6,x5)
| ~ theme(u,x2,skc8)
| ~ agent(skc8,skc13,x1)
| ~ be(u,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,184]),
[iquote('0:Res:507.2,184.30')] ).
cnf(1856,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,skc8)
| ~ jules_forename(skc8,skc14)
| ~ think_believe_consider(skc8,skf2(skc10))
| ~ present(skc8,skf2(skc10))
| ~ event(skc8,skf2(skc10))
| ~ vincent_forename(skc8,skc11)
| ~ jules_forename(skc8,u)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,skf2(skc10),skc8) ),
inference(obv,[status(thm),theory(equality)],[1855]),
[iquote('0:Obv:1855.1')] ).
cnf(1850,plain,
( ~ accessible_world(skc12,skc8)
| ~ jules_forename(skc8,skc14)
| ~ think_believe_consider(skc8,u)
| ~ present(skc8,u)
| ~ event(skc8,u)
| ~ vincent_forename(skc8,skc11)
| ~ jules_forename(skc8,v)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc8,u,skc10)
| ~ of(skc8,v,skc10)
| ~ theme(skc8,u,skc8) ),
inference(mrr,[status(thm)],[1849,12,101,48,177,171,191,2,146,151]),
[iquote('0:MRR:1849.1,1849.2,1849.3,1849.4,1849.5,1849.6,1849.8,1849.12,1849.14,12.0,101.1,48.1,177.1,171.1,191.1,2.0,146.1,151.1')] ).
cnf(1841,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ jules_forename(u,skc14)
| ~ man(u,skc15)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ state(u,skc9)
| ~ vincent_forename(u,w)
| ~ man(u,skc10)
| ~ jules_forename(u,x)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10)
| ~ theme(u,v,skc8) ),
inference(mrr,[status(thm)],[1840,842]),
[iquote('0:MRR:1840.24,842.2')] ).
cnf(1824,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,skc14)
| ~ man(u,skc15)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ state(u,skc9)
| ~ vincent_forename(u,y)
| ~ man(u,skc10)
| ~ jules_forename(u,z)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10)
| ~ theme(u,x,skc8)
| ~ agent(skc8,skc13,w) ),
inference(mrr,[status(thm)],[1823,838]),
[iquote('0:MRR:1823.21,838.1')] ).
cnf(1137,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x1)
| ~ theme(skc8,x,u)
| ~ agent(skc8,x,y)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,v)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,skc14,y)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,209]),
[iquote('0:Res:507.2,209.22')] ).
cnf(1812,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,skc13)
| ~ present(u,skc13)
| ~ think_believe_consider(u,skc13)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ man(u,y)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ state(u,skc9)
| ~ vincent_forename(u,x1)
| ~ man(u,skc10)
| ~ jules_forename(u,x2)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,w)
| ~ agent(u,skc13,w)
| ~ of(u,x,y)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,y) ),
inference(obv,[status(thm),theory(equality)],[1809]),
[iquote('0:Obv:1809.1')] ).
cnf(1589,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ man(u,z)
| ~ think_believe_consider(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ state(u,skc9)
| ~ vincent_forename(u,x2)
| ~ man(u,skc10)
| ~ jules_forename(u,x3)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ of(u,y,z)
| ~ of(u,x2,skc10)
| ~ agent(u,x1,skc10)
| ~ of(u,x3,skc10)
| ~ theme(u,x1,skc8)
| ~ agent(skc8,skc13,z) ),
inference(res,[status(thm),theory(equality)],[861,1197]),
[iquote('0:Res:861.1,1197.29')] ).
cnf(1578,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,v)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ vincent_forename(skc12,w)
| ~ man(skc12,x)
| ~ jules_forename(skc12,y)
| ~ smoke(z,x1)
| ~ present(z,x1)
| ~ man(skc12,x2)
| ~ proposition(skc12,z)
| ~ accessible_world(skc12,z)
| ~ think_believe_consider(skc12,x3)
| ~ present(skc12,x3)
| ~ event(skc12,x3)
| ~ vincent_forename(skc12,x4)
| ~ jules_forename(skc12,x5)
| ~ of(skc12,w,x)
| ~ agent(skc12,u,x)
| ~ agent(z,x1,x2)
| ~ of(skc12,y,x2)
| ~ theme(skc12,x3,z)
| ~ of(skc12,x4,skc10)
| ~ agent(skc12,x3,skc10)
| ~ of(skc12,x5,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1576,12]),
[iquote('0:MRR:1576.2,12.0')] ).
cnf(1557,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,v)
| ~ accessible_world(skc12,v)
| ~ proposition(skc12,v)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ vincent_forename(skc12,w)
| ~ man(skc12,x)
| ~ jules_forename(skc12,y)
| ~ man(skc12,z)
| ~ think_believe_consider(skc12,x1)
| ~ present(skc12,x1)
| ~ event(skc12,x1)
| ~ vincent_forename(skc12,x2)
| ~ jules_forename(skc12,x3)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,w,x)
| ~ agent(skc12,u,x)
| ~ of(skc12,y,z)
| ~ of(skc12,x2,skc10)
| ~ agent(skc12,x1,skc10)
| ~ of(skc12,x3,skc10)
| ~ theme(skc12,x1,skc8)
| ~ agent(skc8,skc13,z)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1553,12]),
[iquote('0:MRR:1553.2,12.0')] ).
cnf(1117,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x1)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x2,v)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,skc11,x1)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,213]),
[iquote('0:Res:507.2,213.22')] ).
cnf(1746,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ accessible_world(skc12,skc12)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,w)
| ~ jules_forename(skc12,x)
| ~ man(skc12,y)
| ~ think_believe_consider(skc12,z)
| ~ present(skc12,z)
| ~ event(skc12,z)
| ~ vincent_forename(skc12,x1)
| ~ jules_forename(skc12,x2)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,v,w)
| ~ agent(skc12,u,w)
| ~ of(skc12,x,y)
| ~ of(skc12,x1,skc10)
| ~ agent(skc12,z,skc10)
| ~ of(skc12,x2,skc10)
| ~ theme(skc12,z,skc8)
| ~ agent(skc8,skc13,y) ),
inference(mrr,[status(thm)],[1742,12]),
[iquote('0:MRR:1742.2,12.0')] ).
cnf(1765,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,v)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ man(skc12,v)
| ~ jules_forename(skc12,w)
| ~ man(skc12,x)
| ~ think_believe_consider(skc12,y)
| ~ present(skc12,y)
| ~ event(skc12,y)
| ~ vincent_forename(skc12,z)
| ~ jules_forename(skc12,x1)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(skc12,skc13,v)
| ~ of(skc12,w,x)
| ~ of(skc12,z,skc10)
| ~ agent(skc12,y,skc10)
| ~ of(skc12,x1,skc10)
| ~ theme(skc12,y,skc8)
| ~ agent(skc8,skc13,x) ),
inference(mrr,[status(thm)],[1755,12]),
[iquote('0:MRR:1755.2,12.0')] ).
cnf(1805,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,skc10)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ man(skc12,v)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ jules_forename(skc12,y)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,u,v)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10)
| ~ theme(skc12,w,skc8)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[1804,12]),
[iquote('0:MRR:1804.2,12.0')] ).
cnf(1764,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ vincent_forename(u,y)
| ~ jules_forename(u,z)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10)
| ~ theme(u,x,skc8)
| ~ agent(skc8,skc13,w) ),
inference(mrr,[status(thm)],[1763,151]),
[iquote('0:MRR:1763.4,151.1')] ).
cnf(1102,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x2)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,v)
| ~ agent(skc8,x3,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,skc14,x5)
| ~ be(skc8,x4,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,210]),
[iquote('0:Res:507.2,210.22')] ).
cnf(1787,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,v)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ jules_forename(skc12,u)
| ~ man(skc12,v)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ jules_forename(skc12,y)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10)
| ~ theme(skc12,w,skc8)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[1780,12]),
[iquote('0:MRR:1780.2,12.0')] ).
cnf(1798,plain,
( ~ actual_world(u)
| ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ think_believe_consider(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ event(u,skf2(skc10))
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,skc10)
| ~ theme(u,skf2(skc10),skc8)
| ~ agent(skc8,skc13,skc10) ),
inference(res,[status(thm),theory(equality)],[507,1793]),
[iquote('0:Res:507.2,1793.12')] ).
cnf(1794,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ accessible_world(skc12,skc12)
| ~ man(skc12,skc15)
| ~ think_believe_consider(skc12,v)
| ~ present(skc12,v)
| ~ event(skc12,v)
| ~ vincent_forename(skc12,u)
| ~ jules_forename(skc12,w)
| ~ proposition(skc12,skc8)
| ~ accessible_world(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)],[1791,12]),
[iquote('0:MRR:1791.2,12.0')] ).
cnf(1793,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,w)
| ~ proposition(u,skc8)
| ~ accessible_world(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)],[1790]),
[iquote('0:Obv:1790.1')] ).
cnf(1074,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ agent(v,w,x2)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,v)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,skc11,x6)
| ~ be(skc8,x4,x6,x6) ),
inference(res,[status(thm),theory(equality)],[507,214]),
[iquote('0:Res:507.2,214.22')] ).
cnf(1786,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ jules_forename(u,x)
| ~ proposition(u,skc8)
| ~ accessible_world(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)],[1785,165,151]),
[iquote('0:MRR:1785.4,1785.5,165.1,151.1')] ).
cnf(1762,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ jules_forename(u,v)
| ~ man(u,w)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ vincent_forename(u,y)
| ~ jules_forename(u,z)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,w)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10)
| ~ theme(u,x,skc8)
| ~ agent(skc8,skc13,w) ),
inference(mrr,[status(thm)],[1761,191,506]),
[iquote('0:MRR:1761.3,1761.15,191.1,506.1')] ).
cnf(1758,plain,
( ~ jules_forename(skc8,u)
| ~ man(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ jules_forename(skc8,y)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ smoke(skc8,skc13)
| ~ of(skc8,u,v)
| ~ of(skc8,x,skc10)
| ~ agent(skc8,w,skc10)
| ~ of(skc8,y,skc10)
| ~ theme(skc8,w,skc8)
| ~ agent(skc8,skc13,v) ),
inference(mrr,[status(thm)],[1757,12,191,2,506]),
[iquote('0:MRR:1757.0,1757.1,1757.2,1757.13,12.0,191.1,2.0,506.1')] ).
cnf(1745,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ man(u,y)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ vincent_forename(u,x1)
| ~ jules_forename(u,x2)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,v,w)
| ~ agent(u,skc13,w)
| ~ of(u,x,y)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10)
| ~ theme(u,z,skc8)
| ~ agent(skc8,skc13,y) ),
inference(mrr,[status(thm)],[1744,185,177,171]),
[iquote('0:MRR:1744.3,1744.4,1744.5,185.1,177.1,171.1')] ).
cnf(1057,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x2)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,v)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x3,x5)
| ~ of(skc8,x6,x5)
| ~ be(skc8,skc9,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,218]),
[iquote('0:Res:507.2,218.22')] ).
cnf(1594,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ man(u,z)
| ~ think_believe_consider(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ vincent_forename(u,x2)
| ~ jules_forename(u,x3)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ of(u,y,z)
| ~ of(u,x2,skc10)
| ~ agent(u,x1,skc10)
| ~ of(u,x3,skc10)
| ~ theme(u,x1,skc8)
| ~ agent(skc8,skc13,z) ),
inference(mrr,[status(thm)],[1590,101,146,151]),
[iquote('0:MRR:1590.3,1590.14,1590.16,101.1,146.1,151.1')] ).
cnf(1474,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ accessible_world(skc12,skc12)
| ~ event(skc12,u)
| ~ present(skc12,u)
| ~ think_believe_consider(skc12,u)
| ~ vincent_forename(skc12,v)
| ~ man(skc12,w)
| ~ jules_forename(skc12,x)
| ~ smoke(y,z)
| ~ present(y,z)
| ~ man(skc12,x1)
| ~ proposition(skc12,y)
| ~ accessible_world(skc12,y)
| ~ think_believe_consider(skc12,x2)
| ~ present(skc12,x2)
| ~ event(skc12,x2)
| ~ vincent_forename(skc12,x3)
| ~ jules_forename(skc12,x4)
| ~ of(skc12,v,w)
| ~ agent(skc12,u,w)
| ~ agent(y,z,x1)
| ~ of(skc12,x,x1)
| ~ theme(skc12,x2,y)
| ~ of(skc12,x3,skc10)
| ~ agent(skc12,x2,skc10)
| ~ of(skc12,x4,skc10) ),
inference(mrr,[status(thm)],[1471,12]),
[iquote('0:MRR:1471.2,12.0')] ).
cnf(1730,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,x)
| ~ of(skc8,y,v)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc14,x) ),
inference(mrr,[status(thm)],[1727,121]),
[iquote('0:MRR:1727.0,121.1')] ).
cnf(1706,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc11,v) ),
inference(mrr,[status(thm)],[1701,121]),
[iquote('0:MRR:1701.0,121.1')] ).
cnf(1039,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,skc10)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x2,v)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,x1,skc10)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,216]),
[iquote('0:Res:507.2,216.22')] ).
cnf(1463,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ of(skc8,z,v)
| ~ theme(skc8,x1,u)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1456,121]),
[iquote('0:MRR:1456.0,121.1')] ).
cnf(1446,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,z)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,x)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ of(skc8,skc14,x) ),
inference(mrr,[status(thm)],[1443,11,10]),
[iquote('0:MRR:1443.13,1443.15,11.0,10.0')] ).
cnf(1719,plain,
( ~ smoke(u,skc13)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ jules_forename(skc8,x)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,skc10)
| ~ agent(skc8,v,skc10)
| ~ of(skc8,x,skc10)
| ~ of(skc8,skc11,skc15) ),
inference(mrr,[status(thm)],[1714,4,2,15]),
[iquote('0:MRR:1714.1,1714.2,1714.10,4.0,2.0,15.0')] ).
cnf(1006,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)))
| ~ 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)
| ~ man(skc8,x1)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x1)
| ~ theme(skc8,x,u)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,v)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,y,skc10)
| ~ agent(skc8,x,skc10)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,215]),
[iquote('0:Res:507.2,215.22')] ).
cnf(1425,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,z)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ of(skc8,skc11,z) ),
inference(mrr,[status(thm)],[1422,11,10]),
[iquote('0:MRR:1422.13,1422.15,11.0,10.0')] ).
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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x2)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,v)
| ~ of(skc8,x5,skc10)
| ~ agent(skc8,x3,skc10)
| ~ of(skc8,x6,skc10)
| ~ be(skc8,x4,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[507,217]),
[iquote('0:Res:507.2,217.22')] ).
cnf(973,plain,
( ~ man(skc12,skf4(u))
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skf4(u)))
| ~ present(u,skf2(skf4(u)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ smoke(skc12,z)
| ~ present(skc12,z)
| ~ man(skc8,x1)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ agent(skc12,z,x1)
| ~ of(skc8,y,x1)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ theme(skc8,x2,skc12)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,220]),
[iquote('0:Res:507.2,220.20')] ).
cnf(878,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)))
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(v,w,x2)
| ~ theme(skc8,x,u)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ of(skc8,x4,x5)
| ~ of(skc8,x6,x5)
| ~ theme(skc8,skc13,v)
| ~ agent(skc8,skc13,x5)
| ~ be(skc8,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[507,212]),
[iquote('0:Res:507.2,212.20')] ).
cnf(1507,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,v)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ man(skc12,v)
| ~ jules_forename(skc12,w)
| ~ smoke(x,y)
| ~ present(x,y)
| ~ man(skc12,z)
| ~ proposition(skc12,x)
| ~ accessible_world(skc12,x)
| ~ think_believe_consider(skc12,x1)
| ~ present(skc12,x1)
| ~ event(skc12,x1)
| ~ vincent_forename(skc12,x2)
| ~ jules_forename(skc12,x3)
| ~ agent(skc12,skc13,v)
| ~ agent(x,y,z)
| ~ of(skc12,w,z)
| ~ theme(skc12,x1,x)
| ~ of(skc12,x2,skc10)
| ~ agent(skc12,x1,skc10)
| ~ of(skc12,x3,skc10) ),
inference(mrr,[status(thm)],[1500,12]),
[iquote('0:MRR:1500.2,12.0')] ).
cnf(1631,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,skc10)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ man(skc12,x)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,y)
| ~ present(skc12,y)
| ~ event(skc12,y)
| ~ vincent_forename(skc12,z)
| ~ jules_forename(skc12,x1)
| ~ agent(v,w,x)
| ~ of(skc12,u,x)
| ~ theme(skc12,y,v)
| ~ of(skc12,z,skc10)
| ~ agent(skc12,y,skc10)
| ~ of(skc12,x1,skc10) ),
inference(mrr,[status(thm)],[1630,12]),
[iquote('0:MRR:1630.2,12.0')] ).
cnf(630,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ accessible_world(skc12,w)
| ~ proposition(skc12,w)
| ~ event(skc12,x)
| ~ present(skc12,x)
| ~ think_believe_consider(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ man(skc12,z)
| ~ jules_forename(skc12,x1)
| ~ smoke(x2,x3)
| ~ present(x2,x3)
| ~ man(skc12,x4)
| ~ proposition(skc12,x2)
| ~ accessible_world(skc12,x2)
| ~ think_believe_consider(skc12,x5)
| ~ present(skc12,x5)
| ~ event(skc12,x5)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x6)
| ~ man(skc12,v)
| ~ jules_forename(skc12,x7)
| ~ theme(skc12,x,w)
| ~ of(skc12,y,z)
| ~ agent(skc12,x,z)
| ~ agent(x2,x3,x4)
| ~ of(skc12,x1,x4)
| ~ theme(skc12,x5,x2)
| ~ of(skc12,x6,v)
| ~ agent(skc12,x5,v)
| ~ of(skc12,x7,v)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[141,96]),
[iquote('0:Res:141.1,96.30')] ).
cnf(1506,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ man(u,y)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ vincent_forename(u,x1)
| ~ jules_forename(u,x2)
| ~ agent(u,skc13,skc10)
| ~ agent(w,x,y)
| ~ of(u,v,y)
| ~ theme(u,z,w)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10) ),
inference(mrr,[status(thm)],[1505,151]),
[iquote('0:MRR:1505.4,151.1')] ).
cnf(1537,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ jules_forename(u,w)
| ~ smoke(v,skf2(x))
| ~ present(v,skf2(x))
| ~ man(u,x)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,y)
| ~ present(u,y)
| ~ event(u,y)
| ~ vincent_forename(u,z)
| ~ jules_forename(u,x1)
| ~ of(u,w,x)
| ~ theme(u,y,v)
| ~ of(u,z,skc10)
| ~ agent(u,y,skc10)
| ~ of(u,x1,skc10) ),
inference(mrr,[status(thm)],[1526,71]),
[iquote('0:MRR:1526.1,71.2')] ).
cnf(1614,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ smoke(v,skc13)
| ~ present(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ jules_forename(u,y)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(obv,[status(thm),theory(equality)],[1612]),
[iquote('0:Obv:1612.1')] ).
cnf(917,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ event(skc12,w)
| ~ present(skc12,w)
| ~ think_believe_consider(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ man(skc12,y)
| ~ jules_forename(skc12,z)
| ~ smoke(x1,x2)
| ~ present(x1,x2)
| ~ man(skc12,x3)
| ~ proposition(skc12,x1)
| ~ accessible_world(skc12,x1)
| ~ think_believe_consider(skc12,x4)
| ~ present(skc12,x4)
| ~ event(skc12,x4)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x5)
| ~ man(skc12,v)
| ~ jules_forename(skc12,x6)
| ~ theme(skc12,w,skc12)
| ~ of(skc12,x,y)
| ~ agent(skc12,w,y)
| ~ agent(x1,x2,x3)
| ~ of(skc12,z,x3)
| ~ theme(skc12,x4,x1)
| ~ of(skc12,x5,v)
| ~ agent(skc12,x4,v)
| ~ of(skc12,x6,v) ),
inference(res,[status(thm),theory(equality)],[141,586]),
[iquote('0:Res:141.1,586.30')] ).
cnf(1616,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc15)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,u)
| ~ smoke(v,skc13)
| ~ present(v,skc13)
| ~ man(skc12,skc15)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ jules_forename(skc12,y)
| ~ theme(skc12,w,v)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10) ),
inference(mrr,[status(thm)],[1615,12]),
[iquote('0:MRR:1615.2,12.0')] ).
cnf(1532,plain,
( ~ actual_world(u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,w)
| ~ smoke(v,skc13)
| ~ present(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ vincent_forename(u,y)
| ~ jules_forename(u,z)
| ~ of(u,w,skc15)
| ~ theme(u,x,v)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10) ),
inference(obv,[status(thm),theory(equality)],[1523]),
[iquote('0:Obv:1523.4')] ).
cnf(1601,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc15)
| ~ accessible_world(skc8,v)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,u)
| ~ smoke(v,skc13)
| ~ man(skc12,skc15)
| ~ proposition(skc12,v)
| ~ accessible_world(skc12,v)
| ~ think_believe_consider(skc12,w)
| ~ present(skc12,w)
| ~ event(skc12,w)
| ~ vincent_forename(skc12,x)
| ~ jules_forename(skc12,y)
| ~ theme(skc12,w,v)
| ~ of(skc12,x,skc10)
| ~ agent(skc12,w,skc10)
| ~ of(skc12,y,skc10) ),
inference(mrr,[status(thm)],[1598,12]),
[iquote('0:MRR:1598.3,12.0')] ).
cnf(901,plain,
( ~ actual_world(skc12)
| ~ be(skc8,u,v,v)
| ~ accessible_world(skc12,w)
| ~ proposition(skc12,w)
| ~ event(skc12,x)
| ~ present(skc12,x)
| ~ think_believe_consider(skc12,x)
| ~ vincent_forename(skc12,y)
| ~ man(skc12,z)
| ~ jules_forename(skc12,x1)
| ~ man(skc12,x2)
| ~ think_believe_consider(skc12,x3)
| ~ present(skc12,x3)
| ~ event(skc12,x3)
| ~ state(skc12,u)
| ~ vincent_forename(skc12,x4)
| ~ man(skc12,v)
| ~ jules_forename(skc12,x5)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(skc12,x,w)
| ~ of(skc12,y,z)
| ~ agent(skc12,x,z)
| ~ of(skc12,x1,x2)
| ~ of(skc12,x4,v)
| ~ agent(skc12,x3,v)
| ~ of(skc12,x5,v)
| ~ theme(skc12,x3,skc8)
| ~ agent(skc8,skc13,x2)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[141,182]),
[iquote('0:Res:141.1,182.29')] ).
cnf(1600,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,v)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ jules_forename(u,y)
| ~ theme(u,w,v)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(obv,[status(thm),theory(equality)],[1597]),
[iquote('0:Obv:1597.1')] ).
cnf(1531,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,v)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,w)
| ~ smoke(v,skc13)
| ~ man(u,skc15)
| ~ proposition(u,v)
| ~ accessible_world(u,v)
| ~ think_believe_consider(u,x)
| ~ present(u,x)
| ~ event(u,x)
| ~ vincent_forename(u,y)
| ~ jules_forename(u,z)
| ~ of(u,w,skc15)
| ~ theme(u,x,v)
| ~ of(u,y,skc10)
| ~ agent(u,x,skc10)
| ~ of(u,z,skc10) ),
inference(mrr,[status(thm)],[1530,177]),
[iquote('0:MRR:1530.6,177.1')] ).
cnf(1585,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc15)
| ~ accessible_world(skc12,skc12)
| ~ jules_forename(skc12,u)
| ~ smoke(skc8,skc13)
| ~ man(skc12,skc15)
| ~ proposition(skc12,skc8)
| ~ accessible_world(skc12,skc8)
| ~ think_believe_consider(skc12,v)
| ~ present(skc12,v)
| ~ event(skc12,v)
| ~ vincent_forename(skc12,w)
| ~ jules_forename(skc12,x)
| ~ theme(skc12,v,skc8)
| ~ of(skc12,w,skc10)
| ~ agent(skc12,v,skc10)
| ~ of(skc12,x,skc10) ),
inference(mrr,[status(thm)],[1582,12]),
[iquote('0:MRR:1582.2,12.0')] ).
cnf(1197,plain,
( ~ actual_world(u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ man(u,z)
| ~ think_believe_consider(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ state(u,x2)
| ~ vincent_forename(u,x3)
| ~ man(u,x4)
| ~ jules_forename(u,x5)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ of(u,y,z)
| ~ of(u,x3,x4)
| ~ agent(u,x1,x4)
| ~ of(u,x5,x4)
| ~ theme(u,x1,skc8)
| ~ agent(skc8,skc13,z)
| ~ be(u,x2,x4,x4) ),
inference(mrr,[status(thm)],[1194,182,224,228]),
[iquote('0:MRR:1194.1,1194.18,1194.19,182.30,224.0,228.0')] ).
cnf(1584,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,skc14)
| ~ smoke(skc8,skc13)
| ~ man(u,skc15)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ jules_forename(u,x)
| ~ theme(u,v,skc8)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10) ),
inference(obv,[status(thm),theory(equality)],[1581]),
[iquote('0:Obv:1581.1')] ).
cnf(1529,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ jules_forename(u,v)
| ~ smoke(skc8,skc13)
| ~ man(u,skc15)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ think_believe_consider(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ vincent_forename(u,x)
| ~ jules_forename(u,y)
| ~ of(u,v,skc15)
| ~ theme(u,w,skc8)
| ~ of(u,x,skc10)
| ~ agent(u,w,skc10)
| ~ of(u,y,skc10) ),
inference(mrr,[status(thm)],[1528,6]),
[iquote('0:MRR:1528.5,6.0')] ).
cnf(1564,plain,
( ~ actual_world(skc12)
| ~ theme(skc8,u,skc12)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,u)
| ~ present(skc12,u)
| ~ event(skc12,u)
| ~ vincent_forename(skc12,v)
| ~ jules_forename(skc12,w)
| ~ of(skc12,v,skc10)
| ~ agent(skc12,u,skc10)
| ~ of(skc12,w,skc10) ),
inference(mrr,[status(thm)],[1561,12]),
[iquote('0:MRR:1561.2,12.0')] ).
cnf(1570,plain,
( ~ actual_world(skc12)
| ~ of(skc8,u,skc10)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,u)
| ~ jules_forename(skc12,v)
| ~ agent(skc12,skc13,skc10)
| ~ of(skc12,v,skc10) ),
inference(mrr,[status(thm)],[1568,12]),
[iquote('0:MRR:1568.2,12.0')] ).
cnf(597,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ smoke(x1,x2)
| ~ present(x1,x2)
| ~ man(u,x3)
| ~ proposition(u,x1)
| ~ accessible_world(u,x1)
| ~ think_believe_consider(u,x4)
| ~ present(u,x4)
| ~ event(u,x4)
| ~ vincent_forename(u,x5)
| ~ jules_forename(u,x6)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ agent(x1,x2,x3)
| ~ of(u,z,x3)
| ~ theme(u,x4,x1)
| ~ of(u,x5,skc10)
| ~ agent(u,x4,skc10)
| ~ of(u,x6,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[596,146,151]),
[iquote('0:MRR:596.18,596.20,146.1,151.1')] ).
cnf(1572,plain,
( ~ actual_world(skc12)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc12,skc15)
| ~ accessible_world(skc12,skc12)
| ~ vincent_forename(skc12,skc11)
| ~ jules_forename(skc12,u)
| ~ of(skc12,u,skc10) ),
inference(mrr,[status(thm)],[1571,12]),
[iquote('0:MRR:1571.2,12.0')] ).
cnf(1569,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,skc11)
| ~ jules_forename(u,v)
| ~ agent(u,skc13,skc10)
| ~ of(u,v,skc10) ),
inference(obv,[status(thm),theory(equality)],[1567]),
[iquote('0:Obv:1567.1')] ).
cnf(1563,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ jules_forename(u,w)
| ~ of(u,v,skc10)
| ~ agent(u,skc13,skc10)
| ~ of(u,w,skc10) ),
inference(mrr,[status(thm)],[1562,171,177,185]),
[iquote('0:MRR:1562.4,1562.5,1562.6,171.1,177.1,185.1')] ).
cnf(1549,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ man(u,skc15)
| ~ accessible_world(u,skc12)
| ~ think_believe_consider(u,v)
| ~ present(u,v)
| ~ event(u,v)
| ~ vincent_forename(u,w)
| ~ jules_forename(u,x)
| ~ theme(u,v,skc12)
| ~ of(u,w,skc10)
| ~ agent(u,v,skc10)
| ~ of(u,x,skc10) ),
inference(mrr,[status(thm)],[1548,165,151]),
[iquote('0:MRR:1548.3,1548.4,165.1,151.1')] ).
cnf(904,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ man(u,x1)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ vincent_forename(u,x3)
| ~ jules_forename(u,x4)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ of(u,z,x1)
| ~ of(u,x3,skc10)
| ~ agent(u,x2,skc10)
| ~ of(u,x4,skc10)
| ~ theme(u,x2,skc8)
| ~ agent(skc8,skc13,x1)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[900,146,151]),
[iquote('0:MRR:900.14,900.16,146.1,151.1')] ).
cnf(1504,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ man(u,skc15)
| ~ jules_forename(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ man(u,y)
| ~ proposition(u,w)
| ~ accessible_world(u,w)
| ~ think_believe_consider(u,z)
| ~ present(u,z)
| ~ event(u,z)
| ~ vincent_forename(u,x1)
| ~ jules_forename(u,x2)
| ~ agent(w,x,y)
| ~ of(u,v,y)
| ~ theme(u,z,w)
| ~ of(u,x1,skc10)
| ~ agent(u,z,skc10)
| ~ of(u,x2,skc10) ),
inference(mrr,[status(thm)],[1503,191,506]),
[iquote('0:MRR:1503.3,1503.16,191.1,506.1')] ).
cnf(1519,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(skc8,skc8)
| ~ jules_forename(skc8,v)
| ~ smoke(u,skf2(w))
| ~ present(u,skf2(w))
| ~ man(skc8,w)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(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) ),
inference(mrr,[status(thm)],[1515,121]),
[iquote('0:MRR:1515.0,121.1')] ).
cnf(1502,plain,
( ~ accessible_world(skc8,skc8)
| ~ jules_forename(skc8,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ man(skc8,x)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(v,w,x)
| ~ of(skc8,u,x)
| ~ theme(skc8,y,v)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10) ),
inference(mrr,[status(thm)],[1501,12,191,2,506]),
[iquote('0:MRR:1501.1,1501.2,1501.3,1501.15,12.0,191.1,2.0,506.1')] ).
cnf(957,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x1)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ theme(skc8,w,skc12)
| ~ be(skc8,x3,x5,x5) ),
inference(mrr,[status(thm)],[954,207,224,228]),
[iquote('0:MRR:954.0,954.19,954.20,207.28,224.0,228.0')] ).
cnf(1473,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ vincent_forename(u,v)
| ~ man(u,w)
| ~ jules_forename(u,x)
| ~ smoke(y,z)
| ~ present(y,z)
| ~ man(u,x1)
| ~ proposition(u,y)
| ~ accessible_world(u,y)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ vincent_forename(u,x3)
| ~ jules_forename(u,x4)
| ~ of(u,v,w)
| ~ agent(u,skc13,w)
| ~ agent(y,z,x1)
| ~ of(u,x,x1)
| ~ theme(u,x2,y)
| ~ of(u,x3,skc10)
| ~ agent(u,x2,skc10)
| ~ of(u,x4,skc10) ),
inference(mrr,[status(thm)],[1472,185,177,171]),
[iquote('0:MRR:1472.3,1472.4,1472.5,185.1,177.1,171.1')] ).
cnf(1487,plain,
( ~ smoke(u,skc13)
| ~ vincent_forename(skc8,v)
| ~ man(skc8,w)
| ~ jules_forename(skc8,x)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ jules_forename(skc8,z)
| ~ of(skc8,v,w)
| ~ agent(skc8,skc13,w)
| ~ of(skc8,x,skc15)
| ~ theme(skc8,y,u)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,z,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1484,5,6,7]),
[iquote('0:MRR:1484.1,1484.2,1484.3,5.0,6.0,7.0')] ).
cnf(1460,plain,
( ~ smoke(u,skc13)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ theme(skc8,v,skc12)
| ~ of(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ of(skc8,y,skc15)
| ~ theme(skc8,z,u)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x1,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1459,177,2]),
[iquote('0:MRR:1459.1,1459.8,177.1,2.0')] ).
cnf(1467,plain,
( ~ vincent_forename(skc8,u)
| ~ man(skc8,v)
| ~ jules_forename(skc8,w)
| ~ man(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ jules_forename(skc8,z)
| ~ of(skc8,u,v)
| ~ agent(skc8,skc13,v)
| ~ of(skc8,w,x)
| ~ theme(skc8,y,skc12)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,z,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1464,5,6,7]),
[iquote('0:MRR:1464.0,1464.1,1464.2,5.0,6.0,7.0')] ).
cnf(920,plain,
( ~ actual_world(u)
| ~ accessible_world(skc8,u)
| ~ accessible_world(u,skc12)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ smoke(z,x1)
| ~ present(z,x1)
| ~ man(u,x2)
| ~ proposition(u,z)
| ~ accessible_world(u,z)
| ~ think_believe_consider(u,x3)
| ~ present(u,x3)
| ~ event(u,x3)
| ~ vincent_forename(u,x4)
| ~ jules_forename(u,x5)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ agent(z,x1,x2)
| ~ of(u,y,x2)
| ~ theme(u,x3,z)
| ~ of(u,x4,skc10)
| ~ agent(u,x3,skc10)
| ~ of(u,x5,skc10) ),
inference(mrr,[status(thm)],[916,101,146,151]),
[iquote('0:MRR:916.3,916.18,916.20,101.1,146.1,151.1')] ).
cnf(1462,plain,
( ~ event(skc8,u)
| ~ present(skc8,u)
| ~ think_believe_consider(skc8,u)
| ~ vincent_forename(skc8,v)
| ~ man(skc8,w)
| ~ jules_forename(skc8,x)
| ~ man(skc8,y)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ theme(skc8,u,skc12)
| ~ of(skc8,v,w)
| ~ agent(skc8,u,w)
| ~ of(skc8,x,y)
| ~ theme(skc8,z,skc12)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x1,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1455,71,224,228,13,12]),
[iquote('0:MRR:1455.0,1455.1,1455.2,1455.10,1455.11,71.2,224.0,228.0,13.0,12.0')] ).
cnf(1398,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,x1)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ agent(skc8,x2,skc10)
| ~ of(skc8,x3,skc10)
| ~ of(skc8,skc14,skc10) ),
inference(mrr,[status(thm)],[1395,11,10]),
[iquote('0:MRR:1395.14,1395.15,11.0,10.0')] ).
cnf(1394,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ of(skc8,z,v)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10) ),
inference(mrr,[status(thm)],[1387,121]),
[iquote('0:MRR:1387.0,121.1')] ).
cnf(1440,plain,
( ~ smoke(u,skc13)
| ~ jules_forename(skc8,skc14)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,v)
| ~ present(skc8,v)
| ~ event(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,skc10)
| ~ agent(skc8,v,skc10) ),
inference(res,[status(thm),theory(equality)],[14,1439]),
[iquote('0:Res:14.0,1439.8')] ).
cnf(1140,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,z)
| ~ theme(skc8,w,skc12)
| ~ agent(skc8,w,x)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ of(skc8,skc14,x)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[1136,197,224,228,12,13]),
[iquote('0:MRR:1136.0,1136.3,1136.4,1136.5,1136.6,197.29,224.0,228.0,12.0,13.0')] ).
cnf(1439,plain,
( ~ smoke(u,skc13)
| ~ jules_forename(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,w)
| ~ present(skc8,w)
| ~ event(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ of(skc8,v,skc15)
| ~ theme(skc8,w,u)
| ~ of(skc8,x,skc10)
| ~ agent(skc8,w,skc10) ),
inference(mrr,[status(thm)],[1434,4,2,15]),
[iquote('0:MRR:1434.1,1434.2,1434.10,4.0,2.0,15.0')] ).
cnf(1421,plain,
( ~ vincent_forename(skc8,u)
| ~ of(skc8,u,skc10)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1418,7,6,5]),
[iquote('0:MRR:1418.0,1418.1,1418.2,7.0,6.0,5.0')] ).
cnf(1120,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,z)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ of(skc8,skc11,z)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[1116,201,224,228,12,13]),
[iquote('0:MRR:1116.0,1116.3,1116.4,1116.5,1116.6,201.29,224.0,228.0,12.0,13.0')] ).
cnf(1417,plain,
( ~ think_believe_consider(skc8,u)
| ~ present(skc8,u)
| ~ event(skc8,u)
| ~ vincent_forename(skc8,v)
| ~ theme(skc8,u,skc12)
| ~ of(skc8,v,skc10)
| ~ agent(skc8,u,skc10) ),
inference(mrr,[status(thm)],[1410,8,10]),
[iquote('0:MRR:1410.0,1410.1,8.0,10.0')] ).
cnf(1105,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x1)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ 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)],[1101,198,224,228,12,13]),
[iquote('0:MRR:1101.0,1101.3,1101.4,1101.5,1101.6,198.29,224.0,228.0,12.0,13.0')] ).
cnf(1382,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ agent(u,v,x1)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x2,skc10) ),
inference(mrr,[status(thm)],[1379,11,10,17]),
[iquote('0:MRR:1379.14,1379.16,1379.25,11.0,10.0,17.0')] ).
cnf(1077,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ agent(u,v,x1)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ 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)],[1073,202,224,228,12,13]),
[iquote('0:MRR:1073.0,1073.3,1073.4,1073.5,1073.6,202.29,224.0,228.0,12.0,13.0')] ).
cnf(1375,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ theme(skc8,v,skc12)
| ~ of(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ theme(skc8,y,u)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10) ),
inference(res,[status(thm),theory(equality)],[507,1368]),
[iquote('0:Res:507.2,1368.14')] ).
cnf(1368,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ agent(u,v,skc10)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10) ),
inference(mrr,[status(thm)],[1367,11,10]),
[iquote('0:MRR:1367.12,1367.14,11.0,10.0')] ).
cnf(1060,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x1)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ 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)],[1056,206,224,228,12,13]),
[iquote('0:MRR:1056.0,1056.3,1056.4,1056.5,1056.6,206.29,224.0,228.0,12.0,13.0')] ).
cnf(1042,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,skc10)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ of(skc8,z,skc10)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[1038,204,224,228,12,13]),
[iquote('0:MRR:1038.0,1038.3,1038.4,1038.5,1038.6,204.29,224.0,228.0,12.0,13.0')] ).
cnf(1337,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,y)
| ~ of(skc8,z,v)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ of(skc8,skc14,y)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[1334,121]),
[iquote('0:MRR:1334.0,121.1')] ).
cnf(1306,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ of(skc8,skc11,v)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[1301,121]),
[iquote('0:MRR:1301.0,121.1')] ).
cnf(1279,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,v)
| ~ theme(skc8,x2,u)
| ~ agent(skc8,x2,skc10)
| ~ of(skc8,x3,skc10)
| ~ of(skc8,skc14,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[1272,121]),
[iquote('0:MRR:1272.0,121.1')] ).
cnf(1233,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,v)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x2,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[1226,121]),
[iquote('0:MRR:1226.0,121.1')] ).
cnf(1132,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(skc10))
| ~ present(u,skf2(skc10))
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,w,v)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[507,788]),
[iquote('0:Res:507.2,788.16')] ).
cnf(851,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x1)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,y)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x2,skc10)
| ~ of(skc8,x4,skc10)
| ~ of(skc8,skc14,y)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[849,11,10]),
[iquote('0:MRR:849.15,849.17,11.0,10.0')] ).
cnf(1276,plain,
( ~ smoke(u,skc13)
| ~ accessible_world(skc8,v)
| ~ proposition(skc8,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,w,v)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ of(skc8,z,skc15)
| ~ theme(skc8,x1,u)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc14,skc10)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[1275,177,2]),
[iquote('0:MRR:1275.1,1275.10,177.1,2.0')] ).
cnf(841,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x1)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x2,skc10)
| ~ of(skc8,x4,skc10)
| ~ of(skc8,skc11,x1)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[839,11,10]),
[iquote('0:MRR:839.15,839.17,11.0,10.0')] ).
cnf(1278,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,z)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,skc12)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x2,skc10)
| ~ of(skc8,skc14,skc10)
| man(u,skf4(u)) ),
inference(mrr,[status(thm)],[1271,71,224,228,13,12]),
[iquote('0:MRR:1271.0,1271.1,1271.2,1271.12,1271.13,71.2,224.0,228.0,13.0,12.0')] ).
cnf(830,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ jules_forename(skc8,x4)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ agent(skc8,x3,skc10)
| ~ of(skc8,x4,skc10)
| ~ of(skc8,skc14,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[828,11,10]),
[iquote('0:MRR:828.16,828.17,11.0,10.0')] ).
cnf(819,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x4,skc10)
| ~ agent(skc8,x3,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[817,11,10,17]),
[iquote('0:MRR:817.16,817.18,817.27,11.0,10.0,17.0')] ).
cnf(98,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x4)
| ~ present(skc8,x4)
| ~ event(skc8,x4)
| ~ state(skc8,x5)
| ~ vincent_forename(skc8,x6)
| ~ man(skc8,x7)
| ~ jules_forename(skc8,x8)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ of(skc8,x2,x3)
| ~ theme(skc8,x4,u)
| ~ of(skc8,x6,x7)
| ~ agent(skc8,x4,x7)
| ~ of(skc8,x8,x7)
| ~ be(skc8,x5,x7,x7) ),
inference(res,[status(thm),theory(equality)],[1,97]),
[iquote('0:Res:1.0,97.0')] ).
cnf(1207,plain,
( ~ vincent_forename(skc8,skc11)
| ~ agent(skc8,skc13,skc10) ),
inference(mrr,[status(thm)],[1204,8]),
[iquote('0:MRR:1204.1,8.0')] ).
cnf(184,plain,
( ~ actual_world(u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ man(u,x1)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ state(u,x3)
| ~ vincent_forename(u,x4)
| ~ man(u,x5)
| ~ jules_forename(u,x6)
| ~ smoke(v,x7)
| ~ present(v,x7)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ of(u,z,x1)
| ~ of(u,x4,x5)
| ~ agent(u,x2,x5)
| ~ of(u,x6,x5)
| ~ theme(u,x2,skc8)
| ~ agent(v,x7,skf4(v))
| ~ agent(skc8,skc13,x1)
| ~ be(u,x3,x5,x5) ),
inference(res,[status(thm),theory(equality)],[6,97]),
[iquote('0:Res:6.0,97.21')] ).
cnf(881,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,x1)
| ~ theme(skc8,w,skc12)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ 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)],[877,200,224,228,12,13]),
[iquote('0:MRR:877.0,877.3,877.4,877.5,877.6,200.27,224.0,228.0,12.0,13.0')] ).
cnf(183,plain,
( ~ actual_world(u)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ smoke(z,x1)
| ~ present(z,x1)
| ~ man(u,x2)
| ~ proposition(u,z)
| ~ accessible_world(u,z)
| ~ think_believe_consider(u,x3)
| ~ present(u,x3)
| ~ event(u,x3)
| ~ state(u,x4)
| ~ vincent_forename(u,x5)
| ~ man(u,x6)
| ~ jules_forename(u,x7)
| ~ accessible_world(u,skc8)
| ~ proposition(u,skc8)
| ~ smoke(skc8,skc13)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ agent(z,x1,x2)
| ~ of(u,y,x2)
| ~ theme(u,x3,z)
| ~ of(u,x5,x6)
| ~ agent(u,x3,x6)
| ~ of(u,x7,x6)
| ~ theme(u,v,skc8)
| ~ agent(skc8,skc13,skf4(skc8))
| ~ be(u,x4,x6,x6) ),
inference(res,[status(thm),theory(equality)],[6,97]),
[iquote('0:Res:6.0,97.2')] ).
cnf(209,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x2)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ agent(skc8,y,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ of(skc8,skc14,z)
| ~ be(skc8,x4,x6,x6) ),
inference(mrr,[status(thm)],[196,1]),
[iquote('0:MRR:196.0,1.0')] ).
cnf(1130,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,v)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[1127,121]),
[iquote('0:MRR:1127.0,121.1')] ).
cnf(788,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,skc10)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[787,11,10]),
[iquote('0:MRR:787.14,787.16,11.0,10.0')] ).
cnf(774,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,z)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,x,skc10)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[773,11,10]),
[iquote('0:MRR:773.14,773.16,11.0,10.0')] ).
cnf(1093,plain,
( ~ accessible_world(skc12,u)
| ~ smoke(u,skf2(v))
| ~ present(u,skf2(v))
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,v)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,z)
| ~ present(skc8,z)
| ~ event(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ of(skc8,w,x)
| ~ of(skc8,y,v)
| ~ theme(skc8,z,u)
| ~ of(skc8,x1,skc10)
| ~ agent(skc8,z,skc10)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,skc13,x) ),
inference(mrr,[status(thm)],[1088,121]),
[iquote('0:MRR:1088.0,121.1')] ).
cnf(213,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x2)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ of(skc8,skc11,x2)
| ~ be(skc8,x4,x6,x6) ),
inference(mrr,[status(thm)],[169,1]),
[iquote('0:MRR:169.0,1.0')] ).
cnf(210,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x4)
| ~ present(skc8,x4)
| ~ event(skc8,x4)
| ~ state(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ of(skc8,x2,x3)
| ~ theme(skc8,x4,u)
| ~ agent(skc8,x4,x6)
| ~ of(skc8,x7,x6)
| ~ of(skc8,skc14,x6)
| ~ be(skc8,x5,x6,x6) ),
inference(mrr,[status(thm)],[195,1]),
[iquote('0:MRR:195.0,1.0')] ).
cnf(1083,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ vincent_forename(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(u,v,z)
| ~ of(skc8,w,x)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x2,skc10)
| ~ agent(skc8,x1,skc10)
| ~ of(skc8,x3,skc10)
| ~ agent(skc8,skc13,x) ),
inference(mrr,[status(thm)],[1080,11,10]),
[iquote('0:MRR:1080.11,1080.13,11.0,10.0')] ).
cnf(860,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ man(skc8,z)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x1)
| ~ present(skc8,x1)
| ~ event(skc8,x1)
| ~ state(skc8,x2)
| ~ vincent_forename(skc8,x3)
| ~ man(skc8,x4)
| ~ jules_forename(skc8,x5)
| ~ agent(u,v,z)
| ~ of(skc8,w,x)
| ~ of(skc8,y,z)
| ~ theme(skc8,x1,u)
| ~ of(skc8,x3,x4)
| ~ agent(skc8,x1,x4)
| ~ of(skc8,x5,x4)
| ~ agent(skc8,skc13,x)
| ~ be(skc8,x2,x4,x4) ),
inference(mrr,[status(thm)],[856,199,224,228,12,13,16]),
[iquote('0:MRR:856.0,856.3,856.4,856.5,856.6,856.27,199.27,224.0,228.0,12.0,13.0,16.0')] ).
cnf(1022,plain,
( ~ accessible_world(skc12,u)
| ~ jules_forename(skc8,v)
| ~ smoke(u,skf2(w))
| ~ present(u,skf2(w))
| ~ man(skc8,w)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(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)
| man(skc12,skf4(skc12)) ),
inference(mrr,[status(thm)],[1014,121]),
[iquote('0:MRR:1014.0,121.1')] ).
cnf(214,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x4)
| ~ present(skc8,x4)
| ~ event(skc8,x4)
| ~ state(skc8,x5)
| ~ vincent_forename(skc8,x6)
| ~ man(skc8,x7)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ of(skc8,x2,x3)
| ~ theme(skc8,x4,u)
| ~ of(skc8,x6,x7)
| ~ agent(skc8,x4,x7)
| ~ of(skc8,skc11,x7)
| ~ be(skc8,x5,x7,x7) ),
inference(mrr,[status(thm)],[168,1]),
[iquote('0:MRR:168.0,1.0')] ).
cnf(1072,plain,
( ~ man(skc12,skc10)
| ~ accessible_world(skc12,skc8)
| ~ think_believe_consider(skc8,skf2(skc10))
| ~ present(skc8,skf2(skc10))
| ~ event(skc8,skf2(skc10))
| ~ vincent_forename(skc8,skc11)
| ~ jules_forename(skc8,u)
| ~ of(skc8,u,skc10)
| ~ theme(skc8,skf2(skc10),skc12) ),
inference(res,[status(thm),theory(equality)],[507,1069]),
[iquote('0:Res:507.2,1069.5')] ).
cnf(1069,plain,
( ~ think_believe_consider(skc8,u)
| ~ present(skc8,u)
| ~ event(skc8,u)
| ~ vincent_forename(skc8,skc11)
| ~ jules_forename(skc8,v)
| ~ agent(skc8,u,skc10)
| ~ of(skc8,v,skc10)
| ~ theme(skc8,u,skc12) ),
inference(res,[status(thm),theory(equality)],[17,1068]),
[iquote('0:Res:17.0,1068.5')] ).
cnf(218,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x4)
| ~ present(skc8,x4)
| ~ event(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ of(skc8,x2,x3)
| ~ theme(skc8,x4,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x4,x6)
| ~ of(skc8,x7,x6)
| ~ be(skc8,skc9,x6,x6) ),
inference(mrr,[status(thm)],[150,1]),
[iquote('0:MRR:150.0,1.0')] ).
cnf(216,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,skc10)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ of(skc8,x2,skc10)
| ~ be(skc8,x4,x6,x6) ),
inference(mrr,[status(thm)],[158,1]),
[iquote('0:MRR:158.0,1.0')] ).
cnf(1004,plain,
( ~ jules_forename(skc8,u)
| ~ smoke(v,w)
| ~ present(v,w)
| ~ man(skc8,x)
| ~ proposition(skc8,v)
| ~ accessible_world(skc8,v)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ agent(v,w,x)
| ~ of(skc8,u,x)
| ~ theme(skc8,y,v)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ of(skc8,x1,skc10)
| man(skc12,skf4(skc12)) ),
inference(mrr,[status(thm)],[999,4,2,15]),
[iquote('0:MRR:999.0,999.1,999.13,4.0,2.0,15.0')] ).
cnf(215,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x2)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ of(skc8,z,skc10)
| ~ agent(skc8,y,skc10)
| ~ be(skc8,x4,x6,x6) ),
inference(mrr,[status(thm)],[159,1]),
[iquote('0:MRR:159.0,1.0')] ).
cnf(976,plain,
( ~ agent(skc8,u,skf4(skc12))
| ~ smoke(skc12,u)
| ~ present(skc12,u)
| ~ jules_forename(skc8,v)
| ~ smoke(skc12,w)
| ~ present(skc12,w)
| ~ man(skc8,x)
| ~ think_believe_consider(skc8,y)
| ~ present(skc8,y)
| ~ event(skc8,y)
| ~ state(skc8,z)
| ~ vincent_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ jules_forename(skc8,x3)
| ~ agent(skc12,w,x)
| ~ of(skc8,v,x)
| ~ of(skc8,x1,x2)
| ~ agent(skc8,y,x2)
| ~ of(skc8,x3,x2)
| ~ theme(skc8,y,skc12)
| ~ be(skc8,z,x2,x2) ),
inference(mrr,[status(thm)],[975,12,13]),
[iquote('0:MRR:975.3,975.4,12.0,13.0')] ).
cnf(217,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x4)
| ~ present(skc8,x4)
| ~ event(skc8,x4)
| ~ state(skc8,x5)
| ~ vincent_forename(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ of(skc8,x2,x3)
| ~ theme(skc8,x4,u)
| ~ of(skc8,x6,skc10)
| ~ agent(skc8,x4,skc10)
| ~ of(skc8,x7,skc10)
| ~ be(skc8,x5,skc10,skc10) ),
inference(mrr,[status(thm)],[157,1]),
[iquote('0:MRR:157.0,1.0')] ).
cnf(978,plain,
( ~ man(skc12,skf4(skc12))
| ~ jules_forename(skc8,u)
| ~ smoke(skc12,v)
| ~ present(skc12,v)
| ~ man(skc8,w)
| ~ think_believe_consider(skc8,x)
| ~ present(skc8,x)
| ~ event(skc8,x)
| ~ state(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ agent(skc12,v,w)
| ~ of(skc8,u,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,x,x1)
| ~ of(skc8,x2,x1)
| ~ theme(skc8,x,skc12)
| ~ be(skc8,y,x1,x1) ),
inference(mrr,[status(thm)],[977,224,228,12,13]),
[iquote('0:MRR:977.1,977.2,977.3,977.4,224.0,228.0,12.0,13.0')] ).
cnf(983,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,604]),
[iquote('0:Res:16.0,604.0')] ).
cnf(604,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)],[139,93]),
[iquote('0:Res:139.1,93.4')] ).
cnf(833,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)],[831,93]),
[iquote('0:Res:831.1,93.4')] ).
cnf(220,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,w)
| ~ present(skc8,w)
| ~ think_believe_consider(skc8,w)
| ~ vincent_forename(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ smoke(skc12,x1)
| ~ present(skc12,x1)
| ~ man(skc8,x2)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,skf4(u))
| ~ theme(skc8,w,u)
| ~ of(skc8,x,y)
| ~ agent(skc8,w,y)
| ~ agent(skc12,x1,x2)
| ~ of(skc8,z,x2)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ theme(skc8,x3,skc12)
| ~ be(skc8,x4,x6,x6) ),
inference(mrr,[status(thm)],[144,1,13]),
[iquote('0:MRR:144.0,144.16,1.0,13.0')] ).
cnf(968,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)],[967,12]),
[iquote('0:MRR:967.1,12.0')] ).
cnf(557,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)],[555,101,171]),
[iquote('0:MRR:555.1,555.3,101.1,171.1')] ).
cnf(948,plain,
( ~ forename(skc12,u)
| ~ forename(skc12,skc11)
| ~ entity(skc12,skc10)
| ~ of(skc12,u,skc10)
| equal(skc11,u) ),
inference(res,[status(thm),theory(equality)],[17,621]),
[iquote('0:Res:17.0,621.0')] ).
cnf(949,plain,
( ~ forename(skc12,u)
| ~ forename(skc12,skc14)
| ~ entity(skc12,skc15)
| ~ of(skc12,u,skc15)
| equal(skc14,u) ),
inference(res,[status(thm),theory(equality)],[14,621]),
[iquote('0:Res:14.0,621.0')] ).
cnf(621,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)],[138,92]),
[iquote('0:Res:138.1,92.3')] ).
cnf(854,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)],[848,92]),
[iquote('0:Res:848.1,92.3')] ).
cnf(846,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)],[843,92]),
[iquote('0:Res:843.1,92.3')] ).
cnf(933,plain,
( ~ of(skc8,u,skc15)
| ~ forename(skc12,u)
| ~ forename(skc12,skc14)
| ~ entity(skc12,skc15)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[932,12]),
[iquote('0:MRR:932.1,12.0')] ).
cnf(99,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,x7,x6)
| ~ be(skc8,x4,x6,x6)
| man(w,skf4(w)) ),
inference(res,[status(thm),theory(equality)],[1,96]),
[iquote('0:Res:1.0,96.0')] ).
cnf(535,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)],[519,92]),
[iquote('0:Res:519.1,92.3')] ).
cnf(925,plain,
( ~ of(skc8,u,skc10)
| ~ forename(skc12,u)
| ~ entity(skc12,skc10)
| equal(skc11,u) ),
inference(mrr,[status(thm)],[924,12]),
[iquote('0:MRR:924.1,12.0')] ).
cnf(538,plain,
( ~ accessible_world(skc8,u)
| ~ forename(u,v)
| ~ entity(u,skc10)
| ~ of(u,v,skc10)
| equal(skc11,v) ),
inference(mrr,[status(thm)],[534,160]),
[iquote('0:MRR:534.2,160.1')] ).
cnf(912,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skf2(skc15),skc15) ),
inference(res,[status(thm),theory(equality)],[2,908]),
[iquote('0:Res:2.0,908.0')] ).
cnf(586,plain,
( ~ actual_world(u)
| ~ accessible_world(u,skc12)
| ~ proposition(u,skc12)
| ~ event(u,v)
| ~ present(u,v)
| ~ think_believe_consider(u,v)
| ~ vincent_forename(u,w)
| ~ man(u,x)
| ~ jules_forename(u,y)
| ~ smoke(z,x1)
| ~ present(z,x1)
| ~ man(u,x2)
| ~ proposition(u,z)
| ~ accessible_world(u,z)
| ~ think_believe_consider(u,x3)
| ~ present(u,x3)
| ~ event(u,x3)
| ~ state(u,x4)
| ~ vincent_forename(u,x5)
| ~ man(u,x6)
| ~ jules_forename(u,x7)
| ~ theme(u,v,skc12)
| ~ of(u,w,x)
| ~ agent(u,v,x)
| ~ agent(z,x1,x2)
| ~ of(u,y,x2)
| ~ theme(u,x3,z)
| ~ of(u,x5,x6)
| ~ agent(u,x3,x6)
| ~ of(u,x7,x6)
| ~ be(u,x4,x6,x6) ),
inference(mrr,[status(thm)],[585,96,224,228]),
[iquote('0:MRR:585.1,585.22,585.23,96.31,224.0,228.0')] ).
cnf(908,plain,
( ~ man(skc8,u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(v,w)
| agent(w,skf2(u),u) ),
inference(res,[status(thm),theory(equality)],[121,642]),
[iquote('0:Res:121.1,642.0')] ).
cnf(910,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skf2(skc10),skc10) ),
inference(mrr,[status(thm)],[909,12]),
[iquote('0:MRR:909.0,12.0')] ).
cnf(642,plain,
( ~ man(skc12,u)
| ~ accessible_world(skc12,v)
| ~ accessible_world(v,w)
| agent(w,skf2(u),u) ),
inference(res,[status(thm),theory(equality)],[507,90]),
[iquote('0:Res:507.2,90.1')] ).
cnf(697,plain,
( ~ proposition(skc8,u)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,v)
| equal(skc12,u) ),
inference(mrr,[status(thm)],[696,13,7]),
[iquote('0:MRR:696.0,696.2,13.0,7.0')] ).
cnf(182,plain,
( ~ actual_world(u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ man(u,x1)
| ~ think_believe_consider(u,x2)
| ~ present(u,x2)
| ~ event(u,x2)
| ~ state(u,x3)
| ~ vincent_forename(u,x4)
| ~ man(u,x5)
| ~ jules_forename(u,x6)
| ~ proposition(u,skc8)
| ~ accessible_world(u,skc8)
| ~ smoke(skc8,skc13)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ of(u,z,x1)
| ~ of(u,x4,x5)
| ~ agent(u,x2,x5)
| ~ of(u,x6,x5)
| ~ theme(u,x2,skc8)
| ~ agent(skc8,skc13,x1)
| ~ be(u,x3,x5,x5)
| man(v,skf4(v)) ),
inference(res,[status(thm),theory(equality)],[6,96]),
[iquote('0:Res:6.0,96.18')] ).
cnf(629,plain,
( ~ be(skc8,u,v,w)
| ~ accessible_world(skc12,x)
| be(x,u,v,w) ),
inference(res,[status(thm),theory(equality)],[141,91]),
[iquote('0:Res:141.1,91.1')] ).
cnf(622,plain,
( ~ of(skc8,u,v)
| ~ accessible_world(skc12,w)
| of(w,u,v) ),
inference(res,[status(thm),theory(equality)],[138,88]),
[iquote('0:Res:138.1,88.1')] ).
cnf(611,plain,
( ~ agent(skc8,u,v)
| ~ accessible_world(skc12,w)
| agent(w,u,v) ),
inference(res,[status(thm),theory(equality)],[140,90]),
[iquote('0:Res:140.1,90.1')] ).
cnf(603,plain,
( ~ theme(skc8,u,v)
| ~ accessible_world(skc12,w)
| theme(w,u,v) ),
inference(res,[status(thm),theory(equality)],[139,89]),
[iquote('0:Res:139.1,89.1')] ).
cnf(212,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ smoke(w,x)
| ~ present(w,x)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,y)
| ~ present(skc8,y)
| ~ think_believe_consider(skc8,y)
| ~ vincent_forename(skc8,z)
| ~ man(skc8,x1)
| ~ jules_forename(skc8,x2)
| ~ man(skc8,x3)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ jules_forename(skc8,x7)
| ~ agent(u,v,x3)
| ~ agent(w,x,skf4(w))
| ~ theme(skc8,y,w)
| ~ of(skc8,z,x1)
| ~ agent(skc8,y,x1)
| ~ of(skc8,x2,x3)
| ~ of(skc8,x5,x6)
| ~ of(skc8,x7,x6)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,x6)
| ~ be(skc8,x4,x6,x6) ),
inference(mrr,[status(thm)],[189,1,6,7]),
[iquote('0:MRR:189.0,189.13,189.14,1.0,6.0,7.0')] ).
cnf(873,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| be(v,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[861,91]),
[iquote('0:Res:861.1,91.1')] ).
cnf(861,plain,
( ~ accessible_world(skc12,u)
| be(u,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[12,595]),
[iquote('0:Res:12.0,595.0')] ).
cnf(595,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| be(v,skc9,skc10,skc10) ),
inference(res,[status(thm),theory(equality)],[525,91]),
[iquote('0:Res:525.1,91.1')] ).
cnf(855,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| of(v,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[848,88]),
[iquote('0:Res:848.1,88.1')] ).
cnf(847,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| of(v,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[843,88]),
[iquote('0:Res:843.1,88.1')] ).
cnf(842,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| agent(v,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[838,90]),
[iquote('0:Res:838.1,90.1')] ).
cnf(832,plain,
( ~ accessible_world(skc12,u)
| ~ accessible_world(u,v)
| theme(v,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[831,89]),
[iquote('0:Res:831.1,89.1')] ).
cnf(848,plain,
( ~ accessible_world(skc12,u)
| of(u,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[12,531]),
[iquote('0:Res:12.0,531.0')] ).
cnf(197,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ man(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x1)
| ~ theme(skc8,x,w)
| ~ agent(skc8,x,y)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,skc14,y)
| ~ be(skc8,x3,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[194,1]),
[iquote('0:MRR:194.0,1.0')] ).
cnf(531,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| of(v,skc14,skc15) ),
inference(res,[status(thm),theory(equality)],[519,88]),
[iquote('0:Res:519.1,88.1')] ).
cnf(843,plain,
( ~ accessible_world(skc12,u)
| of(u,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[12,530]),
[iquote('0:Res:12.0,530.0')] ).
cnf(530,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| of(v,skc11,skc10) ),
inference(res,[status(thm),theory(equality)],[518,88]),
[iquote('0:Res:518.1,88.1')] ).
cnf(838,plain,
( ~ accessible_world(skc12,u)
| agent(u,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[12,520]),
[iquote('0:Res:12.0,520.0')] ).
cnf(201,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x1)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,skc11,x1)
| ~ be(skc8,x3,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[167,1]),
[iquote('0:MRR:167.0,1.0')] ).
cnf(520,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| agent(v,skc13,skc15) ),
inference(res,[status(thm),theory(equality)],[506,90]),
[iquote('0:Res:506.1,90.1')] ).
cnf(831,plain,
( ~ accessible_world(skc12,u)
| theme(u,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[12,512]),
[iquote('0:Res:12.0,512.0')] ).
cnf(512,plain,
( ~ accessible_world(skc8,u)
| ~ accessible_world(u,v)
| theme(v,skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[497,89]),
[iquote('0:Res:497.1,89.1')] ).
cnf(671,plain,
( ~ entity(skc8,skc15)
| ~ of(skc8,skc11,skc15)
| equal(skc14,skc11) ),
inference(mrr,[status(thm)],[668,3]),
[iquote('0:MRR:668.0,3.0')] ).
cnf(198,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ agent(skc8,x3,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,skc14,x5)
| ~ be(skc8,x4,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[193,1]),
[iquote('0:MRR:193.0,1.0')] ).
cnf(826,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc14) ),
inference(res,[status(thm),theory(equality)],[191,816]),
[iquote('0:Res:191.1,816.0')] ).
cnf(816,plain,
( ~ vincent_forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[20,810]),
[iquote('0:Res:20.1,810.0')] ).
cnf(815,plain,
( ~ jules_forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[19,810]),
[iquote('0:Res:19.1,810.0')] ).
cnf(814,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc11) ),
inference(res,[status(thm),theory(equality)],[160,810]),
[iquote('0:Res:160.1,810.0')] ).
cnf(202,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ state(skc8,x4)
| ~ vincent_forename(skc8,x5)
| ~ man(skc8,x6)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x5,x6)
| ~ agent(skc8,x3,x6)
| ~ of(skc8,skc11,x6)
| ~ be(skc8,x4,x6,x6)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[164,1]),
[iquote('0:MRR:164.0,1.0')] ).
cnf(810,plain,
( ~ forename(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[22,784]),
[iquote('0:Res:22.1,784.0')] ).
cnf(784,plain,
( ~ relname(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[21,752]),
[iquote('0:Res:21.1,752.0')] ).
cnf(806,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(u,skc9) ),
inference(res,[status(thm),theory(equality)],[146,783]),
[iquote('0:Res:146.1,783.1')] ).
cnf(783,plain,
( ~ proposition(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[41,752]),
[iquote('0:Res:41.1,752.0')] ).
cnf(206,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x3)
| ~ present(skc8,x3)
| ~ event(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ theme(skc8,x3,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x3,x5)
| ~ of(skc8,x6,x5)
| ~ be(skc8,skc9,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[149,1]),
[iquote('0:MRR:149.0,1.0')] ).
cnf(779,plain,
( ~ human_person(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[32,750]),
[iquote('0:Res:32.1,750.0')] ).
cnf(777,plain,
( ~ human_person(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[32,748]),
[iquote('0:Res:32.1,748.0')] ).
cnf(793,plain,
( ~ accessible_world(skc8,u)
| ~ general(u,skc10) ),
inference(res,[status(thm),theory(equality)],[151,754]),
[iquote('0:Res:151.1,754.0')] ).
cnf(754,plain,
( ~ man(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[33,725]),
[iquote('0:Res:33.1,725.0')] ).
cnf(204,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,skc10)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,x1,skc10)
| ~ be(skc8,x3,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[155,1]),
[iquote('0:MRR:155.0,1.0')] ).
cnf(752,plain,
( ~ relation(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[40,692]),
[iquote('0:Res:40.1,692.0')] ).
cnf(750,plain,
( ~ organism(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[31,624]),
[iquote('0:Res:31.1,624.0')] ).
cnf(748,plain,
( ~ organism(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[31,600]),
[iquote('0:Res:31.1,600.0')] ).
cnf(770,plain,
( ~ accessible_world(skc8,u)
| ~ state(u,skc10) ),
inference(res,[status(thm),theory(equality)],[151,737]),
[iquote('0:Res:151.1,737.0')] ).
cnf(203,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ jules_forename(skc8,z)
| ~ man(skc8,x1)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x1)
| ~ theme(skc8,x,w)
| ~ of(skc8,z,x1)
| ~ theme(skc8,x2,u)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ of(skc8,y,skc10)
| ~ agent(skc8,x,skc10)
| ~ be(skc8,x3,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[156,1]),
[iquote('0:MRR:156.0,1.0')] ).
cnf(737,plain,
( ~ man(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[23,562]),
[iquote('0:Res:23.1,562.1')] ).
cnf(763,plain,
( ~ accessible_world(skc8,u)
| ~ man(u,skc13) ),
inference(res,[status(thm),theory(equality)],[185,729]),
[iquote('0:Res:185.1,729.1')] ).
cnf(762,plain,
~ man(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[225,729]),
[iquote('0:Res:225.0,729.1')] ).
cnf(729,plain,
( ~ man(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[23,561]),
[iquote('0:Res:23.1,561.1')] ).
cnf(725,plain,
( ~ human_person(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[32,553]),
[iquote('0:Res:32.1,553.0')] ).
cnf(692,plain,
( ~ abstraction(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[37,551]),
[iquote('0:Res:37.1,551.1')] ).
cnf(624,plain,
( ~ entity(u,v)
| ~ state(u,v) ),
inference(res,[status(thm),theory(equality)],[28,546]),
[iquote('0:Res:28.1,546.1')] ).
cnf(600,plain,
( ~ entity(u,v)
| ~ event(u,v) ),
inference(res,[status(thm),theory(equality)],[28,545]),
[iquote('0:Res:28.1,545.1')] ).
cnf(208,plain,
( ~ accessible_world(skc8,u)
| ~ proposition(skc8,u)
| ~ event(skc8,v)
| ~ present(skc8,v)
| ~ think_believe_consider(skc8,v)
| ~ vincent_forename(skc8,w)
| ~ man(skc8,x)
| ~ jules_forename(skc8,y)
| ~ smoke(skc12,z)
| ~ present(skc12,z)
| ~ man(skc8,x1)
| ~ think_believe_consider(skc8,x2)
| ~ present(skc8,x2)
| ~ event(skc8,x2)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ theme(skc8,v,u)
| ~ of(skc8,w,x)
| ~ agent(skc8,v,x)
| ~ agent(skc12,z,x1)
| ~ of(skc8,y,x1)
| ~ of(skc8,x4,x5)
| ~ agent(skc8,x2,x5)
| ~ of(skc8,x6,x5)
| ~ theme(skc8,x2,skc12)
| ~ be(skc8,x3,x5,x5)
| man(u,skf4(u)) ),
inference(mrr,[status(thm)],[142,1,13]),
[iquote('0:MRR:142.0,142.13,1.0,13.0')] ).
cnf(565,plain,
( ~ man(u,v)
| ~ abstraction(u,v) ),
inference(res,[status(thm),theory(equality)],[23,255]),
[iquote('0:Res:23.1,255.1')] ).
cnf(736,plain,
( ~ male(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[112,562]),
[iquote('0:Res:112.1,562.1')] ).
cnf(562,plain,
( ~ state(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[35,254]),
[iquote('0:Res:35.1,254.0')] ).
cnf(728,plain,
( ~ male(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[112,561]),
[iquote('0:Res:112.1,561.1')] ).
cnf(200,plain,
( ~ smoke(u,v)
| ~ present(u,v)
| ~ accessible_world(skc8,w)
| ~ proposition(skc8,w)
| ~ event(skc8,x)
| ~ present(skc8,x)
| ~ think_believe_consider(skc8,x)
| ~ vincent_forename(skc8,y)
| ~ man(skc8,z)
| ~ jules_forename(skc8,x1)
| ~ man(skc8,x2)
| ~ proposition(skc8,u)
| ~ accessible_world(skc8,u)
| ~ state(skc8,x3)
| ~ vincent_forename(skc8,x4)
| ~ man(skc8,x5)
| ~ jules_forename(skc8,x6)
| ~ agent(u,v,x2)
| ~ theme(skc8,x,w)
| ~ of(skc8,y,z)
| ~ agent(skc8,x,z)
| ~ of(skc8,x1,x2)
| ~ of(skc8,x4,x5)
| ~ of(skc8,x6,x5)
| ~ theme(skc8,skc13,u)
| ~ agent(skc8,skc13,x5)
| ~ be(skc8,x3,x5,x5)
| man(w,skf4(w)) ),
inference(mrr,[status(thm)],[187,1,6,7]),
[iquote('0:MRR:187.0,187.10,187.11,1.0,6.0,7.0')] ).
cnf(561,plain,
( ~ event(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[47,254]),
[iquote('0:Res:47.1,254.0')] ).
cnf(553,plain,
( ~ organism(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[31,247]),
[iquote('0:Res:31.1,247.0')] ).
cnf(716,plain,
( ~ vincent_forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[20,710]),
[iquote('0:Res:20.1,710.0')] ).
cnf(715,plain,
( ~ jules_forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[19,710]),
[iquote('0:Res:19.1,710.0')] ).
cnf(713,plain,
~ state(skc12,skc14),
inference(res,[status(thm),theory(equality)],[3,710]),
[iquote('0:Res:3.0,710.0')] ).
cnf(710,plain,
( ~ forename(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[22,702]),
[iquote('0:Res:22.1,702.0')] ).
cnf(709,plain,
~ state(skc12,skc11),
inference(res,[status(thm),theory(equality)],[161,702]),
[iquote('0:Res:161.0,702.0')] ).
cnf(702,plain,
( ~ relname(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[21,699]),
[iquote('0:Res:21.1,699.0')] ).
cnf(701,plain,
( ~ proposition(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[41,699]),
[iquote('0:Res:41.1,699.0')] ).
cnf(700,plain,
~ state(skc12,skc12),
inference(res,[status(thm),theory(equality)],[102,699]),
[iquote('0:Res:102.0,699.0')] ).
cnf(699,plain,
( ~ relation(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[40,693]),
[iquote('0:Res:40.1,693.0')] ).
cnf(693,plain,
( ~ abstraction(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[37,691]),
[iquote('0:Res:37.1,691.0')] ).
cnf(172,plain,
( ~ proposition(skc8,u)
| ~ proposition(skc8,v)
| ~ think_believe_consider(skc8,w)
| ~ theme(skc8,w,u)
| ~ agent(skc8,w,x)
| ~ theme(skc8,skc13,v)
| ~ agent(skc8,skc13,x)
| equal(u,v) ),
inference(res,[status(thm),theory(equality)],[7,93]),
[iquote('0:Res:7.0,93.3')] ).
cnf(691,plain,
( ~ general(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[123,551]),
[iquote('0:Res:123.1,551.1')] ).
cnf(551,plain,
( ~ state(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[35,246]),
[iquote('0:Res:35.1,246.0')] ).
cnf(686,plain,
( ~ vincent_forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,683]),
[iquote('0:Res:20.1,683.0')] ).
cnf(685,plain,
( ~ jules_forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,683]),
[iquote('0:Res:19.1,683.0')] ).
cnf(104,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(683,plain,
( ~ forename(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[22,680]),
[iquote('0:Res:22.1,680.0')] ).
cnf(680,plain,
( ~ relname(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[21,675]),
[iquote('0:Res:21.1,675.0')] ).
cnf(679,plain,
( ~ proposition(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[41,675]),
[iquote('0:Res:41.1,675.0')] ).
cnf(675,plain,
( ~ relation(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[40,673]),
[iquote('0:Res:40.1,673.0')] ).
cnf(556,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)],[554,13,7]),
[iquote('0:MRR:554.0,554.2,13.0,7.0')] ).
cnf(673,plain,
( ~ abstraction(u,skc13)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[37,637]),
[iquote('0:Res:37.1,637.1')] ).
cnf(637,plain,
( ~ accessible_world(skc8,u)
| ~ general(u,skc13) ),
inference(res,[status(thm),theory(equality)],[185,550]),
[iquote('0:Res:185.1,550.0')] ).
cnf(664,plain,
~ vincent_forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[20,657]),
[iquote('0:Res:20.1,657.0')] ).
cnf(663,plain,
~ jules_forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[19,657]),
[iquote('0:Res:19.1,657.0')] ).
cnf(163,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(662,plain,
~ vincent_forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[20,656]),
[iquote('0:Res:20.1,656.0')] ).
cnf(661,plain,
~ jules_forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[19,656]),
[iquote('0:Res:19.1,656.0')] ).
cnf(657,plain,
~ forename(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[22,651]),
[iquote('0:Res:22.1,651.0')] ).
cnf(656,plain,
~ forename(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[22,649]),
[iquote('0:Res:22.1,649.0')] ).
cnf(537,plain,
( ~ forename(skc8,u)
| ~ entity(skc8,skc10)
| ~ of(skc8,u,skc10)
| equal(skc11,u) ),
inference(mrr,[status(thm)],[532,9]),
[iquote('0:MRR:532.1,9.0')] ).
cnf(651,plain,
~ relname(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[21,646]),
[iquote('0:Res:21.1,646.0')] ).
cnf(650,plain,
~ proposition(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[41,646]),
[iquote('0:Res:41.1,646.0')] ).
cnf(649,plain,
~ relname(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[21,645]),
[iquote('0:Res:21.1,645.0')] ).
cnf(648,plain,
~ proposition(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[41,645]),
[iquote('0:Res:41.1,645.0')] ).
cnf(536,plain,
( ~ forename(skc8,u)
| ~ entity(skc8,skc15)
| ~ of(skc8,u,skc15)
| equal(skc14,u) ),
inference(mrr,[status(thm)],[533,3]),
[iquote('0:MRR:533.1,3.0')] ).
cnf(646,plain,
~ relation(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[40,641]),
[iquote('0:Res:40.1,641.0')] ).
cnf(645,plain,
~ relation(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[40,640]),
[iquote('0:Res:40.1,640.0')] ).
cnf(641,plain,
~ abstraction(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[37,639]),
[iquote('0:Res:37.1,639.0')] ).
cnf(640,plain,
~ abstraction(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[37,636]),
[iquote('0:Res:37.1,636.0')] ).
cnf(507,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(639,plain,
~ general(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[123,636]),
[iquote('0:Res:123.1,636.0')] ).
cnf(636,plain,
~ general(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[225,550]),
[iquote('0:Res:225.0,550.0')] ).
cnf(550,plain,
( ~ event(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[47,246]),
[iquote('0:Res:47.1,246.0')] ).
cnf(627,plain,
( ~ human_person(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[32,626]),
[iquote('0:Res:32.1,626.0')] ).
cnf(141,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(626,plain,
( ~ organism(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[31,625]),
[iquote('0:Res:31.1,625.0')] ).
cnf(625,plain,
( ~ entity(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[28,623]),
[iquote('0:Res:28.1,623.0')] ).
cnf(623,plain,
( ~ existent(skc8,u)
| ~ state(skc12,u) ),
inference(res,[status(thm),theory(equality)],[117,546]),
[iquote('0:Res:117.1,546.1')] ).
cnf(546,plain,
( ~ state(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[35,237]),
[iquote('0:Res:35.1,237.0')] ).
cnf(138,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(618,plain,
~ state(skc12,skc15),
inference(res,[status(thm),theory(equality)],[2,616]),
[iquote('0:Res:2.0,616.1')] ).
cnf(616,plain,
( ~ state(skc12,u)
| ~ man(skc8,u) ),
inference(res,[status(thm),theory(equality)],[34,607]),
[iquote('0:Res:34.1,607.1')] ).
cnf(614,plain,
~ man(skc8,skf2(u)),
inference(res,[status(thm),theory(equality)],[225,607]),
[iquote('0:Res:225.0,607.1')] ).
cnf(607,plain,
( ~ man(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[33,605]),
[iquote('0:Res:33.1,605.0')] ).
cnf(140,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(609,plain,
~ state(skc12,skc10),
inference(res,[status(thm),theory(equality)],[34,606]),
[iquote('0:Res:34.1,606.0')] ).
cnf(606,plain,
~ event(skc12,skc10),
inference(res,[status(thm),theory(equality)],[153,605]),
[iquote('0:Res:153.0,605.0')] ).
cnf(605,plain,
( ~ human_person(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[32,602]),
[iquote('0:Res:32.1,602.0')] ).
cnf(602,plain,
( ~ organism(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[31,601]),
[iquote('0:Res:31.1,601.0')] ).
cnf(139,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(601,plain,
( ~ entity(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[28,599]),
[iquote('0:Res:28.1,599.0')] ).
cnf(599,plain,
( ~ existent(skc8,u)
| ~ event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[117,545]),
[iquote('0:Res:117.1,545.1')] ).
cnf(545,plain,
( ~ event(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[47,237]),
[iquote('0:Res:47.1,237.0')] ).
cnf(592,plain,
( ~ vincent_forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,589]),
[iquote('0:Res:20.1,589.0')] ).
cnf(525,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(591,plain,
( ~ jules_forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,589]),
[iquote('0:Res:19.1,589.0')] ).
cnf(589,plain,
( ~ forename(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[22,584]),
[iquote('0:Res:22.1,584.0')] ).
cnf(584,plain,
( ~ relname(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[21,581]),
[iquote('0:Res:21.1,581.0')] ).
cnf(583,plain,
( ~ proposition(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[41,581]),
[iquote('0:Res:41.1,581.0')] ).
cnf(97,plain,
( ~ actual_world(u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ smoke(x1,x2)
| ~ present(x1,x2)
| ~ man(u,x3)
| ~ proposition(u,x1)
| ~ accessible_world(u,x1)
| ~ think_believe_consider(u,x4)
| ~ present(u,x4)
| ~ event(u,x4)
| ~ state(u,x5)
| ~ vincent_forename(u,x6)
| ~ man(u,x7)
| ~ jules_forename(u,x8)
| ~ smoke(v,x9)
| ~ present(v,x9)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ agent(x1,x2,x3)
| ~ of(u,z,x3)
| ~ theme(u,x4,x1)
| ~ of(u,x6,x7)
| ~ agent(u,x4,x7)
| ~ of(u,x8,x7)
| ~ agent(v,x9,skf4(v))
| ~ be(u,x5,x7,x7) ),
inference(mrr,[status(thm)],[95,48,19,20]),
[iquote('0:MRR:95.4,95.5,95.13,95.23,95.27,95.33,48.1,19.1,20.1,48.1,19.1,20.1')] ).
cnf(581,plain,
( ~ relation(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[40,579]),
[iquote('0:Res:40.1,579.0')] ).
cnf(579,plain,
( ~ abstraction(u,skc10)
| ~ accessible_world(skc8,u) ),
inference(res,[status(thm),theory(equality)],[38,577]),
[iquote('0:Res:38.1,577.1')] ).
cnf(577,plain,
( ~ accessible_world(skc8,u)
| ~ nonhuman(u,skc10) ),
inference(res,[status(thm),theory(equality)],[151,540]),
[iquote('0:Res:151.1,540.0')] ).
cnf(540,plain,
( ~ man(u,v)
| ~ nonhuman(u,v) ),
inference(res,[status(thm),theory(equality)],[33,230]),
[iquote('0:Res:33.1,230.0')] ).
cnf(96,plain,
( ~ actual_world(u)
| ~ accessible_world(u,v)
| ~ proposition(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ think_believe_consider(u,w)
| ~ vincent_forename(u,x)
| ~ man(u,y)
| ~ jules_forename(u,z)
| ~ smoke(x1,x2)
| ~ present(x1,x2)
| ~ man(u,x3)
| ~ proposition(u,x1)
| ~ accessible_world(u,x1)
| ~ think_believe_consider(u,x4)
| ~ present(u,x4)
| ~ event(u,x4)
| ~ state(u,x5)
| ~ vincent_forename(u,x6)
| ~ man(u,x7)
| ~ jules_forename(u,x8)
| ~ theme(u,w,v)
| ~ of(u,x,y)
| ~ agent(u,w,y)
| ~ agent(x1,x2,x3)
| ~ of(u,z,x3)
| ~ theme(u,x4,x1)
| ~ of(u,x6,x7)
| ~ agent(u,x4,x7)
| ~ of(u,x8,x7)
| ~ be(u,x5,x7,x7)
| man(v,skf4(v)) ),
inference(mrr,[status(thm)],[94,19,20,48]),
[iquote('0:MRR:94.1,94.9,94.19,94.23,94.29,19.1,20.1,48.1,19.1,20.1')] ).
cnf(567,plain,
( ~ man(skc8,u)
| ~ abstraction(skc12,u) ),
inference(res,[status(thm),theory(equality)],[23,564]),
[iquote('0:Res:23.1,564.0')] ).
cnf(564,plain,
( ~ male(skc8,u)
| ~ abstraction(skc12,u) ),
inference(res,[status(thm),theory(equality)],[112,255]),
[iquote('0:Res:112.1,255.1')] ).
cnf(255,plain,
( ~ abstraction(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[36,55]),
[iquote('0:Res:36.1,55.1')] ).
cnf(254,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('NLP254+1.p',unknown),
[] ).
cnf(247,plain,
( ~ entity(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[29,54]),
[iquote('0:Res:29.1,54.1')] ).
cnf(246,plain,
( ~ eventuality(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[44,54]),
[iquote('0:Res:44.1,54.1')] ).
cnf(237,plain,
( ~ eventuality(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[43,52]),
[iquote('0:Res:43.1,52.0')] ).
cnf(230,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('NLP254+1.p',unknown),
[] ).
cnf(519,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(518,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(91,axiom,
( ~ accessible_world(u,v)
| ~ be(u,w,x,y)
| be(v,w,x,y) ),
file('NLP254+1.p',unknown),
[] ).
cnf(511,plain,
( ~ vincent_forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[20,496]),
[iquote('0:Res:20.1,496.0')] ).
cnf(510,plain,
( ~ jules_forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[19,496]),
[iquote('0:Res:19.1,496.0')] ).
cnf(506,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(514,plain,
~ state(skc8,skc14),
inference(res,[status(thm),theory(equality)],[3,505]),
[iquote('0:Res:3.0,505.0')] ).
cnf(88,axiom,
( ~ accessible_world(u,v)
| ~ of(u,w,x)
| of(v,w,x) ),
file('NLP254+1.p',unknown),
[] ).
cnf(497,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(496,plain,
( ~ forename(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[22,467]),
[iquote('0:Res:22.1,467.0')] ).
cnf(504,plain,
~ state(skc8,skc11),
inference(res,[status(thm),theory(equality)],[161,492]),
[iquote('0:Res:161.0,492.0')] ).
cnf(90,axiom,
( ~ accessible_world(u,v)
| ~ agent(u,w,x)
| agent(v,w,x) ),
file('NLP254+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ accessible_world(u,v)
| ~ theme(u,w,x)
| theme(v,w,x) ),
file('NLP254+1.p',unknown),
[] ).
cnf(467,plain,
( ~ relname(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[21,434]),
[iquote('0:Res:21.1,434.0')] ).
cnf(466,plain,
( ~ proposition(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[41,434]),
[iquote('0:Res:41.1,434.0')] ).
cnf(490,plain,
~ state(skc8,skc12),
inference(res,[status(thm),theory(equality)],[102,464]),
[iquote('0:Res:102.0,464.0')] ).
cnf(71,axiom,
( ~ accessible_world(u,v)
| ~ man(u,w)
| man(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(461,plain,
( ~ human_person(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[32,430]),
[iquote('0:Res:32.1,430.0')] ).
cnf(458,plain,
( ~ human_person(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[32,427]),
[iquote('0:Res:32.1,427.0')] ).
cnf(79,axiom,
( ~ accessible_world(u,v)
| ~ present(u,w)
| present(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(480,plain,
~ state(skc8,skc15),
inference(res,[status(thm),theory(equality)],[2,450]),
[iquote('0:Res:2.0,450.0')] ).
cnf(471,plain,
~ general(skc8,skc15),
inference(res,[status(thm),theory(equality)],[123,469]),
[iquote('0:Res:123.1,469.0')] ).
cnf(77,axiom,
( ~ accessible_world(u,v)
| ~ proposition(u,w)
| proposition(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(469,plain,
~ general(skc12,skc15),
inference(res,[status(thm),theory(equality)],[2,436]),
[iquote('0:Res:2.0,436.0')] ).
cnf(436,plain,
( ~ man(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[33,417]),
[iquote('0:Res:33.1,417.0')] ).
cnf(434,plain,
( ~ relation(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[40,415]),
[iquote('0:Res:40.1,415.0')] ).
cnf(78,axiom,
( ~ accessible_world(u,v)
| ~ think_believe_consider(u,w)
| think_believe_consider(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(430,plain,
( ~ organism(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[31,409]),
[iquote('0:Res:31.1,409.0')] ).
cnf(427,plain,
( ~ organism(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[31,407]),
[iquote('0:Res:31.1,407.0')] ).
cnf(86,axiom,
( ~ accessible_world(u,v)
| ~ event(u,w)
| event(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(421,plain,
( ~ man(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[23,395]),
[iquote('0:Res:23.1,395.1')] ).
cnf(419,plain,
( ~ man(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[23,394]),
[iquote('0:Res:23.1,394.1')] ).
cnf(58,axiom,
( ~ accessible_world(u,v)
| ~ jules_forename(u,w)
| jules_forename(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(443,plain,
~ state(skc8,skc10),
inference(res,[status(thm),theory(equality)],[34,441]),
[iquote('0:Res:34.1,441.0')] ).
cnf(441,plain,
~ event(skc8,skc10),
inference(res,[status(thm),theory(equality)],[152,418]),
[iquote('0:Res:152.0,418.0')] ).
cnf(437,plain,
~ general(skc8,skc10),
inference(res,[status(thm),theory(equality)],[123,435]),
[iquote('0:Res:123.1,435.0')] ).
cnf(59,axiom,
( ~ accessible_world(u,v)
| ~ vincent_forename(u,w)
| vincent_forename(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(435,plain,
~ general(skc12,skc10),
inference(res,[status(thm),theory(equality)],[153,417]),
[iquote('0:Res:153.0,417.0')] ).
cnf(417,plain,
( ~ human_person(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[32,391]),
[iquote('0:Res:32.1,391.0')] ).
cnf(415,plain,
( ~ abstraction(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[37,338]),
[iquote('0:Res:37.1,338.1')] ).
cnf(87,axiom,
( ~ accessible_world(u,v)
| ~ smoke(u,w)
| smoke(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(409,plain,
( ~ entity(skc12,u)
| ~ state(skc8,u) ),
inference(res,[status(thm),theory(equality)],[28,302]),
[iquote('0:Res:28.1,302.1')] ).
cnf(407,plain,
( ~ entity(skc12,u)
| ~ event(skc8,u) ),
inference(res,[status(thm),theory(equality)],[28,301]),
[iquote('0:Res:28.1,301.1')] ).
cnf(72,axiom,
( ~ accessible_world(u,v)
| ~ state(u,w)
| state(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(404,plain,
( ~ man(skc12,u)
| ~ abstraction(skc8,u) ),
inference(res,[status(thm),theory(equality)],[23,298]),
[iquote('0:Res:23.1,298.1')] ).
cnf(395,plain,
( ~ state(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[35,297]),
[iquote('0:Res:35.1,297.0')] ).
cnf(394,plain,
( ~ event(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[47,297]),
[iquote('0:Res:47.1,297.0')] ).
cnf(391,plain,
( ~ organism(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[31,296]),
[iquote('0:Res:31.1,296.0')] ).
cnf(61,axiom,
( ~ accessible_world(u,v)
| ~ forename(u,w)
| forename(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(338,plain,
( ~ state(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[35,295]),
[iquote('0:Res:35.1,295.0')] ).
cnf(337,plain,
( ~ event(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[47,295]),
[iquote('0:Res:47.1,295.0')] ).
cnf(302,plain,
( ~ state(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[35,294]),
[iquote('0:Res:35.1,294.0')] ).
cnf(301,plain,
( ~ event(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[47,294]),
[iquote('0:Res:47.1,294.0')] ).
cnf(85,axiom,
( ~ accessible_world(u,v)
| ~ eventuality(u,w)
| eventuality(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(298,plain,
( ~ abstraction(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[36,253]),
[iquote('0:Res:36.1,253.0')] ).
cnf(399,plain,
~ male(skc8,skc9),
inference(res,[status(thm),theory(equality)],[112,393]),
[iquote('0:Res:112.1,393.0')] ).
cnf(396,plain,
~ male(skc8,skc13),
inference(res,[status(thm),theory(equality)],[112,392]),
[iquote('0:Res:112.1,392.0')] ).
cnf(393,plain,
~ male(skc12,skc9),
inference(res,[status(thm),theory(equality)],[148,297]),
[iquote('0:Res:148.0,297.0')] ).
cnf(68,axiom,
( ~ accessible_world(u,v)
| ~ entity(u,w)
| entity(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(392,plain,
~ male(skc12,skc13),
inference(res,[status(thm),theory(equality)],[186,297]),
[iquote('0:Res:186.0,297.0')] ).
cnf(297,plain,
( ~ eventuality(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[42,253]),
[iquote('0:Res:42.1,253.0')] ).
cnf(296,plain,
( ~ entity(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[29,245]),
[iquote('0:Res:29.1,245.0')] ).
cnf(386,plain,
~ vincent_forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[20,376]),
[iquote('0:Res:20.1,376.0')] ).
cnf(70,axiom,
( ~ accessible_world(u,v)
| ~ human_person(u,w)
| human_person(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(385,plain,
~ jules_forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[19,376]),
[iquote('0:Res:19.1,376.0')] ).
cnf(381,plain,
~ vincent_forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[20,371]),
[iquote('0:Res:20.1,371.0')] ).
cnf(380,plain,
~ jules_forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[19,371]),
[iquote('0:Res:19.1,371.0')] ).
cnf(379,plain,
~ vincent_forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[20,370]),
[iquote('0:Res:20.1,370.0')] ).
cnf(75,axiom,
( ~ accessible_world(u,v)
| ~ abstraction(u,w)
| abstraction(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(378,plain,
~ jules_forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[19,370]),
[iquote('0:Res:19.1,370.0')] ).
cnf(376,plain,
~ forename(skc8,skc9),
inference(res,[status(thm),theory(equality)],[22,366]),
[iquote('0:Res:22.1,366.0')] ).
cnf(374,plain,
~ vincent_forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[20,364]),
[iquote('0:Res:20.1,364.0')] ).
cnf(373,plain,
~ jules_forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[19,364]),
[iquote('0:Res:19.1,364.0')] ).
cnf(69,axiom,
( ~ accessible_world(u,v)
| ~ organism(u,w)
| organism(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(371,plain,
~ forename(skc8,skc13),
inference(res,[status(thm),theory(equality)],[22,360]),
[iquote('0:Res:22.1,360.0')] ).
cnf(370,plain,
~ forename(skc12,skc9),
inference(res,[status(thm),theory(equality)],[22,358]),
[iquote('0:Res:22.1,358.0')] ).
cnf(366,plain,
~ relname(skc8,skc9),
inference(res,[status(thm),theory(equality)],[21,355]),
[iquote('0:Res:21.1,355.0')] ).
cnf(365,plain,
~ proposition(skc8,skc9),
inference(res,[status(thm),theory(equality)],[41,355]),
[iquote('0:Res:41.1,355.0')] ).
cnf(76,axiom,
( ~ accessible_world(u,v)
| ~ relation(u,w)
| relation(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(364,plain,
~ forename(skc12,skc13),
inference(res,[status(thm),theory(equality)],[22,354]),
[iquote('0:Res:22.1,354.0')] ).
cnf(360,plain,
~ relname(skc8,skc13),
inference(res,[status(thm),theory(equality)],[21,350]),
[iquote('0:Res:21.1,350.0')] ).
cnf(359,plain,
~ proposition(skc8,skc13),
inference(res,[status(thm),theory(equality)],[41,350]),
[iquote('0:Res:41.1,350.0')] ).
cnf(358,plain,
~ relname(skc12,skc9),
inference(res,[status(thm),theory(equality)],[21,349]),
[iquote('0:Res:21.1,349.0')] ).
cnf(84,axiom,
( ~ accessible_world(u,v)
| ~ thing(u,w)
| thing(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(357,plain,
~ proposition(skc12,skc9),
inference(res,[status(thm),theory(equality)],[41,349]),
[iquote('0:Res:41.1,349.0')] ).
cnf(355,plain,
~ relation(skc8,skc9),
inference(res,[status(thm),theory(equality)],[40,347]),
[iquote('0:Res:40.1,347.0')] ).
cnf(354,plain,
~ relname(skc12,skc13),
inference(res,[status(thm),theory(equality)],[21,346]),
[iquote('0:Res:21.1,346.0')] ).
cnf(353,plain,
~ proposition(skc12,skc13),
inference(res,[status(thm),theory(equality)],[41,346]),
[iquote('0:Res:41.1,346.0')] ).
cnf(60,axiom,
( ~ accessible_world(u,v)
| ~ relname(u,w)
| relname(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(350,plain,
~ relation(skc8,skc13),
inference(res,[status(thm),theory(equality)],[40,343]),
[iquote('0:Res:40.1,343.0')] ).
cnf(349,plain,
~ relation(skc12,skc9),
inference(res,[status(thm),theory(equality)],[40,342]),
[iquote('0:Res:40.1,342.0')] ).
cnf(347,plain,
~ abstraction(skc8,skc9),
inference(res,[status(thm),theory(equality)],[37,341]),
[iquote('0:Res:37.1,341.0')] ).
cnf(346,plain,
~ relation(skc12,skc13),
inference(res,[status(thm),theory(equality)],[40,340]),
[iquote('0:Res:40.1,340.0')] ).
cnf(62,axiom,
( ~ accessible_world(u,v)
| ~ male(u,w)
| male(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(343,plain,
~ abstraction(skc8,skc13),
inference(res,[status(thm),theory(equality)],[37,339]),
[iquote('0:Res:37.1,339.0')] ).
cnf(342,plain,
~ abstraction(skc12,skc9),
inference(res,[status(thm),theory(equality)],[37,336]),
[iquote('0:Res:37.1,336.0')] ).
cnf(341,plain,
~ general(skc8,skc9),
inference(res,[status(thm),theory(equality)],[123,336]),
[iquote('0:Res:123.1,336.0')] ).
cnf(340,plain,
~ abstraction(skc12,skc13),
inference(res,[status(thm),theory(equality)],[37,335]),
[iquote('0:Res:37.1,335.0')] ).
cnf(80,axiom,
( ~ accessible_world(u,v)
| ~ unisex(u,w)
| unisex(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(339,plain,
~ general(skc8,skc13),
inference(res,[status(thm),theory(equality)],[123,335]),
[iquote('0:Res:123.1,335.0')] ).
cnf(336,plain,
~ general(skc12,skc9),
inference(res,[status(thm),theory(equality)],[148,295]),
[iquote('0:Res:148.0,295.0')] ).
cnf(335,plain,
~ general(skc12,skc13),
inference(res,[status(thm),theory(equality)],[186,295]),
[iquote('0:Res:186.0,295.0')] ).
cnf(295,plain,
( ~ eventuality(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[44,245]),
[iquote('0:Res:44.1,245.0')] ).
cnf(82,axiom,
( ~ accessible_world(u,v)
| ~ specific(u,w)
| specific(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(332,plain,
~ man(skc8,skc9),
inference(res,[status(thm),theory(equality)],[33,326]),
[iquote('0:Res:33.1,326.0')] ).
cnf(329,plain,
~ man(skc8,skc13),
inference(res,[status(thm),theory(equality)],[33,322]),
[iquote('0:Res:33.1,322.0')] ).
cnf(327,plain,
~ man(skc12,skc9),
inference(res,[status(thm),theory(equality)],[33,320]),
[iquote('0:Res:33.1,320.0')] ).
cnf(326,plain,
~ human_person(skc8,skc9),
inference(res,[status(thm),theory(equality)],[32,319]),
[iquote('0:Res:32.1,319.0')] ).
cnf(64,axiom,
( ~ accessible_world(u,v)
| ~ human(u,w)
| human(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(323,plain,
~ man(skc12,skc13),
inference(res,[status(thm),theory(equality)],[33,316]),
[iquote('0:Res:33.1,316.0')] ).
cnf(322,plain,
~ human_person(skc8,skc13),
inference(res,[status(thm),theory(equality)],[32,315]),
[iquote('0:Res:32.1,315.0')] ).
cnf(320,plain,
~ human_person(skc12,skc9),
inference(res,[status(thm),theory(equality)],[32,314]),
[iquote('0:Res:32.1,314.0')] ).
cnf(319,plain,
~ organism(skc8,skc9),
inference(res,[status(thm),theory(equality)],[31,312]),
[iquote('0:Res:31.1,312.0')] ).
cnf(67,axiom,
( ~ accessible_world(u,v)
| ~ existent(u,w)
| existent(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(316,plain,
~ human_person(skc12,skc13),
inference(res,[status(thm),theory(equality)],[32,310]),
[iquote('0:Res:32.1,310.0')] ).
cnf(315,plain,
~ organism(skc8,skc13),
inference(res,[status(thm),theory(equality)],[31,308]),
[iquote('0:Res:31.1,308.0')] ).
cnf(314,plain,
~ organism(skc12,skc9),
inference(res,[status(thm),theory(equality)],[31,307]),
[iquote('0:Res:31.1,307.0')] ).
cnf(312,plain,
~ entity(skc8,skc9),
inference(res,[status(thm),theory(equality)],[28,306]),
[iquote('0:Res:28.1,306.0')] ).
cnf(73,axiom,
( ~ accessible_world(u,v)
| ~ general(u,w)
| general(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(310,plain,
~ organism(skc12,skc13),
inference(res,[status(thm),theory(equality)],[31,305]),
[iquote('0:Res:31.1,305.0')] ).
cnf(308,plain,
~ entity(skc8,skc13),
inference(res,[status(thm),theory(equality)],[28,304]),
[iquote('0:Res:28.1,304.0')] ).
cnf(307,plain,
~ entity(skc12,skc9),
inference(res,[status(thm),theory(equality)],[28,300]),
[iquote('0:Res:28.1,300.0')] ).
cnf(306,plain,
~ existent(skc8,skc9),
inference(res,[status(thm),theory(equality)],[117,300]),
[iquote('0:Res:117.1,300.0')] ).
cnf(74,axiom,
( ~ accessible_world(u,v)
| ~ nonhuman(u,w)
| nonhuman(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(305,plain,
~ entity(skc12,skc13),
inference(res,[status(thm),theory(equality)],[28,299]),
[iquote('0:Res:28.1,299.0')] ).
cnf(304,plain,
~ existent(skc8,skc13),
inference(res,[status(thm),theory(equality)],[117,299]),
[iquote('0:Res:117.1,299.0')] ).
cnf(300,plain,
~ existent(skc12,skc9),
inference(res,[status(thm),theory(equality)],[148,294]),
[iquote('0:Res:148.0,294.0')] ).
cnf(299,plain,
~ existent(skc12,skc13),
inference(res,[status(thm),theory(equality)],[186,294]),
[iquote('0:Res:186.0,294.0')] ).
cnf(81,axiom,
( ~ accessible_world(u,v)
| ~ nonexistent(u,w)
| nonexistent(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(294,plain,
( ~ eventuality(skc8,u)
| ~ existent(skc12,u) ),
inference(res,[status(thm),theory(equality)],[43,236]),
[iquote('0:Res:43.1,236.0')] ).
cnf(253,plain,
( ~ unisex(skc8,u)
| ~ male(skc12,u) ),
inference(res,[status(thm),theory(equality)],[130,55]),
[iquote('0:Res:130.1,55.1')] ).
cnf(245,plain,
( ~ specific(skc8,u)
| ~ general(skc12,u) ),
inference(res,[status(thm),theory(equality)],[132,54]),
[iquote('0:Res:132.1,54.1')] ).
cnf(236,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('NLP254+1.p',unknown),
[] ).
cnf(289,plain,
~ vincent_forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[20,284]),
[iquote('0:Res:20.1,284.0')] ).
cnf(288,plain,
~ jules_forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[19,284]),
[iquote('0:Res:19.1,284.0')] ).
cnf(287,plain,
~ vincent_forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[20,282]),
[iquote('0:Res:20.1,282.0')] ).
cnf(286,plain,
~ jules_forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[19,282]),
[iquote('0:Res:19.1,282.0')] ).
cnf(65,axiom,
( ~ accessible_world(u,v)
| ~ living(u,w)
| living(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(284,plain,
~ forename(skc8,skc15),
inference(res,[status(thm),theory(equality)],[22,279]),
[iquote('0:Res:22.1,279.0')] ).
cnf(282,plain,
~ forename(skc12,skc15),
inference(res,[status(thm),theory(equality)],[22,277]),
[iquote('0:Res:22.1,277.0')] ).
cnf(279,plain,
~ relname(skc8,skc15),
inference(res,[status(thm),theory(equality)],[21,273]),
[iquote('0:Res:21.1,273.0')] ).
cnf(278,plain,
~ proposition(skc8,skc15),
inference(res,[status(thm),theory(equality)],[41,273]),
[iquote('0:Res:41.1,273.0')] ).
cnf(66,axiom,
( ~ accessible_world(u,v)
| ~ impartial(u,w)
| impartial(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(277,plain,
~ relname(skc12,skc15),
inference(res,[status(thm),theory(equality)],[21,272]),
[iquote('0:Res:21.1,272.0')] ).
cnf(276,plain,
~ proposition(skc12,skc15),
inference(res,[status(thm),theory(equality)],[41,272]),
[iquote('0:Res:41.1,272.0')] ).
cnf(273,plain,
~ relation(skc8,skc15),
inference(res,[status(thm),theory(equality)],[40,270]),
[iquote('0:Res:40.1,270.0')] ).
cnf(272,plain,
~ relation(skc12,skc15),
inference(res,[status(thm),theory(equality)],[40,269]),
[iquote('0:Res:40.1,269.0')] ).
cnf(83,axiom,
( ~ accessible_world(u,v)
| ~ singleton(u,w)
| singleton(v,w) ),
file('NLP254+1.p',unknown),
[] ).
cnf(270,plain,
~ abstraction(skc8,skc15),
inference(res,[status(thm),theory(equality)],[38,268]),
[iquote('0:Res:38.1,268.0')] ).
cnf(269,plain,
~ abstraction(skc12,skc15),
inference(res,[status(thm),theory(equality)],[38,265]),
[iquote('0:Res:38.1,265.0')] ).
cnf(268,plain,
~ nonhuman(skc8,skc15),
inference(res,[status(thm),theory(equality)],[124,265]),
[iquote('0:Res:124.1,265.0')] ).
cnf(265,plain,
~ nonhuman(skc12,skc15),
inference(res,[status(thm),theory(equality)],[2,233]),
[iquote('0:Res:2.0,233.0')] ).
cnf(57,axiom,
( ~ be(u,v,w,x)
| equal(w,x) ),
file('NLP254+1.p',unknown),
[] ).
cnf(233,plain,
( ~ man(skc8,u)
| ~ nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[33,231]),
[iquote('0:Res:33.1,231.0')] ).
cnf(261,plain,
~ vincent_forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[20,256]),
[iquote('0:Res:20.1,256.0')] ).
cnf(260,plain,
~ jules_forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[19,256]),
[iquote('0:Res:19.1,256.0')] ).
cnf(259,plain,
~ vincent_forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[20,252]),
[iquote('0:Res:20.1,252.0')] ).
cnf(56,axiom,
( ~ man(skc12,u)
| agent(skc12,skf2(u),u) ),
file('NLP254+1.p',unknown),
[] ).
cnf(258,plain,
~ jules_forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[19,252]),
[iquote('0:Res:19.1,252.0')] ).
cnf(256,plain,
~ forename(skc8,skc10),
inference(res,[status(thm),theory(equality)],[22,249]),
[iquote('0:Res:22.1,249.0')] ).
cnf(252,plain,
~ forename(skc12,skc10),
inference(res,[status(thm),theory(equality)],[22,244]),
[iquote('0:Res:22.1,244.0')] ).
cnf(249,plain,
~ relname(skc8,skc10),
inference(res,[status(thm),theory(equality)],[21,241]),
[iquote('0:Res:21.1,241.0')] ).
cnf(55,axiom,
( ~ male(u,v)
| ~ unisex(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(248,plain,
~ proposition(skc8,skc10),
inference(res,[status(thm),theory(equality)],[41,241]),
[iquote('0:Res:41.1,241.0')] ).
cnf(244,plain,
~ relname(skc12,skc10),
inference(res,[status(thm),theory(equality)],[21,240]),
[iquote('0:Res:21.1,240.0')] ).
cnf(243,plain,
~ proposition(skc12,skc10),
inference(res,[status(thm),theory(equality)],[41,240]),
[iquote('0:Res:41.1,240.0')] ).
cnf(241,plain,
~ relation(skc8,skc10),
inference(res,[status(thm),theory(equality)],[40,238]),
[iquote('0:Res:40.1,238.0')] ).
cnf(54,axiom,
( ~ general(u,v)
| ~ specific(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(240,plain,
~ relation(skc12,skc10),
inference(res,[status(thm),theory(equality)],[40,235]),
[iquote('0:Res:40.1,235.0')] ).
cnf(238,plain,
~ abstraction(skc8,skc10),
inference(res,[status(thm),theory(equality)],[38,234]),
[iquote('0:Res:38.1,234.0')] ).
cnf(235,plain,
~ abstraction(skc12,skc10),
inference(res,[status(thm),theory(equality)],[38,232]),
[iquote('0:Res:38.1,232.0')] ).
cnf(234,plain,
~ nonhuman(skc8,skc10),
inference(res,[status(thm),theory(equality)],[124,232]),
[iquote('0:Res:124.1,232.0')] ).
cnf(52,axiom,
( ~ nonexistent(u,v)
| ~ existent(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(232,plain,
~ nonhuman(skc12,skc10),
inference(res,[status(thm),theory(equality)],[153,231]),
[iquote('0:Res:153.0,231.0')] ).
cnf(231,plain,
( ~ human_person(skc8,u)
| ~ nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[25,229]),
[iquote('0:Res:25.1,229.0')] ).
cnf(229,plain,
( ~ human(skc8,u)
| ~ nonhuman(skc12,u) ),
inference(res,[status(thm),theory(equality)],[114,53]),
[iquote('0:Res:114.1,53.0')] ).
cnf(228,plain,
present(skc12,skf2(u)),
inference(mrr,[status(thm)],[227,12]),
[iquote('0:MRR:227.0,12.0')] ).
cnf(53,axiom,
( ~ human(u,v)
| ~ nonhuman(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(221,plain,
( ~ smoke(skc8,u)
| event(skc12,u) ),
inference(res,[status(thm),theory(equality)],[137,48]),
[iquote('0:Res:137.1,48.0')] ).
cnf(225,plain,
event(skc12,skf2(u)),
inference(res,[status(thm),theory(equality)],[224,48]),
[iquote('0:Res:224.0,48.0')] ).
cnf(224,plain,
smoke(skc12,skf2(u)),
inference(mrr,[status(thm)],[223,12]),
[iquote('0:MRR:223.0,12.0')] ).
cnf(48,axiom,
( ~ smoke(u,v)
| event(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ state(u,v)
| event(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ jules_forename(u,v)
| forename(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ vincent_forename(u,v)
| forename(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ event(u,v)
| eventuality(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ state(u,v)
| eventuality(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ organism(u,v)
| entity(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ man(u,v)
| human_person(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ relation(u,v)
| abstraction(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ proposition(u,v)
| relation(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ eventuality(u,v)
| thing(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ entity(u,v)
| thing(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ human_person(u,v)
| organism(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ abstraction(u,v)
| thing(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ relname(u,v)
| relation(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ man(u,v)
| male(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ forename(u,v)
| relname(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ eventuality(u,v)
| unisex(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ eventuality(u,v)
| specific(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ entity(u,v)
| specific(u,v) ),
file('NLP254+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ abstraction(u,v)
| unisex(u,v) ),
file('NLP254+1.p',unknown),
[] ).
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(177,plain,
( ~ accessible_world(skc8,u)
| present(u,skc13) ),
inference(res,[status(thm),theory(equality)],[6,79]),
[iquote('0:Res:6.0,79.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('NLP254+1.p',unknown),
[] ).
cnf(171,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(185,plain,
( ~ accessible_world(skc8,u)
| event(u,skc13) ),
inference(res,[status(thm),theory(equality)],[5,86]),
[iquote('0:Res:5.0,86.0')] ).
cnf(165,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(191,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(28,axiom,
( ~ entity(u,v)
| existent(u,v) ),
file('NLP254+1.p',unknown),
[] ).
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(160,plain,
( ~ accessible_world(skc8,u)
| forename(u,skc11) ),
inference(res,[status(thm),theory(equality)],[9,61]),
[iquote('0:Res:9.0,61.0')] ).
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(129,plain,
( ~ present(skc8,u)
| present(skc12,u) ),
inference(res,[status(thm),theory(equality)],[12,79]),
[iquote('0:Res:12.0,79.1')] ).
cnf(25,axiom,
( ~ human_person(u,v)
| human(u,v) ),
file('NLP254+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(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(37,axiom,
( ~ abstraction(u,v)
| general(u,v) ),
file('NLP254+1.p',unknown),
[] ).
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(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(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('NLP254+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('NLP254+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('NLP254+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('NLP254+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('NLP254+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('NLP254+1.p',unknown),
[] ).
cnf(14,axiom,
of(skc8,skc14,skc15),
file('NLP254+1.p',unknown),
[] ).
cnf(17,axiom,
of(skc8,skc11,skc10),
file('NLP254+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(15,axiom,
agent(skc8,skc13,skc15),
file('NLP254+1.p',unknown),
[] ).
cnf(186,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('NLP254+1.p',unknown),
[] ).
cnf(161,plain,
relname(skc8,skc11),
inference(res,[status(thm),theory(equality)],[9,22]),
[iquote('0:Res:9.0,22.0')] ).
cnf(2,axiom,
man(skc8,skc15),
file('NLP254+1.p',unknown),
[] ).
cnf(10,axiom,
man(skc8,skc10),
file('NLP254+1.p',unknown),
[] ).
cnf(6,axiom,
present(skc8,skc13),
file('NLP254+1.p',unknown),
[] ).
cnf(12,axiom,
accessible_world(skc8,skc12),
file('NLP254+1.p',unknown),
[] ).
cnf(13,axiom,
proposition(skc8,skc12),
file('NLP254+1.p',unknown),
[] ).
cnf(5,axiom,
event(skc8,skc13),
file('NLP254+1.p',unknown),
[] ).
cnf(7,axiom,
think_believe_consider(skc8,skc13),
file('NLP254+1.p',unknown),
[] ).
cnf(4,axiom,
vincent_forename(skc8,skc14),
file('NLP254+1.p',unknown),
[] ).
cnf(8,axiom,
jules_forename(skc8,skc11),
file('NLP254+1.p',unknown),
[] ).
cnf(11,axiom,
state(skc8,skc9),
file('NLP254+1.p',unknown),
[] ).
cnf(3,axiom,
forename(skc8,skc14),
file('NLP254+1.p',unknown),
[] ).
cnf(9,axiom,
forename(skc8,skc11),
file('NLP254+1.p',unknown),
[] ).
cnf(1,axiom,
actual_world(skc8),
file('NLP254+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NLP254+1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.31 % Computer : n012.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 600
% 0.12/0.31 % DateTime : Thu Jun 30 22:55:32 EDT 2022
% 0.12/0.32 % CPUTime :
% 1.82/2.03
% 1.82/2.03 SPASS V 3.9
% 1.82/2.03 SPASS beiseite: Completion found.
% 1.82/2.03 % SZS status CounterSatisfiable
% 1.82/2.03 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.82/2.03 SPASS derived 1506 clauses, backtracked 0 clauses, performed 0 splits and kept 752 clauses.
% 1.82/2.03 SPASS allocated 101948 KBytes.
% 1.82/2.03 SPASS spent 0:00:01.70 on the problem.
% 1.82/2.03 0:00:00.04 for the input.
% 1.82/2.03 0:00:00.17 for the FLOTTER CNF translation.
% 1.82/2.03 0:00:00.10 for inferences.
% 1.82/2.03 0:00:00.00 for the backtracking.
% 1.82/2.03 0:00:01.17 for the reduction.
% 1.82/2.03
% 1.82/2.03
% 1.82/2.03 The saturated set of worked-off clauses is :
% 1.82/2.03 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------