Problem CiME 04 mucrl1

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 mucrl1

stdout:

MAYBE

Problem:
 or(T(),T()) -> T()
 or(F(),T()) -> T()
 or(T(),F()) -> T()
 or(F(),F()) -> F()
 and(T(),B) -> B
 and(B,T()) -> B
 and(F(),B) -> F()
 and(B,F()) -> F()
 imp(T(),B) -> B
 imp(F(),B) -> T()
 not(T()) -> F()
 not(F()) -> T()
 if(T(),B1,B2) -> B1
 if(F(),B1,B2) -> B2
 eq(T(),T()) -> T()
 eq(F(),F()) -> T()
 eq(T(),F()) -> F()
 eq(F(),T()) -> F()
 eqt(nil(),undefined()) -> F()
 eqt(nil(),pid(N2)) -> F()
 eqt(nil(),int(N2)) -> F()
 eqt(nil(),cons(H2,T2)) -> F()
 eqt(nil(),tuple(H2,T2)) -> F()
 eqt(nil(),tuplenil(H2)) -> F()
 eqt(a(),nil()) -> F()
 eqt(a(),a()) -> T()
 eqt(a(),excl()) -> F()
 eqt(a(),false()) -> F()
 eqt(a(),lock()) -> F()
 eqt(a(),locker()) -> F()
 eqt(a(),mcrlrecord()) -> F()
 eqt(a(),ok()) -> F()
 eqt(a(),pending()) -> F()
 eqt(a(),release()) -> F()
 eqt(a(),request()) -> F()
 eqt(a(),resource()) -> F()
 eqt(a(),tag()) -> F()
 eqt(a(),true()) -> F()
 eqt(a(),undefined()) -> F()
 eqt(a(),pid(N2)) -> F()
 eqt(a(),int(N2)) -> F()
 eqt(a(),cons(H2,T2)) -> F()
 eqt(a(),tuple(H2,T2)) -> F()
 eqt(a(),tuplenil(H2)) -> F()
 eqt(excl(),nil()) -> F()
 eqt(excl(),a()) -> F()
 eqt(excl(),excl()) -> T()
 eqt(excl(),false()) -> F()
 eqt(excl(),lock()) -> F()
 eqt(excl(),locker()) -> F()
 eqt(excl(),mcrlrecord()) -> F()
 eqt(excl(),ok()) -> F()
 eqt(excl(),pending()) -> F()
 eqt(excl(),release()) -> F()
 eqt(excl(),request()) -> F()
 eqt(excl(),resource()) -> F()
 eqt(excl(),tag()) -> F()
 eqt(excl(),true()) -> F()
 eqt(excl(),undefined()) -> F()
 eqt(excl(),pid(N2)) -> F()
 eqt(excl(),eqt(false(),int(N2))) -> F()
 eqt(false(),cons(H2,T2)) -> F()
 eqt(false(),tuple(H2,T2)) -> F()
 eqt(false(),tuplenil(H2)) -> F()
 eqt(lock(),nil()) -> F()
 eqt(lock(),a()) -> F()
 eqt(lock(),excl()) -> F()
 eqt(lock(),false()) -> F()
 eqt(lock(),lock()) -> T()
 eqt(lock(),locker()) -> F()
 eqt(lock(),mcrlrecord()) -> F()
 eqt(lock(),ok()) -> F()
 eqt(lock(),pending()) -> F()
 eqt(lock(),release()) -> F()
 eqt(lock(),request()) -> F()
 eqt(lock(),resource()) -> F()
 eqt(lock(),tag()) -> F()
 eqt(lock(),true()) -> F()
 eqt(lock(),undefined()) -> F()
 eqt(lock(),pid(N2)) -> F()
 eqt(lock(),int(N2)) -> F()
 eqt(lock(),cons(H2,T2)) -> F()
 eqt(lock(),tuple(H2,T2)) -> F()
 eqt(lock(),tuplenil(H2)) -> F()
 eqt(locker(),nil()) -> F()
 eqt(locker(),a()) -> F()
 eqt(locker(),excl()) -> F()
 eqt(locker(),false()) -> F()
 eqt(locker(),lock()) -> F()
 eqt(locker(),locker()) -> T()
 eqt(locker(),mcrlrecord()) -> F()
 eqt(locker(),ok()) -> F()
 eqt(locker(),pending()) -> F()
 eqt(locker(),release()) -> F()
 eqt(locker(),request()) -> F()
 eqt(locker(),resource()) -> F()
 eqt(locker(),tag()) -> F()
 eqt(locker(),true()) -> F()
 eqt(locker(),undefined()) -> F()
 eqt(locker(),pid(N2)) -> F()
 eqt(locker(),int(N2)) -> F()
 eqt(locker(),cons(H2,T2)) -> F()
 eqt(locker(),tuple(H2,T2)) -> F()
 eqt(locker(),tuplenil(H2)) -> F()
 eqt(mcrlrecord(),nil()) -> F()
 eqt(mcrlrecord(),a()) -> F()
 eqt(mcrlrecord(),excl()) -> F()
 eqt(mcrlrecord(),false()) -> F()
 eqt(mcrlrecord(),lock()) -> F()
 eqt(mcrlrecord(),locker()) -> F()
 eqt(mcrlrecord(),mcrlrecord()) -> T()
 eqt(mcrlrecord(),ok()) -> F()
 eqt(mcrlrecord(),pending()) -> F()
 eqt(mcrlrecord(),release()) -> F()
 eqt(mcrlrecord(),request()) -> F()
 eqt(mcrlrecord(),resource()) -> F()
 eqt(ok(),resource()) -> F()
 eqt(ok(),tag()) -> F()
 eqt(ok(),true()) -> F()
 eqt(ok(),undefined()) -> F()
 eqt(ok(),pid(N2)) -> F()
 eqt(ok(),int(N2)) -> F()
 eqt(ok(),cons(H2,T2)) -> F()
 eqt(ok(),tuple(H2,T2)) -> F()
 eqt(ok(),tuplenil(H2)) -> F()
 eqt(pending(),nil()) -> F()
 eqt(pending(),a()) -> F()
 eqt(pending(),excl()) -> F()
 eqt(pending(),false()) -> F()
 eqt(pending(),lock()) -> F()
 eqt(pending(),locker()) -> F()
 eqt(pending(),mcrlrecord()) -> F()
 eqt(pending(),ok()) -> F()
 eqt(pending(),pending()) -> T()
 eqt(pending(),release()) -> F()
 eqt(pending(),request()) -> F()
 eqt(pending(),resource()) -> F()
 eqt(pending(),tag()) -> F()
 eqt(pending(),true()) -> F()
 eqt(pending(),undefined()) -> F()
 eqt(pending(),pid(N2)) -> F()
 eqt(pending(),int(N2)) -> F()
 eqt(pending(),cons(H2,T2)) -> F()
 eqt(pending(),tuple(H2,T2)) -> F()
 eqt(pending(),tuplenil(H2)) -> F()
 eqt(release(),nil()) -> F()
 eqt(release(),a()) -> F()
 eqt(release(),excl()) -> F()
 eqt(release(),false()) -> F()
 eqt(release(),lock()) -> F()
 eqt(release(),locker()) -> F()
 eqt(release(),mcrlrecord()) -> F()
 eqt(release(),ok()) -> F()
 eqt(request(),mcrlrecord()) -> F()
 eqt(request(),ok()) -> F()
 eqt(request(),pending()) -> F()
 eqt(request(),release()) -> F()
 eqt(request(),request()) -> T()
 eqt(request(),resource()) -> F()
 eqt(request(),tag()) -> F()
 eqt(request(),true()) -> F()
 eqt(request(),undefined()) -> F()
 eqt(request(),pid(N2)) -> F()
 eqt(request(),int(N2)) -> F()
 eqt(request(),cons(H2,T2)) -> F()
 eqt(request(),tuple(H2,T2)) -> F()
 eqt(request(),tuplenil(H2)) -> F()
 eqt(resource(),nil()) -> F()
 eqt(resource(),a()) -> F()
 eqt(resource(),excl()) -> F()
 eqt(resource(),false()) -> F()
 eqt(resource(),lock()) -> F()
 eqt(resource(),locker()) -> F()
 eqt(resource(),mcrlrecord()) -> F()
 eqt(resource(),ok()) -> F()
 eqt(resource(),pending()) -> F()
 eqt(resource(),release()) -> F()
 eqt(resource(),request()) -> F()
 eqt(resource(),resource()) -> T()
 eqt(resource(),tag()) -> F()
 eqt(resource(),true()) -> F()
 eqt(resource(),undefined()) -> F()
 eqt(resource(),pid(N2)) -> F()
 eqt(resource(),int(N2)) -> F()
 eqt(resource(),cons(H2,T2)) -> F()
 eqt(resource(),tuple(H2,T2)) -> F()
 eqt(resource(),tuplenil(H2)) -> F()
 eqt(tag(),nil()) -> F()
 eqt(tag(),a()) -> F()
 eqt(tag(),excl()) -> F()
 eqt(tag(),false()) -> F()
 eqt(tag(),lock()) -> F()
 eqt(tag(),locker()) -> F()
 eqt(tag(),mcrlrecord()) -> F()
 eqt(tag(),ok()) -> F()
 eqt(tag(),pending()) -> F()
 eqt(tag(),release()) -> F()
 eqt(tag(),request()) -> F()
 eqt(tag(),resource()) -> F()
 eqt(tag(),tag()) -> T()
 eqt(tag(),true()) -> F()
 eqt(tag(),undefined()) -> F()
 eqt(tag(),pid(N2)) -> F()
 eqt(tag(),int(N2)) -> F()
 eqt(tag(),cons(H2,T2)) -> F()
 eqt(tag(),tuple(H2,T2)) -> F()
 eqt(tag(),tuplenil(H2)) -> F()
 eqt(true(),nil()) -> F()
 eqt(true(),a()) -> F()
 eqt(true(),excl()) -> F()
 eqt(true(),false()) -> F()
 eqt(true(),lock()) -> F()
 eqt(true(),locker()) -> F()
 eqt(true(),mcrlrecord()) -> F()
 eqt(true(),ok()) -> F()
 eqt(true(),pending()) -> F()
 eqt(true(),release()) -> F()
 eqt(true(),request()) -> F()
 eqt(true(),resource()) -> F()
 eqt(true(),tag()) -> F()
 eqt(true(),true()) -> T()
 eqt(true(),undefined()) -> F()
 eqt(true(),pid(N2)) -> F()
 eqt(true(),int(N2)) -> F()
 eqt(true(),cons(H2,T2)) -> F()
 eqt(true(),tuple(H2,T2)) -> F()
 eqt(true(),tuplenil(H2)) -> F()
 eqt(undefined(),nil()) -> F()
 eqt(undefined(),a()) -> F()
 eqt(undefined(),tuplenil(H2)) -> F()
 eqt(pid(N1),nil()) -> F()
 eqt(pid(N1),a()) -> F()
 eqt(pid(N1),excl()) -> F()
 eqt(pid(N1),false()) -> F()
 eqt(pid(N1),lock()) -> F()
 eqt(pid(N1),locker()) -> F()
 eqt(pid(N1),mcrlrecord()) -> F()
 eqt(pid(N1),ok()) -> F()
 eqt(pid(N1),pending()) -> F()
 eqt(pid(N1),release()) -> F()
 eqt(pid(N1),request()) -> F()
 eqt(pid(N1),resource()) -> F()
 eqt(pid(N1),tag()) -> F()
 eqt(pid(N1),true()) -> F()
 eqt(pid(N1),undefined()) -> F()
 eqt(pid(N1),pid(N2)) -> eqt(N1,N2)
 eqt(pid(N1),int(N2)) -> F()
 eqt(pid(N1),cons(H2,T2)) -> F()
 eqt(pid(N1),tuple(H2,T2)) -> F()
 eqt(pid(N1),tuplenil(H2)) -> F()
 eqt(int(N1),nil()) -> F()
 eqt(int(N1),a()) -> F()
 eqt(int(N1),excl()) -> F()
 eqt(int(N1),false()) -> F()
 eqt(int(N1),lock()) -> F()
 eqt(int(N1),locker()) -> F()
 eqt(int(N1),mcrlrecord()) -> F()
 eqt(int(N1),ok()) -> F()
 eqt(int(N1),pending()) -> F()
 eqt(int(N1),release()) -> F()
 eqt(int(N1),request()) -> F()
 eqt(int(N1),resource()) -> F()
 eqt(int(N1),tag()) -> F()
 eqt(int(N1),true()) -> F()
 eqt(int(N1),undefined()) -> F()
 eqt(cons(H1,T1),resource()) -> F()
 eqt(cons(H1,T1),tag()) -> F()
 eqt(cons(H1,T1),true()) -> F()
 eqt(cons(H1,T1),undefined()) -> F()
 eqt(cons(H1,T1),pid(N2)) -> F()
 eqt(cons(H1,T1),int(N2)) -> F()
 eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
 eqt(cons(H1,T1),tuple(H2,T2)) -> F()
 eqt(cons(H1,T1),tuplenil(H2)) -> F()
 eqt(tuple(H1,T1),nil()) -> F()
 eqt(tuple(H1,T1),a()) -> F()
 eqt(tuple(H1,T1),excl()) -> F()
 eqt(tuple(H1,T1),false()) -> F()
 eqt(tuple(H1,T1),lock()) -> F()
 eqt(tuple(H1,T1),locker()) -> F()
 eqt(tuple(H1,T1),mcrlrecord()) -> F()
 eqt(tuple(H1,T1),ok()) -> F()
 eqt(tuple(H1,T1),pending()) -> F()
 eqt(tuple(H1,T1),release()) -> F()
 eqt(tuple(H1,T1),request()) -> F()
 eqt(tuple(H1,T1),resource()) -> F()
 eqt(tuple(H1,T1),tag()) -> F()
 eqt(tuple(H1,T1),true()) -> F()
 eqt(tuple(H1,T1),undefined()) -> F()
 eqt(tuple(H1,T1),pid(N2)) -> F()
 eqt(tuple(H1,T1),int(N2)) -> F()
 eqt(tuple(H1,T1),cons(H2,T2)) -> F()
 eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2))
 eqt(tuple(H1,T1),tuplenil(H2)) -> F()
 eqt(tuplenil(H1),nil()) -> F()
 eqt(tuplenil(H1),a()) -> F()
 eqt(tuplenil(H1),excl()) -> F()
 eqt(tuplenil(H1),false()) -> F()
 eqt(tuplenil(H1),lock()) -> F()
 eqt(tuplenil(H1),locker()) -> F()
 eqt(tuplenil(H1),mcrlrecord()) -> F()
 eqt(tuplenil(H1),ok()) -> F()
 eqt(tuplenil(H1),pending()) -> F()
 eqt(tuplenil(H1),release()) -> F()
 eqt(tuplenil(H1),request()) -> F()
 eqt(tuplenil(H1),resource()) -> F()
 eqt(tuplenil(H1),tag()) -> F()
 eqt(tuplenil(H1),true()) -> F()
 eqt(tuplenil(H1),undefined()) -> F()
 eqt(tuplenil(H1),pid(N2)) -> F()
 eqt(tuplenil(H1),int(N2)) -> F()
 eqt(tuplenil(H1),cons(H2,T2)) -> F()
 eqt(tuplenil(H1),tuple(H2,T2)) -> F()
 eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2)
 element(int(s(0())),tuplenil(T1)) -> T1
 element(int(s(0())),tuple(T1,T2)) -> T1
 element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2)
 record_new(lock()) ->
 tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil())))))
 record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),
                lock(),resource())
 -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2)))))
 record_update(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),
               lock(),pending(),NewF)
 -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(NewF)))))
 record_updates(Record,Name,nil()) -> Record
 record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) ->
 record_updates(record_update(Record,Name,Field,NewF),Name,Fields)
 locker2_map_promote_pending(nil(),Pending) -> nil()
 locker2_map_promote_pending(cons(Lock,Locks),Pending) ->
 cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending))
 locker2_map_claim_lock(nil(),Resources,Client) -> nil()
 locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) ->
 cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client))
 locker2_map_add_pending(nil(),Resources,Client) -> nil()
 locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending()))
 case0(Client,Lock,cons(Client,Pendings)) ->
 record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons(
                                                                    tuple
                                                                    (
                                                                    pending(),tuplenil(Pendings)),
                                                                    nil
                                                                    ())))
 case0(Client,Lock,MCRLFree0) -> Lock
 locker2_remove_pending(Lock,Client) ->
 record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract
                                                                   (Lock,lock(),pending()),
                                                                   cons
                                                                   (Client,nil())))),
                                 nil()))
 locker2_add_pending(Lock,Resources,Client) ->
 case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources))
 case1(Client,Resources,Lock,true()) ->
 record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract
                                                                 (Lock,lock(),pending()),
                                                                 cons
                                                                 (Client,nil())))),
                                 nil()))
 case1(Client,Resources,Lock,false()) -> Lock
 locker2_release_lock(Lock,Client) ->
 case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl())))
 case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil()))
 case4(Client,Lock,MCRLFree1) -> false()
 locker2_obtainables(nil(),Client) -> true()
 locker2_obtainables(cons(Lock,Locks),Client) ->
 case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending())))
 case5(Client,Locks,Lock,true()) ->
 andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client))
 case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client)
 locker2_check_available(Resource,nil()) -> false()
 locker2_check_available(Resource,cons(Lock,Locks)) ->
 case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource())))
 case6(Locks,Lock,Resource,true()) ->
 andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()),
                                                            nil()))
 case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks)
 locker2_check_availables(nil(),Locks) -> true()
 locker2_check_availables(cons(Resource,Resources),Locks) ->
 andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks))
 locker2_adduniq(nil(),List) -> List
 append(cons(Head,Tail),List) -> cons(Head,append(Tail,List))
 subtract(List,nil()) -> List
 subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail)
 delete(E,nil()) -> nil()
 delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head))
 case8(Tail,Head,E,true()) -> Tail
 case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail))
 gen_tag(Pid) -> tuple(Pid,tuplenil(tag()))
 gen_modtageq(Client1,Client2) -> equal(Client1,Client2)
 member(E,nil()) -> false()
 member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head))
 case9(Tail,Head,E,true()) -> true()
 case9(Tail,Head,E,false()) -> member(E,Tail)
 eqs(empty(),empty()) -> T()
 eqs(empty(),stack(E2,S2)) -> F()
 eqs(stack(E1,S1),empty()) -> F()
 eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2))
 pushs(E1,S1) -> stack(E1,S1)
 pops(stack(E1,S1)) -> S1
 tops(stack(E1,S1)) -> E1
 istops(E1,empty()) -> F()
 istops(E1,stack(E2,S1)) -> eqt(E1,E2)
 eqc(nocalls(),nocalls()) -> T()
 eqc(nocalls(),calls(E2,S2,CS2)) -> F()
 eqc(calls(E1,S1,CS1),nocalls()) -> F()
 eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2)))
 push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls())
 push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3))
 push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1)

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 mucrl1

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 mucrl1

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  or(T(), T()) -> T()
     , or(F(), T()) -> T()
     , or(T(), F()) -> T()
     , or(F(), F()) -> F()
     , and(T(), B) -> B
     , and(B, T()) -> B
     , and(F(), B) -> F()
     , and(B, F()) -> F()
     , imp(T(), B) -> B
     , imp(F(), B) -> T()
     , not(T()) -> F()
     , not(F()) -> T()
     , if(T(), B1, B2) -> B1
     , if(F(), B1, B2) -> B2
     , eq(T(), T()) -> T()
     , eq(F(), F()) -> T()
     , eq(T(), F()) -> F()
     , eq(F(), T()) -> F()
     , eqt(nil(), undefined()) -> F()
     , eqt(nil(), pid(N2)) -> F()
     , eqt(nil(), int(N2)) -> F()
     , eqt(nil(), cons(H2, T2)) -> F()
     , eqt(nil(), tuple(H2, T2)) -> F()
     , eqt(nil(), tuplenil(H2)) -> F()
     , eqt(a(), nil()) -> F()
     , eqt(a(), a()) -> T()
     , eqt(a(), excl()) -> F()
     , eqt(a(), false()) -> F()
     , eqt(a(), lock()) -> F()
     , eqt(a(), locker()) -> F()
     , eqt(a(), mcrlrecord()) -> F()
     , eqt(a(), ok()) -> F()
     , eqt(a(), pending()) -> F()
     , eqt(a(), release()) -> F()
     , eqt(a(), request()) -> F()
     , eqt(a(), resource()) -> F()
     , eqt(a(), tag()) -> F()
     , eqt(a(), true()) -> F()
     , eqt(a(), undefined()) -> F()
     , eqt(a(), pid(N2)) -> F()
     , eqt(a(), int(N2)) -> F()
     , eqt(a(), cons(H2, T2)) -> F()
     , eqt(a(), tuple(H2, T2)) -> F()
     , eqt(a(), tuplenil(H2)) -> F()
     , eqt(excl(), nil()) -> F()
     , eqt(excl(), a()) -> F()
     , eqt(excl(), excl()) -> T()
     , eqt(excl(), false()) -> F()
     , eqt(excl(), lock()) -> F()
     , eqt(excl(), locker()) -> F()
     , eqt(excl(), mcrlrecord()) -> F()
     , eqt(excl(), ok()) -> F()
     , eqt(excl(), pending()) -> F()
     , eqt(excl(), release()) -> F()
     , eqt(excl(), request()) -> F()
     , eqt(excl(), resource()) -> F()
     , eqt(excl(), tag()) -> F()
     , eqt(excl(), true()) -> F()
     , eqt(excl(), undefined()) -> F()
     , eqt(excl(), pid(N2)) -> F()
     , eqt(excl(), eqt(false(), int(N2))) -> F()
     , eqt(false(), cons(H2, T2)) -> F()
     , eqt(false(), tuple(H2, T2)) -> F()
     , eqt(false(), tuplenil(H2)) -> F()
     , eqt(lock(), nil()) -> F()
     , eqt(lock(), a()) -> F()
     , eqt(lock(), excl()) -> F()
     , eqt(lock(), false()) -> F()
     , eqt(lock(), lock()) -> T()
     , eqt(lock(), locker()) -> F()
     , eqt(lock(), mcrlrecord()) -> F()
     , eqt(lock(), ok()) -> F()
     , eqt(lock(), pending()) -> F()
     , eqt(lock(), release()) -> F()
     , eqt(lock(), request()) -> F()
     , eqt(lock(), resource()) -> F()
     , eqt(lock(), tag()) -> F()
     , eqt(lock(), true()) -> F()
     , eqt(lock(), undefined()) -> F()
     , eqt(lock(), pid(N2)) -> F()
     , eqt(lock(), int(N2)) -> F()
     , eqt(lock(), cons(H2, T2)) -> F()
     , eqt(lock(), tuple(H2, T2)) -> F()
     , eqt(lock(), tuplenil(H2)) -> F()
     , eqt(locker(), nil()) -> F()
     , eqt(locker(), a()) -> F()
     , eqt(locker(), excl()) -> F()
     , eqt(locker(), false()) -> F()
     , eqt(locker(), lock()) -> F()
     , eqt(locker(), locker()) -> T()
     , eqt(locker(), mcrlrecord()) -> F()
     , eqt(locker(), ok()) -> F()
     , eqt(locker(), pending()) -> F()
     , eqt(locker(), release()) -> F()
     , eqt(locker(), request()) -> F()
     , eqt(locker(), resource()) -> F()
     , eqt(locker(), tag()) -> F()
     , eqt(locker(), true()) -> F()
     , eqt(locker(), undefined()) -> F()
     , eqt(locker(), pid(N2)) -> F()
     , eqt(locker(), int(N2)) -> F()
     , eqt(locker(), cons(H2, T2)) -> F()
     , eqt(locker(), tuple(H2, T2)) -> F()
     , eqt(locker(), tuplenil(H2)) -> F()
     , eqt(mcrlrecord(), nil()) -> F()
     , eqt(mcrlrecord(), a()) -> F()
     , eqt(mcrlrecord(), excl()) -> F()
     , eqt(mcrlrecord(), false()) -> F()
     , eqt(mcrlrecord(), lock()) -> F()
     , eqt(mcrlrecord(), locker()) -> F()
     , eqt(mcrlrecord(), mcrlrecord()) -> T()
     , eqt(mcrlrecord(), ok()) -> F()
     , eqt(mcrlrecord(), pending()) -> F()
     , eqt(mcrlrecord(), release()) -> F()
     , eqt(mcrlrecord(), request()) -> F()
     , eqt(mcrlrecord(), resource()) -> F()
     , eqt(ok(), resource()) -> F()
     , eqt(ok(), tag()) -> F()
     , eqt(ok(), true()) -> F()
     , eqt(ok(), undefined()) -> F()
     , eqt(ok(), pid(N2)) -> F()
     , eqt(ok(), int(N2)) -> F()
     , eqt(ok(), cons(H2, T2)) -> F()
     , eqt(ok(), tuple(H2, T2)) -> F()
     , eqt(ok(), tuplenil(H2)) -> F()
     , eqt(pending(), nil()) -> F()
     , eqt(pending(), a()) -> F()
     , eqt(pending(), excl()) -> F()
     , eqt(pending(), false()) -> F()
     , eqt(pending(), lock()) -> F()
     , eqt(pending(), locker()) -> F()
     , eqt(pending(), mcrlrecord()) -> F()
     , eqt(pending(), ok()) -> F()
     , eqt(pending(), pending()) -> T()
     , eqt(pending(), release()) -> F()
     , eqt(pending(), request()) -> F()
     , eqt(pending(), resource()) -> F()
     , eqt(pending(), tag()) -> F()
     , eqt(pending(), true()) -> F()
     , eqt(pending(), undefined()) -> F()
     , eqt(pending(), pid(N2)) -> F()
     , eqt(pending(), int(N2)) -> F()
     , eqt(pending(), cons(H2, T2)) -> F()
     , eqt(pending(), tuple(H2, T2)) -> F()
     , eqt(pending(), tuplenil(H2)) -> F()
     , eqt(release(), nil()) -> F()
     , eqt(release(), a()) -> F()
     , eqt(release(), excl()) -> F()
     , eqt(release(), false()) -> F()
     , eqt(release(), lock()) -> F()
     , eqt(release(), locker()) -> F()
     , eqt(release(), mcrlrecord()) -> F()
     , eqt(release(), ok()) -> F()
     , eqt(request(), mcrlrecord()) -> F()
     , eqt(request(), ok()) -> F()
     , eqt(request(), pending()) -> F()
     , eqt(request(), release()) -> F()
     , eqt(request(), request()) -> T()
     , eqt(request(), resource()) -> F()
     , eqt(request(), tag()) -> F()
     , eqt(request(), true()) -> F()
     , eqt(request(), undefined()) -> F()
     , eqt(request(), pid(N2)) -> F()
     , eqt(request(), int(N2)) -> F()
     , eqt(request(), cons(H2, T2)) -> F()
     , eqt(request(), tuple(H2, T2)) -> F()
     , eqt(request(), tuplenil(H2)) -> F()
     , eqt(resource(), nil()) -> F()
     , eqt(resource(), a()) -> F()
     , eqt(resource(), excl()) -> F()
     , eqt(resource(), false()) -> F()
     , eqt(resource(), lock()) -> F()
     , eqt(resource(), locker()) -> F()
     , eqt(resource(), mcrlrecord()) -> F()
     , eqt(resource(), ok()) -> F()
     , eqt(resource(), pending()) -> F()
     , eqt(resource(), release()) -> F()
     , eqt(resource(), request()) -> F()
     , eqt(resource(), resource()) -> T()
     , eqt(resource(), tag()) -> F()
     , eqt(resource(), true()) -> F()
     , eqt(resource(), undefined()) -> F()
     , eqt(resource(), pid(N2)) -> F()
     , eqt(resource(), int(N2)) -> F()
     , eqt(resource(), cons(H2, T2)) -> F()
     , eqt(resource(), tuple(H2, T2)) -> F()
     , eqt(resource(), tuplenil(H2)) -> F()
     , eqt(tag(), nil()) -> F()
     , eqt(tag(), a()) -> F()
     , eqt(tag(), excl()) -> F()
     , eqt(tag(), false()) -> F()
     , eqt(tag(), lock()) -> F()
     , eqt(tag(), locker()) -> F()
     , eqt(tag(), mcrlrecord()) -> F()
     , eqt(tag(), ok()) -> F()
     , eqt(tag(), pending()) -> F()
     , eqt(tag(), release()) -> F()
     , eqt(tag(), request()) -> F()
     , eqt(tag(), resource()) -> F()
     , eqt(tag(), tag()) -> T()
     , eqt(tag(), true()) -> F()
     , eqt(tag(), undefined()) -> F()
     , eqt(tag(), pid(N2)) -> F()
     , eqt(tag(), int(N2)) -> F()
     , eqt(tag(), cons(H2, T2)) -> F()
     , eqt(tag(), tuple(H2, T2)) -> F()
     , eqt(tag(), tuplenil(H2)) -> F()
     , eqt(true(), nil()) -> F()
     , eqt(true(), a()) -> F()
     , eqt(true(), excl()) -> F()
     , eqt(true(), false()) -> F()
     , eqt(true(), lock()) -> F()
     , eqt(true(), locker()) -> F()
     , eqt(true(), mcrlrecord()) -> F()
     , eqt(true(), ok()) -> F()
     , eqt(true(), pending()) -> F()
     , eqt(true(), release()) -> F()
     , eqt(true(), request()) -> F()
     , eqt(true(), resource()) -> F()
     , eqt(true(), tag()) -> F()
     , eqt(true(), true()) -> T()
     , eqt(true(), undefined()) -> F()
     , eqt(true(), pid(N2)) -> F()
     , eqt(true(), int(N2)) -> F()
     , eqt(true(), cons(H2, T2)) -> F()
     , eqt(true(), tuple(H2, T2)) -> F()
     , eqt(true(), tuplenil(H2)) -> F()
     , eqt(undefined(), nil()) -> F()
     , eqt(undefined(), a()) -> F()
     , eqt(undefined(), tuplenil(H2)) -> F()
     , eqt(pid(N1), nil()) -> F()
     , eqt(pid(N1), a()) -> F()
     , eqt(pid(N1), excl()) -> F()
     , eqt(pid(N1), false()) -> F()
     , eqt(pid(N1), lock()) -> F()
     , eqt(pid(N1), locker()) -> F()
     , eqt(pid(N1), mcrlrecord()) -> F()
     , eqt(pid(N1), ok()) -> F()
     , eqt(pid(N1), pending()) -> F()
     , eqt(pid(N1), release()) -> F()
     , eqt(pid(N1), request()) -> F()
     , eqt(pid(N1), resource()) -> F()
     , eqt(pid(N1), tag()) -> F()
     , eqt(pid(N1), true()) -> F()
     , eqt(pid(N1), undefined()) -> F()
     , eqt(pid(N1), pid(N2)) -> eqt(N1, N2)
     , eqt(pid(N1), int(N2)) -> F()
     , eqt(pid(N1), cons(H2, T2)) -> F()
     , eqt(pid(N1), tuple(H2, T2)) -> F()
     , eqt(pid(N1), tuplenil(H2)) -> F()
     , eqt(int(N1), nil()) -> F()
     , eqt(int(N1), a()) -> F()
     , eqt(int(N1), excl()) -> F()
     , eqt(int(N1), false()) -> F()
     , eqt(int(N1), lock()) -> F()
     , eqt(int(N1), locker()) -> F()
     , eqt(int(N1), mcrlrecord()) -> F()
     , eqt(int(N1), ok()) -> F()
     , eqt(int(N1), pending()) -> F()
     , eqt(int(N1), release()) -> F()
     , eqt(int(N1), request()) -> F()
     , eqt(int(N1), resource()) -> F()
     , eqt(int(N1), tag()) -> F()
     , eqt(int(N1), true()) -> F()
     , eqt(int(N1), undefined()) -> F()
     , eqt(cons(H1, T1), resource()) -> F()
     , eqt(cons(H1, T1), tag()) -> F()
     , eqt(cons(H1, T1), true()) -> F()
     , eqt(cons(H1, T1), undefined()) -> F()
     , eqt(cons(H1, T1), pid(N2)) -> F()
     , eqt(cons(H1, T1), int(N2)) -> F()
     , eqt(cons(H1, T1), cons(H2, T2)) -> and(eqt(H1, H2), eqt(T1, T2))
     , eqt(cons(H1, T1), tuple(H2, T2)) -> F()
     , eqt(cons(H1, T1), tuplenil(H2)) -> F()
     , eqt(tuple(H1, T1), nil()) -> F()
     , eqt(tuple(H1, T1), a()) -> F()
     , eqt(tuple(H1, T1), excl()) -> F()
     , eqt(tuple(H1, T1), false()) -> F()
     , eqt(tuple(H1, T1), lock()) -> F()
     , eqt(tuple(H1, T1), locker()) -> F()
     , eqt(tuple(H1, T1), mcrlrecord()) -> F()
     , eqt(tuple(H1, T1), ok()) -> F()
     , eqt(tuple(H1, T1), pending()) -> F()
     , eqt(tuple(H1, T1), release()) -> F()
     , eqt(tuple(H1, T1), request()) -> F()
     , eqt(tuple(H1, T1), resource()) -> F()
     , eqt(tuple(H1, T1), tag()) -> F()
     , eqt(tuple(H1, T1), true()) -> F()
     , eqt(tuple(H1, T1), undefined()) -> F()
     , eqt(tuple(H1, T1), pid(N2)) -> F()
     , eqt(tuple(H1, T1), int(N2)) -> F()
     , eqt(tuple(H1, T1), cons(H2, T2)) -> F()
     , eqt(tuple(H1, T1), tuple(H2, T2)) ->
       and(eqt(H1, H2), eqt(T1, T2))
     , eqt(tuple(H1, T1), tuplenil(H2)) -> F()
     , eqt(tuplenil(H1), nil()) -> F()
     , eqt(tuplenil(H1), a()) -> F()
     , eqt(tuplenil(H1), excl()) -> F()
     , eqt(tuplenil(H1), false()) -> F()
     , eqt(tuplenil(H1), lock()) -> F()
     , eqt(tuplenil(H1), locker()) -> F()
     , eqt(tuplenil(H1), mcrlrecord()) -> F()
     , eqt(tuplenil(H1), ok()) -> F()
     , eqt(tuplenil(H1), pending()) -> F()
     , eqt(tuplenil(H1), release()) -> F()
     , eqt(tuplenil(H1), request()) -> F()
     , eqt(tuplenil(H1), resource()) -> F()
     , eqt(tuplenil(H1), tag()) -> F()
     , eqt(tuplenil(H1), true()) -> F()
     , eqt(tuplenil(H1), undefined()) -> F()
     , eqt(tuplenil(H1), pid(N2)) -> F()
     , eqt(tuplenil(H1), int(N2)) -> F()
     , eqt(tuplenil(H1), cons(H2, T2)) -> F()
     , eqt(tuplenil(H1), tuple(H2, T2)) -> F()
     , eqt(tuplenil(H1), tuplenil(H2)) -> eqt(H1, H2)
     , element(int(s(0())), tuplenil(T1)) -> T1
     , element(int(s(0())), tuple(T1, T2)) -> T1
     , element(int(s(s(N1))), tuple(T1, T2)) -> element(int(s(N1)), T2)
     , record_new(lock()) ->
       tuple(mcrlrecord(),
             tuple(lock(), tuple(undefined(), tuple(nil(), tuplenil(nil())))))
     , record_extract(tuple(mcrlrecord(),
                            tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))),
                      lock(),
                      resource())
       ->
       tuple(mcrlrecord(),
             tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2)))))
     , record_update(tuple(mcrlrecord(),
                           tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))),
                     lock(),
                     pending(),
                     NewF)
       ->
       tuple(mcrlrecord(),
             tuple(lock(), tuple(F0, tuple(F1, tuplenil(NewF)))))
     , record_updates(Record, Name, nil()) -> Record
     , record_updates(Record,
                      Name,
                      cons(tuple(Field, tuplenil(NewF)), Fields))
       ->
       record_updates(record_update(Record, Name, Field, NewF),
                      Name,
                      Fields)
     , locker2_map_promote_pending(nil(), Pending) -> nil()
     , locker2_map_promote_pending(cons(Lock, Locks), Pending) ->
       cons(locker2_promote_pending(Lock, Pending),
            locker2_map_promote_pending(Locks, Pending))
     , locker2_map_claim_lock(nil(), Resources, Client) -> nil()
     , locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) ->
       cons(locker2_claim_lock(Lock, Resources, Client),
            locker2_map_claim_lock(Locks, Resources, Client))
     , locker2_map_add_pending(nil(), Resources, Client) -> nil()
     , locker2_promote_pending(Lock, Client) ->
       case0(Client, Lock, record_extract(Lock, lock(), pending()))
     , case0(Client, Lock, cons(Client, Pendings)) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(excl(), tuplenil(Client)),
                           cons(tuple(pending(), tuplenil(Pendings)), nil())))
     , case0(Client, Lock, MCRLFree0) -> Lock
     , locker2_remove_pending(Lock, Client) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(pending(),
                                 tuplenil(subtract(record_extract(Lock, lock(), pending()),
                                                   cons(Client, nil())))),
                           nil()))
     , locker2_add_pending(Lock, Resources, Client) ->
       case1(Client,
             Resources,
             Lock,
             member(record_extract(Lock, lock(), resource()), Resources))
     , case1(Client, Resources, Lock, true()) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(pending(),
                                 tuplenil(append(record_extract(Lock, lock(), pending()),
                                                 cons(Client, nil())))),
                           nil()))
     , case1(Client, Resources, Lock, false()) -> Lock
     , locker2_release_lock(Lock, Client) ->
       case2(Client,
             Lock,
             gen_modtageq(Client, record_extract(Lock, lock(), excl())))
     , case2(Client, Lock, true()) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(excllock(), excl()), nil()))
     , case4(Client, Lock, MCRLFree1) -> false()
     , locker2_obtainables(nil(), Client) -> true()
     , locker2_obtainables(cons(Lock, Locks), Client) ->
       case5(Client,
             Locks,
             Lock,
             member(Client, record_extract(Lock, lock(), pending())))
     , case5(Client, Locks, Lock, true()) ->
       andt(locker2_obtainable(Lock, Client),
            locker2_obtainables(Locks, Client))
     , case5(Client, Locks, Lock, false()) ->
       locker2_obtainables(Locks, Client)
     , locker2_check_available(Resource, nil()) -> false()
     , locker2_check_available(Resource, cons(Lock, Locks)) ->
       case6(Locks,
             Lock,
             Resource,
             equal(Resource, record_extract(Lock, lock(), resource())))
     , case6(Locks, Lock, Resource, true()) ->
       andt(equal(record_extract(Lock, lock(), excl()), nil()),
            equal(record_extract(Lock, lock(), pending()), nil()))
     , case6(Locks, Lock, Resource, false()) ->
       locker2_check_available(Resource, Locks)
     , locker2_check_availables(nil(), Locks) -> true()
     , locker2_check_availables(cons(Resource, Resources), Locks) ->
       andt(locker2_check_available(Resource, Locks),
            locker2_check_availables(Resources, Locks))
     , locker2_adduniq(nil(), List) -> List
     , append(cons(Head, Tail), List) -> cons(Head, append(Tail, List))
     , subtract(List, nil()) -> List
     , subtract(List, cons(Head, Tail)) ->
       subtract(delete(Head, List), Tail)
     , delete(E, nil()) -> nil()
     , delete(E, cons(Head, Tail)) ->
       case8(Tail, Head, E, equal(E, Head))
     , case8(Tail, Head, E, true()) -> Tail
     , case8(Tail, Head, E, false()) -> cons(Head, delete(E, Tail))
     , gen_tag(Pid) -> tuple(Pid, tuplenil(tag()))
     , gen_modtageq(Client1, Client2) -> equal(Client1, Client2)
     , member(E, nil()) -> false()
     , member(E, cons(Head, Tail)) ->
       case9(Tail, Head, E, equal(E, Head))
     , case9(Tail, Head, E, true()) -> true()
     , case9(Tail, Head, E, false()) -> member(E, Tail)
     , eqs(empty(), empty()) -> T()
     , eqs(empty(), stack(E2, S2)) -> F()
     , eqs(stack(E1, S1), empty()) -> F()
     , eqs(stack(E1, S1), stack(E2, S2)) ->
       and(eqt(E1, E2), eqs(S1, S2))
     , pushs(E1, S1) -> stack(E1, S1)
     , pops(stack(E1, S1)) -> S1
     , tops(stack(E1, S1)) -> E1
     , istops(E1, empty()) -> F()
     , istops(E1, stack(E2, S1)) -> eqt(E1, E2)
     , eqc(nocalls(), nocalls()) -> T()
     , eqc(nocalls(), calls(E2, S2, CS2)) -> F()
     , eqc(calls(E1, S1, CS1), nocalls()) -> F()
     , eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) ->
       and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))
     , push(E1, E2, nocalls()) ->
       calls(E1, stack(E2, empty()), nocalls())
     , push(E1, E2, calls(E3, S1, CS1)) ->
       push1(E1, E2, E3, S1, CS1, eqt(E1, E3))
     , push1(E1, E2, E3, S1, CS1, T()) -> calls(E3, pushs(E2, S1), CS1)}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputCiME 04 mucrl1

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputCiME 04 mucrl1

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  or(T(), T()) -> T()
     , or(F(), T()) -> T()
     , or(T(), F()) -> T()
     , or(F(), F()) -> F()
     , and(T(), B) -> B
     , and(B, T()) -> B
     , and(F(), B) -> F()
     , and(B, F()) -> F()
     , imp(T(), B) -> B
     , imp(F(), B) -> T()
     , not(T()) -> F()
     , not(F()) -> T()
     , if(T(), B1, B2) -> B1
     , if(F(), B1, B2) -> B2
     , eq(T(), T()) -> T()
     , eq(F(), F()) -> T()
     , eq(T(), F()) -> F()
     , eq(F(), T()) -> F()
     , eqt(nil(), undefined()) -> F()
     , eqt(nil(), pid(N2)) -> F()
     , eqt(nil(), int(N2)) -> F()
     , eqt(nil(), cons(H2, T2)) -> F()
     , eqt(nil(), tuple(H2, T2)) -> F()
     , eqt(nil(), tuplenil(H2)) -> F()
     , eqt(a(), nil()) -> F()
     , eqt(a(), a()) -> T()
     , eqt(a(), excl()) -> F()
     , eqt(a(), false()) -> F()
     , eqt(a(), lock()) -> F()
     , eqt(a(), locker()) -> F()
     , eqt(a(), mcrlrecord()) -> F()
     , eqt(a(), ok()) -> F()
     , eqt(a(), pending()) -> F()
     , eqt(a(), release()) -> F()
     , eqt(a(), request()) -> F()
     , eqt(a(), resource()) -> F()
     , eqt(a(), tag()) -> F()
     , eqt(a(), true()) -> F()
     , eqt(a(), undefined()) -> F()
     , eqt(a(), pid(N2)) -> F()
     , eqt(a(), int(N2)) -> F()
     , eqt(a(), cons(H2, T2)) -> F()
     , eqt(a(), tuple(H2, T2)) -> F()
     , eqt(a(), tuplenil(H2)) -> F()
     , eqt(excl(), nil()) -> F()
     , eqt(excl(), a()) -> F()
     , eqt(excl(), excl()) -> T()
     , eqt(excl(), false()) -> F()
     , eqt(excl(), lock()) -> F()
     , eqt(excl(), locker()) -> F()
     , eqt(excl(), mcrlrecord()) -> F()
     , eqt(excl(), ok()) -> F()
     , eqt(excl(), pending()) -> F()
     , eqt(excl(), release()) -> F()
     , eqt(excl(), request()) -> F()
     , eqt(excl(), resource()) -> F()
     , eqt(excl(), tag()) -> F()
     , eqt(excl(), true()) -> F()
     , eqt(excl(), undefined()) -> F()
     , eqt(excl(), pid(N2)) -> F()
     , eqt(excl(), eqt(false(), int(N2))) -> F()
     , eqt(false(), cons(H2, T2)) -> F()
     , eqt(false(), tuple(H2, T2)) -> F()
     , eqt(false(), tuplenil(H2)) -> F()
     , eqt(lock(), nil()) -> F()
     , eqt(lock(), a()) -> F()
     , eqt(lock(), excl()) -> F()
     , eqt(lock(), false()) -> F()
     , eqt(lock(), lock()) -> T()
     , eqt(lock(), locker()) -> F()
     , eqt(lock(), mcrlrecord()) -> F()
     , eqt(lock(), ok()) -> F()
     , eqt(lock(), pending()) -> F()
     , eqt(lock(), release()) -> F()
     , eqt(lock(), request()) -> F()
     , eqt(lock(), resource()) -> F()
     , eqt(lock(), tag()) -> F()
     , eqt(lock(), true()) -> F()
     , eqt(lock(), undefined()) -> F()
     , eqt(lock(), pid(N2)) -> F()
     , eqt(lock(), int(N2)) -> F()
     , eqt(lock(), cons(H2, T2)) -> F()
     , eqt(lock(), tuple(H2, T2)) -> F()
     , eqt(lock(), tuplenil(H2)) -> F()
     , eqt(locker(), nil()) -> F()
     , eqt(locker(), a()) -> F()
     , eqt(locker(), excl()) -> F()
     , eqt(locker(), false()) -> F()
     , eqt(locker(), lock()) -> F()
     , eqt(locker(), locker()) -> T()
     , eqt(locker(), mcrlrecord()) -> F()
     , eqt(locker(), ok()) -> F()
     , eqt(locker(), pending()) -> F()
     , eqt(locker(), release()) -> F()
     , eqt(locker(), request()) -> F()
     , eqt(locker(), resource()) -> F()
     , eqt(locker(), tag()) -> F()
     , eqt(locker(), true()) -> F()
     , eqt(locker(), undefined()) -> F()
     , eqt(locker(), pid(N2)) -> F()
     , eqt(locker(), int(N2)) -> F()
     , eqt(locker(), cons(H2, T2)) -> F()
     , eqt(locker(), tuple(H2, T2)) -> F()
     , eqt(locker(), tuplenil(H2)) -> F()
     , eqt(mcrlrecord(), nil()) -> F()
     , eqt(mcrlrecord(), a()) -> F()
     , eqt(mcrlrecord(), excl()) -> F()
     , eqt(mcrlrecord(), false()) -> F()
     , eqt(mcrlrecord(), lock()) -> F()
     , eqt(mcrlrecord(), locker()) -> F()
     , eqt(mcrlrecord(), mcrlrecord()) -> T()
     , eqt(mcrlrecord(), ok()) -> F()
     , eqt(mcrlrecord(), pending()) -> F()
     , eqt(mcrlrecord(), release()) -> F()
     , eqt(mcrlrecord(), request()) -> F()
     , eqt(mcrlrecord(), resource()) -> F()
     , eqt(ok(), resource()) -> F()
     , eqt(ok(), tag()) -> F()
     , eqt(ok(), true()) -> F()
     , eqt(ok(), undefined()) -> F()
     , eqt(ok(), pid(N2)) -> F()
     , eqt(ok(), int(N2)) -> F()
     , eqt(ok(), cons(H2, T2)) -> F()
     , eqt(ok(), tuple(H2, T2)) -> F()
     , eqt(ok(), tuplenil(H2)) -> F()
     , eqt(pending(), nil()) -> F()
     , eqt(pending(), a()) -> F()
     , eqt(pending(), excl()) -> F()
     , eqt(pending(), false()) -> F()
     , eqt(pending(), lock()) -> F()
     , eqt(pending(), locker()) -> F()
     , eqt(pending(), mcrlrecord()) -> F()
     , eqt(pending(), ok()) -> F()
     , eqt(pending(), pending()) -> T()
     , eqt(pending(), release()) -> F()
     , eqt(pending(), request()) -> F()
     , eqt(pending(), resource()) -> F()
     , eqt(pending(), tag()) -> F()
     , eqt(pending(), true()) -> F()
     , eqt(pending(), undefined()) -> F()
     , eqt(pending(), pid(N2)) -> F()
     , eqt(pending(), int(N2)) -> F()
     , eqt(pending(), cons(H2, T2)) -> F()
     , eqt(pending(), tuple(H2, T2)) -> F()
     , eqt(pending(), tuplenil(H2)) -> F()
     , eqt(release(), nil()) -> F()
     , eqt(release(), a()) -> F()
     , eqt(release(), excl()) -> F()
     , eqt(release(), false()) -> F()
     , eqt(release(), lock()) -> F()
     , eqt(release(), locker()) -> F()
     , eqt(release(), mcrlrecord()) -> F()
     , eqt(release(), ok()) -> F()
     , eqt(request(), mcrlrecord()) -> F()
     , eqt(request(), ok()) -> F()
     , eqt(request(), pending()) -> F()
     , eqt(request(), release()) -> F()
     , eqt(request(), request()) -> T()
     , eqt(request(), resource()) -> F()
     , eqt(request(), tag()) -> F()
     , eqt(request(), true()) -> F()
     , eqt(request(), undefined()) -> F()
     , eqt(request(), pid(N2)) -> F()
     , eqt(request(), int(N2)) -> F()
     , eqt(request(), cons(H2, T2)) -> F()
     , eqt(request(), tuple(H2, T2)) -> F()
     , eqt(request(), tuplenil(H2)) -> F()
     , eqt(resource(), nil()) -> F()
     , eqt(resource(), a()) -> F()
     , eqt(resource(), excl()) -> F()
     , eqt(resource(), false()) -> F()
     , eqt(resource(), lock()) -> F()
     , eqt(resource(), locker()) -> F()
     , eqt(resource(), mcrlrecord()) -> F()
     , eqt(resource(), ok()) -> F()
     , eqt(resource(), pending()) -> F()
     , eqt(resource(), release()) -> F()
     , eqt(resource(), request()) -> F()
     , eqt(resource(), resource()) -> T()
     , eqt(resource(), tag()) -> F()
     , eqt(resource(), true()) -> F()
     , eqt(resource(), undefined()) -> F()
     , eqt(resource(), pid(N2)) -> F()
     , eqt(resource(), int(N2)) -> F()
     , eqt(resource(), cons(H2, T2)) -> F()
     , eqt(resource(), tuple(H2, T2)) -> F()
     , eqt(resource(), tuplenil(H2)) -> F()
     , eqt(tag(), nil()) -> F()
     , eqt(tag(), a()) -> F()
     , eqt(tag(), excl()) -> F()
     , eqt(tag(), false()) -> F()
     , eqt(tag(), lock()) -> F()
     , eqt(tag(), locker()) -> F()
     , eqt(tag(), mcrlrecord()) -> F()
     , eqt(tag(), ok()) -> F()
     , eqt(tag(), pending()) -> F()
     , eqt(tag(), release()) -> F()
     , eqt(tag(), request()) -> F()
     , eqt(tag(), resource()) -> F()
     , eqt(tag(), tag()) -> T()
     , eqt(tag(), true()) -> F()
     , eqt(tag(), undefined()) -> F()
     , eqt(tag(), pid(N2)) -> F()
     , eqt(tag(), int(N2)) -> F()
     , eqt(tag(), cons(H2, T2)) -> F()
     , eqt(tag(), tuple(H2, T2)) -> F()
     , eqt(tag(), tuplenil(H2)) -> F()
     , eqt(true(), nil()) -> F()
     , eqt(true(), a()) -> F()
     , eqt(true(), excl()) -> F()
     , eqt(true(), false()) -> F()
     , eqt(true(), lock()) -> F()
     , eqt(true(), locker()) -> F()
     , eqt(true(), mcrlrecord()) -> F()
     , eqt(true(), ok()) -> F()
     , eqt(true(), pending()) -> F()
     , eqt(true(), release()) -> F()
     , eqt(true(), request()) -> F()
     , eqt(true(), resource()) -> F()
     , eqt(true(), tag()) -> F()
     , eqt(true(), true()) -> T()
     , eqt(true(), undefined()) -> F()
     , eqt(true(), pid(N2)) -> F()
     , eqt(true(), int(N2)) -> F()
     , eqt(true(), cons(H2, T2)) -> F()
     , eqt(true(), tuple(H2, T2)) -> F()
     , eqt(true(), tuplenil(H2)) -> F()
     , eqt(undefined(), nil()) -> F()
     , eqt(undefined(), a()) -> F()
     , eqt(undefined(), tuplenil(H2)) -> F()
     , eqt(pid(N1), nil()) -> F()
     , eqt(pid(N1), a()) -> F()
     , eqt(pid(N1), excl()) -> F()
     , eqt(pid(N1), false()) -> F()
     , eqt(pid(N1), lock()) -> F()
     , eqt(pid(N1), locker()) -> F()
     , eqt(pid(N1), mcrlrecord()) -> F()
     , eqt(pid(N1), ok()) -> F()
     , eqt(pid(N1), pending()) -> F()
     , eqt(pid(N1), release()) -> F()
     , eqt(pid(N1), request()) -> F()
     , eqt(pid(N1), resource()) -> F()
     , eqt(pid(N1), tag()) -> F()
     , eqt(pid(N1), true()) -> F()
     , eqt(pid(N1), undefined()) -> F()
     , eqt(pid(N1), pid(N2)) -> eqt(N1, N2)
     , eqt(pid(N1), int(N2)) -> F()
     , eqt(pid(N1), cons(H2, T2)) -> F()
     , eqt(pid(N1), tuple(H2, T2)) -> F()
     , eqt(pid(N1), tuplenil(H2)) -> F()
     , eqt(int(N1), nil()) -> F()
     , eqt(int(N1), a()) -> F()
     , eqt(int(N1), excl()) -> F()
     , eqt(int(N1), false()) -> F()
     , eqt(int(N1), lock()) -> F()
     , eqt(int(N1), locker()) -> F()
     , eqt(int(N1), mcrlrecord()) -> F()
     , eqt(int(N1), ok()) -> F()
     , eqt(int(N1), pending()) -> F()
     , eqt(int(N1), release()) -> F()
     , eqt(int(N1), request()) -> F()
     , eqt(int(N1), resource()) -> F()
     , eqt(int(N1), tag()) -> F()
     , eqt(int(N1), true()) -> F()
     , eqt(int(N1), undefined()) -> F()
     , eqt(cons(H1, T1), resource()) -> F()
     , eqt(cons(H1, T1), tag()) -> F()
     , eqt(cons(H1, T1), true()) -> F()
     , eqt(cons(H1, T1), undefined()) -> F()
     , eqt(cons(H1, T1), pid(N2)) -> F()
     , eqt(cons(H1, T1), int(N2)) -> F()
     , eqt(cons(H1, T1), cons(H2, T2)) -> and(eqt(H1, H2), eqt(T1, T2))
     , eqt(cons(H1, T1), tuple(H2, T2)) -> F()
     , eqt(cons(H1, T1), tuplenil(H2)) -> F()
     , eqt(tuple(H1, T1), nil()) -> F()
     , eqt(tuple(H1, T1), a()) -> F()
     , eqt(tuple(H1, T1), excl()) -> F()
     , eqt(tuple(H1, T1), false()) -> F()
     , eqt(tuple(H1, T1), lock()) -> F()
     , eqt(tuple(H1, T1), locker()) -> F()
     , eqt(tuple(H1, T1), mcrlrecord()) -> F()
     , eqt(tuple(H1, T1), ok()) -> F()
     , eqt(tuple(H1, T1), pending()) -> F()
     , eqt(tuple(H1, T1), release()) -> F()
     , eqt(tuple(H1, T1), request()) -> F()
     , eqt(tuple(H1, T1), resource()) -> F()
     , eqt(tuple(H1, T1), tag()) -> F()
     , eqt(tuple(H1, T1), true()) -> F()
     , eqt(tuple(H1, T1), undefined()) -> F()
     , eqt(tuple(H1, T1), pid(N2)) -> F()
     , eqt(tuple(H1, T1), int(N2)) -> F()
     , eqt(tuple(H1, T1), cons(H2, T2)) -> F()
     , eqt(tuple(H1, T1), tuple(H2, T2)) ->
       and(eqt(H1, H2), eqt(T1, T2))
     , eqt(tuple(H1, T1), tuplenil(H2)) -> F()
     , eqt(tuplenil(H1), nil()) -> F()
     , eqt(tuplenil(H1), a()) -> F()
     , eqt(tuplenil(H1), excl()) -> F()
     , eqt(tuplenil(H1), false()) -> F()
     , eqt(tuplenil(H1), lock()) -> F()
     , eqt(tuplenil(H1), locker()) -> F()
     , eqt(tuplenil(H1), mcrlrecord()) -> F()
     , eqt(tuplenil(H1), ok()) -> F()
     , eqt(tuplenil(H1), pending()) -> F()
     , eqt(tuplenil(H1), release()) -> F()
     , eqt(tuplenil(H1), request()) -> F()
     , eqt(tuplenil(H1), resource()) -> F()
     , eqt(tuplenil(H1), tag()) -> F()
     , eqt(tuplenil(H1), true()) -> F()
     , eqt(tuplenil(H1), undefined()) -> F()
     , eqt(tuplenil(H1), pid(N2)) -> F()
     , eqt(tuplenil(H1), int(N2)) -> F()
     , eqt(tuplenil(H1), cons(H2, T2)) -> F()
     , eqt(tuplenil(H1), tuple(H2, T2)) -> F()
     , eqt(tuplenil(H1), tuplenil(H2)) -> eqt(H1, H2)
     , element(int(s(0())), tuplenil(T1)) -> T1
     , element(int(s(0())), tuple(T1, T2)) -> T1
     , element(int(s(s(N1))), tuple(T1, T2)) -> element(int(s(N1)), T2)
     , record_new(lock()) ->
       tuple(mcrlrecord(),
             tuple(lock(), tuple(undefined(), tuple(nil(), tuplenil(nil())))))
     , record_extract(tuple(mcrlrecord(),
                            tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))),
                      lock(),
                      resource())
       ->
       tuple(mcrlrecord(),
             tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2)))))
     , record_update(tuple(mcrlrecord(),
                           tuple(lock(), tuple(F0, tuple(F1, tuplenil(F2))))),
                     lock(),
                     pending(),
                     NewF)
       ->
       tuple(mcrlrecord(),
             tuple(lock(), tuple(F0, tuple(F1, tuplenil(NewF)))))
     , record_updates(Record, Name, nil()) -> Record
     , record_updates(Record,
                      Name,
                      cons(tuple(Field, tuplenil(NewF)), Fields))
       ->
       record_updates(record_update(Record, Name, Field, NewF),
                      Name,
                      Fields)
     , locker2_map_promote_pending(nil(), Pending) -> nil()
     , locker2_map_promote_pending(cons(Lock, Locks), Pending) ->
       cons(locker2_promote_pending(Lock, Pending),
            locker2_map_promote_pending(Locks, Pending))
     , locker2_map_claim_lock(nil(), Resources, Client) -> nil()
     , locker2_map_claim_lock(cons(Lock, Locks), Resources, Client) ->
       cons(locker2_claim_lock(Lock, Resources, Client),
            locker2_map_claim_lock(Locks, Resources, Client))
     , locker2_map_add_pending(nil(), Resources, Client) -> nil()
     , locker2_promote_pending(Lock, Client) ->
       case0(Client, Lock, record_extract(Lock, lock(), pending()))
     , case0(Client, Lock, cons(Client, Pendings)) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(excl(), tuplenil(Client)),
                           cons(tuple(pending(), tuplenil(Pendings)), nil())))
     , case0(Client, Lock, MCRLFree0) -> Lock
     , locker2_remove_pending(Lock, Client) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(pending(),
                                 tuplenil(subtract(record_extract(Lock, lock(), pending()),
                                                   cons(Client, nil())))),
                           nil()))
     , locker2_add_pending(Lock, Resources, Client) ->
       case1(Client,
             Resources,
             Lock,
             member(record_extract(Lock, lock(), resource()), Resources))
     , case1(Client, Resources, Lock, true()) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(pending(),
                                 tuplenil(append(record_extract(Lock, lock(), pending()),
                                                 cons(Client, nil())))),
                           nil()))
     , case1(Client, Resources, Lock, false()) -> Lock
     , locker2_release_lock(Lock, Client) ->
       case2(Client,
             Lock,
             gen_modtageq(Client, record_extract(Lock, lock(), excl())))
     , case2(Client, Lock, true()) ->
       record_updates(Lock,
                      lock(),
                      cons(tuple(excllock(), excl()), nil()))
     , case4(Client, Lock, MCRLFree1) -> false()
     , locker2_obtainables(nil(), Client) -> true()
     , locker2_obtainables(cons(Lock, Locks), Client) ->
       case5(Client,
             Locks,
             Lock,
             member(Client, record_extract(Lock, lock(), pending())))
     , case5(Client, Locks, Lock, true()) ->
       andt(locker2_obtainable(Lock, Client),
            locker2_obtainables(Locks, Client))
     , case5(Client, Locks, Lock, false()) ->
       locker2_obtainables(Locks, Client)
     , locker2_check_available(Resource, nil()) -> false()
     , locker2_check_available(Resource, cons(Lock, Locks)) ->
       case6(Locks,
             Lock,
             Resource,
             equal(Resource, record_extract(Lock, lock(), resource())))
     , case6(Locks, Lock, Resource, true()) ->
       andt(equal(record_extract(Lock, lock(), excl()), nil()),
            equal(record_extract(Lock, lock(), pending()), nil()))
     , case6(Locks, Lock, Resource, false()) ->
       locker2_check_available(Resource, Locks)
     , locker2_check_availables(nil(), Locks) -> true()
     , locker2_check_availables(cons(Resource, Resources), Locks) ->
       andt(locker2_check_available(Resource, Locks),
            locker2_check_availables(Resources, Locks))
     , locker2_adduniq(nil(), List) -> List
     , append(cons(Head, Tail), List) -> cons(Head, append(Tail, List))
     , subtract(List, nil()) -> List
     , subtract(List, cons(Head, Tail)) ->
       subtract(delete(Head, List), Tail)
     , delete(E, nil()) -> nil()
     , delete(E, cons(Head, Tail)) ->
       case8(Tail, Head, E, equal(E, Head))
     , case8(Tail, Head, E, true()) -> Tail
     , case8(Tail, Head, E, false()) -> cons(Head, delete(E, Tail))
     , gen_tag(Pid) -> tuple(Pid, tuplenil(tag()))
     , gen_modtageq(Client1, Client2) -> equal(Client1, Client2)
     , member(E, nil()) -> false()
     , member(E, cons(Head, Tail)) ->
       case9(Tail, Head, E, equal(E, Head))
     , case9(Tail, Head, E, true()) -> true()
     , case9(Tail, Head, E, false()) -> member(E, Tail)
     , eqs(empty(), empty()) -> T()
     , eqs(empty(), stack(E2, S2)) -> F()
     , eqs(stack(E1, S1), empty()) -> F()
     , eqs(stack(E1, S1), stack(E2, S2)) ->
       and(eqt(E1, E2), eqs(S1, S2))
     , pushs(E1, S1) -> stack(E1, S1)
     , pops(stack(E1, S1)) -> S1
     , tops(stack(E1, S1)) -> E1
     , istops(E1, empty()) -> F()
     , istops(E1, stack(E2, S1)) -> eqt(E1, E2)
     , eqc(nocalls(), nocalls()) -> T()
     , eqc(nocalls(), calls(E2, S2, CS2)) -> F()
     , eqc(calls(E1, S1, CS1), nocalls()) -> F()
     , eqc(calls(E1, S1, CS1), calls(E2, S2, CS2)) ->
       and(eqt(E1, E2), and(eqs(S1, S2), eqc(CS1, CS2)))
     , push(E1, E2, nocalls()) ->
       calls(E1, stack(E2, empty()), nocalls())
     , push(E1, E2, calls(E3, S1, CS1)) ->
       push1(E1, E2, E3, S1, CS1, eqt(E1, E3))
     , push1(E1, E2, E3, S1, CS1, T()) -> calls(E3, pushs(E2, S1), CS1)}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds