A natural and interesting topic is the idea of a Term ordering.

Terms are syntax trees that we can throw different features into. An example of a term may be an arithmetic expression like

# (2 * 42) + 3
("+", [("*", [("lit", 2), ("lit",42)]), ("lit", 3)])
('+', [('*', [('lit', 2), ('lit', 42)]), ('lit', 3)])

Why do we want to compare terms? Well, having an ordering on terms enables the use of datastructures like balanced search trees.

But also perhaps more crucially, it is a mathematical way of describing the notion of “simpler”.

The most basic and obvious notion of simpler is to count the number of nodes in the term. Its size.

For some term rewriting simplifiers we may write, we can know thew thing isn’t going to loop (not terminate) if it always makes a little progress into a strictly simpler term. Presumably any reasonable order does not an infinite chain of simpler terms, so the rewriter has to stop eventually. We get rid of extra 0, constant propagate, fuse out things like -(-x) -> x or x - x -> 0. All of these rules make smaller terms so we can’t loop forever.

If we want to show that a particular term rewriting system has this nontermination property, we need to find a term ordering. This term ordering has to comply with the fact that the left and right hand side of rules contain pattern variables, which may stand in for any term. This puts pretty strong and complicated constraints on the term ordering.

I find the definition of the knuth bendix ordering pretty confusing. And yet, when you consider the ground case, it all becomes much simpler and more obvious. This is a general rule of thumb for understanding many techniques in automated reasoning. The ground stuff is a subcase and much easer. Here is the definition from “Term Rewriting and All That”

knuth bendix ordering

  1. KBO1 says that if the term sizes are different, the bigger one is larger.
  2. KBO2 is the tiebreaking rules for equal sized terms. 2a is not relevant to the ground case. 2b says to break ties using the head symbol. 2c says if the heads are equal to recurse lexicographically (compare in order) into the arguments.

Pretty straightforward actually. Compare by size. Tie break by head symbol and then recurse into arguments.

Here I implement this over z3 asts.

from enum import Enum
from z3 import *
Order = Enum("Order", ["LT", "EQ", "NGE", "GT"])
def kbo(t, r):

def size(t:ExprRef):
    return 1 + sum(size(x) for x in t.children())
def ground_kbo(t1, t2):
    if t1.eq(t2): # optimization
        return Order.EQ
    s1 = size(t1)
    s2 = size(t2)
    if s1 < s2:
        return Order.LT
    elif s1 > s2:
        return Order.GT
        if t1.num_args() < t1.num_args():
            return Order.LT
        elif t2.num_args() > t2.num_args():
            return Order.GT
        n1, n2 = t1.decl().name(), t2.decl().name()
        if n1 < n2:
            return Order.LT
        elif n1 > n2:
            return Order.GT
            for x,y in zip(t1.children(), t2.children()):
                o = ground_kbo(x,y)
                if o != Order.EQ:
                    return o
            assert False, "unreachable"

x,y,z = Ints("x y z")
assert ground_kbo(x,x) == Order.EQ
assert ground_kbo(x,y) == Order.LT
assert ground_kbo(y,y) == Order.EQ
assert ground_kbo(x + z, x + y) == Order.GT
assert ground_kbo((x + x) + x, x + (x + x)) == Order.GT
assert ground_kbo((z + z) + z, x * x) == Order.GT

Why is this interesting? Well, one reason is that it let’s you build an egraph. Completion over ground equations is the same thing as congruence closure. I think this road leads to extensions of the egraph that include lambdas (using ground versions of higher order kbo) and principled built in destructive rewriting (under what conditions does adding ground equations to a “good” non ground rewrite system retain the good properties?). I’m coming back around to these ideas. I got stumped and side tracked last time, but they still seem good.

https://pldi24.sigplan.org/details/egraphs-2024-papers/13/E-graphs-and-Automated-Reasoning-Looking-back-to-look-forward Giving a talk next month.

Bits and Bobbles

Completion for ground equations is guaranteed to terminate because you only produce terms smaller than the largest one you started with. Eventually you run out of terms. Critical pairs for ground terms is merely finding a one term as a subterm in another.

Working over z3 asts I think is a good idea. It let’s me bop in and out of z3 and complies with thew current direction I’m going in knuckledragger. Z3 is a vast raft of functionality.

https://www.cs.miami.edu/home/geoff/Courses/TPTPSYS/FirstOrder/SyntacticRefinements.shtml knuht bendix is not ground completable? https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/term-order.html prover 9 term orderings

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324232/ A Knuth-Bendix-Like Ordering for Orienting Combinator Equations

lambda free kbo https://www.isa-afp.org/browser_info/current/AFP/Lambda_Free_KBOs/document.pdf https://arxiv.org/abs/2005.02094

The default “tuple” ordering on terms

Python’s default for tuples is to compare them lexicographically. This corresponds to first comparing head symbols, then recursively comparing the arguments. This ordering is total. It isn’t great in that it isn’t a simplification ordering. A subterm can be larger than the term itself. Ok, why is that a problem? Well, it’s more obviously a problem if terms have variables in them, since to stay consistent we need to be able to substitute in any possible term. If we stick to ground terms though, this is not such a problem. It does run contrary to the idea that “size” is a good measure of simplicity.

An arbitrary (well founded) ordering is basically ok on ground terms because you don’t care as much about things like substitution. The typical union find exploits this to find an arbitrary online ordering that keeps the union find kind of flat.

Path Ordering

Harrison points out that LPO is basically constructed to have the substitution property. That is why we do a recursive check first.


def ground_lpo(s,t, vars=[]):
    if t in vars: #LPO1
        return t in s
    f = s.decl().name()
    g = t.decl().name()
    return any(ground_lpo(si, t) for si in s.children()) or \ #LPO2a
    all(ground_lpo(s, ti) for ti in t.children()) and \ #
    (f > g or # LPO2b no. I need to use Order.EQ Order.LT. This is close though. Oh well.
    f == g and any(ground_lpo(si,ti) for si, ti in zip(s.children(), t.children()))) #LPO2c

Ordering modulo theories. Like Hashing modulo theories, if you want to use an AVL tree to store some things that respect some equations, how do you do it? Set orderings and multiset orderings. Again can basically sort them and then use a lexicographic ordering.

How do you order alpha equiv terms? trvaversal order labelling or “tree maps” a la co de bruijn / hash cons modulo alpha.

In this direction lies alpha egraphs. nominal matching.

https://link.springer.com/content/pdf/10.1007/3-540-17220-3_4.pdf How to choose the weights in the Knuth Bendix ordering – ursula martin

https://academic.oup.com/comjnl/article/34/1/2/427931 An Introduction to Knuth–Bendix Completion Ajj dick

https://link.springer.com/article/10.1007/s10817-006-9031-4 Things to Know when Implementing KBO

We have a notion that simplifiers must terminate because terms get simpler until they can’t

“size” is a basic notion of complexity.

In order to guarantee a rule with variables gets smaller, we can count the number of symbols in it. The number of pattern variables has to be getting smaller, or else the thing is getting bigger.

(X + 0) -> X makes the term simpler

foo(bar(1,2,3,4,5,6,X)) -> biz(X,X) is not definitely a simplification, because X might be huge. In a realistic situation, we might want to guard this rule by size(X) < 3 or something.

A slight extension is to give the symbols in the term weight.

Another example is associating to the right. X + (Y + Z) -> (X + Y) + Z. This also obviously terminates. We can give lexicographic preference to left subtrees.

Another example is getting flatter. The height is descreasing.

distrbutivity is another common case. x(y + z) -> xy + xz. This is getting bigger *and duplicating x. That’s a big nono for most term orderings. But clearly foiling is terminating.

A different system that is obviously terminating is stratified macro expansion. Macros can refer to previously defined macros. The terms however, may get very large and be increasing in size. f(X) -> bar(X,X) is not an issue. Cycles in the dependency graph

We don’t expect to be able to have a total ordering on terms with variables in them. But we do want our definition to have a well defined

A primitive system that is obviously terminating are systems of the form f(x,y,z,...) -> z This is a view on the homeomorphic embedding relation.

right ground systems

Many functional programs are “obviously” terminating even if we don’t think of them in these terms

Negation normal form pushing

What about naive breadth first search: Separate into confluent terminating rules and naughty rules. (maude makes this disctinction but do so dynamically)

Hash cons only things that are normalized with respect to current rules. run twee for a bit, extract oriented rules, confluence them (?) Use the others for search.

TRS/SK90 Joachim Steinbach, Ulrich Kühler: Check your Ordering - termination proofs and open Problems, Technical Report SR-90-25, Universität Kaiserslautern, 1990. TRS/D33 Nachum Dershowitz: 33 Examples of Termination, 1995 Proc. French Spring School of Theoretical Computer Science, LNCS 909, http://www.math.tau.ac.il/~nachumd/papers/printemp-print.pdf TRS/AG01 Thomas Arts, Jürgen Giesl: Termination of term rewriting using dependency pairs, 2000, http://dblp.uni-trier.de/rec/bibtex/journals/tcs/ArtsG00 http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?). They include (as z027 .. z064) a set of one-rule termination problems by Alfons Geser (Habilitationsschrift, Tübingen, 2001) and possibly Winfried Kurth (Dissertation, Clausthal, 1990)

disjunctive normal form example. Makes term bigger.

Extraction Cost is Knuth Bendix Ordering Weights

consider ground extraction

elpi knuth bendix https://www.cl.cam.ac.uk/~jrh13/atp/ harrison’s code

Knuth bendix + grobner Can we do it? It’d be cool https://www3.risc.jku.at/publications/download/risc_3528/paper_48.pdf Knuth-bendix procedure and buchbergher - a synthesis

naive rewriting search engine. Keep score. Greedy. Then Expansive

import swipy import requests r = requests.get(‘https://www.metalevel.at/trs/trs.pl’)


pip install janus_swi

%%file /tmp/trs.pl
% based on markus triska's trs
:- op(800, xfx, ==>).
step([L==>R|Rs], T0, T) :-
        (   subsumes_term(L, T0) ->
            copy_term(L-R, T0-T)
        ;   step(Rs, T0, T)

normal_form(Rs, T0, T) :-
        (   var(T0) -> T = T0
        ;   T0 =.. [F|Args0],
            maplist(normal_form(Rs), Args0, Args1),
            T1 =.. [F|Args1],
            (   step(Rs, T1, T2) ->
                normal_form(Rs, T2, T)
            ;   T = T1

term_to_list(T, L) :-
        (   var(T) -> L = [T]
        ;   T =.. [F|Args],
            maplist(term_to_list, Args, ArgsL),
            L = [F|ArgsL]
Overwriting /tmp/trs.pl

% convert prolog term to lists of lists

# https://www.swi-prolog.org/pldoc/doc_for?object=section(%27packages/janus.html%27)
import janus_swi as janus
ans = janus.query_once("normal_form([f(x) ==> g(x)], f(x), _Res), term_to_list(_Res,Res).")
['g', ['x']]

https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html https://github.com/LPCIC/elpi/blob/master/src/builtin.elpi

%%file /tmp/trs.elpi
kind term type.

%infixr ==> 50.
%type (==>)   tye -> tye -> tye.
type fn string -> list term -> term.
type lam : (term -> term) -> term.

kind rule type.
type rule : term -> term -> rule.

pred normal : list rule,  term, term.

Writing /tmp/trs.elpi
! elpi -exec 'normal (fn "a" []) Ans' /tmp/trs.elpi
class Fn():
    cost: int
    hash: int
    head: str
    args: List['Fn']

def ground_kbo(t1,t2):
    if t1.cost < t2.cost:
        return True
    elif t1.cost > t2.cost:
        return False
    elif t1.head < t2.head:
        return True
    elif t1.head > t2.head:
        return False
        for arg1, arg2 in zip(t1.args ,t2.args):
            if arg1 == arg2:
            return ground_kbo(arg1, arg2)

import requests
res = requests.get("https://www.metalevel.at/trs/trs.pl")
with open("/tmp/trs.pl", "w") as f:

ERROR: /tmp/trs.pl:67:
ERROR:    source_sink `library(clpz)' does not exist
Warning: /tmp/trs.pl:67:
Warning:    Goal (directive) failed: user:use_module(library(clpz))
ERROR: /tmp/trs.pl:69:
ERROR:    source_sink `library(dcgs)' does not exist
Warning: /tmp/trs.pl:69:
Warning:    Goal (directive) failed: user:use_module(library(dcgs))
ERROR: /tmp/trs.pl:71:
ERROR:    source_sink `library(iso_ext)' does not exist
Warning: /tmp/trs.pl:71:
Warning:    Goal (directive) failed: user:use_module(library(iso_ext))
ERROR: /tmp/trs.pl:72:
ERROR:    source_sink `library(format)' does not exist
Warning: /tmp/trs.pl:72:
Warning:    Goal (directive) failed: user:use_module(library(format))
ERROR: /tmp/trs.pl:261:23: Syntax error: Operator expected
ERROR: /tmp/trs.pl:269:9: Syntax error: Operator expected
let rec termsize tm =
  match tm with
  | Fn(f,args) -> itlist (fun t n -> termsize t + n) args 1;;
    Var x -> 1
def termsize(tm):
    match tm:
        case ("Var", x):
            return 1
        case ("Fn", f, args):
            return sum(map(termsize, args)) + 1

from dataclasses import dataclass
from typing import Tuple
class Term:
class Fn(Term):
    f: str
    args: Tuple[Term]

class Var(Term):
    name: str

def Function(fn):
    def res(*args):
        return Fn(fn, args)
    return res
def Vars(xs):
    return [Var(x) for x in xs.split()]
def Functions(fns):
    return [Function(fn) for fn in fns.split()]

import enum

# traat
# harrison
# norvig
# eli bendersky

def unify(x, y, subst):
    """Unifies term x and y with initial subst.

    Returns a subst (map of name->term) that unifies x and y, or None if
    they can't be unified. Pass subst={} if no subst are initially
    known. Note that {} means valid (but empty) subst.
    if subst is None:
        return None
    elif x == y:
        return subst
    elif isinstance(x, Var):
        return unify_variable(x, y, subst)
    elif isinstance(y, Var):
        return unify_variable(y, x, subst)
    elif isinstance(x, Fn) and isinstance(y, Fn):
        if x.f != y.f or len(x.args) != len(y.args):
            return None
            for i in range(len(x.args)):
                subst = unify(x.args[i], y.args[i], subst)
            return subst
        return None

def unify_variable(v, x, subst):
    """Unifies variable v with term x, using subst.

    Returns updated subst or None on failure.
    assert isinstance(v, Var)
    if v.name in subst:
        return unify(subst[v.name], x, subst)
    elif isinstance(x, Var) and x.name in subst:
        return unify(v, subst[x.name], subst)
    elif occurs_check(v, x, subst):
        return None
        # v is not yet in subst and can't simplify x. Extend subst.
        return {**subst, v.name: x}

def occurs_check(v, term, subst):
    """Does the variable v occur anywhere inside term?

    Variables in term are looked up in subst and the check is applied
    assert isinstance(v, Var)
    if v == term:
        return True
    elif isinstance(term, Var) and term.name in subst:
        return occurs_check(v, subst[term.name], subst)
    elif isinstance(term, Fn):
        return any(occurs_check(v, arg, subst) for arg in term.args)
        return False

assert unify(Var("x"), Var("y"), {}) == {"x": Var("y")}
assert unify(Var("x"), Var("x"), {}) == {}
assert unify(Var("x"), Fn("f", [Var("y")]), {}) == {"x": Fn("f", [Var("y")])}
assert unify(Fn("f", [Var("x")]), Fn("f", [Var("y")]), {}) == {"x": Var("y")}
assert unify(Fn("f", [Var("x")]), Fn("g", [Var("y")]), {}) == None

# hmm. This is assuming "x" and "x" in the lhs rhs are the same thing.

def critical_pairs(f,g):
    if isinstance(f, Var) or isinstance(g, Var):
    elif f.f == g.f:
        subst = unify(f,g,{})
        if subst is not None:
            yield subst, f, g
    # This is double counting
    for arg in f.args:
        yield from critical_pairs(arg, g)
    for arg in g.args:
        yield from critical_pairs(f, arg)

list(critical_pairs(Fn("f", [Var("x")]), Fn("f", [Var("y")])))
list(critical_pairs(Fn("f", [Var("x")]), Fn("g", [Var("y")])))

def _match(e,pat,subst):
    match pat, e:
        case (Var(name), _):
            if pat.name in subst:
                if subst[pat.name] == e:
                    return subst
                    return None
                return {**subst, pat.name: e}
        case (Fn(f,args), Fn(f1,args1)):
            if f != f1 or len(args) != len(args1):
                return None
                for a1,a2 in zip(args,args1):
                    subst = _match(a1,a2,subst)
                    if subst == None:
                        return None
                return subst
        case _:
            raise ValueError(f"Can't match {pat} with {e}")


let rec lexord ord l1 l2 =
  match (l1,l2) with
    (h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
                       else h1 = h2 & lexord ord t1 t2
  | _ -> false;;
def lexord(ord, l1, l2):
    match (l1, l2):
        case ([h1,*t1], [h2, *t2]):
            if ord(h1, h2): # yeah I dunno about this. Is this a faithful rep of ord
                return len(t1) == len(t2)
                return h1 == h2 and lexord(ord,t1, t2)
        case _:
            return False

lexord([1,5], [1,4])
let rec lpo_gt w s t =
  match (s,t) with
    (_,Var x) ->
        not(s = t) & mem x (fvt s)
  | (Fn(f,fargs),Fn(g,gargs)) ->
        exists (fun si -> lpo_ge w si t) fargs or
        forall (lpo_gt w s) gargs &
        (f = g & lexord (lpo_gt w) fargs gargs or
         w (f,length fargs) (g,length gargs))
  | _ -> false
def lpo_gt(w,s,t):
    match (s,t):
        case (_, ("Var", x)):
            return s != t and x in fvt(s)
        case (("Fn", f, fargs), ("Fn", g, gargs)):
            return any(lpo_ge(w, si, t) for si in fargs) or \
                all(lpo_gt(w, s, si) for si in gargs) and \
                (f == g and lexord(lambda s,t: lpo_gt(w,s,t), fargs, gargs) or \
                 w(f, len(fargs), g, len(gargs)))
        case _:
            return False
def size(t):
    match t:
        case Var(x):
            return 1
        case Fn(f, args):
            return 1 + sum(map(size, args))

def vars(t):
    match t:
        case Var(x):
            yield x
        case Fn(f, args):
            for arg in args:
                yield from vars(arg)
from collections import Counter # a multiset type

def var_comp_lte(t1,t2):
    # We don't want to have more vars on lhs than rhs
    c1 = Counter(vars(t1))
    c2 = Counter(vars(t2))
    for k in c2:
        if c1[k] < c2[k]:
            return False
    return True

def kbo2a(t1,t2):
    if not isinstance(t2, Var):
        return False
    # check if t1 is iteerated functions symbol f over variable t2
    if not isinstance(t1, Fn):
        return False
    fn = t1.f
    def check(t):
        if isinstance(t, Var):
            return t == t2
        elif isinstance(t, Fn):
            return t.f == fn and len(t.args) == 1 and check(arg[0])
            raise ValueError("Not a term")
    return check(t1)

%%file /tmp/kbo_test.p
cnf(test, axiom, f = g).
cnf(false, conjecture, true = false).

Overwriting /tmp/kbo_test.p
!twee /tmp/kbo_test.p --precedence g,f
Here is the input problem:
  Axiom 1 (test): f = g.
  Goal 1 (false): true = false.

1. g -> f

Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
  g -> f

RESULT: CounterSatisfiable (the conjecture is false).
!twee /tmp/kbo_test.p --precedence f,g
Here is the input problem:
  Axiom 1 (test): f = g.
  Goal 1 (false): true = false.

1. f -> g

Ran out of critical pairs. This means the conjecture is not true.
Here is the final rewrite system:
  f -> g

RESULT: CounterSatisfiable (the conjecture is false).

def kbo(t1,t2):
    if not var_comp_lte(t1,t2):
        return True
    w1 = size(t1)
    w2 = size(t2)
    if w1 > w2:
        return True
    elif w1 < w2:
        return False
         if kbo2a(t1,t2):
             return True
         elif t2.f < t1.f:   #kbo2b
            return True
        elif: #kbo2c
            return None

# naive

def rw(t):
    match t:
        case ("+", 0, x):
            return x
        case x: 
            return ("+", 0, x)
        case ("+", x, 0):
            return x
        case x:
            return ("+", x, 0)
        case ("+", ("-", x), x):
            return 0

def expand(t):
    for (lhs,rhs) in rules:
        yield from apply(lhs,rhs,t)
        yield from apply(rhs,lhs,t)

def prove(lhs,rhs):
    lhsseen = set(lhs)
    rhsseen = set(rhs)
    while lhsseen & rhsseen == set():
        for t in expand(lhsseen):
            if t in rhsseen:
                return True
        for t in expand(rhsseen):
            if t in lhsseen:
                return True

%%file /tmp/eq.p
cnf(axiom1, axiom, a = b).
cnf(axiom2, axiom, b = c).
cnf(axiom3, axiom, c = d).
thf(p_decl, type, p : $i > $i).
thf(qdecl, type, q : $i > $i).
thf(axiom4, axiom, (^[X: $i] : X) = p).

Overwriting /tmp/eq.p

can turn decl = rewrite rule. maybe the special syntax is kind of nice. I don’t like thf that much

https://github.com/sneeuwballen/zipperposition/blob/master/examples/ind/list.zf https://github.com/sneeuwballen/zipperposition/blob/master/examples/ind/tree.zf

val[AC] plus : term -> term -> term. val to declare assert for axioms rewrite data definitions

!zipperposition /tmp/eq.p #--dot /tmp/eq.dot --debug 10
# done 4 iterations in 0.002s
% Final clauses: 4
[a = b*]/id:0/depth:0/penalty:1/red:false

[b = c*]/id:1/depth:0/penalty:1/red:false

forall X0. [X0 = p X0*]/id:3/depth:0/penalty:1/red:false

[b = d*]/id:4/depth:0/penalty:1/red:false
# SZS status Satisfiable for '/tmp/eq.p'
%%file /tmp/test.zf
val term : type.

data nat :=
  | z
  | s nat.

def[infix "+"] plus : nat -> nat -> nat where
  forall (X:nat). ((plus z X) = X);
  forall (X:nat). (forall (Y:nat). ((plus (s X) Y) = (s (plus X Y)))).

def[infix "-"] minus : nat -> nat -> nat where
  forall (X:nat). ((minus X z) = X);
  forall X. minus z X = z;
  forall (X:nat). (forall (Y:nat). ((minus (s X) (s Y)) = (minus X Y))).

def[infix "<"] less : nat -> nat -> prop where
  forall (X:nat). (less z (s X));
  forall X. ~ (less (s X) z);
  forall (X:nat). (forall (Y:nat). ((less (s X) (s Y)) <=> (less X Y))).

def[infix "≤"] leq : nat -> nat -> prop where
  forall (X:nat). (leq z X);
  forall X. ~ (leq (s X) z);
  forall (X:nat). (forall (Y:nat). ((leq (s X) (s Y)) <=> (leq X Y))).

Overwriting /tmp/test.zf
!zipperposition /tmp/test.zf
# done 0 iterations in 0.003s
% Final clauses: 0
# SZS status GaveUp for '/tmp/test.zf'
%%file /tmp/one.zf
data unit := One.

goal forall (x y: unit). x = y.
Writing /tmp/one.zf
!zipperposition /tmp/one.zf
# done 2 iterations in 0.003s
# SZS status Theorem for '/tmp/one.zf'
# SZS output start Refutation
* sk__1 = One(1) by trivial
* sk_ = One(2) by trivial
* sk__1 = sk_(3) by simp 'demod' with sk__1 = One(1), sk_ = One(2)
* goal [file "/tmp/one.zf" "zf_stmt_1"]
    ∀ x/45:unit y/46:unit. (x/45 = y/46). by
  goal 'zf_stmt_1' in '/tmp/one.zf'
* negated_goal ¬ (∀ x/45:unit y/46:unit. (x/45 = y/46)) # skolems: []. by
  esa 'cnf.neg'
    with goal [file "/tmp/one.zf" "zf_stmt_1"]
           ∀ x/45:unit y/46:unit. (x/45 = y/46).
* sk_ ≠ sk__1(0) by
  esa 'cnf'
    with negated_goal
           ¬ (∀ x/45:unit y/46:unit. (x/45 = y/46))
           # skolems: [].
* ⊥(4) by simp 'simplify_reflect-' with sk__1 = sk_(3), sk_ ≠ sk__1(0)

# SZS output end Refutation
!cat /tmp/eq.dot | dot -Tsvg > /tmp/eq.svg
cat: /tmp/eq.dot: No such file or directory