Bob is furry. Bob is green. Bob is kind. Bob is quiet. Bob is red. Bob is smart. Harry is furry. Harry is quiet. Harry is red. Harry is white. If something is white then it is red. All kind, green things are red. If Bob is furry then Bob is smart.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All kind, green things are red.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Bob is furry then Bob is smart.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "smart" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple3 triple2) -> rule2))] Bob is smart.[(triple6 OR ((triple1) -> rule3))] Harry is furry.[(triple7)] Harry is quiet.[(triple8)] Harry is red.[(triple9 OR ((triple10) -> rule1))] Harry is white.[(triple10)]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple3 triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple10