The lion chases the mouse. The lion is green. The lion is kind. The lion is rough. The lion is round. The lion is young. The lion needs the mouse. The lion sees the mouse. The mouse chases the lion. The mouse is kind. The mouse is rough. The mouse is round. The mouse is young. The mouse needs the lion. The mouse sees the lion. If someone is green and they see the mouse then the mouse sees the lion. If someone chases the mouse then the mouse chases the lion. If someone needs the mouse and the mouse chases the lion then the lion sees the mouse. If someone is young and they chase the mouse then they see the mouse. If someone sees the lion then the lion is kind. If the lion is young then the lion chases the mouse.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If someone is green and they see the mouse then the mouse sees the lion.
((("someone" "is" "green" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If someone chases the mouse then the mouse chases the lion.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If someone needs the mouse and the mouse chases the lion then the lion sees the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "chases" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If someone is young and they chase the mouse then they see the mouse.
((("someone" "is" "young" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the lion then the lion is kind.
((("someone" "sees" "lion" "+")) -> ("lion" "is" "kind" "+"))
If the lion is young then the lion chases the mouse.
((("lion" "is" "young" "+")) -> ("lion" "chases" "mouse" "+"))
The lion needs the mouse.
True
1
proof
[(triple7)]
("lion" "needs" "mouse" "+")
triple7
The lion does not see the mouse.
False
1
inv-proof
[(triple8 OR ((triple6 triple1) -> rule4) OR ((triple7 triple9) -> rule3) OR ((triple6 ((triple6) -> rule6)) -> rule4) OR ((triple7 ((triple1) -> rule2)) -> rule3) OR ((triple7 ((((triple6) -> rule6)) -> rule2)) -> rule3))]
("lion" "sees" "mouse" "-")
triple8
((triple6 triple1) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
((triple7 triple9) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
((triple7 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
((triple7 ((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The lion chases the mouse.[(triple1 OR ((triple6) -> rule6))] The lion is green.[(triple2)] The lion is kind.[(triple3 OR ((triple15) -> rule5) OR ((((triple2 triple8) -> rule1)) -> rule5) OR ((((triple2 ((triple6 triple1) -> rule4)) -> rule1)) -> rule5) OR ((((triple2 ((triple7 triple9) -> rule3)) -> rule1)) -> rule5) OR ((((triple2 ((triple6 ((triple6) -> rule6)) -> rule4)) -> rule1)) -> rule5) OR ((((triple2 ((triple7 ((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5) OR ((((triple2 ((triple7 ((((triple6) -> rule6)) -> rule2)) -> rule3)) -> rule1)) -> rule5))] The lion is rough.[(triple4)] The lion is round.[(triple5)] The lion is young.[(triple6)] The lion needs the mouse.[(triple7)] The lion sees the mouse.[(triple8 OR ((triple6 triple1) -> rule4) OR ((triple7 triple9) -> rule3) OR ((triple6 ((triple6) -> rule6)) -> rule4) OR ((triple7 ((triple1) -> rule2)) -> rule3) OR ((triple7 ((((triple6) -> rule6)) -> rule2)) -> rule3))] The mouse chases the lion.[(triple9 OR ((triple1) -> rule2) OR ((((triple6) -> rule6)) -> rule2))] The mouse is kind.[(triple10)] The mouse is rough.[(triple11)] The mouse is round.[(triple12)] The mouse is young.[(triple13)] The mouse needs the lion.[(triple14)] The mouse sees the lion.[(triple15 OR ((triple2 triple8) -> rule1) OR ((triple2 ((triple6 triple1) -> rule4)) -> rule1) OR ((triple2 ((triple7 triple9) -> rule3)) -> rule1) OR ((triple2 ((triple6 ((triple6) -> rule6)) -> rule4)) -> rule1) OR ((triple2 ((triple7 ((triple1) -> rule2)) -> rule3)) -> rule1) OR ((triple2 ((triple7 ((((triple6) -> rule6)) -> rule2)) -> rule3)) -> rule1))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
((triple6) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple15) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple2 triple8) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
((((triple2 ((triple6 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
((((triple2 ((triple7 triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
((((triple2 ((triple6 ((triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int4
((((triple2 ((triple7 ((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int4
((((triple2 ((triple7 ((((triple6) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int4
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int5
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple8
((triple6 triple1) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
((triple7 triple9) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
((triple7 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
((triple7 ((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple9
((triple1) -> (rule2 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple14
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple15
((triple2 triple8) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
((triple2 ((triple6 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((triple2 ((triple7 triple9) -> (rule3 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((triple2 ((triple6 ((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int3
((triple2 ((triple7 ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
((triple2 ((triple7 ((((triple6) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int4