The bear does not chase the lion. The bear chases the squirrel. The bear is cold. The lion chases the rabbit. The lion is cold. The lion needs the rabbit. The lion does not visit the squirrel. The rabbit does not chase the bear. The rabbit does not need the lion. The rabbit does not visit the lion. The rabbit visits the squirrel. The squirrel chases the rabbit. The squirrel is big. The squirrel needs the lion. The squirrel visits the rabbit. If something needs the rabbit then the rabbit is big. All big things are rough.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is cold.
("bear" "is" "cold" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
The rabbit does not visit the lion.
("rabbit" "visits" "lion" "-")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something needs the rabbit then the rabbit is big.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
The bear chases the squirrel.
True
1
proof
[(triple2)]
("bear" "chases" "squirrel" "+")
triple2
The bear is not cold.
False
1
inv-proof
[(triple3)]
("bear" "is" "cold" "-")
triple3
The rabbit is big.
True
2
proof
[(((triple6) -> rule1))]
("rabbit" "is" "big" "+")
((triple6) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "is" "big" "-")
((triple6) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple6) -> rule1)) -> rule2))]
("rabbit" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule2))]
("rabbit" "is" "rough" "-")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "rough" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "rough" "+")
The bear does not visit the squirrel.
Unknown
inv-random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The squirrel does not need the rabbit.
Unknown
inv-random
[@0: The squirrel needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "rabbit" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear chases the squirrel.[(triple2)] The bear does not chase the lion.[(triple1)] The bear is cold.[(triple3)] The lion chases the rabbit.[(triple4)] The lion does not visit the squirrel.[(triple7)] The lion is cold.[(triple5)] The lion needs the rabbit.[(triple6)] The rabbit does not chase the bear.[(triple8)] The rabbit does not need the lion.[(triple9)] The rabbit does not visit the lion.[(triple10)] The rabbit visits the squirrel.[(triple11)] The squirrel chases the rabbit.[(triple12)] The squirrel is big.[(triple13)] The squirrel needs the lion.[(triple14)] The squirrel visits the rabbit.[(triple15)] @1: The rabbit is big.[(((triple6) -> rule1))] The squirrel is rough.[(((triple13) -> rule2))] @2: The rabbit is rough.[(((((triple6) -> rule1)) -> rule2))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple4
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple5
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple6
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
triple8
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple9
The rabbit does not visit the lion.
("rabbit" "visits" "lion" "-")
triple10
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple11
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple12
The squirrel is big.
("squirrel" "is" "big" "+")
triple13
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple14
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple15
The rabbit is big.
("rabbit" "is" "big" "+")
((triple6) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple13) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2