The cat chases the mouse. The cat chases the tiger. The cat is nice. The cat does not see the mouse. The cat sees the tiger. The lion likes the mouse. The lion does not see the mouse. The mouse does not chase the cat. The mouse is kind. The mouse sees the cat. The tiger is nice. The tiger does not see the mouse. If the lion chases the mouse then the lion is nice. If something chases the cat and it chases the mouse then it sees the cat. If something sees the tiger then the tiger chases the cat. If the mouse chases the cat then the mouse is rough. If the mouse sees the cat and the mouse sees the tiger then the tiger is kind. If something likes the mouse and it likes the cat then the cat chases the tiger. If something likes the tiger and it is not nice then the tiger likes the mouse. If something sees the cat and the cat chases the tiger then it likes the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
If the lion chases the mouse then the lion is nice.
((("lion" "chases" "mouse" "+")) -> ("lion" "is" "nice" "+"))
If something chases the cat and it chases the mouse then it sees the cat.
((("something" "chases" "cat" "+") ("something" "chases" "mouse" "+")) -> ("something" "sees" "cat" "+"))
If something sees the tiger then the tiger chases the cat.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "cat" "+"))
If the mouse chases the cat then the mouse is rough.
((("mouse" "chases" "cat" "+")) -> ("mouse" "is" "rough" "+"))
If the mouse sees the cat and the mouse sees the tiger then the tiger is kind.
((("mouse" "sees" "cat" "+") ("mouse" "sees" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If something likes the mouse and it likes the cat then the cat chases the tiger.
((("something" "likes" "mouse" "+") ("something" "likes" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If something likes the tiger and it is not nice then the tiger likes the mouse.
((("something" "likes" "tiger" "+") ("something" "is" "nice" "~")) -> ("tiger" "likes" "mouse" "+"))
If something sees the cat and the cat chases the tiger then it likes the mouse.
((("something" "sees" "cat" "+") ("cat" "chases" "tiger" "+")) -> ("something" "likes" "mouse" "+"))
The mouse is kind.
True
1
proof
[(triple9)]
("mouse" "is" "kind" "+")
triple9
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The tiger chases the cat.
True
2
proof
[(((triple5) -> rule3))]
("tiger" "chases" "cat" "+")
((triple5) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger does not chase the cat.
False
2
inv-proof
[(((triple5) -> rule3))]
("tiger" "chases" "cat" "-")
((triple5) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "kind" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "nice" "+")
The mouse does not chase the lion.
Unknown
inv-random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat chases the mouse.[(triple1)] The cat chases the tiger.[(triple2)] The cat does not see the mouse.[(triple4)] The cat is nice.[(triple3)] The cat sees the tiger.[(triple5)] The lion does not see the mouse.[(triple7)] The lion likes the mouse.[(triple6)] The mouse does not chase the cat.[(triple8)] The mouse is kind.[(triple9)] The mouse sees the cat.[(triple10)] The tiger does not see the mouse.[(triple12)] The tiger is nice.[(triple11)] @1: The mouse likes the mouse.[(((triple10 triple2) -> rule8))] The tiger chases the cat.[(((triple5) -> rule3))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple6
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple10
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple10 triple2) -> (rule8 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple5) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1