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