The bald eagle sees the mouse. The cat eats the mouse. The mouse sees the tiger. The tiger is nice. If someone eats the cat then they are blue. If someone chases the tiger then the tiger sees the bald eagle. If someone sees the mouse then the mouse chases the tiger.
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone eats the cat then they are blue.
((("someone" "eats" "cat" "+")) -> ("someone" "is" "blue" "+"))
If someone chases the tiger then the tiger sees the bald eagle.
((("someone" "chases" "tiger" "+")) -> ("tiger" "sees" "bald eagle" "+"))
If someone sees the mouse then the mouse chases the tiger.
((("someone" "sees" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
The cat eats the mouse.
True
1
proof
[(triple2)]
("cat" "eats" "mouse" "+")
triple2
The tiger is not nice.
False
1
inv-proof
[(triple4)]
("tiger" "is" "nice" "-")
triple4
The mouse chases the tiger.
True
2
proof
[(((triple1) -> rule3))]
("mouse" "chases" "tiger" "+")
((triple1) -> (rule3 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("mouse" "chases" "tiger" "-")
((triple1) -> (rule3 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The tiger sees the bald eagle.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("tiger" "sees" "bald eagle" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The tiger does not see the bald eagle.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("tiger" "sees" "bald eagle" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "blue" "-")
The bald eagle is blue.
Unknown
rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "blue" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "blue" "-")
The bald eagle chases the cat.
Unknown
random
[@0: The bald eagle chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "cat" "+")
The tiger does not eat the cat.
Unknown
inv-random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The bald eagle sees the mouse.[(triple1)] The cat eats the mouse.[(triple2)] The mouse sees the tiger.[(triple3)] The tiger is nice.[(triple4)] @1: The mouse chases the tiger.[(((triple1) -> rule3))] @2: The tiger sees the bald eagle.[(((((triple1) -> rule3)) -> rule2))]
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
((triple1) -> (rule3 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2