%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : PLA060_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n014.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 06:48:49 PM UTC 2026 % Result : Theorem 0.85s 1.16s % Output : CNFRefutation 0.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PLA060_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.13 % Command : spasst-tptp-script %s %d % 0.15/0.34 % Computer : n014.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue May 5 04:50:51 EDT 2026 % 0.15/0.34 % CPUTime : % 0.30/0.47 % Using integer theory % 0.85/1.16 % 0.85/1.16 % 0.85/1.16 % SZS status Theorem for /tmp/SPASST_4610_n014.cluster.edu % 0.85/1.16 % 0.85/1.16 SPASS V 2.2.22 in combination with yices. % 0.85/1.16 SPASS beiseite: Proof found by SPASS. % 0.85/1.16 Problem: /tmp/SPASST_4610_n014.cluster.edu % 0.85/1.16 SPASS derived 351 clauses, backtracked 0 clauses and kept 173 clauses. % 0.85/1.16 SPASS backtracked 1 times (0 times due to theory inconsistency). % 0.85/1.16 SPASS allocated 6545 KBytes. % 0.85/1.16 SPASS spent 0:00:00.05 on the problem. % 0.85/1.16 0:00:00.00 for the input. % 0.85/1.16 0:00:00.00 for the FLOTTER CNF translation. % 0.85/1.16 0:00:00.01 for inferences. % 0.85/1.16 0:00:00.00 for the backtracking. % 0.85/1.16 0:00:00.03 for the reduction. % 0.85/1.16 0:00:00.01 for interacting with the SMT procedure. % 0.85/1.16 % 0.85/1.16 % 0.85/1.16 % SZS output start CNFRefutation for /tmp/SPASST_4610_n014.cluster.edu % 0.85/1.16 % 0.85/1.16 % Here is a proof with depth 5, length 23 : % 0.85/1.16 1[0:Inp] || lesseq(U,200)* -> s0(U,V)*. % 0.85/1.16 2[0:Inp] || greatereq(U,240) s0(U,V)* -> . % 0.85/1.16 3[0:Inp] || lesseq(U,200)* s0(U,V) -> s3(U,V)*. % 0.85/1.16 5[0:Inp] || s4(U,V)* equal(W,plus(U,V))*+ -> s0(W,V)*. % 0.85/1.16 6[0:Inp] || greatereq(U,0) lesseq(U,40)* s3(V,W)* -> s4(V,U)*. % 0.85/1.16 10[0:ThA] || -> equal(plus(U,plus(uminus(U),V)),V)**. % 0.85/1.16 18[0:ThA] || -> lesseq(U,U)*. % 0.85/1.16 40[0:TOC:1.0] || -> s0(U,V)* less(200,U)*. % 0.85/1.16 41[0:ArS:2.0] || lesseq(240,U)* s0(U,V)* -> . % 0.85/1.16 42[0:TOC:41.0] || s0(U,V)*+ -> less(U,240)*. % 0.85/1.16 45[0:TOC:3.0] || s0(U,V) -> less(200,U)* s3(U,V)*. % 0.85/1.16 46[0:MRR:45.0,40.1] || -> s3(U,V)* less(200,U)*. % 0.85/1.16 49[0:ArS:6.0] || lesseq(0,U) lesseq(U,40)* s3(V,W)* -> s4(V,U)*. % 0.85/1.16 50[0:TOC:49.1] || s3(U,V)*+ -> s4(U,W)* less(W,0) less(40,W)*. % 0.85/1.16 56[0:OCE:46.1,18.0] || -> s3(200,U)*. % 0.85/1.16 166[0:Res:56.0,50.0] || -> s4(200,U)* less(U,0) less(40,U). % 0.85/1.16 184[0:EqR:5.1] || s4(U,V) -> s0(plus(U,V),V)*. % 0.85/1.16 207[0:Res:184.1,42.0] || s4(U,V) -> less(plus(U,V),240)*. % 0.85/1.16 229[0:SpR:10.0,207.1] || s4(U,plus(uminus(U),V))* -> less(V,240). % 0.85/1.16 514[0:Res:166.0,229.0] || -> less(plus(uminus(200),U),0) less(40,plus(uminus(200),U))* less(U,240). % 0.85/1.16 519[0:ArS:514.1] || -> less(U,200) less(240,U)* less(U,240)*. % 0.85/1.16 521[0:Fac:519.1,519.2] || -> less(240,200) less(240,240)*. % 0.85/1.16 562(e)[0:ArS:521.1] || -> . % 0.85/1.16 % 0.85/1.16 % SZS output end CNFRefutation for /tmp/SPASST_4610_n014.cluster.edu % 0.85/1.16 % 0.85/1.16 Formulae used in the proof : fof_conj1 fof_ax1 fof_ax6 % 0.85/1.18 % 0.85/1.18 SPASS+T ended %------------------------------------------------------------------------------