The cat needs the mouse. The lion chases the cat. The lion does not need the cat. The lion needs the mouse. The mouse chases the cat. The mouse is big. The mouse does not see the lion. If the cat needs the mouse then the mouse does not need the cat.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion does not need the cat.
("lion" "needs" "cat" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
If the cat needs the mouse then the mouse does not need the cat.
((("cat" "needs" "mouse" "+")) -> ("mouse" "needs" "cat" "-"))
The lion chases the cat.
True
1
proof
[(triple2)]
("lion" "chases" "cat" "+")
triple2
The lion does not chase the cat.
False
1
inv-proof
[(triple2)]
("lion" "chases" "cat" "-")
triple2
The mouse does not need the cat.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "needs" "cat" "-")
((triple1) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse needs the cat.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "needs" "cat" "+")
((triple1) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat needs the mouse.[(triple1)] The lion chases the cat.[(triple2)] The lion does not need the cat.[(triple3)] The lion needs the mouse.[(triple4)] The mouse chases the cat.[(triple5)] The mouse does not see the lion.[(triple7)] The mouse is big.[(triple6)] @1: The mouse does not need the cat.[(((triple1) -> rule1))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The lion chases the cat.
("lion" "chases" "cat" "+")
triple2
The lion does not need the cat.
("lion" "needs" "cat" "-")
triple3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple5
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
((triple1) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1