%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW653_2 : TPTP v8.1.0. Released v6.1.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 : 600s % DateTime : Thu Jul 21 01:30:36 EDT 2022 % Result : Theorem 6.47s 4.49s % Output : Refutation 6.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW653_2 : TPTP v8.1.0. Released v6.1.0. % 0.07/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n022.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 : Mon Jun 6 01:46:05 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.48 % Using integer theory % 6.47/4.49 % 6.47/4.49 % 6.47/4.49 % SZS status Theorem for /tmp/SPASST_17306_n022.cluster.edu % 6.47/4.49 % 6.47/4.49 SPASS V 2.2.22 in combination with yices. % 6.47/4.49 SPASS beiseite: Proof found by SPASS and SMT. % 6.47/4.49 Problem: /tmp/SPASST_17306_n022.cluster.edu % 6.47/4.49 SPASS derived 32912 clauses, backtracked 2949 clauses and kept 6829 clauses. % 6.47/4.49 SPASS backtracked 76 times (2 times due to theory inconsistency). % 6.47/4.49 SPASS allocated 29252 KBytes. % 6.47/4.49 SPASS spent 0:00:03.31 on the problem. % 6.47/4.49 0:00:00.00 for the input. % 6.47/4.49 0:00:00.02 for the FLOTTER CNF translation. % 6.47/4.49 0:00:00.19 for inferences. % 6.47/4.49 0:00:00.23 for the backtracking. % 6.47/4.49 0:00:02.37 for the reduction. % 6.47/4.49 0:00:00.35 for interacting with the SMT procedure. % 6.47/4.49 % 6.47/4.49 % 6.47/4.49 % SZS output start CNFRefutation for /tmp/SPASST_17306_n022.cluster.edu % 6.47/4.49 % 6.47/4.49 % Here is a proof with depth 10, length 134 : % 6.47/4.49 21[0:Inp] || -> uf_pure1(skc14)*. % 6.47/4.49 22[0:Inp] || -> graph1(skc12)*. % 6.47/4.49 23[0:Inp] || -> lesseq(0,skc16)*. % 6.47/4.49 24[0:Inp] || -> lesseq(1,skc13)*. % 6.47/4.49 27[0:Inp] || -> less(skc15,times(skc13,skc13))*. % 6.47/4.49 28[0:Inp] || -> lesseq(0,times(skc13,skc13))*. % 6.47/4.49 34[0:Inp] || -> equal(times(skc13,skc13),num1(skc14))**. % 6.47/4.49 35[0:Inp] || -> equal(times(skc13,skc13),size1(skc14))**. % 6.47/4.49 38[0:Inp] || graph1(U) -> path1(U,V,V)*. % 6.47/4.49 42[0:Inp] || uf_pure1(U) -> equal(state1(mk_uf1(U)),U)**. % 6.47/4.49 43[0:Inp] || equal(U,V) -> path1(skc12,U,V)*. % 6.47/4.49 44[0:Inp] || path1(skc12,U,V)* -> equal(U,V). % 6.47/4.49 53[0:Inp] || lesseq(0,U) lesseq(V,W) -> lesseq(times(V,U),times(W,U))*. % 6.47/4.49 54[0:Inp] || graph1(U) path1(U,V,W)*+ path1(U,W,X)* -> path1(U,V,X)*. % 6.47/4.49 67[0:Inp] || uf_pure1(U)+ -> same1(U,V,W) repr1(U,V,skf6(W,V,U))* repr1(U,W,skf6(W,V,U))*. % 6.47/4.49 68[0:Inp] || equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) lesseq(1,num1(skc14))* -> lesseq(0,skc15). % 6.47/4.49 69[0:Inp] || uf_pure1(U) repr1(U,V,skf6(W,V,U))*+ repr1(U,W,skf6(W,V,U))* -> same1(U,V,W). % 6.47/4.49 72[0:Inp] || equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) lesseq(1,num1(skc14)) -> less(skc16,times(skc13,skc13))*. % 6.47/4.49 76[0:Inp] || lesseq(0,U) lesseq(0,V) less(U,W) less(V,W) lesseq(0,W) -> lesseq(0,plus(times(V,W),U))*. % 6.47/4.49 77[0:Inp] || equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) lesseq(1,num1(skc14)) -> path1(skc12,skc16,skc15) same1(skc14,skc16,skc15)*. % 6.47/4.49 78[0:Inp] || lesseq(0,U) less(U,times(skc13,skc13))* same1(skc14,V,U)* less(V,times(skc13,skc13))* lesseq(0,V) -> equal(V,U). % 6.47/4.49 80[0:Inp] || lesseq(0,U) lesseq(0,V) less(U,W) less(V,W) lesseq(0,W) -> less(plus(times(V,W),U),times(W,W))*. % 6.47/4.49 81[0:Inp] || path1(skc12,skc16,skc15) same1(skc14,skc16,skc15)* equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) lesseq(1,num1(skc14)) -> . % 6.47/4.49 83[0:ThA] || -> equal(uminus(uminus(U)),U)**. % 6.47/4.49 90[0:ThA] || -> equal(plus(U,0),U)**. % 6.47/4.49 94[0:ThA] || -> less(plus(U,-1),U)*. % 6.47/4.49 95[0:ThA] || -> equal(U,V) less(V,U)* less(U,V)*. % 6.47/4.49 98[0:ThA] || -> lesseq(U,V) less(uminus(U),uminus(V))*. % 6.47/4.49 101[0:ThA] || -> equal(times(U,1),U)**. % 6.47/4.49 102[0:ThA] || -> equal(times(1,U),U)**. % 6.47/4.49 104[0:ThA] || -> equal(times(-1,U),uminus(U))**. % 6.47/4.49 114[0:Rew:35.0,28.0] || -> lesseq(0,size1(skc14))*. % 6.47/4.49 115[0:Rew:35.0,27.0] || -> less(skc15,size1(skc14))*. % 6.47/4.49 116[0:Rew:35.0,34.0] || -> equal(size1(skc14),num1(skc14))**. % 6.47/4.49 117[0:Rew:116.0,35.0] || -> equal(times(skc13,skc13),num1(skc14))**. % 6.47/4.49 118[0:Rew:116.0,114.0] || -> lesseq(0,num1(skc14))*. % 6.47/4.49 119[0:Rew:116.0,115.0] || -> less(skc15,num1(skc14))*. % 6.47/4.49 122[0:TOC:53.1] || -> less(U,V) less(W,0) lesseq(times(V,W),times(U,W))*. % 6.47/4.49 125[0:TOC:68.2] || equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) -> less(num1(skc14),1)* lesseq(0,skc15). % 6.47/4.49 126[0:Rew:90.0,125.1,116.0,125.1,117.0,125.0,116.0,125.0] || equal(num1(skc14),num1(skc14)) equal(num1(skc14),num1(skc14)) -> less(num1(skc14),1)* lesseq(0,skc15). % 6.47/4.49 127(e)[0:Obv:126.1] || -> lesseq(0,skc15) less(num1(skc14),1)*. % 6.47/4.49 128[0:TOC:72.2] || equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) -> less(num1(skc14),1) less(skc16,times(skc13,skc13))*. % 6.47/4.49 129[0:Rew:117.0,128.3,90.0,128.1,116.0,128.1,117.0,128.0,116.0,128.0] || equal(num1(skc14),num1(skc14)) equal(num1(skc14),num1(skc14)) -> less(num1(skc14),1) less(skc16,num1(skc14))*. % 6.47/4.49 130[0:Obv:129.1] || -> less(skc16,num1(skc14))* less(num1(skc14),1). % 6.47/4.49 132[0:TOC:76.1] || -> lesseq(U,V) lesseq(U,W) less(W,0) less(U,0) less(V,0) lesseq(0,plus(times(V,U),W))*. % 6.47/4.49 136[0:TOC:78.1] || same1(skc14,U,V)* -> lesseq(times(skc13,skc13),V)* lesseq(times(skc13,skc13),U)* less(U,0) less(V,0) equal(U,V). % 6.47/4.49 137[0:Rew:117.0,136.2,117.0,136.1] || same1(skc14,U,V)*+ -> equal(U,V) less(V,0) less(U,0) lesseq(num1(skc14),U)* lesseq(num1(skc14),V)*. % 6.47/4.49 140[0:TOC:80.1] || -> lesseq(U,V) lesseq(U,W) less(W,0) less(U,0) less(V,0) less(plus(times(V,U),W),times(U,U))*. % 6.47/4.49 141[0:TOC:81.4] || path1(skc12,skc16,skc15) same1(skc14,skc16,skc15)* equal(times(skc13,skc13),size1(skc14)) equal(plus(num1(skc14),0),size1(skc14)) -> less(num1(skc14),1). % 6.47/4.49 142[0:Rew:90.0,141.3,116.0,141.3,117.0,141.2,116.0,141.2] || path1(skc12,skc16,skc15) same1(skc14,skc16,skc15)* equal(num1(skc14),num1(skc14)) equal(num1(skc14),num1(skc14)) -> less(num1(skc14),1). % 6.47/4.49 143[0:Obv:142.3] || same1(skc14,skc16,skc15)* path1(skc12,skc16,skc15) -> less(num1(skc14),1). % 6.47/4.49 149[0:Res:22.0,38.0] || -> path1(skc12,U,U)*. % 6.47/4.49 162[0:Res:21.0,42.0] || -> equal(state1(mk_uf1(skc14)),skc14)**. % 6.47/4.49 220[1:Spt:127.0] || -> lesseq(0,skc15)*. % 6.47/4.49 238(e)[0:OCE:24.0,95.1] || -> equal(skc13,1) less(1,skc13)*. % 6.47/4.49 290(e)[0:OCE:118.0,95.1] || -> equal(num1(skc14),0) less(0,num1(skc14))*. % 6.47/4.49 343[0:SpR:102.0,122.2] || -> less(1,U) less(V,0) lesseq(times(U,V),V)*. % 6.47/4.49 348(e)[0:SpR:117.0,122.2] || -> less(skc13,U) less(skc13,0) lesseq(times(U,skc13),num1(skc14))*. % 6.47/4.49 355(e)[0:SpR:117.0,122.2] || -> less(U,skc13) less(skc13,0) lesseq(num1(skc14),times(U,skc13))*. % 6.47/4.49 358[0:OCh:122.2,122.2] || -> less(U,V)* less(W,0) less(V,X)* less(W,0) lesseq(times(X,W),times(U,W))*. % 6.47/4.49 370[0:Obv:358.1] || -> less(U,V)* less(V,W)* less(X,0) lesseq(times(W,X),times(U,X))*. % 6.47/4.49 436[0:SpR:104.0,343.2] || -> less(1,-1) less(U,0) lesseq(uminus(U),U)*. % 6.47/4.49 448[0:ArS:436.0] || -> less(U,0) lesseq(uminus(U),U)*. % 6.47/4.49 452[0:SpR:83.0,448.1] || -> less(uminus(U),0) lesseq(U,uminus(U))*. % 6.47/4.49 454[0:OCh:448.1,98.1] || -> less(U,0) lesseq(V,U) less(uminus(V),U)*. % 6.47/4.49 455[0:ArS:452.0] || -> less(0,U) lesseq(U,uminus(U))*. % 6.47/4.49 461[0:OCh:455.1,98.1] || -> less(0,U) lesseq(U,V) less(U,uminus(V))*. % 6.47/4.49 465[0:SpR:83.0,454.2] || -> less(U,0) lesseq(uminus(V),U)* less(V,U). % 6.47/4.49 466[0:OCE:454.2,94.0] || -> less(plus(uminus(U),-1),0) lesseq(U,plus(uminus(U),-1))*. % 6.47/4.49 481[0:ArS:466.0] || -> less(-1,U) lesseq(U,plus(uminus(U),-1))*. % 6.47/4.49 495[0:OCh:481.1,94.0] || -> less(-1,U) less(U,uminus(U))*. % 6.47/4.49 501[0:SpR:83.0,495.1] || -> less(-1,uminus(U))* less(uminus(U),U)*. % 6.47/4.49 511[0:ArS:501.0] || -> less(U,1) less(uminus(U),U)*. % 6.47/4.49 535[0:OCE:511.1,455.1] || -> less(U,1)* less(0,U). % 6.47/4.49 545[0:Res:43.1,54.1] || equal(U,V)* graph1(skc12) path1(skc12,V,W)* -> path1(skc12,U,W)*. % 6.47/4.49 547[0:MRR:545.1,22.0] || equal(U,V)* path1(skc12,V,W)*+ -> path1(skc12,U,W)*. % 6.47/4.49 578[0:OCE:535.0,24.0] || -> less(0,skc13)*. % 6.47/4.49 810[0:SpR:83.0,461.2] || -> less(0,U) lesseq(U,uminus(V))* less(U,V). % 6.47/4.49 868[0:OCh:465.1,495.1] || -> less(U,0)* less(V,U)* less(-1,V)* less(V,U)*. % 6.47/4.49 879[0:Obv:868.1] || -> less(U,0)* less(-1,V)* less(V,U)*. % 6.47/4.49 1786[0:Res:21.0,67.0] || -> same1(skc14,U,V) repr1(skc14,U,skf6(V,U,skc14))* repr1(skc14,V,skf6(V,U,skc14))*. % 6.47/4.49 3693[0:OCh:810.1,511.1] || -> less(0,U)* less(U,V)* less(V,1)* less(U,V)*. % 6.47/4.49 3707[0:Obv:3693.1] || -> less(0,U)* less(V,1)* less(U,V)*. % 6.47/4.49 3999[0:OCE:3707.1,24.0] || -> less(0,U) less(U,skc13)*. % 6.47/4.49 4290[0:OCh:140.5,132.5] || -> lesseq(U,V)* lesseq(U,W)* less(W,0) less(U,0) less(V,0) lesseq(U,V)* lesseq(U,W)* less(W,0) less(U,0) less(V,0) less(0,times(U,U))*. % 6.47/4.49 4331[0:Obv:4290.4] || -> lesseq(U,V)* lesseq(U,W)* less(W,0) less(U,0) less(V,0) less(0,times(U,U))*. % 6.47/4.49 4332[0:Con:4331.0] || -> lesseq(U,V)* less(V,0) less(U,0) less(0,times(U,U))*. % 6.47/4.49 6377[0:OCE:23.0,879.0] || -> less(-1,U) less(U,skc16)*. % 6.47/4.49 17783[0:OCE:6377.1,6377.1] || -> less(-1,skc16)* less(-1,skc16)*. % 6.47/4.49 18313[0:Res:149.0,547.1] || equal(U,V) -> path1(skc12,U,V)*. % 6.47/4.49 19768[0:OCE:4332.0,94.0] || -> less(plus(U,-1),0)* less(U,0) less(0,times(U,U))*. % 6.47/4.49 19839[0:ArS:19768.0] || -> less(U,1) less(U,0) less(0,times(U,U))*. % 6.47/4.49 25459[0:SpR:117.0,19839.2] || -> less(skc13,1) less(skc13,0) less(0,num1(skc14))*. % 6.47/4.49 33644[0:SpR:101.0,370.3] || -> less(U,V)* less(V,W)* less(1,0) lesseq(times(W,1),U)*. % 6.47/4.49 34132[0:ArS:33644.3] || -> less(U,V)* less(V,W)* lesseq(times(1,W),U)*. % 6.47/4.49 34133[0:Rew:102.0,34132.2] || -> less(U,V)* less(V,W)* lesseq(W,U)*. % 6.47/4.49 34631[0:OCE:34133.1,578.0] || -> less(U,skc13)* lesseq(0,U). % 6.47/4.49 34917(e)[0:OCE:34133.2,3999.1] || -> less(U,V)* less(V,skc13)* less(0,U)*. % 6.47/4.49 35108(e)[0:OCE:34631.0,34133.2] || -> lesseq(0,U)* less(U,V)* less(V,skc13)*. % 6.47/4.49 47425[1:ThR:220,35108,34917,25459,137,116,18313,17783,1786,69,143,44,130,162,119,21,77,35] || -> . % 6.47/4.49 47426[1:Spt:47425.0,127.0,220.0] || lesseq(0,skc15)* -> . % 6.47/4.49 47427[1:Spt:47425.0,127.1] || -> less(num1(skc14),1)*. % 6.47/4.49 47456(e)[2:Spt:238.0] || -> equal(skc13,1)**. % 6.47/4.49 47545[2:Rew:47456.0,117.0] || -> equal(num1(skc14),times(1,1))**. % 6.47/4.49 47556(e)[2:ArS:47545.0] || -> equal(num1(skc14),1)**. % 6.47/4.49 47557[2:Rew:47556.0,47427.0] || -> less(1,1)*. % 6.47/4.49 47607(e)[2:ArS:47557.0] || -> . % 6.47/4.49 47687[2:Spt:47607.0,238.0,47456.0] || equal(skc13,1)** -> . % 6.47/4.49 47688[2:Spt:47607.0,238.1] || -> less(1,skc13)*. % 6.47/4.49 47862[3:Spt:290.0] || -> equal(num1(skc14),0)**. % 6.47/4.49 47888[3:Rew:47862.0,25459.2] || -> less(skc13,1)* less(skc13,0) less(0,0). % 6.47/4.49 47929(e)[3:ArS:47888.2] || -> less(skc13,1)* less(skc13,0). % 6.47/4.49 48077[4:Spt:47929.0] || -> less(skc13,1)*. % 6.47/4.49 48083(e)[4:OCE:48077.0,47688.0] || -> . % 6.47/4.49 48122[4:Spt:48083.0,47929.0,48077.0] || less(skc13,1)* -> . % 6.47/4.49 48123[4:Spt:48083.0,47929.1] || -> less(skc13,0)*. % 6.47/4.49 48125(e)[4:OCE:48123.0,578.0] || -> . % 6.47/4.49 48153[3:Spt:48125.0,290.0,47862.0] || equal(num1(skc14),0)** -> . % 6.47/4.49 48154[3:Spt:48125.0,290.1] || -> less(0,num1(skc14))*. % 6.47/4.49 49827[4:Spt:355.1] || -> less(skc13,0)*. % 6.47/4.49 49828(e)[4:OCE:49827.0,578.0] || -> . % 6.47/4.49 49886[4:Spt:49828.0,355.1,49827.0] || less(skc13,0)* -> . % 6.47/4.49 49887[4:Spt:49828.0,355.0,355.2] || -> less(U,skc13) lesseq(num1(skc14),times(U,skc13))*. % 6.47/4.49 49976[5:Spt:348.1] || -> less(skc13,0)*. % 6.47/4.49 49977(e)[5:OCE:49976.0,578.0] || -> . % 6.47/4.49 50035[5:Spt:49977.0,348.1,49976.0] || less(skc13,0)* -> . % 6.47/4.49 50036[5:Spt:49977.0,348.0,348.2] || -> less(skc13,U) lesseq(times(U,skc13),num1(skc14))*. % 6.47/4.49 50039(e)[5:SpR:102.0,50036.1] || -> less(skc13,1) lesseq(skc13,num1(skc14))*. % 6.47/4.49 50361[6:Spt:50039.0] || -> less(skc13,1)*. % 6.47/4.49 50367(e)[6:OCE:50361.0,47688.0] || -> . % 6.47/4.49 50436[6:Spt:50367.0,50039.0,50361.0] || less(skc13,1)* -> . % 6.47/4.49 50437[6:Spt:50367.0,50039.1] || -> lesseq(skc13,num1(skc14))*. % 6.47/4.49 50455[6:OCh:50437.0,47427.0] || -> less(skc13,1)*. % 6.47/4.49 50626(e)[6:OCE:50455.0,47688.0] || -> . % 6.47/4.49 % 6.47/4.49 % SZS output end CNFRefutation for /tmp/SPASST_17306_n022.cluster.edu % 6.47/4.49 % 6.47/4.49 Formulae used in the proof : fof_uni fof_wP_parameter_build_maze fof_repr_function_1 fof_witness fof_path_inversion fof_uf_inversion1 fof_state_def1 fof_compatOrderMult fof_match_bool_False fof_same_def fof_same_reprs_def fof_ineq1 % 9.37/6.56 % 9.37/6.56 SPASS+T ended %------------------------------------------------------------------------------