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