The bear is big. The bear is green. The bear needs the cat. The bear sees the mouse. The bear visits the mouse. The cat is nice. The cat needs the mouse. The cat visits the mouse. The dog needs the cat. The mouse is big. If the mouse sees the dog then the mouse sees the bear. If someone needs the cat then they see the mouse.
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
If the mouse sees the dog then the mouse sees the bear.
((("mouse" "sees" "dog" "+")) -> ("mouse" "sees" "bear" "+"))
If someone needs the cat then they see the mouse.
((("someone" "needs" "cat" "+")) -> ("someone" "sees" "mouse" "+"))
The dog needs the cat.
True
1
proof
[(triple9)]
("dog" "needs" "cat" "+")
triple9
The cat does not need the mouse.
False
1
inv-proof
[(triple7)]
("cat" "needs" "mouse" "-")
triple7
The dog sees the mouse.
True
2
proof
[(((triple9) -> rule2))]
("dog" "sees" "mouse" "+")
((triple9) -> (rule2 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog does not see the mouse.
False
2
inv-proof
[(((triple9) -> rule2))]
("dog" "sees" "mouse" "-")
((triple9) -> (rule2 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cat sees the mouse.
Unknown
rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "mouse" "+")
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 bear visits the cat.
Unknown
random
[@0: The bear visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cat" "+")
@0: The bear is big.[(triple1)] The bear is green.[(triple2)] The bear needs the cat.[(triple3)] The bear sees the mouse.[(triple4 OR ((triple3) -> rule2))] The bear visits the mouse.[(triple5)] The cat is nice.[(triple6)] The cat needs the mouse.[(triple7)] The cat visits the mouse.[(triple8)] The dog needs the cat.[(triple9)] The mouse is big.[(triple10)] @1: The dog sees the mouse.[(((triple9) -> rule2))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear needs the cat.
("bear" "needs" "cat" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
((triple3) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple5
The cat is nice.
("cat" "is" "nice" "+")
triple6
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple7
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple8
The dog needs the cat.
("dog" "needs" "cat" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple9) -> (rule2 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1