The dog visits the mouse. The lion does not need the tiger. The lion sees the mouse. The lion visits the dog. The lion does not visit the tiger. The mouse needs the tiger. The mouse sees the tiger. The mouse visits the lion. The tiger is green. The tiger needs the dog. If the dog sees the tiger then the dog does not see the lion. If someone visits the tiger and they do not need the lion then they are not young. If someone is young and they need the dog then they see the mouse. If someone needs the mouse then the mouse is blue. If someone sees the dog and they visit the dog then the dog sees the mouse. If someone sees the tiger then the tiger is young.
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion does not need the tiger.
("lion" "needs" "tiger" "-")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If the dog sees the tiger then the dog does not see the lion.
((("dog" "sees" "tiger" "+")) -> ("dog" "sees" "lion" "-"))
If someone visits the tiger and they do not need the lion then they are not young.
((("someone" "visits" "tiger" "+") ("someone" "needs" "lion" "~")) -> ("someone" "is" "young" "-"))
If someone is young and they need the dog then they see the mouse.
((("someone" "is" "young" "+") ("someone" "needs" "dog" "+")) -> ("someone" "sees" "mouse" "+"))
If someone needs the mouse then the mouse is blue.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone sees the dog and they visit the dog then the dog sees the mouse.
((("someone" "sees" "dog" "+") ("someone" "visits" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
If someone sees the tiger then the tiger is young.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "young" "+"))
The tiger needs the dog.
True
1
proof
[(triple10)]
("tiger" "needs" "dog" "+")
triple10
The dog does not visit the mouse.
False
1
inv-proof
[(triple1)]
("dog" "visits" "mouse" "-")
triple1
The tiger is young.
True
2
proof
[(((triple7) -> rule6))]
("tiger" "is" "young" "+")
((triple7) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple7) -> rule6))]
("tiger" "is" "young" "-")
((triple7) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger sees the mouse.
True
4
proof
[(((((triple7) -> rule6) triple10) -> rule3))]
("tiger" "sees" "mouse" "+")
((((triple7) -> (rule6 % int2)) triple10) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger does not see the mouse.
False
4
inv-proof
[(((((triple7) -> rule6) triple10) -> rule3))]
("tiger" "sees" "mouse" "-")
((((triple7) -> (rule6 % int2)) triple10) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "blue" "+")
The dog does not see the mouse.
Unknown
inv-rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "mouse" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
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 is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The dog visits the mouse.[(triple1)] The lion does not need the tiger.[(triple2)] The lion does not visit the tiger.[(triple5)] The lion sees the mouse.[(triple3)] The lion visits the dog.[(triple4)] The mouse needs the tiger.[(triple6)] The mouse sees the tiger.[(triple7)] The mouse visits the lion.[(triple8)] The tiger is green.[(triple9)] The tiger needs the dog.[(triple10)] @1: The tiger is young.[(((triple7) -> rule6))] @2: The tiger sees the mouse.[(((((triple7) -> rule6) triple10) -> rule3))]
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple1
The lion does not need the tiger.
("lion" "needs" "tiger" "-")
triple2
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
triple5
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The lion visits the dog.
("lion" "visits" "dog" "+")
triple4
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
((triple7) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((((triple7) -> (rule6 % int2)) triple10) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2