%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : DAT069_1 : TPTP v8.1.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n008.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:32:04 EDT 2022 % Result : Theorem 0.80s 1.08s % Output : Refutation 0.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : DAT069_1 : TPTP v8.1.0. Released v5.5.0. % 0.07/0.13 % Command : spasst-tptp-script %s %d % 0.12/0.34 % Computer : n008.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 : Fri Jul 1 20:55:38 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.47 % Using integer theory % 0.80/1.08 % 0.80/1.08 % 0.80/1.08 % SZS status Theorem for /tmp/SPASST_20860_n008.cluster.edu % 0.80/1.08 % 0.80/1.08 SPASS V 2.2.22 in combination with yices. % 0.80/1.08 SPASS beiseite: Proof found by SPASS. % 0.80/1.08 Problem: /tmp/SPASST_20860_n008.cluster.edu % 0.80/1.08 SPASS derived 118 clauses, backtracked 37 clauses and kept 174 clauses. % 0.80/1.08 SPASS backtracked 3 times (0 times due to theory inconsistency). % 0.80/1.08 SPASS allocated 6366 KBytes. % 0.80/1.08 SPASS spent 0:00:00.03 on the problem. % 0.80/1.08 0:00:00.00 for the input. % 0.80/1.08 0:00:00.01 for the FLOTTER CNF translation. % 0.80/1.08 0:00:00.00 for inferences. % 0.80/1.08 0:00:00.00 for the backtracking. % 0.80/1.08 0:00:00.01 for the reduction. % 0.80/1.08 0:00:00.00 for interacting with the SMT procedure. % 0.80/1.08 % 0.80/1.08 % 0.80/1.08 % SZS output start CNFRefutation for /tmp/SPASST_20860_n008.cluster.edu % 0.80/1.08 % 0.80/1.08 % Here is a proof with depth 3, length 38 : % 0.80/1.08 6[0:Inp] || -> heap(skc4)*. % 0.80/1.08 7[0:Inp] || -> equal(length(empty),0)**. % 0.80/1.08 9[0:Inp] || less(length(skc4),skc5)* -> . % 0.80/1.08 17(e)[0:Inp] || equal(sel(app(skc4,skc6),skc5),sel(skc4,skc5))** -> . % 0.80/1.08 19(e)[0:Inp] || heap(U) -> equal(U,empty) equal(app(get(U),toop(U)),U)**. % 0.80/1.08 26[0:Inp] || heap(U) -> equal(V,plus(1,length(U))) equal(sel(app(U,W),V),sel(U,V))**. % 0.80/1.08 31[0:ThA] || -> equal(plus(uminus(U),plus(U,V)),V)**. % 0.80/1.08 33[0:ThA] || -> equal(plus(plus(U,V),uminus(V)),U)**. % 0.80/1.08 35[0:ThA] || -> equal(plus(uminus(U),U),0)**. % 0.80/1.08 40[0:ThA] || -> less(plus(U,-1),U)*. % 0.80/1.08 41[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 0.80/1.08 60[0:TOC:9.0] || -> lesseq(skc5,length(skc4))*. % 0.80/1.08 63(e)[0:ArS:26.1] || heap(U) -> equal(V,plus(length(U),1)) equal(sel(app(U,W),V),sel(U,V))**. % 0.80/1.08 73(e)[0:Res:6.0,19.0] || -> equal(skc4,empty) equal(app(get(skc4),toop(skc4)),skc4)**. % 0.80/1.08 92[0:Res:63.2,17.0] || heap(skc4) -> equal(plus(length(skc4),1),skc5)**. % 0.80/1.08 97[0:MRR:92.0,6.0] || -> equal(plus(length(skc4),1),skc5)**. % 0.80/1.08 123(e)[1:Spt:73.0] || -> equal(skc4,empty)**. % 0.80/1.08 125[1:Rew:123.0,60.0] || -> lesseq(skc5,length(empty))*. % 0.80/1.08 126[1:Rew:123.0,97.0] || -> equal(plus(length(empty),1),skc5)**. % 0.80/1.08 155[1:Rew:7.0,125.0] || -> lesseq(skc5,0)*. % 0.80/1.08 156[1:Rew:7.0,126.0] || -> equal(skc5,plus(0,1))**. % 0.80/1.08 157(e)[1:ArS:156.0] || -> equal(skc5,1)**. % 0.80/1.08 158[1:Rew:157.0,155.0] || -> lesseq(1,0)*. % 0.80/1.08 159(e)[1:ArS:158.0] || -> . % 0.80/1.08 174[1:Spt:159.0,73.0,123.0] || equal(skc4,empty)** -> . % 0.80/1.08 175[1:Spt:159.0,73.1] || -> equal(app(get(skc4),toop(skc4)),skc4)**. % 0.80/1.08 179(e)[0:OCE:60.0,41.1] || -> equal(length(skc4),skc5) less(skc5,length(skc4))*. % 0.80/1.08 181[2:Spt:179.0] || -> equal(length(skc4),skc5)**. % 0.80/1.08 183[2:Rew:181.0,97.0] || -> equal(plus(skc5,1),skc5)**. % 0.80/1.08 188[2:SpR:183.0,31.0] || -> equal(plus(uminus(skc5),skc5),1)**. % 0.80/1.08 194[2:Rew:35.0,188.0] || -> equal(1,0)**. % 0.80/1.08 195(e)[2:ArS:194.0] || -> . % 0.80/1.08 196[2:Spt:195.0,179.0,181.0] || equal(length(skc4),skc5)** -> . % 0.80/1.08 197[2:Spt:195.0,179.1] || -> less(skc5,length(skc4))*. % 0.80/1.08 206[0:SpR:97.0,33.0] || -> equal(length(skc4),plus(skc5,uminus(1)))**. % 0.80/1.08 212(e)[0:ArS:206.0] || -> equal(length(skc4),plus(skc5,-1))**. % 0.80/1.08 213[2:Rew:212.0,197.0] || -> less(skc5,plus(skc5,-1))*. % 0.80/1.08 224(e)[2:OCE:213.0,40.0] || -> . % 0.80/1.08 % 0.80/1.08 % SZS output end CNFRefutation for /tmp/SPASST_20860_n008.cluster.edu % 0.80/1.08 % 0.80/1.08 Formulae used in the proof : fof_heap_type fof_th_4 fof_ax_1 fof_ax_20 fof_ax_26 fof_ax_30 % 0.80/1.08 % 0.80/1.08 SPASS+T ended %------------------------------------------------------------------------------