%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO683-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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:31 EDT 2022 % Result : Unsatisfiable 0.19s 0.52s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO683-1 : TPTP v8.1.0. Released v7.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n015.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jul 9 11:14:52 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.52 % 0.19/0.52 SPASS V 3.9 % 0.19/0.52 SPASS beiseite: Proof found. % 0.19/0.52 % SZS status Theorem % 0.19/0.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 SPASS derived 151 clauses, backtracked 0 clauses, performed 0 splits and kept 112 clauses. % 0.19/0.52 SPASS allocated 63395 KBytes. % 0.19/0.52 SPASS spent 0:00:00.18 on the problem. % 0.19/0.52 0:00:00.04 for the input. % 0.19/0.52 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.52 0:00:00.01 for inferences. % 0.19/0.52 0:00:00.00 for the backtracking. % 0.19/0.52 0:00:00.11 for the reduction. % 0.19/0.52 % 0.19/0.52 % 0.19/0.52 Here is a proof with depth 9, length 109 : % 0.19/0.52 % SZS output start Refutation % 0.19/0.52 1[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u))*. % 0.19/0.52 2[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u)))*+ -> iLEQ(suc(u),suc(u))*. % 0.19/0.52 3[0:Inp] || -> LE(f(u),s(s(s(s(0)))))*. % 0.19/0.52 4[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ -> iLEQ(suc(u),suc(u))*. % 0.19/0.52 5[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(y)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(u)))*+ E(s(s(s(0))),f(suc(y)))* E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(x)))* E(s(s(s(0))),f(suc(v)))* -> . % 0.19/0.52 6[0:Inp] || LE(f(suc(u)),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u))). % 0.19/0.52 7[0:Inp] || LE(f(u),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(u)). % 0.19/0.52 8[0:Inp] || LE(f(suc(u)),s(s(s(s(0)))))* -> E(s(s(s(0))),f(suc(u))) LE(f(u),s(s(s(0)))). % 0.19/0.52 9[0:Inp] || LE(f(z__dfg),0)* -> . % 0.19/0.52 10[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.19/0.52 11[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(y)) E(s(s(0)),f(x)) E(s(s(0)),f(v)) E(s(s(0)),f(w)) E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(x)))* -> . % 0.19/0.52 12[0:Inp] || LE(f(u),s(s(s(s(0)))))* -> E(s(s(s(0))),f(u)) LE(f(u),s(s(s(0)))). % 0.19/0.52 13[0:Inp] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u)))*+ -> iLEQ(suc(u),suc(u))*. % 0.19/0.52 14[0:Inp] || LE(f(suc(u)),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(u))). % 0.19/0.52 15[0:Inp] || LE(f(u),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(u)). % 0.19/0.52 16[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(suc(u)))+ E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(y))) E(0,f(suc(x))) iLEQ(suc(w),suc(v))* iLEQ(suc(u),suc(x))* iLEQ(suc(x),suc(y))* iLEQ(suc(y),suc(w))* -> . % 0.19/0.52 17[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.19/0.52 18[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(y)) E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(x)) E(s(0),f(suc(v)))*+ E(s(0),f(suc(y)))* E(s(0),f(suc(u)))* E(s(0),f(suc(x)))* E(s(0),f(suc(w)))* -> . % 0.19/0.52 19[0:MRR:12.0,3.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.19/0.52 20[0:MRR:8.0,3.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(u)))*. % 0.19/0.52 22[0:Res:20.1,13.1] || E(s(s(s(0))),f(u))* -> LE(f(u),s(s(s(0)))) iLEQ(suc(u),suc(u))*. % 0.19/0.52 23[0:MRR:22.0,19.1] || -> LE(f(u),s(s(s(0))))* iLEQ(suc(u),suc(u))*. % 0.19/0.52 38[0:Res:20.1,5.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(u))* E(s(s(s(0))),f(y)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(y)))* E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(x)))* E(s(s(s(0))),f(suc(v)))* -> LE(f(u),s(s(s(0)))). % 0.19/0.52 39[0:MRR:38.4,19.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(y)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(y)))*+ E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(x)))* E(s(s(s(0))),f(suc(v)))* -> LE(f(u),s(s(s(0))))*. % 0.19/0.52 41[0:Res:20.1,39.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(y))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(x)))* E(s(s(s(0))),f(suc(v)))* -> LE(f(y),s(s(s(0)))) LE(f(u),s(s(s(0))))*. % 0.19/0.52 42[0:MRR:41.4,19.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(w)))*+ E(s(s(s(0))),f(suc(x)))* E(s(s(s(0))),f(suc(v)))* -> LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 44[0:Res:20.1,42.7] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(w))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(x)))* E(s(s(s(0))),f(suc(v)))* -> LE(f(w),s(s(s(0)))) LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 45[0:MRR:44.4,19.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x)) E(s(s(s(0))),f(suc(x)))*+ E(s(s(s(0))),f(suc(v)))* -> LE(f(w),s(s(s(0))))* LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 50[0:Res:20.1,45.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(x))* E(s(s(s(0))),f(suc(v)))* -> LE(f(x),s(s(s(0)))) LE(f(w),s(s(s(0))))* LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 51[0:MRR:50.5,19.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v)))*+ -> LE(f(x),s(s(s(0))))* LE(f(w),s(s(s(0))))* LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 53[0:Res:20.1,51.5] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* E(s(s(s(0))),f(v))* -> LE(f(v),s(s(s(0)))) LE(f(x),s(s(s(0))))* LE(f(w),s(s(s(0))))* LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 54[0:MRR:53.4,19.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(y))* iLEQ(suc(y),suc(w))* -> LE(f(v),s(s(s(0))))* LE(f(x),s(s(s(0))))* LE(f(w),s(s(s(0))))* LE(f(y),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 56[0:Res:23.1,54.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* -> LE(f(w),s(s(s(0))))* LE(f(w),s(s(s(0))))* LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(x),s(s(s(0))))* LE(f(w),s(s(s(0))))*. % 0.19/0.52 62[0:Obv:56.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* -> LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(x),s(s(s(0))))* LE(f(w),s(s(s(0))))*. % 0.19/0.52 70[0:Res:23.1,62.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(w),s(s(s(0))))* LE(f(w),s(s(s(0))))* LE(f(w),s(s(s(0))))* LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 76[0:Obv:70.3] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(w),s(s(s(0))))* LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 87[0:Res:23.1,76.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(s(s(0))))* LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 93[0:Obv:87.3] || iLEQ(suc(u),suc(v))*+ -> LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 101[0:Res:23.1,93.0] || -> LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.19/0.52 107[0:Obv:101.1] || -> LE(f(u),s(s(s(0))))*. % 0.19/0.52 108[0:MRR:7.0,107.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.19/0.52 109[0:MRR:6.0,107.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u)))*. % 0.19/0.52 118[0:Res:109.1,11.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(y)) E(s(s(0)),f(x)) E(s(s(0)),f(v)) 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(y)))* E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(x)))* -> LE(f(u),s(s(0))). % 0.19/0.52 119[0:Res:109.1,4.1] || E(s(s(0)),f(u))* -> LE(f(u),s(s(0))) iLEQ(suc(u),suc(u))*. % 0.19/0.52 120[0:MRR:119.0,108.1] || -> LE(f(u),s(s(0)))* iLEQ(suc(u),suc(u))*. % 0.19/0.52 121[0:MRR:118.8,108.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(y)) E(s(s(0)),f(x)) E(s(s(0)),f(v)) E(s(s(0)),f(w)) E(s(s(0)),f(suc(w)))*+ E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(x)))* -> LE(f(u),s(s(0)))*. % 0.19/0.52 128[0:Res:109.1,121.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(y)) E(s(s(0)),f(x)) E(s(s(0)),f(v)) E(s(s(0)),f(w))* E(s(s(0)),f(suc(y)))* E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(x)))* -> LE(f(w),s(s(0))) LE(f(u),s(s(0)))*. % 0.19/0.52 129[0:MRR:128.7,108.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(y)) E(s(s(0)),f(x)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(y)))*+ E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(x)))* -> LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 131[0:Res:109.1,129.7] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(y))* E(s(s(0)),f(x)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(x)))* -> LE(f(y),s(s(0))) LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 132[0:MRR:131.4,108.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(x)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(v)))*+ E(s(s(0)),f(suc(x)))* -> LE(f(y),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 134[0:Res:109.1,132.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(x)) E(s(s(0)),f(v))* E(s(s(0)),f(suc(x)))* -> LE(f(v),s(s(0))) LE(f(y),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 135[0:MRR:134.5,108.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(x)) E(s(s(0)),f(suc(x)))*+ -> LE(f(v),s(s(0)))* LE(f(y),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 140[0:Res:109.1,135.5] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* E(s(s(0)),f(x))* -> LE(f(x),s(s(0))) LE(f(v),s(s(0)))* LE(f(y),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 141[0:MRR:140.4,108.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(w))* -> LE(f(x),s(s(0)))* LE(f(v),s(s(0)))* LE(f(y),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 143[0:Res:120.1,141.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(w),s(s(0)))* LE(f(v),s(s(0)))* LE(f(w),s(s(0)))* LE(f(x),s(s(0)))* LE(f(u),s(s(0)))* LE(f(w),s(s(0)))*. % 0.19/0.52 148[0:Obv:143.5] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(v),s(s(0)))* LE(f(x),s(s(0)))* LE(f(u),s(s(0)))* LE(f(w),s(s(0)))*. % 0.19/0.52 155[0:Res:120.1,148.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))* LE(f(v),s(s(0)))*. % 0.19/0.52 160[0:Obv:155.3] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(w),s(s(0)))* LE(f(u),s(s(0)))* LE(f(v),s(s(0)))*. % 0.19/0.52 167[0:Res:120.1,160.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(s(0)))* LE(f(u),s(s(0)))* LE(f(v),s(s(0)))* LE(f(v),s(s(0)))*. % 0.19/0.52 172[0:Obv:167.3] || iLEQ(suc(u),suc(v))*+ -> LE(f(u),s(s(0)))* LE(f(v),s(s(0)))*. % 0.19/0.52 182[0:Res:120.1,172.0] || -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(u),s(s(0)))*. % 0.19/0.52 187[0:Obv:182.1] || -> LE(f(u),s(s(0)))*. % 0.19/0.52 188[0:MRR:15.0,187.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.19/0.52 189[0:MRR:14.0,187.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.19/0.52 197[0:Res:189.1,2.1] || E(s(0),f(u)) -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.19/0.52 198[0:Res:189.1,18.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(y)) E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(w)) 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(w)))* -> LE(f(v),s(0)). % 0.19/0.52 199[0:MRR:197.0,188.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.19/0.52 200[0:MRR:198.5,188.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(y)) E(s(0),f(u)) E(s(0),f(w)) 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(w)))* -> LE(f(v),s(0)). % 0.19/0.52 204[0:Res:189.1,200.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(y)) E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(x)) E(s(0),f(suc(u)))* E(s(0),f(suc(x)))* E(s(0),f(suc(w)))* -> LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 205[0:MRR:204.4,188.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(x)) E(s(0),f(suc(u)))*+ E(s(0),f(suc(x)))* E(s(0),f(suc(w)))* -> LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 207[0:Res:189.1,205.7] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(u)) E(s(0),f(w)) E(s(0),f(x)) E(s(0),f(suc(x)))* E(s(0),f(suc(w)))* -> LE(f(u),s(0)) LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 208[0:MRR:207.4,188.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) E(s(0),f(x)) E(s(0),f(suc(x)))*+ E(s(0),f(suc(w)))* -> LE(f(u),s(0)) LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 213[0:Res:189.1,208.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) E(s(0),f(x)) E(s(0),f(suc(w)))* -> LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 214[0:MRR:213.5,188.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) E(s(0),f(suc(w)))*+ -> LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 216[0:Res:189.1,214.5] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* E(s(0),f(w)) -> LE(f(w),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 217[0:MRR:216.4,188.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* -> LE(f(w),s(0)) LE(f(x),s(0)) LE(f(u),s(0)) LE(f(y),s(0)) LE(f(v),s(0)). % 0.19/0.52 218[0:Res:199.1,217.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(u),s(0)) LE(f(v),s(0)) LE(f(w),s(0)) LE(f(u),s(0)) LE(f(x),s(0)) LE(f(u),s(0)). % 0.19/0.52 221[0:Obv:218.6] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(v),s(0)) LE(f(w),s(0)) LE(f(x),s(0)) LE(f(u),s(0)). % 0.19/0.52 224[0:Res:199.1,221.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* -> LE(f(u),s(0)) LE(f(u),s(0)) LE(f(v),s(0)) LE(f(w),s(0)) LE(f(u),s(0)). % 0.19/0.52 227[0:Obv:224.3] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(v),s(0)) LE(f(w),s(0)) LE(f(u),s(0)). % 0.19/0.52 233[0:Res:199.1,227.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(v),s(0)) LE(f(u),s(0)) LE(f(v),s(0)). % 0.19/0.52 236[0:Obv:233.2] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 0.19/0.52 239[0:Res:199.1,236.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 0.19/0.52 242[0:Obv:239.1] || -> LE(f(u),s(0))*. % 0.19/0.52 243[0:MRR:17.0,242.0] || -> E(0,f(u))* LE(f(u),0). % 0.19/0.52 244[0:MRR:10.0,242.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.19/0.52 248[0:Res:244.0,16.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(w))) E(0,f(suc(v))) E(0,f(suc(y))) E(0,f(suc(x))) iLEQ(suc(w),suc(v))* iLEQ(suc(u),suc(x))* iLEQ(suc(x),suc(y))* iLEQ(suc(y),suc(w))* -> LE(f(u),0). % 0.19/0.52 249[0:MRR:248.0,243.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(u))) E(0,f(suc(x))) E(0,f(suc(w))) iLEQ(suc(v),suc(u))* iLEQ(suc(y),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(v))* -> LE(f(y),0). % 0.19/0.52 251[0:Res:244.0,249.4] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(suc(u))) E(0,f(suc(x))) E(0,f(suc(w))) iLEQ(suc(v),suc(u))* iLEQ(suc(y),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(v))* -> LE(f(v),0) LE(f(y),0). % 0.19/0.52 252[0:MRR:251.1,243.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(u)))+ E(0,f(suc(w))) E(0,f(suc(v))) iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* -> LE(f(x),0) LE(f(y),0). % 0.19/0.52 254[0:Res:244.0,252.3] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(w))) E(0,f(suc(v))) iLEQ(suc(x),suc(u))* iLEQ(suc(y),suc(v))* iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* -> LE(f(u),0) LE(f(x),0) LE(f(y),0). % 0.19/0.52 255[0:MRR:254.0,243.0] || E(0,f(u)) E(0,f(v)) E(0,f(suc(v)))+ E(0,f(suc(u))) iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(x),0) LE(f(w),0) LE(f(y),0). % 0.19/0.52 257[0:Res:244.0,255.2] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) iLEQ(suc(w),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(v),0) LE(f(x),0) LE(f(w),0) LE(f(y),0). % 0.19/0.52 258[0:MRR:257.1,243.0] || E(0,f(u)) E(0,f(suc(u)))+ iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* iLEQ(suc(u),suc(y))* iLEQ(suc(y),suc(v))* -> LE(f(y),0) LE(f(w),0) LE(f(v),0) LE(f(x),0). % 0.19/0.52 260[0:Res:244.0,258.1] || E(0,f(u)) iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* iLEQ(suc(u),suc(y))* iLEQ(suc(y),suc(v))* -> LE(f(u),0) LE(f(y),0) LE(f(w),0) LE(f(v),0) LE(f(x),0). % 0.19/0.52 261[0:MRR:260.0,243.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(y))* iLEQ(suc(y),suc(u))* -> LE(f(x),0) LE(f(y),0) LE(f(v),0) LE(f(u),0) LE(f(w),0). % 0.19/0.52 265[0:Res:1.2,261.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* -> LE(f(w),0) LE(f(x),0) LE(f(u),0) LE(f(u),0) LE(f(v),0). % 0.19/0.52 266[0:Obv:265.7] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* iLEQ(suc(x),suc(u))* -> LE(f(w),0) LE(f(x),0) LE(f(u),0) LE(f(v),0). % 0.19/0.52 267[0:MRR:266.0,266.1,243.0,244.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(w),suc(x))* -> LE(f(v),0) LE(f(w),0) LE(f(x),0) LE(f(u),0). % 0.19/0.53 268[0:Res:1.2,267.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(u),0) LE(f(v),0) LE(f(w),0) LE(f(u),0). % 0.19/0.53 269[0:Obv:268.4] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(v),0) LE(f(w),0) LE(f(u),0). % 0.19/0.53 270[0:MRR:269.0,269.1,243.0,244.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(v),0) LE(f(w),0) LE(f(u),0). % 0.19/0.53 271[0:Res:1.2,270.0] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0) LE(f(u),0). % 0.19/0.53 272[0:Obv:271.3] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.19/0.53 273[0:MRR:272.0,272.1,243.0,244.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.19/0.53 274[0:Res:1.2,273.0] || E(0,f(u)) E(0,f(suc(u)))* -> LE(f(u),0) LE(f(u),0). % 0.19/0.53 275[0:Obv:274.2] || E(0,f(u)) E(0,f(suc(u)))* -> LE(f(u),0). % 0.19/0.53 276[0:MRR:275.0,275.1,243.0,244.0] || -> LE(f(u),0)*. % 0.19/0.53 277[0:UnC:276.0,9.0] || -> . % 0.19/0.53 % SZS output end Refutation % 0.19/0.53 Formulae used in the proof : clause_469 clause_398 clause_451 clause_29 clause_560 clause_476 clause_97 clause_443 clause_287 clause_547 clause_563 clause_539 clause_59 clause_222 clause_44 clause_442 clause_89 clause_151 % 0.19/0.53 %------------------------------------------------------------------------------