%------------------------------------------------------------------------------ % 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 : n011.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:27 AM UTC 2025 % Result : Theorem 27.23s 14.89s % Output : Refutation 27.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0. % 0.12/0.13 % Command : spasst-tptp-script %s %d % 0.14/0.34 % Computer : n011.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Sun Apr 6 03:05:18 EDT 2025 % 0.14/0.35 % CPUTime : % 0.21/0.48 % Using integer theory % 27.23/14.89 % 27.23/14.89 % 27.23/14.89 % SZS status Theorem for /tmp/SPASST_15951_n011.cluster.edu % 27.23/14.89 % 27.23/14.89 SPASS V 2.2.22 in combination with yices. % 27.23/14.89 SPASS beiseite: Proof found by SPASS and SMT. % 27.23/14.89 Problem: /tmp/SPASST_15951_n011.cluster.edu % 27.23/14.89 SPASS derived 22267 clauses, backtracked 339 clauses and kept 7052 clauses. % 27.23/14.89 SPASS backtracked 6 times (4 times due to theory inconsistency). % 27.23/14.89 SPASS allocated 32153 KBytes. % 27.23/14.89 SPASS spent 0:00:13.76 on the problem. % 27.23/14.89 0:00:00.00 for the input. % 27.23/14.89 0:00:00.02 for the FLOTTER CNF translation. % 27.23/14.89 0:00:00.49 for inferences. % 27.23/14.89 0:00:00.70 for the backtracking. % 27.23/14.89 0:00:10.98 for the reduction. % 27.23/14.89 0:00:00.36 for interacting with the SMT procedure. % 27.23/14.89 % 27.23/14.89 % 27.23/14.89 % SZS output start CNFRefutation for /tmp/SPASST_15951_n011.cluster.edu % 27.23/14.89 % 27.23/14.89 % Here is a proof with depth 4, length 45 : % 27.23/14.89 6[0:Inp] || -> general(f__integer__(U))*. % 27.23/14.89 8[0:Inp] || -> greater(skc6,0)*. % 27.23/14.89 14[0:Inp] || lesseq(U,V) -> p__less_equal__(f__integer__(U),f__integer__(V))*. % 27.23/14.89 16[0:Inp] || equal(U,V) -> equal(f__integer__(U),f__integer__(V))*. % 27.23/14.89 21[0:Inp] || div_p(f__integer__(plus(skc7,1)),f__integer__(skc6),f__integer__(U),f__integer__(V))* -> . % 27.23/14.89 23[0:Inp] || general(U) general(V) p__greater_equal__(U,V) -> p__less_equal__(V,U)*. % 27.23/14.89 24[0:Inp] || general(U) general(V) p__less_equal__(V,U)* -> p__greater_equal__(U,V). % 27.23/14.89 25[0:Inp] || general(U) general(V) p__less__(U,V) -> p__less_equal__(U,V)*. % 27.23/14.89 28[0:Inp] || greater(skc6,0) -> div_p(f__integer__(skc7),f__integer__(skc6),f__integer__(skc9),f__integer__(skc8))*. % 27.23/14.89 30[0:Inp] || general(U) general(V) p__less__(U,V)* equal(U,V) -> . % 27.23/14.89 35[0:Inp] || general(U) general(V) p__less_equal__(U,V)*+ p__less_equal__(V,U)* -> equal(U,V). % 27.23/14.89 38[0:Inp] || general(U) general(V) general(W) general(X) div_p(U,V,W,X)* -> p__less__(X,V). % 27.23/14.89 40[0:Inp] || equal(U,plus(V,1))* equal(W,plus(X,1))* equal(Y,minus(Z,1)) div_p(f__integer__(X),f__integer__(Z),f__integer__(V),f__integer__(Y))* -> div_p(f__integer__(W),f__integer__(Z),f__integer__(U),f__integer__(0))*. % 27.23/14.89 44[0:Inp] || equal(U,plus(V,1))* equal(W,plus(X,1))* less(V,minus(Y,1)) div_p(f__integer__(X),f__integer__(Y),f__integer__(Z),f__integer__(V))* -> div_p(f__integer__(W),f__integer__(Y),f__integer__(Z),f__integer__(U))*. % 27.23/14.89 79[0:ArS:8.0] || -> less(0,skc6)*. % 27.23/14.89 81[0:TOC:14.0] || -> less(U,V) p__less_equal__(f__integer__(V),f__integer__(U))*. % 27.23/14.89 82[0:ArS:28.0] || less(0,skc6) -> div_p(f__integer__(skc7),f__integer__(skc6),f__integer__(skc9),f__integer__(skc8))*. % 27.23/14.89 83(e)[0:TOC:82.0] || -> lesseq(skc6,0) div_p(f__integer__(skc7),f__integer__(skc6),f__integer__(skc9),f__integer__(skc8))*. % 27.23/14.89 84[0:ArS:40.2] || equal(U,plus(V,-1)) equal(W,plus(X,1))* equal(Y,plus(Z,1))* div_p(f__integer__(X),f__integer__(V),f__integer__(Z),f__integer__(U))*+ -> div_p(f__integer__(W),f__integer__(V),f__integer__(Y),f__integer__(0))*. % 27.23/14.89 85[0:ArS:44.2] || equal(U,plus(V,1))* equal(W,plus(X,1))* less(V,plus(Y,-1)) div_p(f__integer__(X),f__integer__(Y),f__integer__(Z),f__integer__(V))* -> div_p(f__integer__(W),f__integer__(Y),f__integer__(Z),f__integer__(U))*. % 27.23/14.89 86[0:TOC:85.2] || equal(U,plus(V,1))* equal(W,plus(X,1))* div_p(f__integer__(V),f__integer__(Y),f__integer__(Z),f__integer__(X))*+ -> lesseq(plus(Y,-1),X) div_p(f__integer__(U),f__integer__(Y),f__integer__(Z),f__integer__(W))*. % 27.23/14.89 88[0:Res:84.4,21.0] || equal(U,plus(V,1))* equal(plus(skc7,1),plus(W,1)) equal(X,plus(skc6,-1)) div_p(f__integer__(W),f__integer__(skc6),f__integer__(V),f__integer__(X))* -> . % 27.23/14.89 89[0:Res:86.4,21.0] || equal(U,plus(V,1))* equal(plus(skc7,1),plus(W,1)) div_p(f__integer__(W),f__integer__(skc6),f__integer__(X),f__integer__(V))* -> lesseq(plus(skc6,-1),V). % 27.23/14.89 91[0:AED:89.0] || equal(plus(skc7,1),plus(U,1)) div_p(f__integer__(U),f__integer__(skc6),f__integer__(V),f__integer__(W))* -> lesseq(plus(skc6,-1),W). % 27.23/14.89 92[0:AED:88.0] || equal(U,plus(skc6,-1)) equal(plus(skc7,1),plus(V,1)) div_p(f__integer__(V),f__integer__(skc6),f__integer__(W),f__integer__(U))* -> . % 27.23/14.89 94[1:Spt:83.0] || -> lesseq(skc6,0)*. % 27.23/14.89 97(e)[1:OCE:79.0,94.0] || -> . % 27.23/14.89 100[1:Spt:97.0,83.0,94.0] || lesseq(skc6,0)* -> . % 27.23/14.89 101[1:Spt:97.0,83.1] || -> div_p(f__integer__(skc7),f__integer__(skc6),f__integer__(skc9),f__integer__(skc8))*. % 27.23/14.89 249[0:Res:81.1,24.2] || general(f__integer__(U)) general(f__integer__(V)) -> less(U,V) p__greater_equal__(f__integer__(U),f__integer__(V))*. % 27.23/14.89 266[0:MRR:249.0,249.1,6.0,6.0] || -> less(U,V) p__greater_equal__(f__integer__(U),f__integer__(V))*. % 27.23/14.89 698[0:Res:25.3,35.2] || general(U) general(V) p__less__(U,V) general(U) general(V) p__less_equal__(V,U)* -> equal(U,V). % 27.23/14.89 710[0:Obv:698.1] || p__less__(U,V) general(U) general(V) p__less_equal__(V,U)* -> equal(U,V). % 27.23/14.89 711[0:MRR:710.4,30.3] || p__less__(U,V) general(U) general(V) p__less_equal__(V,U)* -> . % 27.23/14.89 2790[0:Res:23.3,711.3] || general(U) general(V) p__greater_equal__(U,V) p__less__(U,V)* general(U) general(V) -> . % 27.23/14.89 2805[0:Obv:2790.1] || p__greater_equal__(U,V) p__less__(U,V)* general(U) general(V) -> . % 27.23/14.89 16627[1:SpR:16.1,101.0] || equal(skc6,U) -> div_p(f__integer__(skc7),f__integer__(U),f__integer__(skc9),f__integer__(skc8))*. % 27.23/14.89 16657[1:Res:101.0,38.4] || general(f__integer__(skc7)) general(f__integer__(skc6)) general(f__integer__(skc9)) general(f__integer__(skc8)) -> p__less__(f__integer__(skc8),f__integer__(skc6))*. % 27.23/14.89 16660[1:MRR:16657.0,16657.1,16657.2,16657.3,6.0,6.0,6.0,6.0] || -> p__less__(f__integer__(skc8),f__integer__(skc6))*. % 27.23/14.89 16692[1:Res:16660.0,2805.1] || p__greater_equal__(f__integer__(skc8),f__integer__(skc6))* general(f__integer__(skc8)) general(f__integer__(skc6)) -> . % 27.23/14.89 16708[1:MRR:16692.1,16692.2,6.0,6.0] || p__greater_equal__(f__integer__(skc8),f__integer__(skc6))* -> . % 27.23/14.89 25349[1:Res:266.1,16708.0] || -> less(skc8,skc6)*. % 27.23/14.89 26932[1:Res:16627.1,91.1] || equal(skc6,skc6) equal(plus(skc7,1),plus(skc7,1)) -> lesseq(plus(skc6,-1),skc8)*. % 27.23/14.89 26934[1:Res:16627.1,92.2] || equal(skc6,skc6) equal(plus(skc6,-1),skc8)** equal(plus(skc7,1),plus(skc7,1)) -> . % 27.23/14.89 31939[1:ThR:26932,26934,25349] || -> . % 27.23/14.89 % 27.23/14.89 % SZS output end CNFRefutation for /tmp/SPASST_15951_n011.cluster.edu % 27.23/14.89 % 27.23/14.89 Formulae used in the proof : fof_p__is_symbolic__def_ax fof_symbol_type fof_formula_3_inductive_step fof_numeral_ordering_ax fof_f__integer__def_ax fof_strongly_connected_ordering_ax fof_p__greater__def_ax fof_p__greater_equal__def_ax fof_p__less__def_ax fof_formula_0_completed_definition_of_div_4 % 27.86/15.56 % 27.86/15.56 SPASS+T ended %------------------------------------------------------------------------------