%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC192+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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:22 EDT 2022 % Result : Theorem 10.13s 10.37s % Output : Refutation 10.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.12 % Problem : SWC192+1 : TPTP v8.1.0. Released v2.4.0. % 0.09/0.12 % Command : run_spass %d %s % 0.14/0.33 % Computer : n015.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sun Jun 12 02:21:36 EDT 2022 % 0.14/0.34 % CPUTime : % 10.13/10.37 % 10.13/10.37 SPASS V 3.9 % 10.13/10.37 SPASS beiseite: Proof found. % 10.13/10.37 % SZS status Theorem % 10.13/10.37 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 10.13/10.37 SPASS derived 9980 clauses, backtracked 2275 clauses, performed 42 splits and kept 6509 clauses. % 10.13/10.37 SPASS allocated 111106 KBytes. % 10.13/10.37 SPASS spent 0:00:09.37 on the problem. % 10.13/10.37 0:00:00.04 for the input. % 10.13/10.37 0:00:00.07 for the FLOTTER CNF translation. % 10.13/10.37 0:00:00.12 for inferences. % 10.13/10.37 0:00:00.28 for the backtracking. % 10.13/10.37 0:00:08.62 for the reduction. % 10.13/10.37 % 10.13/10.37 % 10.13/10.37 Here is a proof with depth 6, length 84 : % 10.13/10.37 % SZS output start Refutation % 10.13/10.37 1[0:Inp] || -> ssList(skc13)*. % 10.13/10.37 2[0:Inp] || -> ssList(skc12)*. % 10.13/10.37 3[0:Inp] || -> ssItem(skc11)*. % 10.13/10.37 4[0:Inp] || -> ssItem(skc10)*. % 10.13/10.37 6[0:Inp] || -> ssList(skc8)*. % 10.13/10.37 8[0:Inp] || -> ssItem(skc14)*. % 10.13/10.37 9[0:Inp] || -> ssList(nil)*. % 10.13/10.37 10[0:Inp] || -> cyclefreeP(nil)*. % 10.13/10.37 11[0:Inp] || -> totalorderP(nil)*. % 10.13/10.37 12[0:Inp] || -> strictorderP(nil)*. % 10.13/10.37 13[0:Inp] || -> totalorderedP(nil)*. % 10.13/10.37 14[0:Inp] || -> strictorderedP(nil)*. % 10.13/10.37 15[0:Inp] || -> duplicatefreeP(nil)*. % 10.13/10.37 16[0:Inp] || -> equalelemsP(nil)*. % 10.13/10.37 55[0:Inp] || -> ssItem(skf44(u,v))*. % 10.13/10.37 56[0:Inp] || equal(skc11,skc10)** -> . % 10.13/10.37 73[0:Inp] || SkP0(skc9,skc8)* -> equal(nil,skc8). % 10.13/10.37 75[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 10.13/10.37 76[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 10.13/10.37 77[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 10.13/10.37 78[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 10.13/10.37 79[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 10.13/10.37 80[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 10.13/10.37 81[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 10.13/10.37 84[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 10.13/10.37 90[0:Inp] || -> SkP0(u,v) equal(cons(skf44(u,v),nil),v)**. % 10.13/10.37 94[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 10.13/10.37 95[0:Inp] ssList(u) ssList(v) || -> ssList(app(v,u))*. % 10.13/10.37 114[0:Inp] ssItem(u) ssList(v) || -> equal(hd(cons(u,v)),u)**. % 10.13/10.37 116[0:Inp] || -> equal(app(app(app(skc12,cons(skc10,nil)),cons(skc11,nil)),skc13),skc8)**. % 10.13/10.37 125[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 10.13/10.37 132[0:Inp] ssItem(u) ssList(v) || -> equal(app(cons(u,nil),v),cons(u,v))**. % 10.13/10.37 137[0:Inp] ssList(u) ssList(v) || -> equal(nil,v) equal(hd(app(v,u)),hd(v))**. % 10.13/10.37 163[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(w,v),u),app(w,app(v,u)))**. % 10.13/10.37 191[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). % 10.13/10.37 193[0:Inp] ssList(u) ssList(v) ssList(w) ssItem(x) ssItem(y) equalelemsP(u) || equal(app(w,cons(y,cons(x,v))),u)* -> equal(y,x). % 10.13/10.37 248[0:Res:6.0,137.0] ssList(u) || -> equal(nil,skc8) equal(hd(app(skc8,u)),hd(skc8))**. % 10.13/10.37 259[0:Res:6.0,114.0] ssItem(u) || -> equal(hd(cons(u,skc8)),u)**. % 10.13/10.37 271[0:Res:6.0,94.0] ssItem(u) || -> ssList(cons(u,skc8))*. % 10.13/10.37 289[0:Res:6.0,191.1] ssList(u) || equal(tl(skc8),tl(u))* equal(hd(skc8),hd(u)) -> equal(nil,u) equal(skc8,u) equal(nil,skc8). % 10.13/10.37 554[1:Spt:248.0,248.2] ssList(u) || -> equal(hd(app(skc8,u)),hd(skc8))**. % 10.13/10.37 1593[2:Spt:289.5] || -> equal(nil,skc8)**. % 10.13/10.37 1629[2:Rew:1593.0,75.1] ssItem(u) || -> cyclefreeP(cons(u,skc8))*. % 10.13/10.37 1630[2:Rew:1593.0,76.1] ssItem(u) || -> totalorderP(cons(u,skc8))*. % 10.13/10.37 1631[2:Rew:1593.0,77.1] ssItem(u) || -> strictorderP(cons(u,skc8))*. % 10.13/10.37 1632[2:Rew:1593.0,78.1] ssItem(u) || -> totalorderedP(cons(u,skc8))*. % 10.13/10.37 1633[2:Rew:1593.0,79.1] ssItem(u) || -> strictorderedP(cons(u,skc8))*. % 10.13/10.37 1634[2:Rew:1593.0,80.1] ssItem(u) || -> duplicatefreeP(cons(u,skc8))*. % 10.13/10.37 1635[2:Rew:1593.0,81.1] ssItem(u) || -> equalelemsP(cons(u,skc8))*. % 10.13/10.37 1641[2:Rew:1593.0,84.1] ssList(u) || -> equal(app(skc8,u),u)**. % 10.13/10.37 1721[2:Rew:1641.1,554.1] ssList(u) || -> equal(hd(u),hd(skc8))*. % 10.13/10.37 1794[2:SpR:1721.1,259.1] ssList(cons(u,skc8)) ssItem(u) || -> equal(hd(skc8),u)*. % 10.13/10.37 1803[2:SSi:1794.0,271.1,1629.1,1630.1,1631.1,1632.1,1633.1,1634.1,1635.1] ssItem(u) || -> equal(hd(skc8),u)*. % 10.13/10.37 1821[2:SpR:1803.1,1803.1] ssItem(u) ssItem(v) || -> equal(u,v)*. % 10.13/10.37 2009[2:EmS:1821.0,8.0] ssItem(u) || -> equal(skc14,u)*. % 10.13/10.37 2035[2:EmS:2009.0,3.0] || -> equal(skc14,skc11)**. % 10.13/10.37 2036[2:EmS:2009.0,4.0] || -> equal(skc14,skc10)**. % 10.13/10.37 2041[2:Rew:2035.0,2036.0] || -> equal(skc11,skc10)**. % 10.13/10.37 2042[2:MRR:2041.0,56.0] || -> . % 10.13/10.37 2247[2:Spt:2042.0,289.5,1593.0] || equal(nil,skc8)** -> . % 10.13/10.37 2248[2:Spt:2042.0,289.0,289.1,289.2,289.3,289.4] ssList(u) || equal(tl(skc8),tl(u))* equal(hd(skc8),hd(u)) -> equal(nil,u) equal(skc8,u). % 10.13/10.37 2254[2:MRR:73.1,2247.0] || SkP0(skc9,skc8)* -> . % 10.13/10.37 2372[0:SpR:90.1,81.1] ssItem(skf44(u,v)) || -> SkP0(u,v)* equalelemsP(v). % 10.13/10.37 2380[0:SSi:2372.0,55.0] || -> SkP0(u,v)* equalelemsP(v). % 10.13/10.37 2388[2:Res:2380.0,2254.0] || -> equalelemsP(skc8)*. % 10.13/10.37 3164[0:EqR:125.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 10.13/10.37 3169[0:SSi:3164.0,81.0,80.0,79.0,78.0,77.0,76.0,75.0,94.0,16.2,15.1,14.1,13.1,12.1,11.1,10.1,9.1] ssItem(u) || -> singletonP(cons(u,nil))*. % 10.13/10.37 5298[0:SpR:163.3,116.0] ssList(skc13) ssList(cons(skc11,nil)) ssList(app(skc12,cons(skc10,nil))) || -> equal(app(app(skc12,cons(skc10,nil)),app(cons(skc11,nil),skc13)),skc8)**. % 10.13/10.37 5362[0:SSi:5298.2,5298.1,5298.0,95.0,2.0,81.0,4.0,80.0,4.0,79.0,4.0,78.0,4.0,77.2,4.0,76.1,4.0,75.1,4.0,3169.1,4.0,94.1,4.0,16.1,15.0,14.1,13.0,12.1,11.0,10.1,9.0,81.0,3.0,80.0,3.0,79.0,3.0,78.0,3.0,77.2,3.0,76.1,3.0,75.1,3.0,3169.1,3.0,94.1,3.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(skc11,nil),skc13)),skc8)**. % 10.13/10.37 10952[0:SpR:132.2,5362.0] ssItem(skc11) ssList(skc13) || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc11,skc13)),skc8)**. % 10.13/10.37 10966[0:SSi:10952.1,10952.0,1.0,3.0] || -> equal(app(app(skc12,cons(skc10,nil)),cons(skc11,skc13)),skc8)**. % 10.13/10.37 11064[0:SpR:10966.0,163.3] ssList(cons(skc11,skc13)) ssList(cons(skc10,nil)) ssList(skc12) || -> equal(app(skc12,app(cons(skc10,nil),cons(skc11,skc13))),skc8)**. % 10.13/10.37 11096[0:SSi:11064.2,11064.1,11064.0,2.0,81.0,4.2,80.0,4.0,79.0,4.0,78.0,4.0,77.0,4.0,76.0,4.2,75.0,4.1,3169.0,4.1,94.0,4.1,16.0,15.1,14.0,13.1,12.0,11.1,10.0,9.1,94.0,3.1,1.0] || -> equal(app(skc12,app(cons(skc10,nil),cons(skc11,skc13))),skc8)**. % 10.13/10.37 11239[0:SpR:132.2,11096.0] ssItem(skc10) ssList(cons(skc11,skc13)) || -> equal(app(skc12,cons(skc10,cons(skc11,skc13))),skc8)**. % 10.13/10.37 11253[0:SSi:11239.1,11239.0,94.0,3.0,1.0,4.2] || -> equal(app(skc12,cons(skc10,cons(skc11,skc13))),skc8)**. % 10.13/10.37 13344[0:SpL:11253.0,193.6] ssList(u) ssList(skc13) ssList(skc12) ssItem(skc11) ssItem(skc10) equalelemsP(u) || equal(skc8,u)* -> equal(skc11,skc10)**. % 10.13/10.37 13348[0:SSi:13344.4,13344.3,13344.2,13344.1,4.0,3.0,2.0,1.0] ssList(u) equalelemsP(u) || equal(skc8,u)* -> equal(skc11,skc10)**. % 10.13/10.37 13349[0:MRR:13348.3,56.0] ssList(u) equalelemsP(u) || equal(skc8,u)* -> . % 10.13/10.37 13645[2:EmS:13349.0,13349.1,6.0,2388.0] || equal(skc8,skc8)* -> . % 10.13/10.37 13699[0:EmS:13349.0,13349.1,9.0,16.0] || equal(nil,skc8)** -> . % 10.13/10.37 13700[2:Obv:13645.0] || -> . % 10.13/10.37 13747[1:Spt:13700.0,248.1] || -> equal(nil,skc8)**. % 10.13/10.37 14180[1:Rew:13747.0,13699.0] || equal(skc8,skc8)* -> . % 10.13/10.37 14181[1:Obv:14180.0] || -> . % 10.13/10.37 % SZS output end Refutation % 10.13/10.37 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax16 ax26 ax23 ax4 ax81 ax85 ax82 ax77 ax14 % 10.13/10.37 %------------------------------------------------------------------------------