The mouse eats the tiger. The mouse is not young. The mouse sees the tiger. The mouse visits the tiger. The tiger is big. The tiger is young. The tiger sees the mouse. If something eats the tiger then it eats the mouse. If something is young then it eats the tiger.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something eats the tiger then it eats the mouse.
((("something" "eats" "tiger" "+")) -> ("something" "eats" "mouse" "+"))
If something is young then it eats the tiger.
((("something" "is" "young" "+")) -> ("something" "eats" "tiger" "+"))
The tiger is young.
True
1
proof
[(triple6)]
("tiger" "is" "young" "+")
triple6
The mouse is young.
False
1
inv-proof
[(triple2)]
("mouse" "is" "young" "+")
triple2
The mouse eats the mouse.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "eats" "mouse" "+")
((triple1) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "eats" "mouse" "-")
((triple1) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The tiger eats the mouse.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("tiger" "eats" "mouse" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger does not eat the mouse.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("tiger" "eats" "mouse" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The tiger does not visit the mouse.
Unknown
inv-random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The mouse eats the tiger.[(triple1)] The mouse is not young.[(triple2)] The mouse sees the tiger.[(triple3)] The mouse visits the tiger.[(triple4)] The tiger is big.[(triple5)] The tiger is young.[(triple6)] The tiger sees the mouse.[(triple7)] @1: The mouse eats the mouse.[(((triple1) -> rule1))] The tiger eats the tiger.[(((triple6) -> rule2))] @2: The tiger eats the mouse.[(((((triple6) -> rule2)) -> rule1))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The mouse is not young.
("mouse" "is" "young" "-")
triple2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple1) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple6) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2