Anne is young. Dave is blue. Dave is green. Dave is kind. Dave is not quiet. Dave is white. Dave is young. Fiona is green. Fiona is kind. Fiona is nice. Fiona is quiet. Fiona is white. Fiona is young. Harry is green. Harry is not white. Blue, kind people are nice. If someone is young and kind then they are blue. Green people are blue. Nice, white people are green. Quiet, white people are kind. Blue, green people are kind.
Anne is young.
("Anne" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not white.
("Harry" "is" "white" "-")
Blue, kind people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and kind then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Nice, white people are green.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Quiet, white people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Blue, green people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Dave is not quiet.
True
1
proof
[(triple5)]
("Dave" "is" "quiet" "-")
triple5
Dave is not blue.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule3) OR ((triple7 triple4) -> rule2))]
("Dave" "is" "blue" "-")
triple2
((triple3) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple7 triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is blue.
True
2
proof
[(((triple14) -> rule3))]
("Harry" "is" "blue" "+")
((triple14) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple8) -> rule3) OR ((triple13 triple9) -> rule2) OR ((((triple10 triple12) -> rule4)) -> rule3) OR ((triple13 ((triple11 triple12) -> rule5)) -> rule2))]
("Fiona" "is" "blue" "-")
((triple8) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple13 triple9) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple10 triple12) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple13 ((triple11 triple12) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is kind.
True
4
proof
[(((((triple14) -> rule3) triple14) -> rule6))]
("Harry" "is" "kind" "+")
((((triple14) -> (rule3 % int2)) triple14) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple14) -> rule3) triple14) -> rule6))]
("Harry" "is" "kind" "-")
((((triple14) -> (rule3 % int2)) triple14) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
True
7
proof
[(((((triple14) -> rule3) ((((triple14) -> rule3) triple14) -> rule6)) -> rule1))]
("Harry" "is" "nice" "+")
((((triple14) -> (rule3 % int3)) ((((triple14) -> (rule3 % int3)) triple14) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not nice.
False
7
inv-proof
[(((((triple14) -> rule3) ((((triple14) -> rule3) triple14) -> rule6)) -> rule1))]
("Harry" "is" "nice" "-")
((((triple14) -> (rule3 % int3)) ((((triple14) -> (rule3 % int3)) triple14) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is nice.
Unknown
rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule4 <- FAIL)]]
("Anne" "is" "nice" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is young.[(triple1)] Dave is blue.[(triple2 OR ((triple3) -> rule3) OR ((triple7 triple4) -> rule2))] Dave is green.[(triple3 OR ((((triple2 triple4) -> rule1) triple6) -> rule4) OR ((((((triple7 triple4) -> rule2) triple4) -> rule1) triple6) -> rule4))] Dave is kind.[(triple4 OR ((triple2 triple3) -> rule6) OR ((((triple3) -> rule3) triple3) -> rule6))] Dave is not quiet.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7)] Fiona is green.[(triple8 OR ((triple10 triple12) -> rule4) OR ((((((triple13 triple9) -> rule2) triple9) -> rule1) triple12) -> rule4) OR ((((((triple13 triple9) -> rule2) ((triple11 triple12) -> rule5)) -> rule1) triple12) -> rule4) OR ((((((triple13 ((triple11 triple12) -> rule5)) -> rule2) triple9) -> rule1) triple12) -> rule4) OR ((((((triple13 ((triple11 triple12) -> rule5)) -> rule2) ((triple11 triple12) -> rule5)) -> rule1) triple12) -> rule4))] Fiona is kind.[(triple9 OR ((triple11 triple12) -> rule5) OR ((((triple8) -> rule3) triple8) -> rule6) OR ((((triple8) -> rule3) ((triple10 triple12) -> rule4)) -> rule6) OR ((((((triple10 triple12) -> rule4)) -> rule3) triple8) -> rule6) OR ((((((triple10 triple12) -> rule4)) -> rule3) ((triple10 triple12) -> rule4)) -> rule6))] Fiona is nice.[(triple10 OR ((((triple8) -> rule3) triple9) -> rule1) OR ((((triple13 triple9) -> rule2) triple9) -> rule1) OR ((((triple8) -> rule3) ((triple11 triple12) -> rule5)) -> rule1) OR ((((triple13 triple9) -> rule2) ((triple11 triple12) -> rule5)) -> rule1) OR ((((triple13 ((triple11 triple12) -> rule5)) -> rule2) triple9) -> rule1) OR ((((triple8) -> rule3) ((((triple8) -> rule3) triple8) -> rule6)) -> rule1) OR ((((triple13 triple9) -> rule2) ((((triple8) -> rule3) triple8) -> rule6)) -> rule1) OR ((((triple13 ((triple11 triple12) -> rule5)) -> rule2) ((triple11 triple12) -> rule5)) -> rule1) OR ((((triple13 ((triple11 triple12) -> rule5)) -> rule2) ((((triple8) -> rule3) triple8) -> rule6)) -> rule1))] Fiona is quiet.[(triple11)] Fiona is white.[(triple12)] Fiona is young.[(triple13)] Harry is green.[(triple14)] Harry is not white.[(triple15)] @1: Dave is nice.[(((triple2 triple4) -> rule1) OR ((triple2 ((triple2 triple3) -> rule6)) -> rule1) OR ((((triple3) -> rule3) triple4) -> rule1) OR ((((triple7 triple4) -> rule2) triple4) -> rule1) OR ((((triple3) -> rule3) ((triple2 triple3) -> rule6)) -> rule1) OR ((((triple7 triple4) -> rule2) ((triple2 triple3) -> rule6)) -> rule1) OR ((triple2 ((((triple3) -> rule3) triple3) -> rule6)) -> rule1) OR ((((triple3) -> rule3) ((((triple3) -> rule3) triple3) -> rule6)) -> rule1) OR ((((triple7 triple4) -> rule2) ((((triple3) -> rule3) triple3) -> rule6)) -> rule1))] Fiona is blue.[(((triple8) -> rule3) OR ((triple13 triple9) -> rule2) OR ((((triple10 triple12) -> rule4)) -> rule3) OR ((triple13 ((triple11 triple12) -> rule5)) -> rule2))] Harry is blue.[(((triple14) -> rule3))] @2: Harry is kind.[(((((triple14) -> rule3) triple14) -> rule6))] @3: Harry is nice.[(((((triple14) -> rule3) ((((triple14) -> rule3) triple14) -> rule6)) -> rule1))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple3) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple7 triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
((((triple2 triple4) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple7 triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple2 triple3) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
((triple10 triple12) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((((triple13 triple9) -> (rule2 % int3)) triple9) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple13 triple9) -> (rule2 % int4)) ((triple11 triple12) -> (rule5 % int3))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((triple13 ((triple11 triple12) -> (rule5 % int4))) -> (rule2 % int3)) triple9) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((((triple13 ((triple11 triple12) -> (rule5 % int4))) -> (rule2 % int3)) ((triple11 triple12) -> (rule5 % int4))) -> (rule1 % int2)) triple12) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
((triple11 triple12) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple8) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple8) -> (rule3 % int3)) ((triple10 triple12) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple10 triple12) -> (rule4 % int3))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((((triple10 triple12) -> (rule4 % int3))) -> (rule3 % int2)) ((triple10 triple12) -> (rule4 % int3))) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((((triple8) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple13 triple9) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple8) -> (rule3 % int3)) ((triple11 triple12) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple13 triple9) -> (rule2 % int3)) ((triple11 triple12) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple13 ((triple11 triple12) -> (rule5 % int3))) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3)) triple8) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple13 triple9) -> (rule2 % int3)) ((((triple8) -> (rule3 % int3)) triple8) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((triple13 ((triple11 triple12) -> (rule5 % int3))) -> (rule2 % int2)) ((triple11 triple12) -> (rule5 % int3))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple13 ((triple11 triple12) -> (rule5 % int3))) -> (rule2 % int2)) ((((triple8) -> (rule3 % int2)) triple8) -> (rule6 % int3))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Fiona is young.
("Fiona" "is" "young" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is not white.
("Harry" "is" "white" "-")
triple15
Dave is nice.
("Dave" "is" "nice" "+")
((triple2 triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple2 ((triple2 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple7 triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple2 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple7 triple4) -> (rule2 % int3)) ((triple2 triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((triple2 ((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple7 triple4) -> (rule2 % int3)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple8) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple13 triple9) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((((triple10 triple12) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple13 ((triple11 triple12) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple14) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple14) -> (rule3 % int2)) triple14) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple14) -> (rule3 % int3)) ((((triple14) -> (rule3 % int3)) triple14) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3