The bear chases the tiger. The lion needs the bear. The squirrel eats the bear. The tiger needs the bear. If someone needs the lion and they chase the tiger then they chase the lion. If someone chases the bear then they are kind. If someone chases the tiger then they need the lion. If someone needs the bear and they are round then they need the squirrel. If the squirrel needs the bear and the squirrel chases the lion then the lion eats the bear. If someone eats the squirrel and they do not need the tiger then the tiger needs the lion. If the bear needs the squirrel and the bear does not need the tiger then the squirrel is rough. If someone chases the bear then the bear is young.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If someone needs the lion and they chase the tiger then they chase the lion.
((("someone" "needs" "lion" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the bear then they are kind.
((("someone" "chases" "bear" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the tiger then they need the lion.
((("someone" "chases" "tiger" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the bear and they are round then they need the squirrel.
((("someone" "needs" "bear" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "squirrel" "+"))
If the squirrel needs the bear and the squirrel chases the lion then the lion eats the bear.
((("squirrel" "needs" "bear" "+") ("squirrel" "chases" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If someone eats the squirrel and they do not need the tiger then the tiger needs the lion.
((("someone" "eats" "squirrel" "+") ("someone" "needs" "tiger" "~")) -> ("tiger" "needs" "lion" "+"))
If the bear needs the squirrel and the bear does not need the tiger then the squirrel is rough.
((("bear" "needs" "squirrel" "+") ("bear" "needs" "tiger" "~")) -> ("squirrel" "is" "rough" "+"))
If someone chases the bear then the bear is young.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "young" "+"))
The lion needs the bear.
True
1
proof
[(triple2)]
("lion" "needs" "bear" "+")
triple2
The tiger does not need the bear.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "bear" "-")
triple4
The bear needs the lion.
True
2
proof
[(((triple1) -> rule3))]
("bear" "needs" "lion" "+")
((triple1) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "needs" "lion" "-")
((triple1) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear chases the lion.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("bear" "chases" "lion" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear does not chase the lion.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("bear" "chases" "lion" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The tiger does not need the squirrel.
Unknown
inv-rconc
[@1: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The lion does not need the squirrel.
Unknown
inv-rconc
[@1: The lion needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "squirrel" "-")
The bear eats the lion.
Unknown
random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger chases the squirrel.
Unknown
random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "+")
@0: The bear chases the tiger.[(triple1)] The lion needs the bear.[(triple2)] The squirrel eats the bear.[(triple3)] The tiger needs the bear.[(triple4)] @1: The bear needs the lion.[(((triple1) -> rule3))] @2: The bear chases the lion.[(((((triple1) -> rule3) triple1) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The lion needs the bear.
("lion" "needs" "bear" "+")
triple2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple4
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple1) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2