%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP224-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 05:28:24 EDT 2022
% Result : Satisfiable 0.72s 0.92s
% Output : Saturation 0.76s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 5152)
% Comments :
%------------------------------------------------------------------------------
cnf(5153,plain,
( ~ accessible_world(skc14,u)
| ~ think_believe_consider(u,skf1(skc17))
| ~ proposition(u,v)
| ~ proposition(u,w)
| ~ theme(u,skf1(skc17),v)
| ~ theme(u,skc15,w)
| equal(w,v) ),
inference(mrr,[status(thm)],[5152,187]),
[iquote('0:MRR:5152.0,187.0')] ).
cnf(5159,plain,
( ~ accessible_world(skc14,u)
| ~ proposition(u,v)
| ~ theme(u,skc15,v)
| equal(v,skc14) ),
inference(mrr,[status(thm)],[5158,1453]),
[iquote('0:MRR:5158.1,1453.1')] ).
cnf(5151,plain,
( ~ accessible_world(skc14,u)
| ~ proposition(u,v)
| ~ proposition(u,w)
| ~ theme(u,skc15,v)
| ~ theme(u,skc15,w)
| equal(w,v) ),
inference(mrr,[status(thm)],[5150,516]),
[iquote('0:MRR:5150.1,516.1')] ).
cnf(2499,plain,
( ~ accessible_world(skc14,u)
| ~ think_believe_consider(u,v)
| ~ proposition(u,w)
| ~ proposition(u,x)
| ~ agent(u,v,skc17)
| ~ theme(u,v,w)
| ~ theme(u,skc15,x)
| equal(x,w) ),
inference(mrr,[status(thm)],[2495,516]),
[iquote('0:MRR:2495.2,516.1')] ).
cnf(5080,plain,
( ~ theme(skc9,skf1(skc17),u)
| ~ think_believe_consider(skc14,skf1(skc17))
| ~ proposition(skc14,u)
| ~ proposition(skc14,v)
| ~ theme(skc14,skc15,v)
| equal(v,u) ),
inference(res,[status(thm),theory(equality)],[102,3042]),
[iquote('0:Res:102.1,3042.3')] ).
cnf(5097,plain,
( ~ proposition(skc14,u)
| ~ proposition(skc14,v)
| ~ theme(skc14,skc15,u)
| ~ theme(skc14,skc15,v)
| equal(v,u) ),
inference(mrr,[status(thm)],[5093,196]),
[iquote('0:MRR:5093.0,196.0')] ).
cnf(5135,plain,
( ~ proposition(skc14,skc14)
| ~ proposition(skc14,u)
| ~ theme(skc14,skc15,u)
| equal(u,skc14) ),
inference(res,[status(thm),theory(equality)],[88,5052]),
[iquote('0:Res:88.0,5052.0')] ).
cnf(5052,plain,
( ~ theme(skc9,skc15,u)
| ~ proposition(skc14,u)
| ~ proposition(skc14,v)
| ~ theme(skc14,skc15,v)
| equal(v,u) ),
inference(mrr,[status(thm)],[5049,84]),
[iquote('0:MRR:5049.1,84.0')] ).
cnf(5130,plain,
( ~ theme(skc9,skc15,u)
| ~ proposition(skc14,u)
| equal(u,skc14) ),
inference(mrr,[status(thm)],[5129,84]),
[iquote('0:MRR:5129.1,84.0')] ).
cnf(5051,plain,
( ~ accessible_world(skc9,u)
| ~ proposition(u,v)
| ~ theme(u,skc15,v)
| equal(v,skc14) ),
inference(mrr,[status(thm)],[5050,98]),
[iquote('0:MRR:5050.1,98.1')] ).
cnf(2569,plain,
( ~ accessible_world(skc14,u)
| ~ forename(u,v)
| ~ of(u,v,skc13)
| equal(v,skc12) ),
inference(mrr,[status(thm)],[2568,2016,1459]),
[iquote('0:MRR:2568.1,2568.3,2016.1,1459.1')] ).
cnf(2523,plain,
( ~ accessible_world(skc14,u)
| ~ forename(u,v)
| ~ of(u,v,skc17)
| equal(v,skc16) ),
inference(mrr,[status(thm)],[2522,2008,572]),
[iquote('0:MRR:2522.1,2522.3,2008.1,572.1')] ).
cnf(3218,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[3171,1034]),
[iquote('0:Res:3171.2,1034.0')] ).
cnf(3071,plain,
( ~ think_believe_consider(skc14,u)
| ~ proposition(skc14,v)
| ~ proposition(skc14,w)
| ~ agent(skc14,u,skc17)
| ~ theme(skc14,u,v)
| ~ theme(skc14,skc15,w)
| equal(w,v) ),
inference(mrr,[status(thm)],[3067,196]),
[iquote('0:MRR:3067.1,196.0')] ).
cnf(3217,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[3171,2071]),
[iquote('0:Res:3171.2,2071.0')] ).
cnf(3186,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[3169,1034]),
[iquote('0:Res:3169.2,1034.0')] ).
cnf(3185,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[3169,2071]),
[iquote('0:Res:3169.2,2071.0')] ).
cnf(3100,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[2245,2168]),
[iquote('0:Res:2245.2,2168.0')] ).
cnf(3041,plain,
( ~ agent(skc9,u,skc17)
| ~ think_believe_consider(skc14,u)
| ~ proposition(skc14,v)
| ~ proposition(skc14,w)
| ~ theme(skc14,u,v)
| ~ theme(skc14,skc15,w)
| equal(w,v) ),
inference(mrr,[status(thm)],[3038,84]),
[iquote('0:MRR:3038.1,84.0')] ).
cnf(3099,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[2251,2168]),
[iquote('0:Res:2251.2,2168.0')] ).
cnf(3006,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[2245,2095]),
[iquote('0:Res:2245.2,2095.0')] ).
cnf(3005,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[2251,2095]),
[iquote('0:Res:2251.2,2095.0')] ).
cnf(2942,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[2245,2081]),
[iquote('0:Res:2245.2,2081.0')] ).
cnf(3042,plain,
( ~ think_believe_consider(skc14,skf1(skc17))
| ~ proposition(skc14,u)
| ~ proposition(skc14,v)
| ~ theme(skc14,skf1(skc17),u)
| ~ theme(skc14,skc15,v)
| equal(v,u) ),
inference(mrr,[status(thm)],[3036,162,84]),
[iquote('0:MRR:3036.0,3036.1,162.1,84.0')] ).
cnf(2941,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[2251,2081]),
[iquote('0:Res:2251.2,2081.0')] ).
cnf(2893,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[2226,2071]),
[iquote('0:Res:2226.2,2071.0')] ).
cnf(2841,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[2260,2052]),
[iquote('0:Res:2260.2,2052.0')] ).
cnf(2785,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[2452,779]),
[iquote('0:Res:2452.2,779.0')] ).
cnf(3040,plain,
( ~ accessible_world(skc9,u)
| ~ proposition(u,v)
| ~ proposition(u,w)
| ~ theme(u,skc15,v)
| ~ theme(u,skc15,w)
| equal(w,v) ),
inference(mrr,[status(thm)],[3039,148]),
[iquote('0:MRR:3039.1,148.1')] ).
cnf(2769,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[2439,780]),
[iquote('0:Res:2439.2,780.0')] ).
cnf(2725,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[2411,781]),
[iquote('0:Res:2411.2,781.0')] ).
cnf(2694,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[2393,781]),
[iquote('0:Res:2393.2,781.0')] ).
cnf(2628,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| existent(w,u) ),
inference(res,[status(thm),theory(equality)],[2260,833]),
[iquote('0:Res:2260.2,833.0')] ).
cnf(2948,plain,
( ~ entity(skc14,skc13)
| ~ forename(skc14,u)
| ~ forename(skc14,skc12)
| ~ of(skc14,u,skc13)
| equal(u,skc12) ),
inference(res,[status(thm),theory(equality)],[89,721]),
[iquote('0:Res:89.0,721.0')] ).
cnf(2627,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[2260,880]),
[iquote('0:Res:2260.2,880.0')] ).
cnf(2626,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[2260,1004]),
[iquote('0:Res:2260.2,1004.0')] ).
cnf(2609,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| abstraction(w,u) ),
inference(res,[status(thm),theory(equality)],[2251,1046]),
[iquote('0:Res:2251.2,1046.0')] ).
cnf(2581,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| abstraction(w,u) ),
inference(res,[status(thm),theory(equality)],[2245,1046]),
[iquote('0:Res:2245.2,1046.0')] ).
cnf(2877,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| agent(w,skf1(u),u) ),
inference(res,[status(thm),theory(equality)],[111,1203]),
[iquote('0:Res:111.1,1203.0')] ).
cnf(2546,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[2226,791]),
[iquote('0:Res:2226.2,791.0')] ).
cnf(2545,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[2226,800]),
[iquote('0:Res:2226.2,800.0')] ).
cnf(2544,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[2226,865]),
[iquote('0:Res:2226.2,865.0')] ).
cnf(2543,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[2226,1034]),
[iquote('0:Res:2226.2,1034.0')] ).
cnf(2954,plain,
( ~ entity(skc14,skc17)
| ~ forename(skc14,u)
| ~ of(skc14,u,skc17)
| equal(u,skc16) ),
inference(mrr,[status(thm)],[2949,192]),
[iquote('0:MRR:2949.2,192.0')] ).
cnf(2457,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| entity(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,1150]),
[iquote('0:Res:1064.2,1150.0')] ).
cnf(2417,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| abstraction(w,u) ),
inference(res,[status(thm),theory(equality)],[940,1046]),
[iquote('0:Res:940.2,1046.0')] ).
cnf(2378,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[908,1034]),
[iquote('0:Res:908.2,1034.0')] ).
cnf(2377,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[928,1034]),
[iquote('0:Res:928.2,1034.0')] ).
cnf(2331,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1093,1022]),
[iquote('0:Res:1093.2,1022.0')] ).
cnf(2297,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[985,1004]),
[iquote('0:Res:985.2,1004.0')] ).
cnf(2234,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relation(w,u) ),
inference(res,[status(thm),theory(equality)],[1171,929]),
[iquote('0:Res:1171.2,929.0')] ).
cnf(2233,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relation(w,u) ),
inference(res,[status(thm),theory(equality)],[1184,929]),
[iquote('0:Res:1184.2,929.0')] ).
cnf(2211,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[1093,892]),
[iquote('0:Res:1093.2,892.0')] ).
cnf(2187,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[985,880]),
[iquote('0:Res:985.2,880.0')] ).
cnf(2176,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[908,865]),
[iquote('0:Res:908.2,865.0')] ).
cnf(2175,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[928,865]),
[iquote('0:Res:928.2,865.0')] ).
cnf(2155,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[1093,855]),
[iquote('0:Res:1093.2,855.0')] ).
cnf(2133,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonexistent(w,u) ),
inference(res,[status(thm),theory(equality)],[1093,841]),
[iquote('0:Res:1093.2,841.0')] ).
cnf(2116,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| existent(w,u) ),
inference(res,[status(thm),theory(equality)],[985,833]),
[iquote('0:Res:985.2,833.0')] ).
cnf(2103,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[908,800]),
[iquote('0:Res:908.2,800.0')] ).
cnf(2102,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[928,800]),
[iquote('0:Res:928.2,800.0')] ).
cnf(2089,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[908,791]),
[iquote('0:Res:908.2,791.0')] ).
cnf(2088,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[928,791]),
[iquote('0:Res:928.2,791.0')] ).
cnf(2073,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1044,781]),
[iquote('0:Res:1044.2,781.0')] ).
cnf(2059,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1103,780]),
[iquote('0:Res:1103.2,780.0')] ).
cnf(2058,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1136,780]),
[iquote('0:Res:1136.2,780.0')] ).
cnf(2051,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1151,779]),
[iquote('0:Res:1151.2,779.0')] ).
cnf(2045,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| impartial(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,764]),
[iquote('0:Res:1064.2,764.0')] ).
cnf(2032,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| living(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,755]),
[iquote('0:Res:1064.2,755.0')] ).
cnf(1985,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| forename(w,u) ),
inference(res,[status(thm),theory(equality)],[1184,54]),
[iquote('0:Res:1184.2,54.0')] ).
cnf(1984,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relname(w,u) ),
inference(res,[status(thm),theory(equality)],[1184,407]),
[iquote('0:Res:1184.2,407.0')] ).
cnf(1958,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| forename(w,u) ),
inference(res,[status(thm),theory(equality)],[1171,54]),
[iquote('0:Res:1171.2,54.0')] ).
cnf(1957,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relname(w,u) ),
inference(res,[status(thm),theory(equality)],[1171,407]),
[iquote('0:Res:1171.2,407.0')] ).
cnf(1926,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| entity(w,u) ),
inference(res,[status(thm),theory(equality)],[1151,47]),
[iquote('0:Res:1151.2,47.0')] ).
cnf(1924,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| existent(w,u) ),
inference(res,[status(thm),theory(equality)],[1151,332]),
[iquote('0:Res:1151.2,332.0')] ).
cnf(1923,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[1151,362]),
[iquote('0:Res:1151.2,362.0')] ).
cnf(1922,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1151,423]),
[iquote('0:Res:1151.2,423.0')] ).
cnf(1911,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonexistent(w,u) ),
inference(res,[status(thm),theory(equality)],[1136,338]),
[iquote('0:Res:1136.2,338.0')] ).
cnf(1910,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[1136,353]),
[iquote('0:Res:1136.2,353.0')] ).
cnf(1909,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[1136,363]),
[iquote('0:Res:1136.2,363.0')] ).
cnf(1908,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1136,424]),
[iquote('0:Res:1136.2,424.0')] ).
cnf(1895,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| eventuality(w,u) ),
inference(res,[status(thm),theory(equality)],[1103,37]),
[iquote('0:Res:1103.2,37.0')] ).
cnf(1891,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonexistent(w,u) ),
inference(res,[status(thm),theory(equality)],[1103,338]),
[iquote('0:Res:1103.2,338.0')] ).
cnf(1890,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[1103,353]),
[iquote('0:Res:1103.2,353.0')] ).
cnf(1889,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[1103,363]),
[iquote('0:Res:1103.2,363.0')] ).
cnf(1888,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1103,424]),
[iquote('0:Res:1103.2,424.0')] ).
cnf(1874,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| event(w,u) ),
inference(res,[status(thm),theory(equality)],[1093,43]),
[iquote('0:Res:1093.2,43.0')] ).
cnf(1870,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| eventuality(w,u) ),
inference(res,[status(thm),theory(equality)],[1093,496]),
[iquote('0:Res:1093.2,496.0')] ).
cnf(1851,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| event(w,u) ),
inference(res,[status(thm),theory(equality)],[1083,43]),
[iquote('0:Res:1083.2,43.0')] ).
cnf(1847,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| eventuality(w,u) ),
inference(res,[status(thm),theory(equality)],[1083,496]),
[iquote('0:Res:1083.2,496.0')] ).
cnf(1821,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| human_person(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,45]),
[iquote('0:Res:1064.2,45.0')] ).
cnf(1819,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| animate(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,261]),
[iquote('0:Res:1064.2,261.0')] ).
cnf(1818,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| human(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,323]),
[iquote('0:Res:1064.2,323.0')] ).
cnf(1816,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| organism(w,u) ),
inference(res,[status(thm),theory(equality)],[1064,418]),
[iquote('0:Res:1064.2,418.0')] ).
cnf(1777,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| abstraction(w,u) ),
inference(res,[status(thm),theory(equality)],[1044,57]),
[iquote('0:Res:1044.2,57.0')] ).
cnf(1776,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[1044,309]),
[iquote('0:Res:1044.2,309.0')] ).
cnf(1775,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[1044,316]),
[iquote('0:Res:1044.2,316.0')] ).
cnf(1774,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[1044,354]),
[iquote('0:Res:1044.2,354.0')] ).
cnf(1773,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1044,425]),
[iquote('0:Res:1044.2,425.0')] ).
cnf(1764,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1035,38]),
[iquote('0:Res:1035.2,38.0')] ).
cnf(1763,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1035,290]),
[iquote('0:Res:1035.2,290.0')] ).
cnf(1755,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1021,38]),
[iquote('0:Res:1021.2,38.0')] ).
cnf(1754,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1021,290]),
[iquote('0:Res:1021.2,290.0')] ).
cnf(1741,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| thing(w,u) ),
inference(res,[status(thm),theory(equality)],[1003,38]),
[iquote('0:Res:1003.2,38.0')] ).
cnf(1740,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[1003,290]),
[iquote('0:Res:1003.2,290.0')] ).
cnf(1715,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| organism(w,u) ),
inference(res,[status(thm),theory(equality)],[985,46]),
[iquote('0:Res:985.2,46.0')] ).
cnf(1714,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| living(w,u) ),
inference(res,[status(thm),theory(equality)],[985,273]),
[iquote('0:Res:985.2,273.0')] ).
cnf(1713,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| impartial(w,u) ),
inference(res,[status(thm),theory(equality)],[985,282]),
[iquote('0:Res:985.2,282.0')] ).
cnf(1711,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| entity(w,u) ),
inference(res,[status(thm),theory(equality)],[985,526]),
[iquote('0:Res:985.2,526.0')] ).
cnf(1702,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| male(w,u) ),
inference(res,[status(thm),theory(equality)],[963,53]),
[iquote('0:Res:963.2,53.0')] ).
cnf(1673,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relname(w,u) ),
inference(res,[status(thm),theory(equality)],[940,55]),
[iquote('0:Res:940.2,55.0')] ).
cnf(1672,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relation(w,u) ),
inference(res,[status(thm),theory(equality)],[940,397]),
[iquote('0:Res:940.2,397.0')] ).
cnf(1642,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relation(w,u) ),
inference(res,[status(thm),theory(equality)],[928,56]),
[iquote('0:Res:928.2,56.0')] ).
cnf(1641,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| abstraction(w,u) ),
inference(res,[status(thm),theory(equality)],[928,443]),
[iquote('0:Res:928.2,443.0')] ).
cnf(1611,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| relation(w,u) ),
inference(res,[status(thm),theory(equality)],[908,56]),
[iquote('0:Res:908.2,56.0')] ).
cnf(1610,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| abstraction(w,u) ),
inference(res,[status(thm),theory(equality)],[908,443]),
[iquote('0:Res:908.2,443.0')] ).
cnf(1591,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[891,40]),
[iquote('0:Res:891.2,40.0')] ).
cnf(1587,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| specific(w,u) ),
inference(res,[status(thm),theory(equality)],[879,40]),
[iquote('0:Res:879.2,40.0')] ).
cnf(1573,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[866,42]),
[iquote('0:Res:866.2,42.0')] ).
cnf(1559,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| unisex(w,u) ),
inference(res,[status(thm),theory(equality)],[854,42]),
[iquote('0:Res:854.2,42.0')] ).
cnf(1555,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonexistent(w,u) ),
inference(res,[status(thm),theory(equality)],[840,41]),
[iquote('0:Res:840.2,41.0')] ).
cnf(2652,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| be(v,skc10,skc13,skc13) ),
inference(res,[status(thm),theory(equality)],[2650,69]),
[iquote('0:Res:2650.1,69.1')] ).
cnf(2066,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1104,780]),
[iquote('0:Res:1104.1,780.0')] ).
cnf(1529,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| existent(w,u) ),
inference(res,[status(thm),theory(equality)],[832,48]),
[iquote('0:Res:832.2,48.0')] ).
cnf(1128,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| nonexistent(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1104,338]),
[iquote('0:Res:1104.1,338.0')] ).
cnf(1127,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| unisex(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1104,353]),
[iquote('0:Res:1104.1,353.0')] ).
cnf(1126,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| specific(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1104,363]),
[iquote('0:Res:1104.1,363.0')] ).
cnf(1125,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1104,424]),
[iquote('0:Res:1104.1,424.0')] ).
cnf(1525,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| human(w,u) ),
inference(res,[status(thm),theory(equality)],[821,51]),
[iquote('0:Res:821.2,51.0')] ).
cnf(1110,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| eventuality(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[474,496]),
[iquote('0:Res:474.1,496.0')] ).
cnf(558,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| event(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[474,43]),
[iquote('0:Res:474.1,43.0')] ).
cnf(551,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| present(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[387,62]),
[iquote('0:Res:387.1,62.0')] ).
cnf(550,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| smoke(v,skf1(w)) ),
inference(res,[status(thm),theory(equality)],[299,61]),
[iquote('0:Res:299.1,61.0')] ).
cnf(1512,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| nonhuman(w,u) ),
inference(res,[status(thm),theory(equality)],[801,58]),
[iquote('0:Res:801.2,58.0')] ).
cnf(4231,plain,
( ~ man(u,v)
| ~ jules_forename(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,3843]),
[iquote('0:Res:19.1,3843.2')] ).
cnf(4203,plain,
( ~ man(u,v)
| ~ vincent_forename(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,3829]),
[iquote('0:Res:19.1,3829.2')] ).
cnf(4158,plain,
( ~ man(u,v)
| ~ forename(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,3535]),
[iquote('0:Res:19.1,3535.2')] ).
cnf(4123,plain,
( ~ man(u,v)
| ~ relname(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,3156]),
[iquote('0:Res:19.1,3156.2')] ).
cnf(1486,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| general(w,u) ),
inference(res,[status(thm),theory(equality)],[792,59]),
[iquote('0:Res:792.2,59.0')] ).
cnf(4087,plain,
( ~ man(u,v)
| ~ proposition(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,3090]),
[iquote('0:Res:19.1,3090.2')] ).
cnf(4059,plain,
( ~ man(u,v)
| ~ relation(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,2407]),
[iquote('0:Res:19.1,2407.2')] ).
cnf(4239,plain,
( ~ man(skc9,u)
| ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v) ),
inference(obv,[status(thm),theory(equality)],[4236]),
[iquote('0:Obv:4236.1')] ).
cnf(4230,plain,
( ~ male(skc9,u)
| ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[120,3843]),
[iquote('0:Res:120.1,3843.2')] ).
cnf(1484,plain,
( ~ thing(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| singleton(w,u) ),
inference(res,[status(thm),theory(equality)],[782,39]),
[iquote('0:Res:782.2,39.0')] ).
cnf(3843,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[3831,31]),
[iquote('0:Res:3831.2,31.0')] ).
cnf(4211,plain,
( ~ man(skc9,u)
| ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v) ),
inference(obv,[status(thm),theory(equality)],[4208]),
[iquote('0:Obv:4208.1')] ).
cnf(4202,plain,
( ~ male(skc9,u)
| ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[120,3829]),
[iquote('0:Res:120.1,3829.2')] ).
cnf(3829,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[3825,31]),
[iquote('0:Res:3825.2,31.0')] ).
cnf(1482,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| impartial(w,u) ),
inference(res,[status(thm),theory(equality)],[765,49]),
[iquote('0:Res:765.2,49.0')] ).
cnf(3586,plain,
( ~ man(u,v)
| ~ abstraction(skc9,v)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,1574]),
[iquote('0:Res:19.1,1574.2')] ).
cnf(4166,plain,
( ~ man(skc9,u)
| ~ forename(skc9,u)
| ~ accessible_world(skc14,v) ),
inference(obv,[status(thm),theory(equality)],[4163]),
[iquote('0:Obv:4163.1')] ).
cnf(4157,plain,
( ~ male(skc9,u)
| ~ forename(skc9,u)
| ~ accessible_world(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[120,3535]),
[iquote('0:Res:120.1,3535.2')] ).
cnf(3535,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[3523,31]),
[iquote('0:Res:3523.2,31.0')] ).
cnf(1475,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| living(w,u) ),
inference(res,[status(thm),theory(equality)],[756,50]),
[iquote('0:Res:756.2,50.0')] ).
cnf(4131,plain,
( ~ man(skc9,u)
| ~ relname(skc9,u)
| ~ accessible_world(skc14,v) ),
inference(obv,[status(thm),theory(equality)],[4128]),
[iquote('0:Obv:4128.1')] ).
cnf(4122,plain,
( ~ male(skc9,u)
| ~ relname(skc9,u)
| ~ accessible_world(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[120,3156]),
[iquote('0:Res:120.1,3156.2')] ).
cnf(3156,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[3093,31]),
[iquote('0:Res:3093.2,31.0')] ).
cnf(4095,plain,
( ~ man(skc9,u)
| ~ proposition(skc9,u)
| ~ accessible_world(skc14,v) ),
inference(obv,[status(thm),theory(equality)],[4092]),
[iquote('0:Obv:4092.1')] ).
cnf(1472,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| animate(w,u) ),
inference(res,[status(thm),theory(equality)],[749,52]),
[iquote('0:Res:749.2,52.0')] ).
cnf(4086,plain,
( ~ male(skc9,u)
| ~ proposition(skc9,u)
| ~ accessible_world(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[120,3090]),
[iquote('0:Res:120.1,3090.2')] ).
cnf(3090,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[3084,31]),
[iquote('0:Res:3084.2,31.0')] ).
cnf(2567,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| of(v,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[2563,66]),
[iquote('0:Res:2563.1,66.1')] ).
cnf(2521,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| of(v,skc16,skc17) ),
inference(res,[status(thm),theory(equality)],[2517,66]),
[iquote('0:Res:2517.1,66.1')] ).
cnf(2882,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skf1(skc13),skc13) ),
inference(mrr,[status(thm)],[2881,84]),
[iquote('0:MRR:2881.0,84.0')] ).
cnf(2510,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| theme(v,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[2505,68]),
[iquote('0:Res:2505.1,68.1')] ).
cnf(2494,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skc15,skc17) ),
inference(res,[status(thm),theory(equality)],[2492,67]),
[iquote('0:Res:2492.1,67.1')] ).
cnf(4067,plain,
( ~ man(skc9,u)
| ~ relation(skc9,u)
| ~ accessible_world(skc14,v) ),
inference(obv,[status(thm),theory(equality)],[4064]),
[iquote('0:Obv:4064.1')] ).
cnf(4058,plain,
( ~ male(skc9,u)
| ~ relation(skc9,u)
| ~ accessible_world(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[120,2407]),
[iquote('0:Res:120.1,2407.2')] ).
cnf(2876,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| agent(v,skf1(skc17),skc17) ),
inference(res,[status(thm),theory(equality)],[187,1203]),
[iquote('0:Res:187.0,1203.0')] ).
cnf(2407,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[2166,31]),
[iquote('0:Res:2166.2,31.0')] ).
cnf(1925,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[1151,235]),
[iquote('0:Res:1151.2,235.0')] ).
cnf(1894,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ existent(v,u) ),
inference(res,[status(thm),theory(equality)],[1103,219]),
[iquote('0:Res:1103.2,219.0')] ).
cnf(1893,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[1103,236]),
[iquote('0:Res:1103.2,236.0')] ).
cnf(1892,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[1103,244]),
[iquote('0:Res:1103.2,244.0')] ).
cnf(1817,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[1064,802]),
[iquote('0:Res:1064.2,802.0')] ).
cnf(1873,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ existent(v,u) ),
inference(res,[status(thm),theory(equality)],[1093,562]),
[iquote('0:Res:1093.2,562.0')] ).
cnf(3917,plain,
( ~ man(skc14,u)
| ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3841]),
[iquote('0:Res:19.1,3841.2')] ).
cnf(1872,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[1093,654]),
[iquote('0:Res:1093.2,654.0')] ).
cnf(3910,plain,
( ~ man(skc14,u)
| ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3827]),
[iquote('0:Res:19.1,3827.2')] ).
cnf(3903,plain,
( ~ man(skc14,u)
| ~ forename(skc9,u)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3533]),
[iquote('0:Res:19.1,3533.2')] ).
cnf(3893,plain,
( ~ man(skc14,u)
| ~ relname(skc9,u)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3154]),
[iquote('0:Res:19.1,3154.2')] ).
cnf(3886,plain,
( ~ man(skc14,u)
| ~ proposition(skc9,u)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3088]),
[iquote('0:Res:19.1,3088.2')] ).
cnf(1871,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[1093,661]),
[iquote('0:Res:1093.2,661.0')] ).
cnf(3879,plain,
( ~ man(skc14,u)
| ~ relation(skc9,u)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,2405]),
[iquote('0:Res:19.1,2405.2')] ).
cnf(3841,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,skc9)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[3831,243]),
[iquote('0:Res:3831.2,243.0')] ).
cnf(3827,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,skc9)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[3825,243]),
[iquote('0:Res:3825.2,243.0')] ).
cnf(3533,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,skc9)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[3523,243]),
[iquote('0:Res:3523.2,243.0')] ).
cnf(1850,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ existent(v,u) ),
inference(res,[status(thm),theory(equality)],[1083,562]),
[iquote('0:Res:1083.2,562.0')] ).
cnf(3154,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,skc9)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[3093,243]),
[iquote('0:Res:3093.2,243.0')] ).
cnf(3088,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,skc9)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[3084,243]),
[iquote('0:Res:3084.2,243.0')] ).
cnf(2405,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,skc9)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[2166,243]),
[iquote('0:Res:2166.2,243.0')] ).
cnf(3870,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[127,3696]),
[iquote('0:Res:127.1,3696.0')] ).
cnf(1849,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[1083,654]),
[iquote('0:Res:1083.2,654.0')] ).
cnf(3696,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[27,3397]),
[iquote('0:Res:27.1,3397.0')] ).
cnf(3866,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[132,3695]),
[iquote('0:Res:132.1,3695.0')] ).
cnf(3695,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[30,3397]),
[iquote('0:Res:30.1,3397.0')] ).
cnf(3853,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[127,3580]),
[iquote('0:Res:127.1,3580.0')] ).
cnf(1848,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[1083,661]),
[iquote('0:Res:1083.2,661.0')] ).
cnf(3580,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[27,3269]),
[iquote('0:Res:27.1,3269.0')] ).
cnf(3848,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[132,3579]),
[iquote('0:Res:132.1,3579.0')] ).
cnf(3579,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[30,3269]),
[iquote('0:Res:30.1,3269.0')] ).
cnf(3831,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[127,3529]),
[iquote('0:Res:127.1,3529.0')] ).
cnf(1820,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[1064,226]),
[iquote('0:Res:1064.2,226.0')] ).
cnf(3529,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[27,3094]),
[iquote('0:Res:27.1,3094.0')] ).
cnf(3825,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[132,3528]),
[iquote('0:Res:132.1,3528.0')] ).
cnf(3528,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[30,3094]),
[iquote('0:Res:30.1,3094.0')] ).
cnf(3798,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[127,3469]),
[iquote('0:Res:127.1,3469.0')] ).
cnf(1712,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[985,650]),
[iquote('0:Res:985.2,650.0')] ).
cnf(3469,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[27,3000]),
[iquote('0:Res:27.1,3000.0')] ).
cnf(3784,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[132,3468]),
[iquote('0:Res:132.1,3468.0')] ).
cnf(3468,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[30,3000]),
[iquote('0:Res:30.1,3000.0')] ).
cnf(3745,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[127,3423]),
[iquote('0:Res:127.1,3423.0')] ).
cnf(1701,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| ~ abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[963,245]),
[iquote('0:Res:963.2,245.1')] ).
cnf(3423,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[27,2936]),
[iquote('0:Res:27.1,2936.0')] ).
cnf(3717,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[132,3422]),
[iquote('0:Res:132.1,3422.0')] ).
cnf(3422,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[30,2936]),
[iquote('0:Res:30.1,2936.0')] ).
cnf(3690,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[121,3397]),
[iquote('0:Res:121.1,3397.0')] ).
cnf(1592,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[891,32]),
[iquote('0:Res:891.2,32.0')] ).
cnf(3397,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[20,2886]),
[iquote('0:Res:20.1,2886.0')] ).
cnf(3680,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[111,3364]),
[iquote('0:Res:111.1,3364.0')] ).
cnf(3364,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[9,2839]),
[iquote('0:Res:9.1,2839.0')] ).
cnf(3635,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[127,3298]),
[iquote('0:Res:127.1,3298.0')] ).
cnf(1588,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| ~ general(v,u) ),
inference(res,[status(thm),theory(equality)],[879,32]),
[iquote('0:Res:879.2,32.0')] ).
cnf(3298,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
inference(res,[status(thm),theory(equality)],[27,2412]),
[iquote('0:Res:27.1,2412.0')] ).
cnf(3602,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[132,3297]),
[iquote('0:Res:132.1,3297.0')] ).
cnf(3297,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
inference(res,[status(thm),theory(equality)],[30,2412]),
[iquote('0:Res:30.1,2412.0')] ).
cnf(3574,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[121,3269]),
[iquote('0:Res:121.1,3269.0')] ).
cnf(1574,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[866,31]),
[iquote('0:Res:866.2,31.0')] ).
cnf(3269,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[20,2370]),
[iquote('0:Res:20.1,2370.0')] ).
cnf(3563,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[111,3240]),
[iquote('0:Res:111.1,3240.0')] ).
cnf(3240,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[9,2295]),
[iquote('0:Res:9.1,2295.0')] ).
cnf(3539,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[111,3133]),
[iquote('0:Res:111.1,3133.0')] ).
cnf(1560,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ male(v,u) ),
inference(res,[status(thm),theory(equality)],[854,31]),
[iquote('0:Res:854.2,31.0')] ).
cnf(3133,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[9,2185]),
[iquote('0:Res:9.1,2185.0')] ).
cnf(3523,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[121,3094]),
[iquote('0:Res:121.1,3094.0')] ).
cnf(3094,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[20,2168]),
[iquote('0:Res:20.1,2168.0')] ).
cnf(3487,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| existent(v,u) ),
inference(res,[status(thm),theory(equality)],[111,3026]),
[iquote('0:Res:111.1,3026.0')] ).
cnf(1556,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| ~ existent(v,u) ),
inference(res,[status(thm),theory(equality)],[840,34]),
[iquote('0:Res:840.2,34.1')] ).
cnf(3026,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| existent(w,v) ),
inference(res,[status(thm),theory(equality)],[9,2114]),
[iquote('0:Res:9.1,2114.0')] ).
cnf(3463,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[121,3000]),
[iquote('0:Res:121.1,3000.0')] ).
cnf(3000,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[20,2095]),
[iquote('0:Res:20.1,2095.0')] ).
cnf(3417,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[121,2936]),
[iquote('0:Res:121.1,2936.0')] ).
cnf(1526,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| ~ nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[821,33]),
[iquote('0:Res:821.2,33.1')] ).
cnf(2936,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[20,2081]),
[iquote('0:Res:20.1,2081.0')] ).
cnf(3396,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[122,2886]),
[iquote('0:Res:122.1,2886.0')] ).
cnf(3395,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,2886]),
[iquote('0:Res:142.0,2886.0')] ).
cnf(3394,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,2886]),
[iquote('0:Res:157.0,2886.0')] ).
cnf(2863,plain,
( ~ proposition(skc9,u)
| ~ theme(skc9,skc15,u)
| equal(u,skc14) ),
inference(res,[status(thm),theory(equality)],[87,202]),
[iquote('0:Res:87.0,202.1')] ).
cnf(2886,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[21,2071]),
[iquote('0:Res:21.1,2071.0')] ).
cnf(3389,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[131,2885]),
[iquote('0:Res:131.1,2885.0')] ).
cnf(2885,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[29,2071]),
[iquote('0:Res:29.1,2071.0')] ).
cnf(3380,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[128,2857]),
[iquote('0:Res:128.1,2857.0')] ).
cnf(2813,plain,
( ~ of(skc9,u,skc13)
| ~ forename(skc14,u)
| equal(u,skc12) ),
inference(mrr,[status(thm)],[2812,84]),
[iquote('0:MRR:2812.1,84.0')] ).
cnf(2857,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[28,2060]),
[iquote('0:Res:28.1,2060.0')] ).
cnf(3365,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[112,2839]),
[iquote('0:Res:112.1,2839.0')] ).
cnf(3363,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,2839]),
[iquote('0:Res:145.0,2839.0')] ).
cnf(3362,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,2839]),
[iquote('0:Res:160.0,2839.0')] ).
cnf(2782,plain,
( ~ of(skc9,u,skc17)
| ~ forename(skc14,u)
| equal(u,skc16) ),
inference(mrr,[status(thm)],[2781,84]),
[iquote('0:MRR:2781.1,84.0')] ).
cnf(2839,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[10,2052]),
[iquote('0:Res:10.1,2052.0')] ).
cnf(3335,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| entity(v,u) ),
inference(res,[status(thm),theory(equality)],[111,2451]),
[iquote('0:Res:111.1,2451.0')] ).
cnf(2451,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| entity(w,v) ),
inference(res,[status(thm),theory(equality)],[9,1150]),
[iquote('0:Res:9.1,1150.0')] ).
cnf(3292,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[121,2412]),
[iquote('0:Res:121.1,2412.0')] ).
cnf(2412,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
inference(res,[status(thm),theory(equality)],[20,1046]),
[iquote('0:Res:20.1,1046.0')] ).
cnf(3268,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[122,2370]),
[iquote('0:Res:122.1,2370.0')] ).
cnf(3263,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[131,2369]),
[iquote('0:Res:131.1,2369.0')] ).
cnf(3267,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,2370]),
[iquote('0:Res:142.0,2370.0')] ).
cnf(3266,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,2370]),
[iquote('0:Res:157.0,2370.0')] ).
cnf(2370,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[21,1034]),
[iquote('0:Res:21.1,1034.0')] ).
cnf(2369,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[29,1034]),
[iquote('0:Res:29.1,1034.0')] ).
cnf(3250,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[128,2327]),
[iquote('0:Res:128.1,2327.0')] ).
cnf(3241,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[112,2295]),
[iquote('0:Res:112.1,2295.0')] ).
cnf(3239,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,2295]),
[iquote('0:Res:145.0,2295.0')] ).
cnf(2327,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[28,1022]),
[iquote('0:Res:28.1,1022.0')] ).
cnf(3238,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,2295]),
[iquote('0:Res:160.0,2295.0')] ).
cnf(2295,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[10,1004]),
[iquote('0:Res:10.1,1004.0')] ).
cnf(3171,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| relation(v,u) ),
inference(res,[status(thm),theory(equality)],[127,2232]),
[iquote('0:Res:127.1,2232.0')] ).
cnf(3169,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| relation(v,u) ),
inference(res,[status(thm),theory(equality)],[132,2231]),
[iquote('0:Res:132.1,2231.0')] ).
cnf(2232,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| relation(w,v) ),
inference(res,[status(thm),theory(equality)],[27,929]),
[iquote('0:Res:27.1,929.0')] ).
cnf(2231,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| relation(w,v) ),
inference(res,[status(thm),theory(equality)],[30,929]),
[iquote('0:Res:30.1,929.0')] ).
cnf(3150,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[128,2207]),
[iquote('0:Res:128.1,2207.0')] ).
cnf(3134,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[112,2185]),
[iquote('0:Res:112.1,2185.0')] ).
cnf(3093,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[122,2168]),
[iquote('0:Res:122.1,2168.0')] ).
cnf(2207,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[28,892]),
[iquote('0:Res:28.1,892.0')] ).
cnf(3126,plain,
( ~ man(u,skc12)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[19,3109]),
[iquote('0:Res:19.1,3109.1')] ).
cnf(3119,plain,
( ~ man(u,skc16)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[19,3105]),
[iquote('0:Res:19.1,3105.1')] ).
cnf(3132,plain,
( ~ accessible_world(skc9,u)
| specific(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,2185]),
[iquote('0:Res:145.0,2185.0')] ).
cnf(3131,plain,
( ~ accessible_world(skc9,u)
| specific(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,2185]),
[iquote('0:Res:160.0,2185.0')] ).
cnf(2185,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[10,880]),
[iquote('0:Res:10.1,880.0')] ).
cnf(3129,plain,
~ man(skc9,skc12),
inference(res,[status(thm),theory(equality)],[19,3128]),
[iquote('0:Res:19.1,3128.0')] ).
cnf(3128,plain,
~ male(skc9,skc12),
inference(mrr,[status(thm)],[3125,84]),
[iquote('0:MRR:3125.1,84.0')] ).
cnf(3109,plain,
( ~ accessible_world(skc9,u)
| ~ male(u,skc12) ),
inference(res,[status(thm),theory(equality)],[3092,31]),
[iquote('0:Res:3092.1,31.0')] ).
cnf(3122,plain,
~ man(skc9,skc16),
inference(res,[status(thm),theory(equality)],[19,3121]),
[iquote('0:Res:19.1,3121.0')] ).
cnf(1204,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,v)
| ~ think_believe_consider(v,w)
| ~ think_believe_consider(v,skf1(u))
| ~ proposition(v,x)
| ~ proposition(v,y)
| ~ agent(v,w,u)
| ~ theme(v,w,x)
| ~ theme(v,skf1(u),y)
| equal(y,x) ),
inference(res,[status(thm),theory(equality)],[587,71]),
[iquote('0:Res:587.2,71.4')] ).
cnf(3121,plain,
~ male(skc9,skc16),
inference(mrr,[status(thm)],[3118,84]),
[iquote('0:MRR:3118.1,84.0')] ).
cnf(3105,plain,
( ~ accessible_world(skc9,u)
| ~ male(u,skc16) ),
inference(res,[status(thm),theory(equality)],[3091,31]),
[iquote('0:Res:3091.1,31.0')] ).
cnf(1336,plain,
( ~ theme(skc9,skf1(u),v)
| ~ man(skc14,u)
| ~ think_believe_consider(skc14,w)
| ~ think_believe_consider(skc14,skf1(u))
| ~ proposition(skc14,x)
| ~ proposition(skc14,v)
| ~ agent(skc14,w,u)
| ~ theme(skc14,w,x)
| equal(v,x) ),
inference(res,[status(thm),theory(equality)],[102,645]),
[iquote('0:Res:102.1,645.7')] ).
cnf(3114,plain,
( ~ man(skc14,skc12)
| ~ accessible_world(skc9,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3107]),
[iquote('0:Res:19.1,3107.1')] ).
cnf(3111,plain,
( ~ man(skc14,skc16)
| ~ accessible_world(skc9,skc9) ),
inference(res,[status(thm),theory(equality)],[19,3103]),
[iquote('0:Res:19.1,3103.1')] ).
cnf(3107,plain,
( ~ accessible_world(skc9,skc9)
| ~ male(skc14,skc12) ),
inference(res,[status(thm),theory(equality)],[3092,243]),
[iquote('0:Res:3092.1,243.0')] ).
cnf(3103,plain,
( ~ accessible_world(skc9,skc9)
| ~ male(skc14,skc16) ),
inference(res,[status(thm),theory(equality)],[3091,243]),
[iquote('0:Res:3091.1,243.0')] ).
cnf(1319,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,skc9)
| ~ think_believe_consider(skc9,skf1(u))
| ~ proposition(skc9,v)
| ~ proposition(skc9,w)
| ~ theme(skc9,skf1(u),w)
| ~ agent(skc9,skc15,u)
| ~ theme(skc9,skc15,v)
| equal(w,v) ),
inference(res,[status(thm),theory(equality)],[587,150]),
[iquote('0:Res:587.2,150.3')] ).
cnf(3092,plain,
( ~ accessible_world(skc9,u)
| unisex(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,2168]),
[iquote('0:Res:142.0,2168.0')] ).
cnf(3091,plain,
( ~ accessible_world(skc9,u)
| unisex(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,2168]),
[iquote('0:Res:157.0,2168.0')] ).
cnf(2168,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[21,865]),
[iquote('0:Res:21.1,865.0')] ).
cnf(3084,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[131,2167]),
[iquote('0:Res:131.1,2167.0')] ).
cnf(1311,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,skc9)
| ~ think_believe_consider(skc9,v)
| ~ think_believe_consider(skc9,skf1(u))
| ~ proposition(skc9,w)
| ~ agent(skc9,v,u)
| ~ theme(skc9,skf1(u),w)
| ~ theme(skc9,v,skc14)
| equal(w,skc14) ),
inference(res,[status(thm),theory(equality)],[587,97]),
[iquote('0:Res:587.2,97.3')] ).
cnf(2167,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[29,865]),
[iquote('0:Res:29.1,865.0')] ).
cnf(3076,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[128,2151]),
[iquote('0:Res:128.1,2151.0')] ).
cnf(2151,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[28,855]),
[iquote('0:Res:28.1,855.0')] ).
cnf(3064,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| nonexistent(v,u) ),
inference(res,[status(thm),theory(equality)],[128,2129]),
[iquote('0:Res:128.1,2129.0')] ).
cnf(705,plain,
( ~ agent(skc9,u,v)
| ~ think_believe_consider(skc14,w)
| ~ think_believe_consider(skc14,u)
| ~ proposition(skc14,x)
| ~ proposition(skc14,y)
| ~ agent(skc14,w,v)
| ~ theme(skc14,w,x)
| ~ theme(skc14,u,y)
| equal(y,x) ),
inference(res,[status(thm),theory(equality)],[101,71]),
[iquote('0:Res:101.1,71.4')] ).
cnf(2129,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| nonexistent(w,v) ),
inference(res,[status(thm),theory(equality)],[28,841]),
[iquote('0:Res:28.1,841.0')] ).
cnf(3027,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| existent(v,u) ),
inference(res,[status(thm),theory(equality)],[112,2114]),
[iquote('0:Res:112.1,2114.0')] ).
cnf(3025,plain,
( ~ accessible_world(skc9,u)
| existent(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,2114]),
[iquote('0:Res:145.0,2114.0')] ).
cnf(3024,plain,
( ~ accessible_world(skc9,u)
| existent(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,2114]),
[iquote('0:Res:160.0,2114.0')] ).
cnf(646,plain,
( ~ accessible_world(skc9,u)
| ~ think_believe_consider(u,v)
| ~ proposition(u,w)
| ~ proposition(u,x)
| ~ agent(u,v,skc17)
| ~ theme(u,v,w)
| ~ theme(u,skc15,x)
| equal(x,w) ),
inference(mrr,[status(thm)],[644,148]),
[iquote('0:MRR:644.2,148.1')] ).
cnf(2114,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| existent(w,v) ),
inference(res,[status(thm),theory(equality)],[10,833]),
[iquote('0:Res:10.1,833.0')] ).
cnf(2999,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[122,2095]),
[iquote('0:Res:122.1,2095.0')] ).
cnf(2998,plain,
( ~ accessible_world(skc9,u)
| nonhuman(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,2095]),
[iquote('0:Res:142.0,2095.0')] ).
cnf(2997,plain,
( ~ accessible_world(skc9,u)
| nonhuman(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,2095]),
[iquote('0:Res:157.0,2095.0')] ).
cnf(1280,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,skc9)
| ~ think_believe_consider(skc9,skf1(u))
| ~ proposition(skc9,v)
| ~ theme(skc9,skf1(u),v)
| ~ agent(skc9,skc15,u)
| equal(v,skc14) ),
inference(res,[status(thm),theory(equality)],[587,186]),
[iquote('0:Res:587.2,186.2')] ).
cnf(2095,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[21,800]),
[iquote('0:Res:21.1,800.0')] ).
cnf(2982,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[131,2094]),
[iquote('0:Res:131.1,2094.0')] ).
cnf(2094,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[29,800]),
[iquote('0:Res:29.1,800.0')] ).
cnf(2935,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[122,2081]),
[iquote('0:Res:122.1,2081.0')] ).
cnf(721,plain,
( ~ of(skc9,u,v)
| ~ entity(skc14,v)
| ~ forename(skc14,w)
| ~ forename(skc14,u)
| ~ of(skc14,w,v)
| equal(w,u) ),
inference(res,[status(thm),theory(equality)],[100,70]),
[iquote('0:Res:100.1,70.3')] ).
cnf(2934,plain,
( ~ accessible_world(skc9,u)
| general(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,2081]),
[iquote('0:Res:142.0,2081.0')] ).
cnf(2933,plain,
( ~ accessible_world(skc9,u)
| general(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,2081]),
[iquote('0:Res:157.0,2081.0')] ).
cnf(2081,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[21,791]),
[iquote('0:Res:21.1,791.0')] ).
cnf(2901,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[131,2080]),
[iquote('0:Res:131.1,2080.0')] ).
cnf(203,plain,
( ~ proposition(skc9,u)
| ~ proposition(skc9,v)
| ~ theme(skc9,skc15,u)
| ~ theme(skc9,skc15,v)
| equal(v,u) ),
inference(mrr,[status(thm)],[201,87]),
[iquote('0:MRR:201.4,87.0')] ).
cnf(2080,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[29,791]),
[iquote('0:Res:29.1,791.0')] ).
cnf(2884,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[123,2071]),
[iquote('0:Res:123.1,2071.0')] ).
cnf(2883,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,2071]),
[iquote('0:Res:96.0,2071.0')] ).
cnf(2071,plain,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[22,781]),
[iquote('0:Res:22.1,781.0')] ).
cnf(1203,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,v)
| ~ accessible_world(v,w)
| agent(w,skf1(u),u) ),
inference(res,[status(thm),theory(equality)],[587,67]),
[iquote('0:Res:587.2,67.1')] ).
cnf(2871,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[103,2061]),
[iquote('0:Res:103.1,2061.0')] ).
cnf(2061,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[1,780]),
[iquote('0:Res:1.1,780.0')] ).
cnf(2852,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[110,2060]),
[iquote('0:Res:110.1,2060.0')] ).
cnf(2853,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,2060]),
[iquote('0:Res:214.0,2060.0')] ).
cnf(2060,plain,
( ~ event(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[8,780]),
[iquote('0:Res:8.1,780.0')] ).
cnf(2840,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[113,2052]),
[iquote('0:Res:113.1,2052.0')] ).
cnf(2052,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[11,779]),
[iquote('0:Res:11.1,779.0')] ).
cnf(2829,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| impartial(v,u) ),
inference(res,[status(thm),theory(equality)],[111,2039]),
[iquote('0:Res:111.1,2039.0')] ).
cnf(188,plain,
( ~ entity(skc9,u)
| ~ of(skc9,skc16,u)
| ~ of(skc9,skc12,u)
| equal(skc12,skc16) ),
inference(res,[status(thm),theory(equality)],[74,143]),
[iquote('0:Res:74.0,143.0')] ).
cnf(2039,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| impartial(w,v) ),
inference(res,[status(thm),theory(equality)],[9,764]),
[iquote('0:Res:9.1,764.0')] ).
cnf(2819,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| living(v,u) ),
inference(res,[status(thm),theory(equality)],[111,2026]),
[iquote('0:Res:111.1,2026.0')] ).
cnf(2026,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| living(w,v) ),
inference(res,[status(thm),theory(equality)],[9,755]),
[iquote('0:Res:9.1,755.0')] ).
cnf(2808,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,2470]),
[iquote('0:Res:84.0,2470.0')] ).
cnf(2459,plain,
( ~ accessible_world(skc9,u)
| ~ forename(u,v)
| ~ of(u,v,skc13)
| equal(v,skc12) ),
inference(mrr,[status(thm)],[633,2450]),
[iquote('0:MRR:633.1,2450.1')] ).
cnf(2470,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc13) ),
inference(res,[status(thm),theory(equality)],[2450,779]),
[iquote('0:Res:2450.1,779.0')] ).
cnf(2805,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,2462]),
[iquote('0:Res:84.0,2462.0')] ).
cnf(2462,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc17) ),
inference(res,[status(thm),theory(equality)],[2449,779]),
[iquote('0:Res:2449.1,779.0')] ).
cnf(2452,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| entity(v,u) ),
inference(res,[status(thm),theory(equality)],[112,1150]),
[iquote('0:Res:112.1,1150.0')] ).
cnf(2458,plain,
( ~ accessible_world(skc9,u)
| ~ forename(u,v)
| ~ of(u,v,skc17)
| equal(v,skc16) ),
inference(mrr,[status(thm)],[634,2449]),
[iquote('0:MRR:634.1,2449.1')] ).
cnf(2439,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| eventuality(v,u) ),
inference(res,[status(thm),theory(equality)],[128,1108]),
[iquote('0:Res:128.1,1108.0')] ).
cnf(2762,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,2429]),
[iquote('0:Res:84.0,2429.0')] ).
cnf(2429,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc12) ),
inference(res,[status(thm),theory(equality)],[2410,781]),
[iquote('0:Res:2410.1,781.0')] ).
cnf(2756,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,2422]),
[iquote('0:Res:84.0,2422.0')] ).
cnf(739,plain,
( ~ be(skc9,u,v,w)
| ~ accessible_world(skc14,x)
| be(x,u,v,w) ),
inference(res,[status(thm),theory(equality)],[99,69]),
[iquote('0:Res:99.1,69.1')] ).
cnf(2422,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc16) ),
inference(res,[status(thm),theory(equality)],[2409,781]),
[iquote('0:Res:2409.1,781.0')] ).
cnf(2411,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[122,1046]),
[iquote('0:Res:122.1,1046.0')] ).
cnf(2393,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[131,1045]),
[iquote('0:Res:131.1,1045.0')] ).
cnf(2684,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,2376]),
[iquote('0:Res:84.0,2376.0')] ).
cnf(720,plain,
( ~ of(skc9,u,v)
| ~ accessible_world(skc14,w)
| of(w,u,v) ),
inference(res,[status(thm),theory(equality)],[100,66]),
[iquote('0:Res:100.1,66.1')] ).
cnf(2376,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc12) ),
inference(res,[status(thm),theory(equality)],[927,1034]),
[iquote('0:Res:927.1,1034.0')] ).
cnf(2680,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,2374]),
[iquote('0:Res:84.0,2374.0')] ).
cnf(2374,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc16) ),
inference(res,[status(thm),theory(equality)],[926,1034]),
[iquote('0:Res:926.1,1034.0')] ).
cnf(2368,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[123,1034]),
[iquote('0:Res:123.1,1034.0')] ).
cnf(715,plain,
( ~ theme(skc9,u,v)
| ~ accessible_world(skc14,w)
| theme(w,u,v) ),
inference(res,[status(thm),theory(equality)],[102,68]),
[iquote('0:Res:102.1,68.1')] ).
cnf(2344,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[103,1023]),
[iquote('0:Res:103.1,1023.0')] ).
cnf(2322,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[110,1022]),
[iquote('0:Res:110.1,1022.0')] ).
cnf(2664,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,2301]),
[iquote('0:Res:84.0,2301.0')] ).
cnf(2301,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc13) ),
inference(res,[status(thm),theory(equality)],[983,1004]),
[iquote('0:Res:983.1,1004.0')] ).
cnf(704,plain,
( ~ agent(skc9,u,v)
| ~ accessible_world(skc14,w)
| agent(w,u,v) ),
inference(res,[status(thm),theory(equality)],[101,67]),
[iquote('0:Res:101.1,67.1')] ).
cnf(2656,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,2299]),
[iquote('0:Res:84.0,2299.0')] ).
cnf(2299,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc17) ),
inference(res,[status(thm),theory(equality)],[982,1004]),
[iquote('0:Res:982.1,1004.0')] ).
cnf(2296,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[113,1004]),
[iquote('0:Res:113.1,1004.0')] ).
cnf(2650,plain,
( ~ accessible_world(skc14,u)
| be(u,skc10,skc13,skc13) ),
inference(res,[status(thm),theory(equality)],[84,692]),
[iquote('0:Res:84.0,692.0')] ).
cnf(692,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| be(v,skc10,skc13,skc13) ),
inference(res,[status(thm),theory(equality)],[182,69]),
[iquote('0:Res:182.1,69.1')] ).
cnf(2260,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| organism(v,u) ),
inference(res,[status(thm),theory(equality)],[111,984]),
[iquote('0:Res:111.1,984.0')] ).
cnf(2251,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| relname(v,u) ),
inference(res,[status(thm),theory(equality)],[127,945]),
[iquote('0:Res:127.1,945.0')] ).
cnf(2245,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| relname(v,u) ),
inference(res,[status(thm),theory(equality)],[132,944]),
[iquote('0:Res:132.1,944.0')] ).
cnf(2563,plain,
( ~ accessible_world(skc14,u)
| of(u,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[84,611]),
[iquote('0:Res:84.0,611.0')] ).
cnf(611,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| of(v,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[164,66]),
[iquote('0:Res:164.1,66.1')] ).
cnf(2226,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| relation(v,u) ),
inference(res,[status(thm),theory(equality)],[121,929]),
[iquote('0:Res:121.1,929.0')] ).
cnf(2220,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[103,893]),
[iquote('0:Res:103.1,893.0')] ).
cnf(2202,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[110,892]),
[iquote('0:Res:110.1,892.0')] ).
cnf(2517,plain,
( ~ accessible_world(skc14,u)
| of(u,skc16,skc17) ),
inference(res,[status(thm),theory(equality)],[84,610]),
[iquote('0:Res:84.0,610.0')] ).
cnf(610,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| of(v,skc16,skc17) ),
inference(res,[status(thm),theory(equality)],[173,66]),
[iquote('0:Res:173.1,66.1')] ).
cnf(2512,plain,
( ~ accessible_world(skc14,u)
| specific(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,2191]),
[iquote('0:Res:84.0,2191.0')] ).
cnf(2191,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| specific(v,skc13) ),
inference(res,[status(thm),theory(equality)],[983,880]),
[iquote('0:Res:983.1,880.0')] ).
cnf(2505,plain,
( ~ accessible_world(skc14,u)
| theme(u,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[84,596]),
[iquote('0:Res:84.0,596.0')] ).
cnf(2504,plain,
( ~ accessible_world(skc14,u)
| specific(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,2189]),
[iquote('0:Res:84.0,2189.0')] ).
cnf(596,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| theme(v,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[166,68]),
[iquote('0:Res:166.1,68.1')] ).
cnf(2189,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| specific(v,skc17) ),
inference(res,[status(thm),theory(equality)],[982,880]),
[iquote('0:Res:982.1,880.0')] ).
cnf(2186,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[113,880]),
[iquote('0:Res:113.1,880.0')] ).
cnf(2492,plain,
( ~ accessible_world(skc14,u)
| agent(u,skc15,skc17) ),
inference(res,[status(thm),theory(equality)],[84,586]),
[iquote('0:Res:84.0,586.0')] ).
cnf(2487,plain,
( ~ man(u,skc12)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,2481]),
[iquote('0:Res:19.1,2481.1')] ).
cnf(586,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| agent(v,skc15,skc17) ),
inference(res,[status(thm),theory(equality)],[169,67]),
[iquote('0:Res:169.1,67.1')] ).
cnf(2481,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skc12) ),
inference(res,[status(thm),theory(equality)],[2477,31]),
[iquote('0:Res:2477.1,31.0')] ).
cnf(1257,plain,
( ~ entity(skc9,skc17)
| ~ of(skc9,skc12,skc17)
| equal(skc12,skc16) ),
inference(mrr,[status(thm)],[1254,74]),
[iquote('0:MRR:1254.1,74.0')] ).
cnf(2483,plain,
( ~ man(skc14,skc12)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,2479]),
[iquote('0:Res:19.1,2479.1')] ).
cnf(2479,plain,
( ~ accessible_world(skc14,skc9)
| ~ male(skc14,skc12) ),
inference(res,[status(thm),theory(equality)],[2477,243]),
[iquote('0:Res:2477.1,243.0')] ).
cnf(2477,plain,
( ~ accessible_world(skc14,u)
| unisex(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,2174]),
[iquote('0:Res:84.0,2174.0')] ).
cnf(2174,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| unisex(v,skc12) ),
inference(res,[status(thm),theory(equality)],[927,865]),
[iquote('0:Res:927.1,865.0')] ).
cnf(190,plain,
( ~ entity(skc9,skc13)
| ~ of(skc9,skc16,skc13)
| equal(skc12,skc16) ),
inference(res,[status(thm),theory(equality)],[74,184]),
[iquote('0:Res:74.0,184.1')] ).
cnf(2444,plain,
( ~ man(u,skc16)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,2421]),
[iquote('0:Res:19.1,2421.1')] ).
cnf(2450,plain,
( ~ accessible_world(skc9,u)
| entity(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,1150]),
[iquote('0:Res:145.0,1150.0')] ).
cnf(2449,plain,
( ~ accessible_world(skc9,u)
| entity(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,1150]),
[iquote('0:Res:160.0,1150.0')] ).
cnf(1150,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| entity(w,v) ),
inference(res,[status(thm),theory(equality)],[10,526]),
[iquote('0:Res:10.1,526.0')] ).
cnf(2421,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skc16) ),
inference(res,[status(thm),theory(equality)],[2408,31]),
[iquote('0:Res:2408.1,31.0')] ).
cnf(2437,plain,
( ~ man(skc14,skc16)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,2419]),
[iquote('0:Res:19.1,2419.1')] ).
cnf(1108,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| eventuality(w,v) ),
inference(res,[status(thm),theory(equality)],[28,496]),
[iquote('0:Res:28.1,496.0')] ).
cnf(2419,plain,
( ~ accessible_world(skc14,skc9)
| ~ male(skc14,skc16) ),
inference(res,[status(thm),theory(equality)],[2408,243]),
[iquote('0:Res:2408.1,243.0')] ).
cnf(2410,plain,
( ~ accessible_world(skc9,u)
| abstraction(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,1046]),
[iquote('0:Res:142.0,1046.0')] ).
cnf(2409,plain,
( ~ accessible_world(skc9,u)
| abstraction(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,1046]),
[iquote('0:Res:157.0,1046.0')] ).
cnf(2408,plain,
( ~ accessible_world(skc14,u)
| unisex(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,2172]),
[iquote('0:Res:84.0,2172.0')] ).
cnf(1046,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
inference(res,[status(thm),theory(equality)],[21,443]),
[iquote('0:Res:21.1,443.0')] ).
cnf(2172,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| unisex(v,skc16) ),
inference(res,[status(thm),theory(equality)],[926,865]),
[iquote('0:Res:926.1,865.0')] ).
cnf(2166,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[123,865]),
[iquote('0:Res:123.1,865.0')] ).
cnf(2162,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[103,856]),
[iquote('0:Res:103.1,856.0')] ).
cnf(2146,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[110,855]),
[iquote('0:Res:110.1,855.0')] ).
cnf(1045,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
inference(res,[status(thm),theory(equality)],[29,443]),
[iquote('0:Res:29.1,443.0')] ).
cnf(2140,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| nonexistent(v,u) ),
inference(res,[status(thm),theory(equality)],[103,842]),
[iquote('0:Res:103.1,842.0')] ).
cnf(2124,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| nonexistent(v,u) ),
inference(res,[status(thm),theory(equality)],[110,841]),
[iquote('0:Res:110.1,841.0')] ).
cnf(2367,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,1034]),
[iquote('0:Res:96.0,1034.0')] ).
cnf(2366,plain,
( ~ accessible_world(skc14,u)
| existent(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,2120]),
[iquote('0:Res:84.0,2120.0')] ).
cnf(1034,plain,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[22,425]),
[iquote('0:Res:22.1,425.0')] ).
cnf(2120,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| existent(v,skc13) ),
inference(res,[status(thm),theory(equality)],[983,833]),
[iquote('0:Res:983.1,833.0')] ).
cnf(2363,plain,
( ~ accessible_world(skc14,u)
| existent(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,2118]),
[iquote('0:Res:84.0,2118.0')] ).
cnf(2118,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| existent(v,skc17) ),
inference(res,[status(thm),theory(equality)],[982,833]),
[iquote('0:Res:982.1,833.0')] ).
cnf(2115,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| existent(v,u) ),
inference(res,[status(thm),theory(equality)],[113,833]),
[iquote('0:Res:113.1,833.0')] ).
cnf(1023,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[1,424]),
[iquote('0:Res:1.1,424.0')] ).
cnf(2109,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| human(v,u) ),
inference(res,[status(thm),theory(equality)],[111,820]),
[iquote('0:Res:111.1,820.0')] ).
cnf(2336,plain,
( ~ accessible_world(skc14,u)
| nonhuman(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,2101]),
[iquote('0:Res:84.0,2101.0')] ).
cnf(2101,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| nonhuman(v,skc12) ),
inference(res,[status(thm),theory(equality)],[927,800]),
[iquote('0:Res:927.1,800.0')] ).
cnf(2323,plain,
( ~ accessible_world(skc14,u)
| thing(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,1022]),
[iquote('0:Res:214.0,1022.0')] ).
cnf(1022,plain,
( ~ event(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[8,424]),
[iquote('0:Res:8.1,424.0')] ).
cnf(2316,plain,
( ~ accessible_world(skc14,u)
| nonhuman(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,2099]),
[iquote('0:Res:84.0,2099.0')] ).
cnf(2099,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| nonhuman(v,skc16) ),
inference(res,[status(thm),theory(equality)],[926,800]),
[iquote('0:Res:926.1,800.0')] ).
cnf(2093,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[123,800]),
[iquote('0:Res:123.1,800.0')] ).
cnf(2294,plain,
( ~ accessible_world(skc14,u)
| general(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,2087]),
[iquote('0:Res:84.0,2087.0')] ).
cnf(1004,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[11,423]),
[iquote('0:Res:11.1,423.0')] ).
cnf(2087,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| general(v,skc12) ),
inference(res,[status(thm),theory(equality)],[927,791]),
[iquote('0:Res:927.1,791.0')] ).
cnf(2291,plain,
( ~ accessible_world(skc14,u)
| general(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,2085]),
[iquote('0:Res:84.0,2085.0')] ).
cnf(2085,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| general(v,skc16) ),
inference(res,[status(thm),theory(equality)],[926,791]),
[iquote('0:Res:926.1,791.0')] ).
cnf(2079,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[123,791]),
[iquote('0:Res:123.1,791.0')] ).
cnf(984,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| organism(w,v) ),
inference(res,[status(thm),theory(equality)],[9,418]),
[iquote('0:Res:9.1,418.0')] ).
cnf(2077,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1859,781]),
[iquote('0:Res:1859.1,781.0')] ).
cnf(2076,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc16) ),
inference(res,[status(thm),theory(equality)],[1852,781]),
[iquote('0:Res:1852.1,781.0')] ).
cnf(2254,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc14) ),
inference(res,[status(thm),theory(equality)],[84,2075]),
[iquote('0:Res:84.0,2075.0')] ).
cnf(2075,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1043,781]),
[iquote('0:Res:1043.1,781.0')] ).
cnf(945,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| relname(w,v) ),
inference(res,[status(thm),theory(equality)],[27,407]),
[iquote('0:Res:27.1,407.0')] ).
cnf(2072,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[124,781]),
[iquote('0:Res:124.1,781.0')] ).
cnf(2057,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[104,780]),
[iquote('0:Res:104.1,780.0')] ).
cnf(2054,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc13) ),
inference(res,[status(thm),theory(equality)],[2016,779]),
[iquote('0:Res:2016.1,779.0')] ).
cnf(2053,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc17) ),
inference(res,[status(thm),theory(equality)],[2008,779]),
[iquote('0:Res:2008.1,779.0')] ).
cnf(944,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| relname(w,v) ),
inference(res,[status(thm),theory(equality)],[30,407]),
[iquote('0:Res:30.1,407.0')] ).
cnf(2050,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[114,779]),
[iquote('0:Res:114.1,779.0')] ).
cnf(2040,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| impartial(v,u) ),
inference(res,[status(thm),theory(equality)],[112,764]),
[iquote('0:Res:112.1,764.0')] ).
cnf(2027,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| living(v,u) ),
inference(res,[status(thm),theory(equality)],[112,755]),
[iquote('0:Res:112.1,755.0')] ).
cnf(2021,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| existent(v,skc13) ),
inference(res,[status(thm),theory(equality)],[2016,332]),
[iquote('0:Res:2016.1,332.0')] ).
cnf(929,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| relation(w,v) ),
inference(res,[status(thm),theory(equality)],[20,397]),
[iquote('0:Res:20.1,397.0')] ).
cnf(2020,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| specific(v,skc13) ),
inference(res,[status(thm),theory(equality)],[2016,362]),
[iquote('0:Res:2016.1,362.0')] ).
cnf(2019,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc13) ),
inference(res,[status(thm),theory(equality)],[2016,423]),
[iquote('0:Res:2016.1,423.0')] ).
cnf(2013,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| existent(v,skc17) ),
inference(res,[status(thm),theory(equality)],[2008,332]),
[iquote('0:Res:2008.1,332.0')] ).
cnf(2012,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| specific(v,skc17) ),
inference(res,[status(thm),theory(equality)],[2008,362]),
[iquote('0:Res:2008.1,362.0')] ).
cnf(893,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[1,363]),
[iquote('0:Res:1.1,363.0')] ).
cnf(2011,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc17) ),
inference(res,[status(thm),theory(equality)],[2008,423]),
[iquote('0:Res:2008.1,423.0')] ).
cnf(2003,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| animate(v,u) ),
inference(res,[status(thm),theory(equality)],[111,748]),
[iquote('0:Res:111.1,748.0')] ).
cnf(1876,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1875,290]),
[iquote('0:Res:1875.1,290.0')] ).
cnf(2203,plain,
( ~ accessible_world(skc14,u)
| specific(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,892]),
[iquote('0:Res:214.0,892.0')] ).
cnf(892,plain,
( ~ event(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[8,363]),
[iquote('0:Res:8.1,363.0')] ).
cnf(2193,plain,
( ~ man(u,skc14)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[19,2180]),
[iquote('0:Res:19.1,2180.1')] ).
cnf(2196,plain,
~ man(skc9,skc14),
inference(res,[status(thm),theory(equality)],[19,2195]),
[iquote('0:Res:19.1,2195.0')] ).
cnf(2195,plain,
~ male(skc9,skc14),
inference(mrr,[status(thm)],[2192,84]),
[iquote('0:MRR:2192.1,84.0')] ).
cnf(2180,plain,
( ~ accessible_world(skc9,u)
| ~ male(u,skc14) ),
inference(res,[status(thm),theory(equality)],[2165,31]),
[iquote('0:Res:2165.1,31.0')] ).
cnf(880,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[11,362]),
[iquote('0:Res:11.1,362.0')] ).
cnf(2182,plain,
( ~ man(skc14,skc14)
| ~ accessible_world(skc9,skc9) ),
inference(res,[status(thm),theory(equality)],[19,2178]),
[iquote('0:Res:19.1,2178.1')] ).
cnf(2178,plain,
( ~ accessible_world(skc9,skc9)
| ~ male(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[2165,243]),
[iquote('0:Res:2165.1,243.0')] ).
cnf(2165,plain,
( ~ accessible_world(skc9,u)
| unisex(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,865]),
[iquote('0:Res:96.0,865.0')] ).
cnf(865,plain,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[22,354]),
[iquote('0:Res:22.1,354.0')] ).
cnf(1863,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| general(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1859,309]),
[iquote('0:Res:1859.1,309.0')] ).
cnf(1862,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| nonhuman(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1859,316]),
[iquote('0:Res:1859.1,316.0')] ).
cnf(1861,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| unisex(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1859,354]),
[iquote('0:Res:1859.1,354.0')] ).
cnf(1860,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1859,425]),
[iquote('0:Res:1859.1,425.0')] ).
cnf(856,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[1,353]),
[iquote('0:Res:1.1,353.0')] ).
cnf(1856,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| general(v,skc16) ),
inference(res,[status(thm),theory(equality)],[1852,309]),
[iquote('0:Res:1852.1,309.0')] ).
cnf(1855,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| nonhuman(v,skc16) ),
inference(res,[status(thm),theory(equality)],[1852,316]),
[iquote('0:Res:1852.1,316.0')] ).
cnf(1854,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| unisex(v,skc16) ),
inference(res,[status(thm),theory(equality)],[1852,354]),
[iquote('0:Res:1852.1,354.0')] ).
cnf(2147,plain,
( ~ accessible_world(skc14,u)
| unisex(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,855]),
[iquote('0:Res:214.0,855.0')] ).
cnf(855,plain,
( ~ event(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[8,353]),
[iquote('0:Res:8.1,353.0')] ).
cnf(1853,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc16) ),
inference(res,[status(thm),theory(equality)],[1852,425]),
[iquote('0:Res:1852.1,425.0')] ).
cnf(1840,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| general(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1836,309]),
[iquote('0:Res:1836.1,309.0')] ).
cnf(1839,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| nonhuman(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1836,316]),
[iquote('0:Res:1836.1,316.0')] ).
cnf(1838,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| unisex(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1836,354]),
[iquote('0:Res:1836.1,354.0')] ).
cnf(842,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| nonexistent(w,v) ),
inference(res,[status(thm),theory(equality)],[1,338]),
[iquote('0:Res:1.1,338.0')] ).
cnf(1837,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1836,425]),
[iquote('0:Res:1836.1,425.0')] ).
cnf(1804,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1803,290]),
[iquote('0:Res:1803.1,290.0')] ).
cnf(1770,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| singleton(v,skc15) ),
inference(res,[status(thm),theory(equality)],[1769,290]),
[iquote('0:Res:1769.1,290.0')] ).
cnf(2125,plain,
( ~ accessible_world(skc14,u)
| nonexistent(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,841]),
[iquote('0:Res:214.0,841.0')] ).
cnf(841,plain,
( ~ event(u,v)
| ~ accessible_world(u,w)
| nonexistent(w,v) ),
inference(res,[status(thm),theory(equality)],[8,338]),
[iquote('0:Res:8.1,338.0')] ).
cnf(1747,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| living(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1743,273]),
[iquote('0:Res:1743.1,273.0')] ).
cnf(1746,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| impartial(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1743,282]),
[iquote('0:Res:1743.1,282.0')] ).
cnf(1744,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| entity(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1743,526]),
[iquote('0:Res:1743.1,526.0')] ).
cnf(1736,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| living(v,skc17) ),
inference(res,[status(thm),theory(equality)],[1732,273]),
[iquote('0:Res:1732.1,273.0')] ).
cnf(833,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| existent(w,v) ),
inference(res,[status(thm),theory(equality)],[11,332]),
[iquote('0:Res:11.1,332.0')] ).
cnf(1735,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| impartial(v,skc17) ),
inference(res,[status(thm),theory(equality)],[1732,282]),
[iquote('0:Res:1732.1,282.0')] ).
cnf(1733,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| entity(v,skc17) ),
inference(res,[status(thm),theory(equality)],[1732,526]),
[iquote('0:Res:1732.1,526.0')] ).
cnf(1690,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| abstraction(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1688,443]),
[iquote('0:Res:1688.1,443.0')] ).
cnf(1659,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| abstraction(v,skc16) ),
inference(res,[status(thm),theory(equality)],[1657,443]),
[iquote('0:Res:1657.1,443.0')] ).
cnf(820,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| human(w,v) ),
inference(res,[status(thm),theory(equality)],[9,323]),
[iquote('0:Res:9.1,323.0')] ).
cnf(1457,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| proposition(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1453,64]),
[iquote('0:Res:1453.1,64.0')] ).
cnf(1450,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| man(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1435,44]),
[iquote('0:Res:1435.1,44.0')] ).
cnf(1422,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| nonexistent(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1408,338]),
[iquote('0:Res:1408.1,338.0')] ).
cnf(2092,plain,
( ~ accessible_world(skc9,u)
| nonhuman(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,800]),
[iquote('0:Res:96.0,800.0')] ).
cnf(800,plain,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[22,316]),
[iquote('0:Res:22.1,316.0')] ).
cnf(1421,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| unisex(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1408,353]),
[iquote('0:Res:1408.1,353.0')] ).
cnf(1420,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| specific(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1408,363]),
[iquote('0:Res:1408.1,363.0')] ).
cnf(1419,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1408,424]),
[iquote('0:Res:1408.1,424.0')] ).
cnf(2078,plain,
( ~ accessible_world(skc9,u)
| general(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,791]),
[iquote('0:Res:96.0,791.0')] ).
cnf(791,plain,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[22,309]),
[iquote('0:Res:22.1,309.0')] ).
cnf(1376,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| human_person(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1363,45]),
[iquote('0:Res:1363.1,45.0')] ).
cnf(1374,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| animate(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1363,261]),
[iquote('0:Res:1363.1,261.0')] ).
cnf(1373,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| human(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1363,323]),
[iquote('0:Res:1363.1,323.0')] ).
cnf(1371,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| organism(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1363,418]),
[iquote('0:Res:1363.1,418.0')] ).
cnf(781,plain,
( ~ abstraction(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[23,290]),
[iquote('0:Res:23.1,290.0')] ).
cnf(1331,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| state(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1320,36]),
[iquote('0:Res:1320.1,36.0')] ).
cnf(1327,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| event(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1320,476]),
[iquote('0:Res:1320.1,476.0')] ).
cnf(2056,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,780]),
[iquote('0:Res:133.0,780.0')] ).
cnf(2055,plain,
( ~ accessible_world(skc9,u)
| singleton(u,skc15) ),
inference(res,[status(thm),theory(equality)],[152,780]),
[iquote('0:Res:152.0,780.0')] ).
cnf(780,plain,
( ~ eventuality(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[2,290]),
[iquote('0:Res:2.1,290.0')] ).
cnf(1326,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| eventuality(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1320,497]),
[iquote('0:Res:1320.1,497.0')] ).
cnf(1252,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| male(v,skc13) ),
inference(res,[status(thm),theory(equality)],[1243,53]),
[iquote('0:Res:1243.1,53.0')] ).
cnf(1241,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| relname(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1234,55]),
[iquote('0:Res:1234.1,55.0')] ).
cnf(1240,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| relation(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1234,397]),
[iquote('0:Res:1234.1,397.0')] ).
cnf(779,plain,
( ~ entity(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[12,290]),
[iquote('0:Res:12.1,290.0')] ).
cnf(1224,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| relation(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1216,56]),
[iquote('0:Res:1216.1,56.0')] ).
cnf(1223,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| abstraction(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1216,443]),
[iquote('0:Res:1216.1,443.0')] ).
cnf(2038,plain,
( ~ accessible_world(skc9,u)
| impartial(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,764]),
[iquote('0:Res:145.0,764.0')] ).
cnf(2037,plain,
( ~ accessible_world(skc9,u)
| impartial(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,764]),
[iquote('0:Res:160.0,764.0')] ).
cnf(764,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| impartial(w,v) ),
inference(res,[status(thm),theory(equality)],[10,282]),
[iquote('0:Res:10.1,282.0')] ).
cnf(1185,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| forename(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1165,577]),
[iquote('0:Res:1165.1,577.0')] ).
cnf(1173,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| jules_forename(v,skc12) ),
inference(res,[status(thm),theory(equality)],[1165,60]),
[iquote('0:Res:1165.1,60.0')] ).
cnf(2025,plain,
( ~ accessible_world(skc9,u)
| living(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,755]),
[iquote('0:Res:145.0,755.0')] ).
cnf(2024,plain,
( ~ accessible_world(skc9,u)
| living(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,755]),
[iquote('0:Res:160.0,755.0')] ).
cnf(755,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| living(w,v) ),
inference(res,[status(thm),theory(equality)],[10,273]),
[iquote('0:Res:10.1,273.0')] ).
cnf(2016,plain,
( ~ accessible_world(skc14,u)
| entity(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,1153]),
[iquote('0:Res:84.0,1153.0')] ).
cnf(1153,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| entity(v,skc13) ),
inference(res,[status(thm),theory(equality)],[983,526]),
[iquote('0:Res:983.1,526.0')] ).
cnf(2008,plain,
( ~ accessible_world(skc14,u)
| entity(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,1152]),
[iquote('0:Res:84.0,1152.0')] ).
cnf(1152,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| entity(v,skc17) ),
inference(res,[status(thm),theory(equality)],[982,526]),
[iquote('0:Res:982.1,526.0')] ).
cnf(748,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| animate(w,v) ),
inference(res,[status(thm),theory(equality)],[9,261]),
[iquote('0:Res:9.1,261.0')] ).
cnf(1117,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| nonexistent(v,skc15) ),
inference(res,[status(thm),theory(equality)],[1102,338]),
[iquote('0:Res:1102.1,338.0')] ).
cnf(1116,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| unisex(v,skc15) ),
inference(res,[status(thm),theory(equality)],[1102,353]),
[iquote('0:Res:1102.1,353.0')] ).
cnf(1115,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| specific(v,skc15) ),
inference(res,[status(thm),theory(equality)],[1102,363]),
[iquote('0:Res:1102.1,363.0')] ).
cnf(1114,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| thing(v,skc15) ),
inference(res,[status(thm),theory(equality)],[1102,424]),
[iquote('0:Res:1102.1,424.0')] ).
cnf(1184,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| forename(v,u) ),
inference(res,[status(thm),theory(equality)],[127,577]),
[iquote('0:Res:127.1,577.0')] ).
cnf(1105,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| eventuality(v,skc15) ),
inference(res,[status(thm),theory(equality)],[472,496]),
[iquote('0:Res:472.1,496.0')] ).
cnf(1073,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| animate(v,skc17) ),
inference(res,[status(thm),theory(equality)],[1063,261]),
[iquote('0:Res:1063.1,261.0')] ).
cnf(1072,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| human(v,skc17) ),
inference(res,[status(thm),theory(equality)],[1063,323]),
[iquote('0:Res:1063.1,323.0')] ).
cnf(1070,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| organism(v,skc17) ),
inference(res,[status(thm),theory(equality)],[1063,418]),
[iquote('0:Res:1063.1,418.0')] ).
cnf(1171,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| forename(v,u) ),
inference(res,[status(thm),theory(equality)],[132,576]),
[iquote('0:Res:132.1,576.0')] ).
cnf(1065,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| human_person(v,skc17) ),
inference(res,[status(thm),theory(equality)],[534,457]),
[iquote('0:Res:534.1,457.0')] ).
cnf(1943,plain,
( ~ accessible_world(skc14,u)
| general(u,skc14) ),
inference(res,[status(thm),theory(equality)],[84,1053]),
[iquote('0:Res:84.0,1053.0')] ).
cnf(1053,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| general(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1043,309]),
[iquote('0:Res:1043.1,309.0')] ).
cnf(1919,plain,
( ~ accessible_world(skc14,u)
| nonhuman(u,skc14) ),
inference(res,[status(thm),theory(equality)],[84,1052]),
[iquote('0:Res:84.0,1052.0')] ).
cnf(1151,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| entity(v,u) ),
inference(res,[status(thm),theory(equality)],[113,526]),
[iquote('0:Res:113.1,526.0')] ).
cnf(1052,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| nonhuman(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1043,316]),
[iquote('0:Res:1043.1,316.0')] ).
cnf(1901,plain,
( ~ man(u,skc14)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,1883]),
[iquote('0:Res:19.1,1883.1')] ).
cnf(1136,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| eventuality(v,u) ),
inference(res,[status(thm),theory(equality)],[103,497]),
[iquote('0:Res:103.1,497.0')] ).
cnf(1883,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skc14) ),
inference(res,[status(thm),theory(equality)],[1879,31]),
[iquote('0:Res:1879.1,31.0')] ).
cnf(1897,plain,
( ~ man(skc14,skc14)
| ~ accessible_world(skc14,skc9) ),
inference(res,[status(thm),theory(equality)],[19,1881]),
[iquote('0:Res:19.1,1881.1')] ).
cnf(1881,plain,
( ~ accessible_world(skc14,skc9)
| ~ male(skc14,skc14) ),
inference(res,[status(thm),theory(equality)],[1879,243]),
[iquote('0:Res:1879.1,243.0')] ).
cnf(1103,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| eventuality(v,u) ),
inference(res,[status(thm),theory(equality)],[110,496]),
[iquote('0:Res:110.1,496.0')] ).
cnf(1879,plain,
( ~ accessible_world(skc14,u)
| unisex(u,skc14) ),
inference(res,[status(thm),theory(equality)],[84,1051]),
[iquote('0:Res:84.0,1051.0')] ).
cnf(1051,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| unisex(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1043,354]),
[iquote('0:Res:1043.1,354.0')] ).
cnf(1875,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc14) ),
inference(res,[status(thm),theory(equality)],[84,1050]),
[iquote('0:Res:84.0,1050.0')] ).
cnf(1050,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc14) ),
inference(res,[status(thm),theory(equality)],[1043,425]),
[iquote('0:Res:1043.1,425.0')] ).
cnf(1093,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| event(v,u) ),
inference(res,[status(thm),theory(equality)],[128,477]),
[iquote('0:Res:128.1,477.0')] ).
cnf(1859,plain,
( ~ accessible_world(skc14,u)
| abstraction(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,1049]),
[iquote('0:Res:84.0,1049.0')] ).
cnf(1049,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| abstraction(v,skc12) ),
inference(res,[status(thm),theory(equality)],[927,443]),
[iquote('0:Res:927.1,443.0')] ).
cnf(1852,plain,
( ~ accessible_world(skc14,u)
| abstraction(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,1048]),
[iquote('0:Res:84.0,1048.0')] ).
cnf(1048,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| abstraction(v,skc16) ),
inference(res,[status(thm),theory(equality)],[926,443]),
[iquote('0:Res:926.1,443.0')] ).
cnf(1083,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| event(v,u) ),
inference(res,[status(thm),theory(equality)],[103,476]),
[iquote('0:Res:103.1,476.0')] ).
cnf(1836,plain,
( ~ accessible_world(skc14,u)
| abstraction(u,skc14) ),
inference(res,[status(thm),theory(equality)],[84,1047]),
[iquote('0:Res:84.0,1047.0')] ).
cnf(1047,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| abstraction(v,skc14) ),
inference(res,[status(thm),theory(equality)],[394,443]),
[iquote('0:Res:394.1,443.0')] ).
cnf(1833,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc10) ),
inference(res,[status(thm),theory(equality)],[84,1028]),
[iquote('0:Res:84.0,1028.0')] ).
cnf(1028,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc10) ),
inference(res,[status(thm),theory(equality)],[1020,290]),
[iquote('0:Res:1020.1,290.0')] ).
cnf(1064,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| human_person(v,u) ),
inference(res,[status(thm),theory(equality)],[111,457]),
[iquote('0:Res:111.1,457.0')] ).
cnf(1807,plain,
( ~ accessible_world(skc14,u)
| singleton(u,skc15) ),
inference(res,[status(thm),theory(equality)],[84,1026]),
[iquote('0:Res:84.0,1026.0')] ).
cnf(1026,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| singleton(v,skc15) ),
inference(res,[status(thm),theory(equality)],[1019,290]),
[iquote('0:Res:1019.1,290.0')] ).
cnf(1803,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc10) ),
inference(res,[status(thm),theory(equality)],[84,1025]),
[iquote('0:Res:84.0,1025.0')] ).
cnf(1025,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc10) ),
inference(res,[status(thm),theory(equality)],[494,424]),
[iquote('0:Res:494.1,424.0')] ).
cnf(1044,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[123,443]),
[iquote('0:Res:123.1,443.0')] ).
cnf(1769,plain,
( ~ accessible_world(skc14,u)
| thing(u,skc15) ),
inference(res,[status(thm),theory(equality)],[84,1024]),
[iquote('0:Res:84.0,1024.0')] ).
cnf(1024,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| thing(v,skc15) ),
inference(res,[status(thm),theory(equality)],[493,424]),
[iquote('0:Res:493.1,424.0')] ).
cnf(1766,plain,
( ~ accessible_world(skc14,u)
| living(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,995]),
[iquote('0:Res:84.0,995.0')] ).
cnf(995,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| living(v,skc13) ),
inference(res,[status(thm),theory(equality)],[983,273]),
[iquote('0:Res:983.1,273.0')] ).
cnf(1035,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[124,425]),
[iquote('0:Res:124.1,425.0')] ).
cnf(1760,plain,
( ~ accessible_world(skc14,u)
| impartial(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,994]),
[iquote('0:Res:84.0,994.0')] ).
cnf(994,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| impartial(v,skc13) ),
inference(res,[status(thm),theory(equality)],[983,282]),
[iquote('0:Res:983.1,282.0')] ).
cnf(1757,plain,
( ~ accessible_world(skc14,u)
| living(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,990]),
[iquote('0:Res:84.0,990.0')] ).
cnf(990,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| living(v,skc17) ),
inference(res,[status(thm),theory(equality)],[982,273]),
[iquote('0:Res:982.1,273.0')] ).
cnf(1021,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[104,424]),
[iquote('0:Res:104.1,424.0')] ).
cnf(1751,plain,
( ~ accessible_world(skc14,u)
| impartial(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,989]),
[iquote('0:Res:84.0,989.0')] ).
cnf(989,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| impartial(v,skc17) ),
inference(res,[status(thm),theory(equality)],[982,282]),
[iquote('0:Res:982.1,282.0')] ).
cnf(1743,plain,
( ~ accessible_world(skc14,u)
| organism(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,987]),
[iquote('0:Res:84.0,987.0')] ).
cnf(987,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| organism(v,skc13) ),
inference(res,[status(thm),theory(equality)],[456,418]),
[iquote('0:Res:456.1,418.0')] ).
cnf(1003,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[114,423]),
[iquote('0:Res:114.1,423.0')] ).
cnf(1732,plain,
( ~ accessible_world(skc14,u)
| organism(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,986]),
[iquote('0:Res:84.0,986.0')] ).
cnf(986,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| organism(v,skc17) ),
inference(res,[status(thm),theory(equality)],[455,418]),
[iquote('0:Res:455.1,418.0')] ).
cnf(985,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| organism(v,u) ),
inference(res,[status(thm),theory(equality)],[112,418]),
[iquote('0:Res:112.1,418.0')] ).
cnf(964,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| male(v,skc17) ),
inference(res,[status(thm),theory(equality)],[534,416]),
[iquote('0:Res:534.1,416.0')] ).
cnf(963,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| male(v,u) ),
inference(res,[status(thm),theory(equality)],[111,416]),
[iquote('0:Res:111.1,416.0')] ).
cnf(946,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| relation(v,skc16) ),
inference(res,[status(thm),theory(equality)],[939,397]),
[iquote('0:Res:939.1,397.0')] ).
cnf(941,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| relname(v,skc16) ),
inference(res,[status(thm),theory(equality)],[572,407]),
[iquote('0:Res:572.1,407.0')] ).
cnf(1688,plain,
( ~ accessible_world(skc14,u)
| relation(u,skc12) ),
inference(res,[status(thm),theory(equality)],[84,931]),
[iquote('0:Res:84.0,931.0')] ).
cnf(931,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| relation(v,skc12) ),
inference(res,[status(thm),theory(equality)],[405,397]),
[iquote('0:Res:405.1,397.0')] ).
cnf(940,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| relname(v,u) ),
inference(res,[status(thm),theory(equality)],[121,407]),
[iquote('0:Res:121.1,407.0')] ).
cnf(1657,plain,
( ~ accessible_world(skc14,u)
| relation(u,skc16) ),
inference(res,[status(thm),theory(equality)],[84,930]),
[iquote('0:Res:84.0,930.0')] ).
cnf(930,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| relation(v,skc16) ),
inference(res,[status(thm),theory(equality)],[404,397]),
[iquote('0:Res:404.1,397.0')] ).
cnf(928,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| relation(v,u) ),
inference(res,[status(thm),theory(equality)],[122,397]),
[iquote('0:Res:122.1,397.0')] ).
cnf(1598,plain,
( ~ accessible_world(skc14,u)
| specific(u,skc10) ),
inference(res,[status(thm),theory(equality)],[84,895]),
[iquote('0:Res:84.0,895.0')] ).
cnf(908,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| relation(v,u) ),
inference(res,[status(thm),theory(equality)],[131,396]),
[iquote('0:Res:131.1,396.0')] ).
cnf(895,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| specific(v,skc10) ),
inference(res,[status(thm),theory(equality)],[494,363]),
[iquote('0:Res:494.1,363.0')] ).
cnf(1593,plain,
( ~ accessible_world(skc14,u)
| specific(u,skc15) ),
inference(res,[status(thm),theory(equality)],[84,894]),
[iquote('0:Res:84.0,894.0')] ).
cnf(894,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| specific(v,skc15) ),
inference(res,[status(thm),theory(equality)],[493,363]),
[iquote('0:Res:493.1,363.0')] ).
cnf(891,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[104,363]),
[iquote('0:Res:104.1,363.0')] ).
cnf(879,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[114,362]),
[iquote('0:Res:114.1,362.0')] ).
cnf(1580,plain,
( ~ accessible_world(skc14,u)
| unisex(u,skc10) ),
inference(res,[status(thm),theory(equality)],[84,858]),
[iquote('0:Res:84.0,858.0')] ).
cnf(858,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| unisex(v,skc10) ),
inference(res,[status(thm),theory(equality)],[494,353]),
[iquote('0:Res:494.1,353.0')] ).
cnf(1575,plain,
( ~ accessible_world(skc14,u)
| unisex(u,skc15) ),
inference(res,[status(thm),theory(equality)],[84,857]),
[iquote('0:Res:84.0,857.0')] ).
cnf(857,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| unisex(v,skc15) ),
inference(res,[status(thm),theory(equality)],[493,353]),
[iquote('0:Res:493.1,353.0')] ).
cnf(866,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[124,354]),
[iquote('0:Res:124.1,354.0')] ).
cnf(1566,plain,
( ~ accessible_world(skc14,u)
| nonexistent(u,skc10) ),
inference(res,[status(thm),theory(equality)],[84,844]),
[iquote('0:Res:84.0,844.0')] ).
cnf(844,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| nonexistent(v,skc10) ),
inference(res,[status(thm),theory(equality)],[494,338]),
[iquote('0:Res:494.1,338.0')] ).
cnf(1561,plain,
( ~ accessible_world(skc14,u)
| nonexistent(u,skc15) ),
inference(res,[status(thm),theory(equality)],[84,843]),
[iquote('0:Res:84.0,843.0')] ).
cnf(843,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| nonexistent(v,skc15) ),
inference(res,[status(thm),theory(equality)],[493,338]),
[iquote('0:Res:493.1,338.0')] ).
cnf(854,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[104,353]),
[iquote('0:Res:104.1,353.0')] ).
cnf(840,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| nonexistent(v,u) ),
inference(res,[status(thm),theory(equality)],[104,338]),
[iquote('0:Res:104.1,338.0')] ).
cnf(1548,plain,
( ~ accessible_world(skc14,u)
| human(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,823]),
[iquote('0:Res:84.0,823.0')] ).
cnf(823,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| human(v,skc13) ),
inference(res,[status(thm),theory(equality)],[456,323]),
[iquote('0:Res:456.1,323.0')] ).
cnf(1527,plain,
( ~ accessible_world(skc14,u)
| human(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,822]),
[iquote('0:Res:84.0,822.0')] ).
cnf(832,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| existent(v,u) ),
inference(res,[status(thm),theory(equality)],[114,332]),
[iquote('0:Res:114.1,332.0')] ).
cnf(822,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| human(v,skc17) ),
inference(res,[status(thm),theory(equality)],[455,323]),
[iquote('0:Res:455.1,323.0')] ).
cnf(821,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| human(v,u) ),
inference(res,[status(thm),theory(equality)],[112,323]),
[iquote('0:Res:112.1,323.0')] ).
cnf(801,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[124,316]),
[iquote('0:Res:124.1,316.0')] ).
cnf(792,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[124,309]),
[iquote('0:Res:124.1,309.0')] ).
cnf(782,plain,
( ~ thing(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[105,290]),
[iquote('0:Res:105.1,290.0')] ).
cnf(765,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| impartial(v,u) ),
inference(res,[status(thm),theory(equality)],[113,282]),
[iquote('0:Res:113.1,282.0')] ).
cnf(1478,plain,
( ~ accessible_world(skc14,u)
| animate(u,skc13) ),
inference(res,[status(thm),theory(equality)],[84,751]),
[iquote('0:Res:84.0,751.0')] ).
cnf(751,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| animate(v,skc13) ),
inference(res,[status(thm),theory(equality)],[456,261]),
[iquote('0:Res:456.1,261.0')] ).
cnf(1473,plain,
( ~ accessible_world(skc14,u)
| animate(u,skc17) ),
inference(res,[status(thm),theory(equality)],[84,750]),
[iquote('0:Res:84.0,750.0')] ).
cnf(756,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| living(v,u) ),
inference(res,[status(thm),theory(equality)],[113,273]),
[iquote('0:Res:113.1,273.0')] ).
cnf(750,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| animate(v,skc17) ),
inference(res,[status(thm),theory(equality)],[455,261]),
[iquote('0:Res:455.1,261.0')] ).
cnf(749,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| animate(v,u) ),
inference(res,[status(thm),theory(equality)],[112,261]),
[iquote('0:Res:112.1,261.0')] ).
cnf(578,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| forename(v,skc16) ),
inference(res,[status(thm),theory(equality)],[572,54]),
[iquote('0:Res:572.1,54.0')] ).
cnf(575,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| forename(v,skc12) ),
inference(res,[status(thm),theory(equality)],[144,54]),
[iquote('0:Res:144.1,54.0')] ).
cnf(574,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| forename(v,skc16) ),
inference(res,[status(thm),theory(equality)],[159,54]),
[iquote('0:Res:159.1,54.0')] ).
cnf(1459,plain,
( ~ accessible_world(skc14,u)
| forename(u,skc12) ),
inference(res,[status(thm),theory(equality)],[80,573]),
[iquote('0:Res:80.0,573.0')] ).
cnf(573,plain,
( ~ forename(skc9,u)
| ~ accessible_world(skc14,v)
| forename(v,u) ),
inference(res,[status(thm),theory(equality)],[121,54]),
[iquote('0:Res:121.1,54.0')] ).
cnf(554,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| proposition(v,skc14) ),
inference(res,[status(thm),theory(equality)],[98,64]),
[iquote('0:Res:98.1,64.0')] ).
cnf(1453,plain,
( ~ accessible_world(skc14,u)
| proposition(u,skc14) ),
inference(res,[status(thm),theory(equality)],[85,553]),
[iquote('0:Res:85.0,553.0')] ).
cnf(553,plain,
( ~ proposition(skc9,u)
| ~ accessible_world(skc14,v)
| proposition(v,u) ),
inference(res,[status(thm),theory(equality)],[131,64]),
[iquote('0:Res:131.1,64.0')] ).
cnf(541,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| man(v,skc17) ),
inference(res,[status(thm),theory(equality)],[534,44]),
[iquote('0:Res:534.1,44.0')] ).
cnf(537,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| man(v,skc13) ),
inference(res,[status(thm),theory(equality)],[181,44]),
[iquote('0:Res:181.1,44.0')] ).
cnf(536,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| man(v,skc17) ),
inference(res,[status(thm),theory(equality)],[162,44]),
[iquote('0:Res:162.1,44.0')] ).
cnf(1435,plain,
( ~ accessible_world(skc14,u)
| man(u,skc13) ),
inference(res,[status(thm),theory(equality)],[79,535]),
[iquote('0:Res:79.0,535.0')] ).
cnf(535,plain,
( ~ man(skc9,u)
| ~ accessible_world(skc14,v)
| man(v,u) ),
inference(res,[status(thm),theory(equality)],[111,44]),
[iquote('0:Res:111.1,44.0')] ).
cnf(527,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| think_believe_consider(v,skc15) ),
inference(res,[status(thm),theory(equality)],[516,63]),
[iquote('0:Res:516.1,63.0')] ).
cnf(525,plain,
( ~ entity(skc9,u)
| ~ accessible_world(skc14,v)
| entity(v,u) ),
inference(res,[status(thm),theory(equality)],[114,47]),
[iquote('0:Res:114.1,47.0')] ).
cnf(518,plain,
( ~ think_believe_consider(skc9,u)
| ~ accessible_world(skc14,v)
| think_believe_consider(v,u) ),
inference(res,[status(thm),theory(equality)],[130,63]),
[iquote('0:Res:130.1,63.0')] ).
cnf(505,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| eventuality(v,skc10) ),
inference(res,[status(thm),theory(equality)],[494,37]),
[iquote('0:Res:494.1,37.0')] ).
cnf(517,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| think_believe_consider(v,skc15) ),
inference(res,[status(thm),theory(equality)],[148,63]),
[iquote('0:Res:148.1,63.0')] ).
cnf(501,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| eventuality(v,skc15) ),
inference(res,[status(thm),theory(equality)],[493,37]),
[iquote('0:Res:493.1,37.0')] ).
cnf(483,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| event(v,skc15) ),
inference(res,[status(thm),theory(equality)],[472,43]),
[iquote('0:Res:472.1,43.0')] ).
cnf(480,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| event(v,skc10) ),
inference(res,[status(thm),theory(equality)],[471,43]),
[iquote('0:Res:471.1,43.0')] ).
cnf(1408,plain,
( ~ accessible_world(skc14,u)
| eventuality(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,495]),
[iquote('0:Res:133.0,495.0')] ).
cnf(495,plain,
( ~ eventuality(skc9,u)
| ~ accessible_world(skc14,v)
| eventuality(v,u) ),
inference(res,[status(thm),theory(equality)],[104,37]),
[iquote('0:Res:104.1,37.0')] ).
cnf(475,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| event(v,skc15) ),
inference(res,[status(thm),theory(equality)],[153,43]),
[iquote('0:Res:153.1,43.0')] ).
cnf(462,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| human_person(v,skc13) ),
inference(res,[status(thm),theory(equality)],[456,45]),
[iquote('0:Res:456.1,45.0')] ).
cnf(460,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| human_person(v,skc17) ),
inference(res,[status(thm),theory(equality)],[455,45]),
[iquote('0:Res:455.1,45.0')] ).
cnf(1388,plain,
( ~ accessible_world(skc14,u)
| event(u,skc10) ),
inference(res,[status(thm),theory(equality)],[134,473]),
[iquote('0:Res:134.0,473.0')] ).
cnf(473,plain,
( ~ event(skc9,u)
| ~ accessible_world(skc14,v)
| event(v,u) ),
inference(res,[status(thm),theory(equality)],[110,43]),
[iquote('0:Res:110.1,43.0')] ).
cnf(1375,plain,
( ~ accessible_world(skc14,u)
| ~ nonhuman(u,skc13) ),
inference(res,[status(thm),theory(equality)],[1363,226]),
[iquote('0:Res:1363.1,226.0')] ).
cnf(1372,plain,
( ~ accessible_world(skc14,u)
| ~ general(u,skc13) ),
inference(res,[status(thm),theory(equality)],[1363,802]),
[iquote('0:Res:1363.1,802.0')] ).
cnf(1363,plain,
( ~ accessible_world(skc14,u)
| human_person(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,458]),
[iquote('0:Res:145.0,458.0')] ).
cnf(458,plain,
( ~ human_person(skc9,u)
| ~ accessible_world(skc14,v)
| human_person(v,u) ),
inference(res,[status(thm),theory(equality)],[112,45]),
[iquote('0:Res:112.1,45.0')] ).
cnf(1359,plain,
( ~ jules_forename(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[27,1352]),
[iquote('0:Res:27.1,1352.0')] ).
cnf(1358,plain,
( ~ vincent_forename(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[30,1352]),
[iquote('0:Res:30.1,1352.0')] ).
cnf(1352,plain,
( ~ forename(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[20,1347]),
[iquote('0:Res:20.1,1347.0')] ).
cnf(1348,plain,
( ~ human_person(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[10,1343]),
[iquote('0:Res:10.1,1343.0')] ).
cnf(444,plain,
( ~ abstraction(skc9,u)
| ~ accessible_world(skc14,v)
| abstraction(v,u) ),
inference(res,[status(thm),theory(equality)],[124,57]),
[iquote('0:Res:124.1,57.0')] ).
cnf(1347,plain,
( ~ relname(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[21,1340]),
[iquote('0:Res:21.1,1340.0')] ).
cnf(1346,plain,
( ~ proposition(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[29,1340]),
[iquote('0:Res:29.1,1340.0')] ).
cnf(1343,plain,
( ~ organism(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[11,1338]),
[iquote('0:Res:11.1,1338.0')] ).
cnf(1340,plain,
( ~ relation(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[22,1335]),
[iquote('0:Res:22.1,1335.0')] ).
cnf(433,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| state(v,skc10) ),
inference(res,[status(thm),theory(equality)],[135,36]),
[iquote('0:Res:135.1,36.0')] ).
cnf(1338,plain,
( ~ entity(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[14,1330]),
[iquote('0:Res:14.1,1330.1')] ).
cnf(1335,plain,
( ~ abstraction(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[25,1329]),
[iquote('0:Res:25.1,1329.1')] ).
cnf(1333,plain,
( ~ man(u,skc10)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,1328]),
[iquote('0:Res:19.1,1328.1')] ).
cnf(1330,plain,
( ~ accessible_world(skc14,u)
| ~ existent(u,skc10) ),
inference(res,[status(thm),theory(equality)],[1320,563]),
[iquote('0:Res:1320.1,563.0')] ).
cnf(645,plain,
( ~ man(skc14,u)
| ~ think_believe_consider(skc14,v)
| ~ think_believe_consider(skc14,skf1(u))
| ~ proposition(skc14,w)
| ~ proposition(skc14,x)
| ~ agent(skc14,v,u)
| ~ theme(skc14,v,w)
| ~ theme(skc14,skf1(u),x)
| equal(x,w) ),
inference(res,[status(thm),theory(equality)],[94,71]),
[iquote('0:Res:94.1,71.4')] ).
cnf(1329,plain,
( ~ accessible_world(skc14,u)
| ~ general(u,skc10) ),
inference(res,[status(thm),theory(equality)],[1320,655]),
[iquote('0:Res:1320.1,655.0')] ).
cnf(1328,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skc10) ),
inference(res,[status(thm),theory(equality)],[1320,662]),
[iquote('0:Res:1320.1,662.0')] ).
cnf(1320,plain,
( ~ accessible_world(skc14,u)
| state(u,skc10) ),
inference(res,[status(thm),theory(equality)],[83,432]),
[iquote('0:Res:83.0,432.0')] ).
cnf(432,plain,
( ~ state(skc9,u)
| ~ accessible_world(skc14,v)
| state(v,u) ),
inference(res,[status(thm),theory(equality)],[103,36]),
[iquote('0:Res:103.1,36.0')] ).
cnf(150,plain,
( ~ think_believe_consider(skc9,u)
| ~ proposition(skc9,v)
| ~ proposition(skc9,w)
| ~ agent(skc9,u,x)
| ~ theme(skc9,u,w)
| ~ agent(skc9,skc15,x)
| ~ theme(skc9,skc15,v)
| equal(w,v) ),
inference(res,[status(thm),theory(equality)],[78,71]),
[iquote('0:Res:78.0,71.4')] ).
cnf(430,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| male(v,skc13) ),
inference(res,[status(thm),theory(equality)],[414,53]),
[iquote('0:Res:414.1,53.0')] ).
cnf(429,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| male(v,skc17) ),
inference(res,[status(thm),theory(equality)],[413,53]),
[iquote('0:Res:413.1,53.0')] ).
cnf(428,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| relname(v,skc12) ),
inference(res,[status(thm),theory(equality)],[405,55]),
[iquote('0:Res:405.1,55.0')] ).
cnf(427,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| relname(v,skc16) ),
inference(res,[status(thm),theory(equality)],[404,55]),
[iquote('0:Res:404.1,55.0')] ).
cnf(97,plain,
( ~ think_believe_consider(skc9,u)
| ~ think_believe_consider(skc9,v)
| ~ proposition(skc9,w)
| ~ agent(skc9,v,x)
| ~ agent(skc9,u,x)
| ~ theme(skc9,v,w)
| ~ theme(skc9,u,skc14)
| equal(w,skc14) ),
inference(res,[status(thm),theory(equality)],[85,71]),
[iquote('0:Res:85.0,71.1')] ).
cnf(426,plain,
( ~ thing(skc9,u)
| ~ accessible_world(skc14,v)
| thing(v,u) ),
inference(res,[status(thm),theory(equality)],[105,38]),
[iquote('0:Res:105.1,38.0')] ).
cnf(422,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| relation(v,skc14) ),
inference(res,[status(thm),theory(equality)],[394,56]),
[iquote('0:Res:394.1,56.0')] ).
cnf(185,plain,
( ~ think_believe_consider(skc9,u)
| ~ proposition(skc9,v)
| ~ proposition(skc9,w)
| ~ theme(skc9,u,v)
| ~ agent(skc9,u,skc17)
| ~ theme(skc9,skc15,w)
| equal(w,v) ),
inference(mrr,[status(thm)],[171,78]),
[iquote('0:MRR:171.3,78.0')] ).
cnf(421,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| present(v,skc15) ),
inference(res,[status(thm),theory(equality)],[384,62]),
[iquote('0:Res:384.1,62.0')] ).
cnf(420,plain,
( ~ accessible_world(skc14,u)
| ~ accessible_world(u,v)
| vincent_forename(v,skc16) ),
inference(res,[status(thm),theory(equality)],[374,65]),
[iquote('0:Res:374.1,65.0')] ).
cnf(186,plain,
( ~ think_believe_consider(skc9,u)
| ~ proposition(skc9,v)
| ~ agent(skc9,u,w)
| ~ theme(skc9,u,v)
| ~ agent(skc9,skc15,w)
| equal(v,skc14) ),
inference(mrr,[status(thm)],[168,85,78]),
[iquote('0:MRR:168.1,168.4,85.0,78.0')] ).
cnf(419,plain,
( ~ organism(skc9,u)
| ~ accessible_world(skc14,v)
| organism(v,u) ),
inference(res,[status(thm),theory(equality)],[113,46]),
[iquote('0:Res:113.1,46.0')] ).
cnf(1272,plain,
( ~ jules_forename(u,skc13)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[27,1265]),
[iquote('0:Res:27.1,1265.0')] ).
cnf(1271,plain,
( ~ vincent_forename(u,skc13)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[30,1265]),
[iquote('0:Res:30.1,1265.0')] ).
cnf(1265,plain,
( ~ forename(u,skc13)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[20,1262]),
[iquote('0:Res:20.1,1262.0')] ).
cnf(158,plain,
( ~ entity(skc9,u)
| ~ forename(skc9,v)
| ~ of(skc9,v,u)
| ~ of(skc9,skc16,u)
| equal(skc16,v) ),
inference(res,[status(thm),theory(equality)],[74,70]),
[iquote('0:Res:74.0,70.2')] ).
cnf(1262,plain,
( ~ relname(u,skc13)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[21,1258]),
[iquote('0:Res:21.1,1258.0')] ).
cnf(1261,plain,
( ~ proposition(u,skc13)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[29,1258]),
[iquote('0:Res:29.1,1258.0')] ).
cnf(1258,plain,
( ~ relation(u,skc13)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[22,1251]),
[iquote('0:Res:22.1,1251.1')] ).
cnf(1251,plain,
( ~ accessible_world(skc14,u)
| ~ abstraction(u,skc13) ),
inference(res,[status(thm),theory(equality)],[1243,245]),
[iquote('0:Res:1243.1,245.1')] ).
cnf(143,plain,
( ~ entity(skc9,u)
| ~ forename(skc9,v)
| ~ of(skc9,v,u)
| ~ of(skc9,skc12,u)
| equal(skc12,v) ),
inference(res,[status(thm),theory(equality)],[80,70]),
[iquote('0:Res:80.0,70.2')] ).
cnf(1243,plain,
( ~ accessible_world(skc14,u)
| male(u,skc13) ),
inference(res,[status(thm),theory(equality)],[146,415]),
[iquote('0:Res:146.0,415.0')] ).
cnf(415,plain,
( ~ male(skc9,u)
| ~ accessible_world(skc14,v)
| male(v,u) ),
inference(res,[status(thm),theory(equality)],[120,53]),
[iquote('0:Res:120.1,53.0')] ).
cnf(1234,plain,
( ~ accessible_world(skc14,u)
| relname(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,406]),
[iquote('0:Res:142.0,406.0')] ).
cnf(406,plain,
( ~ relname(skc9,u)
| ~ accessible_world(skc14,v)
| relname(v,u) ),
inference(res,[status(thm),theory(equality)],[122,55]),
[iquote('0:Res:122.1,55.0')] ).
cnf(183,plain,
( ~ forename(skc9,u)
| ~ entity(skc9,skc17)
| ~ of(skc9,u,skc17)
| equal(u,skc16) ),
inference(mrr,[status(thm)],[174,74]),
[iquote('0:MRR:174.0,74.0')] ).
cnf(1216,plain,
( ~ accessible_world(skc14,u)
| relation(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,395]),
[iquote('0:Res:96.0,395.0')] ).
cnf(395,plain,
( ~ relation(skc9,u)
| ~ accessible_world(skc14,v)
| relation(v,u) ),
inference(res,[status(thm),theory(equality)],[123,56]),
[iquote('0:Res:123.1,56.0')] ).
cnf(184,plain,
( ~ forename(skc9,u)
| ~ entity(skc9,skc13)
| ~ of(skc9,u,skc13)
| equal(u,skc12) ),
inference(mrr,[status(thm)],[165,80]),
[iquote('0:MRR:165.0,80.0')] ).
cnf(386,plain,
( ~ present(skc9,u)
| ~ accessible_world(skc14,v)
| present(v,u) ),
inference(res,[status(thm),theory(equality)],[129,62]),
[iquote('0:Res:129.1,62.0')] ).
cnf(385,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| present(v,skc15) ),
inference(res,[status(thm),theory(equality)],[151,62]),
[iquote('0:Res:151.1,62.0')] ).
cnf(376,plain,
( ~ vincent_forename(skc9,u)
| ~ accessible_world(skc14,v)
| vincent_forename(v,u) ),
inference(res,[status(thm),theory(equality)],[132,65]),
[iquote('0:Res:132.1,65.0')] ).
cnf(375,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| vincent_forename(v,skc16) ),
inference(res,[status(thm),theory(equality)],[155,65]),
[iquote('0:Res:155.1,65.0')] ).
cnf(587,plain,
( ~ man(skc14,u)
| ~ accessible_world(skc14,v)
| agent(v,skf1(u),u) ),
inference(res,[status(thm),theory(equality)],[94,67]),
[iquote('0:Res:94.1,67.1')] ).
cnf(361,plain,
( ~ specific(skc9,u)
| ~ accessible_world(skc14,v)
| specific(v,u) ),
inference(res,[status(thm),theory(equality)],[107,40]),
[iquote('0:Res:107.1,40.0')] ).
cnf(577,plain,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| forename(w,v) ),
inference(res,[status(thm),theory(equality)],[27,54]),
[iquote('0:Res:27.1,54.0')] ).
cnf(352,plain,
( ~ unisex(skc9,u)
| ~ accessible_world(skc14,v)
| unisex(v,u) ),
inference(res,[status(thm),theory(equality)],[109,42]),
[iquote('0:Res:109.1,42.0')] ).
cnf(342,plain,
( ~ accessible_world(skc9,u)
| ~ accessible_world(u,v)
| jules_forename(v,skc12) ),
inference(res,[status(thm),theory(equality)],[140,60]),
[iquote('0:Res:140.1,60.0')] ).
cnf(1165,plain,
( ~ accessible_world(skc14,u)
| jules_forename(u,skc12) ),
inference(res,[status(thm),theory(equality)],[81,341]),
[iquote('0:Res:81.0,341.0')] ).
cnf(576,plain,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| forename(w,v) ),
inference(res,[status(thm),theory(equality)],[30,54]),
[iquote('0:Res:30.1,54.0')] ).
cnf(341,plain,
( ~ jules_forename(skc9,u)
| ~ accessible_world(skc14,v)
| jules_forename(v,u) ),
inference(res,[status(thm),theory(equality)],[127,60]),
[iquote('0:Res:127.1,60.0')] ).
cnf(337,plain,
( ~ nonexistent(skc9,u)
| ~ accessible_world(skc14,v)
| nonexistent(v,u) ),
inference(res,[status(thm),theory(equality)],[108,41]),
[iquote('0:Res:108.1,41.0')] ).
cnf(526,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| entity(w,v) ),
inference(res,[status(thm),theory(equality)],[11,47]),
[iquote('0:Res:11.1,47.0')] ).
cnf(331,plain,
( ~ existent(skc9,u)
| ~ accessible_world(skc14,v)
| existent(v,u) ),
inference(res,[status(thm),theory(equality)],[115,48]),
[iquote('0:Res:115.1,48.0')] ).
cnf(322,plain,
( ~ human(skc9,u)
| ~ accessible_world(skc14,v)
| human(v,u) ),
inference(res,[status(thm),theory(equality)],[118,51]),
[iquote('0:Res:118.1,51.0')] ).
cnf(497,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| eventuality(w,v) ),
inference(res,[status(thm),theory(equality)],[1,37]),
[iquote('0:Res:1.1,37.0')] ).
cnf(315,plain,
( ~ nonhuman(skc9,u)
| ~ accessible_world(skc14,v)
| nonhuman(v,u) ),
inference(res,[status(thm),theory(equality)],[125,58]),
[iquote('0:Res:125.1,58.0')] ).
cnf(308,plain,
( ~ general(skc9,u)
| ~ accessible_world(skc14,v)
| general(v,u) ),
inference(res,[status(thm),theory(equality)],[126,59]),
[iquote('0:Res:126.1,59.0')] ).
cnf(1104,plain,
( ~ accessible_world(skc14,u)
| eventuality(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,496]),
[iquote('0:Res:214.0,496.0')] ).
cnf(1102,plain,
( ~ accessible_world(skc14,u)
| eventuality(u,skc15) ),
inference(res,[status(thm),theory(equality)],[194,496]),
[iquote('0:Res:194.0,496.0')] ).
cnf(496,plain,
( ~ event(u,v)
| ~ accessible_world(u,w)
| eventuality(w,v) ),
inference(res,[status(thm),theory(equality)],[8,37]),
[iquote('0:Res:8.1,37.0')] ).
cnf(298,plain,
( ~ smoke(skc9,u)
| ~ accessible_world(skc14,v)
| smoke(v,u) ),
inference(res,[status(thm),theory(equality)],[128,61]),
[iquote('0:Res:128.1,61.0')] ).
cnf(289,plain,
( ~ singleton(skc9,u)
| ~ accessible_world(skc14,v)
| singleton(v,u) ),
inference(res,[status(thm),theory(equality)],[106,39]),
[iquote('0:Res:106.1,39.0')] ).
cnf(281,plain,
( ~ impartial(skc9,u)
| ~ accessible_world(skc14,v)
| impartial(v,u) ),
inference(res,[status(thm),theory(equality)],[116,49]),
[iquote('0:Res:116.1,49.0')] ).
cnf(272,plain,
( ~ living(skc9,u)
| ~ accessible_world(skc14,v)
| living(v,u) ),
inference(res,[status(thm),theory(equality)],[117,50]),
[iquote('0:Res:117.1,50.0')] ).
cnf(477,plain,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| event(w,v) ),
inference(res,[status(thm),theory(equality)],[28,43]),
[iquote('0:Res:28.1,43.0')] ).
cnf(260,plain,
( ~ animate(skc9,u)
| ~ accessible_world(skc14,v)
| animate(v,u) ),
inference(res,[status(thm),theory(equality)],[119,52]),
[iquote('0:Res:119.1,52.0')] ).
cnf(1080,plain,
( ~ jules_forename(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[27,1077]),
[iquote('0:Res:27.1,1077.0')] ).
cnf(476,plain,
( ~ state(u,v)
| ~ accessible_world(u,w)
| event(w,v) ),
inference(res,[status(thm),theory(equality)],[7,43]),
[iquote('0:Res:7.1,43.0')] ).
cnf(1079,plain,
( ~ vincent_forename(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[30,1077]),
[iquote('0:Res:30.1,1077.0')] ).
cnf(1077,plain,
( ~ forename(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[20,1057]),
[iquote('0:Res:20.1,1057.0')] ).
cnf(1057,plain,
( ~ relname(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[21,1038]),
[iquote('0:Res:21.1,1038.0')] ).
cnf(1063,plain,
( ~ accessible_world(skc14,u)
| human_person(u,skc17) ),
inference(res,[status(thm),theory(equality)],[187,457]),
[iquote('0:Res:187.0,457.0')] ).
cnf(457,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| human_person(w,v) ),
inference(res,[status(thm),theory(equality)],[9,45]),
[iquote('0:Res:9.1,45.0')] ).
cnf(1056,plain,
( ~ proposition(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[29,1038]),
[iquote('0:Res:29.1,1038.0')] ).
cnf(1041,plain,
( ~ human_person(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[10,1037]),
[iquote('0:Res:10.1,1037.0')] ).
cnf(1038,plain,
( ~ relation(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[22,1031]),
[iquote('0:Res:22.1,1031.0')] ).
cnf(1043,plain,
( ~ accessible_world(skc9,u)
| abstraction(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,443]),
[iquote('0:Res:96.0,443.0')] ).
cnf(443,plain,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
inference(res,[status(thm),theory(equality)],[22,57]),
[iquote('0:Res:22.1,57.0')] ).
cnf(1037,plain,
( ~ organism(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[11,1018]),
[iquote('0:Res:11.1,1018.0')] ).
cnf(1033,plain,
( ~ man(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,925]),
[iquote('0:Res:19.1,925.1')] ).
cnf(1031,plain,
( ~ abstraction(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[25,814]),
[iquote('0:Res:25.1,814.1')] ).
cnf(1018,plain,
( ~ entity(u,skf1(v))
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[14,732]),
[iquote('0:Res:14.1,732.1')] ).
cnf(425,plain,
( ~ abstraction(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[23,38]),
[iquote('0:Res:23.1,38.0')] ).
cnf(925,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[474,661]),
[iquote('0:Res:474.1,661.0')] ).
cnf(814,plain,
( ~ accessible_world(skc14,u)
| ~ general(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[474,654]),
[iquote('0:Res:474.1,654.0')] ).
cnf(1020,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,424]),
[iquote('0:Res:133.0,424.0')] ).
cnf(1019,plain,
( ~ accessible_world(skc9,u)
| thing(u,skc15) ),
inference(res,[status(thm),theory(equality)],[152,424]),
[iquote('0:Res:152.0,424.0')] ).
cnf(424,plain,
( ~ eventuality(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[2,38]),
[iquote('0:Res:2.1,38.0')] ).
cnf(732,plain,
( ~ accessible_world(skc14,u)
| ~ existent(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[474,562]),
[iquote('0:Res:474.1,562.0')] ).
cnf(1012,plain,
( ~ accessible_world(skc14,u)
| ~ general(u,skc17) ),
inference(res,[status(thm),theory(equality)],[534,976]),
[iquote('0:Res:534.1,976.0')] ).
cnf(976,plain,
( ~ man(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[9,802]),
[iquote('0:Res:9.1,802.0')] ).
cnf(923,plain,
( ~ smoke(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[28,661]),
[iquote('0:Res:28.1,661.0')] ).
cnf(423,plain,
( ~ entity(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
inference(res,[status(thm),theory(equality)],[12,38]),
[iquote('0:Res:12.1,38.0')] ).
cnf(812,plain,
( ~ smoke(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[28,654]),
[iquote('0:Res:28.1,654.0')] ).
cnf(979,plain,
( ~ accessible_world(skc9,u)
| ~ general(u,skc13) ),
inference(res,[status(thm),theory(equality)],[456,802]),
[iquote('0:Res:456.1,802.0')] ).
cnf(983,plain,
( ~ accessible_world(skc9,u)
| organism(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,418]),
[iquote('0:Res:145.0,418.0')] ).
cnf(982,plain,
( ~ accessible_world(skc9,u)
| organism(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,418]),
[iquote('0:Res:160.0,418.0')] ).
cnf(418,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| organism(w,v) ),
inference(res,[status(thm),theory(equality)],[10,46]),
[iquote('0:Res:10.1,46.0')] ).
cnf(978,plain,
( ~ accessible_world(skc9,u)
| ~ general(u,skc17) ),
inference(res,[status(thm),theory(equality)],[455,802]),
[iquote('0:Res:455.1,802.0')] ).
cnf(802,plain,
( ~ human_person(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[10,650]),
[iquote('0:Res:10.1,650.0')] ).
cnf(730,plain,
( ~ smoke(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[28,562]),
[iquote('0:Res:28.1,562.0')] ).
cnf(962,plain,
( ~ accessible_world(skc14,u)
| male(u,skc17) ),
inference(res,[status(thm),theory(equality)],[187,416]),
[iquote('0:Res:187.0,416.0')] ).
cnf(416,plain,
( ~ man(u,v)
| ~ accessible_world(u,w)
| male(w,v) ),
inference(res,[status(thm),theory(equality)],[19,53]),
[iquote('0:Res:19.1,53.0')] ).
cnf(676,plain,
( ~ man(u,v)
| ~ abstraction(u,v) ),
inference(res,[status(thm),theory(equality)],[19,245]),
[iquote('0:Res:19.1,245.1')] ).
cnf(662,plain,
( ~ state(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[1,244]),
[iquote('0:Res:1.1,244.0')] ).
cnf(920,plain,
( ~ accessible_world(skc14,u)
| ~ male(u,skc15) ),
inference(res,[status(thm),theory(equality)],[472,661]),
[iquote('0:Res:472.1,661.0')] ).
cnf(939,plain,
( ~ accessible_world(skc14,u)
| relname(u,skc16) ),
inference(res,[status(thm),theory(equality)],[192,407]),
[iquote('0:Res:192.0,407.0')] ).
cnf(407,plain,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| relname(w,v) ),
inference(res,[status(thm),theory(equality)],[20,55]),
[iquote('0:Res:20.1,55.0')] ).
cnf(927,plain,
( ~ accessible_world(skc9,u)
| relation(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,397]),
[iquote('0:Res:142.0,397.0')] ).
cnf(926,plain,
( ~ accessible_world(skc9,u)
| relation(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,397]),
[iquote('0:Res:157.0,397.0')] ).
cnf(932,plain,
~ male(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[120,919]),
[iquote('0:Res:120.1,919.0')] ).
cnf(919,plain,
~ male(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[214,661]),
[iquote('0:Res:214.0,661.0')] ).
cnf(397,plain,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| relation(w,v) ),
inference(res,[status(thm),theory(equality)],[21,56]),
[iquote('0:Res:21.1,56.0')] ).
cnf(661,plain,
( ~ event(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[8,244]),
[iquote('0:Res:8.1,244.0')] ).
cnf(655,plain,
( ~ state(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[1,236]),
[iquote('0:Res:1.1,236.0')] ).
cnf(906,plain,
( ~ jules_forename(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[27,903]),
[iquote('0:Res:27.1,903.0')] ).
cnf(905,plain,
( ~ vincent_forename(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[30,903]),
[iquote('0:Res:30.1,903.0')] ).
cnf(396,plain,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| relation(w,v) ),
inference(res,[status(thm),theory(equality)],[29,56]),
[iquote('0:Res:29.1,56.0')] ).
cnf(903,plain,
( ~ forename(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[20,887]),
[iquote('0:Res:20.1,887.0')] ).
cnf(887,plain,
( ~ relname(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[21,883]),
[iquote('0:Res:21.1,883.0')] ).
cnf(890,plain,
( ~ accessible_world(skc9,u)
| specific(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,363]),
[iquote('0:Res:133.0,363.0')] ).
cnf(889,plain,
( ~ accessible_world(skc9,u)
| specific(u,skc15) ),
inference(res,[status(thm),theory(equality)],[152,363]),
[iquote('0:Res:152.0,363.0')] ).
cnf(363,plain,
( ~ eventuality(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[4,40]),
[iquote('0:Res:4.1,40.0')] ).
cnf(886,plain,
( ~ proposition(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[29,883]),
[iquote('0:Res:29.1,883.0')] ).
cnf(883,plain,
( ~ relation(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[22,882]),
[iquote('0:Res:22.1,882.0')] ).
cnf(882,plain,
( ~ abstraction(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[25,809]),
[iquote('0:Res:25.1,809.1')] ).
cnf(809,plain,
( ~ accessible_world(skc14,u)
| ~ general(u,skc15) ),
inference(res,[status(thm),theory(equality)],[472,654]),
[iquote('0:Res:472.1,654.0')] ).
cnf(362,plain,
( ~ entity(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
inference(res,[status(thm),theory(equality)],[13,40]),
[iquote('0:Res:13.1,40.0')] ).
cnf(853,plain,
( ~ accessible_world(skc9,u)
| unisex(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,353]),
[iquote('0:Res:133.0,353.0')] ).
cnf(852,plain,
( ~ accessible_world(skc9,u)
| unisex(u,skc15) ),
inference(res,[status(thm),theory(equality)],[152,353]),
[iquote('0:Res:152.0,353.0')] ).
cnf(839,plain,
( ~ accessible_world(skc9,u)
| nonexistent(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,338]),
[iquote('0:Res:133.0,338.0')] ).
cnf(838,plain,
( ~ accessible_world(skc9,u)
| nonexistent(u,skc15) ),
inference(res,[status(thm),theory(equality)],[152,338]),
[iquote('0:Res:152.0,338.0')] ).
cnf(354,plain,
( ~ abstraction(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[26,42]),
[iquote('0:Res:26.1,42.0')] ).
cnf(819,plain,
( ~ accessible_world(skc9,u)
| human(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,323]),
[iquote('0:Res:145.0,323.0')] ).
cnf(818,plain,
( ~ accessible_world(skc9,u)
| human(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,323]),
[iquote('0:Res:160.0,323.0')] ).
cnf(849,plain,
~ jules_forename(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[27,837]),
[iquote('0:Res:27.1,837.0')] ).
cnf(848,plain,
~ vincent_forename(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[30,837]),
[iquote('0:Res:30.1,837.0')] ).
cnf(353,plain,
( ~ eventuality(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
inference(res,[status(thm),theory(equality)],[6,42]),
[iquote('0:Res:6.1,42.0')] ).
cnf(847,plain,
~ jules_forename(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[27,836]),
[iquote('0:Res:27.1,836.0')] ).
cnf(846,plain,
~ vincent_forename(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[30,836]),
[iquote('0:Res:30.1,836.0')] ).
cnf(837,plain,
~ forename(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[20,831]),
[iquote('0:Res:20.1,831.0')] ).
cnf(836,plain,
~ forename(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[20,829]),
[iquote('0:Res:20.1,829.0')] ).
cnf(338,plain,
( ~ eventuality(u,v)
| ~ accessible_world(u,w)
| nonexistent(w,v) ),
inference(res,[status(thm),theory(equality)],[5,41]),
[iquote('0:Res:5.1,41.0')] ).
cnf(831,plain,
~ relname(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[21,826]),
[iquote('0:Res:21.1,826.0')] ).
cnf(830,plain,
~ proposition(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[29,826]),
[iquote('0:Res:29.1,826.0')] ).
cnf(829,plain,
~ relname(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[21,824]),
[iquote('0:Res:21.1,824.0')] ).
cnf(828,plain,
~ proposition(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[29,824]),
[iquote('0:Res:29.1,824.0')] ).
cnf(332,plain,
( ~ entity(u,v)
| ~ accessible_world(u,w)
| existent(w,v) ),
inference(res,[status(thm),theory(equality)],[14,48]),
[iquote('0:Res:14.1,48.0')] ).
cnf(826,plain,
~ relation(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[22,817]),
[iquote('0:Res:22.1,817.0')] ).
cnf(824,plain,
~ relation(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[22,816]),
[iquote('0:Res:22.1,816.0')] ).
cnf(817,plain,
~ abstraction(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[25,815]),
[iquote('0:Res:25.1,815.0')] ).
cnf(816,plain,
~ abstraction(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[25,808]),
[iquote('0:Res:25.1,808.0')] ).
cnf(323,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| human(w,v) ),
inference(res,[status(thm),theory(equality)],[17,51]),
[iquote('0:Res:17.1,51.0')] ).
cnf(815,plain,
~ general(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[126,808]),
[iquote('0:Res:126.1,808.0')] ).
cnf(808,plain,
~ general(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[214,654]),
[iquote('0:Res:214.0,654.0')] ).
cnf(654,plain,
( ~ event(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[8,236]),
[iquote('0:Res:8.1,236.0')] ).
cnf(650,plain,
( ~ organism(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[11,235]),
[iquote('0:Res:11.1,235.0')] ).
cnf(316,plain,
( ~ abstraction(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
inference(res,[status(thm),theory(equality)],[24,58]),
[iquote('0:Res:24.1,58.0')] ).
cnf(797,plain,
( ~ jules_forename(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[27,794]),
[iquote('0:Res:27.1,794.0')] ).
cnf(796,plain,
( ~ vincent_forename(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[30,794]),
[iquote('0:Res:30.1,794.0')] ).
cnf(794,plain,
( ~ forename(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[20,789]),
[iquote('0:Res:20.1,789.0')] ).
cnf(789,plain,
( ~ relname(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[21,785]),
[iquote('0:Res:21.1,785.0')] ).
cnf(309,plain,
( ~ abstraction(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
inference(res,[status(thm),theory(equality)],[25,59]),
[iquote('0:Res:25.1,59.0')] ).
cnf(788,plain,
( ~ proposition(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[29,785]),
[iquote('0:Res:29.1,785.0')] ).
cnf(785,plain,
( ~ relation(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[22,784]),
[iquote('0:Res:22.1,784.0')] ).
cnf(784,plain,
( ~ abstraction(u,skc17)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[24,776]),
[iquote('0:Res:24.1,776.1')] ).
cnf(776,plain,
( ~ accessible_world(skc14,u)
| ~ nonhuman(u,skc17) ),
inference(res,[status(thm),theory(equality)],[534,600]),
[iquote('0:Res:534.1,600.0')] ).
cnf(290,plain,
( ~ thing(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
inference(res,[status(thm),theory(equality)],[3,39]),
[iquote('0:Res:3.1,39.0')] ).
cnf(600,plain,
( ~ man(u,v)
| ~ nonhuman(u,v) ),
inference(res,[status(thm),theory(equality)],[9,226]),
[iquote('0:Res:9.1,226.0')] ).
cnf(563,plain,
( ~ state(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[1,219]),
[iquote('0:Res:1.1,219.0')] ).
cnf(766,plain,
( ~ man(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[9,762]),
[iquote('0:Res:9.1,762.0')] ).
cnf(762,plain,
( ~ human_person(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[10,761]),
[iquote('0:Res:10.1,761.0')] ).
cnf(282,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| impartial(w,v) ),
inference(res,[status(thm),theory(equality)],[15,49]),
[iquote('0:Res:15.1,49.0')] ).
cnf(761,plain,
( ~ organism(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[11,759]),
[iquote('0:Res:11.1,759.0')] ).
cnf(759,plain,
( ~ entity(u,skc15)
| ~ accessible_world(skc14,u) ),
inference(res,[status(thm),theory(equality)],[14,727]),
[iquote('0:Res:14.1,727.1')] ).
cnf(727,plain,
( ~ accessible_world(skc14,u)
| ~ existent(u,skc15) ),
inference(res,[status(thm),theory(equality)],[472,562]),
[iquote('0:Res:472.1,562.0')] ).
cnf(747,plain,
( ~ accessible_world(skc9,u)
| animate(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,261]),
[iquote('0:Res:145.0,261.0')] ).
cnf(273,plain,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| living(w,v) ),
inference(res,[status(thm),theory(equality)],[16,50]),
[iquote('0:Res:16.1,50.0')] ).
cnf(746,plain,
( ~ accessible_world(skc9,u)
| animate(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,261]),
[iquote('0:Res:160.0,261.0')] ).
cnf(752,plain,
~ man(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[9,743]),
[iquote('0:Res:9.1,743.0')] ).
cnf(744,plain,
~ man(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[9,741]),
[iquote('0:Res:9.1,741.0')] ).
cnf(743,plain,
~ human_person(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[10,740]),
[iquote('0:Res:10.1,740.0')] ).
cnf(261,plain,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| animate(w,v) ),
inference(res,[status(thm),theory(equality)],[18,52]),
[iquote('0:Res:18.1,52.0')] ).
cnf(741,plain,
~ human_person(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[10,737]),
[iquote('0:Res:10.1,737.0')] ).
cnf(740,plain,
~ organism(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[11,735]),
[iquote('0:Res:11.1,735.0')] ).
cnf(737,plain,
~ organism(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[11,734]),
[iquote('0:Res:11.1,734.0')] ).
cnf(735,plain,
~ entity(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[14,733]),
[iquote('0:Res:14.1,733.0')] ).
cnf(99,plain,
( ~ be(skc9,u,v,w)
| be(skc14,u,v,w) ),
inference(res,[status(thm),theory(equality)],[84,69]),
[iquote('0:Res:84.0,69.0')] ).
cnf(734,plain,
~ entity(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[14,726]),
[iquote('0:Res:14.1,726.0')] ).
cnf(733,plain,
~ existent(skc9,skf1(u)),
inference(res,[status(thm),theory(equality)],[115,726]),
[iquote('0:Res:115.1,726.0')] ).
cnf(726,plain,
~ existent(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[214,562]),
[iquote('0:Res:214.0,562.0')] ).
cnf(562,plain,
( ~ event(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[8,219]),
[iquote('0:Res:8.1,219.0')] ).
cnf(100,plain,
( ~ of(skc9,u,v)
| of(skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[84,66]),
[iquote('0:Res:84.0,66.0')] ).
cnf(714,plain,
( ~ jules_forename(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[27,708]),
[iquote('0:Res:27.1,708.0')] ).
cnf(713,plain,
( ~ vincent_forename(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[30,708]),
[iquote('0:Res:30.1,708.0')] ).
cnf(711,plain,
( ~ jules_forename(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[27,703]),
[iquote('0:Res:27.1,703.0')] ).
cnf(710,plain,
( ~ vincent_forename(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[30,703]),
[iquote('0:Res:30.1,703.0')] ).
cnf(102,plain,
( ~ theme(skc9,u,v)
| theme(skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[84,68]),
[iquote('0:Res:84.0,68.0')] ).
cnf(708,plain,
( ~ forename(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[20,695]),
[iquote('0:Res:20.1,695.0')] ).
cnf(703,plain,
( ~ forename(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[20,690]),
[iquote('0:Res:20.1,690.0')] ).
cnf(695,plain,
( ~ relname(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[21,681]),
[iquote('0:Res:21.1,681.0')] ).
cnf(694,plain,
( ~ proposition(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[29,681]),
[iquote('0:Res:29.1,681.0')] ).
cnf(101,plain,
( ~ agent(skc9,u,v)
| agent(skc14,u,v) ),
inference(res,[status(thm),theory(equality)],[84,67]),
[iquote('0:Res:84.0,67.0')] ).
cnf(690,plain,
( ~ relname(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[21,679]),
[iquote('0:Res:21.1,679.0')] ).
cnf(689,plain,
( ~ proposition(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[29,679]),
[iquote('0:Res:29.1,679.0')] ).
cnf(685,plain,
( ~ man(skc9,u)
| ~ abstraction(skc14,u) ),
inference(res,[status(thm),theory(equality)],[19,675]),
[iquote('0:Res:19.1,675.0')] ).
cnf(681,plain,
( ~ relation(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[22,668]),
[iquote('0:Res:22.1,668.0')] ).
cnf(182,plain,
( ~ accessible_world(skc9,u)
| be(u,skc10,skc13,skc13) ),
inference(rew,[status(thm),theory(equality)],[175,176]),
[iquote('0:Rew:175.0,176.1')] ).
cnf(679,plain,
( ~ relation(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[22,666]),
[iquote('0:Res:22.1,666.0')] ).
cnf(675,plain,
( ~ male(skc9,u)
| ~ abstraction(skc14,u) ),
inference(res,[status(thm),theory(equality)],[120,245]),
[iquote('0:Res:120.1,245.1')] ).
cnf(668,plain,
( ~ abstraction(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[25,657]),
[iquote('0:Res:25.1,657.1')] ).
cnf(666,plain,
( ~ abstraction(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[25,656]),
[iquote('0:Res:25.1,656.1')] ).
cnf(245,plain,
( ~ abstraction(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[26,31]),
[iquote('0:Res:26.1,31.0')] ).
cnf(664,plain,
( ~ accessible_world(skc9,u)
| ~ male(u,skc10) ),
inference(res,[status(thm),theory(equality)],[494,244]),
[iquote('0:Res:494.1,244.0')] ).
cnf(663,plain,
( ~ accessible_world(skc9,u)
| ~ male(u,skc15) ),
inference(res,[status(thm),theory(equality)],[493,244]),
[iquote('0:Res:493.1,244.0')] ).
cnf(657,plain,
( ~ accessible_world(skc9,u)
| ~ general(u,skc10) ),
inference(res,[status(thm),theory(equality)],[494,236]),
[iquote('0:Res:494.1,236.0')] ).
cnf(656,plain,
( ~ accessible_world(skc9,u)
| ~ general(u,skc15) ),
inference(res,[status(thm),theory(equality)],[493,236]),
[iquote('0:Res:493.1,236.0')] ).
cnf(244,plain,
( ~ eventuality(u,v)
| ~ male(u,v) ),
inference(res,[status(thm),theory(equality)],[6,31]),
[iquote('0:Res:6.1,31.0')] ).
cnf(236,plain,
( ~ eventuality(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[4,32]),
[iquote('0:Res:4.1,32.0')] ).
cnf(235,plain,
( ~ entity(u,v)
| ~ general(u,v) ),
inference(res,[status(thm),theory(equality)],[13,32]),
[iquote('0:Res:13.1,32.0')] ).
cnf(640,plain,
( ~ jules_forename(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[27,628]),
[iquote('0:Res:27.1,628.0')] ).
cnf(639,plain,
( ~ vincent_forename(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[30,628]),
[iquote('0:Res:30.1,628.0')] ).
cnf(71,axiom,
( ~ think_believe_consider(u,v)
| ~ think_believe_consider(u,w)
| ~ proposition(u,x)
| ~ proposition(u,y)
| ~ agent(u,w,z)
| ~ agent(u,v,z)
| ~ theme(u,v,x)
| ~ theme(u,w,y)
| equal(y,x) ),
file('NLP224-1.p',unknown),
[] ).
cnf(637,plain,
( ~ jules_forename(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[27,625]),
[iquote('0:Res:27.1,625.0')] ).
cnf(636,plain,
( ~ vincent_forename(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[30,625]),
[iquote('0:Res:30.1,625.0')] ).
cnf(628,plain,
( ~ forename(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[20,621]),
[iquote('0:Res:20.1,621.0')] ).
cnf(625,plain,
( ~ forename(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[20,618]),
[iquote('0:Res:20.1,618.0')] ).
cnf(70,axiom,
( ~ entity(u,v)
| ~ forename(u,w)
| ~ forename(u,x)
| ~ of(u,x,v)
| ~ of(u,w,v)
| equal(w,x) ),
file('NLP224-1.p',unknown),
[] ).
cnf(621,plain,
( ~ relname(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[21,614]),
[iquote('0:Res:21.1,614.0')] ).
cnf(620,plain,
( ~ proposition(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[29,614]),
[iquote('0:Res:29.1,614.0')] ).
cnf(618,plain,
( ~ relname(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[21,612]),
[iquote('0:Res:21.1,612.0')] ).
cnf(617,plain,
( ~ proposition(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[29,612]),
[iquote('0:Res:29.1,612.0')] ).
cnf(69,axiom,
( ~ accessible_world(u,v)
| ~ be(u,w,x,y)
| be(v,w,x,y) ),
file('NLP224-1.p',unknown),
[] ).
cnf(614,plain,
( ~ relation(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[22,607]),
[iquote('0:Res:22.1,607.0')] ).
cnf(612,plain,
( ~ relation(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[22,605]),
[iquote('0:Res:22.1,605.0')] ).
cnf(607,plain,
( ~ abstraction(u,skc13)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[24,603]),
[iquote('0:Res:24.1,603.1')] ).
cnf(605,plain,
( ~ abstraction(u,skc17)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[24,602]),
[iquote('0:Res:24.1,602.1')] ).
cnf(66,axiom,
( ~ accessible_world(u,v)
| ~ of(u,w,x)
| of(v,w,x) ),
file('NLP224-1.p',unknown),
[] ).
cnf(603,plain,
( ~ accessible_world(skc9,u)
| ~ nonhuman(u,skc13) ),
inference(res,[status(thm),theory(equality)],[456,226]),
[iquote('0:Res:456.1,226.0')] ).
cnf(602,plain,
( ~ accessible_world(skc9,u)
| ~ nonhuman(u,skc17) ),
inference(res,[status(thm),theory(equality)],[455,226]),
[iquote('0:Res:455.1,226.0')] ).
cnf(226,plain,
( ~ human_person(u,v)
| ~ nonhuman(u,v) ),
inference(res,[status(thm),theory(equality)],[17,33]),
[iquote('0:Res:17.1,33.1')] ).
cnf(592,plain,
( ~ man(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[9,588]),
[iquote('0:Res:9.1,588.0')] ).
cnf(68,axiom,
( ~ accessible_world(u,v)
| ~ theme(u,w,x)
| theme(v,w,x) ),
file('NLP224-1.p',unknown),
[] ).
cnf(590,plain,
( ~ man(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[9,583]),
[iquote('0:Res:9.1,583.0')] ).
cnf(588,plain,
( ~ human_person(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[10,582]),
[iquote('0:Res:10.1,582.0')] ).
cnf(583,plain,
( ~ human_person(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[10,580]),
[iquote('0:Res:10.1,580.0')] ).
cnf(582,plain,
( ~ organism(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[11,569]),
[iquote('0:Res:11.1,569.0')] ).
cnf(67,axiom,
( ~ accessible_world(u,v)
| ~ agent(u,w,x)
| agent(v,w,x) ),
file('NLP224-1.p',unknown),
[] ).
cnf(580,plain,
( ~ organism(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[11,567]),
[iquote('0:Res:11.1,567.0')] ).
cnf(569,plain,
( ~ entity(u,skc10)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[14,565]),
[iquote('0:Res:14.1,565.1')] ).
cnf(567,plain,
( ~ entity(u,skc15)
| ~ accessible_world(skc9,u) ),
inference(res,[status(thm),theory(equality)],[14,564]),
[iquote('0:Res:14.1,564.1')] ).
cnf(572,plain,
( ~ accessible_world(skc14,u)
| forename(u,skc16) ),
inference(res,[status(thm),theory(equality)],[192,54]),
[iquote('0:Res:192.0,54.0')] ).
cnf(54,axiom,
( ~ forename(u,v)
| ~ accessible_world(u,w)
| forename(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(565,plain,
( ~ accessible_world(skc9,u)
| ~ existent(u,skc10) ),
inference(res,[status(thm),theory(equality)],[494,219]),
[iquote('0:Res:494.1,219.0')] ).
cnf(564,plain,
( ~ accessible_world(skc9,u)
| ~ existent(u,skc15) ),
inference(res,[status(thm),theory(equality)],[493,219]),
[iquote('0:Res:493.1,219.0')] ).
cnf(219,plain,
( ~ eventuality(u,v)
| ~ existent(u,v) ),
inference(res,[status(thm),theory(equality)],[5,34]),
[iquote('0:Res:5.1,34.1')] ).
cnf(474,plain,
( ~ accessible_world(skc14,u)
| event(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[214,43]),
[iquote('0:Res:214.0,43.0')] ).
cnf(64,axiom,
( ~ proposition(u,v)
| ~ accessible_world(u,w)
| proposition(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(387,plain,
( ~ accessible_world(skc14,u)
| present(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[210,62]),
[iquote('0:Res:210.0,62.0')] ).
cnf(299,plain,
( ~ accessible_world(skc14,u)
| smoke(u,skf1(v)) ),
inference(res,[status(thm),theory(equality)],[206,61]),
[iquote('0:Res:206.0,61.0')] ).
cnf(512,plain,
( ~ man(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[9,454]),
[iquote('0:Res:9.1,454.0')] ).
cnf(534,plain,
( ~ accessible_world(skc14,u)
| man(u,skc17) ),
inference(res,[status(thm),theory(equality)],[187,44]),
[iquote('0:Res:187.0,44.0')] ).
cnf(44,axiom,
( ~ man(u,v)
| ~ accessible_world(u,w)
| man(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(489,plain,
( ~ smoke(skc9,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[28,436]),
[iquote('0:Res:28.1,436.0')] ).
cnf(467,plain,
( ~ smoke(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[28,345]),
[iquote('0:Res:28.1,345.0')] ).
cnf(516,plain,
( ~ accessible_world(skc14,u)
| think_believe_consider(u,skc15) ),
inference(res,[status(thm),theory(equality)],[196,63]),
[iquote('0:Res:196.0,63.0')] ).
cnf(47,axiom,
( ~ entity(u,v)
| ~ accessible_world(u,w)
| entity(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(521,plain,
~ general(skc9,skc13),
inference(res,[status(thm),theory(equality)],[126,511]),
[iquote('0:Res:126.1,511.0')] ).
cnf(519,plain,
~ general(skc9,skc17),
inference(res,[status(thm),theory(equality)],[126,510]),
[iquote('0:Res:126.1,510.0')] ).
cnf(511,plain,
~ general(skc14,skc13),
inference(res,[status(thm),theory(equality)],[145,454]),
[iquote('0:Res:145.0,454.0')] ).
cnf(510,plain,
~ general(skc14,skc17),
inference(res,[status(thm),theory(equality)],[160,454]),
[iquote('0:Res:160.0,454.0')] ).
cnf(63,axiom,
( ~ think_believe_consider(u,v)
| ~ accessible_world(u,w)
| think_believe_consider(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(454,plain,
( ~ human_person(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[10,339]),
[iquote('0:Res:10.1,339.0')] ).
cnf(447,plain,
( ~ man(skc14,u)
| ~ abstraction(skc9,u) ),
inference(res,[status(thm),theory(equality)],[19,275]),
[iquote('0:Res:19.1,275.1')] ).
cnf(494,plain,
( ~ accessible_world(skc9,u)
| eventuality(u,skc10) ),
inference(res,[status(thm),theory(equality)],[133,37]),
[iquote('0:Res:133.0,37.0')] ).
cnf(493,plain,
( ~ accessible_world(skc9,u)
| eventuality(u,skc15) ),
inference(res,[status(thm),theory(equality)],[152,37]),
[iquote('0:Res:152.0,37.0')] ).
cnf(37,axiom,
( ~ eventuality(u,v)
| ~ accessible_world(u,w)
| eventuality(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(437,plain,
( ~ state(skc9,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[1,274]),
[iquote('0:Res:1.1,274.0')] ).
cnf(436,plain,
( ~ event(skc9,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[8,274]),
[iquote('0:Res:8.1,274.0')] ).
cnf(472,plain,
( ~ accessible_world(skc14,u)
| event(u,skc15) ),
inference(res,[status(thm),theory(equality)],[194,43]),
[iquote('0:Res:194.0,43.0')] ).
cnf(471,plain,
( ~ accessible_world(skc9,u)
| event(u,skc10) ),
inference(res,[status(thm),theory(equality)],[134,43]),
[iquote('0:Res:134.0,43.0')] ).
cnf(43,axiom,
( ~ event(u,v)
| ~ accessible_world(u,w)
| event(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(346,plain,
( ~ state(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[1,271]),
[iquote('0:Res:1.1,271.0')] ).
cnf(345,plain,
( ~ event(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[8,271]),
[iquote('0:Res:8.1,271.0')] ).
cnf(456,plain,
( ~ accessible_world(skc9,u)
| human_person(u,skc13) ),
inference(res,[status(thm),theory(equality)],[145,45]),
[iquote('0:Res:145.0,45.0')] ).
cnf(455,plain,
( ~ accessible_world(skc9,u)
| human_person(u,skc17) ),
inference(res,[status(thm),theory(equality)],[160,45]),
[iquote('0:Res:160.0,45.0')] ).
cnf(45,axiom,
( ~ human_person(u,v)
| ~ accessible_world(u,w)
| human_person(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(339,plain,
( ~ organism(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[11,270]),
[iquote('0:Res:11.1,270.0')] ).
cnf(278,plain,
( ~ man(skc9,u)
| ~ nonhuman(skc14,u) ),
inference(res,[status(thm),theory(equality)],[9,269]),
[iquote('0:Res:9.1,269.0')] ).
cnf(275,plain,
( ~ abstraction(skc9,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[26,243]),
[iquote('0:Res:26.1,243.0')] ).
cnf(440,plain,
~ male(skc9,skc10),
inference(res,[status(thm),theory(equality)],[120,435]),
[iquote('0:Res:120.1,435.0')] ).
cnf(57,axiom,
( ~ abstraction(u,v)
| ~ accessible_world(u,w)
| abstraction(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(438,plain,
~ male(skc9,skc15),
inference(res,[status(thm),theory(equality)],[120,434]),
[iquote('0:Res:120.1,434.0')] ).
cnf(435,plain,
~ male(skc14,skc10),
inference(res,[status(thm),theory(equality)],[133,274]),
[iquote('0:Res:133.0,274.0')] ).
cnf(434,plain,
~ male(skc14,skc15),
inference(res,[status(thm),theory(equality)],[152,274]),
[iquote('0:Res:152.0,274.0')] ).
cnf(274,plain,
( ~ eventuality(skc9,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[6,243]),
[iquote('0:Res:6.1,243.0')] ).
cnf(36,axiom,
( ~ state(u,v)
| ~ accessible_world(u,w)
| state(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(414,plain,
( ~ accessible_world(skc9,u)
| male(u,skc13) ),
inference(res,[status(thm),theory(equality)],[146,53]),
[iquote('0:Res:146.0,53.0')] ).
cnf(413,plain,
( ~ accessible_world(skc9,u)
| male(u,skc17) ),
inference(res,[status(thm),theory(equality)],[161,53]),
[iquote('0:Res:161.0,53.0')] ).
cnf(405,plain,
( ~ accessible_world(skc9,u)
| relname(u,skc12) ),
inference(res,[status(thm),theory(equality)],[142,55]),
[iquote('0:Res:142.0,55.0')] ).
cnf(404,plain,
( ~ accessible_world(skc9,u)
| relname(u,skc16) ),
inference(res,[status(thm),theory(equality)],[157,55]),
[iquote('0:Res:157.0,55.0')] ).
cnf(38,axiom,
( ~ thing(u,v)
| ~ accessible_world(u,w)
| thing(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(394,plain,
( ~ accessible_world(skc9,u)
| relation(u,skc14) ),
inference(res,[status(thm),theory(equality)],[96,56]),
[iquote('0:Res:96.0,56.0')] ).
cnf(384,plain,
( ~ accessible_world(skc14,u)
| present(u,skc15) ),
inference(res,[status(thm),theory(equality)],[195,62]),
[iquote('0:Res:195.0,62.0')] ).
cnf(374,plain,
( ~ accessible_world(skc14,u)
| vincent_forename(u,skc16) ),
inference(res,[status(thm),theory(equality)],[193,65]),
[iquote('0:Res:193.0,65.0')] ).
cnf(411,plain,
~ jules_forename(skc9,skc10),
inference(res,[status(thm),theory(equality)],[27,398]),
[iquote('0:Res:27.1,398.0')] ).
cnf(46,axiom,
( ~ organism(u,v)
| ~ accessible_world(u,w)
| organism(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(410,plain,
~ vincent_forename(skc9,skc10),
inference(res,[status(thm),theory(equality)],[30,398]),
[iquote('0:Res:30.1,398.0')] ).
cnf(403,plain,
~ jules_forename(skc9,skc15),
inference(res,[status(thm),theory(equality)],[27,390]),
[iquote('0:Res:27.1,390.0')] ).
cnf(402,plain,
~ vincent_forename(skc9,skc15),
inference(res,[status(thm),theory(equality)],[30,390]),
[iquote('0:Res:30.1,390.0')] ).
cnf(401,plain,
~ jules_forename(skc14,skc10),
inference(res,[status(thm),theory(equality)],[27,389]),
[iquote('0:Res:27.1,389.0')] ).
cnf(53,axiom,
( ~ male(u,v)
| ~ accessible_world(u,w)
| male(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(400,plain,
~ vincent_forename(skc14,skc10),
inference(res,[status(thm),theory(equality)],[30,389]),
[iquote('0:Res:30.1,389.0')] ).
cnf(398,plain,
~ forename(skc9,skc10),
inference(res,[status(thm),theory(equality)],[20,381]),
[iquote('0:Res:20.1,381.0')] ).
cnf(393,plain,
~ jules_forename(skc14,skc15),
inference(res,[status(thm),theory(equality)],[27,379]),
[iquote('0:Res:27.1,379.0')] ).
cnf(392,plain,
~ vincent_forename(skc14,skc15),
inference(res,[status(thm),theory(equality)],[30,379]),
[iquote('0:Res:30.1,379.0')] ).
cnf(55,axiom,
( ~ relname(u,v)
| ~ accessible_world(u,w)
| relname(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(390,plain,
~ forename(skc9,skc15),
inference(res,[status(thm),theory(equality)],[20,372]),
[iquote('0:Res:20.1,372.0')] ).
cnf(389,plain,
~ forename(skc14,skc10),
inference(res,[status(thm),theory(equality)],[20,370]),
[iquote('0:Res:20.1,370.0')] ).
cnf(381,plain,
~ relname(skc9,skc10),
inference(res,[status(thm),theory(equality)],[21,367]),
[iquote('0:Res:21.1,367.0')] ).
cnf(380,plain,
~ proposition(skc9,skc10),
inference(res,[status(thm),theory(equality)],[29,367]),
[iquote('0:Res:29.1,367.0')] ).
cnf(56,axiom,
( ~ relation(u,v)
| ~ accessible_world(u,w)
| relation(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(379,plain,
~ forename(skc14,skc15),
inference(res,[status(thm),theory(equality)],[20,366]),
[iquote('0:Res:20.1,366.0')] ).
cnf(372,plain,
~ relname(skc9,skc15),
inference(res,[status(thm),theory(equality)],[21,360]),
[iquote('0:Res:21.1,360.0')] ).
cnf(371,plain,
~ proposition(skc9,skc15),
inference(res,[status(thm),theory(equality)],[29,360]),
[iquote('0:Res:29.1,360.0')] ).
cnf(370,plain,
~ relname(skc14,skc10),
inference(res,[status(thm),theory(equality)],[21,358]),
[iquote('0:Res:21.1,358.0')] ).
cnf(62,axiom,
( ~ present(u,v)
| ~ accessible_world(u,w)
| present(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(369,plain,
~ proposition(skc14,skc10),
inference(res,[status(thm),theory(equality)],[29,358]),
[iquote('0:Res:29.1,358.0')] ).
cnf(367,plain,
~ relation(skc9,skc10),
inference(res,[status(thm),theory(equality)],[22,357]),
[iquote('0:Res:22.1,357.0')] ).
cnf(366,plain,
~ relname(skc14,skc15),
inference(res,[status(thm),theory(equality)],[21,355]),
[iquote('0:Res:21.1,355.0')] ).
cnf(365,plain,
~ proposition(skc14,skc15),
inference(res,[status(thm),theory(equality)],[29,355]),
[iquote('0:Res:29.1,355.0')] ).
cnf(65,axiom,
( ~ vincent_forename(u,v)
| ~ accessible_world(u,w)
| vincent_forename(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(360,plain,
~ relation(skc9,skc15),
inference(res,[status(thm),theory(equality)],[22,351]),
[iquote('0:Res:22.1,351.0')] ).
cnf(358,plain,
~ relation(skc14,skc10),
inference(res,[status(thm),theory(equality)],[22,350]),
[iquote('0:Res:22.1,350.0')] ).
cnf(357,plain,
~ abstraction(skc9,skc10),
inference(res,[status(thm),theory(equality)],[25,349]),
[iquote('0:Res:25.1,349.0')] ).
cnf(355,plain,
~ relation(skc14,skc15),
inference(res,[status(thm),theory(equality)],[22,348]),
[iquote('0:Res:22.1,348.0')] ).
cnf(40,axiom,
( ~ specific(u,v)
| ~ accessible_world(u,w)
| specific(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(351,plain,
~ abstraction(skc9,skc15),
inference(res,[status(thm),theory(equality)],[25,347]),
[iquote('0:Res:25.1,347.0')] ).
cnf(350,plain,
~ abstraction(skc14,skc10),
inference(res,[status(thm),theory(equality)],[25,344]),
[iquote('0:Res:25.1,344.0')] ).
cnf(349,plain,
~ general(skc9,skc10),
inference(res,[status(thm),theory(equality)],[126,344]),
[iquote('0:Res:126.1,344.0')] ).
cnf(348,plain,
~ abstraction(skc14,skc15),
inference(res,[status(thm),theory(equality)],[25,343]),
[iquote('0:Res:25.1,343.0')] ).
cnf(42,axiom,
( ~ unisex(u,v)
| ~ accessible_world(u,w)
| unisex(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(347,plain,
~ general(skc9,skc15),
inference(res,[status(thm),theory(equality)],[126,343]),
[iquote('0:Res:126.1,343.0')] ).
cnf(344,plain,
~ general(skc14,skc10),
inference(res,[status(thm),theory(equality)],[133,271]),
[iquote('0:Res:133.0,271.0')] ).
cnf(343,plain,
~ general(skc14,skc15),
inference(res,[status(thm),theory(equality)],[152,271]),
[iquote('0:Res:152.0,271.0')] ).
cnf(271,plain,
( ~ eventuality(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[4,234]),
[iquote('0:Res:4.1,234.0')] ).
cnf(60,axiom,
( ~ jules_forename(u,v)
| ~ accessible_world(u,w)
| jules_forename(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(270,plain,
( ~ entity(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[13,234]),
[iquote('0:Res:13.1,234.0')] ).
cnf(334,plain,
~ jules_forename(skc9,skc13),
inference(res,[status(thm),theory(equality)],[27,321]),
[iquote('0:Res:27.1,321.0')] ).
cnf(333,plain,
~ vincent_forename(skc9,skc13),
inference(res,[status(thm),theory(equality)],[30,321]),
[iquote('0:Res:30.1,321.0')] ).
cnf(328,plain,
~ jules_forename(skc9,skc17),
inference(res,[status(thm),theory(equality)],[27,317]),
[iquote('0:Res:27.1,317.0')] ).
cnf(41,axiom,
( ~ nonexistent(u,v)
| ~ accessible_world(u,w)
| nonexistent(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(327,plain,
~ vincent_forename(skc9,skc17),
inference(res,[status(thm),theory(equality)],[30,317]),
[iquote('0:Res:30.1,317.0')] ).
cnf(326,plain,
~ jules_forename(skc14,skc13),
inference(res,[status(thm),theory(equality)],[27,314]),
[iquote('0:Res:27.1,314.0')] ).
cnf(325,plain,
~ vincent_forename(skc14,skc13),
inference(res,[status(thm),theory(equality)],[30,314]),
[iquote('0:Res:30.1,314.0')] ).
cnf(321,plain,
~ forename(skc9,skc13),
inference(res,[status(thm),theory(equality)],[20,311]),
[iquote('0:Res:20.1,311.0')] ).
cnf(48,axiom,
( ~ existent(u,v)
| ~ accessible_world(u,w)
| existent(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(320,plain,
~ jules_forename(skc14,skc17),
inference(res,[status(thm),theory(equality)],[27,307]),
[iquote('0:Res:27.1,307.0')] ).
cnf(319,plain,
~ vincent_forename(skc14,skc17),
inference(res,[status(thm),theory(equality)],[30,307]),
[iquote('0:Res:30.1,307.0')] ).
cnf(317,plain,
~ forename(skc9,skc17),
inference(res,[status(thm),theory(equality)],[20,304]),
[iquote('0:Res:20.1,304.0')] ).
cnf(314,plain,
~ forename(skc14,skc13),
inference(res,[status(thm),theory(equality)],[20,302]),
[iquote('0:Res:20.1,302.0')] ).
cnf(51,axiom,
( ~ human(u,v)
| ~ accessible_world(u,w)
| human(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(311,plain,
~ relname(skc9,skc13),
inference(res,[status(thm),theory(equality)],[21,297]),
[iquote('0:Res:21.1,297.0')] ).
cnf(310,plain,
~ proposition(skc9,skc13),
inference(res,[status(thm),theory(equality)],[29,297]),
[iquote('0:Res:29.1,297.0')] ).
cnf(307,plain,
~ forename(skc14,skc17),
inference(res,[status(thm),theory(equality)],[20,296]),
[iquote('0:Res:20.1,296.0')] ).
cnf(304,plain,
~ relname(skc9,skc17),
inference(res,[status(thm),theory(equality)],[21,293]),
[iquote('0:Res:21.1,293.0')] ).
cnf(58,axiom,
( ~ nonhuman(u,v)
| ~ accessible_world(u,w)
| nonhuman(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(303,plain,
~ proposition(skc9,skc17),
inference(res,[status(thm),theory(equality)],[29,293]),
[iquote('0:Res:29.1,293.0')] ).
cnf(302,plain,
~ relname(skc14,skc13),
inference(res,[status(thm),theory(equality)],[21,291]),
[iquote('0:Res:21.1,291.0')] ).
cnf(301,plain,
~ proposition(skc14,skc13),
inference(res,[status(thm),theory(equality)],[29,291]),
[iquote('0:Res:29.1,291.0')] ).
cnf(297,plain,
~ relation(skc9,skc13),
inference(res,[status(thm),theory(equality)],[22,288]),
[iquote('0:Res:22.1,288.0')] ).
cnf(59,axiom,
( ~ general(u,v)
| ~ accessible_world(u,w)
| general(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(296,plain,
~ relname(skc14,skc17),
inference(res,[status(thm),theory(equality)],[21,286]),
[iquote('0:Res:21.1,286.0')] ).
cnf(295,plain,
~ proposition(skc14,skc17),
inference(res,[status(thm),theory(equality)],[29,286]),
[iquote('0:Res:29.1,286.0')] ).
cnf(293,plain,
~ relation(skc9,skc17),
inference(res,[status(thm),theory(equality)],[22,285]),
[iquote('0:Res:22.1,285.0')] ).
cnf(291,plain,
~ relation(skc14,skc13),
inference(res,[status(thm),theory(equality)],[22,284]),
[iquote('0:Res:22.1,284.0')] ).
cnf(61,axiom,
( ~ smoke(u,v)
| ~ accessible_world(u,w)
| smoke(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(288,plain,
~ abstraction(skc9,skc13),
inference(res,[status(thm),theory(equality)],[24,283]),
[iquote('0:Res:24.1,283.0')] ).
cnf(286,plain,
~ relation(skc14,skc17),
inference(res,[status(thm),theory(equality)],[22,280]),
[iquote('0:Res:22.1,280.0')] ).
cnf(285,plain,
~ abstraction(skc9,skc17),
inference(res,[status(thm),theory(equality)],[24,279]),
[iquote('0:Res:24.1,279.0')] ).
cnf(284,plain,
~ abstraction(skc14,skc13),
inference(res,[status(thm),theory(equality)],[24,277]),
[iquote('0:Res:24.1,277.0')] ).
cnf(39,axiom,
( ~ singleton(u,v)
| ~ accessible_world(u,w)
| singleton(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(283,plain,
~ nonhuman(skc9,skc13),
inference(res,[status(thm),theory(equality)],[125,277]),
[iquote('0:Res:125.1,277.0')] ).
cnf(280,plain,
~ abstraction(skc14,skc17),
inference(res,[status(thm),theory(equality)],[24,276]),
[iquote('0:Res:24.1,276.0')] ).
cnf(279,plain,
~ nonhuman(skc9,skc17),
inference(res,[status(thm),theory(equality)],[125,276]),
[iquote('0:Res:125.1,276.0')] ).
cnf(277,plain,
~ nonhuman(skc14,skc13),
inference(res,[status(thm),theory(equality)],[145,269]),
[iquote('0:Res:145.0,269.0')] ).
cnf(49,axiom,
( ~ impartial(u,v)
| ~ accessible_world(u,w)
| impartial(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(276,plain,
~ nonhuman(skc14,skc17),
inference(res,[status(thm),theory(equality)],[160,269]),
[iquote('0:Res:160.0,269.0')] ).
cnf(269,plain,
( ~ human_person(skc9,u)
| ~ nonhuman(skc14,u) ),
inference(res,[status(thm),theory(equality)],[17,225]),
[iquote('0:Res:17.1,225.0')] ).
cnf(266,plain,
( ~ smoke(skc9,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[28,223]),
[iquote('0:Res:28.1,223.0')] ).
cnf(243,plain,
( ~ unisex(skc9,u)
| ~ male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[109,31]),
[iquote('0:Res:109.1,31.0')] ).
cnf(50,axiom,
( ~ living(u,v)
| ~ accessible_world(u,w)
| living(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(234,plain,
( ~ specific(skc9,u)
| ~ general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[107,32]),
[iquote('0:Res:107.1,32.0')] ).
cnf(225,plain,
( ~ human(skc9,u)
| ~ nonhuman(skc14,u) ),
inference(res,[status(thm),theory(equality)],[118,33]),
[iquote('0:Res:118.1,33.1')] ).
cnf(224,plain,
( ~ state(skc9,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[1,220]),
[iquote('0:Res:1.1,220.0')] ).
cnf(223,plain,
( ~ event(skc9,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[8,220]),
[iquote('0:Res:8.1,220.0')] ).
cnf(52,axiom,
( ~ animate(u,v)
| ~ accessible_world(u,w)
| animate(w,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(258,plain,
~ man(skc9,skc10),
inference(res,[status(thm),theory(equality)],[9,252]),
[iquote('0:Res:9.1,252.0')] ).
cnf(255,plain,
~ man(skc9,skc15),
inference(res,[status(thm),theory(equality)],[9,249]),
[iquote('0:Res:9.1,249.0')] ).
cnf(253,plain,
~ man(skc14,skc10),
inference(res,[status(thm),theory(equality)],[9,247]),
[iquote('0:Res:9.1,247.0')] ).
cnf(252,plain,
~ human_person(skc9,skc10),
inference(res,[status(thm),theory(equality)],[10,246]),
[iquote('0:Res:10.1,246.0')] ).
cnf(35,axiom,
( ~ be(u,v,w,x)
| equal(w,x) ),
file('NLP224-1.p',unknown),
[] ).
cnf(250,plain,
~ man(skc14,skc15),
inference(res,[status(thm),theory(equality)],[9,241]),
[iquote('0:Res:9.1,241.0')] ).
cnf(249,plain,
~ human_person(skc9,skc15),
inference(res,[status(thm),theory(equality)],[10,240]),
[iquote('0:Res:10.1,240.0')] ).
cnf(247,plain,
~ human_person(skc14,skc10),
inference(res,[status(thm),theory(equality)],[10,239]),
[iquote('0:Res:10.1,239.0')] ).
cnf(246,plain,
~ organism(skc9,skc10),
inference(res,[status(thm),theory(equality)],[11,237]),
[iquote('0:Res:11.1,237.0')] ).
cnf(94,axiom,
( ~ man(skc14,u)
| agent(skc14,skf1(u),u) ),
file('NLP224-1.p',unknown),
[] ).
cnf(241,plain,
~ human_person(skc14,skc15),
inference(res,[status(thm),theory(equality)],[10,233]),
[iquote('0:Res:10.1,233.0')] ).
cnf(240,plain,
~ organism(skc9,skc15),
inference(res,[status(thm),theory(equality)],[11,231]),
[iquote('0:Res:11.1,231.0')] ).
cnf(239,plain,
~ organism(skc14,skc10),
inference(res,[status(thm),theory(equality)],[11,230]),
[iquote('0:Res:11.1,230.0')] ).
cnf(237,plain,
~ entity(skc9,skc10),
inference(res,[status(thm),theory(equality)],[14,229]),
[iquote('0:Res:14.1,229.0')] ).
cnf(31,axiom,
( ~ unisex(u,v)
| ~ male(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(233,plain,
~ organism(skc14,skc15),
inference(res,[status(thm),theory(equality)],[11,228]),
[iquote('0:Res:11.1,228.0')] ).
cnf(231,plain,
~ entity(skc9,skc15),
inference(res,[status(thm),theory(equality)],[14,227]),
[iquote('0:Res:14.1,227.0')] ).
cnf(230,plain,
~ entity(skc14,skc10),
inference(res,[status(thm),theory(equality)],[14,222]),
[iquote('0:Res:14.1,222.0')] ).
cnf(229,plain,
~ existent(skc9,skc10),
inference(res,[status(thm),theory(equality)],[115,222]),
[iquote('0:Res:115.1,222.0')] ).
cnf(32,axiom,
( ~ specific(u,v)
| ~ general(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(228,plain,
~ entity(skc14,skc15),
inference(res,[status(thm),theory(equality)],[14,221]),
[iquote('0:Res:14.1,221.0')] ).
cnf(227,plain,
~ existent(skc9,skc15),
inference(res,[status(thm),theory(equality)],[115,221]),
[iquote('0:Res:115.1,221.0')] ).
cnf(222,plain,
~ existent(skc14,skc10),
inference(res,[status(thm),theory(equality)],[133,220]),
[iquote('0:Res:133.0,220.0')] ).
cnf(221,plain,
~ existent(skc14,skc15),
inference(res,[status(thm),theory(equality)],[152,220]),
[iquote('0:Res:152.0,220.0')] ).
cnf(33,axiom,
( ~ nonhuman(u,v)
| ~ human(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(220,plain,
( ~ eventuality(skc9,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[5,218]),
[iquote('0:Res:5.1,218.0')] ).
cnf(218,plain,
( ~ nonexistent(skc9,u)
| ~ existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[108,34]),
[iquote('0:Res:108.1,34.1')] ).
cnf(164,plain,
( ~ accessible_world(skc9,u)
| of(u,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[89,66]),
[iquote('0:Res:89.0,66.1')] ).
cnf(173,plain,
( ~ accessible_world(skc9,u)
| of(u,skc16,skc17) ),
inference(res,[status(thm),theory(equality)],[86,66]),
[iquote('0:Res:86.0,66.1')] ).
cnf(34,axiom,
( ~ existent(u,v)
| ~ nonexistent(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(166,plain,
( ~ accessible_world(skc9,u)
| theme(u,skc15,skc14) ),
inference(res,[status(thm),theory(equality)],[88,68]),
[iquote('0:Res:88.0,68.1')] ).
cnf(169,plain,
( ~ accessible_world(skc9,u)
| agent(u,skc15,skc17) ),
inference(res,[status(thm),theory(equality)],[87,67]),
[iquote('0:Res:87.0,67.1')] ).
cnf(214,plain,
event(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[187,93]),
[iquote('0:Res:187.0,93.0')] ).
cnf(210,plain,
present(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[187,92]),
[iquote('0:Res:187.0,92.0')] ).
cnf(206,plain,
smoke(skc14,skf1(u)),
inference(res,[status(thm),theory(equality)],[187,91]),
[iquote('0:Res:187.0,91.0')] ).
cnf(30,axiom,
( ~ vincent_forename(u,v)
| forename(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(27,axiom,
( ~ jules_forename(u,v)
| forename(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(11,axiom,
( ~ organism(u,v)
| entity(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ event(u,v)
| eventuality(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(1,axiom,
( ~ state(u,v)
| eventuality(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ state(u,v)
| event(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(28,axiom,
( ~ smoke(u,v)
| event(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(9,axiom,
( ~ man(u,v)
| human_person(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ relation(u,v)
| abstraction(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ forename(u,v)
| relname(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ proposition(u,v)
| relation(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(12,axiom,
( ~ entity(u,v)
| thing(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ man(u,v)
| male(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ eventuality(u,v)
| thing(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ human_person(u,v)
| organism(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ abstraction(u,v)
| thing(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ relname(u,v)
| relation(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(13,axiom,
( ~ entity(u,v)
| specific(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ eventuality(u,v)
| specific(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ eventuality(u,v)
| unisex(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(98,plain,
( ~ accessible_world(skc9,u)
| proposition(u,skc14) ),
inference(res,[status(thm),theory(equality)],[85,64]),
[iquote('0:Res:85.0,64.1')] ).
cnf(26,axiom,
( ~ abstraction(u,v)
| unisex(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(144,plain,
( ~ accessible_world(skc9,u)
| forename(u,skc12) ),
inference(res,[status(thm),theory(equality)],[80,54]),
[iquote('0:Res:80.0,54.1')] ).
cnf(159,plain,
( ~ accessible_world(skc9,u)
| forename(u,skc16) ),
inference(res,[status(thm),theory(equality)],[74,54]),
[iquote('0:Res:74.0,54.1')] ).
cnf(181,plain,
( ~ accessible_world(skc9,u)
| man(u,skc13) ),
inference(rew,[status(thm),theory(equality)],[175,138]),
[iquote('0:Rew:175.0,138.1')] ).
cnf(162,plain,
( ~ accessible_world(skc9,u)
| man(u,skc17) ),
inference(res,[status(thm),theory(equality)],[73,44]),
[iquote('0:Res:73.0,44.1')] ).
cnf(14,axiom,
( ~ entity(u,v)
| existent(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(148,plain,
( ~ accessible_world(skc9,u)
| think_believe_consider(u,skc15) ),
inference(res,[status(thm),theory(equality)],[78,63]),
[iquote('0:Res:78.0,63.1')] ).
cnf(153,plain,
( ~ accessible_world(skc9,u)
| event(u,skc15) ),
inference(res,[status(thm),theory(equality)],[76,43]),
[iquote('0:Res:76.0,43.1')] ).
cnf(135,plain,
( ~ accessible_world(skc9,u)
| state(u,skc10) ),
inference(res,[status(thm),theory(equality)],[83,36]),
[iquote('0:Res:83.0,36.1')] ).
cnf(151,plain,
( ~ accessible_world(skc9,u)
| present(u,skc15) ),
inference(res,[status(thm),theory(equality)],[77,62]),
[iquote('0:Res:77.0,62.1')] ).
cnf(5,axiom,
( ~ eventuality(u,v)
| nonexistent(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(155,plain,
( ~ accessible_world(skc9,u)
| vincent_forename(u,skc16) ),
inference(res,[status(thm),theory(equality)],[75,65]),
[iquote('0:Res:75.0,65.1')] ).
cnf(140,plain,
( ~ accessible_world(skc9,u)
| jules_forename(u,skc12) ),
inference(res,[status(thm),theory(equality)],[81,60]),
[iquote('0:Res:81.0,60.1')] ).
cnf(121,plain,
( ~ forename(skc9,u)
| forename(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,54]),
[iquote('0:Res:84.0,54.0')] ).
cnf(131,plain,
( ~ proposition(skc9,u)
| proposition(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,64]),
[iquote('0:Res:84.0,64.0')] ).
cnf(17,axiom,
( ~ human_person(u,v)
| human(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(111,plain,
( ~ man(skc9,u)
| man(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,44]),
[iquote('0:Res:84.0,44.0')] ).
cnf(114,plain,
( ~ entity(skc9,u)
| entity(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,47]),
[iquote('0:Res:84.0,47.0')] ).
cnf(130,plain,
( ~ think_believe_consider(skc9,u)
| think_believe_consider(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,63]),
[iquote('0:Res:84.0,63.0')] ).
cnf(104,plain,
( ~ eventuality(skc9,u)
| eventuality(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,37]),
[iquote('0:Res:84.0,37.0')] ).
cnf(24,axiom,
( ~ abstraction(u,v)
| nonhuman(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(110,plain,
( ~ event(skc9,u)
| event(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,43]),
[iquote('0:Res:84.0,43.0')] ).
cnf(112,plain,
( ~ human_person(skc9,u)
| human_person(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,45]),
[iquote('0:Res:84.0,45.0')] ).
cnf(124,plain,
( ~ abstraction(skc9,u)
| abstraction(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,57]),
[iquote('0:Res:84.0,57.0')] ).
cnf(103,plain,
( ~ state(skc9,u)
| state(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,36]),
[iquote('0:Res:84.0,36.0')] ).
cnf(25,axiom,
( ~ abstraction(u,v)
| general(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(105,plain,
( ~ thing(skc9,u)
| thing(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,38]),
[iquote('0:Res:84.0,38.0')] ).
cnf(113,plain,
( ~ organism(skc9,u)
| organism(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,46]),
[iquote('0:Res:84.0,46.0')] ).
cnf(120,plain,
( ~ male(skc9,u)
| male(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,53]),
[iquote('0:Res:84.0,53.0')] ).
cnf(122,plain,
( ~ relname(skc9,u)
| relname(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,55]),
[iquote('0:Res:84.0,55.0')] ).
cnf(18,axiom,
( ~ human_person(u,v)
| animate(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(123,plain,
( ~ relation(skc9,u)
| relation(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,56]),
[iquote('0:Res:84.0,56.0')] ).
cnf(129,plain,
( ~ present(skc9,u)
| present(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,62]),
[iquote('0:Res:84.0,62.0')] ).
cnf(132,plain,
( ~ vincent_forename(skc9,u)
| vincent_forename(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,65]),
[iquote('0:Res:84.0,65.0')] ).
cnf(107,plain,
( ~ specific(skc9,u)
| specific(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,40]),
[iquote('0:Res:84.0,40.0')] ).
cnf(3,axiom,
( ~ thing(u,v)
| singleton(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(109,plain,
( ~ unisex(skc9,u)
| unisex(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,42]),
[iquote('0:Res:84.0,42.0')] ).
cnf(127,plain,
( ~ jules_forename(skc9,u)
| jules_forename(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,60]),
[iquote('0:Res:84.0,60.0')] ).
cnf(108,plain,
( ~ nonexistent(skc9,u)
| nonexistent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,41]),
[iquote('0:Res:84.0,41.0')] ).
cnf(115,plain,
( ~ existent(skc9,u)
| existent(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,48]),
[iquote('0:Res:84.0,48.0')] ).
cnf(15,axiom,
( ~ organism(u,v)
| impartial(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(118,plain,
( ~ human(skc9,u)
| human(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,51]),
[iquote('0:Res:84.0,51.0')] ).
cnf(125,plain,
( ~ nonhuman(skc9,u)
| nonhuman(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,58]),
[iquote('0:Res:84.0,58.0')] ).
cnf(126,plain,
( ~ general(skc9,u)
| general(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,59]),
[iquote('0:Res:84.0,59.0')] ).
cnf(128,plain,
( ~ smoke(skc9,u)
| smoke(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,61]),
[iquote('0:Res:84.0,61.0')] ).
cnf(16,axiom,
( ~ organism(u,v)
| living(u,v) ),
file('NLP224-1.p',unknown),
[] ).
cnf(106,plain,
( ~ singleton(skc9,u)
| singleton(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,39]),
[iquote('0:Res:84.0,39.0')] ).
cnf(116,plain,
( ~ impartial(skc9,u)
| impartial(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,49]),
[iquote('0:Res:84.0,49.0')] ).
cnf(117,plain,
( ~ living(skc9,u)
| living(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,50]),
[iquote('0:Res:84.0,50.0')] ).
cnf(119,plain,
( ~ animate(skc9,u)
| animate(skc14,u) ),
inference(res,[status(thm),theory(equality)],[84,52]),
[iquote('0:Res:84.0,52.0')] ).
cnf(178,plain,
be(skc9,skc10,skc13,skc13),
inference(rew,[status(thm),theory(equality)],[175,90]),
[iquote('0:Rew:175.0,90.0')] ).
cnf(192,plain,
forename(skc14,skc16),
inference(res,[status(thm),theory(equality)],[74,121]),
[iquote('0:Res:74.0,121.0')] ).
cnf(187,plain,
man(skc14,skc17),
inference(res,[status(thm),theory(equality)],[73,111]),
[iquote('0:Res:73.0,111.0')] ).
cnf(196,plain,
think_believe_consider(skc14,skc15),
inference(res,[status(thm),theory(equality)],[78,130]),
[iquote('0:Res:78.0,130.0')] ).
cnf(194,plain,
event(skc14,skc15),
inference(res,[status(thm),theory(equality)],[76,110]),
[iquote('0:Res:76.0,110.0')] ).
cnf(86,axiom,
of(skc9,skc16,skc17),
file('NLP224-1.p',unknown),
[] ).
cnf(195,plain,
present(skc14,skc15),
inference(res,[status(thm),theory(equality)],[77,129]),
[iquote('0:Res:77.0,129.0')] ).
cnf(193,plain,
vincent_forename(skc14,skc16),
inference(res,[status(thm),theory(equality)],[75,132]),
[iquote('0:Res:75.0,132.0')] ).
cnf(133,plain,
eventuality(skc9,skc10),
inference(res,[status(thm),theory(equality)],[83,1]),
[iquote('0:Res:83.0,1.0')] ).
cnf(134,plain,
event(skc9,skc10),
inference(res,[status(thm),theory(equality)],[83,7]),
[iquote('0:Res:83.0,7.0')] ).
cnf(89,axiom,
of(skc9,skc12,skc13),
file('NLP224-1.p',unknown),
[] ).
cnf(152,plain,
eventuality(skc9,skc15),
inference(res,[status(thm),theory(equality)],[76,8]),
[iquote('0:Res:76.0,8.0')] ).
cnf(145,plain,
human_person(skc9,skc13),
inference(res,[status(thm),theory(equality)],[79,9]),
[iquote('0:Res:79.0,9.0')] ).
cnf(160,plain,
human_person(skc9,skc17),
inference(res,[status(thm),theory(equality)],[73,9]),
[iquote('0:Res:73.0,9.0')] ).
cnf(96,plain,
relation(skc9,skc14),
inference(res,[status(thm),theory(equality)],[85,29]),
[iquote('0:Res:85.0,29.0')] ).
cnf(88,axiom,
theme(skc9,skc15,skc14),
file('NLP224-1.p',unknown),
[] ).
cnf(142,plain,
relname(skc9,skc12),
inference(res,[status(thm),theory(equality)],[80,20]),
[iquote('0:Res:80.0,20.0')] ).
cnf(146,plain,
male(skc9,skc13),
inference(res,[status(thm),theory(equality)],[79,19]),
[iquote('0:Res:79.0,19.0')] ).
cnf(157,plain,
relname(skc9,skc16),
inference(res,[status(thm),theory(equality)],[74,20]),
[iquote('0:Res:74.0,20.0')] ).
cnf(161,plain,
male(skc9,skc17),
inference(res,[status(thm),theory(equality)],[73,19]),
[iquote('0:Res:73.0,19.0')] ).
cnf(87,axiom,
agent(skc9,skc15,skc17),
file('NLP224-1.p',unknown),
[] ).
cnf(175,plain,
equal(skc11,skc13),
inference(res,[status(thm),theory(equality)],[90,35]),
[iquote('0:Res:90.0,35.0')] ).
cnf(84,axiom,
accessible_world(skc9,skc14),
file('NLP224-1.p',unknown),
[] ).
cnf(74,axiom,
forename(skc9,skc16),
file('NLP224-1.p',unknown),
[] ).
cnf(80,axiom,
forename(skc9,skc12),
file('NLP224-1.p',unknown),
[] ).
cnf(85,axiom,
proposition(skc9,skc14),
file('NLP224-1.p',unknown),
[] ).
cnf(73,axiom,
man(skc9,skc17),
file('NLP224-1.p',unknown),
[] ).
cnf(79,axiom,
man(skc9,skc13),
file('NLP224-1.p',unknown),
[] ).
cnf(78,axiom,
think_believe_consider(skc9,skc15),
file('NLP224-1.p',unknown),
[] ).
cnf(76,axiom,
event(skc9,skc15),
file('NLP224-1.p',unknown),
[] ).
cnf(75,axiom,
vincent_forename(skc9,skc16),
file('NLP224-1.p',unknown),
[] ).
cnf(77,axiom,
present(skc9,skc15),
file('NLP224-1.p',unknown),
[] ).
cnf(83,axiom,
state(skc9,skc10),
file('NLP224-1.p',unknown),
[] ).
cnf(81,axiom,
jules_forename(skc9,skc12),
file('NLP224-1.p',unknown),
[] ).
cnf(72,axiom,
actual_world(skc9),
file('NLP224-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP224-1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Thu Jun 30 18:59:15 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.72/0.92
% 0.72/0.92 SPASS V 3.9
% 0.72/0.92 SPASS beiseite: Completion found.
% 0.72/0.92 % SZS status CounterSatisfiable
% 0.72/0.92 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.92 SPASS derived 4805 clauses, backtracked 0 clauses, performed 0 splits and kept 1326 clauses.
% 0.72/0.92 SPASS allocated 66012 KBytes.
% 0.72/0.92 SPASS spent 0:00:00.57 on the problem.
% 0.72/0.92 0:00:00.04 for the input.
% 0.72/0.92 0:00:00.00 for the FLOTTER CNF translation.
% 0.72/0.92 0:00:00.06 for inferences.
% 0.72/0.92 0:00:00.00 for the backtracking.
% 0.72/0.92 0:00:00.40 for the reduction.
% 0.72/0.92
% 0.72/0.92
% 0.72/0.92 The saturated set of worked-off clauses is :
% 0.72/0.92 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------