The bear likes the mouse. The cat is young. The mouse does not like the cat. The rabbit needs the cat. If someone likes the mouse then they do not need the mouse. If someone eats the bear then they like the mouse. If someone needs the mouse and the mouse is nice then the mouse eats the bear. If the cat needs the bear then the bear does not need the mouse. If someone needs the cat then they eat the bear. If someone eats the bear and they do not like the mouse then they need the rabbit.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The cat is young.
("cat" "is" "young" "+")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone likes the mouse then they do not need the mouse.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "mouse" "-"))
If someone eats the bear then they like the mouse.
((("someone" "eats" "bear" "+")) -> ("someone" "likes" "mouse" "+"))
If someone needs the mouse and the mouse is nice then the mouse eats the bear.
((("someone" "needs" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "eats" "bear" "+"))
If the cat needs the bear then the bear does not need the mouse.
((("cat" "needs" "bear" "+")) -> ("bear" "needs" "mouse" "-"))
If someone needs the cat then they eat the bear.
((("someone" "needs" "cat" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the bear and they do not like the mouse then they need the rabbit.
((("someone" "eats" "bear" "+") ("someone" "likes" "mouse" "~")) -> ("someone" "needs" "rabbit" "+"))
The bear likes the mouse.
True
1
proof
[(triple1)]
("bear" "likes" "mouse" "+")
triple1
The cat is not young.
False
1
inv-proof
[(triple2)]
("cat" "is" "young" "-")
triple2
The bear does not need the mouse.
True
2
proof
[(((triple1) -> rule1))]
("bear" "needs" "mouse" "-")
((triple1) -> (rule1 % int1))
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
int1
The bear needs the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "needs" "mouse" "+")
((triple1) -> (rule1 % int1))
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
int1
The rabbit likes the mouse.
True
3
proof
[(((((triple4) -> rule5)) -> rule2))]
("rabbit" "likes" "mouse" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit does not like the mouse.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule2))]
("rabbit" "likes" "mouse" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit does not need the mouse.
True
4
proof
[(((((((triple4) -> rule5)) -> rule2)) -> rule1))]
("rabbit" "needs" "mouse" "-")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit does not need the mouse.
("rabbit" "needs" "mouse" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int3
The rabbit needs the mouse.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule2)) -> rule1))]
("rabbit" "needs" "mouse" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit does not need the mouse.
("rabbit" "needs" "mouse" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int3
The bear does not need the rabbit.
Unknown
inv-rconc
[@1: The bear needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "rabbit" "-")
The cat likes the mouse.
Unknown
rconc
[@2: The cat likes the mouse.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("cat" "likes" "mouse" "+")
The cat does not eat the bear.
Unknown
inv-rconc
[@1: The cat eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "bear" "-")
The bear eats the bear.
Unknown
rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The bear likes the mouse.[(triple1)] The cat is young.[(triple2)] The mouse does not like the cat.[(triple3)] The rabbit needs the cat.[(triple4)] @1: The bear does not need the mouse.[(((triple1) -> rule1))] The rabbit eats the bear.[(((triple4) -> rule5))] @2: The rabbit likes the mouse.[(((((triple4) -> rule5)) -> rule2))] @3: The rabbit does not need the mouse.[(((((((triple4) -> rule5)) -> rule2)) -> rule1))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple4
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
((triple1) -> (rule1 % int1))
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((triple4) -> (rule5 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit does not need the mouse.
("rabbit" "needs" "mouse" "-")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit does not need the mouse.
("rabbit" "needs" "mouse" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int3