Bob is red. Charlie is white. Fiona is quiet. If someone is red then they are nice. If someone is cold and white then they are nice. If someone is furry and not big then they are cold. If Bob is cold and Bob is quiet then Bob is red. If Bob is red and Bob is not big then Bob is not quiet. If Bob is quiet then Bob is nice.
Bob is red.
("Bob" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and white then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and not big then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "cold" "+"))
If Bob is cold and Bob is quiet then Bob is red.
((("Bob" "is" "cold" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "+"))
If Bob is red and Bob is not big then Bob is not quiet.
((("Bob" "is" "red" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "quiet" "-"))
If Bob is quiet then Bob is nice.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "nice" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Fiona is not quiet.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "quiet" "-")
triple3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is red.[(triple1)] Charlie is white.[(triple2)] Fiona is quiet.[(triple3)] @1: Bob is nice.[(((triple1) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1