The lion chases the squirrel. The mouse eats the squirrel. The squirrel is round. The tiger visits the squirrel. If the mouse chases the squirrel and the squirrel does not visit the mouse then the squirrel is not red. If someone chases the mouse then the mouse chases the tiger. If someone chases the lion and they visit the squirrel then the squirrel does not chase the tiger. If someone is round then they chase the lion. If someone eats the mouse then the mouse does not chase the squirrel. If someone visits the mouse and the mouse chases the lion then the mouse eats the squirrel. If someone eats the lion then they visit the tiger. If someone chases the lion then the lion is round.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the mouse chases the squirrel and the squirrel does not visit the mouse then the squirrel is not red.
((("mouse" "chases" "squirrel" "+") ("squirrel" "visits" "mouse" "~")) -> ("squirrel" "is" "red" "-"))
If someone chases the mouse then the mouse chases the tiger.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
If someone chases the lion and they visit the squirrel then the squirrel does not chase the tiger.
((("someone" "chases" "lion" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "-"))
If someone is round then they chase the lion.
((("someone" "is" "round" "+")) -> ("someone" "chases" "lion" "+"))
If someone eats the mouse then the mouse does not chase the squirrel.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "squirrel" "-"))
If someone visits the mouse and the mouse chases the lion then the mouse eats the squirrel.
((("someone" "visits" "mouse" "+") ("mouse" "chases" "lion" "+")) -> ("mouse" "eats" "squirrel" "+"))
If someone eats the lion then they visit the tiger.
((("someone" "eats" "lion" "+")) -> ("someone" "visits" "tiger" "+"))
If someone chases the lion then the lion is round.
((("someone" "chases" "lion" "+")) -> ("lion" "is" "round" "+"))
The lion chases the squirrel.
True
1
proof
[(triple1)]
("lion" "chases" "squirrel" "+")
triple1
The squirrel is not round.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "round" "-")
triple3
The squirrel chases the lion.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "chases" "lion" "+")
((triple3) -> (rule4 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel does not chase the lion.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "chases" "lion" "-")
((triple3) -> (rule4 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion is round.
True
3
proof
[(((((triple3) -> rule4)) -> rule8))]
("lion" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion is not round.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule8))]
("lion" "is" "round" "-")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion chases the lion.
True
4
proof
[(((((((triple3) -> rule4)) -> rule8)) -> rule4))]
("lion" "chases" "lion" "+")
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3
The lion does not chase the lion.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule8)) -> rule4))]
("lion" "chases" "lion" "-")
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3
The mouse does not visit the tiger.
Unknown
inv-rconc
[@1: The mouse visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "visits" "tiger" "+")
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 chases the tiger.
Unknown
rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "tiger" "+")
The squirrel does not visit the lion.
Unknown
inv-random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The tiger chases the mouse.
Unknown
random
[@0: The tiger chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "mouse" "+")
@0: The lion chases the squirrel.[(triple1)] The mouse eats the squirrel.[(triple2)] The squirrel is round.[(triple3)] The tiger visits the squirrel.[(triple4)] @1: The squirrel chases the lion.[(((triple3) -> rule4))] @2: The lion is round.[(((((triple3) -> rule4)) -> rule8))] @3: The lion chases the lion.[(((((((triple3) -> rule4)) -> rule8)) -> rule4))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple4
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple3) -> (rule4 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3