The bear is round. The rabbit is big. The squirrel chases the bear. The tiger needs the squirrel. If something chases the rabbit then it needs the bear. If something is round then it likes the squirrel. If something likes the tiger and the tiger likes the bear then the bear is young. If the rabbit is young and the rabbit needs the bear then the rabbit chases the tiger. If something needs the tiger and the tiger needs the rabbit then the tiger chases the rabbit. If something is round and kind then it chases the tiger. If something chases the rabbit and the rabbit chases the squirrel then it is kind. If something likes the squirrel then the squirrel is round.
The bear is round.
("bear" "is" "round" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something chases the rabbit then it needs the bear.
((("something" "chases" "rabbit" "+")) -> ("something" "needs" "bear" "+"))
If something is round then it likes the squirrel.
((("something" "is" "round" "+")) -> ("something" "likes" "squirrel" "+"))
If something likes the tiger and the tiger likes the bear then the bear is young.
((("something" "likes" "tiger" "+") ("tiger" "likes" "bear" "+")) -> ("bear" "is" "young" "+"))
If the rabbit is young and the rabbit needs the bear then the rabbit chases the tiger.
((("rabbit" "is" "young" "+") ("rabbit" "needs" "bear" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something needs the tiger and the tiger needs the rabbit then the tiger chases the rabbit.
((("something" "needs" "tiger" "+") ("tiger" "needs" "rabbit" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something is round and kind then it chases the tiger.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the rabbit and the rabbit chases the squirrel then it is kind.
((("something" "chases" "rabbit" "+") ("rabbit" "chases" "squirrel" "+")) -> ("something" "is" "kind" "+"))
If something likes the squirrel then the squirrel is round.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
The tiger needs the squirrel.
True
1
proof
[(triple4)]
("tiger" "needs" "squirrel" "+")
triple4
The squirrel does not chase the bear.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "bear" "-")
triple3
The bear likes the squirrel.
True
2
proof
[(((triple1) -> rule2))]
("bear" "likes" "squirrel" "+")
((triple1) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear does not like the squirrel.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "likes" "squirrel" "-")
((triple1) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The squirrel is round.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("squirrel" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The squirrel is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("squirrel" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The squirrel likes the squirrel.
True
4
proof
[(((((((triple1) -> rule2)) -> rule8)) -> rule2))]
("squirrel" "likes" "squirrel" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The squirrel does not like the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule8)) -> rule2))]
("squirrel" "likes" "squirrel" "-")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "kind" "-")
The tiger is kind.
Unknown
rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "kind" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The rabbit needs the bear.
Unknown
rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "bear" "+")
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 squirrel likes the bear.
Unknown
random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "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 is round.[(triple1)] The rabbit is big.[(triple2)] The squirrel chases the bear.[(triple3)] The tiger needs the squirrel.[(triple4)] @1: The bear likes the squirrel.[(((triple1) -> rule2))] @2: The squirrel is round.[(((((triple1) -> rule2)) -> rule8))] @3: The squirrel likes the squirrel.[(((((((triple1) -> rule2)) -> rule8)) -> rule2))]
The bear is round.
("bear" "is" "round" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple3
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple4
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((triple1) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int3