%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : DAT014_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n016.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 : Sat Jul 16 01:31:46 EDT 2022 % Result : Theorem 0.74s 1.05s % Output : Refutation 0.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : DAT014_1 : TPTP v8.1.0. Released v5.0.0. % 0.03/0.12 % Command : spasst-tptp-script %s %d % 0.11/0.32 % Computer : n016.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Fri Jul 1 21:11:43 EDT 2022 % 0.11/0.32 % CPUTime : % 0.17/0.44 % Using integer theory % 0.74/1.05 % 0.74/1.05 % 0.74/1.05 % SZS status Theorem for /tmp/SPASST_22035_n016.cluster.edu % 0.74/1.05 % 0.74/1.05 SPASS V 2.2.22 in combination with yices. % 0.74/1.05 SPASS beiseite: Proof found by SPASS and SMT. % 0.74/1.05 Problem: /tmp/SPASST_22035_n016.cluster.edu % 0.74/1.05 SPASS derived 100 clauses, backtracked 27 clauses and kept 94 clauses. % 0.74/1.05 SPASS backtracked 7 times (1 times due to theory inconsistency). % 0.74/1.05 SPASS allocated 6342 KBytes. % 0.74/1.05 SPASS spent 0:00:00.06 on the problem. % 0.74/1.05 0:00:00.00 for the input. % 0.74/1.05 0:00:00.00 for the FLOTTER CNF translation. % 0.74/1.05 0:00:00.00 for inferences. % 0.74/1.05 0:00:00.00 for the backtracking. % 0.74/1.05 0:00:00.01 for the reduction. % 0.74/1.05 0:00:00.05 for interacting with the SMT procedure. % 0.74/1.05 % 0.74/1.05 % 0.74/1.05 % SZS output start CNFRefutation for /tmp/SPASST_22035_n016.cluster.edu % 0.74/1.05 % 0.74/1.05 % Here is a proof with depth 4, length 49 : % 0.74/1.05 4[0:Inp] || -> lesseq(6,skc4)*. % 0.74/1.05 5[0:Inp] || -> lesseq(skc4,15)*. % 0.74/1.05 6[0:Inp] || greater(read(skc3,skc4),5)* -> . % 0.74/1.05 9[0:Inp] || lesseq(U,10) lesseq(1,U) -> greater(read(skc3,U),U)*. % 0.74/1.05 10[0:Inp] || lesseq(U,20) lesseq(11,U) -> greater(read(skc3,U),minus(20,U))*. % 0.74/1.05 24[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 0.74/1.05 43[0:ArS:6.0] || less(5,read(skc3,skc4))* -> . % 0.74/1.05 44[0:TOC:43.0] || -> lesseq(read(skc3,skc4),5)*. % 0.74/1.05 45[0:ArS:9.2] || lesseq(U,10) lesseq(1,U) -> less(U,read(skc3,U))*. % 0.74/1.05 46[0:TOC:45.1] || -> less(U,1) less(U,read(skc3,U))* less(10,U). % 0.74/1.05 47[0:ArS:10.2] || lesseq(U,20) lesseq(11,U) -> less(plus(uminus(U),20),read(skc3,U))*. % 0.74/1.05 48[0:TOC:47.1] || -> less(U,11) less(20,U) less(plus(uminus(U),20),read(skc3,U))*. % 0.74/1.05 52(e)[0:OCE:4.0,24.1] || -> equal(skc4,6) less(6,skc4)*. % 0.74/1.05 56[1:Spt:52.0] || -> equal(skc4,6)**. % 0.74/1.05 59[1:Rew:56.0,44.0] || -> lesseq(read(skc3,6),5)*. % 0.74/1.05 67[1:OCh:46.1,59.0] || -> less(6,1) less(10,6)* less(6,5). % 0.74/1.05 68(e)[1:ArS:67.2] || -> . % 0.74/1.05 69[1:Spt:68.0,52.0,56.0] || equal(skc4,6)** -> . % 0.74/1.05 70[1:Spt:68.0,52.1] || -> less(6,skc4)*. % 0.74/1.05 79(e)[0:OCh:44.0,46.1] || -> less(skc4,1) less(10,skc4)* less(skc4,5). % 0.74/1.05 82[2:Spt:79.0] || -> less(skc4,1)*. % 0.74/1.05 84[2:OCh:82.0,4.0] || -> less(6,1)*. % 0.74/1.05 86(e)[2:ArS:84.0] || -> . % 0.74/1.05 87[2:Spt:86.0,79.0,82.0] || less(skc4,1)* -> . % 0.74/1.05 88(e)[2:Spt:86.0,79.1,79.2] || -> less(10,skc4)* less(skc4,5). % 0.74/1.05 89[2:TOC:87.0] || -> lesseq(1,skc4)*. % 0.74/1.05 90[3:Spt:88.0] || -> less(10,skc4)*. % 0.74/1.05 95(e)[2:OCE:89.0,24.1] || -> equal(skc4,1) less(1,skc4)*. % 0.74/1.05 99(e)[4:Spt:95.0] || -> equal(skc4,1)**. % 0.74/1.05 105[4:Rew:99.0,90.0] || -> less(10,1)*. % 0.74/1.05 110(e)[4:ArS:105.0] || -> . % 0.74/1.05 113[4:Spt:110.0,95.0,99.0] || equal(skc4,1)** -> . % 0.74/1.05 114[4:Spt:110.0,95.1] || -> less(1,skc4)*. % 0.74/1.05 146[0:OCh:48.2,44.0] || -> less(skc4,11) less(20,skc4) less(plus(uminus(skc4),20),5)*. % 0.74/1.05 148(e)[0:ArS:146.2] || -> less(skc4,11) less(20,skc4)* less(15,skc4). % 0.74/1.05 152[5:Spt:148.0] || -> less(skc4,11)*. % 0.74/1.05 189[5:ThR:152,90] || -> . % 0.74/1.05 190[5:Spt:189.0,148.0,152.0] || less(skc4,11)* -> . % 0.74/1.05 191(e)[5:Spt:189.0,148.1,148.2] || -> less(20,skc4)* less(15,skc4). % 0.74/1.05 193[6:Spt:191.0] || -> less(20,skc4)*. % 0.74/1.05 196[6:OCh:193.0,5.0] || -> less(20,15)*. % 0.74/1.05 197(e)[6:ArS:196.0] || -> . % 0.74/1.05 198[6:Spt:197.0,191.0,193.0] || less(20,skc4)* -> . % 0.74/1.05 199[6:Spt:197.0,191.1] || -> less(15,skc4)*. % 0.74/1.05 203(e)[6:OCE:199.0,5.0] || -> . % 0.74/1.05 206[3:Spt:203.0,88.0,90.0] || less(10,skc4)* -> . % 0.74/1.05 207[3:Spt:203.0,88.1] || -> less(skc4,5)*. % 0.74/1.05 209[3:OCh:207.0,70.0] || -> less(6,5)*. % 0.74/1.05 212(e)[3:ArS:209.0] || -> . % 0.74/1.05 % 0.74/1.05 % SZS output end CNFRefutation for /tmp/SPASST_22035_n016.cluster.edu % 0.74/1.05 % 0.74/1.05 Formulae used in the proof : fof_co1 fof_ax1 % 0.74/1.05 % 0.74/1.05 SPASS+T ended %------------------------------------------------------------------------------