Anne is blue. Anne is cold. Anne is nice. Anne is rough. Anne is white. Bob is kind. Bob is nice. Bob is round. Bob is white. Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is rough. Gary is white. If someone is blue then they are round. All blue, kind people are white. Cold, blue people are nice. Cold, round people are rough. If someone is kind and nice then they are white. If someone is rough and cold then they are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All blue, kind people are white.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Cold, blue people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Cold, round people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and nice then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and cold then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple9 OR ((triple6 triple7) -> rule5))]
("Bob" "is" "white" "+")
triple9
((triple6 triple7) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple15 OR ((triple10 triple12) -> rule2) OR ((triple12 triple13) -> rule5) OR ((triple12 ((triple11 triple10) -> rule3)) -> rule5) OR ((((triple14 triple11) -> rule6) triple12) -> rule2) OR ((triple12 ((triple11 ((triple14 triple11) -> rule6)) -> rule3)) -> rule5))]
("Gary" "is" "white" "-")
triple15
((triple10 triple12) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple12 triple13) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple12 ((triple11 triple10) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple14 triple11) -> (rule6 % int2)) triple12) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple12 ((triple11 ((triple14 triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is blue.[(triple1 OR ((triple4 triple2) -> rule6))] Anne is cold.[(triple2)] Anne is nice.[(triple3 OR ((triple2 triple1) -> rule3) OR ((triple2 ((triple4 triple2) -> rule6)) -> rule3))] Anne is rough.[(triple4 OR ((triple2 ((triple1) -> rule1)) -> rule4))] Anne is white.[(triple5)] Bob is kind.[(triple6)] Bob is nice.[(triple7)] Bob is round.[(triple8)] Bob is white.[(triple9 OR ((triple6 triple7) -> rule5))] Gary is blue.[(triple10 OR ((triple14 triple11) -> rule6))] Gary is cold.[(triple11)] Gary is kind.[(triple12)] Gary is nice.[(triple13 OR ((triple11 triple10) -> rule3) OR ((triple11 ((triple14 triple11) -> rule6)) -> rule3))] Gary is rough.[(triple14 OR ((triple11 ((triple10) -> rule1)) -> rule4))] Gary is white.[(triple15 OR ((triple10 triple12) -> rule2) OR ((triple12 triple13) -> rule5) OR ((triple12 ((triple11 triple10) -> rule3)) -> rule5) OR ((((triple14 triple11) -> rule6) triple12) -> rule2) OR ((triple12 ((triple11 ((triple14 triple11) -> rule6)) -> rule3)) -> rule5))] @1: Anne is round.[(((triple1) -> rule1) OR ((((triple4 triple2) -> rule6)) -> rule1))] Gary is round.[(((triple10) -> rule1) OR ((((triple14 triple11) -> rule6)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple2 triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple2 ((triple4 triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple2 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
triple8
Bob is white.
("Bob" "is" "white" "+")
triple9
((triple6 triple7) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple10
((triple14 triple11) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
((triple11 triple10) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple11 ((triple14 triple11) -> (rule6 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple14
((triple11 ((triple10) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple15
((triple10 triple12) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple12 triple13) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple12 ((triple11 triple10) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple14 triple11) -> (rule6 % int2)) triple12) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple12 ((triple11 ((triple14 triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple10) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple14 triple11) -> (rule6 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2