%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO669-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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:26 EDT 2022 % Result : Unsatisfiable 0.57s 0.72s % Output : Refutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO669-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat Jul 9 02:31:26 EDT 2022 % 0.12/0.34 % CPUTime : % 0.57/0.72 % 0.57/0.72 SPASS V 3.9 % 0.57/0.72 SPASS beiseite: Proof found. % 0.57/0.72 % SZS status Theorem % 0.57/0.72 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.57/0.72 SPASS derived 1712 clauses, backtracked 0 clauses, performed 0 splits and kept 441 clauses. % 0.57/0.72 SPASS allocated 65015 KBytes. % 0.57/0.72 SPASS spent 0:00:00.37 on the problem. % 0.57/0.72 0:00:00.04 for the input. % 0.57/0.72 0:00:00.00 for the FLOTTER CNF translation. % 0.57/0.72 0:00:00.06 for inferences. % 0.57/0.72 0:00:00.00 for the backtracking. % 0.57/0.72 0:00:00.24 for the reduction. % 0.57/0.72 % 0.57/0.72 % 0.57/0.72 Here is a proof with depth 3, length 117 : % 0.57/0.72 % SZS output start Refutation % 0.57/0.72 1[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.57/0.72 2[0:Inp] || E(f(u),f(suc(suc(u))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(0),f(u)) -> iLEQ(suc(u),suc(u)). % 0.57/0.72 3[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(s(0))))* -> E(s(s(0)),f(suc(suc(suc(u))))) LE(f(u),s(s(0))). % 0.57/0.72 4[0:Inp] || E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(u))) E(f(u),f(suc(u))) E(s(s(0)),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 0.57/0.72 5[0:Inp] || E(f(u),f(suc(suc(u))))* E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(f(v),f(suc(v))) E(s(0),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))*. % 0.57/0.72 6[0:Inp] || LE(f(suc(suc(u))),s(s(s(0))))* -> E(s(s(0)),f(suc(suc(u)))) LE(f(u),s(s(0))). % 0.57/0.72 7[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 0.57/0.72 8[0:Inp] || E(0,f(suc(u))) E(0,f(u)) E(0,f(v)) E(0,f(suc(suc(v)))) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(u)))*. % 0.57/0.72 9[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.57/0.72 10[0:Inp] || LE(f(suc(u)),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(u))). % 0.57/0.72 11[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(v)) E(0,f(suc(suc(v)))) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 12[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) -> iLEQ(suc(u),suc(u)). % 0.57/0.72 13[0:Inp] || E(0,f(suc(u))) E(0,f(u)) E(f(v),f(suc(suc(v))))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(0,f(suc(suc(v)))) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))*. % 0.57/0.72 14[0:Inp] || -> LE(f(u),s(s(s(0))))*. % 0.57/0.72 15[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.57/0.72 16[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u))))* E(0,f(v)) E(0,f(suc(v))) iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) -> E(f(v),f(suc(v)))*. % 0.57/0.72 17[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.57/0.72 18[0:Inp] || E(f(u),f(suc(suc(u))))* E(0,f(suc(suc(suc(u))))) E(0,f(u)) E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u))) -> iLEQ(suc(u),suc(u)). % 0.57/0.72 19[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(v)))* E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(v)) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 0.57/0.72 20[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 21[0:Inp] || E(f(u),f(suc(suc(u))))* E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(suc(v)))) E(f(v),f(suc(suc(v))))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(f(v),f(suc(v))) E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> . % 0.57/0.72 22[0:Inp] || E(f(u),f(suc(suc(u))))* E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))*. % 0.57/0.72 23[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v)))+ E(s(0),f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.57/0.72 24[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 0.57/0.72 25[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(0,f(suc(suc(v)))) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) -> . % 0.57/0.72 26[0:Inp] || E(s(s(0)),f(u)) E(f(v),f(suc(v))) E(s(s(0)),f(suc(u))) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(suc(u)))))* E(s(s(0)),f(suc(v))) E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(v)) -> E(f(v),f(suc(suc(v))))*. % 0.57/0.72 27[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(v),f(suc(suc(v))))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(0,f(suc(suc(v)))) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))*. % 0.57/0.72 28[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.57/0.72 29[0:Inp] || E(s(s(0)),f(u)) E(f(v),f(suc(v))) E(s(s(0)),f(suc(u)))* E(f(v),f(suc(suc(v))))* iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(suc(v)))))* E(s(s(0)),f(v)) -> E(f(u),f(suc(u)))*. % 0.57/0.72 30[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u)))+ E(0,f(suc(v))) iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.57/0.72 31[0:Inp] || LE(f(suc(u)),s(s(s(0))))* -> E(s(s(0)),f(suc(u))) LE(f(u),s(s(0))). % 0.57/0.72 32[0:Inp] || E(s(s(0)),f(u)) E(f(v),f(suc(v))) E(s(s(0)),f(suc(u))) E(f(v),f(suc(suc(v))))* iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v)))) E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(suc(u)))))* E(s(s(0)),f(suc(v))) E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(suc(v)))))* E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(v)) -> . % 0.57/0.72 33[0:Inp] || LE(f(u),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(u)). % 0.57/0.72 34[0:Inp] || iLEQ(suc(u),suc(v))* 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(u)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.57/0.72 35[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) iLEQ(suc(u),suc(v))* E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(suc(u)))))* E(s(s(0)),f(suc(v)))* E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(v)) -> E(f(v),f(suc(v)))*. % 0.57/0.72 36[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(u)))). % 0.57/0.72 37[0:Inp] || E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u))) E(0,f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 0.57/0.72 38[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(v))) E(f(v),f(suc(v))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 39[0:Inp] || E(s(0),f(suc(suc(u)))) E(s(0),f(suc(u))) E(f(u),f(suc(u))) E(s(0),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 0.57/0.72 40[0:Inp] || LE(f(u),s(s(s(0))))* -> E(s(s(0)),f(u)) LE(f(u),s(s(0))). % 0.57/0.72 41[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(v)) E(0,f(suc(v))) iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 42[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u))))* E(0,f(v)) E(0,f(suc(suc(v)))) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) -> E(f(v),f(suc(suc(v))))*. % 0.57/0.72 43[0:Inp] || E(s(s(0)),f(u)) E(f(v),f(suc(v))) E(s(s(0)),f(suc(u)))* iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(v)) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 44[0:Inp] || E(s(s(0)),f(u)) E(f(v),f(suc(v))) E(s(s(0)),f(suc(u))) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(v))) E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(v)) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 45[0:Inp] || LE(f(z__dfg),0)* -> . % 0.57/0.72 46[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(suc(v)))) E(f(v),f(suc(suc(v))))* E(s(0),f(suc(v))) E(f(v),f(suc(v))) E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))*. % 0.57/0.72 47[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 0.57/0.72 48[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u))))). % 0.57/0.72 49[0:Inp] || E(s(s(0)),f(u)) E(f(v),f(suc(v))) E(s(s(0)),f(suc(u))) E(f(v),f(suc(suc(v))))* iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(v))) E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(suc(v)))))* E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(v)) -> E(f(u),f(suc(suc(u))))*. % 0.57/0.72 50[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(v)) E(s(0),f(suc(suc(v)))) E(f(v),f(suc(suc(v))))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(f(v),f(suc(v))) E(s(0),f(suc(suc(suc(v)))))* E(f(u),f(suc(u))) E(s(0),f(u)) iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))*. % 0.57/0.72 51[0:MRR:40.0,14.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.57/0.72 52[0:MRR:31.0,14.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u)))*. % 0.57/0.72 53[0:MRR:6.0,14.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(u))))*. % 0.57/0.72 54[0:MRR:3.0,14.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(suc(u)))))*. % 0.57/0.72 55[0:MRR:37.2,1.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 0.57/0.72 56[0:MRR:39.2,28.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 0.57/0.72 57[0:MRR:4.2,15.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 0.57/0.72 58[0:MRR:18.0,18.5,55.3,1.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 0.57/0.72 59[0:MRR:2.0,2.4,56.3,28.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 0.57/0.72 60[0:MRR:12.2,12.4,57.3,15.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 0.57/0.72 61[0:MRR:8.5,30.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u))))+ iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 62[0:MRR:41.6,30.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v))))+ iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 63[0:MRR:38.4,23.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 64[0:MRR:47.4,23.5] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 65[0:MRR:13.2,13.7,61.6,30.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))*. % 0.57/0.72 66[0:MRR:16.4,16.8,62.7,30.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))*. % 0.57/0.72 67[0:MRR:19.4,34.5] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 68[0:MRR:43.1,34.6] || iLEQ(suc(u),suc(v))* 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(u)))* E(s(s(0)),f(suc(suc(v))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 0.57/0.72 69[0:MRR:11.6,11.8,62.6,61.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 70[0:MRR:22.0,22.6,64.6,23.5] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))*. % 0.57/0.72 71[0:MRR:46.3,46.5,63.7,23.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))*. % 0.57/0.72 72[0:MRR:20.5,20.6,64.7,63.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))+ E(s(0),f(suc(suc(v)))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 73[0:MRR:29.1,29.3,34.6,68.7] || iLEQ(suc(u),suc(v))* 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(u)))* E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))*. % 0.57/0.72 74[0:MRR:35.3,35.6,67.6,34.5] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))*. % 0.57/0.72 75[0:MRR:27.3,27.8,27.10,69.7,62.6,65.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))*. % 0.57/0.72 76[0:MRR:42.4,42.8,42.10,69.8,66.7,61.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))*. % 0.57/0.72 77[0:MRR:44.1,44.6,67.7,68.6] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u))))*+ E(s(s(0)),f(suc(suc(v))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 0.57/0.72 78[0:MRR:5.0,5.6,5.8,72.7,70.7,63.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))*. % 0.57/0.72 79[0:MRR:50.3,50.6,50.8,72.8,64.7,71.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))*. % 0.57/0.72 80[0:MRR:25.4,25.5,25.10,25.12,76.8,75.8,66.7,65.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(u),suc(v))* -> . % 0.57/0.72 81[0:MRR:26.1,26.5,26.8,74.7,77.7,68.6] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))*. % 0.57/0.72 82[0:MRR:49.1,49.3,49.7,67.7,77.8,73.7] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))*. % 0.57/0.72 83[0:MRR:21.0,21.4,21.7,21.10,79.8,78.8,70.7,71.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(u)))))*+ E(s(0),f(suc(suc(suc(v)))))* -> . % 0.57/0.72 84[0:MRR:32.1,32.3,32.6,32.9,74.7,81.8,82.8,73.7] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(suc(suc(v)))))*+ E(s(s(0)),f(suc(suc(suc(u)))))* -> . % 0.57/0.72 106[0:Res:54.1,60.3] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))* -> LE(f(u),s(s(0))) iLEQ(suc(u),suc(u))*. % 0.57/0.72 107[0:MRR:106.0,106.1,106.2,51.1,52.1,53.1] || -> LE(f(u),s(s(0)))* iLEQ(suc(u),suc(u))*. % 0.57/0.72 1753[0:Res:54.1,84.7] || iLEQ(suc(u),suc(v))* 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(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(suc(suc(u)))))* -> LE(f(v),s(s(0))). % 0.57/0.72 1754[0:MRR:1753.1,1753.3,1753.6,51.1,52.1,53.1] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> LE(f(v),s(s(0)))*. % 0.57/0.72 1837[0:Res:54.1,1754.4] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))* -> LE(f(u),s(s(0))) LE(f(v),s(s(0)))*. % 0.57/0.72 1838[0:MRR:1837.1,1837.2,1837.3,51.1,52.1,53.1] || iLEQ(suc(u),suc(v))*+ -> LE(f(u),s(s(0)))* LE(f(v),s(s(0)))*. % 0.57/0.72 1842[0:Res:107.1,1838.0] || -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(u),s(s(0)))*. % 0.57/0.72 1863[0:Obv:1842.1] || -> LE(f(u),s(s(0)))*. % 0.57/0.72 1864[0:MRR:33.0,1863.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.57/0.72 1865[0:MRR:10.0,1863.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.57/0.72 1866[0:MRR:36.0,1863.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 0.57/0.72 1867[0:MRR:48.0,1863.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u)))))*. % 0.57/0.72 1941[0:Res:1867.1,83.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))* -> LE(f(u),s(0)). % 0.57/0.72 1944[0:Res:1867.1,59.3] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))* -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.57/0.72 1949[0:MRR:1944.0,1944.1,1944.2,1864.1,1865.1,1866.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.57/0.72 1957[0:MRR:1941.1,1941.4,1941.5,1864.1,1865.1,1866.1] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ -> LE(f(u),s(0)). % 0.57/0.78 2544[0:Res:1867.1,1957.4] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 0.57/0.78 2545[0:MRR:2544.1,2544.2,2544.3,1864.1,1865.1,1866.1] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 0.57/0.78 2548[0:Res:1949.1,2545.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 0.57/0.78 2566[0:Obv:2548.1] || -> LE(f(u),s(0))*. % 0.57/0.78 2567[0:MRR:9.0,2566.0] || -> E(0,f(u))* LE(f(u),0). % 0.57/0.78 2568[0:MRR:17.0,2566.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.57/0.78 2569[0:MRR:24.0,2566.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 0.57/0.78 2570[0:MRR:7.0,2566.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 0.57/0.78 2641[0:Res:2570.0,80.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u))))* E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))* iLEQ(suc(u),suc(v))* -> LE(f(u),0). % 0.57/0.78 2644[0:Res:2570.0,58.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.57/0.78 2648[0:MRR:2644.0,2644.1,2644.2,2567.0,2568.0,2569.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.57/0.78 2656[0:MRR:2641.0,2641.2,2641.4,2567.0,2568.0,2569.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* -> LE(f(v),0). % 0.57/0.78 2835[0:Res:2570.0,2656.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* iLEQ(suc(v),suc(u))* -> LE(f(u),0) LE(f(v),0). % 0.57/0.78 2836[0:MRR:2835.0,2835.1,2835.2,2567.0,2568.0,2569.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.57/0.78 2840[0:Res:2648.1,2836.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 0.57/0.78 2844[0:Obv:2840.1] || -> LE(f(u),0)*. % 0.57/0.78 2845[0:UnC:2844.0,45.0] || -> . % 0.57/0.78 % SZS output end Refutation % 0.57/0.78 Formulae used in the proof : clause_59 clause_257 clause_88 clause_246 clause_262 clause_301 clause_207 clause_179 clause_18 clause_12 clause_106 clause_267 clause_139 clause_299 clause_25 clause_9 clause_260 clause_295 clause_121 clause_144 clause_292 clause_27 clause_7 clause_4 clause_100 clause_276 clause_55 clause_44 clause_87 clause_248 clause_153 clause_122 clause_272 clause_76 clause_95 clause_196 clause_143 clause_247 clause_72 clause_222 clause_167 clause_90 clause_229 clause_74 clause_151 clause_181 clause_236 clause_263 clause_278 clause_33 % 0.57/0.78 %------------------------------------------------------------------------------