The lion chases the rabbit. The lion does not chase the squirrel. The lion eats the rabbit. The lion does not eat the squirrel. The lion is cold. The lion is round. The lion sees the rabbit. The lion sees the squirrel. The rabbit chases the squirrel. The rabbit does not eat the lion. The rabbit is round. The rabbit sees the lion. The rabbit sees the squirrel. The squirrel is big. The squirrel is round. If the lion chases the squirrel and the squirrel does not eat the rabbit then the rabbit chases the lion. If someone eats the lion then the lion is not cold. If someone sees the rabbit and they are not round then they chase the rabbit. If the squirrel is green then the squirrel sees the rabbit. If the squirrel sees the lion then the squirrel eats the lion. If someone sees the squirrel then they are nice. If someone sees the rabbit and the rabbit is nice then they are cold. All round people are green.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion does not eat the squirrel.
("lion" "eats" "squirrel" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If the lion chases the squirrel and the squirrel does not eat the rabbit then the rabbit chases the lion.
((("lion" "chases" "squirrel" "+") ("squirrel" "eats" "rabbit" "~")) -> ("rabbit" "chases" "lion" "+"))
If someone eats the lion then the lion is not cold.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "cold" "-"))
If someone sees the rabbit and they are not round then they chase the rabbit.
((("someone" "sees" "rabbit" "+") ("someone" "is" "round" "~")) -> ("someone" "chases" "rabbit" "+"))
If the squirrel is green then the squirrel sees the rabbit.
((("squirrel" "is" "green" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If the squirrel sees the lion then the squirrel eats the lion.
((("squirrel" "sees" "lion" "+")) -> ("squirrel" "eats" "lion" "+"))
If someone sees the squirrel then they are nice.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the rabbit and the rabbit is nice then they are cold.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
The lion is round.
True
1
proof
[(triple6)]
("lion" "is" "round" "+")
triple6
The lion does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "chases" "rabbit" "-")
triple1
The lion is green.
True
2
proof
[(((triple6) -> rule8))]
("lion" "is" "green" "+")
((triple6) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple6) -> rule8))]
("lion" "is" "green" "-")
((triple6) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The squirrel sees the rabbit.
True
3
proof
[(((((triple15) -> rule8)) -> rule4))]
("squirrel" "sees" "rabbit" "+")
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not see the rabbit.
False
3
inv-proof
[(((((triple15) -> rule8)) -> rule4))]
("squirrel" "sees" "rabbit" "-")
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is cold.
True
6
proof
[(((((((triple15) -> rule8)) -> rule4) ((triple13) -> rule6)) -> rule7))]
("squirrel" "is" "cold" "+")
((((((triple15) -> (rule8 % int4))) -> (rule4 % int3)) ((triple13) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The squirrel is not cold.
False
6
inv-proof
[(((((((triple15) -> rule8)) -> rule4) ((triple13) -> rule6)) -> rule7))]
("squirrel" "is" "cold" "-")
((((((triple15) -> (rule8 % int4))) -> (rule4 % int3)) ((triple13) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "cold" "+")
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "nice" "-")
The rabbit chases the lion.
Unknown
rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "lion" "+")
The squirrel does not eat the rabbit.
Unknown
inv-random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The squirrel does not chase the lion.
Unknown
inv-random
[@0: The squirrel chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "lion" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The lion chases the rabbit.[(triple1)] The lion does not chase the squirrel.[(triple2)] The lion does not eat the squirrel.[(triple4)] The lion eats the rabbit.[(triple3)] The lion is cold.[(triple5 OR ((triple7 ((triple13) -> rule6)) -> rule7))] The lion is round.[(triple6)] The lion sees the rabbit.[(triple7)] The lion sees the squirrel.[(triple8)] The rabbit chases the squirrel.[(triple9)] The rabbit does not eat the lion.[(triple10)] The rabbit is round.[(triple11)] The rabbit sees the lion.[(triple12)] The rabbit sees the squirrel.[(triple13)] The squirrel is big.[(triple14)] The squirrel is round.[(triple15)] @1: The lion is green.[(((triple6) -> rule8))] The lion is nice.[(((triple8) -> rule6))] The rabbit is green.[(((triple11) -> rule8))] The rabbit is nice.[(((triple13) -> rule6))] The squirrel is green.[(((triple15) -> rule8))] @2: The squirrel sees the rabbit.[(((((triple15) -> rule8)) -> rule4))] @3: The squirrel is cold.[(((((((triple15) -> rule8)) -> rule4) ((triple13) -> rule6)) -> rule7))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
triple2
The lion does not eat the squirrel.
("lion" "eats" "squirrel" "-")
triple4
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple5
((triple7 ((triple13) -> (rule6 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The lion is round.
("lion" "is" "round" "+")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple8
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple9
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple13
The squirrel is big.
("squirrel" "is" "big" "+")
triple14
The squirrel is round.
("squirrel" "is" "round" "+")
triple15
The lion is green.
("lion" "is" "green" "+")
((triple6) -> (rule8 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple8) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple11) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple13) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple15) -> (rule8 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((triple15) -> (rule8 % int4))) -> (rule4 % int3)) ((triple13) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4