The bald eagle is rough. The bear chases the bald eagle. The bear is cold. The lion chases the bear. The lion eats the bald eagle. The rabbit eats the lion. The rabbit sees the bear. If something eats the rabbit and the rabbit chases the bear then the bear is red. If something eats the rabbit then the rabbit chases the bear. If something chases the bear then it eats the rabbit.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bear chases the bald eagle.
("bear" "chases" "bald eagle" "+")
The bear is cold.
("bear" "is" "cold" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If something eats the rabbit and the rabbit chases the bear then the bear is red.
((("something" "eats" "rabbit" "+") ("rabbit" "chases" "bear" "+")) -> ("bear" "is" "red" "+"))
If something eats the rabbit then the rabbit chases the bear.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "chases" "bear" "+"))
If something chases the bear then it eats the rabbit.
((("something" "chases" "bear" "+")) -> ("something" "eats" "rabbit" "+"))
The rabbit sees the bear.
True
1
proof
[(triple7)]
("rabbit" "sees" "bear" "+")
triple7
The rabbit does not eat the lion.
False
1
inv-proof
[(triple6)]
("rabbit" "eats" "lion" "-")
triple6
The lion eats the rabbit.
True
2
proof
[(((triple4) -> rule3))]
("lion" "eats" "rabbit" "+")
((triple4) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion does not eat the rabbit.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "eats" "rabbit" "-")
((triple4) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The rabbit chases the bear.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("rabbit" "chases" "bear" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The rabbit does not chase the bear.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("rabbit" "chases" "bear" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The rabbit eats the rabbit.
True
4
proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
The bear is not red.
False
6
inv-proof
[(((((triple4) -> rule3) ((((triple4) -> rule3)) -> rule2)) -> rule1) OR ((((((((triple4) -> rule3)) -> rule2)) -> rule3) ((((triple4) -> rule3)) -> rule2)) -> rule1))]
("bear" "is" "red" "-")
((((triple4) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
((((((((triple4) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((((triple4) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int4
The bald eagle does not eat the rabbit.
Unknown
inv-rconc
[@1: The bald eagle eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "eats" "rabbit" "-")
The bear eats the rabbit.
Unknown
rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "rabbit" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
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 sees the rabbit.
Unknown
random
[@0: The bear sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "rabbit" "+")
@0: The bald eagle is rough.[(triple1)] The bear chases the bald eagle.[(triple2)] The bear is cold.[(triple3)] The lion chases the bear.[(triple4)] The lion eats the bald eagle.[(triple5)] The rabbit eats the lion.[(triple6)] The rabbit sees the bear.[(triple7)] @1: The lion eats the rabbit.[(((triple4) -> rule3))] @2: The rabbit chases the bear.[(((((triple4) -> rule3)) -> rule2))] @3: The bear is red.[(((((triple4) -> rule3) ((((triple4) -> rule3)) -> rule2)) -> rule1) OR ((((((((triple4) -> rule3)) -> rule2)) -> rule3) ((((triple4) -> rule3)) -> rule2)) -> rule1))] The rabbit eats the rabbit.[(((((((triple4) -> rule3)) -> rule2)) -> rule3))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bear chases the bald eagle.
("bear" "chases" "bald eagle" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The lion chases the bear.
("lion" "chases" "bear" "+")
triple4
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
triple5
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple7
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple4) -> (rule3 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((((triple4) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3
((((((((triple4) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) ((((triple4) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int3