Sigma Proof

ar@leme workspace % echo $SIGMA_CP
/Users/ar/workspace/sigmakee/build/classes:/Users/ar/workspace/sigmakee/build/lib/*:/Users/ar/workspace/sigmakee/lib/*

ar@leme workspace % java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.InferenceTestSuite -t SP01.kif.tq
Info in KBmanager.initializeOnce()
Info in KBmanager.initializeOnce(): initializing with /Users/ar/.sigmakee/KBs
KBmanager.readConfiguration()
KBmanager.serializedExists(): true
KBmanager.serializedOld(config):
KBmanager.serializedOld(config): save date: Thu May 28 01:48:33 BRT 2020
kbsFilenamesFromXML(): Completed loading KB names
KBmanager.serializedOld(config): returning false (not old)
KBmanager.loadSerialized(): KBmanager has been deserialized
WordNet.initOnce(): disable: false
WordNet.initOnce(): using baseDir = /Users/ar/.sigmakee/KBs/WordNetMappings
WordNet.initOnce(): disable: false
WordNet.loadSerialized(): WN has been deserialized
INFO in WordNet.loadSerialized(): origMaxNounSynsetID: 15300051 maxNounSynsetID: 15300051
ENTER DB.readSpreadsheet(/Users/ar/.sigmakee/KBs/WordNetMappings/sentiment.csv, null)
ENTER DB.readSpreadsheet(java.io.FileReader@5f4da5c3, null)
EXIT DB.readSpreadsheet(java.io.FileReader@5f4da5c3, null)
  rows == [list of 8222 rows]
  0.163 seconds elapsed time
EXIT DB.readSpreadsheet(/Users/ar/.sigmakee/KBs/WordNetMappings/sentiment.csv, null)
NLGUtils.init(): initializing with /Users/ar/.sigmakee/KBs
NLGUtils.readKeywordMap():
NLGUtils.serializedExists(): true
NLGUtils.loadSerialized()
NLGUtils.loadSerialized(): NLGUtils has been deserialized
INFO in OMWordnet.readOMWfiles(): reading files:
OMWordnet.loadSerialized(): OMW has been deserialized
VerbNet.readVerbFiles(): loading files from:
VerbNet.readVerbFiles(): no such dir:
Info in KBmanager.initializeOnce(): initialized is true
KBmanager.initializeOnce(): total init time in seconds: 224
INFO in InferenceTestSuite.inferenceUnitTest(): testpath: /Users/ar/.sigmakee/KBs/tests/SP01.kif.tq
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (instance A Object)
KB.tell(): (instance A Object)
KB.tell: using vampire
INFO in Vampire.assertFormula(2):writing to file /Users/ar/.sigmakee/KBs/toplevel_UserAssertions.tptp
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_1,axiom,(( s__instance(s__A,s__Object) ))).
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_2,axiom,(( s__instance(s__Object,s__SetOrClass) ))).
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (note SP01)
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (orientation C B Left)
KB.tell(): (orientation C B Left)
KB.tell: using vampire
INFO in Vampire.assertFormula(2):writing to file /Users/ar/.sigmakee/KBs/toplevel_UserAssertions.tptp
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_3,axiom,(( s__orientation(s__C,s__B,s__Left) ))).
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (time 240)
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (instance B Object)
KB.tell(): (instance B Object)
KB.tell: using vampire
INFO in Vampire.assertFormula(2):writing to file /Users/ar/.sigmakee/KBs/toplevel_UserAssertions.tptp
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_4,axiom,(( s__instance(s__Object,s__SetOrClass) ))).
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_5,axiom,(( s__instance(s__B,s__Object) ))).
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (=> (and (orientation ?X ?Y ?R) (orientation ?Y ?Z ?R)) (orientation ?X ?Z ?R))
KB.tell(): (=>
  (and
    (orientation ?X ?Y ?R)
    (orientation ?Y ?Z ?R))
  (orientation ?X ?Z ?R))
KB.tell: using vampire
INFO in Vampire.assertFormula(2):writing to file /Users/ar/.sigmakee/KBs/toplevel_UserAssertions.tptp
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_6,axiom,(( ( ! [V__R,V__X,V__Y,V__Z] : (((s__instance(V__R,s__PositionalAttribute) & s__instance(V__X,s__Object) & s__instance(V__Y,s__Object) & s__instance(V__Z,s__Object)) => ((s__orientation(V__X,V__Y,V__R) & s__orientation(V__Y,V__Z,V__R)) => s__orientation(V__X,V__Z,V__R))) ) ) ))).
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (answer yes)
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (instance C Object)
KB.tell(): (instance C Object)
KB.tell: using vampire
INFO in Vampire.assertFormula(2):writing to file /Users/ar/.sigmakee/KBs/toplevel_UserAssertions.tptp
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_7,axiom,(( s__instance(s__Object,s__SetOrClass) ))).
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_8,axiom,(( s__instance(s__C,s__Object) ))).
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (orientation A B Right)
KB.tell(): (orientation A B Right)
KB.tell: using vampire
INFO in Vampire.assertFormula(2):writing to file /Users/ar/.sigmakee/KBs/toplevel_UserAssertions.tptp
INFO in Vampire.assertFormula(2): TPTP for user assertion = fof(kb_toplevel_UserAssertion_9,axiom,(( s__orientation(s__A,s__B,s__Right) ))).
INFO in InferenceTestSuite.inferenceUnitTest(): Formula: (query (orientation A C Right))
KBmanager.loadKBforInference(): KB: toplevel
KBmanager.loadKBforInference(): loading Vampire
INFO in KB.loadVampire()
INFO in InferenceTestSuite.inferenceUnitTest(): expected answers: [yes]

============================
InferenceTestSuite.inferenceUnitTest(): ask: (orientation A C Right)
KB.askVampire(): processed query: [(orientation A C Right)]
KB.askVampire(): calling with: /Users/ar/.sigmakee/KBs/toplevel.tptp, 240, [fof(query_0,conjecture,(( s__orientation(s__A,s__C,s__Right) ))).]
Vampire.run(): Initializing Vampire with:
[/Users/ar/workspace/vampire/vampire, --avatar, off, -qa, answer_literal, --mode, casc, --proof, tptp, -t, 240, /Users/ar/.sigmakee/KBs/temp-comb.tptp]
Vampire.run() done executing
InferenceTestSuite.inferenceUnitTest(): proof: WARNING Broken Constraint: if avatar_nonsplittable_components(none) is not default(known) then avatar(off) is equal to on
WARNING Broken Constraint: if avatar_delete_deactivated(large) is not default(on) then avatar(off) is equal to on
WARNING Broken Constraint: if split_at_activation(on) is not default(off) then avatar(off) is equal to on
WARNING Broken Constraint: if avatar_flush_period(40000) is not default(0) then avatar(off) is equal to on
WARNING Broken Constraint: if avatar_minimize_model(off) is not default(all) then avatar(off) is equal to on
WARNING Broken Constraint: if avatar_flush_quotient(1.4) is not default(1.5) then avatar(off) is equal to on
WARNING Broken Constraint: if avatar_fast_restart(on) is not default(off) then avatar(off) is equal to on
% lrs-4_5:1_add=large:afr=on:afp=40000:afq=1.4:amm=off:anc=none:bs=unit_only:bsr=on:irw=on:lcm=reverse:newcnf=on:nwc=1:stl=30:sd=3:ss=axioms:st=2.0:sos=on:sac=on:updr=off_4 on temp-comb
% Refutation found. Thanks to Tanya!
% SZS status Theorem for temp-comb
% SZS output start Proof for temp-comb
fof(f8163,plain,(
  $false),
  inference(unit_resulting_resolution,[],[f8162])).
fof(f8162,plain,(
  $false),
  inference(subsumption_resolution,[],[f8161,f7945])).
fof(f7945,plain,(
  s__instance(s__B,s__Object)),
  inference(cnf_transformation,[],[f7197])).
fof(f7197,axiom,(
  s__instance(s__B,s__Object)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_UserAssertion_4)).
fof(f8161,plain,(
  ~s__instance(s__B,s__Object)),
  inference(subsumption_resolution,[],[f8160,f7776])).
fof(f7776,plain,(
  s__orientation(s__C,s__B,s__Left)),
  inference(cnf_transformation,[],[f7188])).
fof(f7188,axiom,(
  s__orientation(s__C,s__B,s__Left)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_UserAssertion_2)).
fof(f8160,plain,(
  ~s__orientation(s__C,s__B,s__Left) | ~s__instance(s__B,s__Object)),
  inference(subsumption_resolution,[],[f8158,f7777])).
fof(f7777,plain,(
  s__instance(s__C,s__Object)),
  inference(cnf_transformation,[],[f7191])).
fof(f7191,axiom,(
  s__instance(s__C,s__Object)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_UserAssertion_7)).
fof(f8158,plain,(
  ~s__instance(s__C,s__Object) | ~s__orientation(s__C,s__B,s__Left) | ~s__instance(s__B,s__Object)),
  inference(resolution,[],[f8153,f7770])).
fof(f7770,plain,(
  ( ! [X0,X1] : (s__orientation(X0,X1,s__Right) | ~s__instance(X1,s__Object) | ~s__orientation(X1,X0,s__Left) | ~s__instance(X0,s__Object)) )),
  inference(cnf_transformation,[],[f7409])).
fof(f7409,plain,(
  ! [X0,X1] : (((s__orientation(X0,X1,s__Right) | ~s__orientation(X1,X0,s__Left)) & (s__orientation(X1,X0,s__Left) | ~s__orientation(X0,X1,s__Right))) | ~s__instance(X1,s__Object) | ~s__instance(X0,s__Object))),
  inference(flattening,[],[f7408])).
fof(f7408,plain,(
  ! [X0,X1] : (((s__orientation(X0,X1,s__Right) | ~s__orientation(X1,X0,s__Left)) & (s__orientation(X1,X0,s__Left) | ~s__orientation(X0,X1,s__Right))) | (~s__instance(X1,s__Object) | ~s__instance(X0,s__Object)))),
  inference(ennf_transformation,[],[f7208])).
fof(f7208,plain,(
  ! [X0,X1] : ((s__instance(X1,s__Object) & s__instance(X0,s__Object)) => ((s__orientation(X1,X0,s__Left) => s__orientation(X0,X1,s__Right)) & (s__orientation(X0,X1,s__Right) => s__orientation(X1,X0,s__Left))))),
  inference(rectify,[],[f116])).
fof(f116,axiom,(
  ! [X18,X19] : ((s__instance(X19,s__Object) & s__instance(X18,s__Object)) => ((s__orientation(X19,X18,s__Left) => s__orientation(X18,X19,s__Right)) & (s__orientation(X18,X19,s__Right) => s__orientation(X19,X18,s__Left))))),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_116)).
fof(f8153,plain,(
  ~s__orientation(s__B,s__C,s__Right)),
  inference(subsumption_resolution,[],[f8144,f7945])).
fof(f8144,plain,(
  ~s__orientation(s__B,s__C,s__Right) | ~s__instance(s__B,s__Object)),
  inference(resolution,[],[f8138,f7772])).
fof(f7772,plain,(
  s__orientation(s__A,s__B,s__Right)),
  inference(cnf_transformation,[],[f7196])).
fof(f7196,axiom,(
  s__orientation(s__A,s__B,s__Right)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_UserAssertion_8)).
fof(f8138,plain,(
  ( ! [X0] : (~s__orientation(s__A,X0,s__Right) | ~s__orientation(X0,s__C,s__Right) | ~s__instance(X0,s__Object)) )),
  inference(subsumption_resolution,[],[f8137,f7773])).
fof(f7773,plain,(
  s__instance(s__Right,s__PositionalAttribute)),
  inference(cnf_transformation,[],[f4799])).
fof(f4799,axiom,(
  s__instance(s__Right,s__PositionalAttribute)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_4799)).
fof(f8137,plain,(
  ( ! [X0] : (~s__instance(X0,s__Object) | ~s__orientation(s__A,X0,s__Right) | ~s__orientation(X0,s__C,s__Right) | ~s__instance(s__Right,s__PositionalAttribute)) )),
  inference(subsumption_resolution,[],[f8136,f7777])).
fof(f8136,plain,(
  ( ! [X0] : (~s__instance(X0,s__Object) | ~s__instance(s__C,s__Object) | ~s__orientation(s__A,X0,s__Right) | ~s__orientation(X0,s__C,s__Right) | ~s__instance(s__Right,s__PositionalAttribute)) )),
  inference(subsumption_resolution,[],[f8133,f7778])).
fof(f7778,plain,(
  s__instance(s__A,s__Object)),
  inference(cnf_transformation,[],[f7195])).
fof(f7195,axiom,(
  s__instance(s__A,s__Object)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_UserAssertion_0)).
fof(f8133,plain,(
  ( ! [X0] : (~s__instance(s__A,s__Object) | ~s__instance(X0,s__Object) | ~s__instance(s__C,s__Object) | ~s__orientation(s__A,X0,s__Right) | ~s__orientation(X0,s__C,s__Right) | ~s__instance(s__Right,s__PositionalAttribute)) )),
  inference(resolution,[],[f7761,f7769])).
fof(f7769,plain,(
  ( ! [X2,X0,X3,X1] : (s__orientation(X1,X3,X0) | ~s__instance(X1,s__Object) | ~s__instance(X2,s__Object) | ~s__instance(X3,s__Object) | ~s__orientation(X1,X2,X0) | ~s__orientation(X2,X3,X0) | ~s__instance(X0,s__PositionalAttribute)) )),
  inference(cnf_transformation,[],[f7407])).
fof(f7407,plain,(
  ! [X0,X1,X2,X3] : (s__orientation(X1,X3,X0) | ~s__orientation(X2,X3,X0) | ~s__orientation(X1,X2,X0) | ~s__instance(X3,s__Object) | ~s__instance(X2,s__Object) | ~s__instance(X1,s__Object) | ~s__instance(X0,s__PositionalAttribute))),
  inference(flattening,[],[f7406])).
fof(f7406,plain,(
  ! [X0,X1,X2,X3] : ((s__orientation(X1,X3,X0) | (~s__orientation(X2,X3,X0) | ~s__orientation(X1,X2,X0))) | (~s__instance(X3,s__Object) | ~s__instance(X2,s__Object) | ~s__instance(X1,s__Object) | ~s__instance(X0,s__PositionalAttribute)))),
  inference(ennf_transformation,[],[f7207])).
fof(f7207,plain,(
  ! [X0,X1,X2,X3] : ((s__instance(X3,s__Object) & s__instance(X2,s__Object) & s__instance(X1,s__Object) & s__instance(X0,s__PositionalAttribute)) => ((s__orientation(X2,X3,X0) & s__orientation(X1,X2,X0)) => s__orientation(X1,X3,X0)))),
  inference(rectify,[],[f7190])).
fof(f7190,axiom,(
  ! [X141,X71,X174,X352] : ((s__instance(X352,s__Object) & s__instance(X174,s__Object) & s__instance(X71,s__Object) & s__instance(X141,s__PositionalAttribute)) => ((s__orientation(X174,X352,X141) & s__orientation(X71,X174,X141)) => s__orientation(X71,X352,X141)))),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_UserAssertion_5)).
fof(f7761,plain,(
  ~s__orientation(s__A,s__C,s__Right)),
  inference(cnf_transformation,[],[f7199])).
fof(f7199,plain,(
  ~s__orientation(s__A,s__C,s__Right)),
  inference(flattening,[],[f7194])).
fof(f7194,negated_conjecture,(
  ~s__orientation(s__A,s__C,s__Right)),
  inference(negated_conjecture,[],[f7193])).
fof(f7193,conjecture,(
  s__orientation(s__A,s__C,s__Right)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',query_0)).
% SZS output end Proof for temp-comb
% ------------------------------
% Version: Vampire 4.4.0 (commit 3dd0ed0c on 2020-02-04 14:57:07 +0100)
% Termination reason: Refutation

% Memory used [KB]: 7419
% Time elapsed: 0.021 s
% ------------------------------
% ------------------------------
% Success in time 0.154 s

Error in TPTP3ProofProcessor.parseSupports() no id: null for premises at step f7777
Error in TPTP3ProofProcessor.parseSupports() no id: null for premises at step f7945
InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: [1. (not
  (orientation A C Right)) [] negated_conjecture
, 2. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4)
  (=>
    (and
      (and
        (and
          (instance ?VAR4 Object)
          (instance ?VAR3 Object))
        (instance ?VAR2 Object))
      (instance ?VAR1 PositionalAttribute))
    (=>
      (and
        (orientation ?VAR3 ?VAR4 ?VAR1)
        (orientation ?VAR2 ?VAR3 ?VAR1))
      (orientation ?VAR2 ?VAR4 ?VAR1)))) [] kb_toplevel_UserAssertion_5
, 3. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4)
  (or
    (or
      (orientation ?VAR2 ?VAR4 ?VAR1)
      (not
        (orientation ?VAR3 ?VAR4 ?VAR1))
      (not
        (orientation ?VAR2 ?VAR3 ?VAR1)))
    (or
      (or
        (not
          (instance ?VAR4 Object))
        (not
          (instance ?VAR3 Object)))
      (not
        (instance ?VAR2 Object)))
    (not
      (instance ?VAR1 PositionalAttribute)))) [2] ennf_transformation
, 4. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4)
  (or
    (or
      (or
        (or
          (or
            (or
              (orientation ?VAR2 ?VAR4 ?VAR1)
              (not
                (orientation ?VAR3 ?VAR4 ?VAR1)))
            (not
              (orientation ?VAR2 ?VAR3 ?VAR1)))
          (not
            (instance ?VAR4 Object)))
        (not
          (instance ?VAR3 Object)))
      (not
        (instance ?VAR2 Object)))
    (not
      (instance ?VAR1 PositionalAttribute)))) [3] flattening
, 5. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4)
  (or
    (or
      (or
        (or
          (or
            (or
              (orientation ?VAR4 ?VAR3 ?VAR2)
              (not
                (instance ?VAR4 Object)))
            (not
              (instance ?VAR1 Object)))
          (not
            (instance ?VAR3 Object)))
        (not
          (orientation ?VAR4 ?VAR1 ?VAR2)))
      (not
        (orientation ?VAR1 ?VAR3 ?VAR2)))
    (not
      (instance ?VAR2 PositionalAttribute)))) [4] cnf_transformation
, 6. (forall (?VAR1)
  (or
    (or
      (or
        (or
          (or
            (not
              (instance A Object))
            (not
              (instance ?VAR1 Object)))
          (not
            (instance C Object)))
        (not
          (orientation A ?VAR1 Right)))
      (not
        (orientation ?VAR1 C Right)))
    (not
      (instance Right PositionalAttribute)))) [1, 5] resolution
, 7. (instance A Object) [] kb_toplevel_UserAssertion_0
, 8. (forall (?VAR1)
  (or
    (or
      (or
        (or
          (not
            (instance ?VAR1 Object))
          (not
            (instance C Object)))
        (not
          (orientation A ?VAR1 Right)))
      (not
        (orientation ?VAR1 C Right)))
    (not
      (instance Right PositionalAttribute)))) [6, 7] subsumption_resolution
, 9. (forall (?VAR1)
  (or
    (or
      (or
        (not
          (instance ?VAR1 Object))
        (not
          (orientation A ?VAR1 Right)))
      (not
        (orientation ?VAR1 C Right)))
    (not
      (instance Right PositionalAttribute)))) [8] subsumption_resolution
, 10. (instance Right PositionalAttribute) [] kb_toplevel_4799
, 11. (forall (?VAR1)
  (or
    (or
      (not
        (orientation A ?VAR1 Right))
      (not
        (orientation ?VAR1 C Right)))
    (not
      (instance ?VAR1 Object)))) [9, 10] subsumption_resolution
, 12. (orientation A B Right) [] kb_toplevel_UserAssertion_8
, 13. (or
  (not
    (orientation B C Right))
  (not
    (instance B Object))) [11, 12] resolution
, 14. (not
  (orientation B C Right)) [13] subsumption_resolution
, 15. (forall (?VAR1 ?VAR2)
  (=>
    (and
      (instance ?VAR2 Object)
      (instance ?VAR1 Object))
    (and
      (=>
        (orientation ?VAR2 ?VAR1 Left)
        (orientation ?VAR1 ?VAR2 Right))
      (=>
        (orientation ?VAR1 ?VAR2 Right)
        (orientation ?VAR2 ?VAR1 Left))))) [] kb_toplevel_116
, 16. (forall (?VAR1 ?VAR2)
  (or
    (and
      (or
        (orientation ?VAR1 ?VAR2 Right)
        (not
          (orientation ?VAR2 ?VAR1 Left)))
      (or
        (orientation ?VAR2 ?VAR1 Left)
        (not
          (orientation ?VAR1 ?VAR2 Right))))
    (not
      (instance ?VAR2 Object))
    (not
      (instance ?VAR1 Object)))) [15] ennf_transformation
, 17. (forall (?VAR1 ?VAR2)
  (or
    (or
      (and
        (or
          (orientation ?VAR1 ?VAR2 Right)
          (not
            (orientation ?VAR2 ?VAR1 Left)))
        (or
          (orientation ?VAR2 ?VAR1 Left)
          (not
            (orientation ?VAR1 ?VAR2 Right))))
      (not
        (instance ?VAR2 Object)))
    (not
      (instance ?VAR1 Object)))) [16] flattening
, 18. (forall (?VAR1 ?VAR2)
  (or
    (or
      (or
        (orientation ?VAR1 ?VAR2 Right)
        (not
          (instance ?VAR2 Object)))
      (not
        (orientation ?VAR2 ?VAR1 Left)))
    (not
      (instance ?VAR1 Object)))) [17] cnf_transformation
, 19. (or
  (or
    (not
      (instance C Object))
    (not
      (orientation C B Left)))
  (not
    (instance B Object))) [14, 18] resolution
, 20. (instance C Object) [] kb_toplevel_UserAssertion_7
, 21. (or
  (not
    (orientation C B Left))
  (not
    (instance B Object))) [19, 20] subsumption_resolution
, 22. (orientation C B Left) [] kb_toplevel_UserAssertion_2
, 23. (not
  (instance B Object)) [21, 22] subsumption_resolution
, 24. (instance B Object) [] kb_toplevel_UserAssertion_4
, 25. false [23, 24] subsumption_resolution
]
InferenceTestSuite.inferenceUnitTest(): answers: []
InferenceTestSuite.inferenceUnitTest(): tpp status: Theorem for temp-comb

============================
InferenceTestSuite.cmdLineTest() : Success on SP01.kif.tq
ar@leme workspace %