Anne is furry. Anne is kind. Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is red. Dave is blue. Dave is furry. Dave is red. Furry people are kind. If Bob is furry then Bob is nice. All cold people are red. All cold, red people are furry. All red, nice people are cold. If someone is nice then they are blue.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Bob is furry then Bob is nice.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
All cold, red people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Dave is red.
True
1
proof
[(triple10)]
("Dave" "is" "red" "+")
triple10
Dave is not furry.
False
1
inv-proof
[(triple9)]
("Dave" "is" "furry" "-")
triple9
Bob is nice.
True
2
proof
[(((triple4) -> rule2) OR ((((triple3 triple7) -> rule4)) -> rule2) OR ((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule2))]
("Bob" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple3 triple7) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not nice.
False
2
inv-proof
[(((triple4) -> rule2) OR ((((triple3 triple7) -> rule4)) -> rule2) OR ((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule2))]
("Bob" "is" "nice" "-")
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple3 triple7) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2 OR ((triple1) -> rule1))] Bob is cold.[(triple3 OR ((triple7 ((triple4) -> rule2)) -> rule5))] Bob is furry.[(triple4 OR ((triple3 triple7) -> rule4) OR ((triple3 ((triple3) -> rule3)) -> rule4))] Bob is green.[(triple5)] Bob is kind.[(triple6 OR ((triple4) -> rule1) OR ((((triple3 triple7) -> rule4)) -> rule1) OR ((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule1))] Bob is red.[(triple7 OR ((triple3) -> rule3))] Dave is blue.[(triple8)] Dave is furry.[(triple9)] Dave is red.[(triple10)] @1: Bob is nice.[(((triple4) -> rule2) OR ((((triple3 triple7) -> rule4)) -> rule2) OR ((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule2))] Dave is kind.[(((triple9) -> rule1))] @2: Bob is blue.[(((((triple4) -> rule2)) -> rule6) OR ((((((triple3 triple7) -> rule4)) -> rule2)) -> rule6) OR ((((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule2)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple7 ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple4
((triple3 triple7) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
((triple4) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3 triple7) -> (rule4 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple7
((triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple3 triple7) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple3 triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple3 ((triple3) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4