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