Anne is furry. Bob is furry. Bob is green. Bob is round. Dave is round. Dave is white. Harry is quiet. If someone is round then they are red. Green, red people are white. Furry people are red. White, red people are green. All quiet, smart people are white. All white, green people are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Green, red people are white.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
White, red people are green.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All quiet, smart people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All white, green people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Dave is white.
True
1
proof
[(triple6)]
("Dave" "is" "white" "+")
triple6
Dave is not round.
False
1
inv-proof
[(triple5)]
("Dave" "is" "round" "-")
triple5
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is furry.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is round.[(triple4)] Dave is round.[(triple5)] Dave is white.[(triple6)] Harry is quiet.[(triple7)] @1: Anne is red.[(((triple1) -> rule3))] Bob is red.[(((triple2) -> rule3) OR ((triple4) -> rule1))] Dave is red.[(((triple5) -> rule1))] @2: Bob is white.[(((triple3 ((triple2) -> rule3)) -> rule2) OR ((triple3 ((triple4) -> rule1)) -> rule2))] Dave is green.[(((triple6 ((triple5) -> rule1)) -> rule4))] @3: Bob is quiet.[(((((triple3 ((triple2) -> rule3)) -> rule2) triple3) -> rule6) OR ((((triple3 ((triple4) -> rule1)) -> rule2) triple3) -> rule6))] Dave is quiet.[(((triple6 ((triple6 ((triple5) -> rule1)) -> rule4)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple4) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple5) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple3 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple6 ((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple3 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple3 ((triple4) -> (rule1 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6 ((triple6 ((triple5) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3