The dog likes the tiger. The tiger is cold. If something eats the tiger and it likes the tiger then the tiger likes the dog. If the tiger likes the dog then the tiger chases the dog. If something is cold and it eats the dog then it chases the dog. If something eats the tiger and it likes the dog then the tiger likes the dog. If something eats the tiger and the tiger chases the dog then the tiger eats the dog. If something chases the dog then the dog likes the tiger. If something chases the dog then the dog chases the tiger. If something likes the tiger then it eats the tiger.
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something eats the tiger and it likes the tiger then the tiger likes the dog.
((("something" "eats" "tiger" "+") ("something" "likes" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
If the tiger likes the dog then the tiger chases the dog.
((("tiger" "likes" "dog" "+")) -> ("tiger" "chases" "dog" "+"))
If something is cold and it eats the dog then it chases the dog.
((("something" "is" "cold" "+") ("something" "eats" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something eats the tiger and it likes the dog then the tiger likes the dog.
((("something" "eats" "tiger" "+") ("something" "likes" "dog" "+")) -> ("tiger" "likes" "dog" "+"))
If something eats the tiger and the tiger chases the dog then the tiger eats the dog.
((("something" "eats" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("tiger" "eats" "dog" "+"))
If something chases the dog then the dog likes the tiger.
((("something" "chases" "dog" "+")) -> ("dog" "likes" "tiger" "+"))
If something chases the dog then the dog chases the tiger.
((("something" "chases" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If something likes the tiger then it eats the tiger.
((("something" "likes" "tiger" "+")) -> ("something" "eats" "tiger" "+"))
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 dog eats the tiger.
True
2
proof
[(((triple1) -> rule8))]
("dog" "eats" "tiger" "+")
((triple1) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule8))]
("dog" "eats" "tiger" "-")
((triple1) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The tiger likes the dog.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule1))]
("tiger" "likes" "dog" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The tiger does not like the dog.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule1))]
("tiger" "likes" "dog" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The tiger chases the dog.
True
5
proof
[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule2))]
("tiger" "chases" "dog" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The tiger does not chase the dog.
False
5
inv-proof
[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule2))]
("tiger" "chases" "dog" "-")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "dog" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog likes the tiger.[(triple1)] The tiger is cold.[(triple2)] @1: The dog eats the tiger.[(((triple1) -> rule8))] @2: The tiger likes the dog.[(((((triple1) -> rule8) triple1) -> rule1))] @3: The tiger chases the dog.[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule2))] @4: The dog chases the tiger.[(((((((((triple1) -> rule8) triple1) -> rule1)) -> rule2)) -> rule7))] The tiger eats the dog.[(((((triple1) -> rule8) ((((((triple1) -> rule8) triple1) -> rule1)) -> rule2)) -> rule5))]
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple1
The tiger is cold.
("tiger" "is" "cold" "+")
triple2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((triple1) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int4
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((((triple1) -> (rule8 % int4)) ((((((triple1) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int4