The bald eagle chases the mouse. The bald eagle is cold. The bald eagle likes the lion. The bald eagle sees the lion. The cat likes the bald eagle. The cat likes the mouse. The lion likes the bald eagle. The lion sees the bald eagle. The mouse is big. The mouse likes the lion. If something likes the lion and the lion chases the mouse then the lion sees the cat. If something sees the bald eagle then it is big. If something is big then it chases the mouse. If something chases the lion and the lion is kind then it sees the cat. If something is nice and green then it chases the mouse. If the lion is nice and the lion is big then the lion is cold.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If something likes the lion and the lion chases the mouse then the lion sees the cat.
((("something" "likes" "lion" "+") ("lion" "chases" "mouse" "+")) -> ("lion" "sees" "cat" "+"))
If something sees the bald eagle then it is big.
((("something" "sees" "bald eagle" "+")) -> ("something" "is" "big" "+"))
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the lion and the lion is kind then it sees the cat.
((("something" "chases" "lion" "+") ("lion" "is" "kind" "+")) -> ("something" "sees" "cat" "+"))
If something is nice and green then it chases the mouse.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "chases" "mouse" "+"))
If the lion is nice and the lion is big then the lion is cold.
((("lion" "is" "nice" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "cold" "+"))
The mouse is big.
True
1
proof
[(triple9)]
("mouse" "is" "big" "+")
triple9
The bald eagle is not cold.
False
1
inv-proof
[(triple2)]
("bald eagle" "is" "cold" "-")
triple2
The lion is big.
True
2
proof
[(((triple8) -> rule2))]
("lion" "is" "big" "+")
((triple8) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple8) -> rule2))]
("lion" "is" "big" "-")
((triple8) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion chases the mouse.
True
3
proof
[(((((triple8) -> rule2)) -> rule3))]
("lion" "chases" "mouse" "+")
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not chase the mouse.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule3))]
("lion" "chases" "mouse" "-")
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
True
5
proof
[(((triple10 ((((triple8) -> rule2)) -> rule3)) -> rule1) OR ((triple3 ((((triple8) -> rule2)) -> rule3)) -> rule1))]
("lion" "sees" "cat" "+")
((triple10 ((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((triple3 ((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion does not see the cat.
False
5
inv-proof
[(((triple10 ((((triple8) -> rule2)) -> rule3)) -> rule1) OR ((triple3 ((((triple8) -> rule2)) -> rule3)) -> rule1))]
("lion" "sees" "cat" "-")
((triple10 ((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((triple3 ((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "cat" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "big" "+")
The bald eagle is not big.
Unknown
inv-rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "big" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "cold" "+")
The bald eagle is not green.
Unknown
inv-random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The bald eagle chases the mouse.[(triple1)] The bald eagle is cold.[(triple2)] The bald eagle likes the lion.[(triple3)] The bald eagle sees the lion.[(triple4)] The cat likes the bald eagle.[(triple5)] The cat likes the mouse.[(triple6)] The lion likes the bald eagle.[(triple7)] The lion sees the bald eagle.[(triple8)] The mouse is big.[(triple9)] The mouse likes the lion.[(triple10)] @1: The lion is big.[(((triple8) -> rule2))] The mouse chases the mouse.[(((triple9) -> rule3))] @2: The lion chases the mouse.[(((((triple8) -> rule2)) -> rule3))] @3: The lion sees the cat.[(((triple10 ((((triple8) -> rule2)) -> rule3)) -> rule1) OR ((triple3 ((((triple8) -> rule2)) -> rule3)) -> rule1))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple2
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
triple3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple4
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
triple7
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple10
The lion is big.
("lion" "is" "big" "+")
((triple8) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple9) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
((triple10 ((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((triple3 ((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3