The bald eagle is not round. The lion is cold. The rabbit chases the tiger. The tiger sees the rabbit. If something chases the tiger then it is round. If something sees the tiger then the tiger chases the lion. If something is round then it likes the bald eagle. If something chases the tiger and it sees the lion then it likes the lion. If something likes the bald eagle then the bald eagle sees the lion. If the tiger does not like the bald eagle then the tiger likes the rabbit.
The bald eagle is not round.
("bald eagle" "is" "round" "-")
The lion is cold.
("lion" "is" "cold" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something chases the tiger then it is round.
((("something" "chases" "tiger" "+")) -> ("something" "is" "round" "+"))
If something sees the tiger then the tiger chases the lion.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If something is round then it likes the bald eagle.
((("something" "is" "round" "+")) -> ("something" "likes" "bald eagle" "+"))
If something chases the tiger and it sees the lion then it likes the lion.
((("something" "chases" "tiger" "+") ("something" "sees" "lion" "+")) -> ("something" "likes" "lion" "+"))
If something likes the bald eagle then the bald eagle sees the lion.
((("something" "likes" "bald eagle" "+")) -> ("bald eagle" "sees" "lion" "+"))
If the tiger does not like the bald eagle then the tiger likes the rabbit.
((("tiger" "likes" "bald eagle" "~")) -> ("tiger" "likes" "rabbit" "+"))
The tiger sees the rabbit.
True
1
proof
[(triple4)]
("tiger" "sees" "rabbit" "+")
triple4
The rabbit does not chase the tiger.
False
1
inv-proof
[(triple3)]
("rabbit" "chases" "tiger" "-")
triple3
The rabbit is round.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "is" "round" "+")
((triple3) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "is" "round" "-")
((triple3) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit likes the bald eagle.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("rabbit" "likes" "bald eagle" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit does not like the bald eagle.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("rabbit" "likes" "bald eagle" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The bald eagle sees the lion.
True
4
proof
[(((((((triple3) -> rule1)) -> rule3)) -> rule5))]
("bald eagle" "sees" "lion" "+")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The bald eagle does not see the lion.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule3)) -> rule5))]
("bald eagle" "sees" "lion" "-")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The lion does not like the bald eagle.
Unknown
inv-rconc
[@2: The lion likes the bald eagle.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "likes" "bald eagle" "-")
The tiger chases the lion.
Unknown
rconc
[@1: The tiger chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "lion" "+")
The tiger does not like the bald eagle.
Unknown
inv-rconc
[@2: The tiger likes the bald eagle.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("tiger" "likes" "bald eagle" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "round" "+")
The bald eagle does not chase the tiger.
Unknown
inv-random
[@0: The bald eagle chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "tiger" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle is not round.[(triple1)] The lion is cold.[(triple2)] The rabbit chases the tiger.[(triple3)] The tiger sees the rabbit.[(triple4)] @1: The rabbit is round.[(((triple3) -> rule1))] @2: The rabbit likes the bald eagle.[(((((triple3) -> rule1)) -> rule3))] @3: The bald eagle sees the lion.[(((((((triple3) -> rule1)) -> rule3)) -> rule5))]
The bald eagle is not round.
("bald eagle" "is" "round" "-")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
((triple3) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3