YES

TRS:

  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)

max/plus interpretations on N:

  or_A(x1,x2) = max{2, -1, -1}
  or#_A(x1,x2) = max{0, 241, 241}
  T_A = 2
  T#_A = 243
  F_A = 0
  F#_A = 242
  and_A(x1,x2) = max{15, x1, x2}
  and#_A(x1,x2) = max{238, 243 + x1, 241}
  imp_A(x1,x2) = max{0, 1, 2 + x2}
  imp#_A(x1,x2) = max{244, 244, 244}
  not_A(x1) = max{2, -1}
  not#_A(x1) = max{244, 241}
  if_A(x1,x2,x3) = max{0, x1, x2, x3}
  if#_A(x1,x2,x3) = max{0, x1, x2, x3}
  eq_A(x1,x2) = max{2, -1, -1}
  eq#_A(x1,x2) = max{0, 244, 244}
  eqt_A(x1,x2) = max{15, -18, -60}
  eqt#_A(x1,x2) = max{259, 244, 239}
  nil_A = 74
  nil#_A = 321
  undefined_A = 78
  undefined#_A = 126
  pid_A(x1) = max{1, 1 + x1}
  pid#_A(x1) = max{243, 0}
  int_A(x1) = max{0, 61}
  int#_A(x1) = max{243, 244}
  cons_A(x1,x2) = max{0, 31 + x1, 351 + x2}
  cons#_A(x1,x2) = max{130, 239, 136}
  tuple_A(x1,x2) = max{393, 385 + x1, 4 + x2}
  tuple#_A(x1,x2) = max{128, 241, 139}
  tuplenil_A(x1) = max{390, -1 + x1}
  tuplenil#_A(x1) = max{137, 243}
  a_A = 0
  a#_A = 244
  excl_A = 196
  excl#_A = 324
  false_A = 107
  false#_A = 243
  lock_A = 82
  lock#_A = 311
  locker_A = 1
  locker#_A = 244
  mcrlrecord_A = 1
  mcrlrecord#_A = 126
  ok_A = 1
  ok#_A = 243
  pending_A = 1
  pending#_A = 137
  release_A = 1
  release#_A = 243
  request_A = 1
  request#_A = 244
  resource_A = 5
  resource#_A = 231
  tag_A = 392
  tag#_A = 244
  true_A = 102
  true#_A = 310
  element_A(x1,x2) = max{6, 6, 1 + x2}
  element#_A(x1,x2) = max{250, 249, 246 + x2}
  s_A(x1) = max{1, -2 + x1}
  s#_A(x1) = max{248, 247 + x1}
  0_A = 0
  0#_A = 0
  record_new_A(x1) = max{471, 405}
  record_new#_A(x1) = max{322, 127}
  record_extract_A(x1,x2,x3) = max{0, 65 + x1, 67, -4 + x3}
  record_extract#_A(x1,x2,x3) = max{319, 140, 234, 130 + x3}
  record_update_A(x1,x2,x3,x4) = max{747, x1, 426, 747, 15 + x4}
  record_update#_A(x1,x2,x3,x4) = max{244, 244, 312, 312, 244}
  record_updates_A(x1,x2,x3) = max{749, 2 + x1, 698 + x2, 3 + x3}
  record_updates#_A(x1,x2,x3) = max{246, 247, 245, -103 + x3}
  locker2_map_promote_pending_A(x1,x2) = max{496, 815 + x1, 464}
  locker2_map_promote_pending#_A(x1,x2) = max{346, 675 + x1, 1026}
  locker2_promote_pending_A(x1,x2) = max{466, 815 + x1, 1}
  locker2_promote_pending#_A(x1,x2) = max{347, 674 + x1, 349}
  locker2_map_claim_lock_A(x1,x2,x3) = max{425, 745 + x1, 74, -277}
  locker2_map_claim_lock#_A(x1,x2,x3) = max{241, 241, 241, 240}
  locker2_claim_lock_A(x1,x2,x3) = max{746, -308, 394, 1065}
  locker2_claim_lock#_A(x1,x2,x3) = max{239, 0, 239, 239}
  locker2_map_add_pending_A(x1,x2,x3) = max{74, 73, 73, 73}
  locker2_map_add_pending#_A(x1,x2,x3) = max{0, 0, 322, 322}
  case0_A(x1,x2,x3) = max{467, 2, 2 + x2, 748 + x3}
  case0#_A(x1,x2,x3) = max{674, 310, 240, 281 + x3}
  locker2_remove_pending_A(x1,x2) = max{2, 420 + x1, 780 + x2}
  locker2_remove_pending#_A(x1,x2) = max{424, -2 + x1, 138 + x2}
  subtract_A(x1,x2) = max{493, 2 + x1, -2}
  subtract#_A(x1,x2) = max{0, 1, -1 + x2}
  locker2_add_pending_A(x1,x2,x3) = max{354, 780 + x1, 354 + x2, 1}
  locker2_add_pending#_A(x1,x2,x3) = max{585, 321 + x1, 323, 587}
  case1_A(x1,x2,x3,x4) = max{2, 39, 2, 780 + x3, 355}
  case1#_A(x1,x2,x3,x4) = max{322, 315, 317, 320 + x3, 313}
  member_A(x1,x2) = max{32, 384, -1 + x2}
  member#_A(x1,x2) = max{586, 224, 226}
  append_A(x1,x2) = max{319, 322 + x1, 2}
  append#_A(x1,x2) = max{312, 322, 316}
  locker2_release_lock_A(x1,x2) = max{1, 941 + x1, 1 + x2}
  locker2_release_lock#_A(x1,x2) = max{318, 327, 325}
  case2_A(x1,x2,x3) = max{780, 2, 2 + x2, 647 + x3}
  case2#_A(x1,x2,x3) = max{326, 323, 240, 129}
  gen_modtageq_A(x1,x2) = max{1, 1, 102 + x2}
  gen_modtageq#_A(x1,x2) = max{317, 317, 327}
  excllock_A = 1
  excllock#_A = 0
  case4_A(x1,x2,x3) = max{107, 106, 106, 106}
  case4#_A(x1,x2,x3) = max{0, 244, 244, 244}
  locker2_obtainables_A(x1,x2) = max{73, 73, 104}
  locker2_obtainables#_A(x1,x2) = max{303, 235 + x1, 310}
  case5_A(x1,x2,x3,x4) = max{104, 72, 104, 22, 29}
  case5#_A(x1,x2,x3,x4) = max{302, 586, 333 + x2, 309, 202 + x4}
  andt_A(x1,x2) = max{104, 23, 30}
  andt#_A(x1,x2) = max{253, 226 + x1, 228 + x2}
  locker2_obtainable_A(x1,x2) = max{108, -1, 78}
  locker2_obtainable#_A(x1,x2) = max{308, 301, 301}
  locker2_check_available_A(x1,x2) = max{29, 107, -1 + x2}
  locker2_check_available#_A(x1,x2) = max{232, 331, 228}
  case6_A(x1,x2,x3,x4) = max{22, 22 + x1, 22, 108, 30}
  case6#_A(x1,x2,x3,x4) = max{233, 229, 330, 231, 225 + x4}
  equal_A(x1,x2) = max{102, 2, 2}
  equal#_A(x1,x2) = max{227, 137, 137}
  locker2_check_availables_A(x1,x2) = max{104, 23, 1}
  locker2_check_availables#_A(x1,x2) = max{333, 254, 252 + x2}
  locker2_adduniq_A(x1,x2) = max{0, x1, x2}
  locker2_adduniq#_A(x1,x2) = max{0, x1, x2}
  delete_A(x1,x2) = max{0, -3, x2}
  delete#_A(x1,x2) = max{228, 138, 238}
  case8_A(x1,x2,x3,x4) = max{32, 351 + x1, 31 + x2, 347, 348}
  case8#_A(x1,x2,x3,x4) = max{238, 238, 137, 228, 136 + x4}
  gen_tag_A(x1) = max{395, 394 + x1}
  gen_tag#_A(x1) = max{245, 245}
  case9_A(x1,x2,x3,x4) = max{384, -1 + x1, -2, -2, -2}
  case9#_A(x1,x2,x3,x4) = max{225, 223, 586, 223, 484 + x4}
  eqs_A(x1,x2) = max{17, -63 + x1, 1}
  eqs#_A(x1,x2) = max{245, 223 + x1, -1}
  empty_A = 62
  empty#_A = 258
  stack_A(x1,x2) = max{45, -41 + x1, 3 + x2}
  stack#_A(x1,x2) = max{258, 235, 258}
  pushs_A(x1,x2) = max{64, 2 + x1, 3 + x2}
  pushs#_A(x1,x2) = max{236, 258, 258}
  pops_A(x1) = max{0, -3 + x1}
  pops#_A(x1) = max{0, x1}
  tops_A(x1) = max{0, 41 + x1}
  tops#_A(x1) = max{0, x1}
  istops_A(x1,x2) = max{15, -61 + x1, -106 + x2}
  istops#_A(x1,x2) = max{260, 260, 260}
  eqc_A(x1,x2) = max{38, 12 + x1, 6 + x2}
  eqc#_A(x1,x2) = max{0, 235 + x1, 240}
  nocalls_A = 28
  nocalls#_A = 259
  calls_A(x1,x2,x3) = max{2, -7 + x1, -11 + x2, 25 + x3}
  calls#_A(x1,x2,x3) = max{258, 234, 235, 234}
  push_A(x1,x2,x3) = max{0, -1 + x1, 53 + x2, 26 + x3}
  push#_A(x1,x2,x3) = max{257, 243, 257, 234 + x3}
  push1_A(x1,x2,x3,x4,x5,x6) = max{53, 0, -9 + x2, 1 + x3, -8 + x4, 29 + x5, 52}
  push1#_A(x1,x2,x3,x4,x5,x6) = max{235, 258, 235, 235, 235, 235, 235}

precedence:

  locker2_add_pending > locker2_remove_pending = case1 > record_updates = push > record_new = record_update = locker2_map_promote_pending = subtract = gen_tag = push1 > imp = if = tuplenil = 0 = locker2_promote_pending = locker2_map_add_pending = append = locker2_check_availables = locker2_adduniq = delete = pushs = pops = tops = nocalls = calls > case0 = case8 = stack > nil = locker2_release_lock > locker2_map_claim_lock = case2 = gen_modtageq = locker2_check_available > cons = mcrlrecord = locker2_claim_lock = case6 > record_extract = equal > tuple = lock > undefined = locker2_obtainables = istops = eqc > eqt = member = case5 > case4 = andt = locker2_obtainable = case9 = eqs > and = not = eq = pid = excl = false = locker = ok = release = request = resource = tag = true > F = excllock > int = a = empty > T = element > or = pending = s