%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC320+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:03:17 EDT 2022 % Result : Theorem 87.90s 88.13s % Output : Refutation 87.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWC320+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jun 11 23:45:49 EDT 2022 % 0.12/0.33 % CPUTime : % 87.90/88.13 % 87.90/88.13 SPASS V 3.9 % 87.90/88.13 SPASS beiseite: Proof found. % 87.90/88.13 % SZS status Theorem % 87.90/88.13 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 87.90/88.13 SPASS derived 29721 clauses, backtracked 10239 clauses, performed 42 splits and kept 15840 clauses. % 87.90/88.13 SPASS allocated 146118 KBytes. % 87.90/88.13 SPASS spent 0:1:13.19 on the problem. % 87.90/88.13 0:00:00.04 for the input. % 87.90/88.13 0:00:00.07 for the FLOTTER CNF translation. % 87.90/88.13 0:00:00.53 for inferences. % 87.90/88.13 0:00:02.94 for the backtracking. % 87.90/88.13 0:01:09.19 for the reduction. % 87.90/88.13 % 87.90/88.13 % 87.90/88.13 Here is a proof with depth 6, length 91 : % 87.90/88.13 % SZS output start Refutation % 87.90/88.13 1[0:Inp] || -> ssList(skc9)*. % 87.90/88.13 2[0:Inp] || -> ssItem(skc8)*. % 87.90/88.13 3[0:Inp] || -> ssList(skc7)*. % 87.90/88.13 5[0:Inp] || -> ssItem(skc11)*. % 87.90/88.13 6[0:Inp] || -> ssItem(skc10)*. % 87.90/88.13 7[0:Inp] || -> ssList(nil)*. % 87.90/88.13 8[0:Inp] || -> cyclefreeP(nil)*. % 87.90/88.13 9[0:Inp] || -> totalorderP(nil)*. % 87.90/88.13 10[0:Inp] || -> strictorderP(nil)*. % 87.90/88.13 11[0:Inp] || -> totalorderedP(nil)*. % 87.90/88.13 12[0:Inp] || -> strictorderedP(nil)*. % 87.90/88.13 13[0:Inp] || -> duplicatefreeP(nil)*. % 87.90/88.13 14[0:Inp] || -> equalelemsP(nil)*. % 87.90/88.13 53[0:Inp] || equal(skc11,skc10)** -> . % 87.90/88.13 60[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 87.90/88.13 69[0:Inp] || equal(skc7,nil)** -> equal(skc6,nil). % 87.90/88.13 70[0:Inp] || SkP0(skc6,skc7) -> neq(skc7,nil)*. % 87.90/88.13 71[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 87.90/88.13 73[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 87.90/88.13 74[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 87.90/88.13 75[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 87.90/88.13 76[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 87.90/88.13 77[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 87.90/88.13 78[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 87.90/88.13 79[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 87.90/88.13 81[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 87.90/88.13 90[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 87.90/88.13 98[0:Inp] || neq(skc7,nil) -> equal(app(cons(skc8,nil),skc9),skc6)**. % 87.90/88.13 99[0:Inp] || neq(skc7,nil) -> equal(app(skc9,cons(skc8,nil)),skc7)**. % 87.90/88.13 112[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 87.90/88.13 123[0:Inp] ssList(u) ssList(v) || equal(v,u) neq(v,u)* -> . % 87.90/88.13 129[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 87.90/88.13 134[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 87.90/88.13 154[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 87.90/88.13 188[0:Inp] ssItem(u) ssList(v) || equal(app(cons(u,nil),v),skc6)** equal(app(v,cons(u,nil)),skc7)** SkP0(skc6,skc7) -> . % 87.90/88.13 203[0:Rew:129.2,188.2] ssList(u) ssItem(v) || SkP0(skc6,skc7) equal(cons(v,u),skc6) equal(app(u,cons(v,nil)),skc7)** -> . % 87.90/88.13 418[0:Res:3.0,134.0] ssList(u) || -> equal(skc7,nil) equal(hd(app(skc7,u)),hd(skc7))**. % 87.90/88.13 429[0:Res:3.0,112.0] ssItem(u) || -> equal(hd(cons(u,skc7)),u)**. % 87.90/88.13 441[0:Res:3.0,90.0] ssItem(u) || -> ssList(cons(u,skc7))*. % 87.90/88.13 483[0:Res:3.0,154.1] ssItem(u) || strictorderedP(cons(u,skc7))* -> lt(u,hd(skc7)) equal(skc7,nil). % 87.90/88.13 548[1:Spt:418.0,418.2] ssList(u) || -> equal(hd(app(skc7,u)),hd(skc7))**. % 87.90/88.13 556[2:Spt:203.0,203.1,203.3,203.4] ssList(u) ssItem(v) || equal(cons(v,u),skc6) equal(app(u,cons(v,nil)),skc7)** -> . % 87.90/88.13 559[3:Spt:483.3] || -> equal(skc7,nil)**. % 87.90/88.13 560[3:Rew:559.0,548.1] ssList(u) || -> equal(hd(app(nil,u)),hd(nil))**. % 87.90/88.13 583[3:Rew:559.0,441.1] ssItem(u) || -> ssList(cons(u,nil))*. % 87.90/88.13 584[3:Rew:559.0,429.1] ssItem(u) || -> equal(hd(cons(u,nil)),u)**. % 87.90/88.13 909[3:Rew:81.1,560.1] ssList(u) || -> equal(hd(u),hd(nil))*. % 87.90/88.13 1210[3:SpR:584.1,909.1] ssItem(u) ssList(cons(u,nil)) || -> equal(u,hd(nil))*. % 87.90/88.13 1213[3:SSi:1210.1,79.1,78.1,75.1,74.1,73.1,77.1,76.1,583.1] ssItem(u) || -> equal(u,hd(nil))*. % 87.90/88.13 1283[3:SpR:1213.1,1213.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 87.90/88.13 1321[3:EmS:1283.0,2.0] ssItem(u) || -> equal(u,skc8)*. % 87.90/88.13 1343[3:EmS:1321.0,5.0] || -> equal(skc11,skc8)**. % 87.90/88.13 1344[3:EmS:1321.0,6.0] || -> equal(skc10,skc8)**. % 87.90/88.13 1346[3:Rew:1343.0,53.0] || equal(skc10,skc8)** -> . % 87.90/88.13 1453[3:Rew:1344.0,1346.0] || equal(skc8,skc8)* -> . % 87.90/88.13 1454[3:Obv:1453.0] || -> . % 87.90/88.13 1483[3:Spt:1454.0,483.3,559.0] || equal(skc7,nil)** -> . % 87.90/88.13 1484[3:Spt:1454.0,483.0,483.1,483.2] ssItem(u) || strictorderedP(cons(u,skc7))* -> lt(u,hd(skc7)). % 87.90/88.13 2435[4:Spt:70.1] || -> neq(skc7,nil)*. % 87.90/88.13 2436[4:MRR:99.0,2435.0] || -> equal(app(skc9,cons(skc8,nil)),skc7)**. % 87.90/88.13 2437[4:MRR:98.0,2435.0] || -> equal(app(cons(skc8,nil),skc9),skc6)**. % 87.90/88.13 3368[4:SpR:129.2,2437.0] ssItem(skc8) ssList(skc9) || -> equal(cons(skc8,skc9),skc6)**. % 87.90/88.13 3379[4:SSi:3368.1,3368.0,1.0,2.0] || -> equal(cons(skc8,skc9),skc6)**. % 87.90/88.13 44114[4:SpL:2436.0,556.3] ssList(skc9) ssItem(skc8) || equal(cons(skc8,skc9),skc6)** equal(skc7,skc7) -> . % 87.90/88.13 46852[4:Obv:44114.3] ssList(skc9) ssItem(skc8) || equal(cons(skc8,skc9),skc6)** -> . % 87.90/88.13 46853[4:Rew:3379.0,46852.2] ssList(skc9) ssItem(skc8) || equal(skc6,skc6)* -> . % 87.90/88.13 46854[4:Obv:46853.2] ssList(skc9) ssItem(skc8) || -> . % 87.90/88.13 46855[4:SSi:46854.1,46854.0,2.0,1.0] || -> . % 87.90/88.13 47790[4:Spt:46855.0,70.1,2435.0] || neq(skc7,nil)* -> . % 87.90/88.13 47791[4:Spt:46855.0,70.0] || SkP0(skc6,skc7)* -> . % 87.90/88.13 49108[4:Res:60.0,47791.0] || -> equal(skc7,nil)**. % 87.90/88.13 49109[4:MRR:49108.0,1483.0] || -> . % 87.90/88.13 49110[2:Spt:49109.0,203.2] || SkP0(skc6,skc7)* -> . % 87.90/88.13 49421[2:Res:71.1,49110.0] || equal(skc6,nil)** -> . % 87.90/88.13 49422[2:Res:60.0,49110.0] || -> equal(skc7,nil)**. % 87.90/88.13 50581[2:Rew:49422.0,69.0] || equal(nil,nil) -> equal(skc6,nil)**. % 87.90/88.13 50619[2:Obv:50581.0] || -> equal(skc6,nil)**. % 87.90/88.13 50620[2:MRR:50619.0,49421.0] || -> . % 87.90/88.13 51874[1:Spt:50620.0,418.1] || -> equal(skc7,nil)**. % 87.90/88.13 51886[1:Rew:51874.0,70.1,51874.0,70.0] || SkP0(skc6,nil) -> neq(nil,nil)*. % 87.90/88.13 51898[1:Rew:51874.0,69.0] || equal(nil,nil) -> equal(skc6,nil)**. % 87.90/88.13 51899[1:Obv:51898.0] || -> equal(skc6,nil)**. % 87.90/88.13 52843[1:Rew:51899.0,51886.0] || SkP0(nil,nil) -> neq(nil,nil)*. % 87.90/88.13 55716[2:Spt:52843.0] || SkP0(nil,nil)* -> . % 87.90/88.13 55717[2:Res:71.1,55716.0] || equal(nil,nil)* -> . % 87.90/88.13 55719[2:Obv:55717.0] || -> . % 87.90/88.13 55720[2:Spt:55719.0,52843.0,55716.0] || -> SkP0(nil,nil)*. % 87.90/88.13 55721[2:Spt:55719.0,52843.1] || -> neq(nil,nil)*. % 87.90/88.13 55724[2:Res:55721.0,123.3] ssList(nil) ssList(nil) || equal(nil,nil)* -> . % 87.90/88.13 55726[2:Obv:55724.2] ssList(nil) || -> . % 87.90/88.13 55727[2:SSi:55726.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> . % 87.90/88.13 % SZS output end Refutation % 87.90/88.13 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax16 ax23 ax15 ax81 ax85 ax70 % 87.90/88.13 %------------------------------------------------------------------------------