%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG181+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:44:05 PM UTC 2025 % Result : Theorem 56.53s 56.70s % Output : Proof 57.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG181+1 : TPTP v9.2.0. Released v2.7.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n024.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 09:17:53 EDT 2025 % 0.14/0.35 % CPUTime : % 56.53/56.70 SZS status Theorem for theBenchmark.p % 56.53/56.70 SZS output start Proof for theBenchmark.p % 56.53/56.70 Clause #0 (by assumption #[]): Eq % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.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)) % 56.53/56.70 (Ne e11 e14)) % 56.53/56.70 (Ne e12 e13)) % 56.53/56.70 (Ne e12 e14)) % 56.53/56.70 (Ne e13 e14)) % 56.53/56.70 True % 56.53/56.70 Clause #1 (by assumption #[]): Eq % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.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)) % 56.53/56.70 (Ne e21 e24)) % 56.53/56.70 (Ne e22 e23)) % 56.53/56.70 (Ne e22 e24)) % 56.53/56.70 (Ne e23 e24)) % 56.53/56.70 True % 56.53/56.70 Clause #3 (by assumption #[]): Eq % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) % 56.53/56.70 (Eq (op1 e10 e12) e10)) % 56.53/56.70 (Eq (op1 e10 e13) e11)) % 56.53/56.70 (Eq (op1 e10 e14) e14)) % 56.53/56.70 (Eq (op1 e11 e10) e10)) % 56.53/56.70 (Eq (op1 e11 e11) e14)) % 56.53/56.70 (Eq (op1 e11 e12) e11)) % 56.53/56.70 (Eq (op1 e11 e13) e12)) % 56.53/56.70 (Eq (op1 e11 e14) e13)) % 56.53/56.70 (Eq (op1 e12 e10) e11)) % 56.53/56.70 (Eq (op1 e12 e11) e13)) % 56.53/56.70 (Eq (op1 e12 e12) e12)) % 56.53/56.70 (Eq (op1 e12 e13) e14)) % 56.53/56.70 (Eq (op1 e12 e14) e10)) % 56.53/56.70 (Eq (op1 e13 e10) e14)) % 56.53/56.70 (Eq (op1 e13 e11) e11)) % 56.53/56.70 (Eq (op1 e13 e12) e13)) % 56.53/56.70 (Eq (op1 e13 e13) e10)) % 56.53/56.70 (Eq (op1 e13 e14) e12)) % 56.53/56.70 (Eq (op1 e14 e10) e12)) % 56.53/56.70 (Eq (op1 e14 e11) e10)) % 56.53/56.70 (Eq (op1 e14 e12) e14)) % 56.53/56.70 (Eq (op1 e14 e13) e13)) % 56.53/56.70 (Eq (op1 e14 e14) e11)) % 56.53/56.70 True % 56.53/56.70 Clause #4 (by assumption #[]): Eq % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And % 56.53/56.70 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e23)) % 56.53/56.70 (Eq (op2 e20 e22) e24)) % 56.53/56.70 (Eq (op2 e20 e23) e21)) % 56.53/56.70 (Eq (op2 e20 e24) e22)) % 56.53/56.70 (Eq (op2 e21 e20) e24)) % 56.53/56.70 (Eq (op2 e21 e21) e21)) % 56.53/56.70 (Eq (op2 e21 e22) e23)) % 56.53/56.70 (Eq (op2 e21 e23) e22)) % 56.53/56.70 (Eq (op2 e21 e24) e20)) % 56.53/56.70 (Eq (op2 e22 e20) e21)) % 56.53/56.70 (Eq (op2 e22 e21) e20)) % 56.53/56.70 (Eq (op2 e22 e22) e22)) % 56.53/56.70 (Eq (op2 e22 e23) e24)) % 56.53/56.70 (Eq (op2 e22 e24) e23)) % 56.53/56.70 (Eq (op2 e23 e20) e22)) % 56.53/56.73 (Eq (op2 e23 e21) e24)) % 56.53/56.73 (Eq (op2 e23 e22) e20)) % 56.53/56.73 (Eq (op2 e23 e23) e23)) % 56.53/56.73 (Eq (op2 e23 e24) e21)) % 56.53/56.73 (Eq (op2 e24 e20) e23)) % 56.53/56.73 (Eq (op2 e24 e21) e22)) % 56.53/56.73 (Eq (op2 e24 e22) e21)) % 56.53/56.73 (Eq (op2 e24 e23) e20)) % 56.53/56.73 (Eq (op2 e24 e24) e24)) % 56.53/56.73 True % 56.53/56.73 Clause #5 (by assumption #[]): Eq % 56.53/56.73 (Not % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 56.53/56.73 (Eq (h e10) e24)) % 56.53/56.73 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 56.53/56.73 (Eq (h e11) e24))) % 56.53/56.73 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 56.53/56.73 (Eq (h e12) e24))) % 56.53/56.73 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 56.53/56.73 (Eq (h e13) e24))) % 56.53/56.73 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) % 56.53/56.73 (Eq (h e14) e24))) % 56.53/56.73 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) % 56.53/56.73 (Eq (j e20) e14))) % 56.53/56.73 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 56.53/56.73 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 56.53/56.73 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 56.53/56.73 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) → % 56.53/56.73 Not % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.73 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e10 % 56.53/56.74 e10)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e10) % 56.53/56.74 (h % 56.53/56.74 e10))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e10 % 56.53/56.74 e11)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e10) % 56.53/56.74 (h % 56.53/56.74 e11)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e10 % 56.53/56.74 e12)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e10) % 56.53/56.74 (h % 56.53/56.74 e12)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e10 % 56.53/56.74 e13)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e10) % 56.53/56.74 (h % 56.53/56.74 e13)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e10 % 56.53/56.74 e14)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e10) % 56.53/56.74 (h % 56.53/56.74 e14)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e11 % 56.53/56.74 e10)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e11) % 56.53/56.74 (h % 56.53/56.74 e10)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e11 % 56.53/56.74 e11)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e11) % 56.53/56.74 (h % 56.53/56.74 e11)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e11 % 56.53/56.74 e12)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e11) % 56.53/56.74 (h % 56.53/56.74 e12)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e11 % 56.53/56.74 e13)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e11) % 56.53/56.74 (h % 56.53/56.74 e13)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 % 56.53/56.74 e11 % 56.53/56.74 e14)) % 56.53/56.74 (op2 % 56.53/56.74 (h % 56.53/56.74 e11) % 56.53/56.74 (h % 56.53/56.74 e14)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 e12 % 56.53/56.74 e10)) % 56.53/56.74 (op2 % 56.53/56.74 (h e12) % 56.53/56.74 (h % 56.53/56.74 e10)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 e12 % 56.53/56.74 e11)) % 56.53/56.74 (op2 (h e12) % 56.53/56.74 (h e11)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 e12 % 56.53/56.74 e12)) % 56.53/56.74 (op2 (h e12) % 56.53/56.74 (h e12)))) % 56.53/56.74 (Eq % 56.53/56.74 (h % 56.53/56.74 (op1 e12 e13)) % 56.53/56.74 (op2 (h e12) % 56.53/56.74 (h e13)))) % 56.53/56.74 (Eq % 56.53/56.74 (h (op1 e12 e14)) % 56.53/56.74 (op2 (h e12) % 56.53/56.74 (h e14)))) % 56.53/56.74 (Eq (h (op1 e13 e10)) % 56.53/56.74 (op2 (h e13) % 56.53/56.74 (h e10)))) % 56.53/56.74 (Eq (h (op1 e13 e11)) % 56.53/56.74 (op2 (h e13) % 56.53/56.74 (h e11)))) % 56.53/56.74 (Eq (h (op1 e13 e12)) % 56.53/56.74 (op2 (h e13) (h e12)))) % 56.53/56.74 (Eq (h (op1 e13 e13)) % 56.53/56.74 (op2 (h e13) (h e13)))) % 56.53/56.74 (Eq (h (op1 e13 e14)) % 56.53/56.74 (op2 (h e13) (h e14)))) % 56.53/56.74 (Eq (h (op1 e14 e10)) % 56.53/56.74 (op2 (h e14) (h e10)))) % 56.53/56.74 (Eq (h (op1 e14 e11)) % 56.53/56.74 (op2 (h e14) (h e11)))) % 56.53/56.74 (Eq (h (op1 e14 e12)) % 56.53/56.74 (op2 (h e14) (h e12)))) % 56.53/56.74 (Eq (h (op1 e14 e13)) % 56.53/56.74 (op2 (h e14) (h e13)))) % 56.53/56.74 (Eq (h (op1 e14 e14)) % 56.53/56.74 (op2 (h e14) (h e14)))) % 56.53/56.74 (Eq (j (op2 e20 e20)) % 56.53/56.74 (op1 (j e20) (j e20)))) % 56.53/56.74 (Eq (j (op2 e20 e21)) % 56.53/56.74 (op1 (j e20) (j e21)))) % 56.53/56.74 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.53/56.74 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.53/56.74 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.53/56.74 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.53/56.74 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.53/56.74 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.53/56.74 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.53/56.74 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.53/56.74 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.53/56.74 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.53/56.74 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.53/56.74 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.53/56.74 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.53/56.74 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.53/56.74 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.53/56.74 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.53/56.74 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.53/56.74 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.53/56.74 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.53/56.74 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.53/56.74 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.53/56.74 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.53/56.74 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.53/56.74 (Eq (h (j e20)) e20)) % 56.53/56.74 (Eq (h (j e21)) e21)) % 56.53/56.74 (Eq (h (j e22)) e22)) % 56.53/56.74 (Eq (h (j e23)) e23)) % 56.53/56.74 (Eq (h (j e24)) e24)) % 56.53/56.74 (Eq (j (h e10)) e10)) % 56.53/56.74 (Eq (j (h e11)) e11)) % 56.53/56.74 (Eq (j (h e12)) e12)) % 56.53/56.74 (Eq (j (h e13)) e13)) % 56.53/56.74 (Eq (j (h e14)) e14)))) % 56.53/56.74 True % 56.53/56.74 Clause #7 (by clausification #[1]): Eq % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And (And (And (And (And (And (Ne e20 e21) (Ne e20 e22)) (Ne e20 e23)) (Ne e20 e24)) (Ne e21 e22)) (Ne e21 e23)) % 56.53/56.74 (Ne e21 e24)) % 56.53/56.74 (Ne e22 e23)) % 56.53/56.74 (Ne e22 e24)) % 56.53/56.74 True % 56.53/56.74 Clause #9 (by clausification #[7]): Eq (Ne e22 e24) True % 56.53/56.74 Clause #11 (by clausification #[9]): Ne e22 e24 % 56.53/56.74 Clause #22 (by clausification #[0]): Eq % 56.53/56.74 (And % 56.53/56.74 (And % 56.53/56.74 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 56.53/56.74 (Ne e11 e14)) % 56.53/56.74 (Ne e12 e13)) % 56.53/56.74 (Ne e12 e14)) % 56.53/56.74 True % 56.53/56.74 Clause #41 (by clausification #[22]): Eq % 56.53/56.74 (And % 56.53/56.74 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 56.53/56.74 (Ne e11 e14)) % 56.53/56.74 (Ne e12 e13)) % 56.53/56.74 True % 56.53/56.74 Clause #44 (by clausification #[41]): Eq % 56.53/56.74 (And (And (And (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) (Ne e11 e12)) (Ne e11 e13)) % 56.61/56.76 (Ne e11 e14)) % 56.61/56.76 True % 56.61/56.76 Clause #46 (by clausification #[44]): Eq (Ne e11 e14) True % 56.61/56.76 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 % 56.61/56.76 Clause #48 (by clausification #[46]): Ne e11 e14 % 56.61/56.76 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 % 56.61/56.76 Clause #53 (by clausification #[50]): Eq (And (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) (Ne e10 e14)) True % 56.61/56.76 Clause #55 (by clausification #[3]): Eq (Eq (op1 e14 e14) e11) True % 56.61/56.76 Clause #56 (by clausification #[3]): Eq % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) % 56.61/56.76 (Eq (op1 e10 e12) e10)) % 56.61/56.76 (Eq (op1 e10 e13) e11)) % 56.61/56.76 (Eq (op1 e10 e14) e14)) % 56.61/56.76 (Eq (op1 e11 e10) e10)) % 56.61/56.76 (Eq (op1 e11 e11) e14)) % 56.61/56.76 (Eq (op1 e11 e12) e11)) % 56.61/56.76 (Eq (op1 e11 e13) e12)) % 56.61/56.76 (Eq (op1 e11 e14) e13)) % 56.61/56.76 (Eq (op1 e12 e10) e11)) % 56.61/56.76 (Eq (op1 e12 e11) e13)) % 56.61/56.76 (Eq (op1 e12 e12) e12)) % 56.61/56.76 (Eq (op1 e12 e13) e14)) % 56.61/56.76 (Eq (op1 e12 e14) e10)) % 56.61/56.76 (Eq (op1 e13 e10) e14)) % 56.61/56.76 (Eq (op1 e13 e11) e11)) % 56.61/56.76 (Eq (op1 e13 e12) e13)) % 56.61/56.76 (Eq (op1 e13 e13) e10)) % 56.61/56.76 (Eq (op1 e13 e14) e12)) % 56.61/56.76 (Eq (op1 e14 e10) e12)) % 56.61/56.76 (Eq (op1 e14 e11) e10)) % 56.61/56.76 (Eq (op1 e14 e12) e14)) % 56.61/56.76 (Eq (op1 e14 e13) e13)) % 56.61/56.76 True % 56.61/56.76 Clause #57 (by clausification #[55]): Eq (op1 e14 e14) e11 % 56.61/56.76 Clause #59 (by clausification #[53]): Eq (And (And (Ne e10 e11) (Ne e10 e12)) (Ne e10 e13)) True % 56.61/56.76 Clause #61 (by clausification #[59]): Eq (Ne e10 e13) True % 56.61/56.76 Clause #63 (by clausification #[61]): Ne e10 e13 % 56.61/56.76 Clause #71 (by clausification #[4]): Eq (Eq (op2 e24 e24) e24) True % 56.61/56.76 Clause #72 (by clausification #[4]): Eq % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And % 56.61/56.76 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e23)) % 56.61/56.76 (Eq (op2 e20 e22) e24)) % 56.61/56.76 (Eq (op2 e20 e23) e21)) % 56.61/56.76 (Eq (op2 e20 e24) e22)) % 56.61/56.76 (Eq (op2 e21 e20) e24)) % 56.61/56.76 (Eq (op2 e21 e21) e21)) % 56.61/56.76 (Eq (op2 e21 e22) e23)) % 56.61/56.76 (Eq (op2 e21 e23) e22)) % 56.61/56.76 (Eq (op2 e21 e24) e20)) % 56.61/56.76 (Eq (op2 e22 e20) e21)) % 56.61/56.76 (Eq (op2 e22 e21) e20)) % 56.61/56.76 (Eq (op2 e22 e22) e22)) % 56.63/56.80 (Eq (op2 e22 e23) e24)) % 56.63/56.80 (Eq (op2 e22 e24) e23)) % 56.63/56.80 (Eq (op2 e23 e20) e22)) % 56.63/56.80 (Eq (op2 e23 e21) e24)) % 56.63/56.80 (Eq (op2 e23 e22) e20)) % 56.63/56.80 (Eq (op2 e23 e23) e23)) % 56.63/56.80 (Eq (op2 e23 e24) e21)) % 56.63/56.80 (Eq (op2 e24 e20) e23)) % 56.63/56.80 (Eq (op2 e24 e21) e22)) % 56.63/56.80 (Eq (op2 e24 e22) e21)) % 56.63/56.80 (Eq (op2 e24 e23) e20)) % 56.63/56.80 True % 56.63/56.80 Clause #73 (by clausification #[71]): Eq (op2 e24 e24) e24 % 56.63/56.80 Clause #89 (by clausification #[5]): Eq % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 56.63/56.80 (Eq (h e10) e24)) % 56.63/56.80 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 56.63/56.80 (Eq (h e11) e24))) % 56.63/56.80 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 56.63/56.80 (Eq (h e12) e24))) % 56.63/56.80 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 56.63/56.80 (Eq (h e13) e24))) % 56.63/56.80 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) % 56.63/56.80 (Eq (h e14) e24))) % 56.63/56.80 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 56.63/56.80 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 56.63/56.80 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 56.63/56.80 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 56.63/56.80 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14)) → % 56.63/56.80 Not % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (And % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e10 % 56.63/56.80 e10)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e10) % 56.63/56.80 (h % 56.63/56.80 e10))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e10 % 56.63/56.80 e11)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e10) % 56.63/56.80 (h % 56.63/56.80 e11)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e10 % 56.63/56.80 e12)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e10) % 56.63/56.80 (h % 56.63/56.80 e12)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e10 % 56.63/56.80 e13)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e10) % 56.63/56.80 (h % 56.63/56.80 e13)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e10 % 56.63/56.80 e14)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e10) % 56.63/56.80 (h % 56.63/56.80 e14)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e11 % 56.63/56.80 e10)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e11) % 56.63/56.80 (h % 56.63/56.80 e10)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e11 % 56.63/56.80 e11)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e11) % 56.63/56.80 (h % 56.63/56.80 e11)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e11 % 56.63/56.80 e12)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e11) % 56.63/56.80 (h % 56.63/56.80 e12)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 % 56.63/56.80 e11 % 56.63/56.80 e13)) % 56.63/56.80 (op2 % 56.63/56.80 (h % 56.63/56.80 e11) % 56.63/56.80 (h % 56.63/56.80 e13)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 e11 % 56.63/56.80 e14)) % 56.63/56.80 (op2 % 56.63/56.80 (h e11) % 56.63/56.80 (h % 56.63/56.80 e14)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 e12 % 56.63/56.80 e10)) % 56.63/56.80 (op2 (h e12) % 56.63/56.80 (h e10)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 e12 % 56.63/56.80 e11)) % 56.63/56.80 (op2 (h e12) % 56.63/56.80 (h e11)))) % 56.63/56.80 (Eq % 56.63/56.80 (h % 56.63/56.80 (op1 e12 e12)) % 56.63/56.80 (op2 (h e12) % 56.63/56.80 (h e12)))) % 56.63/56.80 (Eq % 56.63/56.80 (h (op1 e12 e13)) % 56.63/56.80 (op2 (h e12) % 56.63/56.80 (h e13)))) % 56.63/56.80 (Eq (h (op1 e12 e14)) % 56.63/56.80 (op2 (h e12) % 56.63/56.80 (h e14)))) % 56.63/56.80 (Eq (h (op1 e13 e10)) % 56.63/56.80 (op2 (h e13) % 56.63/56.80 (h e10)))) % 56.63/56.80 (Eq (h (op1 e13 e11)) % 56.63/56.80 (op2 (h e13) (h e11)))) % 56.63/56.80 (Eq (h (op1 e13 e12)) % 56.63/56.80 (op2 (h e13) (h e12)))) % 56.63/56.80 (Eq (h (op1 e13 e13)) % 56.63/56.80 (op2 (h e13) (h e13)))) % 56.63/56.80 (Eq (h (op1 e13 e14)) % 56.63/56.80 (op2 (h e13) (h e14)))) % 56.63/56.80 (Eq (h (op1 e14 e10)) % 56.63/56.80 (op2 (h e14) (h e10)))) % 56.63/56.80 (Eq (h (op1 e14 e11)) % 56.63/56.80 (op2 (h e14) (h e11)))) % 56.63/56.80 (Eq (h (op1 e14 e12)) % 56.63/56.80 (op2 (h e14) (h e12)))) % 56.63/56.80 (Eq (h (op1 e14 e13)) % 56.63/56.80 (op2 (h e14) (h e13)))) % 56.63/56.80 (Eq (h (op1 e14 e14)) % 56.63/56.80 (op2 (h e14) (h e14)))) % 56.63/56.80 (Eq (j (op2 e20 e20)) % 56.63/56.80 (op1 (j e20) (j e20)))) % 56.63/56.80 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.63/56.80 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.63/56.80 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.63/56.80 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.63/56.80 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.63/56.80 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.63/56.80 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.63/56.80 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.67/56.83 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.67/56.83 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.67/56.83 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.67/56.83 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.67/56.83 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.67/56.83 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.67/56.83 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.67/56.83 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.67/56.83 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.67/56.83 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.67/56.83 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.67/56.83 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.67/56.83 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.67/56.83 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.67/56.83 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.67/56.83 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.67/56.83 (Eq (h (j e20)) e20)) % 56.67/56.83 (Eq (h (j e21)) e21)) % 56.67/56.83 (Eq (h (j e22)) e22)) % 56.67/56.83 (Eq (h (j e23)) e23)) % 56.67/56.83 (Eq (h (j e24)) e24)) % 56.67/56.83 (Eq (j (h e10)) e10)) % 56.67/56.83 (Eq (j (h e11)) e11)) % 56.67/56.83 (Eq (j (h e12)) e12)) % 56.67/56.83 (Eq (j (h e13)) e13)) % 56.67/56.83 (Eq (j (h e14)) e14))) % 56.67/56.83 False % 56.67/56.83 Clause #90 (by clausification #[89]): Eq % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 56.67/56.83 (Eq (h e10) e24)) % 56.67/56.83 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 56.67/56.83 (Eq (h e11) e24))) % 56.67/56.83 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 56.67/56.83 (Eq (h e12) e24))) % 56.67/56.83 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) % 56.67/56.83 (Eq (h e13) e24))) % 56.67/56.83 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) (Eq (h e14) e24))) % 56.67/56.83 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 56.67/56.83 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 56.67/56.83 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 56.67/56.83 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 56.67/56.83 (Or (Or (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) (Eq (j e24) e13)) (Eq (j e24) e14))) % 56.67/56.83 True % 56.67/56.83 Clause #91 (by clausification #[89]): Eq % 56.67/56.83 (Not % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (And % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e10 % 56.67/56.83 e10)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e10) % 56.67/56.83 (h % 56.67/56.83 e10))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e10 % 56.67/56.83 e11)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e10) % 56.67/56.83 (h % 56.67/56.83 e11)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e10 % 56.67/56.83 e12)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e10) % 56.67/56.83 (h % 56.67/56.83 e12)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e10 % 56.67/56.83 e13)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e10) % 56.67/56.83 (h % 56.67/56.83 e13)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e10 % 56.67/56.83 e14)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e10) % 56.67/56.83 (h % 56.67/56.83 e14)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e11 % 56.67/56.83 e10)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e11) % 56.67/56.83 (h % 56.67/56.83 e10)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e11 % 56.67/56.83 e11)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e11) % 56.67/56.83 (h % 56.67/56.83 e11)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 % 56.67/56.83 e11 % 56.67/56.83 e12)) % 56.67/56.83 (op2 % 56.67/56.83 (h % 56.67/56.83 e11) % 56.67/56.83 (h % 56.67/56.83 e12)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 e11 % 56.67/56.83 e13)) % 56.67/56.83 (op2 % 56.67/56.83 (h e11) % 56.67/56.83 (h % 56.67/56.83 e13)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 e11 % 56.67/56.83 e14)) % 56.67/56.83 (op2 (h e11) % 56.67/56.83 (h e14)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 e12 % 56.67/56.83 e10)) % 56.67/56.83 (op2 (h e12) % 56.67/56.83 (h e10)))) % 56.67/56.83 (Eq % 56.67/56.83 (h % 56.67/56.83 (op1 e12 e11)) % 56.67/56.83 (op2 (h e12) % 56.67/56.83 (h e11)))) % 56.67/56.83 (Eq % 56.67/56.83 (h (op1 e12 e12)) % 56.67/56.83 (op2 (h e12) % 56.67/56.83 (h e12)))) % 56.67/56.83 (Eq (h (op1 e12 e13)) % 56.67/56.83 (op2 (h e12) % 56.67/56.83 (h e13)))) % 56.67/56.83 (Eq (h (op1 e12 e14)) % 56.67/56.83 (op2 (h e12) % 56.67/56.83 (h e14)))) % 56.67/56.83 (Eq (h (op1 e13 e10)) % 56.67/56.83 (op2 (h e13) (h e10)))) % 56.67/56.83 (Eq (h (op1 e13 e11)) % 56.67/56.83 (op2 (h e13) (h e11)))) % 56.67/56.83 (Eq (h (op1 e13 e12)) % 56.67/56.83 (op2 (h e13) (h e12)))) % 56.67/56.83 (Eq (h (op1 e13 e13)) % 56.67/56.83 (op2 (h e13) (h e13)))) % 56.67/56.83 (Eq (h (op1 e13 e14)) % 56.67/56.83 (op2 (h e13) (h e14)))) % 56.67/56.83 (Eq (h (op1 e14 e10)) % 56.67/56.83 (op2 (h e14) (h e10)))) % 56.67/56.83 (Eq (h (op1 e14 e11)) % 56.67/56.83 (op2 (h e14) (h e11)))) % 56.67/56.83 (Eq (h (op1 e14 e12)) % 56.67/56.83 (op2 (h e14) (h e12)))) % 56.67/56.83 (Eq (h (op1 e14 e13)) % 56.67/56.83 (op2 (h e14) (h e13)))) % 56.67/56.83 (Eq (h (op1 e14 e14)) % 56.67/56.83 (op2 (h e14) (h e14)))) % 56.67/56.83 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.67/56.83 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.67/56.83 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.67/56.83 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.67/56.83 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.67/56.83 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.67/56.83 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.67/56.83 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.67/56.83 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.67/56.83 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.70/56.85 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.70/56.85 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.70/56.85 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.70/56.85 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.70/56.85 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.70/56.85 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.70/56.85 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.70/56.85 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.70/56.85 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.70/56.85 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.70/56.85 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.70/56.85 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.70/56.85 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.70/56.85 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.70/56.85 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.70/56.85 (Eq (h (j e20)) e20)) % 56.70/56.85 (Eq (h (j e21)) e21)) % 56.70/56.85 (Eq (h (j e22)) e22)) % 56.70/56.85 (Eq (h (j e23)) e23)) % 56.70/56.85 (Eq (h (j e24)) e24)) % 56.70/56.85 (Eq (j (h e10)) e10)) % 56.70/56.85 (Eq (j (h e11)) e11)) % 56.70/56.85 (Eq (j (h e12)) e12)) % 56.70/56.85 (Eq (j (h e13)) e13)) % 56.70/56.85 (Eq (j (h e14)) e14))) % 56.70/56.85 False % 56.70/56.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 % 56.70/56.85 Clause #93 (by clausification #[90]): Eq % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (And % 56.70/56.85 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) % 56.70/56.85 (Eq (h e10) e24)) % 56.70/56.85 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 56.70/56.85 (Eq (h e11) e24))) % 56.70/56.85 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) % 56.70/56.85 (Eq (h e12) e24))) % 56.70/56.85 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) (Eq (h e13) e24))) % 56.70/56.85 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) (Eq (h e14) e24))) % 56.70/56.85 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 56.70/56.85 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 56.70/56.85 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 56.70/56.85 (Or (Or (Or (Or (Eq (j e23) e10) (Eq (j e23) e11)) (Eq (j e23) e12)) (Eq (j e23) e13)) (Eq (j e23) e14))) % 56.70/56.85 True % 56.70/56.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) % 56.70/56.85 (Eq (Eq (j e24) e14) True) % 56.70/56.85 Clause #95 (by clausification #[94]): Or (Eq (Eq (j e24) e14) True) % 56.70/56.85 (Or (Eq (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) True) (Eq (Eq (j e24) e13) True)) % 56.70/56.85 Clause #96 (by clausification #[95]): Or (Eq (Or (Or (Eq (j e24) e10) (Eq (j e24) e11)) (Eq (j e24) e12)) True) % 56.70/56.85 (Or (Eq (Eq (j e24) e13) True) (Eq (j e24) e14)) % 56.70/56.85 Clause #97 (by clausification #[96]): Or (Eq (Eq (j e24) e13) True) % 56.70/56.85 (Or (Eq (j e24) e14) (Or (Eq (Or (Eq (j e24) e10) (Eq (j e24) e11)) True) (Eq (Eq (j e24) e12) True))) % 56.70/56.85 Clause #98 (by clausification #[97]): Or (Eq (j e24) e14) % 56.70/56.85 (Or (Eq (Or (Eq (j e24) e10) (Eq (j e24) e11)) True) (Or (Eq (Eq (j e24) e12) True) (Eq (j e24) e13))) % 56.70/56.85 Clause #99 (by clausification #[98]): Or (Eq (j e24) e14) % 56.70/56.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)))) % 56.70/56.89 Clause #100 (by clausification #[99]): Or (Eq (j e24) e14) % 56.70/56.89 (Or (Eq (j e24) e13) (Or (Eq (Eq (j e24) e10) True) (Or (Eq (Eq (j e24) e11) True) (Eq (j e24) e12)))) % 56.70/56.89 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)))) % 56.70/56.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)))) % 56.70/56.89 Clause #111 (by clausification #[56]): Eq % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) % 56.70/56.89 (Eq (op1 e10 e12) e10)) % 56.70/56.89 (Eq (op1 e10 e13) e11)) % 56.70/56.89 (Eq (op1 e10 e14) e14)) % 56.70/56.89 (Eq (op1 e11 e10) e10)) % 56.70/56.89 (Eq (op1 e11 e11) e14)) % 56.70/56.89 (Eq (op1 e11 e12) e11)) % 56.70/56.89 (Eq (op1 e11 e13) e12)) % 56.70/56.89 (Eq (op1 e11 e14) e13)) % 56.70/56.89 (Eq (op1 e12 e10) e11)) % 56.70/56.89 (Eq (op1 e12 e11) e13)) % 56.70/56.89 (Eq (op1 e12 e12) e12)) % 56.70/56.89 (Eq (op1 e12 e13) e14)) % 56.70/56.89 (Eq (op1 e12 e14) e10)) % 56.70/56.89 (Eq (op1 e13 e10) e14)) % 56.70/56.89 (Eq (op1 e13 e11) e11)) % 56.70/56.89 (Eq (op1 e13 e12) e13)) % 56.70/56.89 (Eq (op1 e13 e13) e10)) % 56.70/56.89 (Eq (op1 e13 e14) e12)) % 56.70/56.89 (Eq (op1 e14 e10) e12)) % 56.70/56.89 (Eq (op1 e14 e11) e10)) % 56.70/56.89 (Eq (op1 e14 e12) e14)) % 56.70/56.89 True % 56.70/56.89 Clause #129 (by clausification #[72]): Eq % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e23)) % 56.70/56.89 (Eq (op2 e20 e22) e24)) % 56.70/56.89 (Eq (op2 e20 e23) e21)) % 56.70/56.89 (Eq (op2 e20 e24) e22)) % 56.70/56.89 (Eq (op2 e21 e20) e24)) % 56.70/56.89 (Eq (op2 e21 e21) e21)) % 56.70/56.89 (Eq (op2 e21 e22) e23)) % 56.70/56.89 (Eq (op2 e21 e23) e22)) % 56.70/56.89 (Eq (op2 e21 e24) e20)) % 56.70/56.89 (Eq (op2 e22 e20) e21)) % 56.70/56.89 (Eq (op2 e22 e21) e20)) % 56.70/56.89 (Eq (op2 e22 e22) e22)) % 56.70/56.89 (Eq (op2 e22 e23) e24)) % 56.70/56.89 (Eq (op2 e22 e24) e23)) % 56.70/56.89 (Eq (op2 e23 e20) e22)) % 56.70/56.89 (Eq (op2 e23 e21) e24)) % 56.70/56.89 (Eq (op2 e23 e22) e20)) % 56.70/56.89 (Eq (op2 e23 e23) e23)) % 56.70/56.89 (Eq (op2 e23 e24) e21)) % 56.70/56.89 (Eq (op2 e24 e20) e23)) % 56.70/56.89 (Eq (op2 e24 e21) e22)) % 56.70/56.89 (Eq (op2 e24 e22) e21)) % 56.70/56.89 True % 56.70/56.89 Clause #146 (by clausification #[91]): Eq % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (And % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e10 % 56.70/56.89 e10)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e10) % 56.70/56.89 (h % 56.70/56.89 e10))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e10 % 56.70/56.89 e11)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e10) % 56.70/56.89 (h % 56.70/56.89 e11)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e10 % 56.70/56.89 e12)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e10) % 56.70/56.89 (h % 56.70/56.89 e12)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e10 % 56.70/56.89 e13)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e10) % 56.70/56.89 (h % 56.70/56.89 e13)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e10 % 56.70/56.89 e14)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e10) % 56.70/56.89 (h % 56.70/56.89 e14)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e11 % 56.70/56.89 e10)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e11) % 56.70/56.89 (h % 56.70/56.89 e10)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 % 56.70/56.89 e11 % 56.70/56.89 e11)) % 56.70/56.89 (op2 % 56.70/56.89 (h % 56.70/56.89 e11) % 56.70/56.89 (h % 56.70/56.89 e11)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 e11 % 56.70/56.89 e12)) % 56.70/56.89 (op2 % 56.70/56.89 (h e11) % 56.70/56.89 (h % 56.70/56.89 e12)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 e11 % 56.70/56.89 e13)) % 56.70/56.89 (op2 (h e11) % 56.70/56.89 (h e13)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 e11 % 56.70/56.89 e14)) % 56.70/56.89 (op2 (h e11) % 56.70/56.89 (h e14)))) % 56.70/56.89 (Eq % 56.70/56.89 (h % 56.70/56.89 (op1 e12 e10)) % 56.70/56.89 (op2 (h e12) % 56.70/56.89 (h e10)))) % 56.70/56.89 (Eq % 56.70/56.89 (h (op1 e12 e11)) % 56.70/56.89 (op2 (h e12) % 56.70/56.89 (h e11)))) % 56.70/56.89 (Eq (h (op1 e12 e12)) % 56.70/56.89 (op2 (h e12) % 56.70/56.89 (h e12)))) % 56.70/56.89 (Eq (h (op1 e12 e13)) % 56.70/56.89 (op2 (h e12) % 56.70/56.89 (h e13)))) % 56.70/56.89 (Eq (h (op1 e12 e14)) % 56.70/56.89 (op2 (h e12) (h e14)))) % 56.70/56.89 (Eq (h (op1 e13 e10)) % 56.70/56.89 (op2 (h e13) (h e10)))) % 56.70/56.89 (Eq (h (op1 e13 e11)) % 56.70/56.89 (op2 (h e13) (h e11)))) % 56.70/56.89 (Eq (h (op1 e13 e12)) % 56.70/56.89 (op2 (h e13) (h e12)))) % 56.70/56.89 (Eq (h (op1 e13 e13)) % 56.70/56.89 (op2 (h e13) (h e13)))) % 56.70/56.89 (Eq (h (op1 e13 e14)) % 56.70/56.89 (op2 (h e13) (h e14)))) % 56.70/56.89 (Eq (h (op1 e14 e10)) % 56.70/56.89 (op2 (h e14) (h e10)))) % 56.70/56.89 (Eq (h (op1 e14 e11)) % 56.70/56.89 (op2 (h e14) (h e11)))) % 56.70/56.89 (Eq (h (op1 e14 e12)) % 56.70/56.89 (op2 (h e14) (h e12)))) % 56.70/56.89 (Eq (h (op1 e14 e13)) % 56.70/56.89 (op2 (h e14) (h e13)))) % 56.70/56.89 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 56.70/56.89 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.70/56.89 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.70/56.89 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.70/56.89 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.70/56.89 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.70/56.89 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.70/56.89 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.70/56.89 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.70/56.89 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.70/56.89 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.70/56.89 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.70/56.89 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.70/56.89 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.70/56.89 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.70/56.89 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.70/56.89 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.70/56.89 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.70/56.89 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.70/56.92 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.70/56.92 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.70/56.92 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.70/56.92 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.70/56.92 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.70/56.92 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.70/56.92 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.70/56.92 (Eq (h (j e20)) e20)) % 56.70/56.92 (Eq (h (j e21)) e21)) % 56.70/56.92 (Eq (h (j e22)) e22)) % 56.70/56.92 (Eq (h (j e23)) e23)) % 56.70/56.92 (Eq (h (j e24)) e24)) % 56.70/56.92 (Eq (j (h e10)) e10)) % 56.70/56.92 (Eq (j (h e11)) e11)) % 56.70/56.92 (Eq (j (h e12)) e12)) % 56.70/56.92 (Eq (j (h e13)) e13)) % 56.70/56.92 (Eq (j (h e14)) e14)) % 56.70/56.92 True % 56.70/56.92 Clause #148 (by clausification #[146]): Eq % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (And % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 % 56.70/56.92 e10 % 56.70/56.92 e10)) % 56.70/56.92 (op2 % 56.70/56.92 (h % 56.70/56.92 e10) % 56.70/56.92 (h % 56.70/56.92 e10))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 % 56.70/56.92 e10 % 56.70/56.92 e11)) % 56.70/56.92 (op2 % 56.70/56.92 (h % 56.70/56.92 e10) % 56.70/56.92 (h % 56.70/56.92 e11)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 % 56.70/56.92 e10 % 56.70/56.92 e12)) % 56.70/56.92 (op2 % 56.70/56.92 (h % 56.70/56.92 e10) % 56.70/56.92 (h % 56.70/56.92 e12)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 % 56.70/56.92 e10 % 56.70/56.92 e13)) % 56.70/56.92 (op2 % 56.70/56.92 (h % 56.70/56.92 e10) % 56.70/56.92 (h % 56.70/56.92 e13)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 % 56.70/56.92 e10 % 56.70/56.92 e14)) % 56.70/56.92 (op2 % 56.70/56.92 (h % 56.70/56.92 e10) % 56.70/56.92 (h % 56.70/56.92 e14)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 % 56.70/56.92 e11 % 56.70/56.92 e10)) % 56.70/56.92 (op2 % 56.70/56.92 (h % 56.70/56.92 e11) % 56.70/56.92 (h % 56.70/56.92 e10)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 e11 % 56.70/56.92 e11)) % 56.70/56.92 (op2 % 56.70/56.92 (h e11) % 56.70/56.92 (h % 56.70/56.92 e11)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 e11 % 56.70/56.92 e12)) % 56.70/56.92 (op2 (h e11) % 56.70/56.92 (h e12)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 e11 % 56.70/56.92 e13)) % 56.70/56.92 (op2 (h e11) % 56.70/56.92 (h e13)))) % 56.70/56.92 (Eq % 56.70/56.92 (h % 56.70/56.92 (op1 e11 e14)) % 56.70/56.92 (op2 (h e11) % 56.70/56.92 (h e14)))) % 56.70/56.92 (Eq % 56.70/56.92 (h (op1 e12 e10)) % 56.70/56.92 (op2 (h e12) % 56.70/56.92 (h e10)))) % 56.70/56.92 (Eq (h (op1 e12 e11)) % 56.70/56.92 (op2 (h e12) % 56.70/56.92 (h e11)))) % 56.70/56.92 (Eq (h (op1 e12 e12)) % 56.70/56.92 (op2 (h e12) % 56.70/56.92 (h e12)))) % 56.70/56.92 (Eq (h (op1 e12 e13)) % 56.70/56.92 (op2 (h e12) (h e13)))) % 56.70/56.92 (Eq (h (op1 e12 e14)) % 56.70/56.92 (op2 (h e12) (h e14)))) % 56.70/56.92 (Eq (h (op1 e13 e10)) % 56.70/56.92 (op2 (h e13) (h e10)))) % 56.70/56.92 (Eq (h (op1 e13 e11)) % 56.70/56.92 (op2 (h e13) (h e11)))) % 56.70/56.92 (Eq (h (op1 e13 e12)) % 56.70/56.92 (op2 (h e13) (h e12)))) % 56.70/56.92 (Eq (h (op1 e13 e13)) % 56.70/56.92 (op2 (h e13) (h e13)))) % 56.70/56.92 (Eq (h (op1 e13 e14)) % 56.70/56.92 (op2 (h e13) (h e14)))) % 56.70/56.92 (Eq (h (op1 e14 e10)) % 56.70/56.92 (op2 (h e14) (h e10)))) % 56.70/56.92 (Eq (h (op1 e14 e11)) % 56.70/56.92 (op2 (h e14) (h e11)))) % 56.70/56.92 (Eq (h (op1 e14 e12)) % 56.70/56.92 (op2 (h e14) (h e12)))) % 56.70/56.92 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 56.70/56.92 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 56.70/56.92 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.70/56.92 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.70/56.92 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.70/56.92 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.70/56.92 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.70/56.92 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.70/56.92 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.70/56.92 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.70/56.92 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.70/56.92 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.70/56.92 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.70/56.92 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.70/56.92 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.70/56.92 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.70/56.92 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.70/56.92 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.70/56.92 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.70/56.92 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.70/56.92 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.70/56.92 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.78/56.94 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.78/56.94 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.78/56.94 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.78/56.94 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.78/56.94 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.78/56.94 (Eq (h (j e20)) e20)) % 56.78/56.94 (Eq (h (j e21)) e21)) % 56.78/56.94 (Eq (h (j e22)) e22)) % 56.78/56.94 (Eq (h (j e23)) e23)) % 56.78/56.94 (Eq (h (j e24)) e24)) % 56.78/56.94 (Eq (j (h e10)) e10)) % 56.78/56.94 (Eq (j (h e11)) e11)) % 56.78/56.94 (Eq (j (h e12)) e12)) % 56.78/56.94 (Eq (j (h e13)) e13)) % 56.78/56.94 True % 56.78/56.94 Clause #166 (by clausification #[93]): Eq % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (Or (Or (Or (Or (Eq (h e10) e20) (Eq (h e10) e21)) (Eq (h e10) e22)) (Eq (h e10) e23)) (Eq (h e10) e24)) % 56.78/56.94 (Or (Or (Or (Or (Eq (h e11) e20) (Eq (h e11) e21)) (Eq (h e11) e22)) (Eq (h e11) e23)) % 56.78/56.94 (Eq (h e11) e24))) % 56.78/56.94 (Or (Or (Or (Or (Eq (h e12) e20) (Eq (h e12) e21)) (Eq (h e12) e22)) (Eq (h e12) e23)) (Eq (h e12) e24))) % 56.78/56.94 (Or (Or (Or (Or (Eq (h e13) e20) (Eq (h e13) e21)) (Eq (h e13) e22)) (Eq (h e13) e23)) (Eq (h e13) e24))) % 56.78/56.94 (Or (Or (Or (Or (Eq (h e14) e20) (Eq (h e14) e21)) (Eq (h e14) e22)) (Eq (h e14) e23)) (Eq (h e14) e24))) % 56.78/56.94 (Or (Or (Or (Or (Eq (j e20) e10) (Eq (j e20) e11)) (Eq (j e20) e12)) (Eq (j e20) e13)) (Eq (j e20) e14))) % 56.78/56.94 (Or (Or (Or (Or (Eq (j e21) e10) (Eq (j e21) e11)) (Eq (j e21) e12)) (Eq (j e21) e13)) (Eq (j e21) e14))) % 56.78/56.94 (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14))) % 56.78/56.94 True % 56.78/56.94 Clause #185 (by clausification #[111]): Eq % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.94 (Eq (op1 e10 e13) e11)) % 56.78/56.94 (Eq (op1 e10 e14) e14)) % 56.78/56.94 (Eq (op1 e11 e10) e10)) % 56.78/56.94 (Eq (op1 e11 e11) e14)) % 56.78/56.94 (Eq (op1 e11 e12) e11)) % 56.78/56.94 (Eq (op1 e11 e13) e12)) % 56.78/56.94 (Eq (op1 e11 e14) e13)) % 56.78/56.94 (Eq (op1 e12 e10) e11)) % 56.78/56.94 (Eq (op1 e12 e11) e13)) % 56.78/56.94 (Eq (op1 e12 e12) e12)) % 56.78/56.94 (Eq (op1 e12 e13) e14)) % 56.78/56.94 (Eq (op1 e12 e14) e10)) % 56.78/56.94 (Eq (op1 e13 e10) e14)) % 56.78/56.94 (Eq (op1 e13 e11) e11)) % 56.78/56.94 (Eq (op1 e13 e12) e13)) % 56.78/56.94 (Eq (op1 e13 e13) e10)) % 56.78/56.94 (Eq (op1 e13 e14) e12)) % 56.78/56.94 (Eq (op1 e14 e10) e12)) % 56.78/56.94 (Eq (op1 e14 e11) e10)) % 56.78/56.94 True % 56.78/56.94 Clause #188 (by clausification #[185]): Eq % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And % 56.78/56.94 (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.94 (Eq (op1 e10 e13) e11)) % 56.78/56.94 (Eq (op1 e10 e14) e14)) % 56.78/56.94 (Eq (op1 e11 e10) e10)) % 56.78/56.94 (Eq (op1 e11 e11) e14)) % 56.78/56.95 (Eq (op1 e11 e12) e11)) % 56.78/56.95 (Eq (op1 e11 e13) e12)) % 56.78/56.95 (Eq (op1 e11 e14) e13)) % 56.78/56.95 (Eq (op1 e12 e10) e11)) % 56.78/56.95 (Eq (op1 e12 e11) e13)) % 56.78/56.95 (Eq (op1 e12 e12) e12)) % 56.78/56.95 (Eq (op1 e12 e13) e14)) % 56.78/56.95 (Eq (op1 e12 e14) e10)) % 56.78/56.95 (Eq (op1 e13 e10) e14)) % 56.78/56.95 (Eq (op1 e13 e11) e11)) % 56.78/56.95 (Eq (op1 e13 e12) e13)) % 56.78/56.95 (Eq (op1 e13 e13) e10)) % 56.78/56.95 (Eq (op1 e13 e14) e12)) % 56.78/56.95 (Eq (op1 e14 e10) e12)) % 56.78/56.95 True % 56.78/56.95 Clause #191 (by clausification #[188]): Eq % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.95 (Eq (op1 e10 e13) e11)) % 56.78/56.95 (Eq (op1 e10 e14) e14)) % 56.78/56.95 (Eq (op1 e11 e10) e10)) % 56.78/56.95 (Eq (op1 e11 e11) e14)) % 56.78/56.95 (Eq (op1 e11 e12) e11)) % 56.78/56.95 (Eq (op1 e11 e13) e12)) % 56.78/56.95 (Eq (op1 e11 e14) e13)) % 56.78/56.95 (Eq (op1 e12 e10) e11)) % 56.78/56.95 (Eq (op1 e12 e11) e13)) % 56.78/56.95 (Eq (op1 e12 e12) e12)) % 56.78/56.95 (Eq (op1 e12 e13) e14)) % 56.78/56.95 (Eq (op1 e12 e14) e10)) % 56.78/56.95 (Eq (op1 e13 e10) e14)) % 56.78/56.95 (Eq (op1 e13 e11) e11)) % 56.78/56.95 (Eq (op1 e13 e12) e13)) % 56.78/56.95 (Eq (op1 e13 e13) e10)) % 56.78/56.95 (Eq (op1 e13 e14) e12)) % 56.78/56.95 True % 56.78/56.95 Clause #194 (by clausification #[191]): Eq % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.95 (Eq (op1 e10 e13) e11)) % 56.78/56.95 (Eq (op1 e10 e14) e14)) % 56.78/56.95 (Eq (op1 e11 e10) e10)) % 56.78/56.95 (Eq (op1 e11 e11) e14)) % 56.78/56.95 (Eq (op1 e11 e12) e11)) % 56.78/56.95 (Eq (op1 e11 e13) e12)) % 56.78/56.95 (Eq (op1 e11 e14) e13)) % 56.78/56.95 (Eq (op1 e12 e10) e11)) % 56.78/56.95 (Eq (op1 e12 e11) e13)) % 56.78/56.95 (Eq (op1 e12 e12) e12)) % 56.78/56.95 (Eq (op1 e12 e13) e14)) % 56.78/56.95 (Eq (op1 e12 e14) e10)) % 56.78/56.95 (Eq (op1 e13 e10) e14)) % 56.78/56.95 (Eq (op1 e13 e11) e11)) % 56.78/56.95 (Eq (op1 e13 e12) e13)) % 56.78/56.95 (Eq (op1 e13 e13) e10)) % 56.78/56.95 True % 56.78/56.95 Clause #196 (by clausification #[194]): Eq (Eq (op1 e13 e13) e10) True % 56.78/56.95 Clause #197 (by clausification #[194]): Eq % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And % 56.78/56.95 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.95 (Eq (op1 e10 e13) e11)) % 56.78/56.95 (Eq (op1 e10 e14) e14)) % 56.78/56.95 (Eq (op1 e11 e10) e10)) % 56.78/56.95 (Eq (op1 e11 e11) e14)) % 56.78/56.95 (Eq (op1 e11 e12) e11)) % 56.78/56.95 (Eq (op1 e11 e13) e12)) % 56.78/56.95 (Eq (op1 e11 e14) e13)) % 56.78/56.95 (Eq (op1 e12 e10) e11)) % 56.78/56.95 (Eq (op1 e12 e11) e13)) % 56.78/56.95 (Eq (op1 e12 e12) e12)) % 56.78/56.95 (Eq (op1 e12 e13) e14)) % 56.78/56.95 (Eq (op1 e12 e14) e10)) % 56.78/56.95 (Eq (op1 e13 e10) e14)) % 56.78/56.97 (Eq (op1 e13 e11) e11)) % 56.78/56.97 (Eq (op1 e13 e12) e13)) % 56.78/56.97 True % 56.78/56.97 Clause #198 (by clausification #[196]): Eq (op1 e13 e13) e10 % 56.78/56.97 Clause #199 (by clausification #[129]): Eq (Eq (op2 e24 e22) e21) True % 56.78/56.97 Clause #200 (by clausification #[129]): Eq % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And (And (Eq (op2 e20 e20) e20) (Eq (op2 e20 e21) e23)) (Eq (op2 e20 e22) e24)) % 56.78/56.97 (Eq (op2 e20 e23) e21)) % 56.78/56.97 (Eq (op2 e20 e24) e22)) % 56.78/56.97 (Eq (op2 e21 e20) e24)) % 56.78/56.97 (Eq (op2 e21 e21) e21)) % 56.78/56.97 (Eq (op2 e21 e22) e23)) % 56.78/56.97 (Eq (op2 e21 e23) e22)) % 56.78/56.97 (Eq (op2 e21 e24) e20)) % 56.78/56.97 (Eq (op2 e22 e20) e21)) % 56.78/56.97 (Eq (op2 e22 e21) e20)) % 56.78/56.97 (Eq (op2 e22 e22) e22)) % 56.78/56.97 (Eq (op2 e22 e23) e24)) % 56.78/56.97 (Eq (op2 e22 e24) e23)) % 56.78/56.97 (Eq (op2 e23 e20) e22)) % 56.78/56.97 (Eq (op2 e23 e21) e24)) % 56.78/56.97 (Eq (op2 e23 e22) e20)) % 56.78/56.97 (Eq (op2 e23 e23) e23)) % 56.78/56.97 (Eq (op2 e23 e24) e21)) % 56.78/56.97 (Eq (op2 e24 e20) e23)) % 56.78/56.97 (Eq (op2 e24 e21) e22)) % 56.78/56.97 True % 56.78/56.97 Clause #201 (by clausification #[199]): Eq (op2 e24 e22) e21 % 56.78/56.97 Clause #203 (by clausification #[197]): Eq % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.97 (Eq (op1 e10 e13) e11)) % 56.78/56.97 (Eq (op1 e10 e14) e14)) % 56.78/56.97 (Eq (op1 e11 e10) e10)) % 56.78/56.97 (Eq (op1 e11 e11) e14)) % 56.78/56.97 (Eq (op1 e11 e12) e11)) % 56.78/56.97 (Eq (op1 e11 e13) e12)) % 56.78/56.97 (Eq (op1 e11 e14) e13)) % 56.78/56.97 (Eq (op1 e12 e10) e11)) % 56.78/56.97 (Eq (op1 e12 e11) e13)) % 56.78/56.97 (Eq (op1 e12 e12) e12)) % 56.78/56.97 (Eq (op1 e12 e13) e14)) % 56.78/56.97 (Eq (op1 e12 e14) e10)) % 56.78/56.97 (Eq (op1 e13 e10) e14)) % 56.78/56.97 (Eq (op1 e13 e11) e11)) % 56.78/56.97 True % 56.78/56.97 Clause #206 (by clausification #[203]): Eq % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.97 (Eq (op1 e10 e13) e11)) % 56.78/56.97 (Eq (op1 e10 e14) e14)) % 56.78/56.97 (Eq (op1 e11 e10) e10)) % 56.78/56.97 (Eq (op1 e11 e11) e14)) % 56.78/56.97 (Eq (op1 e11 e12) e11)) % 56.78/56.97 (Eq (op1 e11 e13) e12)) % 56.78/56.97 (Eq (op1 e11 e14) e13)) % 56.78/56.97 (Eq (op1 e12 e10) e11)) % 56.78/56.97 (Eq (op1 e12 e11) e13)) % 56.78/56.97 (Eq (op1 e12 e12) e12)) % 56.78/56.97 (Eq (op1 e12 e13) e14)) % 56.78/56.97 (Eq (op1 e12 e14) e10)) % 56.78/56.97 (Eq (op1 e13 e10) e14)) % 56.78/56.97 True % 56.78/56.97 Clause #209 (by clausification #[206]): Eq % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And % 56.78/56.97 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.78/56.97 (Eq (op1 e10 e13) e11)) % 56.78/56.97 (Eq (op1 e10 e14) e14)) % 56.83/57.00 (Eq (op1 e11 e10) e10)) % 56.83/57.00 (Eq (op1 e11 e11) e14)) % 56.83/57.00 (Eq (op1 e11 e12) e11)) % 56.83/57.00 (Eq (op1 e11 e13) e12)) % 56.83/57.00 (Eq (op1 e11 e14) e13)) % 56.83/57.00 (Eq (op1 e12 e10) e11)) % 56.83/57.00 (Eq (op1 e12 e11) e13)) % 56.83/57.00 (Eq (op1 e12 e12) e12)) % 56.83/57.00 (Eq (op1 e12 e13) e14)) % 56.83/57.00 (Eq (op1 e12 e14) e10)) % 56.83/57.00 True % 56.83/57.00 Clause #211 (by clausification #[209]): Eq (Eq (op1 e12 e14) e10) True % 56.83/57.00 Clause #212 (by clausification #[209]): Eq % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.83/57.00 (Eq (op1 e10 e13) e11)) % 56.83/57.00 (Eq (op1 e10 e14) e14)) % 56.83/57.00 (Eq (op1 e11 e10) e10)) % 56.83/57.00 (Eq (op1 e11 e11) e14)) % 56.83/57.00 (Eq (op1 e11 e12) e11)) % 56.83/57.00 (Eq (op1 e11 e13) e12)) % 56.83/57.00 (Eq (op1 e11 e14) e13)) % 56.83/57.00 (Eq (op1 e12 e10) e11)) % 56.83/57.00 (Eq (op1 e12 e11) e13)) % 56.83/57.00 (Eq (op1 e12 e12) e12)) % 56.83/57.00 (Eq (op1 e12 e13) e14)) % 56.83/57.00 True % 56.83/57.00 Clause #213 (by clausification #[211]): Eq (op1 e12 e14) e10 % 56.83/57.00 Clause #214 (by clausification #[212]): Eq (Eq (op1 e12 e13) e14) True % 56.83/57.00 Clause #215 (by clausification #[212]): Eq % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.83/57.00 (Eq (op1 e10 e13) e11)) % 56.83/57.00 (Eq (op1 e10 e14) e14)) % 56.83/57.00 (Eq (op1 e11 e10) e10)) % 56.83/57.00 (Eq (op1 e11 e11) e14)) % 56.83/57.00 (Eq (op1 e11 e12) e11)) % 56.83/57.00 (Eq (op1 e11 e13) e12)) % 56.83/57.00 (Eq (op1 e11 e14) e13)) % 56.83/57.00 (Eq (op1 e12 e10) e11)) % 56.83/57.00 (Eq (op1 e12 e11) e13)) % 56.83/57.00 (Eq (op1 e12 e12) e12)) % 56.83/57.00 True % 56.83/57.00 Clause #216 (by clausification #[214]): Eq (op1 e12 e13) e14 % 56.83/57.00 Clause #217 (by clausification #[148]): Eq (Eq (j (h e13)) e13) True % 56.83/57.00 Clause #218 (by clausification #[148]): Eq % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (And % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 % 56.83/57.00 e10 % 56.83/57.00 e10)) % 56.83/57.00 (op2 % 56.83/57.00 (h % 56.83/57.00 e10) % 56.83/57.00 (h % 56.83/57.00 e10))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 % 56.83/57.00 e10 % 56.83/57.00 e11)) % 56.83/57.00 (op2 % 56.83/57.00 (h % 56.83/57.00 e10) % 56.83/57.00 (h % 56.83/57.00 e11)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 % 56.83/57.00 e10 % 56.83/57.00 e12)) % 56.83/57.00 (op2 % 56.83/57.00 (h % 56.83/57.00 e10) % 56.83/57.00 (h % 56.83/57.00 e12)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 % 56.83/57.00 e10 % 56.83/57.00 e13)) % 56.83/57.00 (op2 % 56.83/57.00 (h % 56.83/57.00 e10) % 56.83/57.00 (h % 56.83/57.00 e13)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 % 56.83/57.00 e10 % 56.83/57.00 e14)) % 56.83/57.00 (op2 % 56.83/57.00 (h % 56.83/57.00 e10) % 56.83/57.00 (h % 56.83/57.00 e14)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 e11 % 56.83/57.00 e10)) % 56.83/57.00 (op2 % 56.83/57.00 (h e11) % 56.83/57.00 (h % 56.83/57.00 e10)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 e11 % 56.83/57.00 e11)) % 56.83/57.00 (op2 (h e11) % 56.83/57.00 (h e11)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 e11 % 56.83/57.00 e12)) % 56.83/57.00 (op2 (h e11) % 56.83/57.00 (h e12)))) % 56.83/57.00 (Eq % 56.83/57.00 (h % 56.83/57.00 (op1 e11 e13)) % 56.83/57.00 (op2 (h e11) % 56.83/57.00 (h e13)))) % 56.83/57.00 (Eq % 56.83/57.00 (h (op1 e11 e14)) % 56.83/57.00 (op2 (h e11) % 56.83/57.00 (h e14)))) % 56.83/57.00 (Eq (h (op1 e12 e10)) % 56.83/57.00 (op2 (h e12) % 56.83/57.00 (h e10)))) % 56.83/57.00 (Eq (h (op1 e12 e11)) % 56.83/57.00 (op2 (h e12) % 56.83/57.00 (h e11)))) % 56.83/57.00 (Eq (h (op1 e12 e12)) % 56.83/57.00 (op2 (h e12) (h e12)))) % 56.83/57.00 (Eq (h (op1 e12 e13)) % 56.83/57.00 (op2 (h e12) (h e13)))) % 56.83/57.00 (Eq (h (op1 e12 e14)) % 56.83/57.00 (op2 (h e12) (h e14)))) % 56.83/57.00 (Eq (h (op1 e13 e10)) % 56.83/57.00 (op2 (h e13) (h e10)))) % 56.83/57.00 (Eq (h (op1 e13 e11)) % 56.83/57.00 (op2 (h e13) (h e11)))) % 56.83/57.00 (Eq (h (op1 e13 e12)) % 56.83/57.00 (op2 (h e13) (h e12)))) % 56.83/57.00 (Eq (h (op1 e13 e13)) % 56.83/57.00 (op2 (h e13) (h e13)))) % 56.83/57.00 (Eq (h (op1 e13 e14)) % 56.83/57.00 (op2 (h e13) (h e14)))) % 56.83/57.00 (Eq (h (op1 e14 e10)) % 56.83/57.00 (op2 (h e14) (h e10)))) % 56.83/57.00 (Eq (h (op1 e14 e11)) % 56.83/57.00 (op2 (h e14) (h e11)))) % 56.83/57.00 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 56.83/57.00 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 56.83/57.00 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 56.83/57.00 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.83/57.00 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.83/57.00 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.83/57.00 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.83/57.00 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.83/57.00 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.83/57.00 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.83/57.00 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.83/57.00 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.83/57.00 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.83/57.00 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.83/57.00 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.83/57.00 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.83/57.00 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.83/57.00 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.83/57.00 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.83/57.00 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.83/57.00 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.83/57.00 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.83/57.00 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.83/57.00 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.83/57.00 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.83/57.02 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.83/57.02 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.83/57.02 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.83/57.02 (Eq (h (j e20)) e20)) % 56.83/57.02 (Eq (h (j e21)) e21)) % 56.83/57.02 (Eq (h (j e22)) e22)) % 56.83/57.02 (Eq (h (j e23)) e23)) % 56.83/57.02 (Eq (h (j e24)) e24)) % 56.83/57.02 (Eq (j (h e10)) e10)) % 56.83/57.02 (Eq (j (h e11)) e11)) % 56.83/57.02 (Eq (j (h e12)) e12)) % 56.83/57.02 True % 56.83/57.02 Clause #219 (by clausification #[217]): Eq (j (h e13)) e13 % 56.83/57.02 Clause #221 (by clausification #[215]): Eq % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.83/57.02 (Eq (op1 e10 e13) e11)) % 56.83/57.02 (Eq (op1 e10 e14) e14)) % 56.83/57.02 (Eq (op1 e11 e10) e10)) % 56.83/57.02 (Eq (op1 e11 e11) e14)) % 56.83/57.02 (Eq (op1 e11 e12) e11)) % 56.83/57.02 (Eq (op1 e11 e13) e12)) % 56.83/57.02 (Eq (op1 e11 e14) e13)) % 56.83/57.02 (Eq (op1 e12 e10) e11)) % 56.83/57.02 (Eq (op1 e12 e11) e13)) % 56.83/57.02 True % 56.83/57.02 Clause #223 (by clausification #[221]): Eq (Eq (op1 e12 e11) e13) True % 56.83/57.02 Clause #224 (by clausification #[221]): Eq % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.83/57.02 (Eq (op1 e10 e13) e11)) % 56.83/57.02 (Eq (op1 e10 e14) e14)) % 56.83/57.02 (Eq (op1 e11 e10) e10)) % 56.83/57.02 (Eq (op1 e11 e11) e14)) % 56.83/57.02 (Eq (op1 e11 e12) e11)) % 56.83/57.02 (Eq (op1 e11 e13) e12)) % 56.83/57.02 (Eq (op1 e11 e14) e13)) % 56.83/57.02 (Eq (op1 e12 e10) e11)) % 56.83/57.02 True % 56.83/57.02 Clause #225 (by clausification #[223]): Eq (op1 e12 e11) e13 % 56.83/57.02 Clause #226 (by clausification #[224]): Eq (Eq (op1 e12 e10) e11) True % 56.83/57.02 Clause #227 (by clausification #[224]): Eq % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.83/57.02 (Eq (op1 e10 e13) e11)) % 56.83/57.02 (Eq (op1 e10 e14) e14)) % 56.83/57.02 (Eq (op1 e11 e10) e10)) % 56.83/57.02 (Eq (op1 e11 e11) e14)) % 56.83/57.02 (Eq (op1 e11 e12) e11)) % 56.83/57.02 (Eq (op1 e11 e13) e12)) % 56.83/57.02 (Eq (op1 e11 e14) e13)) % 56.83/57.02 True % 56.83/57.02 Clause #228 (by clausification #[226]): Eq (op1 e12 e10) e11 % 56.83/57.02 Clause #230 (by clausification #[227]): Eq % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) % 56.83/57.02 (Eq (op1 e10 e13) e11)) % 56.83/57.02 (Eq (op1 e10 e14) e14)) % 56.83/57.02 (Eq (op1 e11 e10) e10)) % 56.83/57.02 (Eq (op1 e11 e11) e14)) % 56.83/57.02 (Eq (op1 e11 e12) e11)) % 56.83/57.02 (Eq (op1 e11 e13) e12)) % 56.83/57.02 True % 56.83/57.02 Clause #233 (by clausification #[230]): Eq % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And % 56.83/57.02 (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 56.83/57.02 (Eq (op1 e10 e14) e14)) % 56.83/57.02 (Eq (op1 e11 e10) e10)) % 56.83/57.02 (Eq (op1 e11 e11) e14)) % 56.83/57.02 (Eq (op1 e11 e12) e11)) % 56.83/57.02 True % 56.83/57.02 Clause #235 (by clausification #[166]): Eq (Or (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) (Eq (j e22) e14)) True % 56.83/57.02 Clause #237 (by clausification #[235]): Or (Eq (Or (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) (Eq (j e22) e13)) True) % 56.83/57.02 (Eq (Eq (j e22) e14) True) % 56.83/57.02 Clause #238 (by clausification #[237]): Or (Eq (Eq (j e22) e14) True) % 56.83/57.02 (Or (Eq (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) True) (Eq (Eq (j e22) e13) True)) % 56.83/57.02 Clause #239 (by clausification #[238]): Or (Eq (Or (Or (Eq (j e22) e10) (Eq (j e22) e11)) (Eq (j e22) e12)) True) % 56.83/57.02 (Or (Eq (Eq (j e22) e13) True) (Eq (j e22) e14)) % 56.83/57.02 Clause #240 (by clausification #[239]): Or (Eq (Eq (j e22) e13) True) % 56.83/57.02 (Or (Eq (j e22) e14) (Or (Eq (Or (Eq (j e22) e10) (Eq (j e22) e11)) True) (Eq (Eq (j e22) e12) True))) % 56.83/57.02 Clause #241 (by clausification #[240]): Or (Eq (j e22) e14) % 56.83/57.02 (Or (Eq (Or (Eq (j e22) e10) (Eq (j e22) e11)) True) (Or (Eq (Eq (j e22) e12) True) (Eq (j e22) e13))) % 56.91/57.06 Clause #242 (by clausification #[241]): Or (Eq (j e22) e14) % 56.91/57.06 (Or (Eq (Eq (j e22) e12) True) (Or (Eq (j e22) e13) (Or (Eq (Eq (j e22) e10) True) (Eq (Eq (j e22) e11) True)))) % 56.91/57.06 Clause #243 (by clausification #[242]): Or (Eq (j e22) e14) % 56.91/57.06 (Or (Eq (j e22) e13) (Or (Eq (Eq (j e22) e10) True) (Or (Eq (Eq (j e22) e11) True) (Eq (j e22) e12)))) % 56.91/57.06 Clause #244 (by clausification #[243]): Or (Eq (j e22) e14) (Or (Eq (j e22) e13) (Or (Eq (Eq (j e22) e11) True) (Or (Eq (j e22) e12) (Eq (j e22) e10)))) % 56.91/57.06 Clause #245 (by clausification #[244]): Or (Eq (j e22) e14) (Or (Eq (j e22) e13) (Or (Eq (j e22) e12) (Or (Eq (j e22) e10) (Eq (j e22) e11)))) % 56.91/57.06 Clause #251 (by clausification #[233]): Eq % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 56.91/57.06 (Eq (op1 e10 e14) e14)) % 56.91/57.06 (Eq (op1 e11 e10) e10)) % 56.91/57.06 (Eq (op1 e11 e11) e14)) % 56.91/57.06 True % 56.91/57.06 Clause #253 (by clausification #[200]): Eq (Eq (op2 e24 e21) e22) True % 56.91/57.06 Clause #255 (by clausification #[253]): Eq (op2 e24 e21) e22 % 56.91/57.06 Clause #256 (by clausification #[251]): Eq (Eq (op1 e11 e11) e14) True % 56.91/57.06 Clause #257 (by clausification #[251]): Eq % 56.91/57.06 (And % 56.91/57.06 (And (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 56.91/57.06 (Eq (op1 e10 e14) e14)) % 56.91/57.06 (Eq (op1 e11 e10) e10)) % 56.91/57.06 True % 56.91/57.06 Clause #258 (by clausification #[256]): Eq (op1 e11 e11) e14 % 56.91/57.06 Clause #260 (by clausification #[257]): Eq % 56.91/57.06 (And (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) % 56.91/57.06 (Eq (op1 e10 e14) e14)) % 56.91/57.06 True % 56.91/57.06 Clause #263 (by clausification #[260]): Eq (And (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) (Eq (op1 e10 e13) e11)) True % 56.91/57.06 Clause #266 (by clausification #[263]): Eq (And (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) (Eq (op1 e10 e12) e10)) True % 56.91/57.06 Clause #269 (by clausification #[266]): Eq (And (Eq (op1 e10 e10) e13) (Eq (op1 e10 e11) e12)) True % 56.91/57.06 Clause #271 (by clausification #[218]): Eq (Eq (j (h e12)) e12) True % 56.91/57.06 Clause #272 (by clausification #[218]): Eq % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (And % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 % 56.91/57.06 e10 % 56.91/57.06 e10)) % 56.91/57.06 (op2 % 56.91/57.06 (h % 56.91/57.06 e10) % 56.91/57.06 (h % 56.91/57.06 e10))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 % 56.91/57.06 e10 % 56.91/57.06 e11)) % 56.91/57.06 (op2 % 56.91/57.06 (h % 56.91/57.06 e10) % 56.91/57.06 (h % 56.91/57.06 e11)))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 % 56.91/57.06 e10 % 56.91/57.06 e12)) % 56.91/57.06 (op2 % 56.91/57.06 (h % 56.91/57.06 e10) % 56.91/57.06 (h % 56.91/57.06 e12)))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 % 56.91/57.06 e10 % 56.91/57.06 e13)) % 56.91/57.06 (op2 % 56.91/57.06 (h % 56.91/57.06 e10) % 56.91/57.06 (h % 56.91/57.06 e13)))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 e10 % 56.91/57.06 e14)) % 56.91/57.06 (op2 % 56.91/57.06 (h e10) % 56.91/57.06 (h % 56.91/57.06 e14)))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 e11 % 56.91/57.06 e10)) % 56.91/57.06 (op2 (h e11) % 56.91/57.06 (h e10)))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 e11 % 56.91/57.06 e11)) % 56.91/57.06 (op2 (h e11) % 56.91/57.06 (h e11)))) % 56.91/57.06 (Eq % 56.91/57.06 (h % 56.91/57.06 (op1 e11 e12)) % 56.91/57.06 (op2 (h e11) % 56.91/57.06 (h e12)))) % 56.91/57.06 (Eq % 56.91/57.06 (h (op1 e11 e13)) % 56.91/57.06 (op2 (h e11) % 56.91/57.06 (h e13)))) % 56.91/57.06 (Eq (h (op1 e11 e14)) % 56.91/57.06 (op2 (h e11) % 56.91/57.06 (h e14)))) % 56.91/57.06 (Eq (h (op1 e12 e10)) % 56.91/57.06 (op2 (h e12) % 56.91/57.06 (h e10)))) % 56.91/57.06 (Eq (h (op1 e12 e11)) % 56.91/57.06 (op2 (h e12) (h e11)))) % 56.91/57.06 (Eq (h (op1 e12 e12)) % 56.91/57.06 (op2 (h e12) (h e12)))) % 56.91/57.06 (Eq (h (op1 e12 e13)) % 56.91/57.06 (op2 (h e12) (h e13)))) % 56.91/57.06 (Eq (h (op1 e12 e14)) % 56.91/57.06 (op2 (h e12) (h e14)))) % 56.91/57.06 (Eq (h (op1 e13 e10)) % 56.91/57.06 (op2 (h e13) (h e10)))) % 56.91/57.06 (Eq (h (op1 e13 e11)) % 56.91/57.06 (op2 (h e13) (h e11)))) % 56.91/57.06 (Eq (h (op1 e13 e12)) % 56.91/57.06 (op2 (h e13) (h e12)))) % 56.91/57.06 (Eq (h (op1 e13 e13)) % 56.91/57.06 (op2 (h e13) (h e13)))) % 56.91/57.06 (Eq (h (op1 e13 e14)) % 56.91/57.06 (op2 (h e13) (h e14)))) % 56.93/57.09 (Eq (h (op1 e14 e10)) % 56.93/57.09 (op2 (h e14) (h e10)))) % 56.93/57.09 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 56.93/57.09 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 56.93/57.09 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 56.93/57.09 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 56.93/57.09 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.93/57.09 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.93/57.09 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.93/57.09 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.93/57.09 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.93/57.09 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.93/57.09 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.93/57.09 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.93/57.09 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.93/57.09 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.93/57.09 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.93/57.09 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.93/57.09 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.93/57.09 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.93/57.09 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.93/57.09 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.93/57.09 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.93/57.09 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.93/57.09 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.93/57.09 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.93/57.09 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.93/57.09 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.93/57.09 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.93/57.09 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.93/57.09 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.93/57.09 (Eq (h (j e20)) e20)) % 56.93/57.09 (Eq (h (j e21)) e21)) % 56.93/57.09 (Eq (h (j e22)) e22)) % 56.93/57.09 (Eq (h (j e23)) e23)) % 56.93/57.09 (Eq (h (j e24)) e24)) % 56.93/57.09 (Eq (j (h e10)) e10)) % 56.93/57.09 (Eq (j (h e11)) e11)) % 56.93/57.09 True % 56.93/57.09 Clause #273 (by clausification #[271]): Eq (j (h e12)) e12 % 56.93/57.09 Clause #275 (by clausification #[269]): Eq (Eq (op1 e10 e10) e13) True % 56.93/57.09 Clause #277 (by clausification #[275]): Eq (op1 e10 e10) e13 % 56.93/57.09 Clause #305 (by clausification #[272]): Eq (Eq (j (h e11)) e11) True % 56.93/57.09 Clause #306 (by clausification #[272]): Eq % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (And % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 % 56.93/57.09 e10 % 56.93/57.09 e10)) % 56.93/57.09 (op2 % 56.93/57.09 (h % 56.93/57.09 e10) % 56.93/57.09 (h % 56.93/57.09 e10))) % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 % 56.93/57.09 e10 % 56.93/57.09 e11)) % 56.93/57.09 (op2 % 56.93/57.09 (h % 56.93/57.09 e10) % 56.93/57.09 (h % 56.93/57.09 e11)))) % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 % 56.93/57.09 e10 % 56.93/57.09 e12)) % 56.93/57.09 (op2 % 56.93/57.09 (h % 56.93/57.09 e10) % 56.93/57.09 (h % 56.93/57.09 e12)))) % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 e10 % 56.93/57.09 e13)) % 56.93/57.09 (op2 % 56.93/57.09 (h e10) % 56.93/57.09 (h % 56.93/57.09 e13)))) % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 e10 % 56.93/57.09 e14)) % 56.93/57.09 (op2 (h e10) % 56.93/57.09 (h e14)))) % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 e11 % 56.93/57.09 e10)) % 56.93/57.09 (op2 (h e11) % 56.93/57.09 (h e10)))) % 56.93/57.09 (Eq % 56.93/57.09 (h % 56.93/57.09 (op1 e11 e11)) % 56.93/57.09 (op2 (h e11) % 56.93/57.09 (h e11)))) % 56.93/57.09 (Eq % 56.93/57.09 (h (op1 e11 e12)) % 56.93/57.09 (op2 (h e11) % 56.93/57.09 (h e12)))) % 56.93/57.09 (Eq (h (op1 e11 e13)) % 56.93/57.09 (op2 (h e11) % 56.93/57.09 (h e13)))) % 56.93/57.09 (Eq (h (op1 e11 e14)) % 56.93/57.09 (op2 (h e11) % 56.93/57.09 (h e14)))) % 56.93/57.09 (Eq (h (op1 e12 e10)) % 56.93/57.09 (op2 (h e12) (h e10)))) % 56.93/57.09 (Eq (h (op1 e12 e11)) % 56.93/57.09 (op2 (h e12) (h e11)))) % 56.93/57.09 (Eq (h (op1 e12 e12)) % 56.93/57.09 (op2 (h e12) (h e12)))) % 56.93/57.09 (Eq (h (op1 e12 e13)) % 56.93/57.09 (op2 (h e12) (h e13)))) % 56.93/57.09 (Eq (h (op1 e12 e14)) % 56.93/57.09 (op2 (h e12) (h e14)))) % 56.93/57.09 (Eq (h (op1 e13 e10)) % 56.93/57.09 (op2 (h e13) (h e10)))) % 56.93/57.09 (Eq (h (op1 e13 e11)) % 56.93/57.09 (op2 (h e13) (h e11)))) % 56.93/57.09 (Eq (h (op1 e13 e12)) % 56.93/57.09 (op2 (h e13) (h e12)))) % 56.93/57.09 (Eq (h (op1 e13 e13)) % 56.93/57.09 (op2 (h e13) (h e13)))) % 56.93/57.11 (Eq (h (op1 e13 e14)) % 56.93/57.11 (op2 (h e13) (h e14)))) % 56.93/57.11 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 56.93/57.11 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 56.93/57.11 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 56.93/57.11 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 56.93/57.11 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 56.93/57.11 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.93/57.11 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.93/57.11 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.93/57.11 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.93/57.11 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.93/57.11 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.93/57.11 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.93/57.11 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.93/57.11 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.93/57.11 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.93/57.11 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.93/57.11 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.93/57.11 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.93/57.11 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.93/57.11 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.93/57.11 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.93/57.11 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.93/57.11 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.93/57.11 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.93/57.11 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.93/57.11 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.93/57.11 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.93/57.11 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.93/57.11 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.93/57.11 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.93/57.11 (Eq (h (j e20)) e20)) % 56.93/57.11 (Eq (h (j e21)) e21)) % 56.93/57.11 (Eq (h (j e22)) e22)) % 56.93/57.11 (Eq (h (j e23)) e23)) % 56.93/57.11 (Eq (h (j e24)) e24)) % 56.93/57.11 (Eq (j (h e10)) e10)) % 56.93/57.11 True % 56.93/57.11 Clause #307 (by clausification #[305]): Eq (j (h e11)) e11 % 56.93/57.11 Clause #341 (by clausification #[306]): Eq (Eq (j (h e10)) e10) True % 56.93/57.11 Clause #342 (by clausification #[306]): Eq % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (And % 56.93/57.11 (Eq % 56.93/57.11 (h % 56.93/57.11 (op1 % 56.93/57.11 e10 % 56.93/57.11 e10)) % 56.93/57.11 (op2 % 56.93/57.11 (h % 56.93/57.11 e10) % 56.93/57.11 (h % 56.93/57.11 e10))) % 56.93/57.11 (Eq % 56.93/57.11 (h % 56.93/57.11 (op1 % 56.93/57.11 e10 % 56.93/57.11 e11)) % 56.93/57.11 (op2 % 56.93/57.11 (h % 56.93/57.11 e10) % 56.93/57.11 (h % 56.93/57.11 e11)))) % 56.93/57.11 (Eq % 56.93/57.11 (h % 56.93/57.11 (op1 e10 % 56.93/57.11 e12)) % 56.93/57.11 (op2 % 56.93/57.11 (h e10) % 56.93/57.11 (h % 56.93/57.11 e12)))) % 56.93/57.11 (Eq % 56.93/57.11 (h % 56.93/57.11 (op1 e10 % 56.93/57.11 e13)) % 56.93/57.12 (op2 (h e10) % 56.93/57.12 (h e13)))) % 56.93/57.12 (Eq % 56.93/57.12 (h % 56.93/57.12 (op1 e10 % 56.93/57.12 e14)) % 56.93/57.12 (op2 (h e10) % 56.93/57.12 (h e14)))) % 56.93/57.12 (Eq % 56.93/57.12 (h % 56.93/57.12 (op1 e11 e10)) % 56.93/57.12 (op2 (h e11) % 56.93/57.12 (h e10)))) % 56.93/57.12 (Eq % 56.93/57.12 (h (op1 e11 e11)) % 56.93/57.12 (op2 (h e11) % 56.93/57.12 (h e11)))) % 56.93/57.12 (Eq (h (op1 e11 e12)) % 56.93/57.12 (op2 (h e11) % 56.93/57.12 (h e12)))) % 56.93/57.12 (Eq (h (op1 e11 e13)) % 56.93/57.12 (op2 (h e11) % 56.93/57.12 (h e13)))) % 56.93/57.12 (Eq (h (op1 e11 e14)) % 56.93/57.12 (op2 (h e11) (h e14)))) % 56.93/57.12 (Eq (h (op1 e12 e10)) % 56.93/57.12 (op2 (h e12) (h e10)))) % 56.93/57.12 (Eq (h (op1 e12 e11)) % 56.93/57.12 (op2 (h e12) (h e11)))) % 56.93/57.12 (Eq (h (op1 e12 e12)) % 56.93/57.12 (op2 (h e12) (h e12)))) % 56.93/57.12 (Eq (h (op1 e12 e13)) % 56.93/57.12 (op2 (h e12) (h e13)))) % 56.93/57.12 (Eq (h (op1 e12 e14)) % 56.93/57.12 (op2 (h e12) (h e14)))) % 56.93/57.12 (Eq (h (op1 e13 e10)) % 56.93/57.12 (op2 (h e13) (h e10)))) % 56.93/57.12 (Eq (h (op1 e13 e11)) % 56.93/57.12 (op2 (h e13) (h e11)))) % 56.93/57.12 (Eq (h (op1 e13 e12)) % 56.93/57.12 (op2 (h e13) (h e12)))) % 56.93/57.12 (Eq (h (op1 e13 e13)) % 56.93/57.12 (op2 (h e13) (h e13)))) % 56.93/57.12 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 56.93/57.12 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 56.93/57.12 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 56.93/57.12 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 56.93/57.12 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 56.93/57.12 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 56.93/57.12 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 56.93/57.12 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 56.93/57.12 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 56.93/57.12 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 56.93/57.12 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 56.97/57.14 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 56.97/57.14 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 56.97/57.14 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 56.97/57.14 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 56.97/57.14 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 56.97/57.14 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 56.97/57.14 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 56.97/57.14 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 56.97/57.14 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 56.97/57.14 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 56.97/57.14 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 56.97/57.14 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 56.97/57.14 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 56.97/57.14 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 56.97/57.14 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 56.97/57.14 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 56.97/57.14 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 56.97/57.14 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 56.97/57.14 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 56.97/57.14 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 56.97/57.14 (Eq (h (j e20)) e20)) % 56.97/57.14 (Eq (h (j e21)) e21)) % 56.97/57.14 (Eq (h (j e22)) e22)) % 56.97/57.14 (Eq (h (j e23)) e23)) % 56.97/57.14 (Eq (h (j e24)) e24)) % 56.97/57.14 True % 56.97/57.14 Clause #343 (by clausification #[341]): Eq (j (h e10)) e10 % 56.97/57.14 Clause #375 (by clausification #[342]): Eq (Eq (h (j e24)) e24) True % 56.97/57.14 Clause #376 (by clausification #[342]): Eq % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (And % 56.97/57.14 (Eq % 56.97/57.14 (h % 56.97/57.14 (op1 e10 % 56.97/57.14 e10)) % 56.97/57.14 (op2 % 56.97/57.14 (h e10) % 56.97/57.14 (h % 56.97/57.14 e10))) % 56.97/57.14 (Eq % 56.97/57.14 (h % 56.97/57.14 (op1 e10 % 56.97/57.14 e11)) % 56.97/57.14 (op2 % 56.97/57.14 (h e10) % 56.97/57.14 (h % 56.97/57.14 e11)))) % 56.97/57.14 (Eq % 56.97/57.14 (h % 56.97/57.14 (op1 e10 % 56.97/57.14 e12)) % 56.97/57.14 (op2 (h e10) % 56.97/57.14 (h e12)))) % 56.97/57.14 (Eq % 56.97/57.14 (h % 56.97/57.14 (op1 e10 % 56.97/57.14 e13)) % 56.97/57.14 (op2 (h e10) % 56.97/57.14 (h e13)))) % 56.97/57.14 (Eq % 56.97/57.14 (h % 56.97/57.14 (op1 e10 e14)) % 56.97/57.14 (op2 (h e10) % 56.97/57.14 (h e14)))) % 56.97/57.14 (Eq % 56.97/57.14 (h (op1 e11 e10)) % 56.97/57.14 (op2 (h e11) % 56.97/57.14 (h e10)))) % 56.97/57.14 (Eq (h (op1 e11 e11)) % 56.97/57.14 (op2 (h e11) % 56.97/57.14 (h e11)))) % 56.97/57.14 (Eq (h (op1 e11 e12)) % 56.97/57.14 (op2 (h e11) % 56.97/57.14 (h e12)))) % 56.97/57.14 (Eq (h (op1 e11 e13)) % 56.97/57.14 (op2 (h e11) (h e13)))) % 56.97/57.14 (Eq (h (op1 e11 e14)) % 56.97/57.14 (op2 (h e11) (h e14)))) % 56.97/57.14 (Eq (h (op1 e12 e10)) % 56.97/57.14 (op2 (h e12) (h e10)))) % 56.97/57.14 (Eq (h (op1 e12 e11)) % 56.97/57.14 (op2 (h e12) (h e11)))) % 56.97/57.14 (Eq (h (op1 e12 e12)) % 56.97/57.14 (op2 (h e12) (h e12)))) % 56.97/57.14 (Eq (h (op1 e12 e13)) % 56.97/57.14 (op2 (h e12) (h e13)))) % 56.97/57.14 (Eq (h (op1 e12 e14)) % 56.97/57.14 (op2 (h e12) (h e14)))) % 56.97/57.14 (Eq (h (op1 e13 e10)) % 56.97/57.14 (op2 (h e13) (h e10)))) % 56.97/57.14 (Eq (h (op1 e13 e11)) % 56.97/57.14 (op2 (h e13) (h e11)))) % 56.97/57.14 (Eq (h (op1 e13 e12)) % 56.97/57.14 (op2 (h e13) (h e12)))) % 56.97/57.14 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.01/57.17 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.01/57.17 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.01/57.17 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.01/57.17 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.01/57.17 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.01/57.17 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.01/57.17 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.01/57.17 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.01/57.17 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.01/57.17 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.01/57.17 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.01/57.17 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.01/57.17 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.01/57.17 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.01/57.17 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.01/57.17 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.01/57.17 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.01/57.17 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.01/57.17 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.01/57.17 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.01/57.17 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.01/57.17 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.01/57.17 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.01/57.17 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.01/57.17 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.01/57.17 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.01/57.17 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.01/57.17 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.01/57.17 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.01/57.17 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 57.01/57.17 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 57.01/57.17 (Eq (h (j e20)) e20)) % 57.01/57.17 (Eq (h (j e21)) e21)) % 57.01/57.17 (Eq (h (j e22)) e22)) % 57.01/57.17 (Eq (h (j e23)) e23)) % 57.01/57.17 True % 57.01/57.17 Clause #377 (by clausification #[375]): Eq (h (j e24)) e24 % 57.01/57.17 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)))) % 57.01/57.17 Clause #410 (by clausification #[376]): Eq % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (And % 57.01/57.17 (Eq % 57.01/57.17 (h % 57.01/57.17 (op1 e10 % 57.01/57.17 e10)) % 57.01/57.17 (op2 (h e10) % 57.01/57.17 (h e10))) % 57.01/57.17 (Eq % 57.01/57.17 (h % 57.01/57.17 (op1 e10 % 57.01/57.17 e11)) % 57.01/57.17 (op2 (h e10) % 57.01/57.17 (h e11)))) % 57.01/57.17 (Eq % 57.01/57.17 (h % 57.01/57.17 (op1 e10 % 57.01/57.17 e12)) % 57.01/57.17 (op2 (h e10) % 57.01/57.17 (h e12)))) % 57.01/57.17 (Eq % 57.01/57.17 (h % 57.01/57.17 (op1 e10 e13)) % 57.01/57.17 (op2 (h e10) % 57.01/57.17 (h e13)))) % 57.01/57.17 (Eq % 57.01/57.17 (h (op1 e10 e14)) % 57.01/57.17 (op2 (h e10) % 57.01/57.17 (h e14)))) % 57.01/57.17 (Eq (h (op1 e11 e10)) % 57.01/57.17 (op2 (h e11) % 57.01/57.17 (h e10)))) % 57.01/57.17 (Eq (h (op1 e11 e11)) % 57.01/57.17 (op2 (h e11) % 57.01/57.17 (h e11)))) % 57.01/57.17 (Eq (h (op1 e11 e12)) % 57.01/57.17 (op2 (h e11) (h e12)))) % 57.01/57.17 (Eq (h (op1 e11 e13)) % 57.01/57.17 (op2 (h e11) (h e13)))) % 57.01/57.17 (Eq (h (op1 e11 e14)) % 57.01/57.17 (op2 (h e11) (h e14)))) % 57.01/57.17 (Eq (h (op1 e12 e10)) % 57.01/57.17 (op2 (h e12) (h e10)))) % 57.01/57.17 (Eq (h (op1 e12 e11)) % 57.01/57.17 (op2 (h e12) (h e11)))) % 57.01/57.17 (Eq (h (op1 e12 e12)) % 57.01/57.17 (op2 (h e12) (h e12)))) % 57.01/57.17 (Eq (h (op1 e12 e13)) % 57.01/57.17 (op2 (h e12) (h e13)))) % 57.01/57.17 (Eq (h (op1 e12 e14)) % 57.01/57.17 (op2 (h e12) (h e14)))) % 57.01/57.17 (Eq (h (op1 e13 e10)) % 57.01/57.17 (op2 (h e13) (h e10)))) % 57.01/57.17 (Eq (h (op1 e13 e11)) % 57.01/57.17 (op2 (h e13) (h e11)))) % 57.01/57.17 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.01/57.17 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.01/57.20 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.01/57.20 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.01/57.20 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.01/57.20 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.01/57.20 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.01/57.20 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.01/57.20 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.01/57.20 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.01/57.20 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.01/57.20 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.01/57.20 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.01/57.20 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.01/57.20 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.01/57.20 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.01/57.20 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.01/57.20 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.01/57.20 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.01/57.20 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.01/57.20 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.01/57.20 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.01/57.20 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.01/57.20 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.01/57.20 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.01/57.20 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.01/57.20 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.01/57.20 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.01/57.20 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.01/57.20 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.01/57.20 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.01/57.20 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 57.01/57.20 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 57.01/57.20 (Eq (h (j e20)) e20)) % 57.01/57.20 (Eq (h (j e21)) e21)) % 57.01/57.20 (Eq (h (j e22)) e22)) % 57.01/57.20 True % 57.01/57.20 Clause #465 (by clausification #[410]): Eq (Eq (h (j e22)) e22) True % 57.01/57.20 Clause #466 (by clausification #[410]): Eq % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (And % 57.01/57.20 (Eq % 57.01/57.20 (h % 57.01/57.20 (op1 e10 % 57.01/57.20 e10)) % 57.01/57.20 (op2 (h e10) % 57.01/57.20 (h e10))) % 57.01/57.20 (Eq % 57.01/57.20 (h % 57.01/57.20 (op1 e10 % 57.01/57.20 e11)) % 57.01/57.20 (op2 (h e10) % 57.01/57.20 (h e11)))) % 57.01/57.20 (Eq % 57.01/57.20 (h % 57.01/57.20 (op1 e10 e12)) % 57.01/57.20 (op2 (h e10) % 57.01/57.20 (h e12)))) % 57.01/57.20 (Eq % 57.01/57.20 (h (op1 e10 e13)) % 57.01/57.20 (op2 (h e10) % 57.01/57.20 (h e13)))) % 57.01/57.20 (Eq (h (op1 e10 e14)) % 57.01/57.20 (op2 (h e10) % 57.01/57.20 (h e14)))) % 57.01/57.20 (Eq (h (op1 e11 e10)) % 57.01/57.20 (op2 (h e11) % 57.01/57.20 (h e10)))) % 57.01/57.20 (Eq (h (op1 e11 e11)) % 57.01/57.20 (op2 (h e11) (h e11)))) % 57.01/57.20 (Eq (h (op1 e11 e12)) % 57.01/57.20 (op2 (h e11) (h e12)))) % 57.01/57.20 (Eq (h (op1 e11 e13)) % 57.01/57.20 (op2 (h e11) (h e13)))) % 57.01/57.20 (Eq (h (op1 e11 e14)) % 57.01/57.20 (op2 (h e11) (h e14)))) % 57.01/57.20 (Eq (h (op1 e12 e10)) % 57.01/57.20 (op2 (h e12) (h e10)))) % 57.01/57.20 (Eq (h (op1 e12 e11)) % 57.01/57.20 (op2 (h e12) (h e11)))) % 57.01/57.20 (Eq (h (op1 e12 e12)) % 57.01/57.20 (op2 (h e12) (h e12)))) % 57.01/57.20 (Eq (h (op1 e12 e13)) % 57.01/57.20 (op2 (h e12) (h e13)))) % 57.01/57.20 (Eq (h (op1 e12 e14)) % 57.01/57.20 (op2 (h e12) (h e14)))) % 57.01/57.20 (Eq (h (op1 e13 e10)) % 57.01/57.20 (op2 (h e13) (h e10)))) % 57.01/57.20 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 57.01/57.20 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.01/57.20 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.01/57.20 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.01/57.20 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.01/57.20 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.01/57.20 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.01/57.20 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.01/57.20 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.01/57.20 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.01/57.20 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.01/57.22 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.01/57.22 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.01/57.22 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.01/57.22 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.01/57.22 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.01/57.22 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.01/57.22 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.01/57.22 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.01/57.22 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.01/57.22 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.01/57.22 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.01/57.22 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.01/57.22 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.01/57.22 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.01/57.22 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.01/57.22 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.01/57.22 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.01/57.22 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.01/57.22 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.01/57.22 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.01/57.22 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.01/57.22 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 57.01/57.22 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 57.01/57.22 (Eq (h (j e20)) e20)) % 57.01/57.22 (Eq (h (j e21)) e21)) % 57.01/57.22 True % 57.01/57.22 Clause #467 (by clausification #[465]): Eq (h (j e22)) e22 % 57.01/57.22 Clause #468 (by superposition #[467, 245]): Or (Eq (j e22) e14) (Or (Eq (j e22) e12) (Or (Eq (j e22) e10) (Or (Eq (j e22) e11) (Eq (h e13) e22)))) % 57.01/57.22 Clause #469 (by superposition #[468, 467]): Or (Eq (j e22) e14) (Or (Eq (j e22) e12) (Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Eq (h e10) e22)))) % 57.01/57.22 Clause #473 (by superposition #[469, 467]): Or (Eq (j e22) e14) (Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq (h e12) e22)))) % 57.01/57.22 Clause #591 (by clausification #[466]): Eq % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (And % 57.01/57.22 (Eq % 57.01/57.22 (h % 57.01/57.22 (op1 e10 e10)) % 57.01/57.22 (op2 (h e10) % 57.01/57.22 (h e10))) % 57.01/57.22 (Eq % 57.01/57.22 (h % 57.01/57.22 (op1 e10 e11)) % 57.01/57.22 (op2 (h e10) % 57.01/57.22 (h e11)))) % 57.01/57.22 (Eq % 57.01/57.22 (h (op1 e10 e12)) % 57.01/57.22 (op2 (h e10) % 57.01/57.22 (h e12)))) % 57.01/57.22 (Eq (h (op1 e10 e13)) % 57.01/57.22 (op2 (h e10) % 57.01/57.22 (h e13)))) % 57.01/57.22 (Eq (h (op1 e10 e14)) % 57.01/57.22 (op2 (h e10) % 57.01/57.22 (h e14)))) % 57.01/57.22 (Eq (h (op1 e11 e10)) % 57.01/57.22 (op2 (h e11) (h e10)))) % 57.01/57.22 (Eq (h (op1 e11 e11)) % 57.01/57.22 (op2 (h e11) (h e11)))) % 57.01/57.22 (Eq (h (op1 e11 e12)) % 57.01/57.22 (op2 (h e11) (h e12)))) % 57.01/57.22 (Eq (h (op1 e11 e13)) % 57.01/57.22 (op2 (h e11) (h e13)))) % 57.01/57.22 (Eq (h (op1 e11 e14)) % 57.01/57.22 (op2 (h e11) (h e14)))) % 57.01/57.22 (Eq (h (op1 e12 e10)) % 57.01/57.22 (op2 (h e12) (h e10)))) % 57.01/57.22 (Eq (h (op1 e12 e11)) % 57.01/57.22 (op2 (h e12) (h e11)))) % 57.01/57.22 (Eq (h (op1 e12 e12)) % 57.01/57.22 (op2 (h e12) (h e12)))) % 57.01/57.22 (Eq (h (op1 e12 e13)) % 57.01/57.22 (op2 (h e12) (h e13)))) % 57.01/57.22 (Eq (h (op1 e12 e14)) % 57.01/57.22 (op2 (h e12) (h e14)))) % 57.01/57.22 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 57.01/57.22 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 57.01/57.22 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.01/57.22 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.01/57.22 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.01/57.22 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.01/57.22 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.01/57.22 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.01/57.22 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.01/57.22 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.01/57.22 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.01/57.22 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.01/57.22 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.01/57.22 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.01/57.22 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.01/57.22 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.01/57.22 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.01/57.22 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.01/57.22 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.01/57.22 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.01/57.22 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.01/57.22 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.01/57.22 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.01/57.22 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.01/57.22 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.01/57.22 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.01/57.22 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.01/57.22 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.01/57.22 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.09/57.25 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.09/57.25 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.09/57.25 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.09/57.25 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.09/57.25 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 57.09/57.25 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 57.09/57.25 (Eq (h (j e20)) e20)) % 57.09/57.25 True % 57.09/57.25 Clause #901 (by clausification #[591]): Eq % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (And % 57.09/57.25 (Eq % 57.09/57.25 (h (op1 e10 e10)) % 57.09/57.25 (op2 (h e10) % 57.09/57.25 (h e10))) % 57.09/57.25 (Eq % 57.09/57.25 (h (op1 e10 e11)) % 57.09/57.25 (op2 (h e10) % 57.09/57.25 (h e11)))) % 57.09/57.25 (Eq (h (op1 e10 e12)) % 57.09/57.25 (op2 (h e10) % 57.09/57.25 (h e12)))) % 57.09/57.25 (Eq (h (op1 e10 e13)) % 57.09/57.25 (op2 (h e10) % 57.09/57.25 (h e13)))) % 57.09/57.25 (Eq (h (op1 e10 e14)) % 57.09/57.25 (op2 (h e10) (h e14)))) % 57.09/57.25 (Eq (h (op1 e11 e10)) % 57.09/57.25 (op2 (h e11) (h e10)))) % 57.09/57.25 (Eq (h (op1 e11 e11)) % 57.09/57.25 (op2 (h e11) (h e11)))) % 57.09/57.25 (Eq (h (op1 e11 e12)) % 57.09/57.25 (op2 (h e11) (h e12)))) % 57.09/57.25 (Eq (h (op1 e11 e13)) % 57.09/57.25 (op2 (h e11) (h e13)))) % 57.09/57.25 (Eq (h (op1 e11 e14)) % 57.09/57.25 (op2 (h e11) (h e14)))) % 57.09/57.25 (Eq (h (op1 e12 e10)) % 57.09/57.25 (op2 (h e12) (h e10)))) % 57.09/57.25 (Eq (h (op1 e12 e11)) % 57.09/57.25 (op2 (h e12) (h e11)))) % 57.09/57.25 (Eq (h (op1 e12 e12)) % 57.09/57.25 (op2 (h e12) (h e12)))) % 57.09/57.25 (Eq (h (op1 e12 e13)) % 57.09/57.25 (op2 (h e12) (h e13)))) % 57.09/57.25 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 57.09/57.25 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 57.09/57.25 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 57.09/57.25 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.09/57.25 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.09/57.25 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.09/57.25 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.09/57.25 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.09/57.25 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.09/57.25 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.09/57.25 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.09/57.25 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.09/57.27 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.09/57.27 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.09/57.27 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.09/57.27 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.09/57.27 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.09/57.27 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.09/57.27 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.09/57.27 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.09/57.27 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.09/57.27 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.09/57.27 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.09/57.27 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.09/57.27 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.09/57.27 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.09/57.27 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.09/57.27 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.09/57.27 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.09/57.27 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.09/57.27 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.09/57.27 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.09/57.27 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.09/57.27 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.09/57.27 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 57.09/57.27 (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)))) % 57.09/57.27 True % 57.09/57.27 Clause #1925 (by clausification #[901]): Eq (Eq (j (op2 e24 e24)) (op1 (j e24) (j e24))) True % 57.09/57.27 Clause #1926 (by clausification #[901]): Eq % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (And % 57.09/57.27 (Eq (h (op1 e10 e10)) % 57.09/57.27 (op2 (h e10) % 57.09/57.27 (h e10))) % 57.09/57.27 (Eq (h (op1 e10 e11)) % 57.09/57.27 (op2 (h e10) % 57.09/57.27 (h e11)))) % 57.09/57.27 (Eq (h (op1 e10 e12)) % 57.09/57.27 (op2 (h e10) % 57.09/57.27 (h e12)))) % 57.09/57.27 (Eq (h (op1 e10 e13)) % 57.09/57.27 (op2 (h e10) (h e13)))) % 57.09/57.27 (Eq (h (op1 e10 e14)) % 57.09/57.27 (op2 (h e10) (h e14)))) % 57.09/57.27 (Eq (h (op1 e11 e10)) % 57.09/57.27 (op2 (h e11) (h e10)))) % 57.09/57.27 (Eq (h (op1 e11 e11)) % 57.09/57.27 (op2 (h e11) (h e11)))) % 57.09/57.27 (Eq (h (op1 e11 e12)) % 57.09/57.27 (op2 (h e11) (h e12)))) % 57.09/57.27 (Eq (h (op1 e11 e13)) % 57.09/57.27 (op2 (h e11) (h e13)))) % 57.09/57.27 (Eq (h (op1 e11 e14)) % 57.09/57.27 (op2 (h e11) (h e14)))) % 57.09/57.27 (Eq (h (op1 e12 e10)) % 57.09/57.27 (op2 (h e12) (h e10)))) % 57.09/57.27 (Eq (h (op1 e12 e11)) % 57.09/57.27 (op2 (h e12) (h e11)))) % 57.09/57.27 (Eq (h (op1 e12 e12)) % 57.09/57.27 (op2 (h e12) (h e12)))) % 57.09/57.27 (Eq (h (op1 e12 e13)) (op2 (h e12) (h e13)))) % 57.09/57.27 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 57.09/57.27 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 57.09/57.27 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 57.09/57.27 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.09/57.28 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.09/57.28 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.09/57.28 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.09/57.28 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.09/57.28 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.09/57.28 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.09/57.28 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.09/57.28 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.09/57.28 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.09/57.28 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.09/57.28 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.09/57.28 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.09/57.28 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.09/57.28 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.09/57.28 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.09/57.28 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.09/57.28 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.09/57.28 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.09/57.28 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.09/57.28 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.09/57.28 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.09/57.28 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.09/57.28 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.09/57.28 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.09/57.28 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.09/57.28 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.09/57.28 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.09/57.28 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.09/57.28 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.09/57.28 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.09/57.28 (Eq (j (op2 e24 e23)) (op1 (j e24) (j e23)))) % 57.09/57.28 True % 57.09/57.28 Clause #1927 (by clausification #[1925]): Eq (j (op2 e24 e24)) (op1 (j e24) (j e24)) % 57.09/57.28 Clause #1928 (by forward demodulation #[1927, 73]): Eq (j e24) (op1 (j e24) (j e24)) % 57.09/57.28 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 e10 (op1 e10 e10))))) % 57.09/57.28 Clause #2019 (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 e10 e13)))) % 57.09/57.28 Clause #2020 (by forward contextual literal cutting #[2019, 63]): Or (Eq (j e24) e14) (Or (Eq (j e24) e12) (Or (Eq (j e24) e11) (Eq (h e13) e24))) % 57.09/57.28 Clause #2021 (by superposition #[2020, 377]): Or (Eq (j e24) e14) (Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e12) e24))) % 57.09/57.28 Clause #2027 (by superposition #[2021, 1928]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq e14 (op1 e14 e14)))) % 57.09/57.28 Clause #2031 (by superposition #[2027, 57]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq e14 e11))) % 57.09/57.28 Clause #2032 (by forward contextual literal cutting #[2031, 48]): Or (Eq (j e24) e11) (Or (Eq (h e13) e24) (Eq (h e12) e24)) % 57.09/57.28 Clause #2034 (by superposition #[2032, 1928]): Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq e11 (op1 e11 e11))) % 57.09/57.28 Clause #2053 (by superposition #[2034, 258]): Or (Eq (h e13) e24) (Or (Eq (h e12) e24) (Eq e11 e14)) % 57.09/57.28 Clause #2054 (by forward contextual literal cutting #[2053, 48]): Or (Eq (h e13) e24) (Eq (h e12) e24) % 57.09/57.28 Clause #2055 (by superposition #[2054, 219]): Or (Eq (h e12) e24) (Eq (j e24) e13) % 57.15/57.30 Clause #2061 (by superposition #[2055, 1928]): Or (Eq (h e12) e24) (Eq e13 (op1 e13 e13)) % 57.15/57.30 Clause #2065 (by superposition #[2061, 198]): Or (Eq (h e12) e24) (Eq e13 e10) % 57.15/57.30 Clause #2066 (by forward contextual literal cutting #[2065, 63]): Eq (h e12) e24 % 57.15/57.30 Clause #2067 (by backward demodulation #[2066, 273]): Eq (j e24) e12 % 57.15/57.30 Clause #2074 (by backward demodulation #[2066, 473]): Or (Eq (j e22) e14) (Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq e24 e22)))) % 57.15/57.30 Clause #2250 (by forward contextual literal cutting #[2074, 11]): Or (Eq (j e22) e14) (Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Eq (h e10) e22))) % 57.15/57.30 Clause #4147 (by clausification #[1926]): Eq % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (And % 57.15/57.30 (Eq (h (op1 e10 e10)) % 57.15/57.30 (op2 (h e10) (h e10))) % 57.15/57.30 (Eq (h (op1 e10 e11)) % 57.15/57.30 (op2 (h e10) % 57.15/57.30 (h e11)))) % 57.15/57.30 (Eq (h (op1 e10 e12)) % 57.15/57.30 (op2 (h e10) (h e12)))) % 57.15/57.30 (Eq (h (op1 e10 e13)) % 57.15/57.30 (op2 (h e10) (h e13)))) % 57.15/57.30 (Eq (h (op1 e10 e14)) % 57.15/57.30 (op2 (h e10) (h e14)))) % 57.15/57.30 (Eq (h (op1 e11 e10)) % 57.15/57.30 (op2 (h e11) (h e10)))) % 57.15/57.30 (Eq (h (op1 e11 e11)) % 57.15/57.30 (op2 (h e11) (h e11)))) % 57.15/57.30 (Eq (h (op1 e11 e12)) % 57.15/57.30 (op2 (h e11) (h e12)))) % 57.15/57.30 (Eq (h (op1 e11 e13)) % 57.15/57.30 (op2 (h e11) (h e13)))) % 57.15/57.30 (Eq (h (op1 e11 e14)) % 57.15/57.30 (op2 (h e11) (h e14)))) % 57.15/57.30 (Eq (h (op1 e12 e10)) % 57.15/57.30 (op2 (h e12) (h e10)))) % 57.15/57.30 (Eq (h (op1 e12 e11)) % 57.15/57.30 (op2 (h e12) (h e11)))) % 57.15/57.30 (Eq (h (op1 e12 e12)) (op2 (h e12) (h e12)))) % 57.15/57.30 (Eq (h (op1 e12 e13)) (op2 (h e12) (h e13)))) % 57.15/57.30 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 57.15/57.30 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 57.15/57.30 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 57.15/57.30 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.15/57.30 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.15/57.30 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.15/57.30 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.15/57.30 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.15/57.30 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.15/57.30 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.15/57.30 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.15/57.30 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.15/57.30 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.15/57.30 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.15/57.30 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.15/57.30 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.15/57.30 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.15/57.30 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.15/57.30 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.15/57.30 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.15/57.30 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.15/57.30 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.15/57.33 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.15/57.33 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.15/57.33 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.15/57.33 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.15/57.33 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.15/57.33 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.15/57.33 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.15/57.33 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.15/57.33 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.15/57.33 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.15/57.33 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.15/57.33 (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)))) % 57.15/57.33 True % 57.15/57.33 Clause #4174 (by clausification #[4147]): Eq (Eq (j (op2 e24 e22)) (op1 (j e24) (j e22))) True % 57.15/57.33 Clause #4175 (by clausification #[4147]): Eq % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (And % 57.15/57.33 (Eq (h (op1 e10 e10)) % 57.15/57.33 (op2 (h e10) (h e10))) % 57.15/57.33 (Eq (h (op1 e10 e11)) % 57.15/57.33 (op2 (h e10) (h e11)))) % 57.15/57.33 (Eq (h (op1 e10 e12)) % 57.15/57.33 (op2 (h e10) (h e12)))) % 57.15/57.33 (Eq (h (op1 e10 e13)) % 57.15/57.33 (op2 (h e10) (h e13)))) % 57.15/57.33 (Eq (h (op1 e10 e14)) % 57.15/57.33 (op2 (h e10) (h e14)))) % 57.15/57.33 (Eq (h (op1 e11 e10)) % 57.15/57.33 (op2 (h e11) (h e10)))) % 57.15/57.33 (Eq (h (op1 e11 e11)) % 57.15/57.33 (op2 (h e11) (h e11)))) % 57.15/57.33 (Eq (h (op1 e11 e12)) % 57.15/57.33 (op2 (h e11) (h e12)))) % 57.15/57.33 (Eq (h (op1 e11 e13)) % 57.15/57.33 (op2 (h e11) (h e13)))) % 57.15/57.33 (Eq (h (op1 e11 e14)) % 57.15/57.33 (op2 (h e11) (h e14)))) % 57.15/57.33 (Eq (h (op1 e12 e10)) % 57.15/57.33 (op2 (h e12) (h e10)))) % 57.15/57.33 (Eq (h (op1 e12 e11)) (op2 (h e12) (h e11)))) % 57.15/57.33 (Eq (h (op1 e12 e12)) (op2 (h e12) (h e12)))) % 57.15/57.33 (Eq (h (op1 e12 e13)) (op2 (h e12) (h e13)))) % 57.15/57.33 (Eq (h (op1 e12 e14)) (op2 (h e12) (h e14)))) % 57.15/57.33 (Eq (h (op1 e13 e10)) (op2 (h e13) (h e10)))) % 57.15/57.33 (Eq (h (op1 e13 e11)) (op2 (h e13) (h e11)))) % 57.15/57.33 (Eq (h (op1 e13 e12)) (op2 (h e13) (h e12)))) % 57.15/57.33 (Eq (h (op1 e13 e13)) (op2 (h e13) (h e13)))) % 57.15/57.33 (Eq (h (op1 e13 e14)) (op2 (h e13) (h e14)))) % 57.15/57.33 (Eq (h (op1 e14 e10)) (op2 (h e14) (h e10)))) % 57.15/57.33 (Eq (h (op1 e14 e11)) (op2 (h e14) (h e11)))) % 57.15/57.33 (Eq (h (op1 e14 e12)) (op2 (h e14) (h e12)))) % 57.15/57.33 (Eq (h (op1 e14 e13)) (op2 (h e14) (h e13)))) % 57.15/57.33 (Eq (h (op1 e14 e14)) (op2 (h e14) (h e14)))) % 57.15/57.33 (Eq (j (op2 e20 e20)) (op1 (j e20) (j e20)))) % 57.15/57.33 (Eq (j (op2 e20 e21)) (op1 (j e20) (j e21)))) % 57.15/57.33 (Eq (j (op2 e20 e22)) (op1 (j e20) (j e22)))) % 57.15/57.33 (Eq (j (op2 e20 e23)) (op1 (j e20) (j e23)))) % 57.15/57.33 (Eq (j (op2 e20 e24)) (op1 (j e20) (j e24)))) % 57.15/57.33 (Eq (j (op2 e21 e20)) (op1 (j e21) (j e20)))) % 57.15/57.33 (Eq (j (op2 e21 e21)) (op1 (j e21) (j e21)))) % 57.15/57.33 (Eq (j (op2 e21 e22)) (op1 (j e21) (j e22)))) % 57.15/57.33 (Eq (j (op2 e21 e23)) (op1 (j e21) (j e23)))) % 57.15/57.33 (Eq (j (op2 e21 e24)) (op1 (j e21) (j e24)))) % 57.15/57.33 (Eq (j (op2 e22 e20)) (op1 (j e22) (j e20)))) % 57.15/57.33 (Eq (j (op2 e22 e21)) (op1 (j e22) (j e21)))) % 57.21/57.36 (Eq (j (op2 e22 e22)) (op1 (j e22) (j e22)))) % 57.21/57.36 (Eq (j (op2 e22 e23)) (op1 (j e22) (j e23)))) % 57.21/57.36 (Eq (j (op2 e22 e24)) (op1 (j e22) (j e24)))) % 57.21/57.36 (Eq (j (op2 e23 e20)) (op1 (j e23) (j e20)))) % 57.21/57.36 (Eq (j (op2 e23 e21)) (op1 (j e23) (j e21)))) % 57.21/57.36 (Eq (j (op2 e23 e22)) (op1 (j e23) (j e22)))) % 57.21/57.36 (Eq (j (op2 e23 e23)) (op1 (j e23) (j e23)))) % 57.21/57.36 (Eq (j (op2 e23 e24)) (op1 (j e23) (j e24)))) % 57.21/57.36 (Eq (j (op2 e24 e20)) (op1 (j e24) (j e20)))) % 57.21/57.36 (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)))) % 57.21/57.36 True % 57.21/57.36 Clause #4176 (by clausification #[4174]): Eq (j (op2 e24 e22)) (op1 (j e24) (j e22)) % 57.21/57.36 Clause #4177 (by forward demodulation #[4176, 201]): Eq (j e21) (op1 (j e24) (j e22)) % 57.21/57.36 Clause #4178 (by forward demodulation #[4177, 2067]): Eq (j e21) (op1 e12 (j e22)) % 57.21/57.36 Clause #4183 (by superposition #[4178, 2250]): Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq (j e21) (op1 e12 e14)))) % 57.21/57.36 Clause #4401 (by superposition #[4183, 213]): Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq (j e21) e10))) % 57.21/57.36 Clause #4803 (by clausification #[4175]): Eq (Eq (j (op2 e24 e21)) (op1 (j e24) (j e21))) True % 57.21/57.36 Clause #4805 (by clausification #[4803]): Eq (j (op2 e24 e21)) (op1 (j e24) (j e21)) % 57.21/57.36 Clause #4806 (by forward demodulation #[4805, 255]): Eq (j e22) (op1 (j e24) (j e21)) % 57.21/57.36 Clause #4807 (by forward demodulation #[4806, 2067]): Eq (j e22) (op1 e12 (j e21)) % 57.21/57.36 Clause #4822 (by superposition #[4807, 4401]): Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq (j e22) (op1 e12 e10)))) % 57.21/57.36 Clause #4840 (by superposition #[4822, 228]): Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq (j e22) e11))) % 57.21/57.36 Clause #4844 (by eliminate duplicate literals #[4840]): Or (Eq (j e22) e11) (Or (Eq (h e13) e22) (Eq (h e10) e22)) % 57.21/57.36 Clause #4845 (by superposition #[4844, 467]): Or (Eq (h e13) e22) (Or (Eq (h e10) e22) (Eq (h e11) e22)) % 57.21/57.36 Clause #4854 (by superposition #[4845, 219]): Or (Eq (h e10) e22) (Or (Eq (h e11) e22) (Eq (j e22) e13)) % 57.21/57.36 Clause #4872 (by superposition #[4854, 4178]): Or (Eq (h e10) e22) (Or (Eq (h e11) e22) (Eq (j e21) (op1 e12 e13))) % 57.21/57.36 Clause #4910 (by superposition #[4872, 216]): Or (Eq (h e10) e22) (Or (Eq (h e11) e22) (Eq (j e21) e14)) % 57.21/57.36 Clause #4924 (by superposition #[4910, 4807]): Or (Eq (h e10) e22) (Or (Eq (h e11) e22) (Eq (j e22) (op1 e12 e14))) % 57.21/57.36 Clause #4942 (by superposition #[4924, 213]): Or (Eq (h e10) e22) (Or (Eq (h e11) e22) (Eq (j e22) e10)) % 57.21/57.36 Clause #4945 (by superposition #[4942, 467]): Or (Eq (h e10) e22) (Or (Eq (h e11) e22) (Eq (h e10) e22)) % 57.21/57.36 Clause #4951 (by eliminate duplicate literals #[4945]): Or (Eq (h e10) e22) (Eq (h e11) e22) % 57.21/57.36 Clause #4952 (by superposition #[4951, 343]): Or (Eq (h e11) e22) (Eq (j e22) e10) % 57.21/57.36 Clause #4961 (by superposition #[4952, 4178]): Or (Eq (h e11) e22) (Eq (j e21) (op1 e12 e10)) % 57.21/57.36 Clause #4966 (by superposition #[4961, 228]): Or (Eq (h e11) e22) (Eq (j e21) e11) % 57.21/57.36 Clause #4976 (by superposition #[4966, 4807]): Or (Eq (h e11) e22) (Eq (j e22) (op1 e12 e11)) % 57.21/57.36 Clause #4979 (by superposition #[4976, 225]): Or (Eq (h e11) e22) (Eq (j e22) e13) % 57.21/57.36 Clause #4990 (by superposition #[4979, 4952]): Or (Eq (h e11) e22) (Or (Eq (h e11) e22) (Eq e13 e10)) % 57.21/57.36 Clause #5001 (by eliminate duplicate literals #[4990]): Or (Eq (h e11) e22) (Eq e13 e10) % 57.21/57.36 Clause #5002 (by forward contextual literal cutting #[5001, 63]): Eq (h e11) e22 % 57.21/57.36 Clause #5003 (by backward demodulation #[5002, 307]): Eq (j e22) e11 % 57.21/57.36 Clause #5046 (by backward demodulation #[5003, 4178]): Eq (j e21) (op1 e12 e11) % 57.21/57.36 Clause #5047 (by backward demodulation #[5003, 4807]): Eq e11 (op1 e12 (j e21)) % 57.21/57.36 Clause #5060 (by superposition #[5046, 225]): Eq (j e21) e13 % 57.21/57.36 Clause #5080 (by backward demodulation #[5060, 5047]): Eq e11 (op1 e12 e13) % 57.21/57.36 Clause #5108 (by superposition #[5080, 216]): Eq e11 e14 % 57.21/57.36 Clause #5110 (by forward contextual literal cutting #[5108, 48]): False % 57.21/57.36 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------