%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC104-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:45 EDT 2022 % Result : Unsatisfiable 11.17s 11.38s % Output : Refutation 11.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWC104-1 : TPTP v8.1.0. Released v2.4.0. % 0.13/0.14 % Command : run_spass %d %s % 0.13/0.35 % Computer : n029.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 12 06:14:39 EDT 2022 % 0.13/0.35 % CPUTime : % 11.17/11.38 % 11.17/11.38 SPASS V 3.9 % 11.17/11.38 SPASS beiseite: Proof found. % 11.17/11.38 % SZS status Theorem % 11.17/11.38 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.17/11.38 SPASS derived 11198 clauses, backtracked 6321 clauses, performed 79 splits and kept 11319 clauses. % 11.17/11.38 SPASS allocated 88531 KBytes. % 11.17/11.38 SPASS spent 0:00:09.61 on the problem. % 11.17/11.38 0:00:00.04 for the input. % 11.17/11.38 0:00:00.00 for the FLOTTER CNF translation. % 11.17/11.38 0:00:00.10 for inferences. % 11.17/11.38 0:00:00.29 for the backtracking. % 11.17/11.38 0:00:08.94 for the reduction. % 11.17/11.38 % 11.17/11.38 % 11.17/11.38 Here is a proof with depth 4, length 118 : % 11.17/11.38 % SZS output start Refutation % 11.17/11.38 1[0:Inp] || -> ssList(sk1)*. % 11.17/11.38 2[0:Inp] || -> ssList(sk2)*. % 11.17/11.38 5[0:Inp] || -> equal(sk4,sk2)**. % 11.17/11.38 6[0:Inp] || -> equal(sk3,sk1)**. % 11.17/11.38 7[0:Inp] || -> neq(sk2,nil)*. % 11.17/11.38 8[0:Inp] || -> ssList(sk5)*. % 11.17/11.38 9[0:Inp] || -> equal(app(sk3,sk5),sk4)**. % 11.17/11.38 10[0:Inp] || -> totalorderedP(sk3)*. % 11.17/11.38 12[0:Inp] || equal(nil,sk3) -> equal(sk4,nil)**. % 11.17/11.38 13[0:Inp] || frontsegP(sk2,sk1)* neq(sk1,nil) -> . % 11.17/11.38 14[0:Inp] || -> equalelemsP(nil)*. % 11.17/11.38 15[0:Inp] || -> duplicatefreeP(nil)*. % 11.17/11.38 16[0:Inp] || -> strictorderedP(nil)*. % 11.17/11.38 17[0:Inp] || -> totalorderedP(nil)*. % 11.17/11.38 18[0:Inp] || -> strictorderP(nil)*. % 11.17/11.38 19[0:Inp] || -> totalorderP(nil)*. % 11.17/11.38 20[0:Inp] || -> cyclefreeP(nil)*. % 11.17/11.38 21[0:Inp] || -> ssList(nil)*. % 11.17/11.38 74[0:Inp] ssList(u) || -> frontsegP(u,u)*. % 11.17/11.38 85[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 11.17/11.38 86[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 11.17/11.38 90[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 11.17/11.38 113[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 11.17/11.38 115[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 11.17/11.38 130[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 11.17/11.38 131[0:Inp] ssList(u) ssList(v) || equal(app(u,v),nil)** -> equal(nil,u). % 11.17/11.38 132[0:Inp] ssList(u) ssList(v) || equal(app(u,v),nil)** -> equal(nil,v). % 11.17/11.38 147[0:Inp] ssItem(u) ssList(v) || strictorderedP(cons(u,v)) -> lt(u,hd(v))* equal(nil,v). % 11.17/11.38 148[0:Inp] ssItem(u) ssList(v) || totalorderedP(cons(u,v)) -> leq(u,hd(v))* equal(nil,v). % 11.17/11.38 150[0:Inp] ssList(u) ssList(v) ssList(w) || frontsegP(u,v) -> frontsegP(app(u,w),v)*. % 11.17/11.38 199[0:Rew:6.0,10.0] || -> totalorderedP(sk1)*. % 11.17/11.38 202[0:Rew:6.0,9.0,5.0,9.0] || -> equal(app(sk1,sk5),sk2)**. % 11.17/11.38 203[0:Rew:5.0,12.1,6.0,12.0] || equal(nil,sk1)** -> equal(nil,sk2). % 11.17/11.38 242[0:Res:8.0,147.0] ssItem(u) || strictorderedP(cons(u,sk5)) -> lt(u,hd(sk5))* equal(sk5,nil). % 11.17/11.38 290[0:Res:8.0,85.0] || -> ssItem(u)* duplicatefreeP(sk5)*. % 11.17/11.38 416[0:Res:2.0,148.0] ssItem(u) || totalorderedP(cons(u,sk2)) -> leq(u,hd(sk2))* equal(nil,sk2). % 11.17/11.38 459[0:Res:2.0,90.0] || -> ssList(tl(sk2))* equal(nil,sk2). % 11.17/11.38 463[0:Res:2.0,85.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 11.17/11.38 557[1:Spt:85.1] || -> ssItem(u)*. % 11.17/11.38 587[1:MRR:115.1,115.0,557.0] || -> equal(u,v) neq(u,v)*. % 11.17/11.38 597[1:MRR:130.1,130.0,557.0] || neq(u,v)* equal(u,v) -> . % 11.17/11.38 2955[1:Res:7.0,597.0] || equal(nil,sk2)** -> . % 11.17/11.38 3391[0:SpL:202.0,132.2] ssList(sk1) ssList(sk5) || equal(nil,sk2) -> equal(sk5,nil)**. % 11.17/11.38 3454[0:SpL:202.0,131.2] ssList(sk1) ssList(sk5) || equal(nil,sk2)** -> equal(nil,sk1). % 11.17/11.38 5268[0:SpR:202.0,150.4] ssList(sk1) ssList(u) ssList(sk5) || frontsegP(sk1,u) -> frontsegP(sk2,u)*. % 11.17/11.38 10603[0:SSi:5268.2,5268.0,8.0,199.0,1.0] ssList(u) || frontsegP(sk1,u) -> frontsegP(sk2,u)*. % 11.17/11.38 11256[0:Res:10603.2,13.0] ssList(sk1) || frontsegP(sk1,sk1)* neq(sk1,nil) -> . % 11.17/11.38 11259[0:SSi:11256.0,199.0,1.0] || frontsegP(sk1,sk1)* neq(sk1,nil) -> . % 11.17/11.38 11265[0:Res:74.1,11259.0] ssList(sk1) || neq(sk1,nil)* -> . % 11.17/11.38 11266[0:SSi:11265.0,199.0,1.0] || neq(sk1,nil)* -> . % 11.17/11.38 11267[1:Res:587.1,11266.0] || -> equal(nil,sk1)**. % 11.17/11.38 12190[1:Rew:11267.0,2955.0] || equal(sk2,sk1)** -> . % 11.17/11.38 12215[1:Rew:11267.0,203.1,11267.0,203.0] || equal(sk1,sk1) -> equal(sk2,sk1)**. % 11.17/11.38 12216[1:Obv:12215.0] || -> equal(sk2,sk1)**. % 11.17/11.38 12217[1:MRR:12216.0,12190.0] || -> . % 11.17/11.38 12479[1:Spt:12217.0,85.0,85.2] ssList(u) || -> duplicatefreeP(u)*. % 11.17/11.38 12480[0:SSi:3391.0,199.0,1.0] ssList(sk5) || equal(nil,sk2) -> equal(sk5,nil)**. % 11.17/11.38 12481[0:MRR:12480.0,8.0] || equal(nil,sk2) -> equal(sk5,nil)**. % 11.17/11.38 12483[0:SSi:3454.0,199.0,1.0] ssList(sk5) || equal(nil,sk2)** -> equal(nil,sk1). % 11.17/11.38 12484[0:MRR:12483.0,8.0] || equal(nil,sk2)** -> equal(nil,sk1). % 11.17/11.38 12485[0:Rew:12484.1,12481.1] || equal(nil,sk2) -> equal(sk5,sk1)**. % 11.17/11.38 12523[2:Spt:463.0] || -> ssItem(u)*. % 11.17/11.38 12551[2:MRR:115.1,115.0,12523.0] || -> equal(u,v) neq(u,v)*. % 11.17/11.38 13152[3:Spt:459.1] || -> equal(nil,sk2)**. % 11.17/11.38 13161[3:Rew:13152.0,7.0] || -> neq(sk2,sk2)*. % 11.17/11.38 13166[3:Rew:13152.0,11266.0] || neq(sk1,sk2)* -> . % 11.17/11.38 13193[3:Rew:13152.0,12484.0] || equal(sk2,sk2) -> equal(nil,sk1)**. % 11.17/11.38 13377[3:Obv:13193.0] || -> equal(nil,sk1)**. % 11.17/11.38 13378[3:Rew:13152.0,13377.0] || -> equal(sk2,sk1)**. % 11.17/11.38 13468[3:Rew:13378.0,13161.0] || -> neq(sk1,sk1)*. % 11.17/11.38 13471[3:Rew:13378.0,13166.0] || neq(sk1,sk1)* -> . % 11.17/11.38 13481[3:MRR:13471.0,13468.0] || -> . % 11.17/11.38 13705[3:Spt:13481.0,459.1,13152.0] || equal(nil,sk2)** -> . % 11.17/11.38 13706[3:Spt:13481.0,459.0] || -> ssList(tl(sk2))*. % 11.17/11.38 13710[3:MRR:203.1,13705.0] || equal(nil,sk1)** -> . % 11.17/11.38 13826[2:Res:12551.1,11266.0] || -> equal(nil,sk1)**. % 11.17/11.38 13827[3:MRR:13826.0,13710.0] || -> . % 11.17/11.38 13828[2:Spt:13827.0,463.1] || -> duplicatefreeP(sk2)*. % 11.17/11.38 13831[3:Spt:290.0] || -> ssItem(u)*. % 11.17/11.38 13861[3:MRR:115.1,115.0,13831.0] || -> equal(u,v) neq(u,v)*. % 11.17/11.38 14087[4:Spt:459.1] || -> equal(nil,sk2)**. % 11.17/11.38 14099[4:Rew:14087.0,7.0] || -> neq(sk2,sk2)*. % 11.17/11.38 14101[4:Rew:14087.0,11266.0] || neq(sk1,sk2)* -> . % 11.17/11.38 14217[4:Rew:14087.0,12484.0] || equal(sk2,sk2) -> equal(nil,sk1)**. % 11.17/11.38 14422[4:Obv:14217.0] || -> equal(nil,sk1)**. % 11.17/11.38 14423[4:Rew:14087.0,14422.0] || -> equal(sk2,sk1)**. % 11.17/11.38 14518[4:Rew:14423.0,14099.0] || -> neq(sk1,sk1)*. % 11.17/11.38 14519[4:Rew:14423.0,14101.0] || neq(sk1,sk1)* -> . % 11.17/11.38 14532[4:MRR:14519.0,14518.0] || -> . % 11.17/11.38 14801[4:Spt:14532.0,459.1,14087.0] || equal(nil,sk2)** -> . % 11.17/11.38 14802[4:Spt:14532.0,459.0] || -> ssList(tl(sk2))*. % 11.17/11.38 14806[4:MRR:203.1,14801.0] || equal(nil,sk1)** -> . % 11.17/11.38 15244[3:Res:13861.1,11266.0] || -> equal(nil,sk1)**. % 11.17/11.38 15245[4:MRR:15244.0,14806.0] || -> . % 11.17/11.38 15246[3:Spt:15245.0,290.1] || -> duplicatefreeP(sk5)*. % 11.17/11.38 15248[4:Spt:242.3] || -> equal(sk5,nil)**. % 11.17/11.38 15259[4:Rew:15248.0,202.0] || -> equal(app(sk1,nil),sk2)**. % 11.17/11.38 16285[4:SpR:86.1,15259.0] ssList(sk1) || -> equal(sk2,sk1)**. % 11.17/11.38 16296[4:SSi:16285.0,199.0,1.0] || -> equal(sk2,sk1)**. % 11.17/11.38 16302[4:Rew:16296.0,7.0] || -> neq(sk1,nil)*. % 11.17/11.38 16459[4:MRR:16302.0,11266.0] || -> . % 11.17/11.38 16537[4:Spt:16459.0,242.3,15248.0] || equal(sk5,nil)** -> . % 11.17/11.38 16538[4:Spt:16459.0,242.0,242.1,242.2] ssItem(u) || strictorderedP(cons(u,sk5)) -> lt(u,hd(sk5))*. % 11.17/11.38 16557[5:Spt:416.3] || -> equal(nil,sk2)**. % 11.17/11.38 16676[5:Rew:16557.0,16537.0] || equal(sk5,sk2)** -> . % 11.17/11.38 16685[5:Rew:16557.0,12485.0] || equal(sk2,sk2) -> equal(sk5,sk1)**. % 11.17/11.38 16689[5:Rew:16557.0,12484.0] || equal(sk2,sk2) -> equal(nil,sk1)**. % 11.17/11.38 16733[5:Obv:16685.0] || -> equal(sk5,sk1)**. % 11.17/11.38 16883[5:Rew:16733.0,16676.0] || equal(sk2,sk1)** -> . % 11.17/11.38 16892[5:Obv:16689.0] || -> equal(nil,sk1)**. % 11.17/11.38 16893[5:Rew:16557.0,16892.0] || -> equal(sk2,sk1)**. % 11.17/11.38 16894[5:MRR:16893.0,16883.0] || -> . % 11.17/11.38 17077[5:Spt:16894.0,416.3,16557.0] || equal(nil,sk2)** -> . % 11.17/11.38 17078[5:Spt:16894.0,416.0,416.1,416.2] ssItem(u) || totalorderedP(cons(u,sk2)) -> leq(u,hd(sk2))*. % 11.17/11.38 17084[5:MRR:203.1,17077.0] || equal(nil,sk1)** -> . % 11.17/11.38 17646[0:Res:113.3,11266.0] ssList(sk1) ssList(nil) || -> equal(nil,sk1)**. % 11.17/11.38 17647[0:SSi:17646.1,17646.0,14.0,15.0,16.0,17.0,18.0,19.0,20.0,21.0,199.0,1.0] || -> equal(nil,sk1)**. % 11.17/11.38 17648[5:MRR:17647.0,17084.0] || -> . % 11.17/11.38 % SZS output end Refutation % 11.17/11.38 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_12 co1_13 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause61 clause72 clause73 clause77 clause100 clause102 clause117 clause118 clause119 clause134 clause135 clause137 % 11.17/11.38 %------------------------------------------------------------------------------