src/Main.java

@@ -8,39 +8,42 @@ import java.io.InputStreamReader;
 import java.util.List;
 
 public class Main {
-
+public static boolean DEBUG=false;
     private static final int TOTAL_BOUND = 3;
 
     public static void main(String[] args) throws IOException {
         if (args.length > 0) {
+            System.out.println(new Node.NodeId(128).hashCode());
+            System.out.println(new Node.NodeId(432).hashCode());
             test();
         } else {
+            DEBUG=false;
             System.out.println("Spróbuj wpisać jakie co, na przykład:");
             System.out.println("Paradoks barowy: jeśli jeden pije, to wszyscy piją");
             System.out.println("exists x. forall y. (Pije(x) => Pije(y))");
             System.out.println("Albo udowodnij istnienie liczby 4");
             System.out.println("N(0) ∧ ∀i.((N(i) ⇒ N(s(i)))) ⇒ N(s(s(s(0))))");
-            var in= new BufferedReader( new InputStreamReader(System.in));
+            var in = new BufferedReader(new InputStreamReader(System.in));
             while (true) {
                 System.out.print("> ");
                 var l = in.readLine();
-                if(l==null || l.isEmpty()) break;
+                if (l == null || l.isEmpty()) break;
                 var parseS = System.nanoTime();
-                var f =Parser.parse(l);
+                var f = Parser.parse(l);
                 var parseE = System.nanoTime();
-                System.out.println("Przeczytałem: "+f);
-                var t=new Tree(f);
-                var searchBound=TOTAL_BOUND;
+                System.out.println("Przeczytałem: " + f);
+                var t = new Tree(f);
+                var searchBound = TOTAL_BOUND;
                 var checkS = System.nanoTime();
-                var ok=t.isOk(searchBound);
+                var ok = t.isOk(searchBound);
                 var checkE = System.nanoTime();
-                System.out.printf("%10d <-parsowanie\n",parseE-parseS);
-                System.out.printf("%10d <-sprawdzanie\n",checkE-checkS);
+                System.out.printf("%10d <-parsowanie\n", parseE - parseS);
+                System.out.printf("%10d <-sprawdzanie\n", checkE - checkS);
                 String res;
-                if (ok){
-                    res  ="Jest git!";
-                }else {
-                    res ="Nie udało się. Głębokość szukania: "+searchBound;
+                if (ok) {
+                    res = "Jest git!";
+                } else {
+                    res = "Nie udało się. Głębokość szukania: " + searchBound;
                 }
                 System.out.println(res);
                 t.print();
@@ -49,12 +52,85 @@ public class Main {
     }
 
     public static void test() {
+        przypalcyklicznejUnif();
         trudne();
+        unifeday();
+        ciekawe();
         properunif();
         basic();
         forallex();
         Unifier.test();
         Parser.test();
+        idtest();
+
+    }
+
+    /**
+     * testy mają sprawdzić, czy program nie umiera przez wybranie złej rzeczy do unifikacji, samemu sobie blokując dalszą pracę
+     */
+    public static void przypalcyklicznejUnif(){
+        var ss = List.of(
+                "!((forall x . P(x)) and P(a) and (~P(b) or ~P(a)))",
+                "!((forall x . P(x)) and P(a) and (~P(a) or ~P(b)))",
+                "!(P(a) and (forall x . P(x)) and (~P(a) or ~P(b)))",
+                "!(P(a) and (forall x . P(x)) and (~P(b) or ~P(a)))"
+        );
+        for (String s : ss) {
+            var f = Parser.parse(s);
+            tt(f,true,false,1);
+        }
+    }
+    public static void idtest() {
+
+
+        var idBasics = """
+                (
+                  (forall x Id(x, x)) and
+                  (forall x forall y ( Id(x, y) -> Id(y,x) )) and
+                  (forall x forall y forall z ( Id(x, y) -> Id(y,z) -> Id(x, z) ))
+                )
+                """;
+
+        var testRefl = idBasics + " -> Id(a, a)";
+        var testSym = idBasics + " -> ( Id(a, b) -> Id(b,a) )";
+        var testTrans = idBasics + " -> ( Id(a,b) -> Id(b,c) -> Id(a,c) )";
+        System.out.println(testRefl.replace('\n', ' '));
+        System.out.println(testSym.replace('\n', ' '));
+        System.out.println(testTrans.replace('\n', ' '));
+
+        var fRefl = Parser.parse(testRefl);
+        var fSym = Parser.parse(testSym);
+        var fTrans = Parser.parse(testTrans);
+        tt(fRefl, true);
+        System.out.println("tera będzie ciężko");
+        tt(fSym, true, false);
+        System.out.println("A TERA NAJCIĘŻSZE");
+        tt(fTrans, true, false);
+        System.out.println("udało się");
+
+
+    }
+
+    public static void unifeday() {
+        var s = "~(forall x. (P(a) and P(x) and (~P(a) or ~P(b))))";
+        var f = Parser.parse(s);
+        tt(f, true, false, 1);
+    }
+
+    public static void ciekawe() {
+        var pcz = "forall x. Id(x, x) ";
+
+        var dcza = "forall x. exists y. Id(x,y)";
+        var dczaNie = "exists x. forall y. Id(x,y)";
+
+        var f = Parser.parse(pcz + " -> " + dcza);
+        var f2 = Parser.parse("(" + pcz + ") -> (" + dcza + ")");
+        if (!f.equals(f2)) throw new IllegalArgumentException();
+        tt(f, true, false);
+
+        var fn = Parser.parse("(" + pcz + ") -> (" + dczaNie + ")");
+        tt(fn, null); // nie wiadomo, bo nie jest powiedziane, że forall x y, Id(x, y)
+
     }
 
     public static void trudne() {
@@ -83,8 +159,7 @@ public class Main {
                             ),
                             new Formula.Predicate(N,
                                     List.of(
-                                            new Term.Function(s, new Term.Function(s, new Term.Function(s, zero)))
-
+                                            new Term.Function(s,new Term.Function(s,  new Term.Function(s, new Term.Function(s, new Term.Function(s, zero)))))
                                     ))
 
                     );
@@ -92,7 +167,8 @@ public class Main {
             ,
 
              */
-            tt(f, true, false);
+            tt(f, true, true);
+            tt(f, null, false, 2);
         }
 
         {
@@ -153,9 +229,9 @@ public class Main {
         var y = new Term.Variable.Name("y");
         var P = new Term.Variable.Name("P");
         Formula ok = new Formula.Forall(x, new Formula.Exists(y, new Formula.Equivalent(new Formula.Predicate(P, List.of(x)), new Formula.Predicate(P, List.of(y)))));
-        tt(ok, true);
+        tt(ok, true,false,1);
         Formula nieok = new Formula.Exists(x, new Formula.Forall(y, new Formula.Equivalent(new Formula.Predicate(P, x), new Formula.Predicate(P, y))));
-        tt(nieok, null);
+        tt(nieok, null,false,2);
     }
 
     public static void basic() {
@@ -177,7 +253,7 @@ public class Main {
         boolean cntd = t.isOk(searchB);
         if (cntd) {
             final var ok = !negate;
-            String s = ok ? "tak" : "nie" ;
+            String s = ok ? "tak" : "nie";
             if (expected == null) {
                 throw new IllegalArgumentException("dostałem " + s + " ale nic się nie miało znaleźć");
             }
@@ -189,6 +265,7 @@ public class Main {
             System.out.println(s + " " + f);
             if (printanyway) {
                 t.print();
+                System.out.println(t.successfullUnif);
             }
             return true;
         }
@@ -198,10 +275,14 @@ public class Main {
     public static void tt(Formula f, Boolean expected, boolean printanyway, int searchB) {
 //        for (int i = 0; i <= searchB; i++) {
         boolean fin;
-        fin = tth(f, expected, printanyway, searchB, false);
-        if (fin) return;
-        fin = tth(f, expected, printanyway, searchB, true);
-        if (fin) return;
+        if (expected == null || expected) {
+            fin = tth(f, expected, printanyway, searchB, false);
+            if (fin) return;
+        }
+        if (expected == null || !expected) {
+            fin = tth(f, expected, printanyway, searchB, true);
+            if (fin) return;
+        }
 //        }
         String s = String.format("Failed to prove nor disprove %s (search bound: %d)", f, searchB);
         if (expected != null) {

src/Node.java

@@ -6,30 +6,64 @@ import java.util.Optional;
 import java.util.function.Consumer;
 
 public class Node {
+    final Formula orig;
+    private final NodeId id;
+    public Node closedBy=null;
+
+    private static int COUNT=0;
+    private final Node  originator;
     Node parent;
     Formula formula;
+    public Node(Node parent, Formula f, Node originator ) {
+        this.parent = parent;
+        this.formula = f;
+        this.orig=f;
+        this.expanded = false;
+        this.children = new ArrayList<>();
+        this.id=new NodeId( COUNT++);
+        this.originator=originator;
+//        this.tg=tg;
+    }
+
+    public static Node root(Formula f){
+        return new Node(null,f,null);
+    }
+
+    public void closeBy(Node candidate) {
+        closedBy=candidate;
+    }
 
     List<Node> children;
 
+    public void revertToOrig(){
+        formula=orig;
+    }
+
+    public NodeId getId() {
+        return id;
+    }
+
     boolean expanded;
     boolean mark=false;
     boolean cls=false;
 
-    public Node(Node parent, Formula f) {
-        this.parent = parent;
-        this.formula = f;
-        this.expanded = false;
-        this.children = new ArrayList<>();
-    }
-
     public void expand() {
-//        if (expanded) {
-//            throw new IllegalArgumentException("Cannot expand expanded node");
-//        }
+        if (expanded && ! (RuleType.ofNode(this).isRetryable())) {
+           return;
+        }
         this.expanded = true;
         forEachTip(this, this::expand);
     }
 
+    public Optional<Node> getOriginator() {
+        return Optional.ofNullable(originator);
+    }
+
+    public boolean onlySimplify(){
+        Formula.NonRedundant simplify = formula.simplify();
+        return !simplify.equals(formula);
+    }
+
     private void forEachTip(Node n, Consumer<Node> f) {
         if (n.isTip()) f.accept(n);
         else
@@ -41,10 +75,10 @@ public class Node {
     private void expand(Node tip) {
         Formula.NonRedundant simplify = formula.simplify();
         List<Formula.Branch> branches;
-        if (simplify.equals(formula)) {
-            branches = simplify.subFormulas();
-        } else {
+        if (onlySimplify()) {
             branches = List.of(new Formula.Branch(simplify));
+        } else {
+            branches = simplify.subFormulas();
         }
 
         // DEBG
@@ -61,7 +95,7 @@ public class Node {
         for (Formula.Branch branch : branches) {
             var currentTip = tip;
             for (Formula f : branch.formulas()) {
-                Node node = new Node(currentTip, f);
+                Node node = new Node(currentTip, f, this);
                 currentTip.addChild(node);
                 currentTip = node;
             }
@@ -70,6 +104,13 @@ public class Node {
 //        return res;
     }
 
+    public  record NodeId(int id){
+        @Override
+        public String toString() {
+            return String.valueOf(id);
+        }
+    }
+
     private void addChild(Node child) {
         this.children.add(child);
     }

src/RuleType.java

@@ -0,0 +1,38 @@
+import lang.Formula;
+
+public enum RuleType {
+    NEITHER(false),
+
+    ALPHA(false),
+    BETA(false),
+    DELTA(false),
+    GAMMA(true),
+
+    ;
+
+    private final boolean retryable;
+
+     RuleType(boolean retryable){
+        this.retryable=retryable;
+    }
+
+    public static RuleType ofFormula(Formula.NonRedundant f){
+        return ( switch (f){
+            case Formula.And ignored -> ALPHA;
+            case Formula.Exists ignored -> DELTA;
+            case Formula.Forall ignored -> GAMMA;
+            case Formula.Not ignored -> NEITHER;
+            case Formula.Or ignored -> BETA;
+            case Formula.Predicate ignored -> NEITHER;
+        });
+    }
+    
+    public static RuleType ofNode(Node n){
+         if (n.onlySimplify()) return NEITHER;
+         return ofFormula(n.formula.simplify());
+    }
+
+    public boolean isRetryable(){
+        return retryable;
+    }
+}

src/TermGen.java

@@ -0,0 +1,183 @@
+import lang.Term;
+
+import java.util.*;
+import java.util.function.Predicate;
+import java.util.stream.Collectors;
+
+
+/**
+ * 0. f of arity 0 -> N0
+ * 1. f of arity 1 <=o nested
+ * 2. f of ority 1 w 1-nested arg, f or arity 2 w non-nester arg
+ */
+record AnnotatedFn(Term.FunName fn, int arity) {
+}
+
+public class TermGen implements Iterator<Term> {
+
+    private final Map<Integer, List<Term.FunName>> arities;
+    private int level ;
+    private List<Term> termsOfLevel;
+    private int idxOfLevel;
+
+    private TermGen(Map<Integer, List<Term.FunName>> arities) {
+        this.arities = HashMap.newHashMap(arities.size() + 1);
+        this.arities.putAll(arities);
+        if (!arities.containsKey(0)) {
+            var s = new Term.FunName(new Term.Variable.Intern());
+            arities.put(0, List.of(s));
+        }
+        level = 0;
+        idxOfLevel = 0;
+        termsOfLevel = constants();
+    }
+
+    public static boolean add1(int[] elo, int thr) {
+        var carry = 1;
+        for (int i = 0; i < elo.length; i++) {
+            elo[i] += carry;
+            if (elo[i] == thr) {
+                elo[i] = 0;
+                carry = 1;
+            } else {
+                carry = 0;
+            }
+        }
+        var overflow = carry > 0;
+        return !overflow;
+    }
+
+    public static Iterator<Term> termGen(Map<Integer, List<Term.FunName>> arities) {
+        if (arities.keySet().isEmpty() || arities.keySet().equals(Set.of(0))) {
+            return arities.getOrDefault(0, List.of(new Term.FunName(new Term.Variable.Intern())))
+                    .stream().map(funName -> (Term) new Term.Function(funName)).iterator();
+        }
+        return new TermGen(arities);
+    }
+
+    public static void main(String[] args) {
+        var m = Map.of(
+                0, List.of(new Term.FunName("a0"), new Term.FunName("b0")),
+                1, List.of(new Term.FunName("f1"),new Term.FunName("g1")),
+                2, List.of(new Term.FunName("F2"),new Term.FunName("G2"))
+
+        );
+        var tg = new TermGen(m);
+
+        var elo =new int[3];
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        TermGen.add1(elo,2);
+        for (int i = 0; i < 997; i++) {
+            System.out.println(tg.next());
+
+        }
+    }
+
+    private List<AnnotatedFn> symsOfArityLte(int arity) {
+        List<AnnotatedFn> res = new ArrayList<>();
+        for (int i = 0; i <= arity; i++) {
+            var ar = i;
+            res.addAll(functionSymbols(ar).stream().map(fn -> new AnnotatedFn(fn, ar)).toList());
+        }
+        return res;
+    }
+
+    private int maxDepth(Term t,int x){
+        return switch (t){
+            case Term.Function function ->
+                function.args().stream().mapToInt(f->maxDepth(f,x+1)).max().orElse(x);
+
+
+            case Term.Variable ignored -> x;
+        };
+
+    }
+
+    private int maxArity(Term t){
+        return switch (t){
+            case Term.Function function -> {
+                var r = function.args().size();
+                var r2=function.args().stream().mapToInt(this::maxArity).max().orElse(0);
+                yield Math.max(r,r2);
+            }
+            case Term.Variable ignored -> 0;
+        };
+    }
+
+    private List<Term> genTermsOfLevel(int nestedness) {
+        if (nestedness == 0) return constants();
+
+        List<Term> res = new ArrayList<>(); //będzie wielka szybko, uwaga!
+        var headFunSyms = symsOfArityLte(level);
+        var subTerms = genTermsOfLevel(nestedness - 1);
+
+        Predicate<Term> dododania = t-> maxArity(t)>= level || maxDepth(t,0)>=nestedness;
+        for (Term subTerm : subTerms) {
+            if(dododania.test(subTerm)) res.add(subTerm);
+        }
+        boolean ok;
+        for (AnnotatedFn headSym : headFunSyms) {
+
+            var prms = new int[headSym.arity()];
+            do {
+             var args =new ArrayList<Term>(headSym.arity());
+                for (int prm : prms) {
+                    args.add(subTerms.get(prm));
+                }
+                Term.Function e = new Term.Function(headSym.fn(), args);
+                if (dododania.test(e)) {
+                    res.add(e);
+                }
+                //else was already part of lower level
+                ok = add1(prms, subTerms.size());
+            } while (ok);
+
+        }
+
+        return res;
+    }
+
+    private void updateState() {
+        if (idxOfLevel == termsOfLevel.size()) {
+            level++;
+            idxOfLevel = 0;
+            termsOfLevel = genTermsOfLevel(level);
+        }
+    }
+
+    private List<Term> constants() {
+        return functionSymbols(0).stream().map(Term.Function::new).collect(Collectors.toList());
+    }
+
+    private boolean hasFunction() {
+        return arities.keySet().stream().filter(d -> d != 0).anyMatch(p -> true);
+    }
+
+    private List<Term.FunName> functionSymbols(int arity) {
+        return arities.getOrDefault(arity, List.of());
+    }
+
+    @Override
+    public boolean hasNext() {
+        return true;
+    }
+
+    private int maxArityOfLevel() {
+        return level;
+    }
+
+    @Override
+    public Term next() {
+        updateState();
+        return termsOfLevel.get(idxOfLevel++);
+    }
+
+
+}

src/Tree.java

@@ -6,15 +6,12 @@ import java.io.PrintStream;
 import java.util.*;
 import java.util.function.Function;
 import java.util.function.Predicate;
+import java.util.stream.Collectors;
 
 public class Tree {
     Node root;
 
-    public Tree(Formula formulaToProve) {
-        var f = new Formula.Not(formulaToProve);
-
-        root = (new Node(null, f));
-    }
+    public LinkedHashMap<Unifier.UV.Zmienna, Unifier.Unifiable> successfullUnif;
 
     public Optional<Node> findNode(Predicate<Node> additionalCnd) {
         return fon(root, additionalCnd);
@@ -32,6 +29,44 @@ public class Tree {
     }
 
     private boolean expanded = false;
+    boolean unifiedNything = false;
+
+    public Tree(Formula formulaToProve) {
+        var f = new Formula.Not(formulaToProve);
+
+        root = (Node.root(f));
+    }
+
+    private static LinkedHashMap<Term.Variable, Term> podmien(LinkedHashMap<Unifier.UV.Zmienna, Unifier.Unifiable> successfullUnif) {
+        LinkedHashMap<Term.Variable, Term> subst = new LinkedHashMap<>();
+        for (Unifier.UV.Zmienna uz : successfullUnif.keySet()) {
+            var uv = successfullUnif.get(uz);
+            subst.put(uz.v(), Unifier.toTerm(uv));
+        }
+        return subst;
+    }
+
+    private static Formula swapF(LinkedHashMap<Term.Variable, Term> subst, Formula f) {
+        var trzymak = new Trzymak<>(f);
+
+        subst.forEach((a, b) -> trzymak.zapisz(FormulaUtil.swap(trzymak.wez(), a, b)));
+        return trzymak.wez();
+    }
+
+    public List<Node> findTips() {
+        var r = new ArrayList<Node>();
+        ft(r, root);
+        return r;
+    }
+
+    private void ft(List<Node> r, Node n) {
+        if (n.getChildren().isEmpty()) r.add(n);
+        else {
+            for (Node child : n.getChildren()) {
+                ft(r, child);
+            }
+        }
+    }
 
     private boolean unexpandForalls() {
 
@@ -43,108 +78,251 @@ public class Tree {
         var chng = false;
         while (n.isPresent()) {
             chng = true;
-            n.get().mark=true;
-            n.get().expanded=false;
+            n.get().mark = true;
+            n.get().expanded = false;
             n = findNode(isForallNotMarked);
         }
 
         n = findNode(isForallMarked);
         while (n.isPresent()) {
-            n.get().mark=false;
+            n.get().mark = false;
             n = findNode(isForallMarked);
         }
         return chng;
     }
 
+    private void unmarkNonUnify() {
+
+        Predicate<Node> isNotMarked = nde -> !nde.mark;
+        Predicate<Node> isMarked = nde -> nde.mark;
+        var n = findNode(isNotMarked);
+        while (n.isPresent()) {
+            n.get().mark = true;
+            var nn = n.get();
+            nn.revertToOrig();
+            n = findNode(isNotMarked);
+        }
+
+        n = findNode(isMarked);
+        while (n.isPresent()) {
+            n.get().mark = false;
+            n = findNode(isMarked);
+        }
+
+
+    }
+
     public void expand() {
         if (expanded) return;
         expanded = true;
 
-        Predicate<Node> isForall = nde -> nde.formula instanceof Formula.Forall;
-        Predicate<Node> nonExpandedNotForall = nde -> nde.notExpanded() && Predicate.not(isForall).test(nde);
-        Predicate<Node> isForallNotExpanded = nde -> nde.notExpanded() && (isForall).test(nde);
 
         Optional<Node> n;
         boolean chng;
+
         do {
             chng = false;
-            n = findNode(nonExpandedNotForall);
-            while (n.isPresent()) {
-                n.get().expand();
-                chng = true;
-                n = findNode(nonExpandedNotForall);
-            }
+            for (RuleType type : RuleType.values()) {
+
+                Predicate<Node> nonExpanded = Node::notExpanded;
+                Predicate<Node> ofType = ndd -> RuleType.ofNode(ndd) == type;
+
+                Predicate<Node> thePred = ndd -> nonExpanded.test(ndd) && ofType.test(ndd);
 
-            n = findNode(isForallNotExpanded);
-            while (n.isPresent()) {
-                chng = true;
-                n.get().expand(); // pwt
-                n = findNode(isForallNotExpanded);
+                n = findNode(thePred);
+                while (n.isPresent()) {
+                    n.get().expand();
+                    chng = true;
+                    n = findNode(thePred);
+                }
             }
         } while (chng);
 
+
     }
 
+    public boolean isOk(int searchBound) {
+        for (int i = 0; searchBound < 0 || i < searchBound; i++) {
+            expand();
+            List<Node> tips = findTips();
+            var solutionsForEachbranch = new ArrayList<List<Pair>>();
+            for (Node tip : tips) {
+                solutionsForEachbranch.add(genPossilbeSolutions(tip));
+
+                // 1. generate possible unif. solutions for each open branch
+                // 2. find non-clasing solutions
+//
 
-    public List<Node> findTips() {
-        var r = new ArrayList<Node>();
-        ft(r, root);
-        return r;
-    }
+            }
 
-    private void ft(List<Node> r, Node n) {
-        if (n.getChildren().isEmpty()) r.add(n);
-        else {
-            for (Node child : n.getChildren()) {
-                ft(r, child);
+            var filtered = new ArrayList<List<Pair>>();
+            var ok = true;
+            for (List<Pair> branch : solutionsForEachbranch) {
+                // check if we're doomed -  no solutions even with unconstrained unif
+                if (branch.isEmpty()) {
+                    ok = false;
+                    break;
+                }
+                // remove branches solved without unif - they won't clash
+//                if (branch.stream().anyMatch(Map::isEmpty)) continue;
+                filtered.add(branch);
+            }
+            if (ok) {
+                ok = solveConstraints2(filtered);
             }
+            if (ok) {
+                if (Main.DEBUG) print();
+                return true;
+            }
+
+
+            var warto = unexpandForalls();
+            if (warto) {
+                if (i + 1 < searchBound) System.out.println("Trying another round of `forall` expansion");
+                unmarkNonUnify();
+            } else return false;// no point in expanding
         }
+        return false;
     }
 
-    public boolean isOk(int searchBound) {
-        main:
-        for (int i = 0; searchBound<0 || i < searchBound; i++) {
-            expand();
+
+    // return true if solution ok exists
+    private boolean solveConstraints2(ArrayList<List<Pair>> candidates) {
+        if (candidates.isEmpty()) {
             for (Node tip : findTips()) {
-                var ok = close(tip);
-                tip.cls=ok;
-                if (!ok) {
-                    var warto = unexpandForalls();
-                    if (warto) {
-//                        System.out.println("Trying another round of `forall` expansion");
-                        continue main;
-                    }
-                    else break main;
+                var closed = close(tip, false);
+                if (!closed) {
+                    System.out.println("to się nie powinno dziać, ale cóœ zrobisz");
+                    return false;
                 }
             }
             return true;
         }
+        var myPart = candidates.get(0);
+        var rest = candidates.subList(1, candidates.size());
+
+        for (Pair candidate : myPart) {
+            // try unif
+            var ca = Unifier.fromPred(candidate.a());
+            var cb = Unifier.fromPred(candidate.b());
+            var reso = Unifier.unify(ca, cb);
+            if (reso.isEmpty()) continue; //rodo chng
+            var res = reso.get();
+            // apply unif to tree
+            // first make a copy for bkup
+            var origRoot = new HashMap<Node.NodeId, Formula>();
+            backupFormulas(root, origRoot);
+            propChang(res);
+            // apply unif to remaining candidates(copy?!)
+            var newRest = new ArrayList<List<Pair>>();
+            var pp = podmien(res);
+            for (List<Pair> rr : rest) {
+                var nn = rr.stream().map(pr -> {
+                    var na = (Formula.Predicate) swapF(pp, pr.a());
+                    var nb = (Formula.Predicate) swapF(pp, pr.b());
+                    return new Pair(na, nb);
+                }).collect(Collectors.toList());
+                newRest.add(nn);
+            }
+            // go for rest
+            var ok = solveConstraints2(newRest);
+            if (ok) return true;
+            // revert changes (how?)
+            // so, rest stays rest
+            // revert tree changes
+            revert(root, origRoot);
+        }
+        // unif not found :(
         return false;
     }
 
-    private boolean close(Node tip) {
+    private void backupFormulas(Node node, Map<Node.NodeId, Formula> bkMap) {
+        bkMap.put(node.getId(), node.formula);
+        for (Node child : node.getChildren()) {
+            backupFormulas(child, bkMap);
+        }
+    }
+
+    private void revert(Node node, Map<Node.NodeId, Formula> bkMap) {
+        node.formula = bkMap.getOrDefault(node.getId(), node.formula);
+        for (Node child : node.getChildren()) {
+            revert(child, bkMap);
+        }
+    }
+
+
+
+    private List<Pair> genPossilbeSolutions(Node tip) {
+        var solutions = new ArrayList<Pair>();
         for (Node candidate = tip; candidate != null; candidate = candidate.getParent().orElse(null)) {
-            var candidateFormula = candidate.formula.simplify();
+            var candidateFormula = candidate.formula;//.simplify();
             if (candidateFormula instanceof Formula.Predicate pred) {
                 // look for neg!
                 for (Node othr = tip; othr != null; othr = othr.parent) {
-                    var otf = othr.formula.simplify();
+                    var otf = othr.formula;//.simplify();
                     if (otf instanceof Formula.Not on) {
-                        if (on.simplify() instanceof Formula.Not onn) {
+                        if (on/*.simplify() */ instanceof Formula.Not onn) {
                             var possiblyo = onn.f();
                             if (possiblyo instanceof Formula.Predicate op) {
                                 var a = Unifier.fromPred(pred);
                                 var b = Unifier.fromPred(op);
                                 var res = Unifier.unify(a, b);
                                 if (res.isPresent()) {
-                                    // uwaga kolejność iteracji ważna!!!
-                                    Map<Term.Variable, Term> resq = LinkedHashMap.newLinkedHashMap(res.get().size());
+                                    solutions.add(new Pair(pred, op));
+                                }
+                            }
+                        }
+                    }
+                }
+
+            }
+
+        }
+        return solutions;
+    }
+
+    private boolean close(Node tip, boolean allowUnif) {
+        for (Node candidate = tip; candidate != null; candidate = candidate.getParent().orElse(null)) {
+            var candidateFormula = candidate.formula;//.simplify();
+            if (candidateFormula instanceof Formula.Predicate pred) {
+                // look for neg!
+                for (Node othr = tip; othr != null; othr = othr.parent) {
+
+                    var otf = othr.formula;//.simplify();
+                    if (otf instanceof Formula.Not on) {
+                        if (on/*.simplify() */ instanceof Formula.Not onn) {
+                            var possiblyo = onn.f();
+                            if (possiblyo instanceof Formula.Predicate op) {
+//                                if (othr.dontUnifyWit.contains(candidate.getId())) {
+////                                    System.out.println("no co ty nie bd się z tobą unifikować "+candidateFormula +" " +othr.formula);
+//                                    continue;
+//                                }
+                                var a = Unifier.fromPred(pred);
+                                var b = Unifier.fromPred(op);
+                                var res = Unifier.unify(a, b);
+                                if (res.isPresent()) {
+                                    LinkedHashMap<Term.Variable, Term> resq = LinkedHashMap.newLinkedHashMap(res.get().size());
                                     res.get().forEach((Unifier.UV.Zmienna aq, Unifier.Unifiable bq) ->
                                             resq.put(aq.v(), Unifier.toTerm(bq))
                                     );
-
-
-                                    propagateChanges(resq);
+                                    boolean harmlessUnif = res.get().isEmpty();
+                                    if (!harmlessUnif) {
+                                        if (!allowUnif) {
+                                            throw new IllegalArgumentException();
+                                        }
+                                        unifiedNything = true;
+                                        propagateChanges(resq);
+                                    } else {
+                                        if (Main.DEBUG) {
+                                            System.out.printf("No i chyba git [%s,%s] %s %s%n",
+                                                    candidate.getId(),
+                                                    othr.getId(),
+                                                    candidate.formula,
+                                                    othr.formula
+                                            );
+                                        }
+                                    }
+                                    tip.closeBy(candidate);
                                     return true;
                                 }
                             }
@@ -158,30 +336,39 @@ public class Tree {
         return false;
     }
 
-    private void propagateChanges(Map<Term.Variable, Term> subst) {
+    private void propChang(LinkedHashMap<Unifier.UV.Zmienna, Unifier.Unifiable> successfullUnif) {
 
-        Function<Formula, Formula> swp = f -> {
-            var trzymak = new Trzymak<>(f);
-            // wygląda obejszczenie, ale kolejność ważna!
-            /*
-            przykład
-            Map(X-> d, Y->X)
-            X ^ Y -> d ^ Y ->  d ^ X
-            Map(Y->X, X->d)
-            X ^ Y -> X ^ X -> d ^ d
+        propagateChanges(podmien(successfullUnif));
+    }
 
-             */
+    private void propagateChanges(LinkedHashMap<Term.Variable, Term> subst) {
 
-            subst.forEach((a, b) -> trzymak.zapisz(FormulaUtil.swap(trzymak.wez(), a, b)));
-            return trzymak.wez();
-        };
+        Function<Formula, Formula> swp = f -> swapF(subst, f);
 
         propC(root, swp);
     }
 
-    private void propC(Node root, Function<Formula, Formula> swp) {
-        root.formula = swp.apply(root.formula);
-        root.children.forEach(a -> propC(a, swp));
+    private void propC(Node nde, Function<Formula, Formula> swp) {
+        nde.formula = swp.apply(nde.formula);
+        nde.children.forEach(a -> propC(a, swp));
+    }
+
+    private void print(PrintStream out, Node n, int ident) {
+        var s = "  ";
+        if (n.isTip()) {
+            s = (n.cls ? "XX" : "OO");
+        }
+
+        var ai = (n.closedBy == null ? "" : " {" + n.closedBy.getId() + "}");
+
+        for (int i = 0; i < ident; i++) out.print(s);
+        out.println("|" + n.formula + " " + n.getId() + " [" + n.getOriginator().map(Node::getId).orElse(n.getId()) + "]" + ai);
+        ////
+
+        for (Node child : n.children) {
+            print(out, child, ident + 1);
+        }
+
     }
 
 
@@ -193,19 +380,20 @@ public class Tree {
         print(out, root, 0);
     }
 
-    private void print(PrintStream out, Node n, int ident) {
-        var s = "  ";
-        if(n.isTip()){
-            s=(n.cls ? "XX":"OO");
-        }
-        for (int i = 0; i < ident; i++) out.print(s);
-        out.println( "|"+ n.formula );
-        ////
+    public Node ofId(Node.NodeId id) {
+        return ofIdInt(id, root);
+    }
 
-        for (Node child : n.children) {
-            print(out, child, ident + 1);
+    private Node ofIdInt(Node.NodeId id, Node root) {
+        if (root.getId().equals(id)) return root;
+        for (Node child : root.getChildren()) {
+            var r = ofIdInt(id, child);
+            if (r != null) return r;
         }
+        return null;
+    }
 
+     record Pair(Formula.Predicate a, Formula.Predicate b) {
     }
 
 }

src/Unifier.java

@@ -9,7 +9,6 @@ import java.util.stream.Collectors;
 
 public class Unifier {
 
-    Map<UV.Zmienna, Unifiable> u = new LinkedHashMap<>(); // kojeność ważna potem przy podstawianiu!
 
     public static Unifiable fromPred(Formula.Predicate c) {
         return new Unifiable.Tree(
@@ -39,6 +38,7 @@ public class Unifier {
             case Term.Variable.Unifiable unifiable -> new Unifiable.Atom(new Unifier.UV.Zmienna(unifiable));
         };
     }
+    LinkedHashMap<UV.Zmienna, Unifiable> u = new LinkedHashMap<>(); // kojeność ważna potem przy podstawianiu!
 
 
     public sealed interface Unifiable {
@@ -51,18 +51,25 @@ public class Unifier {
     }
 
 
-    public static Optional<Map<UV.Zmienna, Unifiable>> unify(Unifiable a, Unifiable b) {
-        var n = new Unifier();
-        n.unifyInt(a, b);
-        if (n.fail || n.circular) return Optional.empty();
-
-        n.contractByTransitivity();
-
-        return Optional.of(n.u);
-    }
-
-    public static void main(String[] args) {
-        test();
+//    public static Optional<LinkedHashMap<UV.Zmienna, Unifiable>> unify(List<Unifiable> unifs) {
+//        var n = new Unifier();
+//        var l =new ArrayList<Unifiable>(unifs.size());
+//        l.addAll(unifs);
+//        n.ui(l);
+//        if (n.fail || n.circular) return Optional.empty();
+//
+//        n.contractByTransitivity();
+//        return Optional.of(n.u);
+//    }
+
+    public static Optional<LinkedHashMap<UV.Zmienna, Unifiable>> unify(Unifiable a, Unifiable b) {
+//        return unify(List.of(a,b));
+           var n = new Unifier();
+           n.unifyInt(a, b);
+           if (n.fail || n.circular) return Optional.empty();
+
+           n.contractByTransitivity();
+           return Optional.of(n.u);
     }
 
     public static void test() {
@@ -73,8 +80,8 @@ public class Unifier {
                     new Unifiable.Tree(new UV.Cnst("Eq"), List.of(new Unifiable.Atom(new UV.Cnst("d")), new Unifiable.Atom(new UV.Zmienna("Y"))))
             ));
             if (spo != pr.isPresent()) throw new RuntimeException();
-            var ok=pr.get().values().stream().allMatch(q->q.equals(new Unifiable.Atom(new UV.Cnst("d"))));
-            if(!ok)throw  new RuntimeException();
+            var ok = pr.get().values().stream().allMatch(q -> q.equals(new Unifiable.Atom(new UV.Cnst("d"))));
+            if (!ok) throw new RuntimeException();
         }
 
         {
@@ -84,8 +91,10 @@ public class Unifier {
                     new Unifiable.Tree(new UV.Cnst("Eq"), List.of(new Unifiable.Atom(new UV.Zmienna("Y")), new Unifiable.Atom(new UV.Cnst("d"))))
             ));
             if (spo != pr.isPresent()) throw new RuntimeException();
-            var ok=pr.get().values().stream().allMatch(q->q.equals(new Unifiable.Atom(new UV.Cnst("d"))));
-            if(!ok)throw  new RuntimeException();
+            var prc = pr.get();
+//            prc=
+            var ok = prc.values().stream().allMatch(q -> q.equals(new Unifiable.Atom(new UV.Cnst("d"))));
+            if (!ok) throw new RuntimeException();
         }
 
         {
@@ -95,47 +104,236 @@ public class Unifier {
                     new Unifiable.Tree(new UV.Cnst("Eq"), List.of(new Unifiable.Atom(new UV.Zmienna("X")), new Unifiable.Atom(new UV.Zmienna("X"))))
             ));
             if (spo != pr.isPresent()) throw new RuntimeException();
-            var ok=pr.get().values().stream().allMatch(q->q.equals(new Unifiable.Atom(new UV.Cnst("d"))));
-            if(!ok)throw  new RuntimeException();
+            var ok = pr.get().values().stream().allMatch(q -> q.equals(new Unifiable.Atom(new UV.Cnst("d"))));
+            if (!ok) throw new RuntimeException();
         }
 
-        if(unify(
+        if (unify(
                 new Unifiable.Atom(new UV.Cnst("elo")),
                 new Unifiable.Atom(new UV.Cnst("elo"))
         ).isEmpty()) throw new RuntimeException();
 
-        if(unify(
+        if (unify(
                 new Unifiable.Atom(new UV.Cnst("elo")),
                 new Unifiable.Atom(new UV.Cnst("elow"))
         ).isPresent()) throw new RuntimeException();
 
 
-        if(unify(
+        if (unify(
                 new Unifiable.Atom(new UV.Cnst("elo")),
                 new Unifiable.Atom(new UV.Zmienna("elow"))
         ).isEmpty()) throw new RuntimeException();
 
-        if(unify(
+        if (unify(
                 new Unifiable.Atom(new UV.Zmienna("elo")),
                 new Unifiable.Atom(new UV.Cnst("elow"))
         ).isEmpty()) throw new RuntimeException();
 
 
-        if(unify(
+        if (unify(
                 new Unifiable.Tree(new UV.Cnst("f"), List.of(new Unifiable.Atom(new UV.Zmienna("he")), new Unifiable.Atom(new UV.Cnst("www")))),
                 new Unifiable.Tree(new UV.Cnst("f"), List.of(new Unifiable.Atom(new UV.Cnst("d")), new Unifiable.Atom(new UV.Zmienna("2d"))))
         ).isEmpty()) throw new RuntimeException();
 
-        if(unify(
+        if (unify(
                 new Unifiable.Tree(new UV.Cnst("q"), List.of(new Unifiable.Atom(new UV.Zmienna("he")), new Unifiable.Atom(new UV.Cnst("www")))),
                 new Unifiable.Tree(new UV.Cnst("f"), List.of(new Unifiable.Atom(new UV.Cnst("d")), new Unifiable.Atom(new UV.Zmienna("2d"))))
         ).isPresent()) throw new RuntimeException();
 
-        if(unify(
+        if (unify(
                 new Unifiable.Atom(new UV.Zmienna("2d")),
                 new Unifiable.Tree(new UV.Cnst("f"), List.of(new Unifiable.Atom(new UV.Cnst("d")), new Unifiable.Atom(new UV.Zmienna("2d"))))
-        ).isPresent())throw  new RuntimeException();
+        ).isPresent()) throw new RuntimeException();
+    }
+
+    //    private Unifiable replaceUnifInTrees(Unifiable unifiable) {
+//        return switch (unifiable){
+//            case Unifiable.Atom atom -> switch (atom.v){
+//                case UV.Cnst cnst -> atom;
+//                case UV.Zmienna zmienna -> {
+//                    Unifiable unifiable1 = u.get(zmienna);
+//                    if(unifiable1==null){
+//                        System.out.println("CO????");
+//                        yield atom;
+//                    }
+//                    yield unifiable1;
+//                }
+//            };
+//            case Unifiable.Tree tree ->
+//                    new Unifiable.Tree(tree.head(), tree.args.stream().map(this::replaceUnifInTrees).collect(Collectors.toList()));
+//        };
+//    }
+    private static boolean contains(Unifiable u, UV zmienna) {
+        return switch (u) {
+            case Unifiable.Atom atom -> atom.v().equals(zmienna);
+            case Unifiable.Tree tree -> {
+                for (Unifiable arg : tree.args) {
+                    if (contains(arg, zmienna)) yield true;
+                }
+                yield false;
+            }
+        };
+    }
+
+    public static void main(String[] args) {
+        test();
     }
+//
+//    private List<UV.Zmienna> zmienneH(List<Unifiable> unifiables) {
+//        var res = new ArrayList<UV.Zmienna>();
+//        for (Unifiable unifiable : unifiables) {
+//            switch (unifiable) {
+//                case Unifiable.Atom atom -> {
+//                    switch (atom.v()) {
+//                        case UV.Cnst cnst -> {
+//                        }
+//                        case UV.Zmienna zmienna -> {
+//                            res.add(zmienna);
+//                        }
+//                    }
+//                }
+//                case Unifiable.Tree tree -> {
+//                }
+//            }
+//        }
+//        return res;
+//    }
+//
+//    private List<UV.Cnst> cnstH(List<Unifiable> unifiables) {
+//        var res = new ArrayList<Unifier.UV.Cnst>();
+//        for (Unifiable unifiable : unifiables) {
+//            switch (unifiable) {
+//                case Unifiable.Atom atom -> {
+//                    switch (atom.v()) {
+//                        case UV.Cnst cnst -> {
+//                            res.add(cnst);
+//                        }
+//
+//                        case UV.Zmienna zmienna -> {
+//                        }
+//                    }
+//                }
+//                case Unifiable.Tree tree -> {
+//                }
+//            }
+//        }
+//        return res;
+//    }
+//
+//    private List<Unifiable.Tree> treesH(List<Unifiable> unifiables) {
+//        var res = new ArrayList<Unifiable.Tree>();
+//        for (Unifiable unifiable : unifiables) {
+//            switch (unifiable) {
+//                case Unifiable.Atom atom -> {
+//                    switch (atom.v()) {
+//                        case UV.Cnst cnst -> {
+//                        }
+//
+//                        case UV.Zmienna zmienna -> {
+//                        }
+//                    }
+//                }
+//                case Unifiable.Tree tree -> {
+//                    res.add(tree);
+//                }
+//            }
+//        }
+//        return res;
+//    }
+//
+//    private void ui(List<Unifiable> unifs) {
+//        if (fail) return;
+//
+//        //redundant safety
+//        unifs.replaceAll(this::sub);
+//
+//        if (unifs.isEmpty()) return;
+//        var zmienne = zmienneH(unifs);
+//        var stale = cnstH(unifs);
+//        var drzewa = treesH(unifs);
+//        if (drzewa.size() > 0 && stale.size() > 0) {
+//            doFail();
+//            return;
+//        }
+//
+//        if (drzewa.size() > 0) {
+//            var t0 = drzewa.get(0);
+//            var ok = drzewa.stream().allMatch(t -> t.head.equals(t0.head) && t.args.size() == t0.args.size());
+//            if (!ok) {
+//                doFail();
+//            } else {
+//                //var sub = new HashMap<UV.Zmienna,Unifiable>()
+//                Optional<UV.Zmienna> nakoniec = Optional.empty();
+//                if (!zmienne.isEmpty()) {
+//                    var z0 = zmienne.get(0);
+//                    nakoniec = Optional.of(z0);
+//                    var reszta = zmienne.subList(1, zmienne.size());
+//                    for (UV.Zmienna zmienna : reszta) {
+//                        put(zmienna, new Unifiable.Atom(z0));
+//                    }
+//
+//                }
+//                // to by mogło być pod ifem wyżej ale nie szkodzi
+//                drzewa.replaceAll(x -> (Unifiable.Tree) sub(x));
+//
+//                var occurs =
+//                        nakoniec.map(zm -> drzewa.stream().anyMatch(t -> contains(t, zm)));
+//                if (occurs.orElse(false)) {
+//                    circular = true;
+//                    doFail();
+//                    return;
+//                }
+//
+//                for (int argI = 0; argI < t0.args().size(); argI++) {
+//                    var nl = new ArrayList<Unifiable>();
+//                    for (int drzewoI = 0; drzewoI < drzewa.size(); drzewoI++) {
+//                        var arg = drzewa.get(drzewoI).args().get(argI);
+//                        nl.add(arg);
+//                    }
+//                    ui(nl);
+//                    if (fail) return;
+//                    drzewa.replaceAll(x -> (Unifiable.Tree) sub(x)); // do zoptymalizowania
+//                }
+//                if (nakoniec.isPresent()) {
+//                    var n = nakoniec.get();
+//                    put(n, drzewa.get(0));
+//                }
+//
+//            }
+//
+//
+//        } else if (stale.size() > 0) {
+//            //atomy>0
+//            var s0 = stale.get(0);
+//            var ok = stale.stream().allMatch(c -> c.equals(s0));
+//            if (!ok) {
+//                doFail();
+//                return;
+//            } else {
+//                if (!zmienne.isEmpty()) {
+//                    var z0 = zmienne.get(0);
+//                    var reszta = zmienne.subList(1, zmienne.size());
+//                    for (int i = 0; i < reszta.size(); i++) {
+//                        var zmienna = reszta.get(i);
+//                        put(zmienna, new Unifiable.Atom(z0));
+//                    }
+//                    for (UV.Cnst cnst : stale) {
+//                        put(z0, new Unifiable.Atom(cnst));
+//                    }
+//                } // i git
+//            }
+//        } else {
+//            // zmienne tylko xD
+//            var z0 = zmienne.get(0);
+//            var reszta = zmienne.subList(1, zmienne.size());
+//            for (UV.Zmienna zmienna : reszta) {
+//                put(zmienna, new Unifiable.Atom(z0));
+//            }
+//            // i git
+//        }
+//
+//    }
+
     boolean fail = false;
     boolean circular = false;
 
@@ -186,6 +384,15 @@ public class Unifier {
         fail = true;
     }
 
+    void put(UV.Zmienna z, Unifiable x) {
+        if (new Unifiable.Atom(z).equals(x)) return;
+        if (u.containsKey(z) && !u.get(z).equals(x)) {
+            throw new IllegalArgumentException();
+        }
+        u.put(z, x);
+
+    }
+
     private Unifiable sub(Map<UV.Zmienna, Unifiable> toSubst, Unifiable x) {
         return switch (x) {
             case Unifiable.Atom atom -> switch (atom.v()) {
@@ -199,46 +406,42 @@ public class Unifier {
 
     }
 
+    private Unifiable sub(Unifiable x) {
+        return sub(this.u, x);
+    }
+
     /**
      * dzięki temu już nie trzeba koniecznie linkowanej mapy
      */
-    private void contractByTransitivity(){
-        var ks=u.keySet();
-        ks.forEach (
-            zmienna ->{
-                var z=zmienna;
-                heh: while (u.containsKey(z)) {
-                    var nz = u.get(z);
-                    u.put(zmienna, nz);
-                    switch (nz) {
-                        case Unifiable.Atom atom -> {
-                            switch (atom.v()) {
-                                case UV.Cnst ignored -> {
-                                    break heh;
+    private void contractByTransitivity() {
+        var ks = u.keySet();
+        ks.forEach(
+                zmienna -> {
+                    var z = zmienna;
+                    heh:
+                    while (u.containsKey(z)) {
+                        var nz = u.get(z);
+                        u.put(zmienna, nz);
+                        switch (nz) {
+                            case Unifiable.Atom atom -> {
+                                switch (atom.v()) {
+                                    case UV.Cnst ignored -> {
+                                        break heh;
+                                    }
+                                    case UV.Zmienna zmienna1 -> z = zmienna1;
                                 }
-                                case UV.Zmienna zmienna1 -> z = zmienna1;
                             }
-                        }
-                        case Unifiable.Tree ignored -> {
-                            break heh;
+                            case Unifiable.Tree ignored -> {
+                                break heh;
+                            }
                         }
                     }
                 }
-            }
-
         );
-    }
 
-    private static boolean contains(Unifiable u, UV zmienna) {
-        return switch (u) {
-            case Unifiable.Atom atom -> atom.v().equals(zmienna);
-            case Unifiable.Tree tree -> {
-                for (Unifiable arg : tree.args) {
-                    if (contains(arg, zmienna)) yield true;
-                }
-                yield false;
-            }
-        };
+
+        // replace within tree
+
     }
 
     private void atomAtom(Unifiable.Atom atomA, Unifiable.Atom atomB) {
@@ -276,6 +479,7 @@ public class Unifier {
             }
         }
     }
+
     sealed interface UV {
         record Cnst(Term.Variable v) implements UV {
             Cnst(String v) {

src/lang/Formula.java

@@ -118,6 +118,12 @@ public sealed interface Formula permits Formula.Equivalent, Formula.Implies, For
         public List<Branch> subFormulas() {
             return List.of(new Branch(List.of(a, b)));
         }
+
+        @Override
+        public NonRedundant simplify() {
+            if(a.simplify().equals(b.simplify())) return a.simplify();
+            else return this;
+        }
     }
 
     record Or(Formula a, Formula b) implements NonRedundant {
@@ -128,6 +134,12 @@ public sealed interface Formula permits Formula.Equivalent, Formula.Implies, For
         }
 
         @Override
+        public NonRedundant simplify() {
+            if(a.simplify().equals(b.simplify())) return a.simplify();
+            else return this;
+        }
+
+        @Override
         public List<Branch> subFormulas() {
             return List.of(new Branch(List.of(a)), new Branch(List.of(b)));
         }
@@ -205,6 +217,7 @@ public sealed interface Formula permits Formula.Equivalent, Formula.Implies, For
         }
     }
 
+
     record Exists(Term.Variable var, Formula body) implements NonRedundant {
 
         @Override

src/lang/FormulaUtil.java

@@ -25,7 +25,7 @@ public class FormulaUtil {
         if (args.isEmpty()) return name+"";
         StringBuilder s= new StringBuilder();
         for (int i = 0; i < args.size(); i++) {
-            s.append(args.get(0));
+            s.append(args.get(i));
             if (i+1 !=args.size()) s.append(", ");
         }
 
@@ -119,7 +119,7 @@ public class FormulaUtil {
                 case Term.Function function ->
                         new Term.Function(function.name(),function.args().stream().map(this::swapterm).collect(Collectors.toList()));
                 case Term.Variable v -> {
-                    if (v.equals(old)) yield  nev;
+                    if (v.equals(old)) yield  nev; // meta add old?
                     else yield  term;
                 }
             };

src/lang/Term.java

@@ -5,52 +5,59 @@ import util.Gensym;
 import java.util.Arrays;
 import java.util.List;
 
-public sealed interface Term  permits Term.Variable, Term.Function{
+public sealed interface Term permits Term.Variable, Term.Function {
 
     sealed interface Variable extends Term {
-        record Name(String name) implements Variable{
+        record Name(String name) implements Variable {
             @Override
             public String toString() {
                 return name;
             }
         }
 
-        record Intern(Gensym g) implements Variable{
+        record Intern(Gensym g) implements Variable {
+            public Intern() {
+                this(new Gensym());
+            }
+
             @Override
             public String toString() {
-                return "G"+g.getId();
+                return "G" + g.getId();
             }
+        }
 
-            public Intern(){
+        record Unifiable(Gensym g) implements Variable {
+            public Unifiable() {
                 this(new Gensym());
             }
-        }
 
-        record Unifiable(Gensym g) implements Variable{
             @Override
             public String toString() {
-                return "U"+g.getId();
-            }
-            public Unifiable(){
-                this(new Gensym());
+                return "U" + g.getId();
             }
         }
     }
 
 
-    record FunName(Term.Variable name){
+    record FunName(Term.Variable name) {
+        public FunName(String name) {
+            this(new Variable.Name(name));
+        }
+
         @Override
         public String toString() {
             return name.toString();
         }
     }
-    record Function(FunName name, List<Term> args) implements Term{
-public Function(FunName name, Term... args){
-        this(name, Arrays.stream(args).toList());
-    }
 
-                @Override
+    record Function(FunName name, List<Term> args) implements Term {
+        public Function(FunName name, Term... args) {
+            this(name, Arrays.stream(args).toList());
+        }
+
+        @Override
         public String toString() {
-          return FormulaUtil.printNameArgs(name().name(), args);
-        }}
+            return FormulaUtil.printNameArgs(name().name(), args);
+        }
+    }
 }