(note TQG2)  ;; boolean version

(time 600)

(instance TheKB2-1 ComputerProgram)
(instance Inconsistent Attribute)

(=>
  (and
    (contraryAttribute ?ATTR1 ?ATTR2)
    (property ?X ?ATTR1)
    (property ?X ?ATTR2))
  (property TheKB2-1 Inconsistent))

(instance Entity2-1 Organism)
(instance Entity2-2 Organism)
(mother Entity2-1 Entity2-2)
(father Entity2-1 Entity2-2)

(query (property TheKB2-1 Inconsistent))

(answer yes)


;; Answer 1. [yes]

;; 1. 	(instance Entity2-2 Organism)	[KB]	
;; 2. 	(instance Entity2-2 Organism)	1 	
;; 3. 	(subclass Organism Object)	[KB]	
;; 4. 	(subclass Organism Object)	3 	
;; 5. 	(=>
;;     (subclass ?X403 ?X404)
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass)))	[KB]	
;; 6. 	(or
;;     (instance ?X1 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	5 	
;; 7. 	(or
;;     (instance ?X0 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	5 	
;; 8. 	(=>
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass))
;;     (=>
;;         (and
;;             (subclass ?X403 ?X404)
;;             (instance ?X405 ?X403))
;;         (instance ?X405 ?X404)))	[KB]	
;; 9. 	(or
;;     (instance ?X2 ?X1)
;;     (not
;;         (instance ?X2 ?X0))
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X1 SetOrClass))
;;     (not
;;         (instance ?X0 SetOrClass)))	8 	
;; 10. 	(or
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X2 ?X0))
;;     (instance ?X2 ?X1))	6 7 9 	
;; 11. 	(or
;;     (not
;;         (instance ?X0 Organism))
;;     (instance ?X0 Object))	4 10 	
;; 12. 	(instance Entity2-2 Object)	2 11 	
;; 13. 	(instance Female Attribute)	[KB]	
;; 14. 	(instance Female Attribute)	13 	
;; 15. 	(=>
;;     (and
;;         (instance ?X91 Object)
;;         (instance ?X92 Attribute))
;;     (=>
;;         (attribute ?X91 ?X92)
;;         (property ?X91 ?X92)))	[KB]	
;; 16. 	(or
;;     (property ?X0 ?X1)
;;     (not
;;         (attribute ?X0 ?X1))
;;     (not
;;         (instance ?X1 Attribute))
;;     (not
;;         (instance ?X0 Object)))	15 	
;; 17. 	(instance Entity2-1 Organism)	[KB]	
;; 18. 	(instance Entity2-1 Organism)	17 	
;; 19. 	(mother Entity2-1 Entity2-2)	[KB]	
;; 20. 	(mother Entity2-1 Entity2-2)	19 	
;; 21. 	(=>
;;     (and
;;         (instance ?X109 Organism)
;;         (instance ?X69 Organism))
;;     (=>
;;         (mother ?X109 ?X69)
;;         (attribute ?X69 Female)))	[KB]	
;; 22. 	(or
;;     (attribute ?X1 Female)
;;     (not
;;         (mother ?X0 ?X1))
;;     (not
;;         (instance ?X1 Organism))
;;     (not
;;         (instance ?X0 Organism)))	21 	
;; 23. 	(attribute Entity2-2 Female)	2 18 20 22 	
;; 24. 	(or
;;     (property Entity2-2 Female)
;;     (not
;;         (instance Entity2-2 Object)))	14 16 23 	
;; 25. 	(instance Male Attribute)	[KB]	
;; 26. 	(instance Male Attribute)	25 	
;; 27. 	(not
;;     (property TheKB Inconsistent))	[Negated Query]	
;; 28. 	(not
;;     (property TheKB Inconsistent))	27 	
;; 29. 	(=>
;;     (and
;;         (instance ?X85 Attribute)
;;         (instance ?X86 Attribute))
;;     (=>
;;         (and
;;             (contraryAttribute ?X86 ?X85)
;;             (property ?X403 ?X86)
;;             (property ?X403 ?X85))
;;         (property TheKB Inconsistent)))	[KB]	
;; 30. 	(or
;;     (property TheKB Inconsistent)
;;     (not
;;         (property ?X2 ?X0))
;;     (not
;;         (property ?X2 ?X1))
;;     (not
;;         (contraryAttribute ?X1 ?X0))
;;     (not
;;         (instance ?X1 Attribute))
;;     (not
;;         (instance ?X0 Attribute)))	29 	
;; 31. 	(or
;;     (not
;;         (contraryAttribute ?X0 ?X1))
;;     (not
;;         (property ?X2 ?X1))
;;     (not
;;         (property ?X2 ?X0))
;;     (not
;;         (instance ?X0 Attribute))
;;     (not
;;         (instance ?X1 Attribute)))	28 30 	
;; 32. 	(contraryAttribute Male Female)	[KB]	
;; 33. 	(contraryAttribute Male Female)	32 	
;; 34. 	(or
;;     (not
;;         (property ?X0 Male))
;;     (not
;;         (property ?X0 Female)))	26 14 31 33 	
;; 35. 	(father Entity2-1 Entity2-2)	[KB]	
;; 36. 	(father Entity2-1 Entity2-2)	35 	
;; 37. 	(=>
;;     (and
;;         (instance ?X109 Organism)
;;         (instance ?X68 Organism))
;;     (=>
;;         (father ?X109 ?X68)
;;         (attribute ?X68 Male)))	[KB]	
;; 38. 	(or
;;     (attribute ?X1 Male)
;;     (not
;;         (father ?X0 ?X1))
;;     (not
;;         (instance ?X1 Organism))
;;     (not
;;         (instance ?X0 Organism)))	37 	
;; 39. 	(attribute Entity2-2 Male)	2 18 36 38 	
;; 40. 	(or
;;     (property Entity2-2 Male)
;;     (not
;;         (instance Entity2-2 Object)))	26 16 39 	
;; 41. 	True	12 24 34 40 	


;; EP---0.999 finds the following proof:

;; # Problem is unsatisfiable (or provable), constructing proof object
;; # SZS status: Theorem
;; WATCH: 224.6 CPU 224.6 WC
;; WATCH: 226.6 CPU 226.6 WC
;; # SZS output start CNFRefutation.
;; fof(16, axiom,![X6]:![X7]:(s_subclass(X6,X7)=>(s_instance(X6,s_SetOrClass)&s_instance(X7,s_SetOrClass))),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_26)).
;; fof(17, axiom,![X6]:![X7]:![X8]:((s_instance(X6,s_SetOrClass)&s_instance(X7,s_SetOrClass))=>((s_subclass(X6,X7)&s_instance(X8,X6))=>s_instance(X8,X7))),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_27)).
;; fof(161, axiom,![X15]:![X16]:((s_instance(X15,s_Object)&s_instance(X16,s_Attribute))=>(s_attribute(X15,X16)=>s_property(X15,X16))),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_175)).
;; fof(2993, axiom,![X225]:![X228]:((s_instance(X225,s_Organism)&s_instance(X228,s_Organism))=>(s_mother(X225,X228)=>s_attribute(X228,s_Female))),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_5324)).
;; fof(2996, axiom,![X225]:![X229]:((s_instance(X225,s_Organism)&s_instance(X229,s_Organism))=>(s_father(X225,X229)=>s_attribute(X229,s_Male))),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_5330)).
;; fof(3297, axiom,s_contraryAttribute_2(s_Male,s_Female),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_5875)).
;; fof(5735, axiom,s_subclass(s_Organism,s_Object),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_8333)).
;; fof(8432, axiom,s_instance(s_Male,s_Attribute),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_11030)).
;; fof(9022, axiom,s_instance(s_Female,s_Attribute),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_11620)).
;; fof(10613, axiom,s_mother(s_Entity2_1,s_Entity2_2),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_13211)).
;; fof(10616, axiom,![X24]:![X25]:![X6]:((s_instance(X24,s_Attribute)&s_instance(X25,s_Attribute))=>(((s_contraryAttribute_2(X25,X24)&s_property(X6,X25))&s_property(X6,X24))=>s_property(s_TheKB,s_Inconsistent))),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_13222)).
;; fof(10617, axiom,s_instance(s_Entity2_1,s_Organism),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_13223)).
;; fof(10618, axiom,s_instance(s_Entity2_2,s_Organism),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_13224)).
;; fof(10619, axiom,s_father(s_Entity2_1,s_Entity2_2),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', kb_SUMO_13225)).
;; fof(10620, conjecture,s_property(s_TheKB,s_Inconsistent),file('/tmp/SystemOnTPTP20546/SOT_XIFS60.p', prove_from_SUMO)).
;; fof(10621, negated_conjecture,~(s_property(s_TheKB,s_Inconsistent)),inference(assume_negation,[status(cth)],[10620])).
;; fof(10802, negated_conjecture,~(s_property(s_TheKB,s_Inconsistent)),inference(fof_simplification,[status(thm)],[10621,theory(equality)])).
;; fof(10837, plain,![X6]:![X7]:(~(s_subclass(X6,X7))|(s_instance(X6,s_SetOrClass)&s_instance(X7,s_SetOrClass))),inference(fof_nnf,[status(thm)],[16])).
;; fof(10838, plain,![X8]:![X9]:(~(s_subclass(X8,X9))|(s_instance(X8,s_SetOrClass)&s_instance(X9,s_SetOrClass))),inference(variable_rename,[status(thm)],[10837])).
;; fof(10839, plain,![X8]:![X9]:((s_instance(X8,s_SetOrClass)|~(s_subclass(X8,X9)))&(s_instance(X9,s_SetOrClass)|~(s_subclass(X8,X9)))),inference(distribute,[status(thm)],[10838])).
;; cnf(10840,plain,(s_instance(X2,s_SetOrClass)|~s_subclass(X1,X2)),inference(split_conjunct,[status(thm)],[10839])).
;; cnf(10841,plain,(s_instance(X1,s_SetOrClass)|~s_subclass(X1,X2)),inference(split_conjunct,[status(thm)],[10839])).
;; fof(10842, plain,![X6]:![X7]:![X8]:((~(s_instance(X6,s_SetOrClass))|~(s_instance(X7,s_SetOrClass)))|((~(s_subclass(X6,X7))|~(s_instance(X8,X6)))|s_instance(X8,X7))),inference(fof_nnf,[status(thm)],[17])).
;; fof(10843, plain,![X9]:![X10]:![X11]:((~(s_instance(X9,s_SetOrClass))|~(s_instance(X10,s_SetOrClass)))|((~(s_subclass(X9,X10))|~(s_instance(X11,X9)))|s_instance(X11,X10))),inference(variable_rename,[status(thm)],[10842])).
;; cnf(10844,plain,(s_instance(X1,X2)|~s_instance(X1,X3)|~s_subclass(X3,X2)|~s_instance(X2,s_SetOrClass)|~s_instance(X3,s_SetOrClass)),inference(split_conjunct,[status(thm)],[10843])).
;; fof(11265, plain,![X15]:![X16]:((~(s_instance(X15,s_Object))|~(s_instance(X16,s_Attribute)))|(~(s_attribute(X15,X16))|s_property(X15,X16))),inference(fof_nnf,[status(thm)],[161])).
;; fof(11266, plain,![X17]:![X18]:((~(s_instance(X17,s_Object))|~(s_instance(X18,s_Attribute)))|(~(s_attribute(X17,X18))|s_property(X17,X18))),inference(variable_rename,[status(thm)],[11265])).
;; cnf(11267,plain,(s_property(X1,X2)|~s_attribute(X1,X2)|~s_instance(X2,s_Attribute)|~s_instance(X1,s_Object)),inference(split_conjunct,[status(thm)],[11266])).
;; fof(17531, plain,![X225]:![X228]:((~(s_instance(X225,s_Organism))|~(s_instance(X228,s_Organism)))|(~(s_mother(X225,X228))|s_attribute(X228,s_Female))),inference(fof_nnf,[status(thm)],[2993])).
;; fof(17532, plain,![X229]:![X230]:((~(s_instance(X229,s_Organism))|~(s_instance(X230,s_Organism)))|(~(s_mother(X229,X230))|s_attribute(X230,s_Female))),inference(variable_rename,[status(thm)],[17531])).
;; cnf(17533,plain,(s_attribute(X1,s_Female)|~s_mother(X2,X1)|~s_instance(X1,s_Organism)|~s_instance(X2,s_Organism)),inference(split_conjunct,[status(thm)],[17532])).
;; fof(17536, plain,![X225]:![X229]:((~(s_instance(X225,s_Organism))|~(s_instance(X229,s_Organism)))|(~(s_father(X225,X229))|s_attribute(X229,s_Male))),inference(fof_nnf,[status(thm)],[2996])).
;; fof(17537, plain,![X230]:![X231]:((~(s_instance(X230,s_Organism))|~(s_instance(X231,s_Organism)))|(~(s_father(X230,X231))|s_attribute(X231,s_Male))),inference(variable_rename,[status(thm)],[17536])).
;; cnf(17538,plain,(s_attribute(X1,s_Male)|~s_father(X2,X1)|~s_instance(X1,s_Organism)|~s_instance(X2,s_Organism)),inference(split_conjunct,[status(thm)],[17537])).
;; cnf(18089,plain,(s_contraryAttribute_2(s_Male,s_Female)),inference(split_conjunct,[status(thm)],[3297])).
;; cnf(20556,plain,(s_subclass(s_Organism,s_Object)),inference(split_conjunct,[status(thm)],[5735])).
;; cnf(23253,plain,(s_instance(s_Male,s_Attribute)),inference(split_conjunct,[status(thm)],[8432])).
;; cnf(23843,plain,(s_instance(s_Female,s_Attribute)),inference(split_conjunct,[status(thm)],[9022])).
;; cnf(25436,plain,(s_mother(s_Entity2_1,s_Entity2_2)),inference(split_conjunct,[status(thm)],[10613])).
;; fof(25439, plain,![X24]:![X25]:![X6]:((~(s_instance(X24,s_Attribute))|~(s_instance(X25,s_Attribute)))|(((~(s_contraryAttribute_2(X25,X24))|~(s_property(X6,X25)))|~(s_property(X6,X24)))|s_property(s_TheKB,s_Inconsistent))),inference(fof_nnf,[status(thm)],[10616])).
;; fof(25440, plain,![X26]:![X27]:![X28]:((~(s_instance(X26,s_Attribute))|~(s_instance(X27,s_Attribute)))|(((~(s_contraryAttribute_2(X27,X26))|~(s_property(X28,X27)))|~(s_property(X28,X26)))|s_property(s_TheKB,s_Inconsistent))),inference(variable_rename,[status(thm)],[25439])).
;; cnf(25441,plain,(s_property(s_TheKB,s_Inconsistent)|~s_property(X1,X2)|~s_property(X1,X3)|~s_contraryAttribute_2(X3,X2)|~s_instance(X3,s_Attribute)|~s_instance(X2,s_Attribute)),inference(split_conjunct,[status(thm)],[25440])).
;; cnf(25442,plain,(s_instance(s_Entity2_1,s_Organism)),inference(split_conjunct,[status(thm)],[10617])).
;; cnf(25443,plain,(s_instance(s_Entity2_2,s_Organism)),inference(split_conjunct,[status(thm)],[10618])).
;; cnf(25444,plain,(s_father(s_Entity2_1,s_Entity2_2)),inference(split_conjunct,[status(thm)],[10619])).
;; cnf(25445,negated_conjecture,(~s_property(s_TheKB,s_Inconsistent)),inference(split_conjunct,[status(thm)],[10802])).
;; cnf(49501,plain,(s_attribute(s_Entity2_2,s_Male)|~s_instance(s_Entity2_1,s_Organism)|~s_instance(s_Entity2_2,s_Organism)),inference(spm,[status(thm)],[17538,25444,theory(equality)])).
;; cnf(49502,plain,(s_attribute(s_Entity2_2,s_Male)|$false|~s_instance(s_Entity2_2,s_Organism)),inference(rw,[status(thm)],[49501,25442,theory(equality)])).
;; cnf(49503,plain,(s_attribute(s_Entity2_2,s_Male)|$false|$false),inference(rw,[status(thm)],[49502,25443,theory(equality)])).
;; cnf(49504,plain,(s_attribute(s_Entity2_2,s_Male)),inference(cn,[status(thm)],[49503,theory(equality)])).
;; cnf(49507,plain,(s_attribute(s_Entity2_2,s_Female)|~s_instance(s_Entity2_1,s_Organism)|~s_instance(s_Entity2_2,s_Organism)),inference(spm,[status(thm)],[17533,25436,theory(equality)])).
;; cnf(49508,plain,(s_attribute(s_Entity2_2,s_Female)|$false|~s_instance(s_Entity2_2,s_Organism)),inference(rw,[status(thm)],[49507,25442,theory(equality)])).
;; cnf(49509,plain,(s_attribute(s_Entity2_2,s_Female)|$false|$false),inference(rw,[status(thm)],[49508,25443,theory(equality)])).
;; cnf(49510,plain,(s_attribute(s_Entity2_2,s_Female)),inference(cn,[status(thm)],[49509,theory(equality)])).
;; cnf(50051,plain,(~s_property(X1,X3)|~s_property(X1,X2)|~s_contraryAttribute_2(X3,X2)|~s_instance(X3,s_Attribute)|~s_instance(X2,s_Attribute)),inference(sr,[status(thm)],[25441,25445,theory(equality)])).
;; cnf(50053,plain,(~s_property(X1,s_Male)|~s_property(X1,s_Female)|~s_instance(s_Male,s_Attribute)|~s_instance(s_Female,s_Attribute)),inference(spm,[status(thm)],[50051,18089,theory(equality)])).
;; cnf(50071,plain,(~s_property(X1,s_Male)|~s_property(X1,s_Female)|$false|~s_instance(s_Female,s_Attribute)),inference(rw,[status(thm)],[50053,23253,theory(equality)])).
;; cnf(50072,plain,(~s_property(X1,s_Male)|~s_property(X1,s_Female)|$false|$false),inference(rw,[status(thm)],[50071,23843,theory(equality)])).
;; cnf(50073,plain,(~s_property(X1,s_Male)|~s_property(X1,s_Female)),inference(cn,[status(thm)],[50072,theory(equality)])).
;; cnf(63639,plain,(s_instance(X1,X2)|~s_subclass(X3,X2)|~s_instance(X3,s_SetOrClass)|~s_instance(X1,X3)),inference(csr,[status(thm)],[10844,10840])).
;; cnf(63640,plain,(s_instance(X1,X2)|~s_subclass(X3,X2)|~s_instance(X1,X3)),inference(csr,[status(thm)],[63639,10841])).
;; cnf(63760,plain,(s_instance(X1,s_Object)|~s_instance(X1,s_Organism)),inference(spm,[status(thm)],[63640,20556,theory(equality)])).
;; cnf(86880,plain,(~s_property(X1,s_Female)|~s_attribute(X1,s_Male)|~s_instance(s_Male,s_Attribute)|~s_instance(X1,s_Object)),inference(spm,[status(thm)],[50073,11267,theory(equality)])).
;; cnf(86881,plain,(~s_property(X1,s_Female)|~s_attribute(X1,s_Male)|$false|~s_instance(X1,s_Object)),inference(rw,[status(thm)],[86880,23253,theory(equality)])).
;; cnf(86882,plain,(~s_property(X1,s_Female)|~s_attribute(X1,s_Male)|~s_instance(X1,s_Object)),inference(cn,[status(thm)],[86881,theory(equality)])).
;; cnf(87134,plain,(~s_attribute(X1,s_Male)|~s_instance(X1,s_Object)|~s_attribute(X1,s_Female)|~s_instance(s_Female,s_Attribute)),inference(spm,[status(thm)],[86882,11267,theory(equality)])).
;; cnf(87135,plain,(~s_attribute(X1,s_Male)|~s_instance(X1,s_Object)|~s_attribute(X1,s_Female)|$false),inference(rw,[status(thm)],[87134,23843,theory(equality)])).
;; cnf(87136,plain,(~s_attribute(X1,s_Male)|~s_instance(X1,s_Object)|~s_attribute(X1,s_Female)),inference(cn,[status(thm)],[87135,theory(equality)])).
;; cnf(168493,plain,(~s_attribute(s_Entity2_2,s_Female)|~s_instance(s_Entity2_2,s_Object)),inference(spm,[status(thm)],[87136,49504,theory(equality)])).
;; cnf(168521,plain,($false|~s_instance(s_Entity2_2,s_Object)),inference(rw,[status(thm)],[168493,49510,theory(equality)])).
;; cnf(168522,plain,(~s_instance(s_Entity2_2,s_Object)),inference(cn,[status(thm)],[168521,theory(equality)])).
;; cnf(243133,plain,(s_instance(s_Entity2_2,s_Object)),inference(spm,[status(thm)],[63760,25443,theory(equality)])).
;; cnf(243198,plain,($false),inference(sr,[status(thm)],[243133,168522,theory(equality)])).
;; cnf(243199,plain,($false),243198,['proof']).