The bear chases the dog. The bear is round. The bear visits the squirrel. The dog chases the rabbit. The dog chases the squirrel. The dog is big. The dog sees the bear. The dog sees the squirrel. The rabbit chases the squirrel. The rabbit is not big. The rabbit is kind. The rabbit is round. The rabbit sees the bear. The squirrel is big. The squirrel sees the bear. If the dog visits the bear and the dog visits the squirrel then the squirrel sees the dog. If something chases the bear then the bear does not chase the rabbit. If something sees the bear then it chases the bear. If the dog is round then the dog sees the squirrel. If the rabbit visits the squirrel then the rabbit is red. If something sees the dog then the dog does not see the bear. If something is red and it visits the rabbit then the rabbit visits the dog. If something visits the dog and it does not visit the rabbit then it is round.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is round.
("bear" "is" "round" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is big.
("dog" "is" "big" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If the dog visits the bear and the dog visits the squirrel then the squirrel sees the dog.
((("dog" "visits" "bear" "+") ("dog" "visits" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If something chases the bear then the bear does not chase the rabbit.
((("something" "chases" "bear" "+")) -> ("bear" "chases" "rabbit" "-"))
If something sees the bear then it chases the bear.
((("something" "sees" "bear" "+")) -> ("something" "chases" "bear" "+"))
If the dog is round then the dog sees the squirrel.
((("dog" "is" "round" "+")) -> ("dog" "sees" "squirrel" "+"))
If the rabbit visits the squirrel then the rabbit is red.
((("rabbit" "visits" "squirrel" "+")) -> ("rabbit" "is" "red" "+"))
If something sees the dog then the dog does not see the bear.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "bear" "-"))
If something is red and it visits the rabbit then the rabbit visits the dog.
((("something" "is" "red" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If something visits the dog and it does not visit the rabbit then it is round.
((("something" "visits" "dog" "+") ("something" "visits" "rabbit" "~")) -> ("something" "is" "round" "+"))
The squirrel is big.
True
1
proof
[(triple14)]
("squirrel" "is" "big" "+")
triple14
The dog is not big.
False
1
inv-proof
[(triple6)]
("dog" "is" "big" "-")
triple6
The squirrel chases the bear.
True
2
proof
[(((triple15) -> rule3))]
("squirrel" "chases" "bear" "+")
((triple15) -> (rule3 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel does not chase the bear.
False
2
inv-proof
[(((triple15) -> rule3))]
("squirrel" "chases" "bear" "-")
((triple15) -> (rule3 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The bear does not chase the rabbit.
True
3
proof
[(((((triple13) -> rule3)) -> rule2) OR ((((triple15) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("bear" "chases" "rabbit" "-")
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The bear chases the rabbit.
False
3
inv-proof
[(((((triple13) -> rule3)) -> rule2) OR ((((triple15) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("bear" "chases" "rabbit" "+")
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The rabbit does not visit the dog.
Unknown
inv-rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "visits" "dog" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "bear" "+")
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear chases the dog.[(triple1)] The bear is round.[(triple2)] The bear visits the squirrel.[(triple3)] The dog chases the rabbit.[(triple4)] The dog chases the squirrel.[(triple5)] The dog is big.[(triple6)] The dog sees the bear.[(triple7)] The dog sees the squirrel.[(triple8)] The rabbit chases the squirrel.[(triple9)] The rabbit is kind.[(triple11)] The rabbit is not big.[(triple10)] The rabbit is round.[(triple12)] The rabbit sees the bear.[(triple13)] The squirrel is big.[(triple14)] The squirrel sees the bear.[(triple15)] @1: The dog chases the bear.[(((triple7) -> rule3))] The rabbit chases the bear.[(((triple13) -> rule3))] The squirrel chases the bear.[(((triple15) -> rule3))] @2: The bear does not chase the rabbit.[(((((triple13) -> rule3)) -> rule2) OR ((((triple15) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple4
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple5
The dog is big.
("dog" "is" "big" "+")
triple6
The dog sees the bear.
("dog" "sees" "bear" "+")
triple7
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple8
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is not big.
("rabbit" "is" "big" "-")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple12
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple13
The squirrel is big.
("squirrel" "is" "big" "+")
triple14
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple15
The dog chases the bear.
("dog" "chases" "bear" "+")
((triple7) -> (rule3 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple13) -> (rule3 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((triple15) -> (rule3 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2