The bear is big. The bear is red. The bear needs the mouse. The bear needs the tiger. The bear visits the mouse. The mouse is rough. The mouse likes the bear. The tiger is big. The tiger is kind. The tiger is round. The tiger likes the bear. The tiger visits the mouse. If something is kind then it likes the mouse. If something is big and it likes the mouse then the mouse is not kind.
The bear is big.
("bear" "is" "big" "+")
The bear is red.
("bear" "is" "red" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something is kind then it likes the mouse.
((("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
If something is big and it likes the mouse then the mouse is not kind.
((("something" "is" "big" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "-"))
The tiger is round.
True
1
proof
[(triple10)]
("tiger" "is" "round" "+")
triple10
The bear is not red.
False
1
inv-proof
[(triple2)]
("bear" "is" "red" "-")
triple2
The tiger likes the mouse.
True
2
proof
[(((triple9) -> rule1))]
("tiger" "likes" "mouse" "+")
((triple9) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger does not like the mouse.
False
2
inv-proof
[(((triple9) -> rule1))]
("tiger" "likes" "mouse" "-")
((triple9) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The mouse is not kind.
True
4
proof
[(((triple8 ((triple9) -> rule1)) -> rule2))]
("mouse" "is" "kind" "-")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is not kind.
("mouse" "is" "kind" "-")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The mouse is kind.
False
4
inv-proof
[(((triple8 ((triple9) -> rule1)) -> rule2))]
("mouse" "is" "kind" "+")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is not kind.
("mouse" "is" "kind" "-")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The bear likes the tiger.
Unknown
random
[@0: The bear likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "tiger" "+")
@0: The bear is big.[(triple1)] The bear is red.[(triple2)] The bear needs the mouse.[(triple3)] The bear needs the tiger.[(triple4)] The bear visits the mouse.[(triple5)] The mouse is rough.[(triple6)] The mouse likes the bear.[(triple7)] The tiger is big.[(triple8)] The tiger is kind.[(triple9)] The tiger is round.[(triple10)] The tiger likes the bear.[(triple11)] The tiger visits the mouse.[(triple12)] @1: The tiger likes the mouse.[(((triple9) -> rule1))] @2: The mouse is not kind.[(((triple8 ((triple9) -> rule1)) -> rule2))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple4
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple11
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple12
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((triple9) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The mouse is not kind.
("mouse" "is" "kind" "-")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is not kind.
("mouse" "is" "kind" "-")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2