The bald eagle is rough. The cow needs the lion. The lion eats the bald eagle. The tiger sees the cow. If the bald eagle is blue then the bald eagle sees the tiger. If something sees the bald eagle and it sees the cow then the bald eagle needs the lion. If something needs the bald eagle then the bald eagle sees the tiger. If something needs the bald eagle then it is rough. If the lion eats the cow then the cow needs the lion. If something sees the cow then the cow needs the tiger. If something needs the tiger then it is kind. Rough things are kind.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If the bald eagle is blue then the bald eagle sees the tiger.
((("bald eagle" "is" "blue" "+")) -> ("bald eagle" "sees" "tiger" "+"))
If something sees the bald eagle and it sees the cow then the bald eagle needs the lion.
((("something" "sees" "bald eagle" "+") ("something" "sees" "cow" "+")) -> ("bald eagle" "needs" "lion" "+"))
If something needs the bald eagle then the bald eagle sees the tiger.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "sees" "tiger" "+"))
If something needs the bald eagle then it is rough.
((("something" "needs" "bald eagle" "+")) -> ("something" "is" "rough" "+"))
If the lion eats the cow then the cow needs the lion.
((("lion" "eats" "cow" "+")) -> ("cow" "needs" "lion" "+"))
If something sees the cow then the cow needs the tiger.
((("something" "sees" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
If something needs the tiger then it is kind.
((("something" "needs" "tiger" "+")) -> ("something" "is" "kind" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
The cow needs the lion.
True
1
proof
[(triple2)]
("cow" "needs" "lion" "+")
triple2
The lion does not eat the bald eagle.
False
1
inv-proof
[(triple3)]
("lion" "eats" "bald eagle" "-")
triple3
The cow needs the tiger.
True
2
proof
[(((triple4) -> rule6))]
("cow" "needs" "tiger" "+")
((triple4) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The bald eagle is not kind.
False
2
inv-proof
[(((triple1) -> rule8))]
("bald eagle" "is" "kind" "-")
((triple1) -> (rule8 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cow is kind.
True
3
proof
[(((((triple4) -> rule6)) -> rule7))]
("cow" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule7))]
("cow" "is" "kind" "-")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The bald eagle does not see the tiger.
Unknown
inv-rconc
[@1: The bald eagle sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "sees" "tiger" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "rough" "+")
The lion is not kind.
Unknown
inv-rconc
[@2: The lion is kind.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("lion" "is" "kind" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The tiger does not need the bald eagle.
Unknown
inv-random
[@0: The tiger needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bald eagle" "-")
The cow eats the tiger.
Unknown
random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "+")
@0: The bald eagle is rough.[(triple1)] The cow needs the lion.[(triple2)] The lion eats the bald eagle.[(triple3)] The tiger sees the cow.[(triple4)] @1: The bald eagle is kind.[(((triple1) -> rule8))] The cow needs the tiger.[(((triple4) -> rule6))] @2: The cow is kind.[(((((triple4) -> rule6)) -> rule7))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
triple3
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple4
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((triple1) -> (rule8 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple4) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2