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