The mouse eats the tiger. The mouse is big. The mouse is rough. The tiger eats the mouse. The tiger is big. The tiger is kind. The tiger is rough. If something eats the mouse and it eats the tiger then it sees the mouse. If something is rough then it eats the tiger.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If something eats the mouse and it eats the tiger then it sees the mouse.
((("something" "eats" "mouse" "+") ("something" "eats" "tiger" "+")) -> ("something" "sees" "mouse" "+"))
If something is rough then it eats the tiger.
((("something" "is" "rough" "+")) -> ("something" "eats" "tiger" "+"))
The tiger is rough.
True
1
proof
[(triple7)]
("tiger" "is" "rough" "+")
triple7
The tiger is not rough.
False
1
inv-proof
[(triple7)]
("tiger" "is" "rough" "-")
triple7
The tiger eats the tiger.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "eats" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple7) -> rule2))]
("tiger" "eats" "tiger" "-")
((triple7) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the mouse.
True
4
proof
[(((triple4 ((triple7) -> rule2)) -> rule1))]
("tiger" "sees" "mouse" "+")
((triple4 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger does not see the mouse.
False
4
inv-proof
[(((triple4 ((triple7) -> rule2)) -> rule1))]
("tiger" "sees" "mouse" "-")
((triple4 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse sees the tiger.
Unknown
random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The mouse eats the tiger.[(triple1 OR ((triple3) -> rule2))] The mouse is big.[(triple2)] The mouse is rough.[(triple3)] The tiger eats the mouse.[(triple4)] The tiger is big.[(triple5)] The tiger is kind.[(triple6)] The tiger is rough.[(triple7)] @1: The tiger eats the tiger.[(((triple7) -> rule2))] @2: The tiger sees the mouse.[(((triple4 ((triple7) -> rule2)) -> rule1))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
((triple3) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple4 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2