%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC275-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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:59 EDT 2022 % Result : Unsatisfiable 1.32s 1.49s % Output : Refutation 1.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWC275-1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n023.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 08:56:51 EDT 2022 % 0.13/0.35 % CPUTime : % 1.32/1.49 % 1.32/1.49 SPASS V 3.9 % 1.32/1.49 SPASS beiseite: Proof found. % 1.32/1.49 % SZS status Theorem % 1.32/1.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.32/1.49 SPASS derived 1903 clauses, backtracked 1652 clauses, performed 52 splits and kept 3296 clauses. % 1.32/1.49 SPASS allocated 77551 KBytes. % 1.32/1.49 SPASS spent 0:00:01.12 on the problem. % 1.32/1.49 0:00:00.04 for the input. % 1.32/1.49 0:00:00.00 for the FLOTTER CNF translation. % 1.32/1.49 0:00:00.01 for inferences. % 1.32/1.49 0:00:00.02 for the backtracking. % 1.32/1.49 0:00:00.88 for the reduction. % 1.32/1.49 % 1.32/1.49 % 1.32/1.49 Here is a proof with depth 2, length 86 : % 1.32/1.49 % SZS output start Refutation % 1.32/1.49 1[0:Inp] || -> ssList(sk1)*. % 1.32/1.49 2[0:Inp] || -> ssList(sk2)*. % 1.32/1.49 5[0:Inp] || -> equal(sk4,sk2)**. % 1.32/1.49 6[0:Inp] || -> equal(sk3,sk1)**. % 1.32/1.49 7[0:Inp] || totalorderedP(sk1)* -> . % 1.32/1.49 8[0:Inp] || equal(nil,sk4) -> equal(sk3,nil)**. % 1.32/1.49 9[0:Inp] || neq(sk4,nil)* -> ssItem(sk5). % 1.32/1.49 10[0:Inp] || neq(sk4,nil) -> equal(cons(sk5,nil),sk3)**. % 1.32/1.49 12[0:Inp] || -> equalelemsP(nil)*. % 1.32/1.49 13[0:Inp] || -> duplicatefreeP(nil)*. % 1.32/1.49 14[0:Inp] || -> strictorderedP(nil)*. % 1.32/1.49 15[0:Inp] || -> totalorderedP(nil)*. % 1.32/1.49 16[0:Inp] || -> strictorderP(nil)*. % 1.32/1.49 17[0:Inp] || -> totalorderP(nil)*. % 1.32/1.49 18[0:Inp] || -> cyclefreeP(nil)*. % 1.32/1.49 19[0:Inp] || -> ssList(nil)*. % 1.32/1.49 78[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.32/1.49 83[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.32/1.49 111[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 1.32/1.49 113[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 1.32/1.49 188[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.32/1.49 199[0:Rew:5.0,9.0] || neq(sk2,nil)* -> ssItem(sk5). % 1.32/1.49 201[0:Rew:6.0,8.1,5.0,8.0] || equal(nil,sk2)** -> equal(nil,sk1). % 1.32/1.49 202[0:Rew:6.0,10.1,5.0,10.0] || neq(sk2,nil) -> equal(cons(sk5,nil),sk1)**. % 1.32/1.49 288[0:Res:2.0,83.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.32/1.49 342[0:Res:2.0,111.1] ssList(u) || -> equal(sk2,u) neq(sk2,u)*. % 1.32/1.49 459[0:Res:1.0,83.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.32/1.49 474[0:Res:1.0,188.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.32/1.49 561[1:Spt:83.1] || -> ssItem(u)*. % 1.32/1.49 570[1:MRR:78.0,561.0] || -> totalorderedP(cons(u,nil))*. % 1.32/1.49 592[1:MRR:113.1,113.0,561.0] || -> equal(u,v) neq(u,v)*. % 1.32/1.49 764[2:Spt:474.5] || -> equal(nil,sk1)**. % 1.32/1.49 827[2:Rew:764.0,15.0] || -> totalorderedP(sk1)*. % 1.32/1.49 870[2:MRR:827.0,7.0] || -> . % 1.32/1.49 960[2:Spt:870.0,474.5,764.0] || equal(nil,sk1)** -> . % 1.32/1.49 961[2:Spt:870.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.32/1.49 966[2:MRR:201.1,960.0] || equal(nil,sk2)** -> . % 1.32/1.49 1069[1:SpR:202.1,570.0] || neq(sk2,nil)* -> totalorderedP(sk1). % 1.32/1.49 1077[1:MRR:1069.1,7.0] || neq(sk2,nil)* -> . % 1.32/1.49 1079[1:Res:592.1,1077.0] || -> equal(nil,sk2)**. % 1.32/1.49 1080[2:MRR:1079.0,966.0] || -> . % 1.32/1.49 1081[1:Spt:1080.0,83.0,83.2] ssList(u) || -> duplicatefreeP(u)*. % 1.32/1.49 1113[2:Spt:459.0] || -> ssItem(u)*. % 1.32/1.49 1120[2:MRR:78.0,1113.0] || -> totalorderedP(cons(u,nil))*. % 1.32/1.49 1142[2:MRR:113.1,113.0,1113.0] || -> equal(u,v) neq(u,v)*. % 1.32/1.49 1310[3:Spt:474.5] || -> equal(nil,sk1)**. % 1.32/1.49 1314[3:Rew:1310.0,15.0] || -> totalorderedP(sk1)*. % 1.32/1.49 1416[3:MRR:1314.0,7.0] || -> . % 1.32/1.49 1508[3:Spt:1416.0,474.5,1310.0] || equal(nil,sk1)** -> . % 1.32/1.49 1509[3:Spt:1416.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.32/1.49 1514[3:MRR:201.1,1508.0] || equal(nil,sk2)** -> . % 1.32/1.49 1616[2:SpR:202.1,1120.0] || neq(sk2,nil)* -> totalorderedP(sk1). % 1.32/1.49 1624[2:MRR:1616.1,7.0] || neq(sk2,nil)* -> . % 1.32/1.49 1626[2:Res:1142.1,1624.0] || -> equal(nil,sk2)**. % 1.32/1.49 1627[3:MRR:1626.0,1514.0] || -> . % 1.32/1.49 1628[2:Spt:1627.0,459.1] || -> duplicatefreeP(sk1)*. % 1.32/1.49 1631[3:Spt:288.0] || -> ssItem(u)*. % 1.32/1.49 1640[3:MRR:78.0,1631.0] || -> totalorderedP(cons(u,nil))*. % 1.32/1.49 1662[3:MRR:113.1,113.0,1631.0] || -> equal(u,v) neq(u,v)*. % 1.32/1.49 1826[4:Spt:474.5] || -> equal(nil,sk1)**. % 1.32/1.49 1831[4:Rew:1826.0,15.0] || -> totalorderedP(sk1)*. % 1.32/1.49 1932[4:MRR:1831.0,7.0] || -> . % 1.32/1.49 2024[4:Spt:1932.0,474.5,1826.0] || equal(nil,sk1)** -> . % 1.32/1.49 2025[4:Spt:1932.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.32/1.49 2030[4:MRR:201.1,2024.0] || equal(nil,sk2)** -> . % 1.32/1.49 2132[3:SpR:202.1,1640.0] || neq(sk2,nil)* -> totalorderedP(sk1). % 1.32/1.49 2140[3:MRR:2132.1,7.0] || neq(sk2,nil)* -> . % 1.32/1.49 2142[3:Res:1662.1,2140.0] || -> equal(nil,sk2)**. % 1.32/1.49 2143[4:MRR:2142.0,2030.0] || -> . % 1.32/1.49 2144[3:Spt:2143.0,288.1] || -> duplicatefreeP(sk2)*. % 1.32/1.49 2145[4:Spt:474.5] || -> equal(nil,sk1)**. % 1.32/1.49 2149[4:Rew:2145.0,15.0] || -> totalorderedP(sk1)*. % 1.32/1.49 2254[4:MRR:2149.0,7.0] || -> . % 1.32/1.49 2344[4:Spt:2254.0,474.5,2145.0] || equal(nil,sk1)** -> . % 1.32/1.49 2345[4:Spt:2254.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.32/1.49 2351[4:MRR:201.1,2344.0] || equal(nil,sk2)** -> . % 1.32/1.49 2401[5:Spt:199.0] || neq(sk2,nil)* -> . % 1.32/1.49 2464[5:Res:342.2,2401.0] ssList(nil) || -> equal(nil,sk2)**. % 1.32/1.49 2465[5:SSi:2464.0,19.0,18.0,17.0,16.0,15.0,14.0,13.0,12.0] || -> equal(nil,sk2)**. % 1.32/1.49 2466[5:MRR:2465.0,2351.0] || -> . % 1.32/1.49 2467[5:Spt:2466.0,199.0,2401.0] || -> neq(sk2,nil)*. % 1.32/1.49 2468[5:Spt:2466.0,199.1] || -> ssItem(sk5)*. % 1.32/1.49 2470[5:MRR:202.0,2467.0] || -> equal(cons(sk5,nil),sk1)**. % 1.32/1.49 2474[5:SpR:2470.0,78.1] ssItem(sk5) || -> totalorderedP(sk1)*. % 1.32/1.49 2479[5:SSi:2474.0,2468.0] || -> totalorderedP(sk1)*. % 1.32/1.49 2480[5:MRR:2479.0,7.0] || -> . % 1.32/1.49 % SZS output end Refutation % 1.32/1.49 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause67 clause72 clause100 clause102 clause177 % 1.32/1.49 %------------------------------------------------------------------------------