The dog is red. The dog needs the mouse. The dog sees the mouse. The mouse is big. The mouse visits the dog. The squirrel is big. The squirrel visits the dog. If the squirrel visits the dog and the dog sees the mouse then the dog sees the squirrel.
The dog is red.
("dog" "is" "red" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If the squirrel visits the dog and the dog sees the mouse then the dog sees the squirrel.
((("squirrel" "visits" "dog" "+") ("dog" "sees" "mouse" "+")) -> ("dog" "sees" "squirrel" "+"))
The squirrel is big.
True
1
proof
[(triple6)]
("squirrel" "is" "big" "+")
triple6
The squirrel is not big.
False
1
inv-proof
[(triple6)]
("squirrel" "is" "big" "-")
triple6
The dog sees the squirrel.
True
3
proof
[(((triple7 triple3) -> rule1))]
("dog" "sees" "squirrel" "+")
((triple7 triple3) -> (rule1 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog does not see the squirrel.
False
3
inv-proof
[(((triple7 triple3) -> rule1))]
("dog" "sees" "squirrel" "-")
((triple7 triple3) -> (rule1 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The squirrel sees the dog.
Unknown
random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "+")
The mouse does not see the squirrel.
Unknown
inv-random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The dog is red.[(triple1)] The dog needs the mouse.[(triple2)] The dog sees the mouse.[(triple3)] The mouse is big.[(triple4)] The mouse visits the dog.[(triple5)] The squirrel is big.[(triple6)] The squirrel visits the dog.[(triple7)] @1: The dog sees the squirrel.[(((triple7 triple3) -> rule1))]
The dog is red.
("dog" "is" "red" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple7
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((triple7 triple3) -> (rule1 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1