The dog needs the tiger. The tiger needs the dog. If someone chases the tiger and they like the tiger then they chase the dog. If the dog needs the tiger and the dog is round then the dog chases the tiger. If the dog is blue and the dog is kind then the dog needs the tiger. If someone needs the tiger and the tiger needs the dog then they like the tiger. If someone needs the dog and the dog likes the tiger then the tiger likes the dog. If someone likes the dog then they like the tiger. If someone needs the tiger and the tiger needs the dog then the tiger is round. If the tiger needs the dog and the tiger chases the dog then the tiger is cold.
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone chases the tiger and they like the tiger then they chase the dog.
((("someone" "chases" "tiger" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "chases" "dog" "+"))
If the dog needs the tiger and the dog is round then the dog chases the tiger.
((("dog" "needs" "tiger" "+") ("dog" "is" "round" "+")) -> ("dog" "chases" "tiger" "+"))
If the dog is blue and the dog is kind then the dog needs the tiger.
((("dog" "is" "blue" "+") ("dog" "is" "kind" "+")) -> ("dog" "needs" "tiger" "+"))
If someone needs the tiger and the tiger needs the dog then they like the tiger.
((("someone" "needs" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("someone" "likes" "tiger" "+"))
If someone needs the dog and the dog likes the tiger then the tiger likes the dog.
((("someone" "needs" "dog" "+") ("dog" "likes" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
If someone likes the dog then they like the tiger.
((("someone" "likes" "dog" "+")) -> ("someone" "likes" "tiger" "+"))
If someone needs the tiger and the tiger needs the dog then the tiger is round.
((("someone" "needs" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("tiger" "is" "round" "+"))
If the tiger needs the dog and the tiger chases the dog then the tiger is cold.
((("tiger" "needs" "dog" "+") ("tiger" "chases" "dog" "+")) -> ("tiger" "is" "cold" "+"))
The tiger needs the dog.
True
1
proof
[(triple2)]
("tiger" "needs" "dog" "+")
triple2
The dog does not need the tiger.
False
1
inv-proof
[(triple1)]
("dog" "needs" "tiger" "-")
triple1
The tiger is round.
True
3
proof
[(((triple1 triple2) -> rule7))]
("tiger" "is" "round" "+")
((triple1 triple2) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not round.
False
3
inv-proof
[(((triple1 triple2) -> rule7))]
("tiger" "is" "round" "-")
((triple1 triple2) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the dog.
True
5
proof
[(((triple2 ((triple1 triple2) -> rule4)) -> rule5))]
("tiger" "likes" "dog" "+")
((triple2 ((triple1 triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The tiger does not like the dog.
False
5
inv-proof
[(((triple2 ((triple1 triple2) -> rule4)) -> rule5))]
("tiger" "likes" "dog" "-")
((triple2 ((triple1 triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The tiger likes the tiger.
True
6
proof
[(((((triple2 ((triple1 triple2) -> rule4)) -> rule5)) -> rule6))]
("tiger" "likes" "tiger" "+")
((((triple2 ((triple1 triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int3
The tiger does not like the tiger.
False
6
inv-proof
[(((((triple2 ((triple1 triple2) -> rule4)) -> rule5)) -> rule6))]
("tiger" "likes" "tiger" "-")
((((triple2 ((triple1 triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int3
The tiger is not cold.
Unknown
inv-rconc
[@2: The tiger is cold.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("tiger" "is" "cold" "-")
The dog chases the tiger.
Unknown
rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "tiger" "+")
The tiger does not chase the dog.
Unknown
inv-rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "dog" "-")
The dog chases the dog.
Unknown
rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("dog" "chases" "dog" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog needs the tiger.[(triple1)] The tiger needs the dog.[(triple2)] @1: The dog likes the tiger.[(((triple1 triple2) -> rule4))] The tiger is round.[(((triple1 triple2) -> rule7))] @2: The tiger likes the dog.[(((triple2 ((triple1 triple2) -> rule4)) -> rule5))] @3: The tiger likes the tiger.[(((((triple2 ((triple1 triple2) -> rule4)) -> rule5)) -> rule6))]
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
((triple1 triple2) -> (rule4 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple1 triple2) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple2 ((triple1 triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple2 ((triple1 triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int3