%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP042-10 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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:26:05 EDT 2022
% Result : Satisfiable 0.19s 0.46s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 403)
% Comments :
%------------------------------------------------------------------------------
cnf(412,plain,
equal(ifeq4(of(skc5,u,skc7),true__dfg,ifeq4(of(skc5,v,skc7),true__dfg,ifeq4(forename(skc5,u),true__dfg,ifeq4(forename(skc5,v),true__dfg,u,v),v),v),v),v),
inference(rew,[status(thm),theory(equality)],[1,403]),
[iquote('0:Rew:1.0,403.0')] ).
cnf(413,plain,
equal(ifeq4(of(skc5,u,skc9),true__dfg,ifeq4(of(skc5,v,skc9),true__dfg,ifeq4(forename(skc5,u),true__dfg,ifeq4(forename(skc5,v),true__dfg,u,v),v),v),v),v),
inference(rew,[status(thm),theory(equality)],[1,402]),
[iquote('0:Rew:1.0,402.0')] ).
cnf(449,plain,
equal(ifeq4(of(skc5,skc8,skc7),true__dfg,ifeq4(of(skc5,u,skc7),true__dfg,ifeq4(forename(skc5,u),true__dfg,skc8,u),u),u),u),
inference(rew,[status(thm),theory(equality)],[1,442]),
[iquote('0:Rew:1.0,442.0')] ).
cnf(437,plain,
equal(ifeq4(of(skc5,u,skc7),true__dfg,ifeq4(of(skc5,skc8,skc7),true__dfg,ifeq4(forename(skc5,u),true__dfg,u,skc8),skc8),skc8),skc8),
inference(rew,[status(thm),theory(equality)],[1,430]),
[iquote('0:Rew:1.0,430.0')] ).
cnf(458,plain,
equal(ifeq4(of(skc5,skc8,skc7),true__dfg,ifeq4(of(skc5,skc8,skc7),true__dfg,skc8,skc8),skc8),skc8),
inference(rew,[status(thm),theory(equality)],[1,453]),
[iquote('0:Rew:1.0,453.0')] ).
cnf(436,plain,
equal(ifeq4(of(skc5,skc8,u),true__dfg,ifeq4(of(skc5,skc8,u),true__dfg,ifeq4(entity(skc5,u),true__dfg,skc8,skc8),skc8),skc8),skc8),
inference(rew,[status(thm),theory(equality)],[1,431]),
[iquote('0:Rew:1.0,431.0')] ).
cnf(410,plain,
equal(ifeq4(of(skc5,skc8,u),true__dfg,ifeq4(of(skc5,v,u),true__dfg,ifeq4(forename(skc5,v),true__dfg,ifeq4(entity(skc5,u),true__dfg,skc8,v),v),v),v),v),
inference(rew,[status(thm),theory(equality)],[1,405]),
[iquote('0:Rew:1.0,405.0')] ).
cnf(411,plain,
equal(ifeq4(of(skc5,u,v),true__dfg,ifeq4(of(skc5,skc8,v),true__dfg,ifeq4(forename(skc5,u),true__dfg,ifeq4(entity(skc5,v),true__dfg,u,skc8),skc8),skc8),skc8),skc8),
inference(rew,[status(thm),theory(equality)],[1,404]),
[iquote('0:Rew:1.0,404.0')] ).
cnf(393,plain,
equal(ifeq(tuple(patient(skc5,skc6,u),true__dfg,agent(skc5,skc6,u)),tuple(true__dfg,true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[53,48]),
[iquote('0:SpR:53.0,48.0')] ).
cnf(408,plain,
equal(ifeq4(of(skc5,u,skc9),true__dfg,ifeq4(forename(skc5,u),true__dfg,skc8,u),u),u),
inference(rew,[status(thm),theory(equality)],[1,407,56,120]),
[iquote('0:Rew:1.0,407.0,1.0,407.0,56.0,407.0,1.0,407.0,120.0,407.0')] ).
cnf(409,plain,
equal(ifeq4(of(skc5,u,skc9),true__dfg,ifeq4(forename(skc5,u),true__dfg,u,skc8),skc8),skc8),
inference(rew,[status(thm),theory(equality)],[1,406,56,120]),
[iquote('0:Rew:1.0,406.0,1.0,406.0,56.0,406.0,1.0,406.0,120.0,406.0')] ).
cnf(41,axiom,
equal(ifeq4(of(u,v,w),true__dfg,ifeq4(of(u,x,w),true__dfg,ifeq4(forename(u,v),true__dfg,ifeq4(forename(u,x),true__dfg,ifeq4(entity(u,w),true__dfg,v,x),x),x),x),x),x),
file('NLP042-10.p',unknown),
[] ).
cnf(396,plain,
equal(ifeq(tuple(true__dfg,true__dfg,agent(skc5,skc6,skc7)),tuple(true__dfg,true__dfg,true__dfg),a,b),b),
inference(rew,[status(thm),theory(equality)],[53,394]),
[iquote('0:Rew:53.0,394.0')] ).
cnf(395,plain,
equal(ifeq(tuple(patient(skc5,skc6,skc9),true__dfg,true__dfg),tuple(true__dfg,true__dfg,true__dfg),a,b),b),
inference(rew,[status(thm),theory(equality)],[53,392]),
[iquote('0:Rew:53.0,392.0')] ).
cnf(386,plain,
equal(ifeq2(tuple2(true__dfg,female(skc5,skc6)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[313,42]),
[iquote('0:SpR:313.0,42.0')] ).
cnf(385,plain,
equal(ifeq2(tuple2(true__dfg,female(skc5,skc7)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[236,42]),
[iquote('0:SpR:236.0,42.0')] ).
cnf(48,axiom,
equal(ifeq(tuple(patient(u,v,w),nonreflexive(u,v),agent(u,v,w)),tuple(true__dfg,true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(384,plain,
equal(ifeq2(tuple2(true__dfg,female(skc5,skc8)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[156,42]),
[iquote('0:SpR:156.0,42.0')] ).
cnf(383,plain,
equal(ifeq2(tuple2(unisex(skc5,skc9),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[80,42]),
[iquote('0:SpR:80.0,42.0')] ).
cnf(379,plain,
equal(ifeq2(tuple2(true__dfg,general(skc5,skc6)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[315,43]),
[iquote('0:SpR:315.0,43.0')] ).
cnf(378,plain,
equal(ifeq2(tuple2(true__dfg,general(skc5,skc7)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[262,43]),
[iquote('0:SpR:262.0,43.0')] ).
cnf(42,axiom,
equal(ifeq2(tuple2(unisex(u,v),female(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(377,plain,
equal(ifeq2(tuple2(true__dfg,general(skc5,skc9)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[185,43]),
[iquote('0:SpR:185.0,43.0')] ).
cnf(376,plain,
equal(ifeq2(tuple2(specific(skc5,skc8),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[157,43]),
[iquote('0:SpR:157.0,43.0')] ).
cnf(43,axiom,
equal(ifeq2(tuple2(specific(u,v),general(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(373,plain,
equal(ifeq2(tuple2(true__dfg,living(skc5,skc7)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[238,44]),
[iquote('0:SpR:238.0,44.0')] ).
cnf(44,axiom,
equal(ifeq2(tuple2(nonliving(u,v),living(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(366,plain,
equal(ifeq2(tuple2(true__dfg,human(skc5,skc8)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[158,45]),
[iquote('0:SpR:158.0,45.0')] ).
cnf(365,plain,
equal(ifeq2(tuple2(nonhuman(skc5,skc9),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[99,45]),
[iquote('0:SpR:99.0,45.0')] ).
cnf(362,plain,
equal(ifeq2(tuple2(true__dfg,existent(skc5,skc6)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[314,46]),
[iquote('0:SpR:314.0,46.0')] ).
cnf(361,plain,
equal(ifeq2(tuple2(nonexistent(skc5,skc7),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[261,46]),
[iquote('0:SpR:261.0,46.0')] ).
cnf(45,axiom,
equal(ifeq2(tuple2(nonhuman(u,v),human(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(360,plain,
equal(ifeq2(tuple2(nonexistent(skc5,skc9),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[182,46]),
[iquote('0:SpR:182.0,46.0')] ).
cnf(46,axiom,
equal(ifeq2(tuple2(nonexistent(u,v),existent(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(356,plain,
equal(ifeq2(tuple2(true__dfg,animate(skc5,skc7)),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[238,47]),
[iquote('0:SpR:238.0,47.0')] ).
cnf(355,plain,
equal(ifeq2(tuple2(nonliving(skc5,skc9),true__dfg),tuple2(true__dfg,true__dfg),a,b),b),
inference(spr,[status(thm),theory(equality)],[98,47]),
[iquote('0:SpR:98.0,47.0')] ).
cnf(47,axiom,
equal(ifeq2(tuple2(nonliving(u,v),animate(u,v)),tuple2(true__dfg,true__dfg),a,b),b),
file('NLP042-10.p',unknown),
[] ).
cnf(328,plain,
equal(ifeq3(entity(skc5,skc6),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[315,20]),
[iquote('0:SpR:315.0,20.0')] ).
cnf(319,plain,
equal(ifeq3(object(skc5,skc6),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[313,24]),
[iquote('0:SpR:313.0,24.0')] ).
cnf(318,plain,
equal(ifeq3(abstraction(skc5,skc6),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[313,31]),
[iquote('0:SpR:313.0,31.0')] ).
cnf(344,plain,
equal(act(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,343]),
[iquote('0:Rew:2.0,343.0')] ).
cnf(5,axiom,
equal(ifeq3(order(u,v),true__dfg,act(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(337,plain,
equal(singleton(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,334]),
[iquote('0:Rew:2.0,334.0')] ).
cnf(316,plain,
equal(thing(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,310]),
[iquote('0:Rew:2.0,310.0')] ).
cnf(315,plain,
equal(specific(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,309]),
[iquote('0:Rew:2.0,309.0')] ).
cnf(314,plain,
equal(nonexistent(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,308]),
[iquote('0:Rew:2.0,308.0')] ).
cnf(6,axiom,
equal(ifeq3(act(u,v),true__dfg,event(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(313,plain,
equal(unisex(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,307]),
[iquote('0:Rew:2.0,307.0')] ).
cnf(306,plain,
equal(eventuality(skc5,skc6),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,305]),
[iquote('0:Rew:2.0,305.0')] ).
cnf(7,axiom,
equal(ifeq3(event(u,v),true__dfg,eventuality(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(290,plain,
equal(singleton(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,287]),
[iquote('0:Rew:2.0,287.0')] ).
cnf(8,axiom,
equal(ifeq3(eventuality(u,v),true__dfg,thing(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(289,plain,
equal(singleton(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,286]),
[iquote('0:Rew:2.0,286.0')] ).
cnf(288,plain,
equal(singleton(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,285]),
[iquote('0:Rew:2.0,285.0')] ).
cnf(9,axiom,
equal(ifeq3(thing(u,v),true__dfg,singleton(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(281,plain,
equal(ifeq3(eventuality(skc5,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[185,10]),
[iquote('0:SpR:185.0,10.0')] ).
cnf(10,axiom,
equal(ifeq3(eventuality(u,v),true__dfg,specific(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(254,plain,
equal(ifeq3(eventuality(skc5,skc7),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[236,12]),
[iquote('0:SpR:236.0,12.0')] ).
cnf(253,plain,
equal(ifeq3(eventuality(skc5,skc8),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[156,12]),
[iquote('0:SpR:156.0,12.0')] ).
cnf(245,plain,
equal(ifeq3(organism(skc5,skc7),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[237,36]),
[iquote('0:SpR:237.0,36.0')] ).
cnf(241,plain,
equal(ifeq3(abstraction(skc5,skc7),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[236,31]),
[iquote('0:SpR:236.0,31.0')] ).
cnf(11,axiom,
equal(ifeq3(eventuality(u,v),true__dfg,nonexistent(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(263,plain,
equal(thing(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,258]),
[iquote('0:Rew:2.0,258.0')] ).
cnf(262,plain,
equal(specific(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,257]),
[iquote('0:Rew:2.0,257.0')] ).
cnf(261,plain,
equal(existent(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,256]),
[iquote('0:Rew:2.0,256.0')] ).
cnf(239,plain,
equal(entity(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,233]),
[iquote('0:Rew:2.0,233.0')] ).
cnf(12,axiom,
equal(ifeq3(eventuality(u,v),true__dfg,unisex(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(238,plain,
equal(nonliving(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,232]),
[iquote('0:Rew:2.0,232.0')] ).
cnf(237,plain,
equal(impartial(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,231]),
[iquote('0:Rew:2.0,231.0')] ).
cnf(236,plain,
equal(unisex(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,230]),
[iquote('0:Rew:2.0,230.0')] ).
cnf(223,plain,
equal(object(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,220]),
[iquote('0:Rew:2.0,220.0')] ).
cnf(13,axiom,
equal(ifeq3(order(u,v),true__dfg,event(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(218,plain,
equal(substance_matter(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,215]),
[iquote('0:Rew:2.0,215.0')] ).
cnf(213,plain,
equal(food(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,210]),
[iquote('0:Rew:2.0,210.0')] ).
cnf(209,plain,
equal(beverage(skc5,skc7),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,208]),
[iquote('0:Rew:2.0,208.0')] ).
cnf(14,axiom,
equal(ifeq3(shake_beverage(u,v),true__dfg,beverage(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(15,axiom,
equal(ifeq3(beverage(u,v),true__dfg,food(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(16,axiom,
equal(ifeq3(food(u,v),true__dfg,substance_matter(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(17,axiom,
equal(ifeq3(substance_matter(u,v),true__dfg,object(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(196,plain,
equal(ifeq3(abstraction(skc5,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[195,28]),
[iquote('0:SpR:195.0,28.0')] ).
cnf(193,plain,
equal(ifeq3(entity(skc5,skc8),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[159,19]),
[iquote('0:SpR:159.0,19.0')] ).
cnf(18,axiom,
equal(ifeq3(object(u,v),true__dfg,entity(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(195,plain,
equal(thing(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,194]),
[iquote('0:Rew:2.0,194.0')] ).
cnf(19,axiom,
equal(ifeq3(entity(u,v),true__dfg,thing(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(185,plain,
equal(specific(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,184]),
[iquote('0:Rew:2.0,184.0')] ).
cnf(182,plain,
equal(existent(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,181]),
[iquote('0:Rew:2.0,181.0')] ).
cnf(20,axiom,
equal(ifeq3(entity(u,v),true__dfg,specific(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(21,axiom,
equal(ifeq3(entity(u,v),true__dfg,existent(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(22,axiom,
equal(ifeq3(object(u,v),true__dfg,nonliving(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(176,plain,
equal(ifeq3(object(skc5,skc9),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[119,23]),
[iquote('0:SpR:119.0,23.0')] ).
cnf(163,plain,
equal(ifeq3(object(skc5,skc8),true__dfg,true__dfg,true__dfg),true__dfg),
inference(spr,[status(thm),theory(equality)],[156,24]),
[iquote('0:SpR:156.0,24.0')] ).
cnf(23,axiom,
equal(ifeq3(object(u,v),true__dfg,impartial(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(159,plain,
equal(thing(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,153]),
[iquote('0:Rew:2.0,153.0')] ).
cnf(158,plain,
equal(nonhuman(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,152]),
[iquote('0:Rew:2.0,152.0')] ).
cnf(157,plain,
equal(general(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,151]),
[iquote('0:Rew:2.0,151.0')] ).
cnf(156,plain,
equal(unisex(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,150]),
[iquote('0:Rew:2.0,150.0')] ).
cnf(24,axiom,
equal(ifeq3(object(u,v),true__dfg,unisex(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(148,plain,
equal(abstraction(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,145]),
[iquote('0:Rew:2.0,145.0')] ).
cnf(143,plain,
equal(relation(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,140]),
[iquote('0:Rew:2.0,140.0')] ).
cnf(139,plain,
equal(relname(skc5,skc8),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,138]),
[iquote('0:Rew:2.0,138.0')] ).
cnf(25,axiom,
equal(ifeq3(forename(u,v),true__dfg,relname(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(26,axiom,
equal(ifeq3(relname(u,v),true__dfg,relation(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(27,axiom,
equal(ifeq3(relation(u,v),true__dfg,abstraction(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(28,axiom,
equal(ifeq3(abstraction(u,v),true__dfg,thing(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(29,axiom,
equal(ifeq3(abstraction(u,v),true__dfg,nonhuman(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(30,axiom,
equal(ifeq3(abstraction(u,v),true__dfg,general(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(31,axiom,
equal(ifeq3(abstraction(u,v),true__dfg,unisex(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(120,plain,
equal(entity(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,115]),
[iquote('0:Rew:2.0,115.0')] ).
cnf(119,plain,
equal(impartial(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,114]),
[iquote('0:Rew:2.0,114.0')] ).
cnf(118,plain,
equal(living(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,113]),
[iquote('0:Rew:2.0,113.0')] ).
cnf(100,plain,
equal(organism(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,95]),
[iquote('0:Rew:2.0,95.0')] ).
cnf(32,axiom,
equal(ifeq3(mia_forename(u,v),true__dfg,forename(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(99,plain,
equal(human(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,94]),
[iquote('0:Rew:2.0,94.0')] ).
cnf(98,plain,
equal(animate(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,93]),
[iquote('0:Rew:2.0,93.0')] ).
cnf(92,plain,
equal(human_person(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,91]),
[iquote('0:Rew:2.0,91.0')] ).
cnf(33,axiom,
equal(ifeq3(woman(u,v),true__dfg,human_person(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(34,axiom,
equal(ifeq3(human_person(u,v),true__dfg,organism(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(35,axiom,
equal(ifeq3(organism(u,v),true__dfg,entity(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(36,axiom,
equal(ifeq3(organism(u,v),true__dfg,impartial(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(37,axiom,
equal(ifeq3(organism(u,v),true__dfg,living(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(38,axiom,
equal(ifeq3(human_person(u,v),true__dfg,human(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(39,axiom,
equal(ifeq3(human_person(u,v),true__dfg,animate(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(80,plain,
equal(female(skc5,skc9),true__dfg),
inference(rew,[status(thm),theory(equality)],[2,79]),
[iquote('0:Rew:2.0,79.0')] ).
cnf(40,axiom,
equal(ifeq3(woman(u,v),true__dfg,female(u,v),true__dfg),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(1,axiom,
equal(ifeq4(u,u,v,w),v),
file('NLP042-10.p',unknown),
[] ).
cnf(2,axiom,
equal(ifeq3(u,u,v,w),v),
file('NLP042-10.p',unknown),
[] ).
cnf(3,axiom,
equal(ifeq2(u,u,v,w),v),
file('NLP042-10.p',unknown),
[] ).
cnf(4,axiom,
equal(ifeq(u,u,v,w),v),
file('NLP042-10.p',unknown),
[] ).
cnf(58,axiom,
equal(of(skc5,skc8,skc9),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(59,axiom,
equal(agent(skc5,skc6,skc9),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(60,axiom,
equal(patient(skc5,skc6,skc7),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(50,axiom,
equal(woman(skc5,skc9),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(51,axiom,
equal(shake_beverage(skc5,skc7),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(52,axiom,
equal(order(skc5,skc6),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(53,axiom,
equal(nonreflexive(skc5,skc6),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(54,axiom,
equal(past(skc5,skc6),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(55,axiom,
equal(event(skc5,skc6),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(56,axiom,
equal(forename(skc5,skc8),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(57,axiom,
equal(mia_forename(skc5,skc8),true__dfg),
file('NLP042-10.p',unknown),
[] ).
cnf(61,axiom,
~ equal(b,a),
file('NLP042-10.p',unknown),
[] ).
cnf(49,axiom,
equal(actual_world(skc5),true__dfg),
file('NLP042-10.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NLP042-10 : TPTP v8.1.0. Released v7.3.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Fri Jul 1 01:03:37 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.19/0.46
% 0.19/0.46 SPASS V 3.9
% 0.19/0.46 SPASS beiseite: Completion found.
% 0.19/0.46 % SZS status CounterSatisfiable
% 0.19/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 SPASS derived 303 clauses, backtracked 0 clauses, performed 0 splits and kept 142 clauses.
% 0.19/0.46 SPASS allocated 63565 KBytes.
% 0.19/0.46 SPASS spent 0:00:00.12 on the problem.
% 0.19/0.46 0:00:00.04 for the input.
% 0.19/0.46 0:00:00.00 for the FLOTTER CNF translation.
% 0.19/0.46 0:00:00.01 for inferences.
% 0.19/0.46 0:00:00.00 for the backtracking.
% 0.19/0.46 0:00:00.04 for the reduction.
% 0.19/0.46
% 0.19/0.46
% 0.19/0.46 The saturated set of worked-off clauses is :
% 0.19/0.46 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------