The bear needs the tiger. The cat is round. The squirrel needs the tiger. The tiger likes the squirrel. If someone likes the bear then the bear likes the cat. If someone needs the cat then they like the bear. If someone needs the tiger then the tiger needs the cat.
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The cat is round.
("cat" "is" "round" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If someone likes the bear then the bear likes the cat.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If someone needs the cat then they like the bear.
((("someone" "needs" "cat" "+")) -> ("someone" "likes" "bear" "+"))
If someone needs the tiger then the tiger needs the cat.
((("someone" "needs" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
The squirrel needs the tiger.
True
1
proof
[(triple3)]
("squirrel" "needs" "tiger" "+")
triple3
The cat is not round.
False
1
inv-proof
[(triple2)]
("cat" "is" "round" "-")
triple2
The tiger needs the cat.
True
2
proof
[(((triple1) -> rule3) OR ((triple3) -> rule3))]
("tiger" "needs" "cat" "+")
((triple1) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
((triple3) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger does not need the cat.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple3) -> rule3))]
("tiger" "needs" "cat" "-")
((triple1) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
((triple3) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger likes the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
("tiger" "likes" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger does not like the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
("tiger" "likes" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The bear likes the cat.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((((triple3) -> rule3)) -> rule2)) -> rule1))]
("bear" "likes" "cat" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The bear does not like the cat.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((((triple3) -> rule3)) -> rule2)) -> rule1))]
("bear" "likes" "cat" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The squirrel does not like the bear.
Unknown
inv-rconc
[@1: The squirrel likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "bear" "-")
The cat likes the bear.
Unknown
rconc
[@1: The cat likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "bear" "+")
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "bear" "-")
The squirrel needs the cat.
Unknown
random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The tiger sees the cat.
Unknown
random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "+")
The squirrel does not see the bear.
Unknown
inv-random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "-")
The squirrel likes the tiger.
Unknown
random
[@0: The squirrel likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "tiger" "+")
@0: The bear needs the tiger.[(triple1)] The cat is round.[(triple2)] The squirrel needs the tiger.[(triple3)] The tiger likes the squirrel.[(triple4)] @1: The tiger needs the cat.[(((triple1) -> rule3) OR ((triple3) -> rule3))] @2: The tiger likes the bear.[(((((triple1) -> rule3)) -> rule2) OR ((((triple3) -> rule3)) -> rule2))] @3: The bear likes the cat.[(((((((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((((triple3) -> rule3)) -> rule2)) -> rule1))]
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple3
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple4
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((triple1) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
((triple3) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3