The bear is not big. The dog is young. The mouse chases the bear. If someone is young and they chase the bear then the bear sees the mouse. If someone is blue and they do not like the bear then the bear likes the dog. If someone chases the bear then the bear likes the dog. If someone is big and they do not chase the dog then the dog is cold. If someone sees the dog then the dog is cold. If someone chases the bear and the bear likes the dog then the dog chases the bear. If someone likes the mouse then the mouse is not big. If the bear likes the dog and the bear is not big then the bear does not like the mouse.
The bear is not big.
("bear" "is" "big" "-")
The dog is young.
("dog" "is" "young" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
If someone is young and they chase the bear then the bear sees the mouse.
((("someone" "is" "young" "+") ("someone" "chases" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone is blue and they do not like the bear then the bear likes the dog.
((("someone" "is" "blue" "+") ("someone" "likes" "bear" "~")) -> ("bear" "likes" "dog" "+"))
If someone chases the bear then the bear likes the dog.
((("someone" "chases" "bear" "+")) -> ("bear" "likes" "dog" "+"))
If someone is big and they do not chase the dog then the dog is cold.
((("someone" "is" "big" "+") ("someone" "chases" "dog" "~")) -> ("dog" "is" "cold" "+"))
If someone sees the dog then the dog is cold.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "cold" "+"))
If someone chases the bear and the bear likes the dog then the dog chases the bear.
((("someone" "chases" "bear" "+") ("bear" "likes" "dog" "+")) -> ("dog" "chases" "bear" "+"))
If someone likes the mouse then the mouse is not big.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "big" "-"))
If the bear likes the dog and the bear is not big then the bear does not like the mouse.
((("bear" "likes" "dog" "+") ("bear" "is" "big" "~")) -> ("bear" "likes" "mouse" "-"))
The dog is young.
True
1
proof
[(triple2)]
("dog" "is" "young" "+")
triple2
The bear is big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "+")
triple1
The bear likes the dog.
True
2
proof
[(((triple3) -> rule3))]
("bear" "likes" "dog" "+")
((triple3) -> (rule3 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear does not like the dog.
False
2
inv-proof
[(((triple3) -> rule3))]
("bear" "likes" "dog" "-")
((triple3) -> (rule3 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear does not like the mouse.
True
4
proof
[(((((triple3) -> rule3) triple1) -> rule8))]
("bear" "likes" "mouse" "-")
((((triple3) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The bear does not like the mouse.
("bear" "likes" "mouse" "-")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The dog does not chase the bear.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule6))]
("dog" "chases" "bear" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear sees the mouse.
True
6
proof
[(((triple2 ((triple3 ((triple3) -> rule3)) -> rule6)) -> rule1))]
("bear" "sees" "mouse" "+")
((triple2 ((triple3 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The bear does not see the mouse.
False
6
inv-proof
[(((triple2 ((triple3 ((triple3) -> rule3)) -> rule6)) -> rule1))]
("bear" "sees" "mouse" "-")
((triple2 ((triple3 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "cold" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The mouse does not see the bear.
Unknown
inv-random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "-")
The bear chases the dog.
Unknown
random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "+")
The dog does not like the mouse.
Unknown
inv-random
[@0: The dog likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "mouse" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear is not big.[(triple1)] The dog is young.[(triple2)] The mouse chases the bear.[(triple3)] @1: The bear likes the dog.[(((triple3) -> rule3))] @2: The bear does not like the mouse.[(((((triple3) -> rule3) triple1) -> rule8))] The dog chases the bear.[(((triple3 ((triple3) -> rule3)) -> rule6))] @3: The bear sees the mouse.[(((triple2 ((triple3 ((triple3) -> rule3)) -> rule6)) -> rule1))]
The bear is not big.
("bear" "is" "big" "-")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The bear likes the dog.
("bear" "likes" "dog" "+")
((triple3) -> (rule3 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear does not like the mouse.
("bear" "likes" "mouse" "-")
((((triple3) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The bear does not like the mouse.
("bear" "likes" "mouse" "-")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The dog chases the bear.
("dog" "chases" "bear" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple2 ((triple3 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3