The bald eagle needs the cat. The cat needs the bald eagle. The mouse is kind. If the bald eagle chases the mouse and the bald eagle is blue then the mouse is round. If someone is cold then they visit the mouse. If someone chases the mouse then they do not visit the mouse. If someone is cold and they visit the mouse then the mouse does not chase the cat. If someone needs the cat and the cat needs the bald eagle then the cat is cold. If the cat does not visit the bald eagle then the bald eagle does not chase the mouse. If someone chases the bald eagle then the bald eagle does not chase the mouse. If someone chases the bald eagle and they visit the cat then the cat is kind.
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
If the bald eagle chases the mouse and the bald eagle is blue then the mouse is round.
((("bald eagle" "chases" "mouse" "+") ("bald eagle" "is" "blue" "+")) -> ("mouse" "is" "round" "+"))
If someone is cold then they visit the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "mouse" "+"))
If someone chases the mouse then they do not visit the mouse.
((("someone" "chases" "mouse" "+")) -> ("someone" "visits" "mouse" "-"))
If someone is cold and they visit the mouse then the mouse does not chase the cat.
((("someone" "is" "cold" "+") ("someone" "visits" "mouse" "+")) -> ("mouse" "chases" "cat" "-"))
If someone needs the cat and the cat needs the bald eagle then the cat is cold.
((("someone" "needs" "cat" "+") ("cat" "needs" "bald eagle" "+")) -> ("cat" "is" "cold" "+"))
If the cat does not visit the bald eagle then the bald eagle does not chase the mouse.
((("cat" "visits" "bald eagle" "~")) -> ("bald eagle" "chases" "mouse" "-"))
If someone chases the bald eagle then the bald eagle does not chase the mouse.
((("someone" "chases" "bald eagle" "+")) -> ("bald eagle" "chases" "mouse" "-"))
If someone chases the bald eagle and they visit the cat then the cat is kind.
((("someone" "chases" "bald eagle" "+") ("someone" "visits" "cat" "+")) -> ("cat" "is" "kind" "+"))
The cat needs the bald eagle.
True
1
proof
[(triple2)]
("cat" "needs" "bald eagle" "+")
triple2
The cat does not need the bald eagle.
False
1
inv-proof
[(triple2)]
("cat" "needs" "bald eagle" "-")
triple2
The cat is cold.
True
3
proof
[(((triple1 triple2) -> rule5))]
("cat" "is" "cold" "+")
((triple1 triple2) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
3
inv-proof
[(((triple1 triple2) -> rule5))]
("cat" "is" "cold" "-")
((triple1 triple2) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the mouse.
True
4
proof
[(((((triple1 triple2) -> rule5)) -> rule2))]
("cat" "visits" "mouse" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat does not visit the mouse.
False
4
inv-proof
[(((((triple1 triple2) -> rule5)) -> rule2))]
("cat" "visits" "mouse" "-")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The mouse does not chase the cat.
True
8
proof
[(((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule2)) -> rule4))]
("mouse" "chases" "cat" "-")
((((triple1 triple2) -> (rule5 % int3)) ((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The mouse chases the cat.
False
8
inv-proof
[(((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule2)) -> rule4))]
("mouse" "chases" "cat" "+")
((((triple1 triple2) -> (rule5 % int3)) ((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The bald eagle does not visit the mouse.
Unknown
inv-rconc
[@1: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "visits" "mouse" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "round" "+")
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "kind" "+")
The bald eagle is not blue.
Unknown
inv-random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "-")
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 mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse visits the bald eagle.
Unknown
random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "+")
@0: The bald eagle needs the cat.[(triple1)] The cat needs the bald eagle.[(triple2)] The mouse is kind.[(triple3)] @1: The cat is cold.[(((triple1 triple2) -> rule5))] @2: The cat visits the mouse.[(((((triple1 triple2) -> rule5)) -> rule2))] @3: The mouse does not chase the cat.[(((((triple1 triple2) -> rule5) ((((triple1 triple2) -> rule5)) -> rule2)) -> rule4))]
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
triple1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
((triple1 triple2) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
((((triple1 triple2) -> (rule5 % int3)) ((((triple1 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3