Bob is big. Bob is furry. Bob is quiet. Dave is quiet. Gary is big. Gary is blue. Gary is furry. Gary is kind. Gary is rough. Harry is big. Harry is furry. Harry is red. If Harry is blue and Harry is furry then Harry is kind. If something is red then it is quiet. All blue things are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
If Harry is blue and Harry is furry then Harry is kind.
((("Harry" "is" "blue" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "kind" "+"))
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Bob is quiet.
True
1
proof
[(triple3)]
("Bob" "is" "quiet" "+")
triple3
Harry is not red.
False
1
inv-proof
[(triple12)]
("Harry" "is" "red" "-")
triple12
Harry is quiet.
True
2
proof
[(((triple12) -> rule2))]
("Harry" "is" "quiet" "+")
((triple12) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple12) -> rule2))]
("Harry" "is" "quiet" "-")
((triple12) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is quiet.[(triple3)] Dave is quiet.[(triple4)] Gary is big.[(triple5)] Gary is blue.[(triple6)] Gary is furry.[(triple7)] Gary is kind.[(triple8)] Gary is rough.[(triple9)] Harry is big.[(triple10)] Harry is furry.[(triple11)] Harry is red.[(triple12)] @1: Gary is quiet.[(((triple6) -> rule3))] Harry is quiet.[(((triple12) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple12) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1