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