The lion is cold. The lion is young. The lion needs the mouse. The lion sees the mouse. The mouse chases the tiger. The mouse is young. The mouse needs the tiger. The mouse sees the lion. The mouse sees the tiger. The tiger chases the lion. The tiger chases the mouse. The tiger is cold. The tiger is kind. The tiger needs the lion. The tiger sees the lion. If something needs the lion and it is kind then the lion needs the tiger. If something sees the lion then the lion is rough. If the mouse is kind then the mouse is young.
The lion is cold.
("lion" "is" "cold" "+")
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 tiger.
("mouse" "chases" "tiger" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something needs the lion and it is kind then the lion needs the tiger.
((("something" "needs" "lion" "+") ("something" "is" "kind" "+")) -> ("lion" "needs" "tiger" "+"))
If something sees the lion then the lion is rough.
((("something" "sees" "lion" "+")) -> ("lion" "is" "rough" "+"))
If the mouse is kind then the mouse is young.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "young" "+"))
The mouse chases the tiger.
True
1
proof
[(triple5)]
("mouse" "chases" "tiger" "+")
triple5
The tiger is not kind.
False
1
inv-proof
[(triple13)]
("tiger" "is" "kind" "-")
triple13
The lion needs the tiger.
True
3
proof
[(((triple14 triple13) -> rule1))]
("lion" "needs" "tiger" "+")
((triple14 triple13) -> (rule1 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion does not need the tiger.
False
3
inv-proof
[(((triple14 triple13) -> rule1))]
("lion" "needs" "tiger" "-")
((triple14 triple13) -> (rule1 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
@0: The lion is cold.[(triple1)] The lion is young.[(triple2)] The lion needs the mouse.[(triple3)] The lion sees the mouse.[(triple4)] The mouse chases the tiger.[(triple5)] The mouse is young.[(triple6)] The mouse needs the tiger.[(triple7)] The mouse sees the lion.[(triple8)] The mouse sees the tiger.[(triple9)] The tiger chases the lion.[(triple10)] The tiger chases the mouse.[(triple11)] The tiger is cold.[(triple12)] The tiger is kind.[(triple13)] The tiger needs the lion.[(triple14)] The tiger sees the lion.[(triple15)] @1: The lion is rough.[(((triple15) -> rule2) OR ((triple8) -> rule2))] The lion needs the tiger.[(((triple14 triple13) -> rule1))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple7
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple8
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple9
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple10
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple15
The lion is rough.
("lion" "is" "rough" "+")
((triple15) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple8) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((triple14 triple13) -> (rule1 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1