The cow chases the tiger. The cow is big. The cow is cold. The cow is green. The cow is kind. The cow needs the tiger. The cow does not see the tiger. The tiger chases the cow. The tiger is big. The tiger is cold. The tiger is kind. The tiger is young. If something needs the tiger and it does not see the tiger then the tiger does not need the cow. If something chases the tiger and the tiger is not kind then the tiger does not see the cow. If something chases the cow then the cow chases the tiger.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
If something needs the tiger and it does not see the tiger then the tiger does not need the cow.
((("something" "needs" "tiger" "+") ("something" "sees" "tiger" "~")) -> ("tiger" "needs" "cow" "-"))
If something chases the tiger and the tiger is not kind then the tiger does not see the cow.
((("something" "chases" "tiger" "+") ("tiger" "is" "kind" "~")) -> ("tiger" "sees" "cow" "-"))
If something chases the cow then the cow chases the tiger.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
The cow is green.
True
1
proof
[(triple4)]
("cow" "is" "green" "+")
triple4
The cow is not cold.
False
1
inv-proof
[(triple3)]
("cow" "is" "cold" "-")
triple3
The tiger does not need the cow.
True
3
proof
[(((triple6 triple7) -> rule1))]
("tiger" "needs" "cow" "-")
((triple6 triple7) -> (rule1 % int1))
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
int1
The tiger needs the cow.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("tiger" "needs" "cow" "+")
((triple6 triple7) -> (rule1 % int1))
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
int1
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The tiger sees the cow.
Unknown
random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The cow chases the tiger.[(triple1 OR ((triple8) -> rule3))] The cow does not see the tiger.[(triple7)] The cow is big.[(triple2)] The cow is cold.[(triple3)] The cow is green.[(triple4)] The cow is kind.[(triple5)] The cow needs the tiger.[(triple6)] The tiger chases the cow.[(triple8)] The tiger is big.[(triple9)] The tiger is cold.[(triple10)] The tiger is kind.[(triple11)] The tiger is young.[(triple12)] @1: The tiger does not need the cow.[(((triple6 triple7) -> rule1))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
((triple8) -> (rule3 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
triple7
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
((triple6 triple7) -> (rule1 % int1))
The tiger does not need the cow.
("tiger" "needs" "cow" "-")
int1