prover9_proof(mp2, 5.445, d(d(A, d(d(B, B), d(C, B))), A)-[D=d(2, 2), E=d(1, 2), F=d(1, 1), A=d(d(D, E), d(1, G)), C=d(d(D, F), E), G=d(d(D, d(1, F)), C), B=d(G, d(2, d(d(2, 1), F)))]).
prover9_proof(mp2b, 2.71, d(d(d(A, B), d(1, C)), d(D, d(C, d(2, d(d(2, 1), E)))))-[A=d(2, 2), B=d(1, 2), E=d(1, 1), D=d(d(A, E), B), C=d(d(A, d(1, E)), D)]).
prover9_proof(mpi, 0.439, d(d(2, A), d(d(2, B), d(d(d(C, d(1, B)), d(d(C, B), A)), d(2, d(d(2, 1), B)))))-[C=d(2, 2), A=d(1, 2), B=d(1, 1)]).
prover9_proof(id, 0.162, d(d(2, 1), d(1, 1))-[]).
prover9_proof(idd, 0.087, d(1, d(d(2, 1), d(1, 1)))-[]).
prover9_proof('2a1d', 0.102, d(2, d(1, d(d(2, d(1, 1)), 1)))-[]).
prover9_proof(a1i13, 0.072, d(A, A)-[A=d(2, d(1, 1))]).
prover9_proof('2a1', 0.077, d(d(2, d(1, 1)), 1)-[]).
prover9_proof(a2d, 0.077, d(2, d(1, 2))-[]).
prover9_proof(mpcom, 97.702, d(A, d(d(2, B), A))-[C=d(2, 2), B=d(1, 2), D=d(1, 1), A=d(d(C, B), d(1, d(d(C, d(1, D)), d(d(C, D), B))))]).
prover9_proof('pm2.27', 0.106, d(d(d(A, d(1, B)), d(d(A, B), d(1, 2))), d(2, d(d(2, 1), B)))-[A=d(2, 2), B=d(1, 1)]).
prover9_proof(a1dd, 0.104, d(2, d(1, d(2, d(1, 1))))-[]).
prover9_proof('2a1dd', 0.104, d(d(d(d(2, 2), A), d(1, 2)), d(2, d(1, d(d(2, A), 1))))-[A=d(1, 1)]).
prover9_proof('pm2.43d', 0.09, d(2, d(1, d(d(2, 2), d(2, 1))))-[]).
prover9_proof('pm2.43a', 1.927, d(2, d(d(2, A), d(d(2, B), d(d(d(C, d(1, B)), d(d(C, B), A)), d(2, d(d(2, 1), B))))))-[C=d(2, 2), A=d(1, 2), B=d(1, 1)]).
prover9_proof('pm2.43', 0.071, d(d(2, 2), d(2, 1))-[]).
prover9_proof(imim2d, 0.1, d(A, A)-[A=d(d(d(2, 2), d(1, 1)), d(1, 2))]).
prover9_proof(imim2, 0.074, d(d(d(2, 2), d(1, 1)), d(1, 2))-[]).
prover9_proof(imim1, 2.722, d(d(d(A, B), d(1, d(d(A, d(1, C)), D))), D)-[A=d(2, 2), B=d(1, 2), C=d(1, 1), D=d(d(A, C), B)]).
prover9_proof(peirceroll, 429.853, d(d(d(2, A), 3), d(d(B, d(1, d(C, d(2, d(C, d(C, d(2, D))))))), d(d(E, d(d(F, G), H)), d(I, d(J, d(d(J, d(d(E, E), K)), d(F, d(J, d(d(J, H), d(J, G))))))))))-[B=d(2, 2), F=d(2, L), M=d(2, d(d(2, 1), A)), N=d(1, 2), L=d(1, 3), A=d(1, 1), O=d(B, A), P=d(B, d(1, A)), J=d(d(B, N), d(1, C)), I=d(O, N), D=d(O, L), C=d(P, I), Q=d(P, d(d(M, d(1, D)), F)), G=d(I, d(3, Q)), K=d(I, E), E=d(C, M), H=d(d(E, Q), K)]).
prover9_proof('pm2.04', 1.158, d(d(A, B), d(1, d(d(A, d(1, C)), d(d(A, C), B))))-[A=d(2, 2), B=d(1, 2), C=d(1, 1)]).
prover9_proof(jarr, 0.104, d(d(A, d(1, B)), d(d(A, B), d(1, 2)))-[A=d(2, 2), B=d(1, 1)]).
prover9_proof('pm2.86', 209.456, d(d(d(2, A), B), d(d(C, D), B))-[C=d(2, 2), D=d(1, 2), E=d(1, 1), B=d(1, d(d(C, d(1, E)), A)), A=d(d(C, E), D)]).
prover9_proof(loolin, 6.874, d(d(2, d(1, d(A, d(2, 1)))), d(d(A, d(1, B)), d(d(A, B), d(1, 2))))-[A=d(2, 2), B=d(1, 1)]).
prover9_proof(loowoz, 0.383, d(d(2, A), d(d(B, d(1, C)), d(d(B, C), A)))-[B=d(2, 2), A=d(1, 2), C=d(1, 1)]).
prover9_proof(con4d, 0.076, d(2, d(1, 3))-[]).
prover9_proof(mt4, 0.088, d(d(d(2, 2), d(1, 1)), d(1, d(2, 3)))-[]).
prover9_proof(mt4i, 1.014, d(d(2, d(1, 2)), d(d(2, A), d(d(d(2, 2), A), d(1, d(2, 3)))))-[A=d(1, 1)]).
prover9_proof('pm2.21d', 0.078, d(2, d(1, d(d(d(2, 2), d(1, 1)), d(1, 3))))-[]).
prover9_proof('pm2.21ddALT', 0.551, d(d(2, A), d(B, d(d(d(C, d(1, D)), B), d(2, d(E, d(1, 3))))))-[C=d(2, 2), A=d(1, 2), D=d(1, 1), E=d(C, D), B=d(E, A)]).
prover9_proof('pm2.21', 0.381, d(d(d(2, 2), d(1, 1)), d(1, 3))-[]).
prover9_proof('pm2.24', 0.2, d(d(d(A, d(1, B)), d(C, d(1, 2))), d(2, d(C, d(1, 3))))-[A=d(2, 2), B=d(1, 1), C=d(A, B)]).
prover9_proof(jarl, 0.656, d(d(d(A, d(1, B)), d(C, d(1, 2))), d(A, d(1, d(C, d(1, 3)))))-[A=d(2, 2), B=d(1, 1), C=d(A, B)]).
prover9_proof('pm2.18d', 0.215, d(d(A, d(1, 2)), d(d(B, d(1, C)), d(d(2, D), d(2, d(A, D)))))-[B=d(2, 2), D=d(1, 3), C=d(1, 1), A=d(B, C)]).
prover9_proof('pm2.18', 0.214, d(d(A, d(1, B)), d(d(2, C), d(2, d(d(A, B), C))))-[A=d(2, 2), C=d(1, 3), B=d(1, 1)]).
prover9_proof(notnotr, 0.178, d(d(A, d(1, B)), d(d(d(2, d(d(2, 1), B)), d(1, d(d(A, B), C))), d(2, C)))-[A=d(2, 2), C=d(1, 3), B=d(1, 1)]).
prover9_proof(notnotrd, 0.178, d(d(A, d(1, 2)), d(d(B, d(1, C)), d(d(d(2, d(d(2, 1), C)), d(1, d(A, D))), d(2, D))))-[B=d(2, 2), D=d(1, 3), C=d(1, 1), A=d(B, C)]).
prover9_proof(con2d, 2.88, d(A, d(B, d(d(d(C, D), d(1, E)), d(d(F, d(G, d(d(H, d(1, d(I, J))), B))), d(A, F)))))-[C=d(2, 2), B=d(2, J), H=d(2, d(d(2, 1), K)), D=d(1, 2), J=d(1, 3), K=d(1, 1), I=d(C, K), G=d(C, d(1, K)), A=d(I, D), E=d(G, A), F=d(E, H)]).
prover9_proof(con2, 2.741, d(A, d(d(d(B, C), d(1, D)), d(d(E, d(F, d(d(G, d(1, d(H, I))), A))), d(J, E))))-[B=d(2, 2), A=d(2, I), G=d(2, d(d(2, 1), K)), C=d(1, 2), I=d(1, 3), K=d(1, 1), H=d(B, K), F=d(B, d(1, K)), J=d(H, C), D=d(F, J), E=d(D, G)]).
prover9_proof(mt2i, 5.232, d(d(2, A), d(d(2, B), d(C, d(D, d(C, d(d(E, d(F, d(d(G, d(1, d(H, I))), D))), d(J, E)))))))-[K=d(2, 2), D=d(2, I), G=d(2, d(d(2, 1), B)), A=d(1, 2), I=d(1, 3), B=d(1, 1), H=d(K, B), F=d(K, d(1, B)), C=d(d(K, A), d(1, L)), J=d(H, A), L=d(F, J), E=d(L, G)]).
prover9_proof(nsyl3, 4.63, d(d(2, A), d(d(2, B), d(C, d(d(d(D, A), d(1, E)), d(d(F, d(G, d(d(H, d(1, d(I, J))), C))), d(K, F))))))-[D=d(2, 2), C=d(2, J), H=d(2, d(d(2, 1), B)), A=d(1, 2), J=d(1, 3), B=d(1, 1), I=d(D, B), G=d(D, d(1, B)), K=d(I, A), E=d(G, K), F=d(E, H)]).
prover9_proof(nsyl, 181.819, d(A, d(d(2, B), d(d(2, C), d(D, d(A, d(d(A, d(d(E, F), d(G, E))), d(A, d(G, d(3, F)))))))))-[H=d(2, 2), D=d(2, I), J=d(2, d(d(2, 1), C)), B=d(1, 2), I=d(1, 3), C=d(1, 1), K=d(H, C), L=d(H, d(1, C)), A=d(d(H, B), d(1, M)), G=d(K, B), M=d(L, G), F=d(L, d(d(J, d(1, d(K, I))), D)), E=d(M, J)]).
prover9_proof(nsyl2, 201.804, d(d(d(A, B), d(1, d(C, D))), d(d(D, D), d(E, d(D, d(3, d(C, d(d(d(2, d(d(2, 1), F)), d(1, d(G, H))), E)))))))-[A=d(2, 2), E=d(2, H), B=d(1, 2), H=d(1, 3), F=d(1, 1), G=d(A, F), C=d(A, d(1, F)), D=d(G, B)]).
prover9_proof(notnot, 0.185, d(3, d(d(A, d(1, B)), d(d(d(2, d(d(2, 1), B)), d(1, d(d(A, B), C))), d(2, C))))-[A=d(2, 2), C=d(1, 3), B=d(1, 1)]).
prover9_proof(notnotd, 0.189, d(d(A, d(1, 2)), d(3, d(d(B, d(1, C)), d(d(d(2, d(d(2, 1), C)), d(1, d(A, D))), d(2, D)))))-[B=d(2, 2), D=d(1, 3), C=d(1, 1), A=d(B, C)]).
prover9_proof(con1d, 0.397, d(A, d(B, d(A, d(3, d(d(C, d(1, D)), d(d(d(2, d(d(2, 1), D)), d(1, d(E, F))), B))))))-[C=d(2, 2), B=d(2, F), F=d(1, 3), D=d(1, 1), E=d(C, D), A=d(E, d(1, 2))]).
prover9_proof(con1, 0.255, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(d(d(2, d(d(2, 1), D)), d(1, d(B, E))), A)))))-[C=d(2, 2), A=d(2, E), E=d(1, 3), D=d(1, 1), B=d(C, D)]).
prover9_proof(mt3i, 4.363, d(d(2, A), d(d(2, B), d(d(d(C, A), d(1, d(D, E))), d(F, d(E, d(3, d(D, d(d(d(2, d(d(2, 1), B)), d(1, d(G, H))), F))))))))-[C=d(2, 2), F=d(2, H), A=d(1, 2), H=d(1, 3), B=d(1, 1), G=d(C, B), D=d(C, d(1, B)), E=d(G, A)]).
prover9_proof('pm2.24d', 0.102, d(A, d(d(d(B, d(1, C)), A), d(2, d(D, d(1, 3)))))-[B=d(2, 2), C=d(1, 1), D=d(B, C), A=d(D, d(1, 2))]).
prover9_proof(con3d, 6.004, d(A, d(B, d(C, d(d(C, d(d(D, E), d(A, D))), d(C, d(A, d(3, E)))))))-[F=d(2, 2), B=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), K=d(F, I), L=d(F, d(1, I)), C=d(d(F, J), d(1, M)), A=d(K, J), M=d(L, A), E=d(L, d(d(H, d(1, d(K, G))), B)), D=d(M, H)]).
prover9_proof(con3, 5.999, d(A, d(B, d(d(B, d(d(C, D), d(E, C))), d(B, d(E, d(3, D))))))-[F=d(2, 2), A=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), K=d(F, I), L=d(F, d(1, I)), B=d(d(F, J), d(1, M)), E=d(K, J), M=d(L, E), D=d(L, d(d(H, d(1, d(K, G))), A)), C=d(M, H)]).
prover9_proof(con3rr3, 192.339, d(A, d(d(2, B), d(d(2, C), d(A, d(D, d(A, d(d(A, d(d(E, F), d(G, E))), d(A, d(G, d(3, F))))))))))-[H=d(2, 2), D=d(2, I), J=d(2, d(d(2, 1), C)), B=d(1, 2), I=d(1, 3), C=d(1, 1), K=d(H, C), L=d(H, d(1, C)), A=d(d(H, B), d(1, M)), G=d(K, B), M=d(L, G), F=d(L, d(d(J, d(1, d(K, I))), D)), E=d(M, J)]).
prover9_proof('pm3.2im', 2.719, d(A, d(d(d(B, C), d(D, d(d(C, d(1, d(E, F))), A))), d(d(G, H), d(1, B))))-[G=d(2, 2), A=d(2, F), C=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), E=d(G, I), D=d(G, d(1, I)), B=d(D, d(E, H))]).
prover9_proof(jcn, 5.997, d(d(A, d(d(B, B), C)), d(D, d(A, d(d(A, d(d(B, E), C)), d(A, d(F, d(3, E)))))))-[G=d(2, 2), D=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), A=d(d(G, K), d(1, N)), F=d(L, K), N=d(M, F), E=d(M, d(d(I, d(1, d(L, H))), D)), C=d(F, B), B=d(N, I)]).
prover9_proof(simprim, 0.2, d(3, d(d(A, d(B, d(1, 2))), d(3, d(A, d(d(d(2, d(d(2, 1), C)), d(1, d(B, D))), d(2, D))))))-[E=d(2, 2), D=d(1, 3), C=d(1, 1), B=d(E, C), A=d(E, d(1, C))]).
prover9_proof(simplim, 0.267, d(3, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(A, d(2, E)))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), B=d(C, D), A=d(d(2, d(d(2, 1), D)), d(1, d(B, E)))]).
prover9_proof('pm2.5g', 0.275, d(d(A, d(d(B, A), d(2, C))), d(3, d(D, d(A, d(3, d(B, d(D, d(2, E))))))))-[F=d(2, 2), E=d(1, 3), G=d(1, 1), H=d(F, G), B=d(F, d(1, G)), D=d(d(2, d(d(2, 1), G)), d(1, C)), A=d(H, d(1, 2)), C=d(H, E)]).
prover9_proof('pm2.5', 0.276, d(d(A, d(d(B, A), d(2, C))), d(3, d(D, d(A, d(3, d(B, d(D, d(2, E))))))))-[F=d(2, 2), E=d(1, 3), G=d(1, 1), H=d(F, G), B=d(F, d(1, G)), D=d(d(2, d(d(2, 1), G)), d(1, C)), A=d(H, d(1, 2)), C=d(H, E)]).
prover9_proof(conax1, 0.409, d(d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), E)))), E)-[C=d(2, 2), A=d(2, F), F=d(1, 3), D=d(1, 1), B=d(C, D), E=d(d(d(2, d(d(2, 1), D)), d(1, d(B, F))), A)]).
prover9_proof(conax1k, 0.429, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(A, d(F, d(2, d(F, d(F, d(2, E)))))))-[G=d(2, 2), A=d(2, H), H=d(1, 3), D=d(1, 1), I=d(G, D), C=d(G, d(1, D)), B=d(I, d(1, 2)), E=d(I, H), F=d(C, B)]).
prover9_proof('pm2.51', 0.412, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(A, d(F, d(2, d(F, d(F, d(2, E)))))))-[G=d(2, 2), A=d(2, H), H=d(1, 3), D=d(1, 1), I=d(G, D), C=d(G, d(1, D)), B=d(I, d(1, 2)), E=d(I, H), F=d(C, B)]).
prover9_proof('pm2.52', 0.286, d(d(A, d(d(B, A), d(2, C))), d(3, d(D, d(A, d(3, d(B, d(D, d(2, E))))))))-[F=d(2, 2), E=d(1, 3), G=d(1, 1), H=d(F, G), B=d(F, d(1, G)), D=d(d(2, d(d(2, 1), G)), d(1, C)), A=d(H, d(1, 2)), C=d(H, E)]).
prover9_proof('pm2.521g', 0.155, d(A, d(2, d(A, d(A, d(2, d(B, d(1, 3)))))))-[C=d(2, 2), D=d(1, 1), B=d(C, D), A=d(d(C, d(1, D)), d(B, d(1, 2)))]).
prover9_proof('pm2.521g2', 0.289, d(d(2, A), d(3, d(B, d(d(C, d(1, 2)), d(3, d(d(D, d(1, A)), d(B, d(2, E))))))))-[D=d(2, 2), E=d(1, 3), A=d(1, 1), C=d(D, A), B=d(d(2, d(d(2, 1), A)), d(1, d(C, E)))]).
prover9_proof('pm2.521', 0.163, d(A, d(2, d(A, d(A, d(2, d(B, d(1, 3)))))))-[C=d(2, 2), D=d(1, 1), B=d(C, D), A=d(d(C, d(1, D)), d(B, d(1, 2)))]).
prover9_proof(expt, 400.69, d(A, d(d(d(2, B), d(1, d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), A)))), d(A, B)))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(I, J), F=d(I, d(1, J)), A=d(d(I, K), d(1, D)), B=d(G, K), D=d(F, B)]).
prover9_proof(impt, 385.913, d(d(A, d(B, C)), d(D, d(d(2, E), d(d(2, F), d(D, d(B, d(D, d(d(D, d(d(G, H), d(A, G))), d(D, C)))))))))-[I=d(2, 2), B=d(2, J), K=d(2, d(d(2, 1), F)), E=d(1, 2), J=d(1, 3), F=d(1, 1), L=d(I, F), M=d(I, d(1, F)), D=d(d(I, E), d(1, N)), A=d(L, E), N=d(M, A), H=d(M, d(d(K, d(1, d(L, J))), B)), C=d(A, d(3, H)), G=d(N, K)]).
prover9_proof('pm2.61d1', 2687.015, d(A, d(d(d(d(B, d(C, d(D, d(2, E)))), F), d(d(d(2, G), A), d(d(d(2, B), d(1, H)), d(D, d(2, d(A, d(d(A, d(d(I, I), F)), H))))))), d(B, B)))-[J=d(2, 2), D=d(2, K), L=d(2, d(d(2, 1), G)), M=d(1, 2), K=d(1, 3), G=d(1, 1), N=d(J, G), C=d(J, d(1, G)), H=d(D, d(A, d(d(A, d(d(I, O), F)), d(A, d(B, d(3, O)))))), A=d(d(J, M), d(1, P)), B=d(N, M), E=d(N, K), P=d(C, B), O=d(C, d(d(L, d(1, E)), D)), F=d(B, I), I=d(P, L)]).
prover9_proof('pm2.61d2', 2605.567, d(A, d(d(d(A, B), d(d(C, d(2, D)), B)), d(E, E)))-[F=d(2, 2), G=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(F, J), M=d(F, d(1, J)), N=d(G, d(A, d(d(A, d(d(O, P), Q)), d(A, d(E, d(3, P)))))), A=d(d(F, K), d(1, C)), E=d(L, K), D=d(L, H), C=d(M, E), P=d(M, d(d(I, d(1, D)), G)), B=d(d(d(2, E), d(1, N)), d(G, d(2, d(A, d(d(A, d(d(O, O), Q)), N))))), Q=d(E, O), O=d(C, I)]).
prover9_proof('pm2.01', 1.078, d(d(d(A, d(B, d(C, d(2, D)))), d(2, E)), d(d(C, d(A, d(3, F))), d(d(G, F), d(A, G))))-[H=d(2, 2), C=d(2, I), J=d(2, d(d(2, 1), E)), I=d(1, 3), E=d(1, 1), K=d(H, E), B=d(H, d(1, E)), A=d(K, d(1, 2)), D=d(K, I), F=d(B, d(d(J, d(1, D)), C)), G=d(d(B, A), J)]).
prover9_proof('pm2.01d', 1.091, d(A, d(d(d(A, d(B, d(C, d(2, D)))), d(2, E)), d(d(C, d(A, d(3, F))), d(d(G, F), d(A, G)))))-[H=d(2, 2), C=d(2, I), J=d(2, d(d(2, 1), E)), I=d(1, 3), E=d(1, 1), K=d(H, E), B=d(H, d(1, E)), A=d(K, d(1, 2)), D=d(K, I), F=d(B, d(d(J, d(1, D)), C)), G=d(d(B, A), J)]).
prover9_proof('pm2.6', 202.074, d(A, d(d(d(2, B), d(1, C)), d(D, d(2, d(A, d(d(A, d(d(E, E), F)), C))))))-[G=d(2, 2), D=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), C=d(D, d(A, d(d(A, d(d(E, N), F)), d(A, d(B, d(3, N)))))), A=d(d(G, K), d(1, O)), B=d(L, K), O=d(M, B), N=d(M, d(d(I, d(1, d(L, H))), D)), F=d(B, E), E=d(O, I)]).
prover9_proof('pm2.61', 202.279, d(d(d(2, A), d(1, B)), d(C, d(2, d(D, d(d(D, d(d(E, E), F)), B)))))-[G=d(2, 2), C=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), B=d(C, d(D, d(d(D, d(d(E, N), F)), d(D, d(A, d(3, N)))))), D=d(d(G, K), d(1, O)), A=d(L, K), O=d(M, A), N=d(M, d(d(I, d(1, d(L, H))), C)), F=d(A, E), E=d(O, I)]).
prover9_proof('pm2.65', 107.909, d(d(A, d(B, d(C, d(D, d(A, E))))), d(2, d(B, d(D, C))))-[F=d(2, 2), B=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), K=d(F, I), L=d(F, d(1, I)), C=d(d(F, J), d(1, M)), A=d(K, J), M=d(L, A), E=d(M, H), D=d(E, d(L, d(d(H, d(1, d(K, G))), B)))]).
prover9_proof(mto, 5.993, d(A, d(B, d(A, d(d(A, d(d(C, D), d(E, C))), d(A, d(E, d(3, D)))))))-[F=d(2, 2), B=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), K=d(F, I), L=d(F, d(1, I)), A=d(d(F, J), d(1, M)), E=d(K, J), M=d(L, E), D=d(L, d(d(H, d(1, d(K, G))), B)), C=d(M, H)]).
prover9_proof(mtoi, 6.809, d(d(2, A), d(d(2, B), d(C, d(D, d(C, d(d(C, d(d(E, F), d(G, E))), d(C, d(G, d(3, F)))))))))-[H=d(2, 2), D=d(2, I), J=d(2, d(d(2, 1), B)), A=d(1, 2), I=d(1, 3), B=d(1, 1), K=d(H, B), L=d(H, d(1, B)), C=d(d(H, A), d(1, M)), G=d(K, A), M=d(L, G), F=d(L, d(d(J, d(1, d(K, I))), D)), E=d(M, J)]).
prover9_proof(mt2, 2.856, d(A, d(B, d(A, d(d(C, d(D, d(d(E, d(1, d(F, G))), B))), d(H, C)))))-[I=d(2, 2), B=d(2, G), E=d(2, d(d(2, 1), J)), K=d(1, 2), G=d(1, 3), J=d(1, 1), F=d(I, J), D=d(I, d(1, J)), A=d(d(I, K), d(1, L)), H=d(F, K), L=d(D, H), C=d(L, E)]).
prover9_proof(peirce, 0.957, d(d(A, B), d(d(B, d(A, d(d(2, C), d(2, D)))), d(E, d(1, D))))-[E=d(2, 2), C=d(1, 3), F=d(1, 1), G=d(E, F), A=d(E, d(1, F)), B=d(G, d(1, 2)), D=d(G, C)]).
prover9_proof(looinv, 428.092, d(3, d(d(A, d(1, d(B, d(2, d(B, d(B, d(2, C))))))), d(d(D, d(d(E, F), G)), d(H, d(I, d(d(I, d(d(D, D), J)), d(E, d(I, d(d(I, G), d(I, F))))))))))-[A=d(2, 2), E=d(2, K), L=d(2, d(d(2, 1), M)), N=d(1, 2), K=d(1, 3), M=d(1, 1), O=d(A, M), P=d(A, d(1, M)), I=d(d(A, N), d(1, B)), H=d(O, N), C=d(O, K), B=d(P, H), Q=d(P, d(d(L, d(1, C)), E)), F=d(H, d(3, Q)), J=d(H, D), D=d(B, L), G=d(d(D, Q), J)]).
prover9_proof(bijust0, 0.246, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof(bijust, 0.254, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof(impbi, 2.734, d(A, d(d(d(B, C), d(D, d(d(C, d(1, d(E, F))), A))), d(d(G, H), d(1, B))))-[G=d(2, 2), A=d(2, F), C=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), E=d(G, I), D=d(G, d(1, I)), B=d(D, d(E, H))]).
prover9_proof(biimp, 0.279, d(3, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(A, d(2, E)))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), B=d(C, D), A=d(d(2, d(d(2, 1), D)), d(1, d(B, E)))]).
prover9_proof(sylbi, 4.075, d(d(A, d(d(B, d(3, d(C, d(D, d(3, d(E, d(C, d(2, F)))))))), d(D, B))), d(A, D))-[G=d(2, 2), H=d(2, d(d(2, 1), I)), J=d(1, 2), F=d(1, 3), I=d(1, 1), K=d(G, I), E=d(G, d(1, I)), C=d(H, d(1, d(K, F))), A=d(d(G, J), d(1, L)), D=d(K, J), L=d(E, D), B=d(L, H)]).
prover9_proof(sylib, 457.198, d(d(d(A, B), d(1, d(C, D))), d(d(2, B), d(d(2, E), d(3, d(F, d(D, d(3, d(C, d(F, d(2, G))))))))))-[A=d(2, 2), B=d(1, 2), G=d(1, 3), E=d(1, 1), H=d(A, E), C=d(A, d(1, E)), F=d(d(2, d(d(2, 1), E)), d(1, d(H, G))), D=d(H, B)]).
prover9_proof(biimpr, 0.199, d(3, d(d(A, d(B, d(1, 2))), d(3, d(A, d(d(d(2, d(d(2, 1), C)), d(1, d(B, D))), d(2, D))))))-[E=d(2, 2), D=d(1, 3), C=d(1, 1), B=d(E, C), A=d(E, d(1, C))]).
prover9_proof(bicom1, 4.643, d(d(A, d(B, d(3, C))), d(D, d(A, D)))-[E=d(2, 2), A=d(2, F), G=d(2, d(d(2, 1), H)), I=d(1, 2), F=d(1, 3), H=d(1, 1), J=d(E, H), K=d(E, d(1, H)), B=d(J, I), L=d(K, B), C=d(K, d(d(G, d(1, d(J, F))), A)), D=d(d(d(E, I), d(1, L)), d(d(M, C), d(B, M))), M=d(L, G)]).
prover9_proof(impbid1, 132.676, d(A, d(d(2, B), d(d(2, C), d(A, d(D, d(d(d(E, F), d(G, d(d(F, d(1, d(H, I))), D))), A))))))-[J=d(2, 2), D=d(2, I), F=d(2, d(d(2, 1), C)), B=d(1, 2), I=d(1, 3), C=d(1, 1), H=d(J, C), G=d(J, d(1, C)), A=d(d(J, B), d(1, E)), E=d(G, d(H, B))]).
prover9_proof(impbid2, 4.598, d(d(2, A), d(d(2, B), d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), d(d(I, A), d(1, D))))))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), B)), A=d(1, 2), H=d(1, 3), B=d(1, 1), G=d(I, B), F=d(I, d(1, B)), D=d(F, d(G, A))]).
prover9_proof(biimpd, 0.358, d(A, d(3, d(B, d(A, d(3, d(d(C, d(1, D)), d(B, d(2, E))))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), F=d(C, D), B=d(d(2, d(d(2, 1), D)), d(1, d(F, E))), A=d(F, d(1, 2))]).
prover9_proof(mpbi, 2.737, d(d(d(A, B), d(3, d(C, d(D, d(3, d(E, d(C, d(2, F)))))))), d(d(G, H), d(1, A)))-[G=d(2, 2), B=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), J=d(G, I), E=d(G, d(1, I)), C=d(B, d(1, d(J, F))), D=d(J, H), A=d(E, D)]).
prover9_proof(mpbir, 2.841, d(d(d(A, B), d(3, d(A, d(3, d(C, d(d(B, d(1, d(D, E))), d(2, E))))))), d(d(F, G), d(1, A)))-[F=d(2, 2), B=d(2, d(d(2, 1), H)), G=d(1, 2), E=d(1, 3), H=d(1, 1), D=d(F, H), C=d(F, d(1, H)), A=d(C, d(D, G))]).
prover9_proof(mpbii, 1109.688, d(d(d(A, B), d(d(d(C, d(d(D, D), d(E, d(B, d(2, d(F, G)))))), d(d(d(B, d(2, d(2, H))), d(I, d(J, d(2, K)))), d(C, L))), d(d(M, d(N, d(3, d(O, M)))), C))), d(L, L))-[F=d(2, 2), G=d(2, 1), J=d(2, P), Q=d(2, d(G, H)), E=d(3, R), S=d(1, 2), P=d(1, 3), H=d(1, 1), T=d(F, H), I=d(F, d(1, H)), O=d(Q, d(1, K)), C=d(d(F, S), d(1, B)), L=d(T, S), K=d(T, P), B=d(I, L), R=d(I, d(O, J)), D=d(C, d(d(N, R), A)), M=d(L, E), A=d(L, N), N=d(B, Q)]).
prover9_proof(biimprd, 0.217, d(A, d(3, d(d(B, A), d(3, d(B, d(d(d(2, d(d(2, 1), C)), d(1, d(D, E))), d(2, E)))))))-[F=d(2, 2), E=d(1, 3), C=d(1, 1), D=d(F, C), B=d(F, d(1, C)), A=d(D, d(1, 2))]).
prover9_proof(biimpcd, 1483.276, d(d(d(d(A, B), d(C, d(3, d(D, d(C, d(3, d(E, d(D, d(2, F))))))))), d(G, C)), G)-[H=d(2, 2), B=d(2, d(d(2, 1), I)), J=d(1, 2), F=d(1, 3), I=d(1, 1), K=d(H, I), E=d(H, d(1, I)), D=d(B, d(1, d(K, F))), G=d(d(H, J), d(1, A)), C=d(K, J), A=d(E, C)]).
prover9_proof(biidd, 0.252, d(d(d(2, A), d(d(2, 3), B)), d(d(C, d(1, B)), d(d(C, d(1, A)), d(d(d(2, D), d(1, d(d(C, A), E))), d(2, E)))))-[C=d(2, 2), E=d(1, 3), A=d(1, 1), B=d(1, D), D=d(d(2, 1), A)]).
prover9_proof('pm5.1im', 6.212, d(A, d(B, d(A, d(C, d(d(d(A, D), d(E, d(d(D, d(1, d(F, G))), C))), B)))))-[H=d(2, 2), C=d(2, G), D=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), F=d(H, I), E=d(H, d(1, I)), B=d(d(H, J), d(1, A)), A=d(E, d(F, J))]).
prover9_proof(monothetic, 1.551, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, d(1, D)), D=d(d(2, 1), C)]).
prover9_proof(ibi, 3.004, d(2, d(d(d(A, B), d(3, d(C, d(D, d(3, d(E, d(C, d(2, F)))))))), d(d(G, H), d(1, A))))-[G=d(2, 2), B=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), J=d(G, I), E=d(G, d(1, I)), C=d(B, d(1, d(J, F))), D=d(J, H), A=d(E, D)]).
prover9_proof(ibir, 3.887, d(2, d(d(d(A, B), d(3, d(A, d(3, d(C, d(d(B, d(1, d(D, E))), d(2, E))))))), d(d(F, G), d(1, A))))-[F=d(2, 2), B=d(2, d(d(2, 1), H)), G=d(1, 2), E=d(1, 3), H=d(1, 1), D=d(F, H), C=d(F, d(1, H)), A=d(C, d(D, G))]).
prover9_proof(notnotb, 4.074, d(d(d(A, d(1, d(2, 3))), B), d(d(C, d(3, B)), d(d(C, B), d(d(D, E), d(1, F)))))-[D=d(2, 2), G=d(2, d(d(2, 1), H)), E=d(1, 2), I=d(1, 3), H=d(1, 1), A=d(D, H), J=d(D, d(1, H)), F=d(J, d(A, E)), B=d(J, d(d(G, d(1, d(A, I))), d(2, I))), C=d(F, G)]).
prover9_proof(mtbi, 149.912, d(d(d(A, B), d(A, d(C, d(A, d(d(A, d(d(D, E), F)), d(A, d(B, G))))))), d(A, d(F, d(3, d(H, G)))))-[I=d(2, 2), C=d(2, J), K=d(2, d(d(2, 1), L)), G=d(3, E), M=d(1, 2), J=d(1, 3), L=d(1, 1), N=d(I, L), O=d(I, d(1, L)), A=d(d(I, M), d(1, H)), B=d(N, M), H=d(O, B), E=d(O, d(d(K, d(1, d(N, J))), C)), F=d(B, D), D=d(H, K)]).
prover9_proof(mtbir, 31.718, d(A, d(d(B, C), d(d(2, D), d(E, E))))-[F=d(2, 2), B=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), D=d(1, d(K, G)), K=d(F, I), L=d(F, d(1, I)), E=d(B, d(A, d(d(A, d(d(M, N), d(O, M))), d(A, C)))), A=d(d(F, J), d(1, P)), O=d(K, J), P=d(L, O), N=d(L, d(d(H, D), B)), C=d(O, d(3, N)), M=d(P, H)]).
prover9_proof('pm5.19', 3.345, d(d(3, A), d(d(B, d(C, d(D, E))), d(d(C, d(d(F, d(G, d(B, d(2, H)))), E)), d(d(2, d(I, d(1, d(2, 3)))), d(D, C)))))-[J=d(2, 2), B=d(2, K), L=d(2, d(d(2, 1), M)), N=d(1, 2), K=d(1, 3), M=d(1, 1), I=d(J, M), G=d(J, d(1, M)), C=d(d(J, N), d(1, O)), P=d(I, N), H=d(I, K), O=d(G, P), A=d(G, d(d(L, d(1, H)), B)), E=d(P, F), F=d(O, L), D=d(F, A)]).
prover9_proof('pm4.81', 4.627, d(d(A, d(B, d(C, d(2, D)))), d(B, d(C, d(d(A, d(B, d(d(E, d(1, D)), C))), d(d(F, G), d(1, H))))))-[F=d(2, 2), C=d(2, I), E=d(2, d(d(2, 1), J)), G=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(F, J), B=d(F, d(1, J)), D=d(K, I), H=d(B, d(K, G)), A=d(H, E)]).
prover9_proof('pm4.63', 0.317, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof('pm4.67', 0.31, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof(imnan, 4.159, d(d(d(A, d(1, d(2, 3))), B), d(d(C, d(3, B)), d(d(C, B), d(d(D, E), d(1, F)))))-[D=d(2, 2), G=d(2, d(d(2, 1), H)), E=d(1, 2), I=d(1, 3), H=d(1, 1), A=d(D, H), J=d(D, d(1, H)), F=d(J, d(A, E)), B=d(J, d(d(G, d(1, d(A, I))), d(2, I))), C=d(F, G)]).
prover9_proof(imnani, 0.23, d(d(A, d(1, B)), d(d(d(2, d(d(2, 1), B)), d(1, d(d(A, B), C))), d(2, C)))-[A=d(2, 2), C=d(1, 3), B=d(1, 1)]).
prover9_proof('pm3.24', 0.234, d(A, A)-[B=d(2, 2), A=d(3, d(d(B, d(1, C)), d(d(d(2, d(d(2, 1), C)), d(1, d(d(B, C), D))), d(2, D)))), D=d(1, 3), C=d(1, 1)]).
prover9_proof(impcom, 420.362, d(d(d(d(2, A), d(1, B)), C), d(d(C, d(d(2, D), d(d(2, E), d(C, B)))), d(d(A, d(C, d(d(F, G), d(A, F)))), d(C, d(d(H, d(1, F)), d(1, C))))))-[H=d(2, 2), I=d(2, J), K=d(2, d(d(2, 1), E)), D=d(1, 2), J=d(1, 3), E=d(1, 1), L=d(H, E), M=d(H, d(1, E)), B=d(I, d(A, d(3, G))), C=d(d(H, D), d(1, N)), A=d(L, D), N=d(M, A), G=d(M, d(d(K, d(1, d(L, J))), I)), F=d(N, K)]).
prover9_proof(expcom, 395.747, d(A, d(d(d(2, B), d(1, d(A, d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), A))))), d(A, B)))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(I, J), F=d(I, d(1, J)), A=d(d(I, K), d(1, D)), B=d(G, K), D=d(F, B)]).
prover9_proof('pm3.22', 4.8, d(d(A, d(B, d(3, C))), d(D, d(A, D)))-[E=d(2, 2), A=d(2, F), G=d(2, d(d(2, 1), H)), I=d(1, 2), F=d(1, 3), H=d(1, 1), J=d(E, H), K=d(E, d(1, H)), B=d(J, I), L=d(K, B), C=d(K, d(d(G, d(1, d(J, F))), A)), D=d(d(d(E, I), d(1, L)), d(d(M, C), d(B, M))), M=d(L, G)]).
prover9_proof('pm3.21', 2.761, d(A, d(B, d(d(d(C, D), d(E, d(d(D, d(1, d(F, G))), B))), A)))-[H=d(2, 2), B=d(2, G), D=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), F=d(H, I), E=d(H, d(1, I)), A=d(d(H, J), d(1, C)), C=d(E, d(F, J))]).
prover9_proof(simpl, 0.324, d(3, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(A, d(2, E)))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), B=d(C, D), A=d(d(2, d(d(2, 1), D)), d(1, d(B, E)))]).
prover9_proof(intnan, 0.196, d(d(A, d(B, d(1, 2))), d(3, d(A, d(d(d(2, d(d(2, 1), C)), d(1, d(B, D))), d(2, D)))))-[E=d(2, 2), D=d(1, 3), C=d(1, 1), B=d(E, C), A=d(E, d(1, C))]).
prover9_proof(intnanr, 0.264, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(A, d(2, E))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), B=d(C, D), A=d(d(2, d(d(2, 1), D)), d(1, d(B, E)))]).
prover9_proof(intnand, 0.207, d(A, d(d(B, A), d(3, d(B, d(d(d(2, d(d(2, 1), C)), d(1, d(D, E))), d(2, E))))))-[F=d(2, 2), E=d(1, 3), C=d(1, 1), D=d(F, C), B=d(F, d(1, C)), A=d(D, d(1, 2))]).
prover9_proof(intnanrd, 0.272, d(A, d(B, d(A, d(3, d(d(C, d(1, D)), d(B, d(2, E)))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), F=d(C, D), B=d(d(2, d(d(2, 1), D)), d(1, d(F, E))), A=d(F, d(1, 2))]).
prover9_proof(adantrd, 3.455, d(A, d(d(d(B, C), d(1, D)), d(d(E, d(3, d(F, d(A, d(3, d(G, d(F, d(2, H)))))))), d(A, E))))-[B=d(2, 2), I=d(2, d(d(2, 1), J)), C=d(1, 2), H=d(1, 3), J=d(1, 1), K=d(B, J), G=d(B, d(1, J)), F=d(I, d(1, d(K, H))), A=d(K, C), D=d(G, A), E=d(D, I)]).
prover9_proof('pm3.41', 3.29, d(d(d(A, B), d(1, C)), d(d(D, d(3, d(E, d(F, d(3, d(G, d(E, d(2, H)))))))), d(F, D)))-[A=d(2, 2), I=d(2, d(d(2, 1), J)), B=d(1, 2), H=d(1, 3), J=d(1, 1), K=d(A, J), G=d(A, d(1, J)), E=d(I, d(1, d(K, H))), F=d(K, B), C=d(G, F), D=d(C, I)]).
prover9_proof('pm3.42', 3.496, d(d(d(A, B), d(1, C)), d(d(D, d(C, E)), d(3, d(C, d(3, d(F, d(d(E, d(1, d(G, H))), d(2, H))))))))-[A=d(2, 2), E=d(2, d(d(2, 1), I)), B=d(1, 2), H=d(1, 3), I=d(1, 1), G=d(A, I), F=d(A, d(1, I)), D=d(G, B), C=d(F, D)]).
prover9_proof(simpld, 0.301, d(A, d(3, d(B, d(A, d(3, d(d(C, d(1, D)), d(B, d(2, E))))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), F=d(C, D), B=d(d(2, d(d(2, 1), D)), d(1, d(F, E))), A=d(F, d(1, 2))]).
prover9_proof(simprd, 0.301, d(A, d(3, d(d(B, A), d(3, d(B, d(d(d(2, d(d(2, 1), C)), d(1, d(D, E))), d(2, E)))))))-[F=d(2, 2), E=d(1, 3), C=d(1, 1), D=d(F, C), B=d(F, d(1, C)), A=d(D, d(1, 2))]).
prover9_proof(simprbi, 3.102, d(d(d(d(A, B), d(1, C)), d(d(D, d(3, d(E, d(F, G)))), d(F, D))), d(F, d(3, d(C, G))))-[A=d(2, 2), H=d(2, d(d(2, 1), I)), G=d(3, d(J, d(E, d(2, K)))), B=d(1, 2), K=d(1, 3), I=d(1, 1), L=d(A, I), J=d(A, d(1, I)), E=d(H, d(1, d(L, K))), F=d(L, B), C=d(J, F), D=d(C, H)]).
prover9_proof(simplbi, 3.011, d(d(d(d(A, B), d(1, C)), d(d(D, E), d(F, D))), d(F, E))-[A=d(2, 2), G=d(2, d(d(2, 1), H)), E=d(3, d(I, d(F, d(3, d(J, d(I, d(2, K))))))), B=d(1, 2), K=d(1, 3), H=d(1, 1), L=d(A, H), J=d(A, d(1, H)), I=d(G, d(1, d(L, K))), F=d(L, B), C=d(J, F), D=d(C, G)]).
prover9_proof(jctil, 132.81, d(A, d(d(2, B), d(d(2, C), d(D, d(d(d(E, F), d(G, d(d(F, d(1, d(H, I))), D))), A)))))-[J=d(2, 2), D=d(2, I), F=d(2, d(d(2, 1), C)), B=d(1, 2), I=d(1, 3), C=d(1, 1), H=d(J, C), G=d(J, d(1, C)), A=d(d(J, B), d(1, E)), E=d(G, d(H, B))]).
prover9_proof(jctir, 135.164, d(A, d(d(2, B), d(d(2, C), d(A, d(D, d(d(d(E, F), d(G, d(d(F, d(1, d(H, I))), D))), A))))))-[J=d(2, 2), D=d(2, I), F=d(2, d(d(2, 1), C)), B=d(1, 2), I=d(1, 3), C=d(1, 1), H=d(J, C), G=d(J, d(1, C)), A=d(d(J, B), d(1, E)), E=d(G, d(H, B))]).
prover9_proof(ancl, 2.819, d(2, d(A, d(d(d(B, C), d(D, d(d(C, d(1, d(E, F))), A))), d(d(G, H), d(1, B)))))-[G=d(2, 2), A=d(2, F), C=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), E=d(G, I), D=d(G, d(1, I)), B=d(D, d(E, H))]).
prover9_proof(ancr, 2.886, d(2, d(A, d(B, d(d(d(C, D), d(E, d(d(D, d(1, d(F, G))), B))), A))))-[H=d(2, 2), B=d(2, G), D=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), F=d(H, I), E=d(H, d(1, I)), A=d(d(H, J), d(1, C)), C=d(E, d(F, J))]).
prover9_proof(anidms, 4.088, d(d(A, B), d(d(2, d(C, d(1, d(2, 3)))), d(d(d(D, E), d(F, d(d(E, d(1, d(C, G))), d(2, G)))), A)))-[H=d(2, 2), E=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), C=d(H, I), F=d(H, d(1, I)), A=d(d(H, J), d(1, D)), B=d(C, J), D=d(F, B)]).
prover9_proof('pm3.45', 182.286, d(d(2, d(1, d(A, d(B, d(d(B, d(d(C, D), d(E, C))), d(B, d(E, d(3, D)))))))), d(B, E))-[F=d(2, 2), A=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), K=d(F, I), L=d(F, d(1, I)), B=d(d(F, J), d(1, M)), E=d(K, J), M=d(L, E), D=d(L, d(d(H, d(1, d(K, G))), A)), C=d(M, H)]).
prover9_proof(anabsi5, 1554.06, d(d(d(d(A, d(B, d(C, D))), E), d(F, d(d(d(2, A), d(1, G)), d(C, d(2, d(H, d(d(H, d(E, I)), G))))))), d(d(2, J), d(K, F)))-[L=d(2, 2), C=d(2, M), N=d(2, d(d(2, 1), J)), D=d(2, O), P=d(1, 2), M=d(1, 3), J=d(1, 1), Q=d(L, J), B=d(L, d(1, J)), G=d(C, d(H, d(d(H, d(d(R, S), I)), d(H, d(A, d(3, S)))))), K=d(N, d(1, O)), H=d(d(L, P), d(1, T)), A=d(Q, P), O=d(Q, M), T=d(B, A), S=d(B, d(K, C)), I=d(A, R), F=d(A, d(T, D)), R=d(T, N), E=d(R, R)]).
prover9_proof(mpan, 204.104, d(d(d(2, A), d(1, d(B, d(d(d(C, D), d(E, d(d(D, d(1, d(F, G))), B))), H)))), d(H, A))-[I=d(2, 2), B=d(2, G), D=d(2, d(d(2, 1), J)), K=d(1, 2), G=d(1, 3), J=d(1, 1), F=d(I, J), E=d(I, d(1, J)), H=d(d(I, K), d(1, C)), A=d(F, K), C=d(E, A)]).
prover9_proof(mpan2, 202.897, d(d(d(2, A), d(1, d(B, d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), B))))), d(B, A))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(I, J), F=d(I, d(1, J)), B=d(d(I, K), d(1, D)), A=d(G, K), D=d(F, A)]).
prover9_proof(mp2an, 96.727, d(A, d(d(d(B, C), d(1, D)), d(d(A, d(E, d(3, d(F, d(d(G, d(1, d(H, I))), A))))), d(D, G))))-[B=d(2, 2), A=d(2, I), G=d(2, d(d(2, 1), J)), C=d(1, 2), I=d(1, 3), J=d(1, 1), H=d(B, J), F=d(B, d(1, J)), E=d(H, C), D=d(F, E)]).
prover9_proof(ad2antrr, 4.129, d(d(d(d(A, B), d(1, C)), D), d(d(E, d(D, d(3, d(F, d(G, E))))), d(G, d(D, d(C, d(2, H))))))-[A=d(2, 2), E=d(2, I), B=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(A, J), F=d(A, d(1, J)), G=d(d(2, d(d(2, 1), J)), d(1, H)), D=d(K, B), H=d(K, I), C=d(F, D)]).
prover9_proof(ad2antlr, 4.128, d(d(d(d(A, B), d(1, C)), D), d(d(E, d(D, d(3, d(F, d(d(d(2, d(d(2, 1), G)), d(1, H)), E))))), d(C, d(C, d(2, H)))))-[A=d(2, 2), E=d(2, I), B=d(1, 2), I=d(1, 3), G=d(1, 1), J=d(A, G), F=d(A, d(1, G)), D=d(J, B), H=d(J, I), C=d(F, D)]).
prover9_proof(ad2antrl, 4.133, d(d(d(d(A, B), d(1, d(C, D))), D), d(d(E, F), d(d(2, G), d(H, F))))-[A=d(2, 2), E=d(2, I), B=d(1, 2), I=d(1, 3), G=d(1, 1), J=d(A, G), C=d(A, d(1, G)), H=d(d(2, d(d(2, 1), G)), d(1, d(J, I))), D=d(J, B), F=d(D, d(3, d(C, d(H, E))))]).
prover9_proof('pm3.33', 377.281, d(d(d(A, d(B, C)), D), d(d(2, d(1, d(B, d(D, d(d(D, d(d(E, F), d(A, E))), d(D, C)))))), d(D, A)))-[G=d(2, 2), B=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), D=d(d(G, K), d(1, N)), A=d(L, K), N=d(M, A), F=d(M, d(d(I, d(1, d(L, H))), B)), C=d(A, d(3, F)), E=d(N, I)]).
prover9_proof('pm3.34', 373.718, d(d(d(A, d(B, C)), D), d(d(E, A), d(2, d(1, d(B, d(D, d(d(D, d(d(E, F), d(A, E))), d(D, C))))))))-[G=d(2, 2), B=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), D=d(d(G, K), d(1, N)), A=d(L, K), N=d(M, A), F=d(M, d(d(I, d(1, d(L, H))), B)), C=d(A, d(3, F)), E=d(N, I)]).
prover9_proof(simpll, 0.413, d(d(A, d(B, d(3, d(C, d(D, A))))), d(D, d(B, d(d(C, B), d(2, E)))))-[F=d(2, 2), A=d(2, G), G=d(1, 3), H=d(1, 1), I=d(F, H), C=d(F, d(1, H)), D=d(d(2, d(d(2, 1), H)), d(1, E)), B=d(I, d(1, 2)), E=d(I, G)]).
prover9_proof(simplld, 0.486, d(A, d(d(B, d(A, d(3, d(C, d(D, B))))), d(D, d(A, d(d(C, A), d(2, E))))))-[F=d(2, 2), B=d(2, G), G=d(1, 3), H=d(1, 1), I=d(F, H), C=d(F, d(1, H)), D=d(d(2, d(d(2, 1), H)), d(1, E)), A=d(I, d(1, 2)), E=d(I, G)]).
prover9_proof(simplr, 0.436, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(F, d(F, d(2, E))))-[G=d(2, 2), A=d(2, H), H=d(1, 3), D=d(1, 1), I=d(G, D), C=d(G, d(1, D)), B=d(I, d(1, 2)), E=d(I, H), F=d(C, B)]).
prover9_proof(simplrd, 0.879, d(A, d(d(B, d(A, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), B))))), d(F, d(F, d(2, E)))))-[G=d(2, 2), B=d(2, H), H=d(1, 3), D=d(1, 1), I=d(G, D), C=d(G, d(1, D)), A=d(I, d(1, 2)), E=d(I, H), F=d(C, A)]).
prover9_proof(simprl, 0.793, d(d(A, B), d(d(2, C), d(D, B)))-[E=d(2, 2), A=d(2, F), F=d(1, 3), C=d(1, 1), G=d(E, C), D=d(d(2, d(d(2, 1), C)), d(1, d(G, F))), B=d(d(G, d(1, 2)), d(3, d(d(E, d(1, C)), d(D, A))))]).
prover9_proof(simprld, 1.019, d(A, d(d(B, C), d(d(2, D), d(E, C))))-[F=d(2, 2), B=d(2, G), G=d(1, 3), D=d(1, 1), H=d(F, D), E=d(d(2, d(d(2, 1), D)), d(1, d(H, G))), A=d(H, d(1, 2)), C=d(A, d(3, d(d(F, d(1, D)), d(E, B))))]).
prover9_proof(simprr, 0.402, d(d(A, d(B, C)), d(d(2, D), d(d(E, B), C)))-[F=d(2, 2), A=d(2, G), C=d(3, d(E, d(d(d(2, d(d(2, 1), D)), d(1, d(H, G))), A))), G=d(1, 3), D=d(1, 1), H=d(F, D), E=d(F, d(1, D)), B=d(H, d(1, 2))]).
prover9_proof(simplll, 0.811, d(d(A, d(3, d(B, C))), d(d(D, C), d(B, d(A, d(d(E, A), d(2, F))))))-[G=d(2, 2), D=d(2, H), H=d(1, 3), I=d(1, 1), J=d(G, I), E=d(G, d(1, I)), B=d(d(2, d(d(2, 1), I)), d(1, F)), A=d(J, d(1, 2)), F=d(J, H), C=d(A, d(3, d(E, d(B, D))))]).
prover9_proof(simpllr, 1.181, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(d(B, F), d(G, F)))-[H=d(2, 2), A=d(2, I), I=d(1, 3), D=d(1, 1), J=d(H, D), C=d(H, d(1, D)), B=d(J, d(1, 2)), E=d(J, I), G=d(C, B), F=d(G, d(2, E))]).
prover9_proof(simplrl, 0.885, d(d(A, d(3, d(B, C))), d(d(D, C), d(E, d(E, d(2, F)))))-[G=d(2, 2), D=d(2, H), H=d(1, 3), I=d(1, 1), J=d(G, I), K=d(G, d(1, I)), B=d(d(2, d(d(2, 1), I)), d(1, F)), A=d(J, d(1, 2)), F=d(J, H), E=d(K, A), C=d(A, d(3, d(K, d(B, D))))]).
prover9_proof(simplrr, 1.513, d(d(A, d(3, d(B, C))), d(d(D, d(A, C)), d(B, d(B, d(2, E)))))-[F=d(2, 2), D=d(2, G), C=d(3, d(H, d(d(d(2, d(d(2, 1), I)), d(1, E)), D))), G=d(1, 3), I=d(1, 1), J=d(F, I), H=d(F, d(1, I)), A=d(J, d(1, 2)), E=d(J, G), B=d(H, A)]).
prover9_proof(simprll, 1.022, d(d(A, d(3, B)), d(d(C, D), d(d(2, E), B)))-[F=d(2, 2), C=d(2, G), G=d(1, 3), E=d(1, 1), H=d(F, E), I=d(d(2, d(d(2, 1), E)), d(1, d(H, G))), A=d(H, d(1, 2)), B=d(I, D), D=d(A, d(3, d(d(F, d(1, E)), d(I, C))))]).
prover9_proof(simprlr, 1.503, d(d(A, d(3, d(d(B, A), C))), d(d(D, E), d(d(2, F), d(G, E))))-[H=d(2, 2), D=d(2, I), C=d(3, d(B, d(G, D))), I=d(1, 3), F=d(1, 1), J=d(H, F), B=d(H, d(1, F)), G=d(d(2, d(d(2, 1), F)), d(1, d(J, I))), A=d(J, d(1, 2)), E=d(A, C)]).
prover9_proof(simprrl, 1.986, d(d(A, d(3, d(B, C))), d(d(D, C), d(d(2, E), d(d(F, A), G))))-[H=d(2, 2), D=d(2, I), G=d(3, d(F, d(B, D))), I=d(1, 3), E=d(1, 1), J=d(H, E), F=d(H, d(1, E)), B=d(d(2, d(d(2, 1), E)), d(1, d(J, I))), A=d(J, d(1, 2)), C=d(A, G)]).
prover9_proof('simp-4l', 2914.504, d(d(d(d(d(2, A), d(1, B)), C), d(d(d(A, d(2, D)), d(2, E)), d(1, d(B, d(C, d(F, d(C, d(G, E)))))))), d(d(H, I), d(1, d(d(A, J), J))))-[H=d(2, 2), F=d(2, I), K=d(1, 2), I=d(1, 3), L=d(1, 1), D=d(1, M), N=d(H, L), O=d(H, d(1, L)), B=d(F, P), C=d(d(H, K), d(1, G)), A=d(N, K), M=d(N, I), G=d(O, A), E=d(C, P), P=d(A, d(3, d(O, d(d(d(2, d(d(2, 1), L)), D), F)))), J=d(G, d(2, M))]).
prover9_proof('pm2.01da', 0.691, d(d(d(A, d(1, 2)), d(d(B, d(1, C)), d(d(2, D), d(2, d(A, D))))), d(2, C))-[B=d(2, 2), D=d(1, 3), C=d(1, 1), A=d(B, C)]).
prover9_proof('pm2.18da', 204.53, d(A, d(B, d(d(d(2, C), d(1, d(D, E))), d(D, d(2, d(A, d(B, d(D, d(A, d(E, d(A, d(C, d(3, F)))))))))))))-[G=d(2, 2), D=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), A=d(d(G, K), d(1, N)), C=d(L, K), N=d(M, C), F=d(M, d(d(I, d(1, d(L, H))), D)), E=d(A, d(d(O, F), P)), B=d(A, d(d(O, O), P)), P=d(C, O), O=d(N, I)]).
prover9_proof('pm3.35', 6.159, d(d(A, B), d(C, d(d(C, d(d(D, D), E)), d(A, d(C, d(d(C, d(d(D, F), E)), d(C, B)))))))-[G=d(2, 2), A=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), C=d(d(G, K), d(1, N)), O=d(L, K), N=d(M, O), F=d(M, d(d(I, d(1, d(L, H))), A)), B=d(O, d(3, F)), E=d(O, D), D=d(N, I)]).
prover9_proof('pm3.4', 0.197, d(d(2, A), d(B, d(2, d(B, d(B, d(2, d(C, A)))))))-[D=d(2, 2), A=d(1, 3), E=d(1, 1), C=d(D, E), B=d(d(D, d(1, E)), d(C, d(1, 2)))]).
prover9_proof('pm2.65da', 4.612, d(A, d(2, d(A, d(d(d(B, C), d(D, d(d(C, d(1, d(E, F))), A))), d(d(G, H), d(1, B))))))-[G=d(2, 2), A=d(2, F), C=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), E=d(G, I), D=d(G, d(1, I)), B=d(D, d(E, H))]).
prover9_proof(syldbl2, 0.339, d(A, d(d(d(2, B), 3), d(d(C, d(D, d(1, 2))), d(3, d(C, d(d(d(2, d(d(2, 1), B)), d(1, d(D, E))), d(2, E)))))))-[A=d(2, 2), E=d(1, 3), B=d(1, 1), D=d(A, B), C=d(A, d(1, B))]).
prover9_proof('pm4.64', 0.241, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof('pm4.66', 0.238, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof('pm2.53', 0.068, d(A, A)-[A=d(2, 1)]).
prover9_proof(imorri, 0.413, d(A, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(d(d(2, d(d(2, 1), D)), d(1, d(B, E))), A))))))-[C=d(2, 2), A=d(2, E), E=d(1, 3), D=d(1, 1), B=d(C, D)]).
prover9_proof(jao1i, 1420.676, d(d(d(A, d(A, d(B, d(C, d(2, D))))), d(E, d(d(2, F), d(G, G)))), d(H, d(d(2, d(1, G)), d(E, H))))-[I=d(2, 2), C=d(2, J), G=d(2, K), F=d(1, 2), J=d(1, 3), K=d(1, 1), L=d(I, K), B=d(I, d(1, K)), H=d(C, d(A, d(3, d(B, d(d(d(2, d(d(2, 1), K)), d(1, D)), C))))), E=d(d(I, F), d(1, d(B, A))), A=d(L, F), D=d(L, J)]).
prover9_proof(orrd, 0.07, d(A, A)-[A=d(2, 1)]).
prover9_proof(orcoms, 4.299, d(d(d(d(A, B), d(1, d(C, D))), D), d(E, d(D, d(3, d(C, d(d(d(2, d(d(2, 1), F)), d(1, d(G, H))), E))))))-[A=d(2, 2), E=d(2, H), B=d(1, 2), H=d(1, 3), F=d(1, 1), G=d(A, F), C=d(A, d(1, F)), D=d(G, B)]).
prover9_proof(olcd, 0.217, d(2, d(1, 1))-[]).
prover9_proof(olcs, 0.124, d(d(A, d(1, B)), d(d(A, B), d(1, 2)))-[A=d(2, 2), B=d(1, 1)]).
prover9_proof('pm3.2ni', 5.974, d(d(A, d(d(B, B), C)), d(D, d(A, d(d(A, d(d(B, E), C)), d(A, d(F, d(3, E)))))))-[G=d(2, 2), D=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), A=d(d(G, K), d(1, N)), F=d(L, K), N=d(M, F), E=d(M, d(d(I, d(1, d(L, H))), D)), C=d(F, B), B=d(N, I)]).
prover9_proof('pm2.45', 0.271, d(3, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(A, d(2, E)))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), B=d(C, D), A=d(d(2, d(d(2, 1), D)), d(1, d(B, E)))]).
prover9_proof('pm2.46', 1.243, d(d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), E)))), E)-[C=d(2, 2), A=d(2, F), F=d(1, 3), D=d(1, 1), B=d(C, D), E=d(d(d(2, d(d(2, 1), D)), d(1, d(B, F))), A)]).
prover9_proof('pm2.47', 0.277, d(d(A, d(d(B, A), d(2, C))), d(3, d(D, d(A, d(3, d(B, d(D, d(2, E))))))))-[F=d(2, 2), E=d(1, 3), G=d(1, 1), H=d(F, G), B=d(F, d(1, G)), D=d(d(2, d(d(2, 1), G)), d(1, C)), A=d(H, d(1, 2)), C=d(H, E)]).
prover9_proof('pm2.48', 1.006, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(A, d(F, d(2, d(F, d(F, d(2, E)))))))-[G=d(2, 2), A=d(2, H), H=d(1, 3), D=d(1, 1), I=d(G, D), C=d(G, d(1, D)), B=d(I, d(1, 2)), E=d(I, H), F=d(C, B)]).
prover9_proof('pm2.49', 0.983, d(d(A, d(d(B, A), d(2, C))), d(3, d(D, d(A, d(3, d(B, d(D, d(2, E))))))))-[F=d(2, 2), E=d(1, 3), G=d(1, 1), H=d(F, G), B=d(F, d(1, G)), D=d(d(2, d(d(2, 1), G)), d(1, C)), A=d(H, d(1, 2)), C=d(H, E)]).
prover9_proof(orel1, 0.422, d(d(d(A, d(1, B)), d(d(A, B), d(1, 2))), d(2, d(d(2, 1), B)))-[A=d(2, 2), B=d(1, 1)]).
prover9_proof(orel2, 2.797, d(d(d(A, B), d(1, d(C, D))), d(E, d(D, d(3, d(C, d(d(d(2, d(d(2, 1), F)), d(1, d(G, H))), E))))))-[A=d(2, 2), E=d(2, H), B=d(1, 2), H=d(1, 3), F=d(1, 1), G=d(A, F), C=d(A, d(1, F)), D=d(G, B)]).
prover9_proof('pm2.67-2', 2.701, d(d(d(A, B), d(1, C)), d(d(D, d(D, d(E, d(3, d(F, d(d(G, H), D)))))), d(d(A, H), d(1, d(C, G)))))-[A=d(2, 2), D=d(2, I), G=d(2, d(d(2, 1), J)), B=d(1, 2), I=d(1, 3), J=d(1, 1), H=d(1, d(K, I)), K=d(A, J), F=d(A, d(1, J)), E=d(K, B), C=d(F, E)]).
prover9_proof('pm2.67', 2.685, d(d(d(A, B), d(1, C)), d(d(D, d(D, d(E, d(3, d(F, d(d(G, H), D)))))), d(d(A, H), d(1, d(C, G)))))-[A=d(2, 2), D=d(2, I), G=d(2, d(d(2, 1), J)), B=d(1, 2), I=d(1, 3), J=d(1, 1), H=d(1, d(K, I)), K=d(A, J), F=d(A, d(1, J)), E=d(K, B), C=d(F, E)]).
prover9_proof(exmid, 0.074, d(d(2, 1), d(1, 1))-[]).
prover9_proof(exmidd, 0.074, d(1, d(d(2, 1), d(1, 1)))-[]).
prover9_proof('pm2.13', 0.183, d(3, d(d(A, d(1, B)), d(d(d(2, d(d(2, 1), B)), d(1, d(d(A, B), C))), d(2, C))))-[A=d(2, 2), C=d(1, 3), B=d(1, 1)]).
prover9_proof('pm2.68', 0.65, d(d(d(A, d(1, B)), d(C, d(1, 2))), d(A, d(1, d(C, d(1, 3)))))-[A=d(2, 2), B=d(1, 1), C=d(A, B)]).
prover9_proof('pm4.25', 3.471, d(d(d(A, d(d(B, d(1, 2)), C)), d(D, E)), d(C, d(D, d(A, d(2, F)))))-[G=d(2, 2), A=d(2, H), C=d(3, E), H=d(1, 3), I=d(1, 1), B=d(G, I), D=d(G, d(1, I)), F=d(B, H), E=d(D, d(d(d(2, d(d(2, 1), I)), d(1, F)), A))]).
prover9_proof('pm2.4', 0.073, d(d(2, 2), d(2, 1))-[]).
prover9_proof('pm2.41', 2.296, d(d(d(A, d(B, d(C, d(2, D)))), E), d(E, d(d(C, d(A, d(3, d(B, d(d(F, d(1, D)), C))))), d(d(B, A), F))))-[G=d(2, 2), C=d(2, H), E=d(2, I), F=d(2, d(d(2, 1), I)), H=d(1, 3), I=d(1, 1), J=d(G, I), B=d(G, d(1, I)), A=d(J, d(1, 2)), D=d(J, H)]).
prover9_proof('pm1.5', 1.058, d(d(A, B), d(1, d(d(A, d(1, C)), d(d(A, C), B))))-[A=d(2, 2), B=d(1, 2), C=d(1, 1)]).
prover9_proof('pm2.31', 360.61, d(d(A, B), d(C, d(d(2, D), d(d(2, E), d(C, B)))))-[F=d(2, 2), G=d(2, H), D=d(1, 2), H=d(1, 3), E=d(1, 1), I=d(F, E), J=d(F, d(1, E)), B=d(G, d(A, d(3, d(J, d(d(d(2, d(d(2, 1), E)), d(1, d(I, H))), G))))), C=d(d(F, D), d(1, d(J, A))), A=d(I, D)]).
prover9_proof('pm2.32', 390.229, d(A, d(d(d(2, B), d(1, d(d(A, d(d(C, C), D)), d(E, d(A, d(d(A, d(d(C, F), D)), d(A, d(B, d(3, F))))))))), d(A, B)))-[G=d(2, 2), E=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), A=d(d(G, K), d(1, N)), B=d(L, K), N=d(M, B), F=d(M, d(d(I, d(1, d(L, H))), E)), D=d(B, C), C=d(N, I)]).
prover9_proof('pm2.3', 0.396, d(A, d(B, d(A, d(3, d(d(C, d(1, D)), d(d(d(2, d(d(2, 1), D)), d(1, d(E, F))), B))))))-[C=d(2, 2), B=d(2, F), F=d(1, 3), D=d(1, 1), E=d(C, D), A=d(E, d(1, 2))]).
prover9_proof('pm2.85', 209.911, d(d(d(2, A), B), d(d(C, D), B))-[C=d(2, 2), D=d(1, 2), E=d(1, 1), B=d(1, d(d(C, d(1, E)), A)), A=d(d(C, E), D)]).
prover9_proof('pm2.75', 0.08, d(d(A, d(1, 1)), d(1, A))-[A=d(2, 2)]).
prover9_proof(biort, 569.248, d(d(d(A, B), d(C, d(d(d(D, E), d(1, B)), d(d(A, d(B, F)), d(d(F, d(1, G)), C))))), d(d(2, d(F, d(1, H))), d(1, d(B, d(2, G)))))-[D=d(2, 2), C=d(2, I), F=d(2, H), E=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(D, J), H=d(d(2, 1), J), A=d(K, E), G=d(K, I), B=d(d(D, d(1, J)), A)]).
prover9_proof('pm2.26', 1.068, d(d(A, d(B, d(d(C, d(1, d(D, E))), d(2, E)))), d(F, A))-[G=d(2, 2), C=d(2, d(d(2, 1), H)), E=d(1, 3), H=d(1, 1), D=d(G, H), B=d(G, d(1, H)), F=d(D, d(1, 2)), A=d(d(B, F), C)]).
prover9_proof('pm2.63', 203.428, d(d(d(2, A), d(1, B)), d(C, d(2, d(D, d(d(D, d(d(E, E), F)), B)))))-[G=d(2, 2), C=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), B=d(C, d(D, d(d(D, d(d(E, N), F)), d(D, d(A, d(3, N)))))), D=d(d(G, K), d(1, O)), A=d(L, K), O=d(M, A), N=d(M, d(d(I, d(1, d(L, H))), C)), F=d(A, E), E=d(O, I)]).
prover9_proof('pm2.64', 4.64, d(A, d(2, d(A, d(d(d(B, C), d(D, d(d(C, d(1, d(E, F))), A))), d(d(G, H), d(1, B))))))-[G=d(2, 2), A=d(2, F), C=d(2, d(d(2, 1), I)), H=d(1, 2), F=d(1, 3), I=d(1, 1), E=d(G, I), D=d(G, d(1, I)), B=d(D, d(E, H))]).
prover9_proof('pm2.42', 6.868, d(d(2, d(1, d(A, B))), d(C, d(C, d(d(D, d(1, 2)), d(3, d(d(A, d(1, E)), d(d(d(2, d(B, E)), d(1, d(D, F))), C)))))))-[A=d(2, 2), B=d(2, 1), C=d(2, F), F=d(1, 3), E=d(1, 1), D=d(A, E)]).
prover9_proof(orim2d, 0.12, d(A, A)-[A=d(d(d(2, 2), d(1, 1)), d(1, 2))]).
prover9_proof(orim2, 0.106, d(d(d(2, 2), d(1, 1)), d(1, 2))-[]).
prover9_proof('pm2.38', 197.866, d(d(d(2, A), d(1, d(B, d(C, d(d(C, d(d(D, E), d(A, D))), d(C, d(A, d(3, E)))))))), d(C, A))-[F=d(2, 2), B=d(2, G), H=d(2, d(d(2, 1), I)), J=d(1, 2), G=d(1, 3), I=d(1, 1), K=d(F, I), L=d(F, d(1, I)), C=d(d(F, J), d(1, M)), A=d(K, J), M=d(L, A), E=d(L, d(d(H, d(1, d(K, G))), B)), D=d(M, H)]).
prover9_proof('pm2.36', 384.875, d(d(d(2, A), d(1, d(B, d(C, d(d(C, d(d(D, E), d(A, D))), d(C, F)))))), d(C, d(d(A, A), d(B, F))))-[G=d(2, 2), B=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), C=d(d(G, K), d(1, N)), A=d(L, K), N=d(M, A), E=d(M, d(d(I, d(1, d(L, H))), B)), F=d(A, d(3, E)), D=d(N, I)]).
prover9_proof('pm2.37', 396.902, d(A, d(d(d(2, B), d(1, d(C, d(B, d(3, d(D, d(d(d(2, d(d(2, 1), E)), d(1, d(F, G))), C))))))), d(A, B)))-[H=d(2, 2), C=d(2, G), I=d(1, 2), G=d(1, 3), E=d(1, 1), F=d(H, E), D=d(H, d(1, E)), A=d(d(H, I), d(1, d(D, B))), B=d(F, I)]).
prover9_proof('pm2.8', 197.693, d(d(d(A, B), d(1, d(C, D))), d(d(D, D), d(E, d(E, d(D, d(3, d(C, d(d(d(2, d(d(2, 1), F)), d(1, d(G, H))), E))))))))-[A=d(2, 2), E=d(2, H), B=d(1, 2), H=d(1, 3), F=d(1, 1), G=d(A, F), C=d(A, d(1, F)), D=d(G, B)]).
prover9_proof(animorl, 0.286, d(d(A, d(d(B, A), d(2, C))), d(3, d(D, d(A, d(3, d(B, d(D, d(2, E))))))))-[F=d(2, 2), E=d(1, 3), G=d(1, 1), H=d(F, G), B=d(F, d(1, G)), D=d(d(2, d(d(2, 1), G)), d(1, C)), A=d(H, d(1, 2)), C=d(H, E)]).
prover9_proof(animorr, 0.191, d(d(2, A), d(B, d(2, d(B, d(B, d(2, d(C, A)))))))-[D=d(2, 2), A=d(1, 3), E=d(1, 1), C=d(D, E), B=d(d(D, d(1, E)), d(C, d(1, 2)))]).
prover9_proof(animorlr, 0.275, d(d(2, A), d(3, d(B, d(d(C, d(1, 2)), d(3, d(d(D, d(1, A)), d(B, d(2, E))))))))-[D=d(2, 2), E=d(1, 3), A=d(1, 1), C=d(D, A), B=d(d(2, d(d(2, 1), A)), d(1, d(C, E)))]).
prover9_proof(animorrl, 0.145, d(A, d(2, d(A, d(A, d(2, d(B, d(1, 3)))))))-[C=d(2, 2), D=d(1, 1), B=d(C, D), A=d(d(C, d(1, D)), d(B, d(1, 2)))]).
prover9_proof('pm4.55', 4.142, d(d(d(A, d(1, d(2, 3))), d(3, B)), d(C, d(C, d(d(D, E), d(1, F)))))-[D=d(2, 2), G=d(2, d(d(2, 1), H)), E=d(1, 2), I=d(1, 3), H=d(1, 1), A=d(D, H), J=d(D, d(1, H)), F=d(J, d(A, E)), B=d(J, d(d(G, d(1, d(A, I))), d(2, I))), C=d(d(F, G), B)]).
prover9_proof('pm3.1', 2.857, d(d(A, d(d(d(B, C), d(1, D)), d(d(E, F), d(G, E)))), d(H, d(A, d(A, H))))-[B=d(2, 2), A=d(2, I), J=d(2, d(d(2, 1), K)), C=d(1, 2), I=d(1, 3), K=d(1, 1), L=d(B, K), M=d(B, d(1, K)), G=d(L, C), D=d(M, G), F=d(M, d(d(J, d(1, d(L, I))), A)), H=d(G, d(3, F)), E=d(D, J)]).
prover9_proof('pm3.11', 4.279, d(d(A, d(B, d(3, C))), d(D, D))-[E=d(2, 2), A=d(2, F), G=d(2, d(d(2, 1), H)), I=d(1, 2), F=d(1, 3), H=d(1, 1), J=d(E, H), K=d(E, d(1, H)), B=d(J, I), L=d(K, B), C=d(K, d(d(G, d(1, d(J, F))), A)), D=d(d(d(E, I), d(1, L)), d(d(M, C), d(B, M))), M=d(L, G)]).
prover9_proof('pm3.13', 2.794, d(A, A)-[B=d(2, 2), C=d(2, d(d(2, 1), D)), E=d(1, 2), F=d(1, 3), D=d(1, 1), G=d(B, D), H=d(B, d(1, D)), I=d(G, E), J=d(H, I), A=d(d(d(B, E), d(1, J)), d(d(K, d(H, d(d(C, d(1, d(G, F))), d(2, F)))), d(I, K))), K=d(J, C)]).
prover9_proof('pm3.14', 0.449, d(A, d(B, d(B, A)))-[C=d(2, 2), B=d(2, D), D=d(1, 3), E=d(1, 1), F=d(C, E), A=d(d(F, d(1, 2)), d(3, d(d(C, d(1, E)), d(d(d(2, d(d(2, 1), E)), d(1, d(F, D))), B))))]).
prover9_proof(orcanai, 384.982, d(d(A, d(B, C)), d(D, d(d(2, E), d(d(2, F), d(D, d(B, d(D, d(d(D, d(d(G, H), d(A, G))), d(D, C)))))))))-[I=d(2, 2), B=d(2, J), K=d(2, d(d(2, 1), F)), E=d(1, 2), J=d(1, 3), F=d(1, 1), L=d(I, F), M=d(I, d(1, F)), D=d(d(I, E), d(1, N)), A=d(L, E), N=d(M, A), H=d(M, d(d(K, d(1, d(L, J))), B)), C=d(A, d(3, H)), G=d(N, K)]).
prover9_proof(bianir, 278.069, d(d(A, B), d(d(C, B), d(d(2, d(1, d(2, D))), d(E, d(d(E, d(d(F, F), G)), d(A, d(E, d(d(E, d(d(F, H), G)), d(E, B)))))))))-[I=d(2, 2), A=d(2, J), K=d(2, d(d(2, 1), D)), L=d(1, 2), J=d(1, 3), D=d(1, 1), M=d(I, D), N=d(I, d(1, D)), E=d(d(I, L), d(1, O)), C=d(M, L), O=d(N, C), H=d(N, d(d(K, d(1, d(M, J))), A)), B=d(C, d(3, H)), G=d(C, F), F=d(O, K)]).
prover9_proof(ornld, 423.192, d(d(d(d(2, A), d(1, B)), C), d(d(C, d(d(2, D), d(E, d(C, B)))), d(C, d(d(2, d(1, F)), d(E, G)))))-[F=d(2, 2), H=d(2, I), E=d(2, J), D=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(F, J), L=d(F, d(1, J)), B=d(H, d(A, d(3, d(L, G)))), C=d(d(F, D), d(1, d(L, A))), A=d(K, D), G=d(d(d(2, d(d(2, 1), J)), d(1, d(K, I))), H)]).
prover9_proof('1fpid3', 1346.446, d(d(d(2, A), d(1, d(B, d(C, d(D, d(C, d(A, d(3, E)))))))), d(d(C, d(d(2, F), d(d(2, G), d(C, d(A, E))))), d(C, d(d(A, d(B, D)), d(2, d(H, d(C, d(B, d(I, C)))))))))-[J=d(2, 2), B=d(2, K), L=d(2, d(d(2, 1), G)), F=d(1, 2), K=d(1, 3), G=d(1, 1), M=d(J, G), N=d(J, d(1, G)), C=d(d(J, F), d(1, H)), A=d(M, F), H=d(N, A), E=d(N, d(d(L, d(1, d(M, K))), B)), D=d(C, d(I, d(A, O))), O=d(H, L), I=d(O, E)]).
prover9_proof('3orel1', 202.126, d(d(d(2, A), d(1, d(d(B, d(d(C, C), D)), d(E, d(B, d(d(B, d(d(C, F), D)), d(B, d(A, d(3, F))))))))), d(B, A))-[G=d(2, 2), E=d(2, H), I=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), L=d(G, J), M=d(G, d(1, J)), B=d(d(G, K), d(1, N)), A=d(L, K), N=d(M, A), F=d(M, d(d(I, d(1, d(L, H))), E)), D=d(A, C), C=d(N, I)]).
prover9_proof('3impia', 383.631, d(d(A, d(B, C)), d(D, d(d(2, E), d(d(2, F), d(D, d(B, d(D, d(d(D, d(d(G, H), d(A, G))), d(D, C)))))))))-[I=d(2, 2), B=d(2, J), K=d(2, d(d(2, 1), F)), E=d(1, 2), J=d(1, 3), F=d(1, 1), L=d(I, F), M=d(I, d(1, F)), D=d(d(I, E), d(1, N)), A=d(L, E), N=d(M, A), H=d(M, d(d(K, d(1, d(L, J))), B)), C=d(A, d(3, H)), G=d(N, K)]).
prover9_proof('3expia', 399.162, d(A, d(d(d(2, B), d(1, d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), A)))), d(A, B)))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(I, J), F=d(I, d(1, J)), A=d(d(I, K), d(1, D)), B=d(G, K), D=d(F, B)]).
prover9_proof('3adant3', 2.765, d(d(d(A, B), d(1, C)), d(d(D, d(3, d(E, d(F, d(3, d(G, d(E, d(2, H)))))))), d(F, D)))-[A=d(2, 2), I=d(2, d(d(2, 1), J)), B=d(1, 2), H=d(1, 3), J=d(1, 1), K=d(A, J), G=d(A, d(1, J)), E=d(I, d(1, d(K, H))), F=d(K, B), C=d(G, F), D=d(C, I)]).
prover9_proof('3ad2ant3', 3.386, d(d(d(A, B), d(1, C)), d(d(D, d(C, E)), d(3, d(C, d(3, d(F, d(d(E, d(1, d(G, H))), d(2, H))))))))-[A=d(2, 2), E=d(2, d(d(2, 1), I)), B=d(1, 2), H=d(1, 3), I=d(1, 1), G=d(A, I), F=d(A, d(1, I)), D=d(G, B), C=d(F, D)]).
prover9_proof(simp3, 0.251, d(3, d(d(A, d(B, d(1, 2))), d(3, d(A, d(d(d(2, d(d(2, 1), C)), d(1, d(B, D))), d(2, D))))))-[E=d(2, 2), D=d(1, 3), C=d(1, 1), B=d(E, C), A=d(E, d(1, C))]).
prover9_proof(simp3d, 0.25, d(A, d(3, d(d(B, A), d(3, d(B, d(d(d(2, d(d(2, 1), C)), d(1, d(D, E))), d(2, E)))))))-[F=d(2, 2), E=d(1, 3), C=d(1, 1), D=d(F, C), B=d(F, d(1, C)), A=d(D, d(1, 2))]).
prover9_proof(simp3bi, 3.108, d(d(d(d(A, B), d(1, C)), d(d(D, d(3, d(E, d(F, G)))), d(F, D))), d(F, d(3, d(C, G))))-[A=d(2, 2), H=d(2, d(d(2, 1), I)), G=d(3, d(J, d(E, d(2, K)))), B=d(1, 2), K=d(1, 3), I=d(1, 1), L=d(A, I), J=d(A, d(1, I)), E=d(H, d(1, d(L, K))), F=d(L, B), C=d(J, F), D=d(C, H)]).
prover9_proof('3simpa', 0.311, d(3, d(A, d(d(B, d(1, 2)), d(3, d(d(C, d(1, D)), d(A, d(2, E)))))))-[C=d(2, 2), E=d(1, 3), D=d(1, 1), B=d(C, D), A=d(d(2, d(d(2, 1), D)), d(1, d(B, E)))]).
prover9_proof('3simpb', 6.046, d(d(A, d(B, d(d(B, d(d(C, D), E)), d(B, F)))), d(B, d(d(C, d(3, d(G, F))), E)))-[H=d(2, 2), A=d(2, I), J=d(2, d(d(2, 1), K)), L=d(1, 2), I=d(1, 3), K=d(1, 1), M=d(H, K), N=d(H, d(1, K)), G=d(J, d(1, d(M, I))), B=d(d(H, L), d(1, O)), P=d(M, L), O=d(N, P), D=d(N, d(G, A)), F=d(P, d(3, D)), E=d(P, C), C=d(O, J)]).
prover9_proof('3simpc', 6.061, d(d(A, d(B, d(d(B, d(d(C, D), E)), d(B, d(F, G))))), d(B, d(E, d(3, d(H, G)))))-[I=d(2, 2), A=d(2, J), K=d(2, d(d(2, 1), L)), G=d(3, D), M=d(1, 2), J=d(1, 3), L=d(1, 1), N=d(I, L), O=d(I, d(1, L)), B=d(d(I, M), d(1, H)), F=d(N, M), H=d(O, F), D=d(O, d(d(K, d(1, d(N, J))), A)), E=d(F, C), C=d(H, K)]).
prover9_proof(ad4ant123, 2.762, d(d(d(A, B), d(1, C)), d(d(D, d(3, d(E, d(F, d(3, d(G, d(E, d(2, H)))))))), d(F, D)))-[A=d(2, 2), I=d(2, d(d(2, 1), J)), B=d(1, 2), H=d(1, 3), J=d(1, 1), K=d(A, J), G=d(A, d(1, J)), E=d(I, d(1, d(K, H))), F=d(K, B), C=d(G, F), D=d(C, I)]).
prover9_proof(simpl3, 0.443, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(F, d(F, d(2, E))))-[G=d(2, 2), A=d(2, H), H=d(1, 3), D=d(1, 1), I=d(G, D), C=d(G, d(1, D)), B=d(I, d(1, 2)), E=d(I, H), F=d(C, B)]).
prover9_proof(simpr3, 0.446, d(d(A, d(B, C)), d(d(2, D), d(d(E, B), C)))-[F=d(2, 2), A=d(2, G), C=d(3, d(E, d(d(d(2, d(d(2, 1), D)), d(1, d(H, G))), A))), G=d(1, 3), D=d(1, 1), H=d(F, D), E=d(F, d(1, D)), B=d(H, d(1, 2))]).
prover9_proof(simp3l, 0.825, d(d(A, B), d(d(2, C), d(D, B)))-[E=d(2, 2), A=d(2, F), F=d(1, 3), C=d(1, 1), G=d(E, C), D=d(d(2, d(d(2, 1), C)), d(1, d(G, F))), B=d(d(G, d(1, 2)), d(3, d(d(E, d(1, C)), d(D, A))))]).
prover9_proof(simp3r, 0.443, d(d(A, d(B, C)), d(d(2, D), d(d(E, B), C)))-[F=d(2, 2), A=d(2, G), C=d(3, d(E, d(d(d(2, d(d(2, 1), D)), d(1, d(H, G))), A))), G=d(1, 3), D=d(1, 1), H=d(F, D), E=d(F, d(1, D)), B=d(H, d(1, 2))]).
prover9_proof(simp13, 1.217, d(d(A, d(B, d(3, d(C, d(d(d(2, d(d(2, 1), D)), d(1, E)), A))))), d(d(B, F), d(G, F)))-[H=d(2, 2), A=d(2, I), I=d(1, 3), D=d(1, 1), J=d(H, D), C=d(H, d(1, D)), B=d(J, d(1, 2)), E=d(J, I), G=d(C, B), F=d(G, d(2, E))]).
prover9_proof(simp23, 1.535, d(d(A, d(3, d(B, C))), d(d(D, d(A, C)), d(B, d(B, d(2, E)))))-[F=d(2, 2), D=d(2, G), C=d(3, d(H, d(d(d(2, d(d(2, 1), I)), d(1, E)), D))), G=d(1, 3), I=d(1, 1), J=d(F, I), H=d(F, d(1, I)), A=d(J, d(1, 2)), E=d(J, G), B=d(H, A)]).
prover9_proof(simp31, 1.062, d(d(A, d(3, B)), d(d(C, D), d(d(2, E), B)))-[F=d(2, 2), C=d(2, G), G=d(1, 3), E=d(1, 1), H=d(F, E), I=d(d(2, d(d(2, 1), E)), d(1, d(H, G))), A=d(H, d(1, 2)), B=d(I, D), D=d(A, d(3, d(d(F, d(1, E)), d(I, C))))]).
prover9_proof(simp32, 1.568, d(d(A, d(3, d(d(B, A), C))), d(d(D, E), d(d(2, F), d(G, E))))-[H=d(2, 2), D=d(2, I), C=d(3, d(B, d(G, D))), I=d(1, 3), F=d(1, 1), J=d(H, F), B=d(H, d(1, F)), G=d(d(2, d(d(2, 1), F)), d(1, d(J, I))), A=d(J, d(1, 2)), E=d(A, C)]).
prover9_proof(simp33, 0.445, d(d(A, d(B, C)), d(d(2, D), d(d(E, B), C)))-[F=d(2, 2), A=d(2, G), C=d(3, d(E, d(d(d(2, d(d(2, 1), D)), d(1, d(H, G))), A))), G=d(1, 3), D=d(1, 1), H=d(F, D), E=d(F, d(1, D)), B=d(H, d(1, 2))]).
prover9_proof(simprl3, 1.525, d(d(A, d(3, d(d(B, A), C))), d(d(D, E), d(d(2, F), d(G, E))))-[H=d(2, 2), D=d(2, I), C=d(3, d(B, d(G, D))), I=d(1, 3), F=d(1, 1), J=d(H, F), B=d(H, d(1, F)), G=d(d(2, d(d(2, 1), F)), d(1, d(J, I))), A=d(J, d(1, 2)), E=d(A, C)]).
prover9_proof(simpl3l, 0.927, d(d(A, d(3, d(B, C))), d(d(D, C), d(E, d(E, d(2, F)))))-[G=d(2, 2), D=d(2, H), H=d(1, 3), I=d(1, 1), J=d(G, I), K=d(G, d(1, I)), B=d(d(2, d(d(2, 1), I)), d(1, F)), A=d(J, d(1, 2)), F=d(J, H), E=d(K, A), C=d(A, d(3, d(K, d(B, D))))]).
prover9_proof(simpl3r, 1.529, d(d(A, d(3, d(B, C))), d(d(D, d(A, C)), d(B, d(B, d(2, E)))))-[F=d(2, 2), D=d(2, G), C=d(3, d(H, d(d(d(2, d(d(2, 1), I)), d(1, E)), D))), G=d(1, 3), I=d(1, 1), J=d(F, I), H=d(F, d(1, I)), A=d(J, d(1, 2)), E=d(J, G), B=d(H, A)]).
prover9_proof(simpr3l, 2.034, d(d(A, d(3, d(B, C))), d(d(D, C), d(d(2, E), d(d(F, A), G))))-[H=d(2, 2), D=d(2, I), G=d(3, d(F, d(B, D))), I=d(1, 3), E=d(1, 1), J=d(H, E), F=d(H, d(1, E)), B=d(d(2, d(d(2, 1), E)), d(1, d(J, I))), A=d(J, d(1, 2)), C=d(A, G)]).
prover9_proof(simp3rl, 2.051, d(d(A, d(3, d(B, C))), d(d(D, C), d(d(2, E), d(d(F, A), G))))-[H=d(2, 2), D=d(2, I), G=d(3, d(F, d(B, D))), I=d(1, 3), E=d(1, 1), J=d(H, E), F=d(H, d(1, E)), B=d(d(2, d(d(2, 1), E)), d(1, d(J, I))), A=d(J, d(1, 2)), C=d(A, G)]).
prover9_proof(simpl33, 1.541, d(d(A, d(3, d(B, C))), d(d(D, d(A, C)), d(B, d(B, d(2, E)))))-[F=d(2, 2), D=d(2, G), C=d(3, d(H, d(d(d(2, d(d(2, 1), I)), d(1, E)), D))), G=d(1, 3), I=d(1, 1), J=d(F, I), H=d(F, d(1, I)), A=d(J, d(1, 2)), E=d(J, G), B=d(H, A)]).
prover9_proof(simp3l3, 1.624, d(d(A, d(3, d(d(B, A), C))), d(d(D, E), d(d(2, F), d(G, E))))-[H=d(2, 2), D=d(2, I), C=d(3, d(B, d(G, D))), I=d(1, 3), F=d(1, 1), J=d(H, F), B=d(H, d(1, F)), G=d(d(2, d(d(2, 1), F)), d(1, d(J, I))), A=d(J, d(1, 2)), E=d(A, C)]).
prover9_proof(simp33l, 2.186, d(d(A, d(3, d(B, C))), d(d(D, C), d(d(2, E), d(d(F, A), G))))-[H=d(2, 2), D=d(2, I), G=d(3, d(F, d(B, D))), I=d(1, 3), E=d(1, 1), J=d(H, E), F=d(H, d(1, E)), B=d(d(2, d(d(2, 1), E)), d(1, d(J, I))), A=d(J, d(1, 2)), C=d(A, G)]).
prover9_proof('3mix1', 0.148, d(d(A, B), B)-[C=d(2, 2), D=d(1, 1), E=d(C, D), A=d(E, d(1, 2)), B=d(d(d(C, d(1, D)), A), d(2, d(E, d(1, 3))))]).
prover9_proof('3mix2', 0.111, d(A, d(A, d(2, d(B, d(1, 3)))))-[C=d(2, 2), D=d(1, 1), B=d(C, D), A=d(d(C, d(1, D)), d(B, d(1, 2)))]).
prover9_proof('3mix1d', 0.146, d(A, d(d(A, B), B))-[C=d(2, 2), D=d(1, 1), E=d(C, D), A=d(E, d(1, 2)), B=d(d(d(C, d(1, D)), A), d(2, d(E, d(1, 3))))]).
prover9_proof('3mix2d', 0.117, d(A, d(B, d(B, d(2, d(C, d(1, 3))))))-[D=d(2, 2), E=d(1, 1), C=d(D, E), A=d(C, d(1, 2)), B=d(d(D, d(1, E)), A)]).
prover9_proof('3mix3d', 0.079, d(2, d(1, 1))-[]).
prover9_proof(ex3, 400.715, d(A, d(d(d(2, B), d(1, d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), A)))), d(A, B)))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(I, J), F=d(I, d(1, J)), A=d(d(I, K), d(1, D)), B=d(G, K), D=d(F, B)]).
prover9_proof(ad5ant123, 4.126, d(d(d(d(A, B), d(1, C)), D), d(d(E, d(D, d(3, d(F, d(G, E))))), d(G, d(D, d(C, d(2, H))))))-[A=d(2, 2), E=d(2, I), B=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(A, J), F=d(A, d(1, J)), G=d(d(2, d(d(2, 1), J)), d(1, H)), D=d(K, B), H=d(K, I), C=d(F, D)]).
prover9_proof(mp3an3, 203.316, d(d(d(2, A), d(1, d(B, d(C, d(d(d(D, E), d(F, d(d(E, d(1, d(G, H))), C))), B))))), d(B, A))-[I=d(2, 2), C=d(2, H), E=d(2, d(d(2, 1), J)), K=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(I, J), F=d(I, d(1, J)), B=d(d(I, K), d(1, D)), A=d(G, K), D=d(F, A)]).
prover9_proof(intn3an1d, 3156.184, d(d(d(2, A), d(B, C)), d(d(d(D, d(B, d(E, F))), d(D, d(B, d(G, d(3, d(H, G)))))), d(d(d(D, d(I, J)), d(D, d(J, d(d(2, d(C, d(1, d(2, 3)))), d(K, L))))), d(G, d(d(D, d(M, d(d(D, d(N, d(I, d(2, O)))), P))), d(L, d(d(I, d(I, G)), d(P, d(1, Q)))))))))-[E=d(2, 2), F=d(2, 1), I=d(2, R), B=d(2, S), T=d(2, d(F, S)), A=d(1, 2), R=d(1, 3), S=d(1, 1), U=d(1, O), C=d(E, S), N=d(E, d(1, S)), P=d(E, U), H=d(T, U), L=d(d(E, A), d(1, M)), D=d(C, A), O=d(C, R), M=d(N, D), V=d(N, d(H, I)), J=d(L, d(K, d(D, Q))), G=d(D, d(3, V)), Q=d(M, T), K=d(Q, V)]).
prover9_proof(intn3an2d, 0.76, d(A, d(d(A, d(3, d(B, d(d(d(2, d(d(2, 1), C)), d(1, D)), d(2, E))))), d(F, d(F, d(2, D)))))-[G=d(2, 2), E=d(1, 3), C=d(1, 1), H=d(G, C), B=d(G, d(1, C)), A=d(H, d(1, 2)), D=d(H, E), F=d(B, A)]).
prover9_proof(intn3an3d, 0.247, d(A, d(d(B, A), d(3, d(B, d(d(d(2, d(d(2, 1), C)), d(1, d(D, E))), d(2, E))))))-[F=d(2, 2), E=d(1, 3), C=d(1, 1), D=d(F, C), B=d(F, d(1, C)), A=d(D, d(1, 2))]).
prover9_proof('3orel2', 152.563, d(d(A, d(B, d(d(B, d(d(C, C), D)), d(E, d(B, d(d(B, d(d(C, F), D)), d(B, d(G, d(3, F))))))))), A)-[H=d(2, 2), E=d(2, I), J=d(2, d(d(2, 1), K)), L=d(1, 2), I=d(1, 3), K=d(1, 1), M=d(H, K), N=d(H, d(1, K)), B=d(d(H, L), d(1, O)), G=d(M, L), O=d(N, G), F=d(N, d(d(J, d(1, d(M, I))), E)), A=d(B, G), D=d(G, C), C=d(O, J)]).
prover9_proof('3orel3', 2.725, d(d(d(A, B), d(1, d(C, D))), d(E, d(D, d(3, d(C, d(d(d(2, d(d(2, 1), F)), d(1, d(G, H))), E))))))-[A=d(2, 2), E=d(2, H), B=d(1, 2), H=d(1, 3), F=d(1, 1), G=d(A, F), C=d(A, d(1, F)), D=d(G, B)]).
prover9_proof(dfnan2, 4.193, d(d(d(A, d(1, d(2, 3))), d(3, B)), d(C, d(C, d(d(D, E), d(1, F)))))-[D=d(2, 2), G=d(2, d(d(2, 1), H)), E=d(1, 2), I=d(1, 3), H=d(1, 1), A=d(D, H), J=d(D, d(1, H)), F=d(J, d(A, E)), B=d(J, d(d(G, d(1, d(A, I))), d(2, I))), C=d(d(F, G), B)]).
prover9_proof(xnor, 4.141, d(d(d(A, d(1, d(2, 3))), B), d(d(C, d(3, B)), d(d(C, B), d(d(D, E), d(1, F)))))-[D=d(2, 2), G=d(2, d(d(2, 1), H)), E=d(1, 2), I=d(1, 3), H=d(1, 1), A=d(D, H), J=d(D, d(1, H)), F=d(J, d(A, E)), B=d(J, d(d(G, d(1, d(A, I))), d(2, I))), C=d(F, G)]).
prover9_proof('pm2.21fal', 0.471, d(d(2, A), d(B, d(d(d(C, d(1, D)), B), d(2, d(E, d(1, 3))))))-[C=d(2, 2), A=d(1, 2), D=d(1, 1), E=d(C, D), B=d(E, A)]).
prover9_proof(nottru, 0.293, d(d(d(2, 3), A), d(d(B, d(1, A)), d(d(B, d(1, C)), d(d(d(2, D), d(1, d(d(B, C), E))), d(2, E)))))-[B=d(2, 2), E=d(1, 3), C=d(1, 1), A=d(1, D), D=d(d(2, 1), C)]).
prover9_proof(truortru, 4.686, d(d(A, d(B, d(C, d(2, D)))), d(B, d(C, d(d(A, d(B, d(d(E, d(1, D)), C))), d(d(F, G), d(1, H))))))-[F=d(2, 2), C=d(2, I), E=d(2, d(d(2, 1), J)), G=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(F, J), B=d(F, d(1, J)), D=d(K, I), H=d(B, d(K, G)), A=d(H, E)]).
prover9_proof(falorfal, 4.637, d(d(A, d(B, d(C, d(2, D)))), d(B, d(C, d(d(A, d(B, d(d(E, d(1, D)), C))), d(d(F, G), d(1, H))))))-[F=d(2, 2), C=d(2, I), E=d(2, d(d(2, 1), J)), G=d(1, 2), I=d(1, 3), J=d(1, 1), K=d(F, J), B=d(F, d(1, J)), D=d(K, I), H=d(B, d(K, G)), A=d(H, E)]).
prover9_proof('minimp-ax2c', 0.124, d(d(A, d(1, 1)), d(1, A))-[A=d(2, 2)]).
prover9_proof(impsingle, 428.057, d(d(A, d(d(2, B), d(C, d(D, d(2, C))))), d(d(d(D, d(E, F)), A), d(d(E, d(1, d(D, d(2, d(D, d(D, d(2, G))))))), d(d(H, d(d(I, J), K)), d(L, d(A, d(d(A, d(d(H, H), M)), d(I, d(A, d(d(A, K), d(A, J)))))))))))-[E=d(2, 2), I=d(2, F), C=d(2, N), O=d(2, d(d(2, 1), N)), B=d(1, 2), F=d(1, 3), N=d(1, 1), P=d(E, N), Q=d(E, d(1, N)), A=d(d(E, B), d(1, D)), L=d(P, B), G=d(P, F), D=d(Q, L), R=d(Q, d(d(O, d(1, G)), I)), J=d(L, d(3, R)), M=d(L, H), H=d(D, O), K=d(d(H, R), M)]).
prover9_proof('impsingle-step4', 1.029, d(d(2, A), d(d(B, C), d(d(C, d(B, d(d(2, D), d(2, E)))), d(F, d(1, E)))))-[F=d(2, 2), D=d(1, 3), A=d(1, 1), G=d(F, A), B=d(F, d(1, A)), C=d(G, d(1, 2)), E=d(G, D)]).
prover9_proof('impsingle-step25', 659.508, d(A, d(d(d(2, B), d(1, d(C, d(A, d(d(A, d(d(D, E), F)), d(A, G)))))), d(d(B, d(d(d(B, d(H, d(C, d(2, I)))), J), d(J, d(d(C, G), D)))), d(B, d(d(D, d(3, d(K, G))), F)))))-[L=d(2, 2), C=d(2, M), J=d(2, N), O=d(2, d(d(2, 1), N)), P=d(1, 2), M=d(1, 3), N=d(1, 1), Q=d(L, N), H=d(L, d(1, N)), K=d(O, d(1, I)), A=d(d(L, P), d(1, R)), B=d(Q, P), I=d(Q, M), R=d(H, B), E=d(H, d(K, C)), G=d(B, d(3, E)), F=d(B, D), D=d(R, O)]).
prover9_proof(merlem1, 4.177, d(d(d(d(A, B), d(1, C)), D), d(d(2, E), d(C, d(2, d(F, d(1, 3))))))-[A=d(2, 2), B=d(1, 2), E=d(1, 1), F=d(A, E), D=d(F, B), C=d(d(A, d(1, E)), D)]).
prover9_proof(merlem2, 0.132, d(d(2, A), d(d(2, B), d(1, B)))-[A=d(1, 1), B=d(d(2, 1), A)]).
prover9_proof(merlem4, 0.159, d(d(d(A, d(1, B)), d(d(A, B), d(1, 2))), d(2, d(2, B)))-[A=d(2, 2), B=d(1, 1)]).
prover9_proof(merlem5, 2.763, d(d(d(A, B), d(1, C)), d(d(D, d(E, d(d(F, d(1, d(G, H))), d(2, H)))), d(I, D)))-[A=d(2, 2), F=d(2, d(d(2, 1), J)), B=d(1, 2), H=d(1, 3), J=d(1, 1), G=d(A, J), E=d(A, d(1, J)), I=d(G, B), C=d(E, I), D=d(C, F)]).
prover9_proof(merlem6, 0.159, d(A, d(A, d(2, d(2, B))))-[C=d(2, 2), B=d(1, 1), A=d(d(C, d(1, B)), d(d(C, B), d(1, 2)))]).
prover9_proof(merlem10, 0.12, d(d(2, d(1, 1)), d(d(2, 2), d(2, 1)))-[]).
prover9_proof(merlem12, 0.233, d(d(A, d(A, B)), d(C, d(d(B, d(1, d(D, E))), d(2, E))))-[F=d(2, 2), B=d(2, d(d(2, 1), G)), E=d(1, 3), G=d(1, 1), D=d(F, G), C=d(F, d(1, G)), A=d(C, d(D, d(1, 2)))]).
prover9_proof(luklem2, 1791.979, d(d(d(d(d(2, A), B), C), d(d(D, d(E, d(1, d(d(2, F), d(1, F))))), d(G, d(d(2, H), d(d(2, I), d(D, d(2, d(J, d(1, 3))))))))), C)-[E=d(2, 2), H=d(1, 2), I=d(1, 1), B=d(1, D), J=d(E, I), F=d(d(2, 1), I), G=d(d(E, H), B), A=d(J, H), D=d(d(E, d(1, I)), A), C=d(G, A)]).
prover9_proof(luklem3, 3.083, d(d(d(d(A, B), d(1, C)), d(d(D, d(D, d(E, d(3, d(F, d(d(G, H), D)))))), d(d(A, H), d(1, d(C, G))))), d(C, d(2, d(2, I))))-[A=d(2, 2), D=d(2, J), G=d(2, d(d(2, 1), I)), B=d(1, 2), J=d(1, 3), I=d(1, 1), H=d(1, d(K, J)), K=d(A, I), F=d(A, d(1, I)), E=d(K, B), C=d(F, E)]).
prover9_proof(luklem4, 0.255, d(d(d(A, d(B, d(1, 2))), d(2, d(d(2, 1), C))), d(A, d(d(2, D), d(2, d(B, D)))))-[E=d(2, 2), D=d(1, 3), C=d(1, 1), B=d(E, C), A=d(E, d(1, C))]).
prover9_proof('nic-id', 2.795, d(d(A, A), d(d(2, d(B, d(1, d(2, 3)))), d(d(d(C, D), E), d(d(F, G), d(1, C)))))-[F=d(2, 2), D=d(2, d(d(2, 1), H)), G=d(1, 2), I=d(1, 3), H=d(1, 1), B=d(F, H), J=d(F, d(1, H)), K=d(B, G), C=d(J, K), E=d(J, d(d(D, d(1, d(B, I))), d(2, I))), A=d(K, d(3, E))]).
prover9_proof('nic-isw1', 4.664, d(d(A, d(3, B)), d(C, d(D, C)))-[E=d(2, 2), D=d(2, F), G=d(2, d(d(2, 1), H)), I=d(1, 2), F=d(1, 3), H=d(1, 1), J=d(E, H), K=d(E, d(1, H)), A=d(J, I), L=d(K, A), B=d(K, d(d(G, d(1, d(J, F))), D)), C=d(d(d(E, I), d(1, L)), d(d(M, B), d(A, M))), M=d(L, G)]).
prover9_proof('nic-bijust', 1.73, d(d(A, A), d(d(B, A), d(d(C, d(D, d(B, d(2, E)))), d(B, F))))-[G=d(2, 2), B=d(2, H), H=d(1, 3), I=d(1, 1), J=d(G, I), D=d(G, d(1, I)), C=d(J, d(1, 2)), E=d(J, H), F=d(D, d(d(d(2, d(d(2, 1), I)), d(1, E)), B)), A=d(C, d(3, F))]).
prover9_proof(tbwlem3, 1.004, d(d(A, d(2, d(d(2, 1), B))), d(A, d(d(C, d(D, d(d(2, E), d(2, F)))), d(G, d(1, F)))))-[G=d(2, 2), E=d(1, 3), B=d(1, 1), H=d(G, B), D=d(G, d(1, B)), C=d(H, d(1, 2)), F=d(H, E), A=d(D, C)]).
prover9_proof(merco1lem7, 1.036, d(1, d(d(A, B), d(d(B, d(A, d(d(2, C), d(2, D)))), d(E, d(1, D)))))-[E=d(2, 2), C=d(1, 3), F=d(1, 1), G=d(E, F), A=d(E, d(1, F)), B=d(G, d(1, 2)), D=d(G, C)]).
prover9_proof(merco1lem8, 0.119, d(1, d(d(2, 2), d(2, 1)))-[]).
prover9_proof(merco1lem12, 4.145, d(d(d(d(A, B), d(1, C)), D), d(d(D, d(C, d(d(D, d(E, d(d(2, F), d(2, G)))), d(A, d(1, G))))), C))-[A=d(2, 2), B=d(1, 2), F=d(1, 3), H=d(1, 1), I=d(A, H), E=d(A, d(1, H)), D=d(I, B), G=d(I, F), C=d(E, D)]).
prover9_proof(merco1lem13, 4.11, d(d(d(d(A, B), d(1, C)), D), d(C, d(2, d(2, E))))-[A=d(2, 2), B=d(1, 2), E=d(1, 1), D=d(d(A, E), B), C=d(d(A, d(1, E)), D)]).
prover9_proof(merco1lem14, 3.347, d(d(d(A, B), d(1, C)), d(d(D, D), d(E, D)))-[A=d(2, 2), B=d(1, 2), F=d(1, 1), E=d(d(A, F), B), C=d(d(A, d(1, F)), E), D=d(C, d(2, d(d(2, 1), F)))]).
prover9_proof(merco1lem15, 0.14, d(2, d(1, 1))-[]).
prover9_proof(merco1lem16, 4.124, d(d(d(d(A, B), d(1, d(d(A, d(1, C)), D))), D), d(2, C))-[A=d(2, 2), B=d(1, 2), C=d(1, 1), D=d(d(A, C), B)]).
prover9_proof(merco1lem18, 2.808, d(d(2, A), d(d(B, A), d(1, d(d(B, d(1, C)), d(d(B, C), A)))))-[B=d(2, 2), A=d(1, 2), C=d(1, 1)]).
prover9_proof(mercolem1, 2.748, d(d(d(A, B), d(1, C)), d(C, d(C, d(2, d(2, D)))))-[A=d(2, 2), B=d(1, 2), D=d(1, 1), C=d(d(A, d(1, D)), d(d(A, D), B))]).
prover9_proof(mercolem2, 1.028, d(d(2, d(1, d(d(2, A), 1))), d(d(B, C), d(d(C, d(B, d(d(2, D), d(2, E)))), d(F, d(1, E)))))-[F=d(2, 2), D=d(1, 3), A=d(1, 1), G=d(F, A), B=d(F, d(1, A)), C=d(G, d(1, 2)), E=d(G, D)]).
prover9_proof(mercolem5, 2.749, d(d(d(A, B), d(1, d(d(A, d(1, C)), d(d(A, C), B)))), d(2, d(1, d(d(2, C), 1))))-[A=d(2, 2), B=d(1, 2), C=d(1, 1)]).
prover9_proof(mercolem6, 15.495, d(d(d(d(A, d(B, d(C, d(2, D)))), E), d(E, d(F, G))), d(d(A, G), d(F, d(E, D))))-[H=d(2, 2), C=d(2, I), E=d(2, J), K=d(2, d(d(2, 1), J)), I=d(1, 3), J=d(1, 1), L=d(H, J), B=d(H, d(1, J)), F=d(C, d(A, d(3, d(B, d(d(K, d(1, D)), C))))), A=d(L, d(1, 2)), D=d(L, I), G=d(d(B, A), K)]).
prover9_proof(anmp, 0.494, d(d(A, d(A, d(B, d(3, d(C, d(d(D, d(1, d(E, F))), A)))))), d(d(C, B), D))-[G=d(2, 2), A=d(2, F), D=d(2, d(d(2, 1), H)), F=d(1, 3), H=d(1, 1), E=d(G, H), C=d(G, d(1, H)), B=d(E, d(1, 2))]).
prover9_proof('rb-ax2', 2.82, d(d(d(d(A, B), d(1, C)), d(d(D, E), d(F, D))), d(G, d(F, d(3, E))))-[A=d(2, 2), G=d(2, H), I=d(2, d(d(2, 1), J)), B=d(1, 2), H=d(1, 3), J=d(1, 1), K=d(A, J), L=d(A, d(1, J)), F=d(K, B), C=d(L, F), E=d(L, d(d(I, d(1, d(K, H))), G)), D=d(C, I)]).
prover9_proof('rb-ax3', 0.235, d(d(d(2, d(d(2, 1), A)), d(1, d(d(d(2, 2), A), B))), d(2, B))-[B=d(1, 3), A=d(1, 1)]).
prover9_proof('rb-ax4', 0.657, d(d(d(d(A, B), C), d(A, d(d(C, d(1, D)), E))), d(B, d(A, d(E, d(2, D)))))-[F=d(2, 2), E=d(2, G), C=d(2, d(d(2, 1), H)), G=d(1, 3), H=d(1, 1), I=d(F, H), A=d(F, d(1, H)), B=d(I, d(1, 2)), D=d(I, G)]).
prover9_proof(rbsyl, 2.222, d(d(2, A), d(d(2, B), d(C, d(C, d(d(D, A), d(3, d(d(E, d(1, B)), d(d(d(2, d(d(2, 1), B)), d(1, d(D, F))), C))))))))-[E=d(2, 2), C=d(2, F), A=d(1, 2), F=d(1, 3), B=d(1, 1), D=d(E, B)]).
prover9_proof(rblem2, 2.793, d(d(d(d(A, B), d(1, C)), d(d(D, d(E, d(d(F, d(1, G)), d(2, H)))), d(I, D))), d(I, d(C, d(2, G))))-[A=d(2, 2), F=d(2, d(d(2, 1), J)), B=d(1, 2), H=d(1, 3), J=d(1, 1), K=d(A, J), E=d(A, d(1, J)), I=d(K, B), G=d(K, H), C=d(E, I), D=d(C, F)]).
prover9_proof(rblem3, 3.01, d(d(A, d(d(B, C), D)), d(A, d(d(B, d(3, d(E, d(F, d(3, C))))), D)))-[G=d(2, 2), H=d(2, d(d(2, 1), I)), J=d(1, 2), K=d(1, 3), I=d(1, 1), L=d(G, I), M=d(G, d(1, I)), E=d(H, d(1, d(L, K))), A=d(d(G, J), d(1, N)), F=d(L, J), N=d(M, F), C=d(M, d(E, d(2, K))), D=d(F, B), B=d(N, H)]).
prover9_proof(rblem6, 0.311, d(3, d(d(d(A, B), d(A, d(2, C))), d(D, d(3, d(E, d(d(B, d(1, C)), d(2, F)))))))-[G=d(2, 2), B=d(2, d(d(2, 1), H)), F=d(1, 3), H=d(1, 1), I=d(G, H), E=d(G, d(1, H)), D=d(I, d(1, 2)), C=d(I, F), A=d(E, D)]).
prover9_proof(rblem7, 0.241, d(3, d(d(A, d(B, d(1, 2))), d(3, d(A, d(d(d(2, d(d(2, 1), C)), d(1, d(B, D))), d(2, D))))))-[E=d(2, 2), D=d(1, 3), C=d(1, 1), B=d(E, C), A=d(E, d(1, C))]).
prover9_proof(mptnan, 2.715, d(d(d(A, B), d(C, d(d(B, d(1, d(D, E))), d(2, E)))), d(d(F, G), d(1, A)))-[F=d(2, 2), B=d(2, d(d(2, 1), H)), G=d(1, 2), E=d(1, 3), H=d(1, 1), D=d(F, H), C=d(F, d(1, H)), A=d(C, d(D, G))]).