%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC170+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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 : Tue Jul 19 22:02:13 EDT 2022 % Result : Theorem 7.99s 8.18s % Output : Refutation 7.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC170+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 12 14:42:41 EDT 2022 % 0.12/0.34 % CPUTime : % 7.99/8.18 % 7.99/8.18 SPASS V 3.9 % 7.99/8.18 SPASS beiseite: Proof found. % 7.99/8.18 % SZS status Theorem % 7.99/8.18 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 7.99/8.18 SPASS derived 7996 clauses, backtracked 2214 clauses, performed 39 splits and kept 5274 clauses. % 7.99/8.18 SPASS allocated 109638 KBytes. % 7.99/8.18 SPASS spent 0:00:07.81 on the problem. % 7.99/8.18 0:00:00.04 for the input. % 7.99/8.18 0:00:00.07 for the FLOTTER CNF translation. % 7.99/8.18 0:00:00.10 for inferences. % 7.99/8.18 0:00:00.18 for the backtracking. % 7.99/8.18 0:00:07.23 for the reduction. % 7.99/8.18 % 7.99/8.18 % 7.99/8.18 Here is a proof with depth 6, length 107 : % 7.99/8.18 % SZS output start Refutation % 7.99/8.18 1[0:Inp] || -> ssList(skc13)*. % 7.99/8.18 2[0:Inp] || -> ssList(skc12)*. % 7.99/8.18 3[0:Inp] || -> ssItem(skc11)*. % 7.99/8.18 4[0:Inp] || -> ssItem(skc10)*. % 7.99/8.18 5[0:Inp] || -> ssList(skc9)*. % 7.99/8.18 6[0:Inp] || -> ssList(skc8)*. % 7.99/8.18 7[0:Inp] || -> ssItem(skc15)*. % 7.99/8.18 8[0:Inp] || -> ssItem(skc14)*. % 7.99/8.18 9[0:Inp] || -> ssList(nil)*. % 7.99/8.18 10[0:Inp] || -> cyclefreeP(nil)*. % 7.99/8.18 11[0:Inp] || -> totalorderP(nil)*. % 7.99/8.18 12[0:Inp] || -> strictorderP(nil)*. % 7.99/8.18 13[0:Inp] || -> totalorderedP(nil)*. % 7.99/8.18 14[0:Inp] || -> strictorderedP(nil)*. % 7.99/8.18 15[0:Inp] || -> duplicatefreeP(nil)*. % 7.99/8.18 16[0:Inp] || -> equalelemsP(nil)*. % 7.99/8.18 17[0:Inp] || -> segmentP(skc9,skc8)*. % 7.99/8.18 18[0:Inp] || -> ssItem(skf45(u))*. % 7.99/8.18 56[0:Inp] || neq(skc10,skc11)* -> . % 7.99/8.18 57[0:Inp] || equal(skc15,skc14)** -> . % 7.99/8.18 64[0:Inp] || neq(skc9,nil)* -> singletonP(skc8). % 7.99/8.18 73[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 7.99/8.18 74[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 7.99/8.18 75[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 7.99/8.18 76[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 7.99/8.18 77[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 7.99/8.18 78[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 7.99/8.18 79[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 7.99/8.18 80[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 7.99/8.18 82[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 7.99/8.18 91[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 7.99/8.18 92[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 7.99/8.18 97[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 7.99/8.18 106[0:Inp] ssItem(u) ssItem(v) || -> neq(v,u)* equal(v,u). % 7.99/8.18 107[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf45(u),nil),u)**. % 7.99/8.18 108[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 7.99/8.18 111[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 7.99/8.18 113[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 7.99/8.18 122[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 7.99/8.18 129[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 7.99/8.18 134[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 7.99/8.18 153[0:Inp] ssList(u) ssItem(v) || totalorderedP(cons(v,u))* -> leq(v,hd(u)) equal(nil,u). % 7.99/8.18 154[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 7.99/8.18 160[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 7.99/8.18 187[0:Inp] ssItem(u) ssList(v) ssList(w) ssList(x) || equal(app(x,cons(u,w)),v)*+ -> memberP(v,u)*. % 7.99/8.18 193[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) ssItem(y) ssItem(z) duplicatefreeP(u) || equal(z,y) equal(app(app(x,cons(z,w)),cons(y,v)),u)* -> . % 7.99/8.18 244[0:Res:6.0,134.0] ssList(u) || -> equal(skc8,nil) equal(hd(app(skc8,u)),hd(skc8))**. % 7.99/8.18 255[0:Res:6.0,111.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 7.99/8.18 267[0:Res:6.0,91.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 7.99/8.18 273[0:Res:6.0,97.0] || segmentP(nil,skc8)* -> equal(skc8,nil). % 7.99/8.18 308[0:Res:6.0,154.1] ssItem(u) || strictorderedP(cons(u,skc8))* -> lt(u,hd(skc8)) equal(skc8,nil). % 7.99/8.18 423[0:Res:5.0,108.0] ssList(u) || -> neq(skc9,u)* equal(skc9,u). % 7.99/8.18 478[0:Res:5.0,153.1] ssItem(u) || totalorderedP(cons(u,skc9))* -> leq(u,hd(skc9)) equal(skc9,nil). % 7.99/8.18 544[1:Spt:244.0,244.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 7.99/8.18 552[2:Spt:308.3] || -> equal(skc8,nil)**. % 7.99/8.18 553[2:Rew:552.0,544.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 7.99/8.18 571[2:Rew:552.0,267.1] ssItem(u) || -> ssList(cons(u,nil))*. % 7.99/8.18 572[2:Rew:552.0,255.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 7.99/8.18 726[2:Rew:82.1,553.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 7.99/8.18 1177[2:SpR:572.1,726.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 7.99/8.18 1180[2:SSi:1177.1,80.1,79.1,76.1,75.1,74.1,78.1,77.1,571.1] ssItem(u) || -> equal(u,hd(nil))*. % 7.99/8.18 1246[2:SpR:1180.1,1180.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 7.99/8.18 1286[2:EmS:1246.0,3.0] ssItem(u) || -> equal(u,skc11)*. % 7.99/8.18 1309[2:EmS:1286.0,4.0] || -> equal(skc11,skc10)**. % 7.99/8.18 1310[2:EmS:1286.0,7.0] || -> equal(skc15,skc11)**. % 7.99/8.18 1311[2:EmS:1286.0,8.0] || -> equal(skc14,skc11)**. % 7.99/8.18 1316[2:Rew:1309.0,1310.0] || -> equal(skc15,skc10)**. % 7.99/8.18 1318[2:Rew:1316.0,57.0] || equal(skc14,skc10)** -> . % 7.99/8.18 1320[2:Rew:1309.0,1311.0] || -> equal(skc14,skc10)**. % 7.99/8.18 1439[2:Rew:1320.0,1318.0] || equal(skc10,skc10)* -> . % 7.99/8.18 1440[2:Obv:1439.0] || -> . % 7.99/8.18 1470[2:Spt:1440.0,308.3,552.0] || equal(skc8,nil)** -> . % 7.99/8.18 1471[2:Spt:1440.0,308.0,308.1,308.2] ssItem(u) || strictorderedP(cons(u,skc8))* -> lt(u,hd(skc8)). % 7.99/8.18 1474[2:MRR:273.1,1470.0] || segmentP(nil,skc8)* -> . % 7.99/8.18 1485[3:Spt:478.3] || -> equal(skc9,nil)**. % 7.99/8.18 1493[3:Rew:1485.0,17.0] || -> segmentP(nil,skc8)*. % 7.99/8.18 1638[3:MRR:1493.0,1474.0] || -> . % 7.99/8.18 1749[3:Spt:1638.0,478.3,1485.0] || equal(skc9,nil)** -> . % 7.99/8.18 1750[3:Spt:1638.0,478.0,478.1,478.2] ssItem(u) || totalorderedP(cons(u,skc9))* -> leq(u,hd(skc9)). % 7.99/8.18 1925[0:SpR:107.2,79.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> duplicatefreeP(u)*. % 7.99/8.18 1938[0:SSi:1925.2,18.0] ssList(u) singletonP(u) || -> duplicatefreeP(u)*. % 7.99/8.18 2129[0:Res:106.2,56.0] ssItem(skc11) ssItem(skc10) || -> equal(skc11,skc10)**. % 7.99/8.18 2134[0:SSi:2129.1,2129.0,4.0,3.0] || -> equal(skc11,skc10)**. % 7.99/8.18 2137[0:Rew:2134.0,113.0] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc10,nil)),skc13),skc8)**. % 7.99/8.18 2570[0:EqR:122.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 7.99/8.18 2575[0:SSi:2570.0,91.1,16.1,15.1,12.1,11.1,10.1,14.1,13.0,9.0,80.0,79.0,76.0,75.0,74.0,78.0,77.2] ssItem(u) || -> singletonP(cons(u,nil))*. % 7.99/8.18 4261[0:SpR:160.3,2137.0] ssList(skc13) ssList(cons(skc10,nil)) ssList(app(skc12,cons(skc10,nil))) || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc10,nil),skc13)),skc8)**. % 7.99/8.18 4310[0:SSi:4261.2,4261.1,4261.0,92.0,2.0,91.1,4.0,16.1,15.0,12.1,11.0,10.1,14.0,13.1,9.0,80.1,4.0,79.1,4.0,76.1,4.0,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2575.2,4.0,91.1,4.0,16.1,15.0,12.1,11.0,10.1,14.0,13.1,9.0,80.1,4.0,79.1,4.0,76.1,4.0,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2575.2,4.0,1.2] || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc10,nil),skc13)),skc8)**. % 7.99/8.18 8622[0:SpR:129.2,4310.0] ssItem(skc10) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 7.99/8.18 8636[0:SSi:8622.1,8622.0,1.0,4.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 7.99/8.18 8760[0:SpL:8636.0,193.8] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) ssItem(skc10) duplicatefreeP(u) || equal(skc10,skc10)* equal(skc8,u)* -> . % 7.99/8.18 8763[0:SpL:8636.0,187.4] ssItem(skc10) ssList(u) ssList(skc13) ssList(app(skc12,cons(skc10,nil))) || equal(skc8,u) -> memberP(u,skc10)*. % 7.99/8.18 8772[0:SSi:8763.3,8763.2,8763.0,92.0,2.0,91.0,4.1,16.0,15.1,12.0,11.1,10.0,14.1,13.0,9.1,80.0,4.1,79.0,4.1,76.0,4.1,75.0,4.0,74.0,4.0,78.0,4.0,77.0,4.0,2575.0,4.2,1.0,4.2] ssList(u) || equal(skc8,u) -> memberP(u,skc10)*. % 7.99/8.18 8780[0:Obv:8760.7] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) duplicatefreeP(u) || equal(skc8,u)* -> . % 7.99/8.18 8781[0:SSi:8780.4,8780.3,8780.2,8780.1,4.0,2.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0,1.0] ssList(u) duplicatefreeP(u) || equal(skc8,u)* -> . % 7.99/8.18 8799[0:Res:8772.2,73.1] ssList(nil) ssItem(skc10) || equal(skc8,nil)** -> . % 7.99/8.18 11092[0:EmS:8781.0,8781.1,6.0,1938.2] singletonP(skc8) ssList(skc8) || equal(skc8,skc8)* -> . % 7.99/8.18 11137[0:Obv:11092.2] singletonP(skc8) ssList(skc8) || -> . % 7.99/8.18 12033[0:SSi:11137.1,6.0] singletonP(skc8) || -> . % 7.99/8.18 12034[0:MRR:64.1,12033.0] || neq(skc9,nil)* -> . % 7.99/8.18 12213[0:Res:423.1,12034.0] ssList(nil) || -> equal(skc9,nil)**. % 7.99/8.18 12216[0:SSi:12213.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> equal(skc9,nil)**. % 7.99/8.18 12217[3:MRR:12216.0,1749.0] || -> . % 7.99/8.18 12221[1:Spt:12217.0,244.1] || -> equal(skc8,nil)**. % 7.99/8.18 12735[1:Rew:12221.0,8799.2] ssList(nil) ssItem(skc10) || equal(nil,nil)* -> . % 7.99/8.18 12736[1:Obv:12735.2] ssList(nil) ssItem(skc10) || -> . % 7.99/8.18 12737[1:SSi:12736.1,12736.0,4.0,16.0,15.0,12.0,11.0,10.0,14.0,13.0,9.0] || -> . % 7.99/8.18 % SZS output end Refutation % 7.99/8.18 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax4 ax38 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax16 ax26 ax58 ax1 ax15 ax23 ax81 ax85 ax67 ax70 ax82 ax3 ax13 % 8.53/8.74 %------------------------------------------------------------------------------