The dog eats the squirrel. The dog is green. The dog is kind. The dog needs the mouse. The mouse is kind. The mouse is rough. The mouse is round. The squirrel sees the tiger. The tiger is young. The tiger needs the dog. The tiger needs the mouse. The tiger sees the mouse. If the squirrel needs the mouse and the mouse is kind then the mouse is green. Rough people are young. If someone is young then they need the squirrel. If the dog sees the mouse and the dog needs the squirrel then the mouse needs the dog. If someone needs the squirrel then they eat the tiger. If someone sees the tiger and they need the tiger then the tiger needs the squirrel.
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the squirrel needs the mouse and the mouse is kind then the mouse is green.
((("squirrel" "needs" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "is" "green" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they need the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "needs" "squirrel" "+"))
If the dog sees the mouse and the dog needs the squirrel then the mouse needs the dog.
((("dog" "sees" "mouse" "+") ("dog" "needs" "squirrel" "+")) -> ("mouse" "needs" "dog" "+"))
If someone needs the squirrel then they eat the tiger.
((("someone" "needs" "squirrel" "+")) -> ("someone" "eats" "tiger" "+"))
If someone sees the tiger and they need the tiger then the tiger needs the squirrel.
((("someone" "sees" "tiger" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "needs" "squirrel" "+"))
The tiger sees the mouse.
True
1
proof
[(triple12)]
("tiger" "sees" "mouse" "+")
triple12
The dog does not need the mouse.
False
1
inv-proof
[(triple4)]
("dog" "needs" "mouse" "-")
triple4
The tiger needs the squirrel.
True
2
proof
[(((triple9) -> rule3))]
("tiger" "needs" "squirrel" "+")
((triple9) -> (rule3 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple6) -> rule2))]
("mouse" "is" "young" "-")
((triple6) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger eats the tiger.
True
3
proof
[(((((triple9) -> rule3)) -> rule5))]
("tiger" "eats" "tiger" "+")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int2
The tiger does not eat the tiger.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule5))]
("tiger" "eats" "tiger" "-")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int2
The mouse eats the tiger.
True
4
proof
[(((((((triple6) -> rule2)) -> rule3)) -> rule5))]
("mouse" "eats" "tiger" "+")
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse does not eat the tiger.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule3)) -> rule5))]
("mouse" "eats" "tiger" "-")
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "young" "-")
The mouse is green.
Unknown
rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "green" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@2: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The dog eats the tiger.
Unknown
rconc
[@3: The dog eats the tiger.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule2 <- FAIL)]]
("dog" "eats" "tiger" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The squirrel needs the tiger.
Unknown
random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "+")
The squirrel does not eat the mouse.
Unknown
inv-random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The dog eats the squirrel.[(triple1)] The dog is green.[(triple2)] The dog is kind.[(triple3)] The dog needs the mouse.[(triple4)] The mouse is kind.[(triple5)] The mouse is rough.[(triple6)] The mouse is round.[(triple7)] The squirrel sees the tiger.[(triple8)] The tiger is young.[(triple9)] The tiger needs the dog.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger sees the mouse.[(triple12)] @1: The mouse is young.[(((triple6) -> rule2))] The tiger needs the squirrel.[(((triple9) -> rule3))] @2: The mouse needs the squirrel.[(((((triple6) -> rule2)) -> rule3))] The tiger eats the tiger.[(((((triple9) -> rule3)) -> rule5))] @3: The mouse eats the tiger.[(((((((triple6) -> rule2)) -> rule3)) -> rule5))]
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse is round.
("mouse" "is" "round" "+")
triple7
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple8
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
((triple6) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
((triple9) -> (rule3 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((((((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3