The cow is big. The cow needs the dog. The dog sees the rabbit. The rabbit chases the cow. The rabbit chases the dog. The rabbit is big. The rabbit sees the dog. If the cow is blue and the cow needs the rabbit then the cow needs the dog. If the cow chases the dog then the cow sees the rabbit. If something is big then it chases the dog.
The cow is big.
("cow" "is" "big" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If the cow is blue and the cow needs the rabbit then the cow needs the dog.
((("cow" "is" "blue" "+") ("cow" "needs" "rabbit" "+")) -> ("cow" "needs" "dog" "+"))
If the cow chases the dog then the cow sees the rabbit.
((("cow" "chases" "dog" "+")) -> ("cow" "sees" "rabbit" "+"))
If something is big then it chases the dog.
((("something" "is" "big" "+")) -> ("something" "chases" "dog" "+"))
The cow is big.
True
1
proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The dog does not see the rabbit.
False
1
inv-proof
[(triple3)]
("dog" "sees" "rabbit" "-")
triple3
The cow chases the dog.
True
2
proof
[(((triple1) -> rule3))]
("cow" "chases" "dog" "+")
((triple1) -> (rule3 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "chases" "dog" "-")
((triple1) -> (rule3 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow sees the rabbit.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("cow" "sees" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The cow does not see the rabbit.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("cow" "sees" "rabbit" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "dog" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The cow chases the rabbit.
Unknown
random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cow is big.[(triple1)] The cow needs the dog.[(triple2)] The dog sees the rabbit.[(triple3)] The rabbit chases the cow.[(triple4)] The rabbit chases the dog.[(triple5 OR ((triple6) -> rule3))] The rabbit is big.[(triple6)] The rabbit sees the dog.[(triple7)] @1: The cow chases the dog.[(((triple1) -> rule3))] @2: The cow sees the rabbit.[(((((triple1) -> rule3)) -> rule2))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple5
((triple6) -> (rule3 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple7
The cow chases the dog.
("cow" "chases" "dog" "+")
((triple1) -> (rule3 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2