The bear is not rough. The bear needs the dog. The bear visits the dog. The bear visits the mouse. The dog needs the bear. The dog visits the bear. The mouse likes the bear. If something needs the mouse then it does not need the dog. If something likes the bear then it is kind. If something visits the dog and the dog is not kind then it likes the mouse.
The bear is not rough.
("bear" "is" "rough" "-")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If something needs the mouse then it does not need the dog.
((("something" "needs" "mouse" "+")) -> ("something" "needs" "dog" "-"))
If something likes the bear then it is kind.
((("something" "likes" "bear" "+")) -> ("something" "is" "kind" "+"))
If something visits the dog and the dog is not kind then it likes the mouse.
((("something" "visits" "dog" "+") ("dog" "is" "kind" "~")) -> ("something" "likes" "mouse" "+"))
The dog needs the bear.
True
1
proof
[(triple5)]
("dog" "needs" "bear" "+")
triple5
The dog does not need the bear.
False
1
inv-proof
[(triple5)]
("dog" "needs" "bear" "-")
triple5
The mouse is kind.
True
2
proof
[(((triple7) -> rule2))]
("mouse" "is" "kind" "+")
((triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple7) -> rule2))]
("mouse" "is" "kind" "-")
((triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The dog is kind.
Unknown
rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "kind" "+")
The mouse does not visit the bear.
Unknown
inv-random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The bear is not rough.[(triple1)] The bear needs the dog.[(triple2)] The bear visits the dog.[(triple3)] The bear visits the mouse.[(triple4)] The dog needs the bear.[(triple5)] The dog visits the bear.[(triple6)] The mouse likes the bear.[(triple7)] @1: The mouse is kind.[(((triple7) -> rule2))]
The bear is not rough.
("bear" "is" "rough" "-")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple4
The dog needs the bear.
("dog" "needs" "bear" "+")
triple5
The dog visits the bear.
("dog" "visits" "bear" "+")
triple6
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
((triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1