TermCOMP · jwaldmann · Jul 5, 2026 · Jul 5, 2026
diff --git a/SRS_Relative/Waldmann_26/1.ari b/SRS_Relative/Waldmann_26/1.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (a (b (b (a (a x))))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/10.ari b/SRS_Relative/Waldmann_26/10.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (b (b (b (a (b (b x))))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/11.ari b/SRS_Relative/Waldmann_26/11.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (b (a (a (a (b x)))))))) x)
+(rule x (a (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/12.ari b/SRS_Relative/Waldmann_26/12.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (b (a (a (b (b (b (b x))))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/13.ari b/SRS_Relative/Waldmann_26/13.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (b (b (a (a (b x)))))))) x)
+(rule x (a (b (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/14.ari b/SRS_Relative/Waldmann_26/14.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (b (b (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/15.ari b/SRS_Relative/Waldmann_26/15.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (b (a (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/16.ari b/SRS_Relative/Waldmann_26/16.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (b (a (a (a (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/17.ari b/SRS_Relative/Waldmann_26/17.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (b (b (a (b (a x))))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/18.ari b/SRS_Relative/Waldmann_26/18.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (b (a (b (a (a (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/19.ari b/SRS_Relative/Waldmann_26/19.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (b (a x))))) x)
+(rule x (a (b (a (b (b (a (b (a x)))))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/2.ari b/SRS_Relative/Waldmann_26/2.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (a (a (b (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/20.ari b/SRS_Relative/Waldmann_26/20.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (b (b (b (b x))))))) x)
+(rule x (b (a (b (a (b x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/21.ari b/SRS_Relative/Waldmann_26/21.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (b (b (b (a x))))))) x)
+(rule x (a (b (b (b (a x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/22.ari b/SRS_Relative/Waldmann_26/22.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (b (b (b (a (a x)))))))) x)
+(rule x (a (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/23.ari b/SRS_Relative/Waldmann_26/23.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (a (a (b (b (a x))))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/24.ari b/SRS_Relative/Waldmann_26/24.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (b (b (b (b (b x)))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/25.ari b/SRS_Relative/Waldmann_26/25.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (a (a (b (b (b (b (b x))))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/26.ari b/SRS_Relative/Waldmann_26/26.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (a (b (b (a x)))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/27.ari b/SRS_Relative/Waldmann_26/27.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (b (a (b (b (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/28.ari b/SRS_Relative/Waldmann_26/28.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (b (b (b (a x)))))))) x)
+(rule x (a (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/29.ari b/SRS_Relative/Waldmann_26/29.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (b (b (b (b (b (b x))))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/3.ari b/SRS_Relative/Waldmann_26/3.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (b x))))) x)
+(rule x (b (a (b (a (a (b (a (b x)))))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/30.ari b/SRS_Relative/Waldmann_26/30.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (b (b (b x))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/31.ari b/SRS_Relative/Waldmann_26/31.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (b (b (a (b x))))))) x)
+(rule x (b (b (b (a (a x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/32.ari b/SRS_Relative/Waldmann_26/32.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (b (b (b (a (b (a x)))))))) x)
+(rule x (a (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/33.ari b/SRS_Relative/Waldmann_26/33.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (b (b (a (a (a x))))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/34.ari b/SRS_Relative/Waldmann_26/34.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (a (a x)))))) x)
+(rule x (b (b (b (b (b (b (a x))))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/35.ari b/SRS_Relative/Waldmann_26/35.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (a (a (a (a (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/36.ari b/SRS_Relative/Waldmann_26/36.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (b (a (b (b x))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/37.ari b/SRS_Relative/Waldmann_26/37.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (b (a (a (b x))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/38.ari b/SRS_Relative/Waldmann_26/38.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (a (b (a (b x))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/39.ari b/SRS_Relative/Waldmann_26/39.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (b (a (a (b (b (b (b x))))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/4.ari b/SRS_Relative/Waldmann_26/4.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (b (a (a (b (b (b x)))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/40.ari b/SRS_Relative/Waldmann_26/40.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (a (b (a (a (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/41.ari b/SRS_Relative/Waldmann_26/41.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (b (a (a (b (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/42.ari b/SRS_Relative/Waldmann_26/42.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (a (b (a (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/43.ari b/SRS_Relative/Waldmann_26/43.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (b (b (b (b (a (a x)))))))) x)
+(rule x (a (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/44.ari b/SRS_Relative/Waldmann_26/44.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (a (a (b (b (a x)))))))) x)
+(rule x (b (a (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/45.ari b/SRS_Relative/Waldmann_26/45.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (b (b (a (b (a (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/46.ari b/SRS_Relative/Waldmann_26/46.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (a (b (a (b x))))))) x)
+(rule x (b (b (a (a (a x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/47.ari b/SRS_Relative/Waldmann_26/47.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (a (b (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/48.ari b/SRS_Relative/Waldmann_26/48.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (b (b (b (b (a x)))))))) x)
+(rule x (a (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/49.ari b/SRS_Relative/Waldmann_26/49.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (b (b (a (a x)))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/5.ari b/SRS_Relative/Waldmann_26/5.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (a (a (a (b (b (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/50.ari b/SRS_Relative/Waldmann_26/50.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (b (a (b (a (b (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/51.ari b/SRS_Relative/Waldmann_26/51.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (a (a (b (b (b x))))))) x)
+(rule x (b (a (b (a (b x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/52.ari b/SRS_Relative/Waldmann_26/52.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (a (a (b x))))))) x)
+(rule x (b (a (a (a (b x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/53.ari b/SRS_Relative/Waldmann_26/53.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (b (b (a (a (a x)))))))) x)
+(rule x (a (b (a x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/54.ari b/SRS_Relative/Waldmann_26/54.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (a (a (b (b (a (b x)))))))) x)
+(rule x (b (a (a (b x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/6.ari b/SRS_Relative/Waldmann_26/6.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (b (a (b (b x))))))) x)
+(rule x (b (b (b (a (a x))))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/7.ari b/SRS_Relative/Waldmann_26/7.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (b (a (b (a (b (b x)))))))) x)
+(rule x (b (b (a (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/8.ari b/SRS_Relative/Waldmann_26/8.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (a (a (a (a x)))))))) x)
+(rule x (b (b (b (a x)))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/9.ari b/SRS_Relative/Waldmann_26/9.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (b (a (a (b (b (b (b x)))))))) x)
+(rule x (b (a (b x))) :cost 0)
diff --git a/SRS_Relative/Waldmann_26/README b/SRS_Relative/Waldmann_26/README
@@ -0,0 +1,2 @@
+enumeration of SRS of shape { l -> epsilon, epsilon ->= r }
+not solved by matchbox and mnm (2026) in 1 minute
diff --git a/SRS_Standard/Waldmann_26/1.ari b/SRS_Standard/Waldmann_26/1.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun c 1)
+(fun a 1)
+(rule (c (a (c (a (a x))))) (c (a (c (a (c (a (c (a x)))))))))
+(rule (a (c (c (c x)))) (c (c (c (c (c (a x)))))))
diff --git a/SRS_Standard/Waldmann_26/2.ari b/SRS_Standard/Waldmann_26/2.ari
@@ -0,0 +1,4 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (b (a (a (b (a (b (a (a (b (a (b (a (a (b (a (a (b (a (b (a (a (b (a (b (a (a (b (a x))))))))))))))))))))))))))))) (a (b (a (b (a (a (b (a (b (a (a (b (a (a (b (a (b (a (a (b (a (a (b (a (b (a (a (b (a (b (a (a (b (a (a (b (a (b (a (a (b (a x)))))))))))))))))))))))))))))))))))))))))))
diff --git a/SRS_Standard/Waldmann_26/3.ari b/SRS_Standard/Waldmann_26/3.ari
@@ -0,0 +1,4 @@
+(format TRS)
+(fun a 1)
+(fun b 1)
+(rule (a (a (a (a (a (a (b (a x)))))))) (a (a (b (a (b (a (b (a (a (a (a (a (a x))))))))))))))
diff --git a/SRS_Standard/Waldmann_26/4.ari b/SRS_Standard/Waldmann_26/4.ari
@@ -0,0 +1,4 @@
+(format TRS)
+(fun b 1)
+(fun a 1)
+(rule (b (a (b (a (b (b (a (b (a (b (a (b (a (b (a (b (a (b x)))))))))))))))))) (b (a (b (a (b (a (b (a (b (a (b (a (b (b (a (b (a (b (b (a (b (a (b (a (b x))))))))))))))))))))))))))
diff --git a/SRS_Standard/Waldmann_26/5.ari b/SRS_Standard/Waldmann_26/5.ari
@@ -0,0 +1,5 @@
+(format TRS)
+(fun c 1)
+(fun b 1)
+(rule (c (b (c (b x)))) (b (c (c (b (b x))))))
+(rule (b (b (b (c x)))) (c (b (b (b (b (b x)))))))
diff --git a/SRS_Standard/Waldmann_26/README.md b/SRS_Standard/Waldmann_26/README.md
@@ -0,0 +1,2 @@
+SRS from random enumeration,
+not solvable by matchbox (2026) in 1 minute
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		enumeration of SRS of shape { l -> epsilon, epsilon ->= r }
		not solved by matchbox and mnm (2026) in 1 minute
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		SRS from random enumeration,
		not solvable by matchbox (2026) in 1 minute