/******************************************************************/
/* ACM ICPC 2012-2013                                             */
/* Northeastern European Regional Contest                         */
/* St Petersburg - Barnaul - Tashkent - Tbilisi, December 2, 2012 */
/******************************************************************/
/* Problem D. Disjoint Regular Expressions                        */
/*                                                                */
/* Original idea         Roman Elizarov                           */
/* Problem statement     Andrey Stankevich                        */
/* Test set              Andrey Stankevich                        */
/******************************************************************/
/* Checker                                                        */
/*                                                                */
/* Author                Andrey Stankevich                        */
/******************************************************************/

import ru.ifmo.testlib.Checker;
import ru.ifmo.testlib.InStream;
import ru.ifmo.testlib.Outcome;

import java.util.Arrays;
import java.util.HashSet;
import java.util.Set;

public class Check implements Checker {
    public static final String CORRECT = "Correct";
    public static final String WRONG = "Wrong";

    private static class Ans {
        String guess;
        String match;

        Ans(InStream in) {
            guess = in.nextLine();
            if (guess.equals(CORRECT)) {
                // no match to read
            } else if (guess.equals(WRONG)) {
                match = in.nextLine();
            } else
                throw new Outcome(Outcome.Type.PE, String.format("Expected '%s' or '%s' but found '%s'", CORRECT, WRONG, guess));
            if (!in.seekEoF())
                throw new Outcome(Outcome.Type.PE, "Extra data in output file");
        }
    }

	public Outcome test(InStream inf, InStream ouf, InStream ans) {
        Ans ja = new Ans(ans);
        Ans pa = new Ans(ouf);

        if (pa.guess.equals(CORRECT)) {
            if (ja.guess.equals(CORRECT)) {
                return new Outcome(Outcome.Type.OK, "No solution");
            } else {
                return new Outcome(Outcome.Type.WA, "Solution exists but not found");
            }
        } 
        
        String ps = pa.match;
        String r1 = inf.nextLine();
        String r2 = inf.nextLine();

        if (ps.length() == 0) {
            return new Outcome(Outcome.Type.WA, "Empty answer");
        }
        if (ps.length() > r1.length() * r2.length()) {
            return new Outcome(Outcome.Type.WA, "Definitely too long");
        }
        for (int i = 0; i < ps.length(); i++) {
            if (ps.charAt(i) < 'a' || ps.charAt(i) > 'z') {
                return new Outcome(Outcome.Type.WA, "Answer must contain lowercase letters only");
            }
        }

        Auto a1 = convert(r1);
        Auto a2 = convert(r2);
        if (!a1.accepts(ps)) {
            return new Outcome(Outcome.Type.WA, "Answer doesn't match first expression");
        }
        if (!a2.accepts(ps)) {
            return new Outcome(Outcome.Type.WA, "Answer doesn't match second expression");
        }
        if (ja.guess.equals(CORRECT)) {
            return new Outcome(Outcome.Type.FAIL, "Jury thought there was no such expression");
        }
        
        String js = ja.match;
        if (js.length() < ps.length()) {
            return new Outcome(Outcome.Type.WA, "Jury length " + js.length() + ", user length: " + ps.length());
        }
        if (js.length() > ps.length()) {
            return new Outcome(Outcome.Type.FAIL, "Jury length " + js.length() + ", user length: " + ps.length());
        }

        return new Outcome(Outcome.Type.OK, "Answer length " + js.length());
	}
    
    Auto convert(String re) {
        str = re + "$";
        p = 0;
        nextToken();
        Node tree = expr();
        assert token == Token.END; 
        
        return buildAuto(tree);
    }
    
    Auto buildAuto(Node t) {
        switch (t.op) {
            case TERM: {
                Auto res = new Auto(2);
                res.go[0][t.c - 'a'] = 1;
                return res;
            }
            case CONCAT: {
                Auto ra = buildAuto(t.a);
                Auto rb = buildAuto(t.b);
                Auto res = new Auto(ra.n + rb.n);
                for (int i = 0; i < ra.n; i++) {
                    for (int j = 0; j < 26; j++) {
                        res.go[i][j] = ra.go[i][j];
                    }
                    res.eps[i] = ra.eps[i];
                }
                for (int i = 0; i < rb.n; i++) {
                    for (int j = 0; j < 26; j++) {
                        int z = rb.go[i][j];
                        if (z != -1) {
                            res.go[ra.n + i][j] = z + ra.n;
                        }
                    }
                    for (int z : rb.eps[i]) {
                        res.eps[ra.n + i].add(z + ra.n);
                    }
                }
                res.eps[ra.n - 1].add(ra.n);
                return res;
            }
            case UNION: {
                Auto ra = buildAuto(t.a);
                Auto rb = buildAuto(t.b);
                Auto res = new Auto(ra.n + rb.n + 2);
                for (int i = 0; i < ra.n; i++) {
                    for (int j = 0; j < 26; j++) {
                        int z = ra.go[i][j];
                        if (z != -1) {
                            res.go[i + 1][j] = z + 1;
                        }
                    }
                    for (int z : ra.eps[i]) {
                        res.eps[i + 1].add(z + 1);
                    }
                }
                for (int i = 0; i < rb.n; i++) {
                    for (int j = 0; j < 26; j++) {
                        int z = rb.go[i][j];
                        if (z != -1) {
                            res.go[ra.n + 1 + i][j] = z + 1 + ra.n;
                        }
                    }
                    for (int z : rb.eps[i]) {
                        res.eps[i + ra.n + 1].add(z + ra.n + 1);
                    }
                }
                res.eps[0].add(1);
                res.eps[0].add(ra.n + 1);
                res.eps[ra.n].add(ra.n + rb.n + 1);
                res.eps[ra.n + rb.n].add(ra.n + rb.n + 1);
                return res;
            }
            case KLEENE: {
                Auto ra = buildAuto(t.a);
                Auto res = new Auto(ra.n + 2);
                for (int i = 0; i < ra.n; i++) {
                    for (int j = 0; j < 26; j++) {
                        int z = ra.go[i][j];
                        if (z != -1) {
                            res.go[i + 1][j] = z + 1;
                        }
                    }
                    for (int z : ra.eps[i]) {
                        res.eps[i + 1].add(z + 1);
                    }
                }
                res.eps[0].add(1);
                res.eps[0].add(ra.n + 1);
                res.eps[ra.n].add(ra.n + 1);
                res.eps[ra.n + 1].add(0);
                return res;
            }
        }
        return null;
    }
    
    class Auto {
        int n;
        int go[][];
        Set<Integer> eps[];

        Auto(int n) {
            this.n = n;
            go = new int[n][26];
            for (int[] z : go) {
                Arrays.fill(z, -1);
            }
            eps = new Set[n];
            for (int i = 0; i < n; i++) {
                eps[i] = new HashSet<Integer>();
            }
        }
        
        boolean accepts(String s) {
            boolean[] cur = new boolean[n];
            cur[0] = true;
            fill(cur, eps, 0);
            boolean[] next = new boolean[n];
            
            for (int i = 0; i < s.length(); i++) {
                Arrays.fill(next, false);
                int c = s.charAt(i) - 'a';
                for (int j = 0; j < n; j++) {
                    if (cur[j] && go[j][c] != -1) {
                        next[go[j][c]] = true;
                        fill(next, eps, go[j][c]);
                    }
                }
                
                boolean[] tmp = next;
                next = cur;
                cur = tmp;
            }
            
            return cur[n - 1];
        }
        
        void fill(boolean[] can, Set<Integer>[] eps, int pos) {
            for (int y : eps[pos]) {
                if (!can[y]) {
                    can[y] = true;
                    fill(can, eps, y);
                }
            }
        }
    }

    Node expr() {
        Node t = term();
        while (token == Token.OR) {
            nextToken();
            Node r = term();
            t = new Node(Operation.UNION, t, r);
        }
        return t;
    }
    
    Node term() {
        Node t = star();
        while (token == Token.C || token == Token.LP) {
            Node r = star();
            t = new Node(Operation.CONCAT, t, r);
        }
        return t;
    }
    
    Node star() {
        Node r;
        if (token == Token.C) {
            r = new Node(curc);
            nextToken();
        } else if (token == Token.LP) {
            nextToken();
            r = expr();
            assert token == Token.RP;
            nextToken();
        } else {
            throw new AssertionError();
        }
        if (token == Token.STAR) {
            r = new Node(Operation.KLEENE, r, null);
            while (token == Token.STAR) {
                nextToken();
            }
        }
        return r;
    }
    
    Token token;
    String str;
    char curc;
    int p;
    
    void nextToken() {
        switch (str.charAt(p)) {
            case '(':
                token = Token.LP;
                p++;
                break;
            case ')':
                token = Token.RP;
                p++;
                break;
            case '|':
                token = Token.OR;
                p++;
                break;
            case '*':
                token = Token.STAR;
                p++;
                break;
            case '$':
                token = Token.END;
                p++;
                break;
            default:
                token = Token.C;
                curc = str.charAt(p);
                p++;
        }
    }
    
    enum Token {
        C, LP, RP, STAR, OR, END
    }

    enum Operation {
        TERM, UNION, CONCAT, KLEENE
    }
    
    class Node {
        Operation op;
        Node a, b;
        char c;

        Node(Operation op, Node a, Node b) {
            this.op = op;
            this.a = a;
            this.b = b;
        }

        Node(char c) {
            op = Operation.TERM;
            this.c = c;
        }
    }
    
}

