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