The mouse is rough. The tiger is rough. The tiger likes the mouse. If the tiger likes the mouse and the tiger is rough then the mouse eats the tiger. If someone likes the mouse and the mouse eats the tiger then the tiger needs the mouse.
The mouse is rough.
("mouse" "is" "rough" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the tiger likes the mouse and the tiger is rough then the mouse eats the tiger.
((("tiger" "likes" "mouse" "+") ("tiger" "is" "rough" "+")) -> ("mouse" "eats" "tiger" "+"))
If someone likes the mouse and the mouse eats the tiger then the tiger needs the mouse.
((("someone" "likes" "mouse" "+") ("mouse" "eats" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
The tiger likes the mouse.
True
1
proof
[(triple3)]
("tiger" "likes" "mouse" "+")
triple3
The mouse is not rough.
False
1
inv-proof
[(triple1)]
("mouse" "is" "rough" "-")
triple1
The mouse eats the tiger.
True
3
proof
[(((triple3 triple2) -> rule1))]
("mouse" "eats" "tiger" "+")
((triple3 triple2) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse does not eat the tiger.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("mouse" "eats" "tiger" "-")
((triple3 triple2) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger needs the mouse.
True
5
proof
[(((triple3 ((triple3 triple2) -> rule1)) -> rule2))]
("tiger" "needs" "mouse" "+")
((triple3 ((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger does not need the mouse.
False
5
inv-proof
[(((triple3 ((triple3 triple2) -> rule1)) -> rule2))]
("tiger" "needs" "mouse" "-")
((triple3 ((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
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 cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The mouse is rough.[(triple1)] The tiger is rough.[(triple2)] The tiger likes the mouse.[(triple3)] @1: The mouse eats the tiger.[(((triple3 triple2) -> rule1))] @2: The tiger needs the mouse.[(((triple3 ((triple3 triple2) -> rule1)) -> rule2))]
The mouse is rough.
("mouse" "is" "rough" "+")
triple1
The tiger is rough.
("tiger" "is" "rough" "+")
triple2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple3 triple2) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((triple3 ((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2