The mouse visits the tiger. The tiger chases the mouse. The tiger likes the mouse. If the tiger likes the mouse and the tiger is rough then the tiger chases the mouse. If the tiger likes the mouse then the mouse likes the tiger. If something likes the tiger then it chases the mouse.
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the tiger likes the mouse and the tiger is rough then the tiger chases the mouse.
((("tiger" "likes" "mouse" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "chases" "mouse" "+"))
If the tiger likes the mouse then the mouse likes the tiger.
((("tiger" "likes" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If something likes the tiger then it chases the mouse.
((("something" "likes" "tiger" "+")) -> ("something" "chases" "mouse" "+"))
The tiger likes the mouse.
True
1
proof
[(triple3)]
("tiger" "likes" "mouse" "+")
triple3
The mouse does not visit the tiger.
False
1
inv-proof
[(triple1)]
("mouse" "visits" "tiger" "-")
triple1
The mouse likes the tiger.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "likes" "tiger" "+")
((triple3) -> (rule2 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse does not like the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "likes" "tiger" "-")
((triple3) -> (rule2 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse chases the mouse.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "chases" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse does not chase the mouse.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "chases" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The tiger visits the mouse.
Unknown
random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "+")
@0: The mouse visits the tiger.[(triple1)] The tiger chases the mouse.[(triple2)] The tiger likes the mouse.[(triple3)] @1: The mouse likes the tiger.[(((triple3) -> rule2))] @2: The mouse chases the mouse.[(((((triple3) -> rule2)) -> rule3))]
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple3) -> (rule2 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2