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