The mouse is blue. The mouse is kind. The mouse is nice. The mouse is red. The mouse is young. The mouse likes the tiger. The mouse needs the tiger. The mouse visits the tiger. The tiger is blue. The tiger is kind. The tiger is red. The tiger is young. The tiger does not like the mouse. The tiger needs the mouse. The tiger visits the mouse. If someone needs the mouse then the mouse needs the tiger. If someone needs the mouse then they like the tiger. If someone likes the tiger then they are nice. If someone visits the tiger and the tiger is nice then the tiger does not like the mouse. If the tiger likes the mouse then the tiger does not need the mouse. If the tiger likes the mouse and the tiger is blue then the mouse visits the tiger. If someone needs the tiger and they need the mouse then the mouse visits the tiger. Nice people are red.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone needs the mouse then the mouse needs the tiger.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If someone needs the mouse then they like the tiger.
((("someone" "needs" "mouse" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the tiger then they are nice.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the tiger and the tiger is nice then the tiger does not like the mouse.
((("someone" "visits" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "likes" "mouse" "-"))
If the tiger likes the mouse then the tiger does not need the mouse.
((("tiger" "likes" "mouse" "+")) -> ("tiger" "needs" "mouse" "-"))
If the tiger likes the mouse and the tiger is blue then the mouse visits the tiger.
((("tiger" "likes" "mouse" "+") ("tiger" "is" "blue" "+")) -> ("mouse" "visits" "tiger" "+"))
If someone needs the tiger and they need the mouse then the mouse visits the tiger.
((("someone" "needs" "tiger" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
The mouse needs the tiger.
True
1
proof
[(triple7 OR ((triple14) -> rule1))]
("mouse" "needs" "tiger" "+")
triple7
((triple14) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The tiger does not need the mouse.
False
1
inv-proof
[(triple14)]
("tiger" "needs" "mouse" "-")
triple14
The tiger likes the tiger.
True
2
proof
[(((triple14) -> rule2))]
("tiger" "likes" "tiger" "+")
((triple14) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple14) -> rule2))]
("tiger" "likes" "tiger" "-")
((triple14) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple14) -> rule2)) -> rule3))]
("tiger" "is" "nice" "+")
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is not nice.
False
3
inv-proof
[(((((triple14) -> rule2)) -> rule3))]
("tiger" "is" "nice" "-")
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
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 tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is blue.[(triple1)] The mouse is kind.[(triple2)] The mouse is nice.[(triple3 OR ((triple6) -> rule3))] The mouse is red.[(triple4 OR ((triple3) -> rule8) OR ((((triple6) -> rule3)) -> rule8))] The mouse is young.[(triple5)] The mouse likes the tiger.[(triple6)] The mouse needs the tiger.[(triple7 OR ((triple14) -> rule1))] The mouse visits the tiger.[(triple8)] The tiger does not like the mouse.[(triple13 OR ((triple8 ((((triple14) -> rule2)) -> rule3)) -> rule4))] The tiger is blue.[(triple9)] The tiger is kind.[(triple10)] The tiger is red.[(triple11 OR ((((((triple14) -> rule2)) -> rule3)) -> rule8))] The tiger is young.[(triple12)] The tiger needs the mouse.[(triple14)] The tiger visits the mouse.[(triple15)] @1: The tiger likes the tiger.[(((triple14) -> rule2))] @2: The tiger is nice.[(((((triple14) -> rule2)) -> rule3))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
((triple6) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
triple4
((triple3) -> (rule8 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
triple5
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple6
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple7
((triple14) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
triple13
((triple8 ((((triple14) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
((((((triple14) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple14
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple14) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2