The cow does not chase the tiger. The cow eats the tiger. The cow is blue. The cow is round. The cow needs the tiger. The tiger chases the cow. The tiger eats the cow. The tiger is not blue. The tiger is green. The tiger is rough. The tiger is round. The tiger needs the cow. If someone eats the cow then they are not big.
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If someone eats the cow then they are not big.
((("someone" "eats" "cow" "+")) -> ("someone" "is" "big" "-"))
The tiger eats the cow.
True
1
proof
[(triple7)]
("tiger" "eats" "cow" "+")
triple7
The cow chases the tiger.
False
1
inv-proof
[(triple1)]
("cow" "chases" "tiger" "+")
triple1
The tiger is not big.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "is" "big" "-")
((triple7) -> (rule1 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger is big.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "is" "big" "+")
((triple7) -> (rule1 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow does not chase the tiger.[(triple1)] The cow eats the tiger.[(triple2)] The cow is blue.[(triple3)] The cow is round.[(triple4)] The cow needs the tiger.[(triple5)] The tiger chases the cow.[(triple6)] The tiger eats the cow.[(triple7)] The tiger is green.[(triple9)] The tiger is not blue.[(triple8)] The tiger is rough.[(triple10)] The tiger is round.[(triple11)] The tiger needs the cow.[(triple12)] @1: The tiger is not big.[(((triple7) -> rule1))]
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
triple1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple5
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple6
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger is not blue.
("tiger" "is" "blue" "-")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple12
The tiger is not big.
("tiger" "is" "big" "-")
((triple7) -> (rule1 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1