The bear needs the dog. The dog sees the bear. The squirrel sees the dog. If someone sees the bear and they are red then they need the bear. If the bear needs the dog and the dog chases the squirrel then the bear needs the squirrel. If someone chases the squirrel then the squirrel is rough. If someone needs the squirrel then they chase the squirrel. If someone sees the dog then the dog chases the squirrel. All red people are young. If someone needs the bear and they are not red then the bear sees the dog. If someone chases the bear then the bear is not round.
The bear needs the dog.
("bear" "needs" "dog" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If someone sees the bear and they are red then they need the bear.
((("someone" "sees" "bear" "+") ("someone" "is" "red" "+")) -> ("someone" "needs" "bear" "+"))
If the bear needs the dog and the dog chases the squirrel then the bear needs the squirrel.
((("bear" "needs" "dog" "+") ("dog" "chases" "squirrel" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone chases the squirrel then the squirrel is rough.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If someone needs the squirrel then they chase the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone sees the dog then the dog chases the squirrel.
((("someone" "sees" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone needs the bear and they are not red then the bear sees the dog.
((("someone" "needs" "bear" "+") ("someone" "is" "red" "~")) -> ("bear" "sees" "dog" "+"))
If someone chases the bear then the bear is not round.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "round" "-"))
The squirrel sees the dog.
True
1
proof
[(triple3)]
("squirrel" "sees" "dog" "+")
triple3
The dog does not see the bear.
False
1
inv-proof
[(triple2)]
("dog" "sees" "bear" "-")
triple2
The dog chases the squirrel.
True
2
proof
[(((triple3) -> rule5))]
("dog" "chases" "squirrel" "+")
((triple3) -> (rule5 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule5))]
("dog" "chases" "squirrel" "-")
((triple3) -> (rule5 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The squirrel is rough.
True
3
proof
[(((((triple3) -> rule5)) -> rule3) OR ((((((triple1 ((triple3) -> rule5)) -> rule2)) -> rule4)) -> rule3))]
("squirrel" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
((((((triple1 ((triple3) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int4
The squirrel is not rough.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3) OR ((((((triple1 ((triple3) -> rule5)) -> rule2)) -> rule4)) -> rule3))]
("squirrel" "is" "rough" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
((((((triple1 ((triple3) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int4
The bear chases the squirrel.
True
5
proof
[(((((triple1 ((triple3) -> rule5)) -> rule2)) -> rule4))]
("bear" "chases" "squirrel" "+")
((((triple1 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int3
The bear does not chase the squirrel.
False
5
inv-proof
[(((((triple1 ((triple3) -> rule5)) -> rule2)) -> rule4))]
("bear" "chases" "squirrel" "-")
((((triple1 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int3
The squirrel does not need the bear.
Unknown
inv-rconc
[@1: The squirrel needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "bear" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "young" "+")
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "young" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The dog sees the squirrel.
Unknown
random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "+")
@0: The bear needs the dog.[(triple1)] The dog sees the bear.[(triple2)] The squirrel sees the dog.[(triple3)] @1: The dog chases the squirrel.[(((triple3) -> rule5))] @2: The bear needs the squirrel.[(((triple1 ((triple3) -> rule5)) -> rule2))] The squirrel is rough.[(((((triple3) -> rule5)) -> rule3) OR ((((((triple1 ((triple3) -> rule5)) -> rule2)) -> rule4)) -> rule3))] @3: The bear chases the squirrel.[(((((triple1 ((triple3) -> rule5)) -> rule2)) -> rule4))]
The bear needs the dog.
("bear" "needs" "dog" "+")
triple1
The dog sees the bear.
("dog" "sees" "bear" "+")
triple2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((triple3) -> (rule5 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple1 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
((((((triple1 ((triple3) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int3
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int4
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((((triple1 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int3