The bear is green. The bear is young. The bear needs the dog. The dog is round. The squirrel does not see the bear. The tiger does not need the dog. The tiger needs the squirrel. If something is red then it is green. If the bear sees the squirrel then the squirrel chases the dog. If something needs the dog then the dog sees the tiger. If something is green then it needs the squirrel. If something is round and it sees the tiger then the tiger needs the bear. If something sees the squirrel then it is rough. If the squirrel chases the tiger and the squirrel does not see the bear then the squirrel is red. If something sees the squirrel and the squirrel chases the tiger then it chases the tiger.
The bear is green.
("bear" "is" "green" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The dog is round.
("dog" "is" "round" "+")
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If the bear sees the squirrel then the squirrel chases the dog.
((("bear" "sees" "squirrel" "+")) -> ("squirrel" "chases" "dog" "+"))
If something needs the dog then the dog sees the tiger.
((("something" "needs" "dog" "+")) -> ("dog" "sees" "tiger" "+"))
If something is green then it needs the squirrel.
((("something" "is" "green" "+")) -> ("something" "needs" "squirrel" "+"))
If something is round and it sees the tiger then the tiger needs the bear.
((("something" "is" "round" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "needs" "bear" "+"))
If something sees the squirrel then it is rough.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If the squirrel chases the tiger and the squirrel does not see the bear then the squirrel is red.
((("squirrel" "chases" "tiger" "+") ("squirrel" "sees" "bear" "~")) -> ("squirrel" "is" "red" "+"))
If something sees the squirrel and the squirrel chases the tiger then it chases the tiger.
((("something" "sees" "squirrel" "+") ("squirrel" "chases" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
The tiger does not need the dog.
True
1
proof
[(triple6)]
("tiger" "needs" "dog" "-")
triple6
The bear is not young.
False
1
inv-proof
[(triple2)]
("bear" "is" "young" "-")
triple2
The bear needs the squirrel.
True
2
proof
[(((triple1) -> rule4))]
("bear" "needs" "squirrel" "+")
((triple1) -> (rule4 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The dog does not see the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("dog" "sees" "tiger" "-")
((triple3) -> (rule3 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger needs the bear.
True
4
proof
[(((triple4 ((triple3) -> rule3)) -> rule5))]
("tiger" "needs" "bear" "+")
((triple4 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger does not need the bear.
False
4
inv-proof
[(((triple4 ((triple3) -> rule3)) -> rule5))]
("tiger" "needs" "bear" "-")
((triple4 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "rough" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@3: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel is not green.
Unknown
inv-rconc
[@2: The squirrel is green.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("squirrel" "is" "green" "-")
The squirrel sees the tiger.
Unknown
random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is green.[(triple1)] The bear is young.[(triple2)] The bear needs the dog.[(triple3)] The dog is round.[(triple4)] The squirrel does not see the bear.[(triple5)] The tiger does not need the dog.[(triple6)] The tiger needs the squirrel.[(triple7)] @1: The bear needs the squirrel.[(((triple1) -> rule4))] The dog sees the tiger.[(((triple3) -> rule3))] @2: The tiger needs the bear.[(((triple4 ((triple3) -> rule3)) -> rule5))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
triple5
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
triple6
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple7
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple1) -> (rule4 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple3) -> (rule3 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((triple4 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2