%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG183+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 : 300s % DateTime : Fri Oct 3 07:44:05 PM UTC 2025 % Result : Theorem 86.15s 86.37s % Output : Proof 86.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG183+1 : TPTP v9.2.0. Released v2.7.0. % 0.03/0.13 % Command : duper %s % 0.13/0.35 % Computer : n012.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 09:49:23 EDT 2025 % 0.13/0.35 % CPUTime : % 86.15/86.37 SZS status Theorem for theBenchmark.p % 86.15/86.37 SZS output start Proof for theBenchmark.p % 86.15/86.37 Clause #0 (by assumption #[]): Eq % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 86.15/86.37 (Ne e11 e14)) % 86.15/86.37 (Ne e12 e13)) % 86.15/86.37 (Ne e12 e14)) % 86.15/86.37 (Ne e13 e14)) % 86.15/86.37 True % 86.15/86.37 Clause #1 (by assumption #[]): Eq % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 86.15/86.37 (Ne e21 e24)) % 86.15/86.37 (Ne e22 e23)) % 86.15/86.37 (Ne e22 e24)) % 86.15/86.37 (Ne e23 e24)) % 86.15/86.37 True % 86.15/86.37 Clause #3 (by assumption #[]): Eq % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) % 86.15/86.37 (Eq (op1 e10 e12) e10)) % 86.15/86.37 (Eq (op1 e10 e13) e11)) % 86.15/86.37 (Eq (op1 e10 e14) e13)) % 86.15/86.37 (Eq (op1 e11 e10) e10)) % 86.15/86.37 (Eq (op1 e11 e11) e11)) % 86.15/86.37 (Eq (op1 e11 e12) e12)) % 86.15/86.37 (Eq (op1 e11 e13) e13)) % 86.15/86.37 (Eq (op1 e11 e14) e14)) % 86.15/86.37 (Eq (op1 e12 e10) e11)) % 86.15/86.37 (Eq (op1 e12 e11) e14)) % 86.15/86.37 (Eq (op1 e12 e12) e13)) % 86.15/86.37 (Eq (op1 e12 e13) e10)) % 86.15/86.37 (Eq (op1 e12 e14) e12)) % 86.15/86.37 (Eq (op1 e13 e10) e13)) % 86.15/86.37 (Eq (op1 e13 e11) e10)) % 86.15/86.37 (Eq (op1 e13 e12) e14)) % 86.15/86.37 (Eq (op1 e13 e13) e12)) % 86.15/86.37 (Eq (op1 e13 e14) e11)) % 86.15/86.37 (Eq (op1 e14 e10) e12)) % 86.15/86.37 (Eq (op1 e14 e11) e13)) % 86.15/86.37 (Eq (op1 e14 e12) e11)) % 86.15/86.37 (Eq (op1 e14 e13) e14)) % 86.15/86.37 (Eq (op1 e14 e14) e10)) % 86.15/86.37 True % 86.15/86.37 Clause #4 (by assumption #[]): Eq % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And % 86.15/86.37 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e23)) % 86.15/86.37 (Eq (op2 e20 e22) e24)) % 86.15/86.37 (Eq (op2 e20 e23) e21)) % 86.15/86.37 (Eq (op2 e20 e24) e22)) % 86.15/86.37 (Eq (op2 e21 e20) e24)) % 86.15/86.37 (Eq (op2 e21 e21) e21)) % 86.15/86.37 (Eq (op2 e21 e22) e23)) % 86.15/86.37 (Eq (op2 e21 e23) e22)) % 86.15/86.37 (Eq (op2 e21 e24) e20)) % 86.15/86.37 (Eq (op2 e22 e20) e21)) % 86.15/86.37 (Eq (op2 e22 e21) e20)) % 86.15/86.37 (Eq (op2 e22 e22) e22)) % 86.15/86.37 (Eq (op2 e22 e23) e24)) % 86.15/86.37 (Eq (op2 e22 e24) e23)) % 86.15/86.37 (Eq (op2 e23 e20) e22)) % 86.15/86.41 (Eq (op2 e23 e21) e24)) % 86.15/86.41 (Eq (op2 e23 e22) e20)) % 86.15/86.41 (Eq (op2 e23 e23) e23)) % 86.15/86.41 (Eq (op2 e23 e24) e21)) % 86.15/86.41 (Eq (op2 e24 e20) e23)) % 86.15/86.41 (Eq (op2 e24 e21) e22)) % 86.15/86.41 (Eq (op2 e24 e22) e21)) % 86.15/86.41 (Eq (op2 e24 e23) e20)) % 86.15/86.41 (Eq (op2 e24 e24) e24)) % 86.15/86.41 True % 86.15/86.41 Clause #5 (by assumption #[]): Eq % 86.15/86.41 (Not % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 86.15/86.41 (Eq (h e10) e24)) % 86.15/86.41 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 86.15/86.41 (Eq (h e11) e24))) % 86.15/86.41 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 86.15/86.41 (Eq (h e12) e24))) % 86.15/86.41 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 86.15/86.41 (Eq (h e13) e24))) % 86.15/86.41 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) % 86.15/86.41 (Eq (h e14) e24))) % 86.15/86.41 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) % 86.15/86.41 (Eq (j e20) e14))) % 86.15/86.41 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 86.15/86.41 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 86.15/86.41 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 86.15/86.41 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) → % 86.15/86.41 Not % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e10 % 86.15/86.41 e10)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e10) % 86.15/86.41 (h % 86.15/86.41 e10))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e10 % 86.15/86.41 e11)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e10) % 86.15/86.41 (h % 86.15/86.41 e11)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e10 % 86.15/86.41 e12)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e10) % 86.15/86.41 (h % 86.15/86.41 e12)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e10 % 86.15/86.41 e13)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e10) % 86.15/86.41 (h % 86.15/86.41 e13)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e10 % 86.15/86.41 e14)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e10) % 86.15/86.41 (h % 86.15/86.41 e14)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e11 % 86.15/86.41 e10)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e11) % 86.15/86.41 (h % 86.15/86.41 e10)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e11 % 86.15/86.41 e11)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e11) % 86.15/86.41 (h % 86.15/86.41 e11)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e11 % 86.15/86.41 e12)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e11) % 86.15/86.41 (h % 86.15/86.41 e12)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e11 % 86.15/86.41 e13)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e11) % 86.15/86.41 (h % 86.15/86.41 e13)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 % 86.15/86.41 e11 % 86.15/86.41 e14)) % 86.15/86.41 (op2 % 86.15/86.41 (h % 86.15/86.41 e11) % 86.15/86.41 (h % 86.15/86.41 e14)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 e12 % 86.15/86.41 e10)) % 86.15/86.41 (op2 % 86.15/86.41 (h e12) % 86.15/86.41 (h % 86.15/86.41 e10)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 e12 % 86.15/86.41 e11)) % 86.15/86.41 (op2 (h e12) % 86.15/86.41 (h e11)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 e12 % 86.15/86.41 e12)) % 86.15/86.41 (op2 (h e12) % 86.15/86.41 (h e12)))) % 86.15/86.41 (Eq % 86.15/86.41 (h % 86.15/86.41 (op1 e12 e13)) % 86.15/86.41 (op2 (h e12) % 86.15/86.41 (h e13)))) % 86.15/86.41 (Eq % 86.15/86.41 (h (op1 e12 e14)) % 86.15/86.41 (op2 (h e12) % 86.15/86.41 (h e14)))) % 86.15/86.41 (Eq (h (op1 e13 e10)) % 86.15/86.41 (op2 (h e13) % 86.15/86.41 (h e10)))) % 86.15/86.41 (Eq (h (op1 e13 e11)) % 86.15/86.41 (op2 (h e13) % 86.15/86.41 (h e11)))) % 86.15/86.41 (Eq (h (op1 e13 e12)) % 86.15/86.41 (op2 (h e13) (h e12)))) % 86.15/86.41 (Eq (h (op1 e13 e13)) % 86.15/86.41 (op2 (h e13) (h e13)))) % 86.15/86.41 (Eq (h (op1 e13 e14)) % 86.15/86.41 (op2 (h e13) (h e14)))) % 86.15/86.41 (Eq (h (op1 e14 e10)) % 86.15/86.41 (op2 (h e14) (h e10)))) % 86.15/86.41 (Eq (h (op1 e14 e11)) % 86.15/86.41 (op2 (h e14) (h e11)))) % 86.15/86.41 (Eq (h (op1 e14 e12)) % 86.15/86.41 (op2 (h e14) (h e12)))) % 86.15/86.41 (Eq (h (op1 e14 e13)) % 86.15/86.41 (op2 (h e14) (h e13)))) % 86.15/86.41 (Eq (h (op1 e14 e14)) % 86.15/86.41 (op2 (h e14) (h e14)))) % 86.15/86.41 (Eq (j (op2 e20 e20)) % 86.15/86.41 (op1 (j e20) (j e20)))) % 86.15/86.41 (Eq (j (op2 e20 e21)) % 86.15/86.41 (op1 (j e20) (j e21)))) % 86.15/86.41 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.15/86.41 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.15/86.41 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.15/86.41 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.15/86.41 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.15/86.41 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.15/86.41 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.15/86.41 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.15/86.41 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.15/86.41 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.15/86.41 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.15/86.41 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.15/86.41 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.15/86.41 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.15/86.41 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.15/86.41 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.15/86.41 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.15/86.41 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.15/86.41 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.15/86.41 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.15/86.41 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.15/86.41 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.15/86.41 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.15/86.41 (Eq (h (j e20)) e20)) % 86.15/86.41 (Eq (h (j e21)) e21)) % 86.15/86.41 (Eq (h (j e22)) e22)) % 86.15/86.41 (Eq (h (j e23)) e23)) % 86.15/86.41 (Eq (h (j e24)) e24)) % 86.15/86.41 (Eq (j (h e10)) e10)) % 86.15/86.41 (Eq (j (h e11)) e11)) % 86.15/86.41 (Eq (j (h e12)) e12)) % 86.15/86.41 (Eq (j (h e13)) e13)) % 86.15/86.41 (Eq (j (h e14)) e14)))) % 86.15/86.41 True % 86.15/86.41 Clause #6 (by clausification #[1]): Eq (Ne e23 e24) True % 86.15/86.41 Clause #7 (by clausification #[1]): Eq % 86.15/86.41 (And % 86.15/86.41 (And % 86.15/86.41 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 86.15/86.41 (Ne e21 e24)) % 86.15/86.41 (Ne e22 e23)) % 86.15/86.41 (Ne e22 e24)) % 86.15/86.41 True % 86.15/86.41 Clause #8 (by clausification #[6]): Ne e23 e24 % 86.15/86.41 Clause #10 (by clausification #[7]): Eq % 86.15/86.41 (And % 86.15/86.41 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 86.15/86.41 (Ne e21 e24)) % 86.15/86.41 (Ne e22 e23)) % 86.15/86.41 True % 86.15/86.41 Clause #13 (by clausification #[10]): Eq % 86.15/86.41 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 86.15/86.41 (Ne e21 e24)) % 86.15/86.41 True % 86.15/86.41 Clause #16 (by clausification #[13]): Eq (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) True % 86.15/86.41 Clause #19 (by clausification #[16]): Eq (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) True % 86.22/86.43 Clause #22 (by clausification #[0]): Eq % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 86.22/86.43 (Ne e11 e14)) % 86.22/86.43 (Ne e12 e13)) % 86.22/86.43 (Ne e12 e14)) % 86.22/86.43 True % 86.22/86.43 Clause #25 (by clausification #[19]): Eq (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) True % 86.22/86.43 Clause #28 (by clausification #[25]): Eq (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) True % 86.22/86.43 Clause #30 (by clausification #[28]): Eq (Ne e20 e23) True % 86.22/86.43 Clause #32 (by clausification #[30]): Ne e20 e23 % 86.22/86.43 Clause #41 (by clausification #[22]): Eq % 86.22/86.43 (And % 86.22/86.43 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 86.22/86.43 (Ne e11 e14)) % 86.22/86.43 (Ne e12 e13)) % 86.22/86.43 True % 86.22/86.43 Clause #43 (by clausification #[41]): Eq (Ne e12 e13) True % 86.22/86.43 Clause #44 (by clausification #[41]): Eq % 86.22/86.43 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 86.22/86.43 (Ne e11 e14)) % 86.22/86.43 True % 86.22/86.43 Clause #45 (by clausification #[43]): Ne e12 e13 % 86.22/86.43 Clause #47 (by clausification #[44]): Eq (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) True % 86.22/86.43 Clause #50 (by clausification #[47]): Eq (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) True % 86.22/86.43 Clause #53 (by clausification #[50]): Eq (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) True % 86.22/86.43 Clause #55 (by clausification #[3]): Eq (Eq (op1 e14 e14) e10) True % 86.22/86.43 Clause #56 (by clausification #[3]): Eq % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) % 86.22/86.43 (Eq (op1 e10 e12) e10)) % 86.22/86.43 (Eq (op1 e10 e13) e11)) % 86.22/86.43 (Eq (op1 e10 e14) e13)) % 86.22/86.43 (Eq (op1 e11 e10) e10)) % 86.22/86.43 (Eq (op1 e11 e11) e11)) % 86.22/86.43 (Eq (op1 e11 e12) e12)) % 86.22/86.43 (Eq (op1 e11 e13) e13)) % 86.22/86.43 (Eq (op1 e11 e14) e14)) % 86.22/86.43 (Eq (op1 e12 e10) e11)) % 86.22/86.43 (Eq (op1 e12 e11) e14)) % 86.22/86.43 (Eq (op1 e12 e12) e13)) % 86.22/86.43 (Eq (op1 e12 e13) e10)) % 86.22/86.43 (Eq (op1 e12 e14) e12)) % 86.22/86.43 (Eq (op1 e13 e10) e13)) % 86.22/86.43 (Eq (op1 e13 e11) e10)) % 86.22/86.43 (Eq (op1 e13 e12) e14)) % 86.22/86.43 (Eq (op1 e13 e13) e12)) % 86.22/86.43 (Eq (op1 e13 e14) e11)) % 86.22/86.43 (Eq (op1 e14 e10) e12)) % 86.22/86.43 (Eq (op1 e14 e11) e13)) % 86.22/86.43 (Eq (op1 e14 e12) e11)) % 86.22/86.43 (Eq (op1 e14 e13) e14)) % 86.22/86.43 True % 86.22/86.43 Clause #57 (by clausification #[55]): Eq (op1 e14 e14) e10 % 86.22/86.43 Clause #58 (by clausification #[53]): Eq (Ne e10 e14) True % 86.22/86.43 Clause #60 (by clausification #[58]): Ne e10 e14 % 86.22/86.43 Clause #71 (by clausification #[4]): Eq (Eq (op2 e24 e24) e24) True % 86.22/86.43 Clause #72 (by clausification #[4]): Eq % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.22/86.43 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e23)) % 86.26/86.47 (Eq (op2 e20 e22) e24)) % 86.26/86.47 (Eq (op2 e20 e23) e21)) % 86.26/86.47 (Eq (op2 e20 e24) e22)) % 86.26/86.47 (Eq (op2 e21 e20) e24)) % 86.26/86.47 (Eq (op2 e21 e21) e21)) % 86.26/86.47 (Eq (op2 e21 e22) e23)) % 86.26/86.47 (Eq (op2 e21 e23) e22)) % 86.26/86.47 (Eq (op2 e21 e24) e20)) % 86.26/86.47 (Eq (op2 e22 e20) e21)) % 86.26/86.47 (Eq (op2 e22 e21) e20)) % 86.26/86.47 (Eq (op2 e22 e22) e22)) % 86.26/86.47 (Eq (op2 e22 e23) e24)) % 86.26/86.47 (Eq (op2 e22 e24) e23)) % 86.26/86.47 (Eq (op2 e23 e20) e22)) % 86.26/86.47 (Eq (op2 e23 e21) e24)) % 86.26/86.47 (Eq (op2 e23 e22) e20)) % 86.26/86.47 (Eq (op2 e23 e23) e23)) % 86.26/86.47 (Eq (op2 e23 e24) e21)) % 86.26/86.47 (Eq (op2 e24 e20) e23)) % 86.26/86.47 (Eq (op2 e24 e21) e22)) % 86.26/86.47 (Eq (op2 e24 e22) e21)) % 86.26/86.47 (Eq (op2 e24 e23) e20)) % 86.26/86.47 True % 86.26/86.47 Clause #73 (by clausification #[71]): Eq (op2 e24 e24) e24 % 86.26/86.47 Clause #89 (by clausification #[5]): Eq % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 86.26/86.47 (Eq (h e10) e24)) % 86.26/86.47 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 86.26/86.47 (Eq (h e11) e24))) % 86.26/86.47 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 86.26/86.47 (Eq (h e12) e24))) % 86.26/86.47 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 86.26/86.47 (Eq (h e13) e24))) % 86.26/86.47 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) % 86.26/86.47 (Eq (h e14) e24))) % 86.26/86.47 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 86.26/86.47 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 86.26/86.47 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 86.26/86.47 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 86.26/86.47 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) → % 86.26/86.47 Not % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (And % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e10 % 86.26/86.47 e10)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e10) % 86.26/86.47 (h % 86.26/86.47 e10))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e10 % 86.26/86.47 e11)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e10) % 86.26/86.47 (h % 86.26/86.47 e11)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e10 % 86.26/86.47 e12)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e10) % 86.26/86.47 (h % 86.26/86.47 e12)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e10 % 86.26/86.47 e13)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e10) % 86.26/86.47 (h % 86.26/86.47 e13)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e10 % 86.26/86.47 e14)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e10) % 86.26/86.47 (h % 86.26/86.47 e14)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e11 % 86.26/86.47 e10)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e11) % 86.26/86.47 (h % 86.26/86.47 e10)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e11 % 86.26/86.47 e11)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e11) % 86.26/86.47 (h % 86.26/86.47 e11)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e11 % 86.26/86.47 e12)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e11) % 86.26/86.47 (h % 86.26/86.47 e12)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 % 86.26/86.47 e11 % 86.26/86.47 e13)) % 86.26/86.47 (op2 % 86.26/86.47 (h % 86.26/86.47 e11) % 86.26/86.47 (h % 86.26/86.47 e13)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.47 (op1 e11 % 86.26/86.47 e14)) % 86.26/86.47 (op2 % 86.26/86.47 (h e11) % 86.26/86.47 (h % 86.26/86.47 e14)))) % 86.26/86.47 (Eq % 86.26/86.47 (h % 86.26/86.48 (op1 e12 % 86.26/86.48 e10)) % 86.26/86.48 (op2 (h e12) % 86.26/86.48 (h e10)))) % 86.26/86.48 (Eq % 86.26/86.48 (h % 86.26/86.48 (op1 e12 % 86.26/86.48 e11)) % 86.26/86.48 (op2 (h e12) % 86.26/86.48 (h e11)))) % 86.26/86.48 (Eq % 86.26/86.48 (h % 86.26/86.48 (op1 e12 e12)) % 86.26/86.48 (op2 (h e12) % 86.26/86.48 (h e12)))) % 86.26/86.48 (Eq % 86.26/86.48 (h (op1 e12 e13)) % 86.26/86.48 (op2 (h e12) % 86.26/86.48 (h e13)))) % 86.26/86.48 (Eq (h (op1 e12 e14)) % 86.26/86.48 (op2 (h e12) % 86.26/86.48 (h e14)))) % 86.26/86.48 (Eq (h (op1 e13 e10)) % 86.26/86.48 (op2 (h e13) % 86.26/86.48 (h e10)))) % 86.26/86.48 (Eq (h (op1 e13 e11)) % 86.26/86.48 (op2 (h e13) (h e11)))) % 86.26/86.48 (Eq (h (op1 e13 e12)) % 86.26/86.48 (op2 (h e13) (h e12)))) % 86.26/86.48 (Eq (h (op1 e13 e13)) % 86.26/86.48 (op2 (h e13) (h e13)))) % 86.26/86.48 (Eq (h (op1 e13 e14)) % 86.26/86.48 (op2 (h e13) (h e14)))) % 86.26/86.48 (Eq (h (op1 e14 e10)) % 86.26/86.48 (op2 (h e14) (h e10)))) % 86.26/86.48 (Eq (h (op1 e14 e11)) % 86.26/86.48 (op2 (h e14) (h e11)))) % 86.26/86.48 (Eq (h (op1 e14 e12)) % 86.26/86.48 (op2 (h e14) (h e12)))) % 86.26/86.48 (Eq (h (op1 e14 e13)) % 86.26/86.48 (op2 (h e14) (h e13)))) % 86.26/86.48 (Eq (h (op1 e14 e14)) % 86.26/86.48 (op2 (h e14) (h e14)))) % 86.26/86.48 (Eq (j (op2 e20 e20)) % 86.26/86.48 (op1 (j e20) (j e20)))) % 86.26/86.48 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.26/86.48 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.26/86.48 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.26/86.48 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.26/86.48 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.26/86.48 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.26/86.48 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.26/86.48 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.26/86.48 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.26/86.48 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.26/86.48 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.26/86.48 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.26/86.48 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.26/86.48 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.26/86.48 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.26/86.48 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.26/86.48 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.26/86.48 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.26/86.48 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.26/86.48 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.26/86.48 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.26/86.48 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.26/86.48 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.26/86.48 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.26/86.48 (Eq (h (j e20)) e20)) % 86.26/86.48 (Eq (h (j e21)) e21)) % 86.26/86.48 (Eq (h (j e22)) e22)) % 86.26/86.48 (Eq (h (j e23)) e23)) % 86.26/86.48 (Eq (h (j e24)) e24)) % 86.26/86.48 (Eq (j (h e10)) e10)) % 86.26/86.48 (Eq (j (h e11)) e11)) % 86.26/86.48 (Eq (j (h e12)) e12)) % 86.26/86.48 (Eq (j (h e13)) e13)) % 86.26/86.48 (Eq (j (h e14)) e14))) % 86.26/86.48 False % 86.26/86.48 Clause #90 (by clausification #[89]): Eq % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (And % 86.26/86.48 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 86.26/86.48 (Eq (h e10) e24)) % 86.26/86.48 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 86.26/86.48 (Eq (h e11) e24))) % 86.26/86.48 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 86.26/86.48 (Eq (h e12) e24))) % 86.26/86.48 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 86.26/86.48 (Eq (h e13) e24))) % 86.26/86.48 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) (Eq (h e14) e24))) % 86.26/86.48 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 86.26/86.48 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 86.26/86.48 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 86.26/86.48 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 86.26/86.48 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14))) % 86.26/86.51 True % 86.26/86.51 Clause #91 (by clausification #[89]): Eq % 86.26/86.51 (Not % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (And % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e10 % 86.26/86.51 e10)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e10) % 86.26/86.51 (h % 86.26/86.51 e10))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e10 % 86.26/86.51 e11)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e10) % 86.26/86.51 (h % 86.26/86.51 e11)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e10 % 86.26/86.51 e12)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e10) % 86.26/86.51 (h % 86.26/86.51 e12)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e10 % 86.26/86.51 e13)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e10) % 86.26/86.51 (h % 86.26/86.51 e13)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e10 % 86.26/86.51 e14)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e10) % 86.26/86.51 (h % 86.26/86.51 e14)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e11 % 86.26/86.51 e10)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e11) % 86.26/86.51 (h % 86.26/86.51 e10)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e11 % 86.26/86.51 e11)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e11) % 86.26/86.51 (h % 86.26/86.51 e11)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 % 86.26/86.51 e11 % 86.26/86.51 e12)) % 86.26/86.51 (op2 % 86.26/86.51 (h % 86.26/86.51 e11) % 86.26/86.51 (h % 86.26/86.51 e12)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 e11 % 86.26/86.51 e13)) % 86.26/86.51 (op2 % 86.26/86.51 (h e11) % 86.26/86.51 (h % 86.26/86.51 e13)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 e11 % 86.26/86.51 e14)) % 86.26/86.51 (op2 (h e11) % 86.26/86.51 (h e14)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 e12 % 86.26/86.51 e10)) % 86.26/86.51 (op2 (h e12) % 86.26/86.51 (h e10)))) % 86.26/86.51 (Eq % 86.26/86.51 (h % 86.26/86.51 (op1 e12 e11)) % 86.26/86.51 (op2 (h e12) % 86.26/86.51 (h e11)))) % 86.26/86.51 (Eq % 86.26/86.51 (h (op1 e12 e12)) % 86.26/86.51 (op2 (h e12) % 86.26/86.51 (h e12)))) % 86.26/86.51 (Eq (h (op1 e12 e13)) % 86.26/86.51 (op2 (h e12) % 86.26/86.51 (h e13)))) % 86.26/86.51 (Eq (h (op1 e12 e14)) % 86.26/86.51 (op2 (h e12) % 86.26/86.51 (h e14)))) % 86.26/86.51 (Eq (h (op1 e13 e10)) % 86.26/86.51 (op2 (h e13) (h e10)))) % 86.26/86.51 (Eq (h (op1 e13 e11)) % 86.26/86.51 (op2 (h e13) (h e11)))) % 86.26/86.51 (Eq (h (op1 e13 e12)) % 86.26/86.51 (op2 (h e13) (h e12)))) % 86.26/86.51 (Eq (h (op1 e13 e13)) % 86.26/86.51 (op2 (h e13) (h e13)))) % 86.26/86.51 (Eq (h (op1 e13 e14)) % 86.26/86.51 (op2 (h e13) (h e14)))) % 86.26/86.51 (Eq (h (op1 e14 e10)) % 86.26/86.51 (op2 (h e14) (h e10)))) % 86.26/86.51 (Eq (h (op1 e14 e11)) % 86.26/86.51 (op2 (h e14) (h e11)))) % 86.26/86.51 (Eq (h (op1 e14 e12)) % 86.26/86.51 (op2 (h e14) (h e12)))) % 86.26/86.51 (Eq (h (op1 e14 e13)) % 86.26/86.51 (op2 (h e14) (h e13)))) % 86.26/86.51 (Eq (h (op1 e14 e14)) % 86.26/86.51 (op2 (h e14) (h e14)))) % 86.26/86.51 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.26/86.51 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.26/86.52 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.26/86.52 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.26/86.52 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.26/86.52 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.26/86.52 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.26/86.52 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.26/86.52 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.26/86.52 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.26/86.52 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.26/86.52 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.26/86.52 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.26/86.52 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.26/86.52 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.26/86.52 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.26/86.52 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.26/86.52 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.26/86.52 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.26/86.52 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.26/86.52 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.26/86.52 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.26/86.52 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.26/86.52 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.26/86.52 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.26/86.52 (Eq (h (j e20)) e20)) % 86.26/86.52 (Eq (h (j e21)) e21)) % 86.26/86.52 (Eq (h (j e22)) e22)) % 86.26/86.52 (Eq (h (j e23)) e23)) % 86.26/86.52 (Eq (h (j e24)) e24)) % 86.26/86.52 (Eq (j (h e10)) e10)) % 86.26/86.52 (Eq (j (h e11)) e11)) % 86.26/86.52 (Eq (j (h e12)) e12)) % 86.26/86.52 (Eq (j (h e13)) e13)) % 86.26/86.52 (Eq (j (h e14)) e14))) % 86.26/86.52 False % 86.26/86.52 Clause #92 (by clausification #[90]): Eq (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) True % 86.26/86.52 Clause #93 (by clausification #[90]): Eq % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (And % 86.26/86.52 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 86.26/86.52 (Eq (h e10) e24)) % 86.26/86.52 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 86.26/86.52 (Eq (h e11) e24))) % 86.26/86.52 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 86.26/86.52 (Eq (h e12) e24))) % 86.26/86.52 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) (Eq (h e13) e24))) % 86.26/86.52 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) (Eq (h e14) e24))) % 86.26/86.52 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 86.26/86.52 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 86.26/86.52 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 86.26/86.52 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 86.26/86.52 True % 86.26/86.52 Clause #94 (by clausification #[92]): Or (Eq (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) True) % 86.34/86.57 (Eq (Eq (j e24) e14) True) % 86.34/86.57 Clause #95 (by clausification #[94]): Or (Eq (Eq (j e24) e14) True) % 86.34/86.57 (Or (Eq (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) True) (Eq (Eq (j e24) e13) True)) % 86.34/86.57 Clause #96 (by clausification #[95]): Or (Eq (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) True) % 86.34/86.57 (Or (Eq (Eq (j e24) e13) True) (Eq (j e24) e14)) % 86.34/86.57 Clause #97 (by clausification #[96]): Or (Eq (Eq (j e24) e13) True) % 86.34/86.57 (Or (Eq (j e24) e14) (Or (Eq (Or (Eq (j e24) e10) (Eq (j e24) e11)) True) (Eq (Eq (j e24) e12) True))) % 86.34/86.57 Clause #98 (by clausification #[97]): Or (Eq (j e24) e14) % 86.34/86.57 (Or (Eq (Or (Eq (j e24) e10) (Eq (j e24) e11)) True) (Or (Eq (Eq (j e24) e12) True) (Eq (j e24) e13))) % 86.34/86.57 Clause #99 (by clausification #[98]): Or (Eq (j e24) e14) % 86.34/86.57 (Or (Eq (Eq (j e24) e12) True) (Or (Eq (j e24) e13) (Or (Eq (Eq (j e24) e10) True) (Eq (Eq (j e24) e11) True)))) % 86.34/86.57 Clause #100 (by clausification #[99]): Or (Eq (j e24) e14) % 86.34/86.57 (Or (Eq (j e24) e13) (Or (Eq (Eq (j e24) e10) True) (Or (Eq (Eq (j e24) e11) True) (Eq (j e24) e12)))) % 86.34/86.57 Clause #101 (by clausification #[100]): Or (Eq (j e24) e14) (Or (Eq (j e24) e13) (Or (Eq (Eq (j e24) e11) True) (Or (Eq (j e24) e12) (Eq (j e24) e10)))) % 86.34/86.57 Clause #102 (by clausification #[101]): Or (Eq (j e24) e14) (Or (Eq (j e24) e13) (Or (Eq (j e24) e12) (Or (Eq (j e24) e10) (Eq (j e24) e11)))) % 86.34/86.57 Clause #111 (by clausification #[56]): Eq % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) % 86.34/86.57 (Eq (op1 e10 e12) e10)) % 86.34/86.57 (Eq (op1 e10 e13) e11)) % 86.34/86.57 (Eq (op1 e10 e14) e13)) % 86.34/86.57 (Eq (op1 e11 e10) e10)) % 86.34/86.57 (Eq (op1 e11 e11) e11)) % 86.34/86.57 (Eq (op1 e11 e12) e12)) % 86.34/86.57 (Eq (op1 e11 e13) e13)) % 86.34/86.57 (Eq (op1 e11 e14) e14)) % 86.34/86.57 (Eq (op1 e12 e10) e11)) % 86.34/86.57 (Eq (op1 e12 e11) e14)) % 86.34/86.57 (Eq (op1 e12 e12) e13)) % 86.34/86.57 (Eq (op1 e12 e13) e10)) % 86.34/86.57 (Eq (op1 e12 e14) e12)) % 86.34/86.57 (Eq (op1 e13 e10) e13)) % 86.34/86.57 (Eq (op1 e13 e11) e10)) % 86.34/86.57 (Eq (op1 e13 e12) e14)) % 86.34/86.57 (Eq (op1 e13 e13) e12)) % 86.34/86.57 (Eq (op1 e13 e14) e11)) % 86.34/86.57 (Eq (op1 e14 e10) e12)) % 86.34/86.57 (Eq (op1 e14 e11) e13)) % 86.34/86.57 (Eq (op1 e14 e12) e11)) % 86.34/86.57 True % 86.34/86.57 Clause #128 (by clausification #[72]): Eq (Eq (op2 e24 e23) e20) True % 86.34/86.57 Clause #130 (by clausification #[128]): Eq (op2 e24 e23) e20 % 86.34/86.57 Clause #146 (by clausification #[91]): Eq % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (And % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e10 % 86.34/86.57 e10)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e10) % 86.34/86.57 (h % 86.34/86.57 e10))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e10 % 86.34/86.57 e11)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e10) % 86.34/86.57 (h % 86.34/86.57 e11)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e10 % 86.34/86.57 e12)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e10) % 86.34/86.57 (h % 86.34/86.57 e12)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e10 % 86.34/86.57 e13)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e10) % 86.34/86.57 (h % 86.34/86.57 e13)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e10 % 86.34/86.57 e14)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e10) % 86.34/86.57 (h % 86.34/86.57 e14)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e11 % 86.34/86.57 e10)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e11) % 86.34/86.57 (h % 86.34/86.57 e10)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 % 86.34/86.57 e11 % 86.34/86.57 e11)) % 86.34/86.57 (op2 % 86.34/86.57 (h % 86.34/86.57 e11) % 86.34/86.57 (h % 86.34/86.57 e11)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 e11 % 86.34/86.57 e12)) % 86.34/86.57 (op2 % 86.34/86.57 (h e11) % 86.34/86.57 (h % 86.34/86.57 e12)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 e11 % 86.34/86.57 e13)) % 86.34/86.57 (op2 (h e11) % 86.34/86.57 (h e13)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 e11 % 86.34/86.57 e14)) % 86.34/86.57 (op2 (h e11) % 86.34/86.57 (h e14)))) % 86.34/86.57 (Eq % 86.34/86.57 (h % 86.34/86.57 (op1 e12 e10)) % 86.34/86.57 (op2 (h e12) % 86.34/86.57 (h e10)))) % 86.34/86.57 (Eq % 86.34/86.57 (h (op1 e12 e11)) % 86.34/86.57 (op2 (h e12) % 86.34/86.57 (h e11)))) % 86.34/86.57 (Eq (h (op1 e12 e12)) % 86.34/86.57 (op2 (h e12) % 86.34/86.57 (h e12)))) % 86.34/86.57 (Eq (h (op1 e12 e13)) % 86.34/86.57 (op2 (h e12) % 86.34/86.57 (h e13)))) % 86.34/86.57 (Eq (h (op1 e12 e14)) % 86.34/86.57 (op2 (h e12) (h e14)))) % 86.34/86.57 (Eq (h (op1 e13 e10)) % 86.34/86.57 (op2 (h e13) (h e10)))) % 86.34/86.57 (Eq (h (op1 e13 e11)) % 86.34/86.57 (op2 (h e13) (h e11)))) % 86.34/86.57 (Eq (h (op1 e13 e12)) % 86.34/86.57 (op2 (h e13) (h e12)))) % 86.34/86.57 (Eq (h (op1 e13 e13)) % 86.34/86.57 (op2 (h e13) (h e13)))) % 86.34/86.57 (Eq (h (op1 e13 e14)) % 86.34/86.57 (op2 (h e13) (h e14)))) % 86.34/86.57 (Eq (h (op1 e14 e10)) % 86.34/86.57 (op2 (h e14) (h e10)))) % 86.34/86.57 (Eq (h (op1 e14 e11)) % 86.34/86.57 (op2 (h e14) (h e11)))) % 86.34/86.57 (Eq (h (op1 e14 e12)) % 86.34/86.57 (op2 (h e14) (h e12)))) % 86.34/86.57 (Eq (h (op1 e14 e13)) % 86.34/86.57 (op2 (h e14) (h e13)))) % 86.34/86.57 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.34/86.57 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.34/86.57 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.34/86.57 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.34/86.57 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.34/86.57 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.34/86.57 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.34/86.57 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.34/86.57 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.34/86.57 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.34/86.57 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.34/86.57 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.34/86.57 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.34/86.57 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.34/86.57 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.34/86.57 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.34/86.57 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.34/86.57 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.34/86.57 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.34/86.57 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.34/86.57 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.34/86.57 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.34/86.57 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.34/86.57 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.34/86.57 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.34/86.57 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.34/86.57 (Eq (h (j e20)) e20)) % 86.34/86.57 (Eq (h (j e21)) e21)) % 86.37/86.60 (Eq (h (j e22)) e22)) % 86.37/86.60 (Eq (h (j e23)) e23)) % 86.37/86.60 (Eq (h (j e24)) e24)) % 86.37/86.60 (Eq (j (h e10)) e10)) % 86.37/86.60 (Eq (j (h e11)) e11)) % 86.37/86.60 (Eq (j (h e12)) e12)) % 86.37/86.60 (Eq (j (h e13)) e13)) % 86.37/86.60 (Eq (j (h e14)) e14)) % 86.37/86.60 True % 86.37/86.60 Clause #147 (by clausification #[146]): Eq (Eq (j (h e14)) e14) True % 86.37/86.60 Clause #148 (by clausification #[146]): Eq % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (And % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 % 86.37/86.60 e10 % 86.37/86.60 e10)) % 86.37/86.60 (op2 % 86.37/86.60 (h % 86.37/86.60 e10) % 86.37/86.60 (h % 86.37/86.60 e10))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 % 86.37/86.60 e10 % 86.37/86.60 e11)) % 86.37/86.60 (op2 % 86.37/86.60 (h % 86.37/86.60 e10) % 86.37/86.60 (h % 86.37/86.60 e11)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 % 86.37/86.60 e10 % 86.37/86.60 e12)) % 86.37/86.60 (op2 % 86.37/86.60 (h % 86.37/86.60 e10) % 86.37/86.60 (h % 86.37/86.60 e12)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 % 86.37/86.60 e10 % 86.37/86.60 e13)) % 86.37/86.60 (op2 % 86.37/86.60 (h % 86.37/86.60 e10) % 86.37/86.60 (h % 86.37/86.60 e13)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 % 86.37/86.60 e10 % 86.37/86.60 e14)) % 86.37/86.60 (op2 % 86.37/86.60 (h % 86.37/86.60 e10) % 86.37/86.60 (h % 86.37/86.60 e14)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 % 86.37/86.60 e11 % 86.37/86.60 e10)) % 86.37/86.60 (op2 % 86.37/86.60 (h % 86.37/86.60 e11) % 86.37/86.60 (h % 86.37/86.60 e10)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 e11 % 86.37/86.60 e11)) % 86.37/86.60 (op2 % 86.37/86.60 (h e11) % 86.37/86.60 (h % 86.37/86.60 e11)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 e11 % 86.37/86.60 e12)) % 86.37/86.60 (op2 (h e11) % 86.37/86.60 (h e12)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 e11 % 86.37/86.60 e13)) % 86.37/86.60 (op2 (h e11) % 86.37/86.60 (h e13)))) % 86.37/86.60 (Eq % 86.37/86.60 (h % 86.37/86.60 (op1 e11 e14)) % 86.37/86.60 (op2 (h e11) % 86.37/86.60 (h e14)))) % 86.37/86.60 (Eq % 86.37/86.60 (h (op1 e12 e10)) % 86.37/86.60 (op2 (h e12) % 86.37/86.60 (h e10)))) % 86.37/86.60 (Eq (h (op1 e12 e11)) % 86.37/86.60 (op2 (h e12) % 86.37/86.60 (h e11)))) % 86.37/86.60 (Eq (h (op1 e12 e12)) % 86.37/86.60 (op2 (h e12) % 86.37/86.60 (h e12)))) % 86.37/86.60 (Eq (h (op1 e12 e13)) % 86.37/86.60 (op2 (h e12) (h e13)))) % 86.37/86.60 (Eq (h (op1 e12 e14)) % 86.37/86.60 (op2 (h e12) (h e14)))) % 86.37/86.60 (Eq (h (op1 e13 e10)) % 86.37/86.60 (op2 (h e13) (h e10)))) % 86.37/86.60 (Eq (h (op1 e13 e11)) % 86.37/86.60 (op2 (h e13) (h e11)))) % 86.37/86.60 (Eq (h (op1 e13 e12)) % 86.37/86.60 (op2 (h e13) (h e12)))) % 86.37/86.60 (Eq (h (op1 e13 e13)) % 86.37/86.60 (op2 (h e13) (h e13)))) % 86.37/86.60 (Eq (h (op1 e13 e14)) % 86.37/86.60 (op2 (h e13) (h e14)))) % 86.37/86.60 (Eq (h (op1 e14 e10)) % 86.37/86.60 (op2 (h e14) (h e10)))) % 86.37/86.60 (Eq (h (op1 e14 e11)) % 86.37/86.60 (op2 (h e14) (h e11)))) % 86.37/86.60 (Eq (h (op1 e14 e12)) % 86.37/86.60 (op2 (h e14) (h e12)))) % 86.37/86.60 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.37/86.60 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.37/86.60 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.37/86.60 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.37/86.60 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.37/86.60 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.37/86.60 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.37/86.60 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.37/86.60 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.37/86.60 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.37/86.60 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.37/86.60 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.37/86.60 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.37/86.60 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.37/86.60 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.37/86.60 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.37/86.60 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.37/86.60 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.37/86.60 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.37/86.60 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.37/86.60 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.37/86.60 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.37/86.60 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.37/86.60 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.37/86.60 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.37/86.60 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.37/86.60 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.37/86.60 (Eq (h (j e20)) e20)) % 86.37/86.60 (Eq (h (j e21)) e21)) % 86.37/86.60 (Eq (h (j e22)) e22)) % 86.37/86.60 (Eq (h (j e23)) e23)) % 86.37/86.60 (Eq (h (j e24)) e24)) % 86.37/86.60 (Eq (j (h e10)) e10)) % 86.37/86.62 (Eq (j (h e11)) e11)) % 86.37/86.62 (Eq (j (h e12)) e12)) % 86.37/86.62 (Eq (j (h e13)) e13)) % 86.37/86.62 True % 86.37/86.62 Clause #149 (by clausification #[147]): Eq (j (h e14)) e14 % 86.37/86.62 Clause #165 (by clausification #[93]): Eq (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14)) True % 86.37/86.62 Clause #167 (by clausification #[165]): Or (Eq (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) True) % 86.37/86.62 (Eq (Eq (j e23) e14) True) % 86.37/86.62 Clause #168 (by clausification #[167]): Or (Eq (Eq (j e23) e14) True) % 86.37/86.62 (Or (Eq (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) True) (Eq (Eq (j e23) e13) True)) % 86.37/86.62 Clause #169 (by clausification #[168]): Or (Eq (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) True) % 86.37/86.62 (Or (Eq (Eq (j e23) e13) True) (Eq (j e23) e14)) % 86.37/86.62 Clause #170 (by clausification #[169]): Or (Eq (Eq (j e23) e13) True) % 86.37/86.62 (Or (Eq (j e23) e14) (Or (Eq (Or (Eq (j e23) e10) (Eq (j e23) e11)) True) (Eq (Eq (j e23) e12) True))) % 86.37/86.62 Clause #171 (by clausification #[170]): Or (Eq (j e23) e14) % 86.37/86.62 (Or (Eq (Or (Eq (j e23) e10) (Eq (j e23) e11)) True) (Or (Eq (Eq (j e23) e12) True) (Eq (j e23) e13))) % 86.37/86.62 Clause #172 (by clausification #[171]): Or (Eq (j e23) e14) % 86.37/86.62 (Or (Eq (Eq (j e23) e12) True) (Or (Eq (j e23) e13) (Or (Eq (Eq (j e23) e10) True) (Eq (Eq (j e23) e11) True)))) % 86.37/86.62 Clause #173 (by clausification #[172]): Or (Eq (j e23) e14) % 86.37/86.62 (Or (Eq (j e23) e13) (Or (Eq (Eq (j e23) e10) True) (Or (Eq (Eq (j e23) e11) True) (Eq (j e23) e12)))) % 86.37/86.62 Clause #174 (by clausification #[173]): Or (Eq (j e23) e14) (Or (Eq (j e23) e13) (Or (Eq (Eq (j e23) e11) True) (Or (Eq (j e23) e12) (Eq (j e23) e10)))) % 86.37/86.62 Clause #175 (by clausification #[174]): Or (Eq (j e23) e14) (Or (Eq (j e23) e13) (Or (Eq (j e23) e12) (Or (Eq (j e23) e10) (Eq (j e23) e11)))) % 86.37/86.62 Clause #185 (by clausification #[111]): Eq % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.37/86.62 (Eq (op1 e10 e13) e11)) % 86.37/86.62 (Eq (op1 e10 e14) e13)) % 86.37/86.62 (Eq (op1 e11 e10) e10)) % 86.37/86.62 (Eq (op1 e11 e11) e11)) % 86.37/86.62 (Eq (op1 e11 e12) e12)) % 86.37/86.62 (Eq (op1 e11 e13) e13)) % 86.37/86.62 (Eq (op1 e11 e14) e14)) % 86.37/86.62 (Eq (op1 e12 e10) e11)) % 86.37/86.62 (Eq (op1 e12 e11) e14)) % 86.37/86.62 (Eq (op1 e12 e12) e13)) % 86.37/86.62 (Eq (op1 e12 e13) e10)) % 86.37/86.62 (Eq (op1 e12 e14) e12)) % 86.37/86.62 (Eq (op1 e13 e10) e13)) % 86.37/86.62 (Eq (op1 e13 e11) e10)) % 86.37/86.62 (Eq (op1 e13 e12) e14)) % 86.37/86.62 (Eq (op1 e13 e13) e12)) % 86.37/86.62 (Eq (op1 e13 e14) e11)) % 86.37/86.62 (Eq (op1 e14 e10) e12)) % 86.37/86.62 (Eq (op1 e14 e11) e13)) % 86.37/86.62 True % 86.37/86.62 Clause #188 (by clausification #[185]): Eq % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And % 86.37/86.62 (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.37/86.62 (Eq (op1 e10 e13) e11)) % 86.37/86.62 (Eq (op1 e10 e14) e13)) % 86.37/86.62 (Eq (op1 e11 e10) e10)) % 86.37/86.62 (Eq (op1 e11 e11) e11)) % 86.43/86.64 (Eq (op1 e11 e12) e12)) % 86.43/86.64 (Eq (op1 e11 e13) e13)) % 86.43/86.64 (Eq (op1 e11 e14) e14)) % 86.43/86.64 (Eq (op1 e12 e10) e11)) % 86.43/86.64 (Eq (op1 e12 e11) e14)) % 86.43/86.64 (Eq (op1 e12 e12) e13)) % 86.43/86.64 (Eq (op1 e12 e13) e10)) % 86.43/86.64 (Eq (op1 e12 e14) e12)) % 86.43/86.64 (Eq (op1 e13 e10) e13)) % 86.43/86.64 (Eq (op1 e13 e11) e10)) % 86.43/86.64 (Eq (op1 e13 e12) e14)) % 86.43/86.64 (Eq (op1 e13 e13) e12)) % 86.43/86.64 (Eq (op1 e13 e14) e11)) % 86.43/86.64 (Eq (op1 e14 e10) e12)) % 86.43/86.64 True % 86.43/86.64 Clause #191 (by clausification #[188]): Eq % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.43/86.64 (Eq (op1 e10 e13) e11)) % 86.43/86.64 (Eq (op1 e10 e14) e13)) % 86.43/86.64 (Eq (op1 e11 e10) e10)) % 86.43/86.64 (Eq (op1 e11 e11) e11)) % 86.43/86.64 (Eq (op1 e11 e12) e12)) % 86.43/86.64 (Eq (op1 e11 e13) e13)) % 86.43/86.64 (Eq (op1 e11 e14) e14)) % 86.43/86.64 (Eq (op1 e12 e10) e11)) % 86.43/86.64 (Eq (op1 e12 e11) e14)) % 86.43/86.64 (Eq (op1 e12 e12) e13)) % 86.43/86.64 (Eq (op1 e12 e13) e10)) % 86.43/86.64 (Eq (op1 e12 e14) e12)) % 86.43/86.64 (Eq (op1 e13 e10) e13)) % 86.43/86.64 (Eq (op1 e13 e11) e10)) % 86.43/86.64 (Eq (op1 e13 e12) e14)) % 86.43/86.64 (Eq (op1 e13 e13) e12)) % 86.43/86.64 (Eq (op1 e13 e14) e11)) % 86.43/86.64 True % 86.43/86.64 Clause #194 (by clausification #[191]): Eq % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.43/86.64 (Eq (op1 e10 e13) e11)) % 86.43/86.64 (Eq (op1 e10 e14) e13)) % 86.43/86.64 (Eq (op1 e11 e10) e10)) % 86.43/86.64 (Eq (op1 e11 e11) e11)) % 86.43/86.64 (Eq (op1 e11 e12) e12)) % 86.43/86.64 (Eq (op1 e11 e13) e13)) % 86.43/86.64 (Eq (op1 e11 e14) e14)) % 86.43/86.64 (Eq (op1 e12 e10) e11)) % 86.43/86.64 (Eq (op1 e12 e11) e14)) % 86.43/86.64 (Eq (op1 e12 e12) e13)) % 86.43/86.64 (Eq (op1 e12 e13) e10)) % 86.43/86.64 (Eq (op1 e12 e14) e12)) % 86.43/86.64 (Eq (op1 e13 e10) e13)) % 86.43/86.64 (Eq (op1 e13 e11) e10)) % 86.43/86.64 (Eq (op1 e13 e12) e14)) % 86.43/86.64 (Eq (op1 e13 e13) e12)) % 86.43/86.64 True % 86.43/86.64 Clause #196 (by clausification #[194]): Eq (Eq (op1 e13 e13) e12) True % 86.43/86.64 Clause #197 (by clausification #[194]): Eq % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And % 86.43/86.64 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.43/86.64 (Eq (op1 e10 e13) e11)) % 86.43/86.64 (Eq (op1 e10 e14) e13)) % 86.43/86.64 (Eq (op1 e11 e10) e10)) % 86.43/86.64 (Eq (op1 e11 e11) e11)) % 86.43/86.64 (Eq (op1 e11 e12) e12)) % 86.43/86.64 (Eq (op1 e11 e13) e13)) % 86.43/86.64 (Eq (op1 e11 e14) e14)) % 86.43/86.64 (Eq (op1 e12 e10) e11)) % 86.43/86.64 (Eq (op1 e12 e11) e14)) % 86.43/86.64 (Eq (op1 e12 e12) e13)) % 86.43/86.64 (Eq (op1 e12 e13) e10)) % 86.43/86.64 (Eq (op1 e12 e14) e12)) % 86.45/86.66 (Eq (op1 e13 e10) e13)) % 86.45/86.66 (Eq (op1 e13 e11) e10)) % 86.45/86.66 (Eq (op1 e13 e12) e14)) % 86.45/86.66 True % 86.45/86.66 Clause #198 (by clausification #[196]): Eq (op1 e13 e13) e12 % 86.45/86.66 Clause #203 (by clausification #[197]): Eq % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.66 (Eq (op1 e10 e13) e11)) % 86.45/86.66 (Eq (op1 e10 e14) e13)) % 86.45/86.66 (Eq (op1 e11 e10) e10)) % 86.45/86.66 (Eq (op1 e11 e11) e11)) % 86.45/86.66 (Eq (op1 e11 e12) e12)) % 86.45/86.66 (Eq (op1 e11 e13) e13)) % 86.45/86.66 (Eq (op1 e11 e14) e14)) % 86.45/86.66 (Eq (op1 e12 e10) e11)) % 86.45/86.66 (Eq (op1 e12 e11) e14)) % 86.45/86.66 (Eq (op1 e12 e12) e13)) % 86.45/86.66 (Eq (op1 e12 e13) e10)) % 86.45/86.66 (Eq (op1 e12 e14) e12)) % 86.45/86.66 (Eq (op1 e13 e10) e13)) % 86.45/86.66 (Eq (op1 e13 e11) e10)) % 86.45/86.66 True % 86.45/86.66 Clause #206 (by clausification #[203]): Eq % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.66 (Eq (op1 e10 e13) e11)) % 86.45/86.66 (Eq (op1 e10 e14) e13)) % 86.45/86.66 (Eq (op1 e11 e10) e10)) % 86.45/86.66 (Eq (op1 e11 e11) e11)) % 86.45/86.66 (Eq (op1 e11 e12) e12)) % 86.45/86.66 (Eq (op1 e11 e13) e13)) % 86.45/86.66 (Eq (op1 e11 e14) e14)) % 86.45/86.66 (Eq (op1 e12 e10) e11)) % 86.45/86.66 (Eq (op1 e12 e11) e14)) % 86.45/86.66 (Eq (op1 e12 e12) e13)) % 86.45/86.66 (Eq (op1 e12 e13) e10)) % 86.45/86.66 (Eq (op1 e12 e14) e12)) % 86.45/86.66 (Eq (op1 e13 e10) e13)) % 86.45/86.66 True % 86.45/86.66 Clause #209 (by clausification #[206]): Eq % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.66 (Eq (op1 e10 e13) e11)) % 86.45/86.66 (Eq (op1 e10 e14) e13)) % 86.45/86.66 (Eq (op1 e11 e10) e10)) % 86.45/86.66 (Eq (op1 e11 e11) e11)) % 86.45/86.66 (Eq (op1 e11 e12) e12)) % 86.45/86.66 (Eq (op1 e11 e13) e13)) % 86.45/86.66 (Eq (op1 e11 e14) e14)) % 86.45/86.66 (Eq (op1 e12 e10) e11)) % 86.45/86.66 (Eq (op1 e12 e11) e14)) % 86.45/86.66 (Eq (op1 e12 e12) e13)) % 86.45/86.66 (Eq (op1 e12 e13) e10)) % 86.45/86.66 (Eq (op1 e12 e14) e12)) % 86.45/86.66 True % 86.45/86.66 Clause #212 (by clausification #[209]): Eq % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.66 (Eq (op1 e10 e13) e11)) % 86.45/86.66 (Eq (op1 e10 e14) e13)) % 86.45/86.66 (Eq (op1 e11 e10) e10)) % 86.45/86.66 (Eq (op1 e11 e11) e11)) % 86.45/86.66 (Eq (op1 e11 e12) e12)) % 86.45/86.66 (Eq (op1 e11 e13) e13)) % 86.45/86.66 (Eq (op1 e11 e14) e14)) % 86.45/86.66 (Eq (op1 e12 e10) e11)) % 86.45/86.66 (Eq (op1 e12 e11) e14)) % 86.45/86.66 (Eq (op1 e12 e12) e13)) % 86.45/86.66 (Eq (op1 e12 e13) e10)) % 86.45/86.66 True % 86.45/86.66 Clause #215 (by clausification #[212]): Eq % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And % 86.45/86.66 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.66 (Eq (op1 e10 e13) e11)) % 86.45/86.66 (Eq (op1 e10 e14) e13)) % 86.45/86.66 (Eq (op1 e11 e10) e10)) % 86.45/86.66 (Eq (op1 e11 e11) e11)) % 86.45/86.66 (Eq (op1 e11 e12) e12)) % 86.45/86.68 (Eq (op1 e11 e13) e13)) % 86.45/86.68 (Eq (op1 e11 e14) e14)) % 86.45/86.68 (Eq (op1 e12 e10) e11)) % 86.45/86.68 (Eq (op1 e12 e11) e14)) % 86.45/86.68 (Eq (op1 e12 e12) e13)) % 86.45/86.68 True % 86.45/86.68 Clause #217 (by clausification #[148]): Eq (Eq (j (h e13)) e13) True % 86.45/86.68 Clause #218 (by clausification #[148]): Eq % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (And % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 % 86.45/86.68 e10 % 86.45/86.68 e10)) % 86.45/86.68 (op2 % 86.45/86.68 (h % 86.45/86.68 e10) % 86.45/86.68 (h % 86.45/86.68 e10))) % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 % 86.45/86.68 e10 % 86.45/86.68 e11)) % 86.45/86.68 (op2 % 86.45/86.68 (h % 86.45/86.68 e10) % 86.45/86.68 (h % 86.45/86.68 e11)))) % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 % 86.45/86.68 e10 % 86.45/86.68 e12)) % 86.45/86.68 (op2 % 86.45/86.68 (h % 86.45/86.68 e10) % 86.45/86.68 (h % 86.45/86.68 e12)))) % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 % 86.45/86.68 e10 % 86.45/86.68 e13)) % 86.45/86.68 (op2 % 86.45/86.68 (h % 86.45/86.68 e10) % 86.45/86.68 (h % 86.45/86.68 e13)))) % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 % 86.45/86.68 e10 % 86.45/86.68 e14)) % 86.45/86.68 (op2 % 86.45/86.68 (h % 86.45/86.68 e10) % 86.45/86.68 (h % 86.45/86.68 e14)))) % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 e11 % 86.45/86.68 e10)) % 86.45/86.68 (op2 % 86.45/86.68 (h e11) % 86.45/86.68 (h % 86.45/86.68 e10)))) % 86.45/86.68 (Eq % 86.45/86.68 (h % 86.45/86.68 (op1 e11 % 86.45/86.69 e11)) % 86.45/86.69 (op2 (h e11) % 86.45/86.69 (h e11)))) % 86.45/86.69 (Eq % 86.45/86.69 (h % 86.45/86.69 (op1 e11 % 86.45/86.69 e12)) % 86.45/86.69 (op2 (h e11) % 86.45/86.69 (h e12)))) % 86.45/86.69 (Eq % 86.45/86.69 (h % 86.45/86.69 (op1 e11 e13)) % 86.45/86.69 (op2 (h e11) % 86.45/86.69 (h e13)))) % 86.45/86.69 (Eq % 86.45/86.69 (h (op1 e11 e14)) % 86.45/86.69 (op2 (h e11) % 86.45/86.69 (h e14)))) % 86.45/86.69 (Eq (h (op1 e12 e10)) % 86.45/86.69 (op2 (h e12) % 86.45/86.69 (h e10)))) % 86.45/86.69 (Eq (h (op1 e12 e11)) % 86.45/86.69 (op2 (h e12) % 86.45/86.69 (h e11)))) % 86.45/86.69 (Eq (h (op1 e12 e12)) % 86.45/86.69 (op2 (h e12) (h e12)))) % 86.45/86.69 (Eq (h (op1 e12 e13)) % 86.45/86.69 (op2 (h e12) (h e13)))) % 86.45/86.69 (Eq (h (op1 e12 e14)) % 86.45/86.69 (op2 (h e12) (h e14)))) % 86.45/86.69 (Eq (h (op1 e13 e10)) % 86.45/86.69 (op2 (h e13) (h e10)))) % 86.45/86.69 (Eq (h (op1 e13 e11)) % 86.45/86.69 (op2 (h e13) (h e11)))) % 86.45/86.69 (Eq (h (op1 e13 e12)) % 86.45/86.69 (op2 (h e13) (h e12)))) % 86.45/86.69 (Eq (h (op1 e13 e13)) % 86.45/86.69 (op2 (h e13) (h e13)))) % 86.45/86.69 (Eq (h (op1 e13 e14)) % 86.45/86.69 (op2 (h e13) (h e14)))) % 86.45/86.69 (Eq (h (op1 e14 e10)) % 86.45/86.69 (op2 (h e14) (h e10)))) % 86.45/86.69 (Eq (h (op1 e14 e11)) % 86.45/86.69 (op2 (h e14) (h e11)))) % 86.45/86.69 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.45/86.69 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.45/86.69 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.45/86.69 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.45/86.69 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.45/86.69 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.45/86.69 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.45/86.69 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.45/86.69 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.45/86.69 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.45/86.69 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.45/86.69 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.45/86.69 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.45/86.69 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.45/86.69 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.45/86.69 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.45/86.69 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.45/86.69 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.45/86.69 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.45/86.69 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.45/86.69 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.45/86.69 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.45/86.69 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.45/86.69 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.45/86.69 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.45/86.69 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.45/86.69 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.45/86.69 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.45/86.69 (Eq (h (j e20)) e20)) % 86.45/86.69 (Eq (h (j e21)) e21)) % 86.45/86.69 (Eq (h (j e22)) e22)) % 86.45/86.69 (Eq (h (j e23)) e23)) % 86.45/86.69 (Eq (h (j e24)) e24)) % 86.45/86.69 (Eq (j (h e10)) e10)) % 86.45/86.69 (Eq (j (h e11)) e11)) % 86.45/86.69 (Eq (j (h e12)) e12)) % 86.45/86.69 True % 86.45/86.69 Clause #219 (by clausification #[217]): Eq (j (h e13)) e13 % 86.45/86.69 Clause #220 (by clausification #[215]): Eq (Eq (op1 e12 e12) e13) True % 86.45/86.69 Clause #221 (by clausification #[215]): Eq % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.69 (Eq (op1 e10 e13) e11)) % 86.45/86.69 (Eq (op1 e10 e14) e13)) % 86.45/86.69 (Eq (op1 e11 e10) e10)) % 86.45/86.69 (Eq (op1 e11 e11) e11)) % 86.45/86.69 (Eq (op1 e11 e12) e12)) % 86.45/86.69 (Eq (op1 e11 e13) e13)) % 86.45/86.69 (Eq (op1 e11 e14) e14)) % 86.45/86.69 (Eq (op1 e12 e10) e11)) % 86.45/86.69 (Eq (op1 e12 e11) e14)) % 86.45/86.69 True % 86.45/86.69 Clause #222 (by clausification #[220]): Eq (op1 e12 e12) e13 % 86.45/86.69 Clause #224 (by clausification #[221]): Eq % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.45/86.69 (Eq (op1 e10 e13) e11)) % 86.45/86.69 (Eq (op1 e10 e14) e13)) % 86.45/86.69 (Eq (op1 e11 e10) e10)) % 86.45/86.69 (Eq (op1 e11 e11) e11)) % 86.45/86.69 (Eq (op1 e11 e12) e12)) % 86.45/86.69 (Eq (op1 e11 e13) e13)) % 86.45/86.69 (Eq (op1 e11 e14) e14)) % 86.45/86.69 (Eq (op1 e12 e10) e11)) % 86.45/86.69 True % 86.45/86.69 Clause #227 (by clausification #[224]): Eq % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.45/86.69 (And % 86.53/86.74 (And % 86.53/86.74 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.53/86.74 (Eq (op1 e10 e13) e11)) % 86.53/86.74 (Eq (op1 e10 e14) e13)) % 86.53/86.74 (Eq (op1 e11 e10) e10)) % 86.53/86.74 (Eq (op1 e11 e11) e11)) % 86.53/86.74 (Eq (op1 e11 e12) e12)) % 86.53/86.74 (Eq (op1 e11 e13) e13)) % 86.53/86.74 (Eq (op1 e11 e14) e14)) % 86.53/86.74 True % 86.53/86.74 Clause #229 (by clausification #[227]): Eq (Eq (op1 e11 e14) e14) True % 86.53/86.74 Clause #230 (by clausification #[227]): Eq % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 86.53/86.74 (Eq (op1 e10 e13) e11)) % 86.53/86.74 (Eq (op1 e10 e14) e13)) % 86.53/86.74 (Eq (op1 e11 e10) e10)) % 86.53/86.74 (Eq (op1 e11 e11) e11)) % 86.53/86.74 (Eq (op1 e11 e12) e12)) % 86.53/86.74 (Eq (op1 e11 e13) e13)) % 86.53/86.74 True % 86.53/86.74 Clause #231 (by clausification #[229]): Eq (op1 e11 e14) e14 % 86.53/86.74 Clause #232 (by clausification #[230]): Eq (Eq (op1 e11 e13) e13) True % 86.53/86.74 Clause #233 (by clausification #[230]): Eq % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 86.53/86.74 (Eq (op1 e10 e14) e13)) % 86.53/86.74 (Eq (op1 e11 e10) e10)) % 86.53/86.74 (Eq (op1 e11 e11) e11)) % 86.53/86.74 (Eq (op1 e11 e12) e12)) % 86.53/86.74 True % 86.53/86.74 Clause #234 (by clausification #[232]): Eq (op1 e11 e13) e13 % 86.53/86.74 Clause #250 (by clausification #[233]): Eq (Eq (op1 e11 e12) e12) True % 86.53/86.74 Clause #251 (by clausification #[233]): Eq % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 86.53/86.74 (Eq (op1 e10 e14) e13)) % 86.53/86.74 (Eq (op1 e11 e10) e10)) % 86.53/86.74 (Eq (op1 e11 e11) e11)) % 86.53/86.74 True % 86.53/86.74 Clause #252 (by clausification #[250]): Eq (op1 e11 e12) e12 % 86.53/86.74 Clause #257 (by clausification #[251]): Eq % 86.53/86.74 (And % 86.53/86.74 (And (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 86.53/86.74 (Eq (op1 e10 e14) e13)) % 86.53/86.74 (Eq (op1 e11 e10) e10)) % 86.53/86.74 True % 86.53/86.74 Clause #259 (by clausification #[257]): Eq (Eq (op1 e11 e10) e10) True % 86.53/86.74 Clause #260 (by clausification #[257]): Eq % 86.53/86.74 (And (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 86.53/86.74 (Eq (op1 e10 e14) e13)) % 86.53/86.74 True % 86.53/86.74 Clause #261 (by clausification #[259]): Eq (op1 e11 e10) e10 % 86.53/86.74 Clause #263 (by clausification #[260]): Eq (And (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) True % 86.53/86.74 Clause #266 (by clausification #[263]): Eq (And (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) True % 86.53/86.74 Clause #269 (by clausification #[266]): Eq (And (Eq (op1 e10 e10) e14) (Eq (op1 e10 e11) e12)) True % 86.53/86.74 Clause #271 (by clausification #[218]): Eq (Eq (j (h e12)) e12) True % 86.53/86.74 Clause #272 (by clausification #[218]): Eq % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (And % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 % 86.53/86.74 e10 % 86.53/86.74 e10)) % 86.53/86.74 (op2 % 86.53/86.74 (h % 86.53/86.74 e10) % 86.53/86.74 (h % 86.53/86.74 e10))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 % 86.53/86.74 e10 % 86.53/86.74 e11)) % 86.53/86.74 (op2 % 86.53/86.74 (h % 86.53/86.74 e10) % 86.53/86.74 (h % 86.53/86.74 e11)))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 % 86.53/86.74 e10 % 86.53/86.74 e12)) % 86.53/86.74 (op2 % 86.53/86.74 (h % 86.53/86.74 e10) % 86.53/86.74 (h % 86.53/86.74 e12)))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 % 86.53/86.74 e10 % 86.53/86.74 e13)) % 86.53/86.74 (op2 % 86.53/86.74 (h % 86.53/86.74 e10) % 86.53/86.74 (h % 86.53/86.74 e13)))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 e10 % 86.53/86.74 e14)) % 86.53/86.74 (op2 % 86.53/86.74 (h e10) % 86.53/86.74 (h % 86.53/86.74 e14)))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 e11 % 86.53/86.74 e10)) % 86.53/86.74 (op2 (h e11) % 86.53/86.74 (h e10)))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 e11 % 86.53/86.74 e11)) % 86.53/86.74 (op2 (h e11) % 86.53/86.74 (h e11)))) % 86.53/86.74 (Eq % 86.53/86.74 (h % 86.53/86.74 (op1 e11 e12)) % 86.53/86.74 (op2 (h e11) % 86.53/86.74 (h e12)))) % 86.53/86.74 (Eq % 86.53/86.74 (h (op1 e11 e13)) % 86.53/86.74 (op2 (h e11) % 86.53/86.74 (h e13)))) % 86.53/86.74 (Eq (h (op1 e11 e14)) % 86.53/86.74 (op2 (h e11) % 86.53/86.74 (h e14)))) % 86.53/86.74 (Eq (h (op1 e12 e10)) % 86.53/86.74 (op2 (h e12) % 86.53/86.74 (h e10)))) % 86.53/86.74 (Eq (h (op1 e12 e11)) % 86.53/86.74 (op2 (h e12) (h e11)))) % 86.53/86.74 (Eq (h (op1 e12 e12)) % 86.53/86.74 (op2 (h e12) (h e12)))) % 86.53/86.74 (Eq (h (op1 e12 e13)) % 86.53/86.74 (op2 (h e12) (h e13)))) % 86.53/86.74 (Eq (h (op1 e12 e14)) % 86.53/86.74 (op2 (h e12) (h e14)))) % 86.53/86.74 (Eq (h (op1 e13 e10)) % 86.53/86.74 (op2 (h e13) (h e10)))) % 86.53/86.74 (Eq (h (op1 e13 e11)) % 86.53/86.74 (op2 (h e13) (h e11)))) % 86.53/86.74 (Eq (h (op1 e13 e12)) % 86.53/86.74 (op2 (h e13) (h e12)))) % 86.53/86.74 (Eq (h (op1 e13 e13)) % 86.53/86.74 (op2 (h e13) (h e13)))) % 86.53/86.74 (Eq (h (op1 e13 e14)) % 86.53/86.74 (op2 (h e13) (h e14)))) % 86.53/86.74 (Eq (h (op1 e14 e10)) % 86.53/86.74 (op2 (h e14) (h e10)))) % 86.53/86.74 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.53/86.74 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.53/86.74 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.53/86.74 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.53/86.74 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.53/86.74 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.53/86.74 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.53/86.74 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.53/86.74 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.53/86.74 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.53/86.74 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.53/86.74 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.53/86.74 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.53/86.74 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.53/86.74 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.53/86.74 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.53/86.74 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.53/86.74 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.53/86.74 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.53/86.74 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.53/86.74 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.53/86.74 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.53/86.74 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.53/86.74 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.53/86.74 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.53/86.74 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.53/86.74 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.53/86.74 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.53/86.74 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.53/86.74 (Eq (h (j e20)) e20)) % 86.53/86.74 (Eq (h (j e21)) e21)) % 86.53/86.74 (Eq (h (j e22)) e22)) % 86.53/86.74 (Eq (h (j e23)) e23)) % 86.53/86.74 (Eq (h (j e24)) e24)) % 86.53/86.74 (Eq (j (h e10)) e10)) % 86.53/86.74 (Eq (j (h e11)) e11)) % 86.53/86.74 True % 86.53/86.74 Clause #273 (by clausification #[271]): Eq (j (h e12)) e12 % 86.53/86.74 Clause #275 (by clausification #[269]): Eq (Eq (op1 e10 e10) e14) True % 86.53/86.74 Clause #277 (by clausification #[275]): Eq (op1 e10 e10) e14 % 86.53/86.74 Clause #305 (by clausification #[272]): Eq (Eq (j (h e11)) e11) True % 86.53/86.77 Clause #306 (by clausification #[272]): Eq % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (And % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 % 86.53/86.77 e10 % 86.53/86.77 e10)) % 86.53/86.77 (op2 % 86.53/86.77 (h % 86.53/86.77 e10) % 86.53/86.77 (h % 86.53/86.77 e10))) % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 % 86.53/86.77 e10 % 86.53/86.77 e11)) % 86.53/86.77 (op2 % 86.53/86.77 (h % 86.53/86.77 e10) % 86.53/86.77 (h % 86.53/86.77 e11)))) % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 % 86.53/86.77 e10 % 86.53/86.77 e12)) % 86.53/86.77 (op2 % 86.53/86.77 (h % 86.53/86.77 e10) % 86.53/86.77 (h % 86.53/86.77 e12)))) % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 e10 % 86.53/86.77 e13)) % 86.53/86.77 (op2 % 86.53/86.77 (h e10) % 86.53/86.77 (h % 86.53/86.77 e13)))) % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 e10 % 86.53/86.77 e14)) % 86.53/86.77 (op2 (h e10) % 86.53/86.77 (h e14)))) % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 e11 % 86.53/86.77 e10)) % 86.53/86.77 (op2 (h e11) % 86.53/86.77 (h e10)))) % 86.53/86.77 (Eq % 86.53/86.77 (h % 86.53/86.77 (op1 e11 e11)) % 86.53/86.77 (op2 (h e11) % 86.53/86.77 (h e11)))) % 86.53/86.77 (Eq % 86.53/86.77 (h (op1 e11 e12)) % 86.53/86.77 (op2 (h e11) % 86.53/86.77 (h e12)))) % 86.53/86.77 (Eq (h (op1 e11 e13)) % 86.53/86.77 (op2 (h e11) % 86.53/86.77 (h e13)))) % 86.53/86.77 (Eq (h (op1 e11 e14)) % 86.53/86.77 (op2 (h e11) % 86.53/86.77 (h e14)))) % 86.53/86.77 (Eq (h (op1 e12 e10)) % 86.53/86.77 (op2 (h e12) (h e10)))) % 86.53/86.77 (Eq (h (op1 e12 e11)) % 86.53/86.77 (op2 (h e12) (h e11)))) % 86.53/86.77 (Eq (h (op1 e12 e12)) % 86.53/86.77 (op2 (h e12) (h e12)))) % 86.53/86.77 (Eq (h (op1 e12 e13)) % 86.53/86.77 (op2 (h e12) (h e13)))) % 86.53/86.77 (Eq (h (op1 e12 e14)) % 86.53/86.77 (op2 (h e12) (h e14)))) % 86.53/86.77 (Eq (h (op1 e13 e10)) % 86.58/86.80 (op2 (h e13) (h e10)))) % 86.58/86.80 (Eq (h (op1 e13 e11)) % 86.58/86.80 (op2 (h e13) (h e11)))) % 86.58/86.80 (Eq (h (op1 e13 e12)) % 86.58/86.80 (op2 (h e13) (h e12)))) % 86.58/86.80 (Eq (h (op1 e13 e13)) % 86.58/86.80 (op2 (h e13) (h e13)))) % 86.58/86.80 (Eq (h (op1 e13 e14)) % 86.58/86.80 (op2 (h e13) (h e14)))) % 86.58/86.80 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.58/86.80 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.58/86.80 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.58/86.80 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.58/86.80 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.58/86.80 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.58/86.80 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.58/86.80 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.58/86.80 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.58/86.80 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.58/86.80 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.58/86.80 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.58/86.80 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.58/86.80 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.58/86.80 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.58/86.80 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.58/86.80 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.58/86.80 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.58/86.80 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.58/86.80 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.58/86.80 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.58/86.80 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.58/86.80 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.58/86.80 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.58/86.80 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.58/86.80 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.58/86.80 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.58/86.80 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.58/86.80 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.58/86.80 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.58/86.80 (Eq (h (j e20)) e20)) % 86.58/86.80 (Eq (h (j e21)) e21)) % 86.58/86.80 (Eq (h (j e22)) e22)) % 86.58/86.80 (Eq (h (j e23)) e23)) % 86.58/86.80 (Eq (h (j e24)) e24)) % 86.58/86.80 (Eq (j (h e10)) e10)) % 86.58/86.80 True % 86.58/86.80 Clause #307 (by clausification #[305]): Eq (j (h e11)) e11 % 86.58/86.80 Clause #341 (by clausification #[306]): Eq (Eq (j (h e10)) e10) True % 86.58/86.80 Clause #342 (by clausification #[306]): Eq % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (And % 86.58/86.80 (Eq % 86.58/86.80 (h % 86.58/86.80 (op1 % 86.58/86.80 e10 % 86.58/86.80 e10)) % 86.58/86.80 (op2 % 86.58/86.80 (h % 86.58/86.80 e10) % 86.58/86.80 (h % 86.58/86.80 e10))) % 86.58/86.80 (Eq % 86.58/86.80 (h % 86.58/86.80 (op1 % 86.58/86.80 e10 % 86.58/86.80 e11)) % 86.58/86.80 (op2 % 86.58/86.80 (h % 86.58/86.80 e10) % 86.58/86.80 (h % 86.58/86.80 e11)))) % 86.58/86.80 (Eq % 86.58/86.80 (h % 86.58/86.80 (op1 e10 % 86.58/86.80 e12)) % 86.58/86.80 (op2 % 86.58/86.80 (h e10) % 86.58/86.80 (h % 86.58/86.80 e12)))) % 86.58/86.80 (Eq % 86.58/86.80 (h % 86.58/86.80 (op1 e10 % 86.58/86.80 e13)) % 86.58/86.80 (op2 (h e10) % 86.58/86.80 (h e13)))) % 86.58/86.80 (Eq % 86.58/86.80 (h % 86.58/86.80 (op1 e10 % 86.58/86.80 e14)) % 86.58/86.80 (op2 (h e10) % 86.58/86.80 (h e14)))) % 86.58/86.80 (Eq % 86.58/86.80 (h % 86.58/86.80 (op1 e11 e10)) % 86.58/86.80 (op2 (h e11) % 86.58/86.80 (h e10)))) % 86.58/86.80 (Eq % 86.58/86.80 (h (op1 e11 e11)) % 86.58/86.80 (op2 (h e11) % 86.58/86.80 (h e11)))) % 86.58/86.80 (Eq (h (op1 e11 e12)) % 86.58/86.80 (op2 (h e11) % 86.58/86.80 (h e12)))) % 86.58/86.80 (Eq (h (op1 e11 e13)) % 86.58/86.80 (op2 (h e11) % 86.58/86.80 (h e13)))) % 86.58/86.80 (Eq (h (op1 e11 e14)) % 86.58/86.80 (op2 (h e11) (h e14)))) % 86.58/86.80 (Eq (h (op1 e12 e10)) % 86.58/86.80 (op2 (h e12) (h e10)))) % 86.58/86.80 (Eq (h (op1 e12 e11)) % 86.58/86.80 (op2 (h e12) (h e11)))) % 86.58/86.80 (Eq (h (op1 e12 e12)) % 86.58/86.80 (op2 (h e12) (h e12)))) % 86.58/86.80 (Eq (h (op1 e12 e13)) % 86.58/86.80 (op2 (h e12) (h e13)))) % 86.58/86.80 (Eq (h (op1 e12 e14)) % 86.58/86.80 (op2 (h e12) (h e14)))) % 86.58/86.80 (Eq (h (op1 e13 e10)) % 86.58/86.80 (op2 (h e13) (h e10)))) % 86.58/86.80 (Eq (h (op1 e13 e11)) % 86.58/86.80 (op2 (h e13) (h e11)))) % 86.58/86.80 (Eq (h (op1 e13 e12)) % 86.58/86.80 (op2 (h e13) (h e12)))) % 86.58/86.80 (Eq (h (op1 e13 e13)) % 86.58/86.80 (op2 (h e13) (h e13)))) % 86.58/86.80 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.58/86.80 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.58/86.80 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.58/86.80 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.58/86.80 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.58/86.82 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.58/86.82 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.58/86.82 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.58/86.82 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.58/86.82 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.58/86.82 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.58/86.82 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.58/86.82 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.58/86.82 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.58/86.82 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.58/86.82 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.58/86.82 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.58/86.82 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.58/86.82 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.58/86.82 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.58/86.82 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.58/86.82 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.58/86.82 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.58/86.82 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.58/86.82 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.58/86.82 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.58/86.82 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.58/86.82 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.58/86.82 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.58/86.82 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.58/86.82 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.58/86.82 (Eq (h (j e20)) e20)) % 86.58/86.82 (Eq (h (j e21)) e21)) % 86.58/86.82 (Eq (h (j e22)) e22)) % 86.58/86.82 (Eq (h (j e23)) e23)) % 86.58/86.82 (Eq (h (j e24)) e24)) % 86.58/86.82 True % 86.58/86.82 Clause #343 (by clausification #[341]): Eq (j (h e10)) e10 % 86.58/86.82 Clause #375 (by clausification #[342]): Eq (Eq (h (j e24)) e24) True % 86.58/86.82 Clause #376 (by clausification #[342]): Eq % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (And % 86.58/86.82 (Eq % 86.58/86.82 (h % 86.58/86.82 (op1 e10 % 86.58/86.82 e10)) % 86.58/86.82 (op2 % 86.58/86.82 (h e10) % 86.58/86.82 (h % 86.58/86.82 e10))) % 86.58/86.82 (Eq % 86.58/86.82 (h % 86.58/86.82 (op1 e10 % 86.58/86.82 e11)) % 86.58/86.82 (op2 % 86.58/86.82 (h e10) % 86.58/86.82 (h % 86.58/86.82 e11)))) % 86.58/86.82 (Eq % 86.58/86.82 (h % 86.58/86.82 (op1 e10 % 86.58/86.82 e12)) % 86.58/86.82 (op2 (h e10) % 86.58/86.82 (h e12)))) % 86.58/86.82 (Eq % 86.58/86.82 (h % 86.58/86.82 (op1 e10 % 86.58/86.82 e13)) % 86.58/86.82 (op2 (h e10) % 86.58/86.82 (h e13)))) % 86.58/86.82 (Eq % 86.58/86.82 (h % 86.58/86.82 (op1 e10 e14)) % 86.58/86.82 (op2 (h e10) % 86.58/86.82 (h e14)))) % 86.58/86.82 (Eq % 86.58/86.82 (h (op1 e11 e10)) % 86.58/86.82 (op2 (h e11) % 86.58/86.82 (h e10)))) % 86.58/86.82 (Eq (h (op1 e11 e11)) % 86.58/86.82 (op2 (h e11) % 86.58/86.82 (h e11)))) % 86.58/86.82 (Eq (h (op1 e11 e12)) % 86.58/86.82 (op2 (h e11) % 86.58/86.82 (h e12)))) % 86.58/86.82 (Eq (h (op1 e11 e13)) % 86.58/86.82 (op2 (h e11) (h e13)))) % 86.58/86.82 (Eq (h (op1 e11 e14)) % 86.58/86.82 (op2 (h e11) (h e14)))) % 86.58/86.82 (Eq (h (op1 e12 e10)) % 86.58/86.82 (op2 (h e12) (h e10)))) % 86.58/86.82 (Eq (h (op1 e12 e11)) % 86.58/86.82 (op2 (h e12) (h e11)))) % 86.58/86.82 (Eq (h (op1 e12 e12)) % 86.58/86.82 (op2 (h e12) (h e12)))) % 86.58/86.82 (Eq (h (op1 e12 e13)) % 86.58/86.82 (op2 (h e12) (h e13)))) % 86.58/86.82 (Eq (h (op1 e12 e14)) % 86.58/86.82 (op2 (h e12) (h e14)))) % 86.58/86.82 (Eq (h (op1 e13 e10)) % 86.58/86.83 (op2 (h e13) (h e10)))) % 86.58/86.83 (Eq (h (op1 e13 e11)) % 86.58/86.83 (op2 (h e13) (h e11)))) % 86.58/86.83 (Eq (h (op1 e13 e12)) % 86.58/86.83 (op2 (h e13) (h e12)))) % 86.58/86.83 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 86.58/86.83 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.58/86.83 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.58/86.83 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.58/86.83 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.58/86.83 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.58/86.83 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.58/86.83 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.58/86.83 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.58/86.83 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.58/86.83 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.58/86.83 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.58/86.83 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.58/86.83 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.58/86.83 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.58/86.83 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.58/86.83 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.58/86.83 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.58/86.83 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.58/86.83 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.58/86.83 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.58/86.83 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.58/86.83 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.58/86.83 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.58/86.83 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.58/86.83 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.58/86.83 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.58/86.83 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.58/86.83 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.58/86.83 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.58/86.83 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.58/86.83 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.58/86.83 (Eq (h (j e20)) e20)) % 86.58/86.83 (Eq (h (j e21)) e21)) % 86.58/86.83 (Eq (h (j e22)) e22)) % 86.58/86.83 (Eq (h (j e23)) e23)) % 86.58/86.83 True % 86.58/86.83 Clause #377 (by clausification #[375]): Eq (h (j e24)) e24 % 86.58/86.83 Clause #378 (by superposition #[377, 102]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e10) (Or (Eq (j e24) e11) (Eq (h e13) e24)))) % 86.58/86.83 Clause #379 (by superposition #[378, 377]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e10) e24)))) % 86.58/86.83 Clause #383 (by superposition #[379, 377]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e24) (Eq (h e12) e24)))) % 86.58/86.83 Clause #389 (by superposition #[383, 377]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e24) (Or (Eq (h e12) e24) (Eq (h e14) e24)))) % 86.58/86.86 Clause #391 (by superposition #[389, 377]): Or (Eq (h e13) e24) (Or (Eq (h e10) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Eq (h e11) e24)))) % 86.58/86.86 Clause #409 (by clausification #[376]): Eq (Eq (h (j e23)) e23) True % 86.58/86.86 Clause #410 (by clausification #[376]): Eq % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (And % 86.58/86.86 (Eq % 86.58/86.86 (h % 86.58/86.86 (op1 e10 % 86.58/86.86 e10)) % 86.58/86.86 (op2 (h e10) % 86.58/86.86 (h e10))) % 86.58/86.86 (Eq % 86.58/86.86 (h % 86.58/86.86 (op1 e10 % 86.58/86.86 e11)) % 86.58/86.86 (op2 (h e10) % 86.58/86.86 (h e11)))) % 86.58/86.86 (Eq % 86.58/86.86 (h % 86.58/86.86 (op1 e10 % 86.58/86.86 e12)) % 86.58/86.86 (op2 (h e10) % 86.58/86.86 (h e12)))) % 86.58/86.86 (Eq % 86.58/86.86 (h % 86.58/86.86 (op1 e10 e13)) % 86.58/86.86 (op2 (h e10) % 86.58/86.86 (h e13)))) % 86.58/86.86 (Eq % 86.58/86.86 (h (op1 e10 e14)) % 86.58/86.86 (op2 (h e10) % 86.58/86.86 (h e14)))) % 86.58/86.86 (Eq (h (op1 e11 e10)) % 86.58/86.86 (op2 (h e11) % 86.58/86.86 (h e10)))) % 86.58/86.86 (Eq (h (op1 e11 e11)) % 86.58/86.86 (op2 (h e11) % 86.58/86.86 (h e11)))) % 86.58/86.86 (Eq (h (op1 e11 e12)) % 86.58/86.86 (op2 (h e11) (h e12)))) % 86.58/86.86 (Eq (h (op1 e11 e13)) % 86.58/86.86 (op2 (h e11) (h e13)))) % 86.58/86.86 (Eq (h (op1 e11 e14)) % 86.58/86.86 (op2 (h e11) (h e14)))) % 86.58/86.86 (Eq (h (op1 e12 e10)) % 86.58/86.86 (op2 (h e12) (h e10)))) % 86.58/86.86 (Eq (h (op1 e12 e11)) % 86.58/86.86 (op2 (h e12) (h e11)))) % 86.58/86.86 (Eq (h (op1 e12 e12)) % 86.58/86.86 (op2 (h e12) (h e12)))) % 86.58/86.86 (Eq (h (op1 e12 e13)) % 86.58/86.86 (op2 (h e12) (h e13)))) % 86.58/86.86 (Eq (h (op1 e12 e14)) % 86.58/86.86 (op2 (h e12) (h e14)))) % 86.58/86.86 (Eq (h (op1 e13 e10)) % 86.58/86.86 (op2 (h e13) (h e10)))) % 86.58/86.86 (Eq (h (op1 e13 e11)) % 86.58/86.86 (op2 (h e13) (h e11)))) % 86.58/86.86 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 86.58/86.86 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 86.58/86.86 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.58/86.86 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.58/86.86 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.58/86.86 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.58/86.86 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.58/86.86 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.58/86.86 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.58/86.86 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.58/86.86 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.58/86.86 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.58/86.86 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.58/86.86 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.58/86.86 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.58/86.86 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.58/86.86 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.58/86.86 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.58/86.86 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.58/86.86 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.58/86.86 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.58/86.86 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.58/86.86 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.58/86.86 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.58/86.86 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.58/86.86 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.58/86.86 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.58/86.86 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.58/86.86 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.58/86.86 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.58/86.86 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.58/86.86 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.58/86.86 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.58/86.86 (Eq (h (j e20)) e20)) % 86.67/86.89 (Eq (h (j e21)) e21)) % 86.67/86.89 (Eq (h (j e22)) e22)) % 86.67/86.89 True % 86.67/86.89 Clause #411 (by clausification #[409]): Eq (h (j e23)) e23 % 86.67/86.89 Clause #412 (by superposition #[411, 175]): Or (Eq (j e23) e14) (Or (Eq (j e23) e12) (Or (Eq (j e23) e10) (Or (Eq (j e23) e11) (Eq (h e13) e23)))) % 86.67/86.89 Clause #413 (by superposition #[412, 411]): Or (Eq (j e23) e14) (Or (Eq (j e23) e12) (Or (Eq (j e23) e11) (Or (Eq (h e13) e23) (Eq (h e10) e23)))) % 86.67/86.89 Clause #417 (by superposition #[413, 411]): Or (Eq (j e23) e14) (Or (Eq (j e23) e11) (Or (Eq (h e13) e23) (Or (Eq (h e10) e23) (Eq (h e12) e23)))) % 86.67/86.89 Clause #423 (by superposition #[417, 411]): Or (Eq (j e23) e11) (Or (Eq (h e13) e23) (Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Eq (h e14) e23)))) % 86.67/86.89 Clause #425 (by superposition #[423, 411]): Or (Eq (h e13) e23) (Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (h e11) e23)))) % 86.67/86.89 Clause #426 (by superposition #[391, 219]): Or (Eq (h e10) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq (j e24) e13)))) % 86.67/86.89 Clause #466 (by clausification #[410]): Eq % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (And % 86.67/86.89 (Eq % 86.67/86.89 (h % 86.67/86.89 (op1 e10 % 86.67/86.89 e10)) % 86.67/86.89 (op2 (h e10) % 86.67/86.89 (h e10))) % 86.67/86.89 (Eq % 86.67/86.89 (h % 86.67/86.89 (op1 e10 % 86.67/86.89 e11)) % 86.67/86.89 (op2 (h e10) % 86.67/86.89 (h e11)))) % 86.67/86.89 (Eq % 86.67/86.89 (h % 86.67/86.89 (op1 e10 e12)) % 86.67/86.89 (op2 (h e10) % 86.67/86.89 (h e12)))) % 86.67/86.89 (Eq % 86.67/86.89 (h (op1 e10 e13)) % 86.67/86.89 (op2 (h e10) % 86.67/86.89 (h e13)))) % 86.67/86.89 (Eq (h (op1 e10 e14)) % 86.67/86.89 (op2 (h e10) % 86.67/86.89 (h e14)))) % 86.67/86.89 (Eq (h (op1 e11 e10)) % 86.67/86.89 (op2 (h e11) % 86.67/86.89 (h e10)))) % 86.67/86.89 (Eq (h (op1 e11 e11)) % 86.67/86.89 (op2 (h e11) (h e11)))) % 86.67/86.89 (Eq (h (op1 e11 e12)) % 86.67/86.89 (op2 (h e11) (h e12)))) % 86.67/86.89 (Eq (h (op1 e11 e13)) % 86.67/86.89 (op2 (h e11) (h e13)))) % 86.67/86.89 (Eq (h (op1 e11 e14)) % 86.67/86.89 (op2 (h e11) (h e14)))) % 86.67/86.89 (Eq (h (op1 e12 e10)) % 86.67/86.89 (op2 (h e12) (h e10)))) % 86.71/86.91 (Eq (h (op1 e12 e11)) % 86.71/86.91 (op2 (h e12) (h e11)))) % 86.71/86.91 (Eq (h (op1 e12 e12)) % 86.71/86.91 (op2 (h e12) (h e12)))) % 86.71/86.91 (Eq (h (op1 e12 e13)) % 86.71/86.91 (op2 (h e12) (h e13)))) % 86.71/86.91 (Eq (h (op1 e12 e14)) % 86.71/86.91 (op2 (h e12) (h e14)))) % 86.71/86.91 (Eq (h (op1 e13 e10)) % 86.71/86.91 (op2 (h e13) (h e10)))) % 86.71/86.91 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 86.71/86.91 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 86.71/86.91 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 86.71/86.91 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.71/86.91 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.71/86.91 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.71/86.91 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.71/86.91 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.71/86.91 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.71/86.91 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.71/86.91 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.71/86.91 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.71/86.91 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.71/86.91 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.71/86.91 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.71/86.91 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.71/86.91 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.71/86.91 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.71/86.91 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.71/86.91 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.71/86.91 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.71/86.91 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.71/86.91 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.71/86.91 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.71/86.91 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.71/86.91 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.71/86.91 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.71/86.91 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.71/86.91 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.71/86.91 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.71/86.91 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.71/86.91 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.71/86.91 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.71/86.91 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.71/86.91 (Eq (h (j e20)) e20)) % 86.71/86.91 (Eq (h (j e21)) e21)) % 86.71/86.91 True % 86.71/86.91 Clause #591 (by clausification #[466]): Eq % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (And % 86.71/86.92 (Eq % 86.71/86.92 (h % 86.71/86.92 (op1 e10 e10)) % 86.71/86.92 (op2 (h e10) % 86.71/86.92 (h e10))) % 86.71/86.92 (Eq % 86.71/86.92 (h % 86.71/86.92 (op1 e10 e11)) % 86.71/86.92 (op2 (h e10) % 86.71/86.92 (h e11)))) % 86.71/86.92 (Eq % 86.71/86.92 (h (op1 e10 e12)) % 86.71/86.92 (op2 (h e10) % 86.71/86.92 (h e12)))) % 86.71/86.92 (Eq (h (op1 e10 e13)) % 86.71/86.92 (op2 (h e10) % 86.71/86.92 (h e13)))) % 86.71/86.92 (Eq (h (op1 e10 e14)) % 86.71/86.92 (op2 (h e10) % 86.71/86.92 (h e14)))) % 86.71/86.92 (Eq (h (op1 e11 e10)) % 86.71/86.92 (op2 (h e11) (h e10)))) % 86.71/86.92 (Eq (h (op1 e11 e11)) % 86.71/86.92 (op2 (h e11) (h e11)))) % 86.71/86.92 (Eq (h (op1 e11 e12)) % 86.71/86.92 (op2 (h e11) (h e12)))) % 86.71/86.92 (Eq (h (op1 e11 e13)) % 86.71/86.92 (op2 (h e11) (h e13)))) % 86.71/86.92 (Eq (h (op1 e11 e14)) % 86.71/86.92 (op2 (h e11) (h e14)))) % 86.71/86.92 (Eq (h (op1 e12 e10)) % 86.71/86.92 (op2 (h e12) (h e10)))) % 86.71/86.92 (Eq (h (op1 e12 e11)) % 86.71/86.92 (op2 (h e12) (h e11)))) % 86.71/86.92 (Eq (h (op1 e12 e12)) % 86.71/86.92 (op2 (h e12) (h e12)))) % 86.71/86.92 (Eq (h (op1 e12 e13)) % 86.71/86.92 (op2 (h e12) (h e13)))) % 86.71/86.92 (Eq (h (op1 e12 e14)) % 86.71/86.92 (op2 (h e12) (h e14)))) % 86.71/86.92 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 86.71/86.92 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 86.71/86.92 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 86.71/86.92 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 86.71/86.92 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.71/86.92 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.71/86.92 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.71/86.92 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.71/86.92 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.73/86.94 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.73/86.94 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.73/86.94 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.73/86.94 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.73/86.94 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.73/86.94 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.73/86.94 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.73/86.94 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.73/86.94 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.73/86.94 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.73/86.94 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.73/86.94 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.73/86.94 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.73/86.94 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.73/86.94 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.73/86.94 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.73/86.94 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.73/86.94 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.73/86.94 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.73/86.94 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.73/86.94 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.73/86.94 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.73/86.94 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.73/86.94 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.73/86.94 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.73/86.94 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.73/86.94 (Eq (h (j e20)) e20)) % 86.73/86.94 True % 86.73/86.94 Clause #900 (by clausification #[591]): Eq (Eq (h (j e20)) e20) True % 86.73/86.94 Clause #901 (by clausification #[591]): Eq % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (And % 86.73/86.94 (Eq % 86.73/86.94 (h (op1 e10 e10)) % 86.73/86.94 (op2 (h e10) % 86.73/86.94 (h e10))) % 86.73/86.94 (Eq % 86.73/86.94 (h (op1 e10 e11)) % 86.73/86.94 (op2 (h e10) % 86.73/86.94 (h e11)))) % 86.73/86.94 (Eq (h (op1 e10 e12)) % 86.73/86.94 (op2 (h e10) % 86.73/86.94 (h e12)))) % 86.73/86.94 (Eq (h (op1 e10 e13)) % 86.73/86.94 (op2 (h e10) % 86.73/86.94 (h e13)))) % 86.73/86.94 (Eq (h (op1 e10 e14)) % 86.73/86.94 (op2 (h e10) (h e14)))) % 86.73/86.94 (Eq (h (op1 e11 e10)) % 86.73/86.94 (op2 (h e11) (h e10)))) % 86.73/86.94 (Eq (h (op1 e11 e11)) % 86.73/86.94 (op2 (h e11) (h e11)))) % 86.73/86.94 (Eq (h (op1 e11 e12)) % 86.73/86.94 (op2 (h e11) (h e12)))) % 86.73/86.94 (Eq (h (op1 e11 e13)) % 86.73/86.94 (op2 (h e11) (h e13)))) % 86.73/86.94 (Eq (h (op1 e11 e14)) % 86.73/86.94 (op2 (h e11) (h e14)))) % 86.73/86.94 (Eq (h (op1 e12 e10)) % 86.73/86.94 (op2 (h e12) (h e10)))) % 86.73/86.94 (Eq (h (op1 e12 e11)) % 86.73/86.94 (op2 (h e12) (h e11)))) % 86.73/86.96 (Eq (h (op1 e12 e12)) % 86.73/86.96 (op2 (h e12) (h e12)))) % 86.73/86.96 (Eq (h (op1 e12 e13)) % 86.73/86.96 (op2 (h e12) (h e13)))) % 86.73/86.96 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 86.73/86.96 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 86.73/86.96 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 86.73/86.96 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 86.73/86.96 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 86.73/86.96 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.73/86.96 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.73/86.96 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.73/86.96 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.73/86.96 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.73/86.96 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.73/86.96 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.73/86.96 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.73/86.96 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.73/86.96 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.73/86.96 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.73/86.96 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.73/86.96 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.73/86.96 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.73/86.96 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.73/86.96 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.73/86.96 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.73/86.96 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.73/86.96 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.73/86.96 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.73/86.96 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.73/86.96 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.73/86.96 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.73/86.96 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.73/86.96 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.73/86.96 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.73/86.96 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.73/86.96 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.73/86.96 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.73/86.96 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.73/86.96 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 86.73/86.96 True % 86.73/86.96 Clause #902 (by clausification #[900]): Eq (h (j e20)) e20 % 86.73/86.96 Clause #1925 (by clausification #[901]): Eq (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24))) True % 86.73/86.96 Clause #1926 (by clausification #[901]): Eq % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (And % 86.73/86.96 (Eq (h (op1 e10 e10)) % 86.73/86.96 (op2 (h e10) % 86.73/86.96 (h e10))) % 86.73/86.96 (Eq (h (op1 e10 e11)) % 86.73/86.96 (op2 (h e10) % 86.73/86.96 (h e11)))) % 86.73/86.96 (Eq (h (op1 e10 e12)) % 86.73/86.96 (op2 (h e10) % 86.73/86.96 (h e12)))) % 86.73/86.96 (Eq (h (op1 e10 e13)) % 86.73/86.96 (op2 (h e10) (h e13)))) % 86.73/86.96 (Eq (h (op1 e10 e14)) % 86.73/86.96 (op2 (h e10) (h e14)))) % 86.73/86.96 (Eq (h (op1 e11 e10)) % 86.73/86.96 (op2 (h e11) (h e10)))) % 86.73/86.96 (Eq (h (op1 e11 e11)) % 86.73/86.96 (op2 (h e11) (h e11)))) % 86.73/86.96 (Eq (h (op1 e11 e12)) % 86.73/86.96 (op2 (h e11) (h e12)))) % 86.73/86.96 (Eq (h (op1 e11 e13)) % 86.73/86.96 (op2 (h e11) (h e13)))) % 86.73/86.96 (Eq (h (op1 e11 e14)) % 86.73/86.96 (op2 (h e11) (h e14)))) % 86.73/86.96 (Eq (h (op1 e12 e10)) % 86.73/86.96 (op2 (h e12) (h e10)))) % 86.73/86.96 (Eq (h (op1 e12 e11)) % 86.73/86.96 (op2 (h e12) (h e11)))) % 86.73/86.96 (Eq (h (op1 e12 e12)) % 86.73/86.96 (op2 (h e12) (h e12)))) % 86.73/86.96 (Eq (h (op1 e12 e13)) (op2 (h e12) (h e13)))) % 86.73/86.96 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 86.73/86.96 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 86.73/86.96 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 86.73/86.96 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 86.73/86.96 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 86.73/86.96 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 86.73/86.96 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 86.73/86.96 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 86.73/86.96 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 86.73/86.96 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 86.73/86.96 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 86.73/86.96 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 86.73/86.96 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 86.73/86.96 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 86.73/86.96 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 86.73/86.96 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 86.73/86.96 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 86.73/86.96 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 86.73/86.96 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 86.73/86.96 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 86.73/86.96 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 86.73/86.96 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 86.73/86.96 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 86.73/86.96 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 86.73/86.96 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 86.73/86.96 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 86.73/86.96 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 86.73/86.96 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 86.73/86.96 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 86.73/86.99 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 86.73/86.99 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 86.73/86.99 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 86.73/86.99 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 86.73/86.99 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 86.73/86.99 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 86.73/86.99 True % 86.73/86.99 Clause #1927 (by clausification #[1925]): Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)) % 86.73/86.99 Clause #1928 (by forward demodulation #[1927, 73]): Eq (j e24) (op1 (j e24) (j e24)) % 86.73/86.99 Clause #1934 (by superposition #[1928, 426]): Or (Eq (h e10) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq e13 (op1 e13 e13))))) % 86.73/86.99 Clause #1940 (by superposition #[1934, 198]): Or (Eq (h e10) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq e13 e12)))) % 86.73/86.99 Clause #1941 (by forward contextual literal cutting #[1940, 45]): Or (Eq (h e10) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Eq (h e11) e24))) % 86.73/86.99 Clause #1942 (by superposition #[1941, 343]): Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq (j e24) e10))) % 86.73/86.99 Clause #1966 (by superposition #[1942, 1928]): Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq e10 (op1 e10 e10)))) % 86.73/86.99 Clause #1967 (by superposition #[1966, 277]): Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq e10 e14))) % 86.73/86.99 Clause #1968 (by forward contextual literal cutting #[1967, 60]): Or (Eq (h e12) e24) (Or (Eq (h e14) e24) (Eq (h e11) e24)) % 86.73/86.99 Clause #1969 (by superposition #[1968, 273]): Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq (j e24) e12)) % 86.73/86.99 Clause #1973 (by superposition #[1969, 1928]): Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq e12 (op1 e12 e12))) % 86.73/86.99 Clause #1974 (by superposition #[1973, 222]): Or (Eq (h e14) e24) (Or (Eq (h e11) e24) (Eq e12 e13)) % 86.73/86.99 Clause #1975 (by forward contextual literal cutting #[1974, 45]): Or (Eq (h e14) e24) (Eq (h e11) e24) % 86.73/86.99 Clause #1976 (by superposition #[1975, 149]): Or (Eq (h e11) e24) (Eq (j e24) e14) % 86.73/86.99 Clause #1979 (by superposition #[1976, 1928]): Or (Eq (h e11) e24) (Eq e14 (op1 e14 e14)) % 86.73/86.99 Clause #1980 (by superposition #[1979, 57]): Or (Eq (h e11) e24) (Eq e14 e10) % 86.73/86.99 Clause #1981 (by forward contextual literal cutting #[1980, 60]): Eq (h e11) e24 % 86.73/86.99 Clause #1982 (by backward demodulation #[1981, 307]): Eq (j e24) e11 % 86.73/86.99 Clause #1983 (by backward demodulation #[1981, 425]): Or (Eq (h e13) e23) (Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq e24 e23)))) % 86.73/86.99 Clause #2048 (by forward contextual literal cutting #[1983, 8]): Or (Eq (h e13) e23) (Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Eq (h e14) e23))) % 86.73/86.99 Clause #2049 (by superposition #[2048, 219]): Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (j e23) e13))) % 86.73/86.99 Clause #4173 (by clausification #[1926]): Eq (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23))) True % 86.73/86.99 Clause #4175 (by clausification #[4173]): Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)) % 86.73/86.99 Clause #4176 (by forward demodulation #[4175, 130]): Eq (j e20) (op1 (j e24) (j e23)) % 86.73/86.99 Clause #4177 (by forward demodulation #[4176, 1982]): Eq (j e20) (op1 e11 (j e23)) % 86.73/86.99 Clause #4182 (by superposition #[4177, 2049]): Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (j e20) (op1 e11 e13)))) % 86.73/86.99 Clause #4183 (by superposition #[4182, 234]): Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (j e20) e13))) % 86.73/86.99 Clause #4186 (by superposition #[4183, 902]): Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (h e13) e20))) % 86.73/86.99 Clause #4214 (by superposition #[4186, 2048]): Or (Eq (h e10) e23) % 86.73/86.99 (Or (Eq (h e12) e23) % 86.73/86.99 (Or (Eq (h e14) e23) (Or (Eq e20 e23) (Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Eq (h e14) e23)))))) % 86.73/86.99 Clause #5305 (by eliminate duplicate literals #[4214]): Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq e20 e23))) % 86.73/86.99 Clause #5306 (by forward contextual literal cutting #[5305, 32]): Or (Eq (h e10) e23) (Or (Eq (h e12) e23) (Eq (h e14) e23)) % 86.73/86.99 Clause #5307 (by superposition #[5306, 343]): Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (j e23) e10)) % 86.73/86.99 Clause #5315 (by superposition #[5307, 4177]): Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (j e20) (op1 e11 e10))) % 86.73/87.01 Clause #5324 (by superposition #[5315, 261]): Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (j e20) e10)) % 86.73/87.01 Clause #5329 (by superposition #[5324, 902]): Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq (h e10) e20)) % 86.73/87.01 Clause #5343 (by superposition #[5329, 5306]): Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Or (Eq e20 e23) (Or (Eq (h e12) e23) (Eq (h e14) e23)))) % 86.73/87.01 Clause #5344 (by eliminate duplicate literals #[5343]): Or (Eq (h e12) e23) (Or (Eq (h e14) e23) (Eq e20 e23)) % 86.73/87.01 Clause #5345 (by forward contextual literal cutting #[5344, 32]): Or (Eq (h e12) e23) (Eq (h e14) e23) % 86.73/87.01 Clause #5346 (by superposition #[5345, 273]): Or (Eq (h e14) e23) (Eq (j e23) e12) % 86.73/87.01 Clause #5350 (by superposition #[5346, 4177]): Or (Eq (h e14) e23) (Eq (j e20) (op1 e11 e12)) % 86.73/87.01 Clause #5356 (by superposition #[5350, 252]): Or (Eq (h e14) e23) (Eq (j e20) e12) % 86.73/87.01 Clause #5361 (by superposition #[5356, 902]): Or (Eq (h e14) e23) (Eq (h e12) e20) % 86.73/87.01 Clause #5370 (by superposition #[5361, 5345]): Or (Eq (h e14) e23) (Or (Eq e20 e23) (Eq (h e14) e23)) % 86.73/87.01 Clause #5371 (by eliminate duplicate literals #[5370]): Or (Eq (h e14) e23) (Eq e20 e23) % 86.73/87.01 Clause #5372 (by forward contextual literal cutting #[5371, 32]): Eq (h e14) e23 % 86.73/87.01 Clause #5373 (by backward demodulation #[5372, 149]): Eq (j e23) e14 % 86.73/87.01 Clause #5445 (by backward demodulation #[5373, 4177]): Eq (j e20) (op1 e11 e14) % 86.73/87.01 Clause #5460 (by superposition #[5445, 231]): Eq (j e20) e14 % 86.73/87.01 Clause #5467 (by backward demodulation #[5460, 902]): Eq (h e14) e20 % 86.73/87.01 Clause #5475 (by superposition #[5467, 5372]): Eq e20 e23 % 86.73/87.01 Clause #5476 (by forward contextual literal cutting #[5475, 32]): False % 86.73/87.01 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------