Bob is big. Bob is not blue. Bob is quiet. Charlie is not big. Charlie is blue. Charlie is kind. Charlie is round. Dave is not blue. Dave is nice. Dave is round. If someone is kind and not round then they are nice. If someone is rough and not round then they are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
If someone is kind and not round then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "nice" "+"))
If someone is rough and not round then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
Dave is nice.
True
1
proof
[(triple9)]
("Dave" "is" "nice" "+")
triple9
Dave is blue.
False
1
inv-proof
[(triple8)]
("Dave" "is" "blue" "+")
triple8
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is not blue.[(triple2)] Bob is quiet.[(triple3)] Charlie is blue.[(triple5)] Charlie is kind.[(triple6)] Charlie is not big.[(triple4)] Charlie is round.[(triple7)] Dave is nice.[(triple9)] Dave is not blue.[(triple8)] Dave is round.[(triple10)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is not big.
("Charlie" "is" "big" "-")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is not blue.
("Dave" "is" "blue" "-")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple10