The dog needs the tiger. The tiger needs the dog. If someone needs the dog then they like the tiger. If someone likes the dog then they are red. If someone likes the dog then the dog needs the tiger. If someone eats the dog then they like the dog. If someone likes the tiger and they need the dog then the dog eats the tiger. If someone likes the dog and they like the tiger then they eat the tiger.
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone needs the dog then they like the tiger.
((("someone" "needs" "dog" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the dog then they are red.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "red" "+"))
If someone likes the dog then the dog needs the tiger.
((("someone" "likes" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If someone eats the dog then they like the dog.
((("someone" "eats" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If someone likes the tiger and they need the dog then the dog eats the tiger.
((("someone" "likes" "tiger" "+") ("someone" "needs" "dog" "+")) -> ("dog" "eats" "tiger" "+"))
If someone likes the dog and they like the tiger then they eat the tiger.
((("someone" "likes" "dog" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "eats" "tiger" "+"))
The dog needs the tiger.
True
1
proof
[(triple1)]
("dog" "needs" "tiger" "+")
triple1
The dog does not need the tiger.
False
1
inv-proof
[(triple1)]
("dog" "needs" "tiger" "-")
triple1
The tiger likes the tiger.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "likes" "tiger" "-")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "dog" "-")
The tiger eats the tiger.
Unknown
rconc
[@2: The tiger eats the tiger.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The dog needs the tiger.[(triple1)] The tiger needs the dog.[(triple2)] @1: The tiger likes the tiger.[(((triple2) -> rule1))] @2: The dog eats the tiger.[(((((triple2) -> rule1) triple2) -> rule5))]
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2