%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC273-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:58 EDT 2022 % Result : Unsatisfiable 274.12s 274.29s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC273-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 11 23:04:13 EDT 2022 % 0.13/0.34 % CPUTime : % 274.12/274.29 % 274.12/274.29 SPASS V 3.9 % 274.12/274.29 SPASS beiseite: Proof found. % 274.12/274.29 % SZS status Theorem % 274.12/274.29 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 274.12/274.29 SPASS derived 47712 clauses, backtracked 24037 clauses, performed 95 splits and kept 38340 clauses. % 274.12/274.29 SPASS allocated 145099 KBytes. % 274.12/274.29 SPASS spent 0:4:33.82 on the problem. % 274.12/274.29 0:00:00.04 for the input. % 274.12/274.29 0:00:00.00 for the FLOTTER CNF translation. % 274.12/274.29 0:00:00.92 for inferences. % 274.12/274.29 0:0:12.76 for the backtracking. % 274.12/274.29 0:4:19.04 for the reduction. % 274.12/274.29 % 274.12/274.29 % 274.12/274.29 Here is a proof with depth 3, length 103 : % 274.12/274.29 % SZS output start Refutation % 274.12/274.29 1[0:Inp] || -> ssList(sk1)*. % 274.12/274.29 2[0:Inp] || -> ssList(sk2)*. % 274.12/274.29 5[0:Inp] || -> equal(sk4,sk2)**. % 274.12/274.29 6[0:Inp] || -> equal(sk3,sk1)**. % 274.12/274.29 7[0:Inp] || -> segmentP(sk4,sk3)*. % 274.12/274.29 8[0:Inp] || -> strictorderedP(sk3)*. % 274.12/274.29 10[0:Inp] || totalorderedP(sk1)* -> . % 274.12/274.29 14[0:Inp] || -> totalorderedP(nil)*. % 274.12/274.29 22[0:Inp] || -> ssItem(skaf83(u))*. % 274.12/274.29 28[0:Inp] || -> ssList(skaf77(u))*. % 274.12/274.29 29[0:Inp] || -> ssList(skaf76(u))*. % 274.12/274.29 30[0:Inp] || -> ssList(skaf75(u))*. % 274.12/274.29 37[0:Inp] || -> ssList(skaf68(u))*. % 274.12/274.29 38[0:Inp] || -> ssList(skaf67(u))*. % 274.12/274.29 39[0:Inp] || -> ssList(skaf66(u))*. % 274.12/274.29 52[0:Inp] || -> ssList(skaf53(u))*. % 274.12/274.29 53[0:Inp] || -> ssList(skaf52(u))*. % 274.12/274.29 54[0:Inp] || -> ssList(skaf51(u))*. % 274.12/274.29 73[0:Inp] ssItem(u) || lt(u,u)* -> . % 274.12/274.29 82[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 274.12/274.29 90[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 274.12/274.29 95[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 274.12/274.29 96[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 274.12/274.29 97[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf50(u),skaf49(u))*. % 274.12/274.29 98[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf49(u),skaf50(u))*. % 274.12/274.29 101[0:Inp] ssList(u) || leq(skaf64(u),skaf65(u))* -> totalorderedP(u). % 274.12/274.29 113[0:Inp] ssItem(u) ssItem(v) || lt(u,v)* -> leq(u,v). % 274.12/274.29 140[0:Inp] ssItem(u) ssItem(v) || leq(u,v)*+ leq(v,u)* -> equal(u,v). % 274.12/274.29 167[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 274.12/274.29 172[0:Inp] ssList(u) || -> duplicatefreeP(u) equal(app(app(skaf75(u),cons(skaf74(u),skaf76(u))),cons(skaf74(u),skaf77(u))),u)**. % 274.12/274.29 174[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 274.12/274.29 177[0:Inp] ssList(u) || -> cyclefreeP(u) equal(app(app(skaf51(u),cons(skaf49(u),skaf52(u))),cons(skaf50(u),skaf53(u))),u)**. % 274.12/274.29 187[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). % 274.12/274.29 189[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)* -> . % 274.12/274.29 191[0:Inp] ssList(u) strictorderedP(u) ssItem(v) ssItem(w) ssList(x) ssList(y) ssList(z) || equal(app(app(x,cons(v,y)),cons(w,z)),u)* -> lt(v,w). % 274.12/274.29 196[0:Rew:6.0,8.0] || -> strictorderedP(sk1)*. % 274.12/274.29 198[0:Rew:6.0,7.0] || -> segmentP(sk4,sk1)*. % 274.12/274.29 200[0:Rew:5.0,198.0] || -> segmentP(sk2,sk1)*. % 274.12/274.29 303[0:Res:2.0,187.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 274.12/274.29 396[0:Res:1.0,174.0] || -> totalorderedP(sk1) equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 274.12/274.29 442[0:Res:1.0,101.0] || leq(skaf64(sk1),skaf65(sk1))* -> totalorderedP(sk1). % 274.12/274.29 448[0:Res:1.0,90.0] || segmentP(nil,sk1)* -> equal(nil,sk1). % 274.12/274.29 454[0:Res:1.0,97.0] || -> cyclefreeP(sk1) leq(skaf50(sk1),skaf49(sk1))*. % 274.12/274.29 475[0:Res:1.0,187.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 274.12/274.29 516[0:Res:1.0,96.1] ssItem(u) || -> ssList(cons(u,sk1))*. % 274.12/274.29 549[0:Res:1.0,191.6] ssList(u) ssList(v) ssList(w) ssItem(x) ssItem(y) strictorderedP(sk1) || equal(app(app(w,cons(y,v)),cons(x,u)),sk1)** -> lt(y,x). % 274.12/274.29 550[0:MRR:442.1,10.0] || leq(skaf64(sk1),skaf65(sk1))* -> . % 274.12/274.29 559[0:MRR:396.0,10.0] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 274.12/274.29 560[0:MRR:549.5,196.0] ssItem(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(u,x)),cons(v,y)),sk1)** -> lt(u,v). % 274.12/274.29 561[1:Spt:82.1] || -> ssItem(u)*. % 274.12/274.29 574[1:MRR:73.0,561.0] || lt(u,u)* -> . % 274.12/274.29 600[1:MRR:113.1,113.0,561.0] || lt(u,v)* -> leq(u,v). % 274.12/274.29 628[1:MRR:140.1,140.0,561.0] || leq(u,v)*+ leq(v,u)* -> equal(u,v). % 274.12/274.29 674[1:MRR:560.1,560.0,561.0] ssList(u) ssList(v) ssList(w) || equal(app(app(u,cons(x,v)),cons(y,w)),sk1)** -> lt(x,y). % 274.12/274.29 714[1:MRR:189.2,561.0] ssList(u) duplicatefreeP(u) ssList(v) ssList(w) ssList(x) || equal(app(app(v,cons(y,w)),cons(y,x)),u)* -> . % 274.12/274.29 741[1:MRR:191.3,191.2,561.0] ssList(u) strictorderedP(u) ssList(v) ssList(w) ssList(x) || equal(app(app(v,cons(y,w)),cons(z,x)),u)* -> lt(y,z). % 274.12/274.29 762[2:Spt:303.5] || -> equal(nil,sk2)**. % 274.12/274.29 807[2:Rew:762.0,448.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 274.12/274.29 821[2:Rew:762.0,14.0] || -> totalorderedP(sk2)*. % 274.12/274.29 895[2:Rew:762.0,807.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 274.12/274.29 896[2:MRR:895.0,200.0] || -> equal(sk2,sk1)**. % 274.12/274.29 983[2:Rew:896.0,821.0] || -> totalorderedP(sk1)*. % 274.12/274.29 1002[2:MRR:983.0,10.0] || -> . % 274.12/274.29 1176[2:Spt:1002.0,303.5,762.0] || equal(nil,sk2)** -> . % 274.12/274.29 1177[2:Spt:1002.0,303.0,303.1,303.2,303.3,303.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 274.12/274.29 1191[3:Spt:475.5] || -> equal(nil,sk1)**. % 274.12/274.29 1196[3:Rew:1191.0,14.0] || -> totalorderedP(sk1)*. % 274.12/274.29 1279[3:MRR:1196.0,10.0] || -> . % 274.12/274.29 1358[3:Spt:1279.0,475.5,1191.0] || equal(nil,sk1)** -> . % 274.12/274.29 1359[3:Spt:1279.0,475.0,475.1,475.2,475.3,475.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 274.12/274.29 1629[4:Spt:454.0] || -> cyclefreeP(sk1)*. % 274.12/274.29 1777[1:Res:98.2,628.0] ssList(u) || leq(skaf50(u),skaf49(u))* -> cyclefreeP(u) equal(skaf49(u),skaf50(u)). % 274.12/274.29 1779[1:MRR:1777.1,97.2] ssList(u) || -> cyclefreeP(u) equal(skaf49(u),skaf50(u))**. % 274.12/274.29 1784[1:Rew:1779.2,177.2] ssList(u) || -> cyclefreeP(u) equal(app(app(skaf51(u),cons(skaf50(u),skaf52(u))),cons(skaf50(u),skaf53(u))),u)**. % 274.12/274.29 5207[1:SpL:1784.2,714.5] ssList(u) ssList(v) duplicatefreeP(v) ssList(skaf51(u)) ssList(skaf52(u)) ssList(skaf53(u)) || equal(u,v)* -> cyclefreeP(u)*. % 274.12/274.29 5209[1:SSi:5207.5,5207.4,5207.3,52.0,53.0,54.0] ssList(u) ssList(v) duplicatefreeP(v) || equal(u,v)*+ -> cyclefreeP(u)*. % 274.12/274.29 5375[1:SpL:172.2,741.5] ssList(u) ssList(v) strictorderedP(v) ssList(skaf75(u)) ssList(skaf76(u)) ssList(skaf77(u)) || equal(u,v)* -> duplicatefreeP(u) lt(skaf74(u),skaf74(u))*. % 274.12/274.29 5384[1:SSi:5375.5,5375.4,5375.3,28.0,29.0,30.0] ssList(u) ssList(v) strictorderedP(v) || equal(u,v)* -> duplicatefreeP(u) lt(skaf74(u),skaf74(u))*. % 274.12/274.29 5385[1:MRR:5384.5,574.0] ssList(u) ssList(v) strictorderedP(v) || equal(u,v)*+ -> duplicatefreeP(u)*. % 274.12/274.29 11521[1:EqR:5209.3] ssList(u) ssList(u) duplicatefreeP(u) || -> cyclefreeP(u)*. % 274.12/274.29 11522[1:Obv:11521.0] ssList(u) duplicatefreeP(u) || -> cyclefreeP(u)*. % 274.12/274.29 12015[1:EqR:5385.3] ssList(u) ssList(u) strictorderedP(u) || -> duplicatefreeP(u)*. % 274.12/274.29 12016[1:Obv:12015.0] ssList(u) strictorderedP(u) || -> duplicatefreeP(u)*. % 274.12/274.29 52977[1:SpL:559.0,674.3] ssList(skaf66(sk1)) ssList(skaf67(sk1)) ssList(skaf68(sk1)) || equal(sk1,sk1) -> lt(skaf64(sk1),skaf65(sk1))*. % 274.12/274.29 52981[1:Obv:52977.3] ssList(skaf66(sk1)) ssList(skaf67(sk1)) ssList(skaf68(sk1)) || -> lt(skaf64(sk1),skaf65(sk1))*. % 274.12/274.29 54863[4:SSi:52981.2,52981.1,52981.0,37.0,196.0,1.0,1629.0,38.0,196.0,1.0,1629.0,39.0,196.0,1.0,1629.0] || -> lt(skaf64(sk1),skaf65(sk1))*. % 274.12/274.29 56518[4:Res:54863.0,600.0] || -> leq(skaf64(sk1),skaf65(sk1))*. % 274.12/274.29 56520[4:MRR:56518.0,550.0] || -> . % 274.12/274.29 56522[4:Spt:56520.0,454.0,1629.0] || cyclefreeP(sk1)* -> . % 274.12/274.29 56523[4:Spt:56520.0,454.1] || -> leq(skaf50(sk1),skaf49(sk1))*. % 274.12/274.29 57603[4:Res:11522.2,56522.0] ssList(sk1) duplicatefreeP(sk1) || -> . % 274.12/274.29 57613[4:SSi:57603.1,57603.0,12016.0,196.0,1.0,196.0,1.2] || -> . % 274.12/274.29 57616[1:Spt:57613.0,82.0,82.2] ssList(u) || -> duplicatefreeP(u)*. % 274.12/274.29 57717[1:MRR:189.1,57616.1] ssList(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 274.12/274.29 83772[0:SpR:167.3,95.2] ssList(u) ssList(v) ssItem(w) ssList(cons(w,v)) ssList(u) || -> ssList(cons(w,app(v,u)))*. % 274.12/274.29 83808[0:Obv:83772.0] ssList(u) ssItem(v) ssList(cons(v,u)) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 274.12/274.29 83809[0:SSi:83808.2,96.2] ssList(u) ssItem(v) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 274.12/274.29 84810[1:EqR:57717.5] ssList(app(app(u,cons(v,w)),cons(v,x))) ssItem(v) ssList(u) ssList(w) ssList(x) || -> . % 274.12/274.29 84839[1:SSi:84810.0,95.2,95.2,96.2,96.2] ssItem(u) ssList(v) ssLiCputime limit exceeded (core dumped) %------------------------------------------------------------------------------