The mouse eats the tiger. The mouse is nice. The mouse is red. The mouse is round. The mouse likes the tiger. The mouse sees the tiger. The tiger eats the mouse. The tiger is green. The tiger is nice. The tiger is round. The tiger likes the mouse. The tiger sees the mouse. If someone sees the tiger then they eat the tiger. If someone sees the mouse and the mouse eats the tiger then they see the tiger.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone sees the tiger then they eat the tiger.
((("someone" "sees" "tiger" "+")) -> ("someone" "eats" "tiger" "+"))
If someone sees the mouse and the mouse eats the tiger then they see the tiger.
((("someone" "sees" "mouse" "+") ("mouse" "eats" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
The mouse is round.
True
1
proof
[(triple4)]
("mouse" "is" "round" "+")
triple4
The tiger is not nice.
False
1
inv-proof
[(triple9)]
("tiger" "is" "nice" "-")
triple9
The tiger sees the tiger.
True
3
proof
[(((triple12 triple1) -> rule2) OR ((triple12 ((triple6) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple12 triple1) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
((triple12 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((triple12 triple1) -> rule2) OR ((triple12 ((triple6) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple12 triple1) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
((triple12 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger eats the tiger.
True
4
proof
[(((((triple12 triple1) -> rule2)) -> rule1) OR ((((triple12 ((triple6) -> rule1)) -> rule2)) -> rule1))]
("tiger" "eats" "tiger" "+")
((((triple12 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
((((triple12 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The tiger does not eat the tiger.
False
4
inv-proof
[(((((triple12 triple1) -> rule2)) -> rule1) OR ((((triple12 ((triple6) -> rule1)) -> rule2)) -> rule1))]
("tiger" "eats" "tiger" "-")
((((triple12 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
((((triple12 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
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 cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The mouse eats the tiger.[(triple1 OR ((triple6) -> rule1))] The mouse is nice.[(triple2)] The mouse is red.[(triple3)] The mouse is round.[(triple4)] The mouse likes the tiger.[(triple5)] The mouse sees the tiger.[(triple6)] The tiger eats the mouse.[(triple7)] The tiger is green.[(triple8)] The tiger is nice.[(triple9)] The tiger is round.[(triple10)] The tiger likes the mouse.[(triple11)] The tiger sees the mouse.[(triple12)] @1: The tiger sees the tiger.[(((triple12 triple1) -> rule2) OR ((triple12 ((triple6) -> rule1)) -> rule2))] @2: The tiger eats the tiger.[(((((triple12 triple1) -> rule2)) -> rule1) OR ((((triple12 ((triple6) -> rule1)) -> rule2)) -> rule1))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
((triple6) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple12 triple1) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
((triple12 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple12 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
((((triple12 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3