The lion eats the tiger. The lion is cold. The lion is green. The lion visits the rabbit. The rabbit is round. The rabbit sees the tiger. The squirrel eats the rabbit. The squirrel does not visit the rabbit. The tiger eats the squirrel. The tiger visits the rabbit. If someone visits the lion and they are not rough then they do not visit the rabbit. If someone eats the lion and they visit the tiger then the lion is round. If someone is rough and round then they do not visit the lion. If someone visits the squirrel then the squirrel visits the lion. If someone sees the tiger and the tiger does not eat the rabbit then they do not eat the tiger. If the squirrel visits the tiger and the squirrel eats the tiger then the tiger sees the rabbit. If the lion visits the rabbit then the rabbit visits the squirrel. If someone visits the lion then they do not visit the squirrel.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone visits the lion and they are not rough then they do not visit the rabbit.
((("someone" "visits" "lion" "+") ("someone" "is" "rough" "~")) -> ("someone" "visits" "rabbit" "-"))
If someone eats the lion and they visit the tiger then the lion is round.
((("someone" "eats" "lion" "+") ("someone" "visits" "tiger" "+")) -> ("lion" "is" "round" "+"))
If someone is rough and round then they do not visit the lion.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "-"))
If someone visits the squirrel then the squirrel visits the lion.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "lion" "+"))
If someone sees the tiger and the tiger does not eat the rabbit then they do not eat the tiger.
((("someone" "sees" "tiger" "+") ("tiger" "eats" "rabbit" "~")) -> ("someone" "eats" "tiger" "-"))
If the squirrel visits the tiger and the squirrel eats the tiger then the tiger sees the rabbit.
((("squirrel" "visits" "tiger" "+") ("squirrel" "eats" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If the lion visits the rabbit then the rabbit visits the squirrel.
((("lion" "visits" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If someone visits the lion then they do not visit the squirrel.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "squirrel" "-"))
The rabbit is round.
True
1
proof
[(triple5)]
("rabbit" "is" "round" "+")
triple5
The squirrel does not eat the rabbit.
False
1
inv-proof
[(triple7)]
("squirrel" "eats" "rabbit" "-")
triple7
The rabbit visits the squirrel.
True
2
proof
[(((triple4) -> rule7))]
("rabbit" "visits" "squirrel" "+")
((triple4) -> (rule7 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit does not visit the squirrel.
False
2
inv-proof
[(((triple4) -> rule7))]
("rabbit" "visits" "squirrel" "-")
((triple4) -> (rule7 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel visits the lion.
True
3
proof
[(((((triple4) -> rule7)) -> rule4))]
("squirrel" "visits" "lion" "+")
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel does not visit the lion.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule4))]
("squirrel" "visits" "lion" "-")
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
True
4
proof
[(((((((triple4) -> rule7)) -> rule4)) -> rule8))]
("squirrel" "visits" "squirrel" "-")
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The squirrel visits the squirrel.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule4)) -> rule8))]
("squirrel" "visits" "squirrel" "+")
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "round" "-")
The tiger sees the rabbit.
Unknown
rconc
[@1: The tiger sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "rabbit" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The squirrel sees the lion.
Unknown
random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
@0: The lion eats the tiger.[(triple1)] The lion is cold.[(triple2)] The lion is green.[(triple3)] The lion visits the rabbit.[(triple4)] The rabbit is round.[(triple5)] The rabbit sees the tiger.[(triple6)] The squirrel does not visit the rabbit.[(triple8)] The squirrel eats the rabbit.[(triple7)] The tiger eats the squirrel.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The rabbit visits the squirrel.[(((triple4) -> rule7))] @2: The squirrel visits the lion.[(((((triple4) -> rule7)) -> rule4))] @3: The squirrel does not visit the squirrel.[(((((((triple4) -> rule7)) -> rule4)) -> rule8))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple6
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
triple8
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple7
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple4) -> (rule7 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3