%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC288-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:03:04 EDT 2022 % Result : Unsatisfiable 1.67s 1.88s % Output : Refutation 1.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC288-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n027.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 : Sun Jun 12 12:12:46 EDT 2022 % 0.12/0.33 % CPUTime : % 1.67/1.88 % 1.67/1.88 SPASS V 3.9 % 1.67/1.88 SPASS beiseite: Proof found. % 1.67/1.88 % SZS status Theorem % 1.67/1.88 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.67/1.88 SPASS derived 2754 clauses, backtracked 2870 clauses, performed 71 splits and kept 4880 clauses. % 1.67/1.88 SPASS allocated 78268 KBytes. % 1.67/1.88 SPASS spent 0:00:01.52 on the problem. % 1.67/1.88 0:00:00.04 for the input. % 1.67/1.88 0:00:00.00 for the FLOTTER CNF translation. % 1.67/1.88 0:00:00.00 for inferences. % 1.67/1.88 0:00:00.02 for the backtracking. % 1.67/1.88 0:00:01.27 for the reduction. % 1.67/1.88 % 1.67/1.88 % 1.67/1.88 Here is a proof with depth 2, length 58 : % 1.67/1.88 % SZS output start Refutation % 1.67/1.88 1[0:Inp] || -> ssList(sk1)*. % 1.67/1.88 2[0:Inp] || -> ssList(sk2)*. % 1.67/1.88 6[0:Inp] || -> equal(sk3,sk1)**. % 1.67/1.88 7[0:Inp] || strictorderedP(sk1)* -> . % 1.67/1.88 9[0:Inp] || -> ssItem(sk5)* equal(nil,sk3). % 1.67/1.88 18[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk3). % 1.67/1.88 24[0:Inp] || -> strictorderedP(nil)*. % 1.67/1.88 87[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 1.67/1.88 93[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.67/1.88 198[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). % 1.67/1.88 213[0:Rew:6.0,9.1] || -> ssItem(sk5)* equal(nil,sk1). % 1.67/1.88 215[0:Rew:6.0,18.1,6.0,18.0] || -> equal(nil,sk1) equal(cons(sk5,nil),sk1)**. % 1.67/1.88 308[0:Res:2.0,93.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.67/1.88 479[0:Res:1.0,93.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.67/1.88 494[0:Res:1.0,198.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.67/1.88 576[1:Spt:93.1] || -> ssItem(u)*. % 1.67/1.88 586[1:MRR:87.0,576.0] || -> strictorderedP(cons(u,nil))*. % 1.67/1.88 783[2:Spt:494.5] || -> equal(nil,sk1)**. % 1.67/1.88 846[2:Rew:783.0,24.0] || -> strictorderedP(sk1)*. % 1.67/1.88 890[2:MRR:846.0,7.0] || -> . % 1.67/1.88 1196[2:Spt:890.0,494.5,783.0] || equal(nil,sk1)** -> . % 1.67/1.88 1197[2:Spt:890.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.67/1.88 1204[2:MRR:215.0,1196.0] || -> equal(cons(sk5,nil),sk1)**. % 1.67/1.88 1455[2:SpR:1204.0,586.0] || -> strictorderedP(sk1)*. % 1.67/1.88 1459[2:MRR:1455.0,7.0] || -> . % 1.67/1.88 1462[1:Spt:1459.0,93.0,93.2] ssList(u) || -> duplicatefreeP(u)*. % 1.67/1.88 1478[2:Spt:479.0] || -> ssItem(u)*. % 1.67/1.88 1484[2:MRR:87.0,1478.0] || -> strictorderedP(cons(u,nil))*. % 1.67/1.88 1679[3:Spt:494.5] || -> equal(nil,sk1)**. % 1.67/1.88 1685[3:Rew:1679.0,24.0] || -> strictorderedP(sk1)*. % 1.67/1.88 1786[3:MRR:1685.0,7.0] || -> . % 1.67/1.88 2093[3:Spt:1786.0,494.5,1679.0] || equal(nil,sk1)** -> . % 1.67/1.88 2094[3:Spt:1786.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.67/1.88 2101[3:MRR:215.0,2093.0] || -> equal(cons(sk5,nil),sk1)**. % 1.67/1.88 2347[3:SpR:2101.0,1484.0] || -> strictorderedP(sk1)*. % 1.67/1.88 2354[3:MRR:2347.0,7.0] || -> . % 1.67/1.88 2355[2:Spt:2354.0,479.1] || -> duplicatefreeP(sk1)*. % 1.67/1.88 2358[3:Spt:308.0] || -> ssItem(u)*. % 1.67/1.88 2368[3:MRR:87.0,2358.0] || -> strictorderedP(cons(u,nil))*. % 1.67/1.88 2557[4:Spt:494.5] || -> equal(nil,sk1)**. % 1.67/1.88 2563[4:Rew:2557.0,24.0] || -> strictorderedP(sk1)*. % 1.67/1.88 2664[4:MRR:2563.0,7.0] || -> . % 1.67/1.88 2970[4:Spt:2664.0,494.5,2557.0] || equal(nil,sk1)** -> . % 1.67/1.88 2971[4:Spt:2664.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.67/1.88 2978[4:MRR:215.0,2970.0] || -> equal(cons(sk5,nil),sk1)**. % 1.67/1.88 3223[4:SpR:2978.0,2368.0] || -> strictorderedP(sk1)*. % 1.67/1.88 3227[4:MRR:3223.0,7.0] || -> . % 1.67/1.88 3229[3:Spt:3227.0,308.1] || -> duplicatefreeP(sk2)*. % 1.67/1.88 3230[4:Spt:494.5] || -> equal(nil,sk1)**. % 1.67/1.88 3236[4:Rew:3230.0,24.0] || -> strictorderedP(sk1)*. % 1.67/1.88 3339[4:MRR:3236.0,7.0] || -> . % 1.67/1.88 3429[4:Spt:3339.0,494.5,3230.0] || equal(nil,sk1)** -> . % 1.67/1.88 3430[4:Spt:3339.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.67/1.88 3433[4:MRR:213.1,3429.0] || -> ssItem(sk5)*. % 1.67/1.88 3439[4:MRR:215.0,3429.0] || -> equal(cons(sk5,nil),sk1)**. % 1.67/1.88 3699[4:SpR:3439.0,87.1] ssItem(sk5) || -> strictorderedP(sk1)*. % 1.67/1.88 3700[4:SSi:3699.0,3433.0] || -> strictorderedP(sk1)*. % 1.67/1.88 3701[4:MRR:3700.0,7.0] || -> . % 1.67/1.88 % SZS output end Refutation % 1.67/1.88 Formulae used in the proof : co1_1 co1_2 co1_6 co1_7 co1_9 co1_18 clause3 clause66 clause72 clause177 % 1.67/1.88 %------------------------------------------------------------------------------