The cow chases the tiger. The cow is blue. The cow is rough. The cow is young. The cow likes the tiger. The cow sees the lion. The lion chases the tiger. The lion is young. The lion sees the tiger. The tiger is rough. If someone chases the cow and they chase the tiger then they see the lion. If someone chases the tiger and the tiger sees the cow then the tiger chases the cow. If someone sees the tiger then the tiger sees the cow.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone chases the cow and they chase the tiger then they see the lion.
((("someone" "chases" "cow" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the tiger and the tiger sees the cow then the tiger chases the cow.
((("someone" "chases" "tiger" "+") ("tiger" "sees" "cow" "+")) -> ("tiger" "chases" "cow" "+"))
If someone sees the tiger then the tiger sees the cow.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "cow" "+"))
The tiger is rough.
True
1
proof
[(triple10)]
("tiger" "is" "rough" "+")
triple10
The lion does not chase the tiger.
False
1
inv-proof
[(triple7)]
("lion" "chases" "tiger" "-")
triple7
The tiger sees the cow.
True
2
proof
[(((triple9) -> rule3))]
("tiger" "sees" "cow" "+")
((triple9) -> (rule3 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger does not see the cow.
False
2
inv-proof
[(((triple9) -> rule3))]
("tiger" "sees" "cow" "-")
((triple9) -> (rule3 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger chases the cow.
True
4
proof
[(((triple1 ((triple9) -> rule3)) -> rule2) OR ((triple7 ((triple9) -> rule3)) -> rule2))]
("tiger" "chases" "cow" "+")
((triple1 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
((triple7 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger does not chase the cow.
False
4
inv-proof
[(((triple1 ((triple9) -> rule3)) -> rule2) OR ((triple7 ((triple9) -> rule3)) -> rule2))]
("tiger" "chases" "cow" "-")
((triple1 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
((triple7 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "+")
The tiger does not like the lion.
Unknown
inv-random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The lion does not see the cow.
Unknown
inv-random
[@0: The lion sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cow" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The cow chases the tiger.[(triple1)] The cow is blue.[(triple2)] The cow is rough.[(triple3)] The cow is young.[(triple4)] The cow likes the tiger.[(triple5)] The cow sees the lion.[(triple6)] The lion chases the tiger.[(triple7)] The lion is young.[(triple8)] The lion sees the tiger.[(triple9)] The tiger is rough.[(triple10)] @1: The tiger sees the cow.[(((triple9) -> rule3))] @2: The tiger chases the cow.[(((triple1 ((triple9) -> rule3)) -> rule2) OR ((triple7 ((triple9) -> rule3)) -> rule2))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple5
The cow sees the lion.
("cow" "sees" "lion" "+")
triple6
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((triple9) -> (rule3 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
((triple1 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
((triple7 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2