The cow chases the rabbit. The cow is big. The cow is blue. The cow visits the rabbit. The rabbit is cold. The rabbit likes the tiger. The rabbit visits the tiger. The tiger chases the cow. The tiger chases the rabbit. The tiger is big. The tiger is blue. The tiger likes the cow. The tiger likes the rabbit. The tiger visits the cow. The tiger visits the rabbit. If something chases the tiger then the tiger is big. If something likes the cow then it visits the cow. If something likes the rabbit then it likes the cow.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something chases the tiger then the tiger is big.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If something likes the cow then it visits the cow.
((("something" "likes" "cow" "+")) -> ("something" "visits" "cow" "+"))
If something likes the rabbit then it likes the cow.
((("something" "likes" "rabbit" "+")) -> ("something" "likes" "cow" "+"))
The cow chases the rabbit.
True
1
proof
[(triple1)]
("cow" "chases" "rabbit" "+")
triple1
The tiger does not visit the rabbit.
False
1
inv-proof
[(triple15)]
("tiger" "visits" "rabbit" "-")
triple15
The rabbit does not like the cow.
Unknown
inv-rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "cow" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The cow chases the rabbit.[(triple1)] The cow is big.[(triple2)] The cow is blue.[(triple3)] The cow visits the rabbit.[(triple4)] The rabbit is cold.[(triple5)] The rabbit likes the tiger.[(triple6)] The rabbit visits the tiger.[(triple7)] The tiger chases the cow.[(triple8)] The tiger chases the rabbit.[(triple9)] The tiger is big.[(triple10)] The tiger is blue.[(triple11)] The tiger likes the cow.[(triple12 OR ((triple13) -> rule3))] The tiger likes the rabbit.[(triple13)] The tiger visits the cow.[(triple14 OR ((triple12) -> rule2) OR ((((triple13) -> rule3)) -> rule2))] The tiger visits the rabbit.[(triple15)]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple7
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
((triple13) -> (rule3 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple13
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple14
((triple12) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15