The bear chases the rabbit. The cat needs the rabbit. The dog chases the cat. The dog is big. The dog is cold. The rabbit eats the cat. The rabbit does not need the cat. If something eats the bear then it eats the rabbit. If something eats the dog then it chases the bear. If something chases the bear then the bear needs the rabbit. If something needs the rabbit then it eats the dog. If something is big and it eats the dog then it does not chase the dog. If the rabbit chases the bear then the rabbit needs the dog. If something is cold and not big then it does not eat the bear. If the bear chases the cat and the bear chases the dog then the dog does not need the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
If something eats the bear then it eats the rabbit.
((("something" "eats" "bear" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the dog then it chases the bear.
((("something" "eats" "dog" "+")) -> ("something" "chases" "bear" "+"))
If something chases the bear then the bear needs the rabbit.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "rabbit" "+"))
If something needs the rabbit then it eats the dog.
((("something" "needs" "rabbit" "+")) -> ("something" "eats" "dog" "+"))
If something is big and it eats the dog then it does not chase the dog.
((("something" "is" "big" "+") ("something" "eats" "dog" "+")) -> ("something" "chases" "dog" "-"))
If the rabbit chases the bear then the rabbit needs the dog.
((("rabbit" "chases" "bear" "+")) -> ("rabbit" "needs" "dog" "+"))
If something is cold and not big then it does not eat the bear.
((("something" "is" "cold" "+") ("something" "is" "big" "~")) -> ("something" "eats" "bear" "-"))
If the bear chases the cat and the bear chases the dog then the dog does not need the bear.
((("bear" "chases" "cat" "+") ("bear" "chases" "dog" "+")) -> ("dog" "needs" "bear" "-"))
The cat needs the rabbit.
True
1
proof
[(triple2)]
("cat" "needs" "rabbit" "+")
triple2
The rabbit does not eat the cat.
False
1
inv-proof
[(triple6)]
("rabbit" "eats" "cat" "-")
triple6
The cat eats the dog.
True
2
proof
[(((triple2) -> rule4))]
("cat" "eats" "dog" "+")
((triple2) -> (rule4 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat does not eat the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "eats" "dog" "-")
((triple2) -> (rule4 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat chases the bear.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("cat" "chases" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The cat does not chase the bear.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("cat" "chases" "bear" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The bear needs the rabbit.
True
4
proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule3))]
("bear" "needs" "rabbit" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The bear does not need the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule3))]
("bear" "needs" "rabbit" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The bear eats the dog.
True
5
proof
[(((((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule4))]
("bear" "eats" "dog" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The bear does not eat the dog.
False
5
inv-proof
[(((((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule4))]
("bear" "eats" "dog" "-")
((((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The bear chases the bear.
True
6
proof
[(((((((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule4)) -> rule2))]
("bear" "chases" "bear" "+")
((((((((((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The cat chases the bear.
("cat" "chases" "bear" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The bear does not chase the bear.
False
6
inv-proof
[(((((((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule4)) -> rule2))]
("bear" "chases" "bear" "-")
((((((((((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The cat chases the bear.
("cat" "chases" "bear" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5
The cat does not eat the rabbit.
Unknown
inv-rconc
[@1: The cat eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "rabbit" "-")
The bear eats the rabbit.
Unknown
rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "rabbit" "+")
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit chases the bear.
Unknown
rconc
[@2: The rabbit chases the bear.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("rabbit" "chases" "bear" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "dog" "-")
The dog eats the rabbit.
Unknown
rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "rabbit" "+")
The rabbit does not chase the dog.
Unknown
inv-random
[@0: The rabbit chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "dog" "-")
The cat needs the bear.
Unknown
random
[@0: The cat needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bear" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The dog does not chase the rabbit.
Unknown
inv-random
[@0: The dog chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "rabbit" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The bear chases the rabbit.[(triple1)] The cat needs the rabbit.[(triple2)] The dog chases the cat.[(triple3)] The dog is big.[(triple4)] The dog is cold.[(triple5)] The rabbit does not need the cat.[(triple7)] The rabbit eats the cat.[(triple6)] @1: The cat eats the dog.[(((triple2) -> rule4))] @2: The cat chases the bear.[(((((triple2) -> rule4)) -> rule2))] @3: The bear needs the rabbit.[(((((((triple2) -> rule4)) -> rule2)) -> rule3))] @4: The bear eats the dog.[(((((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule4))] @5: The bear chases the bear.[(((((((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule4)) -> rule2))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple2
The dog chases the cat.
("dog" "chases" "cat" "+")
triple3
The dog is big.
("dog" "is" "big" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
triple7
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple6
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple2) -> (rule4 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The bear eats the dog.
("bear" "eats" "dog" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The bear eats the dog.
("bear" "eats" "dog" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
((((((((((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear eats the dog.
("bear" "eats" "dog" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The cat chases the bear.
("cat" "chases" "bear" "+")
int4
The cat eats the dog.
("cat" "eats" "dog" "+")
int5