SPASS---3.9.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : SPASS---3.9
% Problem  : NLP024-10 : TPTP v8.1.0. Released v7.5.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:25:49 EDT 2022

% Result   : Satisfiable 1.57s 1.75s
% Output   : Saturation 1.59s
% Verified : 
% SZS Type : ERROR: Analysing output (Could not find formula named 2039)

% Comments : 
%------------------------------------------------------------------------------
cnf(2041,plain,
    equal(ifeq(tuple(dance(skc10,skc9),true__dfg,desire_want(skc8,u),true__dfg,true__dfg,true__dfg,present(skc8,u),agent(skc10,skc9,skc15),agent(skc8,u,skc15),theme(skc8,u,skc10)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[2040,2006]),
    [iquote('0:Rew:2040.0,2006.0')] ).

cnf(3301,plain,
    equal(ifeq(tuple(dance(skc10,skc9),true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,agent(skc10,skc9,skc15),agent(skc8,skc9,skc15),true__dfg),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[2040,3298]),
    [iquote('0:Rew:2040.0,3298.0')] ).

cnf(4073,plain,
    equal(ifeq4(theme(skc10,skc9,u),true__dfg,ifeq4(theme(skc10,skc9,v),true__dfg,ifeq4(proposition(skc10,u),true__dfg,ifeq4(proposition(skc10,v),true__dfg,u,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,4064]),
    [iquote('0:Rew:1.0,4064.0')] ).

cnf(1741,plain,
    equal(ifeq4(of(skc10,skc14,u),true__dfg,ifeq4(of(skc10,v,u),true__dfg,ifeq4(entity(skc10,u),true__dfg,ifeq4(forename(skc10,v),true__dfg,skc14,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1722]),
    [iquote('0:Rew:1.0,1722.0')] ).

cnf(1740,plain,
    equal(ifeq4(of(skc10,skc11,u),true__dfg,ifeq4(of(skc10,v,u),true__dfg,ifeq4(entity(skc10,u),true__dfg,ifeq4(forename(skc10,v),true__dfg,skc11,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1723]),
    [iquote('0:Rew:1.0,1723.0')] ).

cnf(1739,plain,
    equal(ifeq4(of(skc8,u,skc15),true__dfg,ifeq4(of(skc8,v,skc15),true__dfg,ifeq4(forename(skc8,u),true__dfg,ifeq4(forename(skc8,v),true__dfg,u,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1724]),
    [iquote('0:Rew:1.0,1724.0')] ).

cnf(1738,plain,
    equal(ifeq4(of(skc8,u,skc12),true__dfg,ifeq4(of(skc8,v,skc12),true__dfg,ifeq4(forename(skc8,u),true__dfg,ifeq4(forename(skc8,v),true__dfg,u,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1725]),
    [iquote('0:Rew:1.0,1725.0')] ).

cnf(4148,plain,
    equal(ifeq4(of(skc10,skc11,skc15),true__dfg,ifeq4(of(skc10,u,skc15),true__dfg,ifeq4(forename(skc10,u),true__dfg,skc11,u),u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,4143]),
    [iquote('0:Rew:1.0,4143.0')] ).

cnf(1737,plain,
    equal(ifeq4(of(skc10,u,skc15),true__dfg,ifeq4(of(skc10,v,skc15),true__dfg,ifeq4(forename(skc10,u),true__dfg,ifeq4(forename(skc10,v),true__dfg,u,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1726]),
    [iquote('0:Rew:1.0,1726.0')] ).

cnf(4116,plain,
    equal(ifeq4(of(skc10,skc14,skc12),true__dfg,ifeq4(of(skc10,u,skc12),true__dfg,ifeq4(forename(skc10,u),true__dfg,skc14,u),u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,4109]),
    [iquote('0:Rew:1.0,4109.0')] ).

cnf(1988,plain,
    equal(ifeq4(theme(skc10,skc9,u),true__dfg,ifeq4(theme(skc10,v,w),true__dfg,ifeq4(proposition(skc10,u),true__dfg,ifeq4(proposition(skc10,w),true__dfg,ifeq4(desire_want(skc10,v),true__dfg,u,w),w),w),w),w),w),
    inference(rew,[status(thm),theory(equality)],[1,1978]),
    [iquote('0:Rew:1.0,1978.0')] ).

cnf(1736,plain,
    equal(ifeq4(of(skc10,u,skc12),true__dfg,ifeq4(of(skc10,v,skc12),true__dfg,ifeq4(forename(skc10,u),true__dfg,ifeq4(forename(skc10,v),true__dfg,u,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1727]),
    [iquote('0:Rew:1.0,1727.0')] ).

cnf(4026,plain,
    equal(ifeq4(theme(skc10,u,skc10),true__dfg,ifeq4(theme(skc10,skc9,v),true__dfg,ifeq4(proposition(skc10,v),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,skc10,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,4017]),
    [iquote('0:Rew:1.0,4017.0')] ).

cnf(4054,plain,
    equal(ifeq4(of(skc10,skc14,u),true__dfg,ifeq4(of(skc10,skc14,u),true__dfg,ifeq4(entity(skc10,u),true__dfg,skc14,skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,4041]),
    [iquote('0:Rew:1.0,4041.0')] ).

cnf(4053,plain,
    equal(ifeq4(of(skc10,skc11,u),true__dfg,ifeq4(of(skc10,skc14,u),true__dfg,ifeq4(entity(skc10,u),true__dfg,skc11,skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,4042]),
    [iquote('0:Rew:1.0,4042.0')] ).

cnf(1987,plain,
    equal(ifeq4(theme(skc10,u,v),true__dfg,ifeq4(theme(skc10,skc9,w),true__dfg,ifeq4(proposition(skc10,v),true__dfg,ifeq4(proposition(skc10,w),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,v,w),w),w),w),w),w),
    inference(rew,[status(thm),theory(equality)],[1,1979]),
    [iquote('0:Rew:1.0,1979.0')] ).

cnf(4061,plain,
    equal(ifeq4(of(skc10,skc14,skc12),true__dfg,ifeq4(of(skc10,skc14,skc12),true__dfg,skc14,skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,4056]),
    [iquote('0:Rew:1.0,4056.0')] ).

cnf(4051,plain,
    equal(ifeq4(of(skc10,u,skc12),true__dfg,ifeq4(of(skc10,skc14,skc12),true__dfg,ifeq4(forename(skc10,u),true__dfg,u,skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,4044]),
    [iquote('0:Rew:1.0,4044.0')] ).

cnf(1745,plain,
    equal(ifeq4(of(skc10,u,v),true__dfg,ifeq4(of(skc10,skc14,v),true__dfg,ifeq4(entity(skc10,v),true__dfg,ifeq4(forename(skc10,u),true__dfg,u,skc14),skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,1718]),
    [iquote('0:Rew:1.0,1718.0')] ).

cnf(3985,plain,
    equal(ifeq4(theme(skc10,skc9,u),true__dfg,ifeq4(theme(skc10,v,skc10),true__dfg,ifeq4(proposition(skc10,u),true__dfg,ifeq4(desire_want(skc10,v),true__dfg,u,skc10),skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,3978]),
    [iquote('0:Rew:1.0,3978.0')] ).

cnf(1940,plain,
    equal(ifeq4(theme(skc10,u,skc10),true__dfg,ifeq4(theme(skc10,v,w),true__dfg,ifeq4(proposition(skc10,w),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,ifeq4(desire_want(skc10,v),true__dfg,skc10,w),w),w),w),w),w),
    inference(rew,[status(thm),theory(equality)],[1,1936]),
    [iquote('0:Rew:1.0,1936.0')] ).

cnf(3984,plain,
    equal(ifeq4(theme(skc10,u,skc10),true__dfg,ifeq4(theme(skc10,v,skc10),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,ifeq4(desire_want(skc10,v),true__dfg,skc10,skc10),skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,3979]),
    [iquote('0:Rew:1.0,3979.0')] ).

cnf(3968,plain,
    equal(ifeq4(of(skc10,skc14,u),true__dfg,ifeq4(of(skc10,skc11,u),true__dfg,ifeq4(entity(skc10,u),true__dfg,skc14,skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3955]),
    [iquote('0:Rew:1.0,3955.0')] ).

cnf(3967,plain,
    equal(ifeq4(of(skc10,skc11,u),true__dfg,ifeq4(of(skc10,skc11,u),true__dfg,ifeq4(entity(skc10,u),true__dfg,skc11,skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3956]),
    [iquote('0:Rew:1.0,3956.0')] ).

cnf(3974,plain,
    equal(ifeq4(of(skc10,skc11,skc15),true__dfg,ifeq4(of(skc10,skc11,skc15),true__dfg,skc11,skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3971]),
    [iquote('0:Rew:1.0,3971.0')] ).

cnf(1941,plain,
    equal(ifeq4(theme(skc10,u,v),true__dfg,ifeq4(theme(skc10,w,skc10),true__dfg,ifeq4(proposition(skc10,v),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,ifeq4(desire_want(skc10,w),true__dfg,v,skc10),skc10),skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,1931]),
    [iquote('0:Rew:1.0,1931.0')] ).

cnf(3966,plain,
    equal(ifeq4(of(skc10,u,skc15),true__dfg,ifeq4(of(skc10,skc11,skc15),true__dfg,ifeq4(forename(skc10,u),true__dfg,u,skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3957]),
    [iquote('0:Rew:1.0,3957.0')] ).

cnf(1744,plain,
    equal(ifeq4(of(skc10,u,v),true__dfg,ifeq4(of(skc10,skc11,v),true__dfg,ifeq4(entity(skc10,v),true__dfg,ifeq4(forename(skc10,u),true__dfg,u,skc11),skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,1719]),
    [iquote('0:Rew:1.0,1719.0')] ).

cnf(3126,plain,
    equal(ifeq4(of(skc8,skc14,skc12),true__dfg,ifeq4(of(skc8,u,skc12),true__dfg,ifeq4(forename(skc8,u),true__dfg,skc14,u),u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,3119]),
    [iquote('0:Rew:1.0,3119.0')] ).

cnf(3089,plain,
    equal(ifeq4(of(skc8,skc11,skc15),true__dfg,ifeq4(of(skc8,u,skc15),true__dfg,ifeq4(forename(skc8,u),true__dfg,skc11,u),u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,3080]),
    [iquote('0:Rew:1.0,3080.0')] ).

cnf(1825,plain,
    equal(ifeq(tuple(dance(skc8,skc9),true__dfg,desire_want(skc8,u),proposition(skc8,skc8),accessible_world(skc8,skc8),true__dfg,present(skc8,u),agent(skc8,skc9,skc15),agent(skc8,u,skc15),theme(skc8,u,skc8)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[89,1821]),
    [iquote('0:Rew:89.0,1821.0')] ).

cnf(3048,plain,
    equal(ifeq4(of(skc8,u,skc12),true__dfg,ifeq4(of(skc8,skc14,skc12),true__dfg,ifeq4(forename(skc8,u),true__dfg,u,skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,3041]),
    [iquote('0:Rew:1.0,3041.0')] ).

cnf(3008,plain,
    equal(ifeq4(of(skc8,u,skc15),true__dfg,ifeq4(of(skc8,skc11,skc15),true__dfg,ifeq4(forename(skc8,u),true__dfg,u,skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,2999]),
    [iquote('0:Rew:1.0,2999.0')] ).

cnf(3912,plain,
    equal(ifeq4(theme(skc10,skc9,u),true__dfg,ifeq4(proposition(skc10,u),true__dfg,skc10,u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,3907]),
    [iquote('0:Rew:1.0,3907.0')] ).

cnf(2450,plain,
    equal(ifeq4(theme(skc10,u,v),true__dfg,ifeq4(proposition(skc10,v),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,skc10,v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,2443,1928,1976]),
    [iquote('0:Rew:1.0,2443.0,1.0,2443.0,1928.0,2443.0,1.0,2443.0,1976.0,2443.0')] ).

cnf(3415,plain,
    equal(ifeq(tuple(dance(skc8,skc9),true__dfg,true__dfg,proposition(skc8,skc8),accessible_world(skc8,skc8),true__dfg,true__dfg,agent(skc8,skc9,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,skc8)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[89,3409]),
    [iquote('0:Rew:89.0,3409.0')] ).

cnf(3893,plain,
    equal(ifeq4(theme(skc10,skc9,u),true__dfg,ifeq4(proposition(skc10,u),true__dfg,u,skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,3888]),
    [iquote('0:Rew:1.0,3888.0')] ).

cnf(3892,plain,
    equal(ifeq4(theme(skc10,u,skc10),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,skc10,skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,3889]),
    [iquote('0:Rew:1.0,3889.0')] ).

cnf(2449,plain,
    equal(ifeq4(theme(skc10,u,v),true__dfg,ifeq4(proposition(skc10,v),true__dfg,ifeq4(desire_want(skc10,u),true__dfg,v,skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,2444,1928,1976]),
    [iquote('0:Rew:1.0,2444.0,1.0,2444.0,1928.0,2444.0,1.0,2444.0,1976.0,2444.0')] ).

cnf(3716,plain,
    equal(ifeq4(of(skc8,skc14,skc12),true__dfg,ifeq4(of(skc8,skc14,skc12),true__dfg,skc14,skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,3711]),
    [iquote('0:Rew:1.0,3711.0')] ).

cnf(3300,plain,
    equal(ifeq(tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,agent(skc10,skc13,skc15),agent(skc8,skc9,skc15),true__dfg),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[80,3299,82]),
    [iquote('0:Rew:80.0,3299.0,82.0,3299.0')] ).

cnf(3608,plain,
    equal(ifeq4(of(skc8,skc11,skc15),true__dfg,ifeq4(of(skc8,skc11,skc15),true__dfg,skc11,skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3601]),
    [iquote('0:Rew:1.0,3601.0')] ).

cnf(3882,plain,
    equal(ifeq4(of(skc10,skc11,skc15),true__dfg,skc14,skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3878]),
    [iquote('0:Rew:1.0,3878.0')] ).

cnf(2426,plain,
    equal(ifeq4(of(skc10,u,skc15),true__dfg,ifeq4(forename(skc10,u),true__dfg,skc14,u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,2419,656,747]),
    [iquote('0:Rew:1.0,2419.0,1.0,2419.0,656.0,2419.0,1.0,2419.0,747.0,2419.0')] ).

cnf(3863,plain,
    equal(ifeq4(of(skc10,skc14,skc12),true__dfg,skc11,skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,3859]),
    [iquote('0:Rew:1.0,3859.0')] ).

cnf(3233,plain,
    equal(ifeq4(theme(skc8,skc9,u),true__dfg,ifeq4(theme(skc8,skc9,v),true__dfg,ifeq4(proposition(skc8,u),true__dfg,ifeq4(proposition(skc8,v),true__dfg,u,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,3224]),
    [iquote('0:Rew:1.0,3224.0')] ).

cnf(2392,plain,
    equal(ifeq4(of(skc10,u,skc12),true__dfg,ifeq4(forename(skc10,u),true__dfg,skc11,u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,2385,1165,1398]),
    [iquote('0:Rew:1.0,2385.0,1.0,2385.0,1165.0,2385.0,1.0,2385.0,1398.0,2385.0')] ).

cnf(3855,plain,
    equal(ifeq4(of(skc10,skc11,skc15),true__dfg,skc11,skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,3851]),
    [iquote('0:Rew:1.0,3851.0')] ).

cnf(2425,plain,
    equal(ifeq4(of(skc10,u,skc15),true__dfg,ifeq4(forename(skc10,u),true__dfg,u,skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,2420,656,747]),
    [iquote('0:Rew:1.0,2420.0,1.0,2420.0,656.0,2420.0,1.0,2420.0,747.0,2420.0')] ).

cnf(3832,plain,
    equal(ifeq4(of(skc10,skc14,skc12),true__dfg,skc14,skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,3828]),
    [iquote('0:Rew:1.0,3828.0')] ).

cnf(3196,plain,
    equal(ifeq4(theme(skc8,u,skc10),true__dfg,ifeq4(theme(skc8,skc9,v),true__dfg,ifeq4(proposition(skc8,v),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,skc10,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,3187]),
    [iquote('0:Rew:1.0,3187.0')] ).

cnf(2391,plain,
    equal(ifeq4(of(skc10,u,skc12),true__dfg,ifeq4(forename(skc10,u),true__dfg,u,skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,2386,1165,1398]),
    [iquote('0:Rew:1.0,2386.0,1.0,2386.0,1165.0,2386.0,1.0,2386.0,1398.0,2386.0')] ).

cnf(2486,plain,
    equal(ifeq3(agent(u,skc9,skc12),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2483,67]),
    [iquote('0:SpR:2483.0,67.0')] ).

cnf(2441,plain,
    equal(ifeq3(theme(u,skc9,skc10),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2440,68]),
    [iquote('0:SpR:2440.0,68.0')] ).

cnf(2417,plain,
    equal(ifeq3(of(u,skc14,skc15),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2416,69]),
    [iquote('0:SpR:2416.0,69.0')] ).

cnf(3161,plain,
    equal(ifeq4(theme(skc8,skc9,u),true__dfg,ifeq4(theme(skc8,v,skc10),true__dfg,ifeq4(proposition(skc8,u),true__dfg,ifeq4(desire_want(skc8,v),true__dfg,u,skc10),skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,3154]),
    [iquote('0:Rew:1.0,3154.0')] ).

cnf(2383,plain,
    equal(ifeq3(of(u,skc11,skc12),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2382,69]),
    [iquote('0:SpR:2382.0,69.0')] ).

cnf(2070,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2057,40]),
    [iquote('0:SpR:2057.0,40.0')] ).

cnf(2062,plain,
    equal(ifeq3(present(u,skc9),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2040,44]),
    [iquote('0:SpR:2040.0,44.0')] ).

cnf(2055,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2018,39]),
    [iquote('0:SpR:2018.0,39.0')] ).

cnf(3160,plain,
    equal(ifeq4(theme(skc8,u,skc10),true__dfg,ifeq4(theme(skc8,v,skc10),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,ifeq4(desire_want(skc8,v),true__dfg,skc10,skc10),skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,3155]),
    [iquote('0:Rew:1.0,3155.0')] ).

cnf(2046,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(specific(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2017,41]),
    [iquote('0:SpR:2017.0,41.0')] ).

cnf(2033,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(nonexistent(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2016,42]),
    [iquote('0:SpR:2016.0,42.0')] ).

cnf(2026,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(unisex(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2015,43]),
    [iquote('0:SpR:2015.0,43.0')] ).

cnf(2013,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(eventuality(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2004,38]),
    [iquote('0:SpR:2004.0,38.0')] ).

cnf(3051,plain,
    equal(ifeq4(of(skc8,skc14,u),true__dfg,ifeq4(of(skc8,skc14,u),true__dfg,ifeq4(entity(skc8,u),true__dfg,skc14,skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,3038]),
    [iquote('0:Rew:1.0,3038.0')] ).

cnf(2001,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(event(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1984,37]),
    [iquote('0:SpR:1984.0,37.0')] ).

cnf(1982,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(desire_want(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1976,45]),
    [iquote('0:SpR:1976.0,45.0')] ).

cnf(1934,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(proposition(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1928,46]),
    [iquote('0:SpR:1928.0,46.0')] ).

cnf(1915,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(relation(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1908,47]),
    [iquote('0:SpR:1908.0,47.0')] ).

cnf(3050,plain,
    equal(ifeq4(of(skc8,skc11,u),true__dfg,ifeq4(of(skc8,skc14,u),true__dfg,ifeq4(entity(skc8,u),true__dfg,skc11,skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,3039]),
    [iquote('0:Rew:1.0,3039.0')] ).

cnf(1889,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1870,40]),
    [iquote('0:SpR:1870.0,40.0')] ).

cnf(1867,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1850,39]),
    [iquote('0:SpR:1850.0,39.0')] ).

cnf(1858,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(unisex(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1847,43]),
    [iquote('0:SpR:1847.0,43.0')] ).

cnf(1845,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(abstraction(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1836,48]),
    [iquote('0:SpR:1836.0,48.0')] ).

cnf(3010,plain,
    equal(ifeq4(of(skc8,skc14,u),true__dfg,ifeq4(of(skc8,skc11,u),true__dfg,ifeq4(entity(skc8,u),true__dfg,skc14,skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,2997]),
    [iquote('0:Rew:1.0,2997.0')] ).

cnf(1762,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(nonhuman(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1757,49]),
    [iquote('0:SpR:1757.0,49.0')] ).

cnf(1674,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(general(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1669,50]),
    [iquote('0:SpR:1669.0,50.0')] ).

cnf(1547,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(eventuality(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[439,38]),
    [iquote('0:SpR:439.0,38.0')] ).

cnf(1542,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1538,40]),
    [iquote('0:SpR:1538.0,40.0')] ).

cnf(3009,plain,
    equal(ifeq4(of(skc8,skc11,u),true__dfg,ifeq4(of(skc8,skc11,u),true__dfg,ifeq4(entity(skc8,u),true__dfg,skc11,skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,2998]),
    [iquote('0:Rew:1.0,2998.0')] ).

cnf(1535,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1471,39]),
    [iquote('0:SpR:1471.0,39.0')] ).

cnf(1526,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(nonhuman(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1470,49]),
    [iquote('0:SpR:1470.0,49.0')] ).

cnf(1519,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(general(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1469,50]),
    [iquote('0:SpR:1469.0,50.0')] ).

cnf(1493,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1177,39]),
    [iquote('0:SpR:1177.0,39.0')] ).

cnf(2971,plain,
    equal(ifeq4(theme(skc8,skc9,u),true__dfg,ifeq4(proposition(skc8,u),true__dfg,skc10,u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,2966]),
    [iquote('0:Rew:1.0,2966.0')] ).

cnf(1492,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[788,39]),
    [iquote('0:SpR:788.0,39.0')] ).

cnf(1491,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[683,39]),
    [iquote('0:SpR:683.0,39.0')] ).

cnf(1490,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(thing(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[449,39]),
    [iquote('0:SpR:449.0,39.0')] ).

cnf(1489,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(thing(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[460,39]),
    [iquote('0:SpR:460.0,39.0')] ).

cnf(2939,plain,
    equal(ifeq4(theme(skc8,skc9,u),true__dfg,ifeq4(proposition(skc8,u),true__dfg,u,skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,2934]),
    [iquote('0:Rew:1.0,2934.0')] ).

cnf(1488,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(thing(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[376,39]),
    [iquote('0:SpR:376.0,39.0')] ).

cnf(1487,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(thing(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[323,39]),
    [iquote('0:SpR:323.0,39.0')] ).

cnf(1486,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(thing(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[307,39]),
    [iquote('0:SpR:307.0,39.0')] ).

cnf(1485,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(thing(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[255,39]),
    [iquote('0:SpR:255.0,39.0')] ).

cnf(2938,plain,
    equal(ifeq4(theme(skc8,u,skc10),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,skc10,skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,2935]),
    [iquote('0:Rew:1.0,2935.0')] ).

cnf(1484,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(thing(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[194,39]),
    [iquote('0:SpR:194.0,39.0')] ).

cnf(1479,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(unisex(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1468,43]),
    [iquote('0:SpR:1468.0,43.0')] ).

cnf(1466,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(abstraction(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1458,48]),
    [iquote('0:SpR:1458.0,48.0')] ).

cnf(1455,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(relation(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1448,47]),
    [iquote('0:SpR:1448.0,47.0')] ).

cnf(1561,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(event(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[337,37]),
    [iquote('0:SpR:337.0,37.0')] ).

cnf(1446,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(relname(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1408,52]),
    [iquote('0:SpR:1408.0,52.0')] ).

cnf(1420,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1191,40]),
    [iquote('0:SpR:1191.0,40.0')] ).

cnf(1419,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[822,40]),
    [iquote('0:SpR:822.0,40.0')] ).

cnf(1418,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[700,40]),
    [iquote('0:SpR:700.0,40.0')] ).

cnf(1548,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(eventuality(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[438,38]),
    [iquote('0:SpR:438.0,38.0')] ).

cnf(1417,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(singleton(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[484,40]),
    [iquote('0:SpR:484.0,40.0')] ).

cnf(1416,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(singleton(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[507,40]),
    [iquote('0:SpR:507.0,40.0')] ).

cnf(1415,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(singleton(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[410,40]),
    [iquote('0:SpR:410.0,40.0')] ).

cnf(1414,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(singleton(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[409,40]),
    [iquote('0:SpR:409.0,40.0')] ).

cnf(1827,plain,
    equal(ifeq(tuple(dance(u,v),event(u,v),true__dfg,proposition(skc8,u),accessible_world(skc8,u),present(u,v),true__dfg,agent(u,v,skc15),agent(skc8,skc9,skc15),theme(skc8,skc9,u)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[89,1819]),
    [iquote('0:Rew:89.0,1819.0')] ).

cnf(1413,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(singleton(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[408,40]),
    [iquote('0:SpR:408.0,40.0')] ).

cnf(1412,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(singleton(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[407,40]),
    [iquote('0:SpR:407.0,40.0')] ).

cnf(1411,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(singleton(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[406,40]),
    [iquote('0:SpR:406.0,40.0')] ).

cnf(1405,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(forename(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1398,51]),
    [iquote('0:SpR:1398.0,51.0')] ).

cnf(1828,plain,
    equal(ifeq(tuple(dance(skc10,u),event(skc10,u),desire_want(skc8,v),true__dfg,true__dfg,present(skc10,u),present(skc8,v),agent(skc10,u,skc15),agent(skc8,v,skc15),theme(skc8,v,skc10)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[87,1818]),
    [iquote('0:Rew:87.0,1818.0')] ).

cnf(1396,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(mia_forename(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1392,53]),
    [iquote('0:SpR:1392.0,53.0')] ).

cnf(1371,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(specific(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1176,41]),
    [iquote('0:SpR:1176.0,41.0')] ).

cnf(1370,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(specific(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[682,41]),
    [iquote('0:SpR:682.0,41.0')] ).

cnf(1369,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(specific(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[448,41]),
    [iquote('0:SpR:448.0,41.0')] ).

cnf(1824,plain,
    equal(ifeq(tuple(true__dfg,true__dfg,desire_want(skc8,u),true__dfg,true__dfg,true__dfg,present(skc8,u),agent(skc10,skc13,skc15),agent(skc8,u,skc15),theme(skc8,u,skc10)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[80,1822,86,87,82]),
    [iquote('0:Rew:80.0,1822.0,86.0,1822.0,87.0,1822.0,82.0,1822.0')] ).

cnf(1368,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(specific(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[459,41]),
    [iquote('0:SpR:459.0,41.0')] ).

cnf(1367,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(specific(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[254,41]),
    [iquote('0:SpR:254.0,41.0')] ).

cnf(1366,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(specific(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[193,41]),
    [iquote('0:SpR:193.0,41.0')] ).

cnf(1352,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(woman(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1346,54]),
    [iquote('0:SpR:1346.0,54.0')] ).

cnf(1823,plain,
    equal(ifeq(tuple(dance(skc10,u),event(skc10,u),true__dfg,true__dfg,true__dfg,present(skc10,u),true__dfg,agent(skc10,u,skc15),agent(skc8,skc9,skc15),true__dfg),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    inference(rew,[status(thm),theory(equality)],[88,1813,86,87,89]),
    [iquote('0:Rew:88.0,1813.0,86.0,1813.0,87.0,1813.0,89.0,1813.0')] ).

cnf(1325,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(nonexistent(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[458,42]),
    [iquote('0:SpR:458.0,42.0')] ).

cnf(1324,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(nonexistent(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[447,42]),
    [iquote('0:SpR:447.0,42.0')] ).

cnf(1312,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(human_person(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1303,55]),
    [iquote('0:SpR:1303.0,55.0')] ).

cnf(1285,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(unisex(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[785,43]),
    [iquote('0:SpR:785.0,43.0')] ).

cnf(1781,plain,
    equal(ifeq4(theme(skc8,u,v),true__dfg,ifeq4(theme(skc8,skc9,w),true__dfg,ifeq4(proposition(skc8,v),true__dfg,ifeq4(proposition(skc8,w),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,v,w),w),w),w),w),w),
    inference(rew,[status(thm),theory(equality)],[1,1770]),
    [iquote('0:Rew:1.0,1770.0')] ).

cnf(1284,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(unisex(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[446,43]),
    [iquote('0:SpR:446.0,43.0')] ).

cnf(1283,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(unisex(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[457,43]),
    [iquote('0:SpR:457.0,43.0')] ).

cnf(1282,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(unisex(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[373,43]),
    [iquote('0:SpR:373.0,43.0')] ).

cnf(1281,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(unisex(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[320,43]),
    [iquote('0:SpR:320.0,43.0')] ).

cnf(1780,plain,
    equal(ifeq4(theme(skc8,skc9,u),true__dfg,ifeq4(theme(skc8,v,w),true__dfg,ifeq4(proposition(skc8,u),true__dfg,ifeq4(proposition(skc8,w),true__dfg,ifeq4(desire_want(skc8,v),true__dfg,u,w),w),w),w),w),w),
    inference(rew,[status(thm),theory(equality)],[1,1771]),
    [iquote('0:Rew:1.0,1771.0')] ).

cnf(1280,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(unisex(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[304,43]),
    [iquote('0:SpR:304.0,43.0')] ).

cnf(1240,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(organism(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1232,56]),
    [iquote('0:SpR:1232.0,56.0')] ).

cnf(1173,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(entity(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1165,57]),
    [iquote('0:SpR:1165.0,57.0')] ).

cnf(1151,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(relation(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[771,47]),
    [iquote('0:SpR:771.0,47.0')] ).

cnf(1778,plain,
    equal(ifeq4(theme(skc8,u,skc10),true__dfg,ifeq4(theme(skc8,v,w),true__dfg,ifeq4(proposition(skc8,w),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,ifeq4(desire_want(skc8,v),true__dfg,skc10,w),w),w),w),w),w),
    inference(rew,[status(thm),theory(equality)],[1,1773]),
    [iquote('0:Rew:1.0,1773.0')] ).

cnf(1150,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(relation(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[313,47]),
    [iquote('0:SpR:313.0,47.0')] ).

cnf(1149,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(relation(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[265,47]),
    [iquote('0:SpR:265.0,47.0')] ).

cnf(1148,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(relation(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[260,47]),
    [iquote('0:SpR:260.0,47.0')] ).

cnf(1115,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(abstraction(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[778,48]),
    [iquote('0:SpR:778.0,48.0')] ).

cnf(1779,plain,
    equal(ifeq4(theme(skc8,u,v),true__dfg,ifeq4(theme(skc8,w,skc10),true__dfg,ifeq4(proposition(skc8,v),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,ifeq4(desire_want(skc8,w),true__dfg,v,skc10),skc10),skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,1772]),
    [iquote('0:Rew:1.0,1772.0')] ).

cnf(1114,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(abstraction(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[346,48]),
    [iquote('0:SpR:346.0,48.0')] ).

cnf(1113,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(abstraction(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[297,48]),
    [iquote('0:SpR:297.0,48.0')] ).

cnf(1112,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(abstraction(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[296,48]),
    [iquote('0:SpR:296.0,48.0')] ).

cnf(1107,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(existent(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1102,58]),
    [iquote('0:SpR:1102.0,58.0')] ).

cnf(1743,plain,
    equal(ifeq4(of(skc8,skc14,u),true__dfg,ifeq4(of(skc8,v,u),true__dfg,ifeq4(entity(skc8,u),true__dfg,ifeq4(forename(skc8,v),true__dfg,skc14,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1720]),
    [iquote('0:Rew:1.0,1720.0')] ).

cnf(1071,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(nonhuman(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[787,49]),
    [iquote('0:SpR:787.0,49.0')] ).

cnf(1070,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(nonhuman(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[375,49]),
    [iquote('0:SpR:375.0,49.0')] ).

cnf(1069,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(nonhuman(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[322,49]),
    [iquote('0:SpR:322.0,49.0')] ).

cnf(1068,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(nonhuman(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[306,49]),
    [iquote('0:SpR:306.0,49.0')] ).

cnf(1742,plain,
    equal(ifeq4(of(skc8,skc11,u),true__dfg,ifeq4(of(skc8,v,u),true__dfg,ifeq4(entity(skc8,u),true__dfg,ifeq4(forename(skc8,v),true__dfg,skc11,v),v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1721]),
    [iquote('0:Rew:1.0,1721.0')] ).

cnf(1059,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(impartial(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1056,59]),
    [iquote('0:SpR:1056.0,59.0')] ).

cnf(1036,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(general(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[786,50]),
    [iquote('0:SpR:786.0,50.0')] ).

cnf(1035,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(general(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[374,50]),
    [iquote('0:SpR:374.0,50.0')] ).

cnf(1034,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(general(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[321,50]),
    [iquote('0:SpR:321.0,50.0')] ).

cnf(1747,plain,
    equal(ifeq4(of(skc8,u,v),true__dfg,ifeq4(of(skc8,skc14,v),true__dfg,ifeq4(entity(skc8,v),true__dfg,ifeq4(forename(skc8,u),true__dfg,u,skc14),skc14),skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,1716]),
    [iquote('0:Rew:1.0,1716.0')] ).

cnf(1033,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(general(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[305,50]),
    [iquote('0:SpR:305.0,50.0')] ).

cnf(1005,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(forename(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[747,51]),
    [iquote('0:SpR:747.0,51.0')] ).

cnf(997,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(living(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[994,60]),
    [iquote('0:SpR:994.0,60.0')] ).

cnf(965,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(relname(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[755,52]),
    [iquote('0:SpR:755.0,52.0')] ).

cnf(1746,plain,
    equal(ifeq4(of(skc8,u,v),true__dfg,ifeq4(of(skc8,skc11,v),true__dfg,ifeq4(entity(skc8,v),true__dfg,ifeq4(forename(skc8,u),true__dfg,u,skc11),skc11),skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,1717]),
    [iquote('0:Rew:1.0,1717.0')] ).

cnf(964,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(relname(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[247,52]),
    [iquote('0:SpR:247.0,52.0')] ).

cnf(963,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(relname(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[246,52]),
    [iquote('0:SpR:246.0,52.0')] ).

cnf(954,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(human(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[950,61]),
    [iquote('0:SpR:950.0,61.0')] ).

cnf(915,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(animate(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[906,62]),
    [iquote('0:SpR:906.0,62.0')] ).

cnf(1776,plain,
    equal(ifeq4(theme(skc8,u,v),true__dfg,ifeq4(proposition(skc8,v),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,skc10,v),v),v),v),
    inference(rew,[status(thm),theory(equality)],[1,1775,86,88]),
    [iquote('0:Rew:1.0,1775.0,1.0,1775.0,86.0,1775.0,1.0,1775.0,88.0,1775.0')] ).

cnf(880,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(human_person(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[623,55]),
    [iquote('0:SpR:623.0,55.0')] ).

cnf(879,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(human_person(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[180,55]),
    [iquote('0:SpR:180.0,55.0')] ).

cnf(878,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(human_person(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[130,55]),
    [iquote('0:SpR:130.0,55.0')] ).

cnf(872,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(female(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[867,63]),
    [iquote('0:SpR:867.0,63.0')] ).

cnf(1777,plain,
    equal(ifeq4(theme(skc8,u,v),true__dfg,ifeq4(proposition(skc8,v),true__dfg,ifeq4(desire_want(skc8,u),true__dfg,v,skc10),skc10),skc10),skc10),
    inference(rew,[status(thm),theory(equality)],[1,1774,86,88]),
    [iquote('0:Rew:1.0,1774.0,1.0,1774.0,86.0,1774.0,1.0,1774.0,88.0,1774.0')] ).

cnf(845,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(organism(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[635,56]),
    [iquote('0:SpR:635.0,56.0')] ).

cnf(844,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(organism(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[204,56]),
    [iquote('0:SpR:204.0,56.0')] ).

cnf(843,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(organism(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[167,56]),
    [iquote('0:SpR:167.0,56.0')] ).

cnf(2913,plain,
    equal(ifeq4(of(skc8,skc14,skc12),true__dfg,skc11,skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,2909]),
    [iquote('0:Rew:1.0,2909.0')] ).

cnf(1733,plain,
    equal(ifeq4(of(skc8,u,skc12),true__dfg,ifeq4(forename(skc8,u),true__dfg,skc11,u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,1730,235,84]),
    [iquote('0:Rew:1.0,1730.0,1.0,1730.0,235.0,1730.0,1.0,1730.0,84.0,1730.0')] ).

cnf(829,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(entity(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[656,57]),
    [iquote('0:SpR:656.0,57.0')] ).

cnf(828,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(entity(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[235,57]),
    [iquote('0:SpR:235.0,57.0')] ).

cnf(827,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(entity(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[175,57]),
    [iquote('0:SpR:175.0,57.0')] ).

cnf(2888,plain,
    equal(ifeq4(of(skc8,skc11,skc15),true__dfg,skc14,skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,2884]),
    [iquote('0:Rew:1.0,2884.0')] ).

cnf(1732,plain,
    equal(ifeq4(of(skc8,u,skc15),true__dfg,ifeq4(forename(skc8,u),true__dfg,skc14,u),u),u),
    inference(rew,[status(thm),theory(equality)],[1,1731,175,90]),
    [iquote('0:Rew:1.0,1731.0,1.0,1731.0,175.0,1731.0,1.0,1731.0,90.0,1731.0')] ).

cnf(799,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(existent(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[681,58]),
    [iquote('0:SpR:681.0,58.0')] ).

cnf(798,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(existent(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[253,58]),
    [iquote('0:SpR:253.0,58.0')] ).

cnf(797,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(existent(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[192,58]),
    [iquote('0:SpR:192.0,58.0')] ).

cnf(2861,plain,
    equal(ifeq4(of(skc8,skc14,skc12),true__dfg,skc14,skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,2857]),
    [iquote('0:Rew:1.0,2857.0')] ).

cnf(1735,plain,
    equal(ifeq4(of(skc8,u,skc12),true__dfg,ifeq4(forename(skc8,u),true__dfg,u,skc11),skc11),skc11),
    inference(rew,[status(thm),theory(equality)],[1,1728,235,84]),
    [iquote('0:Rew:1.0,1728.0,1.0,1728.0,235.0,1728.0,1.0,1728.0,84.0,1728.0')] ).

cnf(759,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(impartial(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[655,59]),
    [iquote('0:SpR:655.0,59.0')] ).

cnf(758,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(impartial(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[234,59]),
    [iquote('0:SpR:234.0,59.0')] ).

cnf(757,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(impartial(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[174,59]),
    [iquote('0:SpR:174.0,59.0')] ).

cnf(2837,plain,
    equal(ifeq4(of(skc8,skc11,skc15),true__dfg,skc11,skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,2833]),
    [iquote('0:Rew:1.0,2833.0')] ).

cnf(1734,plain,
    equal(ifeq4(of(skc8,u,skc15),true__dfg,ifeq4(forename(skc8,u),true__dfg,u,skc14),skc14),skc14),
    inference(rew,[status(thm),theory(equality)],[1,1729,175,90]),
    [iquote('0:Rew:1.0,1729.0,1.0,1729.0,175.0,1729.0,1.0,1729.0,90.0,1729.0')] ).

cnf(744,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(vincent_forename(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[741,64]),
    [iquote('0:SpR:741.0,64.0')] ).

cnf(722,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(living(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[654,60]),
    [iquote('0:SpR:654.0,60.0')] ).

cnf(721,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(living(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[233,60]),
    [iquote('0:SpR:233.0,60.0')] ).

cnf(720,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(living(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[173,60]),
    [iquote('0:SpR:173.0,60.0')] ).

cnf(1681,plain,
    equal(ifeq3(agent(u,skc9,skc12),true__dfg,ifeq3(accessible_world(u,skc8),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[94,67]),
    [iquote('0:SpR:94.0,67.0')] ).

cnf(704,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(human(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[634,61]),
    [iquote('0:SpR:634.0,61.0')] ).

cnf(703,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(human(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[203,61]),
    [iquote('0:SpR:203.0,61.0')] ).

cnf(702,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(human(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[155,61]),
    [iquote('0:SpR:155.0,61.0')] ).

cnf(667,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(animate(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[633,62]),
    [iquote('0:SpR:633.0,62.0')] ).

cnf(1680,plain,
    equal(ifeq3(agent(u,skc13,skc12),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[95,67]),
    [iquote('0:SpR:95.0,67.0')] ).

cnf(666,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(animate(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[202,62]),
    [iquote('0:SpR:202.0,62.0')] ).

cnf(665,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(animate(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[149,62]),
    [iquote('0:SpR:149.0,62.0')] ).

cnf(640,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(female(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[142,63]),
    [iquote('0:SpR:142.0,63.0')] ).

cnf(620,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(man(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[614,65]),
    [iquote('0:SpR:614.0,65.0')] ).

cnf(1655,plain,
    equal(ifeq3(theme(u,skc9,skc10),true__dfg,ifeq3(accessible_world(u,skc8),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[96,68]),
    [iquote('0:SpR:96.0,68.0')] ).

cnf(580,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(male(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[575,66]),
    [iquote('0:SpR:575.0,66.0')] ).

cnf(567,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(male(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[124,66]),
    [iquote('0:SpR:124.0,66.0')] ).

cnf(2044,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc10,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[2017,74]),
    [iquote('0:SpR:2017.0,74.0')] ).

cnf(2031,plain,
    equal(ifeq2(tuple2(true__dfg,existent(skc10,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[2016,77]),
    [iquote('0:SpR:2016.0,77.0')] ).

cnf(1621,plain,
    equal(ifeq3(of(u,skc14,skc15),true__dfg,ifeq3(accessible_world(u,skc8),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[92,69]),
    [iquote('0:SpR:92.0,69.0')] ).

cnf(2024,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc10,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[2015,72]),
    [iquote('0:SpR:2015.0,72.0')] ).

cnf(2023,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc10,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[2015,73]),
    [iquote('0:SpR:2015.0,73.0')] ).

cnf(1856,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc10,skc10)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1847,72]),
    [iquote('0:SpR:1847.0,72.0')] ).

cnf(1855,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc10,skc10)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1847,73]),
    [iquote('0:SpR:1847.0,73.0')] ).

cnf(1620,plain,
    equal(ifeq3(of(u,skc11,skc12),true__dfg,ifeq3(accessible_world(u,skc8),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[93,69]),
    [iquote('0:SpR:93.0,69.0')] ).

cnf(1759,plain,
    equal(ifeq2(tuple2(true__dfg,human(skc10,skc10)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1757,75]),
    [iquote('0:SpR:1757.0,75.0')] ).

cnf(1671,plain,
    equal(ifeq2(tuple2(specific(skc10,skc10),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1669,74]),
    [iquote('0:SpR:1669.0,74.0')] ).

cnf(1524,plain,
    equal(ifeq2(tuple2(true__dfg,human(skc10,skc11)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1470,75]),
    [iquote('0:SpR:1470.0,75.0')] ).

cnf(1517,plain,
    equal(ifeq2(tuple2(specific(skc10,skc11),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1469,74]),
    [iquote('0:SpR:1469.0,74.0')] ).

cnf(1591,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(dance(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[83,36]),
    [iquote('0:SpR:83.0,36.0')] ).

cnf(1477,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc10,skc11)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1468,72]),
    [iquote('0:SpR:1468.0,72.0')] ).

cnf(1476,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc10,skc11)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1468,73]),
    [iquote('0:SpR:1468.0,73.0')] ).

cnf(1182,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc10,skc12)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1176,74]),
    [iquote('0:SpR:1176.0,74.0')] ).

cnf(1104,plain,
    equal(ifeq2(tuple2(nonexistent(skc10,skc12),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[1102,77]),
    [iquote('0:SpR:1102.0,77.0')] ).

cnf(1560,plain,
    equal(ifeq3(accessible_world(u,skc10),true__dfg,ifeq3(event(u,skc13),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[80,37]),
    [iquote('0:SpR:80.0,37.0')] ).

cnf(952,plain,
    equal(ifeq2(tuple2(nonhuman(skc10,skc12),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[950,75]),
    [iquote('0:SpR:950.0,75.0')] ).

cnf(870,plain,
    equal(ifeq2(tuple2(unisex(skc10,skc12),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[867,73]),
    [iquote('0:SpR:867.0,73.0')] ).

cnf(869,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc10,skc12)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[867,76]),
    [iquote('0:SpR:867.0,76.0')] ).

cnf(813,plain,
    equal(ifeq2(tuple2(true__dfg,human(skc10,skc14)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[787,75]),
    [iquote('0:SpR:787.0,75.0')] ).

cnf(1249,plain,
    equal(ifeq3(present(u,skc13),true__dfg,ifeq3(accessible_world(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[82,44]),
    [iquote('0:SpR:82.0,44.0')] ).

cnf(809,plain,
    equal(ifeq2(tuple2(specific(skc10,skc14),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[786,74]),
    [iquote('0:SpR:786.0,74.0')] ).

cnf(793,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc10,skc14)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[785,72]),
    [iquote('0:SpR:785.0,72.0')] ).

cnf(792,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc10,skc14)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[785,73]),
    [iquote('0:SpR:785.0,73.0')] ).

cnf(691,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc10,skc15)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[682,74]),
    [iquote('0:SpR:682.0,74.0')] ).

cnf(1248,plain,
    equal(ifeq3(present(u,skc9),true__dfg,ifeq3(accessible_world(u,skc8),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[89,44]),
    [iquote('0:SpR:89.0,44.0')] ).

cnf(686,plain,
    equal(ifeq2(tuple2(nonexistent(skc10,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[681,77]),
    [iquote('0:SpR:681.0,77.0')] ).

cnf(646,plain,
    equal(ifeq2(tuple2(nonhuman(skc10,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[634,75]),
    [iquote('0:SpR:634.0,75.0')] ).

cnf(578,plain,
    equal(ifeq2(tuple2(unisex(skc10,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[575,72]),
    [iquote('0:SpR:575.0,72.0')] ).

cnf(577,plain,
    equal(ifeq2(tuple2(female(skc10,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[575,76]),
    [iquote('0:SpR:575.0,76.0')] ).

cnf(1207,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(desire_want(u,skc9),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[88,45]),
    [iquote('0:SpR:88.0,45.0')] ).

cnf(561,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc10,skc13)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[446,72]),
    [iquote('0:SpR:446.0,72.0')] ).

cnf(560,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc8,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[457,72]),
    [iquote('0:SpR:457.0,72.0')] ).

cnf(559,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc8,skc10)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[373,72]),
    [iquote('0:SpR:373.0,72.0')] ).

cnf(558,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc8,skc11)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[320,72]),
    [iquote('0:SpR:320.0,72.0')] ).

cnf(1193,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(proposition(u,skc10),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[86,46]),
    [iquote('0:SpR:86.0,46.0')] ).

cnf(557,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc8,skc14)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[304,72]),
    [iquote('0:SpR:304.0,72.0')] ).

cnf(556,plain,
    equal(ifeq2(tuple2(unisex(skc8,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[124,72]),
    [iquote('0:SpR:124.0,72.0')] ).

cnf(550,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc10,skc13)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[446,73]),
    [iquote('0:SpR:446.0,73.0')] ).

cnf(549,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc8,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[457,73]),
    [iquote('0:SpR:457.0,73.0')] ).

cnf(1004,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(forename(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[84,51]),
    [iquote('0:SpR:84.0,51.0')] ).

cnf(548,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc8,skc10)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[373,73]),
    [iquote('0:SpR:373.0,73.0')] ).

cnf(547,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc8,skc11)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[320,73]),
    [iquote('0:SpR:320.0,73.0')] ).

cnf(546,plain,
    equal(ifeq2(tuple2(true__dfg,female(skc8,skc14)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[304,73]),
    [iquote('0:SpR:304.0,73.0')] ).

cnf(545,plain,
    equal(ifeq2(tuple2(unisex(skc8,skc12),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[142,73]),
    [iquote('0:SpR:142.0,73.0')] ).

cnf(1003,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(forename(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[90,51]),
    [iquote('0:SpR:90.0,51.0')] ).

cnf(539,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc10,skc13)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[448,74]),
    [iquote('0:SpR:448.0,74.0')] ).

cnf(538,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc8,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[459,74]),
    [iquote('0:SpR:459.0,74.0')] ).

cnf(537,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc8,skc12)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[254,74]),
    [iquote('0:SpR:254.0,74.0')] ).

cnf(536,plain,
    equal(ifeq2(tuple2(true__dfg,general(skc8,skc15)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[193,74]),
    [iquote('0:SpR:193.0,74.0')] ).

cnf(936,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(mia_forename(u,skc11),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[85,53]),
    [iquote('0:SpR:85.0,53.0')] ).

cnf(535,plain,
    equal(ifeq2(tuple2(specific(skc8,skc10),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[374,74]),
    [iquote('0:SpR:374.0,74.0')] ).

cnf(534,plain,
    equal(ifeq2(tuple2(specific(skc8,skc11),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[321,74]),
    [iquote('0:SpR:321.0,74.0')] ).

cnf(533,plain,
    equal(ifeq2(tuple2(specific(skc8,skc14),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[305,74]),
    [iquote('0:SpR:305.0,74.0')] ).

cnf(527,plain,
    equal(ifeq2(tuple2(true__dfg,human(skc8,skc10)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[375,75]),
    [iquote('0:SpR:375.0,75.0')] ).

cnf(908,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(woman(u,skc12),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[81,54]),
    [iquote('0:SpR:81.0,54.0')] ).

cnf(2489,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,agent(u,skc9,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2487]),
    [iquote('0:Rew:2.0,2487.0')] ).

cnf(2448,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,theme(u,skc9,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2442]),
    [iquote('0:Rew:2.0,2442.0')] ).

cnf(2424,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,of(u,skc14,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2418]),
    [iquote('0:Rew:2.0,2418.0')] ).

cnf(2390,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,of(u,skc11,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2384]),
    [iquote('0:Rew:2.0,2384.0')] ).

cnf(606,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(vincent_forename(u,skc14),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[91,64]),
    [iquote('0:SpR:91.0,64.0')] ).

cnf(2073,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2071]),
    [iquote('0:Rew:2.0,2071.0')] ).

cnf(2066,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,present(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2063]),
    [iquote('0:Rew:2.0,2063.0')] ).

cnf(2059,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2056]),
    [iquote('0:Rew:2.0,2056.0')] ).

cnf(2049,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,specific(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2047]),
    [iquote('0:Rew:2.0,2047.0')] ).

cnf(588,plain,
    equal(ifeq3(accessible_world(u,skc8),true__dfg,ifeq3(man(u,skc15),true__dfg,true__dfg,true__dfg),true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[79,65]),
    [iquote('0:SpR:79.0,65.0')] ).

cnf(2036,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,nonexistent(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2034]),
    [iquote('0:Rew:2.0,2034.0')] ).

cnf(2029,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,unisex(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2027]),
    [iquote('0:Rew:2.0,2027.0')] ).

cnf(2020,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,eventuality(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2014]),
    [iquote('0:Rew:2.0,2014.0')] ).

cnf(2541,plain,
    equal(ifeq3(agent(skc8,skc13,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[95,1687]),
    [iquote('0:SpR:95.0,1687.0')] ).

cnf(1687,plain,
    equal(ifeq3(agent(skc8,u,v),true__dfg,agent(skc10,u,v),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1682]),
    [iquote('0:Rew:2.0,1682.0')] ).

cnf(2005,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,event(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2002]),
    [iquote('0:Rew:2.0,2002.0')] ).

cnf(1986,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,desire_want(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1983]),
    [iquote('0:Rew:2.0,1983.0')] ).

cnf(1939,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,proposition(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1935]),
    [iquote('0:Rew:2.0,1935.0')] ).

cnf(1919,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,relation(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1916]),
    [iquote('0:Rew:2.0,1916.0')] ).

cnf(1659,plain,
    equal(ifeq3(theme(skc8,u,v),true__dfg,theme(skc10,u,v),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1656]),
    [iquote('0:Rew:2.0,1656.0')] ).

cnf(1892,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1890]),
    [iquote('0:Rew:2.0,1890.0')] ).

cnf(1871,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1868]),
    [iquote('0:Rew:2.0,1868.0')] ).

cnf(1861,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,unisex(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1859]),
    [iquote('0:Rew:2.0,1859.0')] ).

cnf(1852,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,abstraction(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1846]),
    [iquote('0:Rew:2.0,1846.0')] ).

cnf(1627,plain,
    equal(ifeq3(of(skc8,u,v),true__dfg,of(skc10,u,v),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1622]),
    [iquote('0:Rew:2.0,1622.0')] ).

cnf(1765,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,nonhuman(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1763]),
    [iquote('0:Rew:2.0,1763.0')] ).

cnf(1677,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,general(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1675]),
    [iquote('0:Rew:2.0,1675.0')] ).

cnf(1566,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,event(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1563]),
    [iquote('0:Rew:2.0,1563.0')] ).

cnf(2483,plain,
    equal(agent(skc10,skc9,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2481]),
    [iquote('0:Rew:2.0,2481.0')] ).

cnf(1686,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,agent(u,skc9,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1684]),
    [iquote('0:Rew:2.0,1684.0')] ).

cnf(1553,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,eventuality(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1550]),
    [iquote('0:Rew:2.0,1550.0')] ).

cnf(1552,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,eventuality(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1549]),
    [iquote('0:Rew:2.0,1549.0')] ).

cnf(1545,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1543]),
    [iquote('0:Rew:2.0,1543.0')] ).

cnf(1539,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1536]),
    [iquote('0:Rew:2.0,1536.0')] ).

cnf(1685,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,agent(u,skc13,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1683]),
    [iquote('0:Rew:2.0,1683.0')] ).

cnf(1529,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,nonhuman(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1527]),
    [iquote('0:Rew:2.0,1527.0')] ).

cnf(1522,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,general(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1520]),
    [iquote('0:Rew:2.0,1520.0')] ).

cnf(1514,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1503]),
    [iquote('0:Rew:2.0,1503.0')] ).

cnf(2440,plain,
    equal(theme(skc10,skc9,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2438]),
    [iquote('0:Rew:2.0,2438.0')] ).

cnf(1658,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,theme(u,skc9,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1657]),
    [iquote('0:Rew:2.0,1657.0')] ).

cnf(1513,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1502]),
    [iquote('0:Rew:2.0,1502.0')] ).

cnf(1512,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1501]),
    [iquote('0:Rew:2.0,1501.0')] ).

cnf(1511,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,thing(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1500]),
    [iquote('0:Rew:2.0,1500.0')] ).

cnf(2416,plain,
    equal(of(skc10,skc14,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2414]),
    [iquote('0:Rew:2.0,2414.0')] ).

cnf(1626,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,of(u,skc14,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1624]),
    [iquote('0:Rew:2.0,1624.0')] ).

cnf(1510,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,thing(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1499]),
    [iquote('0:Rew:2.0,1499.0')] ).

cnf(1509,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,thing(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1498]),
    [iquote('0:Rew:2.0,1498.0')] ).

cnf(1508,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,thing(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1497]),
    [iquote('0:Rew:2.0,1497.0')] ).

cnf(2382,plain,
    equal(of(skc10,skc11,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2380]),
    [iquote('0:Rew:2.0,2380.0')] ).

cnf(1625,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,of(u,skc11,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1623]),
    [iquote('0:Rew:2.0,1623.0')] ).

cnf(1507,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,thing(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1496]),
    [iquote('0:Rew:2.0,1496.0')] ).

cnf(1506,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,thing(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1495]),
    [iquote('0:Rew:2.0,1495.0')] ).

cnf(1505,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,thing(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1494]),
    [iquote('0:Rew:2.0,1494.0')] ).

cnf(2356,plain,
    equal(ifeq3(dance(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[83,1595]),
    [iquote('0:SpR:83.0,1595.0')] ).

cnf(1595,plain,
    equal(ifeq3(dance(skc8,u),true__dfg,dance(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1593]),
    [iquote('0:Rew:2.0,1593.0')] ).

cnf(1482,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,unisex(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1480]),
    [iquote('0:Rew:2.0,1480.0')] ).

cnf(1473,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,abstraction(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1467]),
    [iquote('0:Rew:2.0,1467.0')] ).

cnf(1459,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,relation(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1456]),
    [iquote('0:Rew:2.0,1456.0')] ).

cnf(1450,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,relname(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1447]),
    [iquote('0:Rew:2.0,1447.0')] ).

cnf(1594,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,dance(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1592]),
    [iquote('0:Rew:2.0,1592.0')] ).

cnf(1441,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1430]),
    [iquote('0:Rew:2.0,1430.0')] ).

cnf(1440,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1429]),
    [iquote('0:Rew:2.0,1429.0')] ).

cnf(1439,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1428]),
    [iquote('0:Rew:2.0,1428.0')] ).

cnf(2324,plain,
    equal(ifeq3(event(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[80,1567]),
    [iquote('0:SpR:80.0,1567.0')] ).

cnf(1567,plain,
    equal(ifeq3(event(skc8,u),true__dfg,event(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1564]),
    [iquote('0:Rew:2.0,1564.0')] ).

cnf(1438,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,singleton(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1427]),
    [iquote('0:Rew:2.0,1427.0')] ).

cnf(1437,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,singleton(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1426]),
    [iquote('0:Rew:2.0,1426.0')] ).

cnf(1436,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,singleton(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1425]),
    [iquote('0:Rew:2.0,1425.0')] ).

cnf(1435,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,singleton(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1424]),
    [iquote('0:Rew:2.0,1424.0')] ).

cnf(1565,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,event(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1562]),
    [iquote('0:Rew:2.0,1562.0')] ).

cnf(1434,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,singleton(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1423]),
    [iquote('0:Rew:2.0,1423.0')] ).

cnf(1433,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,singleton(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1422]),
    [iquote('0:Rew:2.0,1422.0')] ).

cnf(1432,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,singleton(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1421]),
    [iquote('0:Rew:2.0,1421.0')] ).

cnf(2275,plain,
    equal(ifeq3(eventuality(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[438,1554]),
    [iquote('0:SpR:438.0,1554.0')] ).

cnf(1554,plain,
    equal(ifeq3(eventuality(skc8,u),true__dfg,eventuality(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1551]),
    [iquote('0:Rew:2.0,1551.0')] ).

cnf(1409,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,forename(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1406]),
    [iquote('0:Rew:2.0,1406.0')] ).

cnf(1400,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,mia_forename(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1397]),
    [iquote('0:Rew:2.0,1397.0')] ).

cnf(1384,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,specific(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1377]),
    [iquote('0:Rew:2.0,1377.0')] ).

cnf(2237,plain,
    equal(ifeq3(thing(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[449,1515]),
    [iquote('0:SpR:449.0,1515.0')] ).

cnf(1515,plain,
    equal(ifeq3(thing(skc8,u),true__dfg,thing(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1504]),
    [iquote('0:Rew:2.0,1504.0')] ).

cnf(1383,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,specific(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1376]),
    [iquote('0:Rew:2.0,1376.0')] ).

cnf(1382,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,specific(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1375]),
    [iquote('0:Rew:2.0,1375.0')] ).

cnf(1381,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,specific(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1374]),
    [iquote('0:Rew:2.0,1374.0')] ).

cnf(2197,plain,
    equal(ifeq3(singleton(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[484,1442]),
    [iquote('0:SpR:484.0,1442.0')] ).

cnf(1442,plain,
    equal(ifeq3(singleton(skc8,u),true__dfg,singleton(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1431]),
    [iquote('0:Rew:2.0,1431.0')] ).

cnf(1380,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,specific(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1373]),
    [iquote('0:Rew:2.0,1373.0')] ).

cnf(1379,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,specific(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1372]),
    [iquote('0:Rew:2.0,1372.0')] ).

cnf(1357,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,woman(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1353]),
    [iquote('0:Rew:2.0,1353.0')] ).

cnf(2165,plain,
    equal(ifeq3(specific(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[448,1385]),
    [iquote('0:SpR:448.0,1385.0')] ).

cnf(1385,plain,
    equal(ifeq3(specific(skc8,u),true__dfg,specific(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1378]),
    [iquote('0:Rew:2.0,1378.0')] ).

cnf(1330,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,nonexistent(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1327]),
    [iquote('0:Rew:2.0,1327.0')] ).

cnf(1329,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,nonexistent(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1326]),
    [iquote('0:Rew:2.0,1326.0')] ).

cnf(1318,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,human_person(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1313]),
    [iquote('0:Rew:2.0,1313.0')] ).

cnf(2145,plain,
    equal(ifeq3(nonexistent(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[447,1331]),
    [iquote('0:SpR:447.0,1331.0')] ).

cnf(1331,plain,
    equal(ifeq3(nonexistent(skc8,u),true__dfg,nonexistent(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1328]),
    [iquote('0:Rew:2.0,1328.0')] ).

cnf(1298,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,unisex(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1291]),
    [iquote('0:Rew:2.0,1291.0')] ).

cnf(1297,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,unisex(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1290]),
    [iquote('0:Rew:2.0,1290.0')] ).

cnf(1296,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,unisex(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1289]),
    [iquote('0:Rew:2.0,1289.0')] ).

cnf(2113,plain,
    equal(ifeq3(unisex(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[446,1299]),
    [iquote('0:SpR:446.0,1299.0')] ).

cnf(1299,plain,
    equal(ifeq3(unisex(skc8,u),true__dfg,unisex(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1292]),
    [iquote('0:Rew:2.0,1292.0')] ).

cnf(1295,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,unisex(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1288]),
    [iquote('0:Rew:2.0,1288.0')] ).

cnf(1294,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,unisex(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1287]),
    [iquote('0:Rew:2.0,1287.0')] ).

cnf(1293,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,unisex(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1286]),
    [iquote('0:Rew:2.0,1286.0')] ).

cnf(1246,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,organism(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1241]),
    [iquote('0:Rew:2.0,1241.0')] ).

cnf(1255,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,present(u,skc13),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1252]),
    [iquote('0:Rew:2.0,1252.0')] ).

cnf(2042,plain,
    equal(ifeq3(entity(skc10,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2017,26]),
    [iquote('0:SpR:2017.0,26.0')] ).

cnf(2038,plain,
    equal(ifeq3(present(skc8,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[82,1253]),
    [iquote('0:SpR:82.0,1253.0')] ).

cnf(2021,plain,
    equal(ifeq3(abstraction(skc10,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[2015,18]),
    [iquote('0:SpR:2015.0,18.0')] ).

cnf(1998,plain,
    equal(ifeq3(dance(skc10,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1984,5]),
    [iquote('0:SpR:1984.0,5.0')] ).

cnf(1254,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,present(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1251]),
    [iquote('0:Rew:2.0,1251.0')] ).

cnf(2057,plain,
    equal(singleton(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2052]),
    [iquote('0:Rew:2.0,2052.0')] ).

cnf(2040,plain,
    equal(present(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2039]),
    [iquote('0:Rew:2.0,2039.0')] ).

cnf(2018,plain,
    equal(thing(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2010]),
    [iquote('0:Rew:2.0,2010.0')] ).

cnf(2017,plain,
    equal(specific(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2009]),
    [iquote('0:Rew:2.0,2009.0')] ).

cnf(1253,plain,
    equal(ifeq3(present(skc8,u),true__dfg,present(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1250]),
    [iquote('0:Rew:2.0,1250.0')] ).

cnf(2016,plain,
    equal(nonexistent(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2008]),
    [iquote('0:Rew:2.0,2008.0')] ).

cnf(2015,plain,
    equal(unisex(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,2007]),
    [iquote('0:Rew:2.0,2007.0')] ).

cnf(2004,plain,
    equal(eventuality(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1997]),
    [iquote('0:Rew:2.0,1997.0')] ).

cnf(1984,plain,
    equal(event(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1977]),
    [iquote('0:Rew:2.0,1977.0')] ).

cnf(1211,plain,
    equal(ifeq3(desire_want(skc8,u),true__dfg,desire_want(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1209]),
    [iquote('0:Rew:2.0,1209.0')] ).

cnf(1976,plain,
    equal(desire_want(skc10,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1975]),
    [iquote('0:Rew:2.0,1975.0')] ).

cnf(1210,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,desire_want(u,skc9),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1208]),
    [iquote('0:Rew:2.0,1208.0')] ).

cnf(1179,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,entity(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1174]),
    [iquote('0:Rew:2.0,1174.0')] ).

cnf(1160,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,relation(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1155]),
    [iquote('0:Rew:2.0,1155.0')] ).

cnf(1197,plain,
    equal(ifeq3(proposition(skc8,u),true__dfg,proposition(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1195]),
    [iquote('0:Rew:2.0,1195.0')] ).

cnf(1159,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,relation(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1154]),
    [iquote('0:Rew:2.0,1154.0')] ).

cnf(1158,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,relation(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1153]),
    [iquote('0:Rew:2.0,1153.0')] ).

cnf(1157,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,relation(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1152]),
    [iquote('0:Rew:2.0,1152.0')] ).

cnf(1928,plain,
    equal(proposition(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1927]),
    [iquote('0:Rew:2.0,1927.0')] ).

cnf(1196,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,proposition(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1194]),
    [iquote('0:Rew:2.0,1194.0')] ).

cnf(1124,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,abstraction(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1119]),
    [iquote('0:Rew:2.0,1119.0')] ).

cnf(1910,plain,
    equal(ifeq3(relname(skc10,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1908,20]),
    [iquote('0:SpR:1908.0,20.0')] ).

cnf(1908,plain,
    equal(relation(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1902]),
    [iquote('0:Rew:2.0,1902.0')] ).

cnf(1161,plain,
    equal(ifeq3(relation(skc8,u),true__dfg,relation(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1156]),
    [iquote('0:Rew:2.0,1156.0')] ).

cnf(1862,plain,
    equal(ifeq3(entity(skc10,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1850,25]),
    [iquote('0:SpR:1850.0,25.0')] ).

cnf(1854,plain,
    equal(ifeq3(eventuality(skc10,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1847,11]),
    [iquote('0:SpR:1847.0,11.0')] ).

cnf(1870,plain,
    equal(singleton(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1864]),
    [iquote('0:Rew:2.0,1864.0')] ).

cnf(1125,plain,
    equal(ifeq3(abstraction(skc8,u),true__dfg,abstraction(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1120]),
    [iquote('0:Rew:2.0,1120.0')] ).

cnf(1850,plain,
    equal(thing(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1841]),
    [iquote('0:Rew:2.0,1841.0')] ).

cnf(1847,plain,
    equal(unisex(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1838]),
    [iquote('0:Rew:2.0,1838.0')] ).

cnf(1836,plain,
    equal(abstraction(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1835]),
    [iquote('0:Rew:2.0,1835.0')] ).

cnf(1123,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,abstraction(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1118]),
    [iquote('0:Rew:2.0,1118.0')] ).

cnf(97,axiom,
    equal(ifeq(tuple(dance(u,v),event(u,v),desire_want(skc8,w),proposition(skc8,u),accessible_world(skc8,u),present(u,v),present(skc8,w),agent(u,v,skc15),agent(skc8,w,skc15),theme(skc8,w,u)),tuple(true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1122,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,abstraction(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1117]),
    [iquote('0:Rew:2.0,1117.0')] ).

cnf(1121,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,abstraction(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1116]),
    [iquote('0:Rew:2.0,1116.0')] ).

cnf(1110,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,existent(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1108]),
    [iquote('0:Rew:2.0,1108.0')] ).

cnf(1081,plain,
    equal(ifeq3(nonhuman(skc8,u),true__dfg,nonhuman(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1076]),
    [iquote('0:Rew:2.0,1076.0')] ).

cnf(71,axiom,
    equal(ifeq4(theme(u,v,w),true__dfg,ifeq4(theme(u,x,y),true__dfg,ifeq4(proposition(u,w),true__dfg,ifeq4(proposition(u,y),true__dfg,ifeq4(desire_want(u,v),true__dfg,ifeq4(desire_want(u,x),true__dfg,w,y),y),y),y),y),y),y),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1080,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,nonhuman(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1075]),
    [iquote('0:Rew:2.0,1075.0')] ).

cnf(1757,plain,
    equal(nonhuman(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1756]),
    [iquote('0:Rew:2.0,1756.0')] ).

cnf(1079,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,nonhuman(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1074]),
    [iquote('0:Rew:2.0,1074.0')] ).

cnf(1078,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,nonhuman(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1073]),
    [iquote('0:Rew:2.0,1073.0')] ).

cnf(70,axiom,
    equal(ifeq4(of(u,v,w),true__dfg,ifeq4(of(u,x,w),true__dfg,ifeq4(entity(u,w),true__dfg,ifeq4(forename(u,v),true__dfg,ifeq4(forename(u,x),true__dfg,v,x),x),x),x),x),x),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1077,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,nonhuman(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1072]),
    [iquote('0:Rew:2.0,1072.0')] ).

cnf(1063,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,impartial(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1060]),
    [iquote('0:Rew:2.0,1060.0')] ).

cnf(1046,plain,
    equal(ifeq3(general(skc8,u),true__dfg,general(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1041]),
    [iquote('0:Rew:2.0,1041.0')] ).

cnf(1045,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,general(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1040]),
    [iquote('0:Rew:2.0,1040.0')] ).

cnf(67,axiom,
    equal(ifeq3(agent(u,v,w),true__dfg,ifeq3(accessible_world(u,x),true__dfg,agent(x,v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1669,plain,
    equal(general(skc10,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1668]),
    [iquote('0:Rew:2.0,1668.0')] ).

cnf(1044,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,general(u,skc10),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1039]),
    [iquote('0:Rew:2.0,1039.0')] ).

cnf(1043,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,general(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1038]),
    [iquote('0:Rew:2.0,1038.0')] ).

cnf(68,axiom,
    equal(ifeq3(theme(u,v,w),true__dfg,ifeq3(accessible_world(u,x),true__dfg,theme(x,v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1042,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,general(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1037]),
    [iquote('0:Rew:2.0,1037.0')] ).

cnf(1013,plain,
    equal(ifeq3(forename(skc8,u),true__dfg,forename(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1009]),
    [iquote('0:Rew:2.0,1009.0')] ).

cnf(1012,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,forename(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1008]),
    [iquote('0:Rew:2.0,1008.0')] ).

cnf(1011,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,forename(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1007]),
    [iquote('0:Rew:2.0,1007.0')] ).

cnf(69,axiom,
    equal(ifeq3(of(u,v,w),true__dfg,ifeq3(accessible_world(u,x),true__dfg,of(x,v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1010,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,forename(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1006]),
    [iquote('0:Rew:2.0,1006.0')] ).

cnf(1001,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,living(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,998]),
    [iquote('0:Rew:2.0,998.0')] ).

cnf(973,plain,
    equal(ifeq3(relname(skc8,u),true__dfg,relname(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,969]),
    [iquote('0:Rew:2.0,969.0')] ).

cnf(972,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,relname(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,968]),
    [iquote('0:Rew:2.0,968.0')] ).

cnf(36,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(dance(u,w),true__dfg,dance(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(971,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,relname(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,967]),
    [iquote('0:Rew:2.0,967.0')] ).

cnf(970,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,relname(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,966]),
    [iquote('0:Rew:2.0,966.0')] ).

cnf(958,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,human(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,955]),
    [iquote('0:Rew:2.0,955.0')] ).

cnf(940,plain,
    equal(ifeq3(mia_forename(skc8,u),true__dfg,mia_forename(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,938]),
    [iquote('0:Rew:2.0,938.0')] ).

cnf(37,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(event(u,w),true__dfg,event(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1530,plain,
    equal(ifeq3(entity(skc10,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1471,25]),
    [iquote('0:SpR:1471.0,25.0')] ).

cnf(1475,plain,
    equal(ifeq3(eventuality(skc10,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1468,11]),
    [iquote('0:SpR:1468.0,11.0')] ).

cnf(1453,plain,
    equal(ifeq3(proposition(skc10,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1448,13]),
    [iquote('0:SpR:1448.0,13.0')] ).

cnf(1401,plain,
    equal(ifeq3(vincent_forename(skc10,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1398,33]),
    [iquote('0:SpR:1398.0,33.0')] ).

cnf(38,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(eventuality(u,w),true__dfg,eventuality(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1538,plain,
    equal(singleton(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1532]),
    [iquote('0:Rew:2.0,1532.0')] ).

cnf(1471,plain,
    equal(thing(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1463]),
    [iquote('0:Rew:2.0,1463.0')] ).

cnf(1470,plain,
    equal(nonhuman(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1462]),
    [iquote('0:Rew:2.0,1462.0')] ).

cnf(1469,plain,
    equal(general(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1461]),
    [iquote('0:Rew:2.0,1461.0')] ).

cnf(39,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(thing(u,w),true__dfg,thing(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1468,plain,
    equal(unisex(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1460]),
    [iquote('0:Rew:2.0,1460.0')] ).

cnf(1458,plain,
    equal(abstraction(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1452]),
    [iquote('0:Rew:2.0,1452.0')] ).

cnf(1448,plain,
    equal(relation(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1443]),
    [iquote('0:Rew:2.0,1443.0')] ).

cnf(1408,plain,
    equal(relname(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1403]),
    [iquote('0:Rew:2.0,1403.0')] ).

cnf(40,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(singleton(u,w),true__dfg,singleton(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1398,plain,
    equal(forename(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1393]),
    [iquote('0:Rew:2.0,1393.0')] ).

cnf(1392,plain,
    equal(mia_forename(skc10,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1391]),
    [iquote('0:Rew:2.0,1391.0')] ).

cnf(939,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,mia_forename(u,skc11),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,937]),
    [iquote('0:Rew:2.0,937.0')] ).

cnf(919,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,animate(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,916]),
    [iquote('0:Rew:2.0,916.0')] ).

cnf(41,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(specific(u,w),true__dfg,specific(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(912,plain,
    equal(ifeq3(woman(skc8,u),true__dfg,woman(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,910]),
    [iquote('0:Rew:2.0,910.0')] ).

cnf(1346,plain,
    equal(woman(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1345]),
    [iquote('0:Rew:2.0,1345.0')] ).

cnf(911,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,woman(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,909]),
    [iquote('0:Rew:2.0,909.0')] ).

cnf(888,plain,
    equal(ifeq3(human_person(skc8,u),true__dfg,human_person(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,884]),
    [iquote('0:Rew:2.0,884.0')] ).

cnf(42,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(nonexistent(u,w),true__dfg,nonexistent(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(887,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,human_person(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,883]),
    [iquote('0:Rew:2.0,883.0')] ).

cnf(1305,plain,
    equal(ifeq3(man(skc10,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1303,34]),
    [iquote('0:SpR:1303.0,34.0')] ).

cnf(1303,plain,
    equal(human_person(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1302]),
    [iquote('0:Rew:2.0,1302.0')] ).

cnf(886,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,human_person(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,882]),
    [iquote('0:Rew:2.0,882.0')] ).

cnf(43,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(unisex(u,w),true__dfg,unisex(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(885,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,human_person(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,881]),
    [iquote('0:Rew:2.0,881.0')] ).

cnf(876,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,female(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,873]),
    [iquote('0:Rew:2.0,873.0')] ).

cnf(853,plain,
    equal(ifeq3(organism(skc8,u),true__dfg,organism(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,849]),
    [iquote('0:Rew:2.0,849.0')] ).

cnf(852,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,organism(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,848]),
    [iquote('0:Rew:2.0,848.0')] ).

cnf(44,axiom,
    equal(ifeq3(present(u,v),true__dfg,ifeq3(accessible_world(u,w),true__dfg,present(w,v),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1232,plain,
    equal(organism(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1231]),
    [iquote('0:Rew:2.0,1231.0')] ).

cnf(851,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,organism(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,847]),
    [iquote('0:Rew:2.0,847.0')] ).

cnf(850,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,organism(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,846]),
    [iquote('0:Rew:2.0,846.0')] ).

cnf(837,plain,
    equal(ifeq3(entity(skc8,u),true__dfg,entity(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,833]),
    [iquote('0:Rew:2.0,833.0')] ).

cnf(45,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(desire_want(u,w),true__dfg,desire_want(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(836,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,entity(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,832]),
    [iquote('0:Rew:2.0,832.0')] ).

cnf(1186,plain,
    equal(ifeq3(abstraction(skc10,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1177,15]),
    [iquote('0:SpR:1177.0,15.0')] ).

cnf(1181,plain,
    equal(ifeq3(eventuality(skc10,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[1176,9]),
    [iquote('0:SpR:1176.0,9.0')] ).

cnf(1191,plain,
    equal(singleton(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1187]),
    [iquote('0:Rew:2.0,1187.0')] ).

cnf(46,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(proposition(u,w),true__dfg,proposition(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1177,plain,
    equal(thing(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1169]),
    [iquote('0:Rew:2.0,1169.0')] ).

cnf(1176,plain,
    equal(specific(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1168]),
    [iquote('0:Rew:2.0,1168.0')] ).

cnf(1165,plain,
    equal(entity(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1164]),
    [iquote('0:Rew:2.0,1164.0')] ).

cnf(835,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,entity(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,831]),
    [iquote('0:Rew:2.0,831.0')] ).

cnf(47,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(relation(u,w),true__dfg,relation(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(834,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,entity(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,830]),
    [iquote('0:Rew:2.0,830.0')] ).

cnf(807,plain,
    equal(ifeq3(existent(skc8,u),true__dfg,existent(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,803]),
    [iquote('0:Rew:2.0,803.0')] ).

cnf(806,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,existent(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,802]),
    [iquote('0:Rew:2.0,802.0')] ).

cnf(48,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(abstraction(u,w),true__dfg,abstraction(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1102,plain,
    equal(existent(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1101]),
    [iquote('0:Rew:2.0,1101.0')] ).

cnf(805,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,existent(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,801]),
    [iquote('0:Rew:2.0,801.0')] ).

cnf(804,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,existent(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,800]),
    [iquote('0:Rew:2.0,800.0')] ).

cnf(767,plain,
    equal(ifeq3(impartial(skc8,u),true__dfg,impartial(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,763]),
    [iquote('0:Rew:2.0,763.0')] ).

cnf(49,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(nonhuman(u,w),true__dfg,nonhuman(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(766,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,impartial(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,762]),
    [iquote('0:Rew:2.0,762.0')] ).

cnf(1056,plain,
    equal(impartial(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,1055]),
    [iquote('0:Rew:2.0,1055.0')] ).

cnf(765,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,impartial(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,761]),
    [iquote('0:Rew:2.0,761.0')] ).

cnf(764,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,impartial(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,760]),
    [iquote('0:Rew:2.0,760.0')] ).

cnf(50,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(general(u,w),true__dfg,general(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(749,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,vincent_forename(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,745]),
    [iquote('0:Rew:2.0,745.0')] ).

cnf(730,plain,
    equal(ifeq3(living(skc8,u),true__dfg,living(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,726]),
    [iquote('0:Rew:2.0,726.0')] ).

cnf(729,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,living(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,725]),
    [iquote('0:Rew:2.0,725.0')] ).

cnf(51,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(forename(u,w),true__dfg,forename(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(994,plain,
    equal(living(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,993]),
    [iquote('0:Rew:2.0,993.0')] ).

cnf(728,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,living(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,724]),
    [iquote('0:Rew:2.0,724.0')] ).

cnf(727,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,living(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,723]),
    [iquote('0:Rew:2.0,723.0')] ).

cnf(712,plain,
    equal(ifeq3(human(skc8,u),true__dfg,human(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,708]),
    [iquote('0:Rew:2.0,708.0')] ).

cnf(52,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(relname(u,w),true__dfg,relname(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(711,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,human(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,707]),
    [iquote('0:Rew:2.0,707.0')] ).

cnf(950,plain,
    equal(human(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,949]),
    [iquote('0:Rew:2.0,949.0')] ).

cnf(710,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,human(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,706]),
    [iquote('0:Rew:2.0,706.0')] ).

cnf(709,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,human(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,705]),
    [iquote('0:Rew:2.0,705.0')] ).

cnf(53,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(mia_forename(u,w),true__dfg,mia_forename(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(675,plain,
    equal(ifeq3(animate(skc8,u),true__dfg,animate(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,671]),
    [iquote('0:Rew:2.0,671.0')] ).

cnf(674,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,animate(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,670]),
    [iquote('0:Rew:2.0,670.0')] ).

cnf(906,plain,
    equal(animate(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,905]),
    [iquote('0:Rew:2.0,905.0')] ).

cnf(54,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(woman(u,w),true__dfg,woman(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(673,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,animate(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,669]),
    [iquote('0:Rew:2.0,669.0')] ).

cnf(672,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,animate(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,668]),
    [iquote('0:Rew:2.0,668.0')] ).

cnf(644,plain,
    equal(ifeq3(female(skc8,u),true__dfg,female(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,642]),
    [iquote('0:Rew:2.0,642.0')] ).

cnf(55,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(human_person(u,w),true__dfg,human_person(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(867,plain,
    equal(female(skc10,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,866]),
    [iquote('0:Rew:2.0,866.0')] ).

cnf(643,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,female(u,skc12),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,641]),
    [iquote('0:Rew:2.0,641.0')] ).

cnf(625,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,man(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,621]),
    [iquote('0:Rew:2.0,621.0')] ).

cnf(610,plain,
    equal(ifeq3(vincent_forename(skc8,u),true__dfg,vincent_forename(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,608]),
    [iquote('0:Rew:2.0,608.0')] ).

cnf(56,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(organism(u,w),true__dfg,organism(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(816,plain,
    equal(ifeq3(entity(skc10,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[788,25]),
    [iquote('0:SpR:788.0,25.0')] ).

cnf(791,plain,
    equal(ifeq3(eventuality(skc10,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[785,11]),
    [iquote('0:SpR:785.0,11.0')] ).

cnf(775,plain,
    equal(ifeq3(proposition(skc10,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[771,13]),
    [iquote('0:SpR:771.0,13.0')] ).

cnf(751,plain,
    equal(ifeq3(mia_forename(skc10,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[747,21]),
    [iquote('0:SpR:747.0,21.0')] ).

cnf(57,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(entity(u,w),true__dfg,entity(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(822,plain,
    equal(singleton(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,818]),
    [iquote('0:Rew:2.0,818.0')] ).

cnf(788,plain,
    equal(thing(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,782]),
    [iquote('0:Rew:2.0,782.0')] ).

cnf(787,plain,
    equal(nonhuman(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,781]),
    [iquote('0:Rew:2.0,781.0')] ).

cnf(786,plain,
    equal(general(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,780]),
    [iquote('0:Rew:2.0,780.0')] ).

cnf(58,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(existent(u,w),true__dfg,existent(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(785,plain,
    equal(unisex(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,779]),
    [iquote('0:Rew:2.0,779.0')] ).

cnf(778,plain,
    equal(abstraction(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,774]),
    [iquote('0:Rew:2.0,774.0')] ).

cnf(771,plain,
    equal(relation(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,768]),
    [iquote('0:Rew:2.0,768.0')] ).

cnf(755,plain,
    equal(relname(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,752]),
    [iquote('0:Rew:2.0,752.0')] ).

cnf(59,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(impartial(u,w),true__dfg,impartial(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(747,plain,
    equal(forename(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,742]),
    [iquote('0:Rew:2.0,742.0')] ).

cnf(741,plain,
    equal(vincent_forename(skc10,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,740]),
    [iquote('0:Rew:2.0,740.0')] ).

cnf(609,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,vincent_forename(u,skc14),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,607]),
    [iquote('0:Rew:2.0,607.0')] ).

cnf(592,plain,
    equal(ifeq3(man(skc8,u),true__dfg,man(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,590]),
    [iquote('0:Rew:2.0,590.0')] ).

cnf(60,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(living(u,w),true__dfg,living(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(695,plain,
    equal(ifeq3(abstraction(skc10,skc15),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[683,15]),
    [iquote('0:SpR:683.0,15.0')] ).

cnf(690,plain,
    equal(ifeq3(eventuality(skc10,skc15),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[682,9]),
    [iquote('0:SpR:682.0,9.0')] ).

cnf(630,plain,
    equal(ifeq3(woman(skc10,skc15),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[623,22]),
    [iquote('0:SpR:623.0,22.0')] ).

cnf(700,plain,
    equal(singleton(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,696]),
    [iquote('0:Rew:2.0,696.0')] ).

cnf(61,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(human(u,w),true__dfg,human(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(683,plain,
    equal(thing(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,678]),
    [iquote('0:Rew:2.0,678.0')] ).

cnf(682,plain,
    equal(specific(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,677]),
    [iquote('0:Rew:2.0,677.0')] ).

cnf(681,plain,
    equal(existent(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,676]),
    [iquote('0:Rew:2.0,676.0')] ).

cnf(656,plain,
    equal(entity(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,651]),
    [iquote('0:Rew:2.0,651.0')] ).

cnf(62,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(animate(u,w),true__dfg,animate(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(655,plain,
    equal(impartial(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,650]),
    [iquote('0:Rew:2.0,650.0')] ).

cnf(654,plain,
    equal(living(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,649]),
    [iquote('0:Rew:2.0,649.0')] ).

cnf(635,plain,
    equal(organism(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,629]),
    [iquote('0:Rew:2.0,629.0')] ).

cnf(634,plain,
    equal(human(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,628]),
    [iquote('0:Rew:2.0,628.0')] ).

cnf(63,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(female(u,w),true__dfg,female(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(633,plain,
    equal(animate(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,627]),
    [iquote('0:Rew:2.0,627.0')] ).

cnf(623,plain,
    equal(human_person(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,617]),
    [iquote('0:Rew:2.0,617.0')] ).

cnf(614,plain,
    equal(man(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,613]),
    [iquote('0:Rew:2.0,613.0')] ).

cnf(591,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,man(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,589]),
    [iquote('0:Rew:2.0,589.0')] ).

cnf(64,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(vincent_forename(u,w),true__dfg,vincent_forename(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(602,plain,
    equal(ifeq3(accessible_world(skc10,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[575,584]),
    [iquote('0:SpR:575.0,584.0')] ).

cnf(601,plain,
    equal(ifeq3(accessible_world(skc10,skc8),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[124,584]),
    [iquote('0:SpR:124.0,584.0')] ).

cnf(584,plain,
    equal(ifeq3(accessible_world(skc10,u),true__dfg,male(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,581]),
    [iquote('0:Rew:2.0,581.0')] ).

cnf(571,plain,
    equal(ifeq3(male(skc8,u),true__dfg,male(skc10,u),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,569]),
    [iquote('0:Rew:2.0,569.0')] ).

cnf(65,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(man(u,w),true__dfg,man(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(573,plain,
    equal(ifeq3(accessible_world(skc8,skc8),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[124,570]),
    [iquote('0:SpR:124.0,570.0')] ).

cnf(575,plain,
    equal(male(skc10,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,574]),
    [iquote('0:Rew:2.0,574.0')] ).

cnf(570,plain,
    equal(ifeq3(accessible_world(skc8,u),true__dfg,male(u,skc15),true__dfg),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,568]),
    [iquote('0:Rew:2.0,568.0')] ).

cnf(66,axiom,
    equal(ifeq3(accessible_world(u,v),true__dfg,ifeq3(male(u,w),true__dfg,male(v,w),true__dfg),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(526,plain,
    equal(ifeq2(tuple2(true__dfg,human(skc8,skc11)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[322,75]),
    [iquote('0:SpR:322.0,75.0')] ).

cnf(525,plain,
    equal(ifeq2(tuple2(true__dfg,human(skc8,skc14)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[306,75]),
    [iquote('0:SpR:306.0,75.0')] ).

cnf(524,plain,
    equal(ifeq2(tuple2(nonhuman(skc8,skc12),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[203,75]),
    [iquote('0:SpR:203.0,75.0')] ).

cnf(523,plain,
    equal(ifeq2(tuple2(nonhuman(skc8,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[155,75]),
    [iquote('0:SpR:155.0,75.0')] ).

cnf(72,axiom,
    equal(ifeq2(tuple2(unisex(u,v),male(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(517,plain,
    equal(ifeq2(tuple2(true__dfg,male(skc8,skc12)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[142,76]),
    [iquote('0:SpR:142.0,76.0')] ).

cnf(516,plain,
    equal(ifeq2(tuple2(female(skc8,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[124,76]),
    [iquote('0:SpR:124.0,76.0')] ).

cnf(497,plain,
    equal(ifeq2(tuple2(true__dfg,existent(skc8,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[458,77]),
    [iquote('0:SpR:458.0,77.0')] ).

cnf(496,plain,
    equal(ifeq2(tuple2(true__dfg,existent(skc10,skc13)),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[447,77]),
    [iquote('0:SpR:447.0,77.0')] ).

cnf(73,axiom,
    equal(ifeq2(tuple2(unisex(u,v),female(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(495,plain,
    equal(ifeq2(tuple2(nonexistent(skc8,skc12),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[253,77]),
    [iquote('0:SpR:253.0,77.0')] ).

cnf(494,plain,
    equal(ifeq2(tuple2(nonexistent(skc8,skc15),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
    inference(spr,[status(thm),theory(equality)],[192,77]),
    [iquote('0:SpR:192.0,77.0')] ).

cnf(498,plain,
    equal(ifeq3(entity(skc8,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[459,26]),
    [iquote('0:SpR:459.0,26.0')] ).

cnf(486,plain,
    equal(ifeq3(abstraction(skc8,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[457,18]),
    [iquote('0:SpR:457.0,18.0')] ).

cnf(74,axiom,
    equal(ifeq2(tuple2(specific(u,v),general(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(475,plain,
    equal(ifeq3(entity(skc10,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[448,26]),
    [iquote('0:SpR:448.0,26.0')] ).

cnf(471,plain,
    equal(ifeq3(dance(skc8,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[337,5]),
    [iquote('0:SpR:337.0,5.0')] ).

cnf(462,plain,
    equal(ifeq3(abstraction(skc10,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[446,18]),
    [iquote('0:SpR:446.0,18.0')] ).

cnf(395,plain,
    equal(ifeq3(eventuality(skc8,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[254,9]),
    [iquote('0:SpR:254.0,9.0')] ).

cnf(75,axiom,
    equal(ifeq2(tuple2(nonhuman(u,v),human(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(394,plain,
    equal(ifeq3(eventuality(skc8,skc15),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[193,9]),
    [iquote('0:SpR:193.0,9.0')] ).

cnf(389,plain,
    equal(ifeq3(entity(skc8,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[376,25]),
    [iquote('0:SpR:376.0,25.0')] ).

cnf(380,plain,
    equal(ifeq3(eventuality(skc8,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[373,11]),
    [iquote('0:SpR:373.0,11.0')] ).

cnf(360,plain,
    equal(ifeq3(entity(skc8,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[323,25]),
    [iquote('0:SpR:323.0,25.0')] ).

cnf(76,axiom,
    equal(ifeq2(tuple2(female(u,v),male(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(507,plain,
    equal(singleton(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,504]),
    [iquote('0:Rew:2.0,504.0')] ).

cnf(484,plain,
    equal(singleton(skc10,skc13),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,481]),
    [iquote('0:Rew:2.0,481.0')] ).

cnf(460,plain,
    equal(thing(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,454]),
    [iquote('0:Rew:2.0,454.0')] ).

cnf(459,plain,
    equal(specific(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,453]),
    [iquote('0:Rew:2.0,453.0')] ).

cnf(77,axiom,
    equal(ifeq2(tuple2(nonexistent(u,v),existent(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
    file('NLP024-10.p',unknown),
    [] ).

cnf(458,plain,
    equal(nonexistent(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,452]),
    [iquote('0:Rew:2.0,452.0')] ).

cnf(457,plain,
    equal(unisex(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,451]),
    [iquote('0:Rew:2.0,451.0')] ).

cnf(449,plain,
    equal(thing(skc10,skc13),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,443]),
    [iquote('0:Rew:2.0,443.0')] ).

cnf(448,plain,
    equal(specific(skc10,skc13),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,442]),
    [iquote('0:Rew:2.0,442.0')] ).

cnf(5,axiom,
    equal(ifeq3(dance(u,v),true__dfg,event(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(447,plain,
    equal(nonexistent(skc10,skc13),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,441]),
    [iquote('0:Rew:2.0,441.0')] ).

cnf(446,plain,
    equal(unisex(skc10,skc13),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,440]),
    [iquote('0:Rew:2.0,440.0')] ).

cnf(439,plain,
    equal(eventuality(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,437]),
    [iquote('0:Rew:2.0,437.0')] ).

cnf(438,plain,
    equal(eventuality(skc10,skc13),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,436]),
    [iquote('0:Rew:2.0,436.0')] ).

cnf(6,axiom,
    equal(ifeq3(event(u,v),true__dfg,eventuality(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(356,plain,
    equal(ifeq3(eventuality(skc8,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[320,11]),
    [iquote('0:SpR:320.0,11.0')] ).

cnf(355,plain,
    equal(ifeq3(eventuality(skc8,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[304,11]),
    [iquote('0:SpR:304.0,11.0')] ).

cnf(342,plain,
    equal(ifeq3(relname(skc8,skc10),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[313,20]),
    [iquote('0:SpR:313.0,20.0')] ).

cnf(410,plain,
    equal(singleton(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,405]),
    [iquote('0:Rew:2.0,405.0')] ).

cnf(7,axiom,
    equal(ifeq3(eventuality(u,v),true__dfg,thing(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(409,plain,
    equal(singleton(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,404]),
    [iquote('0:Rew:2.0,404.0')] ).

cnf(408,plain,
    equal(singleton(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,403]),
    [iquote('0:Rew:2.0,403.0')] ).

cnf(407,plain,
    equal(singleton(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,402]),
    [iquote('0:Rew:2.0,402.0')] ).

cnf(406,plain,
    equal(singleton(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,401]),
    [iquote('0:Rew:2.0,401.0')] ).

cnf(8,axiom,
    equal(ifeq3(thing(u,v),true__dfg,singleton(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(338,plain,
    equal(ifeq3(entity(skc8,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[307,25]),
    [iquote('0:SpR:307.0,25.0')] ).

cnf(335,plain,
    equal(ifeq3(desire_want(skc10,skc13),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[80,12]),
    [iquote('0:SpR:80.0,12.0')] ).

cnf(311,plain,
    equal(ifeq3(proposition(skc8,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[265,13]),
    [iquote('0:SpR:265.0,13.0')] ).

cnf(310,plain,
    equal(ifeq3(proposition(skc8,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[260,13]),
    [iquote('0:SpR:260.0,13.0')] ).

cnf(9,axiom,
    equal(ifeq3(eventuality(u,v),true__dfg,specific(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(376,plain,
    equal(thing(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,370]),
    [iquote('0:Rew:2.0,370.0')] ).

cnf(375,plain,
    equal(nonhuman(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,369]),
    [iquote('0:Rew:2.0,369.0')] ).

cnf(374,plain,
    equal(general(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,368]),
    [iquote('0:Rew:2.0,368.0')] ).

cnf(373,plain,
    equal(unisex(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,367]),
    [iquote('0:Rew:2.0,367.0')] ).

cnf(10,axiom,
    equal(ifeq3(eventuality(u,v),true__dfg,nonexistent(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(346,plain,
    equal(abstraction(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,343]),
    [iquote('0:Rew:2.0,343.0')] ).

cnf(337,plain,
    equal(event(skc8,skc9),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,336]),
    [iquote('0:Rew:2.0,336.0')] ).

cnf(323,plain,
    equal(thing(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,317]),
    [iquote('0:Rew:2.0,317.0')] ).

cnf(322,plain,
    equal(nonhuman(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,316]),
    [iquote('0:Rew:2.0,316.0')] ).

cnf(11,axiom,
    equal(ifeq3(eventuality(u,v),true__dfg,unisex(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(321,plain,
    equal(general(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,315]),
    [iquote('0:Rew:2.0,315.0')] ).

cnf(320,plain,
    equal(unisex(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,314]),
    [iquote('0:Rew:2.0,314.0')] ).

cnf(313,plain,
    equal(relation(skc8,skc10),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,312]),
    [iquote('0:Rew:2.0,312.0')] ).

cnf(307,plain,
    equal(thing(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,301]),
    [iquote('0:Rew:2.0,301.0')] ).

cnf(12,axiom,
    equal(ifeq3(desire_want(u,v),true__dfg,event(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(306,plain,
    equal(nonhuman(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,300]),
    [iquote('0:Rew:2.0,300.0')] ).

cnf(305,plain,
    equal(general(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,299]),
    [iquote('0:Rew:2.0,299.0')] ).

cnf(304,plain,
    equal(unisex(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,298]),
    [iquote('0:Rew:2.0,298.0')] ).

cnf(297,plain,
    equal(abstraction(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,295]),
    [iquote('0:Rew:2.0,295.0')] ).

cnf(13,axiom,
    equal(ifeq3(proposition(u,v),true__dfg,relation(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(296,plain,
    equal(abstraction(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,294]),
    [iquote('0:Rew:2.0,294.0')] ).

cnf(14,axiom,
    equal(ifeq3(relation(u,v),true__dfg,abstraction(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(290,plain,
    equal(ifeq3(abstraction(skc8,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[255,15]),
    [iquote('0:SpR:255.0,15.0')] ).

cnf(289,plain,
    equal(ifeq3(abstraction(skc8,skc15),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[194,15]),
    [iquote('0:SpR:194.0,15.0')] ).

cnf(15,axiom,
    equal(ifeq3(abstraction(u,v),true__dfg,thing(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(16,axiom,
    equal(ifeq3(abstraction(u,v),true__dfg,nonhuman(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(207,plain,
    equal(ifeq3(mia_forename(skc8,skc14),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[90,21]),
    [iquote('0:SpR:90.0,21.0')] ).

cnf(196,plain,
    equal(ifeq3(man(skc8,skc12),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[180,34]),
    [iquote('0:SpR:180.0,34.0')] ).

cnf(178,plain,
    equal(ifeq3(woman(skc8,skc15),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[130,22]),
    [iquote('0:SpR:130.0,22.0')] ).

cnf(17,axiom,
    equal(ifeq3(abstraction(u,v),true__dfg,general(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(265,plain,
    equal(relation(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,262]),
    [iquote('0:Rew:2.0,262.0')] ).

cnf(260,plain,
    equal(relation(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,257]),
    [iquote('0:Rew:2.0,257.0')] ).

cnf(255,plain,
    equal(thing(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,250]),
    [iquote('0:Rew:2.0,250.0')] ).

cnf(254,plain,
    equal(specific(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,249]),
    [iquote('0:Rew:2.0,249.0')] ).

cnf(18,axiom,
    equal(ifeq3(abstraction(u,v),true__dfg,unisex(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(253,plain,
    equal(existent(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,248]),
    [iquote('0:Rew:2.0,248.0')] ).

cnf(247,plain,
    equal(relname(skc8,skc11),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,245]),
    [iquote('0:Rew:2.0,245.0')] ).

cnf(246,plain,
    equal(relname(skc8,skc14),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,244]),
    [iquote('0:Rew:2.0,244.0')] ).

cnf(235,plain,
    equal(entity(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,230]),
    [iquote('0:Rew:2.0,230.0')] ).

cnf(19,axiom,
    equal(ifeq3(forename(u,v),true__dfg,relname(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(234,plain,
    equal(impartial(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,229]),
    [iquote('0:Rew:2.0,229.0')] ).

cnf(233,plain,
    equal(living(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,228]),
    [iquote('0:Rew:2.0,228.0')] ).

cnf(204,plain,
    equal(organism(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,199]),
    [iquote('0:Rew:2.0,199.0')] ).

cnf(203,plain,
    equal(human(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,198]),
    [iquote('0:Rew:2.0,198.0')] ).

cnf(20,axiom,
    equal(ifeq3(relname(u,v),true__dfg,relation(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(202,plain,
    equal(animate(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,197]),
    [iquote('0:Rew:2.0,197.0')] ).

cnf(194,plain,
    equal(thing(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,189]),
    [iquote('0:Rew:2.0,189.0')] ).

cnf(193,plain,
    equal(specific(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,188]),
    [iquote('0:Rew:2.0,188.0')] ).

cnf(192,plain,
    equal(existent(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,187]),
    [iquote('0:Rew:2.0,187.0')] ).

cnf(21,axiom,
    equal(ifeq3(mia_forename(u,v),true__dfg,forename(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(180,plain,
    equal(human_person(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,179]),
    [iquote('0:Rew:2.0,179.0')] ).

cnf(175,plain,
    equal(entity(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,170]),
    [iquote('0:Rew:2.0,170.0')] ).

cnf(174,plain,
    equal(impartial(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,169]),
    [iquote('0:Rew:2.0,169.0')] ).

cnf(173,plain,
    equal(living(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,168]),
    [iquote('0:Rew:2.0,168.0')] ).

cnf(22,axiom,
    equal(ifeq3(woman(u,v),true__dfg,human_person(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(167,plain,
    equal(organism(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,166]),
    [iquote('0:Rew:2.0,166.0')] ).

cnf(23,axiom,
    equal(ifeq3(human_person(u,v),true__dfg,organism(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(24,axiom,
    equal(ifeq3(organism(u,v),true__dfg,entity(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(25,axiom,
    equal(ifeq3(entity(u,v),true__dfg,thing(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(26,axiom,
    equal(ifeq3(entity(u,v),true__dfg,specific(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(27,axiom,
    equal(ifeq3(entity(u,v),true__dfg,existent(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(28,axiom,
    equal(ifeq3(organism(u,v),true__dfg,impartial(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(29,axiom,
    equal(ifeq3(organism(u,v),true__dfg,living(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(155,plain,
    equal(human(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,154]),
    [iquote('0:Rew:2.0,154.0')] ).

cnf(30,axiom,
    equal(ifeq3(human_person(u,v),true__dfg,human(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(149,plain,
    equal(animate(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,148]),
    [iquote('0:Rew:2.0,148.0')] ).

cnf(31,axiom,
    equal(ifeq3(human_person(u,v),true__dfg,animate(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(136,plain,
    equal(ifeq3(vincent_forename(skc8,skc11),true__dfg,true__dfg,true__dfg),true__dfg),
    inference(spr,[status(thm),theory(equality)],[84,33]),
    [iquote('0:SpR:84.0,33.0')] ).

cnf(142,plain,
    equal(female(skc8,skc12),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,141]),
    [iquote('0:Rew:2.0,141.0')] ).

cnf(32,axiom,
    equal(ifeq3(woman(u,v),true__dfg,female(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(33,axiom,
    equal(ifeq3(vincent_forename(u,v),true__dfg,forename(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(130,plain,
    equal(human_person(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,129]),
    [iquote('0:Rew:2.0,129.0')] ).

cnf(34,axiom,
    equal(ifeq3(man(u,v),true__dfg,human_person(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(124,plain,
    equal(male(skc8,skc15),true__dfg),
    inference(rew,[status(thm),theory(equality)],[2,123]),
    [iquote('0:Rew:2.0,123.0')] ).

cnf(35,axiom,
    equal(ifeq3(man(u,v),true__dfg,male(u,v),true__dfg),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(1,axiom,
    equal(ifeq4(u,u,v,w),v),
    file('NLP024-10.p',unknown),
    [] ).

cnf(2,axiom,
    equal(ifeq3(u,u,v,w),v),
    file('NLP024-10.p',unknown),
    [] ).

cnf(3,axiom,
    equal(ifeq2(u,u,v,w),v),
    file('NLP024-10.p',unknown),
    [] ).

cnf(4,axiom,
    equal(ifeq(u,u,v,w),v),
    file('NLP024-10.p',unknown),
    [] ).

cnf(92,axiom,
    equal(of(skc8,skc14,skc15),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(93,axiom,
    equal(of(skc8,skc11,skc12),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(94,axiom,
    equal(agent(skc8,skc9,skc12),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(95,axiom,
    equal(agent(skc10,skc13,skc12),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(96,axiom,
    equal(theme(skc8,skc9,skc10),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(79,axiom,
    equal(man(skc8,skc15),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(80,axiom,
    equal(event(skc10,skc13),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(81,axiom,
    equal(woman(skc8,skc12),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(82,axiom,
    equal(present(skc10,skc13),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(83,axiom,
    equal(dance(skc10,skc13),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(84,axiom,
    equal(forename(skc8,skc11),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(85,axiom,
    equal(mia_forename(skc8,skc11),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(86,axiom,
    equal(proposition(skc8,skc10),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(87,axiom,
    equal(accessible_world(skc8,skc10),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(88,axiom,
    equal(desire_want(skc8,skc9),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(89,axiom,
    equal(present(skc8,skc9),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(90,axiom,
    equal(forename(skc8,skc14),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(91,axiom,
    equal(vincent_forename(skc8,skc14),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

cnf(98,axiom,
    ~ equal(b,a),
    file('NLP024-10.p',unknown),
    [] ).

cnf(78,axiom,
    equal(actual_world(skc8),true__dfg),
    file('NLP024-10.p',unknown),
    [] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NLP024-10 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.13  % Command  : run_spass %d %s
% 0.12/0.34  % Computer : n020.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 600
% 0.12/0.34  % DateTime : Fri Jul  1 03:58:45 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 1.57/1.75  
% 1.57/1.75  SPASS V 3.9 
% 1.57/1.75  SPASS beiseite: Completion found.
% 1.57/1.75  % SZS status CounterSatisfiable
% 1.57/1.75  Problem: /export/starexec/sandbox/benchmark/theBenchmark.p 
% 1.57/1.75  SPASS derived 2705 clauses, backtracked 0 clauses, performed 0 splits and kept 751 clauses.
% 1.57/1.75  SPASS allocated 66499 KBytes.
% 1.57/1.75  SPASS spent	0:00:01.40 on the problem.
% 1.57/1.75  		0:00:00.04 for the input.
% 1.57/1.75  		0:00:00.00 for the FLOTTER CNF translation.
% 1.57/1.75  		0:00:00.20 for inferences.
% 1.57/1.75  		0:00:00.00 for the backtracking.
% 1.57/1.75  		0:00:01.10 for the reduction.
% 1.57/1.75  
% 1.57/1.75  
% 1.57/1.75   The saturated set of worked-off clauses is :
% 1.57/1.75  % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------