%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO657-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:22 EDT 2022 % Result : Unsatisfiable 0.19s 0.43s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO657-1 : TPTP v8.1.0. Released v7.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.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 14:25:00 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.43 % 0.19/0.43 SPASS V 3.9 % 0.19/0.43 SPASS beiseite: Proof found. % 0.19/0.43 % SZS status Theorem % 0.19/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.43 SPASS derived 136 clauses, backtracked 0 clauses, performed 0 splits and kept 86 clauses. % 0.19/0.43 SPASS allocated 63268 KBytes. % 0.19/0.43 SPASS spent 0:00:00.08 on the problem. % 0.19/0.43 0:00:00.03 for the input. % 0.19/0.43 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.43 0:00:00.01 for inferences. % 0.19/0.43 0:00:00.00 for the backtracking. % 0.19/0.43 0:00:00.02 for the reduction. % 0.19/0.43 % 0.19/0.43 % 0.19/0.43 Here is a proof with depth 3, length 51 : % 0.19/0.43 % SZS output start Refutation % 0.19/0.43 1[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u)))+ E(0,f(suc(v))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 0.19/0.43 2[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> E(s(0),f(suc(suc(u)))) LE(f(u),s(0)). % 0.19/0.43 3[0:Inp] || -> LE(f(u),s(s(0)))*. % 0.19/0.43 4[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.19/0.43 5[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u))))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(u)))* -> E(f(v),f(suc(v)))*. % 0.19/0.43 6[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(v),f(suc(v)))* E(0,f(suc(v))) -> E(f(u),f(suc(u)))*. % 0.19/0.43 7[0:Inp] || LE(f(u),s(s(0)))* -> E(s(0),f(u)) LE(f(u),s(0)). % 0.19/0.43 8[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.19/0.43 9[0:Inp] || E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u)))* E(0,f(u)) -> iLEQ(suc(u),suc(u)). % 0.19/0.43 10[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u)))* E(0,f(suc(v))) -> E(f(v),f(suc(v)))*. % 0.19/0.43 11[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.19/0.43 12[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(0,f(suc(v))) -> . % 0.19/0.43 13[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.19/0.43 14[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 0.19/0.43 15[0:Inp] || LE(f(z__dfg),0)* -> . % 0.19/0.43 16[0:Inp] || LE(f(suc(u)),s(s(0)))* -> E(s(0),f(suc(u))) LE(f(u),s(0)). % 0.19/0.43 17[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) 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.19/0.43 18[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)) -> iLEQ(suc(u),suc(u)). % 0.19/0.43 19[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v)))* -> E(f(u),f(suc(u)))*. % 0.19/0.43 20[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u))))* E(s(0),f(u)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* -> . % 0.19/0.43 21[0:MRR:7.0,3.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.19/0.43 22[0:MRR:16.0,3.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.19/0.43 23[0:MRR:2.0,3.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 0.19/0.43 24[0:MRR:9.2,11.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u))*. % 0.19/0.43 25[0:MRR:18.2,4.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u))*. % 0.19/0.43 26[0:MRR:6.5,1.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))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))*. % 0.19/0.43 27[0:MRR:10.5,1.5] || 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(v),suc(u))* -> E(f(u),f(suc(u)))*. % 0.19/0.43 28[0:MRR:5.6,17.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) 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)))*. % 0.19/0.43 29[0:MRR:19.6,17.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) 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)))*. % 0.19/0.43 30[0:MRR:12.6,12.7,26.6,27.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(u))))* iLEQ(suc(v),suc(u))* -> . % 0.19/0.43 31[0:MRR:20.7,20.8,28.6,29.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) 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(u))))* -> . % 0.19/0.43 34[0:Res:23.1,25.2] || E(s(0),f(u)) E(s(0),f(suc(u)))* -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.19/0.43 35[0:MRR:34.0,34.1,21.1,22.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.19/0.43 155[0:Res:23.1,31.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v)))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))* -> LE(f(v),s(0)). % 0.19/0.43 156[0:MRR:155.1,155.3,21.1,22.1] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> LE(f(v),s(0)). % 0.19/0.43 160[0:Res:23.1,156.3] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(u)))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 0.19/0.43 161[0:MRR:160.1,160.2,21.1,22.1] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 0.19/0.43 163[0:Res:35.1,161.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 0.19/0.43 170[0:Obv:163.1] || -> LE(f(u),s(0))*. % 0.19/0.43 171[0:MRR:8.0,170.0] || -> E(0,f(u))* LE(f(u),0). % 0.19/0.43 172[0:MRR:13.0,170.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.19/0.43 173[0:MRR:14.0,170.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 0.19/0.43 197[0:Res:173.0,24.2] || E(0,f(u)) E(0,f(suc(u))) -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.19/0.43 198[0:Res:173.0,30.4] || 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(v),suc(u))* -> LE(f(v),0). % 0.19/0.43 200[0:MRR:197.0,197.1,171.0,172.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.19/0.43 203[0:MRR:198.1,198.3,171.0,172.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))*+ iLEQ(suc(v),suc(u))* -> LE(f(v),0). % 0.19/0.43 246[0:Res:173.0,203.2] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* -> LE(f(u),0) LE(f(v),0). % 0.19/0.43 247[0:MRR:246.0,246.1,171.0,172.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.19/0.43 250[0:Res:200.1,247.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 0.19/0.43 252[0:Obv:250.1] || -> LE(f(u),0)*. % 0.19/0.43 253[0:UnC:252.0,15.0] || -> . % 0.19/0.43 % SZS output end Refutation % 0.19/0.43 Formulae used in the proof : clause_10 clause_45 clause_17 clause_23 clause_56 clause_31 clause_9 clause_34 clause_41 clause_15 clause_26 clause_43 clause_40 clause_51 clause_24 clause_32 clause_52 clause_5 clause_38 clause_33 % 0.19/0.43 %------------------------------------------------------------------------------