The dog chases the lion. The dog does not need the lion. The dog sees the mouse. The lion is nice. The lion is rough. The lion needs the mouse. The mouse chases the lion. The mouse is not rough. The mouse needs the lion. The mouse sees the dog. If someone sees the lion then the lion needs the dog. If someone sees the mouse and they need the lion then the lion is nice. If the dog sees the lion then the dog chases the mouse. If someone chases the mouse then the mouse is young. If someone sees the mouse and they are young then the mouse does not chase the dog. If someone chases the lion then the lion chases the mouse. If someone sees the dog and they do not need the lion then the lion chases the dog. If the lion sees the dog and the lion does not need the dog then the lion needs the mouse.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog does not need the lion.
("dog" "needs" "lion" "-")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If someone sees the lion then the lion needs the dog.
((("someone" "sees" "lion" "+")) -> ("lion" "needs" "dog" "+"))
If someone sees the mouse and they need the lion then the lion is nice.
((("someone" "sees" "mouse" "+") ("someone" "needs" "lion" "+")) -> ("lion" "is" "nice" "+"))
If the dog sees the lion then the dog chases the mouse.
((("dog" "sees" "lion" "+")) -> ("dog" "chases" "mouse" "+"))
If someone chases the mouse then the mouse is young.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone sees the mouse and they are young then the mouse does not chase the dog.
((("someone" "sees" "mouse" "+") ("someone" "is" "young" "+")) -> ("mouse" "chases" "dog" "-"))
If someone chases the lion then the lion chases the mouse.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
If someone sees the dog and they do not need the lion then the lion chases the dog.
((("someone" "sees" "dog" "+") ("someone" "needs" "lion" "~")) -> ("lion" "chases" "dog" "+"))
If the lion sees the dog and the lion does not need the dog then the lion needs the mouse.
((("lion" "sees" "dog" "+") ("lion" "needs" "dog" "~")) -> ("lion" "needs" "mouse" "+"))
The dog sees the mouse.
True
1
proof
[(triple3)]
("dog" "sees" "mouse" "+")
triple3
The lion does not need the mouse.
False
1
inv-proof
[(triple6)]
("lion" "needs" "mouse" "-")
triple6
The lion chases the mouse.
True
2
proof
[(((triple1) -> rule6) OR ((triple7) -> rule6))]
("lion" "chases" "mouse" "+")
((triple1) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
((triple7) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule6) OR ((triple7) -> rule6))]
("lion" "chases" "mouse" "-")
((triple1) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
((triple7) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The mouse is young.
True
3
proof
[(((((triple1) -> rule6)) -> rule4) OR ((((triple7) -> rule6)) -> rule4))]
("mouse" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The mouse is not young.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4) OR ((((triple7) -> rule6)) -> rule4))]
("mouse" "is" "young" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion does not need the dog.
Unknown
inv-rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "dog" "-")
The lion chases the dog.
Unknown
rconc
[@1: The lion chases the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "dog" "+")
The dog does not chase the mouse.
Unknown
inv-rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "mouse" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The mouse does not see the lion.
Unknown
inv-random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The dog chases the lion.[(triple1)] The dog does not need the lion.[(triple2)] The dog sees the mouse.[(triple3)] The lion is nice.[(triple4)] The lion is rough.[(triple5)] The lion needs the mouse.[(triple6)] The mouse chases the lion.[(triple7)] The mouse is not rough.[(triple8)] The mouse needs the lion.[(triple9)] The mouse sees the dog.[(triple10)] @1: The lion chases the mouse.[(((triple1) -> rule6) OR ((triple7) -> rule6))] @2: The mouse is young.[(((((triple1) -> rule6)) -> rule4) OR ((((triple7) -> rule6)) -> rule4))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog does not need the lion.
("dog" "needs" "lion" "-")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple6
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple7
The mouse is not rough.
("mouse" "is" "rough" "-")
triple8
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple9
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple10
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((triple1) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
((triple7) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2