%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW000_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n032.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:29:26 EDT 2022 % Result : Theorem 1.33s 1.87s % Output : Refutation 1.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.13 % Problem : SWW000_1 : TPTP v8.1.0. Released v5.0.0. % 0.10/0.14 % Command : spasst-tptp-script %s %d % 0.11/0.34 % Computer : n032.cluster.edu % 0.11/0.34 % Model : x86_64 x86_64 % 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.34 % Memory : 8042.1875MB % 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.34 % CPULimit : 300 % 0.11/0.34 % WCLimit : 600 % 0.11/0.34 % DateTime : Sun Jun 5 16:39:33 EDT 2022 % 0.11/0.34 % CPUTime : % 0.15/0.46 % Using integer theory % 1.33/1.87 % 1.33/1.87 % 1.33/1.87 % SZS status Theorem for /tmp/SPASST_7302_n032.cluster.edu % 1.33/1.87 % 1.33/1.87 SPASS V 2.2.22 in combination with yices. % 1.33/1.87 SPASS beiseite: Proof found by SPASS. % 1.33/1.87 Problem: /tmp/SPASST_7302_n032.cluster.edu % 1.33/1.87 SPASS derived 369 clauses, backtracked 64 clauses and kept 258 clauses. % 1.33/1.87 SPASS backtracked 11 times (0 times due to theory inconsistency). % 1.33/1.87 SPASS allocated 7104 KBytes. % 1.33/1.87 SPASS spent 0:00:00.16 on the problem. % 1.33/1.87 0:00:00.01 for the input. % 1.33/1.87 0:00:00.04 for the FLOTTER CNF translation. % 1.33/1.87 0:00:00.01 for inferences. % 1.33/1.87 0:00:00.00 for the backtracking. % 1.33/1.87 0:00:00.08 for the reduction. % 1.33/1.87 0:00:00.01 for interacting with the SMT procedure. % 1.33/1.87 % 1.33/1.87 % 1.33/1.87 % SZS output start CNFRefutation for /tmp/SPASST_7302_n032.cluster.edu % 1.33/1.87 % 1.33/1.87 % Here is a proof with depth 6, length 93 : % 1.33/1.87 8[0:Inp] || -> less(z2,z1)*. % 1.33/1.87 13[0:Inp] || equal(z2,z1)** -> . % 1.33/1.87 14[0:Inp] || equal(z3,z1)** -> . % 1.33/1.87 15[0:Inp] || equal(z4,z1)** -> . % 1.33/1.87 17[0:Inp] || equal(z3,z2)** -> . % 1.33/1.87 18[0:Inp] || equal(z4,z2)** -> . % 1.33/1.87 20[0:Inp] || equal(z4,z3)** -> . % 1.33/1.87 23[0:Inp] || -> equal(a(z1),5)**. % 1.33/1.87 24[0:Inp] || -> equal(a(z2),10)**. % 1.33/1.87 26[0:Inp] || -> equal(a(z4),2)**. % 1.33/1.87 28[0:Inp] || -> less(b(z2),3)*. % 1.33/1.87 29[0:Inp] || -> equal(b(z3),5)**. % 1.33/1.87 72[0:Inp] || equal(b(U),2) equal(a(U),8)** equal(a(V),10) less(b(V),3)* less(V,W)* equal(a(W),5) -> equal(V,U)* equal(W,U)* equal(W,V). % 1.33/1.87 86[0:Inp] || equal(a(U),1)** equal(b(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),5) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 1.33/1.87 88[0:Inp] || equal(a(U),2)** equal(a(V),8)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),5) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 1.33/1.87 90[0:Inp] || equal(a(U),2)** equal(b(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),5) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 1.33/1.87 91[0:Inp] || equal(b(U),2)** equal(a(V),8)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),5) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 1.33/1.87 179[0:TOC:72.4] || equal(a(U),5)+ equal(a(V),10) equal(a(W),8)** equal(b(W),2) -> equal(U,V) equal(U,W)* equal(V,W)* lesseq(U,V)* lesseq(3,b(V))*. % 1.33/1.87 193[0:TOC:86.4] || equal(a(U),5)+ equal(a(V),10) equal(b(W),5)** equal(a(X),1)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 1.33/1.87 195[0:TOC:88.4] || equal(a(U),5)+ equal(a(V),10) equal(a(W),8)** equal(a(X),2)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 1.33/1.87 197[0:TOC:90.4] || equal(a(U),5)+ equal(a(V),10) equal(b(W),5)** equal(a(X),2)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 1.33/1.87 198[0:TOC:91.4] || equal(a(U),5)+ equal(a(V),10) equal(a(W),8)** equal(b(X),2)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 1.33/1.87 453[0:SpL:23.0,179.0] || equal(5,5) equal(a(U),10) equal(a(V),8)** equal(b(V),2) -> equal(z1,U) equal(z1,V) equal(U,V)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 454[0:ArS:453.0] || equal(a(U),10)+ equal(a(V),8)** equal(b(V),2) -> equal(z1,U) equal(z1,V) equal(U,V)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 466[0:SpL:24.0,454.0] || equal(10,10) equal(a(U),8)** equal(b(U),2) -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 469[0:ArS:466.0] || equal(a(U),8)** equal(b(U),2) -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 470(e)[0:MRR:469.2,13.0] || equal(a(U),8)** equal(b(U),2) -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 473[1:Spt:470.4] || -> lesseq(z1,z2)*. % 1.33/1.87 476(e)[1:OCE:473.0,8.0] || -> . % 1.33/1.87 479[1:Spt:476.0,470.4,473.0] || lesseq(z1,z2)* -> . % 1.33/1.87 480(e)[1:Spt:476.0,470.0,470.1,470.2,470.3,470.5] || equal(a(U),8)** equal(b(U),2) -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 1.33/1.87 482[2:Spt:480.4] || -> lesseq(3,b(z2))*. % 1.33/1.87 485(e)[2:OCE:482.0,28.0] || -> . % 1.33/1.87 490[2:Spt:485.0,480.4,482.0] || lesseq(3,b(z2))* -> . % 1.33/1.87 491[2:Spt:485.0,480.0,480.1,480.2,480.3] || equal(a(U),8)** equal(b(U),2) -> equal(z1,U) equal(z2,U). % 1.33/1.87 770[0:SpL:23.0,195.0] || equal(5,5) equal(a(U),10) equal(a(V),8)** equal(a(W),2)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 771[0:ArS:770.0] || equal(a(U),10)+ equal(a(V),8)** equal(a(W),2)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 777[0:SpL:24.0,771.0] || equal(10,10) equal(a(U),8)** equal(a(V),2)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 780[0:ArS:777.0] || equal(a(U),8)** equal(a(V),2)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 781(e)[0:MRR:780.2,13.0] || equal(a(U),8)** equal(a(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 792[3:Spt:781.7] || -> lesseq(z1,z2)*. % 1.33/1.87 795(e)[3:OCE:792.0,8.0] || -> . % 1.33/1.87 798[3:Spt:795.0,781.7,792.0] || lesseq(z1,z2)* -> . % 1.33/1.87 799(e)[3:Spt:795.0,781.0,781.1,781.2,781.3,781.4,781.5,781.6,781.8] || equal(a(U),8)** equal(a(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 1.33/1.87 803[4:Spt:799.7] || -> lesseq(3,b(z2))*. % 1.33/1.87 806(e)[4:OCE:803.0,28.0] || -> . % 1.33/1.87 811[4:Spt:806.0,799.7,803.0] || lesseq(3,b(z2))* -> . % 1.33/1.87 812[4:Spt:806.0,799.0,799.1,799.2,799.3,799.4,799.5,799.6] || equal(a(U),8)**+ equal(a(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 1.33/1.87 851[0:SpL:23.0,198.0] || equal(5,5) equal(a(U),10) equal(a(V),8)** equal(b(W),2)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 852[0:ArS:851.0] || equal(a(U),10)+ equal(a(V),8)** equal(b(W),2)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 858[0:SpL:24.0,852.0] || equal(10,10) equal(a(U),8)** equal(b(V),2)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 861[0:ArS:858.0] || equal(a(U),8)** equal(b(V),2)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 862(e)[0:MRR:861.2,13.0] || equal(a(U),8)** equal(b(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 865[5:Spt:862.7] || -> lesseq(z1,z2)*. % 1.33/1.87 868(e)[5:OCE:865.0,8.0] || -> . % 1.33/1.87 871[5:Spt:868.0,862.7,865.0] || lesseq(z1,z2)* -> . % 1.33/1.87 872(e)[5:Spt:868.0,862.0,862.1,862.2,862.3,862.4,862.5,862.6,862.8] || equal(a(U),8)** equal(b(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 1.33/1.87 875[6:Spt:872.7] || -> lesseq(3,b(z2))*. % 1.33/1.87 878(e)[6:OCE:875.0,28.0] || -> . % 1.33/1.87 883[6:Spt:878.0,872.7,875.0] || lesseq(3,b(z2))* -> . % 1.33/1.87 884[6:Spt:878.0,872.0,872.1,872.2,872.3,872.4,872.5,872.6] || equal(a(U),8)**+ equal(b(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 1.33/1.87 897[0:SpL:23.0,193.0] || equal(5,5) equal(a(U),10) equal(b(V),5)** equal(a(W),1)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 898[0:ArS:897.0] || equal(a(U),10)+ equal(b(V),5)** equal(a(W),1)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 914[0:SpL:24.0,898.0] || equal(10,10) equal(b(U),5)** equal(a(V),1)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 917[0:ArS:914.0] || equal(b(U),5)** equal(a(V),1)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 918(e)[0:MRR:917.2,13.0] || equal(b(U),5)** equal(a(V),1)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 924[0:SpL:23.0,197.0] || equal(5,5) equal(a(U),10) equal(b(V),5)** equal(a(W),2)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 925[0:ArS:924.0] || equal(a(U),10)+ equal(b(V),5)** equal(a(W),2)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 1.33/1.87 929[7:Spt:918.7] || -> lesseq(z1,z2)*. % 1.33/1.87 932(e)[7:OCE:929.0,8.0] || -> . % 1.33/1.87 935[7:Spt:932.0,918.7,929.0] || lesseq(z1,z2)* -> . % 1.33/1.87 936(e)[7:Spt:932.0,918.0,918.1,918.2,918.3,918.4,918.5,918.6,918.8] || equal(b(U),5)** equal(a(V),1)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 1.33/1.87 939[8:Spt:936.7] || -> lesseq(3,b(z2))*. % 1.33/1.87 942(e)[8:OCE:939.0,28.0] || -> . % 1.33/1.87 947[8:Spt:942.0,936.7,939.0] || lesseq(3,b(z2))* -> . % 1.33/1.87 948[8:Spt:942.0,936.0,936.1,936.2,936.3,936.4,936.5,936.6] || equal(b(U),5)**+ equal(a(V),1)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 1.33/1.87 983[0:SpL:24.0,925.0] || equal(10,10) equal(b(U),5)** equal(a(V),2)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 986[0:ArS:983.0] || equal(b(U),5)** equal(a(V),2)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 987(e)[0:MRR:986.2,13.0] || equal(b(U),5)** equal(a(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 1.33/1.87 990[9:Spt:987.7] || -> lesseq(z1,z2)*. % 1.33/1.87 993(e)[9:OCE:990.0,8.0] || -> . % 1.33/1.87 996[9:Spt:993.0,987.7,990.0] || lesseq(z1,z2)* -> . % 1.33/1.87 997(e)[9:Spt:993.0,987.0,987.1,987.2,987.3,987.4,987.5,987.6,987.8] || equal(b(U),5)** equal(a(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 1.33/1.87 1000[10:Spt:997.7] || -> lesseq(3,b(z2))*. % 1.33/1.87 1003(e)[10:OCE:1000.0,28.0] || -> . % 1.33/1.87 1008[10:Spt:1003.0,997.7,1000.0] || lesseq(3,b(z2))* -> . % 1.33/1.87 1009[10:Spt:1003.0,997.0,997.1,997.2,997.3,997.4,997.5,997.6] || equal(b(U),5)**+ equal(a(V),2)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 1.33/1.87 1011[10:SpL:29.0,1009.0] || equal(5,5) equal(a(U),2)** -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 1.33/1.87 1014[10:ArS:1011.0] || equal(a(U),2)** -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 1.33/1.87 1015[10:MRR:1014.1,1014.4,14.0,17.0] || equal(a(U),2)** -> equal(z1,U) equal(z2,U) equal(z3,U). % 1.33/1.87 1016[10:SpL:26.0,1015.0] || equal(2,2) -> equal(z4,z1) equal(z4,z2) equal(z4,z3)**. % 1.33/1.87 1020[10:ArS:1016.0] || -> equal(z4,z1) equal(z4,z2) equal(z4,z3)**. % 1.33/1.87 1021(e)[10:MRR:1020.0,1020.1,1020.2,15.0,18.0,20.0] || -> . % 1.33/1.87 % 1.33/1.87 % SZS output end CNFRefutation for /tmp/SPASST_7302_n032.cluster.edu % 1.33/1.87 % 1.33/1.87 Formulae used in the proof : fof_z1_type fof_0 % 1.33/1.90 % 1.33/1.90 SPASS+T ended %------------------------------------------------------------------------------