The bear eats the cat. The cat eats the dog. The dog is blue. The tiger is blue. If the tiger is blue then the tiger eats the bear. If something visits the cat and it eats the dog then the cat is young. If the dog likes the bear and the dog is rough then the bear is nice. If something is big then it visits the cat. If something visits the tiger then it is young. If something is nice then it is rough. If something eats the bear then the bear visits the tiger. If something is nice then it likes the tiger.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If the tiger is blue then the tiger eats the bear.
((("tiger" "is" "blue" "+")) -> ("tiger" "eats" "bear" "+"))
If something visits the cat and it eats the dog then the cat is young.
((("something" "visits" "cat" "+") ("something" "eats" "dog" "+")) -> ("cat" "is" "young" "+"))
If the dog likes the bear and the dog is rough then the bear is nice.
((("dog" "likes" "bear" "+") ("dog" "is" "rough" "+")) -> ("bear" "is" "nice" "+"))
If something is big then it visits the cat.
((("something" "is" "big" "+")) -> ("something" "visits" "cat" "+"))
If something visits the tiger then it is young.
((("something" "visits" "tiger" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something eats the bear then the bear visits the tiger.
((("something" "eats" "bear" "+")) -> ("bear" "visits" "tiger" "+"))
If something is nice then it likes the tiger.
((("something" "is" "nice" "+")) -> ("something" "likes" "tiger" "+"))
The cat eats the dog.
True
1
proof
[(triple2)]
("cat" "eats" "dog" "+")
triple2
The cat does not eat the dog.
False
1
inv-proof
[(triple2)]
("cat" "eats" "dog" "-")
triple2
The tiger eats the bear.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "eats" "bear" "+")
((triple4) -> (rule1 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger does not eat the bear.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "eats" "bear" "-")
((triple4) -> (rule1 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The bear visits the tiger.
True
3
proof
[(((((triple4) -> rule1)) -> rule7))]
("bear" "visits" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The bear does not visit the tiger.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule7))]
("bear" "visits" "tiger" "-")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The bear is young.
True
4
proof
[(((((((triple4) -> rule1)) -> rule7)) -> rule5))]
("bear" "is" "young" "+")
((((((triple4) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int3
The bear is not young.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule7)) -> rule5))]
("bear" "is" "young" "-")
((((((triple4) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int3
The bear does not visit the cat.
Unknown
inv-rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "cat" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "rough" "+")
The dog does not visit the cat.
Unknown
inv-rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "cat" "-")
The cat is young.
Unknown
rconc
[@2: The cat is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("cat" "is" "young" "+")
The dog does not eat the bear.
Unknown
inv-random
[@0: The dog eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "bear" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The tiger does not like the dog.
Unknown
inv-random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "-")
The tiger likes the cat.
Unknown
random
[@0: The tiger likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cat" "+")
@0: The bear eats the cat.[(triple1)] The cat eats the dog.[(triple2)] The dog is blue.[(triple3)] The tiger is blue.[(triple4)] @1: The tiger eats the bear.[(((triple4) -> rule1))] @2: The bear visits the tiger.[(((((triple4) -> rule1)) -> rule7))] @3: The bear is young.[(((((((triple4) -> rule1)) -> rule7)) -> rule5))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The cat eats the dog.
("cat" "eats" "dog" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The tiger eats the bear.
("tiger" "eats" "bear" "+")
((triple4) -> (rule1 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
((((((triple4) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int3