The bald eagle is green. The lion is young. The mouse is blue. The tiger is rough. If the tiger is rough then the tiger chases the mouse. If someone is rough and they chase the mouse then they like the mouse. If someone is nice then they chase the bald eagle.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If the tiger is rough then the tiger chases the mouse.
((("tiger" "is" "rough" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone is rough and they chase the mouse then they like the mouse.
((("someone" "is" "rough" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is nice then they chase the bald eagle.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "bald eagle" "+"))
The tiger is rough.
True
1
proof
[(triple4)]
("tiger" "is" "rough" "+")
triple4
The tiger is not rough.
False
1
inv-proof
[(triple4)]
("tiger" "is" "rough" "-")
triple4
The tiger chases the mouse.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "chases" "mouse" "+")
((triple4) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger does not chase the mouse.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "chases" "mouse" "-")
((triple4) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("tiger" "likes" "mouse" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The tiger does not like the mouse.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule2))]
("tiger" "likes" "mouse" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2
The tiger does not chase the bald eagle.
Unknown
inv-rconc
[@1: The tiger chases the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "bald eagle" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The bald eagle does not like the mouse.
Unknown
inv-rconc
[@1: The bald eagle likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "mouse" "-")
The bald eagle needs the mouse.
Unknown
random
[@0: The bald eagle needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "mouse" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
@0: The bald eagle is green.[(triple1)] The lion is young.[(triple2)] The mouse is blue.[(triple3)] The tiger is rough.[(triple4)] @1: The tiger chases the mouse.[(((triple4) -> rule1))] @2: The tiger likes the mouse.[(((triple4 ((triple4) -> rule1)) -> rule2))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((triple4) -> (rule1 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int2