The bear visits the cow. The cow does not eat the dog. The cow is round. The dog eats the cow. The dog is not green. The rabbit is green. The rabbit visits the bear. If someone is young then they visit the dog. If someone visits the bear then they are young. If someone sees the cow then the cow is not green. If someone visits the dog and they are green then the dog visits the bear. If someone is round and they do not eat the dog then the dog sees the bear. If the dog is green then the dog does not see the bear. If someone visits the cow and they are green then they do not eat the cow. If someone eats the rabbit then they do not eat the cow. If the rabbit eats the dog and the rabbit is round then the dog sees the cow.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow does not eat the dog.
("cow" "eats" "dog" "-")
The cow is round.
("cow" "is" "round" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is not green.
("dog" "is" "green" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
If someone is young then they visit the dog.
((("someone" "is" "young" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the bear then they are young.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "young" "+"))
If someone sees the cow then the cow is not green.
((("someone" "sees" "cow" "+")) -> ("cow" "is" "green" "-"))
If someone visits the dog and they are green then the dog visits the bear.
((("someone" "visits" "dog" "+") ("someone" "is" "green" "+")) -> ("dog" "visits" "bear" "+"))
If someone is round and they do not eat the dog then the dog sees the bear.
((("someone" "is" "round" "+") ("someone" "eats" "dog" "~")) -> ("dog" "sees" "bear" "+"))
If the dog is green then the dog does not see the bear.
((("dog" "is" "green" "+")) -> ("dog" "sees" "bear" "-"))
If someone visits the cow and they are green then they do not eat the cow.
((("someone" "visits" "cow" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "cow" "-"))
If someone eats the rabbit then they do not eat the cow.
((("someone" "eats" "rabbit" "+")) -> ("someone" "eats" "cow" "-"))
If the rabbit eats the dog and the rabbit is round then the dog sees the cow.
((("rabbit" "eats" "dog" "+") ("rabbit" "is" "round" "+")) -> ("dog" "sees" "cow" "+"))
The rabbit visits the bear.
True
1
proof
[(triple7)]
("rabbit" "visits" "bear" "+")
triple7
The cow is not round.
False
1
inv-proof
[(triple3)]
("cow" "is" "round" "-")
triple3
The dog sees the bear.
True
3
proof
[(((triple3 triple2) -> rule5))]
("dog" "sees" "bear" "+")
((triple3 triple2) -> (rule5 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog does not see the bear.
False
3
inv-proof
[(((triple3 triple2) -> rule5))]
("dog" "sees" "bear" "-")
((triple3 triple2) -> (rule5 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The rabbit visits the dog.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("rabbit" "visits" "dog" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not visit the dog.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("rabbit" "visits" "dog" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The dog visits the bear.
True
5
proof
[(((((((triple7) -> rule2)) -> rule1) triple6) -> rule4))]
("dog" "visits" "bear" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The dog does not visit the bear.
False
5
inv-proof
[(((((((triple7) -> rule2)) -> rule1) triple6) -> rule4))]
("dog" "visits" "bear" "-")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The dog is young.
True
6
proof
[(((((((((triple7) -> rule2)) -> rule1) triple6) -> rule4)) -> rule2))]
("dog" "is" "young" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3)) triple6) -> (rule4 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
int4
The dog is not young.
False
6
inv-proof
[(((((((((triple7) -> rule2)) -> rule1) triple6) -> rule4)) -> rule2))]
("dog" "is" "young" "-")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3)) triple6) -> (rule4 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
int4
The dog visits the dog.
True
7
proof
[(((((((((((triple7) -> rule2)) -> rule1) triple6) -> rule4)) -> rule2)) -> rule1))]
("dog" "visits" "dog" "+")
((((((((((triple7) -> (rule2 % int5))) -> (rule1 % int4)) triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int4
The rabbit is young.
("rabbit" "is" "young" "+")
int5
The dog does not visit the dog.
False
7
inv-proof
[(((((((((((triple7) -> rule2)) -> rule1) triple6) -> rule4)) -> rule2)) -> rule1))]
("dog" "visits" "dog" "-")
((((((((((triple7) -> (rule2 % int5))) -> (rule1 % int4)) triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int4
The rabbit is young.
("rabbit" "is" "young" "+")
int5
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "-")
The bear is young.
Unknown
rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "young" "+")
The bear does not visit the dog.
Unknown
inv-rconc
[@2: The bear visits the dog.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bear" "visits" "dog" "-")
The cow visits the dog.
Unknown
rconc
[@2: The cow visits the dog.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("cow" "visits" "dog" "+")
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("dog" "sees" "cow" "-")
The rabbit visits the cow.
Unknown
random
[@0: The rabbit visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cow" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The rabbit eats the bear.
Unknown
random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
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 rabbit sees the dog.
Unknown
random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "+")
@0: The bear visits the cow.[(triple1)] The cow does not eat the dog.[(triple2)] The cow is round.[(triple3)] The dog eats the cow.[(triple4)] The dog is not green.[(triple5)] The rabbit is green.[(triple6)] The rabbit visits the bear.[(triple7)] @1: The dog sees the bear.[(((triple3 triple2) -> rule5))] The rabbit is young.[(((triple7) -> rule2))] @2: The rabbit visits the dog.[(((((triple7) -> rule2)) -> rule1))] @3: The dog visits the bear.[(((((((triple7) -> rule2)) -> rule1) triple6) -> rule4))] @4: The dog is young.[(((((((((triple7) -> rule2)) -> rule1) triple6) -> rule4)) -> rule2))] @5: The dog visits the dog.[(((((((((((triple7) -> rule2)) -> rule1) triple6) -> rule4)) -> rule2)) -> rule1))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cow does not eat the dog.
("cow" "eats" "dog" "-")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The dog eats the cow.
("dog" "eats" "cow" "+")
triple4
The dog is not green.
("dog" "is" "green" "-")
triple5
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple7
The dog sees the bear.
("dog" "sees" "bear" "+")
((triple3 triple2) -> (rule5 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple7) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The dog is young.
("dog" "is" "young" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3)) triple6) -> (rule4 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
int4
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((((((triple7) -> (rule2 % int5))) -> (rule1 % int4)) triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int4
The rabbit is young.
("rabbit" "is" "young" "+")
int5