The bald eagle eats the mouse. The bald eagle sees the mouse. The bald eagle visits the mouse. The cat eats the bald eagle. The cat eats the lion. The cat does not eat the mouse. The cat does not visit the mouse. The lion is not green. The lion is round. The lion visits the cat. The mouse is not cold. The mouse visits the lion. If someone sees the mouse then they eat the cat. If the cat visits the mouse then the cat visits the bald eagle. If someone visits the bald eagle and the bald eagle does not eat the lion then they see the lion. If someone eats the lion and the lion visits the bald eagle then the bald eagle eats the cat. If someone eats the cat then the cat sees the mouse. If someone visits the bald eagle and the bald eagle is round then they eat the mouse.
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat does not eat the mouse.
("cat" "eats" "mouse" "-")
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
The lion is not green.
("lion" "is" "green" "-")
The lion is round.
("lion" "is" "round" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone sees the mouse then they eat the cat.
((("someone" "sees" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If the cat visits the mouse then the cat visits the bald eagle.
((("cat" "visits" "mouse" "+")) -> ("cat" "visits" "bald eagle" "+"))
If someone visits the bald eagle and the bald eagle does not eat the lion then they see the lion.
((("someone" "visits" "bald eagle" "+") ("bald eagle" "eats" "lion" "~")) -> ("someone" "sees" "lion" "+"))
If someone eats the lion and the lion visits the bald eagle then the bald eagle eats the cat.
((("someone" "eats" "lion" "+") ("lion" "visits" "bald eagle" "+")) -> ("bald eagle" "eats" "cat" "+"))
If someone eats the cat then the cat sees the mouse.
((("someone" "eats" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If someone visits the bald eagle and the bald eagle is round then they eat the mouse.
((("someone" "visits" "bald eagle" "+") ("bald eagle" "is" "round" "+")) -> ("someone" "eats" "mouse" "+"))
The cat eats the lion.
True
1
proof
[(triple5)]
("cat" "eats" "lion" "+")
triple5
The cat does not eat the lion.
False
1
inv-proof
[(triple5)]
("cat" "eats" "lion" "-")
triple5
The bald eagle eats the cat.
True
2
proof
[(((triple2) -> rule1))]
("bald eagle" "eats" "cat" "+")
((triple2) -> (rule1 % int1))
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int1
The bald eagle does not eat the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("bald eagle" "eats" "cat" "-")
((triple2) -> (rule1 % int1))
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int1
The cat sees the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("cat" "sees" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int2
The cat does not see the mouse.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("cat" "sees" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int2
The cat eats the cat.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule1))]
("cat" "eats" "cat" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int3
The cat does not eat the cat.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule1))]
("cat" "eats" "cat" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "+")
The mouse does not eat the cat.
Unknown
inv-rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "cat" "-")
The lion eats the cat.
Unknown
rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "cat" "+")
The mouse does not eat the bald eagle.
Unknown
inv-random
[@0: The mouse eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bald eagle" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The bald eagle eats the mouse.[(triple1)] The bald eagle sees the mouse.[(triple2)] The bald eagle visits the mouse.[(triple3)] The cat does not eat the mouse.[(triple6)] The cat does not visit the mouse.[(triple7)] The cat eats the bald eagle.[(triple4)] The cat eats the lion.[(triple5)] The lion is not green.[(triple8)] The lion is round.[(triple9)] The lion visits the cat.[(triple10)] The mouse is not cold.[(triple11)] The mouse visits the lion.[(triple12)] @1: The bald eagle eats the cat.[(((triple2) -> rule1))] @2: The cat sees the mouse.[(((((triple2) -> rule1)) -> rule5))] @3: The cat eats the cat.[(((((((triple2) -> rule1)) -> rule5)) -> rule1))]
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
triple1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple2
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
triple3
The cat does not eat the mouse.
("cat" "eats" "mouse" "-")
triple6
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
triple7
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
triple4
The cat eats the lion.
("cat" "eats" "lion" "+")
triple5
The lion is not green.
("lion" "is" "green" "-")
triple8
The lion is round.
("lion" "is" "round" "+")
triple9
The lion visits the cat.
("lion" "visits" "cat" "+")
triple10
The mouse is not cold.
("mouse" "is" "cold" "-")
triple11
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple12
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
((triple2) -> (rule1 % int1))
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
int3