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