The bear visits the rabbit. The dog chases the rabbit. The dog is green. The dog is red. The dog needs the bear. The dog visits the rabbit. The rabbit chases the bear. The rabbit is green. The rabbit visits the bear. The rabbit visits the dog. If someone chases the bear then the bear chases the rabbit. If the dog visits the bear then the dog chases the bear. If someone needs the rabbit then they are green. If someone needs the bear and the bear chases the rabbit then the bear needs the rabbit. If someone chases the rabbit and they chase the bear then the rabbit needs the bear. If someone chases the dog then they visit the bear. If someone chases the bear then they visit the rabbit. If someone is cold then they visit the dog.
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone chases the bear then the bear chases the rabbit.
((("someone" "chases" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If the dog visits the bear then the dog chases the bear.
((("dog" "visits" "bear" "+")) -> ("dog" "chases" "bear" "+"))
If someone needs the rabbit then they are green.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If someone needs the bear and the bear chases the rabbit then the bear needs the rabbit.
((("someone" "needs" "bear" "+") ("bear" "chases" "rabbit" "+")) -> ("bear" "needs" "rabbit" "+"))
If someone chases the rabbit and they chase the bear then the rabbit needs the bear.
((("someone" "chases" "rabbit" "+") ("someone" "chases" "bear" "+")) -> ("rabbit" "needs" "bear" "+"))
If someone chases the dog then they visit the bear.
((("someone" "chases" "dog" "+")) -> ("someone" "visits" "bear" "+"))
If someone chases the bear then they visit the rabbit.
((("someone" "chases" "bear" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is cold then they visit the dog.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "dog" "+"))
The bear visits the rabbit.
True
1
proof
[(triple1)]
("bear" "visits" "rabbit" "+")
triple1
The rabbit is not green.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "green" "-")
triple8
The bear chases the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("bear" "chases" "rabbit" "+")
((triple7) -> (rule1 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple7) -> rule7))]
("rabbit" "visits" "rabbit" "-")
((triple7) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The bear needs the rabbit.
True
4
proof
[(((triple5 ((triple7) -> rule1)) -> rule4))]
("bear" "needs" "rabbit" "+")
((triple5 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The bear does not need the rabbit.
False
4
inv-proof
[(((triple5 ((triple7) -> rule1)) -> rule4))]
("bear" "needs" "rabbit" "-")
((triple5 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The bear is green.
True
5
proof
[(((((triple5 ((triple7) -> rule1)) -> rule4)) -> rule3))]
("bear" "is" "green" "+")
((((triple5 ((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
The bear is not green.
False
5
inv-proof
[(((((triple5 ((triple7) -> rule1)) -> rule4)) -> rule3))]
("bear" "is" "green" "-")
((((triple5 ((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
The dog does not visit the bear.
Unknown
inv-rconc
[@1: The dog visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "visits" "bear" "-")
The bear visits the dog.
Unknown
rconc
[@1: The bear visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "dog" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "visits" "bear" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "visits" "dog" "+")
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 rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear visits the rabbit.[(triple1)] The dog chases the rabbit.[(triple2)] The dog is green.[(triple3)] The dog is red.[(triple4)] The dog needs the bear.[(triple5)] The dog visits the rabbit.[(triple6)] The rabbit chases the bear.[(triple7)] The rabbit is green.[(triple8)] The rabbit visits the bear.[(triple9)] The rabbit visits the dog.[(triple10)] @1: The bear chases the rabbit.[(((triple7) -> rule1))] The rabbit visits the rabbit.[(((triple7) -> rule7))] @2: The bear needs the rabbit.[(((triple5 ((triple7) -> rule1)) -> rule4))] @3: The bear is green.[(((((triple5 ((triple7) -> rule1)) -> rule4)) -> rule3))]
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog needs the bear.
("dog" "needs" "bear" "+")
triple5
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple6
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple9
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
((triple7) -> (rule1 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple7) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((triple5 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The bear is green.
("bear" "is" "green" "+")
((((triple5 ((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3