R(0) in RNG039-1

prover9.ladr

set(quiet).
clear(auto_denials).
formulas(sos).
-f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f1,f6(f4,f0(f1,f9)))) | -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))) | =(f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))).
f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f1,f6(f4,f0(f1,f9)))).
f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f6(f4,f0(f1,f9)),f6(f4,f0(f1,f9)))).
f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))).
-f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f9,f0(f1,f6(f4,f0(f1,f9))))) | -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f0(f6(f4,f0(f1,f9)),f6(f4,f0(f1,f9)))) | =(f0(f9,f0(f1,f6(f4,f0(f1,f9)))),f6(f4,f0(f1,f9))).
-f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f1,f6(f1,f6(f4,f0(f1,f9))))) | -f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))) | =(f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))).
f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f1,f6(f1,f6(f4,f0(f1,f9))))).
f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f6(f1,f6(f4,f0(f1,f9))),f6(f1,f6(f4,f0(f1,f9))))).
f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))).
-f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))) | -f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f6(f1,f6(f4,f0(f1,f9))),f6(f1,f6(f4,f0(f1,f9))))) | =(f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9)))).
=(f0(f1,f9),f3).
=(f0(f9,f1),f7).
-=(f7,f3).
=(f6(f6(f1,f6(f4,f0(f1,f9))),f6(f1,f6(f4,f0(f1,f9)))),f4).
f8(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))))).
-f8(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))))) | -f8(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))))) | =(f6(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9)))),f6(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))))).
-f5(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9)))))) | -f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f6(f1,f6(f4,f0(f1,f9)))) | -f8(f6(f9,f9),f9,f9) | -f8(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))),f6(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))))) | f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f6(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))))).
f8(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))),f6(f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f1,f6(f4,f0(f1,f9))))).
f8(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))),f6(f6(f1,f6(f4,f0(f1,f9))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9))))))).
f8(f4,f6(f4,f0(f1,f9)),f0(f1,f9)).
-f5(f9,f6(f1,f0(f1,f6(f4,f0(f1,f9)))),f4) | -f5(f9,f0(f1,f6(f4,f0(f1,f9))),f6(f4,f0(f1,f9))) | -f8(f6(f1,f0(f1,f6(f4,f0(f1,f9)))),f0(f1,f6(f4,f0(f1,f9))),f1) | -f8(f4,f6(f4,f0(f1,f9)),f0(f1,f9)) | f5(f9,f1,f0(f1,f9)).
f5(f9,f1,f0(f9,f1)).
f5(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f6(f9,f9),f0(f1,f6(f1,f6(f4,f0(f1,f9)))))).
f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f6(f9,f9),f6(f1,f6(f4,f0(f1,f9))))).
f8(f6(f1,f0(f1,f6(f4,f0(f1,f9)))),f0(f1,f6(f4,f0(f1,f9))),f1).
f8(f6(f9,f9),f9,f9).
-f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f6(f9,f9),f6(f1,f6(f4,f0(f1,f9))))) | -f5(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))) | =(f0(f6(f9,f9),f6(f1,f6(f4,f0(f1,f9)))),f0(f9,f0(f1,f6(f1,f6(f4,f0(f1,f9)))))).
-f5(f9,f1,f0(f9,f1)) | -f5(f9,f1,f0(f1,f9)) | =(f0(f9,f1),f0(f1,f9)).
end_of_list.

smtlib-cnf.smt

(set-logic QF_UF)
(declare-sort S 0)
(declare-fun f5 (S S S ) Bool)
(declare-fun f4 () S)
(declare-fun f7 () S)
(declare-fun f3 () S)
(declare-fun f1 () S)
(declare-fun f6 (S S ) S)
(declare-fun f8 (S S S ) Bool)
(declare-fun f9 () S)
(declare-fun f0 (S S ) S)
(assert (or (or (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f1 (f6 f4 (f0 f1 f9))))) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9))))))) (= (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9)))))))
(assert (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f1 (f6 f4 (f0 f1 f9)))))
(assert (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f4 (f0 f1 f9)) (f6 f4 (f0 f1 f9)))))
(assert (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9))))))
(assert (or (or (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9)))))) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f4 (f0 f1 f9)) (f6 f4 (f0 f1 f9)))))) (= (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9)))) (f6 f4 (f0 f1 f9)))))
(assert (or (or (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))) (= (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))))
(assert (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f1 (f6 f4 (f0 f1 f9))) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))
(assert (or (or (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f1 (f6 f4 (f0 f1 f9))) (f6 f1 (f6 f4 (f0 f1 f9))))))) (= (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (= (f0 f1 f9) f3))
(assert (= (f0 f9 f1) f7))
(assert (not (= f7 f3)))
(assert (= (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f6 f1 (f6 f4 (f0 f1 f9)))) f4))
(assert (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (or (or (not (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))))) (not (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))))) (= (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))) (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))))
(assert (or (or (or (or (not (f5 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f6 f1 (f6 f4 (f0 f1 f9)))))) (not (f8 (f6 f9 f9) f9 f9))) (not (f8 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))) (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))))))
(assert (f8 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))))
(assert (f8 f4 (f6 f4 (f0 f1 f9)) (f0 f1 f9)))
(assert (or (or (or (or (not (f5 f9 (f6 f1 (f0 f1 (f6 f4 (f0 f1 f9)))) f4)) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f6 f4 (f0 f1 f9))))) (not (f8 (f6 f1 (f0 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f4 (f0 f1 f9))) f1))) (not (f8 f4 (f6 f4 (f0 f1 f9)) (f0 f1 f9)))) (f5 f9 f1 (f0 f1 f9))))
(assert (f5 f9 f1 (f0 f9 f1)))
(assert (f5 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))
(assert (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (f8 (f6 f1 (f0 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f4 (f0 f1 f9))) f1))
(assert (f8 (f6 f9 f9) f9 f9))
(assert (or (or (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f6 f1 (f6 f4 (f0 f1 f9)))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))) (= (f0 (f6 f9 f9) (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))))
(assert (or (or (not (f5 f9 f1 (f0 f9 f1))) (not (f5 f9 f1 (f0 f1 f9)))) (= (f0 f9 f1) (f0 f1 f9))))
(check-sat)

smtlib-renamed-vars.smt

(set-logic QF_UF)
(declare-sort S 0)
(declare-fun f5 (S S S ) Bool)
(declare-fun f4 () S)
(declare-fun f7 () S)
(declare-fun f3 () S)
(declare-fun f1 () S)
(declare-fun f6 (S S ) S)
(declare-fun f8 (S S S ) Bool)
(declare-fun f9 () S)
(declare-fun f0 (S S ) S)
(assert (and (and (and (and (or (or (= (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9))))) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f1 (f6 f4 (f0 f1 f9)))))) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9))))))) (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f1 (f6 f4 (f0 f1 f9))))) (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f4 (f0 f1 f9)) (f6 f4 (f0 f1 f9))))) (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9)))))) (or (or (= (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9)))) (f6 f4 (f0 f1 f9))) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 f9 (f0 f1 (f6 f4 (f0 f1 f9))))))) (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f4 (f0 f1 f9)) (f6 f4 (f0 f1 f9))))))))
(assert (and (and (and (and (or (or (= (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))) (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))) (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f1 (f6 f4 (f0 f1 f9))) (f6 f1 (f6 f4 (f0 f1 f9)))))) (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))) (or (or (= (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))) (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f1 (f6 f4 (f0 f1 f9))) (f6 f1 (f6 f4 (f0 f1 f9)))))))))
(assert (= (f0 f1 f9) f3))
(assert (= (f0 f9 f1) f7))
(assert (not (= f7 f3)))
(assert (= (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f6 f1 (f6 f4 (f0 f1 f9)))) f4))
(assert (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (or (not (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))))) (or (not (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))) (= (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))) (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))))))
(assert (or (not (f5 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))) (or (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f6 f1 (f6 f4 (f0 f1 f9))))) (or (not (f8 (f6 f9 f9) f9 f9)) (or (not (f8 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9)))))) (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))))))
(assert (f8 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))) (f6 (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (f8 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))) (f6 (f6 f1 (f6 f4 (f0 f1 f9))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))))
(assert (f8 f4 (f6 f4 (f0 f1 f9)) (f0 f1 f9)))
(assert (or (not (f5 f9 (f6 f1 (f0 f1 (f6 f4 (f0 f1 f9)))) f4)) (or (not (f5 f9 (f0 f1 (f6 f4 (f0 f1 f9))) (f6 f4 (f0 f1 f9)))) (or (not (f8 (f6 f1 (f0 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f4 (f0 f1 f9))) f1)) (or (not (f8 f4 (f6 f4 (f0 f1 f9)) (f0 f1 f9))) (f5 f9 f1 (f0 f1 f9)))))))
(assert (f5 f9 f1 (f0 f9 f1)))
(assert (f5 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))
(assert (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f6 f1 (f6 f4 (f0 f1 f9))))))
(assert (f8 (f6 f1 (f0 f1 (f6 f4 (f0 f1 f9)))) (f0 f1 (f6 f4 (f0 f1 f9))) f1))
(assert (f8 (f6 f9 f9) f9 f9))
(assert (or (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 (f6 f9 f9) (f6 f1 (f6 f4 (f0 f1 f9)))))) (or (not (f5 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9))))))) (= (f0 (f6 f9 f9) (f6 f1 (f6 f4 (f0 f1 f9)))) (f0 f9 (f0 f1 (f6 f1 (f6 f4 (f0 f1 f9)))))))))
(assert (or (not (f5 f9 f1 (f0 f9 f1))) (or (not (f5 f9 f1 (f0 f1 f9))) (= (f0 f9 f1) (f0 f1 f9)))))
(check-sat)

smtlib.smt

(set-logic QF_UF)
(declare-sort S 0)
(declare-fun sum (S S S ) Bool)
(declare-fun b () S)
(declare-fun c () S)
(declare-fun additive_identity () S)
(declare-fun add (S S ) S)
(declare-fun d () S)
(declare-fun product (S S S ) Bool)
(declare-fun a () S)
(declare-fun multiply (S S ) S)
(assert (and (and (and (and (or (or (= (multiply b (add additive_identity (multiply b a))) (multiply a (multiply b (add additive_identity (multiply b a))))) (not (product a (multiply b (add additive_identity (multiply b a))) (multiply b (add additive_identity (multiply b a)))))) (not (product a (multiply b (add additive_identity (multiply b a))) (multiply a (multiply b (add additive_identity (multiply b a))))))) (product a (multiply b (add additive_identity (multiply b a))) (multiply b (add additive_identity (multiply b a))))) (product a (multiply b (add additive_identity (multiply b a))) (multiply (add additive_identity (multiply b a)) (add additive_identity (multiply b a))))) (product a (multiply b (add additive_identity (multiply b a))) (multiply a (multiply b (add additive_identity (multiply b a)))))) (or (or (= (multiply a (multiply b (add additive_identity (multiply b a)))) (add additive_identity (multiply b a))) (not (product a (multiply b (add additive_identity (multiply b a))) (multiply a (multiply b (add additive_identity (multiply b a))))))) (not (product a (multiply b (add additive_identity (multiply b a))) (multiply (add additive_identity (multiply b a)) (add additive_identity (multiply b a))))))))
(assert (and (and (and (and (or (or (= (multiply b (add b (add additive_identity (multiply b a)))) (multiply a (multiply b (add b (add additive_identity (multiply b a)))))) (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply b (add b (add additive_identity (multiply b a))))))) (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply a (multiply b (add b (add additive_identity (multiply b a)))))))) (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply b (add b (add additive_identity (multiply b a)))))) (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply (add b (add additive_identity (multiply b a))) (add b (add additive_identity (multiply b a)))))) (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply a (multiply b (add b (add additive_identity (multiply b a))))))) (or (or (= (multiply a (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a)))) (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply a (multiply b (add b (add additive_identity (multiply b a)))))))) (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply (add b (add additive_identity (multiply b a))) (add b (add additive_identity (multiply b a)))))))))
(assert (= (multiply b a) d))
(assert (= (multiply a b) c))
(assert (not (= c d)))
(assert (= (add (add b (add additive_identity (multiply b a))) (add b (add additive_identity (multiply b a)))) additive_identity))
(assert (sum (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a))))))
(assert (or (not (sum (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a)))))) (or (not (sum (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a)))))))) (= (add (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a)))) (add (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))))))))
(assert (or (not (product (add a a) (multiply b (add b (add additive_identity (multiply b a)))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))))) (or (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (add b (add additive_identity (multiply b a))))) (or (not (sum (add a a) a a)) (or (not (sum (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a))) (add (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a)))))) (product a (multiply b (add b (add additive_identity (multiply b a)))) (add (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a))))))))))
(assert (sum (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a))) (add (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add b (add additive_identity (multiply b a))))))
(assert (sum (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))) (add (add b (add additive_identity (multiply b a))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a))))))))
(assert (sum additive_identity (add additive_identity (multiply b a)) (multiply b a)))
(assert (or (not (product a (add b (multiply b (add additive_identity (multiply b a)))) additive_identity)) (or (not (product a (multiply b (add additive_identity (multiply b a))) (add additive_identity (multiply b a)))) (or (not (sum (add b (multiply b (add additive_identity (multiply b a)))) (multiply b (add additive_identity (multiply b a))) b)) (or (not (sum additive_identity (add additive_identity (multiply b a)) (multiply b a))) (product a b (multiply b a)))))))
(assert (product a b (multiply a b)))
(assert (product (add a a) (multiply b (add b (add additive_identity (multiply b a)))) (multiply (add a a) (multiply b (add b (add additive_identity (multiply b a)))))))
(assert (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply (add a a) (add b (add additive_identity (multiply b a))))))
(assert (sum (add b (multiply b (add additive_identity (multiply b a)))) (multiply b (add additive_identity (multiply b a))) b))
(assert (sum (add a a) a a))
(assert (or (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply (add a a) (add b (add additive_identity (multiply b a)))))) (or (not (product a (multiply b (add b (add additive_identity (multiply b a)))) (multiply a (multiply b (add b (add additive_identity (multiply b a))))))) (= (multiply (add a a) (add b (add additive_identity (multiply b a)))) (multiply a (multiply b (add b (add additive_identity (multiply b a)))))))))
(assert (or (not (product a b (multiply a b))) (or (not (product a b (multiply b a))) (= (multiply a b) (multiply b a)))))
(check-sat)