%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1.1 % Problem : LCL657+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n016.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:00 PM UTC 2026 % Result : Timeout 299.79s 300.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : LCL657+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.42 % Computer : n016.cluster.edu % 0.17/0.42 % Model : x86_64 x86_64 % 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.42 % Memory : 8046.5625MB % 0.17/0.42 % OS : Linux 6.8.0-71-generic % 0.17/0.42 % CPULimit : 300 % 0.17/0.42 % WCLimit : 300 % 0.17/0.42 % DateTime : Sat Sep 5 23:14:15 UTC 2026 % 0.17/0.43 % CPUTime : % 0.17/0.43 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.44 % 0.17/0.44 % Input Clauses: % 0.17/0.44 % 1:1:1:INP:Top: -> r1(x0,x0) % 0.17/0.44 % 2:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0)) % 0.17/0.44 % 3:2:1:INP:Top: ren1(x0),p21(skf1(x0)) -> % 0.17/0.44 % 4:2:1:INP:Top: ren1(x0),p121(skf1(x0)) -> % 0.17/0.44 % 5:2:1:INP:Top: ren1(x0) -> p120(skf1(x0)) % 0.17/0.44 % 6:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0)) % 0.17/0.44 % 7:2:1:INP:Top: ren1(x0) -> p21(skf2(x0)) % 0.17/0.44 % 8:2:1:INP:Top: ren1(x0),p121(skf2(x0)) -> % 0.17/0.44 % 9:2:1:INP:Top: ren1(x0) -> p120(skf2(x0)) % 0.17/0.44 % 10:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0)) % 0.17/0.44 % 11:2:1:INP:Top: ren2(x0),p20(skf3(x0)) -> % 0.17/0.44 % 12:2:1:INP:Top: ren2(x0),p120(skf3(x0)) -> % 0.17/0.44 % 13:2:1:INP:Top: ren2(x0) -> p119(skf3(x0)) % 0.17/0.44 % 14:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0)) % 0.17/0.44 % 15:2:1:INP:Top: ren2(x0) -> p20(skf4(x0)) % 0.17/0.44 % 16:2:1:INP:Top: ren2(x0),p120(skf4(x0)) -> % 0.17/0.44 % 17:2:1:INP:Top: ren2(x0) -> p119(skf4(x0)) % 0.17/0.44 % 18:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0)) % 0.17/0.44 % 19:2:1:INP:Top: ren3(x0),p19(skf5(x0)) -> % 0.17/0.44 % 20:2:1:INP:Top: ren3(x0),p119(skf5(x0)) -> % 0.17/0.44 % 21:2:1:INP:Top: ren3(x0) -> p118(skf5(x0)) % 0.17/0.44 % 22:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0)) % 0.17/0.44 % 23:2:1:INP:Top: ren3(x0) -> p19(skf6(x0)) % 0.17/0.44 % 24:2:1:INP:Top: ren3(x0),p119(skf6(x0)) -> % 0.17/0.44 % 25:2:1:INP:Top: ren3(x0) -> p118(skf6(x0)) % 0.17/0.44 % 26:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0)) % 0.17/0.44 % 27:2:1:INP:Top: ren4(x0),p18(skf7(x0)) -> % 0.17/0.44 % 28:2:1:INP:Top: ren4(x0),p118(skf7(x0)) -> % 0.17/0.44 % 29:2:1:INP:Top: ren4(x0) -> p117(skf7(x0)) % 0.17/0.44 % 30:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0)) % 0.17/0.44 % 31:2:1:INP:Top: ren4(x0) -> p18(skf8(x0)) % 0.17/0.44 % 32:2:1:INP:Top: ren4(x0),p118(skf8(x0)) -> % 0.17/0.44 % 33:2:1:INP:Top: ren4(x0) -> p117(skf8(x0)) % 0.17/0.44 % 34:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0)) % 0.17/0.44 % 35:2:1:INP:Top: ren5(x0),p17(skf9(x0)) -> % 0.17/0.44 % 36:2:1:INP:Top: ren5(x0),p117(skf9(x0)) -> % 0.17/0.44 % 37:2:1:INP:Top: ren5(x0) -> p116(skf9(x0)) % 0.17/0.44 % 38:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0)) % 0.17/0.44 % 39:2:1:INP:Top: ren5(x0) -> p17(skf10(x0)) % 0.17/0.44 % 40:2:1:INP:Top: ren5(x0),p117(skf10(x0)) -> % 0.17/0.44 % 41:2:1:INP:Top: ren5(x0) -> p116(skf10(x0)) % 0.17/0.44 % 42:2:1:INP:Top: ren6(x0) -> r1(x0,skf11(x0)) % 0.17/0.44 % 43:2:1:INP:Top: ren6(x0),p16(skf11(x0)) -> % 0.17/0.44 % 44:2:1:INP:Top: ren6(x0),p116(skf11(x0)) -> % 0.17/0.44 % 45:2:1:INP:Top: ren6(x0) -> p115(skf11(x0)) % 0.17/0.44 % 46:2:1:INP:Top: ren6(x0) -> r1(x0,skf12(x0)) % 0.17/0.44 % 47:2:1:INP:Top: ren6(x0) -> p16(skf12(x0)) % 0.17/0.44 % 48:2:1:INP:Top: ren6(x0),p116(skf12(x0)) -> % 0.17/0.44 % 49:2:1:INP:Top: ren6(x0) -> p115(skf12(x0)) % 0.17/0.44 % 50:2:1:INP:Top: ren7(x0) -> r1(x0,skf13(x0)) % 0.17/0.44 % 51:2:1:INP:Top: ren7(x0),p15(skf13(x0)) -> % 0.17/0.44 % 52:2:1:INP:Top: ren7(x0),p115(skf13(x0)) -> % 0.17/0.44 % 53:2:1:INP:Top: ren7(x0) -> p114(skf13(x0)) % 0.17/0.44 % 54:2:1:INP:Top: ren7(x0) -> r1(x0,skf14(x0)) % 0.17/0.44 % 55:2:1:INP:Top: ren7(x0) -> p15(skf14(x0)) % 0.17/0.44 % 56:2:1:INP:Top: ren7(x0),p115(skf14(x0)) -> % 0.17/0.44 % 57:2:1:INP:Top: ren7(x0) -> p114(skf14(x0)) % 0.17/0.44 % 58:2:1:INP:Top: ren8(x0) -> r1(x0,skf15(x0)) % 0.17/0.44 % 59:2:1:INP:Top: ren8(x0),p14(skf15(x0)) -> % 0.17/0.44 % 60:2:1:INP:Top: ren8(x0),p114(skf15(x0)) -> % 0.17/0.44 % 61:2:1:INP:Top: ren8(x0) -> p113(skf15(x0)) % 0.17/0.44 % 62:2:1:INP:Top: ren8(x0) -> r1(x0,skf16(x0)) % 0.17/0.44 % 63:2:1:INP:Top: ren8(x0) -> p14(skf16(x0)) % 0.17/0.44 % 64:2:1:INP:Top: ren8(x0),p114(skf16(x0)) -> % 0.17/0.44 % 65:2:1:INP:Top: ren8(x0) -> p113(skf16(x0)) % 0.17/0.44 % 66:2:1:INP:Top: ren9(x0) -> r1(x0,skf17(x0)) % 0.17/0.44 % 67:2:1:INP:Top: ren9(x0),p13(skf17(x0)) -> % 0.17/0.44 % 68:2:1:INP:Top: ren9(x0),p113(skf17(x0)) -> % 0.17/0.44 % 69:2:1:INP:Top: ren9(x0) -> p112(skf17(x0)) % 0.17/0.44 % 70:2:1:INP:Top: ren9(x0) -> r1(x0,skf18(x0)) % 0.17/0.44 % 71:2:1:INP:Top: ren9(x0) -> p13(skf18(x0)) % 0.17/0.44 % 72:2:1:INP:Top: ren9(x0),p113(skf18(x0)) -> % 0.17/0.44 % 73:2:1:INP:Top: ren9(x0) -> p112(skf18(x0)) % 0.17/0.44 % 74:2:1:INP:Top: ren10(x0) -> r1(x0,skf19(x0)) % 0.17/0.44 % 75:2:1:INP:Top: ren10(x0),p12(skf19(x0)) -> % 0.17/0.44 % 76:2:1:INP:Top: ren10(x0),p112(skf19(x0)) -> % 0.17/0.44 % 77:2:1:INP:Top: ren10(x0) -> p111(skf19(x0)) % 0.17/0.44 % 78:2:1:INP:Top: ren10(x0) -> r1(x0,skf20(x0)) % 0.17/0.44 % 79:2:1:INP:Top: ren10(x0) -> p12(skf20(x0)) % 0.17/0.44 % 80:2:1:INP:Top: ren10(x0),p112(skf20(x0)) -> % 0.17/0.44 % 81:2:1:INP:Top: ren10(x0) -> p111(skf20(x0)) % 0.17/0.44 % 82:2:1:INP:Top: ren11(x0) -> r1(x0,skf21(x0)) % 0.17/0.44 % 83:2:1:INP:Top: ren11(x0),p11(skf21(x0)) -> % 0.17/0.44 % 84:2:1:INP:Top: ren11(x0),p111(skf21(x0)) -> % 0.17/0.44 % 85:2:1:INP:Top: ren11(x0) -> p110(skf21(x0)) % 0.17/0.44 % 86:2:1:INP:Top: ren11(x0) -> r1(x0,skf22(x0)) % 0.17/0.44 % 87:2:1:INP:Top: ren11(x0) -> p11(skf22(x0)) % 0.17/0.44 % 88:2:1:INP:Top: ren11(x0),p111(skf22(x0)) -> % 0.17/0.44 % 89:2:1:INP:Top: ren11(x0) -> p110(skf22(x0)) % 0.17/0.44 % 90:2:1:INP:Top: ren12(x0) -> r1(x0,skf23(x0)) % 0.17/0.44 % 91:2:1:INP:Top: ren12(x0),p10(skf23(x0)) -> % 0.17/0.44 % 92:2:1:INP:Top: ren12(x0),p110(skf23(x0)) -> % 0.17/0.44 % 93:2:1:INP:Top: ren12(x0) -> p109(skf23(x0)) % 0.17/0.44 % 94:2:1:INP:Top: ren12(x0) -> r1(x0,skf24(x0)) % 0.17/0.44 % 95:2:1:INP:Top: ren12(x0) -> p10(skf24(x0)) % 0.17/0.44 % 96:2:1:INP:Top: ren12(x0),p110(skf24(x0)) -> % 0.17/0.44 % 97:2:1:INP:Top: ren12(x0) -> p109(skf24(x0)) % 0.17/0.44 % 98:2:1:INP:Top: ren13(x0) -> r1(x0,skf25(x0)) % 0.17/0.44 % 99:2:1:INP:Top: ren13(x0),p9(skf25(x0)) -> % 0.17/0.44 % 100:2:1:INP:Top: ren13(x0),p109(skf25(x0)) -> % 0.17/0.44 % 101:2:1:INP:Top: ren13(x0) -> p108(skf25(x0)) % 0.17/0.44 % 102:2:1:INP:Top: ren13(x0) -> r1(x0,skf26(x0)) % 0.17/0.44 % 103:2:1:INP:Top: ren13(x0) -> p9(skf26(x0)) % 0.17/0.44 % 104:2:1:INP:Top: ren13(x0),p109(skf26(x0)) -> % 0.17/0.44 % 105:2:1:INP:Top: ren13(x0) -> p108(skf26(x0)) % 0.17/0.44 % 106:2:1:INP:Top: ren14(x0) -> r1(x0,skf27(x0)) % 0.17/0.44 % 107:2:1:INP:Top: ren14(x0),p8(skf27(x0)) -> % 0.17/0.44 % 108:2:1:INP:Top: ren14(x0),p108(skf27(x0)) -> % 0.17/0.44 % 109:2:1:INP:Top: ren14(x0) -> p107(skf27(x0)) % 0.17/0.44 % 110:2:1:INP:Top: ren14(x0) -> r1(x0,skf28(x0)) % 0.17/0.44 % 111:2:1:INP:Top: ren14(x0) -> p8(skf28(x0)) % 0.17/0.44 % 112:2:1:INP:Top: ren14(x0),p108(skf28(x0)) -> % 0.17/0.44 % 113:2:1:INP:Top: ren14(x0) -> p107(skf28(x0)) % 0.17/0.44 % 114:2:1:INP:Top: ren15(x0) -> r1(x0,skf29(x0)) % 0.17/0.44 % 115:2:1:INP:Top: ren15(x0),p7(skf29(x0)) -> % 0.17/0.44 % 116:2:1:INP:Top: ren15(x0),p107(skf29(x0)) -> % 0.17/0.44 % 117:2:1:INP:Top: ren15(x0) -> p106(skf29(x0)) % 0.17/0.44 % 118:2:1:INP:Top: ren15(x0) -> r1(x0,skf30(x0)) % 0.17/0.44 % 119:2:1:INP:Top: ren15(x0) -> p7(skf30(x0)) % 0.17/0.44 % 120:2:1:INP:Top: ren15(x0),p107(skf30(x0)) -> % 0.17/0.44 % 121:2:1:INP:Top: ren15(x0) -> p106(skf30(x0)) % 0.17/0.44 % 122:2:1:INP:Top: ren16(x0) -> r1(x0,skf31(x0)) % 0.17/0.44 % 123:2:1:INP:Top: ren16(x0),p6(skf31(x0)) -> % 0.17/0.44 % 124:2:1:INP:Top: ren16(x0),p106(skf31(x0)) -> % 0.17/0.44 % 125:2:1:INP:Top: ren16(x0) -> p105(skf31(x0)) % 0.17/0.44 % 126:2:1:INP:Top: ren16(x0) -> r1(x0,skf32(x0)) % 0.17/0.44 % 127:2:1:INP:Top: ren16(x0) -> p6(skf32(x0)) % 0.17/0.44 % 128:2:1:INP:Top: ren16(x0),p106(skf32(x0)) -> % 0.17/0.44 % 129:2:1:INP:Top: ren16(x0) -> p105(skf32(x0)) % 0.17/0.44 % 130:2:1:INP:Top: ren17(x0) -> r1(x0,skf33(x0)) % 0.17/0.44 % 131:2:1:INP:Top: ren17(x0),p5(skf33(x0)) -> % 0.17/0.44 % 132:2:1:INP:Top: ren17(x0),p105(skf33(x0)) -> % 0.17/0.44 % 133:2:1:INP:Top: ren17(x0) -> p104(skf33(x0)) % 0.17/0.44 % 134:2:1:INP:Top: ren17(x0) -> r1(x0,skf34(x0)) % 0.17/0.44 % 135:2:1:INP:Top: ren17(x0) -> p5(skf34(x0)) % 0.17/0.44 % 136:2:1:INP:Top: ren17(x0),p105(skf34(x0)) -> % 0.17/0.44 % 137:2:1:INP:Top: ren17(x0) -> p104(skf34(x0)) % 0.17/0.44 % 138:2:1:INP:Top: ren18(x0) -> r1(x0,skf35(x0)) % 0.17/0.44 % 139:2:1:INP:Top: ren18(x0),p4(skf35(x0)) -> % 0.17/0.44 % 140:2:1:INP:Top: ren18(x0),p104(skf35(x0)) -> % 0.17/0.44 % 141:2:1:INP:Top: ren18(x0) -> p103(skf35(x0)) % 0.17/0.44 % 142:2:1:INP:Top: ren18(x0) -> r1(x0,skf36(x0)) % 0.17/0.44 % 143:2:1:INP:Top: ren18(x0) -> p4(skf36(x0)) % 0.17/0.44 % 144:2:1:INP:Top: ren18(x0),p104(skf36(x0)) -> % 0.17/0.44 % 145:2:1:INP:Top: ren18(x0) -> p103(skf36(x0)) % 0.17/0.44 % 146:2:1:INP:Top: ren19(x0) -> r1(x0,skf37(x0)) % 0.17/0.44 % 147:2:1:INP:Top: ren19(x0),p3(skf37(x0)) -> % 0.17/0.44 % 148:2:1:INP:Top: ren19(x0),p103(skf37(x0)) -> % 0.17/0.44 % 149:2:1:INP:Top: ren19(x0) -> p102(skf37(x0)) % 0.17/0.44 % 150:2:1:INP:Top: ren19(x0) -> r1(x0,skf38(x0)) % 0.17/0.44 % 151:2:1:INP:Top: ren19(x0) -> p3(skf38(x0)) % 0.17/0.44 % 152:2:1:INP:Top: ren19(x0),p103(skf38(x0)) -> % 0.17/0.44 % 153:2:1:INP:Top: ren19(x0) -> p102(skf38(x0)) % 0.17/0.44 % 154:2:1:INP:Top: ren20(x0) -> r1(x0,skf39(x0)) % 0.17/0.44 % 155:2:1:INP:Top: ren20(x0),p2(skf39(x0)) -> % 0.17/0.44 % 156:2:1:INP:Top: ren20(x0),p102(skf39(x0)) -> % 0.17/0.44 % 157:2:1:INP:Top: ren20(x0) -> p101(skf39(x0)) % 0.17/0.44 % 158:2:1:INP:Top: ren20(x0) -> r1(x0,skf40(x0)) % 0.17/0.44 % 159:2:1:INP:Top: ren20(x0) -> p2(skf40(x0)) % 0.17/0.44 % 160:2:1:INP:Top: ren20(x0),p102(skf40(x0)) -> % 0.17/0.44 % 161:2:1:INP:Top: ren20(x0) -> p101(skf40(x0)) % 0.17/0.44 % 162:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p21(x1),p120(x1) -> p21(x0) % 0.17/0.44 % 163:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p120(x1),p21(x0) -> p21(x1) % 0.17/0.44 % 164:5:2:INP:TopTop: ren22(x0),r1(x0,x1),p20(x1),p119(x1) -> p20(x0) % 0.17/0.44 % 165:5:2:INP:TopTop: ren22(x0),r1(x0,x1),p119(x1),p20(x0) -> p20(x1) % 0.17/0.44 % 166:5:2:INP:TopTop: ren23(x0),r1(x0,x1),p19(x1),p118(x1) -> p19(x0) % 0.17/0.44 % 167:5:2:INP:TopTop: ren23(x0),r1(x0,x1),p118(x1),p19(x0) -> p19(x1) % 0.17/0.44 % 168:5:2:INP:TopTop: ren24(x0),r1(x0,x1),p18(x1),p117(x1) -> p18(x0) % 0.17/0.44 % 169:5:2:INP:TopTop: ren24(x0),r1(x0,x1),p117(x1),p18(x0) -> p18(x1) % 0.17/0.44 % 170:5:2:INP:TopTop: ren25(x0),r1(x0,x1),p17(x1),p116(x1) -> p17(x0) % 0.17/0.44 % 171:5:2:INP:TopTop: ren25(x0),r1(x0,x1),p116(x1),p17(x0) -> p17(x1) % 0.17/0.44 % 172:5:2:INP:TopTop: ren26(x0),r1(x0,x1),p16(x1),p115(x1) -> p16(x0) % 0.17/0.44 % 173:5:2:INP:TopTop: ren26(x0),r1(x0,x1),p115(x1),p16(x0) -> p16(x1) % 0.17/0.44 % 174:5:2:INP:TopTop: ren27(x0),r1(x0,x1),p15(x1),p114(x1) -> p15(x0) % 0.17/0.44 % 175:5:2:INP:TopTop: ren27(x0),r1(x0,x1),p114(x1),p15(x0) -> p15(x1) % 0.17/0.44 % 176:5:2:INP:TopTop: ren28(x0),r1(x0,x1),p14(x1),p113(x1) -> p14(x0) % 0.17/0.44 % 177:5:2:INP:TopTop: ren28(x0),r1(x0,x1),p113(x1),p14(x0) -> p14(x1) % 0.17/0.44 % 178:5:2:INP:TopTop: ren29(x0),r1(x0,x1),p13(x1),p112(x1) -> p13(x0) % 0.17/0.44 % 179:5:2:INP:TopTop: ren29(x0),r1(x0,x1),p112(x1),p13(x0) -> p13(x1) % 0.17/0.44 % 180:5:2:INP:TopTop: ren30(x0),r1(x0,x1),p12(x1),p111(x1) -> p12(x0) % 0.17/0.44 % 181:5:2:INP:TopTop: ren30(x0),r1(x0,x1),p111(x1),p12(x0) -> p12(x1) % 0.17/0.44 % 182:5:2:INP:TopTop: ren31(x0),r1(x0,x1),p11(x1),p110(x1) -> p11(x0) % 0.17/0.44 % 183:5:2:INP:TopTop: ren31(x0),r1(x0,x1),p110(x1),p11(x0) -> p11(x1) % 0.17/0.44 % 184:5:2:INP:TopTop: ren32(x0),r1(x0,x1),p10(x1),p109(x1) -> p10(x0) % 0.17/0.44 % 185:5:2:INP:TopTop: ren32(x0),r1(x0,x1),p109(x1),p10(x0) -> p10(x1) % 0.17/0.44 % 186:5:2:INP:TopTop: ren33(x0),r1(x0,x1),p9(x1),p108(x1) -> p9(x0) % 0.17/0.44 % 187:5:2:INP:TopTop: ren33(x0),r1(x0,x1),p108(x1),p9(x0) -> p9(x1) % 0.17/0.44 % 188:5:2:INP:TopTop: ren34(x0),r1(x0,x1),p8(x1),p107(x1) -> p8(x0) % 0.17/0.44 % 189:5:2:INP:TopTop: ren34(x0),r1(x0,x1),p107(x1),p8(x0) -> p8(x1) % 0.17/0.44 % 190:5:2:INP:TopTop: ren35(x0),r1(x0,x1),p7(x1),p106(x1) -> p7(x0) % 0.17/0.44 % 191:5:2:INP:TopTop: ren35(x0),r1(x0,x1),p106(x1),p7(x0) -> p7(x1) % 0.17/0.44 % 192:5:2:INP:TopTop: ren36(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0) % 0.17/0.44 % 193:5:2:INP:TopTop: ren36(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1) % 0.17/0.44 % 194:5:2:INP:TopTop: ren37(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0) % 0.17/0.44 % 195:5:2:INP:TopTop: ren37(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1) % 0.17/0.44 % 196:5:2:INP:TopTop: ren38(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0) % 0.17/0.44 % 197:5:2:INP:TopTop: ren38(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1) % 0.17/0.44 % 198:5:2:INP:TopTop: ren39(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0) % 0.17/0.44 % 199:5:2:INP:TopTop: ren39(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1) % 0.17/0.44 % 200:5:2:INP:TopTop: ren40(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0) % 0.17/0.44 % 201:5:2:INP:TopTop: ren40(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1) % 0.17/0.44 % 202:5:2:INP:TopTop: ren41(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0) % 0.17/0.44 % 203:5:2:INP:TopTop: ren41(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1) % 0.17/0.44 % 204:4:1:INP:Top: ren42(x0),p119(x0) -> ren1(x0),p120(x0) % 0.17/0.44 % 205:4:1:INP:Top: ren42(x0),p118(x0) -> ren2(x0),p119(x0) % 0.17/0.44 % 206:4:1:INP:Top: ren42(x0),p117(x0) -> ren3(x0),p118(x0) % 0.17/0.44 % 207:4:1:INP:Top: ren42(x0),p116(x0) -> ren4(x0),p117(x0) % 0.17/0.44 % 208:4:1:INP:Top: ren42(x0),p115(x0) -> ren5(x0),p116(x0) % 0.17/0.44 % 209:4:1:INP:Top: ren42(x0),p114(x0) -> ren6(x0),p115(x0) % 0.17/0.44 % 210:4:1:INP:Top: ren42(x0),p113(x0) -> ren7(x0),p114(x0) % 0.17/0.44 % 211:4:1:INP:Top: ren42(x0),p112(x0) -> ren8(x0),p113(x0) % 0.17/0.44 % 212:4:1:INP:Top: ren42(x0),p111(x0) -> ren9(x0),p112(x0) % 0.17/0.44 % 213:4:1:INP:Top: ren42(x0),p110(x0) -> ren10(x0),p111(x0) % 0.17/0.44 % 214:4:1:INP:Top: ren42(x0),p109(x0) -> ren11(x0),p110(x0) % 0.17/0.44 % 215:4:1:INP:Top: ren42(x0),p108(x0) -> ren12(x0),p109(x0) % 0.17/0.44 % 216:4:1:INP:Top: ren42(x0),p107(x0) -> ren13(x0),p108(x0) % 0.17/0.44 % 217:4:1:INP:Top: ren42(x0),p106(x0) -> ren14(x0),p107(x0) % 0.17/0.44 % 218:4:1:INP:Top: ren42(x0),p105(x0) -> ren15(x0),p106(x0) % 0.17/0.44 % 219:4:1:INP:Top: ren42(x0),p104(x0) -> ren16(x0),p105(x0) % 0.17/0.44 % 220:4:1:INP:Top: ren42(x0),p103(x0) -> ren17(x0),p104(x0) % 0.17/0.44 % 221:4:1:INP:Top: ren42(x0),p102(x0) -> ren18(x0),p103(x0) % 0.17/0.44 % 222:4:1:INP:Top: ren42(x0),p101(x0) -> ren19(x0),p102(x0) % 0.17/0.44 % 223:4:1:INP:Top: ren42(x0),p100(x0) -> ren20(x0),p101(x0) % 0.17/0.44 % 224:3:1:INP:Top: ren42(x0),p120(x0) -> ren21(x0) % 0.17/0.44 % 225:3:1:INP:Top: ren42(x0),p119(x0) -> ren22(x0) % 0.17/0.44 % 226:3:1:INP:Top: ren42(x0),p118(x0) -> ren23(x0) % 0.17/0.44 % 227:3:1:INP:Top: ren42(x0),p117(x0) -> ren24(x0) % 0.17/0.44 % 228:3:1:INP:Top: ren42(x0),p116(x0) -> ren25(x0) % 0.17/0.44 % 229:3:1:INP:Top: ren42(x0),p115(x0) -> ren26(x0) % 0.17/0.44 % 230:3:1:INP:Top: ren42(x0),p114(x0) -> ren27(x0) % 0.17/0.44 % 231:3:1:INP:Top: ren42(x0),p113(x0) -> ren28(x0) % 0.17/0.44 % 232:3:1:INP:Top: ren42(x0),p112(x0) -> ren29(x0) % 0.17/0.44 % 233:3:1:INP:Top: ren42(x0),p111(x0) -> ren30(x0) % 0.17/0.44 % 234:3:1:INP:Top: ren42(x0),p110(x0) -> ren31(x0) % 0.17/0.44 % 235:3:1:INP:Top: ren42(x0),p109(x0) -> ren32(x0) % 0.17/0.44 % 236:3:1:INP:Top: ren42(x0),p108(x0) -> ren33(x0) % 0.17/0.45 % 237:3:1:INP:Top: ren42(x0),p107(x0) -> ren34(x0) % 0.17/0.45 % 238:3:1:INP:Top: ren42(x0),p106(x0) -> ren35(x0) % 0.17/0.45 % 239:3:1:INP:Top: ren42(x0),p105(x0) -> ren36(x0) % 0.17/0.45 % 240:3:1:INP:Top: ren42(x0),p104(x0) -> ren37(x0) % 0.17/0.45 % 241:3:1:INP:Top: ren42(x0),p103(x0) -> ren38(x0) % 0.17/0.45 % 242:3:1:INP:Top: ren42(x0),p102(x0) -> ren39(x0) % 0.17/0.45 % 243:3:1:INP:Top: ren42(x0),p101(x0) -> ren40(x0) % 0.17/0.45 % 244:3:1:INP:Top: ren42(x0),p100(x0) -> ren41(x0) % 0.17/0.45 % 245:3:1:INP:Top: ren42(x0),p121(x0) -> p120(x0) % 0.17/0.45 % 246:3:1:INP:Top: ren42(x0),p120(x0) -> p119(x0) % 0.17/0.45 % 247:3:1:INP:Top: ren42(x0),p119(x0) -> p118(x0) % 0.17/0.45 % 248:3:1:INP:Top: ren42(x0),p118(x0) -> p117(x0) % 0.17/0.45 % 249:3:1:INP:Top: ren42(x0),p117(x0) -> p116(x0) % 0.17/0.45 % 250:3:1:INP:Top: ren42(x0),p116(x0) -> p115(x0) % 0.17/0.45 % 251:3:1:INP:Top: ren42(x0),p115(x0) -> p114(x0) % 0.17/0.45 % 252:3:1:INP:Top: ren42(x0),p114(x0) -> p113(x0) % 0.17/0.45 % 253:3:1:INP:Top: ren42(x0),p113(x0) -> p112(x0) % 0.17/0.45 % 254:3:1:INP:Top: ren42(x0),p112(x0) -> p111(x0) % 0.17/0.45 % 255:3:1:INP:Top: ren42(x0),p111(x0) -> p110(x0) % 0.17/0.45 % 256:3:1:INP:Top: ren42(x0),p110(x0) -> p109(x0) % 0.17/0.45 % 257:3:1:INP:Top: ren42(x0),p109(x0) -> p108(x0) % 0.17/0.45 % 258:3:1:INP:Top: ren42(x0),p108(x0) -> p107(x0) % 0.17/0.45 % 259:3:1:INP:Top: ren42(x0),p107(x0) -> p106(x0) % 0.17/0.45 % 260:3:1:INP:Top: ren42(x0),p106(x0) -> p105(x0) % 0.17/0.45 % 261:3:1:INP:Top: ren42(x0),p105(x0) -> p104(x0) % 0.17/0.45 % 262:3:1:INP:Top: ren42(x0),p104(x0) -> p103(x0) % 0.17/0.45 % 263:3:1:INP:Top: ren42(x0),p103(x0) -> p102(x0) % 0.17/0.45 % 264:3:1:INP:Top: ren42(x0),p102(x0) -> p101(x0) % 0.17/0.45 % 265:3:1:INP:Top: ren42(x0),p101(x0) -> p100(x0) % 0.17/0.45 % 266:21:20:INP:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: r1(skc41,x0),r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),r1(x5,x6),r1(x6,x7),r1(x7,x8),r1(x8,x9),r1(x9,x10),r1(x10,x11),r1(x11,x12),r1(x12,x13),r1(x13,x14),r1(x14,x15),r1(x15,x16),r1(x16,x17),r1(x17,x18),r1(x18,x19) -> ren42(x19) % 0.17/0.45 % 267:1:0:INP:: p101(skc41) -> % 0.17/0.45 % 268:1:0:INP:: -> p100(skc41) % 0.17/0.45 % 0.17/0.45 % Predicates: r1 p21 p121 p120 p119 p20 p118 p19 p117 p18 p116 p17 p115 p16 p114 p15 p113 p14 p112 p13 p111 p12 p110 p11 p109 p10 p108 p9 p107 p8 p106 p7 p105 p6 p104 p5 p103 p4 p102 p3 p101 p2 p100 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 % 0.17/0.45 % Fol Constants: skc41 % 0.17/0.45 % 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 % 0.17/0.45 % Problem Properties: % 0.17/0.45 % This is a full first-order problem without equality. The Problem is non-linear. % 0.17/0.45 % 0.17/0.45 % 0.17/0.45 % Reduced Input Axiom Clauses: % 0.17/0.45 % 1:1:1:INP:Top: -> r1(x0,x0) % 0.17/0.45 % 2:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0)) % 0.17/0.45 % 3:2:1:INP:Top: ren1(x0),p21(skf1(x0)) -> % 0.17/0.45 % 4:2:1:INP:Top: ren1(x0),p121(skf1(x0)) -> % 0.17/0.45 % 5:2:1:INP:Top: ren1(x0) -> p120(skf1(x0)) % 0.17/0.45 % 6:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0)) % 0.17/0.45 % 7:2:1:INP:Top: ren1(x0) -> p21(skf2(x0)) % 0.17/0.45 % 8:2:1:INP:Top: ren1(x0),p121(skf2(x0)) -> % 0.17/0.45 % 9:2:1:INP:Top: ren1(x0) -> p120(skf2(x0)) % 0.17/0.45 % 10:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0)) % 0.17/0.45 % 11:2:1:INP:Top: ren2(x0),p20(skf3(x0)) -> % 0.17/0.45 % 12:2:1:INP:Top: ren2(x0),p120(skf3(x0)) -> % 0.17/0.45 % 13:2:1:INP:Top: ren2(x0) -> p119(skf3(x0)) % 0.17/0.45 % 14:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0)) % 0.17/0.45 % 15:2:1:INP:Top: ren2(x0) -> p20(skf4(x0)) % 0.17/0.45 % 16:2:1:INP:Top: ren2(x0),p120(skf4(x0)) -> % 0.17/0.45 % 17:2:1:INP:Top: ren2(x0) -> p119(skf4(x0)) % 0.17/0.45 % 18:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0)) % 0.17/0.45 % 19:2:1:INP:Top: ren3(x0),p19(skf5(x0)) -> % 0.17/0.45 % 20:2:1:INP:Top: ren3(x0),p119(skf5(x0)) -> % 0.17/0.45 % 21:2:1:INP:Top: ren3(x0) -> p118(skf5(x0)) % 0.17/0.45 % 22:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0)) % 0.17/0.45 % 23:2:1:INP:Top: ren3(x0) -> p19(skf6(x0)) % 0.17/0.45 % 24:2:1:INP:Top: ren3(x0),p119(skf6(x0)) -> % 0.17/0.45 % 25:2:1:INP:Top: ren3(x0) -> p118(skf6(x0)) % 0.17/0.45 % 26:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0)) % 0.17/0.45 % 27:2:1:INP:Top: ren4(x0),p18(skf7(x0)) -> % 0.17/0.45 % 28:2:1:INP:Top: ren4(x0),p118(skf7(x0)) -> % 0.17/0.45 % 29:2:1:INP:Top: ren4(x0) -> p117(skf7(x0)) % 0.17/0.45 % 30:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0)) % 0.17/0.45 % 31:2:1:INP:Top: ren4(x0) -> p18(skf8(x0)) % 0.17/0.45 % 32:2:1:INP:Top: ren4(x0),p118(skf8(x0)) -> % 0.17/0.45 % 33:2:1:INP:Top: ren4(x0) -> p117(skf8(x0)) % 0.17/0.45 % 34:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0)) % 0.17/0.45 % 35:2:1:INP:Top: ren5(x0),p17(skf9(x0)) -> % 0.17/0.45 % 36:2:1:INP:Top: ren5(x0),p117(skf9(x0)) -> % 0.17/0.45 % 37:2:1:INP:Top: ren5(x0) -> p116(skf9(x0)) % 0.17/0.45 % 38:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0)) % 0.17/0.45 % 39:2:1:INP:Top: ren5(x0) -> p17(skf10(x0)) % 0.17/0.45 % 40:2:1:INP:Top: ren5(x0),p117(skf10(x0)) -> % 0.17/0.45 % 41:2:1:INP:Top: ren5(x0) -> p116(skf10(x0)) % 0.17/0.45 % 42:2:1:INP:Top: ren6(x0) -> r1(x0,skf11(x0)) % 0.17/0.45 % 43:2:1:INP:Top: ren6(x0),p16(skf11(x0)) -> % 0.17/0.45 % 44:2:1:INP:Top: ren6(x0),p116(skf11(x0)) -> % 0.17/0.45 % 45:2:1:INP:Top: ren6(x0) -> p115(skf11(x0)) % 0.17/0.45 % 46:2:1:INP:Top: ren6(x0) -> r1(x0,skf12(x0)) % 0.17/0.45 % 47:2:1:INP:Top: ren6(x0) -> p16(skf12(x0)) % 0.17/0.45 % 48:2:1:INP:Top: ren6(x0),p116(skf12(x0)) -> % 0.17/0.45 % 49:2:1:INP:Top: ren6(x0) -> p115(skf12(x0)) % 0.17/0.45 % 50:2:1:INP:Top: ren7(x0) -> r1(x0,skf13(x0)) % 0.17/0.45 % 51:2:1:INP:Top: ren7(x0),p15(skf13(x0)) -> % 0.17/0.45 % 52:2:1:INP:Top: ren7(x0),p115(skf13(x0)) -> % 0.17/0.45 % 53:2:1:INP:Top: ren7(x0) -> p114(skf13(x0)) % 0.17/0.45 % 54:2:1:INP:Top: ren7(x0) -> r1(x0,skf14(x0)) % 0.17/0.45 % 55:2:1:INP:Top: ren7(x0) -> p15(skf14(x0)) % 0.17/0.45 % 56:2:1:INP:Top: ren7(x0),p115(skf14(x0)) -> % 0.17/0.45 % 57:2:1:INP:Top: ren7(x0) -> p114(skf14(x0)) % 0.17/0.45 % 58:2:1:INP:Top: ren8(x0) -> r1(x0,skf15(x0)) % 0.17/0.45 % 59:2:1:INP:Top: ren8(x0),p14(skf15(x0)) -> % 0.17/0.45 % 60:2:1:INP:Top: ren8(x0),p114(skf15(x0)) -> % 0.17/0.45 % 61:2:1:INP:Top: ren8(x0) -> p113(skf15(x0)) % 0.17/0.45 % 62:2:1:INP:Top: ren8(x0) -> r1(x0,skf16(x0)) % 0.17/0.45 % 63:2:1:INP:Top: ren8(x0) -> p14(skf16(x0)) % 0.17/0.45 % 64:2:1:INP:Top: ren8(x0),p114(skf16(x0)) -> % 0.17/0.45 % 65:2:1:INP:Top: ren8(x0) -> p113(skf16(x0)) % 0.17/0.45 % 66:2:1:INP:Top: ren9(x0) -> r1(x0,skf17(x0)) % 0.17/0.45 % 67:2:1:INP:Top: ren9(x0),p13(skf17(x0)) -> % 0.17/0.45 % 68:2:1:INP:Top: ren9(x0),p113(skf17(x0)) -> % 0.17/0.45 % 69:2:1:INP:Top: ren9(x0) -> p112(skf17(x0)) % 0.17/0.45 % 70:2:1:INP:Top: ren9(x0) -> r1(x0,skf18(x0)) % 0.17/0.45 % 71:2:1:INP:Top: ren9(x0) -> p13(skf18(x0)) % 0.17/0.45 % 72:2:1:INP:Top: ren9(x0),p113(skf18(x0)) -> % 0.17/0.45 % 73:2:1:INP:Top: ren9(x0) -> p112(skf18(x0)) % 0.17/0.45 % 74:2:1:INP:Top: ren10(x0) -> r1(x0,skf19(x0)) % 0.17/0.45 % 75:2:1:INP:Top: ren10(x0),p12(skf19(x0)) -> % 0.17/0.45 % 76:2:1:INP:Top: ren10(x0),p112(skf19(x0)) -> % 0.17/0.45 % 77:2:1:INP:Top: ren10(x0) -> p111(skf19(x0)) % 0.17/0.45 % 78:2:1:INP:Top: ren10(x0) -> r1(x0,skf20(x0)) % 0.17/0.45 % 79:2:1:INP:Top: ren10(x0) -> p12(skf20(x0)) % 0.17/0.45 % 80:2:1:INP:Top: ren10(x0),p112(skf20(x0)) -> % 0.17/0.45 % 81:2:1:INP:Top: ren10(x0) -> p111(skf20(x0)) % 0.17/0.45 % 82:2:1:INP:Top: ren11(x0) -> r1(x0,skf21(x0)) % 0.17/0.45 % 83:2:1:INP:Top: ren11(x0),p11(skf21(x0)) -> % 0.17/0.45 % 84:2:1:INP:Top: ren11(x0),p111(skf21(x0)) -> % 0.17/0.45 % 85:2:1:INP:Top: ren11(x0) -> p110(skf21(x0)) % 0.17/0.45 % 86:2:1:INP:Top: ren11(x0) -> r1(x0,skf22(x0)) % 0.17/0.45 % 87:2:1:INP:Top: ren11(x0) -> p11(skf22(x0)) % 0.17/0.45 % 88:2:1:INP:Top: ren11(x0),p111(skf22(x0)) -> % 0.17/0.45 % 89:2:1:INP:Top: ren11(x0) -> p110(skf22(x0)) % 0.17/0.45 % 90:2:1:INP:Top: ren12(x0) -> r1(x0,skf23(x0)) % 0.17/0.45 % 91:2:1:INP:Top: ren12(x0),p10(skf23(x0)) -> % 0.17/0.45 % 92:2:1:INP:Top: ren12(x0),p110(skf23(x0)) -> % 0.17/0.45 % 93:2:1:INP:Top: ren12(x0) -> p109(skf23(x0)) % 0.17/0.45 % 94:2:1:INP:Top: ren12(x0) -> r1(x0,skf24(x0)) % 0.17/0.45 % 95:2:1:INP:Top: ren12(x0) -> p10(skf24(x0)) % 0.17/0.45 % 96:2:1:INP:Top: ren12(x0),p110(skf24(x0)) -> % 0.17/0.45 % 97:2:1:INP:Top: ren12(x0) -> p109(skf24(x0)) % 0.17/0.45 % 98:2:1:INP:Top: ren13(x0) -> r1(x0,skf25(x0)) % 0.17/0.45 % 99:2:1:INP:Top: ren13(x0),p9(skf25(x0)) -> % 0.17/0.45 % 100:2:1:INP:Top: ren13(x0),p109(skf25(x0)) -> % 0.17/0.45 % 101:2:1:INP:Top: ren13(x0) -> p108(skf25(x0)) % 0.17/0.45 % 102:2:1:INP:Top: ren13(x0) -> r1(x0,skf26(x0)) % 0.17/0.45 % 103:2:1:INP:Top: ren13(x0) -> p9(skf26(x0)) % 0.17/0.45 % 104:2:1:INP:Top: ren13(x0),p109(skf26(x0)) -> % 0.17/0.45 % 105:2:1:INP:Top: ren13(x0) -> p108(skf26(x0)) % 0.17/0.45 % 106:2:1:INP:Top: ren14(x0) -> r1(x0,skf27(x0)) % 0.17/0.45 % 107:2:1:INP:Top: ren14(x0),p8(skf27(x0)) -> % 0.17/0.45 % 108:2:1:INP:Top: ren14(x0),p108(skf27(x0)) -> % 0.17/0.45 % 109:2:1:INP:Top: ren14(x0) -> p107(skf27(x0)) % 0.17/0.45 % 110:2:1:INP:Top: ren14(x0) -> r1(x0,skf28(x0)) % 0.17/0.45 % 111:2:1:INP:Top: ren14(x0) -> p8(skf28(x0)) % 0.17/0.45 % 112:2:1:INP:Top: ren14(x0),p108(skf28(x0)) -> % 0.17/0.45 % 113:2:1:INP:Top: ren14(x0) -> p107(skf28(x0)) % 0.17/0.45 % 114:2:1:INP:Top: ren15(x0) -> r1(x0,skf29(x0)) % 0.17/0.45 % 115:2:1:INP:Top: ren15(x0),p7(skf29(x0)) -> % 0.17/0.45 % 116:2:1:INP:Top: ren15(x0),p107(skf29(x0)) -> % 0.17/0.45 % 117:2:1:INP:Top: ren15(x0) -> p106(skf29(x0)) % 0.17/0.45 % 118:2:1:INP:Top: ren15(x0) -> r1(x0,skf30(x0)) % 0.17/0.45 % 119:2:1:INP:Top: ren15(x0) -> p7(skf30(x0)) % 0.17/0.45 % 120:2:1:INP:Top: ren15(x0),p107(skf30(x0)) -> % 0.17/0.45 % 121:2:1:INP:Top: ren15(x0) -> p106(skf30(x0)) % 0.17/0.45 % 122:2:1:INP:Top: ren16(x0) -> r1(x0,skf31(x0)) % 0.17/0.45 % 123:2:1:INP:Top: ren16(x0),p6(skf31(x0)) -> % 0.17/0.45 % 124:2:1:INP:Top: ren16(x0),p106(skf31(x0)) -> % 0.17/0.45 % 125:2:1:INP:Top: ren16(x0) -> p105(skf31(x0)) % 0.17/0.45 % 126:2:1:INP:Top: ren16(x0) -> r1(x0,skf32(x0)) % 0.17/0.45 % 127:2:1:INP:Top: ren16(x0) -> p6(skf32(x0)) % 0.17/0.45 % 128:2:1:INP:Top: ren16(x0),p106(skf32(x0)) -> % 0.17/0.45 % 129:2:1:INP:Top: ren16(x0) -> p105(skf32(x0)) % 0.17/0.45 % 130:2:1:INP:Top: ren17(x0) -> r1(x0,skf33(x0)) % 0.17/0.45 % 131:2:1:INP:Top: ren17(x0),p5(skf33(x0)) -> % 0.17/0.45 % 132:2:1:INP:Top: ren17(x0),p105(skf33(x0)) -> % 0.17/0.45 % 133:2:1:INP:Top: ren17(x0) -> p104(skf33(x0)) % 0.17/0.45 % 134:2:1:INP:Top: ren17(x0) -> r1(x0,skf34(x0)) % 0.17/0.45 % 135:2:1:INP:Top: ren17(x0) -> p5(skf34(x0)) % 0.17/0.45 % 136:2:1:INP:Top: ren17(x0),p105(skf34(x0)) -> % 0.17/0.45 % 137:2:1:INP:Top: ren17(x0) -> p104(skf34(x0)) % 0.17/0.45 % 138:2:1:INP:Top: ren18(x0) -> r1(x0,skf35(x0)) % 0.17/0.45 % 139:2:1:INP:Top: ren18(x0),p4(skf35(x0)) -> % 0.17/0.45 % 140:2:1:INP:Top: ren18(x0),p104(skf35(x0)) -> % 0.17/0.45 % 141:2:1:INP:Top: ren18(x0) -> p103(skf35(x0)) % 0.17/0.45 % 142:2:1:INP:Top: ren18(x0) -> r1(x0,skf36(x0)) % 0.17/0.45 % 143:2:1:INP:Top: ren18(x0) -> p4(skf36(x0)) % 0.17/0.45 % 144:2:1:INP:Top: ren18(x0),p104(skf36(x0)) -> % 0.17/0.45 % 145:2:1:INP:Top: ren18(x0) -> p103(skf36(x0)) % 0.17/0.45 % 146:2:1:INP:Top: ren19(x0) -> r1(x0,skf37(x0)) % 0.17/0.45 % 147:2:1:INP:Top: ren19(x0),p3(skf37(x0)) -> % 0.17/0.45 % 148:2:1:INP:Top: ren19(x0),p103(skf37(x0)) -> % 0.17/0.45 % 149:2:1:INP:Top: ren19(x0) -> p102(skf37(x0)) % 0.17/0.45 % 150:2:1:INP:Top: ren19(x0) -> r1(x0,skf38(x0)) % 0.17/0.45 % 151:2:1:INP:Top: ren19(x0) -> p3(skf38(x0)) % 0.17/0.45 % 152:2:1:INP:Top: ren19(x0),p103(skf38(x0)) -> % 0.17/0.45 % 153:2:1:INP:Top: ren19(x0) -> p102(skf38(x0)) % 0.17/0.45 % 154:2:1:INP:Top: ren20(x0) -> r1(x0,skf39(x0)) % 0.17/0.45 % 155:2:1:INP:Top: ren20(x0),p2(skf39(x0)) -> % 0.17/0.45 % 156:2:1:INP:Top: ren20(x0),p102(skf39(x0)) -> % 0.17/0.45 % 157:2:1:INP:Top: ren20(x0) -> p101(skf39(x0)) % 0.17/0.45 % 158:2:1:INP:Top: ren20(x0) -> r1(x0,skf40(x0)) % 0.17/0.45 % 159:2:1:INP:Top: ren20(x0) -> p2(skf40(x0)) % 0.17/0.45 % 160:2:1:INP:Top: ren20(x0),p102(skf40(x0)) -> % 0.17/0.45 % 161:2:1:INP:Top: ren20(x0) -> p101(skf40(x0)) % 0.17/0.46 % 162:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p21(x1),p120(x1) -> p21(x0) % 0.17/0.46 % 163:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p120(x1),p21(x0) -> p21(x1) % 0.17/0.46 % 164:5:2:INP:TopTop: ren22(x0),r1(x0,x1),p20(x1),p119(x1) -> p20(x0) % 0.17/0.46 % 165:5:2:INP:TopTop: ren22(x0),r1(x0,x1),p119(x1),p20(x0) -> p20(x1) % 0.17/0.46 % 166:5:2:INP:TopTop: ren23(x0),r1(x0,x1),p19(x1),p118(x1) -> p19(x0) % 0.17/0.46 % 167:5:2:INP:TopTop: ren23(x0),r1(x0,x1),p118(x1),p19(x0) -> p19(x1) % 0.17/0.46 % 168:5:2:INP:TopTop: ren24(x0),r1(x0,x1),p18(x1),p117(x1) -> p18(x0) % 0.17/0.46 % 169:5:2:INP:TopTop: ren24(x0),r1(x0,x1),p117(x1),p18(x0) -> p18(x1) % 0.17/0.46 % 170:5:2:INP:TopTop: ren25(x0),r1(x0,x1),p17(x1),p116(x1) -> p17(x0) % 0.17/0.46 % 171:5:2:INP:TopTop: ren25(x0),r1(x0,x1),p116(x1),p17(x0) -> p17(x1) % 0.17/0.46 % 172:5:2:INP:TopTop: ren26(x0),r1(x0,x1),p16(x1),p115(x1) -> p16(x0) % 0.17/0.46 % 173:5:2:INP:TopTop: ren26(x0),r1(x0,x1),p115(x1),p16(x0) -> p16(x1) % 0.17/0.46 % 174:5:2:INP:TopTop: ren27(x0),r1(x0,x1),p15(x1),p114(x1) -> p15(x0) % 0.17/0.46 % 175:5:2:INP:TopTop: ren27(x0),r1(x0,x1),p114(x1),p15(x0) -> p15(x1) % 0.17/0.46 % 176:5:2:INP:TopTop: ren28(x0),r1(x0,x1),p14(x1),p113(x1) -> p14(x0) % 0.17/0.46 % 177:5:2:INP:TopTop: ren28(x0),r1(x0,x1),p113(x1),p14(x0) -> p14(x1) % 0.17/0.46 % 178:5:2:INP:TopTop: ren29(x0),r1(x0,x1),p13(x1),p112(x1) -> p13(x0) % 0.17/0.46 % 179:5:2:INP:TopTop: ren29(x0),r1(x0,x1),p112(x1),p13(x0) -> p13(x1) % 0.17/0.46 % 180:5:2:INP:TopTop: ren30(x0),r1(x0,x1),p12(x1),p111(x1) -> p12(x0) % 0.17/0.46 % 181:5:2:INP:TopTop: ren30(x0),r1(x0,x1),p111(x1),p12(x0) -> p12(x1) % 0.17/0.46 % 182:5:2:INP:TopTop: ren31(x0),r1(x0,x1),p11(x1),p110(x1) -> p11(x0) % 0.17/0.46 % 183:5:2:INP:TopTop: ren31(x0),r1(x0,x1),p110(x1),p11(x0) -> p11(x1) % 0.17/0.46 % 184:5:2:INP:TopTop: ren32(x0),r1(x0,x1),p10(x1),p109(x1) -> p10(x0) % 0.17/0.46 % 185:5:2:INP:TopTop: ren32(x0),r1(x0,x1),p109(x1),p10(x0) -> p10(x1) % 0.17/0.46 % 186:5:2:INP:TopTop: ren33(x0),r1(x0,x1),p9(x1),p108(x1) -> p9(x0) % 0.17/0.46 % 187:5:2:INP:TopTop: ren33(x0),r1(x0,x1),p108(x1),p9(x0) -> p9(x1) % 0.17/0.46 % 188:5:2:INP:TopTop: ren34(x0),r1(x0,x1),p8(x1),p107(x1) -> p8(x0) % 0.17/0.46 % 189:5:2:INP:TopTop: ren34(x0),r1(x0,x1),p107(x1),p8(x0) -> p8(x1) % 0.17/0.46 % 190:5:2:INP:TopTop: ren35(x0),r1(x0,x1),p7(x1),p106(x1) -> p7(x0) % 0.17/0.46 % 191:5:2:INP:TopTop: ren35(x0),r1(x0,x1),p106(x1),p7(x0) -> p7(x1) % 0.17/0.46 % 192:5:2:INP:TopTop: ren36(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0) % 0.17/0.46 % 193:5:2:INP:TopTop: ren36(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1) % 0.17/0.46 % 194:5:2:INP:TopTop: ren37(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0) % 0.17/0.46 % 195:5:2:INP:TopTop: ren37(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1) % 0.17/0.46 % 196:5:2:INP:TopTop: ren38(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0) % 0.17/0.46 % 197:5:2:INP:TopTop: ren38(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1) % 0.17/0.46 % 198:5:2:INP:TopTop: ren39(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0) % 0.17/0.46 % 199:5:2:INP:TopTop: ren39(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1) % 0.17/0.46 % 200:5:2:INP:TopTop: ren40(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0) % 0.17/0.46 % 201:5:2:INP:TopTop: ren40(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1) % 0.17/0.46 % 202:5:2:INP:TopTop: ren41(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0) % 0.17/0.46 % 203:5:2:INP:TopTop: ren41(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1) % 0.17/0.46 % 204:4:1:INP:Top: ren42(x0),p119(x0) -> ren1(x0),p120(x0) % 0.17/0.46 % 205:4:1:INP:Top: ren42(x0),p118(x0) -> ren2(x0),p119(x0) % 0.17/0.46 % 206:4:1:INP:Top: ren42(x0),p117(x0) -> ren3(x0),p118(x0) % 0.17/0.46 % 207:4:1:INP:Top: ren42(x0),p116(x0) -> ren4(x0),p117(x0) % 0.17/0.46 % 208:4:1:INP:Top: ren42(x0),p115(x0) -> ren5(x0),p116(x0) % 0.17/0.46 % 209:4:1:INP:Top: ren42(x0),p114(x0) -> ren6(x0),p115(x0) % 0.17/0.46 % 210:4:1:INP:Top: ren42(x0),p113(x0) -> ren7(x0),p114(x0) % 0.17/0.46 % 211:4:1:INP:Top: ren42(x0),p112(x0) -> ren8(x0),p113(x0) % 0.17/0.46 % 212:4:1:INP:Top: ren42(x0),p111(x0) -> ren9(x0),p112(x0) % 0.17/0.46 % 213:4:1:INP:Top: ren42(x0),p110(x0) -> ren10(x0),p111(x0) % 0.17/0.46 % 214:4:1:INP:Top: ren42(x0),p109(x0) -> ren11(x0),p110(x0) % 0.17/0.46 % 215:4:1:INP:Top: ren42(x0),p108(x0) -> ren12(x0),p109(x0) % 0.17/0.46 % 216:4:1:INP:Top: ren42(x0),p107(x0) -> ren13(x0),p108(x0) % 0.17/0.46 % 217:4:1:INP:Top: ren42(x0),p106(x0) -> ren14(x0),p107(x0) % 0.17/0.46 % 218:4:1:INP:Top: ren42(x0),p105(x0) -> ren15(x0),p106(x0) % 0.17/0.46 % 219:4:1:INP:Top: ren42(x0),p104(x0) -> ren16(x0),p105(x0) % 0.17/0.46 % 220:4:1:INP:Top: ren42(x0),p103(x0) -> ren17(x0),p104(x0) % 0.17/0.46 % 221:4:1:INP:Top: ren42(x0),p102(x0) -> ren18(x0),p103(x0) % 0.17/0.46 % 222:4:1:INP:Top: ren42(x0),p101(x0) -> ren19(x0),p102(x0) % 0.17/0.46 % 223:4:1:INP:Top: ren42(x0),p100(x0) -> ren20(x0),p101(x0) % 0.17/0.46 % 224:3:1:INP:Top: ren42(x0),p120(x0) -> ren21(x0) % 0.17/0.46 % 225:3:1:INP:Top: ren42(x0),p119(x0) -> ren22(x0) % 0.17/0.46 % 226:3:1:INP:Top: ren42(x0),p118(x0) -> ren23(x0) % 0.17/0.46 % 227:3:1:INP:Top: ren42(x0),p117(x0) -> ren24(x0) % 0.17/0.46 % 228:3:1:INP:Top: ren42(x0),p116(x0) -> ren25(x0) % 0.17/0.46 % 229:3:1:INP:Top: ren42(x0),p115(x0) -> ren26(x0) % 0.17/0.46 % 230:3:1:INP:Top: ren42(x0),p114(x0) -> ren27(x0) % 0.17/0.46 % 231:3:1:INP:Top: ren42(x0),p113(x0) -> ren28(x0) % 0.17/0.46 % 232:3:1:INP:Top: ren42(x0),p112(x0) -> ren29(x0) % 0.17/0.46 % 233:3:1:INP:Top: ren42(x0),p111(x0) -> ren30(x0) % 0.17/0.46 % 234:3:1:INP:Top: ren42(x0),p110(x0) -> ren31(x0) % 0.17/0.46 % 235:3:1:INP:Top: ren42(x0),p109(x0) -> ren32(x0) % 0.17/0.46 % 236:3:1:INP:Top: ren42(x0),p108(x0) -> ren33(x0) % 0.17/0.46 % 237:3:1:INP:Top: ren42(x0),p107(x0) -> ren34(x0) % 0.17/0.46 % 238:3:1:INP:Top: ren42(x0),p106(x0) -> ren35(x0) % 0.17/0.46 % 239:3:1:INP:Top: ren42(x0),p105(x0) -> ren36(x0) % 0.17/0.46 % 240:3:1:INP:Top: ren42(x0),p104(x0) -> ren37(x0) % 0.17/0.46 % 241:3:1:INP:Top: ren42(x0),p103(x0) -> ren38(x0) % 0.17/0.46 % 242:3:1:INP:Top: ren42(x0),p102(x0) -> ren39(x0) % 0.17/0.46 % 243:3:1:INP:Top: ren42(x0),p101(x0) -> ren40(x0) % 0.17/0.46 % 244:3:1:INP:Top: ren42(x0),p100(x0) -> ren41(x0) % 0.17/0.46 % 245:3:1:INP:Top: ren42(x0),p121(x0) -> p120(x0) % 0.17/0.46 % 246:3:1:INP:Top: ren42(x0),p120(x0) -> p119(x0) % 0.17/0.46 % 247:3:1:INP:Top: ren42(x0),p119(x0) -> p118(x0) % 0.17/0.46 % 248:3:1:INP:Top: ren42(x0),p118(x0) -> p117(x0) % 0.17/0.46 % 249:3:1:INP:Top: ren42(x0),p117(x0) -> p116(x0) % 0.17/0.46 % 250:3:1:INP:Top: ren42(x0),p116(x0) -> p115(x0) % 0.17/0.46 % 251:3:1:INP:Top: ren42(x0),p115(x0) -> p114(x0) % 0.17/0.46 % 252:3:1:INP:Top: ren42(x0),p114(x0) -> p113(x0) % 0.17/0.46 % 253:3:1:INP:Top: ren42(x0),p113(x0) -> p112(x0) % 0.17/0.46 % 254:3:1:INP:Top: ren42(x0),p112(x0) -> p111(x0) % 0.17/0.46 % 255:3:1:INP:Top: ren42(x0),p111(x0) -> p110(x0) % 0.17/0.46 % 256:3:1:INP:Top: ren42(x0),p110(x0) -> p109(x0) % 0.17/0.46 % 257:3:1:INP:Top: ren42(x0),p109(x0) -> p108(x0) % 0.17/0.46 % 258:3:1:INP:Top: ren42(x0),p108(x0) -> p107(x0) % 0.17/0.46 % 259:3:1:INP:Top: ren42(x0),p107(x0) -> p106(x0) % 0.17/0.46 % 260:3:1:INP:Top: ren42(x0),p106(x0) -> p105(x0) % 0.17/0.46 % 261:3:1:INP:Top: ren42(x0),p105(x0) -> p104(x0) % 0.17/0.46 % 262:3:1:INP:Top: ren42(x0),p104(x0) -> p103(x0) % 0.17/0.46 % 263:3:1:INP:Top: ren42(x0),p103(x0) -> p102(x0) % 0.17/0.46 % 264:3:1:INP:Top: ren42(x0),p102(x0) -> p101(x0) % 299.79/300.03 % 265:3:1:INP:Top: ren42(x0),p101(x0) -> p100(x0) % 299.79/300.03 % 299.79/300.03 % Reduced Input Conjecture Clauses: % 299.79/300.03 % 266:21:20:INP:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: r1(skc41,x0),r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),r1(x5,x6),r1(x6,x7),r1(x7,x8),r1(x8,x9),r1(x9,x10),r1(x10,x11),r1(x11,x12),r1(x12,x13),r1(x13,x14),r1(x14,x15),r1(x15,x16),r1(x16,x17),r1(x17,x18),r1(x18,x19) -> ren42(x19) % 299.79/300.03 % 267:1:0:INP:: p101(skc41) -> % 299.79/300.03 % 268:1:0:INP:: -> p100(skc41) % 299.79/300.03 % 299.79/300.03 % 299.79/300.03 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 761 atoms initially. Used heuristic: lmodel_grow === % 299.79/300.03 % 299.79/300.03 % 299.79/300.03 % 299.79/300.03 % SZS status Timeout % 299.79/300.03 % 299.79/300.03 % SPASS-SCL-FOL 0.1.1 % 299.79/300.03 % SPASS beiseite: Ran out of time or SPASS was killed. % 299.79/300.03 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.79/300.03 % 299.79/300.03 % SPASS-SCL-FOL Statistics: % 299.79/300.03 % Number of learned clauses: 37 % 299.79/300.03 % Number of propagations: 365 % 299.79/300.03 % Number of decisions: 1747 % 299.79/300.03 % Number of resolutions: 94 % 299.79/300.03 % Number of condensations: 0 % 299.79/300.03 % Number of sub resolutions: 1 % 299.79/300.03 % 299.79/300.03 % SCL allocated 123500 KBytes. % 299.79/300.03 % SCL spent 0:4:59.60 on the problem. %------------------------------------------------------------------------------