The lion is blue. The lion does not see the tiger. The mouse chases the lion. The mouse sees the rabbit. The mouse sees the tiger. The mouse visits the lion. The mouse does not visit the rabbit. The rabbit is young. The rabbit visits the mouse. The tiger does not chase the lion. The tiger chases the mouse. The tiger does not chase the rabbit. The tiger is not blue. The tiger does not see the rabbit. The tiger visits the lion. If someone sees the lion and the lion does not see the tiger then the tiger sees the mouse. If someone visits the mouse then the mouse sees the rabbit. If someone visits the mouse then the mouse sees the lion.
The lion is blue.
("lion" "is" "blue" "+")
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone sees the lion and the lion does not see the tiger then the tiger sees the mouse.
((("someone" "sees" "lion" "+") ("lion" "sees" "tiger" "~")) -> ("tiger" "sees" "mouse" "+"))
If someone visits the mouse then the mouse sees the rabbit.
((("someone" "visits" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone visits the mouse then the mouse sees the lion.
((("someone" "visits" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
The tiger chases the mouse.
True
1
proof
[(triple11)]
("tiger" "chases" "mouse" "+")
triple11
The tiger does not chase the mouse.
False
1
inv-proof
[(triple11)]
("tiger" "chases" "mouse" "-")
triple11
The mouse sees the lion.
True
2
proof
[(((triple9) -> rule3))]
("mouse" "sees" "lion" "+")
((triple9) -> (rule3 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse does not see the lion.
False
2
inv-proof
[(((triple9) -> rule3))]
("mouse" "sees" "lion" "-")
((triple9) -> (rule3 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The tiger sees the mouse.
True
4
proof
[(((((triple9) -> rule3) triple2) -> rule1))]
("tiger" "sees" "mouse" "+")
((((triple9) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The tiger does not see the mouse.
False
4
inv-proof
[(((((triple9) -> rule3) triple2) -> rule1))]
("tiger" "sees" "mouse" "-")
((((triple9) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The rabbit does not visit the tiger.
Unknown
inv-random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The rabbit does not visit the lion.
Unknown
inv-random
[@0: The rabbit visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "lion" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
@0: The lion does not see the tiger.[(triple2)] The lion is blue.[(triple1)] The mouse chases the lion.[(triple3)] The mouse does not visit the rabbit.[(triple7)] The mouse sees the rabbit.[(triple4 OR ((triple9) -> rule2))] The mouse sees the tiger.[(triple5)] The mouse visits the lion.[(triple6)] The rabbit is young.[(triple8)] The rabbit visits the mouse.[(triple9)] The tiger chases the mouse.[(triple11)] The tiger does not chase the lion.[(triple10)] The tiger does not chase the rabbit.[(triple12)] The tiger does not see the rabbit.[(triple14)] The tiger is not blue.[(triple13)] The tiger visits the lion.[(triple15)] @1: The mouse sees the lion.[(((triple9) -> rule3))] @2: The tiger sees the mouse.[(((((triple9) -> rule3) triple2) -> rule1))]
The lion does not see the tiger.
("lion" "sees" "tiger" "-")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple7
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple4
((triple9) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple5
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple8
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple9
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple11
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
triple10
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
triple12
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
triple14
The tiger is not blue.
("tiger" "is" "blue" "-")
triple13
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple9) -> (rule3 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((((triple9) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2