%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV098+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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 3.32s 3.53s % Output : Refutation 3.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWV098+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.03/0.14 % Command : run_spass %d %s % 0.14/0.36 % Computer : n021.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Wed Jun 15 21:24:59 EDT 2022 % 0.14/0.36 % CPUTime : % 3.32/3.53 % 3.32/3.53 SPASS V 3.9 % 3.32/3.53 SPASS beiseite: Proof found. % 3.32/3.53 % SZS status Theorem % 3.32/3.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.32/3.53 SPASS derived 6789 clauses, backtracked 1432 clauses, performed 9 splits and kept 4729 clauses. % 3.32/3.53 SPASS allocated 91979 KBytes. % 3.32/3.53 SPASS spent 0:00:03.15 on the problem. % 3.32/3.53 0:00:00.04 for the input. % 3.32/3.53 0:00:00.10 for the FLOTTER CNF translation. % 3.32/3.53 0:00:00.05 for inferences. % 3.32/3.53 0:00:00.08 for the backtracking. % 3.32/3.53 0:00:02.74 for the reduction. % 3.32/3.53 % 3.32/3.53 % 3.32/3.53 Here is a proof with depth 3, length 168 : % 3.32/3.53 % SZS output start Refutation % 3.32/3.53 2[0:Inp] || -> leq(n0,skc3)*r. % 3.32/3.53 3[0:Inp] || -> leq(n0,pv5)*r. % 3.32/3.53 17[0:Inp] || -> gt(n1,n0)*l. % 3.32/3.53 18[0:Inp] || -> gt(n2,n0)*l. % 3.32/3.53 23[0:Inp] || -> gt(n2,n1)*l. % 3.32/3.53 32[0:Inp] || -> leq(u,u)*. % 3.32/3.53 33[0:Inp] || -> equal(succ(n0),n1)**. % 3.32/3.53 38[0:Inp] || -> equal(a_select2(rho_defuse,n0),use)**. % 3.32/3.53 39[0:Inp] || -> equal(a_select2(rho_defuse,n1),use)**. % 3.32/3.53 40[0:Inp] || -> equal(a_select2(rho_defuse,n2),use)**. % 3.32/3.53 41[0:Inp] || -> equal(a_select2(sigma_defuse,n0),use)**. % 3.32/3.53 42[0:Inp] || -> equal(a_select2(sigma_defuse,n1),use)**. % 3.32/3.53 43[0:Inp] || -> equal(a_select2(sigma_defuse,n2),use)**. % 3.32/3.53 44[0:Inp] || -> equal(a_select2(sigma_defuse,n3),use)**. % 3.32/3.53 45[0:Inp] || -> equal(a_select2(sigma_defuse,n4),use)**. % 3.32/3.53 46[0:Inp] || -> equal(a_select2(sigma_defuse,n5),use)**. % 3.32/3.53 47[0:Inp] || -> equal(a_select2(xinit_defuse,n3),use)**. % 3.32/3.53 48[0:Inp] || -> equal(a_select2(xinit_defuse,n4),use)**. % 3.32/3.53 49[0:Inp] || -> equal(a_select2(xinit_defuse,n5),use)**. % 3.32/3.53 50[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n0),use)**. % 3.32/3.53 51[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n1),use)**. % 3.32/3.53 52[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n2),use)**. % 3.32/3.53 53[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n3),use)**. % 3.32/3.53 54[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n4),use)**. % 3.32/3.53 55[0:Inp] || -> equal(a_select2(xinit_mean_defuse,n5),use)**. % 3.32/3.53 56[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n0),use)**. % 3.32/3.53 57[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n1),use)**. % 3.32/3.53 58[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n2),use)**. % 3.32/3.53 59[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n3),use)**. % 3.32/3.53 60[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n4),use)**. % 3.32/3.53 61[0:Inp] || -> equal(a_select2(xinit_noise_defuse,n5),use)**. % 3.32/3.53 63[0:Inp] || -> equal(succ(succ(n0)),n2)**. % 3.32/3.53 80[0:Inp] || -> equal(pred(succ(u)),u)**. % 3.32/3.53 82[0:Inp] || -> equal(a_select3(u_defuse,n0,n0),use)**. % 3.32/3.53 83[0:Inp] || -> equal(a_select3(u_defuse,n1,n0),use)**. % 3.32/3.53 84[0:Inp] || -> equal(a_select3(u_defuse,n2,n0),use)**. % 3.32/3.53 89[0:Inp] || -> equal(plus(n1,u),succ(u))**. % 3.32/3.53 90[0:Inp] || -> equal(minus(u,n1),pred(u))**. % 3.32/3.53 92[0:Inp] || -> leq(skc2,minus(plus(n1,pv5),n1))*r. % 3.32/3.53 98[0:Inp] || gt(u,v)* -> leq(v,u). % 3.32/3.53 106[0:Inp] || leq(u,v)*+ -> leq(u,succ(v))*. % 3.32/3.53 125[0:Inp] || leq(u,v) -> leq(succ(u),succ(v))*. % 3.32/3.53 137[0:Inp] || leq(u,n1)* leq(n0,u) -> equal(u,n1) equal(u,n0). % 3.32/3.53 139[0:Inp] || leq(u,n2)* leq(n0,u) -> equal(u,n2) equal(u,n1) equal(u,n0). % 3.32/3.53 146[0:Inp] || leq(u,pv5) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(z_defuse,v,u),use)**. % 3.32/3.53 147[0:Inp] || leq(u,pv5) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(u_defuse,v,u),use)**. % 3.32/3.53 176[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,skc2). % 3.32/3.53 177[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(skc3,n2). % 3.32/3.53 178[0:Inp] || equal(a_select3(u_defuse,skc3,skc2),use) equal(a_select3(z_defuse,skc3,skc2),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) -> . % 3.32/3.53 179[0:Rew:33.0,63.0] || -> equal(succ(n1),n2)**. % 3.32/3.53 193[0:Rew:80.0,92.0,90.0,92.0,89.0,92.0] || -> leq(skc2,pv5)*l. % 3.32/3.53 196[0:Rew:61.0,176.26,60.0,176.25,59.0,176.24,58.0,176.23,57.0,176.22,56.0,176.21,55.0,176.20,54.0,176.19,53.0,176.18,52.0,176.17,51.0,176.16,50.0,176.15,49.0,176.14,48.0,176.13,47.0,176.12,84.0,176.11,83.0,176.10,82.0,176.9,46.0,176.8,45.0,176.7,44.0,176.6,43.0,176.5,42.0,176.4,41.0,176.3,40.0,176.2,39.0,176.1,38.0,176.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,skc2). % 3.32/3.53 197[0:Obv:196.26] || -> leq(n0,skc2)*r. % 3.32/3.53 198[0:Rew:61.0,177.26,60.0,177.25,59.0,177.24,58.0,177.23,57.0,177.22,56.0,177.21,55.0,177.20,54.0,177.19,53.0,177.18,52.0,177.17,51.0,177.16,50.0,177.15,49.0,177.14,48.0,177.13,47.0,177.12,84.0,177.11,83.0,177.10,82.0,177.9,46.0,177.8,45.0,177.7,44.0,177.6,43.0,177.5,42.0,177.4,41.0,177.3,40.0,177.2,39.0,177.1,38.0,177.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(skc3,n2). % 3.32/3.53 199[0:Obv:198.26] || -> leq(skc3,n2)*l. % 3.32/3.53 200[0:Rew:61.0,178.28,60.0,178.27,59.0,178.26,58.0,178.25,57.0,178.24,56.0,178.23,55.0,178.22,54.0,178.21,53.0,178.20,52.0,178.19,51.0,178.18,50.0,178.17,49.0,178.16,48.0,178.15,47.0,178.14,84.0,178.13,83.0,178.12,82.0,178.11,46.0,178.10,45.0,178.9,44.0,178.8,43.0,178.7,42.0,178.6,41.0,178.5,40.0,178.4,39.0,178.3,38.0,178.2] || equal(a_select3(u_defuse,skc3,skc2),use) equal(a_select3(z_defuse,skc3,skc2),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) -> . % 3.32/3.53 201[0:Obv:200.28] || equal(a_select3(z_defuse,skc3,skc2),use)** equal(a_select3(u_defuse,skc3,skc2),use) -> . % 3.32/3.53 217[0:Res:3.0,147.0] || leq(u,pv5) leq(n0,u) leq(pv5,n2) -> equal(a_select3(u_defuse,pv5,u),use)**. % 3.32/3.53 224[0:Res:3.0,137.0] || leq(pv5,n1)*l -> equal(pv5,n1) equal(pv5,n0). % 3.32/3.53 258[0:Res:3.0,125.0] || -> leq(succ(n0),succ(pv5))*r. % 3.32/3.53 259[0:Res:3.0,106.0] || -> leq(n0,succ(pv5))*r. % 3.32/3.53 346[0:Res:2.0,139.0] || leq(skc3,n2)*l -> equal(skc3,n0) equal(skc3,n1) equal(skc3,n2). % 3.32/3.53 446[0:Rew:33.0,258.0] || -> leq(n1,succ(pv5))*r. % 3.32/3.53 448[0:MRR:346.0,199.0] || -> equal(skc3,n2)** equal(skc3,n1) equal(skc3,n0). % 3.32/3.53 516[1:Spt:224.1] || -> equal(pv5,n1)**. % 3.32/3.53 531[1:Rew:516.0,446.0] || -> leq(n1,succ(n1))*r. % 3.32/3.53 533[1:Rew:516.0,259.0] || -> leq(n0,succ(n1))*r. % 3.32/3.53 538[1:Rew:516.0,217.2] || leq(u,pv5) leq(n0,u) leq(n1,n2) -> equal(a_select3(u_defuse,pv5,u),use)**. % 3.32/3.53 559[1:Rew:516.0,146.0] || leq(u,n1) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(z_defuse,v,u),use)**. % 3.32/3.53 560[1:Rew:516.0,147.0] || leq(u,n1) leq(v,n2) leq(n0,u) leq(n0,v) -> equal(a_select3(u_defuse,v,u),use)**. % 3.32/3.53 596[1:Rew:516.0,3.0] || -> leq(n0,n1)*r. % 3.32/3.53 597[1:Rew:516.0,193.0] || -> leq(skc2,n1)*l. % 3.32/3.53 610[1:Rew:179.0,531.0] || -> leq(n1,n2)*r. % 3.32/3.53 612[1:Rew:179.0,533.0] || -> leq(n0,n2)*r. % 3.32/3.53 625[1:Rew:516.0,538.3,516.0,538.0] || leq(u,n1) leq(n0,u) leq(n1,n2) -> equal(a_select3(u_defuse,n1,u),use)**. % 3.32/3.53 626[1:MRR:625.2,610.0] || leq(u,n1) leq(n0,u) -> equal(a_select3(u_defuse,n1,u),use)**. % 3.32/3.53 682[2:Spt:448.0] || -> equal(skc3,n2)**. % 3.32/3.53 750[2:Rew:682.0,201.0] || equal(a_select3(z_defuse,n2,skc2),use)** equal(a_select3(u_defuse,skc3,skc2),use) -> . % 3.32/3.53 772[2:Rew:682.0,750.1] || equal(a_select3(z_defuse,n2,skc2),use)** equal(a_select3(u_defuse,n2,skc2),use) -> . % 3.32/3.53 3520[0:Res:23.0,98.0] || -> leq(n1,n2)*r. % 3.32/3.53 3525[0:Res:18.0,98.0] || -> leq(n0,n2)*r. % 3.32/3.53 3526[0:Res:17.0,98.0] || -> leq(n0,n1)*r. % 3.32/3.53 6062[1:Res:597.0,137.0] || leq(n0,skc2)*r -> equal(skc2,n1) equal(skc2,n0). % 3.32/3.53 6142[1:MRR:6062.0,197.0] || -> equal(skc2,n1)** equal(skc2,n0). % 3.32/3.53 6163[3:Spt:6142.0] || -> equal(skc2,n1)**. % 3.32/3.53 6166[3:Rew:6163.0,772.0] || equal(a_select3(z_defuse,n2,n1),use)** equal(a_select3(u_defuse,n2,skc2),use) -> . % 3.32/3.53 6275[3:Rew:6163.0,6166.1] || equal(a_select3(z_defuse,n2,n1),use)** equal(a_select3(u_defuse,n2,n1),use) -> . % 3.32/3.53 7552[3:SpL:559.4,6275.0] || leq(n1,n1) leq(n2,n2) leq(n0,n1) leq(n0,n2) equal(use,use) equal(a_select3(u_defuse,n2,n1),use)** -> . % 3.32/3.53 7553[3:Obv:7552.4] || leq(n1,n1) leq(n2,n2) leq(n0,n1) leq(n0,n2) equal(a_select3(u_defuse,n2,n1),use)** -> . % 3.32/3.53 7554[3:Rew:560.4,7553.4] || leq(n1,n1) leq(n2,n2) leq(n0,n1) leq(n0,n2) equal(use,use)* -> . % 3.32/3.53 7555[3:Obv:7554.4] || leq(n1,n1) leq(n2,n2)* leq(n0,n1) leq(n0,n2) -> . % 3.32/3.53 7556[3:MRR:7555.0,7555.1,7555.2,7555.3,32.0,32.0,596.0,612.0] || -> . % 3.32/3.53 7560[3:Spt:7556.0,6142.0,6163.0] || equal(skc2,n1)** -> . % 3.32/3.53 7561[3:Spt:7556.0,6142.1] || -> equal(skc2,n0)**. % 3.32/3.53 7644[3:Rew:7561.0,772.1,7561.0,772.0] || equal(a_select3(z_defuse,n2,n0),use)** equal(a_select3(u_defuse,n2,n0),use) -> . % 3.32/3.53 7645[3:Rew:84.0,7644.1] || equal(a_select3(z_defuse,n2,n0),use)** equal(use,use) -> . % 3.32/3.53 7646[3:Obv:7645.1] || equal(a_select3(z_defuse,n2,n0),use)** -> . % 3.32/3.53 7700[3:SpL:559.4,7646.0] || leq(n0,n1) leq(n2,n2) leq(n0,n0) leq(n0,n2) equal(use,use)* -> . % 3.32/3.53 7701[3:Obv:7700.4] || leq(n0,n1) leq(n2,n2)* leq(n0,n0) leq(n0,n2) -> . % 3.32/3.53 7702[3:MRR:7701.0,7701.1,7701.2,7701.3,596.0,32.0,32.0,612.0] || -> . % 3.32/3.53 7703[2:Spt:7702.0,448.0,682.0] || equal(skc3,n2)** -> . % 3.32/3.53 7704[2:Spt:7702.0,448.1,448.2] || -> equal(skc3,n1)** equal(skc3,n0). % 3.32/3.53 7724[3:Spt:7704.0] || -> equal(skc3,n1)**. % 3.32/3.53 7734[3:Rew:7724.0,201.0] || equal(a_select3(z_defuse,n1,skc2),use)** equal(a_select3(u_defuse,skc3,skc2),use) -> . % 3.32/3.53 7809[3:Rew:7724.0,7734.1] || equal(a_select3(z_defuse,n1,skc2),use)** equal(a_select3(u_defuse,n1,skc2),use) -> . % 3.32/3.53 7903[4:Spt:6142.0] || -> equal(skc2,n1)**. % 3.32/3.53 8006[4:Rew:7903.0,7809.0] || equal(a_select3(z_defuse,n1,n1),use)** equal(a_select3(u_defuse,n1,skc2),use) -> . % 3.32/3.53 8023[4:Rew:7903.0,8006.1] || equal(a_select3(z_defuse,n1,n1),use)** equal(a_select3(u_defuse,n1,n1),use) -> . % 3.32/3.53 8046[4:SpL:559.4,8023.0] || leq(n1,n1) leq(n1,n2) leq(n0,n1) leq(n0,n1) equal(use,use) equal(a_select3(u_defuse,n1,n1),use)** -> . % 3.32/3.53 8047[4:Obv:8046.4] || leq(n1,n1) leq(n1,n2) leq(n0,n1) equal(a_select3(u_defuse,n1,n1),use)** -> . % 3.32/3.53 8048[4:Rew:626.2,8047.3] || leq(n1,n1) leq(n1,n2) leq(n0,n1) equal(use,use)* -> . % 3.32/3.53 8049[4:Obv:8048.3] || leq(n1,n1) leq(n1,n2)*r leq(n0,n1) -> . % 3.32/3.53 8050[4:MRR:8049.0,8049.1,8049.2,32.0,610.0,596.0] || -> . % 3.32/3.53 8051[4:Spt:8050.0,6142.0,7903.0] || equal(skc2,n1)** -> . % 3.32/3.53 8052[4:Spt:8050.0,6142.1] || -> equal(skc2,n0)**. % 3.32/3.53 8135[4:Rew:8052.0,7809.1,8052.0,7809.0] || equal(a_select3(z_defuse,n1,n0),use)** equal(a_select3(u_defuse,n1,n0),use) -> . % 3.32/3.53 8136[4:Rew:83.0,8135.1] || equal(a_select3(z_defuse,n1,n0),use)** equal(use,use) -> . % 3.32/3.53 8137[4:Obv:8136.1] || equal(a_select3(z_defuse,n1,n0),use)** -> . % 3.32/3.53 8193[4:SpL:559.4,8137.0] || leq(n0,n1) leq(n1,n2) leq(n0,n0) leq(n0,n1) equal(use,use)* -> . % 3.32/3.53 8194[4:Obv:8193.4] || leq(n1,n2)*r leq(n0,n0) leq(n0,n1) -> . % 3.32/3.53 8195[4:MRR:8194.0,8194.1,8194.2,610.0,32.0,596.0] || -> . % 3.32/3.53 8196[3:Spt:8195.0,7704.0,7724.0] || equal(skc3,n1)** -> . % 3.32/3.53 8197[3:Spt:8195.0,7704.1] || -> equal(skc3,n0)**. % 3.32/3.53 8212[3:Rew:8197.0,201.1,8197.0,201.0] || equal(a_select3(z_defuse,n0,skc2),use)** equal(a_select3(u_defuse,n0,skc2),use) -> . % 3.32/3.53 8320[4:Spt:6142.0] || -> equal(skc2,n1)**. % 3.32/3.53 8421[4:Rew:8320.0,8212.0] || equal(a_select3(z_defuse,n0,n1),use)** equal(a_select3(u_defuse,n0,skc2),use) -> . % 3.32/3.53 8440[4:Rew:8320.0,8421.1] || equal(a_select3(z_defuse,n0,n1),use)** equal(a_select3(u_defuse,n0,n1),use) -> . % 3.32/3.53 8463[4:SpL:559.4,8440.0] || leq(n1,n1) leq(n0,n2) leq(n0,n1) leq(n0,n0) equal(use,use) equal(a_select3(u_defuse,n0,n1),use)** -> . % 3.32/3.53 8464[4:Obv:8463.4] || leq(n1,n1) leq(n0,n2) leq(n0,n1) leq(n0,n0) equal(a_select3(u_defuse,n0,n1),use)** -> . % 3.32/3.53 8465[4:Rew:560.4,8464.4] || leq(n1,n1) leq(n0,n2) leq(n0,n1) leq(n0,n0) equal(use,use)* -> . % 3.32/3.53 8466[4:Obv:8465.4] || leq(n1,n1) leq(n0,n2)*r leq(n0,n1) leq(n0,n0) -> . % 3.32/3.53 8467[4:MRR:8466.0,8466.1,8466.2,8466.3,32.0,612.0,596.0,32.0] || -> . % 3.32/3.53 8468[4:Spt:8467.0,6142.0,8320.0] || equal(skc2,n1)** -> . % 3.32/3.53 8469[4:Spt:8467.0,6142.1] || -> equal(skc2,n0)**. % 3.32/3.53 8552[4:Rew:8469.0,8212.1,8469.0,8212.0] || equal(a_select3(z_defuse,n0,n0),use)** equal(a_select3(u_defuse,n0,n0),use) -> . % 3.32/3.53 8553[4:Rew:82.0,8552.1] || equal(a_select3(z_defuse,n0,n0),use)** equal(use,use) -> . % 3.32/3.53 8554[4:Obv:8553.1] || equal(a_select3(z_defuse,n0,n0),use)** -> . % 3.32/3.53 8610[4:SpL:559.4,8554.0] || leq(n0,n1) leq(n0,n2) leq(n0,n0) leq(n0,n0) equal(use,use)* -> . % 3.32/3.53 8611[4:Obv:8610.4] || leq(n0,n1) leq(n0,n2)*r leq(n0,n0) -> . % 3.32/3.53 8612[4:MRR:8611.0,8611.1,8611.2,596.0,612.0,32.0] || -> . % 3.32/3.53 8613[1:Spt:8612.0,224.1,516.0] || equal(pv5,n1)** -> . % 3.32/3.53 8614[1:Spt:8612.0,224.0,224.2] || leq(pv5,n1)*l -> equal(pv5,n0). % 3.32/3.53 8636[2:Spt:448.0] || -> equal(skc3,n2)**. % 3.32/3.53 8648[2:Rew:8636.0,201.0] || equal(a_select3(z_defuse,n2,skc2),use)** equal(a_select3(u_defuse,skc3,skc2),use) -> . % 3.32/3.53 8727[2:Rew:8636.0,8648.1] || equal(a_select3(z_defuse,n2,skc2),use)** equal(a_select3(u_defuse,n2,skc2),use) -> . % 3.32/3.53 9610[2:SpL:146.4,8727.0] || leq(skc2,pv5) leq(n2,n2) leq(n0,skc2) leq(n0,n2) equal(use,use) equal(a_select3(u_defuse,n2,skc2),use)** -> . % 3.32/3.53 9611[2:Obv:9610.4] || leq(skc2,pv5) leq(n2,n2) leq(n0,skc2) leq(n0,n2) equal(a_select3(u_defuse,n2,skc2),use)** -> . % 3.32/3.53 9612[2:Rew:147.4,9611.4] || leq(skc2,pv5) leq(n2,n2) leq(n0,skc2) leq(n0,n2) equal(use,use)* -> . % 3.41/3.57 9613[2:Obv:9612.4] || leq(skc2,pv5)*l leq(n2,n2) leq(n0,skc2) leq(n0,n2) -> . % 3.41/3.57 9614[2:MRR:9613.0,9613.1,9613.2,9613.3,193.0,32.0,197.0,3525.0] || -> . % 3.41/3.57 9618[2:Spt:9614.0,448.0,8636.0] || equal(skc3,n2)** -> . % 3.41/3.57 9619[2:Spt:9614.0,448.1,448.2] || -> equal(skc3,n1)** equal(skc3,n0). % 3.41/3.57 9626[3:Spt:9619.0] || -> equal(skc3,n1)**. % 3.41/3.57 9637[3:Rew:9626.0,201.0] || equal(a_select3(z_defuse,n1,skc2),use)** equal(a_select3(u_defuse,skc3,skc2),use) -> . % 3.41/3.57 9713[3:Rew:9626.0,9637.1] || equal(a_select3(z_defuse,n1,skc2),use)** equal(a_select3(u_defuse,n1,skc2),use) -> . % 3.41/3.57 9805[3:SpL:146.4,9713.0] || leq(skc2,pv5) leq(n1,n2) leq(n0,skc2) leq(n0,n1) equal(use,use) equal(a_select3(u_defuse,n1,skc2),use)** -> . % 3.41/3.57 9808[3:Obv:9805.4] || leq(skc2,pv5) leq(n1,n2) leq(n0,skc2) leq(n0,n1) equal(a_select3(u_defuse,n1,skc2),use)** -> . % 3.41/3.57 9809[3:Rew:147.4,9808.4] || leq(skc2,pv5) leq(n1,n2) leq(n0,skc2) leq(n0,n1) equal(use,use)* -> . % 3.41/3.57 9810[3:Obv:9809.4] || leq(skc2,pv5)*l leq(n1,n2) leq(n0,skc2) leq(n0,n1) -> . % 3.41/3.57 9811[3:MRR:9810.0,9810.1,9810.2,9810.3,193.0,3520.0,197.0,3526.0] || -> . % 3.41/3.57 9812[3:Spt:9811.0,9619.0,9626.0] || equal(skc3,n1)** -> . % 3.41/3.57 9813[3:Spt:9811.0,9619.1] || -> equal(skc3,n0)**. % 3.41/3.57 9828[3:Rew:9813.0,201.1,9813.0,201.0] || equal(a_select3(z_defuse,n0,skc2),use)** equal(a_select3(u_defuse,n0,skc2),use) -> . % 3.41/3.57 9940[3:SpL:146.4,9828.0] || leq(skc2,pv5) leq(n0,n2) leq(n0,skc2) leq(n0,n0) equal(use,use) equal(a_select3(u_defuse,n0,skc2),use)** -> . % 3.41/3.57 9943[3:Obv:9940.4] || leq(skc2,pv5) leq(n0,n2) leq(n0,skc2) leq(n0,n0) equal(a_select3(u_defuse,n0,skc2),use)** -> . % 3.41/3.57 9944[3:Rew:147.4,9943.4] || leq(skc2,pv5) leq(n0,n2) leq(n0,skc2) leq(n0,n0) equal(use,use)* -> . % 3.41/3.57 9945[3:Obv:9944.4] || leq(skc2,pv5)*l leq(n0,n2) leq(n0,skc2) leq(n0,n0) -> . % 3.41/3.57 9946[3:MRR:9945.0,9945.1,9945.2,9945.3,193.0,3525.0,197.0,32.0] || -> . % 3.41/3.57 % SZS output end Refutation % 3.41/3.57 Formulae used in the proof : quaternion_ds1_inuse_0010 gt_succ leq_succ_gt_equiv gt_1_0 gt_2_0 gt_2_1 reflexivity_leq successor_1 successor_2 pred_succ succ_plus_1_l pred_minus_1 leq_gt1 leq_succ leq_succ_succ finite_domain_1 finite_domain_2 % 3.41/3.57 %------------------------------------------------------------------------------