The bear eats the mouse. The dog is big. The mouse sees the rabbit. The rabbit sees the mouse. If something sees the rabbit then it eats the bear. If something eats the rabbit then it eats the mouse.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the rabbit then it eats the bear.
((("something" "sees" "rabbit" "+")) -> ("something" "eats" "bear" "+"))
If something eats the rabbit then it eats the mouse.
((("something" "eats" "rabbit" "+")) -> ("something" "eats" "mouse" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple4)]
("rabbit" "sees" "mouse" "+")
triple4
The mouse does not see the rabbit.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "rabbit" "-")
triple3
The mouse eats the bear.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "eats" "bear" "+")
((triple3) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not eat the bear.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "eats" "bear" "-")
((triple3) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The dog eats the mouse.
Unknown
rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "mouse" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog eats the rabbit.
Unknown
random
[@0: The dog eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "rabbit" "+")
@0: The bear eats the mouse.[(triple1)] The dog is big.[(triple2)] The mouse sees the rabbit.[(triple3)] The rabbit sees the mouse.[(triple4)] @1: The mouse eats the bear.[(((triple3) -> rule1))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple3
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple4
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple3) -> (rule1 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1