The cat sees the mouse. The lion likes the mouse. The mouse does not like the lion. If something likes the mouse then it likes the lion. If something is young then it does not like the cat. If something likes the mouse then it is blue. If something is red and it does not chase the lion then it is round. If something likes the lion then the lion sees the mouse. If something likes the lion then it does not see the lion. If the mouse sees the cat then the cat is not blue. If something chases the mouse and the mouse does not like the cat then the cat sees the lion.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
If something likes the mouse then it likes the lion.
((("something" "likes" "mouse" "+")) -> ("something" "likes" "lion" "+"))
If something is young then it does not like the cat.
((("something" "is" "young" "+")) -> ("something" "likes" "cat" "-"))
If something likes the mouse then it is blue.
((("something" "likes" "mouse" "+")) -> ("something" "is" "blue" "+"))
If something is red and it does not chase the lion then it is round.
((("something" "is" "red" "+") ("something" "chases" "lion" "~")) -> ("something" "is" "round" "+"))
If something likes the lion then the lion sees the mouse.
((("something" "likes" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something likes the lion then it does not see the lion.
((("something" "likes" "lion" "+")) -> ("something" "sees" "lion" "-"))
If the mouse sees the cat then the cat is not blue.
((("mouse" "sees" "cat" "+")) -> ("cat" "is" "blue" "-"))
If something chases the mouse and the mouse does not like the cat then the cat sees the lion.
((("something" "chases" "mouse" "+") ("mouse" "likes" "cat" "~")) -> ("cat" "sees" "lion" "+"))
The lion likes the mouse.
True
1
proof
[(triple2)]
("lion" "likes" "mouse" "+")
triple2
The lion does not like the mouse.
False
1
inv-proof
[(triple2)]
("lion" "likes" "mouse" "-")
triple2
The lion likes the lion.
True
2
proof
[(((triple2) -> rule1))]
("lion" "likes" "lion" "+")
((triple2) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "likes" "lion" "-")
((triple2) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not see the lion.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("lion" "sees" "lion" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion sees the lion.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("lion" "sees" "lion" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "round" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "round" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
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 mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat sees the mouse.[(triple1)] The lion likes the mouse.[(triple2)] The mouse does not like the lion.[(triple3)] @1: The lion is blue.[(((triple2) -> rule3))] The lion likes the lion.[(((triple2) -> rule1))] @2: The lion does not see the lion.[(((((triple2) -> rule1)) -> rule6))] The lion sees the mouse.[(((((triple2) -> rule1)) -> rule5))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
triple3
The lion is blue.
("lion" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple2) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2