The bear chases the tiger. The bear is big. The bear likes the tiger. The dog is not young. The rabbit likes the dog. The tiger chases the dog. The tiger is not nice. The tiger is young. The tiger likes the rabbit. The tiger sees the dog. If something is big then it does not see the tiger. If something is kind and red then it likes the dog. All red, kind things are big. If something is kind and young then it likes the bear. If something is red and young then it likes the bear. If the bear does not see the tiger then the tiger does not chase the bear.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is big.
("bear" "is" "big" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The dog is not young.
("dog" "is" "young" "-")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something is big then it does not see the tiger.
((("something" "is" "big" "+")) -> ("something" "sees" "tiger" "-"))
If something is kind and red then it likes the dog.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "likes" "dog" "+"))
All red, kind things are big.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is kind and young then it likes the bear.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "likes" "bear" "+"))
If something is red and young then it likes the bear.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "likes" "bear" "+"))
If the bear does not see the tiger then the tiger does not chase the bear.
((("bear" "sees" "tiger" "~")) -> ("tiger" "chases" "bear" "-"))
The tiger is not nice.
True
1
proof
[(triple7)]
("tiger" "is" "nice" "-")
triple7
The tiger does not like the rabbit.
False
1
inv-proof
[(triple9)]
("tiger" "likes" "rabbit" "-")
triple9
The bear does not see the tiger.
True
2
proof
[(((triple2) -> rule1))]
("bear" "sees" "tiger" "-")
((triple2) -> (rule1 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1
The bear sees the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1
The tiger does not chase the bear.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("tiger" "chases" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
int1
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int2
The tiger chases the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("tiger" "chases" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
int1
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int2
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "big" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "big" "+")
The rabbit does not like the bear.
Unknown
inv-rconc
[@1: The rabbit likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "bear" "-")
The rabbit sees the dog.
Unknown
random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (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" "+")
@0: The bear chases the tiger.[(triple1)] The bear is big.[(triple2)] The bear likes the tiger.[(triple3)] The dog is not young.[(triple4)] The rabbit likes the dog.[(triple5)] The tiger chases the dog.[(triple6)] The tiger is not nice.[(triple7)] The tiger is young.[(triple8)] The tiger likes the rabbit.[(triple9)] The tiger sees the dog.[(triple10)] @1: The bear does not see the tiger.[(((triple2) -> rule1))] @2: The tiger does not chase the bear.[(((((triple2) -> rule1)) -> rule6))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple3
The dog is not young.
("dog" "is" "young" "-")
triple4
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple6
The tiger is not nice.
("tiger" "is" "nice" "-")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple9
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
((triple2) -> (rule1 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
int1
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int2