Bob is smart. Dave is big. Fiona is big. Big, kind things are blue. Smart, big things are kind. Kind things are rough. If Dave is young then Dave is big. Kind, green things are blue. All smart, blue things are young.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Big, kind things are blue.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Smart, big things are kind.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Dave is young then Dave is big.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "big" "+"))
Kind, green things are blue.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All smart, blue things are young.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Dave is big.[(triple2)] Fiona is big.[(triple3)]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3