%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV029+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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:41:02 EDT 2022 % Result : Theorem 25.31s 25.53s % Output : Refutation 25.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV029+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.03/0.12 % Command : run_spass %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 16 04:57:56 EDT 2022 % 0.13/0.34 % CPUTime : % 25.31/25.53 % 25.31/25.53 SPASS V 3.9 % 25.31/25.53 SPASS beiseite: Proof found. % 25.31/25.53 % SZS status Theorem % 25.31/25.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.31/25.53 SPASS derived 19702 clauses, backtracked 4110 clauses, performed 17 splits and kept 13110 clauses. % 25.31/25.53 SPASS allocated 102895 KBytes. % 25.31/25.53 SPASS spent 0:0:25.16 on the problem. % 25.31/25.53 0:00:00.04 for the input. % 25.31/25.53 0:00:00.08 for the FLOTTER CNF translation. % 25.31/25.53 0:00:00.16 for inferences. % 25.31/25.53 0:00:00.42 for the backtracking. % 25.31/25.53 0:0:24.27 for the reduction. % 25.31/25.53 % 25.31/25.53 % 25.31/25.53 Here is a proof with depth 2, length 132 : % 25.31/25.53 % SZS output start Refutation % 25.31/25.53 1[0:Inp] || -> SkC0*. % 25.31/25.53 2[0:Inp] || -> SkC2*. % 25.31/25.53 3[0:Inp] || -> SkC3*. % 25.31/25.53 7[0:Inp] || -> leq(n0,skc7)*r. % 25.31/25.53 11[0:Inp] || -> equal(init,s_best7_init)**. % 25.31/25.53 12[0:Inp] || -> equal(init,s_sworst7_init)**. % 25.31/25.53 13[0:Inp] || -> equal(init,s_worst7_init)**. % 25.31/25.53 14[0:Inp] || -> leq(n0,s_best7)*r. % 25.31/25.53 15[0:Inp] || -> leq(n0,s_sworst7)*r. % 25.31/25.53 16[0:Inp] || -> leq(n0,s_worst7)*r. % 25.31/25.53 18[0:Inp] || -> leq(s_best7,n3)*r. % 25.31/25.53 19[0:Inp] || -> leq(s_sworst7,n3)*r. % 25.31/25.53 20[0:Inp] || -> leq(s_worst7,n3)*r. % 25.31/25.53 21[0:Inp] || -> leq(pv1376,n3)*r. % 25.31/25.53 44[0:Inp] || -> SkC1* leq(skc7,n3). % 25.31/25.53 76[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1400_init)**. % 25.31/25.53 77[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1401_init)**. % 25.31/25.53 78[0:Inp] || gt(loopcounter,n1) -> equal(init,pvar1402_init)**. % 25.31/25.53 104[0:Inp] || -> equal(a_select2(tptp_update2(u,v,w),v),w)**. % 25.31/25.53 113[0:Inp] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),skc7),init)** -> SkC1. % 25.31/25.53 114[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 25.31/25.53 121[0:Inp] || leq(n0,u) leq(u,n3) -> equal(a_select2(s_values7_init,u),init)**. % 25.31/25.53 124[0:Inp] || -> equal(u,v) equal(a_select2(tptp_update2(w,u,x),v),a_select2(w,v))**. % 25.31/25.53 160[0:Inp] || equal(init,init) equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 25.31/25.53 164[0:Inp] || equal(init,pvar1400_init) equal(init,pvar1401_init) equal(init,pvar1402_init) equal(init,init) equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> . % 25.31/25.53 165[0:Rew:13.0,12.0] || -> equal(s_worst7_init,s_sworst7_init)**. % 25.31/25.53 166[0:Rew:165.0,13.0] || -> equal(init,s_sworst7_init)**. % 25.31/25.53 167[0:Rew:11.0,166.0] || -> equal(s_sworst7_init,s_best7_init)**. % 25.31/25.53 168[0:Rew:167.0,165.0] || -> equal(s_worst7_init,s_best7_init)**. % 25.31/25.53 182[0:Rew:11.0,113.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),skc7),s_best7_init)** -> SkC1. % 25.31/25.53 183[0:Rew:11.0,78.1] || gt(loopcounter,n1) -> equal(pvar1402_init,s_best7_init)**. % 25.31/25.53 184[0:Rew:11.0,77.1] || gt(loopcounter,n1) -> equal(pvar1401_init,s_best7_init)**. % 25.31/25.53 185[0:Rew:11.0,76.1] || gt(loopcounter,n1) -> equal(pvar1400_init,s_best7_init)**. % 25.31/25.53 186[0:Rew:11.0,121.2] || leq(u,n3) leq(n0,u) -> equal(a_select2(s_values7_init,u),s_best7_init)**. % 25.31/25.53 193[0:Obv:160.0] || equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 25.31/25.53 194[0:Rew:11.0,193.2,168.0,193.2,11.0,193.1,167.0,193.1,11.0,193.0] || equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 25.31/25.53 195[0:Obv:194.2] || leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> gt(loopcounter,n1). % 25.31/25.53 196[0:MRR:195.0,195.1,195.2,195.3,195.4,195.5,195.6,195.8,195.9,14.0,15.0,16.0,18.0,19.0,20.0,1.0,2.0,3.0] || SkC1* -> gt(loopcounter,n1). % 25.31/25.53 197[0:Obv:164.3] || equal(init,pvar1400_init) equal(init,pvar1401_init) equal(init,pvar1402_init) equal(init,s_best7_init) equal(init,s_sworst7_init) equal(init,s_worst7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> . % 25.31/25.53 198[0:Rew:11.0,197.5,168.0,197.5,11.0,197.4,167.0,197.4,11.0,197.3,11.0,197.2,11.0,197.1,11.0,197.0] || equal(pvar1400_init,s_best7_init) equal(pvar1401_init,s_best7_init) equal(pvar1402_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> . % 25.31/25.53 199[0:Obv:198.5] || equal(pvar1400_init,s_best7_init) equal(pvar1401_init,s_best7_init) equal(pvar1402_init,s_best7_init) leq(n0,s_best7) leq(n0,s_sworst7) leq(n0,s_worst7) leq(s_best7,n3) leq(s_sworst7,n3) leq(s_worst7,n3) SkC0* SkC1 SkC2 SkC3 -> . % 25.31/25.53 200[0:MRR:199.3,199.4,199.5,199.6,199.7,199.8,199.9,199.11,199.12,14.0,15.0,16.0,18.0,19.0,20.0,1.0,2.0,3.0] || SkC1* equal(pvar1402_init,s_best7_init) equal(pvar1401_init,s_best7_init) equal(pvar1400_init,s_best7_init) -> . % 25.31/25.53 220[0:Res:21.0,114.0] || -> gt(n3,pv1376)*l equal(n3,pv1376). % 25.31/25.53 281[0:Res:20.0,114.0] || -> gt(n3,s_worst7)*l equal(n3,s_worst7). % 25.31/25.53 342[0:Res:19.0,114.0] || -> gt(n3,s_sworst7)*l equal(n3,s_sworst7). % 25.31/25.53 489[1:Spt:342.1] || -> equal(n3,s_sworst7)**. % 25.31/25.53 557[1:Rew:489.0,186.0] || leq(u,s_sworst7) leq(n0,u) -> equal(a_select2(s_values7_init,u),s_best7_init)**. % 25.31/25.53 610[1:Rew:489.0,44.1] || -> SkC1* leq(skc7,s_sworst7). % 25.31/25.53 715[2:Spt:196.0] || SkC1* -> . % 25.31/25.53 716[2:MRR:182.1,715.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),skc7),s_best7_init)** -> . % 25.31/25.53 717[2:MRR:610.0,715.0] || -> leq(skc7,s_sworst7)*l. % 25.31/25.53 5895[2:SpL:124.1,716.0] || equal(a_select2(s_values7_init,skc7),s_best7_init)** -> equal(skc7,pv1376). % 25.31/25.53 7884[2:SpL:557.2,5895.0] || leq(skc7,s_sworst7)*l leq(n0,skc7) equal(s_best7_init,s_best7_init) -> equal(skc7,pv1376). % 25.31/25.53 7885[2:Obv:7884.2] || leq(skc7,s_sworst7)*l leq(n0,skc7) -> equal(skc7,pv1376). % 25.31/25.53 7886[2:MRR:7885.0,7885.1,717.0,7.0] || -> equal(skc7,pv1376)**. % 25.31/25.53 7895[2:Rew:7886.0,716.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),pv1376),s_best7_init)** -> . % 25.31/25.53 7974[2:Rew:104.0,7895.0] || equal(s_best7_init,s_best7_init)* -> . % 25.31/25.53 7975[2:Obv:7974.0] || -> . % 25.31/25.53 8006[2:Spt:7975.0,196.0,715.0] || -> SkC1*. % 25.31/25.53 8007[2:Spt:7975.0,196.1] || -> gt(loopcounter,n1)*l. % 25.31/25.53 8014[2:MRR:184.0,8007.0] || -> equal(pvar1401_init,s_best7_init)**. % 25.31/25.53 8015[2:MRR:185.0,8007.0] || -> equal(pvar1400_init,s_best7_init)**. % 25.31/25.53 8016[2:MRR:183.0,8007.0] || -> equal(pvar1402_init,s_best7_init)**. % 25.31/25.53 8023[2:Rew:8015.0,200.3,8014.0,200.2,8016.0,200.1] || SkC1* equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) -> . % 25.31/25.53 8024[2:Obv:8023.3] || SkC1* -> . % 25.31/25.53 8025[2:MRR:8024.0,8006.0] || -> . % 25.31/25.53 8037[1:Spt:8025.0,342.1,489.0] || equal(n3,s_sworst7)** -> . % 25.31/25.53 8038[1:Spt:8025.0,342.0] || -> gt(n3,s_sworst7)*l. % 25.31/25.53 8107[2:Spt:281.1] || -> equal(n3,s_worst7)**. % 25.31/25.53 8131[2:Rew:8107.0,44.1] || -> SkC1* leq(skc7,s_worst7). % 25.31/25.53 8207[2:Rew:8107.0,186.0] || leq(u,s_worst7) leq(n0,u) -> equal(a_select2(s_values7_init,u),s_best7_init)**. % 25.31/25.53 8381[3:Spt:196.0] || SkC1* -> . % 25.31/25.53 8382[3:MRR:182.1,8381.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),skc7),s_best7_init)** -> . % 25.31/25.53 8383[3:MRR:8131.0,8381.0] || -> leq(skc7,s_worst7)*l. % 25.31/25.53 9170[3:SpL:124.1,8382.0] || equal(a_select2(s_values7_init,skc7),s_best7_init)** -> equal(skc7,pv1376). % 25.31/25.53 13693[3:SpL:8207.2,9170.0] || leq(skc7,s_worst7)*l leq(n0,skc7) equal(s_best7_init,s_best7_init) -> equal(skc7,pv1376). % 25.31/25.53 13694[3:Obv:13693.2] || leq(skc7,s_worst7)*l leq(n0,skc7) -> equal(skc7,pv1376). % 25.31/25.53 13695[3:MRR:13694.0,13694.1,8383.0,7.0] || -> equal(skc7,pv1376)**. % 25.31/25.53 13698[3:Rew:13695.0,8382.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),pv1376),s_best7_init)** -> . % 25.31/25.53 13827[3:Rew:104.0,13698.0] || equal(s_best7_init,s_best7_init)* -> . % 25.31/25.53 13828[3:Obv:13827.0] || -> . % 25.31/25.53 13867[3:Spt:13828.0,196.0,8381.0] || -> SkC1*. % 25.31/25.53 13868[3:Spt:13828.0,196.1] || -> gt(loopcounter,n1)*l. % 25.31/25.53 13871[3:MRR:185.0,13868.0] || -> equal(pvar1400_init,s_best7_init)**. % 25.31/25.53 13872[3:MRR:183.0,13868.0] || -> equal(pvar1402_init,s_best7_init)**. % 25.31/25.53 13873[3:MRR:184.0,13868.0] || -> equal(pvar1401_init,s_best7_init)**. % 25.31/25.53 13876[3:Rew:13871.0,200.3,13873.0,200.2,13872.0,200.1] || SkC1* equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) -> . % 25.63/25.82 13877[3:Obv:13876.3] || SkC1* -> . % 25.63/25.82 13878[3:MRR:13877.0,13867.0] || -> . % 25.63/25.82 13886[2:Spt:13878.0,281.1,8107.0] || equal(n3,s_worst7)** -> . % 25.63/25.82 13887[2:Spt:13878.0,281.0] || -> gt(n3,s_worst7)*l. % 25.63/25.82 13933[3:Spt:220.1] || -> equal(n3,pv1376)**. % 25.63/25.82 13969[3:Rew:13933.0,44.1] || -> SkC1* leq(skc7,pv1376). % 25.63/25.82 14037[3:Rew:13933.0,186.0] || leq(u,pv1376) leq(n0,u) -> equal(a_select2(s_values7_init,u),s_best7_init)**. % 25.63/25.82 14286[4:Spt:196.0] || SkC1* -> . % 25.63/25.82 14287[4:MRR:182.1,14286.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),skc7),s_best7_init)** -> . % 25.63/25.82 14288[4:MRR:13969.0,14286.0] || -> leq(skc7,pv1376)*l. % 25.63/25.82 15240[4:SpL:124.1,14287.0] || equal(a_select2(s_values7_init,skc7),s_best7_init)** -> equal(skc7,pv1376). % 25.63/25.82 19951[4:SpL:14037.2,15240.0] || leq(skc7,pv1376)*l leq(n0,skc7) equal(s_best7_init,s_best7_init) -> equal(skc7,pv1376). % 25.63/25.82 19952[4:Obv:19951.2] || leq(skc7,pv1376)*l leq(n0,skc7) -> equal(skc7,pv1376). % 25.63/25.82 19953[4:MRR:19952.0,19952.1,14288.0,7.0] || -> equal(skc7,pv1376)**. % 25.63/25.82 19956[4:Rew:19953.0,14287.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),pv1376),s_best7_init)** -> . % 25.63/25.82 20127[4:Rew:104.0,19956.0] || equal(s_best7_init,s_best7_init)* -> . % 25.63/25.82 20128[4:Obv:20127.0] || -> . % 25.63/25.82 20240[4:Spt:20128.0,196.0,14286.0] || -> SkC1*. % 25.63/25.82 20241[4:Spt:20128.0,196.1] || -> gt(loopcounter,n1)*l. % 25.63/25.82 20246[4:MRR:183.0,20241.0] || -> equal(pvar1402_init,s_best7_init)**. % 25.63/25.82 20247[4:MRR:184.0,20241.0] || -> equal(pvar1401_init,s_best7_init)**. % 25.63/25.82 20248[4:MRR:185.0,20241.0] || -> equal(pvar1400_init,s_best7_init)**. % 25.63/25.82 20253[4:Rew:20248.0,200.3,20247.0,200.2,20246.0,200.1] || SkC1* equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) -> . % 25.63/25.82 20254[4:Obv:20253.3] || SkC1* -> . % 25.63/25.82 20255[4:MRR:20254.0,20240.0] || -> . % 25.63/25.82 20261[3:Spt:20255.0,220.1,13933.0] || equal(n3,pv1376)** -> . % 25.63/25.82 20262[3:Spt:20255.0,220.0] || -> gt(n3,pv1376)*l. % 25.63/25.82 20295[4:Spt:196.0] || SkC1* -> . % 25.63/25.82 20296[4:MRR:44.0,20295.0] || -> leq(skc7,n3)*l. % 25.63/25.82 20297[4:MRR:182.1,20295.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),skc7),s_best7_init)** -> . % 25.63/25.82 21622[4:SpL:124.1,20297.0] || equal(a_select2(s_values7_init,skc7),s_best7_init)** -> equal(skc7,pv1376). % 25.63/25.82 25936[4:SpL:186.2,21622.0] || leq(skc7,n3)*l leq(n0,skc7) equal(s_best7_init,s_best7_init) -> equal(skc7,pv1376). % 25.63/25.82 25937[4:Obv:25936.2] || leq(skc7,n3)*l leq(n0,skc7) -> equal(skc7,pv1376). % 25.63/25.82 25938[4:MRR:25937.0,25937.1,20296.0,7.0] || -> equal(skc7,pv1376)**. % 25.63/25.82 25941[4:Rew:25938.0,20297.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),pv1376),s_best7_init)** -> . % 25.63/25.82 26130[4:Rew:104.0,25941.0] || equal(s_best7_init,s_best7_init)* -> . % 25.63/25.82 26131[4:Obv:26130.0] || -> . % 25.63/25.82 26193[4:Spt:26131.0,196.0,20295.0] || -> SkC1*. % 25.63/25.82 26194[4:Spt:26131.0,196.1] || -> gt(loopcounter,n1)*l. % 25.63/25.82 26201[4:MRR:184.0,26194.0] || -> equal(pvar1401_init,s_best7_init)**. % 25.63/25.82 26202[4:MRR:185.0,26194.0] || -> equal(pvar1400_init,s_best7_init)**. % 25.63/25.82 26203[4:MRR:183.0,26194.0] || -> equal(pvar1402_init,s_best7_init)**. % 25.63/25.82 26210[4:Rew:26202.0,200.3,26201.0,200.2,26203.0,200.1] || SkC1* equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) equal(s_best7_init,s_best7_init) -> . % 25.63/25.82 26211[4:Obv:26210.3] || SkC1* -> . % 25.63/25.82 26212[4:MRR:26211.0,26193.0] || -> . % 25.63/25.82 % SZS output end Refutation % 25.63/25.82 Formulae used in the proof : gauss_init_0029 reflexivity_leq leq_succ_succ sel2_update_1 leq_gt2 sel2_update_2 % 25.63/25.82 %------------------------------------------------------------------------------