The dog sees the tiger. The tiger needs the dog. If someone needs the tiger then they are young. If someone sees the tiger and the tiger needs the dog then the tiger likes the dog. If someone needs the dog and the dog sees the tiger then they see the dog. If the tiger likes the dog then the tiger is nice. If the tiger sees the dog and the dog needs the tiger then the tiger is big. If someone is nice and they like the dog then they do not see the tiger.
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone needs the tiger then they are young.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone sees the tiger and the tiger needs the dog then the tiger likes the dog.
((("someone" "sees" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("tiger" "likes" "dog" "+"))
If someone needs the dog and the dog sees the tiger then they see the dog.
((("someone" "needs" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("someone" "sees" "dog" "+"))
If the tiger likes the dog then the tiger is nice.
((("tiger" "likes" "dog" "+")) -> ("tiger" "is" "nice" "+"))
If the tiger sees the dog and the dog needs the tiger then the tiger is big.
((("tiger" "sees" "dog" "+") ("dog" "needs" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If someone is nice and they like the dog then they do not see the tiger.
((("someone" "is" "nice" "+") ("someone" "likes" "dog" "+")) -> ("someone" "sees" "tiger" "-"))
The tiger needs the dog.
True
1
proof
[(triple2)]
("tiger" "needs" "dog" "+")
triple2
The tiger does not need the dog.
False
1
inv-proof
[(triple2)]
("tiger" "needs" "dog" "-")
triple2
The tiger sees the dog.
True
3
proof
[(((triple2 triple1) -> rule3))]
("tiger" "sees" "dog" "+")
((triple2 triple1) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger does not like the dog.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("tiger" "likes" "dog" "-")
((triple1 triple2) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger is nice.
True
4
proof
[(((((triple1 triple2) -> rule2)) -> rule4))]
("tiger" "is" "nice" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is not nice.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule4))]
("tiger" "is" "nice" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger does not see the tiger.
True
8
proof
[(((((((triple1 triple2) -> rule2)) -> rule4) ((triple1 triple2) -> rule2)) -> rule6))]
("tiger" "sees" "tiger" "-")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule6 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The tiger sees the tiger.
False
8
inv-proof
[(((((((triple1 triple2) -> rule2)) -> rule4) ((triple1 triple2) -> rule2)) -> rule6))]
("tiger" "sees" "tiger" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule6 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "young" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "big" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "dog" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "young" "+")
The dog does not need the tiger.
Unknown
inv-random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog sees the tiger.[(triple1)] The tiger needs the dog.[(triple2)] @1: The tiger likes the dog.[(((triple1 triple2) -> rule2))] The tiger sees the dog.[(((triple2 triple1) -> rule3))] @2: The tiger is nice.[(((((triple1 triple2) -> rule2)) -> rule4))] @3: The tiger does not see the tiger.[(((((((triple1 triple2) -> rule2)) -> rule4) ((triple1 triple2) -> rule2)) -> rule6))]
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple1 triple2) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple2 triple1) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule6 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3