You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
$ ~/work/vampire/vampire --mode casc -t 300 sumo/SUMO.tptp
% Exception at proof search level
Parsing Error on line 4
) expected at position 467 (text: s__equal__mV__NUMBER2)
In the top of the file:
% 0 of 34694 from file /Users/ar/workspace/sumo/Merge.kif at line 4924% not higher orderfof(kb_SUMO_1,axiom,(( ( ! [V__NUMBER1,V__NUMBER2] : (((s__AbsoluteValueFn(V__NUMBER1)s__equal__mV__NUMBER2)s__and__ms__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__NUMBER2,s__RealNumber))s__<=>((s__instance(V__NUMBER1,s__NonnegativeRealNumber)s__and__m(V__NUMBER1s__equal__mV__NUMBER2))s__or__m(s__instance(V__NUMBER1,s__NegativeRealNumber)s__and__m(V__NUMBER2s__equal__ms__SubtractionFn(0,V__NUMBER1))))) ) ))).
The text was updated successfully, but these errors were encountered:
In the top of the file:
The text was updated successfully, but these errors were encountered: