The bear is rough. The dog likes the bear. The mouse chases the dog. If something likes the bear and the bear likes the dog then it likes the dog. If the dog is young then the dog chases the mouse. If the mouse chases the dog then the mouse chases the bear. If something chases the mouse and it likes the bear then it likes the mouse. If something eats the mouse then the mouse eats the dog. If something chases the bear then it eats the mouse.
The bear is rough.
("bear" "is" "rough" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
If something likes the bear and the bear likes the dog then it likes the dog.
((("something" "likes" "bear" "+") ("bear" "likes" "dog" "+")) -> ("something" "likes" "dog" "+"))
If the dog is young then the dog chases the mouse.
((("dog" "is" "young" "+")) -> ("dog" "chases" "mouse" "+"))
If the mouse chases the dog then the mouse chases the bear.
((("mouse" "chases" "dog" "+")) -> ("mouse" "chases" "bear" "+"))
If something chases the mouse and it likes the bear then it likes the mouse.
((("something" "chases" "mouse" "+") ("something" "likes" "bear" "+")) -> ("something" "likes" "mouse" "+"))
If something eats the mouse then the mouse eats the dog.
((("something" "eats" "mouse" "+")) -> ("mouse" "eats" "dog" "+"))
If something chases the bear then it eats the mouse.
((("something" "chases" "bear" "+")) -> ("something" "eats" "mouse" "+"))
The dog likes the bear.
True
1
proof
[(triple2)]
("dog" "likes" "bear" "+")
triple2
The mouse does not chase the dog.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "dog" "-")
triple3
The mouse chases the bear.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "chases" "bear" "+")
((triple3) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "chases" "bear" "-")
((triple3) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse eats the mouse.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("mouse" "eats" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse does not eat the mouse.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("mouse" "eats" "mouse" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse eats the dog.
True
4
proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule5))]
("mouse" "eats" "dog" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int3
The mouse does not eat the dog.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule5))]
("mouse" "eats" "dog" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int3
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "dog" "-")
The bear eats the mouse.
Unknown
rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "mouse" "+")
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "mouse" "-")
The dog eats the mouse.
Unknown
rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "mouse" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The bear chases the mouse.
Unknown
random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "+")
The bear does not chase the dog.
Unknown
inv-random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The bear is rough.[(triple1)] The dog likes the bear.[(triple2)] The mouse chases the dog.[(triple3)] @1: The mouse chases the bear.[(((triple3) -> rule3))] @2: The mouse eats the mouse.[(((((triple3) -> rule3)) -> rule6))] @3: The mouse eats the dog.[(((((((triple3) -> rule3)) -> rule6)) -> rule5))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The dog likes the bear.
("dog" "likes" "bear" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((triple3) -> (rule3 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int3