The bald eagle is blue. The mouse is cold. The mouse is red. The rabbit chases the mouse. The rabbit is blue. The rabbit is kind. The rabbit is red. The tiger chases the rabbit. The tiger sees the mouse. The tiger visits the mouse. All cold things are kind. If something sees the tiger and it chases the bald eagle then the bald eagle visits the mouse. If something sees the mouse then it sees the tiger. If something chases the tiger then it visits the mouse. If something is kind then it visits the bald eagle. If something visits the bald eagle then the bald eagle is kind. If something chases the bald eagle and it is red then it visits the bald eagle. If something is blue and it visits the rabbit then it visits the tiger.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something sees the tiger and it chases the bald eagle then the bald eagle visits the mouse.
((("something" "sees" "tiger" "+") ("something" "chases" "bald eagle" "+")) -> ("bald eagle" "visits" "mouse" "+"))
If something sees the mouse then it sees the tiger.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "tiger" "+"))
If something chases the tiger then it visits the mouse.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "mouse" "+"))
If something is kind then it visits the bald eagle.
((("something" "is" "kind" "+")) -> ("something" "visits" "bald eagle" "+"))
If something visits the bald eagle then the bald eagle is kind.
((("something" "visits" "bald eagle" "+")) -> ("bald eagle" "is" "kind" "+"))
If something chases the bald eagle and it is red then it visits the bald eagle.
((("something" "chases" "bald eagle" "+") ("something" "is" "red" "+")) -> ("something" "visits" "bald eagle" "+"))
If something is blue and it visits the rabbit then it visits the tiger.
((("something" "is" "blue" "+") ("something" "visits" "rabbit" "+")) -> ("something" "visits" "tiger" "+"))
The rabbit is kind.
True
1
proof
[(triple6)]
("rabbit" "is" "kind" "+")
triple6
The tiger does not see the mouse.
False
1
inv-proof
[(triple9)]
("tiger" "sees" "mouse" "-")
triple9
The rabbit visits the bald eagle.
True
2
proof
[(((triple6) -> rule5))]
("rabbit" "visits" "bald eagle" "+")
((triple6) -> (rule5 % int1))
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int1
The rabbit does not visit the bald eagle.
False
2
inv-proof
[(((triple6) -> rule5))]
("rabbit" "visits" "bald eagle" "-")
((triple6) -> (rule5 % int1))
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
True
3
proof
[(((((triple6) -> rule5)) -> rule6) OR ((((((triple2) -> rule1)) -> rule5)) -> rule6))]
("bald eagle" "is" "kind" "+")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse does not visit the bald eagle.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("mouse" "visits" "bald eagle" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The bald eagle visits the bald eagle.
True
4
proof
[(((((((triple6) -> rule5)) -> rule6)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule5)) -> rule6)) -> rule5))]
("bald eagle" "visits" "bald eagle" "+")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The bald eagle does not visit the bald eagle.
False
4
inv-proof
[(((((((triple6) -> rule5)) -> rule6)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule5)) -> rule6)) -> rule5))]
("bald eagle" "visits" "bald eagle" "-")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4
The mouse does not visit the tiger.
Unknown
inv-rconc
[@1: The mouse visits the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "visits" "tiger" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The rabbit does not see the tiger.
Unknown
inv-rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The mouse chases the bald eagle.
Unknown
random
[@0: The mouse chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bald eagle" "+")
@0: The bald eagle is blue.[(triple1)] The mouse is cold.[(triple2)] The mouse is red.[(triple3)] The rabbit chases the mouse.[(triple4)] The rabbit is blue.[(triple5)] The rabbit is kind.[(triple6)] The rabbit is red.[(triple7)] The tiger chases the rabbit.[(triple8)] The tiger sees the mouse.[(triple9)] The tiger visits the mouse.[(triple10)] @1: The mouse is kind.[(((triple2) -> rule1))] The rabbit visits the bald eagle.[(((triple6) -> rule5))] The tiger sees the tiger.[(((triple9) -> rule3))] @2: The bald eagle is kind.[(((((triple6) -> rule5)) -> rule6) OR ((((((triple2) -> rule1)) -> rule5)) -> rule6))] The mouse visits the bald eagle.[(((((triple2) -> rule1)) -> rule5))] @3: The bald eagle visits the bald eagle.[(((((((triple6) -> rule5)) -> rule6)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule5)) -> rule6)) -> rule5))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple4
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple8
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple9
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
((triple6) -> (rule5 % int1))
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple9) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
int4