(set-logic QF_AUFLIA)
(set-info :source |
Benchmarks used in the followin paper:
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
PDPAR'05
http://www.ai.dist.unige.it/pdpar05/


|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun a_705 () (Array Int Int))
(declare-fun a_707 () (Array Int Int))
(declare-fun a_709 () (Array Int Int))
(declare-fun a_711 () (Array Int Int))
(declare-fun a_713 () (Array Int Int))
(declare-fun a_715 () (Array Int Int))
(declare-fun a_717 () (Array Int Int))
(declare-fun a_719 () (Array Int Int))
(declare-fun a_721 () (Array Int Int))
(declare-fun a_723 () (Array Int Int))
(declare-fun a_725 () (Array Int Int))
(declare-fun a_727 () (Array Int Int))
(declare-fun a_728 () (Array Int Int))
(declare-fun a_729 () (Array Int Int))
(declare-fun e_704 () Int)
(declare-fun e_706 () Int)
(declare-fun e_708 () Int)
(declare-fun e_710 () Int)
(declare-fun e_712 () Int)
(declare-fun e_714 () Int)
(declare-fun e_716 () Int)
(declare-fun e_718 () Int)
(declare-fun e_720 () Int)
(declare-fun e_722 () Int)
(declare-fun e_724 () Int)
(declare-fun e_726 () Int)
(declare-fun e_731 () Int)
(declare-fun e_732 () Int)
(declare-fun i_730 () Int)
(declare-fun a1 () (Array Int Int))
(declare-fun i0 () Int)
(declare-fun i1 () Int)
(declare-fun i2 () Int)
(declare-fun i3 () Int)
(declare-fun i4 () Int)
(declare-fun i5 () Int)
(declare-fun sk ((Array Int Int) (Array Int Int)) Int)
(assert (= a_705 (store a1 i4 e_704)))
(assert (= a_707 (store a_705 i2 e_706)))
(assert (= a_709 (store a_707 i1 e_708)))
(assert (= a_711 (store a_709 i4 e_710)))
(assert (= a_713 (store a_711 i5 e_712)))
(assert (= a_715 (store a_713 i3 e_714)))
(assert (= a_717 (store a_715 i4 e_716)))
(assert (= a_719 (store a_717 i2 e_718)))
(assert (= a_721 (store a_719 i1 e_720)))
(assert (= a_723 (store a_721 i0 e_722)))
(assert (= a_725 (store a_723 i5 e_724)))
(assert (= a_727 (store a_725 i2 e_726)))
(assert (= a_728 (store a_723 i2 e_726)))
(assert (= a_729 (store a_728 i5 e_724)))
(assert (= e_704 (select a1 i2)))
(assert (= e_706 (select a1 i4)))
(assert (= e_708 (select a_707 i4)))
(assert (= e_710 (select a_707 i1)))
(assert (= e_712 (select a_711 i3)))
(assert (= e_714 (select a_711 i5)))
(assert (= e_716 (select a_715 i2)))
(assert (= e_718 (select a_715 i4)))
(assert (= e_720 (select a_719 i0)))
(assert (= e_722 (select a_719 i1)))
(assert (= e_724 (select a_723 i2)))
(assert (= e_726 (select a_723 i5)))
(assert (= e_731 (select a_727 i_730)))
(assert (= e_732 (select a_729 i_730)))
(assert (= i_730 (sk a_727 a_729)))
(assert (not (= e_731 e_732)))
(check-sat)
(exit)