%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV033+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:03 EDT 2022 % Result : Theorem 29.69s 29.94s % Output : Refutation 30.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV033+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n005.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jun 15 14:43:24 EDT 2022 % 0.13/0.33 % CPUTime : % 29.69/29.94 % 29.69/29.94 SPASS V 3.9 % 29.69/29.94 SPASS beiseite: Proof found. % 29.69/29.94 % SZS status Theorem % 29.69/29.94 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 29.69/29.94 SPASS derived 14926 clauses, backtracked 3407 clauses, performed 9 splits and kept 9751 clauses. % 29.69/29.94 SPASS allocated 101143 KBytes. % 29.69/29.94 SPASS spent 0:0:29.59 on the problem. % 29.69/29.94 0:00:00.04 for the input. % 29.69/29.94 0:00:00.08 for the FLOTTER CNF translation. % 29.69/29.94 0:00:00.14 for inferences. % 29.69/29.94 0:00:00.43 for the backtracking. % 29.69/29.94 0:0:28.75 for the reduction. % 29.69/29.94 % 29.69/29.94 % 29.69/29.94 Here is a proof with depth 3, length 150 : % 29.69/29.94 % SZS output start Refutation % 29.69/29.94 1[0:Inp] || -> SkC0*. % 29.69/29.94 5[0:Inp] || -> leq(n0,skc3)*r. % 29.69/29.94 7[0:Inp] || -> leq(n0,pv1376)*r. % 29.69/29.94 8[0:Inp] || -> leq(pv1376,n3)*r. % 29.69/29.94 18[0:Inp] || -> gt(n1,n0)*l. % 29.69/29.94 19[0:Inp] || -> gt(n2,n0)*l. % 29.69/29.94 23[0:Inp] || -> gt(n2,n1)*r. % 29.69/29.94 24[0:Inp] || -> gt(n3,n1)*r. % 29.69/29.94 30[0:Inp] || -> leq(u,u)*. % 29.69/29.94 31[0:Inp] || -> equal(succ(n0),n1)**. % 29.69/29.94 32[0:Inp] || gt(u,u)* -> . % 29.69/29.94 36[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 29.69/29.94 53[0:Inp] || -> equal(pred(succ(u)),u)**. % 29.69/29.94 55[0:Inp] || -> equal(succ(succ(succ(n0))),n3)**. % 29.69/29.94 59[0:Inp] || -> equal(plus(n1,u),succ(u))**. % 29.69/29.94 60[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 29.69/29.94 62[0:Inp] || -> equal(succ(succ(succ(succ(n0)))),n4)**. % 29.69/29.94 67[0:Inp] || gt(u,v)* -> leq(v,u). % 29.69/29.94 74[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 29.69/29.94 75[0:Inp] || leq(u,v)*+ -> leq(u,succ(v))*. % 29.69/29.94 87[0:Inp] || -> equal(a_select2(tptp_update2(u,v,w),v),w)**. % 29.69/29.94 96[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 29.69/29.94 100[0:Inp] || leq(u,n0)*+ leq(n0,u)* -> equal(u,n0). % 29.69/29.94 101[0:Inp] || gt(u,v)* gt(v,w)* -> gt(u,w)*. % 29.69/29.94 102[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 29.69/29.94 103[0:Inp] || equal(init,init) SkC0 -> leq(skc3,minus(plus(n1,pv1376),n1))*r. % 29.69/29.94 106[0:Inp] || -> equal(u,v) equal(a_select2(tptp_update2(w,u,x),v),a_select2(w,v))**. % 29.69/29.94 107[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 29.69/29.94 108[0:Inp] || leq(n0,u) leq(u,minus(pv1376,n1)) -> equal(a_select2(s_values7_init,u),init)**. % 29.69/29.94 109[0:Inp] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),skc3),init)** equal(init,init) SkC0 -> . % 29.69/29.94 111[0:Inp] || leq(u,n2)* leq(n0,u) -> equal(u,n2) equal(u,n1)* equal(u,n0). % 29.69/29.94 113[0:Inp] || leq(u,n3)* leq(n0,u) -> equal(u,n3) equal(u,n2) equal(u,n1)* equal(u,n0). % 29.69/29.94 145[0:Rew:31.0,36.0] || -> equal(succ(n1),n2)**. % 29.69/29.94 148[0:Rew:145.0,55.0,31.0,55.0] || -> equal(succ(n2),n3)**. % 29.69/29.94 150[0:Rew:148.0,62.0,145.0,62.0,31.0,62.0] || -> equal(succ(n3),n4)**. % 29.69/29.94 158[0:Obv:109.1] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),skc3),init)** SkC0 -> . % 29.69/29.94 159[0:MRR:158.1,1.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),skc3),init)** -> . % 29.69/29.94 160[0:Obv:103.0] || SkC0 -> leq(skc3,minus(plus(n1,pv1376),n1))*r. % 29.69/29.94 161[0:Rew:53.0,160.1,59.0,160.1,60.0,160.1] || SkC0* -> leq(skc3,pv1376). % 29.69/29.94 162[0:MRR:161.0,1.0] || -> leq(skc3,pv1376)*l. % 29.69/29.94 163[0:Rew:60.0,108.1] || leq(u,pred(pv1376)) leq(n0,u) -> equal(a_select2(s_values7_init,u),init)**. % 29.69/29.94 182[0:Res:8.0,96.0] || -> gt(n3,pv1376)*l equal(n3,pv1376). % 29.69/29.94 242[0:Res:7.0,113.0] || leq(pv1376,n3) -> equal(pv1376,n0) equal(n1,pv1376)** equal(n2,pv1376) equal(n3,pv1376). % 29.69/29.94 245[0:Res:7.0,107.0] || leq(pv1376,n1)*r -> equal(n1,pv1376) equal(pv1376,n0). % 29.69/29.94 345[0:MRR:242.0,8.0] || -> equal(n3,pv1376) equal(n2,pv1376) equal(n1,pv1376)** equal(pv1376,n0). % 29.69/29.95 405[1:Spt:245.2] || -> equal(pv1376,n0)**. % 29.69/29.95 497[1:Rew:405.0,162.0] || -> leq(skc3,n0)*l. % 29.69/29.95 498[1:Rew:405.0,159.0] || equal(a_select2(tptp_update2(s_values7_init,n0,init),skc3),init)** -> . % 29.69/29.95 602[0:SpR:31.0,53.0] || -> equal(pred(n1),n0)**. % 29.69/29.95 603[0:SpR:145.0,53.0] || -> equal(pred(n2),n1)**. % 29.69/29.95 604[0:SpR:148.0,53.0] || -> equal(pred(n3),n2)**. % 29.69/29.95 1073[0:NCh:101.2,101.1,32.0,24.0] || equal(n1,n3)** -> . % 29.69/29.95 3124[0:Res:23.0,67.0] || -> leq(n1,n2)*l. % 29.69/29.95 3128[0:Res:19.0,67.0] || -> leq(n0,n2)*r. % 29.69/29.95 3129[0:Res:18.0,67.0] || -> leq(n0,n1)*r. % 29.69/29.95 5150[1:Res:497.0,100.0] || leq(n0,skc3)*r -> equal(skc3,n0). % 29.69/29.95 5234[1:MRR:5150.0,5.0] || -> equal(skc3,n0)**. % 29.69/29.95 5237[1:Rew:5234.0,498.0] || equal(a_select2(tptp_update2(s_values7_init,n0,init),n0),init)** -> . % 29.69/29.95 5367[1:Rew:87.0,5237.0] || equal(init,init)* -> . % 29.69/29.95 5368[1:Obv:5367.0] || -> . % 29.69/29.95 5441[1:Spt:5368.0,245.2,405.0] || equal(pv1376,n0)** -> . % 29.69/29.95 5442[1:Spt:5368.0,245.0,245.1] || leq(pv1376,n1)*r -> equal(n1,pv1376). % 29.69/29.95 5444[1:MRR:345.3,5441.0] || -> equal(n3,pv1376) equal(n2,pv1376) equal(n1,pv1376)**. % 29.69/29.95 5451[2:Spt:182.1] || -> equal(n3,pv1376)**. % 29.69/29.95 5453[2:Rew:5451.0,150.0] || -> equal(succ(pv1376),n4)**. % 29.69/29.95 5454[2:Rew:5451.0,604.0] || -> equal(pred(pv1376),n2)**. % 29.69/29.95 5508[2:Rew:5451.0,1073.0] || equal(n1,pv1376)** -> . % 29.69/29.95 5621[2:Rew:5451.0,113.0] || leq(u,pv1376)* leq(n0,u) -> equal(u,n3) equal(u,n2) equal(u,n1)* equal(u,n0). % 29.69/29.95 5830[2:Rew:5454.0,163.0] || leq(u,n2) leq(n0,u) -> equal(a_select2(s_values7_init,u),init)**. % 29.69/29.95 5846[2:Rew:5451.0,5621.2] || leq(u,pv1376)*+ leq(n0,u) -> equal(u,pv1376) equal(u,n2) equal(u,n1)* equal(u,n0). % 29.69/29.95 5996[0:Res:162.0,75.0] || -> leq(skc3,succ(pv1376))*r. % 29.69/29.95 6006[2:Rew:5453.0,5996.0] || -> leq(skc3,n4)*l. % 29.69/29.95 6439[0:SpL:106.1,159.0] || equal(a_select2(s_values7_init,skc3),init)** -> equal(skc3,pv1376). % 29.69/29.95 6915[0:NCh:102.2,102.0,107.0,162.0] || equal(n1,pv1376) leq(n0,skc3)*r -> equal(skc3,n1) equal(skc3,n0). % 29.69/29.95 6917[2:NCh:102.2,102.0,107.0,6006.0] || equal(n4,n1) leq(n0,skc3)*r -> equal(skc3,n1) equal(skc3,n0). % 29.69/29.95 6923[2:MRR:6917.1,5.0] || equal(n4,n1) -> equal(skc3,n1)** equal(skc3,n0). % 29.69/29.95 7240[2:Res:162.0,5846.0] || leq(n0,skc3)*r -> equal(skc3,pv1376) equal(skc3,n2) equal(skc3,n1) equal(skc3,n0). % 29.69/29.95 7303[2:MRR:7240.0,5.0] || -> equal(skc3,pv1376) equal(skc3,n2) equal(skc3,n1)** equal(skc3,n0). % 29.69/29.95 7925[2:SpL:5830.2,6439.0] || leq(skc3,n2) leq(n0,skc3) equal(init,init)* -> equal(skc3,pv1376). % 29.69/29.95 7926[2:Obv:7925.2] || leq(skc3,n2)*l leq(n0,skc3) -> equal(skc3,pv1376). % 29.69/29.95 7927[2:MRR:7926.1,5.0] || leq(skc3,n2)*l -> equal(skc3,pv1376). % 29.69/29.95 11107[3:Spt:6923.1] || -> equal(skc3,n1)**. % 29.69/29.95 11238[3:Rew:11107.0,7927.1] || leq(skc3,n2)*l -> equal(n1,pv1376). % 29.69/29.95 11387[3:Rew:11107.0,11238.0] || leq(n1,n2)*l -> equal(n1,pv1376). % 29.69/29.95 11388[3:MRR:11387.0,11387.1,3124.0,5508.0] || -> . % 29.69/29.95 11591[3:Spt:11388.0,6923.1,11107.0] || equal(skc3,n1)** -> . % 29.69/29.95 11592[3:Spt:11388.0,6923.0,6923.2] || equal(n4,n1) -> equal(skc3,n0)**. % 29.69/29.95 11593[3:MRR:7303.2,11591.0] || -> equal(skc3,pv1376) equal(skc3,n2)** equal(skc3,n0). % 29.69/29.95 11800[0:NCh:102.2,102.0,162.0,111.0] || leq(pv1376,n2) leq(n0,skc3)*r -> equal(skc3,n2) equal(skc3,n1) equal(skc3,n0). % 29.69/29.95 11964[4:Spt:11593.0] || -> equal(skc3,pv1376)**. % 29.69/29.95 11978[4:Rew:11964.0,159.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),pv1376),init)** -> . % 29.69/29.95 12239[4:Rew:87.0,11978.0] || equal(init,init)* -> . % 29.69/29.95 12240[4:Obv:12239.0] || -> . % 29.69/29.95 12457[4:Spt:12240.0,11593.0,11964.0] || equal(skc3,pv1376)** -> . % 29.69/29.95 12458[4:Spt:12240.0,11593.1,11593.2] || -> equal(skc3,n2)** equal(skc3,n0). % 29.69/29.95 12462[4:MRR:7927.1,12457.0] || leq(skc3,n2)*l -> . % 29.69/29.95 12463[5:Spt:12458.0] || -> equal(skc3,n2)**. % 29.69/29.95 12562[5:Rew:12463.0,12462.0] || leq(n2,n2)* -> . % 29.69/29.95 12741[5:MRR:12562.0,30.0] || -> . % 29.69/29.95 12954[5:Spt:12741.0,12458.0,12463.0] || equal(skc3,n2)** -> . % 29.69/29.95 12955[5:Spt:12741.0,12458.1] || -> equal(skc3,n0)**. % 29.69/29.95 12969[5:Rew:12955.0,12462.0] || leq(n0,n2)*r -> . % 29.69/29.95 12970[5:MRR:12969.0,3128.0] || -> . % 29.69/29.95 13289[2:Spt:12970.0,182.1,5451.0] || equal(n3,pv1376)** -> . % 29.69/29.95 13290[2:Spt:12970.0,182.0] || -> gt(n3,pv1376)*l. % 29.69/29.95 13291[2:MRR:5444.0,13289.0] || -> equal(n2,pv1376) equal(n1,pv1376)**. % 29.69/29.95 13309[0:MRR:6915.1,5.0] || equal(n1,pv1376) -> equal(skc3,n1)** equal(skc3,n0). % 29.69/29.95 13321[0:MRR:11800.1,5.0] || leq(pv1376,n2) -> equal(skc3,n2) equal(skc3,n1)** equal(skc3,n0). % 29.69/29.95 13323[2:Res:13290.0,74.0] || -> leq(pv1376,pred(n3))*r. % 29.69/29.95 13331[2:Rew:604.0,13323.0] || -> leq(pv1376,n2)*r. % 29.69/29.95 13332[2:MRR:13321.0,13331.0] || -> equal(skc3,n2) equal(skc3,n1)** equal(skc3,n0). % 29.69/29.95 13507[3:Spt:13291.0] || -> equal(n2,pv1376)**. % 29.69/29.95 13509[3:Rew:13507.0,603.0] || -> equal(pred(pv1376),n1)**. % 29.69/29.95 14044[3:Rew:13507.0,13332.0] || -> equal(skc3,pv1376) equal(skc3,n1)** equal(skc3,n0). % 29.69/29.95 14046[3:Rew:13509.0,163.0] || leq(u,n1) leq(n0,u) -> equal(a_select2(s_values7_init,u),init)**. % 29.69/29.95 16503[3:SpL:14046.2,6439.0] || leq(skc3,n1) leq(n0,skc3) equal(init,init)* -> equal(skc3,pv1376). % 29.69/29.95 16504[3:Obv:16503.2] || leq(skc3,n1)*l leq(n0,skc3) -> equal(skc3,pv1376). % 29.69/29.95 16505[3:MRR:16504.1,5.0] || leq(skc3,n1)*l -> equal(skc3,pv1376). % 29.69/29.95 18055[4:Spt:14044.0] || -> equal(skc3,pv1376)**. % 29.69/29.95 18064[4:Rew:18055.0,159.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),pv1376),init)** -> . % 30.13/30.36 18392[4:Rew:87.0,18064.0] || equal(init,init)* -> . % 30.13/30.36 18393[4:Obv:18392.0] || -> . % 30.13/30.36 18643[4:Spt:18393.0,14044.0,18055.0] || equal(skc3,pv1376)** -> . % 30.13/30.36 18644[4:Spt:18393.0,14044.1,14044.2] || -> equal(skc3,n1)** equal(skc3,n0). % 30.13/30.36 18648[4:MRR:16505.1,18643.0] || leq(skc3,n1)*l -> . % 30.13/30.36 18649[5:Spt:18644.0] || -> equal(skc3,n1)**. % 30.13/30.36 18758[5:Rew:18649.0,18648.0] || leq(n1,n1)* -> . % 30.13/30.36 18990[5:MRR:18758.0,30.0] || -> . % 30.13/30.36 19227[5:Spt:18990.0,18644.0,18649.0] || equal(skc3,n1)** -> . % 30.13/30.36 19228[5:Spt:18990.0,18644.1] || -> equal(skc3,n0)**. % 30.13/30.36 19244[5:Rew:19228.0,18648.0] || leq(n0,n1)*r -> . % 30.13/30.36 19245[5:MRR:19244.0,3129.0] || -> . % 30.13/30.36 19672[3:Spt:19245.0,13291.0,13507.0] || equal(n2,pv1376)** -> . % 30.13/30.36 19673[3:Spt:19245.0,13291.1] || -> equal(n1,pv1376)**. % 30.13/30.36 19675[3:Rew:19673.0,602.0] || -> equal(pred(pv1376),n0)**. % 30.13/30.36 20045[3:Rew:19673.0,13309.1,19673.0,13309.0] || equal(pv1376,pv1376) -> equal(skc3,pv1376)** equal(skc3,n0). % 30.13/30.36 20046[3:Obv:20045.0] || -> equal(skc3,pv1376)** equal(skc3,n0). % 30.13/30.36 20047[3:Rew:20046.1,6439.0] || equal(a_select2(s_values7_init,n0),init)** -> equal(skc3,pv1376). % 30.13/30.36 20147[3:Rew:19675.0,163.0] || leq(u,n0) leq(n0,u) -> equal(a_select2(s_values7_init,u),init)**. % 30.13/30.36 20497[4:Spt:20046.0] || -> equal(skc3,pv1376)**. % 30.13/30.36 20500[4:Rew:20497.0,159.0] || equal(a_select2(tptp_update2(s_values7_init,pv1376,init),pv1376),init)** -> . % 30.13/30.36 20675[4:Rew:87.0,20500.0] || equal(init,init)* -> . % 30.13/30.36 20676[4:Obv:20675.0] || -> . % 30.13/30.36 20908[4:Spt:20676.0,20046.0,20497.0] || equal(skc3,pv1376)** -> . % 30.13/30.36 20909[4:Spt:20676.0,20046.1] || -> equal(skc3,n0)**. % 30.13/30.36 20915[4:Rew:20909.0,20047.1] || equal(a_select2(s_values7_init,n0),init)** -> equal(pv1376,n0). % 30.13/30.36 20916[4:MRR:20915.1,5441.0] || equal(a_select2(s_values7_init,n0),init)** -> . % 30.13/30.36 22083[4:SpL:20147.2,20916.0] || leq(n0,n0) leq(n0,n0) equal(init,init)* -> . % 30.13/30.36 22084[4:Obv:22083.2] || leq(n0,n0)* -> . % 30.13/30.36 22085[4:MRR:22084.0,30.0] || -> . % 30.13/30.36 % SZS output end Refutation % 30.13/30.36 Formulae used in the proof : gauss_init_0045 reflexivity_leq leq_succ_succ gt_1_0 gt_2_0 gt_2_1 gt_3_1 successor_1 irreflexivity_gt successor_2 pred_succ successor_3 succ_plus_1_l pred_minus_1 successor_4 leq_gt1 leq_gt_pred leq_succ sel2_update_1 leq_gt2 finite_domain_0 transitivity_gt transitivity_leq sel2_update_2 finite_domain_1 finite_domain_2 finite_domain_3 % 30.13/30.36 %------------------------------------------------------------------------------