path: root/test/regress/regress0/quantifiers/ricart-agrawala6.smt2

(set-logic AUFLIA)
(set-info :source | An Optimal Algorithm for Mutual Exclusion in Computer Networks. Glenn Ricart and Ashok K. Agrawala. Communications of the ACM Vol.: 24 Number: 1. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo  de Moura |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(declare-fun s () Int)
(declare-fun s0 (Int) Bool)
(declare-fun s1 (Int) Bool)
(declare-fun s2 (Int) Bool)
(declare-fun s3 (Int) Bool)
(declare-fun s4 (Int) Bool)
(declare-fun s5 (Int) Bool)
(declare-fun s6 (Int) Bool)
(declare-fun rcs1 (Int) Bool)
(declare-fun rcs2 (Int) Bool)
(declare-fun x (Int Int) Bool)
(declare-fun ro (Int Int) Bool)
(declare-fun rd (Int Int) Bool)
(declare-fun sn (Int) Int)
(declare-fun time () Int)
(assert (not (=> (and (forall ((?p Int)) (forall ((?q Int)) (=> (or (s0 ?p) (s5 ?p)) (not (x ?p ?q))))) (forall ((?p Int)) (= (or (s0 ?p) (s6 ?p)) (not (rcs2 ?p)))) (forall ((?p Int)) (< (sn ?p) time)) (forall ((?p Int)) (forall ((?q Int)) (=> (not (= ?p ?q)) (not (= (sn ?p) (sn ?q)))))) (forall ((?p Int)) (forall ((?q Int)) (=> (and (not (= ?p ?q)) (or (and (s4 ?p) (x ?p ?q)) (s5 ?p)) (rcs2 ?q)) (< (sn ?p) (sn ?q))))) (forall ((?p Int)) (forall ((?q Int)) (=> (and (not (= ?p ?q)) (rd ?q ?p)) (ro ?p ?q)))) (forall ((?p Int)) (forall ((?q Int)) (let ((?v_0 (x ?p ?q))) (=> (not (= ?p ?q)) (= (not (or (and (s2 ?p) ?v_0) (and (s3 ?p) (not ?v_0)))) (=> (ro ?p ?q) (rd ?q ?p))))))) (forall ((?p Int)) (forall ((?q Int)) (let ((?v_1 (x ?q ?p))) (let ((?v_2 (or (and (s3 ?q) ?v_1) (and (s4 ?q) (not ?v_1))))) (=> (not (= ?p ?q)) (or (and (s6 ?p) (not (x ?p ?q)) ?v_2) (= (rd ?p ?q) (and ?v_2 (rcs2 ?p) (< (sn ?p) (sn ?q)))))))))) (forall ((?p Int)) (=> (s0 ?p) (not (or (s2 ?p) (s3 ?p) (s4 ?p) (s5 ?p) (s6 ?p))))) (forall ((?p Int)) (=> (s2 ?p) (not (or (s3 ?p) (s4 ?p) (s5 ?p) (s6 ?p))))) (forall ((?p Int)) (=> (s3 ?p) (not (or (s4 ?p) (s5 ?p) (s6 ?p))))) (forall ((?p Int)) (=> (s4 ?p) (not (or (s5 ?p) (s6 ?p))))) (forall ((?p Int)) (=> (s5 ?p) (not (s6 ?p)))) (forall ((?r Int)) (let ((?v_3 (not (= ?r p)))) (=> (s0 ?r) (not (or (s2 ?r) (and ?v_3 (=> ?v_3 (s3 ?r))) (=> ?v_3 (s4 ?r)) (s5 ?r) (s6 ?r)))))) (forall ((?r Int)) (let ((?v_4 (not (= ?r p)))) (=> (s2 ?r) (not (or (and ?v_4 (=> ?v_4 (s3 ?r))) (=> ?v_4 (s4 ?r)) (s5 ?r) (s6 ?r)))))) (forall ((?r Int)) (let ((?v_5 (not (= ?r p)))) (=> (and ?v_5 (=> ?v_5 (s3 ?r))) (not (or (=> ?v_5 (s4 ?r)) (s5 ?r) (s6 ?r)))))) (forall ((?r Int)) (=> (=> (not (= ?r p)) (s4 ?r)) (not (or (s5 ?r) (s6 ?r))))) (forall ((?r Int)) (=> (s5 ?r) (not (s6 ?r)))) (s3 p) (forall ((?q Int)) (=> (not (= ?q p)) (x p ?q)))) (and (forall ((?s Int)) (forall ((?r Int)) (let ((?v_6 (not (= ?s p)))) (=> (or (s0 ?s) (s5 ?s)) (not (and ?v_6 (=> ?v_6 (x ?s ?r)))))))) (forall ((?s Int)) (= (or (s0 ?s) (s6 ?s)) (not (rcs2 ?s)))) (forall ((?s Int)) (< (sn ?s) time)) (forall ((?s Int)) (forall ((?r Int)) (=> (not (= ?s ?r)) (not (= (sn ?s) (sn ?r)))))) (forall ((?s Int)) (forall ((?r Int)) (let ((?v_7 (not (= ?s p)))) (=> (and (not (= ?s ?r)) (or (and (=> ?v_7 (s4 ?s)) ?v_7 (=> ?v_7 (x ?s ?r))) (s5 ?s)) (rcs2 ?r)) (< (sn ?s) (sn ?r)))))) (forall ((?s Int)) (forall ((?r Int)) (=> (and (not (= ?s ?r)) (rd ?r ?s)) (ro ?s ?r)))) (forall ((?s Int)) (forall ((?r Int)) (let ((?v_8 (not (= ?s p)))) (let ((?v_9 (=> ?v_8 (x ?s ?r)))) (=> (not (= ?s ?r)) (= (not (or (and (s2 ?s) ?v_8 ?v_9) (and ?v_8 (=> ?v_8 (s3 ?s)) (not (and ?v_8 ?v_9))))) (=> (ro ?s ?r) (rd ?r ?s)))))))) (forall ((?s Int)) (forall ((?r Int)) (let ((?v_10 (not (= ?s p))) (?v_11 (not (= ?r p)))) (let ((?v_12 (=> ?v_11 (x ?r ?s)))) (let ((?v_13 (or (and ?v_11 (=> ?v_11 (s3 ?r)) ?v_11 ?v_12) (and (=> ?v_11 (s4 ?r)) (not (and ?v_11 ?v_12)))))) (=> (not (= ?s ?r)) (or (and (s6 ?s) (not (and ?v_10 (=> ?v_10 (x ?s ?r)))) ?v_13) (= (rd ?s ?r) (and ?v_13 (rcs2 ?s) (< (sn ?s) (sn ?r)))))))))))))))
(check-sat)
(exit)