The cat eats the squirrel. The cow chases the cat. The squirrel chases the cat. The tiger chases the cat. If someone is rough then they visit the cow. If someone visits the cow and the cow is green then they are rough. If someone visits the squirrel and they chase the squirrel then the squirrel chases the cow.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
If someone is rough then they visit the cow.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cow and the cow is green then they are rough.
((("someone" "visits" "cow" "+") ("cow" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the squirrel and they chase the squirrel then the squirrel chases the cow.
((("someone" "visits" "squirrel" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
The squirrel chases the cat.
True
1
proof
[(triple3)]
("squirrel" "chases" "cat" "+")
triple3
The squirrel does not chase the cat.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "cat" "-")
triple3
The squirrel does not visit the cow.
Unknown
inv-rconc
[@2: The squirrel visits the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "visits" "cow" "-")
The tiger eats the squirrel.
Unknown
random
[@0: The tiger eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "squirrel" "+")
@0: The cat eats the squirrel.[(triple1)] The cow chases the cat.[(triple2)] The squirrel chases the cat.[(triple3)] The tiger chases the cat.[(triple4)]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple4