The bear chases the dog. The bear is not nice. The bear is round. The bear sees the dog. The bear does not see the rabbit. The dog is round. The dog is young. The rabbit is nice. The rabbit is young. The rabbit needs the dog. The rabbit needs the tiger. The tiger does not see the bear. If something is big then it is red. If something is big and nice then it does not see the bear. If something is round and big then it sees the bear. If the bear chases the dog then the bear is young. If something sees the rabbit then it does not chase the dog. If something is big and not red then it sees the rabbit. If the tiger needs the rabbit and the tiger needs the bear then the tiger is young. If something is young then it needs the rabbit.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is not nice.
("bear" "is" "nice" "-")
The bear is round.
("bear" "is" "round" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is big and nice then it does not see the bear.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "sees" "bear" "-"))
If something is round and big then it sees the bear.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "sees" "bear" "+"))
If the bear chases the dog then the bear is young.
((("bear" "chases" "dog" "+")) -> ("bear" "is" "young" "+"))
If something sees the rabbit then it does not chase the dog.
((("something" "sees" "rabbit" "+")) -> ("something" "chases" "dog" "-"))
If something is big and not red then it sees the rabbit.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "sees" "rabbit" "+"))
If the tiger needs the rabbit and the tiger needs the bear then the tiger is young.
((("tiger" "needs" "rabbit" "+") ("tiger" "needs" "bear" "+")) -> ("tiger" "is" "young" "+"))
If something is young then it needs the rabbit.
((("something" "is" "young" "+")) -> ("something" "needs" "rabbit" "+"))
The bear is round.
True
1
proof
[(triple3)]
("bear" "is" "round" "+")
triple3
The tiger sees the bear.
False
1
inv-proof
[(triple12)]
("tiger" "sees" "bear" "+")
triple12
The dog needs the rabbit.
True
2
proof
[(((triple7) -> rule8))]
("dog" "needs" "rabbit" "+")
((triple7) -> (rule8 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "young" "-")
((triple1) -> (rule4 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the rabbit.
True
3
proof
[(((((triple1) -> rule4)) -> rule8))]
("bear" "needs" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear does not need the rabbit.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule8))]
("bear" "needs" "rabbit" "-")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The tiger sees the rabbit.
Unknown
rconc
[@1: The tiger sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not see the dog.
Unknown
inv-random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The bear chases the dog.[(triple1)] The bear does not see the rabbit.[(triple5)] The bear is not nice.[(triple2)] The bear is round.[(triple3)] The bear sees the dog.[(triple4)] The dog is round.[(triple6)] The dog is young.[(triple7)] The rabbit is nice.[(triple8)] The rabbit is young.[(triple9)] The rabbit needs the dog.[(triple10)] The rabbit needs the tiger.[(triple11)] The tiger does not see the bear.[(triple12)] @1: The bear is young.[(((triple1) -> rule4))] The dog needs the rabbit.[(((triple7) -> rule8))] The rabbit needs the rabbit.[(((triple9) -> rule8))] @2: The bear needs the rabbit.[(((((triple1) -> rule4)) -> rule8))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple5
The bear is not nice.
("bear" "is" "nice" "-")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear sees the dog.
("bear" "sees" "dog" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple9
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple10
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple11
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
triple12
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule4 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((triple7) -> (rule8 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple9) -> (rule8 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2