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