%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV553-1.004 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:44:11 EDT 2022 % Result : Unsatisfiable 0.51s 0.70s % Output : Refutation 0.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV553-1.004 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n013.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 : Wed Jun 15 04:43:43 EDT 2022 % 0.12/0.33 % CPUTime : % 0.51/0.70 % 0.51/0.70 SPASS V 3.9 % 0.51/0.70 SPASS beiseite: Proof found. % 0.51/0.70 % SZS status Theorem % 0.51/0.70 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.51/0.70 SPASS derived 1097 clauses, backtracked 256 clauses, performed 36 splits and kept 718 clauses. % 0.51/0.70 SPASS allocated 66213 KBytes. % 0.51/0.70 SPASS spent 0:00:00.36 on the problem. % 0.51/0.70 0:00:00.03 for the input. % 0.51/0.70 0:00:00.00 for the FLOTTER CNF translation. % 0.51/0.70 0:00:00.04 for inferences. % 0.51/0.70 0:00:00.01 for the backtracking. % 0.51/0.70 0:00:00.24 for the reduction. % 0.51/0.70 % 0.51/0.70 % 0.51/0.70 Here is a proof with depth 10, length 511 : % 0.51/0.70 % SZS output start Refutation % 0.51/0.70 1[0:Inp] || -> equal(select(store(u,v,w),v),w)**. % 0.51/0.70 2[0:Inp] || -> equal(u,v) equal(select(store(w,u,x),v),select(w,v))**. % 0.51/0.70 3[0:Inp] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)))**. % 0.51/0.70 4[0:Inp] || equal(select(a2,sk(a1,a2)),select(a1,sk(a1,a2)))** -> . % 0.51/0.70 10[0:SpR:3.0,1.0] || -> equal(select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))**. % 0.51/0.70 11[0:SpR:3.0,2.1] || -> equal(i4,u) equal(select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),u),select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),u))**. % 0.51/0.70 18[0:SpR:2.1,3.0] || -> equal(i3,i2) equal(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)),store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)))**. % 0.51/0.70 20[0:Rew:1.0,10.0] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))**. % 0.51/0.70 21[0:Rew:20.0,3.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)))**. % 0.51/0.70 22[0:Rew:2.1,11.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),u))**. % 0.51/0.70 24[0:Rew:2.1,18.1] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)))**. % 0.51/0.70 34[0:SpR:2.1,21.0] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)))**. % 0.51/0.70 43[0:Rew:2.1,34.1] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)))**. % 0.51/0.70 44[0:Rew:24.1,43.1] || -> equal(i3,i2) equal(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)))**. % 0.51/0.70 45[0:Rew:44.1,24.1] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)))**. % 0.51/0.70 53[0:SpR:20.0,2.1] || -> equal(i4,i3) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4),select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4))**. % 0.51/0.70 56[0:SpR:2.1,20.0] || -> equal(i3,i2) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4),select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4))**. % 0.51/0.70 57[0:SpR:2.1,20.0] || -> equal(i2,i1) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4))**. % 0.51/0.70 58[0:Rew:2.1,53.1] || -> equal(i4,i3) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4))**. % 0.51/0.70 60[0:Rew:2.1,57.1] || -> equal(i2,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4))**. % 0.51/0.70 62[0:Rew:2.1,56.1] || -> equal(i3,i2) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4))**. % 0.51/0.70 65[1:Spt:58.0] || -> equal(i4,i3)**. % 0.51/0.70 67[1:Rew:65.0,20.0] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i3),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i3))**. % 0.51/0.70 68[1:Rew:65.0,22.0] || -> equal(i3,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),u))**. % 0.51/0.70 71[1:Rew:65.0,60.1] || -> equal(i2,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i3),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i3))**. % 0.51/0.70 72[1:Rew:65.0,62.1] || -> equal(i3,i2) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i3),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i3))**. % 0.51/0.70 73[1:Rew:1.0,71.1,1.0,71.1] || -> equal(i2,i1) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3))**. % 0.51/0.70 74[1:Rew:1.0,72.1,1.0,72.1] || -> equal(i3,i2) equal(select(store(a2,i1,select(a1,i1)),i3),select(store(a1,i1,select(a2,i1)),i3))**. % 0.51/0.70 75[1:Rew:1.0,67.0,1.0,67.0] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 76[1:Rew:2.1,68.1,2.1,68.1] || -> equal(i3,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),u),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 84[2:Spt:74.0] || -> equal(i3,i2)**. % 0.51/0.70 86[2:Rew:84.0,73.1] || -> equal(i2,i1) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2))**. % 0.51/0.70 87[2:Rew:84.0,75.0] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2))**. % 0.51/0.70 88[2:Rew:84.0,76.0] || -> equal(i2,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),u),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 91[2:Rew:1.0,86.1,1.0,86.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 92[2:Rew:1.0,87.0,1.0,87.0] || -> equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 93[2:Rew:2.1,88.1,2.1,88.1] || -> equal(i2,u) equal(select(store(a2,i1,select(a1,i1)),u),select(store(a1,i1,select(a2,i1)),u))**. % 0.51/0.70 107[3:Spt:91.0] || -> equal(i2,i1)**. % 0.51/0.70 111[3:Rew:107.0,92.0] || -> equal(select(store(a2,i1,select(a1,i1)),i1),select(store(a1,i1,select(a2,i1)),i1))**. % 0.51/0.70 112[3:Rew:107.0,93.0] || -> equal(i1,u) equal(select(store(a2,i1,select(a1,i1)),u),select(store(a1,i1,select(a2,i1)),u))**. % 0.51/0.70 113[3:Rew:1.0,111.0,1.0,111.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 114[3:Rew:2.1,112.1,2.1,112.1] || -> equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 127[3:SpL:114.1,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i1). % 0.51/0.70 128[3:Obv:127.0] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 129[3:Rew:128.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 130[3:Rew:113.0,129.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 131[3:Obv:130.0] || -> . % 0.51/0.70 132[3:Spt:131.0,91.0,107.0] || equal(i2,i1)** -> . % 0.51/0.70 133[3:Spt:131.0,91.1] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 141[2:SpR:93.1,1.0] || -> equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i1),select(a1,i1))**. % 0.51/0.70 142[2:SpR:93.1,2.1] || -> equal(i2,u) equal(i1,u) equal(select(store(a1,i1,select(a2,i1)),u),select(a2,u))**. % 0.51/0.70 145[2:Rew:1.0,141.1] || -> equal(i2,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 146[3:MRR:145.0,132.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 151[2:Rew:2.1,142.2] || -> equal(i2,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 156[2:SpL:151.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 157[2:Obv:156.0] || -> equal(sk(a1,a2),i2)** equal(sk(a1,a2),i1). % 0.51/0.70 165[4:Spt:157.0] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 166[4:Rew:165.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 167[4:Rew:133.0,166.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 168[4:Obv:167.0] || -> . % 0.51/0.70 169[4:Spt:168.0,157.0,165.0] || equal(sk(a1,a2),i2)** -> . % 0.51/0.70 170[4:Spt:168.0,157.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 172[4:Rew:170.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 173[4:Rew:146.0,172.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 174[4:Obv:173.0] || -> . % 0.51/0.70 175[2:Spt:174.0,74.0,84.0] || equal(i3,i2)** -> . % 0.51/0.70 176[2:Spt:174.0,74.1] || -> equal(select(store(a2,i1,select(a1,i1)),i3),select(store(a1,i1,select(a2,i1)),i3))**. % 0.51/0.70 178[2:SpR:176.0,2.1] || -> equal(i3,i1) equal(select(store(a1,i1,select(a2,i1)),i3),select(a2,i3))**. % 0.51/0.70 180[2:Rew:2.1,178.1] || -> equal(i3,i1) equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 182[3:Spt:180.0] || -> equal(i3,i1)**. % 0.51/0.70 183[3:Rew:182.0,176.0] || -> equal(select(store(a2,i1,select(a1,i1)),i1),select(store(a1,i1,select(a2,i1)),i1))**. % 0.51/0.70 185[3:Rew:182.0,175.0] || equal(i2,i1)** -> . % 0.51/0.70 188[3:Rew:182.0,76.0] || -> equal(i1,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),u),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 192[3:Rew:1.0,183.0,1.0,183.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 195[3:Rew:192.0,188.1] || -> equal(i1,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),u),select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 224[3:SpR:195.1,1.0] || -> equal(i2,i1) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2),select(store(a1,i1,select(a1,i1)),i2))**. % 0.51/0.70 225[3:SpR:195.1,2.1] || -> equal(i1,u) equal(i2,u) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 229[3:Rew:2.1,224.1,1.0,224.1,2.1,224.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 230[3:MRR:229.0,185.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 232[3:Rew:2.1,225.2,2.1,225.2,2.1,225.2] || -> equal(i1,u) equal(i2,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 240[3:SpL:232.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i2). % 0.51/0.70 241[3:Obv:240.0] || -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i2)**. % 0.51/0.70 242[4:Spt:241.0] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 243[4:Rew:242.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 244[4:Rew:192.0,243.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 245[4:Obv:244.0] || -> . % 0.51/0.70 246[4:Spt:245.0,241.0,242.0] || equal(sk(a1,a2),i1)** -> . % 0.51/0.70 247[4:Spt:245.0,241.1] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 249[4:Rew:247.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 250[4:Rew:230.0,249.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 251[4:Obv:250.0] || -> . % 0.51/0.70 252[3:Spt:251.0,180.0,182.0] || equal(i3,i1)** -> . % 0.51/0.70 253[3:Spt:251.0,180.1] || -> equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 271[4:Spt:73.0] || -> equal(i2,i1)**. % 0.51/0.70 275[4:Rew:271.0,76.1] || -> equal(i3,u) equal(select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),u),select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),u))**. % 0.51/0.70 278[4:Rew:1.0,275.1,1.0,275.1] || -> equal(i3,u) equal(select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),u),select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),u))**. % 0.51/0.70 285[4:SpR:278.1,1.0] || -> equal(i3,i1) equal(select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1),select(a2,i1))**. % 0.51/0.70 286[4:SpR:278.1,2.1] || -> equal(i3,u) equal(i1,u) equal(select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 289[4:Rew:1.0,285.1] || -> equal(i3,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 290[4:MRR:289.0,252.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 296[4:Rew:2.1,286.2,2.1,286.2,2.1,286.2] || -> equal(i3,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 307[4:SpL:296.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i3) equal(sk(a1,a2),i1). % 0.51/0.70 308[4:Obv:307.0] || -> equal(sk(a1,a2),i3)** equal(sk(a1,a2),i1). % 0.51/0.70 309[5:Spt:308.0] || -> equal(sk(a1,a2),i3)**. % 0.51/0.70 310[5:Rew:309.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.70 311[5:Rew:253.0,310.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.70 312[5:Obv:311.0] || -> . % 0.51/0.70 313[5:Spt:312.0,308.0,309.0] || equal(sk(a1,a2),i3)** -> . % 0.51/0.70 314[5:Spt:312.0,308.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 316[5:Rew:314.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 317[5:Rew:290.0,316.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 318[5:Obv:317.0] || -> . % 0.51/0.70 319[4:Spt:318.0,73.0,271.0] || equal(i2,i1)** -> . % 0.51/0.70 320[4:Spt:318.0,73.1] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3))**. % 0.51/0.70 333[1:SpR:76.1,1.0] || -> equal(i3,i2) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 334[1:SpR:76.1,2.1] || -> equal(i3,u) equal(i2,u) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 338[1:Rew:1.0,333.1] || -> equal(i3,i2) equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 339[2:MRR:338.0,175.0] || -> equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 344[1:Rew:2.1,334.2] || -> equal(i3,u) equal(i2,u) equal(select(store(a2,i1,select(a1,i1)),u),select(store(a1,i1,select(a2,i1)),u))**. % 0.51/0.70 347[2:SpR:339.0,2.1] || -> equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i2),select(a2,i2))**. % 0.51/0.70 349[2:Rew:2.1,347.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 350[4:MRR:349.0,319.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 364[1:SpR:344.2,1.0] || -> equal(i3,i1) equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i1),select(a1,i1))**. % 0.51/0.70 365[1:SpR:344.2,2.1] || -> equal(i3,u) equal(i2,u) equal(i1,u) equal(select(store(a1,i1,select(a2,i1)),u),select(a2,u))**. % 0.51/0.70 369[1:Rew:1.0,364.2] || -> equal(i3,i1) equal(i2,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 370[4:MRR:369.0,369.1,252.0,319.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 381[1:Rew:2.1,365.3] || -> equal(i3,u) equal(i2,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 387[1:SpL:381.3,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i3) equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 388[1:Obv:387.0] || -> equal(sk(a1,a2),i3)** equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 398[5:Spt:388.0] || -> equal(sk(a1,a2),i3)**. % 0.51/0.70 399[5:Rew:398.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.70 400[5:Rew:253.0,399.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.70 401[5:Obv:400.0] || -> . % 0.51/0.70 402[5:Spt:401.0,388.0,398.0] || equal(sk(a1,a2),i3)** -> . % 0.51/0.70 403[5:Spt:401.0,388.1,388.2] || -> equal(sk(a1,a2),i2)** equal(sk(a1,a2),i1). % 0.51/0.70 404[6:Spt:403.0] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 406[6:Rew:404.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 407[6:Rew:350.0,406.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 408[6:Obv:407.0] || -> . % 0.51/0.70 409[6:Spt:408.0,403.0,404.0] || equal(sk(a1,a2),i2)** -> . % 0.51/0.70 410[6:Spt:408.0,403.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 413[6:Rew:410.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 414[6:Rew:370.0,413.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 415[6:Obv:414.0] || -> . % 0.51/0.70 416[1:Spt:415.0,58.0,65.0] || equal(i4,i3)** -> . % 0.51/0.70 417[1:Spt:415.0,58.1] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4))**. % 0.51/0.70 419[1:SpR:417.0,2.1] || -> equal(i4,i2) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4),select(store(a2,i1,select(a1,i1)),i4))**. % 0.51/0.70 421[1:SpR:2.1,417.0] || -> equal(i2,i1) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4),select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4))**. % 0.51/0.70 422[1:Rew:2.1,419.1] || -> equal(i4,i2) equal(select(store(a2,i1,select(a1,i1)),i4),select(store(a1,i1,select(a2,i1)),i4))**. % 0.51/0.70 423[1:Rew:2.1,421.1] || -> equal(i2,i1) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4))**. % 0.51/0.70 424[2:Spt:422.0] || -> equal(i4,i2)**. % 0.51/0.70 425[2:Rew:424.0,417.0] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2))**. % 0.51/0.70 426[2:Rew:424.0,416.0] || equal(i3,i2)** -> . % 0.51/0.70 431[2:Rew:424.0,45.1] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i2,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2)))**. % 0.51/0.70 434[2:Rew:424.0,21.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i2,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2)))**. % 0.51/0.70 435[2:Rew:424.0,423.1] || -> equal(i2,i1) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2))**. % 0.51/0.70 436[2:Rew:1.0,435.1,1.0,435.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 437[2:Rew:1.0,425.0,1.0,425.0] || -> equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 444[2:Rew:1.0,431.1,2.1,431.1] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i2,select(store(a2,i1,select(a1,i1)),i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(store(a2,i1,select(a1,i1)),i2)))**. % 0.51/0.70 445[2:Rew:437.0,444.1] || -> equal(i3,i2) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i2,select(store(a1,i1,select(a2,i1)),i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(store(a1,i1,select(a2,i1)),i2)))**. % 0.51/0.70 446[2:MRR:445.0,426.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i2,select(store(a1,i1,select(a2,i1)),i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(store(a1,i1,select(a2,i1)),i2)))**. % 0.51/0.70 448[2:Rew:437.0,434.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i2)))**. % 0.51/0.70 450[3:Spt:436.0] || -> equal(i2,i1)**. % 0.51/0.70 452[3:Rew:450.0,426.0] || equal(i3,i1)** -> . % 0.51/0.70 453[3:Rew:450.0,437.0] || -> equal(select(store(a2,i1,select(a1,i1)),i1),select(store(a1,i1,select(a2,i1)),i1))**. % 0.51/0.70 458[3:Rew:450.0,448.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),i1,select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),i1)),store(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),i1,select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),i1)))**. % 0.51/0.70 459[3:Rew:1.0,453.0,1.0,453.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 468[3:Rew:1.0,458.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a2,i1)),i3)),i1,select(store(store(store(a1,i1,select(a2,i1)),i1,select(a2,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),i1)),store(store(store(store(a1,i1,select(a2,i1)),i1,select(a2,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),i1,select(store(store(store(a1,i1,select(a2,i1)),i1,select(a2,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),i1)))**. % 0.51/0.70 469[3:Rew:459.0,468.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i1,select(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i1)),store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i1,select(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i1)))**. % 0.51/0.70 477[3:SpR:2.1,469.0] || -> equal(i3,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i1,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i1)),store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i1,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i1)))**. % 0.51/0.70 479[3:Rew:2.1,477.1,2.1,477.1,2.1,477.1,2.1,477.1,1.0,477.1] || -> equal(i3,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a1,i3)),i1,select(a1,i1)),store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i1,select(a1,i1)))**. % 0.51/0.70 480[3:MRR:479.0,452.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a1,i3)),i1,select(a1,i1)),store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i1,select(a1,i1)))**. % 0.51/0.70 485[3:SpR:480.0,2.1] || -> equal(i1,u) equal(select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i1,select(a1,i1)),u),select(store(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a1,i3)),u))**. % 0.51/0.70 487[3:Rew:2.1,485.1] || -> equal(i1,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a1,i3)),u),select(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a2,i3)),u))**. % 0.51/0.70 488[3:SpR:487.1,1.0] || -> equal(i3,i1) equal(select(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i3),select(a1,i3))**. % 0.51/0.70 489[3:SpR:487.1,2.1] || -> equal(i1,u) equal(i3,u) equal(select(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(a2,i3)),u),select(store(store(a2,i1,select(a1,i1)),i1,select(a1,i1)),u))**. % 0.51/0.70 491[3:Rew:1.0,488.1] || -> equal(i3,i1) equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 492[3:MRR:491.0,452.0] || -> equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 495[3:Rew:2.1,489.2,2.1,489.2,2.1,489.2,2.1,489.2,2.1,489.2] || -> equal(i1,u) equal(i3,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 500[3:SpL:495.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i3). % 0.51/0.70 501[3:Obv:500.0] || -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i3)**. % 0.51/0.70 506[4:Spt:501.0] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 507[4:Rew:506.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 508[4:Rew:459.0,507.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 509[4:Obv:508.0] || -> . % 0.51/0.70 510[4:Spt:509.0,501.0,506.0] || equal(sk(a1,a2),i1)** -> . % 0.51/0.70 511[4:Spt:509.0,501.1] || -> equal(sk(a1,a2),i3)**. % 0.51/0.70 513[4:Rew:511.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.70 514[4:Rew:492.0,513.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.70 515[4:Obv:514.0] || -> . % 0.51/0.70 516[3:Spt:515.0,436.0,450.0] || equal(i2,i1)** -> . % 0.51/0.70 517[3:Spt:515.0,436.1] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 535[2:SpR:2.1,446.0] || -> equal(i2,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i2,select(a1,i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(a1,i2)))**. % 0.51/0.70 536[3:MRR:535.0,516.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i2,select(a1,i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(a1,i2)))**. % 0.51/0.70 540[3:SpR:536.0,2.1] || -> equal(i2,u) equal(select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(a1,i2)),u),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),u))**. % 0.51/0.70 542[3:SpR:2.1,536.0] || -> equal(i3,i1) equal(store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i2,select(a1,i2)),store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i2,select(a1,i2)))**. % 0.51/0.70 543[3:Rew:2.1,542.1] || -> equal(i3,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i2,select(a1,i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(a2,i3)),i2,select(a1,i2)))**. % 0.51/0.70 544[3:Rew:2.1,540.1] || -> equal(i2,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),u))**. % 0.51/0.70 559[4:Spt:543.0] || -> equal(i3,i1)**. % 0.51/0.70 570[4:Rew:559.0,544.1] || -> equal(i2,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(store(a1,i1,select(a2,i1)),i1)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i1,select(store(a2,i1,select(a1,i1)),i1)),u))**. % 0.51/0.70 571[4:Rew:1.0,570.1,1.0,570.1] || -> equal(i2,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i1,select(a1,i1)),u))**. % 0.51/0.70 576[4:SpR:571.1,1.0] || -> equal(i2,i1) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i1,select(a1,i1)),i1),select(a2,i1))**. % 0.51/0.70 577[4:SpR:571.1,2.1] || -> equal(i2,u) equal(i1,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i1,select(a1,i1)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),u))**. % 0.51/0.70 579[4:Rew:1.0,576.1] || -> equal(i2,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 580[4:MRR:579.0,516.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 592[4:Rew:2.1,577.2,2.1,577.2,2.1,577.2,2.1,577.2,2.1,577.2] || -> equal(i2,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 597[4:SpL:592.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 598[4:Obv:597.0] || -> equal(sk(a1,a2),i2)** equal(sk(a1,a2),i1). % 0.51/0.70 613[5:Spt:598.0] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 614[5:Rew:613.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 615[5:Rew:517.0,614.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 616[5:Obv:615.0] || -> . % 0.51/0.70 617[5:Spt:616.0,598.0,613.0] || equal(sk(a1,a2),i2)** -> . % 0.51/0.70 618[5:Spt:616.0,598.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 620[5:Rew:618.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 621[5:Rew:580.0,620.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 622[5:Obv:621.0] || -> . % 0.51/0.70 623[4:Spt:622.0,543.0,559.0] || equal(i3,i1)** -> . % 0.51/0.70 624[4:Spt:622.0,543.1] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i2,select(a1,i2)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(a2,i3)),i2,select(a1,i2)))**. % 0.51/0.70 627[4:SpR:624.0,2.1] || -> equal(i2,u) equal(select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(a2,i3)),i2,select(a1,i2)),u),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),u))**. % 0.51/0.70 629[4:Rew:2.1,627.1] || -> equal(i2,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(a2,i3)),u))**. % 0.51/0.70 647[4:SpR:629.1,1.0] || -> equal(i3,i2) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(a2,i3)),i3),select(a1,i3))**. % 0.51/0.70 648[4:SpR:629.1,2.1] || -> equal(i2,u) equal(i3,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a1,i2)),i3,select(a2,i3)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),u))**. % 0.51/0.70 650[4:Rew:1.0,647.1] || -> equal(i3,i2) equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 651[4:MRR:650.0,426.0] || -> equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 655[4:Rew:2.1,648.2,2.1,648.2,2.1,648.2] || -> equal(i2,u) equal(i3,u) equal(select(store(a2,i1,select(a1,i1)),u),select(store(a1,i1,select(a2,i1)),u))**. % 0.51/0.70 657[4:SpR:655.2,1.0] || -> equal(i2,i1) equal(i3,i1) equal(select(store(a1,i1,select(a2,i1)),i1),select(a1,i1))**. % 0.51/0.70 658[4:SpR:655.2,2.1] || -> equal(i2,u) equal(i3,u) equal(i1,u) equal(select(store(a1,i1,select(a2,i1)),u),select(a2,u))**. % 0.51/0.70 661[4:Rew:1.0,657.2] || -> equal(i2,i1) equal(i3,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 662[4:MRR:661.0,661.1,516.0,623.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 678[4:Rew:2.1,658.3] || -> equal(i2,u) equal(i3,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 698[4:SpL:678.3,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i2) equal(sk(a1,a2),i3) equal(sk(a1,a2),i1). % 0.51/0.70 699[4:Obv:698.0] || -> equal(sk(a1,a2),i2) equal(sk(a1,a2),i3)** equal(sk(a1,a2),i1). % 0.51/0.70 700[5:Spt:699.0] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 701[5:Rew:700.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 702[5:Rew:517.0,701.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 703[5:Obv:702.0] || -> . % 0.51/0.70 704[5:Spt:703.0,699.0,700.0] || equal(sk(a1,a2),i2)** -> . % 0.51/0.70 705[5:Spt:703.0,699.1,699.2] || -> equal(sk(a1,a2),i3)** equal(sk(a1,a2),i1). % 0.51/0.70 706[6:Spt:705.0] || -> equal(sk(a1,a2),i3)**. % 0.51/0.70 708[6:Rew:706.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.70 709[6:Rew:651.0,708.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.70 710[6:Obv:709.0] || -> . % 0.51/0.70 711[6:Spt:710.0,705.0,706.0] || equal(sk(a1,a2),i3)** -> . % 0.51/0.70 712[6:Spt:710.0,705.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 715[6:Rew:712.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 716[6:Rew:662.0,715.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 717[6:Obv:716.0] || -> . % 0.51/0.70 718[2:Spt:717.0,422.0,424.0] || equal(i4,i2)** -> . % 0.51/0.70 719[2:Spt:717.0,422.1] || -> equal(select(store(a2,i1,select(a1,i1)),i4),select(store(a1,i1,select(a2,i1)),i4))**. % 0.51/0.70 720[2:SpR:719.0,2.1] || -> equal(i4,i1) equal(select(store(a1,i1,select(a2,i1)),i4),select(a2,i4))**. % 0.51/0.70 722[2:Rew:2.1,720.1] || -> equal(i4,i1) equal(select(a2,i4),select(a1,i4))**. % 0.51/0.70 723[3:Spt:722.0] || -> equal(i4,i1)**. % 0.51/0.70 724[3:Rew:723.0,719.0] || -> equal(select(store(a2,i1,select(a1,i1)),i1),select(store(a1,i1,select(a2,i1)),i1))**. % 0.51/0.70 725[3:Rew:723.0,416.0] || equal(i3,i1)** -> . % 0.51/0.70 726[3:Rew:723.0,718.0] || equal(i2,i1)** -> . % 0.51/0.70 729[3:Rew:723.0,60.1] || -> equal(i2,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i1),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i1))**. % 0.51/0.70 732[3:Rew:723.0,22.0] || -> equal(i1,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),u))**. % 0.51/0.70 736[3:Rew:723.0,21.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i1,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i1)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i1,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i1)))**. % 0.51/0.70 737[3:Rew:1.0,724.0,1.0,724.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 740[3:Rew:737.0,729.1] || -> equal(i2,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3)),i1),select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i1))**. % 0.51/0.70 741[3:MRR:740.0,726.0] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3)),i1),select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i1))**. % 0.51/0.70 744[3:Rew:737.0,732.1] || -> equal(i1,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3,select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),u),select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3)),u))**. % 0.51/0.70 749[3:Rew:737.0,736.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3,select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3)),i1)),store(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3)),i1)))**. % 0.51/0.70 759[3:SpR:2.1,741.0] || -> equal(i3,i2) equal(select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i1),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a1,i1)),i3)),i1))**. % 0.51/0.70 762[3:Rew:2.1,759.1] || -> equal(i3,i2) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a1,i1)),i3)),i1),select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i1))**. % 0.51/0.70 766[4:Spt:762.0] || -> equal(i3,i2)**. % 0.51/0.70 773[4:Rew:766.0,749.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i2)),i1)),store(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i2)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i2)),i1)))**. % 0.51/0.70 779[4:Rew:1.0,773.0,1.0,773.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(a1,i1,select(a1,i1)),i2)),i1)),store(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(a1,i1,select(a1,i1)),i2)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(a1,i1,select(a1,i1)),i2)),i1)))**. % 0.51/0.70 788[4:SpR:2.1,779.0] || -> equal(i2,i1) equal(store(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(a1,i2)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(a1,i2)),i1)),store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(a1,i2)),i1)))**. % 0.51/0.70 790[4:Rew:2.1,788.1,1.0,788.1,2.1,788.1,2.1,788.1] || -> equal(i2,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2,select(a2,i2)),i1,select(a1,i1)),store(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2,select(a1,i2)),i1,select(a1,i1)))**. % 0.51/0.70 791[4:MRR:790.0,726.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2,select(a2,i2)),i1,select(a1,i1)),store(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2,select(a1,i2)),i1,select(a1,i1)))**. % 0.51/0.70 799[4:SpR:791.0,2.1] || -> equal(i1,u) equal(select(store(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2,select(a1,i2)),i1,select(a1,i1)),u),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2,select(a2,i2)),u))**. % 0.51/0.70 801[4:Rew:2.1,799.1] || -> equal(i1,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2,select(a2,i2)),u),select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2,select(a1,i2)),u))**. % 0.51/0.70 802[4:SpR:801.1,1.0] || -> equal(i2,i1) equal(select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2,select(a1,i2)),i2),select(a2,i2))**. % 0.51/0.70 803[4:SpR:801.1,2.1] || -> equal(i1,u) equal(i2,u) equal(select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2,select(a1,i2)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),u))**. % 0.51/0.70 806[4:Rew:1.0,802.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 807[4:MRR:806.0,726.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 813[4:Rew:2.1,803.2,2.1,803.2,2.1,803.2,2.1,803.2,2.1,803.2] || -> equal(i1,u) equal(i2,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 822[4:SpL:813.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i2). % 0.51/0.70 823[4:Obv:822.0] || -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i2)**. % 0.51/0.70 824[5:Spt:823.0] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 825[5:Rew:824.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 826[5:Rew:737.0,825.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 827[5:Obv:826.0] || -> . % 0.51/0.70 828[5:Spt:827.0,823.0,824.0] || equal(sk(a1,a2),i1)** -> . % 0.51/0.70 829[5:Spt:827.0,823.1] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 831[5:Rew:829.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 832[5:Rew:807.0,831.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 833[5:Obv:832.0] || -> . % 0.51/0.70 834[4:Spt:833.0,762.0,766.0] || equal(i3,i2)** -> . % 0.51/0.70 835[4:Spt:833.0,762.1] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a1,i1)),i3)),i1),select(store(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i1))**. % 0.51/0.70 884[3:SpR:744.1,1.0] || -> equal(i3,i1) equal(select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3)),i3),select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 885[3:SpR:744.1,2.1] || -> equal(i1,u) equal(i3,u) equal(select(store(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 891[3:Rew:1.0,884.1] || -> equal(i3,i1) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3),select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 892[3:MRR:891.0,725.0] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),i3),select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 897[3:Rew:2.1,885.2] || -> equal(i1,u) equal(i3,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a1,i1)),i2)),u),select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 903[3:SpR:892.0,2.1] || -> equal(i3,i2) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3),select(store(a2,i1,select(a1,i1)),i3))**. % 0.51/0.70 906[3:Rew:2.1,903.1] || -> equal(i3,i2) equal(select(store(a2,i1,select(a1,i1)),i3),select(store(a1,i1,select(a1,i1)),i3))**. % 0.51/0.70 907[4:MRR:906.0,834.0] || -> equal(select(store(a2,i1,select(a1,i1)),i3),select(store(a1,i1,select(a1,i1)),i3))**. % 0.51/0.70 917[4:SpR:907.0,2.1] || -> equal(i3,i1) equal(select(store(a1,i1,select(a1,i1)),i3),select(a2,i3))**. % 0.51/0.70 919[4:Rew:2.1,917.1] || -> equal(i3,i1) equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 920[4:MRR:919.0,725.0] || -> equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 940[3:SpR:897.2,1.0] || -> equal(i2,i1) equal(i3,i2) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2),select(store(a1,i1,select(a1,i1)),i2))**. % 0.51/0.70 941[3:SpR:897.2,2.1] || -> equal(i1,u) equal(i3,u) equal(i2,u) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 946[3:Rew:2.1,940.2,1.0,940.2,2.1,940.2] || -> equal(i2,i1) equal(i3,i2) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 947[4:MRR:946.0,946.1,726.0,834.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 954[3:Rew:2.1,941.3,2.1,941.3,2.1,941.3] || -> equal(i1,u) equal(i3,u) equal(i2,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 963[3:SpL:954.3,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i3) equal(sk(a1,a2),i2). % 0.51/0.70 964[3:Obv:963.0] || -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i3)** equal(sk(a1,a2),i2). % 0.51/0.70 973[5:Spt:964.0] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 974[5:Rew:973.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 975[5:Rew:737.0,974.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 976[5:Obv:975.0] || -> . % 0.51/0.70 977[5:Spt:976.0,964.0,973.0] || equal(sk(a1,a2),i1)** -> . % 0.51/0.70 978[5:Spt:976.0,964.1,964.2] || -> equal(sk(a1,a2),i3)** equal(sk(a1,a2),i2). % 0.51/0.70 979[6:Spt:978.0] || -> equal(sk(a1,a2),i3)**. % 0.51/0.70 981[6:Rew:979.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.70 982[6:Rew:920.0,981.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.70 983[6:Obv:982.0] || -> . % 0.51/0.70 984[6:Spt:983.0,978.0,979.0] || equal(sk(a1,a2),i3)** -> . % 0.51/0.70 985[6:Spt:983.0,978.1] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 988[6:Rew:985.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 989[6:Rew:947.0,988.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 990[6:Obv:989.0] || -> . % 0.51/0.70 991[3:Spt:990.0,722.0,723.0] || equal(i4,i1)** -> . % 0.51/0.70 992[3:Spt:990.0,722.1] || -> equal(select(a2,i4),select(a1,i4))**. % 0.51/0.70 997[4:Spt:423.0] || -> equal(i2,i1)**. % 0.51/0.70 1000[4:Rew:997.0,62.1] || -> equal(i3,i2) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4))**. % 0.51/0.70 1003[4:Rew:997.0,22.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),u))**. % 0.51/0.70 1007[4:Rew:1.0,1000.1,1.0,1000.1] || -> equal(i3,i2) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4))**. % 0.51/0.70 1008[4:Rew:997.0,1007.0] || -> equal(i3,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4))**. % 0.51/0.70 1009[4:Rew:2.1,1008.1,2.1,1008.1] || -> equal(i3,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4))**. % 0.51/0.70 1011[4:Rew:1.0,1003.1,1.0,1003.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),u),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),u))**. % 0.51/0.70 1021[5:Spt:1009.0] || -> equal(i3,i1)**. % 0.51/0.70 1024[5:Rew:1021.0,1011.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1)),u),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),u))**. % 0.51/0.70 1028[5:Rew:1.0,1024.1,1.0,1024.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(a1,i1)),u),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),u))**. % 0.51/0.70 1040[5:SpR:1028.1,1.0] || -> equal(i4,i1) equal(select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),i1),select(a1,i1))**. % 0.51/0.70 1041[5:SpR:1028.1,2.1] || -> equal(i4,u) equal(i1,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),u),select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),u))**. % 0.51/0.70 1044[5:Rew:1.0,1040.1] || -> equal(i4,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1045[5:MRR:1044.0,991.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1052[5:Rew:2.1,1041.2,2.1,1041.2,2.1,1041.2,2.1,1041.2,2.1,1041.2] || -> equal(i4,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 1057[5:SpL:1052.2,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i4) equal(sk(a1,a2),i1). % 0.51/0.70 1058[5:Obv:1057.0] || -> equal(sk(a1,a2),i4)** equal(sk(a1,a2),i1). % 0.51/0.70 1064[6:Spt:1058.0] || -> equal(sk(a1,a2),i4)**. % 0.51/0.70 1065[6:Rew:1064.0,4.0] || equal(select(a2,i4),select(a1,i4))** -> . % 0.51/0.70 1066[6:Rew:992.0,1065.0] || equal(select(a1,i4),select(a1,i4))* -> . % 0.51/0.70 1067[6:Obv:1066.0] || -> . % 0.51/0.70 1068[6:Spt:1067.0,1058.0,1064.0] || equal(sk(a1,a2),i4)** -> . % 0.51/0.70 1069[6:Spt:1067.0,1058.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 1071[6:Rew:1069.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 1072[6:Rew:1045.0,1071.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 1073[6:Obv:1072.0] || -> . % 0.51/0.70 1074[5:Spt:1073.0,1009.0,1021.0] || equal(i3,i1)** -> . % 0.51/0.70 1075[5:Spt:1073.0,1009.1] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4))**. % 0.51/0.70 1100[4:SpR:1011.1,1.0] || -> equal(i4,i3) equal(select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),i3),select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3))**. % 0.51/0.70 1101[4:SpR:1011.1,2.1] || -> equal(i4,u) equal(i3,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),u),select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),u))**. % 0.51/0.70 1105[4:Rew:1.0,1100.1] || -> equal(i4,i3) equal(select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3),select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3))**. % 0.51/0.70 1106[4:MRR:1105.0,416.0] || -> equal(select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3),select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3))**. % 0.51/0.70 1111[4:Rew:2.1,1101.2] || -> equal(i4,u) equal(i3,u) equal(select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),u),select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),u))**. % 0.51/0.70 1124[4:SpR:1106.0,2.1] || -> equal(i3,i1) equal(select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3),select(store(a2,i1,select(a1,i1)),i3))**. % 0.51/0.70 1126[4:Rew:2.1,1124.1,2.1,1124.1,2.1,1124.1] || -> equal(i3,i1) equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 1127[5:MRR:1126.0,1074.0] || -> equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 1132[4:SpR:1111.2,1.0] || -> equal(i4,i1) equal(i3,i1) equal(select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1),select(a2,i1))**. % 0.51/0.70 1133[4:SpR:1111.2,2.1] || -> equal(i4,u) equal(i3,u) equal(i1,u) equal(select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 1137[4:Rew:1.0,1132.2] || -> equal(i4,i1) equal(i3,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1138[5:MRR:1137.0,1137.1,991.0,1074.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1150[4:Rew:2.1,1133.3,2.1,1133.3,2.1,1133.3] || -> equal(i4,u) equal(i3,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 1165[4:SpL:1150.3,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i4) equal(sk(a1,a2),i3) equal(sk(a1,a2),i1). % 0.51/0.70 1166[4:Obv:1165.0] || -> equal(sk(a1,a2),i4)** equal(sk(a1,a2),i3) equal(sk(a1,a2),i1). % 0.51/0.70 1167[6:Spt:1166.0] || -> equal(sk(a1,a2),i4)**. % 0.51/0.70 1168[6:Rew:1167.0,4.0] || equal(select(a2,i4),select(a1,i4))** -> . % 0.51/0.70 1169[6:Rew:992.0,1168.0] || equal(select(a1,i4),select(a1,i4))* -> . % 0.51/0.70 1170[6:Obv:1169.0] || -> . % 0.51/0.70 1171[6:Spt:1170.0,1166.0,1167.0] || equal(sk(a1,a2),i4)** -> . % 0.51/0.70 1172[6:Spt:1170.0,1166.1,1166.2] || -> equal(sk(a1,a2),i3)** equal(sk(a1,a2),i1). % 0.51/0.70 1173[7:Spt:1172.0] || -> equal(sk(a1,a2),i3)**. % 0.51/0.70 1175[7:Rew:1173.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.70 1176[7:Rew:1127.0,1175.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.70 1177[7:Obv:1176.0] || -> . % 0.51/0.70 1178[7:Spt:1177.0,1172.0,1173.0] || equal(sk(a1,a2),i3)** -> . % 0.51/0.70 1179[7:Spt:1177.0,1172.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 1182[7:Rew:1179.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 1183[7:Rew:1138.0,1182.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 1184[7:Obv:1183.0] || -> . % 0.51/0.70 1185[4:Spt:1184.0,423.0,997.0] || equal(i2,i1)** -> . % 0.51/0.70 1186[4:Spt:1184.0,423.1] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4))**. % 0.51/0.70 1187[4:MRR:60.0,1185.0] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4))**. % 0.51/0.70 1202[4:SpR:2.1,1187.0] || -> equal(i3,i2) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4))**. % 0.51/0.70 1204[4:Rew:2.1,1202.1] || -> equal(i3,i2) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4))**. % 0.51/0.70 1205[5:Spt:1204.0] || -> equal(i3,i2)**. % 0.51/0.70 1210[5:Rew:1205.0,22.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2)),u))**. % 0.51/0.70 1215[5:Rew:1.0,1210.1,1.0,1210.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2,select(store(a2,i1,select(a1,i1)),i2)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(a1,i1,select(a2,i1)),i2)),u))**. % 0.51/0.70 1243[5:SpR:1215.1,1.0] || -> equal(i4,i2) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2),select(store(a2,i1,select(a1,i1)),i2))**. % 0.51/0.70 1244[5:SpR:1215.1,2.1] || -> equal(i4,u) equal(i2,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,select(store(a1,i1,select(a2,i1)),i2)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),u))**. % 0.51/0.70 1249[5:Rew:1.0,1243.1] || -> equal(i4,i2) equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 1250[5:MRR:1249.0,718.0] || -> equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 1259[5:Rew:2.1,1244.2,2.1,1244.2,2.1,1244.2] || -> equal(i4,u) equal(i2,u) equal(select(store(a2,i1,select(a1,i1)),u),select(store(a1,i1,select(a2,i1)),u))**. % 0.51/0.70 1260[5:SpR:1250.0,2.1] || -> equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i2),select(a2,i2))**. % 0.51/0.70 1262[5:Rew:2.1,1260.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 1263[5:MRR:1262.0,1185.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 1278[5:SpR:1259.2,1.0] || -> equal(i4,i1) equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i1),select(a1,i1))**. % 0.51/0.70 1279[5:SpR:1259.2,2.1] || -> equal(i4,u) equal(i2,u) equal(i1,u) equal(select(store(a1,i1,select(a2,i1)),u),select(a2,u))**. % 0.51/0.70 1283[5:Rew:1.0,1278.2] || -> equal(i4,i1) equal(i2,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1284[5:MRR:1283.0,1283.1,991.0,1185.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1297[5:Rew:2.1,1279.3] || -> equal(i4,u) equal(i2,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 1303[5:SpL:1297.3,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i4) equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 1304[5:Obv:1303.0] || -> equal(sk(a1,a2),i4)** equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 1314[6:Spt:1304.0] || -> equal(sk(a1,a2),i4)**. % 0.51/0.70 1315[6:Rew:1314.0,4.0] || equal(select(a2,i4),select(a1,i4))** -> . % 0.51/0.70 1316[6:Rew:992.0,1315.0] || equal(select(a1,i4),select(a1,i4))* -> . % 0.51/0.70 1317[6:Obv:1316.0] || -> . % 0.51/0.70 1318[6:Spt:1317.0,1304.0,1314.0] || equal(sk(a1,a2),i4)** -> . % 0.51/0.70 1319[6:Spt:1317.0,1304.1,1304.2] || -> equal(sk(a1,a2),i2)** equal(sk(a1,a2),i1). % 0.51/0.70 1320[7:Spt:1319.0] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 1322[7:Rew:1320.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 1323[7:Rew:1263.0,1322.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 1324[7:Obv:1323.0] || -> . % 0.51/0.70 1325[7:Spt:1324.0,1319.0,1320.0] || equal(sk(a1,a2),i2)** -> . % 0.51/0.70 1326[7:Spt:1324.0,1319.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 1329[7:Rew:1326.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 1330[7:Rew:1284.0,1329.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 1331[7:Obv:1330.0] || -> . % 0.51/0.70 1332[5:Spt:1331.0,1204.0,1205.0] || equal(i3,i2)** -> . % 0.51/0.70 1333[5:Spt:1331.0,1204.1] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4))**. % 0.51/0.70 1338[5:SpR:2.1,1333.0] || -> equal(i3,i1) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4))**. % 0.51/0.70 1340[5:Rew:2.1,1338.1] || -> equal(i3,i1) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(a2,i3)),i4))**. % 0.51/0.70 1369[6:Spt:1340.0] || -> equal(i3,i1)**. % 0.51/0.70 1373[6:Rew:1369.0,21.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1)),i4)))**. % 0.51/0.70 1389[6:SpR:2.1,1373.0] || -> equal(i2,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i1,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(a2,i1,select(a1,i1)),i1)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(a2,i1,select(a1,i1)),i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i1,select(store(a2,i1,select(a1,i1)),i1)),i4)))**. % 0.51/0.70 1396[6:Rew:2.1,1389.1,1.0,1389.1,2.1,1389.1,2.1,1389.1,1.0,1389.1] || -> equal(i2,i1) equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4)))**. % 0.51/0.70 1397[6:MRR:1396.0,1185.0] || -> equal(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4)),store(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4)))**. % 0.51/0.70 1417[6:SpR:1397.0,2.1] || -> equal(i4,u) equal(select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i4)),u),select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),u))**. % 0.51/0.70 1420[6:Rew:2.1,1417.1] || -> equal(i4,u) equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),u),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),u))**. % 0.51/0.70 1431[6:SpR:1420.1,1.0] || -> equal(i4,i1) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),i1),select(a2,i1))**. % 0.51/0.70 1432[6:SpR:1420.1,2.1] || -> equal(i4,u) equal(i1,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1,select(a1,i1)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),u))**. % 0.51/0.70 1435[6:Rew:1.0,1431.1] || -> equal(i4,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1436[6:MRR:1435.0,991.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1452[6:Rew:2.1,1432.2] || -> equal(i4,u) equal(i1,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),u),select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),u))**. % 0.51/0.70 1453[6:Rew:1436.0,1452.2] || -> equal(i4,u) equal(i1,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),u),select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),u))**. % 0.51/0.70 1478[6:SpR:1453.2,1.0] || -> equal(i4,i2) equal(i2,i1) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2),select(a1,i2))**. % 0.51/0.70 1479[6:SpR:1453.2,2.1] || -> equal(i4,u) equal(i1,u) equal(i2,u) equal(select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 1482[6:Rew:1.0,1478.2] || -> equal(i4,i2) equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 1483[6:MRR:1482.0,1482.1,718.0,1185.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 1492[6:Rew:2.1,1479.3,2.1,1479.3,2.1,1479.3] || -> equal(i4,u) equal(i1,u) equal(i2,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 1498[6:SpL:1492.3,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i4) equal(sk(a1,a2),i1) equal(sk(a1,a2),i2). % 0.51/0.70 1499[6:Obv:1498.0] || -> equal(sk(a1,a2),i4)** equal(sk(a1,a2),i1) equal(sk(a1,a2),i2). % 0.51/0.70 1500[7:Spt:1499.0] || -> equal(sk(a1,a2),i4)**. % 0.51/0.70 1501[7:Rew:1500.0,4.0] || equal(select(a2,i4),select(a1,i4))** -> . % 0.51/0.70 1502[7:Rew:992.0,1501.0] || equal(select(a1,i4),select(a1,i4))* -> . % 0.51/0.70 1503[7:Obv:1502.0] || -> . % 0.51/0.70 1504[7:Spt:1503.0,1499.0,1500.0] || equal(sk(a1,a2),i4)** -> . % 0.51/0.70 1505[7:Spt:1503.0,1499.1,1499.2] || -> equal(sk(a1,a2),i1) equal(sk(a1,a2),i2)**. % 0.51/0.70 1506[8:Spt:1505.0] || -> equal(sk(a1,a2),i1)**. % 0.51/0.70 1508[8:Rew:1506.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.70 1509[8:Rew:1436.0,1508.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.70 1510[8:Obv:1509.0] || -> . % 0.51/0.70 1511[8:Spt:1510.0,1505.0,1506.0] || equal(sk(a1,a2),i1)** -> . % 0.51/0.70 1512[8:Spt:1510.0,1505.1] || -> equal(sk(a1,a2),i2)**. % 0.51/0.70 1515[8:Rew:1512.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.70 1516[8:Rew:1483.0,1515.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.70 1517[8:Obv:1516.0] || -> . % 0.51/0.70 1518[6:Spt:1517.0,1340.0,1369.0] || equal(i3,i1)** -> . % 0.51/0.70 1519[6:Spt:1517.0,1340.1] || -> equal(select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4),select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(a2,i3)),i4))**. % 0.51/0.70 1583[0:SpR:22.1,1.0] || -> equal(i4,i3) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i3),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 1584[0:SpR:22.1,2.1] || -> equal(i4,u) equal(i3,u) equal(select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),u),select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),u))**. % 0.51/0.70 1590[0:Rew:1.0,1583.1] || -> equal(i4,i3) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 1591[1:MRR:1590.0,416.0] || -> equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))**. % 0.51/0.70 1596[0:Rew:2.1,1584.2] || -> equal(i4,u) equal(i3,u) equal(select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),u),select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u))**. % 0.51/0.70 1602[1:SpR:1591.0,2.1] || -> equal(i3,i2) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3),select(store(a2,i1,select(a1,i1)),i3))**. % 0.51/0.70 1605[1:Rew:2.1,1602.1] || -> equal(i3,i2) equal(select(store(a2,i1,select(a1,i1)),i3),select(store(a1,i1,select(a2,i1)),i3))**. % 0.51/0.70 1606[5:MRR:1605.0,1332.0] || -> equal(select(store(a2,i1,select(a1,i1)),i3),select(store(a1,i1,select(a2,i1)),i3))**. % 0.51/0.70 1631[5:SpR:1606.0,2.1] || -> equal(i3,i1) equal(select(store(a1,i1,select(a2,i1)),i3),select(a2,i3))**. % 0.51/0.70 1633[5:Rew:2.1,1631.1] || -> equal(i3,i1) equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 1634[6:MRR:1633.0,1518.0] || -> equal(select(a2,i3),select(a1,i3))**. % 0.51/0.70 1652[0:SpR:1596.2,1.0] || -> equal(i4,i2) equal(i3,i2) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 1653[0:SpR:1596.2,2.1] || -> equal(i4,u) equal(i3,u) equal(i2,u) equal(select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),u),select(store(a2,i1,select(a1,i1)),u))**. % 0.51/0.70 1658[0:Rew:1.0,1652.2] || -> equal(i4,i2) equal(i3,i2) equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 1659[5:MRR:1658.0,1658.1,718.0,1332.0] || -> equal(select(store(a2,i1,select(a1,i1)),i2),select(store(a1,i1,select(a2,i1)),i2))**. % 0.51/0.70 1671[0:Rew:2.1,1653.3] || -> equal(i4,u) equal(i3,u) equal(i2,u) equal(select(store(a2,i1,select(a1,i1)),u),select(store(a1,i1,select(a2,i1)),u))**. % 0.51/0.70 1674[5:SpR:1659.0,2.1] || -> equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i2),select(a2,i2))**. % 0.51/0.70 1676[5:Rew:2.1,1674.1] || -> equal(i2,i1) equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 1677[5:MRR:1676.0,1185.0] || -> equal(select(a2,i2),select(a1,i2))**. % 0.51/0.70 1687[0:SpR:1671.3,1.0] || -> equal(i4,i1) equal(i3,i1) equal(i2,i1) equal(select(store(a1,i1,select(a2,i1)),i1),select(a1,i1))**. % 0.51/0.70 1688[0:SpR:1671.3,2.1] || -> equal(i4,u) equal(i3,u) equal(i2,u) equal(i1,u) equal(select(store(a1,i1,select(a2,i1)),u),select(a2,u))**. % 0.51/0.70 1693[0:Rew:1.0,1687.3] || -> equal(i4,i1) equal(i3,i1) equal(i2,i1) equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1694[6:MRR:1693.0,1693.1,1693.2,991.0,1518.0,1185.0] || -> equal(select(a2,i1),select(a1,i1))**. % 0.51/0.70 1718[0:Rew:2.1,1688.4] || -> equal(i4,u) equal(i3,u) equal(i2,u) equal(i1,u) equal(select(a2,u),select(a1,u))**. % 0.51/0.70 1751[0:SpL:1718.4,4.0] || equal(select(a1,sk(a1,a2)),select(a1,sk(a1,a2)))* -> equal(sk(a1,a2),i4) equal(sk(a1,a2),i3) equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 1752[0:Obv:1751.0] || -> equal(sk(a1,a2),i4)** equal(sk(a1,a2),i3) equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.70 1753[7:Spt:1752.0] || -> equal(sk(a1,a2),i4)**. % 0.51/0.70 1754[7:Rew:1753.0,4.0] || equal(select(a2,i4),select(a1,i4))** -> . % 0.51/0.70 1755[7:Rew:992.0,1754.0] || equal(select(a1,i4),select(a1,i4))* -> . % 0.51/0.70 1756[7:Obv:1755.0] || -> . % 0.51/0.70 1757[7:Spt:1756.0,1752.0,1753.0] || equal(sk(a1,a2),i4)** -> . % 0.51/0.70 1758[7:Spt:1756.0,1752.1,1752.2,1752.3] || -> equal(sk(a1,a2),i3)** equal(sk(a1,a2),i2) equal(sk(a1,a2),i1). % 0.51/0.72 1759[8:Spt:1758.0] || -> equal(sk(a1,a2),i3)**. % 0.51/0.72 1761[8:Rew:1759.0,4.0] || equal(select(a2,i3),select(a1,i3))** -> . % 0.51/0.72 1762[8:Rew:1634.0,1761.0] || equal(select(a1,i3),select(a1,i3))* -> . % 0.51/0.72 1763[8:Obv:1762.0] || -> . % 0.51/0.72 1764[8:Spt:1763.0,1758.0,1759.0] || equal(sk(a1,a2),i3)** -> . % 0.51/0.72 1765[8:Spt:1763.0,1758.1,1758.2] || -> equal(sk(a1,a2),i2)** equal(sk(a1,a2),i1). % 0.51/0.72 1766[9:Spt:1765.0] || -> equal(sk(a1,a2),i2)**. % 0.51/0.72 1769[9:Rew:1766.0,4.0] || equal(select(a2,i2),select(a1,i2))** -> . % 0.51/0.72 1770[9:Rew:1677.0,1769.0] || equal(select(a1,i2),select(a1,i2))* -> . % 0.51/0.72 1771[9:Obv:1770.0] || -> . % 0.51/0.72 1772[9:Spt:1771.0,1765.0,1766.0] || equal(sk(a1,a2),i2)** -> . % 0.51/0.72 1773[9:Spt:1771.0,1765.1] || -> equal(sk(a1,a2),i1)**. % 0.51/0.72 1777[9:Rew:1773.0,4.0] || equal(select(a2,i1),select(a1,i1))** -> . % 0.51/0.72 1778[9:Rew:1694.0,1777.0] || equal(select(a1,i1),select(a1,i1))* -> . % 0.51/0.72 1779[9:Obv:1778.0] || -> . % 0.51/0.72 % SZS output end Refutation % 0.51/0.72 Formulae used in the proof : a1 a2 hyp0 goal % 0.51/0.72 %------------------------------------------------------------------------------