The cow eats the tiger. The cow needs the tiger. The tiger needs the cow. If something is rough and red then it chases the cow. If something eats the tiger then it chases the tiger. If something needs the tiger and the tiger chases the cow then the cow eats the tiger.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If something is rough and red then it chases the cow.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "chases" "cow" "+"))
If something eats the tiger then it chases the tiger.
((("something" "eats" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
If something needs the tiger and the tiger chases the cow then the cow eats the tiger.
((("something" "needs" "tiger" "+") ("tiger" "chases" "cow" "+")) -> ("cow" "eats" "tiger" "+"))
The cow needs the tiger.
True
1
proof
[(triple2)]
("cow" "needs" "tiger" "+")
triple2
The tiger does not need the cow.
False
1
inv-proof
[(triple3)]
("tiger" "needs" "cow" "-")
triple3
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The cow eats the tiger.[(triple1)] The cow needs the tiger.[(triple2)] The tiger needs the cow.[(triple3)] @1: The cow chases the tiger.[(((triple1) -> rule2))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple3
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((triple1) -> (rule2 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1