%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW616_2 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n020.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 01:30:33 EDT 2022 % Result : Theorem 12.91s 7.66s % Output : Refutation 12.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWW616_2 : TPTP v8.1.0. Released v6.1.0. % 0.11/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 4 09:46:22 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.47 % Using integer theory % 12.91/7.66 % 12.91/7.66 % 12.91/7.66 % SZS status Theorem for /tmp/SPASST_9440_n020.cluster.edu % 12.91/7.66 % 12.91/7.66 SPASS V 2.2.22 in combination with yices. % 12.91/7.66 SPASS beiseite: Proof found by SPASS and SMT. % 12.91/7.66 Problem: /tmp/SPASST_9440_n020.cluster.edu % 12.91/7.66 SPASS derived 39086 clauses, backtracked 21779 clauses and kept 33479 clauses. % 12.91/7.66 SPASS backtracked 200 times (2 times due to theory inconsistency). % 12.91/7.66 SPASS allocated 34402 KBytes. % 12.91/7.66 SPASS spent 0:00:06.32 on the problem. % 12.91/7.66 0:00:00.00 for the input. % 12.91/7.66 0:00:00.02 for the FLOTTER CNF translation. % 12.91/7.66 0:00:00.15 for inferences. % 12.91/7.66 0:00:00.55 for the backtracking. % 12.91/7.66 0:00:04.62 for the reduction. % 12.91/7.66 0:00:00.86 for interacting with the SMT procedure. % 12.91/7.66 % 12.91/7.66 % 12.91/7.66 % SZS output start CNFRefutation for /tmp/SPASST_9440_n020.cluster.edu % 12.91/7.66 % 12.91/7.66 % Here is a proof with depth 1, length 28 : % 12.91/7.66 25[0:Inp] || -> lesseq(skc16,skc22)*. % 12.91/7.66 64[0:Inp] || -> lesseq(skc22,plus(skc16,div_f(minus(skc15,skc16),2)))*. % 12.91/7.66 65[0:Inp] || -> equal(plus(skc16,div_f(minus(skc15,skc16),2)),skc18)**. % 12.91/7.66 67[0:Inp] || -> lesseq(skc21,plus(skc16,div_f(minus(skc15,skc16),2)))*. % 12.91/7.66 68[0:Inp] || -> lesseq(plus(skc16,div_f(minus(skc15,skc16),2)),skc21)*. % 12.91/7.66 69[0:Inp] || -> equal(plus(skc16,div_f(minus(skc15,skc16),2)),skc19)**. % 12.91/7.66 75[0:Inp] || lesseq(sum_f(skc17,skc22,skc21),sum_f(skc17,skc20,skc19))* -> . % 12.91/7.66 134[0:Inp] || lesseq(U,plus(skc16,div_f(minus(skc15,skc16),2))) less(minus(skc16,1),U) -> lesseq(sum_f(skc17,U,plus(skc16,div_f(minus(skc15,skc16),2))),sum_f(skc17,skc20,skc19))*. % 12.91/7.66 152[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 12.91/7.66 173[0:ArS:69.0] || -> equal(plus(skc16,div_f(plus(skc15,uminus(skc16)),2)),skc19)**. % 12.91/7.66 174[0:ArS:68.0] || -> lesseq(plus(skc16,div_f(plus(skc15,uminus(skc16)),2)),skc21)*. % 12.91/7.66 175[0:Rew:173.0,174.0] || -> lesseq(skc19,skc21)*. % 12.91/7.66 176[0:ArS:67.0] || -> lesseq(skc21,plus(skc16,div_f(plus(skc15,uminus(skc16)),2)))*. % 12.91/7.66 177[0:Rew:173.0,176.0] || -> lesseq(skc21,skc19)*. % 12.91/7.66 180[0:ArS:65.0] || -> equal(plus(skc16,div_f(plus(skc15,uminus(skc16)),2)),skc18)**. % 12.91/7.66 181[0:Rew:173.0,180.0] || -> equal(skc19,skc18)**. % 12.91/7.66 182[0:Rew:181.0,173.0] || -> equal(plus(skc16,div_f(plus(skc15,uminus(skc16)),2)),skc18)**. % 12.91/7.66 183[0:Rew:181.0,175.0] || -> lesseq(skc18,skc21)*. % 12.91/7.66 184[0:Rew:181.0,177.0] || -> lesseq(skc21,skc18)*. % 12.91/7.66 186[0:ArS:64.0] || -> lesseq(skc22,plus(skc16,div_f(plus(skc15,uminus(skc16)),2)))*. % 12.91/7.66 188[0:TOC:75.0] || -> less(sum_f(skc17,skc20,skc19),sum_f(skc17,skc22,skc21))*. % 12.91/7.66 189[0:Rew:181.0,188.0] || -> less(sum_f(skc17,skc20,skc18),sum_f(skc17,skc22,skc21))*. % 12.91/7.66 190[0:Rew:182.0,186.0] || -> lesseq(skc22,skc18)*. % 12.91/7.66 213[0:ArS:134.2] || lesseq(U,plus(skc16,div_f(plus(skc15,uminus(skc16)),2))) less(plus(skc16,-1),U) -> lesseq(sum_f(skc17,U,plus(skc16,div_f(plus(skc15,uminus(skc16)),2))),sum_f(skc17,skc20,skc19))*. % 12.91/7.66 214[0:TOC:213.1] || -> lesseq(U,plus(skc16,-1)) less(plus(skc16,div_f(plus(skc15,uminus(skc16)),2)),U) lesseq(sum_f(skc17,U,plus(skc16,div_f(plus(skc15,uminus(skc16)),2))),sum_f(skc17,skc20,skc19))*. % 12.91/7.66 215(e)[0:Rew:182.0,214.2,181.0,214.2,182.0,214.1] || -> lesseq(U,plus(skc16,-1)) less(skc18,U) lesseq(sum_f(skc17,U,skc18),sum_f(skc17,skc20,skc18))*. % 12.91/7.66 271[0:OCE:183.0,152.2] || -> equal(skc21,skc18) less(skc18,skc21)*. % 12.91/7.66 75251(e)[0:ThR:190,189,184,215,25,271] || -> . % 12.91/7.66 % 12.91/7.66 % SZS output end CNFRefutation for /tmp/SPASST_9440_n020.cluster.edu % 12.91/7.66 % 12.91/7.66 Formulae used in the proof : fof_wP_parameter_maximum_subarray_rec fof_bool_inversion fof_mk_ref fof_sum_right_extension % 13.56/8.33 % 13.56/8.33 SPASS+T ended %------------------------------------------------------------------------------