The cat chases the cow. The cow chases the tiger. The cow does not like the mouse. The cow needs the mouse. The mouse chases the cow. The mouse likes the cat. The tiger likes the mouse. If the cat is cold then the cat chases the tiger. If someone is green and not cold then they chase the tiger. If someone chases the tiger then the tiger chases the mouse. If someone likes the mouse and the mouse does not like the tiger then the mouse likes the cat. If someone chases the tiger and they do not need the mouse then the tiger is not green. If someone likes the cow and they do not like the cat then the cat needs the tiger. If someone needs the cat then the cat needs the tiger. If someone is green and they do not need the tiger then they chase the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the cat is cold then the cat chases the tiger.
((("cat" "is" "cold" "+")) -> ("cat" "chases" "tiger" "+"))
If someone is green and not cold then they chase the tiger.
((("someone" "is" "green" "+") ("someone" "is" "cold" "~")) -> ("someone" "chases" "tiger" "+"))
If someone chases the tiger then the tiger chases the mouse.
((("someone" "chases" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone likes the mouse and the mouse does not like the tiger then the mouse likes the cat.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "tiger" "~")) -> ("mouse" "likes" "cat" "+"))
If someone chases the tiger and they do not need the mouse then the tiger is not green.
((("someone" "chases" "tiger" "+") ("someone" "needs" "mouse" "~")) -> ("tiger" "is" "green" "-"))
If someone likes the cow and they do not like the cat then the cat needs the tiger.
((("someone" "likes" "cow" "+") ("someone" "likes" "cat" "~")) -> ("cat" "needs" "tiger" "+"))
If someone needs the cat then the cat needs the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If someone is green and they do not need the tiger then they chase the cow.
((("someone" "is" "green" "+") ("someone" "needs" "tiger" "~")) -> ("someone" "chases" "cow" "+"))
The tiger likes the mouse.
True
1
proof
[(triple7)]
("tiger" "likes" "mouse" "+")
triple7
The cat does not chase the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The tiger chases the mouse.
True
2
proof
[(((triple2) -> rule3))]
("tiger" "chases" "mouse" "+")
((triple2) -> (rule3 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "chases" "mouse" "-")
((triple2) -> (rule3 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger does not chase the cow.
Unknown
inv-rconc
[@1: The tiger chases the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "chases" "cow" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "cow" "+")
The mouse does not need the cat.
Unknown
inv-random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cat chases the cow.[(triple1)] The cow chases the tiger.[(triple2)] The cow does not like the mouse.[(triple3)] The cow needs the mouse.[(triple4)] The mouse chases the cow.[(triple5)] The mouse likes the cat.[(triple6)] The tiger likes the mouse.[(triple7)] @1: The tiger chases the mouse.[(((triple2) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple2
The cow does not like the mouse.
("cow" "likes" "mouse" "-")
triple3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple4
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple6
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple7
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((triple2) -> (rule3 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1