The bear needs the mouse. The bear sees the mouse. The dog is green. The dog is kind. The dog sees the lion. The lion is big. The mouse is kind. If the dog sees the lion then the lion sees the mouse. If something needs the mouse and the mouse is young then the mouse needs the bear. If something is young then it sees the mouse. If something visits the lion then it visits the bear. If the bear visits the dog then the bear sees the lion. If the dog is kind then the dog visits the lion. If something visits the lion and the lion needs the mouse then the mouse visits the bear. If something visits the mouse and it visits the dog then the dog is kind.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
If the dog sees the lion then the lion sees the mouse.
((("dog" "sees" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something needs the mouse and the mouse is young then the mouse needs the bear.
((("something" "needs" "mouse" "+") ("mouse" "is" "young" "+")) -> ("mouse" "needs" "bear" "+"))
If something is young then it sees the mouse.
((("something" "is" "young" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the lion then it visits the bear.
((("something" "visits" "lion" "+")) -> ("something" "visits" "bear" "+"))
If the bear visits the dog then the bear sees the lion.
((("bear" "visits" "dog" "+")) -> ("bear" "sees" "lion" "+"))
If the dog is kind then the dog visits the lion.
((("dog" "is" "kind" "+")) -> ("dog" "visits" "lion" "+"))
If something visits the lion and the lion needs the mouse then the mouse visits the bear.
((("something" "visits" "lion" "+") ("lion" "needs" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If something visits the mouse and it visits the dog then the dog is kind.
((("something" "visits" "mouse" "+") ("something" "visits" "dog" "+")) -> ("dog" "is" "kind" "+"))
The bear needs the mouse.
True
1
proof
[(triple1)]
("bear" "needs" "mouse" "+")
triple1
The mouse is not kind.
False
1
inv-proof
[(triple7)]
("mouse" "is" "kind" "-")
triple7
The lion sees the mouse.
True
2
proof
[(((triple5) -> rule1))]
("lion" "sees" "mouse" "+")
((triple5) -> (rule1 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The dog does not visit the lion.
False
2
inv-proof
[(((triple4) -> rule6))]
("dog" "visits" "lion" "-")
((triple4) -> (rule6 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog visits the bear.
True
3
proof
[(((((triple4) -> rule6)) -> rule4))]
("dog" "visits" "bear" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog does not visit the bear.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4))]
("dog" "visits" "bear" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog does not see the mouse.
Unknown
inv-rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "mouse" "-")
The mouse needs the bear.
Unknown
rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "bear" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "bear" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The bear needs the mouse.[(triple1)] The bear sees the mouse.[(triple2)] The dog is green.[(triple3)] The dog is kind.[(triple4)] The dog sees the lion.[(triple5)] The lion is big.[(triple6)] The mouse is kind.[(triple7)] @1: The dog visits the lion.[(((triple4) -> rule6))] The lion sees the mouse.[(((triple5) -> rule1))] @2: The dog visits the bear.[(((((triple4) -> rule6)) -> rule4))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple4) -> (rule6 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((triple5) -> (rule1 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2