The cow chases the tiger. The lion chases the tiger. The lion is cold. The lion visits the tiger. The squirrel does not chase the cow. The squirrel chases the lion. The squirrel does not eat the cow. The squirrel is red. The squirrel does not visit the cow. The tiger eats the squirrel. The tiger is kind. The tiger visits the squirrel. If someone visits the squirrel then the squirrel visits the tiger.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel does not visit the cow.
("squirrel" "visits" "cow" "-")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone visits the squirrel then the squirrel visits the tiger.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
The tiger is kind.
True
1
proof
[(triple11)]
("tiger" "is" "kind" "+")
triple11
The tiger does not eat the squirrel.
False
1
inv-proof
[(triple10)]
("tiger" "eats" "squirrel" "-")
triple10
The squirrel visits the tiger.
True
2
proof
[(((triple12) -> rule1))]
("squirrel" "visits" "tiger" "+")
((triple12) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel does not visit the tiger.
False
2
inv-proof
[(((triple12) -> rule1))]
("squirrel" "visits" "tiger" "-")
((triple12) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The lion does not chase the squirrel.
Unknown
inv-random
[@0: The lion chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "squirrel" "-")
The lion chases the cow.
Unknown
random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "+")
The cow does not chase the lion.
Unknown
inv-random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The cow chases the tiger.[(triple1)] The lion chases the tiger.[(triple2)] The lion is cold.[(triple3)] The lion visits the tiger.[(triple4)] The squirrel chases the lion.[(triple6)] The squirrel does not chase the cow.[(triple5)] The squirrel does not eat the cow.[(triple7)] The squirrel does not visit the cow.[(triple9)] The squirrel is red.[(triple8)] The tiger eats the squirrel.[(triple10)] The tiger is kind.[(triple11)] The tiger visits the squirrel.[(triple12)] @1: The squirrel visits the tiger.[(((triple12) -> rule1))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple4
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple6
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
triple5
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
triple7
The squirrel does not visit the cow.
("squirrel" "visits" "cow" "-")
triple9
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple12) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1