The cat is nice. The cat is red. The cat likes the tiger. The cat sees the dog. The dog likes the cat. The dog needs the lion. The lion needs the cat. The lion sees the cat. The tiger is nice. The tiger is red. The tiger is young. The tiger likes the cat. The tiger likes the lion. The tiger needs the lion. The tiger sees the dog. If something is red then it needs the cat. If something is young and it needs the cat then it needs the tiger. If something needs the cat and it is nice then it is young.
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something is red then it needs the cat.
((("something" "is" "red" "+")) -> ("something" "needs" "cat" "+"))
If something is young and it needs the cat then it needs the tiger.
((("something" "is" "young" "+") ("something" "needs" "cat" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the cat and it is nice then it is young.
((("something" "needs" "cat" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
The tiger is red.
True
1
proof
[(triple10)]
("tiger" "is" "red" "+")
triple10
The tiger does not see the dog.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "dog" "-")
triple15
The tiger needs the cat.
True
2
proof
[(((triple10) -> rule1))]
("tiger" "needs" "cat" "+")
((triple10) -> (rule1 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "needs" "cat" "-")
((triple2) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is young.
True
4
proof
[(((((triple2) -> rule1) triple1) -> rule3))]
("cat" "is" "young" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The tiger does not need the tiger.
False
4
inv-proof
[(((triple11 ((triple10) -> rule1)) -> rule2) OR ((((((triple10) -> rule1) triple9) -> rule3) ((triple10) -> rule1)) -> rule2))]
("tiger" "needs" "tiger" "-")
((triple11 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
((((((triple10) -> (rule1 % int3)) triple9) -> (rule3 % int2)) ((triple10) -> (rule1 % int3))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat needs the tiger.
True
7
proof
[(((((((triple2) -> rule1) triple1) -> rule3) ((triple2) -> rule1)) -> rule2))]
("cat" "needs" "tiger" "+")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat does not need the tiger.
False
7
inv-proof
[(((((((triple2) -> rule1) triple1) -> rule3) ((triple2) -> rule1)) -> rule2))]
("cat" "needs" "tiger" "-")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "young" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "young" "+")
The dog does not need the tiger.
Unknown
inv-rconc
[@2: The dog needs the tiger.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("dog" "needs" "tiger" "-")
The lion needs the tiger.
Unknown
rconc
[@2: The lion needs the tiger.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("lion" "needs" "tiger" "+")
The lion does not need the dog.
Unknown
inv-random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
@0: The cat is nice.[(triple1)] The cat is red.[(triple2)] The cat likes the tiger.[(triple3)] The cat sees the dog.[(triple4)] The dog likes the cat.[(triple5)] The dog needs the lion.[(triple6)] The lion needs the cat.[(triple7)] The lion sees the cat.[(triple8)] The tiger is nice.[(triple9)] The tiger is red.[(triple10)] The tiger is young.[(triple11 OR ((((triple10) -> rule1) triple9) -> rule3))] The tiger likes the cat.[(triple12)] The tiger likes the lion.[(triple13)] The tiger needs the lion.[(triple14)] The tiger sees the dog.[(triple15)] @1: The cat needs the cat.[(((triple2) -> rule1))] The tiger needs the cat.[(((triple10) -> rule1))] @2: The cat is young.[(((((triple2) -> rule1) triple1) -> rule3))] The tiger needs the tiger.[(((triple11 ((triple10) -> rule1)) -> rule2) OR ((((((triple10) -> rule1) triple9) -> rule3) ((triple10) -> rule1)) -> rule2))] @3: The cat needs the tiger.[(((((((triple2) -> rule1) triple1) -> rule3) ((triple2) -> rule1)) -> rule2))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The dog likes the cat.
("dog" "likes" "cat" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The lion sees the cat.
("lion" "sees" "cat" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple11
((((triple10) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple12
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((triple10) -> (rule1 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple11 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
((((((triple10) -> (rule1 % int3)) triple9) -> (rule3 % int2)) ((triple10) -> (rule1 % int3))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3