%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n023.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:07:32 PM UTC 2026 % Result : Theorem 0.76s 1.07s % Output : CNFRefutation 0.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : spasst-tptp-script %s %d % 0.17/0.33 % Computer : n023.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Tue May 5 08:56:38 EDT 2026 % 0.17/0.34 % CPUTime : % 0.31/0.47 % Using integer theory % 0.76/1.07 % 0.76/1.07 % 0.76/1.07 % SZS status Theorem for /tmp/SPASST_27908_n023.cluster.edu % 0.76/1.07 % 0.76/1.07 SPASS V 2.2.22 in combination with yices. % 0.76/1.07 SPASS beiseite: Proof found by SPASS. % 0.76/1.07 Problem: /tmp/SPASST_27908_n023.cluster.edu % 0.76/1.07 SPASS derived 40 clauses, backtracked 0 clauses and kept 84 clauses. % 0.76/1.07 SPASS backtracked 0 times (0 times due to theory inconsistency). % 0.76/1.07 SPASS allocated 6294 KBytes. % 0.76/1.07 SPASS spent 0:00:00.02 on the problem. % 0.76/1.07 0:00:00.00 for the input. % 0.76/1.07 0:00:00.00 for the FLOTTER CNF translation. % 0.76/1.07 0:00:00.00 for inferences. % 0.76/1.07 0:00:00.00 for the backtracking. % 0.76/1.07 0:00:00.00 for the reduction. % 0.76/1.07 0:00:00.00 for interacting with the SMT procedure. % 0.76/1.07 % 0.76/1.07 % 0.76/1.07 % SZS output start CNFRefutation for /tmp/SPASST_27908_n023.cluster.edu % 0.76/1.07 % 0.76/1.07 % Here is a proof with depth 7, length 27 : % 0.76/1.07 1[0:Inp] || cr1w2(U,V)* -> . % 0.76/1.07 7[0:Inp] || sl1cr2(U,V)*+ -> sl1sl2(U,0)*. % 0.76/1.07 8[0:Inp] || equal(U,plus(V,1)) cr1sl2(V,W)* -> cr1w2(V,U)*. % 0.76/1.07 10[0:Inp] || sl1sl2(U,V)* equal(W,plus(V,1))+ -> w1sl2(W,V)*. % 0.76/1.07 13[0:Inp] || sl1sl2(U,V)* equal(W,plus(U,1))+ -> sl1w2(U,W)*. % 0.76/1.07 18[0:Inp] || w1sl2(U,V)* equal(V,0) -> cr1sl2(U,V). % 0.76/1.07 24[0:Inp] || sl1w2(U,V)* equal(U,0) -> sl1cr2(U,V). % 0.76/1.07 26[0:Inp] || greatereq(U,0) greatereq(V,0) -> sl1sl2(V,U)*. % 0.76/1.07 35[0:ThA] || -> equal(plus(0,U),U)**. % 0.76/1.07 58[0:ArS:26.1] || lesseq(0,U) lesseq(0,V) -> sl1sl2(V,U)*. % 0.76/1.07 59[0:TOC:58.1] || -> sl1sl2(U,V)* less(V,0) less(U,0). % 0.76/1.07 68[0:MRR:8.2,1.0] || cr1sl2(U,V)* equal(W,plus(U,1))*+ -> . % 0.76/1.07 69[0:EqR:68.1] || cr1sl2(U,V)* -> . % 0.76/1.07 75[0:MRR:18.2,69.0] || w1sl2(U,V)* equal(V,0) -> . % 0.76/1.07 83[0:EqR:13.1] || sl1sl2(U,V)*+ -> sl1w2(U,plus(U,1))*. % 0.76/1.07 89[0:Res:59.0,83.0] || -> less(U,0)* less(V,0) sl1w2(V,plus(V,1))*. % 0.76/1.07 90[0:BLD:89.0] || -> less(U,0) sl1w2(U,plus(U,1))*. % 0.76/1.07 91[0:SpR:35.0,90.1] || -> less(0,0) sl1w2(0,1)*. % 0.76/1.07 96[0:ArS:91.0] || -> sl1w2(0,1)*. % 0.76/1.07 99[0:Res:96.0,24.0] || equal(0,0) -> sl1cr2(0,1)*. % 0.76/1.07 102[0:ArS:99.0] || -> sl1cr2(0,1)*. % 0.76/1.07 103[0:EqR:10.1] || sl1sl2(U,V)*+ -> w1sl2(plus(V,1),V)*. % 0.76/1.07 109[0:Res:102.0,7.0] || -> sl1sl2(0,0)*. % 0.76/1.07 122[0:Res:109.0,103.0] || -> w1sl2(plus(0,1),0)*. % 0.76/1.07 123[0:ArS:122.0] || -> w1sl2(1,0)*. % 0.76/1.07 131[0:Res:123.0,75.0] || equal(0,0)* -> . % 0.76/1.07 134(e)[0:ArS:131.0] || -> . % 0.76/1.07 % 0.76/1.07 % SZS output end CNFRefutation for /tmp/SPASST_27908_n023.cluster.edu % 0.76/1.07 % 0.76/1.07 Formulae used in the proof : fof_ax8 fof_ax6 fof_ax12 fof_ax3 fof_ax13 fof_ax4 fof_ax2 % 0.76/1.09 % 0.76/1.09 SPASS+T ended %------------------------------------------------------------------------------