The bear visits the dog. The dog is round. The mouse is young. If the dog visits the mouse and the dog does not chase the bear then the dog is round. If something is cold and it sees the dog then the dog is round. If something chases the mouse then the mouse is big.
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is round.
("dog" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
If the dog visits the mouse and the dog does not chase the bear then the dog is round.
((("dog" "visits" "mouse" "+") ("dog" "chases" "bear" "~")) -> ("dog" "is" "round" "+"))
If something is cold and it sees the dog then the dog is round.
((("something" "is" "cold" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "round" "+"))
If something chases the mouse then the mouse is big.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "big" "+"))
The dog is round.
True
1
proof
[(triple2)]
("dog" "is" "round" "+")
triple2
The dog is not round.
False
1
inv-proof
[(triple2)]
("dog" "is" "round" "-")
triple2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The bear visits the dog.[(triple1)] The dog is round.[(triple2)] The mouse is young.[(triple3)]
The bear visits the dog.
("bear" "visits" "dog" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3