%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC013-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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 7.56s 7.79s % Output : Refutation 10.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWC013-1 : TPTP v8.1.0. Released v2.4.0. % 0.12/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n022.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 04:41:18 EDT 2022 % 0.12/0.34 % CPUTime : % 7.56/7.79 % 7.56/7.79 SPASS V 3.9 % 7.56/7.79 SPASS beiseite: Proof found. % 7.56/7.79 % SZS status Theorem % 7.56/7.79 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 7.56/7.79 SPASS derived 16889 clauses, backtracked 6608 clauses, performed 106 splits and kept 14077 clauses. % 7.56/7.79 SPASS allocated 93061 KBytes. % 7.56/7.79 SPASS spent 0:00:07.42 on the problem. % 7.56/7.79 0:00:00.04 for the input. % 7.56/7.79 0:00:00.00 for the FLOTTER CNF translation. % 7.56/7.79 0:00:00.14 for inferences. % 7.56/7.79 0:00:00.19 for the backtracking. % 7.56/7.79 0:00:06.74 for the reduction. % 7.56/7.79 % 7.56/7.79 % 7.56/7.79 Here is a proof with depth 3, length 118 : % 7.56/7.79 % SZS output start Refutation % 7.56/7.79 1[0:Inp] || -> ssList(sk1)*. % 7.56/7.79 2[0:Inp] || -> ssList(sk2)*. % 7.56/7.79 5[0:Inp] || -> equal(sk4,sk2)**. % 7.56/7.79 6[0:Inp] || -> equal(sk3,sk1)**. % 7.56/7.79 7[0:Inp] || -> neq(sk2,nil)* neq(sk2,nil)*. % 7.56/7.79 11[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)* equal(hd(sk4),v) neq(nil,sk4) neq(sk4,nil) -> equal(sk3,u). % 7.56/7.79 12[0:Inp] ssList(u) ssItem(v) || equal(sk1,u) equal(cons(v,nil),u)* equal(hd(sk2),v) neq(nil,sk2) neq(sk4,nil) -> . % 7.56/7.79 13[0:Inp] || -> equalelemsP(nil)*. % 7.56/7.79 14[0:Inp] || -> duplicatefreeP(nil)*. % 7.56/7.79 15[0:Inp] || -> strictorderedP(nil)*. % 7.56/7.79 16[0:Inp] || -> totalorderedP(nil)*. % 7.56/7.79 17[0:Inp] || -> strictorderP(nil)*. % 7.56/7.79 18[0:Inp] || -> totalorderP(nil)*. % 7.56/7.79 19[0:Inp] || -> cyclefreeP(nil)*. % 7.56/7.79 20[0:Inp] || -> ssList(nil)*. % 7.56/7.79 59[0:Inp] || -> ssItem(skaf44(u))*. % 7.56/7.79 66[0:Inp] || equal(skac2,skac3)** -> . % 7.56/7.79 76[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 7.56/7.79 77[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 7.56/7.79 78[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 7.56/7.79 79[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 7.56/7.79 80[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 7.56/7.79 81[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 7.56/7.79 82[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 7.56/7.79 84[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 7.56/7.79 86[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 7.56/7.79 97[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 7.56/7.79 98[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 7.56/7.79 109[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 7.56/7.79 114[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 7.56/7.79 128[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 7.56/7.79 129[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 7.56/7.79 132[0:Inp] ssList(u) ssItem(v) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 7.56/7.79 135[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 7.56/7.79 169[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 7.56/7.79 182[0:Inp] ssList(u) ssList(v) ssItem(w) ssItem(x) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 7.56/7.79 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). % 7.56/7.79 191[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)* -> . % 7.56/7.79 200[0:Obv:7.0] || -> neq(sk2,nil)*. % 7.56/7.79 205[0:Rew:6.0,11.6,5.0,11.5,5.0,11.4,5.0,11.3] ssList(u) ssItem(v) || equal(cons(v,nil),u)* equal(hd(sk2),v) neq(nil,sk2) neq(sk2,nil) -> equal(sk1,u). % 7.56/7.79 206[0:MRR:205.5,200.0] ssItem(u) ssList(v) || neq(nil,sk2) equal(hd(sk2),u) equal(cons(u,nil),v)* -> equal(sk1,v). % 7.56/7.79 207[0:Rew:5.0,12.6] ssList(u) ssItem(v) || equal(sk1,u) equal(cons(v,nil),u)* equal(hd(sk2),v) neq(nil,sk2) neq(sk2,nil) -> . % 7.56/7.79 208[0:MRR:207.6,200.0] ssItem(u) ssList(v) || equal(sk1,v) neq(nil,sk2) equal(hd(sk2),u) equal(cons(u,nil),v)* -> . % 7.56/7.79 307[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). % 7.56/7.79 336[0:Res:2.0,135.1] ssList(u) || -> equal(nil,sk2) equal(hd(app(sk2,u)),hd(sk2))**. % 7.56/7.79 343[0:Res:2.0,109.1] ssItem(u) || -> equal(hd(cons(u,sk2)),u)**. % 7.56/7.79 348[0:Res:2.0,98.1] ssItem(u) || -> ssList(cons(u,sk2))*. % 7.56/7.79 389[0:Res:1.0,208.0] ssItem(u) || equal(sk1,sk1) equal(cons(u,nil),sk1)** equal(hd(sk2),u) neq(nil,sk2) -> . % 7.56/7.79 559[0:Obv:389.1] ssItem(u) || neq(nil,sk2) equal(hd(sk2),u) equal(cons(u,nil),sk1)** -> . % 7.56/7.79 562[1:Spt:84.1] || -> ssItem(u)*. % 7.56/7.79 566[1:MRR:348.0,562.0] || -> ssList(cons(u,sk2))*. % 7.56/7.79 568[1:MRR:82.0,562.0] || -> cyclefreeP(cons(u,nil))*. % 7.56/7.79 569[1:MRR:81.0,562.0] || -> totalorderP(cons(u,nil))*. % 7.56/7.79 570[1:MRR:80.0,562.0] || -> strictorderP(cons(u,nil))*. % 7.56/7.79 571[1:MRR:79.0,562.0] || -> totalorderedP(cons(u,nil))*. % 7.56/7.79 572[1:MRR:78.0,562.0] || -> strictorderedP(cons(u,nil))*. % 7.56/7.79 573[1:MRR:77.0,562.0] || -> duplicatefreeP(cons(u,nil))*. % 7.56/7.79 574[1:MRR:76.0,562.0] || -> equalelemsP(cons(u,nil))*. % 7.56/7.79 582[1:MRR:343.0,562.0] || -> equal(hd(cons(u,sk2)),u)**. % 7.56/7.79 592[1:MRR:114.1,114.0,562.0] || -> equal(u,v) neq(u,v)*. % 7.56/7.79 602[1:MRR:129.1,129.0,562.0] || neq(u,v)* equal(u,v) -> . % 7.56/7.79 634[1:MRR:559.0,562.0] || neq(nil,sk2) equal(hd(sk2),u) equal(cons(u,nil),sk1)** -> . % 7.56/7.79 674[1:MRR:206.0,562.0] ssList(u) || neq(nil,sk2) equal(hd(sk2),v) equal(cons(v,nil),u)* -> equal(sk1,u). % 7.56/7.79 691[1:MRR:98.1,562.0] ssList(u) || -> ssList(cons(v,u))*. % 7.56/7.79 696[1:MRR:128.1,562.0] ssList(u) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 7.56/7.79 697[1:MRR:132.1,562.0] ssList(u) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 7.56/7.79 761[1:MRR:182.3,182.2,562.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 7.56/7.79 764[2:Spt:336.0,336.2] ssList(u) || -> equal(hd(app(sk2,u)),hd(sk2))**. % 7.56/7.79 770[3:Spt:307.5] || -> equal(nil,sk2)**. % 7.56/7.79 850[3:Rew:770.0,86.1] ssList(u) || -> equal(app(sk2,u),u)**. % 7.56/7.79 856[3:Rew:770.0,568.0] || -> cyclefreeP(cons(u,sk2))*. % 7.56/7.79 857[3:Rew:770.0,569.0] || -> totalorderP(cons(u,sk2))*. % 7.56/7.79 858[3:Rew:770.0,570.0] || -> strictorderP(cons(u,sk2))*. % 7.56/7.79 859[3:Rew:770.0,571.0] || -> totalorderedP(cons(u,sk2))*. % 7.56/7.79 860[3:Rew:770.0,572.0] || -> strictorderedP(cons(u,sk2))*. % 7.56/7.79 861[3:Rew:770.0,573.0] || -> duplicatefreeP(cons(u,sk2))*. % 7.56/7.79 862[3:Rew:770.0,574.0] || -> equalelemsP(cons(u,sk2))*. % 7.56/7.79 875[3:Rew:770.0,697.1] ssList(u) || -> equal(app(cons(v,sk2),u),cons(v,u))**. % 7.56/7.79 916[3:Rew:850.1,764.1] ssList(u) || -> equal(hd(u),hd(sk2))*. % 7.56/7.79 1622[3:SpR:916.1,582.0] ssList(cons(u,sk2)) || -> equal(hd(sk2),u)*. % 7.56/7.79 1628[3:SSi:1622.0,862.0,861.0,860.0,859.0,858.0,857.0,856.0,566.0] || -> equal(hd(sk2),u)*. % 7.56/7.79 1837[3:Rew:1628.0,875.1] ssList(u) || -> equal(cons(v,u),hd(sk2))**. % 7.56/7.79 1869[3:Rew:1628.0,761.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk2))** -> equal(w,x)*. % 7.56/7.79 2003[3:Con:1869.1] ssList(u) || equal(cons(v,u),hd(sk2))** -> equal(v,w)*. % 7.56/7.79 2004[3:AED:66.0,2003.2] ssList(u) || equal(cons(v,u),hd(sk2))** -> . % 7.56/7.79 2005[3:Rew:1837.1,2004.1] ssList(u) || equal(hd(sk2),hd(sk2))* -> . % 7.56/7.79 2006[3:Obv:2005.1] ssList(u) || -> . % 7.56/7.79 2007[3:UnC:2006.0,2.0] || -> . % 7.56/7.79 2134[3:Spt:2007.0,307.5,770.0] || equal(nil,sk2)** -> . % 7.56/7.79 2135[3:Spt:2007.0,307.0,307.1,307.2,307.3,307.4] ssList(u) || equal(hd(u),hd(sk2)) equal(tl(u),tl(sk2))* -> equal(u,sk2) equal(nil,u). % 7.56/7.79 2997[1:Res:200.0,602.0] || equal(nil,sk2)** -> . % 7.56/7.79 3155[1:EqR:696.1] ssList(cons(u,nil)) || -> singletonP(cons(u,nil))*. % 7.56/7.79 3156[1:SSi:3155.0,691.0,20.0,19.0,18.0,17.0,16.0,15.0,14.0,13.0,568.0,569.0,570.0,571.0,572.0,573.0,574.1] || -> singletonP(cons(u,nil))*. % 7.56/7.79 5746[4:Spt:674.0,674.2,674.3,674.4] ssList(u) || equal(hd(sk2),v) equal(cons(v,nil),u)* -> equal(sk1,u). % 7.56/7.79 5747[4:EqR:5746.2] ssList(cons(u,nil)) || equal(hd(sk2),u) -> equal(cons(u,nil),sk1)**. % 7.56/7.79 5751[4:SSi:5747.0,691.0,20.0,19.0,18.0,17.0,16.0,15.0,14.0,13.0,568.0,569.0,570.0,571.0,572.0,573.0,574.0,3156.1] || equal(hd(sk2),u) -> equal(cons(u,nil),sk1)**. % 7.56/7.79 5754[4:Rew:5751.1,634.2] || neq(nil,sk2)* equal(hd(sk2),u)* equal(sk1,sk1) -> . % 7.56/7.79 5756[4:Obv:5754.2] || neq(nil,sk2)* equal(hd(sk2),u)* -> . % 7.56/7.79 5757[4:AED:66.0,5756.1] || neq(nil,sk2)* -> . % 7.56/7.79 5762[4:Res:592.1,5757.0] || -> equal(nil,sk2)**. % 7.56/7.79 5763[4:MRR:5762.0,2134.0] || -> . % 7.56/7.79 5764[4:Spt:5763.0,674.1] || neq(nil,sk2)* -> . % 7.56/7.79 5765[4:Res:592.1,5764.0] || -> equal(nil,sk2)**. % 7.56/7.79 5766[4:MRR:5765.0,2134.0] || -> . % 7.56/7.79 5767[2:Spt:5766.0,336.1] || -> equal(nil,sk2)**. % 7.56/7.79 5964[2:Rew:5767.0,2997.0] || equal(sk2,sk2)* -> . % 7.56/7.79 5965[2:Obv:5964.0] || -> . % 7.56/7.79 6227[1:Spt:5965.0,84.0,84.2] ssList(u) || -> duplicatefreeP(u)*. % 7.56/7.79 6244[1:MRR:191.1,6227.1] ssList(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 7.56/7.79 23652[0:SpR:169.3,97.2] ssList(u) ssList(v) ssItem(w) ssList(cons(w,v)) ssList(u) || -> ssList(cons(w,app(v,u)))*. % 7.56/7.79 23708[0:Obv:23652.0] ssList(u) ssItem(v) ssList(cons(v,u)) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 7.56/7.79 23709[0:SSi:23708.2,98.2] ssList(u) ssItem(v) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 7.56/7.79 25362[1:EqR:6244.5] ssList(app(app(u,cons(v,w)),cons(v,x))) ssItem(v) ssList(u) ssList(w) ssList(x) || -> . % 10.20/10.42 25400[1:SSi:25362.0,97.2,97.2,98.2,98.2] ssItem(u) ssList(v) ssList(w) ssList(x) || -> . % 10.20/10.42 25401[1:MRR:23709.3,25400.1] ssList(u) ssItem(v) ssList(w) || -> . % 10.20/10.42 25404[1:Con:25401.2] ssList(u) ssItem(v) || -> . % 10.20/10.42 25406[1:MRR:348.1,25404.0] ssItem(u) || -> . % 10.20/10.42 25410[1:UnC:25406.0,59.0] || -> . % 10.20/10.42 % SZS output end Refutation % 10.20/10.42 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_11 co1_12 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause47 clause54 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause72 clause74 clause85 clause86 clause97 clause102 clause116 clause117 clause120 clause123 clause157 clause170 clause177 clause179 % 10.20/10.42 %------------------------------------------------------------------------------