%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC084-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:36 EDT 2022 % Result : Unsatisfiable 136.04s 136.23s % Output : Refutation 161.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWC084-1 : TPTP v8.1.0. Released v2.4.0. % 0.10/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n007.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:57:37 EDT 2022 % 0.12/0.33 % CPUTime : % 136.04/136.23 % 136.04/136.23 SPASS V 3.9 % 136.04/136.23 SPASS beiseite: Proof found. % 136.04/136.23 % SZS status Theorem % 136.04/136.23 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 136.04/136.23 SPASS derived 39610 clauses, backtracked 22990 clauses, performed 135 splits and kept 31797 clauses. % 136.04/136.23 SPASS allocated 132078 KBytes. % 136.04/136.23 SPASS spent 0:2:15.79 on the problem. % 136.04/136.23 0:00:00.04 for the input. % 136.04/136.23 0:00:00.00 for the FLOTTER CNF translation. % 136.04/136.23 0:00:00.66 for inferences. % 136.04/136.23 0:00:07.63 for the backtracking. % 136.04/136.23 0:02:06.74 for the reduction. % 136.04/136.23 % 136.04/136.23 % 136.04/136.23 Here is a proof with depth 3, length 122 : % 136.04/136.23 % SZS output start Refutation % 136.04/136.23 1[0:Inp] || -> ssList(sk1)*. % 136.04/136.23 2[0:Inp] || -> ssList(sk2)*. % 136.04/136.23 5[0:Inp] || -> equal(sk4,sk2)**. % 136.04/136.23 6[0:Inp] || -> equal(sk3,sk1)**. % 136.04/136.23 7[0:Inp] || -> neq(sk2,nil)*. % 136.04/136.23 8[0:Inp] ssList(u) || neq(u,nil) segmentP(sk1,u) segmentP(sk2,u)* -> . % 136.04/136.23 11[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk4). % 136.04/136.23 14[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk3). % 136.04/136.23 15[0:Inp] || -> memberP(sk4,sk5)* equal(nil,sk3). % 136.04/136.23 28[0:Inp] || -> ssItem(skaf83(u))*. % 136.04/136.23 68[0:Inp] || -> ssList(skaf43(u,v))*. % 136.04/136.23 69[0:Inp] || -> ssList(skaf42(u,v))*. % 136.04/136.23 73[0:Inp] ssList(u) || -> segmentP(u,u)*. % 136.04/136.23 80[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 136.04/136.23 81[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 136.04/136.23 82[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 136.04/136.23 83[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 136.04/136.23 84[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 136.04/136.23 85[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 136.04/136.23 86[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 136.04/136.23 87[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 136.04/136.23 88[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 136.04/136.23 95[0:Inp] ssList(u) || equal(nil,u) -> segmentP(nil,u)*. % 136.04/136.23 101[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 136.04/136.23 102[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 136.04/136.23 115[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 136.04/136.23 118[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 136.04/136.23 132[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 136.04/136.23 136[0:Inp] ssList(u) ssItem(v) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 136.04/136.23 165[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(u,v),w),app(u,app(v,w)))**. % 136.04/136.23 173[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 136.04/136.23 179[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 136.04/136.23 180[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 136.04/136.23 185[0:Inp] ssList(u) ssItem(v) || memberP(u,v) -> equal(app(skaf42(u,v),cons(v,skaf43(v,u))),u)**. % 136.04/136.23 188[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(x,w) -> segmentP(app(app(v,x),u),w)*. % 136.04/136.23 193[0:Inp] ssList(u) ssList(v) || equal(hd(v),hd(u))* equal(tl(v),tl(u)) -> equal(v,u) equal(nil,v) equal(nil,u). % 136.04/136.23 195[0:Inp] ssList(u) duplicatefreeP(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 136.04/136.23 206[0:Rew:6.0,15.1,5.0,15.0] || -> equal(nil,sk1) memberP(sk2,sk5)*. % 136.04/136.23 208[0:Rew:6.0,14.1,6.0,14.0] || -> equal(nil,sk1) equal(cons(sk5,nil),sk1)**. % 136.04/136.23 209[0:Rew:208.1,11.1,5.0,11.1,6.0,11.0] || -> equal(sk2,sk1) equal(cons(sk5,nil),sk1)**. % 136.04/136.23 214[0:Rew:165.3,188.5] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(u,v) -> segmentP(app(w,app(u,x)),v)*. % 136.04/136.23 268[0:Res:2.0,8.0] || neq(sk2,nil) segmentP(sk2,sk2)* segmentP(sk1,sk2) -> . % 136.04/136.23 285[0:Res:2.0,95.0] || equal(nil,sk2) -> segmentP(nil,sk2)*. % 136.04/136.23 300[0:Res:2.0,73.0] || -> segmentP(sk2,sk2)*. % 136.04/136.23 313[0:Res:2.0,193.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 136.04/136.23 319[0:Res:2.0,185.1] ssItem(u) || memberP(sk2,u) -> equal(app(skaf42(sk2,u),cons(u,skaf43(u,sk2))),sk2)**. % 136.04/136.23 354[0:Res:2.0,102.1] ssItem(u) || -> ssList(cons(u,sk2))*. % 136.04/136.23 406[0:Res:1.0,180.0] || -> totalorderedP(sk1) equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 136.04/136.23 407[0:Res:1.0,179.0] || -> strictorderedP(sk1) equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 136.04/136.23 472[0:Res:1.0,73.0] || -> segmentP(sk1,sk1)*. % 136.04/136.23 485[0:Res:1.0,193.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 136.04/136.23 519[0:Res:1.0,132.1] ssItem(u) || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 136.04/136.23 523[0:Res:1.0,115.1] ssItem(u) || equal(cons(u,sk1),sk1)** -> . % 136.04/136.23 550[0:Res:1.0,214.3] ssList(u) ssList(v) ssList(w) || segmentP(sk1,u) -> segmentP(app(v,app(sk1,w)),u)*. % 136.04/136.23 560[0:MRR:268.0,268.1,7.0,300.0] || segmentP(sk1,sk2)* -> . % 136.04/136.23 566[1:Spt:88.1] || -> ssItem(u)*. % 136.04/136.23 571[1:MRR:87.0,566.0] || memberP(nil,u)* -> . % 136.04/136.23 572[1:MRR:86.0,566.0] || -> cyclefreeP(cons(u,nil))*. % 136.04/136.23 573[1:MRR:85.0,566.0] || -> totalorderP(cons(u,nil))*. % 136.04/136.23 574[1:MRR:84.0,566.0] || -> strictorderP(cons(u,nil))*. % 136.04/136.23 575[1:MRR:83.0,566.0] || -> totalorderedP(cons(u,nil))*. % 136.04/136.23 576[1:MRR:82.0,566.0] || -> strictorderedP(cons(u,nil))*. % 136.04/136.23 577[1:MRR:81.0,566.0] || -> duplicatefreeP(cons(u,nil))*. % 136.04/136.23 578[1:MRR:80.0,566.0] || -> equalelemsP(cons(u,nil))*. % 136.04/136.23 580[1:MRR:523.0,566.0] || equal(cons(u,sk1),sk1)** -> . % 136.04/136.23 588[1:MRR:519.0,566.0] || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 136.04/136.23 596[1:MRR:118.1,118.0,566.0] || -> equal(u,v) neq(u,v)*. % 136.04/136.23 644[1:MRR:319.0,566.0] || memberP(sk2,u) -> equal(app(skaf42(sk2,u),cons(u,skaf43(u,sk2))),sk2)**. % 136.04/136.23 699[1:MRR:136.1,566.0] ssList(u) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 136.04/136.23 772[2:Spt:485.5] || -> equal(nil,sk1)**. % 136.04/136.23 780[2:Rew:772.0,209.1] || -> equal(sk2,sk1) equal(cons(sk5,sk1),sk1)**. % 136.04/136.23 819[2:Rew:772.0,285.0] || equal(sk2,sk1) -> segmentP(nil,sk2)*. % 136.04/136.23 909[2:Rew:772.0,819.1] || equal(sk2,sk1) -> segmentP(sk1,sk2)*. % 136.04/136.23 910[2:MRR:909.1,560.0] || equal(sk2,sk1)** -> . % 136.04/136.23 921[2:MRR:780.0,780.1,910.0,580.0] || -> . % 136.04/136.23 988[2:Spt:921.0,485.5,772.0] || equal(nil,sk1)** -> . % 136.04/136.23 989[2:Spt:921.0,485.0,485.1,485.2,485.3,485.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 136.04/136.23 991[2:MRR:206.0,988.0] || -> memberP(sk2,sk5)*. % 136.04/136.23 995[2:MRR:208.0,988.0] || -> equal(cons(sk5,nil),sk1)**. % 136.04/136.23 1008[3:Spt:313.5] || -> equal(nil,sk2)**. % 136.04/136.23 1037[3:Rew:1008.0,571.0] || memberP(sk2,u)* -> . % 136.04/136.23 1109[3:UnC:1037.0,991.0] || -> . % 136.04/136.23 1185[3:Spt:1109.0,313.5,1008.0] || equal(nil,sk2)** -> . % 136.04/136.23 1186[3:Spt:1109.0,313.0,313.1,313.2,313.3,313.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 136.04/136.23 1201[4:Spt:406.0] || -> totalorderedP(sk1)*. % 136.04/136.23 1205[5:Spt:407.0] || -> strictorderedP(sk1)*. % 136.04/136.23 1225[2:SpR:995.0,572.0] || -> cyclefreeP(sk1)*. % 136.04/136.23 1226[2:SpR:995.0,573.0] || -> totalorderP(sk1)*. % 136.04/136.23 1227[2:SpR:995.0,574.0] || -> strictorderP(sk1)*. % 136.04/136.23 1228[2:SpR:995.0,575.0] || -> totalorderedP(sk1)*. % 136.04/136.23 1229[2:SpR:995.0,576.0] || -> strictorderedP(sk1)*. % 136.04/136.23 1230[2:SpR:995.0,577.0] || -> duplicatefreeP(sk1)*. % 136.04/136.23 1231[2:SpR:995.0,578.0] || -> equalelemsP(sk1)*. % 136.04/136.23 1267[2:SpL:995.0,588.0] || equal(sk1,sk1) -> singletonP(sk1)*. % 136.04/136.23 1268[2:Obv:1267.0] || -> singletonP(sk1)*. % 136.04/136.23 1635[2:SpR:995.0,699.1] ssList(u) || -> equal(app(sk1,u),cons(sk5,u))**. % 136.04/136.23 1650[2:Rew:1635.1,550.4] ssList(u) ssList(v) ssList(w) || segmentP(sk1,u) -> segmentP(app(v,cons(sk5,w)),u)*. % 136.04/136.23 38665[2:SpR:644.1,1650.4] ssList(u) ssList(skaf42(sk2,sk5)) ssList(skaf43(sk5,sk2)) || memberP(sk2,sk5)* segmentP(sk1,u) -> segmentP(sk2,u)*. % 136.04/136.23 48064[2:SSi:38665.2,38665.1,68.0,2.0,69.0,2.0] ssList(u) || memberP(sk2,sk5)* segmentP(sk1,u) -> segmentP(sk2,u)*. % 136.04/136.23 48065[2:MRR:48064.1,991.0] ssList(u) || segmentP(sk1,u) -> segmentP(sk2,u)*. % 136.04/136.23 48066[2:MRR:8.3,48065.2] ssList(u) || neq(u,nil) segmentP(sk1,u)* -> . % 136.04/136.23 48740[2:Res:472.0,48066.2] ssList(sk1) || neq(sk1,nil)* -> . % 136.04/136.23 48744[5:SSi:48740.0,1201.0,1.0,1205.0,1230.0,1231.0,1268.0,1227.0,1226.0,1225.0] || neq(sk1,nil)* -> . % 136.04/136.23 48766[5:Res:596.1,48744.0] || -> equal(nil,sk1)**. % 136.04/136.23 48767[5:MRR:48766.0,988.0] || -> . % 136.04/136.23 48768[5:Spt:48767.0,407.0,1205.0] || strictorderedP(sk1)* -> . % 136.04/136.23 48769[5:Spt:48767.0,407.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 136.04/136.23 48770[5:MRR:48768.0,1229.0] || -> . % 136.04/136.23 49246[4:Spt:48770.0,406.0,1201.0] || totalorderedP(sk1)* -> . % 136.04/136.23 49247[4:Spt:48770.0,406.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 136.04/136.23 49248[4:MRR:49246.0,1228.0] || -> . % 136.04/136.23 49687[1:Spt:49248.0,88.0,88.2] ssList(u) || -> duplicatefreeP(u)*. % 161.93/162.16 49882[1:MRR:195.1,49687.1] ssList(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 161.93/162.16 68021[0:SpR:173.3,101.2] ssList(u) ssList(v) ssItem(w) ssList(cons(w,v)) ssList(u) || -> ssList(cons(w,app(v,u)))*. % 161.93/162.16 68076[0:Obv:68021.0] ssList(u) ssItem(v) ssList(cons(v,u)) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 161.93/162.16 68077[0:SSi:68076.2,102.2] ssList(u) ssItem(v) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 161.93/162.16 70442[1:EqR:49882.5] ssList(app(app(u,cons(v,w)),cons(v,x))) ssItem(v) ssList(u) ssList(w) ssList(x) || -> . % 161.93/162.16 70469[1:SSi:70442.0,101.2,101.2,102.2,102.2] ssItem(u) ssList(v) ssList(w) ssList(x) || -> . % 161.93/162.16 70470[1:MRR:68077.3,70469.1] ssList(u) ssItem(v) ssList(w) || -> . % 161.93/162.16 70473[1:Con:70470.2] ssList(u) ssItem(v) || -> . % 161.93/162.16 70475[1:MRR:354.1,70473.0] ssItem(u) || -> . % 161.93/162.16 70485[1:UnC:70475.0,28.0] || -> . % 161.93/162.16 % SZS output end Refutation % 161.93/162.16 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_11 co1_14 co1_15 clause12 clause52 clause53 clause57 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause71 clause72 clause79 clause85 clause86 clause99 clause102 clause116 clause120 clause149 clause157 clause163 clause164 clause169 clause172 clause177 clause179 % 161.93/162.16 %------------------------------------------------------------------------------