%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : DAT017_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n018.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:47 EDT 2022 % Result : Theorem 0.44s 1.02s % Output : Refutation 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : DAT017_1 : TPTP v8.1.0. Released v5.0.0. % 0.07/0.12 % Command : spasst-tptp-script %s %d % 0.12/0.33 % Computer : n018.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 : Fri Jul 1 19:16:03 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.46 % Using integer theory % 0.44/1.02 % 0.44/1.02 % 0.44/1.02 % SZS status Theorem for /tmp/SPASST_28239_n018.cluster.edu % 0.44/1.02 % 0.44/1.02 SPASS V 2.2.22 in combination with yices. % 0.44/1.02 SPASS beiseite: Proof found by SPASS. % 0.44/1.02 Problem: /tmp/SPASST_28239_n018.cluster.edu % 0.44/1.02 SPASS derived 47 clauses, backtracked 7 clauses and kept 74 clauses. % 0.44/1.02 SPASS backtracked 2 times (0 times due to theory inconsistency). % 0.44/1.02 SPASS allocated 6292 KBytes. % 0.44/1.02 SPASS spent 0:00:00.02 on the problem. % 0.44/1.02 0:00:00.00 for the input. % 0.44/1.02 0:00:00.00 for the FLOTTER CNF translation. % 0.44/1.02 0:00:00.00 for inferences. % 0.44/1.02 0:00:00.00 for the backtracking. % 0.44/1.02 0:00:00.01 for the reduction. % 0.44/1.02 0:00:00.00 for interacting with the SMT procedure. % 0.44/1.02 % 0.44/1.02 % 0.44/1.02 % SZS output start CNFRefutation for /tmp/SPASST_28239_n018.cluster.edu % 0.44/1.02 % 0.44/1.02 % Here is a proof with depth 4, length 31 : % 0.44/1.02 3[0:Inp] || -> array(skc5)*. % 0.44/1.02 4[0:Inp] || array(U) -> array(write(U,V,W))*. % 0.44/1.02 5[0:Inp] || equal(read(skc5,skc7),read(skc5,skc6))** -> . % 0.44/1.02 6[0:Inp] || array(U) -> equal(read(write(U,V,W),V),W)**. % 0.44/1.02 8[0:Inp] || array(U) -> equal(V,W) equal(read(write(U,V,X),W),read(U,W))**. % 0.44/1.02 9[0:Inp] || -> equal(read(write(write(write(skc5,skc6,0),skc8,plus(read(skc5,skc8),1)),skc7,0),U),read(skc5,U))**. % 0.44/1.02 12[0:ThA] || -> equal(plus(uminus(U),plus(U,V)),V)**. % 0.44/1.02 16[0:ThA] || -> equal(plus(uminus(U),U),0)**. % 0.44/1.02 42[0:Res:3.0,6.0] || -> equal(read(write(skc5,U,V),U),V)**. % 0.44/1.02 43[0:Res:3.0,4.0] || -> array(write(skc5,U,V))*. % 0.44/1.02 69[0:SpR:9.0,6.1] || array(write(write(skc5,skc6,0),skc8,plus(read(skc5,skc8),1)))* -> equal(read(skc5,skc7),0). % 0.44/1.02 70[0:SpR:9.0,8.2] || array(write(write(skc5,skc6,0),skc8,plus(read(skc5,skc8),1))) -> equal(skc7,U) equal(read(write(write(skc5,skc6,0),skc8,plus(read(skc5,skc8),1)),U),read(skc5,U))**. % 0.44/1.02 71[0:Res:4.1,69.0] || array(write(skc5,skc6,0))* -> equal(read(skc5,skc7),0). % 0.44/1.02 72(e)[0:MRR:71.0,43.0] || -> equal(read(skc5,skc7),0)**. % 0.44/1.02 73[0:Rew:72.0,5.0] || equal(read(skc5,skc6),0)** -> . % 0.44/1.02 77[0:SpR:70.2,6.1] || array(write(write(skc5,skc6,0),skc8,plus(read(skc5,skc8),1)))* array(write(skc5,skc6,0)) -> equal(skc8,skc7) equal(plus(read(skc5,skc8),1),read(skc5,skc8)). % 0.44/1.02 78[0:SpR:70.2,8.2] || array(write(write(skc5,skc6,0),skc8,plus(read(skc5,skc8),1)))* array(write(skc5,skc6,0)) -> equal(skc7,U) equal(skc8,U) equal(read(write(skc5,skc6,0),U),read(skc5,U))**. % 0.44/1.02 79(e)[0:MRR:77.0,77.1,4.1,43.0] || -> equal(skc8,skc7) equal(plus(read(skc5,skc8),1),read(skc5,skc8))**. % 0.44/1.02 80(e)[0:MRR:78.0,78.1,4.1,43.0] || -> equal(skc7,U) equal(skc8,U) equal(read(write(skc5,skc6,0),U),read(skc5,U))**. % 0.44/1.02 81[1:Spt:79.0] || -> equal(skc8,skc7)**. % 0.44/1.02 85[1:Rew:81.0,80.1] || -> equal(skc7,U) equal(skc7,U) equal(read(write(skc5,skc6,0),U),read(skc5,U))**. % 0.44/1.02 87[1:Obv:85.0] || -> equal(skc7,U) equal(read(write(skc5,skc6,0),U),read(skc5,U))**. % 0.44/1.02 93[1:SpR:87.1,42.0] || -> equal(skc7,skc6) equal(read(skc5,skc6),0)**. % 0.44/1.02 98(e)[1:MRR:93.1,73.0] || -> equal(skc7,skc6)**. % 0.44/1.02 99[1:Rew:98.0,72.0] || -> equal(read(skc5,skc6),0)**. % 0.44/1.02 105(e)[1:MRR:99.0,73.0] || -> . % 0.44/1.02 107(e)[1:Spt:105.0,79.0,81.0] || equal(skc8,skc7)** -> . % 0.44/1.02 108[1:Spt:105.0,79.1] || -> equal(plus(read(skc5,skc8),1),read(skc5,skc8))**. % 0.44/1.02 115[1:SpR:108.0,12.0] || -> equal(plus(uminus(read(skc5,skc8)),read(skc5,skc8)),1)**. % 0.44/1.02 121[1:Rew:16.0,115.0] || -> equal(1,0)**. % 0.44/1.02 122(e)[1:ArS:121.0] || -> . % 0.44/1.02 % 0.44/1.02 % SZS output end CNFRefutation for /tmp/SPASST_28239_n018.cluster.edu % 0.44/1.02 % 0.44/1.02 Formulae used in the proof : fof_array_type fof_co1 fof_write_type fof_ax2 % 0.44/1.04 % 0.44/1.04 SPASS+T ended %------------------------------------------------------------------------------