; @origtpdbfilename ./TRS/secret05/cime5.trs
; @xtcfilename "./TRS_Standard/Secret_05_TRS/cime5.xml"
(format TRS)
(fun |intersect'ii'in| 2)
(fun cons 2)
(fun |intersect'ii'out| 0)
(fun |u'1'1| 1)
(fun |u'2'1| 1)
(fun |reduce'ii'in| 2)
(fun sequent 2)
(fun if 2)
(fun |u'3'1| 1)
(fun |x'2b| 2)
(fun |x'2d| 1)
(fun |reduce'ii'out| 0)
(fun iff 2)
(fun |u'4'1| 1)
(fun |x'2a| 2)
(fun |u'5'1| 1)
(fun |u'6'1| 5)
(fun |u'6'2| 1)
(fun |u'7'1| 1)
(fun |u'8'1| 1)
(fun |u'9'1| 1)
(fun p 1)
(fun |u'10'1| 1)
(fun |u'11'1| 1)
(fun |u'12'1| 5)
(fun |u'12'2| 1)
(fun |u'13'1| 1)
(fun nil 0)
(fun |u'14'1| 1)
(fun |u'15'1| 1)
(fun |tautology'i'in| 1)
(fun |u'16'1| 1)
(fun |tautology'i'out| 0)
(rule (|intersect'ii'in| (cons X X0) (cons X X1)) |intersect'ii'out|)
(rule (|intersect'ii'in| Xs (cons X0 Ys)) (|u'1'1| (|intersect'ii'in| Xs Ys)))
(rule (|u'1'1| |intersect'ii'out|) |intersect'ii'out|)
(rule (|intersect'ii'in| (cons X0 Xs) Ys) (|u'2'1| (|intersect'ii'in| Xs Ys)))
(rule (|u'2'1| |intersect'ii'out|) |intersect'ii'out|)
(rule (|reduce'ii'in| (sequent (cons (if A B) Fs) Gs) NF) (|u'3'1| (|reduce'ii'in| (sequent (cons (|x'2b| (|x'2d| B) A) Fs) Gs) NF)))
(rule (|u'3'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent (cons (iff A B) Fs) Gs) NF) (|u'4'1| (|reduce'ii'in| (sequent (cons (|x'2a| (if A B) (if B A)) Fs) Gs) NF)))
(rule (|u'4'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent (cons (|x'2a| F1 F2) Fs) Gs) NF) (|u'5'1| (|reduce'ii'in| (sequent (cons F1 (cons F2 Fs)) Gs) NF)))
(rule (|u'5'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent (cons (|x'2b| F1 F2) Fs) Gs) NF) (|u'6'1| (|reduce'ii'in| (sequent (cons F1 Fs) Gs) NF) F2 Fs Gs NF))
(rule (|u'6'1| |reduce'ii'out| F2 Fs Gs NF) (|u'6'2| (|reduce'ii'in| (sequent (cons F2 Fs) Gs) NF)))
(rule (|u'6'2| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent (cons (|x'2d| F1) Fs) Gs) NF) (|u'7'1| (|reduce'ii'in| (sequent Fs (cons F1 Gs)) NF)))
(rule (|u'7'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent Fs (cons (if A B) Gs)) NF) (|u'8'1| (|reduce'ii'in| (sequent Fs (cons (|x'2b| (|x'2d| B) A) Gs)) NF)))
(rule (|u'8'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent Fs (cons (iff A B) Gs)) NF) (|u'9'1| (|reduce'ii'in| (sequent Fs (cons (|x'2a| (if A B) (if B A)) Gs)) NF)))
(rule (|u'9'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent (cons (p V) Fs) Gs) (sequent Left Right)) (|u'10'1| (|reduce'ii'in| (sequent Fs Gs) (sequent (cons (p V) Left) Right))))
(rule (|u'10'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent Fs (cons (|x'2b| G1 G2) Gs)) NF) (|u'11'1| (|reduce'ii'in| (sequent Fs (cons G1 (cons G2 Gs))) NF)))
(rule (|u'11'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent Fs (cons (|x'2a| G1 G2) Gs)) NF) (|u'12'1| (|reduce'ii'in| (sequent Fs (cons G1 Gs)) NF) Fs G2 Gs NF))
(rule (|u'12'1| |reduce'ii'out| Fs G2 Gs NF) (|u'12'2| (|reduce'ii'in| (sequent Fs (cons G2 Gs)) NF)))
(rule (|u'12'2| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent Fs (cons (|x'2d| G1) Gs)) NF) (|u'13'1| (|reduce'ii'in| (sequent (cons G1 Fs) Gs) NF)))
(rule (|u'13'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent nil (cons (p V) Gs)) (sequent Left Right)) (|u'14'1| (|reduce'ii'in| (sequent nil Gs) (sequent Left (cons (p V) Right)))))
(rule (|u'14'1| |reduce'ii'out|) |reduce'ii'out|)
(rule (|reduce'ii'in| (sequent nil nil) (sequent F1 F2)) (|u'15'1| (|intersect'ii'in| F1 F2)))
(rule (|u'15'1| |intersect'ii'out|) |reduce'ii'out|)
(rule (|tautology'i'in| F) (|u'16'1| (|reduce'ii'in| (sequent nil (cons F nil)) (sequent nil nil))))
(rule (|u'16'1| |reduce'ii'out|) |tautology'i'out|)