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