The bald eagle needs the bear. The bear is rough. The dog is kind. The lion visits the dog. If something is rough then it visits the lion. If the dog needs the bald eagle then the bald eagle is rough. If something visits the lion then it is green. If something visits the lion and it chases the bear then the bear visits the bald eagle. If something is kind then it needs the dog. Kind things are rough.
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
The bear is rough.
("bear" "is" "rough" "+")
The dog is kind.
("dog" "is" "kind" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If something is rough then it visits the lion.
((("something" "is" "rough" "+")) -> ("something" "visits" "lion" "+"))
If the dog needs the bald eagle then the bald eagle is rough.
((("dog" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "rough" "+"))
If something visits the lion then it is green.
((("something" "visits" "lion" "+")) -> ("something" "is" "green" "+"))
If something visits the lion and it chases the bear then the bear visits the bald eagle.
((("something" "visits" "lion" "+") ("something" "chases" "bear" "+")) -> ("bear" "visits" "bald eagle" "+"))
If something is kind then it needs the dog.
((("something" "is" "kind" "+")) -> ("something" "needs" "dog" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
The bear is rough.
True
1
proof
[(triple2)]
("bear" "is" "rough" "+")
triple2
The bear is not rough.
False
1
inv-proof
[(triple2)]
("bear" "is" "rough" "-")
triple2
The dog is rough.
True
2
proof
[(((triple3) -> rule6))]
("dog" "is" "rough" "+")
((triple3) -> (rule6 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The bear does not visit the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "visits" "lion" "-")
((triple2) -> (rule1 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The dog visits the lion.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("dog" "visits" "lion" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The bear is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("bear" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The dog is green.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule3))]
("dog" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog is not green.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule3))]
("dog" "is" "green" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The lion does not visit the lion.
Unknown
inv-rconc
[@2: The lion visits the lion.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "rough" "+")
The bald eagle is not rough.
Unknown
inv-rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "rough" "-")
The bear needs the dog.
Unknown
rconc
[@1: The bear needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "needs" "dog" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The dog visits the bald eagle.
Unknown
random
[@0: The dog visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bald eagle" "+")
@0: The bald eagle needs the bear.[(triple1)] The bear is rough.[(triple2)] The dog is kind.[(triple3)] The lion visits the dog.[(triple4)] @1: The bear visits the lion.[(((triple2) -> rule1))] The dog is rough.[(((triple3) -> rule6))] The dog needs the dog.[(((triple3) -> rule5))] @2: The bear is green.[(((((triple2) -> rule1)) -> rule3))] The dog visits the lion.[(((((triple3) -> rule6)) -> rule1))] @3: The dog is green.[(((((((triple3) -> rule6)) -> rule1)) -> rule3))]
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The lion visits the dog.
("lion" "visits" "dog" "+")
triple4
The bear visits the lion.
("bear" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((triple3) -> (rule6 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple3) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is green.
("dog" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3