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