The mouse chases the tiger. The mouse eats the tiger. The mouse is big. The mouse is blue. The mouse is red. The mouse is rough. The mouse is young. The mouse visits the tiger. The tiger chases the mouse. The tiger eats the mouse. The tiger is big. The tiger is blue. The tiger is red. The tiger is rough. The tiger is young. The tiger visits the mouse. If someone eats the mouse then they eat the tiger. If someone visits the tiger then they are red. If someone chases the mouse then they chase the tiger.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone eats the mouse then they eat the tiger.
((("someone" "eats" "mouse" "+")) -> ("someone" "eats" "tiger" "+"))
If someone visits the tiger then they are red.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "red" "+"))
If someone chases the mouse then they chase the tiger.
((("someone" "chases" "mouse" "+")) -> ("someone" "chases" "tiger" "+"))
The mouse eats the tiger.
True
1
proof
[(triple2)]
("mouse" "eats" "tiger" "+")
triple2
The tiger is not rough.
False
1
inv-proof
[(triple14)]
("tiger" "is" "rough" "-")
triple14
The tiger eats the tiger.
True
2
proof
[(((triple10) -> rule1))]
("tiger" "eats" "tiger" "+")
((triple10) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple9) -> rule3))]
("tiger" "chases" "tiger" "-")
((triple9) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
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 eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
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 visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is big.[(triple3)] The mouse is blue.[(triple4)] The mouse is red.[(triple5 OR ((triple8) -> rule2))] The mouse is rough.[(triple6)] The mouse is young.[(triple7)] The mouse visits the tiger.[(triple8)] The tiger chases the mouse.[(triple9)] The tiger eats the mouse.[(triple10)] The tiger is big.[(triple11)] The tiger is blue.[(triple12)] The tiger is red.[(triple13)] The tiger is rough.[(triple14)] The tiger is young.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The tiger chases the tiger.[(((triple9) -> rule3))] The tiger eats the tiger.[(((triple10) -> rule1))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
((triple8) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple9) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple10) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1