Anne is cold. Bob is smart. Charlie is big. If Charlie is rough and Charlie is nice then Charlie is smart. If something is big then it is blue. If Anne is green and Anne is big then Anne is cold. If something is blue then it is big. If Bob is nice and Bob is smart then Bob is big. Big, rough things are nice.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
If Charlie is rough and Charlie is nice then Charlie is smart.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "smart" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If Anne is green and Anne is big then Anne is cold.
((("Anne" "is" "green" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "cold" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If Bob is nice and Bob is smart then Bob is big.
((("Bob" "is" "nice" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "big" "+"))
Big, rough things are nice.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple3)]
("Charlie" "is" "big" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Bob is smart.[(triple2)] Charlie is big.[(triple3)] @1: Charlie is blue.[(((triple3) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1