%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SYP116_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n022.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 : Tue May 5 07:15:06 PM UTC 2026 % Result : Unsatisfiable 0.88s 1.13s % Output : CNFRefutation 0.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP116_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.13 % Command : spasst-tptp-script %s %d % 0.16/0.34 % Computer : n022.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 17:50:21 EDT 2026 % 0.16/0.34 % CPUTime : % 0.20/0.47 % Using integer theory % 0.88/1.13 % 0.88/1.13 % 0.88/1.13 % SZS status Theorem for /tmp/SPASST_29820_n022.cluster.edu % 0.88/1.13 % 0.88/1.13 SPASS V 2.2.22 in combination with yices. % 0.88/1.13 SPASS beiseite: Proof found by SPASS. % 0.88/1.13 Problem: /tmp/SPASST_29820_n022.cluster.edu % 0.88/1.13 SPASS derived 18 clauses, backtracked 5 clauses and kept 51 clauses. % 0.88/1.13 SPASS backtracked 2 times (0 times due to theory inconsistency). % 0.88/1.13 SPASS allocated 6221 KBytes. % 0.88/1.13 SPASS spent 0:00:00.01 on the problem. % 0.88/1.13 0:00:00.00 for the input. % 0.88/1.13 0:00:00.00 for the FLOTTER CNF translation. % 0.88/1.13 0:00:00.00 for inferences. % 0.88/1.13 0:00:00.00 for the backtracking. % 0.88/1.13 0:00:00.00 for the reduction. % 0.88/1.13 0:00:00.00 for interacting with the SMT procedure. % 0.88/1.13 % 0.88/1.13 % 0.88/1.13 % SZS output start CNFRefutation for /tmp/SPASST_29820_n022.cluster.edu % 0.88/1.13 % 0.88/1.13 % Here is a proof with depth 1, length 20 : % 0.88/1.13 3[0:Inp] || -> r(U)*. % 0.88/1.13 4[0:Inp] || r(U)* -> equal(npb,npa). % 0.88/1.13 5[0:Inp] || less(npb,0)* -> q(npb). % 0.88/1.13 6[0:Inp] || greatereq(npb,0) -> p(npb)*. % 0.88/1.13 7[0:Inp] || q(npa) less(npa,0)* -> . % 0.88/1.13 8[0:Inp] || p(npa)* greatereq(npa,0) -> . % 0.88/1.13 40[0:ArS:6.0] || lesseq(0,npb)* -> p(npb). % 0.88/1.13 41[0:TOC:40.0] || -> less(npb,0)* p(npb). % 0.88/1.13 42[0:TOC:5.0] || -> lesseq(0,npb)* q(npb). % 0.88/1.13 43[0:MRR:4.0,3.0] || -> equal(npb,npa)**. % 0.88/1.13 44[0:Rew:43.0,41.0] || -> less(npa,0)* p(npb). % 0.88/1.13 45[0:Rew:43.0,42.0] || -> lesseq(0,npa)* q(npb). % 0.88/1.13 46[0:Rew:43.0,44.1] || -> less(npa,0)* p(npa). % 0.88/1.13 47[0:Rew:43.0,45.1] || -> lesseq(0,npa)* q(npa). % 0.88/1.13 48[0:ArS:8.1] || p(npa) lesseq(0,npa)* -> . % 0.88/1.13 49[0:TOC:48.1] || p(npa) -> less(npa,0)*. % 0.88/1.13 50[0:MRR:49.0,46.1] || -> less(npa,0)*. % 0.88/1.13 51[0:TOC:7.1] || q(npa) -> lesseq(0,npa)*. % 0.88/1.13 52[0:MRR:51.0,47.1] || -> lesseq(0,npa)*. % 0.88/1.13 70(e)[0:OCE:50.0,52.0] || -> . % 0.88/1.13 % 0.88/1.13 % SZS output end CNFRefutation for /tmp/SPASST_29820_n022.cluster.edu % 0.88/1.13 % 0.88/1.13 Formulae used in the proof : fof_type_npa fof_ax6 fof_ax5 fof_ax4 fof_ax2 fof_ax3 % 0.88/1.15 % 0.88/1.15 SPASS+T ended %------------------------------------------------------------------------------