%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG087+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:43:59 PM UTC 2025 % Result : Theorem 78.44s 78.70s % Output : Proof 79.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : ALG087+1 : TPTP v9.2.0. Released v2.7.0. % 0.03/0.13 % Command : duper %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 09:24:23 EDT 2025 % 0.12/0.34 % CPUTime : % 78.44/78.70 SZS status Theorem for theBenchmark.p % 78.44/78.70 SZS output start Proof for theBenchmark.p % 78.44/78.70 Clause #0 (by assumption #[]): Eq % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 78.44/78.70 (Ne e11 e14)) % 78.44/78.70 (Ne e12 e13)) % 78.44/78.70 (Ne e12 e14)) % 78.44/78.70 (Ne e13 e14)) % 78.44/78.70 True % 78.44/78.70 Clause #1 (by assumption #[]): Eq % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 78.44/78.70 (Ne e21 e24)) % 78.44/78.70 (Ne e22 e23)) % 78.44/78.70 (Ne e22 e24)) % 78.44/78.70 (Ne e23 e24)) % 78.44/78.70 True % 78.44/78.70 Clause #3 (by assumption #[]): Eq % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And % 78.44/78.70 (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) % 78.44/78.70 (Eq (op1 e10 e12) e12)) % 78.44/78.70 (Eq (op1 e10 e13) e13)) % 78.44/78.70 (Eq (op1 e10 e14) e14)) % 78.44/78.70 (Eq (op1 e11 e10) e11)) % 78.44/78.70 (Eq (op1 e11 e11) e10)) % 78.44/78.70 (Eq (op1 e11 e12) e13)) % 78.44/78.70 (Eq (op1 e11 e13) e14)) % 78.44/78.70 (Eq (op1 e11 e14) e12)) % 78.44/78.70 (Eq (op1 e12 e10) e12)) % 78.44/78.70 (Eq (op1 e12 e11) e14)) % 78.44/78.70 (Eq (op1 e12 e12) e10)) % 78.53/78.70 (Eq (op1 e12 e13) e11)) % 78.53/78.70 (Eq (op1 e12 e14) e13)) % 78.53/78.70 (Eq (op1 e13 e10) e13)) % 78.53/78.70 (Eq (op1 e13 e11) e12)) % 78.53/78.70 (Eq (op1 e13 e12) e14)) % 78.53/78.70 (Eq (op1 e13 e13) e10)) % 78.53/78.70 (Eq (op1 e13 e14) e11)) % 78.53/78.70 (Eq (op1 e14 e10) e14)) % 78.53/78.70 (Eq (op1 e14 e11) e13)) % 78.53/78.70 (Eq (op1 e14 e12) e11)) % 78.53/78.70 (Eq (op1 e14 e13) e12)) % 78.53/78.70 (Eq (op1 e14 e14) e10)) % 78.53/78.70 True % 78.53/78.70 Clause #4 (by assumption #[]): Eq % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And % 78.53/78.70 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e21)) % 78.53/78.70 (Eq (op2 e20 e22) e22)) % 78.53/78.70 (Eq (op2 e20 e23) e23)) % 78.53/78.70 (Eq (op2 e20 e24) e24)) % 78.53/78.70 (Eq (op2 e21 e20) e21)) % 78.53/78.70 (Eq (op2 e21 e21) e20)) % 78.53/78.70 (Eq (op2 e21 e22) e24)) % 78.53/78.70 (Eq (op2 e21 e23) e22)) % 78.53/78.70 (Eq (op2 e21 e24) e23)) % 78.53/78.70 (Eq (op2 e22 e20) e22)) % 78.53/78.70 (Eq (op2 e22 e21) e24)) % 78.53/78.70 (Eq (op2 e22 e22) e23)) % 78.53/78.70 (Eq (op2 e22 e23) e20)) % 78.53/78.70 (Eq (op2 e22 e24) e21)) % 78.53/78.70 (Eq (op2 e23 e20) e23)) % 78.53/78.74 (Eq (op2 e23 e21) e22)) % 78.53/78.74 (Eq (op2 e23 e22) e21)) % 78.53/78.74 (Eq (op2 e23 e23) e24)) % 78.53/78.74 (Eq (op2 e23 e24) e20)) % 78.53/78.74 (Eq (op2 e24 e20) e24)) % 78.53/78.74 (Eq (op2 e24 e21) e23)) % 78.53/78.74 (Eq (op2 e24 e22) e20)) % 78.53/78.74 (Eq (op2 e24 e23) e21)) % 78.53/78.74 (Eq (op2 e24 e24) e22)) % 78.53/78.74 True % 78.53/78.74 Clause #5 (by assumption #[]): Eq % 78.53/78.74 (Not % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 78.53/78.74 (Eq (h e10) e24)) % 78.53/78.74 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 78.53/78.74 (Eq (h e11) e24))) % 78.53/78.74 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 78.53/78.74 (Eq (h e12) e24))) % 78.53/78.74 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 78.53/78.74 (Eq (h e13) e24))) % 78.53/78.74 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) % 78.53/78.74 (Eq (h e14) e24))) % 78.53/78.74 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) % 78.53/78.74 (Eq (j e20) e14))) % 78.53/78.74 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 78.53/78.74 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 78.53/78.74 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 78.53/78.74 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) → % 78.53/78.74 Not % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (And % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e10 % 78.53/78.74 e10)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e10) % 78.53/78.74 (h % 78.53/78.74 e10))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e10 % 78.53/78.74 e11)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e10) % 78.53/78.74 (h % 78.53/78.74 e11)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e10 % 78.53/78.74 e12)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e10) % 78.53/78.74 (h % 78.53/78.74 e12)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e10 % 78.53/78.74 e13)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e10) % 78.53/78.74 (h % 78.53/78.74 e13)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e10 % 78.53/78.74 e14)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e10) % 78.53/78.74 (h % 78.53/78.74 e14)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e11 % 78.53/78.74 e10)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e11) % 78.53/78.74 (h % 78.53/78.74 e10)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e11 % 78.53/78.74 e11)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e11) % 78.53/78.74 (h % 78.53/78.74 e11)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e11 % 78.53/78.74 e12)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e11) % 78.53/78.74 (h % 78.53/78.74 e12)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e11 % 78.53/78.74 e13)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e11) % 78.53/78.74 (h % 78.53/78.74 e13)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 % 78.53/78.74 e11 % 78.53/78.74 e14)) % 78.53/78.74 (op2 % 78.53/78.74 (h % 78.53/78.74 e11) % 78.53/78.74 (h % 78.53/78.74 e14)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 e12 % 78.53/78.74 e10)) % 78.53/78.74 (op2 % 78.53/78.74 (h e12) % 78.53/78.74 (h % 78.53/78.74 e10)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 e12 % 78.53/78.74 e11)) % 78.53/78.74 (op2 (h e12) % 78.53/78.74 (h e11)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 e12 % 78.53/78.74 e12)) % 78.53/78.74 (op2 (h e12) % 78.53/78.74 (h e12)))) % 78.53/78.74 (Eq % 78.53/78.74 (h % 78.53/78.74 (op1 e12 e13)) % 78.53/78.74 (op2 (h e12) % 78.53/78.74 (h e13)))) % 78.53/78.74 (Eq % 78.53/78.74 (h (op1 e12 e14)) % 78.53/78.74 (op2 (h e12) % 78.53/78.74 (h e14)))) % 78.53/78.74 (Eq (h (op1 e13 e10)) % 78.53/78.74 (op2 (h e13) % 78.53/78.74 (h e10)))) % 78.53/78.74 (Eq (h (op1 e13 e11)) % 78.53/78.74 (op2 (h e13) % 78.53/78.74 (h e11)))) % 78.53/78.74 (Eq (h (op1 e13 e12)) % 78.53/78.74 (op2 (h e13) (h e12)))) % 78.53/78.74 (Eq (h (op1 e13 e13)) % 78.53/78.74 (op2 (h e13) (h e13)))) % 78.53/78.74 (Eq (h (op1 e13 e14)) % 78.53/78.74 (op2 (h e13) (h e14)))) % 78.53/78.74 (Eq (h (op1 e14 e10)) % 78.53/78.74 (op2 (h e14) (h e10)))) % 78.53/78.74 (Eq (h (op1 e14 e11)) % 78.53/78.74 (op2 (h e14) (h e11)))) % 78.53/78.74 (Eq (h (op1 e14 e12)) % 78.53/78.74 (op2 (h e14) (h e12)))) % 78.53/78.74 (Eq (h (op1 e14 e13)) % 78.53/78.74 (op2 (h e14) (h e13)))) % 78.53/78.74 (Eq (h (op1 e14 e14)) % 78.53/78.74 (op2 (h e14) (h e14)))) % 78.53/78.75 (Eq (j (op2 e20 e20)) % 78.53/78.75 (op1 (j e20) (j e20)))) % 78.53/78.75 (Eq (j (op2 e20 e21)) % 78.53/78.75 (op1 (j e20) (j e21)))) % 78.53/78.75 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.53/78.75 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.53/78.75 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.53/78.75 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.53/78.75 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.53/78.75 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.53/78.75 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.53/78.75 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.53/78.75 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.53/78.75 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.53/78.75 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.53/78.75 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.53/78.75 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.53/78.75 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.53/78.75 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.53/78.75 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.53/78.75 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.53/78.75 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.53/78.75 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.53/78.75 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.53/78.75 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.53/78.75 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.53/78.75 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.53/78.75 (Eq (h (j e20)) e20)) % 78.53/78.75 (Eq (h (j e21)) e21)) % 78.53/78.75 (Eq (h (j e22)) e22)) % 78.53/78.75 (Eq (h (j e23)) e23)) % 78.53/78.75 (Eq (h (j e24)) e24)) % 78.53/78.75 (Eq (j (h e10)) e10)) % 78.53/78.75 (Eq (j (h e11)) e11)) % 78.53/78.75 (Eq (j (h e12)) e12)) % 78.53/78.75 (Eq (j (h e13)) e13)) % 78.53/78.75 (Eq (j (h e14)) e14)))) % 78.53/78.75 True % 78.53/78.75 Clause #7 (by clausification #[1]): Eq % 78.53/78.75 (And % 78.53/78.75 (And % 78.53/78.75 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 78.53/78.75 (Ne e21 e24)) % 78.53/78.75 (Ne e22 e23)) % 78.53/78.75 (Ne e22 e24)) % 78.53/78.75 True % 78.53/78.75 Clause #9 (by clausification #[7]): Eq (Ne e22 e24) True % 78.53/78.75 Clause #10 (by clausification #[7]): Eq % 78.53/78.75 (And % 78.53/78.75 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 78.53/78.75 (Ne e21 e24)) % 78.53/78.75 (Ne e22 e23)) % 78.53/78.75 True % 78.53/78.75 Clause #11 (by clausification #[9]): Ne e22 e24 % 78.53/78.75 Clause #13 (by clausification #[10]): Eq % 78.53/78.75 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 78.53/78.75 (Ne e21 e24)) % 78.53/78.75 True % 78.53/78.75 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 % 78.53/78.75 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 % 78.53/78.77 Clause #22 (by clausification #[0]): Eq % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 78.53/78.77 (Ne e11 e14)) % 78.53/78.77 (Ne e12 e13)) % 78.53/78.77 (Ne e12 e14)) % 78.53/78.77 True % 78.53/78.77 Clause #25 (by clausification #[19]): Eq (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) True % 78.53/78.77 Clause #27 (by clausification #[25]): Eq (Ne e20 e24) True % 78.53/78.77 Clause #29 (by clausification #[27]): Ne e20 e24 % 78.53/78.77 Clause #40 (by clausification #[22]): Eq (Ne e12 e14) True % 78.53/78.77 Clause #41 (by clausification #[22]): Eq % 78.53/78.77 (And % 78.53/78.77 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 78.53/78.77 (Ne e11 e14)) % 78.53/78.77 (Ne e12 e13)) % 78.53/78.77 True % 78.53/78.77 Clause #42 (by clausification #[40]): Ne e12 e14 % 78.53/78.77 Clause #44 (by clausification #[41]): Eq % 78.53/78.77 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 78.53/78.77 (Ne e11 e14)) % 78.53/78.77 True % 78.53/78.77 Clause #46 (by clausification #[44]): Eq (Ne e11 e14) True % 78.53/78.77 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 % 78.53/78.77 Clause #48 (by clausification #[46]): Ne e11 e14 % 78.53/78.77 Clause #49 (by clausification #[47]): Eq (Ne e11 e13) True % 78.53/78.77 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 % 78.53/78.77 Clause #51 (by clausification #[49]): Ne e11 e13 % 78.53/78.77 Clause #52 (by clausification #[50]): Eq (Ne e11 e12) True % 78.53/78.77 Clause #54 (by clausification #[52]): Ne e11 e12 % 78.53/78.77 Clause #55 (by clausification #[3]): Eq (Eq (op1 e14 e14) e10) True % 78.53/78.77 Clause #56 (by clausification #[3]): Eq % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) % 78.53/78.77 (Eq (op1 e10 e12) e12)) % 78.53/78.77 (Eq (op1 e10 e13) e13)) % 78.53/78.77 (Eq (op1 e10 e14) e14)) % 78.53/78.77 (Eq (op1 e11 e10) e11)) % 78.53/78.77 (Eq (op1 e11 e11) e10)) % 78.53/78.77 (Eq (op1 e11 e12) e13)) % 78.53/78.77 (Eq (op1 e11 e13) e14)) % 78.53/78.77 (Eq (op1 e11 e14) e12)) % 78.53/78.77 (Eq (op1 e12 e10) e12)) % 78.53/78.77 (Eq (op1 e12 e11) e14)) % 78.53/78.77 (Eq (op1 e12 e12) e10)) % 78.53/78.77 (Eq (op1 e12 e13) e11)) % 78.53/78.77 (Eq (op1 e12 e14) e13)) % 78.53/78.77 (Eq (op1 e13 e10) e13)) % 78.53/78.77 (Eq (op1 e13 e11) e12)) % 78.53/78.77 (Eq (op1 e13 e12) e14)) % 78.53/78.77 (Eq (op1 e13 e13) e10)) % 78.53/78.77 (Eq (op1 e13 e14) e11)) % 78.53/78.77 (Eq (op1 e14 e10) e14)) % 78.53/78.77 (Eq (op1 e14 e11) e13)) % 78.53/78.77 (Eq (op1 e14 e12) e11)) % 78.53/78.77 (Eq (op1 e14 e13) e12)) % 78.53/78.77 True % 78.53/78.77 Clause #57 (by clausification #[55]): Eq (op1 e14 e14) e10 % 78.53/78.77 Clause #71 (by clausification #[4]): Eq (Eq (op2 e24 e24) e22) True % 78.53/78.77 Clause #72 (by clausification #[4]): Eq % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.53/78.77 (And % 78.62/78.80 (And % 78.62/78.80 (And % 78.62/78.80 (And % 78.62/78.80 (And % 78.62/78.80 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e21)) % 78.62/78.80 (Eq (op2 e20 e22) e22)) % 78.62/78.80 (Eq (op2 e20 e23) e23)) % 78.62/78.80 (Eq (op2 e20 e24) e24)) % 78.62/78.80 (Eq (op2 e21 e20) e21)) % 78.62/78.80 (Eq (op2 e21 e21) e20)) % 78.62/78.80 (Eq (op2 e21 e22) e24)) % 78.62/78.80 (Eq (op2 e21 e23) e22)) % 78.62/78.80 (Eq (op2 e21 e24) e23)) % 78.62/78.80 (Eq (op2 e22 e20) e22)) % 78.62/78.80 (Eq (op2 e22 e21) e24)) % 78.62/78.80 (Eq (op2 e22 e22) e23)) % 78.62/78.80 (Eq (op2 e22 e23) e20)) % 78.62/78.80 (Eq (op2 e22 e24) e21)) % 78.62/78.81 (Eq (op2 e23 e20) e23)) % 78.62/78.81 (Eq (op2 e23 e21) e22)) % 78.62/78.81 (Eq (op2 e23 e22) e21)) % 78.62/78.81 (Eq (op2 e23 e23) e24)) % 78.62/78.81 (Eq (op2 e23 e24) e20)) % 78.62/78.81 (Eq (op2 e24 e20) e24)) % 78.62/78.81 (Eq (op2 e24 e21) e23)) % 78.62/78.81 (Eq (op2 e24 e22) e20)) % 78.62/78.81 (Eq (op2 e24 e23) e21)) % 78.62/78.81 True % 78.62/78.81 Clause #73 (by clausification #[71]): Eq (op2 e24 e24) e22 % 78.62/78.81 Clause #89 (by clausification #[5]): Eq % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 78.62/78.81 (Eq (h e10) e24)) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 78.62/78.81 (Eq (h e11) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 78.62/78.81 (Eq (h e12) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 78.62/78.81 (Eq (h e13) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) % 78.62/78.81 (Eq (h e14) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) → % 78.62/78.81 Not % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e10 % 78.62/78.81 e10)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e10) % 78.62/78.81 (h % 78.62/78.81 e10))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e10 % 78.62/78.81 e11)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e10) % 78.62/78.81 (h % 78.62/78.81 e11)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e10 % 78.62/78.81 e12)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e10) % 78.62/78.81 (h % 78.62/78.81 e12)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e10 % 78.62/78.81 e13)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e10) % 78.62/78.81 (h % 78.62/78.81 e13)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e10 % 78.62/78.81 e14)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e10) % 78.62/78.81 (h % 78.62/78.81 e14)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e11 % 78.62/78.81 e10)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e11) % 78.62/78.81 (h % 78.62/78.81 e10)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e11 % 78.62/78.81 e11)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e11) % 78.62/78.81 (h % 78.62/78.81 e11)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e11 % 78.62/78.81 e12)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e11) % 78.62/78.81 (h % 78.62/78.81 e12)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 % 78.62/78.81 e11 % 78.62/78.81 e13)) % 78.62/78.81 (op2 % 78.62/78.81 (h % 78.62/78.81 e11) % 78.62/78.81 (h % 78.62/78.81 e13)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 e11 % 78.62/78.81 e14)) % 78.62/78.81 (op2 % 78.62/78.81 (h e11) % 78.62/78.81 (h % 78.62/78.81 e14)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 e12 % 78.62/78.81 e10)) % 78.62/78.81 (op2 (h e12) % 78.62/78.81 (h e10)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 e12 % 78.62/78.81 e11)) % 78.62/78.81 (op2 (h e12) % 78.62/78.81 (h e11)))) % 78.62/78.81 (Eq % 78.62/78.81 (h % 78.62/78.81 (op1 e12 e12)) % 78.62/78.81 (op2 (h e12) % 78.62/78.81 (h e12)))) % 78.62/78.81 (Eq % 78.62/78.81 (h (op1 e12 e13)) % 78.62/78.81 (op2 (h e12) % 78.62/78.81 (h e13)))) % 78.62/78.81 (Eq (h (op1 e12 e14)) % 78.62/78.81 (op2 (h e12) % 78.62/78.81 (h e14)))) % 78.62/78.81 (Eq (h (op1 e13 e10)) % 78.62/78.81 (op2 (h e13) % 78.62/78.81 (h e10)))) % 78.62/78.81 (Eq (h (op1 e13 e11)) % 78.62/78.81 (op2 (h e13) (h e11)))) % 78.62/78.81 (Eq (h (op1 e13 e12)) % 78.62/78.81 (op2 (h e13) (h e12)))) % 78.62/78.81 (Eq (h (op1 e13 e13)) % 78.62/78.81 (op2 (h e13) (h e13)))) % 78.62/78.81 (Eq (h (op1 e13 e14)) % 78.62/78.81 (op2 (h e13) (h e14)))) % 78.62/78.81 (Eq (h (op1 e14 e10)) % 78.62/78.81 (op2 (h e14) (h e10)))) % 78.62/78.81 (Eq (h (op1 e14 e11)) % 78.62/78.81 (op2 (h e14) (h e11)))) % 78.62/78.81 (Eq (h (op1 e14 e12)) % 78.62/78.81 (op2 (h e14) (h e12)))) % 78.62/78.81 (Eq (h (op1 e14 e13)) % 78.62/78.81 (op2 (h e14) (h e13)))) % 78.62/78.81 (Eq (h (op1 e14 e14)) % 78.62/78.81 (op2 (h e14) (h e14)))) % 78.62/78.81 (Eq (j (op2 e20 e20)) % 78.62/78.81 (op1 (j e20) (j e20)))) % 78.62/78.81 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.62/78.81 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.62/78.81 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.62/78.81 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.62/78.81 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.62/78.81 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.62/78.81 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.62/78.81 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.62/78.81 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.62/78.81 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.62/78.81 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.62/78.81 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.62/78.81 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.62/78.81 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.62/78.81 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.62/78.81 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.62/78.81 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.62/78.81 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.62/78.81 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.62/78.81 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.62/78.81 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.62/78.81 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.62/78.81 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.62/78.81 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.62/78.81 (Eq (h (j e20)) e20)) % 78.62/78.81 (Eq (h (j e21)) e21)) % 78.62/78.81 (Eq (h (j e22)) e22)) % 78.62/78.81 (Eq (h (j e23)) e23)) % 78.62/78.81 (Eq (h (j e24)) e24)) % 78.62/78.81 (Eq (j (h e10)) e10)) % 78.62/78.81 (Eq (j (h e11)) e11)) % 78.62/78.81 (Eq (j (h e12)) e12)) % 78.62/78.81 (Eq (j (h e13)) e13)) % 78.62/78.81 (Eq (j (h e14)) e14))) % 78.62/78.81 False % 78.62/78.81 Clause #90 (by clausification #[89]): Eq % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (And % 78.62/78.81 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 78.62/78.81 (Eq (h e10) e24)) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 78.62/78.81 (Eq (h e11) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 78.62/78.81 (Eq (h e12) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 78.62/78.81 (Eq (h e13) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) (Eq (h e14) e24))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 78.62/78.81 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14))) % 78.62/78.84 True % 78.62/78.84 Clause #91 (by clausification #[89]): Eq % 78.62/78.84 (Not % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (And % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e10 % 78.62/78.84 e10)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e10) % 78.62/78.84 (h % 78.62/78.84 e10))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e10 % 78.62/78.84 e11)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e10) % 78.62/78.84 (h % 78.62/78.84 e11)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e10 % 78.62/78.84 e12)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e10) % 78.62/78.84 (h % 78.62/78.84 e12)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e10 % 78.62/78.84 e13)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e10) % 78.62/78.84 (h % 78.62/78.84 e13)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e10 % 78.62/78.84 e14)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e10) % 78.62/78.84 (h % 78.62/78.84 e14)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e11 % 78.62/78.84 e10)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e11) % 78.62/78.84 (h % 78.62/78.84 e10)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e11 % 78.62/78.84 e11)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e11) % 78.62/78.84 (h % 78.62/78.84 e11)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 % 78.62/78.84 e11 % 78.62/78.84 e12)) % 78.62/78.84 (op2 % 78.62/78.84 (h % 78.62/78.84 e11) % 78.62/78.84 (h % 78.62/78.84 e12)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 e11 % 78.62/78.84 e13)) % 78.62/78.84 (op2 % 78.62/78.84 (h e11) % 78.62/78.84 (h % 78.62/78.84 e13)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 e11 % 78.62/78.84 e14)) % 78.62/78.84 (op2 (h e11) % 78.62/78.84 (h e14)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 e12 % 78.62/78.84 e10)) % 78.62/78.84 (op2 (h e12) % 78.62/78.84 (h e10)))) % 78.62/78.84 (Eq % 78.62/78.84 (h % 78.62/78.84 (op1 e12 e11)) % 78.62/78.84 (op2 (h e12) % 78.62/78.84 (h e11)))) % 78.62/78.84 (Eq % 78.62/78.84 (h (op1 e12 e12)) % 78.62/78.84 (op2 (h e12) % 78.62/78.84 (h e12)))) % 78.62/78.84 (Eq (h (op1 e12 e13)) % 78.62/78.84 (op2 (h e12) % 78.62/78.84 (h e13)))) % 78.62/78.84 (Eq (h (op1 e12 e14)) % 78.62/78.84 (op2 (h e12) % 78.62/78.84 (h e14)))) % 78.62/78.84 (Eq (h (op1 e13 e10)) % 78.62/78.84 (op2 (h e13) (h e10)))) % 78.62/78.84 (Eq (h (op1 e13 e11)) % 78.62/78.84 (op2 (h e13) (h e11)))) % 78.62/78.84 (Eq (h (op1 e13 e12)) % 78.62/78.84 (op2 (h e13) (h e12)))) % 78.62/78.84 (Eq (h (op1 e13 e13)) % 78.62/78.84 (op2 (h e13) (h e13)))) % 78.62/78.84 (Eq (h (op1 e13 e14)) % 78.62/78.84 (op2 (h e13) (h e14)))) % 78.62/78.84 (Eq (h (op1 e14 e10)) % 78.62/78.84 (op2 (h e14) (h e10)))) % 78.62/78.84 (Eq (h (op1 e14 e11)) % 78.62/78.84 (op2 (h e14) (h e11)))) % 78.62/78.84 (Eq (h (op1 e14 e12)) % 78.62/78.84 (op2 (h e14) (h e12)))) % 78.62/78.84 (Eq (h (op1 e14 e13)) % 78.62/78.84 (op2 (h e14) (h e13)))) % 78.62/78.84 (Eq (h (op1 e14 e14)) % 78.62/78.84 (op2 (h e14) (h e14)))) % 78.62/78.84 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.62/78.84 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.62/78.85 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.62/78.85 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.62/78.85 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.62/78.85 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.62/78.85 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.62/78.85 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.62/78.85 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.62/78.85 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.62/78.85 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.62/78.85 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.62/78.85 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.62/78.85 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.62/78.85 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.62/78.85 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.62/78.85 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.62/78.85 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.62/78.85 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.62/78.85 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.62/78.85 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.62/78.85 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.62/78.85 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.62/78.85 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.62/78.85 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.62/78.85 (Eq (h (j e20)) e20)) % 78.62/78.85 (Eq (h (j e21)) e21)) % 78.62/78.85 (Eq (h (j e22)) e22)) % 78.62/78.85 (Eq (h (j e23)) e23)) % 78.62/78.85 (Eq (h (j e24)) e24)) % 78.62/78.85 (Eq (j (h e10)) e10)) % 78.62/78.85 (Eq (j (h e11)) e11)) % 78.62/78.85 (Eq (j (h e12)) e12)) % 78.62/78.85 (Eq (j (h e13)) e13)) % 78.62/78.85 (Eq (j (h e14)) e14))) % 78.62/78.85 False % 78.62/78.85 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 % 78.62/78.85 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) % 78.62/78.85 (Eq (Eq (j e24) e14) True) % 78.62/78.85 Clause #95 (by clausification #[94]): Or (Eq (Eq (j e24) e14) True) % 78.62/78.85 (Or (Eq (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) True) (Eq (Eq (j e24) e13) True)) % 78.62/78.85 Clause #96 (by clausification #[95]): Or (Eq (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) True) % 78.62/78.85 (Or (Eq (Eq (j e24) e13) True) (Eq (j e24) e14)) % 78.62/78.85 Clause #97 (by clausification #[96]): Or (Eq (Eq (j e24) e13) True) % 78.62/78.85 (Or (Eq (j e24) e14) (Or (Eq (Or (Eq (j e24) e10) (Eq (j e24) e11)) True) (Eq (Eq (j e24) e12) True))) % 78.62/78.85 Clause #98 (by clausification #[97]): Or (Eq (j e24) e14) % 78.62/78.85 (Or (Eq (Or (Eq (j e24) e10) (Eq (j e24) e11)) True) (Or (Eq (Eq (j e24) e12) True) (Eq (j e24) e13))) % 78.62/78.85 Clause #99 (by clausification #[98]): Or (Eq (j e24) e14) % 78.62/78.85 (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)))) % 78.62/78.85 Clause #100 (by clausification #[99]): Or (Eq (j e24) e14) % 78.62/78.85 (Or (Eq (j e24) e13) (Or (Eq (Eq (j e24) e10) True) (Or (Eq (Eq (j e24) e11) True) (Eq (j e24) e12)))) % 78.62/78.85 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)))) % 78.72/78.89 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)))) % 78.72/78.89 Clause #111 (by clausification #[56]): Eq % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) % 78.72/78.89 (Eq (op1 e10 e12) e12)) % 78.72/78.89 (Eq (op1 e10 e13) e13)) % 78.72/78.89 (Eq (op1 e10 e14) e14)) % 78.72/78.89 (Eq (op1 e11 e10) e11)) % 78.72/78.89 (Eq (op1 e11 e11) e10)) % 78.72/78.89 (Eq (op1 e11 e12) e13)) % 78.72/78.89 (Eq (op1 e11 e13) e14)) % 78.72/78.89 (Eq (op1 e11 e14) e12)) % 78.72/78.89 (Eq (op1 e12 e10) e12)) % 78.72/78.89 (Eq (op1 e12 e11) e14)) % 78.72/78.89 (Eq (op1 e12 e12) e10)) % 78.72/78.89 (Eq (op1 e12 e13) e11)) % 78.72/78.89 (Eq (op1 e12 e14) e13)) % 78.72/78.89 (Eq (op1 e13 e10) e13)) % 78.72/78.89 (Eq (op1 e13 e11) e12)) % 78.72/78.89 (Eq (op1 e13 e12) e14)) % 78.72/78.89 (Eq (op1 e13 e13) e10)) % 78.72/78.89 (Eq (op1 e13 e14) e11)) % 78.72/78.89 (Eq (op1 e14 e10) e14)) % 78.72/78.89 (Eq (op1 e14 e11) e13)) % 78.72/78.89 (Eq (op1 e14 e12) e11)) % 78.72/78.89 True % 78.72/78.89 Clause #129 (by clausification #[72]): Eq % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e21)) % 78.72/78.89 (Eq (op2 e20 e22) e22)) % 78.72/78.89 (Eq (op2 e20 e23) e23)) % 78.72/78.89 (Eq (op2 e20 e24) e24)) % 78.72/78.89 (Eq (op2 e21 e20) e21)) % 78.72/78.89 (Eq (op2 e21 e21) e20)) % 78.72/78.89 (Eq (op2 e21 e22) e24)) % 78.72/78.89 (Eq (op2 e21 e23) e22)) % 78.72/78.89 (Eq (op2 e21 e24) e23)) % 78.72/78.89 (Eq (op2 e22 e20) e22)) % 78.72/78.89 (Eq (op2 e22 e21) e24)) % 78.72/78.89 (Eq (op2 e22 e22) e23)) % 78.72/78.89 (Eq (op2 e22 e23) e20)) % 78.72/78.89 (Eq (op2 e22 e24) e21)) % 78.72/78.89 (Eq (op2 e23 e20) e23)) % 78.72/78.89 (Eq (op2 e23 e21) e22)) % 78.72/78.89 (Eq (op2 e23 e22) e21)) % 78.72/78.89 (Eq (op2 e23 e23) e24)) % 78.72/78.89 (Eq (op2 e23 e24) e20)) % 78.72/78.89 (Eq (op2 e24 e20) e24)) % 78.72/78.89 (Eq (op2 e24 e21) e23)) % 78.72/78.89 (Eq (op2 e24 e22) e20)) % 78.72/78.89 True % 78.72/78.89 Clause #146 (by clausification #[91]): Eq % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (And % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e10 % 78.72/78.89 e10)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e10) % 78.72/78.89 (h % 78.72/78.89 e10))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e10 % 78.72/78.89 e11)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e10) % 78.72/78.89 (h % 78.72/78.89 e11)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e10 % 78.72/78.89 e12)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e10) % 78.72/78.89 (h % 78.72/78.89 e12)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e10 % 78.72/78.89 e13)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e10) % 78.72/78.89 (h % 78.72/78.89 e13)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e10 % 78.72/78.89 e14)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e10) % 78.72/78.89 (h % 78.72/78.89 e14)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e11 % 78.72/78.89 e10)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e11) % 78.72/78.89 (h % 78.72/78.89 e10)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 % 78.72/78.89 e11 % 78.72/78.89 e11)) % 78.72/78.89 (op2 % 78.72/78.89 (h % 78.72/78.89 e11) % 78.72/78.89 (h % 78.72/78.89 e11)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 e11 % 78.72/78.89 e12)) % 78.72/78.89 (op2 % 78.72/78.89 (h e11) % 78.72/78.89 (h % 78.72/78.89 e12)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 e11 % 78.72/78.89 e13)) % 78.72/78.89 (op2 (h e11) % 78.72/78.89 (h e13)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 e11 % 78.72/78.89 e14)) % 78.72/78.89 (op2 (h e11) % 78.72/78.89 (h e14)))) % 78.72/78.89 (Eq % 78.72/78.89 (h % 78.72/78.89 (op1 e12 e10)) % 78.72/78.89 (op2 (h e12) % 78.72/78.89 (h e10)))) % 78.72/78.89 (Eq % 78.72/78.89 (h (op1 e12 e11)) % 78.72/78.89 (op2 (h e12) % 78.72/78.89 (h e11)))) % 78.72/78.89 (Eq (h (op1 e12 e12)) % 78.72/78.89 (op2 (h e12) % 78.72/78.89 (h e12)))) % 78.72/78.89 (Eq (h (op1 e12 e13)) % 78.72/78.89 (op2 (h e12) % 78.72/78.89 (h e13)))) % 78.72/78.89 (Eq (h (op1 e12 e14)) % 78.72/78.89 (op2 (h e12) (h e14)))) % 78.72/78.89 (Eq (h (op1 e13 e10)) % 78.72/78.89 (op2 (h e13) (h e10)))) % 78.72/78.89 (Eq (h (op1 e13 e11)) % 78.72/78.89 (op2 (h e13) (h e11)))) % 78.72/78.89 (Eq (h (op1 e13 e12)) % 78.72/78.89 (op2 (h e13) (h e12)))) % 78.72/78.89 (Eq (h (op1 e13 e13)) % 78.72/78.89 (op2 (h e13) (h e13)))) % 78.72/78.89 (Eq (h (op1 e13 e14)) % 78.72/78.89 (op2 (h e13) (h e14)))) % 78.72/78.89 (Eq (h (op1 e14 e10)) % 78.72/78.89 (op2 (h e14) (h e10)))) % 78.72/78.89 (Eq (h (op1 e14 e11)) % 78.72/78.89 (op2 (h e14) (h e11)))) % 78.72/78.89 (Eq (h (op1 e14 e12)) % 78.72/78.89 (op2 (h e14) (h e12)))) % 78.72/78.89 (Eq (h (op1 e14 e13)) % 78.72/78.89 (op2 (h e14) (h e13)))) % 78.72/78.89 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.72/78.89 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.72/78.89 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.72/78.89 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.72/78.89 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.72/78.89 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.72/78.89 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.72/78.89 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.72/78.89 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.72/78.89 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.72/78.89 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.72/78.89 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.72/78.89 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.72/78.89 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.72/78.89 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.72/78.89 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.72/78.89 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.72/78.89 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.72/78.89 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.72/78.89 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.72/78.89 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.72/78.89 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.72/78.89 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.72/78.89 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.74/78.92 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.74/78.92 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.74/78.92 (Eq (h (j e20)) e20)) % 78.74/78.92 (Eq (h (j e21)) e21)) % 78.74/78.92 (Eq (h (j e22)) e22)) % 78.74/78.92 (Eq (h (j e23)) e23)) % 78.74/78.92 (Eq (h (j e24)) e24)) % 78.74/78.92 (Eq (j (h e10)) e10)) % 78.74/78.92 (Eq (j (h e11)) e11)) % 78.74/78.92 (Eq (j (h e12)) e12)) % 78.74/78.92 (Eq (j (h e13)) e13)) % 78.74/78.92 (Eq (j (h e14)) e14)) % 78.74/78.92 True % 78.74/78.92 Clause #147 (by clausification #[146]): Eq (Eq (j (h e14)) e14) True % 78.74/78.92 Clause #148 (by clausification #[146]): Eq % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (And % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 % 78.74/78.92 e10 % 78.74/78.92 e10)) % 78.74/78.92 (op2 % 78.74/78.92 (h % 78.74/78.92 e10) % 78.74/78.92 (h % 78.74/78.92 e10))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 % 78.74/78.92 e10 % 78.74/78.92 e11)) % 78.74/78.92 (op2 % 78.74/78.92 (h % 78.74/78.92 e10) % 78.74/78.92 (h % 78.74/78.92 e11)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 % 78.74/78.92 e10 % 78.74/78.92 e12)) % 78.74/78.92 (op2 % 78.74/78.92 (h % 78.74/78.92 e10) % 78.74/78.92 (h % 78.74/78.92 e12)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 % 78.74/78.92 e10 % 78.74/78.92 e13)) % 78.74/78.92 (op2 % 78.74/78.92 (h % 78.74/78.92 e10) % 78.74/78.92 (h % 78.74/78.92 e13)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 % 78.74/78.92 e10 % 78.74/78.92 e14)) % 78.74/78.92 (op2 % 78.74/78.92 (h % 78.74/78.92 e10) % 78.74/78.92 (h % 78.74/78.92 e14)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 % 78.74/78.92 e11 % 78.74/78.92 e10)) % 78.74/78.92 (op2 % 78.74/78.92 (h % 78.74/78.92 e11) % 78.74/78.92 (h % 78.74/78.92 e10)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 e11 % 78.74/78.92 e11)) % 78.74/78.92 (op2 % 78.74/78.92 (h e11) % 78.74/78.92 (h % 78.74/78.92 e11)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 e11 % 78.74/78.92 e12)) % 78.74/78.92 (op2 (h e11) % 78.74/78.92 (h e12)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 e11 % 78.74/78.92 e13)) % 78.74/78.92 (op2 (h e11) % 78.74/78.92 (h e13)))) % 78.74/78.92 (Eq % 78.74/78.92 (h % 78.74/78.92 (op1 e11 e14)) % 78.74/78.92 (op2 (h e11) % 78.74/78.92 (h e14)))) % 78.74/78.92 (Eq % 78.74/78.92 (h (op1 e12 e10)) % 78.74/78.92 (op2 (h e12) % 78.74/78.92 (h e10)))) % 78.74/78.92 (Eq (h (op1 e12 e11)) % 78.74/78.92 (op2 (h e12) % 78.74/78.92 (h e11)))) % 78.74/78.92 (Eq (h (op1 e12 e12)) % 78.74/78.92 (op2 (h e12) % 78.74/78.92 (h e12)))) % 78.74/78.92 (Eq (h (op1 e12 e13)) % 78.74/78.92 (op2 (h e12) (h e13)))) % 78.74/78.92 (Eq (h (op1 e12 e14)) % 78.74/78.92 (op2 (h e12) (h e14)))) % 78.74/78.92 (Eq (h (op1 e13 e10)) % 78.74/78.92 (op2 (h e13) (h e10)))) % 78.74/78.92 (Eq (h (op1 e13 e11)) % 78.74/78.92 (op2 (h e13) (h e11)))) % 78.74/78.92 (Eq (h (op1 e13 e12)) % 78.74/78.92 (op2 (h e13) (h e12)))) % 78.74/78.92 (Eq (h (op1 e13 e13)) % 78.74/78.92 (op2 (h e13) (h e13)))) % 78.74/78.92 (Eq (h (op1 e13 e14)) % 78.74/78.92 (op2 (h e13) (h e14)))) % 78.74/78.92 (Eq (h (op1 e14 e10)) % 78.74/78.92 (op2 (h e14) (h e10)))) % 78.74/78.92 (Eq (h (op1 e14 e11)) % 78.74/78.92 (op2 (h e14) (h e11)))) % 78.74/78.92 (Eq (h (op1 e14 e12)) % 78.74/78.92 (op2 (h e14) (h e12)))) % 78.74/78.92 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.74/78.92 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.74/78.92 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.74/78.92 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.74/78.92 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.74/78.92 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.74/78.92 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.74/78.92 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.74/78.92 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.74/78.92 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.74/78.92 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.74/78.92 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.74/78.92 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.74/78.92 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.74/78.92 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.74/78.92 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.74/78.92 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.74/78.92 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.74/78.92 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.74/78.92 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.74/78.92 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.74/78.92 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.74/78.92 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.74/78.92 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.74/78.92 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.74/78.92 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.74/78.92 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.74/78.94 (Eq (h (j e20)) e20)) % 78.74/78.94 (Eq (h (j e21)) e21)) % 78.74/78.94 (Eq (h (j e22)) e22)) % 78.74/78.94 (Eq (h (j e23)) e23)) % 78.74/78.94 (Eq (h (j e24)) e24)) % 78.74/78.94 (Eq (j (h e10)) e10)) % 78.74/78.94 (Eq (j (h e11)) e11)) % 78.74/78.94 (Eq (j (h e12)) e12)) % 78.74/78.94 (Eq (j (h e13)) e13)) % 78.74/78.94 True % 78.74/78.94 Clause #149 (by clausification #[147]): Eq (j (h e14)) e14 % 78.74/78.94 Clause #185 (by clausification #[111]): Eq % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.94 (Eq (op1 e10 e13) e13)) % 78.74/78.94 (Eq (op1 e10 e14) e14)) % 78.74/78.94 (Eq (op1 e11 e10) e11)) % 78.74/78.94 (Eq (op1 e11 e11) e10)) % 78.74/78.94 (Eq (op1 e11 e12) e13)) % 78.74/78.94 (Eq (op1 e11 e13) e14)) % 78.74/78.94 (Eq (op1 e11 e14) e12)) % 78.74/78.94 (Eq (op1 e12 e10) e12)) % 78.74/78.94 (Eq (op1 e12 e11) e14)) % 78.74/78.94 (Eq (op1 e12 e12) e10)) % 78.74/78.94 (Eq (op1 e12 e13) e11)) % 78.74/78.94 (Eq (op1 e12 e14) e13)) % 78.74/78.94 (Eq (op1 e13 e10) e13)) % 78.74/78.94 (Eq (op1 e13 e11) e12)) % 78.74/78.94 (Eq (op1 e13 e12) e14)) % 78.74/78.94 (Eq (op1 e13 e13) e10)) % 78.74/78.94 (Eq (op1 e13 e14) e11)) % 78.74/78.94 (Eq (op1 e14 e10) e14)) % 78.74/78.94 (Eq (op1 e14 e11) e13)) % 78.74/78.94 True % 78.74/78.94 Clause #188 (by clausification #[185]): Eq % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.94 (Eq (op1 e10 e13) e13)) % 78.74/78.94 (Eq (op1 e10 e14) e14)) % 78.74/78.94 (Eq (op1 e11 e10) e11)) % 78.74/78.94 (Eq (op1 e11 e11) e10)) % 78.74/78.94 (Eq (op1 e11 e12) e13)) % 78.74/78.94 (Eq (op1 e11 e13) e14)) % 78.74/78.94 (Eq (op1 e11 e14) e12)) % 78.74/78.94 (Eq (op1 e12 e10) e12)) % 78.74/78.94 (Eq (op1 e12 e11) e14)) % 78.74/78.94 (Eq (op1 e12 e12) e10)) % 78.74/78.94 (Eq (op1 e12 e13) e11)) % 78.74/78.94 (Eq (op1 e12 e14) e13)) % 78.74/78.94 (Eq (op1 e13 e10) e13)) % 78.74/78.94 (Eq (op1 e13 e11) e12)) % 78.74/78.94 (Eq (op1 e13 e12) e14)) % 78.74/78.94 (Eq (op1 e13 e13) e10)) % 78.74/78.94 (Eq (op1 e13 e14) e11)) % 78.74/78.94 (Eq (op1 e14 e10) e14)) % 78.74/78.94 True % 78.74/78.94 Clause #190 (by clausification #[188]): Eq (Eq (op1 e14 e10) e14) True % 78.74/78.94 Clause #191 (by clausification #[188]): Eq % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And % 78.74/78.94 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.94 (Eq (op1 e10 e13) e13)) % 78.74/78.94 (Eq (op1 e10 e14) e14)) % 78.74/78.94 (Eq (op1 e11 e10) e11)) % 78.74/78.95 (Eq (op1 e11 e11) e10)) % 78.74/78.95 (Eq (op1 e11 e12) e13)) % 78.74/78.95 (Eq (op1 e11 e13) e14)) % 78.74/78.95 (Eq (op1 e11 e14) e12)) % 78.74/78.95 (Eq (op1 e12 e10) e12)) % 78.74/78.95 (Eq (op1 e12 e11) e14)) % 78.74/78.95 (Eq (op1 e12 e12) e10)) % 78.74/78.95 (Eq (op1 e12 e13) e11)) % 78.74/78.95 (Eq (op1 e12 e14) e13)) % 78.74/78.95 (Eq (op1 e13 e10) e13)) % 78.74/78.95 (Eq (op1 e13 e11) e12)) % 78.74/78.95 (Eq (op1 e13 e12) e14)) % 78.74/78.95 (Eq (op1 e13 e13) e10)) % 78.74/78.95 (Eq (op1 e13 e14) e11)) % 78.74/78.95 True % 78.74/78.95 Clause #192 (by clausification #[190]): Eq (op1 e14 e10) e14 % 78.74/78.95 Clause #194 (by clausification #[191]): Eq % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.95 (Eq (op1 e10 e13) e13)) % 78.74/78.95 (Eq (op1 e10 e14) e14)) % 78.74/78.95 (Eq (op1 e11 e10) e11)) % 78.74/78.95 (Eq (op1 e11 e11) e10)) % 78.74/78.95 (Eq (op1 e11 e12) e13)) % 78.74/78.95 (Eq (op1 e11 e13) e14)) % 78.74/78.95 (Eq (op1 e11 e14) e12)) % 78.74/78.95 (Eq (op1 e12 e10) e12)) % 78.74/78.95 (Eq (op1 e12 e11) e14)) % 78.74/78.95 (Eq (op1 e12 e12) e10)) % 78.74/78.95 (Eq (op1 e12 e13) e11)) % 78.74/78.95 (Eq (op1 e12 e14) e13)) % 78.74/78.95 (Eq (op1 e13 e10) e13)) % 78.74/78.95 (Eq (op1 e13 e11) e12)) % 78.74/78.95 (Eq (op1 e13 e12) e14)) % 78.74/78.95 (Eq (op1 e13 e13) e10)) % 78.74/78.95 True % 78.74/78.95 Clause #196 (by clausification #[194]): Eq (Eq (op1 e13 e13) e10) True % 78.74/78.95 Clause #197 (by clausification #[194]): Eq % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.95 (Eq (op1 e10 e13) e13)) % 78.74/78.95 (Eq (op1 e10 e14) e14)) % 78.74/78.95 (Eq (op1 e11 e10) e11)) % 78.74/78.95 (Eq (op1 e11 e11) e10)) % 78.74/78.95 (Eq (op1 e11 e12) e13)) % 78.74/78.95 (Eq (op1 e11 e13) e14)) % 78.74/78.95 (Eq (op1 e11 e14) e12)) % 78.74/78.95 (Eq (op1 e12 e10) e12)) % 78.74/78.95 (Eq (op1 e12 e11) e14)) % 78.74/78.95 (Eq (op1 e12 e12) e10)) % 78.74/78.95 (Eq (op1 e12 e13) e11)) % 78.74/78.95 (Eq (op1 e12 e14) e13)) % 78.74/78.95 (Eq (op1 e13 e10) e13)) % 78.74/78.95 (Eq (op1 e13 e11) e12)) % 78.74/78.95 (Eq (op1 e13 e12) e14)) % 78.74/78.95 True % 78.74/78.95 Clause #198 (by clausification #[196]): Eq (op1 e13 e13) e10 % 78.74/78.95 Clause #199 (by clausification #[129]): Eq (Eq (op2 e24 e22) e20) True % 78.74/78.95 Clause #201 (by clausification #[199]): Eq (op2 e24 e22) e20 % 78.74/78.95 Clause #203 (by clausification #[197]): Eq % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And % 78.74/78.95 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.95 (Eq (op1 e10 e13) e13)) % 78.74/78.95 (Eq (op1 e10 e14) e14)) % 78.74/78.95 (Eq (op1 e11 e10) e11)) % 78.74/78.95 (Eq (op1 e11 e11) e10)) % 78.74/78.95 (Eq (op1 e11 e12) e13)) % 78.74/78.95 (Eq (op1 e11 e13) e14)) % 78.74/78.95 (Eq (op1 e11 e14) e12)) % 78.74/78.95 (Eq (op1 e12 e10) e12)) % 78.74/78.95 (Eq (op1 e12 e11) e14)) % 78.74/78.95 (Eq (op1 e12 e12) e10)) % 78.74/78.95 (Eq (op1 e12 e13) e11)) % 78.74/78.95 (Eq (op1 e12 e14) e13)) % 78.74/78.99 (Eq (op1 e13 e10) e13)) % 78.74/78.99 (Eq (op1 e13 e11) e12)) % 78.74/78.99 True % 78.74/78.99 Clause #206 (by clausification #[203]): Eq % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.99 (Eq (op1 e10 e13) e13)) % 78.74/78.99 (Eq (op1 e10 e14) e14)) % 78.74/78.99 (Eq (op1 e11 e10) e11)) % 78.74/78.99 (Eq (op1 e11 e11) e10)) % 78.74/78.99 (Eq (op1 e11 e12) e13)) % 78.74/78.99 (Eq (op1 e11 e13) e14)) % 78.74/78.99 (Eq (op1 e11 e14) e12)) % 78.74/78.99 (Eq (op1 e12 e10) e12)) % 78.74/78.99 (Eq (op1 e12 e11) e14)) % 78.74/78.99 (Eq (op1 e12 e12) e10)) % 78.74/78.99 (Eq (op1 e12 e13) e11)) % 78.74/78.99 (Eq (op1 e12 e14) e13)) % 78.74/78.99 (Eq (op1 e13 e10) e13)) % 78.74/78.99 True % 78.74/78.99 Clause #208 (by clausification #[206]): Eq (Eq (op1 e13 e10) e13) True % 78.74/78.99 Clause #209 (by clausification #[206]): Eq % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.99 (Eq (op1 e10 e13) e13)) % 78.74/78.99 (Eq (op1 e10 e14) e14)) % 78.74/78.99 (Eq (op1 e11 e10) e11)) % 78.74/78.99 (Eq (op1 e11 e11) e10)) % 78.74/78.99 (Eq (op1 e11 e12) e13)) % 78.74/78.99 (Eq (op1 e11 e13) e14)) % 78.74/78.99 (Eq (op1 e11 e14) e12)) % 78.74/78.99 (Eq (op1 e12 e10) e12)) % 78.74/78.99 (Eq (op1 e12 e11) e14)) % 78.74/78.99 (Eq (op1 e12 e12) e10)) % 78.74/78.99 (Eq (op1 e12 e13) e11)) % 78.74/78.99 (Eq (op1 e12 e14) e13)) % 78.74/78.99 True % 78.74/78.99 Clause #210 (by clausification #[208]): Eq (op1 e13 e10) e13 % 78.74/78.99 Clause #212 (by clausification #[209]): Eq % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.99 (Eq (op1 e10 e13) e13)) % 78.74/78.99 (Eq (op1 e10 e14) e14)) % 78.74/78.99 (Eq (op1 e11 e10) e11)) % 78.74/78.99 (Eq (op1 e11 e11) e10)) % 78.74/78.99 (Eq (op1 e11 e12) e13)) % 78.74/78.99 (Eq (op1 e11 e13) e14)) % 78.74/78.99 (Eq (op1 e11 e14) e12)) % 78.74/78.99 (Eq (op1 e12 e10) e12)) % 78.74/78.99 (Eq (op1 e12 e11) e14)) % 78.74/78.99 (Eq (op1 e12 e12) e10)) % 78.74/78.99 (Eq (op1 e12 e13) e11)) % 78.74/78.99 True % 78.74/78.99 Clause #215 (by clausification #[212]): Eq % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.74/78.99 (Eq (op1 e10 e13) e13)) % 78.74/78.99 (Eq (op1 e10 e14) e14)) % 78.74/78.99 (Eq (op1 e11 e10) e11)) % 78.74/78.99 (Eq (op1 e11 e11) e10)) % 78.74/78.99 (Eq (op1 e11 e12) e13)) % 78.74/78.99 (Eq (op1 e11 e13) e14)) % 78.74/78.99 (Eq (op1 e11 e14) e12)) % 78.74/78.99 (Eq (op1 e12 e10) e12)) % 78.74/78.99 (Eq (op1 e12 e11) e14)) % 78.74/78.99 (Eq (op1 e12 e12) e10)) % 78.74/78.99 True % 78.74/78.99 Clause #217 (by clausification #[148]): Eq (Eq (j (h e13)) e13) True % 78.74/78.99 Clause #218 (by clausification #[148]): Eq % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (And % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 % 78.74/78.99 e10 % 78.74/78.99 e10)) % 78.74/78.99 (op2 % 78.74/78.99 (h % 78.74/78.99 e10) % 78.74/78.99 (h % 78.74/78.99 e10))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 % 78.74/78.99 e10 % 78.74/78.99 e11)) % 78.74/78.99 (op2 % 78.74/78.99 (h % 78.74/78.99 e10) % 78.74/78.99 (h % 78.74/78.99 e11)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 % 78.74/78.99 e10 % 78.74/78.99 e12)) % 78.74/78.99 (op2 % 78.74/78.99 (h % 78.74/78.99 e10) % 78.74/78.99 (h % 78.74/78.99 e12)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 % 78.74/78.99 e10 % 78.74/78.99 e13)) % 78.74/78.99 (op2 % 78.74/78.99 (h % 78.74/78.99 e10) % 78.74/78.99 (h % 78.74/78.99 e13)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 % 78.74/78.99 e10 % 78.74/78.99 e14)) % 78.74/78.99 (op2 % 78.74/78.99 (h % 78.74/78.99 e10) % 78.74/78.99 (h % 78.74/78.99 e14)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 e11 % 78.74/78.99 e10)) % 78.74/78.99 (op2 % 78.74/78.99 (h e11) % 78.74/78.99 (h % 78.74/78.99 e10)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 e11 % 78.74/78.99 e11)) % 78.74/78.99 (op2 (h e11) % 78.74/78.99 (h e11)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 e11 % 78.74/78.99 e12)) % 78.74/78.99 (op2 (h e11) % 78.74/78.99 (h e12)))) % 78.74/78.99 (Eq % 78.74/78.99 (h % 78.74/78.99 (op1 e11 e13)) % 78.74/78.99 (op2 (h e11) % 78.74/78.99 (h e13)))) % 78.74/78.99 (Eq % 78.74/78.99 (h (op1 e11 e14)) % 78.74/78.99 (op2 (h e11) % 78.74/78.99 (h e14)))) % 78.74/78.99 (Eq (h (op1 e12 e10)) % 78.74/78.99 (op2 (h e12) % 78.74/78.99 (h e10)))) % 78.74/78.99 (Eq (h (op1 e12 e11)) % 78.74/78.99 (op2 (h e12) % 78.74/78.99 (h e11)))) % 78.74/78.99 (Eq (h (op1 e12 e12)) % 78.74/78.99 (op2 (h e12) (h e12)))) % 78.74/78.99 (Eq (h (op1 e12 e13)) % 78.74/78.99 (op2 (h e12) (h e13)))) % 78.74/78.99 (Eq (h (op1 e12 e14)) % 78.74/78.99 (op2 (h e12) (h e14)))) % 78.74/78.99 (Eq (h (op1 e13 e10)) % 78.74/78.99 (op2 (h e13) (h e10)))) % 78.74/78.99 (Eq (h (op1 e13 e11)) % 78.74/78.99 (op2 (h e13) (h e11)))) % 78.74/78.99 (Eq (h (op1 e13 e12)) % 78.74/78.99 (op2 (h e13) (h e12)))) % 78.74/78.99 (Eq (h (op1 e13 e13)) % 78.74/78.99 (op2 (h e13) (h e13)))) % 78.74/78.99 (Eq (h (op1 e13 e14)) % 78.74/78.99 (op2 (h e13) (h e14)))) % 78.74/78.99 (Eq (h (op1 e14 e10)) % 78.74/78.99 (op2 (h e14) (h e10)))) % 78.74/78.99 (Eq (h (op1 e14 e11)) % 78.74/78.99 (op2 (h e14) (h e11)))) % 78.74/78.99 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.74/78.99 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.74/78.99 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.74/78.99 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.74/78.99 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.74/78.99 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.74/78.99 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.74/78.99 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.74/78.99 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.74/78.99 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.74/78.99 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.83/79.00 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.83/79.00 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.83/79.00 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.83/79.00 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.83/79.00 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.83/79.00 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.83/79.00 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.83/79.00 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.83/79.00 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.83/79.00 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.83/79.00 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.83/79.00 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.83/79.00 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.83/79.00 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.83/79.00 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.83/79.00 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.83/79.00 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.83/79.00 (Eq (h (j e20)) e20)) % 78.83/79.00 (Eq (h (j e21)) e21)) % 78.83/79.00 (Eq (h (j e22)) e22)) % 78.83/79.00 (Eq (h (j e23)) e23)) % 78.83/79.00 (Eq (h (j e24)) e24)) % 78.83/79.00 (Eq (j (h e10)) e10)) % 78.83/79.00 (Eq (j (h e11)) e11)) % 78.83/79.00 (Eq (j (h e12)) e12)) % 78.83/79.00 True % 78.83/79.00 Clause #219 (by clausification #[217]): Eq (j (h e13)) e13 % 78.83/79.00 Clause #220 (by clausification #[215]): Eq (Eq (op1 e12 e12) e10) True % 78.83/79.00 Clause #221 (by clausification #[215]): Eq % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.83/79.00 (Eq (op1 e10 e13) e13)) % 78.83/79.00 (Eq (op1 e10 e14) e14)) % 78.83/79.00 (Eq (op1 e11 e10) e11)) % 78.83/79.00 (Eq (op1 e11 e11) e10)) % 78.83/79.00 (Eq (op1 e11 e12) e13)) % 78.83/79.00 (Eq (op1 e11 e13) e14)) % 78.83/79.00 (Eq (op1 e11 e14) e12)) % 78.83/79.00 (Eq (op1 e12 e10) e12)) % 78.83/79.00 (Eq (op1 e12 e11) e14)) % 78.83/79.00 True % 78.83/79.00 Clause #222 (by clausification #[220]): Eq (op1 e12 e12) e10 % 78.83/79.00 Clause #224 (by clausification #[221]): Eq % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.83/79.00 (Eq (op1 e10 e13) e13)) % 78.83/79.00 (Eq (op1 e10 e14) e14)) % 78.83/79.00 (Eq (op1 e11 e10) e11)) % 78.83/79.00 (Eq (op1 e11 e11) e10)) % 78.83/79.00 (Eq (op1 e11 e12) e13)) % 78.83/79.00 (Eq (op1 e11 e13) e14)) % 78.83/79.00 (Eq (op1 e11 e14) e12)) % 78.83/79.00 (Eq (op1 e12 e10) e12)) % 78.83/79.00 True % 78.83/79.00 Clause #226 (by clausification #[224]): Eq (Eq (op1 e12 e10) e12) True % 78.83/79.00 Clause #227 (by clausification #[224]): Eq % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.83/79.00 (Eq (op1 e10 e13) e13)) % 78.83/79.00 (Eq (op1 e10 e14) e14)) % 78.83/79.00 (Eq (op1 e11 e10) e11)) % 78.83/79.00 (Eq (op1 e11 e11) e10)) % 78.83/79.00 (Eq (op1 e11 e12) e13)) % 78.83/79.00 (Eq (op1 e11 e13) e14)) % 78.83/79.00 (Eq (op1 e11 e14) e12)) % 78.83/79.00 True % 78.83/79.00 Clause #228 (by clausification #[226]): Eq (op1 e12 e10) e12 % 78.83/79.00 Clause #230 (by clausification #[227]): Eq % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) % 78.83/79.00 (Eq (op1 e10 e13) e13)) % 78.83/79.00 (Eq (op1 e10 e14) e14)) % 78.83/79.00 (Eq (op1 e11 e10) e11)) % 78.83/79.00 (Eq (op1 e11 e11) e10)) % 78.83/79.00 (Eq (op1 e11 e12) e13)) % 78.83/79.00 (Eq (op1 e11 e13) e14)) % 78.83/79.00 True % 78.83/79.00 Clause #233 (by clausification #[230]): Eq % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.00 (And % 78.83/79.04 (And % 78.83/79.04 (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) (Eq (op1 e10 e13) e13)) % 78.83/79.04 (Eq (op1 e10 e14) e14)) % 78.83/79.04 (Eq (op1 e11 e10) e11)) % 78.83/79.04 (Eq (op1 e11 e11) e10)) % 78.83/79.04 (Eq (op1 e11 e12) e13)) % 78.83/79.04 True % 78.83/79.04 Clause #251 (by clausification #[233]): Eq % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) (Eq (op1 e10 e13) e13)) % 78.83/79.04 (Eq (op1 e10 e14) e14)) % 78.83/79.04 (Eq (op1 e11 e10) e11)) % 78.83/79.04 (Eq (op1 e11 e11) e10)) % 78.83/79.04 True % 78.83/79.04 Clause #256 (by clausification #[251]): Eq (Eq (op1 e11 e11) e10) True % 78.83/79.04 Clause #257 (by clausification #[251]): Eq % 78.83/79.04 (And % 78.83/79.04 (And (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) (Eq (op1 e10 e13) e13)) % 78.83/79.04 (Eq (op1 e10 e14) e14)) % 78.83/79.04 (Eq (op1 e11 e10) e11)) % 78.83/79.04 True % 78.83/79.04 Clause #258 (by clausification #[256]): Eq (op1 e11 e11) e10 % 78.83/79.04 Clause #259 (by clausification #[257]): Eq (Eq (op1 e11 e10) e11) True % 78.83/79.04 Clause #260 (by clausification #[257]): Eq % 78.83/79.04 (And (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) (Eq (op1 e10 e13) e13)) % 78.83/79.04 (Eq (op1 e10 e14) e14)) % 78.83/79.04 True % 78.83/79.04 Clause #261 (by clausification #[259]): Eq (op1 e11 e10) e11 % 78.83/79.04 Clause #263 (by clausification #[260]): Eq (And (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) (Eq (op1 e10 e13) e13)) True % 78.83/79.04 Clause #266 (by clausification #[263]): Eq (And (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) (Eq (op1 e10 e12) e12)) True % 78.83/79.04 Clause #269 (by clausification #[266]): Eq (And (Eq (op1 e10 e10) e10) (Eq (op1 e10 e11) e11)) True % 78.83/79.04 Clause #271 (by clausification #[218]): Eq (Eq (j (h e12)) e12) True % 78.83/79.04 Clause #272 (by clausification #[218]): Eq % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (And % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 % 78.83/79.04 e10 % 78.83/79.04 e10)) % 78.83/79.04 (op2 % 78.83/79.04 (h % 78.83/79.04 e10) % 78.83/79.04 (h % 78.83/79.04 e10))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 % 78.83/79.04 e10 % 78.83/79.04 e11)) % 78.83/79.04 (op2 % 78.83/79.04 (h % 78.83/79.04 e10) % 78.83/79.04 (h % 78.83/79.04 e11)))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 % 78.83/79.04 e10 % 78.83/79.04 e12)) % 78.83/79.04 (op2 % 78.83/79.04 (h % 78.83/79.04 e10) % 78.83/79.04 (h % 78.83/79.04 e12)))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 % 78.83/79.04 e10 % 78.83/79.04 e13)) % 78.83/79.04 (op2 % 78.83/79.04 (h % 78.83/79.04 e10) % 78.83/79.04 (h % 78.83/79.04 e13)))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 e10 % 78.83/79.04 e14)) % 78.83/79.04 (op2 % 78.83/79.04 (h e10) % 78.83/79.04 (h % 78.83/79.04 e14)))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 e11 % 78.83/79.04 e10)) % 78.83/79.04 (op2 (h e11) % 78.83/79.04 (h e10)))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 e11 % 78.83/79.04 e11)) % 78.83/79.04 (op2 (h e11) % 78.83/79.04 (h e11)))) % 78.83/79.04 (Eq % 78.83/79.04 (h % 78.83/79.04 (op1 e11 e12)) % 78.83/79.04 (op2 (h e11) % 78.83/79.04 (h e12)))) % 78.83/79.04 (Eq % 78.83/79.04 (h (op1 e11 e13)) % 78.83/79.04 (op2 (h e11) % 78.83/79.04 (h e13)))) % 78.83/79.04 (Eq (h (op1 e11 e14)) % 78.83/79.04 (op2 (h e11) % 78.83/79.04 (h e14)))) % 78.83/79.04 (Eq (h (op1 e12 e10)) % 78.83/79.04 (op2 (h e12) % 78.83/79.04 (h e10)))) % 78.83/79.04 (Eq (h (op1 e12 e11)) % 78.83/79.04 (op2 (h e12) (h e11)))) % 78.83/79.04 (Eq (h (op1 e12 e12)) % 78.83/79.04 (op2 (h e12) (h e12)))) % 78.83/79.04 (Eq (h (op1 e12 e13)) % 78.83/79.04 (op2 (h e12) (h e13)))) % 78.83/79.04 (Eq (h (op1 e12 e14)) % 78.83/79.04 (op2 (h e12) (h e14)))) % 78.83/79.04 (Eq (h (op1 e13 e10)) % 78.83/79.04 (op2 (h e13) (h e10)))) % 78.83/79.04 (Eq (h (op1 e13 e11)) % 78.83/79.04 (op2 (h e13) (h e11)))) % 78.83/79.04 (Eq (h (op1 e13 e12)) % 78.83/79.04 (op2 (h e13) (h e12)))) % 78.83/79.04 (Eq (h (op1 e13 e13)) % 78.83/79.04 (op2 (h e13) (h e13)))) % 78.83/79.04 (Eq (h (op1 e13 e14)) % 78.83/79.04 (op2 (h e13) (h e14)))) % 78.83/79.04 (Eq (h (op1 e14 e10)) % 78.83/79.04 (op2 (h e14) (h e10)))) % 78.83/79.04 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 78.83/79.04 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.83/79.07 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.83/79.07 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.83/79.07 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.83/79.07 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.83/79.07 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.83/79.07 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.83/79.07 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.83/79.07 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.83/79.07 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.83/79.07 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.83/79.07 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.83/79.07 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.83/79.07 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.83/79.07 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.83/79.07 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.83/79.07 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.83/79.07 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.83/79.07 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.83/79.07 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.83/79.07 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.83/79.07 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.83/79.07 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.83/79.07 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.83/79.07 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.83/79.07 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.83/79.07 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.83/79.07 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.83/79.07 (Eq (h (j e20)) e20)) % 78.83/79.07 (Eq (h (j e21)) e21)) % 78.83/79.07 (Eq (h (j e22)) e22)) % 78.83/79.07 (Eq (h (j e23)) e23)) % 78.83/79.07 (Eq (h (j e24)) e24)) % 78.83/79.07 (Eq (j (h e10)) e10)) % 78.83/79.07 (Eq (j (h e11)) e11)) % 78.83/79.07 True % 78.83/79.07 Clause #273 (by clausification #[271]): Eq (j (h e12)) e12 % 78.83/79.07 Clause #275 (by clausification #[269]): Eq (Eq (op1 e10 e10) e10) True % 78.83/79.07 Clause #277 (by clausification #[275]): Eq (op1 e10 e10) e10 % 78.83/79.07 Clause #305 (by clausification #[272]): Eq (Eq (j (h e11)) e11) True % 78.83/79.07 Clause #306 (by clausification #[272]): Eq % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (And % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 % 78.83/79.07 e10 % 78.83/79.07 e10)) % 78.83/79.07 (op2 % 78.83/79.07 (h % 78.83/79.07 e10) % 78.83/79.07 (h % 78.83/79.07 e10))) % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 % 78.83/79.07 e10 % 78.83/79.07 e11)) % 78.83/79.07 (op2 % 78.83/79.07 (h % 78.83/79.07 e10) % 78.83/79.07 (h % 78.83/79.07 e11)))) % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 % 78.83/79.07 e10 % 78.83/79.07 e12)) % 78.83/79.07 (op2 % 78.83/79.07 (h % 78.83/79.07 e10) % 78.83/79.07 (h % 78.83/79.07 e12)))) % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 e10 % 78.83/79.07 e13)) % 78.83/79.07 (op2 % 78.83/79.07 (h e10) % 78.83/79.07 (h % 78.83/79.07 e13)))) % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 e10 % 78.83/79.07 e14)) % 78.83/79.07 (op2 (h e10) % 78.83/79.07 (h e14)))) % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 e11 % 78.83/79.07 e10)) % 78.83/79.07 (op2 (h e11) % 78.83/79.07 (h e10)))) % 78.83/79.07 (Eq % 78.83/79.07 (h % 78.83/79.07 (op1 e11 e11)) % 78.83/79.07 (op2 (h e11) % 78.83/79.07 (h e11)))) % 78.83/79.07 (Eq % 78.83/79.07 (h (op1 e11 e12)) % 78.83/79.07 (op2 (h e11) % 78.83/79.07 (h e12)))) % 78.83/79.07 (Eq (h (op1 e11 e13)) % 78.83/79.07 (op2 (h e11) % 78.83/79.07 (h e13)))) % 78.83/79.07 (Eq (h (op1 e11 e14)) % 78.83/79.07 (op2 (h e11) % 78.83/79.07 (h e14)))) % 78.83/79.07 (Eq (h (op1 e12 e10)) % 78.83/79.07 (op2 (h e12) (h e10)))) % 78.83/79.07 (Eq (h (op1 e12 e11)) % 78.83/79.07 (op2 (h e12) (h e11)))) % 78.83/79.07 (Eq (h (op1 e12 e12)) % 78.83/79.07 (op2 (h e12) (h e12)))) % 78.83/79.07 (Eq (h (op1 e12 e13)) % 78.83/79.07 (op2 (h e12) (h e13)))) % 78.83/79.07 (Eq (h (op1 e12 e14)) % 78.83/79.07 (op2 (h e12) (h e14)))) % 78.83/79.07 (Eq (h (op1 e13 e10)) % 78.83/79.07 (op2 (h e13) (h e10)))) % 78.83/79.07 (Eq (h (op1 e13 e11)) % 78.83/79.07 (op2 (h e13) (h e11)))) % 78.83/79.07 (Eq (h (op1 e13 e12)) % 78.83/79.07 (op2 (h e13) (h e12)))) % 78.83/79.07 (Eq (h (op1 e13 e13)) % 78.83/79.07 (op2 (h e13) (h e13)))) % 78.83/79.07 (Eq (h (op1 e13 e14)) % 78.83/79.07 (op2 (h e13) (h e14)))) % 78.83/79.07 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 78.83/79.07 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 78.92/79.09 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.92/79.09 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.92/79.09 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.92/79.09 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.92/79.09 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.92/79.09 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.92/79.09 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.92/79.09 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.92/79.09 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.92/79.09 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.92/79.09 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.92/79.09 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.92/79.09 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.92/79.09 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.92/79.09 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.92/79.09 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.92/79.09 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.92/79.09 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.92/79.09 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.92/79.09 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.92/79.09 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.92/79.09 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.92/79.09 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.92/79.09 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.92/79.09 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.92/79.09 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.92/79.09 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.92/79.09 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.92/79.09 (Eq (h (j e20)) e20)) % 78.92/79.09 (Eq (h (j e21)) e21)) % 78.92/79.09 (Eq (h (j e22)) e22)) % 78.92/79.09 (Eq (h (j e23)) e23)) % 78.92/79.09 (Eq (h (j e24)) e24)) % 78.92/79.09 (Eq (j (h e10)) e10)) % 78.92/79.09 True % 78.92/79.09 Clause #307 (by clausification #[305]): Eq (j (h e11)) e11 % 78.92/79.09 Clause #341 (by clausification #[306]): Eq (Eq (j (h e10)) e10) True % 78.92/79.09 Clause #342 (by clausification #[306]): Eq % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (And % 78.92/79.09 (Eq % 78.92/79.09 (h % 78.92/79.09 (op1 % 78.92/79.09 e10 % 78.92/79.09 e10)) % 78.92/79.09 (op2 % 78.92/79.09 (h % 78.92/79.09 e10) % 78.92/79.09 (h % 78.92/79.09 e10))) % 78.92/79.09 (Eq % 78.92/79.09 (h % 78.92/79.09 (op1 % 78.92/79.09 e10 % 78.92/79.09 e11)) % 78.92/79.09 (op2 % 78.92/79.09 (h % 78.92/79.09 e10) % 78.92/79.09 (h % 78.92/79.09 e11)))) % 78.92/79.09 (Eq % 78.92/79.09 (h % 78.92/79.09 (op1 e10 % 78.92/79.09 e12)) % 78.92/79.09 (op2 % 78.92/79.09 (h e10) % 78.92/79.09 (h % 78.92/79.09 e12)))) % 78.92/79.09 (Eq % 78.92/79.09 (h % 78.92/79.09 (op1 e10 % 78.92/79.09 e13)) % 78.92/79.09 (op2 (h e10) % 78.92/79.09 (h e13)))) % 78.92/79.09 (Eq % 78.92/79.09 (h % 78.92/79.09 (op1 e10 % 78.92/79.09 e14)) % 78.92/79.09 (op2 (h e10) % 78.92/79.09 (h e14)))) % 78.92/79.09 (Eq % 78.92/79.09 (h % 78.92/79.09 (op1 e11 e10)) % 78.92/79.09 (op2 (h e11) % 78.92/79.09 (h e10)))) % 78.92/79.09 (Eq % 78.92/79.09 (h (op1 e11 e11)) % 78.92/79.09 (op2 (h e11) % 78.92/79.09 (h e11)))) % 78.92/79.09 (Eq (h (op1 e11 e12)) % 78.92/79.09 (op2 (h e11) % 78.92/79.09 (h e12)))) % 78.92/79.09 (Eq (h (op1 e11 e13)) % 78.92/79.09 (op2 (h e11) % 78.92/79.09 (h e13)))) % 78.92/79.09 (Eq (h (op1 e11 e14)) % 78.92/79.09 (op2 (h e11) (h e14)))) % 78.92/79.09 (Eq (h (op1 e12 e10)) % 78.92/79.09 (op2 (h e12) (h e10)))) % 78.92/79.09 (Eq (h (op1 e12 e11)) % 78.92/79.09 (op2 (h e12) (h e11)))) % 78.92/79.09 (Eq (h (op1 e12 e12)) % 78.92/79.09 (op2 (h e12) (h e12)))) % 78.92/79.09 (Eq (h (op1 e12 e13)) % 78.92/79.09 (op2 (h e12) (h e13)))) % 78.92/79.09 (Eq (h (op1 e12 e14)) % 78.92/79.09 (op2 (h e12) (h e14)))) % 78.92/79.09 (Eq (h (op1 e13 e10)) % 78.92/79.09 (op2 (h e13) (h e10)))) % 78.92/79.09 (Eq (h (op1 e13 e11)) % 78.92/79.09 (op2 (h e13) (h e11)))) % 78.92/79.09 (Eq (h (op1 e13 e12)) % 78.92/79.09 (op2 (h e13) (h e12)))) % 78.92/79.09 (Eq (h (op1 e13 e13)) % 78.92/79.09 (op2 (h e13) (h e13)))) % 78.92/79.09 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 78.92/79.09 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 78.92/79.09 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 78.92/79.09 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.92/79.09 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.92/79.09 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.92/79.09 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.92/79.09 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.92/79.09 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.92/79.09 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.92/79.09 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.92/79.09 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.92/79.09 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.92/79.09 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.92/79.09 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.92/79.09 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.92/79.12 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.92/79.12 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.92/79.12 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.92/79.12 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.92/79.12 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.92/79.12 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.92/79.12 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.92/79.12 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.92/79.12 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.92/79.12 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.92/79.12 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.92/79.12 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.92/79.12 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.92/79.12 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.92/79.12 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.92/79.12 (Eq (h (j e20)) e20)) % 78.92/79.12 (Eq (h (j e21)) e21)) % 78.92/79.12 (Eq (h (j e22)) e22)) % 78.92/79.12 (Eq (h (j e23)) e23)) % 78.92/79.12 (Eq (h (j e24)) e24)) % 78.92/79.12 True % 78.92/79.12 Clause #343 (by clausification #[341]): Eq (j (h e10)) e10 % 78.92/79.12 Clause #375 (by clausification #[342]): Eq (Eq (h (j e24)) e24) True % 78.92/79.12 Clause #376 (by clausification #[342]): Eq % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (And % 78.92/79.12 (Eq % 78.92/79.12 (h % 78.92/79.12 (op1 e10 % 78.92/79.12 e10)) % 78.92/79.12 (op2 % 78.92/79.12 (h e10) % 78.92/79.12 (h % 78.92/79.12 e10))) % 78.92/79.12 (Eq % 78.92/79.12 (h % 78.92/79.12 (op1 e10 % 78.92/79.12 e11)) % 78.92/79.12 (op2 % 78.92/79.12 (h e10) % 78.92/79.12 (h % 78.92/79.12 e11)))) % 78.92/79.12 (Eq % 78.92/79.12 (h % 78.92/79.12 (op1 e10 % 78.92/79.12 e12)) % 78.92/79.12 (op2 (h e10) % 78.92/79.12 (h e12)))) % 78.92/79.12 (Eq % 78.92/79.12 (h % 78.92/79.12 (op1 e10 % 78.92/79.12 e13)) % 78.92/79.12 (op2 (h e10) % 78.92/79.12 (h e13)))) % 78.92/79.12 (Eq % 78.92/79.12 (h % 78.92/79.12 (op1 e10 e14)) % 78.92/79.12 (op2 (h e10) % 78.92/79.12 (h e14)))) % 78.92/79.12 (Eq % 78.92/79.12 (h (op1 e11 e10)) % 78.92/79.12 (op2 (h e11) % 78.92/79.12 (h e10)))) % 78.92/79.12 (Eq (h (op1 e11 e11)) % 78.92/79.12 (op2 (h e11) % 78.92/79.12 (h e11)))) % 78.92/79.12 (Eq (h (op1 e11 e12)) % 78.92/79.12 (op2 (h e11) % 78.92/79.12 (h e12)))) % 78.92/79.12 (Eq (h (op1 e11 e13)) % 78.92/79.12 (op2 (h e11) (h e13)))) % 78.92/79.12 (Eq (h (op1 e11 e14)) % 78.92/79.12 (op2 (h e11) (h e14)))) % 78.92/79.12 (Eq (h (op1 e12 e10)) % 78.92/79.12 (op2 (h e12) (h e10)))) % 78.92/79.12 (Eq (h (op1 e12 e11)) % 78.92/79.12 (op2 (h e12) (h e11)))) % 78.92/79.12 (Eq (h (op1 e12 e12)) % 78.92/79.12 (op2 (h e12) (h e12)))) % 78.92/79.12 (Eq (h (op1 e12 e13)) % 78.92/79.12 (op2 (h e12) (h e13)))) % 78.92/79.12 (Eq (h (op1 e12 e14)) % 78.92/79.12 (op2 (h e12) (h e14)))) % 78.92/79.12 (Eq (h (op1 e13 e10)) % 78.92/79.12 (op2 (h e13) (h e10)))) % 78.92/79.12 (Eq (h (op1 e13 e11)) % 78.92/79.12 (op2 (h e13) (h e11)))) % 78.92/79.12 (Eq (h (op1 e13 e12)) % 78.92/79.12 (op2 (h e13) (h e12)))) % 78.92/79.12 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 78.92/79.12 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 78.92/79.12 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 78.92/79.12 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 78.92/79.12 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.92/79.15 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.92/79.15 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.92/79.15 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.92/79.15 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.92/79.15 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.92/79.15 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.92/79.15 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.92/79.15 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.92/79.15 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.92/79.15 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.92/79.15 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.92/79.15 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.92/79.15 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.92/79.15 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.92/79.15 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.92/79.15 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.92/79.15 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.92/79.15 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.92/79.15 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.92/79.15 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.92/79.15 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.92/79.15 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.92/79.15 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.92/79.15 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.92/79.15 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.92/79.15 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.92/79.15 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.92/79.15 (Eq (h (j e20)) e20)) % 78.92/79.15 (Eq (h (j e21)) e21)) % 78.92/79.15 (Eq (h (j e22)) e22)) % 78.92/79.15 (Eq (h (j e23)) e23)) % 78.92/79.15 True % 78.92/79.15 Clause #377 (by clausification #[375]): Eq (h (j e24)) e24 % 78.92/79.15 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)))) % 78.92/79.15 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)))) % 78.92/79.15 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)))) % 78.92/79.15 Clause #410 (by clausification #[376]): Eq % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (And % 78.92/79.15 (Eq % 78.92/79.15 (h % 78.92/79.15 (op1 e10 % 78.92/79.15 e10)) % 78.92/79.15 (op2 (h e10) % 78.92/79.15 (h e10))) % 78.92/79.15 (Eq % 78.92/79.15 (h % 78.92/79.15 (op1 e10 % 78.92/79.15 e11)) % 78.92/79.15 (op2 (h e10) % 78.92/79.15 (h e11)))) % 78.92/79.15 (Eq % 78.92/79.15 (h % 78.92/79.15 (op1 e10 % 78.92/79.15 e12)) % 78.92/79.15 (op2 (h e10) % 78.92/79.15 (h e12)))) % 78.92/79.15 (Eq % 78.92/79.15 (h % 78.92/79.15 (op1 e10 e13)) % 78.92/79.15 (op2 (h e10) % 78.92/79.15 (h e13)))) % 78.92/79.15 (Eq % 78.92/79.15 (h (op1 e10 e14)) % 78.92/79.15 (op2 (h e10) % 78.92/79.15 (h e14)))) % 78.92/79.15 (Eq (h (op1 e11 e10)) % 78.92/79.15 (op2 (h e11) % 78.92/79.15 (h e10)))) % 78.92/79.15 (Eq (h (op1 e11 e11)) % 78.92/79.15 (op2 (h e11) % 78.92/79.15 (h e11)))) % 78.92/79.15 (Eq (h (op1 e11 e12)) % 78.92/79.15 (op2 (h e11) (h e12)))) % 78.92/79.15 (Eq (h (op1 e11 e13)) % 78.92/79.15 (op2 (h e11) (h e13)))) % 78.92/79.15 (Eq (h (op1 e11 e14)) % 78.92/79.15 (op2 (h e11) (h e14)))) % 78.92/79.15 (Eq (h (op1 e12 e10)) % 78.92/79.15 (op2 (h e12) (h e10)))) % 78.92/79.15 (Eq (h (op1 e12 e11)) % 78.92/79.15 (op2 (h e12) (h e11)))) % 78.92/79.15 (Eq (h (op1 e12 e12)) % 78.92/79.15 (op2 (h e12) (h e12)))) % 78.92/79.15 (Eq (h (op1 e12 e13)) % 78.92/79.15 (op2 (h e12) (h e13)))) % 78.92/79.15 (Eq (h (op1 e12 e14)) % 78.92/79.15 (op2 (h e12) (h e14)))) % 78.92/79.15 (Eq (h (op1 e13 e10)) % 78.92/79.15 (op2 (h e13) (h e10)))) % 78.92/79.15 (Eq (h (op1 e13 e11)) % 78.92/79.15 (op2 (h e13) (h e11)))) % 78.92/79.15 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 78.92/79.15 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 78.92/79.15 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 78.92/79.17 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 78.92/79.17 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 78.92/79.17 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.92/79.17 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.92/79.17 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.92/79.17 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.92/79.17 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.92/79.17 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 78.92/79.17 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 78.92/79.17 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 78.92/79.17 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 78.92/79.17 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 78.92/79.17 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 78.92/79.17 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 78.92/79.17 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 78.92/79.17 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 78.92/79.17 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 78.92/79.17 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 78.92/79.17 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 78.92/79.17 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 78.92/79.17 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 78.92/79.17 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 78.92/79.17 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 78.92/79.17 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 78.92/79.17 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 78.92/79.17 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 78.92/79.17 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 78.92/79.17 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 78.92/79.17 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 78.92/79.17 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 78.92/79.17 (Eq (h (j e20)) e20)) % 78.92/79.17 (Eq (h (j e21)) e21)) % 78.92/79.17 (Eq (h (j e22)) e22)) % 78.92/79.17 True % 78.92/79.17 Clause #465 (by clausification #[410]): Eq (Eq (h (j e22)) e22) True % 78.92/79.17 Clause #466 (by clausification #[410]): Eq % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (And % 78.92/79.17 (Eq % 78.92/79.17 (h % 78.92/79.17 (op1 e10 % 78.92/79.17 e10)) % 78.92/79.17 (op2 (h e10) % 78.92/79.17 (h e10))) % 78.92/79.17 (Eq % 78.92/79.17 (h % 78.92/79.17 (op1 e10 % 78.92/79.17 e11)) % 78.92/79.17 (op2 (h e10) % 78.92/79.17 (h e11)))) % 78.92/79.17 (Eq % 78.92/79.17 (h % 78.92/79.17 (op1 e10 e12)) % 78.92/79.17 (op2 (h e10) % 78.92/79.17 (h e12)))) % 78.92/79.17 (Eq % 78.92/79.17 (h (op1 e10 e13)) % 78.92/79.17 (op2 (h e10) % 78.92/79.17 (h e13)))) % 78.92/79.17 (Eq (h (op1 e10 e14)) % 78.92/79.17 (op2 (h e10) % 78.92/79.17 (h e14)))) % 78.92/79.17 (Eq (h (op1 e11 e10)) % 78.92/79.17 (op2 (h e11) % 78.92/79.17 (h e10)))) % 78.92/79.17 (Eq (h (op1 e11 e11)) % 78.92/79.17 (op2 (h e11) (h e11)))) % 78.92/79.17 (Eq (h (op1 e11 e12)) % 78.92/79.17 (op2 (h e11) (h e12)))) % 78.92/79.17 (Eq (h (op1 e11 e13)) % 78.92/79.17 (op2 (h e11) (h e13)))) % 78.92/79.17 (Eq (h (op1 e11 e14)) % 78.92/79.17 (op2 (h e11) (h e14)))) % 78.92/79.17 (Eq (h (op1 e12 e10)) % 78.92/79.17 (op2 (h e12) (h e10)))) % 78.92/79.17 (Eq (h (op1 e12 e11)) % 78.92/79.17 (op2 (h e12) (h e11)))) % 78.92/79.17 (Eq (h (op1 e12 e12)) % 78.92/79.17 (op2 (h e12) (h e12)))) % 78.92/79.17 (Eq (h (op1 e12 e13)) % 78.92/79.17 (op2 (h e12) (h e13)))) % 78.92/79.17 (Eq (h (op1 e12 e14)) % 78.92/79.17 (op2 (h e12) (h e14)))) % 78.92/79.17 (Eq (h (op1 e13 e10)) % 78.92/79.17 (op2 (h e13) (h e10)))) % 78.92/79.17 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 78.92/79.17 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 78.92/79.17 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 78.92/79.17 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 78.92/79.17 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 78.92/79.17 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 78.92/79.17 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 78.92/79.17 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 78.92/79.17 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 78.92/79.17 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 78.92/79.17 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 78.92/79.17 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 79.01/79.19 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 79.01/79.19 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 79.01/79.19 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 79.01/79.19 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 79.01/79.19 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 79.01/79.19 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 79.01/79.19 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 79.01/79.19 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 79.01/79.19 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 79.01/79.19 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 79.01/79.19 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 79.01/79.19 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 79.01/79.19 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 79.01/79.19 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 79.01/79.19 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 79.01/79.19 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 79.01/79.19 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 79.01/79.19 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 79.01/79.19 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 79.01/79.19 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 79.01/79.19 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 79.01/79.19 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 79.01/79.19 (Eq (h (j e20)) e20)) % 79.01/79.19 (Eq (h (j e21)) e21)) % 79.01/79.19 True % 79.01/79.19 Clause #467 (by clausification #[465]): Eq (h (j e22)) e22 % 79.01/79.19 Clause #591 (by clausification #[466]): Eq % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (And % 79.01/79.19 (Eq % 79.01/79.19 (h % 79.01/79.19 (op1 e10 e10)) % 79.01/79.19 (op2 (h e10) % 79.01/79.19 (h e10))) % 79.01/79.19 (Eq % 79.01/79.19 (h % 79.01/79.19 (op1 e10 e11)) % 79.01/79.19 (op2 (h e10) % 79.01/79.19 (h e11)))) % 79.01/79.19 (Eq % 79.01/79.19 (h (op1 e10 e12)) % 79.01/79.19 (op2 (h e10) % 79.01/79.19 (h e12)))) % 79.01/79.19 (Eq (h (op1 e10 e13)) % 79.01/79.19 (op2 (h e10) % 79.01/79.19 (h e13)))) % 79.01/79.19 (Eq (h (op1 e10 e14)) % 79.01/79.19 (op2 (h e10) % 79.01/79.19 (h e14)))) % 79.01/79.19 (Eq (h (op1 e11 e10)) % 79.01/79.19 (op2 (h e11) (h e10)))) % 79.01/79.19 (Eq (h (op1 e11 e11)) % 79.01/79.20 (op2 (h e11) (h e11)))) % 79.01/79.20 (Eq (h (op1 e11 e12)) % 79.01/79.20 (op2 (h e11) (h e12)))) % 79.01/79.20 (Eq (h (op1 e11 e13)) % 79.01/79.20 (op2 (h e11) (h e13)))) % 79.01/79.20 (Eq (h (op1 e11 e14)) % 79.01/79.20 (op2 (h e11) (h e14)))) % 79.01/79.20 (Eq (h (op1 e12 e10)) % 79.01/79.20 (op2 (h e12) (h e10)))) % 79.04/79.22 (Eq (h (op1 e12 e11)) % 79.04/79.22 (op2 (h e12) (h e11)))) % 79.04/79.22 (Eq (h (op1 e12 e12)) % 79.04/79.22 (op2 (h e12) (h e12)))) % 79.04/79.22 (Eq (h (op1 e12 e13)) % 79.04/79.22 (op2 (h e12) (h e13)))) % 79.04/79.22 (Eq (h (op1 e12 e14)) % 79.04/79.22 (op2 (h e12) (h e14)))) % 79.04/79.22 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 79.04/79.22 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 79.04/79.22 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 79.04/79.22 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 79.04/79.22 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 79.04/79.22 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 79.04/79.22 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 79.04/79.22 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 79.04/79.22 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 79.04/79.22 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 79.04/79.22 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 79.04/79.22 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 79.04/79.22 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 79.04/79.22 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 79.04/79.22 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 79.04/79.22 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 79.04/79.22 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 79.04/79.22 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 79.04/79.22 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 79.04/79.22 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 79.04/79.22 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 79.04/79.22 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 79.04/79.22 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 79.04/79.22 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 79.04/79.22 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 79.04/79.22 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 79.04/79.22 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 79.04/79.22 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 79.04/79.22 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 79.04/79.22 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 79.04/79.22 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 79.04/79.22 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 79.04/79.22 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 79.04/79.22 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 79.04/79.22 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 79.04/79.22 (Eq (h (j e20)) e20)) % 79.04/79.22 True % 79.04/79.22 Clause #900 (by clausification #[591]): Eq (Eq (h (j e20)) e20) True % 79.04/79.22 Clause #901 (by clausification #[591]): Eq % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (And % 79.04/79.22 (Eq % 79.04/79.22 (h (op1 e10 e10)) % 79.04/79.22 (op2 (h e10) % 79.04/79.22 (h e10))) % 79.04/79.22 (Eq % 79.04/79.22 (h (op1 e10 e11)) % 79.04/79.22 (op2 (h e10) % 79.04/79.22 (h e11)))) % 79.04/79.22 (Eq (h (op1 e10 e12)) % 79.04/79.22 (op2 (h e10) % 79.04/79.22 (h e12)))) % 79.04/79.22 (Eq (h (op1 e10 e13)) % 79.04/79.22 (op2 (h e10) % 79.04/79.22 (h e13)))) % 79.04/79.22 (Eq (h (op1 e10 e14)) % 79.04/79.22 (op2 (h e10) (h e14)))) % 79.04/79.22 (Eq (h (op1 e11 e10)) % 79.04/79.22 (op2 (h e11) (h e10)))) % 79.04/79.22 (Eq (h (op1 e11 e11)) % 79.04/79.22 (op2 (h e11) (h e11)))) % 79.04/79.22 (Eq (h (op1 e11 e12)) % 79.04/79.22 (op2 (h e11) (h e12)))) % 79.04/79.22 (Eq (h (op1 e11 e13)) % 79.04/79.22 (op2 (h e11) (h e13)))) % 79.04/79.22 (Eq (h (op1 e11 e14)) % 79.04/79.22 (op2 (h e11) (h e14)))) % 79.04/79.22 (Eq (h (op1 e12 e10)) % 79.04/79.22 (op2 (h e12) (h e10)))) % 79.04/79.22 (Eq (h (op1 e12 e11)) % 79.04/79.22 (op2 (h e12) (h e11)))) % 79.04/79.22 (Eq (h (op1 e12 e12)) % 79.04/79.22 (op2 (h e12) (h e12)))) % 79.04/79.22 (Eq (h (op1 e12 e13)) % 79.04/79.22 (op2 (h e12) (h e13)))) % 79.04/79.22 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 79.04/79.22 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 79.04/79.22 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 79.04/79.22 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 79.04/79.22 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 79.04/79.22 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 79.04/79.22 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 79.04/79.22 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 79.04/79.22 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 79.04/79.22 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 79.04/79.22 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 79.04/79.22 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 79.04/79.22 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 79.04/79.22 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 79.04/79.22 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 79.04/79.22 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 79.04/79.22 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 79.04/79.22 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 79.06/79.24 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 79.06/79.24 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 79.06/79.24 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 79.06/79.24 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 79.06/79.24 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 79.06/79.24 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 79.06/79.24 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 79.06/79.24 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 79.06/79.24 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 79.06/79.24 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 79.06/79.24 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 79.06/79.24 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 79.06/79.24 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 79.06/79.24 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 79.06/79.24 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 79.06/79.24 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 79.06/79.24 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 79.06/79.24 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 79.06/79.24 True % 79.06/79.24 Clause #902 (by clausification #[900]): Eq (h (j e20)) e20 % 79.06/79.24 Clause #1925 (by clausification #[901]): Eq (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24))) True % 79.06/79.24 Clause #1926 (by clausification #[901]): Eq % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (And % 79.06/79.24 (Eq (h (op1 e10 e10)) % 79.06/79.24 (op2 (h e10) % 79.06/79.24 (h e10))) % 79.06/79.24 (Eq (h (op1 e10 e11)) % 79.06/79.24 (op2 (h e10) % 79.06/79.24 (h e11)))) % 79.06/79.24 (Eq (h (op1 e10 e12)) % 79.06/79.24 (op2 (h e10) % 79.06/79.24 (h e12)))) % 79.06/79.24 (Eq (h (op1 e10 e13)) % 79.06/79.24 (op2 (h e10) (h e13)))) % 79.06/79.24 (Eq (h (op1 e10 e14)) % 79.06/79.24 (op2 (h e10) (h e14)))) % 79.06/79.24 (Eq (h (op1 e11 e10)) % 79.06/79.24 (op2 (h e11) (h e10)))) % 79.06/79.24 (Eq (h (op1 e11 e11)) % 79.06/79.24 (op2 (h e11) (h e11)))) % 79.06/79.24 (Eq (h (op1 e11 e12)) % 79.06/79.24 (op2 (h e11) (h e12)))) % 79.06/79.24 (Eq (h (op1 e11 e13)) % 79.06/79.24 (op2 (h e11) (h e13)))) % 79.06/79.24 (Eq (h (op1 e11 e14)) % 79.06/79.24 (op2 (h e11) (h e14)))) % 79.06/79.24 (Eq (h (op1 e12 e10)) % 79.06/79.24 (op2 (h e12) (h e10)))) % 79.06/79.24 (Eq (h (op1 e12 e11)) % 79.06/79.24 (op2 (h e12) (h e11)))) % 79.06/79.24 (Eq (h (op1 e12 e12)) % 79.06/79.24 (op2 (h e12) (h e12)))) % 79.06/79.24 (Eq (h (op1 e12 e13)) (op2 (h e12) (h e13)))) % 79.06/79.24 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 79.06/79.24 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 79.06/79.24 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 79.06/79.24 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 79.06/79.24 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 79.06/79.24 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 79.06/79.24 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 79.06/79.26 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 79.06/79.26 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 79.06/79.26 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 79.06/79.26 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 79.06/79.26 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 79.06/79.26 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 79.06/79.26 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 79.06/79.26 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 79.06/79.26 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 79.06/79.26 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 79.06/79.26 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 79.06/79.26 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 79.06/79.26 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 79.06/79.26 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 79.06/79.26 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 79.06/79.26 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 79.06/79.26 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 79.06/79.26 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 79.06/79.26 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 79.06/79.26 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 79.06/79.26 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 79.06/79.26 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 79.06/79.26 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 79.06/79.26 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 79.06/79.26 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 79.06/79.26 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 79.06/79.26 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 79.06/79.26 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 79.06/79.26 True % 79.06/79.26 Clause #1927 (by clausification #[1925]): Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)) % 79.06/79.26 Clause #1928 (by forward demodulation #[1927, 73]): Eq (j e22) (op1 (j e24) (j e24)) % 79.06/79.26 Clause #1930 (by superposition #[1928, 378]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (j e22) (op1 e10 e10))))) % 79.06/79.26 Clause #2098 (by superposition #[1930, 277]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (j e22) e10)))) % 79.06/79.26 Clause #2099 (by superposition #[2098, 467]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e10) e22)))) % 79.06/79.26 Clause #2121 (by superposition #[2099, 1928]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (j e22) (op1 e12 e12))))) % 79.06/79.26 Clause #2179 (by superposition #[2121, 222]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (j e22) e10)))) % 79.06/79.26 Clause #2187 (by superposition #[2179, 467]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (h e10) e22)))) % 79.06/79.26 Clause #2199 (by eliminate duplicate literals #[2187]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e10) e22))) % 79.06/79.26 Clause #2208 (by superposition #[2199, 1928]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (j e22) (op1 e14 e14)))) % 79.06/79.26 Clause #2326 (by superposition #[2208, 57]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (j e22) e10))) % 79.06/79.26 Clause #2327 (by superposition #[2326, 467]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (h e10) e22))) % 79.06/79.26 Clause #2338 (by eliminate duplicate literals #[2327]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e10) e22)) % 79.06/79.26 Clause #2346 (by superposition #[2338, 1928]): Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (j e22) (op1 e11 e11))) % 79.06/79.26 Clause #2408 (by superposition #[2346, 258]): Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (j e22) e10)) % 79.06/79.29 Clause #2409 (by superposition #[2408, 467]): Or (Eq (h e13) e24) (Or (Eq (h e10) e22) (Eq (h e10) e22)) % 79.06/79.29 Clause #2420 (by eliminate duplicate literals #[2409]): Or (Eq (h e13) e24) (Eq (h e10) e22) % 79.06/79.29 Clause #2421 (by superposition #[2420, 219]): Or (Eq (h e10) e22) (Eq (j e24) e13) % 79.06/79.29 Clause #2436 (by superposition #[2421, 1928]): Or (Eq (h e10) e22) (Eq (j e22) (op1 e13 e13)) % 79.06/79.29 Clause #2437 (by superposition #[2436, 198]): Or (Eq (h e10) e22) (Eq (j e22) e10) % 79.06/79.29 Clause #2438 (by superposition #[2437, 467]): Or (Eq (h e10) e22) (Eq (h e10) e22) % 79.06/79.29 Clause #2448 (by eliminate duplicate literals #[2438]): Eq (h e10) e22 % 79.06/79.29 Clause #2449 (by backward demodulation #[2448, 343]): Eq (j e22) e10 % 79.06/79.29 Clause #2450 (by backward demodulation #[2448, 379]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq e22 e24)))) % 79.06/79.29 Clause #2451 (by backward demodulation #[2448, 383]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq e22 e24) (Eq (h e12) e24)))) % 79.06/79.29 Clause #2633 (by forward contextual literal cutting #[2451, 11]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e12) e24))) % 79.06/79.29 Clause #2711 (by forward contextual literal cutting #[2450, 11]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Eq (h e13) e24))) % 79.06/79.29 Clause #4805 (by clausification #[1926]): Eq % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (And % 79.06/79.29 (Eq (h (op1 e10 e10)) % 79.06/79.29 (op2 (h e10) (h e10))) % 79.06/79.29 (Eq (h (op1 e10 e11)) % 79.06/79.29 (op2 (h e10) % 79.06/79.29 (h e11)))) % 79.06/79.29 (Eq (h (op1 e10 e12)) % 79.06/79.29 (op2 (h e10) (h e12)))) % 79.06/79.29 (Eq (h (op1 e10 e13)) % 79.06/79.29 (op2 (h e10) (h e13)))) % 79.06/79.29 (Eq (h (op1 e10 e14)) % 79.06/79.29 (op2 (h e10) (h e14)))) % 79.06/79.29 (Eq (h (op1 e11 e10)) % 79.06/79.29 (op2 (h e11) (h e10)))) % 79.06/79.29 (Eq (h (op1 e11 e11)) % 79.06/79.29 (op2 (h e11) (h e11)))) % 79.06/79.29 (Eq (h (op1 e11 e12)) % 79.06/79.29 (op2 (h e11) (h e12)))) % 79.06/79.29 (Eq (h (op1 e11 e13)) % 79.06/79.29 (op2 (h e11) (h e13)))) % 79.06/79.29 (Eq (h (op1 e11 e14)) % 79.06/79.29 (op2 (h e11) (h e14)))) % 79.06/79.29 (Eq (h (op1 e12 e10)) % 79.06/79.29 (op2 (h e12) (h e10)))) % 79.06/79.29 (Eq (h (op1 e12 e11)) % 79.06/79.29 (op2 (h e12) (h e11)))) % 79.06/79.29 (Eq (h (op1 e12 e12)) (op2 (h e12) (h e12)))) % 79.06/79.29 (Eq (h (op1 e12 e13)) (op2 (h e12) (h e13)))) % 79.06/79.29 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 79.06/79.29 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 79.06/79.29 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 79.06/79.29 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 79.06/79.29 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 79.06/79.29 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 79.06/79.29 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 79.06/79.29 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 79.06/79.29 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 79.06/79.29 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 79.06/79.29 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 79.06/79.29 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 79.06/79.29 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 79.13/79.30 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 79.13/79.30 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 79.13/79.30 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 79.13/79.30 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 79.13/79.30 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 79.13/79.30 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 79.13/79.30 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 79.13/79.30 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 79.13/79.30 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 79.13/79.30 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 79.13/79.30 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 79.13/79.30 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 79.13/79.30 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 79.13/79.30 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 79.13/79.30 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 79.13/79.30 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 79.13/79.30 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 79.13/79.30 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 79.13/79.30 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 79.13/79.30 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 79.13/79.30 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 79.13/79.30 True % 79.13/79.30 Clause #4855 (by clausification #[4805]): Eq (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22))) True % 79.13/79.30 Clause #4857 (by clausification #[4855]): Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)) % 79.13/79.30 Clause #4858 (by forward demodulation #[4857, 201]): Eq (j e20) (op1 (j e24) (j e22)) % 79.13/79.30 Clause #4859 (by forward demodulation #[4858, 2449]): Eq (j e20) (op1 (j e24) e10) % 79.13/79.30 Clause #4862 (by superposition #[4859, 2633]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq (j e20) (op1 e14 e10)))) % 79.13/79.30 Clause #4864 (by superposition #[4859, 2711]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (j e20) (op1 e12 e10)))) % 79.13/79.30 Clause #4865 (by superposition #[4864, 228]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (j e20) e12))) % 79.13/79.30 Clause #4868 (by superposition #[4865, 902]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e12) e20))) % 79.13/79.30 Clause #4876 (by superposition #[4868, 377]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Eq (h e14) e24))) % 79.13/79.30 Clause #4884 (by superposition #[4868, 4859]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Eq (j e20) (op1 e14 e10)))) % 79.13/79.30 Clause #4886 (by superposition #[4876, 377]): Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Eq (h e11) e24))) % 79.13/79.30 Clause #4893 (by superposition #[4876, 4859]): Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Eq (j e20) (op1 e11 e10)))) % 79.13/79.30 Clause #4926 (by superposition #[4884, 192]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Eq (j e20) e14))) % 79.13/79.30 Clause #5065 (by superposition #[4893, 261]): Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Eq (j e20) e11))) % 79.13/79.30 Clause #5069 (by superposition #[5065, 902]): Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Eq (h e11) e20))) % 79.13/79.30 Clause #5091 (by superposition #[5069, 219]): Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Eq (j e24) e13))) % 79.13/79.30 Clause #5105 (by superposition #[5091, 4859]): Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Eq (j e20) (op1 e13 e10)))) % 79.13/79.30 Clause #5115 (by superposition #[5105, 210]): Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Eq (j e20) e13))) % 79.13/79.30 Clause #5127 (by superposition #[5115, 902]): Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Eq (h e13) e20))) % 79.13/79.30 Clause #5154 (by superposition #[5127, 4886]): Or (Eq (h e12) e20) % 79.13/79.30 (Or (Eq (h e14) e24) % 79.13/79.30 (Or (Eq (h e11) e20) (Or (Eq e20 e24) (Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Eq (h e11) e24)))))) % 79.13/79.30 Clause #5326 (by superposition #[4862, 192]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq (j e20) e14))) % 79.13/79.33 Clause #5329 (by superposition #[5326, 902]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq (h e14) e20))) % 79.13/79.33 Clause #5345 (by superposition #[5329, 377]): Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Eq (h e11) e24))) % 79.13/79.33 Clause #5352 (by superposition #[5329, 4859]): Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Eq (j e20) (op1 e11 e10)))) % 79.13/79.33 Clause #5364 (by superposition #[5345, 219]): Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Eq (j e24) e13))) % 79.13/79.33 Clause #5382 (by superposition #[5364, 4859]): Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Eq (j e20) (op1 e13 e10)))) % 79.13/79.33 Clause #5394 (by superposition #[5352, 261]): Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Eq (j e20) e11))) % 79.13/79.33 Clause #5398 (by superposition #[5394, 902]): Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Eq (h e11) e20))) % 79.13/79.33 Clause #5479 (by superposition #[5382, 210]): Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Eq (j e20) e13))) % 79.13/79.33 Clause #5482 (by superposition #[5479, 902]): Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Eq (h e13) e20))) % 79.13/79.33 Clause #5518 (by superposition #[5482, 5398]): Or (Eq (h e12) e24) % 79.13/79.33 (Or (Eq (h e14) e20) % 79.13/79.33 (Or (Eq (h e11) e24) (Or (Eq e20 e24) (Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Eq (h e11) e20)))))) % 79.13/79.33 Clause #6113 (by eliminate duplicate literals #[5518]): Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Or (Eq e20 e24) (Eq (h e11) e20)))) % 79.13/79.33 Clause #6114 (by forward contextual literal cutting #[6113, 29]): Or (Eq (h e12) e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Eq (h e11) e20))) % 79.13/79.33 Clause #7424 (by eliminate duplicate literals #[5154]): Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq e20 e24) (Eq (h e11) e24)))) % 79.13/79.33 Clause #7425 (by forward contextual literal cutting #[7424, 29]): Or (Eq (h e12) e20) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Eq (h e11) e24))) % 79.13/79.33 Clause #7426 (by superposition #[7425, 273]): Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (j e20) e12))) % 79.13/79.33 Clause #7432 (by superposition #[7425, 6114]): Or (Eq (h e14) e24) % 79.13/79.33 (Or (Eq (h e11) e20) % 79.13/79.33 (Or (Eq (h e11) e24) (Or (Eq e20 e24) (Or (Eq (h e14) e20) (Or (Eq (h e11) e24) (Eq (h e11) e20)))))) % 79.13/79.33 Clause #7466 (by eliminate duplicate literals #[7432]): Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Or (Eq e20 e24) (Eq (h e14) e20)))) % 79.13/79.33 Clause #7467 (by forward contextual literal cutting #[7466, 29]): Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (h e14) e20))) % 79.13/79.33 Clause #7468 (by superposition #[7467, 149]): Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (j e20) e14))) % 79.13/79.33 Clause #7500 (by superposition #[7468, 7426]): Or (Eq (h e14) e24) % 79.13/79.33 (Or (Eq (h e11) e20) % 79.13/79.33 (Or (Eq (h e11) e24) (Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq e14 e12)))))) % 79.13/79.33 Clause #7503 (by eliminate duplicate literals #[7500]): Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq e14 e12))) % 79.13/79.33 Clause #7504 (by forward contextual literal cutting #[7503, 42]): Or (Eq (h e14) e24) (Or (Eq (h e11) e20) (Eq (h e11) e24)) % 79.13/79.33 Clause #7505 (by superposition #[7504, 149]): Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (j e24) e14)) % 79.13/79.33 Clause #7515 (by superposition #[7505, 4859]): Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (j e20) (op1 e14 e10))) % 79.13/79.33 Clause #7546 (by superposition #[7515, 192]): Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (j e20) e14)) % 79.13/79.33 Clause #7549 (by superposition #[7546, 902]): Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq (h e14) e20)) % 79.13/79.33 Clause #7567 (by superposition #[7549, 7504]): Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Or (Eq e20 e24) (Or (Eq (h e11) e20) (Eq (h e11) e24)))) % 79.13/79.33 Clause #7593 (by eliminate duplicate literals #[7567]): Or (Eq (h e11) e20) (Or (Eq (h e11) e24) (Eq e20 e24)) % 79.13/79.33 Clause #7594 (by forward contextual literal cutting #[7593, 29]): Or (Eq (h e11) e20) (Eq (h e11) e24) % 79.13/79.33 Clause #7595 (by superposition #[7594, 307]): Or (Eq (h e11) e24) (Eq (j e20) e11) % 79.13/79.33 Clause #7606 (by superposition #[7595, 4926]): Or (Eq (h e11) e24) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Eq e11 e14)))) % 79.20/79.37 Clause #7623 (by forward contextual literal cutting #[7606, 48]): Or (Eq (h e11) e24) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e12) e20))) % 79.20/79.37 Clause #7624 (by superposition #[7623, 377]): Or (Eq (h e11) e24) (Or (Eq (h e13) e24) (Or (Eq (h e12) e20) (Eq (h e11) e24))) % 79.20/79.37 Clause #7651 (by eliminate duplicate literals #[7624]): Or (Eq (h e11) e24) (Or (Eq (h e13) e24) (Eq (h e12) e20)) % 79.20/79.37 Clause #7652 (by superposition #[7651, 219]): Or (Eq (h e11) e24) (Or (Eq (h e12) e20) (Eq (j e24) e13)) % 79.20/79.37 Clause #7673 (by superposition #[7652, 4859]): Or (Eq (h e11) e24) (Or (Eq (h e12) e20) (Eq (j e20) (op1 e13 e10))) % 79.20/79.37 Clause #7703 (by superposition #[7673, 210]): Or (Eq (h e11) e24) (Or (Eq (h e12) e20) (Eq (j e20) e13)) % 79.20/79.37 Clause #7727 (by superposition #[7703, 7595]): Or (Eq (h e11) e24) (Or (Eq (h e12) e20) (Or (Eq (h e11) e24) (Eq e13 e11))) % 79.20/79.37 Clause #7747 (by eliminate duplicate literals #[7727]): Or (Eq (h e11) e24) (Or (Eq (h e12) e20) (Eq e13 e11)) % 79.20/79.37 Clause #7748 (by forward contextual literal cutting #[7747, 51]): Or (Eq (h e11) e24) (Eq (h e12) e20) % 79.20/79.37 Clause #7749 (by superposition #[7748, 273]): Or (Eq (h e11) e24) (Eq (j e20) e12) % 79.20/79.37 Clause #7782 (by superposition #[7749, 7595]): Or (Eq (h e11) e24) (Or (Eq (h e11) e24) (Eq e12 e11)) % 79.20/79.37 Clause #7783 (by eliminate duplicate literals #[7782]): Or (Eq (h e11) e24) (Eq e12 e11) % 79.20/79.37 Clause #7784 (by forward contextual literal cutting #[7783, 54]): Eq (h e11) e24 % 79.20/79.37 Clause #7785 (by backward demodulation #[7784, 307]): Eq (j e24) e11 % 79.20/79.37 Clause #7894 (by backward demodulation #[7785, 4859]): Eq (j e20) (op1 e11 e10) % 79.20/79.37 Clause #7950 (by superposition #[7894, 261]): Eq (j e20) e11 % 79.20/79.37 Clause #7952 (by backward demodulation #[7950, 902]): Eq (h e11) e20 % 79.20/79.37 Clause #7961 (by superposition #[7952, 7784]): Eq e20 e24 % 79.20/79.37 Clause #7962 (by forward contextual literal cutting #[7961, 29]): False % 79.20/79.37 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------