%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC014-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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:05 EDT 2022 % Result : Unsatisfiable 2.56s 2.75s % Output : Refutation 2.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWC014-1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 12 12:42:53 EDT 2022 % 0.12/0.34 % CPUTime : % 2.56/2.75 % 2.56/2.75 SPASS V 3.9 % 2.56/2.75 SPASS beiseite: Proof found. % 2.56/2.75 % SZS status Theorem % 2.56/2.75 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.56/2.75 SPASS derived 5604 clauses, backtracked 4153 clauses, performed 89 splits and kept 7189 clauses. % 2.56/2.75 SPASS allocated 80161 KBytes. % 2.56/2.75 SPASS spent 0:00:02.28 on the problem. % 2.56/2.75 0:00:00.04 for the input. % 2.56/2.75 0:00:00.00 for the FLOTTER CNF translation. % 2.56/2.75 0:00:00.02 for inferences. % 2.56/2.75 0:00:00.04 for the backtracking. % 2.56/2.75 0:00:01.98 for the reduction. % 2.56/2.75 % 2.56/2.75 % 2.56/2.75 Here is a proof with depth 3, length 96 : % 2.56/2.75 % SZS output start Refutation % 2.56/2.75 1[0:Inp] || -> ssList(sk1)*. % 2.56/2.75 2[0:Inp] || -> ssList(sk2)*. % 2.56/2.75 5[0:Inp] || -> equal(sk4,sk2)**. % 2.56/2.75 6[0:Inp] || -> equal(sk3,sk1)**. % 2.56/2.75 7[0:Inp] || -> neq(sk2,nil)* neq(sk2,nil)*. % 2.56/2.75 10[0:Inp] || -> ssItem(sk5) neq(sk2,nil)*. % 2.56/2.75 11[0:Inp] || -> ssList(sk6) neq(sk2,nil)*. % 2.56/2.75 14[0:Inp] ssList(u) ssList(v) || equal(sk2,u) equal(tl(sk2),v) equal(app(sk1,v),u)* neq(nil,sk2) neq(sk4,nil) -> . % 2.56/2.75 15[0:Inp] || neq(sk4,nil)* -> ssItem(sk5). % 2.56/2.75 16[0:Inp] || neq(sk4,nil)* -> ssList(sk6). % 2.56/2.75 17[0:Inp] || neq(sk4,nil) -> equal(cons(sk5,nil),sk3)**. % 2.56/2.75 18[0:Inp] || neq(sk4,nil) -> equal(app(cons(sk5,nil),sk6),sk4)**. % 2.56/2.75 19[0:Inp] || -> equalelemsP(nil)*. % 2.56/2.75 20[0:Inp] || -> duplicatefreeP(nil)*. % 2.56/2.75 21[0:Inp] || -> strictorderedP(nil)*. % 2.56/2.75 22[0:Inp] || -> totalorderedP(nil)*. % 2.56/2.75 23[0:Inp] || -> strictorderP(nil)*. % 2.56/2.75 24[0:Inp] || -> totalorderP(nil)*. % 2.56/2.75 25[0:Inp] || -> cyclefreeP(nil)*. % 2.56/2.75 26[0:Inp] || -> ssList(nil)*. % 2.56/2.75 90[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 2.56/2.75 92[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 2.56/2.75 114[0:Inp] ssList(u) ssItem(v) || -> equal(tl(cons(v,u)),u)**. % 2.56/2.75 116[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),nil)** -> . % 2.56/2.75 118[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 2.56/2.75 120[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 2.56/2.75 133[0:Inp] ssList(u) ssList(v) || neq(u,v)* equal(u,v) -> . % 2.56/2.75 135[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 2.56/2.75 151[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(app(tl(u),v),tl(app(u,v)))**. % 2.56/2.75 206[0:Rew:5.0,16.0] || neq(sk2,nil)* -> ssList(sk6). % 2.56/2.75 207[0:MRR:206.0,11.1] || -> ssList(sk6)*. % 2.56/2.75 208[0:Rew:5.0,15.0] || neq(sk2,nil)* -> ssItem(sk5). % 2.56/2.75 209[0:MRR:208.0,10.1] || -> ssItem(sk5)*. % 2.56/2.75 210[0:Obv:7.0] || -> neq(sk2,nil)*. % 2.56/2.75 211[0:Rew:6.0,17.1,5.0,17.0] || neq(sk2,nil) -> equal(cons(sk5,nil),sk1)**. % 2.56/2.75 212[0:MRR:211.0,210.0] || -> equal(cons(sk5,nil),sk1)**. % 2.56/2.75 213[0:Rew:212.0,18.1,5.0,18.1,5.0,18.0] || neq(sk2,nil) -> equal(app(sk1,sk6),sk2)**. % 2.56/2.75 214[0:MRR:213.0,210.0] || -> equal(app(sk1,sk6),sk2)**. % 2.56/2.75 219[0:Rew:5.0,14.6] ssList(u) ssList(v) || equal(sk2,u) equal(tl(sk2),v) equal(app(sk1,v),u)* neq(nil,sk2) neq(sk2,nil) -> . % 2.56/2.75 220[0:MRR:219.6,210.0] ssList(u) ssList(v) || equal(sk2,v) neq(nil,sk2) equal(tl(sk2),u) equal(app(sk1,u),v)* -> . % 2.56/2.75 352[0:Res:2.0,133.1] ssList(u) || neq(sk2,u)* equal(sk2,u) -> . % 2.56/2.75 509[0:Res:1.0,151.1] ssList(u) || -> equal(nil,sk1) equal(app(tl(sk1),u),tl(app(sk1,u)))**. % 2.56/2.75 572[1:Spt:90.1] || -> ssItem(u)*. % 2.56/2.75 602[1:MRR:120.1,120.0,572.0] || -> equal(u,v) neq(u,v)*. % 2.56/2.75 612[1:MRR:135.1,135.0,572.0] || neq(u,v)* equal(u,v) -> . % 2.56/2.75 699[1:MRR:116.1,572.0] ssList(u) || equal(cons(v,u),nil)** -> . % 2.56/2.75 701[1:MRR:114.1,572.0] ssList(u) || -> equal(tl(cons(v,u)),u)**. % 2.56/2.75 772[2:Spt:509.0,509.2] ssList(u) || -> equal(app(tl(sk1),u),tl(app(sk1,u)))**. % 2.56/2.75 776[3:Spt:220.0,220.1,220.2,220.4,220.5] ssList(u) ssList(v) || equal(sk2,v) equal(tl(sk2),u) equal(app(sk1,u),v)* -> . % 2.56/2.75 1002[3:SpL:214.0,776.4] ssList(sk6) ssList(u) || equal(sk2,u)* equal(tl(sk2),sk6)** equal(sk2,u)* -> . % 2.56/2.75 1005[3:Obv:1002.2] ssList(sk6) ssList(u) || equal(tl(sk2),sk6)** equal(sk2,u)* -> . % 2.56/2.75 1006[3:SSi:1005.0,207.0] ssList(u) || equal(tl(sk2),sk6)** equal(sk2,u)* -> . % 2.56/2.75 2219[1:Res:210.0,612.0] || equal(nil,sk2)** -> . % 2.56/2.75 2234[1:SpL:212.0,699.1] ssList(nil) || equal(nil,sk1)** -> . % 2.56/2.75 2319[1:SpR:212.0,701.1] ssList(nil) || -> equal(tl(sk1),nil)**. % 2.56/2.75 2320[1:SSi:2319.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,19.0] || -> equal(tl(sk1),nil)**. % 2.56/2.75 2324[2:Rew:2320.0,772.1] ssList(u) || -> equal(tl(app(sk1,u)),app(nil,u))**. % 2.56/2.75 2329[2:Rew:92.1,2324.1] ssList(u) || -> equal(tl(app(sk1,u)),u)**. % 2.56/2.75 2416[2:SpR:214.0,2329.1] ssList(sk6) || -> equal(tl(sk2),sk6)**. % 2.56/2.75 2421[2:SSi:2416.0,207.0] || -> equal(tl(sk2),sk6)**. % 2.56/2.75 2428[3:Rew:2421.0,1006.1] ssList(u) || equal(sk6,sk6)* equal(sk2,u)* -> . % 2.56/2.75 2434[3:Obv:2428.1] ssList(u) || equal(sk2,u)* -> . % 2.56/2.75 2483[3:EmS:2434.0,2.0] || equal(sk2,sk2)* -> . % 2.56/2.75 2485[3:Obv:2483.0] || -> . % 2.56/2.75 2487[3:Spt:2485.0,220.3] || neq(nil,sk2)* -> . % 2.56/2.75 2490[1:SSi:2234.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,19.0] || equal(nil,sk1)** -> . % 2.56/2.75 2532[3:Res:602.1,2487.0] || -> equal(nil,sk2)**. % 2.56/2.75 2533[3:MRR:2532.0,2219.0] || -> . % 2.56/2.75 2534[2:Spt:2533.0,509.1] || -> equal(nil,sk1)**. % 2.56/2.75 2535[2:MRR:2534.0,2490.0] || -> . % 2.56/2.75 2544[1:Spt:2535.0,90.0,90.2] ssList(u) || -> duplicatefreeP(u)*. % 2.56/2.75 2571[2:Spt:509.0,509.2] ssList(u) || -> equal(app(tl(sk1),u),tl(app(sk1,u)))**. % 2.56/2.75 2587[3:Spt:220.0,220.1,220.2,220.4,220.5] ssList(u) ssList(v) || equal(sk2,v) equal(tl(sk2),u) equal(app(sk1,u),v)* -> . % 2.56/2.75 2589[3:SpL:214.0,2587.4] ssList(sk6) ssList(u) || equal(sk2,u)* equal(tl(sk2),sk6)** equal(sk2,u)* -> . % 2.56/2.75 2593[3:Obv:2589.2] ssList(sk6) ssList(u) || equal(tl(sk2),sk6)** equal(sk2,u)* -> . % 2.56/2.75 2594[3:SSi:2593.0,207.0] ssList(u) || equal(tl(sk2),sk6)**+ equal(sk2,u)* -> . % 2.56/2.75 7125[0:Res:210.0,352.1] ssList(nil) || equal(nil,sk2)** -> . % 2.56/2.75 7205[0:SpL:212.0,116.2] ssList(nil) ssItem(sk5) || equal(nil,sk1)** -> . % 2.56/2.75 7224[0:SpR:212.0,114.2] ssList(nil) ssItem(sk5) || -> equal(tl(sk1),nil)**. % 2.56/2.75 7229[0:SSi:7224.1,7224.0,209.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,19.0] || -> equal(tl(sk1),nil)**. % 2.56/2.75 7232[2:Rew:7229.0,2571.1] ssList(u) || -> equal(tl(app(sk1,u)),app(nil,u))**. % 2.56/2.75 7234[2:Rew:92.1,7232.1] ssList(u) || -> equal(tl(app(sk1,u)),u)**. % 2.56/2.75 7379[2:SpR:214.0,7234.1] ssList(sk6) || -> equal(tl(sk2),sk6)**. % 2.56/2.75 7383[2:SSi:7379.0,207.0] || -> equal(tl(sk2),sk6)**. % 2.56/2.75 7385[3:Rew:7383.0,2594.1] ssList(u) || equal(sk6,sk6)* equal(sk2,u)* -> . % 2.56/2.75 7399[3:Obv:7385.1] ssList(u) || equal(sk2,u)* -> . % 2.56/2.75 7462[3:EmS:7399.0,2.0] || equal(sk2,sk2)* -> . % 2.56/2.75 7495[3:Obv:7462.0] || -> . % 2.56/2.75 7496[3:Spt:7495.0,220.3] || neq(nil,sk2)* -> . % 2.56/2.75 7506[0:SSi:7125.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,19.0] || equal(nil,sk2)** -> . % 2.56/2.75 7534[0:SSi:7205.1,7205.0,209.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,19.0] || equal(nil,sk1)** -> . % 2.56/2.75 7592[3:Res:118.3,7496.0] ssList(nil) ssList(sk2) || -> equal(nil,sk2)**. % 2.56/2.75 7596[3:SSi:7592.1,7592.0,2.0,26.0,25.0,24.0,23.0,22.0,21.0,20.0,19.0] || -> equal(nil,sk2)**. % 2.56/2.75 7597[3:MRR:7596.0,7506.0] || -> . % 2.56/2.75 7599[2:Spt:7597.0,509.1] || -> equal(nil,sk1)**. % 2.56/2.75 7600[2:MRR:7599.0,7534.0] || -> . % 2.56/2.75 % SZS output end Refutation % 2.56/2.75 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_10 co1_11 co1_14 co1_15 co1_16 co1_17 co1_18 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause72 clause74 clause96 clause98 clause100 clause102 clause115 clause117 clause133 % 2.56/2.75 %------------------------------------------------------------------------------