The bear visits the cow. The cow sees the bear. The dog visits the rabbit. The rabbit is big. If the dog visits the rabbit then the dog chases the cow. If the dog chases the cow then the cow sees the dog.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If the dog visits the rabbit then the dog chases the cow.
((("dog" "visits" "rabbit" "+")) -> ("dog" "chases" "cow" "+"))
If the dog chases the cow then the cow sees the dog.
((("dog" "chases" "cow" "+")) -> ("cow" "sees" "dog" "+"))
The cow sees the bear.
True
1
proof
[(triple2)]
("cow" "sees" "bear" "+")
triple2
The rabbit is not big.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "big" "-")
triple4
The dog chases the cow.
True
2
proof
[(((triple3) -> rule1))]
("dog" "chases" "cow" "+")
((triple3) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog does not chase the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "chases" "cow" "-")
((triple3) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The cow sees the dog.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("cow" "sees" "dog" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The cow does not see the dog.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("cow" "sees" "dog" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The rabbit does not see the dog.
Unknown
inv-random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "-")
The bear sees the rabbit.
Unknown
random
[@0: The bear sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "rabbit" "+")
The cow does not chase the rabbit.
Unknown
inv-random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The bear chases the rabbit.
Unknown
random
[@0: The bear chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "rabbit" "+")
@0: The bear visits the cow.[(triple1)] The cow sees the bear.[(triple2)] The dog visits the rabbit.[(triple3)] The rabbit is big.[(triple4)] @1: The dog chases the cow.[(((triple3) -> rule1))] @2: The cow sees the dog.[(((((triple3) -> rule1)) -> rule2))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple2
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple3) -> (rule1 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2