%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWC449_1 : TPTP v8.3.0. Released v8.3.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n013.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 : 300s % DateTime : Tue May 14 09:02:08 EDT 2024 % Result : Theorem 1.89s 1.74s % Output : Refutation 1.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWC449_1 : TPTP v8.3.0. Released v8.3.0. % 0.08/0.14 % Command : spasst-tptp-script %s %d % 0.14/0.35 % Computer : n013.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Mon May 13 14:45:38 EDT 2024 % 0.14/0.36 % CPUTime : % 0.20/0.50 % Using integer theory % 1.89/1.74 % 1.89/1.74 % 1.89/1.74 % SZS status Theorem for /tmp/SPASST_15896_n013.cluster.edu % 1.89/1.74 % 1.89/1.74 SPASS V 2.2.22 in combination with yices. % 1.89/1.74 SPASS beiseite: Proof found by SPASS. % 1.89/1.74 Problem: /tmp/SPASST_15896_n013.cluster.edu % 1.89/1.74 SPASS derived 4803 clauses, backtracked 360 clauses and kept 1458 clauses. % 1.89/1.74 SPASS backtracked 11 times (0 times due to theory inconsistency). % 1.89/1.74 SPASS allocated 11413 KBytes. % 1.89/1.74 SPASS spent 0:00:00.69 on the problem. % 1.89/1.74 0:00:00.00 for the input. % 1.89/1.74 0:00:00.00 for the FLOTTER CNF translation. % 1.89/1.74 0:00:00.04 for inferences. % 1.89/1.74 0:00:00.03 for the backtracking. % 1.89/1.74 0:00:00.50 for the reduction. % 1.89/1.74 0:00:00.09 for interacting with the SMT procedure. % 1.89/1.74 % 1.89/1.74 % 1.89/1.74 % SZS output start CNFRefutation for /tmp/SPASST_15896_n013.cluster.edu % 1.89/1.74 % 1.89/1.74 % Here is a proof with depth 6, length 86 : % 1.89/1.74 13[0:Inp] || -> equal(g1,1)**. % 1.89/1.74 14[0:Inp] || -> equal(h0,2)**. % 1.89/1.74 15[0:Inp] || -> greatereq(skc1,0)*. % 1.89/1.74 16[0:Inp] || -> equal(v1(U),fast(U))**. % 1.89/1.74 17[0:Inp] || -> equal(v0(U),small(U))**. % 1.89/1.74 18(e)[0:Inp] || equal(small(skc1),fast(skc1))** -> . % 1.89/1.74 19[0:Inp] || -> equal(u1(g1,h1(U)),v1(U))**. % 1.89/1.74 20[0:Inp] || -> equal(u0(g0(U),h0),v0(U))**. % 1.89/1.74 21[0:Inp] || -> equal(times(2,plus(U,U)),h1(U))*. % 1.89/1.74 22[0:Inp] || -> equal(times(2,plus(U,U)),g0(U))*. % 1.89/1.74 23[0:Inp] || lesseq(U,0) -> equal(u1(U,V),V)**. % 1.89/1.74 24[0:Inp] || lesseq(U,0) -> equal(u0(U,V),V)**. % 1.89/1.74 25[0:Inp] || -> equal(f0(U,V),times(plus(2,V),V))*. % 1.89/1.74 26[0:Inp] || -> equal(times(plus(2,U),U),f1(U))* lesseq(U,0)*. % 1.89/1.74 27[0:Inp] || lesseq(U,0)* -> equal(f1(U),times(plus(2,U),1)). % 1.89/1.74 28[0:Inp] || equal(U,minus(V,1)) -> lesseq(V,0) equal(f1(u1(U,W)),u1(V,W))*. % 1.89/1.74 29[0:Inp] || equal(U,minus(V,1)) -> lesseq(V,0) equal(f0(u0(U,W),V),u0(V,W))**. % 1.89/1.74 36[0:ThA] || -> equal(plus(uminus(U),U),0)**. % 1.89/1.74 38[0:ThA] || -> equal(plus(0,U),U)**. % 1.89/1.74 39[0:ThA] || -> lesseq(U,U)*. % 1.89/1.74 42[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 1.89/1.74 43[0:ThA] || -> lesseq(U,V) less(plus(V,W),plus(U,W))*. % 1.89/1.74 49[0:ThA] || -> equal(times(1,U),U)**. % 1.89/1.74 61[0:ArS:15.0] || -> lesseq(0,skc1)*. % 1.89/1.74 62[0:Rew:14.0,20.0,17.0,20.0] || -> equal(u0(g0(U),2),small(U))**. % 1.89/1.74 63[0:Rew:13.0,19.0,16.0,19.0] || -> equal(u1(1,h1(U)),fast(U))**. % 1.89/1.74 64[0:ArS:25.0] || -> equal(f0(U,V),times(plus(V,2),V))*. % 1.89/1.74 65[0:TOC:24.0] || -> less(0,U) equal(u0(U,V),V)**. % 1.89/1.74 66[0:TOC:23.0] || -> less(0,U) equal(u1(U,V),V)**. % 1.89/1.74 67[0:ArS:26.0] || -> lesseq(U,0)* equal(times(plus(U,2),U),f1(U))*. % 1.89/1.74 68[0:ArS:27.1] || lesseq(U,0)* -> equal(f1(U),times(1,plus(U,2))). % 1.89/1.74 69[0:TOC:68.0] || -> less(0,U)* equal(f1(U),times(1,plus(U,2))). % 1.89/1.74 70[0:Rew:49.0,69.1] || -> less(0,U)* equal(f1(U),plus(U,2)). % 1.89/1.74 71[0:ArS:28.0] || equal(U,plus(V,-1)) -> lesseq(V,0) equal(f1(u1(U,W)),u1(V,W))*. % 1.89/1.74 72[0:ArS:29.0] || equal(U,plus(V,-1)) -> lesseq(V,0) equal(f0(u0(U,W),V),u0(V,W))**. % 1.89/1.74 77(e)[0:OCE:61.0,42.1] || -> equal(skc1,0) less(0,skc1)*. % 1.89/1.74 79[1:Spt:77.0] || -> equal(skc1,0)**. % 1.89/1.74 81[1:Rew:79.0,18.0] || equal(small(0),fast(0))** -> . % 1.89/1.74 92[0:SpR:21.0,22.0] || -> equal(h1(U),g0(U))**. % 1.89/1.74 94[0:SpR:21.0,63.0] || -> equal(u1(1,times(2,plus(U,U))),fast(U))**. % 1.89/1.74 96[0:Rew:92.0,63.0] || -> equal(u1(1,g0(U)),fast(U))**. % 1.89/1.74 101[0:SpR:65.1,62.0] || -> less(0,g0(U))* equal(small(U),2). % 1.89/1.74 108[0:SpR:22.0,101.0] || -> less(0,times(2,plus(U,U)))* equal(small(U),2). % 1.89/1.74 111[0:ArS:108.0] || -> less(0,plus(U,U))* equal(small(U),2). % 1.89/1.74 116[0:OCE:70.0,39.0] || -> equal(f1(0),plus(0,2))**. % 1.89/1.74 117[0:ArS:116.0] || -> equal(f1(0),2)**. % 1.89/1.74 135[0:SpR:38.0,111.0] || -> less(0,0)* equal(small(0),2). % 1.89/1.74 142[0:ArS:135.0] || -> equal(small(0),2)**. % 1.89/1.74 143[1:Rew:142.0,81.0] || equal(fast(0),2)** -> . % 1.89/1.74 166[0:SpR:38.0,94.0] || -> equal(u1(1,times(2,0)),fast(0))**. % 1.89/1.74 169[0:ArS:166.0] || -> equal(u1(1,0),fast(0))**. % 1.89/1.74 176[0:SpR:67.1,64.0] || -> lesseq(U,0) equal(f0(V,U),f1(U))**. % 1.89/1.74 185[0:Rew:176.1,72.2] || equal(U,plus(V,-1))* -> lesseq(V,0) equal(u0(V,W),f1(V))**. % 1.89/1.74 187[0:AED:185.0] || -> lesseq(U,0) equal(u0(U,V),f1(U))**. % 1.89/1.74 195[0:SpR:187.1,62.0] || -> lesseq(g0(U),0)* equal(f1(g0(U)),small(U)). % 1.89/1.74 222[0:SpR:66.1,71.2] || equal(U,plus(V,-1))*+ -> less(0,U)* lesseq(V,0) equal(u1(V,W),f1(W))**. % 1.89/1.74 227[0:SpR:22.0,195.0] || -> lesseq(times(2,plus(U,U)),0)* equal(f1(g0(U)),small(U))**. % 1.89/1.74 230[0:OCE:195.0,101.0] || -> equal(f1(g0(U)),small(U))** equal(small(U),2). % 1.89/1.74 232[0:ArS:227.0] || -> lesseq(plus(U,U),0)* equal(f1(g0(U)),small(U))**. % 1.89/1.74 243[0:OCh:232.0,43.1] || -> equal(f1(g0(U)),small(U))** lesseq(U,V) less(plus(V,U),0)*. % 1.89/1.74 788[0:SpL:36.0,222.0] || equal(U,0) -> less(0,U)* lesseq(uminus(-1),0) equal(u1(uminus(-1),V),f1(V))**. % 1.89/1.74 792(e)[0:ArS:788.3] || equal(U,0) -> less(0,U)* equal(u1(1,V),f1(V))**. % 1.89/1.74 794(e)[2:Spt:792.2] || -> equal(u1(1,U),f1(U))**. % 1.89/1.74 795[2:Rew:794.0,169.0] || -> equal(f1(0),fast(0))**. % 1.89/1.74 798[2:Rew:117.0,795.0] || -> equal(fast(0),2)**. % 1.89/1.74 799(e)[2:MRR:798.0,143.0] || -> . % 1.89/1.74 812[2:Spt:799.0,792.0,792.1] || equal(U,0) -> less(0,U)*. % 1.89/1.74 815[2:OCE:812.1,812.1] || equal(0,0)* equal(0,0)* -> . % 1.89/1.74 839(e)[2:ArS:815.1] || -> . % 1.89/1.74 853[1:Spt:839.0,77.0,79.0] || equal(skc1,0)** -> . % 1.89/1.74 854[1:Spt:839.0,77.1] || -> less(0,skc1)*. % 1.89/1.74 864[2:Spt:792.2] || -> equal(u1(1,U),f1(U))**. % 1.89/1.74 867[2:Rew:864.0,96.0] || -> equal(f1(g0(U)),fast(U))**. % 1.89/1.74 873[2:Rew:867.0,243.0] || -> equal(small(U),fast(U)) lesseq(U,V) less(plus(V,U),0)*. % 1.89/1.74 877[2:Rew:867.0,230.0] || -> equal(small(U),fast(U))** equal(small(U),2). % 1.89/1.74 919[2:SpL:877.0,18.0] || equal(fast(skc1),fast(skc1)) -> equal(small(skc1),2)**. % 1.89/1.74 920[2:Obv:919.0] || -> equal(small(skc1),2)**. % 1.89/1.74 921[2:Rew:920.0,18.0] || equal(fast(skc1),2)** -> . % 1.89/1.74 6224[2:SpR:38.0,873.2] || -> equal(small(U),fast(U)) lesseq(U,0) less(U,0)*. % 1.89/1.74 7555[2:OCE:6224.2,854.0] || -> equal(small(skc1),fast(skc1)) lesseq(skc1,0)*. % 1.89/1.74 7587[2:Rew:920.0,7555.0] || -> equal(fast(skc1),2) lesseq(skc1,0)*. % 1.89/1.74 7588[2:MRR:7587.0,921.0] || -> lesseq(skc1,0)*. % 1.89/1.74 7646(e)[2:OCE:7588.0,854.0] || -> . % 1.89/1.74 7653[2:Spt:7646.0,792.0,792.1] || equal(U,0) -> less(0,U)*. % 1.89/1.74 7812[2:OCE:7653.1,39.0] || equal(0,0)* -> . % 1.89/1.74 7835(e)[2:ArS:7812.0] || -> . % 1.89/1.74 % 1.89/1.74 % SZS output end CNFRefutation for /tmp/SPASST_15896_n013.cluster.edu % 1.89/1.74 % 1.89/1.74 Formulae used in the proof : fof_v0 fof_formula_8 fof_formula_3 fof_conjecture_1 fof_formula_12 fof_formula_6 fof_formula_11 fof_formula_5 fof_formula_9 fof_formula_2 fof_formula_10 fof_formula_4 fof_formula_1 fof_formula_7 % 1.98/1.80 % 1.98/1.80 SPASS+T ended %------------------------------------------------------------------------------