Bob is smart. Charlie is rough. Dave is kind. Fiona is kind. If something is kind and cold then it is furry. If something is kind and rough then it is cold. If Bob is kind and Bob is smart then Bob is big. All smart, kind things are red. Furry things are smart. All furry things are smart.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If something is kind and cold then it is furry.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is kind and rough then it is cold.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Bob is kind and Bob is smart then Bob is big.
((("Bob" "is" "kind" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "big" "+"))
All smart, kind things are red.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is smart.[(triple1)] Charlie is rough.[(triple2)] Dave is kind.[(triple3)] Fiona is kind.[(triple4)]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4