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