%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC178+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % 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 : Tue Jul 19 22:02:16 EDT 2022 % Result : Theorem 7.87s 8.07s % Output : Refutation 7.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC178+1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.34 % Computer : n020.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 21:29:05 EDT 2022 % 0.12/0.34 % CPUTime : % 7.87/8.07 % 7.87/8.07 SPASS V 3.9 % 7.87/8.07 SPASS beiseite: Proof found. % 7.87/8.07 % SZS status Theorem % 7.87/8.07 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 7.87/8.07 SPASS derived 7996 clauses, backtracked 2214 clauses, performed 39 splits and kept 5274 clauses. % 7.87/8.07 SPASS allocated 109638 KBytes. % 7.87/8.07 SPASS spent 0:00:07.72 on the problem. % 7.87/8.07 0:00:00.04 for the input. % 7.87/8.07 0:00:00.07 for the FLOTTER CNF translation. % 7.87/8.07 0:00:00.10 for inferences. % 7.87/8.07 0:00:00.17 for the backtracking. % 7.87/8.07 0:00:07.14 for the reduction. % 7.87/8.07 % 7.87/8.07 % 7.87/8.07 Here is a proof with depth 6, length 107 : % 7.87/8.07 % SZS output start Refutation % 7.87/8.07 1[0:Inp] || -> ssList(skc13)*. % 7.87/8.07 2[0:Inp] || -> ssList(skc12)*. % 7.87/8.07 3[0:Inp] || -> ssItem(skc11)*. % 7.87/8.07 4[0:Inp] || -> ssItem(skc10)*. % 7.87/8.07 5[0:Inp] || -> ssList(skc9)*. % 7.87/8.07 6[0:Inp] || -> ssList(skc8)*. % 7.87/8.07 7[0:Inp] || -> ssItem(skc15)*. % 7.87/8.07 8[0:Inp] || -> ssItem(skc14)*. % 7.87/8.07 9[0:Inp] || -> ssList(nil)*. % 7.87/8.07 10[0:Inp] || -> cyclefreeP(nil)*. % 7.87/8.07 11[0:Inp] || -> totalorderP(nil)*. % 7.87/8.07 12[0:Inp] || -> strictorderP(nil)*. % 7.87/8.07 13[0:Inp] || -> totalorderedP(nil)*. % 7.87/8.07 14[0:Inp] || -> strictorderedP(nil)*. % 7.87/8.07 15[0:Inp] || -> duplicatefreeP(nil)*. % 7.87/8.07 16[0:Inp] || -> equalelemsP(nil)*. % 7.87/8.07 17[0:Inp] || -> segmentP(skc9,skc8)*. % 7.87/8.07 18[0:Inp] || -> ssItem(skf45(u))*. % 7.87/8.07 56[0:Inp] || neq(skc10,skc11)* -> . % 7.87/8.07 57[0:Inp] || equal(skc15,skc14)** -> . % 7.87/8.07 64[0:Inp] || neq(skc9,nil)* -> singletonP(skc8). % 7.87/8.07 73[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 7.87/8.07 74[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 7.87/8.07 75[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 7.87/8.07 76[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 7.87/8.07 77[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 7.87/8.07 78[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 7.87/8.07 79[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 7.87/8.07 80[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 7.87/8.07 82[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 7.87/8.07 91[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 7.87/8.07 92[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 7.87/8.07 97[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 7.87/8.07 106[0:Inp] ssItem(u) ssItem(v) || -> neq(v,u)* equal(v,u). % 7.87/8.07 107[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf45(u),nil),u)**. % 7.87/8.07 108[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 7.87/8.07 111[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 7.87/8.07 113[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 7.87/8.07 122[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 7.87/8.07 129[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 7.87/8.07 134[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 7.87/8.07 153[0:Inp] ssList(u) ssItem(v) || totalorderedP(cons(v,u))* -> leq(v,hd(u)) equal(nil,u). % 7.87/8.07 154[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 7.87/8.07 160[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 7.87/8.07 187[0:Inp] ssItem(u) ssList(v) ssList(w) ssList(x) || equal(app(x,cons(u,w)),v)*+ -> memberP(v,u)*. % 7.87/8.07 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.87/8.07 244[0:Res:6.0,134.0] ssList(u) || -> equal(skc8,nil) equal(hd(app(skc8,u)),hd(skc8))**. % 7.87/8.07 255[0:Res:6.0,111.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 7.87/8.07 267[0:Res:6.0,91.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 7.87/8.07 273[0:Res:6.0,97.0] || segmentP(nil,skc8)* -> equal(skc8,nil). % 7.87/8.07 308[0:Res:6.0,154.1] ssItem(u) || strictorderedP(cons(u,skc8))* -> lt(u,hd(skc8)) equal(skc8,nil). % 7.87/8.07 423[0:Res:5.0,108.0] ssList(u) || -> neq(skc9,u)* equal(skc9,u). % 7.87/8.07 478[0:Res:5.0,153.1] ssItem(u) || totalorderedP(cons(u,skc9))* -> leq(u,hd(skc9)) equal(skc9,nil). % 7.87/8.07 544[1:Spt:244.0,244.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 7.87/8.07 552[2:Spt:308.3] || -> equal(skc8,nil)**. % 7.87/8.07 553[2:Rew:552.0,544.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 7.87/8.07 571[2:Rew:552.0,267.1] ssItem(u) || -> ssList(cons(u,nil))*. % 7.87/8.07 572[2:Rew:552.0,255.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 7.87/8.07 726[2:Rew:82.1,553.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 7.87/8.07 1177[2:SpR:572.1,726.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 7.87/8.07 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.87/8.07 1246[2:SpR:1180.1,1180.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 7.87/8.07 1286[2:EmS:1246.0,3.0] ssItem(u) || -> equal(u,skc11)*. % 7.87/8.07 1309[2:EmS:1286.0,4.0] || -> equal(skc11,skc10)**. % 7.87/8.07 1310[2:EmS:1286.0,7.0] || -> equal(skc15,skc11)**. % 7.87/8.07 1311[2:EmS:1286.0,8.0] || -> equal(skc14,skc11)**. % 7.87/8.07 1316[2:Rew:1309.0,1310.0] || -> equal(skc15,skc10)**. % 7.87/8.07 1318[2:Rew:1316.0,57.0] || equal(skc14,skc10)** -> . % 7.87/8.07 1320[2:Rew:1309.0,1311.0] || -> equal(skc14,skc10)**. % 7.87/8.07 1439[2:Rew:1320.0,1318.0] || equal(skc10,skc10)* -> . % 7.87/8.07 1440[2:Obv:1439.0] || -> . % 7.87/8.07 1470[2:Spt:1440.0,308.3,552.0] || equal(skc8,nil)** -> . % 7.87/8.07 1471[2:Spt:1440.0,308.0,308.1,308.2] ssItem(u) || strictorderedP(cons(u,skc8))* -> lt(u,hd(skc8)). % 7.87/8.07 1474[2:MRR:273.1,1470.0] || segmentP(nil,skc8)* -> . % 7.87/8.07 1485[3:Spt:478.3] || -> equal(skc9,nil)**. % 7.87/8.07 1493[3:Rew:1485.0,17.0] || -> segmentP(nil,skc8)*. % 7.87/8.07 1638[3:MRR:1493.0,1474.0] || -> . % 7.87/8.07 1749[3:Spt:1638.0,478.3,1485.0] || equal(skc9,nil)** -> . % 7.87/8.07 1750[3:Spt:1638.0,478.0,478.1,478.2] ssItem(u) || totalorderedP(cons(u,skc9))* -> leq(u,hd(skc9)). % 7.87/8.07 1925[0:SpR:107.2,79.1] ssList(u) singletonP(u) ssItem(skf45(u)) || -> duplicatefreeP(u)*. % 7.87/8.07 1938[0:SSi:1925.2,18.0] ssList(u) singletonP(u) || -> duplicatefreeP(u)*. % 7.87/8.07 2129[0:Res:106.2,56.0] ssItem(skc11) ssItem(skc10) || -> equal(skc11,skc10)**. % 7.87/8.07 2134[0:SSi:2129.1,2129.0,4.0,3.0] || -> equal(skc11,skc10)**. % 7.87/8.07 2137[0:Rew:2134.0,113.0] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc10,nil)),skc13),skc8)**. % 7.87/8.07 2570[0:EqR:122.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 7.87/8.07 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.87/8.07 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.87/8.07 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.87/8.07 8622[0:SpR:129.2,4310.0] ssItem(skc10) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 7.87/8.07 8636[0:SSi:8622.1,8622.0,1.0,4.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 7.87/8.07 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.87/8.07 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.87/8.07 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.87/8.07 8780[0:Obv:8760.7] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) duplicatefreeP(u) || equal(skc8,u)* -> . % 7.87/8.07 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.87/8.07 8799[0:Res:8772.2,73.1] ssList(nil) ssItem(skc10) || equal(skc8,nil)** -> . % 7.87/8.07 11092[0:EmS:8781.0,8781.1,6.0,1938.2] singletonP(skc8) ssList(skc8) || equal(skc8,skc8)* -> . % 7.87/8.07 11137[0:Obv:11092.2] singletonP(skc8) ssList(skc8) || -> . % 7.87/8.07 12033[0:SSi:11137.1,6.0] singletonP(skc8) || -> . % 7.87/8.07 12034[0:MRR:64.1,12033.0] || neq(skc9,nil)* -> . % 7.87/8.07 12213[0:Res:423.1,12034.0] ssList(nil) || -> equal(skc9,nil)**. % 7.87/8.07 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.87/8.07 12217[3:MRR:12216.0,1749.0] || -> . % 7.87/8.07 12221[1:Spt:12217.0,244.1] || -> equal(skc8,nil)**. % 7.87/8.07 12735[1:Rew:12221.0,8799.2] ssList(nil) ssItem(skc10) || equal(nil,nil)* -> . % 7.87/8.07 12736[1:Obv:12735.2] ssList(nil) ssItem(skc10) || -> . % 7.87/8.07 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.87/8.07 % SZS output end Refutation % 7.87/8.07 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.45/8.63 %------------------------------------------------------------------------------