The bear chases the dog. The dog eats the rabbit. The rabbit eats the dog. All red things are cold. If the bear visits the rabbit and the bear does not eat the dog then the dog does not visit the rabbit. If the dog eats the rabbit then the dog does not visit the rabbit. If the dog chases the bear then the bear chases the rabbit. If something visits the rabbit and it eats the dog then the dog eats the rabbit. If something is green then it eats the bear. If the dog does not visit the rabbit then the dog is green. If something eats the rabbit and it is not green then it visits the bear.
The bear chases the dog.
("bear" "chases" "dog" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If the bear visits the rabbit and the bear does not eat the dog then the dog does not visit the rabbit.
((("bear" "visits" "rabbit" "+") ("bear" "eats" "dog" "~")) -> ("dog" "visits" "rabbit" "-"))
If the dog eats the rabbit then the dog does not visit the rabbit.
((("dog" "eats" "rabbit" "+")) -> ("dog" "visits" "rabbit" "-"))
If the dog chases the bear then the bear chases the rabbit.
((("dog" "chases" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If something visits the rabbit and it eats the dog then the dog eats the rabbit.
((("something" "visits" "rabbit" "+") ("something" "eats" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
If something is green then it eats the bear.
((("something" "is" "green" "+")) -> ("something" "eats" "bear" "+"))
If the dog does not visit the rabbit then the dog is green.
((("dog" "visits" "rabbit" "~")) -> ("dog" "is" "green" "+"))
If something eats the rabbit and it is not green then it visits the bear.
((("something" "eats" "rabbit" "+") ("something" "is" "green" "~")) -> ("something" "visits" "bear" "+"))
The bear chases the dog.
True
1
proof
[(triple1)]
("bear" "chases" "dog" "+")
triple1
The bear does not chase the dog.
False
1
inv-proof
[(triple1)]
("bear" "chases" "dog" "-")
triple1
The dog does not visit the rabbit.
True
2
proof
[(((triple2) -> rule3))]
("dog" "visits" "rabbit" "-")
((triple2) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The dog visits the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "visits" "rabbit" "+")
((triple2) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The dog is green.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("dog" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int2
The dog is not green.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("dog" "is" "green" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int2
The dog eats the bear.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
("dog" "eats" "bear" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int3
The dog does not eat the bear.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
("dog" "eats" "bear" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "bear" "-")
The rabbit visits the bear.
Unknown
rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "bear" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "bear" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "cold" "+")
The dog does not chase the bear.
Unknown
inv-random
[@0: The dog chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bear" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The bear chases the dog.[(triple1)] The dog eats the rabbit.[(triple2)] The rabbit eats the dog.[(triple3)] @1: The dog does not visit the rabbit.[(((triple2) -> rule3))] @2: The dog is green.[(((((triple2) -> rule3)) -> rule7))] @3: The dog eats the bear.[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple3
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
((triple2) -> (rule3 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The dog is green.
("dog" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int3