Left Termination proof of /tmp/tmpRj701u/times.pl

Left Termination of the query pattern times_in_3(g, g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 PiDPToQDPProof (⇐)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔)

        ↳11 YES

    ↳12 PiDP

        ↳13 PiDPToQDPProof (⇐)

        ↳14 QDP

        ↳15 QDPSizeChangeProof (⇔)

        ↳16 YES

    ↳17 PiDP

        ↳18 PiDPToQDPProof (⇐)

        ↳19 QDP

        ↳20 QDPSizeChangeProof (⇔)

        ↳21 YES

    ↳22 PiDP

        ↳23 PiDPToQDPProof (⇐)

        ↳24 QDP

        ↳25 QDPSizeChangeProof (⇔)

        ↳26 YES

    ↳27 PiDP

        ↳28 PiDPToQDPProof (⇐)

        ↳29 QDP

        ↳30 QDPSizeChangeProof (⇔)

        ↳31 YES

    ↳32 PiDP

        ↳33 PiDPToQDPProof (⇐)

        ↳34 QDP

        ↳35 QDPSizeChangeProof (⇔)

        ↳36 YES

    ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔)

        ↳41 YES

    ↳42 PiDP

        ↳43 PiDPToQDPProof (⇐)

        ↳44 QDP

        ↳45 QDPSizeChangeProof (⇔)

        ↳46 YES

    ↳47 PiDP

        ↳48 PiDPToQDPProof (⇐)

        ↳49 QDP

        ↳50 QDPSizeChangeProof (⇔)

        ↳51 YES

(0) Obligation:

Clauses:

times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, 0).
mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z).
mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z).

Queries:

times(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: times(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: times(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: mult(T7, T8, 0, T10)\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 1 | mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 2 | mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 2 | mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: mult(T28, T29, T29, T31)\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 1 | mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 2 | mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 1\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 2 | mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 2\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: mult(T51, 0, 0, T54)\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 1 | mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 2 | mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 1\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 2 | mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 2\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: mult(T63, 0, 0, T65)\n\nT63 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: mult(T75, s(T77), T77, T79)\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 1 | mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 2 | mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 1\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 2 | mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 2\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: mult(T99, s(0), s(0), T102)\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 1 | mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 2 | mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 3\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 2 | mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 3\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 3\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: mult(T111, s(0), 0, T113)\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 1 | mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 2 | mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 3\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 1\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 2 | mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 3\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 2\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: mult(T111, s(0), 0, T113), SCOPE: 7, CLAUSE: 3\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: mult(T122, s(0), s(0), T124)\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: mult(T137, s(s(T139)), T139, T141)\n\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 1 | mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 2 | mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 3\n\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 1\n\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 2 | mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 3\n\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 2\n\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: mult(T137, s(s(T139)), T139, T141), SCOPE: 8, CLAUSE: 3\n\nT137 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: mult(T161, s(s(0)), s(s(0)), T164)\n\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: mult(T161, s(s(0)), s(s(0)), T164), SCOPE: 9, CLAUSE: 1 | mult(T161, s(s(0)), s(s(0)), T164), SCOPE: 9, CLAUSE: 2 | mult(T161, s(s(0)), s(s(0)), T164), SCOPE: 9, CLAUSE: 3\n\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: mult(T161, s(s(0)), s(s(0)), T164), SCOPE: 9, CLAUSE: 2 | mult(T161, s(s(0)), s(s(0)), T164), SCOPE: 9, CLAUSE: 3\n\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: mult(T161, s(s(0)), s(s(0)), T164), SCOPE: 9, CLAUSE: 3\n\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: mult(T173, s(s(0)), s(0), T175)\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: mult(T173, s(s(0)), s(0), T175), SCOPE: 10, CLAUSE: 1 | mult(T173, s(s(0)), s(0), T175), SCOPE: 10, CLAUSE: 2 | mult(T173, s(s(0)), s(0), T175), SCOPE: 10, CLAUSE: 3\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: mult(T173, s(s(0)), s(0), T175), SCOPE: 10, CLAUSE: 2 | mult(T173, s(s(0)), s(0), T175), SCOPE: 10, CLAUSE: 3\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: mult(T173, s(s(0)), s(0), T175), SCOPE: 10, CLAUSE: 3\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: mult(T184, s(s(0)), 0, T186)\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 1 | mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 2 | mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 3\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 1\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 2 | mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 3\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 2\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: mult(T184, s(s(0)), 0, T186), SCOPE: 11, CLAUSE: 3\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: mult(T195, s(s(0)), s(s(0)), T197)\n\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: mult(T210, s(s(s(T212))), T212, T214)\n\nT210 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 1 | mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 2 | mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 3\n\nT210 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 1\n\nT210 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 2 | mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 3\n\nT210 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 2\n\nT210 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: mult(T210, s(s(s(T212))), T212, T214), SCOPE: 12, CLAUSE: 3\n\nT210 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: mult(T234, s(s(s(0))), s(s(s(0))), T237)\n\nT234 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: mult(T234, s(s(s(0))), s(s(s(0))), T237), SCOPE: 13, CLAUSE: 1 | mult(T234, s(s(s(0))), s(s(s(0))), T237), SCOPE: 13, CLAUSE: 2 | mult(T234, s(s(s(0))), s(s(s(0))), T237), SCOPE: 13, CLAUSE: 3\n\nT234 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: mult(T234, s(s(s(0))), s(s(s(0))), T237), SCOPE: 13, CLAUSE: 2 | mult(T234, s(s(s(0))), s(s(s(0))), T237), SCOPE: 13, CLAUSE: 3\n\nT234 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: mult(T234, s(s(s(0))), s(s(s(0))), T237), SCOPE: 13, CLAUSE: 3\n\nT234 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: mult(T246, s(s(s(0))), s(s(0)), T248)\n\nT246 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: mult(T246, s(s(s(0))), s(s(0)), T248), SCOPE: 14, CLAUSE: 1 | mult(T246, s(s(s(0))), s(s(0)), T248), SCOPE: 14, CLAUSE: 2 | mult(T246, s(s(s(0))), s(s(0)), T248), SCOPE: 14, CLAUSE: 3\n\nT246 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: mult(T246, s(s(s(0))), s(s(0)), T248), SCOPE: 14, CLAUSE: 2 | mult(T246, s(s(s(0))), s(s(0)), T248), SCOPE: 14, CLAUSE: 3\n\nT246 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: mult(T246, s(s(s(0))), s(s(0)), T248), SCOPE: 14, CLAUSE: 3\n\nT246 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: mult(T257, s(s(s(0))), s(0), T259)\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: mult(T257, s(s(s(0))), s(0), T259), SCOPE: 15, CLAUSE: 1 | mult(T257, s(s(s(0))), s(0), T259), SCOPE: 15, CLAUSE: 2 | mult(T257, s(s(s(0))), s(0), T259), SCOPE: 15, CLAUSE: 3\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: mult(T257, s(s(s(0))), s(0), T259), SCOPE: 15, CLAUSE: 2 | mult(T257, s(s(s(0))), s(0), T259), SCOPE: 15, CLAUSE: 3\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: mult(T257, s(s(s(0))), s(0), T259), SCOPE: 15, CLAUSE: 3\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: mult(T268, s(s(s(0))), 0, T270)\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 1 | mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 2 | mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 3\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 1\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 2 | mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 3\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 2\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: mult(T268, s(s(s(0))), 0, T270), SCOPE: 16, CLAUSE: 3\n\nT268 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: mult(T279, s(s(s(0))), s(s(s(0))), T281)\n\nT279 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: mult(T294, s(s(s(s(T296)))), T296, T298)\n\nT294 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 1 | mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 2 | mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 3\n\nT294 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 1\n\nT294 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 2 | mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 3\n\nT294 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 2\n\nT294 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: mult(T294, s(s(s(s(T296)))), T296, T298), SCOPE: 17, CLAUSE: 3\n\nT294 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321)\n\nT318 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321), SCOPE: 18, CLAUSE: 1 | mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321), SCOPE: 18, CLAUSE: 2 | mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321), SCOPE: 18, CLAUSE: 3\n\nT318 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321), SCOPE: 18, CLAUSE: 2 | mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321), SCOPE: 18, CLAUSE: 3\n\nT318 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: mult(T318, s(s(s(s(0)))), s(s(s(s(0)))), T321), SCOPE: 18, CLAUSE: 3\n\nT318 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: mult(T330, s(s(s(s(0)))), s(s(s(0))), T332)\n\nT330 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: mult(T330, s(s(s(s(0)))), s(s(s(0))), T332), SCOPE: 19, CLAUSE: 1 | mult(T330, s(s(s(s(0)))), s(s(s(0))), T332), SCOPE: 19, CLAUSE: 2 | mult(T330, s(s(s(s(0)))), s(s(s(0))), T332), SCOPE: 19, CLAUSE: 3\n\nT330 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: mult(T330, s(s(s(s(0)))), s(s(s(0))), T332), SCOPE: 19, CLAUSE: 2 | mult(T330, s(s(s(s(0)))), s(s(s(0))), T332), SCOPE: 19, CLAUSE: 3\n\nT330 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: mult(T330, s(s(s(s(0)))), s(s(s(0))), T332), SCOPE: 19, CLAUSE: 3\n\nT330 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: mult(T341, s(s(s(s(0)))), s(s(0)), T343)\n\nT341 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: mult(T341, s(s(s(s(0)))), s(s(0)), T343), SCOPE: 20, CLAUSE: 1 | mult(T341, s(s(s(s(0)))), s(s(0)), T343), SCOPE: 20, CLAUSE: 2 | mult(T341, s(s(s(s(0)))), s(s(0)), T343), SCOPE: 20, CLAUSE: 3\n\nT341 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: mult(T341, s(s(s(s(0)))), s(s(0)), T343), SCOPE: 20, CLAUSE: 2 | mult(T341, s(s(s(s(0)))), s(s(0)), T343), SCOPE: 20, CLAUSE: 3\n\nT341 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: mult(T341, s(s(s(s(0)))), s(s(0)), T343), SCOPE: 20, CLAUSE: 3\n\nT341 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: mult(T352, s(s(s(s(0)))), s(0), T354)\n\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: mult(T352, s(s(s(s(0)))), s(0), T354), SCOPE: 21, CLAUSE: 1 | mult(T352, s(s(s(s(0)))), s(0), T354), SCOPE: 21, CLAUSE: 2 | mult(T352, s(s(s(s(0)))), s(0), T354), SCOPE: 21, CLAUSE: 3\n\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: mult(T352, s(s(s(s(0)))), s(0), T354), SCOPE: 21, CLAUSE: 2 | mult(T352, s(s(s(s(0)))), s(0), T354), SCOPE: 21, CLAUSE: 3\n\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: mult(T352, s(s(s(s(0)))), s(0), T354), SCOPE: 21, CLAUSE: 3\n\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: mult(T363, s(s(s(s(0)))), 0, T365)\n\nT363 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 1 | mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 2 | mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 3\n\nT363 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 1\n\nT363 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 2 | mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 3\n\nT363 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 2\n\nT363 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: mult(T363, s(s(s(s(0)))), 0, T365), SCOPE: 22, CLAUSE: 3\n\nT363 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: mult(T374, s(s(s(s(0)))), s(s(s(s(0)))), T376)\n\nT374 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: mult(T389, s(s(s(s(s(T391))))), T391, T393)\n\nT389 is ground\nT391 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 1 | mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 2 | mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 3\n\nT389 is ground\nT391 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 1\n\nT389 is ground\nT391 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 2 | mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 3\n\nT389 is ground\nT391 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 2\n\nT389 is ground\nT391 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: mult(T389, s(s(s(s(s(T391))))), T391, T393), SCOPE: 23, CLAUSE: 3\n\nT389 is ground\nT391 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416)\n\nT413 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416), SCOPE: 24, CLAUSE: 1 | mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416), SCOPE: 24, CLAUSE: 2 | mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416), SCOPE: 24, CLAUSE: 3\n\nT413 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416), SCOPE: 24, CLAUSE: 2 | mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416), SCOPE: 24, CLAUSE: 3\n\nT413 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: mult(T413, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T416), SCOPE: 24, CLAUSE: 3\n\nT413 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427)\n\nT425 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427), SCOPE: 25, CLAUSE: 1 | mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427), SCOPE: 25, CLAUSE: 2 | mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427), SCOPE: 25, CLAUSE: 3\n\nT425 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427), SCOPE: 25, CLAUSE: 2 | mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427), SCOPE: 25, CLAUSE: 3\n\nT425 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: mult(T425, s(s(s(s(s(0))))), s(s(s(s(0)))), T427), SCOPE: 25, CLAUSE: 3\n\nT425 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438)\n\nT436 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438), SCOPE: 26, CLAUSE: 1 | mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438), SCOPE: 26, CLAUSE: 2 | mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438), SCOPE: 26, CLAUSE: 3\n\nT436 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438), SCOPE: 26, CLAUSE: 2 | mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438), SCOPE: 26, CLAUSE: 3\n\nT436 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: mult(T436, s(s(s(s(s(0))))), s(s(s(0))), T438), SCOPE: 26, CLAUSE: 3\n\nT436 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: mult(T447, s(s(s(s(s(0))))), s(s(0)), T449)\n\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: mult(T447, s(s(s(s(s(0))))), s(s(0)), T449), SCOPE: 27, CLAUSE: 1 | mult(T447, s(s(s(s(s(0))))), s(s(0)), T449), SCOPE: 27, CLAUSE: 2 | mult(T447, s(s(s(s(s(0))))), s(s(0)), T449), SCOPE: 27, CLAUSE: 3\n\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: mult(T447, s(s(s(s(s(0))))), s(s(0)), T449), SCOPE: 27, CLAUSE: 2 | mult(T447, s(s(s(s(s(0))))), s(s(0)), T449), SCOPE: 27, CLAUSE: 3\n\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: mult(T447, s(s(s(s(s(0))))), s(s(0)), T449), SCOPE: 27, CLAUSE: 3\n\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: mult(T458, s(s(s(s(s(0))))), s(0), T460)\n\nT458 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: mult(T458, s(s(s(s(s(0))))), s(0), T460), SCOPE: 28, CLAUSE: 1 | mult(T458, s(s(s(s(s(0))))), s(0), T460), SCOPE: 28, CLAUSE: 2 | mult(T458, s(s(s(s(s(0))))), s(0), T460), SCOPE: 28, CLAUSE: 3\n\nT458 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: mult(T458, s(s(s(s(s(0))))), s(0), T460), SCOPE: 28, CLAUSE: 2 | mult(T458, s(s(s(s(s(0))))), s(0), T460), SCOPE: 28, CLAUSE: 3\n\nT458 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: mult(T458, s(s(s(s(s(0))))), s(0), T460), SCOPE: 28, CLAUSE: 3\n\nT458 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: mult(T469, s(s(s(s(s(0))))), 0, T471)\n\nT469 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 1 | mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 2 | mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 3\n\nT469 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 1\n\nT469 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 2 | mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 3\n\nT469 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 2\n\nT469 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: mult(T469, s(s(s(s(s(0))))), 0, T471), SCOPE: 29, CLAUSE: 3\n\nT469 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: mult(T480, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T482)\n\nT480 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: mult(T495, s(s(s(s(s(s(T497)))))), T497, T499)\n\nT495 is ground\nT497 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 1 | mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 2 | mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 3\n\nT495 is ground\nT497 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 1\n\nT495 is ground\nT497 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 2 | mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 3\n\nT495 is ground\nT497 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 2\n\nT495 is ground\nT497 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: mult(T495, s(s(s(s(s(s(T497)))))), T497, T499), SCOPE: 30, CLAUSE: 3\n\nT495 is ground\nT497 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522)\n\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522), SCOPE: 31, CLAUSE: 1 | mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522), SCOPE: 31, CLAUSE: 2 | mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522), SCOPE: 31, CLAUSE: 3\n\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522), SCOPE: 31, CLAUSE: 2 | mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522), SCOPE: 31, CLAUSE: 3\n\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T522), SCOPE: 31, CLAUSE: 3\n\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533)\n\nT531 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533), SCOPE: 32, CLAUSE: 1 | mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533), SCOPE: 32, CLAUSE: 2 | mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533), SCOPE: 32, CLAUSE: 3\n\nT531 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533), SCOPE: 32, CLAUSE: 2 | mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533), SCOPE: 32, CLAUSE: 3\n\nT531 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: mult(T531, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T533), SCOPE: 32, CLAUSE: 3\n\nT531 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544)\n\nT542 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544), SCOPE: 33, CLAUSE: 1 | mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544), SCOPE: 33, CLAUSE: 2 | mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544), SCOPE: 33, CLAUSE: 3\n\nT542 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544), SCOPE: 33, CLAUSE: 2 | mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544), SCOPE: 33, CLAUSE: 3\n\nT542 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: mult(T542, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T544), SCOPE: 33, CLAUSE: 3\n\nT542 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555)\n\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555), SCOPE: 34, CLAUSE: 1 | mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555), SCOPE: 34, CLAUSE: 2 | mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555), SCOPE: 34, CLAUSE: 3\n\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555), SCOPE: 34, CLAUSE: 2 | mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555), SCOPE: 34, CLAUSE: 3\n\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: mult(T553, s(s(s(s(s(s(0)))))), s(s(s(0))), T555), SCOPE: 34, CLAUSE: 3\n\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566)\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566), SCOPE: 35, CLAUSE: 1 | mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566), SCOPE: 35, CLAUSE: 2 | mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566), SCOPE: 35, CLAUSE: 3\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566), SCOPE: 35, CLAUSE: 2 | mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566), SCOPE: 35, CLAUSE: 3\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: mult(T564, s(s(s(s(s(s(0)))))), s(s(0)), T566), SCOPE: 35, CLAUSE: 3\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: mult(T575, s(s(s(s(s(s(0)))))), s(0), T577)\n\nT575 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: mult(T575, s(s(s(s(s(s(0)))))), s(0), T577), SCOPE: 36, CLAUSE: 1 | mult(T575, s(s(s(s(s(s(0)))))), s(0), T577), SCOPE: 36, CLAUSE: 2 | mult(T575, s(s(s(s(s(s(0)))))), s(0), T577), SCOPE: 36, CLAUSE: 3\n\nT575 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: mult(T575, s(s(s(s(s(s(0)))))), s(0), T577), SCOPE: 36, CLAUSE: 2 | mult(T575, s(s(s(s(s(s(0)))))), s(0), T577), SCOPE: 36, CLAUSE: 3\n\nT575 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: mult(T575, s(s(s(s(s(s(0)))))), s(0), T577), SCOPE: 36, CLAUSE: 3\n\nT575 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: mult(T586, s(s(s(s(s(s(0)))))), 0, T588)\n\nT586 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 1 | mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 2 | mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 3\n\nT586 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 1\n\nT586 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 2 | mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 3\n\nT586 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 2\n\nT586 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: mult(T586, s(s(s(s(s(s(0)))))), 0, T588), SCOPE: 37, CLAUSE: 3\n\nT586 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: mult(T597, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T599)\n\nT597 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616)\n\nT612 is ground\nT614 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 1 | mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 2 | mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 3\n\nT612 is ground\nT614 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 1\n\nT612 is ground\nT614 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 2 | mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 3\n\nT612 is ground\nT614 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 2\n\nT612 is ground\nT614 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: mult(T612, s(s(s(s(s(s(s(T614))))))), T614, T616), SCOPE: 38, CLAUSE: 3\n\nT612 is ground\nT614 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639)\n\nT636 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639), SCOPE: 39, CLAUSE: 1 | mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639), SCOPE: 39, CLAUSE: 2 | mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639), SCOPE: 39, CLAUSE: 3\n\nT636 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639), SCOPE: 39, CLAUSE: 2 | mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639), SCOPE: 39, CLAUSE: 3\n\nT636 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: mult(T636, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T639), SCOPE: 39, CLAUSE: 3\n\nT636 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650)\n\nT648 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650), SCOPE: 40, CLAUSE: 1 | mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650), SCOPE: 40, CLAUSE: 2 | mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650), SCOPE: 40, CLAUSE: 3\n\nT648 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650), SCOPE: 40, CLAUSE: 2 | mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650), SCOPE: 40, CLAUSE: 3\n\nT648 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: mult(T648, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T650), SCOPE: 40, CLAUSE: 3\n\nT648 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661)\n\nT659 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661), SCOPE: 41, CLAUSE: 1 | mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661), SCOPE: 41, CLAUSE: 2 | mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661), SCOPE: 41, CLAUSE: 3\n\nT659 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661), SCOPE: 41, CLAUSE: 2 | mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661), SCOPE: 41, CLAUSE: 3\n\nT659 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: mult(T659, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T661), SCOPE: 41, CLAUSE: 3\n\nT659 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672)\n\nT670 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672), SCOPE: 42, CLAUSE: 1 | mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672), SCOPE: 42, CLAUSE: 2 | mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672), SCOPE: 42, CLAUSE: 3\n\nT670 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672), SCOPE: 42, CLAUSE: 2 | mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672), SCOPE: 42, CLAUSE: 3\n\nT670 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: mult(T670, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T672), SCOPE: 42, CLAUSE: 3\n\nT670 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683)\n\nT681 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="310: mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683), SCOPE: 43, CLAUSE: 1 | mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683), SCOPE: 43, CLAUSE: 2 | mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683), SCOPE: 43, CLAUSE: 3\n\nT681 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683), SCOPE: 43, CLAUSE: 2 | mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683), SCOPE: 43, CLAUSE: 3\n\nT681 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
312 [label="312: mult(T681, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T683), SCOPE: 43, CLAUSE: 3\n\nT681 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
313 [label="313: mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694)\n\nT692 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694), SCOPE: 44, CLAUSE: 1 | mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694), SCOPE: 44, CLAUSE: 2 | mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694), SCOPE: 44, CLAUSE: 3\n\nT692 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694), SCOPE: 44, CLAUSE: 2 | mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694), SCOPE: 44, CLAUSE: 3\n\nT692 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: mult(T692, s(s(s(s(s(s(s(0))))))), s(s(0)), T694), SCOPE: 44, CLAUSE: 3\n\nT692 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705)\n\nT703 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705), SCOPE: 45, CLAUSE: 1 | mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705), SCOPE: 45, CLAUSE: 2 | mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705), SCOPE: 45, CLAUSE: 3\n\nT703 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705), SCOPE: 45, CLAUSE: 2 | mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705), SCOPE: 45, CLAUSE: 3\n\nT703 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: mult(T703, s(s(s(s(s(s(s(0))))))), s(0), T705), SCOPE: 45, CLAUSE: 3\n\nT703 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716)\n\nT714 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 1 | mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 2 | mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 3\n\nT714 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 1\n\nT714 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 2 | mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 3\n\nT714 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 2\n\nT714 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: mult(T714, s(s(s(s(s(s(s(0))))))), 0, T716), SCOPE: 46, CLAUSE: 3\n\nT714 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: mult(T725, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T727)\n\nT725 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: mult(T740, s(s(s(s(s(s(s(s(T742)))))))), T742, T744)\n\nT740 is ground\nT742 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: mult(T740, s(T747), T742, T744)\n\nT740 is ground\nT742 is ground\nT747 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 1 | mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 2 | mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 3\n\nT740 is ground\nT742 is ground\nT747 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 1\n\nT740 is ground\nT742 is ground\nT747 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 2 | mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 3\n\nT740 is ground\nT742 is ground\nT747 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
344 [label="344: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
345 [label="345: mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 2\n\nT740 is ground\nT742 is ground\nT747 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: mult(T740, s(T747), T742, T744), SCOPE: 47, CLAUSE: 3\n\nT740 is ground\nT742 is ground\nT747 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: mult(T767, s(T768), s(T768), T770)\n\nT767 is ground\nT768 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: mult(T786, s(T787), T788, T790)\n\nT786 is ground\nT787 is ground\nT788 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="350: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 352 [arrowhead = none ];
352 -> 2;

353 [label="ONLY EVAL with clause\ntimes(X4, X5, X6) :- mult(X4, X5, 0, X6).\nand substitution\nT1 -> T7\nX4 -> T7\nT2 -> T8\nX5 -> T8\nT3 -> T10\nX6 -> T10\nT9 -> T10", fontsize=14, style = filled, fillcolor = white];
2 -> 353 [arrowhead = none ];
353 -> 3;

354 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 354 [arrowhead = none ];
354 -> 4;

355 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 355 [arrowhead = none ];
355 -> 5;

356 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 356 [arrowhead = none ];
356 -> 6;

357 [label="EVAL with clause\nmult(0, X11, 0, 0).\nand substitution\nT7 -> 0\nT8 -> T15\nX11 -> T15\nT10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 357 [arrowhead = none ];
357 -> 7;

358 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 358 [arrowhead = none ];
358 -> 8;

359 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 359 [arrowhead = none ];
359 -> 10;

360 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 360 [arrowhead = none ];
360 -> 11;

361 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 361 [arrowhead = none ];
361 -> 9;

362 [label="EVAL with clause\nmult(s(X25), X26, 0, X27) :- mult(X25, X26, X26, X27).\nand substitution\nX25 -> T28\nT7 -> s(T28)\nT8 -> T29\nX26 -> T29\nT10 -> T31\nX27 -> T31\nT30 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 362 [arrowhead = none ];
362 -> 12;

363 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 363 [arrowhead = none ];
363 -> 13;

364 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
11 -> 364 [arrowhead = none ];
364 -> 351;

365 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 365 [arrowhead = none ];
365 -> 14;

366 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 366 [arrowhead = none ];
366 -> 15;

367 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 367 [arrowhead = none ];
367 -> 16;

368 [label="EVAL with clause\nmult(0, X37, 0, 0).\nand substitution\nT28 -> 0\nT29 -> 0\nX37 -> 0\nT38 -> 0\nT31 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 368 [arrowhead = none ];
368 -> 17;

369 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 369 [arrowhead = none ];
369 -> 18;

370 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 370 [arrowhead = none ];
370 -> 20;

371 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 371 [arrowhead = none ];
371 -> 21;

372 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 372 [arrowhead = none ];
372 -> 19;

373 [label="EVAL with clause\nmult(s(X51), X52, 0, X53) :- mult(X51, X52, X52, X53).\nand substitution\nX51 -> T51\nT28 -> s(T51)\nT29 -> 0\nX52 -> 0\nT52 -> 0\nT31 -> T54\nX53 -> T54\nT53 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 373 [arrowhead = none ];
373 -> 22;

374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 374 [arrowhead = none ];
374 -> 23;

375 [label="EVAL with clause\nmult(X97, X98, s(X99), s(X100)) :- mult(X97, X98, X99, X100).\nand substitution\nT28 -> T75\nX97 -> T75\nT29 -> s(T77)\nX98 -> s(T77)\nX99 -> T77\nT76 -> s(T77)\nX100 -> T79\nT31 -> s(T79)\nT78 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 375 [arrowhead = none ];
375 -> 35;

376 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 376 [arrowhead = none ];
376 -> 36;

377 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 377 [arrowhead = none ];
377 -> 24;

378 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 378 [arrowhead = none ];
378 -> 25;

379 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 379 [arrowhead = none ];
379 -> 26;

380 [label="EVAL with clause\nmult(0, X63, 0, 0).\nand substitution\nT51 -> 0\nX63 -> 0\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 380 [arrowhead = none ];
380 -> 27;

381 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 381 [arrowhead = none ];
381 -> 28;

382 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 382 [arrowhead = none ];
382 -> 30;

383 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 383 [arrowhead = none ];
383 -> 31;

384 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 384 [arrowhead = none ];
384 -> 29;

385 [label="EVAL with clause\nmult(s(X77), X78, 0, X79) :- mult(X77, X78, X78, X79).\nand substitution\nX77 -> T63\nT51 -> s(T63)\nX78 -> 0\nT54 -> T65\nX79 -> T65\nT64 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 385 [arrowhead = none ];
385 -> 32;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 386 [arrowhead = none ];
386 -> 33;

387 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
31 -> 387 [arrowhead = none ];
387 -> 34;

388 [label="INSTANCE with matching:\nT51 -> T63\nT54 -> T65", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 388 [arrowhead = none , style=dashed];
388 -> 22[style=dashed];

389 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 389 [arrowhead = none ];
389 -> 37;

390 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 390 [arrowhead = none ];
390 -> 38;

391 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 391 [arrowhead = none ];
391 -> 39;

392 [label="EVAL with clause\nmult(0, X111, 0, 0).\nand substitution\nT75 -> 0\nT77 -> 0\nX111 -> s(0)\nT86 -> 0\nT79 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 392 [arrowhead = none ];
392 -> 40;

393 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 393 [arrowhead = none ];
393 -> 41;

394 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 394 [arrowhead = none ];
394 -> 43;

395 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 395 [arrowhead = none ];
395 -> 44;

396 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 396 [arrowhead = none ];
396 -> 42;

397 [label="EVAL with clause\nmult(s(X125), X126, 0, X127) :- mult(X125, X126, X126, X127).\nand substitution\nX125 -> T99\nT75 -> s(T99)\nT77 -> 0\nX126 -> s(0)\nT100 -> 0\nT79 -> T102\nX127 -> T102\nT101 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 397 [arrowhead = none ];
397 -> 45;

398 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 398 [arrowhead = none ];
398 -> 46;

399 [label="EVAL with clause\nmult(X207, X208, s(X209), s(X210)) :- mult(X207, X208, X209, X210).\nand substitution\nT75 -> T137\nX207 -> T137\nT77 -> s(T139)\nX208 -> s(s(T139))\nX209 -> T139\nT138 -> s(T139)\nX210 -> T141\nT79 -> s(T141)\nT140 -> T141", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 399 [arrowhead = none ];
399 -> 63;

400 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 400 [arrowhead = none ];
400 -> 64;

401 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 401 [arrowhead = none ];
401 -> 47;

402 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
47 -> 402 [arrowhead = none ];
402 -> 48;

403 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
48 -> 403 [arrowhead = none ];
403 -> 49;

404 [label="EVAL with clause\nmult(X152, X153, s(X154), s(X155)) :- mult(X152, X153, X154, X155).\nand substitution\nT99 -> T111\nX152 -> T111\nX153 -> s(0)\nX154 -> 0\nX155 -> T113\nT102 -> s(T113)\nT112 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 404 [arrowhead = none ];
404 -> 50;

405 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 405 [arrowhead = none ];
405 -> 51;

406 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 406 [arrowhead = none ];
406 -> 52;

407 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 407 [arrowhead = none ];
407 -> 53;

408 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 408 [arrowhead = none ];
408 -> 54;

409 [label="EVAL with clause\nmult(0, X166, 0, 0).\nand substitution\nT111 -> 0\nX166 -> s(0)\nT113 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 409 [arrowhead = none ];
409 -> 55;

410 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 410 [arrowhead = none ];
410 -> 56;

411 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 411 [arrowhead = none ];
411 -> 58;

412 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 412 [arrowhead = none ];
412 -> 59;

413 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 413 [arrowhead = none ];
413 -> 57;

414 [label="EVAL with clause\nmult(s(X180), X181, 0, X182) :- mult(X180, X181, X181, X182).\nand substitution\nX180 -> T122\nT111 -> s(T122)\nX181 -> s(0)\nT113 -> T124\nX182 -> T124\nT123 -> T124", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 414 [arrowhead = none ];
414 -> 60;

415 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 415 [arrowhead = none ];
415 -> 61;

416 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
59 -> 416 [arrowhead = none ];
416 -> 62;

417 [label="INSTANCE with matching:\nT99 -> T122\nT102 -> T124", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 417 [arrowhead = none , style=dashed];
417 -> 45[style=dashed];

418 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 418 [arrowhead = none ];
418 -> 65;

419 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 419 [arrowhead = none ];
419 -> 66;

420 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 420 [arrowhead = none ];
420 -> 67;

421 [label="EVAL with clause\nmult(0, X221, 0, 0).\nand substitution\nT137 -> 0\nT139 -> 0\nX221 -> s(s(0))\nT148 -> 0\nT141 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 421 [arrowhead = none ];
421 -> 68;

422 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 422 [arrowhead = none ];
422 -> 69;

423 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 423 [arrowhead = none ];
423 -> 71;

424 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 424 [arrowhead = none ];
424 -> 72;

425 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 425 [arrowhead = none ];
425 -> 70;

426 [label="EVAL with clause\nmult(s(X235), X236, 0, X237) :- mult(X235, X236, X236, X237).\nand substitution\nX235 -> T161\nT137 -> s(T161)\nT139 -> 0\nX236 -> s(s(0))\nT162 -> 0\nT141 -> T164\nX237 -> T164\nT163 -> T164", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 426 [arrowhead = none ];
426 -> 73;

427 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 427 [arrowhead = none ];
427 -> 74;

428 [label="EVAL with clause\nmult(X346, X347, s(X348), s(X349)) :- mult(X346, X347, X348, X349).\nand substitution\nT137 -> T210\nX346 -> T210\nT139 -> s(T212)\nX347 -> s(s(s(T212)))\nX348 -> T212\nT211 -> s(T212)\nX349 -> T214\nT141 -> s(T214)\nT213 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 428 [arrowhead = none ];
428 -> 96;

429 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 429 [arrowhead = none ];
429 -> 97;

430 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 430 [arrowhead = none ];
430 -> 75;

431 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
75 -> 431 [arrowhead = none ];
431 -> 76;

432 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
76 -> 432 [arrowhead = none ];
432 -> 77;

433 [label="EVAL with clause\nmult(X262, X263, s(X264), s(X265)) :- mult(X262, X263, X264, X265).\nand substitution\nT161 -> T173\nX262 -> T173\nX263 -> s(s(0))\nX264 -> s(0)\nX265 -> T175\nT164 -> s(T175)\nT174 -> T175", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 433 [arrowhead = none ];
433 -> 78;

434 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 434 [arrowhead = none ];
434 -> 79;

435 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 435 [arrowhead = none ];
435 -> 80;

436 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
80 -> 436 [arrowhead = none ];
436 -> 81;

437 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
81 -> 437 [arrowhead = none ];
437 -> 82;

438 [label="EVAL with clause\nmult(X291, X292, s(X293), s(X294)) :- mult(X291, X292, X293, X294).\nand substitution\nT173 -> T184\nX291 -> T184\nX292 -> s(s(0))\nX293 -> 0\nX294 -> T186\nT175 -> s(T186)\nT185 -> T186", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 438 [arrowhead = none ];
438 -> 83;

439 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 439 [arrowhead = none ];
439 -> 84;

440 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 440 [arrowhead = none ];
440 -> 85;

441 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 441 [arrowhead = none ];
441 -> 86;

442 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 442 [arrowhead = none ];
442 -> 87;

443 [label="EVAL with clause\nmult(0, X305, 0, 0).\nand substitution\nT184 -> 0\nX305 -> s(s(0))\nT186 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 443 [arrowhead = none ];
443 -> 88;

444 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 444 [arrowhead = none ];
444 -> 89;

445 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 445 [arrowhead = none ];
445 -> 91;

446 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 446 [arrowhead = none ];
446 -> 92;

447 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 447 [arrowhead = none ];
447 -> 90;

448 [label="EVAL with clause\nmult(s(X319), X320, 0, X321) :- mult(X319, X320, X320, X321).\nand substitution\nX319 -> T195\nT184 -> s(T195)\nX320 -> s(s(0))\nT186 -> T197\nX321 -> T197\nT196 -> T197", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 448 [arrowhead = none ];
448 -> 93;

449 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 449 [arrowhead = none ];
449 -> 94;

450 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
92 -> 450 [arrowhead = none ];
450 -> 95;

451 [label="INSTANCE with matching:\nT161 -> T195\nT164 -> T197", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 451 [arrowhead = none , style=dashed];
451 -> 73[style=dashed];

452 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 452 [arrowhead = none ];
452 -> 98;

453 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 453 [arrowhead = none ];
453 -> 99;

454 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 454 [arrowhead = none ];
454 -> 100;

455 [label="EVAL with clause\nmult(0, X360, 0, 0).\nand substitution\nT210 -> 0\nT212 -> 0\nX360 -> s(s(s(0)))\nT221 -> 0\nT214 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 455 [arrowhead = none ];
455 -> 101;

456 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 456 [arrowhead = none ];
456 -> 102;

457 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 457 [arrowhead = none ];
457 -> 104;

458 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 458 [arrowhead = none ];
458 -> 105;

459 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 459 [arrowhead = none ];
459 -> 103;

460 [label="EVAL with clause\nmult(s(X374), X375, 0, X376) :- mult(X374, X375, X375, X376).\nand substitution\nX374 -> T234\nT210 -> s(T234)\nT212 -> 0\nX375 -> s(s(s(0)))\nT235 -> 0\nT214 -> T237\nX376 -> T237\nT236 -> T237", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 460 [arrowhead = none ];
460 -> 106;

461 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 461 [arrowhead = none ];
461 -> 107;

462 [label="EVAL with clause\nmult(X514, X515, s(X516), s(X517)) :- mult(X514, X515, X516, X517).\nand substitution\nT210 -> T294\nX514 -> T294\nT212 -> s(T296)\nX515 -> s(s(s(s(T296))))\nX516 -> T296\nT295 -> s(T296)\nX517 -> T298\nT214 -> s(T298)\nT297 -> T298", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 462 [arrowhead = none ];
462 -> 134;

463 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 463 [arrowhead = none ];
463 -> 135;

464 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
106 -> 464 [arrowhead = none ];
464 -> 108;

465 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
108 -> 465 [arrowhead = none ];
465 -> 109;

466 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
109 -> 466 [arrowhead = none ];
466 -> 110;

467 [label="EVAL with clause\nmult(X401, X402, s(X403), s(X404)) :- mult(X401, X402, X403, X404).\nand substitution\nT234 -> T246\nX401 -> T246\nX402 -> s(s(s(0)))\nX403 -> s(s(0))\nX404 -> T248\nT237 -> s(T248)\nT247 -> T248", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 467 [arrowhead = none ];
467 -> 111;

468 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 468 [arrowhead = none ];
468 -> 112;

469 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
111 -> 469 [arrowhead = none ];
469 -> 113;

470 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
113 -> 470 [arrowhead = none ];
470 -> 114;

471 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
114 -> 471 [arrowhead = none ];
471 -> 115;

472 [label="EVAL with clause\nmult(X430, X431, s(X432), s(X433)) :- mult(X430, X431, X432, X433).\nand substitution\nT246 -> T257\nX430 -> T257\nX431 -> s(s(s(0)))\nX432 -> s(0)\nX433 -> T259\nT248 -> s(T259)\nT258 -> T259", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 472 [arrowhead = none ];
472 -> 116;

473 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 473 [arrowhead = none ];
473 -> 117;

474 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
116 -> 474 [arrowhead = none ];
474 -> 118;

475 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
118 -> 475 [arrowhead = none ];
475 -> 119;

476 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
119 -> 476 [arrowhead = none ];
476 -> 120;

477 [label="EVAL with clause\nmult(X459, X460, s(X461), s(X462)) :- mult(X459, X460, X461, X462).\nand substitution\nT257 -> T268\nX459 -> T268\nX460 -> s(s(s(0)))\nX461 -> 0\nX462 -> T270\nT259 -> s(T270)\nT269 -> T270", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 477 [arrowhead = none ];
477 -> 121;

478 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 478 [arrowhead = none ];
478 -> 122;

479 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
121 -> 479 [arrowhead = none ];
479 -> 123;

480 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 480 [arrowhead = none ];
480 -> 124;

481 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 481 [arrowhead = none ];
481 -> 125;

482 [label="EVAL with clause\nmult(0, X473, 0, 0).\nand substitution\nT268 -> 0\nX473 -> s(s(s(0)))\nT270 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 482 [arrowhead = none ];
482 -> 126;

483 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 483 [arrowhead = none ];
483 -> 127;

484 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 484 [arrowhead = none ];
484 -> 129;

485 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 485 [arrowhead = none ];
485 -> 130;

486 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 486 [arrowhead = none ];
486 -> 128;

487 [label="EVAL with clause\nmult(s(X487), X488, 0, X489) :- mult(X487, X488, X488, X489).\nand substitution\nX487 -> T279\nT268 -> s(T279)\nX488 -> s(s(s(0)))\nT270 -> T281\nX489 -> T281\nT280 -> T281", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 487 [arrowhead = none ];
487 -> 131;

488 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 488 [arrowhead = none ];
488 -> 132;

489 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
130 -> 489 [arrowhead = none ];
489 -> 133;

490 [label="INSTANCE with matching:\nT234 -> T279\nT237 -> T281", fontsize=14, style = filled, fillcolor = lightgrey];
131 -> 490 [arrowhead = none , style=dashed];
490 -> 106[style=dashed];

491 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
134 -> 491 [arrowhead = none ];
491 -> 136;

492 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
136 -> 492 [arrowhead = none ];
492 -> 137;

493 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
136 -> 493 [arrowhead = none ];
493 -> 138;

494 [label="EVAL with clause\nmult(0, X528, 0, 0).\nand substitution\nT294 -> 0\nT296 -> 0\nX528 -> s(s(s(s(0))))\nT305 -> 0\nT298 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 494 [arrowhead = none ];
494 -> 139;

495 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 495 [arrowhead = none ];
495 -> 140;

496 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 496 [arrowhead = none ];
496 -> 142;

497 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 497 [arrowhead = none ];
497 -> 143;

498 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 498 [arrowhead = none ];
498 -> 141;

499 [label="EVAL with clause\nmult(s(X542), X543, 0, X544) :- mult(X542, X543, X543, X544).\nand substitution\nX542 -> T318\nT294 -> s(T318)\nT296 -> 0\nX543 -> s(s(s(s(0))))\nT319 -> 0\nT298 -> T321\nX544 -> T321\nT320 -> T321", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 499 [arrowhead = none ];
499 -> 144;

500 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 500 [arrowhead = none ];
500 -> 145;

501 [label="EVAL with clause\nmult(X711, X712, s(X713), s(X714)) :- mult(X711, X712, X713, X714).\nand substitution\nT294 -> T389\nX711 -> T389\nT296 -> s(T391)\nX712 -> s(s(s(s(s(T391)))))\nX713 -> T391\nT390 -> s(T391)\nX714 -> T393\nT298 -> s(T393)\nT392 -> T393", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 501 [arrowhead = none ];
501 -> 177;

502 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 502 [arrowhead = none ];
502 -> 178;

503 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 503 [arrowhead = none ];
503 -> 146;

504 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
146 -> 504 [arrowhead = none ];
504 -> 147;

505 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
147 -> 505 [arrowhead = none ];
505 -> 148;

506 [label="EVAL with clause\nmult(X569, X570, s(X571), s(X572)) :- mult(X569, X570, X571, X572).\nand substitution\nT318 -> T330\nX569 -> T330\nX570 -> s(s(s(s(0))))\nX571 -> s(s(s(0)))\nX572 -> T332\nT321 -> s(T332)\nT331 -> T332", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 506 [arrowhead = none ];
506 -> 149;

507 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 507 [arrowhead = none ];
507 -> 150;

508 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
149 -> 508 [arrowhead = none ];
508 -> 151;

509 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
151 -> 509 [arrowhead = none ];
509 -> 152;

510 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
152 -> 510 [arrowhead = none ];
510 -> 153;

511 [label="EVAL with clause\nmult(X598, X599, s(X600), s(X601)) :- mult(X598, X599, X600, X601).\nand substitution\nT330 -> T341\nX598 -> T341\nX599 -> s(s(s(s(0))))\nX600 -> s(s(0))\nX601 -> T343\nT332 -> s(T343)\nT342 -> T343", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 511 [arrowhead = none ];
511 -> 154;

512 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 512 [arrowhead = none ];
512 -> 155;

513 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
154 -> 513 [arrowhead = none ];
513 -> 156;

514 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
156 -> 514 [arrowhead = none ];
514 -> 157;

515 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
157 -> 515 [arrowhead = none ];
515 -> 158;

516 [label="EVAL with clause\nmult(X627, X628, s(X629), s(X630)) :- mult(X627, X628, X629, X630).\nand substitution\nT341 -> T352\nX627 -> T352\nX628 -> s(s(s(s(0))))\nX629 -> s(0)\nX630 -> T354\nT343 -> s(T354)\nT353 -> T354", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 516 [arrowhead = none ];
516 -> 159;

517 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 517 [arrowhead = none ];
517 -> 160;

518 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
159 -> 518 [arrowhead = none ];
518 -> 161;

519 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
161 -> 519 [arrowhead = none ];
519 -> 162;

520 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
162 -> 520 [arrowhead = none ];
520 -> 163;

521 [label="EVAL with clause\nmult(X656, X657, s(X658), s(X659)) :- mult(X656, X657, X658, X659).\nand substitution\nT352 -> T363\nX656 -> T363\nX657 -> s(s(s(s(0))))\nX658 -> 0\nX659 -> T365\nT354 -> s(T365)\nT364 -> T365", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 521 [arrowhead = none ];
521 -> 164;

522 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 522 [arrowhead = none ];
522 -> 165;

523 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
164 -> 523 [arrowhead = none ];
523 -> 166;

524 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
166 -> 524 [arrowhead = none ];
524 -> 167;

525 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
166 -> 525 [arrowhead = none ];
525 -> 168;

526 [label="EVAL with clause\nmult(0, X670, 0, 0).\nand substitution\nT363 -> 0\nX670 -> s(s(s(s(0))))\nT365 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 526 [arrowhead = none ];
526 -> 169;

527 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 527 [arrowhead = none ];
527 -> 170;

528 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
168 -> 528 [arrowhead = none ];
528 -> 172;

529 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
168 -> 529 [arrowhead = none ];
529 -> 173;

530 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 530 [arrowhead = none ];
530 -> 171;

531 [label="EVAL with clause\nmult(s(X684), X685, 0, X686) :- mult(X684, X685, X685, X686).\nand substitution\nX684 -> T374\nT363 -> s(T374)\nX685 -> s(s(s(s(0))))\nT365 -> T376\nX686 -> T376\nT375 -> T376", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 531 [arrowhead = none ];
531 -> 174;

532 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 532 [arrowhead = none ];
532 -> 175;

533 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
173 -> 533 [arrowhead = none ];
533 -> 176;

534 [label="INSTANCE with matching:\nT318 -> T374\nT321 -> T376", fontsize=14, style = filled, fillcolor = lightgrey];
174 -> 534 [arrowhead = none , style=dashed];
534 -> 144[style=dashed];

535 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
177 -> 535 [arrowhead = none ];
535 -> 179;

536 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 536 [arrowhead = none ];
536 -> 180;

537 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 537 [arrowhead = none ];
537 -> 181;

538 [label="EVAL with clause\nmult(0, X725, 0, 0).\nand substitution\nT389 -> 0\nT391 -> 0\nX725 -> s(s(s(s(s(0)))))\nT400 -> 0\nT393 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 538 [arrowhead = none ];
538 -> 182;

539 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 539 [arrowhead = none ];
539 -> 183;

540 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
181 -> 540 [arrowhead = none ];
540 -> 185;

541 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
181 -> 541 [arrowhead = none ];
541 -> 186;

542 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 542 [arrowhead = none ];
542 -> 184;

543 [label="EVAL with clause\nmult(s(X739), X740, 0, X741) :- mult(X739, X740, X740, X741).\nand substitution\nX739 -> T413\nT389 -> s(T413)\nT391 -> 0\nX740 -> s(s(s(s(s(0)))))\nT414 -> 0\nT393 -> T416\nX741 -> T416\nT415 -> T416", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 543 [arrowhead = none ];
543 -> 187;

544 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 544 [arrowhead = none ];
544 -> 188;

545 [label="EVAL with clause\nmult(X937, X938, s(X939), s(X940)) :- mult(X937, X938, X939, X940).\nand substitution\nT389 -> T495\nX937 -> T495\nT391 -> s(T497)\nX938 -> s(s(s(s(s(s(T497))))))\nX939 -> T497\nT496 -> s(T497)\nX940 -> T499\nT393 -> s(T499)\nT498 -> T499", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 545 [arrowhead = none ];
545 -> 225;

546 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 546 [arrowhead = none ];
546 -> 226;

547 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
187 -> 547 [arrowhead = none ];
547 -> 189;

548 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
189 -> 548 [arrowhead = none ];
548 -> 190;

549 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
190 -> 549 [arrowhead = none ];
549 -> 191;

550 [label="EVAL with clause\nmult(X766, X767, s(X768), s(X769)) :- mult(X766, X767, X768, X769).\nand substitution\nT413 -> T425\nX766 -> T425\nX767 -> s(s(s(s(s(0)))))\nX768 -> s(s(s(s(0))))\nX769 -> T427\nT416 -> s(T427)\nT426 -> T427", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 550 [arrowhead = none ];
550 -> 192;

551 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 551 [arrowhead = none ];
551 -> 193;

552 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
192 -> 552 [arrowhead = none ];
552 -> 194;

553 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
194 -> 553 [arrowhead = none ];
553 -> 195;

554 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
195 -> 554 [arrowhead = none ];
554 -> 196;

555 [label="EVAL with clause\nmult(X795, X796, s(X797), s(X798)) :- mult(X795, X796, X797, X798).\nand substitution\nT425 -> T436\nX795 -> T436\nX796 -> s(s(s(s(s(0)))))\nX797 -> s(s(s(0)))\nX798 -> T438\nT427 -> s(T438)\nT437 -> T438", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 555 [arrowhead = none ];
555 -> 197;

556 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 556 [arrowhead = none ];
556 -> 198;

557 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
197 -> 557 [arrowhead = none ];
557 -> 199;

558 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
199 -> 558 [arrowhead = none ];
558 -> 200;

559 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
200 -> 559 [arrowhead = none ];
559 -> 201;

560 [label="EVAL with clause\nmult(X824, X825, s(X826), s(X827)) :- mult(X824, X825, X826, X827).\nand substitution\nT436 -> T447\nX824 -> T447\nX825 -> s(s(s(s(s(0)))))\nX826 -> s(s(0))\nX827 -> T449\nT438 -> s(T449)\nT448 -> T449", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 560 [arrowhead = none ];
560 -> 202;

561 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 561 [arrowhead = none ];
561 -> 203;

562 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
202 -> 562 [arrowhead = none ];
562 -> 204;

563 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
204 -> 563 [arrowhead = none ];
563 -> 205;

564 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
205 -> 564 [arrowhead = none ];
564 -> 206;

565 [label="EVAL with clause\nmult(X853, X854, s(X855), s(X856)) :- mult(X853, X854, X855, X856).\nand substitution\nT447 -> T458\nX853 -> T458\nX854 -> s(s(s(s(s(0)))))\nX855 -> s(0)\nX856 -> T460\nT449 -> s(T460)\nT459 -> T460", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 565 [arrowhead = none ];
565 -> 207;

566 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 566 [arrowhead = none ];
566 -> 208;

567 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
207 -> 567 [arrowhead = none ];
567 -> 209;

568 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
209 -> 568 [arrowhead = none ];
568 -> 210;

569 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
210 -> 569 [arrowhead = none ];
569 -> 211;

570 [label="EVAL with clause\nmult(X882, X883, s(X884), s(X885)) :- mult(X882, X883, X884, X885).\nand substitution\nT458 -> T469\nX882 -> T469\nX883 -> s(s(s(s(s(0)))))\nX884 -> 0\nX885 -> T471\nT460 -> s(T471)\nT470 -> T471", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 570 [arrowhead = none ];
570 -> 212;

571 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 571 [arrowhead = none ];
571 -> 213;

572 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
212 -> 572 [arrowhead = none ];
572 -> 214;

573 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
214 -> 573 [arrowhead = none ];
573 -> 215;

574 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
214 -> 574 [arrowhead = none ];
574 -> 216;

575 [label="EVAL with clause\nmult(0, X896, 0, 0).\nand substitution\nT469 -> 0\nX896 -> s(s(s(s(s(0)))))\nT471 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 575 [arrowhead = none ];
575 -> 217;

576 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 576 [arrowhead = none ];
576 -> 218;

577 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
216 -> 577 [arrowhead = none ];
577 -> 220;

578 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
216 -> 578 [arrowhead = none ];
578 -> 221;

579 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 579 [arrowhead = none ];
579 -> 219;

580 [label="EVAL with clause\nmult(s(X910), X911, 0, X912) :- mult(X910, X911, X911, X912).\nand substitution\nX910 -> T480\nT469 -> s(T480)\nX911 -> s(s(s(s(s(0)))))\nT471 -> T482\nX912 -> T482\nT481 -> T482", fontsize=14, style = filled, fillcolor = lightblue];
220 -> 580 [arrowhead = none ];
580 -> 222;

581 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
220 -> 581 [arrowhead = none ];
581 -> 223;

582 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
221 -> 582 [arrowhead = none ];
582 -> 224;

583 [label="INSTANCE with matching:\nT413 -> T480\nT416 -> T482", fontsize=14, style = filled, fillcolor = lightgrey];
222 -> 583 [arrowhead = none , style=dashed];
583 -> 187[style=dashed];

584 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
225 -> 584 [arrowhead = none ];
584 -> 227;

585 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 585 [arrowhead = none ];
585 -> 228;

586 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 586 [arrowhead = none ];
586 -> 229;

587 [label="EVAL with clause\nmult(0, X951, 0, 0).\nand substitution\nT495 -> 0\nT497 -> 0\nX951 -> s(s(s(s(s(s(0))))))\nT506 -> 0\nT499 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 587 [arrowhead = none ];
587 -> 230;

588 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 588 [arrowhead = none ];
588 -> 231;

589 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
229 -> 589 [arrowhead = none ];
589 -> 233;

590 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
229 -> 590 [arrowhead = none ];
590 -> 234;

591 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
230 -> 591 [arrowhead = none ];
591 -> 232;

592 [label="EVAL with clause\nmult(s(X965), X966, 0, X967) :- mult(X965, X966, X966, X967).\nand substitution\nX965 -> T519\nT495 -> s(T519)\nT497 -> 0\nX966 -> s(s(s(s(s(s(0))))))\nT520 -> 0\nT499 -> T522\nX967 -> T522\nT521 -> T522", fontsize=14, style = filled, fillcolor = lightblue];
233 -> 592 [arrowhead = none ];
592 -> 235;

593 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
233 -> 593 [arrowhead = none ];
593 -> 236;

594 [label="EVAL with clause\nmult(X1192, X1193, s(X1194), s(X1195)) :- mult(X1192, X1193, X1194, X1195).\nand substitution\nT495 -> T612\nX1192 -> T612\nT497 -> s(T614)\nX1193 -> s(s(s(s(s(s(s(T614)))))))\nX1194 -> T614\nT613 -> s(T614)\nX1195 -> T616\nT499 -> s(T616)\nT615 -> T616", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 594 [arrowhead = none ];
594 -> 278;

595 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 595 [arrowhead = none ];
595 -> 279;

596 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
235 -> 596 [arrowhead = none ];
596 -> 237;

597 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
237 -> 597 [arrowhead = none ];
597 -> 238;

598 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
238 -> 598 [arrowhead = none ];
598 -> 239;

599 [label="EVAL with clause\nmult(X992, X993, s(X994), s(X995)) :- mult(X992, X993, X994, X995).\nand substitution\nT519 -> T531\nX992 -> T531\nX993 -> s(s(s(s(s(s(0))))))\nX994 -> s(s(s(s(s(0)))))\nX995 -> T533\nT522 -> s(T533)\nT532 -> T533", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 599 [arrowhead = none ];
599 -> 240;

600 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 600 [arrowhead = none ];
600 -> 241;

601 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
240 -> 601 [arrowhead = none ];
601 -> 242;

602 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
242 -> 602 [arrowhead = none ];
602 -> 243;

603 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
243 -> 603 [arrowhead = none ];
603 -> 244;

604 [label="EVAL with clause\nmult(X1021, X1022, s(X1023), s(X1024)) :- mult(X1021, X1022, X1023, X1024).\nand substitution\nT531 -> T542\nX1021 -> T542\nX1022 -> s(s(s(s(s(s(0))))))\nX1023 -> s(s(s(s(0))))\nX1024 -> T544\nT533 -> s(T544)\nT543 -> T544", fontsize=14, style = filled, fillcolor = lightblue];
244 -> 604 [arrowhead = none ];
604 -> 245;

605 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
244 -> 605 [arrowhead = none ];
605 -> 246;

606 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
245 -> 606 [arrowhead = none ];
606 -> 247;

607 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
247 -> 607 [arrowhead = none ];
607 -> 248;

608 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
248 -> 608 [arrowhead = none ];
608 -> 249;

609 [label="EVAL with clause\nmult(X1050, X1051, s(X1052), s(X1053)) :- mult(X1050, X1051, X1052, X1053).\nand substitution\nT542 -> T553\nX1050 -> T553\nX1051 -> s(s(s(s(s(s(0))))))\nX1052 -> s(s(s(0)))\nX1053 -> T555\nT544 -> s(T555)\nT554 -> T555", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 609 [arrowhead = none ];
609 -> 250;

610 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 610 [arrowhead = none ];
610 -> 251;

611 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
250 -> 611 [arrowhead = none ];
611 -> 252;

612 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
252 -> 612 [arrowhead = none ];
612 -> 253;

613 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
253 -> 613 [arrowhead = none ];
613 -> 254;

614 [label="EVAL with clause\nmult(X1079, X1080, s(X1081), s(X1082)) :- mult(X1079, X1080, X1081, X1082).\nand substitution\nT553 -> T564\nX1079 -> T564\nX1080 -> s(s(s(s(s(s(0))))))\nX1081 -> s(s(0))\nX1082 -> T566\nT555 -> s(T566)\nT565 -> T566", fontsize=14, style = filled, fillcolor = lightblue];
254 -> 614 [arrowhead = none ];
614 -> 255;

615 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
254 -> 615 [arrowhead = none ];
615 -> 256;

616 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
255 -> 616 [arrowhead = none ];
616 -> 257;

617 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
257 -> 617 [arrowhead = none ];
617 -> 258;

618 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
258 -> 618 [arrowhead = none ];
618 -> 259;

619 [label="EVAL with clause\nmult(X1108, X1109, s(X1110), s(X1111)) :- mult(X1108, X1109, X1110, X1111).\nand substitution\nT564 -> T575\nX1108 -> T575\nX1109 -> s(s(s(s(s(s(0))))))\nX1110 -> s(0)\nX1111 -> T577\nT566 -> s(T577)\nT576 -> T577", fontsize=14, style = filled, fillcolor = lightblue];
259 -> 619 [arrowhead = none ];
619 -> 260;

620 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
259 -> 620 [arrowhead = none ];
620 -> 261;

621 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
260 -> 621 [arrowhead = none ];
621 -> 262;

622 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
262 -> 622 [arrowhead = none ];
622 -> 263;

623 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
263 -> 623 [arrowhead = none ];
623 -> 264;

624 [label="EVAL with clause\nmult(X1137, X1138, s(X1139), s(X1140)) :- mult(X1137, X1138, X1139, X1140).\nand substitution\nT575 -> T586\nX1137 -> T586\nX1138 -> s(s(s(s(s(s(0))))))\nX1139 -> 0\nX1140 -> T588\nT577 -> s(T588)\nT587 -> T588", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 624 [arrowhead = none ];
624 -> 265;

625 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 625 [arrowhead = none ];
625 -> 266;

626 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
265 -> 626 [arrowhead = none ];
626 -> 267;

627 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
267 -> 627 [arrowhead = none ];
627 -> 268;

628 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
267 -> 628 [arrowhead = none ];
628 -> 269;

629 [label="EVAL with clause\nmult(0, X1151, 0, 0).\nand substitution\nT586 -> 0\nX1151 -> s(s(s(s(s(s(0))))))\nT588 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
268 -> 629 [arrowhead = none ];
629 -> 270;

630 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
268 -> 630 [arrowhead = none ];
630 -> 271;

631 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
269 -> 631 [arrowhead = none ];
631 -> 273;

632 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
269 -> 632 [arrowhead = none ];
632 -> 274;

633 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
270 -> 633 [arrowhead = none ];
633 -> 272;

634 [label="EVAL with clause\nmult(s(X1165), X1166, 0, X1167) :- mult(X1165, X1166, X1166, X1167).\nand substitution\nX1165 -> T597\nT586 -> s(T597)\nX1166 -> s(s(s(s(s(s(0))))))\nT588 -> T599\nX1167 -> T599\nT598 -> T599", fontsize=14, style = filled, fillcolor = lightblue];
273 -> 634 [arrowhead = none ];
634 -> 275;

635 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
273 -> 635 [arrowhead = none ];
635 -> 276;

636 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
274 -> 636 [arrowhead = none ];
636 -> 277;

637 [label="INSTANCE with matching:\nT519 -> T597\nT522 -> T599", fontsize=14, style = filled, fillcolor = lightgrey];
275 -> 637 [arrowhead = none , style=dashed];
637 -> 235[style=dashed];

638 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
278 -> 638 [arrowhead = none ];
638 -> 280;

639 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 639 [arrowhead = none ];
639 -> 281;

640 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 640 [arrowhead = none ];
640 -> 282;

641 [label="EVAL with clause\nmult(0, X1206, 0, 0).\nand substitution\nT612 -> 0\nT614 -> 0\nX1206 -> s(s(s(s(s(s(s(0)))))))\nT623 -> 0\nT616 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
281 -> 641 [arrowhead = none ];
641 -> 283;

642 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
281 -> 642 [arrowhead = none ];
642 -> 284;

643 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
282 -> 643 [arrowhead = none ];
643 -> 286;

644 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
282 -> 644 [arrowhead = none ];
644 -> 287;

645 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
283 -> 645 [arrowhead = none ];
645 -> 285;

646 [label="EVAL with clause\nmult(s(X1220), X1221, 0, X1222) :- mult(X1220, X1221, X1221, X1222).\nand substitution\nX1220 -> T636\nT612 -> s(T636)\nT614 -> 0\nX1221 -> s(s(s(s(s(s(s(0)))))))\nT637 -> 0\nT616 -> T639\nX1222 -> T639\nT638 -> T639", fontsize=14, style = filled, fillcolor = lightblue];
286 -> 646 [arrowhead = none ];
646 -> 288;

647 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
286 -> 647 [arrowhead = none ];
647 -> 289;

648 [label="EVAL with clause\nmult(X1476, X1477, s(X1478), s(X1479)) :- mult(X1476, X1477, X1478, X1479).\nand substitution\nT612 -> T740\nX1476 -> T740\nT614 -> s(T742)\nX1477 -> s(s(s(s(s(s(s(s(T742))))))))\nX1478 -> T742\nT741 -> s(T742)\nX1479 -> T744\nT616 -> s(T744)\nT743 -> T744", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 648 [arrowhead = none ];
648 -> 336;

649 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 649 [arrowhead = none ];
649 -> 337;

650 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
288 -> 650 [arrowhead = none ];
650 -> 290;

651 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
290 -> 651 [arrowhead = none ];
651 -> 291;

652 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
291 -> 652 [arrowhead = none ];
652 -> 292;

653 [label="EVAL with clause\nmult(X1247, X1248, s(X1249), s(X1250)) :- mult(X1247, X1248, X1249, X1250).\nand substitution\nT636 -> T648\nX1247 -> T648\nX1248 -> s(s(s(s(s(s(s(0)))))))\nX1249 -> s(s(s(s(s(s(0))))))\nX1250 -> T650\nT639 -> s(T650)\nT649 -> T650", fontsize=14, style = filled, fillcolor = lightblue];
292 -> 653 [arrowhead = none ];
653 -> 293;

654 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
292 -> 654 [arrowhead = none ];
654 -> 294;

655 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
293 -> 655 [arrowhead = none ];
655 -> 295;

656 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
295 -> 656 [arrowhead = none ];
656 -> 296;

657 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
296 -> 657 [arrowhead = none ];
657 -> 297;

658 [label="EVAL with clause\nmult(X1276, X1277, s(X1278), s(X1279)) :- mult(X1276, X1277, X1278, X1279).\nand substitution\nT648 -> T659\nX1276 -> T659\nX1277 -> s(s(s(s(s(s(s(0)))))))\nX1278 -> s(s(s(s(s(0)))))\nX1279 -> T661\nT650 -> s(T661)\nT660 -> T661", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 658 [arrowhead = none ];
658 -> 298;

659 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 659 [arrowhead = none ];
659 -> 299;

660 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
298 -> 660 [arrowhead = none ];
660 -> 300;

661 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
300 -> 661 [arrowhead = none ];
661 -> 301;

662 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
301 -> 662 [arrowhead = none ];
662 -> 302;

663 [label="EVAL with clause\nmult(X1305, X1306, s(X1307), s(X1308)) :- mult(X1305, X1306, X1307, X1308).\nand substitution\nT659 -> T670\nX1305 -> T670\nX1306 -> s(s(s(s(s(s(s(0)))))))\nX1307 -> s(s(s(s(0))))\nX1308 -> T672\nT661 -> s(T672)\nT671 -> T672", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 663 [arrowhead = none ];
663 -> 303;

664 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 664 [arrowhead = none ];
664 -> 304;

665 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
303 -> 665 [arrowhead = none ];
665 -> 305;

666 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
305 -> 666 [arrowhead = none ];
666 -> 306;

667 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
306 -> 667 [arrowhead = none ];
667 -> 307;

668 [label="EVAL with clause\nmult(X1334, X1335, s(X1336), s(X1337)) :- mult(X1334, X1335, X1336, X1337).\nand substitution\nT670 -> T681\nX1334 -> T681\nX1335 -> s(s(s(s(s(s(s(0)))))))\nX1336 -> s(s(s(0)))\nX1337 -> T683\nT672 -> s(T683)\nT682 -> T683", fontsize=14, style = filled, fillcolor = lightblue];
307 -> 668 [arrowhead = none ];
668 -> 308;

669 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
307 -> 669 [arrowhead = none ];
669 -> 309;

670 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
308 -> 670 [arrowhead = none ];
670 -> 310;

671 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
310 -> 671 [arrowhead = none ];
671 -> 311;

672 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
311 -> 672 [arrowhead = none ];
672 -> 312;

673 [label="EVAL with clause\nmult(X1363, X1364, s(X1365), s(X1366)) :- mult(X1363, X1364, X1365, X1366).\nand substitution\nT681 -> T692\nX1363 -> T692\nX1364 -> s(s(s(s(s(s(s(0)))))))\nX1365 -> s(s(0))\nX1366 -> T694\nT683 -> s(T694)\nT693 -> T694", fontsize=14, style = filled, fillcolor = lightblue];
312 -> 673 [arrowhead = none ];
673 -> 313;

674 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
312 -> 674 [arrowhead = none ];
674 -> 314;

675 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
313 -> 675 [arrowhead = none ];
675 -> 315;

676 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
315 -> 676 [arrowhead = none ];
676 -> 316;

677 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
316 -> 677 [arrowhead = none ];
677 -> 317;

678 [label="EVAL with clause\nmult(X1392, X1393, s(X1394), s(X1395)) :- mult(X1392, X1393, X1394, X1395).\nand substitution\nT692 -> T703\nX1392 -> T703\nX1393 -> s(s(s(s(s(s(s(0)))))))\nX1394 -> s(0)\nX1395 -> T705\nT694 -> s(T705)\nT704 -> T705", fontsize=14, style = filled, fillcolor = lightblue];
317 -> 678 [arrowhead = none ];
678 -> 318;

679 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
317 -> 679 [arrowhead = none ];
679 -> 319;

680 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
318 -> 680 [arrowhead = none ];
680 -> 320;

681 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
320 -> 681 [arrowhead = none ];
681 -> 321;

682 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
321 -> 682 [arrowhead = none ];
682 -> 322;

683 [label="EVAL with clause\nmult(X1421, X1422, s(X1423), s(X1424)) :- mult(X1421, X1422, X1423, X1424).\nand substitution\nT703 -> T714\nX1421 -> T714\nX1422 -> s(s(s(s(s(s(s(0)))))))\nX1423 -> 0\nX1424 -> T716\nT705 -> s(T716)\nT715 -> T716", fontsize=14, style = filled, fillcolor = lightblue];
322 -> 683 [arrowhead = none ];
683 -> 323;

684 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
322 -> 684 [arrowhead = none ];
684 -> 324;

685 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
323 -> 685 [arrowhead = none ];
685 -> 325;

686 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
325 -> 686 [arrowhead = none ];
686 -> 326;

687 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
325 -> 687 [arrowhead = none ];
687 -> 327;

688 [label="EVAL with clause\nmult(0, X1435, 0, 0).\nand substitution\nT714 -> 0\nX1435 -> s(s(s(s(s(s(s(0)))))))\nT716 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
326 -> 688 [arrowhead = none ];
688 -> 328;

689 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
326 -> 689 [arrowhead = none ];
689 -> 329;

690 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
327 -> 690 [arrowhead = none ];
690 -> 331;

691 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
327 -> 691 [arrowhead = none ];
691 -> 332;

692 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
328 -> 692 [arrowhead = none ];
692 -> 330;

693 [label="EVAL with clause\nmult(s(X1449), X1450, 0, X1451) :- mult(X1449, X1450, X1450, X1451).\nand substitution\nX1449 -> T725\nT714 -> s(T725)\nX1450 -> s(s(s(s(s(s(s(0)))))))\nT716 -> T727\nX1451 -> T727\nT726 -> T727", fontsize=14, style = filled, fillcolor = lightblue];
331 -> 693 [arrowhead = none ];
693 -> 333;

694 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
331 -> 694 [arrowhead = none ];
694 -> 334;

695 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = white];
332 -> 695 [arrowhead = none ];
695 -> 335;

696 [label="INSTANCE with matching:\nT636 -> T725\nT639 -> T727", fontsize=14, style = filled, fillcolor = lightgrey];
333 -> 696 [arrowhead = none , style=dashed];
696 -> 288[style=dashed];

697 [label="GENERALIZATION\nT747 <-- s(s(s(s(s(s(s(T742)))))))\n\nNew Knowledge:\nT747 is ground", fontsize=14, style = filled, fillcolor = violet];
336 -> 697 [arrowhead = none ];
697 -> 338;

698 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
338 -> 698 [arrowhead = none ];
698 -> 339;

699 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
339 -> 699 [arrowhead = none ];
699 -> 340;

700 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
339 -> 700 [arrowhead = none ];
700 -> 341;

701 [label="EVAL with clause\nmult(0, X1492, 0, 0).\nand substitution\nT740 -> 0\nT747 -> T754\nX1492 -> s(T754)\nT742 -> 0\nT744 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
340 -> 701 [arrowhead = none ];
701 -> 342;

702 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
340 -> 702 [arrowhead = none ];
702 -> 343;

703 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
341 -> 703 [arrowhead = none ];
703 -> 345;

704 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
341 -> 704 [arrowhead = none ];
704 -> 346;

705 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
342 -> 705 [arrowhead = none ];
705 -> 344;

706 [label="EVAL with clause\nmult(s(X1506), X1507, 0, X1508) :- mult(X1506, X1507, X1507, X1508).\nand substitution\nX1506 -> T767\nT740 -> s(T767)\nT747 -> T768\nX1507 -> s(T768)\nT742 -> 0\nT744 -> T770\nX1508 -> T770\nT769 -> T770", fontsize=14, style = filled, fillcolor = lightblue];
345 -> 706 [arrowhead = none ];
706 -> 347;

707 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
345 -> 707 [arrowhead = none ];
707 -> 348;

708 [label="EVAL with clause\nmult(X1529, X1530, s(X1531), s(X1532)) :- mult(X1529, X1530, X1531, X1532).\nand substitution\nT740 -> T786\nX1529 -> T786\nT747 -> T787\nX1530 -> s(T787)\nX1531 -> T788\nT742 -> s(T788)\nX1532 -> T790\nT744 -> s(T790)\nT789 -> T790", fontsize=14, style = filled, fillcolor = lightblue];
346 -> 708 [arrowhead = none ];
708 -> 349;

709 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
346 -> 709 [arrowhead = none ];
709 -> 350;

710 [label="INSTANCE with matching:\nT28 -> T767\nT29 -> s(T768)\nT31 -> T770", fontsize=14, style = filled, fillcolor = lightgrey];
347 -> 710 [arrowhead = none , style=dashed];
710 -> 12[style=dashed];

711 [label="INSTANCE with matching:\nT740 -> T786\nT747 -> T787\nT742 -> T788\nT744 -> T790", fontsize=14, style = filled, fillcolor = lightgrey];
349 -> 711 [arrowhead = none , style=dashed];
711 -> 338[style=dashed];

}

(2) Obligation:

Triples:

mult22(s(T63), T65) :- mult22(T63, T65).
mult45(s(T122), s(T124)) :- mult45(T122, T124).
mult73(s(T195), s(s(T197))) :- mult73(T195, T197).
mult106(s(T279), s(s(s(T281)))) :- mult106(T279, T281).
mult144(s(T374), s(s(s(s(T376))))) :- mult144(T374, T376).
mult187(s(T480), s(s(s(s(s(T482)))))) :- mult187(T480, T482).
mult235(s(T597), s(s(s(s(s(s(T599))))))) :- mult235(T597, T599).
mult288(s(T725), s(s(s(s(s(s(s(T727)))))))) :- mult288(T725, T727).
mult12(s(T51), 0, T54) :- mult22(T51, T54).
mult12(s(T99), s(0), s(T102)) :- mult45(T99, T102).
mult12(s(T161), s(s(0)), s(s(T164))) :- mult73(T161, T164).
mult12(s(T234), s(s(s(0))), s(s(s(T237)))) :- mult106(T234, T237).
mult12(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) :- mult144(T318, T321).
mult12(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) :- mult187(T413, T416).
mult12(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) :- mult235(T519, T522).
mult12(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) :- mult288(T636, T639).
mult12(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) :- mult338(T740, s(s(s(s(s(s(s(T742))))))), T742, T744).
mult338(s(T767), T768, 0, T770) :- mult12(T767, s(T768), T770).
mult338(T786, T787, s(T788), s(T790)) :- mult338(T786, T787, T788, T790).
times1(s(T28), T29, T31) :- mult12(T28, T29, T31).

Clauses:

multc22(0, 0).
multc22(s(T63), T65) :- multc22(T63, T65).
multc45(0, s(0)).
multc45(s(T122), s(T124)) :- multc45(T122, T124).
multc73(0, s(s(0))).
multc73(s(T195), s(s(T197))) :- multc73(T195, T197).
multc106(0, s(s(s(0)))).
multc106(s(T279), s(s(s(T281)))) :- multc106(T279, T281).
multc144(0, s(s(s(s(0))))).
multc144(s(T374), s(s(s(s(T376))))) :- multc144(T374, T376).
multc187(0, s(s(s(s(s(0)))))).
multc187(s(T480), s(s(s(s(s(T482)))))) :- multc187(T480, T482).
multc235(0, s(s(s(s(s(s(0))))))).
multc235(s(T597), s(s(s(s(s(s(T599))))))) :- multc235(T597, T599).
multc288(0, s(s(s(s(s(s(s(0)))))))).
multc288(s(T725), s(s(s(s(s(s(s(T727)))))))) :- multc288(T725, T727).
multc12(0, 0, 0).
multc12(s(T51), 0, T54) :- multc22(T51, T54).
multc12(0, s(0), s(0)).
multc12(s(T99), s(0), s(T102)) :- multc45(T99, T102).
multc12(0, s(s(0)), s(s(0))).
multc12(s(T161), s(s(0)), s(s(T164))) :- multc73(T161, T164).
multc12(0, s(s(s(0))), s(s(s(0)))).
multc12(s(T234), s(s(s(0))), s(s(s(T237)))) :- multc106(T234, T237).
multc12(0, s(s(s(s(0)))), s(s(s(s(0))))).
multc12(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) :- multc144(T318, T321).
multc12(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))).
multc12(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) :- multc187(T413, T416).
multc12(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))).
multc12(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) :- multc235(T519, T522).
multc12(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))).
multc12(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) :- multc288(T636, T639).
multc12(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) :- multc338(T740, s(s(s(s(s(s(s(T742))))))), T742, T744).
multc338(0, T754, 0, 0).
multc338(s(T767), T768, 0, T770) :- multc12(T767, s(T768), T770).
multc338(T786, T787, s(T788), s(T790)) :- multc338(T786, T787, T788, T790).

Afs:

times1(x1, x2, x3) = times1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
times1_in: (b,b,f)
mult12_in: (b,b,f)
mult22_in: (b,f)
mult45_in: (b,f)
mult73_in: (b,f)
mult106_in: (b,f)
mult144_in: (b,f)
mult187_in: (b,f)
mult235_in: (b,f)
mult288_in: (b,f)
mult338_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TIMES1_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, mult12_in_gga(T28, T29, T31))
TIMES1_IN_GGA(s(T28), T29, T31) → MULT12_IN_GGA(T28, T29, T31)
MULT12_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, mult22_in_ga(T51, T54))
MULT12_IN_GGA(s(T51), 0, T54) → MULT22_IN_GA(T51, T54)
MULT22_IN_GA(s(T63), T65) → U1_GA(T63, T65, mult22_in_ga(T63, T65))
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT12_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, mult45_in_ga(T99, T102))
MULT12_IN_GGA(s(T99), s(0), s(T102)) → MULT45_IN_GA(T99, T102)
MULT45_IN_GA(s(T122), s(T124)) → U2_GA(T122, T124, mult45_in_ga(T122, T124))
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → U11_GGA(T161, T164, mult73_in_ga(T161, T164))
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → MULT73_IN_GA(T161, T164)
MULT73_IN_GA(s(T195), s(s(T197))) → U3_GA(T195, T197, mult73_in_ga(T195, T197))
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_GGA(T234, T237, mult106_in_ga(T234, T237))
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → MULT106_IN_GA(T234, T237)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → U4_GA(T279, T281, mult106_in_ga(T279, T281))
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_GGA(T318, T321, mult144_in_ga(T318, T321))
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → MULT144_IN_GA(T318, T321)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → U5_GA(T374, T376, mult144_in_ga(T374, T376))
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_GGA(T413, T416, mult187_in_ga(T413, T416))
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → MULT187_IN_GA(T413, T416)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → U6_GA(T480, T482, mult187_in_ga(T480, T482))
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_GGA(T519, T522, mult235_in_ga(T519, T522))
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → MULT235_IN_GA(T519, T522)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → U7_GA(T597, T599, mult235_in_ga(T597, T599))
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_GGA(T636, T639, mult288_in_ga(T636, T639))
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → MULT288_IN_GA(T636, T639)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_GA(T725, T727, mult288_in_ga(T725, T727))
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_GGA(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → U18_GGGA(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → U19_GGGA(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
mult12_in_gga(x1, x2, x3) = mult12_in_gga(x1, x2)
0 = 0
mult22_in_ga(x1, x2) = mult22_in_ga(x1)
mult45_in_ga(x1, x2) = mult45_in_ga(x1)
mult73_in_ga(x1, x2) = mult73_in_ga(x1)
mult106_in_ga(x1, x2) = mult106_in_ga(x1)
mult144_in_ga(x1, x2) = mult144_in_ga(x1)
mult187_in_ga(x1, x2) = mult187_in_ga(x1)
mult235_in_ga(x1, x2) = mult235_in_ga(x1)
mult288_in_ga(x1, x2) = mult288_in_ga(x1)
mult338_in_ggga(x1, x2, x3, x4) = mult338_in_ggga(x1, x2, x3)
TIMES1_IN_GGA(x1, x2, x3) = TIMES1_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x1, x2, x4)
MULT12_IN_GGA(x1, x2, x3) = MULT12_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3) = U9_GGA(x1, x3)
MULT22_IN_GA(x1, x2) = MULT22_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U10_GGA(x1, x2, x3) = U10_GGA(x1, x3)
MULT45_IN_GA(x1, x2) = MULT45_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
U11_GGA(x1, x2, x3) = U11_GGA(x1, x3)
MULT73_IN_GA(x1, x2) = MULT73_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U12_GGA(x1, x2, x3) = U12_GGA(x1, x3)
MULT106_IN_GA(x1, x2) = MULT106_IN_GA(x1)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
U13_GGA(x1, x2, x3) = U13_GGA(x1, x3)
MULT144_IN_GA(x1, x2) = MULT144_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
U14_GGA(x1, x2, x3) = U14_GGA(x1, x3)
MULT187_IN_GA(x1, x2) = MULT187_IN_GA(x1)
U6_GA(x1, x2, x3) = U6_GA(x1, x3)
U15_GGA(x1, x2, x3) = U15_GGA(x1, x3)
MULT235_IN_GA(x1, x2) = MULT235_IN_GA(x1)
U7_GA(x1, x2, x3) = U7_GA(x1, x3)
U16_GGA(x1, x2, x3) = U16_GGA(x1, x3)
MULT288_IN_GA(x1, x2) = MULT288_IN_GA(x1)
U8_GA(x1, x2, x3) = U8_GA(x1, x3)
U17_GGA(x1, x2, x3, x4) = U17_GGA(x1, x2, x4)
MULT338_IN_GGGA(x1, x2, x3, x4) = MULT338_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4) = U18_GGGA(x1, x2, x4)
U19_GGGA(x1, x2, x3, x4, x5) = U19_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMES1_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, mult12_in_gga(T28, T29, T31))
TIMES1_IN_GGA(s(T28), T29, T31) → MULT12_IN_GGA(T28, T29, T31)
MULT12_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, mult22_in_ga(T51, T54))
MULT12_IN_GGA(s(T51), 0, T54) → MULT22_IN_GA(T51, T54)
MULT22_IN_GA(s(T63), T65) → U1_GA(T63, T65, mult22_in_ga(T63, T65))
MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)
MULT12_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, mult45_in_ga(T99, T102))
MULT12_IN_GGA(s(T99), s(0), s(T102)) → MULT45_IN_GA(T99, T102)
MULT45_IN_GA(s(T122), s(T124)) → U2_GA(T122, T124, mult45_in_ga(T122, T124))
MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → U11_GGA(T161, T164, mult73_in_ga(T161, T164))
MULT12_IN_GGA(s(T161), s(s(0)), s(s(T164))) → MULT73_IN_GA(T161, T164)
MULT73_IN_GA(s(T195), s(s(T197))) → U3_GA(T195, T197, mult73_in_ga(T195, T197))
MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → U12_GGA(T234, T237, mult106_in_ga(T234, T237))
MULT12_IN_GGA(s(T234), s(s(s(0))), s(s(s(T237)))) → MULT106_IN_GA(T234, T237)
MULT106_IN_GA(s(T279), s(s(s(T281)))) → U4_GA(T279, T281, mult106_in_ga(T279, T281))
MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → U13_GGA(T318, T321, mult144_in_ga(T318, T321))
MULT12_IN_GGA(s(T318), s(s(s(s(0)))), s(s(s(s(T321))))) → MULT144_IN_GA(T318, T321)
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → U5_GA(T374, T376, mult144_in_ga(T374, T376))
MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → U14_GGA(T413, T416, mult187_in_ga(T413, T416))
MULT12_IN_GGA(s(T413), s(s(s(s(s(0))))), s(s(s(s(s(T416)))))) → MULT187_IN_GA(T413, T416)
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → U6_GA(T480, T482, mult187_in_ga(T480, T482))
MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → U15_GGA(T519, T522, mult235_in_ga(T519, T522))
MULT12_IN_GGA(s(T519), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T522))))))) → MULT235_IN_GA(T519, T522)
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → U7_GA(T597, T599, mult235_in_ga(T597, T599))
MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → U16_GGA(T636, T639, mult288_in_ga(T636, T639))
MULT12_IN_GGA(s(T636), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T639)))))))) → MULT288_IN_GA(T636, T639)
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → U8_GA(T725, T727, mult288_in_ga(T725, T727))
MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → U17_GGA(T740, T742, T744, mult338_in_ggga(T740, s(s(s(s(s(s(s(T742))))))), T742, T744))
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → U18_GGGA(T767, T768, T770, mult12_in_gga(T767, s(T768), T770))
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → U19_GGGA(T786, T787, T788, T790, mult338_in_ggga(T786, T787, T788, T790))
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 29 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT288_IN_GA(s(T725), s(s(s(s(s(s(s(T727)))))))) → MULT288_IN_GA(T725, T727)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT288_IN_GA(x1, x2) = MULT288_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT288_IN_GA(s(T725)) → MULT288_IN_GA(T725)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT288_IN_GA(s(T725)) → MULT288_IN_GA(T725)
The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT235_IN_GA(s(T597), s(s(s(s(s(s(T599))))))) → MULT235_IN_GA(T597, T599)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT235_IN_GA(x1, x2) = MULT235_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT235_IN_GA(s(T597)) → MULT235_IN_GA(T597)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT235_IN_GA(s(T597)) → MULT235_IN_GA(T597)
The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT187_IN_GA(s(T480), s(s(s(s(s(T482)))))) → MULT187_IN_GA(T480, T482)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT187_IN_GA(x1, x2) = MULT187_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(18) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT187_IN_GA(s(T480)) → MULT187_IN_GA(T480)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(20) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT187_IN_GA(s(T480)) → MULT187_IN_GA(T480)
The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT144_IN_GA(s(T374), s(s(s(s(T376))))) → MULT144_IN_GA(T374, T376)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT144_IN_GA(x1, x2) = MULT144_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(23) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT144_IN_GA(s(T374)) → MULT144_IN_GA(T374)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT144_IN_GA(s(T374)) → MULT144_IN_GA(T374)
The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT106_IN_GA(s(T279), s(s(s(T281)))) → MULT106_IN_GA(T279, T281)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT106_IN_GA(x1, x2) = MULT106_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(28) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT106_IN_GA(s(T279)) → MULT106_IN_GA(T279)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(30) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT106_IN_GA(s(T279)) → MULT106_IN_GA(T279)
The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT73_IN_GA(s(T195), s(s(T197))) → MULT73_IN_GA(T195, T197)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT73_IN_GA(x1, x2) = MULT73_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT73_IN_GA(s(T195)) → MULT73_IN_GA(T195)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT73_IN_GA(s(T195)) → MULT73_IN_GA(T195)
The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT45_IN_GA(s(T122), s(T124)) → MULT45_IN_GA(T122, T124)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT45_IN_GA(x1, x2) = MULT45_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT45_IN_GA(s(T122)) → MULT45_IN_GA(T122)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT45_IN_GA(s(T122)) → MULT45_IN_GA(T122)
The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742)))))))), s(s(s(s(s(s(s(s(T744))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742, T744)
MULT338_IN_GGGA(s(T767), T768, 0, T770) → MULT12_IN_GGA(T767, s(T768), T770)
MULT338_IN_GGGA(T786, T787, s(T788), s(T790)) → MULT338_IN_GGGA(T786, T787, T788, T790)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
0 = 0
MULT12_IN_GGA(x1, x2, x3) = MULT12_IN_GGA(x1, x2)
MULT338_IN_GGGA(x1, x2, x3, x4) = MULT338_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(43) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742)
MULT338_IN_GGGA(s(T767), T768, 0) → MULT12_IN_GGA(T767, s(T768))
MULT338_IN_GGGA(T786, T787, s(T788)) → MULT338_IN_GGGA(T786, T787, T788)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(45) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT338_IN_GGGA(s(T767), T768, 0) → MULT12_IN_GGA(T767, s(T768))
The graph contains the following edges 1 > 1
MULT338_IN_GGGA(T786, T787, s(T788)) → MULT338_IN_GGGA(T786, T787, T788)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
MULT12_IN_GGA(T740, s(s(s(s(s(s(s(s(T742))))))))) → MULT338_IN_GGGA(T740, s(s(s(s(s(s(s(T742))))))), T742)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(46) YES

(47) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULT22_IN_GA(s(T63), T65) → MULT22_IN_GA(T63, T65)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
MULT22_IN_GA(x1, x2) = MULT22_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(48) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULT22_IN_GA(s(T63)) → MULT22_IN_GA(T63)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(50) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MULT22_IN_GA(s(T63)) → MULT22_IN_GA(T63)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) PiDPToQDPProof (SOUND transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) PiDPToQDPProof (SOUND transformation)

(14) Obligation:

(15) QDPSizeChangeProof (EQUIVALENT transformation)

(16) YES

(17) Obligation:

(18) PiDPToQDPProof (SOUND transformation)

(19) Obligation:

(20) QDPSizeChangeProof (EQUIVALENT transformation)

(21) YES

(22) Obligation:

(23) PiDPToQDPProof (SOUND transformation)

(24) Obligation:

(25) QDPSizeChangeProof (EQUIVALENT transformation)

(26) YES

(27) Obligation:

(28) PiDPToQDPProof (SOUND transformation)

(29) Obligation:

(30) QDPSizeChangeProof (EQUIVALENT transformation)

(31) YES

(32) Obligation:

(33) PiDPToQDPProof (SOUND transformation)

(34) Obligation:

(35) QDPSizeChangeProof (EQUIVALENT transformation)

(36) YES

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) PiDPToQDPProof (SOUND transformation)

(44) Obligation:

(45) QDPSizeChangeProof (EQUIVALENT transformation)

(46) YES

(47) Obligation:

(48) PiDPToQDPProof (SOUND transformation)

(49) Obligation:

(50) QDPSizeChangeProof (EQUIVALENT transformation)

(51) YES