Bob is furry. Bob is red. Bob is rough. Dave is furry. Dave is red. Erin is not blue. Erin is not furry. Erin is white. Harry is blue. Harry is furry. Harry is quiet. Harry is red. Harry is rough. Harry is white. Harry is young. All rough, white things are quiet. If Erin is rough then Erin is red. Red things are white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is white.
("Erin" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough, white things are quiet.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If Erin is rough then Erin is red.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "red" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Harry is young.
True
1
proof
[(triple15)]
("Harry" "is" "young" "+")
triple15
Harry is not blue.
False
1
inv-proof
[(triple9)]
("Harry" "is" "blue" "-")
triple9
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is furry.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3)] Dave is furry.[(triple4)] Dave is red.[(triple5)] Erin is not blue.[(triple6)] Erin is not furry.[(triple7)] Erin is white.[(triple8)] Harry is blue.[(triple9)] Harry is furry.[(triple10)] Harry is quiet.[(triple11 OR ((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule3)) -> rule1))] Harry is red.[(triple12)] Harry is rough.[(triple13)] Harry is white.[(triple14 OR ((triple12) -> rule3))] Harry is young.[(triple15)] @1: Bob is white.[(((triple2) -> rule3))] Dave is white.[(((triple5) -> rule3))] @2: Bob is quiet.[(((triple3 ((triple2) -> rule3)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Erin is not blue.
("Erin" "is" "blue" "-")
triple6
Erin is not furry.
("Erin" "is" "furry" "-")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple13 triple14) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple13 ((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
((triple12) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple5) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2