The cat does not chase the mouse. The cat is nice. The cat sees the cow. The cat sees the lion. The cat sees the mouse. The cow is nice. The lion does not chase the cat. The lion chases the cow. The lion is blue. The mouse chases the lion. The mouse does not need the cat. The mouse sees the lion. If something chases the mouse and the mouse does not see the lion then the lion does not see the cow. If something is nice then it does not chase the cat. If something chases the mouse and the mouse is not red then the mouse does not see the cow.
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is nice.
("cow" "is" "nice" "+")
The lion does not chase the cat.
("lion" "chases" "cat" "-")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something chases the mouse and the mouse does not see the lion then the lion does not see the cow.
((("something" "chases" "mouse" "+") ("mouse" "sees" "lion" "~")) -> ("lion" "sees" "cow" "-"))
If something is nice then it does not chase the cat.
((("something" "is" "nice" "+")) -> ("something" "chases" "cat" "-"))
If something chases the mouse and the mouse is not red then the mouse does not see the cow.
((("something" "chases" "mouse" "+") ("mouse" "is" "red" "~")) -> ("mouse" "sees" "cow" "-"))
The cat sees the cow.
True
1
proof
[(triple3)]
("cat" "sees" "cow" "+")
triple3
The lion does not chase the cow.
False
1
inv-proof
[(triple8)]
("lion" "chases" "cow" "-")
triple8
The cow does not chase the cat.
True
2
proof
[(((triple6) -> rule2))]
("cow" "chases" "cat" "-")
((triple6) -> (rule2 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1
The cow chases the cat.
False
2
inv-proof
[(((triple6) -> rule2))]
("cow" "chases" "cat" "+")
((triple6) -> (rule2 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1
The mouse does not need the cow.
Unknown
inv-random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse does not see the cat.
Unknown
inv-random
[@0: The mouse sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cat" "-")
The lion needs the mouse.
Unknown
random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "+")
@0: The cat does not chase the mouse.[(triple1)] The cat is nice.[(triple2)] The cat sees the cow.[(triple3)] The cat sees the lion.[(triple4)] The cat sees the mouse.[(triple5)] The cow is nice.[(triple6)] The lion chases the cow.[(triple8)] The lion does not chase the cat.[(triple7)] The lion is blue.[(triple9)] The mouse chases the lion.[(triple10)] The mouse does not need the cat.[(triple11)] The mouse sees the lion.[(triple12)] @1: The cat does not chase the cat.[(((triple2) -> rule2))] The cow does not chase the cat.[(((triple6) -> rule2))]
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat sees the cow.
("cat" "sees" "cow" "+")
triple3
The cat sees the lion.
("cat" "sees" "lion" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cow is nice.
("cow" "is" "nice" "+")
triple6
The lion chases the cow.
("lion" "chases" "cow" "+")
triple8
The lion does not chase the cat.
("lion" "chases" "cat" "-")
triple7
The lion is blue.
("lion" "is" "blue" "+")
triple9
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple10
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
triple11
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple12
The cat does not chase the cat.
("cat" "chases" "cat" "-")
((triple2) -> (rule2 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The cow does not chase the cat.
("cow" "chases" "cat" "-")
((triple6) -> (rule2 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1