%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV097+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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:16 EDT 2022 % Result : Theorem 2.83s 3.01s % Output : Refutation 2.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV097+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.11/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n009.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 03:06:38 EDT 2022 % 0.13/0.33 % CPUTime : % 2.83/3.01 % 2.83/3.01 SPASS V 3.9 % 2.83/3.01 SPASS beiseite: Proof found. % 2.83/3.01 % SZS status Theorem % 2.83/3.01 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.83/3.01 SPASS derived 6383 clauses, backtracked 800 clauses, performed 6 splits and kept 4097 clauses. % 2.83/3.01 SPASS allocated 91659 KBytes. % 2.83/3.01 SPASS spent 0:00:02.66 on the problem. % 2.83/3.01 0:00:00.04 for the input. % 2.83/3.01 0:00:00.13 for the FLOTTER CNF translation. % 2.83/3.01 0:00:00.04 for inferences. % 2.83/3.01 0:00:00.06 for the backtracking. % 2.83/3.01 0:00:02.24 for the reduction. % 2.83/3.01 % 2.83/3.01 % 2.83/3.01 Here is a proof with depth 3, length 146 : % 2.83/3.01 % SZS output start Refutation % 2.83/3.01 1[0:Inp] || -> SkC0*. % 2.83/3.01 5[0:Inp] || -> leq(n0,skc5)*r. % 2.83/3.01 6[0:Inp] || -> leq(n0,pv5)*r. % 2.83/3.01 20[0:Inp] || -> gt(n1,n0)*l. % 2.83/3.01 21[0:Inp] || -> gt(n2,n0)*l. % 2.83/3.01 26[0:Inp] || -> gt(n2,n1)*l. % 2.83/3.01 35[0:Inp] || -> leq(u,u)*. % 2.83/3.01 36[0:Inp] || -> equal(succ(n0),n1)**. % 2.83/3.01 41[0:Inp] || -> leq(skc4,minus(pv5,n1))*r. % 2.83/3.01 42[0:Inp] || -> equal(a_select2(rho_defuse,n0),use)**. % 2.83/3.01 43[0:Inp] || -> equal(a_select2(rho_defuse,n1),use)**. % 2.83/3.01 44[0:Inp] || -> equal(a_select2(rho_defuse,n2),use)**. % 2.83/3.01 45[0:Inp] || -> equal(a_select2(sigma_defuse,n0),use)**. % 2.83/3.01 46[0:Inp] || -> equal(a_select2(sigma_defuse,n1),use)**. % 2.83/3.01 47[0:Inp] || -> equal(a_select2(sigma_defuse,n2),use)**. % 2.83/3.01 48[0:Inp] || -> equal(a_select2(sigma_defuse,n3),use)**. % 2.83/3.01 49[0:Inp] || -> equal(a_select2(sigma_defuse,n4),use)**. % 2.83/3.01 50[0:Inp] || -> equal(a_select2(sigma_defuse,n5),use)**. % 2.83/3.01 51[0:Inp] || -> equal(a_select2(xinit_defuse,n3),use)**. % 2.83/3.01 52[0:Inp] || -> equal(a_select2(xinit_defuse,n4),use)**. % 2.83/3.01 53[0:Inp] || -> equal(a_select2(xinit_defuse,n5),use)**. % 2.83/3.01 54[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n0),use)**. % 2.83/3.01 55[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n1),use)**. % 2.83/3.01 56[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n2),use)**. % 2.83/3.01 57[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n3),use)**. % 2.83/3.01 58[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n4),use)**. % 2.83/3.01 59[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n5),use)**. % 2.83/3.01 60[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n0),use)**. % 2.83/3.01 61[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n1),use)**. % 2.83/3.01 62[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n2),use)**. % 2.83/3.01 63[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n3),use)**. % 2.83/3.01 64[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n4),use)**. % 2.83/3.01 65[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n5),use)**. % 2.83/3.01 66[0:Inp] || -> leq(pv5,minus(n999,n1))*r. % 2.83/3.01 67[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 2.83/3.01 84[0:Inp] || -> equal(pred(succ(u)),u)**. % 2.83/3.01 85[0:Inp] || -> equal(succ(pred(u)),u)**. % 2.83/3.01 86[0:Inp] || -> equal(a_select3(u_defuse,n0,n0),use)**. % 2.83/3.01 87[0:Inp] || -> equal(a_select3(u_defuse,n1,n0),use)**. % 2.83/3.01 88[0:Inp] || -> equal(a_select3(u_defuse,n2,n0),use)**. % 2.83/3.01 94[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 2.83/3.01 101[0:Inp] || gt(u,v)* -> leq(v,u). % 2.83/3.01 109[0:Inp] || leq(u,v)*+ -> leq(u,succ(v))*. % 2.83/3.01 128[0:Inp] || leq(u,v) -> leq(succ(u),succ(v))*. % 2.83/3.01 134[0:Inp] || leq(u,n0)*+ leq(n0,u)* -> equal(u,n0). % 2.83/3.01 140[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 2.83/3.01 142[0:Inp] || leq(u,n2)* leq(n0,u) -> equal(u,n2) equal(u,n1) equal(u,n0). % 2.83/3.01 150[0:Inp] || SkC0 leq(n0,u) leq(u,n2) leq(v,pv5) leq(n0,v) -> equal(a_select3(z_defuse,u,v),use)**. % 2.83/3.01 151[0:Inp] || SkC0 leq(n0,u) leq(u,n2) leq(v,pv5) leq(n0,v) -> equal(a_select3(u_defuse,u,v),use)**. % 2.83/3.01 179[0:Inp] || equal(a_select2(rho_defuse,n0),use) equal(a_select2(rho_defuse,n1),use) equal(a_select2(rho_defuse,n2),use) equal(a_select2(sigma_defuse,n0),use) equal(a_select2(sigma_defuse,n1),use) equal(a_select2(sigma_defuse,n2),use) equal(a_select2(sigma_defuse,n3),use) equal(a_select2(sigma_defuse,n4),use) equal(a_select2(sigma_defuse,n5),use) equal(a_select3(u_defuse,n0,n0),use) equal(a_select3(u_defuse,n1,n0),use) equal(a_select3(u_defuse,n2,n0),use)** equal(a_select2(xinit_defuse,n3),use) equal(a_select2(xinit_defuse,n4),use) equal(a_select2(xinit_defuse,n5),use) equal(a_select2(xinit_mean_defuse,n0),use) equal(a_select2(xinit_mean_defuse,n1),use) equal(a_select2(xinit_mean_defuse,n2),use) equal(a_select2(xinit_mean_defuse,n3),use) equal(a_select2(xinit_mean_defuse,n4),use) equal(a_select2(xinit_mean_defuse,n5),use) equal(a_select2(xinit_noise_defuse,n0),use) equal(a_select2(xinit_noise_defuse,n1),use) equal(a_select2(xinit_noise_defuse,n2),use) equal(a_select2(xinit_noise_defuse,n3),use) equal(a_select2(xinit_noise_defuse,n4),use) equal(a_select2(xinit_noise_defuse,n5),use) leq(n0,pv5) leq(pv5,minus(n999,n1)) SkC0 -> leq(n0,skc4). % 2.83/3.01 180[0:Inp] || equal(a_select2(rho_defuse,n0),use) equal(a_select2(rho_defuse,n1),use) equal(a_select2(rho_defuse,n2),use) equal(a_select2(sigma_defuse,n0),use) equal(a_select2(sigma_defuse,n1),use) equal(a_select2(sigma_defuse,n2),use) equal(a_select2(sigma_defuse,n3),use) equal(a_select2(sigma_defuse,n4),use) equal(a_select2(sigma_defuse,n5),use) equal(a_select3(u_defuse,n0,n0),use) equal(a_select3(u_defuse,n1,n0),use) equal(a_select3(u_defuse,n2,n0),use)** equal(a_select2(xinit_defuse,n3),use) equal(a_select2(xinit_defuse,n4),use) equal(a_select2(xinit_defuse,n5),use) equal(a_select2(xinit_mean_defuse,n0),use) equal(a_select2(xinit_mean_defuse,n1),use) equal(a_select2(xinit_mean_defuse,n2),use) equal(a_select2(xinit_mean_defuse,n3),use) equal(a_select2(xinit_mean_defuse,n4),use) equal(a_select2(xinit_mean_defuse,n5),use) equal(a_select2(xinit_noise_defuse,n0),use) equal(a_select2(xinit_noise_defuse,n1),use) equal(a_select2(xinit_noise_defuse,n2),use) equal(a_select2(xinit_noise_defuse,n3),use) equal(a_select2(xinit_noise_defuse,n4),use) equal(a_select2(xinit_noise_defuse,n5),use) leq(n0,pv5) leq(pv5,minus(n999,n1)) SkC0 -> leq(skc5,n2). % 2.83/3.01 181[0:Inp] || equal(a_select3(u_defuse,skc5,skc4),use) equal(a_select3(z_defuse,skc5,skc4),use)** equal(a_select2(rho_defuse,n0),use) equal(a_select2(rho_defuse,n1),use) equal(a_select2(rho_defuse,n2),use) equal(a_select2(sigma_defuse,n0),use) equal(a_select2(sigma_defuse,n1),use) equal(a_select2(sigma_defuse,n2),use) equal(a_select2(sigma_defuse,n3),use) equal(a_select2(sigma_defuse,n4),use) equal(a_select2(sigma_defuse,n5),use) equal(a_select3(u_defuse,n0,n0),use) equal(a_select3(u_defuse,n1,n0),use) equal(a_select3(u_defuse,n2,n0),use) equal(a_select2(xinit_defuse,n3),use) equal(a_select2(xinit_defuse,n4),use) equal(a_select2(xinit_defuse,n5),use) equal(a_select2(xinit_mean_defuse,n0),use) equal(a_select2(xinit_mean_defuse,n1),use) equal(a_select2(xinit_mean_defuse,n2),use) equal(a_select2(xinit_mean_defuse,n3),use) equal(a_select2(xinit_mean_defuse,n4),use) equal(a_select2(xinit_mean_defuse,n5),use) equal(a_select2(xinit_noise_defuse,n0),use) equal(a_select2(xinit_noise_defuse,n1),use) equal(a_select2(xinit_noise_defuse,n2),use) equal(a_select2(xinit_noise_defuse,n3),use) equal(a_select2(xinit_noise_defuse,n4),use) equal(a_select2(xinit_noise_defuse,n5),use) leq(n0,pv5) leq(pv5,minus(n999,n1)) SkC0 -> . % 2.83/3.01 182[0:Rew:36.0,67.0] || -> equal(succ(n1),n2)**. % 2.83/3.01 195[0:Rew:94.0,66.0] || -> leq(pv5,pred(n999))*r. % 2.83/3.01 196[0:Rew:94.0,41.0] || -> leq(skc4,pred(pv5))*r. % 2.83/3.01 197[0:MRR:150.0,1.0] || leq(u,pv5) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(z_defuse,v,u),use)**. % 2.83/3.01 198[0:MRR:151.0,1.0] || leq(u,pv5) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(u_defuse,v,u),use)**. % 2.83/3.01 201[0:Rew:94.0,179.28,65.0,179.26,64.0,179.25,63.0,179.24,62.0,179.23,61.0,179.22,60.0,179.21,59.0,179.20,58.0,179.19,57.0,179.18,56.0,179.17,55.0,179.16,54.0,179.15,53.0,179.14,52.0,179.13,51.0,179.12,88.0,179.11,87.0,179.10,86.0,179.9,50.0,179.8,49.0,179.7,48.0,179.6,47.0,179.5,46.0,179.4,45.0,179.3,44.0,179.2,43.0,179.1,42.0,179.0] || equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) leq(n0,pv5) leq(pv5,pred(n999))*r SkC0 -> leq(n0,skc4). % 2.83/3.01 202[0:Obv:201.26] || leq(n0,pv5) leq(pv5,pred(n999))*r SkC0 -> leq(n0,skc4). % 2.83/3.01 203[0:MRR:202.0,202.1,202.2,6.0,195.0,1.0] || -> leq(n0,skc4)*r. % 2.83/3.01 204[0:Rew:94.0,180.28,65.0,180.26,64.0,180.25,63.0,180.24,62.0,180.23,61.0,180.22,60.0,180.21,59.0,180.20,58.0,180.19,57.0,180.18,56.0,180.17,55.0,180.16,54.0,180.15,53.0,180.14,52.0,180.13,51.0,180.12,88.0,180.11,87.0,180.10,86.0,180.9,50.0,180.8,49.0,180.7,48.0,180.6,47.0,180.5,46.0,180.4,45.0,180.3,44.0,180.2,43.0,180.1,42.0,180.0] || equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) leq(n0,pv5) leq(pv5,pred(n999))*r SkC0 -> leq(skc5,n2). % 2.83/3.01 205[0:Obv:204.26] || leq(n0,pv5) leq(pv5,pred(n999))*r SkC0 -> leq(skc5,n2). % 2.83/3.01 206[0:MRR:205.0,205.1,205.2,6.0,195.0,1.0] || -> leq(skc5,n2)*l. % 2.83/3.01 207[0:Rew:94.0,181.30,65.0,181.28,64.0,181.27,63.0,181.26,62.0,181.25,61.0,181.24,60.0,181.23,59.0,181.22,58.0,181.21,57.0,181.20,56.0,181.19,55.0,181.18,54.0,181.17,53.0,181.16,52.0,181.15,51.0,181.14,88.0,181.13,87.0,181.12,86.0,181.11,50.0,181.10,49.0,181.9,48.0,181.8,47.0,181.7,46.0,181.6,45.0,181.5,44.0,181.4,43.0,181.3,42.0,181.2] || equal(a_select3(u_defuse,skc5,skc4),use) equal(a_select3(z_defuse,skc5,skc4),use)** equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) equal(use,use) leq(n0,pv5) leq(pv5,pred(n999)) SkC0 -> . % 2.83/3.01 208[0:Obv:207.28] || equal(a_select3(u_defuse,skc5,skc4),use) equal(a_select3(z_defuse,skc5,skc4),use)** leq(n0,pv5) leq(pv5,pred(n999)) SkC0 -> . % 2.83/3.01 209[0:MRR:208.2,208.3,208.4,6.0,195.0,1.0] || equal(a_select3(z_defuse,skc5,skc4),use)** equal(a_select3(u_defuse,skc5,skc4),use) -> . % 2.83/3.01 232[0:Res:6.0,140.0] || leq(pv5,n1)*l -> equal(pv5,n1) equal(pv5,n0). % 2.83/3.01 268[0:Res:6.0,128.0] || -> leq(succ(n0),succ(pv5))*r. % 2.83/3.01 269[0:Res:6.0,109.0] || -> leq(n0,succ(pv5))*r. % 2.83/3.01 354[0:Res:5.0,142.0] || leq(skc5,n2)*l -> equal(skc5,n0) equal(skc5,n1) equal(skc5,n2). % 2.83/3.01 454[0:Rew:36.0,268.0] || -> leq(n1,succ(pv5))*r. % 2.83/3.01 456[0:MRR:354.0,206.0] || -> equal(skc5,n2)** equal(skc5,n1) equal(skc5,n0). % 2.83/3.01 524[1:Spt:232.1] || -> equal(pv5,n1)**. % 2.83/3.01 533[1:Rew:524.0,196.0] || -> leq(skc4,pred(n1))*r. % 2.83/3.01 540[1:Rew:524.0,454.0] || -> leq(n1,succ(n1))*r. % 2.83/3.01 542[1:Rew:524.0,269.0] || -> leq(n0,succ(n1))*r. % 2.83/3.01 568[1:Rew:524.0,197.0] || leq(u,n1) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(z_defuse,v,u),use)**. % 2.83/3.01 605[1:Rew:524.0,6.0] || -> leq(n0,n1)*r. % 2.83/3.01 619[1:Rew:182.0,540.0] || -> leq(n1,n2)*r. % 2.83/3.01 621[1:Rew:182.0,542.0] || -> leq(n0,n2)*r. % 2.83/3.01 691[2:Spt:456.0] || -> equal(skc5,n2)**. % 2.83/3.01 759[2:Rew:691.0,209.0] || equal(a_select3(z_defuse,n2,skc4),use)** equal(a_select3(u_defuse,skc5,skc4),use) -> . % 2.83/3.01 781[2:Rew:691.0,759.1] || equal(a_select3(z_defuse,n2,skc4),use)** equal(a_select3(u_defuse,n2,skc4),use) -> . % 2.83/3.01 881[0:SpR:36.0,84.0] || -> equal(pred(n1),n0)**. % 2.83/3.01 887[1:Rew:881.0,533.0] || -> leq(skc4,n0)*l. % 2.83/3.01 3502[0:Res:26.0,101.0] || -> leq(n1,n2)*r. % 2.83/3.01 3507[0:Res:21.0,101.0] || -> leq(n0,n2)*r. % 2.83/3.01 3508[0:Res:20.0,101.0] || -> leq(n0,n1)*r. % 2.83/3.01 5620[1:Res:887.0,134.0] || leq(n0,skc4)*r -> equal(skc4,n0). % 2.83/3.01 5709[1:MRR:5620.0,203.0] || -> equal(skc4,n0)**. % 2.83/3.01 5712[2:Rew:5709.0,781.0] || equal(a_select3(z_defuse,n2,n0),use)** equal(a_select3(u_defuse,n2,skc4),use) -> . % 2.83/3.01 5814[2:Rew:5709.0,5712.1] || equal(a_select3(z_defuse,n2,n0),use)** equal(a_select3(u_defuse,n2,n0),use) -> . % 2.83/3.01 5815[2:Rew:88.0,5814.1] || equal(a_select3(z_defuse,n2,n0),use)** equal(use,use) -> . % 2.83/3.01 5816[2:Obv:5815.1] || equal(a_select3(z_defuse,n2,n0),use)** -> . % 2.83/3.01 7485[2:SpL:568.4,5816.0] || leq(n0,n1) leq(n2,n2) leq(n0,n0) leq(n0,n2) equal(use,use)* -> . % 2.83/3.01 7489[2:Obv:7485.4] || leq(n0,n1) leq(n2,n2)* leq(n0,n0) leq(n0,n2) -> . % 2.83/3.01 7490[2:MRR:7489.0,7489.1,7489.2,7489.3,605.0,35.0,35.0,621.0] || -> . % 2.83/3.01 7494[2:Spt:7490.0,456.0,691.0] || equal(skc5,n2)** -> . % 2.83/3.01 7495[2:Spt:7490.0,456.1,456.2] || -> equal(skc5,n1)** equal(skc5,n0). % 2.83/3.01 7498[1:Rew:5709.0,209.1,5709.0,209.0] || equal(a_select3(z_defuse,skc5,n0),use)** equal(a_select3(u_defuse,skc5,n0),use) -> . % 2.83/3.01 7514[3:Spt:7495.0] || -> equal(skc5,n1)**. % 2.83/3.01 7524[3:Rew:7514.0,7498.0] || equal(a_select3(z_defuse,n1,n0),use)** equal(a_select3(u_defuse,skc5,n0),use) -> . % 2.83/3.01 7599[3:Rew:7514.0,7524.1] || equal(a_select3(z_defuse,n1,n0),use)** equal(a_select3(u_defuse,n1,n0),use) -> . % 2.83/3.01 7600[3:Rew:87.0,7599.1] || equal(a_select3(z_defuse,n1,n0),use)** equal(use,use) -> . % 2.83/3.01 7601[3:Obv:7600.1] || equal(a_select3(z_defuse,n1,n0),use)** -> . % 2.83/3.01 7663[3:SpL:568.4,7601.0] || leq(n0,n1) leq(n1,n2) leq(n0,n0) leq(n0,n1) equal(use,use)* -> . % 2.83/3.01 7664[3:Obv:7663.4] || leq(n1,n2)*r leq(n0,n0) leq(n0,n1) -> . % 2.83/3.01 7665[3:MRR:7664.0,7664.1,7664.2,619.0,35.0,605.0] || -> . % 2.83/3.01 7666[3:Spt:7665.0,7495.0,7514.0] || equal(skc5,n1)** -> . % 2.83/3.01 7667[3:Spt:7665.0,7495.1] || -> equal(skc5,n0)**. % 2.83/3.01 7682[3:Rew:7667.0,7498.1,7667.0,7498.0] || equal(a_select3(z_defuse,n0,n0),use)** equal(a_select3(u_defuse,n0,n0),use) -> . % 2.83/3.01 7683[3:Rew:86.0,7682.1] || equal(a_select3(z_defuse,n0,n0),use)** equal(use,use) -> . % 2.83/3.01 7684[3:Obv:7683.1] || equal(a_select3(z_defuse,n0,n0),use)** -> . % 2.83/3.01 7762[3:SpL:568.4,7684.0] || leq(n0,n1) leq(n0,n2) leq(n0,n0) leq(n0,n0) equal(use,use)* -> . % 2.83/3.01 7763[3:Obv:7762.4] || leq(n0,n1) leq(n0,n2)*r leq(n0,n0) -> . % 2.83/3.01 7764[3:MRR:7763.0,7763.1,7763.2,605.0,621.0,35.0] || -> . % 2.83/3.01 7765[1:Spt:7764.0,232.1,524.0] || equal(pv5,n1)** -> . % 2.83/3.01 7766[1:Spt:7764.0,232.0,232.2] || leq(pv5,n1)*l -> equal(pv5,n0). % 2.83/3.01 7787[2:Spt:456.0] || -> equal(skc5,n2)**. % 2.83/3.01 7799[2:Rew:7787.0,209.0] || equal(a_select3(z_defuse,n2,skc4),use)** equal(a_select3(u_defuse,skc5,skc4),use) -> . % 2.83/3.01 7878[2:Rew:7787.0,7799.1] || equal(a_select3(z_defuse,n2,skc4),use)** equal(a_select3(u_defuse,n2,skc4),use) -> . % 2.83/3.01 8471[0:Res:196.0,109.0] || -> leq(skc4,succ(pred(pv5)))*r. % 2.83/3.01 8484[0:Rew:85.0,8471.0] || -> leq(skc4,pv5)*l. % 2.83/3.01 8742[2:SpL:197.4,7878.0] || leq(skc4,pv5) leq(n2,n2) leq(n0,skc4) leq(n0,n2) equal(use,use) equal(a_select3(u_defuse,n2,skc4),use)** -> . % 2.83/3.01 8743[2:Obv:8742.4] || leq(skc4,pv5) leq(n2,n2) leq(n0,skc4) leq(n0,n2) equal(a_select3(u_defuse,n2,skc4),use)** -> . % 2.83/3.01 8744[2:Rew:198.4,8743.4] || leq(skc4,pv5) leq(n2,n2) leq(n0,skc4) leq(n0,n2) equal(use,use)* -> . % 2.83/3.01 8745[2:Obv:8744.4] || leq(skc4,pv5)*l leq(n2,n2) leq(n0,skc4) leq(n0,n2) -> . % 2.83/3.01 8746[2:MRR:8745.0,8745.1,8745.2,8745.3,8484.0,35.0,203.0,3507.0] || -> . % 2.83/3.01 8750[2:Spt:8746.0,456.0,7787.0] || equal(skc5,n2)** -> . % 2.83/3.01 8751[2:Spt:8746.0,456.1,456.2] || -> equal(skc5,n1)** equal(skc5,n0). % 2.83/3.01 8758[3:Spt:8751.0] || -> equal(skc5,n1)**. % 2.83/3.01 8769[3:Rew:8758.0,209.0] || equal(a_select3(z_defuse,n1,skc4),use)** equal(a_select3(u_defuse,skc5,skc4),use) -> . % 2.83/3.01 8845[3:Rew:8758.0,8769.1] || equal(a_select3(z_defuse,n1,skc4),use)** equal(a_select3(u_defuse,n1,skc4),use) -> . % 2.83/3.01 8943[3:SpL:197.4,8845.0] || leq(skc4,pv5) leq(n1,n2) leq(n0,skc4) leq(n0,n1) equal(use,use) equal(a_select3(u_defuse,n1,skc4),use)** -> . % 2.83/3.01 8944[3:Obv:8943.4] || leq(skc4,pv5) leq(n1,n2) leq(n0,skc4) leq(n0,n1) equal(a_select3(u_defuse,n1,skc4),use)** -> . % 2.83/3.01 8945[3:Rew:198.4,8944.4] || leq(skc4,pv5) leq(n1,n2) leq(n0,skc4) leq(n0,n1) equal(use,use)* -> . % 2.83/3.01 8946[3:Obv:8945.4] || leq(skc4,pv5)*l leq(n1,n2) leq(n0,skc4) leq(n0,n1) -> . % 2.83/3.01 8947[3:MRR:8946.0,8946.1,8946.2,8946.3,8484.0,3502.0,203.0,3508.0] || -> . % 2.83/3.01 8948[3:Spt:8947.0,8751.0,8758.0] || equal(skc5,n1)** -> . % 2.83/3.01 8949[3:Spt:8947.0,8751.1] || -> equal(skc5,n0)**. % 2.83/3.01 8964[3:Rew:8949.0,209.1,8949.0,209.0] || equal(a_select3(z_defuse,n0,skc4),use)** equal(a_select3(u_defuse,n0,skc4),use) -> . % 2.83/3.01 9079[3:SpL:197.4,8964.0] || leq(skc4,pv5) leq(n0,n2) leq(n0,skc4) leq(n0,n0) equal(use,use) equal(a_select3(u_defuse,n0,skc4),use)** -> . % 2.83/3.01 9080[3:Obv:9079.4] || leq(skc4,pv5) leq(n0,n2) leq(n0,skc4) leq(n0,n0) equal(a_select3(u_defuse,n0,skc4),use)** -> . % 2.83/3.01 9081[3:Rew:198.4,9080.4] || leq(skc4,pv5) leq(n0,n2) leq(n0,skc4) leq(n0,n0) equal(use,use)* -> . % 2.83/3.01 9082[3:Obv:9081.4] || leq(skc4,pv5)*l leq(n0,n2) leq(n0,skc4) leq(n0,n0) -> . % 2.83/3.01 9083[3:MRR:9082.0,9082.1,9082.2,9082.3,8484.0,3507.0,203.0,35.0] || -> . % 2.83/3.01 % SZS output end Refutation % 2.83/3.01 Formulae used in the proof : quaternion_ds1_inuse_0009 gt_succ leq_succ_gt_equiv gt_1_0 gt_2_0 gt_2_1 reflexivity_leq successor_1 successor_2 pred_succ succ_pred pred_minus_1 leq_gt1 leq_succ leq_succ_succ finite_domain_0 finite_domain_1 finite_domain_2 % 2.83/3.05 %------------------------------------------------------------------------------