The cat visits the squirrel. The cow does not see the cat. The squirrel is red. If the squirrel is red then the squirrel visits the cat. If something is young then it does not see the squirrel. If something likes the cow and the cow visits the squirrel then the cow likes the cat.
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow does not see the cat.
("cow" "sees" "cat" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
If the squirrel is red then the squirrel visits the cat.
((("squirrel" "is" "red" "+")) -> ("squirrel" "visits" "cat" "+"))
If something is young then it does not see the squirrel.
((("something" "is" "young" "+")) -> ("something" "sees" "squirrel" "-"))
If something likes the cow and the cow visits the squirrel then the cow likes the cat.
((("something" "likes" "cow" "+") ("cow" "visits" "squirrel" "+")) -> ("cow" "likes" "cat" "+"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The cow sees the cat.
False
1
inv-proof
[(triple2)]
("cow" "sees" "cat" "+")
triple2
The squirrel visits the cat.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "visits" "cat" "+")
((triple3) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "visits" "cat" "-")
((triple3) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cat" "-")
The cat sees the squirrel.
Unknown
random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat visits the squirrel.[(triple1)] The cow does not see the cat.[(triple2)] The squirrel is red.[(triple3)] @1: The squirrel visits the cat.[(((triple3) -> rule1))]
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple1
The cow does not see the cat.
("cow" "sees" "cat" "-")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple3) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1