%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV198+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:36 EDT 2022 % Result : Theorem 1.59s 1.79s % Output : Refutation 1.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV198+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n007.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 : Tue Jun 14 15:17:55 EDT 2022 % 0.12/0.34 % CPUTime : % 1.59/1.79 % 1.59/1.79 SPASS V 3.9 % 1.59/1.79 SPASS beiseite: Proof found. % 1.59/1.79 % SZS status Theorem % 1.59/1.79 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.59/1.79 SPASS derived 5399 clauses, backtracked 796 clauses, performed 4 splits and kept 3273 clauses. % 1.59/1.79 SPASS allocated 90271 KBytes. % 1.59/1.79 SPASS spent 0:00:01.42 on the problem. % 1.59/1.79 0:00:00.04 for the input. % 1.59/1.79 0:00:00.08 for the FLOTTER CNF translation. % 1.59/1.79 0:00:00.03 for inferences. % 1.59/1.79 0:00:00.01 for the backtracking. % 1.59/1.79 0:00:01.10 for the reduction. % 1.59/1.79 % 1.59/1.79 % 1.59/1.79 Here is a proof with depth 3, length 87 : % 1.59/1.79 % SZS output start Refutation % 1.59/1.79 2[0:Inp] || -> leq(n0,skc3)*r. % 1.59/1.79 3[0:Inp] || -> leq(skc3,n2)*l. % 1.59/1.79 4[0:Inp] || -> leq(n0,pv5)*r. % 1.59/1.79 5[0:Inp] || -> leq(pv5,n0)*l. % 1.59/1.79 7[0:Inp] || -> leq(skc2,pv5)*l. % 1.59/1.79 8[0:Inp] || -> leq(n0,skc2)*r. % 1.59/1.79 37[0:Inp] || -> leq(u,u)*. % 1.59/1.79 38[0:Inp] || -> equal(succ(n0),n1)**. % 1.59/1.79 39[0:Inp] || gt(u,u)* -> . % 1.59/1.79 67[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 1.59/1.79 84[0:Inp] || -> equal(pred(succ(u)),u)**. % 1.59/1.79 86[0:Inp] || -> equal(a_select3(u_defuse,n0,n0),use)**. % 1.59/1.79 87[0:Inp] || -> equal(a_select3(u_defuse,n1,n0),use)**. % 1.59/1.79 88[0:Inp] || -> equal(a_select3(u_defuse,n2,n0),use)**. % 1.59/1.79 92[0:Inp] || -> equal(plus(u,n1),succ(u))**. % 1.59/1.79 96[0:Inp] || equal(a_select3(u_defuse,skc3,skc2),use)** -> . % 1.59/1.79 103[0:Inp] || -> equal(succ(succ(u)),plus(u,n2))**. % 1.59/1.79 104[0:Inp] || -> equal(succ(succ(u)),plus(n2,u))**. % 1.59/1.79 109[0:Inp] || gt(u,v)*+ -> leq(v,pred(u))*. % 1.59/1.79 131[0:Inp] || leq(u,v)* -> gt(v,u) equal(u,v). % 1.59/1.79 135[0:Inp] || leq(u,n0)*+ leq(n0,u)* -> equal(u,n0). % 1.59/1.79 137[0:Inp] || leq(u,v)* leq(v,w)* -> leq(u,w)*. % 1.59/1.79 141[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 1.59/1.79 143[0:Inp] || leq(u,n2)* leq(n0,u) -> equal(u,n2) equal(u,n1) equal(u,n0). % 1.59/1.79 152[0:Inp] || leq(u,n2) leq(v,pred(pv5)) leq(n0,v) leq(n0,u) -> equal(a_select3(u_defuse,u,v),use)**. % 1.59/1.79 178[0:Rew:38.0,67.0] || -> equal(succ(n1),n2)**. % 1.59/1.79 182[0:Rew:104.0,103.0] || -> equal(plus(n2,u),plus(u,n2))*. % 1.59/1.79 191[0:Res:152.4,96.0] || leq(n0,skc3) leq(skc3,n2) leq(skc2,pred(pv5))*r leq(n0,skc2) -> . % 1.59/1.79 198[0:Res:131.1,96.0] || leq(use,a_select3(u_defuse,skc3,skc2))*r -> gt(a_select3(u_defuse,skc3,skc2),use). % 1.59/1.79 220[0:Res:8.0,141.0] || leq(skc2,n1)*l -> equal(skc2,n1) equal(skc2,n0). % 1.59/1.79 221[0:Res:8.0,135.0] || leq(skc2,n0)*l -> equal(skc2,n0). % 1.59/1.79 333[0:Res:7.0,131.0] || -> gt(pv5,skc2)*r equal(skc2,pv5). % 1.59/1.79 380[0:MRR:191.0,191.1,191.3,2.0,3.0,8.0] || leq(skc2,pred(pv5))*r -> . % 1.59/1.79 435[1:Spt:220.1] || -> equal(skc2,n1)**. % 1.59/1.79 447[1:Rew:435.0,221.1] || leq(skc2,n0)*l -> equal(n1,n0). % 1.59/1.79 531[1:Rew:435.0,7.0] || -> leq(n1,pv5)*r. % 1.59/1.79 534[1:Rew:435.0,380.0] || leq(n1,pred(pv5))*r -> . % 1.59/1.79 565[1:Rew:435.0,447.0] || leq(n1,n0)*l -> equal(n1,n0). % 1.59/1.79 722[0:SpR:104.0,84.0] || -> equal(pred(plus(n2,u)),succ(u))**. % 1.59/1.79 746[0:SpR:182.0,722.0] || -> equal(pred(plus(u,n2)),succ(u))**. % 1.59/1.79 793[1:OCh:137.1,137.0,531.0,5.0] || -> leq(n1,n0)*l. % 1.59/1.79 794[1:MRR:565.0,793.0] || -> equal(n1,n0)**. % 1.59/1.79 798[1:Rew:794.0,38.0] || -> equal(succ(n0),n0)**. % 1.59/1.79 799[1:Rew:794.0,178.0] || -> equal(succ(n0),n2)**. % 1.59/1.79 809[1:Rew:794.0,92.0] || -> equal(plus(u,n0),succ(u))**. % 1.59/1.79 857[1:Rew:794.0,534.0] || leq(n0,pred(pv5))*r -> . % 1.59/1.79 940[1:Rew:798.0,799.0] || -> equal(n2,n0)**. % 1.59/1.79 948[1:Rew:940.0,746.0] || -> equal(pred(plus(u,n0)),succ(u))**. % 1.59/1.79 1022[1:Rew:809.0,948.0] || -> equal(pred(succ(u)),succ(u))**. % 1.59/1.79 1023[1:Rew:84.0,1022.0] || -> equal(succ(u),u)**. % 1.59/1.79 1024[1:Rew:1023.0,84.0] || -> equal(pred(u),u)**. % 1.59/1.79 1091[1:Rew:1024.0,857.0] || leq(n0,pv5)*r -> . % 1.59/1.79 1092[1:MRR:1091.0,4.0] || -> . % 1.59/1.79 1176[1:Spt:1092.0,220.1,435.0] || equal(skc2,n1)** -> . % 1.59/1.79 1177[1:Spt:1092.0,220.0,220.2] || leq(skc2,n1)*l -> equal(skc2,n0). % 1.59/1.79 1182[2:Spt:333.1] || -> equal(skc2,pv5)**. % 1.59/1.79 1192[2:Rew:1182.0,198.1] || leq(use,a_select3(u_defuse,skc3,skc2))*r -> gt(a_select3(u_defuse,skc3,pv5),use). % 1.59/1.79 1209[2:Rew:1182.0,221.1] || leq(skc2,n0)*l -> equal(pv5,n0). % 1.59/1.79 1313[2:Rew:1182.0,1209.0] || leq(pv5,n0)*l -> equal(pv5,n0). % 1.59/1.79 1314[2:MRR:1313.0,5.0] || -> equal(pv5,n0)**. % 1.59/1.79 1320[2:Rew:1314.0,1182.0] || -> equal(skc2,n0)**. % 1.59/1.79 1346[2:Rew:1314.0,1192.1,1320.0,1192.0] || leq(use,a_select3(u_defuse,skc3,n0))*r -> gt(a_select3(u_defuse,skc3,n0),use). % 1.59/1.79 6735[0:Res:3.0,143.0] || leq(n0,skc3)*r -> equal(skc3,n2) equal(skc3,n1) equal(skc3,n0). % 1.59/1.79 6810[0:MRR:6735.0,2.0] || -> equal(skc3,n2)** equal(skc3,n1) equal(skc3,n0). % 1.59/1.79 7205[3:Spt:6810.0] || -> equal(skc3,n2)**. % 1.59/1.79 7229[3:Rew:7205.0,1346.1] || leq(use,a_select3(u_defuse,skc3,n0))*r -> gt(a_select3(u_defuse,n2,n0),use). % 1.59/1.79 7381[3:Rew:88.0,7229.1] || leq(use,a_select3(u_defuse,skc3,n0))*r -> gt(use,use). % 1.59/1.79 7382[3:Rew:7205.0,7381.0] || leq(use,a_select3(u_defuse,n2,n0))*r -> gt(use,use). % 1.59/1.79 7383[3:Rew:88.0,7382.0] || leq(use,use)* -> gt(use,use). % 1.59/1.79 7384[3:MRR:7383.0,7383.1,37.0,39.0] || -> . % 1.59/1.79 7385[3:Spt:7384.0,6810.0,7205.0] || equal(skc3,n2)** -> . % 1.59/1.79 7386[3:Spt:7384.0,6810.1,6810.2] || -> equal(skc3,n1)** equal(skc3,n0). % 1.59/1.79 7389[4:Spt:7386.0] || -> equal(skc3,n1)**. % 1.59/1.79 7403[4:Rew:7389.0,1346.1] || leq(use,a_select3(u_defuse,skc3,n0))*r -> gt(a_select3(u_defuse,n1,n0),use). % 1.59/1.79 7550[4:Rew:87.0,7403.1] || leq(use,a_select3(u_defuse,skc3,n0))*r -> gt(use,use). % 1.59/1.79 7551[4:Rew:7389.0,7550.0] || leq(use,a_select3(u_defuse,n1,n0))*r -> gt(use,use). % 1.59/1.79 7552[4:Rew:87.0,7551.0] || leq(use,use)* -> gt(use,use). % 1.59/1.79 7553[4:MRR:7552.0,7552.1,37.0,39.0] || -> . % 1.59/1.79 7554[4:Spt:7553.0,7386.0,7389.0] || equal(skc3,n1)** -> . % 1.59/1.79 7555[4:Spt:7553.0,7386.1] || -> equal(skc3,n0)**. % 1.59/1.79 7682[4:Rew:7555.0,1346.1,7555.0,1346.0] || leq(use,a_select3(u_defuse,n0,n0))*r -> gt(a_select3(u_defuse,n0,n0),use). % 1.59/1.79 7683[4:Rew:86.0,7682.1,86.0,7682.0] || leq(use,use)* -> gt(use,use). % 1.59/1.79 7684[4:MRR:7683.0,7683.1,37.0,39.0] || -> . % 1.59/1.79 7685[2:Spt:7684.0,333.1,1182.0] || equal(skc2,pv5)** -> . % 1.59/1.79 7686[2:Spt:7684.0,333.0] || -> gt(pv5,skc2)*r. % 1.59/1.79 7691[2:Res:7686.0,109.0] || -> leq(skc2,pred(pv5))*r. % 1.59/1.79 7701[2:MRR:7691.0,380.0] || -> . % 1.59/1.79 % SZS output end Refutation % 1.59/1.79 Formulae used in the proof : quaternion_ds1_inuse_0009 reflexivity_leq successor_1 irreflexivity_gt successor_2 pred_succ succ_plus_1_r succ_plus_2_r succ_plus_2_l leq_gt_pred leq_gt2 finite_domain_0 transitivity_leq finite_domain_1 finite_domain_2 % 1.59/1.79 %------------------------------------------------------------------------------