Anne is big. Anne is cold. Anne is rough. Anne is smart. Charlie is big. Charlie is cold. Charlie is not red. Charlie is rough. Charlie is smart. Dave is big. Dave is cold. Dave is red. If Anne is not blue then Anne is big. If something is big and not rough then it is cold. All blue, rough things are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
If Anne is not blue then Anne is big.
((("Anne" "is" "blue" "~")) -> ("Anne" "is" "big" "+"))
If something is big and not rough then it is cold.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "cold" "+"))
All blue, rough things are smart.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Anne is rough.
True
1
proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Charlie is not rough.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "rough" "-")
triple8
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is rough.[(triple3)] Anne is smart.[(triple4)] Charlie is big.[(triple5)] Charlie is cold.[(triple6)] Charlie is not red.[(triple7)] Charlie is rough.[(triple8)] Charlie is smart.[(triple9)] Dave is big.[(triple10)] Dave is cold.[(triple11)] Dave is red.[(triple12)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is not red.
("Charlie" "is" "red" "-")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple12