The bald eagle is nice. The bear likes the rabbit. The rabbit visits the bear. The tiger is red. If something likes the rabbit then the rabbit visits the bear. If something is green then it likes the bear. If something visits the bear then the bear is green. If something likes the bear and the bear sees the rabbit then the bear visits the bald eagle. If something likes the bear and the bear sees the rabbit then the rabbit sees the bear. If something likes the bear then the bear is young.
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something likes the rabbit then the rabbit visits the bear.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If something is green then it likes the bear.
((("something" "is" "green" "+")) -> ("something" "likes" "bear" "+"))
If something visits the bear then the bear is green.
((("something" "visits" "bear" "+")) -> ("bear" "is" "green" "+"))
If something likes the bear and the bear sees the rabbit then the bear visits the bald eagle.
((("something" "likes" "bear" "+") ("bear" "sees" "rabbit" "+")) -> ("bear" "visits" "bald eagle" "+"))
If something likes the bear and the bear sees the rabbit then the rabbit sees the bear.
((("something" "likes" "bear" "+") ("bear" "sees" "rabbit" "+")) -> ("rabbit" "sees" "bear" "+"))
If something likes the bear then the bear is young.
((("something" "likes" "bear" "+")) -> ("bear" "is" "young" "+"))
The rabbit visits the bear.
True
1
proof
[(triple3 OR ((triple2) -> rule1))]
("rabbit" "visits" "bear" "+")
triple3
((triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit does not visit the bear.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("rabbit" "visits" "bear" "-")
triple3
((triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The bear is green.
True
2
proof
[(((triple3) -> rule3) OR ((((triple2) -> rule1)) -> rule3))]
("bear" "is" "green" "+")
((triple3) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The bear is not green.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple2) -> rule1)) -> rule3))]
("bear" "is" "green" "-")
((triple3) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The bear likes the bear.
True
3
proof
[(((((triple3) -> rule3)) -> rule2) OR ((((((triple2) -> rule1)) -> rule3)) -> rule2))]
("bear" "likes" "bear" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The bear does not like the bear.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2) OR ((((((triple2) -> rule1)) -> rule3)) -> rule2))]
("bear" "likes" "bear" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The bear is young.
True
4
proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule6) OR ((((((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule6))]
("bear" "is" "young" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
The bear is not young.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule6) OR ((((((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule6))]
("bear" "is" "young" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4
The bear does not visit the bald eagle.
Unknown
inv-rconc
[@1: The bear visits the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "bald eagle" "-")
The tiger likes the bear.
Unknown
rconc
[@1: The tiger likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "bear" "+")
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The bald eagle likes the bear.
Unknown
rconc
[@1: The bald eagle likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "bear" "+")
The rabbit does not like the bald eagle.
Unknown
inv-random
[@0: The rabbit likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bald eagle" "-")
The tiger likes the bald eagle.
Unknown
random
[@0: The tiger likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bald eagle" "+")
The bear does not see the tiger.
Unknown
inv-random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "-")
The tiger visits the rabbit.
Unknown
random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "+")
@0: The bald eagle is nice.[(triple1)] The bear likes the rabbit.[(triple2)] The rabbit visits the bear.[(triple3 OR ((triple2) -> rule1))] The tiger is red.[(triple4)] @1: The bear is green.[(((triple3) -> rule3) OR ((((triple2) -> rule1)) -> rule3))] @2: The bear likes the bear.[(((((triple3) -> rule3)) -> rule2) OR ((((((triple2) -> rule1)) -> rule3)) -> rule2))] @3: The bear is young.[(((((((triple3) -> rule3)) -> rule2)) -> rule6) OR ((((((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule6))]
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple3
((triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
triple4
The bear is green.
("bear" "is" "green" "+")
((triple3) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The bear is young.
("bear" "is" "young" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int4