%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC063+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:28 EDT 2022 % Result : Theorem 40.50s 40.67s % Output : Refutation 40.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWC063+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n018.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun Jun 12 09:34:11 EDT 2022 % 0.14/0.35 % CPUTime : % 40.50/40.67 % 40.50/40.67 SPASS V 3.9 % 40.50/40.67 SPASS beiseite: Proof found. % 40.50/40.67 % SZS status Theorem % 40.50/40.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.50/40.67 SPASS derived 21054 clauses, backtracked 9126 clauses, performed 65 splits and kept 13448 clauses. % 40.50/40.67 SPASS allocated 127767 KBytes. % 40.50/40.67 SPASS spent 0:0:35.52 on the problem. % 40.50/40.67 0:00:00.04 for the input. % 40.50/40.67 0:00:00.07 for the FLOTTER CNF translation. % 40.50/40.67 0:00:00.36 for inferences. % 40.50/40.67 0:00:00.98 for the backtracking. % 40.50/40.67 0:0:33.69 for the reduction. % 40.50/40.67 % 40.50/40.67 % 40.50/40.67 Here is a proof with depth 5, length 101 : % 40.50/40.67 % SZS output start Refutation % 40.50/40.67 1[0:Inp] || -> ssList(skc9)*. % 40.50/40.67 2[0:Inp] || -> ssItem(skc8)*. % 40.50/40.67 3[0:Inp] || -> ssList(skc7)*. % 40.50/40.67 4[0:Inp] || -> ssList(skc6)*. % 40.50/40.67 7[0:Inp] || -> ssList(nil)*. % 40.50/40.67 8[0:Inp] || -> cyclefreeP(nil)*. % 40.50/40.67 9[0:Inp] || -> totalorderP(nil)*. % 40.50/40.67 10[0:Inp] || -> strictorderP(nil)*. % 40.50/40.67 11[0:Inp] || -> totalorderedP(nil)*. % 40.50/40.67 12[0:Inp] || -> strictorderedP(nil)*. % 40.50/40.67 13[0:Inp] || -> duplicatefreeP(nil)*. % 40.50/40.67 14[0:Inp] || -> equalelemsP(nil)*. % 40.50/40.67 60[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 40.50/40.67 66[0:Inp] ssList(u) || -> segmentP(u,u)*. % 40.50/40.67 67[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 40.50/40.67 69[0:Inp] || equal(skc7,nil)** -> equal(skc6,nil). % 40.50/40.67 70[0:Inp] || SkP0(skc6,skc7) -> neq(skc7,nil)*. % 40.50/40.67 71[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 40.50/40.67 73[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 40.50/40.67 74[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 40.50/40.67 75[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 40.50/40.67 76[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 40.50/40.67 77[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 40.50/40.67 78[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 40.50/40.67 79[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 40.50/40.67 81[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 40.50/40.67 82[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 40.50/40.67 90[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 40.50/40.67 91[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 40.50/40.67 98[0:Inp] || neq(skc7,nil) -> equal(app(cons(skc8,nil),skc9),skc6)**. % 40.50/40.67 99[0:Inp] || neq(skc7,nil) -> equal(app(skc9,cons(skc8,nil)),skc7)**. % 40.50/40.67 109[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 40.50/40.67 122[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 40.50/40.67 129[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 40.50/40.67 156[0:Inp] ssList(u) || neq(u,nil) segmentP(skc6,u) segmentP(skc7,u)* SkP0(skc6,skc7) -> . % 40.50/40.67 161[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 40.50/40.67 187[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || equal(app(app(u,x),v),w)* -> segmentP(w,x)*. % 40.50/40.67 189[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). % 40.50/40.67 202[0:Rew:161.3,187.4] ssList(u) ssList(v) ssList(w) ssList(x) || equal(app(x,app(u,w)),v)*+ -> segmentP(v,u)*. % 40.50/40.67 279[0:Res:4.0,81.0] || -> equal(app(nil,skc6),skc6)**. % 40.50/40.67 280[0:Res:4.0,82.0] || -> equal(app(skc6,nil),skc6)**. % 40.50/40.67 285[0:Res:4.0,66.0] || -> segmentP(skc6,skc6)*. % 40.50/40.67 405[0:Res:3.0,156.0] || neq(skc7,nil) segmentP(skc7,skc7)* segmentP(skc6,skc7) SkP0(skc6,skc7) -> . % 40.50/40.67 451[0:Res:3.0,81.0] || -> equal(app(nil,skc7),skc7)**. % 40.50/40.67 457[0:Res:3.0,66.0] || -> segmentP(skc7,skc7)*. % 40.50/40.67 458[0:Res:3.0,67.0] || -> segmentP(skc7,nil)*. % 40.50/40.67 459[0:Res:3.0,189.1] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u) equal(skc7,nil). % 40.50/40.67 548[0:MRR:405.0,405.1,70.1,457.0] || SkP0(skc6,skc7) segmentP(skc6,skc7)* -> . % 40.50/40.67 557[1:Spt:459.5] || -> equal(skc7,nil)**. % 40.50/40.67 562[1:Rew:557.0,548.0] || SkP0(skc6,nil) segmentP(skc6,skc7)* -> . % 40.50/40.67 570[1:Rew:557.0,69.0] || equal(nil,nil) -> equal(skc6,nil)**. % 40.50/40.67 668[1:Rew:557.0,458.0] || -> segmentP(nil,nil)*. % 40.50/40.67 716[1:Obv:570.0] || -> equal(skc6,nil)**. % 40.50/40.67 888[1:Rew:716.0,562.1,557.0,562.1,716.0,562.0] || SkP0(nil,nil) segmentP(nil,nil)* -> . % 40.50/40.67 889[1:MRR:888.1,668.0] || SkP0(nil,nil)* -> . % 40.50/40.67 1073[1:Res:71.1,889.0] || equal(nil,nil)* -> . % 40.50/40.67 1074[1:Obv:1073.0] || -> . % 40.50/40.67 1075[1:Spt:1074.0,459.5,557.0] || equal(skc7,nil)** -> . % 40.50/40.67 1076[1:Spt:1074.0,459.0,459.1,459.2,459.3,459.4] ssList(u) || equal(tl(skc7),tl(u))* equal(hd(skc7),hd(u)) -> equal(nil,u) equal(skc7,u). % 40.50/40.67 1878[2:Spt:156.0,156.1,156.2,156.3] ssList(u) || neq(u,nil) segmentP(skc6,u) segmentP(skc7,u)* -> . % 40.50/40.67 1881[2:Res:457.0,1878.3] ssList(skc7) || neq(skc7,nil) segmentP(skc6,skc7)* -> . % 40.50/40.67 1883[2:SSi:1881.0,3.0] || neq(skc7,nil) segmentP(skc6,skc7)* -> . % 40.50/40.67 1887[3:Spt:70.1] || -> neq(skc7,nil)*. % 40.50/40.67 1888[3:MRR:99.0,1887.0] || -> equal(app(skc9,cons(skc8,nil)),skc7)**. % 40.50/40.67 1889[3:MRR:98.0,1887.0] || -> equal(app(cons(skc8,nil),skc9),skc6)**. % 40.50/40.67 1890[3:MRR:1883.0,1887.0] || segmentP(skc6,skc7)* -> . % 40.50/40.67 2528[0:EqR:122.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 40.50/40.67 2531[0:SSi:2528.0,90.1,14.1,13.1,10.1,9.1,8.1,12.1,11.0,7.0,79.0,78.0,75.0,74.0,73.0,77.0,76.2] ssItem(u) || -> singletonP(cons(u,nil))*. % 40.50/40.67 2878[3:SpR:129.2,1889.0] ssItem(skc8) ssList(skc9) || -> equal(cons(skc8,skc9),skc6)**. % 40.50/40.67 2889[3:SSi:2878.1,2878.0,1.0,2.0] || -> equal(cons(skc8,skc9),skc6)**. % 40.50/40.67 6274[0:EqR:202.4] ssList(u) ssList(app(v,app(u,w))) ssList(w) ssList(v) || -> segmentP(app(v,app(u,w)),u)*. % 40.50/40.67 6310[0:SSi:6274.1,91.2,91.2] ssList(u) ssList(v) ssList(w) || -> segmentP(app(w,app(u,v)),u)*. % 40.50/40.67 9416[3:SpR:1889.0,161.3] ssList(u) ssList(skc9) ssList(cons(skc8,nil)) || -> equal(app(cons(skc8,nil),app(skc9,u)),app(skc6,u))**. % 40.50/40.67 18848[3:SpR:1888.0,6310.3] ssList(skc9) ssList(cons(skc8,nil)) ssList(u) || -> segmentP(app(u,skc7),skc9)*. % 40.50/40.67 22455[3:SSi:18848.1,18848.0,90.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,79.1,2.0,78.1,2.0,75.1,2.0,74.1,2.0,73.0,2.0,77.0,2.0,76.0,2.0,2531.0,2.0,1.2] ssList(u) || -> segmentP(app(u,skc7),skc9)*. % 40.50/40.67 22661[3:SSi:9416.2,9416.1,90.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,79.1,2.0,78.1,2.0,75.1,2.0,74.1,2.0,73.0,2.0,77.0,2.0,76.0,2.0,2531.0,2.0,1.2] ssList(u) || -> equal(app(cons(skc8,nil),app(skc9,u)),app(skc6,u))**. % 40.50/40.67 25475[3:SpR:451.0,22455.1] ssList(nil) || -> segmentP(skc7,skc9)*. % 40.50/40.67 25487[3:SSi:25475.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> segmentP(skc7,skc9)*. % 40.50/40.67 27424[3:SpR:22661.1,6310.3] ssList(u) ssList(skc9) ssList(u) ssList(cons(skc8,nil)) || -> segmentP(app(skc6,u),skc9)*. % 40.50/40.67 27453[3:Obv:27424.0] ssList(skc9) ssList(u) ssList(cons(skc8,nil)) || -> segmentP(app(skc6,u),skc9)*. % 40.50/40.67 28862[3:Res:25487.0,1878.3] ssList(skc9) || neq(skc9,nil) segmentP(skc6,skc9)* -> . % 40.50/40.67 30419[3:SSi:28862.0,1.0] || neq(skc9,nil) segmentP(skc6,skc9)* -> . % 40.50/40.67 30505[3:SSi:27453.2,27453.0,90.0,2.0,14.1,13.0,10.1,9.0,8.1,12.0,11.1,7.0,79.1,2.0,78.1,2.0,75.1,2.0,74.1,2.0,73.0,2.0,77.0,2.0,76.0,2.0,2531.0,2.0,1.2] ssList(u) || -> segmentP(app(skc6,u),skc9)*. % 40.50/40.67 32534[3:SpR:280.0,30505.1] ssList(nil) || -> segmentP(skc6,skc9)*. % 40.50/40.67 32544[3:SSi:32534.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> segmentP(skc6,skc9)*. % 40.50/40.67 32545[3:MRR:30419.1,32544.0] || neq(skc9,nil)* -> . % 40.50/40.67 32568[3:Res:109.2,32545.0] ssList(nil) ssList(skc9) || -> equal(skc9,nil)**. % 40.50/40.67 32701[3:SSi:32568.1,32568.0,1.0,14.0,13.0,10.0,9.0,8.0,12.0,11.0,7.0] || -> equal(skc9,nil)**. % 40.50/40.67 32707[3:Rew:32701.0,2889.0] || -> equal(cons(skc8,nil),skc6)**. % 40.50/40.67 32725[3:Rew:32701.0,1888.0] || -> equal(app(nil,cons(skc8,nil)),skc7)**. % 40.50/40.67 32997[3:Rew:32707.0,32725.0] || -> equal(app(nil,skc6),skc7)**. % 40.50/40.67 32998[3:Rew:279.0,32997.0] || -> equal(skc7,skc6)**. % 40.50/40.67 33017[3:Rew:32998.0,1890.0] || segmentP(skc6,skc6)* -> . % 40.50/40.67 33514[3:MRR:33017.0,285.0] || -> . % 40.50/40.67 34870[3:Spt:33514.0,70.1,1887.0] || neq(skc7,nil)* -> . % 40.50/40.67 34871[3:Spt:33514.0,70.0] || SkP0(skc6,skc7)* -> . % 40.50/40.67 35281[3:Res:60.0,34871.0] || -> equal(skc7,nil)**. % 40.50/40.67 35282[3:MRR:35281.0,1075.0] || -> . % 40.50/40.67 35283[2:Spt:35282.0,156.4] || SkP0(skc6,skc7)* -> . % 40.50/40.67 35285[2:Res:60.0,35283.0] || -> equal(skc7,nil)**. % 40.50/40.67 35286[2:MRR:35285.0,1075.0] || -> . % 40.50/40.67 % SZS output end Refutation % 40.50/40.67 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax55 ax57 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax84 ax16 ax26 ax15 ax4 ax81 ax82 ax7 ax77 % 40.50/40.67 %------------------------------------------------------------------------------