The cow chases the tiger. The cow visits the tiger. The tiger chases the cow. If someone likes the tiger then they chase the cow. If someone chases the tiger then the tiger is red. If someone is round and green then they chase the cow. If someone chases the tiger and the tiger visits the cow then they like the cow. If someone visits the tiger and they are rough then the tiger likes the cow. If someone likes the cow then they are blue. If the cow visits the tiger and the tiger chases the cow then the tiger visits the cow. If someone is rough then they visit the cow.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
If someone likes the tiger then they chase the cow.
((("someone" "likes" "tiger" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the tiger then the tiger is red.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone is round and green then they chase the cow.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the tiger and the tiger visits the cow then they like the cow.
((("someone" "chases" "tiger" "+") ("tiger" "visits" "cow" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the tiger and they are rough then the tiger likes the cow.
((("someone" "visits" "tiger" "+") ("someone" "is" "rough" "+")) -> ("tiger" "likes" "cow" "+"))
If someone likes the cow then they are blue.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "blue" "+"))
If the cow visits the tiger and the tiger chases the cow then the tiger visits the cow.
((("cow" "visits" "tiger" "+") ("tiger" "chases" "cow" "+")) -> ("tiger" "visits" "cow" "+"))
If someone is rough then they visit the cow.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "cow" "+"))
The tiger chases the cow.
True
1
proof
[(triple3)]
("tiger" "chases" "cow" "+")
triple3
The cow does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cow" "chases" "tiger" "-")
triple1
The tiger visits the cow.
True
3
proof
[(((triple2 triple3) -> rule7))]
("tiger" "visits" "cow" "+")
((triple2 triple3) -> (rule7 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "is" "red" "-")
((triple1) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The cow likes the cow.
True
5
proof
[(((triple1 ((triple2 triple3) -> rule7)) -> rule4))]
("cow" "likes" "cow" "+")
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The cow does not like the cow.
False
5
inv-proof
[(((triple1 ((triple2 triple3) -> rule7)) -> rule4))]
("cow" "likes" "cow" "-")
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The cow is blue.
True
6
proof
[(((((triple1 ((triple2 triple3) -> rule7)) -> rule4)) -> rule6))]
("cow" "is" "blue" "+")
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The cow is not blue.
False
6
inv-proof
[(((((triple1 ((triple2 triple3) -> rule7)) -> rule4)) -> rule6))]
("cow" "is" "blue" "-")
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "-")
The tiger likes the cow.
Unknown
rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "cow" "+")
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "visits" "cow" "-")
The tiger is blue.
Unknown
rconc
[@2: The tiger is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cow chases the tiger.[(triple1)] The cow visits the tiger.[(triple2)] The tiger chases the cow.[(triple3)] @1: The tiger is red.[(((triple1) -> rule2))] The tiger visits the cow.[(((triple2 triple3) -> rule7))] @2: The cow likes the cow.[(((triple1 ((triple2 triple3) -> rule7)) -> rule4))] @3: The cow is blue.[(((((triple1 ((triple2 triple3) -> rule7)) -> rule4)) -> rule6))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
((triple1) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple2 triple3) -> (rule7 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1 ((triple2 triple3) -> (rule7 % int2))) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
((((triple1 ((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3