%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1.1 % Problem : LCL681+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:10:11 PM UTC 2026 % Result : CounterSatisfiable 0.67s 0.98s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL681+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.38 % Computer : n001.cluster.edu % 0.10/0.38 % Model : x86_64 x86_64 % 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.38 % Memory : 8046.5625MB % 0.10/0.38 % OS : Linux 6.8.0-71-generic % 0.10/0.38 % CPULimit : 300 % 0.10/0.38 % WCLimit : 300 % 0.10/0.38 % DateTime : Fri Sep 4 22:45:15 UTC 2026 % 0.10/0.38 % CPUTime : % 0.10/0.38 Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.41 % 0.10/0.41 % Input Clauses: % 0.10/0.41 % 1:1:1:INP:Top: -> r1(x0,x0) % 0.10/0.41 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2) % 0.10/0.41 % 3:2:1:INP:Top: p2(x0) -> ren1(x0) % 0.10/0.41 % 4:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren1(x0) % 0.10/0.41 % 5:2:1:INP:Top: p2(x0) -> ren2(x0) % 0.10/0.41 % 6:3:2:INP:TopTop: r1(x0,x1),ren1(x1) -> ren2(x0) % 0.10/0.41 % 7:2:1:INP:Top: p2(x0) -> ren3(x0) % 0.10/0.41 % 8:3:2:INP:TopTop: r1(x0,x1),ren2(x1) -> ren3(x0) % 0.10/0.41 % 9:2:1:INP:Top: p2(x0) -> ren4(x0) % 0.10/0.41 % 10:3:2:INP:TopTop: r1(x0,x1),ren3(x1) -> ren4(x0) % 0.10/0.41 % 11:2:1:INP:Top: p2(x0) -> ren5(x0) % 0.10/0.41 % 12:3:2:INP:TopTop: r1(x0,x1),ren4(x1) -> ren5(x0) % 0.10/0.41 % 13:2:1:INP:Top: p2(x0) -> ren6(x0) % 0.10/0.41 % 14:3:2:INP:TopTop: r1(x0,x1),ren5(x1) -> ren6(x0) % 0.10/0.41 % 15:2:1:INP:Top: p2(x0) -> ren7(x0) % 0.10/0.41 % 16:3:2:INP:TopTop: r1(x0,x1),ren6(x1) -> ren7(x0) % 0.10/0.41 % 17:2:1:INP:Top: p2(x0) -> ren8(x0) % 0.10/0.41 % 18:3:2:INP:TopTop: r1(x0,x1),ren7(x1) -> ren8(x0) % 0.10/0.41 % 19:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1) % 0.10/0.41 % 20:2:2:INP:TopTop: p2(x0) -> ren9(x1,x0) % 0.10/0.41 % 21:3:3:INP:TopTopTop: r1(x0,x1),ren8(x1) -> ren9(x2,x0) % 0.10/0.41 % 22:2:1:INP:Top: p2(x0) -> ren10(x0) % 0.10/0.41 % 23:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren9(x2,skf1(x2)) -> p1(x1),ren10(x0) % 0.10/0.41 % 24:2:1:INP:Top: p2(x0) -> ren11(x0) % 0.10/0.41 % 25:3:2:INP:TopTop: r1(x0,x1),ren10(x1) -> ren11(x0) % 0.10/0.41 % 26:2:1:INP:Top: p2(x0) -> ren12(x0) % 0.10/0.41 % 27:3:2:INP:TopTop: r1(x0,x1),ren11(x1) -> ren12(x0) % 0.10/0.41 % 28:2:1:INP:Top: p2(x0) -> ren13(x0) % 0.10/0.41 % 29:3:2:INP:TopTop: r1(x0,x1),ren12(x1) -> ren13(x0) % 0.10/0.41 % 30:2:1:INP:Top: p2(x0) -> ren14(x0) % 0.10/0.41 % 31:3:2:INP:TopTop: r1(x0,x1),ren13(x1) -> ren14(x0) % 0.10/0.41 % 32:2:1:INP:Top: p2(x0) -> ren15(x0) % 0.10/0.41 % 33:3:2:INP:TopTop: r1(x0,x1),ren14(x1) -> ren15(x0) % 0.10/0.41 % 34:2:1:INP:Top: p2(x0) -> ren16(x0) % 0.10/0.41 % 35:3:2:INP:TopTop: r1(x0,x1),ren15(x1) -> ren16(x0) % 0.10/0.41 % 36:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1) % 0.10/0.41 % 37:2:2:INP:TopTop: p2(x0) -> ren17(x1,x0) % 0.10/0.41 % 38:3:3:INP:TopTopTop: r1(x0,x1),ren16(x1) -> ren17(x2,x0) % 0.10/0.41 % 39:2:1:INP:Top: p2(x0) -> ren18(x0) % 0.10/0.41 % 40:3:2:INP:TopTop: r1(x0,x1),ren17(x1,skf2(x1)) -> ren18(x0) % 0.10/0.41 % 41:2:1:INP:Top: p2(x0) -> ren19(x0) % 0.10/0.41 % 42:3:2:INP:TopTop: r1(x0,x1),ren18(x1) -> ren19(x0) % 0.10/0.41 % 43:2:1:INP:Top: p2(x0) -> ren20(x0) % 0.10/0.41 % 44:3:2:INP:TopTop: r1(x0,x1),ren19(x1) -> ren20(x0) % 0.10/0.41 % 45:2:1:INP:Top: p2(x0) -> ren21(x0) % 0.10/0.41 % 46:3:2:INP:TopTop: r1(x0,x1),ren20(x1) -> ren21(x0) % 0.10/0.41 % 47:2:1:INP:Top: p2(x0) -> ren22(x0) % 0.10/0.41 % 48:3:2:INP:TopTop: r1(x0,x1),ren21(x1) -> ren22(x0) % 0.10/0.41 % 49:2:1:INP:Top: p2(x0) -> ren23(x0) % 0.10/0.41 % 50:3:2:INP:TopTop: r1(x0,x1),ren22(x1) -> ren23(x0) % 0.10/0.41 % 51:2:1:INP:Top: p2(x0) -> ren24(x0) % 0.10/0.41 % 52:3:2:INP:TopTop: r1(x0,x1),ren23(x1) -> ren24(x0) % 0.10/0.41 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1) % 0.10/0.41 % 54:2:2:INP:TopTop: p2(x0) -> ren25(x1,x0) % 0.10/0.41 % 55:3:3:INP:TopTopTop: r1(x0,x1),ren24(x1) -> ren25(x2,x0) % 0.10/0.41 % 56:2:1:INP:Top: p2(x0) -> ren26(x0) % 0.10/0.41 % 57:3:2:INP:TopTop: r1(x0,x1),ren25(x1,skf3(x1)) -> ren26(x0) % 0.10/0.41 % 58:2:1:INP:Top: p2(x0) -> ren27(x0) % 0.10/0.41 % 59:3:2:INP:TopTop: r1(x0,x1),ren26(x1) -> ren27(x0) % 0.10/0.41 % 60:2:1:INP:Top: p2(x0) -> ren28(x0) % 0.10/0.41 % 61:3:2:INP:TopTop: r1(x0,x1),ren27(x1) -> ren28(x0) % 0.10/0.41 % 62:2:1:INP:Top: p2(x0) -> ren29(x0) % 0.10/0.41 % 63:3:2:INP:TopTop: r1(x0,x1),ren28(x1) -> ren29(x0) % 0.10/0.41 % 64:2:1:INP:Top: p2(x0) -> ren30(x0) % 0.10/0.41 % 65:3:2:INP:TopTop: r1(x0,x1),ren29(x1) -> ren30(x0) % 0.10/0.41 % 66:2:1:INP:Top: p2(x0) -> ren31(x0) % 0.10/0.41 % 67:3:2:INP:TopTop: r1(x0,x1),ren30(x1) -> ren31(x0) % 0.10/0.41 % 68:2:1:INP:Top: p2(x0) -> ren32(x0) % 0.10/0.41 % 69:3:2:INP:TopTop: r1(x0,x1),ren31(x1) -> ren32(x0) % 0.10/0.41 % 70:2:2:INP:TopTop: -> r1(x0,x1),ren33(x0,x1) % 0.10/0.41 % 71:2:2:INP:TopTop: p2(x0) -> ren33(x1,x0) % 0.10/0.41 % 72:3:3:INP:TopTopTop: r1(x0,x1),ren32(x1) -> ren33(x2,x0) % 0.10/0.41 % 73:2:1:INP:Top: p2(x0) -> ren34(x0) % 0.10/0.41 % 74:3:2:INP:TopTop: r1(x0,x1),ren33(x1,skf4(x1)) -> ren34(x0) % 0.10/0.41 % 75:2:1:INP:Top: p2(x0) -> ren35(x0) % 0.10/0.41 % 76:3:2:INP:TopTop: r1(x0,x1),ren34(x1) -> ren35(x0) % 0.10/0.41 % 77:2:1:INP:Top: p2(x0) -> ren36(x0) % 0.10/0.41 % 78:3:2:INP:TopTop: r1(x0,x1),ren35(x1) -> ren36(x0) % 0.10/0.41 % 79:2:1:INP:Top: p2(x0) -> ren37(x0) % 0.10/0.41 % 80:3:2:INP:TopTop: r1(x0,x1),ren36(x1) -> ren37(x0) % 0.10/0.41 % 81:2:1:INP:Top: p2(x0) -> ren38(x0) % 0.10/0.41 % 82:3:2:INP:TopTop: r1(x0,x1),ren37(x1) -> ren38(x0) % 0.10/0.41 % 83:2:1:INP:Top: p2(x0) -> ren39(x0) % 0.10/0.41 % 84:3:2:INP:TopTop: r1(x0,x1),ren38(x1) -> ren39(x0) % 0.10/0.41 % 85:2:1:INP:Top: p2(x0) -> ren40(x0) % 0.10/0.41 % 86:3:2:INP:TopTop: r1(x0,x1),ren39(x1) -> ren40(x0) % 0.10/0.41 % 87:2:2:INP:TopTop: -> r1(x0,x1),ren41(x0,x1) % 0.10/0.41 % 88:2:2:INP:TopTop: p2(x0) -> ren41(x1,x0) % 0.10/0.41 % 89:3:3:INP:TopTopTop: r1(x0,x1),ren40(x1) -> ren41(x2,x0) % 0.10/0.41 % 90:2:1:INP:Top: p2(x0) -> ren42(x0) % 0.10/0.41 % 91:3:2:INP:TopTop: r1(x0,x1),ren41(x1,skf5(x1)) -> ren42(x0) % 0.10/0.41 % 92:2:1:INP:Top: p2(x0) -> ren43(x0) % 0.10/0.41 % 93:3:2:INP:TopTop: r1(x0,x1),ren42(x1) -> ren43(x0) % 0.10/0.41 % 94:2:1:INP:Top: p2(x0) -> ren44(x0) % 0.10/0.41 % 95:3:2:INP:TopTop: r1(x0,x1),ren43(x1) -> ren44(x0) % 0.10/0.41 % 96:2:1:INP:Top: p2(x0) -> ren45(x0) % 0.10/0.41 % 97:3:2:INP:TopTop: r1(x0,x1),ren44(x1) -> ren45(x0) % 0.10/0.41 % 98:2:1:INP:Top: p2(x0) -> ren46(x0) % 0.10/0.41 % 99:3:2:INP:TopTop: r1(x0,x1),ren45(x1) -> ren46(x0) % 0.10/0.41 % 100:2:1:INP:Top: p2(x0) -> ren47(x0) % 0.10/0.41 % 101:3:2:INP:TopTop: r1(x0,x1),ren46(x1) -> ren47(x0) % 0.10/0.41 % 102:2:1:INP:Top: p2(x0) -> ren48(x0) % 0.10/0.41 % 103:3:2:INP:TopTop: r1(x0,x1),ren47(x1) -> ren48(x0) % 0.10/0.41 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren49(x0,x1) % 0.10/0.41 % 105:2:2:INP:TopTop: p2(x0) -> ren49(x1,x0) % 0.10/0.41 % 106:3:3:INP:TopTopTop: r1(x0,x1),ren48(x1) -> ren49(x2,x0) % 0.10/0.41 % 107:2:1:INP:Top: p2(x0) -> ren50(x0) % 0.10/0.41 % 108:3:2:INP:TopTop: r1(x0,x1),ren49(x1,skf6(x1)) -> ren50(x0) % 0.10/0.41 % 109:2:1:INP:Top: p2(x0) -> ren51(x0) % 0.10/0.41 % 110:3:2:INP:TopTop: r1(x0,x1),ren50(x1) -> ren51(x0) % 0.10/0.41 % 111:2:1:INP:Top: p2(x0) -> ren52(x0) % 0.10/0.41 % 112:3:2:INP:TopTop: r1(x0,x1),ren51(x1) -> ren52(x0) % 0.10/0.41 % 113:2:1:INP:Top: p2(x0) -> ren53(x0) % 0.10/0.41 % 114:3:2:INP:TopTop: r1(x0,x1),ren52(x1) -> ren53(x0) % 0.10/0.41 % 115:2:1:INP:Top: p2(x0) -> ren54(x0) % 0.10/0.41 % 116:3:2:INP:TopTop: r1(x0,x1),ren53(x1) -> ren54(x0) % 0.10/0.41 % 117:2:1:INP:Top: p2(x0) -> ren55(x0) % 0.10/0.41 % 118:3:2:INP:TopTop: r1(x0,x1),ren54(x1) -> ren55(x0) % 0.10/0.41 % 119:2:1:INP:Top: p2(x0) -> ren56(x0) % 0.10/0.41 % 120:3:2:INP:TopTop: r1(x0,x1),ren55(x1) -> ren56(x0) % 0.10/0.41 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren57(x0,x1) % 0.10/0.41 % 122:2:2:INP:TopTop: p2(x0) -> ren57(x1,x0) % 0.10/0.41 % 123:3:3:INP:TopTopTop: r1(x0,x1),ren56(x1) -> ren57(x2,x0) % 0.10/0.41 % 124:2:1:INP:Top: p2(x0) -> ren58(x0) % 0.10/0.41 % 125:3:2:INP:TopTop: r1(x0,x1),ren57(x1,skf7(x1)) -> ren58(x0) % 0.10/0.41 % 126:2:1:INP:Top: p2(x0) -> ren59(x0) % 0.10/0.41 % 127:3:2:INP:TopTop: r1(x0,x1),ren58(x1) -> ren59(x0) % 0.10/0.41 % 128:2:1:INP:Top: p2(x0) -> ren60(x0) % 0.10/0.41 % 129:3:2:INP:TopTop: r1(x0,x1),ren59(x1) -> ren60(x0) % 0.10/0.41 % 130:2:1:INP:Top: p2(x0) -> ren61(x0) % 0.10/0.41 % 131:3:2:INP:TopTop: r1(x0,x1),ren60(x1) -> ren61(x0) % 0.10/0.41 % 132:2:1:INP:Top: p2(x0) -> ren62(x0) % 0.10/0.41 % 133:3:2:INP:TopTop: r1(x0,x1),ren61(x1) -> ren62(x0) % 0.10/0.41 % 134:2:1:INP:Top: p2(x0) -> ren63(x0) % 0.10/0.41 % 135:3:2:INP:TopTop: r1(x0,x1),ren62(x1) -> ren63(x0) % 0.10/0.41 % 136:2:1:INP:Top: p2(x0) -> ren64(x0) % 0.10/0.41 % 137:3:2:INP:TopTop: r1(x0,x1),ren63(x1) -> ren64(x0) % 0.10/0.41 % 138:2:2:INP:TopTop: -> r1(x0,x1),ren65(x0,x1) % 0.10/0.41 % 139:2:2:INP:TopTop: p2(x0) -> ren65(x1,x0) % 0.10/0.41 % 140:3:3:INP:TopTopTop: r1(x0,x1),ren64(x1) -> ren65(x2,x0) % 0.10/0.41 % 141:2:1:INP:Top: p2(x0) -> ren66(x0) % 0.10/0.41 % 142:3:2:INP:TopTop: r1(x0,x1),ren65(x1,skf8(x1)) -> ren66(x0) % 0.10/0.41 % 143:2:1:INP:Top: p2(x0) -> ren67(x0) % 0.10/0.41 % 144:3:2:INP:TopTop: r1(x0,x1),ren66(x1) -> ren67(x0) % 0.10/0.41 % 145:2:1:INP:Top: p2(x0) -> ren68(x0) % 0.10/0.41 % 146:3:2:INP:TopTop: r1(x0,x1),ren67(x1) -> ren68(x0) % 0.10/0.41 % 147:2:1:INP:Top: p2(x0) -> ren69(x0) % 0.10/0.41 % 148:3:2:INP:TopTop: r1(x0,x1),ren68(x1) -> ren69(x0) % 0.10/0.41 % 149:2:1:INP:Top: p2(x0) -> ren70(x0) % 0.10/0.41 % 150:3:2:INP:TopTop: r1(x0,x1),ren69(x1) -> ren70(x0) % 0.10/0.41 % 151:2:1:INP:Top: p2(x0) -> ren71(x0) % 0.10/0.41 % 152:3:2:INP:TopTop: r1(x0,x1),ren70(x1) -> ren71(x0) % 0.10/0.41 % 153:2:1:INP:Top: p2(x0) -> ren72(x0) % 0.10/0.41 % 154:3:2:INP:TopTop: r1(x0,x1),ren71(x1) -> ren72(x0) % 0.10/0.41 % 155:2:2:INP:TopTop: -> r1(x0,x1),ren73(x0,x1) % 0.10/0.41 % 156:2:2:INP:TopTop: p2(x0) -> ren73(x1,x0) % 0.10/0.41 % 157:3:3:INP:TopTopTop: r1(x0,x1),ren72(x1) -> ren73(x2,x0) % 0.10/0.41 % 158:2:1:INP:Top: p2(x0) -> ren74(x0) % 0.10/0.41 % 159:3:2:INP:TopTop: r1(x0,x1),ren73(x1,skf9(x1)) -> ren74(x0) % 0.10/0.41 % 160:2:1:INP:Top: p2(x0) -> ren75(x0) % 0.10/0.41 % 161:3:2:INP:TopTop: r1(x0,x1),ren74(x1) -> ren75(x0) % 0.10/0.41 % 162:2:1:INP:Top: p2(x0) -> ren76(x0) % 0.10/0.41 % 163:3:2:INP:TopTop: r1(x0,x1),ren75(x1) -> ren76(x0) % 0.10/0.41 % 164:2:1:INP:Top: p2(x0) -> ren77(x0) % 0.10/0.41 % 165:3:2:INP:TopTop: r1(x0,x1),ren76(x1) -> ren77(x0) % 0.10/0.41 % 166:2:1:INP:Top: p2(x0) -> ren78(x0) % 0.10/0.41 % 167:3:2:INP:TopTop: r1(x0,x1),ren77(x1) -> ren78(x0) % 0.10/0.41 % 168:2:1:INP:Top: p2(x0) -> ren79(x0) % 0.10/0.41 % 169:3:2:INP:TopTop: r1(x0,x1),ren78(x1) -> ren79(x0) % 0.10/0.41 % 170:2:1:INP:Top: p2(x0) -> ren80(x0) % 0.10/0.41 % 171:3:2:INP:TopTop: r1(x0,x1),ren79(x1) -> ren80(x0) % 0.10/0.41 % 172:2:1:INP:Top: p2(x0) -> ren81(x0) % 0.10/0.41 % 173:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren81(x0) % 0.10/0.41 % 174:2:1:INP:Top: p2(x0) -> ren82(x0) % 0.10/0.41 % 175:3:2:INP:TopTop: r1(x0,x1),ren81(x1) -> ren82(x0) % 0.10/0.41 % 176:2:1:INP:Top: p2(x0) -> ren83(x0) % 0.10/0.41 % 177:3:2:INP:TopTop: r1(x0,x1),ren82(x1) -> ren83(x0) % 0.10/0.41 % 178:2:1:INP:Top: p2(x0) -> ren84(x0) % 0.10/0.41 % 179:3:2:INP:TopTop: r1(x0,x1),ren83(x1) -> ren84(x0) % 0.10/0.41 % 180:2:1:INP:Top: p2(x0) -> ren85(x0) % 0.10/0.41 % 181:3:2:INP:TopTop: r1(x0,x1),ren84(x1) -> ren85(x0) % 0.10/0.41 % 182:2:1:INP:Top: p2(x0) -> ren86(x0) % 0.10/0.41 % 183:3:2:INP:TopTop: r1(x0,x1),ren85(x1) -> ren86(x0) % 0.10/0.41 % 184:2:1:INP:Top: p2(x0) -> ren87(x0) % 0.10/0.41 % 185:3:2:INP:TopTop: r1(x0,x1),ren86(x1) -> ren87(x0) % 0.10/0.41 % 186:2:1:INP:Top: p2(x0) -> ren88(x0) % 0.10/0.41 % 187:3:2:INP:TopTop: r1(x0,x1),ren87(x1) -> ren88(x0) % 0.10/0.41 % 188:2:2:INP:TopTop: -> r1(x0,x1),ren89(x0,x1) % 0.10/0.41 % 189:2:2:INP:TopTop: p2(x0) -> ren89(x1,x0) % 0.10/0.41 % 190:3:3:INP:TopTopTop: r1(x0,x1),ren88(x1) -> ren89(x2,x0) % 0.10/0.41 % 191:2:1:INP:Top: p2(x0) -> ren90(x0) % 0.10/0.41 % 192:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren89(x2,skf10(x2)) -> p1(x1),ren90(x0) % 0.10/0.41 % 193:2:1:INP:Top: p2(x0) -> ren91(x0) % 0.10/0.41 % 194:3:2:INP:TopTop: r1(x0,x1),ren90(x1) -> ren91(x0) % 0.10/0.41 % 195:2:1:INP:Top: p2(x0) -> ren92(x0) % 0.10/0.41 % 196:3:2:INP:TopTop: r1(x0,x1),ren91(x1) -> ren92(x0) % 0.10/0.41 % 197:2:1:INP:Top: p2(x0) -> ren93(x0) % 0.10/0.41 % 198:3:2:INP:TopTop: r1(x0,x1),ren92(x1) -> ren93(x0) % 0.10/0.41 % 199:2:1:INP:Top: p2(x0) -> ren94(x0) % 0.10/0.41 % 200:3:2:INP:TopTop: r1(x0,x1),ren93(x1) -> ren94(x0) % 0.10/0.41 % 201:2:1:INP:Top: p2(x0) -> ren95(x0) % 0.10/0.41 % 202:3:2:INP:TopTop: r1(x0,x1),ren94(x1) -> ren95(x0) % 0.10/0.41 % 203:2:1:INP:Top: p2(x0) -> ren96(x0) % 0.10/0.41 % 204:3:2:INP:TopTop: r1(x0,x1),ren95(x1) -> ren96(x0) % 0.10/0.41 % 205:2:2:INP:TopTop: -> r1(x0,x1),ren97(x0,x1) % 0.10/0.41 % 206:2:2:INP:TopTop: p2(x0) -> ren97(x1,x0) % 0.10/0.41 % 207:3:3:INP:TopTopTop: r1(x0,x1),ren96(x1) -> ren97(x2,x0) % 0.10/0.41 % 208:2:1:INP:Top: p2(x0) -> ren98(x0) % 0.10/0.41 % 209:3:2:INP:TopTop: r1(x0,x1),ren97(x1,skf11(x1)) -> ren98(x0) % 0.10/0.41 % 210:2:1:INP:Top: p2(x0) -> ren99(x0) % 0.10/0.41 % 211:3:2:INP:TopTop: r1(x0,x1),ren98(x1) -> ren99(x0) % 0.10/0.41 % 212:2:1:INP:Top: p2(x0) -> ren100(x0) % 0.10/0.41 % 213:3:2:INP:TopTop: r1(x0,x1),ren99(x1) -> ren100(x0) % 0.10/0.41 % 214:2:1:INP:Top: p2(x0) -> ren101(x0) % 0.10/0.41 % 215:3:2:INP:TopTop: r1(x0,x1),ren100(x1) -> ren101(x0) % 0.10/0.41 % 216:2:1:INP:Top: p2(x0) -> ren102(x0) % 0.10/0.41 % 217:3:2:INP:TopTop: r1(x0,x1),ren101(x1) -> ren102(x0) % 0.10/0.41 % 218:2:1:INP:Top: p2(x0) -> ren103(x0) % 0.10/0.41 % 219:3:2:INP:TopTop: r1(x0,x1),ren102(x1) -> ren103(x0) % 0.10/0.41 % 220:2:1:INP:Top: p2(x0) -> ren104(x0) % 0.10/0.41 % 221:3:2:INP:TopTop: r1(x0,x1),ren103(x1) -> ren104(x0) % 0.10/0.41 % 222:2:2:INP:TopTop: -> r1(x0,x1),ren105(x0,x1) % 0.10/0.41 % 223:2:2:INP:TopTop: p2(x0) -> ren105(x1,x0) % 0.10/0.41 % 224:3:3:INP:TopTopTop: r1(x0,x1),ren104(x1) -> ren105(x2,x0) % 0.10/0.41 % 225:2:1:INP:Top: p2(x0) -> ren106(x0) % 0.10/0.41 % 226:3:2:INP:TopTop: r1(x0,x1),ren105(x1,skf12(x1)) -> ren106(x0) % 0.10/0.41 % 227:2:1:INP:Top: p2(x0) -> ren107(x0) % 0.10/0.41 % 228:3:2:INP:TopTop: r1(x0,x1),ren106(x1) -> ren107(x0) % 0.10/0.41 % 229:2:1:INP:Top: p2(x0) -> ren108(x0) % 0.10/0.41 % 230:3:2:INP:TopTop: r1(x0,x1),ren107(x1) -> ren108(x0) % 0.10/0.41 % 231:2:1:INP:Top: p2(x0) -> ren109(x0) % 0.10/0.41 % 232:3:2:INP:TopTop: r1(x0,x1),ren108(x1) -> ren109(x0) % 0.10/0.41 % 233:2:1:INP:Top: p2(x0) -> ren110(x0) % 0.10/0.41 % 234:3:2:INP:TopTop: r1(x0,x1),ren109(x1) -> ren110(x0) % 0.10/0.41 % 235:2:1:INP:Top: p2(x0) -> ren111(x0) % 0.10/0.41 % 236:3:2:INP:TopTop: r1(x0,x1),ren110(x1) -> ren111(x0) % 0.10/0.41 % 237:2:1:INP:Top: p2(x0) -> ren112(x0) % 0.10/0.41 % 238:3:2:INP:TopTop: r1(x0,x1),ren111(x1) -> ren112(x0) % 0.10/0.41 % 239:2:2:INP:TopTop: -> r1(x0,x1),ren113(x0,x1) % 0.10/0.41 % 240:2:2:INP:TopTop: p2(x0) -> ren113(x1,x0) % 0.10/0.41 % 241:3:3:INP:TopTopTop: r1(x0,x1),ren112(x1) -> ren113(x2,x0) % 0.10/0.41 % 242:2:1:INP:Top: p2(x0) -> ren114(x0) % 0.10/0.41 % 243:3:2:INP:TopTop: r1(x0,x1),ren113(x1,skf13(x1)) -> ren114(x0) % 0.10/0.41 % 244:2:1:INP:Top: p2(x0) -> ren115(x0) % 0.10/0.41 % 245:3:2:INP:TopTop: r1(x0,x1),ren114(x1) -> ren115(x0) % 0.10/0.41 % 246:2:1:INP:Top: p2(x0) -> ren116(x0) % 0.10/0.41 % 247:3:2:INP:TopTop: r1(x0,x1),ren115(x1) -> ren116(x0) % 0.10/0.41 % 248:2:1:INP:Top: p2(x0) -> ren117(x0) % 0.10/0.41 % 249:3:2:INP:TopTop: r1(x0,x1),ren116(x1) -> ren117(x0) % 0.10/0.41 % 250:2:1:INP:Top: p2(x0) -> ren118(x0) % 0.10/0.41 % 251:3:2:INP:TopTop: r1(x0,x1),ren117(x1) -> ren118(x0) % 0.10/0.41 % 252:2:1:INP:Top: p2(x0) -> ren119(x0) % 0.10/0.41 % 253:3:2:INP:TopTop: r1(x0,x1),ren118(x1) -> ren119(x0) % 0.10/0.41 % 254:2:1:INP:Top: p2(x0) -> ren120(x0) % 0.10/0.41 % 255:3:2:INP:TopTop: r1(x0,x1),ren119(x1) -> ren120(x0) % 0.10/0.41 % 256:2:2:INP:TopTop: -> r1(x0,x1),ren121(x0,x1) % 0.10/0.41 % 257:2:2:INP:TopTop: p2(x0) -> ren121(x1,x0) % 0.10/0.41 % 258:3:3:INP:TopTopTop: r1(x0,x1),ren120(x1) -> ren121(x2,x0) % 0.10/0.41 % 259:2:1:INP:Top: p2(x0) -> ren122(x0) % 0.10/0.41 % 260:3:2:INP:TopTop: r1(x0,x1),ren121(x1,skf14(x1)) -> ren122(x0) % 0.10/0.41 % 261:2:1:INP:Top: p2(x0) -> ren123(x0) % 0.10/0.41 % 262:3:2:INP:TopTop: r1(x0,x1),ren122(x1) -> ren123(x0) % 0.10/0.41 % 263:2:1:INP:Top: p2(x0) -> ren124(x0) % 0.10/0.41 % 264:3:2:INP:TopTop: r1(x0,x1),ren123(x1) -> ren124(x0) % 0.10/0.41 % 265:2:1:INP:Top: p2(x0) -> ren125(x0) % 0.10/0.41 % 266:3:2:INP:TopTop: r1(x0,x1),ren124(x1) -> ren125(x0) % 0.10/0.41 % 267:2:1:INP:Top: p2(x0) -> ren126(x0) % 0.10/0.41 % 268:3:2:INP:TopTop: r1(x0,x1),ren125(x1) -> ren126(x0) % 0.10/0.41 % 269:2:1:INP:Top: p2(x0) -> ren127(x0) % 0.10/0.41 % 270:3:2:INP:TopTop: r1(x0,x1),ren126(x1) -> ren127(x0) % 0.10/0.41 % 271:2:1:INP:Top: p2(x0) -> ren128(x0) % 0.10/0.41 % 272:3:2:INP:TopTop: r1(x0,x1),ren127(x1) -> ren128(x0) % 0.10/0.41 % 273:2:2:INP:TopTop: -> r1(x0,x1),ren129(x0,x1) % 0.10/0.41 % 274:2:2:INP:TopTop: p2(x0) -> ren129(x1,x0) % 0.10/0.41 % 275:3:3:INP:TopTopTop: r1(x0,x1),ren128(x1) -> ren129(x2,x0) % 0.10/0.41 % 276:2:1:INP:Top: p2(x0) -> ren130(x0) % 0.10/0.41 % 277:3:2:INP:TopTop: r1(x0,x1),ren129(x1,skf15(x1)) -> ren130(x0) % 0.10/0.41 % 278:2:1:INP:Top: p2(x0) -> ren131(x0) % 0.10/0.41 % 279:3:2:INP:TopTop: r1(x0,x1),ren130(x1) -> ren131(x0) % 0.10/0.41 % 280:2:1:INP:Top: p2(x0) -> ren132(x0) % 0.10/0.41 % 281:3:2:INP:TopTop: r1(x0,x1),ren131(x1) -> ren132(x0) % 0.10/0.41 % 282:2:1:INP:Top: p2(x0) -> ren133(x0) % 0.10/0.41 % 283:3:2:INP:TopTop: r1(x0,x1),ren132(x1) -> ren133(x0) % 0.10/0.41 % 284:2:1:INP:Top: p2(x0) -> ren134(x0) % 0.10/0.41 % 285:3:2:INP:TopTop: r1(x0,x1),ren133(x1) -> ren134(x0) % 0.10/0.41 % 286:2:1:INP:Top: p2(x0) -> ren135(x0) % 0.10/0.41 % 287:3:2:INP:TopTop: r1(x0,x1),ren134(x1) -> ren135(x0) % 0.10/0.41 % 288:2:1:INP:Top: p2(x0) -> ren136(x0) % 0.10/0.41 % 289:3:2:INP:TopTop: r1(x0,x1),ren135(x1) -> ren136(x0) % 0.10/0.41 % 290:2:2:INP:TopTop: -> r1(x0,x1),ren137(x0,x1) % 0.10/0.41 % 291:2:2:INP:TopTop: p2(x0) -> ren137(x1,x0) % 0.10/0.41 % 292:3:3:INP:TopTopTop: r1(x0,x1),ren136(x1) -> ren137(x2,x0) % 0.10/0.41 % 293:2:1:INP:Top: p2(x0) -> ren138(x0) % 0.10/0.41 % 294:3:2:INP:TopTop: r1(x0,x1),ren137(x1,skf16(x1)) -> ren138(x0) % 0.10/0.41 % 295:2:1:INP:Top: p2(x0) -> ren139(x0) % 0.10/0.41 % 296:3:2:INP:TopTop: r1(x0,x1),ren138(x1) -> ren139(x0) % 0.10/0.41 % 297:2:1:INP:Top: p2(x0) -> ren140(x0) % 0.10/0.41 % 298:3:2:INP:TopTop: r1(x0,x1),ren139(x1) -> ren140(x0) % 0.10/0.41 % 299:2:1:INP:Top: p2(x0) -> ren141(x0) % 0.10/0.41 % 300:3:2:INP:TopTop: r1(x0,x1),ren140(x1) -> ren141(x0) % 0.10/0.41 % 301:2:1:INP:Top: p2(x0) -> ren142(x0) % 0.10/0.41 % 302:3:2:INP:TopTop: r1(x0,x1),ren141(x1) -> ren142(x0) % 0.10/0.41 % 303:2:1:INP:Top: p2(x0) -> ren143(x0) % 0.10/0.41 % 304:3:2:INP:TopTop: r1(x0,x1),ren142(x1) -> ren143(x0) % 0.10/0.41 % 305:2:1:INP:Top: p2(x0) -> ren144(x0) % 0.10/0.41 % 306:3:2:INP:TopTop: r1(x0,x1),ren143(x1) -> ren144(x0) % 0.10/0.41 % 307:2:2:INP:TopTop: -> r1(x0,x1),ren145(x0,x1) % 0.10/0.41 % 308:2:2:INP:TopTop: p2(x0) -> ren145(x1,x0) % 0.10/0.41 % 309:3:3:INP:TopTopTop: r1(x0,x1),ren144(x1) -> ren145(x2,x0) % 0.10/0.41 % 310:2:1:INP:Top: p2(x0) -> ren146(x0) % 0.10/0.41 % 311:3:2:INP:TopTop: r1(x0,x1),ren145(x1,skf17(x1)) -> ren146(x0) % 0.10/0.41 % 312:2:1:INP:Top: p2(x0) -> ren147(x0) % 0.10/0.41 % 313:3:2:INP:TopTop: r1(x0,x1),ren146(x1) -> ren147(x0) % 0.10/0.41 % 314:2:1:INP:Top: p2(x0) -> ren148(x0) % 0.10/0.41 % 315:3:2:INP:TopTop: r1(x0,x1),ren147(x1) -> ren148(x0) % 0.10/0.41 % 316:2:1:INP:Top: p2(x0) -> ren149(x0) % 0.10/0.41 % 317:3:2:INP:TopTop: r1(x0,x1),ren148(x1) -> ren149(x0) % 0.10/0.41 % 318:2:1:INP:Top: p2(x0) -> ren150(x0) % 0.10/0.41 % 319:3:2:INP:TopTop: r1(x0,x1),ren149(x1) -> ren150(x0) % 0.10/0.41 % 320:2:1:INP:Top: p2(x0) -> ren151(x0) % 0.10/0.41 % 321:3:2:INP:TopTop: r1(x0,x1),ren150(x1) -> ren151(x0) % 0.10/0.41 % 322:2:1:INP:Top: p2(x0) -> ren152(x0) % 0.10/0.41 % 323:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren152(x0) % 0.10/0.41 % 324:2:1:INP:Top: p2(x0) -> ren153(x0) % 0.10/0.41 % 325:3:2:INP:TopTop: r1(x0,x1),ren152(x1) -> ren153(x0) % 0.10/0.41 % 326:2:1:INP:Top: p2(x0) -> ren154(x0) % 0.10/0.41 % 327:3:2:INP:TopTop: r1(x0,x1),ren153(x1) -> ren154(x0) % 0.10/0.41 % 328:2:1:INP:Top: p2(x0) -> ren155(x0) % 0.10/0.41 % 329:3:2:INP:TopTop: r1(x0,x1),ren154(x1) -> ren155(x0) % 0.10/0.41 % 330:2:1:INP:Top: p2(x0) -> ren156(x0) % 0.10/0.41 % 331:3:2:INP:TopTop: r1(x0,x1),ren155(x1) -> ren156(x0) % 0.10/0.41 % 332:2:1:INP:Top: p2(x0) -> ren157(x0) % 0.10/0.41 % 333:3:2:INP:TopTop: r1(x0,x1),ren156(x1) -> ren157(x0) % 0.10/0.41 % 334:2:1:INP:Top: p2(x0) -> ren158(x0) % 0.10/0.41 % 335:3:2:INP:TopTop: r1(x0,x1),ren157(x1) -> ren158(x0) % 0.10/0.41 % 336:2:1:INP:Top: p2(x0) -> ren159(x0) % 0.10/0.41 % 337:3:2:INP:TopTop: r1(x0,x1),ren158(x1) -> ren159(x0) % 0.10/0.41 % 338:2:2:INP:TopTop: -> r1(x0,x1),ren160(x0,x1) % 0.10/0.41 % 339:2:2:INP:TopTop: p2(x0) -> ren160(x1,x0) % 0.10/0.41 % 340:3:3:INP:TopTopTop: r1(x0,x1),ren159(x1) -> ren160(x2,x0) % 0.10/0.41 % 341:2:1:INP:Top: p2(x0) -> ren161(x0) % 0.10/0.41 % 342:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren160(x2,skf18(x2)) -> p1(x1),ren161(x0) % 0.10/0.41 % 343:2:1:INP:Top: p2(x0) -> ren162(x0) % 0.10/0.41 % 344:3:2:INP:TopTop: r1(x0,x1),ren161(x1) -> ren162(x0) % 0.10/0.41 % 345:2:1:INP:Top: p2(x0) -> ren163(x0) % 0.10/0.41 % 346:3:2:INP:TopTop: r1(x0,x1),ren162(x1) -> ren163(x0) % 0.10/0.41 % 347:2:1:INP:Top: p2(x0) -> ren164(x0) % 0.10/0.41 % 348:3:2:INP:TopTop: r1(x0,x1),ren163(x1) -> ren164(x0) % 0.10/0.41 % 349:2:1:INP:Top: p2(x0) -> ren165(x0) % 0.10/0.41 % 350:3:2:INP:TopTop: r1(x0,x1),ren164(x1) -> ren165(x0) % 0.10/0.41 % 351:2:1:INP:Top: p2(x0) -> ren166(x0) % 0.10/0.41 % 352:3:2:INP:TopTop: r1(x0,x1),ren165(x1) -> ren166(x0) % 0.10/0.41 % 353:2:1:INP:Top: p2(x0) -> ren167(x0) % 0.10/0.41 % 354:3:2:INP:TopTop: r1(x0,x1),ren166(x1) -> ren167(x0) % 0.10/0.41 % 355:2:2:INP:TopTop: -> r1(x0,x1),ren168(x0,x1) % 0.10/0.41 % 356:2:2:INP:TopTop: p2(x0) -> ren168(x1,x0) % 0.10/0.41 % 357:3:3:INP:TopTopTop: r1(x0,x1),ren167(x1) -> ren168(x2,x0) % 0.10/0.41 % 358:2:1:INP:Top: p2(x0) -> ren169(x0) % 0.10/0.41 % 359:3:2:INP:TopTop: r1(x0,x1),ren168(x1,skf19(x1)) -> ren169(x0) % 0.10/0.41 % 360:2:1:INP:Top: p2(x0) -> ren170(x0) % 0.10/0.41 % 361:3:2:INP:TopTop: r1(x0,x1),ren169(x1) -> ren170(x0) % 0.10/0.41 % 362:2:1:INP:Top: p2(x0) -> ren171(x0) % 0.10/0.41 % 363:3:2:INP:TopTop: r1(x0,x1),ren170(x1) -> ren171(x0) % 0.10/0.41 % 364:2:1:INP:Top: p2(x0) -> ren172(x0) % 0.10/0.41 % 365:3:2:INP:TopTop: r1(x0,x1),ren171(x1) -> ren172(x0) % 0.10/0.41 % 366:2:1:INP:Top: p2(x0) -> ren173(x0) % 0.10/0.41 % 367:3:2:INP:TopTop: r1(x0,x1),ren172(x1) -> ren173(x0) % 0.10/0.41 % 368:2:1:INP:Top: p2(x0) -> ren174(x0) % 0.10/0.41 % 369:3:2:INP:TopTop: r1(x0,x1),ren173(x1) -> ren174(x0) % 0.10/0.41 % 370:2:1:INP:Top: p2(x0) -> ren175(x0) % 0.10/0.41 % 371:3:2:INP:TopTop: r1(x0,x1),ren174(x1) -> ren175(x0) % 0.10/0.41 % 372:2:2:INP:TopTop: -> r1(x0,x1),ren176(x0,x1) % 0.10/0.41 % 373:2:2:INP:TopTop: p2(x0) -> ren176(x1,x0) % 0.10/0.41 % 374:3:3:INP:TopTopTop: r1(x0,x1),ren175(x1) -> ren176(x2,x0) % 0.10/0.41 % 375:2:1:INP:Top: p2(x0) -> ren177(x0) % 0.10/0.41 % 376:3:2:INP:TopTop: r1(x0,x1),ren176(x1,skf20(x1)) -> ren177(x0) % 0.10/0.41 % 377:2:1:INP:Top: p2(x0) -> ren178(x0) % 0.10/0.41 % 378:3:2:INP:TopTop: r1(x0,x1),ren177(x1) -> ren178(x0) % 0.10/0.41 % 379:2:1:INP:Top: p2(x0) -> ren179(x0) % 0.10/0.41 % 380:3:2:INP:TopTop: r1(x0,x1),ren178(x1) -> ren179(x0) % 0.10/0.41 % 381:2:1:INP:Top: p2(x0) -> ren180(x0) % 0.10/0.41 % 382:3:2:INP:TopTop: r1(x0,x1),ren179(x1) -> ren180(x0) % 0.10/0.41 % 383:2:1:INP:Top: p2(x0) -> ren181(x0) % 0.10/0.41 % 384:3:2:INP:TopTop: r1(x0,x1),ren180(x1) -> ren181(x0) % 0.10/0.41 % 385:2:1:INP:Top: p2(x0) -> ren182(x0) % 0.10/0.41 % 386:3:2:INP:TopTop: r1(x0,x1),ren181(x1) -> ren182(x0) % 0.10/0.41 % 387:2:1:INP:Top: p2(x0) -> ren183(x0) % 0.10/0.41 % 388:3:2:INP:TopTop: r1(x0,x1),ren182(x1) -> ren183(x0) % 0.10/0.41 % 389:2:2:INP:TopTop: -> r1(x0,x1),ren184(x0,x1) % 0.10/0.41 % 390:2:2:INP:TopTop: p2(x0) -> ren184(x1,x0) % 0.10/0.41 % 391:3:3:INP:TopTopTop: r1(x0,x1),ren183(x1) -> ren184(x2,x0) % 0.10/0.41 % 392:2:1:INP:Top: p2(x0) -> ren185(x0) % 0.10/0.41 % 393:3:2:INP:TopTop: r1(x0,x1),ren184(x1,skf21(x1)) -> ren185(x0) % 0.10/0.41 % 394:2:1:INP:Top: p2(x0) -> ren186(x0) % 0.10/0.41 % 395:3:2:INP:TopTop: r1(x0,x1),ren185(x1) -> ren186(x0) % 0.10/0.41 % 396:2:1:INP:Top: p2(x0) -> ren187(x0) % 0.10/0.41 % 397:3:2:INP:TopTop: r1(x0,x1),ren186(x1) -> ren187(x0) % 0.10/0.41 % 398:2:1:INP:Top: p2(x0) -> ren188(x0) % 0.10/0.41 % 399:3:2:INP:TopTop: r1(x0,x1),ren187(x1) -> ren188(x0) % 0.10/0.41 % 400:2:1:INP:Top: p2(x0) -> ren189(x0) % 0.10/0.41 % 401:3:2:INP:TopTop: r1(x0,x1),ren188(x1) -> ren189(x0) % 0.10/0.41 % 402:2:1:INP:Top: p2(x0) -> ren190(x0) % 0.10/0.41 % 403:3:2:INP:TopTop: r1(x0,x1),ren189(x1) -> ren190(x0) % 0.10/0.41 % 404:2:1:INP:Top: p2(x0) -> ren191(x0) % 0.10/0.41 % 405:3:2:INP:TopTop: r1(x0,x1),ren190(x1) -> ren191(x0) % 0.10/0.41 % 406:2:2:INP:TopTop: -> r1(x0,x1),ren192(x0,x1) % 0.10/0.41 % 407:2:2:INP:TopTop: p2(x0) -> ren192(x1,x0) % 0.10/0.41 % 408:3:3:INP:TopTopTop: r1(x0,x1),ren191(x1) -> ren192(x2,x0) % 0.10/0.41 % 409:2:1:INP:Top: p2(x0) -> ren193(x0) % 0.10/0.41 % 410:3:2:INP:TopTop: r1(x0,x1),ren192(x1,skf22(x1)) -> ren193(x0) % 0.10/0.41 % 411:2:1:INP:Top: p2(x0) -> ren194(x0) % 0.10/0.41 % 412:3:2:INP:TopTop: r1(x0,x1),ren193(x1) -> ren194(x0) % 0.10/0.41 % 413:2:1:INP:Top: p2(x0) -> ren195(x0) % 0.10/0.41 % 414:3:2:INP:TopTop: r1(x0,x1),ren194(x1) -> ren195(x0) % 0.10/0.41 % 415:2:1:INP:Top: p2(x0) -> ren196(x0) % 0.10/0.41 % 416:3:2:INP:TopTop: r1(x0,x1),ren195(x1) -> ren196(x0) % 0.10/0.41 % 417:2:1:INP:Top: p2(x0) -> ren197(x0) % 0.10/0.41 % 418:3:2:INP:TopTop: r1(x0,x1),ren196(x1) -> ren197(x0) % 0.10/0.41 % 419:2:1:INP:Top: p2(x0) -> ren198(x0) % 0.10/0.41 % 420:3:2:INP:TopTop: r1(x0,x1),ren197(x1) -> ren198(x0) % 0.10/0.41 % 421:2:1:INP:Top: p2(x0) -> ren199(x0) % 0.10/0.41 % 422:3:2:INP:TopTop: r1(x0,x1),ren198(x1) -> ren199(x0) % 0.10/0.41 % 423:2:2:INP:TopTop: -> r1(x0,x1),ren200(x0,x1) % 0.10/0.41 % 424:2:2:INP:TopTop: p2(x0) -> ren200(x1,x0) % 0.10/0.41 % 425:3:3:INP:TopTopTop: r1(x0,x1),ren199(x1) -> ren200(x2,x0) % 0.10/0.41 % 426:2:1:INP:Top: p2(x0) -> ren201(x0) % 0.10/0.41 % 427:3:2:INP:TopTop: r1(x0,x1),ren200(x1,skf23(x1)) -> ren201(x0) % 0.10/0.41 % 428:2:1:INP:Top: p2(x0) -> ren202(x0) % 0.10/0.41 % 429:3:2:INP:TopTop: r1(x0,x1),ren201(x1) -> ren202(x0) % 0.10/0.41 % 430:2:1:INP:Top: p2(x0) -> ren203(x0) % 0.10/0.41 % 431:3:2:INP:TopTop: r1(x0,x1),ren202(x1) -> ren203(x0) % 0.10/0.41 % 432:2:1:INP:Top: p2(x0) -> ren204(x0) % 0.10/0.41 % 433:3:2:INP:TopTop: r1(x0,x1),ren203(x1) -> ren204(x0) % 0.10/0.41 % 434:2:1:INP:Top: p2(x0) -> ren205(x0) % 0.10/0.41 % 435:3:2:INP:TopTop: r1(x0,x1),ren204(x1) -> ren205(x0) % 0.10/0.41 % 436:2:1:INP:Top: p2(x0) -> ren206(x0) % 0.10/0.41 % 437:3:2:INP:TopTop: r1(x0,x1),ren205(x1) -> ren206(x0) % 0.10/0.41 % 438:2:1:INP:Top: p2(x0) -> ren207(x0) % 0.10/0.41 % 439:3:2:INP:TopTop: r1(x0,x1),ren206(x1) -> ren207(x0) % 0.10/0.41 % 440:2:2:INP:TopTop: -> r1(x0,x1),ren208(x0,x1) % 0.10/0.41 % 441:2:2:INP:TopTop: p2(x0) -> ren208(x1,x0) % 0.10/0.41 % 442:3:3:INP:TopTopTop: r1(x0,x1),ren207(x1) -> ren208(x2,x0) % 0.10/0.41 % 443:2:1:INP:Top: p2(x0) -> ren209(x0) % 0.10/0.41 % 444:3:2:INP:TopTop: r1(x0,x1),ren208(x1,skf24(x1)) -> ren209(x0) % 0.10/0.41 % 445:2:1:INP:Top: p2(x0) -> ren210(x0) % 0.10/0.41 % 446:3:2:INP:TopTop: r1(x0,x1),ren209(x1) -> ren210(x0) % 0.10/0.41 % 447:2:1:INP:Top: p2(x0) -> ren211(x0) % 0.10/0.41 % 448:3:2:INP:TopTop: r1(x0,x1),ren210(x1) -> ren211(x0) % 0.10/0.41 % 449:2:1:INP:Top: p2(x0) -> ren212(x0) % 0.10/0.41 % 450:3:2:INP:TopTop: r1(x0,x1),ren211(x1) -> ren212(x0) % 0.10/0.41 % 451:2:1:INP:Top: p2(x0) -> ren213(x0) % 0.10/0.41 % 452:3:2:INP:TopTop: r1(x0,x1),ren212(x1) -> ren213(x0) % 0.10/0.41 % 453:2:1:INP:Top: p2(x0) -> ren214(x0) % 0.10/0.41 % 454:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren214(x0) % 0.10/0.41 % 455:2:1:INP:Top: p2(x0) -> ren215(x0) % 0.10/0.41 % 456:3:2:INP:TopTop: r1(x0,x1),ren214(x1) -> ren215(x0) % 0.10/0.41 % 457:2:1:INP:Top: p2(x0) -> ren216(x0) % 0.10/0.41 % 458:3:2:INP:TopTop: r1(x0,x1),ren215(x1) -> ren216(x0) % 0.10/0.41 % 459:2:1:INP:Top: p2(x0) -> ren217(x0) % 0.10/0.41 % 460:3:2:INP:TopTop: r1(x0,x1),ren216(x1) -> ren217(x0) % 0.10/0.41 % 461:2:1:INP:Top: p2(x0) -> ren218(x0) % 0.10/0.41 % 462:3:2:INP:TopTop: r1(x0,x1),ren217(x1) -> ren218(x0) % 0.10/0.41 % 463:2:1:INP:Top: p2(x0) -> ren219(x0) % 0.10/0.41 % 464:3:2:INP:TopTop: r1(x0,x1),ren218(x1) -> ren219(x0) % 0.10/0.41 % 465:2:1:INP:Top: p2(x0) -> ren220(x0) % 0.10/0.41 % 466:3:2:INP:TopTop: r1(x0,x1),ren219(x1) -> ren220(x0) % 0.10/0.41 % 467:2:1:INP:Top: p2(x0) -> ren221(x0) % 0.10/0.41 % 468:3:2:INP:TopTop: r1(x0,x1),ren220(x1) -> ren221(x0) % 0.10/0.41 % 469:2:2:INP:TopTop: -> r1(x0,x1),ren222(x0,x1) % 0.10/0.41 % 470:2:2:INP:TopTop: p2(x0) -> ren222(x1,x0) % 0.10/0.41 % 471:3:3:INP:TopTopTop: r1(x0,x1),ren221(x1) -> ren222(x2,x0) % 0.10/0.41 % 472:2:1:INP:Top: p2(x0) -> ren223(x0) % 0.10/0.41 % 473:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren222(x2,skf25(x2)) -> p1(x1),ren223(x0) % 0.10/0.41 % 474:2:1:INP:Top: p2(x0) -> ren224(x0) % 0.10/0.41 % 475:3:2:INP:TopTop: r1(x0,x1),ren223(x1) -> ren224(x0) % 0.10/0.41 % 476:2:1:INP:Top: p2(x0) -> ren225(x0) % 0.10/0.41 % 477:3:2:INP:TopTop: r1(x0,x1),ren224(x1) -> ren225(x0) % 0.10/0.41 % 478:2:1:INP:Top: p2(x0) -> ren226(x0) % 0.10/0.41 % 479:3:2:INP:TopTop: r1(x0,x1),ren225(x1) -> ren226(x0) % 0.10/0.41 % 480:2:1:INP:Top: p2(x0) -> ren227(x0) % 0.10/0.41 % 481:3:2:INP:TopTop: r1(x0,x1),ren226(x1) -> ren227(x0) % 0.10/0.41 % 482:2:1:INP:Top: p2(x0) -> ren228(x0) % 0.10/0.41 % 483:3:2:INP:TopTop: r1(x0,x1),ren227(x1) -> ren228(x0) % 0.10/0.41 % 484:2:1:INP:Top: p2(x0) -> ren229(x0) % 0.10/0.41 % 485:3:2:INP:TopTop: r1(x0,x1),ren228(x1) -> ren229(x0) % 0.10/0.41 % 486:2:2:INP:TopTop: -> r1(x0,x1),ren230(x0,x1) % 0.10/0.41 % 487:2:2:INP:TopTop: p2(x0) -> ren230(x1,x0) % 0.10/0.41 % 488:3:3:INP:TopTopTop: r1(x0,x1),ren229(x1) -> ren230(x2,x0) % 0.10/0.41 % 489:2:1:INP:Top: p2(x0) -> ren231(x0) % 0.10/0.41 % 490:3:2:INP:TopTop: r1(x0,x1),ren230(x1,skf26(x1)) -> ren231(x0) % 0.10/0.41 % 491:2:1:INP:Top: p2(x0) -> ren232(x0) % 0.10/0.41 % 492:3:2:INP:TopTop: r1(x0,x1),ren231(x1) -> ren232(x0) % 0.10/0.41 % 493:2:1:INP:Top: p2(x0) -> ren233(x0) % 0.10/0.41 % 494:3:2:INP:TopTop: r1(x0,x1),ren232(x1) -> ren233(x0) % 0.10/0.41 % 495:2:1:INP:Top: p2(x0) -> ren234(x0) % 0.10/0.41 % 496:3:2:INP:TopTop: r1(x0,x1),ren233(x1) -> ren234(x0) % 0.10/0.41 % 497:2:1:INP:Top: p2(x0) -> ren235(x0) % 0.10/0.41 % 498:3:2:INP:TopTop: r1(x0,x1),ren234(x1) -> ren235(x0) % 0.10/0.41 % 499:2:1:INP:Top: p2(x0) -> ren236(x0) % 0.10/0.41 % 500:3:2:INP:TopTop: r1(x0,x1),ren235(x1) -> ren236(x0) % 0.10/0.41 % 501:2:1:INP:Top: p2(x0) -> ren237(x0) % 0.10/0.41 % 502:3:2:INP:TopTop: r1(x0,x1),ren236(x1) -> ren237(x0) % 0.10/0.41 % 503:2:2:INP:TopTop: -> r1(x0,x1),ren238(x0,x1) % 0.10/0.41 % 504:2:2:INP:TopTop: p2(x0) -> ren238(x1,x0) % 0.10/0.41 % 505:3:3:INP:TopTopTop: r1(x0,x1),ren237(x1) -> ren238(x2,x0) % 0.10/0.41 % 506:2:1:INP:Top: p2(x0) -> ren239(x0) % 0.10/0.41 % 507:3:2:INP:TopTop: r1(x0,x1),ren238(x1,skf27(x1)) -> ren239(x0) % 0.10/0.41 % 508:2:1:INP:Top: p2(x0) -> ren240(x0) % 0.10/0.41 % 509:3:2:INP:TopTop: r1(x0,x1),ren239(x1) -> ren240(x0) % 0.10/0.41 % 510:2:1:INP:Top: p2(x0) -> ren241(x0) % 0.10/0.41 % 511:3:2:INP:TopTop: r1(x0,x1),ren240(x1) -> ren241(x0) % 0.10/0.41 % 512:2:1:INP:Top: p2(x0) -> ren242(x0) % 0.10/0.41 % 513:3:2:INP:TopTop: r1(x0,x1),ren241(x1) -> ren242(x0) % 0.10/0.41 % 514:2:1:INP:Top: p2(x0) -> ren243(x0) % 0.10/0.41 % 515:3:2:INP:TopTop: r1(x0,x1),ren242(x1) -> ren243(x0) % 0.10/0.41 % 516:2:1:INP:Top: p2(x0) -> ren244(x0) % 0.10/0.41 % 517:3:2:INP:TopTop: r1(x0,x1),ren243(x1) -> ren244(x0) % 0.10/0.41 % 518:2:1:INP:Top: p2(x0) -> ren245(x0) % 0.10/0.41 % 519:3:2:INP:TopTop: r1(x0,x1),ren244(x1) -> ren245(x0) % 0.10/0.41 % 520:2:2:INP:TopTop: -> r1(x0,x1),ren246(x0,x1) % 0.10/0.41 % 521:2:2:INP:TopTop: p2(x0) -> ren246(x1,x0) % 0.10/0.41 % 522:3:3:INP:TopTopTop: r1(x0,x1),ren245(x1) -> ren246(x2,x0) % 0.10/0.41 % 523:2:1:INP:Top: p2(x0) -> ren247(x0) % 0.10/0.41 % 524:3:2:INP:TopTop: r1(x0,x1),ren246(x1,skf28(x1)) -> ren247(x0) % 0.10/0.41 % 525:2:1:INP:Top: p2(x0) -> ren248(x0) % 0.10/0.41 % 526:3:2:INP:TopTop: r1(x0,x1),ren247(x1) -> ren248(x0) % 0.10/0.41 % 527:2:1:INP:Top: p2(x0) -> ren249(x0) % 0.10/0.41 % 528:3:2:INP:TopTop: r1(x0,x1),ren248(x1) -> ren249(x0) % 0.10/0.41 % 529:2:1:INP:Top: p2(x0) -> ren250(x0) % 0.10/0.41 % 530:3:2:INP:TopTop: r1(x0,x1),ren249(x1) -> ren250(x0) % 0.10/0.41 % 531:2:1:INP:Top: p2(x0) -> ren251(x0) % 0.10/0.41 % 532:3:2:INP:TopTop: r1(x0,x1),ren250(x1) -> ren251(x0) % 0.10/0.41 % 533:2:1:INP:Top: p2(x0) -> ren252(x0) % 0.10/0.41 % 534:3:2:INP:TopTop: r1(x0,x1),ren251(x1) -> ren252(x0) % 0.10/0.41 % 535:2:1:INP:Top: p2(x0) -> ren253(x0) % 0.10/0.41 % 536:3:2:INP:TopTop: r1(x0,x1),ren252(x1) -> ren253(x0) % 0.10/0.41 % 537:2:2:INP:TopTop: -> r1(x0,x1),ren254(x0,x1) % 0.10/0.41 % 538:2:2:INP:TopTop: p2(x0) -> ren254(x1,x0) % 0.10/0.41 % 539:3:3:INP:TopTopTop: r1(x0,x1),ren253(x1) -> ren254(x2,x0) % 0.10/0.41 % 540:2:1:INP:Top: p2(x0) -> ren255(x0) % 0.10/0.41 % 541:3:2:INP:TopTop: r1(x0,x1),ren254(x1,skf29(x1)) -> ren255(x0) % 0.10/0.41 % 542:2:1:INP:Top: p2(x0) -> ren256(x0) % 0.10/0.41 % 543:3:2:INP:TopTop: r1(x0,x1),ren255(x1) -> ren256(x0) % 0.10/0.41 % 544:2:1:INP:Top: p2(x0) -> ren257(x0) % 0.10/0.41 % 545:3:2:INP:TopTop: r1(x0,x1),ren256(x1) -> ren257(x0) % 0.10/0.41 % 546:2:1:INP:Top: p2(x0) -> ren258(x0) % 0.10/0.41 % 547:3:2:INP:TopTop: r1(x0,x1),ren257(x1) -> ren258(x0) % 0.10/0.41 % 548:2:1:INP:Top: p2(x0) -> ren259(x0) % 0.10/0.41 % 549:3:2:INP:TopTop: r1(x0,x1),ren258(x1) -> ren259(x0) % 0.10/0.41 % 550:2:1:INP:Top: p2(x0) -> ren260(x0) % 0.10/0.41 % 551:3:2:INP:TopTop: r1(x0,x1),ren259(x1) -> ren260(x0) % 0.10/0.41 % 552:2:1:INP:Top: p2(x0) -> ren261(x0) % 0.10/0.41 % 553:3:2:INP:TopTop: r1(x0,x1),ren260(x1) -> ren261(x0) % 0.10/0.41 % 554:2:2:INP:TopTop: -> r1(x0,x1),ren262(x0,x1) % 0.10/0.41 % 555:2:2:INP:TopTop: p2(x0) -> ren262(x1,x0) % 0.10/0.41 % 556:3:3:INP:TopTopTop: r1(x0,x1),ren261(x1) -> ren262(x2,x0) % 0.10/0.41 % 557:2:1:INP:Top: p2(x0) -> ren263(x0) % 0.10/0.41 % 558:3:2:INP:TopTop: r1(x0,x1),ren262(x1,skf30(x1)) -> ren263(x0) % 0.10/0.41 % 559:2:1:INP:Top: p2(x0) -> ren264(x0) % 0.10/0.41 % 560:3:2:INP:TopTop: r1(x0,x1),ren263(x1) -> ren264(x0) % 0.10/0.41 % 561:2:1:INP:Top: p2(x0) -> ren265(x0) % 0.10/0.41 % 562:3:2:INP:TopTop: r1(x0,x1),ren264(x1) -> ren265(x0) % 0.10/0.41 % 563:2:1:INP:Top: p2(x0) -> ren266(x0) % 0.10/0.41 % 564:3:2:INP:TopTop: r1(x0,x1),ren265(x1) -> ren266(x0) % 0.10/0.41 % 565:2:1:INP:Top: p2(x0) -> ren267(x0) % 0.10/0.41 % 566:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren267(x0) % 0.10/0.41 % 567:2:1:INP:Top: p2(x0) -> ren268(x0) % 0.10/0.41 % 568:3:2:INP:TopTop: r1(x0,x1),ren267(x1) -> ren268(x0) % 0.10/0.41 % 569:2:1:INP:Top: p2(x0) -> ren269(x0) % 0.10/0.41 % 570:3:2:INP:TopTop: r1(x0,x1),ren268(x1) -> ren269(x0) % 0.10/0.41 % 571:2:1:INP:Top: p2(x0) -> ren270(x0) % 0.10/0.41 % 572:3:2:INP:TopTop: r1(x0,x1),ren269(x1) -> ren270(x0) % 0.10/0.41 % 573:2:1:INP:Top: p2(x0) -> ren271(x0) % 0.10/0.41 % 574:3:2:INP:TopTop: r1(x0,x1),ren270(x1) -> ren271(x0) % 0.10/0.41 % 575:2:1:INP:Top: p2(x0) -> ren272(x0) % 0.10/0.41 % 576:3:2:INP:TopTop: r1(x0,x1),ren271(x1) -> ren272(x0) % 0.10/0.41 % 577:2:1:INP:Top: p2(x0) -> ren273(x0) % 0.10/0.41 % 578:3:2:INP:TopTop: r1(x0,x1),ren272(x1) -> ren273(x0) % 0.10/0.41 % 579:2:1:INP:Top: p2(x0) -> ren274(x0) % 0.10/0.41 % 580:3:2:INP:TopTop: r1(x0,x1),ren273(x1) -> ren274(x0) % 0.10/0.41 % 581:2:2:INP:TopTop: -> r1(x0,x1),ren275(x0,x1) % 0.10/0.41 % 582:2:2:INP:TopTop: p2(x0) -> ren275(x1,x0) % 0.10/0.41 % 583:3:3:INP:TopTopTop: r1(x0,x1),ren274(x1) -> ren275(x2,x0) % 0.10/0.41 % 584:2:1:INP:Top: p2(x0) -> ren276(x0) % 0.10/0.41 % 585:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren275(x2,skf31(x2)) -> p1(x1),ren276(x0) % 0.10/0.41 % 586:2:1:INP:Top: p2(x0) -> ren277(x0) % 0.10/0.41 % 587:3:2:INP:TopTop: r1(x0,x1),ren276(x1) -> ren277(x0) % 0.10/0.41 % 588:2:1:INP:Top: p2(x0) -> ren278(x0) % 0.10/0.41 % 589:3:2:INP:TopTop: r1(x0,x1),ren277(x1) -> ren278(x0) % 0.10/0.41 % 590:2:1:INP:Top: p2(x0) -> ren279(x0) % 0.10/0.41 % 591:3:2:INP:TopTop: r1(x0,x1),ren278(x1) -> ren279(x0) % 0.10/0.41 % 592:2:1:INP:Top: p2(x0) -> ren280(x0) % 0.10/0.41 % 593:3:2:INP:TopTop: r1(x0,x1),ren279(x1) -> ren280(x0) % 0.10/0.41 % 594:2:1:INP:Top: p2(x0) -> ren281(x0) % 0.10/0.41 % 595:3:2:INP:TopTop: r1(x0,x1),ren280(x1) -> ren281(x0) % 0.10/0.41 % 596:2:1:INP:Top: p2(x0) -> ren282(x0) % 0.10/0.41 % 597:3:2:INP:TopTop: r1(x0,x1),ren281(x1) -> ren282(x0) % 0.10/0.41 % 598:2:2:INP:TopTop: -> r1(x0,x1),ren283(x0,x1) % 0.10/0.41 % 599:2:2:INP:TopTop: p2(x0) -> ren283(x1,x0) % 0.10/0.41 % 600:3:3:INP:TopTopTop: r1(x0,x1),ren282(x1) -> ren283(x2,x0) % 0.10/0.41 % 601:2:1:INP:Top: p2(x0) -> ren284(x0) % 0.10/0.41 % 602:3:2:INP:TopTop: r1(x0,x1),ren283(x1,skf32(x1)) -> ren284(x0) % 0.10/0.41 % 603:2:1:INP:Top: p2(x0) -> ren285(x0) % 0.10/0.41 % 604:3:2:INP:TopTop: r1(x0,x1),ren284(x1) -> ren285(x0) % 0.10/0.41 % 605:2:1:INP:Top: p2(x0) -> ren286(x0) % 0.10/0.41 % 606:3:2:INP:TopTop: r1(x0,x1),ren285(x1) -> ren286(x0) % 0.10/0.41 % 607:2:1:INP:Top: p2(x0) -> ren287(x0) % 0.10/0.41 % 608:3:2:INP:TopTop: r1(x0,x1),ren286(x1) -> ren287(x0) % 0.10/0.41 % 609:2:1:INP:Top: p2(x0) -> ren288(x0) % 0.10/0.41 % 610:3:2:INP:TopTop: r1(x0,x1),ren287(x1) -> ren288(x0) % 0.10/0.41 % 611:2:1:INP:Top: p2(x0) -> ren289(x0) % 0.10/0.41 % 612:3:2:INP:TopTop: r1(x0,x1),ren288(x1) -> ren289(x0) % 0.10/0.41 % 613:2:1:INP:Top: p2(x0) -> ren290(x0) % 0.10/0.41 % 614:3:2:INP:TopTop: r1(x0,x1),ren289(x1) -> ren290(x0) % 0.10/0.41 % 615:2:2:INP:TopTop: -> r1(x0,x1),ren291(x0,x1) % 0.10/0.41 % 616:2:2:INP:TopTop: p2(x0) -> ren291(x1,x0) % 0.10/0.41 % 617:3:3:INP:TopTopTop: r1(x0,x1),ren290(x1) -> ren291(x2,x0) % 0.10/0.41 % 618:2:1:INP:Top: p2(x0) -> ren292(x0) % 0.10/0.41 % 619:3:2:INP:TopTop: r1(x0,x1),ren291(x1,skf33(x1)) -> ren292(x0) % 0.10/0.41 % 620:2:1:INP:Top: p2(x0) -> ren293(x0) % 0.10/0.41 % 621:3:2:INP:TopTop: r1(x0,x1),ren292(x1) -> ren293(x0) % 0.10/0.41 % 622:2:1:INP:Top: p2(x0) -> ren294(x0) % 0.10/0.41 % 623:3:2:INP:TopTop: r1(x0,x1),ren293(x1) -> ren294(x0) % 0.10/0.41 % 624:2:1:INP:Top: p2(x0) -> ren295(x0) % 0.10/0.41 % 625:3:2:INP:TopTop: r1(x0,x1),ren294(x1) -> ren295(x0) % 0.10/0.41 % 626:2:1:INP:Top: p2(x0) -> ren296(x0) % 0.10/0.41 % 627:3:2:INP:TopTop: r1(x0,x1),ren295(x1) -> ren296(x0) % 0.10/0.41 % 628:2:1:INP:Top: p2(x0) -> ren297(x0) % 0.10/0.41 % 629:3:2:INP:TopTop: r1(x0,x1),ren296(x1) -> ren297(x0) % 0.10/0.41 % 630:2:1:INP:Top: p2(x0) -> ren298(x0) % 0.10/0.41 % 631:3:2:INP:TopTop: r1(x0,x1),ren297(x1) -> ren298(x0) % 0.10/0.41 % 632:2:2:INP:TopTop: -> r1(x0,x1),ren299(x0,x1) % 0.10/0.41 % 633:2:2:INP:TopTop: p2(x0) -> ren299(x1,x0) % 0.10/0.41 % 634:3:3:INP:TopTopTop: r1(x0,x1),ren298(x1) -> ren299(x2,x0) % 0.10/0.41 % 635:2:1:INP:Top: p2(x0) -> ren300(x0) % 0.10/0.41 % 636:3:2:INP:TopTop: r1(x0,x1),ren299(x1,skf34(x1)) -> ren300(x0) % 0.10/0.41 % 637:2:1:INP:Top: p2(x0) -> ren301(x0) % 0.10/0.41 % 638:3:2:INP:TopTop: r1(x0,x1),ren300(x1) -> ren301(x0) % 0.10/0.41 % 639:2:1:INP:Top: p2(x0) -> ren302(x0) % 0.10/0.41 % 640:3:2:INP:TopTop: r1(x0,x1),ren301(x1) -> ren302(x0) % 0.10/0.41 % 641:2:1:INP:Top: p2(x0) -> ren303(x0) % 0.10/0.41 % 642:3:2:INP:TopTop: r1(x0,x1),ren302(x1) -> ren303(x0) % 0.10/0.41 % 643:2:1:INP:Top: p2(x0) -> ren304(x0) % 0.10/0.41 % 644:3:2:INP:TopTop: r1(x0,x1),ren303(x1) -> ren304(x0) % 0.10/0.41 % 645:2:1:INP:Top: p2(x0) -> ren305(x0) % 0.10/0.41 % 646:3:2:INP:TopTop: r1(x0,x1),ren304(x1) -> ren305(x0) % 0.10/0.41 % 647:2:1:INP:Top: p2(x0) -> ren306(x0) % 0.10/0.41 % 648:3:2:INP:TopTop: r1(x0,x1),ren305(x1) -> ren306(x0) % 0.10/0.41 % 649:2:2:INP:TopTop: -> r1(x0,x1),ren307(x0,x1) % 0.10/0.41 % 650:2:2:INP:TopTop: p2(x0) -> ren307(x1,x0) % 0.10/0.41 % 651:3:3:INP:TopTopTop: r1(x0,x1),ren306(x1) -> ren307(x2,x0) % 0.10/0.41 % 652:2:1:INP:Top: p2(x0) -> ren308(x0) % 0.10/0.41 % 653:3:2:INP:TopTop: r1(x0,x1),ren307(x1,skf35(x1)) -> ren308(x0) % 0.10/0.41 % 654:2:1:INP:Top: p2(x0) -> ren309(x0) % 0.10/0.41 % 655:3:2:INP:TopTop: r1(x0,x1),ren308(x1) -> ren309(x0) % 0.10/0.41 % 656:2:1:INP:Top: p2(x0) -> ren310(x0) % 0.10/0.41 % 657:3:2:INP:TopTop: r1(x0,x1),ren309(x1) -> ren310(x0) % 0.10/0.41 % 658:2:1:INP:Top: p2(x0) -> ren311(x0) % 0.10/0.41 % 659:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren311(x0) % 0.10/0.41 % 660:2:1:INP:Top: p2(x0) -> ren312(x0) % 0.10/0.41 % 661:3:2:INP:TopTop: r1(x0,x1),ren311(x1) -> ren312(x0) % 0.10/0.41 % 662:2:1:INP:Top: p2(x0) -> ren313(x0) % 0.10/0.41 % 663:3:2:INP:TopTop: r1(x0,x1),ren312(x1) -> ren313(x0) % 0.10/0.41 % 664:2:1:INP:Top: p2(x0) -> ren314(x0) % 0.10/0.41 % 665:3:2:INP:TopTop: r1(x0,x1),ren313(x1) -> ren314(x0) % 0.10/0.41 % 666:2:1:INP:Top: p2(x0) -> ren315(x0) % 0.10/0.41 % 667:3:2:INP:TopTop: r1(x0,x1),ren314(x1) -> ren315(x0) % 0.10/0.41 % 668:2:1:INP:Top: p2(x0) -> ren316(x0) % 0.10/0.41 % 669:3:2:INP:TopTop: r1(x0,x1),ren315(x1) -> ren316(x0) % 0.10/0.41 % 670:2:1:INP:Top: p2(x0) -> ren317(x0) % 0.10/0.41 % 671:3:2:INP:TopTop: r1(x0,x1),ren316(x1) -> ren317(x0) % 0.10/0.41 % 672:2:1:INP:Top: p2(x0) -> ren318(x0) % 0.10/0.41 % 673:3:2:INP:TopTop: r1(x0,x1),ren317(x1) -> ren318(x0) % 0.10/0.41 % 674:2:2:INP:TopTop: -> r1(x0,x1),ren319(x0,x1) % 0.10/0.41 % 675:2:2:INP:TopTop: p2(x0) -> ren319(x1,x0) % 0.10/0.41 % 676:3:3:INP:TopTopTop: r1(x0,x1),ren318(x1) -> ren319(x2,x0) % 0.10/0.41 % 677:2:1:INP:Top: p2(x0) -> ren320(x0) % 0.10/0.41 % 678:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren319(x2,skf36(x2)) -> p1(x1),ren320(x0) % 0.10/0.41 % 679:2:1:INP:Top: p2(x0) -> ren321(x0) % 0.10/0.41 % 680:3:2:INP:TopTop: r1(x0,x1),ren320(x1) -> ren321(x0) % 0.10/0.41 % 681:2:1:INP:Top: p2(x0) -> ren322(x0) % 0.10/0.41 % 682:3:2:INP:TopTop: r1(x0,x1),ren321(x1) -> ren322(x0) % 0.10/0.41 % 683:2:1:INP:Top: p2(x0) -> ren323(x0) % 0.10/0.41 % 684:3:2:INP:TopTop: r1(x0,x1),ren322(x1) -> ren323(x0) % 0.10/0.41 % 685:2:1:INP:Top: p2(x0) -> ren324(x0) % 0.10/0.41 % 686:3:2:INP:TopTop: r1(x0,x1),ren323(x1) -> ren324(x0) % 0.10/0.41 % 687:2:1:INP:Top: p2(x0) -> ren325(x0) % 0.10/0.41 % 688:3:2:INP:TopTop: r1(x0,x1),ren324(x1) -> ren325(x0) % 0.10/0.41 % 689:2:1:INP:Top: p2(x0) -> ren326(x0) % 0.10/0.41 % 690:3:2:INP:TopTop: r1(x0,x1),ren325(x1) -> ren326(x0) % 0.10/0.41 % 691:2:2:INP:TopTop: -> r1(x0,x1),ren327(x0,x1) % 0.10/0.41 % 692:2:2:INP:TopTop: p2(x0) -> ren327(x1,x0) % 0.10/0.41 % 693:3:3:INP:TopTopTop: r1(x0,x1),ren326(x1) -> ren327(x2,x0) % 0.10/0.41 % 694:2:1:INP:Top: p2(x0) -> ren328(x0) % 0.10/0.41 % 695:3:2:INP:TopTop: r1(x0,x1),ren327(x1,skf37(x1)) -> ren328(x0) % 0.10/0.41 % 696:2:1:INP:Top: p2(x0) -> ren329(x0) % 0.10/0.41 % 697:3:2:INP:TopTop: r1(x0,x1),ren328(x1) -> ren329(x0) % 0.10/0.41 % 698:2:1:INP:Top: p2(x0) -> ren330(x0) % 0.10/0.41 % 699:3:2:INP:TopTop: r1(x0,x1),ren329(x1) -> ren330(x0) % 0.10/0.41 % 700:2:1:INP:Top: p2(x0) -> ren331(x0) % 0.10/0.41 % 701:3:2:INP:TopTop: r1(x0,x1),ren330(x1) -> ren331(x0) % 0.10/0.41 % 702:2:1:INP:Top: p2(x0) -> ren332(x0) % 0.10/0.41 % 703:3:2:INP:TopTop: r1(x0,x1),ren331(x1) -> ren332(x0) % 0.10/0.41 % 704:2:1:INP:Top: p2(x0) -> ren333(x0) % 0.10/0.41 % 705:3:2:INP:TopTop: r1(x0,x1),ren332(x1) -> ren333(x0) % 0.10/0.41 % 706:2:1:INP:Top: p2(x0) -> ren334(x0) % 0.10/0.41 % 707:3:2:INP:TopTop: r1(x0,x1),ren333(x1) -> ren334(x0) % 0.10/0.41 % 708:2:2:INP:TopTop: -> r1(x0,x1),ren335(x0,x1) % 0.10/0.41 % 709:2:2:INP:TopTop: p2(x0) -> ren335(x1,x0) % 0.10/0.41 % 710:3:3:INP:TopTopTop: r1(x0,x1),ren334(x1) -> ren335(x2,x0) % 0.10/0.41 % 711:2:1:INP:Top: p2(x0) -> ren336(x0) % 0.10/0.41 % 712:3:2:INP:TopTop: r1(x0,x1),ren335(x1,skf38(x1)) -> ren336(x0) % 0.10/0.41 % 713:2:1:INP:Top: p2(x0) -> ren337(x0) % 0.10/0.41 % 714:3:2:INP:TopTop: r1(x0,x1),ren336(x1) -> ren337(x0) % 0.10/0.41 % 715:2:1:INP:Top: p2(x0) -> ren338(x0) % 0.10/0.41 % 716:3:2:INP:TopTop: r1(x0,x1),ren337(x1) -> ren338(x0) % 0.10/0.41 % 717:2:1:INP:Top: p2(x0) -> ren339(x0) % 0.10/0.41 % 718:3:2:INP:TopTop: r1(x0,x1),ren338(x1) -> ren339(x0) % 0.10/0.41 % 719:2:1:INP:Top: p2(x0) -> ren340(x0) % 0.10/0.41 % 720:3:2:INP:TopTop: r1(x0,x1),ren339(x1) -> ren340(x0) % 0.10/0.41 % 721:2:1:INP:Top: p2(x0) -> ren341(x0) % 0.10/0.41 % 722:3:2:INP:TopTop: r1(x0,x1),ren340(x1) -> ren341(x0) % 0.10/0.41 % 723:2:1:INP:Top: p2(x0) -> ren342(x0) % 0.10/0.41 % 724:3:2:INP:TopTop: r1(x0,x1),ren341(x1) -> ren342(x0) % 0.10/0.41 % 725:2:2:INP:TopTop: -> r1(x0,x1),ren343(x0,x1) % 0.10/0.41 % 726:2:2:INP:TopTop: p2(x0) -> ren343(x1,x0) % 0.10/0.41 % 727:3:3:INP:TopTopTop: r1(x0,x1),ren342(x1) -> ren343(x2,x0) % 0.10/0.41 % 728:2:1:INP:Top: p2(x0) -> ren344(x0) % 0.10/0.41 % 729:3:2:INP:TopTop: r1(x0,x1),ren343(x1,skf39(x1)) -> ren344(x0) % 0.10/0.41 % 730:2:1:INP:Top: p2(x0) -> ren345(x0) % 0.10/0.41 % 731:3:2:INP:TopTop: r1(x0,x1),ren344(x1) -> ren345(x0) % 0.10/0.41 % 732:2:1:INP:Top: p2(x0) -> ren346(x0) % 0.10/0.41 % 733:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren346(x0) % 0.10/0.41 % 734:2:1:INP:Top: p2(x0) -> ren347(x0) % 0.10/0.41 % 735:3:2:INP:TopTop: r1(x0,x1),ren346(x1) -> ren347(x0) % 0.10/0.41 % 736:2:1:INP:Top: p2(x0) -> ren348(x0) % 0.10/0.41 % 737:3:2:INP:TopTop: r1(x0,x1),ren347(x1) -> ren348(x0) % 0.10/0.41 % 738:2:1:INP:Top: p2(x0) -> ren349(x0) % 0.10/0.41 % 739:3:2:INP:TopTop: r1(x0,x1),ren348(x1) -> ren349(x0) % 0.10/0.41 % 740:2:1:INP:Top: p2(x0) -> ren350(x0) % 0.10/0.41 % 741:3:2:INP:TopTop: r1(x0,x1),ren349(x1) -> ren350(x0) % 0.10/0.41 % 742:2:1:INP:Top: p2(x0) -> ren351(x0) % 0.10/0.41 % 743:3:2:INP:TopTop: r1(x0,x1),ren350(x1) -> ren351(x0) % 0.10/0.41 % 744:2:1:INP:Top: p2(x0) -> ren352(x0) % 0.10/0.41 % 745:3:2:INP:TopTop: r1(x0,x1),ren351(x1) -> ren352(x0) % 0.10/0.41 % 746:2:1:INP:Top: p2(x0) -> ren353(x0) % 0.10/0.41 % 747:3:2:INP:TopTop: r1(x0,x1),ren352(x1) -> ren353(x0) % 0.10/0.41 % 748:2:2:INP:TopTop: -> r1(x0,x1),ren354(x0,x1) % 0.10/0.41 % 749:2:2:INP:TopTop: p2(x0) -> ren354(x1,x0) % 0.10/0.41 % 750:3:3:INP:TopTopTop: r1(x0,x1),ren353(x1) -> ren354(x2,x0) % 0.10/0.41 % 751:2:1:INP:Top: p2(x0) -> ren355(x0) % 0.10/0.41 % 752:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren354(x2,skf40(x2)) -> p1(x1),ren355(x0) % 0.10/0.41 % 753:2:1:INP:Top: p2(x0) -> ren356(x0) % 0.10/0.41 % 754:3:2:INP:TopTop: r1(x0,x1),ren355(x1) -> ren356(x0) % 0.10/0.41 % 755:2:1:INP:Top: p2(x0) -> ren357(x0) % 0.10/0.41 % 756:3:2:INP:TopTop: r1(x0,x1),ren356(x1) -> ren357(x0) % 0.10/0.41 % 757:2:1:INP:Top: p2(x0) -> ren358(x0) % 0.10/0.41 % 758:3:2:INP:TopTop: r1(x0,x1),ren357(x1) -> ren358(x0) % 0.10/0.41 % 759:2:1:INP:Top: p2(x0) -> ren359(x0) % 0.10/0.41 % 760:3:2:INP:TopTop: r1(x0,x1),ren358(x1) -> ren359(x0) % 0.10/0.41 % 761:2:1:INP:Top: p2(x0) -> ren360(x0) % 0.10/0.41 % 762:3:2:INP:TopTop: r1(x0,x1),ren359(x1) -> ren360(x0) % 0.10/0.41 % 763:2:1:INP:Top: p2(x0) -> ren361(x0) % 0.10/0.41 % 764:3:2:INP:TopTop: r1(x0,x1),ren360(x1) -> ren361(x0) % 0.10/0.41 % 765:2:2:INP:TopTop: -> r1(x0,x1),ren362(x0,x1) % 0.10/0.41 % 766:2:2:INP:TopTop: p2(x0) -> ren362(x1,x0) % 0.10/0.41 % 767:3:3:INP:TopTopTop: r1(x0,x1),ren361(x1) -> ren362(x2,x0) % 0.10/0.41 % 768:2:1:INP:Top: p2(x0) -> ren363(x0) % 0.10/0.41 % 769:3:2:INP:TopTop: r1(x0,x1),ren362(x1,skf41(x1)) -> ren363(x0) % 0.10/0.41 % 770:2:1:INP:Top: p2(x0) -> ren364(x0) % 0.10/0.41 % 771:3:2:INP:TopTop: r1(x0,x1),ren363(x1) -> ren364(x0) % 0.10/0.41 % 772:2:1:INP:Top: p2(x0) -> ren365(x0) % 0.10/0.41 % 773:3:2:INP:TopTop: r1(x0,x1),ren364(x1) -> ren365(x0) % 0.10/0.41 % 774:2:1:INP:Top: p2(x0) -> ren366(x0) % 0.10/0.41 % 775:3:2:INP:TopTop: r1(x0,x1),ren365(x1) -> ren366(x0) % 0.10/0.41 % 776:2:1:INP:Top: p2(x0) -> ren367(x0) % 0.10/0.41 % 777:3:2:INP:TopTop: r1(x0,x1),ren366(x1) -> ren367(x0) % 0.10/0.41 % 778:2:1:INP:Top: p2(x0) -> ren368(x0) % 0.10/0.41 % 779:3:2:INP:TopTop: r1(x0,x1),ren367(x1) -> ren368(x0) % 0.10/0.41 % 780:2:1:INP:Top: p2(x0) -> ren369(x0) % 0.10/0.41 % 781:3:2:INP:TopTop: r1(x0,x1),ren368(x1) -> ren369(x0) % 0.10/0.41 % 782:2:2:INP:TopTop: -> r1(x0,x1),ren370(x0,x1) % 0.10/0.41 % 783:2:2:INP:TopTop: p2(x0) -> ren370(x1,x0) % 0.10/0.41 % 784:3:3:INP:TopTopTop: r1(x0,x1),ren369(x1) -> ren370(x2,x0) % 0.10/0.41 % 785:2:1:INP:Top: p2(x0) -> ren371(x0) % 0.10/0.41 % 786:3:2:INP:TopTop: r1(x0,x1),ren370(x1,skf42(x1)) -> ren371(x0) % 0.10/0.41 % 787:2:1:INP:Top: p2(x0) -> ren372(x0) % 0.10/0.41 % 788:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren372(x0) % 0.10/0.41 % 789:2:1:INP:Top: p2(x0) -> ren373(x0) % 0.10/0.41 % 790:3:2:INP:TopTop: r1(x0,x1),ren372(x1) -> ren373(x0) % 0.10/0.41 % 791:2:1:INP:Top: p2(x0) -> ren374(x0) % 0.10/0.41 % 792:3:2:INP:TopTop: r1(x0,x1),ren373(x1) -> ren374(x0) % 0.10/0.41 % 793:2:1:INP:Top: p2(x0) -> ren375(x0) % 0.10/0.41 % 794:3:2:INP:TopTop: r1(x0,x1),ren374(x1) -> ren375(x0) % 0.10/0.41 % 795:2:1:INP:Top: p2(x0) -> ren376(x0) % 0.10/0.41 % 796:3:2:INP:TopTop: r1(x0,x1),ren375(x1) -> ren376(x0) % 0.10/0.41 % 797:2:1:INP:Top: p2(x0) -> ren377(x0) % 0.10/0.41 % 798:3:2:INP:TopTop: r1(x0,x1),ren376(x1) -> ren377(x0) % 0.10/0.41 % 799:2:1:INP:Top: p2(x0) -> ren378(x0) % 0.10/0.41 % 800:3:2:INP:TopTop: r1(x0,x1),ren377(x1) -> ren378(x0) % 0.10/0.41 % 801:2:1:INP:Top: p2(x0) -> ren379(x0) % 0.10/0.41 % 802:3:2:INP:TopTop: r1(x0,x1),ren378(x1) -> ren379(x0) % 0.10/0.41 % 803:2:2:INP:TopTop: -> r1(x0,x1),ren380(x0,x1) % 0.10/0.41 % 804:2:2:INP:TopTop: p2(x0) -> ren380(x1,x0) % 0.10/0.41 % 805:3:3:INP:TopTopTop: r1(x0,x1),ren379(x1) -> ren380(x2,x0) % 0.10/0.41 % 806:2:1:INP:Top: p2(x0) -> ren381(x0) % 0.10/0.41 % 807:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren380(x2,skf43(x2)) -> p1(x1),ren381(x0) % 0.10/0.41 % 808:2:1:INP:Top: p2(x0) -> ren382(x0) % 0.10/0.41 % 809:3:2:INP:TopTop: r1(x0,x1),ren381(x1) -> ren382(x0) % 0.10/0.41 % 810:2:1:INP:Top: p2(x0) -> ren383(x0) % 0.10/0.41 % 811:3:2:INP:TopTop: r1(x0,x1),ren382(x1) -> ren383(x0) % 0.10/0.41 % 812:2:1:INP:Top: p2(x0) -> ren384(x0) % 0.10/0.41 % 813:3:2:INP:TopTop: r1(x0,x1),ren383(x1) -> ren384(x0) % 0.10/0.41 % 814:2:1:INP:Top: p2(x0) -> ren385(x0) % 0.10/0.41 % 815:3:2:INP:TopTop: r1(x0,x1),ren384(x1) -> ren385(x0) % 0.10/0.41 % 816:2:1:INP:Top: p2(x0) -> ren386(x0) % 0.10/0.41 % 817:3:2:INP:TopTop: r1(x0,x1),ren385(x1) -> ren386(x0) % 0.10/0.41 % 818:2:1:INP:Top: p2(x0) -> ren387(x0) % 0.10/0.41 % 819:3:2:INP:TopTop: r1(x0,x1),ren386(x1) -> ren387(x0) % 0.10/0.41 % 820:2:2:INP:TopTop: -> r1(x0,x1),ren388(x0,x1) % 0.10/0.41 % 821:2:2:INP:TopTop: p2(x0) -> ren388(x1,x0) % 0.10/0.41 % 822:3:3:INP:TopTopTop: r1(x0,x1),ren387(x1) -> ren388(x2,x0) % 0.10/0.41 % 823:2:1:INP:Top: p2(x0) -> ren389(x0) % 0.10/0.41 % 824:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren389(x0) % 0.10/0.41 % 825:2:1:INP:Top: p2(x0) -> ren390(x0) % 0.10/0.41 % 826:3:2:INP:TopTop: r1(x0,x1),ren389(x1) -> ren390(x0) % 0.10/0.41 % 827:2:1:INP:Top: p2(x0) -> ren391(x0) % 0.10/0.41 % 828:3:2:INP:TopTop: r1(x0,x1),ren390(x1) -> ren391(x0) % 0.10/0.41 % 829:2:1:INP:Top: p2(x0) -> ren392(x0) % 0.10/0.41 % 830:3:2:INP:TopTop: r1(x0,x1),ren391(x1) -> ren392(x0) % 0.10/0.41 % 831:2:1:INP:Top: p2(x0) -> ren393(x0) % 0.10/0.41 % 832:3:2:INP:TopTop: r1(x0,x1),ren392(x1) -> ren393(x0) % 0.10/0.41 % 833:2:1:INP:Top: p2(x0) -> ren394(x0) % 0.10/0.41 % 834:3:2:INP:TopTop: r1(x0,x1),ren393(x1) -> ren394(x0) % 0.10/0.41 % 835:2:1:INP:Top: p2(x0) -> ren395(x0) % 0.10/0.41 % 836:3:2:INP:TopTop: r1(x0,x1),ren394(x1) -> ren395(x0) % 0.10/0.41 % 837:2:1:INP:Top: p2(x0) -> ren396(x0) % 0.10/0.41 % 838:3:2:INP:TopTop: r1(x0,x1),ren395(x1) -> ren396(x0) % 0.10/0.41 % 839:2:2:INP:TopTop: -> r1(x0,x1),ren397(x0,x1) % 0.10/0.41 % 840:2:2:INP:TopTop: p2(x0) -> ren397(x1,x0) % 0.10/0.41 % 841:3:3:INP:TopTopTop: r1(x0,x1),ren396(x1) -> ren397(x2,x0) % 0.10/0.41 % 842:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 843:2:1:INP:Top: r1(skc44,x0),ren80(x0) -> % 0.10/0.41 % 844:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 845:2:1:INP:Top: r1(skc44,x0),ren151(x0) -> % 0.10/0.41 % 846:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 847:2:1:INP:Top: r1(skc44,x0),ren213(x0) -> % 0.10/0.41 % 848:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 849:2:1:INP:Top: r1(skc44,x0),ren266(x0) -> % 0.10/0.41 % 850:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 851:2:1:INP:Top: r1(skc44,x0),ren310(x0) -> % 0.10/0.41 % 852:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 853:2:1:INP:Top: r1(skc44,x0),ren345(x0) -> % 0.10/0.41 % 854:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 855:2:1:INP:Top: r1(skc44,x0),ren371(x0) -> % 0.10/0.41 % 856:1:0:INP:: p2(skc44) -> % 0.10/0.41 % 857:2:1:INP:Top: r1(skc44,x0),ren388(x0,skf45(x0)) -> % 0.10/0.41 % 858:3:1:INP:Top: r1(skc44,x0),ren397(x0,skf46(x0)) -> p1(skc44) % 0.10/0.41 % 859:1:0:INP:: p1(skc44) -> % 0.10/0.41 % 0.10/0.41 % Predicates: r1 p2 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 ren125 ren126 ren127 ren128 ren129 ren130 ren131 ren132 ren133 ren134 ren135 ren136 ren137 ren138 ren139 ren140 ren141 ren142 ren143 ren144 ren145 ren146 ren147 ren148 ren149 ren150 ren151 ren152 ren153 ren154 ren155 ren156 ren157 ren158 ren159 ren160 ren161 ren162 ren163 ren164 ren165 ren166 ren167 ren168 ren169 ren170 ren171 ren172 ren173 ren174 ren175 ren176 ren177 ren178 ren179 ren180 ren181 ren182 ren183 ren184 ren185 ren186 ren187 ren188 ren189 ren190 ren191 ren192 ren193 ren194 ren195 ren196 ren197 ren198 ren199 ren200 ren201 ren202 ren203 ren204 ren205 ren206 ren207 ren208 ren209 ren210 ren211 ren212 ren213 ren214 ren215 ren216 ren217 ren218 ren219 ren220 ren221 ren222 ren223 ren224 ren225 ren226 ren227 ren228 ren229 ren230 ren231 ren232 ren233 ren234 ren235 ren236 ren237 ren238 ren239 ren240 ren241 ren242 ren243 ren244 ren245 ren246 ren247 ren248 ren249 ren250 ren251 ren252 ren253 ren254 ren255 ren256 ren257 ren258 ren259 ren260 ren261 ren262 ren263 ren264 ren265 ren266 ren267 ren268 ren269 ren270 ren271 ren272 ren273 ren274 ren275 ren276 ren277 ren278 ren279 ren280 ren281 ren282 ren283 ren284 ren285 ren286 ren287 ren288 ren289 ren290 ren291 ren292 ren293 ren294 ren295 ren296 ren297 ren298 ren299 ren300 ren301 ren302 ren303 ren304 ren305 ren306 ren307 ren308 ren309 ren310 ren311 ren312 ren313 ren314 ren315 ren316 ren317 ren318 ren319 ren320 ren321 ren322 ren323 ren324 ren325 ren326 ren327 ren328 ren329 ren330 ren331 ren332 ren333 ren334 ren335 ren336 ren337 ren338 ren339 ren340 ren341 ren342 ren343 ren344 ren345 ren346 ren347 ren348 ren349 ren350 ren351 ren352 ren353 ren354 ren355 ren356 ren357 ren358 ren359 ren360 ren361 ren362 ren363 ren364 ren365 ren366 ren367 ren368 ren369 ren370 ren371 ren372 ren373 ren374 ren375 ren376 ren377 ren378 ren379 ren380 ren381 ren382 ren383 ren384 ren385 ren386 ren387 ren388 ren389 ren390 ren391 ren392 ren393 ren394 ren395 ren396 ren397 % 0.10/0.41 % Fol Constants: skc44 % 0.10/0.41 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 skf25 skf26 skf27 skf28 skf29 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf45 skf46 % 0.22/0.51 % Problem Properties: % 0.22/0.51 % This is a full first-order problem without equality. The Problem is non-linear. % 0.22/0.51 % 0.22/0.51 % 0.22/0.51 % Reduced Input Axiom Clauses: % 0.22/0.51 % 1:1:1:INP:Top: -> r1(x0,x0) % 0.22/0.51 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2) % 0.22/0.51 % 3:2:1:INP:Top: p2(x0) -> ren1(x0) % 0.22/0.51 % 4:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren1(x0) % 0.22/0.51 % 5:2:1:INP:Top: p2(x0) -> ren2(x0) % 0.22/0.51 % 6:3:2:INP:TopTop: r1(x0,x1),ren1(x1) -> ren2(x0) % 0.22/0.51 % 7:2:1:INP:Top: p2(x0) -> ren3(x0) % 0.22/0.51 % 8:3:2:INP:TopTop: r1(x0,x1),ren2(x1) -> ren3(x0) % 0.22/0.51 % 9:2:1:INP:Top: p2(x0) -> ren4(x0) % 0.22/0.51 % 10:3:2:INP:TopTop: r1(x0,x1),ren3(x1) -> ren4(x0) % 0.22/0.51 % 11:2:1:INP:Top: p2(x0) -> ren5(x0) % 0.22/0.51 % 12:3:2:INP:TopTop: r1(x0,x1),ren4(x1) -> ren5(x0) % 0.22/0.51 % 13:2:1:INP:Top: p2(x0) -> ren6(x0) % 0.22/0.51 % 14:3:2:INP:TopTop: r1(x0,x1),ren5(x1) -> ren6(x0) % 0.22/0.51 % 15:2:1:INP:Top: p2(x0) -> ren7(x0) % 0.22/0.51 % 16:3:2:INP:TopTop: r1(x0,x1),ren6(x1) -> ren7(x0) % 0.22/0.51 % 17:2:1:INP:Top: p2(x0) -> ren8(x0) % 0.22/0.51 % 18:3:2:INP:TopTop: r1(x0,x1),ren7(x1) -> ren8(x0) % 0.22/0.51 % 19:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1) % 0.22/0.51 % 20:2:2:INP:TopTop: p2(x0) -> ren9(x1,x0) % 0.22/0.51 % 21:3:3:INP:TopTopTop: r1(x0,x1),ren8(x1) -> ren9(x2,x0) % 0.22/0.51 % 22:2:1:INP:Top: p2(x0) -> ren10(x0) % 0.22/0.51 % 23:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren9(x2,skf1(x2)) -> p1(x1),ren10(x0) % 0.22/0.51 % 24:2:1:INP:Top: p2(x0) -> ren11(x0) % 0.22/0.51 % 25:3:2:INP:TopTop: r1(x0,x1),ren10(x1) -> ren11(x0) % 0.22/0.51 % 26:2:1:INP:Top: p2(x0) -> ren12(x0) % 0.22/0.51 % 27:3:2:INP:TopTop: r1(x0,x1),ren11(x1) -> ren12(x0) % 0.22/0.51 % 28:2:1:INP:Top: p2(x0) -> ren13(x0) % 0.22/0.51 % 29:3:2:INP:TopTop: r1(x0,x1),ren12(x1) -> ren13(x0) % 0.22/0.51 % 30:2:1:INP:Top: p2(x0) -> ren14(x0) % 0.22/0.51 % 31:3:2:INP:TopTop: r1(x0,x1),ren13(x1) -> ren14(x0) % 0.22/0.51 % 32:2:1:INP:Top: p2(x0) -> ren15(x0) % 0.22/0.51 % 33:3:2:INP:TopTop: r1(x0,x1),ren14(x1) -> ren15(x0) % 0.22/0.51 % 34:2:1:INP:Top: p2(x0) -> ren16(x0) % 0.22/0.51 % 35:3:2:INP:TopTop: r1(x0,x1),ren15(x1) -> ren16(x0) % 0.22/0.51 % 36:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1) % 0.22/0.51 % 37:2:2:INP:TopTop: p2(x0) -> ren17(x1,x0) % 0.22/0.51 % 38:3:3:INP:TopTopTop: r1(x0,x1),ren16(x1) -> ren17(x2,x0) % 0.22/0.51 % 39:2:1:INP:Top: p2(x0) -> ren18(x0) % 0.22/0.51 % 40:3:2:INP:TopTop: r1(x0,x1),ren17(x1,skf2(x1)) -> ren18(x0) % 0.22/0.51 % 41:2:1:INP:Top: p2(x0) -> ren19(x0) % 0.22/0.51 % 42:3:2:INP:TopTop: r1(x0,x1),ren18(x1) -> ren19(x0) % 0.22/0.51 % 43:2:1:INP:Top: p2(x0) -> ren20(x0) % 0.22/0.51 % 44:3:2:INP:TopTop: r1(x0,x1),ren19(x1) -> ren20(x0) % 0.22/0.51 % 45:2:1:INP:Top: p2(x0) -> ren21(x0) % 0.22/0.51 % 46:3:2:INP:TopTop: r1(x0,x1),ren20(x1) -> ren21(x0) % 0.22/0.51 % 47:2:1:INP:Top: p2(x0) -> ren22(x0) % 0.22/0.51 % 48:3:2:INP:TopTop: r1(x0,x1),ren21(x1) -> ren22(x0) % 0.22/0.51 % 49:2:1:INP:Top: p2(x0) -> ren23(x0) % 0.22/0.51 % 50:3:2:INP:TopTop: r1(x0,x1),ren22(x1) -> ren23(x0) % 0.22/0.51 % 51:2:1:INP:Top: p2(x0) -> ren24(x0) % 0.22/0.51 % 52:3:2:INP:TopTop: r1(x0,x1),ren23(x1) -> ren24(x0) % 0.22/0.51 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1) % 0.22/0.51 % 54:2:2:INP:TopTop: p2(x0) -> ren25(x1,x0) % 0.22/0.51 % 55:3:3:INP:TopTopTop: r1(x0,x1),ren24(x1) -> ren25(x2,x0) % 0.22/0.51 % 56:2:1:INP:Top: p2(x0) -> ren26(x0) % 0.22/0.51 % 57:3:2:INP:TopTop: r1(x0,x1),ren25(x1,skf3(x1)) -> ren26(x0) % 0.22/0.51 % 58:2:1:INP:Top: p2(x0) -> ren27(x0) % 0.22/0.51 % 59:3:2:INP:TopTop: r1(x0,x1),ren26(x1) -> ren27(x0) % 0.22/0.51 % 60:2:1:INP:Top: p2(x0) -> ren28(x0) % 0.22/0.51 % 61:3:2:INP:TopTop: r1(x0,x1),ren27(x1) -> ren28(x0) % 0.22/0.51 % 62:2:1:INP:Top: p2(x0) -> ren29(x0) % 0.22/0.51 % 63:3:2:INP:TopTop: r1(x0,x1),ren28(x1) -> ren29(x0) % 0.22/0.51 % 64:2:1:INP:Top: p2(x0) -> ren30(x0) % 0.22/0.51 % 65:3:2:INP:TopTop: r1(x0,x1),ren29(x1) -> ren30(x0) % 0.22/0.51 % 66:2:1:INP:Top: p2(x0) -> ren31(x0) % 0.22/0.51 % 67:3:2:INP:TopTop: r1(x0,x1),ren30(x1) -> ren31(x0) % 0.22/0.51 % 68:2:1:INP:Top: p2(x0) -> ren32(x0) % 0.22/0.51 % 69:3:2:INP:TopTop: r1(x0,x1),ren31(x1) -> ren32(x0) % 0.22/0.51 % 70:2:2:INP:TopTop: -> r1(x0,x1),ren33(x0,x1) % 0.22/0.51 % 71:2:2:INP:TopTop: p2(x0) -> ren33(x1,x0) % 0.22/0.51 % 72:3:3:INP:TopTopTop: r1(x0,x1),ren32(x1) -> ren33(x2,x0) % 0.22/0.51 % 73:2:1:INP:Top: p2(x0) -> ren34(x0) % 0.22/0.51 % 74:3:2:INP:TopTop: r1(x0,x1),ren33(x1,skf4(x1)) -> ren34(x0) % 0.22/0.51 % 75:2:1:INP:Top: p2(x0) -> ren35(x0) % 0.22/0.51 % 76:3:2:INP:TopTop: r1(x0,x1),ren34(x1) -> ren35(x0) % 0.22/0.51 % 77:2:1:INP:Top: p2(x0) -> ren36(x0) % 0.22/0.51 % 78:3:2:INP:TopTop: r1(x0,x1),ren35(x1) -> ren36(x0) % 0.22/0.51 % 79:2:1:INP:Top: p2(x0) -> ren37(x0) % 0.22/0.51 % 80:3:2:INP:TopTop: r1(x0,x1),ren36(x1) -> ren37(x0) % 0.22/0.51 % 81:2:1:INP:Top: p2(x0) -> ren38(x0) % 0.22/0.51 % 82:3:2:INP:TopTop: r1(x0,x1),ren37(x1) -> ren38(x0) % 0.22/0.51 % 83:2:1:INP:Top: p2(x0) -> ren39(x0) % 0.22/0.51 % 84:3:2:INP:TopTop: r1(x0,x1),ren38(x1) -> ren39(x0) % 0.22/0.51 % 85:2:1:INP:Top: p2(x0) -> ren40(x0) % 0.22/0.51 % 86:3:2:INP:TopTop: r1(x0,x1),ren39(x1) -> ren40(x0) % 0.22/0.51 % 87:2:2:INP:TopTop: -> r1(x0,x1),ren41(x0,x1) % 0.22/0.51 % 88:2:2:INP:TopTop: p2(x0) -> ren41(x1,x0) % 0.22/0.51 % 89:3:3:INP:TopTopTop: r1(x0,x1),ren40(x1) -> ren41(x2,x0) % 0.22/0.51 % 90:2:1:INP:Top: p2(x0) -> ren42(x0) % 0.22/0.51 % 91:3:2:INP:TopTop: r1(x0,x1),ren41(x1,skf5(x1)) -> ren42(x0) % 0.22/0.51 % 92:2:1:INP:Top: p2(x0) -> ren43(x0) % 0.22/0.51 % 93:3:2:INP:TopTop: r1(x0,x1),ren42(x1) -> ren43(x0) % 0.22/0.51 % 94:2:1:INP:Top: p2(x0) -> ren44(x0) % 0.22/0.51 % 95:3:2:INP:TopTop: r1(x0,x1),ren43(x1) -> ren44(x0) % 0.22/0.51 % 96:2:1:INP:Top: p2(x0) -> ren45(x0) % 0.22/0.51 % 97:3:2:INP:TopTop: r1(x0,x1),ren44(x1) -> ren45(x0) % 0.22/0.51 % 98:2:1:INP:Top: p2(x0) -> ren46(x0) % 0.22/0.51 % 99:3:2:INP:TopTop: r1(x0,x1),ren45(x1) -> ren46(x0) % 0.22/0.51 % 100:2:1:INP:Top: p2(x0) -> ren47(x0) % 0.22/0.51 % 101:3:2:INP:TopTop: r1(x0,x1),ren46(x1) -> ren47(x0) % 0.22/0.51 % 102:2:1:INP:Top: p2(x0) -> ren48(x0) % 0.22/0.51 % 103:3:2:INP:TopTop: r1(x0,x1),ren47(x1) -> ren48(x0) % 0.22/0.51 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren49(x0,x1) % 0.22/0.51 % 105:2:2:INP:TopTop: p2(x0) -> ren49(x1,x0) % 0.22/0.51 % 106:3:3:INP:TopTopTop: r1(x0,x1),ren48(x1) -> ren49(x2,x0) % 0.22/0.51 % 107:2:1:INP:Top: p2(x0) -> ren50(x0) % 0.22/0.51 % 108:3:2:INP:TopTop: r1(x0,x1),ren49(x1,skf6(x1)) -> ren50(x0) % 0.22/0.51 % 109:2:1:INP:Top: p2(x0) -> ren51(x0) % 0.22/0.51 % 110:3:2:INP:TopTop: r1(x0,x1),ren50(x1) -> ren51(x0) % 0.22/0.51 % 111:2:1:INP:Top: p2(x0) -> ren52(x0) % 0.22/0.51 % 112:3:2:INP:TopTop: r1(x0,x1),ren51(x1) -> ren52(x0) % 0.22/0.51 % 113:2:1:INP:Top: p2(x0) -> ren53(x0) % 0.22/0.51 % 114:3:2:INP:TopTop: r1(x0,x1),ren52(x1) -> ren53(x0) % 0.22/0.51 % 115:2:1:INP:Top: p2(x0) -> ren54(x0) % 0.22/0.51 % 116:3:2:INP:TopTop: r1(x0,x1),ren53(x1) -> ren54(x0) % 0.22/0.51 % 117:2:1:INP:Top: p2(x0) -> ren55(x0) % 0.22/0.51 % 118:3:2:INP:TopTop: r1(x0,x1),ren54(x1) -> ren55(x0) % 0.22/0.51 % 119:2:1:INP:Top: p2(x0) -> ren56(x0) % 0.22/0.51 % 120:3:2:INP:TopTop: r1(x0,x1),ren55(x1) -> ren56(x0) % 0.22/0.51 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren57(x0,x1) % 0.22/0.51 % 122:2:2:INP:TopTop: p2(x0) -> ren57(x1,x0) % 0.22/0.51 % 123:3:3:INP:TopTopTop: r1(x0,x1),ren56(x1) -> ren57(x2,x0) % 0.22/0.51 % 124:2:1:INP:Top: p2(x0) -> ren58(x0) % 0.22/0.51 % 125:3:2:INP:TopTop: r1(x0,x1),ren57(x1,skf7(x1)) -> ren58(x0) % 0.22/0.51 % 126:2:1:INP:Top: p2(x0) -> ren59(x0) % 0.22/0.51 % 127:3:2:INP:TopTop: r1(x0,x1),ren58(x1) -> ren59(x0) % 0.22/0.51 % 128:2:1:INP:Top: p2(x0) -> ren60(x0) % 0.22/0.51 % 129:3:2:INP:TopTop: r1(x0,x1),ren59(x1) -> ren60(x0) % 0.22/0.51 % 130:2:1:INP:Top: p2(x0) -> ren61(x0) % 0.22/0.51 % 131:3:2:INP:TopTop: r1(x0,x1),ren60(x1) -> ren61(x0) % 0.22/0.51 % 132:2:1:INP:Top: p2(x0) -> ren62(x0) % 0.22/0.51 % 133:3:2:INP:TopTop: r1(x0,x1),ren61(x1) -> ren62(x0) % 0.22/0.51 % 134:2:1:INP:Top: p2(x0) -> ren63(x0) % 0.22/0.51 % 135:3:2:INP:TopTop: r1(x0,x1),ren62(x1) -> ren63(x0) % 0.22/0.51 % 136:2:1:INP:Top: p2(x0) -> ren64(x0) % 0.22/0.51 % 137:3:2:INP:TopTop: r1(x0,x1),ren63(x1) -> ren64(x0) % 0.22/0.51 % 138:2:2:INP:TopTop: -> r1(x0,x1),ren65(x0,x1) % 0.22/0.51 % 139:2:2:INP:TopTop: p2(x0) -> ren65(x1,x0) % 0.22/0.51 % 140:3:3:INP:TopTopTop: r1(x0,x1),ren64(x1) -> ren65(x2,x0) % 0.22/0.51 % 141:2:1:INP:Top: p2(x0) -> ren66(x0) % 0.22/0.51 % 142:3:2:INP:TopTop: r1(x0,x1),ren65(x1,skf8(x1)) -> ren66(x0) % 0.22/0.51 % 143:2:1:INP:Top: p2(x0) -> ren67(x0) % 0.22/0.51 % 144:3:2:INP:TopTop: r1(x0,x1),ren66(x1) -> ren67(x0) % 0.22/0.51 % 145:2:1:INP:Top: p2(x0) -> ren68(x0) % 0.22/0.51 % 146:3:2:INP:TopTop: r1(x0,x1),ren67(x1) -> ren68(x0) % 0.22/0.51 % 147:2:1:INP:Top: p2(x0) -> ren69(x0) % 0.22/0.51 % 148:3:2:INP:TopTop: r1(x0,x1),ren68(x1) -> ren69(x0) % 0.22/0.51 % 149:2:1:INP:Top: p2(x0) -> ren70(x0) % 0.22/0.51 % 150:3:2:INP:TopTop: r1(x0,x1),ren69(x1) -> ren70(x0) % 0.22/0.51 % 151:2:1:INP:Top: p2(x0) -> ren71(x0) % 0.22/0.51 % 152:3:2:INP:TopTop: r1(x0,x1),ren70(x1) -> ren71(x0) % 0.22/0.51 % 153:2:1:INP:Top: p2(x0) -> ren72(x0) % 0.22/0.51 % 154:3:2:INP:TopTop: r1(x0,x1),ren71(x1) -> ren72(x0) % 0.22/0.51 % 155:2:2:INP:TopTop: -> r1(x0,x1),ren73(x0,x1) % 0.22/0.51 % 156:2:2:INP:TopTop: p2(x0) -> ren73(x1,x0) % 0.22/0.51 % 157:3:3:INP:TopTopTop: r1(x0,x1),ren72(x1) -> ren73(x2,x0) % 0.22/0.51 % 158:2:1:INP:Top: p2(x0) -> ren74(x0) % 0.22/0.51 % 159:3:2:INP:TopTop: r1(x0,x1),ren73(x1,skf9(x1)) -> ren74(x0) % 0.22/0.51 % 160:2:1:INP:Top: p2(x0) -> ren75(x0) % 0.22/0.51 % 161:3:2:INP:TopTop: r1(x0,x1),ren74(x1) -> ren75(x0) % 0.22/0.51 % 162:2:1:INP:Top: p2(x0) -> ren76(x0) % 0.22/0.51 % 163:3:2:INP:TopTop: r1(x0,x1),ren75(x1) -> ren76(x0) % 0.22/0.51 % 164:2:1:INP:Top: p2(x0) -> ren77(x0) % 0.22/0.51 % 165:3:2:INP:TopTop: r1(x0,x1),ren76(x1) -> ren77(x0) % 0.22/0.51 % 166:2:1:INP:Top: p2(x0) -> ren78(x0) % 0.22/0.51 % 167:3:2:INP:TopTop: r1(x0,x1),ren77(x1) -> ren78(x0) % 0.22/0.51 % 168:2:1:INP:Top: p2(x0) -> ren79(x0) % 0.22/0.51 % 169:3:2:INP:TopTop: r1(x0,x1),ren78(x1) -> ren79(x0) % 0.22/0.51 % 170:2:1:INP:Top: p2(x0) -> ren80(x0) % 0.22/0.51 % 171:3:2:INP:TopTop: r1(x0,x1),ren79(x1) -> ren80(x0) % 0.22/0.51 % 172:2:1:INP:Top: p2(x0) -> ren81(x0) % 0.22/0.51 % 173:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren81(x0) % 0.22/0.51 % 174:2:1:INP:Top: p2(x0) -> ren82(x0) % 0.22/0.51 % 175:3:2:INP:TopTop: r1(x0,x1),ren81(x1) -> ren82(x0) % 0.22/0.51 % 176:2:1:INP:Top: p2(x0) -> ren83(x0) % 0.22/0.51 % 177:3:2:INP:TopTop: r1(x0,x1),ren82(x1) -> ren83(x0) % 0.22/0.51 % 178:2:1:INP:Top: p2(x0) -> ren84(x0) % 0.22/0.51 % 179:3:2:INP:TopTop: r1(x0,x1),ren83(x1) -> ren84(x0) % 0.22/0.51 % 180:2:1:INP:Top: p2(x0) -> ren85(x0) % 0.22/0.51 % 181:3:2:INP:TopTop: r1(x0,x1),ren84(x1) -> ren85(x0) % 0.22/0.51 % 182:2:1:INP:Top: p2(x0) -> ren86(x0) % 0.22/0.51 % 183:3:2:INP:TopTop: r1(x0,x1),ren85(x1) -> ren86(x0) % 0.22/0.51 % 184:2:1:INP:Top: p2(x0) -> ren87(x0) % 0.22/0.51 % 185:3:2:INP:TopTop: r1(x0,x1),ren86(x1) -> ren87(x0) % 0.22/0.51 % 186:2:1:INP:Top: p2(x0) -> ren88(x0) % 0.22/0.51 % 187:3:2:INP:TopTop: r1(x0,x1),ren87(x1) -> ren88(x0) % 0.22/0.51 % 188:2:2:INP:TopTop: -> r1(x0,x1),ren89(x0,x1) % 0.22/0.51 % 189:2:2:INP:TopTop: p2(x0) -> ren89(x1,x0) % 0.22/0.51 % 190:3:3:INP:TopTopTop: r1(x0,x1),ren88(x1) -> ren89(x2,x0) % 0.22/0.51 % 191:2:1:INP:Top: p2(x0) -> ren90(x0) % 0.22/0.51 % 192:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren89(x2,skf10(x2)) -> p1(x1),ren90(x0) % 0.22/0.51 % 193:2:1:INP:Top: p2(x0) -> ren91(x0) % 0.22/0.51 % 194:3:2:INP:TopTop: r1(x0,x1),ren90(x1) -> ren91(x0) % 0.22/0.51 % 195:2:1:INP:Top: p2(x0) -> ren92(x0) % 0.22/0.51 % 196:3:2:INP:TopTop: r1(x0,x1),ren91(x1) -> ren92(x0) % 0.22/0.51 % 197:2:1:INP:Top: p2(x0) -> ren93(x0) % 0.22/0.51 % 198:3:2:INP:TopTop: r1(x0,x1),ren92(x1) -> ren93(x0) % 0.22/0.51 % 199:2:1:INP:Top: p2(x0) -> ren94(x0) % 0.22/0.51 % 200:3:2:INP:TopTop: r1(x0,x1),ren93(x1) -> ren94(x0) % 0.22/0.51 % 201:2:1:INP:Top: p2(x0) -> ren95(x0) % 0.22/0.51 % 202:3:2:INP:TopTop: r1(x0,x1),ren94(x1) -> ren95(x0) % 0.22/0.51 % 203:2:1:INP:Top: p2(x0) -> ren96(x0) % 0.22/0.51 % 204:3:2:INP:TopTop: r1(x0,x1),ren95(x1) -> ren96(x0) % 0.22/0.51 % 205:2:2:INP:TopTop: -> r1(x0,x1),ren97(x0,x1) % 0.22/0.51 % 206:2:2:INP:TopTop: p2(x0) -> ren97(x1,x0) % 0.22/0.51 % 207:3:3:INP:TopTopTop: r1(x0,x1),ren96(x1) -> ren97(x2,x0) % 0.22/0.51 % 208:2:1:INP:Top: p2(x0) -> ren98(x0) % 0.22/0.51 % 209:3:2:INP:TopTop: r1(x0,x1),ren97(x1,skf11(x1)) -> ren98(x0) % 0.22/0.51 % 210:2:1:INP:Top: p2(x0) -> ren99(x0) % 0.22/0.51 % 211:3:2:INP:TopTop: r1(x0,x1),ren98(x1) -> ren99(x0) % 0.22/0.51 % 212:2:1:INP:Top: p2(x0) -> ren100(x0) % 0.22/0.51 % 213:3:2:INP:TopTop: r1(x0,x1),ren99(x1) -> ren100(x0) % 0.22/0.51 % 214:2:1:INP:Top: p2(x0) -> ren101(x0) % 0.22/0.51 % 215:3:2:INP:TopTop: r1(x0,x1),ren100(x1) -> ren101(x0) % 0.22/0.51 % 216:2:1:INP:Top: p2(x0) -> ren102(x0) % 0.22/0.51 % 217:3:2:INP:TopTop: r1(x0,x1),ren101(x1) -> ren102(x0) % 0.22/0.51 % 218:2:1:INP:Top: p2(x0) -> ren103(x0) % 0.22/0.51 % 219:3:2:INP:TopTop: r1(x0,x1),ren102(x1) -> ren103(x0) % 0.22/0.51 % 220:2:1:INP:Top: p2(x0) -> ren104(x0) % 0.22/0.51 % 221:3:2:INP:TopTop: r1(x0,x1),ren103(x1) -> ren104(x0) % 0.22/0.51 % 222:2:2:INP:TopTop: -> r1(x0,x1),ren105(x0,x1) % 0.22/0.51 % 223:2:2:INP:TopTop: p2(x0) -> ren105(x1,x0) % 0.22/0.51 % 224:3:3:INP:TopTopTop: r1(x0,x1),ren104(x1) -> ren105(x2,x0) % 0.22/0.51 % 225:2:1:INP:Top: p2(x0) -> ren106(x0) % 0.22/0.51 % 226:3:2:INP:TopTop: r1(x0,x1),ren105(x1,skf12(x1)) -> ren106(x0) % 0.22/0.51 % 227:2:1:INP:Top: p2(x0) -> ren107(x0) % 0.22/0.51 % 228:3:2:INP:TopTop: r1(x0,x1),ren106(x1) -> ren107(x0) % 0.22/0.51 % 229:2:1:INP:Top: p2(x0) -> ren108(x0) % 0.22/0.51 % 230:3:2:INP:TopTop: r1(x0,x1),ren107(x1) -> ren108(x0) % 0.22/0.51 % 231:2:1:INP:Top: p2(x0) -> ren109(x0) % 0.22/0.51 % 232:3:2:INP:TopTop: r1(x0,x1),ren108(x1) -> ren109(x0) % 0.22/0.51 % 233:2:1:INP:Top: p2(x0) -> ren110(x0) % 0.22/0.51 % 234:3:2:INP:TopTop: r1(x0,x1),ren109(x1) -> ren110(x0) % 0.22/0.51 % 235:2:1:INP:Top: p2(x0) -> ren111(x0) % 0.22/0.51 % 236:3:2:INP:TopTop: r1(x0,x1),ren110(x1) -> ren111(x0) % 0.22/0.51 % 237:2:1:INP:Top: p2(x0) -> ren112(x0) % 0.22/0.51 % 238:3:2:INP:TopTop: r1(x0,x1),ren111(x1) -> ren112(x0) % 0.22/0.51 % 239:2:2:INP:TopTop: -> r1(x0,x1),ren113(x0,x1) % 0.22/0.51 % 240:2:2:INP:TopTop: p2(x0) -> ren113(x1,x0) % 0.22/0.51 % 241:3:3:INP:TopTopTop: r1(x0,x1),ren112(x1) -> ren113(x2,x0) % 0.22/0.51 % 242:2:1:INP:Top: p2(x0) -> ren114(x0) % 0.22/0.51 % 243:3:2:INP:TopTop: r1(x0,x1),ren113(x1,skf13(x1)) -> ren114(x0) % 0.22/0.51 % 244:2:1:INP:Top: p2(x0) -> ren115(x0) % 0.22/0.51 % 245:3:2:INP:TopTop: r1(x0,x1),ren114(x1) -> ren115(x0) % 0.22/0.51 % 246:2:1:INP:Top: p2(x0) -> ren116(x0) % 0.22/0.51 % 247:3:2:INP:TopTop: r1(x0,x1),ren115(x1) -> ren116(x0) % 0.22/0.51 % 248:2:1:INP:Top: p2(x0) -> ren117(x0) % 0.22/0.51 % 249:3:2:INP:TopTop: r1(x0,x1),ren116(x1) -> ren117(x0) % 0.22/0.51 % 250:2:1:INP:Top: p2(x0) -> ren118(x0) % 0.22/0.51 % 251:3:2:INP:TopTop: r1(x0,x1),ren117(x1) -> ren118(x0) % 0.22/0.51 % 252:2:1:INP:Top: p2(x0) -> ren119(x0) % 0.22/0.51 % 253:3:2:INP:TopTop: r1(x0,x1),ren118(x1) -> ren119(x0) % 0.22/0.51 % 254:2:1:INP:Top: p2(x0) -> ren120(x0) % 0.22/0.51 % 255:3:2:INP:TopTop: r1(x0,x1),ren119(x1) -> ren120(x0) % 0.22/0.51 % 256:2:2:INP:TopTop: -> r1(x0,x1),ren121(x0,x1) % 0.22/0.51 % 257:2:2:INP:TopTop: p2(x0) -> ren121(x1,x0) % 0.22/0.51 % 258:3:3:INP:TopTopTop: r1(x0,x1),ren120(x1) -> ren121(x2,x0) % 0.22/0.51 % 259:2:1:INP:Top: p2(x0) -> ren122(x0) % 0.22/0.51 % 260:3:2:INP:TopTop: r1(x0,x1),ren121(x1,skf14(x1)) -> ren122(x0) % 0.22/0.51 % 261:2:1:INP:Top: p2(x0) -> ren123(x0) % 0.22/0.51 % 262:3:2:INP:TopTop: r1(x0,x1),ren122(x1) -> ren123(x0) % 0.22/0.51 % 263:2:1:INP:Top: p2(x0) -> ren124(x0) % 0.22/0.51 % 264:3:2:INP:TopTop: r1(x0,x1),ren123(x1) -> ren124(x0) % 0.22/0.51 % 265:2:1:INP:Top: p2(x0) -> ren125(x0) % 0.22/0.51 % 266:3:2:INP:TopTop: r1(x0,x1),ren124(x1) -> ren125(x0) % 0.22/0.51 % 267:2:1:INP:Top: p2(x0) -> ren126(x0) % 0.22/0.51 % 268:3:2:INP:TopTop: r1(x0,x1),ren125(x1) -> ren126(x0) % 0.22/0.51 % 269:2:1:INP:Top: p2(x0) -> ren127(x0) % 0.22/0.51 % 270:3:2:INP:TopTop: r1(x0,x1),ren126(x1) -> ren127(x0) % 0.22/0.51 % 271:2:1:INP:Top: p2(x0) -> ren128(x0) % 0.22/0.51 % 272:3:2:INP:TopTop: r1(x0,x1),ren127(x1) -> ren128(x0) % 0.22/0.51 % 273:2:2:INP:TopTop: -> r1(x0,x1),ren129(x0,x1) % 0.22/0.51 % 274:2:2:INP:TopTop: p2(x0) -> ren129(x1,x0) % 0.22/0.51 % 275:3:3:INP:TopTopTop: r1(x0,x1),ren128(x1) -> ren129(x2,x0) % 0.22/0.51 % 276:2:1:INP:Top: p2(x0) -> ren130(x0) % 0.22/0.51 % 277:3:2:INP:TopTop: r1(x0,x1),ren129(x1,skf15(x1)) -> ren130(x0) % 0.22/0.51 % 278:2:1:INP:Top: p2(x0) -> ren131(x0) % 0.22/0.51 % 279:3:2:INP:TopTop: r1(x0,x1),ren130(x1) -> ren131(x0) % 0.22/0.51 % 280:2:1:INP:Top: p2(x0) -> ren132(x0) % 0.22/0.51 % 281:3:2:INP:TopTop: r1(x0,x1),ren131(x1) -> ren132(x0) % 0.22/0.51 % 282:2:1:INP:Top: p2(x0) -> ren133(x0) % 0.22/0.51 % 283:3:2:INP:TopTop: r1(x0,x1),ren132(x1) -> ren133(x0) % 0.22/0.51 % 284:2:1:INP:Top: p2(x0) -> ren134(x0) % 0.22/0.51 % 285:3:2:INP:TopTop: r1(x0,x1),ren133(x1) -> ren134(x0) % 0.22/0.51 % 286:2:1:INP:Top: p2(x0) -> ren135(x0) % 0.22/0.51 % 287:3:2:INP:TopTop: r1(x0,x1),ren134(x1) -> ren135(x0) % 0.22/0.51 % 288:2:1:INP:Top: p2(x0) -> ren136(x0) % 0.22/0.51 % 289:3:2:INP:TopTop: r1(x0,x1),ren135(x1) -> ren136(x0) % 0.22/0.51 % 290:2:2:INP:TopTop: -> r1(x0,x1),ren137(x0,x1) % 0.22/0.51 % 291:2:2:INP:TopTop: p2(x0) -> ren137(x1,x0) % 0.22/0.51 % 292:3:3:INP:TopTopTop: r1(x0,x1),ren136(x1) -> ren137(x2,x0) % 0.22/0.51 % 293:2:1:INP:Top: p2(x0) -> ren138(x0) % 0.22/0.51 % 294:3:2:INP:TopTop: r1(x0,x1),ren137(x1,skf16(x1)) -> ren138(x0) % 0.22/0.51 % 295:2:1:INP:Top: p2(x0) -> ren139(x0) % 0.22/0.51 % 296:3:2:INP:TopTop: r1(x0,x1),ren138(x1) -> ren139(x0) % 0.22/0.51 % 297:2:1:INP:Top: p2(x0) -> ren140(x0) % 0.22/0.51 % 298:3:2:INP:TopTop: r1(x0,x1),ren139(x1) -> ren140(x0) % 0.22/0.51 % 299:2:1:INP:Top: p2(x0) -> ren141(x0) % 0.22/0.51 % 300:3:2:INP:TopTop: r1(x0,x1),ren140(x1) -> ren141(x0) % 0.22/0.51 % 301:2:1:INP:Top: p2(x0) -> ren142(x0) % 0.22/0.51 % 302:3:2:INP:TopTop: r1(x0,x1),ren141(x1) -> ren142(x0) % 0.22/0.51 % 303:2:1:INP:Top: p2(x0) -> ren143(x0) % 0.22/0.51 % 304:3:2:INP:TopTop: r1(x0,x1),ren142(x1) -> ren143(x0) % 0.22/0.51 % 305:2:1:INP:Top: p2(x0) -> ren144(x0) % 0.22/0.51 % 306:3:2:INP:TopTop: r1(x0,x1),ren143(x1) -> ren144(x0) % 0.22/0.51 % 307:2:2:INP:TopTop: -> r1(x0,x1),ren145(x0,x1) % 0.22/0.51 % 308:2:2:INP:TopTop: p2(x0) -> ren145(x1,x0) % 0.22/0.51 % 309:3:3:INP:TopTopTop: r1(x0,x1),ren144(x1) -> ren145(x2,x0) % 0.22/0.51 % 310:2:1:INP:Top: p2(x0) -> ren146(x0) % 0.22/0.51 % 311:3:2:INP:TopTop: r1(x0,x1),ren145(x1,skf17(x1)) -> ren146(x0) % 0.22/0.51 % 312:2:1:INP:Top: p2(x0) -> ren147(x0) % 0.22/0.51 % 313:3:2:INP:TopTop: r1(x0,x1),ren146(x1) -> ren147(x0) % 0.22/0.51 % 314:2:1:INP:Top: p2(x0) -> ren148(x0) % 0.22/0.51 % 315:3:2:INP:TopTop: r1(x0,x1),ren147(x1) -> ren148(x0) % 0.22/0.51 % 316:2:1:INP:Top: p2(x0) -> ren149(x0) % 0.22/0.51 % 317:3:2:INP:TopTop: r1(x0,x1),ren148(x1) -> ren149(x0) % 0.22/0.51 % 318:2:1:INP:Top: p2(x0) -> ren150(x0) % 0.22/0.51 % 319:3:2:INP:TopTop: r1(x0,x1),ren149(x1) -> ren150(x0) % 0.22/0.51 % 320:2:1:INP:Top: p2(x0) -> ren151(x0) % 0.22/0.51 % 321:3:2:INP:TopTop: r1(x0,x1),ren150(x1) -> ren151(x0) % 0.22/0.51 % 322:2:1:INP:Top: p2(x0) -> ren152(x0) % 0.22/0.51 % 323:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren152(x0) % 0.22/0.51 % 324:2:1:INP:Top: p2(x0) -> ren153(x0) % 0.22/0.51 % 325:3:2:INP:TopTop: r1(x0,x1),ren152(x1) -> ren153(x0) % 0.22/0.51 % 326:2:1:INP:Top: p2(x0) -> ren154(x0) % 0.22/0.51 % 327:3:2:INP:TopTop: r1(x0,x1),ren153(x1) -> ren154(x0) % 0.22/0.51 % 328:2:1:INP:Top: p2(x0) -> ren155(x0) % 0.22/0.51 % 329:3:2:INP:TopTop: r1(x0,x1),ren154(x1) -> ren155(x0) % 0.22/0.51 % 330:2:1:INP:Top: p2(x0) -> ren156(x0) % 0.22/0.51 % 331:3:2:INP:TopTop: r1(x0,x1),ren155(x1) -> ren156(x0) % 0.22/0.51 % 332:2:1:INP:Top: p2(x0) -> ren157(x0) % 0.22/0.51 % 333:3:2:INP:TopTop: r1(x0,x1),ren156(x1) -> ren157(x0) % 0.22/0.51 % 334:2:1:INP:Top: p2(x0) -> ren158(x0) % 0.22/0.51 % 335:3:2:INP:TopTop: r1(x0,x1),ren157(x1) -> ren158(x0) % 0.22/0.51 % 336:2:1:INP:Top: p2(x0) -> ren159(x0) % 0.22/0.51 % 337:3:2:INP:TopTop: r1(x0,x1),ren158(x1) -> ren159(x0) % 0.22/0.51 % 338:2:2:INP:TopTop: -> r1(x0,x1),ren160(x0,x1) % 0.22/0.51 % 339:2:2:INP:TopTop: p2(x0) -> ren160(x1,x0) % 0.22/0.51 % 340:3:3:INP:TopTopTop: r1(x0,x1),ren159(x1) -> ren160(x2,x0) % 0.22/0.51 % 341:2:1:INP:Top: p2(x0) -> ren161(x0) % 0.22/0.51 % 342:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren160(x2,skf18(x2)) -> p1(x1),ren161(x0) % 0.22/0.51 % 343:2:1:INP:Top: p2(x0) -> ren162(x0) % 0.22/0.51 % 344:3:2:INP:TopTop: r1(x0,x1),ren161(x1) -> ren162(x0) % 0.22/0.51 % 345:2:1:INP:Top: p2(x0) -> ren163(x0) % 0.22/0.51 % 346:3:2:INP:TopTop: r1(x0,x1),ren162(x1) -> ren163(x0) % 0.22/0.51 % 347:2:1:INP:Top: p2(x0) -> ren164(x0) % 0.22/0.51 % 348:3:2:INP:TopTop: r1(x0,x1),ren163(x1) -> ren164(x0) % 0.22/0.51 % 349:2:1:INP:Top: p2(x0) -> ren165(x0) % 0.22/0.51 % 350:3:2:INP:TopTop: r1(x0,x1),ren164(x1) -> ren165(x0) % 0.22/0.51 % 351:2:1:INP:Top: p2(x0) -> ren166(x0) % 0.22/0.51 % 352:3:2:INP:TopTop: r1(x0,x1),ren165(x1) -> ren166(x0) % 0.22/0.51 % 353:2:1:INP:Top: p2(x0) -> ren167(x0) % 0.22/0.51 % 354:3:2:INP:TopTop: r1(x0,x1),ren166(x1) -> ren167(x0) % 0.22/0.51 % 355:2:2:INP:TopTop: -> r1(x0,x1),ren168(x0,x1) % 0.22/0.51 % 356:2:2:INP:TopTop: p2(x0) -> ren168(x1,x0) % 0.22/0.51 % 357:3:3:INP:TopTopTop: r1(x0,x1),ren167(x1) -> ren168(x2,x0) % 0.22/0.51 % 358:2:1:INP:Top: p2(x0) -> ren169(x0) % 0.22/0.51 % 359:3:2:INP:TopTop: r1(x0,x1),ren168(x1,skf19(x1)) -> ren169(x0) % 0.22/0.51 % 360:2:1:INP:Top: p2(x0) -> ren170(x0) % 0.22/0.51 % 361:3:2:INP:TopTop: r1(x0,x1),ren169(x1) -> ren170(x0) % 0.22/0.51 % 362:2:1:INP:Top: p2(x0) -> ren171(x0) % 0.22/0.51 % 363:3:2:INP:TopTop: r1(x0,x1),ren170(x1) -> ren171(x0) % 0.22/0.51 % 364:2:1:INP:Top: p2(x0) -> ren172(x0) % 0.22/0.51 % 365:3:2:INP:TopTop: r1(x0,x1),ren171(x1) -> ren172(x0) % 0.22/0.51 % 366:2:1:INP:Top: p2(x0) -> ren173(x0) % 0.22/0.51 % 367:3:2:INP:TopTop: r1(x0,x1),ren172(x1) -> ren173(x0) % 0.22/0.51 % 368:2:1:INP:Top: p2(x0) -> ren174(x0) % 0.22/0.51 % 369:3:2:INP:TopTop: r1(x0,x1),ren173(x1) -> ren174(x0) % 0.22/0.51 % 370:2:1:INP:Top: p2(x0) -> ren175(x0) % 0.22/0.51 % 371:3:2:INP:TopTop: r1(x0,x1),ren174(x1) -> ren175(x0) % 0.22/0.51 % 372:2:2:INP:TopTop: -> r1(x0,x1),ren176(x0,x1) % 0.22/0.51 % 373:2:2:INP:TopTop: p2(x0) -> ren176(x1,x0) % 0.22/0.51 % 374:3:3:INP:TopTopTop: r1(x0,x1),ren175(x1) -> ren176(x2,x0) % 0.22/0.51 % 375:2:1:INP:Top: p2(x0) -> ren177(x0) % 0.22/0.51 % 376:3:2:INP:TopTop: r1(x0,x1),ren176(x1,skf20(x1)) -> ren177(x0) % 0.22/0.51 % 377:2:1:INP:Top: p2(x0) -> ren178(x0) % 0.22/0.51 % 378:3:2:INP:TopTop: r1(x0,x1),ren177(x1) -> ren178(x0) % 0.22/0.51 % 379:2:1:INP:Top: p2(x0) -> ren179(x0) % 0.22/0.51 % 380:3:2:INP:TopTop: r1(x0,x1),ren178(x1) -> ren179(x0) % 0.22/0.51 % 381:2:1:INP:Top: p2(x0) -> ren180(x0) % 0.22/0.51 % 382:3:2:INP:TopTop: r1(x0,x1),ren179(x1) -> ren180(x0) % 0.22/0.51 % 383:2:1:INP:Top: p2(x0) -> ren181(x0) % 0.22/0.51 % 384:3:2:INP:TopTop: r1(x0,x1),ren180(x1) -> ren181(x0) % 0.22/0.51 % 385:2:1:INP:Top: p2(x0) -> ren182(x0) % 0.22/0.51 % 386:3:2:INP:TopTop: r1(x0,x1),ren181(x1) -> ren182(x0) % 0.22/0.51 % 387:2:1:INP:Top: p2(x0) -> ren183(x0) % 0.22/0.51 % 388:3:2:INP:TopTop: r1(x0,x1),ren182(x1) -> ren183(x0) % 0.22/0.51 % 389:2:2:INP:TopTop: -> r1(x0,x1),ren184(x0,x1) % 0.22/0.51 % 390:2:2:INP:TopTop: p2(x0) -> ren184(x1,x0) % 0.22/0.51 % 391:3:3:INP:TopTopTop: r1(x0,x1),ren183(x1) -> ren184(x2,x0) % 0.22/0.51 % 392:2:1:INP:Top: p2(x0) -> ren185(x0) % 0.22/0.51 % 393:3:2:INP:TopTop: r1(x0,x1),ren184(x1,skf21(x1)) -> ren185(x0) % 0.22/0.51 % 394:2:1:INP:Top: p2(x0) -> ren186(x0) % 0.22/0.51 % 395:3:2:INP:TopTop: r1(x0,x1),ren185(x1) -> ren186(x0) % 0.22/0.51 % 396:2:1:INP:Top: p2(x0) -> ren187(x0) % 0.22/0.51 % 397:3:2:INP:TopTop: r1(x0,x1),ren186(x1) -> ren187(x0) % 0.22/0.51 % 398:2:1:INP:Top: p2(x0) -> ren188(x0) % 0.22/0.51 % 399:3:2:INP:TopTop: r1(x0,x1),ren187(x1) -> ren188(x0) % 0.22/0.51 % 400:2:1:INP:Top: p2(x0) -> ren189(x0) % 0.22/0.51 % 401:3:2:INP:TopTop: r1(x0,x1),ren188(x1) -> ren189(x0) % 0.22/0.51 % 402:2:1:INP:Top: p2(x0) -> ren190(x0) % 0.22/0.51 % 403:3:2:INP:TopTop: r1(x0,x1),ren189(x1) -> ren190(x0) % 0.22/0.51 % 404:2:1:INP:Top: p2(x0) -> ren191(x0) % 0.22/0.51 % 405:3:2:INP:TopTop: r1(x0,x1),ren190(x1) -> ren191(x0) % 0.22/0.51 % 406:2:2:INP:TopTop: -> r1(x0,x1),ren192(x0,x1) % 0.22/0.51 % 407:2:2:INP:TopTop: p2(x0) -> ren192(x1,x0) % 0.22/0.51 % 408:3:3:INP:TopTopTop: r1(x0,x1),ren191(x1) -> ren192(x2,x0) % 0.22/0.51 % 409:2:1:INP:Top: p2(x0) -> ren193(x0) % 0.22/0.51 % 410:3:2:INP:TopTop: r1(x0,x1),ren192(x1,skf22(x1)) -> ren193(x0) % 0.22/0.51 % 411:2:1:INP:Top: p2(x0) -> ren194(x0) % 0.22/0.51 % 412:3:2:INP:TopTop: r1(x0,x1),ren193(x1) -> ren194(x0) % 0.22/0.51 % 413:2:1:INP:Top: p2(x0) -> ren195(x0) % 0.22/0.51 % 414:3:2:INP:TopTop: r1(x0,x1),ren194(x1) -> ren195(x0) % 0.22/0.51 % 415:2:1:INP:Top: p2(x0) -> ren196(x0) % 0.22/0.51 % 416:3:2:INP:TopTop: r1(x0,x1),ren195(x1) -> ren196(x0) % 0.22/0.51 % 417:2:1:INP:Top: p2(x0) -> ren197(x0) % 0.22/0.51 % 418:3:2:INP:TopTop: r1(x0,x1),ren196(x1) -> ren197(x0) % 0.22/0.51 % 419:2:1:INP:Top: p2(x0) -> ren198(x0) % 0.22/0.51 % 420:3:2:INP:TopTop: r1(x0,x1),ren197(x1) -> ren198(x0) % 0.22/0.51 % 421:2:1:INP:Top: p2(x0) -> ren199(x0) % 0.22/0.51 % 422:3:2:INP:TopTop: r1(x0,x1),ren198(x1) -> ren199(x0) % 0.22/0.51 % 423:2:2:INP:TopTop: -> r1(x0,x1),ren200(x0,x1) % 0.22/0.51 % 424:2:2:INP:TopTop: p2(x0) -> ren200(x1,x0) % 0.22/0.51 % 425:3:3:INP:TopTopTop: r1(x0,x1),ren199(x1) -> ren200(x2,x0) % 0.22/0.51 % 426:2:1:INP:Top: p2(x0) -> ren201(x0) % 0.22/0.51 % 427:3:2:INP:TopTop: r1(x0,x1),ren200(x1,skf23(x1)) -> ren201(x0) % 0.22/0.51 % 428:2:1:INP:Top: p2(x0) -> ren202(x0) % 0.22/0.51 % 429:3:2:INP:TopTop: r1(x0,x1),ren201(x1) -> ren202(x0) % 0.22/0.51 % 430:2:1:INP:Top: p2(x0) -> ren203(x0) % 0.22/0.51 % 431:3:2:INP:TopTop: r1(x0,x1),ren202(x1) -> ren203(x0) % 0.22/0.51 % 432:2:1:INP:Top: p2(x0) -> ren204(x0) % 0.22/0.51 % 433:3:2:INP:TopTop: r1(x0,x1),ren203(x1) -> ren204(x0) % 0.22/0.51 % 434:2:1:INP:Top: p2(x0) -> ren205(x0) % 0.22/0.51 % 435:3:2:INP:TopTop: r1(x0,x1),ren204(x1) -> ren205(x0) % 0.22/0.51 % 436:2:1:INP:Top: p2(x0) -> ren206(x0) % 0.22/0.51 % 437:3:2:INP:TopTop: r1(x0,x1),ren205(x1) -> ren206(x0) % 0.22/0.51 % 438:2:1:INP:Top: p2(x0) -> ren207(x0) % 0.22/0.51 % 439:3:2:INP:TopTop: r1(x0,x1),ren206(x1) -> ren207(x0) % 0.22/0.51 % 440:2:2:INP:TopTop: -> r1(x0,x1),ren208(x0,x1) % 0.22/0.51 % 441:2:2:INP:TopTop: p2(x0) -> ren208(x1,x0) % 0.22/0.51 % 442:3:3:INP:TopTopTop: r1(x0,x1),ren207(x1) -> ren208(x2,x0) % 0.22/0.51 % 443:2:1:INP:Top: p2(x0) -> ren209(x0) % 0.22/0.51 % 444:3:2:INP:TopTop: r1(x0,x1),ren208(x1,skf24(x1)) -> ren209(x0) % 0.22/0.51 % 445:2:1:INP:Top: p2(x0) -> ren210(x0) % 0.22/0.51 % 446:3:2:INP:TopTop: r1(x0,x1),ren209(x1) -> ren210(x0) % 0.22/0.51 % 447:2:1:INP:Top: p2(x0) -> ren211(x0) % 0.22/0.51 % 448:3:2:INP:TopTop: r1(x0,x1),ren210(x1) -> ren211(x0) % 0.22/0.51 % 449:2:1:INP:Top: p2(x0) -> ren212(x0) % 0.22/0.51 % 450:3:2:INP:TopTop: r1(x0,x1),ren211(x1) -> ren212(x0) % 0.22/0.51 % 451:2:1:INP:Top: p2(x0) -> ren213(x0) % 0.22/0.51 % 452:3:2:INP:TopTop: r1(x0,x1),ren212(x1) -> ren213(x0) % 0.22/0.51 % 453:2:1:INP:Top: p2(x0) -> ren214(x0) % 0.22/0.51 % 454:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren214(x0) % 0.22/0.51 % 455:2:1:INP:Top: p2(x0) -> ren215(x0) % 0.22/0.51 % 456:3:2:INP:TopTop: r1(x0,x1),ren214(x1) -> ren215(x0) % 0.22/0.51 % 457:2:1:INP:Top: p2(x0) -> ren216(x0) % 0.22/0.51 % 458:3:2:INP:TopTop: r1(x0,x1),ren215(x1) -> ren216(x0) % 0.22/0.51 % 459:2:1:INP:Top: p2(x0) -> ren217(x0) % 0.22/0.51 % 460:3:2:INP:TopTop: r1(x0,x1),ren216(x1) -> ren217(x0) % 0.22/0.51 % 461:2:1:INP:Top: p2(x0) -> ren218(x0) % 0.22/0.51 % 462:3:2:INP:TopTop: r1(x0,x1),ren217(x1) -> ren218(x0) % 0.22/0.51 % 463:2:1:INP:Top: p2(x0) -> ren219(x0) % 0.22/0.51 % 464:3:2:INP:TopTop: r1(x0,x1),ren218(x1) -> ren219(x0) % 0.22/0.51 % 465:2:1:INP:Top: p2(x0) -> ren220(x0) % 0.22/0.51 % 466:3:2:INP:TopTop: r1(x0,x1),ren219(x1) -> ren220(x0) % 0.22/0.51 % 467:2:1:INP:Top: p2(x0) -> ren221(x0) % 0.22/0.51 % 468:3:2:INP:TopTop: r1(x0,x1),ren220(x1) -> ren221(x0) % 0.22/0.51 % 469:2:2:INP:TopTop: -> r1(x0,x1),ren222(x0,x1) % 0.22/0.51 % 470:2:2:INP:TopTop: p2(x0) -> ren222(x1,x0) % 0.22/0.51 % 471:3:3:INP:TopTopTop: r1(x0,x1),ren221(x1) -> ren222(x2,x0) % 0.22/0.51 % 472:2:1:INP:Top: p2(x0) -> ren223(x0) % 0.22/0.51 % 473:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren222(x2,skf25(x2)) -> p1(x1),ren223(x0) % 0.22/0.51 % 474:2:1:INP:Top: p2(x0) -> ren224(x0) % 0.22/0.51 % 475:3:2:INP:TopTop: r1(x0,x1),ren223(x1) -> ren224(x0) % 0.22/0.51 % 476:2:1:INP:Top: p2(x0) -> ren225(x0) % 0.22/0.51 % 477:3:2:INP:TopTop: r1(x0,x1),ren224(x1) -> ren225(x0) % 0.22/0.51 % 478:2:1:INP:Top: p2(x0) -> ren226(x0) % 0.22/0.51 % 479:3:2:INP:TopTop: r1(x0,x1),ren225(x1) -> ren226(x0) % 0.22/0.51 % 480:2:1:INP:Top: p2(x0) -> ren227(x0) % 0.22/0.51 % 481:3:2:INP:TopTop: r1(x0,x1),ren226(x1) -> ren227(x0) % 0.22/0.51 % 482:2:1:INP:Top: p2(x0) -> ren228(x0) % 0.22/0.51 % 483:3:2:INP:TopTop: r1(x0,x1),ren227(x1) -> ren228(x0) % 0.22/0.51 % 484:2:1:INP:Top: p2(x0) -> ren229(x0) % 0.22/0.51 % 485:3:2:INP:TopTop: r1(x0,x1),ren228(x1) -> ren229(x0) % 0.22/0.51 % 486:2:2:INP:TopTop: -> r1(x0,x1),ren230(x0,x1) % 0.22/0.51 % 487:2:2:INP:TopTop: p2(x0) -> ren230(x1,x0) % 0.22/0.51 % 488:3:3:INP:TopTopTop: r1(x0,x1),ren229(x1) -> ren230(x2,x0) % 0.22/0.51 % 489:2:1:INP:Top: p2(x0) -> ren231(x0) % 0.22/0.51 % 490:3:2:INP:TopTop: r1(x0,x1),ren230(x1,skf26(x1)) -> ren231(x0) % 0.22/0.51 % 491:2:1:INP:Top: p2(x0) -> ren232(x0) % 0.22/0.51 % 492:3:2:INP:TopTop: r1(x0,x1),ren231(x1) -> ren232(x0) % 0.22/0.51 % 493:2:1:INP:Top: p2(x0) -> ren233(x0) % 0.22/0.51 % 494:3:2:INP:TopTop: r1(x0,x1),ren232(x1) -> ren233(x0) % 0.22/0.51 % 495:2:1:INP:Top: p2(x0) -> ren234(x0) % 0.22/0.51 % 496:3:2:INP:TopTop: r1(x0,x1),ren233(x1) -> ren234(x0) % 0.22/0.51 % 497:2:1:INP:Top: p2(x0) -> ren235(x0) % 0.22/0.51 % 498:3:2:INP:TopTop: r1(x0,x1),ren234(x1) -> ren235(x0) % 0.22/0.51 % 499:2:1:INP:Top: p2(x0) -> ren236(x0) % 0.22/0.51 % 500:3:2:INP:TopTop: r1(x0,x1),ren235(x1) -> ren236(x0) % 0.22/0.51 % 501:2:1:INP:Top: p2(x0) -> ren237(x0) % 0.22/0.51 % 502:3:2:INP:TopTop: r1(x0,x1),ren236(x1) -> ren237(x0) % 0.22/0.51 % 503:2:2:INP:TopTop: -> r1(x0,x1),ren238(x0,x1) % 0.22/0.51 % 504:2:2:INP:TopTop: p2(x0) -> ren238(x1,x0) % 0.22/0.51 % 505:3:3:INP:TopTopTop: r1(x0,x1),ren237(x1) -> ren238(x2,x0) % 0.22/0.51 % 506:2:1:INP:Top: p2(x0) -> ren239(x0) % 0.22/0.51 % 507:3:2:INP:TopTop: r1(x0,x1),ren238(x1,skf27(x1)) -> ren239(x0) % 0.22/0.51 % 508:2:1:INP:Top: p2(x0) -> ren240(x0) % 0.22/0.51 % 509:3:2:INP:TopTop: r1(x0,x1),ren239(x1) -> ren240(x0) % 0.22/0.51 % 510:2:1:INP:Top: p2(x0) -> ren241(x0) % 0.22/0.51 % 511:3:2:INP:TopTop: r1(x0,x1),ren240(x1) -> ren241(x0) % 0.22/0.51 % 512:2:1:INP:Top: p2(x0) -> ren242(x0) % 0.22/0.51 % 513:3:2:INP:TopTop: r1(x0,x1),ren241(x1) -> ren242(x0) % 0.22/0.51 % 514:2:1:INP:Top: p2(x0) -> ren243(x0) % 0.22/0.51 % 515:3:2:INP:TopTop: r1(x0,x1),ren242(x1) -> ren243(x0) % 0.22/0.51 % 516:2:1:INP:Top: p2(x0) -> ren244(x0) % 0.22/0.51 % 517:3:2:INP:TopTop: r1(x0,x1),ren243(x1) -> ren244(x0) % 0.22/0.51 % 518:2:1:INP:Top: p2(x0) -> ren245(x0) % 0.22/0.51 % 519:3:2:INP:TopTop: r1(x0,x1),ren244(x1) -> ren245(x0) % 0.22/0.51 % 520:2:2:INP:TopTop: -> r1(x0,x1),ren246(x0,x1) % 0.22/0.51 % 521:2:2:INP:TopTop: p2(x0) -> ren246(x1,x0) % 0.22/0.51 % 522:3:3:INP:TopTopTop: r1(x0,x1),ren245(x1) -> ren246(x2,x0) % 0.22/0.51 % 523:2:1:INP:Top: p2(x0) -> ren247(x0) % 0.22/0.51 % 524:3:2:INP:TopTop: r1(x0,x1),ren246(x1,skf28(x1)) -> ren247(x0) % 0.22/0.51 % 525:2:1:INP:Top: p2(x0) -> ren248(x0) % 0.22/0.51 % 526:3:2:INP:TopTop: r1(x0,x1),ren247(x1) -> ren248(x0) % 0.22/0.51 % 527:2:1:INP:Top: p2(x0) -> ren249(x0) % 0.22/0.51 % 528:3:2:INP:TopTop: r1(x0,x1),ren248(x1) -> ren249(x0) % 0.22/0.51 % 529:2:1:INP:Top: p2(x0) -> ren250(x0) % 0.22/0.51 % 530:3:2:INP:TopTop: r1(x0,x1),ren249(x1) -> ren250(x0) % 0.22/0.51 % 531:2:1:INP:Top: p2(x0) -> ren251(x0) % 0.22/0.51 % 532:3:2:INP:TopTop: r1(x0,x1),ren250(x1) -> ren251(x0) % 0.22/0.51 % 533:2:1:INP:Top: p2(x0) -> ren252(x0) % 0.22/0.51 % 534:3:2:INP:TopTop: r1(x0,x1),ren251(x1) -> ren252(x0) % 0.22/0.51 % 535:2:1:INP:Top: p2(x0) -> ren253(x0) % 0.22/0.51 % 536:3:2:INP:TopTop: r1(x0,x1),ren252(x1) -> ren253(x0) % 0.22/0.51 % 537:2:2:INP:TopTop: -> r1(x0,x1),ren254(x0,x1) % 0.22/0.51 % 538:2:2:INP:TopTop: p2(x0) -> ren254(x1,x0) % 0.22/0.51 % 539:3:3:INP:TopTopTop: r1(x0,x1),ren253(x1) -> ren254(x2,x0) % 0.22/0.51 % 540:2:1:INP:Top: p2(x0) -> ren255(x0) % 0.22/0.51 % 541:3:2:INP:TopTop: r1(x0,x1),ren254(x1,skf29(x1)) -> ren255(x0) % 0.22/0.51 % 542:2:1:INP:Top: p2(x0) -> ren256(x0) % 0.22/0.51 % 543:3:2:INP:TopTop: r1(x0,x1),ren255(x1) -> ren256(x0) % 0.22/0.51 % 544:2:1:INP:Top: p2(x0) -> ren257(x0) % 0.22/0.51 % 545:3:2:INP:TopTop: r1(x0,x1),ren256(x1) -> ren257(x0) % 0.22/0.51 % 546:2:1:INP:Top: p2(x0) -> ren258(x0) % 0.22/0.51 % 547:3:2:INP:TopTop: r1(x0,x1),ren257(x1) -> ren258(x0) % 0.22/0.51 % 548:2:1:INP:Top: p2(x0) -> ren259(x0) % 0.22/0.51 % 549:3:2:INP:TopTop: r1(x0,x1),ren258(x1) -> ren259(x0) % 0.22/0.51 % 550:2:1:INP:Top: p2(x0) -> ren260(x0) % 0.22/0.51 % 551:3:2:INP:TopTop: r1(x0,x1),ren259(x1) -> ren260(x0) % 0.22/0.51 % 552:2:1:INP:Top: p2(x0) -> ren261(x0) % 0.22/0.51 % 553:3:2:INP:TopTop: r1(x0,x1),ren260(x1) -> ren261(x0) % 0.22/0.51 % 554:2:2:INP:TopTop: -> r1(x0,x1),ren262(x0,x1) % 0.22/0.51 % 555:2:2:INP:TopTop: p2(x0) -> ren262(x1,x0) % 0.22/0.51 % 556:3:3:INP:TopTopTop: r1(x0,x1),ren261(x1) -> ren262(x2,x0) % 0.22/0.51 % 557:2:1:INP:Top: p2(x0) -> ren263(x0) % 0.22/0.51 % 558:3:2:INP:TopTop: r1(x0,x1),ren262(x1,skf30(x1)) -> ren263(x0) % 0.22/0.51 % 559:2:1:INP:Top: p2(x0) -> ren264(x0) % 0.22/0.51 % 560:3:2:INP:TopTop: r1(x0,x1),ren263(x1) -> ren264(x0) % 0.22/0.51 % 561:2:1:INP:Top: p2(x0) -> ren265(x0) % 0.22/0.51 % 562:3:2:INP:TopTop: r1(x0,x1),ren264(x1) -> ren265(x0) % 0.22/0.51 % 563:2:1:INP:Top: p2(x0) -> ren266(x0) % 0.22/0.51 % 564:3:2:INP:TopTop: r1(x0,x1),ren265(x1) -> ren266(x0) % 0.22/0.51 % 565:2:1:INP:Top: p2(x0) -> ren267(x0) % 0.22/0.51 % 566:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren267(x0) % 0.22/0.51 % 567:2:1:INP:Top: p2(x0) -> ren268(x0) % 0.22/0.51 % 568:3:2:INP:TopTop: r1(x0,x1),ren267(x1) -> ren268(x0) % 0.22/0.51 % 569:2:1:INP:Top: p2(x0) -> ren269(x0) % 0.22/0.51 % 570:3:2:INP:TopTop: r1(x0,x1),ren268(x1) -> ren269(x0) % 0.22/0.51 % 571:2:1:INP:Top: p2(x0) -> ren270(x0) % 0.22/0.51 % 572:3:2:INP:TopTop: r1(x0,x1),ren269(x1) -> ren270(x0) % 0.22/0.51 % 573:2:1:INP:Top: p2(x0) -> ren271(x0) % 0.22/0.51 % 574:3:2:INP:TopTop: r1(x0,x1),ren270(x1) -> ren271(x0) % 0.22/0.51 % 575:2:1:INP:Top: p2(x0) -> ren272(x0) % 0.22/0.51 % 576:3:2:INP:TopTop: r1(x0,x1),ren271(x1) -> ren272(x0) % 0.22/0.51 % 577:2:1:INP:Top: p2(x0) -> ren273(x0) % 0.22/0.51 % 578:3:2:INP:TopTop: r1(x0,x1),ren272(x1) -> ren273(x0) % 0.22/0.51 % 579:2:1:INP:Top: p2(x0) -> ren274(x0) % 0.22/0.51 % 580:3:2:INP:TopTop: r1(x0,x1),ren273(x1) -> ren274(x0) % 0.22/0.51 % 581:2:2:INP:TopTop: -> r1(x0,x1),ren275(x0,x1) % 0.22/0.51 % 582:2:2:INP:TopTop: p2(x0) -> ren275(x1,x0) % 0.22/0.51 % 583:3:3:INP:TopTopTop: r1(x0,x1),ren274(x1) -> ren275(x2,x0) % 0.22/0.51 % 584:2:1:INP:Top: p2(x0) -> ren276(x0) % 0.22/0.51 % 585:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren275(x2,skf31(x2)) -> p1(x1),ren276(x0) % 0.22/0.51 % 586:2:1:INP:Top: p2(x0) -> ren277(x0) % 0.22/0.51 % 587:3:2:INP:TopTop: r1(x0,x1),ren276(x1) -> ren277(x0) % 0.22/0.51 % 588:2:1:INP:Top: p2(x0) -> ren278(x0) % 0.22/0.51 % 589:3:2:INP:TopTop: r1(x0,x1),ren277(x1) -> ren278(x0) % 0.22/0.51 % 590:2:1:INP:Top: p2(x0) -> ren279(x0) % 0.22/0.51 % 591:3:2:INP:TopTop: r1(x0,x1),ren278(x1) -> ren279(x0) % 0.22/0.51 % 592:2:1:INP:Top: p2(x0) -> ren280(x0) % 0.22/0.51 % 593:3:2:INP:TopTop: r1(x0,x1),ren279(x1) -> ren280(x0) % 0.22/0.51 % 594:2:1:INP:Top: p2(x0) -> ren281(x0) % 0.22/0.51 % 595:3:2:INP:TopTop: r1(x0,x1),ren280(x1) -> ren281(x0) % 0.22/0.51 % 596:2:1:INP:Top: p2(x0) -> ren282(x0) % 0.22/0.51 % 597:3:2:INP:TopTop: r1(x0,x1),ren281(x1) -> ren282(x0) % 0.22/0.51 % 598:2:2:INP:TopTop: -> r1(x0,x1),ren283(x0,x1) % 0.22/0.51 % 599:2:2:INP:TopTop: p2(x0) -> ren283(x1,x0) % 0.22/0.51 % 600:3:3:INP:TopTopTop: r1(x0,x1),ren282(x1) -> ren283(x2,x0) % 0.22/0.51 % 601:2:1:INP:Top: p2(x0) -> ren284(x0) % 0.22/0.51 % 602:3:2:INP:TopTop: r1(x0,x1),ren283(x1,skf32(x1)) -> ren284(x0) % 0.22/0.51 % 603:2:1:INP:Top: p2(x0) -> ren285(x0) % 0.22/0.51 % 604:3:2:INP:TopTop: r1(x0,x1),ren284(x1) -> ren285(x0) % 0.22/0.51 % 605:2:1:INP:Top: p2(x0) -> ren286(x0) % 0.22/0.51 % 606:3:2:INP:TopTop: r1(x0,x1),ren285(x1) -> ren286(x0) % 0.22/0.51 % 607:2:1:INP:Top: p2(x0) -> ren287(x0) % 0.22/0.51 % 608:3:2:INP:TopTop: r1(x0,x1),ren286(x1) -> ren287(x0) % 0.22/0.51 % 609:2:1:INP:Top: p2(x0) -> ren288(x0) % 0.22/0.51 % 610:3:2:INP:TopTop: r1(x0,x1),ren287(x1) -> ren288(x0) % 0.22/0.51 % 611:2:1:INP:Top: p2(x0) -> ren289(x0) % 0.22/0.51 % 612:3:2:INP:TopTop: r1(x0,x1),ren288(x1) -> ren289(x0) % 0.22/0.51 % 613:2:1:INP:Top: p2(x0) -> ren290(x0) % 0.22/0.51 % 614:3:2:INP:TopTop: r1(x0,x1),ren289(x1) -> ren290(x0) % 0.22/0.51 % 615:2:2:INP:TopTop: -> r1(x0,x1),ren291(x0,x1) % 0.22/0.51 % 616:2:2:INP:TopTop: p2(x0) -> ren291(x1,x0) % 0.22/0.51 % 617:3:3:INP:TopTopTop: r1(x0,x1),ren290(x1) -> ren291(x2,x0) % 0.22/0.51 % 618:2:1:INP:Top: p2(x0) -> ren292(x0) % 0.22/0.51 % 619:3:2:INP:TopTop: r1(x0,x1),ren291(x1,skf33(x1)) -> ren292(x0) % 0.22/0.51 % 620:2:1:INP:Top: p2(x0) -> ren293(x0) % 0.22/0.51 % 621:3:2:INP:TopTop: r1(x0,x1),ren292(x1) -> ren293(x0) % 0.22/0.51 % 622:2:1:INP:Top: p2(x0) -> ren294(x0) % 0.22/0.51 % 623:3:2:INP:TopTop: r1(x0,x1),ren293(x1) -> ren294(x0) % 0.22/0.51 % 624:2:1:INP:Top: p2(x0) -> ren295(x0) % 0.22/0.51 % 625:3:2:INP:TopTop: r1(x0,x1),ren294(x1) -> ren295(x0) % 0.22/0.51 % 626:2:1:INP:Top: p2(x0) -> ren296(x0) % 0.22/0.51 % 627:3:2:INP:TopTop: r1(x0,x1),ren295(x1) -> ren296(x0) % 0.22/0.51 % 628:2:1:INP:Top: p2(x0) -> ren297(x0) % 0.22/0.51 % 629:3:2:INP:TopTop: r1(x0,x1),ren296(x1) -> ren297(x0) % 0.22/0.51 % 630:2:1:INP:Top: p2(x0) -> ren298(x0) % 0.22/0.51 % 631:3:2:INP:TopTop: r1(x0,x1),ren297(x1) -> ren298(x0) % 0.22/0.51 % 632:2:2:INP:TopTop: -> r1(x0,x1),ren299(x0,x1) % 0.22/0.51 % 633:2:2:INP:TopTop: p2(x0) -> ren299(x1,x0) % 0.22/0.51 % 634:3:3:INP:TopTopTop: r1(x0,x1),ren298(x1) -> ren299(x2,x0) % 0.22/0.51 % 635:2:1:INP:Top: p2(x0) -> ren300(x0) % 0.22/0.51 % 636:3:2:INP:TopTop: r1(x0,x1),ren299(x1,skf34(x1)) -> ren300(x0) % 0.22/0.51 % 637:2:1:INP:Top: p2(x0) -> ren301(x0) % 0.22/0.51 % 638:3:2:INP:TopTop: r1(x0,x1),ren300(x1) -> ren301(x0) % 0.22/0.51 % 639:2:1:INP:Top: p2(x0) -> ren302(x0) % 0.22/0.51 % 640:3:2:INP:TopTop: r1(x0,x1),ren301(x1) -> ren302(x0) % 0.22/0.51 % 641:2:1:INP:Top: p2(x0) -> ren303(x0) % 0.22/0.51 % 642:3:2:INP:TopTop: r1(x0,x1),ren302(x1) -> ren303(x0) % 0.22/0.51 % 643:2:1:INP:Top: p2(x0) -> ren304(x0) % 0.22/0.51 % 644:3:2:INP:TopTop: r1(x0,x1),ren303(x1) -> ren304(x0) % 0.22/0.51 % 645:2:1:INP:Top: p2(x0) -> ren305(x0) % 0.22/0.51 % 646:3:2:INP:TopTop: r1(x0,x1),ren304(x1) -> ren305(x0) % 0.22/0.51 % 647:2:1:INP:Top: p2(x0) -> ren306(x0) % 0.22/0.51 % 648:3:2:INP:TopTop: r1(x0,x1),ren305(x1) -> ren306(x0) % 0.22/0.51 % 649:2:2:INP:TopTop: -> r1(x0,x1),ren307(x0,x1) % 0.22/0.51 % 650:2:2:INP:TopTop: p2(x0) -> ren307(x1,x0) % 0.22/0.51 % 651:3:3:INP:TopTopTop: r1(x0,x1),ren306(x1) -> ren307(x2,x0) % 0.22/0.51 % 652:2:1:INP:Top: p2(x0) -> ren308(x0) % 0.22/0.51 % 653:3:2:INP:TopTop: r1(x0,x1),ren307(x1,skf35(x1)) -> ren308(x0) % 0.22/0.51 % 654:2:1:INP:Top: p2(x0) -> ren309(x0) % 0.22/0.51 % 655:3:2:INP:TopTop: r1(x0,x1),ren308(x1) -> ren309(x0) % 0.22/0.51 % 656:2:1:INP:Top: p2(x0) -> ren310(x0) % 0.22/0.51 % 657:3:2:INP:TopTop: r1(x0,x1),ren309(x1) -> ren310(x0) % 0.22/0.51 % 658:2:1:INP:Top: p2(x0) -> ren311(x0) % 0.22/0.51 % 659:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren311(x0) % 0.22/0.51 % 660:2:1:INP:Top: p2(x0) -> ren312(x0) % 0.22/0.51 % 661:3:2:INP:TopTop: r1(x0,x1),ren311(x1) -> ren312(x0) % 0.22/0.51 % 662:2:1:INP:Top: p2(x0) -> ren313(x0) % 0.22/0.51 % 663:3:2:INP:TopTop: r1(x0,x1),ren312(x1) -> ren313(x0) % 0.22/0.51 % 664:2:1:INP:Top: p2(x0) -> ren314(x0) % 0.22/0.51 % 665:3:2:INP:TopTop: r1(x0,x1),ren313(x1) -> ren314(x0) % 0.22/0.51 % 666:2:1:INP:Top: p2(x0) -> ren315(x0) % 0.22/0.51 % 667:3:2:INP:TopTop: r1(x0,x1),ren314(x1) -> ren315(x0) % 0.22/0.51 % 668:2:1:INP:Top: p2(x0) -> ren316(x0) % 0.22/0.51 % 669:3:2:INP:TopTop: r1(x0,x1),ren315(x1) -> ren316(x0) % 0.22/0.51 % 670:2:1:INP:Top: p2(x0) -> ren317(x0) % 0.22/0.51 % 671:3:2:INP:TopTop: r1(x0,x1),ren316(x1) -> ren317(x0) % 0.22/0.51 % 672:2:1:INP:Top: p2(x0) -> ren318(x0) % 0.22/0.51 % 673:3:2:INP:TopTop: r1(x0,x1),ren317(x1) -> ren318(x0) % 0.22/0.51 % 674:2:2:INP:TopTop: -> r1(x0,x1),ren319(x0,x1) % 0.22/0.51 % 675:2:2:INP:TopTop: p2(x0) -> ren319(x1,x0) % 0.22/0.51 % 676:3:3:INP:TopTopTop: r1(x0,x1),ren318(x1) -> ren319(x2,x0) % 0.22/0.51 % 677:2:1:INP:Top: p2(x0) -> ren320(x0) % 0.22/0.51 % 678:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren319(x2,skf36(x2)) -> p1(x1),ren320(x0) % 0.22/0.51 % 679:2:1:INP:Top: p2(x0) -> ren321(x0) % 0.22/0.51 % 680:3:2:INP:TopTop: r1(x0,x1),ren320(x1) -> ren321(x0) % 0.22/0.51 % 681:2:1:INP:Top: p2(x0) -> ren322(x0) % 0.22/0.51 % 682:3:2:INP:TopTop: r1(x0,x1),ren321(x1) -> ren322(x0) % 0.22/0.51 % 683:2:1:INP:Top: p2(x0) -> ren323(x0) % 0.22/0.51 % 684:3:2:INP:TopTop: r1(x0,x1),ren322(x1) -> ren323(x0) % 0.22/0.51 % 685:2:1:INP:Top: p2(x0) -> ren324(x0) % 0.22/0.51 % 686:3:2:INP:TopTop: r1(x0,x1),ren323(x1) -> ren324(x0) % 0.22/0.51 % 687:2:1:INP:Top: p2(x0) -> ren325(x0) % 0.22/0.51 % 688:3:2:INP:TopTop: r1(x0,x1),ren324(x1) -> ren325(x0) % 0.22/0.51 % 689:2:1:INP:Top: p2(x0) -> ren326(x0) % 0.22/0.51 % 690:3:2:INP:TopTop: r1(x0,x1),ren325(x1) -> ren326(x0) % 0.22/0.51 % 691:2:2:INP:TopTop: -> r1(x0,x1),ren327(x0,x1) % 0.22/0.51 % 692:2:2:INP:TopTop: p2(x0) -> ren327(x1,x0) % 0.22/0.51 % 693:3:3:INP:TopTopTop: r1(x0,x1),ren326(x1) -> ren327(x2,x0) % 0.22/0.51 % 694:2:1:INP:Top: p2(x0) -> ren328(x0) % 0.22/0.51 % 695:3:2:INP:TopTop: r1(x0,x1),ren327(x1,skf37(x1)) -> ren328(x0) % 0.22/0.51 % 696:2:1:INP:Top: p2(x0) -> ren329(x0) % 0.22/0.51 % 697:3:2:INP:TopTop: r1(x0,x1),ren328(x1) -> ren329(x0) % 0.22/0.51 % 698:2:1:INP:Top: p2(x0) -> ren330(x0) % 0.22/0.51 % 699:3:2:INP:TopTop: r1(x0,x1),ren329(x1) -> ren330(x0) % 0.22/0.51 % 700:2:1:INP:Top: p2(x0) -> ren331(x0) % 0.22/0.51 % 701:3:2:INP:TopTop: r1(x0,x1),ren330(x1) -> ren331(x0) % 0.22/0.51 % 702:2:1:INP:Top: p2(x0) -> ren332(x0) % 0.22/0.51 % 703:3:2:INP:TopTop: r1(x0,x1),ren331(x1) -> ren332(x0) % 0.22/0.51 % 704:2:1:INP:Top: p2(x0) -> ren333(x0) % 0.22/0.51 % 705:3:2:INP:TopTop: r1(x0,x1),ren332(x1) -> ren333(x0) % 0.22/0.51 % 706:2:1:INP:Top: p2(x0) -> ren334(x0) % 0.22/0.51 % 707:3:2:INP:TopTop: r1(x0,x1),ren333(x1) -> ren334(x0) % 0.22/0.51 % 708:2:2:INP:TopTop: -> r1(x0,x1),ren335(x0,x1) % 0.22/0.51 % 709:2:2:INP:TopTop: p2(x0) -> ren335(x1,x0) % 0.22/0.51 % 710:3:3:INP:TopTopTop: r1(x0,x1),ren334(x1) -> ren335(x2,x0) % 0.22/0.51 % 711:2:1:INP:Top: p2(x0) -> ren336(x0) % 0.22/0.51 % 712:3:2:INP:TopTop: r1(x0,x1),ren335(x1,skf38(x1)) -> ren336(x0) % 0.22/0.51 % 713:2:1:INP:Top: p2(x0) -> ren337(x0) % 0.22/0.51 % 714:3:2:INP:TopTop: r1(x0,x1),ren336(x1) -> ren337(x0) % 0.22/0.51 % 715:2:1:INP:Top: p2(x0) -> ren338(x0) % 0.22/0.51 % 716:3:2:INP:TopTop: r1(x0,x1),ren337(x1) -> ren338(x0) % 0.22/0.51 % 717:2:1:INP:Top: p2(x0) -> ren339(x0) % 0.22/0.51 % 718:3:2:INP:TopTop: r1(x0,x1),ren338(x1) -> ren339(x0) % 0.22/0.51 % 719:2:1:INP:Top: p2(x0) -> ren340(x0) % 0.22/0.51 % 720:3:2:INP:TopTop: r1(x0,x1),ren339(x1) -> ren340(x0) % 0.22/0.51 % 721:2:1:INP:Top: p2(x0) -> ren341(x0) % 0.22/0.51 % 722:3:2:INP:TopTop: r1(x0,x1),ren340(x1) -> ren341(x0) % 0.22/0.51 % 723:2:1:INP:Top: p2(x0) -> ren342(x0) % 0.22/0.51 % 724:3:2:INP:TopTop: r1(x0,x1),ren341(x1) -> ren342(x0) % 0.22/0.51 % 725:2:2:INP:TopTop: -> r1(x0,x1),ren343(x0,x1) % 0.22/0.51 % 726:2:2:INP:TopTop: p2(x0) -> ren343(x1,x0) % 0.22/0.51 % 727:3:3:INP:TopTopTop: r1(x0,x1),ren342(x1) -> ren343(x2,x0) % 0.22/0.51 % 728:2:1:INP:Top: p2(x0) -> ren344(x0) % 0.22/0.51 % 729:3:2:INP:TopTop: r1(x0,x1),ren343(x1,skf39(x1)) -> ren344(x0) % 0.22/0.51 % 730:2:1:INP:Top: p2(x0) -> ren345(x0) % 0.22/0.51 % 731:3:2:INP:TopTop: r1(x0,x1),ren344(x1) -> ren345(x0) % 0.22/0.51 % 732:2:1:INP:Top: p2(x0) -> ren346(x0) % 0.22/0.51 % 733:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren346(x0) % 0.22/0.51 % 734:2:1:INP:Top: p2(x0) -> ren347(x0) % 0.22/0.51 % 735:3:2:INP:TopTop: r1(x0,x1),ren346(x1) -> ren347(x0) % 0.22/0.51 % 736:2:1:INP:Top: p2(x0) -> ren348(x0) % 0.22/0.51 % 737:3:2:INP:TopTop: r1(x0,x1),ren347(x1) -> ren348(x0) % 0.22/0.51 % 738:2:1:INP:Top: p2(x0) -> ren349(x0) % 0.22/0.51 % 739:3:2:INP:TopTop: r1(x0,x1),ren348(x1) -> ren349(x0) % 0.22/0.51 % 740:2:1:INP:Top: p2(x0) -> ren350(x0) % 0.22/0.51 % 741:3:2:INP:TopTop: r1(x0,x1),ren349(x1) -> ren350(x0) % 0.22/0.51 % 742:2:1:INP:Top: p2(x0) -> ren351(x0) % 0.22/0.51 % 743:3:2:INP:TopTop: r1(x0,x1),ren350(x1) -> ren351(x0) % 0.22/0.51 % 744:2:1:INP:Top: p2(x0) -> ren352(x0) % 0.22/0.51 % 745:3:2:INP:TopTop: r1(x0,x1),ren351(x1) -> ren352(x0) % 0.22/0.51 % 746:2:1:INP:Top: p2(x0) -> ren353(x0) % 0.22/0.51 % 747:3:2:INP:TopTop: r1(x0,x1),ren352(x1) -> ren353(x0) % 0.22/0.51 % 748:2:2:INP:TopTop: -> r1(x0,x1),ren354(x0,x1) % 0.22/0.51 % 749:2:2:INP:TopTop: p2(x0) -> ren354(x1,x0) % 0.22/0.51 % 750:3:3:INP:TopTopTop: r1(x0,x1),ren353(x1) -> ren354(x2,x0) % 0.22/0.51 % 751:2:1:INP:Top: p2(x0) -> ren355(x0) % 0.22/0.51 % 752:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren354(x2,skf40(x2)) -> p1(x1),ren355(x0) % 0.22/0.51 % 753:2:1:INP:Top: p2(x0) -> ren356(x0) % 0.22/0.51 % 754:3:2:INP:TopTop: r1(x0,x1),ren355(x1) -> ren356(x0) % 0.22/0.51 % 755:2:1:INP:Top: p2(x0) -> ren357(x0) % 0.22/0.51 % 756:3:2:INP:TopTop: r1(x0,x1),ren356(x1) -> ren357(x0) % 0.22/0.51 % 757:2:1:INP:Top: p2(x0) -> ren358(x0) % 0.22/0.51 % 758:3:2:INP:TopTop: r1(x0,x1),ren357(x1) -> ren358(x0) % 0.22/0.51 % 759:2:1:INP:Top: p2(x0) -> ren359(x0) % 0.22/0.51 % 760:3:2:INP:TopTop: r1(x0,x1),ren358(x1) -> ren359(x0) % 0.22/0.51 % 761:2:1:INP:Top: p2(x0) -> ren360(x0) % 0.22/0.51 % 762:3:2:INP:TopTop: r1(x0,x1),ren359(x1) -> ren360(x0) % 0.22/0.51 % 763:2:1:INP:Top: p2(x0) -> ren361(x0) % 0.22/0.51 % 764:3:2:INP:TopTop: r1(x0,x1),ren360(x1) -> ren361(x0) % 0.22/0.51 % 765:2:2:INP:TopTop: -> r1(x0,x1),ren362(x0,x1) % 0.22/0.51 % 766:2:2:INP:TopTop: p2(x0) -> ren362(x1,x0) % 0.22/0.51 % 767:3:3:INP:TopTopTop: r1(x0,x1),ren361(x1) -> ren362(x2,x0) % 0.22/0.51 % 768:2:1:INP:Top: p2(x0) -> ren363(x0) % 0.22/0.51 % 769:3:2:INP:TopTop: r1(x0,x1),ren362(x1,skf41(x1)) -> ren363(x0) % 0.22/0.51 % 770:2:1:INP:Top: p2(x0) -> ren364(x0) % 0.22/0.51 % 771:3:2:INP:TopTop: r1(x0,x1),ren363(x1) -> ren364(x0) % 0.22/0.51 % 772:2:1:INP:Top: p2(x0) -> ren365(x0) % 0.22/0.51 % 773:3:2:INP:TopTop: r1(x0,x1),ren364(x1) -> ren365(x0) % 0.22/0.51 % 774:2:1:INP:Top: p2(x0) -> ren366(x0) % 0.22/0.51 % 775:3:2:INP:TopTop: r1(x0,x1),ren365(x1) -> ren366(x0) % 0.22/0.51 % 776:2:1:INP:Top: p2(x0) -> ren367(x0) % 0.22/0.51 % 777:3:2:INP:TopTop: r1(x0,x1),ren366(x1) -> ren367(x0) % 0.22/0.51 % 778:2:1:INP:Top: p2(x0) -> ren368(x0) % 0.22/0.51 % 779:3:2:INP:TopTop: r1(x0,x1),ren367(x1) -> ren368(x0) % 0.22/0.51 % 780:2:1:INP:Top: p2(x0) -> ren369(x0) % 0.22/0.51 % 781:3:2:INP:TopTop: r1(x0,x1),ren368(x1) -> ren369(x0) % 0.22/0.51 % 782:2:2:INP:TopTop: -> r1(x0,x1),ren370(x0,x1) % 0.22/0.51 % 783:2:2:INP:TopTop: p2(x0) -> ren370(x1,x0) % 0.22/0.51 % 784:3:3:INP:TopTopTop: r1(x0,x1),ren369(x1) -> ren370(x2,x0) % 0.22/0.51 % 785:2:1:INP:Top: p2(x0) -> ren371(x0) % 0.22/0.51 % 786:3:2:INP:TopTop: r1(x0,x1),ren370(x1,skf42(x1)) -> ren371(x0) % 0.22/0.51 % 787:2:1:INP:Top: p2(x0) -> ren372(x0) % 0.22/0.51 % 788:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren372(x0) % 0.22/0.51 % 789:2:1:INP:Top: p2(x0) -> ren373(x0) % 0.22/0.51 % 790:3:2:INP:TopTop: r1(x0,x1),ren372(x1) -> ren373(x0) % 0.22/0.51 % 791:2:1:INP:Top: p2(x0) -> ren374(x0) % 0.22/0.51 % 792:3:2:INP:TopTop: r1(x0,x1),ren373(x1) -> ren374(x0) % 0.22/0.51 % 793:2:1:INP:Top: p2(x0) -> ren375(x0) % 0.22/0.51 % 794:3:2:INP:TopTop: r1(x0,x1),ren374(x1) -> ren375(x0) % 0.22/0.51 % 795:2:1:INP:Top: p2(x0) -> ren376(x0) % 0.22/0.51 % 796:3:2:INP:TopTop: r1(x0,x1),ren375(x1) -> ren376(x0) % 0.22/0.51 % 797:2:1:INP:Top: p2(x0) -> ren377(x0) % 0.22/0.51 % 798:3:2:INP:TopTop: r1(x0,x1),ren376(x1) -> ren377(x0) % 0.22/0.51 % 799:2:1:INP:Top: p2(x0) -> ren378(x0) % 0.22/0.51 % 800:3:2:INP:TopTop: r1(x0,x1),ren377(x1) -> ren378(x0) % 0.22/0.51 % 801:2:1:INP:Top: p2(x0) -> ren379(x0) % 0.22/0.51 % 802:3:2:INP:TopTop: r1(x0,x1),ren378(x1) -> ren379(x0) % 0.22/0.51 % 803:2:2:INP:TopTop: -> r1(x0,x1),ren380(x0,x1) % 0.22/0.51 % 804:2:2:INP:TopTop: p2(x0) -> ren380(x1,x0) % 0.22/0.51 % 805:3:3:INP:TopTopTop: r1(x0,x1),ren379(x1) -> ren380(x2,x0) % 0.22/0.51 % 806:2:1:INP:Top: p2(x0) -> ren381(x0) % 0.22/0.51 % 807:5:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2),ren380(x2,skf43(x2)) -> p1(x1),ren381(x0) % 0.22/0.51 % 808:2:1:INP:Top: p2(x0) -> ren382(x0) % 0.22/0.51 % 809:3:2:INP:TopTop: r1(x0,x1),ren381(x1) -> ren382(x0) % 0.22/0.51 % 810:2:1:INP:Top: p2(x0) -> ren383(x0) % 0.22/0.51 % 811:3:2:INP:TopTop: r1(x0,x1),ren382(x1) -> ren383(x0) % 0.22/0.51 % 812:2:1:INP:Top: p2(x0) -> ren384(x0) % 0.22/0.51 % 813:3:2:INP:TopTop: r1(x0,x1),ren383(x1) -> ren384(x0) % 0.22/0.51 % 814:2:1:INP:Top: p2(x0) -> ren385(x0) % 0.22/0.51 % 815:3:2:INP:TopTop: r1(x0,x1),ren384(x1) -> ren385(x0) % 0.22/0.51 % 816:2:1:INP:Top: p2(x0) -> ren386(x0) % 0.22/0.51 % 817:3:2:INP:TopTop: r1(x0,x1),ren385(x1) -> ren386(x0) % 0.22/0.51 % 818:2:1:INP:Top: p2(x0) -> ren387(x0) % 0.22/0.51 % 819:3:2:INP:TopTop: r1(x0,x1),ren386(x1) -> ren387(x0) % 0.22/0.51 % 820:2:2:INP:TopTop: -> r1(x0,x1),ren388(x0,x1) % 0.22/0.51 % 821:2:2:INP:TopTop: p2(x0) -> ren388(x1,x0) % 0.22/0.51 % 822:3:3:INP:TopTopTop: r1(x0,x1),ren387(x1) -> ren388(x2,x0) % 0.22/0.51 % 823:2:1:INP:Top: p2(x0) -> ren389(x0) % 0.22/0.51 % 824:3:2:INP:TopTop: r1(x0,x1),p1(x1) -> ren389(x0) % 0.67/0.98 % 825:2:1:INP:Top: p2(x0) -> ren390(x0) % 0.67/0.98 % 826:3:2:INP:TopTop: r1(x0,x1),ren389(x1) -> ren390(x0) % 0.67/0.98 % 827:2:1:INP:Top: p2(x0) -> ren391(x0) % 0.67/0.98 % 828:3:2:INP:TopTop: r1(x0,x1),ren390(x1) -> ren391(x0) % 0.67/0.98 % 829:2:1:INP:Top: p2(x0) -> ren392(x0) % 0.67/0.98 % 830:3:2:INP:TopTop: r1(x0,x1),ren391(x1) -> ren392(x0) % 0.67/0.98 % 831:2:1:INP:Top: p2(x0) -> ren393(x0) % 0.67/0.98 % 832:3:2:INP:TopTop: r1(x0,x1),ren392(x1) -> ren393(x0) % 0.67/0.98 % 833:2:1:INP:Top: p2(x0) -> ren394(x0) % 0.67/0.98 % 834:3:2:INP:TopTop: r1(x0,x1),ren393(x1) -> ren394(x0) % 0.67/0.98 % 835:2:1:INP:Top: p2(x0) -> ren395(x0) % 0.67/0.98 % 836:3:2:INP:TopTop: r1(x0,x1),ren394(x1) -> ren395(x0) % 0.67/0.98 % 837:2:1:INP:Top: p2(x0) -> ren396(x0) % 0.67/0.98 % 838:3:2:INP:TopTop: r1(x0,x1),ren395(x1) -> ren396(x0) % 0.67/0.98 % 839:2:2:INP:TopTop: -> r1(x0,x1),ren397(x0,x1) % 0.67/0.98 % 840:2:2:INP:TopTop: p2(x0) -> ren397(x1,x0) % 0.67/0.98 % 841:3:3:INP:TopTopTop: r1(x0,x1),ren396(x1) -> ren397(x2,x0) % 0.67/0.98 % 0.67/0.98 % Reduced Input Conjecture Clauses: % 0.67/0.98 % 859:1:0:INP:: p1(skc44) -> % 0.67/0.98 % 843:2:1:INP:Top: r1(skc44,x0),ren80(x0) -> % 0.67/0.98 % 860:2:1:[859.0,858.2]:Top: r1(skc44,x0),ren397(x0,skf46(x0)) -> % 0.67/0.98 % 845:2:1:INP:Top: r1(skc44,x0),ren151(x0) -> % 0.67/0.98 % 857:2:1:INP:Top: r1(skc44,x0),ren388(x0,skf45(x0)) -> % 0.67/0.98 % 847:2:1:INP:Top: r1(skc44,x0),ren213(x0) -> % 0.67/0.98 % 856:1:0:INP:: p2(skc44) -> % 0.67/0.98 % 849:2:1:INP:Top: r1(skc44,x0),ren266(x0) -> % 0.67/0.98 % 855:2:1:INP:Top: r1(skc44,x0),ren371(x0) -> % 0.67/0.98 % 851:2:1:INP:Top: r1(skc44,x0),ren310(x0) -> % 0.67/0.98 % 853:2:1:INP:Top: r1(skc44,x0),ren345(x0) -> % 0.67/0.98 % 0.67/0.98 % 0.67/0.98 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 446 atoms initially. Used heuristic: lmodel_grow === % 0.67/0.98 % 0.67/0.98 % 0.67/0.98 % 0.67/0.98 % Linear Model Building succeeded. % 0.67/0.98 % SZS status CounterSatisfiable % 0.67/0.98 % 0.67/0.98 % 0.67/0.98 % SZS status CounterSatisfiable % 0.67/0.98 % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.67/0.98 % 0.67/0.98 % SPASS-SCL-FOL Statistics: % 0.67/0.98 % Number of learned clauses: 0 % 0.67/0.98 % Number of propagations: 2463 % 0.67/0.98 % Number of decisions: 98 % 0.67/0.98 % Number of resolutions: 0 % 0.67/0.98 % Number of condensations: 0 % 0.67/0.98 % Number of sub resolutions: 1 % 0.67/0.98 % 0.67/0.98 % Solver is done. Empty clause found % 0.67/0.98 % 0.67/0.98 % Needed: 0:00:00.59 % 0.67/0.98 % 0.67/0.98 % ### % 0.67/0.98 % ### Pagesize: 8192 % 0.67/0.98 % ### Marksize: 0 % 0.67/0.98 % ### Memory demanded: 25194 KBytes % 0.67/0.98 % ### Memory freed: 25194 KBytes % 0.67/0.98 % ### Memory remaining: 0 Bytes % 0.67/0.98 % ### Pages allocated: 2483 Pages % 0.67/0.98 % ### %------------------------------------------------------------------------------