The cow chases the rabbit. The cow is big. The cow is nice. The dog chases the cow. The dog chases the rabbit. The dog needs the rabbit. The rabbit eats the dog. The rabbit is big. The rabbit is nice. The rabbit needs the dog. If the dog eats the cow then the dog is nice. If someone is red and they need the cow then the cow is round. If someone chases the rabbit then the rabbit chases the cow. If someone is big then they chase the rabbit. All young people are big. If someone chases the rabbit then the rabbit eats the cow. If someone needs the dog then the dog eats the rabbit. If the dog is red and the dog eats the rabbit then the dog chases the rabbit.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If the dog eats the cow then the dog is nice.
((("dog" "eats" "cow" "+")) -> ("dog" "is" "nice" "+"))
If someone is red and they need the cow then the cow is round.
((("someone" "is" "red" "+") ("someone" "needs" "cow" "+")) -> ("cow" "is" "round" "+"))
If someone chases the rabbit then the rabbit chases the cow.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If someone is big then they chase the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "chases" "rabbit" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone chases the rabbit then the rabbit eats the cow.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If someone needs the dog then the dog eats the rabbit.
((("someone" "needs" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
If the dog is red and the dog eats the rabbit then the dog chases the rabbit.
((("dog" "is" "red" "+") ("dog" "eats" "rabbit" "+")) -> ("dog" "chases" "rabbit" "+"))
The dog needs the rabbit.
True
1
proof
[(triple6)]
("dog" "needs" "rabbit" "+")
triple6
The rabbit is not big.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "big" "-")
triple8
The rabbit eats the cow.
True
2
proof
[(((triple1) -> rule6) OR ((triple5) -> rule6) OR ((((triple2) -> rule4)) -> rule6) OR ((((triple8) -> rule4)) -> rule6))]
("rabbit" "eats" "cow" "+")
((triple1) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((triple5) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule6) OR ((triple5) -> rule6) OR ((((triple2) -> rule4)) -> rule6) OR ((((triple8) -> rule4)) -> rule6))]
("rabbit" "eats" "cow" "-")
((triple1) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((triple5) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "big" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "nice" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The cow chases the rabbit.[(triple1 OR ((triple2) -> rule4))] The cow is big.[(triple2)] The cow is nice.[(triple3)] The dog chases the cow.[(triple4)] The dog chases the rabbit.[(triple5)] The dog needs the rabbit.[(triple6)] The rabbit eats the dog.[(triple7)] The rabbit is big.[(triple8)] The rabbit is nice.[(triple9)] The rabbit needs the dog.[(triple10)] @1: The dog eats the rabbit.[(((triple10) -> rule7))] The rabbit chases the cow.[(((triple1) -> rule3) OR ((triple5) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((triple8) -> rule4)) -> rule3))] The rabbit chases the rabbit.[(((triple8) -> rule4))] The rabbit eats the cow.[(((triple1) -> rule6) OR ((triple5) -> rule6) OR ((((triple2) -> rule4)) -> rule6) OR ((((triple8) -> rule4)) -> rule6))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
((triple2) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The dog chases the cow.
("dog" "chases" "cow" "+")
triple4
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple5
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple6
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple10
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple10) -> (rule7 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple1) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
((triple5) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple8) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((triple1) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((triple5) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2