%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC001-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:00:59 EDT 2022 % Result : Unsatisfiable 1.52s 1.73s % Output : Refutation 1.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWC001-1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n023.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 : Sat Jun 11 21:05:07 EDT 2022 % 0.12/0.33 % CPUTime : % 1.52/1.73 % 1.52/1.73 SPASS V 3.9 % 1.52/1.73 SPASS beiseite: Proof found. % 1.52/1.73 % SZS status Theorem % 1.52/1.73 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.52/1.73 SPASS derived 2270 clauses, backtracked 2220 clauses, performed 61 splits and kept 3981 clauses. % 1.52/1.73 SPASS allocated 77861 KBytes. % 1.52/1.73 SPASS spent 0:00:01.38 on the problem. % 1.52/1.73 0:00:00.04 for the input. % 1.52/1.73 0:00:00.00 for the FLOTTER CNF translation. % 1.52/1.73 0:00:00.01 for inferences. % 1.52/1.73 0:00:00.02 for the backtracking. % 1.52/1.73 0:00:01.09 for the reduction. % 1.52/1.73 % 1.52/1.73 % 1.52/1.73 Here is a proof with depth 2, length 72 : % 1.52/1.73 % SZS output start Refutation % 1.52/1.73 1[0:Inp] || -> ssList(sk1)*. % 1.52/1.73 2[0:Inp] || -> ssList(sk2)*. % 1.52/1.73 5[0:Inp] || -> equal(sk4,sk2)**. % 1.52/1.73 6[0:Inp] || -> equal(sk3,sk1)**. % 1.52/1.73 7[0:Inp] || -> duplicatefreeP(sk3)*. % 1.52/1.73 8[0:Inp] ssItem(u) || memberP(sk3,u) -> memberP(sk4,u)*. % 1.52/1.73 9[0:Inp] ssItem(u) || memberP(sk4,u)* -> memberP(sk3,u). % 1.52/1.73 10[0:Inp] || duplicatefreeP(sk1) -> ssItem(sk5)*. % 1.52/1.73 11[0:Inp] || duplicatefreeP(sk1) -> memberP(sk2,sk5)* memberP(sk1,sk5). % 1.52/1.73 12[0:Inp] || memberP(sk2,sk5)* memberP(sk1,sk5) duplicatefreeP(sk1) -> . % 1.52/1.73 83[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 1.52/1.73 84[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.52/1.73 189[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.52/1.73 198[0:Rew:6.0,7.0] || -> duplicatefreeP(sk1)*. % 1.52/1.73 201[0:MRR:10.0,198.0] || -> ssItem(sk5)*. % 1.52/1.73 202[0:MRR:11.0,198.0] || -> memberP(sk1,sk5) memberP(sk2,sk5)*. % 1.52/1.73 203[0:Rew:6.0,9.2,5.0,9.1] ssItem(u) || memberP(sk2,u)* -> memberP(sk1,u). % 1.52/1.73 204[0:Rew:5.0,8.2,6.0,8.1] ssItem(u) || memberP(sk1,u) -> memberP(sk2,u)*. % 1.52/1.73 205[0:MRR:12.2,198.0] || memberP(sk1,sk5) memberP(sk2,sk5)* -> . % 1.52/1.73 291[0:Res:2.0,84.0] || -> ssItem(u)* duplicatefreeP(sk2). % 1.52/1.73 306[0:Res:2.0,189.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 1.52/1.73 477[0:Res:1.0,189.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.52/1.73 557[1:Spt:84.1] || -> ssItem(u)*. % 1.52/1.73 579[1:MRR:203.0,557.0] || memberP(sk2,u)* -> memberP(sk1,u). % 1.52/1.73 580[1:MRR:204.0,557.0] || memberP(sk1,u) -> memberP(sk2,u)*. % 1.52/1.73 755[1:MRR:202.1,579.0] || -> memberP(sk1,sk5)*. % 1.52/1.73 756[1:MRR:205.0,579.1] || memberP(sk2,sk5)* -> . % 1.52/1.73 1212[1:Res:580.1,756.0] || memberP(sk1,sk5)* -> . % 1.52/1.73 1214[1:MRR:1212.0,755.0] || -> . % 1.52/1.73 1215[1:Spt:1214.0,84.0,84.2] ssList(u) || -> duplicatefreeP(u)*. % 1.52/1.73 1233[2:Spt:291.0] || -> ssItem(u)*. % 1.52/1.73 1255[2:MRR:204.0,1233.0] || memberP(sk1,u) -> memberP(sk2,u)*. % 1.52/1.73 1256[2:MRR:203.0,1233.0] || memberP(sk2,u)* -> memberP(sk1,u). % 1.52/1.73 1431[2:MRR:202.0,1255.0] || -> memberP(sk2,sk5)*. % 1.52/1.73 1432[2:MRR:205.1,1255.1] || memberP(sk1,sk5)* -> . % 1.52/1.73 1880[2:Res:1431.0,1256.0] || -> memberP(sk1,sk5)*. % 1.52/1.73 1882[2:MRR:1880.0,1432.0] || -> . % 1.52/1.73 1883[2:Spt:1882.0,291.1] || -> duplicatefreeP(sk2)*. % 1.52/1.73 1885[3:Spt:306.5] || -> equal(nil,sk2)**. % 1.52/1.73 1967[3:Rew:1885.0,83.1] ssItem(u) || memberP(sk2,u)* -> . % 1.52/1.73 2021[3:MRR:204.2,1967.1] ssItem(u) || memberP(sk1,u)* -> . % 1.52/1.73 2102[4:Spt:202.0] || -> memberP(sk1,sk5)*. % 1.52/1.73 2364[4:Res:2102.0,2021.1] ssItem(sk5) || -> . % 1.52/1.73 2365[4:SSi:2364.0,201.0] || -> . % 1.52/1.73 2366[4:Spt:2365.0,202.0,2102.0] || memberP(sk1,sk5)* -> . % 1.52/1.73 2367[4:Spt:2365.0,202.1] || -> memberP(sk2,sk5)*. % 1.52/1.73 2629[4:Res:2367.0,1967.1] ssItem(sk5) || -> . % 1.52/1.73 2630[4:SSi:2629.0,201.0] || -> . % 1.52/1.73 2631[3:Spt:2630.0,306.5,1885.0] || equal(nil,sk2)** -> . % 1.52/1.73 2632[3:Spt:2630.0,306.0,306.1,306.2,306.3,306.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.52/1.73 2647[4:Spt:477.5] || -> equal(nil,sk1)**. % 1.52/1.73 2693[4:Rew:2647.0,83.1] ssItem(u) || memberP(sk1,u)* -> . % 1.52/1.73 2761[4:MRR:203.2,2693.1] ssItem(u) || memberP(sk2,u)* -> . % 1.52/1.73 2834[5:Spt:202.0] || -> memberP(sk1,sk5)*. % 1.52/1.73 2843[5:Res:2834.0,2693.1] ssItem(sk5) || -> . % 1.52/1.73 2844[5:SSi:2843.0,201.0] || -> . % 1.52/1.73 2845[5:Spt:2844.0,202.0,2834.0] || memberP(sk1,sk5)* -> . % 1.52/1.73 2846[5:Spt:2844.0,202.1] || -> memberP(sk2,sk5)*. % 1.52/1.73 2847[5:Res:2846.0,2761.1] ssItem(sk5) || -> . % 1.52/1.73 2848[5:SSi:2847.0,201.0] || -> . % 1.52/1.73 2849[4:Spt:2848.0,477.5,2647.0] || equal(nil,sk1)** -> . % 1.52/1.73 2850[4:Spt:2848.0,477.0,477.1,477.2,477.3,477.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.52/1.73 2887[5:Spt:202.0] || -> memberP(sk1,sk5)*. % 1.52/1.73 2888[5:MRR:205.0,2887.0] || memberP(sk2,sk5)* -> . % 1.52/1.73 2964[5:Res:204.2,2888.0] ssItem(sk5) || memberP(sk1,sk5)* -> . % 1.52/1.73 2965[5:SSi:2964.0,201.0] || memberP(sk1,sk5)* -> . % 1.52/1.73 2966[5:MRR:2965.0,2887.0] || -> . % 1.52/1.73 2967[5:Spt:2966.0,202.0,2887.0] || memberP(sk1,sk5)* -> . % 1.52/1.73 2968[5:Spt:2966.0,202.1] || -> memberP(sk2,sk5)*. % 1.52/1.73 2970[5:Res:2968.0,203.1] ssItem(sk5) || -> memberP(sk1,sk5)*. % 1.52/1.73 2971[5:SSi:2970.0,201.0] || -> memberP(sk1,sk5)*. % 1.52/1.73 2972[5:MRR:2971.0,2967.0] || -> . % 1.52/1.73 % SZS output end Refutation % 1.52/1.73 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_12 clause71 clause72 clause177 % 1.52/1.73 %------------------------------------------------------------------------------