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