The bald eagle eats the rabbit. The bald eagle is nice. The bald eagle sees the rabbit. The bald eagle visits the tiger. The cow is cold. The rabbit eats the cow. The rabbit eats the tiger. The rabbit is rough. The rabbit is round. The rabbit sees the tiger. The tiger eats the bald eagle. The tiger sees the rabbit. If something eats the rabbit and it is nice then the rabbit sees the tiger. If something visits the bald eagle and the bald eagle is young then it is round. If something is rough and it sees the tiger then the tiger visits the cow.
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The cow is cold.
("cow" "is" "cold" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something eats the rabbit and it is nice then the rabbit sees the tiger.
((("something" "eats" "rabbit" "+") ("something" "is" "nice" "+")) -> ("rabbit" "sees" "tiger" "+"))
If something visits the bald eagle and the bald eagle is young then it is round.
((("something" "visits" "bald eagle" "+") ("bald eagle" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is rough and it sees the tiger then the tiger visits the cow.
((("something" "is" "rough" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
The rabbit sees the tiger.
True
1
proof
[(triple10 OR ((triple1 triple2) -> rule1))]
("rabbit" "sees" "tiger" "+")
triple10
((triple1 triple2) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit is not round.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "round" "-")
triple9
The tiger visits the cow.
True
3
proof
[(((triple8 triple10) -> rule3) OR ((triple8 ((triple1 triple2) -> rule1)) -> rule3))]
("tiger" "visits" "cow" "+")
((triple8 triple10) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple8 ((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger does not visit the cow.
False
3
inv-proof
[(((triple8 triple10) -> rule3) OR ((triple8 ((triple1 triple2) -> rule1)) -> rule3))]
("tiger" "visits" "cow" "-")
((triple8 triple10) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple8 ((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "round" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "round" "+")
The bald eagle does not eat the cow.
Unknown
inv-random
[@0: The bald eagle eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The bald eagle eats the rabbit.[(triple1)] The bald eagle is nice.[(triple2)] The bald eagle sees the rabbit.[(triple3)] The bald eagle visits the tiger.[(triple4)] The cow is cold.[(triple5)] The rabbit eats the cow.[(triple6)] The rabbit eats the tiger.[(triple7)] The rabbit is rough.[(triple8)] The rabbit is round.[(triple9)] The rabbit sees the tiger.[(triple10 OR ((triple1 triple2) -> rule1))] The tiger eats the bald eagle.[(triple11)] The tiger sees the rabbit.[(triple12)] @1: The tiger visits the cow.[(((triple8 triple10) -> rule3) OR ((triple8 ((triple1 triple2) -> rule1)) -> rule3))]
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
triple1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
triple2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
triple3
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
triple5
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple6
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple10
((triple1 triple2) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
triple11
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple12
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple8 triple10) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((triple8 ((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2