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