The cow visits the tiger. The dog visits the tiger. The rabbit is young. The tiger eats the dog. If the cow is big then the cow is nice. If someone visits the tiger then the tiger visits the cow. If the rabbit visits the dog then the dog is kind. If someone likes the cow then the cow eats the dog. If the cow is red and the cow visits the tiger then the cow visits the rabbit. If the cow is big and the cow eats the rabbit then the cow visits the dog. If someone is young then they like the cow. If someone eats the dog then they visit the dog.
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
If the cow is big then the cow is nice.
((("cow" "is" "big" "+")) -> ("cow" "is" "nice" "+"))
If someone visits the tiger then the tiger visits the cow.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
If the rabbit visits the dog then the dog is kind.
((("rabbit" "visits" "dog" "+")) -> ("dog" "is" "kind" "+"))
If someone likes the cow then the cow eats the dog.
((("someone" "likes" "cow" "+")) -> ("cow" "eats" "dog" "+"))
If the cow is red and the cow visits the tiger then the cow visits the rabbit.
((("cow" "is" "red" "+") ("cow" "visits" "tiger" "+")) -> ("cow" "visits" "rabbit" "+"))
If the cow is big and the cow eats the rabbit then the cow visits the dog.
((("cow" "is" "big" "+") ("cow" "eats" "rabbit" "+")) -> ("cow" "visits" "dog" "+"))
If someone is young then they like the cow.
((("someone" "is" "young" "+")) -> ("someone" "likes" "cow" "+"))
If someone eats the dog then they visit the dog.
((("someone" "eats" "dog" "+")) -> ("someone" "visits" "dog" "+"))
The tiger eats the dog.
True
1
proof
[(triple4)]
("tiger" "eats" "dog" "+")
triple4
The cow does not visit the tiger.
False
1
inv-proof
[(triple1)]
("cow" "visits" "tiger" "-")
triple1
The rabbit likes the cow.
True
2
proof
[(((triple3) -> rule7))]
("rabbit" "likes" "cow" "+")
((triple3) -> (rule7 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The tiger does not visit the cow.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple2) -> rule2))]
("tiger" "visits" "cow" "-")
((triple1) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple2) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow eats the dog.
True
3
proof
[(((((triple3) -> rule7)) -> rule4))]
("cow" "eats" "dog" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int2
The cow does not eat the dog.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule4))]
("cow" "eats" "dog" "-")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int2
The cow visits the dog.
True
4
proof
[(((((((triple3) -> rule7)) -> rule4)) -> rule8))]
("cow" "visits" "dog" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int3
The cow does not visit the dog.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule4)) -> rule8))]
("cow" "visits" "dog" "-")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int3
The cow does not visit the rabbit.
Unknown
inv-rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "rabbit" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "visits" "dog" "+")
The dog does not like the cow.
Unknown
inv-rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "likes" "cow" "-")
The tiger likes the cow.
Unknown
rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "likes" "cow" "+")
The cow does not eat the rabbit.
Unknown
inv-random
[@0: The cow eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "rabbit" "-")
The rabbit eats the cow.
Unknown
random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The cow visits the tiger.[(triple1)] The dog visits the tiger.[(triple2)] The rabbit is young.[(triple3)] The tiger eats the dog.[(triple4)] @1: The rabbit likes the cow.[(((triple3) -> rule7))] The tiger visits the cow.[(((triple1) -> rule2) OR ((triple2) -> rule2))] The tiger visits the dog.[(((triple4) -> rule8))] @2: The cow eats the dog.[(((((triple3) -> rule7)) -> rule4))] @3: The cow visits the dog.[(((((((triple3) -> rule7)) -> rule4)) -> rule8))]
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple4
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
((triple3) -> (rule7 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple1) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple2) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple4) -> (rule8 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int3