; @origtpdbfilename ./TRS/Koprowski/abp2.trs
; @xtcfilename "./TRS_Relative/Mixed_relative_TRS/abp2.xml"
(format TRS)
(fun v2 0)
(fun f 1)
(fun |0| 0)
(fun nils 0)
(fun sys 4)
(fun S 2)
(fun old 0)
(fun p 2)
(fun R 1)
(fun v3 0)
(fun c 2)
(fun T 1)
(fun bot 0)
(fun |1| 0)
(fun P 2)
(fun new 0)
(fun ok 1)
(fun check 1)
(fun F 1)
(fun not 1)
(rule (T (ok (sys x (P d b) (R b) y))) (T (check (sys x bot (R (not b)) y))))
(rule (T (ok (sys (S b (c d ds)) bot y z))) (T (check (sys (S b (c d ds)) (P d b) y z))) :cost 0)
(rule (T (ok (sys (S b (c d ds)) x y (F b)))) (T (check (sys (S (not b) ds) x y bot))) :cost 0)
(rule (T (ok (sys x y (R b) bot))) (T (check (sys x y (R b) (F (not b))))) :cost 0)
(rule (not |1|) |0| :cost 0)
(rule (not |0|) |1| :cost 0)
(rule nils (c new nils) :cost 0)
(rule (p d b) bot :cost 0)
(rule (f b) bot :cost 0)
(rule (check old) (ok old) :cost 0)
(rule (check (f v1)) (f (check v1)) :cost 0)
(rule (f (ok v1)) (ok (f v1)) :cost 0)
(rule (check (p v1 v2)) (p v1 (check v2)) :cost 0)
(rule (check (p v1 v2)) (p (check v1) v2) :cost 0)
(rule (p v1 (ok v2)) (ok (p v1 v2)) :cost 0)
(rule (p (ok v1) v2) (ok (p v1 v2)) :cost 0)
(rule (check (R v1)) (R (check v1)) :cost 0)
(rule (R (ok v1)) (ok (R v1)) :cost 0)
(rule (check (not v1)) (not (check v1)) :cost 0)
(rule (not (ok v1)) (ok (not v1)) :cost 0)
(rule (check (F v1)) (F (check v1)) :cost 0)
(rule (F (ok v1)) (ok (F v1)) :cost 0)
(rule (check (P v1 v2)) (P v1 (check v2)) :cost 0)
(rule (check (P v1 v2)) (P (check v1) v2) :cost 0)
(rule (P v1 (ok v2)) (ok (P v1 v2)) :cost 0)
(rule (P (ok v1) v2) (ok (P v1 v2)) :cost 0)
(rule (check (c v1 v2)) (c v1 (check v2)) :cost 0)
(rule (check (c v1 v2)) (c (check v1) v2) :cost 0)
(rule (c v1 (ok v2)) (ok (c v1 v2)) :cost 0)
(rule (c (ok v1) v2) (ok (c v1 v2)) :cost 0)
(rule (check (S v1 v2)) (S v1 (check v2)) :cost 0)
(rule (check (S v1 v2)) (S (check v1) v2) :cost 0)
(rule (S v1 (ok v2)) (ok (S v1 v2)) :cost 0)
(rule (S (ok v1) v2) (ok (S v1 v2)) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys v1 v2 v3 (check v4)) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys v1 v2 (check v3) v4) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys v1 (check v2) v3 v4) :cost 0)
(rule (check (sys v1 v2 v3 v4)) (sys (check v1) v2 v3 v4) :cost 0)
(rule (sys v1 v2 v3 (ok v4)) (ok (sys v1 v2 v3 v4)) :cost 0)
(rule (sys v1 v2 (ok v3) v4) (ok (sys v1 v2 v3 v4)) :cost 0)
(rule (sys v1 (ok v2) v3 v4) (ok (sys v1 v2 v3 v4)) :cost 0)
(rule (sys (ok v1) v2 v3 v4) (ok (sys v1 v2 v3 v4)) :cost 0)