The bear chases the lion. The bear chases the squirrel. The bear is young. The bear needs the lion. The lion chases the bear. The lion chases the squirrel. The lion likes the squirrel. The squirrel chases the lion. The squirrel is cold. The squirrel needs the lion. If something likes the squirrel and it needs the squirrel then it is kind. If something chases the lion then the lion likes the bear. If something is kind and it needs the lion then it is cold. If something likes the bear and the bear likes the lion then the lion likes the bear. If something likes the bear then it needs the lion. If something likes the bear and the bear chases the squirrel then it is young. If something needs the lion then it needs the bear. If something likes the squirrel and the squirrel likes the lion then the squirrel chases the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If something likes the squirrel and it needs the squirrel then it is kind.
((("something" "likes" "squirrel" "+") ("something" "needs" "squirrel" "+")) -> ("something" "is" "kind" "+"))
If something chases the lion then the lion likes the bear.
((("something" "chases" "lion" "+")) -> ("lion" "likes" "bear" "+"))
If something is kind and it needs the lion then it is cold.
((("something" "is" "kind" "+") ("something" "needs" "lion" "+")) -> ("something" "is" "cold" "+"))
If something likes the bear and the bear likes the lion then the lion likes the bear.
((("something" "likes" "bear" "+") ("bear" "likes" "lion" "+")) -> ("lion" "likes" "bear" "+"))
If something likes the bear then it needs the lion.
((("something" "likes" "bear" "+")) -> ("something" "needs" "lion" "+"))
If something likes the bear and the bear chases the squirrel then it is young.
((("something" "likes" "bear" "+") ("bear" "chases" "squirrel" "+")) -> ("something" "is" "young" "+"))
If something needs the lion then it needs the bear.
((("something" "needs" "lion" "+")) -> ("something" "needs" "bear" "+"))
If something likes the squirrel and the squirrel likes the lion then the squirrel chases the lion.
((("something" "likes" "squirrel" "+") ("squirrel" "likes" "lion" "+")) -> ("squirrel" "chases" "lion" "+"))
The lion chases the squirrel.
True
1
proof
[(triple6)]
("lion" "chases" "squirrel" "+")
triple6
The squirrel is not cold.
False
1
inv-proof
[(triple9)]
("squirrel" "is" "cold" "-")
triple9
The squirrel needs the bear.
True
2
proof
[(((triple10) -> rule7))]
("squirrel" "needs" "bear" "+")
((triple10) -> (rule7 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The lion does not like the bear.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple8) -> rule2))]
("lion" "likes" "bear" "-")
((triple1) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
((triple8) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion needs the lion.
True
3
proof
[(((((triple1) -> rule2)) -> rule5) OR ((((triple8) -> rule2)) -> rule5))]
("lion" "needs" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion is not young.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule6) OR ((((triple8) -> rule2) triple2) -> rule6))]
("lion" "is" "young" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
((((triple8) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "kind" "-")
The lion is cold.
Unknown
rconc
[@2: The lion is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("lion" "is" "cold" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The bear chases the lion.[(triple1)] The bear chases the squirrel.[(triple2)] The bear is young.[(triple3)] The bear needs the lion.[(triple4)] The lion chases the bear.[(triple5)] The lion chases the squirrel.[(triple6)] The lion likes the squirrel.[(triple7)] The squirrel chases the lion.[(triple8)] The squirrel is cold.[(triple9)] The squirrel needs the lion.[(triple10)] @1: The bear needs the bear.[(((triple4) -> rule7))] The lion likes the bear.[(((triple1) -> rule2) OR ((triple8) -> rule2))] The squirrel needs the bear.[(((triple10) -> rule7))] @2: The lion is young.[(((((triple1) -> rule2) triple2) -> rule6) OR ((((triple8) -> rule2) triple2) -> rule6))] The lion needs the lion.[(((((triple1) -> rule2)) -> rule5) OR ((((triple8) -> rule2)) -> rule5))] @3: The lion needs the bear.[(((((((triple1) -> rule2)) -> rule5)) -> rule7) OR ((((((triple8) -> rule2)) -> rule5)) -> rule7))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear needs the lion.
("bear" "needs" "lion" "+")
triple4
The lion chases the bear.
("lion" "chases" "bear" "+")
triple5
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple6
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple7
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple10
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple4) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
((triple1) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
((triple8) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple10) -> (rule7 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
((((triple8) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion likes the bear.
("lion" "likes" "bear" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion likes the bear.
("lion" "likes" "bear" "+")
int3