The bald eagle does not chase the lion. The bald eagle visits the squirrel. The lion chases the squirrel. The lion is round. The mouse is big. The squirrel sees the mouse. The squirrel does not visit the lion. If someone visits the mouse then the mouse is round. If someone is young then they visit the mouse. If the lion visits the bald eagle and the lion is red then the bald eagle does not chase the lion. All round people are young. If someone visits the lion and the lion chases the mouse then they are young. If the mouse is red and the mouse is round then the mouse does not chase the bald eagle. If someone sees the bald eagle and they do not chase the squirrel then the squirrel is nice. If the lion sees the bald eagle and the bald eagle is nice then the lion is nice. Nice people are red.
The bald eagle does not chase the lion.
("bald eagle" "chases" "lion" "-")
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse is big.
("mouse" "is" "big" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
If someone visits the mouse then the mouse is round.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If someone is young then they visit the mouse.
((("someone" "is" "young" "+")) -> ("someone" "visits" "mouse" "+"))
If the lion visits the bald eagle and the lion is red then the bald eagle does not chase the lion.
((("lion" "visits" "bald eagle" "+") ("lion" "is" "red" "+")) -> ("bald eagle" "chases" "lion" "-"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone visits the lion and the lion chases the mouse then they are young.
((("someone" "visits" "lion" "+") ("lion" "chases" "mouse" "+")) -> ("someone" "is" "young" "+"))
If the mouse is red and the mouse is round then the mouse does not chase the bald eagle.
((("mouse" "is" "red" "+") ("mouse" "is" "round" "+")) -> ("mouse" "chases" "bald eagle" "-"))
If someone sees the bald eagle and they do not chase the squirrel then the squirrel is nice.
((("someone" "sees" "bald eagle" "+") ("someone" "chases" "squirrel" "~")) -> ("squirrel" "is" "nice" "+"))
If the lion sees the bald eagle and the bald eagle is nice then the lion is nice.
((("lion" "sees" "bald eagle" "+") ("bald eagle" "is" "nice" "+")) -> ("lion" "is" "nice" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
The bald eagle does not chase the lion.
True
1
proof
[(triple1)]
("bald eagle" "chases" "lion" "-")
triple1
The mouse is not big.
False
1
inv-proof
[(triple5)]
("mouse" "is" "big" "-")
triple5
The lion is young.
True
2
proof
[(((triple4) -> rule4))]
("lion" "is" "young" "+")
((triple4) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple4) -> rule4))]
("lion" "is" "young" "-")
((triple4) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the mouse.
True
3
proof
[(((((triple4) -> rule4)) -> rule2))]
("lion" "visits" "mouse" "+")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not visit the mouse.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule2))]
("lion" "visits" "mouse" "-")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The mouse is round.
True
4
proof
[(((((((triple4) -> rule4)) -> rule2)) -> rule1))]
("mouse" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The mouse is not round.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule2)) -> rule1))]
("mouse" "is" "round" "-")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The mouse is young.
True
5
proof
[(((((((((triple4) -> rule4)) -> rule2)) -> rule1)) -> rule4))]
("mouse" "is" "young" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The mouse is not young.
False
5
inv-proof
[(((((((((triple4) -> rule4)) -> rule2)) -> rule1)) -> rule4))]
("mouse" "is" "young" "-")
((((((((triple4) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The mouse visits the mouse.
True
6
proof
[(((((((((((triple4) -> rule4)) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
("mouse" "visits" "mouse" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The mouse does not visit the mouse.
False
6
inv-proof
[(((((((((((triple4) -> rule4)) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
("mouse" "visits" "mouse" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The bald eagle is not young.
Unknown
inv-rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "is" "young" "-")
The mouse is red.
Unknown
rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("mouse" "is" "red" "+")
The squirrel is not red.
Unknown
inv-rconc
[@2: The squirrel is red.[CWA. Example of deepest failure = (rule9 <- rule7 <- FAIL)]]
("squirrel" "is" "red" "-")
The bald eagle visits the mouse.
Unknown
rconc
[@2: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("bald eagle" "visits" "mouse" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "young" "-")
The lion is red.
Unknown
rconc
[@2: The lion is red.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("lion" "is" "red" "+")
The lion does not see the mouse.
Unknown
inv-random
[@0: The lion sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The bald eagle does not see the lion.
Unknown
inv-random
[@0: The bald eagle sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "lion" "-")
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" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The mouse chases the bald eagle.
Unknown
random
[@0: The mouse chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bald eagle" "+")
@0: The bald eagle does not chase the lion.[(triple1)] The bald eagle visits the squirrel.[(triple2)] The lion chases the squirrel.[(triple3)] The lion is round.[(triple4)] The mouse is big.[(triple5)] The squirrel does not visit the lion.[(triple7)] The squirrel sees the mouse.[(triple6)] @1: The lion is young.[(((triple4) -> rule4))] @2: The lion visits the mouse.[(((((triple4) -> rule4)) -> rule2))] @3: The mouse is round.[(((((((triple4) -> rule4)) -> rule2)) -> rule1))] @4: The mouse is young.[(((((((((triple4) -> rule4)) -> rule2)) -> rule1)) -> rule4))] @5: The mouse visits the mouse.[(((((((((((triple4) -> rule4)) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
The bald eagle does not chase the lion.
("bald eagle" "chases" "lion" "-")
triple1
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
triple7
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple6
The lion is young.
("lion" "is" "young" "+")
((triple4) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5