%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : HWC001-1 : TPTP v8.1.0. Bugfixed v1.1.1. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 13:07:25 EDT 2022 % Result : Unsatisfiable 28.65s 28.08s % Output : Proof 28.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : HWC001-1 : TPTP v8.1.0. Bugfixed v1.1.1. % 0.04/0.13 % Command : moca.sh %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 9 12:55:06 EDT 2022 % 0.13/0.34 % CPUTime : % 28.65/28.08 % SZS status Unsatisfiable % 28.65/28.08 % SZS output start Proof % 28.65/28.08 The input problem is unsatisfiable because % 28.65/28.08 % 28.65/28.08 [1] the following set of Horn clauses is unsatisfiable: % 28.65/28.08 % 28.65/28.08 nand(X, Y) = not(and(X, Y)) % 28.65/28.08 and(X, n0) = n0 % 28.65/28.08 and(X, n1) = X % 28.65/28.08 not(n0) = n1 % 28.65/28.08 not(n1) = n0 % 28.65/28.08 output(X1, X2, X3, X4) & output(Y1, Y2, Y3, Y4) ==> output(nand(X1, Y1), nand(X2, Y2), nand(X3, Y3), nand(X4, Y4)) % 28.65/28.08 output(n0, n0, n1, n1) % 28.65/28.08 output(n0, n1, n0, n1) % 28.65/28.08 output(n0, n1, n1, n1) ==> \bottom % 28.65/28.08 % 28.65/28.08 This holds because % 28.65/28.08 % 28.65/28.08 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 28.65/28.08 % 28.65/28.08 E: % 28.65/28.08 and(X, n0) = n0 % 28.65/28.08 and(X, n1) = X % 28.65/28.08 f1(true__, X1, Y1, X2, Y2, X3, Y3, X4, Y4) = output(nand(X1, Y1), nand(X2, Y2), nand(X3, Y3), nand(X4, Y4)) % 28.65/28.08 f2(output(Y1, Y2, Y3, Y4), X1, X2, X3, X4, Y1, Y2, Y3, Y4) = true__ % 28.65/28.08 f2(true__, X1, X2, X3, X4, Y1, Y2, Y3, Y4) = f1(output(X1, X2, X3, X4), X1, Y1, X2, Y2, X3, Y3, X4, Y4) % 28.65/28.08 f3(output(n0, n1, n1, n1)) = true__ % 28.65/28.08 f3(true__) = false__ % 28.65/28.08 nand(X, Y) = not(and(X, Y)) % 28.65/28.08 not(n0) = n1 % 28.65/28.08 not(n1) = n0 % 28.65/28.08 output(n0, n0, n1, n1) = true__ % 28.65/28.08 output(n0, n1, n0, n1) = true__ % 28.65/28.08 G: % 28.65/28.08 true__ = false__ % 28.65/28.08 % 28.65/28.08 This holds because % 28.65/28.08 % 28.65/28.08 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 28.65/28.08 % 28.65/28.08 % 28.65/28.08 and(X, n0) -> n0 % 28.65/28.08 and(X, n1) -> X % 28.65/28.08 and(Y0, not(n1)) -> not(n1) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, X1, X2, n1), not(and(n1, X0)), Y4, not(and(n1, X1)), Y5, not(and(n1, X2)), Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(and(n1, X1)), not(and(n1, X2)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, X1, n1, n1), not(and(n1, X0)), Y4, not(and(n1, X1)), Y5, not(n1), Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(and(n1, X1)), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, X1, not(n1), n1), not(and(n1, X0)), Y4, not(and(n1, X1)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(and(n1, X1)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, n1, X1, n1), not(and(n1, X0)), Y4, not(n1), Y5, not(and(n1, X1)), Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(n1), not(and(n1, X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, n1, n1, n1), not(and(n1, X0)), Y4, not(n1), Y5, not(n1), Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(n1), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, n1, not(n1), n1), not(and(n1, X0)), Y4, not(n1), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(n1), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, not(n1), X1, n1), not(and(n1, X0)), Y4, n1, Y5, not(and(n1, X1)), Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), n1, not(and(n1, X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, not(n1), n1, n1), not(and(n1, X0)), Y4, n1, Y5, not(n1), Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), n1, not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, not(n1), not(n1), X1), not(and(n1, X0)), Y4, n1, Y5, n1, Y6, not(and(not(n1), X1)), Y7) -> f2(true__, not(and(n1, X0)), n1, n1, not(and(not(n1), X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, not(n1), not(n1), n1), not(and(n1, X0)), Y4, n1, Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), X0, not(n1), not(n1), not(n1)), not(and(n1, X0)), Y4, n1, Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, X0, X1, n1), not(n1), Y4, not(and(n1, X0)), Y5, not(and(n1, X1)), Y6, n1, Y7) -> f2(true__, not(n1), not(and(n1, X0)), not(and(n1, X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, X0, n1, n1), not(n1), Y4, not(and(n1, X0)), Y5, not(n1), Y6, n1, Y7) -> f2(true__, not(n1), not(and(n1, X0)), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, X0, not(n1), n1), not(n1), Y4, not(and(n1, X0)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(n1), not(and(n1, X0)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, n1, X0, n1), not(n1), Y4, not(n1), Y5, not(and(n1, X0)), Y6, n1, Y7) -> f2(true__, not(n1), not(n1), not(and(n1, X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, n1, n1, X0), not(n1), Y4, not(n1), Y5, not(n1), Y6, not(and(not(n1), X0)), Y7) -> f2(true__, not(n1), not(n1), not(n1), not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, n1, not(n1), X0), not(n1), Y4, not(n1), Y5, n1, Y6, not(and(not(n1), X0)), Y7) -> f2(true__, not(n1), not(n1), n1, not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, not(n1), X0, n1), not(n1), Y4, n1, Y5, not(and(n1, X0)), Y6, n1, Y7) -> f2(true__, not(n1), n1, not(and(n1, X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, not(n1), n1, X0), not(n1), Y4, n1, Y5, not(n1), Y6, not(and(not(n1), X0)), Y7) -> f2(true__, not(n1), n1, not(n1), not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), X0), not(n1), Y4, n1, Y5, n1, Y6, not(and(not(n1), X0)), Y7) -> f2(true__, not(n1), n1, n1, not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), X0, X1, n1), n1, Y4, not(and(n1, X0)), Y5, not(and(n1, X1)), Y6, n1, Y7) -> f2(true__, n1, not(and(n1, X0)), not(and(n1, X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), X0, n1, n1), n1, Y4, not(and(n1, X0)), Y5, not(n1), Y6, n1, Y7) -> f2(true__, n1, not(and(n1, X0)), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), X0, not(n1), X1), n1, Y4, not(and(n1, X0)), Y5, n1, Y6, not(and(not(n1), X1)), Y7) -> f2(true__, n1, not(and(n1, X0)), n1, not(and(not(n1), X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), n1, X0, X1), n1, Y4, not(n1), Y5, not(and(n1, X0)), Y6, not(and(not(n1), X1)), Y7) -> f2(true__, n1, not(n1), not(and(n1, X0)), not(and(not(n1), X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), n1, X0, n1), n1, Y4, not(n1), Y5, not(and(n1, X0)), Y6, n1, Y7) -> f2(true__, n1, not(n1), not(and(n1, X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), n1, n1, X0), n1, Y4, not(n1), Y5, not(n1), Y6, not(and(not(n1), X0)), Y7) -> f2(true__, n1, not(n1), not(n1), not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), n1, n1, n1), n1, Y4, not(n1), Y5, not(n1), Y6, n1, Y7) -> f2(true__, n1, not(n1), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), n1, not(n1), X0), n1, Y4, not(n1), Y5, n1, Y6, not(and(not(n1), X0)), Y7) -> f2(true__, n1, not(n1), n1, not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), X0, X1), n1, Y4, n1, Y5, not(and(n1, X0)), Y6, not(and(not(n1), X1)), Y7) -> f2(true__, n1, n1, not(and(n1, X0)), not(and(not(n1), X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), n1, X0), n1, Y4, n1, Y5, not(n1), Y6, not(and(not(n1), X0)), Y7) -> f2(true__, n1, n1, not(n1), not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), X0), n1, Y4, n1, Y5, n1, Y6, not(and(not(n1), X0)), Y7) -> f2(true__, n1, n1, n1, not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), X0, X1, n1, not(n1)), not(and(n1, X0)), Y4, not(and(n1, X1)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(and(n1, X1)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), X0, X1, not(n1), n1), not(and(n1, X0)), Y4, not(and(n1, X1)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(and(n1, X1)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), X0, n1, n1, not(n1)), not(and(n1, X0)), Y4, not(n1), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(n1), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), X0, n1, not(n1), n1), not(and(n1, X0)), Y4, not(n1), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), not(n1), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), n1, not(n1)), not(and(n1, X0)), Y4, n1, Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), not(n1), n1), not(and(n1, X0)), Y4, n1, Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(n1, X0)), n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), n1, X0, n1, not(n1)), not(n1), Y4, not(and(n1, X0)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(n1), not(and(n1, X0)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), n1, X0, not(n1), n1), not(n1), Y4, not(and(n1, X0)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(n1), not(and(n1, X0)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), n1, n1, X0, n1), not(n1), Y4, not(n1), Y5, not(and(not(n1), X0)), Y6, n1, Y7) -> f2(true__, not(n1), not(n1), not(and(not(n1), X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), X0, n1), not(n1), Y4, n1, Y5, not(and(not(n1), X0)), Y6, n1, Y7) -> f2(true__, not(n1), n1, not(and(not(n1), X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, X0), not(n1), Y4, n1, Y5, n1, Y6, not(and(not(n1), X0)), Y7) -> f2(true__, not(n1), n1, n1, not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, X0), n1, Y4, n1, Y5, n1, Y6, not(and(not(n1), X0)), Y7) -> f2(true__, n1, n1, n1, not(and(not(n1), X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, X1, X2, X3), not(and(not(n1), X0)), Y4, not(and(n1, X1)), Y5, not(and(not(n1), X2)), Y6, not(and(n1, X3)), Y7) -> f2(true__, not(and(not(n1), X0)), not(and(n1, X1)), not(and(not(n1), X2)), not(and(n1, X3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, X1, n1, X2), not(and(not(n1), X0)), Y4, not(and(n1, X1)), Y5, n1, Y6, not(and(n1, X2)), Y7) -> f2(true__, not(and(not(n1), X0)), not(and(n1, X1)), n1, not(and(n1, X2)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, X1, n1, n1), not(and(not(n1), X0)), Y4, not(and(n1, X1)), Y5, n1, Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), not(and(n1, X1)), n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, X1, n1, not(n1)), not(and(not(n1), X0)), Y4, not(and(n1, X1)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), not(and(n1, X1)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, n1, n1, X1), not(and(not(n1), X0)), Y4, not(n1), Y5, n1, Y6, not(and(n1, X1)), Y7) -> f2(true__, not(and(not(n1), X0)), not(n1), n1, not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, n1, n1, n1), not(and(not(n1), X0)), Y4, not(n1), Y5, n1, Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), not(n1), n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, n1, n1, not(n1)), not(and(not(n1), X0)), Y4, not(n1), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), not(n1), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), X1, n1), not(and(not(n1), X0)), Y4, n1, Y5, not(and(not(n1), X1)), Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(and(not(n1), X1)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), X1, not(n1)), not(and(not(n1), X0)), Y4, n1, Y5, not(and(not(n1), X1)), Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(and(not(n1), X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), n1, X1), not(and(not(n1), X0)), Y4, n1, Y5, n1, Y6, not(and(n1, X1)), Y7) -> f2(true__, not(and(not(n1), X0)), n1, n1, not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), n1, n1), not(and(not(n1), X0)), Y4, n1, Y5, n1, Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), n1, n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), n1, not(n1)), not(and(not(n1), X0)), Y4, n1, Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, Y2, n1), not(and(not(n1), Y0)), Y4, not(and(n1, Y1)), Y5, not(and(not(n1), Y2)), Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, Y2, not(n1)), not(and(not(n1), Y0)), Y4, not(and(n1, Y1)), Y5, not(and(not(n1), Y2)), Y6, n1, Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, not(n1), Y3), not(and(not(n1), Y0)), Y4, not(and(n1, Y1)), Y5, n1, Y6, not(and(n1, Y3)), Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(n1, Y1)), n1, not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, Y0, n1, Y2, Y3), not(and(not(n1), Y0)), Y4, not(n1), Y5, not(and(not(n1), Y2)), Y6, not(and(n1, Y3)), Y7) -> f2(true__, not(and(not(n1), Y0)), not(n1), not(and(not(n1), Y2)), not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), Y2, Y3), not(and(not(n1), Y0)), Y4, n1, Y5, not(and(not(n1), Y2)), Y6, not(and(n1, Y3)), Y7) -> f2(true__, not(and(not(n1), Y0)), n1, not(and(not(n1), Y2)), not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, X0, X1, X2), n1, Y4, not(and(n1, X0)), Y5, not(and(not(n1), X1)), Y6, not(and(n1, X2)), Y7) -> f2(true__, n1, not(and(n1, X0)), not(and(not(n1), X1)), not(and(n1, X2)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, X0, X1, n1), n1, Y4, not(and(n1, X0)), Y5, not(and(not(n1), X1)), Y6, not(n1), Y7) -> f2(true__, n1, not(and(n1, X0)), not(and(not(n1), X1)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, X0, X1, not(n1)), n1, Y4, not(and(n1, X0)), Y5, not(and(not(n1), X1)), Y6, n1, Y7) -> f2(true__, n1, not(and(n1, X0)), not(and(not(n1), X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, X0, n1, X1), n1, Y4, not(and(n1, X0)), Y5, n1, Y6, not(and(n1, X1)), Y7) -> f2(true__, n1, not(and(n1, X0)), n1, not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, X0, n1, n1), n1, Y4, not(and(n1, X0)), Y5, n1, Y6, not(n1), Y7) -> f2(true__, n1, not(and(n1, X0)), n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, X0, n1, not(n1)), n1, Y4, not(and(n1, X0)), Y5, n1, Y6, n1, Y7) -> f2(true__, n1, not(and(n1, X0)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, n1, X0, X1), n1, Y4, not(n1), Y5, not(and(not(n1), X0)), Y6, not(and(n1, X1)), Y7) -> f2(true__, n1, not(n1), not(and(not(n1), X0)), not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, n1, X0, n1), n1, Y4, not(n1), Y5, not(and(not(n1), X0)), Y6, not(n1), Y7) -> f2(true__, n1, not(n1), not(and(not(n1), X0)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, n1, X0, not(n1)), n1, Y4, not(n1), Y5, not(and(not(n1), X0)), Y6, n1, Y7) -> f2(true__, n1, not(n1), not(and(not(n1), X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, n1, n1, X0), n1, Y4, not(n1), Y5, n1, Y6, not(and(n1, X0)), Y7) -> f2(true__, n1, not(n1), n1, not(and(n1, X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), X0, X1), n1, Y4, n1, Y5, not(and(not(n1), X0)), Y6, not(and(n1, X1)), Y7) -> f2(true__, n1, n1, not(and(not(n1), X0)), not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), X0, n1), n1, Y4, n1, Y5, not(and(not(n1), X0)), Y6, not(n1), Y7) -> f2(true__, n1, n1, not(and(not(n1), X0)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), X0, not(n1)), n1, Y4, n1, Y5, not(and(not(n1), X0)), Y6, n1, Y7) -> f2(true__, n1, n1, not(and(not(n1), X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), n1, X0), n1, Y4, n1, Y5, n1, Y6, not(and(n1, X0)), Y7) -> f2(true__, n1, n1, n1, not(and(n1, X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), n1, not(n1), n1, not(n1), Y1, Y2, Y3), n1, Y4, not(and(n1, Y1)), Y5, not(and(not(n1), Y2)), Y6, not(and(n1, Y3)), Y7) -> f2(true__, n1, not(and(n1, Y1)), not(and(not(n1), Y2)), not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, X1, X2, X3), not(and(not(n1), X0)), Y4, not(and(not(n1), X1)), Y5, not(and(n1, X2)), Y6, not(and(n1, X3)), Y7) -> f2(true__, not(and(not(n1), X0)), not(and(not(n1), X1)), not(and(n1, X2)), not(and(n1, X3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, X1, n1, not(n1)), not(and(not(n1), X0)), Y4, not(and(not(n1), X1)), Y5, not(n1), Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), not(and(not(n1), X1)), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, X1, not(n1), n1), not(and(not(n1), X0)), Y4, not(and(not(n1), X1)), Y5, n1, Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), not(and(not(n1), X1)), n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, X1, not(n1), not(n1)), not(and(not(n1), X0)), Y4, not(and(not(n1), X1)), Y5, n1, Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), not(and(not(n1), X1)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, X1, X2), not(and(not(n1), X0)), Y4, n1, Y5, not(and(n1, X1)), Y6, not(and(n1, X2)), Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(and(n1, X1)), not(and(n1, X2)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, X1, n1), not(and(not(n1), X0)), Y4, n1, Y5, not(and(n1, X1)), Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(and(n1, X1)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, X1, not(n1)), not(and(not(n1), X0)), Y4, n1, Y5, not(and(n1, X1)), Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(and(n1, X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, n1, X1), not(and(not(n1), X0)), Y4, n1, Y5, not(n1), Y6, not(and(n1, X1)), Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(n1), not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, n1, n1), not(and(not(n1), X0)), Y4, n1, Y5, not(n1), Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(n1), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, n1, not(n1)), not(and(not(n1), X0)), Y4, n1, Y5, not(n1), Y6, n1, Y7) -> f2(true__, not(and(not(n1), X0)), n1, not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, X0, n1, not(n1), X1), not(and(not(n1), X0)), Y4, n1, Y5, n1, Y6, not(and(n1, X1)), Y7) -> f2(true__, not(and(not(n1), X0)), n1, n1, not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, Y2, n1), not(and(not(n1), Y0)), Y4, not(and(not(n1), Y1)), Y5, not(and(n1, Y2)), Y6, not(n1), Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, Y2, not(n1)), not(and(not(n1), Y0)), Y4, not(and(not(n1), Y1)), Y5, not(and(n1, Y2)), Y6, n1, Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, n1, Y3), not(and(not(n1), Y0)), Y4, not(and(not(n1), Y1)), Y5, not(n1), Y6, not(and(n1, Y3)), Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(n1), not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, not(n1), Y3), not(and(not(n1), Y0)), Y4, not(and(not(n1), Y1)), Y5, n1, Y6, not(and(n1, Y3)), Y7) -> f2(true__, not(and(not(n1), Y0)), not(and(not(n1), Y1)), n1, not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), Y2, Y3), not(and(not(n1), Y0)), Y4, n1, Y5, not(and(n1, Y2)), Y6, not(and(n1, Y3)), Y7) -> f2(true__, not(and(not(n1), Y0)), n1, not(and(n1, Y2)), not(and(n1, Y3)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, X1, X2), n1, Y4, not(and(not(n1), X0)), Y5, not(and(n1, X1)), Y6, not(and(n1, X2)), Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(and(n1, X1)), not(and(n1, X2)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, X1, n1), n1, Y4, not(and(not(n1), X0)), Y5, not(and(n1, X1)), Y6, not(n1), Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(and(n1, X1)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, X1, not(n1)), n1, Y4, not(and(not(n1), X0)), Y5, not(and(n1, X1)), Y6, n1, Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(and(n1, X1)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, n1, X1), n1, Y4, not(and(not(n1), X0)), Y5, not(n1), Y6, not(and(n1, X1)), Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(n1), not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, n1, n1), n1, Y4, not(and(not(n1), X0)), Y5, not(n1), Y6, not(n1), Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(n1), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, n1, not(n1)), n1, Y4, not(and(not(n1), X0)), Y5, not(n1), Y6, n1, Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, not(n1), X1), n1, Y4, not(and(not(n1), X0)), Y5, n1, Y6, not(and(n1, X1)), Y7) -> f2(true__, n1, not(and(not(n1), X0)), n1, not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, not(n1), n1), n1, Y4, not(and(not(n1), X0)), Y5, n1, Y6, not(n1), Y7) -> f2(true__, n1, not(and(not(n1), X0)), n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, X0, not(n1), not(n1)), n1, Y4, not(and(not(n1), X0)), Y5, n1, Y6, n1, Y7) -> f2(true__, n1, not(and(not(n1), X0)), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, n1, X0, X1), n1, Y4, n1, Y5, not(and(n1, X0)), Y6, not(and(n1, X1)), Y7) -> f2(true__, n1, n1, not(and(n1, X0)), not(and(n1, X1)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, n1, X0, n1), n1, Y4, n1, Y5, not(and(n1, X0)), Y6, not(n1), Y7) -> f2(true__, n1, n1, not(and(n1, X0)), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, n1, X0, not(n1)), n1, Y4, n1, Y5, not(and(n1, X0)), Y6, n1, Y7) -> f2(true__, n1, n1, not(and(n1, X0)), n1, Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, n1, n1, n1, X0), n1, Y4, n1, Y5, not(n1), Y6, not(and(n1, X0)), Y7) -> f2(true__, n1, n1, not(n1), not(and(n1, X0)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(f2(true__, not(n1), not(n1), n1, n1, not(n1), X0, X1, X2), n1, Y4, not(and(not(n1), X0)), Y5, not(and(n1, X1)), Y6, not(and(n1, X2)), Y7) -> f2(true__, n1, not(and(not(n1), X0)), not(and(n1, X1)), not(and(n1, X2)), Y4, Y5, Y6, Y7) % 28.65/28.08 f1(output(X1, X2, X3, X4), X1, Y1, X2, Y2, X3, Y3, X4, Y4) -> f2(true__, X1, X2, X3, X4, Y1, Y2, Y3, Y4) % 28.65/28.08 f1(true__, X1, Y1, X2, Y2, X3, Y3, X4, Y4) -> output(nand(X1, Y1), nand(X2, Y2), nand(X3, Y3), nand(X4, Y4)) % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, X2, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), not(and(n1, X2)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, X2, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), not(and(n1, X2)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, n1, X2), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), not(n1), not(and(not(n1), X2))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, n1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, not(n1), X2), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), n1, not(and(not(n1), X2))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, not(n1), n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, X1, not(n1), not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, X1, X2), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), not(and(n1, X1)), not(and(not(n1), X2))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, X1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, X1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, n1, X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), not(n1), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, n1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, not(n1), X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, n1, not(n1), n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), X1, X2), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(n1, X1)), not(and(not(n1), X2))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), X1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), X1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), n1, X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(n1), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), n1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), not(n1), X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), not(n1), n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), X0, not(n1), not(n1), not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, X1, X2), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), not(and(n1, X1)), not(and(not(n1), X2))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, X1, n1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, X1, not(n1)), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, n1, X1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), not(n1), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, n1, n1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, not(n1), X1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, X0, not(n1), n1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, n1, X0, X1), Y4, Y5, Y6, Y7, not(n1), not(n1), not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, n1, X0, n1), Y4, Y5, Y6, Y7, not(n1), not(n1), not(and(n1, X0)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, n1, n1, X0), Y4, Y5, Y6, Y7, not(n1), not(n1), not(n1), not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, n1, not(n1), X0), Y4, Y5, Y6, Y7, not(n1), not(n1), n1, not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, not(n1), X0, X1), Y4, Y5, Y6, Y7, not(n1), n1, not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, not(n1), X0, n1), Y4, Y5, Y6, Y7, not(n1), n1, not(and(n1, X0)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, not(n1), n1, X0), Y4, Y5, Y6, Y7, not(n1), n1, not(n1), not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), X0), Y4, Y5, Y6, Y7, not(n1), n1, n1, not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), X0, X1, X2), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(and(n1, X1)), not(and(not(n1), X2))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), X0, X1, n1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), X0, X1, not(n1)), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(and(n1, X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), X0, n1, X1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(n1), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), X0, n1, n1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), X0, not(n1), X1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), Y0, not(n1), n1), Y2, Y3, Y4, Y5, n1, not(and(n1, Y0)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), n1, X0, X1), Y4, Y5, Y6, Y7, n1, not(n1), not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), n1, X0, n1), Y4, Y5, Y6, Y7, n1, not(n1), not(and(n1, X0)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), n1, n1, X0), Y4, Y5, Y6, Y7, n1, not(n1), not(n1), not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), n1, n1, n1), Y4, Y5, Y6, Y7, n1, not(n1), not(n1), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), n1, not(n1), X0), Y4, Y5, Y6, Y7, n1, not(n1), n1, not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), X0, X1), Y4, Y5, Y6, Y7, n1, n1, not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y0, n1), Y2, Y3, Y4, Y5, n1, n1, not(and(n1, Y0)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), n1, X0), Y4, Y5, Y6, Y7, n1, n1, not(n1), not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), X0), Y4, Y5, Y6, Y7, n1, n1, n1, not(and(not(n1), X0))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), n1), Y1, Y2, Y3, Y4, n1, n1, n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, X1, n1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, X1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, X1, not(n1), n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(and(n1, X1)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, n1, X1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), not(and(not(n1), X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, n1, n1, X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, n1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, n1, not(n1), X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, n1, not(n1), n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), not(n1), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), X1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(not(n1), X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), X1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(not(n1), X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), n1, X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), n1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), not(n1), X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), X0, not(n1), not(n1), n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), n1, X0, X1, n1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), not(and(not(n1), X1)), n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), n1, X0, n1, X1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), n1, X0, n1, not(n1)), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), n1, X0, not(n1), X1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), n1, X0, not(n1), n1), Y4, Y5, Y6, Y7, not(n1), not(and(n1, X0)), n1, n1) -> true__ % 28.65/28.08 f2(f2(true__, n1, n1, not(n1), not(n1), n1, n1, X0, n1), Y4, Y5, Y6, Y7, not(n1), not(n1), not(and(not(n1), X0)), n1) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), n1, n1, n1, X0), Y4, Y5, Y6, Y7, not(n1), not(n1), n1, not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), X0, n1), Y4, Y5, Y6, Y7, not(n1), n1, not(and(not(n1), X0)), n1) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, X0), Y4, Y5, Y6, Y7, not(n1), n1, n1, not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), not(n1), X0, n1, X1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), not(n1), X0, not(n1), X1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), n1, not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, n1, X0), Y4, Y5, Y6, Y7, n1, not(n1), n1, not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, X0), Y4, Y5, Y6, Y7, n1, n1, n1, not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), X0, n1, X1, n1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(n1, X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), X0, n1, X1, not(n1)), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(and(n1, X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), X0, n1, n1, X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, not(n1), not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), X0, n1, not(n1), X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), X0, not(n1), not(n1), X1), Y4, Y5, Y6, Y7, not(and(n1, X0)), n1, n1, not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), n1, n1, X0, X1), Y4, Y5, Y6, Y7, not(n1), n1, not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), n1, n1, not(n1), X0), Y4, Y5, Y6, Y7, not(n1), n1, n1, not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, X0, X1), Y4, Y5, Y6, Y7, n1, n1, not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, n1, X0), Y4, Y5, Y6, Y7, n1, n1, not(n1), not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, not(n1), X0), Y4, Y5, Y6, Y7, n1, n1, n1, not(and(not(n1), X0))) -> true__ % 28.65/28.09 f2(f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), X0, X1), Y4, Y5, Y6, Y7, n1, n1, not(and(n1, X0)), not(and(not(n1), X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, X1, X2, X3), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(n1, X1)), not(and(not(n1), X2)), not(and(n1, X3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, X1, n1, X2), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(n1, X1)), n1, not(and(n1, X2))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, X1, n1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(n1, X1)), n1, not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, X1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(n1, X1)), n1, n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, n1, X1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(n1), not(and(not(n1), X1)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, n1, X1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(n1), not(and(not(n1), X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, n1, n1, X1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(n1), n1, not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, n1, n1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(n1), n1, not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, n1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(n1), n1, n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), X1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(and(not(n1), X1)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), X1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(and(not(n1), X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), n1, X1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, n1, not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), n1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, n1, not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, X0, not(n1), n1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, n1, n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, Y2, n1), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, Y2, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, not(n1), Y3), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(n1, Y1)), n1, not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, Y0, n1, Y2, Y3), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(n1), not(and(not(n1), Y2)), not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), Y2, Y3), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), n1, not(and(not(n1), Y2)), not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, X0, X1, X2), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(and(not(n1), X1)), not(and(n1, X2))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, X0, X1, n1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(and(not(n1), X1)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, X0, X1, not(n1)), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), not(and(not(n1), X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, X0, n1, X1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), n1, not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, X0, n1, n1), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), n1, not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, X0, n1, not(n1)), Y4, Y5, Y6, Y7, n1, not(and(n1, X0)), n1, n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, n1, X0, X1), Y4, Y5, Y6, Y7, n1, not(n1), not(and(not(n1), X0)), not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, n1, X0, n1), Y4, Y5, Y6, Y7, n1, not(n1), not(and(not(n1), X0)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, n1, X0, not(n1)), Y4, Y5, Y6, Y7, n1, not(n1), not(and(not(n1), X0)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, n1, n1, X0), Y4, Y5, Y6, Y7, n1, not(n1), n1, not(and(n1, X0))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), X0, X1), Y4, Y5, Y6, Y7, n1, n1, not(and(not(n1), X0)), not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), X0, n1), Y4, Y5, Y6, Y7, n1, n1, not(and(not(n1), X0)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), X0, not(n1)), Y4, Y5, Y6, Y7, n1, n1, not(and(not(n1), X0)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), n1, X0), Y4, Y5, Y6, Y7, n1, n1, n1, not(and(n1, X0))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), n1, not(n1), n1, not(n1), Y1, Y2, Y3), Y4, Y5, Y6, Y7, n1, not(and(n1, Y1)), not(and(not(n1), Y2)), not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, X1, X2, X3), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(not(n1), X1)), not(and(n1, X2)), not(and(n1, X3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, X1, n1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(not(n1), X1)), not(n1), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, X1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(not(n1), X1)), not(n1), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, X1, not(n1), n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(not(n1), X1)), n1, not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, X1, not(n1), not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), not(and(not(n1), X1)), n1, n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, X1, X2), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(and(n1, X1)), not(and(n1, X2))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, X1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(and(n1, X1)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, X1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(and(n1, X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, n1, X1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(n1), not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, n1, n1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(n1), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, n1, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, not(n1), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, X0, n1, not(n1), X1), Y4, Y5, Y6, Y7, not(and(not(n1), X0)), n1, n1, not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, Y2, n1), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, Y2, not(n1)), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, n1, Y3), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(n1), not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, not(n1), Y3), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), not(and(not(n1), Y1)), n1, not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), Y2, Y3), Y4, Y5, Y6, Y7, not(and(not(n1), Y0)), n1, not(and(n1, Y2)), not(and(n1, Y3))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, X1, X2), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(and(n1, X1)), not(and(n1, X2))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, X1, n1), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(and(n1, X1)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, X1, not(n1)), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(and(n1, X1)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, n1, X1), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(n1), not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, n1, n1), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(n1), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, n1, not(n1)), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(n1), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, not(n1), X1), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), n1, not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, not(n1), n1), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), n1, not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, X0, not(n1), not(n1)), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), n1, n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, n1, X0, X1), Y4, Y5, Y6, Y7, n1, n1, not(and(n1, X0)), not(and(n1, X1))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, n1, X0, n1), Y4, Y5, Y6, Y7, n1, n1, not(and(n1, X0)), not(n1)) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, n1, X0, not(n1)), Y4, Y5, Y6, Y7, n1, n1, not(and(n1, X0)), n1) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, n1, n1, n1, X0), Y4, Y5, Y6, Y7, n1, n1, not(n1), not(and(n1, X0))) -> true__ % 28.65/28.09 f2(f2(true__, not(n1), not(n1), n1, n1, not(n1), X0, X1, X2), Y4, Y5, Y6, Y7, n1, not(and(not(n1), X0)), not(and(n1, X1)), not(and(n1, X2))) -> true__ % 28.65/28.09 f2(output(Y1, Y2, Y3, Y4), X1, X2, X3, X4, Y1, Y2, Y3, Y4) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, n1, n1, n1, n1) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, n1, n1, n1, not(n1)) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, n1, n1, not(n1), n1) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, n1, n1, not(n1), not(n1)) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, n1, not(n1), n1, n1) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, n1, not(n1), n1, not(n1)) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, not(n1), n1, n1, n1) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, not(n1), n1, not(n1), n1) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, not(n1), not(n1), n1, n1) -> true__ % 28.65/28.09 f2(true__, Y4, Y5, Y6, Y7, not(n1), not(n1), not(n1), n1) -> true__ % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), Y0, Y1, Y2, not(n1)) -> f2(true__, n1, n1, n1, n1, Y0, Y1, Y2, not(n1)) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), Y0, Y1, n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, n1, n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), Y0, n1, Y2, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, Y2, n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y2, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y2, n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), n1, Y1, Y2, not(n1)) -> f2(true__, n1, n1, n1, not(n1), n1, Y1, Y2, n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), n1) -> true__ % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), not(n1), Y1, Y2, not(n1)) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y1, Y2, n1) % 28.65/28.09 f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), n1) -> true__ % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, not(n1), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, n1, not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, not(n1), not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, n1, Y2, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, Y2, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, n1, n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, n1, not(n1), Y2) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, not(n1), Y2) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, n1, not(n1), Y2) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, n1, Y2) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, n1, not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, n1, not(n1), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, n1, not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), Y2, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), Y2, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, Y0, n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, Y0, not(n1), Y2) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, not(n1), Y2) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, Y0, not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, Y1, Y2, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, Y2, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, Y1, not(n1), Y2) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, n1, Y2) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, Y1, not(n1), n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, n1, not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, n1, n1, Y1) -> f2(true__, n1, n1, n1, not(n1), n1, n1, not(n1), Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, n1, not(n1), Y1) -> f2(true__, n1, n1, n1, not(n1), n1, n1, not(n1), Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), Y1, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), Y1, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, Y1) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), not(n1), Y1) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y0, n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, not(n1), n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y0, n1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y0, not(n1), Y2) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, not(n1), Y2) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y0, not(n1), not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y0, n1, not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, Y2, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, Y2, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, n1, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, n1, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, not(n1), Y2) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, n1, Y2) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, not(n1), n1) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, n1, not(n1)) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, Y1, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, Y1, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, n1, Y1) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, not(n1), Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, n1, not(n1)) -> true__ % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, not(n1), Y1) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, not(n1), Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, not(n1), not(n1)) -> true__ % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), Y1, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), Y1, n1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, Y1) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, not(n1)) -> true__ % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), not(n1), Y1) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), not(n1), not(n1)) -> true__ % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, n1, Y1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y1, n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, n1, Y2, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y2, n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, n1, n1, Y2) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), n1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), Y1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y1, n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), Y1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y1, n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), n1, Y2) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, n1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), Y2) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), Y2) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), Y2) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1), Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), Y2) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, not(n1), Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), not(n1)) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), n1, n1, Y1, Y2) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), Y1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), n1, n1, n1, Y1) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), n1, n1, not(n1), Y1) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), n1, n1, not(n1), Y1) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), n1, not(n1), Y1, Y2) -> f2(true__, n1, not(n1), n1, not(n1), n1, n1, Y1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), n1, not(n1), not(n1), Y1) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, n1, Y1) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, not(n1), Y1) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, not(n1), Y1) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), Y0, n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y0, n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), Y0, not(n1)) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y0, n1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), Y1, Y2) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), Y1, Y2) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, Y1, Y2) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), n1, Y1) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), not(n1), Y1) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, not(n1), Y3) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, n1, Y3) % 28.65/28.09 f2(true__, not(n1), n1, not(n1), n1, n1, Y1, Y2, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, Y2, n1) % 28.65/28.09 f2(true__, not(n1), n1, not(n1), n1, n1, Y1, Y2, not(n1)) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, Y2, not(n1)) % 28.65/28.09 f2(true__, not(n1), n1, not(n1), n1, n1, n1, n1, n1) -> true__ % 28.65/28.09 f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), n1, n1) -> true__ % 28.65/28.09 f2(true__, not(n1), n1, not(n1), n1, not(n1), Y1, Y2, Y3) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y1, Y2, Y3) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, Y0, n1, not(n1), Y1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), n1, Y1) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), Y2, Y3) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, Y2, Y3) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, Y1, Y2, not(n1)) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), Y1, Y2, not(n1)) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y1, n1) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y1, not(n1)) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y1, not(n1)) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y1, not(n1)) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, Y1, n1) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y1, not(n1)) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, Y1, not(n1)) % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, n1, n1, n1) -> true__ % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, n1, n1, not(n1), n1) -> true__ % 28.65/28.09 f2(true__, not(n1), not(n1), n1, n1, not(n1), Y1, Y2, Y3) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y1, Y2, Y3) % 28.65/28.09 f3(output(n0, n1, n1, n1)) -> true__ % 28.65/28.09 f3(output(not(n1), n1, n1, n1)) -> true__ % 28.65/28.09 f3(true__) -> false__ % 28.65/28.09 false__ -> true__ % 28.65/28.09 n0 -> not(n1) % 28.65/28.09 nand(X, Y) -> not(and(X, Y)) % 28.65/28.09 not(n0) -> n1 % 28.65/28.09 not(not(n1)) -> n1 % 28.65/28.09 output(n0, n0, n1, n1) -> true__ % 28.65/28.09 output(n0, n1, n0, n1) -> true__ % 28.65/28.09 output(n1, n1, n1, n1) -> true__ % 28.65/28.09 output(n1, n1, n1, not(and(n1, Y1))) -> f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), n1, Y1) % 28.65/28.09 output(n1, n1, n1, not(and(n1, Y1))) -> f2(true__, not(n1), not(n1), n1, n1, n1, n1, not(n1), Y1) % 28.65/28.09 output(n1, n1, n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), not(n1), Y1) % 28.65/28.09 output(n1, n1, n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 output(n1, n1, n1, not(and(not(n1), Y1))) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, not(n1), Y1) % 28.65/28.09 output(n1, n1, n1, not(n1)) -> true__ % 28.65/28.09 output(n1, n1, not(and(n1, Y0)), n1) -> f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y0, not(n1)) % 28.65/28.09 output(n1, n1, not(and(n1, Y0)), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y0, n1) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, n1, n1, Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, n1, not(n1), Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), n1, Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), not(n1), Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), not(n1), Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(not(n1), Y0)), n1) -> f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), Y0, not(n1)) % 28.65/28.09 output(n1, n1, not(and(not(n1), Y0)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), Y0, n1) % 28.65/28.09 output(n1, n1, not(and(not(n1), Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, n1, not(n1), Y1, Y2) % 28.65/28.09 output(n1, n1, not(and(not(n1), Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), not(n1), Y1, Y2) % 28.65/28.09 output(n1, n1, not(n1), n1) -> true__ % 28.65/28.09 output(n1, n1, not(n1), not(and(n1, Y1))) -> f2(true__, not(n1), not(n1), n1, n1, n1, n1, n1, Y1) % 28.65/28.09 output(n1, n1, not(n1), not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), not(n1), not(n1), n1, Y1) % 28.65/28.09 output(n1, n1, not(n1), not(and(not(n1), Y1))) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), n1, n1, Y1) % 28.65/28.09 output(n1, n1, not(n1), not(n1)) -> true__ % 28.65/28.09 output(n1, not(and(n1, Y0)), n1, n1) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y0, n1, not(n1)) % 28.65/28.09 output(n1, not(and(n1, Y0)), n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y0, n1, Y2) % 28.65/28.09 output(n1, not(and(n1, Y0)), n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y0, not(n1), Y2) % 28.65/28.09 output(n1, not(and(n1, Y0)), n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), Y0, not(n1), Y2) % 28.65/28.09 output(n1, not(and(n1, Y0)), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, not(n1), Y2) % 28.65/28.09 output(n1, not(and(n1, Y0)), n1, not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y0, n1, n1) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(and(not(n1), Y1)), n1) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y0, Y1, not(n1)) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(and(not(n1), Y1)), n1) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), Y0, Y1, not(n1)) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(and(not(n1), Y1)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y0, Y1, n1) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(and(not(n1), Y1)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), Y0, Y1, n1) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, n1, n1) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, n1, not(n1)) % 28.65/28.09 output(n1, not(and(n1, Y0)), not(n1), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y0, n1, Y2) % 28.65/28.09 output(n1, not(and(n1, Y1)), n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), Y1, n1, Y2) % 28.65/28.09 output(n1, not(and(n1, Y1)), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, n1, Y2) % 28.65/28.09 output(n1, not(and(n1, Y1)), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, not(n1), Y2) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y1, Y2, n1) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y1, Y2, not(n1)) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, n1, n1, n1, n1, not(n1), Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, n1, not(n1), not(n1), Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(not(n1), Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), n1, not(n1), n1, n1, Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(not(n1), Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(n1, Y1)), not(and(not(n1), Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), n1, n1) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, not(n1), not(n1)) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), n1, not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, not(n1), Y2) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), n1, not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), Y0, not(n1), Y2) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), n1, not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, not(n1), n1) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(and(n1, Y1)), n1) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, Y1, not(n1)) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(and(n1, Y1)), n1) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), Y0, Y1, not(n1)) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(and(n1, Y1)), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, Y1, n1) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(and(n1, Y1)), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), Y0, Y1, n1) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(n1), n1) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, n1, not(n1)) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(n1), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, n1, Y2) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(n1), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), Y0, n1, Y2) % 28.65/28.09 output(n1, not(and(not(n1), Y0)), not(n1), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y0, n1, n1) % 28.65/28.09 output(n1, not(and(not(n1), Y1)), not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), not(n1), n1, n1, n1, Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(not(n1), Y1)), not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), not(n1), n1, n1, not(n1), Y1, Y2, Y3) % 28.65/28.09 output(n1, not(and(not(n1), Y1)), not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, not(n1), n1, not(n1), not(n1), Y1, Y2, Y3) % 28.65/28.09 output(n1, not(n1), n1, n1) -> true__ % 28.65/28.09 output(n1, not(n1), n1, not(and(n1, Y1))) -> f2(true__, not(n1), n1, not(n1), n1, n1, n1, n1, Y1) % 28.65/28.09 output(n1, not(n1), n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, not(n1), Y1) % 28.65/28.09 output(n1, not(n1), n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, not(n1), not(n1), not(n1), n1, n1, Y1) % 28.65/28.09 output(n1, not(n1), n1, not(n1)) -> true__ % 28.65/28.09 output(n1, not(n1), not(and(n1, Y1)), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, Y1, n1) % 28.65/28.09 output(n1, not(n1), not(and(n1, Y1)), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, Y1, not(n1)) % 28.65/28.09 output(n1, not(n1), not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, Y1, Y2) % 28.65/28.09 output(n1, not(n1), not(and(not(n1), Y0)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, n1, n1, Y0, n1) % 28.65/28.09 output(n1, not(n1), not(and(not(n1), Y1)), n1) -> f2(true__, not(n1), n1, not(n1), n1, n1, n1, Y1, not(n1)) % 28.65/28.09 output(n1, not(n1), not(and(not(n1), Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, n1, n1, Y1, Y2) % 28.65/28.09 output(n1, not(n1), not(and(not(n1), Y1)), not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, not(n1), n1, Y1, Y2) % 28.65/28.09 output(n1, not(n1), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, n1, n1) % 28.65/28.09 output(n1, not(n1), not(n1), not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), not(n1), n1, n1, Y1) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, not(n1), not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), not(n1), Y2) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), n1, Y2) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), not(n1), Y2) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, not(and(not(n1), Y2))) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, not(n1), Y2) % 28.65/28.09 output(not(and(n1, Y0)), n1, n1, not(and(not(n1), Y2))) -> f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), not(n1), Y2) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y1)), n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, Y1, n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y1)), n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, Y1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y2, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, n1, n1, n1, n1, Y0, not(n1), Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, not(n1), n1, not(n1), Y0, not(n1), Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(not(n1), Y2)), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(not(n1), Y2)), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), Y2, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(and(not(n1), Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, not(n1), Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(n1), n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(n1), n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(n1), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), Y0, not(n1), n1, Y2) % 28.65/28.09 output(not(and(n1, Y0)), n1, not(n1), not(and(not(n1), Y2))) -> f2(true__, n1, not(n1), n1, not(n1), Y0, n1, n1, Y2) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, not(n1), not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, not(and(n1, Y3))) -> f2(true__, n1, n1, n1, n1, Y0, Y1, not(n1), Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, not(and(not(n1), Y3))) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, not(n1), Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, not(and(not(n1), Y3))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, n1, Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), n1, not(and(not(n1), Y3))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, not(n1), Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, Y2, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(and(n1, Y2)), not(n1)) -> f2(true__, n1, n1, n1, n1, Y0, Y1, Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, Y1, Y2, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(n1), not(and(n1, Y3))) -> f2(true__, n1, n1, n1, n1, Y0, Y1, n1, Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(n1, Y1)), not(n1), not(and(not(n1), Y3))) -> f2(true__, n1, n1, n1, not(n1), Y0, Y1, n1, Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(not(n1), Y1)), n1, n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, Y1, not(n1), not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(not(n1), Y1)), n1, not(and(not(n1), Y3))) -> f2(true__, n1, not(n1), n1, not(n1), Y0, Y1, not(n1), Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, Y1, Y2, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(and(not(n1), Y1)), not(n1), n1) -> f2(true__, n1, not(n1), n1, not(n1), Y0, Y1, n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, not(n1), not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, not(n1), n1) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, not(n1), Y2) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, n1, Y2) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, not(n1), Y2) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, Y2, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, n1, n1, n1, n1, Y0, n1, Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(and(not(n1), Y2)), n1) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, Y2, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(and(not(n1), Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, not(n1), not(n1), Y0, n1, Y2, Y3) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, n1, n1) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, n1, not(n1)) % 28.65/28.09 output(not(and(n1, Y0)), not(n1), not(n1), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), Y0, n1, n1, Y2) % 28.65/28.09 output(not(and(n1, Y4)), not(and(n1, Y5)), not(and(n1, Y6)), not(and(n1, Y7))) -> f2(true__, n1, n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(n1, Y4)), not(and(n1, Y5)), not(and(n1, Y6)), not(and(not(n1), Y7))) -> f2(true__, n1, n1, n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(n1, Y4)), not(and(n1, Y5)), not(and(not(n1), Y6)), not(and(n1, Y7))) -> f2(true__, n1, n1, not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(n1, Y4)), not(and(n1, Y5)), not(and(not(n1), Y6)), not(and(not(n1), Y7))) -> f2(true__, n1, n1, not(n1), not(n1), Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(n1, Y4)), not(and(not(n1), Y5)), not(and(n1, Y6)), not(and(n1, Y7))) -> f2(true__, n1, not(n1), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(n1, Y4)), not(and(not(n1), Y5)), not(and(n1, Y6)), not(and(not(n1), Y7))) -> f2(true__, n1, not(n1), n1, not(n1), Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), n1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, not(n1), not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), n1, Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), not(n1), Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, not(n1), Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), not(n1), Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), n1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, n1, not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, not(n1), n1) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(n1, Y1)), n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, Y1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(n1, Y1)), n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), Y1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(n1, Y1)), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, Y1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(n1, Y1)), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), Y1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, Y2, Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), Y2, Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(not(n1), Y1)), n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), Y1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(not(n1), Y1)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), Y1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(and(not(n1), Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, not(n1), Y2, Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(n1), n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, n1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(n1), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, n1, Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(n1), not(and(n1, Y2))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, not(n1), n1, Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), n1, not(n1), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, n1, n1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, n1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), n1, n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, not(n1), not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), n1, not(and(n1, Y3))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, n1, Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), n1, not(and(n1, Y3))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, not(n1), Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), n1, not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, n1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), n1, not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, not(n1), n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, Y2, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(n1, Y1)), not(and(not(n1), Y2)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, Y1, Y2, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), n1, n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, not(n1), not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), n1, not(and(n1, Y3))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, not(n1), Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), n1, not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, not(n1), n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, Y2, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(and(n1, Y2)), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, Y2, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(n1), n1) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, n1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(n1), not(and(n1, Y3))) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, n1, Y3) % 28.65/28.09 output(not(and(not(n1), Y0)), not(and(not(n1), Y1)), not(n1), not(n1)) -> f2(true__, not(n1), not(n1), n1, n1, Y0, Y1, n1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), n1, n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, n1, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, n1, Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), n1, not(and(n1, Y2))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, not(n1), Y2) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), n1, not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, n1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), not(and(not(n1), Y1)), not(n1)) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, Y1, n1) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), not(and(not(n1), Y2)), n1) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, Y2, not(n1)) % 28.65/28.09 output(not(and(not(n1), Y0)), not(n1), not(and(not(n1), Y2)), not(and(n1, Y3))) -> f2(true__, not(n1), n1, not(n1), n1, Y0, n1, Y2, Y3) % 28.65/28.09 output(not(and(not(n1), Y4)), not(and(n1, Y5)), not(and(n1, Y6)), not(and(n1, Y7))) -> f2(true__, not(n1), n1, n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(not(n1), Y4)), not(and(n1, Y5)), not(and(not(n1), Y6)), not(and(n1, Y7))) -> f2(true__, not(n1), n1, not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(not(n1), Y4)), not(and(not(n1), Y5)), not(and(n1, Y6)), not(and(n1, Y7))) -> f2(true__, not(n1), not(n1), n1, n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(and(not(n1), Y4)), not(and(not(n1), Y5)), not(and(not(n1), Y6)), not(and(n1, Y7))) -> f2(true__, not(n1), not(n1), not(n1), n1, Y4, Y5, Y6, Y7) % 28.65/28.09 output(not(n1), n1, n1, n1) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), n1) % 28.65/28.09 output(not(n1), n1, n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), not(n1), n1) % 28.65/28.09 output(not(n1), n1, n1, n1) -> true__ % 28.65/28.09 output(not(n1), n1, n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), not(n1), Y1) % 28.65/28.09 output(not(n1), n1, n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), n1, Y1) % 28.65/28.09 output(not(n1), n1, n1, not(and(not(n1), Y1))) -> f2(true__, n1, not(n1), n1, not(n1), n1, n1, not(n1), Y1) % 28.65/28.09 output(not(n1), n1, not(and(n1, Y1)), n1) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), Y1, n1) % 28.65/28.09 output(not(n1), n1, not(and(n1, Y1)), n1) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), Y1, not(n1)) % 28.65/28.09 output(not(n1), n1, not(and(n1, Y1)), n1) -> f2(true__, n1, not(n1), n1, not(n1), n1, n1, Y1, n1) % 28.65/28.09 output(not(n1), n1, not(and(n1, Y1)), n1) -> f2(true__, n1, not(n1), n1, not(n1), n1, n1, Y1, not(n1)) % 28.65/28.09 output(not(n1), n1, not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), Y1, Y2) % 28.65/28.09 output(not(n1), n1, not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, not(n1), n1, not(n1), n1, n1, Y1, Y2) % 28.65/28.09 output(not(n1), n1, not(and(not(n1), Y1)), n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, not(n1), Y1, n1) % 28.65/28.09 output(not(n1), n1, not(n1), n1) -> true__ % 28.65/28.09 output(not(n1), n1, not(n1), not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), n1, not(n1), n1, Y1) % 28.65/28.09 output(not(n1), not(and(n1, Y0)), n1, n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, not(n1), n1) % 28.70/28.10 output(not(n1), not(and(n1, Y0)), n1, n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, not(n1), not(n1)) % 28.70/28.10 output(not(n1), not(and(n1, Y0)), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, not(n1), Y2) % 28.70/28.10 output(not(n1), not(and(n1, Y0)), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, n1, n1) % 28.70/28.10 output(not(n1), not(and(n1, Y0)), not(n1), n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, n1, not(n1)) % 28.70/28.10 output(not(n1), not(and(n1, Y0)), not(n1), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), n1, Y0, n1, Y2) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, n1, n1) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, n1, not(n1)) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), n1, n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, not(n1), n1) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, n1, Y2) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), n1, not(and(not(n1), Y2))) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, not(n1), Y2) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y1, Y2, n1) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, n1, n1, not(n1), n1, Y1, Y2, not(n1)) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), not(and(n1, Y2)), not(and(n1, Y3))) -> f2(true__, n1, n1, n1, n1, n1, Y1, Y2, Y3) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, n1, not(n1), n1, Y1, Y2, Y3) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), not(and(not(n1), Y2)), n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, Y2, n1) % 28.70/28.10 output(not(n1), not(and(n1, Y1)), not(and(not(n1), Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, n1, not(n1), not(n1), n1, Y1, Y2, Y3) % 28.70/28.10 output(not(n1), not(and(not(n1), Y1)), not(and(n1, Y2)), n1) -> f2(true__, n1, not(n1), n1, not(n1), n1, Y1, Y2, not(n1)) % 28.70/28.10 output(not(n1), not(and(not(n1), Y1)), not(and(n1, Y2)), not(and(not(n1), Y3))) -> f2(true__, n1, not(n1), n1, not(n1), n1, Y1, Y2, Y3) % 28.70/28.10 output(not(n1), not(n1), n1, n1) -> true__ % 28.70/28.10 output(not(n1), not(n1), n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), n1, n1, not(n1), Y1) % 28.70/28.10 output(not(n1), not(n1), n1, not(and(not(n1), Y1))) -> f2(true__, n1, n1, not(n1), not(n1), n1, n1, n1, Y1) % 28.70/28.10 output(not(n1), not(n1), not(and(n1, Y1)), n1) -> f2(true__, n1, n1, n1, not(n1), n1, n1, Y1, n1) % 28.70/28.10 output(not(n1), not(n1), not(and(n1, Y1)), n1) -> f2(true__, n1, n1, n1, not(n1), n1, n1, Y1, not(n1)) % 28.70/28.10 output(not(n1), not(n1), not(and(n1, Y1)), not(and(not(n1), Y2))) -> f2(true__, n1, n1, n1, not(n1), n1, n1, Y1, Y2) % 28.70/28.10 output(not(n1), not(n1), not(and(not(n1), Y1)), n1) -> f2(true__, n1, n1, not(n1), not(n1), n1, n1, Y1, n1) % 28.70/28.10 output(not(n1), not(n1), not(n1), n1) -> true__ % 28.70/28.10 output(not(n1), not(n1), not(n1), not(and(not(n1), Y1))) -> f2(true__, n1, n1, n1, not(n1), n1, n1, n1, Y1) % 28.70/28.10 with the LPO induced by % 28.70/28.10 f1 > nand > and > n0 > not > f3 > output > f2 > n1 > false__ > true__ % 28.70/28.10 % 28.70/28.10 % SZS output end Proof % 28.70/28.10 %------------------------------------------------------------------------------