%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO674-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 19:55:28 EDT 2022 % Result : Unsatisfiable 0.37s 0.57s % Output : Refutation 0.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO674-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jul 9 05:23:16 EDT 2022 % 0.13/0.34 % CPUTime : % 0.37/0.57 % 0.37/0.57 SPASS V 3.9 % 0.37/0.57 SPASS beiseite: Proof found. % 0.37/0.57 % SZS status Theorem % 0.37/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.37/0.57 SPASS derived 115 clauses, backtracked 0 clauses, performed 0 splits and kept 92 clauses. % 0.37/0.57 SPASS allocated 63390 KBytes. % 0.37/0.57 SPASS spent 0:00:00.23 on the problem. % 0.37/0.57 0:00:00.04 for the input. % 0.37/0.57 0:00:00.00 for the FLOTTER CNF translation. % 0.37/0.57 0:00:00.01 for inferences. % 0.37/0.57 0:00:00.00 for the backtracking. % 0.37/0.57 0:00:00.15 for the reduction. % 0.37/0.57 % 0.37/0.57 % 0.37/0.57 Here is a proof with depth 11, length 96 : % 0.37/0.57 % SZS output start Refutation % 0.37/0.57 1[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(y)) E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(suc(y)))*+ E(s(0),f(suc(u)))* E(s(0),f(suc(x)))* E(s(0),f(suc(z)))* E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> . % 0.37/0.57 2[0:Inp] || LE(f(u),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(u)). % 0.37/0.57 3[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u))*. % 0.37/0.57 4[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.37/0.57 5[0:Inp] || LE(f(u),s(s(s(0))))* -> E(s(s(0)),f(u)) LE(f(u),s(s(0))). % 0.37/0.57 6[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ -> iLEQ(suc(u),suc(u))*. % 0.37/0.57 7[0:Inp] || -> LE(f(u),s(s(s(0))))*. % 0.37/0.57 8[0:Inp] || LE(f(z__dfg),0)* -> . % 0.37/0.57 9[0:Inp] || LE(f(suc(u)),s(s(s(0))))* -> E(s(s(0)),f(suc(u))) LE(f(u),s(s(0))). % 0.37/0.57 10[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(z)) E(s(s(0)),f(x)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v)))*+ E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(z)))* E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> . % 0.37/0.57 11[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.37/0.57 12[0:Inp] || LE(f(suc(u)),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(u))). % 0.37/0.57 13[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u)))*+ -> iLEQ(suc(u),suc(u))*. % 0.37/0.57 14[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(z)) E(0,f(suc(y)))+ E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(x))) E(0,f(suc(z))) E(0,f(suc(u))) iLEQ(suc(u),suc(y))* iLEQ(suc(z),suc(w))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* iLEQ(suc(x),suc(z))* -> . % 0.37/0.57 15[0:MRR:5.0,7.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.37/0.57 16[0:MRR:9.0,7.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u)))*. % 0.37/0.57 18[0:Res:16.1,6.1] || E(s(s(0)),f(u))* -> LE(f(u),s(s(0))) iLEQ(suc(u),suc(u))*. % 0.37/0.57 19[0:MRR:18.0,15.1] || -> LE(f(u),s(s(0)))* iLEQ(suc(u),suc(u))*. % 0.37/0.57 26[0:Res:16.1,10.11] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(z)) E(s(s(0)),f(x)) E(s(s(0)),f(w)) E(s(s(0)),f(v))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(z)))* E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(v),s(s(0))). % 0.37/0.57 27[0:MRR:26.9,15.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(z)) E(s(s(0)),f(x)) E(s(s(0)),f(w)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(w)))*+ E(s(s(0)),f(suc(z)))* E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(v),s(s(0)))*. % 0.37/0.57 29[0:Res:16.1,27.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(z)) E(s(s(0)),f(x)) E(s(s(0)),f(w))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(z)))* E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(w),s(s(0))) LE(f(v),s(s(0)))*. % 0.37/0.57 30[0:MRR:29.8,15.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(z)) E(s(s(0)),f(x)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(z)))*+ E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 32[0:Res:16.1,30.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(z))* E(s(s(0)),f(x)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(z),s(s(0))) LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 33[0:MRR:32.6,15.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y)) E(s(s(0)),f(x)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(y)))*+ E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 35[0:Res:16.1,33.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(y))* E(s(s(0)),f(x)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(x)))* -> LE(f(y),s(s(0))) LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 36[0:MRR:35.5,15.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(x)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ E(s(s(0)),f(suc(x)))* -> LE(f(y),s(s(0)))* LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 38[0:Res:16.1,36.7] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(x)) E(s(s(0)),f(u))* E(s(s(0)),f(suc(x)))* -> LE(f(u),s(s(0))) LE(f(y),s(s(0)))* LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 39[0:MRR:38.6,15.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(x)) E(s(s(0)),f(suc(x)))*+ -> LE(f(u),s(s(0)))* LE(f(y),s(s(0)))* LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 44[0:Res:16.1,39.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* E(s(s(0)),f(x))* -> LE(f(x),s(s(0))) LE(f(u),s(s(0)))* LE(f(y),s(s(0)))* LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 45[0:MRR:44.5,15.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(z))* iLEQ(suc(z),suc(y))* -> LE(f(x),s(s(0)))* LE(f(u),s(s(0)))* LE(f(y),s(s(0)))* LE(f(z),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))*. % 0.37/0.57 47[0:Res:19.1,45.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(y),suc(w))* -> LE(f(x),s(s(0)))* LE(f(v),s(s(0)))* LE(f(x),s(s(0)))* LE(f(w),s(s(0)))* LE(f(y),s(s(0)))* LE(f(u),s(s(0)))* LE(f(x),s(s(0)))*. % 0.37/0.57 52[0:Obv:47.6] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(y),suc(w))* -> LE(f(v),s(s(0)))* LE(f(w),s(s(0)))* LE(f(y),s(s(0)))* LE(f(u),s(s(0)))* LE(f(x),s(s(0)))*. % 0.37/0.57 59[0:Res:19.1,52.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* -> LE(f(v),s(s(0)))* LE(f(v),s(s(0)))* LE(f(u),s(s(0)))* LE(f(x),s(s(0)))* LE(f(v),s(s(0)))* LE(f(w),s(s(0)))*. % 0.37/0.57 64[0:Obv:59.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* -> LE(f(u),s(s(0)))* LE(f(x),s(s(0)))* LE(f(v),s(s(0)))* LE(f(w),s(s(0)))*. % 0.37/0.57 71[0:Res:19.1,64.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(w),s(s(0)))* LE(f(w),s(s(0)))* LE(f(v),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.37/0.57 76[0:Obv:71.3] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(v),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.37/0.57 86[0:Res:19.1,76.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(v),s(s(0)))* LE(f(u),s(s(0)))*. % 0.37/0.57 91[0:Obv:86.2] || iLEQ(suc(u),suc(v))*+ -> LE(f(v),s(s(0)))* LE(f(u),s(s(0)))*. % 0.37/0.57 98[0:Res:19.1,91.0] || -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(u),s(s(0)))*. % 0.37/0.57 103[0:Obv:98.1] || -> LE(f(u),s(s(0)))*. % 0.37/0.57 104[0:MRR:2.0,103.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.37/0.57 105[0:MRR:12.0,103.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.37/0.57 113[0:Res:105.1,13.1] || E(s(0),f(u)) -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.37/0.57 114[0:Res:105.1,1.11] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(y)) E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(suc(u)))* E(s(0),f(suc(x)))* E(s(0),f(suc(z)))* E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(y),s(0)). % 0.37/0.57 115[0:MRR:113.0,104.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.37/0.57 116[0:MRR:114.6,104.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(suc(u)))*+ E(s(0),f(suc(x)))* E(s(0),f(suc(z)))* E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(y),s(0)). % 0.37/0.57 120[0:Res:105.1,116.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(suc(x)))* E(s(0),f(suc(z)))* E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.57 121[0:MRR:120.6,104.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(suc(x)))*+ E(s(0),f(suc(z)))* E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.57 126[0:Res:105.1,121.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(suc(z)))* E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.57 127[0:MRR:126.8,104.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(z)))*+ E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 129[0:Res:105.1,127.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(z)) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(v)))* E(s(0),f(suc(w)))* -> LE(f(z),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 130[0:MRR:129.5,104.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(v)))*+ E(s(0),f(suc(w)))* -> LE(f(z),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 132[0:Res:105.1,130.7] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(w)))* -> LE(f(v),s(0)) LE(f(z),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 133[0:MRR:132.6,104.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) E(s(0),f(suc(w)))*+ -> LE(f(v),s(0)) LE(f(z),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 135[0:Res:105.1,133.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) -> LE(f(w),s(0)) LE(f(v),s(0)) LE(f(z),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 136[0:MRR:135.5,104.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(x))* iLEQ(suc(y),suc(u))* -> LE(f(w),s(0)) LE(f(v),s(0)) LE(f(z),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)). % 0.37/0.58 140[0:Res:115.1,136.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(u),s(0)) LE(f(v),s(0)) LE(f(u),s(0)) LE(f(y),s(0)) LE(f(w),s(0)) LE(f(u),s(0)) LE(f(x),s(0)). % 0.37/0.58 143[0:Obv:140.6] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(v),s(0)) LE(f(y),s(0)) LE(f(w),s(0)) LE(f(u),s(0)) LE(f(x),s(0)). % 0.37/0.58 146[0:Res:115.1,143.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* iLEQ(suc(v),suc(x))* -> LE(f(x),s(0)) LE(f(x),s(0)) LE(f(w),s(0)) LE(f(u),s(0)) LE(f(x),s(0)) LE(f(v),s(0)). % 0.37/0.58 149[0:Obv:146.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(v),suc(x))* -> LE(f(w),s(0)) LE(f(u),s(0)) LE(f(x),s(0)) LE(f(v),s(0)). % 0.37/0.58 152[0:Res:115.1,149.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(v),s(0)) LE(f(u),s(0)) LE(f(v),s(0)) LE(f(w),s(0)) LE(f(v),s(0)). % 0.37/0.58 155[0:Obv:152.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(u),s(0)) LE(f(w),s(0)) LE(f(v),s(0)). % 0.37/0.58 158[0:Res:115.1,155.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(u),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 0.37/0.58 161[0:Obv:158.2] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 0.37/0.58 167[0:Res:115.1,161.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 0.37/0.58 170[0:Obv:167.1] || -> LE(f(u),s(0))*. % 0.37/0.58 171[0:MRR:4.0,170.0] || -> E(0,f(u))* LE(f(u),0). % 0.37/0.58 172[0:MRR:11.0,170.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.37/0.58 176[0:Res:172.0,14.6] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(z)) E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(x))) E(0,f(suc(z))) E(0,f(suc(u))) iLEQ(suc(u),suc(y))* iLEQ(suc(z),suc(w))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* iLEQ(suc(x),suc(z))* -> LE(f(y),0). % 0.37/0.58 177[0:MRR:176.4,171.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w)))+ E(0,f(suc(v))) E(0,f(suc(x))) E(0,f(suc(y))) E(0,f(suc(u))) iLEQ(suc(u),suc(z))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* iLEQ(suc(x),suc(y))* -> LE(f(z),0). % 0.37/0.58 179[0:Res:172.0,177.5] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(v))) E(0,f(suc(x))) E(0,f(suc(y))) E(0,f(suc(u))) iLEQ(suc(u),suc(z))* iLEQ(suc(y),suc(w))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* iLEQ(suc(x),suc(y))* -> LE(f(w),0) LE(f(z),0). % 0.37/0.58 180[0:MRR:179.2,171.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(suc(v)))+ E(0,f(suc(w))) E(0,f(suc(x))) E(0,f(suc(u))) iLEQ(suc(u),suc(y))* iLEQ(suc(x),suc(z))* iLEQ(suc(v),suc(u))* iLEQ(suc(z),suc(v))* iLEQ(suc(w),suc(x))* -> LE(f(z),0) LE(f(y),0). % 0.37/0.58 182[0:Res:172.0,180.4] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(suc(w))) E(0,f(suc(x))) E(0,f(suc(u))) iLEQ(suc(u),suc(y))* iLEQ(suc(x),suc(z))* iLEQ(suc(v),suc(u))* iLEQ(suc(z),suc(v))* iLEQ(suc(w),suc(x))* -> LE(f(v),0) LE(f(z),0) LE(f(y),0). % 0.37/0.58 183[0:MRR:182.1,171.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v)))+ E(0,f(suc(w))) E(0,f(suc(u))) iLEQ(suc(u),suc(x))* iLEQ(suc(w),suc(y))* iLEQ(suc(z),suc(u))* iLEQ(suc(y),suc(z))* iLEQ(suc(v),suc(w))* -> LE(f(z),0) LE(f(y),0) LE(f(x),0). % 0.37/0.58 185[0:Res:172.0,183.3] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(w))) E(0,f(suc(u))) iLEQ(suc(u),suc(x))* iLEQ(suc(w),suc(y))* iLEQ(suc(z),suc(u))* iLEQ(suc(y),suc(z))* iLEQ(suc(v),suc(w))* -> LE(f(v),0) LE(f(z),0) LE(f(y),0) LE(f(x),0). % 0.37/0.58 186[0:MRR:185.1,171.0] || E(0,f(u)) E(0,f(v)) E(0,f(suc(v)))+ E(0,f(suc(u))) iLEQ(suc(u),suc(w))* iLEQ(suc(v),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(v))* -> LE(f(z),0) LE(f(y),0) LE(f(x),0) LE(f(w),0). % 0.37/0.58 188[0:Res:172.0,186.2] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) iLEQ(suc(u),suc(w))* iLEQ(suc(v),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(v))* -> LE(f(v),0) LE(f(z),0) LE(f(y),0) LE(f(x),0) LE(f(w),0). % 0.37/0.58 189[0:MRR:188.1,171.0] || E(0,f(u)) E(0,f(suc(u)))+ iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(w))* -> LE(f(w),0) LE(f(z),0) LE(f(y),0) LE(f(x),0) LE(f(v),0). % 0.37/0.58 191[0:Res:172.0,189.1] || E(0,f(u)) iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(w))* -> LE(f(u),0) LE(f(w),0) LE(f(z),0) LE(f(y),0) LE(f(x),0) LE(f(v),0). % 0.37/0.58 192[0:MRR:191.0,171.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(x),suc(y))* iLEQ(suc(z),suc(w))* -> LE(f(u),0) LE(f(w),0) LE(f(z),0) LE(f(y),0) LE(f(x),0) LE(f(v),0). % 0.37/0.58 196[0:Res:3.2,192.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(v))* -> LE(f(u),0) LE(f(v),0) LE(f(y),0) LE(f(x),0) LE(f(w),0) LE(f(u),0). % 0.37/0.58 197[0:Obv:196.6] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(v))* -> LE(f(v),0) LE(f(y),0) LE(f(x),0) LE(f(w),0) LE(f(u),0). % 0.37/0.58 198[0:MRR:197.0,197.1,171.0,172.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* -> LE(f(u),0) LE(f(y),0) LE(f(w),0) LE(f(v),0) LE(f(x),0). % 0.37/0.58 199[0:Res:3.2,198.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(u))* -> LE(f(u),0) LE(f(x),0) LE(f(v),0) LE(f(u),0) LE(f(w),0). % 0.37/0.58 200[0:Obv:199.5] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(u))* -> LE(f(x),0) LE(f(v),0) LE(f(u),0) LE(f(w),0). % 0.37/0.58 201[0:MRR:200.0,200.1,171.0,172.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(w))* -> LE(f(x),0) LE(f(u),0) LE(f(w),0) LE(f(v),0). % 0.37/0.58 202[0:Res:3.2,201.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> LE(f(w),0) LE(f(u),0) LE(f(v),0) LE(f(u),0). % 0.37/0.58 203[0:Obv:202.5] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> LE(f(w),0) LE(f(v),0) LE(f(u),0). % 0.37/0.58 204[0:MRR:203.0,203.1,171.0,172.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(w),0) LE(f(u),0) LE(f(v),0). % 0.37/0.58 205[0:Res:3.2,204.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* -> LE(f(v),0) LE(f(u),0) LE(f(u),0). % 0.37/0.58 206[0:Obv:205.4] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* -> LE(f(v),0) LE(f(u),0). % 0.37/0.58 207[0:MRR:206.0,206.1,171.0,172.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 0.37/0.58 211[0:Res:3.2,207.0] || E(0,f(u)) E(0,f(suc(u)))* -> LE(f(u),0) LE(f(u),0). % 0.37/0.58 212[0:Obv:211.2] || E(0,f(u)) E(0,f(suc(u)))* -> LE(f(u),0). % 0.37/0.58 213[0:MRR:212.0,212.1,171.0,172.0] || -> LE(f(u),0)*. % 0.37/0.58 214[0:UnC:213.0,8.0] || -> . % 0.37/0.58 % SZS output end Refutation % 0.37/0.58 Formulae used in the proof : clause_193 clause_298 clause_281 clause_176 clause_139 clause_126 clause_498 clause_204 clause_129 clause_431 clause_50 clause_84 clause_493 clause_453 % 0.37/0.58 %------------------------------------------------------------------------------