The bald eagle needs the lion. The bald eagle needs the mouse. The cat is red. The lion chases the cat. The lion is red. The mouse is nice. The mouse visits the lion. If someone visits the cat then the cat chases the mouse. If someone visits the cat and they visit the bald eagle then they chase the mouse. If someone needs the lion then the lion visits the cat. If someone visits the mouse then the mouse chases the lion. If the cat chases the mouse then the cat visits the bald eagle. If someone chases the cat then they are cold. If someone chases the cat and the cat is cold then the cat visits the lion. If the mouse chases the bald eagle and the mouse visits the bald eagle then the mouse needs the bald eagle.
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cat is red.
("cat" "is" "red" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is red.
("lion" "is" "red" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone visits the cat then the cat chases the mouse.
((("someone" "visits" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If someone visits the cat and they visit the bald eagle then they chase the mouse.
((("someone" "visits" "cat" "+") ("someone" "visits" "bald eagle" "+")) -> ("someone" "chases" "mouse" "+"))
If someone needs the lion then the lion visits the cat.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone visits the mouse then the mouse chases the lion.
((("someone" "visits" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If the cat chases the mouse then the cat visits the bald eagle.
((("cat" "chases" "mouse" "+")) -> ("cat" "visits" "bald eagle" "+"))
If someone chases the cat then they are cold.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the cat and the cat is cold then the cat visits the lion.
((("someone" "chases" "cat" "+") ("cat" "is" "cold" "+")) -> ("cat" "visits" "lion" "+"))
If the mouse chases the bald eagle and the mouse visits the bald eagle then the mouse needs the bald eagle.
((("mouse" "chases" "bald eagle" "+") ("mouse" "visits" "bald eagle" "+")) -> ("mouse" "needs" "bald eagle" "+"))
The bald eagle needs the mouse.
True
1
proof
[(triple2)]
("bald eagle" "needs" "mouse" "+")
triple2
The bald eagle does not need the lion.
False
1
inv-proof
[(triple1)]
("bald eagle" "needs" "lion" "-")
triple1
The lion visits the cat.
True
2
proof
[(((triple1) -> rule3))]
("lion" "visits" "cat" "+")
((triple1) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple4) -> rule6))]
("lion" "is" "cold" "-")
((triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The cat chases the mouse.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("cat" "chases" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat does not chase the mouse.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("cat" "chases" "mouse" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat visits the bald eagle.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
("cat" "visits" "bald eagle" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat does not visit the bald eagle.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
("cat" "visits" "bald eagle" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat does not visit the lion.
Unknown
inv-rconc
[@2: The cat visits the lion.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("cat" "visits" "lion" "-")
The lion chases the mouse.
Unknown
rconc
[@1: The lion chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "mouse" "+")
The mouse does not chase the lion.
Unknown
inv-rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "lion" "-")
The mouse needs the bald eagle.
Unknown
rconc
[@1: The mouse needs the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "needs" "bald eagle" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse needs the cat.
Unknown
random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The cat chases the lion.
Unknown
random
[@0: The cat chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "lion" "+")
@0: The bald eagle needs the lion.[(triple1)] The bald eagle needs the mouse.[(triple2)] The cat is red.[(triple3)] The lion chases the cat.[(triple4)] The lion is red.[(triple5)] The mouse is nice.[(triple6)] The mouse visits the lion.[(triple7)] @1: The lion is cold.[(((triple4) -> rule6))] The lion visits the cat.[(((triple1) -> rule3))] @2: The cat chases the mouse.[(((((triple1) -> rule3)) -> rule1))] @3: The cat visits the bald eagle.[(((((((triple1) -> rule3)) -> rule1)) -> rule5))]
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The lion chases the cat.
("lion" "chases" "cat" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
((triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple1) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3