The bald eagle is young. The bald eagle likes the bear. The bald eagle likes the mouse. The bear likes the bald eagle. The mouse is young. The mouse does not visit the tiger. The tiger likes the bald eagle. If something likes the bald eagle then it needs the tiger.
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
The bear likes the bald eagle.
("bear" "likes" "bald eagle" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
If something likes the bald eagle then it needs the tiger.
((("something" "likes" "bald eagle" "+")) -> ("something" "needs" "tiger" "+"))
The mouse does not visit the tiger.
True
1
proof
[(triple6)]
("mouse" "visits" "tiger" "-")
triple6
The bald eagle is not young.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "young" "-")
triple1
The bear needs the tiger.
True
2
proof
[(((triple4) -> rule1))]
("bear" "needs" "tiger" "+")
((triple4) -> (rule1 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "needs" "tiger" "-")
((triple7) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The bald eagle needs the tiger.
Unknown
rconc
[@1: The bald eagle needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "needs" "tiger" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The mouse visits the bald eagle.
Unknown
random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "+")
@0: The bald eagle is young.[(triple1)] The bald eagle likes the bear.[(triple2)] The bald eagle likes the mouse.[(triple3)] The bear likes the bald eagle.[(triple4)] The mouse does not visit the tiger.[(triple6)] The mouse is young.[(triple5)] The tiger likes the bald eagle.[(triple7)] @1: The bear needs the tiger.[(((triple4) -> rule1))] The tiger needs the tiger.[(((triple7) -> rule1))]
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple1
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple2
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
triple3
The bear likes the bald eagle.
("bear" "likes" "bald eagle" "+")
triple4
The mouse does not visit the tiger.
("mouse" "visits" "tiger" "-")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple5
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple7
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple4) -> (rule1 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple7) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1