Anne is red. Erin is green. Erin is quiet. Erin is red. Erin is rough. Erin is smart. Erin is young. Gary is green. Gary is nice. Harry is quiet. Harry is red. Harry is smart. If someone is red then they are smart. Smart people are young. If someone is smart and young then they are nice.
Anne is red.
("Anne" "is" "red" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is smart and young then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Erin is rough.
True
1
proof
[(triple5)]
("Erin" "is" "rough" "+")
triple5
Harry is not smart.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule1))]
("Harry" "is" "smart" "-")
triple12
((triple11) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is nice.
True
3
proof
[(((triple6 triple7) -> rule3) OR ((triple6 ((triple6) -> rule2)) -> rule3) OR ((((triple4) -> rule1) triple7) -> rule3) OR ((((triple4) -> rule1) ((triple6) -> rule2)) -> rule3) OR ((triple6 ((((triple4) -> rule1)) -> rule2)) -> rule3) OR ((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "nice" "+")
((triple6 triple7) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple6 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple4) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple6 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((triple12 ((triple12) -> rule2)) -> rule3) OR ((((triple11) -> rule1) ((triple12) -> rule2)) -> rule3) OR ((triple12 ((((triple11) -> rule1)) -> rule2)) -> rule3) OR ((((triple11) -> rule1) ((((triple11) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "nice" "-")
((triple12 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple11) -> (rule1 % int3)) ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((triple12 ((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple11) -> (rule1 % int3)) ((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Anne is nice.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not nice.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is red.[(triple1)] Erin is green.[(triple2)] Erin is quiet.[(triple3)] Erin is red.[(triple4)] Erin is rough.[(triple5)] Erin is smart.[(triple6 OR ((triple4) -> rule1))] Erin is young.[(triple7 OR ((triple6) -> rule2) OR ((((triple4) -> rule1)) -> rule2))] Gary is green.[(triple8)] Gary is nice.[(triple9)] Harry is quiet.[(triple10)] Harry is red.[(triple11)] Harry is smart.[(triple12 OR ((triple11) -> rule1))] @1: Anne is smart.[(((triple1) -> rule1))] Erin is nice.[(((triple6 triple7) -> rule3) OR ((triple6 ((triple6) -> rule2)) -> rule3) OR ((((triple4) -> rule1) triple7) -> rule3) OR ((((triple4) -> rule1) ((triple6) -> rule2)) -> rule3) OR ((triple6 ((((triple4) -> rule1)) -> rule2)) -> rule3) OR ((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule2)) -> rule3))] Harry is young.[(((triple12) -> rule2) OR ((((triple11) -> rule1)) -> rule2))] @2: Anne is young.[(((((triple1) -> rule1)) -> rule2))] Harry is nice.[(((triple12 ((triple12) -> rule2)) -> rule3) OR ((((triple11) -> rule1) ((triple12) -> rule2)) -> rule3) OR ((triple12 ((((triple11) -> rule1)) -> rule2)) -> rule3) OR ((((triple11) -> rule1) ((((triple11) -> rule1)) -> rule2)) -> rule3))] @3: Anne is nice.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple11) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple6 triple7) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple6 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple4) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple6 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((triple12) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple12 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple11) -> (rule1 % int3)) ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((triple12 ((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple11) -> (rule1 % int3)) ((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3