workset(( RiskCA(cA, 3) RiskCB(cB, 2)) c workset((RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6))) *********** trial #682 ceq pAAr(rA, cA, P1) c pAAc(rA, cA, P2) c ineqAA(rA, cA, P3) = (pAAc(rA, cA, P2) c ineqAA(rA, cA, P1 - P2)) c pAAr(rA, cA, P1) if P3 =/= P1 - P2 = true [label getIneqAAc] . P1 --> 2 P2 --> 5 P3 --> -3 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 2 - 5 ---> -3 *********** equation (built-in equation for symbol _=/=_) -3 =/= -3 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #682 *********** trial #683 ceq pABr(rA, cB, P1) c pABc(rA, cB, P2) c ineqAB(rA, cB, P3) = (pABc(rA, cB, P2) c ineqAB(rA, cB, P1 - P2)) c pABr(rA, cB, P1) if P3 =/= P1 - P2 = true [label getIneqABc] . P1 --> 4 P2 --> 2 P3 --> 2 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 4 - 2 ---> 2 *********** equation (built-in equation for symbol _=/=_) 2 =/= 2 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #683 *********** trial #684 ceq pBAr(rB, cA, P1) c pBAc(rB, cA, P2) c ineqBA(rB, cA, P3) = (pBAc(rB, cA, P2) c ineqBA(rB, cA, P1 - P2)) c pBAr(rB, cA, P1) if P3 =/= P1 - P2 = true [label getIneqBAc] . P1 --> 4 P2 --> 2 P3 --> 2 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 4 - 2 ---> 2 *********** equation (built-in equation for symbol _=/=_) 2 =/= 2 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #684 *********** trial #685 ceq pBBr(rB, cB, P1) c pBBc(rB, cB, P2) c ineqBB(rB, cB, P3) = (pBBc(rB, cB, P2) c ineqBB(rB, cB, P1 - P2)) c pBBr(rB, cB, P1) if P3 =/= P1 - P2 = true [label getIneqAAc] . P1 --> 2 P2 --> 4 P3 --> -2 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 2 - 4 ---> -2 *********** equation (built-in equation for symbol _=/=_) -2 =/= -2 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #685 *********** trial #686 ceq totIneqcA(cA, P) c ineqAA(rA, cA, P1) c ineqBA(rB, cA, P2) = (totIneqcA(cA, P1 + P2) c ineqBA(rB, cA, P2)) c ineqAA(rA, cA, P1) if P =/= P1 + P2 = true [label gettotIneqcA] . P --> -1 P1 --> -3 P2 --> 2 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + -3 ---> -1 *********** equation (built-in equation for symbol _=/=_) -1 =/= -1 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #686 *********** trial #687 ceq totIneqcB(cB, P) c ineqAB(rA, cB, P2) c ineqBB(rB, cB, P1) = (totIneqcB(cB, P1 + P2) c ineqAB(rA, cB, P2)) c ineqBB(rB, cB, P1) if P =/= P1 + P2 = true [label gettotIneqcB] . P --> 0 P2 --> 2 P1 --> -2 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + -2 ---> 0 *********** equation (built-in equation for symbol _=/=_) 0 =/= 0 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #687 *********** trial #688 ceq totPaycA(cA, P) c pAAc(rA, cA, P1) c pBAc(rB, cA, P2) = (totPaycA(cA, P1 + P2) c pBAc(rB, cA, P2)) c pAAc(rA, cA, P1) if P =/= P1 + P2 = true [label gettotPaycA] . P --> 7 P1 --> 5 P2 --> 2 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + 5 ---> 7 *********** equation (built-in equation for symbol _=/=_) 7 =/= 7 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #688 *********** trial #689 ceq totPaycB(cB, P) c pABc(rA, cB, P1) c pBBc(rB, cB, P2) = (totPaycB(cB, P1 + P2) c pBBc(rB, cB, P2)) c pABc(rA, cB, P1) if P =/= P1 + P2 = true [label gettotPaycB] . P --> 6 P1 --> 2 P2 --> 4 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + 4 ---> 6 *********** equation (built-in equation for symbol _=/=_) 6 =/= 6 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #689 *********** trial #690 ceq RiskCA(cA, P) c pAAc(rA, cA, P1) c pBAc(rB, cA, P2) = (RiskCA(cA, abs(P1 - P2)) c pBAc(rB, cA, P2)) c pAAc(rA, cA, P1) if P =/= abs(P1 - P2) = true [ label getRiskcA] . P --> 3 P1 --> 5 P2 --> 2 *********** solving condition fragment P =/= abs(P1 - P2) = true *********** equation (built-in equation for symbol _-_) 5 - 2 ---> 3 *********** equation (built-in equation for symbol abs) abs(3) ---> 3 *********** equation (built-in equation for symbol _=/=_) 3 =/= 3 ---> false *********** failure for condition fragment P =/= abs(P1 - P2) = true *********** failure #690 *********** trial #691 ceq RiskCB(cB, P) c pABc(rA, cB, P2) c pBBc(rB, cB, P1) = (RiskCB(cB, abs(P1 - P2)) c pABc(rA, cB, P2)) c pBBc(rB, cB, P1) if P =/= abs(P1 - P2) = true [ label getRiskcB] . P --> 2 P2 --> 2 P1 --> 4 *********** solving condition fragment P =/= abs(P1 - P2) = true *********** equation (built-in equation for symbol _-_) 4 - 2 ---> 2 *********** equation (built-in equation for symbol abs) abs(2) ---> 2 *********** equation (built-in equation for symbol _=/=_) 2 =/= 2 ---> false *********** failure for condition fragment P =/= abs(P1 - P2) = true *********** failure #691 *********** trial #692 ceq dec c worklist(L) c workset(S) = dec c worklist(L) c workset(makeSet(L)) if S =/= makeSet(L) = true [label listtoset] . L --> totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) S --> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) *********** solving condition fragment S =/= makeSet(L) = true *********** equation eq makeSet(L) = $makeSet(L, empty) . L --> totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) makeSet(totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2)) ---> $makeSet(totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), empty) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> totPaycA(cA, 7) L --> totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) S --> empty $makeSet(totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), empty) ---> $makeSet(totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), (empty, totPaycA(cA, 7))) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> totPaycB(cB, 6) L --> RiskCA(cA, 3) RiskCB(cB, 2) S --> totPaycA(cA, 7) $makeSet(totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), totPaycA(cA, 7)) ---> $makeSet(RiskCA(cA, 3) RiskCB(cB, 2), (totPaycA(cA, 7), totPaycB(cB, 6))) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> RiskCA(cA, 3) L --> RiskCB(cB, 2) S --> totPaycA(cA, 7), totPaycB(cB, 6) $makeSet(RiskCA(cA, 3) RiskCB(cB, 2), (totPaycA(cA, 7), totPaycB(cB, 6))) ---> $makeSet(RiskCB(cB, 2), ((totPaycA(cA, 7), totPaycB(cB, 6)), RiskCA(cA, 3))) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> RiskCB(cB, 2) L --> nil S --> RiskCA(cA, 3), totPaycA(cA, 7), totPaycB(cB, 6) $makeSet(RiskCB(cB, 2), (RiskCA(cA, 3), totPaycA(cA, 7), totPaycB(cB, 6))) ---> $makeSet(nil, ((RiskCA(cA, 3), totPaycA(cA, 7), totPaycB(cB, 6)), RiskCB(cB, 2))) *********** equation eq $makeSet(nil, S) = S . S --> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) $makeSet(nil, (RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6))) ---> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) *********** equation (built-in equation for symbol _=/=_) (RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6)) =/= (RiskCA( cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6)) ---> false *********** failure for condition fragment S =/= makeSet(L) = true *********** failure #692 *********** trial #693 ceq pAAr(rA, cA, P1) c pAAc(rA, cA, P2) c ineqAA(rA, cA, P3) = (pAAc(rA, cA, P2) c ineqAA(rA, cA, P1 - P2)) c pAAr(rA, cA, P1) if P3 =/= P1 - P2 = true [label getIneqAAc] . P1 --> 2 P2 --> 5 P3 --> -3 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 2 - 5 ---> -3 *********** equation (built-in equation for symbol _=/=_) -3 =/= -3 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #693 *********** trial #694 ceq pABr(rA, cB, P1) c pABc(rA, cB, P2) c ineqAB(rA, cB, P3) = (pABc(rA, cB, P2) c ineqAB(rA, cB, P1 - P2)) c pABr(rA, cB, P1) if P3 =/= P1 - P2 = true [label getIneqABc] . P1 --> 4 P2 --> 2 P3 --> 2 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 4 - 2 ---> 2 *********** equation (built-in equation for symbol _=/=_) 2 =/= 2 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #694 *********** trial #695 ceq pBAr(rB, cA, P1) c pBAc(rB, cA, P2) c ineqBA(rB, cA, P3) = (pBAc(rB, cA, P2) c ineqBA(rB, cA, P1 - P2)) c pBAr(rB, cA, P1) if P3 =/= P1 - P2 = true [label getIneqBAc] . P1 --> 4 P2 --> 2 P3 --> 2 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 4 - 2 ---> 2 *********** equation (built-in equation for symbol _=/=_) 2 =/= 2 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #695 *********** trial #696 ceq pBBr(rB, cB, P1) c pBBc(rB, cB, P2) c ineqBB(rB, cB, P3) = (pBBc(rB, cB, P2) c ineqBB(rB, cB, P1 - P2)) c pBBr(rB, cB, P1) if P3 =/= P1 - P2 = true [label getIneqAAc] . P1 --> 2 P2 --> 4 P3 --> -2 *********** solving condition fragment P3 =/= P1 - P2 = true *********** equation (built-in equation for symbol _-_) 2 - 4 ---> -2 *********** equation (built-in equation for symbol _=/=_) -2 =/= -2 ---> false *********** failure for condition fragment P3 =/= P1 - P2 = true *********** failure #696 *********** trial #697 ceq totIneqcA(cA, P) c ineqAA(rA, cA, P1) c ineqBA(rB, cA, P2) = (totIneqcA(cA, P1 + P2) c ineqBA(rB, cA, P2)) c ineqAA(rA, cA, P1) if P =/= P1 + P2 = true [label gettotIneqcA] . P --> -1 P1 --> -3 P2 --> 2 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + -3 ---> -1 *********** equation (built-in equation for symbol _=/=_) -1 =/= -1 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #697 *********** trial #698 ceq totIneqcB(cB, P) c ineqAB(rA, cB, P2) c ineqBB(rB, cB, P1) = (totIneqcB(cB, P1 + P2) c ineqAB(rA, cB, P2)) c ineqBB(rB, cB, P1) if P =/= P1 + P2 = true [label gettotIneqcB] . P --> 0 P2 --> 2 P1 --> -2 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + -2 ---> 0 *********** equation (built-in equation for symbol _=/=_) 0 =/= 0 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #698 *********** trial #699 ceq totPaycA(cA, P) c pAAc(rA, cA, P1) c pBAc(rB, cA, P2) = (totPaycA(cA, P1 + P2) c pBAc(rB, cA, P2)) c pAAc(rA, cA, P1) if P =/= P1 + P2 = true [label gettotPaycA] . P --> 7 P1 --> 5 P2 --> 2 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + 5 ---> 7 *********** equation (built-in equation for symbol _=/=_) 7 =/= 7 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #699 *********** trial #700 ceq totPaycB(cB, P) c pABc(rA, cB, P1) c pBBc(rB, cB, P2) = (totPaycB(cB, P1 + P2) c pBBc(rB, cB, P2)) c pABc(rA, cB, P1) if P =/= P1 + P2 = true [label gettotPaycB] . P --> 6 P1 --> 2 P2 --> 4 *********** solving condition fragment P =/= P1 + P2 = true *********** equation (built-in equation for symbol _+_) 2 + 4 ---> 6 *********** equation (built-in equation for symbol _=/=_) 6 =/= 6 ---> false *********** failure for condition fragment P =/= P1 + P2 = true *********** failure #700 *********** trial #701 ceq RiskCA(cA, P) c pAAc(rA, cA, P1) c pBAc(rB, cA, P2) = (RiskCA(cA, abs(P1 - P2)) c pBAc(rB, cA, P2)) c pAAc(rA, cA, P1) if P =/= abs(P1 - P2) = true [ label getRiskcA] . P --> 3 P1 --> 5 P2 --> 2 *********** solving condition fragment P =/= abs(P1 - P2) = true *********** equation (built-in equation for symbol _-_) 5 - 2 ---> 3 *********** equation (built-in equation for symbol abs) abs(3) ---> 3 *********** equation (built-in equation for symbol _=/=_) 3 =/= 3 ---> false *********** failure for condition fragment P =/= abs(P1 - P2) = true *********** failure #701 *********** trial #702 ceq RiskCB(cB, P) c pABc(rA, cB, P2) c pBBc(rB, cB, P1) = (RiskCB(cB, abs(P1 - P2)) c pABc(rA, cB, P2)) c pBBc(rB, cB, P1) if P =/= abs(P1 - P2) = true [ label getRiskcB] . P --> 2 P2 --> 2 P1 --> 4 *********** solving condition fragment P =/= abs(P1 - P2) = true *********** equation (built-in equation for symbol _-_) 4 - 2 ---> 2 *********** equation (built-in equation for symbol abs) abs(2) ---> 2 *********** equation (built-in equation for symbol _=/=_) 2 =/= 2 ---> false *********** failure for condition fragment P =/= abs(P1 - P2) = true *********** failure #702 *********** trial #703 ceq dec c timelim(X2) c watch(X1) c worklist(L) c workset(S) = TimeOut c watch( X1) c timelim(X2) c worklist(nil) c workset(empty) if X1 == X2 = true [ label timeOut] . X2 --> 100 X1 --> 4 L --> totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) S --> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) *********** solving condition fragment X1 == X2 = true *********** equation (built-in equation for symbol _==_) 4 == 100 ---> false *********** failure for condition fragment X1 == X2 = true *********** failure #703 *********** trial #704 ceq dec c worklist(L) c workset(S) = dec c worklist(L) c workset(makeSet(L)) if S =/= makeSet(L) = true [label listtoset] . L --> totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) S --> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) *********** solving condition fragment S =/= makeSet(L) = true *********** equation eq makeSet(L) = $makeSet(L, empty) . L --> totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) makeSet(totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2)) ---> $makeSet(totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), empty) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> totPaycA(cA, 7) L --> totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2) S --> empty $makeSet(totPaycA(cA, 7) totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), empty) ---> $makeSet(totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), (empty, totPaycA(cA, 7))) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> totPaycB(cB, 6) L --> RiskCA(cA, 3) RiskCB(cB, 2) S --> totPaycA(cA, 7) $makeSet(totPaycB(cB, 6) RiskCA(cA, 3) RiskCB(cB, 2), totPaycA(cA, 7)) ---> $makeSet(RiskCA(cA, 3) RiskCB(cB, 2), (totPaycA(cA, 7), totPaycB(cB, 6))) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> RiskCA(cA, 3) L --> RiskCB(cB, 2) S --> totPaycA(cA, 7), totPaycB(cB, 6) $makeSet(RiskCA(cA, 3) RiskCB(cB, 2), (totPaycA(cA, 7), totPaycB(cB, 6))) ---> $makeSet(RiskCB(cB, 2), ((totPaycA(cA, 7), totPaycB(cB, 6)), RiskCA(cA, 3))) *********** equation eq $makeSet(E:Fac L, S) = $makeSet(L, (S, E:Fac)) . E:Fac --> RiskCB(cB, 2) L --> nil S --> RiskCA(cA, 3), totPaycA(cA, 7), totPaycB(cB, 6) $makeSet(RiskCB(cB, 2), (RiskCA(cA, 3), totPaycA(cA, 7), totPaycB(cB, 6))) ---> $makeSet(nil, ((RiskCA(cA, 3), totPaycA(cA, 7), totPaycB(cB, 6)), RiskCB(cB, 2))) *********** equation eq $makeSet(nil, S) = S . S --> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) $makeSet(nil, (RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6))) ---> RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6) *********** equation (built-in equation for symbol _=/=_) (RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6)) =/= (RiskCA( cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6)) ---> false *********** failure for condition fragment S =/= makeSet(L) = true *********** failure #704 *********** re-solving condition fragment (size(L) < X2 - 1 and occurs(totPaycB(cB, P2), L) == false) and occurs( totPaycA(cA, P1), L) == false = true *********** failure for condition fragment (size(L) < X2 - 1 and occurs(totPaycB(cB, P2), L) == false) and occurs( totPaycA(cA, P1), L) == false = true *********** failure #661 *********** trial #705 crl dec c memcap(X2) c cognum(X3) c watch(X1) c worklist(L) c RiskCA(cA, P1) c RiskCB(cB, P2) => dec c RiskCA(cA, P1) c RiskCB(cB, P2) c watch(X1 + 2) c memcap(X2) c cognum(X3 + 2) c worklist(append(RiskCA(cA, P1) RiskCB(cB, P2), L)) if (size(L) < X2 - 1 and occurs(RiskCB(cB, P2), L) == false) and occurs(RiskCA(cA, P1), L) == false = true [label addRtolist] . X2 --> 4 X3 --> 2 X1 --> 2 L --> RiskCA(cA, 3) RiskCB(cB, 2) P1 --> 3 P2 --> 2 *********** solving condition fragment (size(L) < X2 - 1 and occurs(RiskCB(cB, P2), L) == false) and occurs(RiskCA(cA, P1), L) == false = true *********** equation eq size(L) = $size(L, 0) . L --> RiskCA(cA, 3) RiskCB(cB, 2) size(RiskCA(cA, 3) RiskCB(cB, 2)) ---> $size(RiskCA(cA, 3) RiskCB(cB, 2), 0) *********** equation eq $size(E:Fac L, C:Nat) = $size(L, C:Nat + 1) . E:Fac --> RiskCA(cA, 3) L --> RiskCB(cB, 2) C:Nat --> 0 $size(RiskCA(cA, 3) RiskCB(cB, 2), 0) ---> $size(RiskCB(cB, 2), 0 + 1) *********** equation (built-in equation for symbol _+_) 0 + 1 ---> 1 *********** equation eq $size(E:Fac L, C:Nat) = $size(L, C:Nat + 1) . E:Fac --> RiskCB(cB, 2) L --> nil C:Nat --> 1 $size(RiskCB(cB, 2), 1) ---> $size(nil, 1 + 1) *********** equation (built-in equation for symbol _+_) 1 + 1 ---> 2 *********** equation eq $size(nil, C:Nat) = C:Nat . C:Nat --> 2 $size(nil, 2) ---> 2 *********** equation (built-in equation for symbol _-_) 4 - 1 ---> 3 *********** equation (built-in equation for symbol _<_) 2 < 3 ---> true *********** equation eq occurs(E:Fac, E':Fac L) = if E:Fac == E':Fac then true else occurs(E:Fac, L) fi . E:Fac --> RiskCB(cB, 2) E':Fac --> RiskCA(cA, 3) L --> RiskCB(cB, 2) occurs(RiskCB(cB, 2), RiskCA(cA, 3) RiskCB(cB, 2)) ---> if RiskCB(cB, 2) == RiskCA(cA, 3) then true else occurs(RiskCB(cB, 2), RiskCB( cB, 2)) fi *********** equation (built-in equation for symbol _==_) RiskCB(cB, 2) == RiskCA(cA, 3) ---> false *********** equation (built-in equation for symbol if_then_else_fi) if false then true else occurs(RiskCB(cB, 2), RiskCB(cB, 2)) fi ---> occurs(RiskCB(cB, 2), RiskCB(cB, 2)) *********** equation eq occurs(E:Fac, E':Fac L) = if E:Fac == E':Fac then true else occurs(E:Fac, L) fi . E:Fac --> RiskCB(cB, 2) E':Fac --> RiskCB(cB, 2) L --> nil occurs(RiskCB(cB, 2), RiskCB(cB, 2)) ---> if RiskCB(cB, 2) == RiskCB(cB, 2) then true else occurs(RiskCB(cB, 2), nil) fi *********** equation (built-in equation for symbol _==_) RiskCB(cB, 2) == RiskCB(cB, 2) ---> true *********** equation (built-in equation for symbol if_then_else_fi) if true then true else occurs(RiskCB(cB, 2), nil) fi ---> true *********** equation (built-in equation for symbol _==_) true == false ---> false *********** equation eq true and A:Bool = A:Bool . A:Bool --> false true and false ---> false *********** equation eq occurs(E:Fac, E':Fac L) = if E:Fac == E':Fac then true else occurs(E:Fac, L) fi . E:Fac --> RiskCA(cA, 3) E':Fac --> RiskCA(cA, 3) L --> RiskCB(cB, 2) occurs(RiskCA(cA, 3), RiskCA(cA, 3) RiskCB(cB, 2)) ---> if RiskCA(cA, 3) == RiskCA(cA, 3) then true else occurs(RiskCA(cA, 3), RiskCB( cB, 2)) fi *********** equation (built-in equation for symbol _==_) RiskCA(cA, 3) == RiskCA(cA, 3) ---> true *********** equation (built-in equation for symbol if_then_else_fi) if true then true else occurs(RiskCA(cA, 3), RiskCB(cB, 2)) fi ---> true *********** equation (built-in equation for symbol _==_) true == false ---> false *********** equation eq false and A:Bool = false . A:Bool --> false false and false ---> false *********** failure for condition fragment (size(L) < X2 - 1 and occurs(RiskCB(cB, P2), L) == false) and occurs(RiskCA(cA, P1), L) == false = true *********** failure #705 *********** rule rl dec c cognum(X2) c watch(X1) c worklist(L) c workset((S, maxtotIneqC(cB, X))) => watch(X1 + 1) c cognum(X2 + 1) c worklist(nil) c workset(empty) c playA c dIonly [label avoidMaxI] . X2 --> 3 X1 --> 3 L --> maxtotIneqC(cB, 0) S --> empty X --> 0 dec c memcap(4) c cognum(3) c timelim(100) c watch(3) c worklist(maxtotIneqC( cB, 0)) c workset(maxtotIneqC(cB, 0)) c RiskCA(cA, 3) c RiskCB(cB, 2) c totPaycA(cA, 7) c totPaycB(cB, 6) c totIneqcA(cA, -1) c totIneqcB(cB, 0) c maxtotPayC(cX, 0) c maxRiskC(cX, 0) c pAAr(rA, cA, 2) c pABr(rA, cB, 4) c pBAr(rB, cA, 4) c pBBr(rB, cB, 2) c pAAc(rA, cA, 5) c pABc(rA, cB, 2) c pBAc(rB, cA, 2) c pBBc(rB, cB, 4) c ineqAA(rA, cA, -3) c ineqAB(rA, cB, 2) c ineqBA(rB, cA, 2) c ineqBB(rB, cB, -2) ---> (memcap(4) c timelim(100) c RiskCA(cA, 3) c RiskCB(cB, 2) c totPaycA(cA, 7) c totPaycB(cB, 6) c totIneqcA(cA, -1) c totIneqcB(cB, 0) c maxtotPayC(cX, 0) c maxRiskC(cX, 0) c pAAr(rA, cA, 2) c pABr(rA, cB, 4) c pBAr(rB, cA, 4) c pBBr(rB, cB, 2) c pAAc(rA, cA, 5) c pABc(rA, cB, 2) c pBAc(rB, cA, 2) c pBBc(rB, cB, 4) c ineqAA(rA, cA, -3) c ineqAB(rA, cB, 2) c ineqBA(rB, cA, 2) c ineqBB(rB, cB, -2)) c watch(3 + 1) c cognum(3 + 1) c worklist(nil) c workset(empty) c playA c dIonly c workset(empty) c (workset((risk)) ****