The bear likes the mouse. The dog likes the rabbit. The dog needs the mouse. The dog sees the mouse. The mouse is kind. The rabbit likes the dog. The rabbit sees the dog. If something needs the dog and the dog likes the rabbit then the rabbit does not need the bear. If the bear is red and the bear is kind then the bear likes the mouse. If something sees the mouse and the mouse likes the dog then the mouse is blue. If the dog is not rough and the dog is not red then the dog sees the bear. If something likes the mouse then the mouse likes the rabbit. If something likes the rabbit then it does not see the bear.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something needs the dog and the dog likes the rabbit then the rabbit does not need the bear.
((("something" "needs" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "needs" "bear" "-"))
If the bear is red and the bear is kind then the bear likes the mouse.
((("bear" "is" "red" "+") ("bear" "is" "kind" "+")) -> ("bear" "likes" "mouse" "+"))
If something sees the mouse and the mouse likes the dog then the mouse is blue.
((("something" "sees" "mouse" "+") ("mouse" "likes" "dog" "+")) -> ("mouse" "is" "blue" "+"))
If the dog is not rough and the dog is not red then the dog sees the bear.
((("dog" "is" "rough" "~") ("dog" "is" "red" "~")) -> ("dog" "sees" "bear" "+"))
If something likes the mouse then the mouse likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something likes the rabbit then it does not see the bear.
((("something" "likes" "rabbit" "+")) -> ("something" "sees" "bear" "-"))
The dog sees the mouse.
True
1
proof
[(triple4)]
("dog" "sees" "mouse" "+")
triple4
The bear does not like the mouse.
False
1
inv-proof
[(triple1)]
("bear" "likes" "mouse" "-")
triple1
The mouse likes the rabbit.
True
2
proof
[(((triple1) -> rule5))]
("mouse" "likes" "rabbit" "+")
((triple1) -> (rule5 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The dog sees the bear.
False
2
inv-proof
[(((triple2) -> rule6))]
("dog" "sees" "bear" "+")
((triple2) -> (rule6 % int1))
The dog does not see the bear.
("dog" "sees" "bear" "-")
int1
The mouse does not see the bear.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("mouse" "sees" "bear" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse sees the bear.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("mouse" "sees" "bear" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The rabbit needs the mouse.
Unknown
random
[@0: The rabbit needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "mouse" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The mouse likes the bear.
Unknown
random
[@0: The mouse likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bear" "+")
The bear does not see the dog.
Unknown
inv-random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "-")
The rabbit likes the mouse.
Unknown
random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "+")
@0: The bear likes the mouse.[(triple1)] The dog likes the rabbit.[(triple2)] The dog needs the mouse.[(triple3)] The dog sees the mouse.[(triple4)] The mouse is kind.[(triple5)] The rabbit likes the dog.[(triple6)] The rabbit sees the dog.[(triple7)] @1: The dog does not see the bear.[(((triple2) -> rule6))] The mouse likes the rabbit.[(((triple1) -> rule5))] @2: The mouse does not see the bear.[(((((triple1) -> rule5)) -> rule6))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple6
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple7
The dog does not see the bear.
("dog" "sees" "bear" "-")
((triple2) -> (rule6 % int1))
The dog does not see the bear.
("dog" "sees" "bear" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((triple1) -> (rule5 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The mouse does not see the bear.
("mouse" "sees" "bear" "-")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2