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