The mouse is kind. The mouse sees the tiger. The tiger needs the mouse. If someone likes the mouse then the mouse likes the tiger. If someone is kind and they see the tiger then the tiger likes the mouse. If someone likes the mouse then the mouse is young. If someone sees the tiger then the tiger is cold. If someone likes the tiger then the tiger needs the mouse. If someone likes the tiger and the tiger needs the mouse then they see the mouse.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone likes the mouse then the mouse likes the tiger.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If someone is kind and they see the tiger then the tiger likes the mouse.
((("someone" "is" "kind" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "likes" "mouse" "+"))
If someone likes the mouse then the mouse is young.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone sees the tiger then the tiger is cold.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If someone likes the tiger then the tiger needs the mouse.
((("someone" "likes" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If someone likes the tiger and the tiger needs the mouse then they see the mouse.
((("someone" "likes" "tiger" "+") ("tiger" "needs" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
The tiger needs the mouse.
True
1
proof
[(triple3 OR ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule5))]
("tiger" "needs" "mouse" "+")
triple3
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The mouse does not see the tiger.
False
1
inv-proof
[(triple2)]
("mouse" "sees" "tiger" "-")
triple2
The tiger likes the mouse.
True
3
proof
[(((triple1 triple2) -> rule2))]
("tiger" "likes" "mouse" "+")
((triple1 triple2) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger is not cold.
False
2
inv-proof
[(((triple2) -> rule4))]
("tiger" "is" "cold" "-")
((triple2) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The mouse is young.
True
4
proof
[(((((triple1 triple2) -> rule2)) -> rule3))]
("mouse" "is" "young" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse is not young.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule3))]
("mouse" "is" "young" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse sees the mouse.
True
6
proof
[(((((((triple1 triple2) -> rule2)) -> rule1) triple3) -> rule6) OR ((((((triple1 triple2) -> rule2)) -> rule1) ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
("mouse" "sees" "mouse" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
((((((triple1 triple2) -> (rule2 % int4))) -> (rule1 % int3)) ((((((triple1 triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The mouse does not see the mouse.
False
6
inv-proof
[(((((((triple1 triple2) -> rule2)) -> rule1) triple3) -> rule6) OR ((((((triple1 triple2) -> rule2)) -> rule1) ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
("mouse" "sees" "mouse" "-")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
((((((triple1 triple2) -> (rule2 % int4))) -> (rule1 % int3)) ((((((triple1 triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger does not see the mouse.
Unknown
inv-rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "mouse" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
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 tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The mouse is kind.[(triple1)] The mouse sees the tiger.[(triple2)] The tiger needs the mouse.[(triple3 OR ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule5))] @1: The tiger is cold.[(((triple2) -> rule4))] The tiger likes the mouse.[(((triple1 triple2) -> rule2))] @2: The mouse is young.[(((((triple1 triple2) -> rule2)) -> rule3))] The mouse likes the tiger.[(((((triple1 triple2) -> rule2)) -> rule1))] @3: The mouse sees the mouse.[(((((((triple1 triple2) -> rule2)) -> rule1) triple3) -> rule6) OR ((((((triple1 triple2) -> rule2)) -> rule1) ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple2
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple3
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
((triple2) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((triple1 triple2) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
((((((triple1 triple2) -> (rule2 % int4))) -> (rule1 % int3)) ((((((triple1 triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4