The bald eagle does not visit the tiger. The mouse is blue. The mouse is kind. The mouse visits the bald eagle. The tiger does not need the bald eagle. The tiger visits the bald eagle. The tiger visits the mouse. If someone is kind and blue then they need the tiger. If someone is blue and they need the tiger then they are red. If someone chases the mouse then they do not need the bald eagle. If the bald eagle chases the tiger then the tiger needs the bald eagle. All red people are young. If someone needs the mouse then the mouse visits the bald eagle. If someone visits the tiger and they are red then the tiger chases the mouse. If someone needs the bald eagle then the bald eagle chases the mouse.
The bald eagle does not visit the tiger.
("bald eagle" "visits" "tiger" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
The tiger does not need the bald eagle.
("tiger" "needs" "bald eagle" "-")
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is kind and blue then they need the tiger.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is blue and they need the tiger then they are red.
((("someone" "is" "blue" "+") ("someone" "needs" "tiger" "+")) -> ("someone" "is" "red" "+"))
If someone chases the mouse then they do not need the bald eagle.
((("someone" "chases" "mouse" "+")) -> ("someone" "needs" "bald eagle" "-"))
If the bald eagle chases the tiger then the tiger needs the bald eagle.
((("bald eagle" "chases" "tiger" "+")) -> ("tiger" "needs" "bald eagle" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone needs the mouse then the mouse visits the bald eagle.
((("someone" "needs" "mouse" "+")) -> ("mouse" "visits" "bald eagle" "+"))
If someone visits the tiger and they are red then the tiger chases the mouse.
((("someone" "visits" "tiger" "+") ("someone" "is" "red" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone needs the bald eagle then the bald eagle chases the mouse.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "chases" "mouse" "+"))
The mouse is kind.
True
1
proof
[(triple3)]
("mouse" "is" "kind" "+")
triple3
The bald eagle visits the tiger.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "tiger" "+")
triple1
The mouse needs the tiger.
True
3
proof
[(((triple3 triple2) -> rule1))]
("mouse" "needs" "tiger" "+")
((triple3 triple2) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("mouse" "needs" "tiger" "-")
((triple3 triple2) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse is red.
True
5
proof
[(((triple2 ((triple3 triple2) -> rule1)) -> rule2))]
("mouse" "is" "red" "+")
((triple2 ((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse is not red.
False
5
inv-proof
[(((triple2 ((triple3 triple2) -> rule1)) -> rule2))]
("mouse" "is" "red" "-")
((triple2 ((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse is young.
True
6
proof
[(((((triple2 ((triple3 triple2) -> rule1)) -> rule2)) -> rule5))]
("mouse" "is" "young" "+")
((((triple2 ((triple3 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The mouse is not young.
False
6
inv-proof
[(((((triple2 ((triple3 triple2) -> rule1)) -> rule2)) -> rule5))]
("mouse" "is" "young" "-")
((((triple2 ((triple3 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The bald eagle is not young.
Unknown
inv-rconc
[@2: The bald eagle is young.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("bald eagle" "is" "young" "-")
The tiger chases the mouse.
Unknown
rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "chases" "mouse" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The bald eagle is red.
Unknown
rconc
[@1: The bald eagle is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "red" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The bald eagle chases the tiger.
Unknown
random
[@0: The bald eagle chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "tiger" "+")
The tiger does not need the mouse.
Unknown
inv-random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The bald eagle does not visit the tiger.[(triple1)] The mouse is blue.[(triple2)] The mouse is kind.[(triple3)] The mouse visits the bald eagle.[(triple4)] The tiger does not need the bald eagle.[(triple5)] The tiger visits the bald eagle.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The mouse needs the tiger.[(((triple3 triple2) -> rule1))] @2: The mouse is red.[(((triple2 ((triple3 triple2) -> rule1)) -> rule2))] @3: The mouse is young.[(((((triple2 ((triple3 triple2) -> rule1)) -> rule2)) -> rule5))]
The bald eagle does not visit the tiger.
("bald eagle" "visits" "tiger" "-")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple4
The tiger does not need the bald eagle.
("tiger" "needs" "bald eagle" "-")
triple5
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple3 triple2) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple2 ((triple3 triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
((((triple2 ((triple3 triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3