%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC165+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:11 EDT 2022 % Result : Theorem 13.93s 14.12s % Output : Refutation 14.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SWC165+1 : TPTP v8.1.0. Released v2.4.0. % 0.10/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n016.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 12 12:41:43 EDT 2022 % 0.13/0.33 % CPUTime : % 13.93/14.12 % 13.93/14.12 SPASS V 3.9 % 13.93/14.12 SPASS beiseite: Proof found. % 13.93/14.12 % SZS status Theorem % 13.93/14.12 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.93/14.12 SPASS derived 10173 clauses, backtracked 5533 clauses, performed 48 splits and kept 8623 clauses. % 13.93/14.12 SPASS allocated 113635 KBytes. % 13.93/14.12 SPASS spent 0:0:13.76 on the problem. % 13.93/14.12 0:00:00.04 for the input. % 13.93/14.12 0:00:00.07 for the FLOTTER CNF translation. % 13.93/14.12 0:00:00.12 for inferences. % 13.93/14.12 0:00:00.47 for the backtracking. % 13.93/14.12 0:0:12.85 for the reduction. % 13.93/14.12 % 13.93/14.12 % 13.93/14.12 Here is a proof with depth 6, length 130 : % 13.93/14.12 % SZS output start Refutation % 13.93/14.12 1[0:Inp] || -> ssList(skc13)*. % 13.93/14.12 2[0:Inp] || -> ssList(skc12)*. % 13.93/14.12 3[0:Inp] || -> ssItem(skc11)*. % 13.93/14.12 4[0:Inp] || -> ssItem(skc10)*. % 13.93/14.12 5[0:Inp] || -> ssList(skc9)*. % 13.93/14.12 6[0:Inp] || -> ssList(skc8)*. % 13.93/14.12 7[0:Inp] || -> ssItem(skc15)*. % 13.93/14.12 8[0:Inp] || -> ssItem(skc14)*. % 13.93/14.12 9[0:Inp] || -> ssList(nil)*. % 13.93/14.12 10[0:Inp] || -> cyclefreeP(nil)*. % 13.93/14.12 11[0:Inp] || -> totalorderP(nil)*. % 13.93/14.12 12[0:Inp] || -> strictorderP(nil)*. % 13.93/14.12 13[0:Inp] || -> totalorderedP(nil)*. % 13.93/14.12 14[0:Inp] || -> strictorderedP(nil)*. % 13.93/14.12 15[0:Inp] || -> duplicatefreeP(nil)*. % 13.93/14.12 16[0:Inp] || -> equalelemsP(nil)*. % 13.93/14.12 17[0:Inp] || -> ssItem(skf51(u))*. % 13.93/14.12 57[0:Inp] || -> ssItem(skf46(u,v))*. % 13.93/14.12 58[0:Inp] || neq(skc10,skc11)* -> . % 13.93/14.12 59[0:Inp] || equal(skc15,skc14)** -> . % 13.93/14.12 74[0:Inp] || SkP0(skc9,skc8)* -> equal(nil,skc9). % 13.93/14.12 75[0:Inp] || SkP0(skc9,skc8)* -> equal(nil,skc8). % 13.93/14.12 77[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 13.93/14.12 78[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 13.93/14.12 79[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 13.93/14.12 80[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 13.93/14.12 81[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 13.93/14.12 82[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 13.93/14.12 83[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 13.93/14.12 85[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 13.93/14.12 91[0:Inp] || -> SkP0(u,v) equal(cons(skf46(u,v),nil),v)**. % 13.93/14.12 95[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 13.93/14.12 96[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 13.93/14.12 110[0:Inp] ssItem(u) ssItem(v) || -> neq(v,u)* equal(v,u). % 13.93/14.12 111[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf51(u),nil),u)**. % 13.93/14.12 113[0:Inp] ssItem(u) ssList(v) || equal(cons(u,v),v)** -> . % 13.93/14.12 115[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 13.93/14.12 117[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 13.93/14.12 127[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)* -> singletonP(u)*. % 13.93/14.12 134[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 13.93/14.12 139[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 13.93/14.12 167[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 13.93/14.12 195[0:Inp] ssList(u) ssList(v) || equal(tl(u),tl(v))* equal(hd(u),hd(v)) -> equal(u,v) equal(nil,v) equal(nil,u). % 13.93/14.12 200[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)* -> . % 13.93/14.12 204[0:Rew:75.1,74.1] || SkP0(skc9,skc8)* -> equal(skc9,skc8). % 13.93/14.12 252[0:Res:6.0,139.0] ssList(u) || -> equal(nil,skc8) equal(hd(app(skc8,u)),hd(skc8))**. % 13.93/14.12 261[0:Res:6.0,113.0] ssItem(u) || equal(cons(u,skc8),skc8)** -> . % 13.93/14.12 263[0:Res:6.0,115.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 13.93/14.12 275[0:Res:6.0,95.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 13.93/14.12 293[0:Res:6.0,195.1] ssList(u) || equal(tl(skc8),tl(u))* equal(hd(skc8),hd(u)) -> equal(nil,u) equal(skc8,u) equal(nil,skc8). % 13.93/14.12 423[0:Res:5.0,139.0] ssList(u) || -> equal(nil,skc9) equal(hd(app(skc9,u)),hd(skc9))**. % 13.93/14.12 464[0:Res:5.0,195.1] ssList(u) || equal(tl(skc9),tl(u))* equal(hd(skc9),hd(u)) -> equal(nil,u) equal(skc9,u) equal(nil,skc9). % 13.93/14.12 556[1:Spt:423.0,423.2] ssList(u) || -> equal(hd(app(skc9,u)),hd(skc9))**. % 13.93/14.12 558[2:Spt:252.0,252.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 13.93/14.12 564[3:Spt:464.5] || -> equal(nil,skc9)**. % 13.93/14.12 661[3:Rew:564.0,85.1] ssList(u) || -> equal(app(skc9,u),u)**. % 13.93/14.12 720[3:Rew:661.1,556.1] ssList(u) || -> equal(hd(u),hd(skc9))*. % 13.93/14.12 1509[3:SpR:720.1,263.1] ssList(cons(u,skc8)) ssItem(u) || -> equal(hd(skc9),u)*. % 13.93/14.12 1514[3:SSi:1509.0,275.1] ssItem(u) || -> equal(hd(skc9),u)*. % 13.93/14.12 1516[3:SpR:1514.1,1514.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 13.93/14.12 1695[3:EmS:1516.0,8.0] ssItem(u) || -> equal(skc14,u)*. % 13.93/14.12 1781[3:EmS:1695.0,7.0] || -> equal(skc15,skc14)**. % 13.93/14.12 1784[3:MRR:1781.0,59.0] || -> . % 13.93/14.12 2002[3:Spt:1784.0,464.5,564.0] || equal(nil,skc9)** -> . % 13.93/14.12 2003[3:Spt:1784.0,464.0,464.1,464.2,464.3,464.4] ssList(u) || equal(tl(skc9),tl(u))* equal(hd(skc9),hd(u)) -> equal(nil,u) equal(skc9,u). % 13.93/14.12 2027[4:Spt:293.5] || -> equal(nil,skc8)**. % 13.93/14.12 2044[4:Rew:2027.0,2002.0] || equal(skc9,skc8)** -> . % 13.93/14.12 2063[4:Rew:2027.0,77.1] ssItem(u) || -> cyclefreeP(cons(u,skc8))*. % 13.93/14.12 2064[4:Rew:2027.0,78.1] ssItem(u) || -> totalorderP(cons(u,skc8))*. % 13.93/14.12 2065[4:Rew:2027.0,79.1] ssItem(u) || -> strictorderP(cons(u,skc8))*. % 13.93/14.12 2066[4:Rew:2027.0,80.1] ssItem(u) || -> totalorderedP(cons(u,skc8))*. % 13.93/14.12 2067[4:Rew:2027.0,81.1] ssItem(u) || -> strictorderedP(cons(u,skc8))*. % 13.93/14.12 2068[4:Rew:2027.0,82.1] ssItem(u) || -> duplicatefreeP(cons(u,skc8))*. % 13.93/14.12 2069[4:Rew:2027.0,83.1] ssItem(u) || -> equalelemsP(cons(u,skc8))*. % 13.93/14.12 2075[4:Rew:2027.0,85.1] ssList(u) || -> equal(app(skc8,u),u)**. % 13.93/14.12 2104[4:Rew:2027.0,91.1] || -> SkP0(u,v) equal(cons(skf46(u,v),skc8),v)**. % 13.93/14.12 2125[4:MRR:204.1,2044.0] || SkP0(skc9,skc8)* -> . % 13.93/14.12 2161[4:Rew:2075.1,558.1] ssList(u) || -> equal(hd(u),hd(skc8))*. % 13.93/14.12 2232[4:SpR:2161.1,263.1] ssList(cons(u,skc8)) ssItem(u) || -> equal(hd(skc8),u)*. % 13.93/14.12 2242[4:SSi:2232.0,275.1,2063.1,2064.1,2065.1,2066.1,2067.1,2068.1,2069.1] ssItem(u) || -> equal(hd(skc8),u)*. % 13.93/14.12 2412[4:SpR:2104.1,263.1] ssItem(skf46(u,v)) || -> SkP0(u,v) equal(skf46(u,v),hd(v))**. % 13.93/14.12 2434[4:SSi:2412.0,57.0] || -> SkP0(u,v) equal(skf46(u,v),hd(v))**. % 13.93/14.12 2435[4:Rew:2434.1,2104.1] || -> SkP0(u,v)* equal(cons(hd(v),skc8),v)**. % 13.93/14.12 2458[4:SpR:2242.1,2435.1] ssItem(u) || -> SkP0(v,skc8)* equal(cons(u,skc8),skc8)**. % 13.93/14.12 2462[4:MRR:2458.2,261.1] ssItem(u) || -> SkP0(v,skc8)*. % 13.93/14.12 2492[4:EmS:2462.0,4.0] || -> SkP0(u,skc8)*. % 13.93/14.12 2515[4:UnC:2492.0,2125.0] || -> . % 13.93/14.12 2516[4:Spt:2515.0,293.5,2027.0] || equal(nil,skc8)** -> . % 13.93/14.12 2517[4:Spt:2515.0,293.0,293.1,293.2,293.3,293.4] ssList(u) || equal(tl(skc8),tl(u))* equal(hd(skc8),hd(u)) -> equal(nil,u) equal(skc8,u). % 13.93/14.12 2523[4:MRR:75.1,2516.0] || SkP0(skc9,skc8)* -> . % 13.93/14.12 2633[0:SpR:91.1,83.1] ssItem(skf46(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 13.93/14.12 2641[0:SSi:2633.0,57.0] || -> SkP0(u,v)* equalelemsP(v). % 13.93/14.12 2649[4:Res:2641.0,2523.0] || -> equalelemsP(skc8)*. % 13.93/14.12 2717[0:SpR:111.2,82.1] ssList(u) singletonP(u) ssItem(skf51(u)) || -> duplicatefreeP(u)*. % 13.93/14.12 2728[0:SSi:2717.2,17.0] ssList(u) singletonP(u) || -> duplicatefreeP(u)*. % 13.93/14.12 2791[0:SpR:91.1,115.2] ssItem(skf46(u,v)) ssList(nil) || -> SkP0(u,v) equal(skf46(u,v),hd(v))**. % 13.93/14.12 2795[0:SSi:2791.1,2791.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0,9.0,57.0] || -> SkP0(u,v) equal(skf46(u,v),hd(v))**. % 13.93/14.12 2796[0:Rew:2795.1,91.1] || -> SkP0(u,v)* equal(cons(hd(v),nil),v)**. % 13.93/14.12 2880[0:SpR:2795.1,57.0] || -> SkP0(u,v)* ssItem(hd(v)). % 13.93/14.12 2927[0:Res:110.2,58.0] ssItem(skc11) ssItem(skc10) || -> equal(skc11,skc10)**. % 13.93/14.12 2928[0:SSi:2927.1,2927.0,4.0,3.0] || -> equal(skc11,skc10)**. % 13.93/14.12 2931[0:Rew:2928.0,117.0] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc10,nil)),skc13),skc8)**. % 13.93/14.12 3351[0:EqR:127.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 13.93/14.12 3356[0:SSi:3351.0,83.0,82.0,81.0,80.0,79.0,78.0,77.0,95.0,16.2,15.1,14.1,13.1,12.1,11.1,10.1,9.1] ssItem(u) || -> singletonP(cons(u,nil))*. % 13.93/14.12 3410[0:SpR:2796.1,3356.1] ssItem(hd(u)) || -> SkP0(v,u)* singletonP(u). % 13.93/14.12 3412[0:MRR:3410.0,2880.1] || -> SkP0(u,v)* singletonP(v). % 13.93/14.12 3415[4:Res:3412.0,2523.0] || -> singletonP(skc8)*. % 13.93/14.12 5679[0:SpR:167.3,2931.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)**. % 13.93/14.12 5747[0:SSi:5679.2,5679.1,5679.0,96.0,2.0,83.0,4.0,82.0,4.0,81.0,4.0,80.0,4.0,79.2,4.0,78.1,4.0,77.1,4.0,3356.1,4.0,95.1,4.0,16.1,15.0,14.1,13.0,12.1,11.0,10.1,9.0,83.0,4.0,82.0,4.0,81.0,4.0,80.0,4.0,79.2,4.0,78.1,4.0,77.1,4.0,3356.1,4.0,95.1,4.0,16.1,15.0,14.1,13.0,12.1,11.0,10.1,9.0,1.2] || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc10,nil),skc13)),skc8)**. % 13.93/14.12 10664[0:SpR:134.2,5747.0] ssItem(skc10) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 13.93/14.12 10678[0:SSi:10664.1,10664.0,1.0,4.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc10,skc13)),skc8)**. % 14.94/15.11 13936[0:SpL:10678.0,200.8] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) ssItem(skc10) duplicatefreeP(u) || equal(skc10,skc10)* equal(skc8,u)* -> . % 14.94/15.11 13948[0:Obv:13936.7] ssList(u) ssList(skc13) ssList(nil) ssList(skc12) ssItem(skc10) duplicatefreeP(u) || equal(skc8,u)* -> . % 14.94/15.11 13949[0:SSi:13948.4,13948.3,13948.2,13948.1,4.0,2.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0,9.0,1.0] ssList(u) duplicatefreeP(u) || equal(skc8,u)* -> . % 14.94/15.11 13964[0:EmS:13949.0,13949.1,9.0,15.0] || equal(nil,skc8)** -> . % 14.94/15.11 14018[0:EmS:13949.0,13949.1,6.0,2728.2] singletonP(skc8) ssList(skc8) || equal(skc8,skc8)* -> . % 14.94/15.11 14021[0:Obv:14018.2] singletonP(skc8) ssList(skc8) || -> . % 14.94/15.11 15606[0:Obv:14018.2] singletonP(skc8) ssList(skc8) || -> . % 14.94/15.11 15607[4:SSi:15606.1,6.0,2649.0] singletonP(skc8) || -> . % 14.94/15.11 15608[4:MRR:15607.0,3415.0] || -> . % 14.94/15.11 15787[2:Spt:15608.0,252.1] || -> equal(nil,skc8)**. % 14.94/15.11 16235[2:Rew:15787.0,13964.0] || equal(skc8,skc8)* -> . % 14.94/15.11 16236[2:Obv:16235.0] || -> . % 14.94/15.11 16237[0:SSi:14021.1,6.0] singletonP(skc8) || -> . % 14.94/15.11 17317[1:Spt:16236.0,423.1] || -> equal(nil,skc9)**. % 14.94/15.11 17334[1:Rew:17317.0,13964.0] || equal(skc9,skc8)** -> . % 14.94/15.11 17374[1:Rew:17317.0,75.1] || SkP0(skc9,skc8)* -> equal(skc9,skc8). % 14.94/15.11 17375[1:MRR:17374.1,17334.0] || SkP0(skc9,skc8)* -> . % 14.94/15.11 18375[1:Res:3412.0,17375.0] || -> singletonP(skc8)*. % 14.94/15.11 18385[1:MRR:18375.0,16237.0] || -> . % 14.94/15.11 % SZS output end Refutation % 14.94/15.11 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax4 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax16 ax26 ax1 ax18 ax23 ax81 ax85 ax82 ax77 ax13 % 14.94/15.11 %------------------------------------------------------------------------------