The bald eagle is not green. The bald eagle is kind. The rabbit eats the squirrel. The rabbit is red. The rabbit visits the bald eagle. The rabbit visits the tiger. The squirrel is green. The squirrel visits the bald eagle. The tiger is blue. The tiger needs the bald eagle. If the bald eagle visits the tiger and the bald eagle is rough then the tiger visits the bald eagle. If someone needs the squirrel then the squirrel does not need the rabbit. If someone is green then they eat the tiger. If someone is rough and green then they do not need the rabbit. If someone needs the squirrel and the squirrel visits the bald eagle then the bald eagle does not need the rabbit. If the tiger eats the bald eagle then the tiger is red. Blue people are green. If the tiger is not green and the tiger does not eat the bald eagle then the tiger eats the squirrel.
The bald eagle is not green.
("bald eagle" "is" "green" "-")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
If the bald eagle visits the tiger and the bald eagle is rough then the tiger visits the bald eagle.
((("bald eagle" "visits" "tiger" "+") ("bald eagle" "is" "rough" "+")) -> ("tiger" "visits" "bald eagle" "+"))
If someone needs the squirrel then the squirrel does not need the rabbit.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "rabbit" "-"))
If someone is green then they eat the tiger.
((("someone" "is" "green" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is rough and green then they do not need the rabbit.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "rabbit" "-"))
If someone needs the squirrel and the squirrel visits the bald eagle then the bald eagle does not need the rabbit.
((("someone" "needs" "squirrel" "+") ("squirrel" "visits" "bald eagle" "+")) -> ("bald eagle" "needs" "rabbit" "-"))
If the tiger eats the bald eagle then the tiger is red.
((("tiger" "eats" "bald eagle" "+")) -> ("tiger" "is" "red" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If the tiger is not green and the tiger does not eat the bald eagle then the tiger eats the squirrel.
((("tiger" "is" "green" "~") ("tiger" "eats" "bald eagle" "~")) -> ("tiger" "eats" "squirrel" "+"))
The squirrel is green.
True
1
proof
[(triple7)]
("squirrel" "is" "green" "+")
triple7
The tiger is not blue.
False
1
inv-proof
[(triple9)]
("tiger" "is" "blue" "-")
triple9
The tiger is green.
True
2
proof
[(((triple9) -> rule7))]
("tiger" "is" "green" "+")
((triple9) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The squirrel does not eat the tiger.
False
2
inv-proof
[(((triple7) -> rule3))]
("squirrel" "eats" "tiger" "-")
((triple7) -> (rule3 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The tiger eats the tiger.
True
3
proof
[(((((triple9) -> rule7)) -> rule3))]
("tiger" "eats" "tiger" "+")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger does not eat the tiger.
False
3
inv-proof
[(((((triple9) -> rule7)) -> rule3))]
("tiger" "eats" "tiger" "-")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "green" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "red" "+")
The tiger does not eat the squirrel.
Unknown
inv-rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "squirrel" "-")
The tiger eats the rabbit.
Unknown
random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "+")
The bald eagle does not need the tiger.
Unknown
inv-random
[@0: The bald eagle needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "tiger" "-")
The tiger needs the squirrel.
Unknown
random
[@0: The tiger needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "squirrel" "+")
@0: The bald eagle is kind.[(triple2)] The bald eagle is not green.[(triple1)] The rabbit eats the squirrel.[(triple3)] The rabbit is red.[(triple4)] The rabbit visits the bald eagle.[(triple5)] The rabbit visits the tiger.[(triple6)] The squirrel is green.[(triple7)] The squirrel visits the bald eagle.[(triple8)] The tiger is blue.[(triple9)] The tiger needs the bald eagle.[(triple10)] @1: The squirrel eats the tiger.[(((triple7) -> rule3))] The tiger is green.[(((triple9) -> rule7))] @2: The tiger eats the tiger.[(((((triple9) -> rule7)) -> rule3))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple2
The bald eagle is not green.
("bald eagle" "is" "green" "-")
triple1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
triple4
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
triple5
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel visits the bald eagle.
("squirrel" "visits" "bald eagle" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple10
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((triple7) -> (rule3 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple9) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2