Bob is rough. Charlie is furry. Fiona is furry. Gary is kind. If someone is nice then they are rough. If someone is round then they are quiet. If Bob is rough then Bob is furry. All round people are quiet. All quiet, kind people are nice. If someone is kind and rough then they are green.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is rough then Bob is furry.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "furry" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, kind people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and rough then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is rough.[(triple1)] Charlie is furry.[(triple2)] Fiona is furry.[(triple3)] Gary is kind.[(triple4)] @1: Bob is furry.[(((triple1) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1