The bald eagle is not big. The bald eagle is round. The bald eagle sees the mouse. The bald eagle does not visit the mouse. The bald eagle visits the tiger. The mouse sees the bald eagle. The mouse visits the bald eagle. The tiger is cold. The tiger likes the bald eagle. The tiger likes the mouse. If the mouse visits the bald eagle then the mouse is round. If something sees the tiger then the tiger is rough. If something is round and it visits the bald eagle then it does not see the tiger. If something is cold and not round then it sees the tiger. If something visits the tiger and it likes the mouse then the mouse sees the bald eagle. If something visits the bald eagle and it does not see the tiger then it likes the mouse.
The bald eagle is not big.
("bald eagle" "is" "big" "-")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the mouse visits the bald eagle then the mouse is round.
((("mouse" "visits" "bald eagle" "+")) -> ("mouse" "is" "round" "+"))
If something sees the tiger then the tiger is rough.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something is round and it visits the bald eagle then it does not see the tiger.
((("something" "is" "round" "+") ("something" "visits" "bald eagle" "+")) -> ("something" "sees" "tiger" "-"))
If something is cold and not round then it sees the tiger.
((("something" "is" "cold" "+") ("something" "is" "round" "~")) -> ("something" "sees" "tiger" "+"))
If something visits the tiger and it likes the mouse then the mouse sees the bald eagle.
((("something" "visits" "tiger" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "sees" "bald eagle" "+"))
If something visits the bald eagle and it does not see the tiger then it likes the mouse.
((("something" "visits" "bald eagle" "+") ("something" "sees" "tiger" "~")) -> ("something" "likes" "mouse" "+"))
The tiger likes the mouse.
True
1
proof
[(triple10)]
("tiger" "likes" "mouse" "+")
triple10
The tiger does not like the bald eagle.
False
1
inv-proof
[(triple9)]
("tiger" "likes" "bald eagle" "-")
triple9
The mouse is round.
True
2
proof
[(((triple7) -> rule1))]
("mouse" "is" "round" "+")
((triple7) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple7) -> rule1))]
("mouse" "is" "round" "-")
((triple7) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not see the tiger.
True
4
proof
[(((((triple7) -> rule1) triple7) -> rule3))]
("mouse" "sees" "tiger" "-")
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse sees the tiger.
False
4
inv-proof
[(((((triple7) -> rule1) triple7) -> rule3))]
("mouse" "sees" "tiger" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the mouse.
True
6
proof
[(((triple7 ((((triple7) -> rule1) triple7) -> rule3)) -> rule6))]
("mouse" "likes" "mouse" "+")
((triple7 ((((triple7) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The mouse does not like the mouse.
False
6
inv-proof
[(((triple7 ((((triple7) -> rule1) triple7) -> rule3)) -> rule6))]
("mouse" "likes" "mouse" "-")
((triple7 ((((triple7) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The bald eagle sees the tiger.
Unknown
rconc
[@1: The bald eagle sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "sees" "tiger" "+")
The bald eagle does not like the mouse.
Unknown
inv-rconc
[@1: The bald eagle likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "likes" "mouse" "-")
The tiger is rough.
Unknown
rconc
[@2: The tiger is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The bald eagle is rough.
Unknown
random
[@0: The bald eagle is rough.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "rough" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The bald eagle does not visit the mouse.[(triple4)] The bald eagle is not big.[(triple1)] The bald eagle is round.[(triple2)] The bald eagle sees the mouse.[(triple3)] The bald eagle visits the tiger.[(triple5)] The mouse sees the bald eagle.[(triple6)] The mouse visits the bald eagle.[(triple7)] The tiger is cold.[(triple8)] The tiger likes the bald eagle.[(triple9)] The tiger likes the mouse.[(triple10)] @1: The mouse is round.[(((triple7) -> rule1))] @2: The mouse does not see the tiger.[(((((triple7) -> rule1) triple7) -> rule3))] @3: The mouse likes the mouse.[(((triple7 ((((triple7) -> rule1) triple7) -> rule3)) -> rule6))]
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
triple4
The bald eagle is not big.
("bald eagle" "is" "big" "-")
triple1
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple2
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple3
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple5
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
triple6
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple9
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple10
The mouse is round.
("mouse" "is" "round" "+")
((triple7) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
((((triple7) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple7 ((((triple7) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3