The cat sees the mouse. The dog is young. The mouse sees the cat. The tiger sees the dog. If someone sees the cat then the cat is green.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The dog is young.
("dog" "is" "young" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone sees the cat then the cat is green.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "green" "+"))
The cat sees the mouse.
True
1
proof
[(triple1)]
("cat" "sees" "mouse" "+")
triple1
The dog is not young.
False
1
inv-proof
[(triple2)]
("dog" "is" "young" "-")
triple2
The cat is green.
True
2
proof
[(((triple3) -> rule1))]
("cat" "is" "green" "+")
((triple3) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "is" "green" "-")
((triple3) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog does not see the cat.
Unknown
inv-random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The mouse does not see the dog.
Unknown
inv-random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
@0: The cat sees the mouse.[(triple1)] The dog is young.[(triple2)] The mouse sees the cat.[(triple3)] The tiger sees the dog.[(triple4)] @1: The cat is green.[(((triple3) -> rule1))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple3
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple4
The cat is green.
("cat" "is" "green" "+")
((triple3) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1