The mouse is green. The mouse is kind. The mouse is nice. The mouse sees the tiger. The tiger eats the mouse. The tiger is kind. The tiger visits the mouse. If someone is cold and they visit the tiger then they eat the mouse. If the mouse is kind then the mouse visits the tiger. If someone is cold and they see the mouse then the mouse visits the tiger. If the tiger visits the mouse and the mouse visits the tiger then the tiger sees the mouse. If someone sees the mouse then they are cold. If someone visits the tiger then they visit the mouse.
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is cold and they visit the tiger then they eat the mouse.
((("someone" "is" "cold" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "eats" "mouse" "+"))
If the mouse is kind then the mouse visits the tiger.
((("mouse" "is" "kind" "+")) -> ("mouse" "visits" "tiger" "+"))
If someone is cold and they see the mouse then the mouse visits the tiger.
((("someone" "is" "cold" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If the tiger visits the mouse and the mouse visits the tiger then the tiger sees the mouse.
((("tiger" "visits" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone sees the mouse then they are cold.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone visits the tiger then they visit the mouse.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "mouse" "+"))
The mouse sees the tiger.
True
1
proof
[(triple4)]
("mouse" "sees" "tiger" "+")
triple4
The mouse is not green.
False
1
inv-proof
[(triple1)]
("mouse" "is" "green" "-")
triple1
The mouse visits the tiger.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "visits" "tiger" "+")
((triple2) -> (rule2 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "visits" "tiger" "-")
((triple2) -> (rule2 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The tiger sees the mouse.
True
4
proof
[(((triple7 ((triple2) -> rule2)) -> rule4))]
("tiger" "sees" "mouse" "+")
((triple7 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse does not visit the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("mouse" "visits" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The tiger is cold.
True
5
proof
[(((((triple7 ((triple2) -> rule2)) -> rule4)) -> rule5))]
("tiger" "is" "cold" "+")
((((triple7 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The tiger is not cold.
False
5
inv-proof
[(((((triple7 ((triple2) -> rule2)) -> rule4)) -> rule5))]
("tiger" "is" "cold" "-")
((((triple7 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-rconc
[@2: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "cold" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The mouse does not eat the tiger.
Unknown
inv-random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is green.[(triple1)] The mouse is kind.[(triple2)] The mouse is nice.[(triple3)] The mouse sees the tiger.[(triple4)] The tiger eats the mouse.[(triple5)] The tiger is kind.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The mouse visits the tiger.[(((triple2) -> rule2))] @2: The mouse visits the mouse.[(((((triple2) -> rule2)) -> rule6))] The tiger sees the mouse.[(((triple7 ((triple2) -> rule2)) -> rule4))] @3: The tiger is cold.[(((((triple7 ((triple2) -> rule2)) -> rule4)) -> rule5))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple2) -> (rule2 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple7 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple7 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3