Bob is not round. Bob is not smart. Dave is big. Dave is not quiet. Dave is red. Dave is round. Dave is smart. Gary is not big. Gary is round. Harry is quiet. Harry is round. Harry is not smart. If Gary is red then Gary is not young. If someone is smart and not round then they are big. If Bob is not young then Bob is quiet.
Bob is not round.
("Bob" "is" "round" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is round.
("Gary" "is" "round" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Gary is red then Gary is not young.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "young" "-"))
If someone is smart and not round then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
If Bob is not young then Bob is quiet.
((("Bob" "is" "young" "~")) -> ("Bob" "is" "quiet" "+"))
Gary is round.
True
1
proof
[(triple9)]
("Gary" "is" "round" "+")
triple9
Harry is smart.
False
1
inv-proof
[(triple12)]
("Harry" "is" "smart" "+")
triple12
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is not round.[(triple1)] Bob is not smart.[(triple2)] Dave is big.[(triple3)] Dave is not quiet.[(triple4)] Dave is red.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7)] Gary is not big.[(triple8)] Gary is round.[(triple9)] Harry is not smart.[(triple12)] Harry is quiet.[(triple10)] Harry is round.[(triple11)]
Bob is not round.
("Bob" "is" "round" "-")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Gary is not big.
("Gary" "is" "big" "-")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Harry is not smart.
("Harry" "is" "smart" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11