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