The dog is kind. The dog is round. The dog needs the tiger. The mouse likes the dog. The mouse likes the tiger. The mouse needs the tiger. The mouse sees the tiger. The tiger is blue. The tiger is kind. The tiger is round. The tiger likes the dog. The tiger likes the mouse. The tiger needs the dog. The tiger needs the mouse. The tiger sees the dog. If the mouse is rough and the mouse sees the tiger then the tiger sees the dog. If someone sees the mouse then the mouse is kind. If someone needs the dog then they like the mouse. If someone likes the dog and the dog sees the tiger then the dog is round. If someone needs the tiger and the tiger sees the dog then the tiger likes the mouse. If someone is kind then they see the mouse.
The dog is kind.
("dog" "is" "kind" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If the mouse is rough and the mouse sees the tiger then the tiger sees the dog.
((("mouse" "is" "rough" "+") ("mouse" "sees" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If someone sees the mouse then the mouse is kind.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If someone needs the dog then they like the mouse.
((("someone" "needs" "dog" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the dog and the dog sees the tiger then the dog is round.
((("someone" "likes" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("dog" "is" "round" "+"))
If someone needs the tiger and the tiger sees the dog then the tiger likes the mouse.
((("someone" "needs" "tiger" "+") ("tiger" "sees" "dog" "+")) -> ("tiger" "likes" "mouse" "+"))
If someone is kind then they see the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "mouse" "+"))
The tiger likes the dog.
True
1
proof
[(triple11)]
("tiger" "likes" "dog" "+")
triple11
The dog is not round.
False
1
inv-proof
[(triple2)]
("dog" "is" "round" "-")
triple2
The dog sees the mouse.
True
2
proof
[(((triple1) -> rule6))]
("dog" "sees" "mouse" "+")
((triple1) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The tiger does not see the mouse.
False
2
inv-proof
[(((triple9) -> rule6))]
("tiger" "sees" "mouse" "-")
((triple9) -> (rule6 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse is kind.
True
3
proof
[(((((triple1) -> rule6)) -> rule2) OR ((((triple9) -> rule6)) -> rule2))]
("mouse" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse is not kind.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2) OR ((((triple9) -> rule6)) -> rule2))]
("mouse" "is" "kind" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse sees the mouse.
True
4
proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule6) OR ((((((triple9) -> rule6)) -> rule2)) -> rule6))]
("mouse" "sees" "mouse" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse does not see the mouse.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule2)) -> rule6) OR ((((((triple9) -> rule6)) -> rule2)) -> rule6))]
("mouse" "sees" "mouse" "-")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The dog does not like the mouse.
Unknown
inv-rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog sees the tiger.
Unknown
random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The dog is kind.[(triple1)] The dog is round.[(triple2)] The dog needs the tiger.[(triple3)] The mouse likes the dog.[(triple4)] The mouse likes the tiger.[(triple5)] The mouse needs the tiger.[(triple6)] The mouse sees the tiger.[(triple7)] The tiger is blue.[(triple8)] The tiger is kind.[(triple9)] The tiger is round.[(triple10)] The tiger likes the dog.[(triple11)] The tiger likes the mouse.[(triple12 OR ((triple13) -> rule3) OR ((triple3 triple15) -> rule5) OR ((triple6 triple15) -> rule5))] The tiger needs the dog.[(triple13)] The tiger needs the mouse.[(triple14)] The tiger sees the dog.[(triple15)] @1: The dog sees the mouse.[(((triple1) -> rule6))] The tiger sees the mouse.[(((triple9) -> rule6))] @2: The mouse is kind.[(((((triple1) -> rule6)) -> rule2) OR ((((triple9) -> rule6)) -> rule2))] @3: The mouse sees the mouse.[(((((((triple1) -> rule6)) -> rule2)) -> rule6) OR ((((((triple9) -> rule6)) -> rule2)) -> rule6))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple11
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple12
((triple13) -> (rule3 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
((triple3 triple15) -> (rule5 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
((triple6 triple15) -> (rule5 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple13
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple1) -> (rule6 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple9) -> (rule6 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3