The cat is young. The cat needs the mouse. The lion is rough. The lion is not young. The lion needs the rabbit. The mouse eats the rabbit. The mouse is not rough. The mouse needs the cat. The mouse visits the cat. The rabbit eats the cat. The rabbit eats the mouse. The rabbit is blue. The rabbit is red. The rabbit is rough. The rabbit needs the mouse. If the lion is young and the lion eats the cat then the lion needs the mouse. If something needs the lion and it eats the rabbit then the lion eats the mouse. If something needs the mouse and the mouse needs the cat then the mouse needs the lion.
The cat is young.
("cat" "is" "young" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If the lion is young and the lion eats the cat then the lion needs the mouse.
((("lion" "is" "young" "+") ("lion" "eats" "cat" "+")) -> ("lion" "needs" "mouse" "+"))
If something needs the lion and it eats the rabbit then the lion eats the mouse.
((("something" "needs" "lion" "+") ("something" "eats" "rabbit" "+")) -> ("lion" "eats" "mouse" "+"))
If something needs the mouse and the mouse needs the cat then the mouse needs the lion.
((("something" "needs" "mouse" "+") ("mouse" "needs" "cat" "+")) -> ("mouse" "needs" "lion" "+"))
The rabbit is blue.
True
1
proof
[(triple12)]
("rabbit" "is" "blue" "+")
triple12
The mouse does not need the cat.
False
1
inv-proof
[(triple8)]
("mouse" "needs" "cat" "-")
triple8
The mouse needs the lion.
True
3
proof
[(((triple15 triple8) -> rule3) OR ((triple2 triple8) -> rule3))]
("mouse" "needs" "lion" "+")
((triple15 triple8) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
((triple2 triple8) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not need the lion.
False
3
inv-proof
[(((triple15 triple8) -> rule3) OR ((triple2 triple8) -> rule3))]
("mouse" "needs" "lion" "-")
((triple15 triple8) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
((triple2 triple8) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion eats the mouse.
True
5
proof
[(((((triple15 triple8) -> rule3) triple6) -> rule2) OR ((((triple2 triple8) -> rule3) triple6) -> rule2))]
("lion" "eats" "mouse" "+")
((((triple15 triple8) -> (rule3 % int2)) triple6) -> (rule2 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple2 triple8) -> (rule3 % int2)) triple6) -> (rule2 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion does not eat the mouse.
False
5
inv-proof
[(((((triple15 triple8) -> rule3) triple6) -> rule2) OR ((((triple2 triple8) -> rule3) triple6) -> rule2))]
("lion" "eats" "mouse" "-")
((((triple15 triple8) -> (rule3 % int2)) triple6) -> (rule2 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple2 triple8) -> (rule3 % int2)) triple6) -> (rule2 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion does not need the mouse.
Unknown
inv-rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "mouse" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The mouse eats the cat.
Unknown
random
[@0: The mouse eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cat" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
@0: The cat is young.[(triple1)] The cat needs the mouse.[(triple2)] The lion is not young.[(triple4)] The lion is rough.[(triple3)] The lion needs the rabbit.[(triple5)] The mouse eats the rabbit.[(triple6)] The mouse is not rough.[(triple7)] The mouse needs the cat.[(triple8)] The mouse visits the cat.[(triple9)] The rabbit eats the cat.[(triple10)] The rabbit eats the mouse.[(triple11)] The rabbit is blue.[(triple12)] The rabbit is red.[(triple13)] The rabbit is rough.[(triple14)] The rabbit needs the mouse.[(triple15)] @1: The mouse needs the lion.[(((triple15 triple8) -> rule3) OR ((triple2 triple8) -> rule3))] @2: The lion eats the mouse.[(((((triple15 triple8) -> rule3) triple6) -> rule2) OR ((((triple2 triple8) -> rule3) triple6) -> rule2))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The lion is not young.
("lion" "is" "young" "-")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple5
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple6
The mouse is not rough.
("mouse" "is" "rough" "-")
triple7
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple8
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple9
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple10
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple11
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple13
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple14
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple15
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple15 triple8) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
((triple2 triple8) -> (rule3 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((((triple15 triple8) -> (rule3 % int2)) triple6) -> (rule2 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple2 triple8) -> (rule3 % int2)) triple6) -> (rule2 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2