The cow is big. The cow is cold. The squirrel chases the cow. The squirrel is nice. The squirrel is not rough. The squirrel needs the cow. The tiger needs the squirrel. If someone likes the squirrel and they are nice then the squirrel chases the cow. If someone needs the cow and they do not like the tiger then the tiger likes the squirrel. If the tiger chases the squirrel then the tiger needs the squirrel. If someone chases the squirrel and the squirrel is nice then the squirrel is not big. If the cow chases the squirrel and the cow does not need the tiger then the cow is nice. If someone likes the squirrel and they are nice then the squirrel chases the tiger. If someone is rough and they like the squirrel then the squirrel likes the cow. If someone needs the squirrel then they are not big.
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If someone likes the squirrel and they are nice then the squirrel chases the cow.
((("someone" "likes" "squirrel" "+") ("someone" "is" "nice" "+")) -> ("squirrel" "chases" "cow" "+"))
If someone needs the cow and they do not like the tiger then the tiger likes the squirrel.
((("someone" "needs" "cow" "+") ("someone" "likes" "tiger" "~")) -> ("tiger" "likes" "squirrel" "+"))
If the tiger chases the squirrel then the tiger needs the squirrel.
((("tiger" "chases" "squirrel" "+")) -> ("tiger" "needs" "squirrel" "+"))
If someone chases the squirrel and the squirrel is nice then the squirrel is not big.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "big" "-"))
If the cow chases the squirrel and the cow does not need the tiger then the cow is nice.
((("cow" "chases" "squirrel" "+") ("cow" "needs" "tiger" "~")) -> ("cow" "is" "nice" "+"))
If someone likes the squirrel and they are nice then the squirrel chases the tiger.
((("someone" "likes" "squirrel" "+") ("someone" "is" "nice" "+")) -> ("squirrel" "chases" "tiger" "+"))
If someone is rough and they like the squirrel then the squirrel likes the cow.
((("someone" "is" "rough" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "cow" "+"))
If someone needs the squirrel then they are not big.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "big" "-"))
The squirrel is nice.
True
1
proof
[(triple4)]
("squirrel" "is" "nice" "+")
triple4
The squirrel is rough.
False
1
inv-proof
[(triple5)]
("squirrel" "is" "rough" "+")
triple5
The tiger does not like the squirrel.
Unknown
inv-rconc
[@1: The tiger likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "squirrel" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The cow is big.[(triple1)] The cow is cold.[(triple2)] The squirrel chases the cow.[(triple3)] The squirrel is nice.[(triple4)] The squirrel is not rough.[(triple5)] The squirrel needs the cow.[(triple6)] The tiger needs the squirrel.[(triple7)] @1: The tiger is not big.[(((triple7) -> rule8))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple5
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple6
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple7
The tiger is not big.
("tiger" "is" "big" "-")
((triple7) -> (rule8 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1