This would be one of the things i would like to extract: starting with this workset((RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(cB, 6))) ending with dIonly.
However as you can see, it is important to reverse the string beforehand, because there are several worksets before and after the desired one.
When I have this working I would then run another code again on the output extracting the workset with two brackets that is remaining after the first round of extracting the string. That is the plan.
Sorry about the long string now, but this is the only way it can make sense.
workset((
RiskCA(cA, 3) RiskCB(cB, 2)) c
workset((RiskCA(cA, 3), RiskCB(cB, 2), totPaycA(cA, 7), totPaycB(c
+B, 6)))
*********** trial #682
ceq pAAr(rA, cA, P1) c pAAc(rA, cA, P2) c ineqAA(rA, cA, P3) = (pAAc(r
+A, cA,
P2) c ineqAA(rA, cA, P1 - P2)) c pAAr(rA, cA, P1) if P3 =/= P1 - P
+2 = 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(r
+A, cB,
P2) c ineqAB(rA, cB, P1 - P2)) c pABr(rA, cB, P1) if P3 =/= P1 - P
+2 = 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(r
+B, cA,
P2) c ineqBA(rB, cA, P1 - P2)) c pBAr(rB, cA, P1) if P3 =/= P1 - P
+2 = 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(r
+B, cB,
P2) c ineqBB(rB, cB, P1 - P2)) c pBBr(rB, cB, P1) if P3 =/= P1 - P
+2 = 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) = (totI
+neqcA(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) = (totI
+neqcB(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(makeS
+et(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)), Risk
+CB(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(r
+A, cA,
P2) c ineqAA(rA, cA, P1 - P2)) c pAAr(rA, cA, P1) if P3 =/= P1 - P
+2 = 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(r
+A, cB,
P2) c ineqAB(rA, cB, P1 - P2)) c pABr(rA, cB, P1) if P3 =/= P1 - P
+2 = 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(r
+B, cA,
P2) c ineqBA(rB, cA, P1 - P2)) c pBAr(rB, cA, P1) if P3 =/= P1 - P
+2 = 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(r
+B, cB,
P2) c ineqBB(rB, cB, P1 - P2)) c pBBr(rB, cB, P1) if P3 =/= P1 - P
+2 = 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) = (totI
+neqcA(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) = (totI
+neqcB(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 = t
+rue [
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(makeS
+et(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)), Risk
+CB(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(c
+A, 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) RiskC
+B(cB,
P2), L)) if (size(L) < X2 - 1 and occurs(RiskCB(cB, P2), L) == fal
+se) 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(R
+iskCA(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(R
+iskCA(cA,
P1), L) == false = true
*********** failure #705
*********** rule
rl dec c cognum(X2) c watch(X1) c worklist(L) c workset((S, maxtotIneq
+C(cB,
X))) => watch(X1 + 1) c cognum(X2 + 1) c worklist(nil) c workset(e
+mpty) 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(maxto
+tIneqC(
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, c
+B, 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(c
+A, 7) c
totPaycB(cB, 6) c totIneqcA(cA, -1) c totIneqcB(cB, 0) c maxtotPay
+C(cX, 0)
c maxRiskC(cX, 0) c pAAr(rA, cA, 2) c pABr(rA, cB, 4) c pBAr(rB, c
+A, 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)
+)
****