Skip to content
This repository has been archived by the owner on Aug 28, 2024. It is now read-only.

Unexpected failure to parse Vampire output #1

Open
pluehne opened this issue Nov 25, 2020 · 0 comments
Open

Unexpected failure to parse Vampire output #1

pluehne opened this issue Nov 25, 2020 · 0 comments
Assignees
@pluehne
Labels
bug

Comments

@pluehne
Copy link
Member

pluehne commented Nov 25, 2020 •
edited
Loading

Sometimes, anthem fails to parse Vampire’s output.

    Finished release [optimized] target(s) in 0.02s
     Running `target/release/anthem vprog examples/example-exact-cover.lp examples/example-exact-cover.spec`
     Started verification of specification from translated program
 Presupposed assumption: n >= 0
 Presupposed assumption: forall X1 (exists X2 s(X2, X1) -> exists N (X1 = N and N >= 1 and N <= n))
 Presupposed completed definition of covered/1: forall X (covered(X) <-> exists N (in_cover(N) and s(X, N)))
 Presupposed completed definition of in_cover/1: forall X (in_cover(X) <-> in_cover(X) and exists N (1 <= N and N <= n and X = N))
 Presupposed integrity constraint: forall N1, N2, X not (N1 != N2 and in_cover(N1) and in_cover(N2) and s(X, N1) and s(X, N2))
 Presupposed integrity constraint: forall X, N not (s(X, N) and not covered(X))
    Verified spec: forall X (in_cover(X) -> exists N (X = N and N >= 1 and N <= n)) in 0.003 seconds
 ERROR anthem::commands::verify_program > could not verify program: could not parse Vampire output
==== stdout ===========================================================
% (193365)lrs+1011_2:1_add=large:afr=on:afp=4000:afq=1.1:amm=off:anc=none:cond=on:fsr=off:gs=on:irw=on:nm=64:nwc=1:sas=z3:stl=30:sos=on:sp=reverse_arity:thf=on:urr=on:updr=off_2 on 
% (193366)lrs+1_2:3_afr=on:afp=1000:afq=1.1:amm=sco:anc=none:fsr=off:fde=none:gs=on:gsaa=full_model:gsem=on:lma=on:nm=64:nwc=1.3:sas=z3:stl=30:sac=on:tha=off:uwa=one_side_interpreted:updr=off_2 on 
% (193367)lrs+1010_4:1_aac=none:add=off:afp=40000:afq=1.0:amm=sco:anc=none:bd=off:cond=on:gs=on:gsem=on:irw=on:nm=0:nwc=2.5:sas=z3:stl=30:sos=theory:sp=reverse_arity:updr=off_2 on 
% (193368)dis+10_5_add=off:afp=4000:afq=1.1:anc=none:cond=fast:ep=RSTC:fsr=off:gs=on:gsem=on:lwlo=on:nm=64:nwc=1:sp=reverse_arity:thi=all_3 on 
% (193369)dis+4_3:2_afr=on:afp=1000:afq=1.1:amm=sco:bs=unit_only:cond=fast:fsr=off:fde=none:gsp=input_only:gs=on:gsem=off:inw=on:lcm=reverse:nwc=1:sas=z3:sos=all:sp=reverse_arity:tha=off:updr=off_4 on 
% (193370)dis+10_5_add=large:amm=sco:anc=none:fsr=off:gs=on:irw=on:lma=on:nm=64:nwc=1:sas=z3:sos=all:tha=off:thf=on_2 on 
% (193371)dis+11_4_afp=100000:afq=1.1:anc=none:cond=on:gs=on:gsaa=full_model:nm=64:nwc=1:sac=on:sp=reverse_arity:thi=all_2 on 
% (193372)dis+11_3_add=off:afp=10000:afq=2.0:amm=sco:anc=none:ep=RST:gs=on:gsaa=from_current:gsem=on:inw=on:nm=64:nwc=1:sd=10:ss=axioms:st=5.0:sos=all:tha=off:updr=off:uhcvi=on_59 on 
% (193369)Refutation found. Thanks to Tanya!
% SZS status Theorem for 
% SZS output start Proof for 
tff(type_def_5, type, object: $tType).
tff(func_def_0, type, f__integer__: $int > object).
tff(func_def_1, type, f__symbolic__: $i > object).
tff(func_def_2, type, c__infimum__: object).
tff(func_def_3, type, c__supremum__: object).
tff(func_def_4, type, n: $int).
tff(func_def_7, type, sK0: object).
tff(func_def_8, type, sK1: object).
tff(func_def_9, type, sK2: object > $int).
tff(func_def_10, type, sK3: object > $int).
tff(func_def_11, type, sK4: object > $int).
tff(func_def_12, type, sK5: object > $i).
tff(func_def_13, type, sK6: object > $int).
tff(func_def_14, type, sK7: object > $int).
tff(pred_def_1, type, p__is_integer__: object > $o).
tff(pred_def_2, type, p__is_symbolic__: object > $o).
tff(pred_def_3, type, p__less_equal__: (object * object) > $o).
tff(pred_def_4, type, p__less__: (object * object) > $o).
tff(pred_def_5, type, p__greater_equal__: (object * object) > $o).
tff(pred_def_6, type, p__greater__: (object * object) > $o).
tff(pred_def_8, type, covered: object > $o).
tff(pred_def_9, type, in_cover: object > $o).
tff(pred_def_10, type, s: (object * object) > $o).
tff(f1,axiom,(
  ! [X0 : object] : (p__is_integer__(X0) <=> ? [X1 : $int] : f__integer__(X1) = X0)),
  file(unknown,axiom)).
tff(f6,axiom,(
  ! [X4 : $int,X5 : $int] : (p__less_equal__(f__integer__(X4),f__integer__(X5)) <=> $lesseq(X4,X5))),
  file(unknown,axiom)).
tff(f10,axiom,(
  ! [X2 : object,X3 : object] : (p__less__(X2,X3) <=> (X2 != X3 & p__less_equal__(X2,X3)))),
  file(unknown,axiom)).
tff(f13,axiom,(
  ! [X1 : $int] : p__less__(c__infimum__,f__integer__(X1))),
  file(unknown,axiom)).
tff(f17,axiom,(
  ! [X2 : object] : (? [X3 : object] : s(X3,X2) => ? [X1 : $int] : ($lesseq(X1,n) & $greatereq(X1,1) & f__integer__(X1) = X2))),
  file(unknown,statement_2)).
tff(f18,axiom,(
  ! [X0 : object] : (covered(X0) <=> ? [X1 : $int] : (s(X0,f__integer__(X1)) & in_cover(f__integer__(X1))))),
  file(unknown,completed_definition_covered_1)).
tff(f21,axiom,(
  ! [X0 : object,X1 : $int] : ~(~covered(X0) & s(X0,f__integer__(X1)))),
  file(unknown,integrity_constraint)).
tff(f23,conjecture,(
  ! [X2 : object] : (? [X3 : object] : s(X2,X3) => ? [X8 : object] : (in_cover(X8) & s(X2,X8)))),
  file(unknown,statement_2)).
tff(f24,negated_conjecture,(
  ~! [X2 : object] : (? [X3 : object] : s(X2,X3) => ? [X8 : object] : (in_cover(X8) & s(X2,X8)))),
  inference(negated_conjecture,[],[f23])).
tff(f27,plain,(
  ! [X2 : object] : (? [X3 : object] : s(X3,X2) => ? [X1 : $int] : (~$less(n,X1) & ~$less(X1,1) & f__integer__(X1) = X2))),
  inference(evaluation,[],[f17])).
tff(f29,plain,(
  ! [X4 : $int,X5 : $int] : (p__less_equal__(f__integer__(X4),f__integer__(X5)) <=> ~$less(X5,X4))),
  inference(evaluation,[],[f6])).
tff(f30,plain,(
  ~! [X0 : object] : (? [X1 : object] : s(X0,X1) => ? [X2 : object] : (in_cover(X2) & s(X0,X2)))),
  inference(rectify,[],[f24])).
tff(f31,plain,(
  ! [X0 : $int] : p__less__(c__infimum__,f__integer__(X0))),
  inference(rectify,[],[f13])).
tff(f33,plain,(
  ! [X0 : object] : (? [X1 : object] : s(X1,X0) => ? [X2 : $int] : (~$less(n,X2) & ~$less(X2,1) & f__integer__(X2) = X0))),
  inference(rectify,[],[f27])).
tff(f40,plain,(
  ! [X0 : object,X1 : object] : (p__less__(X0,X1) <=> (X0 != X1 & p__less_equal__(X0,X1)))),
  inference(rectify,[],[f10])).
tff(f43,plain,(
  ! [X0 : $int,X1 : $int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) <=> ~$less(X1,X0))),
  inference(rectify,[],[f29])).
tff(f46,plain,(
  ? [X0 : object] : (! [X2 : object] : (~in_cover(X2) | ~s(X0,X2)) & ? [X1 : object] : s(X0,X1))),
  inference(ennf_transformation,[],[f30])).
tff(f48,plain,(
  ! [X0 : object] : (? [X2 : $int] : (~$less(n,X2) & ~$less(X2,1) & f__integer__(X2) = X0) | ! [X1 : object] : ~s(X1,X0))),
  inference(ennf_transformation,[],[f33])).
tff(f51,plain,(
  ! [X0 : object,X1 : $int] : (covered(X0) | ~s(X0,f__integer__(X1)))),
  inference(ennf_transformation,[],[f21])).
tff(f55,plain,(
  ? [X0 : object] : (! [X1 : object] : (~in_cover(X1) | ~s(X0,X1)) & ? [X2 : object] : s(X0,X2))),
  inference(rectify,[],[f46])).
tff(f56,plain,(
  ? [X0 : object] : (! [X1 : object] : (~in_cover(X1) | ~s(X0,X1)) & ? [X2 : object] : s(X0,X2)) => (! [X1 : object] : (~in_cover(X1) | ~s(sK0,X1)) & ? [X2 : object] : s(sK0,X2))),
  introduced(choice_axiom,[])).
tff(f57,plain,(
  ( ! [X0:object] : (? [X2 : object] : s(X0,X2) => s(X0,sK1)) )),
  introduced(choice_axiom,[])).
tff(f58,plain,(
  ! [X1 : object] : (~in_cover(X1) | ~s(sK0,X1)) & s(sK0,sK1)),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f55,f57,f56])).
tff(f61,plain,(
  ! [X0 : object] : (? [X1 : $int] : (~$less(n,X1) & ~$less(X1,1) & f__integer__(X1) = X0) | ! [X2 : object] : ~s(X2,X0))),
  inference(rectify,[],[f48])).
tff(f62,plain,(
  ! [X0 : object] : (? [X1 : $int] : (~$less(n,X1) & ~$less(X1,1) & f__integer__(X1) = X0) => (~$less(n,sK3(X0)) & ~$less(sK3(X0),1) & f__integer__(sK3(X0)) = X0))),
  introduced(choice_axiom,[])).
tff(f63,plain,(
  ! [X0 : object] : ((~$less(n,sK3(X0)) & ~$less(sK3(X0),1) & f__integer__(sK3(X0)) = X0) | ! [X2 : object] : ~s(X2,X0))),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK3])],[f61,f62])).
tff(f73,plain,(
  ! [X0 : object] : ((p__is_integer__(X0) | ! [X1 : $int] : f__integer__(X1) != X0) & (? [X1 : $int] : f__integer__(X1) = X0 | ~p__is_integer__(X0)))),
  inference(nnf_transformation,[],[f1])).
tff(f74,plain,(
  ! [X0 : object] : ((p__is_integer__(X0) | ! [X1 : $int] : f__integer__(X1) != X0) & (? [X2 : $int] : f__integer__(X2) = X0 | ~p__is_integer__(X0)))),
  inference(rectify,[],[f73])).
tff(f75,plain,(
  ! [X0 : object] : (? [X2 : $int] : f__integer__(X2) = X0 => f__integer__(sK6(X0)) = X0)),
  introduced(choice_axiom,[])).
tff(f76,plain,(
  ! [X0 : object] : ((p__is_integer__(X0) | ! [X1 : $int] : f__integer__(X1) != X0) & (f__integer__(sK6(X0)) = X0 | ~p__is_integer__(X0)))),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK6])],[f74,f75])).
tff(f77,plain,(
  ! [X0 : object] : ((covered(X0) | ! [X1 : $int] : (~s(X0,f__integer__(X1)) | ~in_cover(f__integer__(X1)))) & (? [X1 : $int] : (s(X0,f__integer__(X1)) & in_cover(f__integer__(X1))) | ~covered(X0)))),
  inference(nnf_transformation,[],[f18])).
tff(f78,plain,(
  ! [X0 : object] : ((covered(X0) | ! [X1 : $int] : (~s(X0,f__integer__(X1)) | ~in_cover(f__integer__(X1)))) & (? [X2 : $int] : (s(X0,f__integer__(X2)) & in_cover(f__integer__(X2))) | ~covered(X0)))),
  inference(rectify,[],[f77])).
tff(f79,plain,(
  ! [X0 : object] : (? [X2 : $int] : (s(X0,f__integer__(X2)) & in_cover(f__integer__(X2))) => (s(X0,f__integer__(sK7(X0))) & in_cover(f__integer__(sK7(X0)))))),
  introduced(choice_axiom,[])).
tff(f80,plain,(
  ! [X0 : object] : ((covered(X0) | ! [X1 : $int] : (~s(X0,f__integer__(X1)) | ~in_cover(f__integer__(X1)))) & ((s(X0,f__integer__(sK7(X0))) & in_cover(f__integer__(sK7(X0)))) | ~covered(X0)))),
  inference(skolemisation,[status(esa),new_symbols(skolem,[sK7])],[f78,f79])).
tff(f84,plain,(
  ! [X0 : object,X1 : object] : ((p__less__(X0,X1) | (X0 = X1 | ~p__less_equal__(X0,X1))) & ((X0 != X1 & p__less_equal__(X0,X1)) | ~p__less__(X0,X1)))),
  inference(nnf_transformation,[],[f40])).
tff(f85,plain,(
  ! [X0 : object,X1 : object] : ((p__less__(X0,X1) | X0 = X1 | ~p__less_equal__(X0,X1)) & ((X0 != X1 & p__less_equal__(X0,X1)) | ~p__less__(X0,X1)))),
  inference(flattening,[],[f84])).
tff(f88,plain,(
  ! [X0 : $int,X1 : $int] : ((p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) & (~$less(X1,X0) | ~p__less_equal__(f__integer__(X0),f__integer__(X1))))),
  inference(nnf_transformation,[],[f43])).
tff(f89,plain,(
  s(sK0,sK1)),
  inference(cnf_transformation,[],[f58])).
tff(f90,plain,(
  ( ! [X1:object] : (~s(sK0,X1) | ~in_cover(X1)) )),
  inference(cnf_transformation,[],[f58])).
tff(f92,plain,(
  ( ! [X0:$int] : (p__less__(c__infimum__,f__integer__(X0))) )),
  inference(cnf_transformation,[],[f31])).
tff(f98,plain,(
  ( ! [X2:object,X0:object] : (f__integer__(sK3(X0)) = X0 | ~s(X2,X0)) )),
  inference(cnf_transformation,[],[f63])).
tff(f99,plain,(
  ( ! [X2:object,X0:object] : (~$less(sK3(X0),1) | ~s(X2,X0)) )),
  inference(cnf_transformation,[],[f63])).
tff(f100,plain,(
  ( ! [X2:object,X0:object] : (~$less(n,sK3(X0)) | ~s(X2,X0)) )),
  inference(cnf_transformation,[],[f63])).
tff(f108,plain,(
  ( ! [X0:object] : (f__integer__(sK6(X0)) = X0 | ~p__is_integer__(X0)) )),
  inference(cnf_transformation,[],[f76])).
tff(f109,plain,(
  ( ! [X0:object,X1:$int] : (p__is_integer__(X0) | f__integer__(X1) != X0) )),
  inference(cnf_transformation,[],[f76])).
tff(f110,plain,(
  ( ! [X0:object] : (in_cover(f__integer__(sK7(X0))) | ~covered(X0)) )),
  inference(cnf_transformation,[],[f80])).
tff(f111,plain,(
  ( ! [X0:object] : (s(X0,f__integer__(sK7(X0))) | ~covered(X0)) )),
  inference(cnf_transformation,[],[f80])).
tff(f121,plain,(
  ( ! [X0:object,X1:object] : (p__less_equal__(X0,X1) | ~p__less__(X0,X1)) )),
  inference(cnf_transformation,[],[f85])).
tff(f129,plain,(
  ( ! [X0:$int,X1:$int] : (p__less_equal__(f__integer__(X0),f__integer__(X1)) | $less(X1,X0)) )),
  inference(cnf_transformation,[],[f88])).
tff(f130,plain,(
  ( ! [X0:object,X1:$int] : (covered(X0) | ~s(X0,f__integer__(X1))) )),
  inference(cnf_transformation,[],[f51])).
tff(f135,plain,(
  ( ! [X1:$int] : (p__is_integer__(f__integer__(X1))) )),
  inference(equality_resolution,[],[f109])).
tff(f141,plain,(
  spl8_1 <=> ~s(sK0,sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_1])])).
tff(f144,plain,(
  spl8_0 <=> s(sK0,sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_0])])).
tff(f145,plain,(
  s(sK0,sK1) | ~spl8_0),
  inference(avatar_component_clause,[],[f144])).
tff(f146,plain,(
  spl8_0),
  inference(avatar_split_clause,[],[f89,f144])).
tff(f147,plain,(
  f__integer__(sK3(sK1)) = sK1 | ~spl8_0),
  inference(resolution,[],[f145,f98])).
tff(f148,plain,(
  ~$less(sK3(sK1),1) | ~spl8_0),
  inference(resolution,[],[f145,f99])).
tff(f149,plain,(
  ~$less(n,sK3(sK1)) | ~spl8_0),
  inference(resolution,[],[f145,f100])).
tff(f154,plain,(
  spl8_2 <=> f__integer__(sK3(sK1)) = sK1),
  introduced(avatar_definition,[new_symbols(naming,[spl8_2])])).
tff(f155,plain,(
  f__integer__(sK3(sK1)) = sK1 | ~spl8_2),
  inference(avatar_component_clause,[],[f154])).
tff(f156,plain,(
  spl8_2 | ~spl8_0),
  inference(avatar_split_clause,[],[f147,f144,f154])).
tff(f161,plain,(
  spl8_5 <=> ~$less(sK3(sK1),1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_5])])).
tff(f162,plain,(
  ~$less(sK3(sK1),1) | ~spl8_5),
  inference(avatar_component_clause,[],[f161])).
tff(f163,plain,(
  ~spl8_5 | ~spl8_0),
  inference(avatar_split_clause,[],[f148,f144,f161])).
tff(f168,plain,(
  spl8_7 <=> ~$less(n,sK3(sK1))),
  introduced(avatar_definition,[new_symbols(naming,[spl8_7])])).
tff(f169,plain,(
  ~$less(n,sK3(sK1)) | ~spl8_7),
  inference(avatar_component_clause,[],[f168])).
tff(f170,plain,(
  ~spl8_7 | ~spl8_0),
  inference(avatar_split_clause,[],[f149,f144,f168])).
tff(f171,plain,(
  p__less_equal__(f__integer__(1),f__integer__(sK3(sK1))) | ~spl8_5),
  inference(resolution,[],[f162,f129])).
tff(f176,plain,(
  spl8_8 <=> p__less_equal__(f__integer__(1),f__integer__(sK3(sK1)))),
  introduced(avatar_definition,[new_symbols(naming,[spl8_8])])).
tff(f178,plain,(
  spl8_8 | spl8_5),
  inference(avatar_split_clause,[],[f171,f161,f176])).
tff(f179,plain,(
  ~in_cover(sK1) | ~spl8_0),
  inference(resolution,[],[f90,f145])).
tff(f180,plain,(
  ~in_cover(f__integer__(sK7(sK0))) | ~covered(sK0)),
  inference(resolution,[],[f90,f111])).
tff(f185,plain,(
  spl8_11 <=> ~in_cover(sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_11])])).
tff(f187,plain,(
  ~spl8_11 | ~spl8_0),
  inference(avatar_split_clause,[],[f179,f144,f185])).
tff(f192,plain,(
  spl8_13 <=> ~covered(sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_13])])).
tff(f193,plain,(
  ~covered(sK0) | ~spl8_13),
  inference(avatar_component_clause,[],[f192])).
tff(f198,plain,(
  spl8_15 <=> ~in_cover(f__integer__(sK7(sK0)))),
  introduced(avatar_definition,[new_symbols(naming,[spl8_15])])).
tff(f199,plain,(
  ~in_cover(f__integer__(sK7(sK0))) | ~spl8_15),
  inference(avatar_component_clause,[],[f198])).
tff(f200,plain,(
  ~spl8_13 | ~spl8_15),
  inference(avatar_split_clause,[],[f180,f198,f192])).
tff(f201,plain,(
  p__less_equal__(f__integer__(sK3(sK1)),f__integer__(n)) | ~spl8_7),
  inference(resolution,[],[f169,f129])).
tff(f206,plain,(
  spl8_16 <=> p__less_equal__(f__integer__(sK3(sK1)),f__integer__(n))),
  introduced(avatar_definition,[new_symbols(naming,[spl8_16])])).
tff(f208,plain,(
  spl8_16 | spl8_7),
  inference(avatar_split_clause,[],[f201,f168,f206])).
tff(f209,plain,(
  ~covered(sK0) | ~spl8_15),
  inference(resolution,[],[f199,f110])).
tff(f210,plain,(
  ~spl8_13 | spl8_15),
  inference(avatar_split_clause,[],[f209,f198,f192])).
tff(f211,plain,(
  ( ! [X0:$int] : (~s(sK0,f__integer__(X0))) ) | ~spl8_13),
  inference(resolution,[],[f193,f130])).
tff(f213,plain,(
  p__less__(c__infimum__,sK1) | ~spl8_2),
  inference(superposition,[],[f92,f155])).
tff(f228,plain,(
  p__is_integer__(sK1) | ~spl8_2),
  inference(superposition,[],[f135,f155])).
tff(f233,plain,(
  spl8_18 <=> p__less__(c__infimum__,sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_18])])).
tff(f234,plain,(
  p__less__(c__infimum__,sK1) | ~spl8_18),
  inference(avatar_component_clause,[],[f233])).
tff(f235,plain,(
  spl8_18 | ~spl8_2),
  inference(avatar_split_clause,[],[f213,f154,f233])).
tff(f243,plain,(
  spl8_20 <=> p__is_integer__(sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_20])])).
tff(f244,plain,(
  p__is_integer__(sK1) | ~spl8_20),
  inference(avatar_component_clause,[],[f243])).
tff(f245,plain,(
  spl8_20 | ~spl8_2),
  inference(avatar_split_clause,[],[f228,f154,f243])).
tff(f246,plain,(
  f__integer__(sK6(sK1)) = sK1 | ~spl8_20),
  inference(resolution,[],[f244,f108])).
tff(f251,plain,(
  spl8_22 <=> f__integer__(sK6(sK1)) = sK1),
  introduced(avatar_definition,[new_symbols(naming,[spl8_22])])).
tff(f253,plain,(
  spl8_22 | ~spl8_20),
  inference(avatar_split_clause,[],[f246,f243,f251])).
tff(f254,plain,(
  p__less_equal__(c__infimum__,sK1) | ~spl8_18),
  inference(resolution,[],[f234,f121])).
tff(f260,plain,(
  spl8_24 <=> p__less_equal__(c__infimum__,sK1)),
  introduced(avatar_definition,[new_symbols(naming,[spl8_24])])).
tff(f262,plain,(
  spl8_24 | ~spl8_18),
  inference(avatar_split_clause,[],[f254,f233,f260])).
tff(f266,plain,(
  ~s(sK0,sK1) | (~spl8_2 | ~spl8_13)),
  inference(superposition,[],[f211,f155])).
tff(f270,plain,(
  ~spl8_1 | ~spl8_2 | spl8_13),
  inference(avatar_split_clause,[],[f266,f192,f154,f141])).
tff(f271,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f146,f156,f163,f170,f178,f187,f200,f208,f210,f235,f245,f253,f262,f270])).
% SZS output end Proof for 
% (193364)Success in time 0.029 s
==== stderr ===========================================================
@pluehne pluehne added the bug label Nov 25, 2020
@pluehne pluehne self-assigned this Nov 25, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@pluehne pluehne

Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@pluehne