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