The cat chases the squirrel. The cat is big. The cat is round. The cat is young. The cat likes the squirrel. The cat visits the squirrel. The squirrel chases the cat. The squirrel is big. The squirrel likes the cat. The squirrel visits the cat. If something visits the squirrel then it visits the cat.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If something visits the squirrel then it visits the cat.
((("something" "visits" "squirrel" "+")) -> ("something" "visits" "cat" "+"))
The squirrel chases the cat.
True
1
proof
[(triple7)]
("squirrel" "chases" "cat" "+")
triple7
The cat is not big.
False
1
inv-proof
[(triple2)]
("cat" "is" "big" "-")
triple2
The cat visits the cat.
True
2
proof
[(((triple6) -> rule1))]
("cat" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple6) -> rule1))]
("cat" "visits" "cat" "-")
((triple6) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the squirrel.[(triple1)] The cat is big.[(triple2)] The cat is round.[(triple3)] The cat is young.[(triple4)] The cat likes the squirrel.[(triple5)] The cat visits the squirrel.[(triple6)] The squirrel chases the cat.[(triple7)] The squirrel is big.[(triple8)] The squirrel likes the cat.[(triple9)] The squirrel visits the cat.[(triple10)] @1: The cat visits the cat.[(((triple6) -> rule1))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple6
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple9
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple10
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1