%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR082+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:13:31 PM UTC 2026
% Result : Theorem 56.43s 8.08s
% Output : CNFRefutation 57.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 98
% Syntax : Number of formulae : 360 ( 97 unt; 61 def)
% Number of atoms : 896 ( 43 equ)
% Maximal formula atoms : 22 ( 2 avg)
% Number of connectives : 912 ( 376 ~; 399 |; 53 &)
% ( 63 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 62 prp; 0-3 aty)
% Number of functors : 35 ( 34 usr; 29 con; 0-3 aty)
% Number of variables : 231 ( 220 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [V__X,V__Y] :
( s__subclass(V__X,V__Y)
=> ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [V__X,V__Y,V__Z] :
( ( s__instance(V__X,s__SetOrClass)
& s__instance(V__Y,s__SetOrClass) )
=> ( ( s__instance(V__Z,V__X)
& s__subclass(V__X,V__Y) )
=> s__instance(V__Z,V__Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [V__CLASS1,V__CLASS2] :
( ( s__instance(V__CLASS1,s__SetOrClass)
& s__instance(V__CLASS2,s__SetOrClass) )
=> ( s__immediateSubclass(V__CLASS1,V__CLASS2)
=> ~ ? [V__CLASS3] :
( V__CLASS1 != V__CLASS3
& V__CLASS2 != V__CLASS3
& s__subclass(V__CLASS1,V__CLASS3)
& s__subclass(V__CLASS3,V__CLASS2)
& s__instance(V__CLASS3,s__SetOrClass) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [V__ROW1,V__ROW2] :
( ( s__instance(V__ROW1,s__SetOrClass)
& s__instance(V__ROW2,s__SetOrClass) )
=> ( s__immediateSubclass(V__ROW1,V__ROW2)
=> s__subclass(V__ROW1,V__ROW2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,axiom,
! [V__ROW1,V__ROW2] :
( ( s__instance(V__ROW1,s__Human)
& s__instance(V__ROW2,s__Human) )
=> ( s__domesticPartner(V__ROW1,V__ROW2)
=> s__cohabitant(V__ROW1,V__ROW2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,axiom,
! [V__ROW1,V__ROW2] :
( ( s__instance(V__ROW1,s__Human)
& s__instance(V__ROW2,s__Human) )
=> ( s__cohabitant(V__ROW1,V__ROW2)
=> s__mutualAcquaintance(V__ROW1,V__ROW2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [V__ROW1,V__ROW2] :
( ( s__instance(V__ROW1,s__Human)
& s__instance(V__ROW2,s__Human) )
=> ( s__mutualAcquaintance(V__ROW1,V__ROW2)
=> s__acquaintance(V__ROW1,V__ROW2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f826,axiom,
s__subclass(s__Agent,s__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f829,axiom,
s__subclass(s__SentientAgent,s__Agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f831,axiom,
s__subclass(s__CognitiveAgent,s__SentientAgent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f834,axiom,
s__subclass(s__LegalAgent,s__Agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1106,axiom,
! [V__INST] : s__relatedInternalConcept(V__INST,V__INST),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2742,axiom,
! [V__ROW1,V__ROW2] :
( V__ROW1 = V__ROW2
=> s__ListLengthFn(s__ListFn_2(V__ROW1,V__ROW2)) = "2" ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2958,axiom,
! [V__ROW1,V__ROW2] :
( s__relatedInternalConcept(V__ROW1,V__ROW2)
=> s__ListLengthFn(s__ListFn_2(V__ROW1,V__ROW2)) = "2" ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4670,axiom,
! [V__C2,V__U,V__C1] :
( V__U = s__UnionFn(V__C1,V__C2)
<=> ! [V__I1,V__I2,V__I3] :
( ( s__instance(V__C2,s__SetOrClass)
& s__instance(V__U,s__SetOrClass)
& s__instance(V__C1,s__SetOrClass) )
=> ( ( s__instance(V__I3,V__U)
& s__instance(V__I2,V__C2)
& s__instance(V__I1,V__C1) )
=> ( ( s__instance(V__I3,V__C2)
| s__instance(V__I3,V__C1) )
& s__instance(V__I2,V__U)
& s__instance(V__I1,V__U) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6100,axiom,
s__subclass(s__IntentionalProcess,s__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6104,axiom,
s__subclass(s__IntentionalPsychologicalProcess,s__IntentionalProcess),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6105,axiom,
s__subclass(s__IntentionalPsychologicalProcess,s__PsychologicalProcess),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6168,axiom,
s__subclass(s__Planning,s__IntentionalPsychologicalProcess),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6211,axiom,
s__subclass(s__Motion,s__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6469,axiom,
s__subclass(s__Reasoning,s__IntentionalPsychologicalProcess),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6472,axiom,
! [V__AGENT] :
( s__instance(V__AGENT,s__Object)
=> ( s__instance(V__AGENT,s__CognitiveAgent)
=> s__capability(s__Reasoning,s__agent__m,V__AGENT) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6596,axiom,
s__subclass(s__InternalChange,s__Process),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6820,axiom,
s__subclass(s__Perception,s__PsychologicalProcess),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6823,axiom,
! [V__AGENT] :
( s__instance(V__AGENT,s__Object)
=> ( s__instance(V__AGENT,s__SentientAgent)
=> s__capability(s__Perception,s__experiencer__m,V__AGENT) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6824,axiom,
s__subclass(s__Seeing,s__Perception),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6942,axiom,
s__subclass(s__AstronomicalBody,s__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7056,axiom,
s__subclass(s__Organism,s__Agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7100,axiom,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7207,axiom,
s__subclass(s__Human,s__CognitiveAgent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7215,axiom,
s__subclass(s__Woman,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8429,axiom,
s__subclass(s__HumanAdult,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8434,axiom,
s__subclass(s__HumanYouth,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9744,axiom,
s__subclass(s__TwoDimensionalObject,s__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13615,axiom,
s__subclass(s__DomesticAnimal,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16749,axiom,
s__instance(s__Jane8_1,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16750,conjecture,
? [V_ROLE1,V_ROLE2] :
( s__capability(s__Perception,V_ROLE2,s__Jane8_1)
& s__capability(s__Reasoning,V_ROLE1,s__Jane8_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16751,negated_conjecture,
~ ? [V_ROLE1,V_ROLE2] :
( s__capability(s__Perception,V_ROLE2,s__Jane8_1)
& s__capability(s__Reasoning,V_ROLE1,s__Jane8_1) ),
inference(negated_conjecture,[status(cth)],[f16750]) ).
fof(f16791,plain,
! [V__X,V__Y] :
( ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) )
| ~ s__subclass(V__X,V__Y) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f16792,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16791]) ).
fof(f16793,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16791]) ).
fof(f16794,plain,
! [V__X,V__Y,V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y)
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f16795,plain,
! [V__X,V__Y] :
( ! [V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y) )
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(miniscoping,[status(thm)],[f16794]) ).
fof(f16796,plain,
! [X0,X1,X2] :
( s__instance(X2,X0)
| ~ s__instance(X2,X1)
| ~ s__subclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f16795]) ).
fof(f16802,plain,
! [V__CLASS1,V__CLASS2] :
( ! [V__CLASS3] :
( V__CLASS1 = V__CLASS3
| V__CLASS2 = V__CLASS3
| ~ s__subclass(V__CLASS1,V__CLASS3)
| ~ s__subclass(V__CLASS3,V__CLASS2)
| ~ s__instance(V__CLASS3,s__SetOrClass) )
| ~ s__immediateSubclass(V__CLASS1,V__CLASS2)
| ~ s__instance(V__CLASS1,s__SetOrClass)
| ~ s__instance(V__CLASS2,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f16803,plain,
! [X0,X1,X2] :
( X1 = X2
| X0 = X2
| ~ s__subclass(X1,X2)
| ~ s__subclass(X2,X0)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__immediateSubclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f16802]) ).
fof(f16847,plain,
! [V__ROW1,V__ROW2] :
( s__subclass(V__ROW1,V__ROW2)
| ~ s__immediateSubclass(V__ROW1,V__ROW2)
| ~ s__instance(V__ROW1,s__SetOrClass)
| ~ s__instance(V__ROW2,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f16848,plain,
! [X0,X1] :
( s__subclass(X1,X0)
| ~ s__immediateSubclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f16847]) ).
fof(f17031,plain,
! [V__ROW1,V__ROW2] :
( s__cohabitant(V__ROW1,V__ROW2)
| ~ s__domesticPartner(V__ROW1,V__ROW2)
| ~ s__instance(V__ROW1,s__Human)
| ~ s__instance(V__ROW2,s__Human) ),
inference(pre_NNF_transformation,[status(thm)],[f146]) ).
fof(f17032,plain,
! [X0,X1] :
( s__cohabitant(X1,X0)
| ~ s__domesticPartner(X1,X0)
| ~ s__instance(X1,s__Human)
| ~ s__instance(X0,s__Human) ),
inference(cnf_transformation,[status(thm)],[f17031]) ).
fof(f17047,plain,
! [V__ROW1,V__ROW2] :
( s__mutualAcquaintance(V__ROW1,V__ROW2)
| ~ s__cohabitant(V__ROW1,V__ROW2)
| ~ s__instance(V__ROW1,s__Human)
| ~ s__instance(V__ROW2,s__Human) ),
inference(pre_NNF_transformation,[status(thm)],[f154]) ).
fof(f17048,plain,
! [X0,X1] :
( s__mutualAcquaintance(X1,X0)
| ~ s__cohabitant(X1,X0)
| ~ s__instance(X1,s__Human)
| ~ s__instance(X0,s__Human) ),
inference(cnf_transformation,[status(thm)],[f17047]) ).
fof(f17078,plain,
! [V__ROW1,V__ROW2] :
( s__acquaintance(V__ROW1,V__ROW2)
| ~ s__mutualAcquaintance(V__ROW1,V__ROW2)
| ~ s__instance(V__ROW1,s__Human)
| ~ s__instance(V__ROW2,s__Human) ),
inference(pre_NNF_transformation,[status(thm)],[f169]) ).
fof(f17079,plain,
! [X0,X1] :
( s__acquaintance(X1,X0)
| ~ s__mutualAcquaintance(X1,X0)
| ~ s__instance(X1,s__Human)
| ~ s__instance(X0,s__Human) ),
inference(cnf_transformation,[status(thm)],[f17078]) ).
fof(f18382,plain,
s__subclass(s__Agent,s__Object),
inference(cnf_transformation,[status(thm)],[f826]) ).
fof(f18390,plain,
s__subclass(s__SentientAgent,s__Agent),
inference(cnf_transformation,[status(thm)],[f829]) ).
fof(f18392,plain,
s__subclass(s__CognitiveAgent,s__SentientAgent),
inference(cnf_transformation,[status(thm)],[f831]) ).
fof(f18395,plain,
s__subclass(s__LegalAgent,s__Agent),
inference(cnf_transformation,[status(thm)],[f834]) ).
fof(f18870,plain,
! [X0] : s__relatedInternalConcept(X0,X0),
inference(cnf_transformation,[status(thm)],[f1106]) ).
fof(f22083,plain,
! [V__ROW1,V__ROW2] :
( s__ListLengthFn(s__ListFn_2(V__ROW1,V__ROW2)) = "2"
| V__ROW1 != V__ROW2 ),
inference(pre_NNF_transformation,[status(thm)],[f2742]) ).
fof(f22084,plain,
! [X0,X1] :
( s__ListLengthFn(s__ListFn_2(X0,X1)) = "2"
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f22083]) ).
fof(f22530,plain,
! [V__ROW1,V__ROW2] :
( s__ListLengthFn(s__ListFn_2(V__ROW1,V__ROW2)) = "2"
| ~ s__relatedInternalConcept(V__ROW1,V__ROW2) ),
inference(pre_NNF_transformation,[status(thm)],[f2958]) ).
fof(f22531,plain,
! [X0,X1] :
( s__ListLengthFn(s__ListFn_2(X0,X1)) = "2"
| ~ s__relatedInternalConcept(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22530]) ).
fof(f25553,plain,
! [V__C2,V__U,V__C1] :
( V__U = s__UnionFn(V__C1,V__C2)
<=> ! [V__I1,V__I2,V__I3] :
( ( ( s__instance(V__I3,V__C2)
| s__instance(V__I3,V__C1) )
& s__instance(V__I2,V__U)
& s__instance(V__I1,V__U) )
| ~ s__instance(V__I3,V__U)
| ~ s__instance(V__I2,V__C2)
| ~ s__instance(V__I1,V__C1)
| ~ s__instance(V__C2,s__SetOrClass)
| ~ s__instance(V__U,s__SetOrClass)
| ~ s__instance(V__C1,s__SetOrClass) ) ),
inference(pre_NNF_transformation,[status(thm)],[f4670]) ).
fof(f25554,plain,
! [V__C2,V__U,V__C1] :
( ( ? [V__I1,V__I2,V__I3] :
( ( ( ~ s__instance(V__I3,V__C2)
& ~ s__instance(V__I3,V__C1) )
| ~ s__instance(V__I2,V__U)
| ~ s__instance(V__I1,V__U) )
& s__instance(V__I3,V__U)
& s__instance(V__I2,V__C2)
& s__instance(V__I1,V__C1)
& s__instance(V__C2,s__SetOrClass)
& s__instance(V__U,s__SetOrClass)
& s__instance(V__C1,s__SetOrClass) )
| V__U = s__UnionFn(V__C1,V__C2) )
& ( ! [V__I1,V__I2,V__I3] :
( ( ( s__instance(V__I3,V__C2)
| s__instance(V__I3,V__C1) )
& s__instance(V__I2,V__U)
& s__instance(V__I1,V__U) )
| ~ s__instance(V__I3,V__U)
| ~ s__instance(V__I2,V__C2)
| ~ s__instance(V__I1,V__C1)
| ~ s__instance(V__C2,s__SetOrClass)
| ~ s__instance(V__U,s__SetOrClass)
| ~ s__instance(V__C1,s__SetOrClass) )
| V__U != s__UnionFn(V__C1,V__C2) ) ),
inference(NNF_transformation,[status(thm)],[f25553]) ).
fof(f25555,plain,
( ! [V__C2,V__U,V__C1] :
( ( ? [V__I1,V__I2,V__I3] :
( ( ( ~ s__instance(V__I3,V__C2)
& ~ s__instance(V__I3,V__C1) )
| ~ s__instance(V__I2,V__U)
| ~ s__instance(V__I1,V__U) )
& s__instance(V__I3,V__U)
& s__instance(V__I2,V__C2)
& s__instance(V__I1,V__C1) )
& s__instance(V__C2,s__SetOrClass)
& s__instance(V__U,s__SetOrClass)
& s__instance(V__C1,s__SetOrClass) )
| V__U = s__UnionFn(V__C1,V__C2) )
& ! [V__C2,V__U,V__C1] :
( ! [V__I1,V__I2,V__I3] :
( ( ( s__instance(V__I3,V__C2)
| s__instance(V__I3,V__C1) )
& s__instance(V__I2,V__U)
& s__instance(V__I1,V__U) )
| ~ s__instance(V__I3,V__U)
| ~ s__instance(V__I2,V__C2)
| ~ s__instance(V__I1,V__C1) )
| ~ s__instance(V__C2,s__SetOrClass)
| ~ s__instance(V__U,s__SetOrClass)
| ~ s__instance(V__C1,s__SetOrClass)
| V__U != s__UnionFn(V__C1,V__C2) ) ),
inference(miniscoping,[status(thm)],[f25554]) ).
fof(f25556,plain,
( ! [V__C2,V__U,V__C1] :
( ( ( ( ~ s__instance(sK189_skl(V__C1,V__U,V__C2),V__C2)
& ~ s__instance(sK189_skl(V__C1,V__U,V__C2),V__C1) )
| ~ s__instance(sK188_skl(V__C1,V__U,V__C2),V__U)
| ~ s__instance(sK187_skl(V__C1,V__U,V__C2),V__U) )
& s__instance(sK189_skl(V__C1,V__U,V__C2),V__U)
& s__instance(sK188_skl(V__C1,V__U,V__C2),V__C2)
& s__instance(sK187_skl(V__C1,V__U,V__C2),V__C1)
& s__instance(V__C2,s__SetOrClass)
& s__instance(V__U,s__SetOrClass)
& s__instance(V__C1,s__SetOrClass) )
| V__U = s__UnionFn(V__C1,V__C2) )
& ! [V__C2,V__U,V__C1] :
( ! [V__I1,V__I2,V__I3] :
( ( ( s__instance(V__I3,V__C2)
| s__instance(V__I3,V__C1) )
& s__instance(V__I2,V__U)
& s__instance(V__I1,V__U) )
| ~ s__instance(V__I3,V__U)
| ~ s__instance(V__I2,V__C2)
| ~ s__instance(V__I1,V__C1) )
| ~ s__instance(V__C2,s__SetOrClass)
| ~ s__instance(V__U,s__SetOrClass)
| ~ s__instance(V__C1,s__SetOrClass)
| V__U != s__UnionFn(V__C1,V__C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK187_skl,sK188_skl,sK189_skl]),skolemize(V__I1,sK187_skl(V__C1,V__U,V__C2)),skolemize(V__I2,sK188_skl(V__C1,V__U,V__C2)),skolemize(V__I3,sK189_skl(V__C1,V__U,V__C2))],[f25555]) ).
fof(f25560,plain,
! [X0,X1,X2] :
( s__instance(X1,s__SetOrClass)
| X0 = s__UnionFn(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f25556]) ).
fof(f27731,plain,
s__subclass(s__IntentionalProcess,s__Process),
inference(cnf_transformation,[status(thm)],[f6100]) ).
fof(f27742,plain,
s__subclass(s__IntentionalPsychologicalProcess,s__IntentionalProcess),
inference(cnf_transformation,[status(thm)],[f6104]) ).
fof(f27743,plain,
s__subclass(s__IntentionalPsychologicalProcess,s__PsychologicalProcess),
inference(cnf_transformation,[status(thm)],[f6105]) ).
fof(f27831,plain,
s__subclass(s__Planning,s__IntentionalPsychologicalProcess),
inference(cnf_transformation,[status(thm)],[f6168]) ).
fof(f27912,plain,
s__subclass(s__Motion,s__Process),
inference(cnf_transformation,[status(thm)],[f6211]) ).
fof(f28353,plain,
s__subclass(s__Reasoning,s__IntentionalPsychologicalProcess),
inference(cnf_transformation,[status(thm)],[f6469]) ).
fof(f28356,plain,
! [V__AGENT] :
( s__capability(s__Reasoning,s__agent__m,V__AGENT)
| ~ s__instance(V__AGENT,s__CognitiveAgent)
| ~ s__instance(V__AGENT,s__Object) ),
inference(pre_NNF_transformation,[status(thm)],[f6472]) ).
fof(f28357,plain,
! [X0] :
( s__capability(s__Reasoning,s__agent__m,X0)
| ~ s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[status(thm)],[f28356]) ).
fof(f28581,plain,
s__subclass(s__InternalChange,s__Process),
inference(cnf_transformation,[status(thm)],[f6596]) ).
fof(f28981,plain,
s__subclass(s__Perception,s__PsychologicalProcess),
inference(cnf_transformation,[status(thm)],[f6820]) ).
fof(f28985,plain,
! [V__AGENT] :
( s__capability(s__Perception,s__experiencer__m,V__AGENT)
| ~ s__instance(V__AGENT,s__SentientAgent)
| ~ s__instance(V__AGENT,s__Object) ),
inference(pre_NNF_transformation,[status(thm)],[f6823]) ).
fof(f28986,plain,
! [X0] :
( s__capability(s__Perception,s__experiencer__m,X0)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__Object) ),
inference(cnf_transformation,[status(thm)],[f28985]) ).
fof(f28987,plain,
s__subclass(s__Seeing,s__Perception),
inference(cnf_transformation,[status(thm)],[f6824]) ).
fof(f29167,plain,
s__subclass(s__AstronomicalBody,s__Object),
inference(cnf_transformation,[status(thm)],[f6942]) ).
fof(f29321,plain,
s__subclass(s__Organism,s__Agent),
inference(cnf_transformation,[status(thm)],[f7056]) ).
fof(f29374,plain,
s__subclass(s__Animal,s__Organism),
inference(cnf_transformation,[status(thm)],[f7100]) ).
fof(f29498,plain,
s__subclass(s__Human,s__CognitiveAgent),
inference(cnf_transformation,[status(thm)],[f7207]) ).
fof(f29507,plain,
s__subclass(s__Woman,s__Human),
inference(cnf_transformation,[status(thm)],[f7215]) ).
fof(f31241,plain,
s__subclass(s__HumanAdult,s__Human),
inference(cnf_transformation,[status(thm)],[f8429]) ).
fof(f31248,plain,
s__subclass(s__HumanYouth,s__Human),
inference(cnf_transformation,[status(thm)],[f8434]) ).
fof(f33318,plain,
s__subclass(s__TwoDimensionalObject,s__Object),
inference(cnf_transformation,[status(thm)],[f9744]) ).
fof(f39790,plain,
s__subclass(s__DomesticAnimal,s__Animal),
inference(cnf_transformation,[status(thm)],[f13615]) ).
fof(f44204,plain,
s__instance(s__Jane8_1,s__Human),
inference(cnf_transformation,[status(thm)],[f16749]) ).
fof(f44205,plain,
! [V_ROLE1,V_ROLE2] :
( ~ s__capability(s__Perception,V_ROLE2,s__Jane8_1)
| ~ s__capability(s__Reasoning,V_ROLE1,s__Jane8_1) ),
inference(pre_NNF_transformation,[status(thm)],[f16751]) ).
fof(f44206,plain,
( ! [V_ROLE2] : ~ s__capability(s__Perception,V_ROLE2,s__Jane8_1)
| ! [V_ROLE1] : ~ s__capability(s__Reasoning,V_ROLE1,s__Jane8_1) ),
inference(miniscoping,[status(thm)],[f44205]) ).
fof(f44207,plain,
! [X0,X1] :
( ~ s__capability(s__Perception,X1,s__Jane8_1)
| ~ s__capability(s__Reasoning,X0,s__Jane8_1) ),
inference(cnf_transformation,[status(thm)],[f44206]) ).
fof(f45049,definition,
! [X1] :
( sQ188_spl
<=> ~ s__instance(X1,s__Human) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f45050,plain,
! [X0] :
( ~ sQ188_spl
| ~ s__instance(X0,s__Human) ),
inference(component_clause,[status(thm)],[f45049]) ).
fof(f45233,definition,
! [X0] :
( sQ240_spl
<=> ~ s__capability(s__Reasoning,X0,s__Jane8_1) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f45234,plain,
! [X0] :
( ~ sQ240_spl
| ~ s__capability(s__Reasoning,X0,s__Jane8_1) ),
inference(component_clause,[status(thm)],[f45233]) ).
fof(f45236,definition,
! [X1] :
( sQ241_spl
<=> ~ s__capability(s__Perception,X1,s__Jane8_1) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f45237,plain,
! [X0] :
( ~ sQ241_spl
| ~ s__capability(s__Perception,X0,s__Jane8_1) ),
inference(component_clause,[status(thm)],[f45236]) ).
fof(f45239,plain,
( sQ241_spl
| sQ240_spl ),
inference(split_clause,[status(thm)],[f44207,f45233,f45236]) ).
fof(f45328,plain,
! [X0] : s__ListLengthFn(s__ListFn_2(X0,X0)) = "2",
inference(destructive_equality_resolution,[status(thm)],[f22084]) ).
fof(f45605,plain,
( ~ sQ240_spl
| ~ s__instance(s__Jane8_1,s__CognitiveAgent)
| ~ s__instance(s__Jane8_1,s__Object) ),
inference(resolution,[status(thm)],[f28357,f45234]) ).
fof(f45606,definition,
( sQ242_spl
<=> s__instance(s__Jane8_1,s__Object) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f45608,plain,
( sQ242_spl
| ~ s__instance(s__Jane8_1,s__Object) ),
inference(component_clause,[status(thm)],[f45606]) ).
fof(f45609,definition,
( sQ243_spl
<=> s__instance(s__Jane8_1,s__CognitiveAgent) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f45610,plain,
( ~ sQ243_spl
| s__instance(s__Jane8_1,s__CognitiveAgent) ),
inference(component_clause,[status(thm)],[f45609]) ).
fof(f45611,plain,
( sQ243_spl
| ~ s__instance(s__Jane8_1,s__CognitiveAgent) ),
inference(component_clause,[status(thm)],[f45609]) ).
fof(f45612,plain,
( ~ sQ240_spl
| ~ sQ243_spl
| ~ sQ242_spl ),
inference(split_clause,[status(thm)],[f45605,f45606,f45609,f45233]) ).
fof(f45615,plain,
( ~ sQ241_spl
| ~ s__instance(s__Jane8_1,s__SentientAgent)
| ~ s__instance(s__Jane8_1,s__Object) ),
inference(resolution,[status(thm)],[f28986,f45237]) ).
fof(f45616,definition,
( sQ244_spl
<=> s__instance(s__Jane8_1,s__SentientAgent) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f45618,plain,
( sQ244_spl
| ~ s__instance(s__Jane8_1,s__SentientAgent) ),
inference(component_clause,[status(thm)],[f45616]) ).
fof(f45619,plain,
( ~ sQ241_spl
| ~ sQ244_spl
| ~ sQ242_spl ),
inference(split_clause,[status(thm)],[f45615,f45606,f45616,f45236]) ).
fof(f45622,plain,
( ~ sQ188_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f44204,f45050]) ).
fof(f45623,plain,
~ sQ188_spl,
inference(contradiction_clause,[status(thm)],[f45622]) ).
fof(f45643,definition,
( sQ245_spl
<=> s__instance(s__IntentionalPsychologicalProcess,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f45645,plain,
( sQ245_spl
| ~ s__instance(s__IntentionalPsychologicalProcess,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45643]) ).
fof(f45659,definition,
( sQ250_spl
<=> s__instance(s__Planning,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f45661,plain,
( sQ250_spl
| ~ s__instance(s__Planning,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45659]) ).
fof(f45666,definition,
( sQ252_spl
<=> s__instance(s__PsychologicalProcess,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f45668,plain,
( sQ252_spl
| ~ s__instance(s__PsychologicalProcess,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45666]) ).
fof(f45676,definition,
( sQ255_spl
<=> s__instance(s__IntentionalProcess,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f45678,plain,
( sQ255_spl
| ~ s__instance(s__IntentionalProcess,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45676]) ).
fof(f45686,definition,
( sQ258_spl
<=> s__instance(s__Process,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f45688,plain,
( sQ258_spl
| ~ s__instance(s__Process,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45686]) ).
fof(f45726,definition,
( sQ270_spl
<=> s__instance(s__Agent,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f45728,plain,
( sQ270_spl
| ~ s__instance(s__Agent,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45726]) ).
fof(f45732,definition,
( sQ272_spl
<=> s__instance(s__LegalAgent,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f45734,plain,
( sQ272_spl
| ~ s__instance(s__LegalAgent,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45732]) ).
fof(f45739,definition,
( sQ274_spl
<=> s__instance(s__SentientAgent,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f45741,plain,
( sQ274_spl
| ~ s__instance(s__SentientAgent,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45739]) ).
fof(f45745,definition,
( sQ276_spl
<=> s__instance(s__CognitiveAgent,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition]) ).
fof(f45747,plain,
( sQ276_spl
| ~ s__instance(s__CognitiveAgent,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45745]) ).
fof(f45759,definition,
( sQ280_spl
<=> s__instance(s__Object,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f45761,plain,
( sQ280_spl
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45759]) ).
fof(f45809,definition,
( sQ295_spl
<=> s__instance(s__Perception,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition]) ).
fof(f45811,plain,
( sQ295_spl
| ~ s__instance(s__Perception,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45809]) ).
fof(f45815,definition,
( sQ297_spl
<=> s__instance(s__Seeing,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f45817,plain,
( sQ297_spl
| ~ s__instance(s__Seeing,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45815]) ).
fof(f45832,definition,
( sQ302_spl
<=> s__instance(s__Reasoning,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f45834,plain,
( sQ302_spl
| ~ s__instance(s__Reasoning,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45832]) ).
fof(f45854,definition,
( sQ308_spl
<=> s__instance(s__Motion,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f45856,plain,
( sQ308_spl
| ~ s__instance(s__Motion,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f45854]) ).
fof(f46008,definition,
( sQ350_spl
<=> s__instance(s__Organism,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition]) ).
fof(f46010,plain,
( sQ350_spl
| ~ s__instance(s__Organism,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46008]) ).
fof(f46019,definition,
( sQ353_spl
<=> s__instance(s__Animal,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition]) ).
fof(f46021,plain,
( sQ353_spl
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46019]) ).
fof(f46052,definition,
( sQ362_spl
<=> s__instance(s__Human,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f46054,plain,
( sQ362_spl
| ~ s__instance(s__Human,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46052]) ).
fof(f46074,definition,
( sQ368_spl
<=> s__instance(s__Woman,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ368_spl])],[split_symbol_definition]) ).
fof(f46076,plain,
( sQ368_spl
| ~ s__instance(s__Woman,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46074]) ).
fof(f46077,definition,
( sQ369_spl
<=> s__Woman = s__Human ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f46078,plain,
( ~ sQ369_spl
| s__Woman = s__Human ),
inference(component_clause,[status(thm)],[f46077]) ).
fof(f46079,plain,
( sQ369_spl
| s__Woman != s__Human ),
inference(component_clause,[status(thm)],[f46077]) ).
fof(f46129,definition,
( sQ383_spl
<=> s__instance(s__HumanAdult,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f46131,plain,
( sQ383_spl
| ~ s__instance(s__HumanAdult,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46129]) ).
fof(f46140,definition,
( sQ386_spl
<=> s__instance(s__HumanYouth,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition]) ).
fof(f46142,plain,
( sQ386_spl
| ~ s__instance(s__HumanYouth,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46140]) ).
fof(f46162,definition,
( sQ392_spl
<=> s__instance(s__TwoDimensionalObject,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f46164,plain,
( sQ392_spl
| ~ s__instance(s__TwoDimensionalObject,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46162]) ).
fof(f46274,definition,
( sQ422_spl
<=> s__instance(s__DomesticAnimal,s__SetOrClass) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f46276,plain,
( sQ422_spl
| ~ s__instance(s__DomesticAnimal,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f46274]) ).
fof(f46354,plain,
s__instance(s__Human,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f29498]) ).
fof(f46357,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f29374]) ).
fof(f46358,plain,
s__instance(s__Organism,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f29321]) ).
fof(f46376,plain,
s__instance(s__IntentionalPsychologicalProcess,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f27743]) ).
fof(f46378,plain,
s__instance(s__IntentionalProcess,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f27731]) ).
fof(f46383,plain,
s__instance(s__CognitiveAgent,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f18392]) ).
fof(f46384,plain,
s__instance(s__SentientAgent,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f18390]) ).
fof(f46385,plain,
s__instance(s__Agent,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f18382]) ).
fof(f46390,plain,
s__instance(s__Seeing,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f28987]) ).
fof(f46391,plain,
s__instance(s__Perception,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f28981]) ).
fof(f46392,plain,
s__instance(s__Reasoning,s__SetOrClass),
inference(resolution,[status(thm)],[f16792,f28353]) ).
fof(f46393,plain,
( sQ362_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46354,f46054]) ).
fof(f46394,plain,
sQ362_spl,
inference(contradiction_clause,[status(thm)],[f46393]) ).
fof(f46395,plain,
( sQ353_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46357,f46021]) ).
fof(f46396,plain,
sQ353_spl,
inference(contradiction_clause,[status(thm)],[f46395]) ).
fof(f46397,plain,
( sQ350_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46358,f46010]) ).
fof(f46398,plain,
sQ350_spl,
inference(contradiction_clause,[status(thm)],[f46397]) ).
fof(f46399,plain,
( sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46376,f45645]) ).
fof(f46400,plain,
sQ245_spl,
inference(contradiction_clause,[status(thm)],[f46399]) ).
fof(f46401,plain,
( sQ255_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46378,f45678]) ).
fof(f46402,plain,
sQ255_spl,
inference(contradiction_clause,[status(thm)],[f46401]) ).
fof(f46403,plain,
( sQ276_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46383,f45747]) ).
fof(f46404,plain,
sQ276_spl,
inference(contradiction_clause,[status(thm)],[f46403]) ).
fof(f46405,plain,
( sQ274_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46384,f45741]) ).
fof(f46406,plain,
sQ274_spl,
inference(contradiction_clause,[status(thm)],[f46405]) ).
fof(f46407,plain,
( sQ270_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46385,f45728]) ).
fof(f46408,plain,
sQ270_spl,
inference(contradiction_clause,[status(thm)],[f46407]) ).
fof(f46409,plain,
( sQ297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46390,f45817]) ).
fof(f46410,plain,
sQ297_spl,
inference(contradiction_clause,[status(thm)],[f46409]) ).
fof(f46411,plain,
( sQ295_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46391,f45811]) ).
fof(f46412,plain,
sQ295_spl,
inference(contradiction_clause,[status(thm)],[f46411]) ).
fof(f46479,plain,
( ~ sQ369_spl
| s__instance(s__Jane8_1,s__Woman) ),
inference(backward_demodulation,[status(thm)],[f46078,f44204]) ).
fof(f46496,plain,
s__instance(s__PsychologicalProcess,s__SetOrClass),
inference(resolution,[status(thm)],[f16793,f28981]) ).
fof(f46499,plain,
s__instance(s__Object,s__SetOrClass),
inference(resolution,[status(thm)],[f16793,f29167]) ).
fof(f46501,plain,
s__instance(s__Process,s__SetOrClass),
inference(resolution,[status(thm)],[f16793,f28581]) ).
fof(f46527,plain,
( sQ252_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46496,f45668]) ).
fof(f46528,plain,
sQ252_spl,
inference(contradiction_clause,[status(thm)],[f46527]) ).
fof(f46529,plain,
( sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46499,f45761]) ).
fof(f46530,plain,
sQ280_spl,
inference(contradiction_clause,[status(thm)],[f46529]) ).
fof(f46531,plain,
( sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46501,f45688]) ).
fof(f46532,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f46531]) ).
fof(f46534,definition,
( sQ436_spl
<=> s__instance(s__Jane8_1,s__Woman) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f46535,plain,
( ~ sQ436_spl
| s__instance(s__Jane8_1,s__Woman) ),
inference(component_clause,[status(thm)],[f46534]) ).
fof(f46536,plain,
( sQ436_spl
| ~ s__instance(s__Jane8_1,s__Woman) ),
inference(component_clause,[status(thm)],[f46534]) ).
fof(f46545,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[status(thm)],[f16796,f16793]) ).
fof(f46546,plain,
! [X0] :
( s__instance(X0,s__PsychologicalProcess)
| ~ s__instance(X0,s__Perception)
| ~ s__instance(s__Perception,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f28981]) ).
fof(f46547,plain,
! [X0] :
( s__instance(X0,s__Perception)
| ~ s__instance(X0,s__Seeing)
| ~ s__instance(s__Seeing,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f28987]) ).
fof(f46548,plain,
! [X0] :
( s__instance(X0,s__IntentionalPsychologicalProcess)
| ~ s__instance(X0,s__Reasoning)
| ~ s__instance(s__Reasoning,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f28353]) ).
fof(f46555,plain,
! [X0] :
( s__instance(X0,s__Process)
| ~ s__instance(X0,s__Motion)
| ~ s__instance(s__Motion,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f27912]) ).
fof(f46558,plain,
! [X0] :
( s__instance(X0,s__IntentionalPsychologicalProcess)
| ~ s__instance(X0,s__Planning)
| ~ s__instance(s__Planning,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f27831]) ).
fof(f46559,plain,
! [X0] :
( s__instance(X0,s__PsychologicalProcess)
| ~ s__instance(X0,s__IntentionalPsychologicalProcess)
| ~ s__instance(s__IntentionalPsychologicalProcess,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f27743]) ).
fof(f46560,plain,
! [X0] :
( s__instance(X0,s__IntentionalProcess)
| ~ s__instance(X0,s__IntentionalPsychologicalProcess)
| ~ s__instance(s__IntentionalPsychologicalProcess,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f27742]) ).
fof(f46561,plain,
! [X0] :
( s__instance(X0,s__Process)
| ~ s__instance(X0,s__IntentionalProcess)
| ~ s__instance(s__IntentionalProcess,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f27731]) ).
fof(f46565,plain,
! [X0] :
( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__LegalAgent)
| ~ s__instance(s__LegalAgent,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f18395]) ).
fof(f46566,plain,
! [X0] :
( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__SentientAgent)
| ~ s__instance(s__SentientAgent,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f18390]) ).
fof(f46567,plain,
! [X0] :
( s__instance(X0,s__Object)
| ~ s__instance(X0,s__Agent)
| ~ s__instance(s__Agent,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46545,f18382]) ).
fof(f46572,definition,
! [X0] :
( sQ437_spl
<=> ( s__instance(X0,s__PsychologicalProcess)
| ~ s__instance(X0,s__Perception) ) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f46575,plain,
( sQ437_spl
| ~ sQ295_spl ),
inference(split_clause,[status(thm)],[f46546,f45809,f46572]) ).
fof(f46576,definition,
! [X0] :
( sQ438_spl
<=> ( s__instance(X0,s__Perception)
| ~ s__instance(X0,s__Seeing) ) ),
introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition]) ).
fof(f46579,plain,
( sQ438_spl
| ~ sQ297_spl ),
inference(split_clause,[status(thm)],[f46547,f45815,f46576]) ).
fof(f46580,definition,
! [X0] :
( sQ439_spl
<=> ( s__instance(X0,s__IntentionalPsychologicalProcess)
| ~ s__instance(X0,s__Reasoning) ) ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f46583,plain,
( sQ439_spl
| ~ sQ302_spl ),
inference(split_clause,[status(thm)],[f46548,f45832,f46580]) ).
fof(f46608,definition,
! [X0] :
( sQ446_spl
<=> ( s__instance(X0,s__Process)
| ~ s__instance(X0,s__Motion) ) ),
introduced(definition,[new_symbols(definition,[sQ446_spl])],[split_symbol_definition]) ).
fof(f46611,plain,
( sQ446_spl
| ~ sQ308_spl ),
inference(split_clause,[status(thm)],[f46555,f45854,f46608]) ).
fof(f46620,definition,
! [X0] :
( sQ449_spl
<=> ( s__instance(X0,s__IntentionalPsychologicalProcess)
| ~ s__instance(X0,s__Planning) ) ),
introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition]) ).
fof(f46623,plain,
( sQ449_spl
| ~ sQ250_spl ),
inference(split_clause,[status(thm)],[f46558,f45659,f46620]) ).
fof(f46624,definition,
! [X0] :
( sQ450_spl
<=> ( s__instance(X0,s__PsychologicalProcess)
| ~ s__instance(X0,s__IntentionalPsychologicalProcess) ) ),
introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition]) ).
fof(f46627,plain,
( sQ450_spl
| ~ sQ245_spl ),
inference(split_clause,[status(thm)],[f46559,f45643,f46624]) ).
fof(f46628,definition,
! [X0] :
( sQ451_spl
<=> ( s__instance(X0,s__IntentionalProcess)
| ~ s__instance(X0,s__IntentionalPsychologicalProcess) ) ),
introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition]) ).
fof(f46631,plain,
( sQ451_spl
| ~ sQ245_spl ),
inference(split_clause,[status(thm)],[f46560,f45643,f46628]) ).
fof(f46632,definition,
! [X0] :
( sQ452_spl
<=> ( s__instance(X0,s__Process)
| ~ s__instance(X0,s__IntentionalProcess) ) ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f46635,plain,
( sQ452_spl
| ~ sQ255_spl ),
inference(split_clause,[status(thm)],[f46561,f45676,f46632]) ).
fof(f46648,definition,
! [X0] :
( sQ456_spl
<=> ( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__LegalAgent) ) ),
introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition]) ).
fof(f46651,plain,
( sQ456_spl
| ~ sQ272_spl ),
inference(split_clause,[status(thm)],[f46565,f45732,f46648]) ).
fof(f46652,definition,
! [X0] :
( sQ457_spl
<=> ( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__SentientAgent) ) ),
introduced(definition,[new_symbols(definition,[sQ457_spl])],[split_symbol_definition]) ).
fof(f46653,plain,
! [X0] :
( ~ sQ457_spl
| s__instance(X0,s__Agent)
| ~ s__instance(X0,s__SentientAgent) ),
inference(component_clause,[status(thm)],[f46652]) ).
fof(f46655,plain,
( sQ457_spl
| ~ sQ274_spl ),
inference(split_clause,[status(thm)],[f46566,f45739,f46652]) ).
fof(f46656,definition,
! [X0] :
( sQ458_spl
<=> ( s__instance(X0,s__Object)
| ~ s__instance(X0,s__Agent) ) ),
introduced(definition,[new_symbols(definition,[sQ458_spl])],[split_symbol_definition]) ).
fof(f46657,plain,
! [X0] :
( ~ sQ458_spl
| s__instance(X0,s__Object)
| ~ s__instance(X0,s__Agent) ),
inference(component_clause,[status(thm)],[f46656]) ).
fof(f46659,plain,
( sQ458_spl
| ~ sQ270_spl ),
inference(split_clause,[status(thm)],[f46567,f45726,f46656]) ).
fof(f46678,plain,
( sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f45834,f46392]) ).
fof(f46679,plain,
sQ302_spl,
inference(contradiction_clause,[status(thm)],[f46678]) ).
fof(f46717,plain,
! [X0,X1,X2] :
( X0 = X2
| X1 = X2
| ~ s__subclass(X0,X2)
| ~ s__subclass(X2,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__immediateSubclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[status(thm)],[f16803,f16793]) ).
fof(f47494,plain,
! [X0] :
( s__instance(X0,s__Object)
| ~ s__instance(X0,s__TwoDimensionalObject)
| ~ s__instance(s__TwoDimensionalObject,s__SetOrClass) ),
inference(resolution,[status(thm)],[f33318,f46545]) ).
fof(f47496,plain,
s__instance(s__TwoDimensionalObject,s__SetOrClass),
inference(resolution,[status(thm)],[f33318,f16792]) ).
fof(f47505,definition,
! [X0] :
( sQ556_spl
<=> ( s__instance(X0,s__Object)
| ~ s__instance(X0,s__TwoDimensionalObject) ) ),
introduced(definition,[new_symbols(definition,[sQ556_spl])],[split_symbol_definition]) ).
fof(f47508,plain,
( sQ556_spl
| ~ sQ392_spl ),
inference(split_clause,[status(thm)],[f47494,f46162,f47505]) ).
fof(f47509,plain,
( sQ392_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f47496,f46164]) ).
fof(f47510,plain,
sQ392_spl,
inference(contradiction_clause,[status(thm)],[f47509]) ).
fof(f47578,plain,
! [X0] :
( s__subclass(s__PsychologicalProcess,X0)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[status(thm)],[f16848,f46496]) ).
fof(f47597,plain,
! [X0,X1] :
( s__PsychologicalProcess = X0
| X1 = X0
| ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__immediateSubclass(s__PsychologicalProcess,X1)
| ~ s__instance(s__PsychologicalProcess,s__SetOrClass)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[status(thm)],[f47578,f46717]) ).
fof(f47599,plain,
! [X0,X1] :
( X1 = s__PsychologicalProcess
| X0 = s__PsychologicalProcess
| ~ s__subclass(X1,s__PsychologicalProcess)
| ~ s__instance(s__PsychologicalProcess,s__SetOrClass)
| ~ s__immediateSubclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[status(thm)],[f47578,f46717]) ).
fof(f47600,plain,
! [X0,X1] :
( s__instance(X1,X0)
| ~ s__instance(X1,s__PsychologicalProcess)
| ~ s__instance(s__PsychologicalProcess,s__SetOrClass)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[status(thm)],[f47578,f46545]) ).
fof(f47604,definition,
! [X0,X1] :
( sQ562_spl
<=> ( s__PsychologicalProcess = X0
| X1 = X0
| ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__immediateSubclass(s__PsychologicalProcess,X1)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[sQ562_spl])],[split_symbol_definition]) ).
fof(f47607,plain,
( ~ sQ252_spl
| sQ562_spl ),
inference(split_clause,[status(thm)],[f47597,f47604,f45666]) ).
fof(f47609,definition,
! [X0,X1] :
( sQ563_spl
<=> ( X1 = s__PsychologicalProcess
| X0 = s__PsychologicalProcess
| ~ s__subclass(X1,s__PsychologicalProcess)
| ~ s__immediateSubclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[sQ563_spl])],[split_symbol_definition]) ).
fof(f47612,plain,
( ~ sQ252_spl
| sQ563_spl ),
inference(split_clause,[status(thm)],[f47599,f47609,f45666]) ).
fof(f47613,definition,
! [X0,X1] :
( sQ564_spl
<=> ( s__instance(X1,X0)
| ~ s__instance(X1,s__PsychologicalProcess)
| ~ s__immediateSubclass(s__PsychologicalProcess,X0)
| ~ s__instance(X0,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition]) ).
fof(f47616,plain,
( ~ sQ252_spl
| sQ564_spl ),
inference(split_clause,[status(thm)],[f47600,f47613,f45666]) ).
fof(f47726,plain,
! [X0] :
( s__instance(X0,s__Human)
| ~ s__instance(X0,s__Woman)
| ~ s__instance(s__Woman,s__SetOrClass) ),
inference(resolution,[status(thm)],[f29507,f46545]) ).
fof(f47728,plain,
s__instance(s__Woman,s__SetOrClass),
inference(resolution,[status(thm)],[f29507,f16792]) ).
fof(f47737,definition,
! [X0] :
( sQ581_spl
<=> ( s__instance(X0,s__Human)
| ~ s__instance(X0,s__Woman) ) ),
introduced(definition,[new_symbols(definition,[sQ581_spl])],[split_symbol_definition]) ).
fof(f47740,plain,
( sQ581_spl
| ~ sQ368_spl ),
inference(split_clause,[status(thm)],[f47726,f46074,f47737]) ).
fof(f47741,plain,
( sQ368_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f47728,f46076]) ).
fof(f47742,plain,
sQ368_spl,
inference(contradiction_clause,[status(thm)],[f47741]) ).
fof(f47744,plain,
( ~ sQ369_spl
| sQ436_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46479,f46536]) ).
fof(f47745,plain,
( ~ sQ369_spl
| sQ436_spl ),
inference(contradiction_clause,[status(thm)],[f47744]) ).
fof(f47987,plain,
! [X0] :
( s__instance(X0,s__Animal)
| ~ s__instance(X0,s__DomesticAnimal)
| ~ s__instance(s__DomesticAnimal,s__SetOrClass) ),
inference(resolution,[status(thm)],[f39790,f46545]) ).
fof(f47998,definition,
! [X0] :
( sQ615_spl
<=> ( s__instance(X0,s__Animal)
| ~ s__instance(X0,s__DomesticAnimal) ) ),
introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition]) ).
fof(f48001,plain,
( sQ615_spl
| ~ sQ422_spl ),
inference(split_clause,[status(thm)],[f47987,f46274,f47998]) ).
fof(f48018,plain,
! [X0] :
( s__instance(X0,s__Organism)
| ~ s__instance(X0,s__Animal)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolution,[status(thm)],[f29374,f46545]) ).
fof(f48029,definition,
! [X0] :
( sQ618_spl
<=> ( s__instance(X0,s__Organism)
| ~ s__instance(X0,s__Animal) ) ),
introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition]) ).
fof(f48032,plain,
( sQ618_spl
| ~ sQ353_spl ),
inference(split_clause,[status(thm)],[f48018,f46019,f48029]) ).
fof(f48131,plain,
s__instance(s__Planning,s__SetOrClass),
inference(resolution,[status(thm)],[f27831,f16792]) ).
fof(f48135,plain,
( sQ250_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48131,f45661]) ).
fof(f48136,plain,
sQ250_spl,
inference(contradiction_clause,[status(thm)],[f48135]) ).
fof(f48165,plain,
s__instance(s__Motion,s__SetOrClass),
inference(resolution,[status(thm)],[f27912,f16792]) ).
fof(f48169,plain,
( sQ308_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48165,f45856]) ).
fof(f48170,plain,
sQ308_spl,
inference(contradiction_clause,[status(thm)],[f48169]) ).
fof(f48389,plain,
! [X0] :
( s__instance(X0,s__Human)
| ~ s__instance(X0,s__HumanYouth)
| ~ s__instance(s__HumanYouth,s__SetOrClass) ),
inference(resolution,[status(thm)],[f31248,f46545]) ).
fof(f48391,plain,
s__instance(s__HumanYouth,s__SetOrClass),
inference(resolution,[status(thm)],[f31248,f16792]) ).
fof(f48400,definition,
! [X0] :
( sQ664_spl
<=> ( s__instance(X0,s__Human)
| ~ s__instance(X0,s__HumanYouth) ) ),
introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition]) ).
fof(f48403,plain,
( sQ664_spl
| ~ sQ386_spl ),
inference(split_clause,[status(thm)],[f48389,f46140,f48400]) ).
fof(f48404,plain,
( sQ386_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48391,f46142]) ).
fof(f48405,plain,
sQ386_spl,
inference(contradiction_clause,[status(thm)],[f48404]) ).
fof(f48409,plain,
! [X0] :
( s__instance(X0,s__Human)
| ~ s__instance(X0,s__HumanAdult)
| ~ s__instance(s__HumanAdult,s__SetOrClass) ),
inference(resolution,[status(thm)],[f31241,f46545]) ).
fof(f48411,plain,
s__instance(s__HumanAdult,s__SetOrClass),
inference(resolution,[status(thm)],[f31241,f16792]) ).
fof(f48420,definition,
! [X0] :
( sQ667_spl
<=> ( s__instance(X0,s__Human)
| ~ s__instance(X0,s__HumanAdult) ) ),
introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition]) ).
fof(f48423,plain,
( sQ667_spl
| ~ sQ383_spl ),
inference(split_clause,[status(thm)],[f48409,f46129,f48420]) ).
fof(f48424,plain,
( sQ383_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48411,f46131]) ).
fof(f48425,plain,
sQ383_spl,
inference(contradiction_clause,[status(thm)],[f48424]) ).
fof(f48757,definition,
! [X0] :
( sQ707_spl
<=> ( s__instance(X0,s__Object)
| ~ s__instance(X0,s__CognitiveAgent) ) ),
introduced(definition,[new_symbols(definition,[sQ707_spl])],[split_symbol_definition]) ).
fof(f48758,plain,
! [X0] :
( ~ sQ707_spl
| s__instance(X0,s__Object)
| ~ s__instance(X0,s__CognitiveAgent) ),
inference(component_clause,[status(thm)],[f48757]) ).
fof(f48865,plain,
s__instance(s__DomesticAnimal,s__SetOrClass),
inference(resolution,[status(thm)],[f39790,f16792]) ).
fof(f48869,plain,
( sQ422_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f48865,f46276]) ).
fof(f48870,plain,
sQ422_spl,
inference(contradiction_clause,[status(thm)],[f48869]) ).
fof(f48895,plain,
! [X0] :
( s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Human)
| ~ s__instance(s__Human,s__SetOrClass) ),
inference(resolution,[status(thm)],[f29498,f46545]) ).
fof(f48906,definition,
! [X0] :
( sQ716_spl
<=> ( s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Human) ) ),
introduced(definition,[new_symbols(definition,[sQ716_spl])],[split_symbol_definition]) ).
fof(f48907,plain,
! [X0] :
( ~ sQ716_spl
| s__instance(X0,s__CognitiveAgent)
| ~ s__instance(X0,s__Human) ),
inference(component_clause,[status(thm)],[f48906]) ).
fof(f48909,plain,
( sQ716_spl
| ~ sQ362_spl ),
inference(split_clause,[status(thm)],[f48895,f46052,f48906]) ).
fof(f49037,plain,
! [X0] :
( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Organism,s__SetOrClass) ),
inference(resolution,[status(thm)],[f29321,f46545]) ).
fof(f49048,definition,
! [X0] :
( sQ731_spl
<=> ( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__Organism) ) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f49051,plain,
( sQ731_spl
| ~ sQ350_spl ),
inference(split_clause,[status(thm)],[f49037,f46008,f49048]) ).
fof(f49070,definition,
! [X0] :
( sQ735_spl
<=> ( s__instance(X0,s__Agent)
| ~ s__instance(X0,s__CognitiveAgent) ) ),
introduced(definition,[new_symbols(definition,[sQ735_spl])],[split_symbol_definition]) ).
fof(f49071,plain,
! [X0] :
( ~ sQ735_spl
| s__instance(X0,s__Agent)
| ~ s__instance(X0,s__CognitiveAgent) ),
inference(component_clause,[status(thm)],[f49070]) ).
fof(f49152,plain,
s__instance(s__LegalAgent,s__SetOrClass),
inference(resolution,[status(thm)],[f18395,f16792]) ).
fof(f49156,plain,
( sQ272_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f49152,f45734]) ).
fof(f49157,plain,
sQ272_spl,
inference(contradiction_clause,[status(thm)],[f49156]) ).
fof(f49378,definition,
( sQ758_spl
<=> s__instance(s__Jane8_1,s__Human) ),
introduced(definition,[new_symbols(definition,[sQ758_spl])],[split_symbol_definition]) ).
fof(f49380,plain,
( sQ758_spl
| ~ s__instance(s__Jane8_1,s__Human) ),
inference(component_clause,[status(thm)],[f49378]) ).
fof(f49385,plain,
( sQ758_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f49380,f44204]) ).
fof(f49386,plain,
sQ758_spl,
inference(contradiction_clause,[status(thm)],[f49385]) ).
fof(f49411,plain,
! [X0] :
( s__cohabitant(s__Jane8_1,X0)
| ~ s__domesticPartner(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human) ),
inference(resolution,[status(thm)],[f17032,f44204]) ).
fof(f49436,plain,
! [X0] :
( ~ s__domesticPartner(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human)
| s__mutualAcquaintance(s__Jane8_1,X0)
| ~ s__instance(s__Jane8_1,s__Human)
| ~ s__instance(X0,s__Human) ),
inference(resolution,[status(thm)],[f17048,f49411]) ).
fof(f49438,definition,
! [X0] :
( sQ760_spl
<=> ( ~ s__domesticPartner(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human)
| s__mutualAcquaintance(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human) ) ),
introduced(definition,[new_symbols(definition,[sQ760_spl])],[split_symbol_definition]) ).
fof(f49439,plain,
! [X0] :
( ~ sQ760_spl
| ~ s__domesticPartner(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human)
| s__mutualAcquaintance(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human) ),
inference(component_clause,[status(thm)],[f49438]) ).
fof(f49441,plain,
( ~ sQ758_spl
| sQ760_spl ),
inference(split_clause,[status(thm)],[f49436,f49438,f49378]) ).
fof(f49443,plain,
! [X0] :
( ~ sQ760_spl
| ~ s__domesticPartner(s__Jane8_1,X0)
| s__mutualAcquaintance(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human) ),
inference(duplicate_literals_removal,[status(thm)],[f49439]) ).
fof(f49448,plain,
! [X0,X1,X2] :
( s__instance(X2,s__SetOrClass)
| s__instance(X2,s__SetOrClass)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f25560,f25560]) ).
fof(f49449,definition,
! [X0,X1] :
( sQ761_spl
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition]) ).
fof(f49450,plain,
! [X0,X1] :
( ~ sQ761_spl
| X0 = X1 ),
inference(component_clause,[status(thm)],[f49449]) ).
fof(f49452,definition,
! [X2] :
( sQ762_spl
<=> ( s__instance(X2,s__SetOrClass)
| s__instance(X2,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[sQ762_spl])],[split_symbol_definition]) ).
fof(f49453,plain,
! [X0] :
( ~ sQ762_spl
| s__instance(X0,s__SetOrClass)
| s__instance(X0,s__SetOrClass) ),
inference(component_clause,[status(thm)],[f49452]) ).
fof(f49455,plain,
( sQ762_spl
| sQ761_spl ),
inference(split_clause,[status(thm)],[f49448,f49449,f49452]) ).
fof(f49456,plain,
! [X0] :
( ~ sQ762_spl
| s__instance(X0,s__SetOrClass) ),
inference(duplicate_literals_removal,[status(thm)],[f49453]) ).
fof(f49463,plain,
! [X0,X1,X2] :
( ~ sQ762_spl
| s__instance(X2,X1)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f46545,f49456]) ).
fof(f49474,plain,
! [X0] :
( ~ sQ761_spl
| s__instance(X0,s__SetOrClass) ),
inference(paramodulation,[status(thm)],[f49450,f46496]) ).
fof(f49478,plain,
! [X0,X1] :
( ~ sQ761_spl
| s__instance(X0,X1) ),
inference(paramodulation,[status(thm)],[f49450,f49474]) ).
fof(f49602,plain,
( sQ242_spl
| ~ sQ761_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f45608,f49478]) ).
fof(f49682,plain,
( sQ242_spl
| ~ sQ761_spl ),
inference(contradiction_clause,[status(thm)],[f49602]) ).
fof(f49713,plain,
! [X0] :
( ~ sQ761_spl
| ~ sQ436_spl
| s__instance(X0,s__Woman) ),
inference(paramodulation,[status(thm)],[f49450,f46535]) ).
fof(f49717,plain,
! [X0,X1] :
( ~ sQ761_spl
| ~ sQ436_spl
| s__instance(X0,X1) ),
inference(paramodulation,[status(thm)],[f49450,f49713]) ).
fof(f49741,plain,
( sQ244_spl
| ~ sQ761_spl
| ~ sQ436_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f45618,f49717]) ).
fof(f49742,plain,
( sQ244_spl
| ~ sQ761_spl
| ~ sQ436_spl ),
inference(contradiction_clause,[status(thm)],[f49741]) ).
fof(f49743,plain,
( sQ369_spl
| ~ sQ761_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f46079,f49450]) ).
fof(f49744,plain,
( sQ369_spl
| ~ sQ761_spl ),
inference(contradiction_clause,[status(thm)],[f49743]) ).
fof(f49797,plain,
! [X0] :
( ~ sQ760_spl
| s__acquaintance(s__Jane8_1,X0)
| ~ s__instance(s__Jane8_1,s__Human)
| ~ s__instance(X0,s__Human)
| ~ s__domesticPartner(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human) ),
inference(resolution,[status(thm)],[f49443,f17079]) ).
fof(f49798,definition,
! [X0] :
( sQ767_spl
<=> ( s__acquaintance(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human)
| ~ s__domesticPartner(s__Jane8_1,X0)
| ~ s__instance(X0,s__Human) ) ),
introduced(definition,[new_symbols(definition,[sQ767_spl])],[split_symbol_definition]) ).
fof(f49801,plain,
( ~ sQ760_spl
| ~ sQ758_spl
| sQ767_spl ),
inference(split_clause,[status(thm)],[f49797,f49798,f49378,f49438]) ).
fof(f50128,plain,
( sQ243_spl
| ~ sQ716_spl
| ~ s__instance(s__Jane8_1,s__Human) ),
inference(resolution,[status(thm)],[f48907,f45611]) ).
fof(f50130,plain,
( sQ243_spl
| ~ sQ716_spl
| ~ sQ758_spl ),
inference(split_clause,[status(thm)],[f50128,f49378,f48906,f45609]) ).
fof(f50570,plain,
( ~ sQ243_spl
| ~ sQ707_spl
| s__instance(s__Jane8_1,s__Object) ),
inference(resolution,[status(thm)],[f48758,f45610]) ).
fof(f50571,plain,
( ~ sQ243_spl
| ~ sQ707_spl
| sQ242_spl ),
inference(split_clause,[status(thm)],[f50570,f45606,f48757,f45609]) ).
fof(f50578,plain,
! [X0] :
( ~ sQ458_spl
| ~ sQ735_spl
| s__instance(X0,s__Object)
| ~ s__instance(X0,s__CognitiveAgent) ),
inference(resolution,[status(thm)],[f49071,f46657]) ).
fof(f50580,plain,
( ~ sQ458_spl
| ~ sQ735_spl
| sQ707_spl ),
inference(split_clause,[status(thm)],[f50578,f48757,f49070,f46656]) ).
fof(f50705,definition,
( sQ819_spl
<=> "2" = "2" ),
introduced(definition,[new_symbols(definition,[sQ819_spl])],[split_symbol_definition]) ).
fof(f50710,plain,
! [X0] :
( "2" = "2"
| ~ s__relatedInternalConcept(X0,X0) ),
inference(paramodulation,[status(thm)],[f45328,f22531]) ).
fof(f50711,definition,
! [X0] :
( sQ820_spl
<=> ~ s__relatedInternalConcept(X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ820_spl])],[split_symbol_definition]) ).
fof(f50712,plain,
! [X0] :
( ~ sQ820_spl
| ~ s__relatedInternalConcept(X0,X0) ),
inference(component_clause,[status(thm)],[f50711]) ).
fof(f50714,plain,
( sQ819_spl
| sQ820_spl ),
inference(split_clause,[status(thm)],[f50710,f50711,f50705]) ).
fof(f50715,plain,
( ~ sQ820_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f50712,f18870]) ).
fof(f50716,plain,
~ sQ820_spl,
inference(contradiction_clause,[status(thm)],[f50715]) ).
fof(f50739,plain,
! [X0] :
( ~ sQ762_spl
| s__instance(X0,s__SentientAgent)
| ~ s__instance(X0,s__CognitiveAgent) ),
inference(resolution,[status(thm)],[f49463,f18392]) ).
fof(f50777,plain,
( sQ244_spl
| ~ sQ762_spl
| ~ s__instance(s__Jane8_1,s__CognitiveAgent) ),
inference(resolution,[status(thm)],[f50739,f45618]) ).
fof(f50778,plain,
! [X0] :
( ~ sQ457_spl
| ~ sQ762_spl
| s__instance(X0,s__Agent)
| ~ s__instance(X0,s__CognitiveAgent) ),
inference(resolution,[status(thm)],[f50739,f46653]) ).
fof(f50779,plain,
( sQ244_spl
| ~ sQ762_spl
| ~ sQ243_spl ),
inference(split_clause,[status(thm)],[f50777,f45609,f49452,f45616]) ).
fof(f50780,plain,
( ~ sQ457_spl
| ~ sQ762_spl
| sQ735_spl ),
inference(split_clause,[status(thm)],[f50778,f49070,f49452,f46652]) ).
fof(f50781,plain,
$false,
inference(sat_refutation,[status(thm)],[f45239,f45612,f45619,f45623,f46394,f46396,f46398,f46400,f46402,f46404,f46406,f46408,f46410,f46412,f46528,f46530,f46532,f46575,f46579,f46583,f46611,f46623,f46627,f46631,f46635,f46651,f46655,f46659,f46679,f47508,f47510,f47607,f47612,f47616,f47740,f47742,f47745,f48001,f48032,f48136,f48170,f48403,f48405,f48423,f48425,f48870,f48909,f49051,f49157,f49386,f49441,f49455,f49682,f49742,f49744,f49801,f50130,f50571,f50580,f50714,f50716,f50779,f50780]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR082+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 14:51:02 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.66/0.94 % Drodi V4.1.1
% 56.43/8.08 % Refutation found
% 56.43/8.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.43/8.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 44.33/8.29 % Elapsed time: 7.904493 seconds
% 44.33/8.29 % CPU time: 57.730728 seconds
% 44.33/8.29 % Total memory used: 1.244 GB
% 44.33/8.29 % Net memory used: 1.235 GB
%------------------------------------------------------------------------------