%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC030+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:01:13 EDT 2022 % Result : Theorem 1.62s 1.81s % Output : Refutation 1.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWC030+1 : TPTP v8.1.0. Released v2.4.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n013.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 : Sun Jun 12 00:56:28 EDT 2022 % 0.13/0.34 % CPUTime : % 1.62/1.81 % 1.62/1.81 SPASS V 3.9 % 1.62/1.81 SPASS beiseite: Proof found. % 1.62/1.81 % SZS status Theorem % 1.62/1.81 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.62/1.81 SPASS derived 3704 clauses, backtracked 1419 clauses, performed 42 splits and kept 3504 clauses. % 1.62/1.81 SPASS allocated 101258 KBytes. % 1.62/1.81 SPASS spent 0:00:01.41 on the problem. % 1.62/1.81 0:00:00.04 for the input. % 1.62/1.81 0:00:00.06 for the FLOTTER CNF translation. % 1.62/1.81 0:00:00.02 for inferences. % 1.62/1.81 0:00:00.03 for the backtracking. % 1.62/1.81 0:00:01.10 for the reduction. % 1.62/1.81 % 1.62/1.81 % 1.62/1.81 Here is a proof with depth 6, length 90 : % 1.62/1.81 % SZS output start Refutation % 1.62/1.81 1[0:Inp] || -> ssList(skc9)*. % 1.62/1.81 2[0:Inp] || -> ssList(skc8)*. % 1.62/1.81 3[0:Inp] || -> ssList(skc7)*. % 1.62/1.81 4[0:Inp] || -> ssList(skc6)*. % 1.62/1.81 5[0:Inp] || -> ssItem(skc11)*. % 1.62/1.81 6[0:Inp] || -> ssItem(skc10)*. % 1.62/1.81 53[0:Inp] || equal(skc11,skc10)** -> . % 1.62/1.81 60[0:Inp] || -> equal(app(skc8,skc9),skc7)**. % 1.62/1.81 61[0:Inp] || -> equal(app(skc9,skc8),skc6)**. % 1.62/1.81 62[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 1.62/1.81 71[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 1.62/1.81 73[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 1.62/1.81 74[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 1.62/1.81 75[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 1.62/1.81 76[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.62/1.81 77[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 1.62/1.81 78[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 1.62/1.81 79[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 1.62/1.81 81[0:Inp] || SkP0(skc7,skc6)* SkP0(skc6,skc7) -> . % 1.62/1.81 82[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 1.62/1.81 83[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 1.62/1.81 91[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 1.62/1.81 111[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 1.62/1.81 130[0:Inp] ssList(u) ssList(v) || equal(app(v,u),nil)** -> equal(nil,v). % 1.62/1.81 133[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 1.62/1.81 154[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(app(tl(v),u),tl(app(v,u)))**. % 1.62/1.81 187[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). % 1.62/1.81 243[0:Res:4.0,133.0] ssList(u) || -> equal(skc6,nil) equal(hd(app(skc6,u)),hd(skc6))**. % 1.62/1.81 254[0:Res:4.0,111.0] ssItem(u) || -> equal(hd(cons(u,skc6)),u)**. % 1.62/1.81 266[0:Res:4.0,91.0] ssItem(u) || -> ssList(cons(u,skc6))*. % 1.62/1.81 276[0:Res:4.0,82.0] || -> equal(app(nil,skc6),skc6)**. % 1.62/1.81 284[0:Res:4.0,187.1] ssList(u) || equal(tl(skc6),tl(u))* equal(hd(skc6),hd(u)) -> equal(nil,u) equal(skc6,u) equal(skc6,nil). % 1.62/1.81 408[0:Res:3.0,154.0] ssList(u) || -> equal(skc7,nil) equal(app(tl(skc7),u),tl(app(skc7,u)))**. % 1.62/1.81 447[0:Res:3.0,82.0] || -> equal(app(nil,skc7),skc7)**. % 1.62/1.81 455[0:Res:3.0,187.1] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u) equal(skc7,nil). % 1.62/1.81 545[1:Spt:243.0,243.2] ssList(u) || -> equal(hd(app(skc6,u)),hd(skc6))**. % 1.62/1.81 551[2:Spt:284.5] || -> equal(skc6,nil)**. % 1.62/1.81 552[2:Rew:551.0,545.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 1.62/1.81 568[2:Rew:551.0,266.1] ssItem(u) || -> ssList(cons(u,nil))*. % 1.62/1.81 569[2:Rew:551.0,254.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 1.62/1.81 724[2:Rew:82.1,552.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 1.62/1.81 1144[2:SpR:569.1,724.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 1.62/1.81 1147[2:SSi:1144.1,79.1,78.1,75.1,74.1,73.1,77.1,76.1,568.1] ssItem(u) || -> equal(u,hd(nil))*. % 1.62/1.81 1237[2:SpR:1147.1,1147.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 1.62/1.81 1334[2:EmS:1237.0,5.0] ssItem(u) || -> equal(u,skc11)*. % 1.62/1.81 1356[2:EmS:1334.0,6.0] || -> equal(skc11,skc10)**. % 1.62/1.81 1357[2:MRR:1356.0,53.0] || -> . % 1.62/1.81 1555[2:Spt:1357.0,284.5,551.0] || equal(skc6,nil)** -> . % 1.62/1.81 1556[2:Spt:1357.0,284.0,284.1,284.2,284.3,284.4] ssList(u) || equal(tl(skc6),tl(u))* equal(hd(skc6),hd(u)) -> equal(nil,u) equal(skc6,u). % 1.62/1.81 1575[3:Spt:455.5] || -> equal(skc7,nil)**. % 1.62/1.81 1584[3:Rew:1575.0,60.0] || -> equal(app(skc8,skc9),nil)**. % 1.62/1.81 4432[0:SpL:61.0,130.2] ssList(skc8) ssList(skc9) || equal(skc6,nil) -> equal(skc9,nil)**. % 1.62/1.81 4433[3:SpL:1584.0,130.2] ssList(skc9) ssList(skc8) || equal(nil,nil) -> equal(skc8,nil)**. % 1.62/1.81 4434[3:Obv:4433.2] ssList(skc9) ssList(skc8) || -> equal(skc8,nil)**. % 1.62/1.81 4435[3:SSi:4434.1,4434.0,2.0,1.0] || -> equal(skc8,nil)**. % 1.62/1.81 4437[3:Rew:4435.0,61.0] || -> equal(app(skc9,nil),skc6)**. % 1.62/1.81 4438[3:Rew:4435.0,1584.0] || -> equal(app(nil,skc9),nil)**. % 1.62/1.81 4441[3:SpR:4437.0,83.1] ssList(skc9) || -> equal(skc9,skc6)**. % 1.62/1.81 4445[3:SSi:4441.0,1.0] || -> equal(skc9,skc6)**. % 1.62/1.81 4448[3:Rew:4445.0,4438.0] || -> equal(app(nil,skc6),nil)**. % 1.62/1.81 4449[3:Rew:276.0,4448.0] || -> equal(skc6,nil)**. % 1.62/1.81 4450[3:MRR:4449.0,1555.0] || -> . % 1.62/1.81 4451[3:Spt:4450.0,455.5,1575.0] || equal(skc7,nil)** -> . % 1.62/1.81 4452[3:Spt:4450.0,455.0,455.1,455.2,455.3,455.4] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u). % 1.62/1.81 4534[0:Res:71.1,81.0] || equal(skc7,nil) SkP0(skc6,skc7)* -> . % 1.62/1.81 4535[0:Res:62.0,81.0] || SkP0(skc6,skc7)* -> equal(skc6,nil). % 1.62/1.81 4536[2:MRR:4535.1,1555.0] || SkP0(skc6,skc7)* -> . % 1.62/1.81 4538[2:Res:62.0,4536.0] || -> equal(skc7,nil)**. % 1.62/1.81 4539[3:MRR:4538.0,4451.0] || -> . % 1.62/1.81 4540[1:Spt:4539.0,243.1] || -> equal(skc6,nil)**. % 1.62/1.81 4559[1:Rew:4540.0,61.0] || -> equal(app(skc9,skc8),nil)**. % 1.62/1.81 4675[1:Rew:4540.0,4534.1] || equal(skc7,nil) SkP0(nil,skc7)* -> . % 1.62/1.81 4692[1:Rew:4540.0,4432.2] ssList(skc8) ssList(skc9) || equal(nil,nil) -> equal(skc9,nil)**. % 1.62/1.81 4693[1:Obv:4692.2] ssList(skc8) ssList(skc9) || -> equal(skc9,nil)**. % 1.62/1.81 4694[1:SSi:4693.1,4693.0,1.0,2.0] || -> equal(skc9,nil)**. % 1.62/1.81 4696[1:Rew:4694.0,60.0] || -> equal(app(skc8,nil),skc7)**. % 1.62/1.81 4697[1:Rew:4694.0,4559.0] || -> equal(app(nil,skc8),nil)**. % 1.62/1.81 4793[2:Spt:408.1] || -> equal(skc7,nil)**. % 1.62/1.81 4928[2:Rew:4793.0,4675.0] || equal(nil,nil) SkP0(nil,skc7)* -> . % 1.62/1.81 4960[2:Obv:4928.0] || SkP0(nil,skc7)* -> . % 1.62/1.81 4961[2:Rew:4793.0,4960.0] || SkP0(nil,nil)* -> . % 1.62/1.81 5049[2:Res:71.1,4961.0] || equal(nil,nil)* -> . % 1.62/1.81 5051[2:Obv:5049.0] || -> . % 1.62/1.81 5052[2:Spt:5051.0,408.1,4793.0] || equal(skc7,nil)** -> . % 1.62/1.81 5053[2:Spt:5051.0,408.0,408.2] ssList(u) || -> equal(app(tl(skc7),u),tl(app(skc7,u)))**. % 1.62/1.81 5088[1:SpR:4696.0,83.1] ssList(skc8) || -> equal(skc8,skc7)**. % 1.62/1.81 5092[1:SSi:5088.0,2.0] || -> equal(skc8,skc7)**. % 1.62/1.81 5095[1:Rew:5092.0,4697.0] || -> equal(app(nil,skc7),nil)**. % 1.62/1.81 5096[1:Rew:447.0,5095.0] || -> equal(skc7,nil)**. % 1.62/1.81 5097[2:MRR:5096.0,5052.0] || -> . % 1.62/1.81 % SZS output end Refutation % 1.62/1.81 Formulae used in the proof : co1 ax2 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax84 ax16 ax23 ax83 ax85 ax86 ax77 % 1.62/1.81 %------------------------------------------------------------------------------