%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV396+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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 : Wed Jul 20 21:42:38 EDT 2022 % Result : Theorem 36.16s 36.32s % Output : Refutation 36.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWV396+1 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n008.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 : Wed Jun 15 15:48:22 EDT 2022 % 0.12/0.33 % CPUTime : % 36.16/36.32 % 36.16/36.32 SPASS V 3.9 % 36.16/36.32 SPASS beiseite: Proof found. % 36.16/36.32 % SZS status Theorem % 36.16/36.32 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.16/36.32 SPASS derived 22157 clauses, backtracked 11930 clauses, performed 10 splits and kept 18837 clauses. % 36.16/36.32 SPASS allocated 120386 KBytes. % 36.16/36.32 SPASS spent 0:0:35.95 on the problem. % 36.16/36.32 0:00:00.04 for the input. % 36.16/36.32 0:00:00.04 for the FLOTTER CNF translation. % 36.16/36.32 0:00:00.31 for inferences. % 36.16/36.32 0:00:01.69 for the backtracking. % 36.16/36.32 0:0:33.80 for the reduction. % 36.16/36.32 % 36.16/36.32 % 36.16/36.32 Here is a proof with depth 8, length 124 : % 36.16/36.32 % SZS output start Refutation % 36.16/36.32 1[0:Inp] || -> strictly_less_than(skc8,skc11)*. % 36.16/36.32 2[0:Inp] || -> less_than(u,u)*. % 36.16/36.32 3[0:Inp] || -> less_than(bottom,u)*. % 36.16/36.32 9[0:Inp] || -> check_cpq(triple(u,create_slb,v))*. % 36.16/36.32 10[0:Inp] || -> equal(findmin_cpq_res(u),removemin_cpq_res(u))**. % 36.16/36.32 11[0:Inp] || -> less_than(u,v)* less_than(v,u)*. % 36.16/36.32 13[0:Inp] || ok(triple(u,v,bad))* -> . % 36.16/36.32 15[0:Inp] || -> equal(findmin_cpq_res(triple(u,create_slb,v)),bottom)**. % 36.16/36.32 16[0:Inp] || -> pair_in_list(insert_slb(skc7,pair(skc9,skc10)),skc8,skc11)*. % 36.16/36.32 20[0:Inp] || -> ok(triple(u,v,w))* equal(w,bad). % 36.16/36.32 22[0:Inp] || -> equal(remove_slb(insert_slb(u,pair(v,w)),v),u)**. % 36.16/36.32 23[0:Inp] || -> equal(lookup_slb(insert_slb(u,pair(v,w)),v),w)**. % 36.16/36.32 26[0:Inp] || less_than(u,v) -> less_than(v,u) strictly_less_than(u,v)*. % 36.16/36.32 30[0:Inp] || pair_in_list(remove_slb(insert_slb(skc7,pair(skc9,skc10)),skc8),skc8,skc11)* -> . % 36.16/36.32 31[0:Inp] || -> ok(remove_cpq(triple(skc12,insert_slb(skc7,pair(skc9,skc10)),skc13),skc8))*. % 36.16/36.32 36[0:Inp] || pair_in_list(u,v,w) -> pair_in_list(insert_slb(u,pair(x,y)),v,w)*. % 36.16/36.32 37[0:Inp] || contains_slb(insert_slb(u,pair(v,w)),x)* -> contains_slb(u,x) equal(v,x). % 36.16/36.32 38[0:Inp] || check_cpq(triple(u,insert_slb(v,pair(w,x)),y))* strictly_less_than(w,x) -> . % 36.16/36.32 39[0:Inp] || -> contains_slb(u,v) equal(remove_cpq(triple(w,u,x),v),triple(w,u,bad))**. % 36.16/36.32 40[0:Inp] || pair_in_list(insert_slb(u,pair(v,w)),x,y)* -> equal(v,x) pair_in_list(u,x,y). % 36.16/36.32 41[0:Inp] || pair_in_list(insert_slb(u,pair(v,w)),x,y)* -> equal(w,y) pair_in_list(u,x,y). % 36.16/36.32 43[0:Inp] || -> equal(triple(insert_pqp(u,v),insert_slb(w,pair(v,bottom)),x),insert_cpq(triple(u,w,x),v))**. % 36.16/36.32 44[0:Inp] || contains_slb(u,v) -> equal(w,v) equal(lookup_slb(insert_slb(u,pair(w,x)),v),lookup_slb(u,v))**. % 36.16/36.32 45[0:Inp] || strictly_less_than(u,v) -> equal(update_slb(insert_slb(w,pair(x,u)),v),insert_slb(update_slb(w,v),pair(x,v)))*. % 36.16/36.32 46[0:Inp] || less_than(u,v) -> equal(insert_slb(update_slb(w,u),pair(x,v)),update_slb(insert_slb(w,pair(x,v)),u))**. % 36.16/36.32 48[0:Inp] || check_cpq(triple(u,v,w)) less_than(x,y) -> check_cpq(triple(u,insert_slb(v,pair(y,x)),w))*. % 36.16/36.32 50[0:Inp] || contains_slb(u,v) -> equal(w,v) equal(insert_slb(remove_slb(u,v),pair(w,x)),remove_slb(insert_slb(u,pair(w,x)),v))**. % 36.16/36.32 51[0:Inp] || ok(remove_cpq(triple(u,skc7,v),w))*+ strictly_less_than(w,x) pair_in_list(skc7,w,x) -> pair_in_list(remove_slb(skc7,w),w,x)*. % 36.16/36.32 52[0:Inp] || contains_slb(u,v) strictly_less_than(v,lookup_slb(u,v)) -> equal(remove_cpq(triple(w,u,x),v),triple(remove_pqp(w,v),remove_slb(u,v),bad))*. % 36.16/36.32 53[0:Inp] || contains_slb(u,v) less_than(lookup_slb(u,v),v) -> equal(triple(remove_pqp(w,v),remove_slb(u,v),x),remove_cpq(triple(w,u,x),v))**. % 36.16/36.32 56[0:Rew:10.0,15.0] || -> equal(removemin_cpq_res(triple(u,create_slb,v)),bottom)**. % 36.16/36.32 59[0:MRR:26.0,11.0] || -> strictly_less_than(u,v)* less_than(v,u). % 36.16/36.32 61[0:Res:1.0,51.1] || ok(remove_cpq(triple(u,skc7,v),skc8))* pair_in_list(skc7,skc8,skc11) -> pair_in_list(remove_slb(skc7,skc8),skc8,skc11). % 36.16/36.32 62[0:Res:1.0,45.0] || -> equal(insert_slb(update_slb(u,skc11),pair(v,skc11)),update_slb(insert_slb(u,pair(v,skc8)),skc11))**. % 36.16/36.32 65[0:Res:1.0,38.1] || check_cpq(triple(u,insert_slb(v,pair(skc8,skc11)),w))* -> . % 36.16/36.32 67[0:Res:16.0,40.0] || -> equal(skc9,skc8) pair_in_list(skc7,skc8,skc11)*. % 36.16/36.32 68[0:Res:16.0,41.0] || -> equal(skc11,skc10) pair_in_list(skc7,skc8,skc11)*. % 36.16/36.32 74[1:Spt:68.0] || -> equal(skc11,skc10)**. % 36.16/36.32 75[1:Rew:74.0,61.1] || ok(remove_cpq(triple(u,skc7,v),skc8))* pair_in_list(skc7,skc8,skc10) -> pair_in_list(remove_slb(skc7,skc8),skc8,skc11). % 36.16/36.32 76[1:Rew:74.0,67.1] || -> equal(skc9,skc8) pair_in_list(skc7,skc8,skc10)*. % 36.16/36.32 77[1:Rew:74.0,1.0] || -> strictly_less_than(skc8,skc10)*. % 36.16/36.32 81[1:Rew:74.0,65.0] || check_cpq(triple(u,insert_slb(v,pair(skc8,skc10)),w))* -> . % 36.16/36.32 82[1:Rew:74.0,30.0] || pair_in_list(remove_slb(insert_slb(skc7,pair(skc9,skc10)),skc8),skc8,skc10)* -> . % 36.16/36.32 83[1:Rew:74.0,62.0] || -> equal(insert_slb(update_slb(u,skc10),pair(v,skc10)),update_slb(insert_slb(u,pair(v,skc8)),skc10))**. % 36.16/36.32 84[1:Rew:74.0,75.2] || ok(remove_cpq(triple(u,skc7,v),skc8))* pair_in_list(skc7,skc8,skc10) -> pair_in_list(remove_slb(skc7,skc8),skc8,skc10). % 36.16/36.32 88[2:Spt:76.0] || -> equal(skc9,skc8)**. % 36.16/36.32 89[2:Rew:88.0,31.0] || -> ok(remove_cpq(triple(skc12,insert_slb(skc7,pair(skc8,skc10)),skc13),skc8))*. % 36.16/36.32 141[2:SpR:39.1,89.0] || -> contains_slb(insert_slb(skc7,pair(skc8,skc10)),skc8) ok(triple(skc12,insert_slb(skc7,pair(skc8,skc10)),bad))*. % 36.16/36.32 152[2:MRR:141.1,13.0] || -> contains_slb(insert_slb(skc7,pair(skc8,skc10)),skc8)*. % 36.16/36.32 172[1:SpL:83.0,81.0] || check_cpq(triple(u,update_slb(insert_slb(v,pair(skc8,skc8)),skc10),w))* -> . % 36.16/36.32 421[0:SpR:50.2,36.1] || contains_slb(u,v) pair_in_list(remove_slb(u,v),w,x) -> equal(y,v) pair_in_list(remove_slb(insert_slb(u,pair(y,z)),v),w,x)*. % 36.16/36.32 580[1:SpR:46.1,83.0] || less_than(skc10,skc10) -> equal(update_slb(insert_slb(u,pair(v,skc10)),skc10),update_slb(insert_slb(u,pair(v,skc8)),skc10))**. % 36.16/36.32 613[1:MRR:580.0,2.0] || -> equal(update_slb(insert_slb(u,pair(v,skc10)),skc10),update_slb(insert_slb(u,pair(v,skc8)),skc10))**. % 36.16/36.32 623[1:SpR:83.0,613.0] || -> equal(update_slb(insert_slb(update_slb(u,skc10),pair(v,skc8)),skc10),update_slb(update_slb(insert_slb(u,pair(v,skc8)),skc10),skc10))**. % 36.16/36.32 660[0:SpR:43.0,48.2] || check_cpq(triple(insert_pqp(u,v),w,x))* less_than(bottom,v) -> check_cpq(insert_cpq(triple(u,w,x),v)). % 36.16/36.32 663[0:MRR:660.1,3.0] || check_cpq(triple(insert_pqp(u,v),w,x))* -> check_cpq(insert_cpq(triple(u,w,x),v)). % 36.16/36.32 665[0:SpL:43.0,663.0] || check_cpq(insert_cpq(triple(u,v,w),x)) -> check_cpq(insert_cpq(triple(u,insert_slb(v,pair(x,bottom)),w),x))*. % 36.16/36.32 667[0:Res:9.0,663.0] || -> check_cpq(insert_cpq(triple(u,create_slb,v),w))*. % 36.16/36.32 733[0:SpL:52.2,13.0] || contains_slb(u,v) strictly_less_than(v,lookup_slb(u,v))* ok(remove_cpq(triple(w,u,x),v))*+ -> . % 36.16/36.32 779[0:SpR:53.2,20.0] || contains_slb(u,v) less_than(lookup_slb(u,v),v) -> ok(remove_cpq(triple(w,u,x),v))* equal(x,bad). % 36.16/36.32 1003[2:Res:89.0,733.2] || contains_slb(insert_slb(skc7,pair(skc8,skc10)),skc8) strictly_less_than(skc8,lookup_slb(insert_slb(skc7,pair(skc8,skc10)),skc8))* -> . % 36.16/36.32 1004[2:Rew:23.0,1003.1] || contains_slb(insert_slb(skc7,pair(skc8,skc10)),skc8)* strictly_less_than(skc8,skc10) -> . % 36.16/36.32 1005[2:MRR:1004.0,1004.1,152.0,77.0] || -> . % 36.16/36.32 1008[2:Spt:1005.0,76.0,88.0] || equal(skc9,skc8)** -> . % 36.16/36.32 1009[2:Spt:1005.0,76.1] || -> pair_in_list(skc7,skc8,skc10)*. % 36.16/36.32 1010[2:MRR:84.1,1009.0] || ok(remove_cpq(triple(u,skc7,v),skc8))* -> pair_in_list(remove_slb(skc7,skc8),skc8,skc10). % 36.16/36.32 1013[0:SpR:39.1,31.0] || -> contains_slb(insert_slb(skc7,pair(skc9,skc10)),skc8) ok(triple(skc12,insert_slb(skc7,pair(skc9,skc10)),bad))*. % 36.16/36.32 1014[0:Res:31.0,733.2] || contains_slb(insert_slb(skc7,pair(skc9,skc10)),skc8) strictly_less_than(skc8,lookup_slb(insert_slb(skc7,pair(skc9,skc10)),skc8))* -> . % 36.16/36.32 1015[0:MRR:1013.1,13.0] || -> contains_slb(insert_slb(skc7,pair(skc9,skc10)),skc8)*. % 36.16/36.32 1016[0:MRR:1014.0,1015.0] || strictly_less_than(skc8,lookup_slb(insert_slb(skc7,pair(skc9,skc10)),skc8))* -> . % 36.16/36.32 1017[0:Res:1015.0,37.0] || -> contains_slb(skc7,skc8)* equal(skc9,skc8). % 36.16/36.32 1018[2:MRR:1017.1,1008.0] || -> contains_slb(skc7,skc8)*. % 36.16/36.32 1019[0:SpL:44.2,1016.0] || contains_slb(skc7,skc8) strictly_less_than(skc8,lookup_slb(skc7,skc8))* -> equal(skc9,skc8). % 36.16/36.32 1020[0:Res:59.0,1016.0] || -> less_than(lookup_slb(insert_slb(skc7,pair(skc9,skc10)),skc8),skc8)*l. % 36.16/36.32 1021[2:MRR:1019.0,1019.2,1018.0,1008.0] || strictly_less_than(skc8,lookup_slb(skc7,skc8))* -> . % 36.16/36.32 1022[2:Res:59.0,1021.0] || -> less_than(lookup_slb(skc7,skc8),skc8)*l. % 36.16/36.32 1041[0:SpR:44.2,1020.0] || contains_slb(skc7,skc8) -> equal(skc9,skc8) less_than(lookup_slb(skc7,skc8),skc8)*l. % 36.16/36.32 1432[1:SpL:623.0,172.0] || check_cpq(triple(u,update_slb(update_slb(insert_slb(v,pair(skc8,skc8)),skc10),skc10),w))* -> . % 36.16/36.32 1590[1:SpL:623.0,1432.0] || check_cpq(triple(u,update_slb(update_slb(update_slb(insert_slb(v,pair(skc8,skc8)),skc10),skc10),skc10),w))* -> . % 36.62/36.79 1637[1:SpL:623.0,1590.0] || check_cpq(triple(u,update_slb(update_slb(update_slb(update_slb(insert_slb(v,pair(skc8,skc8)),skc10),skc10),skc10),skc10),w))* -> . % 36.62/36.79 1902[1:SpL:623.0,1637.0] || check_cpq(triple(u,update_slb(update_slb(update_slb(update_slb(update_slb(insert_slb(v,pair(skc8,skc8)),skc10),skc10),skc10),skc10),skc10),w))* -> . % 36.62/36.79 2537[0:SpR:43.0,665.1] || check_cpq(insert_cpq(triple(insert_pqp(u,v),w,x),v))* -> check_cpq(insert_cpq(insert_cpq(triple(u,w,x),v),v)). % 36.62/36.79 2623[0:Res:667.0,2537.0] || -> check_cpq(insert_cpq(insert_cpq(triple(u,create_slb,v),w),w))*. % 36.62/36.79 2735[1:SpL:623.0,1902.0] || check_cpq(triple(u,update_slb(update_slb(update_slb(update_slb(update_slb(update_slb(insert_slb(v,pair(skc8,skc8)),skc10),skc10),skc10),skc10),skc10),skc10),w))* -> . % 36.62/36.79 8337[1:Res:421.3,82.0] || contains_slb(skc7,skc8) pair_in_list(remove_slb(skc7,skc8),skc8,skc10)* -> equal(skc9,skc8). % 36.62/36.79 8338[2:MRR:8337.0,8337.2,1018.0,1008.0] || pair_in_list(remove_slb(skc7,skc8),skc8,skc10)* -> . % 36.62/36.79 8339[2:MRR:1010.1,8338.0] || ok(remove_cpq(triple(u,skc7,v),skc8))* -> . % 36.62/36.79 8893[2:Res:779.2,8339.0] || contains_slb(skc7,skc8) less_than(lookup_slb(skc7,skc8),skc8)*l -> equal(u,bad)*. % 36.62/36.79 14442[2:MRR:8893.0,8893.1,1018.0,1022.0] || -> equal(u,bad)*. % 36.62/36.79 14461[2:Rew:14442.0,56.0] || -> equal(bad,bottom)**. % 36.62/36.79 14548[2:Rew:14442.0,22.0] || -> equal(bad,u)*. % 36.62/36.79 14570[2:Rew:14442.0,2623.0] || -> check_cpq(bad)*. % 36.62/36.79 14584[2:Rew:14461.0,14570.0] || -> check_cpq(bottom)*. % 36.62/36.79 14593[2:Rew:14461.0,14548.0] || -> equal(bottom,u)*. % 36.62/36.79 14708[2:Rew:14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0,14593.0,2735.0] || check_cpq(bottom)* -> . % 36.62/36.79 14709[2:MRR:14708.0,14584.0] || -> . % 36.62/36.79 16572[1:Spt:14709.0,68.0,74.0] || equal(skc11,skc10)** -> . % 36.62/36.79 16573[1:Spt:14709.0,68.1] || -> pair_in_list(skc7,skc8,skc11)*. % 36.62/36.79 16575[0:MRR:1041.0,1017.0] || -> equal(skc9,skc8) less_than(lookup_slb(skc7,skc8),skc8)*l. % 36.62/36.79 16582[1:MRR:61.1,16573.0] || ok(remove_cpq(triple(u,skc7,v),skc8))* -> pair_in_list(remove_slb(skc7,skc8),skc8,skc11). % 36.62/36.79 16660[2:Spt:1017.0] || -> contains_slb(skc7,skc8)*. % 36.62/36.79 16721[3:Spt:16575.0] || -> equal(skc9,skc8)**. % 36.62/36.79 16726[3:Rew:16721.0,30.0] || pair_in_list(remove_slb(insert_slb(skc7,pair(skc8,skc10)),skc8),skc8,skc11)* -> . % 36.62/36.79 16757[3:Rew:22.0,16726.0] || pair_in_list(skc7,skc8,skc11)* -> . % 36.62/36.79 16758[3:MRR:16757.0,16573.0] || -> . % 36.62/36.79 16764[3:Spt:16758.0,16575.0,16721.0] || equal(skc9,skc8)** -> . % 36.62/36.79 16765[3:Spt:16758.0,16575.1] || -> less_than(lookup_slb(skc7,skc8),skc8)*l. % 36.62/36.79 26303[0:Res:421.3,30.0] || contains_slb(skc7,skc8) pair_in_list(remove_slb(skc7,skc8),skc8,skc11)* -> equal(skc9,skc8). % 36.62/36.79 26304[3:MRR:26303.0,26303.2,16660.0,16764.0] || pair_in_list(remove_slb(skc7,skc8),skc8,skc11)* -> . % 36.62/36.79 26305[3:MRR:16582.1,26304.0] || ok(remove_cpq(triple(u,skc7,v),skc8))* -> . % 36.62/36.79 26902[3:Res:779.2,26305.0] || contains_slb(skc7,skc8) less_than(lookup_slb(skc7,skc8),skc8)*l -> equal(u,bad)*. % 36.62/36.79 32359[3:MRR:26902.0,26902.1,16660.0,16765.0] || -> equal(u,bad)*. % 36.62/36.79 32378[3:Rew:32359.0,56.0] || -> equal(bad,bottom)**. % 36.62/36.79 32441[3:Rew:32359.0,30.0] || pair_in_list(remove_slb(insert_slb(skc7,pair(bad,skc10)),skc8),skc8,skc11)* -> . % 36.62/36.79 32445[3:Rew:32359.0,16573.0] || -> pair_in_list(skc7,bad,skc11)*. % 36.62/36.79 32468[3:Rew:32359.0,22.0] || -> equal(bad,u)*. % 36.62/36.79 32512[3:Rew:32378.0,32468.0] || -> equal(bottom,u)*. % 36.62/36.79 32528[3:Rew:32512.0,32445.0,32512.0,32445.0,32512.0,32445.0] || -> pair_in_list(bottom,bottom,bottom)*. % 36.62/36.79 32584[3:Rew:32512.0,32441.0,32512.0,32441.0,32512.0,32441.0,32512.0,32441.0,32512.0,32441.0,32512.0,32441.0,32512.0,32441.0,32512.0,32441.0] || pair_in_list(bottom,bottom,bottom)* -> . % 36.62/36.79 32585[3:MRR:32584.0,32528.0] || -> . % 36.62/36.79 34458[2:Spt:32585.0,1017.0,16660.0] || contains_slb(skc7,skc8)* -> . % 36.62/36.79 34459[2:Spt:32585.0,1017.1] || -> equal(skc9,skc8)**. % 36.62/36.79 34477[2:Rew:22.0,30.0,34459.0,30.0] || pair_in_list(skc7,skc8,skc11)* -> . % 36.62/36.79 34478[2:MRR:34477.0,16573.0] || -> . % 36.62/36.79 % SZS output end Refutation % 36.62/36.79 Formulae used in the proof : l32_co reflexivity bottom_smallest ax36 ax53 totality ax40 ax50 ax41 ax24 ax26 stricly_smaller_definition ax23 ax21 ax38 ax43 ax42 ax27 ax29 ax30 ax37 ax25 ax45 ax44 % 36.62/36.79 %------------------------------------------------------------------------------