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