search

ontologyportal / sigmakee

Sigma Knowledge Engineering Environment
GNU General Public License v3.0
101 stars 34 forks source link

Vampire proves both (subclass A B) and (not (subclass A B)) , same for instance on Merge.kif #69

Open kharus opened 4 years ago

kharus commented 4 years ago

Vampire derives that something is both subclass of another thing and not subclass of the same another thing.

  <kb name="SUMO" >
    <constituent filename="Merge.kif" />
  </kb>

I use RealNumber and Fish but it seems to work on anything.

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -av \
"(subclass RealNumber Fish)"
...
KB.main(): proof: [1. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5)
  (=>
    (and
      (and
        (and
          (subclass ?VAR4 Attribute)
          (instance ?VAR3 Attribute)
...

then negation

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -av \
"(not (subclass RealNumber Fish))"
...
KB.main(): proof: [1. (forall (?VAR1)
  (and
    (=>
      (exists (?VAR2)
        (and
          (and
...

And also together

 $JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -av \
"(and (not (subclass RealNumber Fish)) (subclass RealNumber Fish))"
...
KB.main(): proof: [1. (forall (?VAR1)
  (and
    (=>
      (exists (?VAR2)
        (and
          (and
...

same for the instance

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -av \
"(and (not (instance RealNumber Fish)) (instance RealNumber Fish))"
...
KB.main(): proof: [1. (forall (?VAR1)
  (and
    (=>
      (exists (?VAR2)
...

E works as expected: RealNumber is neither subclass nor instance of Fish

I tried both vampire from head and also pre-compiled binary vampire 4.5.1

arademaker commented 4 years ago

I got refutation for both (subclass RealNumber Number) and (subclass RealNumber Fish). But I believe this should bew reported it in the SUMO repository.

% java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.KB -av "(subclass RealNumber Number)"
...
KB.askVampire(): processed query: [(subclass RealNumber Number)]
KB.askVampire(): calling with: /Users/ar/.sigmakee/KBs/toplevel.tptp, 30, [fof(query_0,conjecture,(( s__subclass(s__RealNumber,s__Number) ))).]
Vampire.run(): Initializing Vampire with:
[/Users/ar/workspace/vampire/vampire, --avatar, off, -qa, answer_literal, --mode, casc, --proof, tptp, -t, 30, /Users/ar/.sigmakee/KBs/temp-comb.tptp]
Vampire.run() done executing
...
% Refutation found. Thanks to Tanya!
% SZS status Theorem for temp-comb
% SZS output start Proof for temp-comb
fof(f14696,plain,(
  $false),
  inference(unit_resulting_resolution,[],[f14695])).
fof(f14695,plain,(
  $false),
  inference(subsumption_resolution,[],[f14614,f14618])).
fof(f14618,plain,(
  s__subclass(s__RealNumber,s__Number)),
  inference(cnf_transformation,[],[f13065])).
fof(f13065,axiom,(
  s__subclass(s__RealNumber,s__Number)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_13065)).
fof(f14614,plain,(
  ~s__subclass(s__RealNumber,s__Number)),
  inference(cnf_transformation,[],[f14592])).
fof(f14592,plain,(
  ~s__subclass(s__RealNumber,s__Number)),
  inference(flattening,[],[f14591])).
fof(f14591,negated_conjecture,(
  ~s__subclass(s__RealNumber,s__Number)),
  inference(negated_conjecture,[],[f14590])).
fof(f14590,conjecture,(
  s__subclass(s__RealNumber,s__Number)),
  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]: 8955
% Time elapsed: 0.023 s
% ------------------------------
% ------------------------------
% Success in time 0.198 s
KB.main(): bindings: []
KB.main(): proof: [1. (not
  (subclass RealNumber Number)) [] negated_conjecture
, 2. (subclass RealNumber Number) [] kb_toplevel_13065
, 3. false [1, 2] subsumption_resolution]

% java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.KB -av "(subclass RealNumber Fish)"
...
KB.askVampire(): processed query: [(subclass RealNumber Fish)]
...
lrs+1010_3:2_afr=on:afp=100000:afq=1.1:anc=none:gsp=input_only:irw=on:lwlo=on:nm=2:newcnf=on:nwc=1.7:sac=on:sp=occurrence_300 on temp-comb
% Refutation found. Thanks to Tanya!
% SZS status Theorem for temp-comb
% SZS output start Proof for temp-comb
fof(f115440,plain,(
  $false),
  inference(unit_resulting_resolution,[],[f115439])).
fof(f115439,plain,(
  $false),
  inference(subsumption_resolution,[],[f115438,f78947])).
fof(f78947,plain,(
  sP1099),
  inference(subsumption_resolution,[],[f78945,f72124])).
fof(f72124,plain,(
  ( ! [X0] : (sP1098(X0)) )),
  inference(subsumption_resolution,[],[f65618,f53973])).
fof(f53973,plain,(
  ( ! [X0] : (s__subclass(s__RealNumber,X0) | sP1098(X0)) )),
  inference(superposition,[],[f29173,f41088])).
fof(f41088,plain,(
  ( ! [X6,X0] : (X0 = X6 | sP1098(X0)) )),
  inference(cnf_transformation,[],[f41088_D])).
fof(f41088_D,plain,(
  ( ! [X0] : (( ! [X6] : X0 = X6 ) <=> ~sP1098(X0)) )),
  introduced(general_splitting_component_introduction,[new_symbols(naming,[sP1098])])).
fof(f29173,plain,(
  s__subclass(s__RealNumber,s__Quantity)),
  inference(cnf_transformation,[],[f13066])).
fof(f13066,axiom,(
  s__subclass(s__RealNumber,s__Quantity)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_13066)).
fof(f65618,plain,(
  ( ! [X0] : (~s__subclass(s__RealNumber,X0) | sP1098(X0)) )),
  inference(superposition,[],[f24409,f41088])).
fof(f24409,plain,(
  ~s__subclass(s__RealNumber,s__Fish)),
  inference(cnf_transformation,[],[f14592])).
fof(f14592,plain,(
  ~s__subclass(s__RealNumber,s__Fish)),
  inference(flattening,[],[f14591])).
fof(f14591,negated_conjecture,(
  ~s__subclass(s__RealNumber,s__Fish)),
  inference(negated_conjecture,[],[f14590])).
fof(f14590,conjecture,(
  s__subclass(s__RealNumber,s__Fish)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',query_0)).
fof(f78945,plain,(
  ( ! [X0] : (~sP1098(sK21(X0)) | sP1099) )),
  inference(resolution,[],[f41090,f41558])).
fof(f41558,plain,(
  ( ! [X0] : (s__instance(sK21(X0),s__PositiveInteger)) )),
  inference(subsumption_resolution,[],[f41557,f33903])).
fof(f33903,plain,(
  s__instance(s__immediateInstance__m,s__Predicate)),
  inference(cnf_transformation,[],[f7819])).
fof(f7819,axiom,(
  s__instance(s__immediateInstance__m,s__Predicate)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_7819)).
fof(f41557,plain,(
  ( ! [X0] : (~s__instance(s__immediateInstance__m,s__Predicate) | s__instance(sK21(X0),s__PositiveInteger)) )),
  inference(subsumption_resolution,[],[f35816,f33878])).
fof(f33878,plain,(
  s__instance(s__immediateInstance__m,s__TotalValuedRelation)),
  inference(cnf_transformation,[],[f7821])).
fof(f7821,axiom,(
  s__instance(s__immediateInstance__m,s__TotalValuedRelation)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_7821)).
fof(f35816,plain,(
  ( ! [X0] : (~s__instance(s__immediateInstance__m,s__TotalValuedRelation) | ~s__instance(s__immediateInstance__m,s__Predicate) | s__instance(sK21(X0),s__PositiveInteger)) )),
  inference(cnf_transformation,[],[f19560])).
fof(f19560,plain,(
  ! [X0] : (((s__instance(s__immediateInstance__m,s__Predicate) & s__instance(s__immediateInstance__m,s__TotalValuedRelation)) | ! [X1] : ((! [X5] : ~s__immediateInstance(X0,X5) & ! [X2,X3,X4] : (s__instance(X3,X4) | s__ListOrderFn(s__ListFn__1Fn(X0),X2) != X3 | ~s__domain(s__immediateInstance__m,X2,X4) | ~s__lessThan(X2,X1) | ~s__instance(X4,s__SetOrClass) | ~s__instance(X2,s__PositiveInteger))) | ~s__valence(s__immediateInstance__m,X1) | ~s__instance(s__immediateInstance__m,s__Relation) | ~s__instance(X1,s__PositiveInteger))) & (? [X6] : ((? [X10] : s__immediateInstance(X0,X10) | ? [X7,X8,X9] : (~s__instance(X8,X9) & s__ListOrderFn(s__ListFn__1Fn(X0),X7) = X8 & s__domain(s__immediateInstance__m,X7,X9) & s__lessThan(X7,X6) & s__instance(X9,s__SetOrClass) & s__instance(X7,s__PositiveInteger))) & s__valence(s__immediateInstance__m,X6) & s__instance(s__immediateInstance__m,s__Relation) & s__instance(X6,s__PositiveInteger)) | ~s__instance(s__immediateInstance__m,s__Predicate) | ~s__instance(s__immediateInstance__m,s__TotalValuedRelation)))),
  inference(flattening,[],[f19559])).
fof(f19559,plain,(
  ! [X0] : (((s__instance(s__immediateInstance__m,s__Predicate) & s__instance(s__immediateInstance__m,s__TotalValuedRelation)) | ! [X1] : ((! [X5] : ~s__immediateInstance(X0,X5) & ! [X2,X3,X4] : ((s__instance(X3,X4) | (s__ListOrderFn(s__ListFn__1Fn(X0),X2) != X3 | ~s__domain(s__immediateInstance__m,X2,X4) | ~s__lessThan(X2,X1))) | (~s__instance(X4,s__SetOrClass) | ~s__instance(X2,s__PositiveInteger)))) | ~s__valence(s__immediateInstance__m,X1) | ~s__instance(s__immediateInstance__m,s__Relation) | ~s__instance(X1,s__PositiveInteger))) & (? [X6] : ((? [X10] : s__immediateInstance(X0,X10) | ? [X7,X8,X9] : ((~s__instance(X8,X9) & (s__ListOrderFn(s__ListFn__1Fn(X0),X7) = X8 & s__domain(s__immediateInstance__m,X7,X9) & s__lessThan(X7,X6))) & (s__instance(X9,s__SetOrClass) & s__instance(X7,s__PositiveInteger)))) & s__valence(s__immediateInstance__m,X6) & s__instance(s__immediateInstance__m,s__Relation) & s__instance(X6,s__PositiveInteger)) | (~s__instance(s__immediateInstance__m,s__Predicate) | ~s__instance(s__immediateInstance__m,s__TotalValuedRelation))))),
  inference(ennf_transformation,[],[f14974])).
fof(f14974,plain,(
  ! [X0] : ((? [X1] : ((! [X2,X3,X4] : ((s__instance(X4,s__SetOrClass) & s__instance(X2,s__PositiveInteger)) => ((s__ListOrderFn(s__ListFn__1Fn(X0),X2) = X3 & s__domain(s__immediateInstance__m,X2,X4) & s__lessThan(X2,X1)) => s__instance(X3,X4))) => ? [X5] : s__immediateInstance(X0,X5)) & s__valence(s__immediateInstance__m,X1) & s__instance(s__immediateInstance__m,s__Relation) & s__instance(X1,s__PositiveInteger)) => (s__instance(s__immediateInstance__m,s__Predicate) & s__instance(s__immediateInstance__m,s__TotalValuedRelation))) & ((s__instance(s__immediateInstance__m,s__Predicate) & s__instance(s__immediateInstance__m,s__TotalValuedRelation)) => ? [X6] : ((! [X7,X8,X9] : ((s__instance(X9,s__SetOrClass) & s__instance(X7,s__PositiveInteger)) => ((s__ListOrderFn(s__ListFn__1Fn(X0),X7) = X8 & s__domain(s__immediateInstance__m,X7,X9) & s__lessThan(X7,X6)) => s__instance(X8,X9))) => ? [X10] : s__immediateInstance(X0,X10)) & s__valence(s__immediateInstance__m,X6) & s__instance(s__immediateInstance__m,s__Relation) & s__instance(X6,s__PositiveInteger))))),
  inference(rectify,[],[f11])).
fof(f11,axiom,(
  ! [X9] : ((? [X10] : ((! [X11,X12,X13] : ((s__instance(X13,s__SetOrClass) & s__instance(X11,s__PositiveInteger)) => ((s__ListOrderFn(s__ListFn__1Fn(X9),X11) = X12 & s__domain(s__immediateInstance__m,X11,X13) & s__lessThan(X11,X10)) => s__instance(X12,X13))) => ? [X14] : s__immediateInstance(X9,X14)) & s__valence(s__immediateInstance__m,X10) & s__instance(s__immediateInstance__m,s__Relation) & s__instance(X10,s__PositiveInteger)) => (s__instance(s__immediateInstance__m,s__Predicate) & s__instance(s__immediateInstance__m,s__TotalValuedRelation))) & ((s__instance(s__immediateInstance__m,s__Predicate) & s__instance(s__immediateInstance__m,s__TotalValuedRelation)) => ? [X10] : ((! [X11,X12,X13] : ((s__instance(X13,s__SetOrClass) & s__instance(X11,s__PositiveInteger)) => ((s__ListOrderFn(s__ListFn__1Fn(X9),X11) = X12 & s__domain(s__immediateInstance__m,X11,X13) & s__lessThan(X11,X10)) => s__instance(X12,X13))) => ? [X14] : s__immediateInstance(X9,X14)) & s__valence(s__immediateInstance__m,X10) & s__instance(s__immediateInstance__m,s__Relation) & s__instance(X10,s__PositiveInteger))))),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_11)).
fof(f41090,plain,(
  ( ! [X0] : (~s__instance(X0,s__PositiveInteger) | ~sP1098(X0) | sP1099) )),
  inference(cnf_transformation,[],[f41090_D])).
fof(f41090_D,plain,(
  ( ! [X0] : (~s__instance(X0,s__PositiveInteger) | ~sP1098(X0)) ) <=> ~sP1099),
  introduced(general_splitting_component_introduction,[new_symbols(naming,[sP1099])])).
fof(f115438,plain,(
  ~sP1099),
  inference(subsumption_resolution,[],[f115437,f31321])).
fof(f31321,plain,(
  s__instance(s__Dead,s__Attribute)),
  inference(cnf_transformation,[],[f4824])).
fof(f4824,axiom,(
  s__instance(s__Dead,s__Attribute)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_4824)).
fof(f115437,plain,(
  ~s__instance(s__Dead,s__Attribute) | ~sP1099),
  inference(subsumption_resolution,[],[f115436,f26476])).
fof(f26476,plain,(
  s__subclass(s__AnimacyAttribute,s__Attribute)),
  inference(cnf_transformation,[],[f9561])).
fof(f9561,axiom,(
  s__subclass(s__AnimacyAttribute,s__Attribute)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_9561)).
fof(f115436,plain,(
  ~s__subclass(s__AnimacyAttribute,s__Attribute) | ~s__instance(s__Dead,s__Attribute) | ~sP1099),
  inference(subsumption_resolution,[],[f115433,f30848])).
fof(f30848,plain,(
  s__instance(s__Living,s__Attribute)),
  inference(cnf_transformation,[],[f5476])).
fof(f5476,axiom,(
  s__instance(s__Living,s__Attribute)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_5476)).
fof(f115433,plain,(
  ~s__instance(s__Living,s__Attribute) | ~s__subclass(s__AnimacyAttribute,s__Attribute) | ~s__instance(s__Dead,s__Attribute) | ~sP1099),
  inference(resolution,[],[f41091,f34627])).
fof(f34627,plain,(
  s__exhaustiveAttribute__3(s__AnimacyAttribute,s__Living,s__Dead)),
  inference(cnf_transformation,[],[f4381])).
fof(f4381,axiom,(
  s__exhaustiveAttribute__3(s__AnimacyAttribute,s__Living,s__Dead)),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_4381)).
fof(f41091,plain,(
  ( ! [X2,X3,X1] : (~s__exhaustiveAttribute__3(X3,X2,X1) | ~s__instance(X2,s__Attribute) | ~s__subclass(X3,s__Attribute) | ~s__instance(X1,s__Attribute) | ~sP1099) )),
  inference(general_splitting,[],[f41089,f41090_D])).
fof(f41089,plain,(
  ( ! [X2,X0,X3,X1] : (~s__instance(X0,s__PositiveInteger) | ~s__instance(X1,s__Attribute) | ~s__instance(X2,s__Attribute) | ~s__subclass(X3,s__Attribute) | ~s__exhaustiveAttribute__3(X3,X2,X1) | ~sP1098(X0)) )),
  inference(general_splitting,[],[f40276,f41088_D])).
fof(f40276,plain,(
  ( ! [X6,X2,X0,X3,X1] : (~s__instance(X0,s__PositiveInteger) | ~s__instance(X1,s__Attribute) | ~s__instance(X2,s__Attribute) | ~s__subclass(X3,s__Attribute) | ~s__exhaustiveAttribute__3(X3,X2,X1) | X0 = X6) )),
  inference(equality_resolution,[],[f40275])).
fof(f40275,plain,(
  ( ! [X6,X2,X0,X5,X3,X1] : (~s__instance(X0,s__PositiveInteger) | ~s__instance(X1,s__Attribute) | ~s__instance(X2,s__Attribute) | ~s__subclass(X3,s__Attribute) | ~s__exhaustiveAttribute__3(X3,X2,X1) | s__ListOrderFn(s__ListFn__2Fn(X2,X1),X0) != X5 | X0 = X6) )),
  inference(equality_resolution,[],[f39711])).
fof(f39711,plain,(
  ( ! [X6,X4,X2,X0,X5,X3,X1] : (~s__instance(X0,s__PositiveInteger) | ~s__instance(X1,s__Attribute) | ~s__instance(X2,s__Attribute) | ~s__subclass(X3,s__Attribute) | ~s__exhaustiveAttribute__3(X3,X2,X1) | s__ListOrderFn(s__ListFn__2Fn(X2,X1),X0) != X4 | X4 != X5 | X0 = X6) )),
  inference(cnf_transformation,[],[f24014])).
fof(f24014,plain,(
  ! [X0,X1,X2,X3,X4] : (! [X5,X6] : (X0 = X6 | X4 != X5) | s__ListOrderFn(s__ListFn__2Fn(X2,X1),X0) != X4 | ~s__exhaustiveAttribute__3(X3,X2,X1) | ~s__subclass(X3,s__Attribute) | ~s__instance(X2,s__Attribute) | ~s__instance(X1,s__Attribute) | ~s__instance(X0,s__PositiveInteger))),
  inference(flattening,[],[f24013])).
fof(f24013,plain,(
  ! [X0,X1,X2,X3,X4] : (((! [X5,X6] : (X0 = X6 | X4 != X5) | s__ListOrderFn(s__ListFn__2Fn(X2,X1),X0) != X4) | ~s__exhaustiveAttribute__3(X3,X2,X1)) | (~s__subclass(X3,s__Attribute) | ~s__instance(X2,s__Attribute) | ~s__instance(X1,s__Attribute) | ~s__instance(X0,s__PositiveInteger)))),
  inference(ennf_transformation,[],[f17809])).
fof(f17809,plain,(
  ! [X0,X1,X2,X3,X4] : ((s__subclass(X3,s__Attribute) & s__instance(X2,s__Attribute) & s__instance(X1,s__Attribute) & s__instance(X0,s__PositiveInteger)) => (s__exhaustiveAttribute__3(X3,X2,X1) => (s__ListOrderFn(s__ListFn__2Fn(X2,X1),X0) = X4 => ~? [X5,X6] : (X0 != X6 & X4 = X5))))),
  inference(rectify,[],[f2862])).
fof(f2862,axiom,(
  ! [X172,X15,X9,X13,X329] : ((s__subclass(X13,s__Attribute) & s__instance(X9,s__Attribute) & s__instance(X15,s__Attribute) & s__instance(X172,s__PositiveInteger)) => (s__exhaustiveAttribute__3(X13,X9,X15) => (s__ListOrderFn(s__ListFn__2Fn(X9,X15),X172) = X329 => ~? [X330,X173] : (X172 != X173 & X329 = X330))))),
  file('/Users/ar/.sigmakee/KBs/temp-comb.tptp',kb_toplevel_2862)).
% 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]: 52323
% Time elapsed: 1.267 s
% ------------------------------
% ------------------------------
% Success in time 25.874 s
KB.main(): bindings: []
KB.main(): proof: [1. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5)
  (=>
    (and
      (and
        (and
          (subclass ?VAR4 Attribute)
          (instance ?VAR3 Attribute))
        (instance ?VAR2 Attribute))
      (instance ?VAR1 PositiveInteger))
    (=>
      (exhaustiveAttribute__3 ?VAR4 ?VAR3 ?VAR2)
      (=>
        (=
          (ListOrderFn
            (ListFn__2Fn ?VAR3 ?VAR2) ?VAR1) ?VAR5)
        (not
          (exists (?VAR6 ?VAR7)
            (and
              (not
                (= ?VAR1 ?VAR7))
              (= ?VAR5 ?VAR6)))))))) [] kb_toplevel_2862
, 2. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5)
  (or
    (or
      (or
        (forall (?VAR6 ?VAR7)
          (or
            (= ?VAR1 ?VAR7)
            (not
              (= ?VAR5 ?VAR6))))
        (not
          (=
            (ListOrderFn
              (ListFn__2Fn ?VAR3 ?VAR2) ?VAR1) ?VAR5)))
      (not
        (exhaustiveAttribute__3 ?VAR4 ?VAR3 ?VAR2)))
    (or
      (or
        (not
          (subclass ?VAR4 Attribute))
        (not
          (instance ?VAR3 Attribute)))
      (not
        (instance ?VAR2 Attribute)))
    (not
      (instance ?VAR1 PositiveInteger)))) [1] ennf_transformation
, 3. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5)
  (or
    (or
      (or
        (or
          (or
            (or
              (forall (?VAR6 ?VAR7)
                (or
                  (= ?VAR1 ?VAR7)
                  (not
                    (= ?VAR5 ?VAR6))))
              (not
                (=
                  (ListOrderFn
                    (ListFn__2Fn ?VAR3 ?VAR2) ?VAR1) ?VAR5)))
            (not
              (exhaustiveAttribute__3 ?VAR4 ?VAR3 ?VAR2)))
          (not
            (subclass ?VAR4 Attribute)))
        (not
          (instance ?VAR3 Attribute)))
      (not
        (instance ?VAR2 Attribute)))
    (not
      (instance ?VAR1 PositiveInteger)))) [2] flattening
, 4. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5 ?VAR6 ?VAR7)
  (or
    (or
      (or
        (or
          (or
            (or
              (or
                (not
                  (instance ?VAR4 PositiveInteger))
                (not
                  (instance ?VAR7 Attribute)))
              (not
                (instance ?VAR3 Attribute)))
            (not
              (subclass ?VAR6 Attribute)))
          (not
            (exhaustiveAttribute__3 ?VAR6 ?VAR3 ?VAR7)))
        (not
          (=
            (ListOrderFn
              (ListFn__2Fn ?VAR3 ?VAR7) ?VAR4) ?VAR2)))
      (not
        (= ?VAR2 ?VAR5)))
    (= ?VAR4 ?VAR1))) [3] cnf_transformation
, 5. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5 ?VAR6)
  (or
    (or
      (or
        (or
          (or
            (or
              (not
                (instance ?VAR3 PositiveInteger))
              (not
                (instance ?VAR6 Attribute)))
            (not
              (instance ?VAR2 Attribute)))
          (not
            (subclass ?VAR5 Attribute)))
        (not
          (exhaustiveAttribute__3 ?VAR5 ?VAR2 ?VAR6)))
      (not
        (=
          (ListOrderFn
            (ListFn__2Fn ?VAR2 ?VAR6) ?VAR3) ?VAR4)))
    (= ?VAR3 ?VAR1))) [4] equality_resolution
, 6. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4 ?VAR5)
  (or
    (or
      (or
        (or
          (or
            (not
              (instance ?VAR3 PositiveInteger))
            (not
              (instance ?VAR5 Attribute)))
          (not
            (instance ?VAR2 Attribute)))
        (not
          (subclass ?VAR4 Attribute)))
      (not
        (exhaustiveAttribute__3 ?VAR4 ?VAR2 ?VAR5)))
    (= ?VAR3 ?VAR1))) [5] equality_resolution
, 7. (forall (?VAR1 ?VAR2 ?VAR3 ?VAR4)
  (or
    (or
      (or
        (or
          (or
            (not
              (instance ?VAR2 PositiveInteger))
            (not
              (instance ?VAR4 Attribute)))
          (not
            (instance ?VAR1 Attribute)))
        (not
          (subclass ?VAR3 Attribute)))
      (not
        (exhaustiveAttribute__3 ?VAR3 ?VAR1 ?VAR4)))
    (not
      (sP1098 ?VAR2)))) [6, 9] general_splitting
, 8. (forall (?VAR1 ?VAR2 ?VAR3)
  (or
    (or
      (or
        (or
          (not
            (exhaustiveAttribute__3 ?VAR2 ?VAR1 ?VAR3))
          (not
            (instance ?VAR1 Attribute)))
        (not
          (subclass ?VAR2 Attribute)))
      (not
        (instance ?VAR3 Attribute)))
    (not sP1099))) [7, 9] general_splitting
, 9. (exhaustiveAttribute__3 AnimacyAttribute Living Dead) [] kb_toplevel_4381
, 10. (or
  (or
    (or
      (not
        (instance Living Attribute))
      (not
        (subclass AnimacyAttribute Attribute)))
    (not
      (instance Dead Attribute)))
  (not sP1099)) [8, 9] resolution
, 11. (instance Living Attribute) [] kb_toplevel_5476
, 12. (or
  (or
    (not
      (subclass AnimacyAttribute Attribute))
    (not
      (instance Dead Attribute)))
  (not sP1099)) [10, 11] subsumption_resolution
, 13. (subclass AnimacyAttribute Attribute) [] kb_toplevel_9561
, 14. (or
  (not
    (instance Dead Attribute))
  (not sP1099)) [12, 13] subsumption_resolution
, 15. (instance Dead Attribute) [] kb_toplevel_4824
, 16. (not sP1099) [14, 15] subsumption_resolution
, 17. (<=>
  (forall (?VAR1)
    (or
      (not
        (instance ?VAR1 PositiveInteger))
      (not
        (sP1098 ?VAR1))))
  (not sP1099)) [] introduced:general_splitting_component_introduction
, 18. (forall (?VAR1)
  (or
    (or
      (not
        (instance ?VAR1 PositiveInteger))
      (not
        (sP1098 ?VAR1))) sP1099)) [17] cnf_transformation
, 19. (forall (?VAR1)
  (and
    (=>
      (exists (?VAR2)
        (and
          (and
            (and
              (=>
                (forall (?VAR3 ?VAR4 ?VAR5)
                  (=>
                    (and
                      (instance ?VAR5 SetOrClass)
                      (instance ?VAR3 PositiveInteger))
                    (=>
                      (and
                        (and
                          (=
                            (ListOrderFn
                              (ListFn__1Fn ?VAR1) ?VAR3) ?VAR4)
                          (domain immediateInstance ?VAR3 ?VAR5))
                        (lessThan ?VAR3 ?VAR2))
                      (instance ?VAR4 ?VAR5))))
                (exists (?VAR6)
                  (immediateInstance ?VAR1 ?VAR6)))
              (valence immediateInstance ?VAR2))
            (instance immediateInstance Relation))
          (instance ?VAR2 PositiveInteger)))
      (and
        (instance immediateInstance Predicate)
        (instance immediateInstance TotalValuedRelation)))
    (=>
      (and
        (instance immediateInstance Predicate)
        (instance immediateInstance TotalValuedRelation))
      (exists (?VAR2)
        (and
          (and
            (and
              (=>
                (forall (?VAR3 ?VAR4 ?VAR5)
                  (=>
                    (and
                      (instance ?VAR5 SetOrClass)
                      (instance ?VAR3 PositiveInteger))
                    (=>
                      (and
                        (and
                          (=
                            (ListOrderFn
                              (ListFn__1Fn ?VAR1) ?VAR3) ?VAR4)
                          (domain immediateInstance ?VAR3 ?VAR5))
                        (lessThan ?VAR3 ?VAR2))
                      (instance ?VAR4 ?VAR5))))
                (exists (?VAR6)
                  (immediateInstance ?VAR1 ?VAR6)))
              (valence immediateInstance ?VAR2))
            (instance immediateInstance Relation))
          (instance ?VAR2 PositiveInteger)))))) [] kb_toplevel_11
, 20. (forall (?VAR1)
  (and
    (=>
      (exists (?VAR2)
        (and
          (and
            (and
              (=>
                (forall (?VAR3 ?VAR4 ?VAR5)
                  (=>
                    (and
                      (instance ?VAR5 SetOrClass)
                      (instance ?VAR3 PositiveInteger))
                    (=>
                      (and
                        (and
                          (=
                            (ListOrderFn
                              (ListFn__1Fn ?VAR1) ?VAR3) ?VAR4)
                          (domain immediateInstance ?VAR3 ?VAR5))
                        (lessThan ?VAR3 ?VAR2))
                      (instance ?VAR4 ?VAR5))))
                (exists (?VAR6)
                  (immediateInstance ?VAR1 ?VAR6)))
              (valence immediateInstance ?VAR2))
            (instance immediateInstance Relation))
          (instance ?VAR2 PositiveInteger)))
      (and
        (instance immediateInstance Predicate)
        (instance immediateInstance TotalValuedRelation)))
    (=>
      (and
        (instance immediateInstance Predicate)
        (instance immediateInstance TotalValuedRelation))
      (exists (?VAR7)
        (and
          (and
            (and
              (=>
                (forall (?VAR8 ?VAR9 ?VAR10)
                  (=>
                    (and
                      (instance ?VAR10 SetOrClass)
                      (instance ?VAR8 PositiveInteger))
                    (=>
                      (and
                        (and
                          (=
                            (ListOrderFn
                              (ListFn__1Fn ?VAR1) ?VAR8) ?VAR9)
                          (domain immediateInstance ?VAR8 ?VAR10))
                        (lessThan ?VAR8 ?VAR7))
                      (instance ?VAR9 ?VAR10))))
                (exists (?VAR11)
                  (immediateInstance ?VAR1 ?VAR11)))
              (valence immediateInstance ?VAR7))
            (instance immediateInstance Relation))
          (instance ?VAR7 PositiveInteger)))))) [19] rectify
, 21. (forall (?VAR1)
  (and
    (or
      (and
        (instance immediateInstance Predicate)
        (instance immediateInstance TotalValuedRelation))
      (forall (?VAR2)
        (or
          (or
            (or
              (and
                (forall (?VAR3)
                  (not
                    (immediateInstance ?VAR1 ?VAR3)))
                (forall (?VAR4 ?VAR5 ?VAR6)
                  (or
                    (or
                      (instance ?VAR5 ?VAR6)
                      (or
                        (not
                          (=
                            (ListOrderFn
                              (ListFn__1Fn ?VAR1) ?VAR4) ?VAR5))
                        (not
                          (domain immediateInstance ?VAR4 ?VAR6)))
                      (not
                        (lessThan ?VAR4 ?VAR2)))
                    (not
                      (instance ?VAR6 SetOrClass))
                    (not
                      (instance ?VAR4 PositiveInteger)))))
              (not
                (valence immediateInstance ?VAR2)))
            (not
              (instance immediateInstance Relation)))
          (not
            (instance ?VAR2 PositiveInteger)))))
    (or
      (exists (?VAR7)
        (and
          (and
            (and
              (or
                (exists (?VAR8)
                  (immediateInstance ?VAR1 ?VAR8))
                (exists (?VAR9 ?VAR10 ?VAR11)
                  (and
                    (and
                      (not
                        (instance ?VAR10 ?VAR11))
                      (and
                        (=
                          (ListOrderFn
                            (ListFn__1Fn ?VAR1) ?VAR9) ?VAR10)
                        (domain immediateInstance ?VAR9 ?VAR11))
                      (lessThan ?VAR9 ?VAR7))
                    (instance ?VAR11 SetOrClass)
                    (instance ?VAR9 PositiveInteger))))
              (valence immediateInstance ?VAR7))
            (instance immediateInstance Relation))
          (instance ?VAR7 PositiveInteger)))
      (not
        (instance immediateInstance Predicate))
      (not
        (instance immediateInstance TotalValuedRelation))))) [20] ennf_transformation
, 22. (forall (?VAR1)
  (and
    (or
      (and
        (instance immediateInstance Predicate)
        (instance immediateInstance TotalValuedRelation))
      (forall (?VAR2)
        (or
          (or
            (or
              (and
                (forall (?VAR3)
                  (not
                    (immediateInstance ?VAR1 ?VAR3)))
                (forall (?VAR4 ?VAR5 ?VAR6)
                  (or
                    (or
                      (or
                        (or
                          (or
                            (instance ?VAR5 ?VAR6)
                            (not
                              (=
                                (ListOrderFn
                                  (ListFn__1Fn ?VAR1) ?VAR4) ?VAR5)))
                          (not
                            (domain immediateInstance ?VAR4 ?VAR6)))
                        (not
                          (lessThan ?VAR4 ?VAR2)))
                      (not
                        (instance ?VAR6 SetOrClass)))
                    (not
                      (instance ?VAR4 PositiveInteger)))))
              (not
                (valence immediateInstance ?VAR2)))
            (not
              (instance immediateInstance Relation)))
          (not
            (instance ?VAR2 PositiveInteger)))))
    (or
      (or
        (exists (?VAR7)
          (and
            (and
              (and
                (or
                  (exists (?VAR8)
                    (immediateInstance ?VAR1 ?VAR8))
                  (exists (?VAR9 ?VAR10 ?VAR11)
                    (and
                      (and
                        (and
                          (and
                            (and
                              (not
                                (instance ?VAR10 ?VAR11))
                              (=
                                (ListOrderFn
                                  (ListFn__1Fn ?VAR1) ?VAR9) ?VAR10))
                            (domain immediateInstance ?VAR9 ?VAR11))
                          (lessThan ?VAR9 ?VAR7))
                        (instance ?VAR11 SetOrClass))
                      (instance ?VAR9 PositiveInteger))))
                (valence immediateInstance ?VAR7))
              (instance immediateInstance Relation))
            (instance ?VAR7 PositiveInteger)))
        (not
          (instance immediateInstance Predicate)))
      (not
        (instance immediateInstance TotalValuedRelation))))) [21] flattening
, 23. (forall (?VAR1)
  (or
    (or
      (not
        (instance immediateInstance TotalValuedRelation))
      (not
        (instance immediateInstance Predicate)))
    (instance
      (sK21 ?VAR1) PositiveInteger))) [22] cnf_transformation
, 24. (instance immediateInstance TotalValuedRelation) [] kb_toplevel_7821
, 25. (forall (?VAR1)
  (or
    (not
      (instance immediateInstance Predicate))
    (instance
      (sK21 ?VAR1) PositiveInteger))) [23, 24] subsumption_resolution
, 26. (instance immediateInstance Predicate) [] kb_toplevel_7819
, 27. (forall (?VAR1)
  (instance
    (sK21 ?VAR1) PositiveInteger)) [25, 26] subsumption_resolution
, 28. (forall (?VAR1)
  (or
    (not
      (sP1098
        (sK21 ?VAR1))) sP1099)) [18, 27] resolution
, 29. (not
  (subclass RealNumber Fish)) [] negated_conjecture
, 30. (forall (?VAR1)
  (or
    (not
      (subclass RealNumber ?VAR1))
    (sP1098 ?VAR1))) [29, 9] superposition
, 31. (subclass RealNumber Quantity) [] kb_toplevel_13066
, 32. (forall (?VAR1)
  (<=>
    (forall (?VAR2)
      (= ?VAR1 ?VAR2))
    (not
      (sP1098 ?VAR1)))) [] introduced:general_splitting_component_introduction
, 33. (forall (?VAR1 ?VAR2)
  (or
    (= ?VAR2 ?VAR1)
    (sP1098 ?VAR2))) [32] cnf_transformation
, 34. (forall (?VAR1)
  (or
    (subclass RealNumber ?VAR1)
    (sP1098 ?VAR1))) [31, 33] superposition
, 35. (forall (?VAR1)
  (sP1098 ?VAR1)) [30, 34] subsumption_resolution
, 36. sP1099 [28, 35] subsumption_resolution
, 37. false [16, 36] subsumption_resolution
]
apease commented 4 years ago

the appearance of a skolem function in step 7 (of the KIF output) is very odd. It seems to come from nowhere. More investigation needed

apease commented 4 years ago

I was not able to duplicate this with the current Merge.kif

apease commented 4 years ago

java -Xmx7g -classpath /home/apease/workspace/sigmakee/build/classes:/home/apease/workspace/sigmakee/lib/* com.articulate.sigma.KB -av "(subclass RealNumber Fish)"

... <preference name="logDir" value="/home/apease/.sigmakee/logs" /> <kb name="SUMO" > <constituent filename="/home/apease/.sigmakee/KBs/Merge.kif" /> </kb> </configuration>

% Proof not found in time 29.839 s % SZS status GaveUp for temp-comb KB.main(): bindings: [] KB.main(): proof: []

kharus commented 4 years ago

I updated sumo and sigma again and still get the same results. I'm attaching my merge and temp-comb

Merge.zip temp-comb.zip

apease commented 4 years ago

one possibility is that this is a caching issue. Please delete all the .ser files and .tptp files from your .sigmakee/KBs directory

kharus commented 4 years ago

I cleaned and re-created directory but I still have the same issue. I compared fresh temp-comb.tptp with one I attached earlier and they match exactly. I also tried to use other vampire versions: 4.4 and 4.2 but they find proof as well.

apease commented 4 years ago

I'll have a chance to work in depth on this Friday. Sorry I'm out of ideas on what might be wrong though

apease commented 4 years ago

I can replicate the faulty proof with your tptp file, but it doesn't occur in the current version. I have made some changes to Merge.kif. Could I trouble you to update and try again?

kharus commented 4 years ago

Hi Adam, Can you please post your Merge.kif ? I tried to update from the head but still get the same error.

apease commented 4 years ago

sorry I somehow neglected to push the update, just done now. Just in case, please be sure to copy the updated version of Merge.kif from your local Git repository (presumably workspace/sumo/Merge.kif) to your Sigma data directory (.sigmakee/KBs/Merge.kif)

kharus commented 4 years ago

I updated sumo, derivation now is much longer (attached zip) But I still get a proof for (subclass RealNumber Fish) My files proof.zip temp-comb.zip Merge.zip

apease commented 4 years ago

our Merge.kif files are identical but I don't get the contradiction. Have you deleted all the tptp files in your .sigmakee/KBs directory before running

java -Xmx7g -classpath /home/apease/workspace/sigmakee/build/classes:/home/apease/workspace/sigmakee/lib/* com.articulate.sigma.KB -av "(subclass RealNumber Fish)

apease commented 4 years ago

our tptp files are different however, so my best guess is that there's still some sort of caching issue. Here's my tptp file SUMO.zip

/home/apease/workspace/vampire/vampire --avatar off -qa answer_literal --mode casc --proof tptp -t 60 /home/apease/.sigmakee/KBs/temp-comb.tptp

... % Proof not found in time 59.817 s % SZS status GaveUp for temp-comb temp-comb.zip

kharus commented 4 years ago

I did a clean run and I still get the same results. I compared tptp files and there are more parens in my version. Could be the issue in translation from kif to tptp?

apease commented 4 years ago

your tptp file is also much larger. I've just double-checked that I've pushed all my latest sigmakee updates to git. So somehow it would appear that you're running different code. I've had to change some of the parentheses output to support both E and Vampire, since they differ slightly. Vampire is a little more forgiving than E, but there was one parser bug in Vampire I had to accommodate

kharus commented 4 years ago

I did a fresh checkout of sigma and built it from scratch - still get the same results. Can you please post your $SIGMA_SRC/build/classes or sigmakee.jar ?

apease commented 4 years ago

This is really quite a mystery. Here's my jar file and my config file in hopes it will help config.zip

sigmakee.zip

arademaker commented 4 years ago

Just to contribute with my outputs. I didn't get a proof for 

% java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.KB -av "(subclass RealNumber Fish)"
...
% Memory used [KB]: 59615
% Time elapsed: 0.300 s
% Proof not found in time 29.826 s
% SZS status GaveUp for temp-comb
KB.main(): bindings: []
KB.main(): proof: []

But I also didn't get a proof for:

ar@leme .sigmakee % java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.KB -av "(subclass RealNumber Number)"
...
% Memory used [KB]: 76885
% Time elapsed: 0.400 s
% Proof not found in time 29.975 s
% SZS status Timeout for temp-comb
KB.main(): bindings: []
KB.main(): proof: []

Using only Merge.kif last version from the master branch.

apease commented 4 years ago

This gets more an more mysterious. I get the proof as expected

% Refutation found. Thanks to Tanya! % SZS status Theorem for temp-comb % SZS output start Proof for temp-comb fof(f7382,plain,( $false), inference(unit_resulting_resolution,[],[f7381])). fof(f7381,plain,( $false), inference(subsumption_resolution,[],[f7359,f7362])). fof(f7362,plain,( ssubclass(sRealNumber,sNumber)), inference(cnf_transformation,[],[f6909])). fof(f6909,axiom,( ssubclass(sRealNumber,sNumber)), file('/home/apease/.sigmakee/KBs/temp-comb.tptp',kb_SUMO_6909)). fof(f7359,plain,( ~ssubclass(sRealNumber,sNumber)), inference(cnf_transformation,[],[f7344])). fof(f7344,plain,( ~ssubclass(sRealNumber,sNumber)), inference(flattening,[],[f7343])). fof(f7343,negated_conjecture,( ~ssubclass(sRealNumber,s__Number)), inference(negated_conjecture,[],[f7342])). fof(f7342,conjecture,( ssubclass(sRealNumber,s__Number)), file('/home/apease/.sigmakee/KBs/temp-comb.tptp',query_0)). % SZS output end Proof for temp-comb % ------------------------------ % Version: Vampire 4.4.0 (commit c41a8b5f on 2020-03-31 20:18:58 +0200) % Termination reason: Refutation

% Memory used [KB]: 6780 % Time elapsed: 0.015 s % ------------------------------ % ------------------------------ % Success in time 0.181 s

apease commented 4 years ago

/home/apease/workspace/vampire/vampire --avatar off -qa answer_literal --mode casc --proof tptp -t 60 /home/apease/.sigmakee/KBs/temp-comb.tptp

kharus commented 4 years ago

If I use your SUMO.tptp then -av "(subclass RealNumber Fish)" works fine for me as well. But if I clean everything and use your sigmakee.jar to regenerate SUMO.tptp I still get the same result (75 steps proof).

apease commented 4 years ago

so I guess that narrows it down to something in your .sigmakee/KBs dir. I'll suggest you delete all the .kif and .tptp files there and have the Merge.kif I linked to above as the only .kif file. Sorry this is such a tough puzzle. I've never had so many challenges with someone else's installation. Once we figure out what the issue is, I'll have to add some diagnostic that prevents it for people in the future. I'm grateful for your efforts in finding the diagnosis. Another option if that still doesn't work is to create a Linux VM that I can log into and we can do a Zoom call while I work on it with you.

kharus commented 4 years ago

I cleaned KBs folder from kif and tptp and downloaded Merge.kif directly from github. wget https://raw.githubusercontent.com/ontologyportal/sumo/master/Merge.kif But it's still the same. I suspect the difference is in the code which produces tptp files. This is why I wanted to run with your local juar. But even with your sigmakee.jar I get sumo.tptp with many parens. Do you remember commit version for change which reduced parens wrapping? I want to double-checked it's applied locally.

apease commented 4 years ago

is Merge.kif the only kif file in your .sigmakee/KBs ? Especially, is there a UserAssertions.kif file? If so, that could be the problem. The parens change was quite a while ago. Another possibility is to delete the contents of the workspace/sigmakee/build directory but it sounds like you've already tried that. I've triple-checked now that I've pushed all the code in workspace/sigmakee to GitHub

kharus commented 4 years ago

I checked your config line by line and I noticed you have caching disabled. This fixes issue on my original install

 <preference name="cache" value="no" />

I also created another clean installation of sigma without checking out code. I just downloaded libraries from mvncentral and used jar you posted.

wget https://repo1.maven.org/maven2/com/google/guava/guava/19.0/guava-19.0.jar
wget https://repo1.maven.org/maven2/com/igormaznitsa/java-prolog-parser/2.0.2/java-prolog-parser-2.0.2.jar
wget https://repo1.maven.org/maven2/antlr/antlr/2.7.5/antlr-2.7.5.jar
wget https://github.com/ontologyportal/sigmakee/files/5196005/sigmakee.zip -> sigmakee.jar

Then I added config you posted earlier and downloaded sumo from the github

wget https://github.com/ontologyportal/sigmakee/files/5196011/config.zip -> config.xml
wget https://raw.githubusercontent.com/ontologyportal/sumo/master/Merge.kif

And I noticed that first time even with cache enabled it runs fine. But after that it starts to get the same error even if I clean KBs folder every time.

~/.sigmakee/KBs$ ls
Merge.kif  config.xml

I suspect sigma keeps caching information somewhere else as well.

apease commented 4 years ago

The only cached information should be in your $SIGMA_HOME/KBs . Sigma serializes the cache of transitive relations, WordNet etc and puts it in kbmanager.ser . It saves user assertions done in the Ask/Tell window into _UserAssertions.kif . Cached statements from transitive relation processing are placed in <kbname>_Cache.kif . A TPTP translation of the current KB will be created as <kbname>.tptp . Before sending a TPTP query to Vampire or E it will create temp-stmt.tptp for the query and concatenate with the translated KB file into temp-comb.tptp . For queries to E a file called EBatchConfig.txt will be created to point to the tptp files. That's everything I can think of that's saved, and it all goes in the .sigmakee/KBs directory