The bear is round. The cat sees the squirrel. The dog does not chase the squirrel. The squirrel is young. Young people are green. If someone sees the bear then they chase the bear. If someone chases the cat then they are cold. If someone likes the cat and they are rough then the cat is not rough. All young people are rough. If the bear does not chase the cat then the cat chases the bear. If someone likes the squirrel then they chase the squirrel. If the squirrel is rough then the squirrel sees the bear.
The bear is round.
("bear" "is" "round" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone sees the bear then they chase the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the cat then they are cold.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the cat and they are rough then the cat is not rough.
((("someone" "likes" "cat" "+") ("someone" "is" "rough" "+")) -> ("cat" "is" "rough" "-"))
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If the bear does not chase the cat then the cat chases the bear.
((("bear" "chases" "cat" "~")) -> ("cat" "chases" "bear" "+"))
If someone likes the squirrel then they chase the squirrel.
((("someone" "likes" "squirrel" "+")) -> ("someone" "chases" "squirrel" "+"))
If the squirrel is rough then the squirrel sees the bear.
((("squirrel" "is" "rough" "+")) -> ("squirrel" "sees" "bear" "+"))
The dog does not chase the squirrel.
True
1
proof
[(triple3)]
("dog" "chases" "squirrel" "-")
triple3
The dog chases the squirrel.
False
1
inv-proof
[(triple3)]
("dog" "chases" "squirrel" "+")
triple3
The squirrel is green.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "is" "green" "+")
((triple4) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple4) -> rule5))]
("squirrel" "is" "rough" "-")
((triple4) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the bear.
True
3
proof
[(((((triple4) -> rule5)) -> rule8))]
("squirrel" "sees" "bear" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not see the bear.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule8))]
("squirrel" "sees" "bear" "-")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the bear.
True
4
proof
[(((((((triple4) -> rule5)) -> rule8)) -> rule2))]
("squirrel" "chases" "bear" "+")
((((((triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel does not chase the bear.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule8)) -> rule2))]
("squirrel" "chases" "bear" "-")
((((((triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "green" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "cold" "+")
The dog does not chase the bear.
Unknown
inv-rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "bear" "-")
The cat chases the bear.
Unknown
rconc
[@1: The cat chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "bear" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The squirrel does not chase the cat.
Unknown
inv-random
[@0: The squirrel chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cat" "-")
The squirrel chases the dog.
Unknown
random
[@0: The squirrel chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "dog" "+")
@0: The bear is round.[(triple1)] The cat sees the squirrel.[(triple2)] The dog does not chase the squirrel.[(triple3)] The squirrel is young.[(triple4)] @1: The squirrel is green.[(((triple4) -> rule1))] The squirrel is rough.[(((triple4) -> rule5))] @2: The squirrel sees the bear.[(((((triple4) -> rule5)) -> rule8))] @3: The squirrel chases the bear.[(((((((triple4) -> rule5)) -> rule8)) -> rule2))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple2
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
((triple4) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple4) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((((((triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3