The cat is big. The cat is not blue. The cat needs the lion. The cat needs the mouse. The cat visits the squirrel. The lion is blue. The lion does not like the squirrel. The lion visits the mouse. The lion does not visit the squirrel. The mouse needs the cat. The squirrel is big. The squirrel is blue. The squirrel is cold. The squirrel likes the mouse. The squirrel needs the cat. If the mouse visits the squirrel and the mouse visits the cat then the cat visits the lion. If the lion likes the mouse and the lion visits the cat then the cat visits the squirrel. If someone needs the cat then the cat does not need the squirrel. If someone needs the squirrel and the squirrel is green then they are not blue. If someone is young then they need the lion. If someone likes the mouse and the mouse needs the lion then the mouse likes the lion. If the lion is cold then the lion is not young. If someone is young then they visit the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is not blue.
("cat" "is" "blue" "-")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If the mouse visits the squirrel and the mouse visits the cat then the cat visits the lion.
((("mouse" "visits" "squirrel" "+") ("mouse" "visits" "cat" "+")) -> ("cat" "visits" "lion" "+"))
If the lion likes the mouse and the lion visits the cat then the cat visits the squirrel.
((("lion" "likes" "mouse" "+") ("lion" "visits" "cat" "+")) -> ("cat" "visits" "squirrel" "+"))
If someone needs the cat then the cat does not need the squirrel.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "squirrel" "-"))
If someone needs the squirrel and the squirrel is green then they are not blue.
((("someone" "needs" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("someone" "is" "blue" "-"))
If someone is young then they need the lion.
((("someone" "is" "young" "+")) -> ("someone" "needs" "lion" "+"))
If someone likes the mouse and the mouse needs the lion then the mouse likes the lion.
((("someone" "likes" "mouse" "+") ("mouse" "needs" "lion" "+")) -> ("mouse" "likes" "lion" "+"))
If the lion is cold then the lion is not young.
((("lion" "is" "cold" "+")) -> ("lion" "is" "young" "-"))
If someone is young then they visit the cat.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cat" "+"))
The cat visits the squirrel.
True
1
proof
[(triple5)]
("cat" "visits" "squirrel" "+")
triple5
The lion likes the squirrel.
False
1
inv-proof
[(triple7)]
("lion" "likes" "squirrel" "+")
triple7
The cat does not need the squirrel.
True
2
proof
[(((triple10) -> rule3) OR ((triple15) -> rule3))]
("cat" "needs" "squirrel" "-")
((triple10) -> (rule3 % int1))
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
int1
((triple15) -> (rule3 % int1))
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
int1
The cat needs the squirrel.
False
2
inv-proof
[(((triple10) -> rule3) OR ((triple15) -> rule3))]
("cat" "needs" "squirrel" "+")
((triple10) -> (rule3 % int1))
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
int1
((triple15) -> (rule3 % int1))
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
int1
The mouse does not need the lion.
Unknown
inv-rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "lion" "-")
The mouse visits the cat.
Unknown
rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "visits" "cat" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cat is big.[(triple1)] The cat is not blue.[(triple2)] The cat needs the lion.[(triple3)] The cat needs the mouse.[(triple4)] The cat visits the squirrel.[(triple5)] The lion does not like the squirrel.[(triple7)] The lion does not visit the squirrel.[(triple9)] The lion is blue.[(triple6)] The lion visits the mouse.[(triple8)] The mouse needs the cat.[(triple10)] The squirrel is big.[(triple11)] The squirrel is blue.[(triple12)] The squirrel is cold.[(triple13)] The squirrel likes the mouse.[(triple14)] The squirrel needs the cat.[(triple15)] @1: The cat does not need the squirrel.[(((triple10) -> rule3) OR ((triple15) -> rule3))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is not blue.
("cat" "is" "blue" "-")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple5
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
triple7
The lion does not visit the squirrel.
("lion" "visits" "squirrel" "-")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple8
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple11
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple14
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple15
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
((triple10) -> (rule3 % int1))
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
int1
((triple15) -> (rule3 % int1))
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
int1