The cow is young. The dog needs the rabbit. The rabbit needs the cow. If someone eats the rabbit and the rabbit needs the dog then the rabbit eats the dog. If the cow sees the dog then the cow is kind. If someone needs the rabbit then they see the dog. If someone is kind and big then they see the cow. If the dog eats the rabbit and the rabbit eats the dog then the dog needs the cow. If someone needs the cow then they need the dog. If someone sees the dog then they need the cow. If the cow sees the dog and the cow is kind then the dog eats the cow.
The cow is young.
("cow" "is" "young" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If someone eats the rabbit and the rabbit needs the dog then the rabbit eats the dog.
((("someone" "eats" "rabbit" "+") ("rabbit" "needs" "dog" "+")) -> ("rabbit" "eats" "dog" "+"))
If the cow sees the dog then the cow is kind.
((("cow" "sees" "dog" "+")) -> ("cow" "is" "kind" "+"))
If someone needs the rabbit then they see the dog.
((("someone" "needs" "rabbit" "+")) -> ("someone" "sees" "dog" "+"))
If someone is kind and big then they see the cow.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "sees" "cow" "+"))
If the dog eats the rabbit and the rabbit eats the dog then the dog needs the cow.
((("dog" "eats" "rabbit" "+") ("rabbit" "eats" "dog" "+")) -> ("dog" "needs" "cow" "+"))
If someone needs the cow then they need the dog.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "dog" "+"))
If someone sees the dog then they need the cow.
((("someone" "sees" "dog" "+")) -> ("someone" "needs" "cow" "+"))
If the cow sees the dog and the cow is kind then the dog eats the cow.
((("cow" "sees" "dog" "+") ("cow" "is" "kind" "+")) -> ("dog" "eats" "cow" "+"))
The dog needs the rabbit.
True
1
proof
[(triple2)]
("dog" "needs" "rabbit" "+")
triple2
The rabbit does not need the cow.
False
1
inv-proof
[(triple3)]
("rabbit" "needs" "cow" "-")
triple3
The rabbit needs the dog.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "needs" "dog" "+")
((triple3) -> (rule6 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit does not need the dog.
False
2
inv-proof
[(((triple3) -> rule6))]
("rabbit" "needs" "dog" "-")
((triple3) -> (rule6 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The dog needs the cow.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("dog" "needs" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog does not need the cow.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("dog" "needs" "cow" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog needs the dog.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
("dog" "needs" "dog" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog does not need the dog.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
("dog" "needs" "dog" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The rabbit does not see the dog.
Unknown
inv-rconc
[@1: The rabbit sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "dog" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "sees" "cow" "+")
The cow does not see the dog.
Unknown
inv-rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "dog" "-")
The cow is kind.
Unknown
rconc
[@2: The cow is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("cow" "is" "kind" "+")
The cow does not eat the dog.
Unknown
inv-random
[@0: The cow eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "dog" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The cow is young.[(triple1)] The dog needs the rabbit.[(triple2)] The rabbit needs the cow.[(triple3)] @1: The dog sees the dog.[(((triple2) -> rule3))] The rabbit needs the dog.[(((triple3) -> rule6))] @2: The dog needs the cow.[(((((triple2) -> rule3)) -> rule7))] @3: The dog needs the dog.[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
The cow is young.
("cow" "is" "young" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple3
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple2) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple3) -> (rule6 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3