The bald eagle visits the squirrel. The lion sees the squirrel. The mouse eats the bald eagle. The squirrel visits the lion. If something is young then it sees the lion. If something eats the bald eagle then it is young. If something visits the squirrel and the squirrel sees the mouse then the mouse does not see the squirrel. If something sees the squirrel and the squirrel is not red then it eats the bald eagle. If something is red and it does not visit the lion then it eats the lion. If the mouse sees the lion then the mouse does not see the bald eagle.
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something is young then it sees the lion.
((("something" "is" "young" "+")) -> ("something" "sees" "lion" "+"))
If something eats the bald eagle then it is young.
((("something" "eats" "bald eagle" "+")) -> ("something" "is" "young" "+"))
If something visits the squirrel and the squirrel sees the mouse then the mouse does not see the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "sees" "mouse" "+")) -> ("mouse" "sees" "squirrel" "-"))
If something sees the squirrel and the squirrel is not red then it eats the bald eagle.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "red" "~")) -> ("something" "eats" "bald eagle" "+"))
If something is red and it does not visit the lion then it eats the lion.
((("something" "is" "red" "+") ("something" "visits" "lion" "~")) -> ("something" "eats" "lion" "+"))
If the mouse sees the lion then the mouse does not see the bald eagle.
((("mouse" "sees" "lion" "+")) -> ("mouse" "sees" "bald eagle" "-"))
The squirrel visits the lion.
True
1
proof
[(triple4)]
("squirrel" "visits" "lion" "+")
triple4
The lion does not see the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "sees" "squirrel" "-")
triple2
The mouse is young.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "is" "young" "+")
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "is" "young" "-")
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse sees the lion.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("mouse" "sees" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not see the lion.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("mouse" "sees" "lion" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The lion does not eat the bald eagle.
Unknown
inv-rconc
[@1: The lion eats the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "bald eagle" "-")
The bald eagle sees the lion.
Unknown
rconc
[@3: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- FAIL)]]
("bald eagle" "sees" "lion" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "lion" "-")
The bald eagle eats the squirrel.
Unknown
random
[@0: The bald eagle eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "squirrel" "+")
The bald eagle is not round.
Unknown
inv-random
[@0: The bald eagle is round.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "round" "-")
The squirrel eats the mouse.
Unknown
random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "+")
@0: The bald eagle visits the squirrel.[(triple1)] The lion sees the squirrel.[(triple2)] The mouse eats the bald eagle.[(triple3)] The squirrel visits the lion.[(triple4)] @1: The mouse is young.[(((triple3) -> rule2))] @2: The mouse sees the lion.[(((((triple3) -> rule2)) -> rule1))] @3: The mouse does not see the bald eagle.[(((((((triple3) -> rule2)) -> rule1)) -> rule6))]
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
triple3
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3