The bear visits the cow. The cow eats the rabbit. The dog visits the bear. The rabbit eats the bear. If something is big then it visits the cow. If something likes the bear then it is round. If something likes the bear then it eats the cow. If something visits the cow then it likes the bear. If something is big and it eats the rabbit then it eats the dog. If the cow eats the rabbit and the rabbit visits the dog then the rabbit visits the bear. All round things are rough. If something is red and it likes the rabbit then the rabbit eats the bear.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
If something is big then it visits the cow.
((("something" "is" "big" "+")) -> ("something" "visits" "cow" "+"))
If something likes the bear then it is round.
((("something" "likes" "bear" "+")) -> ("something" "is" "round" "+"))
If something likes the bear then it eats the cow.
((("something" "likes" "bear" "+")) -> ("something" "eats" "cow" "+"))
If something visits the cow then it likes the bear.
((("something" "visits" "cow" "+")) -> ("something" "likes" "bear" "+"))
If something is big and it eats the rabbit then it eats the dog.
((("something" "is" "big" "+") ("something" "eats" "rabbit" "+")) -> ("something" "eats" "dog" "+"))
If the cow eats the rabbit and the rabbit visits the dog then the rabbit visits the bear.
((("cow" "eats" "rabbit" "+") ("rabbit" "visits" "dog" "+")) -> ("rabbit" "visits" "bear" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is red and it likes the rabbit then the rabbit eats the bear.
((("something" "is" "red" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "eats" "bear" "+"))
The cow eats the rabbit.
True
1
proof
[(triple2)]
("cow" "eats" "rabbit" "+")
triple2
The dog does not visit the bear.
False
1
inv-proof
[(triple3)]
("dog" "visits" "bear" "-")
triple3
The bear likes the bear.
True
2
proof
[(((triple1) -> rule4))]
("bear" "likes" "bear" "+")
((triple1) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear does not like the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "likes" "bear" "-")
((triple1) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is round.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("bear" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear does not eat the cow.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("bear" "eats" "cow" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is rough.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule7))]
("bear" "is" "rough" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear is not rough.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule7))]
("bear" "is" "rough" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear does not eat the dog.
Unknown
inv-rconc
[@1: The bear eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "dog" "-")
The rabbit visits the bear.
Unknown
rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "bear" "+")
The cow does not eat the dog.
Unknown
inv-rconc
[@1: The cow eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "dog" "-")
The rabbit is rough.
Unknown
rconc
[@4: The rabbit is rough.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule4 <- rule1 <- FAIL)]]
("rabbit" "is" "rough" "+")
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 rabbit likes the cow.
Unknown
random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear visits the cow.[(triple1)] The cow eats the rabbit.[(triple2)] The dog visits the bear.[(triple3)] The rabbit eats the bear.[(triple4)] @1: The bear likes the bear.[(((triple1) -> rule4))] @2: The bear eats the cow.[(((((triple1) -> rule4)) -> rule3))] The bear is round.[(((((triple1) -> rule4)) -> rule2))] @3: The bear is rough.[(((((((triple1) -> rule4)) -> rule2)) -> rule7))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
The dog visits the bear.
("dog" "visits" "bear" "+")
triple3
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple4
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple1) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3