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