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