The cow chases the tiger. The cow is big. The cow visits the lion. The lion chases the cow. The lion chases the squirrel. The squirrel chases the cow. The tiger chases the squirrel. The tiger is cold. The tiger is nice. The tiger visits the squirrel. If the tiger visits the lion then the lion is kind. If something is cold and it visits the squirrel then the squirrel chases the lion.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is big.
("cow" "is" "big" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the tiger visits the lion then the lion is kind.
((("tiger" "visits" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something is cold and it visits the squirrel then the squirrel chases the lion.
((("something" "is" "cold" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "chases" "lion" "+"))
The cow is big.
True
1
proof
[(triple2)]
("cow" "is" "big" "+")
triple2
The cow does not visit the lion.
False
1
inv-proof
[(triple3)]
("cow" "visits" "lion" "-")
triple3
The squirrel chases the lion.
True
3
proof
[(((triple8 triple10) -> rule2))]
("squirrel" "chases" "lion" "+")
((triple8 triple10) -> (rule2 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel does not chase the lion.
False
3
inv-proof
[(((triple8 triple10) -> rule2))]
("squirrel" "chases" "lion" "-")
((triple8 triple10) -> (rule2 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "kind" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not visit the cow.
Unknown
inv-random
[@0: The tiger visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cow" "-")
The squirrel chases the tiger.
Unknown
random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "+")
@0: The cow chases the tiger.[(triple1)] The cow is big.[(triple2)] The cow visits the lion.[(triple3)] The lion chases the cow.[(triple4)] The lion chases the squirrel.[(triple5)] The squirrel chases the cow.[(triple6)] The tiger chases the squirrel.[(triple7)] The tiger is cold.[(triple8)] The tiger is nice.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The squirrel chases the lion.[(((triple8 triple10) -> rule2))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow visits the lion.
("cow" "visits" "lion" "+")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple5
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple6
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple8 triple10) -> (rule2 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1