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