%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : ARI727_1 : TPTP v8.1.0. Released v6.3.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n028.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 : 600s % DateTime : Thu Jul 14 22:18:47 EDT 2022 % Result : Theorem 0.77s 1.05s % Output : Refutation 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ARI727_1 : TPTP v8.1.0. Released v6.3.0. % 0.13/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jun 17 12:31:27 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.48 % Using real theory % 0.77/1.05 % 0.77/1.05 % 0.77/1.05 % SZS status Theorem for /tmp/SPASST_18940_n028.cluster.edu % 0.77/1.05 % 0.77/1.05 SPASS V 2.2.22 in combination with yices. % 0.77/1.05 SPASS beiseite: Proof found by SPASS. % 0.77/1.05 Problem: /tmp/SPASST_18940_n028.cluster.edu % 0.77/1.05 SPASS derived 425 clauses, backtracked 63 clauses and kept 277 clauses. % 0.77/1.05 SPASS backtracked 7 times (0 times due to theory inconsistency). % 0.77/1.05 SPASS allocated 6488 KBytes. % 0.77/1.05 SPASS spent 0:00:00.04 on the problem. % 0.77/1.05 0:00:00.00 for the input. % 0.77/1.05 0:00:00.00 for the FLOTTER CNF translation. % 0.77/1.05 0:00:00.00 for inferences. % 0.77/1.05 0:00:00.00 for the backtracking. % 0.77/1.05 0:00:00.02 for the reduction. % 0.77/1.05 0:00:00.01 for interacting with the SMT procedure. % 0.77/1.05 % 0.77/1.05 % 0.77/1.05 % SZS output start CNFRefutation for /tmp/SPASST_18940_n028.cluster.edu % 0.77/1.05 % 0.77/1.05 % Here is a proof with depth 5, length 31 : % 0.77/1.05 1[0:Inp] || -> isint(skc1)*. % 0.77/1.05 2[0:Inp] || greater(skc1,19/5)* -> . % 0.77/1.05 3[0:Inp] || less(skc1,16/5)* -> . % 0.77/1.05 13[0:ThA] || -> lesseq(U,U)*. % 0.77/1.05 16[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 0.77/1.05 43[0:ThX] || isint(U) -> equal(floor(U),U)**. % 0.77/1.05 53[0:ThX] || -> less(U,V)* less(W,U)* lesseq(floor(V),floor(W))*. % 0.77/1.05 58[0:TOC:3.0] || -> lesseq(16/5,skc1)*. % 0.77/1.05 59[0:ArS:2.0] || less(19/5,skc1)* -> . % 0.77/1.05 60[0:TOC:59.0] || -> lesseq(skc1,19/5)*. % 0.77/1.05 61[0:OCE:58.0,53.0] || -> less(U,skc1)* lesseq(floor(16/5),floor(U)). % 0.77/1.05 63(e)[0:OCE:58.0,16.2] || -> equal(skc1,16/5) less(16/5,skc1)*. % 0.77/1.05 65[0:ArS:61.1] || -> less(U,skc1)* lesseq(3,floor(U)). % 0.77/1.05 67(e)[1:Spt:63.0] || -> equal(skc1,16/5)**. % 0.77/1.05 68[1:Rew:67.0,1.0] || -> isint(16/5)*. % 0.77/1.05 73(e)[1:ArS:68.0] || -> . % 0.77/1.05 76[1:Spt:73.0,63.0,67.0] || equal(skc1,16/5)** -> . % 0.77/1.05 77[1:Spt:73.0,63.1] || -> less(16/5,skc1)*. % 0.77/1.05 90[0:OCE:60.0,53.1] || -> less(skc1,U)* lesseq(floor(U),floor(19/5)). % 0.77/1.05 96[0:ArS:90.1] || -> less(skc1,U)* lesseq(floor(U),3). % 0.77/1.05 107[0:OCE:65.0,13.0] || -> lesseq(3,floor(skc1))*. % 0.77/1.05 116(e)[0:OCE:107.0,16.2] || -> equal(floor(skc1),3) less(3,floor(skc1))*. % 0.77/1.05 123[2:Spt:116.0] || -> equal(floor(skc1),3)**. % 0.77/1.05 132[2:SpR:123.0,43.1] || isint(skc1)* -> equal(skc1,3). % 0.77/1.05 141(e)[2:MRR:132.0,1.0] || -> equal(skc1,3)**. % 0.77/1.05 144[2:Rew:141.0,58.0] || -> lesseq(16/5,3)*. % 0.77/1.05 163(e)[2:ArS:144.0] || -> . % 0.77/1.05 177[2:Spt:163.0,116.0,123.0] || equal(floor(skc1),3)** -> . % 0.77/1.05 178[2:Spt:163.0,116.1] || -> less(3,floor(skc1))*. % 0.77/1.05 642[0:OCE:96.0,13.0] || -> lesseq(floor(skc1),3)*. % 0.77/1.05 664(e)[2:OCE:642.0,178.0] || -> . % 0.77/1.05 % 0.77/1.05 % SZS output end CNFRefutation for /tmp/SPASST_18940_n028.cluster.edu % 0.77/1.05 % 0.77/1.05 Formulae used in the proof : fof_prove % 0.77/1.08 % 0.83/1.08 SPASS+T ended %------------------------------------------------------------------------------