The cat is green. The lion sees the squirrel. The mouse likes the cat. The squirrel is young. If something sees the cat then the cat does not visit the lion. If something likes the cat then it visits the lion. If something likes the cat then the cat likes the squirrel. If something visits the lion and the lion sees the squirrel then the lion sees the cat. If something visits the mouse and the mouse likes the cat then the cat sees the mouse. If something is blue and it sees the squirrel then the squirrel visits the cat. If something sees the squirrel and the squirrel visits the lion then the squirrel is not cold. If something sees the squirrel then the squirrel sees the mouse.
The cat is green.
("cat" "is" "green" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something sees the cat then the cat does not visit the lion.
((("something" "sees" "cat" "+")) -> ("cat" "visits" "lion" "-"))
If something likes the cat then it visits the lion.
((("something" "likes" "cat" "+")) -> ("something" "visits" "lion" "+"))
If something likes the cat then the cat likes the squirrel.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
If something visits the lion and the lion sees the squirrel then the lion sees the cat.
((("something" "visits" "lion" "+") ("lion" "sees" "squirrel" "+")) -> ("lion" "sees" "cat" "+"))
If something visits the mouse and the mouse likes the cat then the cat sees the mouse.
((("something" "visits" "mouse" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If something is blue and it sees the squirrel then the squirrel visits the cat.
((("something" "is" "blue" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
If something sees the squirrel and the squirrel visits the lion then the squirrel is not cold.
((("something" "sees" "squirrel" "+") ("squirrel" "visits" "lion" "+")) -> ("squirrel" "is" "cold" "-"))
If something sees the squirrel then the squirrel sees the mouse.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "+"))
The lion sees the squirrel.
True
1
proof
[(triple2)]
("lion" "sees" "squirrel" "+")
triple2
The squirrel is not young.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "young" "-")
triple4
The squirrel sees the mouse.
True
2
proof
[(((triple2) -> rule8))]
("squirrel" "sees" "mouse" "+")
((triple2) -> (rule8 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The mouse does not visit the lion.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "visits" "lion" "-")
((triple3) -> (rule2 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The lion sees the cat.
True
4
proof
[(((((triple3) -> rule2) triple2) -> rule4))]
("lion" "sees" "cat" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
The lion does not see the cat.
False
4
inv-proof
[(((((triple3) -> rule2) triple2) -> rule4))]
("lion" "sees" "cat" "-")
((((triple3) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
The cat does not visit the lion.
True
5
proof
[(((((((triple3) -> rule2) triple2) -> rule4)) -> rule1))]
("cat" "visits" "lion" "-")
((((((triple3) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int3
The cat visits the lion.
False
5
inv-proof
[(((((((triple3) -> rule2) triple2) -> rule4)) -> rule1))]
("cat" "visits" "lion" "+")
((((((triple3) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int3
The cat does not see the mouse.
Unknown
inv-rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "mouse" "-")
The squirrel visits the cat.
Unknown
rconc
[@1: The squirrel visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "visits" "cat" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "-")
The squirrel visits the lion.
Unknown
rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "lion" "+")
The mouse does not see the cat.
Unknown
inv-random
[@0: The mouse sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cat" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The cat is green.[(triple1)] The lion sees the squirrel.[(triple2)] The mouse likes the cat.[(triple3)] The squirrel is young.[(triple4)] @1: The cat likes the squirrel.[(((triple3) -> rule3))] The mouse visits the lion.[(((triple3) -> rule2))] The squirrel sees the mouse.[(((triple2) -> rule8))] @2: The lion sees the cat.[(((((triple3) -> rule2) triple2) -> rule4))] @3: The cat does not visit the lion.[(((((((triple3) -> rule2) triple2) -> rule4)) -> rule1))]
The cat is green.
("cat" "is" "green" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((triple3) -> (rule3 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((triple3) -> (rule2 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((triple2) -> (rule8 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
The cat does not visit the lion.
("cat" "visits" "lion" "-")
((((((triple3) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int3