%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n025.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 : Sun Apr 6 10:09:28 AM UTC 2025 % Result : Theorem 262.24s 141.74s % Output : Refutation 262.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0. % 0.06/0.13 % Command : spasst-tptp-script %s %d % 0.12/0.33 % Computer : n025.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Apr 6 02:57:05 EDT 2025 % 0.12/0.34 % CPUTime : % 0.20/0.47 % Using integer theory % 262.24/141.74 % 262.24/141.74 % 262.24/141.74 % SZS status Theorem for /tmp/SPASST_23432_n025.cluster.edu % 262.24/141.74 % 262.24/141.74 SPASS V 2.2.22 in combination with yices. % 262.24/141.74 SPASS beiseite: Proof found by SPASS and SMT. % 262.24/141.74 Problem: /tmp/SPASST_23432_n025.cluster.edu % 262.24/141.74 SPASS derived 60379 clauses, backtracked 3619 clauses and kept 30114 clauses. % 262.24/141.74 SPASS backtracked 6 times (2 times due to theory inconsistency). % 262.24/141.74 SPASS allocated 101432 KBytes. % 262.24/141.74 SPASS spent 0:02:20.51 on the problem. % 262.24/141.74 0:00:00.00 for the input. % 262.24/141.74 0:00:00.08 for the FLOTTER CNF translation. % 262.24/141.74 0:00:01.97 for inferences. % 262.24/141.74 0:00:06.61 for the backtracking. % 262.24/141.74 0:02:00.15 for the reduction. % 262.24/141.74 0:00:01.38 for interacting with the SMT procedure. % 262.24/141.74 % 262.24/141.74 % 262.24/141.74 % SZS output start CNFRefutation for /tmp/SPASST_23432_n025.cluster.edu % 262.24/141.74 % 262.24/141.74 % Here is a proof with depth 5, length 57 : % 262.24/141.74 16[0:Inp] || -> general(f__integer__(U))*. % 262.24/141.74 17[0:Inp] || -> greatereq(skc4,0)*. % 262.24/141.74 26[0:Inp] || -> sqrt(f__integer__(skc5),f__integer__(skc4))*. % 262.24/141.74 30[0:Inp] || sqrt(f__integer__(U),f__integer__(plus(skc4,1)))* -> . % 262.24/141.74 31[0:Inp] || sqrt(f__integer__(U),f__integer__(V))* -> greatereq(U,0). % 262.24/141.74 35[0:Inp] || p__less_equal__(f__integer__(U),f__integer__(V))* -> lesseq(U,V). % 262.24/141.74 45[0:Inp] || sqrt(f__integer__(U),f__integer__(V))*+ -> lesseq(times(U,U),V)*. % 262.24/141.74 65[0:Inp] || general(U)+ general(V) -> p__less_equal__(U,V)* p__less_equal__(V,U)*. % 262.24/141.74 88[0:Inp] || greatereq(U,0) less(V,times(plus(U,1),plus(U,1)))* lesseq(times(U,U),V) -> sqrt(f__integer__(U),f__integer__(V))*. % 262.24/141.74 89[0:Inp] || equal(U,plus(V,1))* equal(W,plus(X,1))* lesseq(times(plus(X,1),plus(X,1)),plus(V,1))* sqrt(f__integer__(X),f__integer__(V))* -> sqrt(f__integer__(W),f__integer__(U))*. % 262.24/141.74 105[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 262.24/141.74 124[0:ArS:17.0] || -> lesseq(0,skc4)*. % 262.24/141.74 127[0:ArS:31.1] || sqrt(f__integer__(U),f__integer__(V))* -> lesseq(0,U). % 262.24/141.74 129[0:ArS:88.0] || lesseq(0,U) less(V,times(plus(U,1),plus(U,1)))* lesseq(times(U,U),V) -> sqrt(f__integer__(U),f__integer__(V))*. % 262.24/141.74 130[0:TOC:129.1] || -> less(U,0) less(V,times(U,U)) sqrt(f__integer__(U),f__integer__(V))* lesseq(times(plus(U,1),plus(U,1)),V)*. % 262.24/141.74 131[0:TOC:89.2] || equal(U,plus(V,1))*+ equal(W,plus(X,1))* sqrt(f__integer__(V),f__integer__(X))* -> sqrt(f__integer__(U),f__integer__(W))* less(plus(X,1),times(plus(V,1),plus(V,1)))*. % 262.24/141.74 138[0:Res:26.0,127.0] || -> lesseq(0,skc5)*. % 262.24/141.74 140[0:Res:130.3,30.0] || -> less(U,0) less(plus(skc4,1),times(U,U)) lesseq(times(plus(U,1),plus(U,1)),plus(skc4,1))*. % 262.24/141.74 141[0:Res:131.4,30.0] || equal(plus(skc4,1),plus(U,1)) equal(V,plus(W,1))* sqrt(f__integer__(W),f__integer__(U))* -> less(plus(U,1),times(plus(W,1),plus(W,1)))*. % 262.24/141.74 142[0:AED:141.1] || sqrt(f__integer__(U),f__integer__(V))* equal(plus(skc4,1),plus(V,1))+ -> less(plus(V,1),times(plus(U,1),plus(U,1)))*. % 262.24/141.74 143[0:Res:26.0,142.1] || equal(plus(skc4,1),plus(skc4,1)) -> less(plus(skc4,1),times(plus(skc5,1),plus(skc5,1)))*. % 262.24/141.74 145[0:Obv:143.0] || -> less(plus(skc4,1),times(plus(skc5,1),plus(skc5,1)))*. % 262.24/141.74 148(e)[0:OCE:124.0,105.1] || -> equal(skc4,0) less(0,skc4)*. % 262.24/141.74 150[1:Spt:148.0] || -> equal(skc4,0)**. % 262.24/141.74 153[1:Rew:150.0,145.0] || -> less(plus(0,1),times(plus(skc5,1),plus(skc5,1)))*. % 262.24/141.74 154[1:Rew:150.0,140.1] || -> less(U,0) less(plus(0,1),times(U,U)) lesseq(times(plus(U,1),plus(U,1)),plus(skc4,1))*. % 262.24/141.74 156[1:Rew:150.0,26.0] || -> sqrt(f__integer__(skc5),f__integer__(0))*. % 262.24/141.74 161[1:ArS:153.0] || -> less(1,times(plus(skc5,1),plus(skc5,1)))*. % 262.24/141.74 162[1:ArS:154.1] || -> less(U,0) less(1,times(U,U)) lesseq(times(plus(U,1),plus(U,1)),plus(skc4,1))*. % 262.24/141.74 163[1:Rew:150.0,162.2] || -> less(U,0) less(1,times(U,U)) lesseq(times(plus(U,1),plus(U,1)),plus(0,1))*. % 262.24/141.74 164[1:ArS:163.2] || -> less(U,0) less(1,times(U,U)) lesseq(times(plus(U,1),plus(U,1)),1)*. % 262.24/141.74 170(e)[0:OCE:138.0,105.1] || -> equal(skc5,0) less(0,skc5)*. % 262.24/141.74 172(e)[2:Spt:170.0] || -> equal(skc5,0)**. % 262.24/141.74 177[2:Rew:172.0,161.0] || -> less(1,times(plus(0,1),plus(0,1)))*. % 262.24/141.74 181(e)[2:ArS:177.0] || -> . % 262.24/141.74 182[2:Spt:181.0,170.0,172.0] || equal(skc5,0)** -> . % 262.24/141.74 183[2:Spt:181.0,170.1] || -> less(0,skc5)*. % 262.24/141.74 840[1:Res:156.0,45.0] || -> lesseq(times(skc5,skc5),0)*. % 262.24/141.74 1317[0:Res:16.0,65.0] || general(U)+ -> p__less_equal__(f__integer__(V),U)* p__less_equal__(U,f__integer__(V))*. % 262.24/141.74 2605[0:Res:16.0,1317.0] || -> p__less_equal__(f__integer__(U),f__integer__(V))* p__less_equal__(f__integer__(V),f__integer__(U))*. % 262.24/141.74 2655[0:Res:2605.0,35.0] || -> p__less_equal__(f__integer__(U),f__integer__(V))* lesseq(V,U). % 262.24/141.74 2768[0:Res:2655.0,35.0] || -> lesseq(U,V)* lesseq(V,U)*. % 262.24/141.74 2787[2:OCE:2768.0,183.0] || -> lesseq(0,skc5)*. % 262.24/141.74 12181[1:OCh:164.2,161.0] || -> less(skc5,0) less(1,times(skc5,skc5))* less(1,1). % 262.24/141.74 18358[2:ThR:12181,2787,840] || -> . % 262.24/141.74 18359[1:Spt:18358.0,148.0,150.0] || equal(skc4,0)** -> . % 262.24/141.74 18360[1:Spt:18358.0,148.1] || -> less(0,skc4)*. % 262.24/141.74 18373[2:Spt:170.0] || -> equal(skc5,0)**. % 262.24/141.74 18378[2:Rew:18373.0,145.0] || -> less(plus(skc4,1),times(plus(0,1),plus(0,1)))*. % 262.24/141.74 18382[2:ArS:18378.0] || -> less(skc4,0)*. % 262.24/141.74 18433(e)[2:OCE:18382.0,18360.0] || -> . % 262.24/141.74 18440[2:Spt:18433.0,170.0,18373.0] || equal(skc5,0)** -> . % 262.24/141.74 18441[2:Spt:18433.0,170.1] || -> less(0,skc5)*. % 262.24/141.74 18444[2:OCE:18441.0,2768.0] || -> lesseq(0,skc5)*. % 262.24/141.74 64761[0:Res:26.0,45.0] || -> lesseq(times(skc5,skc5),skc4)*. % 262.24/141.74 76119[0:OCh:145.0,140.2] || -> less(skc5,0) less(plus(skc4,1),times(skc5,skc5))* less(plus(skc4,1),plus(skc4,1)). % 262.24/141.74 88108[2:ThR:18444,76119,64761] || -> . % 262.24/141.74 % 262.24/141.74 % SZS output end CNFRefutation for /tmp/SPASST_23432_n025.cluster.edu % 262.24/141.74 % 262.24/141.74 Formulae used in the proof : fof_p__is_symbolic__def_ax fof_symbol_type fof_f__integer___decl fof_formula_3_completed_definition_of_composite_1 fof_sup_type fof_numerals_less_than_symbols_ax fof_formula_7_inductive_step fof_formula_2_completed_definition_of_sqrtb_1 fof_p__is_integer__def_ax fof_formula_1_completed_definition_of_composite_1 fof_formula_4_completed_definition_of_prime_1 fof_formula_5_unnamed_formula % 282.51/162.02 % 282.51/162.02 SPASS+T ended %------------------------------------------------------------------------------