Bob is not furry. Bob is red. Bob is smart. Bob is young. Dave is furry. Dave is green. Dave is smart. All green things are furry. Kind, red things are not smart.
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Kind, red things are not smart.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "-"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple6)]
("Dave" "is" "green" "-")
triple6
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Bob is not furry.[(triple1)] Bob is red.[(triple2)] Bob is smart.[(triple3)] Bob is young.[(triple4)] Dave is furry.[(triple5 OR ((triple6) -> rule1))] Dave is green.[(triple6)] Dave is smart.[(triple7)]
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
((triple6) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7