The cat visits the squirrel. The mouse sees the squirrel. The squirrel sees the mouse. If someone visits the squirrel then they are nice. If someone is nice then they visit the mouse.
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone visits the squirrel then they are nice.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they visit the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "mouse" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple3)]
("squirrel" "sees" "mouse" "+")
triple3
The cat does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "visits" "squirrel" "-")
triple1
The cat is nice.
True
2
proof
[(((triple1) -> rule1))]
("cat" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the mouse.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("cat" "visits" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat does not visit the mouse.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("cat" "visits" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "nice" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "nice" "+")
The squirrel does not visit the mouse.
Unknown
inv-rconc
[@2: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("squirrel" "visits" "mouse" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
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 mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cat visits the squirrel.[(triple1)] The mouse sees the squirrel.[(triple2)] The squirrel sees the mouse.[(triple3)] @1: The cat is nice.[(((triple1) -> rule1))] @2: The cat visits the mouse.[(((((triple1) -> rule1)) -> rule2))]
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2