; @origtpdbfilename ./TRS/SK90/4.20.trs
; @xtcfilename "./TRS_Standard/SK90/4.20.xml"
(format TRS)
(fun not 1)
(fun xor 2)
(fun true 0)
(fun or 2)
(fun and 2)
(fun implies 2)
(fun false 0)
(rule (not x) (xor x true))
(rule (or x y) (xor (and x y) (xor x y)))
(rule (implies x y) (xor (and x y) (xor x true)))
(rule (and x true) x)
(rule (and x false) false)
(rule (and x x) x)
(rule (xor x false) x)
(rule (xor x x) false)
(rule (and (xor x y) z) (xor (and x z) (and y z)))