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