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