%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : DAT072_1 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n020.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 : Sat Jul 16 01:32:05 EDT 2022 % Result : Theorem 6.00s 3.79s % Output : Refutation 6.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : DAT072_1 : TPTP v8.1.0. Released v6.1.0. % 0.07/0.12 % Command : spasst-tptp-script %s %d % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 17:35:15 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.45 % Using integer theory % 6.00/3.79 % 6.00/3.79 % 6.00/3.79 % SZS status Theorem for /tmp/SPASST_30479_n020.cluster.edu % 6.00/3.79 % 6.00/3.79 SPASS V 2.2.22 in combination with yices. % 6.00/3.79 SPASS beiseite: Proof found by SPASS and SMT. % 6.00/3.79 Problem: /tmp/SPASST_30479_n020.cluster.edu % 6.00/3.79 SPASS derived 15234 clauses, backtracked 827 clauses and kept 3380 clauses. % 6.00/3.79 SPASS backtracked 5 times (1 times due to theory inconsistency). % 6.00/3.79 SPASS allocated 23407 KBytes. % 6.00/3.79 SPASS spent 0:00:02.72 on the problem. % 6.00/3.79 0:00:00.00 for the input. % 6.00/3.79 0:00:00.01 for the FLOTTER CNF translation. % 6.00/3.79 0:00:00.12 for inferences. % 6.00/3.79 0:00:00.12 for the backtracking. % 6.00/3.79 0:00:01.79 for the reduction. % 6.00/3.79 0:00:00.16 for interacting with the SMT procedure. % 6.00/3.79 % 6.00/3.79 % 6.00/3.79 % SZS output start CNFRefutation for /tmp/SPASST_30479_n020.cluster.edu % 6.00/3.79 % 6.00/3.79 % Here is a proof with depth 3, length 35 : % 6.00/3.79 5[0:Inp] || -> array(skc6)*. % 6.00/3.79 6[0:Inp] || -> array(skc5)*. % 6.00/3.79 8[0:Inp] || equal(skc6,skc5)** -> . % 6.00/3.79 18[0:Inp] || SkP0(U,V,W,X)* -> greater(W,X). % 6.00/3.79 19[0:Inp] || SkP0(U,V,W,X)* -> greatereq(X,0). % 6.00/3.79 24[0:Inp] || -> greatereq(U,skc8) greater(0,U) SkP0(skc7,skc6,skc8,U)*. % 6.00/3.79 25[0:Inp] || -> greatereq(U,skc8) greater(0,U) SkP0(skc7,skc5,skc8,U)*. % 6.00/3.79 26[0:Inp] || -> equal(read(skc7,U),read(skc6,U)) SkP0(skc7,skc6,skc8,U)*. % 6.00/3.79 27[0:Inp] || -> equal(read(skc7,U),read(skc5,U)) SkP0(skc7,skc5,skc8,U)*. % 6.00/3.79 33[0:Inp] || equal(U,minus(V,plus(W,1)))* SkP0(X,Y,V,W)* -> equal(read(Y,W),read(X,U))*. % 6.00/3.79 35[0:Inp] || array(U) array(V) equal(read(U,skf8(V,U)),read(V,skf8(V,U)))* -> equal(U,V). % 6.00/3.79 81[0:ArS:19.1] || SkP0(U,V,W,X)* -> lesseq(0,X). % 6.00/3.79 82[0:ArS:18.1] || SkP0(U,V,W,X)* -> less(X,W). % 6.00/3.79 83[0:ArS:25.1] || -> less(U,0) lesseq(skc8,U) SkP0(skc7,skc5,skc8,U)*. % 6.00/3.79 84[0:ArS:24.1] || -> less(U,0) lesseq(skc8,U) SkP0(skc7,skc6,skc8,U)*. % 6.00/3.79 89[0:ArS:33.0] || equal(U,plus(V,uminus(plus(W,1))))*+ SkP0(X,Y,V,W)* -> equal(read(Y,W),read(X,U))*. % 6.00/3.79 133[0:Res:6.0,35.2] || array(U) equal(read(skc5,skf8(U,skc5)),read(U,skf8(U,skc5)))* -> equal(skc5,U). % 6.00/3.79 278[0:Res:27.1,82.0] || -> equal(read(skc7,U),read(skc5,U))** less(U,skc8). % 6.00/3.79 279[0:Res:27.1,81.0] || -> equal(read(skc7,U),read(skc5,U))** lesseq(0,U). % 6.00/3.79 302[0:Res:26.1,82.0] || -> equal(read(skc7,U),read(skc6,U))** less(U,skc8). % 6.00/3.79 303[0:Res:26.1,81.0] || -> equal(read(skc7,U),read(skc6,U))** lesseq(0,U). % 6.00/3.79 304[0:Rew:278.0,302.0] || -> equal(read(skc6,U),read(skc5,U))** less(U,skc8). % 6.00/3.79 305[0:Rew:279.0,303.0] || -> equal(read(skc6,U),read(skc5,U))** lesseq(0,U). % 6.00/3.79 606[0:EqR:89.0] || SkP0(U,V,W,X)*+ -> equal(read(V,X),read(U,plus(W,uminus(plus(X,1)))))*. % 6.00/3.79 3218[0:SpL:305.0,133.1] || array(skc6) equal(read(skc5,skf8(skc6,skc5)),read(skc5,skf8(skc6,skc5)))* -> lesseq(0,skf8(skc6,skc5)) equal(skc6,skc5). % 6.00/3.79 3219[0:SpL:304.0,133.1] || array(skc6) equal(read(skc5,skf8(skc6,skc5)),read(skc5,skf8(skc6,skc5)))* -> less(skf8(skc6,skc5),skc8) equal(skc6,skc5). % 6.00/3.79 3221[0:Obv:3219.1] || array(skc6) -> less(skf8(skc6,skc5),skc8)* equal(skc6,skc5). % 6.00/3.79 3222[0:MRR:3221.0,3221.2,5.0,8.0] || -> less(skf8(skc6,skc5),skc8)*. % 6.00/3.79 3223[0:Obv:3218.1] || array(skc6) -> lesseq(0,skf8(skc6,skc5))* equal(skc6,skc5). % 6.00/3.79 3224[0:MRR:3223.0,3223.2,5.0,8.0] || -> lesseq(0,skf8(skc6,skc5))*. % 6.00/3.79 17012[0:Res:83.2,606.0] || -> less(U,0) lesseq(skc8,U) equal(read(skc7,plus(skc8,uminus(plus(U,1)))),read(skc5,U))**. % 6.00/3.79 17069[0:Res:84.2,606.0] || -> less(U,0) lesseq(skc8,U) equal(read(skc7,plus(skc8,uminus(plus(U,1)))),read(skc6,U))**. % 6.00/3.79 17075[0:Rew:17012.2,17069.2] || -> less(U,0) lesseq(skc8,U) equal(read(skc6,U),read(skc5,U))**. % 6.00/3.79 20343[0:SpL:17075.2,133.1] || array(skc6) equal(read(skc5,skf8(skc6,skc5)),read(skc5,skf8(skc6,skc5)))* -> less(skf8(skc6,skc5),0) lesseq(skc8,skf8(skc6,skc5)) equal(skc6,skc5). % 6.00/3.79 26393(e)[0:ThR:20343,3224,3222,8,5] || -> . % 6.00/3.79 % 6.00/3.79 % SZS output end CNFRefutation for /tmp/SPASST_30479_n020.cluster.edu % 6.00/3.79 % 6.00/3.79 Formulae used in the proof : fof_c fof_init_type fof_write_type fof_ax1 fof_distinct fof_sorted1 % 6.15/3.98 % 6.15/3.98 SPASS+T ended %------------------------------------------------------------------------------